awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
X Y : C
f g : X ⟶ Y
W : C
ι : W ⟶ X
q : IsSplitEqualizer f g ι
F : Functor.{v, v₂, u, u₂} C D
rw : F.map (g ≫ q.rightRetraction) = 𝟙 (F.obj X)
⊢ F.map g ≫ F.map q.rightRetraction = 𝟙 (F.obj X)
have rw₁ : F.map (𝟙 X) = 𝟙 (F.obj X)
Tactic: rw [← F.map_comp, q.bottom_rightRetraction, F.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
X Y : C
f g : X ⟶ Y
W : C
ι : W ⟶ X
q : IsSplitEqualizer f g ι
F : Functor.{v, v₂, u, u₂} C D
rw : F.map (g ≫ q.rightRetraction) = 𝟙 (F.obj X)
rw₁ : F.map (𝟙 X) = 𝟙 (F.obj X)
⊢ F.map g ≫ F.map q.rightRetraction = 𝟙 (F.obj X)
have rw₂ : Eq.{v₂ + 1} (α := F.obj X ⟶ F.obj X) (𝟙 (F.obj X)) (𝟙 (F.obj X))
Tactic: rw [← F.map_comp, q.bottom_rightRetraction, F.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
X Y : C
f g : X ⟶ Y
W : C
ι : W ⟶ X
q : IsSplitEqualizer f g ι
F : Functor.{v, v₂, u, u₂} C D
⊢ F.map f ≫ F.map q.rightRetraction = F.map q.leftRetraction ≫ F.map ι
have rw : F.map (f ≫ q.rightRetraction) = F.map q.leftRetraction ≫ F.map ι
Tactic: rw [← F.map_comp, q.top_rightRetraction, F.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
X Y : C
f g : X ⟶ Y
W : C
ι : W ⟶ X
q : IsSplitEqualizer f g ι
F : Functor.{v, v₂, u, u₂} C D
rw : F.map (f ≫ q.rightRetraction) = F.map q.leftRetraction ≫ F.map ι
⊢ F.map f ≫ F.map q.rightRetraction = F.map q.leftRetraction ≫ F.map ι
have rw₁ : F.map (q.leftRetraction ≫ ι) = F.map q.leftRetraction ≫ F.map ι
Tactic: rw [← F.map_comp, q.top_rightRetraction, F.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
X Y : C
f g : X ⟶ Y
W : C
ι : W ⟶ X
q : IsSplitEqualizer f g ι
F : Functor.{v, v₂, u, u₂} C D
rw : F.map (f ≫ q.rightRetraction) = F.map q.leftRetraction ≫ F.map ι
rw₁ : F.map (q.leftRetraction ≫ ι) = F.map q.leftRetraction ≫ F.map ι
⊢ F.map f ≫ F.map q.rightRetraction = F.map q.leftRetraction ≫ F.map ι
have rw₂ : F.map q.leftRetraction ≫ F.map ι = F.map q.leftRetraction ≫ F.map ι
Tactic: rw [← F.map_comp, q.top_rightRetraction, F.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.StrictInitial (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictInitialObjects.{v, u} C
I : C
hI : IsInitial.{v, u} I
A : C
f g : A ⟶ I
⊢ f = g
have this : IsIso f
Tactic: haveI := hI.isIso_to f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.StrictInitial (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictInitialObjects.{v, u} C
I : C
hI : IsInitial.{v, u} I
A : C
f g : A ⟶ I
this : IsIso f
⊢ f = g
have this₁ : IsIso g
Tactic: haveI := hI.isIso_to g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.StrictInitial (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictInitialObjects.{v, u} C
I X : C
inst_2 : HasBinaryProduct.{v, u} X I
hI : IsInitial.{v, u} I
⊢ prod.{v, u} X I ≅ I
have this : IsIso.{v, u} (C := C) (X := prod.{v, u} X I) prod.snd
Tactic: have := hI.isIso_to (prod.snd : X ⨯ I ⟶ I)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.StrictInitial (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictInitialObjects.{v, u} C
I X : C
inst_2 : HasBinaryProduct.{v, u} I X
hI : IsInitial.{v, u} I
⊢ prod.{v, u} I X ≅ I
have this : IsIso.{v, u} (C := C) (X := prod.{v, u} I X) prod.fst
Tactic: have := hI.isIso_to (prod.fst : I ⨯ X ⟶ I)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.StrictInitial (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
h : ∀ (A : C) (f : A ⟶ initial.{v, u} C), IsIso f
I A : C
f : A ⟶ I
hI : IsInitial.{v, u} I
this : IsIso (Y := initial.{v, u} C) (f ≫ hI.to (initial.{v, u} C))
⊢ f ≫ CategoryStruct.comp (Y := initial.{v, u} C) (hI.to (initial.{v, u} C)) (inv (f ≫ hI.to (initial.{v, u} C))) = 𝟙 A
have rw : CategoryStruct.comp (Y := initial.{v, u} C) (f ≫ hI.to (initial.{v, u} C)) (inv (f ≫ hI.to (initial.{v, u} C))) = 𝟙 A
Tactic: rw [← assoc, IsIso.hom_inv_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.StrictInitial (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
h : ∀ (A : C) (f : A ⟶ initial.{v, u} C), IsIso f
I A : C
f : A ⟶ I
hI : IsInitial.{v, u} I
this : IsIso (Y := initial.{v, u} C) (f ≫ hI.to (initial.{v, u} C))
rw :
  CategoryStruct.comp (Y := initial.{v, u} C) (f ≫ hI.to (initial.{v, u} C)) (inv (f ≫ hI.to (initial.{v, u} C))) = 𝟙 A
⊢ f ≫ CategoryStruct.comp (Y := initial.{v, u} C) (hI.to (initial.{v, u} C)) (inv (f ≫ hI.to (initial.{v, u} C))) = 𝟙 A
have rw₁ : Eq.{v + 1} (α := A ⟶ A) (𝟙 A) (𝟙 A)
Tactic: rw [← assoc, IsIso.hom_inv_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.StrictInitial (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictTerminalObjects.{v, u} C
I : C
hI : IsTerminal.{v, u} I
A : C
f g : I ⟶ A
⊢ f = g
have this : IsIso f
Tactic: haveI := hI.isIso_from f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.StrictInitial (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictTerminalObjects.{v, u} C
I : C
hI : IsTerminal.{v, u} I
A : C
f g : I ⟶ A
this : IsIso f
⊢ f = g
have this₁ : IsIso g
Tactic: haveI := hI.isIso_from g
-- 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: refine ⟨⟨limit.lift _ ⟨_, ⟨?_, ?_⟩⟩, ?_, ?_⟩⟩
-- 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: refine ⟨⟨limit.lift _ ⟨_, ⟨?_, ?_⟩⟩, ?_, ?_⟩⟩
-- 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: refine ⟨⟨limit.lift _ ⟨_, ⟨?_, ?_⟩⟩, ?_, ?_⟩⟩
-- 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: refine ⟨⟨limit.lift _ ⟨_, ⟨?_, ?_⟩⟩, ?_, ?_⟩⟩
-- 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
⊢ Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j = F.obj j
have refl : Functor.obj (Functor.obj (Functor.const J) (F.1 i)) i = F.obj 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)
j k : J
f : j ⟶ k
⊢ Eq (α := Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j ⟶ F.obj k)
    (Functor.map (Functor.obj (Functor.const J) (F.1 i)) f ≫
      if h : k = i then eqToHom ⋯ else (H k h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) k))
    ((if h : j = i then eqToHom ⋯ else (H j h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j)) ≫ F.map f)
have pos : ∀ (h : k = i) (h_1 : j = i),
  Eq (α := Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j ⟶ F.obj k)
    (Functor.map (Functor.obj (Functor.const J) (F.1 i)) f ≫ eqToHom sorry) (eqToHom sorry ≫ F.map f)
Tactic: split_ifs with h h_1 h_1
-- 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 k : J
f : j ⟶ k
pos :
  ∀ (h : k = i) (h_1 : j = i),
    Eq (α := Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j ⟶ F.obj k)
      (Functor.map (Functor.obj (Functor.const J) (F.1 i)) f ≫ eqToHom ⋯) (eqToHom ⋯ ≫ F.map f)
⊢ Eq (α := Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j ⟶ F.obj k)
    (Functor.map (Functor.obj (Functor.const J) (F.1 i)) f ≫
      if h : k = i then eqToHom ⋯ else (H k h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) k))
    ((if h : j = i then eqToHom ⋯ else (H j h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j)) ≫ F.map f)
have neg : ∀ (h : k = i) (h_1 : ¬j = i),
  Eq (α := Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j ⟶ F.obj k)
    (Functor.map (Functor.obj (Functor.const J) (F.1 i)) f ≫ eqToHom sorry)
    ((H j h_1).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j) ≫ F.map f)
Tactic: split_ifs with h h_1 h_1
-- 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 k : J
f : j ⟶ k
pos :
  ∀ (h : k = i) (h_1 : j = i),
    Eq (α := Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j ⟶ F.obj k)
      (Functor.map (Functor.obj (Functor.const J) (F.1 i)) f ≫ eqToHom ⋯) (eqToHom ⋯ ≫ F.map f)
neg :
  ∀ (h : k = i) (h_1 : ¬j = i),
    Eq (α := Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j ⟶ F.obj k)
      (Functor.map (Functor.obj (Functor.const J) (F.1 i)) f ≫ eqToHom ⋯)
      ((H j h_1).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j) ≫ F.map f)
⊢ Eq (α := Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j ⟶ F.obj k)
    (Functor.map (Functor.obj (Functor.const J) (F.1 i)) f ≫
      if h : k = i then eqToHom ⋯ else (H k h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) k))
    ((if h : j = i then eqToHom ⋯ else (H j h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j)) ≫ F.map f)
have pos₁ : ∀ (h : ¬k = i) (h_1 : j = i),
  Eq (α := Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j ⟶ F.obj k)
    (Functor.map (Functor.obj (Functor.const J) (F.1 i)) f ≫
      (H k h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) k))
    (eqToHom sorry ≫ F.map f)
Tactic: split_ifs with h h_1 h_1
-- 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 k : J
f : j ⟶ k
pos :
  ∀ (h : k = i) (h_1 : j = i),
    Eq (α := Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j ⟶ F.obj k)
      (Functor.map (Functor.obj (Functor.const J) (F.1 i)) f ≫ eqToHom ⋯) (eqToHom ⋯ ≫ F.map f)
neg :
  ∀ (h : k = i) (h_1 : ¬j = i),
    Eq (α := Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j ⟶ F.obj k)
      (Functor.map (Functor.obj (Functor.const J) (F.1 i)) f ≫ eqToHom ⋯)
      ((H j h_1).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j) ≫ F.map f)
pos₁ :
  ∀ (h : ¬k = i) (h_1 : j = i),
    Eq (α := Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j ⟶ F.obj k)
      (Functor.map (Functor.obj (Functor.const J) (F.1 i)) f ≫
        (H k h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) k))
      (eqToHom ⋯ ≫ F.map f)
⊢ Eq (α := Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j ⟶ F.obj k)
    (Functor.map (Functor.obj (Functor.const J) (F.1 i)) f ≫
      if h : k = i then eqToHom ⋯ else (H k h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) k))
    ((if h : j = i then eqToHom ⋯ else (H j h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j)) ≫ F.map f)
have neg₁ : ∀ (h : ¬k = i) (h_1 : ¬j = i),
  Eq (α := Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j ⟶ F.obj k)
    (Functor.map (Functor.obj (Functor.const J) (F.1 i)) f ≫
      (H k h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) k))
    ((H j h_1).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j) ≫ F.map f)
Tactic: split_ifs with h h_1 h_1
-- 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 k : J
f : j ⟶ k
h : k = i
h_1 : j = i
⊢ Eq (α := Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j ⟶ F.obj k)
    (Functor.map (Functor.obj (Functor.const J) (F.1 i)) f ≫ eqToHom ⋯) (eqToHom ⋯ ≫ F.map f)
have pos : ∀ (f : j ⟶ i),
  Eq (α := Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j ⟶ F.obj i)
    (Functor.map (Functor.obj (Functor.const J) (F.1 i)) f ≫ eqToHom sorry) (eqToHom sorry ≫ F.map f)
Tactic: cases h
Cleared hypotheses: k, f, 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_1 : j = i
f : j ⟶ i
⊢ Eq (α := Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j ⟶ F.obj i)
    (Functor.map (Functor.obj (Functor.const J) (F.1 i)) f ≫ eqToHom ⋯) (eqToHom ⋯ ≫ F.map f)
have pos : ∀ (f : i ⟶ i),
  Eq (α := Functor.obj (Functor.obj (Functor.const J) (F.1 i)) i ⟶ F.obj i)
    (Functor.map (Functor.obj (Functor.const J) (F.1 i)) f ≫ eqToHom sorry) (eqToHom sorry ≫ F.map f)
Tactic: cases h_1
Cleared hypotheses: j, h_1, f
-- 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)
f : i ⟶ i
⊢ Eq (α := Functor.obj (Functor.obj (Functor.const J) (F.1 i)) i ⟶ F.obj i)
    (Functor.map (Functor.obj (Functor.const J) (F.1 i)) f ≫ eqToHom ⋯) (eqToHom ⋯ ≫ F.map f)
have pos : Eq (α := Functor.obj (Functor.obj (Functor.const J) (F.1 i)) i ⟶ F.obj i)
  (Functor.map (Functor.obj (Functor.const J) (F.1 i)) (𝟙 i) ≫ eqToHom sorry) (eqToHom sorry ≫ F.map (𝟙 i))
Tactic: obtain rfl : f = 𝟙 _ := Subsingleton.elim _ _
Cleared hypotheses: f
-- 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 k : J
f : j ⟶ k
h : k = i
h_1 : ¬j = i
⊢ Eq (α := Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j ⟶ F.obj k)
    (Functor.map (Functor.obj (Functor.const J) (F.1 i)) f ≫ eqToHom ⋯)
    ((H j h_1).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j) ≫ F.map f)
have neg : ∀ (f : j ⟶ i),
  Eq (α := Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j ⟶ F.obj i)
    (Functor.map (Functor.obj (Functor.const J) (F.1 i)) f ≫ eqToHom sorry)
    ((H j h_1).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j) ≫ F.map f)
Tactic: cases h
Cleared hypotheses: k, f, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.StrictInitial (hypothesis)
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_1 : ¬j = i
f : j ⟶ i
⊢ Eq (α := Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j ⟶ F.obj i)
    (Functor.map (Functor.obj (Functor.const J) (F.1 i)) f ≫ eqToHom ⋯)
    ((H j h_1).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j) ≫ F.map f)
have this : IsIso (F.map f)
Tactic: haveI : IsIso (F.map f) := (H _ h_1).isIso_from _
-- 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_1 : ¬j = i
f : j ⟶ i
this : IsIso (F.map f)
⊢ Eq (α := Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j ⟶ F.obj i)
    (Functor.map (Functor.obj (Functor.const J) (F.1 i)) f ≫ eqToHom ⋯)
    ((H j h_1).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j) ≫ F.map f)
have neg : Eq (α := Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j ⟶ F.obj j)
  ((Functor.map (Functor.obj (Functor.const J) (F.1 i)) f ≫ eqToHom sorry) ≫ inv (F.map f))
  ((H j h_1).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j))
Tactic: rw [← IsIso.comp_inv_eq]
-- 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 k : J
f : j ⟶ k
h : ¬k = i
h_1 : j = i
⊢ Eq (α := Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j ⟶ F.obj k)
    (Functor.map (Functor.obj (Functor.const J) (F.1 i)) f ≫
      (H k h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) k))
    (eqToHom ⋯ ≫ F.map f)
have pos : ∀ (f : i ⟶ k),
  Eq (α := Functor.obj (Functor.obj (Functor.const J) (F.1 i)) i ⟶ F.obj k)
    (Functor.map (Functor.obj (Functor.const J) (F.1 i)) f ≫
      (H k h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) k))
    (eqToHom sorry ≫ F.map f)
Tactic: cases h_1
Cleared hypotheses: j, f, h_1
-- 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 ≫
      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)
have refine_3 : ∀ (j : J),
  CategoryStruct.comp (Y := limit F)
      (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 j) =
    𝟙 (limit F) ≫ limit.π F j
Tactic: ext
-- 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
⊢ CategoryStruct.comp (Y := limit F)
      (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 j) =
    𝟙 (limit F) ≫ limit.π F j
have refine_3 : limit.π F i ≫
    NatTrans.app
      (Cone.π
        { 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 } })
      j =
  𝟙 (limit F) ≫ limit.π F j
Tactic: rw [assoc, limit.lift_π]