awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M →ₗ[R] M
v : M
⊢ (∀ (l : ℕ →₀ R),
      Eq.{w + 1} (α := M) (l.sum fun (i : ℕ) (a : R) ↦ HSMul.hSMul (β := M) a ((f ^ i : (a : M) → M) v : M)) 0 →
        l = 0) ↔
    ∀ (q : AddMonoidAlgebra R ℕ),
      Eq.{w + 1} (α := M)
          ({ toFinsupp := q : R[X] }.sum fun (n : ℕ) (b : R) ↦ HSMul.hSMul (β := M) b ((f ^ n : (a : M) → M) v : M)) 0 →
        q = 0

Tactic:
Iff.rfl

Premises used: Iff.rfl, Polynomial.sum, Polynomial.coeff, AddMonoidAlgebra, Polynomial.support
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M →ₗ[R] M
v : M
⊢ (∀ (l : ℕ →₀ R),
      Eq.{w + 1} (α := M) (l.sum fun (i : ℕ) (a : R) ↦ HSMul.hSMul (β := M) a ((f ^ i : (a : M) → M) v : M)) 0 →
        l = 0) ↔
    ∀ (q : AddMonoidAlgebra R ℕ),
      Eq.{w + 1} (α := M)
          ({ toFinsupp := q : R[X] }.sum fun (n : ℕ) (b : R) ↦ HSMul.hSMul (β := M) b ((f ^ n : (a : M) → M) v : M)) 0 →
        q = 0

Tactic:
exact Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M →ₗ[R] M
p q : R[X]
hpq : IsCoprime p q
rw :
  LE.le.{w} (α := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) p) ⊓
      LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q))
    ⊥
⊢ Disjoint.{w} (α := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) p))
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q))

Tactic:
rw [disjoint_iff_inf_le]

Premises used: disjoint_iff_inf_le
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M →ₗ[R] M
p q : R[X]
hpq : IsCoprime p q
v : M
hv :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) p) ⊓
      LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q))
    v
rcases : ∀ (p' q' : R[X]) (hpq' : p' * p + q' * q = 1), Membership.mem (γ := Submodule R M) ⊥ v
⊢ Membership.mem (γ := Submodule R M) ⊥ v

Tactic:
rcases hpq with ⟨p', q', hpq'⟩
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) p) ⊓
      LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q))
    v
p' q' : R[X]
hpq' : p' * p + q' * q = 1
⊢ Membership.mem (γ := Submodule R M) ⊥ v

Tactic:
simpa [LinearMap.mem_ker.1 (Submodule.mem_inf.1 hv).1,
    LinearMap.mem_ker.1 (Submodule.mem_inf.1 hv).2] using
    congr_arg (fun p : R[X] => aeval f p v) hpq'.symm

Premises used: Submodule.mem_inf, LinearMap.mem_ker, congr_arg, And.right, And.left, Iff.mp, Polynomial.aeval, Eq.symm, DFunLike.coe
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M →ₗ[R] M
p q : R[X]
hpq : IsCoprime p q
rw :
  LE.le.{w} (α := Submodule R M) ⊤
    (LinearMap.range (R := R) (M := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) p) ⊔
      LinearMap.range (R := R) (M := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q))
⊢ Eq.{w + 1} (α := Submodule R M)
    (LinearMap.range (R := R) (M := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) p) ⊔
      LinearMap.range (R := R) (M := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q))
    ⊤

Tactic:
rw [eq_top_iff]

Premises used: eq_top_iff
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M →ₗ[R] M
p q : R[X]
hpq : IsCoprime p q
v : M
_ :
  Membership.mem (γ := Submodule R M) ⊤ v →
    Membership.mem (γ := Submodule R M)
      (LinearMap.range (R := R) (M := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) p) ⊔
        LinearMap.range (R := R) (M := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q))
      v
⊢ Membership.mem (γ := Submodule R M) ⊤ v →
    Membership.mem (γ := Submodule R M)
      (LinearMap.range (R := R) (M := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) p) ⊔
        LinearMap.range (R := R) (M := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q))
      v

Tactic:
_
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M →ₗ[R] M
p q : R[X]
hpq : IsCoprime p q
v : M
h : Membership.mem (γ := Submodule R M) ⊤ v
rw :
  ∃ (y : M),
    Membership.mem (γ := Submodule R M)
        (LinearMap.range (R := R) (M := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) p)) y ∧
      ∃ (z : M),
        Membership.mem (γ := Submodule R M)
            (LinearMap.range (R := R) (M := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q)) z ∧
          y + z = v
⊢ Membership.mem (γ := Submodule R M)
    (LinearMap.range (R := R) (M := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) p) ⊔
      LinearMap.range (R := R) (M := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q))
    v

Tactic:
rw [Submodule.mem_sup]

Premises used: Submodule.mem_sup
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M →ₗ[R] M
p q : R[X]
hpq : IsCoprime p q
v : M
h : Membership.mem (γ := Submodule R M) ⊤ v
rcases :
  ∀ (p' q' : R[X]) (hpq' : p' * p + q' * q = 1),
    ∃ (y : M),
      Membership.mem (γ := Submodule R M)
          (LinearMap.range (R := R) (M := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) p)) y ∧
        ∃ (z : M),
          Membership.mem (γ := Submodule R M)
              (LinearMap.range (R := R) (M := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q)) z ∧
            y + z = v
⊢ ∃ (y : M),
    Membership.mem (γ := Submodule R M)
        (LinearMap.range (R := R) (M := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) p)) y ∧
      ∃ (z : M),
        Membership.mem (γ := Submodule R M)
            (LinearMap.range (R := R) (M := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q)) z ∧
          y + z = v

Tactic:
rcases hpq with ⟨p', q', hpq'⟩
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
h_1 : Membership.mem (γ := Submodule R M) ⊤ v
p' q' : R[X]
hpq' : p' * p + q' * q = 1
h :
  Membership.mem (α := M) (γ := Submodule R M)
      (LinearMap.range (R := R) (M := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) p))
      ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * p') : M →ₗ[R] M) : (a : M) → M) v : M) ∧
    ∃ (z : M),
      Membership.mem (γ := Submodule R M)
          (LinearMap.range (R := R) (M := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q)) z ∧
        HAdd.hAdd (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * p') : M →ₗ[R] M) : (a : M) → M) v : M) z = v
⊢ ∃ (y : M),
    Membership.mem (γ := Submodule R M)
        (LinearMap.range (R := R) (M := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) p)) y ∧
      ∃ (z : M),
        Membership.mem (γ := Submodule R M)
            (LinearMap.range (R := R) (M := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q)) z ∧
          y + z = v

Tactic:
use aeval f (p * p') v

Premises used: HMul.hMul, Polynomial.aeval, DFunLike.coe
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
h : Membership.mem (γ := Submodule R M) ⊤ v
p' q' : R[X]
hpq' : p' * p + q' * q = 1
⊢ Eq (α := M)
    ((((aeval f : (a : R[X]) → M →ₗ[R] M) p : M →ₗ[R] M) : (a : M) → M)
        ((((aeval f : (a : R[X]) → M →ₗ[R] M) p' : M →ₗ[R] M) : (a : M) → M) v : M) :
      M)
    ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * p') : M →ₗ[R] M) : (a : M) → M) v : M)

Tactic:
simp only [Module.End.mul_apply, aeval_mul]

Premises used: Polynomial.aeval_mul, Module.End.mul_apply
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
h : Membership.mem (γ := Submodule R M) ⊤ v
p' q' : R[X]
hpq' : p' * p + q' * q = 1
right :
  ∃ (z : M),
    Membership.mem (γ := Submodule R M)
        (LinearMap.range (R := R) (M := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q)) z ∧
      HAdd.hAdd (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * p') : M →ₗ[R] M) : (a : M) → M) v : M) z = v
⊢ Membership.mem (α := M) (γ := Submodule R M)
      (LinearMap.range (R := R) (M := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) p))
      ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * p') : M →ₗ[R] M) : (a : M) → M) v : M) ∧
    ∃ (z : M),
      Membership.mem (γ := Submodule R M)
          (LinearMap.range (R := R) (M := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q)) z ∧
        HAdd.hAdd (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * p') : M →ₗ[R] M) : (a : M) → M) v : M) z = v

Tactic:
use LinearMap.mem_range.2 ⟨aeval f p' v, by simp only [Module.End.mul_apply, aeval_mul]⟩

Premises used: Iff.mpr, LinearMap.mem_range, Exists.intro, Polynomial.aeval, DFunLike.coe
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
h_1 : Membership.mem (γ := Submodule R M) ⊤ v
p' q' : R[X]
hpq' : p' * p + q' * q = 1
h :
  Membership.mem (α := M) (γ := Submodule R M)
      (LinearMap.range (R := R) (M := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q))
      ((((aeval f : (a : R[X]) → M →ₗ[R] M) (q * q') : M →ₗ[R] M) : (a : M) → M) v : M) ∧
    HAdd.hAdd (α := M) (β := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * p') : M →ₗ[R] M) : (a : M) → M) v : M)
        ((((aeval f : (a : R[X]) → M →ₗ[R] M) (q * q') : M →ₗ[R] M) : (a : M) → M) v : M) =
      v
⊢ ∃ (z : M),
    Membership.mem (γ := Submodule R M)
        (LinearMap.range (R := R) (M := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q)) z ∧
      HAdd.hAdd (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * p') : M →ₗ[R] M) : (a : M) → M) v : M) z = v

Tactic:
use aeval f (q * q') v

Premises used: HMul.hMul, Polynomial.aeval, DFunLike.coe
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
h : Membership.mem (γ := Submodule R M) ⊤ v
p' q' : R[X]
hpq' : p' * p + q' * q = 1
⊢ Eq (α := M)
    ((((aeval f : (a : R[X]) → M →ₗ[R] M) q : M →ₗ[R] M) : (a : M) → M)
        ((((aeval f : (a : R[X]) → M →ₗ[R] M) q' : M →ₗ[R] M) : (a : M) → M) v : M) :
      M)
    ((((aeval f : (a : R[X]) → M →ₗ[R] M) (q * q') : M →ₗ[R] M) : (a : M) → M) v : M)

Tactic:
simp only [Module.End.mul_apply, aeval_mul]

Premises used: Polynomial.aeval_mul, Module.End.mul_apply
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
h : Membership.mem (γ := Submodule R M) ⊤ v
p' q' : R[X]
hpq' : p' * p + q' * q = 1
right :
  HAdd.hAdd (α := M) (β := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * p') : M →ₗ[R] M) : (a : M) → M) v : M)
      ((((aeval f : (a : R[X]) → M →ₗ[R] M) (q * q') : M →ₗ[R] M) : (a : M) → M) v : M) =
    v
⊢ Membership.mem (α := M) (γ := Submodule R M)
      (LinearMap.range (R := R) (M := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q))
      ((((aeval f : (a : R[X]) → M →ₗ[R] M) (q * q') : M →ₗ[R] M) : (a : M) → M) v : M) ∧
    HAdd.hAdd (α := M) (β := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * p') : M →ₗ[R] M) : (a : M) → M) v : M)
        ((((aeval f : (a : R[X]) → M →ₗ[R] M) (q * q') : M →ₗ[R] M) : (a : M) → M) v : M) =
      v

Tactic:
use LinearMap.mem_range.2 ⟨aeval f q' v, by simp only [Module.End.mul_apply, aeval_mul]⟩

Premises used: Iff.mpr, LinearMap.mem_range, Exists.intro, Polynomial.aeval, DFunLike.coe
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
h : Membership.mem (γ := Submodule R M) ⊤ v
p' q' : R[X]
hpq' : p' * p + q' * q = 1
⊢ HAdd.hAdd (α := M) (β := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * p') : M →ₗ[R] M) : (a : M) → M) v : M)
      ((((aeval f : (a : R[X]) → M →ₗ[R] M) (q * q') : M →ₗ[R] M) : (a : M) → M) v : M) =
    v

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

Premises used: Polynomial.aeval_one, congr_arg, mul_comm, Polynomial.aeval, DFunLike.coe, Polynomial.aeval_add
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) p) ⊔
      LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q))
    v
rcases :
  ∀ (x : M)
    (hx :
      Membership.mem (γ := Submodule R M)
        (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) p)) x)
    (y : M)
    (hy :
      Membership.mem (γ := Submodule R M)
        (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q)) y)
    (hxy : x + y = v),
    Membership.mem (γ := Submodule R M)
      (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q))) v
⊢ Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q))) v

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

Premises used: Iff.mp, Submodule.mem_sup
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) p) ⊔
      LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q))
    v
x : M
hx :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) p)) x
y : M
hy :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q)) y
hxy : x + y = v
rw : Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (q * p) : M →ₗ[R] M) : (a : M) → M) x : M) (0 : M)
rw₁ :
  Eq (α := M)
    ((HMul.hMul (α := M →ₗ[R] M) (β := M →ₗ[R] M) ((aeval f : (a : R[X]) → M →ₗ[R] M) q : M →ₗ[R] M)
            ((aeval f : (a : R[X]) → M →ₗ[R] M) p : M →ₗ[R] M) :
          (a : M) → M)
        x :
      M)
    (0 : M)
rw₂ :
  Eq (α := M)
    ((((aeval f : (a : R[X]) → M →ₗ[R] M) q : M →ₗ[R] M) : (a : M) → M)
        ((((aeval f : (a : R[X]) → M →ₗ[R] M) p : M →ₗ[R] M) : (a : M) → M) x : M) :
      M)
    (0 : M)
rw₃ : Eq.{w + 1} (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) q : M →ₗ[R] M) : (a : M) → M) 0 : M) (0 : M)
rw₄ rw₅ : Eq.{w + 1} (α := M) 0 0
⊢ Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) : (a : M) → M) x : M) (0 : M)

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

Premises used: map_zero, Polynomial.aeval_mul, LinearMap.mem_ker, Iff.mp, mul_comm, Module.End.mul_apply
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) p) ⊔
      LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q))
    v
x : M
hx :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) p)) x
y : M
hy :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q)) y
hxy : x + y = v
⊢ Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) : (a : M) → M) x : M) (0 : M)

Tactic:
have h_eval_x : aeval f (p * q) x = 0 := by
    rw [mul_comm, aeval_mul, Module.End.mul_apply, LinearMap.mem_ker.1 hx, map_zero]
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) p) ⊔
      LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q))
    v
x : M
hx :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) p)) x
y : M
hy :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q)) y
hxy : x + y = v
h_eval_x : Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) : (a : M) → M) x : M) (0 : M)
rw :
  Eq (α := M)
    ((HMul.hMul (α := M →ₗ[R] M) (β := M →ₗ[R] M) ((aeval f : (a : R[X]) → M →ₗ[R] M) p : M →ₗ[R] M)
            ((aeval f : (a : R[X]) → M →ₗ[R] M) q : M →ₗ[R] M) :
          (a : M) → M)
        y :
      M)
    (0 : M)
rw₁ :
  Eq (α := M)
    ((((aeval f : (a : R[X]) → M →ₗ[R] M) p : M →ₗ[R] M) : (a : M) → M)
        ((((aeval f : (a : R[X]) → M →ₗ[R] M) q : M →ₗ[R] M) : (a : M) → M) y : M) :
      M)
    (0 : M)
rw₂ : Eq.{w + 1} (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) p : M →ₗ[R] M) : (a : M) → M) 0 : M) (0 : M)
rw₃ rw₄ : Eq.{w + 1} (α := M) 0 0
⊢ Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) : (a : M) → M) y : M) (0 : M)

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

Premises used: map_zero, Polynomial.aeval_mul, LinearMap.mem_ker, Iff.mp, Module.End.mul_apply
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) p) ⊔
      LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q))
    v
x : M
hx :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) p)) x
y : M
hy :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q)) y
hxy : x + y = v
h_eval_x : Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) : (a : M) → M) x : M) (0 : M)
⊢ Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) : (a : M) → M) y : M) (0 : M)

Tactic:
have h_eval_y : aeval f (p * q) y = 0 := by
    rw [aeval_mul, Module.End.mul_apply, LinearMap.mem_ker.1 hy, map_zero]
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) p) ⊔
      LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q))
    v
x : M
hx :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) p)) x
y : M
hy :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q)) y
hxy : x + y = v
h_eval_x : Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) : (a : M) → M) x : M) (0 : M)
h_eval_y : Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) : (a : M) → M) y : M) (0 : M)
rw : Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) : (a : M) → M) v : M) (0 : M)
rw₁ : Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) : (a : M) → M) (x + y) : M) (0 : M)
rw₂ :
  HAdd.hAdd (α := M) (β := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) : (a : M) → M) x : M)
      ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) : (a : M) → M) y : M) =
    0
rw₃ :
  HAdd.hAdd (α := M) (β := M) (0 : M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) : (a : M) → M) y : M) =
    0
rw₄ : HAdd.hAdd (α := M) 0 0 = 0
rw₅ rw₆ : Eq.{w + 1} (α := M) 0 0
⊢ Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q))) v

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

Premises used: map_add, LinearMap.mem_ker, add_zero
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M →ₗ[R] M
p q : R[X]
hpq : IsCoprime p q
apply :
  LE.le.{w} (α := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q)))
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) p) ⊔
      LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q))
⊢ Eq.{w + 1} (α := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) p) ⊔
      LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q))
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q)))

Tactic:
apply le_antisymm sup_ker_aeval_le_ker_aeval_mul

Premises used: le_antisymm, Polynomial.sup_ker_aeval_le_ker_aeval_mul
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M →ₗ[R] M
p q : R[X]
hpq : IsCoprime p q
v : M
hv :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q))) v
rw :
  ∃ (y : M),
    Membership.mem (γ := Submodule R M)
        (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) p)) y ∧
      ∃ (z : M),
        Membership.mem (γ := Submodule R M)
            (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q)) z ∧
          y + z = v
⊢ Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) p) ⊔
      LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q))
    v

Tactic:
rw [Submodule.mem_sup]

Premises used: Submodule.mem_sup