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.Initial
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
c : Cone (F ⋙ G)
X Y : D
f : X ⟶ Y
Z₁ Z₂ : C
k₁ : F.obj Z₁ ⟶ Y
k₂ : F.obj Z₂ ⟶ Y
g : Z₁ ⟶ Z₂
a : F.map g ≫ k₂ = k₁
z : c.π.app Z₂ ≫ G.map k₂ = (c.π.app (lift F X) ≫ G.map (homToLift F X)) ≫ G.map f
h₁ :
  Eq (α := c.pt ⟶ G.obj Y)
    ((c.π.app (lift F X) ≫ G.map (homToLift F X)) ≫ G.map f :
      obj.{v₁, v₃, u₁, u₃} (obj (const C) c.pt) (lift F X) ⟶ G.obj Y)
    (c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f)
⊢ c.π.app Z₂ ≫ G.map k₂ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
have h₂ : Eq (α := c.pt ⟶ G.obj Y)
  (c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f :
    obj.{v₁, v₃, u₁, u₃} (obj (const C) c.pt) (lift F X) ⟶ G.obj Y)
  (c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f)
Tactic: rw [z, Category.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.Initial
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
c : Cone (F ⋙ G)
X Y : D
f : X ⟶ Y
Z₁ Z₂ : C
k₁ : F.obj Z₁ ⟶ Y
k₂ : F.obj Z₂ ⟶ Y
g : Z₁ ⟶ Z₂
a : F.map g ≫ k₂ = k₁
z : c.π.app Z₂ ≫ G.map k₂ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
⊢ c.π.app Z₁ ≫ G.map k₁ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
have h₂ : c.π.app Z₁ ≫ G.map (F.map g ≫ k₂) = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
Tactic: rw [← a, Functor.map_comp, ← Functor.comp_map, ← Category.assoc, ← Category.assoc,
                c.w, z, Category.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.Initial
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
c : Cone (F ⋙ G)
X Y : D
f : X ⟶ Y
Z₁ Z₂ : C
k₁ : F.obj Z₁ ⟶ Y
k₂ : F.obj Z₂ ⟶ Y
g : Z₁ ⟶ Z₂
a : F.map g ≫ k₂ = k₁
z : c.π.app Z₂ ≫ G.map k₂ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
h₂ : c.π.app Z₁ ≫ G.map (F.map g ≫ k₂) = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
⊢ c.π.app Z₁ ≫ G.map k₁ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
have h₃ : c.π.app Z₁ ≫ G.map (F.map g) ≫ G.map k₂ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
Tactic: rw [← a, Functor.map_comp, ← Functor.comp_map, ← Category.assoc, ← Category.assoc,
                c.w, z, Category.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.Initial
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
c : Cone (F ⋙ G)
X Y : D
f : X ⟶ Y
Z₁ Z₂ : C
k₁ : F.obj Z₁ ⟶ Y
k₂ : F.obj Z₂ ⟶ Y
g : Z₁ ⟶ Z₂
a : F.map g ≫ k₂ = k₁
z : c.π.app Z₂ ≫ G.map k₂ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
h₂ : c.π.app Z₁ ≫ G.map (F.map g ≫ k₂) = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
h₃ : c.π.app Z₁ ≫ G.map (F.map g) ≫ G.map k₂ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
⊢ c.π.app Z₁ ≫ G.map k₁ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
have h₄ : c.π.app Z₁ ≫ (F ⋙ G).map g ≫ G.map k₂ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
Tactic: rw [← a, Functor.map_comp, ← Functor.comp_map, ← Category.assoc, ← Category.assoc,
                c.w, z, Category.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.Initial
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
c : Cone (F ⋙ G)
X Y : D
f : X ⟶ Y
Z₁ Z₂ : C
k₁ : F.obj Z₁ ⟶ Y
k₂ : F.obj Z₂ ⟶ Y
g : Z₁ ⟶ Z₂
a : F.map g ≫ k₂ = k₁
z : c.π.app Z₂ ≫ G.map k₂ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
h₂ : c.π.app Z₁ ≫ G.map (F.map g ≫ k₂) = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
h₃ : c.π.app Z₁ ≫ G.map (F.map g) ≫ G.map k₂ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
h₄ : c.π.app Z₁ ≫ (F ⋙ G).map g ≫ G.map k₂ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
⊢ c.π.app Z₁ ≫ G.map k₁ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
have h₅ : (c.π.app Z₁ ≫ (F ⋙ G).map g) ≫ G.map k₂ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
Tactic: rw [← a, Functor.map_comp, ← Functor.comp_map, ← Category.assoc, ← Category.assoc,
                c.w, z, Category.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.Initial
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
c : Cone (F ⋙ G)
X Y : D
f : X ⟶ Y
Z₁ Z₂ : C
k₁ : F.obj Z₁ ⟶ Y
k₂ : F.obj Z₂ ⟶ Y
g : Z₁ ⟶ Z₂
a : F.map g ≫ k₂ = k₁
z : c.π.app Z₂ ≫ G.map k₂ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
h₂ : c.π.app Z₁ ≫ G.map (F.map g ≫ k₂) = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
h₃ : c.π.app Z₁ ≫ G.map (F.map g) ≫ G.map k₂ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
h₄ : c.π.app Z₁ ≫ (F ⋙ G).map g ≫ G.map k₂ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
h₅ : (c.π.app Z₁ ≫ (F ⋙ G).map g) ≫ G.map k₂ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
⊢ c.π.app Z₁ ≫ G.map k₁ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
have h₆ : (c.π.app Z₁ ≫ (F ⋙ G).map g) ≫ G.map k₂ = (c.π.app (lift F X) ≫ G.map (homToLift F X)) ≫ G.map f
Tactic: rw [← a, Functor.map_comp, ← Functor.comp_map, ← Category.assoc, ← Category.assoc,
                c.w, z, Category.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.Initial
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
c : Cone (F ⋙ G)
X Y : D
f : X ⟶ Y
Z₁ Z₂ : C
k₁ : F.obj Z₁ ⟶ Y
k₂ : F.obj Z₂ ⟶ Y
g : Z₁ ⟶ Z₂
a : F.map g ≫ k₂ = k₁
z : c.π.app Z₂ ≫ G.map k₂ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
h₂ : c.π.app Z₁ ≫ G.map (F.map g ≫ k₂) = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
h₃ : c.π.app Z₁ ≫ G.map (F.map g) ≫ G.map k₂ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
h₄ : c.π.app Z₁ ≫ (F ⋙ G).map g ≫ G.map k₂ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
h₅ : (c.π.app Z₁ ≫ (F ⋙ G).map g) ≫ G.map k₂ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
h₆ : (c.π.app Z₁ ≫ (F ⋙ G).map g) ≫ G.map k₂ = (c.π.app (lift F X) ≫ G.map (homToLift F X)) ≫ G.map f
⊢ c.π.app Z₁ ≫ G.map k₁ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
have h₇ : c.π.app Z₂ ≫ G.map k₂ = (c.π.app (lift F X) ≫ G.map (homToLift F X)) ≫ G.map f
Tactic: rw [← a, Functor.map_comp, ← Functor.comp_map, ← Category.assoc, ← Category.assoc,
                c.w, z, Category.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.Initial
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
c : Cone (F ⋙ G)
X Y : D
f : X ⟶ Y
Z₁ Z₂ : C
k₁ : F.obj Z₁ ⟶ Y
k₂ : F.obj Z₂ ⟶ Y
g : Z₁ ⟶ Z₂
a : F.map g ≫ k₂ = k₁
z : c.π.app Z₂ ≫ G.map k₂ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
h₂ : c.π.app Z₁ ≫ G.map (F.map g ≫ k₂) = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
h₃ : c.π.app Z₁ ≫ G.map (F.map g) ≫ G.map k₂ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
h₄ : c.π.app Z₁ ≫ (F ⋙ G).map g ≫ G.map k₂ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
h₅ : (c.π.app Z₁ ≫ (F ⋙ G).map g) ≫ G.map k₂ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
h₆ : (c.π.app Z₁ ≫ (F ⋙ G).map g) ≫ G.map k₂ = (c.π.app (lift F X) ≫ G.map (homToLift F X)) ≫ G.map f
h₇ : c.π.app Z₂ ≫ G.map k₂ = (c.π.app (lift F X) ≫ G.map (homToLift F X)) ≫ G.map f
⊢ c.π.app Z₁ ≫ G.map k₁ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
have h₈ : Eq (α := c.pt ⟶ G.obj Y)
  (c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f :
    obj.{v₁, v₃, u₁, u₃} (obj (const C) c.pt) (lift F X) ⟶ G.obj Y)
  ((c.π.app (lift F X) ≫ G.map (homToLift F X)) ≫ G.map f)
Tactic: rw [← a, Functor.map_comp, ← Functor.comp_map, ← Category.assoc, ← Category.assoc,
                c.w, z, Category.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.Initial
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
c : Cone (F ⋙ G)
X Y : D
f : X ⟶ Y
Z₁ Z₂ : C
k₁ : F.obj Z₁ ⟶ Y
k₂ : F.obj Z₂ ⟶ Y
g : Z₁ ⟶ Z₂
a : F.map g ≫ k₂ = k₁
z : c.π.app Z₂ ≫ G.map k₂ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
h₂ : c.π.app Z₁ ≫ G.map (F.map g ≫ k₂) = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
h₃ : c.π.app Z₁ ≫ G.map (F.map g) ≫ G.map k₂ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
h₄ : c.π.app Z₁ ≫ (F ⋙ G).map g ≫ G.map k₂ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
h₅ : (c.π.app Z₁ ≫ (F ⋙ G).map g) ≫ G.map k₂ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
h₆ : (c.π.app Z₁ ≫ (F ⋙ G).map g) ≫ G.map k₂ = (c.π.app (lift F X) ≫ G.map (homToLift F X)) ≫ G.map f
h₇ : c.π.app Z₂ ≫ G.map k₂ = (c.π.app (lift F X) ≫ G.map (homToLift F X)) ≫ G.map f
h₈ :
  Eq (α := c.pt ⟶ G.obj Y)
    (c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f :
      obj.{v₁, v₃, u₁, u₃} (obj (const C) c.pt) (lift F X) ⟶ G.obj Y)
    ((c.π.app (lift F X) ≫ G.map (homToLift F X)) ≫ G.map f)
⊢ c.π.app Z₁ ≫ G.map k₁ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
have h₉ : Eq (α := c.pt ⟶ G.obj Y)
  (c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f :
    obj.{v₁, v₃, u₁, u₃} (obj (const C) c.pt) (lift F X) ⟶ G.obj Y)
  (c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f)
Tactic: rw [← a, Functor.map_comp, ← Functor.comp_map, ← Category.assoc, ← Category.assoc,
                c.w, z, Category.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.Initial
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
c : Cone (F ⋙ G)
X Y : D
f : X ⟶ Y
⊢ Eq (α := c.pt ⟶ G.obj Y)
    (CategoryStruct.comp (Y := (F ⋙ G).obj (lift F X)) (c.π.app (lift F X)) (G.map (homToLift F X ≫ f)) :
      c.pt ⟶ G.obj Y)
    (c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f :
      obj.{v₁, v₃, u₁, u₃} (obj (const C) c.pt) (lift F X) ⟶ G.obj Y)
have z : Eq (α := c.pt ⟶ G.obj Y)
  (CategoryStruct.comp (Y := (F ⋙ G).obj (lift F X)) (c.π.app (lift F X)) (G.map (homToLift F X ≫ f)) : c.pt ⟶ G.obj Y)
  (c.π.app (lift F X) ≫ G.map (homToLift F X ≫ f) : obj.{v₁, v₃, u₁, u₃} (obj (const C) c.pt) (lift F X) ⟶ G.obj Y)
Tactic: rw [← Functor.map_comp]
-- 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.Initial
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
c : Cone (F ⋙ G)
X : C
Y : D
f : F.obj X ⟶ Y
⊢ (obj extendCone c).π.app Y = c.π.app X ≫ G.map f
have h₁ : ∀ (X₁ X₂ : C) (k₁ : F.obj X₁ ⟶ Y) (k₂ : F.obj X₂ ⟶ Y) (f_1 : X₁ ⟶ X₂),
  F.map f_1 ≫ k₂ = k₁ →
    (fun (Z : C) (g : F.obj Z ⟶ Y) ↦ c.π.app Z ≫ G.map g = c.π.app X ≫ G.map f) X₁ k₁ →
      (fun (Z : C) (g : F.obj Z ⟶ Y) ↦ c.π.app Z ≫ G.map g = c.π.app X ≫ G.map f) X₂ k₂
Tactic: apply induction (k₀ := f) (z := rfl) F fun Z g =>
    c.π.app Z ≫ G.map g = c.π.app X ≫ G.map f
-- 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.Initial
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
c : Cone (F ⋙ G)
X : C
Y : D
f : F.obj X ⟶ Y
h₁ :
  ∀ (X₁ X₂ : C) (k₁ : F.obj X₁ ⟶ Y) (k₂ : F.obj X₂ ⟶ Y) (f_1 : X₁ ⟶ X₂),
    F.map f_1 ≫ k₂ = k₁ →
      (fun (Z : C) (g : F.obj Z ⟶ Y) ↦ c.π.app Z ≫ G.map g = c.π.app X ≫ G.map f) X₁ k₁ →
        (fun (Z : C) (g : F.obj Z ⟶ Y) ↦ c.π.app Z ≫ G.map g = c.π.app X ≫ G.map f) X₂ k₂
⊢ (obj extendCone c).π.app Y = c.π.app X ≫ G.map f
have h₂ : ∀ (X₁ X₂ : C) (k₁ : F.obj X₁ ⟶ Y) (k₂ : F.obj X₂ ⟶ Y) (f_1 : X₁ ⟶ X₂),
  F.map f_1 ≫ k₂ = k₁ →
    (fun (Z : C) (g : F.obj Z ⟶ Y) ↦ c.π.app Z ≫ G.map g = c.π.app X ≫ G.map f) X₂ k₂ →
      (fun (Z : C) (g : F.obj Z ⟶ Y) ↦ c.π.app Z ≫ G.map g = c.π.app X ≫ G.map f) X₁ k₁
Tactic: apply induction (k₀ := f) (z := rfl) F fun Z g =>
    c.π.app Z ≫ G.map g = c.π.app X ≫ G.map f
-- 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.Initial
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
s : Cone (F ⋙ G)
j : C
⊢ s.π.app (lift F (F.obj j)) ≫ G.map (homToLift F (F.obj j)) = s.π.app j
have h₁ : ∀ (X₁ X₂ : C) (k₁ : F.obj X₁ ⟶ F.obj j) (k₂ : F.obj X₂ ⟶ F.obj j) (f : X₁ ⟶ X₂),
  F.map f ≫ k₂ = k₁ → s.π.app X₁ ≫ G.map k₁ = s.π.app j → s.π.app X₂ ≫ G.map k₂ = s.π.app j
Tactic: apply induction F fun X k => s.π.app X ≫ G.map k = (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.Initial
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
s : Cone (F ⋙ G)
j : C
h₁ :
  ∀ (X₁ X₂ : C) (k₁ : F.obj X₁ ⟶ F.obj j) (k₂ : F.obj X₂ ⟶ F.obj j) (f : X₁ ⟶ X₂),
    F.map f ≫ k₂ = k₁ → s.π.app X₁ ≫ G.map k₁ = s.π.app j → s.π.app X₂ ≫ G.map k₂ = s.π.app j
⊢ s.π.app (lift F (F.obj j)) ≫ G.map (homToLift F (F.obj j)) = s.π.app j
have h₂ : ∀ (X₁ X₂ : C) (k₁ : F.obj X₁ ⟶ F.obj j) (k₂ : F.obj X₂ ⟶ F.obj j) (f : X₁ ⟶ X₂),
  F.map f ≫ k₂ = k₁ → s.π.app X₂ ≫ G.map k₂ = s.π.app j → s.π.app X₁ ≫ G.map k₁ = s.π.app j
Tactic: apply induction F fun X k => s.π.app X ≫ G.map k = (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.Initial
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
s : Cone (F ⋙ G)
j : C
h₁ :
  ∀ (X₁ X₂ : C) (k₁ : F.obj X₁ ⟶ F.obj j) (k₂ : F.obj X₂ ⟶ F.obj j) (f : X₁ ⟶ X₂),
    F.map f ≫ k₂ = k₁ → s.π.app X₁ ≫ G.map k₁ = s.π.app j → s.π.app X₂ ≫ G.map k₂ = s.π.app j
h₂ :
  ∀ (X₁ X₂ : C) (k₁ : F.obj X₁ ⟶ F.obj j) (k₂ : F.obj X₂ ⟶ F.obj j) (f : X₁ ⟶ X₂),
    F.map f ≫ k₂ = k₁ → s.π.app X₂ ≫ G.map k₂ = s.π.app j → s.π.app X₁ ≫ G.map k₁ = s.π.app j
⊢ s.π.app (lift F (F.obj j)) ≫ G.map (homToLift F (F.obj j)) = s.π.app j
have z : s.π.app j ≫ G.map (F.map (𝟙 j)) = s.π.app j
Tactic: apply induction F fun X k => s.π.app X ≫ G.map k = (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.Initial
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
s : Cone (F ⋙ G)
j : C
h₁ :
  ∀ (X₁ X₂ : C) (k₁ : F.obj X₁ ⟶ F.obj j) (k₂ : F.obj X₂ ⟶ F.obj j) (f : X₁ ⟶ X₂),
    F.map f ≫ k₂ = k₁ → s.π.app X₁ ≫ G.map k₁ = s.π.app j → s.π.app X₂ ≫ G.map k₂ = s.π.app j
h₂ :
  ∀ (X₁ X₂ : C) (k₁ : F.obj X₁ ⟶ F.obj j) (k₂ : F.obj X₂ ⟶ F.obj j) (f : X₁ ⟶ X₂),
    F.map f ≫ k₂ = k₁ → s.π.app X₂ ≫ G.map k₂ = s.π.app j → s.π.app X₁ ≫ G.map k₁ = s.π.app j
z : s.π.app j ≫ G.map (F.map (𝟙 j)) = s.π.app j
X₀ : C
⊢ s.π.app (lift F (F.obj j)) ≫ G.map (homToLift F (F.obj j)) = s.π.app j
have k₀ : F.obj j ⟶ F.obj j
Tactic: apply induction F fun X k => s.π.app X ≫ G.map k = (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.Initial
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
s : Cone (F ⋙ G)
j j₁ j₂ : C
k₁ : F.obj j₁ ⟶ F.obj j
k₂ : F.obj j₂ ⟶ F.obj j
f : j₁ ⟶ j₂
w : F.map f ≫ k₂ = k₁
h : s.π.app j₁ ≫ G.map k₁ = s.π.app j
⊢ s.π.app j₂ ≫ G.map k₂ = s.π.app j
have h₁ : (s.π.app j₁ ≫ (F ⋙ G).map f) ≫ G.map k₂ = s.π.app j
Tactic: rw [← s.w f]
-- 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.Initial
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
s : Cone (F ⋙ G)
j j₁ j₂ : C
k₁ : F.obj j₁ ⟶ F.obj j
k₂ : F.obj j₂ ⟶ F.obj j
f : j₁ ⟶ j₂
w : F.map f ≫ k₂ = k₁
h : s.π.app j₁ ≫ G.map k₁ = s.π.app j
⊢ (s.π.app j₁ ≫ (F ⋙ G).map f) ≫ G.map k₂ = s.π.app j
have h₁ : s.π.app j₁ ≫ G.map (F.map f ≫ k₂) = s.π.app j
Tactic: rw [← w] 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.Initial
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
s : Cone (F ⋙ G)
j j₁ j₂ : C
k₁ : F.obj j₁ ⟶ F.obj j
k₂ : F.obj j₂ ⟶ F.obj j
f : j₁ ⟶ j₂
w : F.map f ≫ k₂ = k₁
h : s.π.app j₂ ≫ G.map k₂ = s.π.app j
⊢ s.π.app j₁ ≫ G.map k₁ = s.π.app j
have h₁ : (s.π.app j₁ ≫ (F ⋙ G).map f) ≫ G.map k₂ = s.π.app j
Tactic: rw [← s.w f] 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.Initial
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
s : Cone (F ⋙ G)
j j₁ j₂ : C
k₁ : F.obj j₁ ⟶ F.obj j
k₂ : F.obj j₂ ⟶ F.obj j
f : j₁ ⟶ j₂
w : F.map f ≫ k₂ = k₁
h : (s.π.app j₁ ≫ (F ⋙ G).map f) ≫ G.map k₂ = s.π.app j
⊢ s.π.app j₁ ≫ G.map k₁ = s.π.app j
have h₂ : s.π.app j₁ ≫ G.map (F.map f ≫ k₂) = s.π.app j
Tactic: rw [← w]
-- 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.Initial
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
B : Type u₄
inst_4 : Category.{v₄, u₄} B
H : Functor.{v₃, v₄, u₃, u₄} E B
inst_5 : PreservesLimit G H
c : Cone (F ⋙ G)
hc : IsLimit c
⊢ Nonempty (IsLimit (H.mapCone c))
have refine : IsLimit (obj extendCone (H.mapCone c))
Tactic: refine ⟨isLimitExtendConeEquiv (G := G ⋙ H) F (H.mapCone c) ?_⟩
-- 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.Initial
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
B : Type u₄
inst_4 : Category.{v₄, u₄} B
H : Functor.{v₃, v₄, u₃, u₄} E B
inst_5 : ReflectsLimit G H
c : Cone (F ⋙ G)
hc : IsLimit (H.mapCone c)
⊢ Nonempty (IsLimit c)
have refine : IsLimit (H.mapCone (obj extendCone c))
Tactic: refine ⟨isLimitExtendConeEquiv F _ (isLimitOfReflects 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.Initial
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
B : Type u₄
inst_4 : Category.{v₄, u₄} B
H : Functor.{v₃, v₄, u₃, u₄} E B
inst_5 : CreatesLimit G H
c : Cone ((F ⋙ G) ⋙ H)
hc : IsLimit c
⊢ LiftableCone (F ⋙ G) H c
have refine : H.mapCone
    (Cone.whisker F
      (liftLimit.{v₂, u₂, v₃, v₄, u₃, u₄} (D := B) (F := H) (c := obj extendCone c)
        (((Equiv.symm (isLimitExtendConeEquiv F c) : IsLimit c ≃ IsLimit (obj extendCone c)) :
            (a : IsLimit c) → IsLimit (extendCone.obj c))
          hc))) ≅
  c
Tactic: refine ⟨(liftLimit ((isLimitExtendConeEquiv F (G := G ⋙ H) _).symm hc)).whisker F, ?_⟩
-- 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.Initial
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_4 : HasLimit G
⊢ IsIso (X := limit G) (Y := limit (F ⋙ G)) (limit.pre G F)
have rw : IsIso (X := limit G) (Y := limit (F ⋙ G))
  (Iso.hom (limit.isoLimitCone (getLimitCone G)) ≫
    (limitConeComp F (getLimitCone G)).isLimit.lift (Cone.whisker F (getLimitCone G).cone) ≫
      Iso.inv (limit.isoLimitCone (limitConeComp F (getLimitCone G))))
Tactic: rw [limit.pre_eq (limitConeComp F (getLimitCone G)) (getLimitCone G)]
-- 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.Initial
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_4 : HasLimit G
⊢ IsIso (X := limit G) (Y := limit (F ⋙ G))
    (Iso.hom (limit.isoLimitCone (getLimitCone G)) ≫
      (limitConeComp F (getLimitCone G)).isLimit.lift (Cone.whisker F (getLimitCone G).cone) ≫
        Iso.inv (limit.isoLimitCone (limitConeComp F (getLimitCone G))))
have simp : IsIso (Y := limit (F ⋙ G)) (Iso.inv (limit.isoLimitCone (limitConeComp F (getLimitCone G))))
Tactic: simp only [limitConeComp_cone, Cone.whisker_pt, limitConeComp_isLimit, IsLimit.lift_self,
    Category.id_comp, isIso_comp_left_iff]
-- 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.Initial
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_4 : HasLimitsOfShape.{v₂, u₂, v₃, u₃} D E
inst_5 : HasLimitsOfShape.{v₁, u₁, v₃, u₃} C E
X Y : Functor.{v₂, v₃, u₂, u₃} D E
f : X ⟶ Y
⊢ Eq (α := obj lim X ⟶ obj (obj (whiskeringLeft C D E) F ⋙ lim) Y)
    (map lim f ≫
      Iso.hom ((fun (G : Functor.{v₂, v₃, u₂, u₃} D E) ↦ (Iso.symm (limitIso F G) : limit G ≅ limit (F ⋙ G))) Y))
    (Iso.hom ((fun (G : Functor.{v₂, v₃, u₂, u₃} D E) ↦ (Iso.symm (limitIso F G) : limit G ≅ limit (F ⋙ G))) X) ≫
      map (obj (whiskeringLeft C D E) F ⋙ lim) f)
have simp : Eq (α := limit X ⟶ limit (F ⋙ Y)) (CategoryStruct.comp (Y := limit Y) (limMap f) (limit.pre Y F))
  (CategoryStruct.comp (Y := limit (F ⋙ X)) (limit.pre X F) (limMap (F.whiskerLeft f)))
Tactic: simp only [comp_obj, whiskeringLeft_obj_obj, lim_obj, comp_map, whiskeringLeft_obj_map, lim_map,
      Iso.symm_hom, limitIso_inv]
-- 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.Initial
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_4 : HasLimitsOfShape.{v₂, u₂, v₃, u₃} D E
inst_5 : HasLimitsOfShape.{v₁, u₁, v₃, u₃} C E
X Y : Functor.{v₂, v₃, u₂, u₃} D E
f : X ⟶ Y
⊢ Eq (α := limit X ⟶ limit (F ⋙ Y)) (CategoryStruct.comp (Y := limit Y) (limMap f) (limit.pre Y F))
    (CategoryStruct.comp (Y := limit (F ⋙ X)) (limit.pre X F) (limMap (F.whiskerLeft f)))
have w : ∀ (j : C),
  Eq (α := limit X ⟶ (F ⋙ Y).obj j)
    (CategoryStruct.comp (Y := limit (F ⋙ Y)) (CategoryStruct.comp (Y := limit Y) (limMap f) (limit.pre Y F))
      (limit.π (F ⋙ Y) j))
    (CategoryStruct.comp (Y := limit (F ⋙ Y))
      (CategoryStruct.comp (Y := limit (F ⋙ X)) (limit.pre X F) (limMap (F.whiskerLeft f))) (limit.π (F ⋙ Y) j))
Tactic: ext