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
inst_2 : HasBinaryBiproducts.{v, u} C
X₁ X₂ Y₁ Y₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
inst_3 : IsIso f₁₁
inst_4 :
  IsIso (X := biprod.{v, u} X₁ X₂) (Y := biprod.{v, u} Y₁ Y₂)
    (ofComponents f₁₁ f₁₂ f₂₁ f₂₂ : biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂)
L : biprod.{v, u} X₁ X₂ ≅ biprod.{v, u} X₁ X₂
R : biprod.{v, u} Y₁ Y₂ ≅ biprod.{v, u} Y₁ Y₂
g : X₂ ⟶ Y₂
w : L.hom ≫ ofComponents f₁₁ f₁₂ f₂₁ f₂₂ ≫ R.hom = biprod.map f₁₁ g
⊢ IsIso (X := biprod.{v, u} X₁ X₂) (Y := biprod.{v, u} Y₁ Y₂) (biprod.map f₁₁ g)
have rw : IsIso (L.hom ≫ ofComponents f₁₁ f₁₂ f₂₁ f₂₂ ≫ R.hom)
Tactic: rw [← w]
-- 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
X₁ X₂ Y₁ Y₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
f : biprod.{v, u} X₁ X₂ ≅ biprod.{v, u} Y₁ Y₂
inst_3 : IsIso (biprod.inl ≫ f.hom ≫ biprod.fst)
⊢ IsIso (X := biprod.{v, u} X₁ X₂) (Y := biprod.{v, u} Y₁ Y₂)
    (ofComponents (biprod.inl ≫ f.hom ≫ biprod.fst) (biprod.inl ≫ f.hom ≫ biprod.snd) (biprod.inr ≫ f.hom ≫ biprod.fst)
        (biprod.inr ≫ f.hom ≫ biprod.snd) :
      biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂)
have simp : IsIso f.hom
Tactic: simp only [Biprod.ofComponents_eq]
-- 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 : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
⊢ Eq.{v + 1} (α := W ⟶ W) (𝟙 W) 0 ∨ biprod.inl ≫ f ≫ biprod.fst ≠ 0 ∨ biprod.inl ≫ f ≫ biprod.snd ≠ 0
have by_contra! : ∀ (nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0) (a₁ : biprod.inl ≫ f ≫ biprod.fst = 0) (a₂ : biprod.inl ≫ f ≫ biprod.snd = 0),
  False
Tactic: by_contra! ⟨nz, a₁, a₂⟩
-- 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
inst_2 : HasBinaryBiproducts.{v, u} C
W X Y Z : C
f : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
⊢ False
have h₁ : x = 𝟙 W
Tactic: have h₁ : x = 𝟙 W := by simp [x]
-- 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 : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
⊢ biprod.inl ≫ f ≫ inv f ≫ biprod.fst = 0
have rw : biprod.inl ≫
    f ≫
      HAdd.hAdd (α := biprod.{v, u} Y Z ⟶ biprod.{v, u} Y Z) (biprod.fst ≫ biprod.inl) (biprod.snd ≫ biprod.inr) ≫
        inv f ≫ biprod.fst =
  0
Tactic: rw [← Category.id_comp (inv f), Category.assoc, ← biprod.total]
-- 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 : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
| biprod.inl ≫
    f ≫
      HAdd.hAdd (α := biprod.{v, u} Y Z ⟶ biprod.{v, u} Y Z) (biprod.fst ≫ biprod.inl) (biprod.snd ≫ biprod.inr) ≫
        inv f ≫ biprod.fst
have a : f ≫ HAdd.hAdd (α := biprod.{v, u} Y Z ⟶ biprod.{v, u} Y Z) (biprod.fst ≫ biprod.inl) (biprod.snd ≫ biprod.inr)
Tactic: slice 2 3
-- 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 : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
a : f ≫ HAdd.hAdd (α := biprod.{v, u} Y Z ⟶ biprod.{v, u} Y Z) (biprod.fst ≫ biprod.inl) (biprod.snd ≫ biprod.inr)
| biprod.inl ≫
    f ≫
      HAdd.hAdd (α := biprod.{v, u} Y Z ⟶ biprod.{v, u} Y Z) (biprod.fst ≫ biprod.inl) (biprod.snd ≫ biprod.inr) ≫
        inv f ≫ biprod.fst
have a₃ : inv f
Tactic: slice 2 3
-- 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 : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
a : f ≫ HAdd.hAdd (α := biprod.{v, u} Y Z ⟶ biprod.{v, u} Y Z) (biprod.fst ≫ biprod.inl) (biprod.snd ≫ biprod.inr)
a₃ : inv f
| biprod.inl ≫
    f ≫
      HAdd.hAdd (α := biprod.{v, u} Y Z ⟶ biprod.{v, u} Y Z) (biprod.fst ≫ biprod.inl) (biprod.snd ≫ biprod.inr) ≫
        inv f ≫ biprod.fst
have a₄ : biprod.fst
Tactic: slice 2 3
-- 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 : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
a : f ≫ HAdd.hAdd (α := biprod.{v, u} Y Z ⟶ biprod.{v, u} Y Z) (biprod.fst ≫ biprod.inl) (biprod.snd ≫ biprod.inr)
a₃ : inv f
a₄ : biprod.fst
| biprod.inl ≫
    f ≫
      HAdd.hAdd (α := biprod.{v, u} Y Z ⟶ biprod.{v, u} Y Z) (biprod.fst ≫ biprod.inl) (biprod.snd ≫ biprod.inr) ≫
        inv f ≫ biprod.fst
have a₅ : biprod.inl
Tactic: slice 2 3
-- 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 : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
| f ≫ HAdd.hAdd (α := biprod.{v, u} Y Z ⟶ biprod.{v, u} Y Z) (biprod.fst ≫ biprod.inl) (biprod.snd ≫ biprod.inr)
have a : HAdd.hAdd (α := biprod.{v, u} W X ⟶ biprod.{v, u} Y Z) (f ≫ biprod.fst ≫ biprod.inl) (f ≫ biprod.snd ≫ biprod.inr)
Tactic: rw [comp_add]
-- 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 : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
| biprod.inl ≫
    f ≫
      HAdd.hAdd (α := biprod.{v, u} Y Z ⟶ biprod.{v, u} Y Z) (biprod.fst ≫ biprod.inl) (biprod.snd ≫ biprod.inr) ≫
        inv f ≫ biprod.fst
have a : HAdd.hAdd (α := biprod.{v, u} W X ⟶ biprod.{v, u} Y Z) (f ≫ biprod.fst ≫ biprod.inl) (f ≫ biprod.snd ≫ biprod.inr)
Tactic: slice 2 3
      rw [comp_add]
-- 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 : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
a : HAdd.hAdd (α := biprod.{v, u} W X ⟶ biprod.{v, u} Y Z) (f ≫ biprod.fst ≫ biprod.inl) (f ≫ biprod.snd ≫ biprod.inr)
| biprod.inl ≫
    f ≫
      HAdd.hAdd (α := biprod.{v, u} Y Z ⟶ biprod.{v, u} Y Z) (biprod.fst ≫ biprod.inl) (biprod.snd ≫ biprod.inr) ≫
        inv f ≫ biprod.fst
have a₃ : inv f
Tactic: slice 2 3
      rw [comp_add]
-- 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 : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
a : HAdd.hAdd (α := biprod.{v, u} W X ⟶ biprod.{v, u} Y Z) (f ≫ biprod.fst ≫ biprod.inl) (f ≫ biprod.snd ≫ biprod.inr)
a₃ : inv f
| biprod.inl ≫
    f ≫
      HAdd.hAdd (α := biprod.{v, u} Y Z ⟶ biprod.{v, u} Y Z) (biprod.fst ≫ biprod.inl) (biprod.snd ≫ biprod.inr) ≫
        inv f ≫ biprod.fst
have a₄ : biprod.fst
Tactic: slice 2 3
      rw [comp_add]
-- 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 : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
a : HAdd.hAdd (α := biprod.{v, u} W X ⟶ biprod.{v, u} Y Z) (f ≫ biprod.fst ≫ biprod.inl) (f ≫ biprod.snd ≫ biprod.inr)
a₃ : inv f
a₄ : biprod.fst
| biprod.inl ≫
    f ≫
      HAdd.hAdd (α := biprod.{v, u} Y Z ⟶ biprod.{v, u} Y Z) (biprod.fst ≫ biprod.inl) (biprod.snd ≫ biprod.inr) ≫
        inv f ≫ biprod.fst
have a₅ : biprod.inl
Tactic: slice 2 3
      rw [comp_add]
-- 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 : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
⊢ biprod.inl ≫
      f ≫
        HAdd.hAdd (α := biprod.{v, u} Y Z ⟶ biprod.{v, u} Y Z) (biprod.fst ≫ biprod.inl) (biprod.snd ≫ biprod.inr) ≫
          inv f ≫ biprod.fst =
    0
have conv_lhs : biprod.inl ≫
    (HAdd.hAdd (α := biprod.{v, u} W X ⟶ biprod.{v, u} Y Z) (f ≫ biprod.fst ≫ biprod.inl)
          (f ≫ biprod.snd ≫ biprod.inr) ≫
        inv f) ≫
      biprod.fst =
  0
Tactic: conv_lhs =>
      slice 2 3
      rw [comp_add]
-- 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 : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
⊢ biprod.inl ≫
      (HAdd.hAdd (α := biprod.{v, u} W X ⟶ biprod.{v, u} Y Z) (f ≫ biprod.fst ≫ biprod.inl)
            (f ≫ biprod.snd ≫ biprod.inr) ≫
          inv f) ≫
        biprod.fst =
    0
have simp : biprod.inl ≫
    HAdd.hAdd (α := biprod.{v, u} W X ⟶ biprod.{v, u} Y Z) (f ≫ biprod.fst ≫ biprod.inl) (f ≫ biprod.snd ≫ biprod.inr) ≫
      inv f ≫ biprod.fst =
  0
Tactic: simp only [Category.assoc]
-- 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 : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
⊢ biprod.inl ≫
      HAdd.hAdd (α := biprod.{v, u} W X ⟶ biprod.{v, u} Y Z) (f ≫ biprod.fst ≫ biprod.inl)
          (f ≫ biprod.snd ≫ biprod.inr) ≫
        inv f ≫ biprod.fst =
    0
have rw : (biprod.inl ≫ f ≫ biprod.fst ≫ biprod.inl) ≫ inv f ≫ biprod.fst +
    (biprod.inl ≫ f ≫ biprod.snd ≫ biprod.inr) ≫ inv f ≫ biprod.fst =
  0
Tactic: rw [comp_add_assoc, add_comp]
-- 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 : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
| (biprod.inl ≫ f ≫ biprod.fst ≫ biprod.inl) ≫ inv f ≫ biprod.fst +
    (biprod.inl ≫ f ≫ biprod.snd ≫ biprod.inr) ≫ inv f ≫ biprod.fst
have congr : (biprod.inl ≫ f ≫ biprod.fst ≫ biprod.inl) ≫ inv f ≫ biprod.fst
Tactic: congr
-- 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 : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
congr : (biprod.inl ≫ f ≫ biprod.fst ≫ biprod.inl) ≫ inv f ≫ biprod.fst
| (biprod.inl ≫ f ≫ biprod.fst ≫ biprod.inl) ≫ inv f ≫ biprod.fst +
    (biprod.inl ≫ f ≫ biprod.snd ≫ biprod.inr) ≫ inv f ≫ biprod.fst
have a : (biprod.inl ≫ f ≫ biprod.snd ≫ biprod.inr) ≫ inv f ≫ biprod.fst
Tactic: congr
-- 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 : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
a : biprod.inl ≫ f ≫ biprod.snd
| (biprod.inl ≫ f ≫ biprod.snd ≫ biprod.inr) ≫ inv f ≫ biprod.fst
have a₃ : biprod.inr
Tactic: slice 1 3
-- 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 : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
a : biprod.inl ≫ f ≫ biprod.snd
a₃ : biprod.inr
| (biprod.inl ≫ f ≫ biprod.snd ≫ biprod.inr) ≫ inv f ≫ biprod.fst
have a₄ : inv f
Tactic: slice 1 3
-- 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 : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
a : biprod.inl ≫ f ≫ biprod.snd
a₃ : biprod.inr
a₄ : inv f
| (biprod.inl ≫ f ≫ biprod.snd ≫ biprod.inr) ≫ inv f ≫ biprod.fst
have a₅ : biprod.fst
Tactic: slice 1 3
-- 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 : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
| biprod.inl ≫ f ≫ biprod.snd
have a : 0
Tactic: rw [a₂]
-- 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 : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
| (biprod.inl ≫ f ≫ biprod.fst ≫ biprod.inl) ≫ inv f ≫ biprod.fst +
    (biprod.inl ≫ f ≫ biprod.snd ≫ biprod.inr) ≫ inv f ≫ biprod.fst
have a : 0
Tactic: congr
      next => skip
      slice 1 3
      rw [a₂]
-- 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 : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
a : 0
| (biprod.inl ≫ f ≫ biprod.fst ≫ biprod.inl) ≫ inv f ≫ biprod.fst +
    (biprod.inl ≫ f ≫ biprod.snd ≫ biprod.inr) ≫ inv f ≫ biprod.fst
have a₃ : biprod.inr
Tactic: congr
      next => skip
      slice 1 3
      rw [a₂]
-- 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 : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
a : 0
a₃ : biprod.inr
| (biprod.inl ≫ f ≫ biprod.fst ≫ biprod.inl) ≫ inv f ≫ biprod.fst +
    (biprod.inl ≫ f ≫ biprod.snd ≫ biprod.inr) ≫ inv f ≫ biprod.fst
have a₄ : inv f
Tactic: congr
      next => skip
      slice 1 3
      rw [a₂]
-- 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 : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
a : 0
a₃ : biprod.inr
a₄ : inv f
| (biprod.inl ≫ f ≫ biprod.fst ≫ biprod.inl) ≫ inv f ≫ biprod.fst +
    (biprod.inl ≫ f ≫ biprod.snd ≫ biprod.inr) ≫ inv f ≫ biprod.fst
have a₅ : biprod.fst
Tactic: congr
      next => skip
      slice 1 3
      rw [a₂]
-- 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 : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
⊢ (biprod.inl ≫ f ≫ biprod.fst ≫ biprod.inl) ≫ inv f ≫ biprod.fst +
      (biprod.inl ≫ f ≫ biprod.snd ≫ biprod.inr) ≫ inv f ≫ biprod.fst =
    0
have conv_lhs : (biprod.inl ≫ f ≫ biprod.fst ≫ biprod.inl) ≫ inv f ≫ biprod.fst + ((0 ≫ biprod.inr) ≫ inv f) ≫ biprod.fst = 0
Tactic: conv_lhs =>
      congr
      next => skip
      slice 1 3
      rw [a₂]
-- 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 : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
⊢ (biprod.inl ≫ f ≫ biprod.fst ≫ biprod.inl) ≫ inv f ≫ biprod.fst + ((0 ≫ biprod.inr) ≫ inv f) ≫ biprod.fst = 0
have simp : (biprod.inl ≫ f ≫ biprod.fst ≫ biprod.inl) ≫ inv f ≫ biprod.fst = 0
Tactic: simp only [zero_comp, add_zero]
-- 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 : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
a : biprod.inl ≫ f ≫ biprod.fst
| (biprod.inl ≫ f ≫ biprod.fst ≫ biprod.inl) ≫ inv f ≫ biprod.fst
have a₃ : biprod.inl
Tactic: slice 1 3
-- 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 : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
a : biprod.inl ≫ f ≫ biprod.fst
a₃ : biprod.inl
| (biprod.inl ≫ f ≫ biprod.fst ≫ biprod.inl) ≫ inv f ≫ biprod.fst
have a₄ : inv f
Tactic: slice 1 3
-- 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 : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
a : biprod.inl ≫ f ≫ biprod.fst
a₃ : biprod.inl
a₄ : inv f
| (biprod.inl ≫ f ≫ biprod.fst ≫ biprod.inl) ≫ inv f ≫ biprod.fst
have a₅ : biprod.fst
Tactic: slice 1 3
-- 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 : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
| biprod.inl ≫ f ≫ biprod.fst
have a : 0
Tactic: rw [a₁]
-- 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 : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
| (biprod.inl ≫ f ≫ biprod.fst ≫ biprod.inl) ≫ inv f ≫ biprod.fst
have a : 0
Tactic: slice 1 3
      rw [a₁]
-- 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 : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
a : 0
| (biprod.inl ≫ f ≫ biprod.fst ≫ biprod.inl) ≫ inv f ≫ biprod.fst
have a₃ : biprod.inl
Tactic: slice 1 3
      rw [a₁]
-- 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 : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
a : 0
a₃ : biprod.inl
| (biprod.inl ≫ f ≫ biprod.fst ≫ biprod.inl) ≫ inv f ≫ biprod.fst
have a₄ : inv f
Tactic: slice 1 3
      rw [a₁]