Theorem: toSubset_iUnion (Sard/ToSubset.lean)

State before:
X : Type u_1
t : Set X
S : ℕ → Set X
⊢ (⋃ n, S n).toSubset t = ⋃ n, (S n).toSubset t
Tactic:
ext
State after:
case h
X : Type u_1
t : Set X
S : ℕ → Set X
x✝ : ↑t
⊢ x✝ ∈ (⋃ n, S n).toSubset t ↔ x✝ ∈ ⋃ n, (S n).toSubset t

State before:
case h
X : Type u_1
t : Set X
S : ℕ → Set X
x✝ : ↑t
⊢ x✝ ∈ (⋃ n, S n).toSubset t ↔ x✝ ∈ ⋃ n, (S n).toSubset t
Tactic:
rw [mem_toSubset]
State after:
case h
X : Type u_1
t : Set X
S : ℕ → Set X
x✝ : ↑t
⊢ ↑x✝ ∈ ⋃ n, S n ↔ x✝ ∈ ⋃ n, (S n).toSubset t

State before:
case h
X : Type u_1
t : Set X
S : ℕ → Set X
x✝ : ↑t
⊢ ↑x✝ ∈ ⋃ n, S n ↔ x✝ ∈ ⋃ n, (S n).toSubset t
Tactic:
sorry
State after:
no goals