-- Mathlib/LinearAlgebra/Eigenspace/Matrix.lean
/-- Eigenvalues of a diagonal linear operator are the diagonal entries. -/
lemma hasEigenvalue_toLin_diagonal_iff (d : n → R) {μ : R} [NoZeroSMulDivisors R M]
    (b : Basis n R M) : HasEigenvalue (toLin b b (diagonal d)) μ ↔ ∃ i, d i = μ

Proof state:
R : Type u_1
n : Type u_2
M : Type u_3
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : Nontrivial R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
d : n → R
μ : R
inst✝ : NoZeroSMulDivisors R M
b : Basis n R M
this : ∀ (i : n), HasEigenvalue ((toLin b b) (diagonal d)) (d i)
hμ : ∀ (i : n), d i ≠ μ
h_eig : HasEigenvalue ((toLin b b) (diagonal d)) μ
⊢ ⨆ μ ∈ Set.range d, eigenspace ((toLin b b) (diagonal d)) μ = ⊤

Tactic:
rw [eq_top_iff, ← b.span_eq, Submodule.span_le]

Result:
R : Type u_1
n : Type u_2
M : Type u_3
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : Nontrivial R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
d : n → R
μ : R
inst✝ : NoZeroSMulDivisors R M
b : Basis n R M
this : ∀ (i : n), HasEigenvalue ((toLin b b) (diagonal d)) (d i)
hμ : ∀ (i : n), d i ≠ μ
h_eig : HasEigenvalue ((toLin b b) (diagonal d)) μ
⊢ Set.range ⇑b ⊆ ↑(⨆ μ ∈ Set.range d, eigenspace ((toLin b b) (diagonal d)) μ)

Proof state:
case intro
R : Type u_1
n : Type u_2
M : Type u_3
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : Nontrivial R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
d : n → R
μ : R
inst✝ : NoZeroSMulDivisors R M
b : Basis n R M
this : ∀ (i : n), HasEigenvalue ((toLin b b) (diagonal d)) (d i)
hμ : ∀ (i : n), d i ≠ μ
h_eig : HasEigenvalue ((toLin b b) (diagonal d)) μ
i : n
⊢ b i ∈ eigenspace ((toLin b b) (diagonal d)) (d i)

Tactic:
rw [mem_eigenspace_iff]

Result:
case intro
R : Type u_1
n : Type u_2
M : Type u_3
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : Nontrivial R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
d : n → R
μ : R
inst✝ : NoZeroSMulDivisors R M
b : Basis n R M
this : ∀ (i : n), HasEigenvalue ((toLin b b) (diagonal d)) (d i)
hμ : ∀ (i : n), d i ≠ μ
h_eig : HasEigenvalue ((toLin b b) (diagonal d)) μ
i : n
⊢ ((toLin b b) (diagonal d)) (b i) = d i • b i

Proof state:
case mp
R : Type u_1
n : Type u_2
M : Type u_3
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : Nontrivial R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
d : n → R
μ : R
inst✝ : NoZeroSMulDivisors R M
b : Basis n R M
this : ∀ (i : n), HasEigenvalue ((toLin b b) (diagonal d)) (d i)
⊢ HasEigenvalue ((toLin b b) (diagonal d)) μ → ∃ i, d i = μ

Tactic:
contrapose!

Result:
case mp
R : Type u_1
n : Type u_2
M : Type u_3
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : Nontrivial R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
d : n → R
μ : R
inst✝ : NoZeroSMulDivisors R M
b : Basis n R M
this : ∀ (i : n), HasEigenvalue ((toLin b b) (diagonal d)) (d i)
⊢ (∀ (i : n), d i ≠ μ) → ¬HasEigenvalue ((toLin b b) (diagonal d)) μ

Proof state:
case mp
R : Type u_1
n : Type u_2
M : Type u_3
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : Nontrivial R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
d : n → R
μ : R
inst✝ : NoZeroSMulDivisors R M
b : Basis n R M
this✝ : ∀ (i : n), HasEigenvalue ((toLin b b) (diagonal d)) (d i)
hμ : ∀ (i : n), d i ≠ μ
h_eig : HasEigenvalue ((toLin b b) (diagonal d)) μ
h_iSup : ⨆ μ ∈ Set.range d, eigenspace ((toLin b b) (diagonal d)) μ = ⊤
hμ_not_mem : μ ∉ Set.range d
this : eigenspace ((toLin b b) (diagonal d)) μ = ⊥
⊢ False

Tactic:
exact h_eig this

Result:
no goals

Proof state:
R : Type u_1
n : Type u_2
M : Type u_3
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : Nontrivial R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
d : n → R
μ : R
inst✝ : NoZeroSMulDivisors R M
b : Basis n R M
this : ∀ (i : n), HasEigenvalue ((toLin b b) (diagonal d)) (d i)
hμ : ∀ (i : n), d i ≠ μ
h_eig : HasEigenvalue ((toLin b b) (diagonal d)) μ
h_iSup : ⨆ μ ∈ Set.range d, eigenspace ((toLin b b) (diagonal d)) μ = ⊤
⊢ μ ∉ Set.range d

Tactic:
simpa using fun i ↦ (hμ i)

Result:
no goals

Proof state:
R : Type u_1
n : Type u_2
M : Type u_3
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : Nontrivial R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
d : n → R
μ : R
inst✝ : NoZeroSMulDivisors R M
b : Basis n R M
this : ∀ (i : n), HasEigenvalue ((toLin b b) (diagonal d)) (d i)
⊢ HasEigenvalue ((toLin b b) (diagonal d)) μ ↔ ∃ i, d i = μ

Tactic:
constructor

Result:
case mp
R : Type u_1
n : Type u_2
M : Type u_3
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : Nontrivial R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
d : n → R
μ : R
inst✝ : NoZeroSMulDivisors R M
b : Basis n R M
this : ∀ (i : n), HasEigenvalue ((toLin b b) (diagonal d)) (d i)
⊢ HasEigenvalue ((toLin b b) (diagonal d)) μ → ∃ i, d i = μ

case mpr
R : Type u_1
n : Type u_2
M : Type u_3
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : Nontrivial R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
d : n → R
μ : R
inst✝ : NoZeroSMulDivisors R M
b : Basis n R M
this : ∀ (i : n), HasEigenvalue ((toLin b b) (diagonal d)) (d i)
⊢ (∃ i, d i = μ) → HasEigenvalue ((toLin b b) (diagonal d)) μ

Proof state:
case mpr
R : Type u_1
n : Type u_2
M : Type u_3
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : Nontrivial R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
d : n → R
μ : R
inst✝ : NoZeroSMulDivisors R M
b : Basis n R M
this : ∀ (i : n), HasEigenvalue ((toLin b b) (diagonal d)) (d i)
⊢ (∃ i, d i = μ) → HasEigenvalue ((toLin b b) (diagonal d)) μ

Tactic:
rintro ⟨i, rfl⟩

Result:
case mpr.intro
R : Type u_1
n : Type u_2
M : Type u_3
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : Nontrivial R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
d : n → R
inst✝ : NoZeroSMulDivisors R M
b : Basis n R M
this : ∀ (i : n), HasEigenvalue ((toLin b b) (diagonal d)) (d i)
i : n
⊢ HasEigenvalue ((toLin b b) (diagonal d)) (d i)

Proof state:
case intro
R : Type u_1
n : Type u_2
M : Type u_3
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : Nontrivial R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
d : n → R
μ : R
inst✝ : NoZeroSMulDivisors R M
b : Basis n R M
this : ∀ (i : n), HasEigenvalue ((toLin b b) (diagonal d)) (d i)
hμ : ∀ (i : n), d i ≠ μ
h_eig : HasEigenvalue ((toLin b b) (diagonal d)) μ
i : n
⊢ b i ∈ ⨆ μ ∈ Set.range d, eigenspace ((toLin b b) (diagonal d)) μ

Tactic:
apply Submodule.mem_iSup_of_mem (d i)

Result:
case intro
R : Type u_1
n : Type u_2
M : Type u_3
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : Nontrivial R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
d : n → R
μ : R
inst✝ : NoZeroSMulDivisors R M
b : Basis n R M
this : ∀ (i : n), HasEigenvalue ((toLin b b) (diagonal d)) (d i)
hμ : ∀ (i : n), d i ≠ μ
h_eig : HasEigenvalue ((toLin b b) (diagonal d)) μ
i : n
⊢ b i ∈ ⨆ (_ : d i ∈ Set.range d), eigenspace ((toLin b b) (diagonal d)) (d i)