awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : LindelofSpace X
⊢ coLindelof X = ⊥

Tactic:
hasBasis_coLindelof.eq_bot_iff.mpr ⟨Set.univ, isLindelof_univ, Set.compl_univ⟩

Premises used: Iff.mpr, Filter.HasBasis.eq_bot_iff, Set.univ, hasBasis_coLindelof, Set.compl_univ, And.intro, Exists.intro, isLindelof_univ
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
inst_2 : NonLindelofSpace X
⊢ (coclosedLindelof X).NeBot

Tactic:
neBot_of_le coLindelof_le_coclosedLindelof

Premises used: coLindelof_le_coclosedLindelof, Filter.neBot_of_le
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
h : (coLindelof X).NeBot
⊢ NonLindelofSpace X

Tactic:
⟨fun h' => (Filter.nonempty_of_mem h'.compl_mem_coLindelof).ne_empty compl_univ⟩

Premises used: IsLindelof.compl_mem_coLindelof, Set.Nonempty.ne_empty, Filter.nonempty_of_mem, NonLindelofSpace.mk, Set.compl_univ
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
⊢ (coLindelof X).NeBot ↔ NonLindelofSpace X

Tactic:
⟨nonLindelofSpace_of_neBot, fun _ => inferInstance⟩

Premises used: nonLindelofSpace_of_neBot, inferInstance, Iff.intro
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
⊢ ¬LindelofSpace X ↔ NonLindelofSpace X

Tactic:
⟨fun h₁ => ⟨fun h₂ => h₁ ⟨h₂⟩⟩, fun ⟨h₁⟩ ⟨h₂⟩ => h₁ h₂⟩

Premises used: False, _private.0.not_LindelofSpace_iff.match_2, NonLindelofSpace.mk, LindelofSpace.mk, Iff.intro, _private.0.not_LindelofSpace_iff.match_1
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : LindelofSpace X
inst_2 : DiscreteTopology X
⊢ Countable X

Tactic:
countable_univ_iff.mp isLindelof_univ.countable_of_discrete

Premises used: Set.countable_univ_iff, Iff.mp, IsLindelof.countable_of_discrete, isLindelof_univ
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : LindelofSpace X
U : X → Set X
hU : ∀ (x : X), U x ∈ 𝓝 x
⊢ ∃ (t : Set X), t.Countable ∧ Eq.{u + 1} (α := Set X) (⋃ x ∈ t, interior (U x)) univ

Tactic:
let ⟨t, ht⟩ := isLindelof_univ.elim_countable_subcover (fun x => interior (U x))
    (fun _ => isOpen_interior) fun x _ => mem_iUnion.2 ⟨x, mem_interior_iff_mem_nhds.2 (hU x)⟩
  ⟨t, ⟨ht.1, univ_subset_iff.1 ht.2⟩⟩

Premises used: Iff.mpr, Set.univ_subset_iff, mem_interior_iff_mem_nhds, isOpen_interior, Set.univ, Set.mem_iUnion, Exists, And, And.right, And.left, And.intro, interior, Exists.intro, Iff.mp, IsLindelof.elim_countable_subcover, isLindelof_univ, _private.0.countable_cover_nhds_interior.match_1, Set.Countable, Eq, Set.iUnion
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : LindelofSpace X
U : X → Set X
hU : ∀ (x : X), U x ∈ 𝓝 x
⊢ ∃ (t : Set X), t.Countable ∧ Eq.{u + 1} (α := Set X) (⋃ x ∈ t, U x) univ

Tactic:
let ⟨t, ht⟩ := countable_cover_nhds_interior hU
  ⟨t, ⟨ht.1, univ_subset_iff.1 <| ht.2.symm.subset.trans <|
    iUnion₂_mono fun _ _ => interior_subset⟩⟩

Premises used: Set.univ_subset_iff, interior_subset, Set.univ, _private.0.countable_cover_nhds.match_1, countable_cover_nhds_interior, Exists, HasSubset.Subset.trans, Eq.subset, Set.iUnion₂_mono, And, And.right, And.left, And.intro, Exists.intro, Iff.mp, Set.Countable, Eq.symm, Eq, Set.iUnion
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : Continuous[inst, inst_1] f
rw : ∀ (i' : Set X), IsLindelof i' → ∃ (i : Set Y), IsLindelof i ∧ f ⁻¹' iᶜ ⊆ i'ᶜ
⊢ comap f (coLindelof Y) ≤ coLindelof X

Tactic:
rw [(hasBasis_coLindelof.comap f).le_basis_iff hasBasis_coLindelof]

Premises used: hasBasis_coLindelof, Filter.HasBasis.le_basis_iff, Filter.HasBasis.comap
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : Continuous[inst, inst_1] f
t : Set X
ht : IsLindelof t
⊢ ∃ (i : Set Y), IsLindelof i ∧ f ⁻¹' iᶜ ⊆ tᶜ

Tactic:
⟨f '' t, ht.image hf, ?_⟩

Premises used: IsLindelof.image, And.intro, Exists.intro, Set.image
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : Continuous[inst, inst_1] f
t : Set X
ht : IsLindelof t
refine : f ⁻¹' (f '' t)ᶜ ⊆ tᶜ
⊢ ∃ (i : Set Y), IsLindelof i ∧ f ⁻¹' iᶜ ⊆ tᶜ

Tactic:
refine ⟨f '' t, ht.image hf, ?_⟩
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : Continuous[inst, inst_1] f
t : Set X
ht : IsLindelof t
⊢ f ⁻¹' (f '' t)ᶜ ⊆ tᶜ

Tactic:
simpa using t.subset_preimage_image f

Premises used: Set.subset_preimage_image
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : LindelofSpace X
f : X → Y
hf : Continuous[inst, inst_1] f
rw : IsLindelof (f '' univ)
⊢ IsLindelof (range f)

Tactic:
rw [← image_univ]

Premises used: Set.image_univ
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : LindelofSpace X
f : X → Y
hf : Continuous[inst, inst_1] f
⊢ IsLindelof (f '' univ)

Tactic:
isLindelof_univ.image hf

Premises used: IsLindelof.image, isLindelof_univ
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : LindelofSpace X
f : X → Y
hf : Continuous[inst, inst_1] f
⊢ IsLindelof (f '' univ)

Tactic:
exact isLindelof_univ.image hf

Premises used: IsLindelof.image, isLindelof_univ
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : LindelofSpace X
⊢ IsLindelof (diagonal X)

Tactic:
@range_diag X ▸ isLindelof_range (continuous_id.prodMk continuous_id)

Premises used: Eq.rec, continuous_id, Set.range_diag, isLindelof_range, Continuous.prodMk
-- 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
hf : IsInducing f
⊢ IsLindelof s ↔ IsLindelof (f '' s)

Tactic:
⟨fun hs => hs.image hf.continuous, fun hs F F_ne_bot _ F_le => ?_⟩

Premises used: IsLindelof.image, Iff.intro, Topology.IsInducing.continuous
-- 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
hf : IsInducing f
refine :
  ∀ (hs : IsLindelof (f '' s)) (F : Filter X) (F_ne_bot : F.NeBot),
    CountableInterFilter F → ∀ (F_le : F ≤ 𝓟 s), ∃ x ∈ s, ClusterPt x F
⊢ IsLindelof s ↔ IsLindelof (f '' s)

Tactic:
refine ⟨fun hs => hs.image hf.continuous, fun hs F F_ne_bot _ F_le => ?_⟩
-- 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
hf : IsInducing f
hs : IsLindelof (f '' s)
F : Filter X
F_ne_bot : F.NeBot
h : CountableInterFilter F
F_le : F ≤ 𝓟 s
obtain : ∀ (x : X) (x_in : x ∈ s) (hx : ClusterPt (f x) (map f F)), ∃ x ∈ s, ClusterPt x F
⊢ ∃ x ∈ s, ClusterPt x F

Tactic:
obtain ⟨_, ⟨x, x_in : x ∈ s, rfl⟩, hx : ClusterPt (f x) (map f F)⟩ :=
    hs ((map_mono F_le).trans_eq map_principal)

Premises used: Filter.map_mono, LE.le.trans_eq, Filter.map_principal, 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
hf : IsInducing f
hs : IsLindelof (f '' s)
F : Filter X
F_ne_bot : F.NeBot
h : CountableInterFilter F
F_le : F ≤ 𝓟 s
x : X
x_in : x ∈ s
hx : ClusterPt (f x) (map f F)
⊢ ∃ x ∈ s, ClusterPt x F

Tactic:
⟨x, x_in, hf.mapClusterPt_iff.1 hx⟩

Premises used: And.intro, Exists.intro, Iff.mp, Topology.IsInducing.mapClusterPt_iff
-- 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
hf : IsInducing f
hs : IsLindelof (f '' s)
F : Filter X
F_ne_bot : F.NeBot
h : CountableInterFilter F
F_le : F ≤ 𝓟 s
x : X
x_in : x ∈ s
hx : ClusterPt (f x) (map f F)
⊢ ∃ x ∈ s, ClusterPt x F

Tactic:
exact ⟨x, x_in, hf.mapClusterPt_iff.1 hx⟩
-- 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
hf : IsEmbedding f
⊢ IsLindelof s ↔ IsLindelof (f '' s)

Tactic:
hf.isInducing.isLindelof_iff

Premises used: Topology.IsEmbedding.isInducing, Topology.IsInducing.isLindelof_iff
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsInducing f
hf' : IsClosed[inst_1] (range f)
K : Set Y
hK : IsLindelof K
⊢ IsLindelof (K ∩ range f)

Tactic:
replace hK := hK.inter_right hf'
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsInducing f
hf' : IsClosed[inst_1] (range f)
K : Set Y
hK : IsLindelof (K ∩ range f)
rwa : IsLindelof (f '' f ⁻¹' K)
rwa₁ rwa₂ rwa₃ rwa₄ : IsLindelof (K ∩ range f)
⊢ IsLindelof (f ⁻¹' K)

Tactic:
rwa [hf.isLindelof_iff, image_preimage_eq_inter_range]

Premises used: Set.image_preimage_eq_inter_range, Topology.IsInducing.isLindelof_iff
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsClosedEmbedding f
K : Set Y
hK : IsLindelof K
⊢ IsLindelof (f ⁻¹' K)

Tactic:
hf.isInducing.isLindelof_preimage (hf.isClosed_range) hK

Premises used: Topology.IsClosedEmbedding.isInducing, Topology.IsInducing.isLindelof_preimage, Topology.IsClosedEmbedding.isClosed_range
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsClosedEmbedding f
⊢ Tendsto f (coLindelof X) (coLindelof Y)

Tactic:
hasBasis_coLindelof.tendsto_right_iff.mpr fun _K hK =>
    (hf.isLindelof_preimage hK).compl_mem_coLindelof

Premises used: Iff.mpr, IsLindelof.compl_mem_coLindelof, hasBasis_coLindelof, Filter.HasBasis.tendsto_right_iff, Topology.IsClosedEmbedding.isLindelof_preimage
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
p : X → Prop
s : Set { x : X // p x }
⊢ IsLindelof s ↔ IsLindelof (val (p := fun (x : X) ↦ p x) '' s)

Tactic:
IsEmbedding.subtypeVal.isLindelof_iff

Premises used: Topology.IsEmbedding.isLindelof_iff, Topology.IsEmbedding.subtypeVal
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
rw :
  IsLindelof s ↔ IsLindelof.{u} (X := X) (image (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) univ)
rw₁ : IsLindelof s ↔ IsLindelof.{u} (X := X) (range (ι := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)))
rw₂ rw₃ : IsLindelof s ↔ IsLindelof s
⊢ IsLindelof s ↔ IsLindelof.{u} (X := (↑s : Type u)) univ

Tactic:
rw [Subtype.isLindelof_iff, image_univ, Subtype.range_coe]

Premises used: Set.image_univ, Subtype.range_coe, Subtype.isLindelof_iff
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ IsLindelof s ↔ LindelofSpace.{u} (↑s : Type u)

Tactic:
isLindelof_iff_isLindelof_univ.trans isLindelof_univ_iff

Premises used: isLindelof_iff_isLindelof_univ, Iff.trans, isLindelof_univ_iff
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
inst_1 : LindelofSpace.{u} (↑s : Type u)
⊢ IsLindelof s

Tactic:
isLindelof_iff_lindelofSpace.mpr ‹_›

Premises used: Iff.mpr, isLindelof_iff_lindelofSpace
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsLindelof s
hs' : DiscreteTopology.{u} (↑s : Type u)
⊢ s.Countable

Tactic:
countable_coe_iff.mp
  (@countable_of_Lindelof_of_discrete _ _ (isLindelof_iff_lindelofSpace.mp hs) hs')

Premises used: Set.countable_coe_iff, countable_of_Lindelof_of_discrete, Iff.mp
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsLindelof s
hs' : IsDiscrete s
⊢ s.Countable

Tactic:
hs.countable hs'.to_subtype

Premises used: IsDiscrete.to_subtype, IsLindelof.countable
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NonLindelofSpace X
f : X → Y
hf : IsClosedEmbedding f
⊢ NonLindelofSpace Y

Tactic:
nonLindelofSpace_of_neBot hf.tendsto_coLindelof.neBot

Premises used: nonLindelofSpace_of_neBot, Topology.IsClosedEmbedding.tendsto_coLindelof, Filter.Tendsto.neBot
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : LindelofSpace Y
f : X → Y
hf : IsClosedEmbedding f
rw : IsLindelof (range f)
⊢ IsLindelof.{u} (X := X) univ

Tactic:
rw [hf.isInducing.isLindelof_iff, image_univ]

Premises used: Topology.IsClosedEmbedding.isInducing, Set.image_univ, Topology.IsInducing.isLindelof_iff
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : LindelofSpace Y
f : X → Y
hf : IsClosedEmbedding f
⊢ IsLindelof (range f)

Tactic:
hf.isClosed_range.isLindelof

Premises used: IsClosed.isLindelof, Topology.IsClosedEmbedding.isClosed_range
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : LindelofSpace Y
f : X → Y
hf : IsClosedEmbedding f
⊢ IsLindelof (range f)

Tactic:
exact hf.isClosed_range.isLindelof

Premises used: IsClosed.isLindelof, Topology.IsClosedEmbedding.isClosed_range
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
inst_2 : LindelofSpace X
inst_3 : LindelofSpace Y
rw : IsLindelof (X := X ⊕ Y) (range Sum.inl ∪ range Sum.inr)
⊢ IsLindelof (X := X ⊕ Y) univ

Tactic:
rw [← range_inl_union_range_inr]

Premises used: Set.range_inl_union_range_inr
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
inst_2 : LindelofSpace X
inst_3 : LindelofSpace Y
⊢ IsLindelof (X := X ⊕ Y) (range Sum.inl ∪ range Sum.inr)

Tactic:
(isLindelof_range continuous_inl).union (isLindelof_range continuous_inr)

Premises used: continuous_inl, continuous_inr, IsLindelof.union, isLindelof_range
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
inst_2 : LindelofSpace X
inst_3 : LindelofSpace Y
⊢ IsLindelof (X := X ⊕ Y) (range Sum.inl ∪ range Sum.inr)

Tactic:
exact (isLindelof_range continuous_inl).union (isLindelof_range continuous_inr)

Premises used: continuous_inl, continuous_inr, IsLindelof.union, isLindelof_range
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X_1 : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s t : Set X_1
X : ι → Type u_2
inst_2 : Countable ι
inst_3 : (i : ι) → TopologicalSpace (X i)
inst_4 : ∀ (i : ι), LindelofSpace.{u_2} (X i)
rw : IsLindelof (X := (i : ι) × X i) (⋃ (a : ι), range (Sigma.mk (β := fun (a : ι) ↦ X a) a))
⊢ IsLindelof (X := (i : ι) × X i) univ

Tactic:
rw [Sigma.univ]

Premises used: Set.Sigma.univ
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X_1 : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s t : Set X_1
X : ι → Type u_2
inst_2 : Countable ι
inst_3 : (i : ι) → TopologicalSpace (X i)
inst_4 : ∀ (i : ι), LindelofSpace.{u_2} (X i)
⊢ IsLindelof (X := (i : ι) × X i) (⋃ (a : ι), range (Sigma.mk (β := fun (a : ι) ↦ X a) a))

Tactic:
isLindelof_iUnion fun i => isLindelof_range continuous_sigmaMk

Premises used: continuous_sigmaMk, isLindelof_range, isLindelof_iUnion
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X_1 : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s t : Set X_1
X : ι → Type u_2
inst_2 : Countable ι
inst_3 : (i : ι) → TopologicalSpace (X i)
inst_4 : ∀ (i : ι), LindelofSpace.{u_2} (X i)
⊢ IsLindelof (X := (i : ι) × X i) (⋃ (a : ι), range (Sigma.mk (β := fun (a : ι) ↦ X a) a))

Tactic:
exact isLindelof_iUnion fun i => isLindelof_range continuous_sigmaMk

Premises used: continuous_sigmaMk, isLindelof_range, isLindelof_iUnion
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
r : X → X → Prop
inst_2 : LindelofSpace X
rw : IsLindelof (range (mk r))
⊢ IsLindelof.{u} (X := Quot r) univ

Tactic:
rw [← range_quot_mk]

Premises used: Set.range_quot_mk
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
r : X → X → Prop
inst_2 : LindelofSpace X
⊢ IsLindelof (range (mk r))

Tactic:
isLindelof_range continuous_quot_mk

Premises used: continuous_quot_mk, isLindelof_range
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
r : X → X → Prop
inst_2 : LindelofSpace X
⊢ IsLindelof (range (mk r))

Tactic:
exact isLindelof_range continuous_quot_mk

Premises used: continuous_quot_mk, isLindelof_range
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s_1 t : Set X
s : Setoid X
inst_2 : LindelofSpace X
⊢ LindelofSpace.{u} (Quotient s)

Tactic:
Quot.lindelofSpace

Premises used: Quotient, Quotient.mk', Quot.lindelofSpace
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : LindelofSpace X
hf : Continuous[inst, inst_1] f
hsur : Function.Surjective f
rw : IsLindelof (f '' univ)
⊢ IsLindelof.{v} (X := Y) univ

Tactic:
rw [← Set.image_univ_of_surjective hsur]

Premises used: Set.image_univ_of_surjective
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : LindelofSpace X
hf : Continuous[inst, inst_1] f
hsur : Function.Surjective f
⊢ IsLindelof (f '' univ)

Tactic:
IsLindelof.image (isLindelof_univ_iff.mpr ‹_›) hf

Premises used: Iff.mpr, IsLindelof.image, isLindelof_univ_iff
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : LindelofSpace X
hf : Continuous[inst, inst_1] f
hsur : Function.Surjective f
⊢ IsLindelof (f '' univ)

Tactic:
exact IsLindelof.image (isLindelof_univ_iff.mpr ‹_›) hf

Premises used: Iff.mpr, IsLindelof.image, isLindelof_univ_iff
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hs : IsHereditarilyLindelof s
ht : t ⊆ s
⊢ IsLindelof t

Tactic:
hs t ht
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsHereditarilyLindelof s
⊢ IsLindelof s

Tactic:
hs.isLindelof_subset Subset.rfl

Premises used: IsHereditarilyLindelof.isLindelof_subset, Set.Subset.rfl
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
s : Set X
a : s ⊆ univ
⊢ IsLindelof s

Tactic:
apply HereditarilyLindelofSpace.isHereditarilyLindelof_univ

Premises used: HereditarilyLindelofSpace.isHereditarilyLindelof_univ
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
s : Set X
⊢ s ⊆ univ

Tactic:
subset_univ s

Premises used: Set.subset_univ
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
s : Set X
⊢ s ⊆ univ

Tactic:
exact subset_univ s

Premises used: Set.subset_univ
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
H : ∀ (s : Set X), IsOpen[inst] s → IsLindelof s
⊢ HereditarilyLindelofSpace X

Tactic:
⟨fun s _ ↦ isLindelof_of_countable_subcover fun U U_open hU ↦ ?_⟩

Premises used: isLindelof_of_countable_subcover, HereditarilyLindelofSpace.mk
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
H : ∀ (s : Set X), IsOpen[inst] s → IsLindelof s
refine :
  ∀ s ⊆ univ,
    ∀ {ι : Type u} (U : ι → Set X) (U_open : ∀ (i : ι), IsOpen[inst] (U i)) (hU : s ⊆ ⋃ (i : ι), U i),
      ∃ (t : Set ι), t.Countable ∧ s ⊆ ⋃ i ∈ t, U i
⊢ HereditarilyLindelofSpace X

Tactic:
refine ⟨fun s _ ↦ isLindelof_of_countable_subcover fun U U_open hU ↦ ?_⟩
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
H : ∀ (s : Set X), IsOpen[inst] s → IsLindelof s
s : Set X
h : s ⊆ univ
ι : Type u
U : ι → Set X
U_open : ∀ (i : ι), IsOpen[inst] (U i)
hU : s ⊆ ⋃ (i : ι), U i
obtain :
  ∀ (t : Set ι) (t_count : t.Countable) (ht : Subset.{u} (α := Set X) (⋃ (i : ι), U i) (⋃ i ∈ t, U i)),
    ∃ (t : Set ι), t.Countable ∧ s ⊆ ⋃ i ∈ t, U i
⊢ ∃ (t : Set ι), t.Countable ∧ s ⊆ ⋃ i ∈ t, U i

Tactic:
obtain ⟨t, t_count, ht⟩ := H (⋃ i, U i) (isOpen_iUnion U_open)
    |>.elim_countable_subcover U U_open subset_rfl

Premises used: isOpen_iUnion, IsLindelof.elim_countable_subcover, Set.iUnion, subset_rfl
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
H : ∀ (s : Set X), IsOpen[inst] s → IsLindelof s
s : Set X
h : s ⊆ univ
ι : Type u
U : ι → Set X
U_open : ∀ (i : ι), IsOpen[inst] (U i)
hU : s ⊆ ⋃ (i : ι), U i
t : Set ι
t_count : t.Countable
ht : Subset.{u} (α := Set X) (⋃ (i : ι), U i) (⋃ i ∈ t, U i)
⊢ ∃ (t : Set ι), t.Countable ∧ s ⊆ ⋃ i ∈ t, U i

Tactic:
⟨t, t_count, hU.trans ht⟩

Premises used: HasSubset.Subset.trans, And.intro, Exists.intro
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
H : ∀ (s : Set X), IsOpen[inst] s → IsLindelof s
s : Set X
h : s ⊆ univ
ι : Type u
U : ι → Set X
U_open : ∀ (i : ι), IsOpen[inst] (U i)
hU : s ⊆ ⋃ (i : ι), U i
t : Set ι
t_count : t.Countable
ht : Subset.{u} (α := Set X) (⋃ (i : ι), U i) (⋃ i ∈ t, U i)
⊢ ∃ (t : Set ι), t.Countable ∧ s ⊆ ⋃ i ∈ t, U i

Tactic:
exact ⟨t, t_count, hU.trans ht⟩
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t_1 : Set X
inst_2 : SecondCountableTopology X
t : Set X
h : t ⊆ univ
x : Filter X
a :
  ∀ {ι : Type u} (U : ι → Set X),
    (∀ (i : ι), IsOpen[inst] (U i)) → t ⊆ ⋃ (i : ι), U i → ∃ (t_2 : Set ι), t_2.Countable ∧ t ⊆ ⋃ i ∈ t_2, U i
⊢ ∀ [x.NeBot] [CountableInterFilter x], x ≤ 𝓟 t → ∃ x_1 ∈ t, ClusterPt x_1 x

Tactic:
apply isLindelof_iff_countable_subcover.mpr

Premises used: Iff.mpr, isLindelof_iff_countable_subcover
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
ι_1 : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t_1 : Set X
inst_2 : SecondCountableTopology X
t : Set X
h : t ⊆ univ
x : Filter X
ι : Type u
U : ι → Set X
hι : ∀ (i : ι), IsOpen[inst] (U i)
hcover : t ⊆ ⋃ (i : ι), U i
⊢ ∃ (T : Set ι), T.Countable ∧ Eq.{u + 1} (α := Set X) (⋃ i ∈ T, U i) (⋃ (i : ι), U i)

Tactic:
have := @isOpen_iUnion_countable X _ _ ι U hι
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
ι_1 : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t_1 : Set X
inst_2 : SecondCountableTopology X
t : Set X
h : t ⊆ univ
x : Filter X
ι : Type u
U : ι → Set X
hι : ∀ (i : ι), IsOpen[inst] (U i)
hcover : t ⊆ ⋃ (i : ι), U i
this : ∃ (T : Set ι), T.Countable ∧ Eq.{u + 1} (α := Set X) (⋃ i ∈ T, U i) (⋃ (i : ι), U i)
a :
  ∀ (t_2 : Set ι) (htc : t_2.Countable) (htu : Eq.{u + 1} (α := Set X) (⋃ i ∈ t_2, U i) (⋃ (i : ι), U i)),
    ∃ (t_3 : Set ι), t_3.Countable ∧ t ⊆ ⋃ i ∈ t_3, U i
⊢ ∃ (t_2 : Set ι), t_2.Countable ∧ t ⊆ ⋃ i ∈ t_2, U i

Tactic:
rcases this with ⟨t, ⟨htc, htu⟩⟩