awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Countable
hf : ∀ i ∈ s, IsLindelof (f i)
i : Type u
U : i → Set X
hU : ∀ (i : i), IsOpen[inst] (U i)
hUcover : Subset.{u} (α := Set X) (⋃ i ∈ s, f i) (⋃ (i : i), U i)
hiU : ∀ i_1 ∈ s, f i_1 ⊆ ⋃ (i : i), U i
r : (i_1 : ι) → Set i
hr : ∀ (i_1 : ι) (is : i_1 ∈ s), (r i_1).Countable ∧ f i_1 ⊆ ⋃ i_2 ∈ r i_1, U i_2
⊢ Subset.{u} (α := Set X) (⋃ i ∈ s, f i)
    (⋃ (i_1 : i), ⋃ (_ : Membership.mem (γ := Set i) (⋃ i_2 ∈ s, r i_2) i_1), U i_1)

Tactic:
iUnion₂_subset ?h.right.h

Premises used: Set.iUnion₂_subset
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Countable
hf : ∀ i ∈ s, IsLindelof (f i)
i : Type u
U : i → Set X
hU : ∀ (i : i), IsOpen[inst] (U i)
hUcover : Subset.{u} (α := Set X) (⋃ i ∈ s, f i) (⋃ (i : i), U i)
hiU : ∀ i_1 ∈ s, f i_1 ⊆ ⋃ (i : i), U i
r : (i_1 : ι) → Set i
hr : ∀ (i_1 : ι) (is : i_1 ∈ s), (r i_1).Countable ∧ f i_1 ⊆ ⋃ i_2 ∈ r i_1, U i_2
h : ∀ (i_1 : ι) (j : i_1 ∈ s), f i_1 ⊆ ⋃ (i_2 : i), ⋃ (_ : Membership.mem (γ := Set i) (⋃ i_3 ∈ s, r i_3) i_2), U i_2
⊢ Subset.{u} (α := Set X) (⋃ i ∈ s, f i)
    (⋃ (i_1 : i), ⋃ (_ : Membership.mem (γ := Set i) (⋃ i_2 ∈ s, r i_2) i_1), U i_1)

Tactic:
refine iUnion₂_subset ?h.right.h
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Countable
hf : ∀ i ∈ s, IsLindelof (f i)
i_1 : Type u
U : i_1 → Set X
hU : ∀ (i : i_1), IsOpen[inst] (U i)
hUcover : Subset.{u} (α := Set X) (⋃ i ∈ s, f i) (⋃ (i : i_1), U i)
hiU : ∀ i ∈ s, f i ⊆ ⋃ (i : i_1), U i
r : (i : ι) → Set i_1
hr : ∀ (i : ι) (is : i ∈ s), (r i).Countable ∧ f i ⊆ ⋃ i_2 ∈ r i, U i_2
i : ι
is : i ∈ s
h : f i ⊆ ⋃ y ∈ s, ⋃ x ∈ r y, U x
⊢ f i ⊆ ⋃ (i : i_1), ⋃ (_ : Membership.mem (γ := Set i_1) (⋃ i ∈ s, r i) 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
ι : Type u_1
inst : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Countable
hf : ∀ i ∈ s, IsLindelof (f i)
i_1 : Type u
U : i_1 → Set X
hU : ∀ (i : i_1), IsOpen[inst] (U i)
hUcover : Subset.{u} (α := Set X) (⋃ i ∈ s, f i) (⋃ (i : i_1), U i)
hiU : ∀ i ∈ s, f i ⊆ ⋃ (i : i_1), U i
r : (i : ι) → Set i_1
hr : ∀ (i : ι) (is : i ∈ s), (r i).Countable ∧ f i ⊆ ⋃ i_2 ∈ r i, U i_2
i : ι
is : i ∈ s
x : X
hx : x ∈ f i
⊢ Membership.mem (γ := Set X) (⋃ y ∈ s, ⋃ x ∈ r y, U x) x

Tactic:
mem_biUnion is ((hr i is).2 hx)

Premises used: Set.mem_biUnion, And.right
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Countable
hf : ∀ i ∈ s, IsLindelof (f i)
i_1 : Type u
U : i_1 → Set X
hU : ∀ (i : i_1), IsOpen[inst] (U i)
hUcover : Subset.{u} (α := Set X) (⋃ i ∈ s, f i) (⋃ (i : i_1), U i)
hiU : ∀ i ∈ s, f i ⊆ ⋃ (i : i_1), U i
r : (i : ι) → Set i_1
hr : ∀ (i : ι) (is : i ∈ s), (r i).Countable ∧ f i ⊆ ⋃ i_2 ∈ r i, U i_2
i : ι
is : i ∈ s
x : X
hx : x ∈ f i
⊢ Membership.mem (γ := Set X) (⋃ y ∈ s, ⋃ x ∈ r y, U x) x

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

Premises used: Set.mem_biUnion
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Finite
hf : ∀ i ∈ s, IsLindelof (f i)
⊢ IsLindelof.{u} (X := X) (⋃ i ∈ s, f i)

Tactic:
Set.Countable.isLindelof_biUnion (countable hs) hf

Premises used: Set.Countable.isLindelof_biUnion, Set.Finite.countable
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
s : Finset ι
f : ι → Set X
hf : ∀ i ∈ s, IsLindelof (f i)
⊢ IsLindelof.{u} (X := X) (⋃ i ∈ s, f i)

Tactic:
s.finite_toSet.isLindelof_biUnion hf

Premises used: Set.Finite.isLindelof_biUnion, Finset.finite_toSet
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
K : ℕ → Set X
hK : ∀ (n : ℕ), IsLindelof (K n)
n : ℕ
⊢ IsLindelof (accumulate K n)

Tactic:
(finite_le_nat n).isLindelof_biUnion fun k _ => hK k

Premises used: Set.Mem, setOf, Set.Finite.isLindelof_biUnion, Set.accumulate, Set.finite_le_nat
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
S : Set (Set X)
hf : S.Countable
hc : ∀ s ∈ S, IsLindelof s
rw : IsLindelof.{u} (X := X) (⋃ i ∈ S, i)
⊢ IsLindelof (⋃₀ S)

Tactic:
rw [sUnion_eq_biUnion]

Premises used: Set.sUnion_eq_biUnion
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
S : Set (Set X)
hf : S.Countable
hc : ∀ s ∈ S, IsLindelof s
⊢ IsLindelof.{u} (X := X) (⋃ i ∈ S, i)

Tactic:
hf.isLindelof_biUnion hc

Premises used: Set.Countable.isLindelof_biUnion
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
S : Set (Set X)
hf : S.Countable
hc : ∀ s ∈ S, IsLindelof s
⊢ IsLindelof.{u} (X := X) (⋃ i ∈ S, i)

Tactic:
exact hf.isLindelof_biUnion hc

Premises used: Set.Countable.isLindelof_biUnion
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
S : Set (Set X)
hf : S.Finite
hc : ∀ s ∈ S, IsLindelof s
rw : IsLindelof.{u} (X := X) (⋃ i ∈ S, i)
⊢ IsLindelof (⋃₀ S)

Tactic:
rw [sUnion_eq_biUnion]

Premises used: Set.sUnion_eq_biUnion
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
S : Set (Set X)
hf : S.Finite
hc : ∀ s ∈ S, IsLindelof s
⊢ IsLindelof.{u} (X := X) (⋃ i ∈ S, i)

Tactic:
hf.isLindelof_biUnion hc

Premises used: Set.Finite.isLindelof_biUnion
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
S : Set (Set X)
hf : S.Finite
hc : ∀ s ∈ S, IsLindelof s
⊢ IsLindelof.{u} (X := X) (⋃ i ∈ S, i)

Tactic:
exact hf.isLindelof_biUnion hc

Premises used: Set.Finite.isLindelof_biUnion
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
ι : Sort u_2
f : ι → Set X
inst_1 : Countable ι
h : ∀ (i : ι), IsLindelof (f i)
⊢ IsLindelof.{u} (X := X) (⋃ (i : ι), f i)

Tactic:
(countable_range f).isLindelof_sUnion <| forall_mem_range.2 h

Premises used: Iff.mpr, Set.Countable.isLindelof_sUnion, Set.forall_mem_range, Set.Mem, iSup, setOf, Set.countable_range, Set.iUnion
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : s.Countable
⊢ IsLindelof s

Tactic:
biUnion_of_singleton s ▸ hs.isLindelof_biUnion fun _ _ => isLindelof_singleton

Premises used: Set.Countable.isLindelof_biUnion, isLindelof_singleton, Set.biUnion_of_singleton, Eq.rec
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : s.Finite
⊢ IsLindelof s

Tactic:
biUnion_of_singleton s ▸ hs.isLindelof_biUnion fun _ _ => isLindelof_singleton

Premises used: isLindelof_singleton, Set.biUnion_of_singleton, Eq.rec, Set.Finite.isLindelof_biUnion
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
inst_1 : DiscreteTopology X
hs : IsLindelof s
⊢ ∀ (x : X), {x} ∈ 𝓝 x

Tactic:
simp [nhds_discrete]

Premises used: nhds_discrete
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
inst_1 : DiscreteTopology X
hs : IsLindelof s
⊢ ∀ (x : X), {x} ∈ 𝓝 x

Tactic:
have : ∀ x : X, ({x} : Set X) ∈ 𝓝 x := by simp [nhds_discrete]
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
inst_1 : DiscreteTopology X
hs : IsLindelof s
this : ∀ (x : X), {x} ∈ 𝓝 x
rcases : ∀ (t : Set X) (ht : t.Countable), (∀ x ∈ t, x ∈ s) → ∀ (hssubt : s ⊆ ⋃ x ∈ t, {x}), s.Countable
⊢ s.Countable

Tactic:
rcases hs.elim_nhds_subcover (fun x => {x}) fun x _ => this x with ⟨t, ht, _, hssubt⟩

Premises used: IsLindelof.elim_nhds_subcover, Singleton.singleton
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
inst_1 : DiscreteTopology X
hs : IsLindelof s
this : ∀ (x : X), {x} ∈ 𝓝 x
t : Set X
ht : t.Countable
left : ∀ x ∈ t, x ∈ s
hssubt : s ⊆ ⋃ x ∈ t, {x}
⊢ s ⊆ t

Tactic:
rw [biUnion_of_singleton] at hssubt

Premises used: Set.biUnion_of_singleton
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
inst_1 : DiscreteTopology X
hs : IsLindelof s
this : ∀ (x : X), {x} ∈ 𝓝 x
t : Set X
ht : t.Countable
left : ∀ x ∈ t, x ∈ s
hssubt : s ⊆ t
⊢ s.Countable

Tactic:
ht.mono hssubt

Premises used: Set.Countable.mono
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
inst_1 : DiscreteTopology X
hs : IsLindelof s
this : ∀ (x : X), {x} ∈ 𝓝 x
t : Set X
ht : t.Countable
left : ∀ x ∈ t, x ∈ s
hssubt : s ⊆ t
⊢ s.Countable

Tactic:
exact ht.mono hssubt

Premises used: Set.Countable.mono
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
inst_1 : DiscreteTopology X
⊢ IsLindelof s ↔ s.Countable

Tactic:
⟨fun h => h.countable_of_discrete, fun h => h.isLindelof⟩

Premises used: Iff.intro, IsLindelof.countable_of_discrete, Set.Countable.isLindelof
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hs : IsLindelof s
ht : IsLindelof t
rw : IsLindelof.{u} (X := X) (⋃ (b : Bool), bif b then s else t)
⊢ IsLindelof (s ∪ t)

Tactic:
rw [union_eq_iUnion]

Premises used: Set.union_eq_iUnion
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hs : IsLindelof s
ht : IsLindelof t
b : Bool
false : IsLindelof (bif Bool.false then s else t)
true : IsLindelof (bif Bool.true then s else t)
⊢ IsLindelof (bif b then s else t)

Tactic:
cases b
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hs : IsLindelof s
ht : IsLindelof t
⊢ IsLindelof (bif false then s else t)

Tactic:
assumption
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hs : IsLindelof s
ht : IsLindelof t
⊢ IsLindelof (bif true then s else t)

Tactic:
assumption
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hs : IsLindelof s
ht : IsLindelof t
⊢ IsLindelof.{u} (X := X) (⋃ (b : Bool), bif b then s else t)

Tactic:
exact isLindelof_iUnion fun b => by cases b <;> assumption

Premises used: isLindelof_iUnion
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsLindelof s
a : X
⊢ IsLindelof (insert a s)

Tactic:
isLindelof_singleton.union hs

Premises used: Set.insert, Set.Mem, setOf, IsLindelof.union, isLindelof_singleton, Set.singleton
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
U : Set X
mp : IsLindelof U ∧ IsOpen[inst] U → ∃ (s : Set ι), s.Countable ∧ U = ⋃ i ∈ s, b i
mpr : (∃ (s : Set ι), s.Countable ∧ U = ⋃ i ∈ s, b i) → IsLindelof U ∧ IsOpen[inst] U
⊢ IsLindelof U ∧ IsOpen[inst] U ↔ ∃ (s : Set ι), s.Countable ∧ U = ⋃ i ∈ s, b i

Tactic:
constructor
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
U : Set X
h₁ : IsLindelof U
h₂ : IsOpen[inst] U
mp :
  ∀ (Y : Type u) (f : Y → Set X) (hf : ∀ (i : Y), f i ∈ range b) (h₁ : IsLindelof.{u} (X := X) (⋃ (i : Y), f i))
    (h₂ : IsOpen[inst] (⋃ (i : Y), f i)),
    ∃ (s : Set ι), s.Countable ∧ Eq.{u + 1} (α := Set X) (⋃ (i : Y), f i) (⋃ i ∈ s, b i)
⊢ ∃ (s : Set ι), s.Countable ∧ U = ⋃ i ∈ s, b i

Tactic:
obtain ⟨Y, f, rfl, hf⟩ := hb.open_eq_iUnion h₂

Premises used: TopologicalSpace.IsTopologicalBasis.open_eq_iUnion, rfl
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
Y : Type u
f : Y → Set X
hf : ∀ (i : Y), f i ∈ range b
h₁ : IsLindelof.{u} (X := X) (⋃ (i : Y), f i)
h₂ : IsOpen[inst] (⋃ (i : Y), f i)
mp :
  ∀ (f' : (i : Y) → ι) (hf' : ∀ (i : Y), b (f' i) = f i),
    ∃ (s : Set ι), s.Countable ∧ Eq.{u + 1} (α := Set X) (⋃ (i : Y), f i) (⋃ i ∈ s, b i)
⊢ ∃ (s : Set ι), s.Countable ∧ Eq.{u + 1} (α := Set X) (⋃ (i : Y), f i) (⋃ i ∈ s, b i)

Tactic:
choose f' hf' using hf
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
Y : Type u
f : Y → Set X
h₁ : IsLindelof.{u} (X := X) (⋃ (i : Y), f i)
h₂ : IsOpen[inst] (⋃ (i : Y), f i)
f' : (i : Y) → ι
hf' : ∀ (i : Y), b (f' i) = f i
⊢ b ∘ f' = f

Tactic:
have : b ∘ f' = f := funext hf'
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
Y : Type u
f : Y → Set X
h₁ : IsLindelof.{u} (X := X) (⋃ (i : Y), f i)
h₂ : IsOpen[inst] (⋃ (i : Y), f i)
f' : (i : Y) → ι
hf' : ∀ (i : Y), b (f' i) = f i
this : b ∘ f' = f
mp :
  ∀ (h₁ : IsLindelof.{u} (X := X) (⋃ (i : Y), (b ∘ f') i)) (h₂ : IsOpen[inst] (⋃ (i : Y), (b ∘ f') i))
    (hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i),
    ∃ (s : Set ι), s.Countable ∧ Eq.{u + 1} (α := Set X) (⋃ (i : Y), (b ∘ f') i) (⋃ i ∈ s, b i)
⊢ ∃ (s : Set ι), s.Countable ∧ Eq.{u + 1} (α := Set X) (⋃ (i : Y), f i) (⋃ i ∈ s, b i)

Tactic:
subst this
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
Y : Type u
f' : (i : Y) → ι
h₁ : IsLindelof.{u} (X := X) (⋃ (i : Y), (b ∘ f') i)
h₂ : IsOpen[inst] (⋃ (i : Y), (b ∘ f') i)
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
mp :
  ∀ (t : Set Y) (ht : t.Countable ∧ Subset.{u} (α := Set X) (⋃ (i : Y), (b ∘ f') i) (⋃ i ∈ t, (b ∘ f') i)),
    ∃ (s : Set ι), s.Countable ∧ Eq.{u + 1} (α := Set X) (⋃ (i : Y), (b ∘ f') i) (⋃ i ∈ s, b i)
⊢ ∃ (s : Set ι), s.Countable ∧ Eq.{u + 1} (α := Set X) (⋃ (i : Y), (b ∘ f') i) (⋃ i ∈ s, b i)

Tactic:
obtain ⟨t, ht⟩ :=
      h₁.elim_countable_subcover (b ∘ f') (fun i => hb.isOpen (Set.mem_range_self _)) Subset.rfl

Premises used: Set.mem_range_self, TopologicalSpace.IsTopologicalBasis.isOpen, Function.comp, Set.Subset.rfl, IsLindelof.elim_countable_subcover
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
Y : Type u
f' : (i : Y) → ι
h₁ : IsLindelof.{u} (X := X) (⋃ (i : Y), (b ∘ f') i)
h₂ : IsOpen[inst] (⋃ (i : Y), (b ∘ f') i)
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Set Y
ht : t.Countable ∧ Subset.{u} (α := Set X) (⋃ (i : Y), (b ∘ f') i) (⋃ i ∈ t, (b ∘ f') i)
⊢ ∃ (s : Set ι), s.Countable ∧ Eq.{u + 1} (α := Set X) (⋃ (i : Y), (b ∘ f') i) (⋃ i ∈ s, b i)

Tactic:
⟨t.image f', Countable.image (ht.1) f', le_antisymm ?_ ?_⟩

Premises used: Set.Countable.image, le_antisymm, And.left, And.intro, Exists.intro, Set.image
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
Y : Type u
f' : (i : Y) → ι
h₁ : IsLindelof.{u} (X := X) (⋃ (i : Y), (b ∘ f') i)
h₂ : IsOpen[inst] (⋃ (i : Y), (b ∘ f') i)
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Set Y
ht : t.Countable ∧ Subset.{u} (α := Set X) (⋃ (i : Y), (b ∘ f') i) (⋃ i ∈ t, (b ∘ f') i)
mp : LE.le.{u} (α := Set X) (⋃ (i : Y), (b ∘ f') i) (⋃ i ∈ f' '' t, b i)
mp₁ : LE.le.{u} (α := Set X) (⋃ i ∈ f' '' t, b i) (⋃ (i : Y), (b ∘ f') i)
⊢ ∃ (s : Set ι), s.Countable ∧ Eq.{u + 1} (α := Set X) (⋃ (i : Y), (b ∘ f') i) (⋃ i ∈ s, b i)

Tactic:
refine ⟨t.image f', Countable.image (ht.1) f', le_antisymm ?_ ?_⟩
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
Y : Type u
f' : (i : Y) → ι
h₁ : IsLindelof.{u} (X := X) (⋃ (i : Y), (b ∘ f') i)
h₂ : IsOpen[inst] (⋃ (i : Y), (b ∘ f') i)
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Set Y
ht : t.Countable ∧ Subset.{u} (α := Set X) (⋃ (i : Y), (b ∘ f') i) (⋃ i ∈ t, (b ∘ f') i)
⊢ LE.le.{u} (α := Set X) (⋃ (i : Y), (b ∘ f') i) (⋃ i ∈ f' '' t, b i)

Tactic:
Set.Subset.trans ht.2 ?_

Premises used: Set.Subset.trans, And.right
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
Y : Type u
f' : (i : Y) → ι
h₁ : IsLindelof.{u} (X := X) (⋃ (i : Y), (b ∘ f') i)
h₂ : IsOpen[inst] (⋃ (i : Y), (b ∘ f') i)
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Set Y
ht : t.Countable ∧ Subset.{u} (α := Set X) (⋃ (i : Y), (b ∘ f') i) (⋃ i ∈ t, (b ∘ f') i)
mp : Subset.{u} (α := Set X) (⋃ i ∈ t, (b ∘ f') i) (⋃ i ∈ f' '' t, b i)
⊢ LE.le.{u} (α := Set X) (⋃ (i : Y), (b ∘ f') i) (⋃ i ∈ f' '' t, b i)

Tactic:
refine Set.Subset.trans ht.2 ?_

Premises used: Set.Subset.trans, And.right
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
Y : Type u
f' : (i : Y) → ι
h₁ : IsLindelof.{u} (X := X) (⋃ (i : Y), (b ∘ f') i)
h₂ : IsOpen[inst] (⋃ (i : Y), (b ∘ f') i)
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Set Y
ht : t.Countable ∧ Subset.{u} (α := Set X) (⋃ (i : Y), (b ∘ f') i) (⋃ i ∈ t, (b ∘ f') i)
mp : ∀ (i : Y) (i_1 : i ∈ t), (b ∘ f') i ⊆ ⋃ i ∈ f' '' t, b i
⊢ Subset.{u} (α := Set X) (⋃ i ∈ t, (b ∘ f') i) (⋃ i ∈ f' '' t, b i)

Tactic:
simp only [Set.iUnion_subset_iff]

Premises used: Set.iUnion_subset_iff
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
Y : Type u
f' : (i : Y) → ι
h₁ : IsLindelof.{u} (X := X) (⋃ (i : Y), (b ∘ f') i)
h₂ : IsOpen[inst] (⋃ (i : Y), (b ∘ f') i)
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Set Y
ht : t.Countable ∧ Subset.{u} (α := Set X) (⋃ (i : Y), (b ∘ f') i) (⋃ i ∈ t, (b ∘ f') i)
i : Y
hi : i ∈ t
mp : (b ∘ f') i ⊆ ⋃ (x : { x : ι // x ∈ f' '' t }), b (↑x : ι)
⊢ (b ∘ f') i ⊆ ⋃ i ∈ f' '' t, b i

Tactic:
rw [← Set.iUnion_subtype (fun x : ι => x ∈ t.image f') fun i => b i.1]

Premises used: Membership.mem, Set.iUnion_subtype, Set.image, Subtype.val
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
Y : Type u
f' : (i : Y) → ι
h₁ : IsLindelof.{u} (X := X) (⋃ (i : Y), (b ∘ f') i)
h₂ : IsOpen[inst] (⋃ (i : Y), (b ∘ f') i)
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Set Y
ht : t.Countable ∧ Subset.{u} (α := Set X) (⋃ (i : Y), (b ∘ f') i) (⋃ i ∈ t, (b ∘ f') i)
i : Y
hi : i ∈ t
⊢ (b ∘ f') i ⊆ ⋃ (x : { x : ι // x ∈ f' '' t }), b (↑x : ι)

Tactic:
Set.subset_iUnion (fun i : t.image f' => b i) ⟨_, mem_image_of_mem _ hi⟩

Premises used: Subtype.mk, Set.subset_iUnion, Set.mem_image_of_mem, Subtype.val
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
Y : Type u
f' : (i : Y) → ι
h₁ : IsLindelof.{u} (X := X) (⋃ (i : Y), (b ∘ f') i)
h₂ : IsOpen[inst] (⋃ (i : Y), (b ∘ f') i)
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Set Y
ht : t.Countable ∧ Subset.{u} (α := Set X) (⋃ (i : Y), (b ∘ f') i) (⋃ i ∈ t, (b ∘ f') i)
i : Y
hi : i ∈ t
⊢ (b ∘ f') i ⊆ ⋃ (x : { x : ι // x ∈ f' '' t }), b (↑x : ι)

Tactic:
exact Set.subset_iUnion (fun i : t.image f' => b i) ⟨_, mem_image_of_mem _ hi⟩

Premises used: Subtype.mk, Set.subset_iUnion, Set.mem_image_of_mem, Subtype.val
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
Y : Type u
f' : (i : Y) → ι
h₁ : IsLindelof.{u} (X := X) (⋃ (i : Y), (b ∘ f') i)
h₂ : IsOpen[inst] (⋃ (i : Y), (b ∘ f') i)
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Set Y
ht : t.Countable ∧ Subset.{u} (α := Set X) (⋃ (i : Y), (b ∘ f') i) (⋃ i ∈ t, (b ∘ f') i)
mp : ∀ (i : ι) (j : i ∈ f' '' t), b i ⊆ ⋃ (i : Y), (b ∘ f') i
⊢ LE.le.{u} (α := Set X) (⋃ i ∈ f' '' t, b i) (⋃ (i : Y), (b ∘ f') i)

Tactic:
apply Set.iUnion₂_subset

Premises used: Set.iUnion₂_subset
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
Y : Type u
f' : (i : Y) → ι
h₁ : IsLindelof.{u} (X := X) (⋃ (i : Y), (b ∘ f') i)
h₂ : IsOpen[inst] (⋃ (i : Y), (b ∘ f') i)
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Set Y
ht : t.Countable ∧ Subset.{u} (α := Set X) (⋃ (i : Y), (b ∘ f') i) (⋃ i ∈ t, (b ∘ f') i)
i : ι
hi : i ∈ f' '' t
mp : ∀ (j : Y) (hi : f' j ∈ f' '' t), b (f' j) ⊆ ⋃ (i : Y), (b ∘ f') i
⊢ b i ⊆ ⋃ (i : Y), (b ∘ f') i

Tactic:
obtain ⟨j, -, rfl⟩ := (mem_image ..).mp hi

Premises used: Set.mem_image, Iff.mp, rfl
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
Y : Type u
f' : (i : Y) → ι
h₁ : IsLindelof.{u} (X := X) (⋃ (i : Y), (b ∘ f') i)
h₂ : IsOpen[inst] (⋃ (i : Y), (b ∘ f') i)
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Set Y
ht : t.Countable ∧ Subset.{u} (α := Set X) (⋃ (i : Y), (b ∘ f') i) (⋃ i ∈ t, (b ∘ f') i)
j : Y
hi : f' j ∈ f' '' t
⊢ b (f' j) ⊆ ⋃ (i : Y), (b ∘ f') i

Tactic:
Set.subset_iUnion (b ∘ f') j

Premises used: Function.comp, Set.subset_iUnion
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
Y : Type u
f' : (i : Y) → ι
h₁ : IsLindelof.{u} (X := X) (⋃ (i : Y), (b ∘ f') i)
h₂ : IsOpen[inst] (⋃ (i : Y), (b ∘ f') i)
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Set Y
ht : t.Countable ∧ Subset.{u} (α := Set X) (⋃ (i : Y), (b ∘ f') i) (⋃ i ∈ t, (b ∘ f') i)
j : Y
hi : f' j ∈ f' '' t
⊢ b (f' j) ⊆ ⋃ (i : Y), (b ∘ f') i

Tactic:
exact Set.subset_iUnion (b ∘ f') j

Premises used: Function.comp, Set.subset_iUnion
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
s : Set ι
hs : s.Countable
mpr : IsLindelof.{u} (X := X) (⋃ i ∈ s, b i)
mpr₁ : IsOpen[inst] (⋃ i ∈ s, b i)
⊢ IsLindelof.{u} (X := X) (⋃ i ∈ s, b i) ∧ IsOpen[inst] (⋃ i ∈ s, b i)

Tactic:
constructor
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
s : Set ι
hs : s.Countable
⊢ IsLindelof.{u} (X := X) (⋃ i ∈ s, b i)

Tactic:
hs.isLindelof_biUnion fun i _ => hb' i

Premises used: Set.Countable.isLindelof_biUnion
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
s : Set ι
hs : s.Countable
⊢ IsLindelof.{u} (X := X) (⋃ i ∈ s, b i)

Tactic:
exact hs.isLindelof_biUnion fun i _ => hb' i

Premises used: Set.Countable.isLindelof_biUnion
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
s : Set ι
hs : s.Countable
⊢ IsOpen[inst] (⋃ i ∈ s, b i)

Tactic:
isOpen_biUnion fun i _ => hb.isOpen (Set.mem_range_self _)

Premises used: Set.mem_range_self, TopologicalSpace.IsTopologicalBasis.isOpen, isOpen_biUnion