awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
f : σ → τ
inst : TendstoCofinite f
R : Type u_6
inst_1 : CommRing R
p : MvPowerSeries σ R
n : τ →₀ ℕ
this :
  ∀ (d : σ →₀ ℕ)
    (hd :
      HMul.hMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) p : R)
          ((coeff n : (a : MvPowerSeries τ R) → R)
              (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries τ R) (X (f s)) e) :
            R) ≠
        0),
    mapDomain f d = n
h :
  Set.Finite.toFinset (s :=
      Function.support.{u_1, u_6} (M := R) fun (d : σ →₀ ℕ) ↦
        HSMul.hSMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) p : R)
          ((coeff n : (a : MvPowerSeries τ R) → R)
              (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries τ R) ((X ∘ f) s) e) :
            R))
      ⋯ ⊆
    Set.Finite.toFinset (s := mapDomain f ⁻¹' {n}) ⋯
h₁ :
  ∀
    x ∈
      Set.Finite.toFinset (s := mapDomain f ⁻¹' {n}) ⋯ \
        Set.Finite.toFinset (s :=
          Function.support.{u_1, u_6} (M := R) fun (d : σ →₀ ℕ) ↦
            HSMul.hSMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) p : R)
              ((coeff n : (a : MvPowerSeries τ R) → R)
                  (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries τ R) ((X ∘ f) s) e) :
                R))
          ⋯,
    Eq.{u_6 + 1} (α := R) ((coeff x : (a : MvPowerSeries σ R) → R) p : R) (0 : R)
h₂ :
  ∀ (x : σ →₀ ℕ)
    (hx :
      x ∈
        Set.Finite.toFinset (s :=
          Function.support.{u_1, u_6} (M := R) fun (d : σ →₀ ℕ) ↦
            HSMul.hSMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) p : R)
              ((coeff n : (a : MvPowerSeries τ R) → R)
                  (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries τ R) ((X ∘ f) s) e) :
                R))
          ⋯),
    HSMul.hSMul (α := R) (β := R) ((coeff x : (a : MvPowerSeries σ R) → R) p : R)
        ((coeff n : (a : MvPowerSeries τ R) → R)
            (x.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries τ R) ((X ∘ f) s) e) :
          R) =
      (coeff x : (a : MvPowerSeries σ R) → R) p
⊢ Eq.{u_6 + 1} (α := R)
    (∑ x ∈ Set.Finite.toFinset (s := mapDomain f ⁻¹' {n}) ⋯, (coeff x : (a : MvPowerSeries σ R) → R) p)
    (∑
      i ∈
        Set.Finite.toFinset (s :=
          Function.support.{u_1, u_6} (M := R) fun (d : σ →₀ ℕ) ↦
            HSMul.hSMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) p : R)
              ((coeff n : (a : MvPowerSeries τ R) → R)
                  (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries τ R) ((X ∘ f) s) e) :
                R))
          ⋯,
      HSMul.hSMul (α := R) (β := R) ((coeff i : (a : MvPowerSeries σ R) → R) p : R)
        ((coeff n : (a : MvPowerSeries τ R) → R)
            (i.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries τ R) ((X ∘ f) s) e) :
          R))

Tactic:
refine (Finset.sum_subset_zero_on_sdiff ?_ ?_ (fun x hx => ?_)).symm

Premises used: Eq.symm, Finset.sum_subset_zero_on_sdiff
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
f : σ → τ
inst : TendstoCofinite f
R : Type u_6
inst_1 : CommRing R
p : MvPowerSeries σ R
n : τ →₀ ℕ
this :
  ∀ (d : σ →₀ ℕ)
    (hd :
      HMul.hMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) p : R)
          ((coeff n : (a : MvPowerSeries τ R) → R)
              (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries τ R) (X (f s)) e) :
            R) ≠
        0),
    mapDomain f d = n
⊢ Set.Finite.toFinset (s :=
      Function.support.{u_1, u_6} (M := R) fun (d : σ →₀ ℕ) ↦
        HSMul.hSMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) p : R)
          ((coeff n : (a : MvPowerSeries τ R) → R)
              (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries τ R) ((X ∘ f) s) e) :
            R))
      ⋯ ⊆
    Set.Finite.toFinset (s := mapDomain f ⁻¹' {n}) ⋯

Tactic:
Set.Finite.toFinset_mono this

Premises used: Set.Mem, setOf, Set.Finite.toFinset_mono
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
f : σ → τ
inst : TendstoCofinite f
R : Type u_6
inst_1 : CommRing R
p : MvPowerSeries σ R
n : τ →₀ ℕ
this :
  ∀ (d : σ →₀ ℕ)
    (hd :
      HMul.hMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) p : R)
          ((coeff n : (a : MvPowerSeries τ R) → R)
              (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries τ R) (X (f s)) e) :
            R) ≠
        0),
    mapDomain f d = n
⊢ Set.Finite.toFinset (s :=
      Function.support.{u_1, u_6} (M := R) fun (d : σ →₀ ℕ) ↦
        HSMul.hSMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) p : R)
          ((coeff n : (a : MvPowerSeries τ R) → R)
              (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries τ R) ((X ∘ f) s) e) :
            R))
      ⋯ ⊆
    Set.Finite.toFinset (s := mapDomain f ⁻¹' {n}) ⋯

Tactic:
exact Set.Finite.toFinset_mono this

Premises used: Set.Finite.toFinset_mono
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
f : σ → τ
inst : TendstoCofinite f
R : Type u_6
inst_1 : CommRing R
p : MvPowerSeries σ R
n : τ →₀ ℕ
this :
  ∀ (d : σ →₀ ℕ)
    (hd :
      HMul.hMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) p : R)
          ((coeff n : (a : MvPowerSeries τ R) → R)
              (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries τ R) (X (f s)) e) :
            R) ≠
        0),
    mapDomain f d = n
⊢ ∀
    x ∈
      Set.Finite.toFinset (s := mapDomain f ⁻¹' {n}) ⋯ \
        Set.Finite.toFinset (s :=
          Function.support.{u_1, u_6} (M := R) fun (d : σ →₀ ℕ) ↦
            HSMul.hSMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) p : R)
              ((coeff n : (a : MvPowerSeries τ R) → R)
                  (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries τ R) ((X ∘ f) s) e) :
                R))
          ⋯,
    Eq.{u_6 + 1} (α := R) ((coeff x : (a : MvPowerSeries σ R) → R) p : R) (0 : R)

Tactic:
simp +contextual [← monomial_mapDomain_apply_one]

Premises used: MvPowerSeries.monomial_mapDomain_apply_one
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
f : σ → τ
inst : TendstoCofinite f
R : Type u_6
inst_1 : CommRing R
p : MvPowerSeries σ R
n : τ →₀ ℕ
this :
  ∀ (d : σ →₀ ℕ)
    (hd :
      HMul.hMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) p : R)
          ((coeff n : (a : MvPowerSeries τ R) → R)
              (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries τ R) (X (f s)) e) :
            R) ≠
        0),
    mapDomain f d = n
x : σ →₀ ℕ
hx :
  x ∈
    Set.Finite.toFinset (s :=
      Function.support.{u_1, u_6} (M := R) fun (d : σ →₀ ℕ) ↦
        HSMul.hSMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) p : R)
          ((coeff n : (a : MvPowerSeries τ R) → R)
              (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries τ R) ((X ∘ f) s) e) :
            R))
      ⋯
⊢ Membership.mem (γ := Set (σ →₀ ℕ))
    (Function.support.{u_1, u_6} (M := R) fun (d : σ →₀ ℕ) ↦
      HSMul.hSMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) p : R)
        ((coeff n : (a : MvPowerSeries τ R) → R)
            (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries τ R) ((X ∘ f) s) e) :
          R))
    x

Tactic:
simp only [Set.Finite.mem_toFinset] at hx

Premises used: Set.Finite.mem_toFinset
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
f : σ → τ
inst : TendstoCofinite f
R : Type u_6
inst_1 : CommRing R
p : MvPowerSeries σ R
n : τ →₀ ℕ
this :
  ∀ (d : σ →₀ ℕ)
    (hd :
      HMul.hMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) p : R)
          ((coeff n : (a : MvPowerSeries τ R) → R)
              (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries τ R) (X (f s)) e) :
            R) ≠
        0),
    mapDomain f d = n
x : σ →₀ ℕ
hx :
  Membership.mem (γ := Set (σ →₀ ℕ))
    (Function.support.{u_1, u_6} (M := R) fun (d : σ →₀ ℕ) ↦
      HSMul.hSMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) p : R)
        ((coeff n : (a : MvPowerSeries τ R) → R)
            (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries τ R) ((X ∘ f) s) e) :
          R))
    x
⊢ HSMul.hSMul (α := R) (β := R) ((coeff x : (a : MvPowerSeries σ R) → R) p : R)
      ((coeff n : (a : MvPowerSeries τ R) → R)
          (x.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries τ R) ((X ∘ f) s) e) :
        R) =
    (coeff x : (a : MvPowerSeries σ R) → R) p

Tactic:
simp [← this _ hx, ← monomial_mapDomain_apply_one, coeff_monomial_same]

Premises used: MvPowerSeries.coeff_monomial_same, MvPowerSeries.monomial_mapDomain_apply_one
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
τ : Type u_4
S : Type u_5
inst : CommRing S
a : σ → MvPowerSeries τ S
inst_1 : TopologicalSpace S
inst_2 : DiscreteTopology S
⊢ Filter.Tendsto a Filter.cofinite (nhds 0) ↔
    ∀ (d : τ →₀ ℕ),
      Set.Finite.{u_1} (α := σ)
        {s : σ | Ne.{u_5 + 1} (α := S) ((coeff d : (a : MvPowerSeries τ S) → S) (a s) : S) (0 : S)}

Tactic:
simp [tendsto_iff_coeff_tendsto, coeff_zero, nhds_discrete]

Premises used: MvPowerSeries.coeff_zero, nhds_discrete, MvPowerSeries.WithPiTopology.tendsto_iff_coeff_tendsto
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
τ : Type u_4
S : Type u_5
inst : CommRing S
a : σ → MvPowerSeries τ S
inst_1 : TopologicalSpace S
inst_2 : DiscreteTopology S
simp_rw :
  ((∀ (s : σ), IsNilpotent.{u_5} (R := S) ((constantCoeff : (a : MvPowerSeries τ S) → S) (a s) : S)) ∧
      ∀ (d : τ →₀ ℕ),
        Set.Finite.{u_1} (α := σ)
          {s : σ | Ne.{u_5 + 1} (α := S) ((coeff d : (a : MvPowerSeries τ S) → S) (a s) : S) (0 : S)}) ↔
    HasEval a
simp_rw₁ :
  ((∀ (s : σ), IsNilpotent.{u_5} (R := S) ((constantCoeff : (a : MvPowerSeries τ S) → S) (a s) : S)) ∧
      ∀ (d : τ →₀ ℕ),
        Set.Finite.{u_1} (α := σ)
          {s : σ | Ne.{u_5 + 1} (α := S) ((coeff d : (a : MvPowerSeries τ S) → S) (a s) : S) (0 : S)}) ↔
    (∀ (s : σ), IsTopologicallyNilpotent (a s)) ∧ Filter.Tendsto a Filter.cofinite (nhds 0)
simp_rw₂ :
  ((∀ (s : σ), IsNilpotent.{u_5} (R := S) ((constantCoeff : (a : MvPowerSeries τ S) → S) (a s) : S)) ∧
      ∀ (d : τ →₀ ℕ),
        Set.Finite.{u_1} (α := σ)
          {s : σ | Ne.{u_5 + 1} (α := S) ((coeff d : (a : MvPowerSeries τ S) → S) (a s) : S) (0 : S)}) ↔
    (∀ (s : σ), IsTopologicallyNilpotent (a s)) ∧
      ∀ (d : τ →₀ ℕ),
        Set.Finite.{u_1} (α := σ)
          {s : σ | Ne.{u_5 + 1} (α := S) ((coeff d : (a : MvPowerSeries τ S) → S) (a s) : S) (0 : S)}
⊢ HasSubst a ↔ HasEval a

Tactic:
simp_rw [hasSubst_def, hasEval_def, coeff_zero_iff,
    isTopologicallyNilpotent_iff_constantCoeff_isNilpotent]

Premises used: MvPowerSeries.hasSubst_def, MvPowerSeries.WithPiTopology.isTopologicallyNilpotent_iff_constantCoeff_isNilpotent, MvPowerSeries.hasEval_def, MvPowerSeries.coeff_zero_iff
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
τ : Type u_4
S : Type u_5
inst : CommRing S
a : σ → MvPowerSeries τ S
inst_1 : TopologicalSpace S
ha : HasSubst a
⊢ HasEval a

Tactic:
HasEval.mono (instTopologicalSpace_mono τ bot_le) <|
  (@hasSubst_iff_hasEval_of_discreteTopology σ τ _ _ a ⊥ (@DiscreteTopology.mk S ⊥ rfl)).mp ha

Premises used: MvPowerSeries.HasEval.mono, MvPowerSeries.hasSubst_iff_hasEval_of_discreteTopology, Iff.mp, MvPowerSeries.WithPiTopology.instTopologicalSpace_mono, bot_le
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
τ : Type u_4
S : Type u_5
inst : CommRing S
this : UniformSpace S := ⊥
⊢ HasSubst.{u_1, u_4, u_5} (τ := τ) (S := S) fun (x : σ) ↦ 0

Tactic:
simpa [hasSubst_iff_hasEval_of_discreteTopology] using HasEval.zero

Premises used: MvPowerSeries.HasEval.zero, MvPowerSeries.hasSubst_iff_hasEval_of_discreteTopology
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
τ : Type u_4
S : Type u_5
inst : CommRing S
a b : σ → MvPowerSeries τ S
ha : HasSubst a
hb : HasSubst b
this : UniformSpace S := ⊥
rw : ∀ (hb : HasEval b) (ha : HasEval a), HasEval (a + b)
⊢ HasSubst (a + b)

Tactic:
rw [hasSubst_iff_hasEval_of_discreteTopology] at ha hb ⊢

Premises used: MvPowerSeries.hasSubst_iff_hasEval_of_discreteTopology
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
τ : Type u_4
S : Type u_5
inst : CommRing S
a b : σ → MvPowerSeries τ S
this : UniformSpace S := ⊥
hb : HasEval b
ha : HasEval a
⊢ HasEval (a + b)

Tactic:
ha.add hb

Premises used: MvPowerSeries.HasEval.add
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
τ : Type u_4
S : Type u_5
inst : CommRing S
a b : σ → MvPowerSeries τ S
this : UniformSpace S := ⊥
hb : HasEval b
ha : HasEval a
⊢ HasEval (a + b)

Tactic:
exact ha.add hb

Premises used: MvPowerSeries.HasEval.add
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
τ : Type u_4
S : Type u_5
inst : CommRing S
b a : σ → MvPowerSeries τ S
ha : HasSubst a
this : UniformSpace S := ⊥
rw : ∀ (ha : HasEval a), HasEval (b * a)
⊢ HasSubst (b * a)

Tactic:
rw [hasSubst_iff_hasEval_of_discreteTopology] at ha ⊢

Premises used: MvPowerSeries.hasSubst_iff_hasEval_of_discreteTopology
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
τ : Type u_4
S : Type u_5
inst : CommRing S
b a : σ → MvPowerSeries τ S
this : UniformSpace S := ⊥
ha : HasEval a
⊢ HasEval (b * a)

Tactic:
ha.mul_left b

Premises used: MvPowerSeries.HasEval.mul_left
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
τ : Type u_4
S : Type u_5
inst : CommRing S
b a : σ → MvPowerSeries τ S
this : UniformSpace S := ⊥
ha : HasEval a
⊢ HasEval (b * a)

Tactic:
exact ha.mul_left b

Premises used: MvPowerSeries.HasEval.mul_left
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
τ : Type u_4
S : Type u_5
inst : CommRing S
b a : σ → MvPowerSeries τ S
ha : HasSubst a
⊢ HasSubst (a * b)

Tactic:
mul_comm a b ▸ ha.mul_left b

Premises used: Eq.rec, mul_comm, Eq.symm, MvPowerSeries.HasSubst.mul_left
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
τ : Type u_4
S : Type u_5
inst : CommRing S
r : MvPowerSeries τ S
a : σ → MvPowerSeries τ S
ha : HasSubst a
⊢ HasSubst (r • a)

Tactic:
ha.mul_left _

Premises used: MvPowerSeries.HasSubst.mul_left
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
S : Type u_5
inst : CommRing S
this : UniformSpace S := ⊥
⊢ HasSubst.{u_1, u_1, u_5} (τ := σ) (S := S) fun (s : σ) ↦ X s

Tactic:
simpa [hasSubst_iff_hasEval_of_discreteTopology] using HasEval.X

Premises used: MvPowerSeries.hasSubst_iff_hasEval_of_discreteTopology, MvPowerSeries.HasEval.X
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
τ : Type u_4
S : Type u_5
inst_1 : CommRing S
a : σ → MvPowerSeries τ R
ha : HasSubst a
h : R →+* S
d : τ →₀ ℕ
⊢ Subset.{u_1} (α := Set σ)
    {s : σ |
      Ne.{u_5 + 1} (α := S)
        ((coeff d : (a : MvPowerSeries τ S) → S)
            ((map h : (a : MvPowerSeries τ R) → MvPowerSeries τ S) (a s) : MvPowerSeries τ S) :
          S)
        (0 : S)}
    {s : σ | Ne.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries τ R) → R) (a s) : R) (0 : R)}

Tactic:
grind [coeff_map]

Premises used: MvPowerSeries.coeff_map
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
a : σ → R
⊢ HasSubst
    (HMul.hMul (α := σ → MvPowerSeries σ R)
      (fun (s : σ) ↦ (algebraMap R (MvPowerSeries σ R) : (a : R) → MvPowerSeries σ R) (a s)) fun (s : σ) ↦ X s)

Tactic:
HasSubst.X.mul_left (fun s ↦ algebraMap R (MvPowerSeries σ R) (a s))

Premises used: Algebra.algebraMap, MvPowerSeries, MvPowerSeries.HasSubst.X, DFunLike.coe, MvPowerSeries.HasSubst.mul_left
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
a : σ → R
h :
  Eq (α := ((s : σ) → MvPowerSeries σ R) → σ → MvPowerSeries σ R) (HSMul.hSMul a)
    (HMul.hMul (α := σ → MvPowerSeries σ R) fun (s : σ) ↦
      (algebraMap R (MvPowerSeries σ R) : (a : R) → MvPowerSeries σ R) (a s))
⊢ HasSubst (HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) a X)

Tactic:
convert! HasSubst.X.mul_left (fun s ↦ algebraMap R (MvPowerSeries σ R) (a s))

Premises used: Algebra.algebraMap, MvPowerSeries, MvPowerSeries.HasSubst.X, DFunLike.coe, MvPowerSeries.HasSubst.mul_left
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
a : σ → R
⊢ Eq (α := ((s : σ) → MvPowerSeries σ R) → σ → MvPowerSeries σ R) (HSMul.hSMul a)
    (HMul.hMul (α := σ → MvPowerSeries σ R) fun (s : σ) ↦
      (algebraMap R (MvPowerSeries σ R) : (a : R) → MvPowerSeries σ R) (a s))

Tactic:
simp [funext_iff, algebra_compatible_smul (MvPowerSeries σ R)]

Premises used: algebra_compatible_smul, funext_iff, MvPowerSeries
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
τ : Type u_4
S : Type u_5
inst : CommRing S
inst_1 : Finite σ
a : σ → MvPowerSeries τ S
ha : ∀ (s : σ), Eq.{u_5 + 1} (α := S) ((constantCoeff : (a : MvPowerSeries τ S) → S) (a s) : S) (0 : S)
s : σ
⊢ IsNilpotent.{u_5} (R := S) ((constantCoeff : (a : MvPowerSeries τ S) → S) (a s) : S)

Tactic:
simp only [ha s, IsNilpotent.zero]

Premises used: IsNilpotent.zero
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
i j : σ
⊢ ∀ (s : Fin (Nat.succ 0).succ),
    Eq.{u_3 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) (![X i, X j] s) : R) (0 : R)

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
τ : Type u_4
S : Type u_5
inst : CommRing S
n : ℕ
hn : n ≠ 0
a : σ → MvPowerSeries τ S
h : HasSubst a
⊢ 0 < n

Tactic:
lia
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
S : Type u_5
inst : CommRing S
n : ℕ
hn : n ≠ 0
⊢ n ≠ 0

Tactic:
lia
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
τ : Type u_4
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : UniformSpace R
inst_4 : DiscreteUniformity R
inst_5 : UniformSpace S
inst_6 : DiscreteUniformity S
h :
  ∀ (x : σ → MvPowerSeries τ S) (x_1 : MvPowerSeries σ R) (n : τ →₀ ℕ),
    Eq.{u_5 + 1} (α := S) ((coeff n : (a : MvPowerSeries τ S) → S) (subst x x_1) : S)
      ((coeff n : (a : MvPowerSeries τ S) → S) (eval₂ (algebraMap R (MvPowerSeries τ S)) x x_1) : S)
⊢ Eq (α := (a : σ → MvPowerSeries τ S) → (f : MvPowerSeries σ R) → MvPowerSeries τ S) subst
    (eval₂ (algebraMap R (MvPowerSeries τ S)))

Tactic:
ext
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
τ : Type u_4
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : UniformSpace R
inst_4 : DiscreteUniformity R
inst_5 : UniformSpace S
inst_6 : DiscreteUniformity S
x : σ → MvPowerSeries τ S
x_1 : MvPowerSeries σ R
n : τ →₀ ℕ
⊢ Eq.{u_5 + 1} (α := S) ((coeff n : (a : MvPowerSeries τ S) → S) (subst x x_1) : S)
    ((coeff n : (a : MvPowerSeries τ S) → S) (eval₂ (algebraMap R (MvPowerSeries τ S)) x x_1) : S)

Tactic:
simp +instances [subst, DiscreteUniformity.eq_bot]

Premises used: MvPowerSeries.subst, DiscreteUniformity.eq_bot
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
τ : Type u_4
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
a : σ → MvPowerSeries τ S
p : MvPolynomial σ R
this_1 : UniformSpace R := ⊥
this : UniformSpace S := ⊥
rw :
  eval₂ (algebraMap R (MvPowerSeries τ S)) a (↑p : MvPowerSeries σ R) =
    ((MvPolynomial.aeval (R := R) a : MvPolynomial σ R →ₐ[R] MvPowerSeries τ S) :
        (a : MvPolynomial σ R) → MvPowerSeries τ S)
      p
rw₁ :
  MvPolynomial.eval₂ (algebraMap R (MvPowerSeries τ S)) a p =
    ((MvPolynomial.aeval (R := R) a : MvPolynomial σ R →ₐ[R] MvPowerSeries τ S) :
        (a : MvPolynomial σ R) → MvPowerSeries τ S)
      p
rw₂ rw₃ :
  MvPolynomial.eval₂ (algebraMap R (MvPowerSeries τ S)) a p = MvPolynomial.eval₂ (algebraMap R (MvPowerSeries τ S)) a p
⊢ subst a (↑p : MvPowerSeries σ R) =
    ((MvPolynomial.aeval (R := R) a : MvPolynomial σ R →ₐ[R] MvPowerSeries τ S) :
        (a : MvPolynomial σ R) → MvPowerSeries τ S)
      p

Tactic:
rw [subst_eq_eval₂, eval₂_coe, MvPolynomial.aeval_def]

Premises used: MvPowerSeries.eval₂_coe, MvPowerSeries.subst_eq_eval₂, MvPolynomial.aeval_def
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
τ : Type u_4
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
a : σ → MvPowerSeries τ S
inst_3 : UniformSpace R
inst_4 : DiscreteUniformity R
inst_5 : UniformSpace S
inst_6 : DiscreteUniformity S
ha : HasSubst a
simp :
  (⇑(aeval (σ := σ) (R := R) (S := MvPowerSeries τ S) (a := a) ⋯ : MvPowerSeries σ R →ₐ[R] MvPowerSeries τ S) :
      (a : MvPowerSeries σ R) → MvPowerSeries τ S) =
    eval₂ (algebraMap R (MvPowerSeries τ S)) a
⊢ Eq (α := (a : MvPowerSeries σ R) → MvPowerSeries τ S)
    (⇑(substAlgHom ha) : (a : MvPowerSeries σ R) → MvPowerSeries τ S)
    (⇑(aeval (σ := σ) (R := R) (S := MvPowerSeries τ S) (a := a) ⋯ : MvPowerSeries σ R →ₐ[R] MvPowerSeries τ S) :
      (a : MvPowerSeries σ R) → MvPowerSeries τ S)

Tactic:
simp only [substAlgHom, coe_aeval ha.hasEval]

Premises used: MvPowerSeries.substAlgHom, MvPowerSeries.coe_aeval, MvPowerSeries.HasSubst.hasEval
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
τ : Type u_4
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
a : σ → MvPowerSeries τ S
inst_3 : UniformSpace R
inst_4 : DiscreteUniformity R
inst_5 : UniformSpace S
inst_6 : DiscreteUniformity S
ha : HasSubst a
⊢ (⇑(aeval (σ := σ) (R := R) (S := MvPowerSeries τ S) (a := a) ⋯ : MvPowerSeries σ R →ₐ[R] MvPowerSeries τ S) :
      (a : MvPowerSeries σ R) → MvPowerSeries τ S) =
    eval₂ (algebraMap R (MvPowerSeries τ S)) a

Tactic:
coe_aeval (R := R) (hasSubst_iff_hasEval_of_discreteTopology.mp ha)

Premises used: MvPowerSeries.hasSubst_iff_hasEval_of_discreteTopology, MvPowerSeries.coe_aeval, Iff.mp
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
τ : Type u_4
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
a : σ → MvPowerSeries τ S
inst_3 : UniformSpace R
inst_4 : DiscreteUniformity R
inst_5 : UniformSpace S
inst_6 : DiscreteUniformity S
ha : HasSubst a
h : ⊥ = inst_3
h₁ : ⊥ = inst_5
⊢ (⇑(aeval (σ := σ) (R := R) (S := MvPowerSeries τ S) (a := a) ⋯ : MvPowerSeries σ R →ₐ[R] MvPowerSeries τ S) :
      (a : MvPowerSeries σ R) → MvPowerSeries τ S) =
    eval₂ (algebraMap R (MvPowerSeries τ S)) a

Tactic:
convert! coe_aeval (R := R) (hasSubst_iff_hasEval_of_discreteTopology.mp ha)

Premises used: MvPowerSeries.hasSubst_iff_hasEval_of_discreteTopology, MvPowerSeries.coe_aeval, Iff.mp
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
τ : Type u_4
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
a : σ → MvPowerSeries τ S
inst_3 : UniformSpace R
inst_4 : DiscreteUniformity R
inst_5 : UniformSpace S
inst_6 : DiscreteUniformity S
ha : HasSubst a
⊢ ⊥ = inst_3

Tactic:
DiscreteUniformity.eq_bot.symm

Premises used: DiscreteUniformity.eq_bot, Eq.symm
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
τ : Type u_4
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
a : σ → MvPowerSeries τ S
inst_3 : UniformSpace R
inst_4 : DiscreteUniformity R
inst_5 : UniformSpace S
inst_6 : DiscreteUniformity S
ha : HasSubst a
⊢ ⊥ = inst_3

Tactic:
exact DiscreteUniformity.eq_bot.symm

Premises used: DiscreteUniformity.eq_bot, Eq.symm
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
τ : Type u_4
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
a : σ → MvPowerSeries τ S
inst_3 : UniformSpace R
inst_4 : DiscreteUniformity R
inst_5 : UniformSpace S
inst_6 : DiscreteUniformity S
ha : HasSubst a
⊢ ⊥ = inst_5

Tactic:
DiscreteUniformity.eq_bot.symm

Premises used: DiscreteUniformity.eq_bot, Eq.symm