awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Gershgorin (goal)
Goal:
K : Type u_1
n : Type u_2
inst : NormedField K
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (M := n → K) ((Matrix.toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) A) μ
h : Nonempty n
v : n → K
h_eg :
  Membership.mem (γ := Submodule K (n → K))
    (((Module.End.genEigenspace (M := n → K) ((Matrix.toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) A) μ :
            ℕ∞ →o Submodule K (n → K)) :
          (a : ℕ∞) → Submodule K (n → K))
        1 :
      Submodule K (n → K))
    v
h_nz_1 : v ≠ 0
i : n
h_i : (Finset.sup' Finset.univ ⋯ fun (i : n) ↦ ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
h_le : ∀ (j : n), ‖v j * (v i)⁻¹‖ ≤ 1
⊢ ∃ (k : n), ‖A k k - μ‖ ≤ ∑ j ∈ Finset.erase Finset.univ k, ‖A k j‖
have inr : ‖A i i - μ‖ ≤ ∑ j ∈ Finset.erase Finset.univ i, ‖A i j‖
Tactic: refine ⟨i, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Gershgorin (goal)
Goal:
K : Type u_1
n : Type u_2
inst : NormedField K
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (M := n → K) ((Matrix.toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) A) μ
h : Nonempty n
v : n → K
h_eg :
  Membership.mem (γ := Submodule K (n → K))
    (((Module.End.genEigenspace (M := n → K) ((Matrix.toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) A) μ :
            ℕ∞ →o Submodule K (n → K)) :
          (a : ℕ∞) → Submodule K (n → K))
        1 :
      Submodule K (n → K))
    v
h_nz_1 : v ≠ 0
i : n
h_i : (Finset.sup' Finset.univ ⋯ fun (i : n) ↦ ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
h_le : ∀ (j : n), ‖v j * (v i)⁻¹‖ ≤ 1
⊢ ‖A i i - μ‖ = ‖(A i i * v i - μ * v i) * (v i)⁻¹‖
have e_a : A i i - μ = (A i i * v i - μ * v i) * (v i)⁻¹
Tactic: congr
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Gershgorin (goal)
Goal:
K : Type u_1
n : Type u_2
inst : NormedField K
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (M := n → K) ((Matrix.toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) A) μ
h : Nonempty n
v : n → K
h_eg :
  Membership.mem (γ := Submodule K (n → K))
    (((Module.End.genEigenspace (M := n → K) ((Matrix.toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) A) μ :
            ℕ∞ →o Submodule K (n → K)) :
          (a : ℕ∞) → Submodule K (n → K))
        1 :
      Submodule K (n → K))
    v
h_nz_1 : v ≠ 0
i : n
h_i : (Finset.sup' Finset.univ ⋯ fun (i : n) ↦ ‖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
have rw : μ * v i = A.mulVec v i
Tactic: rw [← dotProduct, ← Matrix.mulVec]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Gershgorin (goal)
Goal:
K : Type u_1
n : Type u_2
inst : NormedField K
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (M := n → K) ((Matrix.toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) A) μ
h : Nonempty n
v : n → K
h_eg :
  Membership.mem (γ := Submodule K (n → K))
    (((Module.End.genEigenspace (M := n → K) ((Matrix.toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) A) μ :
            ℕ∞ →o Submodule K (n → K)) :
          (a : ℕ∞) → Submodule K (n → K))
        1 :
      Submodule K (n → K))
    v
h_nz_1 : v ≠ 0
i : n
h_i : (Finset.sup' Finset.univ ⋯ fun (i : n) ↦ ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
h_le : ∀ (j : n), ‖v j * (v i)⁻¹‖ ≤ 1
⊢ ‖(A i i * v i - μ * v i) * (v i)⁻¹‖ = ‖(A i i * v i - ∑ j : n, A i j * v j) * (v i)⁻¹‖
have rw : ‖(A i i * v i - ∑ x : n, A i x * v x) * (v i)⁻¹‖ = ‖(A i i * v i - ∑ j : n, A i j * v j) * (v i)⁻¹‖
Tactic: rw [show μ * v i = ∑ x : n, A i x * v x by
                  rw [← dotProduct, ← Matrix.mulVec]
                  exact (congrFun (Module.End.mem_eigenspace_iff.mp h_eg) i).symm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Gershgorin (goal)
Goal:
K : Type u_1
n : Type u_2
inst : NormedField K
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (M := n → K) ((Matrix.toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) A) μ
h : Nonempty n
v : n → K
h_eg :
  Membership.mem (γ := Submodule K (n → K))
    (((Module.End.genEigenspace (M := n → K) ((Matrix.toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) A) μ :
            ℕ∞ →o Submodule K (n → K)) :
          (a : ℕ∞) → Submodule K (n → K))
        1 :
      Submodule K (n → K))
    v
h_nz_1 : v ≠ 0
i : n
h_i : (Finset.sup' Finset.univ ⋯ fun (i : n) ↦ ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
h_le : ∀ (j : n), ‖v j * (v i)⁻¹‖ ≤ 1
⊢ ‖(A i i * v i - ∑ j : n, A i j * v j) * (v i)⁻¹‖ = ‖(∑ j ∈ Finset.erase Finset.univ i, A i j * v j) * (v i)⁻¹‖
have rw : ‖(A i i * v i - ∑ j : n, A i j * v j) * (v i)⁻¹‖ = ‖(∑ x : n, A i x * v x - A i i * v i) * (v i)⁻¹‖
Tactic: rw [Finset.sum_erase_eq_sub (Finset.mem_univ i), ← neg_sub, neg_mul, norm_neg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Gershgorin (goal)
Goal:
K : Type u_1
n : Type u_2
inst : NormedField K
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (M := n → K) ((Matrix.toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) A) μ
h : Nonempty n
v : n → K
h_eg :
  Membership.mem (γ := Submodule K (n → K))
    (((Module.End.genEigenspace (M := n → K) ((Matrix.toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) A) μ :
            ℕ∞ →o Submodule K (n → K)) :
          (a : ℕ∞) → Submodule K (n → K))
        1 :
      Submodule K (n → K))
    v
h_nz_1 : v ≠ 0
i : n
h_i : (Finset.sup' Finset.univ ⋯ fun (i : n) ↦ ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
h_le : ∀ (j : n), ‖v j * (v i)⁻¹‖ ≤ 1
rw : ‖(A i i * v i - ∑ j : n, A i j * v j) * (v i)⁻¹‖ = ‖(∑ x : n, A i x * v x - A i i * v i) * (v i)⁻¹‖
⊢ ‖(A i i * v i - ∑ j : n, A i j * v j) * (v i)⁻¹‖ = ‖(∑ j ∈ Finset.erase Finset.univ i, A i j * v j) * (v i)⁻¹‖
have rw₁ : ‖-(∑ j : n, A i j * v j - A i i * v i) * (v i)⁻¹‖ = ‖(∑ x : n, A i x * v x - A i i * v i) * (v i)⁻¹‖
Tactic: rw [Finset.sum_erase_eq_sub (Finset.mem_univ i), ← neg_sub, neg_mul, norm_neg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Gershgorin (goal)
Goal:
K : Type u_1
n : Type u_2
inst : NormedField K
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (M := n → K) ((Matrix.toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) A) μ
h : Nonempty n
v : n → K
h_eg :
  Membership.mem (γ := Submodule K (n → K))
    (((Module.End.genEigenspace (M := n → K) ((Matrix.toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) A) μ :
            ℕ∞ →o Submodule K (n → K)) :
          (a : ℕ∞) → Submodule K (n → K))
        1 :
      Submodule K (n → K))
    v
h_nz_1 : v ≠ 0
i : n
h_i : (Finset.sup' Finset.univ ⋯ fun (i : n) ↦ ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
h_le : ∀ (j : n), ‖v j * (v i)⁻¹‖ ≤ 1
rw : ‖(A i i * v i - ∑ j : n, A i j * v j) * (v i)⁻¹‖ = ‖(∑ x : n, A i x * v x - A i i * v i) * (v i)⁻¹‖
rw₁ : ‖-(∑ j : n, A i j * v j - A i i * v i) * (v i)⁻¹‖ = ‖(∑ x : n, A i x * v x - A i i * v i) * (v i)⁻¹‖
⊢ ‖(A i i * v i - ∑ j : n, A i j * v j) * (v i)⁻¹‖ = ‖(∑ j ∈ Finset.erase Finset.univ i, A i j * v j) * (v i)⁻¹‖
have rw₂ : ‖-((∑ j : n, A i j * v j - A i i * v i) * (v i)⁻¹)‖ = ‖(∑ x : n, A i x * v x - A i i * v i) * (v i)⁻¹‖
Tactic: rw [Finset.sum_erase_eq_sub (Finset.mem_univ i), ← neg_sub, neg_mul, norm_neg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Gershgorin (goal)
Goal:
K : Type u_1
n : Type u_2
inst : NormedField K
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (M := n → K) ((Matrix.toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) A) μ
h : Nonempty n
v : n → K
h_eg :
  Membership.mem (γ := Submodule K (n → K))
    (((Module.End.genEigenspace (M := n → K) ((Matrix.toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) A) μ :
            ℕ∞ →o Submodule K (n → K)) :
          (a : ℕ∞) → Submodule K (n → K))
        1 :
      Submodule K (n → K))
    v
h_nz_1 : v ≠ 0
i : n
h_i : (Finset.sup' Finset.univ ⋯ fun (i : n) ↦ ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
h_le : ∀ (j : n), ‖v j * (v i)⁻¹‖ ≤ 1
rw : ‖(A i i * v i - ∑ j : n, A i j * v j) * (v i)⁻¹‖ = ‖(∑ x : n, A i x * v x - A i i * v i) * (v i)⁻¹‖
rw₁ : ‖-(∑ j : n, A i j * v j - A i i * v i) * (v i)⁻¹‖ = ‖(∑ x : n, A i x * v x - A i i * v i) * (v i)⁻¹‖
rw₂ : ‖-((∑ j : n, A i j * v j - A i i * v i) * (v i)⁻¹)‖ = ‖(∑ x : n, A i x * v x - A i i * v i) * (v i)⁻¹‖
⊢ ‖(A i i * v i - ∑ j : n, A i j * v j) * (v i)⁻¹‖ = ‖(∑ j ∈ Finset.erase Finset.univ i, A i j * v j) * (v i)⁻¹‖
have rw₃ : ‖(∑ j : n, A i j * v j - A i i * v i) * (v i)⁻¹‖ = ‖(∑ x : n, A i x * v x - A i i * v i) * (v i)⁻¹‖
Tactic: rw [Finset.sum_erase_eq_sub (Finset.mem_univ i), ← neg_sub, neg_mul, norm_neg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Gershgorin (goal)
Goal:
K : Type u_1
n : Type u_2
inst : NormedField K
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (M := n → K) ((Matrix.toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) A) μ
h : Nonempty n
v : n → K
h_eg :
  Membership.mem (γ := Submodule K (n → K))
    (((Module.End.genEigenspace (M := n → K) ((Matrix.toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) A) μ :
            ℕ∞ →o Submodule K (n → K)) :
          (a : ℕ∞) → Submodule K (n → K))
        1 :
      Submodule K (n → K))
    v
h_nz_1 : v ≠ 0
i : n
h_i : (Finset.sup' Finset.univ ⋯ fun (i : n) ↦ ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
h_le : ∀ (j : n), ‖v j * (v i)⁻¹‖ ≤ 1
⊢ ‖(∑ j ∈ Finset.erase Finset.univ i, A i j * v j) * (v i)⁻¹‖ ≤
    ∑ j ∈ Finset.erase Finset.univ i, ‖A i j‖ * ‖v j * (v i)⁻¹‖
have rw : norm.{u_1} (E := K) (∑ i_1 ∈ Finset.erase Finset.univ i, A i i_1 * v i_1 * (v i)⁻¹) ≤
  ∑ j ∈ Finset.erase Finset.univ i, ‖A i j‖ * ‖v j * (v i)⁻¹‖
Tactic: rw [Finset.sum_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Gershgorin (goal)
Goal:
K : Type u_1
n : Type u_2
inst : NormedField K
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (M := n → K) ((Matrix.toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) A) μ
h : Nonempty n
v : n → K
h_eg :
  Membership.mem (γ := Submodule K (n → K))
    (((Module.End.genEigenspace (M := n → K) ((Matrix.toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) A) μ :
            ℕ∞ →o Submodule K (n → K)) :
          (a : ℕ∞) → Submodule K (n → K))
        1 :
      Submodule K (n → K))
    v
h_nz_1 : v ≠ 0
i : n
h_i : (Finset.sup' Finset.univ ⋯ fun (i : n) ↦ ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
h_le : ∀ (j : n), ‖v j * (v i)⁻¹‖ ≤ 1
⊢ Eq (α := ℝ) (∑ i_1 ∈ Finset.erase Finset.univ i, ‖A i i_1 * v i_1 * (v i)⁻¹‖)
    (∑ j ∈ Finset.erase Finset.univ i, ‖A i j‖ * ‖v j * (v i)⁻¹‖)
have simp_rw : Eq (α := ℝ) (∑ x ∈ Finset.erase Finset.univ i, ‖A i x * (v x * (v i)⁻¹)‖)
  (∑ j ∈ Finset.erase Finset.univ i, ‖A i j‖ * ‖v j * (v i)⁻¹‖)
Tactic: simp_rw [mul_assoc, norm_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Gershgorin (goal)
Goal:
K : Type u_1
n : Type u_2
inst : NormedField K
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (M := n → K) ((Matrix.toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) A) μ
h : Nonempty n
v : n → K
h_eg :
  Membership.mem (γ := Submodule K (n → K))
    (((Module.End.genEigenspace (M := n → K) ((Matrix.toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) A) μ :
            ℕ∞ →o Submodule K (n → K)) :
          (a : ℕ∞) → Submodule K (n → K))
        1 :
      Submodule K (n → K))
    v
h_nz_1 : v ≠ 0
i : n
h_i : (Finset.sup' Finset.univ ⋯ fun (i : n) ↦ ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
h_le : ∀ (j : n), ‖v j * (v i)⁻¹‖ ≤ 1
⊢ ‖A i i - μ‖ ≤ ∑ j ∈ Finset.erase Finset.univ i, ‖A i j‖
have _ : ‖A i i - μ‖ = ‖(A i i * v i - μ * v i) * (v i)⁻¹‖
Tactic: calc
      _ = ‖(A i i * v i - μ * v i) * (v i)⁻¹‖ := by congr; field
      _ = ‖(A i i * v i - ∑ j, A i j * v j) * (v i)⁻¹‖ := by
                rw [show μ * v i = ∑ x : n, A i x * v x by
                  rw [← dotProduct, ← Matrix.mulVec]
                  exact (congrFun (Module.End.mem_eigenspace_iff.mp h_eg) i).symm]
      _ = ‖(∑ j ∈ Finset.univ.erase i, A i j * v j) * (v i)⁻¹‖ := by
                rw [Finset.sum_erase_eq_sub (Finset.mem_univ i), ← neg_sub, neg_mul, norm_neg]
      _ ≤ ∑ j ∈ Finset.univ.erase i, ‖A i j‖ * ‖v j * (v i)⁻¹‖ := by
                rw [Finset.sum_mul]
                exact (norm_sum_le _ _).trans (le_of_eq (by simp_rw [mul_assoc, norm_mul]))
      _ ≤ ∑ j ∈ Finset.univ.erase i, ‖A i j‖ :=
                (Finset.sum_le_sum fun j _ => mul_le_of_le_one_right (norm_nonneg _) (h_le j))
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Gershgorin (goal)
Goal:
K : Type u_1
n : Type u_2
inst : NormedField K
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (M := n → K) ((Matrix.toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) A) μ
h : Nonempty n
v : n → K
h_eg :
  Membership.mem (γ := Submodule K (n → K))
    (((Module.End.genEigenspace (M := n → K) ((Matrix.toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) A) μ :
            ℕ∞ →o Submodule K (n → K)) :
          (a : ℕ∞) → Submodule K (n → K))
        1 :
      Submodule K (n → K))
    v
h_nz_1 : v ≠ 0
i : n
h_i : (Finset.sup' Finset.univ ⋯ fun (i : n) ↦ ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
h_le : ∀ (j : n), ‖v j * (v i)⁻¹‖ ≤ 1
_ : ‖A i i - μ‖ = ‖(A i i * v i - μ * v i) * (v i)⁻¹‖
⊢ ‖A i i - μ‖ ≤ ∑ j ∈ Finset.erase Finset.univ i, ‖A i j‖
have _₁ : ‖(A i i * v i - μ * v i) * (v i)⁻¹‖ = ‖(A i i * v i - ∑ j : n, A i j * v j) * (v i)⁻¹‖
Tactic: calc
      _ = ‖(A i i * v i - μ * v i) * (v i)⁻¹‖ := by congr; field
      _ = ‖(A i i * v i - ∑ j, A i j * v j) * (v i)⁻¹‖ := by
                rw [show μ * v i = ∑ x : n, A i x * v x by
                  rw [← dotProduct, ← Matrix.mulVec]
                  exact (congrFun (Module.End.mem_eigenspace_iff.mp h_eg) i).symm]
      _ = ‖(∑ j ∈ Finset.univ.erase i, A i j * v j) * (v i)⁻¹‖ := by
                rw [Finset.sum_erase_eq_sub (Finset.mem_univ i), ← neg_sub, neg_mul, norm_neg]
      _ ≤ ∑ j ∈ Finset.univ.erase i, ‖A i j‖ * ‖v j * (v i)⁻¹‖ := by
                rw [Finset.sum_mul]
                exact (norm_sum_le _ _).trans (le_of_eq (by simp_rw [mul_assoc, norm_mul]))
      _ ≤ ∑ j ∈ Finset.univ.erase i, ‖A i j‖ :=
                (Finset.sum_le_sum fun j _ => mul_le_of_le_one_right (norm_nonneg _) (h_le j))
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Gershgorin (goal)
Goal:
K : Type u_1
n : Type u_2
inst : NormedField K
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (M := n → K) ((Matrix.toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) A) μ
h : Nonempty n
v : n → K
h_eg :
  Membership.mem (γ := Submodule K (n → K))
    (((Module.End.genEigenspace (M := n → K) ((Matrix.toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) A) μ :
            ℕ∞ →o Submodule K (n → K)) :
          (a : ℕ∞) → Submodule K (n → K))
        1 :
      Submodule K (n → K))
    v
h_nz_1 : v ≠ 0
i : n
h_i : (Finset.sup' Finset.univ ⋯ fun (i : n) ↦ ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
h_le : ∀ (j : n), ‖v j * (v i)⁻¹‖ ≤ 1
_ : ‖A i i - μ‖ = ‖(A i i * v i - μ * v i) * (v i)⁻¹‖
_₁ : ‖(A i i * v i - μ * v i) * (v i)⁻¹‖ = ‖(A i i * v i - ∑ j : n, A i j * v j) * (v i)⁻¹‖
⊢ ‖A i i - μ‖ ≤ ∑ j ∈ Finset.erase Finset.univ i, ‖A i j‖
have _₂ : ‖(A i i * v i - ∑ j : n, A i j * v j) * (v i)⁻¹‖ = ‖(∑ j ∈ Finset.erase Finset.univ i, A i j * v j) * (v i)⁻¹‖
Tactic: calc
      _ = ‖(A i i * v i - μ * v i) * (v i)⁻¹‖ := by congr; field
      _ = ‖(A i i * v i - ∑ j, A i j * v j) * (v i)⁻¹‖ := by
                rw [show μ * v i = ∑ x : n, A i x * v x by
                  rw [← dotProduct, ← Matrix.mulVec]
                  exact (congrFun (Module.End.mem_eigenspace_iff.mp h_eg) i).symm]
      _ = ‖(∑ j ∈ Finset.univ.erase i, A i j * v j) * (v i)⁻¹‖ := by
                rw [Finset.sum_erase_eq_sub (Finset.mem_univ i), ← neg_sub, neg_mul, norm_neg]
      _ ≤ ∑ j ∈ Finset.univ.erase i, ‖A i j‖ * ‖v j * (v i)⁻¹‖ := by
                rw [Finset.sum_mul]
                exact (norm_sum_le _ _).trans (le_of_eq (by simp_rw [mul_assoc, norm_mul]))
      _ ≤ ∑ j ∈ Finset.univ.erase i, ‖A i j‖ :=
                (Finset.sum_le_sum fun j _ => mul_le_of_le_one_right (norm_nonneg _) (h_le j))
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Gershgorin (goal)
Goal:
K : Type u_1
n : Type u_2
inst : NormedField K
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (M := n → K) ((Matrix.toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) A) μ
h : Nonempty n
v : n → K
h_eg :
  Membership.mem (γ := Submodule K (n → K))
    (((Module.End.genEigenspace (M := n → K) ((Matrix.toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) A) μ :
            ℕ∞ →o Submodule K (n → K)) :
          (a : ℕ∞) → Submodule K (n → K))
        1 :
      Submodule K (n → K))
    v
h_nz_1 : v ≠ 0
i : n
h_i : (Finset.sup' Finset.univ ⋯ fun (i : n) ↦ ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
h_le : ∀ (j : n), ‖v j * (v i)⁻¹‖ ≤ 1
_ : ‖A i i - μ‖ = ‖(A i i * v i - μ * v i) * (v i)⁻¹‖
_₁ : ‖(A i i * v i - μ * v i) * (v i)⁻¹‖ = ‖(A i i * v i - ∑ j : n, A i j * v j) * (v i)⁻¹‖
_₂ : ‖(A i i * v i - ∑ j : n, A i j * v j) * (v i)⁻¹‖ = ‖(∑ j ∈ Finset.erase Finset.univ i, A i j * v j) * (v i)⁻¹‖
⊢ ‖A i i - μ‖ ≤ ∑ j ∈ Finset.erase Finset.univ i, ‖A i j‖
have _₃ : ‖(∑ j ∈ Finset.erase Finset.univ i, A i j * v j) * (v i)⁻¹‖ ≤
  ∑ j ∈ Finset.erase Finset.univ i, ‖A i j‖ * ‖v j * (v i)⁻¹‖
Tactic: calc
      _ = ‖(A i i * v i - μ * v i) * (v i)⁻¹‖ := by congr; field
      _ = ‖(A i i * v i - ∑ j, A i j * v j) * (v i)⁻¹‖ := by
                rw [show μ * v i = ∑ x : n, A i x * v x by
                  rw [← dotProduct, ← Matrix.mulVec]
                  exact (congrFun (Module.End.mem_eigenspace_iff.mp h_eg) i).symm]
      _ = ‖(∑ j ∈ Finset.univ.erase i, A i j * v j) * (v i)⁻¹‖ := by
                rw [Finset.sum_erase_eq_sub (Finset.mem_univ i), ← neg_sub, neg_mul, norm_neg]
      _ ≤ ∑ j ∈ Finset.univ.erase i, ‖A i j‖ * ‖v j * (v i)⁻¹‖ := by
                rw [Finset.sum_mul]
                exact (norm_sum_le _ _).trans (le_of_eq (by simp_rw [mul_assoc, norm_mul]))
      _ ≤ ∑ j ∈ Finset.univ.erase i, ‖A i j‖ :=
                (Finset.sum_le_sum fun j _ => mul_le_of_le_one_right (norm_nonneg _) (h_le j))
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Gershgorin (goal)
Goal:
K : Type u_1
n : Type u_2
inst : NormedField K
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n K
h : ∀ (k : n), ∑ j ∈ Finset.erase Finset.univ k, ‖A k j‖ < ‖A k k‖
⊢ A.det ≠ 0
have contrapose! : ∀ (h : A.det = 0), ∃ (k : n), ‖A k k‖ ≤ ∑ j ∈ Finset.erase Finset.univ k, ‖A k j‖
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Gershgorin (goal)
Goal:
K : Type u_1
n : Type u_2
inst : NormedField K
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n K
h_1 : A.det = 0
this : ∃ (k : n), 0 ∈ Metric.closedBall (A k k) (∑ j ∈ Finset.erase Finset.univ k, ‖A k j‖)
a : n
h : 0 ∈ Metric.closedBall (A a a) (∑ j ∈ Finset.erase Finset.univ a, ‖A a j‖)
⊢ ‖A a a‖ ≤ ∑ j ∈ Finset.erase Finset.univ a, ‖A a j‖
have rwa : ∀ (h : ‖A a a - 0‖ ≤ ∑ j ∈ Finset.erase Finset.univ a, ‖A a j‖), ‖A a a‖ ≤ ∑ j ∈ Finset.erase Finset.univ a, ‖A a j‖
Tactic: rwa [mem_closedBall_iff_norm', sub_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Gershgorin (goal)
Goal:
K : Type u_1
n : Type u_2
inst : NormedField K
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n K
h_1 : A.det = 0
this : ∃ (k : n), 0 ∈ Metric.closedBall (A k k) (∑ j ∈ Finset.erase Finset.univ k, ‖A k j‖)
a : n
h : 0 ∈ Metric.closedBall (A a a) (∑ j ∈ Finset.erase Finset.univ a, ‖A a j‖)
rwa :
  ∀ (h : ‖A a a - 0‖ ≤ ∑ j ∈ Finset.erase Finset.univ a, ‖A a j‖), ‖A a a‖ ≤ ∑ j ∈ Finset.erase Finset.univ a, ‖A a j‖
⊢ ‖A a a‖ ≤ ∑ j ∈ Finset.erase Finset.univ a, ‖A a j‖
have rwa₁ : ∀ (h : ‖A a a‖ ≤ ∑ j ∈ Finset.erase Finset.univ a, ‖A a j‖), ‖A a a‖ ≤ ∑ j ∈ Finset.erase Finset.univ a, ‖A a j‖
Tactic: rwa [mem_closedBall_iff_norm', sub_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Gershgorin (goal)
Goal:
K : Type u_1
n : Type u_2
inst : NormedField K
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n K
h : A.det = 0
⊢ ∃ (k : n), ‖A k k‖ ≤ ∑ j ∈ Finset.erase Finset.univ k, ‖A k j‖
have suffices : ∃ (k : n), 0 ∈ Metric.closedBall (A k k) (∑ j ∈ Finset.erase Finset.univ k, ‖A k j‖)
Tactic: suffices ∃ k, 0 ∈ Metric.closedBall (A k k) (∑ j ∈ Finset.univ.erase k, ‖A k j‖) by
    exact this.imp (fun a h ↦ by rwa [mem_closedBall_iff_norm', sub_zero] at h)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Gershgorin (goal)
Goal:
K : Type u_1
n : Type u_2
inst : NormedField K
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n K
h : A.det = 0
⊢ ∃ (k : n), 0 ∈ Metric.closedBall (A k k) (∑ j ∈ Finset.erase Finset.univ k, ‖A k j‖)
have refine : Module.End.HasEigenvalue (R := K) (M := n → K) ((Matrix.toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) A) 0
Tactic: refine eigenvalue_mem_ball ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Gershgorin (goal)
Goal:
K : Type u_1
n : Type u_2
inst : NormedField K
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n K
h : A.det = 0
⊢ Module.End.HasEigenvalue (R := K) (M := n → K) ((Matrix.toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) A) 0
have rw : Ne (α := Submodule K (n → K)) ⊥
  (LinearMap.ker (R₂ := K) (M₂ := n → K) (τ₁₂ := RingHom.id K)
    ((Matrix.toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) A))
Tactic: rw [Module.End.hasEigenvalue_iff, Module.End.eigenspace_zero, ne_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Gershgorin (goal)
Goal:
K : Type u_1
n : Type u_2
inst : NormedField K
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n K
h : ∀ (k : n), ∑ i ∈ Finset.erase Finset.univ k, ‖A i k‖ < ‖A k k‖
⊢ A.det ≠ 0
have rw : A.transpose.det ≠ 0
Tactic: rw [← Matrix.det_transpose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hadamard (goal)
Goal:
α : Type u_1
m : Type u_2
n : Type u_3
inst : MulOneClass α
A : Matrix m n α
⊢ A ⊙ (of : (a : m → n → α) → Matrix m n α) 1 = A
have a : ∀ (i : m) (j : n), (A ⊙ (of : (a : m → n → α) → Matrix m n α) 1) i j = A i j
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hadamard (goal)
Goal:
α : Type u_1
m : Type u_2
n : Type u_3
inst : MulOneClass α
A : Matrix m n α
⊢ (of : (a : m → n → α) → Matrix m n α) 1 ⊙ A = A
have a : ∀ (i : m) (j : n), ((of : (a : m → n → α) → Matrix m n α) 1 ⊙ A) i j = A i j
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hadamard (goal)
Goal:
α : Type u_1
m : Type u_2
n : Type u_3
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : MulZeroClass α
ia : m
ja : n
ib : m
jb : n
h : ¬(ia = ib ∧ ja = jb)
a b : α
⊢ single ia ja a ⊙ single ib jb b = 0
have rw : ∀ (h : ¬ia = ib ∨ ¬ja = jb) (a b : α), single ia ja a ⊙ single ib jb b = 0
Tactic: rw [not_and_or] at h
Cleared hypotheses: h, a, b
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hadamard (goal)
Goal:
α : Type u_1
m : Type u_2
n : Type u_3
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : MulZeroClass α
ia : m
ja : n
ib : m
jb : n
h : ¬ia = ib ∨ ¬ja = jb
a b : α
⊢ single ia ja a ⊙ single ib jb b = 0
have inl : ¬ia = ib → single ia ja a ⊙ single ib jb b = 0
Tactic: cases h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hadamard (goal)
Goal:
α : Type u_1
m : Type u_2
n : Type u_3
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : MulZeroClass α
ia : m
ja : n
ib : m
jb : n
h : ¬ia = ib ∨ ¬ja = jb
a b : α
inl : ¬ia = ib → single ia ja a ⊙ single ib jb b = 0
⊢ single ia ja a ⊙ single ib jb b = 0
have inr : ¬ja = jb → single ia ja a ⊙ single ib jb b = 0
Tactic: cases h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hadamard (goal)
Goal:
α : Type u_1
m : Type u_2
n : Type u_3
A B : Matrix m n α
inst : Fintype m
inst_1 : Fintype n
inst_2 : NonUnitalSemiring α
inst_3 : DecidableEq m
inst_4 : DecidableEq n
v : m → α
w : n → α
⊢ v ᵥ* A ⊙ B ⬝ᵥ w = (diagonal v * A * (B * diagonal w)ᵀ).trace
have rw : v ᵥ* A ⊙ B ⬝ᵥ w = ∑ y : n, ∑ x : m, ((diagonal v * A) ⊙ (B * diagonal w)) x y
Tactic: rw [← sum_hadamard_eq, Finset.sum_comm]