Theorem: Set.Infinite.sUnion (Matroid/ForMathlib/Data/Set/Finite.lean)

State before:
α : Type u_1
s✝ : Set α
s : Set (Set α)
hs : s.Infinite
⊢ (⋃₀ s).Infinite
Tactic:
rw [sUnion_eq_iUnion]
State after:
α : Type u_1
s✝ : Set α
s : Set (Set α)
hs : s.Infinite
⊢ (⋃ i, ↑i).Infinite

State before:
α : Type u_1
s✝ : Set α
s : Set (Set α)
hs : s.Infinite
⊢ (⋃ i, ↑i).Infinite
Tactic:
have _ := hs.to_subtype
State after:
α : Type u_1
s✝ : Set α
s : Set (Set α)
hs : s.Infinite
x✝ : Infinite ↑s
⊢ (⋃ i, ↑i).Infinite

State before:
α : Type u_1
s✝ : Set α
s : Set (Set α)
hs : s.Infinite
x✝ : Infinite ↑s
⊢ (⋃ i, ↑i).Infinite
Tactic:
exact infinite_iUnion Subtype.coe_injective
State after:
no goals