awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
s : Set X
simp_rw :
  (∀ t ∈ 𝓝 x, (t ∩ s).Nonempty) ↔ NeBot (α := { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝 x))
simp_rw₁ : (∀ t ∈ 𝓝 x, (t ∩ s).Nonempty) ↔ ∀ t ∈ 𝓝 x, ∃ (a : { x : X // x ∈ s }), (↑a : X) ∈ t
⊢ x ∈ closure[inst] s ↔ NeBot (α := { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝 x))
have simp_rw₂ : (∀ t ∈ 𝓝 x, ∃ x ∈ s, x ∈ t) ↔ ∀ t ∈ 𝓝 x, ∃ (a : { x : X // x ∈ s }), (↑a : X) ∈ t
Tactic: simp_rw [mem_closure_iff_nhds, comap_neBot_iff, Set.inter_nonempty_iff_exists_right,
    SetCoe.exists, exists_prop]
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
s : Set X
simp_rw :
  (∀ t ∈ 𝓝 x, (t ∩ s).Nonempty) ↔ NeBot (α := { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝 x))
simp_rw₁ : (∀ t ∈ 𝓝 x, (t ∩ s).Nonempty) ↔ ∀ t ∈ 𝓝 x, ∃ (a : { x : X // x ∈ s }), (↑a : X) ∈ t
simp_rw₂ : (∀ t ∈ 𝓝 x, ∃ x ∈ s, x ∈ t) ↔ ∀ t ∈ 𝓝 x, ∃ (a : { x : X // x ∈ s }), (↑a : X) ∈ t
⊢ x ∈ closure[inst] s ↔ NeBot (α := { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝 x))
have simp_rw₃ : (∀ t ∈ 𝓝 x, ∃ x ∈ s, x ∈ t) ↔ ∀ t ∈ 𝓝 x, ∃ (x : X) (_ : x ∈ s), x ∈ t
Tactic: simp_rw [mem_closure_iff_nhds, comap_neBot_iff, Set.inter_nonempty_iff_exists_right,
    SetCoe.exists, exists_prop]
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
F : Filter X
⊢ ClusterPt x F ↔ pure x ≤ F.lift' closure[inst]
have simp_rw : (∀ s ∈ F, x ∈ closure[inst] s) ↔ pure x ≤ F.lift' closure[inst]
Tactic: simp_rw [clusterPt_iff_forall_mem_closure,
    (hasBasis_pure _).le_basis_iff F.basis_sets.lift'_closure, id, singleton_subset_iff, true_and,
    exists_const]
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
F : Filter X
simp_rw : (∀ s ∈ F, x ∈ closure[inst] s) ↔ pure x ≤ F.lift' closure[inst]
⊢ ClusterPt x F ↔ pure x ≤ F.lift' closure[inst]
have simp_rw₁ : (∀ s ∈ F, x ∈ closure[inst] s) ↔ ∀ i' ∈ F, ∃ (i : Unit), True ∧ {x} ⊆ closure[inst] (id i')
Tactic: simp_rw [clusterPt_iff_forall_mem_closure,
    (hasBasis_pure _).le_basis_iff F.basis_sets.lift'_closure, id, singleton_subset_iff, true_and,
    exists_const]
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
F : Filter X
simp_rw : (∀ s ∈ F, x ∈ closure[inst] s) ↔ pure x ≤ F.lift' closure[inst]
simp_rw₁ : (∀ s ∈ F, x ∈ closure[inst] s) ↔ ∀ i' ∈ F, ∃ (i : Unit), True ∧ {x} ⊆ closure[inst] (id i')
⊢ ClusterPt x F ↔ pure x ≤ F.lift' closure[inst]
have simp_rw₂ : (∀ s ∈ F, x ∈ closure[inst] s) ↔ ∀ i' ∈ F, ∃ (i : Unit), True ∧ {x} ⊆ closure[inst] i'
Tactic: simp_rw [clusterPt_iff_forall_mem_closure,
    (hasBasis_pure _).le_basis_iff F.basis_sets.lift'_closure, id, singleton_subset_iff, true_and,
    exists_const]
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
F : Filter X
simp_rw : (∀ s ∈ F, x ∈ closure[inst] s) ↔ pure x ≤ F.lift' closure[inst]
simp_rw₁ : (∀ s ∈ F, x ∈ closure[inst] s) ↔ ∀ i' ∈ F, ∃ (i : Unit), True ∧ {x} ⊆ closure[inst] (id i')
simp_rw₂ : (∀ s ∈ F, x ∈ closure[inst] s) ↔ ∀ i' ∈ F, ∃ (i : Unit), True ∧ {x} ⊆ closure[inst] i'
⊢ ClusterPt x F ↔ pure x ≤ F.lift' closure[inst]
have simp_rw₃ : (∀ s ∈ F, x ∈ closure[inst] s) ↔ ∀ i' ∈ F, ∃ (i : Unit), True ∧ x ∈ closure[inst] i'
Tactic: simp_rw [clusterPt_iff_forall_mem_closure,
    (hasBasis_pure _).le_basis_iff F.basis_sets.lift'_closure, id, singleton_subset_iff, true_and,
    exists_const]
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
F : Filter X
simp_rw : (∀ s ∈ F, x ∈ closure[inst] s) ↔ pure x ≤ F.lift' closure[inst]
simp_rw₁ : (∀ s ∈ F, x ∈ closure[inst] s) ↔ ∀ i' ∈ F, ∃ (i : Unit), True ∧ {x} ⊆ closure[inst] (id i')
simp_rw₂ : (∀ s ∈ F, x ∈ closure[inst] s) ↔ ∀ i' ∈ F, ∃ (i : Unit), True ∧ {x} ⊆ closure[inst] i'
simp_rw₃ : (∀ s ∈ F, x ∈ closure[inst] s) ↔ ∀ i' ∈ F, ∃ (i : Unit), True ∧ x ∈ closure[inst] i'
⊢ ClusterPt x F ↔ pure x ≤ F.lift' closure[inst]
have simp_rw₄ : (∀ s ∈ F, x ∈ closure[inst] s) ↔ ∀ i' ∈ F, ∃ (i : Unit), x ∈ closure[inst] i'
Tactic: simp_rw [clusterPt_iff_forall_mem_closure,
    (hasBasis_pure _).le_basis_iff F.basis_sets.lift'_closure, id, singleton_subset_iff, true_and,
    exists_const]
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
F : Filter X
⊢ ClusterPt x F ↔ (F.lift' closure[inst] ⊓ pure x).NeBot
have rw : pure x ≤ F.lift' closure[inst] ↔ (pure x ⊓ F.lift' closure[inst]).NeBot
Tactic: rw [clusterPt_iff_lift'_closure, inf_comm]
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
F : Filter X
⊢ pure x ≤ F.lift' closure[inst] ↔ (pure x ⊓ F.lift' closure[inst]).NeBot
have mp : pure x ≤ F.lift' closure[inst] → (pure x ⊓ F.lift' closure[inst]).NeBot
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
F : Filter X
mp : pure x ≤ F.lift' closure[inst] → (pure x ⊓ F.lift' closure[inst]).NeBot
⊢ pure x ≤ F.lift' closure[inst] ↔ (pure x ⊓ F.lift' closure[inst]).NeBot
have mpr : (pure x ⊓ F.lift' closure[inst]).NeBot → pure x ≤ F.lift' closure[inst]
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
F : Filter X
h : (pure x ⊓ F.lift' closure[inst]).NeBot
U : Set X
hU : U ∈ F.lift' closure[inst]
⊢ Membership.mem (γ := Filter X) (pure x) U
have h₁ : ∀ (s : Set X),
  (∃ (t₁ : Set X), Membership.mem (γ := Filter X) (pure x) t₁ ∧ ∃ t₂ ∈ F.lift' closure[inst], s = t₁ ∩ t₂) → s.Nonempty
Tactic: simp_rw [← forall_mem_nonempty_iff_neBot, mem_inf_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ IsClosed[inst] s ↔ ∀ (x : X), (∀ U ∈ 𝓝 x, (U ∩ s).Nonempty) → x ∈ s
have simp_rw : (∀ (a : X), ClusterPt a (𝓟 s) → a ∈ s) ↔ ∀ (x : X), (∀ U ∈ 𝓝 x, (U ∩ s).Nonempty) → x ∈ s
Tactic: simp_rw [isClosed_iff_clusterPt, ClusterPt, inf_principal_neBot_iff]
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
simp_rw : (∀ (a : X), ClusterPt a (𝓟 s) → a ∈ s) ↔ ∀ (x : X), (∀ U ∈ 𝓝 x, (U ∩ s).Nonempty) → x ∈ s
⊢ IsClosed[inst] s ↔ ∀ (x : X), (∀ U ∈ 𝓝 x, (U ∩ s).Nonempty) → x ∈ s
have simp_rw₁ : (∀ (a : X), (𝓝 a ⊓ 𝓟 s).NeBot → a ∈ s) ↔ ∀ (x : X), (∀ U ∈ 𝓝 x, (U ∩ s).Nonempty) → x ∈ s
Tactic: simp_rw [isClosed_iff_clusterPt, ClusterPt, inf_principal_neBot_iff]
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ IsClosed[inst] s ↔ ∀ (x : X) (F : Filter X), F.NeBot → F ≤ 𝓟 s → F ≤ 𝓝 x → x ∈ s
have simp_rw : (∀ (a : X), ClusterPt a (𝓟 s) → a ∈ s) ↔ ∀ (x : X) (F : Filter X), F.NeBot → F ≤ 𝓟 s → F ≤ 𝓝 x → x ∈ s
Tactic: simp_rw [isClosed_iff_clusterPt]
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
s₁ s₂ : Set X
h : x ∈ closure[inst] (s₁ ∪ s₂)
h₁ : s₁ᶜ ∈ 𝓝 x
⊢ x ∈ closure[inst] s₂
have rw : ∀ (h : 𝓝 x ⊓ 𝓟 (s₁ ∪ s₂) ≠ ⊥) (h₁ : s₁ᶜ ∈ 𝓝 x), 𝓝 x ⊓ 𝓟 s₂ ≠ ⊥
Tactic: rw [mem_closure_iff_nhds_ne_bot] at *
Cleared hypotheses: h, h₁
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
s₁ s₂ : Set X
h : 𝓝 x ⊓ 𝓟 (s₁ ∪ s₂) ≠ ⊥
h₁ : s₁ᶜ ∈ 𝓝 x
⊢ 𝓝 x ⊓ 𝓟 s₂ ≠ ⊥
have rwa : ∀ (h : 𝓝 x ⊓ (𝓟 s₁ ⊔ 𝓟 s₂) ≠ ⊥) (h₁ : s₁ᶜ ∈ 𝓝 x), 𝓝 x ⊓ 𝓟 s₂ ≠ ⊥
Tactic: rwa [← sup_principal, inf_sup_left, inf_principal_eq_bot.mpr h₁, bot_sup_eq] at h
Cleared hypotheses: h, h₁
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
s₁ s₂ : Set X
h : 𝓝 x ⊓ 𝓟 (s₁ ∪ s₂) ≠ ⊥
h₁ : s₁ᶜ ∈ 𝓝 x
rwa : ∀ (h : 𝓝 x ⊓ (𝓟 s₁ ⊔ 𝓟 s₂) ≠ ⊥) (h₁ : s₁ᶜ ∈ 𝓝 x), 𝓝 x ⊓ 𝓟 s₂ ≠ ⊥
⊢ 𝓝 x ⊓ 𝓟 s₂ ≠ ⊥
have rwa₁ : ∀ (h : 𝓝 x ⊓ 𝓟 s₁ ⊔ 𝓝 x ⊓ 𝓟 s₂ ≠ ⊥) (h₁ : s₁ᶜ ∈ 𝓝 x), 𝓝 x ⊓ 𝓟 s₂ ≠ ⊥
Tactic: rwa [← sup_principal, inf_sup_left, inf_principal_eq_bot.mpr h₁, bot_sup_eq] at h
Cleared hypotheses: h, h₁
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
s₁ s₂ : Set X
h : 𝓝 x ⊓ 𝓟 (s₁ ∪ s₂) ≠ ⊥
h₁ : s₁ᶜ ∈ 𝓝 x
rwa : ∀ (h : 𝓝 x ⊓ (𝓟 s₁ ⊔ 𝓟 s₂) ≠ ⊥) (h₁ : s₁ᶜ ∈ 𝓝 x), 𝓝 x ⊓ 𝓟 s₂ ≠ ⊥
rwa₁ : ∀ (h : 𝓝 x ⊓ 𝓟 s₁ ⊔ 𝓝 x ⊓ 𝓟 s₂ ≠ ⊥) (h₁ : s₁ᶜ ∈ 𝓝 x), 𝓝 x ⊓ 𝓟 s₂ ≠ ⊥
⊢ 𝓝 x ⊓ 𝓟 s₂ ≠ ⊥
have rwa₂ : ∀ (h : ⊥ ⊔ 𝓝 x ⊓ 𝓟 s₂ ≠ ⊥) (h₁ : s₁ᶜ ∈ 𝓝 x), 𝓝 x ⊓ 𝓟 s₂ ≠ ⊥
Tactic: rwa [← sup_principal, inf_sup_left, inf_principal_eq_bot.mpr h₁, bot_sup_eq] at h
Cleared hypotheses: h, h₁
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
s₁ s₂ : Set X
h : 𝓝 x ⊓ 𝓟 (s₁ ∪ s₂) ≠ ⊥
h₁ : s₁ᶜ ∈ 𝓝 x
rwa : ∀ (h : 𝓝 x ⊓ (𝓟 s₁ ⊔ 𝓟 s₂) ≠ ⊥) (h₁ : s₁ᶜ ∈ 𝓝 x), 𝓝 x ⊓ 𝓟 s₂ ≠ ⊥
rwa₁ : ∀ (h : 𝓝 x ⊓ 𝓟 s₁ ⊔ 𝓝 x ⊓ 𝓟 s₂ ≠ ⊥) (h₁ : s₁ᶜ ∈ 𝓝 x), 𝓝 x ⊓ 𝓟 s₂ ≠ ⊥
rwa₂ : ∀ (h : ⊥ ⊔ 𝓝 x ⊓ 𝓟 s₂ ≠ ⊥) (h₁ : s₁ᶜ ∈ 𝓝 x), 𝓝 x ⊓ 𝓟 s₂ ≠ ⊥
⊢ 𝓝 x ⊓ 𝓟 s₂ ≠ ⊥
have rwa₃ : ∀ (h : 𝓝 x ⊓ 𝓟 s₂ ≠ ⊥) (h₁ : s₁ᶜ ∈ 𝓝 x), 𝓝 x ⊓ 𝓟 s₂ ≠ ⊥
Tactic: rwa [← sup_principal, inf_sup_left, inf_principal_eq_bot.mpr h₁, bot_sup_eq] at h
Cleared hypotheses: h, h₁
-- Lean 4 proof step from Mathlib.Topology.Coherent (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (Set X)
h : ∀ (f : X → Prop), (∀ s ∈ S, ContinuousOn f s) → Continuous[inst, _] f
u : Set X
hu : ∀ s ∈ S, IsOpen[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' u)
⊢ IsOpen[inst] u
have h₁ : ∀ (f : X → Prop),
  (∀ s ∈ S, IsOpen[instTopologicalSpaceSubtype] {x : (↑s : Type u_1) | s.restrict (π := fun (a : X) ↦ Prop) f x}) →
    IsOpen[inst] {x : X | f x}
Tactic: simp only [continuousOn_iff_continuous_restrict, continuous_Prop] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Coherent (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (Set X)
inst_1 : SequentialSpace X
h : ∀ ⦃u : ℕ → X⦄ ⦃x : X⦄, Tendsto u atTop (𝓝 x) → insert x (range u) ∈ S
⊢ IsCoherentWith S
have refine : ∀ (t : Set X) (ht : ∀ s ∈ S, IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' t))
  (u : ℕ → X) (x : X) (hut : ∀ (n : ℕ), u n ∈ t) (hux : Tendsto u atTop (𝓝 x)), x ∈ t
Tactic: refine of_isClosed fun t ht ↦ IsSeqClosed.isClosed fun u x hut hux ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Coherent (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (Set X)
inst_1 : SequentialSpace X
h : ∀ ⦃u : ℕ → X⦄ ⦃x : X⦄, Tendsto u atTop (𝓝 x) → insert x (range u) ∈ S
t : Set X
ht : ∀ s ∈ S, IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' t)
u : ℕ → X
x : X
hut : ∀ (n : ℕ), u n ∈ t
hux : Tendsto u atTop (𝓝 x)
⊢ x ∈ t
have rcases : ∀ (s : Set X) (hsc : IsClosed[inst] s)
  (hst :
    Eq (α := Set (↑(insert x (range u)) : Type u_1)) (Subtype.val (p := fun (x_1 : X) ↦ x_1 ∈ insert x (range u)) ⁻¹' s)
      (Subtype.val (p := fun (x_1 : X) ↦ x_1 ∈ insert x (range u)) ⁻¹' t)),
  x ∈ t
Tactic: rcases isClosed_induced_iff.1 (ht _ (h hux)) with ⟨s, hsc, hst⟩
-- Lean 4 proof step from Mathlib.Topology.Coherent (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (Set X)
inst_1 : SequentialSpace X
h : ∀ ⦃u : ℕ → X⦄ ⦃x : X⦄, Tendsto u atTop (𝓝 x) → insert x (range u) ∈ S
t : Set X
ht : ∀ s ∈ S, IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' t)
u : ℕ → X
x : X
hut : ∀ (n : ℕ), u n ∈ t
hux : Tendsto u atTop (𝓝 x)
s : Set X
hsc : IsClosed[inst] s
hst :
  Eq (α := Set (↑(insert x (range u)) : Type u_1)) (Subtype.val (p := fun (x_1 : X) ↦ x_1 ∈ insert x (range u)) ⁻¹' s)
    (Subtype.val (p := fun (x_1 : X) ↦ x_1 ∈ insert x (range u)) ⁻¹' t)
⊢ x ∈ t
have hst₁ : ∀ (x_1 : X), x_1 ∈ insert x (range u) ∩ s ↔ x_1 ∈ insert x (range u) ∩ t
Tactic: rw [Subtype.preimage_val_eq_preimage_val_iff, Set.ext_iff] at hst
Cleared hypotheses: hst
-- Lean 4 proof step from Mathlib.Topology.Coherent (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (Set X)
inst_1 : SequentialSpace X
h : ∀ ⦃u : ℕ → X⦄ ⦃x : X⦄, Tendsto u atTop (𝓝 x) → insert x (range u) ∈ S
t : Set X
ht : ∀ s ∈ S, IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' t)
u : ℕ → X
x : X
hut : ∀ (n : ℕ), u n ∈ t
hux : Tendsto u atTop (𝓝 x)
s : Set X
hsc : IsClosed[inst] s
hst : ∀ (x_1 : X), x_1 ∈ insert x (range u) ∩ s ↔ x_1 ∈ insert x (range u) ∩ t
this : x ∈ s
⊢ x ∈ t
have hst₁ : x ∈ insert x (range u) ∩ s ↔ x ∈ insert x (range u) ∩ t
Tactic: specialize hst x
Cleared hypotheses: hst
-- Lean 4 proof step from Mathlib.Topology.Coherent (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (Set X)
inst_1 : SequentialSpace X
h : ∀ ⦃u : ℕ → X⦄ ⦃x : X⦄, Tendsto u atTop (𝓝 x) → insert x (range u) ∈ S
t : Set X
ht : ∀ s ∈ S, IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' t)
u : ℕ → X
x : X
hut : ∀ (n : ℕ), u n ∈ t
hux : Tendsto u atTop (𝓝 x)
s : Set X
hsc : IsClosed[inst] s
hst : ∀ (x_1 : X), x_1 ∈ insert x (range u) ∩ s ↔ x_1 ∈ insert x (range u) ∩ t
⊢ x ∈ t
have suffices : x ∈ s
Tactic: suffices x ∈ s by specialize hst x; simp_all
-- Lean 4 proof step from Mathlib.Topology.Coherent (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (Set X)
inst_1 : SequentialSpace X
h : ∀ ⦃u : ℕ → X⦄ ⦃x : X⦄, Tendsto u atTop (𝓝 x) → insert x (range u) ∈ S
t : Set X
ht : ∀ s ∈ S, IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' t)
u : ℕ → X
x : X
hut : ∀ (n : ℕ), u n ∈ t
hux : Tendsto u atTop (𝓝 x)
s : Set X
hsc : IsClosed[inst] s
hst : ∀ (x_1 : X), x_1 ∈ insert x (range u) ∩ s ↔ x_1 ∈ insert x (range u) ∩ t
⊢ x ∈ s
have refine : ∀ (k : ℕ), u k ∈ s
Tactic: refine hsc.mem_of_tendsto hux <| Eventually.of_forall fun k ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Coherent (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (Set X)
inst_1 : SequentialSpace X
h : ∀ ⦃u : ℕ → X⦄ ⦃x : X⦄, Tendsto u atTop (𝓝 x) → insert x (range u) ∈ S
t : Set X
ht : ∀ s ∈ S, IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' t)
u : ℕ → X
x : X
hut : ∀ (n : ℕ), u n ∈ t
hux : Tendsto u atTop (𝓝 x)
s : Set X
hsc : IsClosed[inst] s
hst : ∀ (x_1 : X), x_1 ∈ insert x (range u) ∩ s ↔ x_1 ∈ insert x (range u) ∩ t
k : ℕ
⊢ u k ∈ s
have hst₁ : u k ∈ insert x (range u) ∩ s ↔ u k ∈ insert x (range u) ∩ t
Tactic: specialize hst (u k)
Cleared hypotheses: hst
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (goal)
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
U : Set Y
inst_2 : CompactSpace X
hU : IsOpen[inst_1] U
⊢ IsOpen (X := C(X, Y)) {f : C(X, Y) | range.{u_3, u_2 + 1} (ι := X) (⇑f : (a : X) → Y) ⊆ U}
have simp_rw : IsOpen (X := C(X, Y)) {f : C(X, Y) | MapsTo.{u_2, u_3} (α := X) (⇑f : (a : X) → Y) univ U}
Tactic: simp_rw [← mapsTo_univ_iff_range_subset]
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (goal)
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : C(X, Y)
simp_rw :
  𝓝 f =
    ⨅ (K : Set X),
      ⨅ (_ : IsCompact K),
        ⨅ (U : Set Y),
          ⨅ (_ : IsOpen[inst_1] U),
            ⨅ (_ : MapsTo (⇑f : (a : X) → Y) K U), 𝓟 {g : C(X, Y) | MapsTo (⇑g : (a : X) → Y) K U}
⊢ 𝓝 f =
    ⨅ (K : Set X),
      ⨅ (_ : IsCompact K),
        ⨅ (U : Set Y),
          ⨅ (_ : IsOpen[inst_1] U),
            ⨅ (_ : MapsTo (⇑f : (a : X) → Y) K U), 𝓟 {g : C(X, Y) | MapsTo (⇑g : (a : X) → Y) K U}
have simp_rw₁ : Eq (α := Filter C(X, Y))
  (⨅ (s : Set C(X, Y)),
    ⨅ (_ :
      Membership.mem (γ := Set (Set C(X, Y)))
        {s : Set C(X, Y) |
          f ∈ s ∧
            Membership.mem (γ := Set (Set C(X, Y)))
              (image2 (fun (K : Set X) (U : Set Y) ↦ {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) K U})
                {K : Set X | IsCompact K} {t : Set Y | IsOpen[inst_1] t})
              s}
        s),
      𝓟 s)
  (⨅ (K : Set X),
    ⨅ (_ : IsCompact K),
      ⨅ (U : Set Y),
        ⨅ (_ : IsOpen[inst_1] U),
          ⨅ (_ : MapsTo (⇑f : (a : X) → Y) K U), 𝓟 {g : C(X, Y) | MapsTo (⇑g : (a : X) → Y) K U})
Tactic: simp_rw +instances [compactOpen_eq, nhds_generateFrom, mem_setOf_eq, @and_comm (f ∈ _), iInf_and,
    ← image_prod, iInf_image, biInf_prod, mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (goal)
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : C(X, Y)
simp_rw :
  𝓝 f =
    ⨅ (K : Set X),
      ⨅ (_ : IsCompact K),
        ⨅ (U : Set Y),
          ⨅ (_ : IsOpen[inst_1] U),
            ⨅ (_ : MapsTo (⇑f : (a : X) → Y) K U), 𝓟 {g : C(X, Y) | MapsTo (⇑g : (a : X) → Y) K U}
simp_rw₁ :
  Eq (α := Filter C(X, Y))
    (⨅ (s : Set C(X, Y)),
      ⨅ (_ :
        Membership.mem (γ := Set (Set C(X, Y)))
          {s : Set C(X, Y) |
            f ∈ s ∧
              Membership.mem (γ := Set (Set C(X, Y)))
                (image2 (fun (K : Set X) (U : Set Y) ↦ {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) K U})
                  {K : Set X | IsCompact K} {t : Set Y | IsOpen[inst_1] t})
                s}
          s),
        𝓟 s)
    (⨅ (K : Set X),
      ⨅ (_ : IsCompact K),
        ⨅ (U : Set Y),
          ⨅ (_ : IsOpen[inst_1] U),
            ⨅ (_ : MapsTo (⇑f : (a : X) → Y) K U), 𝓟 {g : C(X, Y) | MapsTo (⇑g : (a : X) → Y) K U})
⊢ 𝓝 f =
    ⨅ (K : Set X),
      ⨅ (_ : IsCompact K),
        ⨅ (U : Set Y),
          ⨅ (_ : IsOpen[inst_1] U),
            ⨅ (_ : MapsTo (⇑f : (a : X) → Y) K U), 𝓟 {g : C(X, Y) | MapsTo (⇑g : (a : X) → Y) K U}
have simp_rw₂ : Eq (α := Filter C(X, Y))
  (⨅ (s : Set C(X, Y)),
    ⨅ (_ :
      f ∈ s ∧
        Membership.mem (γ := Set (Set C(X, Y)))
          (image2 (fun (K : Set X) (U : Set Y) ↦ {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) K U})
            {K : Set X | IsCompact K} {t : Set Y | IsOpen[inst_1] t})
          s),
      𝓟 s)
  (⨅ (K : Set X),
    ⨅ (_ : IsCompact K),
      ⨅ (U : Set Y),
        ⨅ (_ : IsOpen[inst_1] U),
          ⨅ (_ : MapsTo (⇑f : (a : X) → Y) K U), 𝓟 {g : C(X, Y) | MapsTo (⇑g : (a : X) → Y) K U})
Tactic: simp_rw +instances [compactOpen_eq, nhds_generateFrom, mem_setOf_eq, @and_comm (f ∈ _), iInf_and,
    ← image_prod, iInf_image, biInf_prod, mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (goal)
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : C(X, Y)
simp_rw :
  𝓝 f =
    ⨅ (K : Set X),
      ⨅ (_ : IsCompact K),
        ⨅ (U : Set Y),
          ⨅ (_ : IsOpen[inst_1] U),
            ⨅ (_ : MapsTo (⇑f : (a : X) → Y) K U), 𝓟 {g : C(X, Y) | MapsTo (⇑g : (a : X) → Y) K U}
simp_rw₁ :
  Eq (α := Filter C(X, Y))
    (⨅ (s : Set C(X, Y)),
      ⨅ (_ :
        Membership.mem (γ := Set (Set C(X, Y)))
          {s : Set C(X, Y) |
            f ∈ s ∧
              Membership.mem (γ := Set (Set C(X, Y)))
                (image2 (fun (K : Set X) (U : Set Y) ↦ {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) K U})
                  {K : Set X | IsCompact K} {t : Set Y | IsOpen[inst_1] t})
                s}
          s),
        𝓟 s)
    (⨅ (K : Set X),
      ⨅ (_ : IsCompact K),
        ⨅ (U : Set Y),
          ⨅ (_ : IsOpen[inst_1] U),
            ⨅ (_ : MapsTo (⇑f : (a : X) → Y) K U), 𝓟 {g : C(X, Y) | MapsTo (⇑g : (a : X) → Y) K U})
simp_rw₂ :
  Eq (α := Filter C(X, Y))
    (⨅ (s : Set C(X, Y)),
      ⨅ (_ :
        f ∈ s ∧
          Membership.mem (γ := Set (Set C(X, Y)))
            (image2 (fun (K : Set X) (U : Set Y) ↦ {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) K U})
              {K : Set X | IsCompact K} {t : Set Y | IsOpen[inst_1] t})
            s),
        𝓟 s)
    (⨅ (K : Set X),
      ⨅ (_ : IsCompact K),
        ⨅ (U : Set Y),
          ⨅ (_ : IsOpen[inst_1] U),
            ⨅ (_ : MapsTo (⇑f : (a : X) → Y) K U), 𝓟 {g : C(X, Y) | MapsTo (⇑g : (a : X) → Y) K U})
⊢ 𝓝 f =
    ⨅ (K : Set X),
      ⨅ (_ : IsCompact K),
        ⨅ (U : Set Y),
          ⨅ (_ : IsOpen[inst_1] U),
            ⨅ (_ : MapsTo (⇑f : (a : X) → Y) K U), 𝓟 {g : C(X, Y) | MapsTo (⇑g : (a : X) → Y) K U}
have simp_rw₃ : Eq (α := Filter C(X, Y))
  (⨅ (s : Set C(X, Y)),
    ⨅ (_ :
      Membership.mem (γ := Set (Set C(X, Y)))
          (image2 (fun (K : Set X) (U : Set Y) ↦ {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) K U})
            {K : Set X | IsCompact K} {t : Set Y | IsOpen[inst_1] t})
          s ∧
        f ∈ s),
      𝓟 s)
  (⨅ (K : Set X),
    ⨅ (_ : IsCompact K),
      ⨅ (U : Set Y),
        ⨅ (_ : IsOpen[inst_1] U),
          ⨅ (_ : MapsTo (⇑f : (a : X) → Y) K U), 𝓟 {g : C(X, Y) | MapsTo (⇑g : (a : X) → Y) K U})
Tactic: simp_rw +instances [compactOpen_eq, nhds_generateFrom, mem_setOf_eq, @and_comm (f ∈ _), iInf_and,
    ← image_prod, iInf_image, biInf_prod, mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (goal)
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : C(X, Y)
simp_rw :
  𝓝 f =
    ⨅ (K : Set X),
      ⨅ (_ : IsCompact K),
        ⨅ (U : Set Y),
          ⨅ (_ : IsOpen[inst_1] U),
            ⨅ (_ : MapsTo (⇑f : (a : X) → Y) K U), 𝓟 {g : C(X, Y) | MapsTo (⇑g : (a : X) → Y) K U}
simp_rw₁ :
  Eq (α := Filter C(X, Y))
    (⨅ (s : Set C(X, Y)),
      ⨅ (_ :
        Membership.mem (γ := Set (Set C(X, Y)))
          {s : Set C(X, Y) |
            f ∈ s ∧
              Membership.mem (γ := Set (Set C(X, Y)))
                (image2 (fun (K : Set X) (U : Set Y) ↦ {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) K U})
                  {K : Set X | IsCompact K} {t : Set Y | IsOpen[inst_1] t})
                s}
          s),
        𝓟 s)
    (⨅ (K : Set X),
      ⨅ (_ : IsCompact K),
        ⨅ (U : Set Y),
          ⨅ (_ : IsOpen[inst_1] U),
            ⨅ (_ : MapsTo (⇑f : (a : X) → Y) K U), 𝓟 {g : C(X, Y) | MapsTo (⇑g : (a : X) → Y) K U})
simp_rw₂ :
  Eq (α := Filter C(X, Y))
    (⨅ (s : Set C(X, Y)),
      ⨅ (_ :
        f ∈ s ∧
          Membership.mem (γ := Set (Set C(X, Y)))
            (image2 (fun (K : Set X) (U : Set Y) ↦ {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) K U})
              {K : Set X | IsCompact K} {t : Set Y | IsOpen[inst_1] t})
            s),
        𝓟 s)
    (⨅ (K : Set X),
      ⨅ (_ : IsCompact K),
        ⨅ (U : Set Y),
          ⨅ (_ : IsOpen[inst_1] U),
            ⨅ (_ : MapsTo (⇑f : (a : X) → Y) K U), 𝓟 {g : C(X, Y) | MapsTo (⇑g : (a : X) → Y) K U})
simp_rw₃ :
  Eq (α := Filter C(X, Y))
    (⨅ (s : Set C(X, Y)),
      ⨅ (_ :
        Membership.mem (γ := Set (Set C(X, Y)))
            (image2 (fun (K : Set X) (U : Set Y) ↦ {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) K U})
              {K : Set X | IsCompact K} {t : Set Y | IsOpen[inst_1] t})
            s ∧
          f ∈ s),
        𝓟 s)
    (⨅ (K : Set X),
      ⨅ (_ : IsCompact K),
        ⨅ (U : Set Y),
          ⨅ (_ : IsOpen[inst_1] U),
            ⨅ (_ : MapsTo (⇑f : (a : X) → Y) K U), 𝓟 {g : C(X, Y) | MapsTo (⇑g : (a : X) → Y) K U})
⊢ 𝓝 f =
    ⨅ (K : Set X),
      ⨅ (_ : IsCompact K),
        ⨅ (U : Set Y),
          ⨅ (_ : IsOpen[inst_1] U),
            ⨅ (_ : MapsTo (⇑f : (a : X) → Y) K U), 𝓟 {g : C(X, Y) | MapsTo (⇑g : (a : X) → Y) K U}
have simp_rw₄ : Eq (α := Filter C(X, Y))
  (⨅ (s : Set C(X, Y)),
    ⨅ (_ :
      Membership.mem (γ := Set (Set C(X, Y)))
        (image2 (fun (K : Set X) (U : Set Y) ↦ {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) K U}) {K : Set X | IsCompact K}
          {t : Set Y | IsOpen[inst_1] t})
        s),
      ⨅ (_ : f ∈ s), 𝓟 s)
  (⨅ (K : Set X),
    ⨅ (_ : IsCompact K),
      ⨅ (U : Set Y),
        ⨅ (_ : IsOpen[inst_1] U),
          ⨅ (_ : MapsTo (⇑f : (a : X) → Y) K U), 𝓟 {g : C(X, Y) | MapsTo (⇑g : (a : X) → Y) K U})
Tactic: simp_rw +instances [compactOpen_eq, nhds_generateFrom, mem_setOf_eq, @and_comm (f ∈ _), iInf_and,
    ← image_prod, iInf_image, biInf_prod, mem_setOf_eq]