awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Separation.SeparatedNhds (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
u : ℕ → Set X
u_cov : s ⊆ ⋃ (n : ℕ), u n
u_props : ∀ (n : ℕ), IsOpen[inst] (u n) ∧ Disjoint (closure[inst] (u n)) t
v : ℕ → Set X
v_cov : t ⊆ ⋃ (n : ℕ), v n
v_props : ∀ (n : ℕ), IsOpen[inst] (v n) ∧ Disjoint (closure[inst] (v n)) s
⊢ SeparatedNhds s t
have open_lemma : ∀ (u₀ a : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst] (u₀ n)) → IsOpen[inst] (⋃ (n : ℕ), u₀ n \ closure[inst] (a n))
Tactic: have open_lemma : ∀ (u₀ a : ℕ → Set X), (∀ n, IsOpen (u₀ n)) →
      IsOpen (⋃ n, u₀ n \ closure (a n)) := fun _ _ u₀i_open ↦
        isOpen_iUnion fun i ↦ (u₀i_open i).sdiff isClosed_closure
-- Lean 4 proof step from Mathlib.Topology.Separation.SeparatedNhds (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
u : ℕ → Set X
u_cov : s ⊆ ⋃ (n : ℕ), u n
u_props : ∀ (n : ℕ), IsOpen[inst] (u n) ∧ Disjoint (closure[inst] (u n)) t
v : ℕ → Set X
v_cov : t ⊆ ⋃ (n : ℕ), v n
v_props : ∀ (n : ℕ), IsOpen[inst] (v n) ∧ Disjoint (closure[inst] (v n)) s
open_lemma :
  ∀ (u₀ a : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst] (u₀ n)) → IsOpen[inst] (⋃ (n : ℕ), u₀ n \ closure[inst] (a n))
h₀ : Set X
u₀ v₀ : ℕ → Set X
h₀_cov : h₀ ⊆ ⋃ (n : ℕ), u₀ n
dis : ∀ (n : ℕ), Disjoint (closure[inst] (v₀ n)) h₀
x : X
xinh : x ∈ h₀
⊢ Membership.mem (γ := Set X) (⋃ (n : ℕ), u₀ n \ closure[inst] (⋃ (m : ℕ), ⋃ (_ : m ≤ n), v₀ m)) x
have rcases : ∀ (n : ℕ) (xinun : Membership.mem (γ := Set X) ((fun (n : ℕ) ↦ u₀ n) n) x),
  Membership.mem (γ := Set X) (⋃ (n : ℕ), u₀ n \ closure[inst] (⋃ (m : ℕ), ⋃ (_ : m ≤ n), v₀ m)) x
Tactic: rcases h₀_cov xinh with ⟨un, ⟨n, rfl⟩, xinun⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.SeparatedNhds (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
u : ℕ → Set X
u_cov : s ⊆ ⋃ (n : ℕ), u n
u_props : ∀ (n : ℕ), IsOpen[inst] (u n) ∧ Disjoint (closure[inst] (u n)) t
v : ℕ → Set X
v_cov : t ⊆ ⋃ (n : ℕ), v n
v_props : ∀ (n : ℕ), IsOpen[inst] (v n) ∧ Disjoint (closure[inst] (v n)) s
open_lemma :
  ∀ (u₀ a : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst] (u₀ n)) → IsOpen[inst] (⋃ (n : ℕ), u₀ n \ closure[inst] (a n))
h₀ : Set X
u₀ v₀ : ℕ → Set X
h₀_cov : h₀ ⊆ ⋃ (n : ℕ), u₀ n
dis : ∀ (n : ℕ), Disjoint (closure[inst] (v₀ n)) h₀
x : X
xinh : x ∈ h₀
n : ℕ
xinun : Membership.mem (γ := Set X) ((fun (n : ℕ) ↦ u₀ n) n) x
⊢ Membership.mem (γ := Set X) (⋃ (n : ℕ), u₀ n \ closure[inst] (⋃ (m : ℕ), ⋃ (_ : m ≤ n), v₀ m)) x
have simp : ∃ (i : ℕ), x ∈ u₀ i \ closure[inst] (⋃ (m : ℕ), ⋃ (_ : m ≤ i), v₀ m)
Tactic: simp only [mem_iUnion]
-- Lean 4 proof step from Mathlib.Topology.Separation.SeparatedNhds (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
u : ℕ → Set X
u_cov : s ⊆ ⋃ (n : ℕ), u n
u_props : ∀ (n : ℕ), IsOpen[inst] (u n) ∧ Disjoint (closure[inst] (u n)) t
v : ℕ → Set X
v_cov : t ⊆ ⋃ (n : ℕ), v n
v_props : ∀ (n : ℕ), IsOpen[inst] (v n) ∧ Disjoint (closure[inst] (v n)) s
open_lemma :
  ∀ (u₀ a : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst] (u₀ n)) → IsOpen[inst] (⋃ (n : ℕ), u₀ n \ closure[inst] (a n))
h₀ : Set X
u₀ v₀ : ℕ → Set X
h₀_cov : h₀ ⊆ ⋃ (n : ℕ), u₀ n
dis : ∀ (n : ℕ), Disjoint (closure[inst] (v₀ n)) h₀
x : X
xinh : x ∈ h₀
n : ℕ
xinun : Membership.mem (γ := Set X) ((fun (n : ℕ) ↦ u₀ n) n) x
⊢ ∃ (i : ℕ), x ∈ u₀ i \ closure[inst] (⋃ (m : ℕ), ⋃ (_ : m ≤ i), v₀ m)
have refine : x ∉ closure[inst] (⋃ (m : ℕ), ⋃ (_ : m ≤ n), v₀ m)
Tactic: refine ⟨n, xinun, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.SeparatedNhds (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
u : ℕ → Set X
u_cov : s ⊆ ⋃ (n : ℕ), u n
u_props : ∀ (n : ℕ), IsOpen[inst] (u n) ∧ Disjoint (closure[inst] (u n)) t
v : ℕ → Set X
v_cov : t ⊆ ⋃ (n : ℕ), v n
v_props : ∀ (n : ℕ), IsOpen[inst] (v n) ∧ Disjoint (closure[inst] (v n)) s
open_lemma :
  ∀ (u₀ a : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst] (u₀ n)) → IsOpen[inst] (⋃ (n : ℕ), u₀ n \ closure[inst] (a n))
⊢ SeparatedNhds s t
have cover_lemma : ∀ (h₀ : Set X) (u₀ v₀ : ℕ → Set X),
  h₀ ⊆ ⋃ (n : ℕ), u₀ n →
    (∀ (n : ℕ), Disjoint (closure[inst] (v₀ n)) h₀) →
      h₀ ⊆ ⋃ (n : ℕ), u₀ n \ closure[inst] (⋃ (m : ℕ), ⋃ (_ : m ≤ n), v₀ m)
Tactic: have cover_lemma : ∀ (h₀ : Set X) (u₀ v₀ : ℕ → Set X),
        (h₀ ⊆ ⋃ n, u₀ n) → (∀ n, Disjoint (closure (v₀ n)) h₀) →
        (h₀ ⊆ ⋃ n, u₀ n \ closure (⋃ m ≤ n, v₀ m)) :=
        fun h₀ u₀ v₀ h₀_cov dis x xinh ↦ by
      rcases h₀_cov xinh with ⟨un, ⟨n, rfl⟩, xinun⟩
      simp only [mem_iUnion]
      refine ⟨n, xinun, ?_⟩
      simp_all only [closure_iUnion₂_le_nat, disjoint_right, mem_iUnion,
        exists_false, not_false_eq_true]
-- Lean 4 proof step from Mathlib.Topology.Separation.SeparatedNhds (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
u : ℕ → Set X
u_cov : s ⊆ ⋃ (n : ℕ), u n
u_props : ∀ (n : ℕ), IsOpen[inst] (u n) ∧ Disjoint (closure[inst] (u n)) t
v : ℕ → Set X
v_cov : t ⊆ ⋃ (n : ℕ), v n
v_props : ∀ (n : ℕ), IsOpen[inst] (v n) ∧ Disjoint (closure[inst] (v n)) s
open_lemma :
  ∀ (u₀ a : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst] (u₀ n)) → IsOpen[inst] (⋃ (n : ℕ), u₀ n \ closure[inst] (a n))
cover_lemma :
  ∀ (h₀ : Set X) (u₀ v₀ : ℕ → Set X),
    h₀ ⊆ ⋃ (n : ℕ), u₀ n →
      (∀ (n : ℕ), Disjoint (closure[inst] (v₀ n)) h₀) →
        h₀ ⊆ ⋃ (n : ℕ), u₀ n \ closure[inst] (⋃ (m : ℕ), ⋃ (_ : m ≤ n), v₀ m)
⊢ SeparatedNhds s t
have mp : Disjoint.{u_1} (α := Set X) (⋃ (n : ℕ), u n \ closure[inst] (⋃ (m : ℕ), ⋃ (_ : m ≤ n), v m))
  (⋃ (n : ℕ), v n \ closure[inst] (⋃ (m : ℕ), ⋃ (_ : m ≤ n), u m))
Tactic: refine
      ⟨⋃ n : ℕ, u n \ (closure (⋃ m ≤ n, v m)),
       ⋃ n : ℕ, v n \ (closure (⋃ m ≤ n, u m)),
       open_lemma u (fun n ↦ ⋃ m ≤ n, v m) (fun n ↦ (u_props n).1),
       open_lemma v (fun n ↦ ⋃ m ≤ n, u m) (fun n ↦ (v_props n).1),
       cover_lemma s u v u_cov (fun n ↦ (v_props n).2),
       cover_lemma t v u v_cov (fun n ↦ (u_props n).2),
       ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.SeparatedNhds (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
u : ℕ → Set X
u_cov : s ⊆ ⋃ (n : ℕ), u n
u_props : ∀ (n : ℕ), IsOpen[inst] (u n) ∧ Disjoint (closure[inst] (u n)) t
v : ℕ → Set X
v_cov : t ⊆ ⋃ (n : ℕ), v n
v_props : ∀ (n : ℕ), IsOpen[inst] (v n) ∧ Disjoint (closure[inst] (v n)) s
open_lemma :
  ∀ (u₀ a : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst] (u₀ n)) → IsOpen[inst] (⋃ (n : ℕ), u₀ n \ closure[inst] (a n))
cover_lemma :
  ∀ (h₀ : Set X) (u₀ v₀ : ℕ → Set X),
    h₀ ⊆ ⋃ (n : ℕ), u₀ n →
      (∀ (n : ℕ), Disjoint (closure[inst] (v₀ n)) h₀) →
        h₀ ⊆ ⋃ (n : ℕ), u₀ n \ closure[inst] (⋃ (m : ℕ), ⋃ (_ : m ≤ n), v₀ m)
⊢ Disjoint.{u_1} (α := Set X) (⋃ (n : ℕ), u n \ closure[inst] (⋃ (m : ℕ), ⋃ (_ : m ≤ n), v m))
    (⋃ (n : ℕ), v n \ closure[inst] (⋃ (m : ℕ), ⋃ (_ : m ≤ n), u m))
have mp : ∀ ⦃a : X⦄,
  Membership.mem (γ := Set X) (⋃ (n : ℕ), u n \ closure[inst] (⋃ (m : ℕ), ⋃ (_ : m ≤ n), v m)) a →
    a ∉ ⋃ (n : ℕ), v n \ closure[inst] (⋃ (m : ℕ), ⋃ (_ : m ≤ n), u m)
Tactic: rw [Set.disjoint_left]
-- Lean 4 proof step from Mathlib.Topology.Separation.SeparatedNhds (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
u : ℕ → Set X
u_cov : s ⊆ ⋃ (n : ℕ), u n
u_props : ∀ (n : ℕ), IsOpen[inst] (u n) ∧ Disjoint (closure[inst] (u n)) t
v : ℕ → Set X
v_cov : t ⊆ ⋃ (n : ℕ), v n
v_props : ∀ (n : ℕ), IsOpen[inst] (v n) ∧ Disjoint (closure[inst] (v n)) s
open_lemma :
  ∀ (u₀ a : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst] (u₀ n)) → IsOpen[inst] (⋃ (n : ℕ), u₀ n \ closure[inst] (a n))
cover_lemma :
  ∀ (h₀ : Set X) (u₀ v₀ : ℕ → Set X),
    h₀ ⊆ ⋃ (n : ℕ), u₀ n →
      (∀ (n : ℕ), Disjoint (closure[inst] (v₀ n)) h₀) →
        h₀ ⊆ ⋃ (n : ℕ), u₀ n \ closure[inst] (⋃ (m : ℕ), ⋃ (_ : m ≤ n), v₀ m)
x : X
n : ℕ
xinun : Membership.mem (γ := Set X) ((fun (n : ℕ) ↦ u n \ closure[inst] (⋃ (m : ℕ), ⋃ (_ : m ≤ n), v m)) n) x
⊢ x ∉ ⋃ (n : ℕ), v n \ closure[inst] (⋃ (m : ℕ), ⋃ (_ : m ≤ n), u m)
have mp : ∀ (m : ℕ),
  x ∈ v m →
    Membership.mem (γ := Set X)
      (closure[inst] (⋃ (m' : ℕ), ⋃ (_ : Membership.mem (γ := Set ℕ) {m' : ℕ | m' ≤ m} m'), u m')) x
Tactic: suffices ∀ (m : ℕ), x ∈ v m → x ∈ closure (⋃ m' ∈ {m' | m' ≤ m}, u m') by simpa
-- Lean 4 proof step from Mathlib.Topology.Separation.SeparatedNhds (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
u : ℕ → Set X
u_cov : s ⊆ ⋃ (n : ℕ), u n
u_props : ∀ (n : ℕ), IsOpen[inst] (u n) ∧ Disjoint (closure[inst] (u n)) t
v : ℕ → Set X
v_cov : t ⊆ ⋃ (n : ℕ), v n
v_props : ∀ (n : ℕ), IsOpen[inst] (v n) ∧ Disjoint (closure[inst] (v n)) s
open_lemma :
  ∀ (u₀ a : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst] (u₀ n)) → IsOpen[inst] (⋃ (n : ℕ), u₀ n \ closure[inst] (a n))
cover_lemma :
  ∀ (h₀ : Set X) (u₀ v₀ : ℕ → Set X),
    h₀ ⊆ ⋃ (n : ℕ), u₀ n →
      (∀ (n : ℕ), Disjoint (closure[inst] (v₀ n)) h₀) →
        h₀ ⊆ ⋃ (n : ℕ), u₀ n \ closure[inst] (⋃ (m : ℕ), ⋃ (_ : m ≤ n), v₀ m)
x : X
n : ℕ
xinun : Membership.mem (γ := Set X) ((fun (n : ℕ) ↦ u n \ closure[inst] (⋃ (m : ℕ), ⋃ (_ : m ≤ n), v m)) n) x
m : ℕ
xinvm : x ∈ v m
⊢ n ≤ m
have by_contra : ∀ (m_gt_n : ¬n ≤ m), False
Tactic: by_contra m_gt_n
-- Lean 4 proof step from Mathlib.Topology.Separation.SeparatedNhds (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
u : ℕ → Set X
u_cov : s ⊆ ⋃ (n : ℕ), u n
u_props : ∀ (n : ℕ), IsOpen[inst] (u n) ∧ Disjoint (closure[inst] (u n)) t
v : ℕ → Set X
v_cov : t ⊆ ⋃ (n : ℕ), v n
v_props : ∀ (n : ℕ), IsOpen[inst] (v n) ∧ Disjoint (closure[inst] (v n)) s
open_lemma :
  ∀ (u₀ a : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst] (u₀ n)) → IsOpen[inst] (⋃ (n : ℕ), u₀ n \ closure[inst] (a n))
cover_lemma :
  ∀ (h₀ : Set X) (u₀ v₀ : ℕ → Set X),
    h₀ ⊆ ⋃ (n : ℕ), u₀ n →
      (∀ (n : ℕ), Disjoint (closure[inst] (v₀ n)) h₀) →
        h₀ ⊆ ⋃ (n : ℕ), u₀ n \ closure[inst] (⋃ (m : ℕ), ⋃ (_ : m ≤ n), v₀ m)
x : X
n : ℕ
xinun : Membership.mem (γ := Set X) ((fun (n : ℕ) ↦ u n \ closure[inst] (⋃ (m : ℕ), ⋃ (_ : m ≤ n), v m)) n) x
m : ℕ
xinvm : x ∈ v m
⊢ Membership.mem (γ := Set X)
    (closure[inst] (⋃ (m' : ℕ), ⋃ (_ : Membership.mem (γ := Set ℕ) {m' : ℕ | m' ≤ m} m'), u m')) x
have n_le_m : n ≤ m
Tactic: have n_le_m : n ≤ m := by
      by_contra m_gt_n
      exact xinun.2 (subset_closure (mem_biUnion (le_of_lt (not_le.mp m_gt_n)) xinvm))
-- Lean 4 proof step from Mathlib.Topology.Separation.SeparatedNhds (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s₁ s₂ t₁ t₂ : Set X
sc_st : HasSeparatingCover s₂ t₂
s_sub : s₁ ⊆ s₂
t_sub : t₁ ⊆ t₂
⊢ HasSeparatingCover s₁ t₁
have obtain : ∀ (u : ℕ → Set X) (u_cov : s₂ ⊆ ⋃ (n : ℕ), u n)
  (u_props : ∀ (n : ℕ), IsOpen[inst] (u n) ∧ Disjoint (closure[inst] (u n)) t₂), HasSeparatingCover s₁ t₁
Tactic: obtain ⟨u, u_cov, u_props⟩ := sc_st
Cleared hypotheses: sc_st
-- Lean 4 proof step from Mathlib.Topology.Separation.SeparatedNhds (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hst : SeparatedNhds s t
hst' : IsOpen[inst] (s ∪ t)
⊢ IsOpen[inst] s
have obtain : ∀ (u v : Set X) (hu : IsOpen[inst] u) (hv : IsOpen[inst] v) (hsu : s ⊆ u) (htv : t ⊆ v) (huv : Disjoint u v),
  IsOpen[inst] s
Tactic: obtain ⟨u, v, hu, hv, hsu, htv, huv⟩ := hst
Cleared hypotheses: hst
-- Lean 4 proof step from Mathlib.Topology.Separation.SeparatedNhds (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hst' : IsOpen[inst] (s ∪ t)
u v : Set X
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hsu : s ⊆ u
htv : t ⊆ v
huv : Disjoint u v
⊢ IsOpen[inst] s
have suffices : s = (s ∪ t) ∩ u
Tactic: suffices s = (s ∪ t) ∩ u from this ▸ hst'.inter hu
-- Lean 4 proof step from Mathlib.Topology.Separation.SeparatedNhds (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hst' : IsOpen[inst] (s ∪ t)
u v : Set X
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hsu : s ⊆ u
htv : t ⊆ v
huv : Disjoint u v
⊢ s = (s ∪ t) ∩ u
have rw : s = s ∩ u ∪ t ∩ u
Tactic: rw [union_inter_distrib_right, (huv.symm.mono_left htv).inter_eq, union_empty,
    inter_eq_left.2 hsu]
-- Lean 4 proof step from Mathlib.Topology.Separation.SeparatedNhds (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hst' : IsOpen[inst] (s ∪ t)
u v : Set X
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hsu : s ⊆ u
htv : t ⊆ v
huv : Disjoint u v
rw : s = s ∩ u ∪ t ∩ u
⊢ s = (s ∪ t) ∩ u
have rw₁ : s = s ∩ u ∪ ∅
Tactic: rw [union_inter_distrib_right, (huv.symm.mono_left htv).inter_eq, union_empty,
    inter_eq_left.2 hsu]
-- Lean 4 proof step from Mathlib.Topology.Separation.SeparatedNhds (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hst' : IsOpen[inst] (s ∪ t)
u v : Set X
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hsu : s ⊆ u
htv : t ⊆ v
huv : Disjoint u v
rw : s = s ∩ u ∪ t ∩ u
rw₁ : s = s ∩ u ∪ ∅
⊢ s = (s ∪ t) ∩ u
have rw₂ : s = s ∩ u
Tactic: rw [union_inter_distrib_right, (huv.symm.mono_left htv).inter_eq, union_empty,
    inter_eq_left.2 hsu]
-- Lean 4 proof step from Mathlib.Topology.Separation.SeparatedNhds (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hst' : IsOpen[inst] (s ∪ t)
u v : Set X
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hsu : s ⊆ u
htv : t ⊆ v
huv : Disjoint u v
rw : s = s ∩ u ∪ t ∩ u
rw₁ : s = s ∩ u ∪ ∅
rw₂ : s = s ∩ u
⊢ s = (s ∪ t) ∩ u
have rw₃ : s = s
Tactic: rw [union_inter_distrib_right, (huv.symm.mono_left htv).inter_eq, union_empty,
    inter_eq_left.2 hsu]
-- Lean 4 proof step from Mathlib.Topology.Separation.SeparatedNhds (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hst : SeparatedNhds s t
hst' : IsClosed[inst] (s ∪ t)
⊢ IsClosed[inst] s
have obtain : ∀ (u v : Set X) (hu : IsOpen[inst] u) (hv : IsOpen[inst] v) (hsu : s ⊆ u) (htv : t ⊆ v) (huv : Disjoint u v),
  IsClosed[inst] s
Tactic: obtain ⟨u, v, hu, hv, hsu, htv, huv⟩ := hst
Cleared hypotheses: hst
-- Lean 4 proof step from Mathlib.Topology.Separation.SeparatedNhds (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hst' : IsClosed[inst] (s ∪ t)
u v : Set X
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hsu : s ⊆ u
htv : t ⊆ v
huv : Disjoint u v
⊢ IsClosed[inst] s
have rw : ∀ (hst' : IsOpen[inst] (s ∪ t)ᶜ) (u v : Set X) (hu : IsOpen[inst] u) (hv : IsOpen[inst] v) (hsu : s ⊆ u) (htv : t ⊆ v)
  (huv : Disjoint u v), IsOpen[inst] sᶜ
Tactic: rw [← isOpen_compl_iff] at hst' ⊢
Cleared hypotheses: hst', u, v, hu, hv, hsu, htv, huv
-- Lean 4 proof step from Mathlib.Topology.Separation.SeparatedNhds (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hst' : IsOpen[inst] (s ∪ t)ᶜ
u v : Set X
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hsu : s ⊆ u
htv : t ⊆ v
huv : Disjoint u v
⊢ IsOpen[inst] sᶜ
have suffices : sᶜ = (s ∪ t)ᶜ ∪ v
Tactic: suffices sᶜ = (s ∪ t)ᶜ ∪ v from this ▸ hst'.union hv
-- Lean 4 proof step from Mathlib.Topology.Separation.SeparatedNhds (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hst' : IsOpen[inst] (s ∪ t)ᶜ
u v : Set X
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hsu : s ⊆ u
htv : t ⊆ v
huv : Disjoint u v
⊢ sᶜ = (s ∪ t)ᶜ ∪ v
have rw : v ⊆ sᶜ
Tactic: rw [← compl_inj_iff, Set.compl_union, compl_compl, compl_compl, union_inter_distrib_right,
    (disjoint_compl_right.mono_left htv).inter_eq, union_empty, left_eq_inter, subset_compl_comm]
-- Lean 4 proof step from Mathlib.Topology.Sequences (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : FrechetUrysohnSpace X
s : Set X
a : X
⊢ a ∈ closure[inst] s ↔ ∃ (x : ℕ → X), (∀ (n : ℕ), x n ∈ s) ∧ Tendsto x atTop (𝓝 a)
have rw : a ∈ seqClosure s ↔ ∃ (x : ℕ → X), (∀ (n : ℕ), x n ∈ s) ∧ Tendsto x atTop (𝓝 a)
Tactic: rw [← seqClosure_eq_closure]
-- Lean 4 proof step from Mathlib.Topology.Sequences (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : FrechetUrysohnSpace X
f : X → Y
a : X
b : Y
⊢ Tendsto f (𝓝 a) (𝓝 b) ↔ ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)
have hf : ∀ (h : ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)) (ib : Set Y),
  b ∉ ib ∧ IsClosed[inst_1] ib → ∃ (ia : Set X), (a ∉ ia ∧ IsClosed[inst] ia) ∧ ∀ x ∈ iaᶜ, f x ∈ ibᶜ
Tactic: refine
    ⟨fun hf u hu => hf.comp hu, fun h =>
      ((nhds_basis_closeds _).tendsto_iff (nhds_basis_closeds _)).2 ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Sequences (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : FrechetUrysohnSpace X
f : X → Y
a : X
b : Y
h : ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)
s : Set Y
hbs : b ∉ s
hsc : IsClosed[inst_1] s
⊢ ∃ (ia : Set X), (a ∉ ia ∧ IsClosed[inst] ia) ∧ ∀ x ∈ iaᶜ, f x ∈ sᶜ
have refine : a ∈ closure[inst] (f ⁻¹' s) → b ∈ s
Tactic: refine ⟨closure (f ⁻¹' s), ⟨mt ?_ hbs, isClosed_closure⟩, fun x => mt fun hx => subset_closure hx⟩
-- Lean 4 proof step from Mathlib.Topology.Sequences (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : FrechetUrysohnSpace X
f : X → Y
a : X
b : Y
h : ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)
s : Set Y
hbs : b ∉ s
hsc : IsClosed[inst_1] s
⊢ a ∈ closure[inst] (f ⁻¹' s) → b ∈ s
have rw : a ∈ seqClosure (f ⁻¹' s) → b ∈ s
Tactic: rw [← seqClosure_eq_closure]
-- Lean 4 proof step from Mathlib.Topology.Sequences (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
⊢ FrechetUrysohnSpace X
have refine : ∀ (s : Set X) (x : X) (hcx : x ∈ closure[inst] s), x ∈ seqClosure s
Tactic: refine ⟨fun s x hcx => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Sequences (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
s : Set X
x : X
hcx : x ∈ closure[inst] s
⊢ x ∈ seqClosure s
have pos : ∀ (hx : x ∈ s), x ∈ seqClosure s
Tactic: by_cases hx : x ∈ s
-- Lean 4 proof step from Mathlib.Topology.Sequences (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
s : Set X
x : X
hcx : x ∈ closure[inst] s
pos : ∀ (hx : x ∈ s), x ∈ seqClosure s
⊢ x ∈ seqClosure s
have neg : ∀ (hx : x ∉ s), x ∈ seqClosure s
Tactic: by_cases hx : x ∈ s
-- Lean 4 proof step from Mathlib.Topology.Sequences (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
s : Set X
x : X
hcx : x ∈ closure[inst] s
hx : x ∉ s
⊢ x ∈ seqClosure s
have neg : ∀ (u : ℕ → X) (hux : Tendsto u atTop (𝓝 x)) (hus : ∃ᶠ (x : ℕ) in atTop, u x ∈ s), x ∈ seqClosure s
Tactic: obtain ⟨u, hux, hus⟩ : ∃ u : ℕ → X, Tendsto u atTop (𝓝 x) ∧ ∃ᶠ x in atTop, u x ∈ s := by
      simpa only [ContinuousAt, hx, tendsto_nhds_true, (· ∘ ·), ← not_frequently, exists_prop,
        ← mem_closure_iff_frequently, hcx, imp_false, not_forall, not_not, not_false_eq_true,
        not_true_eq_false] using h (· ∉ s) x
-- Lean 4 proof step from Mathlib.Topology.Sequences (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
s : Set X
x : X
hcx : x ∈ closure[inst] s
hx : x ∉ s
u : ℕ → X
hux : Tendsto u atTop (𝓝 x)
hus : ∃ᶠ (x : ℕ) in atTop, u x ∈ s
⊢ x ∈ seqClosure s
have neg : ∀ (φ : ℕ → ℕ) (φ_mono : StrictMono φ) (hφ : ∀ (n : ℕ), u (φ n) ∈ s), x ∈ seqClosure s
Tactic: rcases extraction_of_frequently_atTop hus with ⟨φ, φ_mono, hφ⟩
-- Lean 4 proof step from Mathlib.Topology.Sequences (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : FrechetUrysohnSpace X
s : Set X
hs : IsSeqClosed s
⊢ IsClosed[inst] s
have rw : closure[inst] s = s
Tactic: rw [← closure_eq_iff_isClosed, ← seqClosure_eq_closure, hs.seqClosure_eq]
-- Lean 4 proof step from Mathlib.Topology.Sequences (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : FrechetUrysohnSpace X
s : Set X
hs : IsSeqClosed s
rw : closure[inst] s = s
⊢ IsClosed[inst] s
have rw₁ : seqClosure s = s
Tactic: rw [← closure_eq_iff_isClosed, ← seqClosure_eq_closure, hs.seqClosure_eq]
-- Lean 4 proof step from Mathlib.Topology.Sequences (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : FrechetUrysohnSpace X
s : Set X
hs : IsSeqClosed s
rw : closure[inst] s = s
rw₁ : seqClosure s = s
⊢ IsClosed[inst] s
have rw₂ : s = s
Tactic: rw [← closure_eq_iff_isClosed, ← seqClosure_eq_closure, hs.seqClosure_eq]
-- Lean 4 proof step from Mathlib.Topology.Sequences (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : FrechetUrysohnSpace Y
f : X → Y
hf : IsInducing f
⊢ FrechetUrysohnSpace X
have refine : ∀ (s : Set X) (x : X) (hx : x ∈ closure[inst] s), x ∈ seqClosure s
Tactic: refine ⟨fun s x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Sequences (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : FrechetUrysohnSpace Y
f : X → Y
hf : IsInducing f
s : Set X
x : X
hx : x ∈ closure[inst] s
⊢ x ∈ seqClosure s
have hx₁ : ∃ (x_1 : ℕ → Y), (∀ (n : ℕ), x_1 n ∈ f '' s) ∧ Tendsto x_1 atTop (𝓝 (f x))
Tactic: rw [hf.closure_eq_preimage_closure_image, mem_preimage, mem_closure_iff_seq_limit] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.Sequences (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : FrechetUrysohnSpace Y
f : X → Y
hf : IsInducing f
s : Set X
x : X
hx : ∃ (x_1 : ℕ → Y), (∀ (n : ℕ), x_1 n ∈ f '' s) ∧ Tendsto x_1 atTop (𝓝 (f x))
⊢ x ∈ seqClosure s
have rcases : ∀ (u : ℕ → Y) (hus : ∀ (n : ℕ), u n ∈ f '' s) (hu : Tendsto u atTop (𝓝 (f x))), x ∈ seqClosure s
Tactic: rcases hx with ⟨u, hus, hu⟩
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.Sequences (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : FrechetUrysohnSpace Y
f : X → Y
hf : IsInducing f
s : Set X
x : X
u : ℕ → Y
hus : ∀ (n : ℕ), u n ∈ f '' s
hu : Tendsto u atTop (𝓝 (f x))
⊢ x ∈ seqClosure s
have choose : ∀ (v : (n : ℕ) → X) (hv : ∀ (n : ℕ), v n ∈ s) (hvu : ∀ (n : ℕ), f (v n) = u n), x ∈ seqClosure s
Tactic: choose v hv hvu using hus
Cleared hypotheses: hus
-- Lean 4 proof step from Mathlib.Topology.Sequences (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : FrechetUrysohnSpace Y
f : X → Y
hf : IsInducing f
s : Set X
x : X
u : ℕ → Y
hu : Tendsto u atTop (𝓝 (f x))
v : (n : ℕ) → X
hv : ∀ (n : ℕ), v n ∈ s
hvu : ∀ (n : ℕ), f (v n) = u n
⊢ x ∈ seqClosure s
have refine : Tendsto v atTop (𝓝 x)
Tactic: refine ⟨v, hv, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Sequences (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x : ℕ → X
inst_1 : SequentialSpace X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
⊢ IsClosed[inst] (⋃ (i : ℕ), closure[inst] {x i})
have refine : ∀ (y : ℕ → X) (l : X) (hy : ∀ (n : ℕ), Membership.mem (γ := Set X) (⋃ (i : ℕ), closure[inst] {x i}) (y n))
  (hy' : Tendsto y atTop (𝓝 l)), Membership.mem (γ := Set X) (⋃ (i : ℕ), closure[inst] {x i}) l
Tactic: refine IsSeqClosed.isClosed fun y l hy hy' => ?_
-- Lean 4 proof step from Mathlib.Topology.Sequences (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x : ℕ → X
inst_1 : SequentialSpace X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
y : ℕ → X
l : X
hy : ∀ (n : ℕ), Membership.mem (γ := Set X) (⋃ (i : ℕ), closure[inst] {x i}) (y n)
hy' : Tendsto y atTop (𝓝 l)
⊢ Membership.mem (γ := Set X) (⋃ (i : ℕ), closure[inst] {x i}) l
have pos : ∀ (hm : ∃ (m : ℕ), ∃ᶠ (n : ℕ) in atTop, Membership.mem (γ := Set X) (closure[inst] {x m}) (y n)),
  Membership.mem (γ := Set X) (⋃ (i : ℕ), closure[inst] {x i}) l
Tactic: by_cases! hm : ∃ m, ∃ᶠ n in atTop, y n ∈ closure {x m}