-- Mathlib/Analysis/InnerProductSpace/Spectrum.lean
theorem orthogonalFamily_eigenspaces (hT : T.IsSymmetric) :
    OrthogonalFamily 𝕜 (fun μ => eigenspace T μ) fun μ => (eigenspace T μ).subtypeₗᵢ

Proof state:
case neg
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
μ ν : 𝕜
hμν : μ ≠ ν
v : E
hv✝ : v ∈ eigenspace T μ
hv : T v = μ • v
w : E
hw✝ : w ∈ eigenspace T ν
hw : T w = ν • w
hv' : ¬v = 0
H : (starRingEnd 𝕜) μ = μ
⊢ inner (((fun μ => (eigenspace T μ).subtypeₗᵢ) μ) ⟨v, hv✝⟩) (((fun μ => (eigenspace T μ).subtypeₗᵢ) ν) ⟨w, hw✝⟩) = 0

Tactic:
refine Or.resolve_left ?_ hμν.symm

Result:
case neg
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
μ ν : 𝕜
hμν : μ ≠ ν
v : E
hv✝ : v ∈ eigenspace T μ
hv : T v = μ • v
w : E
hw✝ : w ∈ eigenspace T ν
hw : T w = ν • w
hv' : ¬v = 0
H : (starRingEnd 𝕜) μ = μ
⊢ ν = μ ∨
    inner (((fun μ => (eigenspace T μ).subtypeₗᵢ) μ) ⟨v, hv✝⟩) (((fun μ => (eigenspace T μ).subtypeₗᵢ) ν) ⟨w, hw✝⟩) = 0

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
⊢ OrthogonalFamily 𝕜 (fun μ => ↥(eigenspace T μ)) fun μ => (eigenspace T μ).subtypeₗᵢ

Tactic:
rintro μ ν hμν ⟨v, hv⟩ ⟨w, hw⟩

Result:
case mk.mk
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
μ ν : 𝕜
hμν : μ ≠ ν
v : E
hv : v ∈ eigenspace T μ
w : E
hw : w ∈ eigenspace T ν
⊢ inner (((fun μ => (eigenspace T μ).subtypeₗᵢ) μ) ⟨v, hv⟩) (((fun μ => (eigenspace T μ).subtypeₗᵢ) ν) ⟨w, hw⟩) = 0

Proof state:
case pos
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
μ ν : 𝕜
hμν : μ ≠ ν
v : E
hv : v ∈ eigenspace T μ
w : E
hw : w ∈ eigenspace T ν
hv' : v = 0
⊢ inner (((fun μ => (eigenspace T μ).subtypeₗᵢ) μ) ⟨v, hv⟩) (((fun μ => (eigenspace T μ).subtypeₗᵢ) ν) ⟨w, hw⟩) = 0

Tactic:
simp [hv']

Result:
no goals

Proof state:
case mk.mk
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
μ ν : 𝕜
hμν : μ ≠ ν
v : E
hv : v ∈ eigenspace T μ
w : E
hw : w ∈ eigenspace T ν
⊢ inner (((fun μ => (eigenspace T μ).subtypeₗᵢ) μ) ⟨v, hv⟩) (((fun μ => (eigenspace T μ).subtypeₗᵢ) ν) ⟨w, hw⟩) = 0

Tactic:
by_cases hv' : v = 0

Result:
case pos
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
μ ν : 𝕜
hμν : μ ≠ ν
v : E
hv : v ∈ eigenspace T μ
w : E
hw : w ∈ eigenspace T ν
hv' : v = 0
⊢ inner (((fun μ => (eigenspace T μ).subtypeₗᵢ) μ) ⟨v, hv⟩) (((fun μ => (eigenspace T μ).subtypeₗᵢ) ν) ⟨w, hw⟩) = 0

case neg
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
μ ν : 𝕜
hμν : μ ≠ ν
v : E
hv : v ∈ eigenspace T μ
w : E
hw : w ∈ eigenspace T ν
hv' : ¬v = 0
⊢ inner (((fun μ => (eigenspace T μ).subtypeₗᵢ) μ) ⟨v, hv⟩) (((fun μ => (eigenspace T μ).subtypeₗᵢ) ν) ⟨w, hw⟩) = 0

Proof state:
case neg
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
μ ν : 𝕜
hμν : μ ≠ ν
v : E
hv✝ : v ∈ eigenspace T μ
hv : T v = μ • v
w : E
hw✝ : w ∈ eigenspace T ν
hw : T w = ν • w
hv' : ¬v = 0
H : (starRingEnd 𝕜) μ = μ
⊢ ν = μ ∨
    inner (((fun μ => (eigenspace T μ).subtypeₗᵢ) μ) ⟨v, hv✝⟩) (((fun μ => (eigenspace T μ).subtypeₗᵢ) ν) ⟨w, hw✝⟩) = 0

Tactic:
simpa [inner_smul_left, inner_smul_right, hv, hw, H] using (hT v w).symm

Result:
no goals

Proof state:
case neg
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
μ ν : 𝕜
hμν : μ ≠ ν
v : E
hv : v ∈ eigenspace T μ
w : E
hw : w ∈ eigenspace T ν
hv' : ¬v = 0
H : (starRingEnd 𝕜) μ = μ
⊢ inner (((fun μ => (eigenspace T μ).subtypeₗᵢ) μ) ⟨v, hv⟩) (((fun μ => (eigenspace T μ).subtypeₗᵢ) ν) ⟨w, hw⟩) = 0

Tactic:
rw [mem_eigenspace_iff] at hv hw

Result:
case neg
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
μ ν : 𝕜
hμν : μ ≠ ν
v : E
hv✝ : v ∈ eigenspace T μ
hv : T v = μ • v
w : E
hw✝ : w ∈ eigenspace T ν
hw : T w = ν • w
hv' : ¬v = 0
H : (starRingEnd 𝕜) μ = μ
⊢ inner (((fun μ => (eigenspace T μ).subtypeₗᵢ) μ) ⟨v, hv✝⟩) (((fun μ => (eigenspace T μ).subtypeₗᵢ) ν) ⟨w, hw✝⟩) = 0

Proof state:
case neg
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
μ ν : 𝕜
hμν : μ ≠ ν
v : E
hv : v ∈ eigenspace T μ
w : E
hw : w ∈ eigenspace T ν
hv' : ¬v = 0
⊢ inner (((fun μ => (eigenspace T μ).subtypeₗᵢ) μ) ⟨v, hv⟩) (((fun μ => (eigenspace T μ).subtypeₗᵢ) ν) ⟨w, hw⟩) = 0

Tactic:
have H := hT.conj_eigenvalue_eq_self (hasEigenvalue_of_hasEigenvector ⟨hv, hv'⟩)

Result:
case neg
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
μ ν : 𝕜
hμν : μ ≠ ν
v : E
hv : v ∈ eigenspace T μ
w : E
hw : w ∈ eigenspace T ν
hv' : ¬v = 0
H : (starRingEnd 𝕜) μ = μ
⊢ inner (((fun μ => (eigenspace T μ).subtypeₗᵢ) μ) ⟨v, hv⟩) (((fun μ => (eigenspace T μ).subtypeₗᵢ) ν) ⟨w, hw⟩) = 0