awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
refine_1 :
  ∀ (t₁ : Set α),
    Membership.mem (γ := Set (Set α)) ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ s}) t₁ →
      ∀ (t₂ : Set α),
        Membership.mem (γ := Set (Set α)) ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ s}) t₂ →
          ∀ x ∈ t₁ ∩ t₂,
            ∃ (t₃ : Set α),
              Membership.mem (γ := Set (Set α)) ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ s})
                  t₃ ∧
                x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂
⊢ IsTopologicalBasis.{u} (α := α) ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ s})
have refine_2 : Eq.{u + 1} (α := Set α) (⋃₀ ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ s})) univ
Tactic: refine ⟨?_, ?_, le_antisymm (le_generateFrom ?_) <| generateFrom_anti fun t ht => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
refine_1 :
  ∀ (t₁ : Set α),
    Membership.mem (γ := Set (Set α)) ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ s}) t₁ →
      ∀ (t₂ : Set α),
        Membership.mem (γ := Set (Set α)) ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ s}) t₂ →
          ∀ x ∈ t₁ ∩ t₂,
            ∃ (t₃ : Set α),
              Membership.mem (γ := Set (Set α)) ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ s})
                  t₃ ∧
                x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂
refine_2 : Eq.{u + 1} (α := Set α) (⋃₀ ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ s})) univ
⊢ IsTopologicalBasis.{u} (α := α) ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ s})
have refine_3 : ∀ (s_1 : Set α),
  Membership.mem (γ := Set (Set α)) ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ s}) s_1 →
    IsOpen[generateFrom s] s_1
Tactic: refine ⟨?_, ?_, le_antisymm (le_generateFrom ?_) <| generateFrom_anti fun t ht => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
refine_1 :
  ∀ (t₁ : Set α),
    Membership.mem (γ := Set (Set α)) ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ s}) t₁ →
      ∀ (t₂ : Set α),
        Membership.mem (γ := Set (Set α)) ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ s}) t₂ →
          ∀ x ∈ t₁ ∩ t₂,
            ∃ (t₃ : Set α),
              Membership.mem (γ := Set (Set α)) ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ s})
                  t₃ ∧
                x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂
refine_2 : Eq.{u + 1} (α := Set α) (⋃₀ ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ s})) univ
refine_3 :
  ∀ (s_1 : Set α),
    Membership.mem (γ := Set (Set α)) ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ s}) s_1 →
      IsOpen[generateFrom s] s_1
⊢ IsTopologicalBasis.{u} (α := α) ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ s})
have refine_4 : ∀ (t : Set α) (ht : t ∈ s),
  Membership.mem (γ := Set (Set α)) ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ s}) t
Tactic: refine ⟨?_, ?_, le_antisymm (le_generateFrom ?_) <| generateFrom_anti fun t ht => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
⊢ Eq.{u + 1} (α := Set α) (⋃₀ ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ s})) univ
have refine_2 : ∀ (a : α),
  ∃ (i : Set (Set α)) (_ : Membership.mem (γ := Set (Set (Set α))) {f : Set (Set α) | f.Finite ∧ f ⊆ s} i), a ∈ ⋂₀ i
Tactic: rw [sUnion_image, iUnion₂_eq_univ_iff]
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
t : Set α
ht : t ∈ s
⊢ Membership.mem (γ := Set (Set α)) ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ s}) t
have refine_4 : Membership.mem (γ := Set (Set α)) ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ s}) (⋂₀ {t})
Tactic: rw [← sInter_singleton t]
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
s : Set (Set α)
hsg : t = generateFrom s
hsi : FiniteInter s
⊢ IsTopologicalBasis s
have h : s = (fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ s}
Tactic: convert! isTopologicalBasis_of_subbasis hsg
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
s : Set (Set α)
hsg : t = generateFrom s
hsi : FiniteInter s
⊢ s = (fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ s}
have h : (fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ s} ≤ s
Tactic: refine le_antisymm (fun t ht ↦ ⟨{t}, by simpa using ht⟩) ?_
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
s : Set (Set α)
hsg : t = generateFrom s
hsi : FiniteInter s
g : Set (Set α)
hg : g.Finite
hgs : g ⊆ s
⊢ (fun (f : Set (Set α)) ↦ ⋂₀ f) g ∈ s
have h : ∀ (g : Finset (Set α)) (hgs : (↑g : Set (Set α)) ⊆ s), (fun (f : Set (Set α)) ↦ ⋂₀ f) (↑g : Set (Set α)) ∈ s
Tactic: lift g to Finset (Set α) using hg
Cleared hypotheses: g, hg, hgs
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
a : α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
⊢ s ∈ (𝓝 a).sets ↔ ∃ t ∈ b, a ∈ t ∧ t ⊆ s
have rw : Membership.mem (γ := Set (Set α))
    (⋃ (i : Set α), ⋃ (_ : Membership.mem (γ := Set (Set α)) {s : Set α | a ∈ s ∧ s ∈ b} i), (𝓟 i).sets) s ↔
  ∃ t ∈ b, a ∈ t ∧ t ⊆ s
Tactic: rw [hb.eq_generateFrom, nhds_generateFrom, biInf_sets_eq]
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
a : α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
rw :
  Membership.mem (γ := Set (Set α))
      (⋃ (i : Set α), ⋃ (_ : Membership.mem (γ := Set (Set α)) {s : Set α | a ∈ s ∧ s ∈ b} i), (𝓟 i).sets) s ↔
    ∃ t ∈ b, a ∈ t ∧ t ⊆ s
⊢ s ∈ (𝓝 a).sets ↔ ∃ t ∈ b, a ∈ t ∧ t ⊆ s
have h : DirectedOn.{u} (α := Set α) (𝓟 ⁻¹'o fun (x1 x2 : Filter α) ↦ x1 ≥ x2) {s : Set α | a ∈ s ∧ s ∈ b}
Tactic: rw [hb.eq_generateFrom, nhds_generateFrom, biInf_sets_eq]
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
a : α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
rw :
  Membership.mem (γ := Set (Set α))
      (⋃ (i : Set α), ⋃ (_ : Membership.mem (γ := Set (Set α)) {s : Set α | a ∈ s ∧ s ∈ b} i), (𝓟 i).sets) s ↔
    ∃ t ∈ b, a ∈ t ∧ t ⊆ s
h : DirectedOn.{u} (α := Set α) (𝓟 ⁻¹'o fun (x1 x2 : Filter α) ↦ x1 ≥ x2) {s : Set α | a ∈ s ∧ s ∈ b}
⊢ s ∈ (𝓝 a).sets ↔ ∃ t ∈ b, a ∈ t ∧ t ⊆ s
have ne : Set.Nonempty.{u} (α := Set α) {s : Set α | a ∈ s ∧ s ∈ b}
Tactic: rw [hb.eq_generateFrom, nhds_generateFrom, biInf_sets_eq]
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t_1 : TopologicalSpace α
a : α
s_1 : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
s : Set α
hs₁ : a ∈ s
hs₂ : s ∈ b
t : Set α
ht₁ : a ∈ t
ht₂ : t ∈ b
⊢ ∃ (z : Set α),
    Membership.mem (γ := Set (Set α)) {s : Set α | a ∈ s ∧ s ∈ b} z ∧
      (𝓟 ⁻¹'o fun (x1 x2 : Filter α) ↦ x1 ≥ x2) s z ∧ (𝓟 ⁻¹'o fun (x1 x2 : Filter α) ↦ x1 ≥ x2) t z
have h : ∀ (u : Set α) (hu₁ : u ∈ b) (hu₂ : a ∈ u) (hu₃ : u ⊆ s ∩ t),
  ∃ (z : Set α),
    Membership.mem (γ := Set (Set α)) {s : Set α | a ∈ s ∧ s ∈ b} z ∧
      (𝓟 ⁻¹'o fun (x1 x2 : Filter α) ↦ x1 ≥ x2) s z ∧ (𝓟 ⁻¹'o fun (x1 x2 : Filter α) ↦ x1 ≥ x2) t z
Tactic: let ⟨u, hu₁, hu₂, hu₃⟩ := hb.1 _ hs₂ _ ht₂ _ ⟨hs₁, ht₁⟩
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
a : α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
⊢ Set.Nonempty.{u} (α := Set α) {s : Set α | a ∈ s ∧ s ∈ b}
have ne : ∀ (i : Set α) (h1 : i ∈ b) (h2 : a ∈ i), Set.Nonempty.{u} (α := Set α) {s : Set α | a ∈ s ∧ s ∈ b}
Tactic: rcases eq_univ_iff_forall.1 hb.sUnion_eq a with ⟨i, h1, h2⟩
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
hs : s ∈ b
⊢ IsOpen[t] s
have rw : IsOpen[generateFrom b] s
Tactic: rw [hb.eq_generateFrom]
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
B B' : Set (Set α)
hB : IsTopologicalBasis B
h_open : ∀ u ∈ B', IsOpen[t] u
h : ∀ u ∈ B, ∀ x ∈ u, ∃ v ∈ B', x ∈ v ∧ v ⊆ u
⊢ IsTopologicalBasis B'
have refine : ∀ (x : α) (u : Set α) (hx : x ∈ u) (hu : IsOpen[t] u), ∃ v ∈ B', x ∈ v ∧ v ⊆ u
Tactic: refine isTopologicalBasis_of_isOpen_of_nhds h_open fun x u hx hu => ?_
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
B B' : Set (Set α)
hB : IsTopologicalBasis B
h_open : ∀ u ∈ B', IsOpen[t] u
h : ∀ u ∈ B, ∀ x ∈ u, ∃ v ∈ B', x ∈ v ∧ v ⊆ u
x : α
u : Set α
hx : x ∈ u
hu : IsOpen[t] u
⊢ ∃ v ∈ B', x ∈ v ∧ v ⊆ u
have obtain : ∀ (w : Set α) (hwB : w ∈ B) (hxw : x ∈ w) (hwu : w ⊆ u), ∃ v ∈ B', x ∈ v ∧ v ⊆ u
Tactic: obtain ⟨w, hwB, hxw, hwu⟩ := hB.exists_subset_of_mem_open hx hu
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
B B' : Set (Set α)
hB : IsTopologicalBasis B
h_open : ∀ u ∈ B', IsOpen[t] u
h : ∀ u ∈ B, ∀ x ∈ u, ∃ v ∈ B', x ∈ v ∧ v ⊆ u
x : α
u : Set α
hx : x ∈ u
hu : IsOpen[t] u
w : Set α
hwB : w ∈ B
hxw : x ∈ w
hwu : w ⊆ u
⊢ ∃ v ∈ B', x ∈ v ∧ v ⊆ u
have obtain : ∀ (v : Set α) (hvB' : v ∈ B') (hxv : x ∈ v) (hvw : v ⊆ w), ∃ v ∈ B', x ∈ v ∧ v ⊆ u
Tactic: obtain ⟨v, hvB', hxv, hvw⟩ := h w hwB x hxw
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set α
ou : IsOpen[t] u
⊢ u = ⋃ (i : (↑{s : Set α | s ∈ B ∧ s ⊆ u} : Type u)), (↑i : Set α)
have rw : u = ⋃₀ {s : Set α | s ∈ B ∧ s ⊆ u}
Tactic: rw [← sUnion_eq_iUnion]
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
B : Set (Set α)
P : Set α → Prop
hB : IsTopologicalBasis B
basis : ∀ b ∈ B, P b
sUnion : ∀ (S : Set (Set α)), (∀ s ∈ S, P s) → P (⋃₀ S)
s : Set α
hs : IsOpen[t] s
⊢ P s
have obtain : ∀ (S : Set (Set α)) (hS : S ⊆ B) (hs : IsOpen[t] (⋃₀ S)), P (⋃₀ S)
Tactic: obtain ⟨S, hS, rfl⟩ := hB.open_eq_sUnion hs
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t_1 : TopologicalSpace α
B : Set (Set α)
s t : Set α
hB : IsTopologicalBasis B
hs : IsOpen[t_1] s
h : ∀ U ∈ B, U ⊆ s → U ⊆ t
⊢ s ⊆ t
have rw : ⋃₀ {s_1 : Set α | s_1 ∈ B ∧ s_1 ⊆ s} ⊆ t
Tactic: rw [hB.open_eq_sUnion' hs]
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t_1 : TopologicalSpace α
B : Set (Set α)
s t : Set α
hB : IsTopologicalBasis B
hs : IsOpen[t_1] s
ht : IsOpen[t_1] t
h : ∀ U ∈ B, U ⊆ s ↔ U ⊆ t
⊢ s = t
have rw : Eq.{u + 1} (α := Set α) (⋃₀ {s_1 : Set α | s_1 ∈ B ∧ s_1 ⊆ s}) (⋃₀ {s : Set α | s ∈ B ∧ s ⊆ t})
Tactic: rw [hB.open_eq_sUnion' hs, hB.open_eq_sUnion' ht]
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
b : Set (Set α)
hb : IsTopologicalBasis b
s : Set α
⊢ Dense s ↔ ∀ o ∈ b, o.Nonempty → (o ∩ s).Nonempty
have simp : (∀ (x : α), ∀ o ∈ b, x ∈ o → (o ∩ s).Nonempty) ↔ ∀ o ∈ b, o.Nonempty → (o ∩ s).Nonempty
Tactic: simp only [Dense, hb.mem_closure_iff]
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
inst : TopologicalSpace β
B : Set (Set α)
hB : IsTopologicalBasis B
f : α → β
⊢ IsOpenMap f ↔ ∀ s ∈ B, IsOpen[inst] (f '' s)
have refine : ∀ (hf : ∀ s ∈ B, IsOpen[inst] (f '' s)) (o : Set α) (ho : IsOpen[t] o), IsOpen[inst] (f '' o)
Tactic: refine ⟨fun H o ho => H _ (hB.isOpen ho), fun hf o ho => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
inst : TopologicalSpace β
B : Set (Set α)
hB : IsTopologicalBasis B
f : α → β
hf : ∀ s ∈ B, IsOpen[inst] (f '' s)
o : Set α
ho : IsOpen[t] o
⊢ IsOpen[inst] (f '' o)
have rw : IsOpen[inst] (⋃ (i : (↑{s : Set α | s ∈ B ∧ s ⊆ o} : Type u)), f '' (↑i : Set α))
Tactic: rw [hB.open_eq_sUnion' ho, sUnion_eq_iUnion, image_iUnion]
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ tauto₈ tauto₉ tauto₁₀ :
  ∀ (a : α) (u : Set α),
    a ∈ u → IsOpen[t] u → ∃ (v : Set α), Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[t] U} v ∧ a ∈ v ∧ v ⊆ u
⊢ ∀ (a : α) (u : Set α),
    a ∈ u → IsOpen[t] u → ∃ (v : Set α), Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[t] U} v ∧ a ∈ v ∧ v ⊆ u
have h : ∀ (a : α) (u : Set α),
  a ∈ u → IsOpen[t] u → Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[t] U} u ∧ a ∈ u ∧ u ⊆ u
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ tauto₈ tauto₉ tauto₁₀ :
  ∀ (a : α) (u : Set α),
    a ∈ u → IsOpen[t] u → ∃ (v : Set α), Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[t] U} v ∧ a ∈ v ∧ v ⊆ u
h :
  ∀ (a : α) (u : Set α),
    a ∈ u → IsOpen[t] u → Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[t] U} u ∧ a ∈ u ∧ u ⊆ u
⊢ ∀ (a : α) (u : Set α),
    a ∈ u → IsOpen[t] u → ∃ (v : Set α), Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[t] U} v ∧ a ∈ v ∧ v ⊆ u
have w : (a : α) → (u : Set α) → a ∈ u → IsOpen[t] u → Set α
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ tauto₈ tauto₉ tauto₁₀ :
  ∀ (a : α) (u : Set α),
    a ∈ u → IsOpen[t] u → ∃ (v : Set α), Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[t] U} v ∧ a ∈ v ∧ v ⊆ u
h :
  ∀ (a : α) (u : Set α),
    a ∈ u → IsOpen[t] u → Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[t] U} u ∧ a ∈ u ∧ u ⊆ u
w : (a : α) → (u : Set α) → a ∈ u → IsOpen[t] u → Set α
h₁ :
  ∀ (a : α) (u : Set α),
    a ∈ u → IsOpen[t] u → Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[t] U} u ∧ a ∈ u ∧ u ⊆ u
w₁ : (a : α) → (u : Set α) → a ∈ u → IsOpen[t] u → Set α
⊢ ∀ (a : α) (u : Set α),
    a ∈ u → IsOpen[t] u → ∃ (v : Set α), Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[t] U} v ∧ a ∈ v ∧ v ⊆ u
have h₂ : ∀ (a : α) (u : Set α), a ∈ u → IsOpen[t] u → Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[t] U} u
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ tauto₈ tauto₉ tauto₁₀ :
  ∀ (a : α) (u : Set α),
    a ∈ u → IsOpen[t] u → ∃ (v : Set α), Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[t] U} v ∧ a ∈ v ∧ v ⊆ u
h :
  ∀ (a : α) (u : Set α),
    a ∈ u → IsOpen[t] u → Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[t] U} u ∧ a ∈ u ∧ u ⊆ u
w : (a : α) → (u : Set α) → a ∈ u → IsOpen[t] u → Set α
h₁ :
  ∀ (a : α) (u : Set α),
    a ∈ u → IsOpen[t] u → Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[t] U} u ∧ a ∈ u ∧ u ⊆ u
w₁ : (a : α) → (u : Set α) → a ∈ u → IsOpen[t] u → Set α
h₂ : ∀ (a : α) (u : Set α), a ∈ u → IsOpen[t] u → Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[t] U} u
⊢ ∀ (a : α) (u : Set α),
    a ∈ u → IsOpen[t] u → ∃ (v : Set α), Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[t] U} v ∧ a ∈ v ∧ v ⊆ u
have h₃ : ∀ (a : α) (u : Set α), a ∈ u → IsOpen[t] u → a ∈ u ∧ u ⊆ u
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
inst : TopologicalSpace β
f : α → β
T : Set (Set β)
hf : IsInducing f
h : IsTopologicalBasis T
a : α
⊢ (𝓝 a).HasBasis (fun (t : Set α) ↦ t ∈ preimage f '' T ∧ a ∈ t) id
have h₁ : ∀ (s : Set α),
  s ∈ preimage f '' T ∧ a ∈ s ↔ s ∈ image (α := Set β) (preimage f ∘ fun (t : Set β) ↦ t) {i : Set β | i ∈ T ∧ f a ∈ i}
Tactic: convert! (hf.basis_nhds (h.nhds_hasBasis (a := f a))).to_image_id with s
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
β : Type u_1
t₁ t₂ : TopologicalSpace β
B₁ B₂ : Set (Set β)
h₁ : IsTopologicalBasis B₁
h₂ : IsTopologicalBasis B₂
⊢ IsTopologicalBasis (α := β) (image2 (fun (x1 x2 : Set β) ↦ x1 ∩ x2) B₁ B₂)
have refine : ∀ (a : β),
  (𝓝 a).HasBasis
    (fun (t : Set β) ↦ Membership.mem (γ := Set (Set β)) (image2 (fun (x1 x2 : Set β) ↦ x1 ∩ x2) B₁ B₂) t ∧ a ∈ t) id
Tactic: refine .of_hasBasis_nhds (t := ?_) fun a ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
β : Type u_1
t₁ t₂ : TopologicalSpace β
B₁ B₂ : Set (Set β)
h₁ : IsTopologicalBasis B₁
h₂ : IsTopologicalBasis B₂
a : β
⊢ (𝓝 a).HasBasis
    (fun (t : Set β) ↦ Membership.mem (γ := Set (Set β)) (image2 (fun (x1 x2 : Set β) ↦ x1 ∩ x2) B₁ B₂) t ∧ a ∈ t) id
have rw : (𝓝 a ⊓ 𝓝 a).HasBasis
  (fun (t : Set β) ↦ Membership.mem (γ := Set (Set β)) (image2 (fun (x1 x2 : Set β) ↦ x1 ∩ x2) B₁ B₂) t ∧ a ∈ t) id
Tactic: rw [nhds_inf (t₁ := t₁)]
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
β : Type u_1
t₁ t₂ : TopologicalSpace β
B₁ B₂ : Set (Set β)
h₁ : IsTopologicalBasis B₁
h₂ : IsTopologicalBasis B₂
a : β
⊢ (𝓝 a ⊓ 𝓝 a).HasBasis
    (fun (t : Set β) ↦ Membership.mem (γ := Set (Set β)) (image2 (fun (x1 x2 : Set β) ↦ x1 ∩ x2) B₁ B₂) t ∧ a ∈ t) id
have h : ∀ (x : Set β),
  Membership.mem (γ := Set (Set β)) (image2 (fun (x1 x2 : Set β) ↦ x1 ∩ x2) B₁ B₂) x ∧ a ∈ x ↔
    Membership.mem (γ := Set (Set β))
      ((fun (i : Set β × Set β) ↦ i.1 ∩ i.2) '' {i : Set β × Set β | (i.1 ∈ B₁ ∧ a ∈ i.1) ∧ i.2 ∈ B₂ ∧ a ∈ i.2}) x
Tactic: convert! ((h₁.nhds_hasBasis (t := t₁)).inf (h₂.nhds_hasBasis (t := t₂))).to_image_id
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
ι : Sort u_2
U : ι → Set α
Uo : ∀ (i : ι), IsOpen[t] (U i)
Uc : Eq.{u + 1} (α := Set α) (⋃ (i : ι), U i) univ
b : (i : ι) → Set (Set (↑(U i) : Type u))
hb : ∀ (i : ι), IsTopologicalBasis (b i)
⊢ IsTopologicalBasis.{u} (α := α) (⋃ (i : ι), image (Subtype.val (p := fun (x : α) ↦ x ∈ U i)) '' b i)
have refine_1 : ∀ (u : Set α)
  (hu : Membership.mem (γ := Set (Set α)) (⋃ (i : ι), image (Subtype.val (p := fun (x : α) ↦ x ∈ U i)) '' b i) u),
  IsOpen[t] u
Tactic: refine isTopologicalBasis_of_isOpen_of_nhds (fun u hu => ?_) ?_
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
ι : Sort u_2
U : ι → Set α
Uo : ∀ (i : ι), IsOpen[t] (U i)
Uc : Eq.{u + 1} (α := Set α) (⋃ (i : ι), U i) univ
b : (i : ι) → Set (Set (↑(U i) : Type u))
hb : ∀ (i : ι), IsTopologicalBasis (b i)
refine_1 :
  ∀ (u : Set α)
    (hu : Membership.mem (γ := Set (Set α)) (⋃ (i : ι), image (Subtype.val (p := fun (x : α) ↦ x ∈ U i)) '' b i) u),
    IsOpen[t] u
⊢ IsTopologicalBasis.{u} (α := α) (⋃ (i : ι), image (Subtype.val (p := fun (x : α) ↦ x ∈ U i)) '' b i)
have refine_2 : ∀ (a : α) (u : Set α),
  a ∈ u →
    IsOpen[t] u →
      ∃ (v : Set α),
        Membership.mem (γ := Set (Set α)) (⋃ (i : ι), image (Subtype.val (p := fun (x : α) ↦ x ∈ U i)) '' b i) v ∧
          a ∈ v ∧ v ⊆ u
Tactic: refine isTopologicalBasis_of_isOpen_of_nhds (fun u hu => ?_) ?_
-- Lean 4 proof step from Mathlib.Topology.Bases (hypothesis)
Goal:
α : Type u
t : TopologicalSpace α
ι : Sort u_2
U : ι → Set α
Uo : ∀ (i : ι), IsOpen[t] (U i)
Uc : Eq.{u + 1} (α := Set α) (⋃ (i : ι), U i) univ
b : (i : ι) → Set (Set (↑(U i) : Type u))
hb : ∀ (i : ι), IsTopologicalBasis (b i)
u : Set α
hu : Membership.mem (γ := Set (Set α)) (⋃ (i : ι), image (Subtype.val (p := fun (x : α) ↦ x ∈ U i)) '' b i) u
⊢ IsOpen[t] u
have hu₁ : ∃ (i : ι), ∃ x ∈ b i, Subtype.val (p := fun (x : α) ↦ x ∈ U i) '' x = u
Tactic: simp only [mem_iUnion, mem_image] at hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
ι : Sort u_2
U : ι → Set α
Uo : ∀ (i : ι), IsOpen[t] (U i)
Uc : Eq.{u + 1} (α := Set α) (⋃ (i : ι), U i) univ
b : (i : ι) → Set (Set (↑(U i) : Type u))
hb : ∀ (i : ι), IsTopologicalBasis (b i)
u : Set α
hu : ∃ (i : ι), ∃ x ∈ b i, Subtype.val (p := fun (x : α) ↦ x ∈ U i) '' x = u
⊢ IsOpen[t] u
have refine_1 : ∀ (i : ι) (s : Set { x : α // x ∈ U i }) (sb : s ∈ b i), IsOpen[t] (Subtype.val (p := fun (x : α) ↦ x ∈ U i) '' s)
Tactic: rcases hu with ⟨i, s, sb, rfl⟩
Cleared hypotheses: u, hu
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
ι : Sort u_2
U : ι → Set α
Uo : ∀ (i : ι), IsOpen[t] (U i)
Uc : Eq.{u + 1} (α := Set α) (⋃ (i : ι), U i) univ
b : (i : ι) → Set (Set (↑(U i) : Type u))
hb : ∀ (i : ι), IsTopologicalBasis (b i)
a : α
u : Set α
ha : a ∈ u
uo : IsOpen[t] u
⊢ ∃ (v : Set α),
    Membership.mem (γ := Set (Set α)) (⋃ (i : ι), image (Subtype.val (p := fun (x : α) ↦ x ∈ U i)) '' b i) v ∧
      a ∈ v ∧ v ⊆ u
have refine_2 : ∀ (i : ι) (hi : a ∈ U i),
  ∃ (v : Set α),
    Membership.mem (γ := Set (Set α)) (⋃ (i : ι), image (Subtype.val (p := fun (x : α) ↦ x ∈ U i)) '' b i) v ∧
      a ∈ v ∧ v ⊆ u
Tactic: rcases iUnion_eq_univ_iff.1 Uc a with ⟨i, hi⟩
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
ι : Sort u_2
U : ι → Set α
Uo : ∀ (i : ι), IsOpen[t] (U i)
Uc : Eq.{u + 1} (α := Set α) (⋃ (i : ι), U i) univ
b : (i : ι) → Set (Set (↑(U i) : Type u))
hb : ∀ (i : ι), IsTopologicalBasis (b i)
a : α
u : Set α
ha : a ∈ u
uo : IsOpen[t] u
i : ι
hi : a ∈ U i
⊢ ∃ (v : Set α),
    Membership.mem (γ := Set (Set α)) (⋃ (i : ι), image (Subtype.val (p := fun (x : α) ↦ x ∈ U i)) '' b i) v ∧
      a ∈ v ∧ v ⊆ u
have refine_2 : ∀ (a : { x : α // x ∈ U i }) (ha : (↑a : α) ∈ u),
  ∃ (v : Set α),
    Membership.mem (γ := Set (Set α)) (⋃ (i : ι), image (Subtype.val (p := fun (x : α) ↦ x ∈ U i)) '' b i) v ∧
      (↑a : α) ∈ v ∧ v ⊆ u
Tactic: lift a to ↥(U i) using hi
Cleared hypotheses: a, ha, hi
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
ι : Sort u_2
U : ι → Set α
Uo : ∀ (i : ι), IsOpen[t] (U i)
Uc : Eq.{u + 1} (α := Set α) (⋃ (i : ι), U i) univ
b : (i : ι) → Set (Set (↑(U i) : Type u))
hb : ∀ (i : ι), IsTopologicalBasis (b i)
u : Set α
uo : IsOpen[t] u
i : ι
a : { x : α // x ∈ U i }
ha : (↑a : α) ∈ u
⊢ ∃ (v : Set α),
    Membership.mem (γ := Set (Set α)) (⋃ (i : ι), image (Subtype.val (p := fun (x : α) ↦ x ∈ U i)) '' b i) v ∧
      (↑a : α) ∈ v ∧ v ⊆ u
have refine_2 : ∀ (v : Set (↑(U i) : Type u)) (hvb : v ∈ b i) (hav : a ∈ v) (hvu : v ⊆ Subtype.val (p := fun (x : α) ↦ x ∈ U i) ⁻¹' u),
  ∃ (v : Set α),
    Membership.mem (γ := Set (Set α)) (⋃ (i : ι), image (Subtype.val (p := fun (x : α) ↦ x ∈ U i)) '' b i) v ∧
      (↑a : α) ∈ v ∧ v ⊆ u
Tactic: rcases (hb i).exists_subset_of_mem_open ha (uo.preimage continuous_subtype_val) with
      ⟨v, hvb, hav, hvu⟩
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
inst : TopologicalSpace β
B : Set (Set β)
hB : IsTopologicalBasis B
f : α → β
⊢ Continuous[t, inst] f ↔ ∀ s ∈ B, IsOpen[t] (f ⁻¹' s)
have rw : Continuous[t, generateFrom B] f ↔ ∀ s ∈ B, IsOpen[t] (f ⁻¹' s)
Tactic: rw [hB.eq_generateFrom, continuous_generateFrom_iff]
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
inst : TopologicalSpace β
B : Set (Set β)
hB : IsTopologicalBasis B
f : α → β
rw : Continuous[t, generateFrom B] f ↔ ∀ s ∈ B, IsOpen[t] (f ⁻¹' s)
⊢ Continuous[t, inst] f ↔ ∀ s ∈ B, IsOpen[t] (f ⁻¹' s)
have rw₁ : (∀ s ∈ B, IsOpen[t] (f ⁻¹' s)) ↔ ∀ s ∈ B, IsOpen[t] (f ⁻¹' s)
Tactic: rw [hB.eq_generateFrom, continuous_generateFrom_iff]
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
s : Set α
inst : TopologicalSpace β
B : Set (Set β)
hB : IsTopologicalBasis B
f : α → β
⊢ ContinuousOn f s ↔ ∀ t_1 ∈ B, ∃ (u : Set α), IsOpen[t] u ∧ f ⁻¹' t_1 ∩ s = u ∩ s
have rw : (∀ (t_1 : Set β), IsOpen[inst] t_1 → ∃ (u : Set α), IsOpen[t] u ∧ f ⁻¹' t_1 ∩ s = u ∩ s) ↔
  ∀ t_1 ∈ B, ∃ (u : Set α), IsOpen[t] u ∧ f ⁻¹' t_1 ∩ s = u ∩ s
Tactic: rw [continuousOn_iff']