awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
Goal:
n : Type u_1
R : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
u : Rˣ
rw :
  Membership.mem (α := GL n R) (γ := Subgroup (GL n R)) (MonoidHom.range (GeneralLinearGroup.scalar n))
    ((GeneralLinearGroup.scalar n : (a : Rˣ) → GL n R) u : GL n R)
⊢ Eq (α := PGL(n, R))
    ((mk : (a : GL n R) → PGL(n, R)) ((GeneralLinearGroup.scalar n : (a : Rˣ) → GL n R) u) : PGL(n, R)) (1 : PGL(n, R))

Tactic:
rw [← MonoidHom.mem_ker, ker_mk, GeneralLinearGroup.center_eq_range_scalar]

Premises used: Matrix.GeneralLinearGroup.center_eq_range_scalar, Matrix.ProjGenLinGroup.ker_mk, MonoidHom.mem_ker
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
Goal:
n : Type u_1
R : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
u : Rˣ
⊢ Membership.mem (α := GL n R) (γ := Subgroup (GL n R)) (MonoidHom.range (GeneralLinearGroup.scalar n))
    ((GeneralLinearGroup.scalar n : (a : Rˣ) → GL n R) u : GL n R)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
Goal:
n : Type u_1
R : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
motive : PGL(n, R) → Prop
g : PGL(n, R)
mk : ∀ (g : GL n R), motive ((ProjGenLinGroup.mk : (a : GL n R) → PGL(n, R)) g)
⊢ motive g

Tactic:
Quotient.inductionOn g mk

Premises used: Quotient.inductionOn
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
Goal:
n : Type u_1
R : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
M : Type u_3
inst_3 : Monoid M
f : GL n R →* M
hf : f.comp (GeneralLinearGroup.scalar n) = 1
rwa : MonoidHom.range (GeneralLinearGroup.scalar n) ≤ f.ker
rwa₁ rwa₂ rwa₃ rwa₄ : f.comp (GeneralLinearGroup.scalar n) = 1
⊢ Subgroup.center (GL n R) ≤ f.ker

Tactic:
rwa [GeneralLinearGroup.center_eq_range_scalar, MonoidHom.range_le_ker_iff]

Premises used: Matrix.GeneralLinearGroup.center_eq_range_scalar, MonoidHom.range_le_ker_iff
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
Goal:
n : Type u_1
R : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
M : Type u_3
inst_3 : Monoid M
f : GL n R →* M
hf : f.comp (GeneralLinearGroup.scalar n) = 1
g : GL n R
⊢ Eq.{u_3 + 1} (α := M) ((lift f hf : (a : PGL(n, R)) → M) ((mk : (a : GL n R) → PGL(n, R)) g : PGL(n, R)) : M)
    ((f : (a : GL n R) → M) g : M)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
Goal:
n : Type u_1
R : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
M : Type u_3
inst_3 : Monoid M
f : GL n R →* M
hf : f.comp (GeneralLinearGroup.scalar n) = 1
⊢ (lift f hf).comp mk = f

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
Goal:
n : Type u_1
R : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
M : Type u_3
inst_3 : Monoid M
α : Type u_4
inst_4 : MulAction (GL n R) α
h : ∀ (u : Rˣ) (a : α), HSMul.hSMul (α := GL n R) ((GeneralLinearGroup.scalar n : (a : Rˣ) → GL n R) u : GL n R) a = a
h₁ :
  ∀ (u : Rˣ),
    Eq.{u_4 + 1} (α := Function.End α)
      ((MonoidHom.comp (N := GL n R) MulAction.toEndHom (GeneralLinearGroup.scalar n) : (a : Rˣ) → Function.End α) u :
        Function.End α)
      (((1 : MonoidHom.{u_2, u_4} Rˣ (Function.End α)) : (a : Rˣ) → Function.End α) u : Function.End α)
⊢ Eq (α := MonoidHom.{u_2, u_4} Rˣ (Function.End α))
    (MonoidHom.comp (N := GL n R) MulAction.toEndHom (GeneralLinearGroup.scalar n)) 1

Tactic:
ext u
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
Goal:
n : Type u_1
R : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
M : Type u_3
inst_3 : Monoid M
α : Type u_4
inst_4 : MulAction (GL n R) α
h : ∀ (u : Rˣ) (a : α), HSMul.hSMul (α := GL n R) ((GeneralLinearGroup.scalar n : (a : Rˣ) → GL n R) u : GL n R) a = a
u : Rˣ
h₁ :
  ∀ (a : α),
    Eq.{u_4 + 1} (α := α)
      ((MonoidHom.comp (N := GL n R) MulAction.toEndHom (GeneralLinearGroup.scalar n) : (a : Rˣ) → Function.End α) u a :
        α)
      (((1 : MonoidHom.{u_2, u_4} Rˣ (Function.End α)) : (a : Rˣ) → Function.End α) u a : α)
⊢ Eq.{u_4 + 1} (α := Function.End α)
    ((MonoidHom.comp (N := GL n R) MulAction.toEndHom (GeneralLinearGroup.scalar n) : (a : Rˣ) → Function.End α) u :
      Function.End α)
    (((1 : MonoidHom.{u_2, u_4} Rˣ (Function.End α)) : (a : Rˣ) → Function.End α) u : Function.End α)

Tactic:
funext a
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
Goal:
n : Type u_1
R : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
M : Type u_3
inst_3 : Monoid M
α : Type u_4
inst_4 : MulAction (GL n R) α
h : ∀ (u : Rˣ) (a : α), HSMul.hSMul (α := GL n R) ((GeneralLinearGroup.scalar n : (a : Rˣ) → GL n R) u : GL n R) a = a
u : Rˣ
a : α
⊢ Eq.{u_4 + 1} (α := α)
    ((MonoidHom.comp (N := GL n R) MulAction.toEndHom (GeneralLinearGroup.scalar n) : (a : Rˣ) → Function.End α) u a :
      α)
    (((1 : MonoidHom.{u_2, u_4} Rˣ (Function.End α)) : (a : Rˣ) → Function.End α) u a : α)

Tactic:
h u a
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
Goal:
n : Type u_1
R : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
M : Type u_3
inst_3 : Monoid M
α : Type u_4
inst_4 : MulAction (GL n R) α
h : ∀ (u : Rˣ) (a : α), HSMul.hSMul (α := GL n R) ((GeneralLinearGroup.scalar n : (a : Rˣ) → GL n R) u : GL n R) a = a
u : Rˣ
a : α
⊢ Eq.{u_4 + 1} (α := α)
    ((MonoidHom.comp (N := GL n R) MulAction.toEndHom (GeneralLinearGroup.scalar n) : (a : Rˣ) → Function.End α) u a :
      α)
    (((1 : MonoidHom.{u_2, u_4} Rˣ (Function.End α)) : (a : Rˣ) → Function.End α) u a : α)

Tactic:
exact h u a
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
Goal:
n : Type u_1
R : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
α : Type u_4
inst_3 : MulAction (GL n R) α
h : ∀ (u : Rˣ) (a : α), HSMul.hSMul (α := GL n R) ((GeneralLinearGroup.scalar n : (a : Rˣ) → GL n R) u : GL n R) a = a
g : GL n R
a : α
⊢ HSMul.hSMul (α := PGL(n, R)) ((mk : (a : GL n R) → PGL(n, R)) g : PGL(n, R)) a = g • a

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
Goal:
n : Type u_1
R : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
M : Type u_3
inst_3 : Monoid M
inst_4 : Fact (Even (Fintype.card n))
inst_5 : LinearOrder R
inst_6 : IsStrictOrderedRing R
h :
  ∀ (u : Rˣ),
    Eq (α := SignType)
      (↑(((MonoidHom.comp (N := GL n R) (MonoidHom.comp (Units.map (↑signHom : R →* SignType)) GeneralLinearGroup.det)
                  (GeneralLinearGroup.scalar n) :
                Rˣ →* SignTypeˣ) :
              (a : Rˣ) → SignTypeˣ)
            u) :
        SignType)
      (↑(((1 : Rˣ →* SignTypeˣ) : (a : Rˣ) → SignTypeˣ) u) : SignType)
⊢ Eq.{max (u_2 + 1) 1} (α := Rˣ →* SignTypeˣ)
    (MonoidHom.comp (N := GL n R) (MonoidHom.comp (Units.map (↑signHom : R →* SignType)) GeneralLinearGroup.det)
      (GeneralLinearGroup.scalar n))
    1

Tactic:
ext u
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
Goal:
n : Type u_1
R : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
M : Type u_3
inst_3 : Monoid M
inst_4 : Fact (Even (Fintype.card n))
inst_5 : LinearOrder R
inst_6 : IsStrictOrderedRing R
u : Rˣ
⊢ Eq (α := SignType)
    (↑(((MonoidHom.comp (N := GL n R) (MonoidHom.comp (Units.map (↑signHom : R →* SignType)) GeneralLinearGroup.det)
                (GeneralLinearGroup.scalar n) :
              Rˣ →* SignTypeˣ) :
            (a : Rˣ) → SignTypeˣ)
          u) :
      SignType)
    (↑(((1 : Rˣ →* SignTypeˣ) : (a : Rˣ) → SignTypeˣ) u) : SignType)

Tactic:
simp [← sign_pow, Even.pow_pos Fact.out]

Premises used: Even.pow_pos, sign_pow, Fact.out
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
Goal:
n : Type u_1
R : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
inst_3 : Fact (Even (Fintype.card n))
inst_4 : LinearOrder R
inst_5 : IsStrictOrderedRing R
g : GL n R
⊢ Eq (α := SignTypeˣ)
    (((signDet : PGL(n, R) →* SignTypeˣ) : (a : PGL(n, R)) → SignTypeˣ) ((mk : (a : GL n R) → PGL(n, R)) g) : SignTypeˣ)
    (((Units.map (↑signHom : R →* SignType) : Rˣ →* SignTypeˣ) : (a : Rˣ) → SignTypeˣ)
        ((GeneralLinearGroup.det : (a : GL n R) → Rˣ) g) :
      SignTypeˣ)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
Goal:
n : Type u_1
R : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
inst_3 : Fact (Even (Fintype.card n))
inst_4 : LinearOrder R
inst_5 : IsStrictOrderedRing R
g : GL n R
⊢ Eq (α := SignType)
    ((↑(((signDet : PGL(n, R) →* SignTypeˣ) : (a : PGL(n, R)) → SignTypeˣ) ((mk : (a : GL n R) → PGL(n, R)) g)) :
        SignType) :
      SignType)
    ((SignType.sign : (a : R) → SignType) (↑((GeneralLinearGroup.det : (a : GL n R) → Rˣ) g) : R) : SignType)

Tactic:
rfl
-- 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) μ
inl : IsEmpty n → ∃ (k : n), μ ∈ Metric.closedBall (A k k) (∑ j ∈ Finset.erase Finset.univ k, ‖A k j‖)
inr : Nonempty n → ∃ (k : n), μ ∈ Metric.closedBall (A k k) (∑ j ∈ Finset.erase Finset.univ k, ‖A k j‖)
⊢ ∃ (k : n), μ ∈ Metric.closedBall (A k k) (∑ j ∈ Finset.erase Finset.univ k, ‖A k j‖)

Tactic:
cases isEmpty_or_nonempty n

Premises used: isEmpty_or_nonempty
-- 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 : IsEmpty n
inl : False
⊢ ∃ (k : n), μ ∈ Metric.closedBall (A k k) (∑ j ∈ Finset.erase Finset.univ k, ‖A k j‖)

Tactic:
exfalso
-- 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 : IsEmpty n
⊢ False

Tactic:
hμ Submodule.eq_bot_of_subsingleton

Premises used: Submodule.eq_bot_of_subsingleton
-- 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 : IsEmpty n
⊢ False

Tactic:
exact hμ Submodule.eq_bot_of_subsingleton

Premises used: Submodule.eq_bot_of_subsingleton
-- 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
inr :
  ∀ (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 : v ≠ 0), ∃ (k : n), μ ∈ Metric.closedBall (A k k) (∑ j ∈ Finset.erase Finset.univ k, ‖A k j‖)
⊢ ∃ (k : n), μ ∈ Metric.closedBall (A k k) (∑ j ∈ Finset.erase Finset.univ k, ‖A k j‖)

Tactic:
obtain ⟨v, h_eg, h_nz⟩ := hμ.exists_hasEigenvector

Premises used: Module.End.HasEigenvalue.exists_hasEigenvector
-- 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 : v ≠ 0
inr :
  ∀ (i : n) (h_i : (Finset.sup' Finset.univ ⋯ fun (i : n) ↦ ‖v i‖) = ‖v i‖),
    ∃ (k : n), μ ∈ Metric.closedBall (A k k) (∑ j ∈ Finset.erase Finset.univ k, ‖A k j‖)
⊢ ∃ (k : n), μ ∈ Metric.closedBall (A k k) (∑ j ∈ Finset.erase Finset.univ k, ‖A k j‖)

Tactic:
obtain ⟨i, -, h_i⟩ := Finset.exists_mem_eq_sup' Finset.univ_nonempty (fun i => ‖v i‖)

Premises used: Norm.norm, Finset.univ_nonempty, Finset.exists_mem_eq_sup'
-- 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 : v ≠ 0
i : n
h_i : (Finset.sup' Finset.univ ⋯ fun (i : n) ↦ ‖v i‖) = ‖v i‖
contrapose : ∀ (h_nz : v i = 0), v = 0
⊢ v i ≠ 0

Tactic:
contrapose h_nz
-- 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_1 : 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
i : n
h_i : (Finset.sup' Finset.univ ⋯ fun (i : n) ↦ ‖v i‖) = ‖v i‖
h_nz : v i = 0
h : ∀ (j : n), v j = 0 j
⊢ v = 0

Tactic:
ext j
-- 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_1 : 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
i : n
h_i : (Finset.sup' Finset.univ ⋯ fun (i : n) ↦ ‖v i‖) = ‖v i‖
h_nz : v i = 0
j : n
h : ‖v j‖ ≤ 0
⊢ v j = 0 j

Tactic:
rw [Pi.zero_apply, ← norm_le_zero_iff]

Premises used: Pi.zero_apply, norm_le_zero_iff
-- 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_1 : 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
i : n
h_i : (Finset.sup' Finset.univ ⋯ fun (i : n) ↦ ‖v i‖) = ‖v i‖
h_nz : v i = 0
j : n
h : ‖v i‖ ≤ 0
⊢ ‖v j‖ ≤ 0

Tactic:
refine (h_i ▸ Finset.le_sup' (fun i => ‖v i‖) (Finset.mem_univ j)).trans ?_
-- 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
i : n
h_i : (Finset.sup' Finset.univ ⋯ fun (i : n) ↦ ‖v i‖) = ‖v i‖
h_nz : v i = 0
j : n
⊢ ‖v i‖ ≤ 0

Tactic:
norm_le_zero_iff.mpr h_nz

Premises used: Iff.mpr, norm_le_zero_iff
-- 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
i : n
h_i : (Finset.sup' Finset.univ ⋯ fun (i : n) ↦ ‖v i‖) = ‖v i‖
h_nz : v i = 0
j : n
⊢ ‖v i‖ ≤ 0

Tactic:
exact norm_le_zero_iff.mpr h_nz

Premises used: Iff.mpr, norm_le_zero_iff
-- 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 : v ≠ 0
i : n
h_i : (Finset.sup' Finset.univ ⋯ fun (i : n) ↦ ‖v i‖) = ‖v i‖
⊢ v i ≠ 0

Tactic:
have h_nz : v i ≠ 0 := by
      contrapose h_nz
      ext j
      rw [Pi.zero_apply, ← norm_le_zero_iff]
      refine (h_i ▸ Finset.le_sup' (fun i => ‖v i‖) (Finset.mem_univ j)).trans ?_
      exact norm_le_zero_iff.mpr h_nz
-- 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
j : n
rw : ‖v j‖ ≤ ‖v i‖
⊢ ‖v j * (v i)⁻¹‖ ≤ 1

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

Premises used: Iff.mpr, norm_pos_iff, mul_inv_le_iff₀, norm_mul, norm_inv, one_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
j : n
⊢ ‖v j‖ ≤ ‖v i‖

Tactic:
h_i ▸ Finset.le_sup' (fun i => ‖v i‖) (Finset.mem_univ j)

Premises used: Finset.mem_univ, Norm.norm, Eq.rec, Finset.le_sup'
-- 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
j : n
⊢ ‖v j‖ ≤ ‖v i‖

Tactic:
exact h_i ▸ Finset.le_sup' (fun i => ‖v i‖) (Finset.mem_univ j)
-- 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
⊢ ∀ (j : n), ‖v j * (v i)⁻¹‖ ≤ 1

Tactic:
have h_le : ∀ j, ‖v j * (v i)⁻¹‖ ≤ 1 := fun j => by
      rw [norm_mul, norm_inv, mul_inv_le_iff₀ (norm_pos_iff.mpr h_nz), one_mul]
      exact h_i ▸ Finset.le_sup' (fun i => ‖v i‖) (Finset.mem_univ j)
-- 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 : ∃ (k : n), ‖A k k - μ‖ ≤ ∑ j ∈ Finset.erase Finset.univ k, ‖A k j‖
⊢ ∃ (k : n), μ ∈ Metric.closedBall (A k k) (∑ j ∈ Finset.erase Finset.univ k, ‖A k j‖)

Tactic:
simp_rw [mem_closedBall_iff_norm']

Premises used: 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
μ : 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‖

Tactic:
⟨i, ?_⟩

Premises used: Exists.intro