awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
g : GL (Fin 2) K
h_det :
  Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (1 : Kˣ) ∨
    Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (-1 : Kˣ)
hg10 : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
hg00 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 0 = (↑g : Matrix (Fin 2) (Fin 2) K) 1 1
hg01 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 ≠ 0
this : HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2 = 1
⊢ (∃ (x : K), x ≠ 0 ∧ g = (upperRightHom : (a : K) → GL (Fin 2) K) x) ∨
    ∃ (x : K), x ≠ 0 ∧ g = -(upperRightHom : (a : K) → GL (Fin 2) K) x
have mp : (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 = 1 → ∃ (x : K), x ≠ 0 ∧ g = (upperRightHom : (a : K) → GL (Fin 2) K) x
Tactic: apply (sq_eq_one_iff.mp this).imp
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
g : GL (Fin 2) K
h_det :
  Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (1 : Kˣ) ∨
    Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (-1 : Kˣ)
hg10 : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
hg00 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 0 = (↑g : Matrix (Fin 2) (Fin 2) K) 1 1
hg01 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 ≠ 0
this : HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2 = 1
mp : (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 = 1 → ∃ (x : K), x ≠ 0 ∧ g = (upperRightHom : (a : K) → GL (Fin 2) K) x
⊢ (∃ (x : K), x ≠ 0 ∧ g = (upperRightHom : (a : K) → GL (Fin 2) K) x) ∨
    ∃ (x : K), x ≠ 0 ∧ g = -(upperRightHom : (a : K) → GL (Fin 2) K) x
have mp₁ : (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 = -1 → ∃ (x : K), x ≠ 0 ∧ g = -(upperRightHom : (a : K) → GL (Fin 2) K) x
Tactic: apply (sq_eq_one_iff.mp this).imp
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
g : GL (Fin 2) K
h_det :
  Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (1 : Kˣ) ∨
    Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (-1 : Kˣ)
hg10 : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
hg00 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 0 = (↑g : Matrix (Fin 2) (Fin 2) K) 1 1
hg01 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 ≠ 0
this : HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2 = 1
hg11 : (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 = 1
⊢ ∃ (x : K), x ≠ 0 ∧ g = (upperRightHom : (a : K) → GL (Fin 2) K) x
have mp : ∃ (x : K),
  x ≠ 0 ∧ (↑g : Matrix (Fin 2) (Fin 2) K) = (↑((upperRightHom : (a : K) → GL (Fin 2) K) x) : Matrix (Fin 2) (Fin 2) K)
Tactic: simp only [Units.ext_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
g : GL (Fin 2) K
h_det :
  Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (1 : Kˣ) ∨
    Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (-1 : Kˣ)
hg10 : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
hg00 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 0 = (↑g : Matrix (Fin 2) (Fin 2) K) 1 1
hg01 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 ≠ 0
this : HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2 = 1
hg11 : (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 = -1
⊢ ∃ (x : K), x ≠ 0 ∧ g = -(upperRightHom : (a : K) → GL (Fin 2) K) x
have mp : ∃ (x : K),
  x ≠ 0 ∧ (↑g : Matrix (Fin 2) (Fin 2) K) = (↑(-(upperRightHom : (a : K) → GL (Fin 2) K) x) : Matrix (Fin 2) (Fin 2) K)
Tactic: simp only [Units.ext_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
g : GL (Fin 2) K
h_det :
  Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (1 : Kˣ) ∨
    Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (-1 : Kˣ)
hg10 : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
hg00 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 0 = (↑g : Matrix (Fin 2) (Fin 2) K) 1 1
hg01 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 ≠ 0
this : HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2 = 1
hg11 : (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 = 1
⊢ ∃ (x : K),
    x ≠ 0 ∧ (↑g : Matrix (Fin 2) (Fin 2) K) = (↑((upperRightHom : (a : K) → GL (Fin 2) K) x) : Matrix (Fin 2) (Fin 2) K)
have mp : (↑g : Matrix (Fin 2) (Fin 2) K) =
  (↑((upperRightHom : (a : K) → GL (Fin 2) K) ((↑g : Matrix (Fin 2) (Fin 2) K) 0 1)) : Matrix (Fin 2) (Fin 2) K)
Tactic: refine ⟨g 0 1, hg01, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
g : GL (Fin 2) K
h_det :
  Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (1 : Kˣ) ∨
    Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (-1 : Kˣ)
hg10 : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
hg00 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 0 = (↑g : Matrix (Fin 2) (Fin 2) K) 1 1
hg01 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 ≠ 0
this : HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2 = 1
hg11 : (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 = 1
⊢ (↑g : Matrix (Fin 2) (Fin 2) K) =
    (↑((upperRightHom : (a : K) → GL (Fin 2) K) ((↑g : Matrix (Fin 2) (Fin 2) K) 0 1)) : Matrix (Fin 2) (Fin 2) K)
have mp : Eq (α := Matrix (Fin 2) (Fin 2) K)
  (!![(↑g : Matrix (Fin 2) (Fin 2) K) 0 0, (↑g : Matrix (Fin 2) (Fin 2) K) 0 1;
      (↑g : Matrix (Fin 2) (Fin 2) K) 1 0, (↑g : Matrix (Fin 2) (Fin 2) K) 1 1] :
    Matrix (Fin 2) (Fin 2) K)
  ((↑((upperRightHom : (a : K) → GL (Fin 2) K)
          (!![(↑g : Matrix (Fin 2) (Fin 2) K) 0 0, (↑g : Matrix (Fin 2) (Fin 2) K) 0 1;
              (↑g : Matrix (Fin 2) (Fin 2) K) 1 0, (↑g : Matrix (Fin 2) (Fin 2) K) 1 1]
            0 1)) :
      Matrix (Fin 2) (Fin 2) K) :
    Matrix (Fin 2) (Fin 2) K)
Tactic: rw [g.val.eta_fin_two]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
g : GL (Fin 2) K
h_det :
  Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (1 : Kˣ) ∨
    Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (-1 : Kˣ)
hg10 : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
hg00 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 0 = (↑g : Matrix (Fin 2) (Fin 2) K) 1 1
hg01 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 ≠ 0
this : HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2 = 1
hg11 : (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 = -1
⊢ ∃ (x : K),
    x ≠ 0 ∧
      (↑g : Matrix (Fin 2) (Fin 2) K) = (↑(-(upperRightHom : (a : K) → GL (Fin 2) K) x) : Matrix (Fin 2) (Fin 2) K)
have mp : (↑g : Matrix (Fin 2) (Fin 2) K) =
  (↑(-(upperRightHom : (a : K) → GL (Fin 2) K) (-(↑g : Matrix (Fin 2) (Fin 2) K) 0 1)) : Matrix (Fin 2) (Fin 2) K)
Tactic: refine ⟨-g 0 1, neg_eq_zero.not.mpr hg01, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
g : GL (Fin 2) K
h_det :
  Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (1 : Kˣ) ∨
    Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (-1 : Kˣ)
hg10 : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
hg00 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 0 = (↑g : Matrix (Fin 2) (Fin 2) K) 1 1
hg01 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 ≠ 0
this : HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2 = 1
hg11 : (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 = -1
⊢ (↑g : Matrix (Fin 2) (Fin 2) K) =
    (↑(-(upperRightHom : (a : K) → GL (Fin 2) K) (-(↑g : Matrix (Fin 2) (Fin 2) K) 0 1)) : Matrix (Fin 2) (Fin 2) K)
have mp : Eq (α := Matrix (Fin 2) (Fin 2) K)
  (!![(↑g : Matrix (Fin 2) (Fin 2) K) 0 0, (↑g : Matrix (Fin 2) (Fin 2) K) 0 1;
      (↑g : Matrix (Fin 2) (Fin 2) K) 1 0, (↑g : Matrix (Fin 2) (Fin 2) K) 1 1] :
    Matrix (Fin 2) (Fin 2) K)
  ((↑(-(upperRightHom : (a : K) → GL (Fin 2) K)
            (-!![(↑g : Matrix (Fin 2) (Fin 2) K) 0 0, (↑g : Matrix (Fin 2) (Fin 2) K) 0 1;
                  (↑g : Matrix (Fin 2) (Fin 2) K) 1 0, (↑g : Matrix (Fin 2) (Fin 2) K) 1 1]
                0 1)) :
      Matrix (Fin 2) (Fin 2) K) :
    Matrix (Fin 2) (Fin 2) K)
Tactic: rw [g.val.eta_fin_two]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective (goal)
Goal:
n : Type u_1
R : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
g : GL n R
⊢ Eq (α := PGL(n, R)) ((mk : (a : GL n R) → PGL(n, R)) g : PGL(n, R)) (1 : PGL(n, R)) ↔
    Membership.mem (γ := Subgroup (GL n R)) (Subgroup.center (GL n R)) g
have rw : Membership.mem (γ := Subgroup (GL n R)) (MonoidHom.ker mk) g ↔
  Membership.mem (γ := Subgroup (GL n R)) (Subgroup.center (GL n R)) g
Tactic: rw [← MonoidHom.mem_ker, ker_mk]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective (goal)
Goal:
n : Type u_1
R : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
g : GL n R
rw :
  Membership.mem (γ := Subgroup (GL n R)) (MonoidHom.ker mk) g ↔
    Membership.mem (γ := Subgroup (GL n R)) (Subgroup.center (GL n R)) g
⊢ Eq (α := PGL(n, R)) ((mk : (a : GL n R) → PGL(n, R)) g : PGL(n, R)) (1 : PGL(n, R)) ↔
    Membership.mem (γ := Subgroup (GL n R)) (Subgroup.center (GL n R)) g
have rw₁ : Membership.mem (γ := Subgroup (GL n R)) (Subgroup.center (GL n R)) g ↔
  Membership.mem (γ := Subgroup (GL n R)) (Subgroup.center (GL n R)) g
Tactic: rw [← MonoidHom.mem_ker, ker_mk]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective (goal)
Goal:
n : Type u_1
R : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
u : 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))
have 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)
Tactic: rw [← MonoidHom.mem_ker, ker_mk, GeneralLinearGroup.center_eq_range_scalar]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective (goal)
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
⊢ Subgroup.center (GL n R) ≤ f.ker
have rwa : MonoidHom.range (GeneralLinearGroup.scalar n) ≤ f.ker
Tactic: rwa [GeneralLinearGroup.center_eq_range_scalar, MonoidHom.range_le_ker_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective (goal)
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
⊢ Eq (α := MonoidHom.{u_2, u_4} Rˣ (Function.End α))
    (MonoidHom.comp (N := GL n R) MulAction.toEndHom (GeneralLinearGroup.scalar n)) 1
have 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 α)
Tactic: ext u
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective (goal)
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ˣ
⊢ 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 α)
have 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 : α)
Tactic: funext a
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective (goal)
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
⊢ 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
have 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)
Tactic: ext u
-- 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) μ
⊢ ∃ (k : n), μ ∈ Metric.closedBall (A k k) (∑ j ∈ Finset.erase Finset.univ k, ‖A k j‖)
have inl : IsEmpty n → ∃ (k : n), μ ∈ Metric.closedBall (A k k) (∑ j ∈ Finset.erase Finset.univ k, ‖A k j‖)
Tactic: cases isEmpty_or_nonempty n
-- 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) μ
inl : IsEmpty 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‖)
have inr : Nonempty n → ∃ (k : n), μ ∈ Metric.closedBall (A k k) (∑ j ∈ Finset.erase Finset.univ k, ‖A k j‖)
Tactic: cases isEmpty_or_nonempty n
-- 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 : IsEmpty n
⊢ ∃ (k : n), μ ∈ Metric.closedBall (A k k) (∑ j ∈ Finset.erase Finset.univ k, ‖A k j‖)
have inl : False
Tactic: exfalso
-- 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
⊢ ∃ (k : n), μ ∈ Metric.closedBall (A k k) (∑ j ∈ Finset.erase Finset.univ k, ‖A k j‖)
have 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‖)
Tactic: obtain ⟨v, h_eg, h_nz⟩ := hμ.exists_hasEigenvector
-- 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 : v ≠ 0
⊢ ∃ (k : n), μ ∈ Metric.closedBall (A k k) (∑ j ∈ Finset.erase Finset.univ k, ‖A k j‖)
have inr : ∀ (i : n) (h_i : (Finset.sup' Finset.univ sorry fun (i : n) ↦ ‖v i‖) = ‖v i‖),
  ∃ (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‖)
-- 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 : v ≠ 0
i : n
h_i : (Finset.sup' Finset.univ ⋯ fun (i : n) ↦ ‖v i‖) = ‖v i‖
⊢ v i ≠ 0
have contrapose : ∀ (h_nz : v i = 0), v = 0
Tactic: contrapose h_nz
Cleared hypotheses: h_nz
-- 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
i : n
h_i : (Finset.sup' Finset.univ ⋯ fun (i : n) ↦ ‖v i‖) = ‖v i‖
h_nz : v i = 0
⊢ v = 0
have h : ∀ (j : n), v j = 0 j
Tactic: ext 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
i : n
h_i : (Finset.sup' Finset.univ ⋯ fun (i : n) ↦ ‖v i‖) = ‖v i‖
h_nz : v i = 0
j : n
⊢ v j = 0 j
have h : ‖v j‖ ≤ 0
Tactic: rw [Pi.zero_apply, ← norm_le_zero_iff]
-- 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
i : n
h_i : (Finset.sup' Finset.univ ⋯ fun (i : n) ↦ ‖v i‖) = ‖v i‖
h_nz : v i = 0
j : n
⊢ ‖v j‖ ≤ 0
have h : ‖v i‖ ≤ 0
Tactic: refine (h_i ▸ Finset.le_sup' (fun i => ‖v i‖) (Finset.mem_univ j)).trans ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Gershgorin (hypothesis)
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‖
⊢ ∃ (k : n), μ ∈ Metric.closedBall (A k k) (∑ j ∈ Finset.erase Finset.univ k, ‖A k j‖)
have h_nz₁ : 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
-- 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
j : n
⊢ ‖v j * (v i)⁻¹‖ ≤ 1
have rw : ‖v j‖ ≤ ‖v i‖
Tactic: rw [norm_mul, norm_inv, mul_inv_le_iff₀ (norm_pos_iff.mpr h_nz), one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Gershgorin (hypothesis)
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
⊢ ∃ (k : n), μ ∈ Metric.closedBall (A k k) (∑ j ∈ Finset.erase Finset.univ k, ‖A k j‖)
have h_le : ∀ (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)
-- 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), μ ∈ Metric.closedBall (A k k) (∑ j ∈ Finset.erase Finset.univ k, ‖A k j‖)
have inr : ∃ (k : n), ‖A k k - μ‖ ≤ ∑ j ∈ Finset.erase Finset.univ k, ‖A k j‖
Tactic: simp_rw [mem_closedBall_iff_norm']