Theorem: PowerSeries.coeff_subst_single (DividedPowers/ExponentialModule/Basic.lean)

State before:
A : Type u_1
inst✝⁶ : CommRing A
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Algebra A R
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
σ : Type u_4
inst✝¹ : DecidableEq σ
inst✝ : Finite σ
s : σ
f : R⟦X⟧
e : σ →₀ ℕ
⊢ (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X s) f) = if e = Finsupp.single s (e s) then (coeff R (e s)) f else 0
Tactic:
rw [PowerSeries.coeff_subst (PowerSeries.substDomain_of_constantCoeff_zero (by simp))]
State after:
A : Type u_1
inst✝⁶ : CommRing A
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Algebra A R
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
σ : Type u_4
inst✝¹ : DecidableEq σ
inst✝ : Finite σ
s : σ
f : R⟦X⟧
e : σ →₀ ℕ
⊢ ∑ᶠ (d : ℕ), (coeff R d) f • (MvPowerSeries.coeff R e) (MvPowerSeries.X s ^ d) =
    if e = Finsupp.single s (e s) then (coeff R (e s)) f else 0

State before:
A : Type u_1
inst✝⁶ : CommRing A
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Algebra A R
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
σ : Type u_4
inst✝¹ : DecidableEq σ
inst✝ : Finite σ
s : σ
f : R⟦X⟧
e : σ →₀ ℕ
⊢ ∑ᶠ (d : ℕ), (coeff R d) f • (MvPowerSeries.coeff R e) (MvPowerSeries.X s ^ d) =
    if e = Finsupp.single s (e s) then (coeff R (e s)) f else 0
Tactic:
rw [finsum_eq_single _ (e s)]
State after:
A : Type u_1
inst✝⁶ : CommRing A
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Algebra A R
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
σ : Type u_4
inst✝¹ : DecidableEq σ
inst✝ : Finite σ
s : σ
f : R⟦X⟧
e : σ →₀ ℕ
⊢ (coeff R (e s)) f • (MvPowerSeries.coeff R e) (MvPowerSeries.X s ^ e s) =
    if e = Finsupp.single s (e s) then (coeff R (e s)) f else 0

A : Type u_1
inst✝⁶ : CommRing A
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Algebra A R
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
σ : Type u_4
inst✝¹ : DecidableEq σ
inst✝ : Finite σ
s : σ
f : R⟦X⟧
e : σ →₀ ℕ
⊢ ∀ (x : ℕ), x ≠ e s → (coeff R x) f • (MvPowerSeries.coeff R e) (MvPowerSeries.X s ^ x) = 0

State before:
A : Type u_1
inst✝⁶ : CommRing A
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Algebra A R
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
σ : Type u_4
inst✝¹ : DecidableEq σ
inst✝ : Finite σ
s : σ
f : R⟦X⟧
e : σ →₀ ℕ
⊢ (MvPowerSeries.constantCoeff σ R) (MvPowerSeries.X s) = 0
Tactic:
simp
State after:
no goals

State before:
A : Type u_1
inst✝⁶ : CommRing A
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Algebra A R
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
σ : Type u_4
inst✝¹ : DecidableEq σ
inst✝ : Finite σ
s : σ
f : R⟦X⟧
e : σ →₀ ℕ
⊢ (coeff R (e s)) f • (MvPowerSeries.coeff R e) (MvPowerSeries.X s ^ e s) =
    if e = Finsupp.single s (e s) then (coeff R (e s)) f else 0
Tactic:
rw [MvPowerSeries.coeff_X_pow]
State after:
A : Type u_1
inst✝⁶ : CommRing A
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Algebra A R
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
σ : Type u_4
inst✝¹ : DecidableEq σ
inst✝ : Finite σ
s : σ
f : R⟦X⟧
e : σ →₀ ℕ
⊢ ((coeff R (e s)) f • if e = Finsupp.single s (e s) then 1 else 0) =
    if e = Finsupp.single s (e s) then (coeff R (e s)) f else 0

State before:
A : Type u_1
inst✝⁶ : CommRing A
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Algebra A R
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
σ : Type u_4
inst✝¹ : DecidableEq σ
inst✝ : Finite σ
s : σ
f : R⟦X⟧
e : σ →₀ ℕ
⊢ ((coeff R (e s)) f • if e = Finsupp.single s (e s) then 1 else 0) =
    if e = Finsupp.single s (e s) then (coeff R (e s)) f else 0
Tactic:
simp only [Fin.isValue, ↓reduceIte, smul_eq_mul, mul_one]
State after:
A : Type u_1
inst✝⁶ : CommRing A
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Algebra A R
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
σ : Type u_4
inst✝¹ : DecidableEq σ
inst✝ : Finite σ
s : σ
f : R⟦X⟧
e : σ →₀ ℕ
⊢ ((coeff R (e s)) f * if e = Finsupp.single s (e s) then 1 else 0) =
    if e = Finsupp.single s (e s) then (coeff R (e s)) f else 0

State before:
A : Type u_1
inst✝⁶ : CommRing A
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Algebra A R
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
σ : Type u_4
inst✝¹ : DecidableEq σ
inst✝ : Finite σ
s : σ
f : R⟦X⟧
e : σ →₀ ℕ
⊢ ((coeff R (e s)) f * if e = Finsupp.single s (e s) then 1 else 0) =
    if e = Finsupp.single s (e s) then (coeff R (e s)) f else 0
Tactic:
split_ifs with he
State after:
case pos
A : Type u_1
inst✝⁶ : CommRing A
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Algebra A R
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
σ : Type u_4
inst✝¹ : DecidableEq σ
inst✝ : Finite σ
s : σ
f : R⟦X⟧
e : σ →₀ ℕ
he : e = Finsupp.single s (e s)
⊢ (coeff R (e s)) f * 1 = (coeff R (e s)) f

case neg
A : Type u_1
inst✝⁶ : CommRing A
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Algebra A R
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
σ : Type u_4
inst✝¹ : DecidableEq σ
inst✝ : Finite σ
s : σ
f : R⟦X⟧
e : σ →₀ ℕ
he : ¬e = Finsupp.single s (e s)
⊢ (coeff R (e s)) f * 0 = 0

State before:
case pos
A : Type u_1
inst✝⁶ : CommRing A
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Algebra A R
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
σ : Type u_4
inst✝¹ : DecidableEq σ
inst✝ : Finite σ
s : σ
f : R⟦X⟧
e : σ →₀ ℕ
he : e = Finsupp.single s (e s)
⊢ (coeff R (e s)) f * 1 = (coeff R (e s)) f
Tactic:
rw [mul_one]
State after:
no goals

State before:
case neg
A : Type u_1
inst✝⁶ : CommRing A
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Algebra A R
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
σ : Type u_4
inst✝¹ : DecidableEq σ
inst✝ : Finite σ
s : σ
f : R⟦X⟧
e : σ →₀ ℕ
he : ¬e = Finsupp.single s (e s)
⊢ (coeff R (e s)) f * 0 = 0
Tactic:
rw [mul_zero]
State after:
no goals

State before:
A : Type u_1
inst✝⁶ : CommRing A
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Algebra A R
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
σ : Type u_4
inst✝¹ : DecidableEq σ
inst✝ : Finite σ
s : σ
f : R⟦X⟧
e : σ →₀ ℕ
⊢ ∀ (x : ℕ), x ≠ e s → (coeff R x) f • (MvPowerSeries.coeff R e) (MvPowerSeries.X s ^ x) = 0
Tactic:
intro d hd
State after:
A : Type u_1
inst✝⁶ : CommRing A
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Algebra A R
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
σ : Type u_4
inst✝¹ : DecidableEq σ
inst✝ : Finite σ
s : σ
f : R⟦X⟧
e : σ →₀ ℕ
d : ℕ
hd : d ≠ e s
⊢ (coeff R d) f • (MvPowerSeries.coeff R e) (MvPowerSeries.X s ^ d) = 0

State before:
A : Type u_1
inst✝⁶ : CommRing A
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Algebra A R
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
σ : Type u_4
inst✝¹ : DecidableEq σ
inst✝ : Finite σ
s : σ
f : R⟦X⟧
e : σ →₀ ℕ
d : ℕ
hd : d ≠ e s
⊢ (coeff R d) f • (MvPowerSeries.coeff R e) (MvPowerSeries.X s ^ d) = 0
Tactic:
simp only [MvPowerSeries.coeff_X_pow, smul_eq_mul, mul_ite, mul_one, mul_zero, ite_eq_right_iff]
State after:
A : Type u_1
inst✝⁶ : CommRing A
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Algebra A R
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
σ : Type u_4
inst✝¹ : DecidableEq σ
inst✝ : Finite σ
s : σ
f : R⟦X⟧
e : σ →₀ ℕ
d : ℕ
hd : d ≠ e s
⊢ e = Finsupp.single s d → (coeff R d) f = 0

State before:
A : Type u_1
inst✝⁶ : CommRing A
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Algebra A R
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
σ : Type u_4
inst✝¹ : DecidableEq σ
inst✝ : Finite σ
s : σ
f : R⟦X⟧
e : σ →₀ ℕ
d : ℕ
hd : d ≠ e s
⊢ e = Finsupp.single s d → (coeff R d) f = 0
Tactic:
intro hd'
State after:
A : Type u_1
inst✝⁶ : CommRing A
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Algebra A R
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
σ : Type u_4
inst✝¹ : DecidableEq σ
inst✝ : Finite σ
s : σ
f : R⟦X⟧
e : σ →₀ ℕ
d : ℕ
hd : d ≠ e s
hd' : e = Finsupp.single s d
⊢ (coeff R d) f = 0

State before:
A : Type u_1
inst✝⁶ : CommRing A
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Algebra A R
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
σ : Type u_4
inst✝¹ : DecidableEq σ
inst✝ : Finite σ
s : σ
f : R⟦X⟧
e : σ →₀ ℕ
d : ℕ
hd : d ≠ e s
hd' : e = Finsupp.single s d
⊢ (coeff R d) f = 0
Tactic:
simp only [hd', Finsupp.single_eq_same, ne_eq, not_true_eq_false] at hd
State after:
no goals