awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
b : R
h : ¬Eq.{v + 1} (α := S₁) ((f : (a : R) → S₁) b : S₁) (0 : S₁)
⊢ Eq (α := MvPolynomial σ S₁)
    ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) ((C : (a : R) → MvPolynomial σ R) b) : MvPolynomial σ S₁)
    ((C : (a : S₁) → MvPolynomial σ S₁) ((f : (a : R) → S₁) b) : MvPolynomial σ S₁)

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
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:
exact ⟨C b, by simp⟩
-- Module: Mathlib.Algebra.MvPolynomial.Eval
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₁)
⊢ (↑p.coeffs : Set S₁) ⊆ range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)

Tactic:
rw [coeffs_mul_X] at hx

Premises used: MvPolynomial.coeffs_mul_X
-- Module: Mathlib.Algebra.MvPolynomial.Eval
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.coeffs : Set S₁) ⊆ range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)
refine_2 :
  ∀ (q : MvPolynomial σ R)
    (ih :
      ∀
        (hx :
          (↑(coeffs.{v, u_1} (σ := σ) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) q)) : 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₁))
          ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) q : MvPolynomial σ S₁))
    (hx :
      (↑(coeffs.{v, u_1} (σ := σ) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) q)) : 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₁))
      (HMul.hMul (α := MvPolynomial σ S₁) (β := MvPolynomial σ S₁)
        ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) q : MvPolynomial σ S₁) (X n))
⊢ Membership.mem (γ := Set (MvPolynomial σ S₁))
    (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁)) (p * X n)

Tactic:
obtain ⟨q, rfl⟩ := ih hx

Premises used: rfl
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
n : σ
q : MvPolynomial σ R
ih :
  ∀
    (hx :
      (↑(coeffs.{v, u_1} (σ := σ) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) q)) : 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₁))
      ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) q : MvPolynomial σ S₁)
hx :
  (↑(coeffs.{v, u_1} (σ := σ) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) q)) : Set S₁) ⊆
    range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)
⊢ (map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) (q * X n) =
    HMul.hMul (α := MvPolynomial σ S₁) (β := MvPolynomial σ S₁)
      ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) q : MvPolynomial σ S₁) (X n)

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
n : σ
q : MvPolynomial σ R
ih :
  ∀
    (hx :
      (↑(coeffs.{v, u_1} (σ := σ) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) q)) : 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₁))
      ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) q : MvPolynomial σ S₁)
hx :
  (↑(coeffs.{v, u_1} (σ := σ) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) q)) : 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₁))
    (HMul.hMul (α := MvPolynomial σ S₁) (β := MvPolynomial σ S₁)
      ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) q : MvPolynomial σ S₁) (X n))

Tactic:
exact ⟨q * X n, by simp⟩
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
a : σ →₀ ℕ
s : S₁
p : MvPolynomial σ S₁
ha : a ∉ p.support
hs : s ≠ 0
hp :
  ∀ (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
ih :
  ∀
    (hx :
      (↑(coeffs.{v, u_1} (σ := σ) ((monomial a : (a : S₁) → MvPolynomial σ S₁) s)) : 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₁))
      ((monomial a : (a : S₁) → MvPolynomial σ S₁) s : MvPolynomial σ S₁)
hx :
  (↑(HAdd.hAdd (α := MvPolynomial σ S₁) ((monomial a : (a : S₁) → MvPolynomial σ S₁) s : MvPolynomial σ S₁) p).coeffs :
      Set S₁) ⊆
    range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)
⊢ (↑(coeffs.{v, u_1} (σ := σ) ((monomial a : (a : S₁) → MvPolynomial σ S₁) s) ∪ p.coeffs) : Set S₁) ⊆
    range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)

Tactic:
rw [coeffs_add (disjoint_support_monomial ha hs)] at hx

Premises used: MvPolynomial.coeffs_add, MvPolynomial.disjoint_support_monomial
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
a : σ →₀ ℕ
s : S₁
p : MvPolynomial σ S₁
ha : a ∉ p.support
hs : s ≠ 0
hp :
  ∀ (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
ih :
  ∀
    (hx :
      (↑(coeffs.{v, u_1} (σ := σ) ((monomial a : (a : S₁) → MvPolynomial σ S₁) s)) : 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₁))
      ((monomial a : (a : S₁) → MvPolynomial σ S₁) s : MvPolynomial σ S₁)
hx :
  (↑(coeffs.{v, u_1} (σ := σ) ((monomial a : (a : S₁) → MvPolynomial σ S₁) s) ∪ p.coeffs) : Set S₁) ⊆
    range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)
⊢ (↑(coeffs.{v, u_1} (σ := σ) ((monomial a : (a : S₁) → MvPolynomial σ S₁) s)) : Set S₁) ⊆
      range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁) ∧
    (↑p.coeffs : Set S₁) ⊆ range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)

Tactic:
simp only [Finset.coe_union, Set.union_subset_iff] at hx

Premises used: Set.union_subset_iff, Finset.coe_union
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
a : σ →₀ ℕ
s : S₁
p : MvPolynomial σ S₁
ha : a ∉ p.support
hs : s ≠ 0
hp :
  ∀ (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
ih :
  ∀
    (hx :
      (↑(coeffs.{v, u_1} (σ := σ) ((monomial a : (a : S₁) → MvPolynomial σ S₁) s)) : 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₁))
      ((monomial a : (a : S₁) → MvPolynomial σ S₁) s : MvPolynomial σ S₁)
hx :
  (↑(coeffs.{v, u_1} (σ := σ) ((monomial a : (a : S₁) → MvPolynomial σ S₁) s)) : Set S₁) ⊆
      range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁) ∧
    (↑p.coeffs : Set S₁) ⊆ range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)
refine_2 :
  ∀ (q : MvPolynomial σ R)
    (hq :
      Eq (α := MvPolynomial σ S₁) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) q : MvPolynomial σ S₁)
        ((monomial a : (a : S₁) → MvPolynomial σ S₁) s : MvPolynomial σ S₁)),
    Membership.mem (γ := Set (MvPolynomial σ S₁))
      (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁))
      (HAdd.hAdd (α := MvPolynomial σ S₁) ((monomial a : (a : S₁) → MvPolynomial σ S₁) s : MvPolynomial σ S₁) p)
⊢ Membership.mem (γ := Set (MvPolynomial σ S₁))
    (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁))
    (HAdd.hAdd (α := MvPolynomial σ S₁) ((monomial a : (a : S₁) → MvPolynomial σ S₁) s : MvPolynomial σ S₁) p)

Tactic:
obtain ⟨q, hq⟩ := ih hx.1

Premises used: And.left
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
a : σ →₀ ℕ
s : S₁
p : MvPolynomial σ S₁
ha : a ∉ p.support
hs : s ≠ 0
hp :
  ∀ (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
ih :
  ∀
    (hx :
      (↑(coeffs.{v, u_1} (σ := σ) ((monomial a : (a : S₁) → MvPolynomial σ S₁) s)) : 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₁))
      ((monomial a : (a : S₁) → MvPolynomial σ S₁) s : MvPolynomial σ S₁)
hx :
  (↑(coeffs.{v, u_1} (σ := σ) ((monomial a : (a : S₁) → MvPolynomial σ S₁) s)) : Set S₁) ⊆
      range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁) ∧
    (↑p.coeffs : Set S₁) ⊆ range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)
q : MvPolynomial σ R
hq :
  Eq (α := MvPolynomial σ S₁) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) q : MvPolynomial σ S₁)
    ((monomial a : (a : S₁) → MvPolynomial σ S₁) s : MvPolynomial σ S₁)
refine_2 :
  ∀ (u : MvPolynomial σ R) (hu : (map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) u = p),
    Membership.mem (γ := Set (MvPolynomial σ S₁))
      (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁))
      (HAdd.hAdd (α := MvPolynomial σ S₁) ((monomial a : (a : S₁) → MvPolynomial σ S₁) s : MvPolynomial σ S₁) p)
⊢ Membership.mem (γ := Set (MvPolynomial σ S₁))
    (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁))
    (HAdd.hAdd (α := MvPolynomial σ S₁) ((monomial a : (a : S₁) → MvPolynomial σ S₁) s : MvPolynomial σ S₁) p)

Tactic:
obtain ⟨u, hu⟩ := hp hx.2

Premises used: And.right
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
a : σ →₀ ℕ
s : S₁
p : MvPolynomial σ S₁
ha : a ∉ p.support
hs : s ≠ 0
hp :
  ∀ (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
ih :
  ∀
    (hx :
      (↑(coeffs.{v, u_1} (σ := σ) ((monomial a : (a : S₁) → MvPolynomial σ S₁) s)) : 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₁))
      ((monomial a : (a : S₁) → MvPolynomial σ S₁) s : MvPolynomial σ S₁)
hx :
  (↑(coeffs.{v, u_1} (σ := σ) ((monomial a : (a : S₁) → MvPolynomial σ S₁) s)) : Set S₁) ⊆
      range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁) ∧
    (↑p.coeffs : Set S₁) ⊆ range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)
q : MvPolynomial σ R
hq :
  Eq (α := MvPolynomial σ S₁) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) q : MvPolynomial σ S₁)
    ((monomial a : (a : S₁) → MvPolynomial σ S₁) s : MvPolynomial σ S₁)
u : MvPolynomial σ R
hu : (map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) u = p
⊢ (map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) (q + u) =
    HAdd.hAdd (α := MvPolynomial σ S₁) ((monomial a : (a : S₁) → MvPolynomial σ S₁) s : MvPolynomial σ S₁) p

Tactic:
simp [hq, hu]
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
a : σ →₀ ℕ
s : S₁
p : MvPolynomial σ S₁
ha : a ∉ p.support
hs : s ≠ 0
hp :
  ∀ (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
ih :
  ∀
    (hx :
      (↑(coeffs.{v, u_1} (σ := σ) ((monomial a : (a : S₁) → MvPolynomial σ S₁) s)) : 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₁))
      ((monomial a : (a : S₁) → MvPolynomial σ S₁) s : MvPolynomial σ S₁)
hx :
  (↑(coeffs.{v, u_1} (σ := σ) ((monomial a : (a : S₁) → MvPolynomial σ S₁) s)) : Set S₁) ⊆
      range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁) ∧
    (↑p.coeffs : Set S₁) ⊆ range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)
q : MvPolynomial σ R
hq :
  Eq (α := MvPolynomial σ S₁) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) q : MvPolynomial σ S₁)
    ((monomial a : (a : S₁) → MvPolynomial σ S₁) s : MvPolynomial σ S₁)
u : MvPolynomial σ R
hu : (map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) u = p
⊢ Membership.mem (γ := Set (MvPolynomial σ S₁))
    (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁))
    (HAdd.hAdd (α := MvPolynomial σ S₁) ((monomial a : (a : S₁) → MvPolynomial σ S₁) s : MvPolynomial σ S₁) p)

Tactic:
exact ⟨q + u, by simp [hq, hu]⟩
-- Module: Mathlib.Algebra.MvPolynomial.Eval
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₁)
refine_2 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
⊢ 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:
classical
  refine ⟨fun hx ↦ ?_, fun hx ↦ ?_⟩
  · obtain ⟨p, rfl⟩ := hx
    exact subset_trans (coe_coeffs_map f p) (by simp)
  · induction x using induction_on'' with
    | C a =>
      by_cases h : a = 0
      · subst h
        exact ⟨0, by simp⟩
      · simp only [coeffs_C, h, reduceIte, Finset.coe_singleton, Set.singleton_subset_iff] at hx
        obtain ⟨b, rfl⟩ := hx
        exact ⟨C b, by simp⟩
    | mul_X p n ih =>
      rw [coeffs_mul_X] at hx
      obtain ⟨q, rfl⟩ := ih hx
      exact ⟨q * X n, by simp⟩
    | monomial_add a s p ha hs hp ih =>
      rw [coeffs_add (disjoint_support_monomial ha hs)] at hx
      simp only [Finset.coe_union, Set.union_subset_iff] at hx
      obtain ⟨q, hq⟩ := ih hx.1
      obtain ⟨u, hu⟩ := hp hx.2
      exact ⟨q + u, by simp [hq, hu]⟩

Premises used: Set.singleton_subset_iff, Finset.coe_singleton, MvPolynomial.coeffs_mul_X, Set.union_subset_iff, MvPolynomial.coeffs_C, MvPolynomial.induction_on'', reduceIte, MvPolynomial.C, rfl, Finset.coe_union
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst : CommSemiring R
inst_1 : CommSemiring S₁
p q : MvPolynomial σ R
f : R →+* S₁
inst_2 : Algebra R S₁
g : σ → S₁
r : R
⊢ OneHom.toFun (M := MvPolynomial σ R)
      (↑(↑(eval₂Hom (algebraMap R S₁) g) : MvPolynomial σ R →* S₁) : OneHom (MvPolynomial σ R) S₁)
      ((algebraMap R (MvPolynomial σ R) : (a : R) → MvPolynomial σ R) r) =
    (algebraMap R S₁ : (a : R) → S₁) r

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : Algebra R S₁
g : σ → S₁
P : MvPolynomial σ R
⊢ Eq.{v + 1} (α := S₁) ((eval₂AlgHom R g : (a : MvPolynomial σ R) → S₁) P : S₁)
    ((eval₂Hom (algebraMap R S₁) g : (a : MvPolynomial σ R) → S₁) P : S₁)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : Algebra R S₁
g : σ → S₁
⊢ Eq (α := (a : MvPolynomial σ R) → S₁) (⇑(eval₂AlgHom R g) : (a : MvPolynomial σ R) → S₁) (eval₂ (algebraMap R S₁) g)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, MvPolynomial.eval₂, Finset.sum, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : Algebra R S₁
g : σ → S₁
i : σ
⊢ (eval₂AlgHom R g : (a : MvPolynomial σ R) → S₁) (X i) = g i

Tactic:
eval₂_X (algebraMap R S₁) g i

Premises used: Multiset.sum, Multiset.foldr, Algebra.algebraMap, Finsupp.sum, MvPolynomial.eval₂_X, MvPolynomial.eval₂, Finset.sum
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : CommSemiring S₂
inst_3 : Algebra R S₁
inst_4 : Algebra R S₂
f : S₁ →ₐ[R] S₂
x : MvPolynomial σ S₁
⊢ Eq (α := MvPolynomial σ S₂) ((mapAlgHom f : (a : MvPolynomial σ S₁) → MvPolynomial σ S₂) x : MvPolynomial σ S₂)
    ((map (↑f : S₁ →+* S₂) : (a : MvPolynomial σ S₁) → MvPolynomial σ S₂) x : MvPolynomial σ S₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : Algebra R S₁
⊢ Eq (α := MvPolynomial σ S₁ →ₐ[R] MvPolynomial σ S₁) (mapAlgHom (AlgHom.id R S₁)) (AlgHom.id R (MvPolynomial σ S₁))

Tactic:
AlgHom.ext map_id

Premises used: AlgHom.ext, MvPolynomial.map_id
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : CommSemiring S₂
inst_3 : Algebra R S₁
inst_4 : Algebra R S₂
f : S₁ →ₐ[R] S₂
⊢ (↑(mapAlgHom f) : MvPolynomial σ S₁ →+* MvPolynomial σ S₂) = map (↑f : S₁ →+* S₂)

Tactic:
RingHom.mk_coe _ _ _ _ _

Premises used: AddMonoidAlgebra.mapRingHom, MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, MvPolynomial.map, RingHom.mk_coe
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : CommSemiring S₂
inst_3 : Algebra R S₁
inst_4 : Algebra R S₂
f : S₁ →ₐ[R] S₂
simp :
  range (ι := MvPolynomial σ S₁) (⇑(mapAlgHom f) : (a : MvPolynomial σ S₁) → MvPolynomial σ S₂) =
    (↑(coeffsIn σ ((Subalgebra.toSubmodule : (a : Subalgebra R S₂) → Submodule R S₂) f.range)) :
      Set (MvPolynomial σ S₂))
⊢ Eq (α := Submodule R (MvPolynomial σ S₂))
    ((Subalgebra.toSubmodule : (a : Subalgebra R (MvPolynomial σ S₂)) → Submodule R (MvPolynomial σ S₂))
        (AlgHom.range (mapAlgHom f)) :
      Submodule R (MvPolynomial σ S₂))
    (coeffsIn σ ((Subalgebra.toSubmodule : (a : Subalgebra R S₂) → Submodule R S₂) f.range) :
      Submodule R (MvPolynomial σ S₂))

Tactic:
simp only [← SetLike.coe_set_eq, Subalgebra.coe_toSubmodule, AlgHom.coe_range]

Premises used: AlgHom.coe_range, SetLike.coe_set_eq, Subalgebra.coe_toSubmodule
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : CommSemiring S₂
inst_3 : Algebra R S₁
inst_4 : Algebra R S₂
f : S₁ →ₐ[R] S₂
h :
  ∀ (x : MvPolynomial σ S₂),
    Membership.mem (γ := Set (MvPolynomial σ S₂))
        (range (ι := MvPolynomial σ S₁) (⇑(mapAlgHom f) : (a : MvPolynomial σ S₁) → MvPolynomial σ S₂)) x ↔
      x ∈
        (↑(coeffsIn σ ((Subalgebra.toSubmodule : (a : Subalgebra R S₂) → Submodule R S₂) f.range)) :
          Set (MvPolynomial σ S₂))
⊢ range (ι := MvPolynomial σ S₁) (⇑(mapAlgHom f) : (a : MvPolynomial σ S₁) → MvPolynomial σ S₂) =
    (↑(coeffsIn σ ((Subalgebra.toSubmodule : (a : Subalgebra R S₂) → Submodule R S₂) f.range)) :
      Set (MvPolynomial σ S₂))

Tactic:
ext
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : CommSemiring S₂
inst_3 : Algebra R S₁
inst_4 : Algebra R S₂
f : S₁ →ₐ[R] S₂
x : MvPolynomial σ S₂
h :
  (↑x.coeffs : Set S₂) ⊆ range.{w, v + 1} (ι := S₁) (⇑(↑f : S₁ →+* S₂) : (a : S₁) → S₂) ↔
    (↑x.coeffs : Set S₂) ⊆
      (↑((Subalgebra.toSubmodule : (a : Subalgebra R S₂) → Submodule R S₂) f.range : Submodule R S₂) : Set S₂)
⊢ Membership.mem (γ := Set (MvPolynomial σ S₂))
      (range (ι := MvPolynomial σ S₁) (⇑(mapAlgHom f) : (a : MvPolynomial σ S₁) → MvPolynomial σ S₂)) x ↔
    x ∈
      (↑(coeffsIn σ ((Subalgebra.toSubmodule : (a : Subalgebra R S₂) → Submodule R S₂) f.range)) :
        Set (MvPolynomial σ S₂))

Tactic:
erw [mem_range_map_iff_coeffs_subset, mem_coeffsIn_iff_coeffs_subset]

Premises used: MvPolynomial.mem_range_map_iff_coeffs_subset, MvPolynomial.mem_coeffsIn_iff_coeffs_subset
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : CommSemiring S₂
inst_3 : Algebra R S₁
inst_4 : Algebra R S₂
f : S₁ →ₐ[R] S₂
x : MvPolynomial σ S₂
⊢ (↑x.coeffs : Set S₂) ⊆ range.{w, v + 1} (ι := S₁) (⇑(↑f : S₁ →+* S₂) : (a : S₁) → S₂) ↔
    (↑x.coeffs : Set S₂) ⊆
      (↑((Subalgebra.toSubmodule : (a : Subalgebra R S₂) → Submodule R S₂) f.range : Submodule R S₂) : Set S₂)

Tactic:
simp [Set.subset_def]

Premises used: Set.subset_def
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : Algebra R S₁
f : σ → S₁
p : MvPolynomial σ R
⊢ (aeval f : (a : MvPolynomial σ R) → S₁) p = eval₂ (algebraMap R S₁) f p

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, MvPolynomial.eval₂, Finset.sum, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : Algebra R S₁
f : σ → S₁
p : MvPolynomial σ R
⊢ Eq.{v + 1} (α := S₁) ((aeval f : (a : MvPolynomial σ R) → S₁) p : S₁)
    ((eval₂Hom (algebraMap R S₁) f : (a : MvPolynomial σ R) → S₁) p : S₁)

Tactic:
rfl

Premises used: rfl