awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Final
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)
h₂ 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

Tactic:
rw [z, Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Limits.Final
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)
h₉ 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

Tactic:
rw [← a, Functor.map_comp, ← Functor.comp_map, ← Category.assoc, ← Category.assoc,
                c.w, z, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.Cone.w, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.comp_map
-- Module: Mathlib.CategoryTheory.Limits.Final
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₁ :
  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)
⊢ 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)

Tactic:
rw [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Final
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₂
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

Tactic:
apply induction (k₀ := f) (z := rfl) F fun Z g =>
    c.π.app Z ≫ G.map g = c.π.app X ≫ G.map f

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.Functor.map, CategoryTheory.Functor.Initial.induction, CategoryTheory.CategoryStruct.comp, Eq, CategoryTheory.NatTrans.app, rfl
-- Module: Mathlib.CategoryTheory.Limits.Final
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
X₁ : C
h₁ :
  ∀ (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₂
⊢ ∀ (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:
_
-- Module: Mathlib.CategoryTheory.Limits.Final
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
X₁ X₂ : C
h₁ :
  ∀ (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₂
⊢ ∀ (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:
_
-- Module: Mathlib.CategoryTheory.Limits.Final
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
X₁ X₂ : C
k₁ : F.obj X₁ ⟶ Y
h₁ :
  ∀ (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₂
⊢ ∀ (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:
_
-- Module: Mathlib.CategoryTheory.Limits.Final
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
X₁ X₂ : C
k₁ : F.obj X₁ ⟶ Y
k₂ : F.obj X₂ ⟶ Y
h₁ :
  ∀ (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₂
⊢ ∀ (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:
_
-- Module: Mathlib.CategoryTheory.Limits.Final
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
X₁ X₂ : C
k₁ : F.obj X₁ ⟶ Y
k₂ : F.obj X₂ ⟶ Y
f_1 : X₁ ⟶ X₂
h₁ : F.map f_1 ≫ k₂ = k₁
h₂ : c.π.app X₁ ≫ G.map k₁ = c.π.app X ≫ G.map f
⊢ c.π.app X₂ ≫ G.map k₂ = c.π.app X ≫ G.map f

Tactic:
simp [← h₂, ← h₁, ← Functor.comp_map]

Premises used: CategoryTheory.Functor.comp_map
-- Module: Mathlib.CategoryTheory.Limits.Final
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
X₁ : C
h₂ :
  ∀ (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₁
⊢ ∀ (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:
_
-- Module: Mathlib.CategoryTheory.Limits.Final
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
X₁ X₂ : C
h₂ :
  ∀ (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₁
⊢ ∀ (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:
_
-- Module: Mathlib.CategoryTheory.Limits.Final
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
X₁ X₂ : C
k₁ : F.obj X₁ ⟶ Y
h₂ :
  ∀ (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₁
⊢ ∀ (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:
_
-- Module: Mathlib.CategoryTheory.Limits.Final
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
X₁ X₂ : C
k₁ : F.obj X₁ ⟶ Y
k₂ : F.obj X₂ ⟶ Y
h₂ :
  ∀ (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₁
⊢ ∀ (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:
_
-- Module: Mathlib.CategoryTheory.Limits.Final
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
X₁ X₂ : C
k₁ : F.obj X₁ ⟶ Y
k₂ : F.obj X₂ ⟶ Y
f_1 : X₁ ⟶ X₂
h₁ : F.map f_1 ≫ k₂ = k₁
h₂ : c.π.app X₂ ≫ G.map k₂ = c.π.app X ≫ G.map f
⊢ c.π.app X₁ ≫ G.map k₁ = c.π.app X ≫ G.map f

Tactic:
simp [← h₁, ← Functor.comp_map, h₂]

Premises used: CategoryTheory.Functor.comp_map
-- Module: Mathlib.CategoryTheory.Limits.Final
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
k₀ : F.obj j ⟶ F.obj j
⊢ s.π.app (lift F (F.obj j)) ≫ G.map (homToLift F (F.obj j)) = s.π.app j

Tactic:
apply induction F fun X k => s.π.app X ≫ G.map k = (s.π.app j :)

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.Functor.map, CategoryTheory.Functor.Initial.induction, CategoryTheory.CategoryStruct.comp, Eq, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Limits.Final
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
h₁ : (s.π.app j₁ ≫ (F ⋙ G).map f) ≫ G.map k₂ = s.π.app j
⊢ s.π.app j₂ ≫ G.map k₂ = s.π.app j

Tactic:
rw [← s.w f]

Premises used: CategoryTheory.Limits.Cone.w
-- Module: Mathlib.CategoryTheory.Limits.Final
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 (F.map f ≫ k₂) = s.π.app j

Tactic:
rw [← w] at h
-- Module: Mathlib.CategoryTheory.Limits.Final
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 (F.map f ≫ k₂) = s.π.app j
⊢ (s.π.app j₁ ≫ (F ⋙ G).map f) ≫ G.map k₂ = s.π.app j

Tactic:
simpa using h
-- Module: Mathlib.CategoryTheory.Limits.Final
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

Tactic:
rw [← s.w f] at h

Premises used: CategoryTheory.Limits.Cone.w
-- Module: Mathlib.CategoryTheory.Limits.Final
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
h₂ : s.π.app j₁ ≫ G.map (F.map f ≫ k₂) = s.π.app j
⊢ s.π.app j₁ ≫ G.map k₁ = s.π.app j

Tactic:
rw [← w]
-- Module: Mathlib.CategoryTheory.Limits.Final
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 (F.map f ≫ k₂) = s.π.app j

Tactic:
simpa using h
-- Module: Mathlib.CategoryTheory.Limits.Final
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 j ≫ G.map (F.map (𝟙 j)) = s.π.app j

Tactic:
s.w (𝟙 _)

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Limits.Cone.w
-- Module: Mathlib.CategoryTheory.Limits.Final
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 j ≫ G.map (F.map (𝟙 j)) = s.π.app j

Tactic:
exact s.w (𝟙 _)

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Limits.Cone.w
-- Module: Mathlib.CategoryTheory.Limits.Final
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
⊢ HasLimit (F ⋙ G)

Tactic:
HasLimit.mk (limitConeComp F (getLimitCone G))

Premises used: CategoryTheory.Functor.Initial.limitConeComp, CategoryTheory.Limits.getLimitCone, CategoryTheory.Limits.HasLimit.mk
-- Module: Mathlib.CategoryTheory.Limits.Final
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))

Tactic:
⟨isLimitExtendConeEquiv (G := G ⋙ H) F (H.mapCone c) ?_⟩

Premises used: CategoryTheory.Functor.Initial.isLimitExtendConeEquiv, Nonempty.intro, CategoryTheory.Functor.mapCone, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Limits.Final
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
refine : IsLimit (obj extendCone (H.mapCone c))
⊢ Nonempty (IsLimit (H.mapCone c))

Tactic:
refine ⟨isLimitExtendConeEquiv (G := G ⋙ H) F (H.mapCone c) ?_⟩
-- Module: Mathlib.CategoryTheory.Limits.Final
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
hc' : IsLimit (H.mapCone (obj extendCone c)) :=
  isLimitOfPreserves H ((Equiv.symm (isLimitExtendConeEquiv F c) : (a : IsLimit c) → IsLimit (extendCone.obj c)) hc)
⊢ ∀ (j : D),
    (H.mapCone (obj extendCone c)).π.app j =
      Iso.hom (Iso.refl (H.mapCone (obj extendCone c)).pt) ≫ NatTrans.app (obj extendCone (H.mapCone c)).π j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Final
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
hc' : IsLimit (H.mapCone (obj extendCone c)) :=
  isLimitOfPreserves H ((Equiv.symm (isLimitExtendConeEquiv F c) : (a : IsLimit c) → IsLimit (extendCone.obj c)) hc)
⊢ IsLimit (obj extendCone (H.mapCone c))

Tactic:
exact IsLimit.ofIsoLimit hc' (Cone.ext (Iso.refl _) (by simp))

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Limits.IsLimit.ofIsoLimit, CategoryTheory.Limits.Cone.ext
-- Module: Mathlib.CategoryTheory.Limits.Final
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)

Tactic:
⟨isLimitExtendConeEquiv F _ (isLimitOfReflects H ?_)⟩

Premises used: CategoryTheory.Functor.Initial.isLimitExtendConeEquiv, CategoryTheory.Limits.isLimitOfReflects, Nonempty.intro, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Limits.Final
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)
refine : IsLimit (H.mapCone (obj extendCone c))
⊢ Nonempty (IsLimit c)

Tactic:
refine ⟨isLimitExtendConeEquiv F _ (isLimitOfReflects H ?_)⟩
-- Module: Mathlib.CategoryTheory.Limits.Final
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)
hc' : IsLimit (obj extendCone (H.mapCone c)) :=
  ((Equiv.symm (isLimitExtendConeEquiv F (H.mapCone c)) :
        IsLimit (H.mapCone c) ≃ IsLimit (obj extendCone (H.mapCone c))) :
      (a : IsLimit (H.mapCone c)) → IsLimit (extendCone.obj (H.mapCone c)))
    hc
⊢ ∀ (j : D),
    NatTrans.app (obj extendCone (H.mapCone c)).π j =
      Iso.hom (Iso.refl (obj extendCone (H.mapCone c)).pt) ≫ (H.mapCone (obj extendCone c)).π.app j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Final
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)
hc' : IsLimit (obj extendCone (H.mapCone c)) :=
  ((Equiv.symm (isLimitExtendConeEquiv F (H.mapCone c)) :
        IsLimit (H.mapCone c) ≃ IsLimit (obj extendCone (H.mapCone c))) :
      (a : IsLimit (H.mapCone c)) → IsLimit (extendCone.obj (H.mapCone c)))
    hc
⊢ IsLimit (H.mapCone (obj extendCone c))

Tactic:
exact IsLimit.ofIsoLimit hc' (Cone.ext (Iso.refl _) (by simp))

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Limits.IsLimit.ofIsoLimit, CategoryTheory.Limits.Cone.ext