-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem sup_ker_aeval_le_ker_aeval_mul {f : M →ₗ[R] M} {p q : R[X]} :
    LinearMap.ker (aeval f p) ⊔ LinearMap.ker (aeval f q) ≤ LinearMap.ker (aeval f (p * q))

Proof state:
R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ LinearMap.ker ((aeval f) p) ⊔ LinearMap.ker ((aeval f) q)
x : M
hx : x ∈ LinearMap.ker ((aeval f) p)
y : M
hy : y ∈ LinearMap.ker ((aeval f) q)
hxy : x + y = v
h_eval_x : ((aeval f) (p * q)) x = 0
⊢ ((aeval f) (p * q)) y = 0

Tactic:
rw [aeval_mul, LinearMap.mul_apply, LinearMap.mem_ker.1 hy, LinearMap.map_zero]

Result:
no goals

Proof state:
case intro.intro.intro.intro
R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ LinearMap.ker ((aeval f) p) ⊔ LinearMap.ker ((aeval f) q)
x : M
hx : x ∈ LinearMap.ker ((aeval f) p)
y : M
hy : y ∈ LinearMap.ker ((aeval f) q)
hxy : x + y = v
h_eval_x : ((aeval f) (p * q)) x = 0
h_eval_y : ((aeval f) (p * q)) y = 0
⊢ v ∈ LinearMap.ker ((aeval f) (p * q))

Tactic:
rw [LinearMap.mem_ker, ← hxy, LinearMap.map_add, h_eval_x, h_eval_y, add_zero]

Result:
no goals

Proof state:
case intro.intro.intro.intro
R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ LinearMap.ker ((aeval f) p) ⊔ LinearMap.ker ((aeval f) q)
x : M
hx : x ∈ LinearMap.ker ((aeval f) p)
y : M
hy : y ∈ LinearMap.ker ((aeval f) q)
hxy : x + y = v
h_eval_x : ((aeval f) (p * q)) x = 0
⊢ v ∈ LinearMap.ker ((aeval f) (p * q))

Tactic:
have h_eval_y : aeval f (p * q) y = 0 := by
  rw [aeval_mul, LinearMap.mul_apply, LinearMap.mem_ker.1 hy, LinearMap.map_zero]

Result:
case intro.intro.intro.intro
R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ LinearMap.ker ((aeval f) p) ⊔ LinearMap.ker ((aeval f) q)
x : M
hx : x ∈ LinearMap.ker ((aeval f) p)
y : M
hy : y ∈ LinearMap.ker ((aeval f) q)
hxy : x + y = v
h_eval_x : ((aeval f) (p * q)) x = 0
h_eval_y : ((aeval f) (p * q)) y = 0
⊢ v ∈ LinearMap.ker ((aeval f) (p * q))

Proof state:
R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ LinearMap.ker ((aeval f) p) ⊔ LinearMap.ker ((aeval f) q)
x : M
hx : x ∈ LinearMap.ker ((aeval f) p)
y : M
hy : y ∈ LinearMap.ker ((aeval f) q)
hxy : x + y = v
⊢ ((aeval f) (p * q)) x = 0

Tactic:
rw [mul_comm, aeval_mul, LinearMap.mul_apply, LinearMap.mem_ker.1 hx, LinearMap.map_zero]

Result:
no goals

Proof state:
R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ LinearMap.ker ((aeval f) p) ⊔ LinearMap.ker ((aeval f) q)
⊢ v ∈ LinearMap.ker ((aeval f) (p * q))

Tactic:
rcases Submodule.mem_sup.1 hv with ⟨x, hx, y, hy, hxy⟩

Result:
case intro.intro.intro.intro
R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ LinearMap.ker ((aeval f) p) ⊔ LinearMap.ker ((aeval f) q)
x : M
hx : x ∈ LinearMap.ker ((aeval f) p)
y : M
hy : y ∈ LinearMap.ker ((aeval f) q)
hxy : x + y = v
⊢ v ∈ LinearMap.ker ((aeval f) (p * q))

Proof state:
R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
⊢ LinearMap.ker ((aeval f) p) ⊔ LinearMap.ker ((aeval f) q) ≤ LinearMap.ker ((aeval f) (p * q))

Tactic:
intro v hv

Result:
R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ LinearMap.ker ((aeval f) p) ⊔ LinearMap.ker ((aeval f) q)
⊢ v ∈ LinearMap.ker ((aeval f) (p * q))

Proof state:
case intro.intro.intro.intro
R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ LinearMap.ker ((aeval f) p) ⊔ LinearMap.ker ((aeval f) q)
x : M
hx : x ∈ LinearMap.ker ((aeval f) p)
y : M
hy : y ∈ LinearMap.ker ((aeval f) q)
hxy : x + y = v
⊢ v ∈ LinearMap.ker ((aeval f) (p * q))

Tactic:
have h_eval_x : aeval f (p * q) x = 0 := by
  rw [mul_comm, aeval_mul, LinearMap.mul_apply, LinearMap.mem_ker.1 hx, LinearMap.map_zero]

Result:
case intro.intro.intro.intro
R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ LinearMap.ker ((aeval f) p) ⊔ LinearMap.ker ((aeval f) q)
x : M
hx : x ∈ LinearMap.ker ((aeval f) p)
y : M
hy : y ∈ LinearMap.ker ((aeval f) q)
hxy : x + y = v
h_eval_x : ((aeval f) (p * q)) x = 0
⊢ v ∈ LinearMap.ker ((aeval f) (p * q))