awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPowerSeries.Evaluation
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : UniformSpace R
S : Type u_3
inst_2 : CommRing S
inst_3 : UniformSpace S
a : σ → S
inst_4 : IsTopologicalSemiring R
inst_5 : IsUniformAddGroup R
inst_6 : IsUniformAddGroup S
inst_7 : CompleteSpace S
inst_8 : T2Space S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
inst_11 : Algebra R S
inst_12 : ContinuousSMul R S
ha : HasEval a
f : MvPowerSeries σ R
simp_rw :
  HasSum
    (fun (d : σ →₀ ℕ) ↦
      HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) : S)
        (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e : S))
    (eval₂ (algebraMap R S) a f)
⊢ HasSum.{u_3, u_1} (α := S)
    (fun (d : σ →₀ ℕ) ↦
      HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := S) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
        (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e))
    ((aeval ha : (a : MvPowerSeries σ R) → S) f : S)

Tactic:
simp_rw [coe_aeval, ← algebraMap_smul (R := R) S, smul_eq_mul]

Premises used: algebraMap_smul, MvPowerSeries.coe_aeval, smul_eq_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.Evaluation
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : UniformSpace R
S : Type u_3
inst_2 : CommRing S
inst_3 : UniformSpace S
a : σ → S
inst_4 : IsTopologicalSemiring R
inst_5 : IsUniformAddGroup R
inst_6 : IsUniformAddGroup S
inst_7 : CompleteSpace S
inst_8 : T2Space S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
inst_11 : Algebra R S
inst_12 : ContinuousSMul R S
ha : HasEval a
f : MvPowerSeries σ R
⊢ HasSum
    (fun (d : σ →₀ ℕ) ↦
      HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) : S)
        (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e : S))
    (eval₂ (algebraMap R S) a f)

Tactic:
hasSum_eval₂ (continuous_algebraMap R S) ha f

Premises used: continuous_algebraMap, MvPowerSeries.hasSum_eval₂
-- Module: Mathlib.RingTheory.MvPowerSeries.Evaluation
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : UniformSpace R
S : Type u_3
inst_2 : CommRing S
inst_3 : UniformSpace S
a : σ → S
inst_4 : IsTopologicalSemiring R
inst_5 : IsUniformAddGroup R
inst_6 : IsUniformAddGroup S
inst_7 : CompleteSpace S
inst_8 : T2Space S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
inst_11 : Algebra R S
inst_12 : ContinuousSMul R S
ha : HasEval a
f : MvPowerSeries σ R
⊢ HasSum
    (fun (d : σ →₀ ℕ) ↦
      HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) : S)
        (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e : S))
    (eval₂ (algebraMap R S) a f)

Tactic:
exact hasSum_eval₂ (continuous_algebraMap R S) ha f

Premises used: continuous_algebraMap, MvPowerSeries.hasSum_eval₂
-- Module: Mathlib.RingTheory.MvPowerSeries.Evaluation
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : UniformSpace R
S : Type u_3
inst_2 : CommRing S
inst_3 : UniformSpace S
a : σ → S
inst_4 : IsTopologicalSemiring R
inst_5 : IsUniformAddGroup R
inst_6 : IsUniformAddGroup S
inst_7 : CompleteSpace S
inst_8 : T2Space S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
inst_11 : Algebra R S
inst_12 : ContinuousSMul R S
ha : HasEval a
f : MvPowerSeries σ R
⊢ Eq.{u_3 + 1} (α := S) ((aeval ha : (a : MvPowerSeries σ R) → S) f : S)
    (∑' (d : σ →₀ ℕ),
        HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := S) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
          (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e) :
      S)

Tactic:
(hasSum_aeval ha f).tsum_eq.symm

Premises used: MvPowerSeries.hasSum_aeval, HasSum.tsum_eq, Eq.symm
-- Module: Mathlib.RingTheory.MvPowerSeries.Evaluation
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : UniformSpace R
S : Type u_3
inst_2 : CommRing S
inst_3 : UniformSpace S
a : σ → S
inst_4 : IsTopologicalSemiring R
inst_5 : IsUniformAddGroup R
inst_6 : IsUniformAddGroup S
inst_7 : CompleteSpace S
inst_8 : T2Space S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
inst_11 : Algebra R S
inst_12 : ContinuousSMul R S
ha : HasEval a
T : Type u_4
inst_13 : CommRing T
inst_14 : UniformSpace T
inst_15 : IsUniformAddGroup T
inst_16 : IsTopologicalRing T
inst_17 : IsLinearTopology T T
inst_18 : T2Space T
inst_19 : Algebra R T
inst_20 : ContinuousSMul R T
inst_21 : CompleteSpace T
ε : S →ₐ[R] T
hε : Continuous[inst_3.toTopologicalSpace, inst_14.toTopologicalSpace] (⇑ε : (a : S) → T)
h :
  Eq (α := (a : MvPowerSeries σ R) → T) (⇑(ε.comp (aeval ha)) : (a : MvPowerSeries σ R) → T)
    (⇑(aeval ⋯) : (a : MvPowerSeries σ R) → T)
⊢ ε.comp (aeval ha) = aeval ⋯

Tactic:
apply DFunLike.ext'

Premises used: DFunLike.ext'
-- Module: Mathlib.RingTheory.MvPowerSeries.Evaluation
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : UniformSpace R
S : Type u_3
inst_2 : CommRing S
inst_3 : UniformSpace S
a : σ → S
inst_4 : IsTopologicalSemiring R
inst_5 : IsUniformAddGroup R
inst_6 : IsUniformAddGroup S
inst_7 : CompleteSpace S
inst_8 : T2Space S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
inst_11 : Algebra R S
inst_12 : ContinuousSMul R S
ha : HasEval a
T : Type u_4
inst_13 : CommRing T
inst_14 : UniformSpace T
inst_15 : IsUniformAddGroup T
inst_16 : IsTopologicalRing T
inst_17 : IsLinearTopology T T
inst_18 : T2Space T
inst_19 : Algebra R T
inst_20 : ContinuousSMul R T
inst_21 : CompleteSpace T
ε : S →ₐ[R] T
hε : Continuous[inst_3.toTopologicalSpace, inst_14.toTopologicalSpace] (⇑ε : (a : S) → T)
h :
  Eq (α := (a : MvPowerSeries σ R) → T) ((⇑ε : (a : S) → T) ∘ eval₂ (algebraMap R S) a)
    (⇑(aeval ⋯) : (a : MvPowerSeries σ R) → T)
⊢ Eq (α := (a : MvPowerSeries σ R) → T) (⇑(ε.comp (aeval ha)) : (a : MvPowerSeries σ R) → T)
    (⇑(aeval ⋯) : (a : MvPowerSeries σ R) → T)

Tactic:
simp only [AlgHom.coe_comp, coe_aeval ha]

Premises used: AlgHom.coe_comp, MvPowerSeries.coe_aeval
-- Module: Mathlib.RingTheory.MvPowerSeries.Evaluation
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : UniformSpace R
S : Type u_3
inst_2 : CommRing S
inst_3 : UniformSpace S
a : σ → S
inst_4 : IsTopologicalSemiring R
inst_5 : IsUniformAddGroup R
inst_6 : IsUniformAddGroup S
inst_7 : CompleteSpace S
inst_8 : T2Space S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
inst_11 : Algebra R S
inst_12 : ContinuousSMul R S
ha : HasEval a
T : Type u_4
inst_13 : CommRing T
inst_14 : UniformSpace T
inst_15 : IsUniformAddGroup T
inst_16 : IsTopologicalRing T
inst_17 : IsLinearTopology T T
inst_18 : T2Space T
inst_19 : Algebra R T
inst_20 : ContinuousSMul R T
inst_21 : CompleteSpace T
ε : S →ₐ[R] T
hε : Continuous[inst_3.toTopologicalSpace, inst_14.toTopologicalSpace] (⇑ε : (a : S) → T)
h :
  eval₂ (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑ε : S →+* T) (algebraMap R S))
      ((⇑(↑ε : S →+* T) : (a : S) → T) ∘ a) =
    eval₂ (algebraMap R T) fun (s : σ) ↦ (ε.toRingHom : (a : S) → T) (a s)
⊢ Eq (α := (a : MvPowerSeries σ R) → T) ((⇑ε : (a : S) → T) ∘ eval₂ (algebraMap R S) a)
    (⇑(aeval ⋯) : (a : MvPowerSeries σ R) → T)

Tactic:
rw [← RingHom.coe_coe,
    comp_eval₂ (continuous_algebraMap R S) ha (show Continuous (ε : S →+* T) from hε), coe_aeval]

Premises used: RingHom.coe_coe, continuous_algebraMap, MvPowerSeries.coe_aeval, MvPowerSeries.comp_eval₂
-- Module: Mathlib.RingTheory.MvPowerSeries.Evaluation
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : UniformSpace R
S : Type u_3
inst_2 : CommRing S
inst_3 : UniformSpace S
a : σ → S
inst_4 : IsTopologicalSemiring R
inst_5 : IsUniformAddGroup R
inst_6 : IsUniformAddGroup S
inst_7 : CompleteSpace S
inst_8 : T2Space S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
inst_11 : Algebra R S
inst_12 : ContinuousSMul R S
ha : HasEval a
T : Type u_4
inst_13 : CommRing T
inst_14 : UniformSpace T
inst_15 : IsUniformAddGroup T
inst_16 : IsTopologicalRing T
inst_17 : IsLinearTopology T T
inst_18 : T2Space T
inst_19 : Algebra R T
inst_20 : ContinuousSMul R T
inst_21 : CompleteSpace T
ε : S →ₐ[R] T
hε : Continuous[inst_3.toTopologicalSpace, inst_14.toTopologicalSpace] (⇑ε : (a : S) → T)
h : Eq (α := R →+* T) (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑ε : S →+* T) (algebraMap R S)) (algebraMap R T)
⊢ eval₂ (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑ε : S →+* T) (algebraMap R S))
      ((⇑(↑ε : S →+* T) : (a : S) → T) ∘ a) =
    eval₂ (algebraMap R T) fun (s : σ) ↦ (ε.toRingHom : (a : S) → T) (a s)

Tactic:
congr!
-- Module: Mathlib.RingTheory.MvPowerSeries.Evaluation
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : UniformSpace R
S : Type u_3
inst_2 : CommRing S
inst_3 : UniformSpace S
a : σ → S
inst_4 : IsTopologicalSemiring R
inst_5 : IsUniformAddGroup R
inst_6 : IsUniformAddGroup S
inst_7 : CompleteSpace S
inst_8 : T2Space S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
inst_11 : Algebra R S
inst_12 : ContinuousSMul R S
ha : HasEval a
T : Type u_4
inst_13 : CommRing T
inst_14 : UniformSpace T
inst_15 : IsUniformAddGroup T
inst_16 : IsTopologicalRing T
inst_17 : IsLinearTopology T T
inst_18 : T2Space T
inst_19 : Algebra R T
inst_20 : ContinuousSMul R T
inst_21 : CompleteSpace T
ε : S →ₐ[R] T
hε : Continuous[inst_3.toTopologicalSpace, inst_14.toTopologicalSpace] (⇑ε : (a : S) → T)
⊢ Eq (α := R →+* T) (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑ε : S →+* T) (algebraMap R S)) (algebraMap R T)

Tactic:
simp only [AlgHom.comp_algebraMap_of_tower]

Premises used: AlgHom.comp_algebraMap_of_tower
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
r : R
rw : ((C : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)
| ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) ((C : (a : R) → MvPowerSeries σ R) r) :
    MvPowerSeries σ R)

Tactic:
rw [← mul_one (C r), ← smul_eq_C_mul, expand, AlgHom.map_smul_of_tower,
    map_one, smul_eq_C_mul, mul_one]

Premises used: MvPowerSeries.expand, MvPowerSeries.smul_eq_C_mul, AlgHom.map_smul_of_tower, map_one, mul_one, DFunLike.coe, MvPowerSeries.C
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
r : R
conv_lhs :
  Eq (α := MvPowerSeries σ R)
    ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) ((C : (a : R) → MvPowerSeries σ R) r) :
      MvPowerSeries σ R)
    ((C : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)
conv_lhs₁ :
  Eq (α := MvPowerSeries σ R) ((C : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)
    ((C : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)
⊢ Eq (α := MvPowerSeries σ R)
    ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) ((C : (a : R) → MvPowerSeries σ R) r) :
      MvPowerSeries σ R)
    ((C : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)

Tactic:
conv_lhs => rw [← mul_one (C r), ← smul_eq_C_mul, expand, AlgHom.map_smul_of_tower,
    map_one, smul_eq_C_mul, mul_one]

Premises used: MvPowerSeries.expand, MvPowerSeries.smul_eq_C_mul, AlgHom.map_smul_of_tower, map_one, mul_one, DFunLike.coe, MvPowerSeries.C
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
i : σ
⊢ (expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) (X i) = HPow.hPow (α := MvPowerSeries σ R) (X i) p

Tactic:
substAlgHom_X (HasSubst.X_pow hp) i

Premises used: MvPowerSeries.substAlgHom_X, MvPowerSeries.HasSubst.X_pow
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
d : σ →₀ ℕ
r : R
rw :
  HMul.hMul (α := MvPowerSeries σ R) (β := MvPowerSeries σ R)
      ((algebraMap R (MvPowerSeries σ R) : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)
      (∏ a ∈ d.support, HPow.hPow (β := ℕ) (HPow.hPow (α := MvPowerSeries σ R) (X a) p) ((d : (a : σ) → ℕ) a : ℕ) :
        MvPowerSeries σ R) =
    HMul.hMul (α := MvPowerSeries σ R) (β := MvPowerSeries σ R)
      ((C : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)
      (∏ x ∈ d.support, HPow.hPow (α := MvPowerSeries σ R) (β := ℕ) (X x) ((p • d : (a : σ) → ℕ) x : ℕ) :
        MvPowerSeries σ R)
h : ∀ i ∈ d.support, HPow.hPow (α := MvPowerSeries σ R) (β := ℕ) (X i) 0 = 1
⊢ Eq (α := MvPowerSeries σ R)
    ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) ((monomial d : (a : R) → MvPowerSeries σ R) r) :
      MvPowerSeries σ R)
    ((monomial (p • d) : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)

Tactic:
rw [expand, substAlgHom_monomial (HasSubst.X_pow hp), monomial_eq', Finsupp.prod,
    Finsupp.prod_of_support_subset _ Finsupp.support_smul]

Premises used: MvPowerSeries.expand, Finsupp.prod_of_support_subset, MvPowerSeries.HasSubst.X_pow, Finsupp.support_smul, MvPowerSeries.substAlgHom_monomial, Finsupp.prod, MvPowerSeries.monomial_eq'
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
d : σ →₀ ℕ
r : R
⊢ HMul.hMul (α := MvPowerSeries σ R) (β := MvPowerSeries σ R)
      ((algebraMap R (MvPowerSeries σ R) : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)
      (∏ a ∈ d.support, HPow.hPow (β := ℕ) (HPow.hPow (α := MvPowerSeries σ R) (X a) p) ((d : (a : σ) → ℕ) a : ℕ) :
        MvPowerSeries σ R) =
    HMul.hMul (α := MvPowerSeries σ R) (β := MvPowerSeries σ R)
      ((C : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)
      (∏ x ∈ d.support, HPow.hPow (α := MvPowerSeries σ R) (β := ℕ) (X x) ((p • d : (a : σ) → ℕ) x : ℕ) :
        MvPowerSeries σ R)

Tactic:
simp [pow_mul, algebraMap_apply, Algebra.algebraMap_self]

Premises used: Algebra.algebraMap_self, pow_mul, MvPowerSeries.algebraMap_apply
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
d : σ →₀ ℕ
r : R
⊢ ∀ i ∈ d.support, HPow.hPow (α := MvPowerSeries σ R) (β := ℕ) (X i) 0 = 1

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
H :
  ∀ (i : MvPowerSeries σ R),
    Eq (α := MvPowerSeries σ R) ((expand 1 ⋯ : (a : MvPowerSeries σ R) → MvPowerSeries σ R) i : MvPowerSeries σ R)
      ((AlgHom.id R (MvPowerSeries σ R) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) i : MvPowerSeries σ R)
⊢ Eq (α := MvPowerSeries σ R →ₐ[R] MvPowerSeries σ R) (expand 1 ⋯) (AlgHom.id R (MvPowerSeries σ R))

Tactic:
ext1 i
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
i : MvPowerSeries σ R
⊢ Eq (α := MvPowerSeries σ R) ((expand 1 ⋯ : (a : MvPowerSeries σ R) → MvPowerSeries σ R) i : MvPowerSeries σ R)
    ((AlgHom.id R (MvPowerSeries σ R) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) i : MvPowerSeries σ R)

Tactic:
simp [expand, subst_self]

Premises used: MvPowerSeries.expand, MvPowerSeries.subst_self
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
f : MvPowerSeries σ R
⊢ (expand 1 ⋯ : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f = f

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
p : ℕ
hp : p ≠ 0
f : R →+* S
φ : MvPowerSeries σ R
⊢ Eq (α := MvPowerSeries σ S)
    ((map f : (a : MvPowerSeries σ R) → MvPowerSeries σ S)
        ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ) :
      MvPowerSeries σ S)
    ((expand p hp : (a : MvPowerSeries σ S) → MvPowerSeries σ S)
        ((map f : (a : MvPowerSeries σ R) → MvPowerSeries σ S) φ) :
      MvPowerSeries σ S)

Tactic:
simp [expand, map_subst (HasSubst.X_pow hp)]

Premises used: MvPowerSeries.expand, MvPowerSeries.map_subst, MvPowerSeries.HasSubst.X_pow
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
τ : Type u_2
S : Type u_4
inst : CommRing S
p : ℕ
hp : p ≠ 0
f : σ → MvPowerSeries τ S
hf : HasSubst f
⊢ HasSubst.{u_1, u_2, u_4} (τ := τ) (S := S) fun (i : σ) ↦
    (MvPowerSeries.expand p hp : (a : MvPowerSeries τ S) → MvPowerSeries τ S) (f i)

Tactic:
comp hf (HasSubst.X_pow hp)

Premises used: MvPowerSeries.HasSubst.comp, MvPowerSeries.HasSubst.X_pow
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
τ : Type u_2
S : Type u_4
inst : CommRing S
p : ℕ
hp : p ≠ 0
f : σ → MvPowerSeries τ S
hf : HasSubst f
H :
  ∀ (i : MvPowerSeries σ S),
    Eq (α := MvPowerSeries τ S)
      ((AlgHom.comp (expand p hp) (substAlgHom hf) : (a : MvPowerSeries σ S) → MvPowerSeries τ S) i : MvPowerSeries τ S)
      ((substAlgHom ⋯ : (a : MvPowerSeries σ S) → MvPowerSeries τ S) i : MvPowerSeries τ S)
⊢ AlgHom.comp (expand p hp) (substAlgHom hf) = substAlgHom ⋯

Tactic:
ext1 i
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
τ : Type u_2
S : Type u_4
inst : CommRing S
p : ℕ
hp : p ≠ 0
f : σ → MvPowerSeries τ S
hf : HasSubst f
i : MvPowerSeries σ S
⊢ Eq (α := MvPowerSeries τ S)
    ((AlgHom.comp (expand p hp) (substAlgHom hf) : (a : MvPowerSeries σ S) → MvPowerSeries τ S) i : MvPowerSeries τ S)
    ((substAlgHom ⋯ : (a : MvPowerSeries σ S) → MvPowerSeries τ S) i : MvPowerSeries τ S)

Tactic:
simp [expand, subst_comp_subst_apply hf (HasSubst.X_pow hp)]

Premises used: MvPowerSeries.expand, MvPowerSeries.subst_comp_subst_apply, MvPowerSeries.HasSubst.X_pow
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
τ : Type u_2
S : Type u_4
inst : CommRing S
p : ℕ
hp : p ≠ 0
f : σ → MvPowerSeries τ S
hf : HasSubst f
φ : MvPowerSeries σ S
rw :
  Eq (α := MvPowerSeries τ S)
    ((AlgHom.comp (expand p hp) (substAlgHom hf) : (a : MvPowerSeries σ S) → MvPowerSeries τ S) φ : MvPowerSeries τ S)
    ((substAlgHom ⋯ : (a : MvPowerSeries σ S) → MvPowerSeries τ S) φ : MvPowerSeries τ S)
rw₁ rw₂ :
  Eq (α := MvPowerSeries τ S) ((substAlgHom ⋯ : (a : MvPowerSeries σ S) → MvPowerSeries τ S) φ : MvPowerSeries τ S)
    ((substAlgHom ⋯ : (a : MvPowerSeries σ S) → MvPowerSeries τ S) φ : MvPowerSeries τ S)
⊢ Eq (α := MvPowerSeries τ S)
    ((expand p hp : (a : MvPowerSeries τ S) → MvPowerSeries τ S)
        ((substAlgHom hf : (a : MvPowerSeries σ S) → MvPowerSeries τ S) φ) :
      MvPowerSeries τ S)
    ((substAlgHom ⋯ : (a : MvPowerSeries σ S) → MvPowerSeries τ S) φ : MvPowerSeries τ S)

Tactic:
rw [← AlgHom.comp_apply, expand_comp_substAlgHom]

Premises used: AlgHom.comp_apply, MvPowerSeries.expand_comp_substAlgHom
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
f : σ → MvPowerSeries τ R
hf : HasSubst f
φ : MvPowerSeries σ R
rw :
  Eq (α := MvPowerSeries τ R)
    ((expand p hp : (a : MvPowerSeries τ R) → MvPowerSeries τ R)
        ((substAlgHom hf : (a : MvPowerSeries σ R) → MvPowerSeries τ R) φ) :
      MvPowerSeries τ R)
    (subst (fun (i : σ) ↦ (expand p hp : (a : MvPowerSeries τ R) → MvPowerSeries τ R) (f i)) φ : MvPowerSeries τ R)
rw₁ :
  Eq (α := MvPowerSeries τ R) ((substAlgHom ⋯ : (a : MvPowerSeries σ R) → MvPowerSeries τ R) φ : MvPowerSeries τ R)
    (subst (fun (i : σ) ↦ (expand p hp : (a : MvPowerSeries τ R) → MvPowerSeries τ R) (f i)) φ : MvPowerSeries τ R)
rw₂ rw₃ :
  Eq (α := MvPowerSeries τ R)
    (subst (fun (i : σ) ↦ (expand p hp : (a : MvPowerSeries τ R) → MvPowerSeries τ R) (f i)) φ)
    (subst (fun (i : σ) ↦ (expand p hp : (a : MvPowerSeries τ R) → MvPowerSeries τ R) (f i)) φ)
⊢ Eq (α := MvPowerSeries τ R)
    ((expand p hp : (a : MvPowerSeries τ R) → MvPowerSeries τ R) (subst f φ) : MvPowerSeries τ R)
    (subst (fun (i : σ) ↦ (expand p hp : (a : MvPowerSeries τ R) → MvPowerSeries τ R) (f i)) φ : MvPowerSeries τ R)

Tactic:
rw [← substAlgHom_apply hf, expand_substAlgHom, substAlgHom_apply]

Premises used: MvPowerSeries.expand_substAlgHom, MvPowerSeries.substAlgHom_apply
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
q : ℕ
hq : q ≠ 0
H :
  ∀ (i : MvPowerSeries σ R),
    Eq (α := MvPowerSeries σ R) ((expand (p * q) ⋯ : (a : MvPowerSeries σ R) → MvPowerSeries σ R) i : MvPowerSeries σ R)
      ((AlgHom.comp (expand p hp) (expand q hq) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) i : MvPowerSeries σ R)
⊢ Eq (α := MvPowerSeries σ R →ₐ[R] MvPowerSeries σ R) (expand (p * q) ⋯) (AlgHom.comp (expand p hp) (expand q hq))

Tactic:
ext1 i
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
q : ℕ
hq : q ≠ 0
i : MvPowerSeries σ R
⊢ Eq (α := MvPowerSeries σ R) ((expand (p * q) ⋯ : (a : MvPowerSeries σ R) → MvPowerSeries σ R) i : MvPowerSeries σ R)
    ((AlgHom.comp (expand p hp) (expand q hq) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) i : MvPowerSeries σ R)

Tactic:
simp [expand, pow_mul, subst_comp_subst_apply (HasSubst.X_pow hq) (HasSubst.X_pow hp),
    subst_pow (HasSubst.X_pow hp), subst_X (HasSubst.X_pow hp)]

Premises used: MvPowerSeries.expand, MvPowerSeries.subst_pow, MvPowerSeries.subst_comp_subst_apply, pow_mul, MvPowerSeries.HasSubst.X_pow, MvPowerSeries.subst_X
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
q : ℕ
hq : q ≠ 0
φ : MvPowerSeries σ R
⊢ Eq (α := MvPowerSeries σ R) ((expand (p * q) ⋯ : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ : MvPowerSeries σ R)
    ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
        ((expand q hq : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ) :
      MvPowerSeries σ R)

Tactic:
DFunLike.congr_fun (expand_mul_eq_comp p hp q hq) φ

Premises used: DFunLike.congr_fun, Classical.epsilon, Set.Mem, Filter.lim, MvPowerSeries.expand_mul_eq_comp, Filter.limUnder, IsDenseInducing.extend
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
m : σ →₀ ℕ
simp :
  Eq.{u_3 + 1} (α := R)
    (∑ᶠ (d : σ →₀ ℕ),
        HMul.hMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R)
          ((coeff (p • m) : (a : MvPowerSeries σ R) → R)
              (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e) :
            R) :
      R)
    ((coeff m : (a : MvPowerSeries σ R) → R) φ : R)
⊢ Eq.{u_3 + 1} (α := R)
    ((coeff (p • m) : (a : MvPowerSeries σ R) → R)
        ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ : MvPowerSeries σ R) :
      R)
    ((coeff m : (a : MvPowerSeries σ R) → R) φ : R)

Tactic:
simp only [expand, substAlgHom_apply, coeff_subst (HasSubst.X_pow hp), smul_eq_mul]

Premises used: MvPowerSeries.expand, MvPowerSeries.coeff_subst, MvPowerSeries.HasSubst.X_pow, smul_eq_mul, MvPowerSeries.substAlgHom_apply
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
m d : σ →₀ ℕ
⊢ Eq (α := MvPowerSeries σ R) (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e)
    ((monomial (p • d) : (a : R) → MvPowerSeries σ R) 1)

Tactic:
simp [monomial_smul_eq]

Premises used: MvPowerSeries.monomial_smul_eq
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
m : σ →₀ ℕ
⊢ ∀ {d : σ →₀ ℕ},
    Eq (α := MvPowerSeries σ R) (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e)
      ((monomial (p • d) : (a : R) → MvPowerSeries σ R) 1)

Tactic:
have {d : σ →₀ ℕ} : (d.prod fun s e ↦ (X s (R := R) ^ p) ^ e) = monomial (p • d) 1 := by
    simp [monomial_smul_eq]