[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝ : HasZeroMorphisms C
o : HomOrthogonal s
i j : ι
w : i ≠ j
f : s i ⟶ s j
⊢ f = 0
[PROOFSTEP]
haveI := o i j w
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝ : HasZeroMorphisms C
o : HomOrthogonal s
i j : ι
w : i ≠ j
f : s i ⟶ s j
this : Subsingleton (s i ⟶ s j)
⊢ f = 0
[PROOFSTEP]
apply Subsingleton.elim
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
o : HomOrthogonal s
α β : Type
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ι
g : β → ι
z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)
i : ι
j : ↑(g ⁻¹' {i})
k : ↑(f ⁻¹' {i})
⊢ s i = s (f ↑k)
[PROOFSTEP]
rcases k with ⟨k, ⟨⟩⟩
[GOAL]
case mk.refl
C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
o : HomOrthogonal s
α β : Type
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ι
g : β → ι
z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)
k : α
j : ↑(g ⁻¹' {f k})
⊢ s (f k) = s (f ↑{ val := k, property := (_ : f k = f k) })
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
o : HomOrthogonal s
α β : Type
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ι
g : β → ι
z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)
i : ι
j : ↑(g ⁻¹' {i})
k : ↑(f ⁻¹' {i})
⊢ s (g ↑j) = s i
[PROOFSTEP]
rcases j with ⟨j, ⟨⟩⟩
[GOAL]
case mk.refl
C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
o : HomOrthogonal s
α β : Type
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ι
g : β → ι
z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)
j : β
k : ↑(f ⁻¹' {g j})
⊢ s (g ↑{ val := j, property := (_ : g j = g j) }) = s (g j)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
o : HomOrthogonal s
α β : Type
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ι
g : β → ι
z : (i : ι) → Matrix (↑(g ⁻¹' {i})) (↑(f ⁻¹' {i})) (End (s i))
j : α
k : β
h : f j = g k
⊢ k ∈ g ⁻¹' {f j}
[PROOFSTEP]
simp [h]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
o : HomOrthogonal s
α β : Type
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ι
g : β → ι
z : (i : ι) → Matrix (↑(g ⁻¹' {i})) (↑(f ⁻¹' {i})) (End (s i))
j : α
k : β
h : f j = g k
⊢ j ∈ f ⁻¹' {f j}
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
o : HomOrthogonal s
α β : Type
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ι
g : β → ι
z : (i : ι) → Matrix (↑(g ⁻¹' {i})) (↑(f ⁻¹' {i})) (End (s i))
j : α
k : β
h : f j = g k
⊢ s (f j) = s (g k)
[PROOFSTEP]
simp [h]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
o : HomOrthogonal s
α β : Type
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ι
g : β → ι
z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)
⊢ (fun z =>
        biproduct.matrix fun j k =>
          if h : f j = g k then
            z (f j) { val := k, property := (_ : k ∈ g ⁻¹' {f j}) } { val := j, property := (_ : j ∈ f ⁻¹' {f j}) } ≫
              eqToHom (_ : s (f j) = s (g k))
          else 0)
      ((fun z i j k => eqToHom (_ : s i = s (f ↑k)) ≫ biproduct.components z ↑k ↑j ≫ eqToHom (_ : s (g ↑j) = s i)) z) =
    z
[PROOFSTEP]
ext j k
[GOAL]
case w.w
C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
o : HomOrthogonal s
α β : Type
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ι
g : β → ι
z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)
j : β
k : α
⊢ biproduct.ι (fun a => s (f a)) k ≫
      (fun z =>
            biproduct.matrix fun j k =>
              if h : f j = g k then
                z (f j) { val := k, property := (_ : k ∈ g ⁻¹' {f j}) }
                    { val := j, property := (_ : j ∈ f ⁻¹' {f j}) } ≫
                  eqToHom (_ : s (f j) = s (g k))
              else 0)
          ((fun z i j k => eqToHom (_ : s i = s (f ↑k)) ≫ biproduct.components z ↑k ↑j ≫ eqToHom (_ : s (g ↑j) = s i))
            z) ≫
        biproduct.π (fun b => s (g b)) j =
    biproduct.ι (fun a => s (f a)) k ≫ z ≫ biproduct.π (fun b => s (g b)) j
[PROOFSTEP]
simp only [biproduct.matrix_π, biproduct.ι_desc]
[GOAL]
case w.w
C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
o : HomOrthogonal s
α β : Type
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ι
g : β → ι
z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)
j : β
k : α
⊢ (if h : f k = g j then
      (eqToHom (_ : s (f k) = s (f ↑{ val := k, property := (_ : k ∈ f ⁻¹' {f k}) })) ≫
          biproduct.components z k j ≫ eqToHom (_ : s (g ↑{ val := j, property := (_ : j ∈ g ⁻¹' {f k}) }) = s (f k))) ≫
        eqToHom (_ : s (f k) = s (g j))
    else 0) =
    biproduct.ι (fun a => s (f a)) k ≫ z ≫ biproduct.π (fun b => s (g b)) j
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
o : HomOrthogonal s
α β : Type
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ι
g : β → ι
z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)
j : β
k : α
h : f k = g j
⊢ (eqToHom (_ : s (f k) = s (f ↑{ val := k, property := (_ : k ∈ f ⁻¹' {f k}) })) ≫
        biproduct.components z k j ≫ eqToHom (_ : s (g ↑{ val := j, property := (_ : j ∈ g ⁻¹' {f k}) }) = s (f k))) ≫
      eqToHom (_ : s (f k) = s (g j)) =
    biproduct.ι (fun a => s (f a)) k ≫ z ≫ biproduct.π (fun b => s (g b)) j
[PROOFSTEP]
simp
[GOAL]
case pos
C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
o : HomOrthogonal s
α β : Type
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ι
g : β → ι
z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)
j : β
k : α
h : f k = g j
⊢ biproduct.components z k j = biproduct.ι (fun a => s (f a)) k ≫ z ≫ biproduct.π (fun b => s (g b)) j
[PROOFSTEP]
rfl
[GOAL]
case neg
C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
o : HomOrthogonal s
α β : Type
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ι
g : β → ι
z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)
j : β
k : α
h : ¬f k = g j
⊢ 0 = biproduct.ι (fun a => s (f a)) k ≫ z ≫ biproduct.π (fun b => s (g b)) j
[PROOFSTEP]
symm
[GOAL]
case neg
C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
o : HomOrthogonal s
α β : Type
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ι
g : β → ι
z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)
j : β
k : α
h : ¬f k = g j
⊢ biproduct.ι (fun a => s (f a)) k ≫ z ≫ biproduct.π (fun b => s (g b)) j = 0
[PROOFSTEP]
apply o.eq_zero h
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
o : HomOrthogonal s
α β : Type
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ι
g : β → ι
z : (i : ι) → Matrix (↑(g ⁻¹' {i})) (↑(f ⁻¹' {i})) (End (s i))
⊢ (fun z i j k => eqToHom (_ : s i = s (f ↑k)) ≫ biproduct.components z ↑k ↑j ≫ eqToHom (_ : s (g ↑j) = s i))
      ((fun z =>
          biproduct.matrix fun j k =>
            if h : f j = g k then
              z (f j) { val := k, property := (_ : k ∈ g ⁻¹' {f j}) } { val := j, property := (_ : j ∈ f ⁻¹' {f j}) } ≫
                eqToHom (_ : s (f j) = s (g k))
            else 0)
        z) =
    z
[PROOFSTEP]
ext i ⟨j, w⟩ ⟨k, ⟨⟩⟩
[GOAL]
case h.h.mk.h.mk.refl
C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
o : HomOrthogonal s
α β : Type
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ι
g : β → ι
z : (i : ι) → Matrix (↑(g ⁻¹' {i})) (↑(f ⁻¹' {i})) (End (s i))
j : β
k : α
w : j ∈ g ⁻¹' {f k}
⊢ (fun z i j k => eqToHom (_ : s i = s (f ↑k)) ≫ biproduct.components z ↑k ↑j ≫ eqToHom (_ : s (g ↑j) = s i))
      ((fun z =>
          biproduct.matrix fun j k =>
            if h : f j = g k then
              z (f j) { val := k, property := (_ : k ∈ g ⁻¹' {f j}) } { val := j, property := (_ : j ∈ f ⁻¹' {f j}) } ≫
                eqToHom (_ : s (f j) = s (g k))
            else 0)
        z)
      (f k) { val := j, property := w } { val := k, property := (_ : f k = f k) } =
    z (f k) { val := j, property := w } { val := k, property := (_ : f k = f k) }
[PROOFSTEP]
simp only [eqToHom_refl, biproduct.matrix_components, Category.id_comp]
[GOAL]
case h.h.mk.h.mk.refl
C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
o : HomOrthogonal s
α β : Type
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ι
g : β → ι
z : (i : ι) → Matrix (↑(g ⁻¹' {i})) (↑(f ⁻¹' {i})) (End (s i))
j : β
k : α
w : j ∈ g ⁻¹' {f k}
⊢ (if h : f k = g j then
        z (f k) { val := j, property := (_ : j ∈ g ⁻¹' {f k}) } { val := k, property := (_ : k ∈ f ⁻¹' {f k}) } ≫
          eqToHom (_ : s (f k) = s (g j))
      else 0) ≫
      eqToHom (_ : s (g ↑{ val := j, property := w }) = s (f k)) =
    z (f k) { val := j, property := w } { val := k, property := (_ : f k = f k) }
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
o : HomOrthogonal s
α β : Type
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ι
g : β → ι
z : (i : ι) → Matrix (↑(g ⁻¹' {i})) (↑(f ⁻¹' {i})) (End (s i))
j : β
k : α
w : j ∈ g ⁻¹' {f k}
h : f k = g j
⊢ (z (f k) { val := j, property := (_ : j ∈ g ⁻¹' {f k}) } { val := k, property := (_ : k ∈ f ⁻¹' {f k}) } ≫
        eqToHom (_ : s (f k) = s (g j))) ≫
      eqToHom (_ : s (g ↑{ val := j, property := w }) = s (f k)) =
    z (f k) { val := j, property := w } { val := k, property := (_ : f k = f k) }
[PROOFSTEP]
simp
[GOAL]
case neg
C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
o : HomOrthogonal s
α β : Type
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ι
g : β → ι
z : (i : ι) → Matrix (↑(g ⁻¹' {i})) (↑(f ⁻¹' {i})) (End (s i))
j : β
k : α
w : j ∈ g ⁻¹' {f k}
h : ¬f k = g j
⊢ 0 ≫ eqToHom (_ : s (g ↑{ val := j, property := w }) = s (f k)) =
    z (f k) { val := j, property := w } { val := k, property := (_ : f k = f k) }
[PROOFSTEP]
exfalso
[GOAL]
case neg.h
C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
o : HomOrthogonal s
α β : Type
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ι
g : β → ι
z : (i : ι) → Matrix (↑(g ⁻¹' {i})) (↑(f ⁻¹' {i})) (End (s i))
j : β
k : α
w : j ∈ g ⁻¹' {f k}
h : ¬f k = g j
⊢ False
[PROOFSTEP]
exact h w.symm
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝³ : Preadditive C
inst✝² : HasFiniteBiproducts C
o : HomOrthogonal s
α β : Type
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ι
g : β → ι
src✝ : ((⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)) ≃
  ((i : ι) → Matrix (↑((fun b => g b) ⁻¹' {i})) (↑((fun a => f a) ⁻¹' {i})) (End (s i))) :=
  matrixDecomposition o
w z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)
⊢ Equiv.toFun
      { toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
        right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
      (w + z) =
    Equiv.toFun
        { toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
          right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        w +
      Equiv.toFun
        { toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
          right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        z
[PROOFSTEP]
ext
[GOAL]
case h.a.h
C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝³ : Preadditive C
inst✝² : HasFiniteBiproducts C
o : HomOrthogonal s
α β : Type
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ι
g : β → ι
src✝ : ((⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)) ≃
  ((i : ι) → Matrix (↑((fun b => g b) ⁻¹' {i})) (↑((fun a => f a) ⁻¹' {i})) (End (s i))) :=
  matrixDecomposition o
w z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)
x✝¹ : ι
i✝ : ↑(g ⁻¹' {x✝¹})
x✝ : ↑(f ⁻¹' {x✝¹})
⊢ Equiv.toFun
      { toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
        right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
      (w + z) x✝¹ i✝ x✝ =
    (Equiv.toFun
          { toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
          w +
        Equiv.toFun
          { toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
          z)
      x✝¹ i✝ x✝
[PROOFSTEP]
dsimp [biproduct.components]
[GOAL]
case h.a.h
C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝³ : Preadditive C
inst✝² : HasFiniteBiproducts C
o : HomOrthogonal s
α β : Type
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ι
g : β → ι
src✝ : ((⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)) ≃
  ((i : ι) → Matrix (↑((fun b => g b) ⁻¹' {i})) (↑((fun a => f a) ⁻¹' {i})) (End (s i))) :=
  matrixDecomposition o
w z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)
x✝¹ : ι
i✝ : ↑(g ⁻¹' {x✝¹})
x✝ : ↑(f ⁻¹' {x✝¹})
⊢ eqToHom (_ : s x✝¹ = s (f ↑x✝)) ≫
      (biproduct.ι (fun a => s (f a)) ↑x✝ ≫ (w + z) ≫ biproduct.π (fun b => s (g b)) ↑i✝) ≫
        eqToHom (_ : s (g ↑i✝) = s x✝¹) =
    eqToHom (_ : s x✝¹ = s (f ↑x✝)) ≫
        (biproduct.ι (fun a => s (f a)) ↑x✝ ≫ w ≫ biproduct.π (fun b => s (g b)) ↑i✝) ≫
          eqToHom (_ : s (g ↑i✝) = s x✝¹) +
      eqToHom (_ : s x✝¹ = s (f ↑x✝)) ≫
        (biproduct.ι (fun a => s (f a)) ↑x✝ ≫ z ≫ biproduct.π (fun b => s (g b)) ↑i✝) ≫ eqToHom (_ : s (g ↑i✝) = s x✝¹)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} 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
[PROOFSTEP]
ext ⟨b, ⟨⟩⟩ ⟨a, j_property⟩
[GOAL]
case a.mk.refl.h.mk
C : Type u
inst✝³ : Category.{v, u} 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 }
[PROOFSTEP]
simp only [Set.mem_preimage, Set.mem_singleton_iff] at j_property 
[GOAL]
case a.mk.refl.h.mk
C : Type u
inst✝³ : Category.{v, u} 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✝ }
[PROOFSTEP]
simp only [Category.comp_id, Category.id_comp, Category.assoc, End.one_def, eqToHom_refl, Matrix.one_apply,
  HomOrthogonal.matrixDecomposition_apply, biproduct.components]
[GOAL]
case a.mk.refl.h.mk
C : Type u
inst✝³ : Category.{v, u} 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
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
C : Type u
inst✝³ : Category.{v, u} 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))
[PROOFSTEP]
cases h
[GOAL]
case pos.refl
C : Type u
inst✝³ : Category.{v, u} 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))
[PROOFSTEP]
simp
[GOAL]
case neg
C : Type u
inst✝³ : Category.{v, u} 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
[PROOFSTEP]
simp at h 
[GOAL]
case neg
C : Type u
inst✝³ : Category.{v, u} 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
[PROOFSTEP]
have : biproduct.ι (fun a ↦ s (f a)) a ≫ biproduct.π (fun b ↦ s (f b)) b = 0 := by
  simpa using biproduct.ι_π_ne _ (Ne.symm h)
[GOAL]
C : Type u
inst✝³ : Category.{v, u} 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
[PROOFSTEP]
simpa using biproduct.ι_π_ne _ (Ne.symm h)
[GOAL]
case neg
C : Type u
inst✝³ : Category.{v, u} 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
[PROOFSTEP]
rw [this, comp_zero]
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
o : HomOrthogonal s
α β γ : Type
inst✝² : Fintype α
inst✝¹ : Fintype β
inst✝ : Fintype γ
f : α → ι
g : β → ι
h : γ → ι
z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)
w : (⨁ fun b => s (g b)) ⟶ ⨁ fun c => s (h c)
i : ι
⊢ ↑(matrixDecomposition o) (z ≫ w) i = ↑(matrixDecomposition o) w i * ↑(matrixDecomposition o) z i
[PROOFSTEP]
ext ⟨c, ⟨⟩⟩ ⟨a, j_property⟩
[GOAL]
case a.mk.refl.h.mk
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
o : HomOrthogonal s
α β γ : Type
inst✝² : Fintype α
inst✝¹ : Fintype β
inst✝ : Fintype γ
f : α → ι
g : β → ι
h : γ → ι
z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)
w : (⨁ fun b => s (g b)) ⟶ ⨁ fun c => s (h c)
c : γ
a : α
j_property : a ∈ (fun a => f a) ⁻¹' {(fun b => h b) c}
⊢ ↑(matrixDecomposition o) (z ≫ w) ((fun b => h b) c)
      { val := c, property := (_ : (fun b => h b) c = (fun b => h b) c) } { val := a, property := j_property } =
    (↑(matrixDecomposition o) w ((fun b => h b) c) * ↑(matrixDecomposition o) z ((fun b => h b) c))
      { val := c, property := (_ : (fun b => h b) c = (fun b => h b) c) } { val := a, property := j_property }
[PROOFSTEP]
simp only [Set.mem_preimage, Set.mem_singleton_iff] at j_property 
[GOAL]
case a.mk.refl.h.mk
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
o : HomOrthogonal s
α β γ : Type
inst✝² : Fintype α
inst✝¹ : Fintype β
inst✝ : Fintype γ
f : α → ι
g : β → ι
h : γ → ι
z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)
w : (⨁ fun b => s (g b)) ⟶ ⨁ fun c => s (h c)
c : γ
a : α
j_property✝ : a ∈ (fun a => f a) ⁻¹' {(fun b => h b) c}
j_property : f a = h c
⊢ ↑(matrixDecomposition o) (z ≫ w) ((fun b => h b) c)
      { val := c, property := (_ : (fun b => h b) c = (fun b => h b) c) } { val := a, property := j_property✝ } =
    (↑(matrixDecomposition o) w ((fun b => h b) c) * ↑(matrixDecomposition o) z ((fun b => h b) c))
      { val := c, property := (_ : (fun b => h b) c = (fun b => h b) c) } { val := a, property := j_property✝ }
[PROOFSTEP]
simp only [Matrix.mul_apply, Limits.biproduct.components, HomOrthogonal.matrixDecomposition_apply, Category.comp_id,
  Category.id_comp, Category.assoc, End.mul_def, eqToHom_refl, eqToHom_trans_assoc, Finset.sum_congr]
[GOAL]
case a.mk.refl.h.mk
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
o : HomOrthogonal s
α β γ : Type
inst✝² : Fintype α
inst✝¹ : Fintype β
inst✝ : Fintype γ
f : α → ι
g : β → ι
h : γ → ι
z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)
w : (⨁ fun b => s (g b)) ⟶ ⨁ fun c => s (h c)
c : γ
a : α
j_property✝ : a ∈ (fun a => f a) ⁻¹' {(fun b => h b) c}
j_property : f a = h c
⊢ eqToHom (_ : s (h c) = s (f ↑{ val := a, property := j_property✝ })) ≫
      biproduct.ι (fun a => s (f a)) a ≫ z ≫ w ≫ biproduct.π (fun b => s (h b)) c =
    Finset.sum Finset.univ fun x =>
      eqToHom (_ : s (h c) = s (f ↑{ val := a, property := j_property✝ })) ≫
        biproduct.ι (fun a => s (f a)) a ≫
          z ≫
            biproduct.π (fun b => s (g b)) ↑x ≫ biproduct.ι (fun a => s (g a)) ↑x ≫ w ≫ biproduct.π (fun b => s (h b)) c
[PROOFSTEP]
conv_lhs => rw [← Category.id_comp w, ← biproduct.total]
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
o : HomOrthogonal s
α β γ : Type
inst✝² : Fintype α
inst✝¹ : Fintype β
inst✝ : Fintype γ
f : α → ι
g : β → ι
h : γ → ι
z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)
w : (⨁ fun b => s (g b)) ⟶ ⨁ fun c => s (h c)
c : γ
a : α
j_property✝ : a ∈ (fun a => f a) ⁻¹' {(fun b => h b) c}
j_property : f a = h c
| eqToHom (_ : s (h c) = s (f ↑{ val := a, property := j_property✝ })) ≫
    biproduct.ι (fun a => s (f a)) a ≫ z ≫ w ≫ biproduct.π (fun b => s (h b)) c
[PROOFSTEP]
rw [← Category.id_comp w, ← biproduct.total]
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
o : HomOrthogonal s
α β γ : Type
inst✝² : Fintype α
inst✝¹ : Fintype β
inst✝ : Fintype γ
f : α → ι
g : β → ι
h : γ → ι
z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)
w : (⨁ fun b => s (g b)) ⟶ ⨁ fun c => s (h c)
c : γ
a : α
j_property✝ : a ∈ (fun a => f a) ⁻¹' {(fun b => h b) c}
j_property : f a = h c
| eqToHom (_ : s (h c) = s (f ↑{ val := a, property := j_property✝ })) ≫
    biproduct.ι (fun a => s (f a)) a ≫ z ≫ w ≫ biproduct.π (fun b => s (h b)) c
[PROOFSTEP]
rw [← Category.id_comp w, ← biproduct.total]
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
o : HomOrthogonal s
α β γ : Type
inst✝² : Fintype α
inst✝¹ : Fintype β
inst✝ : Fintype γ
f : α → ι
g : β → ι
h : γ → ι
z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)
w : (⨁ fun b => s (g b)) ⟶ ⨁ fun c => s (h c)
c : γ
a : α
j_property✝ : a ∈ (fun a => f a) ⁻¹' {(fun b => h b) c}
j_property : f a = h c
| eqToHom (_ : s (h c) = s (f ↑{ val := a, property := j_property✝ })) ≫
    biproduct.ι (fun a => s (f a)) a ≫ z ≫ w ≫ biproduct.π (fun b => s (h b)) c
[PROOFSTEP]
rw [← Category.id_comp w, ← biproduct.total]
[GOAL]
case a.mk.refl.h.mk
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
o : HomOrthogonal s
α β γ : Type
inst✝² : Fintype α
inst✝¹ : Fintype β
inst✝ : Fintype γ
f : α → ι
g : β → ι
h : γ → ι
z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)
w : (⨁ fun b => s (g b)) ⟶ ⨁ fun c => s (h c)
c : γ
a : α
j_property✝ : a ∈ (fun a => f a) ⁻¹' {(fun b => h b) c}
j_property : f a = h c
⊢ eqToHom (_ : s (h c) = s (f ↑{ val := a, property := j_property✝ })) ≫
      biproduct.ι (fun a => s (f a)) a ≫
        z ≫
          ((Finset.sum Finset.univ fun j => biproduct.π (fun b => s (g b)) j ≫ biproduct.ι (fun b => s (g b)) j) ≫ w) ≫
            biproduct.π (fun b => s (h b)) c =
    Finset.sum Finset.univ fun x =>
      eqToHom (_ : s (h c) = s (f ↑{ val := a, property := j_property✝ })) ≫
        biproduct.ι (fun a => s (f a)) a ≫
          z ≫
            biproduct.π (fun b => s (g b)) ↑x ≫ biproduct.ι (fun a => s (g a)) ↑x ≫ w ≫ biproduct.π (fun b => s (h b)) c
[PROOFSTEP]
simp only [Preadditive.sum_comp, Preadditive.comp_sum]
[GOAL]
case a.mk.refl.h.mk
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
o : HomOrthogonal s
α β γ : Type
inst✝² : Fintype α
inst✝¹ : Fintype β
inst✝ : Fintype γ
f : α → ι
g : β → ι
h : γ → ι
z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)
w : (⨁ fun b => s (g b)) ⟶ ⨁ fun c => s (h c)
c : γ
a : α
j_property✝ : a ∈ (fun a => f a) ⁻¹' {(fun b => h b) c}
j_property : f a = h c
⊢ (Finset.sum Finset.univ fun j =>
      eqToHom (_ : s (h c) = s (f ↑{ val := a, property := j_property✝ })) ≫
        biproduct.ι (fun a => s (f a)) a ≫
          z ≫
            ((biproduct.π (fun b => s (g b)) j ≫ biproduct.ι (fun b => s (g b)) j) ≫ w) ≫
              biproduct.π (fun b => s (h b)) c) =
    Finset.sum Finset.univ fun x =>
      eqToHom (_ : s (h c) = s (f ↑{ val := a, property := j_property✝ })) ≫
        biproduct.ι (fun a => s (f a)) a ≫
          z ≫
            biproduct.π (fun b => s (g b)) ↑x ≫ biproduct.ι (fun a => s (g a)) ↑x ≫ w ≫ biproduct.π (fun b => s (h b)) c
[PROOFSTEP]
apply Finset.sum_congr_set
[GOAL]
case a.mk.refl.h.mk.w
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
o : HomOrthogonal s
α β γ : Type
inst✝² : Fintype α
inst✝¹ : Fintype β
inst✝ : Fintype γ
f : α → ι
g : β → ι
h : γ → ι
z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)
w : (⨁ fun b => s (g b)) ⟶ ⨁ fun c => s (h c)
c : γ
a : α
j_property✝ : a ∈ (fun a => f a) ⁻¹' {(fun b => h b) c}
j_property : f a = h c
⊢ ∀ (x : β) (h_1 : x ∈ (fun a => g a) ⁻¹' {h c}),
    eqToHom (_ : s (h c) = s (f ↑{ val := a, property := j_property✝ })) ≫
        biproduct.ι (fun a => s (f a)) a ≫
          z ≫
            ((biproduct.π (fun b => s (g b)) x ≫ biproduct.ι (fun b => s (g b)) x) ≫ w) ≫
              biproduct.π (fun b => s (h b)) c =
      eqToHom (_ : s (h c) = s (f ↑{ val := a, property := j_property✝ })) ≫
        biproduct.ι (fun a => s (f a)) a ≫
          z ≫
            biproduct.π (fun b => s (g b)) ↑{ val := x, property := h_1 } ≫
              biproduct.ι (fun a => s (g a)) ↑{ val := x, property := h_1 } ≫ w ≫ biproduct.π (fun b => s (h b)) c
[PROOFSTEP]
intros
[GOAL]
case a.mk.refl.h.mk.w
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
o : HomOrthogonal s
α β γ : Type
inst✝² : Fintype α
inst✝¹ : Fintype β
inst✝ : Fintype γ
f : α → ι
g : β → ι
h : γ → ι
z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)
w : (⨁ fun b => s (g b)) ⟶ ⨁ fun c => s (h c)
c : γ
a : α
j_property✝ : a ∈ (fun a => f a) ⁻¹' {(fun b => h b) c}
j_property : f a = h c
x✝ : β
h✝ : x✝ ∈ (fun a => g a) ⁻¹' {h c}
⊢ eqToHom (_ : s (h c) = s (f ↑{ val := a, property := j_property✝ })) ≫
      biproduct.ι (fun a => s (f a)) a ≫
        z ≫
          ((biproduct.π (fun b => s (g b)) x✝ ≫ biproduct.ι (fun b => s (g b)) x✝) ≫ w) ≫
            biproduct.π (fun b => s (h b)) c =
    eqToHom (_ : s (h c) = s (f ↑{ val := a, property := j_property✝ })) ≫
      biproduct.ι (fun a => s (f a)) a ≫
        z ≫
          biproduct.π (fun b => s (g b)) ↑{ val := x✝, property := h✝ } ≫
            biproduct.ι (fun a => s (g a)) ↑{ val := x✝, property := h✝ } ≫ w ≫ biproduct.π (fun b => s (h b)) c
[PROOFSTEP]
simp
[GOAL]
case a.mk.refl.h.mk.w'
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
o : HomOrthogonal s
α β γ : Type
inst✝² : Fintype α
inst✝¹ : Fintype β
inst✝ : Fintype γ
f : α → ι
g : β → ι
h : γ → ι
z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)
w : (⨁ fun b => s (g b)) ⟶ ⨁ fun c => s (h c)
c : γ
a : α
j_property✝ : a ∈ (fun a => f a) ⁻¹' {(fun b => h b) c}
j_property : f a = h c
⊢ ∀ (x : β),
    ¬x ∈ (fun a => g a) ⁻¹' {h c} →
      eqToHom (_ : s (h c) = s (f ↑{ val := a, property := j_property✝ })) ≫
          biproduct.ι (fun a => s (f a)) a ≫
            z ≫
              ((biproduct.π (fun b => s (g b)) x ≫ biproduct.ι (fun b => s (g b)) x) ≫ w) ≫
                biproduct.π (fun b => s (h b)) c =
        0
[PROOFSTEP]
intro b nm
[GOAL]
case a.mk.refl.h.mk.w'
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
o : HomOrthogonal s
α β γ : Type
inst✝² : Fintype α
inst✝¹ : Fintype β
inst✝ : Fintype γ
f : α → ι
g : β → ι
h : γ → ι
z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)
w : (⨁ fun b => s (g b)) ⟶ ⨁ fun c => s (h c)
c : γ
a : α
j_property✝ : a ∈ (fun a => f a) ⁻¹' {(fun b => h b) c}
j_property : f a = h c
b : β
nm : ¬b ∈ (fun a => g a) ⁻¹' {h c}
⊢ eqToHom (_ : s (h c) = s (f ↑{ val := a, property := j_property✝ })) ≫
      biproduct.ι (fun a => s (f a)) a ≫
        z ≫
          ((biproduct.π (fun b => s (g b)) b ≫ biproduct.ι (fun b => s (g b)) b) ≫ w) ≫
            biproduct.π (fun b => s (h b)) c =
    0
[PROOFSTEP]
simp only [Set.mem_preimage, Set.mem_singleton_iff] at nm 
[GOAL]
case a.mk.refl.h.mk.w'
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
o : HomOrthogonal s
α β γ : Type
inst✝² : Fintype α
inst✝¹ : Fintype β
inst✝ : Fintype γ
f : α → ι
g : β → ι
h : γ → ι
z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)
w : (⨁ fun b => s (g b)) ⟶ ⨁ fun c => s (h c)
c : γ
a : α
j_property✝ : a ∈ (fun a => f a) ⁻¹' {(fun b => h b) c}
j_property : f a = h c
b : β
nm : ¬g b = h c
⊢ eqToHom (_ : s (h c) = s (f ↑{ val := a, property := j_property✝ })) ≫
      biproduct.ι (fun a => s (f a)) a ≫
        z ≫
          ((biproduct.π (fun b => s (g b)) b ≫ biproduct.ι (fun b => s (g b)) b) ≫ w) ≫
            biproduct.π (fun b => s (h b)) c =
    0
[PROOFSTEP]
simp only [Category.assoc]
  -- porting note: this used to be 4 times `convert comp_zero`
[GOAL]
case a.mk.refl.h.mk.w'
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
o : HomOrthogonal s
α β γ : Type
inst✝² : Fintype α
inst✝¹ : Fintype β
inst✝ : Fintype γ
f : α → ι
g : β → ι
h : γ → ι
z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)
w : (⨁ fun b => s (g b)) ⟶ ⨁ fun c => s (h c)
c : γ
a : α
j_property✝ : a ∈ (fun a => f a) ⁻¹' {(fun b => h b) c}
j_property : f a = h c
b : β
nm : ¬g b = h c
⊢ eqToHom (_ : s (h c) = s (f ↑{ val := a, property := j_property✝ })) ≫
      biproduct.ι (fun a => s (f a)) a ≫
        z ≫ biproduct.π (fun b => s (g b)) b ≫ biproduct.ι (fun b => s (g b)) b ≫ w ≫ biproduct.π (fun b => s (h b)) c =
    0
[PROOFSTEP]
have : biproduct.ι (fun b ↦ s (g b)) b ≫ w ≫ biproduct.π (fun b ↦ s (h b)) c = 0 := by apply o.eq_zero nm
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
o : HomOrthogonal s
α β γ : Type
inst✝² : Fintype α
inst✝¹ : Fintype β
inst✝ : Fintype γ
f : α → ι
g : β → ι
h : γ → ι
z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)
w : (⨁ fun b => s (g b)) ⟶ ⨁ fun c => s (h c)
c : γ
a : α
j_property✝ : a ∈ (fun a => f a) ⁻¹' {(fun b => h b) c}
j_property : f a = h c
b : β
nm : ¬g b = h c
⊢ biproduct.ι (fun b => s (g b)) b ≫ w ≫ biproduct.π (fun b => s (h b)) c = 0
[PROOFSTEP]
apply o.eq_zero nm
[GOAL]
case a.mk.refl.h.mk.w'
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
o : HomOrthogonal s
α β γ : Type
inst✝² : Fintype α
inst✝¹ : Fintype β
inst✝ : Fintype γ
f : α → ι
g : β → ι
h : γ → ι
z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)
w : (⨁ fun b => s (g b)) ⟶ ⨁ fun c => s (h c)
c : γ
a : α
j_property✝ : a ∈ (fun a => f a) ⁻¹' {(fun b => h b) c}
j_property : f a = h c
b : β
nm : ¬g b = h c
this : biproduct.ι (fun b => s (g b)) b ≫ w ≫ biproduct.π (fun b => s (h b)) c = 0
⊢ eqToHom (_ : s (h c) = s (f ↑{ val := a, property := j_property✝ })) ≫
      biproduct.ι (fun a => s (f a)) a ≫
        z ≫ biproduct.π (fun b => s (g b)) b ≫ biproduct.ι (fun b => s (g b)) b ≫ w ≫ biproduct.π (fun b => s (h b)) c =
    0
[PROOFSTEP]
simp only [this, comp_zero]
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁵ : Preadditive C
inst✝⁴ : HasFiniteBiproducts C
R : Type u_2
inst✝³ : Semiring R
inst✝² : Linear R C
o : HomOrthogonal s
α β : Type
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ι
g : β → ι
src✝ : ((⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)) ≃+
  ((i : ι) → Matrix (↑((fun b => g b) ⁻¹' {i})) (↑((fun a => f a) ⁻¹' {i})) (End (s i))) :=
  matrixDecompositionAddEquiv o
w : R
z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)
⊢ AddHom.toFun
      { toFun := src✝.toFun,
        map_add' :=
          (_ :
            ∀ (x y : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)),
              Equiv.toFun src✝.toEquiv (x + y) = Equiv.toFun src✝.toEquiv x + Equiv.toFun src✝.toEquiv y) }
      (w • z) =
    ↑(RingHom.id R) w •
      AddHom.toFun
        { toFun := src✝.toFun,
          map_add' :=
            (_ :
              ∀ (x y : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)),
                Equiv.toFun src✝.toEquiv (x + y) = Equiv.toFun src✝.toEquiv x + Equiv.toFun src✝.toEquiv y) }
        z
[PROOFSTEP]
ext
[GOAL]
case h.a.h
C : Type u
inst✝⁶ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁵ : Preadditive C
inst✝⁴ : HasFiniteBiproducts C
R : Type u_2
inst✝³ : Semiring R
inst✝² : Linear R C
o : HomOrthogonal s
α β : Type
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ι
g : β → ι
src✝ : ((⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)) ≃+
  ((i : ι) → Matrix (↑((fun b => g b) ⁻¹' {i})) (↑((fun a => f a) ⁻¹' {i})) (End (s i))) :=
  matrixDecompositionAddEquiv o
w : R
z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)
x✝¹ : ι
i✝ : ↑(g ⁻¹' {x✝¹})
x✝ : ↑(f ⁻¹' {x✝¹})
⊢ AddHom.toFun
      { toFun := src✝.toFun,
        map_add' :=
          (_ :
            ∀ (x y : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)),
              Equiv.toFun src✝.toEquiv (x + y) = Equiv.toFun src✝.toEquiv x + Equiv.toFun src✝.toEquiv y) }
      (w • z) x✝¹ i✝ x✝ =
    (↑(RingHom.id R) w •
        AddHom.toFun
          { toFun := src✝.toFun,
            map_add' :=
              (_ :
                ∀ (x y : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)),
                  Equiv.toFun src✝.toEquiv (x + y) = Equiv.toFun src✝.toEquiv x + Equiv.toFun src✝.toEquiv y) }
          z)
      x✝¹ i✝ x✝
[PROOFSTEP]
dsimp [biproduct.components]
[GOAL]
case h.a.h
C : Type u
inst✝⁶ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁵ : Preadditive C
inst✝⁴ : HasFiniteBiproducts C
R : Type u_2
inst✝³ : Semiring R
inst✝² : Linear R C
o : HomOrthogonal s
α β : Type
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ι
g : β → ι
src✝ : ((⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)) ≃+
  ((i : ι) → Matrix (↑((fun b => g b) ⁻¹' {i})) (↑((fun a => f a) ⁻¹' {i})) (End (s i))) :=
  matrixDecompositionAddEquiv o
w : R
z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)
x✝¹ : ι
i✝ : ↑(g ⁻¹' {x✝¹})
x✝ : ↑(f ⁻¹' {x✝¹})
⊢ eqToHom (_ : s x✝¹ = s (f ↑x✝)) ≫
      (biproduct.ι (fun a => s (f a)) ↑x✝ ≫ (w • z) ≫ biproduct.π (fun b => s (g b)) ↑i✝) ≫
        eqToHom (_ : s (g ↑i✝) = s x✝¹) =
    w •
      eqToHom (_ : s x✝¹ = s (f ↑x✝)) ≫
        (biproduct.ι (fun a => s (f a)) ↑x✝ ≫ z ≫ biproduct.π (fun b => s (g b)) ↑i✝) ≫ eqToHom (_ : s (g ↑i✝) = s x✝¹)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ι
g : β → ι
i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)
⊢ ∃ e, ∀ (a : α), g (↑e a) = f a
[PROOFSTEP]
refine' ⟨Equiv.ofPreimageEquiv _, fun a => Equiv.ofPreimageEquiv_map _ _⟩
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ι
g : β → ι
i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)
⊢ (c : ι) → ↑((fun a => f a) ⁻¹' {c}) ≃ ↑(g ⁻¹' {c})
[PROOFSTEP]
intro c
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ι
g : β → ι
i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)
c : ι
⊢ ↑((fun a => f a) ⁻¹' {c}) ≃ ↑(g ⁻¹' {c})
[PROOFSTEP]
apply Nonempty.some
[GOAL]
case h
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ι
g : β → ι
i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)
c : ι
⊢ Nonempty (↑((fun a => f a) ⁻¹' {c}) ≃ ↑(g ⁻¹' {c}))
[PROOFSTEP]
apply Cardinal.eq.1
[GOAL]
case h
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ι
g : β → ι
i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)
c : ι
⊢ Cardinal.mk ↑((fun a => f a) ⁻¹' {c}) = Cardinal.mk ↑(g ⁻¹' {c})
[PROOFSTEP]
simp only [Cardinal.mk_fintype, Nat.cast_inj]
[GOAL]
case h
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ι
g : β → ι
i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)
c : ι
⊢ Fintype.card ↑((fun a => f a) ⁻¹' {c}) = Fintype.card ↑(g ⁻¹' {c})
[PROOFSTEP]
exact
  Matrix.square_of_invertible (o.matrixDecomposition i.inv c) (o.matrixDecomposition i.hom c)
    (by
      rw [← o.matrixDecomposition_comp]
      simp)
    (by
      rw [← o.matrixDecomposition_comp]
      simp)
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ι
g : β → ι
i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)
c : ι
⊢ ↑(matrixDecomposition o) i.inv c * ↑(matrixDecomposition o) i.hom c = 1
[PROOFSTEP]
rw [← o.matrixDecomposition_comp]
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ι
g : β → ι
i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)
c : ι
⊢ ↑(matrixDecomposition o) (i.hom ≫ i.inv) c = 1
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ι
g : β → ι
i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)
c : ι
⊢ ↑(matrixDecomposition o) i.hom c * ↑(matrixDecomposition o) i.inv c = 1
[PROOFSTEP]
rw [← o.matrixDecomposition_comp]
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ι
g : β → ι
i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)
c : ι
⊢ ↑(matrixDecomposition o) (i.inv ≫ i.hom) c = 1
[PROOFSTEP]
simp
