awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hfgC :
  Eq (α := MvPolynomial S₂ R →+* MvPolynomial S₁ (MvPolynomial S₂ R))
    (RingHom.comp (RingHom.comp (sumToIter R S₁ S₂) (iterToSum R S₁ S₂)) C) C
hfgX :
  ∀ (n : S₁),
    Eq (α := MvPolynomial S₁ (MvPolynomial S₂ R))
      ((sumToIter R S₁ S₂ : (a : MvPolynomial (S₁ ⊕ S₂) R) → MvPolynomial S₁ (MvPolynomial S₂ R))
          ((iterToSum R S₁ S₂ : (a : MvPolynomial S₁ (MvPolynomial S₂ R)) → MvPolynomial (S₁ ⊕ S₂) R) (X n)) :
        MvPolynomial S₁ (MvPolynomial S₂ R))
      (X n : MvPolynomial S₁ (MvPolynomial S₂ R))
hgfC :
  Eq (α := R →+* MvPolynomial (S₁ ⊕ S₂) R) (RingHom.comp (RingHom.comp (iterToSum R S₁ S₂) (sumToIter R S₁ S₂)) C) C
hgfX :
  ∀ (n : S₁ ⊕ S₂),
    Eq (α := MvPolynomial (S₁ ⊕ S₂) R)
      ((iterToSum R S₁ S₂ : (a : MvPolynomial S₁ (MvPolynomial S₂ R)) → MvPolynomial (S₁ ⊕ S₂) R)
          ((sumToIter R S₁ S₂ : (a : MvPolynomial (S₁ ⊕ S₂) R) → MvPolynomial S₁ (MvPolynomial S₂ R)) (X n)) :
        MvPolynomial (S₁ ⊕ S₂) R)
      (X n : MvPolynomial (S₁ ⊕ S₂) R)
⊢ MvPolynomial (S₁ ⊕ S₂) R ≃+* MvPolynomial S₁ (MvPolynomial S₂ R)

Tactic:
apply mvPolynomialEquivMvPolynomial R (S₁ ⊕ S₂) _ _ (sumToIter R S₁ S₂) (iterToSum R S₁ S₂)

Premises used: MvPolynomial.iterToSum, Sum, MvPolynomial.mvPolynomialEquivMvPolynomial, MvPolynomial.sumToIter
-- 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
⊢ Eq (α := MvPolynomial S₂ R →+* MvPolynomial S₁ (MvPolynomial S₂ R))
    (RingHom.comp (RingHom.comp (sumToIter R S₁ S₂) (iterToSum R S₁ S₂)) C) C

Tactic:
RingHom.ext (hom_eq_hom _ _ ?hC ?hX)

Premises used: MvPolynomial.hom_eq_hom, RingHom.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
refine :
  Eq (α := R →+* MvPolynomial S₁ (MvPolynomial S₂ R))
    (RingHom.comp (RingHom.comp (RingHom.comp (sumToIter R S₁ S₂) (iterToSum R S₁ S₂)) C) C) (RingHom.comp C C)
refine₁ :
  ∀ (n : S₂),
    Eq (α := MvPolynomial S₁ (MvPolynomial S₂ R))
      ((RingHom.comp (RingHom.comp (sumToIter R S₁ S₂) (iterToSum R S₁ S₂)) C :
            (a : MvPolynomial S₂ R) → MvPolynomial S₁ (MvPolynomial S₂ R))
          (X n) :
        MvPolynomial S₁ (MvPolynomial S₂ R))
      ((C : (a : MvPolynomial S₂ R) → MvPolynomial S₁ (MvPolynomial S₂ R)) (X n) : MvPolynomial S₁ (MvPolynomial S₂ R))
⊢ Eq (α := MvPolynomial S₂ R →+* MvPolynomial S₁ (MvPolynomial S₂ R))
    (RingHom.comp (RingHom.comp (sumToIter R S₁ S₂) (iterToSum R S₁ S₂)) C) C

Tactic:
refine RingHom.ext (hom_eq_hom _ _ ?hC ?hX)

Premises used: MvPolynomial.hom_eq_hom, RingHom.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
a₃ :
  ∀ (x : R),
    Eq (α := MvPolynomial S₁ (MvPolynomial S₂ R))
      ((RingHom.comp (RingHom.comp (RingHom.comp (sumToIter R S₁ S₂) (iterToSum R S₁ S₂)) C) C :
            (a : R) → MvPolynomial S₁ (MvPolynomial S₂ R))
          x :
        MvPolynomial S₁ (MvPolynomial S₂ R))
      ((RingHom.comp C C : (a : R) → MvPolynomial S₁ (MvPolynomial S₂ R)) x : MvPolynomial S₁ (MvPolynomial S₂ R))
⊢ Eq (α := R →+* MvPolynomial S₁ (MvPolynomial S₂ R))
    (RingHom.comp (RingHom.comp (RingHom.comp (sumToIter R S₁ S₂) (iterToSum R S₁ S₂)) C) C) (RingHom.comp C C)

Tactic:
ext1
-- 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
x : R
⊢ Eq (α := MvPolynomial S₁ (MvPolynomial S₂ R))
    ((RingHom.comp (RingHom.comp (RingHom.comp (sumToIter R S₁ S₂) (iterToSum R S₁ S₂)) C) C :
          (a : R) → MvPolynomial S₁ (MvPolynomial S₂ R))
        x :
      MvPolynomial S₁ (MvPolynomial S₂ R))
    ((RingHom.comp C C : (a : R) → MvPolynomial S₁ (MvPolynomial S₂ R)) x : MvPolynomial S₁ (MvPolynomial S₂ R))

Tactic:
simp only [RingHom.comp_apply, iterToSum_C_C, sumToIter_C]

Premises used: RingHom.comp_apply, MvPolynomial.iterToSum_C_C, MvPolynomial.sumToIter_C
-- 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
⊢ Eq (α := R →+* MvPolynomial S₁ (MvPolynomial S₂ R))
    (RingHom.comp (RingHom.comp (RingHom.comp (sumToIter R S₁ S₂) (iterToSum R S₁ S₂)) C) C) (RingHom.comp C C)

Tactic:
case hC => ext1; simp only [RingHom.comp_apply, iterToSum_C_C, sumToIter_C]

Premises used: RingHom.comp_apply, MvPolynomial.iterToSum_C_C, MvPolynomial.sumToIter_C
-- 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
n : S₂
⊢ Eq (α := MvPolynomial S₁ (MvPolynomial S₂ R))
    ((RingHom.comp (RingHom.comp (sumToIter R S₁ S₂) (iterToSum R S₁ S₂)) C :
          (a : MvPolynomial S₂ R) → MvPolynomial S₁ (MvPolynomial S₂ R))
        (X n) :
      MvPolynomial S₁ (MvPolynomial S₂ R))
    ((C : (a : MvPolynomial S₂ R) → MvPolynomial S₁ (MvPolynomial S₂ R)) (X n) : MvPolynomial S₁ (MvPolynomial S₂ R))

Tactic:
simp only [RingHom.comp_apply, iterToSum_C_X, sumToIter_Xr]

Premises used: MvPolynomial.iterToSum_C_X, MvPolynomial.sumToIter_Xr, RingHom.comp_apply
-- 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
case case₁ :
  ∀ (n : S₂),
    Eq (α := MvPolynomial S₁ (MvPolynomial S₂ R))
      ((RingHom.comp (RingHom.comp (sumToIter R S₁ S₂) (iterToSum R S₁ S₂)) C :
            (a : MvPolynomial S₂ R) → MvPolynomial S₁ (MvPolynomial S₂ R))
          (X n) :
        MvPolynomial S₁ (MvPolynomial S₂ R))
      ((C : (a : MvPolynomial S₂ R) → MvPolynomial S₁ (MvPolynomial S₂ R)) (X n) : MvPolynomial S₁ (MvPolynomial S₂ R))
⊢ ∀ (n : S₂),
    Eq (α := MvPolynomial S₁ (MvPolynomial S₂ R))
      ((RingHom.comp (RingHom.comp (sumToIter R S₁ S₂) (iterToSum R S₁ S₂)) C :
            (a : MvPolynomial S₂ R) → MvPolynomial S₁ (MvPolynomial S₂ R))
          (X n) :
        MvPolynomial S₁ (MvPolynomial S₂ R))
      ((C : (a : MvPolynomial S₂ R) → MvPolynomial S₁ (MvPolynomial S₂ R)) (X n) : MvPolynomial S₁ (MvPolynomial S₂ R))

Tactic:
case hX => intro; simp only [RingHom.comp_apply, iterToSum_C_X, sumToIter_Xr]

Premises used: MvPolynomial.iterToSum_C_X, MvPolynomial.sumToIter_Xr, RingHom.comp_apply
-- 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
⊢ ∀ (n : S₁),
    Eq (α := MvPolynomial S₁ (MvPolynomial S₂ R))
      ((sumToIter R S₁ S₂ : (a : MvPolynomial (S₁ ⊕ S₂) R) → MvPolynomial S₁ (MvPolynomial S₂ R))
          ((iterToSum R S₁ S₂ : (a : MvPolynomial S₁ (MvPolynomial S₂ R)) → MvPolynomial (S₁ ⊕ S₂) R) (X n)) :
        MvPolynomial S₁ (MvPolynomial S₂ R))
      (X n : MvPolynomial S₁ (MvPolynomial S₂ R))

Tactic:
simp [iterToSum_X, sumToIter_Xl]

Premises used: MvPolynomial.iterToSum_X, MvPolynomial.sumToIter_Xl
-- 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
hgfC :
  ∀ (x : R),
    Eq (α := MvPolynomial (S₁ ⊕ S₂) R)
      ((RingHom.comp (RingHom.comp (iterToSum R S₁ S₂) (sumToIter R S₁ S₂)) C : (a : R) → MvPolynomial (S₁ ⊕ S₂) R) x :
        MvPolynomial (S₁ ⊕ S₂) R)
      ((C : (a : R) → MvPolynomial (S₁ ⊕ S₂) R) x : MvPolynomial (S₁ ⊕ S₂) R)
⊢ Eq (α := R →+* MvPolynomial (S₁ ⊕ S₂) R) (RingHom.comp (RingHom.comp (iterToSum R S₁ S₂) (sumToIter R S₁ S₂)) C) C

Tactic:
ext1
-- 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
x : R
⊢ Eq (α := MvPolynomial (S₁ ⊕ S₂) R)
    ((RingHom.comp (RingHom.comp (iterToSum R S₁ S₂) (sumToIter R S₁ S₂)) C : (a : R) → MvPolynomial (S₁ ⊕ S₂) R) x :
      MvPolynomial (S₁ ⊕ S₂) R)
    ((C : (a : R) → MvPolynomial (S₁ ⊕ S₂) R) x : MvPolynomial (S₁ ⊕ S₂) R)

Tactic:
simp only [RingHom.comp_apply, sumToIter_C, iterToSum_C_C]

Premises used: RingHom.comp_apply, MvPolynomial.iterToSum_C_C, MvPolynomial.sumToIter_C
-- 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
val : S₁
⊢ Eq (α := MvPolynomial (S₁ ⊕ S₂) R)
    ((iterToSum R S₁ S₂ : (a : MvPolynomial S₁ (MvPolynomial S₂ R)) → MvPolynomial (S₁ ⊕ S₂) R)
        ((sumToIter R S₁ S₂ : (a : MvPolynomial (S₁ ⊕ S₂) R) → MvPolynomial S₁ (MvPolynomial S₂ R)) (X (Sum.inl val))) :
      MvPolynomial (S₁ ⊕ S₂) R)
    (X (Sum.inl val) : MvPolynomial (S₁ ⊕ S₂) R)

Tactic:
simp only [sumToIter_Xl, iterToSum_X, sumToIter_Xr, iterToSum_C_X]

Premises used: MvPolynomial.iterToSum_C_X, MvPolynomial.iterToSum_X, MvPolynomial.sumToIter_Xr, MvPolynomial.sumToIter_Xl
-- 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
val : S₂
⊢ Eq (α := MvPolynomial (S₁ ⊕ S₂) R)
    ((iterToSum R S₁ S₂ : (a : MvPolynomial S₁ (MvPolynomial S₂ R)) → MvPolynomial (S₁ ⊕ S₂) R)
        ((sumToIter R S₁ S₂ : (a : MvPolynomial (S₁ ⊕ S₂) R) → MvPolynomial S₁ (MvPolynomial S₂ R)) (X (Sum.inr val))) :
      MvPolynomial (S₁ ⊕ S₂) R)
    (X (Sum.inr val) : MvPolynomial (S₁ ⊕ S₂) R)

Tactic:
simp only [sumToIter_Xl, iterToSum_X, sumToIter_Xr, iterToSum_C_X]

Premises used: MvPolynomial.iterToSum_C_X, MvPolynomial.iterToSum_X, MvPolynomial.sumToIter_Xr, MvPolynomial.sumToIter_Xl
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
inst : CommSemiring R
p : MvPolynomial (S₁ ⊕ S₂) R
⊢ (iterToSum R S₁ S₂ : (a : MvPolynomial S₁ (MvPolynomial S₂ R)) → MvPolynomial (S₁ ⊕ S₂) R)
      ((sumToIter R S₁ S₂ : (a : MvPolynomial (S₁ ⊕ S₂) R) → MvPolynomial S₁ (MvPolynomial S₂ R)) p) =
    p

Tactic:
(sumRingEquiv _ _ _).symm_apply_apply _

Premises used: Multiset.sum, Multiset.foldr, RingEquiv.symm_apply_apply, Finsupp.sum, MvPolynomial.eval₂, MvPolynomial.sumRingEquiv, Finset.sum
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
inst : CommSemiring R
p : MvPolynomial S₁ (MvPolynomial S₂ R)
⊢ (sumToIter R S₁ S₂ : (a : MvPolynomial (S₁ ⊕ S₂) R) → MvPolynomial S₁ (MvPolynomial S₂ R))
      ((iterToSum R S₁ S₂ : (a : MvPolynomial S₁ (MvPolynomial S₂ R)) → MvPolynomial (S₁ ⊕ S₂) R) p) =
    p

Tactic:
(sumRingEquiv _ _ _).apply_symm_apply _

Premises used: Multiset.sum, RingEquiv.apply_symm_apply, Multiset.foldr, Finsupp.sum, MvPolynomial.eval₂, MvPolynomial.sumRingEquiv, Finset.sum
-- 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
r : R
⊢ Eq (α := MvPolynomial S₁ (MvPolynomial S₂ R))
    ((algebraMap R (MvPolynomial S₁ (MvPolynomial S₂ R)) : (a : R) → MvPolynomial S₁ (MvPolynomial S₂ R)) r :
      MvPolynomial S₁ (MvPolynomial S₂ R))
    ((C : (a : MvPolynomial S₂ R) → MvPolynomial S₁ (MvPolynomial S₂ R)) ((C : (a : R) → MvPolynomial S₂ R) r) :
      MvPolynomial S₁ (MvPolynomial S₂ R))

Tactic:
have A : algebraMap R (MvPolynomial S₁ (MvPolynomial S₂ R)) r = (C (C r) :) := rfl
-- 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
r : R
A :
  Eq (α := MvPolynomial S₁ (MvPolynomial S₂ R))
    ((algebraMap R (MvPolynomial S₁ (MvPolynomial S₂ R)) : (a : R) → MvPolynomial S₁ (MvPolynomial S₂ R)) r :
      MvPolynomial S₁ (MvPolynomial S₂ R))
    ((C : (a : MvPolynomial S₂ R) → MvPolynomial S₁ (MvPolynomial S₂ R)) ((C : (a : R) → MvPolynomial S₂ R) r) :
      MvPolynomial S₁ (MvPolynomial S₂ R))
⊢ Eq (α := MvPolynomial (S₁ ⊕ S₂) R)
    ((algebraMap R (MvPolynomial (S₁ ⊕ S₂) R) : (a : R) → MvPolynomial (S₁ ⊕ S₂) R) r : MvPolynomial (S₁ ⊕ S₂) R)
    ((C : (a : R) → MvPolynomial (S₁ ⊕ S₂) R) r : MvPolynomial (S₁ ⊕ S₂) R)

Tactic:
have B : algebraMap R (MvPolynomial (S₁ ⊕ S₂) R) r = C r := rfl
-- 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
r : R
A :
  Eq (α := MvPolynomial S₁ (MvPolynomial S₂ R))
    ((algebraMap R (MvPolynomial S₁ (MvPolynomial S₂ R)) : (a : R) → MvPolynomial S₁ (MvPolynomial S₂ R)) r :
      MvPolynomial S₁ (MvPolynomial S₂ R))
    ((C : (a : MvPolynomial S₂ R) → MvPolynomial S₁ (MvPolynomial S₂ R)) ((C : (a : R) → MvPolynomial S₂ R) r) :
      MvPolynomial S₁ (MvPolynomial S₂ R))
B :
  Eq (α := MvPolynomial (S₁ ⊕ S₂) R)
    ((algebraMap R (MvPolynomial (S₁ ⊕ S₂) R) : (a : R) → MvPolynomial (S₁ ⊕ S₂) R) r : MvPolynomial (S₁ ⊕ S₂) R)
    ((C : (a : R) → MvPolynomial (S₁ ⊕ S₂) R) r : MvPolynomial (S₁ ⊕ S₂) R)
⊢ Eq (α := MvPolynomial S₁ (MvPolynomial S₂ R))
    (Equiv.toFun (RingEquiv.toEquiv (sumRingEquiv R S₁ S₂))
      ((algebraMap R (MvPolynomial (S₁ ⊕ S₂) R) : (a : R) → MvPolynomial (S₁ ⊕ S₂) R) r))
    ((algebraMap R (MvPolynomial S₁ (MvPolynomial S₂ R)) : (a : R) → MvPolynomial S₁ (MvPolynomial S₂ R)) r)

Tactic:
simp only [sumRingEquiv, mvPolynomialEquivMvPolynomial, Equiv.toFun_as_coe,
        Equiv.coe_fn_mk, B, sumToIter_C, A]

Premises used: Equiv.toFun_as_coe, MvPolynomial.mvPolynomialEquivMvPolynomial, MvPolynomial.sumRingEquiv, Equiv.coe_fn_mk, MvPolynomial.sumToIter_C
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
inst : CommSemiring R
hf :
  ∀ (i : S₂) (m : S₁ →₀ ℕ) (m_1 : S₂ →₀ ℕ),
    Eq.{u + 1} (α := R)
      (coeff m_1
        (coeff m
          ((AlgHom.comp (↑(sumAlgEquiv R S₁ S₂) : MvPolynomial (S₁ ⊕ S₂) R →ₐ[R] MvPolynomial S₁ (MvPolynomial S₂ R))
                (rename Sum.inr) :
              (a : MvPolynomial S₂ R) → MvPolynomial S₁ (MvPolynomial S₂ R))
            (X i))))
      (coeff m_1
        (coeff m
          ((IsScalarTower.toAlgHom R (MvPolynomial S₂ R) (MvPolynomial S₁ (MvPolynomial S₂ R)) :
              (a : MvPolynomial S₂ R) → MvPolynomial S₁ (MvPolynomial S₂ R))
            (X i))))
⊢ Eq (α := MvPolynomial S₂ R →ₐ[R] MvPolynomial S₁ (MvPolynomial S₂ R))
    (AlgHom.comp (↑(sumAlgEquiv R S₁ S₂) : MvPolynomial (S₁ ⊕ S₂) R →ₐ[R] MvPolynomial S₁ (MvPolynomial S₂ R))
      (rename Sum.inr))
    (IsScalarTower.toAlgHom R (MvPolynomial S₂ R) (MvPolynomial S₁ (MvPolynomial S₂ R)))

Tactic:
ext i
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
inst : CommSemiring R
i : S₂
m : S₁ →₀ ℕ
m_1 : S₂ →₀ ℕ
⊢ Eq.{u + 1} (α := R)
    (coeff m_1
      (coeff m
        ((AlgHom.comp (↑(sumAlgEquiv R S₁ S₂) : MvPolynomial (S₁ ⊕ S₂) R →ₐ[R] MvPolynomial S₁ (MvPolynomial S₂ R))
              (rename Sum.inr) :
            (a : MvPolynomial S₂ R) → MvPolynomial S₁ (MvPolynomial S₂ R))
          (X i))))
    (coeff m_1
      (coeff m
        ((IsScalarTower.toAlgHom R (MvPolynomial S₂ R) (MvPolynomial S₁ (MvPolynomial S₂ R)) :
            (a : MvPolynomial S₂ R) → MvPolynomial S₁ (MvPolynomial S₂ R))
          (X i))))

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
inst : CommSemiring R
hf :
  ∀ (i : S₁) (m : S₁ →₀ ℕ) (m_1 : S₂ →₀ ℕ),
    Eq.{u + 1} (α := R)
      (coeff m_1
        (coeff m
          ((AlgHom.comp (↑(sumAlgEquiv R S₁ S₂) : MvPolynomial (S₁ ⊕ S₂) R →ₐ[R] MvPolynomial S₁ (MvPolynomial S₂ R))
                (rename Sum.inl) :
              (a : MvPolynomial S₁ R) → MvPolynomial S₁ (MvPolynomial S₂ R))
            (X i))))
      (coeff m_1
        (coeff m
          ((mapAlgHom (Algebra.ofId R (MvPolynomial S₂ R)) :
              (a : MvPolynomial S₁ R) → MvPolynomial S₁ (MvPolynomial S₂ R))
            (X i))))
⊢ Eq (α := MvPolynomial S₁ R →ₐ[R] MvPolynomial S₁ (MvPolynomial S₂ R))
    (AlgHom.comp (↑(sumAlgEquiv R S₁ S₂) : MvPolynomial (S₁ ⊕ S₂) R →ₐ[R] MvPolynomial S₁ (MvPolynomial S₂ R))
      (rename Sum.inl))
    (mapAlgHom (Algebra.ofId R (MvPolynomial S₂ R)))

Tactic:
ext i
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
inst : CommSemiring R
i : S₁
m : S₁ →₀ ℕ
m_1 : S₂ →₀ ℕ
⊢ Eq.{u + 1} (α := R)
    (coeff m_1
      (coeff m
        ((AlgHom.comp (↑(sumAlgEquiv R S₁ S₂) : MvPolynomial (S₁ ⊕ S₂) R →ₐ[R] MvPolynomial S₁ (MvPolynomial S₂ R))
              (rename Sum.inl) :
            (a : MvPolynomial S₁ R) → MvPolynomial S₁ (MvPolynomial S₂ R))
          (X i))))
    (coeff m_1
      (coeff m
        ((mapAlgHom (Algebra.ofId R (MvPolynomial S₂ R)) :
            (a : MvPolynomial S₁ R) → MvPolynomial S₁ (MvPolynomial S₂ R))
          (X i))))

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u_2
S₁ : Type u_3
S₂ : Type u_4
inst : CommSemiring R
p : MvPolynomial S₂ R
this :
  Eq (α := MvPolynomial S₂ R →ₐ[R] MvPolynomial S₂ (MvPolynomial S₁ R))
    (AlgHom.comp
      (↑(commAlgEquiv R S₁ S₂) : MvPolynomial S₁ (MvPolynomial S₂ R) →ₐ[R] MvPolynomial S₂ (MvPolynomial S₁ R))
      (IsScalarTower.toAlgHom R (MvPolynomial S₂ R) (MvPolynomial S₁ (MvPolynomial S₂ R))))
    (mapAlgHom (Algebra.ofId R (MvPolynomial S₁ R)))
⊢ Eq (α := MvPolynomial S₂ (MvPolynomial S₁ R))
    ((commAlgEquiv R S₁ S₂ : (a : MvPolynomial S₁ (MvPolynomial S₂ R)) → MvPolynomial S₂ (MvPolynomial S₁ R))
        ((C : (a : MvPolynomial S₂ R) → MvPolynomial S₁ (MvPolynomial S₂ R)) p) :
      MvPolynomial S₂ (MvPolynomial S₁ R))
    ((map C : (a : MvPolynomial S₂ R) → MvPolynomial S₂ (MvPolynomial S₁ R)) p : MvPolynomial S₂ (MvPolynomial S₁ R))

Tactic:
DFunLike.congr_fun this p

Premises used: Multiset.sum, Multiset.foldr, DFunLike.congr_fun, Finsupp.sum, MvPolynomial.eval₂, MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, MvPolynomial.C, Finset.sum, Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u_2
S₁ : Type u_3
S₂ : Type u_4
inst : CommSemiring R
p : MvPolynomial S₂ R
this :
  Eq (α := MvPolynomial S₂ R →ₐ[R] MvPolynomial S₂ (MvPolynomial S₁ R))
    (AlgHom.comp
      (↑(commAlgEquiv R S₁ S₂) : MvPolynomial S₁ (MvPolynomial S₂ R) →ₐ[R] MvPolynomial S₂ (MvPolynomial S₁ R))
      (IsScalarTower.toAlgHom R (MvPolynomial S₂ R) (MvPolynomial S₁ (MvPolynomial S₂ R))))
    (mapAlgHom (Algebra.ofId R (MvPolynomial S₁ R)))
⊢ Eq (α := MvPolynomial S₂ (MvPolynomial S₁ R))
    ((commAlgEquiv R S₁ S₂ : (a : MvPolynomial S₁ (MvPolynomial S₂ R)) → MvPolynomial S₂ (MvPolynomial S₁ R))
        ((C : (a : MvPolynomial S₂ R) → MvPolynomial S₁ (MvPolynomial S₂ R)) p) :
      MvPolynomial S₂ (MvPolynomial S₁ R))
    ((map C : (a : MvPolynomial S₂ R) → MvPolynomial S₂ (MvPolynomial S₁ R)) p : MvPolynomial S₂ (MvPolynomial S₁ R))

Tactic:
exact DFunLike.congr_fun this p

Premises used: DFunLike.congr_fun
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u_2
S₁ : Type u_3
S₂ : Type u_4
inst : CommSemiring R
p : MvPolynomial S₂ R
suffices :
  Eq (α := MvPolynomial S₂ R →ₐ[R] MvPolynomial S₂ (MvPolynomial S₁ R))
    (AlgHom.comp
      (↑(commAlgEquiv R S₁ S₂) : MvPolynomial S₁ (MvPolynomial S₂ R) →ₐ[R] MvPolynomial S₂ (MvPolynomial S₁ R))
      (IsScalarTower.toAlgHom R (MvPolynomial S₂ R) (MvPolynomial S₁ (MvPolynomial S₂ R))))
    (mapAlgHom (Algebra.ofId R (MvPolynomial S₁ R)))
⊢ Eq (α := MvPolynomial S₂ (MvPolynomial S₁ R))
    ((commAlgEquiv R S₁ S₂ : (a : MvPolynomial S₁ (MvPolynomial S₂ R)) → MvPolynomial S₂ (MvPolynomial S₁ R))
        ((C : (a : MvPolynomial S₂ R) → MvPolynomial S₁ (MvPolynomial S₂ R)) p) :
      MvPolynomial S₂ (MvPolynomial S₁ R))
    ((map C : (a : MvPolynomial S₂ R) → MvPolynomial S₂ (MvPolynomial S₁ R)) p : MvPolynomial S₂ (MvPolynomial S₁ R))

Tactic:
suffices (commAlgEquiv R S₁ S₂).toAlgHom.comp
      (IsScalarTower.toAlgHom R (MvPolynomial S₂ R) _) = mapAlgHom (Algebra.ofId _ _) by
    exact DFunLike.congr_fun this p
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u_2
S₁ : Type u_3
S₂ : Type u_4
inst : CommSemiring R
p : MvPolynomial S₂ R
hf :
  ∀ (x : S₂),
    Eq (α := MvPolynomial S₂ (MvPolynomial S₁ R))
      ((AlgHom.comp
              (↑(commAlgEquiv R S₁ S₂) : MvPolynomial S₁ (MvPolynomial S₂ R) →ₐ[R] MvPolynomial S₂ (MvPolynomial S₁ R))
              (IsScalarTower.toAlgHom R (MvPolynomial S₂ R) (MvPolynomial S₁ (MvPolynomial S₂ R))) :
            (a : MvPolynomial S₂ R) → MvPolynomial S₂ (MvPolynomial S₁ R))
          (X x) :
        MvPolynomial S₂ (MvPolynomial S₁ R))
      ((mapAlgHom (Algebra.ofId R (MvPolynomial S₁ R)) : (a : MvPolynomial S₂ R) → MvPolynomial S₂ (MvPolynomial S₁ R))
          (X x) :
        MvPolynomial S₂ (MvPolynomial S₁ R))
⊢ Eq (α := MvPolynomial S₂ R →ₐ[R] MvPolynomial S₂ (MvPolynomial S₁ R))
    (AlgHom.comp
      (↑(commAlgEquiv R S₁ S₂) : MvPolynomial S₁ (MvPolynomial S₂ R) →ₐ[R] MvPolynomial S₂ (MvPolynomial S₁ R))
      (IsScalarTower.toAlgHom R (MvPolynomial S₂ R) (MvPolynomial S₁ (MvPolynomial S₂ R))))
    (mapAlgHom (Algebra.ofId R (MvPolynomial S₁ R)))

Tactic:
ext x : 1
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u_2
S₁ : Type u_3
S₂ : Type u_4
inst : CommSemiring R
p : MvPolynomial S₂ R
x : S₂
⊢ Eq (α := MvPolynomial S₂ (MvPolynomial S₁ R))
    ((AlgHom.comp
            (↑(commAlgEquiv R S₁ S₂) : MvPolynomial S₁ (MvPolynomial S₂ R) →ₐ[R] MvPolynomial S₂ (MvPolynomial S₁ R))
            (IsScalarTower.toAlgHom R (MvPolynomial S₂ R) (MvPolynomial S₁ (MvPolynomial S₂ R))) :
          (a : MvPolynomial S₂ R) → MvPolynomial S₂ (MvPolynomial S₁ R))
        (X x) :
      MvPolynomial S₂ (MvPolynomial S₁ R))
    ((mapAlgHom (Algebra.ofId R (MvPolynomial S₁ R)) : (a : MvPolynomial S₂ R) → MvPolynomial S₂ (MvPolynomial S₁ R))
        (X x) :
      MvPolynomial S₂ (MvPolynomial S₁ R))

Tactic:
simp [commAlgEquiv]

Premises used: MvPolynomial.commAlgEquiv
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u_2
S₁ : Type u_3
S₂ : Type u_4
inst : CommSemiring R
i : S₂
⊢ Eq (α := MvPolynomial S₂ (MvPolynomial S₁ R))
    ((commAlgEquiv R S₁ S₂ : (a : MvPolynomial S₁ (MvPolynomial S₂ R)) → MvPolynomial S₂ (MvPolynomial S₁ R))
        ((C : (a : MvPolynomial S₂ R) → MvPolynomial S₁ (MvPolynomial S₂ R)) (X i)) :
      MvPolynomial S₂ (MvPolynomial S₁ R))
    (X i : MvPolynomial S₂ (MvPolynomial S₁ R))

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u_2
S₁ : Type u_3
S₂ : Type u_4
inst : CommSemiring R
i : S₁
⊢ Eq (α := MvPolynomial S₂ (MvPolynomial S₁ R))
    ((commAlgEquiv R S₁ S₂ : (a : MvPolynomial S₁ (MvPolynomial S₂ R)) → MvPolynomial S₂ (MvPolynomial S₁ R)) (X i) :
      MvPolynomial S₂ (MvPolynomial S₁ R))
    ((C : (a : MvPolynomial S₁ R) → MvPolynomial S₂ (MvPolynomial S₁ R)) (X i) : MvPolynomial S₂ (MvPolynomial S₁ R))

Tactic:
simp [commAlgEquiv]

Premises used: MvPolynomial.commAlgEquiv