awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
f : MvPolynomial.{u_1, u} (Option σ) R
h : f ≠ 0
rw :
  Eq (α := ℕ)
    ((Polynomial.support (R := MvPolynomial σ R)
          ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).sup
      fun (x : ℕ) ↦ x)
    (f.support.sup fun (m : Option σ →₀ ℕ) ↦ (m : (a : Option σ) → ℕ) none)
⊢ ((Polynomial.support (R := MvPolynomial σ R)
          ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).sup
      fun (x : ℕ) ↦ x) =
    degreeOf none f
have rw₁ : Eq (α := ℕ)
  (Finset.sup (Finset.image (fun (m : Option σ →₀ ℕ) ↦ (m : (a : Option σ) → ℕ) none) f.support) fun (x : ℕ) ↦ x)
  (f.support.sup fun (m : Option σ →₀ ℕ) ↦ (m : (a : Option σ) → ℕ) none)
Tactic: rw [degreeOf_eq_sup, support_optionEquivLeft, Finset.sup_image, Function.comp_def]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
f : MvPolynomial.{u_1, u} (Option σ) R
h : f ≠ 0
rw :
  Eq (α := ℕ)
    ((Polynomial.support (R := MvPolynomial σ R)
          ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).sup
      fun (x : ℕ) ↦ x)
    (f.support.sup fun (m : Option σ →₀ ℕ) ↦ (m : (a : Option σ) → ℕ) none)
rw₁ :
  Eq (α := ℕ)
    (Finset.sup (Finset.image (fun (m : Option σ →₀ ℕ) ↦ (m : (a : Option σ) → ℕ) none) f.support) fun (x : ℕ) ↦ x)
    (f.support.sup fun (m : Option σ →₀ ℕ) ↦ (m : (a : Option σ) → ℕ) none)
⊢ ((Polynomial.support (R := MvPolynomial σ R)
          ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).sup
      fun (x : ℕ) ↦ x) =
    degreeOf none f
have rw₂ : Eq (α := ℕ) (f.support.sup ((fun (x : ℕ) ↦ x) ∘ fun (m : Option σ →₀ ℕ) ↦ (m : (a : Option σ) → ℕ) none))
  (f.support.sup fun (m : Option σ →₀ ℕ) ↦ (m : (a : Option σ) → ℕ) none)
Tactic: rw [degreeOf_eq_sup, support_optionEquivLeft, Finset.sup_image, Function.comp_def]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
f : MvPolynomial.{u_1, u} (Option σ) R
h : f ≠ 0
rw :
  Eq (α := ℕ)
    ((Polynomial.support (R := MvPolynomial σ R)
          ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).sup
      fun (x : ℕ) ↦ x)
    (f.support.sup fun (m : Option σ →₀ ℕ) ↦ (m : (a : Option σ) → ℕ) none)
rw₁ :
  Eq (α := ℕ)
    (Finset.sup (Finset.image (fun (m : Option σ →₀ ℕ) ↦ (m : (a : Option σ) → ℕ) none) f.support) fun (x : ℕ) ↦ x)
    (f.support.sup fun (m : Option σ →₀ ℕ) ↦ (m : (a : Option σ) → ℕ) none)
rw₂ :
  Eq (α := ℕ) (f.support.sup ((fun (x : ℕ) ↦ x) ∘ fun (m : Option σ →₀ ℕ) ↦ (m : (a : Option σ) → ℕ) none))
    (f.support.sup fun (m : Option σ →₀ ℕ) ↦ (m : (a : Option σ) → ℕ) none)
⊢ ((Polynomial.support (R := MvPolynomial σ R)
          ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).sup
      fun (x : ℕ) ↦ x) =
    degreeOf none f
have rw₃ : Eq (α := ℕ) (f.support.sup fun (x : Option σ →₀ ℕ) ↦ (x : (a : Option σ) → ℕ) none)
  (f.support.sup fun (m : Option σ →₀ ℕ) ↦ (m : (a : Option σ) → ℕ) none)
Tactic: rw [degreeOf_eq_sup, support_optionEquivLeft, Finset.sup_image, Function.comp_def]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (hypothesis)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
f : MvPolynomial.{u_1, u} (Option σ) R
h : f ≠ 0
⊢ degree (R := MvPolynomial σ R) ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f) =
    (↑(degreeOf none f) : WithBot ℕ)
have h' : ((Polynomial.support (R := MvPolynomial σ R)
        ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).sup
    fun (x : ℕ) ↦ x) =
  degreeOf none f
Tactic: have h' : ((optionEquivLeft R σ f).support.sup fun x => x) = degreeOf none f := by
    rw [degreeOf_eq_sup, support_optionEquivLeft, Finset.sup_image, Function.comp_def]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
f : MvPolynomial.{u_1, u} (Option σ) R
h : f ≠ 0
h' :
  ((Polynomial.support (R := MvPolynomial σ R)
          ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).sup
      fun (x : ℕ) ↦ x) =
    degreeOf none f
⊢ degree (R := MvPolynomial σ R) ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f) =
    (↑(degreeOf none f) : WithBot ℕ)
have rw : (Polynomial.support (R := MvPolynomial σ R)
      ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).max =
  (↑(degreeOf none f) : WithBot ℕ)
Tactic: rw [Polynomial.degree, ← h', Nat.cast_withBot,
    Finset.coe_sup_of_nonempty (nonempty_support_optionEquivLeft R h), Finset.max_eq_sup_coe,
    Function.comp_def]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
f : MvPolynomial.{u_1, u} (Option σ) R
h : f ≠ 0
h' :
  ((Polynomial.support (R := MvPolynomial σ R)
          ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).sup
      fun (x : ℕ) ↦ x) =
    degreeOf none f
rw :
  (Polynomial.support (R := MvPolynomial σ R)
        ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).max =
    (↑(degreeOf none f) : WithBot ℕ)
⊢ degree (R := MvPolynomial σ R) ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f) =
    (↑(degreeOf none f) : WithBot ℕ)
have rw₁ : (Polynomial.support (R := MvPolynomial σ R)
      ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).max =
  (↑((Polynomial.support (R := MvPolynomial σ R)
            ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).sup
        fun (x : ℕ) ↦ x) :
    WithBot ℕ)
Tactic: rw [Polynomial.degree, ← h', Nat.cast_withBot,
    Finset.coe_sup_of_nonempty (nonempty_support_optionEquivLeft R h), Finset.max_eq_sup_coe,
    Function.comp_def]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
f : MvPolynomial.{u_1, u} (Option σ) R
h : f ≠ 0
h' :
  ((Polynomial.support (R := MvPolynomial σ R)
          ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).sup
      fun (x : ℕ) ↦ x) =
    degreeOf none f
rw :
  (Polynomial.support (R := MvPolynomial σ R)
        ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).max =
    (↑(degreeOf none f) : WithBot ℕ)
rw₁ :
  (Polynomial.support (R := MvPolynomial σ R)
        ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).max =
    (↑((Polynomial.support (R := MvPolynomial σ R)
              ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).sup
          fun (x : ℕ) ↦ x) :
      WithBot ℕ)
⊢ degree (R := MvPolynomial σ R) ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f) =
    (↑(degreeOf none f) : WithBot ℕ)
have rw₂ : (Polynomial.support (R := MvPolynomial σ R)
      ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).max =
  (↑((Polynomial.support (R := MvPolynomial σ R)
            ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).sup
        fun (x : ℕ) ↦ x) :
    WithBot ℕ)
Tactic: rw [Polynomial.degree, ← h', Nat.cast_withBot,
    Finset.coe_sup_of_nonempty (nonempty_support_optionEquivLeft R h), Finset.max_eq_sup_coe,
    Function.comp_def]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
f : MvPolynomial.{u_1, u} (Option σ) R
h : f ≠ 0
h' :
  ((Polynomial.support (R := MvPolynomial σ R)
          ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).sup
      fun (x : ℕ) ↦ x) =
    degreeOf none f
rw :
  (Polynomial.support (R := MvPolynomial σ R)
        ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).max =
    (↑(degreeOf none f) : WithBot ℕ)
rw₁ :
  (Polynomial.support (R := MvPolynomial σ R)
        ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).max =
    (↑((Polynomial.support (R := MvPolynomial σ R)
              ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).sup
          fun (x : ℕ) ↦ x) :
      WithBot ℕ)
rw₂ :
  (Polynomial.support (R := MvPolynomial σ R)
        ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).max =
    (↑((Polynomial.support (R := MvPolynomial σ R)
              ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).sup
          fun (x : ℕ) ↦ x) :
      WithBot ℕ)
⊢ degree (R := MvPolynomial σ R) ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f) =
    (↑(degreeOf none f) : WithBot ℕ)
have rw₃ : (Polynomial.support (R := MvPolynomial σ R)
      ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).max =
  (Polynomial.support (R := MvPolynomial σ R)
        ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).sup
    (WithBot.some ∘ fun (x : ℕ) ↦ x)
Tactic: rw [Polynomial.degree, ← h', Nat.cast_withBot,
    Finset.coe_sup_of_nonempty (nonempty_support_optionEquivLeft R h), Finset.max_eq_sup_coe,
    Function.comp_def]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
f : MvPolynomial.{u_1, u} (Option σ) R
h : f ≠ 0
h' :
  ((Polynomial.support (R := MvPolynomial σ R)
          ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).sup
      fun (x : ℕ) ↦ x) =
    degreeOf none f
rw :
  (Polynomial.support (R := MvPolynomial σ R)
        ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).max =
    (↑(degreeOf none f) : WithBot ℕ)
rw₁ :
  (Polynomial.support (R := MvPolynomial σ R)
        ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).max =
    (↑((Polynomial.support (R := MvPolynomial σ R)
              ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).sup
          fun (x : ℕ) ↦ x) :
      WithBot ℕ)
rw₂ :
  (Polynomial.support (R := MvPolynomial σ R)
        ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).max =
    (↑((Polynomial.support (R := MvPolynomial σ R)
              ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).sup
          fun (x : ℕ) ↦ x) :
      WithBot ℕ)
rw₃ :
  (Polynomial.support (R := MvPolynomial σ R)
        ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).max =
    (Polynomial.support (R := MvPolynomial σ R)
          ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).sup
      (WithBot.some ∘ fun (x : ℕ) ↦ x)
⊢ degree (R := MvPolynomial σ R) ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f) =
    (↑(degreeOf none f) : WithBot ℕ)
have rw₄ : (Polynomial.support (R := MvPolynomial σ R)
        ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).sup
    WithBot.some =
  (Polynomial.support (R := MvPolynomial σ R)
        ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).sup
    (WithBot.some ∘ fun (x : ℕ) ↦ x)
Tactic: rw [Polynomial.degree, ← h', Nat.cast_withBot,
    Finset.coe_sup_of_nonempty (nonempty_support_optionEquivLeft R h), Finset.max_eq_sup_coe,
    Function.comp_def]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
f : MvPolynomial.{u_1, u} (Option σ) R
h : f ≠ 0
h' :
  ((Polynomial.support (R := MvPolynomial σ R)
          ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).sup
      fun (x : ℕ) ↦ x) =
    degreeOf none f
rw :
  (Polynomial.support (R := MvPolynomial σ R)
        ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).max =
    (↑(degreeOf none f) : WithBot ℕ)
rw₁ :
  (Polynomial.support (R := MvPolynomial σ R)
        ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).max =
    (↑((Polynomial.support (R := MvPolynomial σ R)
              ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).sup
          fun (x : ℕ) ↦ x) :
      WithBot ℕ)
rw₂ :
  (Polynomial.support (R := MvPolynomial σ R)
        ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).max =
    (↑((Polynomial.support (R := MvPolynomial σ R)
              ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).sup
          fun (x : ℕ) ↦ x) :
      WithBot ℕ)
rw₃ :
  (Polynomial.support (R := MvPolynomial σ R)
        ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).max =
    (Polynomial.support (R := MvPolynomial σ R)
          ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).sup
      (WithBot.some ∘ fun (x : ℕ) ↦ x)
rw₄ :
  (Polynomial.support (R := MvPolynomial σ R)
          ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).sup
      WithBot.some =
    (Polynomial.support (R := MvPolynomial σ R)
          ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).sup
      (WithBot.some ∘ fun (x : ℕ) ↦ x)
⊢ degree (R := MvPolynomial σ R) ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f) =
    (↑(degreeOf none f) : WithBot ℕ)
have rw₅ : (Polynomial.support (R := MvPolynomial σ R)
        ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).sup
    WithBot.some =
  (Polynomial.support (R := MvPolynomial σ R)
        ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).sup
    fun (x : ℕ) ↦ (↑x : WithBot ℕ)
Tactic: rw [Polynomial.degree, ← h', Nat.cast_withBot,
    Finset.coe_sup_of_nonempty (nonempty_support_optionEquivLeft R h), Finset.max_eq_sup_coe,
    Function.comp_def]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial.{u_1, u} (Option σ) R
⊢ natDegree (R := MvPolynomial σ R)
      ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p) =
    degreeOf none p
have pos : ∀ (c : p = 0),
  natDegree (R := MvPolynomial σ R)
      ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p) =
    degreeOf none p
Tactic: by_cases c : p = 0
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial.{u_1, u} (Option σ) R
pos :
  ∀ (c : p = 0),
    natDegree (R := MvPolynomial σ R)
        ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p) =
      degreeOf none p
⊢ natDegree (R := MvPolynomial σ R)
      ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p) =
    degreeOf none p
have neg : ∀ (c : ¬p = 0),
  natDegree (R := MvPolynomial σ R)
      ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p) =
    degreeOf none p
Tactic: by_cases c : p = 0
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial.{u_1, u} (Option σ) R
c : p = 0
⊢ natDegree (R := MvPolynomial σ R)
      ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p) =
    degreeOf none p
have pos : natDegree (R := MvPolynomial σ R) ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) 0) =
  degreeOf.{u, u_1} (R := R) (σ := Option σ) none 0
Tactic: rw [c, map_zero, Polynomial.natDegree_zero, degreeOf_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial.{u_1, u} (Option σ) R
c : p = 0
pos :
  natDegree (R := MvPolynomial σ R)
      ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) 0) =
    degreeOf.{u, u_1} (R := R) (σ := Option σ) none 0
⊢ natDegree (R := MvPolynomial σ R)
      ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p) =
    degreeOf none p
have pos₁ : natDegree (R := MvPolynomial σ R) 0 = degreeOf.{u, u_1} (R := R) (σ := Option σ) none 0
Tactic: rw [c, map_zero, Polynomial.natDegree_zero, degreeOf_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial.{u_1, u} (Option σ) R
c : p = 0
pos :
  natDegree (R := MvPolynomial σ R)
      ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) 0) =
    degreeOf.{u, u_1} (R := R) (σ := Option σ) none 0
pos₁ : natDegree (R := MvPolynomial σ R) 0 = degreeOf.{u, u_1} (R := R) (σ := Option σ) none 0
⊢ natDegree (R := MvPolynomial σ R)
      ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p) =
    degreeOf none p
have pos₂ : 0 = degreeOf.{u, u_1} (R := R) (σ := Option σ) none 0
Tactic: rw [c, map_zero, Polynomial.natDegree_zero, degreeOf_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial.{u_1, u} (Option σ) R
c : p = 0
pos :
  natDegree (R := MvPolynomial σ R)
      ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) 0) =
    degreeOf.{u, u_1} (R := R) (σ := Option σ) none 0
pos₁ : natDegree (R := MvPolynomial σ R) 0 = degreeOf.{u, u_1} (R := R) (σ := Option σ) none 0
pos₂ : 0 = degreeOf.{u, u_1} (R := R) (σ := Option σ) none 0
⊢ natDegree (R := MvPolynomial σ R)
      ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p) =
    degreeOf none p
have pos₃ : Eq (α := ℕ) 0 0
Tactic: rw [c, map_zero, Polynomial.natDegree_zero, degreeOf_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial.{u_1, u} (Option σ) R
c : ¬p = 0
⊢ natDegree (R := MvPolynomial σ R)
      ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p) =
    degreeOf none p
have neg : WithBot.unbotD 0
    (degree (R := MvPolynomial σ R)
      ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p)) =
  degreeOf none p
Tactic: rw [Polynomial.natDegree, degree_optionEquivLeft R c, Nat.cast_withBot, WithBot.unbotD_coe]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial.{u_1, u} (Option σ) R
c : ¬p = 0
neg :
  WithBot.unbotD 0
      (degree (R := MvPolynomial σ R)
        ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p)) =
    degreeOf none p
⊢ natDegree (R := MvPolynomial σ R)
      ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p) =
    degreeOf none p
have neg₁ : WithBot.unbotD 0 (↑(degreeOf none p) : WithBot ℕ) = degreeOf none p
Tactic: rw [Polynomial.natDegree, degree_optionEquivLeft R c, Nat.cast_withBot, WithBot.unbotD_coe]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial.{u_1, u} (Option σ) R
c : ¬p = 0
neg :
  WithBot.unbotD 0
      (degree (R := MvPolynomial σ R)
        ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p)) =
    degreeOf none p
neg₁ : WithBot.unbotD 0 (↑(degreeOf none p) : WithBot ℕ) = degreeOf none p
⊢ natDegree (R := MvPolynomial σ R)
      ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p) =
    degreeOf none p
have neg₂ : WithBot.unbotD 0 (↑(degreeOf none p) : WithBot ℕ) = degreeOf none p
Tactic: rw [Polynomial.natDegree, degree_optionEquivLeft R c, Nat.cast_withBot, WithBot.unbotD_coe]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial.{u_1, u} (Option σ) R
c : ¬p = 0
neg :
  WithBot.unbotD 0
      (degree (R := MvPolynomial σ R)
        ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p)) =
    degreeOf none p
neg₁ : WithBot.unbotD 0 (↑(degreeOf none p) : WithBot ℕ) = degreeOf none p
neg₂ : WithBot.unbotD 0 (↑(degreeOf none p) : WithBot ℕ) = degreeOf none p
⊢ natDegree (R := MvPolynomial σ R)
      ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p) =
    degreeOf none p
have neg₃ : degreeOf none p = degreeOf none p
Tactic: rw [Polynomial.natDegree, degree_optionEquivLeft R c, Nat.cast_withBot, WithBot.unbotD_coe]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
p : MvPolynomial.{v, u} (Option S₁) R
i : ℕ
hi : i ≤ p.totalDegree
⊢ totalDegree.{u, v} (R := R) (σ := S₁)
        (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) +
      i ≤
    p.totalDegree
have pos : ∀
  (hpi :
    Eq (α := MvPolynomial S₁ R)
      (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) 0),
  totalDegree.{u, v} (R := R) (σ := S₁)
        (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) +
      i ≤
    p.totalDegree
Tactic: by_cases hpi : (optionEquivLeft R S₁ p).coeff i = 0
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
p : MvPolynomial.{v, u} (Option S₁) R
i : ℕ
hi : i ≤ p.totalDegree
pos :
  ∀
    (hpi :
      Eq (α := MvPolynomial S₁ R)
        (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) 0),
    totalDegree.{u, v} (R := R) (σ := S₁)
          (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) +
        i ≤
      p.totalDegree
⊢ totalDegree.{u, v} (R := R) (σ := S₁)
        (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) +
      i ≤
    p.totalDegree
have neg : ∀
  (hpi :
    ¬Eq (α := MvPolynomial S₁ R)
        (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) 0),
  totalDegree.{u, v} (R := R) (σ := S₁)
        (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) +
      i ≤
    p.totalDegree
Tactic: by_cases hpi : (optionEquivLeft R S₁ p).coeff i = 0
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
p : MvPolynomial.{v, u} (Option S₁) R
i : ℕ
hi : i ≤ p.totalDegree
hpi :
  Eq (α := MvPolynomial S₁ R)
    (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) 0
⊢ totalDegree.{u, v} (R := R) (σ := S₁)
        (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) +
      i ≤
    p.totalDegree
have pos : totalDegree.{u, v} (R := R) (σ := S₁) 0 + i ≤ p.totalDegree
Tactic: rw [hpi]