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

State before:
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι : Type u_3
inst✝¹ : Semiring α
inst✝ : DecidableEq ι
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
⊢ {I | I ⊆ hf.unionOfSupportOfCoeffLe d}.Finite
Tactic:
suffices {I : Finset ι | I ⊆ hf.unionOfSupportOfCoeffLe  d} =
  (hf.unionOfSupportOfCoeffLe  d).powerset by
  rw [this]; apply finite_toSet
State after:
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι : Type u_3
inst✝¹ : Semiring α
inst✝ : DecidableEq ι
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
⊢ {I | I ⊆ hf.unionOfSupportOfCoeffLe d} = ↑(hf.unionOfSupportOfCoeffLe d).powerset

State before:
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι : Type u_3
inst✝¹ : Semiring α
inst✝ : DecidableEq ι
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
⊢ {I | I ⊆ hf.unionOfSupportOfCoeffLe d} = ↑(hf.unionOfSupportOfCoeffLe d).powerset
Tactic:
ext I
State after:
case h
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι : Type u_3
inst✝¹ : Semiring α
inst✝ : DecidableEq ι
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
I : Finset ι
⊢ I ∈ {I | I ⊆ hf.unionOfSupportOfCoeffLe d} ↔ I ∈ ↑(hf.unionOfSupportOfCoeffLe d).powerset

State before:
case h
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι : Type u_3
inst✝¹ : Semiring α
inst✝ : DecidableEq ι
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
I : Finset ι
⊢ I ∈ {I | I ⊆ hf.unionOfSupportOfCoeffLe d} ↔ I ∈ ↑(hf.unionOfSupportOfCoeffLe d).powerset
Tactic:
simp only [mem_setOf_eq, coe_powerset, Set.mem_preimage, mem_powerset_iff, Finset.coe_subset]
State after:
no goals

State before:
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι : Type u_3
inst✝¹ : Semiring α
inst✝ : DecidableEq ι
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
this : {I | I ⊆ hf.unionOfSupportOfCoeffLe d} = ↑(hf.unionOfSupportOfCoeffLe d).powerset
⊢ {I | I ⊆ hf.unionOfSupportOfCoeffLe d}.Finite
Tactic:
rw [this]
State after:
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι : Type u_3
inst✝¹ : Semiring α
inst✝ : DecidableEq ι
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
this : {I | I ⊆ hf.unionOfSupportOfCoeffLe d} = ↑(hf.unionOfSupportOfCoeffLe d).powerset
⊢ (↑(hf.unionOfSupportOfCoeffLe d).powerset).Finite

State before:
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι : Type u_3
inst✝¹ : Semiring α
inst✝ : DecidableEq ι
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
this : {I | I ⊆ hf.unionOfSupportOfCoeffLe d} = ↑(hf.unionOfSupportOfCoeffLe d).powerset
⊢ (↑(hf.unionOfSupportOfCoeffLe d).powerset).Finite
Tactic:
apply finite_toSet
State after:
no goals