awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
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) (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
have 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
Tactic: rw [add_comm, mul_comm p p', mul_comm q q']
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
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
⊢ natDegree.{u_2} (R := R) ((aeval f : (a : MvPolynomial σ R) → R[X]) F) ≤ m * n
have 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
Tactic: rw [MvPolynomial.aeval_def, MvPolynomial.eval₂]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
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
⊢ 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
have 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
Tactic: apply (Polynomial.natDegree_sum_le _ _).trans
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
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
⊢ 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
have 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
Tactic: apply Finset.sup_le
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
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
⊢ 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
have 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
Tactic: simp_rw [Function.comp_apply, ← C_eq_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
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
⊢ (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
have a : natDegree.{u_2} (R := R) (d.prod fun (n : σ) (e : ℕ) ↦ f n ^ e) ≤ m * n
Tactic: apply (Polynomial.natDegree_C_mul_le _ _).trans
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
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
⊢ natDegree.{u_2} (R := R) (d.prod fun (n : σ) (e : ℕ) ↦ f n ^ e) ≤ m * n
have a : ∑ i ∈ d.support, natDegree.{u_2} (R := R) ((fun (n : σ) (e : ℕ) ↦ f n ^ e) i ((d : (a : σ) → ℕ) i)) ≤ m * n
Tactic: apply (Polynomial.natDegree_prod_le _ _).trans
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
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
have rw : (∑ i ∈ d.support, (d : (a : σ) → ℕ) i) * n ≤ m * n
Tactic: rw [← Finset.sum_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
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, (d : (a : σ) → ℕ) i) * n ≤ m * n
have apply : ∑ i ∈ d.support, (d : (a : σ) → ℕ) i ≤ F.totalDegree
Tactic: apply mul_le_mul' (.trans _ hF) le_rfl
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (hypothesis)
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, natDegree.{u_2} (R := R) ((fun (n : σ) (e : ℕ) ↦ f n ^ e) i ((d : (a : σ) → ℕ) i)) ≤ m * n
have this : ∑ 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
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
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 ∈ d.support, natDegree.{u_2} (R := R) ((fun (n : σ) (e : ℕ) ↦ f n ^ e) i ((d : (a : σ) → ℕ) i)) ≤ m * n
have 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
Tactic: apply (Finset.sum_le_sum _).trans this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
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 : σ
⊢ natDegree.{u_2} (R := R) ((fun (n : σ) (e : ℕ) ↦ f n ^ e) i ((d : (a : σ) → ℕ) i)) ≤
    HMul.hMul (α := ℕ) ((d : (a : σ) → ℕ) i : ℕ) n
have apply : HMul.hMul (α := ℕ) ((d : (a : σ) → ℕ) i : ℕ) (f i).natDegree ≤ HMul.hMul (α := ℕ) ((d : (a : σ) → ℕ) i : ℕ) n
Tactic: apply Polynomial.natDegree_pow_le.trans
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsNoetherianRing R
⊢ IsNoetherianRing.{u} (MvPolynomial (Fin 0) R)
have f : R ≃+* MvPolynomial (Fin 0) R
Tactic: apply isNoetherianRing_of_ringEquiv R
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsNoetherianRing R
⊢ R ≃+* MvPolynomial (Fin 0) R
have f : MvPolynomial (Fin 0) R ≃+* R
Tactic: symm
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
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
⊢ IsNoetherianRing (MvPolynomial σ R)
have intro : ∀ (val : Fintype σ), IsNoetherianRing (MvPolynomial σ R)
Tactic: cases nonempty_fintype σ
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
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
⊢ (ϕ : (a : MvPolynomial σ R) → S) p = eval₂ (ϕ.comp C) (fun (s : σ) ↦ (ϕ : (a : MvPolynomial σ R) → S) (X s)) p
have intro : ∀ (val : Fintype σ),
  (ϕ : (a : MvPolynomial σ R) → S) p = eval₂ (ϕ.comp C) (fun (s : σ) ↦ (ϕ : (a : MvPolynomial σ R) → S) (X s)) p
Tactic: cases nonempty_fintype σ
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
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
have 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
Tactic: refine Trans.trans (congr_arg ϕ (MvPolynomial.as_sum p)) ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
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) (∑ v ∈ p.support, (monomial v : (a : R) → MvPolynomial σ R) (coeff v p)) =
    eval₂ (ϕ.comp C) (fun (s : σ) ↦ (ϕ : (a : MvPolynomial σ R) → S) (X s)) p
have 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))
Tactic: rw [MvPolynomial.eval₂_eq', map_sum ϕ]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
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 σ
⊢ 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))
have 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)
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
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 σ
⊢ 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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
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)
⊢ p ∈ I
have rw : ∑ v ∈ p.support, (monomial v : (a : R) → MvPolynomial σ R) (coeff v p) ∈ I
Tactic: rw [as_sum p]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
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)
⊢ ∑ v ∈ p.support, (monomial v : (a : R) → MvPolynomial σ R) (coeff v p) ∈ I
have suffices : ∀ m ∈ p.support,
  Membership.mem (α := MvPolynomial σ R) I ((monomial m : (a : R) → MvPolynomial σ R) (coeff m p) : MvPolynomial σ R)
Tactic: suffices ∀ m ∈ p.support, monomial m (MvPolynomial.coeff m p) ∈ I by
    exact Submodule.sum_mem I this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
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 ((monomial m : (a : R) → MvPolynomial σ R) (coeff m p) : MvPolynomial σ R)
have 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
Tactic: rw [← mul_one (coeff m p), ← C_mul_monomial]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
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
⊢ 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
have suffices : Membership.mem (α := MvPolynomial σ R) I ((C : (a : R) → MvPolynomial σ R) (coeff m p) : MvPolynomial σ R)
Tactic: suffices C (coeff m p) ∈ I by exact I.mul_mem_right (monomial m 1) this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
σ : Type v
inst : CommRing R
I : Ideal R
f : MvPolynomial σ R
⊢ Membership.mem (γ := Ideal (MvPolynomial σ R)) (Ideal.map (F := R →+* MvPolynomial σ R) C I) f ↔
    ∀ (m : σ →₀ ℕ), coeff m f ∈ I
have mp : Membership.mem (γ := Ideal (MvPolynomial σ R)) (Ideal.map (F := R →+* MvPolynomial σ R) C I) f →
  ∀ (m : σ →₀ ℕ), coeff m f ∈ I
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
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
⊢ Membership.mem (γ := Ideal (MvPolynomial σ R)) (Ideal.map (F := R →+* MvPolynomial σ R) C I) f ↔
    ∀ (m : σ →₀ ℕ), coeff m f ∈ I
have mpr : (∀ (m : σ →₀ ℕ), coeff m f ∈ I) →
  Membership.mem (γ := Ideal (MvPolynomial σ R)) (Ideal.map (F := R →+* MvPolynomial σ R) C I) f
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
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
have mp : ∀ (x : MvPolynomial σ R)
  (h : Membership.mem (γ := Set (MvPolynomial σ R)) ((⇑C : (a : R) → MvPolynomial σ R) '' (↑I : Set R)) x) (m : σ →₀ ℕ),
  coeff m x ∈ I
Tactic: refine Submodule.span_induction ?_ ?_ ?_ ?_ hf
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
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
⊢ ∀ (m : σ →₀ ℕ), coeff m f ∈ I
have mp₁ : ∀ (m : σ →₀ ℕ), coeff m 0 ∈ I
Tactic: refine Submodule.span_induction ?_ ?_ ?_ ?_ hf
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
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
⊢ ∀ (m : σ →₀ ℕ), coeff m f ∈ I
have 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
Tactic: refine Submodule.span_induction ?_ ?_ ?_ ?_ hf
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
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
⊢ ∀ (m : σ →₀ ℕ), coeff m f ∈ I
have 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
Tactic: refine Submodule.span_induction ?_ ?_ ?_ ?_ hf
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
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 : σ →₀ ℕ
⊢ coeff n f ∈ I
have mp : ∀ (x : R) (hx : x ∈ (↑I : Set R) ∧ (C : (a : R) → MvPolynomial σ R) x = f), coeff n f ∈ I
Tactic: obtain ⟨x, hx⟩ := (Set.mem_image _ _ _).mp hf
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
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
⊢ coeff n f ∈ I
have mp : (if 0 = n then x else 0) ∈ I
Tactic: rw [← hx.right, coeff_C]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
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
⊢ (if 0 = n then x else 0) ∈ I
have pos : ∀ (h : n = 0), (if 0 = n then x else 0) ∈ I
Tactic: by_cases h : n = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
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
⊢ (if 0 = n then x else 0) ∈ I
have neg : ∀ (h : ¬n = 0), (if 0 = n then x else 0) ∈ I
Tactic: by_cases h : n = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
σ : Type v
inst : CommRing R
I : Ideal R
f : MvPolynomial σ R
hf : ∀ (m : σ →₀ ℕ), coeff m f ∈ I
⊢ Membership.mem (γ := Ideal (MvPolynomial σ R)) (Ideal.map (F := R →+* MvPolynomial σ R) C I) f
have mpr : Membership.mem (γ := Ideal (MvPolynomial σ R)) (Ideal.map (F := R →+* MvPolynomial σ R) C I)
  (∑ v ∈ f.support, (monomial v : (a : R) → MvPolynomial σ R) (coeff v f))
Tactic: rw [as_sum f]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
σ : Type v
inst : CommRing R
I : Ideal R
f : MvPolynomial σ R
hf : ∀ (m : σ →₀ ℕ), coeff m f ∈ I
⊢ Membership.mem (γ := Ideal (MvPolynomial σ R)) (Ideal.map (F := R →+* MvPolynomial σ R) C I)
    (∑ v ∈ f.support, (monomial v : (a : R) → MvPolynomial σ R) (coeff v f))
have mpr : ∀ m ∈ f.support,
  Membership.mem (α := MvPolynomial σ R) (γ := Ideal (MvPolynomial σ R)) (Ideal.map (F := R →+* MvPolynomial σ R) C I)
    ((monomial m : (a : R) → MvPolynomial σ R) (coeff m f) : MvPolynomial σ R)
Tactic: suffices ∀ m ∈ f.support, monomial m (coeff m f) ∈ (Ideal.map C I : Ideal (MvPolynomial σ R)) by
      exact Submodule.sum_mem _ this