mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
I : Type u_3
e : I → R
inst✝ : Fintype I
he : OrthogonalIdempotents e
⊢ (∑ i, e i) * (1 - ∑ i, e i) = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
I : Type u_3
e : I → R
inst✝ : Fintype I
he : OrthogonalIdempotents e
⊢ ∑ i, i.elim (1 - ∑ i, e i) e = 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Congruence.BigOperators

Goal state before:
pp: ι : Type u_1
β : Type u_2
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : Zero β
c : Con M
h h' : ι → β → M
f g : ι →₀ β
hf : ∀ (i : ι), c (h i 0) 1
hf' : ∀ (i : ι), c (h' i 0) 1
H : ∀ (i : ι), c (h i (f i)) (h' i (g i))
⊢ c (f.prod h) (g.prod h')

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Congruence.BigOperators

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
M : Type u_3
inst✝³ : DecidableEq ι
inst✝² : CommMonoid M
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (y : β i) → Decidable (y ≠ 0)
c : Con M
h h' : (i : ι) → β i → M
f g : Π₀ (i : ι), β i
hf : ∀ (i : ι), c (h i 0) 1
hf' : ∀ (i : ι), c (h' i 0) 1
H : ∀ (i : ι), c (h i (f i)) (h' i (g i))
⊢ c (f.prod h) (g.prod h')

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Congruence.BigOperators

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : AddCommMonoid M
inst✝ : (i : ι) → AddCommMonoid (β i)
c : AddCon M
h h' : (i : ι) → β i →+ M
f g : Π₀ (i : ι), β i
H : ∀ (i : ι), c ((h i) (f i)) ((h' i) (g i))
⊢ c ((DFinsupp.sumAddHom h) f) ((DFinsupp.sumAddHom h') g)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Congruence.BigOperators

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : AddCommMonoid M
inst✝ : (i : ι) → AddCommMonoid (β i)
c : AddCon M
h : (i : ι) → β i →+ M
f : Π₀ (i : ι), β i
⊢ ↑((DFinsupp.sumAddHom h) f) = (DFinsupp.sumAddHom fun i ↦ c.mk'.comp (h i)) f

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case inr.inr.succ
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
h✝¹ : Nontrivial R
h✝ : Nontrivial S
n : ℕ
e : Fin (n + 1) → S
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : Fin (n + 1)), e i ∈ f.range
e' : Fin (n + 1) → R
h₁ : OrthogonalIdempotents e'
h₂ : ⇑f ∘ e' = e
i : Fin (n + 1)
this : ∀ (i : Fin (n + 1)), f (e' i) = e i
⊢ (⇑f ∘ (fun x ↦ x.elim (1 - ∑ i, (e' ∘ ⇑(Fin.succEmb n)) i) (e' ∘ ⇑(Fin.succEmb n))) ∘ ⇑(finSuccEquiv n)) i = e i

Tactic:
cases i using Fin.cases with
  | zero => simp [this, Fin.sum_univ_succ, ← he.complete]
  | succ i => simp [this]

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
n : ℕ
e : Fin n → S
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : Fin n), e i ∈ f.range
⊢ ∃ e', CompleteOrthogonalIdempotents e' ∧ ⇑f ∘ e' = e

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : Ring S
f : R →+* S
I : Type u_3
inst✝ : Fintype I
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e : I → S
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : I), e i ∈ f.range
e' : Fin (Fintype.card I) → R
h₁ : CompleteOrthogonalIdempotents e'
h₂ : ⇑f ∘ e' = e ∘ ⇑(Fintype.equivFin I).symm
⊢ ⇑f ∘ e' ∘ ⇑(Fintype.equivFin I) = e

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : Ring S
f : R →+* S
I : Type u_3
inst✝ : Fintype I
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e : I → S
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : I), e i ∈ f.range
⊢ ∃ e', CompleteOrthogonalIdempotents e' ∧ ⇑f ∘ e' = e

Tactic:
by

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
k : ℕ∞
x : M
this : Nonempty { l // ↑l ≤ k }
m n : { i // ↑i ≤ k }
h : m ≤ n
⊢ ((f - μ • 1) ^ ↑m).ker ≤ ((f - μ • 1) ^ ↑n).ker

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H : IsNilpotent (e₁ - e₂)
H' : Commute e₁ e₂
⊢ (e₁ - e₂) ^ 3 = e₁ - e₂

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H' : Commute e₁ e₂
this : (e₁ - e₂) ^ 3 = e₁ - e₂
n : ℕ
hn : (e₁ - e₂) ^ n = 0
⊢ (e₁ - e₂) ^ (2 * n + 1) = e₁ - e₂

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H : IsNilpotent (e₁ - e₂)
H' : Commute e₁ e₂
⊢ e₁ = e₂

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
M N : Matrix n n R
hN : N ∈ I.matrix.carrier
⊢ M • N ∈ I.matrix.carrier

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
M : Matrix n n R
⊢ M ∈ matrix n I ↔ ∀ (i j : n), M i j ∈ I

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : Nonempty n
I J : Ideal R
eq : matrix n I = matrix n J
⊢ I = J

Tactic:
by

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
k : ℕ∞
x : M
⊢ x ∈ (f.genEigenspace μ) k ↔ ∃ l, ↑l ≤ k ∧ x ∈ ((f - μ • 1) ^ l).ker

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : Ring S
f : R →+* S
I : Type u_3
e : I → R
inst✝ : Fintype I
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
he : ∀ (i : I), IsIdempotentElem (e i)
he' : ∀ (i : I), IsMulCentral (e i)
he'' : CompleteOrthogonalIdempotents (⇑f ∘ e)
e' : I → R
h₁ : CompleteOrthogonalIdempotents e'
h₂ : ⇑f ∘ e' = ⇑f ∘ e
⊢ e = e'

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
⊢ matrix n ⊥ = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
⊢ matrix n ⊤ = ⊤

Tactic:
by

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
k : ℕ∞
x y : { l // ↑l ≤ k }
h : x ≤ y
⊢ (fun x ↦ ↑↑x) x ≤ (fun x ↦ ↑↑x) y

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : Ring S
f : R →+* S
I : Type u_3
e : I → R
inst✝ : Fintype I
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
he : ∀ (i : I), IsIdempotentElem (e i)
he' : ∀ (i : I), IsMulCentral (e i)
he'' : CompleteOrthogonalIdempotents (⇑f ∘ e)
⊢ CompleteOrthogonalIdempotents e

Tactic:
by

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
k : ℕ∞
⊢ Directed (fun x1 x2 ↦ x1 ≤ x2) fun l ↦ (f.genEigenspace μ) ↑↑l

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e' : R
he₂ : IsIdempotentElem e'
he : f e' ∈ f.range
he' : IsIdempotentElem (f e')
x : R
x✝ : (fun e'_1 ↦ IsIdempotentElem e'_1 ∧ f e'_1 = f e') x
hx : IsIdempotentElem x
hx' : f x = f e'
⊢ x - e' ∈ RingHom.ker f

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e : S
he : e ∈ f.range
he' : IsIdempotentElem e
⊢ ∃! e', IsIdempotentElem e' ∧ f e' = e

Tactic:
by

Goal state after:
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 : Ideal R
⊢ ∀ x ∈ I.jacobson, ∀ (i j : n), single i j x ∈ (matrix n I).jacobson

Tactic:
by

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
k : ℕ
x : M
⊢ x ∈ (f.genEigenspace μ) ↑k ↔ x ∈ ((f - μ • 1) ^ k).ker

Tactic:
by

Goal state after:
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
this : Pairwise fun i j ↦ IsCoprime (Ideal.span {1 - e i}) (Ideal.span {1 - e j})
x : R
⊢ (RingHom.pi fun i ↦ Ideal.Quotient.mk (Ideal.span {1 - e i})) x =
    (Ideal.quotientInfToPiQuotient fun i ↦ Ideal.span {1 - e i}) ((Ideal.Quotient.mk (⨅ i, Ideal.span {1 - e i})) x)

Tactic:
by

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 ∈ (f.genEigenspace μ) ⊤ ↔ ∃ k, x ∈ ((f - μ • 1) ^ k).ker

Tactic:
by

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
k : ℕ
⊢ (f.genEigenspace μ) ↑k = ((f - μ • 1) ^ k).ker

Tactic:
by

Goal state after:
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
this : Pairwise fun i j ↦ IsCoprime (Ideal.span {1 - e i}) (Ideal.span {1 - e j})
⊢ Function.Surjective ⇑(RingHom.pi fun i ↦ Ideal.Quotient.mk (Ideal.span {1 - e i}))

Tactic:
by

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
k : ℕ∞
⊢ (f.genEigenspace μ) k = ⨆ l, (f.genEigenspace μ) ↑↑l

Tactic:
by

Goal state after:
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 : Ideal R
⊢ matrix n I.jacobson ≤ (matrix n I).jacobson

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Ideal

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

Tactic:
by

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.genEigenspace μ) ⊤ = ⨆ k, (f.genEigenspace μ) ↑k

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon R
i j : n
x y : R
h : c x y
i' j' : n
⊢ c (Matrix.single i j x i' j') (Matrix.single i j y i' j')

Tactic:
obtain hi | rfl := ne_or_eq i i'

Goal state after:
case inl
R : Type u_1
n : Type u_2
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon R
i j : n
x y : R
h : c x y
i' j' : n
hi : i ≠ i'
⊢ c (Matrix.single i j x i' j') (Matrix.single i j y i' j')

case inr
R : Type u_1
n : Type u_2
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon R
i j : n
x y : R
h : c x y
j' : n
⊢ c (Matrix.single i j x i j') (Matrix.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✝ : Finite I
e : I → R
he : OrthogonalIdempotents e
i j : I
hij : i ≠ j
⊢ 1 * (1 - e i) + e i * (1 - e j) = 1

Tactic:
by

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.genEigenspace μ) 1 = (f - μ • 1).ker

Tactic:
by

Goal state after:
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
⊢ Function.Surjective ⇑(RingHom.pi fun i ↦ Ideal.Quotient.mk (Ideal.span {1 - e i}))

Tactic:
by

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 ∈ (f.genEigenspace μ) 1 ↔ f x = μ • x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
s : Finset I
⊢ ∏ i ∈ s, (1 - e i) = 1 - ∑ i ∈ s, e i

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon R
i j : n
x y : R
⊢ (matrix n c) (Matrix.single i j x) (Matrix.single i j y) ↔ c x y

Tactic:
by

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 ∈ (f.genEigenspace μ) 0 ↔ x = 0

Tactic:
by

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
⊢ ∏ i, (1 - e i) = 0

Tactic:
by

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.genEigenspace μ) 0 = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : Nonempty n
I J : RingCon R
eq : matrix n I = matrix n J
r s : R
⊢ I r s ↔ J r s

Tactic:
by

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
k : ℕ
⊢ (f.genEigenspace 0) ↑k = LinearMap.ker (f ^ k)

Tactic:
by

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, (1 - e i) = 0
⊢ ∑ i, e i = 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : Fintype n
x✝⁴ x✝³ : Matrix n n R
x✝² : ⊤ x✝⁴ x✝³
x✝¹ x✝ : n
⊢ ⊤ (x✝⁴ x✝¹ x✝) (x✝³ x✝¹ x✝)

Tactic:
by

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
k : ℕ∞
x : M
h : f.HasUnifEigenvector μ k x
⊢ f.HasUnifEigenvalue μ k

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon (Matrix n n R)
w✝ x✝ y✝ z✝ : R
h₁ : ∀ (i j : n), c (single i j w✝) (single i j x✝)
h₂ : ∀ (i j : n), c (single i j y✝) (single i j z✝)
i j : n
⊢ c (single i j (w✝ * y✝)) (single i j (x✝ * z✝))

Tactic:
by

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
x : R
hx : ∀ (x_1 : I), 1 - e x_1 ∣ x
this : ∀ (s : Finset I), (∏ i ∈ s, (1 - e i)) * x = x
⊢ x = 0

Tactic:
by

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
v : M
hv : f.HasUnifEigenvector μ 1 v
n : ℕ
⊢ (f ^ n) v = μ ^ n • v

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon (Matrix n n R)
w✝ x✝² y✝ z✝ : R
h₁ : ∀ (i j : n), c (single i j w✝) (single i j x✝²)
h₂ : ∀ (i j : n), c (single i j y✝) (single i j z✝)
x✝¹ x✝ : n
⊢ c (single x✝¹ x✝ (w✝ + y✝)) (single x✝¹ x✝ (x✝² + z✝))

Tactic:
by

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
x : R
hx : ∀ (x_1 : I), 1 - e x_1 ∣ x
s : Finset I
⊢ (∏ i ∈ ∅, (1 - e i)) * x = x

Tactic:
by

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 : ℕ
m : M
hm : f.HasUnifEigenvector μ 1 m
⊢ m ∈ ((f ^ n).genEigenspace (μ ^ n)) 1

Tactic:
by

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
x : R
hx : ∀ (x_1 : I), 1 - e x_1 ∣ x
s✝ : Finset I
a : I
s : Finset I
has : a ∉ s
e' : (∏ i ∈ s, (1 - e i)) * x = x
this : (1 - e a) * x = x
⊢ (∏ i ∈ insert a s, (1 - e i)) * x = x

Tactic:
by

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 : ℕ
⊢ (f ^ n).HasUnifEigenvalue (μ ^ n) 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝³ : NonUnitalNonAssocSemiring R
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : Nonempty n
c : RingCon R
⊢ (matrix n c).ofMatrix = c

Tactic:
by

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
hf : f.HasUnifEigenvalue μ 1
m : M
hm : f.HasUnifEigenvector μ 1 m
n : ℕ
hn : f ^ n = 0
⊢ μ ^ n = 0

Tactic:
by

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
hfn : IsNilpotent f
μ : R
hf : f.HasUnifEigenvalue μ 1
⊢ IsNilpotent μ

Tactic:
by

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
⊢ Function.Bijective ⇑(RingHom.pi fun i ↦ Ideal.Quotient.mk (Ideal.span {1 - e i}))

Tactic:
by

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 fun x ↦ 1 - e x
⊢ ∀ (x : I), 1 - (1 - e x) = e x

Tactic:
by

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 fun x ↦ 1 - e x
⊢ Function.Bijective ⇑(RingHom.pi fun i ↦ Ideal.Quotient.mk (Ideal.span {e i}))

Tactic:
by

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
⊢ μ ∈ spectrum R f

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon (Matrix n n R)
⊢ matrix n c.ofMatrix = c

Tactic:
by

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 : ∀ (i : I), IsIdempotentElem (e i)
he₁ : ∀ (i j : I), i ≠ j → (1 - e i) * (1 - e j) = 0
he₂ : ∏ i, e i = 0
⊢ ∏ i, (1 - (1 - e i)) = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: 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 : R
i j : n
⊢ c.ofMatrix x y ↔ c (single i j x) (single i j y)

Tactic:
by

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.HasUnifEigenvalue μ 1 ↔ μ ∈ spectrum K f

Tactic:
by

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.genEigenspace (a / b)) 1 = (f.genEigenspace (b⁻¹ * a)) 1

Tactic:
by

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.genEigenspace (b⁻¹ * a)) 1 = (f - (b⁻¹ * a) • 1).ker

Tactic:
by

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:
by

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 = (b • (f - b⁻¹ • a • 1)).ker

Tactic:
by

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
⊢ (b • (f - b⁻¹ • a • 1)).ker = (b • f - a • 1).ker

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon (Matrix n n R)
i j : n
⊢ ⇑c.ofMatrix = Relation.Map (⇑c) (fun x ↦ x i j) fun x ↦ x i j

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: 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
r : R
h : r ∈ ↑(equivMatrix.symm I)
⊢ single i j r ∈ I

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: 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
r : R
h : r ∈ ↑(equivMatrix.symm I)
⊢ single i j r i j = r

Tactic:
by

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
k : ℕ
x : M
i : ℕ
hi : i ≤ k
⊢ k = i + (k - i)

Tactic:
by

Goal state after: