awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
p : MvPolynomial τ R
s : σ →₀ ℕ
u : τ →₀ ℕ
r : R
monomial :
  Eq.{u_4 + 1} (α := R)
    (coeff s
      (if (↑u.support : Set τ) ⊆ range f then
        (MvPolynomial.monomial (Finsupp.comapDomain f u ⋯) : (a : R) → MvPolynomial σ R) r
      else 0))
    (coeff (Finsupp.mapDomain f s) ((MvPolynomial.monomial u : (a : R) → MvPolynomial τ R) r))
⊢ Eq.{u_4 + 1} (α := R)
    (coeff s
      ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R)
        ((MvPolynomial.monomial u : (a : R) → MvPolynomial τ R) r)))
    (coeff (Finsupp.mapDomain f s) ((MvPolynomial.monomial u : (a : R) → MvPolynomial τ R) r))

Tactic:
rw [killCompl_monomial]

Premises used: MvPolynomial.killCompl_monomial
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
p : MvPolynomial τ R
s : σ →₀ ℕ
u : τ →₀ ℕ
r : R
pos :
  ∀ (h : (↑u.support : Set τ) ⊆ range f),
    Eq.{u_4 + 1} (α := R) (coeff s ((monomial (Finsupp.comapDomain f u ⋯) : (a : R) → MvPolynomial σ R) r))
      (coeff (Finsupp.mapDomain f s) ((monomial u : (a : R) → MvPolynomial τ R) r))
neg :
  ∀ (h : ¬(↑u.support : Set τ) ⊆ range f),
    Eq.{u_4 + 1} (α := R) (coeff s 0) (coeff (Finsupp.mapDomain f s) ((monomial u : (a : R) → MvPolynomial τ R) r))
⊢ Eq.{u_4 + 1} (α := R)
    (coeff s
      (if (↑u.support : Set τ) ⊆ range f then (monomial (Finsupp.comapDomain f u ⋯) : (a : R) → MvPolynomial σ R) r
      else 0))
    (coeff (Finsupp.mapDomain f s) ((monomial u : (a : R) → MvPolynomial τ R) r))

Tactic:
split_ifs with h
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
p : MvPolynomial τ R
s : σ →₀ ℕ
u : τ →₀ ℕ
r : R
h : (↑u.support : Set τ) ⊆ range f
⊢ Eq.{u_4 + 1} (α := R) (coeff s ((monomial (Finsupp.comapDomain f u ⋯) : (a : R) → MvPolynomial σ R) r))
    (coeff (Finsupp.mapDomain f s) ((monomial u : (a : R) → MvPolynomial τ R) r))

Tactic:
simp [← (Finsupp.mapDomain_injective hf).eq_iff, u.mapDomain_comapDomain _ hf h]

Premises used: Function.Injective.eq_iff, Finsupp.mapDomain_comapDomain, 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
p : MvPolynomial τ R
s : σ →₀ ℕ
u : τ →₀ ℕ
r : R
h : ¬(↑u.support : Set τ) ⊆ range f
neg : u = Finsupp.mapDomain f s → 0 = r
⊢ Eq.{u_4 + 1} (α := R) (coeff s 0) (coeff (Finsupp.mapDomain f s) ((monomial u : (a : R) → MvPolynomial τ R) r))

Tactic:
simp only [coeff_zero, coeff_monomial, right_eq_ite_iff]

Premises used: MvPolynomial.coeff_zero, MvPolynomial.coeff_monomial, right_eq_ite_iff
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
p : MvPolynomial τ R
s : σ →₀ ℕ
u : τ →₀ ℕ
r : R
h : ¬(↑u.support : Set τ) ⊆ range f
neg : u = Finsupp.mapDomain f s → 0 = r
⊢ Eq.{u_4 + 1} (α := R) (coeff s 0) (coeff (Finsupp.mapDomain f s) ((monomial u : (a : R) → MvPolynomial τ R) r))

Tactic:
simp? says simp only [coeff_zero, coeff_monomial, right_eq_ite_iff]

Premises used: MvPolynomial.coeff_zero, MvPolynomial.coeff_monomial, right_eq_ite_iff
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
p : MvPolynomial τ R
s : σ →₀ ℕ
r : R
h : ¬(↑(Finsupp.mapDomain f s).support : Set τ) ⊆ range f
neg : ∀ (h : 0 ≠ r), (↑(Finsupp.mapDomain f s).support : Set τ) ⊆ range f
⊢ 0 = r

Tactic:
contrapose! h
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
p : MvPolynomial τ R
s : σ →₀ ℕ
r : R
h : 0 ≠ r
neg : (↑(Finset.image f s.support) : Set τ) ⊆ range f
⊢ (↑(Finsupp.mapDomain f s).support : Set τ) ⊆ range f

Tactic:
apply subset_trans <| SetLike.coe_subset_coe.mpr <| Finsupp.mapDomain_support

Premises used: Iff.mpr, Finsupp.mapDomain_support, subset_trans, SetLike.coe_subset_coe
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
p : MvPolynomial τ R
s : σ →₀ ℕ
r : R
h : 0 ≠ r
⊢ (↑(Finset.image f s.support) : Set τ) ⊆ range f

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
p : MvPolynomial τ R
s : σ →₀ ℕ
⊢ ∀ (p q : MvPolynomial τ R),
    coeff s ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R) p) = coeff (Finsupp.mapDomain f s) p →
      coeff s ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R) q) = coeff (Finsupp.mapDomain f s) q →
        coeff s ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R) (p + q)) =
          coeff (Finsupp.mapDomain f s) (p + q)

Tactic:
simp_intro ..
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
p : MvPolynomial τ R
s : σ →₀ ℕ
monomial :
  ∀ (u : τ →₀ ℕ) (a : R),
    Eq.{u_4 + 1} (α := R)
      (coeff s
        ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R)
          ((MvPolynomial.monomial u : (a : R) → MvPolynomial τ R) a)))
      (coeff (Finsupp.mapDomain f s) ((MvPolynomial.monomial u : (a : R) → MvPolynomial τ R) a))
add add₁ :
  ∀ (p q : MvPolynomial τ R),
    coeff s ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R) p) = coeff (Finsupp.mapDomain f s) p →
      coeff s ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R) q) = coeff (Finsupp.mapDomain f s) q →
        coeff s ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R) (p + q)) =
          coeff (Finsupp.mapDomain f s) (p + q)
⊢ coeff s ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R) p) = coeff (Finsupp.mapDomain f s) p

Tactic:
classical
  apply p.induction_on' (P := fun p ↦ (p.killCompl hf).coeff s = p.coeff (s.mapDomain f))
  · intro u r
    rw [killCompl_monomial]
    split_ifs with h
    · simp [← (Finsupp.mapDomain_injective hf).eq_iff, u.mapDomain_comapDomain _ hf h]
    · simp? says simp only [coeff_zero, coeff_monomial, right_eq_ite_iff]
      intro rfl
      contrapose! h
      apply subset_trans <| SetLike.coe_subset_coe.mpr <| Finsupp.mapDomain_support
      simp
  · simp_intro ..

Premises used: Iff.mpr, Finsupp.mapDomain_support, subset_trans, Function.Injective.eq_iff, MvPolynomial.induction_on', SetLike.coe_subset_coe, MvPolynomial.coeff_zero, MvPolynomial.coeff_monomial, right_eq_ite_iff, MvPolynomial.killCompl_monomial, Finsupp.mapDomain_injective, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
p : MvPolynomial τ R
h :
  ∀ (x : σ →₀ ℕ),
    Membership.mem (γ := Finset (σ →₀ ℕ))
        (support.{u_4, u_1} (R := R) ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R) p)) x ↔
      x ∈ p.support.preimage (Finsupp.mapDomain f) ⋯
⊢ support.{u_4, u_1} (R := R) ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R) p) =
    p.support.preimage (Finsupp.mapDomain f) ⋯

Tactic:
ext x
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
p : MvPolynomial τ R
x : σ →₀ ℕ
⊢ Membership.mem (γ := Finset (σ →₀ ℕ))
      (support.{u_4, u_1} (R := R) ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R) p)) x ↔
    x ∈ p.support.preimage (Finsupp.mapDomain f) ⋯

Tactic:
simp [coeff_killCompl]

Premises used: MvPolynomial.coeff_killCompl
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
f : σ ≃ τ
p : MvPolynomial σ R
rw :
  (rename (comp.{u_1 + 1, u_2 + 1, u_1 + 1} (β := τ) (⇑f.symm : (a : τ) → σ) (⇑f : (a : σ) → τ)) :
        (a : MvPolynomial σ R) → MvPolynomial σ R)
      p =
    p
rw₁ : (rename id : (a : MvPolynomial σ R) → MvPolynomial σ R) p = p
rw₂ rw₃ : p = p
⊢ (rename (⇑f.symm : (a : τ) → σ) : (a : MvPolynomial τ R) → MvPolynomial σ R)
      ((rename (⇑f : (a : σ) → τ) : (a : MvPolynomial σ R) → MvPolynomial τ R) p) =
    p

Tactic:
rw [rename_rename, f.symm_comp_self, rename_id_apply]

Premises used: MvPolynomial.rename_rename, Equiv.symm_comp_self, MvPolynomial.rename_id_apply
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
f : σ ≃ τ
p : MvPolynomial τ R
rw :
  (rename (comp.{u_2 + 1, u_1 + 1, u_2 + 1} (β := σ) (⇑f : (a : σ) → τ) (⇑f.symm : (a : τ) → σ)) :
        (a : MvPolynomial τ R) → MvPolynomial τ R)
      p =
    p
rw₁ : (rename id : (a : MvPolynomial τ R) → MvPolynomial τ R) p = p
rw₂ rw₃ : p = p
⊢ (rename (⇑f : (a : σ) → τ) : (a : MvPolynomial σ R) → MvPolynomial τ R)
      ((rename (⇑f.symm : (a : τ) → σ) : (a : MvPolynomial τ R) → MvPolynomial σ R) p) =
    p

Tactic:
rw [rename_rename, f.self_comp_symm, rename_id_apply]

Premises used: MvPolynomial.rename_rename, MvPolynomial.rename_id_apply, Equiv.self_comp_symm
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
⊢ ∀ (a : MvPolynomial σ R),
    Eq (α := MvPolynomial σ R)
      ((renameEquiv R (Equiv.refl σ) : (a : MvPolynomial σ R) → MvPolynomial σ R) a : MvPolynomial σ R)
      ((AlgEquiv.refl : (a : MvPolynomial σ R) → MvPolynomial σ R) a : MvPolynomial σ R)

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ ≃ τ
⊢ Eq (α := MvPolynomial τ R ≃ₐ[R] MvPolynomial σ R) (AlgEquiv.symm (renameEquiv R f)) (renameEquiv R f.symm)

Tactic:
rfl

Premises used: AlgEquiv.symm, Equiv.symm, MvPolynomial.renameEquiv, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
inst : CommSemiring R
e : σ ≃ τ
f : τ ≃ α
⊢ Eq (α := MvPolynomial σ R ≃ₐ[R] MvPolynomial α R) (AlgEquiv.trans (renameEquiv R e) (renameEquiv R f))
    (renameEquiv R (e.trans f))

Tactic:
AlgEquiv.ext (rename_rename e f)

Premises used: MvPolynomial.rename_rename, AlgEquiv.ext, DFunLike.coe
-- 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
k : σ → τ
g : τ → S
p : MvPolynomial σ R
C :
  ∀ (a : R),
    eval₂ f g
        ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)) =
      eval₂ f (g ∘ k) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)
add :
  ∀ (p q : MvPolynomial σ R),
    eval₂ f g ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) p) = eval₂ f (g ∘ k) p →
      eval₂ f g ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) q) = eval₂ f (g ∘ k) q →
        eval₂ f g ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) (p + q)) = eval₂ f (g ∘ k) (p + q)
mul_X :
  ∀ (p : MvPolynomial σ R) (n : σ),
    eval₂ f g ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) p) = eval₂ f (g ∘ k) p →
      eval₂ f g ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) (p * X n)) = eval₂ f (g ∘ k) (p * X n)
⊢ eval₂ f g ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) p) = eval₂ f (g ∘ k) p

Tactic:
apply MvPolynomial.induction_on p

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
k : σ → τ
g : τ → S
p : MvPolynomial σ R
a : R
⊢ eval₂ f g ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) ((C : (a : R) → MvPolynomial σ R) a)) =
    eval₂ f (g ∘ k) ((C : (a : R) → MvPolynomial σ R) a)

Tactic:
simp [*]
-- 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
k : σ → τ
g : τ → S
p p_1 q : MvPolynomial σ R
h : eval₂ f g ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) p_1) = eval₂ f (g ∘ k) p_1
h_1 : eval₂ f g ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) q) = eval₂ f (g ∘ k) q
⊢ eval₂ f g ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) (p_1 + q)) = eval₂ f (g ∘ k) (p_1 + q)

Tactic:
simp [*]
-- 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
k : σ → τ
g : τ → S
p p_1 : MvPolynomial σ R
n : σ
h : eval₂ f g ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) p_1) = eval₂ f (g ∘ k) p_1
⊢ eval₂ f g ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) (p_1 * X n)) = eval₂ f (g ∘ k) (p_1 * X n)

Tactic:
simp [*]
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
k : σ → τ
g : τ → R
p : MvPolynomial σ R
⊢ Eq.{u_4 + 1} (α := R)
    ((eval g : (a : MvPolynomial τ R) → R)
        ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) p : MvPolynomial τ R) :
      R)
    ((eval (g ∘ k) : (a : MvPolynomial σ R) → R) p : R)

Tactic:
eval₂_rename _ _ _ _

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, MvPolynomial.eval₂, MvPolynomial.eval₂_rename, Finset.sum
-- 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
k : σ → τ
g : τ → S
p : MvPolynomial σ R
⊢ Eq.{u_5 + 1} (α := S)
    ((eval₂Hom f g : (a : MvPolynomial τ R) → S)
        ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) p : MvPolynomial τ R) :
      S)
    ((eval₂Hom f (g ∘ k) : (a : MvPolynomial σ R) → S) p : S)

Tactic:
eval₂_rename _ _ _ _

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, MvPolynomial.eval₂, MvPolynomial.eval₂_rename, Finset.sum
-- 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
k : σ → τ
g : τ → S
p : MvPolynomial σ R
inst_2 : Algebra R S
⊢ Eq.{u_5 + 1} (α := S)
    ((aeval g : (a : MvPolynomial τ R) → S)
        ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) p : MvPolynomial τ R) :
      S)
    ((aeval (g ∘ k) : (a : MvPolynomial σ R) → S) p : S)

Tactic:
eval₂Hom_rename _ _ _ _

Premises used: MvPolynomial.eval₂Hom_rename
-- 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
k : σ → τ
g : τ → S
inst_2 : Algebra R S
⊢ Eq (α := MvPolynomial σ R →ₐ[R] S) (AlgHom.comp (aeval g) (rename k)) (aeval (g ∘ k))

Tactic:
AlgHom.ext fun p ↦ aeval_rename k g p

Premises used: AlgHom.ext, MvPolynomial.aeval_rename
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
k : σ → τ
p : MvPolynomial σ R
g : τ → MvPolynomial σ R
C :
  ∀ (a : R),
    Eq (α := MvPolynomial τ R)
      ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R)
          (eval₂ MvPolynomial.C (g ∘ k) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)) :
        MvPolynomial τ R)
      (eval₂ MvPolynomial.C ((⇑(rename k) : (a : MvPolynomial σ R) → MvPolynomial τ R) ∘ g)
          ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)) :
        MvPolynomial τ R)
add :
  ∀ (p q : MvPolynomial σ R),
    Eq (α := MvPolynomial τ R)
        ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) (eval₂ MvPolynomial.C (g ∘ k) p) : MvPolynomial τ R)
        (eval₂ MvPolynomial.C ((⇑(rename k) : (a : MvPolynomial σ R) → MvPolynomial τ R) ∘ g)
            ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) p) :
          MvPolynomial τ R) →
      Eq (α := MvPolynomial τ R)
          ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) (eval₂ MvPolynomial.C (g ∘ k) q) : MvPolynomial τ R)
          (eval₂ MvPolynomial.C ((⇑(rename k) : (a : MvPolynomial σ R) → MvPolynomial τ R) ∘ g)
              ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) q) :
            MvPolynomial τ R) →
        Eq (α := MvPolynomial τ R)
          ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) (eval₂ MvPolynomial.C (g ∘ k) (p + q)) :
            MvPolynomial τ R)
          (eval₂ MvPolynomial.C ((⇑(rename k) : (a : MvPolynomial σ R) → MvPolynomial τ R) ∘ g)
              ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) (p + q)) :
            MvPolynomial τ R)
mul_X :
  ∀ (p : MvPolynomial σ R) (n : σ),
    Eq (α := MvPolynomial τ R)
        ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) (eval₂ MvPolynomial.C (g ∘ k) p) : MvPolynomial τ R)
        (eval₂ MvPolynomial.C ((⇑(rename k) : (a : MvPolynomial σ R) → MvPolynomial τ R) ∘ g)
            ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) p) :
          MvPolynomial τ R) →
      Eq (α := MvPolynomial τ R)
        ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) (eval₂ MvPolynomial.C (g ∘ k) (p * X n)) :
          MvPolynomial τ R)
        (eval₂ MvPolynomial.C ((⇑(rename k) : (a : MvPolynomial σ R) → MvPolynomial τ R) ∘ g)
            ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) (p * X n)) :
          MvPolynomial τ R)
⊢ Eq (α := MvPolynomial τ R)
    ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) (eval₂ MvPolynomial.C (g ∘ k) p) : MvPolynomial τ R)
    (eval₂ MvPolynomial.C ((⇑(rename k) : (a : MvPolynomial σ R) → MvPolynomial τ R) ∘ g)
        ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) p) :
      MvPolynomial τ R)

Tactic:
apply MvPolynomial.induction_on p

Premises used: MvPolynomial.induction_on
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
k : σ → τ
p : MvPolynomial σ R
g : τ → MvPolynomial σ R
a : R
⊢ Eq (α := MvPolynomial τ R)
    ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) (eval₂ C (g ∘ k) ((C : (a : R) → MvPolynomial σ R) a)) :
      MvPolynomial τ R)
    (eval₂ C ((⇑(rename k) : (a : MvPolynomial σ R) → MvPolynomial τ R) ∘ g)
        ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) ((C : (a : R) → MvPolynomial σ R) a)) :
      MvPolynomial τ R)

Tactic:
simp [*]
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
k : σ → τ
p : MvPolynomial σ R
g : τ → MvPolynomial σ R
p_1 q : MvPolynomial σ R
h :
  Eq (α := MvPolynomial τ R)
    ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) (eval₂ C (g ∘ k) p_1) : MvPolynomial τ R)
    (eval₂ C ((⇑(rename k) : (a : MvPolynomial σ R) → MvPolynomial τ R) ∘ g)
        ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) p_1) :
      MvPolynomial τ R)
h_1 :
  Eq (α := MvPolynomial τ R)
    ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) (eval₂ C (g ∘ k) q) : MvPolynomial τ R)
    (eval₂ C ((⇑(rename k) : (a : MvPolynomial σ R) → MvPolynomial τ R) ∘ g)
        ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) q) :
      MvPolynomial τ R)
⊢ Eq (α := MvPolynomial τ R)
    ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) (eval₂ C (g ∘ k) (p_1 + q)) : MvPolynomial τ R)
    (eval₂ C ((⇑(rename k) : (a : MvPolynomial σ R) → MvPolynomial τ R) ∘ g)
        ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) (p_1 + q)) :
      MvPolynomial τ R)

Tactic:
simp [*]
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
k : σ → τ
p : MvPolynomial σ R
g : τ → MvPolynomial σ R
p_1 : MvPolynomial σ R
n : σ
h :
  Eq (α := MvPolynomial τ R)
    ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) (eval₂ C (g ∘ k) p_1) : MvPolynomial τ R)
    (eval₂ C ((⇑(rename k) : (a : MvPolynomial σ R) → MvPolynomial τ R) ∘ g)
        ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) p_1) :
      MvPolynomial τ R)
⊢ Eq (α := MvPolynomial τ R)
    ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) (eval₂ C (g ∘ k) (p_1 * X n)) : MvPolynomial τ R)
    (eval₂ C ((⇑(rename k) : (a : MvPolynomial σ R) → MvPolynomial τ R) ∘ g)
        ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) (p_1 * X n)) :
      MvPolynomial τ R)

Tactic:
simp [*]
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
p : MvPolynomial σ R
j : τ
g : σ → MvPolynomial σ R
C :
  ∀ (a : R),
    Eq (α := MvPolynomial (τ × σ) R)
      ((rename (Prod.mk j) : (a : MvPolynomial σ R) → MvPolynomial (τ × σ) R)
          (eval₂ MvPolynomial.C g ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)) :
        MvPolynomial (τ × σ) R)
      (eval₂ MvPolynomial.C (fun (x : σ) ↦ (rename (Prod.mk j) : (a : MvPolynomial σ R) → MvPolynomial (τ × σ) R) (g x))
          ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a) :
        MvPolynomial (τ × σ) R)
add :
  ∀ (p q : MvPolynomial σ R),
    Eq (α := MvPolynomial (τ × σ) R)
        ((rename (Prod.mk j) : (a : MvPolynomial σ R) → MvPolynomial (τ × σ) R) (eval₂ MvPolynomial.C g p) :
          MvPolynomial (τ × σ) R)
        (eval₂ MvPolynomial.C
            (fun (x : σ) ↦ (rename (Prod.mk j) : (a : MvPolynomial σ R) → MvPolynomial (τ × σ) R) (g x)) p :
          MvPolynomial (τ × σ) R) →
      Eq (α := MvPolynomial (τ × σ) R)
          ((rename (Prod.mk j) : (a : MvPolynomial σ R) → MvPolynomial (τ × σ) R) (eval₂ MvPolynomial.C g q) :
            MvPolynomial (τ × σ) R)
          (eval₂ MvPolynomial.C
              (fun (x : σ) ↦ (rename (Prod.mk j) : (a : MvPolynomial σ R) → MvPolynomial (τ × σ) R) (g x)) q :
            MvPolynomial (τ × σ) R) →
        Eq (α := MvPolynomial (τ × σ) R)
          ((rename (Prod.mk j) : (a : MvPolynomial σ R) → MvPolynomial (τ × σ) R) (eval₂ MvPolynomial.C g (p + q)) :
            MvPolynomial (τ × σ) R)
          (eval₂ MvPolynomial.C
              (fun (x : σ) ↦ (rename (Prod.mk j) : (a : MvPolynomial σ R) → MvPolynomial (τ × σ) R) (g x)) (p + q) :
            MvPolynomial (τ × σ) R)
mul_X :
  ∀ (p : MvPolynomial σ R) (n : σ),
    Eq (α := MvPolynomial (τ × σ) R)
        ((rename (Prod.mk j) : (a : MvPolynomial σ R) → MvPolynomial (τ × σ) R) (eval₂ MvPolynomial.C g p) :
          MvPolynomial (τ × σ) R)
        (eval₂ MvPolynomial.C
            (fun (x : σ) ↦ (rename (Prod.mk j) : (a : MvPolynomial σ R) → MvPolynomial (τ × σ) R) (g x)) p :
          MvPolynomial (τ × σ) R) →
      Eq (α := MvPolynomial (τ × σ) R)
        ((rename (Prod.mk j) : (a : MvPolynomial σ R) → MvPolynomial (τ × σ) R) (eval₂ MvPolynomial.C g (p * X n)) :
          MvPolynomial (τ × σ) R)
        (eval₂ MvPolynomial.C
            (fun (x : σ) ↦ (rename (Prod.mk j) : (a : MvPolynomial σ R) → MvPolynomial (τ × σ) R) (g x)) (p * X n) :
          MvPolynomial (τ × σ) R)
⊢ Eq (α := MvPolynomial (τ × σ) R)
    ((rename (Prod.mk j) : (a : MvPolynomial σ R) → MvPolynomial (τ × σ) R) (eval₂ MvPolynomial.C g p) :
      MvPolynomial (τ × σ) R)
    (eval₂ MvPolynomial.C (fun (x : σ) ↦ (rename (Prod.mk j) : (a : MvPolynomial σ R) → MvPolynomial (τ × σ) R) (g x))
        p :
      MvPolynomial (τ × σ) R)

Tactic:
apply MvPolynomial.induction_on p

Premises used: MvPolynomial.induction_on
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
p : MvPolynomial σ R
j : τ
g : σ → MvPolynomial σ R
a : R
⊢ Eq (α := MvPolynomial (τ × σ) R)
    ((rename (Prod.mk j) : (a : MvPolynomial σ R) → MvPolynomial (τ × σ) R)
        (eval₂ C g ((C : (a : R) → MvPolynomial σ R) a)) :
      MvPolynomial (τ × σ) R)
    (eval₂ C (fun (x : σ) ↦ (rename (Prod.mk j) : (a : MvPolynomial σ R) → MvPolynomial (τ × σ) R) (g x))
        ((C : (a : R) → MvPolynomial σ R) a) :
      MvPolynomial (τ × σ) R)

Tactic:
simp [*]