awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.StrictInitial (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictTerminalObjects.{v, u} C
J : Type v
inst_2 : SmallCategory J
F : J ⥤ C
inst_3 : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal.{v, u} (F.obj j)
inst_4 : Subsingleton.{v + 1} (i ⟶ i)
j : J
⊢ limit.π F i ≫
      NatTrans.app
        (Cone.π
          { pt := F.1 i,
            π :=
              {
                app := fun (j : J) ↦
                  if h : j = i then eqToHom ⋯ else (H j h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j),
                naturality := ⋯ } })
        j =
    𝟙 (limit F) ≫ limit.π F j
have refine_3 : (limit.π F i ≫ if h : j = i then eqToHom sorry else (H j h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j)) =
  𝟙 (limit F) ≫ limit.π F j
Tactic: dsimp only
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.StrictInitial (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictTerminalObjects.{v, u} C
J : Type v
inst_2 : SmallCategory J
F : J ⥤ C
inst_3 : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal.{v, u} (F.obj j)
inst_4 : Subsingleton.{v + 1} (i ⟶ i)
j : J
⊢ (limit.π F i ≫
      if h : j = i then eqToHom ⋯ else (H j h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j)) =
    𝟙 (limit F) ≫ limit.π F j
have pos : ∀ (h : j = i), limit.π F i ≫ eqToHom sorry = 𝟙 (limit F) ≫ limit.π F j
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.StrictInitial (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictTerminalObjects.{v, u} C
J : Type v
inst_2 : SmallCategory J
F : J ⥤ C
inst_3 : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal.{v, u} (F.obj j)
inst_4 : Subsingleton.{v + 1} (i ⟶ i)
j : J
pos : ∀ (h : j = i), limit.π F i ≫ eqToHom ⋯ = 𝟙 (limit F) ≫ limit.π F j
⊢ (limit.π F i ≫
      if h : j = i then eqToHom ⋯ else (H j h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j)) =
    𝟙 (limit F) ≫ limit.π F j
have neg : ∀ (h : ¬j = i),
  limit.π F i ≫ (H j h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j) = 𝟙 (limit F) ≫ limit.π F j
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.StrictInitial (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictTerminalObjects.{v, u} C
J : Type v
inst_2 : SmallCategory J
F : J ⥤ C
inst_3 : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal.{v, u} (F.obj j)
inst_4 : Subsingleton.{v + 1} (i ⟶ i)
j : J
h : j = i
⊢ limit.π F i ≫ eqToHom ⋯ = 𝟙 (limit F) ≫ limit.π F j
have pos : limit.π F i ≫ eqToHom sorry = 𝟙 (limit F) ≫ limit.π F i
Tactic: cases h
Cleared hypotheses: j, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.StrictInitial (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictTerminalObjects.{v, u} C
J : Type v
inst_2 : SmallCategory J
F : J ⥤ C
inst_3 : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal.{v, u} (F.obj j)
inst_4 : Subsingleton.{v + 1} (i ⟶ i)
⊢ limit.π F i ≫ eqToHom ⋯ = 𝟙 (limit F) ≫ limit.π F i
have pos : Eq (α := limit F ⟶ F.obj i) (limit.π F i ≫ 𝟙 (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) i)) (limit.π F i)
Tactic: rw [id_comp, eqToHom_refl]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.StrictInitial (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictTerminalObjects.{v, u} C
J : Type v
inst_2 : SmallCategory J
F : J ⥤ C
inst_3 : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal.{v, u} (F.obj j)
inst_4 : Subsingleton.{v + 1} (i ⟶ i)
⊢ IsIso (X := limit F) (limit.π F i)
have refine_1 : (X : J) → Functor.obj (Functor.obj (Functor.const J) (F.1 i)) X ⟶ F.obj X
Tactic: classical
    refine ⟨⟨limit.lift _ ⟨_, ⟨?_, ?_⟩⟩, ?_, ?_⟩⟩
    · exact fun j =>
        dite (j = i)
          (fun h => eqToHom (by cases h; rfl))
          fun h => (H _ h).from _
    · intro j k f
      split_ifs with h h_1 h_1
      · cases h
        cases h_1
        obtain rfl : f = 𝟙 _ := Subsingleton.elim _ _
        simp
      · cases h
        haveI : IsIso (F.map f) := (H _ h_1).isIso_from _
        rw [← IsIso.comp_inv_eq]
        apply (H _ h_1).hom_ext
      · cases h_1
        apply (H _ h).hom_ext
      · apply (H _ h).hom_ext
    · ext
      rw [assoc, limit.lift_π]
      dsimp only
      split_ifs with h
      · cases h
        rw [id_comp, eqToHom_refl]
        exact comp_id _
      · apply (H _ h).hom_ext
    · simp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.StrictInitial (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictTerminalObjects.{v, u} C
J : Type v
inst_2 : SmallCategory J
F : J ⥤ C
inst_3 : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal.{v, u} (F.obj j)
inst_4 : Subsingleton.{v + 1} (i ⟶ i)
refine_1 : (X : J) → Functor.obj (Functor.obj (Functor.const J) (F.1 i)) X ⟶ F.obj X
⊢ IsIso (X := limit F) (limit.π F i)
have refine_2 : ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
  Eq (α := Functor.obj (Functor.obj (Functor.const J) (F.1 i)) X ⟶ F.obj Y)
    (Functor.map (Functor.obj (Functor.const J) (F.1 i)) f ≫
      if h : Y = i then eqToHom sorry else (H Y h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) Y))
    ((if h : X = i then eqToHom sorry else (H X h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) X)) ≫ F.map f)
Tactic: classical
    refine ⟨⟨limit.lift _ ⟨_, ⟨?_, ?_⟩⟩, ?_, ?_⟩⟩
    · exact fun j =>
        dite (j = i)
          (fun h => eqToHom (by cases h; rfl))
          fun h => (H _ h).from _
    · intro j k f
      split_ifs with h h_1 h_1
      · cases h
        cases h_1
        obtain rfl : f = 𝟙 _ := Subsingleton.elim _ _
        simp
      · cases h
        haveI : IsIso (F.map f) := (H _ h_1).isIso_from _
        rw [← IsIso.comp_inv_eq]
        apply (H _ h_1).hom_ext
      · cases h_1
        apply (H _ h).hom_ext
      · apply (H _ h).hom_ext
    · ext
      rw [assoc, limit.lift_π]
      dsimp only
      split_ifs with h
      · cases h
        rw [id_comp, eqToHom_refl]
        exact comp_id _
      · apply (H _ h).hom_ext
    · simp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.StrictInitial (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictTerminalObjects.{v, u} C
J : Type v
inst_2 : SmallCategory J
F : J ⥤ C
inst_3 : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal.{v, u} (F.obj j)
inst_4 : Subsingleton.{v + 1} (i ⟶ i)
refine_1 : (X : J) → Functor.obj (Functor.obj (Functor.const J) (F.1 i)) X ⟶ F.obj X
refine_2 :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    Eq (α := Functor.obj (Functor.obj (Functor.const J) (F.1 i)) X ⟶ F.obj Y)
      (Functor.map (Functor.obj (Functor.const J) (F.1 i)) f ≫
        if h : Y = i then eqToHom ⋯ else (H Y h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) Y))
      ((if h : X = i then eqToHom ⋯ else (H X h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) X)) ≫
        F.map f)
⊢ IsIso (X := limit F) (limit.π F i)
have refine_3 : limit.π F i ≫
    limit.lift F
      { pt := F.1 i,
        π :=
          {
            app := fun (j : J) ↦
              if h : j = i then eqToHom sorry else (H j h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j),
            naturality := sorry } } =
  𝟙 (limit F)
Tactic: classical
    refine ⟨⟨limit.lift _ ⟨_, ⟨?_, ?_⟩⟩, ?_, ?_⟩⟩
    · exact fun j =>
        dite (j = i)
          (fun h => eqToHom (by cases h; rfl))
          fun h => (H _ h).from _
    · intro j k f
      split_ifs with h h_1 h_1
      · cases h
        cases h_1
        obtain rfl : f = 𝟙 _ := Subsingleton.elim _ _
        simp
      · cases h
        haveI : IsIso (F.map f) := (H _ h_1).isIso_from _
        rw [← IsIso.comp_inv_eq]
        apply (H _ h_1).hom_ext
      · cases h_1
        apply (H _ h).hom_ext
      · apply (H _ h).hom_ext
    · ext
      rw [assoc, limit.lift_π]
      dsimp only
      split_ifs with h
      · cases h
        rw [id_comp, eqToHom_refl]
        exact comp_id _
      · apply (H _ h).hom_ext
    · simp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.StrictInitial (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictTerminalObjects.{v, u} C
J : Type v
inst_2 : SmallCategory J
F : J ⥤ C
inst_3 : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal.{v, u} (F.obj j)
inst_4 : Subsingleton.{v + 1} (i ⟶ i)
refine_1 : (X : J) → Functor.obj (Functor.obj (Functor.const J) (F.1 i)) X ⟶ F.obj X
refine_2 :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    Eq (α := Functor.obj (Functor.obj (Functor.const J) (F.1 i)) X ⟶ F.obj Y)
      (Functor.map (Functor.obj (Functor.const J) (F.1 i)) f ≫
        if h : Y = i then eqToHom ⋯ else (H Y h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) Y))
      ((if h : X = i then eqToHom ⋯ else (H X h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) X)) ≫
        F.map f)
refine_3 :
  limit.π F i ≫
      limit.lift F
        { pt := F.1 i,
          π :=
            {
              app := fun (j : J) ↦
                if h : j = i then eqToHom ⋯ else (H j h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j),
              naturality := ⋯ } } =
    𝟙 (limit F)
⊢ IsIso (X := limit F) (limit.π F i)
have refine_4 : Eq (α := F.obj i ⟶ F.obj i)
  (CategoryStruct.comp (Y := limit F)
      (limit.lift F
        { pt := F.1 i,
          π :=
            {
              app := fun (j : J) ↦
                if h : j = i then eqToHom sorry else (H j h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j),
              naturality := sorry } })
      (limit.π F i) :
    F.obj i ⟶ F.obj i)
  (𝟙 (F.obj i) : F.obj i ⟶ F.obj i)
Tactic: classical
    refine ⟨⟨limit.lift _ ⟨_, ⟨?_, ?_⟩⟩, ?_, ?_⟩⟩
    · exact fun j =>
        dite (j = i)
          (fun h => eqToHom (by cases h; rfl))
          fun h => (H _ h).from _
    · intro j k f
      split_ifs with h h_1 h_1
      · cases h
        cases h_1
        obtain rfl : f = 𝟙 _ := Subsingleton.elim _ _
        simp
      · cases h
        haveI : IsIso (F.map f) := (H _ h_1).isIso_from _
        rw [← IsIso.comp_inv_eq]
        apply (H _ h_1).hom_ext
      · cases h_1
        apply (H _ h).hom_ext
      · apply (H _ h).hom_ext
    · ext
      rw [assoc, limit.lift_π]
      dsimp only
      split_ifs with h
      · cases h
        rw [id_comp, eqToHom_refl]
        exact comp_id _
      · apply (H _ h).hom_ext
    · simp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.StrictInitial (goal)
Goal:
C : Type u
inst : Category.{v, u} C
I : C
h : ∀ (A : C) (f : I ⟶ A), IsIso f
I' A : C
f : I' ⟶ A
hI' : IsTerminal.{v, u} I'
this : IsIso (hI'.from I ≫ f)
⊢ (inv (hI'.from I ≫ f) ≫ hI'.from I) ≫ f = 𝟙 A
have rw : inv (hI'.from I ≫ f) ≫ hI'.from I ≫ f = 𝟙 A
Tactic: rw [assoc, IsIso.inv_hom_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.StrictInitial (goal)
Goal:
C : Type u
inst : Category.{v, u} C
I : C
h : ∀ (A : C) (f : I ⟶ A), IsIso f
I' A : C
f : I' ⟶ A
hI' : IsTerminal.{v, u} I'
this : IsIso (hI'.from I ≫ f)
rw : inv (hI'.from I ≫ f) ≫ hI'.from I ≫ f = 𝟙 A
⊢ (inv (hI'.from I ≫ f) ≫ hI'.from I) ≫ f = 𝟙 A
have rw₁ : Eq.{v + 1} (α := A ⟶ A) (𝟙 A) (𝟙 A)
Tactic: rw [assoc, IsIso.inv_hom_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.StrongEpi (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst_1 : StrongEpi (f ≫ g)
X Y : C
z : X ⟶ Y
h : Mono z
⊢ HasLiftingProperty g z
have sq_hasLift : ∀ {f : Q ⟶ X} {g_1 : R ⟶ Y} (sq : CommSq f g z g_1), sq.HasLift
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.StrongEpi (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst_1 : StrongEpi (f ≫ g)
X Y : C
z : X ⟶ Y
h : Mono z
u : Q ⟶ X
v : R ⟶ Y
sq : CommSq u g z v
⊢ sq.HasLift
have h₀ : (f ≫ u) ≫ z = (f ≫ g) ≫ v
Tactic: have h₀ : (f ≫ u) ≫ z = (f ≫ g) ≫ v := by simp only [Category.assoc, sq.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.StrongEpi (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst_1 : StrongMono (f ≫ g)
X Y : C
z : X ⟶ Y
inst_2 : Epi z
⊢ HasLiftingProperty z f
have sq_hasLift : ∀ {f_1 : X ⟶ P} {g : Y ⟶ Q} (sq : CommSq f_1 z f g), sq.HasLift
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.StrongEpi (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst_1 : StrongMono (f ≫ g)
X Y : C
z : X ⟶ Y
inst_2 : Epi z
u : X ⟶ P
v : Y ⟶ Q
sq : CommSq u z f v
⊢ u ≫ f ≫ g = z ≫ v ≫ g
have rw : (u ≫ f) ≫ g = z ≫ v ≫ g
Tactic: rw [← Category.assoc, eq_whisker sq.w, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.StrongEpi (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst_1 : StrongMono (f ≫ g)
X Y : C
z : X ⟶ Y
inst_2 : Epi z
u : X ⟶ P
v : Y ⟶ Q
sq : CommSq u z f v
rw : (u ≫ f) ≫ g = z ≫ v ≫ g
⊢ u ≫ f ≫ g = z ≫ v ≫ g
have rw₁ : (z ≫ v) ≫ g = z ≫ v ≫ g
Tactic: rw [← Category.assoc, eq_whisker sq.w, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.StrongEpi (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst_1 : StrongMono (f ≫ g)
X Y : C
z : X ⟶ Y
inst_2 : Epi z
u : X ⟶ P
v : Y ⟶ Q
sq : CommSq u z f v
rw : (u ≫ f) ≫ g = z ≫ v ≫ g
rw₁ : (z ≫ v) ≫ g = z ≫ v ≫ g
⊢ u ≫ f ≫ g = z ≫ v ≫ g
have rw₂ : z ≫ v ≫ g = z ≫ v ≫ g
Tactic: rw [← Category.assoc, eq_whisker sq.w, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.StrongEpi (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst_1 : StrongMono (f ≫ g)
X Y : C
z : X ⟶ Y
inst_2 : Epi z
u : X ⟶ P
v : Y ⟶ Q
sq : CommSq u z f v
⊢ sq.HasLift
have h₀ : u ≫ f ≫ g = z ≫ v ≫ g
Tactic: have h₀ : u ≫ f ≫ g = z ≫ v ≫ g := by
        rw [← Category.assoc, eq_whisker sq.w, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.StrongEpi (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
h : StrongEpi f
⊢ Epi g
have rw : Epi (Arrow.Hom.left e.inv ≫ f ≫ Arrow.Hom.right e.hom)
Tactic: rw [Arrow.iso_w' e]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.StrongEpi (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
h : StrongMono f
⊢ Mono g
have rw : Mono (Arrow.Hom.left e.inv ≫ f ≫ Arrow.Hom.right e.hom)
Tactic: rw [Arrow.iso_w' e]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.StrongEpi (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
⊢ StrongEpi f ↔ StrongEpi g
have mp : StrongEpi f → StrongEpi g
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.StrongEpi (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
mp : StrongEpi f → StrongEpi g
⊢ StrongEpi f ↔ StrongEpi g
have mpr : StrongEpi g → StrongEpi f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.StrongEpi (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
⊢ StrongMono f ↔ StrongMono g
have mp : StrongMono f → StrongMono g
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.StrongEpi (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
mp : StrongMono f → StrongMono g
⊢ StrongMono f ↔ StrongMono g
have mpr : StrongMono g → StrongMono f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Terminal (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
j : J
I : IsInitial.{v, u} j
F : Functor.{v, v₁, u, u₁} J C
inst_2 : HasLimit F
⊢ limit.π F j ≫ limit.lift F (coneOfDiagramInitial I F) = 𝟙 (limit F)
have w : ∀ (j_1 : J),
  CategoryStruct.comp (Y := limit F) (limit.π F j ≫ limit.lift F (coneOfDiagramInitial I F)) (limit.π F j_1) =
    𝟙 (limit F) ≫ limit.π F j_1
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Terminal (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
j : J
I : IsTerminal.{v, u} j
F : Functor.{v, v₁, u, u₁} J C
inst_2 : HasLimit F
inst_3 : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
⊢ limit.π F j ≫ limit.lift F (coneOfDiagramTerminal I F) = 𝟙 (limit F)
have w : ∀ (j_1 : J),
  CategoryStruct.comp (Y := limit F) (limit.π F j ≫ limit.lift F (coneOfDiagramTerminal I F)) (limit.π F j_1) =
    𝟙 (limit F) ≫ limit.π F j_1
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Terminal (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
j : J
I : IsTerminal.{v, u} j
F : Functor.{v, v₁, u, u₁} J C
inst_2 : HasColimit F
⊢ CategoryStruct.comp (Y := F.obj j)
      (colimit.desc F (coconeOfDiagramTerminal I F) : colimit F ⟶ (coconeOfDiagramTerminal I F).pt) (colimit.ι F j) =
    𝟙 (colimit F)
have w : ∀ (j_1 : J),
  CategoryStruct.comp (Y := colimit F) (colimit.ι F j_1)
      (CategoryStruct.comp (Y := F.obj j)
        (colimit.desc F (coconeOfDiagramTerminal I F) : colimit F ⟶ (coconeOfDiagramTerminal I F).pt) (colimit.ι F j)) =
    colimit.ι F j_1 ≫ 𝟙 (colimit F)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Terminal (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
j : J
I : IsInitial.{v, u} j
F : Functor.{v, v₁, u, u₁} J C
inst_2 : HasColimit F
inst_3 : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
⊢ CategoryStruct.comp (Y := F.obj j)
      (colimit.desc F (coconeOfDiagramInitial I F) : colimit F ⟶ (coconeOfDiagramInitial I F).pt) (colimit.ι F j) =
    𝟙 (colimit F)
have w : ∀ (j_1 : J),
  CategoryStruct.comp (Y := colimit F) (colimit.ι F j_1)
      (CategoryStruct.comp (Y := F.obj j)
        (colimit.desc F (coconeOfDiagramInitial I F) : colimit F ⟶ (coconeOfDiagramInitial I F).pt) (colimit.ι F j)) =
    colimit.ι F j_1 ≫ 𝟙 (colimit F)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Terminal (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
j : J
I : IsInitial.{v, u} j
F : Functor.{v, v₁, u, u₁} J C
inst_2 : HasColimit F
inst_3 : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
⊢ Eq (α := F.obj j ⟶ F.obj j)
      (CategoryStruct.comp (Y := colimit F) (colimit.ι F j) (colimit.desc F (coconeOfDiagramInitial I F)) :
        F.obj j ⟶ F.obj j)
      (𝟙 (F.obj j) : F.obj j ⟶ F.obj j) ∧
    CategoryStruct.comp (Y := F.obj j)
        (colimit.desc F (coconeOfDiagramInitial I F) : colimit F ⟶ (coconeOfDiagramInitial I F).pt) (colimit.ι F j) =
      𝟙 (colimit F)
have refine : Eq (α := F.obj j ⟶ F.obj j)
  (CategoryStruct.comp (Y := colimit F) (colimit.ι F j) (colimit.desc F (coconeOfDiagramInitial I F)) :
    F.obj j ⟶ F.obj j)
  (𝟙 (F.obj j) : F.obj j ⟶ F.obj j)
Tactic: refine ⟨?_, by ext; simp⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Terminal (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
j : J
I : IsInitial.{v, u} j
F : Functor.{v, v₁, u, u₁} J C
inst_2 : HasColimit F
inst_3 : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
⊢ Eq (α := F.obj j ⟶ F.obj j)
    (CategoryStruct.comp (Y := colimit F) (colimit.ι F j) (colimit.desc F (coconeOfDiagramInitial I F)) :
      F.obj j ⟶ F.obj j)
    (𝟙 (F.obj j) : F.obj j ⟶ F.obj j)
have simp : inv (F.map (𝟙 j)) = 𝟙 (F.obj j)
Tactic: simp only [colimit.ι_desc, coconeOfDiagramInitial_pt, coconeOfDiagramInitial_ι_app,
      Functor.const_obj_obj, IsInitial.to_self]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : Functor.{w, v, w, u} (WalkingParallelFamily J) C
j : WalkingParallelFamily J
⊢ F.obj j = Functor.obj.{w, v, w, u} (parallelFamily (X := F.obj zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j)) j
have zero : F.obj zero =
  Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
    (parallelFamily (X := F.obj zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j)) zero
Tactic: cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : Functor.{w, v, w, u} (WalkingParallelFamily J) C
j : WalkingParallelFamily J
zero :
  F.obj WalkingParallelFamily.zero =
    Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
      (parallelFamily (X := F.obj WalkingParallelFamily.zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j))
      WalkingParallelFamily.zero
⊢ F.obj j =
    Functor.obj.{w, v, w, u}
      (parallelFamily (X := F.obj WalkingParallelFamily.zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j)) j
have one : F.obj one =
  Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
    (parallelFamily (X := F.obj WalkingParallelFamily.zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j)) one
Tactic: cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X_1 Y : C
f : J → (X_1 ⟶ Y)
X : WalkingParallelFamily (ULift.{w, 0} Bool)
⊢ Functor.obj (𝟭 (WalkingParallelFamily (ULift.{w, 0} Bool))) X =
    Functor.obj
      ((parallelFamily (X := WalkingParallelPair.zero) (Y := WalkingParallelPair.one) fun (p : ULift.{w, 0} Bool) ↦
          bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right) ⋙
        parallelPair (line { down := true : ULift.{w, 0} Bool }) (line { down := false : ULift.{w, 0} Bool }))
      X
have zero : Eq.{w + 1} (α := WalkingParallelFamily (ULift.{w, 0} Bool))
  (Functor.obj (𝟭 (WalkingParallelFamily (ULift.{w, 0} Bool))) zero)
  (Functor.obj (C := WalkingParallelFamily (ULift.{w, 0} Bool))
    ((parallelFamily (X := WalkingParallelPair.zero) (Y := WalkingParallelPair.one) fun (p : ULift.{w, 0} Bool) ↦
        bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right) ⋙
      parallelPair (line { down := true : ULift.{w, 0} Bool }) (line { down := false : ULift.{w, 0} Bool }))
    zero)
Tactic: cases X
Cleared hypotheses: X
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X_1 Y : C
f : J → (X_1 ⟶ Y)
X : WalkingParallelFamily (ULift.{w, 0} Bool)
zero :
  Eq.{w + 1} (α := WalkingParallelFamily (ULift.{w, 0} Bool))
    (Functor.obj (𝟭 (WalkingParallelFamily (ULift.{w, 0} Bool))) WalkingParallelFamily.zero)
    (Functor.obj (C := WalkingParallelFamily (ULift.{w, 0} Bool))
      ((parallelFamily (X := WalkingParallelPair.zero) (Y := WalkingParallelPair.one) fun (p : ULift.{w, 0} Bool) ↦
          bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right) ⋙
        parallelPair (line { down := true : ULift.{w, 0} Bool }) (line { down := false : ULift.{w, 0} Bool }))
      WalkingParallelFamily.zero)
⊢ Functor.obj (𝟭 (WalkingParallelFamily (ULift.{w, 0} Bool))) X =
    Functor.obj
      ((parallelFamily (X := WalkingParallelPair.zero) (Y := WalkingParallelPair.one) fun (p : ULift.{w, 0} Bool) ↦
          bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right) ⋙
        parallelPair (line { down := true : ULift.{w, 0} Bool }) (line { down := false : ULift.{w, 0} Bool }))
      X
have one : Eq.{w + 1} (α := WalkingParallelFamily (ULift.{w, 0} Bool))
  (Functor.obj (𝟭 (WalkingParallelFamily (ULift.{w, 0} Bool))) one)
  (Functor.obj (C := WalkingParallelFamily (ULift.{w, 0} Bool))
    ((parallelFamily (X := WalkingParallelPair.zero) (Y := WalkingParallelPair.one) fun (p : ULift.{w, 0} Bool) ↦
        bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right) ⋙
      parallelPair (line { down := true : ULift.{w, 0} Bool }) (line { down := false : ULift.{w, 0} Bool }))
    one)
Tactic: cases X
Cleared hypotheses: X