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

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

State before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
s : Set ι
d : σ →₀ ℕ
⊢ (support fun i => (coeff α d) ((fun i => s.indicator f i) i)).Finite
Tactic:
apply (hf d).subset
State after:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
s : Set ι
d : σ →₀ ℕ
⊢ (support fun i => (coeff α d) ((fun i => s.indicator 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 σ α
hf : StronglySummable f
s : Set ι
d : σ →₀ ℕ
⊢ (support fun i => (coeff α d) ((fun i => s.indicator f i) 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 σ α
hf : StronglySummable f
s : Set ι
d : σ →₀ ℕ
i : ι
⊢ (i ∈ support fun i => (coeff α d) ((fun i => s.indicator f i) 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 σ α
hf : StronglySummable f
s : Set ι
d : σ →₀ ℕ
i : ι
⊢ (i ∈ support fun i => (coeff α d) ((fun i => s.indicator f i) i)) → i ∈ support fun i => (coeff α d) (f i)
Tactic:
simp only [mem_support, ne_eq, not_imp_not]
State after:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
s : Set ι
d : σ →₀ ℕ
i : ι
⊢ (coeff α d) (f i) = 0 → (coeff α d) (s.indicator f i) = 0

State before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
s : Set ι
d : σ →₀ ℕ
i : ι
⊢ (coeff α d) (f i) = 0 → (coeff α d) (s.indicator f i) = 0
Tactic:
intro hi
State after:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
s : Set ι
d : σ →₀ ℕ
i : ι
hi : (coeff α d) (f i) = 0
⊢ (coeff α d) (s.indicator f i) = 0

State before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
s : Set ι
d : σ →₀ ℕ
i : ι
hi : (coeff α d) (f i) = 0
⊢ (coeff α d) (s.indicator f i) = 0
Tactic:
cases' s.indicator_eq_zero_or_self f i with h h <;>
. simp only [h, hi, map_zero]
State after:
no goals

State before:
case inr
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
s : Set ι
d : σ →₀ ℕ
i : ι
hi : (coeff α d) (f i) = 0
h : s.indicator f i = f i
⊢ (coeff α d) (s.indicator f i) = 0
Tactic:
simp only [h, hi, map_zero]
State after:
no goals