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₁
hf : Surjective.{u + 1, v + 1} (α := R) (β := S₁) (⇑f : (a : R) → S₁)
a b : MvPolynomial σ S₁
ha : ∃ (a_1 : MvPolynomial σ R), (map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) a_1 = a
hb : ∃ (a : MvPolynomial σ R), (map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) a = b
add :
  ∀ (a : MvPolynomial σ R),
    ∃ (a_1 : MvPolynomial σ R),
      (map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) a_1 =
        HAdd.hAdd (α := MvPolynomial σ S₁) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) a : MvPolynomial σ S₁)
          b
⊢ ∃ (a_1 : MvPolynomial σ R), (map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) a_1 = a + b

Tactic:
obtain ⟨a, rfl⟩ := ha

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₁
hf : Surjective.{u + 1, v + 1} (α := R) (β := S₁) (⇑f : (a : R) → S₁)
b : MvPolynomial σ S₁
hb : ∃ (a : MvPolynomial σ R), (map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) a = b
a : MvPolynomial σ R
add :
  ∀ (b : MvPolynomial σ R),
    ∃ (a_1 : MvPolynomial σ R),
      (map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) a_1 =
        HAdd.hAdd (α := MvPolynomial σ S₁) (β := MvPolynomial σ S₁)
          ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) a : MvPolynomial σ S₁)
          ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) b : MvPolynomial σ S₁)
⊢ ∃ (a_1 : MvPolynomial σ R),
    (map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) a_1 =
      HAdd.hAdd (α := MvPolynomial σ S₁) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) a : MvPolynomial σ S₁) b

Tactic:
obtain ⟨b, rfl⟩ := hb

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₁
hf : Surjective.{u + 1, v + 1} (α := R) (β := S₁) (⇑f : (a : R) → S₁)
a b : MvPolynomial σ R
⊢ ∃ (a_1 : MvPolynomial σ R),
    (map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) a_1 =
      HAdd.hAdd (α := MvPolynomial σ S₁) (β := MvPolynomial σ S₁)
        ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) a : MvPolynomial σ S₁)
        ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) b : MvPolynomial σ S₁)

Tactic:
⟨a + b, map_add _ _ _⟩

Premises used: map_add, HAdd.hAdd, Exists.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₁
hf : Surjective.{u + 1, v + 1} (α := R) (β := S₁) (⇑f : (a : R) → S₁)
a b : MvPolynomial σ R
⊢ ∃ (a_1 : MvPolynomial σ R),
    (map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) a_1 =
      HAdd.hAdd (α := MvPolynomial σ S₁) (β := MvPolynomial σ S₁)
        ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) a : MvPolynomial σ S₁)
        ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) b : MvPolynomial σ S₁)

Tactic:
exact ⟨a + b, map_add _ _ _⟩
-- 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₁
hf : Surjective.{u + 1, v + 1} (α := R) (β := S₁) (⇑f : (a : R) → S₁)
p : MvPolynomial σ S₁
monomial :
  ∀ (i : σ →₀ ℕ) (fr : S₁),
    ∃ (a : MvPolynomial σ R),
      Eq (α := MvPolynomial σ S₁) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) a : MvPolynomial σ S₁)
        ((MvPolynomial.monomial i : (a : S₁) → MvPolynomial σ S₁) fr : MvPolynomial σ S₁)
add :
  ∀ (a b : MvPolynomial σ S₁)
    (ha : ∃ (a_1 : MvPolynomial σ R), (map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) a_1 = a)
    (hb : ∃ (a : MvPolynomial σ R), (map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) a = b),
    ∃ (a_1 : MvPolynomial σ R), (map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) a_1 = a + b
⊢ ∃ (a : MvPolynomial σ R), (map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) a = p

Tactic:
induction p using MvPolynomial.induction_on' with
  | monomial i fr =>
    obtain ⟨r, rfl⟩ := hf fr
    exact ⟨monomial i r, map_monomial _ _ _⟩
  | add a b ha hb =>
    obtain ⟨a, rfl⟩ := ha
    obtain ⟨b, rfl⟩ := hb
    exact ⟨a + b, map_add _ _ _⟩

Premises used: MvPolynomial.monomial, 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₁
h_1 :
  Surjective (α := MvPolynomial σ R) (β := MvPolynomial σ S₁) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁)
s : S₁
p : MvPolynomial σ R
h :
  Eq (α := MvPolynomial σ S₁) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p : MvPolynomial σ S₁)
    ((C : (a : S₁) → MvPolynomial σ S₁) s : MvPolynomial σ S₁)
⊢ (f : (a : R) → S₁) (coeff 0 p) = s

Tactic:
simpa [coeff_map] using congr(coeff 0 $h)

Premises used: MvPolynomial.coeff_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₁
g : S₁ →+* R
hf : LeftInverse.{v + 1, u + 1} (α := S₁) (β := R) (⇑f : (a : R) → S₁) (⇑g : (a : S₁) → R)
X : MvPolynomial σ S₁
rw : (map (f.comp g) : (a : MvPolynomial σ S₁) → MvPolynomial σ S₁) X = X
rw₁ : (map (RingHom.id S₁) : (a : MvPolynomial σ S₁) → MvPolynomial σ S₁) X = X
rw₂ rw₃ : X = X
⊢ (map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) ((map g : (a : MvPolynomial σ S₁) → MvPolynomial σ R) X) = X

Tactic:
rw [map_map, (RingHom.ext hf : f.comp g = RingHom.id _), map_id]

Premises used: MvPolynomial.map_map, RingHom.ext, MvPolynomial.map_id
-- 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₁
g : S₁ →+* R
hf : RightInverse.{v + 1, u + 1} (α := S₁) (β := R) (⇑f : (a : R) → S₁) (⇑g : (a : S₁) → R)
⊢ RightInverse (α := MvPolynomial σ S₁) (β := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁)
    (⇑(map g) : (a : MvPolynomial σ S₁) → MvPolynomial σ R)

Tactic:
(map_leftInverse hf.leftInverse).rightInverse

Premises used: MvPolynomial.map_leftInverse, Function.LeftInverse.rightInverse, Function.RightInverse.leftInverse
-- 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₁
g : σ → S₁
p : MvPolynomial σ R
C :
  ∀ (a : R),
    (eval g : (a : MvPolynomial σ S₁) → S₁)
        ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a) :
          MvPolynomial σ S₁) =
      eval₂ f g ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)
add :
  ∀ (p q : MvPolynomial σ R),
    (eval g : (a : MvPolynomial σ S₁) → S₁)
          ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p : MvPolynomial σ S₁) =
        eval₂ f g p →
      (eval g : (a : MvPolynomial σ S₁) → S₁)
            ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) q : MvPolynomial σ S₁) =
          eval₂ f g q →
        (eval g : (a : MvPolynomial σ S₁) → S₁)
            ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) (p + q) : MvPolynomial σ S₁) =
          eval₂ f g (p + q)
mul_X :
  ∀ (p : MvPolynomial σ R) (n : σ),
    (eval g : (a : MvPolynomial σ S₁) → S₁)
          ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p : MvPolynomial σ S₁) =
        eval₂ f g p →
      (eval g : (a : MvPolynomial σ S₁) → S₁)
          ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) (p * X n) : MvPolynomial σ S₁) =
        eval₂ f g (p * X n)
⊢ (eval g : (a : MvPolynomial σ S₁) → S₁) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p : MvPolynomial σ S₁) =
    eval₂ f g p

Tactic:
apply MvPolynomial.induction_on p

Premises used: MvPolynomial.induction_on
-- 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₁
g : σ → S₁
p : MvPolynomial σ R
⊢ ∀ (a : R),
    (eval g : (a : MvPolynomial σ S₁) → S₁)
        ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) ((C : (a : R) → MvPolynomial σ R) a) :
          MvPolynomial σ S₁) =
      eval₂ f g ((C : (a : R) → MvPolynomial σ R) a)

Tactic:
simp +contextual
-- 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₁
g : σ → S₁
p : MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R),
    (eval g : (a : MvPolynomial σ S₁) → S₁)
          ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p : MvPolynomial σ S₁) =
        eval₂ f g p →
      (eval g : (a : MvPolynomial σ S₁) → S₁)
            ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) q : MvPolynomial σ S₁) =
          eval₂ f g q →
        (eval g : (a : MvPolynomial σ S₁) → S₁)
            ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) (p + q) : MvPolynomial σ S₁) =
          eval₂ f g (p + q)

Tactic:
simp +contextual
-- 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₁
g : σ → S₁
p : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    (eval g : (a : MvPolynomial σ S₁) → S₁)
          ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p : MvPolynomial σ S₁) =
        eval₂ f g p →
      (eval g : (a : MvPolynomial σ S₁) → S₁)
          ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) (p * X n) : MvPolynomial σ S₁) =
        eval₂ f g (p * X n)

Tactic:
simp +contextual
-- 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₁
g : σ → R
p : MvPolynomial σ R
rw :
  (f : (a : R) → S₁)
      ((eval g : (a : MvPolynomial σ R) → R)
          ((map (RingHom.id R) : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R) :
        R) =
    eval₂ f ((⇑f : (a : R) → S₁) ∘ g) ((map (RingHom.id R) : (a : MvPolynomial σ R) → MvPolynomial σ R) p)
rw₁ :
  (f : (a : R) → S₁) (eval₂ (RingHom.id R) g p) =
    eval₂ f ((⇑f : (a : R) → S₁) ∘ g) ((map (RingHom.id R) : (a : MvPolynomial σ R) → MvPolynomial σ R) p)
rw₂ rw₃ :
  eval₂ f ((⇑f : (a : R) → S₁) ∘ g) ((map (RingHom.id R) : (a : MvPolynomial σ R) → MvPolynomial σ R) p) =
    eval₂ f ((⇑f : (a : R) → S₁) ∘ g) ((map (RingHom.id R) : (a : MvPolynomial σ R) → MvPolynomial σ R) p)
⊢ (f : (a : R) → S₁) ((eval g : (a : MvPolynomial σ R) → R) p : R) = eval₂ f ((⇑f : (a : R) → S₁) ∘ g) p

Tactic:
rw [← p.map_id, eval_map, eval₂_comp_right]

Premises used: MvPolynomial.eval_map, MvPolynomial.eval₂_comp_right, 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₂
f : R →+* S₁
g : σ → S₂
φ : S₁ →+* S₂
p : MvPolynomial σ R
rw :
  (eval g : (a : MvPolynomial σ S₂) → S₂)
      ((map φ : (a : MvPolynomial σ S₁) → MvPolynomial σ S₂) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) :
        MvPolynomial σ S₂) =
    eval₂ (φ.comp f) g p
rw₁ :
  Eq.{w + 1} (α := S₂)
    ((eval g : (a : MvPolynomial σ S₂) → S₂)
        ((map φ : (a : MvPolynomial σ S₁) → MvPolynomial σ S₂)
            ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) :
          MvPolynomial σ S₂) :
      S₂)
    ((eval g : (a : MvPolynomial σ S₂) → S₂)
        ((map (φ.comp f) : (a : MvPolynomial σ R) → MvPolynomial σ S₂) p : MvPolynomial σ S₂) :
      S₂)
rw₂ rw₃ :
  Eq.{w + 1} (α := S₂)
    ((eval g : (a : MvPolynomial σ S₂) → S₂)
        ((map (φ.comp f) : (a : MvPolynomial σ R) → MvPolynomial σ S₂) p : MvPolynomial σ S₂) :
      S₂)
    ((eval g : (a : MvPolynomial σ S₂) → S₂)
        ((map (φ.comp f) : (a : MvPolynomial σ R) → MvPolynomial σ S₂) p : MvPolynomial σ S₂) :
      S₂)
⊢ eval₂ φ g ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) = eval₂ (φ.comp f) g p

Tactic:
rw [← eval_map, ← eval_map, map_map]

Premises used: MvPolynomial.eval_map, MvPolynomial.map_map
-- 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₂
f : R →+* S₁
g : σ → S₂
φ : S₁ →+* S₂
p : MvPolynomial σ R
⊢ Eq.{w + 1} (α := S₂)
    ((eval₂Hom φ g : (a : MvPolynomial σ S₁) → S₂)
        ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p : MvPolynomial σ S₁) :
      S₂)
    ((eval₂Hom (φ.comp f) g : (a : MvPolynomial σ R) → S₂) p : S₂)

Tactic:
eval₂_map f g φ p

Premises used: Multiset.sum, Multiset.foldr, MvPolynomial.eval₂_map, Finsupp.sum, MvPolynomial.eval₂, Finset.sum
-- 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₁
φ : MvPolynomial σ R
⊢ Eq.{v + 1} (α := S₁)
    ((constantCoeff : (a : MvPolynomial σ S₁) → S₁)
        ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) φ : MvPolynomial σ S₁) :
      S₁)
    ((f : (a : R) → S₁) ((constantCoeff : (a : MvPolynomial σ R) → R) φ : R) : S₁)

Tactic:
coeff_map f φ 0

Premises used: MvPolynomial.coeff, MvPolynomial.coeff_map, OfNat.ofNat
-- 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₁
hC :
  ∀ (x : R),
    Eq.{v + 1} (α := S₁)
      ((RingHom.comp (β := MvPolynomial σ R) (RingHom.comp constantCoeff (map f)) C : (a : R) → S₁) x : S₁)
      ((RingHom.comp (β := MvPolynomial σ R) (f.comp constantCoeff) C : (a : R) → S₁) x : S₁)
hX :
  ∀ (i : σ),
    Eq.{v + 1} (α := S₁) ((RingHom.comp constantCoeff (map f) : (a : MvPolynomial σ R) → S₁) (X i) : S₁)
      ((f.comp constantCoeff : (a : MvPolynomial σ R) → S₁) (X i) : S₁)
⊢ Eq (α := MvPolynomial σ R →+* S₁) (RingHom.comp constantCoeff (map f)) (f.comp constantCoeff)

Tactic:
ext
-- 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 : R
⊢ Eq.{v + 1} (α := S₁)
    ((RingHom.comp (β := MvPolynomial σ R) (RingHom.comp constantCoeff (map f)) C : (a : R) → S₁) x : S₁)
    ((RingHom.comp (β := MvPolynomial σ R) (f.comp constantCoeff) C : (a : R) → S₁) x : 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₁
i : σ
⊢ Eq.{v + 1} (α := S₁) ((RingHom.comp constantCoeff (map f) : (a : MvPolynomial σ R) → S₁) (X i) : S₁)
    ((f.comp constantCoeff : (a : MvPolynomial σ R) → S₁) (X i) : 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
simp :
  ∀ ⦃x : σ →₀ ℕ⦄,
    Ne.{v + 1} (α := S₁) (coeff x ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p)) 0 → coeff x p ≠ 0
⊢ support.{v, u_1} (R := S₁) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) ⊆ p.support

Tactic:
simp only [Finset.subset_iff, mem_support_iff]

Premises used: MvPolynomial.mem_support_iff, Finset.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
x : σ →₀ ℕ
hx : Ne.{v + 1} (α := S₁) (coeff x ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p)) 0
contrapose :
  ∀ (hx : coeff x p = 0), Eq.{v + 1} (α := S₁) (coeff x ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p)) 0
⊢ coeff x p ≠ 0

Tactic:
contrapose 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₁
p : MvPolynomial σ R
x : σ →₀ ℕ
hx : coeff x p = 0
rw : Eq.{v + 1} (α := S₁) ((f : (a : R) → S₁) (coeff x p) : S₁) (0 : S₁)
rw₁ : Eq.{v + 1} (α := S₁) ((f : (a : R) → S₁) 0 : S₁) (0 : S₁)
rw₂ rw₃ : Eq.{v + 1} (α := S₁) 0 0
⊢ Eq.{v + 1} (α := S₁) (coeff x ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p)) 0

Tactic:
rw [coeff_map, hx, map_zero]

Premises used: map_zero, MvPolynomial.coeff_map
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
p : MvPolynomial σ R
f : R →+* S₁
hf : Injective.{u + 1, v + 1} (α := R) (β := S₁) (⇑f : (a : R) → S₁)
H₁ : support.{v, u_1} (R := S₁) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) ⊆ p.support
H₂ : p.support ⊆ support.{v, u_1} (R := S₁) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p)
⊢ support.{v, u_1} (R := S₁) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) = p.support

Tactic:
apply Finset.Subset.antisymm

Premises used: Finset.Subset.antisymm
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
p : MvPolynomial σ R
f : R →+* S₁
hf : Injective.{u + 1, v + 1} (α := R) (β := S₁) (⇑f : (a : R) → S₁)
⊢ support.{v, u_1} (R := S₁) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) ⊆ p.support

Tactic:
MvPolynomial.support_map_subset _ _

Premises used: MvPolynomial.support_map_subset
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
p : MvPolynomial σ R
f : R →+* S₁
hf : Injective.{u + 1, v + 1} (α := R) (β := S₁) (⇑f : (a : R) → S₁)
⊢ support.{v, u_1} (R := S₁) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) ⊆ p.support

Tactic:
exact MvPolynomial.support_map_subset _ _

Premises used: MvPolynomial.support_map_subset
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
p : MvPolynomial σ R
f : R →+* S₁
hf : Injective.{u + 1, v + 1} (α := R) (β := S₁) (⇑f : (a : R) → S₁)
H₂ :
  ∀ ⦃x : σ →₀ ℕ⦄,
    coeff x p ≠ 0 → Ne.{v + 1} (α := S₁) (coeff x ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p)) 0
⊢ p.support ⊆ support.{v, u_1} (R := S₁) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p)

Tactic:
simp only [Finset.subset_iff, mem_support_iff]

Premises used: MvPolynomial.mem_support_iff, Finset.subset_iff
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
p : MvPolynomial σ R
f : R →+* S₁
hf : Injective.{u + 1, v + 1} (α := R) (β := S₁) (⇑f : (a : R) → S₁)
x : σ →₀ ℕ
hx : coeff x p ≠ 0
H₂ : ∀ (hx : Eq.{v + 1} (α := S₁) (coeff x ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p)) 0), coeff x p = 0
⊢ Ne.{v + 1} (α := S₁) (coeff x ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p)) 0

Tactic:
contrapose hx
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
p : MvPolynomial σ R
f : R →+* S₁
hf : Injective.{u + 1, v + 1} (α := R) (β := S₁) (⇑f : (a : R) → S₁)
x : σ →₀ ℕ
hx : Eq.{v + 1} (α := S₁) (coeff x ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p)) 0
⊢ Eq.{v + 1} (α := S₁) ((f : (a : R) → S₁) (coeff x p) : S₁) ((f : (a : R) → S₁) 0 : S₁)

Tactic:
rw [coeff_map, ← f.map_zero] at hx

Premises used: MvPolynomial.coeff_map, RingHom.map_zero
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
p : MvPolynomial σ R
f : R →+* S₁
hf : Injective.{u + 1, v + 1} (α := R) (β := S₁) (⇑f : (a : R) → S₁)
x : σ →₀ ℕ
hx : Eq.{v + 1} (α := S₁) ((f : (a : R) → S₁) (coeff x p) : S₁) ((f : (a : R) → S₁) 0 : S₁)
⊢ coeff x p = 0

Tactic:
hf hx
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
p : MvPolynomial σ R
f : R →+* S₁
hf : Injective.{u + 1, v + 1} (α := R) (β := S₁) (⇑f : (a : R) → S₁)
x : σ →₀ ℕ
hx : Eq.{v + 1} (α := S₁) ((f : (a : R) → S₁) (coeff x p) : S₁) ((f : (a : R) → S₁) 0 : S₁)
⊢ coeff x p = 0

Tactic:
exact hf hx
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
q : R →+* S₁
r : R
hr : ∀ (r' : R), Eq.{v + 1} (α := S₁) ((q : (a : R) → S₁) r' : S₁) (0 : S₁) ↔ r ∣ r'
φ : MvPolynomial σ R
rw :
  (∀ (i : σ →₀ ℕ), r ∣ coeff i φ) ↔
    ∀ (m : σ →₀ ℕ), Eq.{v + 1} (α := S₁) (coeff m ((map q : (a : MvPolynomial σ R) → MvPolynomial σ S₁) φ)) (coeff m 0)
⊢ (C : (a : R) → MvPolynomial σ R) r ∣ φ ↔
    Eq (α := MvPolynomial σ S₁) ((map q : (a : MvPolynomial σ R) → MvPolynomial σ S₁) φ : MvPolynomial σ S₁)
      (0 : MvPolynomial σ S₁)

Tactic:
rw [C_dvd_iff_dvd_coeff, MvPolynomial.ext_iff]

Premises used: MvPolynomial.ext_iff, MvPolynomial.C_dvd_iff_dvd_coeff
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
q : R →+* S₁
r : R
hr : ∀ (r' : R), Eq.{v + 1} (α := S₁) ((q : (a : R) → S₁) r' : S₁) (0 : S₁) ↔ r ∣ r'
φ : MvPolynomial σ R
⊢ (∀ (i : σ →₀ ℕ), r ∣ coeff i φ) ↔
    ∀ (m : σ →₀ ℕ), Eq.{v + 1} (α := S₁) (coeff m ((map q : (a : MvPolynomial σ R) → MvPolynomial σ S₁) φ)) (coeff m 0)

Tactic:
simp only [coeff_map, coeff_zero, hr]

Premises used: MvPolynomial.coeff_map, MvPolynomial.coeff_zero
-- 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₁
g : S₁ → R
hg : g 0 = 0
φ : MvPolynomial σ S₁
simp_rw :
  (∀ (m : σ →₀ ℕ), (f : (a : R) → S₁) (coeff m (mapRange g hg φ)) = coeff m φ) ↔
    ∀ (d : σ →₀ ℕ), (f : (a : R) → S₁) (g (coeff d φ)) = coeff d φ
⊢ (map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) (mapRange g hg φ) = φ ↔
    ∀ (d : σ →₀ ℕ), (f : (a : R) → S₁) (g (coeff d φ)) = coeff d φ

Tactic:
simp_rw [MvPolynomial.ext_iff, coeff_map]

Premises used: MvPolynomial.ext_iff, MvPolynomial.coeff_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₁
g : S₁ → R
hg : g 0 = 0
φ : MvPolynomial σ S₁
⊢ (∀ (m : σ →₀ ℕ), (f : (a : R) → S₁) (coeff m (mapRange g hg φ)) = coeff m φ) ↔
    ∀ (d : σ →₀ ℕ), (f : (a : R) → S₁) (g (coeff d φ)) = coeff d φ

Tactic:
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₁
inst_2 : DecidableEq S₁
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:
aesop (add simp coeffs_C)

Premises used: MvPolynomial.coeffs_C
-- 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₁
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:
simpa