awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MvPolynomial.Comap
Goal:
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
simp :
  Eq.{u_4 + 1} (α := R)
    ((eval₂Hom (RingHom.comp (β := MvPolynomial υ R) (eval₂Hom (algebraMap R R) x) (algebraMap R (MvPolynomial υ R)))
            fun (i : τ) ↦
            (eval₂Hom (algebraMap R R) x : (a : MvPolynomial υ R) → R)
              ((g : (a : MvPolynomial τ R) → MvPolynomial υ R) (X i) : MvPolynomial υ R) :
          (a : MvPolynomial τ R) → R)
        ((f : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i) : MvPolynomial τ R) :
      R)
    ((eval₂Hom (algebraMap R R) (comap g x) : (a : MvPolynomial τ R) → R)
        ((f : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i) : MvPolynomial τ R) :
      R)
⊢ (aeval x : (a : MvPolynomial υ R) → R)
      ((aeval fun (i : τ) ↦ (g : (a : MvPolynomial τ R) → MvPolynomial υ R) (X i) :
            (a : MvPolynomial τ R) → MvPolynomial υ R)
          ((f : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i)) :
        MvPolynomial υ R) =
    comap f (comap g x) i

Tactic:
simp only [comap, aeval_eq_eval₂Hom, map_eval₂Hom]

Premises used: MvPolynomial.comap, MvPolynomial.map_eval₂Hom, MvPolynomial.aeval_eq_eval₂Hom
-- Module: Mathlib.Algebra.MvPolynomial.Comap
Goal:
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
⊢ Eq.{u_4 + 1} (α := R)
    ((eval₂Hom (RingHom.comp (β := MvPolynomial υ R) (eval₂Hom (algebraMap R R) x) (algebraMap R (MvPolynomial υ R)))
            fun (i : τ) ↦
            (eval₂Hom (algebraMap R R) x : (a : MvPolynomial υ R) → R)
              ((g : (a : MvPolynomial τ R) → MvPolynomial υ R) (X i) : MvPolynomial υ R) :
          (a : MvPolynomial τ R) → R)
        ((f : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i) : MvPolynomial τ R) :
      R)
    ((eval₂Hom (algebraMap R R) (comap g x) : (a : MvPolynomial τ R) → R)
        ((f : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i) : MvPolynomial τ R) :
      R)

Tactic:
eval₂Hom_congr ?_ rfl rfl

Premises used: MvPolynomial.eval₂Hom_congr, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Comap
Goal:
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
refine :
  Eq (α := R →+* R)
    (RingHom.comp (β := MvPolynomial υ R) (eval₂Hom (algebraMap R R) x) (algebraMap R (MvPolynomial υ R)))
    (algebraMap R R)
⊢ Eq.{u_4 + 1} (α := R)
    ((eval₂Hom (RingHom.comp (β := MvPolynomial υ R) (eval₂Hom (algebraMap R R) x) (algebraMap R (MvPolynomial υ R)))
            fun (i : τ) ↦
            (eval₂Hom (algebraMap R R) x : (a : MvPolynomial υ R) → R)
              ((g : (a : MvPolynomial τ R) → MvPolynomial υ R) (X i) : MvPolynomial υ R) :
          (a : MvPolynomial τ R) → R)
        ((f : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i) : MvPolynomial τ R) :
      R)
    ((eval₂Hom (algebraMap R R) (comap g x) : (a : MvPolynomial τ R) → R)
        ((f : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i) : MvPolynomial τ R) :
      R)

Tactic:
refine eval₂Hom_congr ?_ rfl rfl

Premises used: MvPolynomial.eval₂Hom_congr, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Comap
Goal:
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
a :
  ∀ (r : R),
    Eq (α := R)
      ((RingHom.comp (β := MvPolynomial υ R) (eval₂Hom (algebraMap R R) x) (algebraMap R (MvPolynomial υ R)) :
            (a : R) → R)
          r :
        R)
      ((algebraMap R R : (a : R) → R) r : R)
⊢ Eq (α := R →+* R)
    (RingHom.comp (β := MvPolynomial υ R) (eval₂Hom (algebraMap R R) x) (algebraMap R (MvPolynomial υ R)))
    (algebraMap R R)

Tactic:
ext r
-- Module: Mathlib.Algebra.MvPolynomial.Comap
Goal:
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
r : R
⊢ Eq (α := R)
    ((RingHom.comp (β := MvPolynomial υ R) (eval₂Hom (algebraMap R R) x) (algebraMap R (MvPolynomial υ R)) :
          (a : R) → R)
        r :
      R)
    ((algebraMap R R : (a : R) → R) r : R)

Tactic:
apply aeval_C

Premises used: MvPolynomial.aeval_C
-- Module: Mathlib.Algebra.MvPolynomial.Comap
Goal:
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
h : ∀ (x : υ → R), comap (g.comp f) x = (comap f ∘ comap g) x
⊢ comap (g.comp f) = comap f ∘ comap g

Tactic:
funext x
-- Module: Mathlib.Algebra.MvPolynomial.Comap
Goal:
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
⊢ comap (g.comp f) x = (comap f ∘ comap g) x

Tactic:
comap_comp_apply _ _ _

Premises used: MvPolynomial.comap, MvPolynomial.comap_comp_apply
-- Module: Mathlib.Algebra.MvPolynomial.Comap
Goal:
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
⊢ comap (g.comp f) x = (comap f ∘ comap g) x

Tactic:
exact comap_comp_apply _ _ _

Premises used: MvPolynomial.comap_comp_apply
-- Module: Mathlib.Algebra.MvPolynomial.Comap
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial σ R
hf : ∀ (φ : MvPolynomial σ R), (f : (a : MvPolynomial σ R) → MvPolynomial σ R) φ = φ
x : σ → R
⊢ comap (AlgHom.id R (MvPolynomial σ R)) x = x

Tactic:
comap_id_apply x

Premises used: MvPolynomial.comap_id_apply
-- Module: Mathlib.Algebra.MvPolynomial.Comap
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial σ R
hf : ∀ (φ : MvPolynomial σ R), (f : (a : MvPolynomial σ R) → MvPolynomial σ R) φ = φ
x : σ → R
h : f = AlgHom.id R (MvPolynomial σ R)
⊢ comap f x = x

Tactic:
convert! comap_id_apply x

Premises used: MvPolynomial.comap_id_apply
-- Module: Mathlib.Algebra.MvPolynomial.Comap
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial σ R
hf : ∀ (φ : MvPolynomial σ R), (f : (a : MvPolynomial σ R) → MvPolynomial σ R) φ = φ
x : σ → R
h :
  ∀ (φ : σ),
    Eq (α := MvPolynomial σ R) ((f : (a : MvPolynomial σ R) → MvPolynomial σ R) (X φ) : MvPolynomial σ R)
      ((AlgHom.id R (MvPolynomial σ R) : (a : MvPolynomial σ R) → MvPolynomial σ R) (X φ) : MvPolynomial σ R)
⊢ f = AlgHom.id R (MvPolynomial σ R)

Tactic:
ext1 φ
-- Module: Mathlib.Algebra.MvPolynomial.Comap
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial σ R
hf : ∀ (φ : MvPolynomial σ R), (f : (a : MvPolynomial σ R) → MvPolynomial σ R) φ = φ
x : σ → R
φ : σ
⊢ Eq (α := MvPolynomial σ R) ((f : (a : MvPolynomial σ R) → MvPolynomial σ R) (X φ) : MvPolynomial σ R)
    ((AlgHom.id R (MvPolynomial σ R) : (a : MvPolynomial σ R) → MvPolynomial σ R) (X φ) : MvPolynomial σ R)

Tactic:
simp [hf, AlgHom.id_apply]

Premises used: AlgHom.id_apply
-- Module: Mathlib.Algebra.MvPolynomial.Comap
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
x : τ → R
h : ∀ (x_1 : σ), comap (rename f) x x_1 = (x ∘ f) x_1
⊢ comap (rename f) x = x ∘ f

Tactic:
funext
-- Module: Mathlib.Algebra.MvPolynomial.Comap
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
x : τ → R
x_1 : σ
⊢ comap (rename f) x x_1 = (x ∘ f) x_1

Tactic:
simp [rename_X, comap_apply, aeval_X]

Premises used: MvPolynomial.aeval_X, MvPolynomial.comap_apply, MvPolynomial.rename_X
-- Module: Mathlib.Algebra.MvPolynomial.Comap
Goal:
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst : CommSemiring R
f : MvPolynomial σ R ≃ₐ[R] MvPolynomial τ R
x : τ → R
rw :
  comap ((↑f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R).comp (↑f.symm : MvPolynomial τ R →ₐ[R] MvPolynomial σ R)) x = x
⊢ comap (↑f.symm : MvPolynomial τ R →ₐ[R] MvPolynomial σ R) (comap (↑f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R) x) = x

Tactic:
rw [← comap_comp_apply]

Premises used: MvPolynomial.comap_comp_apply
-- Module: Mathlib.Algebra.MvPolynomial.Comap
Goal:
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst : CommSemiring R
f : MvPolynomial σ R ≃ₐ[R] MvPolynomial τ R
x : τ → R
hf :
  ∀ (φ : MvPolynomial τ R),
    ((↑f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R).comp (↑f.symm : MvPolynomial τ R →ₐ[R] MvPolynomial σ R) :
          (a : MvPolynomial τ R) → MvPolynomial τ R)
        φ =
      φ
⊢ comap ((↑f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R).comp (↑f.symm : MvPolynomial τ R →ₐ[R] MvPolynomial σ R)) x = x

Tactic:
apply comap_eq_id_of_eq_id

Premises used: MvPolynomial.comap_eq_id_of_eq_id
-- Module: Mathlib.Algebra.MvPolynomial.Comap
Goal:
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst : CommSemiring R
f : MvPolynomial σ R ≃ₐ[R] MvPolynomial τ R
x : τ → R
φ : MvPolynomial τ R
⊢ ((↑f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R).comp (↑f.symm : MvPolynomial τ R →ₐ[R] MvPolynomial σ R) :
        (a : MvPolynomial τ R) → MvPolynomial τ R)
      φ =
    φ

Tactic:
simp only [AlgHom.id_apply, AlgEquiv.comp_symm]

Premises used: AlgEquiv.comp_symm, AlgHom.id_apply
-- Module: Mathlib.Algebra.MvPolynomial.Comap
Goal:
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst : CommSemiring R
f : MvPolynomial σ R ≃ₐ[R] MvPolynomial τ R
x : σ → R
rw :
  comap ((↑f.symm : MvPolynomial τ R →ₐ[R] MvPolynomial σ R).comp (↑f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R)) x = x
⊢ comap (↑f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R) (comap (↑f.symm : MvPolynomial τ R →ₐ[R] MvPolynomial σ R) x) = x

Tactic:
rw [← comap_comp_apply]

Premises used: MvPolynomial.comap_comp_apply
-- Module: Mathlib.Algebra.MvPolynomial.Comap
Goal:
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst : CommSemiring R
f : MvPolynomial σ R ≃ₐ[R] MvPolynomial τ R
x : σ → R
hf :
  ∀ (φ : MvPolynomial σ R),
    ((↑f.symm : MvPolynomial τ R →ₐ[R] MvPolynomial σ R).comp (↑f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R) :
          (a : MvPolynomial σ R) → MvPolynomial σ R)
        φ =
      φ
⊢ comap ((↑f.symm : MvPolynomial τ R →ₐ[R] MvPolynomial σ R).comp (↑f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R)) x = x

Tactic:
apply comap_eq_id_of_eq_id

Premises used: MvPolynomial.comap_eq_id_of_eq_id
-- Module: Mathlib.Algebra.MvPolynomial.Comap
Goal:
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst : CommSemiring R
f : MvPolynomial σ R ≃ₐ[R] MvPolynomial τ R
x : σ → R
φ : MvPolynomial σ R
⊢ ((↑f.symm : MvPolynomial τ R →ₐ[R] MvPolynomial σ R).comp (↑f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R) :
        (a : MvPolynomial σ R) → MvPolynomial σ R)
      φ =
    φ

Tactic:
simp only [AlgHom.id_apply, AlgEquiv.symm_comp]

Premises used: AlgEquiv.symm_comp, AlgHom.id_apply
-- Module: Mathlib.Algebra.MvPolynomial.Comap
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : MvPolynomial σ R ≃ₐ[R] MvPolynomial τ R
⊢ (⇑(comapEquiv f) : (a : τ → R) → σ → R) = comap (↑f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, MvPolynomial.comap, Finsupp.sum, MvPolynomial.eval₂, Finset.sum, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Comap
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : MvPolynomial σ R ≃ₐ[R] MvPolynomial τ R
⊢ (⇑(comapEquiv f).symm : (a : σ → R) → τ → R) = comap (↑f.symm : MvPolynomial τ R →ₐ[R] MvPolynomial σ R)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, MvPolynomial.comap, Finsupp.sum, MvPolynomial.eval₂, Finset.sum, rfl
-- Module: Mathlib.Algebra.MvPolynomial.CommRing
Goal:
R : Type u
σ : Type u_1
a a' : R
inst : CommRing R
⊢ (C : (a : R) → MvPolynomial σ R) (a - a') =
    HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      ((C : (a : R) → MvPolynomial σ R) a' : MvPolynomial σ R)

Tactic:
map_sub _ _ _

Premises used: map_sub
-- Module: Mathlib.Algebra.MvPolynomial.CommRing
Goal:
R : Type u
σ : Type u_1
a : R
inst : CommRing R
⊢ Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) (-a) : MvPolynomial σ R)
    (-(C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)

Tactic:
map_neg _ _

Premises used: map_neg
-- Module: Mathlib.Algebra.MvPolynomial.CommRing
Goal:
R : Type u
σ : Type u_1
inst : CommRing R
m : σ →₀ ℕ
p : MvPolynomial σ R
⊢ coeff m (-p) = -coeff m p

Tactic:
Finsupp.neg_apply _ _

Premises used: MvPolynomial.coeff, Finsupp.neg_apply
-- Module: Mathlib.Algebra.MvPolynomial.CommRing
Goal:
R : Type u
σ : Type u_1
inst : CommRing R
m : σ →₀ ℕ
p q : MvPolynomial σ R
⊢ coeff m (p - q) = coeff m p - coeff m q

Tactic:
Finsupp.sub_apply _ _ _

Premises used: Finsupp.sub_apply, MvPolynomial.coeff
-- Module: Mathlib.Algebra.MvPolynomial.CommRing
Goal:
R : Type u
σ : Type u_1
inst : CommRing R
p : MvPolynomial σ R
⊢ (-p).support = p.support

Tactic:
Finsupp.support_neg p

Premises used: MvPolynomial.support, Finsupp.support_neg
-- Module: Mathlib.Algebra.MvPolynomial.CommRing
Goal:
R : Type u
σ : Type u_1
inst : CommRing R
inst_1 : DecidableEq σ
p q : MvPolynomial σ R
⊢ (p - q).support ⊆ p.support ∪ q.support

Tactic:
Finsupp.support_sub

Premises used: Set.Mem, setOf, Finsupp.support_sub
-- Module: Mathlib.Algebra.MvPolynomial.CommRing
Goal:
R : Type u
σ : Type u_1
inst : CommRing R
p : MvPolynomial σ R
rw : (p.support.sup fun (s : σ →₀ ℕ) ↦ (toMultiset : (a : σ →₀ ℕ) → Multiset σ) s) = p.degrees
⊢ (-p).degrees = p.degrees

Tactic:
rw [degrees, support_neg]

Premises used: MvPolynomial.support_neg, MvPolynomial.degrees
-- Module: Mathlib.Algebra.MvPolynomial.CommRing
Goal:
R : Type u
σ : Type u_1
inst : CommRing R
p : MvPolynomial σ R
⊢ (p.support.sup fun (s : σ →₀ ℕ) ↦ (toMultiset : (a : σ →₀ ℕ) → Multiset σ) s) = p.degrees

Tactic:
rfl
-- Module: Mathlib.Algebra.MvPolynomial.CommRing
Goal:
R : Type u
σ : Type u_1
inst : CommRing R
inst_1 : DecidableEq σ
p q : MvPolynomial σ R
⊢ (p - q).degrees ≤ p.degrees ∪ q.degrees

Tactic:
simpa [degrees_def] using AddMonoidAlgebra.supDegree_sub_le

Premises used: MvPolynomial.degrees_def, AddMonoidAlgebra.supDegree_sub_le
-- Module: Mathlib.Algebra.MvPolynomial.CommRing
Goal:
R : Type u
σ : Type u_1
inst : CommRing R
i : σ
p : MvPolynomial σ R
rw : Multiset.count i (-p).degrees = degreeOf i p
rw₁ : Multiset.count i (-p).degrees = Multiset.count i p.degrees
rw₂ rw₃ : Multiset.count i p.degrees = Multiset.count i p.degrees
⊢ degreeOf i (-p) = degreeOf i p

Tactic:
rw [degreeOf, degreeOf, degrees_neg]

Premises used: MvPolynomial.degrees_neg, MvPolynomial.degreeOf
-- Module: Mathlib.Algebra.MvPolynomial.CommRing
Goal:
R : Type u
σ : Type u_1
inst : CommRing R
i : σ
p q : MvPolynomial σ R
⊢ degreeOf i (p - q) ≤ max (degreeOf i p) (degreeOf i q)

Tactic:
simpa only [sub_eq_add_neg, degreeOf_neg] using degreeOf_add_le i p (-q)

Premises used: sub_eq_add_neg, MvPolynomial.degreeOf_neg, Neg.neg, MvPolynomial.degreeOf_add_le
-- Module: Mathlib.Algebra.MvPolynomial.CommRing
Goal:
R : Type u
σ : Type u_1
inst : CommRing R
p : MvPolynomial σ R
⊢ (-p).vars = p.vars

Tactic:
simp [vars, degrees_neg]

Premises used: MvPolynomial.degrees_neg, MvPolynomial.vars
-- Module: Mathlib.Algebra.MvPolynomial.CommRing
Goal:
R : Type u
σ : Type u_1
inst : CommRing R
p q : MvPolynomial σ R
inst_1 : DecidableEq σ
⊢ (p + -q).vars ⊆ p.vars ∪ (-q).vars

Tactic:
vars_add_subset p (-q)

Premises used: MvPolynomial.vars_add_subset, Neg.neg
-- Module: Mathlib.Algebra.MvPolynomial.CommRing
Goal:
R : Type u
σ : Type u_1
inst : CommRing R
p q : MvPolynomial σ R
inst_1 : DecidableEq σ
h : p - q = p + -q
h₁ : q.vars = (-q).vars
⊢ (p - q).vars ⊆ p.vars ∪ q.vars

Tactic:
convert! vars_add_subset p (-q) using 2

Premises used: MvPolynomial.vars_add_subset, Neg.neg
-- Module: Mathlib.Algebra.MvPolynomial.CommRing
Goal:
R : Type u
σ : Type u_1
inst : CommRing R
p q : MvPolynomial σ R
inst_1 : DecidableEq σ
⊢ p - q = p + -q

Tactic:
simp [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.Algebra.MvPolynomial.CommRing
Goal:
R : Type u
σ : Type u_1
inst : CommRing R
p q : MvPolynomial σ R
inst_1 : DecidableEq σ
⊢ q.vars = (-q).vars

Tactic:
simp [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.Algebra.MvPolynomial.CommRing
Goal:
R : Type u
σ : Type u_1
inst : CommRing R
p q : MvPolynomial σ R
inst_1 : DecidableEq σ
hpq : Disjoint p.vars q.vars
⊢ Disjoint p.vars (-q).vars

Tactic:
rw [← vars_neg q] at hpq

Premises used: MvPolynomial.vars_neg
-- Module: Mathlib.Algebra.MvPolynomial.CommRing
Goal:
R : Type u
σ : Type u_1
inst : CommRing R
p q : MvPolynomial σ R
inst_1 : DecidableEq σ
hpq : Disjoint p.vars (-q).vars
⊢ (p + -q).vars = p.vars ∪ (-q).vars

Tactic:
vars_add_of_disjoint hpq

Premises used: MvPolynomial.vars_add_of_disjoint
-- Module: Mathlib.Algebra.MvPolynomial.CommRing
Goal:
R : Type u
σ : Type u_1
inst : CommRing R
p q : MvPolynomial σ R
inst_1 : DecidableEq σ
hpq : Disjoint p.vars (-q).vars
h : p - q = p + -q
h₁ : q.vars = (-q).vars
⊢ (p - q).vars = p.vars ∪ q.vars

Tactic:
convert! vars_add_of_disjoint hpq using 2

Premises used: MvPolynomial.vars_add_of_disjoint
-- Module: Mathlib.Algebra.MvPolynomial.CommRing
Goal:
R : Type u
σ : Type u_1
inst : CommRing R
p q : MvPolynomial σ R
inst_1 : DecidableEq σ
hpq : Disjoint p.vars (-q).vars
⊢ p - q = p + -q

Tactic:
simp [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.Algebra.MvPolynomial.CommRing
Goal:
R : Type u
σ : Type u_1
inst : CommRing R
p q : MvPolynomial σ R
inst_1 : DecidableEq σ
hpq : Disjoint p.vars (-q).vars
⊢ q.vars = (-q).vars

Tactic:
simp [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.Algebra.MvPolynomial.CommRing
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommRing R
p q : MvPolynomial σ R
inst_1 : CommRing S
f : R →+* S
g : σ → S
⊢ eval₂ f g (p - q) = eval₂ f g p - eval₂ f g q

Tactic:
(eval₂Hom f g).map_sub _ _

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, MvPolynomial.eval₂, MvPolynomial.eval₂Hom, RingHom.map_sub, Finset.sum
-- Module: Mathlib.Algebra.MvPolynomial.CommRing
Goal:
R : Type u
σ : Type u_1
inst : CommRing R
p q : MvPolynomial σ R
f : σ → R
⊢ (eval f : (a : MvPolynomial σ R) → R) (p - q) =
    HSub.hSub (α := R) (β := R) ((eval f : (a : MvPolynomial σ R) → R) p : R)
      ((eval f : (a : MvPolynomial σ R) → R) q : R)

Tactic:
eval₂_sub _ _ _

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, MvPolynomial.eval₂, MvPolynomial.eval₂_sub, Finset.sum
-- Module: Mathlib.Algebra.MvPolynomial.CommRing
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommRing R
p : MvPolynomial σ R
inst_1 : CommRing S
f : R →+* S
g : σ → S
⊢ eval₂ f g (-p) = -eval₂ f g p

Tactic:
(eval₂Hom f g).map_neg _

Premises used: Multiset.sum, Multiset.foldr, RingHom.map_neg, Finsupp.sum, MvPolynomial.eval₂, MvPolynomial.eval₂Hom, Finset.sum
-- Module: Mathlib.Algebra.MvPolynomial.CommRing
Goal:
R : Type u
σ : Type u_1
inst : CommRing R
p : MvPolynomial σ R
f : σ → R
⊢ Eq.{u + 1} (α := R) ((eval f : (a : MvPolynomial σ R) → R) (-p) : R) (-(eval f : (a : MvPolynomial σ R) → R) p : R)

Tactic:
eval₂_neg _ _ _

Premises used: Multiset.sum, Multiset.foldr, MvPolynomial.eval₂_neg, Finsupp.sum, MvPolynomial.eval₂, Finset.sum
-- Module: Mathlib.Algebra.MvPolynomial.CommRing
Goal:
S : Type v
σ : Type u_1
inst : CommRing S
f : RingHom.{u_1, v} (MvPolynomial σ ℤ) S
n : ℤ
⊢ Eq.{v + 1} (α := S) ((f : (a : MvPolynomial σ ℤ) → S) ((C : (a : ℤ) → MvPolynomial σ ℤ) n : MvPolynomial σ ℤ) : S)
    ((↑n : S) : S)

Tactic:
eq_intCast (f.comp C) n

Premises used: eq_intCast, RingHom.comp, MvPolynomial.C
-- Module: Mathlib.Algebra.MvPolynomial.CommRing
Goal:
S : Type v
inst : CommRing S
R : Type u
c : ℤ →+* S
f : RingHom.{u, v} (MvPolynomial R ℤ) S
x : MvPolynomial R ℤ
n : ℤ
rw : Eq (α := S) ((c : (a : ℤ) → S) n : S) ((↑n : S) : S)
⊢ eval₂.{0, v, u} (σ := R) c (comp (β := MvPolynomial R ℤ) (⇑f : (a : MvPolynomial R ℤ) → S) X)
      ((C : (a : ℤ) → MvPolynomial R ℤ) n) =
    (f : (a : MvPolynomial R ℤ) → S) ((C : (a : ℤ) → MvPolynomial R ℤ) n : MvPolynomial R ℤ)

Tactic:
rw [hom_C f, eval₂_C]

Premises used: MvPolynomial.hom_C, MvPolynomial.eval₂_C
-- Module: Mathlib.Algebra.MvPolynomial.CommRing
Goal:
S : Type v
inst : CommRing S
R : Type u
c : ℤ →+* S
f : RingHom.{u, v} (MvPolynomial R ℤ) S
x : MvPolynomial R ℤ
n : ℤ
⊢ Eq (α := S) ((c : (a : ℤ) → S) n : S) ((↑n : S) : S)

Tactic:
eq_intCast c n

Premises used: eq_intCast
-- Module: Mathlib.Algebra.MvPolynomial.CommRing
Goal:
S : Type v
inst : CommRing S
R : Type u
c : ℤ →+* S
f : RingHom.{u, v} (MvPolynomial R ℤ) S
x : MvPolynomial R ℤ
n : ℤ
⊢ Eq (α := S) ((c : (a : ℤ) → S) n : S) ((↑n : S) : S)

Tactic:
exact eq_intCast c n

Premises used: eq_intCast
-- Module: Mathlib.Algebra.MvPolynomial.CommRing
Goal:
S : Type v
inst : CommRing S
R : Type u
c : ℤ →+* S
f : RingHom.{u, v} (MvPolynomial R ℤ) S
x p q : MvPolynomial R ℤ
hp : eval₂ c (comp (β := MvPolynomial R ℤ) (⇑f : (a : MvPolynomial R ℤ) → S) X) p = (f : (a : MvPolynomial R ℤ) → S) p
hq : eval₂ c (comp (β := MvPolynomial R ℤ) (⇑f : (a : MvPolynomial R ℤ) → S) X) q = (f : (a : MvPolynomial R ℤ) → S) q
rw :
  HAdd.hAdd (α := S) (β := S) ((f : (a : MvPolynomial R ℤ) → S) p : S) ((f : (a : MvPolynomial R ℤ) → S) q : S) =
    (f : (a : MvPolynomial R ℤ) → S) (p + q)
⊢ eval₂ c (comp (β := MvPolynomial R ℤ) (⇑f : (a : MvPolynomial R ℤ) → S) X) (p + q) =
    (f : (a : MvPolynomial R ℤ) → S) (p + q)

Tactic:
rw [eval₂_add, hp, hq]

Premises used: MvPolynomial.eval₂_add
-- Module: Mathlib.Algebra.MvPolynomial.CommRing
Goal:
S : Type v
inst : CommRing S
R : Type u
c : ℤ →+* S
f : RingHom.{u, v} (MvPolynomial R ℤ) S
x p q : MvPolynomial R ℤ
hp : eval₂ c (comp (β := MvPolynomial R ℤ) (⇑f : (a : MvPolynomial R ℤ) → S) X) p = (f : (a : MvPolynomial R ℤ) → S) p
hq : eval₂ c (comp (β := MvPolynomial R ℤ) (⇑f : (a : MvPolynomial R ℤ) → S) X) q = (f : (a : MvPolynomial R ℤ) → S) q
⊢ HAdd.hAdd (α := S) (β := S) ((f : (a : MvPolynomial R ℤ) → S) p : S) ((f : (a : MvPolynomial R ℤ) → S) q : S) =
    (f : (a : MvPolynomial R ℤ) → S) (p + q)

Tactic:
(f.map_add _ _).symm

Premises used: RingHom.map_add, Eq.symm
-- Module: Mathlib.Algebra.MvPolynomial.CommRing
Goal:
S : Type v
inst : CommRing S
R : Type u
c : ℤ →+* S
f : RingHom.{u, v} (MvPolynomial R ℤ) S
x p q : MvPolynomial R ℤ
hp : eval₂ c (comp (β := MvPolynomial R ℤ) (⇑f : (a : MvPolynomial R ℤ) → S) X) p = (f : (a : MvPolynomial R ℤ) → S) p
hq : eval₂ c (comp (β := MvPolynomial R ℤ) (⇑f : (a : MvPolynomial R ℤ) → S) X) q = (f : (a : MvPolynomial R ℤ) → S) q
⊢ HAdd.hAdd (α := S) (β := S) ((f : (a : MvPolynomial R ℤ) → S) p : S) ((f : (a : MvPolynomial R ℤ) → S) q : S) =
    (f : (a : MvPolynomial R ℤ) → S) (p + q)

Tactic:
exact (f.map_add _ _).symm

Premises used: RingHom.map_add, Eq.symm
-- Module: Mathlib.Algebra.MvPolynomial.CommRing
Goal:
S : Type v
inst : CommRing S
R : Type u
c : ℤ →+* S
f : RingHom.{u, v} (MvPolynomial R ℤ) S
x p : MvPolynomial R ℤ
n : R
hp : eval₂ c (comp (β := MvPolynomial R ℤ) (⇑f : (a : MvPolynomial R ℤ) → S) X) p = (f : (a : MvPolynomial R ℤ) → S) p
rw :
  HMul.hMul (α := S) (β := S) ((f : (a : MvPolynomial R ℤ) → S) p : S)
      (comp (β := MvPolynomial R ℤ) (⇑f : (a : MvPolynomial R ℤ) → S) X n : S) =
    (f : (a : MvPolynomial R ℤ) → S) (p * X n)
⊢ eval₂ c (comp (β := MvPolynomial R ℤ) (⇑f : (a : MvPolynomial R ℤ) → S) X) (p * X n) =
    (f : (a : MvPolynomial R ℤ) → S) (p * X n)

Tactic:
rw [eval₂_mul, eval₂_X, hp]

Premises used: MvPolynomial.eval₂_X, MvPolynomial.eval₂_mul
-- Module: Mathlib.Algebra.MvPolynomial.CommRing
Goal:
S : Type v
inst : CommRing S
R : Type u
c : ℤ →+* S
f : RingHom.{u, v} (MvPolynomial R ℤ) S
x p : MvPolynomial R ℤ
n : R
hp : eval₂ c (comp (β := MvPolynomial R ℤ) (⇑f : (a : MvPolynomial R ℤ) → S) X) p = (f : (a : MvPolynomial R ℤ) → S) p
⊢ HMul.hMul (α := S) (β := S) ((f : (a : MvPolynomial R ℤ) → S) p : S)
      (comp (β := MvPolynomial R ℤ) (⇑f : (a : MvPolynomial R ℤ) → S) X n : S) =
    (f : (a : MvPolynomial R ℤ) → S) (p * X n)

Tactic:
(f.map_mul _ _).symm

Premises used: RingHom.map_mul, Eq.symm