-- Mathlib/CategoryTheory/Limits/Presheaf.lean
@[ext]
lemma hom_ext {Φ : yoneda.LeftExtension (F ⋙ yoneda)}
    (f g : Functor.LeftExtension.mk F.op.lan (compYonedaIsoYonedaCompLan F).hom ⟶ Φ) :
    f = g

Proof state:
case h.w.h.hγ
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₁, u₂} D
F : C ⥤ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type v₁), F.op.HasLeftKanExtension P
Φ : yoneda.LeftExtension (F ⋙ yoneda)
f g : Functor.LeftExtension.mk F.op.lan (compYonedaIsoYonedaCompLan F).hom ⟶ Φ
P : Cᵒᵖ ⥤ Type v₁
x : P.Elementsᵒᵖ
eq :
  (𝟭 (Cᵒᵖ ⥤ Type v₁)).map (yonedaEquiv.symm (Opposite.unop x).snd) ≫ F.op.lanUnit.app P =
    F.op.lanUnit.app (yoneda.obj (Opposite.unop (Opposite.unop x).1)) ≫
      (F.op.lan ⋙ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type v₁)).obj F.op).map (yonedaEquiv.symm (Opposite.unop x).snd)
⊢ (coconeOfRepresentable P).ι.app x ≫ F.op.lanUnit.app P ≫ whiskerLeft F.op (f.right.app P) =
    (coconeOfRepresentable P).ι.app x ≫ F.op.lanUnit.app P ≫ whiskerLeft F.op (g.right.app P)

Tactic:
have eq₁ := congr_fun (congr_app (congr_app (StructuredArrow.w f) x.unop.1.unop)
  (F.op.obj x.unop.1)) (𝟙 _)

Result:
case h.w.h.hγ
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₁, u₂} D
F : C ⥤ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type v₁), F.op.HasLeftKanExtension P
Φ : yoneda.LeftExtension (F ⋙ yoneda)
f g : Functor.LeftExtension.mk F.op.lan (compYonedaIsoYonedaCompLan F).hom ⟶ Φ
P : Cᵒᵖ ⥤ Type v₁
x : P.Elementsᵒᵖ
eq :
  (𝟭 (Cᵒᵖ ⥤ Type v₁)).map (yonedaEquiv.symm (Opposite.unop x).snd) ≫ F.op.lanUnit.app P =
    F.op.lanUnit.app (yoneda.obj (Opposite.unop (Opposite.unop x).1)) ≫
      (F.op.lan ⋙ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type v₁)).obj F.op).map (yonedaEquiv.symm (Opposite.unop x).snd)
eq₁ :
  (((Functor.LeftExtension.mk F.op.lan (compYonedaIsoYonedaCompLan F).hom).hom ≫
              ((whiskeringLeft C (Cᵒᵖ ⥤ Type v₁) (Dᵒᵖ ⥤ Type v₁)).obj yoneda).map f.right).app
          (Opposite.unop (Opposite.unop x).fst)).app
      (F.op.obj (Opposite.unop x).fst) (𝟙 (Opposite.unop (F.op.obj (Opposite.unop x).fst))) =
    (Φ.hom.app (Opposite.unop (Opposite.unop x).fst)).app (F.op.obj (Opposite.unop x).fst)
      (𝟙 (Opposite.unop (F.op.obj (Opposite.unop x).fst)))
⊢ (coconeOfRepresentable P).ι.app x ≫ F.op.lanUnit.app P ≫ whiskerLeft F.op (f.right.app P) =
    (coconeOfRepresentable P).ι.app x ≫ F.op.lanUnit.app P ≫ whiskerLeft F.op (g.right.app P)

Proof state:
case h.w.h.hγ.e_a.e_α
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₁, u₂} D
F : C ⥤ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type v₁), F.op.HasLeftKanExtension P
Φ : yoneda.LeftExtension (F ⋙ yoneda)
f g : Functor.LeftExtension.mk F.op.lan (compYonedaIsoYonedaCompLan F).hom ⟶ Φ
P : Cᵒᵖ ⥤ Type v₁
x : P.Elementsᵒᵖ
eq :
  yonedaEquiv.symm (Opposite.unop x).snd ≫ F.op.lanUnit.app P =
    F.op.lanUnit.app (yoneda.obj (Opposite.unop (Opposite.unop x).1)) ≫
      whiskerLeft F.op (F.op.lan.map (yonedaEquiv.symm (Opposite.unop x).snd))
eq₁ :
  (f.right.app (yoneda.obj (Opposite.unop (Opposite.unop x).fst))).app
      (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst)))
      (((compYonedaIsoYonedaCompLan F).hom.app (Opposite.unop (Opposite.unop x).fst)).app
        (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst))) (𝟙 (F.obj (Opposite.unop (Opposite.unop x).fst)))) =
    (Φ.hom.app (Opposite.unop (Opposite.unop x).fst)).app (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst)))
      (𝟙 (F.obj (Opposite.unop (Opposite.unop x).fst)))
eq₂ :
  (g.right.app (yoneda.obj (Opposite.unop (Opposite.unop x).fst))).app
      (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst)))
      (((compYonedaIsoYonedaCompLan F).hom.app (Opposite.unop (Opposite.unop x).fst)).app
        (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst))) (𝟙 (F.obj (Opposite.unop (Opposite.unop x).fst)))) =
    (Φ.hom.app (Opposite.unop (Opposite.unop x).fst)).app (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst)))
      (𝟙 (F.obj (Opposite.unop (Opposite.unop x).fst)))
⊢ F.op.lan.map (yonedaEquiv.symm (Opposite.unop x).snd) ≫ f.right.app P =
    F.op.lan.map (yonedaEquiv.symm (Opposite.unop x).snd) ≫ g.right.app P

Tactic:
simp only [← cancel_epi ((compYonedaIsoYonedaCompLan F).hom.app x.unop.1.unop),
  NatTrans.naturality]

Result:
case h.w.h.hγ.e_a.e_α
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₁, u₂} D
F : C ⥤ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type v₁), F.op.HasLeftKanExtension P
Φ : yoneda.LeftExtension (F ⋙ yoneda)
f g : Functor.LeftExtension.mk F.op.lan (compYonedaIsoYonedaCompLan F).hom ⟶ Φ
P : Cᵒᵖ ⥤ Type v₁
x : P.Elementsᵒᵖ
eq :
  yonedaEquiv.symm (Opposite.unop x).snd ≫ F.op.lanUnit.app P =
    F.op.lanUnit.app (yoneda.obj (Opposite.unop (Opposite.unop x).1)) ≫
      whiskerLeft F.op (F.op.lan.map (yonedaEquiv.symm (Opposite.unop x).snd))
eq₁ :
  (f.right.app (yoneda.obj (Opposite.unop (Opposite.unop x).fst))).app
      (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst)))
      (((compYonedaIsoYonedaCompLan F).hom.app (Opposite.unop (Opposite.unop x).fst)).app
        (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst))) (𝟙 (F.obj (Opposite.unop (Opposite.unop x).fst)))) =
    (Φ.hom.app (Opposite.unop (Opposite.unop x).fst)).app (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst)))
      (𝟙 (F.obj (Opposite.unop (Opposite.unop x).fst)))
eq₂ :
  (g.right.app (yoneda.obj (Opposite.unop (Opposite.unop x).fst))).app
      (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst)))
      (((compYonedaIsoYonedaCompLan F).hom.app (Opposite.unop (Opposite.unop x).fst)).app
        (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst))) (𝟙 (F.obj (Opposite.unop (Opposite.unop x).fst)))) =
    (Φ.hom.app (Opposite.unop (Opposite.unop x).fst)).app (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst)))
      (𝟙 (F.obj (Opposite.unop (Opposite.unop x).fst)))
⊢ (compYonedaIsoYonedaCompLan F).hom.app (Opposite.unop (Opposite.unop x).fst) ≫
      f.right.app (yoneda.obj (Opposite.unop (Opposite.unop x).1)) ≫
        Φ.right.map (yonedaEquiv.symm (Opposite.unop x).snd) =
    (compYonedaIsoYonedaCompLan F).hom.app (Opposite.unop (Opposite.unop x).fst) ≫
      g.right.app (yoneda.obj (Opposite.unop (Opposite.unop x).1)) ≫
        Φ.right.map (yonedaEquiv.symm (Opposite.unop x).snd)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₁, u₂} D
F : C ⥤ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type v₁), F.op.HasLeftKanExtension P
Φ : yoneda.LeftExtension (F ⋙ yoneda)
f g : Functor.LeftExtension.mk F.op.lan (compYonedaIsoYonedaCompLan F).hom ⟶ Φ
⊢ f = g

Tactic:
ext P : 3

Result:
case h.w.h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₁, u₂} D
F : C ⥤ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type v₁), F.op.HasLeftKanExtension P
Φ : yoneda.LeftExtension (F ⋙ yoneda)
f g : Functor.LeftExtension.mk F.op.lan (compYonedaIsoYonedaCompLan F).hom ⟶ Φ
P : Cᵒᵖ ⥤ Type v₁
⊢ f.right.app P = g.right.app P

Proof state:
case h.w.h.hγ
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₁, u₂} D
F : C ⥤ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type v₁), F.op.HasLeftKanExtension P
Φ : yoneda.LeftExtension (F ⋙ yoneda)
f g : Functor.LeftExtension.mk F.op.lan (compYonedaIsoYonedaCompLan F).hom ⟶ Φ
P : Cᵒᵖ ⥤ Type v₁
⊢ ∀ (j : P.Elementsᵒᵖ),
    (coconeOfRepresentable P).ι.app j ≫ F.op.lanUnit.app P ≫ whiskerLeft F.op (f.right.app P) =
      (coconeOfRepresentable P).ι.app j ≫ F.op.lanUnit.app P ≫ whiskerLeft F.op (g.right.app P)

Tactic:
intro x

Result:
case h.w.h.hγ
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₁, u₂} D
F : C ⥤ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type v₁), F.op.HasLeftKanExtension P
Φ : yoneda.LeftExtension (F ⋙ yoneda)
f g : Functor.LeftExtension.mk F.op.lan (compYonedaIsoYonedaCompLan F).hom ⟶ Φ
P : Cᵒᵖ ⥤ Type v₁
x : P.Elementsᵒᵖ
⊢ (coconeOfRepresentable P).ι.app x ≫ F.op.lanUnit.app P ≫ whiskerLeft F.op (f.right.app P) =
    (coconeOfRepresentable P).ι.app x ≫ F.op.lanUnit.app P ≫ whiskerLeft F.op (g.right.app P)