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₁
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))
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))
⊢ 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:
rw [coeffs_add (disjoint_support_monomial ha hs), map_add, coeffs_add]

Premises used: MvPolynomial.coeffs_add, map_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₁
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)))
      (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)
⊢ 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 [Finset.image_union, Finset.union_subset_iff]

Premises used: Finset.image_union, Finset.union_subset_iff
-- 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₁
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₁)
    (Finset.image.{u, v} (α := R) (⇑f : (a : R) → S₁)
      (coeffs.{u, u_1} (σ := σ) ((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)

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₁
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₁) (Finset.image (⇑f : (a : R) → S₁) p.coeffs)
    (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:
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₁
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)))
      (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:
exact ⟨ih.trans (by simp), hp.trans (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₁
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)))
⊢ 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:
Finset.disjoint_of_subset_left (support_map_subset _ _) <|
        Finset.disjoint_of_subset_right (support_map_subset _ _) <|
          disjoint_support_monomial ha hs

Premises used: Finset.disjoint_of_subset_left, MvPolynomial.support_map_subset, MvPolynomial.disjoint_support_monomial, Finset.disjoint_of_subset_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₁
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)))
⊢ 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:
exact Finset.disjoint_of_subset_left (support_map_subset _ _) <|
        Finset.disjoint_of_subset_right (support_map_subset _ _) <|
          disjoint_support_monomial ha hs

Premises used: Finset.disjoint_of_subset_left, MvPolynomial.support_map_subset, MvPolynomial.disjoint_support_monomial, Finset.disjoint_of_subset_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₁
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)
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)
⊢ Subset.{v} (α := Finset S₁) (coeffs.{v, u_1} (σ := σ) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p))
    (Finset.image (⇑f : (a : R) → S₁) 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

Premises used: MvPolynomial.coeffs_add, MvPolynomial.coeffs_C, MvPolynomial.induction_on'', Finset.image_union, map_add, Finset.disjoint_of_subset_left, MvPolynomial.support_map_subset, Finset.disjoint_of_subset_right, MvPolynomial.C, Finset.union_subset_iff
-- 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 σ 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)
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)
⊢ Subset.{v} (α := Finset S₁) (coeffs.{v, u_1} (σ := σ) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p))
    (Finset.image (⇑f : (a : R) → S₁) 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

Premises used: MvPolynomial.coeffs_add, MvPolynomial.coeffs_C, MvPolynomial.induction_on'', Finset.image_union, map_add, Finset.disjoint_of_subset_left, MvPolynomial.support_map_subset, Finset.disjoint_of_subset_right, MvPolynomial.C, Finset.union_subset_iff
-- 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 σ R
⊢ (↑(coeffs.{v, u_1} (σ := σ) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p)) : Set S₁) ⊆
    (⇑f : (a : R) → S₁) '' (↑p.coeffs : Set R)

Tactic:
mod_cast coeffs_map f p

Premises used: SetLike.coe_subset_coe._simp_1, congrArg, MvPolynomial.coeffs, cast, Finset.coe_image._simp_1, HasSubset.Subset, SetLike.coe, MvPolynomial.coeffs_map, MvPolynomial.map, Eq.symm, DFunLike.coe, Eq.trans
-- 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 σ R
⊢ (↑(coeffs.{v, u_1} (σ := σ) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p)) : Set S₁) ⊆
    (⇑f : (a : R) → S₁) '' (↑p.coeffs : Set R)

Tactic:
exact mod_cast coeffs_map f p

Premises used: MvPolynomial.coeffs_map
-- 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 σ R
⊢ (↑(coeffs.{v, u_1} (σ := σ) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p)) : Set S₁) ⊆
    (⇑f : (a : R) → S₁) '' (↑p.coeffs : Set R)

Tactic:
classical
  exact mod_cast coeffs_map f p
-- 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₁
⊢ 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:
⟨fun hx ↦ ?_, fun hx ↦ ?_⟩

Premises used: Iff.intro
-- 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 :
  ∀ (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:
refine ⟨fun hx ↦ ?_, fun hx ↦ ?_⟩
-- 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₁
hx :
  Membership.mem (γ := Set (MvPolynomial σ S₁))
    (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁)) x
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₁)
⊢ (↑x.coeffs : Set S₁) ⊆ range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)

Tactic:
obtain ⟨p, rfl⟩ := 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₁
p : MvPolynomial σ R
⊢ Subset.{v} (α := Set S₁) ((⇑f : (a : R) → S₁) '' (↑p.coeffs : Set R)) (range.{v, u + 1} (ι := R) (⇑f : (a : R) → 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₁
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:
exact subset_trans (coe_coeffs_map f p) (by simp)

Premises used: subset_trans, MvPolynomial.coe_coeffs_map
-- 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₁
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₁)
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₁)
⊢ 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
-- 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₁
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
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)
⊢ 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:
subst h
-- 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₁
hx :
  (↑(coeffs.{v, u_1} (σ := σ) ((C : (a : S₁) → MvPolynomial σ S₁) 0)) : Set S₁) ⊆
    range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)
⊢ Eq (α := MvPolynomial σ S₁) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) 0)
    ((C : (a : S₁) → MvPolynomial σ S₁) 0)

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₁
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:
exact ⟨0, 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₁
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 (γ := 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

Premises used: Set.singleton_subset_iff, Finset.coe_singleton, MvPolynomial.coeffs_C, reduceIte
-- 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₁
h : ¬a = 0
hx : Membership.mem (γ := Set S₁) (range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)) a
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₁)
⊢ 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:
obtain ⟨b, rfl⟩ := hx

Premises used: rfl