awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hs : IsLindelof s
ht : IsClosed[inst] t
h : t ⊆ s
⊢ IsLindelof t

Tactic:
inter_eq_self_of_subset_right h ▸ hs.inter_right ht

Premises used: Eq.rec, Set.inter_eq_self_of_subset_right, IsLindelof.inter_right
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
hs : IsLindelof s
hf : ContinuousOn f s
l : Filter Y
lne : l.NeBot
_ : ∀ [CountableInterFilter l], l ≤ 𝓟 (f '' s) → ∃ x ∈ f '' s, ClusterPt x l
⊢ ∀ [CountableInterFilter l], l ≤ 𝓟 (f '' s) → ∃ x ∈ f '' s, ClusterPt x l

Tactic:
_
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
hs : IsLindelof s
hf : ContinuousOn f s
l : Filter Y
lne : l.NeBot
inst_2 : CountableInterFilter l
ls : l ≤ 𝓟 (f '' s)
⊢ (comap f l ⊓ 𝓟 s).NeBot

Tactic:
have : NeBot (l.comap f ⊓ 𝓟 s) :=
    comap_inf_principal_neBot_of_image_mem lne (le_principal_iff.1 ls)
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
hs : IsLindelof s
hf : ContinuousOn f s
l : Filter Y
lne : l.NeBot
inst_2 : CountableInterFilter l
ls : l ≤ 𝓟 (f '' s)
this : (comap f l ⊓ 𝓟 s).NeBot
⊢ ∃ x ∈ s, ClusterPt x (comap f l ⊓ 𝓟 s)

Tactic:
@hs _ this _ inf_le_right

Premises used: inf_le_right
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
hs : IsLindelof s
hf : ContinuousOn f s
l : Filter Y
lne : l.NeBot
inst_2 : CountableInterFilter l
ls : l ≤ 𝓟 (f '' s)
this : (comap f l ⊓ 𝓟 s).NeBot
obtain : ∀ (x : X) (hxs : x ∈ s) (hx : ClusterPt x (comap f l ⊓ 𝓟 s)), ∃ x ∈ f '' s, ClusterPt x l
⊢ ∃ x ∈ f '' s, ClusterPt x l

Tactic:
obtain ⟨x, hxs, hx⟩ : ∃ x ∈ s, ClusterPt x (l.comap f ⊓ 𝓟 s) := @hs _ this _ inf_le_right

Premises used: inf_le_right
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
hs : IsLindelof s
hf : ContinuousOn f s
l : Filter Y
lne : l.NeBot
inst_2 : CountableInterFilter l
ls : l ≤ 𝓟 (f '' s)
this : (comap f l ⊓ 𝓟 s).NeBot
x : X
hxs : x ∈ s
hx : ClusterPt x (comap f l ⊓ 𝓟 s)
⊢ (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)).NeBot

Tactic:
haveI := hx.neBot
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
hs : IsLindelof s
hf : ContinuousOn f s
l : Filter Y
lne : l.NeBot
inst_2 : CountableInterFilter l
ls : l ≤ 𝓟 (f '' s)
this_1 : (comap f l ⊓ 𝓟 s).NeBot
x : X
hxs : x ∈ s
hx : ClusterPt x (comap f l ⊓ 𝓟 s)
this : (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)).NeBot
right : ClusterPt (f x) l
⊢ ∃ x ∈ f '' s, ClusterPt x l

Tactic:
use f x, mem_image_of_mem f hxs

Premises used: Set.mem_image_of_mem
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
hs : IsLindelof s
hf : ContinuousOn f s
l : Filter Y
lne : l.NeBot
inst_2 : CountableInterFilter l
ls : l ≤ 𝓟 (f '' s)
this_1 : (comap f l ⊓ 𝓟 s).NeBot
x : X
hxs : x ∈ s
hx : ClusterPt x (comap f l ⊓ 𝓟 s)
this : (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)).NeBot
⊢ Tendsto f (𝓝[s] x ⊓ comap f l) (𝓝 (f x) ⊓ l)

Tactic:
(hf x hxs).inf (@tendsto_comap _ _ f l)

Premises used: Filter.tendsto_comap, Filter.Tendsto.inf
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
hs : IsLindelof s
hf : ContinuousOn f s
l : Filter Y
lne : l.NeBot
inst_2 : CountableInterFilter l
ls : l ≤ 𝓟 (f '' s)
this_1 : (comap f l ⊓ 𝓟 s).NeBot
x : X
hxs : x ∈ s
hx : ClusterPt x (comap f l ⊓ 𝓟 s)
this : (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)).NeBot
h : 𝓝 x ⊓ (comap f l ⊓ 𝓟 s) = 𝓝[s] x ⊓ comap f l
⊢ Tendsto f (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)) (𝓝 (f x) ⊓ l)

Tactic:
convert! (hf x hxs).inf (@tendsto_comap _ _ f l) using 1

Premises used: Filter.tendsto_comap, Filter.Tendsto.inf
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
hs : IsLindelof s
hf : ContinuousOn f s
l : Filter Y
lne : l.NeBot
inst_2 : CountableInterFilter l
ls : l ≤ 𝓟 (f '' s)
this_1 : (comap f l ⊓ 𝓟 s).NeBot
x : X
hxs : x ∈ s
hx : ClusterPt x (comap f l ⊓ 𝓟 s)
this : (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)).NeBot
⊢ 𝓝 x ⊓ (comap f l ⊓ 𝓟 s) = 𝓝 x ⊓ 𝓟 s ⊓ comap f l

Tactic:
ac_rfl
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
hs : IsLindelof s
hf : ContinuousOn f s
l : Filter Y
lne : l.NeBot
inst_2 : CountableInterFilter l
ls : l ≤ 𝓟 (f '' s)
this_1 : (comap f l ⊓ 𝓟 s).NeBot
x : X
hxs : x ∈ s
hx : ClusterPt x (comap f l ⊓ 𝓟 s)
this : (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)).NeBot
⊢ Tendsto f (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)) (𝓝 (f x) ⊓ l)

Tactic:
have : Tendsto f (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)) (𝓝 (f x) ⊓ l) := by
    convert! (hf x hxs).inf (@tendsto_comap _ _ f l) using 1
    rw [nhdsWithin]
    ac_rfl
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
hs : IsLindelof s
hf : ContinuousOn f s
l : Filter Y
lne : l.NeBot
inst_2 : CountableInterFilter l
ls : l ≤ 𝓟 (f '' s)
this_1 : (comap f l ⊓ 𝓟 s).NeBot
x : X
hxs : x ∈ s
hx : ClusterPt x (comap f l ⊓ 𝓟 s)
this_2 : (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)).NeBot
this : Tendsto f (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)) (𝓝 (f x) ⊓ l)
⊢ ClusterPt (f x) l

Tactic:
this.neBot

Premises used: ClusterPt, Filter.Tendsto.neBot
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
hs : IsLindelof s
hf : ContinuousOn f s
l : Filter Y
lne : l.NeBot
inst_2 : CountableInterFilter l
ls : l ≤ 𝓟 (f '' s)
this_1 : (comap f l ⊓ 𝓟 s).NeBot
x : X
hxs : x ∈ s
hx : ClusterPt x (comap f l ⊓ 𝓟 s)
this_2 : (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)).NeBot
this : Tendsto f (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)) (𝓝 (f x) ⊓ l)
⊢ ClusterPt (f x) l

Tactic:
exact this.neBot

Premises used: Filter.Tendsto.neBot
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
hs : IsLindelof s
hf : Continuous[inst, inst_1] f
⊢ IsLindelof (f '' s)

Tactic:
hs.image_of_continuousOn hf.continuousOn

Premises used: Continuous.continuousOn, IsLindelof.image_of_continuousOn
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
f : Filter X
inst_1 : CountableInterFilter f
hs : IsLindelof s
hf₂ : f ≤ 𝓟 s
ht₁ : IsOpen[inst] t
ht₂ : ∀ x ∈ s, ClusterPt x f → x ∈ t
⊢ t ∈ f

Tactic:
(eq_or_neBot _).casesOn mem_of_eq_bot fun _ ↦
    let ⟨x, hx, hfx⟩ := @hs (f ⊓ 𝓟 tᶜ) _ _ <| inf_le_of_left_le hf₂
    have : x ∈ t := ht₂ x hx hfx.of_inf_left
    have : tᶜ ∩ t ∈ 𝓝[tᶜ] x := inter_mem_nhdsWithin _ (ht₁.mem_nhds this)
    have A : 𝓝[tᶜ] x = ⊥ := empty_mem_iff_bot.1 <| compl_inter_self t ▸ this
    have : 𝓝[tᶜ] x ≠ ⊥ := hfx.of_inf_right.ne
    absurd A this

Premises used: Or.casesOn, Filter.eq_or_neBot
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊆ ⋃ (i : ι), U i
s_1 : Set X
_ :
  ∀ ⦃t : Set X⦄,
    s_1 ⊆ t → (∃ (r : Set ι), r.Countable ∧ t ⊆ ⋃ i ∈ r, U i) → ∃ (r : Set ι), r.Countable ∧ s_1 ⊆ ⋃ i ∈ r, U i
⊢ ∀ ⦃t : Set X⦄,
    s_1 ⊆ t → (∃ (r : Set ι), r.Countable ∧ t ⊆ ⋃ i ∈ r, U i) → ∃ (r : Set ι), r.Countable ∧ s_1 ⊆ ⋃ i ∈ r, U i

Tactic:
_
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊆ ⋃ (i : ι), U i
s_1 t : Set X
hst : s_1 ⊆ t
this :
  ∀ (r : Set ι) (hrcountable : r.Countable) (hsub : t ⊆ ⋃ i ∈ r, U i), ∃ (r : Set ι), r.Countable ∧ s_1 ⊆ ⋃ i ∈ r, U i
⊢ (∃ (r : Set ι), r.Countable ∧ t ⊆ ⋃ i ∈ r, U i) → ∃ (r : Set ι), r.Countable ∧ s_1 ⊆ ⋃ i ∈ r, U i

Tactic:
⟨r, ⟨hrcountable, hsub⟩⟩
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊆ ⋃ (i : ι), U i
s_1 t : Set X
hst : s_1 ⊆ t
r : Set ι
hrcountable : r.Countable
hsub : t ⊆ ⋃ i ∈ r, U i
⊢ ∃ (r : Set ι), r.Countable ∧ s_1 ⊆ ⋃ i ∈ r, U i

Tactic:
⟨r, hrcountable, Subset.trans hst hsub⟩

Premises used: Set.Subset.trans, And.intro, Exists.intro
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊆ ⋃ (i : ι), U i
s_1 t : Set X
hst : s_1 ⊆ t
r : Set ι
hrcountable : r.Countable
hsub : t ⊆ ⋃ i ∈ r, U i
⊢ ∃ (r : Set ι), r.Countable ∧ s_1 ⊆ ⋃ i ∈ r, U i

Tactic:
exact ⟨r, hrcountable, Subset.trans hst hsub⟩
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊆ ⋃ (i : ι), U i
⊢ ∀ ⦃s t : Set X⦄,
    s ⊆ t → (∃ (r : Set ι), r.Countable ∧ t ⊆ ⋃ i ∈ r, U i) → ∃ (r : Set ι), r.Countable ∧ s ⊆ ⋃ i ∈ r, U i

Tactic:
have hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → (∃ r : Set ι, r.Countable ∧ t ⊆ ⋃ i ∈ r, U i)
      → (∃ r : Set ι, r.Countable ∧ s ⊆ ⋃ i ∈ r, U i) := by
    intro _ _ hst ⟨r, ⟨hrcountable, hsub⟩⟩
    exact ⟨r, hrcountable, Subset.trans hst hsub⟩
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊆ ⋃ (i : ι), U i
hmono :
  ∀ ⦃s t : Set X⦄,
    s ⊆ t → (∃ (r : Set ι), r.Countable ∧ t ⊆ ⋃ i ∈ r, U i) → ∃ (r : Set ι), r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
S : Set (Set X)
hS : S.Countable
hsr : ∀ s ∈ S, ∃ (r : Set ι), r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
choose! :
  ∀ (r : (s : Set X) → Set ι) (hr : ∀ s ∈ S, (r s).Countable ∧ s ⊆ ⋃ i ∈ r s, U i),
    ∃ (r : Set ι), r.Countable ∧ ⋃₀ S ⊆ ⋃ i ∈ r, U i
⊢ ∃ (r : Set ι), r.Countable ∧ ⋃₀ S ⊆ ⋃ i ∈ r, U i

Tactic:
choose! r hr using hsr
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊆ ⋃ (i : ι), U i
hmono :
  ∀ ⦃s t : Set X⦄,
    s ⊆ t → (∃ (r : Set ι), r.Countable ∧ t ⊆ ⋃ i ∈ r, U i) → ∃ (r : Set ι), r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
S : Set (Set X)
hS : S.Countable
r : (s : Set X) → Set ι
hr : ∀ s ∈ S, (r s).Countable ∧ s ⊆ ⋃ i ∈ r s, U i
⊢ ∃ (r : Set ι), r.Countable ∧ ⋃₀ S ⊆ ⋃ i ∈ r, U i

Tactic:
⟨⋃ s ∈ S, r s, hS.biUnion_iff.mpr (fun s hs ↦ (hr s hs).1), ?_⟩

Premises used: Iff.mpr, And.left, And.intro, Exists.intro, Set.Countable.biUnion_iff, Set.iUnion
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊆ ⋃ (i : ι), U i
hmono :
  ∀ ⦃s t : Set X⦄,
    s ⊆ t → (∃ (r : Set ι), r.Countable ∧ t ⊆ ⋃ i ∈ r, U i) → ∃ (r : Set ι), r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
S : Set (Set X)
hS : S.Countable
r : (s : Set X) → Set ι
hr : ∀ s ∈ S, (r s).Countable ∧ s ⊆ ⋃ i ∈ r s, U i
refine : ⋃₀ S ⊆ ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Set ι) (⋃ s ∈ S, r s) i), U i
⊢ ∃ (r : Set ι), r.Countable ∧ ⋃₀ S ⊆ ⋃ i ∈ r, U i

Tactic:
refine ⟨⋃ s ∈ S, r s, hS.biUnion_iff.mpr (fun s hs ↦ (hr s hs).1), ?_⟩
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊆ ⋃ (i : ι), U i
hmono :
  ∀ ⦃s t : Set X⦄,
    s ⊆ t → (∃ (r : Set ι), r.Countable ∧ t ⊆ ⋃ i ∈ r, U i) → ∃ (r : Set ι), r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
S : Set (Set X)
hS : S.Countable
r : (s : Set X) → Set ι
hr : ∀ s ∈ S, (r s).Countable ∧ s ⊆ ⋃ i ∈ r s, U i
⊢ ⋃₀ S ⊆ ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Set ι) (⋃ s ∈ S, r s) i), U i

Tactic:
sUnion_subset ?h.right.h

Premises used: Set.sUnion_subset
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊆ ⋃ (i : ι), U i
hmono :
  ∀ ⦃s t : Set X⦄,
    s ⊆ t → (∃ (r : Set ι), r.Countable ∧ t ⊆ ⋃ i ∈ r, U i) → ∃ (r : Set ι), r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
S : Set (Set X)
hS : S.Countable
r : (s : Set X) → Set ι
hr : ∀ s ∈ S, (r s).Countable ∧ s ⊆ ⋃ i ∈ r s, U i
h : ∀ t' ∈ S, t' ⊆ ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Set ι) (⋃ s ∈ S, r s) i), U i
⊢ ⋃₀ S ⊆ ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Set ι) (⋃ s ∈ S, r s) i), U i

Tactic:
refine sUnion_subset ?h.right.h

Premises used: Set.sUnion_subset
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊆ ⋃ (i : ι), U i
hmono :
  ∀ ⦃s t : Set X⦄,
    s ⊆ t → (∃ (r : Set ι), r.Countable ∧ t ⊆ ⋃ i ∈ r, U i) → ∃ (r : Set ι), r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
S : Set (Set X)
hS : S.Countable
r : (s : Set X) → Set ι
hr : ∀ s ∈ S, (r s).Countable ∧ s ⊆ ⋃ i ∈ r s, U i
h : ∀ t' ∈ S, t' ⊆ ⋃ y ∈ S, ⋃ x ∈ r y, U x
⊢ ∀ t' ∈ S, t' ⊆ ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Set ι) (⋃ s ∈ S, r s) i), U i

Tactic:
simp only [mem_iUnion, exists_prop, iUnion_exists, biUnion_and']

Premises used: Set.mem_iUnion, exists_prop, Set.iUnion_exists, Set.biUnion_and'
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊆ ⋃ (i : ι), U i
hmono :
  ∀ ⦃s t : Set X⦄,
    s ⊆ t → (∃ (r : Set ι), r.Countable ∧ t ⊆ ⋃ i ∈ r, U i) → ∃ (r : Set ι), r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
S : Set (Set X)
hS : S.Countable
r : (s : Set X) → Set ι
hr : ∀ s ∈ S, (r s).Countable ∧ s ⊆ ⋃ i ∈ r s, U i
⊢ ∀ t' ∈ S, t' ⊆ ⋃ y ∈ S, ⋃ x ∈ r y, U x

Tactic:
fun i is x hx ↦ mem_biUnion is ((hr i is).2 hx)

Premises used: Set.mem_biUnion, Set.Subset, And.right
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊆ ⋃ (i : ι), U i
hmono :
  ∀ ⦃s t : Set X⦄,
    s ⊆ t → (∃ (r : Set ι), r.Countable ∧ t ⊆ ⋃ i ∈ r, U i) → ∃ (r : Set ι), r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
S : Set (Set X)
hS : S.Countable
r : (s : Set X) → Set ι
hr : ∀ s ∈ S, (r s).Countable ∧ s ⊆ ⋃ i ∈ r s, U i
⊢ ∀ t' ∈ S, t' ⊆ ⋃ y ∈ S, ⋃ x ∈ r y, U x

Tactic:
exact fun i is x hx ↦ mem_biUnion is ((hr i is).2 hx)

Premises used: Set.mem_biUnion
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊆ ⋃ (i : ι), U i
hmono :
  ∀ ⦃s t : Set X⦄,
    s ⊆ t → (∃ (r : Set ι), r.Countable ∧ t ⊆ ⋃ i ∈ r, U i) → ∃ (r : Set ι), r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
⊢ ∀ (S : Set (Set X)),
    S.Countable →
      (∀ s ∈ S, ∃ (r : Set ι), r.Countable ∧ s ⊆ ⋃ i ∈ r, U i) → ∃ (r : Set ι), r.Countable ∧ ⋃₀ S ⊆ ⋃ i ∈ r, U i

Tactic:
have hcountable_union : ∀ (S : Set (Set X)), S.Countable
      → (∀ s ∈ S, ∃ r : Set ι, r.Countable ∧ (s ⊆ ⋃ i ∈ r, U i))
      → ∃ r : Set ι, r.Countable ∧ (⋃₀ S ⊆ ⋃ i ∈ r, U i) := by
    intro S hS hsr
    choose! r hr using hsr
    refine ⟨⋃ s ∈ S, r s, hS.biUnion_iff.mpr (fun s hs ↦ (hr s hs).1), ?_⟩
    refine sUnion_subset ?h.right.h
    simp only [mem_iUnion, exists_prop, iUnion_exists, biUnion_and']
    exact fun i is x hx ↦ mem_biUnion is ((hr i is).2 hx)
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊆ ⋃ (i : ι), U i
hmono :
  ∀ ⦃s t : Set X⦄,
    s ⊆ t → (∃ (r : Set ι), r.Countable ∧ t ⊆ ⋃ i ∈ r, U i) → ∃ (r : Set ι), r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
hcountable_union :
  ∀ (S : Set (Set X)),
    S.Countable →
      (∀ s ∈ S, ∃ (r : Set ι), r.Countable ∧ s ⊆ ⋃ i ∈ r, U i) → ∃ (r : Set ι), r.Countable ∧ ⋃₀ S ⊆ ⋃ i ∈ r, U i
x : X
hx : x ∈ s
let : ∀ (i : ι) (hi : x ∈ U i), ∃ t ∈ 𝓝[s] x, ∃ (r : Set ι), r.Countable ∧ t ⊆ ⋃ i ∈ r, U i
⊢ ∃ t ∈ 𝓝[s] x, ∃ (r : Set ι), r.Countable ∧ t ⊆ ⋃ i ∈ r, U i

Tactic:
let ⟨i, hi⟩ := mem_iUnion.1 (hsU hx)
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊆ ⋃ (i : ι), U i
hmono :
  ∀ ⦃s t : Set X⦄,
    s ⊆ t → (∃ (r : Set ι), r.Countable ∧ t ⊆ ⋃ i ∈ r, U i) → ∃ (r : Set ι), r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
hcountable_union :
  ∀ (S : Set (Set X)),
    S.Countable →
      (∀ s ∈ S, ∃ (r : Set ι), r.Countable ∧ s ⊆ ⋃ i ∈ r, U i) → ∃ (r : Set ι), r.Countable ∧ ⋃₀ S ⊆ ⋃ i ∈ r, U i
x : X
hx : x ∈ s
i : ι
hi : x ∈ U i
⊢ Set.Countable (α := ι) {i}

Tactic:
simp
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊆ ⋃ (i : ι), U i
hmono :
  ∀ ⦃s t : Set X⦄,
    s ⊆ t → (∃ (r : Set ι), r.Countable ∧ t ⊆ ⋃ i ∈ r, U i) → ∃ (r : Set ι), r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
hcountable_union :
  ∀ (S : Set (Set X)),
    S.Countable →
      (∀ s ∈ S, ∃ (r : Set ι), r.Countable ∧ s ⊆ ⋃ i ∈ r, U i) → ∃ (r : Set ι), r.Countable ∧ ⋃₀ S ⊆ ⋃ i ∈ r, U i
x : X
hx : x ∈ s
i : ι
hi : x ∈ U i
refine : U i ⊆ ⋃ (i_1 : ι), ⋃ (_ : Membership.mem (γ := Set ι) {i} i_1), U i_1
⊢ ∃ t ∈ 𝓝[s] x, ∃ (r : Set ι), r.Countable ∧ t ⊆ ⋃ i ∈ r, U i

Tactic:
refine ⟨U i, mem_nhdsWithin_of_mem_nhds ((hUo i).mem_nhds hi), {i}, by simp, ?_⟩
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊆ ⋃ (i : ι), U i
hmono :
  ∀ ⦃s t : Set X⦄,
    s ⊆ t → (∃ (r : Set ι), r.Countable ∧ t ⊆ ⋃ i ∈ r, U i) → ∃ (r : Set ι), r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
hcountable_union :
  ∀ (S : Set (Set X)),
    S.Countable →
      (∀ s ∈ S, ∃ (r : Set ι), r.Countable ∧ s ⊆ ⋃ i ∈ r, U i) → ∃ (r : Set ι), r.Countable ∧ ⋃₀ S ⊆ ⋃ i ∈ r, U i
x : X
hx : x ∈ s
i : ι
hi : x ∈ U i
simp : U i ⊆ U i
⊢ U i ⊆ ⋃ (i_1 : ι), ⋃ (_ : Membership.mem (γ := Set ι) {i} i_1), U i_1

Tactic:
simp only [mem_singleton_iff, iUnion_iUnion_eq_left]

Premises used: Set.iUnion_iUnion_eq_left, Set.mem_singleton_iff
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊆ ⋃ (i : ι), U i
hmono :
  ∀ ⦃s t : Set X⦄,
    s ⊆ t → (∃ (r : Set ι), r.Countable ∧ t ⊆ ⋃ i ∈ r, U i) → ∃ (r : Set ι), r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
hcountable_union :
  ∀ (S : Set (Set X)),
    S.Countable →
      (∀ s ∈ S, ∃ (r : Set ι), r.Countable ∧ s ⊆ ⋃ i ∈ r, U i) → ∃ (r : Set ι), r.Countable ∧ ⋃₀ S ⊆ ⋃ i ∈ r, U i
x : X
hx : x ∈ s
i : ι
hi : x ∈ U i
⊢ U i ⊆ U i

Tactic:
Subset.refl _

Premises used: Set.Subset.refl
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊆ ⋃ (i : ι), U i
hmono :
  ∀ ⦃s t : Set X⦄,
    s ⊆ t → (∃ (r : Set ι), r.Countable ∧ t ⊆ ⋃ i ∈ r, U i) → ∃ (r : Set ι), r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
hcountable_union :
  ∀ (S : Set (Set X)),
    S.Countable →
      (∀ s ∈ S, ∃ (r : Set ι), r.Countable ∧ s ⊆ ⋃ i ∈ r, U i) → ∃ (r : Set ι), r.Countable ∧ ⋃₀ S ⊆ ⋃ i ∈ r, U i
x : X
hx : x ∈ s
i : ι
hi : x ∈ U i
⊢ U i ⊆ U i

Tactic:
exact Subset.refl _

Premises used: Set.Subset.refl
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊆ ⋃ (i : ι), U i
hmono :
  ∀ ⦃s t : Set X⦄,
    s ⊆ t → (∃ (r : Set ι), r.Countable ∧ t ⊆ ⋃ i ∈ r, U i) → ∃ (r : Set ι), r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
hcountable_union :
  ∀ (S : Set (Set X)),
    S.Countable →
      (∀ s ∈ S, ∃ (r : Set ι), r.Countable ∧ s ⊆ ⋃ i ∈ r, U i) → ∃ (r : Set ι), r.Countable ∧ ⋃₀ S ⊆ ⋃ i ∈ r, U i
⊢ ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∃ (r : Set ι), r.Countable ∧ t ⊆ ⋃ i ∈ r, U i

Tactic:
have h_nhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∃ r : Set ι, r.Countable ∧ (t ⊆ ⋃ i ∈ r, U i) := by
    intro x hx
    let ⟨i, hi⟩ := mem_iUnion.1 (hsU hx)
    refine ⟨U i, mem_nhdsWithin_of_mem_nhds ((hUo i).mem_nhds hi), {i}, by simp, ?_⟩
    simp only [mem_singleton_iff, iUnion_iUnion_eq_left]
    exact Subset.refl _
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊆ ⋃ (i : ι), U i
hmono :
  ∀ ⦃s t : Set X⦄,
    s ⊆ t → (∃ (r : Set ι), r.Countable ∧ t ⊆ ⋃ i ∈ r, U i) → ∃ (r : Set ι), r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
hcountable_union :
  ∀ (S : Set (Set X)),
    S.Countable →
      (∀ s ∈ S, ∃ (r : Set ι), r.Countable ∧ s ⊆ ⋃ i ∈ r, U i) → ∃ (r : Set ι), r.Countable ∧ ⋃₀ S ⊆ ⋃ i ∈ r, U i
h_nhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∃ (r : Set ι), r.Countable ∧ t ⊆ ⋃ i ∈ r, U i
⊢ ∃ (r : Set ι), r.Countable ∧ s ⊆ ⋃ i ∈ r, U i

Tactic:
hs.induction_on hmono hcountable_union h_nhds

Premises used: IsLindelof.induction_on
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊆ ⋃ (i : ι), U i
hmono :
  ∀ ⦃s t : Set X⦄,
    s ⊆ t → (∃ (r : Set ι), r.Countable ∧ t ⊆ ⋃ i ∈ r, U i) → ∃ (r : Set ι), r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
hcountable_union :
  ∀ (S : Set (Set X)),
    S.Countable →
      (∀ s ∈ S, ∃ (r : Set ι), r.Countable ∧ s ⊆ ⋃ i ∈ r, U i) → ∃ (r : Set ι), r.Countable ∧ ⋃₀ S ⊆ ⋃ i ∈ r, U i
h_nhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∃ (r : Set ι), r.Countable ∧ t ⊆ ⋃ i ∈ r, U i
⊢ ∃ (r : Set ι), r.Countable ∧ s ⊆ ⋃ i ∈ r, U i

Tactic:
exact hs.induction_on hmono hcountable_union h_nhds
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsLindelof s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
⊢ ∃ (r : Set (↑s : Type u)), r.Countable ∧ s ⊆ ⋃ i ∈ r, (fun (x : (↑s : Type u)) ↦ interior (U (↑x : X) ⋯)) i

Tactic:
have := hs.elim_countable_subcover (fun x : s ↦ interior (U x x.2)) (fun _ ↦ isOpen_interior)
    fun x hx ↦
      mem_iUnion.2 ⟨⟨x, hx⟩, mem_interior_iff_mem_nhds.2 <| hU _ _⟩
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsLindelof s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
this : ∃ (r : Set (↑s : Type u)), r.Countable ∧ s ⊆ ⋃ i ∈ r, (fun (x : (↑s : Type u)) ↦ interior (U (↑x : X) ⋯)) i
rcases :
  ∀ (r : Set (↑s : Type u)) (hr : r.Countable)
    (hs : s ⊆ ⋃ i ∈ r, (fun (x : (↑s : Type u)) ↦ interior (U (↑x : X) ⋯)) i),
    ∃ (t : Set (↑s : Type u)), t.Countable ∧ s ⊆ ⋃ x ∈ t, U (↑x : X) ⋯
⊢ ∃ (t : Set (↑s : Type u)), t.Countable ∧ s ⊆ ⋃ x ∈ t, U (↑x : X) ⋯

Tactic:
rcases this with ⟨r, ⟨hr, hs⟩⟩
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs_1 : IsLindelof s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
r : Set (↑s : Type u)
hr : r.Countable
hs : s ⊆ ⋃ i ∈ r, (fun (x : (↑s : Type u)) ↦ interior (U (↑x : X) ⋯)) i
right : s ⊆ ⋃ x ∈ r, U (↑x : X) ⋯
⊢ ∃ (t : Set (↑s : Type u)), t.Countable ∧ s ⊆ ⋃ x ∈ t, U (↑x : X) ⋯

Tactic:
use r, hr
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs_1 : IsLindelof s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
r : Set (↑s : Type u)
hr : r.Countable
hs : s ⊆ ⋃ i ∈ r, (fun (x : (↑s : Type u)) ↦ interior (U (↑x : X) ⋯)) i
right : Subset.{u} (α := Set X) (⋃ i ∈ r, (fun (x : (↑s : Type u)) ↦ interior (U (↑x : X) ⋯)) i) (⋃ x ∈ r, U (↑x : X) ⋯)
⊢ s ⊆ ⋃ x ∈ r, U (↑x : X) ⋯

Tactic:
apply Subset.trans hs

Premises used: Set.Subset.trans