Theorem: MvPowerSeries.StronglySummable.smul (DividedPowers/ForMathlib/MvPowerSeries/StronglySummable/Basic.lean)

State before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
a : ι → α
hf : StronglySummable f
⊢ StronglySummable (a • f)
Tactic:
intro d
State after:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
a : ι → α
hf : StronglySummable f
d : σ →₀ ℕ
⊢ (support fun i => (coeff α d) ((a • f) i)).Finite

State before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
a : ι → α
hf : StronglySummable f
d : σ →₀ ℕ
⊢ (support fun i => (coeff α d) ((a • f) i)).Finite
Tactic:
apply Finite.subset (hf d)
State after:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
a : ι → α
hf : StronglySummable f
d : σ →₀ ℕ
⊢ (support fun i => (coeff α d) ((a • f) i)) ⊆ support fun i => (coeff α d) (f i)

State before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
a : ι → α
hf : StronglySummable f
d : σ →₀ ℕ
⊢ (support fun i => (coeff α d) ((a • f) i)) ⊆ support fun i => (coeff α d) (f i)
Tactic:
intro i
State after:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
a : ι → α
hf : StronglySummable f
d : σ →₀ ℕ
i : ι
⊢ (i ∈ support fun i => (coeff α d) ((a • f) i)) → i ∈ support fun i => (coeff α d) (f i)

State before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
a : ι → α
hf : StronglySummable f
d : σ →₀ ℕ
i : ι
⊢ (i ∈ support fun i => (coeff α d) ((a • f) i)) → i ∈ support fun i => (coeff α d) (f i)
Tactic:
simp only [Pi.smul_apply', Pi.smul_apply, Function.mem_support, ne_eq]
State after:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
a : ι → α
hf : StronglySummable f
d : σ →₀ ℕ
i : ι
⊢ ¬(coeff α d) (a i • f i) = 0 → ¬(coeff α d) (f i) = 0

State before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
a : ι → α
hf : StronglySummable f
d : σ →₀ ℕ
i : ι
⊢ ¬(coeff α d) (a i • f i) = 0 → ¬(coeff α d) (f i) = 0
Tactic:
intro h h'
State after:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
a : ι → α
hf : StronglySummable f
d : σ →₀ ℕ
i : ι
h : ¬(coeff α d) (a i • f i) = 0
h' : (coeff α d) (f i) = 0
⊢ False

State before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
a : ι → α
hf : StronglySummable f
d : σ →₀ ℕ
i : ι
h : ¬(coeff α d) (a i • f i) = 0
h' : (coeff α d) (f i) = 0
⊢ False
Tactic:
apply h
State after:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
a : ι → α
hf : StronglySummable f
d : σ →₀ ℕ
i : ι
h : ¬(coeff α d) (a i • f i) = 0
h' : (coeff α d) (f i) = 0
⊢ (coeff α d) (a i • f i) = 0

State before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
a : ι → α
hf : StronglySummable f
d : σ →₀ ℕ
i : ι
h : ¬(coeff α d) (a i • f i) = 0
h' : (coeff α d) (f i) = 0
⊢ (coeff α d) (a i • f i) = 0
Tactic:
rw [coeff_smul, h', MulZeroClass.mul_zero]
State after:
no goals