awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J : Type w
K : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g ((e : (a : J) → K) j) ≅ f j
inst_2 : HasBiproduct.{w, v, u} f
inst_3 : HasBiproduct.{u_1, v, u} g
k : K
j : J
h : ¬k = (e : (a : J) → K) j
neg : (w j).inv ≫ 0 = 0 ≫ Iso.inv (w ((e.symm : (a : K) → J) k)) ≫ eqToHom ⋯
neg₁ : j ≠ (e.symm : (a : K) → J) k
⊢ (w j).inv ≫ CategoryStruct.comp (Y := biproduct.{u_1, v, u} g) (ι g ((e : (a : J) → K) j)) (π g k) =
    CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j)
      (π f ((e.symm : (a : K) → J) k) ≫ Iso.inv (w ((e.symm : (a : K) → J) k)) ≫ eqToHom ⋯)
have neg₂ : (e : (a : J) → K) j ≠ k
Tactic: rw [biproduct.ι_π_ne, biproduct.ι_π_ne_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J : Type w
K : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g ((e : (a : J) → K) j) ≅ f j
inst_2 : HasBiproduct.{w, v, u} f
inst_3 : HasBiproduct.{u_1, v, u} g
⊢ Eq.{v + 1} (α := biproduct.{u_1, v, u} g ⟶ biproduct.{w, v, u} f)
    (desc fun (k : K) ↦ eqToHom ⋯ ≫ Iso.hom (w ((e.symm : (a : K) → J) k)) ≫ ι f ((e.symm : (a : K) → J) k))
    (lift fun (j : J) ↦ π g ((e : (a : J) → K) j) ≫ (w j).hom)
have w₁ : ∀ (j : J) (k : K),
  Eq.{v + 1} (α := g k ⟶ f j)
    (CategoryStruct.comp (Y := biproduct.{u_1, v, u} g) (ι g k)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} f)
        (desc fun (k : K) ↦ eqToHom sorry ≫ Iso.hom (w ((e.symm : (a : K) → J) k)) ≫ ι f ((e.symm : (a : K) → J) k))
        (π f j)))
    (CategoryStruct.comp (Y := biproduct.{u_1, v, u} g) (ι g k)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (lift fun (j : J) ↦ π g ((e : (a : J) → K) j) ≫ (w j).hom)
        (π f j)))
Tactic: ext j k
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J : Type w
K : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g ((e : (a : J) → K) j) ≅ f j
inst_2 : HasBiproduct.{w, v, u} f
inst_3 : HasBiproduct.{u_1, v, u} g
j : J
k : K
⊢ Eq.{v + 1} (α := g k ⟶ f j)
    (CategoryStruct.comp (Y := biproduct.{u_1, v, u} g) (ι g k)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} f)
        (desc fun (k : K) ↦ eqToHom ⋯ ≫ Iso.hom (w ((e.symm : (a : K) → J) k)) ≫ ι f ((e.symm : (a : K) → J) k))
        (π f j)))
    (CategoryStruct.comp (Y := biproduct.{u_1, v, u} g) (ι g k)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (lift fun (j : J) ↦ π g ((e : (a : J) → K) j) ≫ (w j).hom)
        (π f j)))
have pos : ∀ (h : k = (e : (a : J) → K) j),
  Eq.{v + 1} (α := g k ⟶ f j)
    (CategoryStruct.comp (Y := biproduct.{u_1, v, u} g) (ι g k)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} f)
        (desc fun (k : K) ↦ eqToHom sorry ≫ Iso.hom (w ((e.symm : (a : K) → J) k)) ≫ ι f ((e.symm : (a : K) → J) k))
        (π f j)))
    (CategoryStruct.comp (Y := biproduct.{u_1, v, u} g) (ι g k)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (lift fun (j : J) ↦ π g ((e : (a : J) → K) j) ≫ (w j).hom)
        (π f j)))
Tactic: by_cases h : k = e j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J : Type w
K : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g ((e : (a : J) → K) j) ≅ f j
inst_2 : HasBiproduct.{w, v, u} f
inst_3 : HasBiproduct.{u_1, v, u} g
j : J
k : K
pos :
  ∀ (h : k = (e : (a : J) → K) j),
    Eq.{v + 1} (α := g k ⟶ f j)
      (CategoryStruct.comp (Y := biproduct.{u_1, v, u} g) (ι g k)
        (CategoryStruct.comp (Y := biproduct.{w, v, u} f)
          (desc fun (k : K) ↦ eqToHom ⋯ ≫ Iso.hom (w ((e.symm : (a : K) → J) k)) ≫ ι f ((e.symm : (a : K) → J) k))
          (π f j)))
      (CategoryStruct.comp (Y := biproduct.{u_1, v, u} g) (ι g k)
        (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (lift fun (j : J) ↦ π g ((e : (a : J) → K) j) ≫ (w j).hom)
          (π f j)))
⊢ Eq.{v + 1} (α := g k ⟶ f j)
    (CategoryStruct.comp (Y := biproduct.{u_1, v, u} g) (ι g k)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} f)
        (desc fun (k : K) ↦ eqToHom ⋯ ≫ Iso.hom (w ((e.symm : (a : K) → J) k)) ≫ ι f ((e.symm : (a : K) → J) k))
        (π f j)))
    (CategoryStruct.comp (Y := biproduct.{u_1, v, u} g) (ι g k)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (lift fun (j : J) ↦ π g ((e : (a : J) → K) j) ≫ (w j).hom)
        (π f j)))
have neg : ∀ (h : ¬k = (e : (a : J) → K) j),
  Eq.{v + 1} (α := g k ⟶ f j)
    (CategoryStruct.comp (Y := biproduct.{u_1, v, u} g) (ι g k)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} f)
        (desc fun (k : K) ↦ eqToHom sorry ≫ Iso.hom (w ((e.symm : (a : K) → J) k)) ≫ ι f ((e.symm : (a : K) → J) k))
        (π f j)))
    (CategoryStruct.comp (Y := biproduct.{u_1, v, u} g) (ι g k)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (lift fun (j : J) ↦ π g ((e : (a : J) → K) j) ≫ (w j).hom)
        (π f j)))
Tactic: by_cases h : k = e j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J : Type w
K : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g ((e : (a : J) → K) j) ≅ f j
inst_2 : HasBiproduct.{w, v, u} f
inst_3 : HasBiproduct.{u_1, v, u} g
j : J
k : K
h : k = (e : (a : J) → K) j
⊢ Eq.{v + 1} (α := g k ⟶ f j)
    (CategoryStruct.comp (Y := biproduct.{u_1, v, u} g) (ι g k)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} f)
        (desc fun (k : K) ↦ eqToHom ⋯ ≫ Iso.hom (w ((e.symm : (a : K) → J) k)) ≫ ι f ((e.symm : (a : K) → J) k))
        (π f j)))
    (CategoryStruct.comp (Y := biproduct.{u_1, v, u} g) (ι g k)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (lift fun (j : J) ↦ π g ((e : (a : J) → K) j) ≫ (w j).hom)
        (π f j)))
have pos : Eq.{v + 1} (α := g ((e : (a : J) → K) j) ⟶ f j)
  (CategoryStruct.comp (Y := biproduct.{u_1, v, u} g) (ι g ((e : (a : J) → K) j))
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f)
      (desc fun (k : K) ↦ eqToHom sorry ≫ Iso.hom (w ((e.symm : (a : K) → J) k)) ≫ ι f ((e.symm : (a : K) → J) k)) (π f j)))
  (CategoryStruct.comp (Y := biproduct.{u_1, v, u} g) (ι g ((e : (a : J) → K) j))
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (lift fun (j : J) ↦ π g ((e : (a : J) → K) j) ≫ (w j).hom)
      (π f j)))
Tactic: subst h
Cleared hypotheses: k, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J : Type w
K : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g ((e : (a : J) → K) j) ≅ f j
inst_2 : HasBiproduct.{w, v, u} f
inst_3 : HasBiproduct.{u_1, v, u} g
j : J
k : K
h : ¬k = (e : (a : J) → K) j
⊢ Eq.{v + 1} (α := g k ⟶ f j)
    (CategoryStruct.comp (Y := biproduct.{u_1, v, u} g) (ι g k)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} f)
        (desc fun (k : K) ↦ eqToHom ⋯ ≫ Iso.hom (w ((e.symm : (a : K) → J) k)) ≫ ι f ((e.symm : (a : K) → J) k))
        (π f j)))
    (CategoryStruct.comp (Y := biproduct.{u_1, v, u} g) (ι g k)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (lift fun (j : J) ↦ π g ((e : (a : J) → K) j) ≫ (w j).hom)
        (π f j)))
have neg : eqToHom sorry ≫
    Iso.hom (w ((e.symm : (a : K) → J) k)) ≫
      CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f ((e.symm : (a : K) → J) k)) (π f j) =
  CategoryStruct.comp (Y := biproduct.{u_1, v, u} g) (ι g k) (π g ((e : (a : J) → K) j) ≫ (w j).hom)
Tactic: simp only [ι_desc_assoc, Category.assoc, lift_π]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J : Type w
K : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g ((e : (a : J) → K) j) ≅ f j
inst_2 : HasBiproduct.{w, v, u} f
inst_3 : HasBiproduct.{u_1, v, u} g
j : J
k : K
h : ¬k = (e : (a : J) → K) j
⊢ eqToHom ⋯ ≫
      Iso.hom (w ((e.symm : (a : K) → J) k)) ≫
        CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f ((e.symm : (a : K) → J) k)) (π f j) =
    CategoryStruct.comp (Y := biproduct.{u_1, v, u} g) (ι g k) (π g ((e : (a : J) → K) j) ≫ (w j).hom)
have neg : eqToHom sorry ≫ Iso.hom (w ((e.symm : (a : K) → J) k)) ≫ 0 = 0 ≫ (w j).hom
Tactic: rw [biproduct.ι_π_ne, biproduct.ι_π_ne_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J : Type w
K : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g ((e : (a : J) → K) j) ≅ f j
inst_2 : HasBiproduct.{w, v, u} f
inst_3 : HasBiproduct.{u_1, v, u} g
j : J
k : K
h : ¬k = (e : (a : J) → K) j
neg : eqToHom ⋯ ≫ Iso.hom (w ((e.symm : (a : K) → J) k)) ≫ 0 = 0 ≫ (w j).hom
⊢ eqToHom ⋯ ≫
      Iso.hom (w ((e.symm : (a : K) → J) k)) ≫
        CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f ((e.symm : (a : K) → J) k)) (π f j) =
    CategoryStruct.comp (Y := biproduct.{u_1, v, u} g) (ι g k) (π g ((e : (a : J) → K) j) ≫ (w j).hom)
have neg₁ : k ≠ (e : (a : J) → K) j
Tactic: rw [biproduct.ι_π_ne, biproduct.ι_π_ne_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J : Type w
K : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g ((e : (a : J) → K) j) ≅ f j
inst_2 : HasBiproduct.{w, v, u} f
inst_3 : HasBiproduct.{u_1, v, u} g
j : J
k : K
h : ¬k = (e : (a : J) → K) j
neg : eqToHom ⋯ ≫ Iso.hom (w ((e.symm : (a : K) → J) k)) ≫ 0 = 0 ≫ (w j).hom
neg₁ : k ≠ (e : (a : J) → K) j
⊢ eqToHom ⋯ ≫
      Iso.hom (w ((e.symm : (a : K) → J) k)) ≫
        CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f ((e.symm : (a : K) → J) k)) (π f j) =
    CategoryStruct.comp (Y := biproduct.{u_1, v, u} g) (ι g k) (π g ((e : (a : J) → K) j) ≫ (w j).hom)
have neg₂ : (e.symm : (a : K) → J) k ≠ j
Tactic: rw [biproduct.ι_π_ne, biproduct.ι_π_ne_assoc]
-- 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 : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
ι : Type u_3
f : ι → Type u_2
g : (i : ι) → f i → C
inst_6 : ∀ (i : ι), HasBiproduct.{u_2, v, u} (g i)
inst_7 : HasBiproduct.{u_3, v, u} (C := C) fun (i : ι) ↦ biproduct.{u_2, v, u} (g i)
x_1 x_2 : (i : ι) × f i
j : ι
x : f j
j' : ι
y : f j'
h : ¬Sigma.mk (β := fun (i : ι) ↦ f i) j x = Sigma.mk (β := fun (i : ι) ↦ f i) j' y
⊢ Eq.{v + 1} (α :=
    g ((Sigma.mk (β := fun (i : ι) ↦ f i) j x).fst (β := fun (i : ι) ↦ f i))
        ((Sigma.mk (β := fun (i : ι) ↦ f i) j x).snd (β := fun (i : ι) ↦ f i)) ⟶
      g ((Sigma.mk (β := fun (i : ι) ↦ f i) j' y).fst (β := fun (i : ι) ↦ f i))
        ((Sigma.mk (β := fun (i : ι) ↦ f i) j' y).snd (β := fun (i : ι) ↦ f i)))
    (CategoryStruct.comp (Y := biproduct.{u_3, v, u} fun (i : ι) ↦ biproduct.{u_2, v, u} (g i))
      (CategoryStruct.comp (Y :=
        biproduct.{u_2, v, u} (J := f ((Sigma.mk (β := fun (i : ι) ↦ f i) j x).fst (β := fun (i : ι) ↦ f i)))
          (g ((Sigma.mk (β := fun (i : ι) ↦ f i) j x).fst (β := fun (i : ι) ↦ f i))))
        (biproduct.ι (g ((Sigma.mk (β := fun (i : ι) ↦ f i) j x).fst (β := fun (i : ι) ↦ f i)))
          ((Sigma.mk (β := fun (i : ι) ↦ f i) j x).snd (β := fun (i : ι) ↦ f i)))
        (biproduct.ι.{u_3, v, u} (C := C) (fun (i : ι) ↦ biproduct.{u_2, v, u} (g i))
          ((Sigma.mk (β := fun (i : ι) ↦ f i) j x).fst (β := fun (i : ι) ↦ f i))))
      (biproduct.π (fun (i : ι) ↦ biproduct.{u_2, v, u} (g i))
          ((Sigma.mk (β := fun (i : ι) ↦ f i) j' y).fst (β := fun (i : ι) ↦ f i)) ≫
        biproduct.π (g ((Sigma.mk (β := fun (i : ι) ↦ f i) j' y).fst (β := fun (i : ι) ↦ f i)))
          ((Sigma.mk (β := fun (i : ι) ↦ f i) j' y).snd (β := fun (i : ι) ↦ f i))))
    0
have h₁ : j = j' → ¬x ≍ y
Tactic: simp only [Sigma.mk.inj_iff, not_and] at h
Cleared hypotheses: 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 : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
ι : Type u_3
f : ι → Type u_2
g : (i : ι) → f i → C
inst_6 : ∀ (i : ι), HasBiproduct.{u_2, v, u} (g i)
inst_7 : HasBiproduct.{u_3, v, u} (C := C) fun (i : ι) ↦ biproduct.{u_2, v, u} (g i)
x_1 x_2 : (i : ι) × f i
j : ι
x y : f j
h : j = j → ¬x ≍ y
⊢ Eq.{v + 1} (α :=
    g ((Sigma.mk (β := fun (i : ι) ↦ f i) j x).fst (β := fun (i : ι) ↦ f i))
        ((Sigma.mk (β := fun (i : ι) ↦ f i) j x).snd (β := fun (i : ι) ↦ f i)) ⟶
      g ((Sigma.mk (β := fun (i : ι) ↦ f i) j y).fst (β := fun (i : ι) ↦ f i))
        ((Sigma.mk (β := fun (i : ι) ↦ f i) j y).snd (β := fun (i : ι) ↦ f i)))
    (CategoryStruct.comp (Y := biproduct.{u_3, v, u} fun (i : ι) ↦ biproduct.{u_2, v, u} (g i))
      (CategoryStruct.comp (Y :=
        biproduct.{u_2, v, u} (J := f ((Sigma.mk (β := fun (i : ι) ↦ f i) j x).fst (β := fun (i : ι) ↦ f i)))
          (g ((Sigma.mk (β := fun (i : ι) ↦ f i) j x).fst (β := fun (i : ι) ↦ f i))))
        (biproduct.ι (g ((Sigma.mk (β := fun (i : ι) ↦ f i) j x).fst (β := fun (i : ι) ↦ f i)))
          ((Sigma.mk (β := fun (i : ι) ↦ f i) j x).snd (β := fun (i : ι) ↦ f i)))
        (biproduct.ι.{u_3, v, u} (C := C) (fun (i : ι) ↦ biproduct.{u_2, v, u} (g i))
          ((Sigma.mk (β := fun (i : ι) ↦ f i) j x).fst (β := fun (i : ι) ↦ f i))))
      (biproduct.π (fun (i : ι) ↦ biproduct.{u_2, v, u} (g i))
          ((Sigma.mk (β := fun (i : ι) ↦ f i) j y).fst (β := fun (i : ι) ↦ f i)) ≫
        biproduct.π (g ((Sigma.mk (β := fun (i : ι) ↦ f i) j y).fst (β := fun (i : ι) ↦ f i)))
          ((Sigma.mk (β := fun (i : ι) ↦ f i) j y).snd (β := fun (i : ι) ↦ f i))))
    0
have h₁ : ¬x = y
Tactic: simp only [heq_eq_eq, forall_true_left] at h
Cleared hypotheses: h
-- 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
p : J → Prop
inst_3 : HasBiproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)
inst_4 : DecidablePred p
j : J
⊢ Eq.{v + 1} (α := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f) ⟶ f j)
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (fromSubtype f p) (π f j))
    (if h : p j then π (Subtype.restrict (β := fun (x : J) ↦ C) p f) (Subtype.mk (p := p) j h) else 0)
have w : ∀ (i : Subtype p),
  Eq.{v + 1} (α := Subtype.restrict (β := fun (x : J) ↦ C) p f i ⟶ f j)
    (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
      (ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) i)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (fromSubtype f p) (π f j)))
    (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
      (ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) i)
      (if h : p j then π (Subtype.restrict (β := fun (x : J) ↦ C) p f) (Subtype.mk (p := p) j h) else 0))
Tactic: ext i
-- 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
p : J → Prop
inst_3 : HasBiproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)
inst_4 : DecidablePred p
j : J
i : Subtype p
⊢ Eq.{v + 1} (α := Subtype.restrict (β := fun (x : J) ↦ C) p f i ⟶ f j)
    (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
      (ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) i)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (fromSubtype f p) (π f j)))
    (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
      (ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) i)
      (if h : p j then π (Subtype.restrict (β := fun (x : J) ↦ C) p f) (Subtype.mk (p := p) j h) else 0))
have w : Eq.{v + 1} (α := Subtype.restrict (β := fun (x : J) ↦ C) p f i ⟶ f j) (if h : (↑i : J) = j then eqToHom sorry else 0)
  (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
    (ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) i)
    (if h : p j then π (Subtype.restrict (β := fun (x : J) ↦ C) p f) (Subtype.mk (p := p) j h) else 0))
Tactic: rw [biproduct.fromSubtype, biproduct.ι_desc_assoc, biproduct.ι_π]
-- 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
p : J → Prop
inst_3 : HasBiproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)
inst_4 : DecidablePred p
j : J
i : Subtype p
⊢ Eq.{v + 1} (α := Subtype.restrict (β := fun (x : J) ↦ C) p f i ⟶ f j) (if h : (↑i : J) = j then eqToHom ⋯ else 0)
    (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
      (ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) i)
      (if h : p j then π (Subtype.restrict (β := fun (x : J) ↦ C) p f) (Subtype.mk (p := p) j h) else 0))
have pos : ∀ (h : p j),
  Eq.{v + 1} (α := Subtype.restrict (β := fun (x : J) ↦ C) p f i ⟶ f j) (if h : (↑i : J) = j then eqToHom sorry else 0)
    (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
      (ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) i)
      (if h : p j then π (Subtype.restrict (β := fun (x : J) ↦ C) p f) (Subtype.mk (p := p) j h) else 0))
Tactic: by_cases h : p 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
p : J → Prop
inst_3 : HasBiproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)
inst_4 : DecidablePred p
j : J
i : Subtype p
pos :
  ∀ (h : p j),
    Eq.{v + 1} (α := Subtype.restrict (β := fun (x : J) ↦ C) p f i ⟶ f j) (if h : (↑i : J) = j then eqToHom ⋯ else 0)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
        (ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) i)
        (if h : p j then π (Subtype.restrict (β := fun (x : J) ↦ C) p f) (Subtype.mk (p := p) j h) else 0))
⊢ Eq.{v + 1} (α := Subtype.restrict (β := fun (x : J) ↦ C) p f i ⟶ f j) (if h : (↑i : J) = j then eqToHom ⋯ else 0)
    (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
      (ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) i)
      (if h : p j then π (Subtype.restrict (β := fun (x : J) ↦ C) p f) (Subtype.mk (p := p) j h) else 0))
have neg : ∀ (h : ¬p j),
  Eq.{v + 1} (α := Subtype.restrict (β := fun (x : J) ↦ C) p f i ⟶ f j) (if h : (↑i : J) = j then eqToHom sorry else 0)
    (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
      (ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) i)
      (if h : p j then π (Subtype.restrict (β := fun (x : J) ↦ C) p f) (Subtype.mk (p := p) j h) else 0))
Tactic: by_cases h : p 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
p : J → Prop
inst_3 : HasBiproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)
inst_4 : DecidablePred p
j : J
i : Subtype p
h : p j
⊢ Eq.{v + 1} (α := Subtype.restrict (β := fun (x : J) ↦ C) p f i ⟶ f j) (if h : (↑i : J) = j then eqToHom ⋯ else 0)
    (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
      (ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) i)
      (if h : p j then π (Subtype.restrict (β := fun (x : J) ↦ C) p f) (Subtype.mk (p := p) j h) else 0))
have pos : Eq.{v + 1} (α := Subtype.restrict (β := fun (x : J) ↦ C) p f i ⟶ f j) (if h : (↑i : J) = j then eqToHom sorry else 0)
  (if h_1 : i = Subtype.mk (p := p) j h then eqToHom sorry else 0)
Tactic: rw [dif_pos h, biproduct.ι_π]
-- 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
p : J → Prop
inst_3 : HasBiproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)
inst_4 : DecidablePred p
j : J
i : Subtype p
h : p j
⊢ Eq.{v + 1} (α := Subtype.restrict (β := fun (x : J) ↦ C) p f i ⟶ f j) (if h : (↑i : J) = j then eqToHom ⋯ else 0)
    (if h_1 : i = Subtype.mk (p := p) j h then eqToHom ⋯ else 0)
have pos : ∀ (h₁ : (↑i : J) = j) (h₂ : i = Subtype.mk (p := p) j h),
  Eq.{v + 1} (α := Subtype.restrict (β := fun (x : J) ↦ C) p f i ⟶ f j) (eqToHom sorry) (eqToHom sorry)
Tactic: split_ifs with h₁ h₂ h₂
-- 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
p : J → Prop
inst_3 : HasBiproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)
inst_4 : DecidablePred p
j : J
i : Subtype p
h : p j
pos :
  ∀ (h₁ : (↑i : J) = j) (h₂ : i = Subtype.mk (p := p) j h),
    Eq.{v + 1} (α := Subtype.restrict (β := fun (x : J) ↦ C) p f i ⟶ f j) (eqToHom ⋯) (eqToHom ⋯)
⊢ Eq.{v + 1} (α := Subtype.restrict (β := fun (x : J) ↦ C) p f i ⟶ f j) (if h : (↑i : J) = j then eqToHom ⋯ else 0)
    (if h_1 : i = Subtype.mk (p := p) j h then eqToHom ⋯ else 0)
have neg : ∀ (h₁ : (↑i : J) = j) (h₂ : ¬i = Subtype.mk (p := p) j h),
  Eq.{v + 1} (α := Subtype.restrict (β := fun (x : J) ↦ C) p f i ⟶ f j) (eqToHom sorry) 0
Tactic: split_ifs with h₁ h₂ h₂
-- 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
p : J → Prop
inst_3 : HasBiproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)
inst_4 : DecidablePred p
j : J
i : Subtype p
h : p j
pos :
  ∀ (h₁ : (↑i : J) = j) (h₂ : i = Subtype.mk (p := p) j h),
    Eq.{v + 1} (α := Subtype.restrict (β := fun (x : J) ↦ C) p f i ⟶ f j) (eqToHom ⋯) (eqToHom ⋯)
neg :
  ∀ (h₁ : (↑i : J) = j) (h₂ : ¬i = Subtype.mk (p := p) j h),
    Eq.{v + 1} (α := Subtype.restrict (β := fun (x : J) ↦ C) p f i ⟶ f j) (eqToHom ⋯) 0
⊢ Eq.{v + 1} (α := Subtype.restrict (β := fun (x : J) ↦ C) p f i ⟶ f j) (if h : (↑i : J) = j then eqToHom ⋯ else 0)
    (if h_1 : i = Subtype.mk (p := p) j h then eqToHom ⋯ else 0)
have pos₁ : ∀ (h₁ : ¬(↑i : J) = j) (h₂ : i = Subtype.mk (p := p) j h),
  Eq.{v + 1} (α := Subtype.restrict (β := fun (x : J) ↦ C) p f i ⟶ f j) 0 (eqToHom sorry)
Tactic: split_ifs with h₁ h₂ h₂