awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u_1
ts : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : (u : Set α) → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
u : Set α
hu : u ∈ s'
v : Set α
hv : v ∈ f u
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | IsOpen[ts] s} v
have refine_2 : Membership.mem (γ := Set (Set α)) {s : Set α | IsOpen[generateFrom t] s} v
Tactic: rw [ht]
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u_1
ts : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : (u : Set α) → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
u : Set α
hu : u ∈ s'
v : Set α
hv : v ∈ f u
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | IsOpen[generateFrom t] s} v
have refine_2 : v ∈ t
Tactic: apply isOpen_generateFrom_of_mem
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u_1
ts : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : (u : Set α) → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
⊢ generateFrom (⋃ u ∈ s', f u) ≤ ts
have refine_2 : generateFrom (⋃ u ∈ s', f u) ≤ generateFrom s'
Tactic: rw [hs'.eq_generateFrom]
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u_1
ts : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : (u : Set α) → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
⊢ generateFrom (⋃ u ∈ s', f u) ≤ generateFrom s'
have refine_2 : s' ⊆ {s : Set α | IsOpen[generateFrom (⋃ u ∈ s', f u)] s}
Tactic: apply le_generateFrom_iff_subset_isOpen.2
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u_1
ts : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : (u : Set α) → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
u : Set α
hu : u ∈ s'
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | IsOpen[generateFrom (⋃ u ∈ s', f u)] s} u
have refine_2 : Membership.mem (γ := Set (Set α)) {s : Set α | IsOpen[generateFrom (⋃ u ∈ s', f u)] s} (⋂ i ∈ f u, i)
Tactic: rw [← hf u hu, sInter_eq_biInter]
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u_1
ts : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : (u : Set α) → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
u : Set α
hu : u ∈ s'
⊢ IsOpen[generateFrom (⋃ u ∈ s', f u)] (⋂ i ∈ f u, i)
have refine_2 : (f u).Finite
Tactic: apply @Finite.isOpen_biInter _ _ (generateFrom (⋃ u ∈ s', f u)) _ _
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u_1
ts : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : (u : Set α) → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
u : Set α
hu : u ∈ s'
refine_2 : (f u).Finite
⊢ IsOpen[generateFrom (⋃ u ∈ s', f u)] (⋂ i ∈ f u, i)
have refine_2₁ : ∀ i ∈ f u, IsOpen[generateFrom (⋃ u ∈ s', f u)] i
Tactic: apply @Finite.isOpen_biInter _ _ (generateFrom (⋃ u ∈ s', f u)) _ _
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u_1
ts : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : (u : Set α) → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
u : Set α
hu : u ∈ s'
i : Set α
hi : i ∈ f u
⊢ IsOpen[generateFrom (⋃ u ∈ s', f u)] i
have refine_2 : Membership.mem (γ := Set (Set α)) (⋃ u ∈ s', f u) i
Tactic: apply isOpen_generateFrom_of_mem
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u_1
ts : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : (u : Set α) → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
u : Set α
hu : u ∈ s'
i : Set α
hi : i ∈ f u
⊢ Membership.mem (γ := Set (Set α)) (⋃ u ∈ s', f u) i
have refine_2 : ∃ i_1 ∈ s', i ∈ f i_1
Tactic: simp
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → TopologicalSpace (E i)
s : (i : ι) → Set (Set (E i))
hs : ∀ (i : ι), IsTopologicalBasis (s i)
⊢ IsTopologicalBasis (α := (i : ι) × E i)
    (⋃ (i : ι), (fun (u : Set (E i)) ↦ Sigma.mk (β := fun (i : ι) ↦ E i) i '' u) '' s i)
have refine : ∀ (a : (i : ι) × E i),
  (𝓝 a).HasBasis
    (fun (t : Set ((i : ι) × E i)) ↦
      Membership.mem (γ := Set (Set ((i : ι) × E i)))
          (⋃ (i : ι), (fun (u : Set (E i)) ↦ Sigma.mk (β := fun (i : ι) ↦ E i) i '' u) '' s i) t ∧
        a ∈ t)
    id
Tactic: refine .of_hasBasis_nhds fun a ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → TopologicalSpace (E i)
s : (i : ι) → Set (Set (E i))
hs : ∀ (i : ι), IsTopologicalBasis (s i)
a : (i : ι) × E i
⊢ (𝓝 a).HasBasis
    (fun (t : Set ((i : ι) × E i)) ↦
      Membership.mem (γ := Set (Set ((i : ι) × E i)))
          (⋃ (i : ι), (fun (u : Set (E i)) ↦ Sigma.mk (β := fun (i : ι) ↦ E i) i '' u) '' s i) t ∧
        a ∈ t)
    id
have rw : (map (Sigma.mk (β := fun (i : ι) ↦ E i) (a.fst (β := fun (i : ι) ↦ E i))) (𝓝 (a.snd (β := fun (i : ι) ↦ E i)))).HasBasis
  (fun (t : Set ((i : ι) × E i)) ↦
    Membership.mem (γ := Set (Set ((i : ι) × E i)))
        (⋃ (i : ι), (fun (u : Set (E i)) ↦ Sigma.mk (β := fun (i : ι) ↦ E i) i '' u) '' s i) t ∧
      a ∈ t)
  id
Tactic: rw [Sigma.nhds_eq]
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → TopologicalSpace (E i)
s : (i : ι) → Set (Set (E i))
hs : ∀ (i : ι), IsTopologicalBasis (s i)
a : (i : ι) × E i
⊢ (map (Sigma.mk (β := fun (i : ι) ↦ E i) (a.fst (β := fun (i : ι) ↦ E i)))
        (𝓝 (a.snd (β := fun (i : ι) ↦ E i)))).HasBasis
    (fun (t : Set ((i : ι) × E i)) ↦
      Membership.mem (γ := Set (Set ((i : ι) × E i)))
          (⋃ (i : ι), (fun (u : Set (E i)) ↦ Sigma.mk (β := fun (i : ι) ↦ E i) i '' u) '' s i) t ∧
        a ∈ t)
    id
have h : ∀ (x : Set ((i : ι) × E i)),
  Membership.mem (γ := Set (Set ((i : ι) × E i)))
        (⋃ (i : ι), (fun (u : Set (E i)) ↦ Sigma.mk (β := fun (i : ι) ↦ E i) i '' u) '' s i) x ∧
      a ∈ x ↔
    Membership.mem (γ := Set (Set ((i : ι) × E i)))
      ((fun (i : Set (E (a.fst (β := fun (i : ι) ↦ E i)))) ↦
          Sigma.mk (β := fun (i : ι) ↦ E i) (a.fst (β := fun (i : ι) ↦ E i)) '' i) ''
        {i : Set (E (a.fst (β := fun (i : ι) ↦ E i))) |
          Membership.mem (γ := Set (Set (E (a.fst (β := fun (i : ι) ↦ E i))))) (s (a.fst (β := fun (i : ι) ↦ E i))) i ∧
            a.snd (β := fun (i : ι) ↦ E i) ∈ i})
      x
Tactic: convert! (((hs a.1).nhds_hasBasis).map _).to_image_id
-- Lean 4 proof step from Mathlib.Topology.Bases (hypothesis)
Goal:
α : Type u
t : TopologicalSpace α
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → TopologicalSpace (E i)
inst_1 : Countable ι
inst_2 : ∀ (i : ι), SecondCountableTopology.{u_2} (E i)
b : Set (Set ((i : ι) × E i)) :=
  ⋃ (i : ι), (fun (u : Set (E i)) ↦ Sigma.mk (β := fun (i : ι) ↦ E i) i '' u) '' countableBasis (E i)
⊢ SecondCountableTopology ((i : ι) × E i)
have A : IsTopologicalBasis b
Tactic: have A : IsTopologicalBasis b := IsTopologicalBasis.sigma fun i => isBasis_countableBasis _
-- Lean 4 proof step from Mathlib.Topology.Bases (hypothesis)
Goal:
α : Type u
t : TopologicalSpace α
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → TopologicalSpace (E i)
inst_1 : Countable ι
inst_2 : ∀ (i : ι), SecondCountableTopology.{u_2} (E i)
b : Set (Set ((i : ι) × E i)) :=
  ⋃ (i : ι), (fun (u : Set (E i)) ↦ Sigma.mk (β := fun (i : ι) ↦ E i) i '' u) '' countableBasis (E i)
A : IsTopologicalBasis b
⊢ SecondCountableTopology ((i : ι) × E i)
have B : b.Countable
Tactic: have B : b.Countable := countable_iUnion fun i => (countable_countableBasis _).image _
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t_1 : TopologicalSpace α
β : Type u_1
inst : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
⊢ IsTopologicalBasis (α := α ⊕ β) ((fun (u : Set α) ↦ Sum.inl '' u) '' s ∪ (fun (u : Set β) ↦ Sum.inr '' u) '' t)
have h_open : ∀ (u : Set (α ⊕ β)),
  Membership.mem (γ := Set (Set (α ⊕ β)))
      ((fun (u : Set α) ↦ Sum.inl '' u) '' s ∪ (fun (u : Set β) ↦ Sum.inr '' u) '' t) u →
    IsOpen[instTopologicalSpaceSum] u
Tactic: apply isTopologicalBasis_of_isOpen_of_nhds
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t_1 : TopologicalSpace α
β : Type u_1
inst : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
h_open :
  ∀ (u : Set (α ⊕ β)),
    Membership.mem (γ := Set (Set (α ⊕ β)))
        ((fun (u : Set α) ↦ Sum.inl '' u) '' s ∪ (fun (u : Set β) ↦ Sum.inr '' u) '' t) u →
      IsOpen[instTopologicalSpaceSum] u
⊢ IsTopologicalBasis (α := α ⊕ β) ((fun (u : Set α) ↦ Sum.inl '' u) '' s ∪ (fun (u : Set β) ↦ Sum.inr '' u) '' t)
have h_nhds : ∀ (a : α ⊕ β) (u : Set (α ⊕ β)),
  a ∈ u →
    IsOpen[instTopologicalSpaceSum] u →
      ∃ (v : Set (α ⊕ β)),
        Membership.mem (γ := Set (Set (α ⊕ β)))
            ((fun (u : Set α) ↦ Sum.inl '' u) '' s ∪ (fun (u : Set β) ↦ Sum.inr '' u) '' t) v ∧
          a ∈ v ∧ v ⊆ u
Tactic: apply isTopologicalBasis_of_isOpen_of_nhds
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t_1 : TopologicalSpace α
β : Type u_1
inst : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
x : α
u : Set (α ⊕ β)
hxu : Sum.inl x ∈ u
u_open : IsOpen[instTopologicalSpaceSum] u
⊢ ∃ (v : Set (α ⊕ β)),
    Membership.mem (γ := Set (Set (α ⊕ β)))
        ((fun (u : Set α) ↦ Sum.inl '' u) '' s ∪ (fun (u : Set β) ↦ Sum.inr '' u) '' t) v ∧
      Sum.inl x ∈ v ∧ v ⊆ u
have h_nhds : ∀ (v : Set α) (vs : v ∈ s) (xv : x ∈ v) (vu : v ⊆ Sum.inl ⁻¹' u),
  ∃ (v : Set (α ⊕ β)),
    Membership.mem (γ := Set (Set (α ⊕ β)))
        ((fun (u : Set α) ↦ Sum.inl '' u) '' s ∪ (fun (u : Set β) ↦ Sum.inr '' u) '' t) v ∧
      Sum.inl x ∈ v ∧ v ⊆ u
Tactic: obtain ⟨v, vs, xv, vu⟩ : ∃ v ∈ s, x ∈ v ∧ v ⊆ Sum.inl ⁻¹' u :=
        hs.exists_subset_of_mem_open hxu (isOpen_sum_iff.1 u_open).1
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t_1 : TopologicalSpace α
β : Type u_1
inst : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
x : β
u : Set (α ⊕ β)
hxu : Sum.inr x ∈ u
u_open : IsOpen[instTopologicalSpaceSum] u
⊢ ∃ (v : Set (α ⊕ β)),
    Membership.mem (γ := Set (Set (α ⊕ β)))
        ((fun (u : Set α) ↦ Sum.inl '' u) '' s ∪ (fun (u : Set β) ↦ Sum.inr '' u) '' t) v ∧
      Sum.inr x ∈ v ∧ v ⊆ u
have h_nhds : ∀ (v : Set β) (vs : v ∈ t) (xv : x ∈ v) (vu : v ⊆ Sum.inr ⁻¹' u),
  ∃ (v : Set (α ⊕ β)),
    Membership.mem (γ := Set (Set (α ⊕ β)))
        ((fun (u : Set α) ↦ Sum.inl '' u) '' s ∪ (fun (u : Set β) ↦ Sum.inr '' u) '' t) v ∧
      Sum.inr x ∈ v ∧ v ⊆ u
Tactic: obtain ⟨v, vs, xv, vu⟩ : ∃ v ∈ t, x ∈ v ∧ v ⊆ Sum.inr ⁻¹' u :=
        ht.exists_subset_of_mem_open hxu (isOpen_sum_iff.1 u_open).2
-- Lean 4 proof step from Mathlib.Topology.Bases (hypothesis)
Goal:
α : Type u
t : TopologicalSpace α
β : Type u_1
inst : TopologicalSpace β
inst_1 : SecondCountableTopology α
inst_2 : SecondCountableTopology β
b : Set (Set (α ⊕ β)) :=
  (fun (u : Set α) ↦ Sum.inl '' u) '' countableBasis α ∪ (fun (u : Set β) ↦ Sum.inr '' u) '' countableBasis β
⊢ SecondCountableTopology (α ⊕ β)
have A : IsTopologicalBasis b
Tactic: have A : IsTopologicalBasis b := (isBasis_countableBasis α).sum (isBasis_countableBasis β)
-- Lean 4 proof step from Mathlib.Topology.Bases (hypothesis)
Goal:
α : Type u
t : TopologicalSpace α
β : Type u_1
inst : TopologicalSpace β
inst_1 : SecondCountableTopology α
inst_2 : SecondCountableTopology β
b : Set (Set (α ⊕ β)) :=
  (fun (u : Set α) ↦ Sum.inl '' u) '' countableBasis α ∪ (fun (u : Set β) ↦ Sum.inr '' u) '' countableBasis β
A : IsTopologicalBasis b
⊢ SecondCountableTopology (α ⊕ β)
have B : b.Countable
Tactic: have B : b.Countable :=
    (Countable.image (countable_countableBasis _) _).union
      (Countable.image (countable_countableBasis _) _)
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : IsQuotientMap π
h : IsOpenMap π
⊢ IsTopologicalBasis (image π '' V)
have h_open : ∀ u ∈ image π '' V, IsOpen[inst_1] u
Tactic: apply isTopologicalBasis_of_isOpen_of_nhds
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : IsQuotientMap π
h : IsOpenMap π
h_open : ∀ u ∈ image π '' V, IsOpen[inst_1] u
⊢ IsTopologicalBasis (image π '' V)
have h_nhds : ∀ (a : Y) (u : Set Y), a ∈ u → IsOpen[inst_1] u → ∃ v ∈ image π '' V, a ∈ v ∧ v ⊆ u
Tactic: apply isTopologicalBasis_of_isOpen_of_nhds
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : IsQuotientMap π
h : IsOpenMap π
y : Y
U : Set Y
y_in_U : y ∈ U
U_open : IsOpen[inst_1] U
⊢ ∃ v ∈ image π '' V, y ∈ v ∧ v ⊆ U
have h_nhds : ∀ (x : X) (y_in_U : π x ∈ U), ∃ v ∈ image π '' V, π x ∈ v ∧ v ⊆ U
Tactic: obtain ⟨x, rfl⟩ := h'.surjective y
Cleared hypotheses: y, y_in_U
-- Lean 4 proof step from Mathlib.Topology.Bases (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : IsQuotientMap π
h : IsOpenMap π
U : Set Y
U_open : IsOpen[inst_1] U
x : X
y_in_U : π x ∈ U
W : Set X := π ⁻¹' U
⊢ ∃ v ∈ image π '' V, π x ∈ v ∧ v ⊆ U
have x_in_W : x ∈ W
Tactic: have x_in_W : x ∈ W := y_in_U
-- Lean 4 proof step from Mathlib.Topology.Bases (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : IsQuotientMap π
h : IsOpenMap π
U : Set Y
U_open : IsOpen[inst_1] U
x : X
y_in_U : π x ∈ U
W : Set X := π ⁻¹' U
x_in_W : x ∈ W
⊢ ∃ v ∈ image π '' V, π x ∈ v ∧ v ⊆ U
have W_open : IsOpen[inst] W
Tactic: have W_open : IsOpen W := U_open.preimage h'.continuous
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : IsQuotientMap π
h : IsOpenMap π
U : Set Y
U_open : IsOpen[inst_1] U
x : X
y_in_U : π x ∈ U
W : Set X := π ⁻¹' U
x_in_W : x ∈ W
W_open : IsOpen[inst] W
⊢ ∃ v ∈ image π '' V, π x ∈ v ∧ v ⊆ U
have h_nhds : ∀ (Z : Set X) (Z_in_V : Z ∈ V) (x_in_Z : x ∈ Z) (Z_in_W : Z ⊆ W), ∃ v ∈ image π '' V, π x ∈ v ∧ v ⊆ U
Tactic: obtain ⟨Z, Z_in_V, x_in_Z, Z_in_W⟩ := hV.exists_subset_of_mem_open x_in_W W_open
-- Lean 4 proof step from Mathlib.Topology.Bases (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : IsQuotientMap π
h : IsOpenMap π
U : Set Y
U_open : IsOpen[inst_1] U
x : X
y_in_U : π x ∈ U
W : Set X := π ⁻¹' U
x_in_W : x ∈ W
W_open : IsOpen[inst] W
Z : Set X
Z_in_V : Z ∈ V
x_in_Z : x ∈ Z
Z_in_W : Z ⊆ W
⊢ ∃ v ∈ image π '' V, π x ∈ v ∧ v ⊆ U
have XZ_in_U : π '' Z ⊆ U
Tactic: have XZ_in_U : π '' Z ⊆ U := (Set.image_mono Z_in_W).trans (image_preimage_subset π U)
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : TopologicalSpace Y
π : X → Y
inst_2 : SecondCountableTopology X
h' : IsQuotientMap π
h : IsOpenMap π
⊢ ∃ (b : Set (Set Y)), b.Countable ∧ inst_1 = generateFrom b
have obtain : ∀ (V : Set (Set X)) (V_countable : V.Countable) (V_generates : IsTopologicalBasis V),
  ∃ (b : Set (Set Y)), b.Countable ∧ inst_1 = generateFrom b
Tactic: obtain ⟨V, V_countable, -, V_generates⟩ := exists_countable_basis X
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f : α → β
inst_1 : TopologicalSpace β
inst_2 : SecondCountableTopology β
hf : IsInducing f
⊢ SecondCountableTopology α
have rw : SecondCountableTopology α
Tactic: rw [hf.1]
-- Lean 4 proof step from Mathlib.Topology.Bases (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : SecondCountableTopology β
f : α → β
hf : IsEmbedding f
⊢ SeparableSpace α
have this : SecondCountableTopology α
Tactic: have := hf.secondCountableTopology
-- Lean 4 proof step from Mathlib.Topology.Basic (goal)
Goal:
X : Type u
T : Set (Set X)
empty_mem : ∅ ∈ T
sInter_mem : ∀ A ⊆ T, ⋂₀ A ∈ T
union_mem : ∀ A ∈ T, ∀ B ∈ T, A ∪ B ∈ T
s : Set (Set X)
hs : ∀ t ∈ s, tᶜ ∈ T
⊢ (⋃₀ s)ᶜ ∈ T
have simp : ⋂₀ (compl '' s) ∈ T
Tactic: simp only [Set.compl_sUnion]
-- Lean 4 proof step from Mathlib.Topology.Basic (goal)
Goal:
X : Type u
s₁ s₂ : Set X
inst : TopologicalSpace X
h₁ : IsOpen[inst] s₁
h₂ : IsOpen[inst] s₂
⊢ IsOpen[inst] (s₁ ∪ s₂)
have rw : IsOpen[inst] (⋃ (b : Bool), bif b then s₁ else s₂)
Tactic: rw [union_eq_iUnion]
-- Lean 4 proof step from Mathlib.Topology.Basic (goal)
Goal:
X : Type u
α : Type u_1
s : Set X
inst : TopologicalSpace X
f : α → Set X
ho : ∀ (i : α), IsOpen[inst] (f i)
hU : Eq.{u + 1} (α := Set X) (⋃ (i : α), f i) univ
⊢ IsOpen[inst] s ↔ ∀ (i : α), IsOpen[inst] (f i ∩ s)
have refine : ∀ (h : ∀ (i : α), IsOpen[inst] (f i ∩ s)), IsOpen[inst] s
Tactic: refine ⟨fun h i ↦ (ho i).inter h, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Basic (goal)
Goal:
X : Type u
α : Type u_1
s : Set X
inst : TopologicalSpace X
f : α → Set X
ho : ∀ (i : α), IsOpen[inst] (f i)
hU : Eq.{u + 1} (α := Set X) (⋃ (i : α), f i) univ
h : ∀ (i : α), IsOpen[inst] (f i ∩ s)
⊢ IsOpen[inst] s
have rw : IsOpen[inst] (⋃ (i : α), f i ∩ s)
Tactic: rw [← s.inter_univ, inter_comm, ← hU, iUnion_inter]
-- Lean 4 proof step from Mathlib.Topology.Basic (goal)
Goal:
X : Type u
inst : TopologicalSpace X
⊢ IsOpen[inst] ∅
have rw : IsOpen[inst] (⋃₀ ∅)
Tactic: rw [← sUnion_empty]
-- Lean 4 proof step from Mathlib.Topology.Basic (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set (Set X)
h : ∀ (t : Set X), Membership.mem (γ := Set (Set X)) ∅ t → IsOpen[inst] t
⊢ IsOpen[inst] (⋂₀ ∅)
have empty : IsOpen[inst] univ
Tactic: rw [sInter_empty]
-- Lean 4 proof step from Mathlib.Topology.Basic (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set (Set X)
a : Set X
s_1 : Set (Set X)
h_1 : a ∉ s_1
hs : s_1.Finite
ih : ∀ (h : ∀ t ∈ s_1, IsOpen[inst] t), IsOpen[inst] (⋂₀ s_1)
h : ∀ t ∈ insert a s_1, IsOpen[inst] t
⊢ IsOpen[inst] (⋂₀ insert a s_1)
have insert : ∀ (h : IsOpen[inst] a ∧ ∀ x ∈ s_1, IsOpen[inst] x), IsOpen[inst] (a ∩ ⋂₀ s_1)
Tactic: simp only [sInter_insert, forall_mem_insert] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Basic (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set (Set X)
hs : s.Finite
h : ∀ t ∈ s, IsOpen[inst] t
⊢ IsOpen[inst] (⋂₀ s)
have empty : ∀ (h : ∀ (t : Set X), Membership.mem (γ := Set (Set X)) ∅ t → IsOpen[inst] t), IsOpen[inst] (⋂₀ ∅)
Tactic: induction s, hs using Set.Finite.induction_on with
  | empty => rw [sInter_empty]; exact isOpen_univ
  | insert _ _ ih =>
    simp only [sInter_insert, forall_mem_insert] at h ⊢
    exact h.1.inter (ih h.2)
Cleared hypotheses: hs, h
-- Lean 4 proof step from Mathlib.Topology.Basic (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set (Set X)
hs : s.Finite
h : ∀ t ∈ s, IsOpen[inst] t
empty : ∀ (h : ∀ (t : Set X), Membership.mem (γ := Set (Set X)) ∅ t → IsOpen[inst] t), IsOpen[inst] (⋂₀ ∅)
⊢ IsOpen[inst] (⋂₀ s)
have insert : ∀ {a : Set X} {s : Set (Set X)},
  a ∉ s →
    s.Finite →
      ∀ (ih : ∀ (h : ∀ t ∈ s, IsOpen[inst] t), IsOpen[inst] (⋂₀ s)) (h : ∀ t ∈ insert a s, IsOpen[inst] t),
        IsOpen[inst] (⋂₀ insert a s)
Tactic: induction s, hs using Set.Finite.induction_on with
  | empty => rw [sInter_empty]; exact isOpen_univ
  | insert _ _ ih =>
    simp only [sInter_insert, forall_mem_insert] at h ⊢
    exact h.1.inter (ih h.2)
Cleared hypotheses: hs, h
-- Lean 4 proof step from Mathlib.Topology.Basic (goal)
Goal:
X : Type u
inst : TopologicalSpace X
p : Prop
⊢ IsOpen[inst] {_x : X | p}
have pos : p → IsOpen[inst] {_x : X | p}
Tactic: by_cases p
-- Lean 4 proof step from Mathlib.Topology.Basic (goal)
Goal:
X : Type u
inst : TopologicalSpace X
p : Prop
pos : p → IsOpen[inst] {_x : X | p}
⊢ IsOpen[inst] {_x : X | p}
have neg : ¬p → IsOpen[inst] {_x : X | p}
Tactic: by_cases p
-- Lean 4 proof step from Mathlib.Topology.Basic (goal)
Goal:
X : Type u_2
t₁ t₂ : TopologicalSpace X
⊢ t₁ = t₂ ↔ ∀ (s : Set X), IsClosed[t₁] s ↔ IsClosed[t₂] s
have rw : (∀ (x : Set X), IsOpen[t₁] xᶜ ↔ IsOpen[t₂] xᶜ) ↔ ∀ (s : Set X), IsClosed[t₁] s ↔ IsClosed[t₂] s
Tactic: rw [TopologicalSpace.ext_iff, compl_surjective.forall]
-- Lean 4 proof step from Mathlib.Topology.Basic (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ IsClosed[inst] sᶜ ↔ IsOpen[inst] s
have rw : IsOpen[inst] sᶜᶜ ↔ IsOpen[inst] s
Tactic: rw [← isOpen_compl_iff, compl_compl]
-- Lean 4 proof step from Mathlib.Topology.Basic (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
rw : IsOpen[inst] sᶜᶜ ↔ IsOpen[inst] s
⊢ IsClosed[inst] sᶜ ↔ IsOpen[inst] s
have rw₁ : IsOpen[inst] s ↔ IsOpen[inst] s
Tactic: rw [← isOpen_compl_iff, compl_compl]
-- Lean 4 proof step from Mathlib.Topology.Basic (goal)
Goal:
X : Type u
s₁ s₂ : Set X
inst : TopologicalSpace X
h₁ : IsClosed[inst] s₁
h₂ : IsClosed[inst] s₂
⊢ IsClosed[inst] (s₁ ∩ s₂)
have rw : ∀ (h₁ : IsOpen[inst] s₁ᶜ) (h₂ : IsOpen[inst] s₂ᶜ), IsOpen[inst] (s₁ ∩ s₂)ᶜ
Tactic: rw [← isOpen_compl_iff] at *
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Topology.Basic (goal)
Goal:
X : Type u
s₁ s₂ : Set X
inst : TopologicalSpace X
h₁ : IsOpen[inst] s₁ᶜ
h₂ : IsOpen[inst] s₂ᶜ
⊢ IsOpen[inst] (s₁ ∩ s₂)ᶜ
have rw : IsOpen[inst] (s₁ᶜ ∪ s₂ᶜ)
Tactic: rw [compl_inter]