awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
β γ : Type
inst_2 : Finite β
ε : β ≃ γ
f : γ → C
inst_3 : HasBiproduct.{0, v, u} f
inst_4 : HasBiproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ))
intro :
  ∀ (val : Fintype β),
    Eq.{v + 1} (α := biproduct.{0, v, u} f ⟶ biproduct.{0, v, u} f)
      (CategoryStruct.comp (Y := biproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ)))
        (lift fun (b : β) ↦ π f ((ε : (a : β) → γ) b)) (desc fun (b : β) ↦ ι f ((ε : (a : β) → γ) b)))
      (𝟙 (biproduct.{0, v, u} f))
⊢ Eq.{v + 1} (α := biproduct.{0, v, u} f ⟶ biproduct.{0, v, u} f)
    (CategoryStruct.comp (Y := biproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ)))
      (lift fun (b : β) ↦ π f ((ε : (a : β) → γ) b)) (desc fun (b : β) ↦ ι f ((ε : (a : β) → γ) b)))
    (𝟙 (biproduct.{0, v, u} f))
have intro₁ : ∀ (val : Fintype β) (g g' : γ),
  CategoryStruct.comp (Y := biproduct.{0, v, u} f) (ι f g')
      (CategoryStruct.comp (Y := biproduct.{0, v, u} f)
        (CategoryStruct.comp (Y := biproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ)))
          (lift fun (b : β) ↦ π f ((ε : (a : β) → γ) b)) (desc fun (b : β) ↦ ι f ((ε : (a : β) → γ) b)))
        (π f g)) =
    ι f g' ≫ 𝟙 (biproduct.{0, v, u} f) ≫ π f g
Tactic: classical
    cases nonempty_fintype β
    ext g g'
    by_cases h : g' = g <;>
      simp [Preadditive.sum_comp, biproduct.lift_desc, biproduct.ι_π, comp_dite,
        Equiv.apply_eq_iff_eq_symm_apply, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
b : BinaryBicone.{v, u} X Y
total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.pt
s : Cone.{0, v, 0, u} (pair X Y)
j : Discrete WalkingPair
⊢ (BinaryFan.fst s ≫ b.inl + BinaryFan.snd s ≫ b.inr) ≫ b.toCone.π.app j = s.π.app j
have left : Eq (α := s.pt ⟶ obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
  ((BinaryFan.fst s ≫ b.inl + BinaryFan.snd s ≫ b.inr) ≫ b.toCone.π.app { as := WalkingPair.left })
  (s.π.app { as := WalkingPair.left })
Tactic: rcases j with ⟨⟨⟩⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
b : BinaryBicone.{v, u} X Y
total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.pt
s : Cone.{0, v, 0, u} (pair X Y)
j : Discrete WalkingPair
left :
  Eq (α := s.pt ⟶ obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
    ((BinaryFan.fst s ≫ b.inl + BinaryFan.snd s ≫ b.inr) ≫ b.toCone.π.app { as := WalkingPair.left })
    (s.π.app { as := WalkingPair.left })
⊢ (BinaryFan.fst s ≫ b.inl + BinaryFan.snd s ≫ b.inr) ≫ b.toCone.π.app j = s.π.app j
have right : Eq (α := s.pt ⟶ obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })
  ((BinaryFan.fst s ≫ b.inl + BinaryFan.snd s ≫ b.inr) ≫ b.toCone.π.app { as := WalkingPair.right })
  (s.π.app { as := WalkingPair.right })
Tactic: rcases j with ⟨⟨⟩⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
b : BinaryBicone.{v, u} X Y
total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.pt
s : Cone.{0, v, 0, u} (pair X Y)
m : s.pt ⟶ b.toCone.pt
h : ∀ (j : Discrete WalkingPair), m ≫ b.toCone.π.app j = s.π.app j
⊢ m = BinaryFan.fst s ≫ b.inl + BinaryFan.snd s ≫ b.inr
have hₗ : Eq (α := s.pt ⟶ obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
  (m ≫ b.toCone.π.app { as := WalkingPair.left }) (s.π.app { as := WalkingPair.left })
Tactic: have hₗ := h ⟨.left⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
b : BinaryBicone.{v, u} X Y
total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.pt
s : Cone.{0, v, 0, u} (pair X Y)
m : s.pt ⟶ b.toCone.pt
h : ∀ (j : Discrete WalkingPair), m ≫ b.toCone.π.app j = s.π.app j
hₗ :
  Eq (α := s.pt ⟶ obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
    (m ≫ b.toCone.π.app { as := WalkingPair.left }) (s.π.app { as := WalkingPair.left })
⊢ m = BinaryFan.fst s ≫ b.inl + BinaryFan.snd s ≫ b.inr
have hᵣ : Eq (α := s.pt ⟶ obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })
  (m ≫ b.toCone.π.app { as := WalkingPair.right }) (s.π.app { as := WalkingPair.right })
Tactic: have hᵣ := h ⟨.right⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
b : BinaryBicone.{v, u} X Y
total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.pt
s : Cocone.{0, v, 0, u} (pair X Y)
j : Discrete WalkingPair
⊢ b.toCocone.ι.app j ≫ (b.fst ≫ BinaryCofan.inl s + b.snd ≫ BinaryCofan.inr s) = s.ι.app j
have left : Eq (α := obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair } ⟶ s.pt)
  (b.toCocone.ι.app { as := WalkingPair.left } ≫ (b.fst ≫ BinaryCofan.inl s + b.snd ≫ BinaryCofan.inr s))
  (s.ι.app { as := WalkingPair.left })
Tactic: rcases j with ⟨⟨⟩⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
b : BinaryBicone.{v, u} X Y
total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.pt
s : Cocone.{0, v, 0, u} (pair X Y)
j : Discrete WalkingPair
left :
  Eq (α := obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair } ⟶ s.pt)
    (b.toCocone.ι.app { as := WalkingPair.left } ≫ (b.fst ≫ BinaryCofan.inl s + b.snd ≫ BinaryCofan.inr s))
    (s.ι.app { as := WalkingPair.left })
⊢ b.toCocone.ι.app j ≫ (b.fst ≫ BinaryCofan.inl s + b.snd ≫ BinaryCofan.inr s) = s.ι.app j
have right : Eq (α := obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair } ⟶ s.pt)
  (b.toCocone.ι.app { as := WalkingPair.right } ≫ (b.fst ≫ BinaryCofan.inl s + b.snd ≫ BinaryCofan.inr s))
  (s.ι.app { as := WalkingPair.right })
Tactic: rcases j with ⟨⟨⟩⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
b : BinaryBicone.{v, u} X Y
total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.pt
s : Cocone.{0, v, 0, u} (pair X Y)
m : b.toCocone.pt ⟶ s.pt
h : ∀ (j : Discrete WalkingPair), b.toCocone.ι.app j ≫ m = s.ι.app j
⊢ m = b.fst ≫ BinaryCofan.inl s + b.snd ≫ BinaryCofan.inr s
have hₗ : Eq (α := obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair } ⟶ s.pt)
  (b.toCocone.ι.app { as := WalkingPair.left } ≫ m) (s.ι.app { as := WalkingPair.left })
Tactic: have hₗ := h ⟨.left⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
b : BinaryBicone.{v, u} X Y
i : b.IsBilimit
j : Discrete WalkingPair
⊢ (b.fst ≫ b.inl + b.snd ≫ b.inr) ≫ b.toCone.π.app j = 𝟙 b.pt ≫ b.toCone.π.app j
have left : Eq (α := b.pt ⟶ obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
  ((b.fst ≫ b.inl + b.snd ≫ b.inr) ≫ b.toCone.π.app { as := WalkingPair.left })
  (𝟙 b.pt ≫ b.toCone.π.app { as := WalkingPair.left })
Tactic: rcases j with ⟨⟨⟩⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
b : BinaryBicone.{v, u} X Y
i : b.IsBilimit
j : Discrete WalkingPair
left :
  Eq (α := b.pt ⟶ obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
    ((b.fst ≫ b.inl + b.snd ≫ b.inr) ≫ b.toCone.π.app { as := WalkingPair.left })
    (𝟙 b.pt ≫ b.toCone.π.app { as := WalkingPair.left })
⊢ (b.fst ≫ b.inl + b.snd ≫ b.inr) ≫ b.toCone.π.app j = 𝟙 b.pt ≫ b.toCone.π.app j
have right : Eq (α := b.pt ⟶ obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })
  ((b.fst ≫ b.inl + b.snd ≫ b.inr) ≫ b.toCone.π.app { as := WalkingPair.right })
  (𝟙 b.pt ≫ b.toCone.π.app { as := WalkingPair.right })
Tactic: rcases j with ⟨⟨⟩⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
t : BinaryBicone.{v, u} X Y
ht : IsLimit t.toCone
⊢ t.inl = BinaryFan.IsLimit.lift ht (𝟙 X) 0
have x : ∀ (j : Discrete WalkingPair), t.inl ≫ t.toCone.π.app j = NatTrans.app (Cone.π (BinaryFan.mk (𝟙 X) 0)) j
Tactic: apply ht.uniq (BinaryFan.mk (𝟙 X) 0)
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
t : BinaryBicone.{v, u} X Y
ht : IsLimit t.toCone
⊢ t.inr = BinaryFan.IsLimit.lift ht 0 (𝟙 Y)
have x : ∀ (j : Discrete WalkingPair), t.inr ≫ t.toCone.π.app j = NatTrans.app (Cone.π (BinaryFan.mk 0 (𝟙 Y))) j
Tactic: apply ht.uniq (BinaryFan.mk 0 (𝟙 Y))
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
t : BinaryBicone.{v, u} X Y
ht : IsLimit t.toCone
⊢ t.fst ≫ t.inl + t.snd ≫ t.inr = 𝟙 t.pt
have refine_1 : (t.fst ≫ t.inl + t.snd ≫ t.inr) ≫ BinaryFan.fst t.toCone = 𝟙 t.pt ≫ BinaryFan.fst t.toCone
Tactic: refine BinaryFan.IsLimit.hom_ext ht ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
t : BinaryBicone.{v, u} X Y
ht : IsLimit t.toCone
refine_1 : (t.fst ≫ t.inl + t.snd ≫ t.inr) ≫ BinaryFan.fst t.toCone = 𝟙 t.pt ≫ BinaryFan.fst t.toCone
⊢ t.fst ≫ t.inl + t.snd ≫ t.inr = 𝟙 t.pt
have refine_2 : (t.fst ≫ t.inl + t.snd ≫ t.inr) ≫ BinaryFan.snd t.toCone = 𝟙 t.pt ≫ BinaryFan.snd t.toCone
Tactic: refine BinaryFan.IsLimit.hom_ext ht ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
t : BinaryBicone.{v, u} X Y
ht : IsColimit t.toCocone
⊢ t.fst = BinaryCofan.IsColimit.desc ht (𝟙 X) 0
have x : ∀ (j : Discrete WalkingPair), t.toCocone.ι.app j ≫ t.fst = NatTrans.app (Cocone.ι (BinaryCofan.mk (𝟙 X) 0)) j
Tactic: apply ht.uniq (BinaryCofan.mk (𝟙 X) 0)
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
t : BinaryBicone.{v, u} X Y
ht : IsColimit t.toCocone
⊢ t.snd = BinaryCofan.IsColimit.desc ht 0 (𝟙 Y)
have x : ∀ (j : Discrete WalkingPair), t.toCocone.ι.app j ≫ t.snd = NatTrans.app (Cocone.ι (BinaryCofan.mk 0 (𝟙 Y))) j
Tactic: apply ht.uniq (BinaryCofan.mk 0 (𝟙 Y))
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
t : BinaryBicone.{v, u} X Y
ht : IsColimit t.toCocone
⊢ t.fst ≫ t.inl + t.snd ≫ t.inr = 𝟙 t.pt
have refine_1 : BinaryCofan.inl t.toCocone ≫ (t.fst ≫ t.inl + t.snd ≫ t.inr) = BinaryCofan.inl t.toCocone ≫ 𝟙 t.pt
Tactic: refine BinaryCofan.IsColimit.hom_ext ht ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
t : BinaryBicone.{v, u} X Y
ht : IsColimit t.toCocone
refine_1 : BinaryCofan.inl t.toCocone ≫ (t.fst ≫ t.inl + t.snd ≫ t.inr) = BinaryCofan.inl t.toCocone ≫ 𝟙 t.pt
⊢ t.fst ≫ t.inl + t.snd ≫ t.inr = 𝟙 t.pt
have refine_2 : BinaryCofan.inr t.toCocone ≫ (t.fst ≫ t.inl + t.snd ≫ t.inr) = BinaryCofan.inr t.toCocone ≫ 𝟙 t.pt
Tactic: refine BinaryCofan.IsColimit.hom_ext ht ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
t : Cocone.{0, v, 0, u} (pair X Y)
ht : IsColimit t
j : Discrete WalkingPair
⊢ t.ι.app j ≫ Iso.hom (Iso.refl t.pt) = (BinaryBicone.toCocone (BinaryBicone.ofColimitCocone ht)).ι.app j
have left : Eq (α :=
  obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair } ⟶
    (BinaryBicone.toCocone (BinaryBicone.ofColimitCocone ht)).pt)
  (t.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫ Iso.hom (Iso.refl t.pt))
  ((BinaryBicone.toCocone (BinaryBicone.ofColimitCocone ht)).ι.app { as := WalkingPair.left })
Tactic: rcases j with ⟨⟨⟩⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
t : Cocone.{0, v, 0, u} (pair X Y)
ht : IsColimit t
j : Discrete WalkingPair
left :
  Eq (α :=
    obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair } ⟶
      (BinaryBicone.toCocone (BinaryBicone.ofColimitCocone ht)).pt)
    (t.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫ Iso.hom (Iso.refl t.pt))
    ((BinaryBicone.toCocone (BinaryBicone.ofColimitCocone ht)).ι.app { as := WalkingPair.left })
⊢ t.ι.app j ≫ Iso.hom (Iso.refl t.pt) = (BinaryBicone.toCocone (BinaryBicone.ofColimitCocone ht)).ι.app j
have right : Eq (α :=
  obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair } ⟶
    (BinaryBicone.toCocone (BinaryBicone.ofColimitCocone ht)).pt)
  (t.ι.app { as := WalkingPair.right : Discrete WalkingPair } ≫ Iso.hom (Iso.refl t.pt))
  ((BinaryBicone.toCocone (BinaryBicone.ofColimitCocone ht)).ι.app { as := WalkingPair.right })
Tactic: rcases j with ⟨⟨⟩⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
inst_2 : HasBinaryBiproduct.{v, u} X Y
⊢ HAdd.hAdd (α := biprod.{v, u} X Y ⟶ biprod.{v, u} X Y) (fst ≫ inl) (snd ≫ inr) = 𝟙 (biprod.{v, u} X Y)
have h₀ : (inl ≫ HAdd.hAdd (α := biprod.{v, u} X Y ⟶ biprod.{v, u} X Y) (fst ≫ inl) (snd ≫ inr)) ≫ fst =
  (inl ≫ 𝟙 (biprod.{v, u} X Y)) ≫ fst
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
inst_2 : HasBinaryBiproduct.{v, u} X Y
h₀ :
  (inl ≫ HAdd.hAdd (α := biprod.{v, u} X Y ⟶ biprod.{v, u} X Y) (fst ≫ inl) (snd ≫ inr)) ≫ fst =
    (inl ≫ 𝟙 (biprod.{v, u} X Y)) ≫ fst
⊢ HAdd.hAdd (α := biprod.{v, u} X Y ⟶ biprod.{v, u} X Y) (fst ≫ inl) (snd ≫ inr) = 𝟙 (biprod.{v, u} X Y)
have h₁ : (inl ≫ HAdd.hAdd (α := biprod.{v, u} X Y ⟶ biprod.{v, u} X Y) (fst ≫ inl) (snd ≫ inr)) ≫ snd =
  (inl ≫ 𝟙 (biprod.{v, u} X Y)) ≫ snd
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
inst_2 : HasBinaryBiproduct.{v, u} X Y
h₀ :
  (inl ≫ HAdd.hAdd (α := biprod.{v, u} X Y ⟶ biprod.{v, u} X Y) (fst ≫ inl) (snd ≫ inr)) ≫ fst =
    (inl ≫ 𝟙 (biprod.{v, u} X Y)) ≫ fst
h₁ :
  (inl ≫ HAdd.hAdd (α := biprod.{v, u} X Y ⟶ biprod.{v, u} X Y) (fst ≫ inl) (snd ≫ inr)) ≫ snd =
    (inl ≫ 𝟙 (biprod.{v, u} X Y)) ≫ snd
⊢ HAdd.hAdd (α := biprod.{v, u} X Y ⟶ biprod.{v, u} X Y) (fst ≫ inl) (snd ≫ inr) = 𝟙 (biprod.{v, u} X Y)
have h₂ : (inr ≫ HAdd.hAdd (α := biprod.{v, u} X Y ⟶ biprod.{v, u} X Y) (fst ≫ inl) (snd ≫ inr)) ≫ fst =
  (inr ≫ 𝟙 (biprod.{v, u} X Y)) ≫ fst
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
inst_2 : HasBinaryBiproduct.{v, u} X Y
h₀ :
  (inl ≫ HAdd.hAdd (α := biprod.{v, u} X Y ⟶ biprod.{v, u} X Y) (fst ≫ inl) (snd ≫ inr)) ≫ fst =
    (inl ≫ 𝟙 (biprod.{v, u} X Y)) ≫ fst
h₁ :
  (inl ≫ HAdd.hAdd (α := biprod.{v, u} X Y ⟶ biprod.{v, u} X Y) (fst ≫ inl) (snd ≫ inr)) ≫ snd =
    (inl ≫ 𝟙 (biprod.{v, u} X Y)) ≫ snd
h₂ :
  (inr ≫ HAdd.hAdd (α := biprod.{v, u} X Y ⟶ biprod.{v, u} X Y) (fst ≫ inl) (snd ≫ inr)) ≫ fst =
    (inr ≫ 𝟙 (biprod.{v, u} X Y)) ≫ fst
⊢ HAdd.hAdd (α := biprod.{v, u} X Y ⟶ biprod.{v, u} X Y) (fst ≫ inl) (snd ≫ inr) = 𝟙 (biprod.{v, u} X Y)
have h₃ : (inr ≫ HAdd.hAdd (α := biprod.{v, u} X Y ⟶ biprod.{v, u} X Y) (fst ≫ inl) (snd ≫ inr)) ≫ snd =
  (inr ≫ 𝟙 (biprod.{v, u} X Y)) ≫ snd
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
inst_2 : HasBinaryBiproduct.{v, u} X Y
T : C
f : T ⟶ X
g : T ⟶ Y
⊢ lift f g = HAdd.hAdd (α := T ⟶ biprod.{v, u} X Y) (f ≫ inl) (g ≫ inr)
have h₀ : CategoryStruct.comp (Y := biprod.{v, u} X Y) (lift f g) fst =
  HAdd.hAdd (α := T ⟶ biprod.{v, u} X Y) (f ≫ inl) (g ≫ inr) ≫ fst
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
inst_2 : HasBinaryBiproduct.{v, u} X Y
T : C
f : T ⟶ X
g : T ⟶ Y
h₀ :
  CategoryStruct.comp (Y := biprod.{v, u} X Y) (lift f g) fst =
    HAdd.hAdd (α := T ⟶ biprod.{v, u} X Y) (f ≫ inl) (g ≫ inr) ≫ fst
⊢ lift f g = HAdd.hAdd (α := T ⟶ biprod.{v, u} X Y) (f ≫ inl) (g ≫ inr)
have h₁ : CategoryStruct.comp (Y := biprod.{v, u} X Y) (lift f g) snd =
  HAdd.hAdd (α := T ⟶ biprod.{v, u} X Y) (f ≫ inl) (g ≫ inr) ≫ snd
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
inst_2 : HasBinaryBiproduct.{v, u} X Y
T : C
f : X ⟶ T
g : Y ⟶ T
⊢ desc f g = HAdd.hAdd (α := biprod.{v, u} X Y ⟶ T) (fst ≫ f) (snd ≫ g)
have h₀ : CategoryStruct.comp (Y := biprod.{v, u} X Y) inl (desc f g) =
  inl ≫ HAdd.hAdd (α := biprod.{v, u} X Y ⟶ T) (fst ≫ f) (snd ≫ g)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
inst_2 : HasBinaryBiproduct.{v, u} X Y
T : C
f : X ⟶ T
g : Y ⟶ T
h₀ :
  CategoryStruct.comp (Y := biprod.{v, u} X Y) inl (desc f g) =
    inl ≫ HAdd.hAdd (α := biprod.{v, u} X Y ⟶ T) (fst ≫ f) (snd ≫ g)
⊢ desc f g = HAdd.hAdd (α := biprod.{v, u} X Y ⟶ T) (fst ≫ f) (snd ≫ g)
have h₁ : CategoryStruct.comp (Y := biprod.{v, u} X Y) inr (desc f g) =
  inr ≫ HAdd.hAdd (α := biprod.{v, u} X Y ⟶ T) (fst ≫ f) (snd ≫ g)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
⊢ map f g = HAdd.hAdd (α := biprod.{v, u} W X ⟶ biprod.{v, u} Y Z) (fst ≫ f ≫ inl) (snd ≫ g ≫ inr)
have h₀ : CategoryStruct.comp (Y := biprod.{v, u} Y Z) (CategoryStruct.comp (Y := biprod.{v, u} W X) inl (map f g)) fst =
  (inl ≫ HAdd.hAdd (α := biprod.{v, u} W X ⟶ biprod.{v, u} Y Z) (fst ≫ f ≫ inl) (snd ≫ g ≫ inr)) ≫ fst
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
h₀ :
  CategoryStruct.comp (Y := biprod.{v, u} Y Z) (CategoryStruct.comp (Y := biprod.{v, u} W X) inl (map f g)) fst =
    (inl ≫ HAdd.hAdd (α := biprod.{v, u} W X ⟶ biprod.{v, u} Y Z) (fst ≫ f ≫ inl) (snd ≫ g ≫ inr)) ≫ fst
⊢ map f g = HAdd.hAdd (α := biprod.{v, u} W X ⟶ biprod.{v, u} Y Z) (fst ≫ f ≫ inl) (snd ≫ g ≫ inr)
have h₁ : CategoryStruct.comp (Y := biprod.{v, u} Y Z) (CategoryStruct.comp (Y := biprod.{v, u} W X) inl (map f g)) snd =
  (inl ≫ HAdd.hAdd (α := biprod.{v, u} W X ⟶ biprod.{v, u} Y Z) (fst ≫ f ≫ inl) (snd ≫ g ≫ inr)) ≫ snd
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
h₀ :
  CategoryStruct.comp (Y := biprod.{v, u} Y Z) (CategoryStruct.comp (Y := biprod.{v, u} W X) inl (map f g)) fst =
    (inl ≫ HAdd.hAdd (α := biprod.{v, u} W X ⟶ biprod.{v, u} Y Z) (fst ≫ f ≫ inl) (snd ≫ g ≫ inr)) ≫ fst
h₁ :
  CategoryStruct.comp (Y := biprod.{v, u} Y Z) (CategoryStruct.comp (Y := biprod.{v, u} W X) inl (map f g)) snd =
    (inl ≫ HAdd.hAdd (α := biprod.{v, u} W X ⟶ biprod.{v, u} Y Z) (fst ≫ f ≫ inl) (snd ≫ g ≫ inr)) ≫ snd
⊢ map f g = HAdd.hAdd (α := biprod.{v, u} W X ⟶ biprod.{v, u} Y Z) (fst ≫ f ≫ inl) (snd ≫ g ≫ inr)
have h₂ : CategoryStruct.comp (Y := biprod.{v, u} Y Z) (CategoryStruct.comp (Y := biprod.{v, u} W X) inr (map f g)) fst =
  (inr ≫ HAdd.hAdd (α := biprod.{v, u} W X ⟶ biprod.{v, u} Y Z) (fst ≫ f ≫ inl) (snd ≫ g ≫ inr)) ≫ fst
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
h₀ :
  CategoryStruct.comp (Y := biprod.{v, u} Y Z) (CategoryStruct.comp (Y := biprod.{v, u} W X) inl (map f g)) fst =
    (inl ≫ HAdd.hAdd (α := biprod.{v, u} W X ⟶ biprod.{v, u} Y Z) (fst ≫ f ≫ inl) (snd ≫ g ≫ inr)) ≫ fst
h₁ :
  CategoryStruct.comp (Y := biprod.{v, u} Y Z) (CategoryStruct.comp (Y := biprod.{v, u} W X) inl (map f g)) snd =
    (inl ≫ HAdd.hAdd (α := biprod.{v, u} W X ⟶ biprod.{v, u} Y Z) (fst ≫ f ≫ inl) (snd ≫ g ≫ inr)) ≫ snd
h₂ :
  CategoryStruct.comp (Y := biprod.{v, u} Y Z) (CategoryStruct.comp (Y := biprod.{v, u} W X) inr (map f g)) fst =
    (inr ≫ HAdd.hAdd (α := biprod.{v, u} W X ⟶ biprod.{v, u} Y Z) (fst ≫ f ≫ inl) (snd ≫ g ≫ inr)) ≫ fst
⊢ map f g = HAdd.hAdd (α := biprod.{v, u} W X ⟶ biprod.{v, u} Y Z) (fst ≫ f ≫ inl) (snd ≫ g ≫ inr)
have h₃ : CategoryStruct.comp (Y := biprod.{v, u} Y Z) (CategoryStruct.comp (Y := biprod.{v, u} W X) inr (map f g)) snd =
  (inr ≫ HAdd.hAdd (α := biprod.{v, u} W X ⟶ biprod.{v, u} Y Z) (fst ≫ f ≫ inl) (snd ≫ g ≫ inr)) ≫ snd
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
f : X ⟶ Y
inst_3 : IsSplitMono f
c : CokernelCofork f
i : IsColimit c
⊢ Eq (α := c.pt ⟶ X)
    (SplitEpi.section_ (f := Cofork.π (coforkOfCokernelCofork (CokernelCofork.ofπ (Cofork.π c) ⋯)))
          (splitEpiOfIdempotentOfIsColimitCofork C ⋯
              (isColimitCoforkOfCokernelCofork (isCokernelEpiComp i (retraction f) ⋯)) :
            SplitEpi (Y :=
              Cocone.pt (F := parallelPair (𝟙 Y) (𝟙 Y - retraction f ≫ f))
                (coforkOfCokernelCofork (CokernelCofork.ofπ (Cofork.π c) ⋯)))
              (Cofork.π (coforkOfCokernelCofork (CokernelCofork.ofπ (Cofork.π c) ⋯)))) ≫
        retraction f :
      c.pt ⟶ X)
    (0 : c.pt ⟶ X)
have rw : Eq (α := c.pt ⟶ X)
  (i.desc (Cofork.ofπ (Cofork.π (cokernelCoforkOfCofork (Cofork.ofπ (𝟙 Y - retraction f ≫ f) sorry))) sorry) ≫ retraction f) 0
Tactic: rw [splitEpiOfIdempotentOfIsColimitCofork_section_,
      isColimitCoforkOfCokernelCofork_desc, isCokernelEpiComp_desc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
f : X ⟶ Y
inst_3 : IsSplitMono f
c : CokernelCofork f
i : IsColimit c
⊢ Eq (α := c.pt ⟶ X)
    (i.desc (Cofork.ofπ (Cofork.π (cokernelCoforkOfCofork (Cofork.ofπ (𝟙 Y - retraction f ≫ f) ⋯))) ⋯) ≫ retraction f) 0
have dsimp : Eq (α := c.pt ⟶ X) (i.desc (Cofork.ofπ (Cofork.π (CokernelCofork.ofπ (𝟙 Y - retraction f ≫ f) sorry)) sorry) ≫ retraction f) 0
Tactic: dsimp only [cokernelCoforkOfCofork_ofπ]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
f : X ⟶ Y
inst_3 : IsSplitMono f
c : CokernelCofork f
i : IsColimit c
this : Epi (Cofork.π c) := ⋯
⊢ Eq (α := c.pt ⟶ X) (i.desc (Cofork.ofπ (Cofork.π (CokernelCofork.ofπ (𝟙 Y - retraction f ≫ f) ⋯)) ⋯) ≫ retraction f) 0
have apply : Eq (α := Y ⟶ X)
  (Cofork.π c ≫ i.desc (Cofork.ofπ (Cofork.π (CokernelCofork.ofπ (𝟙 Y - retraction f ≫ f) sorry)) sorry) ≫ retraction f) 0
Tactic: apply zero_of_epi_comp c.π