awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
A₁ : Type u_2
A₂ : Type u_3
inst_1 : CommSemiring A₁
inst_2 : CommSemiring A₂
inst_3 : Algebra R A₁
inst_4 : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
x : MvPolynomial σ A₁
⊢ Eq (α := MvPolynomial σ A₂) ((mapAlgEquiv σ e : (a : MvPolynomial σ A₁) → MvPolynomial σ A₂) x : MvPolynomial σ A₂)
    ((map (↑e : A₁ →+* A₂) : (a : MvPolynomial σ A₁) → MvPolynomial σ A₂) x : MvPolynomial σ A₂)

Tactic:
rfl

Premises used: Finsupp.onFinset, AddMonoidAlgebra.ofCoeff, AddMonoidAlgebra.map, Finsupp.mapRange, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
A₁ : Type u_2
inst_1 : CommSemiring A₁
inst_2 : Algebra R A₁
⊢ Eq (α := MvPolynomial σ A₁ ≃ₐ[R] MvPolynomial σ A₁) (mapAlgEquiv σ AlgEquiv.refl) AlgEquiv.refl

Tactic:
AlgEquiv.ext map_id

Premises used: AlgEquiv.ext, MvPolynomial.map_id
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
A₁ : Type u_2
A₂ : Type u_3
inst_1 : CommSemiring A₁
inst_2 : CommSemiring A₂
inst_3 : Algebra R A₁
inst_4 : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
⊢ (mapAlgEquiv σ e).symm = mapAlgEquiv σ e.symm

Tactic:
rfl

Premises used: AlgEquiv.symm, MvPolynomial.mapAlgEquiv, Finsupp.onFinset, AddMonoidAlgebra.ofCoeff, AddMonoidAlgebra.mapAlgEquiv, AddMonoidAlgebra.map, Equiv.symm, Finsupp.mapRange, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
A₁ : Type u_2
A₂ : Type u_3
A₃ : Type u_4
inst_1 : CommSemiring A₁
inst_2 : CommSemiring A₂
inst_3 : CommSemiring A₃
inst_4 : Algebra R A₁
inst_5 : Algebra R A₂
inst_6 : Algebra R A₃
e : A₁ ≃ₐ[R] A₂
f : A₂ ≃ₐ[R] A₃
⊢ (mapAlgEquiv σ e).trans (mapAlgEquiv σ f) = mapAlgEquiv σ (e.trans f)

Tactic:
(AddMonoidAlgebra.mapAlgEquiv_trans _ _).symm

Premises used: AddMonoidAlgebra.mapAlgEquiv_trans, MvPolynomial.mapAlgEquiv, Eq.symm
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Unique σ
f : MvPolynomial σ R
φ : R →+* S
a : σ → S
simp : Polynomial.eval₂ φ (a default) (eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) f) = eval₂ φ a f
⊢ Polynomial.eval₂ φ (a default) ((uniqueAlgEquiv R σ : (a : MvPolynomial σ R) → R[X]) f) = eval₂ φ a f

Tactic:
simp only [MvPolynomial.uniqueAlgEquiv_apply]

Premises used: MvPolynomial.uniqueAlgEquiv_apply
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Unique σ
φ : R →+* S
a : σ → S
d : σ →₀ ℕ
r : R
monomial :
  Polynomial.eval₂ φ (a default) ((Polynomial.monomial ((d : (a : σ) → ℕ) default) : (a : R) → R[X]) r) =
    eval₂ φ a ((MvPolynomial.monomial d : (a : R) → MvPolynomial σ R) r)
⊢ Polynomial.eval₂ φ (a default)
      (eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) ((MvPolynomial.monomial d : (a : R) → MvPolynomial σ R) r)) =
    eval₂ φ a ((MvPolynomial.monomial d : (a : R) → MvPolynomial σ R) r)

Tactic:
rw [← MvPolynomial.uniqueAlgEquiv_apply (R := R) (σ := σ), uniqueAlgEquiv_monomial]

Premises used: MvPolynomial.uniqueAlgEquiv_monomial, MvPolynomial.uniqueAlgEquiv_apply
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Unique σ
φ : R →+* S
a : σ → S
d : σ →₀ ℕ
r : R
monomial :
  HMul.hMul (α := S) ((φ : (a : R) → S) r : S) (HPow.hPow (β := ℕ) (a default) ((d : (a : σ) → ℕ) default : ℕ)) =
    HMul.hMul (α := S) (β := S) ((φ : (a : R) → S) r : S) (d.prod fun (n : σ) (e : ℕ) ↦ a n ^ e : S)
⊢ Polynomial.eval₂ φ (a default) ((Polynomial.monomial ((d : (a : σ) → ℕ) default) : (a : R) → R[X]) r) =
    eval₂ φ a ((MvPolynomial.monomial d : (a : R) → MvPolynomial σ R) r)

Tactic:
simp only [Polynomial.eval₂_monomial, eval₂_monomial]

Premises used: Polynomial.eval₂_monomial, MvPolynomial.eval₂_monomial
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Unique σ
φ : R →+* S
a : σ → S
d : σ →₀ ℕ
r : R
monomial :
  HMul.hMul (α := S) ((φ : (a : R) → S) r : S)
      (HPow.hPow (β := ℕ) (a default)
        (((Finsupp.single default ((d : (a : σ) → ℕ) default) : σ →₀ ℕ) : (a : σ) → ℕ) default : ℕ)) =
    HMul.hMul (α := S) ((φ : (a : R) → S) r : S) (HPow.hPow (β := ℕ) (a default) ((d : (a : σ) → ℕ) default : ℕ))
monomial₁ : HPow.hPow (β := ℕ) (a default) 0 = 1
⊢ HMul.hMul (α := S) ((φ : (a : R) → S) r : S) (HPow.hPow (β := ℕ) (a default) ((d : (a : σ) → ℕ) default : ℕ)) =
    HMul.hMul (α := S) (β := S) ((φ : (a : R) → S) r : S) (d.prod fun (n : σ) (e : ℕ) ↦ a n ^ e : S)

Tactic:
rw [Finsupp.unique_single d, Finsupp.prod_single_index]

Premises used: Finsupp.unique_single, Finsupp.prod_single_index
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Unique σ
φ : R →+* S
a : σ → S
d : σ →₀ ℕ
r : R
⊢ HMul.hMul (α := S) ((φ : (a : R) → S) r : S)
      (HPow.hPow (β := ℕ) (a default)
        (((Finsupp.single default ((d : (a : σ) → ℕ) default) : σ →₀ ℕ) : (a : σ) → ℕ) default : ℕ)) =
    HMul.hMul (α := S) ((φ : (a : R) → S) r : S) (HPow.hPow (β := ℕ) (a default) ((d : (a : σ) → ℕ) default : ℕ))

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Unique σ
φ : R →+* S
a : σ → S
d : σ →₀ ℕ
r : R
⊢ HPow.hPow (β := ℕ) (a default) 0 = 1

Tactic:
simp only [pow_zero]

Premises used: pow_zero
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Unique σ
φ : R →+* S
a : σ → S
f g : MvPolynomial σ R
hf : Polynomial.eval₂ φ (a default) (eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) f) = eval₂ φ a f
hg : Polynomial.eval₂ φ (a default) (eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) g) = eval₂ φ a g
⊢ Polynomial.eval₂ φ (a default) (eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) (f + g)) = eval₂ φ a (f + g)

Tactic:
simp only [eval₂_add, Polynomial.eval₂_add, hf, hg]

Premises used: MvPolynomial.eval₂_add, Polynomial.eval₂_add
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Unique σ
f : MvPolynomial σ R
φ : R →+* S
a : σ → S
monomial :
  ∀ (d : σ →₀ ℕ) (r : R),
    Polynomial.eval₂ φ (a default)
        (eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) ((MvPolynomial.monomial d : (a : R) → MvPolynomial σ R) r)) =
      eval₂ φ a ((MvPolynomial.monomial d : (a : R) → MvPolynomial σ R) r)
add :
  ∀ (f g : MvPolynomial σ R)
    (hf : Polynomial.eval₂ φ (a default) (eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) f) = eval₂ φ a f)
    (hg : Polynomial.eval₂ φ (a default) (eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) g) = eval₂ φ a g),
    Polynomial.eval₂ φ (a default) (eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) (f + g)) = eval₂ φ a (f + g)
⊢ Polynomial.eval₂ φ (a default) (eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) f) = eval₂ φ a f

Tactic:
induction f using MvPolynomial.induction_on' with
  | monomial d r =>
    rw [← MvPolynomial.uniqueAlgEquiv_apply (R := R) (σ := σ), uniqueAlgEquiv_monomial]
    simp only [Polynomial.eval₂_monomial, eval₂_monomial]
    rw [Finsupp.unique_single d, Finsupp.prod_single_index]
    · simp
    · simp only [pow_zero]
  | add f g hf hg => simp only [eval₂_add, Polynomial.eval₂_add, hf, hg]

Premises used: Polynomial.eval₂_monomial, MvPolynomial.monomial, MvPolynomial.uniqueAlgEquiv_monomial, MvPolynomial.eval₂_add, pow_zero, MvPolynomial.uniqueAlgEquiv_apply, MvPolynomial.eval₂_monomial, Finsupp.prod_single_index, Polynomial.eval₂_add
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Unique σ
f : R[X]
φ : R →+* S
a : σ → S
rw :
  Polynomial.eval₂ φ (a default)
      ((uniqueAlgEquiv R σ : (a : MvPolynomial σ R) → R[X])
        ((AlgEquiv.symm (uniqueAlgEquiv R σ) : (a : R[X]) → MvPolynomial σ R) f)) =
    Polynomial.eval₂ φ (a default) f
⊢ eval₂ φ a ((AlgEquiv.symm (uniqueAlgEquiv R σ) : (a : R[X]) → MvPolynomial σ R) f) = Polynomial.eval₂ φ (a default) f

Tactic:
rw [(eval₂_uniqueAlgEquiv (R := R) (σ := σ) (f := (MvPolynomial.uniqueAlgEquiv R σ).symm f)
    (φ := φ) (a := a)).symm]

Premises used: MvPolynomial.eval₂_uniqueAlgEquiv, Eq.symm
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Unique σ
f : R[X]
φ : R →+* S
a : σ → S
rw rw₁ : Polynomial.eval₂ φ (a default) f = Polynomial.eval₂ φ (a default) f
⊢ Polynomial.eval₂ φ (a default)
      ((uniqueAlgEquiv R σ : (a : MvPolynomial σ R) → R[X])
        ((AlgEquiv.symm (uniqueAlgEquiv R σ) : (a : R[X]) → MvPolynomial σ R) f)) =
    Polynomial.eval₂ φ (a default) f

Tactic:
rw [AlgEquiv.apply_symm_apply]

Premises used: AlgEquiv.apply_symm_apply
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Unique σ
f : R[X]
φ : R →+* S
a : S
rw rw₁ : Polynomial.eval₂ φ a f = Polynomial.eval₂ φ a f
⊢ eval₂ φ (fun (x : σ) ↦ a) ((AlgEquiv.symm (uniqueAlgEquiv R σ) : (a : R[X]) → MvPolynomial σ R) f) =
    Polynomial.eval₂ φ a f

Tactic:
rw [eval₂_uniqueAlgEquiv_symm]

Premises used: MvPolynomial.eval₂_uniqueAlgEquiv_symm
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Unique σ
f : MvPolynomial σ R
φ : R →+* S
a : S
rw rw₁ :
  Polynomial.eval₂ φ a ((uniqueAlgEquiv R σ : (a : MvPolynomial σ R) → R[X]) f) =
    Polynomial.eval₂ φ a ((uniqueAlgEquiv R σ : (a : MvPolynomial σ R) → R[X]) f)
⊢ Polynomial.eval₂ φ a ((uniqueAlgEquiv R σ : (a : MvPolynomial σ R) → R[X]) f) = eval₂ φ (fun (x : σ) ↦ a) f

Tactic:
rw [← eval₂_uniqueAlgEquiv]

Premises used: MvPolynomial.eval₂_uniqueAlgEquiv
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
f : R[X]
φ : R →+* S
a : Unit → S
⊢ eval₂ φ a ((AlgEquiv.symm (pUnitAlgEquiv R) : (a : R[X]) → MvPolynomial PUnit.{1} R) f) = Polynomial.eval₂ φ (a ()) f

Tactic:
eval₂_uniqueAlgEquiv_symm

Premises used: MvPolynomial.eval₂_uniqueAlgEquiv_symm
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
f : R[X]
φ : R →+* S
a : S
⊢ eval₂ φ (fun (x : PUnit.{1}) ↦ a) ((AlgEquiv.symm (pUnitAlgEquiv R) : (a : R[X]) → MvPolynomial PUnit.{1} R) f) =
    Polynomial.eval₂ φ a f

Tactic:
eval₂_const_uniqueAlgEquiv_symm

Premises used: MvPolynomial.eval₂_const_uniqueAlgEquiv_symm
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
f : MvPolynomial PUnit.{u_4 + 1} R
φ : R →+* S
a : PUnit.{u_4 + 1} → S
⊢ Polynomial.eval₂ φ (a default) ((pUnitAlgEquiv R : (a : MvPolynomial PUnit.{u_4 + 1} R) → R[X]) f) = eval₂ φ a f

Tactic:
eval₂_uniqueAlgEquiv

Premises used: MvPolynomial.eval₂_uniqueAlgEquiv
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
f : MvPolynomial PUnit.{u_4 + 1} R
φ : R →+* S
a : S
⊢ Polynomial.eval₂ φ a ((pUnitAlgEquiv R : (a : MvPolynomial PUnit.{u_4 + 1} R) → R[X]) f) =
    eval₂ φ (fun (x : PUnit.{u_4 + 1}) ↦ a) f

Tactic:
eval₂_const_uniqueAlgEquiv

Premises used: MvPolynomial.eval₂_const_uniqueAlgEquiv
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
inst : CommSemiring R
a : R
⊢ Eq (α := MvPolynomial S₁ (MvPolynomial S₂ R))
    ((sumToIter R S₁ S₂ : (a : MvPolynomial (S₁ ⊕ S₂) R) → MvPolynomial S₁ (MvPolynomial S₂ R))
        ((C : (a : R) → MvPolynomial (S₁ ⊕ S₂) R) a) :
      MvPolynomial S₁ (MvPolynomial S₂ R))
    ((C : (a : MvPolynomial S₂ R) → MvPolynomial S₁ (MvPolynomial S₂ R)) ((C : (a : R) → MvPolynomial S₂ R) a) :
      MvPolynomial S₁ (MvPolynomial S₂ R))

Tactic:
eval₂_C _ _ a

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, MvPolynomial.eval₂_C, MvPolynomial.eval₂, Finset.sum, Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
inst : CommSemiring R
b : S₁
⊢ Eq (α := MvPolynomial S₁ (MvPolynomial S₂ R))
    ((sumToIter R S₁ S₂ : (a : MvPolynomial (S₁ ⊕ S₂) R) → MvPolynomial S₁ (MvPolynomial S₂ R)) (X (Sum.inl b)) :
      MvPolynomial S₁ (MvPolynomial S₂ R))
    (X b : MvPolynomial S₁ (MvPolynomial S₂ R))

Tactic:
eval₂_X _ _ (Sum.inl b)

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, MvPolynomial.eval₂_X, MvPolynomial.eval₂, Sum.inl, Finset.sum
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
inst : CommSemiring R
c : S₂
⊢ Eq (α := MvPolynomial S₁ (MvPolynomial S₂ R))
    ((sumToIter R S₁ S₂ : (a : MvPolynomial (S₁ ⊕ S₂) R) → MvPolynomial S₁ (MvPolynomial S₂ R)) (X (Sum.inr c)) :
      MvPolynomial S₁ (MvPolynomial S₂ R))
    ((C : (a : MvPolynomial S₂ R) → MvPolynomial S₁ (MvPolynomial S₂ R)) (X c) : MvPolynomial S₁ (MvPolynomial S₂ R))

Tactic:
eval₂_X _ _ (Sum.inr c)

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, MvPolynomial.eval₂_X, MvPolynomial.eval₂, Sum.inr, Finset.sum
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
inst : CommSemiring R
a : R
⊢ Eq (α := MvPolynomial (S₁ ⊕ S₂) R)
    ((iterToSum R S₁ S₂ : (a : MvPolynomial S₁ (MvPolynomial S₂ R)) → MvPolynomial (S₁ ⊕ S₂) R)
        ((C : (a : MvPolynomial S₂ R) → MvPolynomial S₁ (MvPolynomial S₂ R)) ((C : (a : R) → MvPolynomial S₂ R) a)) :
      MvPolynomial (S₁ ⊕ S₂) R)
    ((C : (a : R) → MvPolynomial (S₁ ⊕ S₂) R) a : MvPolynomial (S₁ ⊕ S₂) R)

Tactic:
Eq.trans (eval₂_C _ _ (C a)) (eval₂_C _ _ _)

Premises used: MvPolynomial.eval₂_C, MvPolynomial.C, DFunLike.coe, Eq.trans
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
inst : CommSemiring R
b : S₁
⊢ Eq (α := MvPolynomial (S₁ ⊕ S₂) R)
    ((iterToSum R S₁ S₂ : (a : MvPolynomial S₁ (MvPolynomial S₂ R)) → MvPolynomial (S₁ ⊕ S₂) R) (X b) :
      MvPolynomial (S₁ ⊕ S₂) R)
    (X (Sum.inl b) : MvPolynomial (S₁ ⊕ S₂) 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.Equiv
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
inst : CommSemiring R
c : S₂
⊢ Eq (α := MvPolynomial (S₁ ⊕ S₂) R)
    ((iterToSum R S₁ S₂ : (a : MvPolynomial S₁ (MvPolynomial S₂ R)) → MvPolynomial (S₁ ⊕ S₂) R)
        ((C : (a : MvPolynomial S₂ R) → MvPolynomial S₁ (MvPolynomial S₂ R)) (X c)) :
      MvPolynomial (S₁ ⊕ S₂) R)
    (X (Sum.inr c) : MvPolynomial (S₁ ⊕ S₂) R)

Tactic:
Eq.trans (eval₂_C _ _ (X c)) (eval₂_X _ _ _)

Premises used: MvPolynomial.X, MvPolynomial.eval₂_X, MvPolynomial.eval₂_C, Eq.trans
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst : CommSemiring R
inst_1 : IsEmpty σ
⊢ Eq (α := R →ₐ[R] R)
    (AlgHom.comp (B := MvPolynomial σ R) (aeval fun (a : σ) ↦ isEmptyElim (p := fun (x : σ) ↦ R) a)
      (Algebra.ofId R (MvPolynomial σ R)))
    (AlgHom.id R R)

Tactic:
ext
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst : CommSemiring R
inst_1 : IsEmpty σ
hf :
  ∀ (i : σ) (m : σ →₀ ℕ),
    Eq.{u + 1} (α := R)
      (coeff m
        ((AlgHom.comp (Algebra.ofId R (MvPolynomial σ R)) (aeval fun (a : σ) ↦ isEmptyElim (p := fun (x : σ) ↦ R) a) :
            (a : MvPolynomial σ R) → MvPolynomial σ R)
          (X i)))
      (coeff m ((AlgHom.id R (MvPolynomial σ R) : (a : MvPolynomial σ R) → MvPolynomial σ R) (X i)))
⊢ Eq (α := MvPolynomial σ R →ₐ[R] MvPolynomial σ R)
    (AlgHom.comp (Algebra.ofId R (MvPolynomial σ R)) (aeval fun (a : σ) ↦ isEmptyElim (p := fun (x : σ) ↦ R) a))
    (AlgHom.id R (MvPolynomial σ R))

Tactic:
ext i m
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst : CommSemiring R
inst_1 : IsEmpty σ
i : σ
m : σ →₀ ℕ
⊢ Eq.{u + 1} (α := R)
    (coeff m
      ((AlgHom.comp (Algebra.ofId R (MvPolynomial σ R)) (aeval fun (a : σ) ↦ isEmptyElim (p := fun (x : σ) ↦ R) a) :
          (a : MvPolynomial σ R) → MvPolynomial σ R)
        (X i)))
    (coeff m ((AlgHom.id R (MvPolynomial σ R) : (a : MvPolynomial σ R) → MvPolynomial σ R) (X i)))

Tactic:
isEmptyElim i

Premises used: isEmptyElim
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst : CommSemiring R
inst_1 : IsEmpty σ
i : σ
m : σ →₀ ℕ
⊢ Eq.{u + 1} (α := R)
    (coeff m
      ((AlgHom.comp (Algebra.ofId R (MvPolynomial σ R)) (aeval fun (a : σ) ↦ isEmptyElim (p := fun (x : σ) ↦ R) a) :
          (a : MvPolynomial σ R) → MvPolynomial σ R)
        (X i)))
    (coeff m ((AlgHom.id R (MvPolynomial σ R) : (a : MvPolynomial σ R) → MvPolynomial σ R) (X i)))

Tactic:
exact isEmptyElim i
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : IsEmpty σ
inst_2 : CommSemiring S₁
inst_3 : Algebra R S₁
f : σ → S₁
hf :
  ∀ (i : σ),
    Eq.{v + 1} (α := S₁) ((aeval f : (a : MvPolynomial σ R) → S₁) (X i) : S₁)
      ((AlgHom.comp (Algebra.ofId R S₁) (↑(isEmptyAlgEquiv R σ) : MvPolynomial σ R →ₐ[R] R) :
            (a : MvPolynomial σ R) → S₁)
          (X i) :
        S₁)
⊢ Eq (α := MvPolynomial σ R →ₐ[R] S₁) (aeval f)
    (AlgHom.comp (Algebra.ofId R S₁) (↑(isEmptyAlgEquiv R σ) : MvPolynomial σ R →ₐ[R] R))

Tactic:
ext i
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : IsEmpty σ
inst_2 : CommSemiring S₁
inst_3 : Algebra R S₁
f : σ → S₁
i : σ
⊢ Eq.{v + 1} (α := S₁) ((aeval f : (a : MvPolynomial σ R) → S₁) (X i) : S₁)
    ((AlgHom.comp (Algebra.ofId R S₁) (↑(isEmptyAlgEquiv R σ) : MvPolynomial σ R →ₐ[R] R) : (a : MvPolynomial σ R) → S₁)
        (X i) :
      S₁)

Tactic:
IsEmpty.elim' ‹IsEmpty σ› i

Premises used: IsEmpty.elim'
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : IsEmpty σ
inst_2 : CommSemiring S₁
inst_3 : Algebra R S₁
f : σ → S₁
i : σ
⊢ Eq.{v + 1} (α := S₁) ((aeval f : (a : MvPolynomial σ R) → S₁) (X i) : S₁)
    ((AlgHom.comp (Algebra.ofId R S₁) (↑(isEmptyAlgEquiv R σ) : MvPolynomial σ R →ₐ[R] R) : (a : MvPolynomial σ R) → S₁)
        (X i) :
      S₁)

Tactic:
exact IsEmpty.elim' ‹IsEmpty σ› i

Premises used: IsEmpty.elim'
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : IsEmpty σ
inst_2 : CommSemiring S₁
inst_3 : Algebra R S₁
f : σ → S₁
⊢ Eq (α := MvPolynomial σ R →ₐ[R] S₁) (aeval f)
    (AlgHom.comp (Algebra.ofId R S₁) (↑(isEmptyAlgEquiv R σ) : MvPolynomial σ R →ₐ[R] R))

Tactic:
have : aeval f = (Algebra.ofId R S₁).comp (@isEmptyAlgEquiv R σ _ _).toAlgHom := by
    ext i
    exact IsEmpty.elim' ‹IsEmpty σ› i
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : IsEmpty σ
inst_2 : CommSemiring S₁
inst_3 : Algebra R S₁
f : σ → S₁
this :
  Eq (α := MvPolynomial σ R →ₐ[R] S₁) (aeval f)
    (AlgHom.comp (Algebra.ofId R S₁) (↑(isEmptyAlgEquiv R σ) : MvPolynomial σ R →ₐ[R] R))
rw :
  Injective (α := MvPolynomial σ R) (β := S₁)
      (⇑(AlgHom.comp (Algebra.ofId R S₁) (↑(isEmptyAlgEquiv R σ) : MvPolynomial σ R →ₐ[R] R)) :
        (a : MvPolynomial σ R) → S₁) ↔
    Injective (α := MvPolynomial σ R) (β := S₁)
      (Function.comp (β := R) (⇑(algebraMap R S₁) : (a : R) → S₁) (⇑(isEmptyAlgEquiv R σ) : (a : MvPolynomial σ R) → R))
⊢ Injective (α := MvPolynomial σ R) (β := S₁) (⇑(aeval f) : (a : MvPolynomial σ R) → S₁) ↔
    Injective.{u + 1, v + 1} (α := R) (β := S₁) (⇑(algebraMap R S₁) : (a : R) → S₁)

Tactic:
rw [this, ← Injective.of_comp_iff' _ (@isEmptyAlgEquiv R σ _ _).bijective]

Premises used: Function.Injective.of_comp_iff', MvPolynomial.isEmptyAlgEquiv, AlgEquiv.bijective
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : IsEmpty σ
inst_2 : CommSemiring S₁
inst_3 : Algebra R S₁
f : σ → S₁
this :
  Eq (α := MvPolynomial σ R →ₐ[R] S₁) (aeval f)
    (AlgHom.comp (Algebra.ofId R S₁) (↑(isEmptyAlgEquiv R σ) : MvPolynomial σ R →ₐ[R] R))
⊢ Injective (α := MvPolynomial σ R) (β := S₁)
      (⇑(AlgHom.comp (Algebra.ofId R S₁) (↑(isEmptyAlgEquiv R σ) : MvPolynomial σ R →ₐ[R] R)) :
        (a : MvPolynomial σ R) → S₁) ↔
    Injective (α := MvPolynomial σ R) (β := S₁)
      (Function.comp (β := R) (⇑(algebraMap R S₁) : (a : R) → S₁) (⇑(isEmptyAlgEquiv R σ) : (a : MvPolynomial σ R) → R))

Tactic:
rfl
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : IsEmpty σ
⊢ Eq (α := R →+* MvPolynomial σ R) (RingEquiv.toRingHom (RingEquiv.symm (isEmptyRingEquiv R σ))) C

Tactic:
rfl

Premises used: MulEquiv.toMonoidHom, RingEquiv.toRingHom, MvPolynomial.C, rfl, Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : IsEmpty σ
r : R
⊢ Eq (α := MvPolynomial σ R) ((RingEquiv.symm (isEmptyRingEquiv R σ) : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
    ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)

Tactic:
rfl

Premises used: rfl, Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
σ : Type u_2
R : Type u_3
inst : CommSemiring R
inst_1 : IsEmpty σ
x : MvPolynomial σ R
obtain :
  ∀ (x : R),
    Eq.{u_3 + 1} (α := R)
      ((isEmptyRingEquiv R σ : (a : MvPolynomial σ R) → R)
          ((RingEquiv.symm (isEmptyRingEquiv R σ) : (a : R) → MvPolynomial σ R) x : MvPolynomial σ R) :
        R)
      (coeff.{u_3, u_2} (σ := σ) 0 ((RingEquiv.symm (isEmptyRingEquiv R σ) : (a : R) → MvPolynomial σ R) x) : R)
⊢ (isEmptyRingEquiv R σ : (a : MvPolynomial σ R) → R) x = coeff 0 x

Tactic:
obtain ⟨x, rfl⟩ := (isEmptyRingEquiv R σ).symm.surjective x

Premises used: RingEquiv.surjective, MvPolynomial.isEmptyRingEquiv, RingEquiv.symm, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
σ : Type u_2
R : Type u_3
inst : CommSemiring R
inst_1 : IsEmpty σ
x : R
⊢ Eq.{u_3 + 1} (α := R)
    ((isEmptyRingEquiv R σ : (a : MvPolynomial σ R) → R)
        ((RingEquiv.symm (isEmptyRingEquiv R σ) : (a : R) → MvPolynomial σ R) x : MvPolynomial σ R) :
      R)
    (coeff.{u_3, u_2} (σ := σ) 0 ((RingEquiv.symm (isEmptyRingEquiv R σ) : (a : R) → MvPolynomial σ R) x) : R)

Tactic:
simp