Theorem: Filter.clusterPt_principal_subtype_iff_frequently (Sion/ForMathlib/Misc.lean)

State before:
α✝ : Type ?u.2106
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
hst : s ⊆ t
J : Set ↑s
a : ↑s
⊢ ClusterPt a (𝓟 J) ↔ ∃ᶠ (x : α) in nhdsWithin (↑a) t, ∃ (h : x ∈ s), { val := x, property := h } ∈ J
Tactic:
rw [nhdsWithin_eq_map_subtype_coe (hst a.prop), Filter.frequently_map,
  clusterPt_principal_iff_frequently, inducing_subtype_val.nhds_eq_comap, Filter.frequently_comap,
  inducing_subtype_val.nhds_eq_comap, Filter.frequently_comap, Subtype.coe_mk]
State after:
α✝ : Type ?u.2106
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
hst : s ⊆ t
J : Set ↑s
a : ↑s
⊢ (∃ᶠ (b : α) in nhds ↑a, ∃ a, ↑a = b ∧ a ∈ J) ↔
    ∃ᶠ (b : α) in nhds ↑a, ∃ a, ↑a = b ∧ ∃ (h : ↑a ∈ s), { val := ↑a, property := h } ∈ J

State before:
α✝ : Type ?u.2106
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
hst : s ⊆ t
J : Set ↑s
a : ↑s
⊢ (∃ᶠ (b : α) in nhds ↑a, ∃ a, ↑a = b ∧ a ∈ J) ↔
    ∃ᶠ (b : α) in nhds ↑a, ∃ a, ↑a = b ∧ ∃ (h : ↑a ∈ s), { val := ↑a, property := h } ∈ J
Tactic:
apply frequently_congr
State after:
case h
α✝ : Type ?u.2106
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
hst : s ⊆ t
J : Set ↑s
a : ↑s
⊢ ∀ᶠ (x : α) in nhds ↑a, (∃ a, ↑a = x ∧ a ∈ J) ↔ ∃ a, ↑a = x ∧ ∃ (h : ↑a ∈ s), { val := ↑a, property := h } ∈ J

State before:
case h
α✝ : Type ?u.2106
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
hst : s ⊆ t
J : Set ↑s
a : ↑s
⊢ ∀ᶠ (x : α) in nhds ↑a, (∃ a, ↑a = x ∧ a ∈ J) ↔ ∃ a, ↑a = x ∧ ∃ (h : ↑a ∈ s), { val := ↑a, property := h } ∈ J
Tactic:
apply eventually_of_forall
State after:
case h.hp
α✝ : Type ?u.2106
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
hst : s ⊆ t
J : Set ↑s
a : ↑s
⊢ ∀ (x : α), (∃ a, ↑a = x ∧ a ∈ J) ↔ ∃ a, ↑a = x ∧ ∃ (h : ↑a ∈ s), { val := ↑a, property := h } ∈ J

State before:
case h.hp
α✝ : Type ?u.2106
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
hst : s ⊆ t
J : Set ↑s
a : ↑s
⊢ ∀ (x : α), (∃ a, ↑a = x ∧ a ∈ J) ↔ ∃ a, ↑a = x ∧ ∃ (h : ↑a ∈ s), { val := ↑a, property := h } ∈ J
Tactic:
intro x
State after:
case h.hp
α✝ : Type ?u.2106
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
hst : s ⊆ t
J : Set ↑s
a : ↑s
x : α
⊢ (∃ a, ↑a = x ∧ a ∈ J) ↔ ∃ a, ↑a = x ∧ ∃ (h : ↑a ∈ s), { val := ↑a, property := h } ∈ J

State before:
case h.hp
α✝ : Type ?u.2106
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
hst : s ⊆ t
J : Set ↑s
a : ↑s
x : α
⊢ (∃ a, ↑a = x ∧ a ∈ J) ↔ ∃ a, ↑a = x ∧ ∃ (h : ↑a ∈ s), { val := ↑a, property := h } ∈ J
Tactic:
simp only [Subtype.coe_mk, SetCoe.exists, exists_and_left, exists_eq_left]
State after:
case h.hp
α✝ : Type ?u.2106
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
hst : s ⊆ t
J : Set ↑s
a : ↑s
x : α
⊢ (∃ (x_1 : x ∈ s), { val := x, property := ⋯ } ∈ J) ↔ ∃ (x_1 : x ∈ t) (h : x ∈ s), { val := x, property := ⋯ } ∈ J

State before:
case h.hp
α✝ : Type ?u.2106
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
hst : s ⊆ t
J : Set ↑s
a : ↑s
x : α
⊢ (∃ (x_1 : x ∈ s), { val := x, property := ⋯ } ∈ J) ↔ ∃ (x_1 : x ∈ t) (h : x ∈ s), { val := x, property := ⋯ } ∈ J
Tactic:
exact ⟨fun ⟨h, hx⟩ => ⟨hst h, h, hx⟩, fun ⟨_, hx⟩ => hx⟩
State after:
no goals