Theorem: Module.End.eigenspace_add (CvxLean/Lib/Math/LinearAlgebra/Eigenspace.lean)

State before:
K R : Type v
V M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f g : End R M
a b : R
⊢ f.eigenspace a ⊓ g.eigenspace b ≤ (f + g).eigenspace (a + b)
Tactic:
rintro x ⟨hf, hg⟩
State after:
case intro
K R : Type v
V M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f g : End R M
a b : R
x : M
hf : x ∈ ↑(f.eigenspace a)
hg : x ∈ ↑(g.eigenspace b)
⊢ x ∈ (f + g).eigenspace (a + b)

State before:
case intro
K R : Type v
V M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f g : End R M
a b : R
x : M
hf : x ∈ ↑(f.eigenspace a)
hg : x ∈ ↑(g.eigenspace b)
⊢ x ∈ (f + g).eigenspace (a + b)
Tactic:
simp only [eigenspace, SetLike.mem_coe, LinearMap.mem_ker,
  LinearMap.sub_apply, algebraMap_end_apply] at hf hg
State after:
case intro
K R : Type v
V M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f g : End R M
a b : R
x : M
hf : f x - a • x = 0
hg : g x - b • x = 0
⊢ x ∈ (f + g).eigenspace (a + b)

State before:
case intro
K R : Type v
V M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f g : End R M
a b : R
x : M
hf : f x - a • x = 0
hg : g x - b • x = 0
⊢ x ∈ (f + g).eigenspace (a + b)
Tactic:
simp only [eigenspace, map_add, LinearMap.mem_ker, LinearMap.sub_apply,
  LinearMap.add_apply, algebraMap_end_apply]
State after:
case intro
K R : Type v
V M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f g : End R M
a b : R
x : M
hf : f x - a • x = 0
hg : g x - b • x = 0
⊢ f x + g x - (a • x + b • x) = 0

State before:
case intro
K R : Type v
V M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f g : End R M
a b : R
x : M
hf : f x - a • x = 0
hg : g x - b • x = 0
⊢ f x + g x - (a • x + b • x) = 0
Tactic:
rw [← add_sub, add_comm (a • x), ← sub_sub, hg, add_sub, add_zero, hf]
State after:
no goals