awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Module R S
M : Submodule R S
x : S
⊢ Membership.mem (α := MvPolynomial σ S) (coeffsIn σ M) ((C : (a : S) → MvPolynomial σ S) x : MvPolynomial σ S) ↔ x ∈ M

Tactic:
simpa using monomial_mem_coeffsIn (i := 0)

Premises used: MvPolynomial.monomial_mem_coeffsIn
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Module R S
M : Submodule R S
⊢ 1 ∈ coeffsIn σ M ↔ 1 ∈ M

Tactic:
simpa using C_mem_coeffsIn (x := (1 : S))

Premises used: MvPolynomial.C_mem_coeffsIn
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Module R S
M : Submodule R S
p : MvPolynomial σ S
i : σ →₀ ℕ
simp : (∀ (i_1 : σ →₀ ℕ), (if i ≤ i_1 then coeff (i_1 - i) p * 1 else 0) ∈ M) ↔ ∀ (i : σ →₀ ℕ), coeff i p ∈ M
⊢ p * (monomial i : (a : S) → MvPolynomial σ S) 1 ∈ coeffsIn σ M ↔ p ∈ coeffsIn σ M

Tactic:
simp only [mem_coeffsIn, coeff_mul_monomial']

Premises used: MvPolynomial.mem_coeffsIn, MvPolynomial.coeff_mul_monomial'
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Module R S
M : Submodule R S
p : MvPolynomial σ S
i : σ →₀ ℕ
mp : (∀ (i_1 : σ →₀ ℕ), (if i ≤ i_1 then coeff (i_1 - i) p * 1 else 0) ∈ M) → ∀ (i : σ →₀ ℕ), coeff i p ∈ M
mpr : (∀ (i : σ →₀ ℕ), coeff i p ∈ M) → ∀ (i_1 : σ →₀ ℕ), (if i ≤ i_1 then coeff (i_1 - i) p * 1 else 0) ∈ M
⊢ (∀ (i_1 : σ →₀ ℕ), (if i ≤ i_1 then coeff (i_1 - i) p * 1 else 0) ∈ M) ↔ ∀ (i : σ →₀ ℕ), coeff i p ∈ M

Tactic:
constructor
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Module R S
M : Submodule R S
p : MvPolynomial σ S
i : σ →₀ ℕ
hp : ∀ (i_1 : σ →₀ ℕ), (if i ≤ i_1 then coeff (i_1 - i) p * 1 else 0) ∈ M
j : σ →₀ ℕ
⊢ coeff j p ∈ M

Tactic:
simpa using hp (j + i)

Premises used: HAdd.hAdd
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Module R S
M : Submodule R S
p : MvPolynomial σ S
i_1 : σ →₀ ℕ
hp : ∀ (i : σ →₀ ℕ), coeff i p ∈ M
i : σ →₀ ℕ
mpr : i_1 ≤ i → coeff (i - i_1) p * 1 ∈ M
mpr₁ : ¬i_1 ≤ i → 0 ∈ M
⊢ (if i_1 ≤ i then coeff (i - i_1) p * 1 else 0) ∈ M

Tactic:
split
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Module R S
M : Submodule R S
p : MvPolynomial σ S
i_1 : σ →₀ ℕ
hp : ∀ (i : σ →₀ ℕ), coeff i p ∈ M
i : σ →₀ ℕ
h : i_1 ≤ i
⊢ coeff (i - i_1) p * 1 ∈ M

Tactic:
simp [hp]
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Module R S
M : Submodule R S
p : MvPolynomial σ S
i_1 : σ →₀ ℕ
hp : ∀ (i : σ →₀ ℕ), coeff i p ∈ M
i : σ →₀ ℕ
h : ¬i_1 ≤ i
⊢ 0 ∈ M

Tactic:
simp [hp]
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Module R S
M : Submodule R S
p : MvPolynomial σ S
i : σ →₀ ℕ
simp : (∀ (i_1 : σ →₀ ℕ), (if i ≤ i_1 then coeff (i_1 - i) p * 1 else 0) ∈ M) ↔ ∀ (i : σ →₀ ℕ), coeff i p ∈ M
mp : (∀ (i_1 : σ →₀ ℕ), (if i ≤ i_1 then coeff (i_1 - i) p * 1 else 0) ∈ M) → ∀ (i : σ →₀ ℕ), coeff i p ∈ M
mpr mpr₁ : (∀ (i : σ →₀ ℕ), coeff i p ∈ M) → ∀ (i_1 : σ →₀ ℕ), (if i ≤ i_1 then coeff (i_1 - i) p * 1 else 0) ∈ M
⊢ p * (monomial i : (a : S) → MvPolynomial σ S) 1 ∈ coeffsIn σ M ↔ p ∈ coeffsIn σ M

Tactic:
classical
  simp only [mem_coeffsIn, coeff_mul_monomial']
  constructor
  · rintro hp j
    simpa using hp (j + i)
  · rintro hp i
    split <;> simp [hp]

Premises used: MvPolynomial.mem_coeffsIn, MvPolynomial.coeff_mul_monomial'
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Module R S
M : Submodule R S
p : MvPolynomial σ S
i : σ →₀ ℕ
⊢ (monomial i : (a : S) → MvPolynomial σ S) 1 * p ∈ coeffsIn σ M ↔ p ∈ coeffsIn σ M

Tactic:
simp [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Module R S
M : Submodule R S
p : MvPolynomial σ S
s : σ
⊢ p * X s ∈ coeffsIn σ M ↔ p ∈ coeffsIn σ M

Tactic:
simpa [-mul_monomial_mem_coeffsIn] using mul_monomial_mem_coeffsIn (i := .single s 1)

Premises used: MvPolynomial.mul_monomial_mem_coeffsIn
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Module R S
M : Submodule R S
p : MvPolynomial σ S
s : σ
⊢ X s * p ∈ coeffsIn σ M ↔ p ∈ coeffsIn σ M

Tactic:
simp [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Module R S
M : Submodule R S
⊢ coeffsIn σ M =
    Submodule.span R {x : MvPolynomial σ S | ∃ m ∈ M, ∃ (i : σ →₀ ℕ), (monomial i : (a : S) → MvPolynomial σ S) m = x}

Tactic:
le_antisymm ?_ <| Submodule.span_le.2 ?_

Premises used: Iff.mpr, le_antisymm, Submodule.span_le
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Module R S
M : Submodule R S
refine_1 :
  coeffsIn σ M ≤
    Submodule.span R {x : MvPolynomial σ S | ∃ m ∈ M, ∃ (i : σ →₀ ℕ), (monomial i : (a : S) → MvPolynomial σ S) m = x}
refine_2 :
  {x : MvPolynomial σ S | ∃ m ∈ M, ∃ (i : σ →₀ ℕ), (monomial i : (a : S) → MvPolynomial σ S) m = x} ⊆
    (↑(coeffsIn σ M) : Set (MvPolynomial σ S))
⊢ coeffsIn σ M =
    Submodule.span R {x : MvPolynomial σ S | ∃ m ∈ M, ∃ (i : σ →₀ ℕ), (monomial i : (a : S) → MvPolynomial σ S) m = x}

Tactic:
refine le_antisymm ?_ <| Submodule.span_le.2 ?_

Premises used: Iff.mpr, le_antisymm, Submodule.span_le
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Module R S
M : Submodule R S
p : MvPolynomial σ S
hp : p ∈ coeffsIn σ M
refine_1 :
  Membership.mem (γ := Submodule R (MvPolynomial σ S))
    (Submodule.span R {x : MvPolynomial σ S | ∃ m ∈ M, ∃ (i : σ →₀ ℕ), (monomial i : (a : S) → MvPolynomial σ S) m = x})
    (∑ v ∈ p.support, (monomial v : (a : S) → MvPolynomial σ S) (coeff v p))
⊢ Membership.mem (γ := Submodule R (MvPolynomial σ S))
    (Submodule.span R {x : MvPolynomial σ S | ∃ m ∈ M, ∃ (i : σ →₀ ℕ), (monomial i : (a : S) → MvPolynomial σ S) m = x})
    p

Tactic:
rw [p.as_sum]

Premises used: MvPolynomial.as_sum
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Module R S
M : Submodule R S
p : MvPolynomial σ S
hp : p ∈ coeffsIn σ M
⊢ Membership.mem (γ := Submodule R (MvPolynomial σ S))
    (Submodule.span R {x : MvPolynomial σ S | ∃ m ∈ M, ∃ (i : σ →₀ ℕ), (monomial i : (a : S) → MvPolynomial σ S) m = x})
    (∑ v ∈ p.support, (monomial v : (a : S) → MvPolynomial σ S) (coeff v p))

Tactic:
sum_mem fun i hi ↦ Submodule.subset_span ⟨_, hp i, _, rfl⟩

Premises used: Set.Mem, MvPolynomial.coeff, And.intro, Exists.intro, Submodule.subset_span, sum_mem, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Module R S
M : Submodule R S
p : MvPolynomial σ S
hp : p ∈ coeffsIn σ M
⊢ Membership.mem (γ := Submodule R (MvPolynomial σ S))
    (Submodule.span R {x : MvPolynomial σ S | ∃ m ∈ M, ∃ (i : σ →₀ ℕ), (monomial i : (a : S) → MvPolynomial σ S) m = x})
    (∑ v ∈ p.support, (monomial v : (a : S) → MvPolynomial σ S) (coeff v p))

Tactic:
exact sum_mem fun i hi ↦ Submodule.subset_span ⟨_, hp i, _, rfl⟩
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Module R S
M : Submodule R S
m : S
hm : m ∈ M
s i : σ →₀ ℕ
refine_2 : (if s = i then m else 0) ∈ M
⊢ coeff i ((monomial s : (a : S) → MvPolynomial σ S) m) ∈ M

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Module R S
M : Submodule R S
m : S
hm : m ∈ M
s i : σ →₀ ℕ
refine_2 : s = i → m ∈ M
refine_2₁ : ¬s = i → 0 ∈ M
⊢ (if s = i then m else 0) ∈ M

Tactic:
split
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Module R S
M : Submodule R S
m : S
hm : m ∈ M
s i : σ →₀ ℕ
h : s = i
⊢ m ∈ M

Tactic:
simp [hm]
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Module R S
M : Submodule R S
m : S
hm : m ∈ M
s i : σ →₀ ℕ
h : ¬s = i
⊢ 0 ∈ M

Tactic:
simp [hm]
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Module R S
M : Submodule R S
refine_1 :
  coeffsIn σ M ≤
    Submodule.span R {x : MvPolynomial σ S | ∃ m ∈ M, ∃ (i : σ →₀ ℕ), (monomial i : (a : S) → MvPolynomial σ S) m = x}
refine_2 refine_2₁ :
  {x : MvPolynomial σ S | ∃ m ∈ M, ∃ (i : σ →₀ ℕ), (monomial i : (a : S) → MvPolynomial σ S) m = x} ⊆
    (↑(coeffsIn σ M) : Set (MvPolynomial σ S))
⊢ coeffsIn σ M =
    Submodule.span R {x : MvPolynomial σ S | ∃ m ∈ M, ∃ (i : σ →₀ ℕ), (monomial i : (a : S) → MvPolynomial σ S) m = x}

Tactic:
classical
  refine le_antisymm ?_ <| Submodule.span_le.2 ?_
  · rintro p hp
    rw [p.as_sum]
    exact sum_mem fun i hi ↦ Submodule.subset_span ⟨_, hp i, _, rfl⟩
  · rintro _ ⟨m, hm, s, n, rfl⟩ i
    simp
    split <;> simp [hm]

Premises used: Iff.mpr, le_antisymm, Submodule.span_le, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Module R S
M : Submodule R S
N : Submodule R (MvPolynomial σ S)
⊢ coeffsIn σ M ≤ N ↔
    ∀ m ∈ M,
      ∀ (i : σ →₀ ℕ),
        Membership.mem (α := MvPolynomial σ S) N ((monomial i : (a : S) → MvPolynomial σ S) m : MvPolynomial σ S)

Tactic:
simp [coeffsIn_eq_span_monomial, Submodule.span_le, Set.subset_def,
    forall_comm (α := MvPolynomial σ S)]

Premises used: Set.subset_def, forall_comm, MvPolynomial.coeffsIn_eq_span_monomial, Submodule.span_le
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Module R S
M : Submodule R S
p : MvPolynomial σ S
simp : (∀ (i : σ →₀ ℕ), coeff i p ∈ M) ↔ (↑p.support : Set (σ →₀ ℕ)) ⊆ (fun (m : σ →₀ ℕ) ↦ coeff m p) ⁻¹' (↑M : Set S)
⊢ p ∈ coeffsIn σ M ↔ (↑p.coeffs : Set S) ⊆ (↑M : Set S)

Tactic:
simp only [mem_coeffsIn, coeffs, Finset.coe_image, image_subset_iff]

Premises used: MvPolynomial.coeffs, Finset.coe_image, MvPolynomial.mem_coeffsIn, Set.image_subset_iff
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Module R S
M : Submodule R S
p : MvPolynomial σ S
⊢ (∀ (i : σ →₀ ℕ), coeff i p ∈ M) ↔ (↑p.support : Set (σ →₀ ℕ)) ⊆ (fun (m : σ →₀ ℕ) ↦ coeff m p) ⁻¹' (↑M : Set S)

Tactic:
⟨fun h x _ ↦ h x, fun h i ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Module R S
M : Submodule R S
p : MvPolynomial σ S
refine :
  ∀ (h : (↑p.support : Set (σ →₀ ℕ)) ⊆ (fun (m : σ →₀ ℕ) ↦ coeff m p) ⁻¹' (↑M : Set S)) (i : σ →₀ ℕ), coeff i p ∈ M
⊢ (∀ (i : σ →₀ ℕ), coeff i p ∈ M) ↔ (↑p.support : Set (σ →₀ ℕ)) ⊆ (fun (m : σ →₀ ℕ) ↦ coeff m p) ⁻¹' (↑M : Set S)

Tactic:
refine ⟨fun h x _ ↦ h x, fun h i ↦ ?_⟩
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Module R S
M : Submodule R S
p : MvPolynomial σ S
h : (↑p.support : Set (σ →₀ ℕ)) ⊆ (fun (m : σ →₀ ℕ) ↦ coeff m p) ⁻¹' (↑M : Set S)
i : σ →₀ ℕ
pos : ∀ (hp : i ∈ p.support), coeff i p ∈ M
neg : ∀ (hp : i ∉ p.support), coeff i p ∈ M
⊢ coeff i p ∈ M

Tactic:
by_cases hp : i ∈ p.support

Premises used: MvPolynomial.support
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Module R S
M : Submodule R S
p : MvPolynomial σ S
h : (↑p.support : Set (σ →₀ ℕ)) ⊆ (fun (m : σ →₀ ℕ) ↦ coeff m p) ⁻¹' (↑M : Set S)
i : σ →₀ ℕ
hp : i ∈ p.support
⊢ coeff i p ∈ M

Tactic:
h hp

Premises used: Set.Mem, setOf, Set.preimage
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Module R S
M : Submodule R S
p : MvPolynomial σ S
h : (↑p.support : Set (σ →₀ ℕ)) ⊆ (fun (m : σ →₀ ℕ) ↦ coeff m p) ⁻¹' (↑M : Set S)
i : σ →₀ ℕ
hp : i ∈ p.support
⊢ coeff i p ∈ M

Tactic:
exact h hp
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Module R S
M : Submodule R S
p : MvPolynomial σ S
h : (↑p.support : Set (σ →₀ ℕ)) ⊆ (fun (m : σ →₀ ℕ) ↦ coeff m p) ⁻¹' (↑M : Set S)
i : σ →₀ ℕ
hp : i ∉ p.support
⊢ 0 ∈ M

Tactic:
M.zero_mem

Premises used: Submodule.zero_mem
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Module R S
M : Submodule R S
p : MvPolynomial σ S
h : (↑p.support : Set (σ →₀ ℕ)) ⊆ (fun (m : σ →₀ ℕ) ↦ coeff m p) ⁻¹' (↑M : Set S)
i : σ →₀ ℕ
hp : i ∉ p.support
h₁ : coeff i p = 0
⊢ coeff i p ∈ M

Tactic:
convert! M.zero_mem

Premises used: Submodule.zero_mem
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Module R S
M : Submodule R S
p : MvPolynomial σ S
h : (↑p.support : Set (σ →₀ ℕ)) ⊆ (fun (m : σ →₀ ℕ) ↦ coeff m p) ⁻¹' (↑M : Set S)
i : σ →₀ ℕ
hp : i ∉ p.support
⊢ coeff i p = 0

Tactic:
simpa using hp
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
M N : Submodule R S
⊢ coeffsIn σ (M * N) = coeffsIn σ M * coeffsIn σ N

Tactic:
le_antisymm (coeffsIn_le.2 ?_) ?_

Premises used: Iff.mpr, le_antisymm, MvPolynomial.coeffsIn_le
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
M N : Submodule R S
refine_1 :
  ∀ m ∈ M * N,
    ∀ (i : σ →₀ ℕ),
      Membership.mem (α := MvPolynomial σ S) (coeffsIn σ M * coeffsIn σ N)
        ((monomial i : (a : S) → MvPolynomial σ S) m : MvPolynomial σ S)
refine_2 : coeffsIn σ M * coeffsIn σ N ≤ coeffsIn σ (M * N)
⊢ coeffsIn σ (M * N) = coeffsIn σ M * coeffsIn σ N

Tactic:
refine le_antisymm (coeffsIn_le.2 ?_) ?_

Premises used: Iff.mpr, le_antisymm, MvPolynomial.coeffsIn_le
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
M N : Submodule R S
r : S
s : σ →₀ ℕ
m : S
hm : m ∈ M
n : S
hn : n ∈ N
refine_1 :
  HMul.hMul (α := MvPolynomial σ S) (β := MvPolynomial σ S)
      ((monomial s : (a : S) → MvPolynomial σ S) m : MvPolynomial σ S)
      ((monomial 0 : (a : S) → MvPolynomial σ S) n : MvPolynomial σ S) ∈
    coeffsIn σ M * coeffsIn σ N
⊢ Membership.mem (α := MvPolynomial σ S) (coeffsIn σ M * coeffsIn σ N)
    ((monomial s : (a : S) → MvPolynomial σ S) (m * n) : MvPolynomial σ S)

Tactic:
rw [← add_zero s, ← monomial_mul]

Premises used: MvPolynomial.monomial_mul, add_zero
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
M N : Submodule R S
r : S
s : σ →₀ ℕ
m : S
hm : m ∈ M
n : S
hn : n ∈ N
refine_1 :
  Membership.mem (α := MvPolynomial σ S) (coeffsIn σ M) ((monomial s : (a : S) → MvPolynomial σ S) m : MvPolynomial σ S)
refine_1₁ :
  Membership.mem (α := MvPolynomial σ S) (coeffsIn σ N) ((monomial 0 : (a : S) → MvPolynomial σ S) n : MvPolynomial σ S)
⊢ HMul.hMul (α := MvPolynomial σ S) (β := MvPolynomial σ S)
      ((monomial s : (a : S) → MvPolynomial σ S) m : MvPolynomial σ S)
      ((monomial 0 : (a : S) → MvPolynomial σ S) n : MvPolynomial σ S) ∈
    coeffsIn σ M * coeffsIn σ N

Tactic:
apply Submodule.mul_mem_mul

Premises used: Submodule.mul_mem_mul
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
M N : Submodule R S
r : S
s : σ →₀ ℕ
m : S
hm : m ∈ M
n : S
hn : n ∈ N
⊢ Membership.mem (α := MvPolynomial σ S) (coeffsIn σ M) ((monomial s : (a : S) → MvPolynomial σ S) m : MvPolynomial σ S)

Tactic:
simpa
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
M N : Submodule R S
r : S
s : σ →₀ ℕ
m : S
hm : m ∈ M
n : S
hn : n ∈ N
⊢ Membership.mem (α := MvPolynomial σ S) (coeffsIn σ N) ((monomial 0 : (a : S) → MvPolynomial σ S) n : MvPolynomial σ S)

Tactic:
simpa
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
M N : Submodule R S
r : S
s : σ →₀ ℕ
x : S
hx_1 : x ∈ M * N
y : S
hy_1 : y ∈ M * N
hx :
  Membership.mem (α := MvPolynomial σ S) (coeffsIn σ M * coeffsIn σ N)
    ((monomial s : (a : S) → MvPolynomial σ S) x : MvPolynomial σ S)
hy :
  Membership.mem (α := MvPolynomial σ S) (coeffsIn σ M * coeffsIn σ N)
    ((monomial s : (a : S) → MvPolynomial σ S) y : MvPolynomial σ S)
⊢ Membership.mem (α := MvPolynomial σ S) (coeffsIn σ M * coeffsIn σ N)
    ((monomial s : (a : S) → MvPolynomial σ S) (x + y) : MvPolynomial σ S)

Tactic:
simpa [map_add] using add_mem hx hy

Premises used: map_add, AddMemClass.add_mem
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
M N : Submodule R S
r : S
hr : r ∈ M * N
s : σ →₀ ℕ
refine_1 :
  ∀ (m : S) (hm : m ∈ M) (n : S) (hn : n ∈ N),
    Membership.mem (α := MvPolynomial σ S) (coeffsIn σ M * coeffsIn σ N)
      ((monomial s : (a : S) → MvPolynomial σ S) (m * n) : MvPolynomial σ S)
refine_1₁ :
  ∀ x ∈ M * N,
    ∀ y ∈ M * N,
      ∀
        (hx :
          Membership.mem (α := MvPolynomial σ S) (coeffsIn σ M * coeffsIn σ N)
            ((monomial s : (a : S) → MvPolynomial σ S) x : MvPolynomial σ S))
        (hy :
          Membership.mem (α := MvPolynomial σ S) (coeffsIn σ M * coeffsIn σ N)
            ((monomial s : (a : S) → MvPolynomial σ S) y : MvPolynomial σ S)),
        Membership.mem (α := MvPolynomial σ S) (coeffsIn σ M * coeffsIn σ N)
          ((monomial s : (a : S) → MvPolynomial σ S) (x + y) : MvPolynomial σ S)
⊢ Membership.mem (α := MvPolynomial σ S) (coeffsIn σ M * coeffsIn σ N)
    ((monomial s : (a : S) → MvPolynomial σ S) r : MvPolynomial σ S)

Tactic:
induction hr using Submodule.mul_induction_on' with
    | mem_mul_mem m hm n hn =>
      rw [← add_zero s, ← monomial_mul]
      apply Submodule.mul_mem_mul <;> simpa
    | add x _ y _ hx hy =>
      simpa [map_add] using add_mem hx hy

Premises used: Submodule.mul_mem_mul, map_add, MvPolynomial.monomial_mul, add_zero
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
M N : Submodule R S
refine_2 : ∀ m ∈ coeffsIn σ M, ∀ n ∈ coeffsIn σ N, m * n ∈ coeffsIn σ (M * N)
⊢ coeffsIn σ M * coeffsIn σ N ≤ coeffsIn σ (M * N)

Tactic:
rw [Submodule.mul_le]

Premises used: Submodule.mul_le
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
M N : Submodule R S
x : MvPolynomial σ S
hx : x ∈ coeffsIn σ M
y : MvPolynomial σ S
hy : y ∈ coeffsIn σ N
k : σ →₀ ℕ
refine_2 : ∑ x_1 ∈ @Finset.antidiagonal _ instAddMonoid _ k, coeff x_1.1 x * coeff x_1.2 y ∈ M * N
⊢ coeff k (x * y) ∈ M * N

Tactic:
rw [MvPolynomial.coeff_mul]

Premises used: MvPolynomial.coeff_mul
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
M N : Submodule R S
x : MvPolynomial σ S
hx : x ∈ coeffsIn σ M
y : MvPolynomial σ S
hy : y ∈ coeffsIn σ N
k : σ →₀ ℕ
⊢ ∑ x_1 ∈ @Finset.antidiagonal _ instAddMonoid _ k, coeff x_1.1 x * coeff x_1.2 y ∈ M * N

Tactic:
sum_mem fun c hc ↦ Submodule.mul_mem_mul (hx _) (hy _)

Premises used: Submodule.mul_mem_mul, Prod.fst, Prod.snd, sum_mem
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
M N : Submodule R S
x : MvPolynomial σ S
hx : x ∈ coeffsIn σ M
y : MvPolynomial σ S
hy : y ∈ coeffsIn σ N
k : σ →₀ ℕ
⊢ ∑ x_1 ∈ @Finset.antidiagonal _ instAddMonoid _ k, coeff x_1.1 x * coeff x_1.2 y ∈ M * N

Tactic:
exact sum_mem fun c hc ↦ Submodule.mul_mem_mul (hx _) (hy _)

Premises used: Submodule.mul_mem_mul, sum_mem
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
M N : Submodule R S
refine_1 :
  ∀ m ∈ M * N,
    ∀ (i : σ →₀ ℕ),
      Membership.mem (α := MvPolynomial σ S) (coeffsIn σ M * coeffsIn σ N)
        ((monomial i : (a : S) → MvPolynomial σ S) m : MvPolynomial σ S)
refine_2 refine_2₁ : coeffsIn σ M * coeffsIn σ N ≤ coeffsIn σ (M * N)
⊢ coeffsIn σ (M * N) = coeffsIn σ M * coeffsIn σ N

Tactic:
classical
  refine le_antisymm (coeffsIn_le.2 ?_) ?_
  · intro r hr s
    induction hr using Submodule.mul_induction_on' with
    | mem_mul_mem m hm n hn =>
      rw [← add_zero s, ← monomial_mul]
      apply Submodule.mul_mem_mul <;> simpa
    | add x _ y _ hx hy =>
      simpa [map_add] using add_mem hx hy
  · rw [Submodule.mul_le]
    intro x hx y hy k
    rw [MvPolynomial.coeff_mul]
    exact sum_mem fun c hc ↦ Submodule.mul_mem_mul (hx _) (hy _)

Premises used: Iff.mpr, Submodule.mul_mem_mul, map_add, le_antisymm, MvPolynomial.monomial_mul, Submodule.mul_le, MvPolynomial.coeffsIn_le, MvPolynomial.coeff_mul
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
h : Ne (α := ℕ) 1 0
M : Submodule R S
⊢ coeffsIn σ (HPow.hPow (β := ℕ) M 1) = HPow.hPow (β := ℕ) (coeffsIn σ M) 1

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
n : ℕ
h : n + 2 ≠ 0
M : Submodule R S
a : n + 1 ≠ 0
⊢ coeffsIn σ (M ^ (n + 2)) = coeffsIn σ M ^ (n + 2)

Tactic:
rw [pow_succ, coeffsIn_mul, coeffsIn_pow, ← pow_succ]

Premises used: pow_succ, MvPolynomial.coeffsIn_mul
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
n : ℕ
h : n + 2 ≠ 0
M : Submodule R S
⊢ n + 1 ≠ 0

Tactic:
n.succ_ne_zero

Premises used: Nat.succ_ne_zero
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
n : ℕ
h : n + 2 ≠ 0
M : Submodule R S
⊢ n + 1 ≠ 0

Tactic:
exact n.succ_ne_zero

Premises used: Nat.succ_ne_zero
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
M : Submodule R S
⊢ HPow.hPow (β := ℕ) (coeffsIn σ M) 0 ≤ coeffsIn σ (HPow.hPow (β := ℕ) M 0)

Tactic:
simpa using ⟨1, map_one _⟩