case a.mk.refl.h.mk
C : Type u
inst✝³ : Category C
ι : Type u_1
s : ι → C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
o : HomOrthogonal s
α : Type
inst✝ : Fintype α
f : α → ι
b a : α
j_property : a ∈ (fun a => f a) ⁻¹' {(fun b => f b) b}
⊢ ↑(matrixDecomposition o) (𝟙 (⨁ fun a => s (f a))) ((fun b => f b) b)
      { val := b, property := (_ : (fun b => f b) b = (fun b => f b) b) } { val := a, property := j_property } =
    OfNat.ofNat 1 { val := b, property := (_ : (fun b => f b) b = (fun b => f b) b) }
      { val := a, property := j_property }
C : Type u
inst✝³ : Category C
ι : Type u_1
s : ι → C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
o : HomOrthogonal s
α : Type
inst✝ : Fintype α
f : α → ι
i : ι
⊢ ↑(matrixDecomposition o) (𝟙 (⨁ fun a => s (f a))) i = 1
ext (⟨b, ⟨⟩⟩⟨a, j_property⟩)
case a.mk.refl.h.mk
C : Type u
inst✝³ : Category C
ι : Type u_1
s : ι → C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
o : HomOrthogonal s
α : Type
inst✝ : Fintype α
f : α → ι
b a : α
j_property✝ : a ∈ (fun a => f a) ⁻¹' {(fun b => f b) b}
j_property : f a = f b
⊢ ↑(matrixDecomposition o) (𝟙 (⨁ fun a => s (f a))) ((fun b => f b) b)
      { val := b, property := (_ : (fun b => f b) b = (fun b => f b) b) } { val := a, property := j_property✝ } =
    OfNat.ofNat 1 { val := b, property := (_ : (fun b => f b) b = (fun b => f b) b) }
      { val := a, property := j_property✝ }
case a.mk.refl.h.mk
C : Type u
inst✝³ : Category C
ι : Type u_1
s : ι → C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
o : HomOrthogonal s
α : Type
inst✝ : Fintype α
f : α → ι
b a : α
j_property : a ∈ (fun a => f a) ⁻¹' {(fun b => f b) b}
⊢ ↑(matrixDecomposition o) (𝟙 (⨁ fun a => s (f a))) ((fun b => f b) b)
      { val := b, property := (_ : (fun b => f b) b = (fun b => f b) b) } { val := a, property := j_property } =
    OfNat.ofNat 1 { val := b, property := (_ : (fun b => f b) b = (fun b => f b) b) }
      { val := a, property := j_property }
simp only [Set.mem_preimage, Set.mem_singleton_iff] at j_property
case a.mk.refl.h.mk
C : Type u
inst✝³ : Category C
ι : Type u_1
s : ι → C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
o : HomOrthogonal s
α : Type
inst✝ : Fintype α
f : α → ι
b a : α
j_property✝ : a ∈ (fun a => f a) ⁻¹' {(fun b => f b) b}
j_property : f a = f b
⊢ eqToHom (_ : s (f b) = s (f ↑{ val := a, property := j_property✝ })) ≫
      biproduct.ι (fun a => s (f a)) a ≫ biproduct.π (fun b => s (f b)) b =
    if { val := b, property := (_ : (fun b => f b) b = (fun b => f b) b) } = { val := a, property := j_property✝ } then
      𝟙 (s (f b))
    else 0
case a.mk.refl.h.mk
C : Type u
inst✝³ : Category C
ι : Type u_1
s : ι → C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
o : HomOrthogonal s
α : Type
inst✝ : Fintype α
f : α → ι
b a : α
j_property✝ : a ∈ (fun a => f a) ⁻¹' {(fun b => f b) b}
j_property : f a = f b
⊢ ↑(matrixDecomposition o) (𝟙 (⨁ fun a => s (f a))) ((fun b => f b) b)
      { val := b, property := (_ : (fun b => f b) b = (fun b => f b) b) } { val := a, property := j_property✝ } =
    OfNat.ofNat 1 { val := b, property := (_ : (fun b => f b) b = (fun b => f b) b) }
      { val := a, property := j_property✝ }
simp only [Category.comp_id, Category.id_comp, Category.assoc, End.one_def, eqToHom_refl,
  Matrix.one_apply, HomOrthogonal.matrixDecomposition_apply, biproduct.components]
case a.mk.refl.h.mk.inl
C : Type u
inst✝³ : Category C
ι : Type u_1
s : ι → C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
o : HomOrthogonal s
α : Type
inst✝ : Fintype α
f : α → ι
b a : α
j_property✝ : a ∈ (fun a => f a) ⁻¹' {(fun b => f b) b}
j_property : f a = f b
h : { val := b, property := (_ : (fun b => f b) b = (fun b => f b) b) } = { val := a, property := j_property✝ }
⊢ eqToHom (_ : s (f b) = s (f ↑{ val := a, property := j_property✝ })) ≫
      biproduct.ι (fun a => s (f a)) a ≫ biproduct.π (fun b => s (f b)) b =
    𝟙 (s (f b))

case a.mk.refl.h.mk.inr
C : Type u
inst✝³ : Category C
ι : Type u_1
s : ι → C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
o : HomOrthogonal s
α : Type
inst✝ : Fintype α
f : α → ι
b a : α
j_property✝ : a ∈ (fun a => f a) ⁻¹' {(fun b => f b) b}
j_property : f a = f b
h : ¬{ val := b, property := (_ : (fun b => f b) b = (fun b => f b) b) } = { val := a, property := j_property✝ }
⊢ eqToHom (_ : s (f b) = s (f ↑{ val := a, property := j_property✝ })) ≫
      biproduct.ι (fun a => s (f a)) a ≫ biproduct.π (fun b => s (f b)) b =
    0
case a.mk.refl.h.mk
C : Type u
inst✝³ : Category C
ι : Type u_1
s : ι → C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
o : HomOrthogonal s
α : Type
inst✝ : Fintype α
f : α → ι
b a : α
j_property✝ : a ∈ (fun a => f a) ⁻¹' {(fun b => f b) b}
j_property : f a = f b
⊢ eqToHom (_ : s (f b) = s (f ↑{ val := a, property := j_property✝ })) ≫
      biproduct.ι (fun a => s (f a)) a ≫ biproduct.π (fun b => s (f b)) b =
    if { val := b, property := (_ : (fun b => f b) b = (fun b => f b) b) } = { val := a, property := j_property✝ } then
      𝟙 (s (f b))
    else 0
split_ifs with h
case a.mk.refl.h.mk.inl.refl
C : Type u
inst✝³ : Category C
ι : Type u_1
s : ι → C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
o : HomOrthogonal s
α : Type
inst✝ : Fintype α
f : α → ι
b : α
j_property✝ : b ∈ (fun a => f a) ⁻¹' {(fun b => f b) b}
j_property : f b = f b
⊢ eqToHom (_ : s (f b) = s (f ↑{ val := b, property := j_property✝ })) ≫
      biproduct.ι (fun a => s (f a)) b ≫ biproduct.π (fun b => s (f b)) b =
    𝟙 (s (f b))
case a.mk.refl.h.mk.inl
C : Type u
inst✝³ : Category C
ι : Type u_1
s : ι → C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
o : HomOrthogonal s
α : Type
inst✝ : Fintype α
f : α → ι
b a : α
j_property✝ : a ∈ (fun a => f a) ⁻¹' {(fun b => f b) b}
j_property : f a = f b
h : { val := b, property := (_ : (fun b => f b) b = (fun b => f b) b) } = { val := a, property := j_property✝ }
⊢ eqToHom (_ : s (f b) = s (f ↑{ val := a, property := j_property✝ })) ≫
      biproduct.ι (fun a => s (f a)) a ≫ biproduct.π (fun b => s (f b)) b =
    𝟙 (s (f b))
cases h
no goals
case a.mk.refl.h.mk.inl.refl
C : Type u
inst✝³ : Category C
ι : Type u_1
s : ι → C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
o : HomOrthogonal s
α : Type
inst✝ : Fintype α
f : α → ι
b : α
j_property✝ : b ∈ (fun a => f a) ⁻¹' {(fun b => f b) b}
j_property : f b = f b
⊢ eqToHom (_ : s (f b) = s (f ↑{ val := b, property := j_property✝ })) ≫
      biproduct.ι (fun a => s (f a)) b ≫ biproduct.π (fun b => s (f b)) b =
    𝟙 (s (f b))
simp
case a.mk.refl.h.mk.inr
C : Type u
inst✝³ : Category C
ι : Type u_1
s : ι → C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
o : HomOrthogonal s
α : Type
inst✝ : Fintype α
f : α → ι
b a : α
j_property✝ : a ∈ (fun a => f a) ⁻¹' {(fun b => f b) b}
j_property : f a = f b
h : ¬b = a
⊢ eqToHom (_ : s (f b) = s (f ↑{ val := a, property := j_property✝ })) ≫
      biproduct.ι (fun a => s (f a)) a ≫ biproduct.π (fun b => s (f b)) b =
    0
case a.mk.refl.h.mk.inr
C : Type u
inst✝³ : Category C
ι : Type u_1
s : ι → C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
o : HomOrthogonal s
α : Type
inst✝ : Fintype α
f : α → ι
b a : α
j_property✝ : a ∈ (fun a => f a) ⁻¹' {(fun b => f b) b}
j_property : f a = f b
h : ¬{ val := b, property := (_ : (fun b => f b) b = (fun b => f b) b) } = { val := a, property := j_property✝ }
⊢ eqToHom (_ : s (f b) = s (f ↑{ val := a, property := j_property✝ })) ≫
      biproduct.ι (fun a => s (f a)) a ≫ biproduct.π (fun b => s (f b)) b =
    0
simp at h
case a.mk.refl.h.mk.inr
C : Type u
inst✝³ : Category C
ι : Type u_1
s : ι → C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
o : HomOrthogonal s
α : Type
inst✝ : Fintype α
f : α → ι
b a : α
j_property✝ : a ∈ (fun a => f a) ⁻¹' {(fun b => f b) b}
j_property : f a = f b
h : ¬b = a
this : biproduct.ι (fun a => s (f a)) a ≫ biproduct.π (fun b => s (f b)) b = 0
⊢ eqToHom (_ : s (f b) = s (f ↑{ val := a, property := j_property✝ })) ≫
      biproduct.ι (fun a => s (f a)) a ≫ biproduct.π (fun b => s (f b)) b =
    0
case a.mk.refl.h.mk.inr
C : Type u
inst✝³ : Category C
ι : Type u_1
s : ι → C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
o : HomOrthogonal s
α : Type
inst✝ : Fintype α
f : α → ι
b a : α
j_property✝ : a ∈ (fun a => f a) ⁻¹' {(fun b => f b) b}
j_property : f a = f b
h : ¬b = a
⊢ eqToHom (_ : s (f b) = s (f ↑{ val := a, property := j_property✝ })) ≫
      biproduct.ι (fun a => s (f a)) a ≫ biproduct.π (fun b => s (f b)) b =
    0
have : biproduct.ι (fun a ↦ s (f a)) a ≫ biproduct.π (fun b ↦ s (f b)) b = 0 := by
  simpa using biproduct.ι_π_ne _ (Ne.symm h)
no goals
case a.mk.refl.h.mk.inr
C : Type u
inst✝³ : Category C
ι : Type u_1
s : ι → C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
o : HomOrthogonal s
α : Type
inst✝ : Fintype α
f : α → ι
b a : α
j_property✝ : a ∈ (fun a => f a) ⁻¹' {(fun b => f b) b}
j_property : f a = f b
h : ¬b = a
this : biproduct.ι (fun a => s (f a)) a ≫ biproduct.π (fun b => s (f b)) b = 0
⊢ eqToHom (_ : s (f b) = s (f ↑{ val := a, property := j_property✝ })) ≫
      biproduct.ι (fun a => s (f a)) a ≫ biproduct.π (fun b => s (f b)) b =
    0
rw [this, comp_zero]
no goals
C : Type u
inst✝³ : Category C
ι : Type u_1
s : ι → C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
o : HomOrthogonal s
α : Type
inst✝ : Fintype α
f : α → ι
b a : α
j_property✝ : a ∈ (fun a => f a) ⁻¹' {(fun b => f b) b}
j_property : f a = f b
h : ¬b = a
⊢ biproduct.ι (fun a => s (f a)) a ≫ biproduct.π (fun b => s (f b)) b = 0
simpa using biproduct.ι_π_ne _ (Ne.symm h)