awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J_1 → C_1
J : Type w
K_1 : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
K : Type
inst_6 : Finite K
inst_7 : HasFiniteBiproducts.{v, u} C
f : K → C
p : K → Prop
W : C
g' : biproduct.{0, v, u} f ⟶ W
w : Eq (α := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f) ⟶ W) (biproduct.fromSubtype f p ≫ g') 0
j : K
⊢ (if (p j)ᶜ then 𝟙 (f j) else 0) ≫ biproduct.ι f j ≫ g' = biproduct.ι f j ≫ g'
have pos : ∀ (h : (p j)ᶜ), 𝟙 (f j) ≫ biproduct.ι f j ≫ g' = biproduct.ι f j ≫ g'
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J_1 → C_1
J : Type w
K_1 : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
K : Type
inst_6 : Finite K
inst_7 : HasFiniteBiproducts.{v, u} C
f : K → C
p : K → Prop
W : C
g' : biproduct.{0, v, u} f ⟶ W
w : Eq (α := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f) ⟶ W) (biproduct.fromSubtype f p ≫ g') 0
j : K
pos : ∀ (h : (p j)ᶜ), 𝟙 (f j) ≫ biproduct.ι f j ≫ g' = biproduct.ι f j ≫ g'
⊢ (if (p j)ᶜ then 𝟙 (f j) else 0) ≫ biproduct.ι f j ≫ g' = biproduct.ι f j ≫ g'
have neg : ∀ (h : ¬(p j)ᶜ), 0 ≫ biproduct.ι f j ≫ g' = biproduct.ι f j ≫ g'
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (hypothesis)
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J_1 → C_1
J : Type w
K_1 : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
K : Type
inst_6 : Finite K
inst_7 : HasFiniteBiproducts.{v, u} C
f : K → C
p : K → Prop
W : C
g' : biproduct.{0, v, u} f ⟶ W
w : Eq (α := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f) ⟶ W) (biproduct.fromSubtype f p ≫ g') 0
j : K
h : ¬(p j)ᶜ
⊢ 0 ≫ biproduct.ι f j ≫ g' = biproduct.ι f j ≫ g'
have w₁ : Eq (α := Subtype.restrict (β := fun (x : K) ↦ C) p f (Subtype.mk (p := p) j sorry) ⟶ W)
  (CategoryStruct.comp (Y := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f))
    (biproduct.ι (Subtype.restrict (β := fun (x : K) ↦ C) p f) (Subtype.mk (p := p) j sorry))
    (biproduct.fromSubtype f p ≫ g'))
  (CategoryStruct.comp (Y := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f))
    (biproduct.ι (Subtype.restrict (β := fun (x : K) ↦ C) p f) (Subtype.mk (p := p) j sorry)) 0)
Tactic: replace w := biproduct.ι _ (⟨j, not_not.mp h⟩ : Subtype p) ≫= w
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J_1 → C_1
J : Type w
K_1 : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
K : Type
inst_6 : Finite K
inst_7 : HasFiniteBiproducts.{v, u} C
f : K → C
p : K → Prop
intro intro₁ intro₂ :
  ∀ {W : C} (g' : biproduct.{0, v, u} f ⟶ W)
    (w :
      Eq (α := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f) ⟶ W) (biproduct.fromSubtype f p ≫ g')
        0),
    CategoryStruct.comp (Y := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f))
        (biproduct.toSubtype f pᶜ)
        ((fun {x : C} (g : biproduct.{0, v, u} f ⟶ x)
              (x_1 :
                Eq (α := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f) ⟶ x)
                  (biproduct.fromSubtype f p ≫ g) 0) ↦
            (biproduct.fromSubtype f pᶜ ≫ g : biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f) ⟶ x))
          g' w) =
      g'
⊢ ∀ {Z' : C} (g' : biproduct.{0, v, u} f ⟶ Z')
    (eq' :
      Eq (α := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f) ⟶ Z') (biproduct.fromSubtype f p ≫ g')
        0),
    CategoryStruct.comp (Y := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f))
        (biproduct.toSubtype f pᶜ)
        ((fun {x : C} (g : biproduct.{0, v, u} f ⟶ x)
              (x_1 :
                Eq (α := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f) ⟶ x)
                  (biproduct.fromSubtype f p ≫ g) 0) ↦
            (biproduct.fromSubtype f pᶜ ≫ g : biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f) ⟶ x))
          g' eq') =
      g'
have w : ∀ {W : C} (g' : biproduct.{0, v, u} f ⟶ W)
  (w :
    Eq (α := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f) ⟶ W) (biproduct.fromSubtype f p ≫ g') 0)
  (j : K),
  CategoryStruct.comp (Y := biproduct.{0, v, u} f) (biproduct.ι f j)
      (CategoryStruct.comp (Y := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f))
        (biproduct.toSubtype f pᶜ)
        ((fun {x : C} (g : biproduct.{0, v, u} f ⟶ x)
              (x_1 :
                Eq (α := biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) p f) ⟶ x)
                  (biproduct.fromSubtype f p ≫ g) 0) ↦
            (biproduct.fromSubtype f pᶜ ≫ g : biproduct.{0, v, u} (Subtype.restrict (β := fun (x : K) ↦ C) pᶜ f) ⟶ x))
          g' w)) =
    biproduct.ι f j ≫ g'
Tactic: classical
        intro W g' w
        ext j
        simp only [biproduct.toSubtype_fromSubtype_assoc, Pi.compl_apply, biproduct.ι_map_assoc]
        split_ifs with h
        · simp
        · replace w := biproduct.ι _ (⟨j, not_not.mp h⟩ : Subtype p) ≫= w
          simpa using w.symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J : Type
inst : Finite J
K : Type
inst_1 : Finite K
C : Type u
inst_2 : Category.{v, u} C
inst_3 : HasZeroMorphisms.{v, u} C
inst_4 : HasFiniteBiproducts.{v, u} C
f : J → C
g : K → C
m : (j : J) → (k : K) → f j ⟶ g k
k : K
⊢ Eq (α := biproduct.{0, v, u} f ⟶ g k)
    (CategoryStruct.comp (Y := biproduct.{0, v, u} g) (matrix m : biproduct.{0, v, u} f ⟶ biproduct.{0, v, u} g)
        (π g k : biproduct.{0, v, u} g ⟶ g k) :
      biproduct.{0, v, u} f ⟶ g k)
    (desc fun (j : J) ↦ m j k : biproduct.{0, v, u} f ⟶ g k)
have w : ∀ (j : J),
  CategoryStruct.comp (Y := biproduct.{0, v, u} f) (ι f j : f j ⟶ biproduct.{0, v, u} f)
      (CategoryStruct.comp (Y := biproduct.{0, v, u} g) (matrix m : biproduct.{0, v, u} f ⟶ biproduct.{0, v, u} g)
          (π g k : biproduct.{0, v, u} g ⟶ g k) :
        biproduct.{0, v, u} f ⟶ g k) =
    CategoryStruct.comp (Y := biproduct.{0, v, u} f) (ι f j) (desc fun (j : J) ↦ m j k)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J : Type
inst : Finite J
K : Type
inst_1 : Finite K
C : Type u
inst_2 : Category.{v, u} C
inst_3 : HasZeroMorphisms.{v, u} C
inst_4 : HasFiniteBiproducts.{v, u} C
f : J → C
g : K → C
m : biproduct.{0, v, u} f ⟶ biproduct.{0, v, u} g
⊢ (matrix fun (j : J) (k : K) ↦ components m j k) = m
have w : ∀ (j : K) (j_1 : J),
  CategoryStruct.comp (Y := biproduct.{0, v, u} f) (ι f j_1 : f j_1 ⟶ biproduct.{0, v, u} f)
      (CategoryStruct.comp (Y := biproduct.{0, v, u} g)
          (matrix fun (j : J) (k : K) ↦ components m j k : biproduct.{0, v, u} f ⟶ biproduct.{0, v, u} g)
          (π g j : biproduct.{0, v, u} g ⟶ g j) :
        biproduct.{0, v, u} f ⟶ g j) =
    ι f j_1 ≫ m ≫ π g j
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J_1 → C_1
J_2 : Type w
K_1 : Type u_1
C_2 : Type u
inst_4 : Category.{v, u} C_2
inst_5 : HasZeroMorphisms.{v, u} C_2
J : Type
inst_6 : Finite J
K : Type
inst_7 : Finite K
C : Type u
inst_8 : Category.{v, u} C
inst_9 : HasZeroMorphisms.{v, u} C
inst_10 : HasFiniteBiproducts.{v, u} C
f : J → C
g : K → C
m : (j : J) → (k : K) → f j ⟶ g k
⊢ components (matrix m) = m
have h : ∀ (x : J) (x_1 : K), components (matrix m) x x_1 = m x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f : J → C
inst_2 : HasBiproduct.{w, v, u} f
b : Bicone.{w, v, u} f
hb : b.IsBilimit
⊢ Eq (α := Cone.pt.{w, v, w, u} (Bicone.toCone (bicone f)) ⟶ b.toCone.pt)
    (Iso.inv (hb.isLimit.conePointUniqueUpToIso (isLimit f))) (desc b.ι)
have refine : ∀ (j : J) (j' : Discrete J),
  CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (Iso.inv (hb.isLimit.conePointUniqueUpToIso (isLimit f))) ≫
      b.toCone.π.app j' =
    CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (desc b.ι) ≫ b.toCone.π.app j'
Tactic: refine biproduct.hom_ext' _ _ fun j => hb.isLimit.hom_ext fun j' => ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f : J → C
inst_2 : HasBiproduct.{w, v, u} f
b : Bicone.{w, v, u} f
hb : b.IsBilimit
j : J
j' : Discrete J
⊢ CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (Iso.inv (hb.isLimit.conePointUniqueUpToIso (isLimit f))) ≫
      b.toCone.π.app j' =
    CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (desc b.ι) ≫ b.toCone.π.app j'
have rw : CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j)
    (Iso.inv (hb.isLimit.conePointUniqueUpToIso (isLimit f)) ≫ b.toCone.π.app j') =
  CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (desc b.ι) ≫ b.toCone.π.app j'
Tactic: rw [Category.assoc, IsLimit.conePointUniqueUpToIso_inv_comp, Bicone.toCone_π_app,
    biproduct.bicone_π, biproduct.ι_desc, biproduct.ι_π, b.toCone_π_app, b.ι_π]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f : J → C
inst_2 : HasBiproduct.{w, v, u} f
b : Bicone.{w, v, u} f
hb : b.IsBilimit
j : J
j' : Discrete J
rw :
  CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j)
      (Iso.inv (hb.isLimit.conePointUniqueUpToIso (isLimit f)) ≫ b.toCone.π.app j') =
    CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (desc b.ι) ≫ b.toCone.π.app j'
⊢ CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (Iso.inv (hb.isLimit.conePointUniqueUpToIso (isLimit f))) ≫
      b.toCone.π.app j' =
    CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (desc b.ι) ≫ b.toCone.π.app j'
have rw₁ : CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (NatTrans.app (Cone.π (Bicone.toCone (bicone f))) j') =
  CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (desc b.ι) ≫ b.toCone.π.app j'
Tactic: rw [Category.assoc, IsLimit.conePointUniqueUpToIso_inv_comp, Bicone.toCone_π_app,
    biproduct.bicone_π, biproduct.ι_desc, biproduct.ι_π, b.toCone_π_app, b.ι_π]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f : J → C
inst_2 : HasBiproduct.{w, v, u} f
b : Bicone.{w, v, u} f
hb : b.IsBilimit
j : J
j' : Discrete J
rw :
  CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j)
      (Iso.inv (hb.isLimit.conePointUniqueUpToIso (isLimit f)) ≫ b.toCone.π.app j') =
    CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (desc b.ι) ≫ b.toCone.π.app j'
rw₁ :
  CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (NatTrans.app (Cone.π (Bicone.toCone (bicone f))) j') =
    CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (desc b.ι) ≫ b.toCone.π.app j'
⊢ CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (Iso.inv (hb.isLimit.conePointUniqueUpToIso (isLimit f))) ≫
      b.toCone.π.app j' =
    CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (desc b.ι) ≫ b.toCone.π.app j'
have rw₂ : CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (Bicone.π (bicone f) j'.as) =
  CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (desc b.ι) ≫ b.toCone.π.app j'
Tactic: rw [Category.assoc, IsLimit.conePointUniqueUpToIso_inv_comp, Bicone.toCone_π_app,
    biproduct.bicone_π, biproduct.ι_desc, biproduct.ι_π, b.toCone_π_app, b.ι_π]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f : J → C
inst_2 : HasBiproduct.{w, v, u} f
b : Bicone.{w, v, u} f
hb : b.IsBilimit
j : J
j' : Discrete J
rw :
  CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j)
      (Iso.inv (hb.isLimit.conePointUniqueUpToIso (isLimit f)) ≫ b.toCone.π.app j') =
    CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (desc b.ι) ≫ b.toCone.π.app j'
rw₁ :
  CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (NatTrans.app (Cone.π (Bicone.toCone (bicone f))) j') =
    CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (desc b.ι) ≫ b.toCone.π.app j'
rw₂ :
  CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (Bicone.π (bicone f) j'.as) =
    CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (desc b.ι) ≫ b.toCone.π.app j'
⊢ CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (Iso.inv (hb.isLimit.conePointUniqueUpToIso (isLimit f))) ≫
      b.toCone.π.app j' =
    CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (desc b.ι) ≫ b.toCone.π.app j'
have rw₃ : CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (π f j'.as) =
  CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (desc b.ι) ≫ b.toCone.π.app j'
Tactic: rw [Category.assoc, IsLimit.conePointUniqueUpToIso_inv_comp, Bicone.toCone_π_app,
    biproduct.bicone_π, biproduct.ι_desc, biproduct.ι_π, b.toCone_π_app, b.ι_π]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f : J → C
inst_2 : HasBiproduct.{w, v, u} f
b : Bicone.{w, v, u} f
hb : b.IsBilimit
j : J
j' : Discrete J
rw :
  CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j)
      (Iso.inv (hb.isLimit.conePointUniqueUpToIso (isLimit f)) ≫ b.toCone.π.app j') =
    CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (desc b.ι) ≫ b.toCone.π.app j'
rw₁ :
  CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (NatTrans.app (Cone.π (Bicone.toCone (bicone f))) j') =
    CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (desc b.ι) ≫ b.toCone.π.app j'
rw₂ :
  CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (Bicone.π (bicone f) j'.as) =
    CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (desc b.ι) ≫ b.toCone.π.app j'
rw₃ :
  CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (π f j'.as) =
    CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (desc b.ι) ≫ b.toCone.π.app j'
⊢ CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (Iso.inv (hb.isLimit.conePointUniqueUpToIso (isLimit f))) ≫
      b.toCone.π.app j' =
    CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (desc b.ι) ≫ b.toCone.π.app j'
have rw₄ : CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (π f j'.as) = b.ι j ≫ b.toCone.π.app j'
Tactic: rw [Category.assoc, IsLimit.conePointUniqueUpToIso_inv_comp, Bicone.toCone_π_app,
    biproduct.bicone_π, biproduct.ι_desc, biproduct.ι_π, b.toCone_π_app, b.ι_π]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f : J → C
inst_2 : HasBiproduct.{w, v, u} f
b : Bicone.{w, v, u} f
hb : b.IsBilimit
j : J
j' : Discrete J
rw :
  CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j)
      (Iso.inv (hb.isLimit.conePointUniqueUpToIso (isLimit f)) ≫ b.toCone.π.app j') =
    CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (desc b.ι) ≫ b.toCone.π.app j'
rw₁ :
  CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (NatTrans.app (Cone.π (Bicone.toCone (bicone f))) j') =
    CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (desc b.ι) ≫ b.toCone.π.app j'
rw₂ :
  CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (Bicone.π (bicone f) j'.as) =
    CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (desc b.ι) ≫ b.toCone.π.app j'
rw₃ :
  CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (π f j'.as) =
    CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (desc b.ι) ≫ b.toCone.π.app j'
rw₄ : CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (π f j'.as) = b.ι j ≫ b.toCone.π.app j'
⊢ CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (Iso.inv (hb.isLimit.conePointUniqueUpToIso (isLimit f))) ≫
      b.toCone.π.app j' =
    CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (desc b.ι) ≫ b.toCone.π.app j'
have rw₅ : (if h : j = j'.as then eqToHom sorry else 0) = b.ι j ≫ b.toCone.π.app j'
Tactic: rw [Category.assoc, IsLimit.conePointUniqueUpToIso_inv_comp, Bicone.toCone_π_app,
    biproduct.bicone_π, biproduct.ι_desc, biproduct.ι_π, b.toCone_π_app, b.ι_π]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f : J → C
inst_2 : HasBiproduct.{w, v, u} f
b : Bicone.{w, v, u} f
hb : b.IsBilimit
j : J
j' : Discrete J
rw :
  CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j)
      (Iso.inv (hb.isLimit.conePointUniqueUpToIso (isLimit f)) ≫ b.toCone.π.app j') =
    CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (desc b.ι) ≫ b.toCone.π.app j'
rw₁ :
  CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (NatTrans.app (Cone.π (Bicone.toCone (bicone f))) j') =
    CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (desc b.ι) ≫ b.toCone.π.app j'
rw₂ :
  CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (Bicone.π (bicone f) j'.as) =
    CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (desc b.ι) ≫ b.toCone.π.app j'
rw₃ :
  CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (π f j'.as) =
    CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (desc b.ι) ≫ b.toCone.π.app j'
rw₄ : CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (π f j'.as) = b.ι j ≫ b.toCone.π.app j'
rw₅ : (if h : j = j'.as then eqToHom ⋯ else 0) = b.ι j ≫ b.toCone.π.app j'
⊢ CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (Iso.inv (hb.isLimit.conePointUniqueUpToIso (isLimit f))) ≫
      b.toCone.π.app j' =
    CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (desc b.ι) ≫ b.toCone.π.app j'
have rw₆ : Eq (α := f j ⟶ obj.{w, v, w, u} (Discrete.functor f) j') (if h : j = j'.as then eqToHom sorry else 0) (b.ι j ≫ b.π j'.as)
Tactic: rw [Category.assoc, IsLimit.conePointUniqueUpToIso_inv_comp, Bicone.toCone_π_app,
    biproduct.bicone_π, biproduct.ι_desc, biproduct.ι_π, b.toCone_π_app, b.ι_π]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f : J → C
inst_2 : HasBiproduct.{w, v, u} f
b : Bicone.{w, v, u} f
hb : b.IsBilimit
j : J
j' : Discrete J
rw :
  CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j)
      (Iso.inv (hb.isLimit.conePointUniqueUpToIso (isLimit f)) ≫ b.toCone.π.app j') =
    CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (desc b.ι) ≫ b.toCone.π.app j'
rw₁ :
  CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (NatTrans.app (Cone.π (Bicone.toCone (bicone f))) j') =
    CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (desc b.ι) ≫ b.toCone.π.app j'
rw₂ :
  CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (Bicone.π (bicone f) j'.as) =
    CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (desc b.ι) ≫ b.toCone.π.app j'
rw₃ :
  CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (π f j'.as) =
    CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (desc b.ι) ≫ b.toCone.π.app j'
rw₄ : CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (π f j'.as) = b.ι j ≫ b.toCone.π.app j'
rw₅ : (if h : j = j'.as then eqToHom ⋯ else 0) = b.ι j ≫ b.toCone.π.app j'
rw₆ :
  Eq (α := f j ⟶ obj.{w, v, w, u} (Discrete.functor f) j') (if h : j = j'.as then eqToHom ⋯ else 0) (b.ι j ≫ b.π j'.as)
⊢ CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (Iso.inv (hb.isLimit.conePointUniqueUpToIso (isLimit f))) ≫
      b.toCone.π.app j' =
    CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (desc b.ι) ≫ b.toCone.π.app j'
have rw₇ : Eq.{v + 1} (α := f j ⟶ obj.{w, v, w, u} (Discrete.functor f) j') (if h : j = j'.as then eqToHom sorry else 0)
  (if h : j = j'.as then eqToHom sorry else 0)
Tactic: rw [Category.assoc, IsLimit.conePointUniqueUpToIso_inv_comp, Bicone.toCone_π_app,
    biproduct.bicone_π, biproduct.ι_desc, biproduct.ι_π, b.toCone_π_app, b.ι_π]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f : J → C
inst_2 : HasBiproduct.{w, v, u} f
b : Bicone.{w, v, u} f
hb : b.IsBilimit
⊢ Eq (α := Cone.pt.{w, v, w, u} (Bicone.toCone (bicone f)) ⟶ b.toCone.pt)
    (Iso.inv (hb.isLimit.conePointUniqueUpToIso (isLimit f))) (desc b.ι)
have refine : ∀ (j : J) (j' : Discrete J),
  CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (Iso.inv (hb.isLimit.conePointUniqueUpToIso (isLimit f))) ≫
      b.toCone.π.app j' =
    CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (desc b.ι) ≫ b.toCone.π.app j'
Tactic: classical
  refine biproduct.hom_ext' _ _ fun j => hb.isLimit.hom_ext fun j' => ?_
  rw [Category.assoc, IsLimit.conePointUniqueUpToIso_inv_comp, Bicone.toCone_π_app,
    biproduct.bicone_π, biproduct.ι_desc, biproduct.ι_π, b.toCone_π_app, b.ι_π]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D_1 : Type uD
inst_2 : Category.{uD', uD} D_1
inst_3 : HasZeroMorphisms.{uD', uD} D_1
F : J_1 → C_1
J_2 : Type w
K : Type u_1
C_2 : Type u
inst_4 : Category.{v, u} C_2
inst_5 : HasZeroMorphisms.{v, u} C_2
J : Type w
C : Type u
inst_6 : Category.{v, u} C
inst_7 : HasZeroMorphisms.{v, u} C
D : Type uD
inst_8 : Category.{uD', uD} D
inst_9 : HasZeroMorphisms.{uD', uD} D
f : J → C
inst_10 : HasBiproduct.{w, v, u} f
b : Bicone.{w, v, u} f
hb : b.IsBilimit
⊢ CategoryStruct.comp (Y := biproduct.{w, v, u} f) (lift b.π) (desc b.ι) = 𝟙 b.pt
have rw : CategoryStruct.comp (Y := biproduct.{w, v, u} f) (Iso.hom (hb.isLimit.conePointUniqueUpToIso (isLimit f))) (desc b.ι) =
  𝟙 b.pt
Tactic: rw [← biproduct.conePointUniqueUpToIso_hom f hb, ←
      biproduct.conePointUniqueUpToIso_inv f hb, Iso.hom_inv_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D_1 : Type uD
inst_2 : Category.{uD', uD} D_1
inst_3 : HasZeroMorphisms.{uD', uD} D_1
F : J_1 → C_1
J_2 : Type w
K : Type u_1
C_2 : Type u
inst_4 : Category.{v, u} C_2
inst_5 : HasZeroMorphisms.{v, u} C_2
J : Type w
C : Type u
inst_6 : Category.{v, u} C
inst_7 : HasZeroMorphisms.{v, u} C
D : Type uD
inst_8 : Category.{uD', uD} D
inst_9 : HasZeroMorphisms.{uD', uD} D
f : J → C
inst_10 : HasBiproduct.{w, v, u} f
b : Bicone.{w, v, u} f
hb : b.IsBilimit
rw :
  CategoryStruct.comp (Y := biproduct.{w, v, u} f) (Iso.hom (hb.isLimit.conePointUniqueUpToIso (isLimit f)))
      (desc b.ι) =
    𝟙 b.pt
⊢ CategoryStruct.comp (Y := biproduct.{w, v, u} f) (lift b.π) (desc b.ι) = 𝟙 b.pt
have rw₁ : CategoryStruct.comp (Y := biproduct.{w, v, u} f) (Iso.hom (hb.isLimit.conePointUniqueUpToIso (isLimit f)))
    (Iso.inv (hb.isLimit.conePointUniqueUpToIso (isLimit f))) =
  𝟙 b.pt
Tactic: rw [← biproduct.conePointUniqueUpToIso_hom f hb, ←
      biproduct.conePointUniqueUpToIso_inv f hb, Iso.hom_inv_id]