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

State before:
A : Type u_1
inst✝¹² : CommRing A
R : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : Algebra A R
τ : Type u_3
inst✝⁹ : DecidableEq τ
S : Type u_4
inst✝⁸ : CommRing S
inst✝⁷ : Algebra A S
inst✝⁶ : Algebra R S
inst✝⁵ : IsScalarTower A R S
υ : Type u_5
inst✝⁴ : DecidableEq υ
T : Type u_6
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
a : MvPowerSeries τ S
ha : SubstDomain a
f : R⟦X⟧
e : τ →₀ ℕ
⊢ (MvPowerSeries.coeff S e) (subst a f) = ∑ᶠ (d : ℕ), (coeff R d) f • (MvPowerSeries.coeff S e) (a ^ d)
Tactic:
erw [MvPowerSeries.coeff_subst ha.const f e]
State after:
A : Type u_1
inst✝¹² : CommRing A
R : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : Algebra A R
τ : Type u_3
inst✝⁹ : DecidableEq τ
S : Type u_4
inst✝⁸ : CommRing S
inst✝⁷ : Algebra A S
inst✝⁶ : Algebra R S
inst✝⁵ : IsScalarTower A R S
υ : Type u_5
inst✝⁴ : DecidableEq υ
T : Type u_6
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
a : MvPowerSeries τ S
ha : SubstDomain a
f : R⟦X⟧
e : τ →₀ ℕ
⊢ ∑ᶠ (d : Unit →₀ ℕ), (MvPowerSeries.coeff R d) f • (MvPowerSeries.coeff S e) (d.prod fun s e => a ^ e) =
    ∑ᶠ (d : ℕ), (coeff R d) f • (MvPowerSeries.coeff S e) (a ^ d)

State before:
A : Type u_1
inst✝¹² : CommRing A
R : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : Algebra A R
τ : Type u_3
inst✝⁹ : DecidableEq τ
S : Type u_4
inst✝⁸ : CommRing S
inst✝⁷ : Algebra A S
inst✝⁶ : Algebra R S
inst✝⁵ : IsScalarTower A R S
υ : Type u_5
inst✝⁴ : DecidableEq υ
T : Type u_6
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
a : MvPowerSeries τ S
ha : SubstDomain a
f : R⟦X⟧
e : τ →₀ ℕ
⊢ ∑ᶠ (d : Unit →₀ ℕ), (MvPowerSeries.coeff R d) f • (MvPowerSeries.coeff S e) (d.prod fun s e => a ^ e) =
    ∑ᶠ (d : ℕ), (coeff R d) f • (MvPowerSeries.coeff S e) (a ^ d)
Tactic:
rw [← finsum_comp_equiv (Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv.symm]
State after:
A : Type u_1
inst✝¹² : CommRing A
R : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : Algebra A R
τ : Type u_3
inst✝⁹ : DecidableEq τ
S : Type u_4
inst✝⁸ : CommRing S
inst✝⁷ : Algebra A S
inst✝⁶ : Algebra R S
inst✝⁵ : IsScalarTower A R S
υ : Type u_5
inst✝⁴ : DecidableEq υ
T : Type u_6
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
a : MvPowerSeries τ S
ha : SubstDomain a
f : R⟦X⟧
e : τ →₀ ℕ
⊢ ∑ᶠ (i : ℕ),
      (MvPowerSeries.coeff R ((Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv.symm i)) f •
        (MvPowerSeries.coeff S e)
          (((Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv.symm i).prod fun s e => a ^ e) =
    ∑ᶠ (d : ℕ), (coeff R d) f • (MvPowerSeries.coeff S e) (a ^ d)

State before:
A : Type u_1
inst✝¹² : CommRing A
R : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : Algebra A R
τ : Type u_3
inst✝⁹ : DecidableEq τ
S : Type u_4
inst✝⁸ : CommRing S
inst✝⁷ : Algebra A S
inst✝⁶ : Algebra R S
inst✝⁵ : IsScalarTower A R S
υ : Type u_5
inst✝⁴ : DecidableEq υ
T : Type u_6
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
a : MvPowerSeries τ S
ha : SubstDomain a
f : R⟦X⟧
e : τ →₀ ℕ
⊢ ∑ᶠ (i : ℕ),
      (MvPowerSeries.coeff R ((Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv.symm i)) f •
        (MvPowerSeries.coeff S e)
          (((Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv.symm i).prod fun s e => a ^ e) =
    ∑ᶠ (d : ℕ), (coeff R d) f • (MvPowerSeries.coeff S e) (a ^ d)
Tactic:
apply finsum_congr
State after:
case h
A : Type u_1
inst✝¹² : CommRing A
R : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : Algebra A R
τ : Type u_3
inst✝⁹ : DecidableEq τ
S : Type u_4
inst✝⁸ : CommRing S
inst✝⁷ : Algebra A S
inst✝⁶ : Algebra R S
inst✝⁵ : IsScalarTower A R S
υ : Type u_5
inst✝⁴ : DecidableEq υ
T : Type u_6
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
a : MvPowerSeries τ S
ha : SubstDomain a
f : R⟦X⟧
e : τ →₀ ℕ
⊢ ∀ (x : ℕ),
    (MvPowerSeries.coeff R ((Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv.symm x)) f •
        (MvPowerSeries.coeff S e)
          (((Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv.symm x).prod fun s e => a ^ e) =
      (coeff R x) f • (MvPowerSeries.coeff S e) (a ^ x)

State before:
case h
A : Type u_1
inst✝¹² : CommRing A
R : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : Algebra A R
τ : Type u_3
inst✝⁹ : DecidableEq τ
S : Type u_4
inst✝⁸ : CommRing S
inst✝⁷ : Algebra A S
inst✝⁶ : Algebra R S
inst✝⁵ : IsScalarTower A R S
υ : Type u_5
inst✝⁴ : DecidableEq υ
T : Type u_6
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
a : MvPowerSeries τ S
ha : SubstDomain a
f : R⟦X⟧
e : τ →₀ ℕ
⊢ ∀ (x : ℕ),
    (MvPowerSeries.coeff R ((Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv.symm x)) f •
        (MvPowerSeries.coeff S e)
          (((Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv.symm x).prod fun s e => a ^ e) =
      (coeff R x) f • (MvPowerSeries.coeff S e) (a ^ x)
Tactic:
intro d
State after:
case h
A : Type u_1
inst✝¹² : CommRing A
R : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : Algebra A R
τ : Type u_3
inst✝⁹ : DecidableEq τ
S : Type u_4
inst✝⁸ : CommRing S
inst✝⁷ : Algebra A S
inst✝⁶ : Algebra R S
inst✝⁵ : IsScalarTower A R S
υ : Type u_5
inst✝⁴ : DecidableEq υ
T : Type u_6
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
a : MvPowerSeries τ S
ha : SubstDomain a
f : R⟦X⟧
e : τ →₀ ℕ
d : ℕ
⊢ (MvPowerSeries.coeff R ((Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv.symm d)) f •
      (MvPowerSeries.coeff S e) (((Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv.symm d).prod fun s e => a ^ e) =
    (coeff R d) f • (MvPowerSeries.coeff S e) (a ^ d)

State before:
case h
A : Type u_1
inst✝¹² : CommRing A
R : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : Algebra A R
τ : Type u_3
inst✝⁹ : DecidableEq τ
S : Type u_4
inst✝⁸ : CommRing S
inst✝⁷ : Algebra A S
inst✝⁶ : Algebra R S
inst✝⁵ : IsScalarTower A R S
υ : Type u_5
inst✝⁴ : DecidableEq υ
T : Type u_6
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
a : MvPowerSeries τ S
ha : SubstDomain a
f : R⟦X⟧
e : τ →₀ ℕ
d : ℕ
⊢ (MvPowerSeries.coeff R ((Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv.symm d)) f •
      (MvPowerSeries.coeff S e) (((Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv.symm d).prod fun s e => a ^ e) =
    (coeff R d) f • (MvPowerSeries.coeff S e) (a ^ d)
Tactic:
congr
State after:
case h.e_a.e_a.e_n
A : Type u_1
inst✝¹² : CommRing A
R : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : Algebra A R
τ : Type u_3
inst✝⁹ : DecidableEq τ
S : Type u_4
inst✝⁸ : CommRing S
inst✝⁷ : Algebra A S
inst✝⁶ : Algebra R S
inst✝⁵ : IsScalarTower A R S
υ : Type u_5
inst✝⁴ : DecidableEq υ
T : Type u_6
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
a : MvPowerSeries τ S
ha : SubstDomain a
f : R⟦X⟧
e : τ →₀ ℕ
d : ℕ
⊢ (Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv.symm d = Finsupp.single () d

case h.e_a.h.e_6.h
A : Type u_1
inst✝¹² : CommRing A
R : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : Algebra A R
τ : Type u_3
inst✝⁹ : DecidableEq τ
S : Type u_4
inst✝⁸ : CommRing S
inst✝⁷ : Algebra A S
inst✝⁶ : Algebra R S
inst✝⁵ : IsScalarTower A R S
υ : Type u_5
inst✝⁴ : DecidableEq υ
T : Type u_6
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
a : MvPowerSeries τ S
ha : SubstDomain a
f : R⟦X⟧
e : τ →₀ ℕ
d : ℕ
⊢ (((Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv.symm d).prod fun s e => a ^ e) = a ^ d

State before:
case h.e_a.e_a.e_n
A : Type u_1
inst✝¹² : CommRing A
R : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : Algebra A R
τ : Type u_3
inst✝⁹ : DecidableEq τ
S : Type u_4
inst✝⁸ : CommRing S
inst✝⁷ : Algebra A S
inst✝⁶ : Algebra R S
inst✝⁵ : IsScalarTower A R S
υ : Type u_5
inst✝⁴ : DecidableEq υ
T : Type u_6
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
a : MvPowerSeries τ S
ha : SubstDomain a
f : R⟦X⟧
e : τ →₀ ℕ
d : ℕ
⊢ (Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv.symm d = Finsupp.single () d
Tactic:
ext
State after:
case h.e_a.e_a.e_n.h
A : Type u_1
inst✝¹² : CommRing A
R : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : Algebra A R
τ : Type u_3
inst✝⁹ : DecidableEq τ
S : Type u_4
inst✝⁸ : CommRing S
inst✝⁷ : Algebra A S
inst✝⁶ : Algebra R S
inst✝⁵ : IsScalarTower A R S
υ : Type u_5
inst✝⁴ : DecidableEq υ
T : Type u_6
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
a : MvPowerSeries τ S
ha : SubstDomain a
f : R⟦X⟧
e : τ →₀ ℕ
d : ℕ
⊢ ((Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv.symm d) default = (Finsupp.single () d) default

State before:
case h.e_a.e_a.e_n.h
A : Type u_1
inst✝¹² : CommRing A
R : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : Algebra A R
τ : Type u_3
inst✝⁹ : DecidableEq τ
S : Type u_4
inst✝⁸ : CommRing S
inst✝⁷ : Algebra A S
inst✝⁶ : Algebra R S
inst✝⁵ : IsScalarTower A R S
υ : Type u_5
inst✝⁴ : DecidableEq υ
T : Type u_6
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
a : MvPowerSeries τ S
ha : SubstDomain a
f : R⟦X⟧
e : τ →₀ ℕ
d : ℕ
⊢ ((Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv.symm d) default = (Finsupp.single () d) default
Tactic:
simp
State after:
no goals

State before:
case h.e_a.h.e_6.h
A : Type u_1
inst✝¹² : CommRing A
R : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : Algebra A R
τ : Type u_3
inst✝⁹ : DecidableEq τ
S : Type u_4
inst✝⁸ : CommRing S
inst✝⁷ : Algebra A S
inst✝⁶ : Algebra R S
inst✝⁵ : IsScalarTower A R S
υ : Type u_5
inst✝⁴ : DecidableEq υ
T : Type u_6
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
a : MvPowerSeries τ S
ha : SubstDomain a
f : R⟦X⟧
e : τ →₀ ℕ
d : ℕ
⊢ (((Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv.symm d).prod fun s e => a ^ e) = a ^ d
Tactic:
simp
State after:
no goals