mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
⊢ ⨆ i, ⨆ (h : ↑i ≤ ⊤), (f.genEigenspace μ) ↑↑⟨i, h⟩ = ⨆ k, (f.genEigenspace μ) ↑k

Tactic:
]

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
⊢ ⨆ i, ⨆ (h : ↑i ≤ ⊤), (f.genEigenspace μ) ↑↑⟨i, h⟩ = ⨆ k, (f.genEigenspace μ) ↑k
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Finite I
e : I → R
he : OrthogonalIdempotents e
i j : I
hij : i ≠ j
⊢ IsCoprime (1 - e i) (1 - e j)

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Finite I
e : I → R
he : OrthogonalIdempotents e
i j : I
hij : i ≠ j
⊢ IsCoprime (1 - e i) (1 - e j)
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
⊢ LinearMap.ker (f - μ • 1) = (f - μ • 1).ker

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
x : M
⊢ f x = μ • x ↔ f x = μ • x

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
x : M
⊢ x = 0 ↔ x = 0

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : OrthogonalIdempotents e
he' : ∑ i, e i = 1
__spread✝⁻⁰ : OrthogonalIdempotents e := he
⊢ ∑ i, e i = 1

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : OrthogonalIdempotents e
he' : ∑ i, e i = 1
__spread✝⁻⁰ : OrthogonalIdempotents e := he
⊢ ∑ i, e i = 1
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
⊢ ∀ (a : R), (RingHom.pi fun i ↦ Ideal.Quotient.mk (Ideal.span {1 - e i})) a = 0 → a = 0

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
⊢ ∀ (a : R), (RingHom.pi fun i ↦ Ideal.Quotient.mk (Ideal.span {1 - e i})) a = 0 → a = 0
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ∞
x : M
h : f.HasUnifEigenvector μ k x
⊢ ∃ x ∈ (f.genEigenspace μ) k, x ≠ 0

Tactic:
]

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ∞
x : M
h : f.HasUnifEigenvector μ k x
⊢ ∃ x ∈ (f.genEigenspace μ) k, x ≠ 0
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
x : R
hx : ∀ (x_1 : I), 1 - e x_1 ∣ x
this : ∀ (s : Finset I), (∏ i ∈ s, (1 - e i)) * x = x
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
h : f.HasUnifEigenvalue μ 1
n : ℕ
⊢ ∃ x ∈ ((f ^ n).genEigenspace (μ ^ n)) 1, x ≠ 0

Tactic:
]

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
h : f.HasUnifEigenvalue μ 1
n : ℕ
⊢ ∃ x ∈ ((f ^ n).genEigenspace (μ ^ n)) 1, x ≠ 0
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: case mpr
R : Type u_1
n : Type u_2
inst✝³ : NonUnitalNonAssocSemiring R
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : Nonempty n
c : RingCon R
x y : R
h : c x y
i j : n
⊢ c x y

Tactic:
]

Goal state after:
case mpr
R : Type u_1
n : Type u_2
inst✝³ : NonUnitalNonAssocSemiring R
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : Nonempty n
c : RingCon R
x y : R
h : c x y
i j : n
⊢ c x y
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: case mp
R : Type u_1
n : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon (Matrix n n R)
x y : Matrix n n R
h : (matrix n c.ofMatrix) x y
⊢ c (∑ i, ∑ j, single i j (x i j)) (∑ i, ∑ j, single i j (y i j))

Tactic:
]

Goal state after:
case mp
R : Type u_1
n : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon (Matrix n n R)
x y : Matrix n n R
h : (matrix n c.ofMatrix) x y
⊢ c (∑ i, ∑ j, single i j (x i j)) (∑ i, ∑ j, single i j (y i j))
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
s✝ : Finset I
a : I
s : Finset I
has : a ∉ s
c : R
hx : ∀ (x : I), 1 - e x ∣ (1 - e a) * c
e' : (∏ i ∈ s, (1 - e i)) * ((1 - e a) * c) = (1 - e a) * c
⊢ (1 - e a) * c = (1 - e a) * c

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
hμ : f.HasUnifEigenvalue μ 1
h_unit : IsUnit ((algebraMap R (End R M)) μ - f)
f' : M ≃ₗ[R] M := LinearMap.GeneralLinearGroup.toLinearEquiv h_unit.unit
v : M
hv : f.HasUnifEigenvector μ 1 v
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
⊢ (f - μ • 1).ker = ⊥ ↔ LinearMap.ker (f - (algebraMap K (End K V)) μ) = ⊥

Tactic:
]

Goal state after:
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
⊢ (f - μ • 1).ker = ⊥ ↔ LinearMap.ker (f - (algebraMap K (End K V)) μ) = ⊥
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : Fin 2 → R :=
  fun i ↦
    match i with
    | 0 => e
    | 1 => f
⊢ Function.Bijective ⇑(RingHom.pi fun i ↦ Ideal.Quotient.mk (Ideal.span {o i}))

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : Fin 2 → R :=
  fun i ↦
    match i with
    | 0 => e
    | 1 => f
⊢ Function.Bijective ⇑(RingHom.pi fun i ↦ Ideal.Quotient.mk (Ideal.span {o i}))
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
a b : K
hb : b ≠ 0
⊢ (f.genEigenspace (b⁻¹ * a)) 1 = (f.genEigenspace (b⁻¹ * a)) 1

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
a b : K
hb : b ≠ 0
⊢ (f - (b⁻¹ * a) • 1).ker = (f - (b⁻¹ * a) • 1).ker

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
a b : K
hb : b ≠ 0
⊢ (f - b⁻¹ • a • 1).ker = LinearMap.ker (f - b⁻¹ • a • 1)

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
a b : K
hb : b ≠ 0
⊢ LinearMap.ker (b • f - a • 1) = (b • f - a • 1).ker

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: case mpr
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
x : M
i : ℕ
hi : i ≤ k
this : k = i + (k - i)
⊢ ∃ y, ((f - μ • 1) ^ i) y = ((f - μ • 1) ^ i * (f - μ • 1) ^ (k - i)) x

Tactic:
]

Goal state after:
case mpr
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
x : M
i : ℕ
hi : i ≤ k
this : k = i + (k - i)
⊢ ∃ y, ((f - μ • 1) ^ i) y = ((f - μ • 1) ^ i * (f - μ • 1) ^ (k - i)) x
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: case mpr
R : Type u_1
n✝ : Type u_2
inst✝³ : NonAssocRing R
inst✝² : Fintype n✝
inst✝¹ : Nonempty n✝
inst✝ : DecidableEq n✝
I : TwoSidedIdeal (Matrix n✝ n✝ R)
i j : n✝
n : Matrix n✝ n✝ R
hn : n ∈ I
⊢ Relation.Map (⇑I.ringCon) (fun x ↦ x i j) (fun x ↦ x i j) (n i j) 0

Tactic:
]

Goal state after:
case mpr
R : Type u_1
n✝ : Type u_2
inst✝³ : NonAssocRing R
inst✝² : Fintype n✝
inst✝¹ : Nonempty n✝
inst✝ : DecidableEq n✝
I : TwoSidedIdeal (Matrix n✝ n✝ R)
i j : n✝
n : Matrix n✝ n✝ R
hn : n ∈ I
⊢ Relation.Map (⇑I.ringCon) (fun x ↦ x i j) (fun x ↦ x i j) (n i j) 0
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: case e'_2
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : End R M
μ : R
this :
  iSup ⇑((f.genEigenspace μ).comp WithTop.coeOrderHom.toOrderHom) =
    monotonicSequenceLimit ((f.genEigenspace μ).comp WithTop.coeOrderHom.toOrderHom)
⊢ sSup (range fun l ↦ ((f - μ • 1) ^ l).ker) = sSup (range fun x ↦ ((f - μ • 1) ^ (↑x).2).ker)

Tactic:
]

Goal state after:
case e'_2
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : End R M
μ : R
this :
  iSup ⇑((f.genEigenspace μ).comp WithTop.coeOrderHom.toOrderHom) =
    monotonicSequenceLimit ((f.genEigenspace μ).comp WithTop.coeOrderHom.toOrderHom)
⊢ sSup (range fun l ↦ ((f - μ • 1) ^ l).ker) = sSup (range fun x ↦ ((f - μ • 1) ^ (↑x).2).ker)
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : TwoSidedIdeal R
M : Matrix n n R
Mmem : M ∈ (matrix n I).jacobson
p q : n
⊢ ∀ (y : R), ∃ z, z * y * M p q + z - 1 ∈ I

Tactic:
]

Goal state after:
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : TwoSidedIdeal R
M : Matrix n n R
Mmem : M ∈ (matrix n I).jacobson
p q : n
⊢ ∀ (y : R), ∃ z, z * y * M p q + z - 1 ∈ I
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : TwoSidedIdeal R
M : Matrix n n R
p q : n
Mmem : ∀ (y : Matrix n n R), ∃ z, z * y * (M * single q p 1) + z - 1 ∈ matrix n I
⊢ ∀ (y : R), ∃ z, z * y * M p q + z - 1 ∈ I

Tactic:
]

Goal state after:
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : TwoSidedIdeal R
M : Matrix n n R
p q : n
Mmem : ∀ (y : Matrix n n R), ∃ z, z * y * (M * single q p 1) + z - 1 ∈ matrix n I
⊢ ∀ (y : R), ∃ z, z * y * M p q + z - 1 ∈ I
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : End R M
μ : R
k : ℕ∞
⊢ (f.genEigenspace μ) k ≤ (f.genEigenspace μ) ⊤

Tactic:
]

Goal state after:
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : End R M
μ : R
k : ℕ∞
⊢ (f.genEigenspace μ) k ≤ (f.genEigenspace μ) ⊤
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k m : ℕ∞
hm : k ≤ m
hk : (f.genEigenspace μ) m = ⊥
⊢ (f.genEigenspace μ) k ≤ (f.genEigenspace μ) m

Tactic:
]

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k m : ℕ∞
hm : k ≤ m
hk : (f.genEigenspace μ) m = ⊥
⊢ (f.genEigenspace μ) k ≤ (f.genEigenspace μ) m
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k m : ℕ∞
hm : 0 < m
hk : f.HasUnifEigenvalue μ k
contra : Function.Injective ⇑(f - μ • 1)
⊢ (f.genEigenspace μ) k = ⊥

Tactic:
]

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k m : ℕ∞
hm : 0 < m
hk : f.HasUnifEigenvalue μ k
contra : Function.Injective ⇑(f - μ • 1)
⊢ (f.genEigenspace μ) k = ⊥
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k m : ℕ∞
hm : 0 < m
hk : f.HasUnifEigenvalue μ k
contra : Function.Injective ⇑(f - μ • 1)
⊢ (f.genEigenspace μ) k ≤ ⊥

Tactic:
]

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k m : ℕ∞
hm : 0 < m
hk : f.HasUnifEigenvalue μ k
contra : Function.Injective ⇑(f - μ • 1)
⊢ (f.genEigenspace μ) k ≤ ⊥
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k m : ℕ∞
hm : 0 < m
hk : f.HasUnifEigenvalue μ k
contra : Function.Injective ⇑(f - μ • 1)
x : M
hx : ∃ l, ↑l ≤ k ∧ x ∈ ((f - μ • 1) ^ l).ker
⊢ x ∈ ⊥

Tactic:
]

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k m : ℕ∞
hm : 0 < m
hk : f.HasUnifEigenvalue μ k
contra : Function.Injective ⇑(f - μ • 1)
x : M
hx : ∃ l, ↑l ≤ k ∧ x ∈ ((f - μ • 1) ^ l).ker
⊢ x ∈ ⊥
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k m : ℕ∞
hm : 0 < m
hk : f.HasUnifEigenvalue μ k
contra : Function.Injective ⇑(f - μ • 1)
x : M
l : ℕ
hx : x ∈ ⊥
⊢ x ∈ ⊥

pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k m : ℕ∞
hm : 0 < m
hk : f.HasUnifEigenvalue μ k
contra : Function.Injective ⇑(f - μ • 1)
x : M
l : ℕ
hx : x ∈ ((f - μ • 1) ^ l).ker
⊢ Function.Injective ⇑((f - μ • 1) ^ l)

Tactic:
]

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k m : ℕ∞
hm : 0 < m
hk : f.HasUnifEigenvalue μ k
contra : Function.Injective ⇑(f - μ • 1)
x : M
l : ℕ
hx : x ∈ ⊥
⊢ x ∈ ⊥

R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k m : ℕ∞
hm : 0 < m
hk : f.HasUnifEigenvalue μ k
contra : Function.Injective ⇑(f - μ • 1)
x : M
l : ℕ
hx : x ∈ ((f - μ • 1) ^ l).ker
⊢ Function.Injective ⇑((f - μ • 1) ^ l)
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k m : ℕ∞
hm : 0 < m
hk : f.HasUnifEigenvalue μ k
contra : Function.Injective ⇑(f - μ • 1)
x : M
l : ℕ
hx : x ∈ ((f - μ • 1) ^ l).ker
⊢ Function.Injective (⇑(f - μ • 1))^[l]

Tactic:
]

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k m : ℕ∞
hm : 0 < m
hk : f.HasUnifEigenvalue μ k
contra : Function.Injective ⇑(f - μ • 1)
x : M
l : ℕ
hx : x ∈ ((f - μ • 1) ^ l).ker
⊢ Function.Injective (⇑(f - μ • 1))^[l]
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: case a
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
n : ℕ
hn : finrank K V ≤ n
⊢ ((f - μ • 1) ^ n).ker ≤ ((f - μ • 1) ^ finrank K V).ker

Tactic:
]

Goal state after:
case a
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
n : ℕ
hn : finrank K V ≤ n
⊢ ((f - μ • 1) ^ n).ker ≤ ((f - μ • 1) ^ finrank K V).ker
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
k : ℕ∞
⊢ (f.genEigenspace μ) ↑(f.maxUnifEigenspaceIndex μ) ≤ (f.genEigenspace μ) ↑(finrank K V)

Tactic:
]

Goal state after:
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
k : ℕ∞
⊢ (f.genEigenspace μ) ↑(f.maxUnifEigenspaceIndex μ) ≤ (f.genEigenspace μ) ↑(finrank K V)
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
k : ℕ∞
⊢ ↑(f.maxUnifEigenspaceIndex μ) ≤ ↑(finrank K V)

Tactic:
simpa using maxUnifEigenspaceIndex_le_finrank f μ

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: case right
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f g : End R M
μ : R
k : ℕ∞
x : M
l : ℕ
hl : ↑l ≤ k
hx : ((f - μ • 1) ^ l) x = 0
h : Commute ((f - μ • 1) ^ l) g
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: case h
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
h : MapsTo ⇑(f - μ • 1) ↑((f.genEigenspace μ) ↑k) ↑((f.genEigenspace μ) ↑k)
x : M
hx✝ : x ∈ (f.genEigenspace μ) ↑k
hx : x ∈ ((f - μ • 1) ^ k).ker
⊢ ↑((LinearMap.restrict (f - μ • 1) h ^ k) ⟨x, hx✝⟩) = ↑(0 ⟨x, hx✝⟩)

Tactic:
]

Goal state after:
case h
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
h : MapsTo ⇑(f - μ • 1) ↑((f.genEigenspace μ) ↑k) ↑((f.genEigenspace μ) ↑k)
x : M
hx✝ : x ∈ (f.genEigenspace μ) ↑k
hx : x ∈ ((f - μ • 1) ^ k).ker
⊢ ↑((LinearMap.restrict (f - μ • 1) h ^ k) ⟨x, hx✝⟩) = ↑(0 ⟨x, hx✝⟩)
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: case h
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
h : MapsTo ⇑(f - μ • 1) ↑((f.genEigenspace μ) ↑k) ↑((f.genEigenspace μ) ↑k)
x : M
hx✝ : x ∈ (f.genEigenspace μ) ↑k
hx : x ∈ ((f - μ • 1) ^ k).ker
⊢ ⟨((f - μ • 1) ^ k) ↑⟨x, hx✝⟩, ⋯⟩ = 0

Tactic:
]

Goal state after:
case h
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
h : MapsTo ⇑(f - μ • 1) ↑((f.genEigenspace μ) ↑k) ↑((f.genEigenspace μ) ↑k)
x : M
hx✝ : x ∈ (f.genEigenspace μ) ↑k
hx : x ∈ ((f - μ • 1) ^ k).ker
⊢ ⟨((f - μ • 1) ^ k) ↑⟨x, hx✝⟩, ⋯⟩ = 0
Module: Mathlib.Algebra.DirectSum.LinearMap

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : ι → Submodule R M
inst✝² : DecidableEq ι
inst✝¹ : ∀ (i : ι), Module.Finite R ↥(N i)
inst✝ : ∀ (i : ι), Free R ↥(N i)
h : IsInternal N
hN : {i | N i ≠ ⊥}.Finite
f : M →ₗ[R] M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N i)
x✝¹ : Fintype { i // N i ≠ ⊥ } := hN.fintype
x✝ : Fintype ↑{i | N i ≠ ⊥} := hN.fintype
⊢ ∑ i, (trace R ↥(N ↑i)) (f.restrict ⋯) = ∑ i, (trace R ↥(N ↑i)) (f.restrict ⋯)

Tactic:
]

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : ι → Submodule R M
inst✝² : DecidableEq ι
inst✝¹ : ∀ (i : ι), Module.Finite R ↥(N i)
inst✝ : ∀ (i : ι), Free R ↥(N i)
h : IsInternal N
hN : {i | N i ≠ ⊥}.Finite
f : M →ₗ[R] M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N i)
x✝¹ : Fintype { i // N i ≠ ⊥ } := hN.fintype
x✝ : Fintype ↑{i | N i ≠ ⊥} := hN.fintype
⊢ ∑ i, (trace R ↥(N ↑i)) (f.restrict ⋯) = ∑ i, (trace R ↥(N ↑i)) (f.restrict ⋯)
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case refine_1.some.some
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
I : Type u_3
inst✝ : Fintype I
f : R →+* S
e₀ : R
he₀ : IsIdempotentElem e₀
hfe₀ : RingHom.ker f = Ideal.span {e₀}
e : I → S
he : CompleteOrthogonalIdempotents e
e' : I → R
he' : ∀ (i : I), f (e' i) = e i
k✝ : I → R
hk✝ : ∀ (i : I), e' i * e' i - e' i = e₀ * k✝ i
i j : I
h : some i ≠ some j
k : R
hk : e' i * e' j = e₀ * k
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: case h
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : End R M
μ : R
h : MapsTo ⇑(f - μ • 1) ↑((f.genEigenspace μ) ⊤) ↑((f.genEigenspace μ) ⊤)
⊢ (f.genEigenspace μ) ↑(f.maxUnifEigenspaceIndex μ) ≤ (f.genEigenspace μ) ↑(f.maxUnifEigenspaceIndex μ)

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
⊢ (f - μ • 1).ker = (f - μ • 1).ker

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
n : ℕ∞
k : ℕ
ih : ∀ ⦃x : M⦄, ↑k ≤ n → ((f - μ • 1) ^ k) x = 0 → ((f - μ • 1) ^ k) (f x) = 0
x : M
hk : ↑(k + 1) ≤ n
hx : ((f - μ • 1) ^ k) ((f - μ • 1) x) = 0
⊢ ((f - μ • 1) ^ k) ((f - μ • 1) (f x)) = 0

Tactic:
]

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
n : ℕ∞
k : ℕ
ih : ∀ ⦃x : M⦄, ↑k ≤ n → ((f - μ • 1) ^ k) x = 0 → ((f - μ • 1) ^ k) (f x) = 0
x : M
hk : ↑(k + 1) ≤ n
hx : ((f - μ • 1) ^ k) ((f - μ • 1) x) = 0
⊢ ((f - μ • 1) ^ k) ((f - μ • 1) (f x)) = 0
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
e : R
inst✝ : Semigroup R
idem : IsIdempotentElem e
hc : IsMulCentral e
r : R
⊢ e * r = r ↔ e * r = r

pp: R : Type u_1
e : R
inst✝ : Semigroup R
idem : IsIdempotentElem e
hc : IsMulCentral e
r : R
⊢ e * r = r → r * e = r

Tactic:
]

Goal state after:
R : Type u_1
e : R
inst✝ : Semigroup R
idem : IsIdempotentElem e
hc : IsMulCentral e
r : R
⊢ e * r = r → r * e = r
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
e : R
inst✝ : Semigroup R
idem : IsIdempotentElem e
hc : IsMulCentral e
r : R
a✝ : e * r = r
⊢ e * r = r

Tactic:
]

Goal state after:
R : Type u_1
e : R
inst✝ : Semigroup R
idem : IsIdempotentElem e
hc : IsMulCentral e
r : R
a✝ : e * r = r
⊢ e * r = r
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
e : R
inst✝ : Semigroup R
idem : IsIdempotentElem e
hc : IsMulCentral e
r : R
⊢ r * e = r ↔ r * e = r

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
⊢ (f.genEigenspace μ) ↑(f.maxUnifEigenspaceIndex μ) ≤ (f.genEigenspace μ) ↑(finrank K V)

Tactic:
]

Goal state after:
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
⊢ (f.genEigenspace μ) ↑(f.maxUnifEigenspaceIndex μ) ≤ (f.genEigenspace μ) ↑(finrank K V)
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : End R M
μ : R
h : MapsTo ⇑(f - (algebraMap R (End R M)) μ) ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
⊢ (f.genEigenspace μ) ↑(f.maxGenEigenspaceIndex μ) ≤ (f.genEigenspace μ) ↑(f.maxUnifEigenspaceIndex μ)

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k l : ℕ∞
⊢ Disjoint (⨆ l, (f.genEigenspace μ₁) ↑↑l) (⨆ l_1, (f.genEigenspace μ₂) ↑↑l_1)

Tactic:
]

Goal state after:
R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k l : ℕ∞
⊢ Disjoint (⨆ l, (f.genEigenspace μ₁) ↑↑l) (⨆ l_1, (f.genEigenspace μ₂) ↑↑l_1)