awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Pointwise (goal)
Goal:
C : Type u_1
D : Type u_2
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_1, v_4, u_1, u_4} C H
⊢ ∀ {Y₁ Y₂ : D} (e : Y₁ ≅ Y₂), L.HasPointwiseRightKanExtensionAt F Y₁ ↔ L.HasPointwiseRightKanExtensionAt F Y₂
have suffices : ∀ ⦃Y₁ Y₂ : D⦄ (x : Y₁ ≅ Y₂) [L.HasPointwiseRightKanExtensionAt F Y₁], L.HasPointwiseRightKanExtensionAt F Y₂
Tactic: suffices ∀ ⦃Y₁ Y₂ : D⦄ (_ : Y₁ ≅ Y₂) [HasPointwiseRightKanExtensionAt L F Y₁],
      HasPointwiseRightKanExtensionAt L F Y₂ from
    fun Y₁ Y₂ e => ⟨fun _ => this e, fun _ => this e.symm⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Pointwise (goal)
Goal:
C : Type u_1
D : Type u_2
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_1, v_4, u_1, u_4} C H
Y₁ Y₂ : D
e : Y₁ ≅ Y₂
inst_3 : L.HasPointwiseRightKanExtensionAt F Y₁
⊢ L.HasPointwiseRightKanExtensionAt F Y₂
have change : HasLimit (Equivalence.functor (StructuredArrow.mapIso e.symm) ⋙ StructuredArrow.proj Y₁ L ⋙ F)
Tactic: change HasLimit ((StructuredArrow.mapIso e.symm).functor ⋙ StructuredArrow.proj Y₁ L ⋙ F)
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Pointwise (goal)
Goal:
C : Type u_1
D : Type u_2
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_1, v_4, u_1, u_4} C H
L' : Functor.{v_1, v_2, u_1, u_2} C D
e : L ≅ L'
Y : D
⊢ L.HasPointwiseLeftKanExtensionAt F Y ↔ L'.HasPointwiseLeftKanExtensionAt F Y
have revert : ∀ {L L' : Functor.{v_1, v_2, u_1, u_2} C D} (e : L ≅ L'),
  L.HasPointwiseLeftKanExtensionAt F Y ↔ L'.HasPointwiseLeftKanExtensionAt F Y
Tactic: revert L L' e
Cleared hypotheses: L, L', e
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Pointwise (goal)
Goal:
C : Type u_1
D : Type u_2
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_4, u_4} H
F : Functor.{v_1, v_4, u_1, u_4} C H
Y : D
⊢ ∀ {L L' : Functor.{v_1, v_2, u_1, u_2} C D} (e : L ≅ L'),
    L.HasPointwiseLeftKanExtensionAt F Y ↔ L'.HasPointwiseLeftKanExtensionAt F Y
have suffices : ∀ ⦃L L' : Functor.{v_1, v_2, u_1, u_2} C D⦄ (x : L ≅ L') [L.HasPointwiseLeftKanExtensionAt F Y],
  L'.HasPointwiseLeftKanExtensionAt F Y
Tactic: suffices ∀ ⦃L L' : C ⥤ D⦄ (_ : L ≅ L') [HasPointwiseLeftKanExtensionAt L F Y],
      HasPointwiseLeftKanExtensionAt L' F Y from
    fun L L' e => ⟨fun _ => this e, fun _ => this e.symm⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Pointwise (goal)
Goal:
C : Type u_1
D : Type u_2
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_1, v_4, u_1, u_4} C H
L' : Functor.{v_1, v_2, u_1, u_2} C D
e : L ≅ L'
Y : D
⊢ L.HasPointwiseRightKanExtensionAt F Y ↔ L'.HasPointwiseRightKanExtensionAt F Y
have revert : ∀ {L L' : Functor.{v_1, v_2, u_1, u_2} C D} (e : L ≅ L'),
  L.HasPointwiseRightKanExtensionAt F Y ↔ L'.HasPointwiseRightKanExtensionAt F Y
Tactic: revert L L' e
Cleared hypotheses: L, L', e
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Pointwise (goal)
Goal:
C : Type u_1
D : Type u_2
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_4, u_4} H
F : Functor.{v_1, v_4, u_1, u_4} C H
Y : D
⊢ ∀ {L L' : Functor.{v_1, v_2, u_1, u_2} C D} (e : L ≅ L'),
    L.HasPointwiseRightKanExtensionAt F Y ↔ L'.HasPointwiseRightKanExtensionAt F Y
have suffices : ∀ ⦃L L' : Functor.{v_1, v_2, u_1, u_2} C D⦄ (x : L ≅ L') [L.HasPointwiseRightKanExtensionAt F Y],
  L'.HasPointwiseRightKanExtensionAt F Y
Tactic: suffices ∀ ⦃L L' : C ⥤ D⦄ (_ : L ≅ L') [HasPointwiseRightKanExtensionAt L F Y],
      HasPointwiseRightKanExtensionAt L' F Y from
    fun L L' e => ⟨fun _ => this e, fun _ => this e.symm⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Pointwise (goal)
Goal:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D'
inst_3 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
L' : Functor.{v_1, v_3, u_1, u_3} C D'
F : Functor.{v_1, v_4, u_1, u_4} C H
E : Equivalence.{v_2, v_3, u_2, u_3} D D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
inst_4 : L.HasPointwiseLeftKanExtensionAt F Y
⊢ L'.HasPointwiseLeftKanExtensionAt F Y'
have rw : (L ⋙ E.functor).HasPointwiseLeftKanExtensionAt F (E.functor.obj Y)
Tactic: rw [← hasPointwiseLeftKanExtensionAt_iff_of_natIso F eL,
    hasPointwiseLeftKanExtensionAt_iff_of_iso _ F e.symm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Pointwise (hypothesis)
Goal:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D'
inst_3 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
L' : Functor.{v_1, v_3, u_1, u_3} C D'
F : Functor.{v_1, v_4, u_1, u_4} C H
E : Equivalence.{v_2, v_3, u_2, u_3} D D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
inst_4 : L.HasPointwiseLeftKanExtensionAt F Y
Φ : CostructuredArrow L Y ⥤ CostructuredArrow (L ⋙ E.functor) (E.functor.obj Y) := CostructuredArrow.post L E.functor Y
⊢ (L ⋙ E.functor).HasPointwiseLeftKanExtensionAt F (E.functor.obj Y)
have this : HasColimit (Φ.asEquivalence.functor ⋙ CostructuredArrow.proj (L ⋙ E.functor) (E.functor.obj Y) ⋙ F)
Tactic: have : HasColimit ((asEquivalence Φ).functor ⋙
    CostructuredArrow.proj (L ⋙ E.functor) (E.functor.obj Y) ⋙ F) :=
    (inferInstance : HasPointwiseLeftKanExtensionAt L F Y)
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Pointwise (goal)
Goal:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D'
inst_3 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
L' : Functor.{v_1, v_3, u_1, u_3} C D'
F : Functor.{v_1, v_4, u_1, u_4} C H
E : Equivalence.{v_2, v_3, u_2, u_3} D D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
⊢ L.HasPointwiseLeftKanExtensionAt F Y ↔ L'.HasPointwiseLeftKanExtensionAt F Y'
have mp : L.HasPointwiseLeftKanExtensionAt F Y → L'.HasPointwiseLeftKanExtensionAt F Y'
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Pointwise (goal)
Goal:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D'
inst_3 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
L' : Functor.{v_1, v_3, u_1, u_3} C D'
F : Functor.{v_1, v_4, u_1, u_4} C H
E : Equivalence.{v_2, v_3, u_2, u_3} D D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
mp : L.HasPointwiseLeftKanExtensionAt F Y → L'.HasPointwiseLeftKanExtensionAt F Y'
⊢ L.HasPointwiseLeftKanExtensionAt F Y ↔ L'.HasPointwiseLeftKanExtensionAt F Y'
have mpr : L'.HasPointwiseLeftKanExtensionAt F Y' → L.HasPointwiseLeftKanExtensionAt F Y
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Pointwise (goal)
Goal:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D'
inst_3 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
L' : Functor.{v_1, v_3, u_1, u_3} C D'
F : Functor.{v_1, v_4, u_1, u_4} C H
E : Equivalence.{v_2, v_3, u_2, u_3} D D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
inst_4 : L.HasPointwiseRightKanExtensionAt F Y
⊢ L'.HasPointwiseRightKanExtensionAt F Y'
have rw : (L ⋙ E.functor).HasPointwiseRightKanExtensionAt F (E.functor.obj Y)
Tactic: rw [← hasPointwiseRightKanExtensionAt_iff_of_natIso F eL,
    hasPointwiseRightKanExtensionAt_iff_of_iso _ F e.symm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Pointwise (hypothesis)
Goal:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D'
inst_3 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
L' : Functor.{v_1, v_3, u_1, u_3} C D'
F : Functor.{v_1, v_4, u_1, u_4} C H
E : Equivalence.{v_2, v_3, u_2, u_3} D D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
inst_4 : L.HasPointwiseRightKanExtensionAt F Y
Φ : StructuredArrow Y L ⥤ StructuredArrow (E.functor.obj Y) (L ⋙ E.functor) := StructuredArrow.post Y L E.functor
⊢ (L ⋙ E.functor).HasPointwiseRightKanExtensionAt F (E.functor.obj Y)
have this : HasLimit (Φ.asEquivalence.functor ⋙ StructuredArrow.proj (E.functor.obj Y) (L ⋙ E.functor) ⋙ F)
Tactic: have : HasLimit ((asEquivalence Φ).functor ⋙
    StructuredArrow.proj (E.functor.obj Y) (L ⋙ E.functor) ⋙ F) :=
    (inferInstance : HasPointwiseRightKanExtensionAt L F Y)
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Pointwise (goal)
Goal:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D'
inst_3 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
L' : Functor.{v_1, v_3, u_1, u_3} C D'
F : Functor.{v_1, v_4, u_1, u_4} C H
E : Equivalence.{v_2, v_3, u_2, u_3} D D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
⊢ L.HasPointwiseRightKanExtensionAt F Y ↔ L'.HasPointwiseRightKanExtensionAt F Y'
have mp : L.HasPointwiseRightKanExtensionAt F Y → L'.HasPointwiseRightKanExtensionAt F Y'
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Pointwise (goal)
Goal:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D'
inst_3 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
L' : Functor.{v_1, v_3, u_1, u_3} C D'
F : Functor.{v_1, v_4, u_1, u_4} C H
E : Equivalence.{v_2, v_3, u_2, u_3} D D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
mp : L.HasPointwiseRightKanExtensionAt F Y → L'.HasPointwiseRightKanExtensionAt F Y'
⊢ L.HasPointwiseRightKanExtensionAt F Y ↔ L'.HasPointwiseRightKanExtensionAt F Y'
have mpr : L'.HasPointwiseRightKanExtensionAt F Y' → L.HasPointwiseRightKanExtensionAt F Y
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Pointwise (goal)
Goal:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D'
inst_3 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
L' : Functor.{v_1, v_3, u_1, u_3} C D'
F : Functor.{v_1, v_4, u_1, u_4} C H
E : L.LeftExtension F
Y : D
g₁ g₂ : CostructuredArrow L Y
φ : g₁ ⟶ g₂
⊢ (CostructuredArrow.proj L Y ⋙ F).map φ ≫ (StructuredArrow.hom E).app g₂.left ≫ (StructuredArrow.right E).map g₂.hom =
    ((StructuredArrow.hom E).app g₁.left ≫ (StructuredArrow.right E).map g₁.hom) ≫
      map (obj (const (CostructuredArrow L Y)) ((StructuredArrow.right E).obj Y)) φ
have dsimp : F.map φ.left ≫ (StructuredArrow.hom E).app g₂.left ≫ (StructuredArrow.right E).map g₂.hom =
  ((StructuredArrow.hom E).app g₁.left ≫ (StructuredArrow.right E).map g₁.hom) ≫ 𝟙 ((StructuredArrow.right E).obj Y)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Pointwise (goal)
Goal:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D'
inst_3 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
L' : Functor.{v_1, v_3, u_1, u_3} C D'
F : Functor.{v_1, v_4, u_1, u_4} C H
E : L.LeftExtension F
Y : D
g₁ g₂ : CostructuredArrow L Y
φ : g₁ ⟶ g₂
⊢ F.map φ.left ≫ (StructuredArrow.hom E).app g₂.left ≫ (StructuredArrow.right E).map g₂.hom =
    ((StructuredArrow.hom E).app g₁.left ≫ (StructuredArrow.right E).map g₁.hom) ≫ 𝟙 ((StructuredArrow.right E).obj Y)
have rw : F.map φ.left ≫ (StructuredArrow.hom E).app g₂.left ≫ (StructuredArrow.right E).map g₂.hom =
  ((StructuredArrow.hom E).app g₁.left ≫ (StructuredArrow.right E).map (L.map φ.left ≫ g₂.hom)) ≫
    𝟙 ((StructuredArrow.right E).obj Y)
Tactic: rw [← CostructuredArrow.w φ]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Pointwise (goal)
Goal:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D'
inst_3 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
L' : Functor.{v_1, v_3, u_1, u_3} C D'
F : Functor.{v_1, v_4, u_1, u_4} C H
E_1 : L.LeftExtension F
Y : D
E E' : L.LeftExtension F
φ : E ⟶ E'
G : CostructuredArrow L Y
⊢ (E.coconeAt Y).ι.app G ≫ (StructuredArrow.Hom.right φ).app Y = (E'.coconeAt Y).ι.app G
have dsimp : ((StructuredArrow.hom E).app G.left ≫ (StructuredArrow.right E).map G.hom) ≫ (StructuredArrow.Hom.right φ).app Y =
  (StructuredArrow.hom E').app G.left ≫ (StructuredArrow.right E').map G.hom
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Pointwise (goal)
Goal:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D'
inst_3 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
L' : Functor.{v_1, v_3, u_1, u_3} C D'
F : Functor.{v_1, v_4, u_1, u_4} C H
E_1 : L.LeftExtension F
Y : D
E E' : L.LeftExtension F
φ : E ⟶ E'
G : CostructuredArrow L Y
⊢ ((StructuredArrow.hom E).app G.left ≫ (StructuredArrow.right E).map G.hom) ≫ (StructuredArrow.Hom.right φ).app Y =
    (StructuredArrow.hom E').app G.left ≫ (StructuredArrow.right E').map G.hom
have rw : ((StructuredArrow.hom E).app G.left ≫ (StructuredArrow.right E).map G.hom) ≫ (StructuredArrow.Hom.right φ).app Y =
  (StructuredArrow.hom E ≫ map (obj (whiskeringLeft C D H) L) (StructuredArrow.Hom.right φ)).app G.left ≫
    (StructuredArrow.right E').map G.hom
Tactic: rw [← StructuredArrow.w φ]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Pointwise (goal)
Goal:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D'
inst_3 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
L' : Functor.{v_1, v_3, u_1, u_3} C D'
F : Functor.{v_1, v_4, u_1, u_4} C H
E : L.LeftExtension F
E' : ?m.13
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
Y₁ Y₂ : D
φ : Y₁ ⟶ Y₂
X : CostructuredArrow L Y₁
⊢ Eq (α := (CostructuredArrow.proj L Y₁ ⋙ F).obj X ⟶ (StructuredArrow.right G).obj Y₂)
    ((E.coconeAt Y₁).ι.app X ≫ (StructuredArrow.right E).map φ ≫ (h Y₂).desc (G.coconeAt Y₂) :
      (CostructuredArrow.proj L Y₁ ⋙ F).obj X ⟶ (StructuredArrow.right G).obj Y₂)
    ((E.coconeAt Y₁).ι.app X ≫ (h Y₁).desc (G.coconeAt Y₁) ≫ (StructuredArrow.right G).map φ :
      (CostructuredArrow.proj L Y₁ ⋙ F).obj X ⟶ (StructuredArrow.right G).obj Y₂)
have rw : (E.coconeAt Y₁).ι.app X ≫ (StructuredArrow.right E).map φ ≫ (h Y₂).desc (G.coconeAt Y₂) =
  (G.coconeAt Y₁).ι.app X ≫ (StructuredArrow.right G).map φ
Tactic: rw [(h Y₁).fac_assoc (coconeAt G Y₁) X]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Pointwise (goal)
Goal:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D'
inst_3 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
L' : Functor.{v_1, v_3, u_1, u_3} C D'
F : Functor.{v_1, v_4, u_1, u_4} C H
E : L.LeftExtension F
E' : ?m.13
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
⊢ StructuredArrow.hom E ≫
      map (obj (whiskeringLeft C D H) L) { app := fun (Y : D) ↦ (h Y).desc (G.coconeAt Y), naturality := ⋯ } =
    StructuredArrow.hom G
have w : ∀ (X : C),
  NatTrans.app
      (StructuredArrow.hom E ≫
        map (obj (whiskeringLeft C D H) L) { app := fun (Y : D) ↦ (h Y).desc (G.coconeAt Y), naturality := sorry })
      X =
    (StructuredArrow.hom G).app X
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Pointwise (goal)
Goal:
C : Type u_1
D : Type u_2
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_1, v_4, u_1, u_4} C H
E : L.LeftExtension F
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
f₁ f₂ : E ⟶ G
⊢ f₁ = f₂
have h₁ : ∀ (Y : D), (StructuredArrow.Hom.right f₁).app Y = (StructuredArrow.Hom.right f₂).app Y
Tactic: ext Y
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Pointwise (goal)
Goal:
C : Type u_1
D : Type u_2
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_1, v_4, u_1, u_4} C H
E : L.LeftExtension F
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
f₁ f₂ : E ⟶ G
Y : D
⊢ (StructuredArrow.Hom.right f₁).app Y = (StructuredArrow.Hom.right f₂).app Y
have h₁ : ∀ (j : CostructuredArrow L Y),
  (E.coconeAt Y).ι.app j ≫ (StructuredArrow.Hom.right f₁).app Y =
    (E.coconeAt Y).ι.app j ≫ (StructuredArrow.Hom.right f₂).app Y
Tactic: apply (h Y).hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Pointwise (hypothesis)
Goal:
C : Type u_1
D : Type u_2
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_1, v_4, u_1, u_4} 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 ≫ (StructuredArrow.Hom.right f₁).app Y =
    (E.coconeAt Y).ι.app X ≫ (StructuredArrow.Hom.right f₂).app Y
have eq₁ : Eq (α := F.obj X.left ⟶ (obj (obj (whiskeringLeft C D H) L) (StructuredArrow.right G)).obj X.left)
  ((StructuredArrow.hom E ≫ map (obj (whiskeringLeft C D H) L) (StructuredArrow.Hom.right f₁)).app X.left)
  ((StructuredArrow.hom G).app X.left)
Tactic: have eq₁ := congr_app (StructuredArrow.w f₁) X.left
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Pointwise (hypothesis)
Goal:
C : Type u_1
D : Type u_2
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_1, v_4, u_1, u_4} C H
E : L.LeftExtension F
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
f₁ f₂ : E ⟶ G
Y : D
X : CostructuredArrow L Y
eq₁ :
  Eq (α := F.obj X.left ⟶ (obj (obj (whiskeringLeft C D H) L) (StructuredArrow.right G)).obj X.left)
    ((StructuredArrow.hom E ≫ map (obj (whiskeringLeft C D H) L) (StructuredArrow.Hom.right f₁)).app X.left)
    ((StructuredArrow.hom G).app X.left)
⊢ (E.coconeAt Y).ι.app X ≫ (StructuredArrow.Hom.right f₁).app Y =
    (E.coconeAt Y).ι.app X ≫ (StructuredArrow.Hom.right f₂).app Y
have eq₂ : Eq (α := F.obj X.left ⟶ (obj (obj (whiskeringLeft C D H) L) (StructuredArrow.right G)).obj X.left)
  ((StructuredArrow.hom E ≫ map (obj (whiskeringLeft C D H) L) (StructuredArrow.Hom.right f₂)).app X.left)
  ((StructuredArrow.hom G).app X.left)
Tactic: have eq₂ := congr_app (StructuredArrow.w f₂) X.left
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Pointwise (goal)
Goal:
C : Type u_1
D : Type u_2
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_1, v_4, u_1, u_4} C H
E : L.LeftExtension F
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
f₁ f₂ : E ⟶ G
Y : D
X : CostructuredArrow L Y
eq₁ :
  Eq (α := F.obj X.left ⟶ (obj (obj (whiskeringLeft C D H) L) (StructuredArrow.right G)).obj X.left)
    ((StructuredArrow.hom E ≫ map (obj (whiskeringLeft C D H) L) (StructuredArrow.Hom.right f₁)).app X.left)
    ((StructuredArrow.hom G).app X.left)
eq₂ :
  Eq (α := F.obj X.left ⟶ (obj (obj (whiskeringLeft C D H) L) (StructuredArrow.right G)).obj X.left)
    ((StructuredArrow.hom E ≫ map (obj (whiskeringLeft C D H) L) (StructuredArrow.Hom.right f₂)).app X.left)
    ((StructuredArrow.hom G).app X.left)
⊢ (E.coconeAt Y).ι.app X ≫ (StructuredArrow.Hom.right f₁).app Y =
    (E.coconeAt Y).ι.app X ≫ (StructuredArrow.Hom.right f₂).app Y
have h₁ : ((StructuredArrow.hom E).app X.left ≫ (StructuredArrow.right E).map X.hom) ≫ (StructuredArrow.Hom.right f₁).app Y =
  ((StructuredArrow.hom E).app X.left ≫ (StructuredArrow.right E).map X.hom) ≫ (StructuredArrow.Hom.right f₂).app Y
Tactic: dsimp at eq₁ eq₂ ⊢
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Pointwise (goal)
Goal:
C : Type u_1
D : Type u_2
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_1, v_4, u_1, u_4} C H
E : L.LeftExtension F
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
f₁ f₂ : E ⟶ G
Y : D
X : CostructuredArrow L Y
eq₁ :
  Eq (α := F.obj X.left ⟶ (StructuredArrow.right G).obj (L.obj X.left))
    ((StructuredArrow.hom E).app X.left ≫ (StructuredArrow.Hom.right f₁).app (L.obj X.left))
    ((StructuredArrow.hom G).app X.left)
eq₂ :
  Eq (α := F.obj X.left ⟶ (StructuredArrow.right G).obj (L.obj X.left))
    ((StructuredArrow.hom E).app X.left ≫ (StructuredArrow.Hom.right f₂).app (L.obj X.left))
    ((StructuredArrow.hom G).app X.left)
⊢ ((StructuredArrow.hom E).app X.left ≫ (StructuredArrow.right E).map X.hom) ≫ (StructuredArrow.Hom.right f₁).app Y =
    ((StructuredArrow.hom E).app X.left ≫ (StructuredArrow.right E).map X.hom) ≫ (StructuredArrow.Hom.right f₂).app Y
have h₁ : (StructuredArrow.hom E).app X.left ≫
    (StructuredArrow.Hom.right f₁).app (L.obj X.left) ≫ (StructuredArrow.right G).map X.hom =
  (StructuredArrow.hom E).app X.left ≫
    (StructuredArrow.Hom.right f₂).app (L.obj X.left) ≫ (StructuredArrow.right G).map X.hom
Tactic: simp only [assoc, NatTrans.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Pointwise (goal)
Goal:
C : Type u_1
D : Type u_2
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_1, v_4, u_1, u_4} C H
E : L.LeftExtension F
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
f₁ f₂ : E ⟶ G
Y : D
X : CostructuredArrow L Y
eq₁ :
  Eq (α := F.obj X.left ⟶ (StructuredArrow.right G).obj (L.obj X.left))
    ((StructuredArrow.hom E).app X.left ≫ (StructuredArrow.Hom.right f₁).app (L.obj X.left))
    ((StructuredArrow.hom G).app X.left)
eq₂ :
  Eq (α := F.obj X.left ⟶ (StructuredArrow.right G).obj (L.obj X.left))
    ((StructuredArrow.hom E).app X.left ≫ (StructuredArrow.Hom.right f₂).app (L.obj X.left))
    ((StructuredArrow.hom G).app X.left)
⊢ (StructuredArrow.hom E).app X.left ≫
      (StructuredArrow.Hom.right f₁).app (L.obj X.left) ≫ (StructuredArrow.right G).map X.hom =
    (StructuredArrow.hom E).app X.left ≫
      (StructuredArrow.Hom.right f₂).app (L.obj X.left) ≫ (StructuredArrow.right G).map X.hom
have h₁ : (StructuredArrow.hom G).app X.left ≫ (StructuredArrow.right G).map X.hom =
  (StructuredArrow.hom E).app X.left ≫
    (StructuredArrow.Hom.right f₂).app (L.obj X.left) ≫ (StructuredArrow.right G).map X.hom
Tactic: rw [reassoc_of% eq₁, reassoc_of% eq₂]