-- Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean
lemma IsPointwiseLeftKanExtension.hom_ext
    {G : LeftExtension L F} {f₁ f₂ : E ⟶ G} : f₁ = f₂

Proof state:
C : Type u_1
D : Type u_2
H : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_6, u_2} D
inst✝ : Category.{u_5, u_3} H
L : C ⥤ D
F : C ⥤ H
E : L.LeftExtension F
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
f₁ f₂ : E ⟶ G
⊢ f₁ = f₂

Tactic:
ext Y

Result:
case h.w.h
C : Type u_1
D : Type u_2
H : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_6, u_2} D
inst✝ : Category.{u_5, u_3} H
L : C ⥤ D
F : C ⥤ H
E : L.LeftExtension F
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
f₁ f₂ : E ⟶ G
Y : D
⊢ f₁.right.app Y = f₂.right.app Y

Proof state:
case h.w.h
C : Type u_1
D : Type u_2
H : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_6, u_2} D
inst✝ : Category.{u_5, u_3} H
L : C ⥤ D
F : C ⥤ H
E : L.LeftExtension F
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
f₁ f₂ : E ⟶ G
Y : D
X : CostructuredArrow L Y
eq₁ : E.hom.app X.left ≫ f₁.right.app (L.obj X.left) = G.hom.app X.left
eq₂ : E.hom.app X.left ≫ f₂.right.app (L.obj X.left) = G.hom.app X.left
⊢ E.hom.app X.left ≫ f₁.right.app (L.obj X.left) ≫ G.right.map X.hom =
    E.hom.app X.left ≫ f₂.right.app (L.obj X.left) ≫ G.right.map X.hom

Tactic:
rw [reassoc_of% eq₁, reassoc_of% eq₂]

Result:
no goals

Proof state:
case h.w.h
C : Type u_1
D : Type u_2
H : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_6, u_2} D
inst✝ : Category.{u_5, u_3} H
L : C ⥤ D
F : C ⥤ H
E : L.LeftExtension F
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
f₁ f₂ : E ⟶ G
Y : D
⊢ ∀ (j : CostructuredArrow L Y), (E.coconeAt Y).ι.app j ≫ f₁.right.app Y = (E.coconeAt Y).ι.app j ≫ f₂.right.app Y

Tactic:
intro X

Result:
case h.w.h
C : Type u_1
D : Type u_2
H : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_6, u_2} D
inst✝ : Category.{u_5, u_3} H
L : C ⥤ D
F : C ⥤ H
E : L.LeftExtension F
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
f₁ f₂ : E ⟶ G
Y : D
X : CostructuredArrow L Y
⊢ (E.coconeAt Y).ι.app X ≫ f₁.right.app Y = (E.coconeAt Y).ι.app X ≫ f₂.right.app Y

Proof state:
case h.w.h
C : Type u_1
D : Type u_2
H : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_6, u_2} D
inst✝ : Category.{u_5, u_3} H
L : C ⥤ D
F : C ⥤ H
E : L.LeftExtension F
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
f₁ f₂ : E ⟶ G
Y : D
⊢ f₁.right.app Y = f₂.right.app Y

Tactic:
apply (h Y).hom_ext

Result:
case h.w.h
C : Type u_1
D : Type u_2
H : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_6, u_2} D
inst✝ : Category.{u_5, u_3} H
L : C ⥤ D
F : C ⥤ H
E : L.LeftExtension F
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
f₁ f₂ : E ⟶ G
Y : D
⊢ ∀ (j : CostructuredArrow L Y), (E.coconeAt Y).ι.app j ≫ f₁.right.app Y = (E.coconeAt Y).ι.app j ≫ f₂.right.app Y

Proof state:
case h.w.h
C : Type u_1
D : Type u_2
H : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_6, u_2} D
inst✝ : Category.{u_5, u_3} H
L : C ⥤ D
F : C ⥤ H
E : L.LeftExtension F
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
f₁ f₂ : E ⟶ G
Y : D
X : CostructuredArrow L Y
eq₁ : (E.hom ≫ ((whiskeringLeft C D H).obj L).map f₁.right).app X.left = G.hom.app X.left
eq₂ : (E.hom ≫ ((whiskeringLeft C D H).obj L).map f₂.right).app X.left = G.hom.app X.left
⊢ (E.coconeAt Y).ι.app X ≫ f₁.right.app Y = (E.coconeAt Y).ι.app X ≫ f₂.right.app Y

Tactic:
dsimp at eq₁ eq₂ ⊢

Result:
case h.w.h
C : Type u_1
D : Type u_2
H : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_6, u_2} D
inst✝ : Category.{u_5, u_3} H
L : C ⥤ D
F : C ⥤ H
E : L.LeftExtension F
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
f₁ f₂ : E ⟶ G
Y : D
X : CostructuredArrow L Y
eq₁ : E.hom.app X.left ≫ f₁.right.app (L.obj X.left) = G.hom.app X.left
eq₂ : E.hom.app X.left ≫ f₂.right.app (L.obj X.left) = G.hom.app X.left
⊢ (E.hom.app X.left ≫ E.right.map X.hom) ≫ f₁.right.app Y = (E.hom.app X.left ≫ E.right.map X.hom) ≫ f₂.right.app Y

Proof state:
case h.w.h
C : Type u_1
D : Type u_2
H : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_6, u_2} D
inst✝ : Category.{u_5, u_3} H
L : C ⥤ D
F : C ⥤ H
E : L.LeftExtension F
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
f₁ f₂ : E ⟶ G
Y : D
X : CostructuredArrow L Y
eq₁ : (E.hom ≫ ((whiskeringLeft C D H).obj L).map f₁.right).app X.left = G.hom.app X.left
⊢ (E.coconeAt Y).ι.app X ≫ f₁.right.app Y = (E.coconeAt Y).ι.app X ≫ f₂.right.app Y

Tactic:
have eq₂ := congr_app (StructuredArrow.w f₂) X.left

Result:
case h.w.h
C : Type u_1
D : Type u_2
H : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_6, u_2} D
inst✝ : Category.{u_5, u_3} H
L : C ⥤ D
F : C ⥤ H
E : L.LeftExtension F
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
f₁ f₂ : E ⟶ G
Y : D
X : CostructuredArrow L Y
eq₁ : (E.hom ≫ ((whiskeringLeft C D H).obj L).map f₁.right).app X.left = G.hom.app X.left
eq₂ : (E.hom ≫ ((whiskeringLeft C D H).obj L).map f₂.right).app X.left = G.hom.app X.left
⊢ (E.coconeAt Y).ι.app X ≫ f₁.right.app Y = (E.coconeAt Y).ι.app X ≫ f₂.right.app Y

Proof state:
case h.w.h
C : Type u_1
D : Type u_2
H : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_6, u_2} D
inst✝ : Category.{u_5, u_3} H
L : C ⥤ D
F : C ⥤ H
E : L.LeftExtension F
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
f₁ f₂ : E ⟶ G
Y : D
X : CostructuredArrow L Y
eq₁ : E.hom.app X.left ≫ f₁.right.app (L.obj X.left) = G.hom.app X.left
eq₂ : E.hom.app X.left ≫ f₂.right.app (L.obj X.left) = G.hom.app X.left
⊢ (E.hom.app X.left ≫ E.right.map X.hom) ≫ f₁.right.app Y = (E.hom.app X.left ≫ E.right.map X.hom) ≫ f₂.right.app Y

Tactic:
simp only [assoc, NatTrans.naturality]

Result:
case h.w.h
C : Type u_1
D : Type u_2
H : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_6, u_2} D
inst✝ : Category.{u_5, u_3} H
L : C ⥤ D
F : C ⥤ H
E : L.LeftExtension F
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
f₁ f₂ : E ⟶ G
Y : D
X : CostructuredArrow L Y
eq₁ : E.hom.app X.left ≫ f₁.right.app (L.obj X.left) = G.hom.app X.left
eq₂ : E.hom.app X.left ≫ f₂.right.app (L.obj X.left) = G.hom.app X.left
⊢ E.hom.app X.left ≫ f₁.right.app (L.obj X.left) ≫ G.right.map X.hom =
    E.hom.app X.left ≫ f₂.right.app (L.obj X.left) ≫ G.right.map X.hom

Proof state:
case h.w.h
C : Type u_1
D : Type u_2
H : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_6, u_2} D
inst✝ : Category.{u_5, u_3} H
L : C ⥤ D
F : C ⥤ H
E : L.LeftExtension F
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
f₁ f₂ : E ⟶ G
Y : D
X : CostructuredArrow L Y
⊢ (E.coconeAt Y).ι.app X ≫ f₁.right.app Y = (E.coconeAt Y).ι.app X ≫ f₂.right.app Y

Tactic:
have eq₁ := congr_app (StructuredArrow.w f₁) X.left

Result:
case h.w.h
C : Type u_1
D : Type u_2
H : Type u_3
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_6, u_2} D
inst✝ : Category.{u_5, u_3} H
L : C ⥤ D
F : C ⥤ H
E : L.LeftExtension F
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
f₁ f₂ : E ⟶ G
Y : D
X : CostructuredArrow L Y
eq₁ : (E.hom ≫ ((whiskeringLeft C D H).obj L).map f₁.right).app X.left = G.hom.app X.left
⊢ (E.coconeAt Y).ι.app X ≫ f₁.right.app Y = (E.coconeAt Y).ι.app X ≫ f₂.right.app Y