awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Gershgorin
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
inr : ‖A i i - μ‖ ≤ ∑ j ∈ Finset.erase Finset.univ i, ‖A i j‖
⊢ ∃ (k : n), ‖A k k - μ‖ ≤ ∑ j ∈ Finset.erase Finset.univ k, ‖A k j‖

Tactic:
refine ⟨i, ?_⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Gershgorin
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
e_a : A i i - μ = (A i i * v i - μ * v i) * (v i)⁻¹
⊢ ‖A i i - μ‖ = ‖(A i i * v i - μ * v i) * (v i)⁻¹‖

Tactic:
congr
-- Module: Mathlib.LinearAlgebra.Matrix.Gershgorin
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)⁻¹

Tactic:
field
-- Module: Mathlib.LinearAlgebra.Matrix.Gershgorin
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 : μ * v i = A.mulVec v i
⊢ μ * v i = ∑ x : n, A i x * v x

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

Premises used: dotProduct, Matrix.mulVec
-- Module: Mathlib.LinearAlgebra.Matrix.Gershgorin
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 = A.mulVec v i

Tactic:
(congrFun (Module.End.mem_eigenspace_iff.mp h_eg) i).symm

Premises used: Multiset.sum, Multiset.foldr, dotProduct, Module.End.mem_eigenspace_iff, congrFun, Iff.mp, Eq.symm, Matrix.mulVec, Finset.sum
-- Module: Mathlib.LinearAlgebra.Matrix.Gershgorin
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 = A.mulVec v i

Tactic:
exact (congrFun (Module.End.mem_eigenspace_iff.mp h_eg) i).symm

Premises used: Module.End.mem_eigenspace_iff, congrFun, Iff.mp, Eq.symm
-- Module: Mathlib.LinearAlgebra.Matrix.Gershgorin
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 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)⁻¹‖
⊢ ‖(A i i * v i - μ * v i) * (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]
-- Module: Mathlib.LinearAlgebra.Matrix.Gershgorin
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)⁻¹‖
rw₃ 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)⁻¹‖

Tactic:
rw [Finset.sum_erase_eq_sub (Finset.mem_univ i), ← neg_sub, neg_mul, norm_neg]

Premises used: Finset.mem_univ, neg_sub, Finset.sum_erase_eq_sub, norm_neg, neg_mul
-- Module: Mathlib.LinearAlgebra.Matrix.Gershgorin
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 :
  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)⁻¹‖
⊢ ‖(∑ 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:
rw [Finset.sum_mul]

Premises used: Finset.sum_mul
-- Module: Mathlib.LinearAlgebra.Matrix.Gershgorin
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
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)⁻¹‖)
⊢ 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)⁻¹‖)

Tactic:
simp_rw [mul_assoc, norm_mul]

Premises used: mul_assoc, norm_mul
-- Module: Mathlib.LinearAlgebra.Matrix.Gershgorin
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
⊢ 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:
exact (norm_sum_le _ _).trans (le_of_eq (by simp_rw [mul_assoc, norm_mul]))

Premises used: LE.le.trans, le_of_eq, norm_sum_le
-- Module: Mathlib.LinearAlgebra.Matrix.Gershgorin
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
⊢ LE.le (α := ℝ) (∑ j ∈ Finset.erase Finset.univ i, ‖A i j‖ * ‖v j * (v i)⁻¹‖)
    (∑ j ∈ Finset.erase Finset.univ i, ‖A i j‖)

Tactic:
(Finset.sum_le_sum fun j _ => mul_le_of_le_one_right (norm_nonneg _) (h_le j))

Premises used: mul_le_of_le_one_right, Finset.sum_le_sum, norm_nonneg
-- Module: Mathlib.LinearAlgebra.Matrix.Gershgorin
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)⁻¹‖
_₃ :
  ‖(∑ 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)⁻¹‖
⊢ ‖A i i - μ‖ ≤ ∑ j ∈ Finset.erase Finset.univ i, ‖A i j‖

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))

Premises used: HMul.hMul, Finset.univ, HSub.hSub, mul_le_of_le_one_right, Finset.sum_le_sum, Finset.erase, norm_nonneg, Finset.sum
-- Module: Mathlib.LinearAlgebra.Matrix.Gershgorin
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‖
contrapose! : ∀ (h : A.det = 0), ∃ (k : n), ‖A k k‖ ≤ ∑ j ∈ Finset.erase Finset.univ k, ‖A k j‖
⊢ A.det ≠ 0

Tactic:
contrapose! h
-- Module: Mathlib.LinearAlgebra.Matrix.Gershgorin
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‖
rwa₁ rwa₂ rwa₃ 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‖
⊢ ‖A a a‖ ≤ ∑ j ∈ Finset.erase Finset.univ a, ‖A a j‖

Tactic:
rwa [mem_closedBall_iff_norm', sub_zero] at h

Premises used: sub_zero, mem_closedBall_iff_norm'
-- Module: Mathlib.LinearAlgebra.Matrix.Gershgorin
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
this : ∃ (k : n), 0 ∈ Metric.closedBall (A k k) (∑ j ∈ Finset.erase Finset.univ k, ‖A k j‖)
⊢ ∃ (k : n), ‖A k k‖ ≤ ∑ j ∈ Finset.erase Finset.univ k, ‖A k j‖

Tactic:
exact this.imp (fun a h ↦ by rwa [mem_closedBall_iff_norm', sub_zero] at h)

Premises used: Exists.imp
-- Module: Mathlib.LinearAlgebra.Matrix.Gershgorin
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
suffices : ∃ (k : n), 0 ∈ Metric.closedBall (A k k) (∑ j ∈ Finset.erase Finset.univ k, ‖A k j‖)
⊢ ∃ (k : n), ‖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)
-- Module: Mathlib.LinearAlgebra.Matrix.Gershgorin
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‖)

Tactic:
eigenvalue_mem_ball ?_

Premises used: eigenvalue_mem_ball
-- Module: Mathlib.LinearAlgebra.Matrix.Gershgorin
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
refine : Module.End.HasEigenvalue (R := K) (M := n → K) ((Matrix.toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) A) 0
⊢ ∃ (k : n), 0 ∈ Metric.closedBall (A k k) (∑ j ∈ Finset.erase Finset.univ k, ‖A k j‖)

Tactic:
refine eigenvalue_mem_ball ?_

Premises used: eigenvalue_mem_ball
-- Module: Mathlib.LinearAlgebra.Matrix.Gershgorin
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
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))
⊢ Module.End.HasEigenvalue (R := K) (M := n → K) ((Matrix.toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) A) 0

Tactic:
rw [Module.End.hasEigenvalue_iff, Module.End.eigenspace_zero, ne_comm]

Premises used: Module.End.hasEigenvalue_iff, Module.End.eigenspace_zero, ne_comm
-- Module: Mathlib.LinearAlgebra.Matrix.Gershgorin
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
rwa rwa₁ rwa₂ rwa₃ : A.det = 0
⊢ Eq.{u_1 + 1} (α := K)
    (((LinearMap.det (M := n → K) (A := K) : ((n → K) →ₗ[K] n → K) →* K) : (a : (n → K) →ₗ[K] n → K) → K)
        ((Matrix.toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) A : (n → K) →ₗ[K] n → K) :
      K)
    (0 : K)

Tactic:
rwa [LinearMap.det_toLin']

Premises used: LinearMap.det_toLin'
-- Module: Mathlib.LinearAlgebra.Matrix.Gershgorin
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
⊢ 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:
exact ne_of_lt (LinearMap.bot_lt_ker_of_det_eq_zero (by rwa [LinearMap.det_toLin']))

Premises used: LinearMap.bot_lt_ker_of_det_eq_zero, ne_of_lt
-- Module: Mathlib.LinearAlgebra.Matrix.Gershgorin
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‖
rw : A.transpose.det ≠ 0
⊢ A.det ≠ 0

Tactic:
rw [← Matrix.det_transpose]

Premises used: Matrix.det_transpose
-- Module: Mathlib.LinearAlgebra.Matrix.Gershgorin
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 simp_rw : ∀ (k : n), ∑ x ∈ Finset.erase Finset.univ k, ‖A x k‖ < ‖A k k‖
⊢ ∀ (k : n), ∑ j ∈ Finset.erase Finset.univ k, ‖A.transpose k j‖ < ‖A.transpose k k‖

Tactic:
simp_rw [Matrix.transpose_apply]

Premises used: Matrix.transpose_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Gershgorin
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‖
⊢ ∀ (k : n), ∑ x ∈ Finset.erase Finset.univ k, ‖A x k‖ < ‖A k k‖

Tactic:
h
-- Module: Mathlib.LinearAlgebra.Matrix.Gershgorin
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‖
⊢ ∀ (k : n), ∑ x ∈ Finset.erase Finset.univ k, ‖A x k‖ < ‖A k k‖

Tactic:
exact h
-- Module: Mathlib.LinearAlgebra.Matrix.Gershgorin
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.transpose.det ≠ 0

Tactic:
exact det_ne_zero_of_sum_row_lt_diag (by simp_rw [Matrix.transpose_apply]; exact h)

Premises used: det_ne_zero_of_sum_row_lt_diag
-- Module: Mathlib.LinearAlgebra.Matrix.Hadamard
Goal:
α : Type u_1
m : Type u_2
n : Type u_3
inst : Mul α
A B : Matrix m n α
i : m
j : n
⊢ A.hadamard B i j = A i j * B i j

Tactic:
rfl

Premises used: Matrix.hadamard, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Hadamard
Goal:
α : Type u_1
m : Type u_2
n : Type u_3
A B : Matrix m n α
inst : CommMagma α
⊢ A ⊙ B = B ⊙ A

Tactic:
ext fun _ _ => mul_comm _ _

Premises used: mul_comm, Matrix.ext
-- Module: Mathlib.LinearAlgebra.Matrix.Hadamard
Goal:
α : Type u_1
m : Type u_2
n : Type u_3
A B C : Matrix m n α
inst : Semigroup α
⊢ A ⊙ B ⊙ C = A ⊙ (B ⊙ C)

Tactic:
ext fun _ _ => mul_assoc _ _ _

Premises used: mul_assoc, Matrix.ext
-- Module: Mathlib.LinearAlgebra.Matrix.Hadamard
Goal:
α : Type u_1
m : Type u_2
n : Type u_3
A B C : Matrix m n α
inst : Distrib α
⊢ A ⊙ (B + C) = A ⊙ B + A ⊙ C

Tactic:
ext fun _ _ => left_distrib _ _ _

Premises used: Matrix.ext, left_distrib
-- Module: Mathlib.LinearAlgebra.Matrix.Hadamard
Goal:
α : Type u_1
m : Type u_2
n : Type u_3
A B C : Matrix m n α
inst : Distrib α
⊢ (B + C) ⊙ A = B ⊙ A + C ⊙ A

Tactic:
ext fun _ _ => right_distrib _ _ _

Premises used: right_distrib, Matrix.ext
-- Module: Mathlib.LinearAlgebra.Matrix.Hadamard
Goal:
α : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
A B : Matrix m n α
inst : Mul α
inst_1 : SMul R α
inst_2 : IsScalarTower R α α
k : R
⊢ (k • A) ⊙ B = k • A ⊙ B

Tactic:
ext fun _ _ => smul_mul_assoc _ _ _

Premises used: smul_mul_assoc, Matrix.ext
-- Module: Mathlib.LinearAlgebra.Matrix.Hadamard
Goal:
α : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
A B : Matrix m n α
inst : Mul α
inst_1 : SMul R α
inst_2 : SMulCommClass R α α
k : R
⊢ A ⊙ (k • B) = k • A ⊙ B

Tactic:
ext fun _ _ => mul_smul_comm _ _ _

Premises used: mul_smul_comm, Matrix.ext
-- Module: Mathlib.LinearAlgebra.Matrix.Hadamard
Goal:
α : Type u_1
m : Type u_2
n : Type u_3
A : Matrix m n α
inst : MulZeroClass α
⊢ A ⊙ 0 = 0

Tactic:
ext fun _ _ => mul_zero _

Premises used: MulZeroClass.mul_zero, Matrix.ext
-- Module: Mathlib.LinearAlgebra.Matrix.Hadamard
Goal:
α : Type u_1
m : Type u_2
n : Type u_3
A : Matrix m n α
inst : MulZeroClass α
⊢ 0 ⊙ A = 0

Tactic:
ext fun _ _ => zero_mul _

Premises used: MulZeroClass.zero_mul, Matrix.ext
-- Module: Mathlib.LinearAlgebra.Matrix.Hadamard
Goal:
α : Type u_1
n : Type u_3
inst : DecidableEq n
inst_1 : MulZeroClass α
M : Matrix n n α
w : n → α
⊢ M ⊙ diagonal w = diagonal (M.diag * w)

Tactic:
aesop (add simp diagonal)

Premises used: Matrix.diagonal
-- Module: Mathlib.LinearAlgebra.Matrix.Hadamard
Goal:
α : Type u_1
n : Type u_3
inst : DecidableEq n
inst_1 : MulZeroClass α
M : Matrix n n α
w : n → α
⊢ diagonal w ⊙ M = diagonal (w * M.diag)

Tactic:
aesop (add simp diagonal)

Premises used: Matrix.diagonal
-- Module: Mathlib.LinearAlgebra.Matrix.Hadamard
Goal:
α : Type u_1
n : Type u_3
inst : DecidableEq n
inst_1 : MulZeroClass α
v w : n → α
⊢ diagonal v ⊙ diagonal w = diagonal (v * w)

Tactic:
simp [diagonal_hadamard]

Premises used: Matrix.diagonal_hadamard
-- Module: Mathlib.LinearAlgebra.Matrix.Hadamard
Goal:
α : Type u_1
n : Type u_3
inst : DecidableEq n
inst_1 : MulZeroClass α
A : Matrix n n α
d e : n → α
⊢ diagonal d ⊙ A = diagonal e ↔ d * A.diag = e

Tactic:
simp [diagonal_hadamard, diagonal_eq_diagonal_iff, funext_iff]

Premises used: Matrix.diagonal_eq_diagonal_iff, funext_iff, Matrix.diagonal_hadamard
-- Module: Mathlib.LinearAlgebra.Matrix.Hadamard
Goal:
α : Type u_1
n : Type u_3
inst : DecidableEq n
inst_1 : MulZeroClass α
A : Matrix n n α
d e : n → α
⊢ A ⊙ diagonal d = diagonal e ↔ A.diag * d = e

Tactic:
simp [hadamard_diagonal, diagonal_eq_diagonal_iff, funext_iff]

Premises used: Matrix.diagonal_eq_diagonal_iff, funext_iff, Matrix.hadamard_diagonal