-- Mathlib/CategoryTheory/Monoidal/NaturalTransformation.lean
@[ext]
lemma hom_ext {F G : LaxMonoidalFunctor C D} {α β : F ⟶ G} (h : α.hom = β.hom) : α = β

Proof state:
case mk.mk
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F G : LaxMonoidalFunctor C D
hom✝ : F.toFunctor ⟶ G.toFunctor
isMonoidal✝¹ : NatTrans.IsMonoidal hom✝
isMonoidal✝ : NatTrans.IsMonoidal { hom := hom✝, isMonoidal := isMonoidal✝¹ }.hom
⊢ { hom := hom✝, isMonoidal := isMonoidal✝¹ } =
    { hom := { hom := hom✝, isMonoidal := isMonoidal✝¹ }.hom, isMonoidal := isMonoidal✝ }

Tactic:
rfl

Result:
no goals

Proof state:
case mk
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F G : LaxMonoidalFunctor C D
β : F ⟶ G
hom✝ : F.toFunctor ⟶ G.toFunctor
isMonoidal✝ : NatTrans.IsMonoidal hom✝
h : { hom := hom✝, isMonoidal := isMonoidal✝ }.hom = β.hom
⊢ { hom := hom✝, isMonoidal := isMonoidal✝ } = β

Tactic:
cases β

Result:
case mk.mk
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F G : LaxMonoidalFunctor C D
hom✝¹ : F.toFunctor ⟶ G.toFunctor
isMonoidal✝¹ : NatTrans.IsMonoidal hom✝¹
hom✝ : F.toFunctor ⟶ G.toFunctor
isMonoidal✝ : NatTrans.IsMonoidal hom✝
h : { hom := hom✝¹, isMonoidal := isMonoidal✝¹ }.hom = { hom := hom✝, isMonoidal := isMonoidal✝ }.hom
⊢ { hom := hom✝¹, isMonoidal := isMonoidal✝¹ } = { hom := hom✝, isMonoidal := isMonoidal✝ }

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F G : LaxMonoidalFunctor C D
α β : F ⟶ G
h : α.hom = β.hom
⊢ α = β

Tactic:
cases α

Result:
case mk
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F G : LaxMonoidalFunctor C D
β : F ⟶ G
hom✝ : F.toFunctor ⟶ G.toFunctor
isMonoidal✝ : NatTrans.IsMonoidal hom✝
h : { hom := hom✝, isMonoidal := isMonoidal✝ }.hom = β.hom
⊢ { hom := hom✝, isMonoidal := isMonoidal✝ } = β

Proof state:
case mk.mk
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F G : LaxMonoidalFunctor C D
hom✝¹ : F.toFunctor ⟶ G.toFunctor
isMonoidal✝¹ : NatTrans.IsMonoidal hom✝¹
hom✝ : F.toFunctor ⟶ G.toFunctor
isMonoidal✝ : NatTrans.IsMonoidal hom✝
h : { hom := hom✝¹, isMonoidal := isMonoidal✝¹ }.hom = { hom := hom✝, isMonoidal := isMonoidal✝ }.hom
⊢ { hom := hom✝¹, isMonoidal := isMonoidal✝¹ } = { hom := hom✝, isMonoidal := isMonoidal✝ }

Tactic:
subst h

Result:
case mk.mk
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F G : LaxMonoidalFunctor C D
hom✝ : F.toFunctor ⟶ G.toFunctor
isMonoidal✝¹ : NatTrans.IsMonoidal hom✝
isMonoidal✝ : NatTrans.IsMonoidal { hom := hom✝, isMonoidal := isMonoidal✝¹ }.hom
⊢ { hom := hom✝, isMonoidal := isMonoidal✝¹ } =
    { hom := { hom := hom✝, isMonoidal := isMonoidal✝¹ }.hom, isMonoidal := isMonoidal✝ }