awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Pullbacks
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
rw₂ rw₃ : (g ≫ ι₂) ≫ coequalizer.π (f ≫ ι₁) (g ≫ ι₂) = (g ≫ ι₂) ≫ c
⊢ f ≫ ι₁ ≫ c = g ≫ ι₂ ≫ c

Tactic:
rw [← Category.assoc, ← Category.assoc, coequalizer.condition]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.coequalizer.condition
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Pullbacks
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
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 })
⊢ (f ≫ ι₁) ≫ coprod.desc (s.ι.app WalkingSpan.left) (s.ι.app WalkingSpan.right) =
    (g ≫ ι₂) ≫ coprod.desc (s.ι.app WalkingSpan.left) (s.ι.app WalkingSpan.right)

Tactic:
rw [Category.assoc, colimit.ι_desc, Category.assoc, colimit.ι_desc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.colimit.ι_desc
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Pullbacks
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
⊢ 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:
PushoutCocone.condition _

Premises used: CategoryTheory.Limits.PushoutCocone.condition
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Pullbacks
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
⊢ 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:
exact PushoutCocone.condition _

Premises used: CategoryTheory.Limits.PushoutCocone.condition
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Pullbacks
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),
    (ι₁ ≫ c) ≫
        (fun (s : PushoutCocone f g) ↦
            (coequalizer.desc (coprod.desc (s.ι.app WalkingSpan.left) (s.ι.app WalkingSpan.right)) ⋯ :
              coequalizer (f ≫ ι₁) (g ≫ ι₂) ⟶ s.pt))
          s =
      s.inl

Tactic:
simp [ι₁, c]
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Pullbacks
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),
    (ι₂ ≫ c) ≫
        (fun (s : PushoutCocone f g) ↦
            (coequalizer.desc (coprod.desc (s.ι.app WalkingSpan.left) (s.ι.app WalkingSpan.right)) ⋯ :
              coequalizer (f ≫ ι₁) (g ≫ ι₂) ⟶ s.pt))
          s =
      s.inr

Tactic:
simp [ι₂, c]
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Pullbacks
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)
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)) ⋯ :
              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

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Pullbacks
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
⊢ 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)

Tactic:
simpa using h₁
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Pullbacks
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
⊢ 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)) ⋯ :
              coequalizer (f ≫ ι₁) (g ≫ ι₂) ⟶ s.pt))
          s)

Tactic:
simpa using h₂
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Pullbacks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasBinaryCoproducts.{v, u} C
inst_2 : HasCoequalizers.{v, u} C
⊢ HasPushouts.{v, u} C

Tactic:
hasPushouts_of_hasColimit_span C

Premises used: CategoryTheory.Limits.hasPushouts_of_hasColimit_span
-- Module: Mathlib.CategoryTheory.Limits.Constructions.WeaklyInitial
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{v, v, u} C
ι : Type v
B : ι → C
hB : ∀ (A : C), ∃ (i : ι), Nonempty.{v + 1} (B i ⟶ A)
⊢ ∃ (T : C), ∀ (X : C), Nonempty.{v + 1} (T ⟶ X)

Tactic:
⟨∏ᶜ B, fun X => ⟨Pi.π _ _ ≫ (hB X).choose_spec.some⟩⟩

Premises used: Exists.choose_spec, CategoryTheory.Limits.Pi.π, Nonempty.some, Nonempty.intro, CategoryTheory.Limits.piObj, Exists.intro, CategoryTheory.CategoryStruct.comp, Exists.choose
-- Module: Mathlib.CategoryTheory.Limits.Constructions.WeaklyInitial
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
⊢ Nonempty endos

Tactic:
haveI : Nonempty endos := ⟨𝟙 _⟩
-- Module: Mathlib.CategoryTheory.Limits.Constructions.WeaklyInitial
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
refine : ∀ (a : wideEqualizer.{v, v, u} (J := endos) id ⟶ X), a = default
⊢ Unique (wideEqualizer.{v, v, u} (J := endos) id ⟶ X)

Tactic:
refine ⟨⟨i ≫ Classical.choice (hT X)⟩, fun a => ?_⟩
-- Module: Mathlib.CategoryTheory.Limits.Constructions.WeaklyInitial
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 ⋯
rw : i ≫ h ≫ e ≫ i = i ≫ 𝟙 T
⊢ ((i ≫ h) ≫ e) ≫ i = i ≫ 𝟙 T

Tactic:
rw [Category.assoc, Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Limits.Constructions.WeaklyInitial
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

Tactic:
apply wideEqualizer.condition (id : endos → endos) (h ≫ e ≫ i)

Premises used: id, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.wideEqualizer.condition
-- Module: Mathlib.CategoryTheory.Limits.Constructions.WeaklyInitial
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

Tactic:
have : ((i ≫ h) ≫ e) ≫ i = i ≫ 𝟙 _ := by
      rw [Category.assoc, Category.assoc]
      apply wideEqualizer.condition (id : endos → endos) (h ≫ e ≫ i)
-- Module: Mathlib.CategoryTheory.Limits.Constructions.WeaklyInitial
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
⊢ (i ≫ h) ≫ e = 𝟙 (wideEqualizer.{v, v, u} (J := endos) id)

Tactic:
rw [Category.comp_id, cancel_mono_id i] at this

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.cancel_mono_id
-- Module: Mathlib.CategoryTheory.Limits.Constructions.WeaklyInitial
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)
⊢ IsSplitEpi e

Tactic:
haveI : IsSplitEpi e := IsSplitEpi.mk' ⟨i ≫ h, this⟩
-- Module: Mathlib.CategoryTheory.Limits.Constructions.WeaklyInitial
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
rw : e ≫ a = e ≫ default
⊢ a = default

Tactic:
rw [← cancel_epi e]

Premises used: CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Limits.Constructions.WeaklyInitial
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
⊢ e ≫ a = e ≫ default

Tactic:
apply equalizer.condition

Premises used: CategoryTheory.Limits.equalizer.condition
-- Module: Mathlib.CategoryTheory.Limits.Constructions.WeaklyInitial
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
have : ∀ (this : (X : C) → Unique (wideEqualizer.{v, v, u} (J := endos) id ⟶ X)), HasInitial.{v, u} C
⊢ 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
-- Module: Mathlib.CategoryTheory.Limits.Constructions.WeaklyInitial
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
this : (X : C) → Unique (wideEqualizer.{v, v, u} (J := endos) id ⟶ X)
⊢ HasInitial.{v, u} C

Tactic:
hasInitial_of_unique (wideEqualizer (id : endos → endos))

Premises used: CategoryTheory.Limits.hasInitial_of_unique, id, CategoryTheory.Limits.wideEqualizer
-- Module: Mathlib.CategoryTheory.Limits.Constructions.WeaklyInitial
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
this : (X : C) → Unique (wideEqualizer.{v, v, u} (J := endos) id ⟶ X)
⊢ HasInitial.{v, u} C

Tactic:
exact hasInitial_of_unique (wideEqualizer (id : endos → endos))

Premises used: CategoryTheory.Limits.hasInitial_of_unique, id, CategoryTheory.Limits.wideEqualizer
-- Module: Mathlib.CategoryTheory.Limits.Constructions.WidePullbackOfTerminal
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type w
B : C
objs : ι → C
arrows : (j : ι) → objs j ⟶ B
c : Fan.{w, v, u} objs
hc : IsLimit c
hB : IsTerminal.{v, u} B
s : WidePullbackCone arrows
m : s.pt ⟶ (ofFan arrows c hB).pt
h : m ≫ (ofFan arrows c hB).base = s.base
hm : ∀ (i : ι), m ≫ (ofFan arrows c hB).π i = s.π i
x : Discrete ι
i : ι
⊢ Eq (α := s.pt ⟶ Functor.obj.{w, v, w, u} (Discrete.functor objs) { as := i : Discrete ι }) (m ≫ c.π.app { as := i })
    ((fun (s : WidePullbackCone arrows) ↦ (hc.lift (toFan arrows s) : (toFan arrows s).pt ⟶ c.pt)) s ≫
      c.π.app { as := i : Discrete ι })

Tactic:
simpa using hm i
-- Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
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
⊢ ∀ (s : BinaryFan.{v_1, u_1} 0 X), (fun (s : BinaryFan.{v_1, u_1} 0 X) ↦ s.snd) s ≫ 𝟙 X = s.snd

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
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
s : BinaryFan.{v_1, u_1} 0 X
m : s.pt ⟶ X
h : m ≫ 0 = s.fst
h₂ : m ≫ 𝟙 X = s.snd
⊢ m = (fun (s : BinaryFan.{v_1, u_1} 0 X) ↦ s.snd) s

Tactic:
simpa using h₂
-- Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
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
⊢ HasBinaryProduct.{v_1, u_1} 0 X

Tactic:
HasLimit.mk ⟨_, binaryFanZeroLeftIsLimit X⟩

Premises used: CategoryTheory.Limits.binaryFanZeroLeftIsLimit, CategoryTheory.Limits.HasLimit.mk, CategoryTheory.Limits.LimitCone.mk
-- Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
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} (α := prod.{v_1, u_1} 0 X ⟶ X) (Iso.hom (zeroProdIso X) : prod.{v_1, u_1} 0 X ⟶ X)
    (prod.snd : prod.{v_1, u_1} 0 X ⟶ X)

Tactic:
rfl

Premises used: CategoryTheory.Limits.limit.π, rfl
-- Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
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
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)
⊢ 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)

Tactic:
dsimp [zeroProdIso, binaryFanZeroLeft]

Premises used: CategoryTheory.Limits.zeroProdIso, CategoryTheory.Limits.binaryFanZeroLeft
-- Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
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 (limit.isoLimitCone { cone := BinaryFan.mk 0 (𝟙 X), isLimit := binaryFanZeroLeftIsLimit X }))
        prod.snd :
      X ⟶ X)
    (𝟙 X : X ⟶ X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
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
⊢ ∀ (s : BinaryFan.{v_1, u_1} X 0), (fun (s : BinaryFan.{v_1, u_1} X 0) ↦ s.fst) s ≫ 𝟙 X = s.fst

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
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
s : BinaryFan.{v_1, u_1} X 0
m : s.pt ⟶ X
h₁ : m ≫ 𝟙 X = s.fst
h : m ≫ 0 = s.snd
⊢ m = (fun (s : BinaryFan.{v_1, u_1} X 0) ↦ s.fst) s

Tactic:
simpa using h₁
-- Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
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
⊢ HasBinaryProduct.{v_1, u_1} X 0

Tactic:
HasLimit.mk ⟨_, binaryFanZeroRightIsLimit X⟩

Premises used: CategoryTheory.Limits.HasLimit.mk, CategoryTheory.Limits.LimitCone.mk, CategoryTheory.Limits.binaryFanZeroRightIsLimit
-- Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
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} (α := prod.{v_1, u_1} X 0 ⟶ X) (Iso.hom (prodZeroIso X) : prod.{v_1, u_1} X 0 ⟶ X)
    (prod.fst : prod.{v_1, u_1} X 0 ⟶ X)

Tactic:
rfl

Premises used: CategoryTheory.Limits.limit.π, rfl
-- Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
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
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)
⊢ 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)

Tactic:
dsimp [prodZeroIso, binaryFanZeroRight]

Premises used: CategoryTheory.Limits.prodZeroIso, CategoryTheory.Limits.binaryFanZeroRight
-- Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
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 (limit.isoLimitCone { cone := BinaryFan.mk (𝟙 X) 0, isLimit := binaryFanZeroRightIsLimit X }))
        prod.fst :
      X ⟶ X)
    (𝟙 X : X ⟶ X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
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
⊢ ∀ (s : BinaryCofan.{v_1, u_1} 0 X), 𝟙 X ≫ (fun (s : BinaryCofan.{v_1, u_1} 0 X) ↦ s.inr) s = s.inr

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
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
s : BinaryCofan.{v_1, u_1} 0 X
m : X ⟶ s.pt
h : 0 ≫ m = s.inl
h₂ : 𝟙 X ≫ m = s.inr
⊢ m = (fun (s : BinaryCofan.{v_1, u_1} 0 X) ↦ s.inr) s

Tactic:
simpa using h₂