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
inst_3 : UniformSpace R
inst_4 : DiscreteUniformity R
inst_5 : UniformSpace S
inst_6 : DiscreteUniformity S
ha : HasSubst a
⊢ ⊥ = inst_5

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
ha : HasSubst a
this_1 : UniformSpace R := ⊥
this : UniformSpace S := ⊥
rw :
  Eq (α := (a : MvPowerSeries σ R) → MvPowerSeries τ S)
    (⇑(aeval (σ := σ) (R := R) (S := MvPowerSeries τ S) (a := a) ⋯ : MvPowerSeries σ R →ₐ[R] MvPowerSeries τ S) :
      (a : MvPowerSeries σ R) → MvPowerSeries τ S)
    (subst a)
rw₁ : eval₂ (algebraMap R (MvPowerSeries τ S)) a = subst a
rw₂ rw₃ : eval₂ (algebraMap R (MvPowerSeries τ S)) a = eval₂ (algebraMap R (MvPowerSeries τ S)) a
⊢ Eq (α := (a : MvPowerSeries σ R) → MvPowerSeries τ S)
    (⇑(substAlgHom ha) : (a : MvPowerSeries σ R) → MvPowerSeries τ S) (subst a)

Tactic:
rw [substAlgHom_eq_aeval, coe_aeval ha.hasEval, subst_eq_eval₂]

Premises used: MvPowerSeries.subst_eq_eval₂, MvPowerSeries.substAlgHom_eq_aeval, MvPowerSeries.coe_aeval, MvPowerSeries.HasSubst.hasEval
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
rw :
  Eq (α := (f : MvPowerSeries σ R) → MvPowerSeries σ R) (⇑(substAlgHom ⋯) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
    id
⊢ Eq (α := (f : MvPowerSeries σ R) → MvPowerSeries σ R) (subst X) id

Tactic:
rw [← coe_substAlgHom HasSubst.X]

Premises used: MvPowerSeries.coe_substAlgHom, MvPowerSeries.HasSubst.X
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
this : UniformSpace R := ⊥
h : ∀ (f : MvPowerSeries σ R), (substAlgHom ⋯ : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f = id f
⊢ Eq (α := (f : MvPowerSeries σ R) → MvPowerSeries σ R) (⇑(substAlgHom ⋯) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
    id

Tactic:
ext1 f
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
this : UniformSpace R := ⊥
f : MvPowerSeries σ R
h :
  ((aeval (σ := σ) (R := R) (S := MvPowerSeries σ R) (a := fun (s : σ) ↦ X s) ⋯ :
          MvPowerSeries σ R →ₐ[R] MvPowerSeries σ R) :
        (a : MvPowerSeries σ R) → MvPowerSeries σ R)
      f =
    id f
⊢ (substAlgHom ⋯ : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f = id f

Tactic:
simp only [substAlgHom_eq_aeval]

Premises used: MvPowerSeries.substAlgHom_eq_aeval
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
this : UniformSpace R := ⊥
f : MvPowerSeries σ R
⊢ Eq (α := MvPowerSeries σ R →ₐ[R] MvPowerSeries σ R)
    (aeval (σ := σ) (R := R) (S := MvPowerSeries σ R) (a := fun (s : σ) ↦
        (AlgHom.toRingHom (AlgHom.id R (MvPowerSeries σ R)) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) (X s)) ⋯ :
      MvPowerSeries σ R →ₐ[R] MvPowerSeries σ R)
    (AlgHom.id R (MvPowerSeries σ R) : MvPowerSeries σ R →ₐ[R] MvPowerSeries σ R)

Tactic:
have := aeval_unique (ε := AlgHom.id R (MvPowerSeries σ R)) continuous_id
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
this_1 : UniformSpace R := ⊥
f : MvPowerSeries σ R
this :
  Eq (α := MvPowerSeries σ R →ₐ[R] MvPowerSeries σ R)
    (aeval (σ := σ) (R := R) (S := MvPowerSeries σ R) (a := fun (s : σ) ↦
        (AlgHom.toRingHom (AlgHom.id R (MvPowerSeries σ R)) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) (X s)) ⋯ :
      MvPowerSeries σ R →ₐ[R] MvPowerSeries σ R)
    (AlgHom.id R (MvPowerSeries σ R) : MvPowerSeries σ R →ₐ[R] MvPowerSeries σ R)
⊢ ∀ (x : MvPowerSeries σ R),
    Eq (α := MvPowerSeries σ R)
      (((aeval (σ := σ) (R := R) (S := MvPowerSeries σ R) (a := fun (s : σ) ↦
                (AlgHom.toRingHom (AlgHom.id R (MvPowerSeries σ R)) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
                  (X s))
                ⋯ :
              MvPowerSeries σ R →ₐ[R] MvPowerSeries σ R) :
            (a : MvPowerSeries σ R) → MvPowerSeries σ R)
          x :
        MvPowerSeries σ R)
      ((AlgHom.id R (MvPowerSeries σ R) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) x : MvPowerSeries σ R)

Tactic:
rw [DFunLike.ext_iff] at this

Premises used: DFunLike.ext_iff
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
this_1 : UniformSpace R := ⊥
f : MvPowerSeries σ R
this :
  ∀ (x : MvPowerSeries σ R),
    Eq (α := MvPowerSeries σ R)
      (((aeval (σ := σ) (R := R) (S := MvPowerSeries σ R) (a := fun (s : σ) ↦
                (AlgHom.toRingHom (AlgHom.id R (MvPowerSeries σ R)) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
                  (X s))
                ⋯ :
              MvPowerSeries σ R →ₐ[R] MvPowerSeries σ R) :
            (a : MvPowerSeries σ R) → MvPowerSeries σ R)
          x :
        MvPowerSeries σ R)
      ((AlgHom.id R (MvPowerSeries σ R) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) x : MvPowerSeries σ R)
⊢ ((aeval (σ := σ) (R := R) (S := MvPowerSeries σ R) (a := fun (s : σ) ↦ X s) ⋯ :
          MvPowerSeries σ R →ₐ[R] MvPowerSeries σ R) :
        (a : MvPowerSeries σ R) → MvPowerSeries σ R)
      f =
    id f

Tactic:
this f

Premises used: Function.update, Pi.single, dite, MvPowerSeries.X
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
this_1 : UniformSpace R := ⊥
f : MvPowerSeries σ R
this :
  ∀ (x : MvPowerSeries σ R),
    Eq (α := MvPowerSeries σ R)
      (((aeval (σ := σ) (R := R) (S := MvPowerSeries σ R) (a := fun (s : σ) ↦
                (AlgHom.toRingHom (AlgHom.id R (MvPowerSeries σ R)) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
                  (X s))
                ⋯ :
              MvPowerSeries σ R →ₐ[R] MvPowerSeries σ R) :
            (a : MvPowerSeries σ R) → MvPowerSeries σ R)
          x :
        MvPowerSeries σ R)
      ((AlgHom.id R (MvPowerSeries σ R) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) x : MvPowerSeries σ R)
⊢ ((aeval (σ := σ) (R := R) (S := MvPowerSeries σ R) (a := fun (s : σ) ↦ X s) ⋯ :
          MvPowerSeries σ R →ₐ[R] MvPowerSeries σ R) :
        (a : MvPowerSeries σ R) → MvPowerSeries σ R)
      f =
    id f

Tactic:
exact this f
-- 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
rw rw₁ : subst a f = subst a f
⊢ (substAlgHom ha : (a : MvPowerSeries σ R) → MvPowerSeries τ S) f = subst a f

Tactic:
rw [coe_substAlgHom]

Premises used: 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 g : MvPowerSeries σ R
⊢ subst a (f + g) = subst a f + subst a g

Tactic:
simp only [← substAlgHom_apply ha, map_add]

Premises used: map_add, MvPowerSeries.substAlgHom_apply
-- 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 g : MvPowerSeries σ R
simp_rw :
  (substAlgHom ha : (a : MvPowerSeries σ R) → MvPowerSeries τ S) (f - g) =
    HSub.hSub (α := MvPowerSeries τ S) (β := MvPowerSeries τ S)
      ((substAlgHom ha : (a : MvPowerSeries σ R) → MvPowerSeries τ S) f : MvPowerSeries τ S)
      ((substAlgHom ha : (a : MvPowerSeries σ R) → MvPowerSeries τ S) g : MvPowerSeries τ S)
⊢ subst a (f - g) = subst a f - subst a g

Tactic:
simp_rw [← substAlgHom_apply ha, map_sub]

Premises used: map_sub, MvPowerSeries.substAlgHom_apply
-- 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 g : MvPowerSeries σ R
⊢ subst a (f * g) = subst a f * subst a g

Tactic:
simp only [← substAlgHom_apply ha, map_mul]

Premises used: map_mul, MvPowerSeries.substAlgHom_apply
-- 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
n : ℕ
⊢ subst a (f ^ n) = subst a f ^ n

Tactic:
simp only [← substAlgHom_apply ha, map_pow]

Premises used: map_pow, MvPowerSeries.substAlgHom_apply
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
A : Type u_2
inst : CommSemiring A
R : Type u_3
inst_1 : CommRing R
inst_2 : Algebra A R
τ : Type u_4
S : Type u_5
inst_3 : CommRing S
inst_4 : Algebra A S
inst_5 : Algebra R S
inst_6 : IsScalarTower A R S
a : σ → MvPowerSeries τ S
ha : HasSubst a
r : A
f : MvPowerSeries σ R
⊢ subst a (r • f) = r • subst a f

Tactic:
simp only [← substAlgHom_apply ha, AlgHom.map_smul_of_tower]

Premises used: AlgHom.map_smul_of_tower, MvPowerSeries.substAlgHom_apply
-- 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
p : MvPolynomial σ R
⊢ Eq (α := MvPowerSeries τ S)
    ((substAlgHom ha : (a : MvPowerSeries σ R) → MvPowerSeries τ S) (↑p : MvPowerSeries σ R) : MvPowerSeries τ S)
    (((MvPolynomial.aeval (R := R) a : MvPolynomial σ R →ₐ[R] MvPowerSeries τ S) :
          (a : MvPolynomial σ R) → MvPowerSeries τ S)
        p :
      MvPowerSeries τ S)

Tactic:
simp [substAlgHom]

Premises used: MvPowerSeries.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
s : σ
rw : (substAlgHom ha : (a : MvPowerSeries σ R) → MvPowerSeries τ S) (↑(MvPolynomial.X s) : MvPowerSeries σ R) = a s
rw₁ :
  ((MvPolynomial.aeval (R := R) a : MvPolynomial σ R →ₐ[R] MvPowerSeries τ S) :
        (a : MvPolynomial σ R) → MvPowerSeries τ S)
      (MvPolynomial.X s) =
    a s
rw₂ rw₃ : a s = a s
⊢ (substAlgHom ha : (a : MvPowerSeries σ R) → MvPowerSeries τ S) (X s) = a s

Tactic:
rw [← MvPolynomial.coe_X, substAlgHom_coe ha, MvPolynomial.aeval_X]

Premises used: MvPolynomial.aeval_X, MvPolynomial.coe_X, MvPowerSeries.substAlgHom_coe
-- 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
e : σ →₀ ℕ
r : R
rw :
  (substAlgHom ha : (a : MvPowerSeries σ R) → MvPowerSeries τ S)
      (↑((MvPolynomial.monomial e : (a : R) → MvPolynomial σ R) r) : MvPowerSeries σ R) =
    HMul.hMul (α := MvPowerSeries τ S) (β := MvPowerSeries τ S)
      ((algebraMap R (MvPowerSeries τ S) : (a : R) → MvPowerSeries τ S) r : MvPowerSeries τ S)
      (e.prod fun (s : σ) (n : ℕ) ↦ a s ^ n : MvPowerSeries τ S)
rw₁ :
  ((MvPolynomial.aeval (R := R) a : MvPolynomial σ R →ₐ[R] MvPowerSeries τ S) :
        (a : MvPolynomial σ R) → MvPowerSeries τ S)
      ((MvPolynomial.monomial e : (a : R) → MvPolynomial σ R) r) =
    HMul.hMul (α := MvPowerSeries τ S) (β := MvPowerSeries τ S)
      ((algebraMap R (MvPowerSeries τ S) : (a : R) → MvPowerSeries τ S) r : MvPowerSeries τ S)
      (e.prod fun (s : σ) (n : ℕ) ↦ a s ^ n : MvPowerSeries τ S)
rw₂ rw₃ :
  HMul.hMul (α := MvPowerSeries τ S) (β := MvPowerSeries τ S)
      ((algebraMap R (MvPowerSeries τ S) : (a : R) → MvPowerSeries τ S) r : MvPowerSeries τ S)
      (e.prod fun (i : σ) (k : ℕ) ↦ a i ^ k : MvPowerSeries τ S) =
    HMul.hMul (α := MvPowerSeries τ S) (β := MvPowerSeries τ S)
      ((algebraMap R (MvPowerSeries τ S) : (a : R) → MvPowerSeries τ S) r : MvPowerSeries τ S)
      (e.prod fun (s : σ) (n : ℕ) ↦ a s ^ n : MvPowerSeries τ S)
⊢ (substAlgHom ha : (a : MvPowerSeries σ R) → MvPowerSeries τ S) ((monomial e : (a : R) → MvPowerSeries σ R) r) =
    HMul.hMul (α := MvPowerSeries τ S) (β := MvPowerSeries τ S)
      ((algebraMap R (MvPowerSeries τ S) : (a : R) → MvPowerSeries τ S) r : MvPowerSeries τ S)
      (e.prod fun (s : σ) (n : ℕ) ↦ a s ^ n : MvPowerSeries τ S)

Tactic:
rw [← MvPolynomial.coe_monomial, substAlgHom_coe, MvPolynomial.aeval_monomial]

Premises used: MvPolynomial.coe_monomial, MvPowerSeries.substAlgHom_coe, MvPolynomial.aeval_monomial
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
τ : Type u_4
S : Type u_5
inst : CommRing S
a : σ → MvPowerSeries τ S
r : S
⊢ subst (R := S) a ((C : (a : S) → MvPowerSeries σ S) r) = (C : (a : S) → MvPowerSeries τ S) r

Tactic:
simp [subst, algebraMap_apply]

Premises used: MvPowerSeries.subst, MvPowerSeries.algebraMap_apply
-- 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
s : σ
rw : (substAlgHom ha : (a : MvPowerSeries σ R) → MvPowerSeries τ S) (X s) = a s
rw₁ rw₂ : a s = a s
⊢ subst.{u_1, u_3, u_4, u_5} (R := R) a (X s) = a s

Tactic:
rw [← coe_substAlgHom ha, substAlgHom_X]

Premises used: MvPowerSeries.substAlgHom_X, 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
e : σ →₀ ℕ
r : R
rw :
  (substAlgHom ha : (a : MvPowerSeries σ R) → MvPowerSeries τ S) ((monomial e : (a : R) → MvPowerSeries σ R) r) =
    HMul.hMul (α := MvPowerSeries τ S) (β := MvPowerSeries τ S)
      ((algebraMap R (MvPowerSeries τ S) : (a : R) → MvPowerSeries τ S) r : MvPowerSeries τ S)
      (e.prod fun (s : σ) (n : ℕ) ↦ a s ^ n : MvPowerSeries τ S)
rw₁ rw₂ :
  HMul.hMul (α := MvPowerSeries τ S) (β := MvPowerSeries τ S)
      ((algebraMap R (MvPowerSeries τ S) : (a : R) → MvPowerSeries τ S) r : MvPowerSeries τ S)
      (e.prod fun (s : σ) (n : ℕ) ↦ a s ^ n : MvPowerSeries τ S) =
    HMul.hMul (α := MvPowerSeries τ S) (β := MvPowerSeries τ S)
      ((algebraMap R (MvPowerSeries τ S) : (a : R) → MvPowerSeries τ S) r : MvPowerSeries τ S)
      (e.prod fun (s : σ) (n : ℕ) ↦ a s ^ n : MvPowerSeries τ S)
⊢ subst.{u_1, u_3, u_4, u_5} (R := R) a ((monomial e : (a : R) → MvPowerSeries σ R) r) =
    HMul.hMul (α := MvPowerSeries τ S) (β := MvPowerSeries τ S)
      ((algebraMap R (MvPowerSeries τ S) : (a : R) → MvPowerSeries τ S) r : MvPowerSeries τ S)
      (e.prod fun (s : σ) (n : ℕ) ↦ a s ^ n : MvPowerSeries τ S)

Tactic:
rw [← coe_substAlgHom ha, substAlgHom_monomial]

Premises used: MvPowerSeries.coe_substAlgHom, MvPowerSeries.substAlgHom_monomial
-- 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
inst_3 : UniformSpace R
inst_4 : DiscreteUniformity R
inst_5 : UniformSpace S
inst_6 : DiscreteUniformity S
rw : Continuous (eval₂ (algebraMap R (MvPowerSeries τ S)) a)
⊢ Continuous (X := MvPowerSeries σ R) (subst a)

Tactic:
rw [subst_eq_eval₂]

Premises used: MvPowerSeries.subst_eq_eval₂
-- 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
inst_3 : UniformSpace R
inst_4 : DiscreteUniformity R
inst_5 : UniformSpace S
inst_6 : DiscreteUniformity S
⊢ Continuous (eval₂ (algebraMap R (MvPowerSeries τ S)) a)

Tactic:
continuous_eval₂ (continuous_algebraMap _ _) ha.hasEval

Premises used: MvPowerSeries.continuous_eval₂, continuous_algebraMap, 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
ha : HasSubst a
inst_3 : UniformSpace R
inst_4 : DiscreteUniformity R
inst_5 : UniformSpace S
inst_6 : DiscreteUniformity S
⊢ Continuous (eval₂ (algebraMap R (MvPowerSeries τ S)) a)

Tactic:
exact continuous_eval₂ (continuous_algebraMap _ _) ha.hasEval

Premises used: MvPowerSeries.continuous_eval₂, continuous_algebraMap, 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
ha : HasSubst a
f : MvPowerSeries σ R
e : τ →₀ ℕ
⊢ Function.HasFiniteSupport.{u_1, u_5} (M := S) fun (d : σ →₀ ℕ) ↦
    HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff e : (a : MvPowerSeries τ S) → S) (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e) : S)

Tactic:
letI : UniformSpace R := ⊥
  letI : UniformSpace S := ⊥
  Summable.hasFiniteSupport_of_discreteTopology _
    ((hasSum_aeval ha.hasEval f).map (coeff e) (continuous_coeff S e)).summable

Premises used: HasSum.map, MvPowerSeries.hasSum_aeval, MvPowerSeries.WithPiTopology.continuous_coeff, HasSum.summable, HPow.hPow, Summable.hasFiniteSupport_of_discreteTopology, MvPowerSeries.coeff, HSMul.hSMul, MvPowerSeries.HasSubst.hasEval, DFunLike.coe, Finsupp.prod
-- 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
e : τ →₀ ℕ
this_1 : UniformSpace R := ⊥
this : UniformSpace S := ⊥
⊢ HasSum.{u_5, u_1} (α := S) (β := σ →₀ ℕ)
    (Function.comp (β := MvPowerSeries τ S) (⇑(coeff e) : (a : MvPowerSeries τ S) → S) fun (d : σ →₀ ℕ) ↦
        HSMul.hSMul (α := R) (β := MvPowerSeries τ S) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
          (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e) :
      (σ →₀ ℕ) → S)
    ((coeff e : (a : MvPowerSeries τ S) → S)
        (((aeval (σ := σ) (R := R) (S := MvPowerSeries τ S) (a := a) ⋯ : MvPowerSeries σ R →ₐ[R] MvPowerSeries τ S) :
              (a : MvPowerSeries σ R) → MvPowerSeries τ S)
            f :
          MvPowerSeries τ S) :
      S)

Tactic:
have := ((hasSum_aeval ha.hasEval f).map (coeff e) (continuous_coeff S e))
-- 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
e : τ →₀ ℕ
this_1 : UniformSpace R := ⊥
this_2 : UniformSpace S := ⊥
this :
  HasSum.{u_5, u_1} (α := S) (β := σ →₀ ℕ)
    (Function.comp (β := MvPowerSeries τ S) (⇑(coeff e) : (a : MvPowerSeries τ S) → S) fun (d : σ →₀ ℕ) ↦
        HSMul.hSMul (α := R) (β := MvPowerSeries τ S) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
          (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e) :
      (σ →₀ ℕ) → S)
    ((coeff e : (a : MvPowerSeries τ S) → S)
        (((aeval (σ := σ) (R := R) (S := MvPowerSeries τ S) (a := a) ⋯ : MvPowerSeries σ R →ₐ[R] MvPowerSeries τ S) :
              (a : MvPowerSeries σ R) → MvPowerSeries τ S)
            f :
          MvPowerSeries τ S) :
      S)
⊢ Eq.{u_5 + 1} (α := S) ((coeff e : (a : MvPowerSeries τ S) → S) (subst a f) : S)
    (∑ᶠ (d : σ →₀ ℕ),
        HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
          ((coeff e : (a : MvPowerSeries τ S) → S) (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e) : S) :
      S)

Tactic:
simp [← coe_substAlgHom ha, substAlgHom, ← this.tsum_eq,
    tsum_eq_finsum (coeff_subst_finite ha f e)]

Premises used: MvPowerSeries.coe_substAlgHom, tsum_eq_finsum, MvPowerSeries.substAlgHom, HasSum.tsum_eq, MvPowerSeries.coeff_subst_finite
-- 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
⊢ Eq.{u_5 + 1} (α := S) ((constantCoeff : (a : MvPowerSeries τ S) → S) (subst a f) : 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) :
      S)

Tactic:
simp only [← coeff_zero_eq_constantCoeff_apply, coeff_subst ha f 0]

Premises used: MvPowerSeries.coeff_zero_eq_constantCoeff_apply, MvPowerSeries.coeff_subst, OfNat.ofNat
-- 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
ha' : ∀ (i : σ), Eq.{u_5 + 1} (α := S) ((constantCoeff : (a : MvPowerSeries τ S) → S) (a i) : S) (0 : S)
f : MvPowerSeries σ R
hf : Eq.{u_3 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
rw :
  ∀ (x : σ →₀ ℕ),
    HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff x : (a : MvPowerSeries σ R) → R) f : R)
        ((constantCoeff : (a : MvPowerSeries τ S) → S) (x.prod fun (s : σ) (e : ℕ) ↦ a s ^ e) : S) =
      0
⊢ Eq.{u_5 + 1} (α := S) ((constantCoeff : (a : MvPowerSeries τ S) → S) (subst a f) : S) (0 : S)

Tactic:
rw [constantCoeff_subst ha, finsum_eq_zero_of_forall_eq_zero]

Premises used: MvPowerSeries.constantCoeff_subst, finsum_eq_zero_of_forall_eq_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
ha' : ∀ (i : σ), Eq.{u_5 + 1} (α := S) ((constantCoeff : (a : MvPowerSeries τ S) → S) (a i) : S) (0 : S)
f : MvPowerSeries σ R
hf : Eq.{u_3 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
d : σ →₀ ℕ
pos :
  ∀ (hd : d = 0),
    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) =
      0
neg :
  ∀ (hd : ¬d = 0),
    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) =
      0
⊢ 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) =
    0

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
ha' : ∀ (i : σ), Eq.{u_5 + 1} (α := S) ((constantCoeff : (a : MvPowerSeries τ S) → S) (a i) : S) (0 : S)
f : MvPowerSeries σ R
hf : Eq.{u_3 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
d : σ →₀ ℕ
hd : d = 0
⊢ 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) =
    0

Tactic:
simp [hd, hf]
-- 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
ha' : ∀ (i : σ), Eq.{u_5 + 1} (α := S) ((constantCoeff : (a : MvPowerSeries τ S) → S) (a i) : S) (0 : S)
f : MvPowerSeries σ R
hf : Eq.{u_3 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
d : σ →₀ ℕ
hd : ¬d = 0
by_contra! : ∀ (hc : ∀ (i : σ), Eq (α := ℕ) ((d : (a : σ) → ℕ) i : ℕ) (0 : ℕ)), False
⊢ ∃ (i : σ), Ne (α := ℕ) ((d : (a : σ) → ℕ) i : ℕ) (0 : ℕ)

Tactic:
by_contra! hc