awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
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 : σ →₀ ℕ
⊢ p * (monomial i : (a : S) → MvPolynomial σ S) 1 ∈ coeffsIn σ M ↔ p ∈ coeffsIn σ M
have simp : (∀ (i_1 : σ →₀ ℕ), (if i ≤ i_1 then coeff (i_1 - i) p * 1 else 0) ∈ M) ↔ ∀ (i : σ →₀ ℕ), coeff i p ∈ 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]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
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
have mp : (∀ (i_1 : σ →₀ ℕ), (if i ≤ i_1 then coeff (i_1 - i) p * 1 else 0) ∈ M) → ∀ (i : σ →₀ ℕ), coeff i p ∈ 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]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
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
⊢ p * (monomial i : (a : S) → MvPolynomial σ S) 1 ∈ coeffsIn σ M ↔ p ∈ coeffsIn σ M
have mpr : (∀ (i : σ →₀ ℕ), coeff i p ∈ M) → ∀ (i_1 : σ →₀ ℕ), (if i ≤ i_1 then coeff (i_1 - i) p * 1 else 0) ∈ 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]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
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}
have refine_1 : 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 ?_
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
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}
⊢ coeffsIn σ M =
    Submodule.span R {x : MvPolynomial σ S | ∃ m ∈ M, ∃ (i : σ →₀ ℕ), (monomial i : (a : S) → MvPolynomial σ S) m = x}
have refine_2 : {x : MvPolynomial σ S | ∃ m ∈ M, ∃ (i : σ →₀ ℕ), (monomial i : (a : S) → MvPolynomial σ S) m = x} ⊆
  (↑(coeffsIn σ M) : Set (MvPolynomial σ S))
Tactic: refine le_antisymm ?_ <| Submodule.span_le.2 ?_
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
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})
    p
have 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))
Tactic: rw [p.as_sum]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
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 : σ →₀ ℕ
⊢ coeff i ((monomial s : (a : S) → MvPolynomial σ S) m) ∈ M
have refine_2 : (if s = i then m else 0) ∈ M
Tactic: simp
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
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 : σ →₀ ℕ
⊢ (if s = i then m else 0) ∈ M
have refine_2 : s = i → m ∈ M
Tactic: split
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
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
⊢ (if s = i then m else 0) ∈ M
have refine_2₁ : ¬s = i → 0 ∈ M
Tactic: split
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
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}
have refine_1 : 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]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
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}
⊢ coeffsIn σ M =
    Submodule.span R {x : MvPolynomial σ S | ∃ m ∈ M, ∃ (i : σ →₀ ℕ), (monomial i : (a : S) → MvPolynomial σ S) m = x}
have refine_2 : {x : MvPolynomial σ S | ∃ m ∈ M, ∃ (i : σ →₀ ℕ), (monomial i : (a : S) → MvPolynomial σ S) m = x} ⊆
  (↑(coeffsIn σ M) : Set (MvPolynomial σ S))
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]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
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
⊢ p ∈ coeffsIn σ M ↔ (↑p.coeffs : Set S) ⊆ (↑M : Set S)
have simp : (∀ (i : σ →₀ ℕ), coeff i p ∈ M) ↔ (↑p.support : Set (σ →₀ ℕ)) ⊆ (fun (m : σ →₀ ℕ) ↦ coeff m p) ⁻¹' (↑M : Set S)
Tactic: simp only [mem_coeffsIn, coeffs, Finset.coe_image, image_subset_iff]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
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)
have refine : ∀ (h : (↑p.support : Set (σ →₀ ℕ)) ⊆ (fun (m : σ →₀ ℕ) ↦ coeff m p) ⁻¹' (↑M : Set S)) (i : σ →₀ ℕ), coeff i p ∈ M
Tactic: refine ⟨fun h x _ ↦ h x, fun h i ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
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 : σ →₀ ℕ
⊢ coeff i p ∈ M
have pos : ∀ (hp : i ∈ p.support), coeff i p ∈ M
Tactic: by_cases hp : i ∈ p.support
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
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
⊢ coeff i p ∈ M
have neg : ∀ (hp : i ∉ p.support), coeff i p ∈ M
Tactic: by_cases hp : i ∈ p.support
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
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
have h₁ : coeff i p = 0
Tactic: convert! M.zero_mem
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
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
have refine_1 : ∀ m ∈ M * N,
  ∀ (i : σ →₀ ℕ),
    Membership.mem (α := MvPolynomial σ S) (coeffsIn σ M * coeffsIn σ N)
      ((monomial i : (a : S) → MvPolynomial σ S) m : MvPolynomial σ S)
Tactic: refine le_antisymm (coeffsIn_le.2 ?_) ?_
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
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)
⊢ coeffsIn σ (M * N) = coeffsIn σ M * coeffsIn σ N
have refine_2 : coeffsIn σ M * coeffsIn σ N ≤ coeffsIn σ (M * N)
Tactic: refine le_antisymm (coeffsIn_le.2 ?_) ?_
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
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 * coeffsIn σ N)
    ((monomial s : (a : S) → MvPolynomial σ S) (m * n) : MvPolynomial σ S)
have 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
Tactic: rw [← add_zero s, ← monomial_mul]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
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
⊢ 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
have refine_1 : Membership.mem (α := MvPolynomial σ S) (coeffsIn σ M) ((monomial s : (a : S) → MvPolynomial σ S) m : MvPolynomial σ S)
Tactic: apply Submodule.mul_mem_mul
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
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)
⊢ 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
have refine_1₁ : Membership.mem (α := MvPolynomial σ S) (coeffsIn σ N) ((monomial 0 : (a : S) → MvPolynomial σ S) n : MvPolynomial σ S)
Tactic: apply Submodule.mul_mem_mul
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
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 : σ →₀ ℕ
⊢ Membership.mem (α := MvPolynomial σ S) (coeffsIn σ M * coeffsIn σ N)
    ((monomial s : (a : S) → MvPolynomial σ S) r : MvPolynomial σ S)
have 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)
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
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
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)
⊢ Membership.mem (α := MvPolynomial σ S) (coeffsIn σ M * coeffsIn σ N)
    ((monomial s : (a : S) → MvPolynomial σ S) r : MvPolynomial σ S)
have 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)
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
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
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 * coeffsIn σ N ≤ coeffsIn σ (M * N)
have refine_2 : ∀ m ∈ coeffsIn σ M, ∀ n ∈ coeffsIn σ N, m * n ∈ coeffsIn σ (M * N)
Tactic: rw [Submodule.mul_le]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
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 : σ →₀ ℕ
⊢ coeff k (x * y) ∈ M * N
have refine_2 : ∑ x_1 ∈ @Finset.antidiagonal _ instAddMonoid _ k, coeff x_1.1 x * coeff x_1.2 y ∈ M * N
Tactic: rw [MvPolynomial.coeff_mul]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
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
have refine_1 : ∀ m ∈ M * N,
  ∀ (i : σ →₀ ℕ),
    Membership.mem (α := MvPolynomial σ S) (coeffsIn σ M * coeffsIn σ N)
      ((monomial i : (a : S) → MvPolynomial σ S) m : MvPolynomial σ S)
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 _)
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
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)
⊢ coeffsIn σ (M * N) = coeffsIn σ M * coeffsIn σ N
have refine_2 : coeffsIn σ M * coeffsIn σ N ≤ coeffsIn σ (M * 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 _)
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
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
⊢ coeffsIn σ (M ^ (n + 2)) = coeffsIn σ M ^ (n + 2)
have a : n + 1 ≠ 0
Tactic: rw [pow_succ, coeffsIn_mul, coeffsIn_pow, ← pow_succ]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Cardinal (hypothesis)
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
⊢ #(MvPolynomial σ R) ≤ max (max (lift.{u, v} #R) (lift.{v, u} #σ)) ℵ₀
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Cardinal (goal)
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
h : Nontrivial R
⊢ #(MvPolynomial σ R) ≤ max (max (lift.{u, v} #R) (lift.{v, u} #σ)) ℵ₀
have inl : IsEmpty σ → #(MvPolynomial σ R) ≤ max (max (lift.{u, v} #R) (lift.{v, u} #σ)) ℵ₀
Tactic: cases isEmpty_or_nonempty σ
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Cardinal (goal)
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
h : Nontrivial R
inl : IsEmpty σ → #(MvPolynomial σ R) ≤ max (max (lift.{u, v} #R) (lift.{v, u} #σ)) ℵ₀
⊢ #(MvPolynomial σ R) ≤ max (max (lift.{u, v} #R) (lift.{v, u} #σ)) ℵ₀
have inr : Nonempty σ → #(MvPolynomial σ R) ≤ max (max (lift.{u, v} #R) (lift.{v, u} #σ)) ℵ₀
Tactic: cases isEmpty_or_nonempty σ
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Cardinal (goal)
Goal:
σ R : Type u
inst : CommSemiring R
⊢ max (max (lift.{u, u} #R) (lift.{u, u} #σ)) ℵ₀ ≤ max (max #R #σ) ℵ₀
have rw : max (max (#R) (lift.{u, u} #σ)) ℵ₀ ≤ max (max #R #σ) ℵ₀
Tactic: rw [lift_id, lift_id]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Cardinal (goal)
Goal:
σ R : Type u
inst : CommSemiring R
rw : max (max (#R) (lift.{u, u} #σ)) ℵ₀ ≤ max (max #R #σ) ℵ₀
⊢ max (max (lift.{u, u} #R) (lift.{u, u} #σ)) ℵ₀ ≤ max (max #R #σ) ℵ₀
have rw₁ : max (max #R #σ) ℵ₀ ≤ max (max #R #σ) ℵ₀
Tactic: rw [lift_id, lift_id]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Coeff (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
s : σ →₀ ℕ
a : σ →₀ R
n : ℕ
hs : (s.sum fun (x : σ) (m : ℕ) ↦ m) = n
⊢ coeff s
      (HPow.hPow (α := MvPolynomial σ R)
        ((linearCombination R X : (a : σ →₀ R) → MvPolynomial σ R) a : MvPolynomial σ R) n) =
    HMul.hMul (α := R) (↑s.multinomial : R)
      (s.prod fun (r : σ) (m : ℕ) ↦ HPow.hPow (α := R) ((a : (a : σ) → R) r : R) m)
have simp : (∑ x ∈ a.support.piAntidiag n,
    if s = indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i then
      HMul.hMul (α := R) (↑(Nat.multinomial a.support x) : R)
        (∏ x_1 ∈ a.support, HPow.hPow (α := R) ((a : (a : σ) → R) x_1 : R) (x x_1))
    else 0) =
  HMul.hMul (α := R) (↑s.multinomial : R) (s.prod fun (r : σ) (m : ℕ) ↦ HPow.hPow (α := R) ((a : (a : σ) → R) r : R) m)
Tactic: simp only [sum, linearCombination_apply, Finset.sum_pow_eq_sum_piAntidiag, coeff_sum,
    ← C_eq_coe_nat, coeff_C_mul, smul_eq_C_mul, mul_pow, Finset.prod_mul_distrib, ← map_pow,
    ← map_prod, coeff_prod_X_pow, mul_ite, mul_one, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Coeff (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
s : σ →₀ ℕ
a : σ →₀ R
n : ℕ
hs : (s.sum fun (x : σ) (m : ℕ) ↦ m) = n
⊢ (∑ x ∈ a.support.piAntidiag n,
      if s = indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i then
        HMul.hMul (α := R) (↑(Nat.multinomial a.support x) : R)
          (∏ x_1 ∈ a.support, HPow.hPow (α := R) ((a : (a : σ) → R) x_1 : R) (x x_1))
      else 0) =
    HMul.hMul (α := R) (↑s.multinomial : R)
      (s.prod fun (r : σ) (m : ℕ) ↦ HPow.hPow (α := R) ((a : (a : σ) → R) r : R) m)
have rw : (if s = indicator a.support fun (i : σ) (x : i ∈ a.support) ↦ (s : (a : σ) → ℕ) i then
    HMul.hMul (α := R) (↑(Nat.multinomial a.support (⇑s : (a : σ) → ℕ)) : R)
      (∏ x ∈ a.support, HPow.hPow (α := R) (β := ℕ) ((a : (a : σ) → R) x : R) ((s : (a : σ) → ℕ) x : ℕ))
  else 0) =
  HMul.hMul (α := R) (↑s.multinomial : R) (s.prod fun (r : σ) (m : ℕ) ↦ HPow.hPow (α := R) ((a : (a : σ) → R) r : R) m)
Tactic: rw [Finset.sum_eq_single (s : σ → ℕ)]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Coeff (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
s : σ →₀ ℕ
a : σ →₀ R
n : ℕ
hs : (s.sum fun (x : σ) (m : ℕ) ↦ m) = n
rw :
  (if s = indicator a.support fun (i : σ) (x : i ∈ a.support) ↦ (s : (a : σ) → ℕ) i then
      HMul.hMul (α := R) (↑(Nat.multinomial a.support (⇑s : (a : σ) → ℕ)) : R)
        (∏ x ∈ a.support, HPow.hPow (α := R) (β := ℕ) ((a : (a : σ) → R) x : R) ((s : (a : σ) → ℕ) x : ℕ))
    else 0) =
    HMul.hMul (α := R) (↑s.multinomial : R)
      (s.prod fun (r : σ) (m : ℕ) ↦ HPow.hPow (α := R) ((a : (a : σ) → R) r : R) m)
⊢ (∑ x ∈ a.support.piAntidiag n,
      if s = indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i then
        HMul.hMul (α := R) (↑(Nat.multinomial a.support x) : R)
          (∏ x_1 ∈ a.support, HPow.hPow (α := R) ((a : (a : σ) → R) x_1 : R) (x x_1))
      else 0) =
    HMul.hMul (α := R) (↑s.multinomial : R)
      (s.prod fun (r : σ) (m : ℕ) ↦ HPow.hPow (α := R) ((a : (a : σ) → R) r : R) m)
have h₀ : ∀ b ∈ a.support.piAntidiag n,
  b ≠ (⇑s : (a : σ) → ℕ) →
    (if s = indicator a.support fun (i : σ) (x : i ∈ a.support) ↦ b i then
        HMul.hMul (α := R) (↑(Nat.multinomial a.support b) : R)
          (∏ x ∈ a.support, HPow.hPow (α := R) ((a : (a : σ) → R) x : R) (b x))
      else 0) =
      0
Tactic: rw [Finset.sum_eq_single (s : σ → ℕ)]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Coeff (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
s : σ →₀ ℕ
a : σ →₀ R
n : ℕ
hs : (s.sum fun (x : σ) (m : ℕ) ↦ m) = n
rw :
  (if s = indicator a.support fun (i : σ) (x : i ∈ a.support) ↦ (s : (a : σ) → ℕ) i then
      HMul.hMul (α := R) (↑(Nat.multinomial a.support (⇑s : (a : σ) → ℕ)) : R)
        (∏ x ∈ a.support, HPow.hPow (α := R) (β := ℕ) ((a : (a : σ) → R) x : R) ((s : (a : σ) → ℕ) x : ℕ))
    else 0) =
    HMul.hMul (α := R) (↑s.multinomial : R)
      (s.prod fun (r : σ) (m : ℕ) ↦ HPow.hPow (α := R) ((a : (a : σ) → R) r : R) m)
h₀ :
  ∀ b ∈ a.support.piAntidiag n,
    b ≠ (⇑s : (a : σ) → ℕ) →
      (if s = indicator a.support fun (i : σ) (x : i ∈ a.support) ↦ b i then
          HMul.hMul (α := R) (↑(Nat.multinomial a.support b) : R)
            (∏ x ∈ a.support, HPow.hPow (α := R) ((a : (a : σ) → R) x : R) (b x))
        else 0) =
        0
⊢ (∑ x ∈ a.support.piAntidiag n,
      if s = indicator a.support fun (i : σ) (x_1 : i ∈ a.support) ↦ x i then
        HMul.hMul (α := R) (↑(Nat.multinomial a.support x) : R)
          (∏ x_1 ∈ a.support, HPow.hPow (α := R) ((a : (a : σ) → R) x_1 : R) (x x_1))
      else 0) =
    HMul.hMul (α := R) (↑s.multinomial : R)
      (s.prod fun (r : σ) (m : ℕ) ↦ HPow.hPow (α := R) ((a : (a : σ) → R) r : R) m)
have h₁ : (⇑s : (a : σ) → ℕ) ∉ a.support.piAntidiag n →
  (if s = indicator a.support fun (i : σ) (x : i ∈ a.support) ↦ (s : (a : σ) → ℕ) i then
      HMul.hMul (α := R) (↑(Nat.multinomial a.support (⇑s : (a : σ) → ℕ)) : R)
        (∏ x ∈ a.support, HPow.hPow (α := R) (β := ℕ) ((a : (a : σ) → R) x : R) ((s : (a : σ) → ℕ) x : ℕ))
    else 0) =
    0
Tactic: rw [Finset.sum_eq_single (s : σ → ℕ)]