Theorem: MvPowerSeries.coeff_subst (DividedPowers/ForMathlib/MvPowerSeries/Substitutions.lean)

State before:
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a : σ → MvPowerSeries τ S
ha : SubstDomain a
f : MvPowerSeries σ R
e : τ →₀ ℕ
⊢ (coeff S e) (subst a f) = ∑ᶠ (d : σ →₀ ℕ), (coeff R d) f • (coeff S e) (d.prod fun s e => a s ^ e)
Tactic:
letI : UniformSpace S := ⊥
State after:
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a : σ → MvPowerSeries τ S
ha : SubstDomain a
f : MvPowerSeries σ R
e : τ →₀ ℕ
this : UniformSpace S := ⊥
⊢ (coeff S e) (subst a f) = ∑ᶠ (d : σ →₀ ℕ), (coeff R d) f • (coeff S e) (d.prod fun s e => a s ^ e)

State before:
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a : σ → MvPowerSeries τ S
ha : SubstDomain a
f : MvPowerSeries σ R
e : τ →₀ ℕ
this : UniformSpace S := ⊥
⊢ (coeff S e) (subst a f) = ∑ᶠ (d : σ →₀ ℕ), (coeff R d) f • (coeff S e) (d.prod fun s e => a s ^ e)
Tactic:
letI : UniformSpace R := ⊥
State after:
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a : σ → MvPowerSeries τ S
ha : SubstDomain a
f : MvPowerSeries σ R
e : τ →₀ ℕ
this✝ : UniformSpace S := ⊥
this : UniformSpace R := ⊥
⊢ (coeff S e) (subst a f) = ∑ᶠ (d : σ →₀ ℕ), (coeff R d) f • (coeff S e) (d.prod fun s e => a s ^ e)

State before:
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a : σ → MvPowerSeries τ S
ha : SubstDomain a
f : MvPowerSeries σ R
e : τ →₀ ℕ
this✝ : UniformSpace S := ⊥
this : UniformSpace R := ⊥
⊢ (coeff S e) (subst a f) = ∑ᶠ (d : σ →₀ ℕ), (coeff R d) f • (coeff S e) (d.prod fun s e => a s ^ e)
Tactic:
have := ((hasSum_aeval ha.evalDomain f).map (coeff S e) (continuous_coeff e))
State after:
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a : σ → MvPowerSeries τ S
ha : SubstDomain a
f : MvPowerSeries σ R
e : τ →₀ ℕ
this✝¹ : UniformSpace S := ⊥
this✝ : UniformSpace R := ⊥
this : HasSum (⇑(coeff S e) ∘ fun d => (coeff R d) f • d.prod fun s e => a s ^ e) ((coeff S e) ((aeval ⋯) f))
⊢ (coeff S e) (subst a f) = ∑ᶠ (d : σ →₀ ℕ), (coeff R d) f • (coeff S e) (d.prod fun s e => a s ^ e)

State before:
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a : σ → MvPowerSeries τ S
ha : SubstDomain a
f : MvPowerSeries σ R
e : τ →₀ ℕ
this✝¹ : UniformSpace S := ⊥
this✝ : UniformSpace R := ⊥
this : HasSum (⇑(coeff S e) ∘ fun d => (coeff R d) f • d.prod fun s e => a s ^ e) ((coeff S e) ((aeval ⋯) f))
⊢ (coeff S e) (subst a f) = ∑ᶠ (d : σ →₀ ℕ), (coeff R d) f • (coeff S e) (d.prod fun s e => a s ^ e)
Tactic:
erw [← this.tsum_eq, tsum_def]
State after:
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a : σ → MvPowerSeries τ S
ha : SubstDomain a
f : MvPowerSeries σ R
e : τ →₀ ℕ
this✝¹ : UniformSpace S := ⊥
this✝ : UniformSpace R := ⊥
this : HasSum (⇑(coeff S e) ∘ fun d => (coeff R d) f • d.prod fun s e => a s ^ e) ((coeff S e) ((aeval ⋯) f))
⊢ (if h : Summable fun b => (⇑(coeff S e) ∘ fun d => (coeff R d) f • d.prod fun s e => a s ^ e) b then
      if (Function.support fun b => (⇑(coeff S e) ∘ fun d => (coeff R d) f • d.prod fun s e => a s ^ e) b).Finite then
        ∑ᶠ (b : σ →₀ ℕ), (⇑(coeff S e) ∘ fun d => (coeff R d) f • d.prod fun s e => a s ^ e) b
      else Exists.choose h
    else 0) =
    ∑ᶠ (d : σ →₀ ℕ), (coeff R d) f • (coeff S e) (d.prod fun s e => a s ^ e)

State before:
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a : σ → MvPowerSeries τ S
ha : SubstDomain a
f : MvPowerSeries σ R
e : τ →₀ ℕ
this✝¹ : UniformSpace S := ⊥
this✝ : UniformSpace R := ⊥
this : HasSum (⇑(coeff S e) ∘ fun d => (coeff R d) f • d.prod fun s e => a s ^ e) ((coeff S e) ((aeval ⋯) f))
⊢ (if h : Summable fun b => (⇑(coeff S e) ∘ fun d => (coeff R d) f • d.prod fun s e => a s ^ e) b then
      if (Function.support fun b => (⇑(coeff S e) ∘ fun d => (coeff R d) f • d.prod fun s e => a s ^ e) b).Finite then
        ∑ᶠ (b : σ →₀ ℕ), (⇑(coeff S e) ∘ fun d => (coeff R d) f • d.prod fun s e => a s ^ e) b
      else Exists.choose h
    else 0) =
    ∑ᶠ (d : σ →₀ ℕ), (coeff R d) f • (coeff S e) (d.prod fun s e => a s ^ e)
Tactic:
erw [dif_pos this.summable, if_pos (coeff_subst_finite ha f e)]
State after:
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a : σ → MvPowerSeries τ S
ha : SubstDomain a
f : MvPowerSeries σ R
e : τ →₀ ℕ
this✝¹ : UniformSpace S := ⊥
this✝ : UniformSpace R := ⊥
this : HasSum (⇑(coeff S e) ∘ fun d => (coeff R d) f • d.prod fun s e => a s ^ e) ((coeff S e) ((aeval ⋯) f))
⊢ ∑ᶠ (b : σ →₀ ℕ), (⇑(coeff S e) ∘ fun d => (coeff R d) f • d.prod fun s e => a s ^ e) b =
    ∑ᶠ (d : σ →₀ ℕ), (coeff R d) f • (coeff S e) (d.prod fun s e => a s ^ e)

State before:
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a : σ → MvPowerSeries τ S
ha : SubstDomain a
f : MvPowerSeries σ R
e : τ →₀ ℕ
this✝¹ : UniformSpace S := ⊥
this✝ : UniformSpace R := ⊥
this : HasSum (⇑(coeff S e) ∘ fun d => (coeff R d) f • d.prod fun s e => a s ^ e) ((coeff S e) ((aeval ⋯) f))
⊢ ∑ᶠ (b : σ →₀ ℕ), (⇑(coeff S e) ∘ fun d => (coeff R d) f • d.prod fun s e => a s ^ e) b =
    ∑ᶠ (d : σ →₀ ℕ), (coeff R d) f • (coeff S e) (d.prod fun s e => a s ^ e)
Tactic:
rfl
State after:
no goals