awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
inst_2 : DecidableEq S₁
a : σ →₀ ℕ
s : R
p : MvPolynomial σ R
ha : a ∉ p.support
hs : s ≠ 0
hp :
  Subset.{v} (α := Finset S₁) (coeffs.{v, u_1} (σ := σ) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p))
    (Finset.image (⇑f : (a : R) → S₁) p.coeffs)
ih :
  Subset.{v} (α := Finset S₁)
    (coeffs.{v, u_1} (σ := σ)
      ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) ((monomial a : (a : R) → MvPolynomial σ R) s)))
    (Finset.image.{u, v} (α := R) (⇑f : (a : R) → S₁)
      (coeffs.{u, u_1} (σ := σ) ((monomial a : (a : R) → MvPolynomial σ R) s)))
⊢ Subset.{v} (α := Finset S₁)
    (coeffs.{v, u_1} (σ := σ)
      ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁)
        (HAdd.hAdd (α := MvPolynomial σ R) ((monomial a : (a : R) → MvPolynomial σ R) s : MvPolynomial σ R) p)))
    (Finset.image (⇑f : (a : R) → S₁)
      (HAdd.hAdd (α := MvPolynomial σ R) ((monomial a : (a : R) → MvPolynomial σ R) s : MvPolynomial σ R) p).coeffs)
have monomial_add : Subset.{v} (α := Finset S₁)
  (coeffs.{v, u_1} (σ := σ)
      ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) ((monomial a : (a : R) → MvPolynomial σ R) s)) ∪
    coeffs.{v, u_1} (σ := σ) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p))
  (Finset.image (⇑f : (a : R) → S₁) (coeffs.{u, u_1} (σ := σ) ((monomial a : (a : R) → MvPolynomial σ R) s) ∪ p.coeffs))
Tactic: rw [coeffs_add (disjoint_support_monomial ha hs), map_add, coeffs_add]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
inst_2 : DecidableEq S₁
a : σ →₀ ℕ
s : R
p : MvPolynomial σ R
ha : a ∉ p.support
hs : s ≠ 0
hp :
  Subset.{v} (α := Finset S₁) (coeffs.{v, u_1} (σ := σ) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p))
    (Finset.image (⇑f : (a : R) → S₁) p.coeffs)
ih :
  Subset.{v} (α := Finset S₁)
    (coeffs.{v, u_1} (σ := σ)
      ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) ((monomial a : (a : R) → MvPolynomial σ R) s)))
    (Finset.image.{u, v} (α := R) (⇑f : (a : R) → S₁)
      (coeffs.{u, u_1} (σ := σ) ((monomial a : (a : R) → MvPolynomial σ R) s)))
monomial_add :
  Subset.{v} (α := Finset S₁)
    (coeffs.{v, u_1} (σ := σ)
        ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) ((monomial a : (a : R) → MvPolynomial σ R) s)) ∪
      coeffs.{v, u_1} (σ := σ) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p))
    (Finset.image (⇑f : (a : R) → S₁)
      (coeffs.{u, u_1} (σ := σ) ((monomial a : (a : R) → MvPolynomial σ R) s) ∪ p.coeffs))
⊢ Subset.{v} (α := Finset S₁)
    (coeffs.{v, u_1} (σ := σ)
      ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁)
        (HAdd.hAdd (α := MvPolynomial σ R) ((monomial a : (a : R) → MvPolynomial σ R) s : MvPolynomial σ R) p)))
    (Finset.image (⇑f : (a : R) → S₁)
      (HAdd.hAdd (α := MvPolynomial σ R) ((monomial a : (a : R) → MvPolynomial σ R) s : MvPolynomial σ R) p).coeffs)
have monomial_add₁ : Disjoint.{u_1} (α := Finset (σ →₀ ℕ))
  (support.{v, u_1} (R := S₁)
    ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) ((monomial a : (a : R) → MvPolynomial σ R) s)))
  (support.{v, u_1} (R := S₁) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p))
Tactic: rw [coeffs_add (disjoint_support_monomial ha hs), map_add, coeffs_add]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
inst_2 : DecidableEq S₁
a : σ →₀ ℕ
s : R
p : MvPolynomial σ R
ha : a ∉ p.support
hs : s ≠ 0
hp :
  Subset.{v} (α := Finset S₁) (coeffs.{v, u_1} (σ := σ) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p))
    (Finset.image (⇑f : (a : R) → S₁) p.coeffs)
ih :
  Subset.{v} (α := Finset S₁)
    (coeffs.{v, u_1} (σ := σ)
      ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) ((monomial a : (a : R) → MvPolynomial σ R) s)))
    (Finset.image.{u, v} (α := R) (⇑f : (a : R) → S₁)
      (coeffs.{u, u_1} (σ := σ) ((monomial a : (a : R) → MvPolynomial σ R) s)))
⊢ Subset.{v} (α := Finset S₁)
    (coeffs.{v, u_1} (σ := σ)
        ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) ((monomial a : (a : R) → MvPolynomial σ R) s)) ∪
      coeffs.{v, u_1} (σ := σ) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p))
    (Finset.image (⇑f : (a : R) → S₁)
      (coeffs.{u, u_1} (σ := σ) ((monomial a : (a : R) → MvPolynomial σ R) s) ∪ p.coeffs))
have monomial_add : Subset.{v} (α := Finset S₁)
    (coeffs.{v, u_1} (σ := σ)
      ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) ((monomial a : (a : R) → MvPolynomial σ R) s)))
    (Finset.image.{u, v} (α := R) (⇑f : (a : R) → S₁)
        (coeffs.{u, u_1} (σ := σ) ((monomial a : (a : R) → MvPolynomial σ R) s)) ∪
      Finset.image (⇑f : (a : R) → S₁) p.coeffs) ∧
  Subset.{v} (α := Finset S₁) (coeffs.{v, u_1} (σ := σ) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p))
    (Finset.image.{u, v} (α := R) (⇑f : (a : R) → S₁)
        (coeffs.{u, u_1} (σ := σ) ((monomial a : (a : R) → MvPolynomial σ R) s)) ∪
      Finset.image (⇑f : (a : R) → S₁) p.coeffs)
Tactic: rw [Finset.image_union, Finset.union_subset_iff]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
p : MvPolynomial σ R
inst_2 : DecidableEq S₁
⊢ Subset.{v} (α := Finset S₁) (coeffs.{v, u_1} (σ := σ) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p))
    (Finset.image (⇑f : (a : R) → S₁) p.coeffs)
have C : ∀ (a : R),
  Subset.{v} (α := Finset S₁)
    (coeffs.{v, u_1} (σ := σ)
      ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) ((C : (a : R) → MvPolynomial σ R) a)))
    (Finset.image.{u, v} (α := R) (⇑f : (a : R) → S₁) (coeffs.{u, u_1} (σ := σ) ((C : (a : R) → MvPolynomial σ R) a)))
Tactic: induction p using induction_on'' with
  | C a => aesop (add simp coeffs_C)
  | mul_X p n ih => simpa
  | monomial_add a s p ha hs hp ih =>
    rw [coeffs_add (disjoint_support_monomial ha hs), map_add, coeffs_add]
    · rw [Finset.image_union, Finset.union_subset_iff]
      exact ⟨ih.trans (by simp), hp.trans (by simp)⟩
    · exact Finset.disjoint_of_subset_left (support_map_subset _ _) <|
        Finset.disjoint_of_subset_right (support_map_subset _ _) <|
          disjoint_support_monomial ha hs
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
p : MvPolynomial σ R
inst_2 : DecidableEq S₁
C :
  ∀ (a : R),
    Subset.{v} (α := Finset S₁)
      (coeffs.{v, u_1} (σ := σ)
        ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)))
      (Finset.image.{u, v} (α := R) (⇑f : (a : R) → S₁)
        (coeffs.{u, u_1} (σ := σ) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)))
⊢ Subset.{v} (α := Finset S₁) (coeffs.{v, u_1} (σ := σ) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p))
    (Finset.image (⇑f : (a : R) → S₁) p.coeffs)
have mul_X : ∀ (p : MvPolynomial σ R) (n : σ)
  (ih :
    Subset.{v} (α := Finset S₁) (coeffs.{v, u_1} (σ := σ) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p))
      (Finset.image (⇑f : (a : R) → S₁) p.coeffs)),
  Subset.{v} (α := Finset S₁)
    (coeffs.{v, u_1} (σ := σ) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) (p * X n)))
    (Finset.image (⇑f : (a : R) → S₁) (p * X n).coeffs)
Tactic: induction p using induction_on'' with
  | C a => aesop (add simp coeffs_C)
  | mul_X p n ih => simpa
  | monomial_add a s p ha hs hp ih =>
    rw [coeffs_add (disjoint_support_monomial ha hs), map_add, coeffs_add]
    · rw [Finset.image_union, Finset.union_subset_iff]
      exact ⟨ih.trans (by simp), hp.trans (by simp)⟩
    · exact Finset.disjoint_of_subset_left (support_map_subset _ _) <|
        Finset.disjoint_of_subset_right (support_map_subset _ _) <|
          disjoint_support_monomial ha hs
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
p : MvPolynomial σ R
inst_2 : DecidableEq S₁
C :
  ∀ (a : R),
    Subset.{v} (α := Finset S₁)
      (coeffs.{v, u_1} (σ := σ)
        ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)))
      (Finset.image.{u, v} (α := R) (⇑f : (a : R) → S₁)
        (coeffs.{u, u_1} (σ := σ) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)))
mul_X :
  ∀ (p : MvPolynomial σ R) (n : σ)
    (ih :
      Subset.{v} (α := Finset S₁) (coeffs.{v, u_1} (σ := σ) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p))
        (Finset.image (⇑f : (a : R) → S₁) p.coeffs)),
    Subset.{v} (α := Finset S₁)
      (coeffs.{v, u_1} (σ := σ) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) (p * X n)))
      (Finset.image (⇑f : (a : R) → S₁) (p * X n).coeffs)
⊢ Subset.{v} (α := Finset S₁) (coeffs.{v, u_1} (σ := σ) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p))
    (Finset.image (⇑f : (a : R) → S₁) p.coeffs)
have monomial_add : ∀ (a : σ →₀ ℕ) (s : R) (p : MvPolynomial σ R) (ha : a ∉ p.support) (hs : s ≠ 0)
  (hp :
    Subset.{v} (α := Finset S₁) (coeffs.{v, u_1} (σ := σ) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p))
      (Finset.image (⇑f : (a : R) → S₁) p.coeffs))
  (ih :
    Subset.{v} (α := Finset S₁)
      (coeffs.{v, u_1} (σ := σ)
        ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) ((monomial a : (a : R) → MvPolynomial σ R) s)))
      (Finset.image.{u, v} (α := R) (⇑f : (a : R) → S₁)
        (coeffs.{u, u_1} (σ := σ) ((monomial a : (a : R) → MvPolynomial σ R) s)))),
  Subset.{v} (α := Finset S₁)
    (coeffs.{v, u_1} (σ := σ)
      ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁)
        (HAdd.hAdd (α := MvPolynomial σ R) ((monomial a : (a : R) → MvPolynomial σ R) s : MvPolynomial σ R) p)))
    (Finset.image (⇑f : (a : R) → S₁)
      (HAdd.hAdd (α := MvPolynomial σ R) ((monomial a : (a : R) → MvPolynomial σ R) s : MvPolynomial σ R) p).coeffs)
Tactic: induction p using induction_on'' with
  | C a => aesop (add simp coeffs_C)
  | mul_X p n ih => simpa
  | monomial_add a s p ha hs hp ih =>
    rw [coeffs_add (disjoint_support_monomial ha hs), map_add, coeffs_add]
    · rw [Finset.image_union, Finset.union_subset_iff]
      exact ⟨ih.trans (by simp), hp.trans (by simp)⟩
    · exact Finset.disjoint_of_subset_left (support_map_subset _ _) <|
        Finset.disjoint_of_subset_right (support_map_subset _ _) <|
          disjoint_support_monomial ha hs
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
p : MvPolynomial σ R
inst_2 : DecidableEq S₁
⊢ Subset.{v} (α := Finset S₁) (coeffs.{v, u_1} (σ := σ) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p))
    (Finset.image (⇑f : (a : R) → S₁) p.coeffs)
have C : ∀ (a : R),
  Subset.{v} (α := Finset S₁)
    (coeffs.{v, u_1} (σ := σ)
      ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) ((C : (a : R) → MvPolynomial σ R) a)))
    (Finset.image.{u, v} (α := R) (⇑f : (a : R) → S₁) (coeffs.{u, u_1} (σ := σ) ((C : (a : R) → MvPolynomial σ R) a)))
Tactic: classical
  induction p using induction_on'' with
  | C a => aesop (add simp coeffs_C)
  | mul_X p n ih => simpa
  | monomial_add a s p ha hs hp ih =>
    rw [coeffs_add (disjoint_support_monomial ha hs), map_add, coeffs_add]
    · rw [Finset.image_union, Finset.union_subset_iff]
      exact ⟨ih.trans (by simp), hp.trans (by simp)⟩
    · exact Finset.disjoint_of_subset_left (support_map_subset _ _) <|
        Finset.disjoint_of_subset_right (support_map_subset _ _) <|
          disjoint_support_monomial ha hs
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
p : MvPolynomial σ R
inst_2 : DecidableEq S₁
C :
  ∀ (a : R),
    Subset.{v} (α := Finset S₁)
      (coeffs.{v, u_1} (σ := σ)
        ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)))
      (Finset.image.{u, v} (α := R) (⇑f : (a : R) → S₁)
        (coeffs.{u, u_1} (σ := σ) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)))
⊢ Subset.{v} (α := Finset S₁) (coeffs.{v, u_1} (σ := σ) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p))
    (Finset.image (⇑f : (a : R) → S₁) p.coeffs)
have mul_X : ∀ (p : MvPolynomial σ R) (n : σ)
  (ih :
    Subset.{v} (α := Finset S₁) (coeffs.{v, u_1} (σ := σ) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p))
      (Finset.image (⇑f : (a : R) → S₁) p.coeffs)),
  Subset.{v} (α := Finset S₁)
    (coeffs.{v, u_1} (σ := σ) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) (p * X n)))
    (Finset.image (⇑f : (a : R) → S₁) (p * X n).coeffs)
Tactic: classical
  induction p using induction_on'' with
  | C a => aesop (add simp coeffs_C)
  | mul_X p n ih => simpa
  | monomial_add a s p ha hs hp ih =>
    rw [coeffs_add (disjoint_support_monomial ha hs), map_add, coeffs_add]
    · rw [Finset.image_union, Finset.union_subset_iff]
      exact ⟨ih.trans (by simp), hp.trans (by simp)⟩
    · exact Finset.disjoint_of_subset_left (support_map_subset _ _) <|
        Finset.disjoint_of_subset_right (support_map_subset _ _) <|
          disjoint_support_monomial ha hs
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
p : MvPolynomial σ R
inst_2 : DecidableEq S₁
C :
  ∀ (a : R),
    Subset.{v} (α := Finset S₁)
      (coeffs.{v, u_1} (σ := σ)
        ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)))
      (Finset.image.{u, v} (α := R) (⇑f : (a : R) → S₁)
        (coeffs.{u, u_1} (σ := σ) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)))
mul_X :
  ∀ (p : MvPolynomial σ R) (n : σ)
    (ih :
      Subset.{v} (α := Finset S₁) (coeffs.{v, u_1} (σ := σ) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p))
        (Finset.image (⇑f : (a : R) → S₁) p.coeffs)),
    Subset.{v} (α := Finset S₁)
      (coeffs.{v, u_1} (σ := σ) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) (p * X n)))
      (Finset.image (⇑f : (a : R) → S₁) (p * X n).coeffs)
⊢ Subset.{v} (α := Finset S₁) (coeffs.{v, u_1} (σ := σ) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p))
    (Finset.image (⇑f : (a : R) → S₁) p.coeffs)
have monomial_add : ∀ (a : σ →₀ ℕ) (s : R) (p : MvPolynomial σ R) (ha : a ∉ p.support) (hs : s ≠ 0)
  (hp :
    Subset.{v} (α := Finset S₁) (coeffs.{v, u_1} (σ := σ) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p))
      (Finset.image (⇑f : (a : R) → S₁) p.coeffs))
  (ih :
    Subset.{v} (α := Finset S₁)
      (coeffs.{v, u_1} (σ := σ)
        ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) ((monomial a : (a : R) → MvPolynomial σ R) s)))
      (Finset.image.{u, v} (α := R) (⇑f : (a : R) → S₁)
        (coeffs.{u, u_1} (σ := σ) ((monomial a : (a : R) → MvPolynomial σ R) s)))),
  Subset.{v} (α := Finset S₁)
    (coeffs.{v, u_1} (σ := σ)
      ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁)
        (HAdd.hAdd (α := MvPolynomial σ R) ((monomial a : (a : R) → MvPolynomial σ R) s : MvPolynomial σ R) p)))
    (Finset.image (⇑f : (a : R) → S₁)
      (HAdd.hAdd (α := MvPolynomial σ R) ((monomial a : (a : R) → MvPolynomial σ R) s : MvPolynomial σ R) p).coeffs)
Tactic: classical
  induction p using induction_on'' with
  | C a => aesop (add simp coeffs_C)
  | mul_X p n ih => simpa
  | monomial_add a s p ha hs hp ih =>
    rw [coeffs_add (disjoint_support_monomial ha hs), map_add, coeffs_add]
    · rw [Finset.image_union, Finset.union_subset_iff]
      exact ⟨ih.trans (by simp), hp.trans (by simp)⟩
    · exact Finset.disjoint_of_subset_left (support_map_subset _ _) <|
        Finset.disjoint_of_subset_right (support_map_subset _ _) <|
          disjoint_support_monomial ha hs
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
x : MvPolynomial σ S₁
⊢ Membership.mem (γ := Set (MvPolynomial σ S₁))
      (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁)) x ↔
    (↑x.coeffs : Set S₁) ⊆ range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)
have refine_1 : ∀
  (hx :
    Membership.mem (γ := Set (MvPolynomial σ S₁))
      (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁)) x),
  (↑x.coeffs : Set S₁) ⊆ range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)
Tactic: refine ⟨fun hx ↦ ?_, fun hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
x : MvPolynomial σ S₁
refine_1 :
  ∀
    (hx :
      Membership.mem (γ := Set (MvPolynomial σ S₁))
        (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁)) x),
    (↑x.coeffs : Set S₁) ⊆ range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)
⊢ Membership.mem (γ := Set (MvPolynomial σ S₁))
      (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁)) x ↔
    (↑x.coeffs : Set S₁) ⊆ range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)
have refine_2 : ∀ (hx : (↑x.coeffs : Set S₁) ⊆ range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)),
  Membership.mem (γ := Set (MvPolynomial σ S₁))
    (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁)) x
Tactic: refine ⟨fun hx ↦ ?_, fun hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
x : MvPolynomial σ S₁
hx :
  Membership.mem (γ := Set (MvPolynomial σ S₁))
    (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁)) x
⊢ (↑x.coeffs : Set S₁) ⊆ range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)
have refine_1 : ∀ (p : MvPolynomial σ R),
  (↑(coeffs.{v, u_1} (σ := σ) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p)) : Set S₁) ⊆
    range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)
Tactic: obtain ⟨p, rfl⟩ := hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
a : S₁
hx :
  (↑(coeffs.{v, u_1} (σ := σ) ((C : (a : S₁) → MvPolynomial σ S₁) a)) : Set S₁) ⊆
    range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)
⊢ Membership.mem (α := MvPolynomial σ S₁) (γ := Set (MvPolynomial σ S₁))
    (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁))
    ((C : (a : S₁) → MvPolynomial σ S₁) a : MvPolynomial σ S₁)
have pos : ∀ (h : a = 0),
  Membership.mem (α := MvPolynomial σ S₁) (γ := Set (MvPolynomial σ S₁))
    (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁))
    ((C : (a : S₁) → MvPolynomial σ S₁) a : MvPolynomial σ S₁)
Tactic: by_cases h : a = 0
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
a : S₁
hx :
  (↑(coeffs.{v, u_1} (σ := σ) ((C : (a : S₁) → MvPolynomial σ S₁) a)) : Set S₁) ⊆
    range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)
pos :
  ∀ (h : a = 0),
    Membership.mem (α := MvPolynomial σ S₁) (γ := Set (MvPolynomial σ S₁))
      (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁))
      ((C : (a : S₁) → MvPolynomial σ S₁) a : MvPolynomial σ S₁)
⊢ Membership.mem (α := MvPolynomial σ S₁) (γ := Set (MvPolynomial σ S₁))
    (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁))
    ((C : (a : S₁) → MvPolynomial σ S₁) a : MvPolynomial σ S₁)
have neg : ∀ (h : ¬a = 0),
  Membership.mem (α := MvPolynomial σ S₁) (γ := Set (MvPolynomial σ S₁))
    (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁))
    ((C : (a : S₁) → MvPolynomial σ S₁) a : MvPolynomial σ S₁)
Tactic: by_cases h : a = 0
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
a : S₁
hx :
  (↑(coeffs.{v, u_1} (σ := σ) ((C : (a : S₁) → MvPolynomial σ S₁) a)) : Set S₁) ⊆
    range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)
h : a = 0
⊢ Membership.mem (α := MvPolynomial σ S₁) (γ := Set (MvPolynomial σ S₁))
    (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁))
    ((C : (a : S₁) → MvPolynomial σ S₁) a : MvPolynomial σ S₁)
have pos : ∀
  (hx :
    (↑(coeffs.{v, u_1} (σ := σ) ((C : (a : S₁) → MvPolynomial σ S₁) 0)) : Set S₁) ⊆
      range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)),
  Membership.mem (γ := Set (MvPolynomial σ S₁))
    (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁))
    ((C : (a : S₁) → MvPolynomial σ S₁) 0)
Tactic: subst h
Cleared hypotheses: a, hx, h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (hypothesis)
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
a : S₁
hx :
  (↑(coeffs.{v, u_1} (σ := σ) ((C : (a : S₁) → MvPolynomial σ S₁) a)) : Set S₁) ⊆
    range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)
h : ¬a = 0
⊢ Membership.mem (α := MvPolynomial σ S₁) (γ := Set (MvPolynomial σ S₁))
    (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁))
    ((C : (a : S₁) → MvPolynomial σ S₁) a : MvPolynomial σ S₁)
have hx₁ : Membership.mem (γ := Set S₁) (range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)) a
Tactic: simp only [coeffs_C, h, reduceIte, Finset.coe_singleton, Set.singleton_subset_iff] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
a : S₁
h : ¬a = 0
hx : Membership.mem (γ := Set S₁) (range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)) a
⊢ Membership.mem (α := MvPolynomial σ S₁) (γ := Set (MvPolynomial σ S₁))
    (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁))
    ((C : (a : S₁) → MvPolynomial σ S₁) a : MvPolynomial σ S₁)
have neg : ∀ (b : R) (h : ¬Eq.{v + 1} (α := S₁) ((f : (a : R) → S₁) b : S₁) (0 : S₁)),
  Membership.mem (α := MvPolynomial σ S₁) (γ := Set (MvPolynomial σ S₁))
    (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁))
    ((C : (a : S₁) → MvPolynomial σ S₁) ((f : (a : R) → S₁) b) : MvPolynomial σ S₁)
Tactic: obtain ⟨b, rfl⟩ := hx
Cleared hypotheses: a, h, hx
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (hypothesis)
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
p : MvPolynomial σ S₁
n : σ
ih :
  ∀ (hx : (↑p.coeffs : Set S₁) ⊆ range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)),
    Membership.mem (γ := Set (MvPolynomial σ S₁))
      (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁)) p
hx : (↑(p * X n).coeffs : Set S₁) ⊆ range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)
⊢ Membership.mem (γ := Set (MvPolynomial σ S₁))
    (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁)) (p * X n)
have hx₁ : (↑p.coeffs : Set S₁) ⊆ range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)
Tactic: rw [coeffs_mul_X] at hx
Cleared hypotheses: hx