Skip to content

Commit

Permalink
Trigger CI for leanprover/lean4#3422
Browse files Browse the repository at this point in the history
  • Loading branch information
leanprover-community-mathlib4-bot committed Feb 21, 2024
2 parents 8b4e87e + e7f46cf commit 997f4a1
Showing 56 changed files with 296 additions and 156 deletions.
12 changes: 6 additions & 6 deletions Mathlib/Algebra/Category/GroupCat/Basic.lean
Original file line number Diff line number Diff line change
@@ -68,18 +68,18 @@ instance {X Y : GroupCat} : CoeFun (X ⟶ Y) fun _ => X → Y where
instance instFunLike (X Y : GroupCat) : FunLike (X ⟶ Y) X Y :=
show FunLike (X →* Y) X Y from inferInstance

-- porting note: added
-- porting note (#10756): added lemma
@[to_additive (attr := simp)]
lemma coe_id {X : GroupCat} : (𝟙 X : X → X) = id := rfl

-- porting note: added
-- porting note (#10756): added lemma
@[to_additive (attr := simp)]
lemma coe_comp {X Y Z : GroupCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl

@[to_additive]
lemma comp_def {X Y Z : GroupCat} {f : X ⟶ Y} {g : Y ⟶ Z} : f ≫ g = g.comp f := rfl

-- porting note: added
-- porting note (#10756): added lemma
@[simp] lemma forget_map (f : X ⟶ Y) : (forget GroupCat).map f = (f : X → Y) := rfl

@[to_additive (attr := ext)]
@@ -217,18 +217,18 @@ instance {X Y : CommGroupCat} : CoeFun (X ⟶ Y) fun _ => X → Y where
instance instFunLike (X Y : CommGroupCat) : FunLike (X ⟶ Y) X Y :=
show FunLike (X →* Y) X Y from inferInstance

-- porting note: added
-- porting note (#10756): added lemma
@[to_additive (attr := simp)]
lemma coe_id {X : CommGroupCat} : (𝟙 X : X → X) = id := rfl

-- porting note: added
-- porting note (#10756): added lemma
@[to_additive (attr := simp)]
lemma coe_comp {X Y Z : CommGroupCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl

@[to_additive]
lemma comp_def {X Y Z : CommGroupCat} {f : X ⟶ Y} {g : Y ⟶ Z} : f ≫ g = g.comp f := rfl

-- porting note: added
-- porting note (#10756): added lemma
@[to_additive (attr := simp)]
lemma forget_map {X Y : CommGroupCat} (f : X ⟶ Y) :
(forget CommGroupCat).map f = (f : X → Y) :=
2 changes: 1 addition & 1 deletion Mathlib/Algebra/Category/GroupWithZeroCat.lean
Original file line number Diff line number Diff line change
@@ -72,7 +72,7 @@ instance groupWithZeroConcreteCategory : ConcreteCategory GroupWithZeroCat where
map := fun f => f.toFun }
forget_faithful := ⟨fun h => DFunLike.coe_injective h⟩

-- porting note: added
-- porting note (#10756): added lemma
@[simp] lemma forget_map (f : X ⟶ Y) : (forget GroupWithZeroCat).map f = f := rfl
instance hasForgetToBipointed : HasForget₂ GroupWithZeroCat Bipointed where
forget₂ :=
2 changes: 1 addition & 1 deletion Mathlib/Algebra/Category/ModuleCat/Basic.lean
Original file line number Diff line number Diff line change
@@ -227,7 +227,7 @@ theorem comp_def (f : M ⟶ N) (g : N ⟶ U) : f ≫ g = g.comp f :=
rfl
#align Module.comp_def ModuleCat.comp_def

-- porting note: added
-- porting note (#10756): added lemma
@[simp] lemma forget_map (f : M ⟶ N) : (forget (ModuleCat R)).map f = (f : M → N) := rfl

end ModuleCat
8 changes: 4 additions & 4 deletions Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
Original file line number Diff line number Diff line change
@@ -500,7 +500,7 @@ protected def unit' : 𝟭 (ModuleCat S) ⟶ restrictScalars f ⋙ coextendScala
app Y := app' f Y
naturality Y Y' g :=
LinearMap.ext fun y : Y => LinearMap.ext fun s : S => by
-- Porting note: previously simp [CoextendScalars.map_apply]
-- Porting note (#10745): previously simp [CoextendScalars.map_apply]
simp only [ModuleCat.coe_comp, Functor.id_map, Functor.id_obj, Functor.comp_obj,
Functor.comp_map]
rw [coe_comp, coe_comp, Function.comp, Function.comp]
@@ -545,12 +545,12 @@ def restrictCoextendScalarsAdj {R : Type u₁} {S : Type u₂} [Ring R] [Ring S]
{ toFun := RestrictionCoextensionAdj.HomEquiv.fromRestriction.{u₁,u₂,v} f
invFun := RestrictionCoextensionAdj.HomEquiv.toRestriction.{u₁,u₂,v} f
left_inv := fun g => LinearMap.ext fun x : X => by
-- Porting note: once just simp
-- Porting note (#10745): once just simp
rw [RestrictionCoextensionAdj.HomEquiv.toRestriction_apply, AddHom.toFun_eq_coe,
LinearMap.coe_toAddHom, RestrictionCoextensionAdj.HomEquiv.fromRestriction_apply_apply,
one_smul]
right_inv := fun g => LinearMap.ext fun x => LinearMap.ext fun s : S => by
-- Porting note: once just simp
-- Porting note (#10745): once just simp
rw [RestrictionCoextensionAdj.HomEquiv.fromRestriction_apply_apply,
RestrictionCoextensionAdj.HomEquiv.toRestriction_apply, AddHom.toFun_eq_coe,
LinearMap.coe_toAddHom, LinearMap.map_smulₛₗ, RingHom.id_apply,
@@ -559,7 +559,7 @@ def restrictCoextendScalarsAdj {R : Type u₁} {S : Type u₂} [Ring R] [Ring S]
counit := RestrictionCoextensionAdj.counit'.{u₁,u₂,v} f
homEquiv_unit := LinearMap.ext fun y => rfl
homEquiv_counit := fun {X Y g} => LinearMap.ext <| by
-- Porting note: previously simp [RestrictionCoextensionAdj.counit']
-- Porting note (#10745): previously simp [RestrictionCoextensionAdj.counit']
intro x; dsimp
rw [coe_comp, Function.comp]
change _ = (((restrictScalars f).map g) x).toFun (1 : S)
12 changes: 6 additions & 6 deletions Mathlib/Algebra/Category/MonCat/Basic.lean
Original file line number Diff line number Diff line change
@@ -93,15 +93,15 @@ instance instFunLike (X Y : MonCat) : FunLike (X ⟶ Y) X Y :=
instance instMonoidHomClass (X Y : MonCat) : MonoidHomClass (X ⟶ Y) X Y :=
inferInstanceAs <| MonoidHomClass (X →* Y) X Y

-- porting note: added
-- porting note (#10756): added lemma
@[to_additive (attr := simp)]
lemma coe_id {X : MonCat} : (𝟙 X : X → X) = id := rfl

-- porting note: added
-- porting note (#10756): added lemma
@[to_additive (attr := simp)]
lemma coe_comp {X Y Z : MonCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl

-- porting note: added
-- porting note (#10756): added lemma
@[to_additive (attr := simp)] lemma forget_map (f : X ⟶ Y) : (forget MonCat).map f = f := rfl

@[to_additive (attr := ext)]
@@ -215,15 +215,15 @@ instance {X Y : CommMonCat} : CoeFun (X ⟶ Y) fun _ => X → Y where
instance instFunLike (X Y : CommMonCat) : FunLike (X ⟶ Y) X Y :=
show FunLike (X →* Y) X Y by infer_instance

-- porting note: added
-- porting note (#10756): added lemma
@[to_additive (attr := simp)]
lemma coe_id {X : CommMonCat} : (𝟙 X : X → X) = id := rfl

-- porting note: added
-- porting note (#10756): added lemma
@[to_additive (attr := simp)]
lemma coe_comp {X Y Z : CommMonCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl

-- porting note: added
-- porting note (#10756): added lemma
@[to_additive (attr := simp)]
lemma forget_map {X Y : CommMonCat} (f : X ⟶ Y) :
(forget CommMonCat).map f = (f : X → Y) :=
8 changes: 4 additions & 4 deletions Mathlib/Algebra/Category/Ring/Basic.lean
Original file line number Diff line number Diff line change
@@ -91,7 +91,7 @@ lemma coe_id {X : SemiRingCat} : (𝟙 X : X → X) = id := rfl
-- Porting note (#10756): added lemma
lemma coe_comp {X Y Z : SemiRingCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl

-- porting note: added
-- porting note (#10756): added lemma
@[simp] lemma forget_map (f : X ⟶ Y) : (forget SemiRingCat).map f = (f : X → Y) := rfl

lemma ext {X Y : SemiRingCat} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g :=
@@ -215,7 +215,7 @@ lemma coe_id {X : RingCat} : (𝟙 X : X → X) = id := rfl
-- Porting note (#10756): added lemma
lemma coe_comp {X Y Z : RingCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl

-- porting note: added
-- porting note (#10756): added lemma
@[simp] lemma forget_map (f : X ⟶ Y) : (forget RingCat).map f = (f : X → Y) := rfl

lemma ext {X Y : RingCat} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g :=
@@ -321,7 +321,7 @@ lemma coe_id {X : CommSemiRingCat} : (𝟙 X : X → X) = id := rfl
-- Porting note (#10756): added lemma
lemma coe_comp {X Y Z : CommSemiRingCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl

-- porting note: added
-- porting note (#10756): added lemma
@[simp] lemma forget_map (f : X ⟶ Y) : (forget CommSemiRingCat).map f = (f : X → Y) := rfl

lemma ext {X Y : CommSemiRingCat} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g :=
@@ -441,7 +441,7 @@ lemma coe_id {X : CommRingCat} : (𝟙 X : X → X) = id := rfl
-- Porting note (#10756): added lemma
lemma coe_comp {X Y Z : CommRingCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl

-- porting note: added
-- porting note (#10756): added lemma
@[simp] lemma forget_map (f : X ⟶ Y) : (forget CommRingCat).map f = (f : X → Y) := rfl

lemma ext {X Y : CommRingCat} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g :=
4 changes: 2 additions & 2 deletions Mathlib/Algebra/PUnitInstances.lean
Original file line number Diff line number Diff line change
@@ -97,12 +97,12 @@ instance normalizedGCDMonoid : NormalizedGCDMonoid PUnit where
normalize_gcd := by intros; rfl
normalize_lcm := by intros; rfl

-- Porting notes (#10618): simpNF lint: simp can prove this @[simp]
-- Porting note (#10618): simpNF lint: simp can prove this @[simp]
theorem gcd_eq : gcd x y = unit :=
rfl
#align punit.gcd_eq PUnit.gcd_eq

-- Porting notes (#10618): simpNF lint: simp can prove this @[simp]
-- Porting note (#10618): simpNF lint: simp can prove this @[simp]
theorem lcm_eq : lcm x y = unit :=
rfl
#align punit.lcm_eq PUnit.lcm_eq
5 changes: 5 additions & 0 deletions Mathlib/Algebra/Star/SelfAdjoint.lean
Original file line number Diff line number Diff line change
@@ -596,6 +596,11 @@ protected instance IsStarNormal.neg [Ring R] [StarAddMonoid R] {x : R} [IsStarNo
IsStarNormal (-x) :=
show star (-x) * -x = -x * star (-x) by simp_rw [star_neg, neg_mul_neg, star_comm_self']⟩

protected instance IsStarNormal.map {F R S : Type*} [Mul R] [Star R] [Mul S] [Star S]
[FunLike F R S] [MulHomClass F R S] [StarHomClass F R S] (f : F) (r : R) [hr : IsStarNormal r] :
IsStarNormal (f r) where
star_comm_self := by simpa [map_star] using congr(f $(hr.star_comm_self))

-- see Note [lower instance priority]
instance (priority := 100) TrivialStar.isStarNormal [Mul R] [StarMul R] [TrivialStar R]
{x : R} : IsStarNormal x :=
15 changes: 12 additions & 3 deletions Mathlib/Algebra/Star/Unitary.lean
Original file line number Diff line number Diff line change
@@ -3,7 +3,7 @@ Copyright (c) 2022 Frédéric Dupuis. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Shing Tak Lam, Frédéric Dupuis
-/
import Mathlib.Algebra.Star.Basic
import Mathlib.Algebra.Star.SelfAdjoint
import Mathlib.GroupTheory.Submonoid.Operations

#align_import algebra.star.unitary from "leanprover-community/mathlib"@"247a102b14f3cebfee126293341af5f6bed00237"
@@ -135,9 +135,18 @@ def toUnits : unitary R →* Rˣ
map_mul' _ _ := Units.ext rfl
#align unitary.to_units unitary.toUnits

theorem to_units_injective : Function.Injective (toUnits : unitary R → Rˣ) := fun _ _ h =>
theorem toUnits_injective : Function.Injective (toUnits : unitary R → Rˣ) := fun _ _ h =>
Subtype.ext <| Units.ext_iff.mp h
#align unitary.to_units_injective unitary.to_units_injective
#align unitary.to_units_injective unitary.toUnits_injective

instance instIsStarNormal (u : unitary R) : IsStarNormal u where
star_comm_self := star_mul_self u |>.trans <| (mul_star_self u).symm

instance coe_isStarNormal (u : unitary R) : IsStarNormal (u : R) where
star_comm_self := congr(Subtype.val $(star_comm_self' u))

lemma _root_.isStarNormal_of_mem_unitary {u : R} (hu : u ∈ unitary R) : IsStarNormal u :=
coe_isStarNormal ⟨u, hu⟩

end Monoid

2 changes: 1 addition & 1 deletion Mathlib/AlgebraicGeometry/Scheme.lean
Original file line number Diff line number Diff line change
@@ -59,7 +59,7 @@ def Hom (X Y : Scheme) : Type* :=
instance : Category Scheme :=
{ InducedCategory.category Scheme.toLocallyRingedSpace with Hom := Hom }

-- porting note: added to ease automation
-- porting note (#10688): added to ease automation
@[continuity]
lemma Hom.continuous {X Y : Scheme} (f : X ⟶ Y) : Continuous f.1.base := f.1.base.2

8 changes: 4 additions & 4 deletions Mathlib/AlgebraicTopology/SimplicialObject.lean
Original file line number Diff line number Diff line change
@@ -76,7 +76,7 @@ instance [HasColimits C] : HasColimits (SimplicialObject C) :=

variable {C}

-- porting note: added to ease automation
-- Porting note (#10688): added to ease automation
@[ext]
lemma hom_ext {X Y : SimplicialObject C} (f g : X ⟶ Y)
(h : ∀ (n : SimplexCategoryᵒᵖ), f.app n = g.app n) : f = g :=
@@ -300,7 +300,7 @@ variable {C}

namespace Augmented

-- porting note: added to ease automation
-- Porting note (#10688): added to ease automation
@[ext]
lemma hom_ext {X Y : Augmented C} (f g : X ⟶ Y) (h₁ : f.left = g.left) (h₂ : f.right = g.right) :
f = g :=
@@ -446,7 +446,7 @@ instance [HasColimits C] : HasColimits (CosimplicialObject C) :=

variable {C}

-- porting note: added to ease automation
-- Porting note (#10688): added to ease automation
@[ext]
lemma hom_ext {X Y : CosimplicialObject C} (f g : X ⟶ Y)
(h : ∀ (n : SimplexCategory), f.app n = g.app n) : f = g :=
@@ -672,7 +672,7 @@ variable {C}

namespace Augmented

-- porting note: added to ease automation
-- Porting note (#10688): added to ease automation
@[ext]
lemma hom_ext {X Y : Augmented C} (f g : X ⟶ Y) (h₁ : f.left = g.left) (h₂ : f.right = g.right) :
f = g :=
2 changes: 1 addition & 1 deletion Mathlib/Analysis/Normed/Group/SemiNormedGroupCat.lean
Original file line number Diff line number Diff line change
@@ -67,7 +67,7 @@ instance toAddMonoidHomClass {V W : SemiNormedGroupCat} : AddMonoidHomClass (V
map_add f := f.map_add'
map_zero f := (AddMonoidHom.mk' f.toFun f.map_add').map_zero

-- Porting note: added to ease automation
-- Porting note (#10688): added to ease automation
@[ext]
lemma ext {M N : SemiNormedGroupCat} {f₁ f₂ : M ⟶ N} (h : ∀ (x : M), f₁ x = f₂ x) : f₁ = f₂ :=
DFunLike.ext _ _ h
18 changes: 18 additions & 0 deletions Mathlib/Analysis/NormedSpace/Star/Spectrum.lean
Original file line number Diff line number Diff line change
@@ -155,6 +155,24 @@ noncomputable instance (priority := 100) : ContinuousLinearMapClass F ℂ A B :=

end StarAlgHom

namespace StarAlgEquiv

variable {F A B : Type*} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [StarRing A]
[CstarRing A] [NormedRing B] [NormedAlgebra ℂ B] [CompleteSpace B] [StarRing B] [CstarRing B]
[EquivLike F A B] [NonUnitalAlgEquivClass F ℂ A B] [StarAlgEquivClass F ℂ A B]

lemma nnnorm_map (φ : F) (a : A) : ‖φ a‖₊ = ‖a‖₊ :=
le_antisymm (StarAlgHom.nnnorm_apply_le φ a) <| by
simpa using StarAlgHom.nnnorm_apply_le (symm (φ : A ≃⋆ₐ[ℂ] B)) ((φ : A ≃⋆ₐ[ℂ] B) a)

lemma norm_map (φ : F) (a : A) : ‖φ a‖ = ‖a‖ :=
congr_arg NNReal.toReal (nnnorm_map φ a)

lemma isometry (φ : F) : Isometry φ :=
AddMonoidHomClass.isometry_of_norm φ (norm_map φ)

end StarAlgEquiv

end

namespace WeakDual
5 changes: 5 additions & 0 deletions Mathlib/Analysis/SpecificLimits/Basic.lean
Original file line number Diff line number Diff line change
@@ -624,6 +624,11 @@ theorem tendsto_nat_floor_atTop {α : Type*} [LinearOrderedSemiring α] [FloorSe
Nat.floor_mono.tendsto_atTop_atTop fun x ↦ ⟨max 0 (x + 1), by simp [Nat.le_floor_iff]⟩
#align tendsto_nat_floor_at_top tendsto_nat_floor_atTop

lemma tendsto_nat_ceil_atTop {α : Type*} [LinearOrderedSemiring α] [FloorSemiring α] :
Tendsto (fun x : α ↦ ⌈x⌉₊) atTop atTop := by
refine Nat.ceil_mono.tendsto_atTop_atTop (fun x ↦ ⟨x, ?_⟩)
simp only [Nat.ceil_natCast, le_refl]

lemma tendsto_nat_floor_mul_atTop {α : Type _} [LinearOrderedSemifield α] [FloorSemiring α]
[Archimedean α] (a : α) (ha : 0 < a) : Tendsto (fun (x:ℕ) => ⌊a * x⌋₊) atTop atTop :=
Tendsto.comp tendsto_nat_floor_atTop
4 changes: 2 additions & 2 deletions Mathlib/CategoryTheory/Comma/Arrow.lean
Original file line number Diff line number Diff line change
@@ -64,12 +64,12 @@ theorem id_right (f : Arrow T) : CommaMorphism.right (𝟙 f) = 𝟙 f.right :=
rfl
#align category_theory.arrow.id_right CategoryTheory.Arrow.id_right

-- porting note: added to ease automation
-- Porting note (#10688): added to ease automation
@[simp, reassoc]
theorem comp_left {X Y Z : Arrow T} (f : X ⟶ Y) (g : Y ⟶ Z) :
(f ≫ g).left = f.left ≫ g.left := rfl

-- porting note: added to ease automation
-- Porting note (#10688): added to ease automation
@[simp, reassoc]
theorem comp_right {X Y Z : Arrow T} (f : X ⟶ Y) (g : Y ⟶ Z) :
(f ≫ g).right = f.right ≫ g.right := rfl
2 changes: 1 addition & 1 deletion Mathlib/CategoryTheory/FintypeCat.lean
Original file line number Diff line number Diff line change
@@ -92,7 +92,7 @@ lemma hom_inv_id_apply {X Y : FintypeCat} (f : X ≅ Y) (x : X) : f.inv (f.hom x
lemma inv_hom_id_apply {X Y : FintypeCat} (f : X ≅ Y) (y : Y) : f.hom (f.inv y) = y :=
congr_fun f.inv_hom_id y

-- porting note: added to ease automation
-- Porting note (#10688): added to ease automation
@[ext]
lemma hom_ext {X Y : FintypeCat} (f g : X ⟶ Y) (h : ∀ x, f x = g x) : f = g := by
funext
2 changes: 1 addition & 1 deletion Mathlib/CategoryTheory/GradedObject.lean
Original file line number Diff line number Diff line change
@@ -70,7 +70,7 @@ instance categoryOfGradedObjects (β : Type w) : Category.{max w v} (GradedObjec
CategoryTheory.pi fun _ => C
#align category_theory.graded_object.category_of_graded_objects CategoryTheory.GradedObject.categoryOfGradedObjects

-- porting note: added to ease automation
-- Porting note (#10688): added to ease automation
@[ext]
lemma hom_ext {X Y : GradedObject β C} (f g : X ⟶ Y) (h : ∀ x, f x = g x) : f = g := by
funext
2 changes: 1 addition & 1 deletion Mathlib/CategoryTheory/Idempotents/KaroubiKaroubi.lean
Original file line number Diff line number Diff line change
@@ -28,7 +28,7 @@ namespace KaroubiKaroubi

variable (C : Type*) [Category C]

-- porting note: added to ease automation
-- Porting note (#10688): added to ease automation
@[reassoc (attr := simp)]
lemma idem_f (P : Karoubi (Karoubi C)) : P.p.f ≫ P.p.f = P.p.f := by
simpa only [hom_ext_iff, comp_f] using P.idem
2 changes: 1 addition & 1 deletion Mathlib/CategoryTheory/Limits/Shapes/Products.lean
Original file line number Diff line number Diff line change
@@ -203,7 +203,7 @@ abbrev Sigma.ι (f : β → C) [HasCoproduct f] (b : β) : f b ⟶ ∐ f :=
colimit.ι (Discrete.functor f) (Discrete.mk b)
#align category_theory.limits.sigma.ι CategoryTheory.Limits.Sigma.ι

-- porting note: added the next two lemmas to ease automation; without these lemmas,
-- porting note (#10688): added the next two lemmas to ease automation; without these lemmas,
-- `limit.hom_ext` would be applied, but the goal would involve terms
-- in `Discrete β` rather than `β` itself
@[ext 1050]
4 changes: 2 additions & 2 deletions Mathlib/CategoryTheory/Monad/Basic.lean
Original file line number Diff line number Diff line change
@@ -203,12 +203,12 @@ instance : Quiver (Monad C) where
instance : Quiver (Comonad C) where
Hom := ComonadHom

-- porting note: added to ease automation
-- Porting note (#10688): added to ease automation
@[ext]
lemma MonadHom.ext' {T₁ T₂ : Monad C} (f g : T₁ ⟶ T₂) (h : f.app = g.app) : f = g :=
MonadHom.ext f g h

-- porting note: added to ease automation
-- Porting note (#10688): added to ease automation
@[ext]
lemma ComonadHom.ext' {T₁ T₂ : Comonad C} (f g : T₁ ⟶ T₂) (h : f.app = g.app) : f = g :=
ComonadHom.ext f g h
Loading

0 comments on commit 997f4a1

Please sign in to comment.