awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.FreeCommRing (goal)
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_3
inst : DecidableEq κ
inst_1 : CommRing R
inst_2 : DecidableEq R
monoms : ι → Finset (κ →₀ ℕ)
p : (i : ι) × ↥(monoms i) → R
⊢ (fun (p : { p : ι → MvPolynomial κ R // ∀ (i : ι), (p i).support ⊆ monoms i }) (i : (i : ι) × ↥(monoms i)) ↦
        coeff (↑(i.snd (β := fun (i : ι) ↦ ↥(monoms i))) : κ →₀ ℕ)
          ((↑p : ι → MvPolynomial κ R) (i.fst (β := fun (i : ι) ↦ ↥(monoms i)))))
      ((fun (p : (i : ι) × ↥(monoms i) → R) ↦
          (Subtype.mk (p := fun (p : ι → MvPolynomial κ R) ↦ ∀ (i : ι), (p i).support ⊆ monoms i)
              (fun (i : ι) ↦
                {
                  support :=
                    {m ∈ monoms i |
                      ∃ (hm : m ∈ monoms i),
                        p
                            (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i
                              (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) m hm)) ≠
                          0},
                  toFun := fun (m : κ →₀ ℕ) ↦
                    if hm : m ∈ monoms i then
                      p
                        (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i
                          (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) m hm))
                    else 0,
                  mem_support_toFun := ⋯ })
              ⋯ :
            { p : ι → MvPolynomial κ R // ∀ (i : ι), (p i).support ⊆ monoms i }))
        p) =
    p
have h : ∀ (x : (i : ι) × ↥(monoms i)),
  (fun (p : { p : ι → MvPolynomial κ R // ∀ (i : ι), (p i).support ⊆ monoms i }) (i : (i : ι) × ↥(monoms i)) ↦
        coeff (↑(i.snd (β := fun (i : ι) ↦ ↥(monoms i))) : κ →₀ ℕ)
          ((↑p : ι → MvPolynomial κ R) (i.fst (β := fun (i : ι) ↦ ↥(monoms i)))))
      ((fun (p : (i : ι) × ↥(monoms i) → R) ↦
          (Subtype.mk (p := fun (p : ι → MvPolynomial κ R) ↦ ∀ (i : ι), (p i).support ⊆ monoms i)
              (fun (i : ι) ↦
                {
                  support :=
                    {m ∈ monoms i |
                      ∃ (hm : m ∈ monoms i),
                        p
                            (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i
                              (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) m hm)) ≠
                          0},
                  toFun := fun (m : κ →₀ ℕ) ↦
                    if hm : m ∈ monoms i then
                      p
                        (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i
                          (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) m hm))
                    else 0,
                  mem_support_toFun := sorry })
              sorry :
            { p : ι → MvPolynomial κ R // ∀ (i : ι), (p i).support ⊆ monoms i }))
        p)
      x =
    p x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.FreeCommRing (goal)
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_3
inst : DecidableEq κ
inst_1 : CommRing R
inst_2 : DecidableEq R
monoms : ι → Finset (κ →₀ ℕ)
f : (i : ι) × ↥(monoms i) ⊕ κ → R
i : ι
⊢ Eq.{u_3 + 1} (α := R)
    ((((lift : (a : (i : ι) × ↥(monoms i) ⊕ κ → R) → FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ) →+* R) f :
            FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ) →+* R) :
          (a : FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ)) → R)
        (genericPolyMap monoms i) :
      R)
    ((eval (f ∘ Sum.inr) : (a : MvPolynomial κ R) → R)
        ((↑((Equiv.symm (mvPolynomialSupportLEEquiv monoms) :
                  (a : (i : ι) × ↥(monoms i) → R) → { p : ι → MvPolynomial κ R // ∀ (i : ι), (p i).support ⊆ monoms i })
                (f ∘ Sum.inl)) :
            ι → MvPolynomial κ R)
          i) :
      R)
have simp : Eq.{u_3 + 1} (α := R)
  (∑ x ∈ (monoms i).attach,
    HMul.hMul (β := R) (f (Sum.inl (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i x)))
      ((((lift : (a : (i : ι) × ↥(monoms i) ⊕ κ → R) → FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ) →+* R) f :
              FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ) →+* R) :
            (a : FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ)) → R)
          ((↑x : κ →₀ ℕ).prod fun (j : κ) (n : ℕ) ↦
            HPow.hPow (α := FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ)) (of (Sum.inr j)) n) :
        R))
  (∑ a ∈ monoms i,
    if
        ∃ (h : a ∈ monoms i),
          ¬f
                (Sum.inl
                  (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i
                    (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) a sorry))) =
              0 then
      HMul.hMul (α := R)
        (if h : a ∈ monoms i then
          f
            (Sum.inl
              (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) a sorry)))
        else 0)
        (∏ x ∈ a.support, HPow.hPow (β := ℕ) (f (Sum.inr x)) ((a : (a : κ) → ℕ) x : ℕ))
    else 0)
Tactic: simp only [genericPolyMap, map_sum, map_mul, lift_of, support,
    mvPolynomialSupportLEEquiv, coeff, Finset.sum_filter, MvPolynomial.eval_eq,
    ne_eq, Function.comp, Equiv.coe_fn_symm_mk, Finsupp.coe_mk]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.FreeCommRing (goal)
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_3
inst : DecidableEq κ
inst_1 : CommRing R
inst_2 : DecidableEq R
monoms : ι → Finset (κ →₀ ℕ)
f : (i : ι) × ↥(monoms i) ⊕ κ → R
i : ι
| ∑ a ∈ monoms i,
    if
        ∃ (h : a ∈ monoms i),
          ¬f
                (Sum.inl
                  (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i
                    (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) a ⋯))) =
              0 then
      HMul.hMul (α := R)
        (if h : a ∈ monoms i then
          f
            (Sum.inl
              (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) a ⋯)))
        else 0)
        (∏ x ∈ a.support, HPow.hPow (β := ℕ) (f (Sum.inr x)) ((a : (a : κ) → ℕ) x : ℕ))
    else 0
have rw : ∑ x ∈ (monoms i).attach,
  if
      ∃ (h : (↑x : κ →₀ ℕ) ∈ monoms i),
        ¬f
              (Sum.inl
                (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i
                  (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) (↑x : κ →₀ ℕ) sorry))) =
            0 then
    HMul.hMul (α := R)
      (if h : (↑x : κ →₀ ℕ) ∈ monoms i then
        f
          (Sum.inl
            (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i
              (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) (↑x : κ →₀ ℕ) sorry)))
      else 0)
      (∏ x_1 ∈ (↑x : κ →₀ ℕ).support, HPow.hPow (β := ℕ) (f (Sum.inr x_1)) (((↑x : κ →₀ ℕ) : (a : κ) → ℕ) x_1 : ℕ))
  else 0
Tactic: rw [← Finset.sum_attach]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.FreeCommRing (goal)
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_3
inst : DecidableEq κ
inst_1 : CommRing R
inst_2 : DecidableEq R
monoms : ι → Finset (κ →₀ ℕ)
f : (i : ι) × ↥(monoms i) ⊕ κ → R
i : ι
⊢ Eq.{u_3 + 1} (α := R)
    (∑ x ∈ (monoms i).attach,
      HMul.hMul (β := R) (f (Sum.inl (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i x)))
        ((((lift : (a : (i : ι) × ↥(monoms i) ⊕ κ → R) → FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ) →+* R) f :
                FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ) →+* R) :
              (a : FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ)) → R)
            ((↑x : κ →₀ ℕ).prod fun (j : κ) (n : ℕ) ↦
              HPow.hPow (α := FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ)) (of (Sum.inr j)) n) :
          R))
    (∑ a ∈ monoms i,
      if
          ∃ (h : a ∈ monoms i),
            ¬f
                  (Sum.inl
                    (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i
                      (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) a ⋯))) =
                0 then
        HMul.hMul (α := R)
          (if h : a ∈ monoms i then
            f
              (Sum.inl
                (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) a ⋯)))
          else 0)
          (∏ x ∈ a.support, HPow.hPow (β := ℕ) (f (Sum.inr x)) ((a : (a : κ) → ℕ) x : ℕ))
      else 0)
have conv_rhs : Eq.{u_3 + 1} (α := R)
  (∑ x ∈ (monoms i).attach,
    HMul.hMul (β := R) (f (Sum.inl (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i x)))
      ((((lift : (a : (i : ι) × ↥(monoms i) ⊕ κ → R) → FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ) →+* R) f :
              FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ) →+* R) :
            (a : FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ)) → R)
          ((↑x : κ →₀ ℕ).prod fun (j : κ) (n : ℕ) ↦
            HPow.hPow (α := FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ)) (of (Sum.inr j)) n) :
        R))
  (∑ x ∈ (monoms i).attach,
    if
        ∃ (h : (↑x : κ →₀ ℕ) ∈ monoms i),
          ¬f
                (Sum.inl
                  (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i
                    (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) (↑x : κ →₀ ℕ) sorry))) =
              0 then
      HMul.hMul (α := R)
        (if h : (↑x : κ →₀ ℕ) ∈ monoms i then
          f
            (Sum.inl
              (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i
                (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) (↑x : κ →₀ ℕ) sorry)))
        else 0)
        (∏ x_1 ∈ (↑x : κ →₀ ℕ).support, HPow.hPow (β := ℕ) (f (Sum.inr x_1)) (((↑x : κ →₀ ℕ) : (a : κ) → ℕ) x_1 : ℕ))
    else 0)
Tactic: conv_rhs => rw [← Finset.sum_attach]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.FreeCommRing (goal)
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_3
inst : DecidableEq κ
inst_1 : CommRing R
inst_2 : DecidableEq R
monoms : ι → Finset (κ →₀ ℕ)
f : (i : ι) × ↥(monoms i) ⊕ κ → R
i : ι
⊢ Eq.{u_3 + 1} (α := R)
    (∑ x ∈ (monoms i).attach,
      HMul.hMul (β := R) (f (Sum.inl (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i x)))
        ((((lift : (a : (i : ι) × ↥(monoms i) ⊕ κ → R) → FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ) →+* R) f :
                FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ) →+* R) :
              (a : FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ)) → R)
            ((↑x : κ →₀ ℕ).prod fun (j : κ) (n : ℕ) ↦
              HPow.hPow (α := FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ)) (of (Sum.inr j)) n) :
          R))
    (∑ x ∈ (monoms i).attach,
      if
          ∃ (h : (↑x : κ →₀ ℕ) ∈ monoms i),
            ¬f
                  (Sum.inl
                    (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i
                      (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) (↑x : κ →₀ ℕ) ⋯))) =
                0 then
        HMul.hMul (α := R)
          (if h : (↑x : κ →₀ ℕ) ∈ monoms i then
            f
              (Sum.inl
                (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i
                  (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) (↑x : κ →₀ ℕ) ⋯)))
          else 0)
          (∏ x_1 ∈ (↑x : κ →₀ ℕ).support, HPow.hPow (β := ℕ) (f (Sum.inr x_1)) (((↑x : κ →₀ ℕ) : (a : κ) → ℕ) x_1 : ℕ))
      else 0)
have refine : ∀ x ∈ (monoms i).attach,
  HMul.hMul (β := R) (f (Sum.inl (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i x)))
      ((((lift : (a : (i : ι) × ↥(monoms i) ⊕ κ → R) → FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ) →+* R) f :
              FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ) →+* R) :
            (a : FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ)) → R)
          ((↑x : κ →₀ ℕ).prod fun (j : κ) (n : ℕ) ↦
            HPow.hPow (α := FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ)) (of (Sum.inr j)) n) :
        R) =
    if
        ∃ (h : (↑x : κ →₀ ℕ) ∈ monoms i),
          ¬f
                (Sum.inl
                  (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i
                    (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) (↑x : κ →₀ ℕ) sorry))) =
              0 then
      HMul.hMul (α := R)
        (if h : (↑x : κ →₀ ℕ) ∈ monoms i then
          f
            (Sum.inl
              (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i
                (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) (↑x : κ →₀ ℕ) sorry)))
        else 0)
        (∏ x_1 ∈ (↑x : κ →₀ ℕ).support, HPow.hPow (β := ℕ) (f (Sum.inr x_1)) (((↑x : κ →₀ ℕ) : (a : κ) → ℕ) x_1 : ℕ))
    else 0
Tactic: refine Finset.sum_congr rfl ?_
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.FreeCommRing (goal)
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_3
inst : DecidableEq κ
inst_1 : CommRing R
inst_2 : DecidableEq R
monoms : ι → Finset (κ →₀ ℕ)
f : (i : ι) × ↥(monoms i) ⊕ κ → R
i : ι
m : ↥(monoms i)
h : m ∈ (monoms i).attach
⊢ HMul.hMul (β := R) (f (Sum.inl (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i m)))
      ((((lift : (a : (i : ι) × ↥(monoms i) ⊕ κ → R) → FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ) →+* R) f :
              FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ) →+* R) :
            (a : FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ)) → R)
          ((↑m : κ →₀ ℕ).prod fun (j : κ) (n : ℕ) ↦
            HPow.hPow (α := FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ)) (of (Sum.inr j)) n) :
        R) =
    if
        ∃ (h : (↑m : κ →₀ ℕ) ∈ monoms i),
          ¬f
                (Sum.inl
                  (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i
                    (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) (↑m : κ →₀ ℕ) ⋯))) =
              0 then
      HMul.hMul (α := R)
        (if h : (↑m : κ →₀ ℕ) ∈ monoms i then
          f
            (Sum.inl
              (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i
                (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) (↑m : κ →₀ ℕ) ⋯)))
        else 0)
        (∏ x ∈ (↑m : κ →₀ ℕ).support, HPow.hPow (β := ℕ) (f (Sum.inr x)) (((↑m : κ →₀ ℕ) : (a : κ) → ℕ) x : ℕ))
    else 0
have simp : f (Sum.inl (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i m)) *
    ∏ x ∈ (↑m : κ →₀ ℕ).support, HPow.hPow (β := ℕ) (f (Sum.inr x)) (((↑m : κ →₀ ℕ) : (a : κ) → ℕ) x : ℕ) =
  if f (Sum.inl (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i m)) = 0 then 0
  else
    f (Sum.inl (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i m)) *
      ∏ x ∈ (↑m : κ →₀ ℕ).support, HPow.hPow (β := ℕ) (f (Sum.inr x)) (((↑m : κ →₀ ℕ) : (a : κ) → ℕ) x : ℕ)
Tactic: simp only [Finsupp.prod, map_prod, map_pow, lift_of, Subtype.coe_eta, Finset.coe_mem,
    exists_prop, true_and, dite_eq_ite, ite_true, ite_not]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.FreeCommRing (goal)
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_3
inst : DecidableEq κ
inst_1 : CommRing R
inst_2 : DecidableEq R
monoms : ι → Finset (κ →₀ ℕ)
f : (i : ι) × ↥(monoms i) ⊕ κ → R
i : ι
m : ↥(monoms i)
h : m ∈ (monoms i).attach
⊢ f (Sum.inl (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i m)) *
      ∏ x ∈ (↑m : κ →₀ ℕ).support, HPow.hPow (β := ℕ) (f (Sum.inr x)) (((↑m : κ →₀ ℕ) : (a : κ) → ℕ) x : ℕ) =
    if f (Sum.inl (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i m)) = 0 then 0
    else
      f (Sum.inl (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i m)) *
        ∏ x ∈ (↑m : κ →₀ ℕ).support, HPow.hPow (β := ℕ) (f (Sum.inr x)) (((↑m : κ →₀ ℕ) : (a : κ) → ℕ) x : ℕ)
have pos : ∀ (h0 : f (Sum.inl (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i m)) = 0),
  f (Sum.inl (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i m)) *
      ∏ x ∈ (↑m : κ →₀ ℕ).support, HPow.hPow (β := ℕ) (f (Sum.inr x)) (((↑m : κ →₀ ℕ) : (a : κ) → ℕ) x : ℕ) =
    0
Tactic: split_ifs with h0
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.FreeCommRing (goal)
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_3
inst : DecidableEq κ
inst_1 : CommRing R
inst_2 : DecidableEq R
monoms : ι → Finset (κ →₀ ℕ)
f : (i : ι) × ↥(monoms i) ⊕ κ → R
i : ι
m : ↥(monoms i)
h : m ∈ (monoms i).attach
pos :
  ∀ (h0 : f (Sum.inl (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i m)) = 0),
    f (Sum.inl (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i m)) *
        ∏ x ∈ (↑m : κ →₀ ℕ).support, HPow.hPow (β := ℕ) (f (Sum.inr x)) (((↑m : κ →₀ ℕ) : (a : κ) → ℕ) x : ℕ) =
      0
⊢ f (Sum.inl (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i m)) *
      ∏ x ∈ (↑m : κ →₀ ℕ).support, HPow.hPow (β := ℕ) (f (Sum.inr x)) (((↑m : κ →₀ ℕ) : (a : κ) → ℕ) x : ℕ) =
    if f (Sum.inl (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i m)) = 0 then 0
    else
      f (Sum.inl (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i m)) *
        ∏ x ∈ (↑m : κ →₀ ℕ).support, HPow.hPow (β := ℕ) (f (Sum.inr x)) (((↑m : κ →₀ ℕ) : (a : κ) → ℕ) x : ℕ)
have neg : ∀ (h0 : ¬f (Sum.inl (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i m)) = 0),
  f (Sum.inl (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i m)) *
      ∏ x ∈ (↑m : κ →₀ ℕ).support, HPow.hPow (β := ℕ) (f (Sum.inr x)) (((↑m : κ →₀ ℕ) : (a : κ) → ℕ) x : ℕ) =
    f (Sum.inl (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i m)) *
      ∏ x ∈ (↑m : κ →₀ ℕ).support, HPow.hPow (β := ℕ) (f (Sum.inr x)) (((↑m : κ →₀ ℕ) : (a : κ) → ℕ) x : ℕ)
Tactic: split_ifs with h0
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Groebner (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f : MvPolynomial σ R
⊢ LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.subLTerm f)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
have apply : LE.le.{u_3} (α := m.syn)
  (max ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f))
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
        (degree.{u_1, u_2, u_3} m (R := R) ((monomial (m.degree f) : (a : R) → MvPolynomial σ R) (m.leadingCoeff f)))) :
    m.syn)
  ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
Tactic: apply le_trans degree_sub_le
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Groebner (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f : MvPolynomial σ R
⊢ LE.le.{u_3} (α := m.syn)
    (max ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f))
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
          (degree.{u_1, u_2, u_3} m (R := R)
            ((monomial (m.degree f) : (a : R) → MvPolynomial σ R) (m.leadingCoeff f)))) :
      m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
have simp : LE.le.{u_3} (α := m.syn)
  ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
      (degree.{u_1, u_2, u_3} m (R := R) ((monomial (m.degree f) : (a : R) → MvPolynomial σ R) (m.leadingCoeff f))) :
    m.syn)
  ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
Tactic: simp only [sup_le_iff, le_refl, true_and]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Groebner (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f : MvPolynomial σ R
hf : m.degree f ≠ 0
⊢ LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.subLTerm f)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
have rw : LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.subLTerm f)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn) ∧
  Ne.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.subLTerm f)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
Tactic: rw [lt_iff_le_and_ne]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Groebner (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f : MvPolynomial σ R
hf : m.degree f ≠ 0
⊢ LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.subLTerm f)) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn) ∧
    Ne.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.subLTerm f)) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
have refine : Ne.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.subLTerm f)) : m.syn)
  ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
Tactic: refine ⟨degree_sub_LTerm_le f, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Groebner (hypothesis)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f : MvPolynomial σ R
hf : m.degree f ≠ 0
hf' :
  Eq.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.subLTerm f)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
⊢ False
have hf'₁ : m.degree (m.subLTerm f) = m.degree f
Tactic: simp only [EmbeddingLike.apply_eq_iff_eq] at hf'
Cleared hypotheses: hf'
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Groebner (hypothesis)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f : MvPolynomial σ R
hf : m.degree f ≠ 0
hf' : m.degree (m.subLTerm f) = m.degree f
h : m.subLTerm f = 0
⊢ False
have hf'₁ : 0 = m.degree f
Tactic: simp only [h, degree_zero] at hf'
Cleared hypotheses: hf'
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Groebner (hypothesis)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f : MvPolynomial σ R
hf : m.degree f ≠ 0
hf' : m.degree (m.subLTerm f) = m.degree f
⊢ False
have this : m.subLTerm f ≠ 0
Tactic: have : m.subLTerm f ≠ 0 := by
    intro h
    simp only [h, degree_zero] at hf'
    exact hf hf'.symm
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Groebner (hypothesis)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f : MvPolynomial σ R
hf : m.degree f ≠ 0
hf' : m.degree (m.subLTerm f) = m.degree f
this : m.subLTerm f ≠ 0
⊢ False
have this₁ : coeff (m.degree f) (m.subLTerm f) ≠ 0
Tactic: rw [← coeff_degree_ne_zero_iff (m := m), hf'] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Groebner (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f : MvPolynomial σ R
hf : m.degree f ≠ 0
hf' : m.degree (m.subLTerm f) = m.degree f
this : coeff (m.degree f) (m.subLTerm f) ≠ 0
⊢ False
have apply : coeff (m.degree f) (m.subLTerm f) = 0
Tactic: apply this
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Groebner (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f : MvPolynomial σ R
hf : m.degree f ≠ 0
intro :
  ∀
    (hf' :
      Eq.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.subLTerm f)) : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)),
    False
⊢ Ne.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.subLTerm f)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
have intro₁ : ∀ (hf' : m.degree (m.subLTerm f) = m.degree f), False
Tactic: classical
  intro hf'
  simp only [EmbeddingLike.apply_eq_iff_eq] at hf'
  have : m.subLTerm f ≠ 0 := by
    intro h
    simp only [h, degree_zero] at hf'
    exact hf hf'.symm
  rw [← coeff_degree_ne_zero_iff (m := m), hf'] at this
  apply this
  simp [subLTerm, coeff_monomial, leadingCoeff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Groebner (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
f : MvPolynomial σ R
hf : m.degree f ≠ 0
intro :
  ∀
    (hf' :
      Eq.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.subLTerm f)) : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)),
    False
intro₁ : ∀ (hf' : m.degree (m.subLTerm f) = m.degree f), False
⊢ Ne.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (m.subLTerm f)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
have intro₂ : ∀ (hf' : m.degree (m.subLTerm f) = m.degree f) (this : m.subLTerm f ≠ 0), False
Tactic: classical
  intro hf'
  simp only [EmbeddingLike.apply_eq_iff_eq] at hf'
  have : m.subLTerm f ≠ 0 := by
    intro h
    simp only [h, degree_zero] at hf'
    exact hf hf'.symm
  rw [← coeff_degree_ne_zero_iff (m := m), hf'] at this
  apply this
  simp [subLTerm, coeff_monomial, leadingCoeff]