internlm/Lean-Github huggingface dataset:
Theorem: MvPowerSeries.scale_linear_eq_smul
Proof state before:
case pos
σ : 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
T✝ : Type u_6
inst✝¹⁴ : CommRing T✝
inst✝¹³ : UniformSpace T✝
inst✝¹² : T2Space T✝
inst✝¹¹ : CompleteSpace T✝
inst✝¹⁰ : UniformAddGroup T✝
inst✝⁹ : TopologicalRing T✝
inst✝⁸ : LinearTopology T✝
inst✝⁷ : Algebra R T✝
inst✝⁶ : Algebra S T✝
inst✝⁵ : IsScalarTower R S T✝
ε : MvPowerSeries τ S →ₐ[R] T✝
υ : Type u_7
inst✝⁴ : DecidableEq υ
T : Type u_8
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
b : τ → MvPowerSeries υ T
hb : SubstDomain b
r : A
f : MvPowerSeries σ R
hf : ∀ (d : σ →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (coeff R d) f = 0
e : σ →₀ ℕ
he : ∑ x ∈ e.support, e x = 1
⊢ (r ^ ∑ i ∈ e.support, e i) • (coeff R e) f = (coeff R e) (r • f)
Tactic:
simp only [he, pow_one, LinearMap.map_smul_of_tower]
Proof state after:
no goals
Theorem: MvPowerSeries.scale_linear_eq_smul
Proof state before:
case neg
σ : 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
T✝ : Type u_6
inst✝¹⁴ : CommRing T✝
inst✝¹³ : UniformSpace T✝
inst✝¹² : T2Space T✝
inst✝¹¹ : CompleteSpace T✝
inst✝¹⁰ : UniformAddGroup T✝
inst✝⁹ : TopologicalRing T✝
inst✝⁸ : LinearTopology T✝
inst✝⁷ : Algebra R T✝
inst✝⁶ : Algebra S T✝
inst✝⁵ : IsScalarTower R S T✝
ε : MvPowerSeries τ S →ₐ[R] T✝
υ : Type u_7
inst✝⁴ : DecidableEq υ
T : Type u_8
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
b : τ → MvPowerSeries υ T
hb : SubstDomain b
r : A
f : MvPowerSeries σ R
hf : ∀ (d : σ →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (coeff R d) f = 0
e : σ →₀ ℕ
he : ¬(e.sum fun x n => n) = 1
⊢ (r ^ ∑ i ∈ e.support, e i) • (coeff R e) f = (coeff R e) (r • f)
Tactic:
simp only [hf e he, smul_zero, LinearMap.map_smul_of_tower]
Proof state after:
no goals
Theorem: PowerSeries.substDomain_X
Proof 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
⊢ (MvPowerSeries.constantCoeff Unit R) X = 0
Tactic:
change constantCoeff R X = 0
Proof 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
⊢ (constantCoeff R) X = 0
Theorem: PowerSeries.substDomain_X
Proof 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
⊢ (constantCoeff R) X = 0
Tactic:
rw [constantCoeff_X]
Proof state after:
no goals
Theorem: PowerSeries.substDomain_smul_X
Proof 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
a : A
⊢ (MvPowerSeries.constantCoeff Unit R) (a • X) = 0
Tactic:
change constantCoeff R (a • X) = 0
Proof 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
a : A
⊢ (constantCoeff R) (a • X) = 0
Theorem: PowerSeries.substDomain_smul_X
Proof 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
a : A
⊢ (constantCoeff R) (a • X) = 0
Tactic:
rw [← coeff_zero_eq_constantCoeff]
Proof 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
a : A
⊢ (coeff R 0) (a • X) = 0
Theorem: PowerSeries.substDomain_smul_X
Proof 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
a : A
⊢ (coeff R 0) (a • X) = 0
Tactic:
simp only [LinearMap.map_smul_of_tower, coeff_zero_X, smul_zero]
Proof state after:
no goals
Theorem: PowerSeries.subst_add
Proof 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 g : R⟦X⟧
⊢ subst a (f + g) = subst a f + subst a g
Tactic:
rw [← coe_substAlgHom ha, map_add]
Proof state after:
no goals
Theorem: PowerSeries.subst_pow
Proof 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⟧
n : ℕ
⊢ subst a (f ^ n) = subst a f ^ n
Tactic:
rw [← coe_substAlgHom ha, map_pow]
Proof state after:
no goals
Theorem: PowerSeries.subst_mul
Proof 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 g : R⟦X⟧
⊢ subst a (f * g) = subst a f * subst a g
Tactic:
rw [← coe_substAlgHom ha, map_mul]
Proof state after:
no goals
Theorem: PowerSeries.subst_smul
Proof 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
r : A
f : R⟦X⟧
⊢ subst a (r • f) = r • subst a f
Tactic:
rw [← coe_substAlgHom ha, AlgHom.map_smul_of_tower]
Proof state after:
no goals
Theorem: PowerSeries.coeff_subst_finite
Proof 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
Proof 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)
Theorem: PowerSeries.coeff_subst_finite
Proof 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]
Proof 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)
Theorem: PowerSeries.coeff_subst_finite
Proof 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
Proof 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)
Theorem: PowerSeries.coeff_subst_finite
Proof 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]
Proof 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
Theorem: PowerSeries.coeff_subst_finite
Proof 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
Proof 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
Theorem: PowerSeries.coeff_subst_finite
Proof 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]
Proof 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)
Theorem: PowerSeries.coeff_subst_finite
Proof 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
Proof state after:
no goals
Theorem: PowerSeries.coeff_subst
Proof 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]
Proof 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)
Theorem: PowerSeries.coeff_subst
Proof 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]
Proof 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)
Theorem: PowerSeries.coeff_subst
Proof 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
Proof 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)
Theorem: PowerSeries.coeff_subst
Proof 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
Proof 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)