awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
inst_2 : SemilatticeSup M
inst_3 : OrderBot M
w : σ → M
p : MvPolynomial σ R
m : M
hm : (↑m : WithBot M) = weightedTotalDegree' w p
hm' : weightedTotalDegree' w p ≤ (↑m : WithBot M)
⊢ (↑(p.support.sup fun (s : σ →₀ ℕ) ↦ (weight w : (a : σ →₀ ℕ) → M) s) : WithBot M) ≤ weightedTotalDegree' w p
have a : (↑(p.support.sup fun (s : σ →₀ ℕ) ↦ (weight w : (a : σ →₀ ℕ) → M) s) : WithBot M) ≤ (↑m : WithBot M)
Tactic: rw [← hm]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
m : M
a b : MvPolynomial σ R
ha : Membership.mem (γ := Set (MvPolynomial σ R)) {x : MvPolynomial σ R | IsWeightedHomogeneous w x m} a
hb : Membership.mem (γ := Set (MvPolynomial σ R)) {x : MvPolynomial σ R | IsWeightedHomogeneous w x m} b
c : σ →₀ ℕ
hc : coeff c (a + b) ≠ 0
⊢ (weight w : (a : σ →₀ ℕ) → M) c = m
have hc₁ : coeff c a + coeff c b ≠ 0
Tactic: rw [coeff_add] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
m : M
a b : MvPolynomial σ R
ha : Membership.mem (γ := Set (MvPolynomial σ R)) {x : MvPolynomial σ R | IsWeightedHomogeneous w x m} a
hb : Membership.mem (γ := Set (MvPolynomial σ R)) {x : MvPolynomial σ R | IsWeightedHomogeneous w x m} b
c : σ →₀ ℕ
hc : coeff c a + coeff c b ≠ 0
⊢ coeff c a ≠ 0 ∨ coeff c b ≠ 0
have contrapose! : ∀ (hc : coeff c a = 0 ∧ coeff c b = 0), coeff c a + coeff c b = 0
Tactic: contrapose! hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
m : M
r : R
a : MvPolynomial σ R
ha : Membership.mem (γ := Set (MvPolynomial σ R)) {x : MvPolynomial σ R | IsWeightedHomogeneous w x m} a
c : σ →₀ ℕ
hc : coeff c (r • a) ≠ 0
⊢ (weight w : (a : σ →₀ ℕ) → M) c = m
have hc₁ : r • coeff c a ≠ 0
Tactic: rw [coeff_smul] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
m : M
⊢ Eq (α := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w m)
    (Finsupp.supported R R {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → M) d = m})
have h : ∀ (x : MvPolynomial σ R),
  Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w m) x ↔
    Membership.mem (γ := Submodule R (MvPolynomial σ R))
      (Finsupp.supported R R {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → M) d = m}) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
m : M
x : MvPolynomial σ R
⊢ Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w m) x ↔
    ∀ x_1 ∈ (↑x.support : Set (σ →₀ ℕ)),
      Membership.mem (γ := Set (σ →₀ ℕ)) {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → M) d = m} x_1
have h : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w m) x ↔
  ∀ (x_1 : σ →₀ ℕ),
    Ne.{u_1 + 1} (α := R) ((x : (a : σ →₀ ℕ) → R) x_1 : R) (0 : R) →
      Membership.mem (γ := Set (σ →₀ ℕ)) {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → M) d = m} x_1
Tactic: simp only [Finsupp.mem_support_iff, mem_coe]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
m n : M
⊢ HMul.hMul (α := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w m)
      (weightedHomogeneousSubmodule R w n) ≤
    weightedHomogeneousSubmodule R w (m + n)
have rw : ∀ (m_1 : MvPolynomial σ R),
  Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w m) m_1 →
    ∀ (n_1 : MvPolynomial σ R),
      Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w n) n_1 →
        Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w (m + n)) (m_1 * n_1)
Tactic: rw [Submodule.mul_le]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
m n : M
φ : MvPolynomial σ R
hφ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w m) φ
ψ : MvPolynomial σ R
hψ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w n) ψ
c : σ →₀ ℕ
hc : coeff c (φ * ψ) ≠ 0
⊢ (weight w : (a : σ →₀ ℕ) → M) c = m + n
have hc₁ : Ne.{u_1 + 1} (α := R) (∑ x ∈ @antidiagonal _ instAddMonoid _ c, coeff x.1 φ * coeff x.2 ψ) 0
Tactic: rw [coeff_mul] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
m n : M
φ : MvPolynomial σ R
hφ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w m) φ
ψ : MvPolynomial σ R
hψ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w n) ψ
c : σ →₀ ℕ
hc : Ne.{u_1 + 1} (α := R) (∑ x ∈ @antidiagonal _ instAddMonoid _ c, coeff x.1 φ * coeff x.2 ψ) 0
⊢ (weight w : (a : σ →₀ ℕ) → M) c = m + n
have obtain : ∀ (d e : σ →₀ ℕ) (hde : (d, e) ∈ @antidiagonal _ instAddMonoid _ c) (H : coeff (d, e).1 φ * coeff (d, e).2 ψ ≠ 0),
  (weight w : (a : σ →₀ ℕ) → M) c = m + n
Tactic: obtain ⟨⟨d, e⟩, hde, H⟩ := Finset.exists_ne_zero_of_sum_ne_zero hc
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
m n : M
φ : MvPolynomial σ R
hφ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w m) φ
ψ : MvPolynomial σ R
hψ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w n) ψ
c : σ →₀ ℕ
hc : Ne.{u_1 + 1} (α := R) (∑ x ∈ @antidiagonal _ instAddMonoid _ c, coeff x.1 φ * coeff x.2 ψ) 0
d e : σ →₀ ℕ
hde : (d, e) ∈ @antidiagonal _ instAddMonoid _ c
H : coeff (d, e).1 φ * coeff (d, e).2 ψ ≠ 0
⊢ coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0
have contrapose! : ∀ (H : ∀ (_ : coeff d φ ≠ 0), coeff e ψ = 0), coeff (d, e).1 φ * coeff (d, e).2 ψ = 0
Tactic: contrapose! H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
m n : M
φ : MvPolynomial σ R
hφ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w m) φ
ψ : MvPolynomial σ R
hψ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w n) ψ
c : σ →₀ ℕ
hc : Ne.{u_1 + 1} (α := R) (∑ x ∈ @antidiagonal _ instAddMonoid _ c, coeff x.1 φ * coeff x.2 ψ) 0
d e : σ →₀ ℕ
hde : (d, e) ∈ @antidiagonal _ instAddMonoid _ c
H : ∀ (_ : coeff d φ ≠ 0), coeff e ψ = 0
⊢ coeff (d, e).1 φ * coeff (d, e).2 ψ = 0
have pos : ∀ (h : coeff d φ = 0), coeff (d, e).1 φ * coeff (d, e).2 ψ = 0
Tactic: by_cases h : coeff d φ = 0
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
m n : M
φ : MvPolynomial σ R
hφ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w m) φ
ψ : MvPolynomial σ R
hψ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w n) ψ
c : σ →₀ ℕ
hc : Ne.{u_1 + 1} (α := R) (∑ x ∈ @antidiagonal _ instAddMonoid _ c, coeff x.1 φ * coeff x.2 ψ) 0
d e : σ →₀ ℕ
hde : (d, e) ∈ @antidiagonal _ instAddMonoid _ c
H : ∀ (_ : coeff d φ ≠ 0), coeff e ψ = 0
pos : ∀ (h : coeff d φ = 0), coeff (d, e).1 φ * coeff (d, e).2 ψ = 0
⊢ coeff (d, e).1 φ * coeff (d, e).2 ψ = 0
have neg : ∀ (h : ¬coeff d φ = 0), coeff (d, e).1 φ * coeff (d, e).2 ψ = 0
Tactic: by_cases h : coeff d φ = 0
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
m n : M
φ : MvPolynomial σ R
hφ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w m) φ
ψ : MvPolynomial σ R
hψ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w n) ψ
c : σ →₀ ℕ
hc : Ne.{u_1 + 1} (α := R) (∑ x ∈ @antidiagonal _ instAddMonoid _ c, coeff x.1 φ * coeff x.2 ψ) 0
d e : σ →₀ ℕ
hde : (d, e) ∈ @antidiagonal _ instAddMonoid _ c
H : coeff (d, e).1 φ * coeff (d, e).2 ψ ≠ 0
⊢ (weight w : (a : σ →₀ ℕ) → M) c = m + n
have aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0
Tactic: have aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0 := by
    contrapose! H
    by_cases h : coeff d φ = 0 <;>
      simp_all only [Ne, not_false_iff, zero_mul, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
m n : M
φ : MvPolynomial σ R
hφ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w m) φ
ψ : MvPolynomial σ R
hψ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w n) ψ
c : σ →₀ ℕ
hc : Ne.{u_1 + 1} (α := R) (∑ x ∈ @antidiagonal _ instAddMonoid _ c, coeff x.1 φ * coeff x.2 ψ) 0
d e : σ →₀ ℕ
hde : (d, e) ∈ @antidiagonal _ instAddMonoid _ c
H : coeff (d, e).1 φ * coeff (d, e).2 ψ ≠ 0
aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0
⊢ (weight w : (a : σ →₀ ℕ) → M) c = m + n
have rw : (weight w : (a : σ →₀ ℕ) → M) ((d, e).1 + (d, e).2) = m + n
Tactic: rw [← mem_antidiagonal.mp hde, ← hφ aux.1, ← hψ aux.2, map_add]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
m n : M
φ : MvPolynomial σ R
hφ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w m) φ
ψ : MvPolynomial σ R
hψ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w n) ψ
c : σ →₀ ℕ
hc : Ne.{u_1 + 1} (α := R) (∑ x ∈ @antidiagonal _ instAddMonoid _ c, coeff x.1 φ * coeff x.2 ψ) 0
d e : σ →₀ ℕ
hde : (d, e) ∈ @antidiagonal _ instAddMonoid _ c
H : coeff (d, e).1 φ * coeff (d, e).2 ψ ≠ 0
aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0
rw : (weight w : (a : σ →₀ ℕ) → M) ((d, e).1 + (d, e).2) = m + n
⊢ (weight w : (a : σ →₀ ℕ) → M) c = m + n
have rw₁ : (weight w : (a : σ →₀ ℕ) → M) ((d, e).1 + (d, e).2) = HAdd.hAdd (α := M) ((weight w : (a : σ →₀ ℕ) → M) d : M) n
Tactic: rw [← mem_antidiagonal.mp hde, ← hφ aux.1, ← hψ aux.2, map_add]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
m n : M
φ : MvPolynomial σ R
hφ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w m) φ
ψ : MvPolynomial σ R
hψ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w n) ψ
c : σ →₀ ℕ
hc : Ne.{u_1 + 1} (α := R) (∑ x ∈ @antidiagonal _ instAddMonoid _ c, coeff x.1 φ * coeff x.2 ψ) 0
d e : σ →₀ ℕ
hde : (d, e) ∈ @antidiagonal _ instAddMonoid _ c
H : coeff (d, e).1 φ * coeff (d, e).2 ψ ≠ 0
aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0
rw : (weight w : (a : σ →₀ ℕ) → M) ((d, e).1 + (d, e).2) = m + n
rw₁ : (weight w : (a : σ →₀ ℕ) → M) ((d, e).1 + (d, e).2) = HAdd.hAdd (α := M) ((weight w : (a : σ →₀ ℕ) → M) d : M) n
⊢ (weight w : (a : σ →₀ ℕ) → M) c = m + n
have rw₂ : (weight w : (a : σ →₀ ℕ) → M) ((d, e).1 + (d, e).2) =
  HAdd.hAdd (α := M) (β := M) ((weight w : (a : σ →₀ ℕ) → M) d : M) ((weight w : (a : σ →₀ ℕ) → M) e : M)
Tactic: rw [← mem_antidiagonal.mp hde, ← hφ aux.1, ← hψ aux.2, map_add]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
m n : M
φ : MvPolynomial σ R
hφ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w m) φ
ψ : MvPolynomial σ R
hψ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w n) ψ
c : σ →₀ ℕ
hc : Ne.{u_1 + 1} (α := R) (∑ x ∈ @antidiagonal _ instAddMonoid _ c, coeff x.1 φ * coeff x.2 ψ) 0
d e : σ →₀ ℕ
hde : (d, e) ∈ @antidiagonal _ instAddMonoid _ c
H : coeff (d, e).1 φ * coeff (d, e).2 ψ ≠ 0
aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0
rw : (weight w : (a : σ →₀ ℕ) → M) ((d, e).1 + (d, e).2) = m + n
rw₁ : (weight w : (a : σ →₀ ℕ) → M) ((d, e).1 + (d, e).2) = HAdd.hAdd (α := M) ((weight w : (a : σ →₀ ℕ) → M) d : M) n
rw₂ :
  (weight w : (a : σ →₀ ℕ) → M) ((d, e).1 + (d, e).2) =
    HAdd.hAdd (α := M) (β := M) ((weight w : (a : σ →₀ ℕ) → M) d : M) ((weight w : (a : σ →₀ ℕ) → M) e : M)
⊢ (weight w : (a : σ →₀ ℕ) → M) c = m + n
have rw₃ : HAdd.hAdd (α := M) (β := M) ((weight w : (a : σ →₀ ℕ) → M) (d, e).1 : M) ((weight w : (a : σ →₀ ℕ) → M) (d, e).2 : M) =
  HAdd.hAdd (α := M) (β := M) ((weight w : (a : σ →₀ ℕ) → M) d : M) ((weight w : (a : σ →₀ ℕ) → M) e : M)
Tactic: rw [← mem_antidiagonal.mp hde, ← hφ aux.1, ← hψ aux.2, map_add]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
m n : M
⊢ HMul.hMul (α := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w m)
      (weightedHomogeneousSubmodule R w n) ≤
    weightedHomogeneousSubmodule R w (m + n)
have rw : ∀ (m_1 : MvPolynomial σ R),
  Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w m) m_1 →
    ∀ (n_1 : MvPolynomial σ R),
      Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w n) n_1 →
        Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w (m + n)) (m_1 * n_1)
Tactic: classical
  rw [Submodule.mul_le]
  intro φ hφ ψ hψ c hc
  rw [coeff_mul] at hc
  obtain ⟨⟨d, e⟩, hde, H⟩ := Finset.exists_ne_zero_of_sum_ne_zero hc
  have aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0 := by
    contrapose! H
    by_cases h : coeff d φ = 0 <;>
      simp_all only [Ne, not_false_iff, zero_mul, mul_zero]
  rw [← mem_antidiagonal.mp hde, ← hφ aux.1, ← hψ aux.2, map_add]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
m n : M
rw rw₁ rw₂ :
  ∀ (m_1 : MvPolynomial σ R),
    Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w m) m_1 →
      ∀ (n_1 : MvPolynomial σ R),
        Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w n) n_1 →
          Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w (m + n)) (m_1 * n_1)
⊢ HMul.hMul (α := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w m)
      (weightedHomogeneousSubmodule R w n) ≤
    weightedHomogeneousSubmodule R w (m + n)
have rw₃ : ∀ (φ : MvPolynomial σ R)
  (hφ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w m) φ)
  (ψ : MvPolynomial σ R)
  (hψ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w n) ψ) ⦃c : σ →₀ ℕ⦄
  (hc : coeff c (φ * ψ) ≠ 0), (weight w : (a : σ →₀ ℕ) → M) c = m + n
Tactic: classical
  rw [Submodule.mul_le]
  intro φ hφ ψ hψ c hc
  rw [coeff_mul] at hc
  obtain ⟨⟨d, e⟩, hde, H⟩ := Finset.exists_ne_zero_of_sum_ne_zero hc
  have aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0 := by
    contrapose! H
    by_cases h : coeff d φ = 0 <;>
      simp_all only [Ne, not_false_iff, zero_mul, mul_zero]
  rw [← mem_antidiagonal.mp hde, ← hφ aux.1, ← hψ aux.2, map_add]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
m n : M
rw rw₁ rw₂ :
  ∀ (m_1 : MvPolynomial σ R),
    Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w m) m_1 →
      ∀ (n_1 : MvPolynomial σ R),
        Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w n) n_1 →
          Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w (m + n)) (m_1 * n_1)
rw₃ :
  ∀ (φ : MvPolynomial σ R)
    (hφ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w m) φ)
    (ψ : MvPolynomial σ R)
    (hψ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w n) ψ) ⦃c : σ →₀ ℕ⦄
    (hc : coeff c (φ * ψ) ≠ 0), (weight w : (a : σ →₀ ℕ) → M) c = m + n
⊢ HMul.hMul (α := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w m)
      (weightedHomogeneousSubmodule R w n) ≤
    weightedHomogeneousSubmodule R w (m + n)
have rw₄ : ∀ (φ : MvPolynomial σ R)
  (hφ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w m) φ)
  (ψ : MvPolynomial σ R)
  (hψ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w n) ψ) ⦃c : σ →₀ ℕ⦄
  (hc : Ne.{u_1 + 1} (α := R) (∑ x ∈ @antidiagonal _ instAddMonoid _ c, coeff x.1 φ * coeff x.2 ψ) 0),
  (weight w : (a : σ →₀ ℕ) → M) c = m + n
Tactic: classical
  rw [Submodule.mul_le]
  intro φ hφ ψ hψ c hc
  rw [coeff_mul] at hc
  obtain ⟨⟨d, e⟩, hde, H⟩ := Finset.exists_ne_zero_of_sum_ne_zero hc
  have aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0 := by
    contrapose! H
    by_cases h : coeff d φ = 0 <;>
      simp_all only [Ne, not_false_iff, zero_mul, mul_zero]
  rw [← mem_antidiagonal.mp hde, ← hφ aux.1, ← hψ aux.2, map_add]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
m n : M
rw rw₁ rw₂ :
  ∀ (m_1 : MvPolynomial σ R),
    Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w m) m_1 →
      ∀ (n_1 : MvPolynomial σ R),
        Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w n) n_1 →
          Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w (m + n)) (m_1 * n_1)
rw₃ :
  ∀ (φ : MvPolynomial σ R)
    (hφ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w m) φ)
    (ψ : MvPolynomial σ R)
    (hψ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w n) ψ) ⦃c : σ →₀ ℕ⦄
    (hc : coeff c (φ * ψ) ≠ 0), (weight w : (a : σ →₀ ℕ) → M) c = m + n
rw₄ :
  ∀ (φ : MvPolynomial σ R)
    (hφ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w m) φ)
    (ψ : MvPolynomial σ R)
    (hψ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w n) ψ) ⦃c : σ →₀ ℕ⦄
    (hc : Ne.{u_1 + 1} (α := R) (∑ x ∈ @antidiagonal _ instAddMonoid _ c, coeff x.1 φ * coeff x.2 ψ) 0),
    (weight w : (a : σ →₀ ℕ) → M) c = m + n
⊢ HMul.hMul (α := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w m)
      (weightedHomogeneousSubmodule R w n) ≤
    weightedHomogeneousSubmodule R w (m + n)
have rw₅ : ∀ (φ : MvPolynomial σ R)
  (hφ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w m) φ)
  (ψ : MvPolynomial σ R)
  (hψ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w n) ψ) ⦃c : σ →₀ ℕ⦄
  (hc : Ne.{u_1 + 1} (α := R) (∑ x ∈ @antidiagonal _ instAddMonoid _ c, coeff x.1 φ * coeff x.2 ψ) 0) (d e : σ →₀ ℕ)
  (hde : (d, e) ∈ @antidiagonal _ instAddMonoid _ c) (H : coeff (d, e).1 φ * coeff (d, e).2 ψ ≠ 0),
  (weight w : (a : σ →₀ ℕ) → M) c = m + n
Tactic: classical
  rw [Submodule.mul_le]
  intro φ hφ ψ hψ c hc
  rw [coeff_mul] at hc
  obtain ⟨⟨d, e⟩, hde, H⟩ := Finset.exists_ne_zero_of_sum_ne_zero hc
  have aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0 := by
    contrapose! H
    by_cases h : coeff d φ = 0 <;>
      simp_all only [Ne, not_false_iff, zero_mul, mul_zero]
  rw [← mem_antidiagonal.mp hde, ← hφ aux.1, ← hψ aux.2, map_add]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
m n : M
rw rw₁ rw₂ :
  ∀ (m_1 : MvPolynomial σ R),
    Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w m) m_1 →
      ∀ (n_1 : MvPolynomial σ R),
        Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w n) n_1 →
          Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w (m + n)) (m_1 * n_1)
rw₃ :
  ∀ (φ : MvPolynomial σ R)
    (hφ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w m) φ)
    (ψ : MvPolynomial σ R)
    (hψ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w n) ψ) ⦃c : σ →₀ ℕ⦄
    (hc : coeff c (φ * ψ) ≠ 0), (weight w : (a : σ →₀ ℕ) → M) c = m + n
rw₄ :
  ∀ (φ : MvPolynomial σ R)
    (hφ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w m) φ)
    (ψ : MvPolynomial σ R)
    (hψ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w n) ψ) ⦃c : σ →₀ ℕ⦄
    (hc : Ne.{u_1 + 1} (α := R) (∑ x ∈ @antidiagonal _ instAddMonoid _ c, coeff x.1 φ * coeff x.2 ψ) 0),
    (weight w : (a : σ →₀ ℕ) → M) c = m + n
rw₅ :
  ∀ (φ : MvPolynomial σ R)
    (hφ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w m) φ)
    (ψ : MvPolynomial σ R)
    (hψ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w n) ψ) ⦃c : σ →₀ ℕ⦄
    (hc : Ne.{u_1 + 1} (α := R) (∑ x ∈ @antidiagonal _ instAddMonoid _ c, coeff x.1 φ * coeff x.2 ψ) 0) (d e : σ →₀ ℕ)
    (hde : (d, e) ∈ @antidiagonal _ instAddMonoid _ c) (H : coeff (d, e).1 φ * coeff (d, e).2 ψ ≠ 0),
    (weight w : (a : σ →₀ ℕ) → M) c = m + n
⊢ HMul.hMul (α := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w m)
      (weightedHomogeneousSubmodule R w n) ≤
    weightedHomogeneousSubmodule R w (m + n)
have rw₆ : ∀ (φ : MvPolynomial σ R)
  (hφ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w m) φ)
  (ψ : MvPolynomial σ R)
  (hψ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w n) ψ) ⦃c : σ →₀ ℕ⦄
  (hc : Ne.{u_1 + 1} (α := R) (∑ x ∈ @antidiagonal _ instAddMonoid _ c, coeff x.1 φ * coeff x.2 ψ) 0) (d e : σ →₀ ℕ)
  (hde : (d, e) ∈ @antidiagonal _ instAddMonoid _ c) (H : coeff (d, e).1 φ * coeff (d, e).2 ψ ≠ 0)
  (aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0), (weight w : (a : σ →₀ ℕ) → M) c = m + n
Tactic: classical
  rw [Submodule.mul_le]
  intro φ hφ ψ hψ c hc
  rw [coeff_mul] at hc
  obtain ⟨⟨d, e⟩, hde, H⟩ := Finset.exists_ne_zero_of_sum_ne_zero hc
  have aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0 := by
    contrapose! H
    by_cases h : coeff d φ = 0 <;>
      simp_all only [Ne, not_false_iff, zero_mul, mul_zero]
  rw [← mem_antidiagonal.mp hde, ← hφ aux.1, ← hψ aux.2, map_add]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
d : σ →₀ ℕ
r : R
m : M
hm : (weight w : (a : σ →₀ ℕ) → M) d = m
c : σ →₀ ℕ
hc : Ne.{u_1 + 1} (α := R) (coeff c ((monomial d : (a : R) → MvPolynomial σ R) r)) 0
⊢ (weight w : (a : σ →₀ ℕ) → M) c = m
have hc₁ : (if d = c then r else 0) ≠ 0
Tactic: rw [coeff_monomial] at hc
Cleared hypotheses: hc