awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MvPolynomial.Polynomial
Goal:
R : Type u_1
n : ℕ
x : Fin n → R
inst : CommSemiring R
f : MvPolynomial (Fin (n + 1)) R
q : MvPolynomial (Fin n) R
simp :
  Eq (α := R)
    ((eval fun (s : Fin (n + 1)) ↦
            (eval x : (a : MvPolynomial (Fin n) R) → R)
              (Polynomial.eval q
                (Fin.cases (motive := fun (x : Fin (n + 1)) ↦ Polynomial (MvPolynomial (Fin n) R)) Polynomial.X
                  (fun (k : Fin n) ↦
                    (Polynomial.C : (a : MvPolynomial (Fin n) R) → Polynomial (MvPolynomial (Fin n) R)) (X k))
                  s)) :
          (a : MvPolynomial (Fin (n + 1)) R) → R)
        f :
      R)
    ((eval fun (i : Fin (n + 1)) ↦
            Fin.cases (motive := fun (x : Fin (n + 1)) ↦ R) ((eval x : (a : MvPolynomial (Fin n) R) → R) q) x i :
          (a : MvPolynomial (Fin (n + 1)) R) → R)
        f :
      R)
⊢ eval₂ (RingHom.id R)
      (fun (s : Fin (n + 1)) ↦
        (eval x : (a : MvPolynomial (Fin n) R) → R)
          (Polynomial.eval q
            (Fin.cases (motive := fun (x : Fin (n + 1)) ↦ Polynomial (MvPolynomial (Fin n) R)) Polynomial.X
              (fun (k : Fin n) ↦
                (Polynomial.C : (a : MvPolynomial (Fin n) R) → Polynomial (MvPolynomial (Fin n) R)) (X k))
              s)))
      f =
    (eval fun (i : Fin (n + 1)) ↦
          Fin.cases (motive := fun (x : Fin (n + 1)) ↦ R) ((eval x : (a : MvPolynomial (Fin n) R) → R) q) x i :
        (a : MvPolynomial (Fin (n + 1)) R) → R)
      f

Tactic:
simp only [eval₂_id]

Premises used: MvPolynomial.eval₂_id
-- Module: Mathlib.Algebra.MvPolynomial.Polynomial
Goal:
R : Type u_1
n : ℕ
x : Fin n → R
inst : CommSemiring R
f : MvPolynomial (Fin (n + 1)) R
q : MvPolynomial (Fin n) R
e_a :
  Eq.{u_1 + 1} (α := Fin (n + 1) → R)
    (fun (s : Fin (n + 1)) ↦
      (eval x : (a : MvPolynomial (Fin n) R) → R)
        (Polynomial.eval q
          (Fin.cases (motive := fun (x : Fin (n + 1)) ↦ Polynomial (MvPolynomial (Fin n) R)) Polynomial.X
            (fun (k : Fin n) ↦
              (Polynomial.C : (a : MvPolynomial (Fin n) R) → Polynomial (MvPolynomial (Fin n) R)) (X k))
            s)))
    fun (i : Fin (n + 1)) ↦
    Fin.cases (motive := fun (x : Fin (n + 1)) ↦ R) ((eval x : (a : MvPolynomial (Fin n) R) → R) q) x i
⊢ Eq (α := R)
    ((eval fun (s : Fin (n + 1)) ↦
            (eval x : (a : MvPolynomial (Fin n) R) → R)
              (Polynomial.eval q
                (Fin.cases (motive := fun (x : Fin (n + 1)) ↦ Polynomial (MvPolynomial (Fin n) R)) Polynomial.X
                  (fun (k : Fin n) ↦
                    (Polynomial.C : (a : MvPolynomial (Fin n) R) → Polynomial (MvPolynomial (Fin n) R)) (X k))
                  s)) :
          (a : MvPolynomial (Fin (n + 1)) R) → R)
        f :
      R)
    ((eval fun (i : Fin (n + 1)) ↦
            Fin.cases (motive := fun (x : Fin (n + 1)) ↦ R) ((eval x : (a : MvPolynomial (Fin n) R) → R) q) x i :
          (a : MvPolynomial (Fin (n + 1)) R) → R)
        f :
      R)

Tactic:
congr
-- Module: Mathlib.Algebra.MvPolynomial.Polynomial
Goal:
R : Type u_1
n : ℕ
x : Fin n → R
inst : CommSemiring R
f : MvPolynomial (Fin (n + 1)) R
q : MvPolynomial (Fin n) R
e_a :
  ∀ (i : Fin (n + 1)),
    Eq (α := R)
      ((eval x : (a : MvPolynomial (Fin n) R) → R)
          (Polynomial.eval q
            (Fin.cases (motive := fun (x : Fin (n + 1)) ↦ Polynomial (MvPolynomial (Fin n) R)) Polynomial.X
              (fun (k : Fin n) ↦
                (Polynomial.C : (a : MvPolynomial (Fin n) R) → Polynomial (MvPolynomial (Fin n) R)) (X k))
              i)) :
        R)
      (Fin.cases (motive := fun (x : Fin (n + 1)) ↦ R) ((eval x : (a : MvPolynomial (Fin n) R) → R) q) x i : R)
⊢ Eq.{u_1 + 1} (α := Fin (n + 1) → R)
    (fun (s : Fin (n + 1)) ↦
      (eval x : (a : MvPolynomial (Fin n) R) → R)
        (Polynomial.eval q
          (Fin.cases (motive := fun (x : Fin (n + 1)) ↦ Polynomial (MvPolynomial (Fin n) R)) Polynomial.X
            (fun (k : Fin n) ↦
              (Polynomial.C : (a : MvPolynomial (Fin n) R) → Polynomial (MvPolynomial (Fin n) R)) (X k))
            s)))
    fun (i : Fin (n + 1)) ↦
    Fin.cases (motive := fun (x : Fin (n + 1)) ↦ R) ((eval x : (a : MvPolynomial (Fin n) R) → R) q) x i

Tactic:
funext i
-- Module: Mathlib.Algebra.MvPolynomial.Polynomial
Goal:
R : Type u_1
n : ℕ
x : Fin n → R
inst : CommSemiring R
f : MvPolynomial (Fin (n + 1)) R
q : MvPolynomial (Fin n) R
i : Fin (n + 1)
⊢ Eq (α := R)
    ((eval x : (a : MvPolynomial (Fin n) R) → R)
        (Polynomial.eval q
          (Fin.cases (motive := fun (x : Fin (n + 1)) ↦ Polynomial (MvPolynomial (Fin n) R)) Polynomial.X
            (fun (k : Fin n) ↦
              (Polynomial.C : (a : MvPolynomial (Fin n) R) → Polynomial (MvPolynomial (Fin n) R)) (X k))
            0)) :
      R)
    (Fin.cases (motive := fun (x : Fin (n + 1)) ↦ R) ((eval x : (a : MvPolynomial (Fin n) R) → R) q) x 0 : R)

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Polynomial
Goal:
R : Type u_1
n : ℕ
x : Fin n → R
inst : CommSemiring R
f : MvPolynomial (Fin (n + 1)) R
q : MvPolynomial (Fin n) R
i : Fin (n + 1)
⊢ ∀ (i : Fin n),
    Eq (α := R)
      ((eval x : (a : MvPolynomial (Fin n) R) → R)
          (Polynomial.eval q
            (Fin.cases (motive := fun (x : Fin (n + 1)) ↦ Polynomial (MvPolynomial (Fin n) R)) Polynomial.X
              (fun (k : Fin n) ↦
                (Polynomial.C : (a : MvPolynomial (Fin n) R) → Polynomial (MvPolynomial (Fin n) R)) (X k))
              i.succ)) :
        R)
      (Fin.cases (motive := fun (x : Fin (n + 1)) ↦ R) ((eval x : (a : MvPolynomial (Fin n) R) → R) q) x i.succ : R)

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Polynomial
Goal:
R : Type u_1
n : ℕ
x : Fin n → R
inst : CommSemiring R
f : MvPolynomial (Fin (n + 1)) R
q : MvPolynomial (Fin n) R
i : Fin (n + 1)
⊢ Eq (α := R)
    ((eval x : (a : MvPolynomial (Fin n) R) → R)
        (Polynomial.eval q
          (Fin.cases (motive := fun (x : Fin (n + 1)) ↦ Polynomial (MvPolynomial (Fin n) R)) Polynomial.X
            (fun (k : Fin n) ↦
              (Polynomial.C : (a : MvPolynomial (Fin n) R) → Polynomial (MvPolynomial (Fin n) R)) (X k))
            i)) :
      R)
    (Fin.cases (motive := fun (x : Fin (n + 1)) ↦ R) ((eval x : (a : MvPolynomial (Fin n) R) → R) q) x i : R)

Tactic:
refine Fin.cases (by simp) (by simp) i
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
r : R
⊢ Eq (α := MvPolynomial τ R)
    ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) ((C : (a : R) → MvPolynomial σ R) r) : MvPolynomial τ R)
    ((C : (a : R) → MvPolynomial τ R) r : MvPolynomial τ R)

Tactic:
eval₂_C _ _ _

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, MvPolynomial.eval₂_C, MvPolynomial.eval₂, Finset.sum
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
i : σ
⊢ Eq (α := MvPolynomial τ R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i) : MvPolynomial τ R)
    (X (f i) : MvPolynomial τ R)

Tactic:
eval₂_X _ _ _

Premises used: Multiset.sum, Multiset.foldr, MvPolynomial.X, Finsupp.sum, MvPolynomial.eval₂_X, MvPolynomial.eval₂, Finset.sum
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
⊢ Eq (α := MvPolynomial τ R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) 0) 0

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, MvPolynomial.eval₂, List.foldr, Finset.sum, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
g : σ → τ
p : MvPolynomial σ R
a : R
⊢ Eq (α := MvPolynomial τ S)
    ((map f : (a : MvPolynomial τ R) → MvPolynomial τ S)
        ((rename g : (a : MvPolynomial σ R) → MvPolynomial τ R) ((C : (a : R) → MvPolynomial σ R) a)) :
      MvPolynomial τ S)
    ((rename g : (a : MvPolynomial σ S) → MvPolynomial τ S)
        ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S) ((C : (a : R) → MvPolynomial σ R) a)) :
      MvPolynomial τ S)

Tactic:
simp only [map_C, rename_C]

Premises used: MvPolynomial.map_C, MvPolynomial.rename_C
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
g : σ → τ
p_1 p q : MvPolynomial σ R
hp :
  Eq (α := MvPolynomial τ S)
    ((map f : (a : MvPolynomial τ R) → MvPolynomial τ S) ((rename g : (a : MvPolynomial σ R) → MvPolynomial τ R) p) :
      MvPolynomial τ S)
    ((rename g : (a : MvPolynomial σ S) → MvPolynomial τ S) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S) p) :
      MvPolynomial τ S)
hq :
  Eq (α := MvPolynomial τ S)
    ((map f : (a : MvPolynomial τ R) → MvPolynomial τ S) ((rename g : (a : MvPolynomial σ R) → MvPolynomial τ R) q) :
      MvPolynomial τ S)
    ((rename g : (a : MvPolynomial σ S) → MvPolynomial τ S) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S) q) :
      MvPolynomial τ S)
⊢ Eq (α := MvPolynomial τ S)
    ((map f : (a : MvPolynomial τ R) → MvPolynomial τ S)
        ((rename g : (a : MvPolynomial σ R) → MvPolynomial τ R) (p + q)) :
      MvPolynomial τ S)
    ((rename g : (a : MvPolynomial σ S) → MvPolynomial τ S)
        ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S) (p + q)) :
      MvPolynomial τ S)

Tactic:
simp only [hp, hq, map_add]

Premises used: map_add
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
g : σ → τ
p_1 p : MvPolynomial σ R
n : σ
hp :
  Eq (α := MvPolynomial τ S)
    ((map f : (a : MvPolynomial τ R) → MvPolynomial τ S) ((rename g : (a : MvPolynomial σ R) → MvPolynomial τ R) p) :
      MvPolynomial τ S)
    ((rename g : (a : MvPolynomial σ S) → MvPolynomial τ S) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S) p) :
      MvPolynomial τ S)
⊢ Eq (α := MvPolynomial τ S)
    ((map f : (a : MvPolynomial τ R) → MvPolynomial τ S)
        ((rename g : (a : MvPolynomial σ R) → MvPolynomial τ R) (p * X n)) :
      MvPolynomial τ S)
    ((rename g : (a : MvPolynomial σ S) → MvPolynomial τ S)
        ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S) (p * X n)) :
      MvPolynomial τ S)

Tactic:
simp only [hp, rename_X, map_X, map_mul]

Premises used: map_mul, MvPolynomial.rename_X, MvPolynomial.map_X
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
g : σ → τ
p : MvPolynomial σ R
⊢ Eq (α := MvPolynomial τ S)
    ((map f : (a : MvPolynomial τ R) → MvPolynomial τ S) ((rename g : (a : MvPolynomial σ R) → MvPolynomial τ R) p) :
      MvPolynomial τ S)
    ((rename g : (a : MvPolynomial σ S) → MvPolynomial τ S) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S) p) :
      MvPolynomial τ S)

Tactic:
apply MvPolynomial.induction_on p
    (fun a => by simp only [map_C, rename_C])
    (fun p q hp hq => by simp only [hp, hq, map_add]) fun p n hp => by
    simp only [hp, rename_X, map_X, map_mul]

Premises used: MvPolynomial.induction_on
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
g : σ → τ
⊢ RingHom.comp (map f) (AlgHom.toRingHom (rename g)) = RingHom.comp (AlgHom.toRingHom (rename g)) (map f)

Tactic:
RingHom.ext fun p ↦ map_rename f g p

Premises used: MvPolynomial.map_rename, RingHom.ext
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
inst : CommSemiring R
f : σ → τ
g : τ → α
p : MvPolynomial σ R
simp_rw :
  Eq (α := MvPolynomial α R)
    ((eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g) : (a : MvPolynomial τ R) → MvPolynomial α R)
        (eval₂ C (X ∘ f) p) :
      MvPolynomial α R)
    ((eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g ∘ f) : (a : MvPolynomial σ R) → MvPolynomial α R) p :
      MvPolynomial α R)
⊢ Eq (α := MvPolynomial α R)
    ((rename g : (a : MvPolynomial τ R) → MvPolynomial α R)
        ((aeval (X ∘ f) : (a : MvPolynomial σ R) → MvPolynomial τ R) p) :
      MvPolynomial α R)
    ((rename (g ∘ f) : (a : MvPolynomial σ R) → MvPolynomial α R) p : MvPolynomial α R)

Tactic:
simp_rw [aeval_def, algebraMap_eq, rename, aeval_eq_eval₂Hom]

Premises used: MvPolynomial.aeval_def, MvPolynomial.rename, MvPolynomial.algebraMap_eq, MvPolynomial.aeval_eq_eval₂Hom
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
inst : CommSemiring R
f : σ → τ
g : τ → α
p : MvPolynomial σ R
rw :
  Eq (α := MvPolynomial α R)
    (eval₂ (RingHom.comp (eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g)) C)
      (comp (β := MvPolynomial τ R)
        (⇑(eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g)) : (a : MvPolynomial τ R) → MvPolynomial α R) (X ∘ f))
      p)
    ((eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g ∘ f) : (a : MvPolynomial σ R) → MvPolynomial α R) p)
⊢ Eq (α := MvPolynomial α R)
    ((eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g) : (a : MvPolynomial τ R) → MvPolynomial α R)
        (eval₂ C (X ∘ f) p) :
      MvPolynomial α R)
    ((eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g ∘ f) : (a : MvPolynomial σ R) → MvPolynomial α R) p :
      MvPolynomial α R)

Tactic:
rw [eval₂_comp_left (eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g)) C (X ∘ f) p]

Premises used: Algebra.algebraMap, MvPolynomial.X, Function.comp, MvPolynomial.eval₂Hom, MvPolynomial, MvPolynomial.eval₂_comp_left, MvPolynomial.C
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
inst : CommSemiring R
f : σ → τ
g : τ → α
p : MvPolynomial σ R
simp :
  Eq (α := MvPolynomial α R)
    (eval₂ (RingHom.comp (β := MvPolynomial τ R) (eval₂Hom (algebraMap R (MvPolynomial α R)) fun (x : τ) ↦ X (g x)) C)
        (fun (x : σ) ↦ X (g (f x))) p :
      MvPolynomial α R)
    ((eval₂Hom (algebraMap R (MvPolynomial α R)) fun (x : σ) ↦ X (g (f x)) : (a : MvPolynomial σ R) → MvPolynomial α R)
        p :
      MvPolynomial α R)
⊢ Eq (α := MvPolynomial α R)
    (eval₂ (RingHom.comp (eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g)) C)
      (comp (β := MvPolynomial τ R)
        (⇑(eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g)) : (a : MvPolynomial τ R) → MvPolynomial α R) (X ∘ f))
      p)
    ((eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g ∘ f) : (a : MvPolynomial σ R) → MvPolynomial α R) p)

Tactic:
simp only [comp_def, eval₂Hom_X']

Premises used: MvPolynomial.eval₂Hom_X', Function.comp_def
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
inst : CommSemiring R
f : σ → τ
g : τ → α
p : MvPolynomial σ R
⊢ Eq (α := MvPolynomial α R)
    (eval₂ (RingHom.comp (β := MvPolynomial τ R) (eval₂Hom (algebraMap R (MvPolynomial α R)) fun (x : τ) ↦ X (g x)) C)
        (fun (x : σ) ↦ X (g (f x))) p :
      MvPolynomial α R)
    ((eval₂Hom (algebraMap R (MvPolynomial α R)) fun (x : σ) ↦ X (g (f x)) : (a : MvPolynomial σ R) → MvPolynomial α R)
        p :
      MvPolynomial α R)

Tactic:
eval₂Hom_congr ?_ rfl rfl

Premises used: Multiset.sum, Multiset.foldr, MvPolynomial.eval₂Hom_congr, Finsupp.sum, MvPolynomial.eval₂, Finset.sum, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
inst : CommSemiring R
f : σ → τ
g : τ → α
p : MvPolynomial σ R
refine :
  Eq (α := R →+* MvPolynomial α R)
    (RingHom.comp (β := MvPolynomial τ R) (eval₂Hom (algebraMap R (MvPolynomial α R)) fun (x : τ) ↦ X (g x)) C)
    (algebraMap R (MvPolynomial α R))
⊢ Eq (α := MvPolynomial α R)
    (eval₂ (RingHom.comp (β := MvPolynomial τ R) (eval₂Hom (algebraMap R (MvPolynomial α R)) fun (x : τ) ↦ X (g x)) C)
        (fun (x : σ) ↦ X (g (f x))) p :
      MvPolynomial α R)
    ((eval₂Hom (algebraMap R (MvPolynomial α R)) fun (x : σ) ↦ X (g (f x)) : (a : MvPolynomial σ R) → MvPolynomial α R)
        p :
      MvPolynomial α R)

Tactic:
refine eval₂Hom_congr ?_ rfl rfl

Premises used: MvPolynomial.eval₂Hom_congr, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
inst : CommSemiring R
f : σ → τ
g : τ → α
p : MvPolynomial σ R
a :
  ∀ (x : R),
    Eq (α := MvPolynomial α R)
      ((RingHom.comp (β := MvPolynomial τ R) (eval₂Hom (algebraMap R (MvPolynomial α R)) fun (x : τ) ↦ X (g x)) C :
            (a : R) → MvPolynomial α R)
          x :
        MvPolynomial α R)
      ((algebraMap R (MvPolynomial α R) : (a : R) → MvPolynomial α R) x : MvPolynomial α R)
⊢ Eq (α := R →+* MvPolynomial α R)
    (RingHom.comp (β := MvPolynomial τ R) (eval₂Hom (algebraMap R (MvPolynomial α R)) fun (x : τ) ↦ X (g x)) C)
    (algebraMap R (MvPolynomial α R))

Tactic:
ext1
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
inst : CommSemiring R
f : σ → τ
g : τ → α
p : MvPolynomial σ R
x : R
⊢ Eq (α := MvPolynomial α R)
    ((RingHom.comp (β := MvPolynomial τ R) (eval₂Hom (algebraMap R (MvPolynomial α R)) fun (x : τ) ↦ X (g x)) C :
          (a : R) → MvPolynomial α R)
        x :
      MvPolynomial α R)
    ((algebraMap R (MvPolynomial α R) : (a : R) → MvPolynomial α R) x : MvPolynomial α R)

Tactic:
simp only [comp_apply, RingHom.coe_comp, eval₂Hom_C]

Premises used: RingHom.coe_comp, Function.comp_apply, MvPolynomial.eval₂Hom_C
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
inst : CommSemiring R
f : σ → τ
g : τ → α
⊢ Eq (α := MvPolynomial σ R →ₐ[R] MvPolynomial α R) (AlgHom.comp (rename g) (rename f)) (rename (g ∘ f))

Tactic:
AlgHom.ext fun p ↦ rename_rename f g p

Premises used: MvPolynomial.rename_rename, AlgHom.ext
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
⊢ Eq (α := MvPolynomial σ R →ₐ[R] MvPolynomial σ R) (rename id) (AlgHom.id R (MvPolynomial σ R))

Tactic:
AlgHom.ext fun p ↦ eval₂_eta p

Premises used: AlgHom.ext, MvPolynomial.eval₂_eta
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
p : MvPolynomial σ R
⊢ (rename id : (a : MvPolynomial σ R) → MvPolynomial σ R) p = p

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
d : σ →₀ ℕ
r : R
rw :
  HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R) ((C : (a : R) → MvPolynomial τ R) r : MvPolynomial τ R)
      (d.prod fun (i : σ) (k : ℕ) ↦ HPow.hPow (α := MvPolynomial τ R) ((X ∘ f) i) k : MvPolynomial τ R) =
    HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R) ((C : (a : R) → MvPolynomial τ R) r : MvPolynomial τ R)
      (d.prod fun (a : σ) (m : ℕ) ↦ HPow.hPow (α := MvPolynomial τ R) (X (f a)) m : MvPolynomial τ R)
h_zero : ∀ (b : τ), HPow.hPow (α := MvPolynomial τ R) (β := ℕ) (X b) 0 = 1
h_add :
  ∀ (b : τ) (m₁ m₂ : ℕ),
    HPow.hPow (α := MvPolynomial τ R) (X b) (m₁ + m₂) =
      HPow.hPow (α := MvPolynomial τ R) (X b) m₁ * HPow.hPow (α := MvPolynomial τ R) (X b) m₂
⊢ Eq (α := MvPolynomial τ R)
    ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) ((monomial d : (a : R) → MvPolynomial σ R) r) :
      MvPolynomial τ R)
    ((monomial (Finsupp.mapDomain f d) : (a : R) → MvPolynomial τ R) r : MvPolynomial τ R)

Tactic:
rw [rename, aeval_monomial, monomial_eq (s := Finsupp.mapDomain f d),
    Finsupp.prod_mapDomain_index, algebraMap_eq]

Premises used: MvPolynomial.rename, Finsupp.prod_mapDomain_index, MvPolynomial.algebraMap_eq, MvPolynomial.monomial_eq, MvPolynomial.aeval_monomial
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
d : σ →₀ ℕ
r : R
⊢ HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R) ((C : (a : R) → MvPolynomial τ R) r : MvPolynomial τ R)
      (d.prod fun (i : σ) (k : ℕ) ↦ HPow.hPow (α := MvPolynomial τ R) ((X ∘ f) i) k : MvPolynomial τ R) =
    HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R) ((C : (a : R) → MvPolynomial τ R) r : MvPolynomial τ R)
      (d.prod fun (a : σ) (m : ℕ) ↦ HPow.hPow (α := MvPolynomial τ R) (X (f a)) m : MvPolynomial τ R)

Tactic:
simp_rw [Function.comp_apply]

Premises used: Function.comp_apply
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
d : σ →₀ ℕ
r : R
⊢ ∀ (b : τ), HPow.hPow (α := MvPolynomial τ R) (β := ℕ) (X b) 0 = 1

Tactic:
fun n => pow_zero _

Premises used: MvPolynomial.X, pow_zero
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
d : σ →₀ ℕ
r : R
⊢ ∀ (b : τ), HPow.hPow (α := MvPolynomial τ R) (β := ℕ) (X b) 0 = 1

Tactic:
exact fun n => pow_zero _

Premises used: pow_zero
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
d : σ →₀ ℕ
r : R
⊢ ∀ (b : τ) (m₁ m₂ : ℕ),
    HPow.hPow (α := MvPolynomial τ R) (X b) (m₁ + m₂) =
      HPow.hPow (α := MvPolynomial τ R) (X b) m₁ * HPow.hPow (α := MvPolynomial τ R) (X b) m₂

Tactic:
fun n i₁ i₂ => pow_add _ _ _

Premises used: MvPolynomial.X, pow_add
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
d : σ →₀ ℕ
r : R
⊢ ∀ (b : τ) (m₁ m₂ : ℕ),
    HPow.hPow (α := MvPolynomial τ R) (X b) (m₁ + m₂) =
      HPow.hPow (α := MvPolynomial τ R) (X b) m₁ * HPow.hPow (α := MvPolynomial τ R) (X b) m₂

Tactic:
exact fun n i₁ i₂ => pow_add _ _ _

Premises used: pow_add
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
⊢ Eq (α := (a : MvPolynomial σ R) → MvPolynomial τ R) (⇑(rename f) : (a : MvPolynomial σ R) → MvPolynomial τ R)
    (Finsupp.mapDomain (Finsupp.mapDomain f))

Tactic:
have :
    (rename f : MvPolynomial σ R → MvPolynomial τ R) = Finsupp.mapDomain (Finsupp.mapDomain f) :=
    funext (rename_eq f)
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
this :
  Eq (α := (a : MvPolynomial σ R) → MvPolynomial τ R) (⇑(rename f) : (a : MvPolynomial σ R) → MvPolynomial τ R)
    (Finsupp.mapDomain (Finsupp.mapDomain f))
rw : Injective (α := MvPolynomial σ R) (Finsupp.mapDomain (Finsupp.mapDomain f))
⊢ Injective (α := MvPolynomial σ R) (β := MvPolynomial τ R) (⇑(rename f) : (a : MvPolynomial σ R) → MvPolynomial τ R)

Tactic:
rw [this]
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
this :
  Eq (α := (a : MvPolynomial σ R) → MvPolynomial τ R) (⇑(rename f) : (a : MvPolynomial σ R) → MvPolynomial τ R)
    (Finsupp.mapDomain (Finsupp.mapDomain f))
⊢ Injective (α := MvPolynomial σ R) (Finsupp.mapDomain (Finsupp.mapDomain f))

Tactic:
Finsupp.mapDomain_injective (Finsupp.mapDomain_injective hf)

Premises used: AddMonoidAlgebra, Finsupp.mapDomain_injective
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
this :
  Eq (α := (a : MvPolynomial σ R) → MvPolynomial τ R) (⇑(rename f) : (a : MvPolynomial σ R) → MvPolynomial τ R)
    (Finsupp.mapDomain (Finsupp.mapDomain f))
⊢ Injective (α := MvPolynomial σ R) (Finsupp.mapDomain (Finsupp.mapDomain f))

Tactic:
exact Finsupp.mapDomain_injective (Finsupp.mapDomain_injective hf)

Premises used: Finsupp.mapDomain_injective