internlm/Lean-Github huggingface dataset:
Theorem: PowerSeries.subst_comp_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✝
υ : 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
a : S⟦X⟧
ha : SubstDomain a
b : MvPowerSeries υ T
hb : SubstDomain b
a' : MvPowerSeries τ S
ha' : SubstDomain a'
b' : τ → MvPowerSeries υ T
hb' : MvPowerSeries.SubstDomain b'
⊢ subst b ∘ subst a = subst (subst b a)
Tactic:
have h := substAlgHom_comp_substAlgHom (R := R) ha hb
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✝
υ : 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
a : S⟦X⟧
ha : SubstDomain a
b : MvPowerSeries υ T
hb : SubstDomain b
a' : MvPowerSeries τ S
ha' : SubstDomain a'
b' : τ → MvPowerSeries υ T
hb' : MvPowerSeries.SubstDomain b'
h : (AlgHom.restrictScalars R (substAlgHom hb)).comp (substAlgHom ha) = substAlgHom ⋯
⊢ subst b ∘ subst a = subst (subst b a)
Theorem: PowerSeries.subst_comp_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✝
υ : 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
a : S⟦X⟧
ha : SubstDomain a
b : MvPowerSeries υ T
hb : SubstDomain b
a' : MvPowerSeries τ S
ha' : SubstDomain a'
b' : τ → MvPowerSeries υ T
hb' : MvPowerSeries.SubstDomain b'
h : (AlgHom.restrictScalars R (substAlgHom hb)).comp (substAlgHom ha) = substAlgHom ⋯
⊢ subst b ∘ subst a = subst (subst b a)
Tactic:
simp only [DFunLike.ext_iff, AlgHom.coe_comp, AlgHom.coe_restrictScalars', Function.comp_apply] at h
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✝
υ : 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
a : S⟦X⟧
ha : SubstDomain a
b : MvPowerSeries υ T
hb : SubstDomain b
a' : MvPowerSeries τ S
ha' : SubstDomain a'
b' : τ → MvPowerSeries υ T
hb' : MvPowerSeries.SubstDomain b'
h : ∀ (x : R⟦X⟧), (substAlgHom hb) ((substAlgHom ha) x) = (substAlgHom ⋯) x
⊢ subst b ∘ subst a = subst (subst b a)
Theorem: PowerSeries.subst_comp_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✝
υ : 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
a : S⟦X⟧
ha : SubstDomain a
b : MvPowerSeries υ T
hb : SubstDomain b
a' : MvPowerSeries τ S
ha' : SubstDomain a'
b' : τ → MvPowerSeries υ T
hb' : MvPowerSeries.SubstDomain b'
h : ∀ (x : R⟦X⟧), (substAlgHom hb) ((substAlgHom ha) x) = (substAlgHom ⋯) x
⊢ subst b ∘ subst a = subst (subst b a)
Tactic:
exact funext h
Proof state after:
no goals
Theorem: PowerSeries.scale_algHom_comp
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✝¹
υ : 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
a✝ : S⟦X⟧
ha : SubstDomain a✝
b✝ : MvPowerSeries υ T
hb : SubstDomain b✝
a' : MvPowerSeries τ S
ha' : SubstDomain a'
b' : τ → MvPowerSeries υ T
hb' : MvPowerSeries.SubstDomain b'
a b : A
⊢ (scale_algHom R a).comp (scale_algHom R b) = scale_algHom R (a * b)
Tactic:
simp only [scale_algHom]
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✝¹
υ : 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
a✝ : S⟦X⟧
ha : SubstDomain a✝
b✝ : MvPowerSeries υ T
hb : SubstDomain b✝
a' : MvPowerSeries τ S
ha' : SubstDomain a'
b' : τ → MvPowerSeries υ T
hb' : MvPowerSeries.SubstDomain b'
a b : A
⊢ (MvPowerSeries.scale_algHom R (Function.const Unit a)).comp (MvPowerSeries.scale_algHom R (Function.const Unit b)) =
    MvPowerSeries.scale_algHom R (Function.const Unit (a * b))
Theorem: PowerSeries.scale_algHom_comp
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✝¹
υ : 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
a✝ : S⟦X⟧
ha : SubstDomain a✝
b✝ : MvPowerSeries υ T
hb : SubstDomain b✝
a' : MvPowerSeries τ S
ha' : SubstDomain a'
b' : τ → MvPowerSeries υ T
hb' : MvPowerSeries.SubstDomain b'
a b : A
⊢ (MvPowerSeries.scale_algHom R (Function.const Unit a)).comp (MvPowerSeries.scale_algHom R (Function.const Unit b)) =
    MvPowerSeries.scale_algHom R (Function.const Unit (a * b))
Tactic:
rw [MvPowerSeries.scale_algHom_comp]
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✝¹
υ : 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
a✝ : S⟦X⟧
ha : SubstDomain a✝
b✝ : MvPowerSeries υ T
hb : SubstDomain b✝
a' : MvPowerSeries τ S
ha' : SubstDomain a'
b' : τ → MvPowerSeries υ T
hb' : MvPowerSeries.SubstDomain b'
a b : A
⊢ MvPowerSeries.scale_algHom R (Function.const Unit a * Function.const Unit b) =
    MvPowerSeries.scale_algHom R (Function.const Unit (a * b))
Theorem: PowerSeries.scale_algHom_comp
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✝¹
υ : 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
a✝ : S⟦X⟧
ha : SubstDomain a✝
b✝ : MvPowerSeries υ T
hb : SubstDomain b✝
a' : MvPowerSeries τ S
ha' : SubstDomain a'
b' : τ → MvPowerSeries υ T
hb' : MvPowerSeries.SubstDomain b'
a b : A
⊢ MvPowerSeries.scale_algHom R (Function.const Unit a * Function.const Unit b) =
    MvPowerSeries.scale_algHom R (Function.const Unit (a * b))
Tactic:
rfl
Proof state after:
no goals
Theorem: PowerSeries.coeff_scale
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✝¹
υ : 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
a✝ : S⟦X⟧
ha : SubstDomain a✝
b : MvPowerSeries υ T
hb : SubstDomain b
a' : MvPowerSeries τ S
ha' : SubstDomain a'
b' : τ → MvPowerSeries υ T
hb' : MvPowerSeries.SubstDomain b'
a : A
f : R⟦X⟧
d : ℕ
⊢ (coeff R d) (scale a f) = a ^ d • (coeff R d) f
Tactic:
convert MvPowerSeries.coeff_scale (Function.const Unit a) f (Finsupp.single default d)
Proof state after:
case h.e'_3.h.e'_5
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✝¹
υ : 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
a✝ : S⟦X⟧
ha : SubstDomain a✝
b : MvPowerSeries υ T
hb : SubstDomain b
a' : MvPowerSeries τ S
ha' : SubstDomain a'
b' : τ → MvPowerSeries υ T
hb' : MvPowerSeries.SubstDomain b'
a : A
f : R⟦X⟧
d : ℕ
⊢ a ^ d = (Finsupp.single default d).prod fun s n => Function.const Unit a s ^ n
Theorem: PowerSeries.coeff_scale
Proof state before:
case h.e'_3.h.e'_5
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✝¹
υ : 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
a✝ : S⟦X⟧
ha : SubstDomain a✝
b : MvPowerSeries υ T
hb : SubstDomain b
a' : MvPowerSeries τ S
ha' : SubstDomain a'
b' : τ → MvPowerSeries υ T
hb' : MvPowerSeries.SubstDomain b'
a : A
f : R⟦X⟧
d : ℕ
⊢ a ^ d = (Finsupp.single default d).prod fun s n => Function.const Unit a s ^ n
Tactic:
simp only [PUnit.default_eq_unit, Function.const_apply, pow_zero, Finsupp.prod_single_index]
Proof state after:
no goals
Theorem: PowerSeries.scale_algebraMap
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✝¹
υ : 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
a✝ : S⟦X⟧
ha : SubstDomain a✝
b : MvPowerSeries υ T
hb : SubstDomain b
a' : MvPowerSeries τ S
ha' : SubstDomain a'
b' : τ → MvPowerSeries υ T
hb' : MvPowerSeries.SubstDomain b'
a : A
⊢ scale ((algebraMap A R) a) = scale a
Tactic:
ext f n
Proof state after:
case 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✝¹
υ : 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
a✝ : S⟦X⟧
ha : SubstDomain a✝
b : MvPowerSeries υ T
hb : SubstDomain b
a' : MvPowerSeries τ S
ha' : SubstDomain a'
b' : τ → MvPowerSeries υ T
hb' : MvPowerSeries.SubstDomain b'
a : A
f : R⟦X⟧
n : ℕ
⊢ (coeff R n) (scale ((algebraMap A R) a) f) = (coeff R n) (scale a f)
Theorem: PowerSeries.scale_algebraMap
Proof state before:
case 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✝¹
υ : 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
a✝ : S⟦X⟧
ha : SubstDomain a✝
b : MvPowerSeries υ T
hb : SubstDomain b
a' : MvPowerSeries τ S
ha' : SubstDomain a'
b' : τ → MvPowerSeries υ T
hb' : MvPowerSeries.SubstDomain b'
a : A
f : R⟦X⟧
n : ℕ
⊢ (coeff R n) (scale ((algebraMap A R) a) f) = (coeff R n) (scale a f)
Tactic:
simp only [coeff_scale]
Proof state after:
case 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✝¹
υ : 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
a✝ : S⟦X⟧
ha : SubstDomain a✝
b : MvPowerSeries υ T
hb : SubstDomain b
a' : MvPowerSeries τ S
ha' : SubstDomain a'
b' : τ → MvPowerSeries υ T
hb' : MvPowerSeries.SubstDomain b'
a : A
f : R⟦X⟧
n : ℕ
⊢ (algebraMap A R) a ^ n • (coeff R n) f = a ^ n • (coeff R n) f
Theorem: PowerSeries.scale_algebraMap
Proof state before:
case 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✝¹
υ : 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
a✝ : S⟦X⟧
ha : SubstDomain a✝
b : MvPowerSeries υ T
hb : SubstDomain b
a' : MvPowerSeries τ S
ha' : SubstDomain a'
b' : τ → MvPowerSeries υ T
hb' : MvPowerSeries.SubstDomain b'
a : A
f : R⟦X⟧
n : ℕ
⊢ (algebraMap A R) a ^ n • (coeff R n) f = a ^ n • (coeff R n) f
Tactic:
rw [← algebraMap_smul (R := A) R, map_pow]
Proof state after:
no goals
Theorem: PowerSeries.subst_linear_subst_scalar_comm
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✝¹
υ : 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
a✝ : S⟦X⟧
ha : SubstDomain a✝
b : MvPowerSeries υ T
hb : SubstDomain b
a' : MvPowerSeries τ S
ha' : SubstDomain a'
b' : τ → MvPowerSeries υ T
hb' : MvPowerSeries.SubstDomain b'
a : A
σ : Type u_9
inst✝¹ : DecidableEq σ
inst✝ : Finite σ
p : MvPowerSeries σ R
hp_lin : ∀ (d : σ →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (MvPowerSeries.coeff R d) p = 0
f : R⟦X⟧
⊢ subst p (scale a f) = MvPowerSeries.scale (Function.const σ a) (subst p f)
Tactic:
have hp : PowerSeries.SubstDomain p := by
  apply substDomain_of_constantCoeff_zero
  rw [← MvPowerSeries.coeff_zero_eq_constantCoeff_apply]
  apply hp_lin
  simp only [Finsupp.sum_zero_index, ne_eq, zero_ne_one, not_false_eq_true]
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✝¹
υ : 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
a✝ : S⟦X⟧
ha : SubstDomain a✝
b : MvPowerSeries υ T
hb : SubstDomain b
a' : MvPowerSeries τ S
ha' : SubstDomain a'
b' : τ → MvPowerSeries υ T
hb' : MvPowerSeries.SubstDomain b'
a : A
σ : Type u_9
inst✝¹ : DecidableEq σ
inst✝ : Finite σ
p : MvPowerSeries σ R
hp_lin : ∀ (d : σ →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (MvPowerSeries.coeff R d) p = 0
f : R⟦X⟧
hp : SubstDomain p
⊢ subst p (scale a f) = MvPowerSeries.scale (Function.const σ a) (subst p f)
Theorem: PowerSeries.subst_linear_subst_scalar_comm
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✝¹
υ : 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
a✝ : S⟦X⟧
ha : SubstDomain a✝
b : MvPowerSeries υ T
hb : SubstDomain b
a' : MvPowerSeries τ S
ha' : SubstDomain a'
b' : τ → MvPowerSeries υ T
hb' : MvPowerSeries.SubstDomain b'
a : A
σ : Type u_9
inst✝¹ : DecidableEq σ
inst✝ : Finite σ
p : MvPowerSeries σ R
hp_lin : ∀ (d : σ →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (MvPowerSeries.coeff R d) p = 0
f : R⟦X⟧
hp : SubstDomain p
⊢ subst p (scale a f) = MvPowerSeries.scale (Function.const σ a) (subst p f)
Tactic:
rw [scale_eq_subst, MvPowerSeries.scale_eq_subst]
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✝¹
υ : 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
a✝ : S⟦X⟧
ha : SubstDomain a✝
b : MvPowerSeries υ T
hb : SubstDomain b
a' : MvPowerSeries τ S
ha' : SubstDomain a'
b' : τ → MvPowerSeries υ T
hb' : MvPowerSeries.SubstDomain b'
a : A
σ : Type u_9
inst✝¹ : DecidableEq σ
inst✝ : Finite σ
p : MvPowerSeries σ R
hp_lin : ∀ (d : σ →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (MvPowerSeries.coeff R d) p = 0
f : R⟦X⟧
hp : SubstDomain p
⊢ subst p (subst (a • X) f) = MvPowerSeries.subst (Function.const σ a • MvPowerSeries.X) (subst p f)
Theorem: PowerSeries.subst_linear_subst_scalar_comm
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✝¹
υ : 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
a✝ : S⟦X⟧
ha : SubstDomain a✝
b : MvPowerSeries υ T
hb : SubstDomain b
a' : MvPowerSeries τ S
ha' : SubstDomain a'
b' : τ → MvPowerSeries υ T
hb' : MvPowerSeries.SubstDomain b'
a : A
σ : Type u_9
inst✝¹ : DecidableEq σ
inst✝ : Finite σ
p : MvPowerSeries σ R
hp_lin : ∀ (d : σ →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (MvPowerSeries.coeff R d) p = 0
f : R⟦X⟧
hp : SubstDomain p
⊢ subst p (subst (a • X) f) = MvPowerSeries.subst (Function.const σ a • MvPowerSeries.X) (subst p f)
Tactic:
rw [subst_comp_subst_apply (substDomain_scale R _) hp]
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✝¹
υ : 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
a✝ : S⟦X⟧
ha : SubstDomain a✝
b : MvPowerSeries υ T
hb : SubstDomain b
a' : MvPowerSeries τ S
ha' : SubstDomain a'
b' : τ → MvPowerSeries υ T
hb' : MvPowerSeries.SubstDomain b'
a : A
σ : Type u_9
inst✝¹ : DecidableEq σ
inst✝ : Finite σ
p : MvPowerSeries σ R
hp_lin : ∀ (d : σ →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (MvPowerSeries.coeff R d) p = 0
f : R⟦X⟧
hp : SubstDomain p
⊢ subst (subst p (a • X)) f = MvPowerSeries.subst (Function.const σ a • MvPowerSeries.X) (subst p f)