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
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
a₄ : inv f
| (biprod.inl ≫ f ≫ biprod.fst ≫ biprod.inl) ≫ inv f ≫ biprod.fst
have a₅ : biprod.fst
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
⊢ (biprod.inl ≫ f ≫ biprod.fst ≫ biprod.inl) ≫ inv f ≫ biprod.fst = 0
have conv_lhs : Eq (α := W ⟶ W) (((0 ≫ biprod.inl) ≫ inv f) ≫ biprod.fst) 0
Tactic: conv_lhs =>
      slice 1 3
      rw [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
h₁ : x = 𝟙 W
⊢ False
have h₀ : x = 0
Tactic: have h₀ : x = 0 := by
    dsimp [x]
    rw [← Category.id_comp (inv f), Category.assoc, ← biprod.total]
    conv_lhs =>
      slice 2 3
      rw [comp_add]
    simp only [Category.assoc]
    rw [comp_add_assoc, add_comp]
    conv_lhs =>
      congr
      next => skip
      slice 1 3
      rw [a₂]
    simp only [zero_comp, add_zero]
    conv_lhs =>
      slice 1 3
      rw [a₁]
    simp only [zero_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
σ τ : Type
inst_2 : Finite τ
S : σ → C
inst_3 : HasBiproduct.{0, v, u} S
T : τ → C
inst_4 : HasBiproduct.{0, v, u} T
s : σ
f : biproduct.{0, v, u} S ⟶ biproduct.{0, v, u} T
inst_5 : IsIso f
⊢ (∀ (t : τ), biproduct.ι S s ≫ f ≫ biproduct.π T t = 0) → Eq.{v + 1} (α := S s ⟶ S s) (𝟙 (S s)) 0
have intro : ∀ (val : Fintype τ), (∀ (t : τ), biproduct.ι S s ≫ f ≫ biproduct.π T t = 0) → Eq.{v + 1} (α := S s ⟶ S s) (𝟙 (S s)) 0
Tactic: cases nonempty_fintype τ
-- 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
σ τ : Type
inst_2 : Finite τ
S : σ → C
inst_3 : HasBiproduct.{0, v, u} S
T : τ → C
inst_4 : HasBiproduct.{0, v, u} T
s : σ
f : biproduct.{0, v, u} S ⟶ biproduct.{0, v, u} T
inst_5 : IsIso f
val : Fintype τ
z : ∀ (t : τ), biproduct.ι S s ≫ f ≫ biproduct.π T t = 0
⊢ Eq.{v + 1} (α := S s ⟶ S s) (𝟙 (S s)) 0
have reassoced : ∀ {t : τ} {W : C} (h : T t ⟶ W), biproduct.ι S s ≫ f ≫ biproduct.π T t ≫ h = 0 ≫ h
Tactic: have reassoced {t : τ} {W : C} (h : _ ⟶ W) :
    biproduct.ι S s ≫ f ≫ biproduct.π T t ≫ h = 0 ≫ h := by grind
-- 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
σ τ : Type
inst_2 : Finite τ
S : σ → C
inst_3 : HasBiproduct.{0, v, u} S
T : τ → C
inst_4 : HasBiproduct.{0, v, u} T
s : σ
f : biproduct.{0, v, u} S ⟶ biproduct.{0, v, u} T
inst_5 : IsIso f
val : Fintype τ
z : ∀ (t : τ), biproduct.ι S s ≫ f ≫ biproduct.π T t = 0
reassoced : ∀ {t : τ} {W : C} (h : T t ⟶ W), biproduct.ι S s ≫ f ≫ biproduct.π T t ≫ h = 0 ≫ h
x : S s ⟶ S s := biproduct.ι S s ≫ f ≫ inv f ≫ biproduct.π S s
⊢ Eq.{v + 1} (α := S s ⟶ S s) (𝟙 (S s)) 0
have h₁ : x = 𝟙 (S s)
Tactic: have h₁ : x = 𝟙 (S s) := 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
σ τ : Type
inst_2 : Finite τ
S : σ → C
inst_3 : HasBiproduct.{0, v, u} S
T : τ → C
inst_4 : HasBiproduct.{0, v, u} T
s : σ
f : biproduct.{0, v, u} S ⟶ biproduct.{0, v, u} T
inst_5 : IsIso f
val : Fintype τ
z : ∀ (t : τ), biproduct.ι S s ≫ f ≫ biproduct.π T t = 0
reassoced : ∀ {t : τ} {W : C} (h : T t ⟶ W), biproduct.ι S s ≫ f ≫ biproduct.π T t ≫ h = 0 ≫ h
x : S s ⟶ S s := biproduct.ι S s ≫ f ≫ inv f ≫ biproduct.π S s
h₁ : x = 𝟙 (S s)
⊢ biproduct.ι S s ≫ f ≫ inv f ≫ biproduct.π S s = 0
have rw : biproduct.ι S s ≫ f ≫ (∑ j : τ, biproduct.π T j ≫ biproduct.ι T j) ≫ inv f ≫ biproduct.π S s = 0
Tactic: rw [← Category.id_comp (inv f), Category.assoc, ← biproduct.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
σ τ : Type
inst_2 : Finite τ
S : σ → C
inst_3 : HasBiproduct.{0, v, u} S
T : τ → C
inst_4 : HasBiproduct.{0, v, u} T
s : σ
f : biproduct.{0, v, u} S ⟶ biproduct.{0, v, u} T
inst_5 : IsIso f
val : Fintype τ
z : ∀ (t : τ), biproduct.ι S s ≫ f ≫ biproduct.π T t = 0
reassoced : ∀ {t : τ} {W : C} (h : T t ⟶ W), biproduct.ι S s ≫ f ≫ biproduct.π T t ≫ h = 0 ≫ h
x : S s ⟶ S s := biproduct.ι S s ≫ f ≫ inv f ≫ biproduct.π S s
h₁ : x = 𝟙 (S s)
⊢ biproduct.ι S s ≫ f ≫ (∑ j : τ, biproduct.π T j ≫ biproduct.ι T j) ≫ inv f ≫ biproduct.π S s = 0
have simp : Eq (α := S s ⟶ S s) ((∑ j : τ, biproduct.ι S s ≫ f ≫ biproduct.π T j ≫ biproduct.ι T j) ≫ inv f ≫ biproduct.π S s) 0
Tactic: simp only [comp_sum_assoc]
-- 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
σ τ : Type
inst_2 : Finite τ
S : σ → C
inst_3 : HasBiproduct.{0, v, u} S
T : τ → C
inst_4 : HasBiproduct.{0, v, u} T
s : σ
f : biproduct.{0, v, u} S ⟶ biproduct.{0, v, u} T
inst_5 : IsIso f
val : Fintype τ
z : ∀ (t : τ), biproduct.ι S s ≫ f ≫ biproduct.π T t = 0
reassoced : ∀ {t : τ} {W : C} (h : T t ⟶ W), biproduct.ι S s ≫ f ≫ biproduct.π T t ≫ h = 0 ≫ h
x : S s ⟶ S s := biproduct.ι S s ≫ f ≫ inv f ≫ biproduct.π S s
h₁ : x = 𝟙 (S s)
⊢ Eq.{v + 1} (α := S s ⟶ S s) (𝟙 (S s)) 0
have h₀ : x = 0
Tactic: have h₀ : x = 0 := by
    dsimp [x]
    rw [← Category.id_comp (inv f), Category.assoc, ← biproduct.total]
    simp only [comp_sum_assoc]
    grind [CategoryTheory.Limits.zero_comp, Finset.sum_const_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
σ τ : Type
inst_2 : Fintype τ
S : σ → C
inst_3 : HasBiproduct.{0, v, u} S
T : τ → C
inst_4 : HasBiproduct.{0, v, u} T
s : σ
nz : Ne.{v + 1} (α := S s ⟶ S s) (𝟙 (S s)) 0
f : biproduct.{0, v, u} S ⟶ biproduct.{0, v, u} T
inst_5 : IsIso f
⊢ Trunc ((t : τ) ×' biproduct.ι S s ≫ f ≫ biproduct.π T t ≠ 0)
have h : ∃ (a : τ), biproduct.ι S s ≫ f ≫ biproduct.π T a ≠ 0
Tactic: apply truncSigmaOfExists
-- 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
σ τ : Type
inst_2 : Fintype τ
S : σ → C
inst_3 : HasBiproduct.{0, v, u} S
T : τ → C
inst_4 : HasBiproduct.{0, v, u} T
s : σ
nz : Ne.{v + 1} (α := S s ⟶ S s) (𝟙 (S s)) 0
f : biproduct.{0, v, u} S ⟶ biproduct.{0, v, u} T
inst_5 : IsIso f
⊢ ∃ (a : τ), biproduct.ι S s ≫ f ≫ biproduct.π T a ≠ 0
have t : (∀ (t : τ), biproduct.ι S s ≫ f ≫ biproduct.π T t = 0) → Eq.{v + 1} (α := S s ⟶ S s) (𝟙 (S s)) 0
Tactic: have t := Biproduct.column_nonzero_of_iso'.{v} s f
-- 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 : Fintype τ
S : σ → C
inst_3 : HasBiproduct.{0, v, u} S
T : τ → C
inst_4 : HasBiproduct.{0, v, u} T
s : σ
nz : Ne.{v + 1} (α := S s ⟶ S s) (𝟙 (S s)) 0
f : biproduct.{0, v, u} S ⟶ biproduct.{0, v, u} T
inst_5 : IsIso f
t : (∀ (t : τ), biproduct.ι S s ≫ f ≫ biproduct.π T t = 0) → Eq.{v + 1} (α := S s ⟶ S s) (𝟙 (S s)) 0
⊢ ∃ (a : τ), biproduct.ι S s ≫ f ≫ biproduct.π T a ≠ 0
have h : ∀ (h : ¬∃ (a : τ), biproduct.ι S s ≫ f ≫ biproduct.π T a ≠ 0), False
Tactic: by_contra h
-- 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
σ τ : Type
inst_2 : Fintype τ
S : σ → C
inst_3 : HasBiproduct.{0, v, u} S
T : τ → C
inst_4 : HasBiproduct.{0, v, u} T
s : σ
nz : Ne.{v + 1} (α := S s ⟶ S s) (𝟙 (S s)) 0
f : biproduct.{0, v, u} S ⟶ biproduct.{0, v, u} T
inst_5 : IsIso f
t : (∀ (t : τ), biproduct.ι S s ≫ f ≫ biproduct.π T t = 0) → Eq.{v + 1} (α := S s ⟶ S s) (𝟙 (S s)) 0
h : ¬∃ (a : τ), biproduct.ι S s ≫ f ≫ biproduct.π T a ≠ 0
⊢ False
have h₁ : ∀ (x : τ), biproduct.ι S s ≫ f ≫ biproduct.π T x = 0
Tactic: simp only [not_exists_not] at h
Cleared hypotheses: 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
σ τ : Type
inst_2 : Fintype τ
S : σ → C
inst_3 : HasBiproduct.{0, v, u} S
T : τ → C
inst_4 : HasBiproduct.{0, v, u} T
s : σ
nz : Ne.{v + 1} (α := S s ⟶ S s) (𝟙 (S s)) 0
f : biproduct.{0, v, u} S ⟶ biproduct.{0, v, u} T
inst_5 : IsIso f
⊢ Trunc ((t : τ) ×' biproduct.ι S s ≫ f ≫ biproduct.π T t ≠ 0)
have h : ∃ (a : τ), biproduct.ι S s ≫ f ≫ biproduct.π T a ≠ 0
Tactic: classical
    apply truncSigmaOfExists
    have t := Biproduct.column_nonzero_of_iso'.{v} s f
    by_contra h
    simp only [not_exists_not] at h
    exact nz (t 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
σ τ : Type
inst_2 : Fintype τ
S : σ → C
inst_3 : HasBiproduct.{0, v, u} S
T : τ → C
inst_4 : HasBiproduct.{0, v, u} T
s : σ
nz : Ne.{v + 1} (α := S s ⟶ S s) (𝟙 (S s)) 0
f : biproduct.{0, v, u} S ⟶ biproduct.{0, v, u} T
inst_5 : IsIso f
h : ∃ (a : τ), biproduct.ι S s ≫ f ≫ biproduct.π T a ≠ 0
⊢ Trunc ((t : τ) ×' biproduct.ι S s ≫ f ≫ biproduct.π T t ≠ 0)
have h₁ : ∀ (t : (∀ (t : τ), biproduct.ι S s ≫ f ≫ biproduct.π T t = 0) → Eq.{v + 1} (α := S s ⟶ S s) (𝟙 (S s)) 0),
  ∃ (a : τ), biproduct.ι S s ≫ f ≫ biproduct.π T a ≠ 0
Tactic: classical
    apply truncSigmaOfExists
    have t := Biproduct.column_nonzero_of_iso'.{v} s f
    by_contra h
    simp only [not_exists_not] at h
    exact nz (t 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
σ τ : Type
inst_2 : Fintype τ
S : σ → C
inst_3 : HasBiproduct.{0, v, u} S
T : τ → C
inst_4 : HasBiproduct.{0, v, u} T
s : σ
nz : Ne.{v + 1} (α := S s ⟶ S s) (𝟙 (S s)) 0
f : biproduct.{0, v, u} S ⟶ biproduct.{0, v, u} T
inst_5 : IsIso f
h : ∃ (a : τ), biproduct.ι S s ≫ f ≫ biproduct.π T a ≠ 0
h₁ :
  ∀ (t : (∀ (t : τ), biproduct.ι S s ≫ f ≫ biproduct.π T t = 0) → Eq.{v + 1} (α := S s ⟶ S s) (𝟙 (S s)) 0),
    ∃ (a : τ), biproduct.ι S s ≫ f ≫ biproduct.π T a ≠ 0
⊢ Trunc ((t : τ) ×' biproduct.ι S s ≫ f ≫ biproduct.π T t ≠ 0)
have h₂ : ∀ (t : (∀ (t : τ), biproduct.ι S s ≫ f ≫ biproduct.π T t = 0) → Eq.{v + 1} (α := S s ⟶ S s) (𝟙 (S s)) 0)
  (h : ¬∃ (a : τ), biproduct.ι S s ≫ f ≫ biproduct.π T a ≠ 0), False
Tactic: classical
    apply truncSigmaOfExists
    have t := Biproduct.column_nonzero_of_iso'.{v} s f
    by_contra h
    simp only [not_exists_not] at h
    exact nz (t 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
σ τ : Type
inst_2 : Fintype τ
S : σ → C
inst_3 : HasBiproduct.{0, v, u} S
T : τ → C
inst_4 : HasBiproduct.{0, v, u} T
s : σ
nz : Ne.{v + 1} (α := S s ⟶ S s) (𝟙 (S s)) 0
f : biproduct.{0, v, u} S ⟶ biproduct.{0, v, u} T
inst_5 : IsIso f
h : ∃ (a : τ), biproduct.ι S s ≫ f ≫ biproduct.π T a ≠ 0
h₁ :
  ∀ (t : (∀ (t : τ), biproduct.ι S s ≫ f ≫ biproduct.π T t = 0) → Eq.{v + 1} (α := S s ⟶ S s) (𝟙 (S s)) 0),
    ∃ (a : τ), biproduct.ι S s ≫ f ≫ biproduct.π T a ≠ 0
h₂ :
  ∀ (t : (∀ (t : τ), biproduct.ι S s ≫ f ≫ biproduct.π T t = 0) → Eq.{v + 1} (α := S s ⟶ S s) (𝟙 (S s)) 0)
    (h : ¬∃ (a : τ), biproduct.ι S s ≫ f ≫ biproduct.π T a ≠ 0), False
⊢ Trunc ((t : τ) ×' biproduct.ι S s ≫ f ≫ biproduct.π T t ≠ 0)
have h₃ : ∀ (t : (∀ (t : τ), biproduct.ι S s ≫ f ≫ biproduct.π T t = 0) → Eq.{v + 1} (α := S s ⟶ S s) (𝟙 (S s)) 0)
  (h : ∀ (x : τ), biproduct.ι S s ≫ f ≫ biproduct.π T x = 0), False
Tactic: classical
    apply truncSigmaOfExists
    have t := Biproduct.column_nonzero_of_iso'.{v} s f
    by_contra h
    simp only [not_exists_not] at h
    exact nz (t 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
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.PreservesZeroMorphisms
J : Type u_1
inst_5 : Finite J
f : J → C
inst_6 : HasBiproduct.{u_1, v, u} f
inst_7 : HasBiproduct.{u_1, v', u'} (F.obj ∘ f)
inst_8 :
  Mono (X := F.obj (biproduct.{u_1, v, u} f)) (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)
⊢ HasProduct.{u_1, v', u'} (C := D) fun (b : J) ↦ F.obj (f b)
have change : HasProduct.{u_1, v', u'} (F.obj ∘ f)
Tactic: change HasProduct (F.obj ∘ f)
-- 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
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.PreservesZeroMorphisms
J : Type u_1
inst_5 : Finite J
f : J → C
inst_6 : HasBiproduct.{u_1, v, u} f
inst_7 : HasBiproduct.{u_1, v', u'} (F.obj ∘ f)
inst_8 :
  Mono (X := F.obj (biproduct.{u_1, v, u} f)) (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)
⊢ PreservesBiproduct f F
have this : HasProduct.{u_1, v', u'} (C := D) fun (b : J) ↦ F.obj (f b)
Tactic: haveI : HasProduct fun b => F.obj (f b) := by
    change HasProduct (F.obj ∘ f)
    infer_instance
-- 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
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.PreservesZeroMorphisms
J : Type u_1
inst_5 : Finite J
f : J → C
inst_6 : HasBiproduct.{u_1, v, u} f
inst_7 : HasBiproduct.{u_1, v', u'} (F.obj ∘ f)
inst_8 :
  Mono (X := F.obj (biproduct.{u_1, v, u} f)) (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)
this : HasProduct.{u_1, v', u'} (C := D) fun (b : J) ↦ F.obj (f b)
⊢ Eq (α := F.obj (piObj.{u_1, v, u} f) ⟶ piObj.{u_1, v', u'} fun (b : J) ↦ F.obj (f b))
    (piComparison F f : F.obj (piObj.{u_1, v, u} f) ⟶ piObj.{u_1, v', u'} fun (b : J) ↦ F.obj (f b))
    (CategoryStruct.comp (Y := F.obj (biproduct.{u_1, v, u} f)) (Iso.inv (F.mapIso (biproduct.isoProduct f)))
        (CategoryStruct.comp (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)
          (Iso.hom (biproduct.isoProduct (F.obj ∘ f)))) :
      F.obj (piObj.{u_1, v, u} f) ⟶ piObj.{u_1, v', u'} (F.obj ∘ f))
have h : ∀ (j : J),
  Eq (α := F.obj (piObj.{u_1, v, u} f) ⟶ F.obj (f j))
    (CategoryStruct.comp (Y := piObj.{u_1, v', u'} fun (b : J) ↦ F.obj (f b)) (piComparison F f)
        (Pi.π (fun (b : J) ↦ F.obj (f b)) j) :
      F.obj (piObj.{u_1, v, u} f) ⟶ F.obj (f j))
    (CategoryStruct.comp (Y := piObj.{u_1, v', u'} fun (b : J) ↦ F.obj (f b))
        (CategoryStruct.comp (Y := F.obj (biproduct.{u_1, v, u} f)) (Iso.inv (F.mapIso (biproduct.isoProduct f)))
            (CategoryStruct.comp (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)
              (Iso.hom (biproduct.isoProduct (F.obj ∘ f)))) :
          F.obj (piObj.{u_1, v, u} f) ⟶ piObj.{u_1, v', u'} (F.obj ∘ f))
        (Pi.π (fun (b : J) ↦ F.obj (f b)) j : (piObj.{u_1, v', u'} fun (b : J) ↦ F.obj (f b)) ⟶ F.obj (f j)) :
      F.obj (piObj.{u_1, v, u} f) ⟶ F.obj (f j))
Tactic: ext 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
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.PreservesZeroMorphisms
J : Type u_1
inst_5 : Finite J
f : J → C
inst_6 : HasBiproduct.{u_1, v, u} f
inst_7 : HasBiproduct.{u_1, v', u'} (F.obj ∘ f)
inst_8 :
  Mono (X := F.obj (biproduct.{u_1, v, u} f)) (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)
this : HasProduct.{u_1, v', u'} (C := D) fun (b : J) ↦ F.obj (f b)
j : J
⊢ Eq (α := F.obj (piObj.{u_1, v, u} f) ⟶ F.obj (f j))
    (CategoryStruct.comp (Y := piObj.{u_1, v', u'} fun (b : J) ↦ F.obj (f b)) (piComparison F f)
        (Pi.π (fun (b : J) ↦ F.obj (f b)) j) :
      F.obj (piObj.{u_1, v, u} f) ⟶ F.obj (f j))
    (CategoryStruct.comp (Y := piObj.{u_1, v', u'} fun (b : J) ↦ F.obj (f b))
        (CategoryStruct.comp (Y := F.obj (biproduct.{u_1, v, u} f)) (Iso.inv (F.mapIso (biproduct.isoProduct f)))
            (CategoryStruct.comp (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)
              (Iso.hom (biproduct.isoProduct (F.obj ∘ f)))) :
          F.obj (piObj.{u_1, v, u} f) ⟶ piObj.{u_1, v', u'} (F.obj ∘ f))
        (Pi.π (fun (b : J) ↦ F.obj (f b)) j : (piObj.{u_1, v', u'} fun (b : J) ↦ F.obj (f b)) ⟶ F.obj (f j)) :
      F.obj (piObj.{u_1, v, u} f) ⟶ F.obj (f j))
have h : Eq (α := F.obj (piObj.{u_1, v, u} f) ⟶ F.obj (f j))
  (CategoryStruct.comp (Y := piObj.{u_1, v', u'} fun (b : J) ↦ F.obj (f b))
      (CategoryStruct.comp (Y := F.obj (biproduct.{u_1, v, u} f)) (Iso.inv (F.mapIso (biproduct.isoProduct f)))
          (CategoryStruct.comp (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)
            (Iso.hom (biproduct.isoProduct (F.obj ∘ f)))) :
        F.obj (piObj.{u_1, v, u} f) ⟶ piObj.{u_1, v', u'} (F.obj ∘ f))
      (Pi.π (fun (b : J) ↦ F.obj (f b)) j : (piObj.{u_1, v', u'} fun (b : J) ↦ F.obj (f b)) ⟶ F.obj (f j)) :
    F.obj (piObj.{u_1, v, u} f) ⟶ F.obj (f j))
  (F.map (Pi.π f j) : F.obj (piObj.{u_1, v, u} f) ⟶ F.obj (f j))
Tactic: convert! piComparison_comp_π F f 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
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.PreservesZeroMorphisms
J : Type u_1
inst_5 : Finite J
f : J → C
inst_6 : HasBiproduct.{u_1, v, u} f
inst_7 : HasBiproduct.{u_1, v', u'} (F.obj ∘ f)
inst_8 :
  Mono (X := F.obj (biproduct.{u_1, v, u} f)) (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)
this : HasProduct.{u_1, v', u'} (C := D) fun (b : J) ↦ F.obj (f b)
⊢ PreservesBiproduct f F
have that : Eq (α := F.obj (piObj.{u_1, v, u} f) ⟶ piObj.{u_1, v', u'} fun (b : J) ↦ F.obj (f b))
  (piComparison F f : F.obj (piObj.{u_1, v, u} f) ⟶ piObj.{u_1, v', u'} fun (b : J) ↦ F.obj (f b))
  (CategoryStruct.comp (Y := F.obj (biproduct.{u_1, v, u} f)) (Iso.inv (F.mapIso (biproduct.isoProduct f)))
      (CategoryStruct.comp (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)
        (Iso.hom (biproduct.isoProduct (F.obj ∘ f)))) :
    F.obj (piObj.{u_1, v, u} f) ⟶ piObj.{u_1, v', u'} (F.obj ∘ f))
Tactic: have that : piComparison F f =
      (F.mapIso (biproduct.isoProduct f)).inv ≫
        biproductComparison F f ≫ (biproduct.isoProduct _).hom := by
    ext j
    convert! piComparison_comp_π F f j; simp [← Function.comp_def, ← Functor.map_comp]
-- 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
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.PreservesZeroMorphisms
J : Type u_1
inst_5 : Finite J
f : J → C
inst_6 : HasBiproduct.{u_1, v, u} f
inst_7 : HasBiproduct.{u_1, v', u'} (F.obj ∘ f)
inst_8 :
  Mono (X := F.obj (biproduct.{u_1, v, u} f)) (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)
this : HasProduct.{u_1, v', u'} (C := D) fun (b : J) ↦ F.obj (f b)
that :
  Eq (α := F.obj (piObj.{u_1, v, u} f) ⟶ piObj.{u_1, v', u'} fun (b : J) ↦ F.obj (f b))
    (piComparison F f : F.obj (piObj.{u_1, v, u} f) ⟶ piObj.{u_1, v', u'} fun (b : J) ↦ F.obj (f b))
    (CategoryStruct.comp (Y := F.obj (biproduct.{u_1, v, u} f)) (Iso.inv (F.mapIso (biproduct.isoProduct f)))
        (CategoryStruct.comp (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)
          (Iso.hom (biproduct.isoProduct (F.obj ∘ f)))) :
      F.obj (piObj.{u_1, v, u} f) ⟶ piObj.{u_1, v', u'} (F.obj ∘ f))
⊢ PreservesBiproduct f F
have this₁ : IsIso (X := F.obj (biproduct.{u_1, v, u} f)) (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)
Tactic: haveI : IsIso (biproductComparison F f) := isIso_of_mono_of_isSplitEpi _
-- 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
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.PreservesZeroMorphisms
J : Type u_1
inst_5 : Finite J
f : J → C
inst_6 : HasBiproduct.{u_1, v, u} f
inst_7 : HasBiproduct.{u_1, v', u'} (F.obj ∘ f)
inst_8 :
  Mono (X := F.obj (biproduct.{u_1, v, u} f)) (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)
this_1 : HasProduct.{u_1, v', u'} (C := D) fun (b : J) ↦ F.obj (f b)
that :
  Eq (α := F.obj (piObj.{u_1, v, u} f) ⟶ piObj.{u_1, v', u'} fun (b : J) ↦ F.obj (f b))
    (piComparison F f : F.obj (piObj.{u_1, v, u} f) ⟶ piObj.{u_1, v', u'} fun (b : J) ↦ F.obj (f b))
    (CategoryStruct.comp (Y := F.obj (biproduct.{u_1, v, u} f)) (Iso.inv (F.mapIso (biproduct.isoProduct f)))
        (CategoryStruct.comp (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)
          (Iso.hom (biproduct.isoProduct (F.obj ∘ f)))) :
      F.obj (piObj.{u_1, v, u} f) ⟶ piObj.{u_1, v', u'} (F.obj ∘ f))
this : IsIso (X := F.obj (biproduct.{u_1, v, u} f)) (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)
⊢ IsIso (X := F.obj (piObj.{u_1, v, u} f)) (Y := piObj.{u_1, v', u'} fun (b : J) ↦ F.obj (f b)) (piComparison F f)
have rw : IsIso (X := F.obj (piObj.{u_1, v, u} f)) (Y := piObj.{u_1, v', u'} fun (b : J) ↦ F.obj (f b))
  (CategoryStruct.comp (Y := F.obj (biproduct.{u_1, v, u} f)) (Iso.inv (F.mapIso (biproduct.isoProduct f)))
      (CategoryStruct.comp (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)
        (Iso.hom (biproduct.isoProduct (F.obj ∘ f)))) :
    F.obj (piObj.{u_1, v, u} f) ⟶ piObj.{u_1, v', u'} (F.obj ∘ f))
Tactic: rw [that]