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
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
rcases :
  ∀ (p' q' : R[X]) (hpq' : p' * p + q' * q = 1),
    ∃ (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
⊢ ∃ (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

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 * q))) v
p' q' : R[X]
hpq' : p' * p + q' * q = 1
rw :
  Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * p' * q) : M →ₗ[R] M) : (a : M) → M) v : M)
    ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p' * (p * q)) : M →ₗ[R] M) : (a : M) → M) v : M)
rw₁ :
  Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * (p' * q)) : M →ₗ[R] M) : (a : M) → M) v : M)
    ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p' * (p * q)) : M →ₗ[R] M) : (a : M) → M) v : M)
rw₂ :
  Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p' * q * p) : M →ₗ[R] M) : (a : M) → M) v : M)
    ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p' * (p * q)) : M →ₗ[R] M) : (a : M) → M) v : M)
rw₃ :
  Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p' * (q * p)) : M →ₗ[R] M) : (a : M) → M) v : M)
    ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p' * (p * q)) : M →ₗ[R] M) : (a : M) → M) v : M)
rw₄ rw₅ :
  Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p' * (p * q)) : M →ₗ[R] M) : (a : M) → M) v : M)
    ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p' * (p * q)) : M →ₗ[R] M) : (a : M) → M) v : M)
⊢ Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (q * (p * p')) : M →ₗ[R] M) : (a : M) → M) v : M)
    ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p' * (p * q)) : M →ₗ[R] M) : (a : M) → M) v : M)

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

Premises used: mul_assoc, mul_comm
-- 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 * q))) v
p' q' : R[X]
hpq' : p' * p + q' * q = 1
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) (p * q) : M →ₗ[R] M) :
          (a : M) → M)
        v :
      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) (p * q) : M →ₗ[R] M) : (a : M) → M) v : 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' * (p * q)) : M →ₗ[R] M) : (a : M) → M) v : M) (0 : M)

Tactic:
rw [aeval_mul, Module.End.mul_apply, LinearMap.mem_ker.1 hv, 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 * q))) v
p' q' : R[X]
hpq' : p' * p + q' * q = 1
⊢ Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (q * (p * p')) : M →ₗ[R] M) : (a : M) → M) v : M) (0 : M)

Tactic:
have h_eval₂_qpp' :=
    calc
      aeval f (q * (p * p')) v = aeval f (p' * (p * q)) v := by
        rw [mul_comm, mul_assoc, mul_comm, mul_assoc, mul_comm q p]
      _ = 0 := by rw [aeval_mul, Module.End.mul_apply, LinearMap.mem_ker.1 hv, 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 * q))) v
p' q' : R[X]
hpq' : p' * p + q' * q = 1
h_eval₂_qpp' :
  Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (q * (p * p')) : M →ₗ[R] M) : (a : M) → M) v : M) (0 : M)
rw :
  Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q * q') : M →ₗ[R] M) : (a : M) → M) v : M)
    ((((aeval f : (a : R[X]) → M →ₗ[R] M) (q' * (p * q)) : M →ₗ[R] M) : (a : M) → M) v : M)
rw₁ rw₂ :
  Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (q' * (p * q)) : M →ₗ[R] M) : (a : M) → M) v : M)
    ((((aeval f : (a : R[X]) → M →ₗ[R] M) (q' * (p * q)) : M →ₗ[R] M) : (a : M) → M) v : M)
⊢ Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * (q * q')) : M →ₗ[R] M) : (a : M) → M) v : M)
    ((((aeval f : (a : R[X]) → M →ₗ[R] M) (q' * (p * q)) : M →ₗ[R] M) : (a : M) → M) v : M)

Tactic:
rw [← mul_assoc, mul_comm]

Premises used: mul_assoc, mul_comm
-- 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 * q))) v
p' q' : R[X]
hpq' : p' * p + q' * q = 1
h_eval₂_qpp' :
  Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (q * (p * p')) : M →ₗ[R] M) : (a : M) → M) v : 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 * q) : M →ₗ[R] M) :
          (a : M) → M)
        v :
      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 * q) : M →ₗ[R] M) : (a : M) → M) v : 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) (q' * (p * q)) : M →ₗ[R] M) : (a : M) → M) v : M) (0 : M)

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

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, Module.End.mul_apply, LinearMap.mem_ker.1 hv, 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 * q))) v
p' q' : R[X]
hpq' : p' * p + q' * q = 1
h_eval₂_qpp' :
  Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (q * (p * p')) : M →ₗ[R] M) : (a : M) → M) v : M) (0 : M)
h_eval₂_pqq' :
  Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * (q * q')) : M →ₗ[R] M) : (a : M) → M) v : M) (0 : M)
⊢ 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 * p') : M →ₗ[R] M) :
          (a : M) → M)
        v :
      M)
    (0 : M)

Tactic:
rw [aeval_mul] at h_eval₂_qpp' h_eval₂_pqq'

Premises used: Polynomial.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]
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
p' q' : R[X]
hpq' : p' * p + q' * q = 1
h_eval₂_qpp' :
  Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (q * (p * p')) : M →ₗ[R] M) : (a : M) → M) v : M) (0 : M)
h_eval₂_pqq' :
  Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * (q * q')) : M →ₗ[R] M) : (a : M) → M) v : M) (0 : M)
h_eval₂_qpp'₁ :
  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 * p') : M →ₗ[R] M) :
          (a : M) → M)
        v :
      M)
    (0 : M)
⊢ 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 * q') : M →ₗ[R] M) :
          (a : M) → M)
        v :
      M)
    (0 : M)

Tactic:
rw [aeval_mul] at h_eval₂_qpp' h_eval₂_pqq'

Premises used: Polynomial.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]
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
p' q' : R[X]
hpq' : p' * p + q' * q = 1
h_eval₂_qpp' :
  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 * p') : M →ₗ[R] M) :
          (a : M) → M)
        v :
      M)
    (0 : M)
h_eval₂_pqq' :
  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 * q') : M →ₗ[R] M) :
          (a : M) → M)
        v :
      M)
    (0 : M)
⊢ ∃ (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

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

Premises used: HMul.hMul, LinearMap.mem_ker, And.intro, Exists.intro, Iff.mp, 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
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
p' q' : R[X]
hpq' : p' * p + q' * q = 1
h_eval₂_qpp' :
  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 * p') : M →ₗ[R] M) :
          (a : M) → M)
        v :
      M)
    (0 : M)
h_eval₂_pqq' :
  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 * q') : M →ₗ[R] M) :
          (a : M) → M)
        v :
      M)
    (0 : M)
f₁ :
  HAdd.hAdd (α := M) (β := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (q * q') : M →ₗ[R] M) : (a : M) → M) v : M)
      ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * p') : M →ₗ[R] M) : (a : M) → M) v : M) =
    v
⊢ ∃ (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

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', ?_⟩
-- 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 * q))) v
p' q' : R[X]
hpq' : p' * p + q' * q = 1
h_eval₂_qpp' :
  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 * p') : M →ₗ[R] M) :
          (a : M) → M)
        v :
      M)
    (0 : M)
h_eval₂_pqq' :
  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 * q') : M →ₗ[R] M) :
          (a : M) → M)
        v :
      M)
    (0 : M)
rw :
  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
⊢ HAdd.hAdd (α := M) (β := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (q * q') : M →ₗ[R] M) : (a : M) → M) v : M)
      ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * p') : M →ₗ[R] M) : (a : M) → M) v : M) =
    v

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

Premises used: add_comm, mul_comm
-- 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 * q))) v
p' q' : R[X]
hpq' : p' * p + q' * q = 1
h_eval₂_qpp' :
  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 * p') : M →ₗ[R] M) :
          (a : M) → M)
        v :
      M)
    (0 : M)
h_eval₂_pqq' :
  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 * q') : M →ₗ[R] M) :
          (a : M) → M)
        v :
      M)
    (0 : 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:
simpa only [map_add, map_mul, aeval_one] using congr_arg (fun p : R[X] => aeval f p v) hpq'

Premises used: Polynomial.aeval_one, map_add, congr_arg, map_mul, Polynomial.aeval, DFunLike.coe
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
σ : Type v
R : Type u_2
inst : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
rw :
  natDegree (R := R)
      ((AddMonoidAlgebra.coeff F).sum fun (s : σ →₀ ℕ) (a : R) ↦
        HMul.hMul (α := R[X]) (β := R[X]) ((algebraMap R R[X] : (a : R) → R[X]) a : R[X])
          (s.prod fun (n : σ) (e : ℕ) ↦ f n ^ e : R[X])) ≤
    m * n
⊢ natDegree.{u_2} (R := R) ((aeval f : (a : MvPolynomial σ R) → R[X]) F) ≤ m * n

Tactic:
rw [MvPolynomial.aeval_def, MvPolynomial.eval₂]

Premises used: MvPolynomial.eval₂, MvPolynomial.aeval_def
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
σ : Type v
R : Type u_2
inst : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
apply :
  fold max 0
      (Function.comp.{v + 1, u_2 + 1, 1} (β := R[X]) natDegree fun (i : σ →₀ ℕ) ↦
        (fun (s : σ →₀ ℕ) (a : R) ↦
            HMul.hMul (α := R[X]) (β := R[X]) ((algebraMap R R[X] : (a : R) → R[X]) a : R[X])
              (s.prod fun (n : σ) (e : ℕ) ↦ f n ^ e : R[X]))
          i ((AddMonoidAlgebra.coeff F : (a : σ →₀ ℕ) → R) i))
      (AddMonoidAlgebra.coeff F).support ≤
    m * n
⊢ natDegree (R := R)
      ((AddMonoidAlgebra.coeff F).sum fun (s : σ →₀ ℕ) (a : R) ↦
        HMul.hMul (α := R[X]) (β := R[X]) ((algebraMap R R[X] : (a : R) → R[X]) a : R[X])
          (s.prod fun (n : σ) (e : ℕ) ↦ f n ^ e : R[X])) ≤
    m * n

Tactic:
apply (Polynomial.natDegree_sum_le _ _).trans

Premises used: Polynomial.natDegree_sum_le, LE.le.trans
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
σ : Type v
R : Type u_2
inst : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
a :
  ∀ b ∈ (AddMonoidAlgebra.coeff F).support,
    Function.comp.{v + 1, u_2 + 1, 1} (β := R[X]) natDegree
        (fun (i : σ →₀ ℕ) ↦
          (fun (s : σ →₀ ℕ) (a : R) ↦
              HMul.hMul (α := R[X]) (β := R[X]) ((algebraMap R R[X] : (a : R) → R[X]) a : R[X])
                (s.prod fun (n : σ) (e : ℕ) ↦ f n ^ e : R[X]))
            i ((AddMonoidAlgebra.coeff F : (a : σ →₀ ℕ) → R) i))
        b ≤
      m * n
⊢ fold max 0
      (Function.comp.{v + 1, u_2 + 1, 1} (β := R[X]) natDegree fun (i : σ →₀ ℕ) ↦
        (fun (s : σ →₀ ℕ) (a : R) ↦
            HMul.hMul (α := R[X]) (β := R[X]) ((algebraMap R R[X] : (a : R) → R[X]) a : R[X])
              (s.prod fun (n : σ) (e : ℕ) ↦ f n ^ e : R[X]))
          i ((AddMonoidAlgebra.coeff F : (a : σ →₀ ℕ) → R) i))
      (AddMonoidAlgebra.coeff F).support ≤
    m * n

Tactic:
apply Finset.sup_le

Premises used: Finset.sup_le
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
σ : Type v
R : Type u_2
inst : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
d : σ →₀ ℕ
hd : d ∈ (AddMonoidAlgebra.coeff F).support
a :
  (HMul.hMul (α := R[X]) (β := R[X])
        ((Polynomial.C : (a : R) → R[X]) ((AddMonoidAlgebra.coeff F : (a : σ →₀ ℕ) → R) d) : R[X])
        (d.prod fun (n : σ) (e : ℕ) ↦ f n ^ e : R[X])).natDegree ≤
    m * n
⊢ Function.comp.{v + 1, u_2 + 1, 1} (β := R[X]) natDegree
      (fun (i : σ →₀ ℕ) ↦
        (fun (s : σ →₀ ℕ) (a : R) ↦
            HMul.hMul (α := R[X]) (β := R[X]) ((algebraMap R R[X] : (a : R) → R[X]) a : R[X])
              (s.prod fun (n : σ) (e : ℕ) ↦ f n ^ e : R[X]))
          i ((AddMonoidAlgebra.coeff F : (a : σ →₀ ℕ) → R) i))
      d ≤
    m * n

Tactic:
simp_rw [Function.comp_apply, ← C_eq_algebraMap]

Premises used: Polynomial.C_eq_algebraMap, Function.comp_apply
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
σ : Type v
R : Type u_2
inst : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
d : σ →₀ ℕ
hd : d ∈ (AddMonoidAlgebra.coeff F).support
a : natDegree.{u_2} (R := R) (d.prod fun (n : σ) (e : ℕ) ↦ f n ^ e) ≤ m * n
⊢ (HMul.hMul (α := R[X]) (β := R[X])
        ((Polynomial.C : (a : R) → R[X]) ((AddMonoidAlgebra.coeff F : (a : σ →₀ ℕ) → R) d) : R[X])
        (d.prod fun (n : σ) (e : ℕ) ↦ f n ^ e : R[X])).natDegree ≤
    m * n

Tactic:
apply (Polynomial.natDegree_C_mul_le _ _).trans

Premises used: Polynomial.natDegree_C_mul_le, LE.le.trans
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
σ : Type v
R : Type u_2
inst : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
d : σ →₀ ℕ
hd : d ∈ (AddMonoidAlgebra.coeff F).support
a : ∑ i ∈ d.support, natDegree.{u_2} (R := R) ((fun (n : σ) (e : ℕ) ↦ f n ^ e) i ((d : (a : σ) → ℕ) i)) ≤ m * n
⊢ natDegree.{u_2} (R := R) (d.prod fun (n : σ) (e : ℕ) ↦ f n ^ e) ≤ m * n

Tactic:
apply (Polynomial.natDegree_prod_le _ _).trans

Premises used: Polynomial.natDegree_prod_le, LE.le.trans
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
σ : Type v
R : Type u_2
inst : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
d : σ →₀ ℕ
hd : d ∈ (AddMonoidAlgebra.coeff F).support
rw : (∑ i ∈ d.support, (d : (a : σ) → ℕ) i) * n ≤ m * n
⊢ ∑ i ∈ d.support, HMul.hMul (α := ℕ) ((d : (a : σ) → ℕ) i : ℕ) n ≤ m * n

Tactic:
rw [← Finset.sum_mul]

Premises used: Finset.sum_mul
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
σ : Type v
R : Type u_2
inst : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
d : σ →₀ ℕ
hd : d ∈ (AddMonoidAlgebra.coeff F).support
apply : ∑ i ∈ d.support, (d : (a : σ) → ℕ) i ≤ F.totalDegree
⊢ (∑ i ∈ d.support, (d : (a : σ) → ℕ) i) * n ≤ m * n

Tactic:
apply mul_le_mul' (.trans _ hF) le_rfl

Premises used: le_rfl, LE.le.trans, mul_le_mul'
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
σ : Type v
R : Type u_2
inst : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
d : σ →₀ ℕ
hd : d ∈ (AddMonoidAlgebra.coeff F).support
⊢ LE.le (α := ℕ) (∑ i ∈ d.support, (d : (a : σ) → ℕ) i) (F.support.sup fun (s : σ →₀ ℕ) ↦ s.sum fun (x : σ) (e : ℕ) ↦ e)

Tactic:
Finset.le_sup_of_le hd le_rfl

Premises used: le_rfl, Finset.le_sup_of_le
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
σ : Type v
R : Type u_2
inst : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
d : σ →₀ ℕ
hd : d ∈ (AddMonoidAlgebra.coeff F).support
⊢ LE.le (α := ℕ) (∑ i ∈ d.support, (d : (a : σ) → ℕ) i) (F.support.sup fun (s : σ →₀ ℕ) ↦ s.sum fun (x : σ) (e : ℕ) ↦ e)

Tactic:
exact Finset.le_sup_of_le hd le_rfl

Premises used: le_rfl, Finset.le_sup_of_le
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
σ : Type v
R : Type u_2
inst : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
d : σ →₀ ℕ
hd : d ∈ (AddMonoidAlgebra.coeff F).support
⊢ ∑ i ∈ d.support, HMul.hMul (α := ℕ) ((d : (a : σ) → ℕ) i : ℕ) n ≤ m * n

Tactic:
have : ∑ i ∈ d.support, (d i) * n ≤ m * n := by
    rw [← Finset.sum_mul]
    apply mul_le_mul' (.trans _ hF) le_rfl
    rw [MvPolynomial.totalDegree]
    exact Finset.le_sup_of_le hd le_rfl
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
σ : Type v
R : Type u_2
inst : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
d : σ →₀ ℕ
hd : d ∈ (AddMonoidAlgebra.coeff F).support
this : ∑ i ∈ d.support, HMul.hMul (α := ℕ) ((d : (a : σ) → ℕ) i : ℕ) n ≤ m * n
apply :
  ∀ i ∈ d.support,
    natDegree.{u_2} (R := R) ((fun (n : σ) (e : ℕ) ↦ f n ^ e) i ((d : (a : σ) → ℕ) i)) ≤
      HMul.hMul (α := ℕ) ((d : (a : σ) → ℕ) i : ℕ) n
⊢ ∑ i ∈ d.support, natDegree.{u_2} (R := R) ((fun (n : σ) (e : ℕ) ↦ f n ^ e) i ((d : (a : σ) → ℕ) i)) ≤ m * n

Tactic:
apply (Finset.sum_le_sum _).trans this

Premises used: Finset.sum_le_sum, LE.le.trans