awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
i : σ
apply : HMul.hMul (α := ℕ) ((d : (a : σ) → ℕ) i : ℕ) (f i).natDegree ≤ HMul.hMul (α := ℕ) ((d : (a : σ) → ℕ) i : ℕ) n
⊢ natDegree.{u_2} (R := R) ((fun (n : σ) (e : ℕ) ↦ f n ^ e) i ((d : (a : σ) → ℕ) i)) ≤
    HMul.hMul (α := ℕ) ((d : (a : σ) → ℕ) i : ℕ) n

Tactic:
apply Polynomial.natDegree_pow_le.trans

Premises used: Polynomial.natDegree_pow_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
this : ∑ i ∈ d.support, HMul.hMul (α := ℕ) ((d : (a : σ) → ℕ) i : ℕ) n ≤ m * n
i : σ
⊢ HMul.hMul (α := ℕ) ((d : (a : σ) → ℕ) i : ℕ) (f i).natDegree ≤ HMul.hMul (α := ℕ) ((d : (a : σ) → ℕ) i : ℕ) n

Tactic:
mul_le_mul' le_rfl (hf i)

Premises used: le_rfl, 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
this : ∑ i ∈ d.support, HMul.hMul (α := ℕ) ((d : (a : σ) → ℕ) i : ℕ) n ≤ m * n
i : σ
⊢ HMul.hMul (α := ℕ) ((d : (a : σ) → ℕ) i : ℕ) (f i).natDegree ≤ HMul.hMul (α := ℕ) ((d : (a : σ) → ℕ) i : ℕ) n

Tactic:
exact mul_le_mul' le_rfl (hf i)

Premises used: le_rfl, mul_le_mul'
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : IsNoetherianRing R
f : R ≃+* MvPolynomial (Fin 0) R
⊢ IsNoetherianRing.{u} (MvPolynomial (Fin 0) R)

Tactic:
apply isNoetherianRing_of_ringEquiv R

Premises used: isNoetherianRing_of_ringEquiv
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : IsNoetherianRing R
f : MvPolynomial (Fin 0) R ≃+* R
⊢ R ≃+* MvPolynomial (Fin 0) R

Tactic:
symm
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : IsNoetherianRing R
⊢ MvPolynomial (Fin 0) R ≃+* R

Tactic:
apply MvPolynomial.isEmptyRingEquiv R (Fin 0)

Premises used: OfNat.ofNat, Fin, MvPolynomial.isEmptyRingEquiv
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
S : Type u_1
σ : Type v
M : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Finite σ
inst_5 : IsNoetherianRing R
intro : ∀ (val : Fintype σ), IsNoetherianRing (MvPolynomial σ R)
⊢ IsNoetherianRing (MvPolynomial σ R)

Tactic:
cases nonempty_fintype σ

Premises used: nonempty_fintype
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
S : Type u_1
σ : Type v
M : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Finite σ
inst_5 : IsNoetherianRing R
val : Fintype σ
⊢ IsNoetherianRing (MvPolynomial σ R)

Tactic:
@isNoetherianRing_of_ringEquiv (MvPolynomial (Fin (Fintype.card σ)) R) _ _ _
      (renameEquiv R (Fintype.equivFin σ).symm).toRingEquiv isNoetherianRing_fin

Premises used: Fintype.card, Fintype.equivFin, AlgEquiv.toRingEquiv, MvPolynomial, Equiv.symm, Fin, MvPolynomial.renameEquiv, isNoetherianRing_of_ringEquiv
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
S : Type u_1
σ : Type v
M : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Finite σ
inst_5 : IsNoetherianRing R
val : Fintype σ
⊢ IsNoetherianRing (MvPolynomial σ R)

Tactic:
exact
    @isNoetherianRing_of_ringEquiv (MvPolynomial (Fin (Fintype.card σ)) R) _ _ _
      (renameEquiv R (Fintype.equivFin σ).symm).toRingEquiv isNoetherianRing_fin

Premises used: Fintype.card, Fintype.equivFin, AlgEquiv.toRingEquiv, MvPolynomial, Equiv.symm, Fin, MvPolynomial.renameEquiv, isNoetherianRing_of_ringEquiv
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
σ : Type v
inst : CommRing R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Finite σ
ϕ : MvPolynomial σ R →+* S
p : MvPolynomial σ R
intro :
  ∀ (val : Fintype σ),
    (ϕ : (a : MvPolynomial σ R) → S) p = eval₂ (ϕ.comp C) (fun (s : σ) ↦ (ϕ : (a : MvPolynomial σ R) → S) (X s)) p
⊢ (ϕ : (a : MvPolynomial σ R) → S) p = eval₂ (ϕ.comp C) (fun (s : σ) ↦ (ϕ : (a : MvPolynomial σ R) → S) (X s)) p

Tactic:
cases nonempty_fintype σ

Premises used: nonempty_fintype
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
σ : Type v
inst : CommRing R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Finite σ
ϕ : MvPolynomial σ R →+* S
p : MvPolynomial σ R
val : Fintype σ
⊢ (ϕ : (a : MvPolynomial σ R) → S) p = eval₂ (ϕ.comp C) (fun (s : σ) ↦ (ϕ : (a : MvPolynomial σ R) → S) (X s)) p

Tactic:
Trans.trans (congr_arg ϕ (MvPolynomial.as_sum p)) ?_

Premises used: Trans.trans, MvPolynomial.as_sum, congr_arg, DFunLike.coe
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
σ : Type v
inst : CommRing R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Finite σ
ϕ : MvPolynomial σ R →+* S
p : MvPolynomial σ R
val : Fintype σ
intro :
  (ϕ : (a : MvPolynomial σ R) → S) (∑ v ∈ p.support, (monomial v : (a : R) → MvPolynomial σ R) (coeff v p)) =
    eval₂ (ϕ.comp C) (fun (s : σ) ↦ (ϕ : (a : MvPolynomial σ R) → S) (X s)) p
⊢ (ϕ : (a : MvPolynomial σ R) → S) p = eval₂ (ϕ.comp C) (fun (s : σ) ↦ (ϕ : (a : MvPolynomial σ R) → S) (X s)) p

Tactic:
refine Trans.trans (congr_arg ϕ (MvPolynomial.as_sum p)) ?_

Premises used: Trans.trans, MvPolynomial.as_sum, congr_arg, DFunLike.coe
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
σ : Type v
inst : CommRing R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Finite σ
ϕ : MvPolynomial σ R →+* S
p : MvPolynomial σ R
val : Fintype σ
intro :
  Eq.{u_2 + 1} (α := S)
    (∑ x ∈ p.support,
      (ϕ : (a : MvPolynomial σ R) → S) ((monomial x : (a : R) → MvPolynomial σ R) (coeff x p) : MvPolynomial σ R))
    (∑ d ∈ p.support,
      HMul.hMul (α := S) (β := S) ((ϕ.comp C : (a : R) → S) (coeff d p) : S)
        (∏ i : σ, HPow.hPow (α := S) (β := ℕ) ((ϕ : (a : MvPolynomial σ R) → S) (X i) : S) ((d : (a : σ) → ℕ) i : ℕ) :
          S))
⊢ (ϕ : (a : MvPolynomial σ R) → S) (∑ v ∈ p.support, (monomial v : (a : R) → MvPolynomial σ R) (coeff v p)) =
    eval₂ (ϕ.comp C) (fun (s : σ) ↦ (ϕ : (a : MvPolynomial σ R) → S) (X s)) p

Tactic:
rw [MvPolynomial.eval₂_eq', map_sum ϕ]

Premises used: map_sum, MvPolynomial.eval₂_eq'
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
σ : Type v
inst : CommRing R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Finite σ
ϕ : MvPolynomial σ R →+* S
p : MvPolynomial σ R
val : Fintype σ
intro :
  Eq (α := (σ →₀ ℕ) → S)
    (fun (x : σ →₀ ℕ) ↦
      (ϕ : (a : MvPolynomial σ R) → S) ((monomial x : (a : R) → MvPolynomial σ R) (coeff x p) : MvPolynomial σ R))
    fun (d : σ →₀ ℕ) ↦
    HMul.hMul (α := S) (β := S) ((ϕ.comp C : (a : R) → S) (coeff d p) : S)
      (∏ i : σ, HPow.hPow (α := S) (β := ℕ) ((ϕ : (a : MvPolynomial σ R) → S) (X i) : S) ((d : (a : σ) → ℕ) i : ℕ) : S)
⊢ Eq.{u_2 + 1} (α := S)
    (∑ x ∈ p.support,
      (ϕ : (a : MvPolynomial σ R) → S) ((monomial x : (a : R) → MvPolynomial σ R) (coeff x p) : MvPolynomial σ R))
    (∑ d ∈ p.support,
      HMul.hMul (α := S) (β := S) ((ϕ.comp C : (a : R) → S) (coeff d p) : S)
        (∏ i : σ, HPow.hPow (α := S) (β := ℕ) ((ϕ : (a : MvPolynomial σ R) → S) (X i) : S) ((d : (a : σ) → ℕ) i : ℕ) :
          S))

Tactic:
congr
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
σ : Type v
inst : CommRing R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Finite σ
ϕ : MvPolynomial σ R →+* S
p : MvPolynomial σ R
val : Fintype σ
intro :
  ∀ (x : σ →₀ ℕ),
    (ϕ : (a : MvPolynomial σ R) → S) ((monomial x : (a : R) → MvPolynomial σ R) (coeff x p) : MvPolynomial σ R) =
      HMul.hMul (α := S) (β := S) ((ϕ.comp C : (a : R) → S) (coeff x p) : S)
        (∏ i : σ, HPow.hPow (α := S) (β := ℕ) ((ϕ : (a : MvPolynomial σ R) → S) (X i) : S) ((x : (a : σ) → ℕ) i : ℕ) :
          S)
⊢ Eq (α := (σ →₀ ℕ) → S)
    (fun (x : σ →₀ ℕ) ↦
      (ϕ : (a : MvPolynomial σ R) → S) ((monomial x : (a : R) → MvPolynomial σ R) (coeff x p) : MvPolynomial σ R))
    fun (d : σ →₀ ℕ) ↦
    HMul.hMul (α := S) (β := S) ((ϕ.comp C : (a : R) → S) (coeff d p) : S)
      (∏ i : σ, HPow.hPow (α := S) (β := ℕ) ((ϕ : (a : MvPolynomial σ R) → S) (X i) : S) ((d : (a : σ) → ℕ) i : ℕ) : S)

Tactic:
ext
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
σ : Type v
inst : CommRing R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Finite σ
ϕ : MvPolynomial σ R →+* S
p : MvPolynomial σ R
val : Fintype σ
x : σ →₀ ℕ
⊢ (ϕ : (a : MvPolynomial σ R) → S) ((monomial x : (a : R) → MvPolynomial σ R) (coeff x p) : MvPolynomial σ R) =
    HMul.hMul (α := S) (β := S) ((ϕ.comp C : (a : R) → S) (coeff x p) : S)
      (∏ i : σ, HPow.hPow (α := S) (β := ℕ) ((ϕ : (a : MvPolynomial σ R) → S) (X i) : S) ((x : (a : σ) → ℕ) i : ℕ) : S)

Tactic:
simp only [monomial_eq, ϕ.map_pow, map_prod ϕ, ϕ.comp_apply, ϕ.map_mul, Finsupp.prod_pow]

Premises used: map_prod, Finsupp.prod_pow, MvPolynomial.monomial_eq, RingHom.comp_apply, RingHom.map_mul, RingHom.map_pow
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
σ : Type v
inst : CommRing R
I : Ideal (MvPolynomial σ R)
p : MvPolynomial σ R
hcoe : ∀ (m : σ →₀ ℕ), Membership.mem (γ := Ideal R) (Ideal.comap (F := R →+* MvPolynomial σ R) C I) (coeff m p)
rw : ∑ v ∈ p.support, (monomial v : (a : R) → MvPolynomial σ R) (coeff v p) ∈ I
⊢ p ∈ I

Tactic:
rw [as_sum p]

Premises used: MvPolynomial.as_sum
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
σ : Type v
inst : CommRing R
I : Ideal (MvPolynomial σ R)
p : MvPolynomial σ R
hcoe : ∀ (m : σ →₀ ℕ), Membership.mem (γ := Ideal R) (Ideal.comap (F := R →+* MvPolynomial σ R) C I) (coeff m p)
this :
  ∀ m ∈ p.support,
    Membership.mem (α := MvPolynomial σ R) I ((monomial m : (a : R) → MvPolynomial σ R) (coeff m p) : MvPolynomial σ R)
⊢ ∑ v ∈ p.support, (monomial v : (a : R) → MvPolynomial σ R) (coeff v p) ∈ I

Tactic:
Submodule.sum_mem I this

Premises used: Set.Mem, Submodule.sum_mem
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
σ : Type v
inst : CommRing R
I : Ideal (MvPolynomial σ R)
p : MvPolynomial σ R
hcoe : ∀ (m : σ →₀ ℕ), Membership.mem (γ := Ideal R) (Ideal.comap (F := R →+* MvPolynomial σ R) C I) (coeff m p)
this :
  ∀ m ∈ p.support,
    Membership.mem (α := MvPolynomial σ R) I ((monomial m : (a : R) → MvPolynomial σ R) (coeff m p) : MvPolynomial σ R)
⊢ ∑ v ∈ p.support, (monomial v : (a : R) → MvPolynomial σ R) (coeff v p) ∈ I

Tactic:
exact Submodule.sum_mem I this

Premises used: Submodule.sum_mem
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
σ : Type v
inst : CommRing R
I : Ideal (MvPolynomial σ R)
p : MvPolynomial σ R
hcoe : ∀ (m : σ →₀ ℕ), Membership.mem (γ := Ideal R) (Ideal.comap (F := R →+* MvPolynomial σ R) C I) (coeff m p)
suffices :
  ∀ m ∈ p.support,
    Membership.mem (α := MvPolynomial σ R) I ((monomial m : (a : R) → MvPolynomial σ R) (coeff m p) : MvPolynomial σ R)
⊢ ∑ v ∈ p.support, (monomial v : (a : R) → MvPolynomial σ R) (coeff v p) ∈ I

Tactic:
suffices ∀ m ∈ p.support, monomial m (MvPolynomial.coeff m p) ∈ I by
    exact Submodule.sum_mem I this
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
σ : Type v
inst : CommRing R
I : Ideal (MvPolynomial σ R)
p : MvPolynomial σ R
hcoe : ∀ (m : σ →₀ ℕ), Membership.mem (γ := Ideal R) (Ideal.comap (F := R →+* MvPolynomial σ R) C I) (coeff m p)
m : σ →₀ ℕ
_ :
  m ∈ p.support →
    Membership.mem (α := MvPolynomial σ R) I ((monomial m : (a : R) → MvPolynomial σ R) (coeff m p) : MvPolynomial σ R)
⊢ m ∈ p.support →
    Membership.mem (α := MvPolynomial σ R) I ((monomial m : (a : R) → MvPolynomial σ R) (coeff m p) : MvPolynomial σ R)

Tactic:
_
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
σ : Type v
inst : CommRing R
I : Ideal (MvPolynomial σ R)
p : MvPolynomial σ R
hcoe : ∀ (m : σ →₀ ℕ), Membership.mem (γ := Ideal R) (Ideal.comap (F := R →+* MvPolynomial σ R) C I) (coeff m p)
m : σ →₀ ℕ
h : m ∈ p.support
rw :
  HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((C : (a : R) → MvPolynomial σ R) (coeff m p) : MvPolynomial σ R)
      ((monomial m : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R) ∈
    I
⊢ Membership.mem (α := MvPolynomial σ R) I ((monomial m : (a : R) → MvPolynomial σ R) (coeff m p) : MvPolynomial σ R)

Tactic:
rw [← mul_one (coeff m p), ← C_mul_monomial]

Premises used: MvPolynomial.C_mul_monomial, MvPolynomial.coeff, mul_one
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
σ : Type v
inst : CommRing R
I : Ideal (MvPolynomial σ R)
p : MvPolynomial σ R
hcoe : ∀ (m : σ →₀ ℕ), Membership.mem (γ := Ideal R) (Ideal.comap (F := R →+* MvPolynomial σ R) C I) (coeff m p)
m : σ →₀ ℕ
h : m ∈ p.support
this : Membership.mem (α := MvPolynomial σ R) I ((C : (a : R) → MvPolynomial σ R) (coeff m p) : MvPolynomial σ R)
⊢ HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((C : (a : R) → MvPolynomial σ R) (coeff m p) : MvPolynomial σ R)
      ((monomial m : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R) ∈
    I

Tactic:
I.mul_mem_right (monomial m 1) this

Premises used: Set.Mem, MvPolynomial.monomial, Ideal.mul_mem_right, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
σ : Type v
inst : CommRing R
I : Ideal (MvPolynomial σ R)
p : MvPolynomial σ R
hcoe : ∀ (m : σ →₀ ℕ), Membership.mem (γ := Ideal R) (Ideal.comap (F := R →+* MvPolynomial σ R) C I) (coeff m p)
m : σ →₀ ℕ
h : m ∈ p.support
this : Membership.mem (α := MvPolynomial σ R) I ((C : (a : R) → MvPolynomial σ R) (coeff m p) : MvPolynomial σ R)
⊢ HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((C : (a : R) → MvPolynomial σ R) (coeff m p) : MvPolynomial σ R)
      ((monomial m : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R) ∈
    I

Tactic:
exact I.mul_mem_right (monomial m 1) this

Premises used: MvPolynomial.monomial, Ideal.mul_mem_right, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
σ : Type v
inst : CommRing R
I : Ideal (MvPolynomial σ R)
p : MvPolynomial σ R
hcoe : ∀ (m : σ →₀ ℕ), Membership.mem (γ := Ideal R) (Ideal.comap (F := R →+* MvPolynomial σ R) C I) (coeff m p)
m : σ →₀ ℕ
h : m ∈ p.support
suffices : Membership.mem (α := MvPolynomial σ R) I ((C : (a : R) → MvPolynomial σ R) (coeff m p) : MvPolynomial σ R)
⊢ HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((C : (a : R) → MvPolynomial σ R) (coeff m p) : MvPolynomial σ R)
      ((monomial m : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R) ∈
    I

Tactic:
suffices C (coeff m p) ∈ I by exact I.mul_mem_right (monomial m 1) this
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
σ : Type v
inst : CommRing R
I : Ideal (MvPolynomial σ R)
p : MvPolynomial σ R
hcoe : ∀ (m : σ →₀ ℕ), Membership.mem (γ := Ideal R) (Ideal.comap (F := R →+* MvPolynomial σ R) C I) (coeff m p)
m : σ →₀ ℕ
h : m ∈ p.support
⊢ Membership.mem (α := MvPolynomial σ R) I ((C : (a : R) → MvPolynomial σ R) (coeff m p) : MvPolynomial σ R)

Tactic:
simpa [Ideal.mem_comap] using hcoe m

Premises used: Ideal.mem_comap
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
σ : Type v
inst : CommRing R
I : Ideal R
f : MvPolynomial σ R
mp :
  Membership.mem (γ := Ideal (MvPolynomial σ R)) (Ideal.map (F := R →+* MvPolynomial σ R) C I) f →
    ∀ (m : σ →₀ ℕ), coeff m f ∈ I
mpr :
  (∀ (m : σ →₀ ℕ), coeff m f ∈ I) →
    Membership.mem (γ := Ideal (MvPolynomial σ R)) (Ideal.map (F := R →+* MvPolynomial σ R) C I) f
⊢ Membership.mem (γ := Ideal (MvPolynomial σ R)) (Ideal.map (F := R →+* MvPolynomial σ R) C I) f ↔
    ∀ (m : σ →₀ ℕ), coeff m f ∈ I

Tactic:
constructor
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
σ : Type v
inst : CommRing R
I : Ideal R
f : MvPolynomial σ R
hf : Membership.mem (γ := Ideal (MvPolynomial σ R)) (Ideal.map (F := R →+* MvPolynomial σ R) C I) f
⊢ ∀ (m : σ →₀ ℕ), coeff m f ∈ I

Tactic:
Submodule.span_induction ?_ ?_ ?_ ?_ hf

Premises used: Submodule.span_induction
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
σ : Type v
inst : CommRing R
I : Ideal R
f : MvPolynomial σ R
hf : Membership.mem (γ := Ideal (MvPolynomial σ R)) (Ideal.map (F := R →+* MvPolynomial σ R) C I) f
mp :
  ∀ (x : MvPolynomial σ R)
    (h : Membership.mem (γ := Set (MvPolynomial σ R)) ((⇑C : (a : R) → MvPolynomial σ R) '' (↑I : Set R)) x)
    (m : σ →₀ ℕ), coeff m x ∈ I
mp₁ : ∀ (m : σ →₀ ℕ), coeff m 0 ∈ I
mp₂ :
  ∀ (x y : MvPolynomial σ R)
    (hx :
      Membership.mem (γ := Submodule (MvPolynomial σ R) (MvPolynomial σ R))
        (Submodule.span (MvPolynomial σ R) ((⇑C : (a : R) → MvPolynomial σ R) '' (↑I : Set R))) x)
    (hy :
      Membership.mem (γ := Submodule (MvPolynomial σ R) (MvPolynomial σ R))
        (Submodule.span (MvPolynomial σ R) ((⇑C : (a : R) → MvPolynomial σ R) '' (↑I : Set R))) y),
    (∀ (m : σ →₀ ℕ), coeff m x ∈ I) → (∀ (m : σ →₀ ℕ), coeff m y ∈ I) → ∀ (m : σ →₀ ℕ), coeff m (x + y) ∈ I
mp₃ :
  ∀ (a x : MvPolynomial σ R)
    (hx :
      Membership.mem (γ := Submodule (MvPolynomial σ R) (MvPolynomial σ R))
        (Submodule.span (MvPolynomial σ R) ((⇑C : (a : R) → MvPolynomial σ R) '' (↑I : Set R))) x),
    (∀ (m : σ →₀ ℕ), coeff m x ∈ I) → ∀ (m : σ →₀ ℕ), coeff m (a • x) ∈ I
⊢ ∀ (m : σ →₀ ℕ), coeff m f ∈ I

Tactic:
refine Submodule.span_induction ?_ ?_ ?_ ?_ hf
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
σ : Type v
inst : CommRing R
I : Ideal R
f_1 : MvPolynomial σ R
hf_1 : Membership.mem (γ := Ideal (MvPolynomial σ R)) (Ideal.map (F := R →+* MvPolynomial σ R) C I) f_1
f : MvPolynomial σ R
hf : Membership.mem (γ := Set (MvPolynomial σ R)) ((⇑C : (a : R) → MvPolynomial σ R) '' (↑I : Set R)) f
n : σ →₀ ℕ
mp : ∀ (x : R) (hx : x ∈ (↑I : Set R) ∧ (C : (a : R) → MvPolynomial σ R) x = f), coeff n f ∈ I
⊢ coeff n f ∈ I

Tactic:
obtain ⟨x, hx⟩ := (Set.mem_image _ _ _).mp hf

Premises used: Set.mem_image, Iff.mp
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
σ : Type v
inst : CommRing R
I : Ideal R
f_1 : MvPolynomial σ R
hf_1 : Membership.mem (γ := Ideal (MvPolynomial σ R)) (Ideal.map (F := R →+* MvPolynomial σ R) C I) f_1
f : MvPolynomial σ R
hf : Membership.mem (γ := Set (MvPolynomial σ R)) ((⇑C : (a : R) → MvPolynomial σ R) '' (↑I : Set R)) f
n : σ →₀ ℕ
x : R
hx : x ∈ (↑I : Set R) ∧ (C : (a : R) → MvPolynomial σ R) x = f
mp : (if 0 = n then x else 0) ∈ I
⊢ coeff n f ∈ I

Tactic:
rw [← hx.right, coeff_C]

Premises used: MvPolynomial.coeff_C, And.right
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
σ : Type v
inst : CommRing R
I : Ideal R
f_1 : MvPolynomial σ R
hf_1 : Membership.mem (γ := Ideal (MvPolynomial σ R)) (Ideal.map (F := R →+* MvPolynomial σ R) C I) f_1
f : MvPolynomial σ R
hf : Membership.mem (γ := Set (MvPolynomial σ R)) ((⇑C : (a : R) → MvPolynomial σ R) '' (↑I : Set R)) f
n : σ →₀ ℕ
x : R
hx : x ∈ (↑I : Set R) ∧ (C : (a : R) → MvPolynomial σ R) x = f
pos : ∀ (h : n = 0), (if 0 = n then x else 0) ∈ I
neg : ∀ (h : ¬n = 0), (if 0 = n then x else 0) ∈ I
⊢ (if 0 = n then x else 0) ∈ I

Tactic:
by_cases h : n = 0
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
σ : Type v
inst : CommRing R
I : Ideal R
f_1 : MvPolynomial σ R
hf_1 : Membership.mem (γ := Ideal (MvPolynomial σ R)) (Ideal.map (F := R →+* MvPolynomial σ R) C I) f_1
f : MvPolynomial σ R
hf : Membership.mem (γ := Set (MvPolynomial σ R)) ((⇑C : (a : R) → MvPolynomial σ R) '' (↑I : Set R)) f
n : σ →₀ ℕ
x : R
hx : x ∈ (↑I : Set R) ∧ (C : (a : R) → MvPolynomial σ R) x = f
h : n = 0
⊢ (if 0 = n then x else 0) ∈ I

Tactic:
simpa [h] using hx.left

Premises used: And.left
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
σ : Type v
inst : CommRing R
I : Ideal R
f_1 : MvPolynomial σ R
hf_1 : Membership.mem (γ := Ideal (MvPolynomial σ R)) (Ideal.map (F := R →+* MvPolynomial σ R) C I) f_1
f : MvPolynomial σ R
hf : Membership.mem (γ := Set (MvPolynomial σ R)) ((⇑C : (a : R) → MvPolynomial σ R) '' (↑I : Set R)) f
n : σ →₀ ℕ
x : R
hx : x ∈ (↑I : Set R) ∧ (C : (a : R) → MvPolynomial σ R) x = f
h : ¬n = 0
⊢ (if 0 = n then x else 0) ∈ I

Tactic:
simp [Ne.symm h]

Premises used: Ne.symm
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
σ : Type v
inst : CommRing R
I : Ideal R
f : MvPolynomial σ R
hf : Membership.mem (γ := Ideal (MvPolynomial σ R)) (Ideal.map (F := R →+* MvPolynomial σ R) C I) f
⊢ ∀ (m : σ →₀ ℕ), coeff m 0 ∈ I

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
σ : Type v
inst : CommRing R
I : Ideal R
f_1 : MvPolynomial σ R
hf_1 : Membership.mem (γ := Ideal (MvPolynomial σ R)) (Ideal.map (F := R →+* MvPolynomial σ R) C I) f_1
f g : MvPolynomial σ R
h :
  Membership.mem (γ := Submodule (MvPolynomial σ R) (MvPolynomial σ R))
    (Submodule.span (MvPolynomial σ R) ((⇑C : (a : R) → MvPolynomial σ R) '' (↑I : Set R))) f
h_1 :
  Membership.mem (γ := Submodule (MvPolynomial σ R) (MvPolynomial σ R))
    (Submodule.span (MvPolynomial σ R) ((⇑C : (a : R) → MvPolynomial σ R) '' (↑I : Set R))) g
hf : ∀ (m : σ →₀ ℕ), coeff m f ∈ I
hg : ∀ (m : σ →₀ ℕ), coeff m g ∈ I
n : σ →₀ ℕ
⊢ coeff n (f + g) ∈ I

Tactic:
simp [I.add_mem (hf n) (hg n)]

Premises used: Ideal.add_mem
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
σ : Type v
inst : CommRing R
I : Ideal R
f : MvPolynomial σ R
hf : Membership.mem (γ := Ideal (MvPolynomial σ R)) (Ideal.map (F := R →+* MvPolynomial σ R) C I) f
⊢ ∀ (x y : MvPolynomial σ R)
    (hx :
      Membership.mem (γ := Submodule (MvPolynomial σ R) (MvPolynomial σ R))
        (Submodule.span (MvPolynomial σ R) ((⇑C : (a : R) → MvPolynomial σ R) '' (↑I : Set R))) x)
    (hy :
      Membership.mem (γ := Submodule (MvPolynomial σ R) (MvPolynomial σ R))
        (Submodule.span (MvPolynomial σ R) ((⇑C : (a : R) → MvPolynomial σ R) '' (↑I : Set R))) y),
    (∀ (m : σ →₀ ℕ), coeff m x ∈ I) → (∀ (m : σ →₀ ℕ), coeff m y ∈ I) → ∀ (m : σ →₀ ℕ), coeff m (x + y) ∈ I

Tactic:
exact fun f g _ _ hf hg n => by simp [I.add_mem (hf n) (hg n)]
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
σ : Type v
inst : CommRing R
I : Ideal R
f : MvPolynomial σ R
hf : Membership.mem (γ := Ideal (MvPolynomial σ R)) (Ideal.map (F := R →+* MvPolynomial σ R) C I) f
⊢ ∀ (a x : MvPolynomial σ R)
    (hx :
      Membership.mem (γ := Submodule (MvPolynomial σ R) (MvPolynomial σ R))
        (Submodule.span (MvPolynomial σ R) ((⇑C : (a : R) → MvPolynomial σ R) '' (↑I : Set R))) x),
    (∀ (m : σ →₀ ℕ), coeff m x ∈ I) → ∀ (m : σ →₀ ℕ), coeff m (a • x) ∈ I

Tactic:
fun f g _ hg n => ?_
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
σ : Type v
inst : CommRing R
I : Ideal R
f : MvPolynomial σ R
hf : Membership.mem (γ := Ideal (MvPolynomial σ R)) (Ideal.map (F := R →+* MvPolynomial σ R) C I) f
mp :
  ∀ (f g : MvPolynomial σ R),
    Membership.mem (γ := Submodule (MvPolynomial σ R) (MvPolynomial σ R))
        (Submodule.span (MvPolynomial σ R) ((⇑C : (a : R) → MvPolynomial σ R) '' (↑I : Set R))) g →
      ∀ (hg : ∀ (m : σ →₀ ℕ), coeff m g ∈ I) (n : σ →₀ ℕ), coeff n (f • g) ∈ I
⊢ ∀ (a x : MvPolynomial σ R)
    (hx :
      Membership.mem (γ := Submodule (MvPolynomial σ R) (MvPolynomial σ R))
        (Submodule.span (MvPolynomial σ R) ((⇑C : (a : R) → MvPolynomial σ R) '' (↑I : Set R))) x),
    (∀ (m : σ →₀ ℕ), coeff m x ∈ I) → ∀ (m : σ →₀ ℕ), coeff m (a • x) ∈ I

Tactic:
refine fun f g _ hg n => ?_
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
σ : Type v
inst : CommRing R
I : Ideal R
f_1 : MvPolynomial σ R
hf : Membership.mem (γ := Ideal (MvPolynomial σ R)) (Ideal.map (F := R →+* MvPolynomial σ R) C I) f_1
f g : MvPolynomial σ R
h :
  Membership.mem (γ := Submodule (MvPolynomial σ R) (MvPolynomial σ R))
    (Submodule.span (MvPolynomial σ R) ((⇑C : (a : R) → MvPolynomial σ R) '' (↑I : Set R))) g
hg : ∀ (m : σ →₀ ℕ), coeff m g ∈ I
n : σ →₀ ℕ
⊢ ∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ n, coeff x.1 f * coeff x.2 g ∈ I

Tactic:
I.sum_mem fun c _ => I.mul_mem_left (f.coeff c.fst) (hg c.snd)

Premises used: Set.Mem, Submodule.sum_mem, Prod.fst, MvPolynomial.coeff, Ideal.mul_mem_left, Prod.snd