Theorem: MvPowerSeries.StronglySummable.on_subtype (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 (f ∘ Subtype.val)
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) ((f ∘ Subtype.val) 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) ((f ∘ Subtype.val) i)).Finite
Tactic:
apply Finite.of_finite_image _ (injOn_of_injective Subtype.coe_injective _)
State after:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
s : Set ι
d : σ →₀ ℕ
⊢ ((fun a => ↑a) '' support fun i => (coeff α d) ((f ∘ Subtype.val) 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 : σ →₀ ℕ
⊢ ((fun a => ↑a) '' support fun i => (coeff α d) ((f ∘ Subtype.val) 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 : σ →₀ ℕ
⊢ ((fun a => ↑a) '' support fun i => (coeff α d) ((f ∘ Subtype.val) 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 : σ →₀ ℕ
⊢ ((fun a => ↑a) '' support fun i => (coeff α d) ((f ∘ Subtype.val) i)) ⊆ support fun i => (coeff α d) (f i)
Tactic:
rintro i ⟨j, hj, rfl⟩
State after:
case intro.intro
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
s : Set ι
d : σ →₀ ℕ
j : { x // x ∈ s }
hj : j ∈ support fun i => (coeff α d) ((f ∘ Subtype.val) i)
⊢ (fun a => ↑a) j ∈ support fun i => (coeff α d) (f i)

State before:
case intro.intro
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
s : Set ι
d : σ →₀ ℕ
j : { x // x ∈ s }
hj : j ∈ support fun i => (coeff α d) ((f ∘ Subtype.val) i)
⊢ (fun a => ↑a) j ∈ support fun i => (coeff α d) (f i)
Tactic:
simp only [comp_apply, mem_support, ne_eq] at hj ⊢
State after:
case intro.intro
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
s : Set ι
d : σ →₀ ℕ
j : { x // x ∈ s }
hj : ¬(coeff α d) (f ↑j) = 0
⊢ ¬(coeff α d) (f ↑j) = 0

State before:
case intro.intro
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
s : Set ι
d : σ →₀ ℕ
j : { x // x ∈ s }
hj : ¬(coeff α d) (f ↑j) = 0
⊢ ¬(coeff α d) (f ↑j) = 0
Tactic:
exact hj
State after:
no goals