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

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.RightExtension F
h : E.IsPointwiseRightKanExtension
G : L.RightExtension F
f₁ f₂ : G ⟶ E
Y : D
⊢ ∀ (j : StructuredArrow Y L), f₁.left.app Y ≫ (E.coneAt Y).π.app j = f₂.left.app Y ≫ (E.coneAt Y).π.app j

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.RightExtension F
h : E.IsPointwiseRightKanExtension
G : L.RightExtension F
f₁ f₂ : G ⟶ E
Y : D
X : StructuredArrow Y L
⊢ f₁.left.app Y ≫ (E.coneAt Y).π.app X = f₂.left.app Y ≫ (E.coneAt Y).π.app X

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.RightExtension F
h : E.IsPointwiseRightKanExtension
G : L.RightExtension F
f₁ f₂ : G ⟶ E
Y : D
X : StructuredArrow Y L
eq₁ : (((whiskeringLeft C D H).obj L).map f₁.left ≫ E.hom).app X.right = G.hom.app X.right
⊢ f₁.left.app Y ≫ (E.coneAt Y).π.app X = f₂.left.app Y ≫ (E.coneAt Y).π.app X

Tactic:
have eq₂ := congr_app (CostructuredArrow.w f₂) X.right

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.RightExtension F
h : E.IsPointwiseRightKanExtension
G : L.RightExtension F
f₁ f₂ : G ⟶ E
Y : D
X : StructuredArrow Y L
eq₁ : (((whiskeringLeft C D H).obj L).map f₁.left ≫ E.hom).app X.right = G.hom.app X.right
eq₂ : (((whiskeringLeft C D H).obj L).map f₂.left ≫ E.hom).app X.right = G.hom.app X.right
⊢ f₁.left.app Y ≫ (E.coneAt Y).π.app X = f₂.left.app Y ≫ (E.coneAt Y).π.app X

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.RightExtension F
h : E.IsPointwiseRightKanExtension
G : L.RightExtension F
f₁ f₂ : G ⟶ E
⊢ 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.RightExtension F
h : E.IsPointwiseRightKanExtension
G : L.RightExtension F
f₁ f₂ : G ⟶ E
Y : D
⊢ f₁.left.app Y = f₂.left.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.RightExtension F
h : E.IsPointwiseRightKanExtension
G : L.RightExtension F
f₁ f₂ : G ⟶ E
Y : D
X : StructuredArrow Y L
⊢ f₁.left.app Y ≫ (E.coneAt Y).π.app X = f₂.left.app Y ≫ (E.coneAt Y).π.app X

Tactic:
have eq₁ := congr_app (CostructuredArrow.w f₁) X.right

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.RightExtension F
h : E.IsPointwiseRightKanExtension
G : L.RightExtension F
f₁ f₂ : G ⟶ E
Y : D
X : StructuredArrow Y L
eq₁ : (((whiskeringLeft C D H).obj L).map f₁.left ≫ E.hom).app X.right = G.hom.app X.right
⊢ f₁.left.app Y ≫ (E.coneAt Y).π.app X = f₂.left.app Y ≫ (E.coneAt Y).π.app X

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.RightExtension F
h : E.IsPointwiseRightKanExtension
G : L.RightExtension F
f₁ f₂ : G ⟶ E
Y : D
X : StructuredArrow Y L
eq₁ : (((whiskeringLeft C D H).obj L).map f₁.left ≫ E.hom).app X.right = G.hom.app X.right
eq₂ : (((whiskeringLeft C D H).obj L).map f₂.left ≫ E.hom).app X.right = G.hom.app X.right
⊢ f₁.left.app Y ≫ (E.coneAt Y).π.app X = f₂.left.app Y ≫ (E.coneAt Y).π.app X

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.RightExtension F
h : E.IsPointwiseRightKanExtension
G : L.RightExtension F
f₁ f₂ : G ⟶ E
Y : D
X : StructuredArrow Y L
eq₁ : f₁.left.app (L.obj X.right) ≫ E.hom.app X.right = G.hom.app X.right
eq₂ : f₂.left.app (L.obj X.right) ≫ E.hom.app X.right = G.hom.app X.right
⊢ f₁.left.app Y ≫ E.left.map X.hom ≫ E.hom.app X.right = f₂.left.app Y ≫ E.left.map X.hom ≫ E.hom.app X.right

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.RightExtension F
h : E.IsPointwiseRightKanExtension
G : L.RightExtension F
f₁ f₂ : G ⟶ E
Y : D
⊢ f₁.left.app Y = f₂.left.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.RightExtension F
h : E.IsPointwiseRightKanExtension
G : L.RightExtension F
f₁ f₂ : G ⟶ E
Y : D
⊢ ∀ (j : StructuredArrow Y L), f₁.left.app Y ≫ (E.coneAt Y).π.app j = f₂.left.app Y ≫ (E.coneAt Y).π.app j

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.RightExtension F
h : E.IsPointwiseRightKanExtension
G : L.RightExtension F
f₁ f₂ : G ⟶ E
Y : D
X : StructuredArrow Y L
eq₁ : f₁.left.app (L.obj X.right) ≫ E.hom.app X.right = G.hom.app X.right
eq₂ : f₂.left.app (L.obj X.right) ≫ E.hom.app X.right = G.hom.app X.right
⊢ f₁.left.app Y ≫ E.left.map X.hom ≫ E.hom.app X.right = f₂.left.app Y ≫ E.left.map X.hom ≫ E.hom.app X.right

Tactic:
simp only [assoc, ← NatTrans.naturality_assoc, eq₁, eq₂]

Result:
no goals