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

Proof state:
case 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 * q))
p' q' : R[X]
hpq' : p' * p + q' * q = 1
h_eval₂_qpp' : ((aeval f) q * (aeval f) (p * p')) v = 0
h_eval₂_pqq' : ((aeval f) p * (aeval f) (q * q')) v = 0
⊢ ((aeval f) (q * q')) v + ((aeval f) (p * p')) v = v

Tactic:
rw [add_comm, mul_comm p p', mul_comm q q']

Result:
case 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 * q))
p' q' : R[X]
hpq' : p' * p + q' * q = 1
h_eval₂_qpp' : ((aeval f) q * (aeval f) (p * p')) v = 0
h_eval₂_pqq' : ((aeval f) p * (aeval f) (q * q')) v = 0
⊢ ((aeval f) (p' * p)) v + ((aeval f) (q' * q)) v = v

Proof state:
case 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 * q))
p' q' : R[X]
hpq' : p' * p + q' * q = 1
h_eval₂_qpp' : ((aeval f) q * (aeval f) (p * p')) v = 0
h_eval₂_pqq' : ((aeval f) p * (aeval f) (q * q')) v = 0
⊢ ∃ y ∈ LinearMap.ker ((aeval f) p), ∃ z ∈ LinearMap.ker ((aeval f) q), y + z = v

Tactic:
refine
  ⟨aeval f (q * q') v, LinearMap.mem_ker.1 h_eval₂_pqq', aeval f (p * p') v,
    LinearMap.mem_ker.1 h_eval₂_qpp', ?_⟩

Result:
case 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 * q))
p' q' : R[X]
hpq' : p' * p + q' * q = 1
h_eval₂_qpp' : ((aeval f) q * (aeval f) (p * p')) v = 0
h_eval₂_pqq' : ((aeval f) p * (aeval f) (q * q')) v = 0
⊢ ((aeval f) (q * q')) v + ((aeval f) (p * p')) v = v

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 * q))
p' q' : R[X]
hpq' : p' * p + q' * q = 1
h_eval₂_qpp' : ((aeval f) (q * (p * p'))) v = 0
⊢ ((aeval f) (p * (q * q'))) v = ((aeval f) (q' * (p * q))) v

Tactic:
rw [← mul_assoc, mul_comm]

Result:
no goals

Proof state:
case 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 * q))
p' q' : R[X]
hpq' : p' * p + q' * q = 1
h_eval₂_qpp' : ((aeval f) (q * (p * p'))) v = 0
⊢ ∃ y ∈ LinearMap.ker ((aeval f) p), ∃ z ∈ LinearMap.ker ((aeval f) q), y + z = v

Tactic:
have h_eval₂_pqq' :=
  calc
    aeval f (p * (q * q')) v = aeval f (q' * (p * q)) v := by rw [← mul_assoc, mul_comm]
    _ = 0 := by rw [aeval_mul, LinearMap.mul_apply, LinearMap.mem_ker.1 hv, LinearMap.map_zero]

Result:
case 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 * q))
p' q' : R[X]
hpq' : p' * p + q' * q = 1
h_eval₂_qpp' : ((aeval f) (q * (p * p'))) v = 0
h_eval₂_pqq' : ((aeval f) (p * (q * q'))) v = 0
⊢ ∃ y ∈ LinearMap.ker ((aeval f) p), ∃ z ∈ LinearMap.ker ((aeval f) q), y + z = v

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]
hpq : IsCoprime p q
v : M
hv : v ∈ LinearMap.ker ((aeval f) (p * q))
⊢ v ∈ LinearMap.ker ((aeval f) p) ⊔ LinearMap.ker ((aeval f) q)

Tactic:
rw [Submodule.mem_sup]

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]
hpq : IsCoprime p q
v : M
hv : v ∈ LinearMap.ker ((aeval f) (p * q))
⊢ ∃ y ∈ LinearMap.ker ((aeval f) p), ∃ z ∈ LinearMap.ker ((aeval f) q), y + z = v

Proof state:
case 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 * q))
p' q' : R[X]
hpq' : p' * p + q' * q = 1
h_eval₂_qpp' : ((aeval f) q * (aeval f) (p * p')) v = 0
h_eval₂_pqq' : ((aeval f) p * (aeval f) (q * q')) v = 0
⊢ ((aeval f) (p' * p)) v + ((aeval f) (q' * q)) v = v

Tactic:
simpa only [map_add, map_mul, aeval_one] using congr_arg (fun p : R[X] => aeval f p v) hpq'

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]
hpq : IsCoprime p q
⊢ LinearMap.ker ((aeval f) (p * q)) ≤ LinearMap.ker ((aeval f) p) ⊔ LinearMap.ker ((aeval f) 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]
hpq : IsCoprime p q
v : M
hv : v ∈ LinearMap.ker ((aeval f) (p * q))
⊢ v ∈ LinearMap.ker ((aeval f) p) ⊔ LinearMap.ker ((aeval f) 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]
hpq : IsCoprime p q
v : M
hv : v ∈ LinearMap.ker ((aeval f) (p * q))
⊢ ∃ y ∈ LinearMap.ker ((aeval f) p), ∃ z ∈ LinearMap.ker ((aeval f) q), y + z = v

Tactic:
rcases hpq with ⟨p', q', hpq'⟩

Result:
case 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 * q))
p' q' : R[X]
hpq' : p' * p + q' * q = 1
⊢ ∃ y ∈ LinearMap.ker ((aeval f) p), ∃ z ∈ LinearMap.ker ((aeval f) q), y + z = v

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 * q))
p' q' : R[X]
hpq' : p' * p + q' * q = 1
⊢ ((aeval f) (p' * (p * q))) v = 0

Tactic:
rw [aeval_mul, LinearMap.mul_apply, LinearMap.mem_ker.1 hv, 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 * q))
p' q' : R[X]
hpq' : p' * p + q' * q = 1
h_eval₂_qpp' : ((aeval f) (q * (p * p'))) v = 0
⊢ ((aeval f) (q' * (p * q))) v = 0

Tactic:
rw [aeval_mul, LinearMap.mul_apply, LinearMap.mem_ker.1 hv, 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]
hpq : IsCoprime p q
⊢ LinearMap.ker ((aeval f) p) ⊔ LinearMap.ker ((aeval f) q) = LinearMap.ker ((aeval f) (p * q))

Tactic:
apply le_antisymm sup_ker_aeval_le_ker_aeval_mul

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]
hpq : IsCoprime p q
⊢ LinearMap.ker ((aeval f) (p * q)) ≤ LinearMap.ker ((aeval f) p) ⊔ LinearMap.ker ((aeval f) 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 * q))
p' q' : R[X]
hpq' : p' * p + q' * q = 1
⊢ ((aeval f) (q * (p * p'))) v = ((aeval f) (p' * (p * q))) v

Tactic:
rw [mul_comm, mul_assoc, mul_comm, mul_assoc, mul_comm q p]

Result:
no goals