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
k m : ℕ∞
hm : 0 < m
hk : f.HasUnifEigenvalue μ k
contra : (f.genEigenspace μ) 1 = ⊥
⊢ False

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 : (f.genEigenspace μ) 1 = ⊥
⊢ False
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case refine_1.none.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
j : I
h : none ≠ some j
⊢ e₀ * ((1 - e₀) * e' j) = 0

Tactic:
;

Goal state after:
case refine_1.none.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
j : I
h : none ≠ some j
⊢ e₀ * ((1 - e₀) * e' j) = 0
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case refine_1.some.none
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 : I
h : some i ≠ none
⊢ (1 - e₀) * e' i * e₀ = 0

Tactic:
;

Goal state after:
case refine_1.some.none
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 : I
h : some i ≠ none
⊢ (1 - e₀) * e' i * e₀ = 0
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
e : R
inst✝ : Semigroup R
a b : R
⊢ (fun x ↦ e * x * e) a * (fun x ↦ e * x * e) b ∈ Set.range fun x ↦ e * x * e

Tactic:
;

Goal state after:
R : Type u_1
e : R
inst✝ : Semigroup R
a b : R
⊢ (fun x ↦ e * x * e) a * (fun x ↦ e * x * e) b ∈ Set.range fun x ↦ e * x * e
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
e : R
inst✝ : Semigroup R
idem : IsIdempotentElem e
r : R
⊢ e * (fun x ↦ e * x * e) r = (fun x ↦ e * x * e) r ∧ (fun x ↦ e * x * e) r * e = (fun x ↦ e * x * e) r

Tactic:
;

Goal state after:
R : Type u_1
e : R
inst✝ : Semigroup R
idem : IsIdempotentElem e
r : R
⊢ e * (fun x ↦ e * x * e) r = (fun x ↦ e * x * e) r ∧ (fun x ↦ e * x * e) r * e = (fun x ↦ e * x * 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
⊢ 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
⊢ r * e = 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
⊢ r * e = r
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.maxGenEigenspace μ ↔ x✝ ∈ (f - μ • 1).maxGenEigenspace 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
x✝ : M
⊢ x✝ ∈ f.maxGenEigenspace μ ↔ x✝ ∈ (f - μ • 1).maxGenEigenspace 0
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
e : R
inst✝ : NonUnitalSemiring R
a b : R
⊢ (fun x ↦ e * x * e) a + (fun x ↦ e * x * e) b ∈ (Subsemigroup.corner e).carrier

Tactic:
;

Goal state after:
R : Type u_1
e : R
inst✝ : NonUnitalSemiring R
a b : R
⊢ (fun x ↦ e * x * e) a + (fun x ↦ e * x * e) b ∈ (Subsemigroup.corner e).carrier
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
e : R
inst✝ : NonUnitalRing R
a : R
⊢ -(fun x ↦ e * x * e) a ∈ (NonUnitalSubsemiring.corner e).carrier

Tactic:
;

Goal state after:
R : Type u_1
e : R
inst✝ : NonUnitalRing R
a : R
⊢ -(fun x ↦ e * x * e) a ∈ (NonUnitalSubsemiring.corner e).carrier
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
e✝ : R
I : Type u_2
inst✝¹ : Fintype I
e : I → R
inst✝ : Semiring R
he : CompleteOrthogonalIdempotents e
hc : ∀ (i : I), IsMulCentral (e i)
r : (i : I) → ⋯.Corner
i : I
r' : R
eq : (fun x ↦ e i * x * e i) r' = ↑(r i)
⊢ e i * (fun x ↦ e i * x * e i) r' * e i = (fun x ↦ e i * x * e i) r'

Tactic:
;

Goal state after:
R : Type u_1
e✝ : R
I : Type u_2
inst✝¹ : Fintype I
e : I → R
inst✝ : Semiring R
he : CompleteOrthogonalIdempotents e
hc : ∀ (i : I), IsMulCentral (e i)
r : (i : I) → ⋯.Corner
i : I
r' : R
eq : (fun x ↦ e i * x * e i) r' = ↑(r i)
⊢ e i * (fun x ↦ e i * x * e i) r' * e i = (fun x ↦ e i * x * e i) r'
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
e✝ : R
I : Type u_2
inst✝¹ : Fintype I
e : I → R
inst✝ : Semiring R
he : CompleteOrthogonalIdempotents e
hc : ∀ (i : I), IsMulCentral (e i)
r : (i : I) → ⋯.Corner
i j : I
a✝ : j ∈ Finset.univ
ne : j ≠ i
⊢ e i * ↑(r j) * e i = 0

Tactic:
;

Goal state after:
R : Type u_1
e✝ : R
I : Type u_2
inst✝¹ : Fintype I
e : I → R
inst✝ : Semiring R
he : CompleteOrthogonalIdempotents e
hc : ∀ (i : I), IsMulCentral (e i)
r : (i : I) → ⋯.Corner
i j : I
a✝ : j ∈ Finset.univ
ne : j ≠ i
⊢ e i * ↑(r j) * e i = 0
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
e✝ : R
I : Type u_2
inst✝¹ : Fintype I
e : I → R
inst✝ : Semiring R
he : CompleteOrthogonalIdempotents e
hc : ∀ (i : I), IsMulCentral (e i)
r : (i : I) → ⋯.Corner
i j : I
a✝ : j ∈ Finset.univ
ne : j ≠ i
r' : R
eq : (fun x ↦ e j * x * e j) r' = ↑(r j)
⊢ e i * (fun x ↦ e j * x * e j) r' * e i = 0

Tactic:
;

Goal state after:
R : Type u_1
e✝ : R
I : Type u_2
inst✝¹ : Fintype I
e : I → R
inst✝ : Semiring R
he : CompleteOrthogonalIdempotents e
hc : ∀ (i : I), IsMulCentral (e i)
r : (i : I) → ⋯.Corner
i j : I
a✝ : j ∈ Finset.univ
ne : j ≠ i
r' : R
eq : (fun x ↦ e j * x * e j) r' = ↑(r j)
⊢ e i * (fun x ↦ e j * x * e j) r' * e i = 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
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k✝ l✝ : ℕ∞
k : ℕ
property✝¹ : ↑k ≤ k✝
l : ℕ
property✝ : ↑l ≤ l✝
a✝ : Nontrivial M
p : Submodule R M := ⋯
hp : Nontrivial ↥p
f₁ : End R ↥p := ⋯
f₂ : End R ↥p := ⋯
x✝ : ↥p
⊢ ↑((f₂ * f₁) x✝) = ↑((f₁ * f₂) x✝)

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✝ : ℕ∞
k : ℕ
property✝¹ : ↑k ≤ k✝
l : ℕ
property✝ : ↑l ≤ l✝
a✝ : Nontrivial M
p : Submodule R M := ⋯
hp : Nontrivial ↥p
f₁ : End R ↥p := ⋯
f₂ : End R ↥p := ⋯
x✝ : ↥p
⊢ ↑((f₂ * f₁) x✝) = ↑((f₁ * f₂) x✝)
Module: Mathlib.Algebra.Divisibility.Prod

Goal state before:
pp: case mk
G₁ : Type u_2
G₂ : Type u_3
inst✝¹ : Semigroup G₁
inst✝ : Semigroup G₂
y : G₁ × G₂
fst✝ : G₁
snd✝ : G₂
⊢ (fst✝, snd✝) ∣ y ↔ (fst✝, snd✝).1 ∣ y.1 ∧ (fst✝, snd✝).2 ∣ y.2

Tactic:
;

Goal state after:
case mk
G₁ : Type u_2
G₂ : Type u_3
inst✝¹ : Semigroup G₁
inst✝ : Semigroup G₂
y : G₁ × G₂
fst✝ : G₁
snd✝ : G₂
⊢ (fst✝, snd✝) ∣ y ↔ (fst✝, snd✝).1 ∣ y.1 ∧ (fst✝, snd✝).2 ∣ y.2
Module: Mathlib.Algebra.Divisibility.Prod

Goal state before:
pp: ι : Type u_1
G : ι → Type u_4
inst✝ : (i : ι) → Semigroup (G i)
x y : (i : ι) → G i
⊢ (∃ c, ∀ (x_1 : ι), y x_1 = (x * c) x_1) ↔ ∃ f, ∀ (x_1 : ι), y x_1 = x x_1 * f x_1

Tactic:
;

Goal state after:
ι : Type u_1
G : ι → Type u_4
inst✝ : (i : ι) → Semigroup (G i)
x y : (i : ι) → G i
⊢ (∃ c, ∀ (x_1 : ι), y x_1 = (x * c) x_1) ↔ ∃ f, ∀ (x_1 : ι), y x_1 = x x_1 * f x_1
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✝ : ℕ∞
k : ℕ
property✝¹ : ↑k ≤ k✝
l : ℕ
property✝ : ↑l ≤ l✝
a✝ : Nontrivial M
p : Submodule R M := ⋯
hp : Nontrivial ↥p
f₁ : End R ↥p := ⋯
f₂ : End R ↥p := ⋯
this : IsNilpotent (f₂ - f₁)
x✝ : ↥p
⊢ ↑((f₂ - f₁) x✝) = ↑(((algebraMap R (End R ↥p)) (μ₁ - μ₂)) x✝)

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✝ : ℕ∞
k : ℕ
property✝¹ : ↑k ≤ k✝
l : ℕ
property✝ : ↑l ≤ l✝
a✝ : Nontrivial M
p : Submodule R M := ⋯
hp : Nontrivial ↥p
f₁ : End R ↥p := ⋯
f₂ : End R ↥p := ⋯
this : IsNilpotent (f₂ - f₁)
x✝ : ↥p
⊢ ↑((f₂ - f₁) x✝) = ↑(((algebraMap R (End R ↥p)) (μ₁ - μ₂)) 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
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
k : ℕ∞
⊢ iSupIndep fun x ↦ (f.genEigenspace x) k

Tactic:
suffices ∀ μ₁ (s : Finset R), μ₁ ∉ s → Disjoint (f.genEigenspace μ₁ k)
    (s.sup fun μ ↦ f.genEigenspace μ k) by
    simp_rw [iSupIndep_iff_supIndep,
      Finset.supIndep_iff_disjoint_erase]
    exact fun s μ _ ↦ this _ _ (s.notMem_erase μ)

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
k : ℕ∞
⊢ ∀ (μ₁ : R) (s : Finset R), μ₁ ∉ s → Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ ↦ (f.genEigenspace μ) k)
Module: Mathlib.Algebra.DualNumber

Goal state before:
pp: R : Type u_1
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : TrivSqZeroExt A A
hx : x ∈ ⊤
⊢ x ∈ (inlAlgHom R A A).range ⊔ R[ ε]

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : TrivSqZeroExt A A
hx : x ∈ ⊤
⊢ x ∈ (inlAlgHom R A A).range ⊔ R[ ε]
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: case insert
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
k : ℕ∞
μ₁ μ₂ : R
s : Finset R
a✝ : μ₂ ∉ s
ih : Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ ↦ (f.genEigenspace μ) k)
hμ₁₂✝ : μ₁ ∉ insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ s
y : M
hy : y ∈ (f.genEigenspace μ₂) k
z : M
hz : z ∈ s.sup fun μ ↦ (f.genEigenspace μ) k
hx : y + z ∈ (f.genEigenspace μ₁) k
hx' : y + z ∈ (f.genEigenspace μ₂) k ⊔ s.sup fun μ ↦ (f.genEigenspace μ) k
⊢ y + z ∈ (f.genEigenspace μ₂) k

Tactic:
;

Goal state after:
case insert
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
k : ℕ∞
μ₁ μ₂ : R
s : Finset R
a✝ : μ₂ ∉ s
ih : Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ ↦ (f.genEigenspace μ) k)
hμ₁₂✝ : μ₁ ∉ insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ s
y : M
hy : y ∈ (f.genEigenspace μ₂) k
z : M
hz : z ∈ s.sup fun μ ↦ (f.genEigenspace μ) k
hx : y + z ∈ (f.genEigenspace μ₁) k
hx' : y + z ∈ (f.genEigenspace μ₂) k ⊔ s.sup fun μ ↦ (f.genEigenspace μ) k
⊢ y + z ∈ (f.genEigenspace μ₂) k
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
e : Dual R M ⊗[R] M ≃ₗ[R] M →ₗ[R] M := dualTensorHomEquiv R M M
h : Function.Surjective ⇑↑e
f : Dual R M
m : M
⊢ ((AlgebraTensorModule.curry ((trace R (Dual R M) ∘ₗ Dual.transpose) ∘ₗ ↑e)) f) m =
    ((AlgebraTensorModule.curry (trace R M ∘ₗ ↑e)) f) m

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
e : Dual R M ⊗[R] M ≃ₗ[R] M →ₗ[R] M := dualTensorHomEquiv R M M
h : Function.Surjective ⇑↑e
f : Dual R M
m : M
⊢ ((AlgebraTensorModule.curry ((trace R (Dual R M) ∘ₗ Dual.transpose) ∘ₗ ↑e)) f) m =
    ((AlgebraTensorModule.curry (trace R M ∘ₗ ↑e)) f) 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
p : Submodule R M
k : ℕ∞
μ : R
hfp : ∀ x ∈ p, f x ∈ p
x : ↥p
⊢ x ∈ (genEigenspace (LinearMap.restrict f hfp) μ) k ↔ x ∈ Submodule.comap p.subtype ((f.genEigenspace μ) k)

Tactic:
suffices ∀ l : ℕ, genEigenspace (LinearMap.restrict f hfp) μ l =
      Submodule.comap p.subtype (f.genEigenspace μ l) by
    simp_rw [mem_genEigenspace, ← mem_genEigenspace_nat, this,
      Submodule.mem_comap, mem_genEigenspace (k := k), mem_genEigenspace_nat]

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
k : ℕ∞
μ : R
hfp : ∀ x ∈ p, f x ∈ p
x : ↥p
⊢ ∀ (l : ℕ), (genEigenspace (LinearMap.restrict f hfp) μ) ↑l = Submodule.comap p.subtype ((f.genEigenspace μ) ↑l)
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] R
x : M
⊢ (trace R M) (f.smulRight x) = f x

Tactic:
rw [trace_eq_matrix_trace _ (Free.chooseBasis R M), ← (Free.chooseBasis R M).sum_repr x]

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] R
x : M
⊢ ((toMatrix (Free.chooseBasis R M) (Free.chooseBasis R M))
        (f.smulRight (∑ i, ((Free.chooseBasis R M).repr x) i • (Free.chooseBasis R M) i))).trace =
    f (∑ i, ((Free.chooseBasis R M).repr x) i • (Free.chooseBasis R M) 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
inst✝ : FiniteDimensional K V
f : End K V
μ : K
⊢ (((f - μ • 1) ^ finrank K V) ∘ₗ (f - μ • 1) ^ finrank K V).ker =
    ((f - (algebraMap K (End K V)) μ) ^ finrank K V * (f - (algebraMap K (End K V)) μ) ^ finrank K V).ker

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) ^ finrank K V) ∘ₗ (f - μ • 1) ^ finrank K V).ker =
    ((f - (algebraMap K (End K V)) μ) ^ finrank K V * (f - (algebraMap K (End K V)) μ) ^ 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
⊢ LinearMap.ker ((f - (algebraMap K (End K V)) μ) ^ (finrank K V + finrank K V)) =
    ((f - μ • 1) ^ (finrank K V + finrank K V)).ker

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
⊢ LinearMap.ker ((f - (algebraMap K (End K V)) μ) ^ (finrank K V + finrank K V)) =
    ((f - μ • 1) ^ (finrank K V + finrank K V)).ker
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: case hk
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
⊢ finrank K V ≤ finrank K V + finrank K V

Tactic:
;

Goal state after:
case hk
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
⊢ finrank K V ≤ finrank K V + finrank K V
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] M
e : M ≃ₗ[R] N
⊢ (trace R N) (e.conj f) = (trace R M) f

Tactic:
by_cases hM : ∃ s : Finset M, Nonempty (Basis s R M)
  · obtain ⟨s, ⟨b⟩⟩ := hM
    have := Module.Finite.of_basis b
    have := (Module.free_def R M).mpr ⟨_, ⟨b⟩⟩
    have := Module.Finite.of_basis (b.map e)
    have := (Module.free_def R N).mpr ⟨_, ⟨(b.map e).reindex (e.toEquiv.image _)⟩⟩
    rw [e.conj_apply, trace_comp_comm', ← comp_assoc, LinearEquiv.comp_coe,
      LinearEquiv.self_trans_symm, LinearEquiv.refl_toLinearMap, id_comp]
  · rw [trace, trace, dif_neg hM, dif_neg ?_, zero_apply, zero_apply]
    rintro ⟨s, ⟨b⟩⟩
    exact hM ⟨s.image e.symm, ⟨(b.map e.symm).reindex
      ((e.symm.toEquiv.image s).trans (Equiv.setCongr Finset.coe_image.symm))⟩⟩

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
μ : K
n : ℕ
⊢ Submodule.map f ((f - μ • 1) ^ n).range = (f * (f - (algebraMap K (End K V)) μ) ^ n).range

Tactic:
;

Goal state after:
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
μ : K
n : ℕ
⊢ Submodule.map f ((f - μ • 1) ^ n).range = (f * (f - (algebraMap K (End K V)) μ) ^ n).range
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
μ : K
n : ℕ
⊢ Submodule.map ((f - (algebraMap K (End K V)) μ) ^ n) (LinearMap.range f) ≤ ((f - μ • 1) ^ n).range

Tactic:
;

Goal state after:
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
μ : K
n : ℕ
⊢ Submodule.map ((f - (algebraMap K (End K V)) μ) ^ n) (LinearMap.range f) ≤ ((f - μ • 1) ^ n).range
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₁ f₂ : End R M
μ₁ μ₂ : R
k₁ k₂ : ℕ∞
h : Commute f₁ f₂
m : M
l₁ : ℕ
hlk₁ : ↑l₁ ≤ k₁
hl₁ : ((f₁ - μ₁ • 1) ^ l₁) m = 0
l₂ : ℕ
hlk₂ : ↑l₂ ≤ k₂
hl₂ : ((f₂ - μ₂ • 1) ^ l₂) m = 0
⊢ f₁ + f₂ - (μ₁ • 1 + μ₂ • 1) = f₁ - μ₁ • 1 + (f₂ - μ₂ • 1)

Tactic:
;

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f₁ f₂ : End R M
μ₁ μ₂ : R
k₁ k₂ : ℕ∞
h : Commute f₁ f₂
m : M
l₁ : ℕ
hlk₁ : ↑l₁ ≤ k₁
hl₁ : ((f₁ - μ₁ • 1) ^ l₁) m = 0
l₂ : ℕ
hlk₂ : ↑l₂ ≤ k₂
hl₂ : ((f₂ - μ₂ • 1) ^ l₂) m = 0
⊢ f₁ + f₂ - (μ₁ • 1 + μ₂ • 1) = f₁ - μ₁ • 1 + (f₂ - μ₂ • 1)
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsReduced R
f g : End R M
μ : R
h_comm : Commute f g
n : End R M := g - (algebraMap R (End R M)) μ
hg : (trace R M) (f ∘ₗ n) = 0
hμ : g = (algebraMap R (End R M)) μ + n
x✝ : M
⊢ (f ∘ₗ (algebraMap R (M →ₗ[R] M)) μ) x✝ = (μ • f) x✝

Tactic:
;

Goal state after:
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsReduced R
f g : End R M
μ : R
h_comm : Commute f g
n : End R M := g - (algebraMap R (End R M)) μ
hg : (trace R M) (f ∘ₗ n) = 0
hμ : g = (algebraMap R (End R M)) μ + n
x✝ : M
⊢ (f ∘ₗ (algebraMap R (M →ₗ[R] M)) μ) x✝ = (μ • f) x✝
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
inst✝¹ : Nontrivial R
inst✝ : Free R S
h : finrank R S = 1
this✝ : Module.Finite R S
this : Free R (End R S)
f : S →ₐ[R] S →ₗ[R] S := ⋯
⊢ (LinearMap.trace R S ∘ₗ ↑f ∘ₗ Algebra.linearMap R S) 1 = LinearMap.id 1

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
inst✝¹ : Nontrivial R
inst✝ : Free R S
h : finrank R S = 1
this✝ : Module.Finite R S
this : Free R (End R S)
f : S →ₐ[R] S →ₗ[R] S := ⋯
⊢ (LinearMap.trace R S ∘ₗ ↑f ∘ₗ Algebra.linearMap R S) 1 = LinearMap.id 1
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: case h.right
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f₁ f₂ : End R M
μ₁ μ₂ : R
k₁ k₂ : ℕ∞
m : M
l₁ : ℕ
hlk₁ : ↑l₁ ≤ k₁
hl₁ : ((f₁ - μ₁ • 1) ^ l₁) m = 0
l₂ : ℕ
hlk₂ : ↑l₂ ≤ k₂
hl₂ : ((f₂ - μ₂ • 1) ^ l₂) m = 0
this : f₁ + f₂ - (μ₁ + μ₂) • 1 = f₁ - μ₁ • 1 + (f₂ - μ₂ • 1)
h : Commute (f₁ - μ₁ • 1) (f₂ - μ₂ • 1)
x✝ : ℕ × ℕ
i j : ℕ
hij : (i, j).1 + (i, j).2 = l₁ + l₂
⊢ ((f₁ - μ₁ • 1) ^ i * (f₂ - μ₂ • 1) ^ j) m = 0

Tactic:
obtain hi | hj : l₁ ≤ i ∨ l₂ ≤ j := by lia

Goal state after:
case h.right.inl
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f₁ f₂ : End R M
μ₁ μ₂ : R
k₁ k₂ : ℕ∞
m : M
l₁ : ℕ
hlk₁ : ↑l₁ ≤ k₁
hl₁ : ((f₁ - μ₁ • 1) ^ l₁) m = 0
l₂ : ℕ
hlk₂ : ↑l₂ ≤ k₂
hl₂ : ((f₂ - μ₂ • 1) ^ l₂) m = 0
this : f₁ + f₂ - (μ₁ + μ₂) • 1 = f₁ - μ₁ • 1 + (f₂ - μ₂ • 1)
h : Commute (f₁ - μ₁ • 1) (f₂ - μ₂ • 1)
x✝ : ℕ × ℕ
i j : ℕ
hij : (i, j).1 + (i, j).2 = l₁ + l₂
hi : l₁ ≤ i
⊢ ((f₁ - μ₁ • 1) ^ i * (f₂ - μ₂ • 1) ^ j) m = 0

case h.right.inr
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f₁ f₂ : End R M
μ₁ μ₂ : R
k₁ k₂ : ℕ∞
m : M
l₁ : ℕ
hlk₁ : ↑l₁ ≤ k₁
hl₁ : ((f₁ - μ₁ • 1) ^ l₁) m = 0
l₂ : ℕ
hlk₂ : ↑l₂ ≤ k₂
hl₂ : ((f₂ - μ₂ • 1) ^ l₂) m = 0
this : f₁ + f₂ - (μ₁ + μ₂) • 1 = f₁ - μ₁ • 1 + (f₂ - μ₂ • 1)
h : Commute (f₁ - μ₁ • 1) (f₂ - μ₂ • 1)
x✝ : ℕ × ℕ
i j : ℕ
hij : (i, j).1 + (i, j).2 = l₁ + l₂
hj : l₂ ≤ j
⊢ ((f₁ - μ₁ • 1) ^ i * (f₂ - μ₂ • 1) ^ j) m = 0
Module: Mathlib.Algebra.Free

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Mul β
f g : FreeMagma α →ₙ* β
h : ⇑f ∘ of = ⇑g ∘ of
x x✝ y✝ : FreeMagma α
a✝¹ : f x✝ = g x✝
a✝ : f y✝ = g y✝
⊢ f (x✝ * y✝) = g (x✝ * y✝)

Tactic:
;

Goal state after:
α : Type u
β : Type v
inst✝ : Mul β
f g : FreeMagma α →ₙ* β
h : ⇑f ∘ of = ⇑g ∘ of
x x✝ y✝ : FreeMagma α
a✝¹ : f x✝ = g x✝
a✝ : f y✝ = g y✝
⊢ f (x✝ * y✝) = g (x✝ * y✝)
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
p : Prop
x : α
b : Bool
L1 L2 L3 : List (α × Bool)
x' : α
b' : Bool
r : reduce L1 = []
⊢ [(x, b)] = L2 ++ (x', b') :: (x', !b') :: L3 → p

Tactic:
;

Goal state after:
case nil
α : Type u_1
inst✝ : DecidableEq α
p : Prop
x : α
b : Bool
L1 L2 L3 : List (α × Bool)
x' : α
b' : Bool
r : reduce L1 = []
⊢ [(x, b)] = L2 ++ (x', b') :: (x', !b') :: L3 → p
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: case neg.nil
α : Type u_1
inst✝ : DecidableEq α
p : Prop
x : α
b : Bool
L1 L3 : List (α × Bool)
x' : α
b' : Bool
tail : List (α × Bool)
y : α
c : Bool
r : reduce L1 = (y, c) :: tail
h : ¬(x = y ∧ b = !c)
fst_eq✝¹ : x = x'
snd_eq✝¹ : b = b'
tail_eq✝ : tail = L3
fst_eq✝ : y = x'
snd_eq✝ : c = !b'
⊢ p

Tactic:
;

Goal state after:
case neg.nil
α : Type u_1
inst✝ : DecidableEq α
p : Prop
x : α
b : Bool
L1 L3 : List (α × Bool)
x' : α
b' : Bool
tail : List (α × Bool)
y : α
c : Bool
r : reduce L1 = (y, c) :: tail
h : ¬(x = y ∧ b = !c)
fst_eq✝¹ : x = x'
snd_eq✝¹ : b = b'
tail_eq✝ : tail = L3
fst_eq✝ : y = x'
snd_eq✝ : c = !b'
⊢ p