awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst : CommSemiring R
i : Option S₁
m : Option S₁ →₀ ℕ
hf :
  Eq.{u + 1} (α := R)
    (coeff m
      ((AlgHom.comp (Polynomial.aevalTower (rename Option.some) (X none))
            (aeval fun (o : Option S₁) ↦
              o.elim Polynomial.X fun (s : S₁) ↦
                (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s)) :
          (a : MvPolynomial (Option S₁) R) → MvPolynomial (Option S₁) R)
        (X none)))
    (coeff m
      ((AlgHom.id R (MvPolynomial.{v, u} (Option S₁) R) : (a : MvPolynomial (Option S₁) R) → MvPolynomial (Option S₁) R)
        (X none)))
⊢ Eq.{u + 1} (α := R)
    (coeff m
      ((AlgHom.comp (Polynomial.aevalTower (rename Option.some) (X none))
            (aeval fun (o : Option S₁) ↦
              o.elim Polynomial.X fun (s : S₁) ↦
                (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s)) :
          (a : MvPolynomial (Option S₁) R) → MvPolynomial (Option S₁) R)
        (X i)))
    (coeff m
      ((AlgHom.id R (MvPolynomial.{v, u} (Option S₁) R) : (a : MvPolynomial (Option S₁) R) → MvPolynomial (Option S₁) R)
        (X i)))
have hf₁ : ∀ (val : S₁),
  Eq.{u + 1} (α := R)
    (coeff m
      ((AlgHom.comp (Polynomial.aevalTower (rename Option.some) (X none))
            (aeval fun (o : Option S₁) ↦
              o.elim Polynomial.X fun (s : S₁) ↦
                (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s)) :
          (a : MvPolynomial (Option S₁) R) → MvPolynomial (Option S₁) R)
        (X (Option.some val))))
    (coeff m
      ((AlgHom.id R (MvPolynomial.{v, u} (Option S₁) R) : (a : MvPolynomial (Option S₁) R) → MvPolynomial (Option S₁) R)
        (X (Option.some val))))
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
m : Option S₁ →₀ ℕ
r : R
⊢ Eq (α := (MvPolynomial S₁ R)[X])
    ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X])
        ((monomial m : (a : R) → MvPolynomial (Option S₁) R) r) :
      (MvPolynomial S₁ R)[X])
    ((Polynomial.monomial ((m : (a : Option S₁) → ℕ) none) : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X])
        ((monomial m.some : (a : R) → MvPolynomial S₁ R) r) :
      (MvPolynomial S₁ R)[X])
have rw : HMul.hMul (α := (MvPolynomial S₁ R)[X])
    ((algebraMap R (MvPolynomial S₁ R)[X] : (a : R) → (MvPolynomial S₁ R)[X]) r : (MvPolynomial S₁ R)[X])
    (HPow.hPow (α := (MvPolynomial S₁ R)[X]) (β := ℕ)
        (Option.elim none Polynomial.X fun (s : S₁) ↦
          (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s))
        ((m : (a : Option S₁) → ℕ) none : ℕ) *
      m.some.prod fun (a : S₁) (k : ℕ) ↦
        HPow.hPow (α := (MvPolynomial S₁ R)[X])
          ((Option.some a).elim Polynomial.X fun (s : S₁) ↦
            (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s))
          k) =
  (Polynomial.monomial ((m : (a : Option S₁) → ℕ) none) : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X])
    ((monomial m.some : (a : R) → MvPolynomial S₁ R) r)
Tactic: rw [optionEquivLeft_apply, aeval_monomial, prod_option_index]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
m : Option S₁ →₀ ℕ
r : R
rw :
  HMul.hMul (α := (MvPolynomial S₁ R)[X])
      ((algebraMap R (MvPolynomial S₁ R)[X] : (a : R) → (MvPolynomial S₁ R)[X]) r : (MvPolynomial S₁ R)[X])
      (HPow.hPow (α := (MvPolynomial S₁ R)[X]) (β := ℕ)
          (Option.elim none Polynomial.X fun (s : S₁) ↦
            (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s))
          ((m : (a : Option S₁) → ℕ) none : ℕ) *
        m.some.prod fun (a : S₁) (k : ℕ) ↦
          HPow.hPow (α := (MvPolynomial S₁ R)[X])
            ((Option.some a).elim Polynomial.X fun (s : S₁) ↦
              (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s))
            k) =
    (Polynomial.monomial ((m : (a : Option S₁) → ℕ) none) : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X])
      ((monomial m.some : (a : R) → MvPolynomial S₁ R) r)
⊢ Eq (α := (MvPolynomial S₁ R)[X])
    ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X])
        ((monomial m : (a : R) → MvPolynomial (Option S₁) R) r) :
      (MvPolynomial S₁ R)[X])
    ((Polynomial.monomial ((m : (a : Option S₁) → ℕ) none) : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X])
        ((monomial m.some : (a : R) → MvPolynomial S₁ R) r) :
      (MvPolynomial S₁ R)[X])
have h_zero : ∀ (o : Option S₁),
  HPow.hPow (α := (MvPolynomial S₁ R)[X]) (β := ℕ)
      (o.elim Polynomial.X fun (s : S₁) ↦ (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s)) 0 =
    1
Tactic: rw [optionEquivLeft_apply, aeval_monomial, prod_option_index]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
m : Option S₁ →₀ ℕ
r : R
rw :
  HMul.hMul (α := (MvPolynomial S₁ R)[X])
      ((algebraMap R (MvPolynomial S₁ R)[X] : (a : R) → (MvPolynomial S₁ R)[X]) r : (MvPolynomial S₁ R)[X])
      (HPow.hPow (α := (MvPolynomial S₁ R)[X]) (β := ℕ)
          (Option.elim none Polynomial.X fun (s : S₁) ↦
            (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s))
          ((m : (a : Option S₁) → ℕ) none : ℕ) *
        m.some.prod fun (a : S₁) (k : ℕ) ↦
          HPow.hPow (α := (MvPolynomial S₁ R)[X])
            ((Option.some a).elim Polynomial.X fun (s : S₁) ↦
              (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s))
            k) =
    (Polynomial.monomial ((m : (a : Option S₁) → ℕ) none) : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X])
      ((monomial m.some : (a : R) → MvPolynomial S₁ R) r)
h_zero :
  ∀ (o : Option S₁),
    HPow.hPow (α := (MvPolynomial S₁ R)[X]) (β := ℕ)
        (o.elim Polynomial.X fun (s : S₁) ↦ (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s)) 0 =
      1
⊢ Eq (α := (MvPolynomial S₁ R)[X])
    ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X])
        ((monomial m : (a : R) → MvPolynomial (Option S₁) R) r) :
      (MvPolynomial S₁ R)[X])
    ((Polynomial.monomial ((m : (a : Option S₁) → ℕ) none) : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X])
        ((monomial m.some : (a : R) → MvPolynomial S₁ R) r) :
      (MvPolynomial S₁ R)[X])
have h_add : ∀ (o : Option S₁) (m₁ m₂ : ℕ),
  HPow.hPow (α := (MvPolynomial S₁ R)[X])
      (o.elim Polynomial.X fun (s : S₁) ↦ (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s))
      (m₁ + m₂) =
    HPow.hPow (α := (MvPolynomial S₁ R)[X])
        (o.elim Polynomial.X fun (s : S₁) ↦ (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s))
        m₁ *
      HPow.hPow (α := (MvPolynomial S₁ R)[X])
        (o.elim Polynomial.X fun (s : S₁) ↦ (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s)) m₂
Tactic: rw [optionEquivLeft_apply, aeval_monomial, prod_option_index]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
m : Option S₁ →₀ ℕ
r : R
⊢ HMul.hMul (α := (MvPolynomial S₁ R)[X])
      ((algebraMap R (MvPolynomial S₁ R)[X] : (a : R) → (MvPolynomial S₁ R)[X]) r : (MvPolynomial S₁ R)[X])
      (HPow.hPow (α := (MvPolynomial S₁ R)[X]) (β := ℕ)
          (Option.elim none Polynomial.X fun (s : S₁) ↦
            (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s))
          ((m : (a : Option S₁) → ℕ) none : ℕ) *
        m.some.prod fun (a : S₁) (k : ℕ) ↦
          HPow.hPow (α := (MvPolynomial S₁ R)[X])
            ((Option.some a).elim Polynomial.X fun (s : S₁) ↦
              (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s))
            k) =
    (Polynomial.monomial ((m : (a : Option S₁) → ℕ) none) : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X])
      ((monomial m.some : (a : R) → MvPolynomial S₁ R) r)
have rw : HMul.hMul (α := (MvPolynomial S₁ R)[X])
    ((algebraMap R (MvPolynomial S₁ R)[X] : (a : R) → (MvPolynomial S₁ R)[X]) r : (MvPolynomial S₁ R)[X])
    (HPow.hPow (α := (MvPolynomial S₁ R)[X]) (β := ℕ)
        (Option.elim none Polynomial.X fun (s : S₁) ↦
          (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s))
        ((m : (a : Option S₁) → ℕ) none : ℕ) *
      m.some.prod fun (a : S₁) (k : ℕ) ↦
        HPow.hPow (α := (MvPolynomial S₁ R)[X])
          ((Option.some a).elim Polynomial.X fun (s : S₁) ↦
            (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s))
          k) =
  HMul.hMul (α := (MvPolynomial S₁ R)[X])
    ((Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X])
        (HMul.hMul (α := MvPolynomial S₁ R) (β := MvPolynomial S₁ R)
          ((C : (a : R) → MvPolynomial S₁ R) r : MvPolynomial S₁ R)
          (m.some.prod fun (n : S₁) (e : ℕ) ↦ HPow.hPow (α := MvPolynomial S₁ R) (X n) e : MvPolynomial S₁ R)) :
      (MvPolynomial S₁ R)[X])
    (HPow.hPow (α := (MvPolynomial S₁ R)[X]) (β := ℕ) Polynomial.X ((m : (a : Option S₁) → ℕ) none : ℕ))
Tactic: rw [MvPolynomial.monomial_eq, ← Polynomial.C_mul_X_pow_eq_monomial]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
m : Option S₁ →₀ ℕ
r : R
⊢ HMul.hMul (α := (MvPolynomial S₁ R)[X])
      ((algebraMap R (MvPolynomial S₁ R)[X] : (a : R) → (MvPolynomial S₁ R)[X]) r : (MvPolynomial S₁ R)[X])
      (HPow.hPow (α := (MvPolynomial S₁ R)[X]) (β := ℕ)
          (Option.elim none Polynomial.X fun (s : S₁) ↦
            (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s))
          ((m : (a : Option S₁) → ℕ) none : ℕ) *
        m.some.prod fun (a : S₁) (k : ℕ) ↦
          HPow.hPow (α := (MvPolynomial S₁ R)[X])
            ((Option.some a).elim Polynomial.X fun (s : S₁) ↦
              (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s))
            k) =
    HMul.hMul (α := (MvPolynomial S₁ R)[X])
      ((Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X])
          (HMul.hMul (α := MvPolynomial S₁ R) (β := MvPolynomial S₁ R)
            ((C : (a : R) → MvPolynomial S₁ R) r : MvPolynomial S₁ R)
            (m.some.prod fun (n : S₁) (e : ℕ) ↦ HPow.hPow (α := MvPolynomial S₁ R) (X n) e : MvPolynomial S₁ R)) :
        (MvPolynomial S₁ R)[X])
      (HPow.hPow (α := (MvPolynomial S₁ R)[X]) (β := ℕ) Polynomial.X ((m : (a : Option S₁) → ℕ) none : ℕ))
have simp : HMul.hMul (α := (MvPolynomial S₁ R)[X])
    ((Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) ((C : (a : R) → MvPolynomial S₁ R) r) :
      (MvPolynomial S₁ R)[X])
    (HPow.hPow (α := (MvPolynomial S₁ R)[X]) (β := ℕ) Polynomial.X ((m : (a : Option S₁) → ℕ) none : ℕ) *
      m.some.prod fun (a : S₁) (k : ℕ) ↦
        HPow.hPow (α := (MvPolynomial S₁ R)[X])
          ((Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X a) : (MvPolynomial S₁ R)[X]) k) =
  HMul.hMul (α := (MvPolynomial S₁ R)[X])
    ((Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) ((C : (a : R) → MvPolynomial S₁ R) r) :
      (MvPolynomial S₁ R)[X])
    ((Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X])
        (m.some.prod fun (n : S₁) (e : ℕ) ↦ HPow.hPow (α := MvPolynomial S₁ R) (X n) e) *
      HPow.hPow (α := (MvPolynomial S₁ R)[X]) (β := ℕ) Polynomial.X ((m : (a : Option S₁) → ℕ) none : ℕ))
Tactic: simp only [Polynomial.algebraMap_apply, algebraMap_eq, Option.elim_none, Option.elim_some,
      map_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
m : Option S₁ →₀ ℕ
r : R
o : Option S₁
m₁ m₂ : ℕ
⊢ HPow.hPow (α := (MvPolynomial S₁ R)[X])
      (o.elim Polynomial.X fun (s : S₁) ↦ (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s))
      (m₁ + m₂) =
    HPow.hPow (α := (MvPolynomial S₁ R)[X])
        (o.elim Polynomial.X fun (s : S₁) ↦ (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s))
        m₁ *
      HPow.hPow (α := (MvPolynomial S₁ R)[X])
        (o.elim Polynomial.X fun (s : S₁) ↦ (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s)) m₂
have h_add : HPow.hPow (α := (MvPolynomial S₁ R)[X])
      (o.elim Polynomial.X fun (s : S₁) ↦ (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s)) m₁ *
    HPow.hPow (α := (MvPolynomial S₁ R)[X])
      (o.elim Polynomial.X fun (s : S₁) ↦ (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s)) m₂ =
  HPow.hPow (α := (MvPolynomial S₁ R)[X])
      (o.elim Polynomial.X fun (s : S₁) ↦ (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s)) m₁ *
    HPow.hPow (α := (MvPolynomial S₁ R)[X])
      (o.elim Polynomial.X fun (s : S₁) ↦ (Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X]) (X s)) m₂
Tactic: rw [pow_add]
-- 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₁ →₀ ℕ
⊢ 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))
have monomial : Eq.{u + 1} (α := R)
  (coeff n.some
    (Polynomial.coeff
      ((Polynomial.monomial ((j : (a : Option S₁) → ℕ) none) : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X])
        ((monomial j.some : (a : R) → MvPolynomial S₁ R) r))
      ((n : (a : Option S₁) → ℕ) none)))
  (coeff n ((monomial j : (a : R) → MvPolynomial (Option S₁) R) r))
Tactic: rw [optionEquivLeft_monomial]
-- 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₁ →₀ ℕ
⊢ Eq.{u + 1} (α := R)
    (coeff n.some
      (Polynomial.coeff
        ((Polynomial.monomial ((j : (a : Option S₁) → ℕ) none) : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X])
          ((monomial j.some : (a : R) → MvPolynomial S₁ R) r))
        ((n : (a : Option S₁) → ℕ) none)))
    (coeff n ((monomial j : (a : R) → MvPolynomial (Option S₁) R) r))
have 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
Tactic: simp only [Polynomial.coeff_monomial, MvPolynomial.coeff_monomial, apply_ite]
-- 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₁ →₀ ℕ
⊢ 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
have 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
Tactic: simp only [coeff_zero]
-- 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₁ →₀ ℕ
⊢ 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
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: by_cases hj : j = n
-- 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₁ →₀ ℕ
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
⊢ 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
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: by_cases hj : j = n
-- 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₁ →₀ ℕ
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
have neg : (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: rw [if_neg hj]
-- 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₁ →₀ ℕ
hj : ¬j = n
⊢ (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
have neg : Eq (α := ℕ) ((j : (a : Option S₁) → ℕ) none : ℕ) ((n : (a : Option S₁) → ℕ) none : ℕ) → j.some = n.some → r = 0
Tactic: simp only [ite_eq_right_iff]
-- 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₁ →₀ ℕ
hj : ¬j = n
hj_none : Eq (α := ℕ) ((j : (a : Option S₁) → ℕ) none : ℕ) ((n : (a : Option S₁) → ℕ) none : ℕ)
hj_some : j.some = n.some
⊢ r = 0
have apply : j = n
Tactic: apply False.elim (hj _)
-- 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₁ →₀ ℕ
hj : ¬j = n
hj_none : Eq (α := ℕ) ((j : (a : Option S₁) → ℕ) none : ℕ) ((n : (a : Option S₁) → ℕ) none : ℕ)
hj_some : j.some = n.some
⊢ j = n
have simp : ∀ (x : S₁), Eq (α := ℕ) ((j : (a : Option S₁) → ℕ) (Option.some x) : ℕ) ((n : (a : Option S₁) → ℕ) (Option.some x) : ℕ)
Tactic: simp only [Finsupp.ext_iff, Option.forall, hj_none, true_and]
-- 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₁ →₀ ℕ
⊢ Eq.{u + 1} (α := R)
    (coeff n.some
      (Polynomial.coeff
        ((Polynomial.monomial ((j : (a : Option S₁) → ℕ) none) : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X])
          ((monomial j.some : (a : R) → MvPolynomial S₁ R) r))
        ((n : (a : Option S₁) → ℕ) none)))
    (coeff n ((monomial j : (a : R) → MvPolynomial (Option S₁) R) r))
have 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
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
⊢ 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 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
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