Theorem: PowerSeries.coeff_subst_finite (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 : τ →₀ ℕ
⊢ (Function.support fun d => (coeff R d) f • (MvPowerSeries.coeff S e) (a ^ d)).Finite
Tactic:
convert (MvPowerSeries.coeff_subst_finite ha.const f e).image
  ⇑(Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv
State after:
case h.e'_2
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 : τ →₀ ℕ
⊢ (Function.support fun d => (coeff R d) f • (MvPowerSeries.coeff S e) (a ^ d)) =
    ⇑(Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv ''
      Function.support fun d => (MvPowerSeries.coeff R d) f • (MvPowerSeries.coeff S e) (d.prod fun s e => a ^ e)

State before:
case h.e'_2
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 : τ →₀ ℕ
⊢ (Function.support fun d => (coeff R d) f • (MvPowerSeries.coeff S e) (a ^ d)) =
    ⇑(Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv ''
      Function.support fun d => (MvPowerSeries.coeff R d) f • (MvPowerSeries.coeff S e) (d.prod fun s e => a ^ e)
Tactic:
rw [← Equiv.preimage_eq_iff_eq_image, ← Function.support_comp_eq_preimage]
State after:
case h.e'_2
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 : τ →₀ ℕ
⊢ Function.support
      ((fun d => (coeff R d) f • (MvPowerSeries.coeff S e) (a ^ d)) ∘
        ⇑(Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv) =
    Function.support fun d => (MvPowerSeries.coeff R d) f • (MvPowerSeries.coeff S e) (d.prod fun s e => a ^ e)

State before:
case h.e'_2
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 : τ →₀ ℕ
⊢ Function.support
      ((fun d => (coeff R d) f • (MvPowerSeries.coeff S e) (a ^ d)) ∘
        ⇑(Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv) =
    Function.support fun d => (MvPowerSeries.coeff R d) f • (MvPowerSeries.coeff S e) (d.prod fun s e => a ^ e)
Tactic:
apply congr_arg
State after:
case h.e'_2.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 : τ →₀ ℕ
⊢ (fun d => (coeff R d) f • (MvPowerSeries.coeff S e) (a ^ d)) ∘ ⇑(Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv =
    fun d => (MvPowerSeries.coeff R d) f • (MvPowerSeries.coeff S e) (d.prod fun s e => a ^ e)

State before:
case h.e'_2.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 : τ →₀ ℕ
⊢ (fun d => (coeff R d) f • (MvPowerSeries.coeff S e) (a ^ d)) ∘ ⇑(Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv =
    fun d => (MvPowerSeries.coeff R d) f • (MvPowerSeries.coeff S e) (d.prod fun s e => a ^ e)
Tactic:
rw [← Equiv.eq_comp_symm]
State after:
case h.e'_2.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 : τ →₀ ℕ
⊢ (fun d => (coeff R d) f • (MvPowerSeries.coeff S e) (a ^ d)) =
    (fun d => (MvPowerSeries.coeff R d) f • (MvPowerSeries.coeff S e) (d.prod fun s e => a ^ e)) ∘
      ⇑(Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv.symm

State before:
case h.e'_2.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 : τ →₀ ℕ
⊢ (fun d => (coeff R d) f • (MvPowerSeries.coeff S e) (a ^ d)) =
    (fun d => (MvPowerSeries.coeff R d) f • (MvPowerSeries.coeff S e) (d.prod fun s e => a ^ e)) ∘
      ⇑(Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv.symm
Tactic:
ext d
State after:
case h.e'_2.h.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 : ℕ
⊢ (coeff R d) f • (MvPowerSeries.coeff S e) (a ^ d) =
    ((fun d => (MvPowerSeries.coeff R d) f • (MvPowerSeries.coeff S e) (d.prod fun s e => a ^ e)) ∘
        ⇑(Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv.symm)
      d

State before:
case h.e'_2.h.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 : ℕ
⊢ (coeff R d) f • (MvPowerSeries.coeff S e) (a ^ d) =
    ((fun d => (MvPowerSeries.coeff R d) f • (MvPowerSeries.coeff S e) (d.prod fun s e => a ^ e)) ∘
        ⇑(Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv.symm)
      d
Tactic:
simp only [Finsupp.prod_pow, Finset.univ_unique, PUnit.default_eq_unit, Finset.prod_singleton,
  LinearEquiv.coe_toEquiv_symm, EquivLike.coe_coe, Function.comp_apply,
  Finsupp.LinearEquiv.finsuppUnique_symm_apply, Finsupp.single_eq_same]
State after:
case h.e'_2.h.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 : ℕ
⊢ (coeff R d) f • (MvPowerSeries.coeff S e) (a ^ d) =
    (MvPowerSeries.coeff R (Finsupp.single PUnit.unit d)) f • (MvPowerSeries.coeff S e) (a ^ d)

State before:
case h.e'_2.h.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 : ℕ
⊢ (coeff R d) f • (MvPowerSeries.coeff S e) (a ^ d) =
    (MvPowerSeries.coeff R (Finsupp.single PUnit.unit d)) f • (MvPowerSeries.coeff S e) (a ^ d)
Tactic:
congr
State after:
no goals