awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
j : Option S₁ →₀ ℕ
r : R
n : Option S₁ →₀ ℕ
monomial :
  if j = n then
    (if Eq (α := ℕ) ((j : (a : Option S₁) → ℕ) none : ℕ) ((n : (a : Option S₁) → ℕ) none : ℕ) then
        if j.some = n.some then r else 0
      else coeff n.some 0) =
      r
  else
    (if Eq (α := ℕ) ((j : (a : Option S₁) → ℕ) none : ℕ) ((n : (a : Option S₁) → ℕ) none : ℕ) then
        if j.some = n.some then r else 0
      else coeff n.some 0) =
      0
monomial₁ :
  if j = n then
    (if Eq (α := ℕ) ((j : (a : Option S₁) → ℕ) none : ℕ) ((n : (a : Option S₁) → ℕ) none : ℕ) then
        if j.some = n.some then r else 0
      else 0) =
      r
  else
    (if Eq (α := ℕ) ((j : (a : Option S₁) → ℕ) none : ℕ) ((n : (a : Option S₁) → ℕ) none : ℕ) then
        if j.some = n.some then r else 0
      else 0) =
      0
⊢ Eq.{u + 1} (α := R)
    (coeff n.some
      (Polynomial.coeff
        ((Polynomial.monomial ((j : (a : Option S₁) → ℕ) none) : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X])
          ((MvPolynomial.monomial j.some : (a : R) → MvPolynomial S₁ R) r))
        ((n : (a : Option S₁) → ℕ) none)))
    (coeff n ((MvPolynomial.monomial j : (a : R) → MvPolynomial (Option S₁) R) r))
have pos : ∀ (hj : j = n),
  if j = n then
    (if Eq (α := ℕ) ((j : (a : Option S₁) → ℕ) none : ℕ) ((n : (a : Option S₁) → ℕ) none : ℕ) then
        if j.some = n.some then r else 0
      else 0) =
      r
  else
    (if Eq (α := ℕ) ((j : (a : Option S₁) → ℕ) none : ℕ) ((n : (a : Option S₁) → ℕ) none : ℕ) then
        if j.some = n.some then r else 0
      else 0) =
      0
Tactic: classical
    simp only [Polynomial.coeff_monomial, MvPolynomial.coeff_monomial, apply_ite]
    simp only [coeff_zero]
    by_cases hj : j = n
    · simp [hj]
    · rw [if_neg hj]
      simp only [ite_eq_right_iff]
      intro hj_none hj_some
      apply False.elim (hj _)
      simp only [Finsupp.ext_iff, Option.forall, hj_none, true_and]
      simpa only [Finsupp.ext_iff] using hj_some
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
j : Option S₁ →₀ ℕ
r : R
n : Option S₁ →₀ ℕ
monomial :
  if j = n then
    (if Eq (α := ℕ) ((j : (a : Option S₁) → ℕ) none : ℕ) ((n : (a : Option S₁) → ℕ) none : ℕ) then
        if j.some = n.some then r else 0
      else coeff n.some 0) =
      r
  else
    (if Eq (α := ℕ) ((j : (a : Option S₁) → ℕ) none : ℕ) ((n : (a : Option S₁) → ℕ) none : ℕ) then
        if j.some = n.some then r else 0
      else coeff n.some 0) =
      0
monomial₁ :
  if j = n then
    (if Eq (α := ℕ) ((j : (a : Option S₁) → ℕ) none : ℕ) ((n : (a : Option S₁) → ℕ) none : ℕ) then
        if j.some = n.some then r else 0
      else 0) =
      r
  else
    (if Eq (α := ℕ) ((j : (a : Option S₁) → ℕ) none : ℕ) ((n : (a : Option S₁) → ℕ) none : ℕ) then
        if j.some = n.some then r else 0
      else 0) =
      0
pos :
  ∀ (hj : j = n),
    if j = n then
      (if Eq (α := ℕ) ((j : (a : Option S₁) → ℕ) none : ℕ) ((n : (a : Option S₁) → ℕ) none : ℕ) then
          if j.some = n.some then r else 0
        else 0) =
        r
    else
      (if Eq (α := ℕ) ((j : (a : Option S₁) → ℕ) none : ℕ) ((n : (a : Option S₁) → ℕ) none : ℕ) then
          if j.some = n.some then r else 0
        else 0) =
        0
⊢ Eq.{u + 1} (α := R)
    (coeff n.some
      (Polynomial.coeff
        ((Polynomial.monomial ((j : (a : Option S₁) → ℕ) none) : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X])
          ((MvPolynomial.monomial j.some : (a : R) → MvPolynomial S₁ R) r))
        ((n : (a : Option S₁) → ℕ) none)))
    (coeff n ((MvPolynomial.monomial j : (a : R) → MvPolynomial (Option S₁) R) r))
have neg : ∀ (hj : ¬j = n),
  if j = n then
    (if Eq (α := ℕ) ((j : (a : Option S₁) → ℕ) none : ℕ) ((n : (a : Option S₁) → ℕ) none : ℕ) then
        if j.some = n.some then r else 0
      else 0) =
      r
  else
    (if Eq (α := ℕ) ((j : (a : Option S₁) → ℕ) none : ℕ) ((n : (a : Option S₁) → ℕ) none : ℕ) then
        if j.some = n.some then r else 0
      else 0) =
      0
Tactic: classical
    simp only [Polynomial.coeff_monomial, MvPolynomial.coeff_monomial, apply_ite]
    simp only [coeff_zero]
    by_cases hj : j = n
    · simp [hj]
    · rw [if_neg hj]
      simp only [ite_eq_right_iff]
      intro hj_none hj_some
      apply False.elim (hj _)
      simp only [Finsupp.ext_iff, Option.forall, hj_none, true_and]
      simpa only [Finsupp.ext_iff] using hj_some
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
n : Option S₁ →₀ ℕ
f : MvPolynomial.{v, u} (Option S₁) R
⊢ coeff n.some
      (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) f)
        ((n : (a : Option S₁) → ℕ) none)) =
    coeff n f
have monomial : ∀ (j : Option S₁ →₀ ℕ) (r : R) (n : Option S₁ →₀ ℕ),
  Eq.{u + 1} (α := R)
    (coeff n.some
      (Polynomial.coeff
        ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X])
          ((monomial j : (a : R) → MvPolynomial (Option S₁) R) r))
        ((n : (a : Option S₁) → ℕ) none)))
    (coeff n ((monomial j : (a : R) → MvPolynomial (Option S₁) R) r))
Tactic: induction f using MvPolynomial.induction_on' generalizing n with
  | monomial j r =>
    rw [optionEquivLeft_monomial]
    classical
    simp only [Polynomial.coeff_monomial, MvPolynomial.coeff_monomial, apply_ite]
    simp only [coeff_zero]
    by_cases hj : j = n
    · simp [hj]
    · rw [if_neg hj]
      simp only [ite_eq_right_iff]
      intro hj_none hj_some
      apply False.elim (hj _)
      simp only [Finsupp.ext_iff, Option.forall, hj_none, true_and]
      simpa only [Finsupp.ext_iff] using hj_some
  | add p q hp hq => simp only [map_add, Polynomial.coeff_add, coeff_add, hp, hq]
Cleared hypotheses: n, f
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
n : Option S₁ →₀ ℕ
f : MvPolynomial.{v, u} (Option S₁) R
monomial :
  ∀ (j : Option S₁ →₀ ℕ) (r : R) (n : Option S₁ →₀ ℕ),
    Eq.{u + 1} (α := R)
      (coeff n.some
        (Polynomial.coeff
          ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X])
            ((MvPolynomial.monomial j : (a : R) → MvPolynomial (Option S₁) R) r))
          ((n : (a : Option S₁) → ℕ) none)))
      (coeff n ((MvPolynomial.monomial j : (a : R) → MvPolynomial (Option S₁) R) r))
⊢ coeff n.some
      (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) f)
        ((n : (a : Option S₁) → ℕ) none)) =
    coeff n f
have add : ∀ (p q : MvPolynomial.{v, u} (Option S₁) R)
  (hp :
    ∀ (n : Option S₁ →₀ ℕ),
      coeff n.some
          (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p)
            ((n : (a : Option S₁) → ℕ) none)) =
        coeff n p)
  (hq :
    ∀ (n : Option S₁ →₀ ℕ),
      coeff n.some
          (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) q)
            ((n : (a : Option S₁) → ℕ) none)) =
        coeff n q)
  (n : Option S₁ →₀ ℕ),
  coeff n.some
      (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) (p + q))
        ((n : (a : Option S₁) → ℕ) none)) =
    coeff n (p + q)
Tactic: induction f using MvPolynomial.induction_on' generalizing n with
  | monomial j r =>
    rw [optionEquivLeft_monomial]
    classical
    simp only [Polynomial.coeff_monomial, MvPolynomial.coeff_monomial, apply_ite]
    simp only [coeff_zero]
    by_cases hj : j = n
    · simp [hj]
    · rw [if_neg hj]
      simp only [ite_eq_right_iff]
      intro hj_none hj_some
      apply False.elim (hj _)
      simp only [Finsupp.ext_iff, Option.forall, hj_none, true_and]
      simpa only [Finsupp.ext_iff] using hj_some
  | add p q hp hq => simp only [map_add, Polynomial.coeff_add, coeff_add, hp, hq]
Cleared hypotheses: n, f
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
s : S₁ → R
y : R
f : MvPolynomial.{v, u} (Option S₁) R
r : R
⊢ Eq (α := R[X])
    (OneHom.toFun
      (↑(↑(Polynomial.mapRingHom (eval s)) : (MvPolynomial S₁ R)[X] →* R[X]) : OneHom (MvPolynomial S₁ R)[X] R[X])
      ((algebraMap R (MvPolynomial S₁ R)[X] : (a : R) → (MvPolynomial S₁ R)[X]) r))
    ((algebraMap R R[X] : (a : R) → R[X]) r)
have h : r =
  (eval s : (a : MvPolynomial S₁ R) → R)
    ((algebraMap R (MvPolynomial S₁ R) : (a : R) → MvPolynomial S₁ R) r : MvPolynomial S₁ R)
Tactic: convert! Polynomial.map_C (eval s)
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
s : S₁ → R
y : R
f : MvPolynomial.{v, u} (Option S₁) R
φ : (MvPolynomial S₁ R)[X] →ₐ[R] R[X] :=
  let __src : (MvPolynomial S₁ R)[X] →+* R[X] := Polynomial.mapRingHom (eval s);
  { toRingHom := __src, commutes' := ⋯ }
⊢ (eval fun (x : Option S₁) ↦ x.elim y s : (a : MvPolynomial (Option S₁) R) → R) f =
    Polynomial.eval y
      (Polynomial.map (eval s) ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) f))
have aeval : Eq.{u + 1} (α := R) ((aeval fun (x : Option S₁) ↦ x.elim y s : (a : MvPolynomial (Option S₁) R) → R) f : R)
  ((AlgHom.comp (Polynomial.aeval y)
          (φ.comp (↑(optionEquivLeft R S₁) : MvPolynomial (Option S₁) R →ₐ[R] (MvPolynomial S₁ R)[X])) :
        (a : MvPolynomial (Option S₁) R) → R)
      f :
    R)
Tactic: change
    aeval (fun x ↦ Option.elim x y s) f =
      (Polynomial.aeval y).comp (φ.comp (optionEquivLeft _ _).toAlgHom) f
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
s : S₁ → R
y : R
f : MvPolynomial.{v, u} (Option S₁) R
φ : (MvPolynomial S₁ R)[X] →ₐ[R] R[X] :=
  let __src : (MvPolynomial S₁ R)[X] →+* R[X] := Polynomial.mapRingHom (eval s);
  { toRingHom := __src, commutes' := ⋯ }
⊢ Eq.{u + 1} (α := R) ((aeval fun (x : Option S₁) ↦ x.elim y s : (a : MvPolynomial (Option S₁) R) → R) f : R)
    ((AlgHom.comp (Polynomial.aeval y)
            (φ.comp (↑(optionEquivLeft R S₁) : MvPolynomial (Option S₁) R →ₐ[R] (MvPolynomial S₁ R)[X])) :
          (a : MvPolynomial (Option S₁) R) → R)
        f :
      R)
have e_a : Eq (α := MvPolynomial.{v, u} (Option S₁) R →ₐ[R] R) (aeval fun (x : Option S₁) ↦ x.elim y s)
  (AlgHom.comp (Polynomial.aeval y)
    (φ.comp (↑(optionEquivLeft R S₁) : MvPolynomial (Option S₁) R →ₐ[R] (MvPolynomial S₁ R)[X])))
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
s : S₁ → R
y : R
f : MvPolynomial.{v, u} (Option S₁) R
φ : (MvPolynomial S₁ R)[X] →ₐ[R] R[X] :=
  let __src : (MvPolynomial S₁ R)[X] →+* R[X] := Polynomial.mapRingHom (eval s);
  { toRingHom := __src, commutes' := ⋯ }
⊢ Eq (α := MvPolynomial.{v, u} (Option S₁) R →ₐ[R] R) (aeval fun (x : Option S₁) ↦ x.elim y s)
    (AlgHom.comp (Polynomial.aeval y)
      (φ.comp (↑(optionEquivLeft R S₁) : MvPolynomial (Option S₁) R →ₐ[R] (MvPolynomial S₁ R)[X])))
have e_a : ∀ (i : Option S₁),
  Eq.{u + 1} (α := R) ((aeval fun (x : Option S₁) ↦ x.elim y s : (a : MvPolynomial (Option S₁) R) → R) (X i) : R)
    ((AlgHom.comp (Polynomial.aeval y)
            (φ.comp (↑(optionEquivLeft R S₁) : MvPolynomial (Option S₁) R →ₐ[R] (MvPolynomial S₁ R)[X])) :
          (a : MvPolynomial (Option S₁) R) → R)
        (X i) :
      R)
Tactic: apply MvPolynomial.algHom_ext
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
s : S₁ → R
y : R
f : MvPolynomial.{v, u} (Option S₁) R
φ : (MvPolynomial S₁ R)[X] →ₐ[R] R[X] :=
  let __src : (MvPolynomial S₁ R)[X] →+* R[X] := Polynomial.mapRingHom (eval s);
  { toRingHom := __src, commutes' := ⋯ }
⊢ ∀ (i : Option S₁),
    Eq.{u + 1} (α := R) ((aeval fun (x : Option S₁) ↦ x.elim y s : (a : MvPolynomial (Option S₁) R) → R) (X i) : R)
      ((AlgHom.comp (Polynomial.aeval y)
              (φ.comp (↑(optionEquivLeft R S₁) : MvPolynomial (Option S₁) R →ₐ[R] (MvPolynomial S₁ R)[X])) :
            (a : MvPolynomial (Option S₁) R) → R)
          (X i) :
        R)
have e_a : Eq.{u + 1} (α := R) ((aeval fun (x : Option S₁) ↦ x.elim y s : (a : MvPolynomial (Option S₁) R) → R) (X none) : R)
    ((AlgHom.comp (Polynomial.aeval y)
            (φ.comp (↑(optionEquivLeft R S₁) : MvPolynomial (Option S₁) R →ₐ[R] (MvPolynomial S₁ R)[X])) :
          (a : MvPolynomial (Option S₁) R) → R)
        (X none) :
      R) ∧
  ∀ (x : S₁),
    Eq.{u + 1} (α := R)
      ((aeval fun (x : Option S₁) ↦ x.elim y s : (a : MvPolynomial (Option S₁) R) → R) (X (Option.some x)) : R)
      ((AlgHom.comp (Polynomial.aeval y)
              (φ.comp (↑(optionEquivLeft R S₁) : MvPolynomial (Option S₁) R →ₐ[R] (MvPolynomial S₁ R)[X])) :
            (a : MvPolynomial (Option S₁) R) → R)
          (X (Option.some x)) :
        R)
Tactic: rw [Option.forall]
-- 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
⊢ Polynomial.support (R := MvPolynomial σ R)
      ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p) =
    Finset.image (fun (m : Option σ →₀ ℕ) ↦ (m : (a : Option σ) → ℕ) none) p.support
have h : ∀ (i : ℕ),
  i ∈
      Polynomial.support (R := MvPolynomial σ R)
        ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p) ↔
    Membership.mem (γ := Finset ℕ) (Finset.image (fun (m : Option σ →₀ ℕ) ↦ (m : (a : Option σ) → ℕ) none) p.support) i
Tactic: ext i
-- 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
i : ℕ
⊢ i ∈
      Polynomial.support (R := MvPolynomial σ R)
        ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p) ↔
    Membership.mem (γ := Finset ℕ) (Finset.image (fun (m : Option σ →₀ ℕ) ↦ (m : (a : Option σ) → ℕ) none) p.support) i
have h : (∃ (a : σ →₀ ℕ),
    Ne.{u + 1} (α := R)
      ((Polynomial.coeff ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p) i :
            (a : σ →₀ ℕ) → R)
          a :
        R)
      ((0 : (a : σ →₀ ℕ) → R) a : R)) ↔
  ∃ a ∈ p.support, (a : (a : Option σ) → ℕ) none = i
Tactic: rw [Polynomial.mem_support_iff, Finset.mem_image, Finsupp.ne_iff]
-- 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
i : ℕ
⊢ (∃ (a : σ →₀ ℕ),
      Ne.{u + 1} (α := R)
        ((Polynomial.coeff ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p) i :
              (a : σ →₀ ℕ) → R)
            a :
          R)
        ((0 : (a : σ →₀ ℕ) → R) a : R)) ↔
    ∃ a ∈ p.support, (a : (a : Option σ) → ℕ) none = i
have h : (∃ (a : σ →₀ ℕ),
    Ne.{u + 1} (α := R)
      ((Polynomial.coeff ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p) i :
            (a : σ →₀ ℕ) → R)
          a :
        R)
      ((0 : (a : σ →₀ ℕ) → R) a : R)) →
  ∃ a ∈ p.support, (a : (a : Option σ) → ℕ) none = i
Tactic: constructor
-- 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
i : ℕ
h :
  (∃ (a : σ →₀ ℕ),
      Ne.{u + 1} (α := R)
        ((Polynomial.coeff ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p) i :
              (a : σ →₀ ℕ) → R)
            a :
          R)
        ((0 : (a : σ →₀ ℕ) → R) a : R)) →
    ∃ a ∈ p.support, (a : (a : Option σ) → ℕ) none = i
⊢ (∃ (a : σ →₀ ℕ),
      Ne.{u + 1} (α := R)
        ((Polynomial.coeff ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p) i :
              (a : σ →₀ ℕ) → R)
            a :
          R)
        ((0 : (a : σ →₀ ℕ) → R) a : R)) ↔
    ∃ a ∈ p.support, (a : (a : Option σ) → ℕ) none = i
have h₁ : (∃ a ∈ p.support, (a : (a : Option σ) → ℕ) none = i) →
  ∃ (a : σ →₀ ℕ),
    Ne.{u + 1} (α := R)
      ((Polynomial.coeff ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p) i :
            (a : σ →₀ ℕ) → R)
          a :
        R)
      ((0 : (a : σ →₀ ℕ) → R) a : R)
Tactic: constructor
-- 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
i : ℕ
m : σ →₀ ℕ
hm :
  Ne.{u + 1} (α := R)
    ((Polynomial.coeff ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p) i :
          (a : σ →₀ ℕ) → R)
        m :
      R)
    ((0 : (a : σ →₀ ℕ) → R) m : R)
⊢ ∃ a ∈ p.support, (a : (a : Option σ) → ℕ) none = i
have h : optionElim i m ∈ p.support
Tactic: refine ⟨optionElim i m, ?_, optionElim_apply_none _ _⟩
-- 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
i : ℕ
m : σ →₀ ℕ
hm :
  Ne.{u + 1} (α := R)
    ((Polynomial.coeff ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p) i :
          (a : σ →₀ ℕ) → R)
        m :
      R)
    ((0 : (a : σ →₀ ℕ) → R) m : R)
⊢ optionElim i m ∈ p.support
have h : Membership.mem (γ := Finset (σ →₀ ℕ))
  (support.{u, u_1} (R := R)
    (Polynomial.coeff ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p) i))
  m
Tactic: rw [← mem_support_coeff_optionEquivLeft]
-- 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
m : Option σ →₀ ℕ
h : m ∈ p.support
⊢ ∃ (a : σ →₀ ℕ),
    Ne.{u + 1} (α := R)
      ((Polynomial.coeff ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p)
              ((m : (a : Option σ) → ℕ) none) :
            (a : σ →₀ ℕ) → R)
          a :
        R)
      ((0 : (a : σ →₀ ℕ) → R) a : R)
have h₁ : Ne.{u + 1} (α := R)
  ((Polynomial.coeff ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p)
          ((m : (a : Option σ) → ℕ) none) :
        (a : σ →₀ ℕ) → R)
      m.some :
    R)
  ((0 : (a : σ →₀ ℕ) → R) m.some : R)
Tactic: refine ⟨some m, ?_⟩
-- 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
m : Option σ →₀ ℕ
h : m ∈ p.support
⊢ Ne.{u + 1} (α := R)
    ((Polynomial.coeff ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p)
            ((m : (a : Option σ) → ℕ) none) :
          (a : σ →₀ ℕ) → R)
        m.some :
      R)
    ((0 : (a : σ →₀ ℕ) → R) m.some : R)
have h₁ : Ne.{u + 1} (α := R)
  (coeff m.some
      (Polynomial.coeff ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p)
        ((m : (a : Option σ) → ℕ) none)) :
    R)
  ((0 : (a : σ →₀ ℕ) → R) m.some : R)
Tactic: rwa [← coeff, zero_apply, ← mem_support_iff, mem_support_coeff_optionEquivLeft, optionElim_some]
-- 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
m : Option σ →₀ ℕ
h : m ∈ p.support
h₁ :
  Ne.{u + 1} (α := R)
    (coeff m.some
        (Polynomial.coeff ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p)
          ((m : (a : Option σ) → ℕ) none)) :
      R)
    ((0 : (a : σ →₀ ℕ) → R) m.some : R)
⊢ Ne.{u + 1} (α := R)
    ((Polynomial.coeff ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p)
            ((m : (a : Option σ) → ℕ) none) :
          (a : σ →₀ ℕ) → R)
        m.some :
      R)
    ((0 : (a : σ →₀ ℕ) → R) m.some : R)
have h₂ : Ne.{u + 1} (α := R)
  (coeff m.some
    (Polynomial.coeff ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p)
      ((m : (a : Option σ) → ℕ) none)))
  0
Tactic: rwa [← coeff, zero_apply, ← mem_support_iff, mem_support_coeff_optionEquivLeft, optionElim_some]
-- 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
m : Option σ →₀ ℕ
h : m ∈ p.support
h₁ :
  Ne.{u + 1} (α := R)
    (coeff m.some
        (Polynomial.coeff ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p)
          ((m : (a : Option σ) → ℕ) none)) :
      R)
    ((0 : (a : σ →₀ ℕ) → R) m.some : R)
h₂ :
  Ne.{u + 1} (α := R)
    (coeff m.some
      (Polynomial.coeff ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p)
        ((m : (a : Option σ) → ℕ) none)))
    0
⊢ Ne.{u + 1} (α := R)
    ((Polynomial.coeff ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p)
            ((m : (a : Option σ) → ℕ) none) :
          (a : σ →₀ ℕ) → R)
        m.some :
      R)
    ((0 : (a : σ →₀ ℕ) → R) m.some : R)
have h₃ : Membership.mem (γ := Finset (σ →₀ ℕ))
  (support.{u, u_1} (R := R)
    (Polynomial.coeff ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p)
      ((m : (a : Option σ) → ℕ) none)))
  m.some
Tactic: rwa [← coeff, zero_apply, ← mem_support_iff, mem_support_coeff_optionEquivLeft, optionElim_some]
-- 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
m : Option σ →₀ ℕ
h : m ∈ p.support
h₁ :
  Ne.{u + 1} (α := R)
    (coeff m.some
        (Polynomial.coeff ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p)
          ((m : (a : Option σ) → ℕ) none)) :
      R)
    ((0 : (a : σ →₀ ℕ) → R) m.some : R)
h₂ :
  Ne.{u + 1} (α := R)
    (coeff m.some
      (Polynomial.coeff ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p)
        ((m : (a : Option σ) → ℕ) none)))
    0
h₃ :
  Membership.mem (γ := Finset (σ →₀ ℕ))
    (support.{u, u_1} (R := R)
      (Polynomial.coeff ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p)
        ((m : (a : Option σ) → ℕ) none)))
    m.some
⊢ Ne.{u + 1} (α := R)
    ((Polynomial.coeff ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p)
            ((m : (a : Option σ) → ℕ) none) :
          (a : σ →₀ ℕ) → R)
        m.some :
      R)
    ((0 : (a : σ →₀ ℕ) → R) m.some : R)
have h₄ : Membership.mem (α := Option σ →₀ ℕ) p.support (optionElim ((m : (a : Option σ) → ℕ) none) m.some : Option σ →₀ ℕ)
Tactic: rwa [← coeff, zero_apply, ← mem_support_iff, mem_support_coeff_optionEquivLeft, optionElim_some]
-- 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
⊢ (Polynomial.support (R := MvPolynomial σ R)
      ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f)).Nonempty
have rwa : Ne (α := (MvPolynomial σ R)[X])
  ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f : (MvPolynomial σ R)[X])
  (0 : (MvPolynomial σ R)[X])
Tactic: rwa [Polynomial.support_nonempty, EmbeddingLike.map_ne_zero_iff]
-- 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
⊢ ((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 (α := ℕ)
  ((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)
Tactic: rw [degreeOf_eq_sup, support_optionEquivLeft, Finset.sup_image, Function.comp_def]