-- Mathlib/LinearAlgebra/Matrix/Gershgorin.lean
theorem eigenvalue_mem_ball {μ : K} (hμ : Module.End.HasEigenvalue (Matrix.toLin' A) μ) :
    ∃ k, μ ∈ Metric.closedBall (A k k) (∑ j ∈ Finset.univ.erase k, ‖A k j‖)

Proof state:
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ (Module.End.genEigenspace (Matrix.toLin' A) μ) 1
h_nz✝ : v ≠ 0
i : n
h_i : (Finset.univ.sup' ⋯ fun i => ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
j : n
⊢ ‖v j * (v i)⁻¹‖ ≤ 1

Tactic:
rw [norm_mul, norm_inv, mul_inv_le_iff₀ (norm_pos_iff.mpr h_nz), one_mul]

Result:
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ (Module.End.genEigenspace (Matrix.toLin' A) μ) 1
h_nz✝ : v ≠ 0
i : n
h_i : (Finset.univ.sup' ⋯ fun i => ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
j : n
⊢ ‖v j‖ ≤ ‖v i‖

Proof state:
case inl
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (Matrix.toLin' A) μ
h✝ : IsEmpty n
⊢ False

Tactic:
exact hμ Submodule.eq_bot_of_subsingleton

Result:
no goals

Proof state:
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ (Module.End.genEigenspace (Matrix.toLin' A) μ) 1
h_nz✝ : v ≠ 0
i : n
h_i : (Finset.univ.sup' ⋯ fun i => ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
h_le : ∀ (j : n), ‖v j * (v i)⁻¹‖ ≤ 1
⊢ μ * v i = ∑ x : n, A i x * v x

Tactic:
rw [← dotProduct, ← Matrix.mulVec]

Result:
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ (Module.End.genEigenspace (Matrix.toLin' A) μ) 1
h_nz✝ : v ≠ 0
i : n
h_i : (Finset.univ.sup' ⋯ fun i => ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
h_le : ∀ (j : n), ‖v j * (v i)⁻¹‖ ≤ 1
⊢ μ * v i = A.mulVec v i

Proof state:
case h
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ (Module.End.genEigenspace (Matrix.toLin' A) μ) 1
i : n
h_i : (Finset.univ.sup' ⋯ fun i => ‖v i‖) = ‖v i‖
h_nz : v i = 0
j : n
⊢ ‖v i‖ ≤ 0

Tactic:
exact norm_le_zero_iff.mpr h_nz

Result:
no goals

Proof state:
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ (Module.End.genEigenspace (Matrix.toLin' A) μ) 1
h_nz : v ≠ 0
i : n
h_i : (Finset.univ.sup' ⋯ fun i => ‖v i‖) = ‖v i‖
⊢ v i ≠ 0

Tactic:
contrapose! h_nz

Result:
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ (Module.End.genEigenspace (Matrix.toLin' A) μ) 1
i : n
h_i : (Finset.univ.sup' ⋯ fun i => ‖v i‖) = ‖v i‖
h_nz : v i = 0
⊢ v = 0

Proof state:
case h
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ (Module.End.genEigenspace (Matrix.toLin' A) μ) 1
i : n
h_i : (Finset.univ.sup' ⋯ fun i => ‖v i‖) = ‖v i‖
h_nz : v i = 0
j : n
⊢ v j = 0 j

Tactic:
rw [Pi.zero_apply, ← norm_le_zero_iff]

Result:
case h
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ (Module.End.genEigenspace (Matrix.toLin' A) μ) 1
i : n
h_i : (Finset.univ.sup' ⋯ fun i => ‖v i‖) = ‖v i‖
h_nz : v i = 0
j : n
⊢ ‖v j‖ ≤ 0

Proof state:
case inl
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (Matrix.toLin' A) μ
h✝ : IsEmpty n
⊢ ∃ k, μ ∈ Metric.closedBall (A k k) (∑ j ∈ Finset.univ.erase k, ‖A k j‖)

Tactic:
exfalso

Result:
case inl
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (Matrix.toLin' A) μ
h✝ : IsEmpty n
⊢ False

Proof state:
case inr.intro.intro.intro.intro
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ (Module.End.genEigenspace (Matrix.toLin' A) μ) 1
h_nz✝ : v ≠ 0
i : n
h_i : (Finset.univ.sup' ⋯ fun i => ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
h_le : ∀ (j : n), ‖v j * (v i)⁻¹‖ ≤ 1
⊢ ∃ k, μ ∈ Metric.closedBall (A k k) (∑ j ∈ Finset.univ.erase k, ‖A k j‖)

Tactic:
simp_rw [mem_closedBall_iff_norm']

Result:
case inr.intro.intro.intro.intro
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ (Module.End.genEigenspace (Matrix.toLin' A) μ) 1
h_nz✝ : v ≠ 0
i : n
h_i : (Finset.univ.sup' ⋯ fun i => ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
h_le : ∀ (j : n), ‖v j * (v i)⁻¹‖ ≤ 1
⊢ ∃ k, ‖A k k - μ‖ ≤ ∑ j ∈ Finset.univ.erase k, ‖A k j‖