awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Pullbacks (goal)
Goal:
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst : HasLimit.{0, 0, v, u} (pair X Y)
inst_1 : HasLimit (parallelPair (X := prod.{v, u} X Y) (prod.fst ≫ f) (prod.snd ≫ g))
π₁ : prod.{v, u} X Y ⟶ X := prod.fst
π₂ : prod.{v, u} X Y ⟶ Y := prod.snd
e : equalizer (π₁ ≫ f) (π₂ ≫ g) ⟶ prod.{v, u} X Y := equalizer.ι (π₁ ≫ f) (π₂ ≫ g)
⊢ (e ≫ π₁) ≫ f = (e ≫ π₂) ≫ g
have rw : equalizer.ι (π₁ ≫ f) (π₂ ≫ g) ≫ π₂ ≫ g = (e ≫ π₂) ≫ g
Tactic: rw [Category.assoc, equalizer.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Pullbacks (goal)
Goal:
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst : HasLimit.{0, 0, v, u} (pair X Y)
inst_1 : HasLimit (parallelPair (X := prod.{v, u} X Y) (prod.fst ≫ f) (prod.snd ≫ g))
π₁ : prod.{v, u} X Y ⟶ X := prod.fst
π₂ : prod.{v, u} X Y ⟶ Y := prod.snd
e : equalizer (π₁ ≫ f) (π₂ ≫ g) ⟶ prod.{v, u} X Y := equalizer.ι (π₁ ≫ f) (π₂ ≫ g)
s : PullbackCone f g
⊢ prod.lift (s.π.app WalkingCospan.left) (s.π.app WalkingCospan.right) ≫ π₁ ≫ f =
    prod.lift (s.π.app WalkingCospan.left) (s.π.app WalkingCospan.right) ≫ π₂ ≫ g
have rw : Eq (α := s.pt ⟶ Z)
  ((BinaryFan.mk (s.π.app WalkingCospan.left) (s.π.app WalkingCospan.right)).π.app { as := WalkingPair.left } ≫ f :
    s.pt ⟶ Z)
  ((BinaryFan.mk (s.π.app WalkingCospan.left) (s.π.app WalkingCospan.right)).π.app { as := WalkingPair.right } ≫ g :
    s.pt ⟶ Z)
Tactic: rw [← Category.assoc, limit.lift_π, ← Category.assoc, limit.lift_π]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Pullbacks (goal)
Goal:
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst : HasLimit.{0, 0, v, u} (pair X Y)
inst_1 : HasLimit (parallelPair (X := prod.{v, u} X Y) (prod.fst ≫ f) (prod.snd ≫ g))
π₁ : prod.{v, u} X Y ⟶ X := prod.fst
π₂ : prod.{v, u} X Y ⟶ Y := prod.snd
e : equalizer (π₁ ≫ f) (π₂ ≫ g) ⟶ prod.{v, u} X Y := equalizer.ι (π₁ ≫ f) (π₂ ≫ g)
s : PullbackCone f g
m : s.pt ⟶ equalizer (π₁ ≫ f) (π₂ ≫ g)
h₁ : m ≫ e ≫ π₁ = s.fst
h₂ : m ≫ e ≫ π₂ = s.snd
⊢ m =
    (fun (s : PullbackCone f g) ↦
        (equalizer.lift (prod.lift (s.π.app WalkingCospan.left) (s.π.app WalkingCospan.right)) ⋯ :
          s.pt ⟶ equalizer (π₁ ≫ f) (π₂ ≫ g)))
      s
have h : (m ≫ equalizer.ι (π₁ ≫ f) (π₂ ≫ g)) ≫ prod.fst =
  CategoryStruct.comp (Y := equalizer (π₁ ≫ f) (π₂ ≫ g))
      ((fun (s : PullbackCone f g) ↦
          (equalizer.lift (prod.lift (s.π.app WalkingCospan.left) (s.π.app WalkingCospan.right)) sorry :
            s.pt ⟶ equalizer (π₁ ≫ f) (π₂ ≫ g)))
        s)
      (equalizer.ι (π₁ ≫ f) (π₂ ≫ g)) ≫
    prod.fst
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Pullbacks (goal)
Goal:
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst : HasLimit.{0, 0, v, u} (pair X Y)
inst_1 : HasLimit (parallelPair (X := prod.{v, u} X Y) (prod.fst ≫ f) (prod.snd ≫ g))
π₁ : prod.{v, u} X Y ⟶ X := prod.fst
π₂ : prod.{v, u} X Y ⟶ Y := prod.snd
e : equalizer (π₁ ≫ f) (π₂ ≫ g) ⟶ prod.{v, u} X Y := equalizer.ι (π₁ ≫ f) (π₂ ≫ g)
s : PullbackCone f g
m : s.pt ⟶ equalizer (π₁ ≫ f) (π₂ ≫ g)
h₁ : m ≫ e ≫ π₁ = s.fst
h₂ : m ≫ e ≫ π₂ = s.snd
h :
  (m ≫ equalizer.ι (π₁ ≫ f) (π₂ ≫ g)) ≫ prod.fst =
    CategoryStruct.comp (Y := equalizer (π₁ ≫ f) (π₂ ≫ g))
        ((fun (s : PullbackCone f g) ↦
            (equalizer.lift (prod.lift (s.π.app WalkingCospan.left) (s.π.app WalkingCospan.right)) ⋯ :
              s.pt ⟶ equalizer (π₁ ≫ f) (π₂ ≫ g)))
          s)
        (equalizer.ι (π₁ ≫ f) (π₂ ≫ g)) ≫
      prod.fst
⊢ m =
    (fun (s : PullbackCone f g) ↦
        (equalizer.lift (prod.lift (s.π.app WalkingCospan.left) (s.π.app WalkingCospan.right)) ⋯ :
          s.pt ⟶ equalizer (π₁ ≫ f) (π₂ ≫ g)))
      s
have h₃ : (m ≫ equalizer.ι (π₁ ≫ f) (π₂ ≫ g)) ≫ prod.snd =
  CategoryStruct.comp (Y := equalizer (π₁ ≫ f) (π₂ ≫ g))
      ((fun (s : PullbackCone f g) ↦
          (equalizer.lift (prod.lift (s.π.app WalkingCospan.left) (s.π.app WalkingCospan.right)) sorry :
            s.pt ⟶ equalizer (π₁ ≫ f) (π₂ ≫ g)))
        s)
      (equalizer.ι (π₁ ≫ f) (π₂ ≫ g)) ≫
    prod.snd
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Pullbacks (goal)
Goal:
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst : HasColimit.{0, 0, v, u} (pair Y Z)
inst_1 : HasColimit (parallelPair (Y := coprod.{v, u} Y Z) (f ≫ coprod.inl) (g ≫ coprod.inr))
ι₁ : Y ⟶ coprod.{v, u} Y Z := coprod.inl
ι₂ : Z ⟶ coprod.{v, u} Y Z := coprod.inr
c : coprod.{v, u} Y Z ⟶ coequalizer (f ≫ ι₁) (g ≫ ι₂) := coequalizer.π (f ≫ ι₁) (g ≫ ι₂)
⊢ f ≫ ι₁ ≫ c = g ≫ ι₂ ≫ c
have rw : (f ≫ ι₁) ≫ c = g ≫ ι₂ ≫ c
Tactic: rw [← Category.assoc, ← Category.assoc, coequalizer.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Pullbacks (goal)
Goal:
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst : HasColimit.{0, 0, v, u} (pair Y Z)
inst_1 : HasColimit (parallelPair (Y := coprod.{v, u} Y Z) (f ≫ coprod.inl) (g ≫ coprod.inr))
ι₁ : Y ⟶ coprod.{v, u} Y Z := coprod.inl
ι₂ : Z ⟶ coprod.{v, u} Y Z := coprod.inr
c : coprod.{v, u} Y Z ⟶ coequalizer (f ≫ ι₁) (g ≫ ι₂) := coequalizer.π (f ≫ ι₁) (g ≫ ι₂)
rw : (f ≫ ι₁) ≫ c = g ≫ ι₂ ≫ c
⊢ f ≫ ι₁ ≫ c = g ≫ ι₂ ≫ c
have rw₁ : (f ≫ ι₁) ≫ c = (g ≫ ι₂) ≫ c
Tactic: rw [← Category.assoc, ← Category.assoc, coequalizer.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Pullbacks (goal)
Goal:
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst : HasColimit.{0, 0, v, u} (pair Y Z)
inst_1 : HasColimit (parallelPair (Y := coprod.{v, u} Y Z) (f ≫ coprod.inl) (g ≫ coprod.inr))
ι₁ : Y ⟶ coprod.{v, u} Y Z := coprod.inl
ι₂ : Z ⟶ coprod.{v, u} Y Z := coprod.inr
c : coprod.{v, u} Y Z ⟶ coequalizer (f ≫ ι₁) (g ≫ ι₂) := coequalizer.π (f ≫ ι₁) (g ≫ ι₂)
rw : (f ≫ ι₁) ≫ c = g ≫ ι₂ ≫ c
rw₁ : (f ≫ ι₁) ≫ c = (g ≫ ι₂) ≫ c
⊢ f ≫ ι₁ ≫ c = g ≫ ι₂ ≫ c
have rw₂ : (g ≫ ι₂) ≫ coequalizer.π (f ≫ ι₁) (g ≫ ι₂) = (g ≫ ι₂) ≫ c
Tactic: rw [← Category.assoc, ← Category.assoc, coequalizer.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Pullbacks (goal)
Goal:
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst : HasColimit.{0, 0, v, u} (pair Y Z)
inst_1 : HasColimit (parallelPair (Y := coprod.{v, u} Y Z) (f ≫ coprod.inl) (g ≫ coprod.inr))
ι₁ : Y ⟶ coprod.{v, u} Y Z := coprod.inl
ι₂ : Z ⟶ coprod.{v, u} Y Z := coprod.inr
c : coprod.{v, u} Y Z ⟶ coequalizer (f ≫ ι₁) (g ≫ ι₂) := coequalizer.π (f ≫ ι₁) (g ≫ ι₂)
s : PushoutCocone f g
⊢ (f ≫ ι₁) ≫ coprod.desc (s.ι.app WalkingSpan.left) (s.ι.app WalkingSpan.right) =
    (g ≫ ι₂) ≫ coprod.desc (s.ι.app WalkingSpan.left) (s.ι.app WalkingSpan.right)
have rw : Eq (α := X ⟶ s.pt)
  (f ≫ (BinaryCofan.mk (s.ι.app WalkingSpan.left) (s.ι.app WalkingSpan.right)).ι.app { as := WalkingPair.left })
  (g ≫ (BinaryCofan.mk (s.ι.app WalkingSpan.left) (s.ι.app WalkingSpan.right)).ι.app { as := WalkingPair.right })
Tactic: rw [Category.assoc, colimit.ι_desc, Category.assoc, colimit.ι_desc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Pullbacks (goal)
Goal:
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst : HasColimit.{0, 0, v, u} (pair Y Z)
inst_1 : HasColimit (parallelPair (Y := coprod.{v, u} Y Z) (f ≫ coprod.inl) (g ≫ coprod.inr))
ι₁ : Y ⟶ coprod.{v, u} Y Z := coprod.inl
ι₂ : Z ⟶ coprod.{v, u} Y Z := coprod.inr
c : coprod.{v, u} Y Z ⟶ coequalizer (f ≫ ι₁) (g ≫ ι₂) := coequalizer.π (f ≫ ι₁) (g ≫ ι₂)
s : PushoutCocone f g
m : coequalizer (f ≫ ι₁) (g ≫ ι₂) ⟶ s.pt
h₁ : (ι₁ ≫ c) ≫ m = s.inl
h₂ : (ι₂ ≫ c) ≫ m = s.inr
⊢ m =
    (fun (s : PushoutCocone f g) ↦
        (coequalizer.desc (coprod.desc (s.ι.app WalkingSpan.left) (s.ι.app WalkingSpan.right)) ⋯ :
          coequalizer (f ≫ ι₁) (g ≫ ι₂) ⟶ s.pt))
      s
have h : coprod.inl ≫ coequalizer.π (f ≫ ι₁) (g ≫ ι₂) ≫ m =
  coprod.inl ≫
    CategoryStruct.comp (Y := coequalizer (f ≫ ι₁) (g ≫ ι₂)) (coequalizer.π (f ≫ ι₁) (g ≫ ι₂))
      ((fun (s : PushoutCocone f g) ↦
          (coequalizer.desc (coprod.desc (s.ι.app WalkingSpan.left) (s.ι.app WalkingSpan.right)) sorry :
            coequalizer (f ≫ ι₁) (g ≫ ι₂) ⟶ s.pt))
        s)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Pullbacks (goal)
Goal:
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst : HasColimit.{0, 0, v, u} (pair Y Z)
inst_1 : HasColimit (parallelPair (Y := coprod.{v, u} Y Z) (f ≫ coprod.inl) (g ≫ coprod.inr))
ι₁ : Y ⟶ coprod.{v, u} Y Z := coprod.inl
ι₂ : Z ⟶ coprod.{v, u} Y Z := coprod.inr
c : coprod.{v, u} Y Z ⟶ coequalizer (f ≫ ι₁) (g ≫ ι₂) := coequalizer.π (f ≫ ι₁) (g ≫ ι₂)
s : PushoutCocone f g
m : coequalizer (f ≫ ι₁) (g ≫ ι₂) ⟶ s.pt
h₁ : (ι₁ ≫ c) ≫ m = s.inl
h₂ : (ι₂ ≫ c) ≫ m = s.inr
h :
  coprod.inl ≫ coequalizer.π (f ≫ ι₁) (g ≫ ι₂) ≫ m =
    coprod.inl ≫
      CategoryStruct.comp (Y := coequalizer (f ≫ ι₁) (g ≫ ι₂)) (coequalizer.π (f ≫ ι₁) (g ≫ ι₂))
        ((fun (s : PushoutCocone f g) ↦
            (coequalizer.desc (coprod.desc (s.ι.app WalkingSpan.left) (s.ι.app WalkingSpan.right)) ⋯ :
              coequalizer (f ≫ ι₁) (g ≫ ι₂) ⟶ s.pt))
          s)
⊢ m =
    (fun (s : PushoutCocone f g) ↦
        (coequalizer.desc (coprod.desc (s.ι.app WalkingSpan.left) (s.ι.app WalkingSpan.right)) ⋯ :
          coequalizer (f ≫ ι₁) (g ≫ ι₂) ⟶ s.pt))
      s
have h₃ : coprod.inr ≫ coequalizer.π (f ≫ ι₁) (g ≫ ι₂) ≫ m =
  coprod.inr ≫
    CategoryStruct.comp (Y := coequalizer (f ≫ ι₁) (g ≫ ι₂)) (coequalizer.π (f ≫ ι₁) (g ≫ ι₂))
      ((fun (s : PushoutCocone f g) ↦
          (coequalizer.desc (coprod.desc (s.ι.app WalkingSpan.left) (s.ι.app WalkingSpan.right)) sorry :
            coequalizer (f ≫ ι₁) (g ≫ ι₂) ⟶ s.pt))
        s)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.WeaklyInitial (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasWideEqualizers.{v, v, u} C
T : C
hT : ∀ (X : C), Nonempty.{v + 1} (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer.{v, v, u} (J := endos) id ⟶ T := wideEqualizer.ι id
⊢ HasInitial.{v, u} C
have this : Nonempty endos
Tactic: haveI : Nonempty endos := ⟨𝟙 _⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.WeaklyInitial (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasWideEqualizers.{v, v, u} C
T : C
hT : ∀ (X : C), Nonempty.{v + 1} (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer.{v, v, u} (J := endos) id ⟶ T := wideEqualizer.ι id
this : Nonempty endos
X : C
⊢ Unique (wideEqualizer.{v, v, u} (J := endos) id ⟶ X)
have refine : ∀ (a : wideEqualizer.{v, v, u} (J := endos) id ⟶ X), a = default
Tactic: refine ⟨⟨i ≫ Classical.choice (hT X)⟩, fun a => ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.WeaklyInitial (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasWideEqualizers.{v, v, u} C
T : C
hT : ∀ (X : C), Nonempty.{v + 1} (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer.{v, v, u} (J := endos) id ⟶ T := wideEqualizer.ι id
this : Nonempty endos
X : C
a : wideEqualizer.{v, v, u} (J := endos) id ⟶ X
E : C := equalizer a (i ≫ Classical.choice ⋯)
e : E ⟶ wideEqualizer.{v, v, u} (J := T ⟶ T) id := equalizer.ι a (i ≫ Classical.choice ⋯)
h : T ⟶ E := Classical.choice ⋯
⊢ ((i ≫ h) ≫ e) ≫ i = i ≫ 𝟙 T
have rw : i ≫ h ≫ e ≫ i = i ≫ 𝟙 T
Tactic: rw [Category.assoc, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.WeaklyInitial (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasWideEqualizers.{v, v, u} C
T : C
hT : ∀ (X : C), Nonempty.{v + 1} (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer.{v, v, u} (J := endos) id ⟶ T := wideEqualizer.ι id
this : Nonempty endos
X : C
a : wideEqualizer.{v, v, u} (J := endos) id ⟶ X
E : C := equalizer a (i ≫ Classical.choice ⋯)
e : E ⟶ wideEqualizer.{v, v, u} (J := T ⟶ T) id := equalizer.ι a (i ≫ Classical.choice ⋯)
h : T ⟶ E := Classical.choice ⋯
⊢ a = default
have this₁ : ((i ≫ h) ≫ e) ≫ i = i ≫ 𝟙 T
Tactic: have : ((i ≫ h) ≫ e) ≫ i = i ≫ 𝟙 _ := by
      rw [Category.assoc, Category.assoc]
      apply wideEqualizer.condition (id : endos → endos) (h ≫ e ≫ i)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.WeaklyInitial (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasWideEqualizers.{v, v, u} C
T : C
hT : ∀ (X : C), Nonempty.{v + 1} (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer.{v, v, u} (J := endos) id ⟶ T := wideEqualizer.ι id
this_1 : Nonempty endos
X : C
a : wideEqualizer.{v, v, u} (J := endos) id ⟶ X
E : C := equalizer a (i ≫ Classical.choice ⋯)
e : E ⟶ wideEqualizer.{v, v, u} (J := T ⟶ T) id := equalizer.ι a (i ≫ Classical.choice ⋯)
h : T ⟶ E := Classical.choice ⋯
this : ((i ≫ h) ≫ e) ≫ i = i ≫ 𝟙 T
⊢ a = default
have this₁ : (i ≫ h) ≫ e = 𝟙 (wideEqualizer.{v, v, u} (J := endos) id)
Tactic: rw [Category.comp_id, cancel_mono_id i] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.WeaklyInitial (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasWideEqualizers.{v, v, u} C
T : C
hT : ∀ (X : C), Nonempty.{v + 1} (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer.{v, v, u} (J := endos) id ⟶ T := wideEqualizer.ι id
this_1 : Nonempty endos
X : C
a : wideEqualizer.{v, v, u} (J := endos) id ⟶ X
E : C := equalizer a (i ≫ Classical.choice ⋯)
e : E ⟶ wideEqualizer.{v, v, u} (J := T ⟶ T) id := equalizer.ι a (i ≫ Classical.choice ⋯)
h : T ⟶ E := Classical.choice ⋯
this : (i ≫ h) ≫ e = 𝟙 (wideEqualizer.{v, v, u} (J := endos) id)
⊢ a = default
have this₁ : IsSplitEpi e
Tactic: haveI : IsSplitEpi e := IsSplitEpi.mk' ⟨i ≫ h, this⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.WeaklyInitial (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasWideEqualizers.{v, v, u} C
T : C
hT : ∀ (X : C), Nonempty.{v + 1} (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer.{v, v, u} (J := endos) id ⟶ T := wideEqualizer.ι id
this_1 : Nonempty endos
X : C
a : wideEqualizer.{v, v, u} (J := endos) id ⟶ X
E : C := equalizer a (i ≫ Classical.choice ⋯)
e : E ⟶ wideEqualizer.{v, v, u} (J := T ⟶ T) id := equalizer.ι a (i ≫ Classical.choice ⋯)
h : T ⟶ E := Classical.choice ⋯
this_2 : (i ≫ h) ≫ e = 𝟙 (wideEqualizer.{v, v, u} (J := endos) id)
this : IsSplitEpi e
⊢ a = default
have rw : e ≫ a = e ≫ default
Tactic: rw [← cancel_epi e]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.WeaklyInitial (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasWideEqualizers.{v, v, u} C
T : C
hT : ∀ (X : C), Nonempty.{v + 1} (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer.{v, v, u} (J := endos) id ⟶ T := wideEqualizer.ι id
this : Nonempty endos
⊢ HasInitial.{v, u} C
have have : ∀ (this : (X : C) → Unique (wideEqualizer.{v, v, u} (J := endos) id ⟶ X)), HasInitial.{v, u} C
Tactic: have : ∀ X : C, Unique (wideEqualizer (id : endos → endos) ⟶ X) := by
    intro X
    refine ⟨⟨i ≫ Classical.choice (hT X)⟩, fun a => ?_⟩
    let E := equalizer a (i ≫ Classical.choice (hT _))
    let e : E ⟶ wideEqualizer id := equalizer.ι _ _
    let h : T ⟶ E := Classical.choice (hT E)
    have : ((i ≫ h) ≫ e) ≫ i = i ≫ 𝟙 _ := by
      rw [Category.assoc, Category.assoc]
      apply wideEqualizer.condition (id : endos → endos) (h ≫ e ≫ i)
    rw [Category.comp_id, cancel_mono_id i] at this
    haveI : IsSplitEpi e := IsSplitEpi.mk' ⟨i ≫ h, this⟩
    rw [← cancel_epi e]
    apply equalizer.condition
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasZeroMorphisms.{v_1, u_1} C
X : C
⊢ Eq.{v_1 + 1} (α := X ⟶ X)
    (CategoryStruct.comp (Y := prod.{v_1, u_1} 0 X) (Iso.inv (zeroProdIso X) : X ⟶ prod.{v_1, u_1} 0 X)
      (prod.snd : prod.{v_1, u_1} 0 X ⟶ X))
    (𝟙 X)
have dsimp : Eq.{v_1 + 1} (α := X ⟶ X)
  (CategoryStruct.comp (Y := prod.{v_1, u_1} 0 X)
      (Iso.inv (limit.isoLimitCone { cone := BinaryFan.mk 0 (𝟙 X), isLimit := binaryFanZeroLeftIsLimit X })) prod.snd :
    X ⟶ X)
  (𝟙 X : X ⟶ X)
Tactic: dsimp [zeroProdIso, binaryFanZeroLeft]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasZeroMorphisms.{v_1, u_1} C
X : C
⊢ Eq.{v_1 + 1} (α := X ⟶ X)
    (CategoryStruct.comp (Y := prod.{v_1, u_1} X 0) (Iso.inv (prodZeroIso X) : X ⟶ prod.{v_1, u_1} X 0)
      (prod.fst : prod.{v_1, u_1} X 0 ⟶ X))
    (𝟙 X)
have dsimp : Eq.{v_1 + 1} (α := X ⟶ X)
  (CategoryStruct.comp (Y := prod.{v_1, u_1} X 0)
      (Iso.inv (limit.isoLimitCone { cone := BinaryFan.mk (𝟙 X) 0, isLimit := binaryFanZeroRightIsLimit X })) prod.fst :
    X ⟶ X)
  (𝟙 X : X ⟶ X)
Tactic: dsimp [prodZeroIso, binaryFanZeroRight]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasZeroMorphisms.{v_1, u_1} C
X : C
⊢ Eq.{v_1 + 1} (α := X ⟶ X)
    (CategoryStruct.comp (Y := coprod.{v_1, u_1} 0 X) (coprod.inr : X ⟶ coprod.{v_1, u_1} 0 X)
      (Iso.hom (zeroCoprodIso X) : coprod.{v_1, u_1} 0 X ⟶ X))
    (𝟙 X)
have dsimp : Eq.{v_1 + 1} (α := X ⟶ X)
  (CategoryStruct.comp (Y := coprod.{v_1, u_1} 0 X) coprod.inr
      (Iso.hom
        (colimit.isoColimitCocone { cocone := BinaryCofan.mk 0 (𝟙 X), isColimit := binaryCofanZeroLeftIsColimit X })) :
    X ⟶ X)
  (𝟙 X : X ⟶ X)
Tactic: dsimp [zeroCoprodIso, binaryCofanZeroLeft]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasZeroMorphisms.{v_1, u_1} C
X : C
⊢ Eq.{v_1 + 1} (α := X ⟶ X)
    (CategoryStruct.comp (Y := coprod.{v_1, u_1} X 0) (coprod.inl : X ⟶ coprod.{v_1, u_1} X 0)
      (Iso.hom (coprodZeroIso X) : coprod.{v_1, u_1} X 0 ⟶ X))
    (𝟙 X)
have dsimp : Eq.{v_1 + 1} (α := X ⟶ X)
  (CategoryStruct.comp (Y := coprod.{v_1, u_1} X 0) coprod.inl
      (Iso.hom
        (colimit.isoColimitCocone { cocone := BinaryCofan.mk (𝟙 X) 0, isColimit := binaryCofanZeroRightIsColimit X })) :
    X ⟶ X)
  (𝟙 X : X ⟶ X)
Tactic: dsimp [coprodZeroIso, binaryCofanZeroRight]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasZeroMorphisms.{v_1, u_1} C
X Y : C
inst_3 : HasBinaryProduct.{v_1, u_1} X Y
⊢ Eq.{v_1 + 1} (α := prod.{v_1, u_1} X Y ⟶ X)
    (CategoryStruct.comp (Y := pullback.{v_1, u_1} (X := X) (Y := Y) (Z := 0) 0 0) (Iso.inv (pullbackZeroZeroIso X Y))
      (pullback.fst 0 0))
    prod.fst
have dsimp : Eq.{v_1 + 1} (α := prod.{v_1, u_1} X Y ⟶ X)
  (CategoryStruct.comp (Y := pullback.{v_1, u_1} (X := X) (Y := Y) (Z := 0) 0 0)
      (Iso.inv
        (limit.isoLimitCone
          { cone := PullbackCone.mk (W := prod.{v_1, u_1} X Y) prod.fst prod.snd sorry,
            isLimit :=
              (isPullbackOfIsTerminalIsProduct 0 0 prod.fst prod.snd HasZeroObject.zeroIsTerminal (prodIsProd X Y) :
                IsLimit.{0, v_1, 0, u_1} (C := C) (F := cospan (X := X) (Y := Y) (Z := 0) 0 0)
                  (PullbackCone.mk (W := prod.{v_1, u_1} X Y) prod.fst prod.snd sorry)) }))
      (pullback.fst 0 0) :
    prod.{v_1, u_1} X Y ⟶ X)
  (prod.fst : prod.{v_1, u_1} X Y ⟶ X)
Tactic: dsimp [pullbackZeroZeroIso]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasZeroMorphisms.{v_1, u_1} C
X Y : C
inst_3 : HasBinaryProduct.{v_1, u_1} X Y
⊢ Eq.{v_1 + 1} (α := prod.{v_1, u_1} X Y ⟶ Y)
    (CategoryStruct.comp (Y := pullback.{v_1, u_1} (X := X) (Y := Y) (Z := 0) 0 0) (Iso.inv (pullbackZeroZeroIso X Y))
      (pullback.snd 0 0))
    prod.snd
have dsimp : Eq.{v_1 + 1} (α := prod.{v_1, u_1} X Y ⟶ Y)
  (CategoryStruct.comp (Y := pullback.{v_1, u_1} (X := X) (Y := Y) (Z := 0) 0 0)
      (Iso.inv
        (limit.isoLimitCone
          { cone := PullbackCone.mk (W := prod.{v_1, u_1} X Y) prod.fst prod.snd sorry,
            isLimit :=
              (isPullbackOfIsTerminalIsProduct 0 0 prod.fst prod.snd HasZeroObject.zeroIsTerminal (prodIsProd X Y) :
                IsLimit.{0, v_1, 0, u_1} (C := C) (F := cospan (X := X) (Y := Y) (Z := 0) 0 0)
                  (PullbackCone.mk (W := prod.{v_1, u_1} X Y) prod.fst prod.snd sorry)) }))
      (pullback.snd 0 0) :
    prod.{v_1, u_1} X Y ⟶ Y)
  (prod.snd : prod.{v_1, u_1} X Y ⟶ Y)
Tactic: dsimp [pullbackZeroZeroIso]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasZeroMorphisms.{v_1, u_1} C
X Y : C
inst_3 : HasBinaryCoproduct.{v_1, u_1} X Y
⊢ Eq.{v_1 + 1} (α := X ⟶ coprod.{v_1, u_1} X Y)
    (CategoryStruct.comp (Y := pushout.{v_1, u_1} (X := 0) (Y := X) (Z := Y) 0 0) (pushout.inl 0 0)
      (Iso.hom (pushoutZeroZeroIso X Y)))
    coprod.inl
have dsimp : Eq.{v_1 + 1} (α := X ⟶ coprod.{v_1, u_1} X Y)
  (CategoryStruct.comp (Y := pushout.{v_1, u_1} (X := 0) (Y := X) (Z := Y) 0 0) (pushout.inl 0 0)
      (Iso.hom
        (colimit.isoColimitCocone
          { cocone := PushoutCocone.mk (W := coprod.{v_1, u_1} X Y) coprod.inl coprod.inr sorry,
            isColimit :=
              (isPushoutOfIsInitialIsCoproduct coprod.inl coprod.inr 0 0 HasZeroObject.zeroIsInitial
                  (coprodIsCoprod X Y) :
                IsColimit.{0, v_1, 0, u_1} (C := C) (F := span (X := 0) (Y := X) (Z := Y) 0 0)
                  (PushoutCocone.mk (W := coprod.{v_1, u_1} X Y) coprod.inl coprod.inr sorry)) })) :
    X ⟶ coprod.{v_1, u_1} X Y)
  (coprod.inl : X ⟶ coprod.{v_1, u_1} X Y)
Tactic: dsimp [pushoutZeroZeroIso]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasZeroMorphisms.{v_1, u_1} C
X Y : C
inst_3 : HasBinaryCoproduct.{v_1, u_1} X Y
⊢ Eq.{v_1 + 1} (α := Y ⟶ coprod.{v_1, u_1} X Y)
    (CategoryStruct.comp (Y := pushout.{v_1, u_1} (X := 0) (Y := X) (Z := Y) 0 0) (pushout.inr 0 0)
      (Iso.hom (pushoutZeroZeroIso X Y)))
    coprod.inr
have dsimp : Eq.{v_1 + 1} (α := Y ⟶ coprod.{v_1, u_1} X Y)
  (CategoryStruct.comp (Y := pushout.{v_1, u_1} (X := 0) (Y := X) (Z := Y) 0 0) (pushout.inr 0 0)
      (Iso.hom
        (colimit.isoColimitCocone
          { cocone := PushoutCocone.mk (W := coprod.{v_1, u_1} X Y) coprod.inl coprod.inr sorry,
            isColimit :=
              (isPushoutOfIsInitialIsCoproduct coprod.inl coprod.inr 0 0 HasZeroObject.zeroIsInitial
                  (coprodIsCoprod X Y) :
                IsColimit.{0, v_1, 0, u_1} (C := C) (F := span (X := 0) (Y := X) (Z := Y) 0 0)
                  (PushoutCocone.mk (W := coprod.{v_1, u_1} X Y) coprod.inl coprod.inr sorry)) })) :
    Y ⟶ coprod.{v_1, u_1} X Y)
  (coprod.inr : Y ⟶ coprod.{v_1, u_1} X Y)
Tactic: dsimp [pushoutZeroZeroIso]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Creates (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : CreatesLimit K F
c : Cone (K ⋙ F)
t : IsLimit c
j : J
⊢ ConeMorphism.hom (Iso.inv (liftedLimitMapsToOriginal t)) ≫ F.map ((liftLimit t).π.app j) = c.π.app j
have rw : (CategoryStruct.comp (Y := F.mapCone (liftLimit t)) (Iso.inv (liftedLimitMapsToOriginal t))
        (Iso.hom (liftedLimitMapsToOriginal t))).hom ≫
    c.π.app j =
  c.π.app j
Tactic: rw [show F.map ((liftLimit t).π.app j) = (liftedLimitMapsToOriginal t).hom.hom ≫ c.π.app j
    from (by simp), ← Category.assoc, ← Cone.category_comp_hom]