-- Mathlib/CategoryTheory/Preadditive/HomOrthogonal.lean
theorem matrixDecomposition_id (o : HomOrthogonal s) {α : Type} [Finite α] {f : α → ι} (i : ι) :
    o.matrixDecomposition (𝟙 (⨁ fun a => s (f a))) i = 1

Proof state:
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✝ : Finite α
f : α → ι
b : α
j_property✝ : b ∈ f ⁻¹' {f b}
j_property : f b = f b
⊢ eqToHom ⋯ ≫ biproduct.ι (fun a => s (f a)) b ≫ biproduct.π (fun b => s (f b)) b = 𝟙 (s (f b))

Tactic:
simp

Result:
no goals

Proof state:
case a.mk.refl.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✝ : Finite α
f : α → ι
b a : α
j_property : a ∈ f ⁻¹' {f b}
⊢ o.matrixDecomposition (𝟙 (⨁ fun a => s (f a))) (f b) ⟨b, ⋯⟩ ⟨a, j_property⟩ = 1 ⟨b, ⋯⟩ ⟨a, j_property⟩

Tactic:
simp only [Set.mem_preimage, Set.mem_singleton_iff] at j_property

Result:
case a.mk.refl.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✝ : Finite α
f : α → ι
b a : α
j_property✝ : a ∈ f ⁻¹' {f b}
j_property : f a = f b
⊢ o.matrixDecomposition (𝟙 (⨁ fun a => s (f a))) (f b) ⟨b, ⋯⟩ ⟨a, j_property✝⟩ = 1 ⟨b, ⋯⟩ ⟨a, j_property✝⟩

Proof state:
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✝ : Finite α
f : α → ι
b a : α
j_property✝ : a ∈ f ⁻¹' {f b}
j_property : f a = f b
h : ¬b = a
⊢ eqToHom ⋯ ≫ biproduct.ι (fun a => s (f a)) a ≫ biproduct.π (fun b => s (f b)) b = 0

Tactic:
have : biproduct.ι (fun a ↦ s (f a)) a ≫ biproduct.π (fun b ↦ s (f b)) b = 0 := by
  simpa using biproduct.ι_π_ne _ (Ne.symm h)

Result:
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✝ : Finite α
f : α → ι
b a : α
j_property✝ : a ∈ f ⁻¹' {f 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 ⋯ ≫ biproduct.ι (fun a => s (f a)) a ≫ biproduct.π (fun b => s (f b)) b = 0

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
o : HomOrthogonal s
α : Type
inst✝ : Finite α
f : α → ι
i : ι
⊢ o.matrixDecomposition (𝟙 (⨁ fun a => s (f a))) i = 1

Tactic:
ext ⟨b, ⟨⟩⟩ ⟨a, j_property⟩

Result:
case a.mk.refl.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✝ : Finite α
f : α → ι
b a : α
j_property : a ∈ f ⁻¹' {f b}
⊢ o.matrixDecomposition (𝟙 (⨁ fun a => s (f a))) (f b) ⟨b, ⋯⟩ ⟨a, j_property⟩ = 1 ⟨b, ⋯⟩ ⟨a, j_property⟩

Proof state:
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✝ : Finite α
f : α → ι
b a : α
j_property✝ : a ∈ f ⁻¹' {f 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 ⋯ ≫ biproduct.ι (fun a => s (f a)) a ≫ biproduct.π (fun b => s (f b)) b = 0

Tactic:
rw [this, comp_zero]

Result:
no goals

Proof state:
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✝ : Finite α
f : α → ι
b a : α
j_property✝ : a ∈ f ⁻¹' {f b}
j_property : f a = f b
h : ⟨b, ⋯⟩ = ⟨a, j_property✝⟩
⊢ eqToHom ⋯ ≫ biproduct.ι (fun a => s (f a)) a ≫ biproduct.π (fun b => s (f b)) b = 𝟙 (s (f b))

Tactic:
cases h

Result:
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✝ : Finite α
f : α → ι
b : α
j_property✝ : b ∈ f ⁻¹' {f b}
j_property : f b = f b
⊢ eqToHom ⋯ ≫ biproduct.ι (fun a => s (f a)) b ≫ biproduct.π (fun b => s (f b)) b = 𝟙 (s (f b))

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
o : HomOrthogonal s
α : Type
inst✝ : Finite α
f : α → ι
b a : α
j_property✝ : a ∈ f ⁻¹' {f 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

Tactic:
simpa using biproduct.ι_π_ne _ (Ne.symm h)

Result:
no goals

Proof state:
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✝ : Finite α
f : α → ι
b a : α
j_property✝ : a ∈ f ⁻¹' {f b}
j_property : f a = f b
h : ¬⟨b, ⋯⟩ = ⟨a, j_property✝⟩
⊢ eqToHom ⋯ ≫ biproduct.ι (fun a => s (f a)) a ≫ biproduct.π (fun b => s (f b)) b = 0

Tactic:
simp only [Subtype.mk.injEq] at h

Result:
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✝ : Finite α
f : α → ι
b a : α
j_property✝ : a ∈ f ⁻¹' {f b}
j_property : f a = f b
h : ¬b = a
⊢ eqToHom ⋯ ≫ biproduct.ι (fun a => s (f a)) a ≫ biproduct.π (fun b => s (f b)) b = 0

Proof state:
case a.mk.refl.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✝ : Finite α
f : α → ι
b a : α
j_property✝ : a ∈ f ⁻¹' {f b}
j_property : f a = f b
⊢ o.matrixDecomposition (𝟙 (⨁ fun a => s (f a))) (f b) ⟨b, ⋯⟩ ⟨a, j_property✝⟩ = 1 ⟨b, ⋯⟩ ⟨a, j_property✝⟩

Tactic:
simp only [Category.comp_id, Category.id_comp, Category.assoc, End.one_def, eqToHom_refl,
  Matrix.one_apply, HomOrthogonal.matrixDecomposition_apply, biproduct.components]

Result:
case a.mk.refl.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✝ : Finite α
f : α → ι
b a : α
j_property✝ : a ∈ f ⁻¹' {f b}
j_property : f a = f b
⊢ eqToHom ⋯ ≫ biproduct.ι (fun a => s (f a)) a ≫ biproduct.π (fun b => s (f b)) b =
    if ⟨b, ⋯⟩ = ⟨a, j_property✝⟩ then 𝟙 (s (f b)) else 0

Proof state:
case a.mk.refl.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✝ : Finite α
f : α → ι
b a : α
j_property✝ : a ∈ f ⁻¹' {f b}
j_property : f a = f b
⊢ eqToHom ⋯ ≫ biproduct.ι (fun a => s (f a)) a ≫ biproduct.π (fun b => s (f b)) b =
    if ⟨b, ⋯⟩ = ⟨a, j_property✝⟩ then 𝟙 (s (f b)) else 0

Tactic:
split_ifs with h

Result:
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✝ : Finite α
f : α → ι
b a : α
j_property✝ : a ∈ f ⁻¹' {f b}
j_property : f a = f b
h : ⟨b, ⋯⟩ = ⟨a, j_property✝⟩
⊢ eqToHom ⋯ ≫ biproduct.ι (fun a => s (f a)) a ≫ biproduct.π (fun b => s (f b)) b = 𝟙 (s (f b))

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✝ : Finite α
f : α → ι
b a : α
j_property✝ : a ∈ f ⁻¹' {f b}
j_property : f a = f b
h : ¬⟨b, ⋯⟩ = ⟨a, j_property✝⟩
⊢ eqToHom ⋯ ≫ biproduct.ι (fun a => s (f a)) a ≫ biproduct.π (fun b => s (f b)) b = 0