internlm/Lean-Github huggingface dataset:
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 (subst p (a • X)) f = MvPowerSeries.subst (Function.const σ a • MvPowerSeries.X) (subst p f)
Tactic:
nth_rewrite 3 [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 (subst p (a • X)) f =
    MvPowerSeries.subst (Function.const σ a • MvPowerSeries.X) (MvPowerSeries.subst (fun x => 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 (subst p (a • X)) f =
    MvPowerSeries.subst (Function.const σ a • MvPowerSeries.X) (MvPowerSeries.subst (fun x => p) f)
Tactic:
rw [MvPowerSeries.subst_comp_subst_apply hp.const (MvPowerSeries.substDomain_scale R _)]
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 (fun s => MvPowerSeries.subst (Function.const σ a • MvPowerSeries.X) 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 (subst p (a • X)) f =
    MvPowerSeries.subst (fun s => MvPowerSeries.subst (Function.const σ a • MvPowerSeries.X) p) f
Tactic:
rw [Function.funext_iff]
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
⊢ ∀ (a_1 : σ →₀ ℕ),
    subst (subst p (a • X)) f a_1 =
      MvPowerSeries.subst (fun s => MvPowerSeries.subst (Function.const σ a • MvPowerSeries.X) p) f a_1
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
⊢ ∀ (a_1 : σ →₀ ℕ),
    subst (subst p (a • X)) f a_1 =
      MvPowerSeries.subst (fun s => MvPowerSeries.subst (Function.const σ a • MvPowerSeries.X) p) f a_1
Tactic:
intro _
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
a✝ : σ →₀ ℕ
⊢ subst (subst p (a • X)) f a✝ =
    MvPowerSeries.subst (fun s => MvPowerSeries.subst (Function.const σ a • MvPowerSeries.X) p) f a✝
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
a✝ : σ →₀ ℕ
⊢ subst (subst p (a • X)) f a✝ =
    MvPowerSeries.subst (fun s => MvPowerSeries.subst (Function.const σ a • MvPowerSeries.X) p) f a✝
Tactic:
rw [subst_smul hp, ← Polynomial.coe_X, subst_coe hp, Polynomial.aeval_X]
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
a✝ : σ →₀ ℕ
⊢ subst (a • p) f a✝ = MvPowerSeries.subst (fun s => MvPowerSeries.subst (Function.const σ a • MvPowerSeries.X) p) f a✝
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
a✝ : σ →₀ ℕ
⊢ subst (a • p) f a✝ = MvPowerSeries.subst (fun s => MvPowerSeries.subst (Function.const σ a • MvPowerSeries.X) p) f a✝
Tactic:
rw [← 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
a✝ : σ →₀ ℕ
⊢ subst (a • p) f a✝ = MvPowerSeries.subst (fun s => MvPowerSeries.scale (Function.const σ a) p) f a✝
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
a✝ : σ →₀ ℕ
⊢ subst (a • p) f a✝ = MvPowerSeries.subst (fun s => MvPowerSeries.scale (Function.const σ a) p) f a✝
Tactic:
rw [MvPowerSeries.scale_linear_eq_smul _ _ hp_lin]
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
a✝ : σ →₀ ℕ
⊢ subst (a • p) f a✝ = MvPowerSeries.subst (fun s => a • p) f a✝
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
a✝ : σ →₀ ℕ
⊢ subst (a • p) f a✝ = MvPowerSeries.subst (fun s => a • p) f a✝
Tactic:
rfl
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⟧
⊢ SubstDomain p
Tactic:
apply substDomain_of_constantCoeff_zero
Proof state after:
case ha
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⟧
⊢ (MvPowerSeries.constantCoeff σ R) p = 0
Theorem: PowerSeries.subst_linear_subst_scalar_comm
Proof state before:
case ha
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⟧
⊢ (MvPowerSeries.constantCoeff σ R) p = 0
Tactic:
rw [← MvPowerSeries.coeff_zero_eq_constantCoeff_apply]
Proof state after:
case ha
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⟧
⊢ (MvPowerSeries.coeff R 0) p = 0
Theorem: PowerSeries.subst_linear_subst_scalar_comm
Proof state before:
case ha
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⟧
⊢ (MvPowerSeries.coeff R 0) p = 0
Tactic:
apply hp_lin
Proof state after:
case ha.a
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⟧
⊢ (Finsupp.sum 0 fun x n => n) ≠ 1
Theorem: PowerSeries.subst_linear_subst_scalar_comm
Proof state before:
case ha.a
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⟧
⊢ (Finsupp.sum 0 fun x n => n) ≠ 1
Tactic:
simp only [Finsupp.sum_zero_index, ne_eq, zero_ne_one, not_false_eq_true]
Proof state after:
no goals