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
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
adj : L ⊣ R
c : C
u : StructuredArrow c R := StructuredArrow.mk (adj.unit.app c)
f g : StructuredArrow c R
⊢ u.hom ≫
      R.map
        (((Equiv.symm (adj.homEquiv c g.right) : Equiv.{v₁ + 1, v₂ + 1} (c ⟶ R.obj g.right) (L.obj c ⟶ g.right)) :
            (a : c ⟶ R.obj g.right) → L.obj c ⟶ g.right)
          g.hom) =
    g.hom

Tactic:
simp [u]
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
adj : L ⊣ R
d : D
u : CostructuredArrow L d := CostructuredArrow.mk (adj.counit.app d)
f g : CostructuredArrow L d
⊢ L.map
        (((adj.homEquiv f.left d : Equiv.{v₂ + 1, v₁ + 1} (L.obj f.left ⟶ d) (f.left ⟶ R.obj d)) :
            (a : L.obj f.left ⟶ d) → f.left ⟶ R.obj d)
          f.hom) ≫
      u.hom =
    f.hom

Tactic:
simp [u]
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
adj : L ⊣ R
d : D
u : CostructuredArrow L d := CostructuredArrow.mk (adj.counit.app d)
f g : CostructuredArrow L d
⊢ L.map
        (((adj.homEquiv g.left d : Equiv.{v₂ + 1, v₁ + 1} (L.obj g.left ⟶ d) (g.left ⟶ R.obj d)) :
            (a : L.obj g.left ⟶ d) → g.left ⟶ R.obj d)
          g.hom) ≫
      u.hom =
    g.hom

Tactic:
simp [u]
-- 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.IsRightAdjoint
⊢ F.Final

Tactic:
final_of_adjunction (Adjunction.ofIsRightAdjoint F)

Premises used: CategoryTheory.Functor.final_of_adjunction, CategoryTheory.Adjunction.ofIsRightAdjoint
-- 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.IsLeftAdjoint
⊢ F.Initial

Tactic:
initial_of_adjunction (Adjunction.ofIsLeftAdjoint F)

Premises used: CategoryTheory.Functor.initial_of_adjunction, CategoryTheory.Adjunction.ofIsLeftAdjoint
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F F' : Functor.{v₁, v₂, u₁, u₂} C D
i : F ≅ F'
⊢ F.Final ↔ F'.Final

Tactic:
⟨fun _ => final_of_natIso i, fun _ => final_of_natIso i.symm⟩

Premises used: CategoryTheory.Functor.final_of_natIso, Iff.intro, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F F' : Functor.{v₁, v₂, u₁, u₂} C D
i : F ≅ F'
⊢ F.Initial ↔ F'.Initial

Tactic:
⟨fun _ => initial_of_natIso i, fun _ => initial_of_natIso i.symm⟩

Premises used: Iff.intro, CategoryTheory.Iso.symm, CategoryTheory.Functor.initial_of_natIso
-- 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.Final
d : D
⊢ Nonempty (StructuredArrow d F)

Tactic:
IsConnected.is_nonempty

Premises used: CategoryTheory.IsConnected.is_nonempty
-- 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.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 : Nonempty.{u_1} (Z (lift F d) (homToLift F d))
⊢ Z (lift F d) (homToLift F d)

Tactic:
apply Nonempty.some

Premises used: Nonempty.some
-- 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.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))

Tactic:
isPreconnected_induction (Z := fun Y : StructuredArrow d F => Z Y.right Y.hom)
    ?_ ?_ (j₀ := StructuredArrow.mk k₀) z _

Premises used: CategoryTheory.StructuredArrow.hom, CategoryTheory.isPreconnected_induction, CategoryTheory.StructuredArrow.right, CategoryTheory.Functor.Final.lift, CategoryTheory.Functor.Final.homToLift
-- 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.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₂
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))

Tactic:
refine isPreconnected_induction (Z := fun Y : StructuredArrow d F => Z Y.right Y.hom)
    ?_ ?_ (j₀ := StructuredArrow.mk k₀) z _

Premises used: CategoryTheory.StructuredArrow.hom, CategoryTheory.isPreconnected_induction, CategoryTheory.StructuredArrow.right
-- 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.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₀
⊢ {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:
exact fun f a ↦ h₁ _ _ _ _ f.right f.w a
-- 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.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₀
⊢ {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:
exact fun f a ↦ h₂ _ _ _ _ f.right f.w a
-- 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.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
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)
⊢ 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)

Tactic:
dsimp
-- 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.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
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)
⊢ 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:
simp only [Category.comp_id]

Premises used: CategoryTheory.Category.comp_id
-- 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.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
k₀ : X ⟶ F.obj (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)

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

Premises used: CategoryTheory.Functor.Final.induction, CategoryTheory.Functor.map, CategoryTheory.Limits.Cocone.ι, CategoryTheory.CategoryStruct.comp, CategoryTheory.Functor.Final.lift, Eq, CategoryTheory.NatTrans.app, CategoryTheory.Functor.Final.homToLift
-- 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.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₁
h₆ h₇ : G.map k₁ ≫ c.ι.app Z₁ = 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₂

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

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.Cocone.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.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₁

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

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.Cocone.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.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₂ h₃ : G.map k₁ ≫ c.ι.app Z₁ = 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₁

Tactic:
rw [z]
-- 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.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₁ :
  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))
⊢ 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:
rw [← Functor.map_comp_assoc]

Premises used: CategoryTheory.Functor.map_comp_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.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₂
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

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

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

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

Premises used: CategoryTheory.Limits.Cocone.ι, CategoryTheory.NatTrans.naturality, 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.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
X₁ : C
h₂ :
  ∀ (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₁
⊢ ∀ (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:
_
-- 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.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
X₁ X₂ : C
h₂ :
  ∀ (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₁
⊢ ∀ (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:
_
-- 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.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
X₁ X₂ : C
k₁ : X ⟶ F.obj X₁
h₂ :
  ∀ (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₁
⊢ ∀ (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:
_
-- 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.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
X₁ X₂ : C
k₁ : X ⟶ F.obj X₁
k₂ : X ⟶ F.obj X₂
h₂ :
  ∀ (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₁
⊢ ∀ (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:
_