[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


[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : Preadditive C
inst✝² : HasKernels C
X Y : C
inst✝¹ : Simple X
inst✝ : Simple Y
f : X ⟶ Y
I : IsIso f
⊢ f ≠ 0
[PROOFSTEP]
intro h
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : Preadditive C
inst✝² : HasKernels C
X Y : C
inst✝¹ : Simple X
inst✝ : Simple Y
f : X ⟶ Y
I : IsIso f
h : f = 0
⊢ False
[PROOFSTEP]
apply id_nonzero X
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : Preadditive C
inst✝² : HasKernels C
X Y : C
inst✝¹ : Simple X
inst✝ : Simple Y
f : X ⟶ Y
I : IsIso f
h : f = 0
⊢ 𝟙 X = 0
[PROOFSTEP]
simp only [← IsIso.hom_inv_id f, h, zero_comp]
[GOAL]
C : Type u_1
inst✝³ : Category.{?u.3173, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasKernels C
X : C
inst✝ : Simple X
⊢ DivisionRing (End X)
[PROOFSTEP]
classical exact
  {
    (inferInstance :
      Ring (End X)) with
    inv := fun f =>
      if h : f = 0 then 0
      else
        haveI := isIso_of_hom_simple h
        inv f
    exists_pair_ne := ⟨𝟙 X, 0, id_nonzero _⟩
    inv_zero := dif_pos rfl
    mul_inv_cancel := fun f h => by
      dsimp
      rw [dif_neg h]
      haveI := isIso_of_hom_simple h
      exact IsIso.inv_hom_id f }
[GOAL]
C : Type u_1
inst✝³ : Category.{?u.3173, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasKernels C
X : C
inst✝ : Simple X
⊢ DivisionRing (End X)
[PROOFSTEP]
exact
  {
    (inferInstance :
      Ring (End X)) with
    inv := fun f =>
      if h : f = 0 then 0
      else
        haveI := isIso_of_hom_simple h
        inv f
    exists_pair_ne := ⟨𝟙 X, 0, id_nonzero _⟩
    inv_zero := dif_pos rfl
    mul_inv_cancel := fun f h => by
      dsimp
      rw [dif_neg h]
      haveI := isIso_of_hom_simple h
      exact IsIso.inv_hom_id f }
[GOAL]
C : Type u_1
inst✝³ : Category.{?u.4991, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasKernels C
X : C
inst✝ : Simple X
src✝ : Ring (End X) := inferInstance
f : End X
h : f ≠ 0
⊢ f * f⁻¹ = 1
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝³ : Category.{?u.4991, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasKernels C
X : C
inst✝ : Simple X
src✝ : Ring (End X) := inferInstance
f : End X
h : f ≠ 0
⊢ (if h : f = 0 then 0 else inv f) ≫ f = 𝟙 X
[PROOFSTEP]
rw [dif_neg h]
[GOAL]
C : Type u_1
inst✝³ : Category.{?u.4991, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasKernels C
X : C
inst✝ : Simple X
src✝ : Ring (End X) := inferInstance
f : End X
h : f ≠ 0
⊢ inv f ≫ f = 𝟙 X
[PROOFSTEP]
haveI := isIso_of_hom_simple h
[GOAL]
C : Type u_1
inst✝³ : Category.{?u.4991, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasKernels C
X : C
inst✝ : Simple X
src✝ : Ring (End X) := inferInstance
f : End X
h : f ≠ 0
this : IsIso f
⊢ inv f ≫ f = 𝟙 X
[PROOFSTEP]
exact IsIso.inv_hom_id f
[GOAL]
C : Type u_1
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Preadditive C
𝕜 : Type u_2
inst✝⁴ : DivisionRing 𝕜
inst✝³ : HasKernels C
inst✝² : Linear 𝕜 C
X Y : C
inst✝¹ : Simple X
inst✝ : Simple Y
h : (X ≅ Y) → False
f : X ⟶ Y
⊢ f = 0
[PROOFSTEP]
have p := not_congr (isIso_iff_nonzero f)
[GOAL]
C : Type u_1
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Preadditive C
𝕜 : Type u_2
inst✝⁴ : DivisionRing 𝕜
inst✝³ : HasKernels C
inst✝² : Linear 𝕜 C
X Y : C
inst✝¹ : Simple X
inst✝ : Simple Y
h : (X ≅ Y) → False
f : X ⟶ Y
p : ¬IsIso f ↔ ¬f ≠ 0
⊢ f = 0
[PROOFSTEP]
simp only [Classical.not_not, Ne.def] at p
[GOAL]
C : Type u_1
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Preadditive C
𝕜 : Type u_2
inst✝⁴ : DivisionRing 𝕜
inst✝³ : HasKernels C
inst✝² : Linear 𝕜 C
X Y : C
inst✝¹ : Simple X
inst✝ : Simple Y
h : (X ≅ Y) → False
f : X ⟶ Y
p : ¬IsIso f ↔ f = 0
⊢ f = 0
[PROOFSTEP]
refine' p.mp fun _ => h (asIso f)
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Preadditive C
𝕜 : Type u_2
inst✝² : Field 𝕜
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Linear 𝕜 C
X : C
isIso_iff_nonzero : ∀ (f : X ⟶ X), IsIso f ↔ f ≠ 0
I : FiniteDimensional 𝕜 (X ⟶ X)
⊢ finrank 𝕜 (X ⟶ X) = 1
[PROOFSTEP]
have id_nonzero := (isIso_iff_nonzero (𝟙 X)).mp (by infer_instance)
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Preadditive C
𝕜 : Type u_2
inst✝² : Field 𝕜
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Linear 𝕜 C
X : C
isIso_iff_nonzero : ∀ (f : X ⟶ X), IsIso f ↔ f ≠ 0
I : FiniteDimensional 𝕜 (X ⟶ X)
⊢ IsIso (𝟙 X)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Preadditive C
𝕜 : Type u_2
inst✝² : Field 𝕜
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Linear 𝕜 C
X : C
isIso_iff_nonzero : ∀ (f : X ⟶ X), IsIso f ↔ f ≠ 0
I : FiniteDimensional 𝕜 (X ⟶ X)
id_nonzero : 𝟙 X ≠ 0
⊢ finrank 𝕜 (X ⟶ X) = 1
[PROOFSTEP]
refine' finrank_eq_one (𝟙 X) id_nonzero _
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Preadditive C
𝕜 : Type u_2
inst✝² : Field 𝕜
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Linear 𝕜 C
X : C
isIso_iff_nonzero : ∀ (f : X ⟶ X), IsIso f ↔ f ≠ 0
I : FiniteDimensional 𝕜 (X ⟶ X)
id_nonzero : 𝟙 X ≠ 0
⊢ ∀ (w : X ⟶ X), ∃ c, c • 𝟙 X = w
[PROOFSTEP]
intro f
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Preadditive C
𝕜 : Type u_2
inst✝² : Field 𝕜
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Linear 𝕜 C
X : C
isIso_iff_nonzero : ∀ (f : X ⟶ X), IsIso f ↔ f ≠ 0
I : FiniteDimensional 𝕜 (X ⟶ X)
id_nonzero : 𝟙 X ≠ 0
f : X ⟶ X
⊢ ∃ c, c • 𝟙 X = f
[PROOFSTEP]
have : Nontrivial (End X) := nontrivial_of_ne _ _ id_nonzero
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Preadditive C
𝕜 : Type u_2
inst✝² : Field 𝕜
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Linear 𝕜 C
X : C
isIso_iff_nonzero : ∀ (f : X ⟶ X), IsIso f ↔ f ≠ 0
I : FiniteDimensional 𝕜 (X ⟶ X)
id_nonzero : 𝟙 X ≠ 0
f : X ⟶ X
this : Nontrivial (End X)
⊢ ∃ c, c • 𝟙 X = f
[PROOFSTEP]
have : FiniteDimensional 𝕜 (End X) := I
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Preadditive C
𝕜 : Type u_2
inst✝² : Field 𝕜
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Linear 𝕜 C
X : C
isIso_iff_nonzero : ∀ (f : X ⟶ X), IsIso f ↔ f ≠ 0
I : FiniteDimensional 𝕜 (X ⟶ X)
id_nonzero : 𝟙 X ≠ 0
f : X ⟶ X
this✝ : Nontrivial (End X)
this : FiniteDimensional 𝕜 (End X)
⊢ ∃ c, c • 𝟙 X = f
[PROOFSTEP]
obtain ⟨c, nu⟩ := spectrum.nonempty_of_isAlgClosed_of_finiteDimensional 𝕜 (End.of f)
[GOAL]
case intro
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Preadditive C
𝕜 : Type u_2
inst✝² : Field 𝕜
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Linear 𝕜 C
X : C
isIso_iff_nonzero : ∀ (f : X ⟶ X), IsIso f ↔ f ≠ 0
I : FiniteDimensional 𝕜 (X ⟶ X)
id_nonzero : 𝟙 X ≠ 0
f : X ⟶ X
this✝ : Nontrivial (End X)
this : FiniteDimensional 𝕜 (End X)
c : 𝕜
nu : c ∈ spectrum 𝕜 (End.of f)
⊢ ∃ c, c • 𝟙 X = f
[PROOFSTEP]
use c
[GOAL]
case h
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Preadditive C
𝕜 : Type u_2
inst✝² : Field 𝕜
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Linear 𝕜 C
X : C
isIso_iff_nonzero : ∀ (f : X ⟶ X), IsIso f ↔ f ≠ 0
I : FiniteDimensional 𝕜 (X ⟶ X)
id_nonzero : 𝟙 X ≠ 0
f : X ⟶ X
this✝ : Nontrivial (End X)
this : FiniteDimensional 𝕜 (End X)
c : 𝕜
nu : c ∈ spectrum 𝕜 (End.of f)
⊢ c • 𝟙 X = f
[PROOFSTEP]
rw [spectrum.mem_iff, IsUnit.sub_iff, isUnit_iff_isIso, isIso_iff_nonzero, Ne.def, Classical.not_not, sub_eq_zero,
  Algebra.algebraMap_eq_smul_one] at nu
[GOAL]
case h
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Preadditive C
𝕜 : Type u_2
inst✝² : Field 𝕜
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Linear 𝕜 C
X : C
isIso_iff_nonzero : ∀ (f : X ⟶ X), IsIso f ↔ f ≠ 0
I : FiniteDimensional 𝕜 (X ⟶ X)
id_nonzero : 𝟙 X ≠ 0
f : X ⟶ X
this✝ : Nontrivial (End X)
this : FiniteDimensional 𝕜 (End X)
c : 𝕜
nu : End.of f = c • 1
⊢ c • 𝟙 X = f
[PROOFSTEP]
exact nu.symm
[GOAL]
C : Type u_1
inst✝⁶ : Category.{?u.16907, u_1} C
inst✝⁵ : Preadditive C
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : IsAlgClosed 𝕜
inst✝² : Linear 𝕜 C
inst✝¹ : HasKernels C
X : C
inst✝ : Simple X
I : FiniteDimensional 𝕜 (X ⟶ X)
⊢ Field (End X)
[PROOFSTEP]
classical exact
  { (inferInstance : DivisionRing (End X)) with
    mul_comm := fun f g => by
      obtain ⟨c, rfl⟩ := endomorphism_simple_eq_smul_id 𝕜 f
      obtain ⟨d, rfl⟩ := endomorphism_simple_eq_smul_id 𝕜 g
      simp [← mul_smul, mul_comm c d] }
[GOAL]
C : Type u_1
inst✝⁶ : Category.{?u.16907, u_1} C
inst✝⁵ : Preadditive C
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : IsAlgClosed 𝕜
inst✝² : Linear 𝕜 C
inst✝¹ : HasKernels C
X : C
inst✝ : Simple X
I : FiniteDimensional 𝕜 (X ⟶ X)
⊢ Field (End X)
[PROOFSTEP]
exact
  { (inferInstance : DivisionRing (End X)) with
    mul_comm := fun f g => by
      obtain ⟨c, rfl⟩ := endomorphism_simple_eq_smul_id 𝕜 f
      obtain ⟨d, rfl⟩ := endomorphism_simple_eq_smul_id 𝕜 g
      simp [← mul_smul, mul_comm c d] }
[GOAL]
C : Type u_1
inst✝⁶ : Category.{?u.16907, u_1} C
inst✝⁵ : Preadditive C
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : IsAlgClosed 𝕜
inst✝² : Linear 𝕜 C
inst✝¹ : HasKernels C
X : C
inst✝ : Simple X
I : FiniteDimensional 𝕜 (X ⟶ X)
src✝ : DivisionRing (End X) := inferInstance
f g : End X
⊢ f * g = g * f
[PROOFSTEP]
obtain ⟨c, rfl⟩ := endomorphism_simple_eq_smul_id 𝕜 f
[GOAL]
case intro
C : Type u_1
inst✝⁶ : Category.{?u.16907, u_1} C
inst✝⁵ : Preadditive C
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : IsAlgClosed 𝕜
inst✝² : Linear 𝕜 C
inst✝¹ : HasKernels C
X : C
inst✝ : Simple X
I : FiniteDimensional 𝕜 (X ⟶ X)
src✝ : DivisionRing (End X) := inferInstance
g : End X
c : 𝕜
⊢ c • 𝟙 X * g = g * c • 𝟙 X
[PROOFSTEP]
obtain ⟨d, rfl⟩ := endomorphism_simple_eq_smul_id 𝕜 g
[GOAL]
case intro.intro
C : Type u_1
inst✝⁶ : Category.{?u.16907, u_1} C
inst✝⁵ : Preadditive C
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : IsAlgClosed 𝕜
inst✝² : Linear 𝕜 C
inst✝¹ : HasKernels C
X : C
inst✝ : Simple X
I : FiniteDimensional 𝕜 (X ⟶ X)
src✝ : DivisionRing (End X) := inferInstance
c d : 𝕜
⊢ c • 𝟙 X * d • 𝟙 X = d • 𝟙 X * c • 𝟙 X
[PROOFSTEP]
simp [← mul_smul, mul_comm c d]
[GOAL]
C : Type u_1
inst✝⁸ : Category.{u_3, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : FiniteDimensional 𝕜 (X ⟶ X)
inst✝¹ : Simple X
inst✝ : Simple Y
⊢ finrank 𝕜 (X ⟶ Y) ≤ 1
[PROOFSTEP]
obtain (h | h) := subsingleton_or_nontrivial (X ⟶ Y)
[GOAL]
case inl
C : Type u_1
inst✝⁸ : Category.{u_3, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : FiniteDimensional 𝕜 (X ⟶ X)
inst✝¹ : Simple X
inst✝ : Simple Y
h : Subsingleton (X ⟶ Y)
⊢ finrank 𝕜 (X ⟶ Y) ≤ 1
[PROOFSTEP]
rw [finrank_zero_of_subsingleton]
[GOAL]
case inl
C : Type u_1
inst✝⁸ : Category.{u_3, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : FiniteDimensional 𝕜 (X ⟶ X)
inst✝¹ : Simple X
inst✝ : Simple Y
h : Subsingleton (X ⟶ Y)
⊢ 0 ≤ 1
[PROOFSTEP]
exact zero_le_one
[GOAL]
case inr
C : Type u_1
inst✝⁸ : Category.{u_3, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : FiniteDimensional 𝕜 (X ⟶ X)
inst✝¹ : Simple X
inst✝ : Simple Y
h : Nontrivial (X ⟶ Y)
⊢ finrank 𝕜 (X ⟶ Y) ≤ 1
[PROOFSTEP]
obtain ⟨f, nz⟩ := (nontrivial_iff_exists_ne 0).mp h
[GOAL]
case inr.intro
C : Type u_1
inst✝⁸ : Category.{u_3, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : FiniteDimensional 𝕜 (X ⟶ X)
inst✝¹ : Simple X
inst✝ : Simple Y
h : Nontrivial (X ⟶ Y)
f : X ⟶ Y
nz : f ≠ 0
⊢ finrank 𝕜 (X ⟶ Y) ≤ 1
[PROOFSTEP]
haveI fi := (isIso_iff_nonzero f).mpr nz
[GOAL]
case inr.intro
C : Type u_1
inst✝⁸ : Category.{u_3, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : FiniteDimensional 𝕜 (X ⟶ X)
inst✝¹ : Simple X
inst✝ : Simple Y
h : Nontrivial (X ⟶ Y)
f : X ⟶ Y
nz : f ≠ 0
fi : IsIso f
⊢ finrank 𝕜 (X ⟶ Y) ≤ 1
[PROOFSTEP]
refine' finrank_le_one f _
[GOAL]
case inr.intro
C : Type u_1
inst✝⁸ : Category.{u_3, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : FiniteDimensional 𝕜 (X ⟶ X)
inst✝¹ : Simple X
inst✝ : Simple Y
h : Nontrivial (X ⟶ Y)
f : X ⟶ Y
nz : f ≠ 0
fi : IsIso f
⊢ ∀ (w : X ⟶ Y), ∃ c, c • f = w
[PROOFSTEP]
intro g
[GOAL]
case inr.intro
C : Type u_1
inst✝⁸ : Category.{u_3, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : FiniteDimensional 𝕜 (X ⟶ X)
inst✝¹ : Simple X
inst✝ : Simple Y
h : Nontrivial (X ⟶ Y)
f : X ⟶ Y
nz : f ≠ 0
fi : IsIso f
g : X ⟶ Y
⊢ ∃ c, c • f = g
[PROOFSTEP]
obtain ⟨c, w⟩ := endomorphism_simple_eq_smul_id 𝕜 (g ≫ inv f)
[GOAL]
case inr.intro.intro
C : Type u_1
inst✝⁸ : Category.{u_3, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : FiniteDimensional 𝕜 (X ⟶ X)
inst✝¹ : Simple X
inst✝ : Simple Y
h : Nontrivial (X ⟶ Y)
f : X ⟶ Y
nz : f ≠ 0
fi : IsIso f
g : X ⟶ Y
c : 𝕜
w : c • 𝟙 X = g ≫ inv f
⊢ ∃ c, c • f = g
[PROOFSTEP]
exact ⟨c, by simpa using w =≫ f⟩
[GOAL]
C : Type u_1
inst✝⁸ : Category.{u_3, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : FiniteDimensional 𝕜 (X ⟶ X)
inst✝¹ : Simple X
inst✝ : Simple Y
h : Nontrivial (X ⟶ Y)
f : X ⟶ Y
nz : f ≠ 0
fi : IsIso f
g : X ⟶ Y
c : 𝕜
w : c • 𝟙 X = g ≫ inv f
⊢ c • f = g
[PROOFSTEP]
simpa using w =≫ f
[GOAL]
C : Type u_1
inst✝⁹ : Category.{u_3, u_1} C
inst✝⁸ : Preadditive C
𝕜 : Type u_2
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
⊢ finrank 𝕜 (X ⟶ Y) = 1 ↔ Nonempty (X ≅ Y)
[PROOFSTEP]
fconstructor
[GOAL]
case mp
C : Type u_1
inst✝⁹ : Category.{u_3, u_1} C
inst✝⁸ : Preadditive C
𝕜 : Type u_2
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
⊢ finrank 𝕜 (X ⟶ Y) = 1 → Nonempty (X ≅ Y)
[PROOFSTEP]
intro h
[GOAL]
case mp
C : Type u_1
inst✝⁹ : Category.{u_3, u_1} C
inst✝⁸ : Preadditive C
𝕜 : Type u_2
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
h : finrank 𝕜 (X ⟶ Y) = 1
⊢ Nonempty (X ≅ Y)
[PROOFSTEP]
rw [finrank_eq_one_iff'] at h
[GOAL]
case mp
C : Type u_1
inst✝⁹ : Category.{u_3, u_1} C
inst✝⁸ : Preadditive C
𝕜 : Type u_2
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
h : ∃ v _n, ∀ (w : X ⟶ Y), ∃ c, c • v = w
⊢ Nonempty (X ≅ Y)
[PROOFSTEP]
obtain ⟨f, nz, -⟩ := h
[GOAL]
case mp.intro.intro
C : Type u_1
inst✝⁹ : Category.{u_3, u_1} C
inst✝⁸ : Preadditive C
𝕜 : Type u_2
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
f : X ⟶ Y
nz : f ≠ 0
⊢ Nonempty (X ≅ Y)
[PROOFSTEP]
rw [← isIso_iff_nonzero] at nz
[GOAL]
case mp.intro.intro
C : Type u_1
inst✝⁹ : Category.{u_3, u_1} C
inst✝⁸ : Preadditive C
𝕜 : Type u_2
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
f : X ⟶ Y
nz : IsIso f
⊢ Nonempty (X ≅ Y)
[PROOFSTEP]
exact ⟨asIso f⟩
[GOAL]
case mpr
C : Type u_1
inst✝⁹ : Category.{u_3, u_1} C
inst✝⁸ : Preadditive C
𝕜 : Type u_2
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
⊢ Nonempty (X ≅ Y) → finrank 𝕜 (X ⟶ Y) = 1
[PROOFSTEP]
rintro ⟨f⟩
[GOAL]
case mpr.intro
C : Type u_1
inst✝⁹ : Category.{u_3, u_1} C
inst✝⁸ : Preadditive C
𝕜 : Type u_2
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
f : X ≅ Y
⊢ finrank 𝕜 (X ⟶ Y) = 1
[PROOFSTEP]
have le_one := finrank_hom_simple_simple_le_one 𝕜 X Y
[GOAL]
case mpr.intro
C : Type u_1
inst✝⁹ : Category.{u_3, u_1} C
inst✝⁸ : Preadditive C
𝕜 : Type u_2
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
f : X ≅ Y
le_one : finrank 𝕜 (X ⟶ Y) ≤ 1
⊢ finrank 𝕜 (X ⟶ Y) = 1
[PROOFSTEP]
have zero_lt : 0 < finrank 𝕜 (X ⟶ Y) :=
  finrank_pos_iff_exists_ne_zero.mpr ⟨f.hom, (isIso_iff_nonzero f.hom).mp inferInstance⟩
[GOAL]
case mpr.intro
C : Type u_1
inst✝⁹ : Category.{u_3, u_1} C
inst✝⁸ : Preadditive C
𝕜 : Type u_2
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
f : X ≅ Y
le_one : finrank 𝕜 (X ⟶ Y) ≤ 1
zero_lt : 0 < finrank 𝕜 (X ⟶ Y)
⊢ finrank 𝕜 (X ⟶ Y) = 1
[PROOFSTEP]
linarith
[GOAL]
C : Type u_1
inst✝⁹ : Category.{u_3, u_1} C
inst✝⁸ : Preadditive C
𝕜 : Type u_2
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
⊢ finrank 𝕜 (X ⟶ Y) = 0 ↔ IsEmpty (X ≅ Y)
[PROOFSTEP]
rw [← not_nonempty_iff, ← not_congr (finrank_hom_simple_simple_eq_one_iff 𝕜 X Y)]
[GOAL]
C : Type u_1
inst✝⁹ : Category.{u_3, u_1} C
inst✝⁸ : Preadditive C
𝕜 : Type u_2
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
⊢ finrank 𝕜 (X ⟶ Y) = 0 ↔ ¬finrank 𝕜 (X ⟶ Y) = 1
[PROOFSTEP]
refine' ⟨fun h => by rw [h]; simp, fun h => _⟩
[GOAL]
C : Type u_1
inst✝⁹ : Category.{u_3, u_1} C
inst✝⁸ : Preadditive C
𝕜 : Type u_2
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
h : finrank 𝕜 (X ⟶ Y) = 0
⊢ ¬finrank 𝕜 (X ⟶ Y) = 1
[PROOFSTEP]
rw [h]
[GOAL]
C : Type u_1
inst✝⁹ : Category.{u_3, u_1} C
inst✝⁸ : Preadditive C
𝕜 : Type u_2
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
h : finrank 𝕜 (X ⟶ Y) = 0
⊢ ¬0 = 1
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝⁹ : Category.{u_3, u_1} C
inst✝⁸ : Preadditive C
𝕜 : Type u_2
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
h : ¬finrank 𝕜 (X ⟶ Y) = 1
⊢ finrank 𝕜 (X ⟶ Y) = 0
[PROOFSTEP]
have := finrank_hom_simple_simple_le_one 𝕜 X Y
[GOAL]
C : Type u_1
inst✝⁹ : Category.{u_3, u_1} C
inst✝⁸ : Preadditive C
𝕜 : Type u_2
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
h : ¬finrank 𝕜 (X ⟶ Y) = 1
this : finrank 𝕜 (X ⟶ Y) ≤ 1
⊢ finrank 𝕜 (X ⟶ Y) = 0
[PROOFSTEP]
interval_cases finrank 𝕜 (X ⟶ Y)
[GOAL]
case «0»
C : Type u_1
inst✝⁹ : Category.{u_3, u_1} C
inst✝⁸ : Preadditive C
𝕜 : Type u_2
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
h : ¬0 = 1
this : 0 ≤ 1
⊢ 0 = 0
[PROOFSTEP]
rfl
[GOAL]
case «1»
C : Type u_1
inst✝⁹ : Category.{u_3, u_1} C
inst✝⁸ : Preadditive C
𝕜 : Type u_2
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
h : ¬1 = 1
this : 1 ≤ 1
⊢ 1 = 0
[PROOFSTEP]
exact False.elim (h rfl)
[GOAL]
C : Type u_1
inst✝⁸ : Category.{u_3, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : ∀ (X Y : C), FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
⊢ finrank 𝕜 (X ⟶ Y) = if Nonempty (X ≅ Y) then 1 else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
C : Type u_1
inst✝⁸ : Category.{u_3, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : ∀ (X Y : C), FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
h : Nonempty (X ≅ Y)
⊢ finrank 𝕜 (X ⟶ Y) = 1
case neg
C : Type u_1
inst✝⁸ : Category.{u_3, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : ∀ (X Y : C), FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
h : ¬Nonempty (X ≅ Y)
⊢ finrank 𝕜 (X ⟶ Y) = 0
[PROOFSTEP]
exact (finrank_hom_simple_simple_eq_one_iff 𝕜 X Y).2 h
[GOAL]
case neg
C : Type u_1
inst✝⁸ : Category.{u_3, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : ∀ (X Y : C), FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
h : ¬Nonempty (X ≅ Y)
⊢ finrank 𝕜 (X ⟶ Y) = 0
[PROOFSTEP]
exact (finrank_hom_simple_simple_eq_zero_iff 𝕜 X Y).2 (not_nonempty_iff.mp h)


[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P : Karoubi (Karoubi C)
⊢ P.p.f ≫ P.p.f = P.p.f
[PROOFSTEP]
simpa only [hom_ext_iff, comp_f] using P.idem
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P Q : Karoubi (Karoubi C)
f : P ⟶ Q
⊢ P.p.f ≫ f.f.f = f.f.f ≫ Q.p.f
[PROOFSTEP]
simpa only [hom_ext_iff, comp_f] using p_comm f
[GOAL]
C : Type u_1
inst✝ : Category.{?u.1759, u_1} C
P : Karoubi (Karoubi C)
⊢ P.p.f ≫ P.p.f = P.p.f
[PROOFSTEP]
simpa only [hom_ext_iff] using P.idem
[GOAL]
C : Type u_1
inst✝ : Category.{?u.1759, u_1} C
X✝ Y✝ : Karoubi (Karoubi C)
f : X✝ ⟶ Y✝
⊢ f.f.f = ((fun P => Karoubi.mk P.X.X P.p.f) X✝).p ≫ f.f.f ≫ ((fun P => Karoubi.mk P.X.X P.p.f) Y✝).p
[PROOFSTEP]
simpa only [hom_ext_iff] using f.comm
[GOAL]
C : Type u_1
inst✝ : Category.{?u.7379, u_1} C
⊢ ∀ (X : Karoubi C), (𝟭 (Karoubi C)).obj X = (toKaroubi (Karoubi C) ⋙ inverse C).obj X
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
inst✝ : Category.{?u.7379, u_1} C
⊢ ∀ (X Y : Karoubi C) (f : X ⟶ Y),
    (𝟭 (Karoubi C)).map f =
      eqToHom (_ : (𝟭 (Karoubi C)).obj X = (toKaroubi (Karoubi C) ⋙ inverse C).obj X) ≫
        (toKaroubi (Karoubi C) ⋙ inverse C).map f ≫
          eqToHom (_ : (toKaroubi (Karoubi C) ⋙ inverse C).obj Y = (𝟭 (Karoubi C)).obj Y)
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
inst✝ : Category.{?u.11252, u_1} C
P : Karoubi (Karoubi C)
⊢ P.p.f = ((inverse C ⋙ toKaroubi (Karoubi C)).obj P).X.p ≫ P.p.f ≫ ((𝟭 (Karoubi (Karoubi C))).obj P).X.p
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝ : Category.{?u.11252, u_1} C
P : Karoubi (Karoubi C)
⊢ Hom.mk P.p.f = ((inverse C ⋙ toKaroubi (Karoubi C)).obj P).p ≫ Hom.mk P.p.f ≫ ((𝟭 (Karoubi (Karoubi C))).obj P).p
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝ : Category.{?u.11252, u_1} C
P : Karoubi (Karoubi C)
⊢ P.p.f = ((𝟭 (Karoubi (Karoubi C))).obj P).X.p ≫ P.p.f ≫ ((inverse C ⋙ toKaroubi (Karoubi C)).obj P).X.p
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝ : Category.{?u.11252, u_1} C
P : Karoubi (Karoubi C)
⊢ Hom.mk P.p.f = ((𝟭 (Karoubi (Karoubi C))).obj P).p ≫ Hom.mk P.p.f ≫ ((inverse C ⋙ toKaroubi (Karoubi C)).obj P).p
[PROOFSTEP]
simp


[GOAL]
C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive C
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : Additive F
J✝ : Type
inst✝ : Fintype J✝
f✝ : J✝ → C
b✝ : Bicone f✝
hb : Bicone.IsBilimit b✝
⊢ (Finset.sum Finset.univ fun j => Bicone.π (mapBicone F b✝) j ≫ Bicone.ι (mapBicone F b✝) j) = 𝟙 (mapBicone F b✝).pt
[PROOFSTEP]
simp_rw [F.mapBicone_π, F.mapBicone_ι, ← F.map_comp]
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive C
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : Additive F
J✝ : Type
inst✝ : Fintype J✝
f✝ : J✝ → C
b✝ : Bicone f✝
hb : Bicone.IsBilimit b✝
⊢ (Finset.sum Finset.univ fun x => F.map (Bicone.π b✝ x ≫ Bicone.ι b✝ x)) = 𝟙 (mapBicone F b✝).pt
[PROOFSTEP]
erw [← F.map_sum, ← F.map_id, IsBilimit.total hb]
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : HasBinaryBiproducts C
inst✝¹ : PreservesZeroMorphisms F
inst✝ : PreservesBinaryBiproducts F
X Y : C
f g : X ⟶ Y
⊢ F.map (f + g) = F.map f + F.map g
[PROOFSTEP]
rw [biprod.add_eq_lift_id_desc, F.map_comp, ← biprod.lift_mapBiprod, ← biprod.mapBiprod_hom_desc, Category.assoc,
  Iso.inv_hom_id_assoc, F.map_id, biprod.add_eq_lift_id_desc]
[GOAL]
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{?u.46335, u_1} C
inst✝³ : Category.{?u.46339, u_2} D
inst✝² : Preadditive C
inst✝¹ : Preadditive D
e : C ≌ D
inst✝ : Functor.Additive e.functor
f g : D
f✝ g✝ : f ⟶ g
⊢ e.functor.map (e.inverse.map (f✝ + g✝)) = e.functor.map (e.inverse.map f✝ + e.inverse.map g✝)
[PROOFSTEP]
simp


[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.4011, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P : Karoubi (HomologicalComplex C c)
n : ι
⊢ HomologicalComplex.Hom.f P.p n ≫ HomologicalComplex.Hom.f P.p n = HomologicalComplex.Hom.f P.p n
[PROOFSTEP]
simpa only [HomologicalComplex.comp_f] using HomologicalComplex.congr_hom P.idem n
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.4011, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P : Karoubi (HomologicalComplex C c)
i j : ι
hij : ¬ComplexShape.Rel c i j
⊢ (fun i j => Hom.mk (HomologicalComplex.Hom.f P.p i ≫ HomologicalComplex.d P.X i j)) i j = 0
[PROOFSTEP]
simp only [hom_eq_zero_iff, P.X.shape i j hij, Limits.comp_zero]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.4011, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P : Karoubi (HomologicalComplex C c)
i j : ι
hij : ¬ComplexShape.Rel c i j
⊢ HomologicalComplex.Hom.f P.p i ≫ HomologicalComplex.d P.X i j = 0
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.12005, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex (Karoubi C) c
i j k : ι
x✝¹ : ComplexShape.Rel c i j
x✝ : ComplexShape.Rel c j k
⊢ (fun i j => (HomologicalComplex.d K i j).f) i j ≫ (fun i j => (HomologicalComplex.d K i j).f) j k = 0
[PROOFSTEP]
simpa only [comp_f] using hom_eq_zero_iff.mp (K.d_comp_d i j k)
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.17622, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
K L : HomologicalComplex (Karoubi C) c
f : K ⟶ L
i j : ι
hij : ComplexShape.Rel c i j
⊢ (fun n => (HomologicalComplex.Hom.f f n).f) i ≫ HomologicalComplex.d (obj L).X i j =
    HomologicalComplex.d (obj K).X i j ≫ (fun n => (HomologicalComplex.Hom.f f n).f) j
[PROOFSTEP]
simpa only [comp_f] using hom_ext_iff.mp (f.comm' i j hij)
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.22640, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P : HomologicalComplex (Karoubi C) c
⊢ ((inverse ⋙ functor).obj P).X = ((𝟭 (HomologicalComplex (Karoubi C) c)).obj P).X
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.22640, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P : HomologicalComplex (Karoubi C) c
⊢ ∀ (i j : ι),
    ComplexShape.Rel c i j →
      HomologicalComplex.d ((inverse ⋙ functor).obj P) i j ≫
          eqToHom
            (_ :
              HomologicalComplex.X ((inverse ⋙ functor).obj P) j =
                HomologicalComplex.X ((𝟭 (HomologicalComplex (Karoubi C) c)).obj P) j) =
        eqToHom
            (_ :
              HomologicalComplex.X ((inverse ⋙ functor).obj P) i =
                HomologicalComplex.X ((𝟭 (HomologicalComplex (Karoubi C) c)).obj P) i) ≫
          HomologicalComplex.d ((𝟭 (HomologicalComplex (Karoubi C) c)).obj P) i j
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.22640, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
⊢ ∀ (X Y : HomologicalComplex (Karoubi C) c) (f : X ⟶ Y),
    (inverse ⋙ functor).map f =
      eqToHom (_ : (inverse ⋙ functor).obj X = (𝟭 (HomologicalComplex (Karoubi C) c)).obj X) ≫
        (𝟭 (HomologicalComplex (Karoubi C) c)).map f ≫
          eqToHom (_ : (𝟭 (HomologicalComplex (Karoubi C) c)).obj Y = (inverse ⋙ functor).obj Y)
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.35996, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P : Karoubi (HomologicalComplex C c)
i j : ι
x✝ : ComplexShape.Rel c i j
⊢ (fun n => HomologicalComplex.Hom.f P.p n) i ≫ HomologicalComplex.d ((functor ⋙ inverse).obj P).X i j =
    HomologicalComplex.d ((𝟭 (Karoubi (HomologicalComplex C c))).obj P).X i j ≫
      (fun n => HomologicalComplex.Hom.f P.p n) j
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.35996, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P : Karoubi (HomologicalComplex C c)
i j : ι
x✝ : ComplexShape.Rel c i j
⊢ HomologicalComplex.Hom.f P.p i ≫ HomologicalComplex.Hom.f P.p i ≫ HomologicalComplex.d P.X i j =
    HomologicalComplex.d P.X i j ≫ HomologicalComplex.Hom.f P.p j
[PROOFSTEP]
simp only [HomologicalComplex.Hom.comm, HomologicalComplex.Hom.comm_assoc, HomologicalComplex.p_idem]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.35996, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P : Karoubi (HomologicalComplex C c)
⊢ (HomologicalComplex.Hom.mk fun n => HomologicalComplex.Hom.f P.p n) =
    ((𝟭 (Karoubi (HomologicalComplex C c))).obj P).p ≫
      (HomologicalComplex.Hom.mk fun n => HomologicalComplex.Hom.f P.p n) ≫ ((functor ⋙ inverse).obj P).p
[PROOFSTEP]
ext n
[GOAL]
case h
C : Type u_1
inst✝¹ : Category.{?u.35996, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P : Karoubi (HomologicalComplex C c)
n : ι
⊢ HomologicalComplex.Hom.f (HomologicalComplex.Hom.mk fun n => HomologicalComplex.Hom.f P.p n) n =
    HomologicalComplex.Hom.f
      (((𝟭 (Karoubi (HomologicalComplex C c))).obj P).p ≫
        (HomologicalComplex.Hom.mk fun n => HomologicalComplex.Hom.f P.p n) ≫ ((functor ⋙ inverse).obj P).p)
      n
[PROOFSTEP]
dsimp
[GOAL]
case h
C : Type u_1
inst✝¹ : Category.{?u.35996, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P : Karoubi (HomologicalComplex C c)
n : ι
⊢ HomologicalComplex.Hom.f P.p n =
    HomologicalComplex.Hom.f P.p n ≫ HomologicalComplex.Hom.f P.p n ≫ HomologicalComplex.Hom.f P.p n
[PROOFSTEP]
simp only [HomologicalComplex.p_idem]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.35996, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P Q : Karoubi (HomologicalComplex C c)
φ : P ⟶ Q
⊢ (𝟭 (Karoubi (HomologicalComplex C c))).map φ ≫
      (fun P => Hom.mk (HomologicalComplex.Hom.mk fun n => HomologicalComplex.Hom.f P.p n)) Q =
    (fun P => Hom.mk (HomologicalComplex.Hom.mk fun n => HomologicalComplex.Hom.f P.p n)) P ≫ (functor ⋙ inverse).map φ
[PROOFSTEP]
ext
[GOAL]
case h.h
C : Type u_1
inst✝¹ : Category.{?u.35996, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P Q : Karoubi (HomologicalComplex C c)
φ : P ⟶ Q
i✝ : ι
⊢ HomologicalComplex.Hom.f
      ((𝟭 (Karoubi (HomologicalComplex C c))).map φ ≫
          (fun P => Hom.mk (HomologicalComplex.Hom.mk fun n => HomologicalComplex.Hom.f P.p n)) Q).f
      i✝ =
    HomologicalComplex.Hom.f
      ((fun P => Hom.mk (HomologicalComplex.Hom.mk fun n => HomologicalComplex.Hom.f P.p n)) P ≫
          (functor ⋙ inverse).map φ).f
      i✝
[PROOFSTEP]
dsimp
[GOAL]
case h.h
C : Type u_1
inst✝¹ : Category.{?u.35996, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P Q : Karoubi (HomologicalComplex C c)
φ : P ⟶ Q
i✝ : ι
⊢ HomologicalComplex.Hom.f φ.f i✝ ≫ HomologicalComplex.Hom.f Q.p i✝ =
    HomologicalComplex.Hom.f P.p i✝ ≫ HomologicalComplex.Hom.f φ.f i✝
[PROOFSTEP]
simp only [comp_f, HomologicalComplex.comp_f, HomologicalComplex.comp_p_d, Inverse.map_f_f, Functor.map_f_f,
  HomologicalComplex.p_comp_d]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.35996, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P : Karoubi (HomologicalComplex C c)
i j : ι
x✝ : ComplexShape.Rel c i j
⊢ (fun n => HomologicalComplex.Hom.f P.p n) i ≫
      HomologicalComplex.d ((𝟭 (Karoubi (HomologicalComplex C c))).obj P).X i j =
    HomologicalComplex.d ((functor ⋙ inverse).obj P).X i j ≫ (fun n => HomologicalComplex.Hom.f P.p n) j
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.35996, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P : Karoubi (HomologicalComplex C c)
i j : ι
x✝ : ComplexShape.Rel c i j
⊢ HomologicalComplex.Hom.f P.p i ≫ HomologicalComplex.d P.X i j =
    (HomologicalComplex.Hom.f P.p i ≫ HomologicalComplex.d P.X i j) ≫ HomologicalComplex.Hom.f P.p j
[PROOFSTEP]
simp only [HomologicalComplex.Hom.comm, assoc, HomologicalComplex.p_idem]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.35996, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P : Karoubi (HomologicalComplex C c)
⊢ (HomologicalComplex.Hom.mk fun n => HomologicalComplex.Hom.f P.p n) =
    ((functor ⋙ inverse).obj P).p ≫
      (HomologicalComplex.Hom.mk fun n => HomologicalComplex.Hom.f P.p n) ≫
        ((𝟭 (Karoubi (HomologicalComplex C c))).obj P).p
[PROOFSTEP]
ext n
[GOAL]
case h
C : Type u_1
inst✝¹ : Category.{?u.35996, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P : Karoubi (HomologicalComplex C c)
n : ι
⊢ HomologicalComplex.Hom.f (HomologicalComplex.Hom.mk fun n => HomologicalComplex.Hom.f P.p n) n =
    HomologicalComplex.Hom.f
      (((functor ⋙ inverse).obj P).p ≫
        (HomologicalComplex.Hom.mk fun n => HomologicalComplex.Hom.f P.p n) ≫
          ((𝟭 (Karoubi (HomologicalComplex C c))).obj P).p)
      n
[PROOFSTEP]
dsimp
[GOAL]
case h
C : Type u_1
inst✝¹ : Category.{?u.35996, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P : Karoubi (HomologicalComplex C c)
n : ι
⊢ HomologicalComplex.Hom.f P.p n =
    HomologicalComplex.Hom.f P.p n ≫ HomologicalComplex.Hom.f P.p n ≫ HomologicalComplex.Hom.f P.p n
[PROOFSTEP]
simp only [HomologicalComplex.p_idem]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.35996, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P Q : Karoubi (HomologicalComplex C c)
φ : P ⟶ Q
⊢ (functor ⋙ inverse).map φ ≫ (fun P => Hom.mk (HomologicalComplex.Hom.mk fun n => HomologicalComplex.Hom.f P.p n)) Q =
    (fun P => Hom.mk (HomologicalComplex.Hom.mk fun n => HomologicalComplex.Hom.f P.p n)) P ≫
      (𝟭 (Karoubi (HomologicalComplex C c))).map φ
[PROOFSTEP]
ext
[GOAL]
case h.h
C : Type u_1
inst✝¹ : Category.{?u.35996, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P Q : Karoubi (HomologicalComplex C c)
φ : P ⟶ Q
i✝ : ι
⊢ HomologicalComplex.Hom.f
      ((functor ⋙ inverse).map φ ≫
          (fun P => Hom.mk (HomologicalComplex.Hom.mk fun n => HomologicalComplex.Hom.f P.p n)) Q).f
      i✝ =
    HomologicalComplex.Hom.f
      ((fun P => Hom.mk (HomologicalComplex.Hom.mk fun n => HomologicalComplex.Hom.f P.p n)) P ≫
          (𝟭 (Karoubi (HomologicalComplex C c))).map φ).f
      i✝
[PROOFSTEP]
dsimp
[GOAL]
case h.h
C : Type u_1
inst✝¹ : Category.{?u.35996, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P Q : Karoubi (HomologicalComplex C c)
φ : P ⟶ Q
i✝ : ι
⊢ HomologicalComplex.Hom.f φ.f i✝ ≫ HomologicalComplex.Hom.f Q.p i✝ =
    HomologicalComplex.Hom.f P.p i✝ ≫ HomologicalComplex.Hom.f φ.f i✝
[PROOFSTEP]
simp only [comp_f, HomologicalComplex.comp_f, Inverse.map_f_f, Functor.map_f_f, HomologicalComplex.comp_p_d,
  HomologicalComplex.p_comp_d]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.35996, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
⊢ ((NatTrans.mk fun P => Hom.mk (HomologicalComplex.Hom.mk fun n => HomologicalComplex.Hom.f P.p n)) ≫
      NatTrans.mk fun P => Hom.mk (HomologicalComplex.Hom.mk fun n => HomologicalComplex.Hom.f P.p n)) =
    𝟙 (𝟭 (Karoubi (HomologicalComplex C c)))
[PROOFSTEP]
ext
[GOAL]
case w.h.h.h
C : Type u_1
inst✝¹ : Category.{?u.35996, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
x✝ : Karoubi (HomologicalComplex C c)
i✝ : ι
⊢ HomologicalComplex.Hom.f
      (NatTrans.app
          ((NatTrans.mk fun P => Hom.mk (HomologicalComplex.Hom.mk fun n => HomologicalComplex.Hom.f P.p n)) ≫
            NatTrans.mk fun P => Hom.mk (HomologicalComplex.Hom.mk fun n => HomologicalComplex.Hom.f P.p n))
          x✝).f
      i✝ =
    HomologicalComplex.Hom.f (NatTrans.app (𝟙 (𝟭 (Karoubi (HomologicalComplex C c)))) x✝).f i✝
[PROOFSTEP]
dsimp
[GOAL]
case w.h.h.h
C : Type u_1
inst✝¹ : Category.{?u.35996, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
x✝ : Karoubi (HomologicalComplex C c)
i✝ : ι
⊢ HomologicalComplex.Hom.f x✝.p i✝ ≫ HomologicalComplex.Hom.f x✝.p i✝ = HomologicalComplex.Hom.f x✝.p i✝
[PROOFSTEP]
simp only [HomologicalComplex.p_idem, comp_f, HomologicalComplex.comp_f, _root_.id_eq]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.35996, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
⊢ ((NatTrans.mk fun P => Hom.mk (HomologicalComplex.Hom.mk fun n => HomologicalComplex.Hom.f P.p n)) ≫
      NatTrans.mk fun P => Hom.mk (HomologicalComplex.Hom.mk fun n => HomologicalComplex.Hom.f P.p n)) =
    𝟙 (functor ⋙ inverse)
[PROOFSTEP]
ext
[GOAL]
case w.h.h.h
C : Type u_1
inst✝¹ : Category.{?u.35996, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
x✝ : Karoubi (HomologicalComplex C c)
i✝ : ι
⊢ HomologicalComplex.Hom.f
      (NatTrans.app
          ((NatTrans.mk fun P => Hom.mk (HomologicalComplex.Hom.mk fun n => HomologicalComplex.Hom.f P.p n)) ≫
            NatTrans.mk fun P => Hom.mk (HomologicalComplex.Hom.mk fun n => HomologicalComplex.Hom.f P.p n))
          x✝).f
      i✝ =
    HomologicalComplex.Hom.f (NatTrans.app (𝟙 (functor ⋙ inverse)) x✝).f i✝
[PROOFSTEP]
dsimp
[GOAL]
case w.h.h.h
C : Type u_1
inst✝¹ : Category.{?u.35996, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
x✝ : Karoubi (HomologicalComplex C c)
i✝ : ι
⊢ HomologicalComplex.Hom.f x✝.p i✝ ≫ HomologicalComplex.Hom.f x✝.p i✝ = HomologicalComplex.Hom.f x✝.p i✝
[PROOFSTEP]
simp only [HomologicalComplex.p_idem, comp_f, HomologicalComplex.comp_f, _root_.id_eq, Inverse.obj_p_f, Functor.obj_X_p]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.61291, u_1} C
inst✝³ : Preadditive C
ι : Type u_2
c : ComplexShape ι
α : Type u_3
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : IsIdempotentComplete C
⊢ IsIdempotentComplete (HomologicalComplex C c)
[PROOFSTEP]
rw [isIdempotentComplete_iff_of_equivalence ((toKaroubiEquivalence C).mapHomologicalComplex c), ←
  isIdempotentComplete_iff_of_equivalence (karoubiHomologicalComplexEquivalence C c)]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.61291, u_1} C
inst✝³ : Preadditive C
ι : Type u_2
c : ComplexShape ι
α : Type u_3
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : IsIdempotentComplete C
⊢ IsIdempotentComplete (Karoubi (HomologicalComplex C c))
[PROOFSTEP]
infer_instance


[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
𝒢 : Set C
h𝒢 : IsSeparating 𝒢
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), G ∈ 𝒢 → ∀ (h : G ⟶ X), h ≫ f = 0
⊢ ∀ (G : C), G ∈ 𝒢 → ∀ (h : G ⟶ X), h ≫ f = h ≫ 0
[PROOFSTEP]
simpa only [Limits.comp_zero] using hf
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
𝒢 : Set C
h𝒢 : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (G : C), G ∈ 𝒢 → ∀ (h : G ⟶ X), h ≫ f = 0) → f = 0
X Y : C
f g : X ⟶ Y
hfg : ∀ (G : C), G ∈ 𝒢 → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
⊢ ∀ (G : C), G ∈ 𝒢 → ∀ (h : G ⟶ X), h ≫ (f - g) = 0
[PROOFSTEP]
simpa only [Preadditive.comp_sub, sub_eq_zero] using hfg
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
𝒢 : Set C
h𝒢 : IsCoseparating 𝒢
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), G ∈ 𝒢 → ∀ (h : Y ⟶ G), f ≫ h = 0
⊢ ∀ (G : C), G ∈ 𝒢 → ∀ (h : Y ⟶ G), f ≫ h = 0 ≫ h
[PROOFSTEP]
simpa only [Limits.zero_comp] using hf
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
𝒢 : Set C
h𝒢 : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (G : C), G ∈ 𝒢 → ∀ (h : Y ⟶ G), f ≫ h = 0) → f = 0
X Y : C
f g : X ⟶ Y
hfg : ∀ (G : C), G ∈ 𝒢 → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
⊢ ∀ (G : C), G ∈ 𝒢 → ∀ (h : Y ⟶ G), (f - g) ≫ h = 0
[PROOFSTEP]
simpa only [Preadditive.sub_comp, sub_eq_zero] using hfg
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
G : C
hG : IsSeparator G
X Y : C
f : X ⟶ Y
hf : ∀ (h : G ⟶ X), h ≫ f = 0
⊢ ∀ (h : G ⟶ X), h ≫ f = h ≫ 0
[PROOFSTEP]
simpa only [Limits.comp_zero] using hf
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
G : C
hG : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (h : G ⟶ X), h ≫ f = 0) → f = 0
X Y : C
f g : X ⟶ Y
hfg : ∀ (h : G ⟶ X), h ≫ f = h ≫ g
⊢ ∀ (h : G ⟶ X), h ≫ (f - g) = 0
[PROOFSTEP]
simpa only [Preadditive.comp_sub, sub_eq_zero] using hfg
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
G : C
hG : IsCoseparator G
X Y : C
f : X ⟶ Y
hf : ∀ (h : Y ⟶ G), f ≫ h = 0
⊢ ∀ (h : Y ⟶ G), f ≫ h = 0 ≫ h
[PROOFSTEP]
simpa only [Limits.zero_comp] using hf
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
G : C
hG : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (h : Y ⟶ G), f ≫ h = 0) → f = 0
X Y : C
f g : X ⟶ Y
hfg : ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
⊢ ∀ (h : Y ⟶ G), (f - g) ≫ h = 0
[PROOFSTEP]
simpa only [Preadditive.sub_comp, sub_eq_zero] using hfg
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
G : C
⊢ IsSeparator G ↔ Faithful (preadditiveCoyoneda.obj (op G))
[PROOFSTEP]
rw [isSeparator_iff_faithful_coyoneda_obj, ← whiskering_preadditiveCoyoneda, Functor.comp_obj, whiskeringRight_obj_obj]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
G : C
⊢ Faithful (preadditiveCoyoneda.obj (op G) ⋙ forget AddCommGroupCat) ↔ Faithful (preadditiveCoyoneda.obj (op G))
[PROOFSTEP]
exact ⟨fun h => Faithful.of_comp _ (forget AddCommGroupCat), fun h => Faithful.comp _ _⟩
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
G : C
⊢ IsSeparator G ↔ Faithful (preadditiveCoyonedaObj (op G))
[PROOFSTEP]
rw [isSeparator_iff_faithful_preadditiveCoyoneda, preadditiveCoyoneda_obj]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
G : C
⊢ Faithful (preadditiveCoyonedaObj (op G) ⋙ forget₂ (ModuleCat (End (op G))) AddCommGroupCat) ↔
    Faithful (preadditiveCoyonedaObj (op G))
[PROOFSTEP]
exact ⟨fun h => Faithful.of_comp _ (forget₂ _ AddCommGroupCat.{v}), fun h => Faithful.comp _ _⟩
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
G : C
⊢ IsCoseparator G ↔ Faithful (preadditiveYoneda.obj G)
[PROOFSTEP]
rw [isCoseparator_iff_faithful_yoneda_obj, ← whiskering_preadditiveYoneda, Functor.comp_obj, whiskeringRight_obj_obj]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
G : C
⊢ Faithful (preadditiveYoneda.obj G ⋙ forget AddCommGroupCat) ↔ Faithful (preadditiveYoneda.obj G)
[PROOFSTEP]
exact ⟨fun h => Faithful.of_comp _ (forget AddCommGroupCat), fun h => Faithful.comp _ _⟩
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
G : C
⊢ IsCoseparator G ↔ Faithful (preadditiveYonedaObj G)
[PROOFSTEP]
rw [isCoseparator_iff_faithful_preadditiveYoneda, preadditiveYoneda_obj]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
G : C
⊢ Faithful (preadditiveYonedaObj G ⋙ forget₂ (ModuleCat (End G)) AddCommGroupCat) ↔ Faithful (preadditiveYonedaObj G)
[PROOFSTEP]
exact ⟨fun h => Faithful.of_comp _ (forget₂ _ AddCommGroupCat.{v}), fun h => Faithful.comp _ _⟩