awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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
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
⊢ 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
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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

Tactic:
simp [hj]
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
j : Option S₁ →₀ ℕ
r : R
n : Option S₁ →₀ ℕ
hj : ¬j = n
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
⊢ 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:
rw [if_neg hj]

Premises used: if_neg
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
j : Option S₁ →₀ ℕ
r : R
n : Option S₁ →₀ ℕ
hj : ¬j = n
neg : Eq (α := ℕ) ((j : (a : Option S₁) → ℕ) none : ℕ) ((n : (a : Option S₁) → ℕ) none : ℕ) → j.some = n.some → r = 0
⊢ (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 [ite_eq_right_iff]

Premises used: ite_eq_right_iff
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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
apply : j = n
⊢ r = 0

Tactic:
apply False.elim (hj _)

Premises used: False.elim
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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
simp :
  ∀ (x : S₁),
    Eq (α := ℕ) ((j : (a : Option S₁) → ℕ) (Option.some x) : ℕ) ((n : (a : Option S₁) → ℕ) (Option.some x) : ℕ)
⊢ j = n

Tactic:
simp only [Finsupp.ext_iff, Option.forall, hj_none, true_and]

Premises used: Option.forall, Finsupp.ext_iff, true_and
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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
⊢ ∀ (x : S₁),
    Eq (α := ℕ) ((j : (a : Option S₁) → ℕ) (Option.some x) : ℕ) ((n : (a : Option S₁) → ℕ) (Option.some x) : ℕ)

Tactic:
simpa only [Finsupp.ext_iff] using hj_some

Premises used: Finsupp.ext_iff
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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
neg 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
⊢ 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))

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

Premises used: apply_ite, Option.forall, Polynomial.coeff_monomial, ite_eq_right_iff, MvPolynomial.coeff_zero, MvPolynomial.coeff_monomial, Finsupp.ext_iff, true_and
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
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:
simp only [map_add, Polynomial.coeff_add, coeff_add, hp, hq]

Premises used: map_add, Polynomial.coeff_add, MvPolynomial.coeff_add
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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))
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)
⊢ 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

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]

Premises used: MvPolynomial.monomial, apply_ite, map_add, Option.forall, Polynomial.coeff_monomial, Polynomial.coeff_add, ite_eq_right_iff, MvPolynomial.coeff_zero, MvPolynomial.coeff_add, MvPolynomial.optionEquivLeft_monomial, MvPolynomial.coeff_monomial, Finsupp.ext_iff, true_and
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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])
    (Polynomial.map (eval s)
      ((Polynomial.C : (a : MvPolynomial S₁ R) → (MvPolynomial S₁ R)[X])
        ((algebraMap R (MvPolynomial S₁ R) : (a : R) → MvPolynomial S₁ R) r)))
    ((Polynomial.C : (a : R) → R[X])
      ((eval s : (a : MvPolynomial S₁ R) → R)
        ((algebraMap R (MvPolynomial S₁ R) : (a : R) → MvPolynomial S₁ R) r : MvPolynomial S₁ R)))

Tactic:
Polynomial.map_C (eval s)

Premises used: MvPolynomial.eval, Polynomial.map_C
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
s : S₁ → R
y : R
f : MvPolynomial.{v, u} (Option S₁) R
r : R
h :
  r =
    (eval s : (a : MvPolynomial S₁ R) → R)
      ((algebraMap R (MvPolynomial S₁ R) : (a : R) → MvPolynomial S₁ R) r : MvPolynomial S₁ 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)

Tactic:
convert! Polynomial.map_C (eval s)

Premises used: MvPolynomial.eval, Polynomial.map_C
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
s : S₁ → R
y : R
f : MvPolynomial.{v, u} (Option S₁) R
r : R
⊢ r =
    (eval s : (a : MvPolynomial S₁ R) → R)
      ((algebraMap R (MvPolynomial S₁ R) : (a : R) → MvPolynomial S₁ R) r : MvPolynomial S₁ R)

Tactic:
(eval_C _).symm

Premises used: MvPolynomial.eval_C, Eq.symm
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
s : S₁ → R
y : R
f : MvPolynomial.{v, u} (Option S₁) R
r : R
⊢ r =
    (eval s : (a : MvPolynomial S₁ R) → R)
      ((algebraMap R (MvPolynomial S₁ R) : (a : R) → MvPolynomial S₁ R) r : MvPolynomial S₁ R)

Tactic:
exact (eval_C _).symm

Premises used: MvPolynomial.eval_C, Eq.symm
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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' := ⋯ }
aeval :
  Eq.{u + 1} (α := R)
    ((MvPolynomial.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)
⊢ (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))

Tactic:
change
    aeval (fun x ↦ Option.elim x y s) f =
      (Polynomial.aeval y).comp (φ.comp (optionEquivLeft _ _).toAlgHom) f

Premises used: MvPolynomial.aeval, AlgEquiv.toAlgHom, MvPolynomial.optionEquivLeft, Polynomial.aeval, AlgHom.comp, Option.elim, DFunLike.coe
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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' := ⋯ }
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])))
⊢ 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:
congr 2
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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' := ⋯ }
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)
⊢ 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:
apply MvPolynomial.algHom_ext

Premises used: MvPolynomial.algHom_ext
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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' := ⋯ }
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)
⊢ ∀ (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:
rw [Option.forall]

Premises used: Option.forall
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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) (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:
simp only [aeval_X, Option.elim_none, AlgHom.coe_comp, Polynomial.coe_aeval_eq_eval,
    AlgHom.coe_mk, Polynomial.coe_mapRingHom, AlgEquiv.coe_algHom, comp_apply,
    optionEquivLeft_apply, Polynomial.map_X, Polynomial.eval_X, Option.elim_some,
    Polynomial.map_C, eval_X, Polynomial.eval_C, implies_true, and_self, φ]

Premises used: AlgHom.coe_mk, MvPolynomial.aeval_X, MvPolynomial.optionEquivLeft_apply, Polynomial.eval_C, and_self, Polynomial.eval_X, Option.elim_none, Polynomial.map_X, Option.elim_some, AlgHom.coe_comp, Polynomial.coe_mapRingHom, AlgEquiv.coe_algHom, Function.comp_apply, implies_true, Polynomial.coe_aeval_eq_eval, Polynomial.map_C, MvPolynomial.eval_X
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
f : MvPolynomial.{u_1, u} (Option σ) R
i : ℕ
m : σ →₀ ℕ
⊢ Membership.mem (γ := Finset (σ →₀ ℕ))
      (support.{u, u_1} (R := R)
        (Polynomial.coeff ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) f) i))
      m ↔
    optionElim i m ∈ f.support

Tactic:
simp [← optionEquivLeft_coeff_some_coeff_none]

Premises used: MvPolynomial.optionEquivLeft_coeff_some_coeff_none
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial.{u_1, u} (Option σ) R
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
⊢ 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

Tactic:
ext i
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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
⊢ 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:
rw [Polynomial.mem_support_iff, Finset.mem_image, Finsupp.ne_iff]

Premises used: Finset.mem_image, Polynomial.mem_support_iff, Finsupp.ne_iff
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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
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)
⊢ (∃ (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
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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

Tactic:
⟨optionElim i m, ?_, optionElim_apply_none _ _⟩

Premises used: Finsupp.optionElim, And.intro, Exists.intro, Finsupp.optionElim_apply_none
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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)
h : optionElim i m ∈ p.support
⊢ ∃ a ∈ p.support, (a : (a : Option σ) → ℕ) none = i

Tactic:
refine ⟨optionElim i m, ?_, optionElim_apply_none _ _⟩
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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)
h :
  Membership.mem (γ := Finset (σ →₀ ℕ))
    (support.{u, u_1} (R := R)
      (Polynomial.coeff ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p) i))
    m
⊢ optionElim i m ∈ p.support

Tactic:
rw [← mem_support_coeff_optionEquivLeft]

Premises used: MvPolynomial.mem_support_coeff_optionEquivLeft
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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)
⊢ Membership.mem (γ := Finset (σ →₀ ℕ))
    (support.{u, u_1} (R := R)
      (Polynomial.coeff ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p) i))
    m

Tactic:
simpa using hm