awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
T : Type u_6
inst_3 : CommRing T
inst_4 : UniformSpace T
inst_5 : T2Space T
inst_6 : CompleteSpace T
inst_7 : IsUniformAddGroup T
inst_8 : IsTopologicalRing T
inst_9 : IsLinearTopology T T
inst_10 : Algebra R T
ε : MvPowerSeries τ S →ₐ[R] T
inst_11 : UniformSpace R
inst_12 : DiscreteUniformity R
inst_13 : UniformSpace S
inst_14 : DiscreteUniformity S
ha : HasSubst a
hε : Continuous (X := MvPowerSeries τ S) (Y := T) (⇑ε : (a : MvPowerSeries τ S) → T)
rw :
  Eq (α := MvPowerSeries σ R → T) ((⇑ε : (a : MvPowerSeries τ S) → T) ∘ subst a)
    (⇑(ε.comp (substAlgHom ha)) : (a : MvPowerSeries σ R) → T)
rw₁ :
  Eq (α := MvPowerSeries σ R → T) ((⇑ε : (a : MvPowerSeries τ S) → T) ∘ subst a)
    (Function.comp (β := MvPowerSeries τ S) (⇑ε : (a : MvPowerSeries τ S) → T)
      (⇑(substAlgHom ha) : (a : MvPowerSeries σ R) → MvPowerSeries τ S))
rw₂ rw₃ :
  Eq (α := MvPowerSeries σ R → T) ((⇑ε : (a : MvPowerSeries τ S) → T) ∘ subst a)
    ((⇑ε : (a : MvPowerSeries τ S) → T) ∘ subst a)
⊢ Eq (α := MvPowerSeries σ R → T) ((⇑ε : (a : MvPowerSeries τ S) → T) ∘ subst a)
    (⇑(aeval (a := fun (s : σ) ↦ (ε.toRingHom : (a : MvPowerSeries τ S) → T) (a s)) ⋯) : (a : MvPowerSeries σ R) → T)

Tactic:
rw [← comp_substAlgHom ha hε, AlgHom.coe_comp, coe_substAlgHom]

Premises used: MvPowerSeries.coe_substAlgHom, AlgHom.coe_comp, MvPowerSeries.comp_substAlgHom
-- 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
T : Type u_6
inst_3 : CommRing T
inst_4 : UniformSpace T
inst_5 : T2Space T
inst_6 : CompleteSpace T
inst_7 : IsUniformAddGroup T
inst_8 : IsTopologicalRing T
inst_9 : IsLinearTopology T T
inst_10 : Algebra R T
ε : MvPowerSeries τ S →ₐ[R] T
inst_11 : UniformSpace R
inst_12 : DiscreteUniformity R
inst_13 : UniformSpace S
inst_14 : DiscreteUniformity S
ha : HasSubst a
hε : Continuous (X := MvPowerSeries τ S) (Y := T) (⇑ε : (a : MvPowerSeries τ S) → T)
f : MvPowerSeries σ R
⊢ Eq.{u_6 + 1} (α := T) ((ε : (a : MvPowerSeries τ S) → T) (subst a f) : T)
    ((aeval (a := fun (s : σ) ↦ (ε.toRingHom : (a : MvPowerSeries τ S) → T) (a s)) ⋯ : (a : MvPowerSeries σ R) → T) f :
      T)

Tactic:
congr_fun (comp_subst ha hε) f

Premises used: MvPowerSeries.comp_subst, congr_fun
-- 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
T : Type u_6
inst_3 : CommRing T
inst_4 : UniformSpace T
inst_5 : T2Space T
inst_6 : CompleteSpace T
inst_7 : IsUniformAddGroup T
inst_8 : IsTopologicalRing T
inst_9 : IsLinearTopology T T
inst_10 : Algebra R T
inst_11 : Algebra S T
inst_12 : IsScalarTower R S T
inst_13 : UniformSpace R
inst_14 : DiscreteUniformity R
inst_15 : UniformSpace S
inst_16 : DiscreteUniformity S
ha : HasSubst a
b : τ → T
hb : HasEval b
f : MvPowerSeries σ R
ε : MvPowerSeries τ S →ₐ[R] T := AlgHom.restrictScalars R (aeval hb)
⊢ Continuous (X := MvPowerSeries τ S) (Y := T) (⇑ε : (a : MvPowerSeries τ S) → T)

Tactic:
have hε : Continuous ε := continuous_aeval hb
-- 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
T : Type u_6
inst_3 : CommRing T
inst_4 : UniformSpace T
inst_5 : T2Space T
inst_6 : CompleteSpace T
inst_7 : IsUniformAddGroup T
inst_8 : IsTopologicalRing T
inst_9 : IsLinearTopology T T
inst_10 : Algebra R T
inst_11 : Algebra S T
inst_12 : IsScalarTower R S T
inst_13 : UniformSpace R
inst_14 : DiscreteUniformity R
inst_15 : UniformSpace S
inst_16 : DiscreteUniformity S
ha : HasSubst a
b : τ → T
hb : HasEval b
f : MvPowerSeries σ R
ε : MvPowerSeries τ S →ₐ[R] T := AlgHom.restrictScalars R (aeval hb)
hε : Continuous (X := MvPowerSeries τ S) (Y := T) (⇑ε : (a : MvPowerSeries τ S) → T)
⊢ eval₂ (algebraMap S T) b (subst a f) = eval₂ (algebraMap R T) (fun (s : σ) ↦ eval₂ (algebraMap S T) b (a s)) f

Tactic:
simpa only [AlgHom.coe_restrictScalars', AlgHom.toRingHom_eq_coe,
    AlgHom.coe_restrictScalars, RingHom.coe_coe, ε, coe_aeval]
    using comp_subst_apply ha hε f

Premises used: RingHom.coe_coe, AlgHom.coe_restrictScalars, MvPowerSeries.comp_subst_apply, AlgHom.coe_restrictScalars', AlgHom.toRingHom_eq_coe, MvPowerSeries.coe_aeval
-- 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
ha : HasSubst a
f : MvPowerSeries σ R
hf : IsNilpotent.{u_3} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
rw :
  IsNilpotent.{u_5} (R := S)
    (∑ᶠ (d : σ →₀ ℕ),
      HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
        ((constantCoeff : (a : MvPowerSeries τ S) → S) (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e) : S))
⊢ IsNilpotent.{u_5} (R := S)
    ((constantCoeff : (a : MvPowerSeries τ S) → S)
        ((substAlgHom ha : (a : MvPowerSeries σ R) → MvPowerSeries τ S) f : MvPowerSeries τ S) :
      S)

Tactic:
rw [coe_substAlgHom, constantCoeff_subst ha]

Premises used: MvPowerSeries.constantCoeff_subst, MvPowerSeries.coe_substAlgHom
-- 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
ha : HasSubst a
f : MvPowerSeries σ R
hf : IsNilpotent.{u_3} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
hf₁ :
  ∀ (b : σ →₀ ℕ),
    IsNilpotent
      (HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff b : (a : MvPowerSeries σ R) → R) f : R)
        ((constantCoeff : (a : MvPowerSeries τ S) → S) (b.prod fun (s : σ) (e : ℕ) ↦ a s ^ e) : S))
⊢ IsNilpotent.{u_5} (R := S)
    (∑ᶠ (d : σ →₀ ℕ),
      HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
        ((constantCoeff : (a : MvPowerSeries τ S) → S) (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e) : S))

Tactic:
apply isNilpotent_finsum

Premises used: isNilpotent_finsum
-- 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
ha : HasSubst a
f : MvPowerSeries σ R
hf : IsNilpotent.{u_3} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
d : σ →₀ ℕ
pos :
  ∀ (hd : d = 0),
    IsNilpotent
      (HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
        ((constantCoeff : (a : MvPowerSeries τ S) → S) (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e) : S))
neg :
  ∀ (hd : ¬d = 0),
    IsNilpotent
      (HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
        ((constantCoeff : (a : MvPowerSeries τ S) → S) (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e) : S))
⊢ IsNilpotent
    (HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
      ((constantCoeff : (a : MvPowerSeries τ S) → S) (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e) : S))

Tactic:
by_cases hd : d = 0
-- 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
ha : HasSubst a
f : MvPowerSeries σ R
hf : IsNilpotent.{u_3} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
d : σ →₀ ℕ
hd : d = 0
pos :
  IsNilpotent
    (HSMul.hSMul (α := S) (β := S)
      ((constantCoeff : (a : MvPowerSeries τ S) → S) (Finsupp.prod 0 fun (s : σ) (e : ℕ) ↦ a s ^ e) : S)
      ((algebraMap R S : (a : R) → S) ((coeff 0 : (a : MvPowerSeries σ R) → R) f : R) : S))
⊢ IsNilpotent
    (HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
      ((constantCoeff : (a : MvPowerSeries τ S) → S) (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e) : S))

Tactic:
rw [← algebraMap_smul S, smul_eq_mul, mul_comm, ← smul_eq_mul, hd]

Premises used: algebraMap_smul, mul_comm, smul_eq_mul
-- 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
ha : HasSubst a
f : MvPowerSeries σ R
hf : IsNilpotent.{u_3} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
d : σ →₀ ℕ
hd : d = 0
pos : IsNilpotent.{u_5} (R := S) ((algebraMap R S : (a : R) → S) ((coeff 0 : (a : MvPowerSeries σ R) → R) f : R) : S)
⊢ IsNilpotent
    (HSMul.hSMul (α := S) (β := S)
      ((constantCoeff : (a : MvPowerSeries τ S) → S) (Finsupp.prod 0 fun (s : σ) (e : ℕ) ↦ a s ^ e) : S)
      ((algebraMap R S : (a : R) → S) ((coeff 0 : (a : MvPowerSeries σ R) → R) f : R) : S))

Tactic:
apply IsNilpotent.smul

Premises used: IsNilpotent.smul
-- 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
ha : HasSubst a
f : MvPowerSeries σ R
hf : IsNilpotent.{u_3} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
d : σ →₀ ℕ
hd : d = 0
⊢ IsNilpotent.{u_5} (R := S) ((algebraMap R S : (a : R) → S) ((coeff 0 : (a : MvPowerSeries σ R) → R) f : R) : S)

Tactic:
simpa using IsNilpotent.map hf (algebraMap R S)

Premises used: Algebra.algebraMap, IsNilpotent.map
-- 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
ha : HasSubst a
f : MvPowerSeries σ R
hf : IsNilpotent.{u_3} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
d : σ →₀ ℕ
hd : ¬d = 0
neg :
  IsNilpotent.{u_5} (R := S) ((constantCoeff : (a : MvPowerSeries τ S) → S) (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e) : S)
⊢ IsNilpotent
    (HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
      ((constantCoeff : (a : MvPowerSeries τ S) → S) (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e) : S))

Tactic:
apply IsNilpotent.smul

Premises used: IsNilpotent.smul
-- 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
ha : HasSubst a
f : MvPowerSeries σ R
hf : IsNilpotent.{u_3} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
d : σ →₀ ℕ
hd : ¬d = 0
⊢ ∃ (a : σ), Ne (α := ℕ) ((d : (a : σ) → ℕ) a : ℕ) ((0 : (a : σ) → ℕ) a : ℕ)

Tactic:
rw [← ne_eq, Finsupp.ne_iff] at hd

Premises used: ne_eq, Finsupp.ne_iff
-- 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
ha : HasSubst a
f : MvPowerSeries σ R
hf : IsNilpotent.{u_3} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
d : σ →₀ ℕ
hd : ∃ (a : σ), Ne (α := ℕ) ((d : (a : σ) → ℕ) a : ℕ) ((0 : (a : σ) → ℕ) a : ℕ)
neg :
  ∀ (t : σ) (hs : Ne (α := ℕ) ((d : (a : σ) → ℕ) t : ℕ) ((0 : (a : σ) → ℕ) t : ℕ)),
    IsNilpotent.{u_5} (R := S)
      ((constantCoeff : (a : MvPowerSeries τ S) → S) (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e) : S)
⊢ IsNilpotent.{u_5} (R := S) ((constantCoeff : (a : MvPowerSeries τ S) → S) (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e) : S)

Tactic:
obtain ⟨t, hs⟩ := hd
-- 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
ha : HasSubst a
f : MvPowerSeries σ R
hf : IsNilpotent.{u_3} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
d : σ →₀ ℕ
t : σ
hs : Ne (α := ℕ) ((d : (a : σ) → ℕ) t : ℕ) ((0 : (a : σ) → ℕ) t : ℕ)
neg :
  IsNilpotent
    (HSMul.hSMul (α := S) (β := S)
      ((constantCoeff : (a : MvPowerSeries τ S) → S)
          ((Finsupp.filter (fun (a : σ) ↦ ¬a = t) d).prod fun (s : σ) (e : ℕ) ↦ a s ^ e) :
        S)
      ((constantCoeff : (a : MvPowerSeries τ S) → S)
          ((Finsupp.filter (fun (i : σ) ↦ i = t) d).prod fun (s : σ) (e : ℕ) ↦ a s ^ e) :
        S))
⊢ IsNilpotent.{u_5} (R := S) ((constantCoeff : (a : MvPowerSeries τ S) → S) (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e) : S)

Tactic:
rw [← Finsupp.prod_filter_mul_prod_filter_not (fun i ↦ i = t), map_mul,
      mul_comm, ← smul_eq_mul]

Premises used: Finsupp.prod_filter_mul_prod_filter_not, map_mul, mul_comm, smul_eq_mul, Eq
-- 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
ha : HasSubst a
f : MvPowerSeries σ R
hf : IsNilpotent.{u_3} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
d : σ →₀ ℕ
t : σ
hs : Ne (α := ℕ) ((d : (a : σ) → ℕ) t : ℕ) ((0 : (a : σ) → ℕ) t : ℕ)
neg :
  IsNilpotent.{u_5} (R := S)
    ((constantCoeff : (a : MvPowerSeries τ S) → S)
        ((Finsupp.filter (fun (i : σ) ↦ i = t) d).prod fun (s : σ) (e : ℕ) ↦ a s ^ e) :
      S)
⊢ IsNilpotent
    (HSMul.hSMul (α := S) (β := S)
      ((constantCoeff : (a : MvPowerSeries τ S) → S)
          ((Finsupp.filter (fun (a : σ) ↦ ¬a = t) d).prod fun (s : σ) (e : ℕ) ↦ a s ^ e) :
        S)
      ((constantCoeff : (a : MvPowerSeries τ S) → S)
          ((Finsupp.filter (fun (i : σ) ↦ i = t) d).prod fun (s : σ) (e : ℕ) ↦ a s ^ e) :
        S))

Tactic:
apply IsNilpotent.smul

Premises used: IsNilpotent.smul
-- 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
ha : HasSubst a
f : MvPowerSeries σ R
hf : IsNilpotent.{u_3} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
d : σ →₀ ℕ
t : σ
hs : Ne (α := ℕ) ((d : (a : σ) → ℕ) t : ℕ) ((0 : (a : σ) → ℕ) t : ℕ)
neg :
  IsNilpotent.{u_5} (R := S)
    ((constantCoeff : (a : MvPowerSeries τ S) → S)
        (HPow.hPow (β := ℕ) (a t) ((Finsupp.filter (fun (i : σ) ↦ i = t) d : (a : σ) → ℕ) t : ℕ)) :
      S)
neg₁ :
  ∀ (b : σ),
    Ne (α := ℕ) ((Finsupp.filter (fun (i : σ) ↦ i = t) d : (a : σ) → ℕ) b : ℕ) (0 : ℕ) →
      b ≠ t → HPow.hPow (β := ℕ) (a b) ((Finsupp.filter (fun (i : σ) ↦ i = t) d : (a : σ) → ℕ) b : ℕ) = 1
neg₂ :
  Eq (α := ℕ) ((Finsupp.filter (fun (i : σ) ↦ i = t) d : (a : σ) → ℕ) t : ℕ) (0 : ℕ) → HPow.hPow (β := ℕ) (a t) 0 = 1
⊢ IsNilpotent.{u_5} (R := S)
    ((constantCoeff : (a : MvPowerSeries τ S) → S)
        ((Finsupp.filter (fun (i : σ) ↦ i = t) d).prod fun (s : σ) (e : ℕ) ↦ a s ^ e) :
      S)

Tactic:
rw [Finsupp.prod_eq_single t]

Premises used: Finsupp.prod_eq_single
-- 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
ha : HasSubst a
f : MvPowerSeries σ R
hf : IsNilpotent.{u_3} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
d : σ →₀ ℕ
t : σ
hs : Ne (α := ℕ) ((d : (a : σ) → ℕ) t : ℕ) ((0 : (a : σ) → ℕ) t : ℕ)
⊢ IsNilpotent.{u_5} (R := S)
    ((constantCoeff : (a : MvPowerSeries τ S) → S)
        (HPow.hPow (β := ℕ) (a t) ((Finsupp.filter (fun (i : σ) ↦ i = t) d : (a : σ) → ℕ) t : ℕ)) :
      S)

Tactic:
simpa using IsNilpotent.pow_of_pos (ha.const_coeff t) hs

Premises used: MvPowerSeries.HasSubst.const_coeff, IsNilpotent.pow_of_pos
-- 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
ha : HasSubst a
f : MvPowerSeries σ R
hf : IsNilpotent.{u_3} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
d : σ →₀ ℕ
t : σ
hs : Ne (α := ℕ) ((d : (a : σ) → ℕ) t : ℕ) ((0 : (a : σ) → ℕ) t : ℕ)
t' : σ
htt' : Ne (α := ℕ) ((Finsupp.filter (fun (i : σ) ↦ i = t) d : (a : σ) → ℕ) t' : ℕ) (0 : ℕ)
ht' : t' ≠ t
⊢ HPow.hPow (β := ℕ) (a t') ((Finsupp.filter (fun (i : σ) ↦ i = t) d : (a : σ) → ℕ) t' : ℕ) = 1

Tactic:
simp [ht'] at htt'
-- 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
ha : HasSubst a
f : MvPowerSeries σ R
hf : IsNilpotent.{u_3} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
d : σ →₀ ℕ
t : σ
hs : Ne (α := ℕ) ((d : (a : σ) → ℕ) t : ℕ) ((0 : (a : σ) → ℕ) t : ℕ)
h : Eq (α := ℕ) ((Finsupp.filter (fun (i : σ) ↦ i = t) d : (a : σ) → ℕ) t : ℕ) (0 : ℕ)
rw rw₁ : Eq (α := MvPowerSeries τ S) 1 1
⊢ HPow.hPow (β := ℕ) (a t) 0 = 1

Tactic:
rw [pow_zero]

Premises used: pow_zero
-- 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
ha : HasSubst a
f : MvPowerSeries σ R
hf : IsNilpotent.{u_3} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
d : σ →₀ ℕ
t : σ
hs : Ne (α := ℕ) ((d : (a : σ) → ℕ) t : ℕ) ((0 : (a : σ) → ℕ) t : ℕ)
⊢ Eq (α := ℕ) ((Finsupp.filter (fun (i : σ) ↦ i = t) d : (a : σ) → ℕ) t : ℕ) (0 : ℕ) → HPow.hPow (β := ℕ) (a t) 0 = 1

Tactic:
exact fun _ ↦ by rw [pow_zero]
-- 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
ha : HasSubst a
f : MvPowerSeries σ R
hf : IsNilpotent.{u_3} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
rw : IsNilpotent.{u_5} (R := S) ((constantCoeff : (a : MvPowerSeries τ S) → S) (subst a f) : S)
rw₁ rw₂ rw₃ :
  IsNilpotent.{u_5} (R := S)
    (∑ᶠ (d : σ →₀ ℕ),
      HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
        ((constantCoeff : (a : MvPowerSeries τ S) → S) (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e) : S))
hf₁ hf₂ :
  ∀ (d : σ →₀ ℕ),
    IsNilpotent
      (HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
        ((constantCoeff : (a : MvPowerSeries τ S) → S) (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e) : S))
pos :
  ∀ (d : σ →₀ ℕ) (hd : d = 0),
    IsNilpotent
      (HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
        ((constantCoeff : (a : MvPowerSeries τ S) → S) (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e) : S))
neg neg₁ :
  ∀ (d : σ →₀ ℕ) (hd : ¬d = 0),
    IsNilpotent
      (HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
        ((constantCoeff : (a : MvPowerSeries τ S) → S) (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e) : S))
⊢ IsNilpotent.{u_5} (R := S)
    ((constantCoeff : (a : MvPowerSeries τ S) → S)
        ((substAlgHom ha : (a : MvPowerSeries σ R) → MvPowerSeries τ S) f : MvPowerSeries τ S) :
      S)

Tactic:
classical
  rw [coe_substAlgHom, constantCoeff_subst ha]
  apply isNilpotent_finsum
  intro d
  by_cases hd : d = 0
  · rw [← algebraMap_smul S, smul_eq_mul, mul_comm, ← smul_eq_mul, hd]
    apply IsNilpotent.smul
    simpa using IsNilpotent.map hf (algebraMap R S)
  · apply IsNilpotent.smul
    rw [← ne_eq, Finsupp.ne_iff] at hd
    obtain ⟨t, hs⟩ := hd
    rw [← Finsupp.prod_filter_mul_prod_filter_not (fun i ↦ i = t), map_mul,
      mul_comm, ← smul_eq_mul]
    apply IsNilpotent.smul
    rw [Finsupp.prod_eq_single t]
    · simpa using IsNilpotent.pow_of_pos (ha.const_coeff t) hs
    · intro t' htt' ht'
      simp [ht'] at htt'
    · exact fun _ ↦ by rw [pow_zero]

Premises used: MvPowerSeries.constantCoeff_subst, Algebra.algebraMap, MvPowerSeries.coe_substAlgHom, IsNilpotent.smul, algebraMap_smul, ne_eq, IsNilpotent.map, map_mul, mul_comm, smul_eq_mul, isNilpotent_finsum, Finsupp.ne_iff
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
τ : Type u_4
S : Type u_5
inst : CommRing S
a : σ → MvPowerSeries τ S
υ : Type u_7
T : Type u_8
inst_1 : CommRing T
inst_2 : Algebra S T
b : τ → MvPowerSeries υ T
ha : HasSubst a
hb : HasSubst b
this_1 : UniformSpace S := ⊥
this : UniformSpace T := ⊥
rw :
  Filter.Tendsto (β := MvPowerSeries υ T)
    (fun (s : σ) ↦ (substAlgHom hb : (a : MvPowerSeries τ S) → MvPowerSeries υ T) (a s)) Filter.cofinite (nhds 0)
⊢ ∀ (d : υ →₀ ℕ),
    Set.Finite.{u_1} (α := σ)
      {s : σ |
        Ne.{u_8 + 1} (α := T)
          ((coeff d : (a : MvPowerSeries υ T) → T)
              ((substAlgHom hb : (a : MvPowerSeries τ S) → MvPowerSeries υ T) (a s) : MvPowerSeries υ T) :
            T)
          (0 : T)}

Tactic:
rw [← coeff_zero_iff]

Premises used: 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
υ : Type u_7
T : Type u_8
inst_1 : CommRing T
inst_2 : Algebra S T
b : τ → MvPowerSeries υ T
ha : HasSubst a
hb : HasSubst b
this_1 : UniformSpace S := ⊥
this : UniformSpace T := ⊥
apply :
  Filter.Tendsto (α := MvPowerSeries τ S) (β := MvPowerSeries υ T)
    (⇑(substAlgHom hb) : (a : MvPowerSeries τ S) → MvPowerSeries υ T) (nhds 0) (nhds 0)
⊢ Filter.Tendsto (β := MvPowerSeries υ T)
    (fun (s : σ) ↦ (substAlgHom hb : (a : MvPowerSeries τ S) → MvPowerSeries υ T) (a s)) Filter.cofinite (nhds 0)

Tactic:
apply Filter.Tendsto.comp _ (ha.hasEval.tendsto_zero)

Premises used: Filter.Tendsto.comp, MvPowerSeries.HasSubst.hasEval, MvPowerSeries.HasEval.tendsto_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
τ : Type u_4
S : Type u_5
inst : CommRing S
a : σ → MvPowerSeries τ S
υ : Type u_7
T : Type u_8
inst_1 : CommRing T
inst_2 : Algebra S T
b : τ → MvPowerSeries υ T
ha : HasSubst a
hb : HasSubst b
this_1 : UniformSpace S := ⊥
this : UniformSpace T := ⊥
⊢ Filter.Tendsto (α := MvPowerSeries τ S) (β := MvPowerSeries υ T)
    (⇑(substAlgHom hb) : (a : MvPowerSeries τ S) → MvPowerSeries υ T) (nhds 0) (nhds 0)

Tactic:
simpa [← map_zero (substAlgHom (R := S) hb)] using (continuous_subst hb).continuousAt

Premises used: MvPowerSeries.substAlgHom, map_zero, MvPowerSeries.continuous_subst, Continuous.continuousAt
-- 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
υ : Type u_7
T : Type u_8
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
b : τ → MvPowerSeries υ T
ha : HasSubst a
hb : HasSubst b
this_1 : UniformSpace R := ⊥
this_2 : UniformSpace S := ⊥
this : UniformSpace T := ⊥
apply :
  Continuous (X := MvPowerSeries τ S) (Y := MvPowerSeries υ T)
    (⇑(AlgHom.restrictScalars R (substAlgHom hb)) : (a : MvPowerSeries τ S) → MvPowerSeries υ T)
⊢ Eq (α := MvPowerSeries σ R →ₐ[R] MvPowerSeries υ T)
    (AlgHom.comp (AlgHom.restrictScalars R (substAlgHom hb)) (substAlgHom ha))
    (substAlgHom (a := fun (s : σ) ↦ (substAlgHom hb : (a : MvPowerSeries τ S) → MvPowerSeries υ T) (a s)) ⋯)

Tactic:
apply comp_aeval (R := R) (ε := (substAlgHom hb).restrictScalars R) ha.hasEval

Premises used: MvPowerSeries.comp_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
υ : Type u_7
T : Type u_8
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
b : τ → MvPowerSeries υ T
ha : HasSubst a
hb : HasSubst b
this_1 : UniformSpace R := ⊥
this_2 : UniformSpace S := ⊥
this : UniformSpace T := ⊥
⊢ Continuous (X := MvPowerSeries τ S) (Y := MvPowerSeries υ T)
    (⇑(AlgHom.restrictScalars R (substAlgHom hb)) : (a : MvPowerSeries τ S) → MvPowerSeries υ T)

Tactic:
simpa [AlgHom.coe_restrictScalars'] using continuous_subst (R := S) hb

Premises used: MvPowerSeries.continuous_subst, AlgHom.coe_restrictScalars'