awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
| fun (a : Fin n →₀ ℕ) ↦
    Membership.mem (γ := Finset (Fin n →₀ ℕ))
        (support.{u, 0} (R := R)
          (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)
            i))
        a ∧
      cons i a = m
have p : ∀ (x : Fin n →₀ ℕ),
  Membership.mem (γ := Finset (Fin n →₀ ℕ))
      (support.{u, 0} (R := R)
        (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i))
      x ∧
    cons i x = m
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
x : Fin n →₀ ℕ
| Membership.mem (γ := Finset (Fin n →₀ ℕ))
      (support.{u, 0} (R := R)
        (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i))
      x ∧
    cons i x = m
have p : ¬coeff (cons i x) f = 0 ∧ cons i x = m
Tactic: rw [mem_support_iff, finSuccEquiv_coeff_coeff, Ne]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
| ∃ (a : Fin n →₀ ℕ),
    Membership.mem (γ := Finset (Fin n →₀ ℕ))
        (support.{u, 0} (R := R)
          (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)
            i))
        a ∧
      cons i a = m
have p : ∀ (x : Fin n →₀ ℕ), ¬coeff (cons i x) f = 0 ∧ cons i x = m
Tactic: congr
    ext
    rw [mem_support_iff, finSuccEquiv_coeff_coeff, Ne]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
⊢ (∃ (a : Fin n →₀ ℕ),
      Membership.mem (γ := Finset (Fin n →₀ ℕ))
          (support.{u, 0} (R := R)
            (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)
              i))
          a ∧
        cons i a = m) ↔
    coeff m f ≠ 0 ∧ (m : (a : Fin (n + 1)) → ℕ) 0 = i
have h : (∃ (x : Fin n →₀ ℕ), ¬coeff (cons i x) f = 0 ∧ cons i x = m) ↔ coeff m f ≠ 0 ∧ (m : (a : Fin (n + 1)) → ℕ) 0 = i
Tactic: conv_lhs =>
    congr
    ext
    rw [mem_support_iff, finSuccEquiv_coeff_coeff, Ne]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
⊢ (∃ (x : Fin n →₀ ℕ), ¬coeff (cons i x) f = 0 ∧ cons i x = m) ↔ coeff m f ≠ 0 ∧ (m : (a : Fin (n + 1)) → ℕ) 0 = i
have h : (∃ (x : Fin n →₀ ℕ), ¬coeff (cons i x) f = 0 ∧ cons i x = m) → coeff m f ≠ 0 ∧ (m : (a : Fin (n + 1)) → ℕ) 0 = i
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
h : (∃ (x : Fin n →₀ ℕ), ¬coeff (cons i x) f = 0 ∧ cons i x = m) → coeff m f ≠ 0 ∧ (m : (a : Fin (n + 1)) → ℕ) 0 = i
⊢ (∃ (x : Fin n →₀ ℕ), ¬coeff (cons i x) f = 0 ∧ cons i x = m) ↔ coeff m f ≠ 0 ∧ (m : (a : Fin (n + 1)) → ℕ) 0 = i
have h₁ : coeff m f ≠ 0 ∧ (m : (a : Fin (n + 1)) → ℕ) 0 = i → ∃ (x : Fin n →₀ ℕ), ¬coeff (cons i x) f = 0 ∧ cons i x = m
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
h : coeff m f ≠ 0 ∧ (m : (a : Fin (n + 1)) → ℕ) 0 = i
⊢ ∃ (x : Fin n →₀ ℕ), ¬coeff (cons i x) f = 0 ∧ cons i x = m
have h₁ : ¬coeff (cons i m.tail) f = 0 ∧ cons i m.tail = m
Tactic: use tail m
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
h : coeff m f ≠ 0 ∧ (m : (a : Fin (n + 1)) → ℕ) 0 = i
⊢ ¬coeff (cons i m.tail) f = 0 ∧ cons i m.tail = m
have h₁ : ¬coeff m f = 0 ∧ m = m
Tactic: rw [← h.2, cons_tail]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
⊢ (Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
      ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).Nonempty
have rwa : Ne (α := (MvPolynomial (Fin n) R)[X])
  ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f :
    (MvPolynomial (Fin n) R)[X])
  (0 : (MvPolynomial (Fin n) R)[X])
Tactic: rwa [Polynomial.support_nonempty, EmbeddingLike.map_ne_zero_iff]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
⊢ degree.{u} (R := MvPolynomial (Fin n) R)
      ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) =
    (↑(degreeOf 0 f) : WithBot ℕ)
have h₀ : ∀ {α β : Type} (f : α → β), (fun (x : β) ↦ x) ∘ f = f
Tactic: have h₀ : ∀ {α β : Type _} (f : α → β), (fun x => x) ∘ f = f := fun f => rfl
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
h₀ : ∀ {α β : Type} (f : α → β), (fun (x : β) ↦ x) ∘ f = f
⊢ degree.{u} (R := MvPolynomial (Fin n) R)
      ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) =
    (↑(degreeOf 0 f) : WithBot ℕ)
have h₁ : ∀ {α β : Type} (f : α → β), (f ∘ fun (x : α) ↦ x) = f
Tactic: have h₁ : ∀ {α β : Type _} (f : α → β), f ∘ (fun x => x) = f := fun f => rfl
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
h₀ : ∀ {α β : Type} (f : α → β), (fun (x : β) ↦ x) ∘ f = f
h₁ : ∀ {α β : Type} (f : α → β), (f ∘ fun (x : α) ↦ x) = f
⊢ ((Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
          ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).sup
      fun (x : ℕ) ↦ x) =
    degreeOf 0 f
have rw : Eq (α := ℕ)
  ((Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
        ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).sup
    fun (x : ℕ) ↦ x)
  (f.support.sup fun (m : Fin (n + 1) →₀ ℕ) ↦ (m : (a : Fin (n + 1)) → ℕ) 0)
Tactic: rw [degreeOf_eq_sup, support_finSuccEquiv, Finset.sup_image, h₀]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
h₀ : ∀ {α β : Type} (f : α → β), (fun (x : β) ↦ x) ∘ f = f
h₁ : ∀ {α β : Type} (f : α → β), (f ∘ fun (x : α) ↦ x) = f
rw :
  Eq (α := ℕ)
    ((Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
          ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).sup
      fun (x : ℕ) ↦ x)
    (f.support.sup fun (m : Fin (n + 1) →₀ ℕ) ↦ (m : (a : Fin (n + 1)) → ℕ) 0)
⊢ ((Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
          ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).sup
      fun (x : ℕ) ↦ x) =
    degreeOf 0 f
have rw₁ : Eq (α := ℕ)
  (Finset.sup (Finset.image (fun (m : Fin (n + 1) →₀ ℕ) ↦ (m : (a : Fin (n + 1)) → ℕ) 0) f.support) fun (x : ℕ) ↦ x)
  (f.support.sup fun (m : Fin (n + 1) →₀ ℕ) ↦ (m : (a : Fin (n + 1)) → ℕ) 0)
Tactic: rw [degreeOf_eq_sup, support_finSuccEquiv, Finset.sup_image, h₀]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
h₀ : ∀ {α β : Type} (f : α → β), (fun (x : β) ↦ x) ∘ f = f
h₁ : ∀ {α β : Type} (f : α → β), (f ∘ fun (x : α) ↦ x) = f
rw :
  Eq (α := ℕ)
    ((Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
          ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).sup
      fun (x : ℕ) ↦ x)
    (f.support.sup fun (m : Fin (n + 1) →₀ ℕ) ↦ (m : (a : Fin (n + 1)) → ℕ) 0)
rw₁ :
  Eq (α := ℕ)
    (Finset.sup (Finset.image (fun (m : Fin (n + 1) →₀ ℕ) ↦ (m : (a : Fin (n + 1)) → ℕ) 0) f.support) fun (x : ℕ) ↦ x)
    (f.support.sup fun (m : Fin (n + 1) →₀ ℕ) ↦ (m : (a : Fin (n + 1)) → ℕ) 0)
⊢ ((Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
          ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).sup
      fun (x : ℕ) ↦ x) =
    degreeOf 0 f
have rw₂ : Eq (α := ℕ) (f.support.sup ((fun (x : ℕ) ↦ x) ∘ fun (m : Fin (n + 1) →₀ ℕ) ↦ (m : (a : Fin (n + 1)) → ℕ) 0))
  (f.support.sup fun (m : Fin (n + 1) →₀ ℕ) ↦ (m : (a : Fin (n + 1)) → ℕ) 0)
Tactic: rw [degreeOf_eq_sup, support_finSuccEquiv, Finset.sup_image, h₀]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
h₀ : ∀ {α β : Type} (f : α → β), (fun (x : β) ↦ x) ∘ f = f
h₁ : ∀ {α β : Type} (f : α → β), (f ∘ fun (x : α) ↦ x) = f
rw :
  Eq (α := ℕ)
    ((Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
          ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).sup
      fun (x : ℕ) ↦ x)
    (f.support.sup fun (m : Fin (n + 1) →₀ ℕ) ↦ (m : (a : Fin (n + 1)) → ℕ) 0)
rw₁ :
  Eq (α := ℕ)
    (Finset.sup (Finset.image (fun (m : Fin (n + 1) →₀ ℕ) ↦ (m : (a : Fin (n + 1)) → ℕ) 0) f.support) fun (x : ℕ) ↦ x)
    (f.support.sup fun (m : Fin (n + 1) →₀ ℕ) ↦ (m : (a : Fin (n + 1)) → ℕ) 0)
rw₂ :
  Eq (α := ℕ) (f.support.sup ((fun (x : ℕ) ↦ x) ∘ fun (m : Fin (n + 1) →₀ ℕ) ↦ (m : (a : Fin (n + 1)) → ℕ) 0))
    (f.support.sup fun (m : Fin (n + 1) →₀ ℕ) ↦ (m : (a : Fin (n + 1)) → ℕ) 0)
⊢ ((Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
          ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).sup
      fun (x : ℕ) ↦ x) =
    degreeOf 0 f
have rw₃ : Eq (α := ℕ) (f.support.sup fun (m : Fin (n + 1) →₀ ℕ) ↦ (m : (a : Fin (n + 1)) → ℕ) 0)
  (f.support.sup fun (m : Fin (n + 1) →₀ ℕ) ↦ (m : (a : Fin (n + 1)) → ℕ) 0)
Tactic: rw [degreeOf_eq_sup, support_finSuccEquiv, Finset.sup_image, h₀]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
h₀ : ∀ {α β : Type} (f : α → β), (fun (x : β) ↦ x) ∘ f = f
h₁ : ∀ {α β : Type} (f : α → β), (f ∘ fun (x : α) ↦ x) = f
⊢ degree.{u} (R := MvPolynomial (Fin n) R)
      ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) =
    (↑(degreeOf 0 f) : WithBot ℕ)
have h' : ((Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
        ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).sup
    fun (x : ℕ) ↦ x) =
  degreeOf 0 f
Tactic: have h' : ((finSuccEquiv R n f).support.sup fun x => x) = degreeOf 0 f := by
    rw [degreeOf_eq_sup, support_finSuccEquiv, Finset.sup_image, h₀]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
h₀ : ∀ {α β : Type} (f : α → β), (fun (x : β) ↦ x) ∘ f = f
h₁ : ∀ {α β : Type} (f : α → β), (f ∘ fun (x : α) ↦ x) = f
h' :
  ((Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
          ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).sup
      fun (x : ℕ) ↦ x) =
    degreeOf 0 f
⊢ degree.{u} (R := MvPolynomial (Fin n) R)
      ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) =
    (↑(degreeOf 0 f) : WithBot ℕ)
have rw : (Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
      ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).max =
  (↑(degreeOf 0 f) : WithBot ℕ)
Tactic: rw [Polynomial.degree, ← h', Nat.cast_withBot,
    Finset.coe_sup_of_nonempty (nonempty_support_finSuccEquiv h), Finset.max_eq_sup_coe, h₁]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
h₀ : ∀ {α β : Type} (f : α → β), (fun (x : β) ↦ x) ∘ f = f
h₁ : ∀ {α β : Type} (f : α → β), (f ∘ fun (x : α) ↦ x) = f
h' :
  ((Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
          ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).sup
      fun (x : ℕ) ↦ x) =
    degreeOf 0 f
rw :
  (Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
        ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).max =
    (↑(degreeOf 0 f) : WithBot ℕ)
⊢ degree.{u} (R := MvPolynomial (Fin n) R)
      ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) =
    (↑(degreeOf 0 f) : WithBot ℕ)
have rw₁ : (Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
      ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).max =
  (↑((Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
            ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).sup
        fun (x : ℕ) ↦ x) :
    WithBot ℕ)
Tactic: rw [Polynomial.degree, ← h', Nat.cast_withBot,
    Finset.coe_sup_of_nonempty (nonempty_support_finSuccEquiv h), Finset.max_eq_sup_coe, h₁]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
h₀ : ∀ {α β : Type} (f : α → β), (fun (x : β) ↦ x) ∘ f = f
h₁ : ∀ {α β : Type} (f : α → β), (f ∘ fun (x : α) ↦ x) = f
h' :
  ((Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
          ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).sup
      fun (x : ℕ) ↦ x) =
    degreeOf 0 f
rw :
  (Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
        ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).max =
    (↑(degreeOf 0 f) : WithBot ℕ)
rw₁ :
  (Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
        ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).max =
    (↑((Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
              ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).sup
          fun (x : ℕ) ↦ x) :
      WithBot ℕ)
⊢ degree.{u} (R := MvPolynomial (Fin n) R)
      ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) =
    (↑(degreeOf 0 f) : WithBot ℕ)
have rw₂ : (Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
      ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).max =
  (↑((Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
            ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).sup
        fun (x : ℕ) ↦ x) :
    WithBot ℕ)
Tactic: rw [Polynomial.degree, ← h', Nat.cast_withBot,
    Finset.coe_sup_of_nonempty (nonempty_support_finSuccEquiv h), Finset.max_eq_sup_coe, h₁]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
h₀ : ∀ {α β : Type} (f : α → β), (fun (x : β) ↦ x) ∘ f = f
h₁ : ∀ {α β : Type} (f : α → β), (f ∘ fun (x : α) ↦ x) = f
h' :
  ((Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
          ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).sup
      fun (x : ℕ) ↦ x) =
    degreeOf 0 f
rw :
  (Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
        ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).max =
    (↑(degreeOf 0 f) : WithBot ℕ)
rw₁ :
  (Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
        ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).max =
    (↑((Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
              ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).sup
          fun (x : ℕ) ↦ x) :
      WithBot ℕ)
rw₂ :
  (Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
        ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).max =
    (↑((Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
              ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).sup
          fun (x : ℕ) ↦ x) :
      WithBot ℕ)
⊢ degree.{u} (R := MvPolynomial (Fin n) R)
      ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) =
    (↑(degreeOf 0 f) : WithBot ℕ)
have rw₃ : (Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
      ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).max =
  (Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
        ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).sup
    (WithBot.some ∘ fun (x : ℕ) ↦ x)
Tactic: rw [Polynomial.degree, ← h', Nat.cast_withBot,
    Finset.coe_sup_of_nonempty (nonempty_support_finSuccEquiv h), Finset.max_eq_sup_coe, h₁]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
h₀ : ∀ {α β : Type} (f : α → β), (fun (x : β) ↦ x) ∘ f = f
h₁ : ∀ {α β : Type} (f : α → β), (f ∘ fun (x : α) ↦ x) = f
h' :
  ((Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
          ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).sup
      fun (x : ℕ) ↦ x) =
    degreeOf 0 f
rw :
  (Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
        ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).max =
    (↑(degreeOf 0 f) : WithBot ℕ)
rw₁ :
  (Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
        ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).max =
    (↑((Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
              ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).sup
          fun (x : ℕ) ↦ x) :
      WithBot ℕ)
rw₂ :
  (Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
        ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).max =
    (↑((Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
              ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).sup
          fun (x : ℕ) ↦ x) :
      WithBot ℕ)
rw₃ :
  (Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
        ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).max =
    (Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
          ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).sup
      (WithBot.some ∘ fun (x : ℕ) ↦ x)
⊢ degree.{u} (R := MvPolynomial (Fin n) R)
      ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) =
    (↑(degreeOf 0 f) : WithBot ℕ)
have rw₄ : (Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
        ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).sup
    WithBot.some =
  (Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
        ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).sup
    (WithBot.some ∘ fun (x : ℕ) ↦ x)
Tactic: rw [Polynomial.degree, ← h', Nat.cast_withBot,
    Finset.coe_sup_of_nonempty (nonempty_support_finSuccEquiv h), Finset.max_eq_sup_coe, h₁]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
h₀ : ∀ {α β : Type} (f : α → β), (fun (x : β) ↦ x) ∘ f = f
h₁ : ∀ {α β : Type} (f : α → β), (f ∘ fun (x : α) ↦ x) = f
h' :
  ((Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
          ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).sup
      fun (x : ℕ) ↦ x) =
    degreeOf 0 f
rw :
  (Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
        ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).max =
    (↑(degreeOf 0 f) : WithBot ℕ)
rw₁ :
  (Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
        ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).max =
    (↑((Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
              ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).sup
          fun (x : ℕ) ↦ x) :
      WithBot ℕ)
rw₂ :
  (Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
        ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).max =
    (↑((Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
              ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).sup
          fun (x : ℕ) ↦ x) :
      WithBot ℕ)
rw₃ :
  (Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
        ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).max =
    (Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
          ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).sup
      (WithBot.some ∘ fun (x : ℕ) ↦ x)
rw₄ :
  (Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
          ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).sup
      WithBot.some =
    (Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
          ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).sup
      (WithBot.some ∘ fun (x : ℕ) ↦ x)
⊢ degree.{u} (R := MvPolynomial (Fin n) R)
      ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) =
    (↑(degreeOf 0 f) : WithBot ℕ)
have rw₅ : (Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
        ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).sup
    WithBot.some =
  (Polynomial.support.{u} (R := MvPolynomial (Fin n) R)
        ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)).sup
    WithBot.some
Tactic: rw [Polynomial.degree, ← h', Nat.cast_withBot,
    Finset.coe_sup_of_nonempty (nonempty_support_finSuccEquiv h), Finset.max_eq_sup_coe, h₁]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
⊢ natDegree.{u} (R := MvPolynomial (Fin n) R)
      ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) =
    degreeOf 0 f
have pos : ∀ (c : f = 0),
  natDegree.{u} (R := MvPolynomial (Fin n) R)
      ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) =
    degreeOf 0 f
Tactic: by_cases c : f = 0
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
pos :
  ∀ (c : f = 0),
    natDegree.{u} (R := MvPolynomial (Fin n) R)
        ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) =
      degreeOf 0 f
⊢ natDegree.{u} (R := MvPolynomial (Fin n) R)
      ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) =
    degreeOf 0 f
have neg : ∀ (c : ¬f = 0),
  natDegree.{u} (R := MvPolynomial (Fin n) R)
      ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) =
    degreeOf 0 f
Tactic: by_cases c : f = 0