awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
d : D
Z : (X : C) → (d ⟶ F.obj X) → Sort u_1
h₁ : (X₁ X₂ : C) → (k₁ : d ⟶ F.obj X₁) → (k₂ : d ⟶ F.obj X₂) → (f : X₁ ⟶ X₂) → k₁ ≫ F.map f = k₂ → Z X₁ k₁ → Z X₂ k₂
h₂ : (X₁ X₂ : C) → (k₁ : d ⟶ F.obj X₁) → (k₂ : d ⟶ F.obj X₂) → (f : X₁ ⟶ X₂) → k₁ ≫ F.map f = k₂ → Z X₂ k₂ → Z X₁ k₁
X₀ : C
k₀ : d ⟶ F.obj X₀
z : Z X₀ k₀
⊢ Nonempty.{u_1} (Z (lift F d) (homToLift F d))
have h : {j₁ j₂ : StructuredArrow d F} →
  (j₁ ⟶ j₂) →
    (fun (Y : StructuredArrow d F) ↦ Z Y.right Y.hom) j₁ → (fun (Y : StructuredArrow d F) ↦ Z Y.right Y.hom) j₂
Tactic: refine isPreconnected_induction (Z := fun Y : StructuredArrow d F => Z Y.right Y.hom)
    ?_ ?_ (j₀ := StructuredArrow.mk k₀) z _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
d : D
Z : (X : C) → (d ⟶ F.obj X) → Sort u_1
h₁ : (X₁ X₂ : C) → (k₁ : d ⟶ F.obj X₁) → (k₂ : d ⟶ F.obj X₂) → (f : X₁ ⟶ X₂) → k₁ ≫ F.map f = k₂ → Z X₁ k₁ → Z X₂ k₂
h₂ : (X₁ X₂ : C) → (k₁ : d ⟶ F.obj X₁) → (k₂ : d ⟶ F.obj X₂) → (f : X₁ ⟶ X₂) → k₁ ≫ F.map f = k₂ → Z X₂ k₂ → Z X₁ k₁
X₀ : C
k₀ : d ⟶ F.obj X₀
z : Z X₀ k₀
h :
  {j₁ j₂ : StructuredArrow d F} →
    (j₁ ⟶ j₂) →
      (fun (Y : StructuredArrow d F) ↦ Z Y.right Y.hom) j₁ → (fun (Y : StructuredArrow d F) ↦ Z Y.right Y.hom) j₂
⊢ Nonempty.{u_1} (Z (lift F d) (homToLift F d))
have h₃ : {j₁ j₂ : StructuredArrow d F} →
  (j₁ ⟶ j₂) →
    (fun (Y : StructuredArrow d F) ↦ Z Y.right Y.hom) j₂ → (fun (Y : StructuredArrow d F) ↦ Z Y.right Y.hom) j₁
Tactic: refine isPreconnected_induction (Z := fun Y : StructuredArrow d F => Z Y.right Y.hom)
    ?_ ?_ (j₀ := StructuredArrow.mk k₀) z _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
c : Cocone (F ⋙ G)
X Y : D
f : X ⟶ Y
⊢ Eq (α := G.obj X ⟶ obj.{v₂, v₃, u₂, u₃} (obj (const D) c.pt) Y)
    (G.map f ≫ CategoryStruct.comp (Y := G.obj (F.obj (lift F Y))) (G.map (homToLift F Y)) (c.ι.app (lift F Y)) :
      G.obj X ⟶ obj.{v₂, v₃, u₂, u₃} (obj (const D) c.pt) Y)
    (CategoryStruct.comp (Y := obj.{v₂, v₃, u₂, u₃} (obj (const D) c.pt) X)
        (CategoryStruct.comp (Y := G.obj (F.obj (lift F X))) (G.map (homToLift F X)) (c.ι.app (lift F X)) :
          G.obj X ⟶ obj.{v₂, v₃, u₂, u₃} (obj (const D) c.pt) X)
        (map (obj (const D) c.pt) f :
          obj.{v₂, v₃, u₂, u₃} (obj (const D) c.pt) X ⟶ obj.{v₂, v₃, u₂, u₃} (obj (const D) c.pt) Y) :
      G.obj X ⟶ obj.{v₂, v₃, u₂, u₃} (obj (const D) c.pt) Y)
have dsimp : G.map f ≫ CategoryStruct.comp (Y := G.obj (F.obj (lift F Y))) (G.map (homToLift F Y)) (c.ι.app (lift F Y)) =
  CategoryStruct.comp (Y := c.pt)
    (CategoryStruct.comp (Y := G.obj (F.obj (lift F X))) (G.map (homToLift F X)) (c.ι.app (lift F X)) : G.obj X ⟶ c.pt)
    (𝟙 c.pt : c.pt ⟶ c.pt)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
c : Cocone (F ⋙ G)
X Y : D
f : X ⟶ Y
⊢ G.map f ≫ CategoryStruct.comp (Y := G.obj (F.obj (lift F Y))) (G.map (homToLift F Y)) (c.ι.app (lift F Y)) =
    CategoryStruct.comp (Y := c.pt)
      (CategoryStruct.comp (Y := G.obj (F.obj (lift F X))) (G.map (homToLift F X)) (c.ι.app (lift F X)) :
        G.obj X ⟶ c.pt)
      (𝟙 c.pt : c.pt ⟶ c.pt)
have simp : Eq (α := G.obj X ⟶ c.pt)
  (G.map f ≫ CategoryStruct.comp (Y := G.obj (F.obj (lift F Y))) (G.map (homToLift F Y)) (c.ι.app (lift F Y)) :
    G.obj X ⟶ c.pt)
  (CategoryStruct.comp (Y := G.obj (F.obj (lift F X))) (G.map (homToLift F X)) (c.ι.app (lift F X)) : G.obj X ⟶ c.pt)
Tactic: simp only [Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
c : Cocone (F ⋙ G)
X Y : D
f : X ⟶ Y
⊢ Eq (α := G.obj X ⟶ c.pt)
    (G.map f ≫ CategoryStruct.comp (Y := G.obj (F.obj (lift F Y))) (G.map (homToLift F Y)) (c.ι.app (lift F Y)) :
      G.obj X ⟶ c.pt)
    (CategoryStruct.comp (Y := G.obj (F.obj (lift F X))) (G.map (homToLift F X)) (c.ι.app (lift F X)) : G.obj X ⟶ c.pt)
have h₁ : ∀ (X₁ X₂ : C) (k₁ : X ⟶ F.obj X₁) (k₂ : X ⟶ F.obj X₂) (f_1 : X₁ ⟶ X₂),
  k₁ ≫ F.map f_1 = k₂ →
    G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₁ ≫ c.ι.app X₁ →
      G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₂ ≫ c.ι.app X₂
Tactic: apply
              induction F fun Z k =>
                G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k ≫ c.ι.app Z
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
c : Cocone (F ⋙ G)
X Y : D
f : X ⟶ Y
h₁ :
  ∀ (X₁ X₂ : C) (k₁ : X ⟶ F.obj X₁) (k₂ : X ⟶ F.obj X₂) (f_1 : X₁ ⟶ X₂),
    k₁ ≫ F.map f_1 = k₂ →
      G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₁ ≫ c.ι.app X₁ →
        G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₂ ≫ c.ι.app X₂
⊢ Eq (α := G.obj X ⟶ c.pt)
    (G.map f ≫ CategoryStruct.comp (Y := G.obj (F.obj (lift F Y))) (G.map (homToLift F Y)) (c.ι.app (lift F Y)) :
      G.obj X ⟶ c.pt)
    (CategoryStruct.comp (Y := G.obj (F.obj (lift F X))) (G.map (homToLift F X)) (c.ι.app (lift F X)) : G.obj X ⟶ c.pt)
have h₂ : ∀ (X₁ X₂ : C) (k₁ : X ⟶ F.obj X₁) (k₂ : X ⟶ F.obj X₂) (f_1 : X₁ ⟶ X₂),
  k₁ ≫ F.map f_1 = k₂ →
    G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₂ ≫ c.ι.app X₂ →
      G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₁ ≫ c.ι.app X₁
Tactic: apply
              induction F fun Z k =>
                G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k ≫ c.ι.app Z
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
c : Cocone (F ⋙ G)
X Y : D
f : X ⟶ Y
h₁ :
  ∀ (X₁ X₂ : C) (k₁ : X ⟶ F.obj X₁) (k₂ : X ⟶ F.obj X₂) (f_1 : X₁ ⟶ X₂),
    k₁ ≫ F.map f_1 = k₂ →
      G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₁ ≫ c.ι.app X₁ →
        G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₂ ≫ c.ι.app X₂
h₂ :
  ∀ (X₁ X₂ : C) (k₁ : X ⟶ F.obj X₁) (k₂ : X ⟶ F.obj X₂) (f_1 : X₁ ⟶ X₂),
    k₁ ≫ F.map f_1 = k₂ →
      G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₂ ≫ c.ι.app X₂ →
        G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₁ ≫ c.ι.app X₁
⊢ Eq (α := G.obj X ⟶ c.pt)
    (G.map f ≫ CategoryStruct.comp (Y := G.obj (F.obj (lift F Y))) (G.map (homToLift F Y)) (c.ι.app (lift F Y)) :
      G.obj X ⟶ c.pt)
    (CategoryStruct.comp (Y := G.obj (F.obj (lift F X))) (G.map (homToLift F X)) (c.ι.app (lift F X)) : G.obj X ⟶ c.pt)
have z : Eq (α := G.obj X ⟶ obj.{v₁, v₃, u₁, u₃} (obj (const C) c.pt) (lift F Y))
  (G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y)) (G.map (f ≫ homToLift F Y) ≫ c.ι.app (lift F Y))
Tactic: apply
              induction F fun Z k =>
                G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k ≫ c.ι.app Z
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
c : Cocone (F ⋙ G)
X Y : D
f : X ⟶ Y
h₁ :
  ∀ (X₁ X₂ : C) (k₁ : X ⟶ F.obj X₁) (k₂ : X ⟶ F.obj X₂) (f_1 : X₁ ⟶ X₂),
    k₁ ≫ F.map f_1 = k₂ →
      G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₁ ≫ c.ι.app X₁ →
        G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₂ ≫ c.ι.app X₂
h₂ :
  ∀ (X₁ X₂ : C) (k₁ : X ⟶ F.obj X₁) (k₂ : X ⟶ F.obj X₂) (f_1 : X₁ ⟶ X₂),
    k₁ ≫ F.map f_1 = k₂ →
      G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₂ ≫ c.ι.app X₂ →
        G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₁ ≫ c.ι.app X₁
z :
  Eq (α := G.obj X ⟶ obj.{v₁, v₃, u₁, u₃} (obj (const C) c.pt) (lift F Y))
    (G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y)) (G.map (f ≫ homToLift F Y) ≫ c.ι.app (lift F Y))
⊢ Eq (α := G.obj X ⟶ c.pt)
    (G.map f ≫ CategoryStruct.comp (Y := G.obj (F.obj (lift F Y))) (G.map (homToLift F Y)) (c.ι.app (lift F Y)) :
      G.obj X ⟶ c.pt)
    (CategoryStruct.comp (Y := G.obj (F.obj (lift F X))) (G.map (homToLift F X)) (c.ι.app (lift F X)) : G.obj X ⟶ c.pt)
have X₀ : C
Tactic: apply
              induction F fun Z k =>
                G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k ≫ c.ι.app Z
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
c : Cocone (F ⋙ G)
X Y : D
f : X ⟶ Y
h₁ :
  ∀ (X₁ X₂ : C) (k₁ : X ⟶ F.obj X₁) (k₂ : X ⟶ F.obj X₂) (f_1 : X₁ ⟶ X₂),
    k₁ ≫ F.map f_1 = k₂ →
      G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₁ ≫ c.ι.app X₁ →
        G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₂ ≫ c.ι.app X₂
h₂ :
  ∀ (X₁ X₂ : C) (k₁ : X ⟶ F.obj X₁) (k₂ : X ⟶ F.obj X₂) (f_1 : X₁ ⟶ X₂),
    k₁ ≫ F.map f_1 = k₂ →
      G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₂ ≫ c.ι.app X₂ →
        G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₁ ≫ c.ι.app X₁
z :
  Eq (α := G.obj X ⟶ obj.{v₁, v₃, u₁, u₃} (obj (const C) c.pt) (lift F Y))
    (G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y)) (G.map (f ≫ homToLift F Y) ≫ c.ι.app (lift F Y))
X₀ : C
⊢ Eq (α := G.obj X ⟶ c.pt)
    (G.map f ≫ CategoryStruct.comp (Y := G.obj (F.obj (lift F Y))) (G.map (homToLift F Y)) (c.ι.app (lift F Y)) :
      G.obj X ⟶ c.pt)
    (CategoryStruct.comp (Y := G.obj (F.obj (lift F X))) (G.map (homToLift F X)) (c.ι.app (lift F X)) : G.obj X ⟶ c.pt)
have k₀ : X ⟶ F.obj (lift F Y)
Tactic: apply
              induction F fun Z k =>
                G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k ≫ c.ι.app Z
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
c : Cocone (F ⋙ G)
X Y : D
f : X ⟶ Y
Z₁ Z₂ : C
k₁ : X ⟶ F.obj Z₁
k₂ : X ⟶ F.obj Z₂
g : Z₁ ⟶ Z₂
a : k₁ ≫ F.map g = k₂
z : G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₁ ≫ c.ι.app Z₁
⊢ G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₂ ≫ c.ι.app Z₂
have h₁ : G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map (k₁ ≫ F.map g) ≫ c.ι.app Z₂
Tactic: rw [← a, Functor.map_comp, Category.assoc, ← Functor.comp_map, c.w, z]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
c : Cocone (F ⋙ G)
X Y : D
f : X ⟶ Y
Z₁ Z₂ : C
k₁ : X ⟶ F.obj Z₁
k₂ : X ⟶ F.obj Z₂
g : Z₁ ⟶ Z₂
a : k₁ ≫ F.map g = k₂
z : G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₁ ≫ c.ι.app Z₁
h₁ : G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map (k₁ ≫ F.map g) ≫ c.ι.app Z₂
⊢ G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₂ ≫ c.ι.app Z₂
have h₂ : G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = (G.map k₁ ≫ G.map (F.map g)) ≫ c.ι.app Z₂
Tactic: rw [← a, Functor.map_comp, Category.assoc, ← Functor.comp_map, c.w, z]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
c : Cocone (F ⋙ G)
X Y : D
f : X ⟶ Y
Z₁ Z₂ : C
k₁ : X ⟶ F.obj Z₁
k₂ : X ⟶ F.obj Z₂
g : Z₁ ⟶ Z₂
a : k₁ ≫ F.map g = k₂
z : G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₁ ≫ c.ι.app Z₁
h₁ : G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map (k₁ ≫ F.map g) ≫ c.ι.app Z₂
h₂ : G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = (G.map k₁ ≫ G.map (F.map g)) ≫ c.ι.app Z₂
⊢ G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₂ ≫ c.ι.app Z₂
have h₃ : G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₁ ≫ G.map (F.map g) ≫ c.ι.app Z₂
Tactic: rw [← a, Functor.map_comp, Category.assoc, ← Functor.comp_map, c.w, z]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
c : Cocone (F ⋙ G)
X Y : D
f : X ⟶ Y
Z₁ Z₂ : C
k₁ : X ⟶ F.obj Z₁
k₂ : X ⟶ F.obj Z₂
g : Z₁ ⟶ Z₂
a : k₁ ≫ F.map g = k₂
z : G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₁ ≫ c.ι.app Z₁
h₁ : G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map (k₁ ≫ F.map g) ≫ c.ι.app Z₂
h₂ : G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = (G.map k₁ ≫ G.map (F.map g)) ≫ c.ι.app Z₂
h₃ : G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₁ ≫ G.map (F.map g) ≫ c.ι.app Z₂
⊢ G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₂ ≫ c.ι.app Z₂
have h₄ : G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₁ ≫ (F ⋙ G).map g ≫ c.ι.app Z₂
Tactic: rw [← a, Functor.map_comp, Category.assoc, ← Functor.comp_map, c.w, z]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
c : Cocone (F ⋙ G)
X Y : D
f : X ⟶ Y
Z₁ Z₂ : C
k₁ : X ⟶ F.obj Z₁
k₂ : X ⟶ F.obj Z₂
g : Z₁ ⟶ Z₂
a : k₁ ≫ F.map g = k₂
z : G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₁ ≫ c.ι.app Z₁
h₁ : G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map (k₁ ≫ F.map g) ≫ c.ι.app Z₂
h₂ : G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = (G.map k₁ ≫ G.map (F.map g)) ≫ c.ι.app Z₂
h₃ : G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₁ ≫ G.map (F.map g) ≫ c.ι.app Z₂
h₄ : G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₁ ≫ (F ⋙ G).map g ≫ c.ι.app Z₂
h₅ : G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₁ ≫ c.ι.app Z₁
⊢ G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₂ ≫ c.ι.app Z₂
have h₆ : G.map k₁ ≫ c.ι.app Z₁ = G.map k₁ ≫ c.ι.app Z₁
Tactic: rw [← a, Functor.map_comp, Category.assoc, ← Functor.comp_map, c.w, z]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
c : Cocone (F ⋙ G)
X Y : D
f : X ⟶ Y
Z₁ Z₂ : C
k₁ : X ⟶ F.obj Z₁
k₂ : X ⟶ F.obj Z₂
g : Z₁ ⟶ Z₂
a : k₁ ≫ F.map g = k₂
z : G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₁ ≫ c.ι.app Z₁
⊢ G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₁ ≫ c.ι.app Z₁
have h₂ : G.map k₁ ≫ c.ι.app Z₁ = G.map k₁ ≫ c.ι.app Z₁
Tactic: rw [z]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
c : Cocone (F ⋙ G)
X Y : D
f : X ⟶ Y
⊢ Eq (α := G.obj X ⟶ obj.{v₁, v₃, u₁, u₃} (obj (const C) c.pt) (lift F Y))
    (G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y)) (G.map (f ≫ homToLift F Y) ≫ c.ι.app (lift F Y))
have z : Eq (α := G.obj X ⟶ obj.{v₁, v₃, u₁, u₃} (obj (const C) c.pt) (lift F Y))
  (G.map (f ≫ homToLift F Y) ≫ c.ι.app (lift F Y)) (G.map (f ≫ homToLift F Y) ≫ c.ι.app (lift F Y))
Tactic: rw [← Functor.map_comp_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
c : Cocone (F ⋙ G)
X : D
Y : C
f : X ⟶ F.obj Y
⊢ (obj extendCocone c).ι.app X = G.map f ≫ c.ι.app Y
have h₁ : ∀ (X₁ X₂ : C) (k₁ : X ⟶ F.obj X₁) (k₂ : X ⟶ F.obj X₂) (f_1 : X₁ ⟶ X₂),
  k₁ ≫ F.map f_1 = k₂ →
    (fun (Z : C) (g : X ⟶ F.obj Z) ↦ G.map g ≫ c.ι.app Z = G.map f ≫ c.ι.app Y) X₁ k₁ →
      (fun (Z : C) (g : X ⟶ F.obj Z) ↦ G.map g ≫ c.ι.app Z = G.map f ≫ c.ι.app Y) X₂ k₂
Tactic: apply induction (k₀ := f) (z := rfl) F fun Z g =>
    G.map g ≫ c.ι.app Z = G.map f ≫ c.ι.app Y
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
c : Cocone (F ⋙ G)
X : D
Y : C
f : X ⟶ F.obj Y
h₁ :
  ∀ (X₁ X₂ : C) (k₁ : X ⟶ F.obj X₁) (k₂ : X ⟶ F.obj X₂) (f_1 : X₁ ⟶ X₂),
    k₁ ≫ F.map f_1 = k₂ →
      (fun (Z : C) (g : X ⟶ F.obj Z) ↦ G.map g ≫ c.ι.app Z = G.map f ≫ c.ι.app Y) X₁ k₁ →
        (fun (Z : C) (g : X ⟶ F.obj Z) ↦ G.map g ≫ c.ι.app Z = G.map f ≫ c.ι.app Y) X₂ k₂
⊢ (obj extendCocone c).ι.app X = G.map f ≫ c.ι.app Y
have h₂ : ∀ (X₁ X₂ : C) (k₁ : X ⟶ F.obj X₁) (k₂ : X ⟶ F.obj X₂) (f_1 : X₁ ⟶ X₂),
  k₁ ≫ F.map f_1 = k₂ →
    (fun (Z : C) (g : X ⟶ F.obj Z) ↦ G.map g ≫ c.ι.app Z = G.map f ≫ c.ι.app Y) X₂ k₂ →
      (fun (Z : C) (g : X ⟶ F.obj Z) ↦ G.map g ≫ c.ι.app Z = G.map f ≫ c.ι.app Y) X₁ k₁
Tactic: apply induction (k₀ := f) (z := rfl) F fun Z g =>
    G.map g ≫ c.ι.app Z = G.map f ≫ c.ι.app Y
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
s : Cocone (F ⋙ G)
j : C
⊢ G.map (homToLift F (F.obj j)) ≫ s.ι.app (lift F (F.obj j)) = s.ι.app j
have h₁ : ∀ (X₁ X₂ : C) (k₁ : F.obj j ⟶ F.obj X₁) (k₂ : F.obj j ⟶ F.obj X₂) (f : X₁ ⟶ X₂),
  k₁ ≫ F.map f = k₂ → G.map k₁ ≫ s.ι.app X₁ = s.ι.app j → G.map k₂ ≫ s.ι.app X₂ = s.ι.app j
Tactic: apply induction F fun X k => G.map k ≫ s.ι.app X = (s.ι.app j :)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
s : Cocone (F ⋙ G)
j : C
h₁ :
  ∀ (X₁ X₂ : C) (k₁ : F.obj j ⟶ F.obj X₁) (k₂ : F.obj j ⟶ F.obj X₂) (f : X₁ ⟶ X₂),
    k₁ ≫ F.map f = k₂ → G.map k₁ ≫ s.ι.app X₁ = s.ι.app j → G.map k₂ ≫ s.ι.app X₂ = s.ι.app j
⊢ G.map (homToLift F (F.obj j)) ≫ s.ι.app (lift F (F.obj j)) = s.ι.app j
have h₂ : ∀ (X₁ X₂ : C) (k₁ : F.obj j ⟶ F.obj X₁) (k₂ : F.obj j ⟶ F.obj X₂) (f : X₁ ⟶ X₂),
  k₁ ≫ F.map f = k₂ → G.map k₂ ≫ s.ι.app X₂ = s.ι.app j → G.map k₁ ≫ s.ι.app X₁ = s.ι.app j
Tactic: apply induction F fun X k => G.map k ≫ s.ι.app X = (s.ι.app j :)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
s : Cocone (F ⋙ G)
j : C
h₁ :
  ∀ (X₁ X₂ : C) (k₁ : F.obj j ⟶ F.obj X₁) (k₂ : F.obj j ⟶ F.obj X₂) (f : X₁ ⟶ X₂),
    k₁ ≫ F.map f = k₂ → G.map k₁ ≫ s.ι.app X₁ = s.ι.app j → G.map k₂ ≫ s.ι.app X₂ = s.ι.app j
h₂ :
  ∀ (X₁ X₂ : C) (k₁ : F.obj j ⟶ F.obj X₁) (k₂ : F.obj j ⟶ F.obj X₂) (f : X₁ ⟶ X₂),
    k₁ ≫ F.map f = k₂ → G.map k₂ ≫ s.ι.app X₂ = s.ι.app j → G.map k₁ ≫ s.ι.app X₁ = s.ι.app j
⊢ G.map (homToLift F (F.obj j)) ≫ s.ι.app (lift F (F.obj j)) = s.ι.app j
have z : G.map (F.map (𝟙 j)) ≫ s.ι.app j = s.ι.app j
Tactic: apply induction F fun X k => G.map k ≫ s.ι.app X = (s.ι.app j :)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
s : Cocone (F ⋙ G)
j : C
h₁ :
  ∀ (X₁ X₂ : C) (k₁ : F.obj j ⟶ F.obj X₁) (k₂ : F.obj j ⟶ F.obj X₂) (f : X₁ ⟶ X₂),
    k₁ ≫ F.map f = k₂ → G.map k₁ ≫ s.ι.app X₁ = s.ι.app j → G.map k₂ ≫ s.ι.app X₂ = s.ι.app j
h₂ :
  ∀ (X₁ X₂ : C) (k₁ : F.obj j ⟶ F.obj X₁) (k₂ : F.obj j ⟶ F.obj X₂) (f : X₁ ⟶ X₂),
    k₁ ≫ F.map f = k₂ → G.map k₂ ≫ s.ι.app X₂ = s.ι.app j → G.map k₁ ≫ s.ι.app X₁ = s.ι.app j
z : G.map (F.map (𝟙 j)) ≫ s.ι.app j = s.ι.app j
X₀ : C
⊢ G.map (homToLift F (F.obj j)) ≫ s.ι.app (lift F (F.obj j)) = s.ι.app j
have k₀ : F.obj j ⟶ F.obj j
Tactic: apply induction F fun X k => G.map k ≫ s.ι.app X = (s.ι.app j :)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
s : Cocone (F ⋙ G)
j j₁ j₂ : C
k₁ : F.obj j ⟶ F.obj j₁
k₂ : F.obj j ⟶ F.obj j₂
f : j₁ ⟶ j₂
w : k₁ ≫ F.map f = k₂
h : G.map k₁ ≫ s.ι.app j₁ = s.ι.app j
⊢ G.map k₂ ≫ s.ι.app j₂ = s.ι.app j
have h₁ : G.map (k₁ ≫ F.map f) ≫ s.ι.app j₂ = s.ι.app j
Tactic: rw [← w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
s : Cocone (F ⋙ G)
j j₁ j₂ : C
k₁ : F.obj j ⟶ F.obj j₁
k₂ : F.obj j ⟶ F.obj j₂
f : j₁ ⟶ j₂
w : k₁ ≫ F.map f = k₂
h : G.map k₁ ≫ s.ι.app j₁ = s.ι.app j
⊢ G.map (k₁ ≫ F.map f) ≫ s.ι.app j₂ = s.ι.app j
have h₁ : G.map k₁ ≫ (F ⋙ G).map f ≫ s.ι.app j₂ = s.ι.app j
Tactic: rw [← s.w f] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
s : Cocone (F ⋙ G)
j j₁ j₂ : C
k₁ : F.obj j ⟶ F.obj j₁
k₂ : F.obj j ⟶ F.obj j₂
f : j₁ ⟶ j₂
w : k₁ ≫ F.map f = k₂
h : G.map k₂ ≫ s.ι.app j₂ = s.ι.app j
⊢ G.map k₁ ≫ s.ι.app j₁ = s.ι.app j
have h₁ : G.map (k₁ ≫ F.map f) ≫ s.ι.app j₂ = s.ι.app j
Tactic: rw [← w] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
s : Cocone (F ⋙ G)
j j₁ j₂ : C
k₁ : F.obj j ⟶ F.obj j₁
k₂ : F.obj j ⟶ F.obj j₂
f : j₁ ⟶ j₂
w : k₁ ≫ F.map f = k₂
h : G.map (k₁ ≫ F.map f) ≫ s.ι.app j₂ = s.ι.app j
⊢ G.map k₁ ≫ s.ι.app j₁ = s.ι.app j
have h₂ : G.map k₁ ≫ (F ⋙ G).map f ≫ s.ι.app j₂ = s.ι.app j
Tactic: rw [← s.w f]