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

State before:
α : Type u_1
s✝ : Set α
ι : Type u_2
s : ι → Set α
a : Set ι
ha : a.Infinite
hs : InjOn s a
⊢ (⋃ i ∈ a, s i).Infinite
Tactic:
rw [biUnion_eq_iUnion]
State after:
α : Type u_1
s✝ : Set α
ι : Type u_2
s : ι → Set α
a : Set ι
ha : a.Infinite
hs : InjOn s a
⊢ (⋃ x, s ↑x).Infinite

State before:
α : Type u_1
s✝ : Set α
ι : Type u_2
s : ι → Set α
a : Set ι
ha : a.Infinite
hs : InjOn s a
⊢ (⋃ x, s ↑x).Infinite
Tactic:
have _ := ha.to_subtype
State after:
α : Type u_1
s✝ : Set α
ι : Type u_2
s : ι → Set α
a : Set ι
ha : a.Infinite
hs : InjOn s a
x✝ : Infinite ↑a
⊢ (⋃ x, s ↑x).Infinite

State before:
α : Type u_1
s✝ : Set α
ι : Type u_2
s : ι → Set α
a : Set ι
ha : a.Infinite
hs : InjOn s a
x✝ : Infinite ↑a
⊢ (⋃ x, s ↑x).Infinite
Tactic:
exact infinite_iUnion fun ⟨i,hi⟩ ⟨j,hj⟩ hij ↦ by simp [hs hi hj hij]
State after:
no goals

State before:
α : Type u_1
s✝ : Set α
ι : Type u_2
s : ι → Set α
a : Set ι
ha : a.Infinite
hs : InjOn s a
x✝² : Infinite ↑a
x✝¹ x✝ : ↑a
i : ι
hi : i ∈ a
j : ι
hj : j ∈ a
hij : s ↑⟨i, hi⟩ = s ↑⟨j, hj⟩
⊢ ⟨i, hi⟩ = ⟨j, hj⟩
Tactic:
simp [hs hi hj hij]
State after:
no goals