awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
ι : Type v
hι : Nonempty ι
t : ι → Set X
htd : Directed (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) t
htc : ∀ (i : ι), IsCompact (t i)
htcl : ∀ (i : ι), IsClosed[inst] (t i)
i₀ : ι := hι.some
htn : ∀ (i : ι), t i ≠ ∅
⊢ Directed (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) t ∧ ∀ (i : ι), (t i₀ ∩ t i).Nonempty
have htn₁ : ∀ (i : ι), (t i).Nonempty
Tactic: simp only [← nonempty_iff_ne_empty] at htn ⊢
Cleared hypotheses: htn
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
ι : Type v
hι : Nonempty ι
t : ι → Set X
htd : Directed (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) t
htc : ∀ (i : ι), IsCompact (t i)
htcl : ∀ (i : ι), IsClosed[inst] (t i)
i₀ : ι := hι.some
htn : ∀ (i : ι), (t i).Nonempty
⊢ Directed (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) t ∧ ∀ (i : ι), (t i₀ ∩ t i).Nonempty
have refine : ∀ (i : ι), (t i₀ ∩ t i).Nonempty
Tactic: refine ⟨htd, fun i => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
ι : Type v
hι : Nonempty ι
t : ι → Set X
htd : Directed (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) t
htc : ∀ (i : ι), IsCompact (t i)
htcl : ∀ (i : ι), IsClosed[inst] (t i)
i₀ : ι := hι.some
htn : ∀ (i : ι), (t i).Nonempty
i : ι
⊢ (t i₀ ∩ t i).Nonempty
have rcases : ∀ (j : ι) (hji₀ : t i₀ ⊇ t j) (hji : t i ⊇ t j), (t i₀ ∩ t i).Nonempty
Tactic: rcases htd i₀ i with ⟨j, hji₀, hji⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
S : Set (Set X)
hS : Nonempty.{u + 1} (↑S : Type u)
hSd : DirectedOn (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) S
hSn : ∀ U ∈ S, U.Nonempty
hSc : ∀ U ∈ S, IsCompact U
hScl : ∀ U ∈ S, IsClosed[inst] U
⊢ (⋂₀ S).Nonempty
have rw : Set.Nonempty.{u} (α := X) (⋂ (i : (↑S : Type u)), (↑i : Set X))
Tactic: rw [sInter_eq_iInter]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (hypothesis)
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
s : Set X
b : Set ι
c : ι → Set X
hs : IsCompact s
hc₁ : ∀ i ∈ b, IsOpen[inst] (c i)
hc₂ : s ⊆ ⋃ i ∈ b, c i
⊢ ∃ b' ⊆ b, b'.Finite ∧ s ⊆ ⋃ i ∈ b', c i
have hc₃ : ∀ (x : { a : ι // a ∈ b }), IsOpen[inst] (c (↑x : ι))
Tactic: simp only [Subtype.forall', biUnion_eq_iUnion] at hc₁ hc₂
Cleared hypotheses: hc₁, hc₂
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (hypothesis)
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
s : Set X
b : Set ι
c : ι → Set X
hs : IsCompact s
hc₁ : ∀ i ∈ b, IsOpen[inst] (c i)
hc₂ : s ⊆ ⋃ i ∈ b, c i
hc₃ : ∀ (x : { a : ι // a ∈ b }), IsOpen[inst] (c (↑x : ι))
⊢ ∃ b' ⊆ b, b'.Finite ∧ s ⊆ ⋃ i ∈ b', c i
have hc₄ : s ⊆ ⋃ (x : (↑b : Type u_1)), c (↑x : ι)
Tactic: simp only [Subtype.forall', biUnion_eq_iUnion] at hc₁ hc₂
Cleared hypotheses: hc₁, hc₂
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
s : Set X
b : Set ι
c : ι → Set X
hs : IsCompact s
hc₁ : ∀ (x : { a : ι // a ∈ b }), IsOpen[inst] (c (↑x : ι))
hc₂ : s ⊆ ⋃ (x : (↑b : Type u_1)), c (↑x : ι)
⊢ ∃ b' ⊆ b, b'.Finite ∧ s ⊆ ⋃ i ∈ b', c i
have rcases : ∀ (d : Finset (↑b : Type u_1)) (hd : s ⊆ ⋃ i ∈ d, c (↑i : ι)), ∃ b' ⊆ b, b'.Finite ∧ s ⊆ ⋃ i ∈ b', c i
Tactic: rcases hs.elim_finite_subcover (fun i => c i : b → Set X) hc₁ hc₂ with ⟨d, hd⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
s : Set X
b : Set ι
c : ι → Set X
hs : IsCompact s
hc₁ : ∀ (x : { a : ι // a ∈ b }), IsOpen[inst] (c (↑x : ι))
hc₂ : s ⊆ ⋃ (x : (↑b : Type u_1)), c (↑x : ι)
d : Finset (↑b : Type u_1)
hd : s ⊆ ⋃ i ∈ d, c (↑i : ι)
⊢ ∃ b' ⊆ b, b'.Finite ∧ s ⊆ ⋃ i ∈ b', c i
have refine_1 : Subtype.val (p := fun (x : ι) ↦ x ∈ b) '' (↑d : Set (↑b : Type u_1)) ⊆ b
Tactic: refine ⟨Subtype.val '' (d : Set b), ?_, d.finite_toSet.image _, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
s : Set X
b : Set ι
c : ι → Set X
hs : IsCompact s
hc₁ : ∀ (x : { a : ι // a ∈ b }), IsOpen[inst] (c (↑x : ι))
hc₂ : s ⊆ ⋃ (x : (↑b : Type u_1)), c (↑x : ι)
d : Finset (↑b : Type u_1)
hd : s ⊆ ⋃ i ∈ d, c (↑i : ι)
refine_1 : Subtype.val (p := fun (x : ι) ↦ x ∈ b) '' (↑d : Set (↑b : Type u_1)) ⊆ b
⊢ ∃ b' ⊆ b, b'.Finite ∧ s ⊆ ⋃ i ∈ b', c i
have refine_2 : s ⊆ ⋃ i ∈ Subtype.val (p := fun (x : ι) ↦ x ∈ b) '' (↑d : Set (↑b : Type u_1)), c i
Tactic: refine ⟨Subtype.val '' (d : Set b), ?_, d.finite_toSet.image _, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
s : Set X
b : Set ι
c : ι → Set X
hs : IsCompact s
hc₁ : ∀ (x : { a : ι // a ∈ b }), IsOpen[inst] (c (↑x : ι))
hc₂ : s ⊆ ⋃ (x : (↑b : Type u_1)), c (↑x : ι)
d : Finset (↑b : Type u_1)
hd : s ⊆ ⋃ i ∈ d, c (↑i : ι)
⊢ s ⊆ ⋃ i ∈ Subtype.val (p := fun (x : ι) ↦ x ∈ b) '' (↑d : Set (↑b : Type u_1)), c i
have refine_2 : s ⊆ ⋃ y ∈ (↑d : Set (↑b : Type u_1)), c (↑y : ι)
Tactic: rwa [biUnion_image]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
h :
  ∀ {ι : Type u} (U : ι → Set X),
    (∀ (i : ι), IsOpen[inst] (U i)) → s ⊆ ⋃ (i : ι), U i → ∃ (t : Finset ι), s ⊆ ⋃ i ∈ t, U i
f : Filter X
hf : f.NeBot
hfs : f ≤ 𝓟 s
⊢ ∃ x ∈ s, ClusterPt x f
have contrapose! : ∀ (h : ∀ (x : X) (_ : x ∈ s), ¬ClusterPt x f),
  ∃ (ι : Type u) (U : ι → Set X),
    (∀ (i : ι), IsOpen[inst] (U i)) ∧ s ⊆ ⋃ (i : ι), U i ∧ ∀ (t : Finset ι), ¬s ⊆ ⋃ i ∈ t, U i
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
f : Filter X
hf : f.NeBot
hfs : f ≤ 𝓟 s
h : ∀ (x : X) (_ : x ∈ s), ¬ClusterPt x f
⊢ ∃ (ι : Type u) (U : ι → Set X),
    (∀ (i : ι), IsOpen[inst] (U i)) ∧ s ⊆ ⋃ (i : ι), U i ∧ ∀ (t : Finset ι), ¬s ⊆ ⋃ i ∈ t, U i
have h₁ : ∀ (x : (↑s : Type u)), ∃ (i : Set X), ((↑x : X) ∈ i ∧ IsOpen[inst] i) ∧ iᶜ ∈ f
Tactic: simp only [ClusterPt, not_neBot, ← disjoint_iff, SetCoe.forall',
    (nhds_basis_opens _).disjoint_iff_left] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
f : Filter X
hf : f.NeBot
hfs : f ≤ 𝓟 s
h : ∀ (x : (↑s : Type u)), ∃ (i : Set X), ((↑x : X) ∈ i ∧ IsOpen[inst] i) ∧ iᶜ ∈ f
⊢ ∃ (ι : Type u) (U : ι → Set X),
    (∀ (i : ι), IsOpen[inst] (U i)) ∧ s ⊆ ⋃ (i : ι), U i ∧ ∀ (t : Finset ι), ¬s ⊆ ⋃ i ∈ t, U i
have choose : ∀ (U : (x : (↑s : Type u)) → Set X) (hU : ∀ (x : (↑s : Type u)), (↑x : X) ∈ U x ∧ IsOpen[inst] (U x))
  (hUf : ∀ (x : (↑s : Type u)), (U x)ᶜ ∈ f),
  ∃ (ι : Type u) (U : ι → Set X),
    (∀ (i : ι), IsOpen[inst] (U i)) ∧ s ⊆ ⋃ (i : ι), U i ∧ ∀ (t : Finset ι), ¬s ⊆ ⋃ i ∈ t, U i
Tactic: choose U hU hUf using h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
f : Filter X
hf : f.NeBot
hfs : f ≤ 𝓟 s
U : (x : (↑s : Type u)) → Set X
hU : ∀ (x : (↑s : Type u)), (↑x : X) ∈ U x ∧ IsOpen[inst] (U x)
hUf : ∀ (x : (↑s : Type u)), (U x)ᶜ ∈ f
⊢ ∃ (ι : Type u) (U : ι → Set X),
    (∀ (i : ι), IsOpen[inst] (U i)) ∧ s ⊆ ⋃ (i : ι), U i ∧ ∀ (t : Finset ι), ¬s ⊆ ⋃ i ∈ t, U i
have refine : ∀ (t : Finset (↑s : Type u)) (ht : s ⊆ ⋃ i ∈ t, U i), False
Tactic: refine ⟨s, U, fun x => (hU x).2, fun x hx => mem_iUnion.2 ⟨⟨x, hx⟩, (hU _).1⟩, fun t ht => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
f : Filter X
hf : f.NeBot
hfs : f ≤ 𝓟 s
U : (x : (↑s : Type u)) → Set X
hU : ∀ (x : (↑s : Type u)), (↑x : X) ∈ U x ∧ IsOpen[inst] (U x)
hUf : ∀ (x : (↑s : Type u)), (U x)ᶜ ∈ f
t : Finset (↑s : Type u)
ht : s ⊆ ⋃ i ∈ t, U i
⊢ False
have refine : sᶜ ∈ f
Tactic: refine compl_notMem (le_principal_iff.1 hfs) ?_
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
f : Filter X
hf : f.NeBot
hfs : f ≤ 𝓟 s
U : (x : (↑s : Type u)) → Set X
hU : ∀ (x : (↑s : Type u)), (↑x : X) ∈ U x ∧ IsOpen[inst] (U x)
hUf : ∀ (x : (↑s : Type u)), (U x)ᶜ ∈ f
t : Finset (↑s : Type u)
ht : s ⊆ ⋃ i ∈ t, U i
⊢ sᶜ ∈ f
have refine : ⋂ i ∈ t, (U i)ᶜ ⊆ sᶜ
Tactic: refine mem_of_superset ((biInter_finset_mem t).2 fun x _ => hUf x) ?_
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
f : Filter X
hf : f.NeBot
hfs : f ≤ 𝓟 s
U : (x : (↑s : Type u)) → Set X
hU : ∀ (x : (↑s : Type u)), (↑x : X) ∈ U x ∧ IsOpen[inst] (U x)
hUf : ∀ (x : (↑s : Type u)), (U x)ᶜ ∈ f
t : Finset (↑s : Type u)
ht : s ⊆ ⋃ i ∈ t, U i
⊢ ⋂ i ∈ t, (U i)ᶜ ⊆ sᶜ
have rw : s ⊆ ⋃ i ∈ t, (U i)ᶜᶜ
Tactic: rw [subset_compl_comm, compl_iInter₂]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
h :
  ∀ {ι : Type u} (t : ι → Set X),
    (∀ (i : ι), IsClosed[inst] (t i)) → s ∩ ⋂ (i : ι), t i = ∅ → ∃ (u : Finset ι), s ∩ ⋂ i ∈ u, t i = ∅
ι : Type u
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊆ ⋃ (i : ι), U i
⊢ ∃ (t : Finset ι), s ⊆ ⋃ i ∈ t, U i
have hsU₁ : s ⊓ ⋂ (i : ι), (U i)ᶜ = ⊥
Tactic: rw [← disjoint_compl_right_iff_subset, compl_iUnion, disjoint_iff] at hsU
Cleared hypotheses: hsU
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
h :
  ∀ {ι : Type u} (t : ι → Set X),
    (∀ (i : ι), IsClosed[inst] (t i)) → s ∩ ⋂ (i : ι), t i = ∅ → ∃ (u : Finset ι), s ∩ ⋂ i ∈ u, t i = ∅
ι : Type u
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊓ ⋂ (i : ι), (U i)ᶜ = ⊥
⊢ ∃ (t : Finset ι), s ⊆ ⋃ i ∈ t, U i
have rcases : ∀ (t : Finset ι) (ht : s ∩ ⋂ i ∈ t, (U i)ᶜ = ∅), ∃ (t : Finset ι), s ⊆ ⋃ i ∈ t, U i
Tactic: rcases h (fun i => (U i)ᶜ) (fun i => (hUo _).isClosed_compl) hsU with ⟨t, ht⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
h :
  ∀ {ι : Type u} (t : ι → Set X),
    (∀ (i : ι), IsClosed[inst] (t i)) → s ∩ ⋂ (i : ι), t i = ∅ → ∃ (u : Finset ι), s ∩ ⋂ i ∈ u, t i = ∅
ι : Type u
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊓ ⋂ (i : ι), (U i)ᶜ = ⊥
t : Finset ι
ht : s ∩ ⋂ i ∈ t, (U i)ᶜ = ∅
⊢ ∃ (t : Finset ι), s ⊆ ⋃ i ∈ t, U i
have refine : s ⊆ ⋃ i ∈ t, U i
Tactic: refine ⟨t, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
h :
  ∀ {ι : Type u} (t : ι → Set X),
    (∀ (i : ι), IsClosed[inst] (t i)) → s ∩ ⋂ (i : ι), t i = ∅ → ∃ (u : Finset ι), s ∩ ⋂ i ∈ u, t i = ∅
ι : Type u
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊓ ⋂ (i : ι), (U i)ᶜ = ⊥
t : Finset ι
ht : s ∩ ⋂ i ∈ t, (U i)ᶜ = ∅
⊢ s ⊆ ⋃ i ∈ t, U i
have rwa : Disjoint s (⋃ i ∈ t, U i)ᶜ
Tactic: rwa [← disjoint_compl_right_iff_subset, compl_iUnion₂, disjoint_iff]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
h :
  ∀ {ι : Type u} (t : ι → Set X),
    (∀ (i : ι), IsClosed[inst] (t i)) → s ∩ ⋂ (i : ι), t i = ∅ → ∃ (u : Finset ι), s ∩ ⋂ i ∈ u, t i = ∅
ι : Type u
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊓ ⋂ (i : ι), (U i)ᶜ = ⊥
t : Finset ι
ht : s ∩ ⋂ i ∈ t, (U i)ᶜ = ∅
rwa : Disjoint s (⋃ i ∈ t, U i)ᶜ
⊢ s ⊆ ⋃ i ∈ t, U i
have rwa₁ : Disjoint s (⋂ i ∈ t, (U i)ᶜ)
Tactic: rwa [← disjoint_compl_right_iff_subset, compl_iUnion₂, disjoint_iff]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
h :
  ∀ {ι : Type u} (t : ι → Set X),
    (∀ (i : ι), IsClosed[inst] (t i)) → s ∩ ⋂ (i : ι), t i = ∅ → ∃ (u : Finset ι), s ∩ ⋂ i ∈ u, t i = ∅
ι : Type u
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊓ ⋂ (i : ι), (U i)ᶜ = ⊥
t : Finset ι
ht : s ∩ ⋂ i ∈ t, (U i)ᶜ = ∅
rwa : Disjoint s (⋃ i ∈ t, U i)ᶜ
rwa₁ : Disjoint s (⋂ i ∈ t, (U i)ᶜ)
⊢ s ⊆ ⋃ i ∈ t, U i
have rwa₂ : s ⊓ ⋂ i ∈ t, (U i)ᶜ = ⊥
Tactic: rwa [← disjoint_compl_right_iff_subset, compl_iUnion₂, disjoint_iff]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
K : Set X
Y : Type u_2
l : Filter Y
s : Set (X × Y)
hK : IsCompact K
hs : ∀ x ∈ K, s ∈ 𝓝 x ×ˢ l
⊢ s ∈ 𝓝ˢ K ×ˢ l
have refine_1 : ∀ (t t' : Set X) (ht : t ⊆ t') (hs : s ∈ 𝓝ˢ t' ×ˢ l), s ∈ 𝓝ˢ t ×ˢ l
Tactic: refine hK.induction_on (by simp) (fun t t' ht hs ↦ ?_) (fun t t' ht ht' ↦ ?_) fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
K : Set X
Y : Type u_2
l : Filter Y
s : Set (X × Y)
hK : IsCompact K
hs : ∀ x ∈ K, s ∈ 𝓝 x ×ˢ l
refine_1 : ∀ (t t' : Set X) (ht : t ⊆ t') (hs : s ∈ 𝓝ˢ t' ×ˢ l), s ∈ 𝓝ˢ t ×ˢ l
⊢ s ∈ 𝓝ˢ K ×ˢ l
have refine_2 : ∀ (t t' : Set X) (ht : s ∈ 𝓝ˢ t ×ˢ l) (ht' : s ∈ 𝓝ˢ t' ×ˢ l), s ∈ 𝓝ˢ (t ∪ t') ×ˢ l
Tactic: refine hK.induction_on (by simp) (fun t t' ht hs ↦ ?_) (fun t t' ht ht' ↦ ?_) fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
K : Set X
Y : Type u_2
l : Filter Y
s : Set (X × Y)
hK : IsCompact K
hs : ∀ x ∈ K, s ∈ 𝓝 x ×ˢ l
refine_1 : ∀ (t t' : Set X) (ht : t ⊆ t') (hs : s ∈ 𝓝ˢ t' ×ˢ l), s ∈ 𝓝ˢ t ×ˢ l
refine_2 : ∀ (t t' : Set X) (ht : s ∈ 𝓝ˢ t ×ˢ l) (ht' : s ∈ 𝓝ˢ t' ×ˢ l), s ∈ 𝓝ˢ (t ∪ t') ×ˢ l
⊢ s ∈ 𝓝ˢ K ×ˢ l
have refine_3 : ∀ (x : X) (hx : x ∈ K), ∃ t ∈ 𝓝[K] x, s ∈ 𝓝ˢ t ×ˢ l
Tactic: refine hK.induction_on (by simp) (fun t t' ht hs ↦ ?_) (fun t t' ht ht' ↦ ?_) fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
K : Set X
Y : Type u_2
l : Filter Y
s : Set (X × Y)
hK : IsCompact K
hs : ∀ x ∈ K, s ∈ 𝓝 x ×ˢ l
x : X
hx : x ∈ K
⊢ ∃ t ∈ 𝓝[K] x, s ∈ 𝓝ˢ t ×ˢ l
have refine_3 : ∀ (u : Set X) (v : Set Y) (hs : (u, v).1 ×ˢ id (u, v).2 ⊆ s) (hv : (u, v).2 ∈ l) (hx : x ∈ (u, v).1)
  (huo : IsOpen[inst] (u, v).1), ∃ t ∈ 𝓝[K] x, s ∈ 𝓝ˢ t ×ˢ l
Tactic: rcases ((nhds_basis_opens _).prod l.basis_sets).mem_iff.1 (hs x hx)
      with ⟨⟨u, v⟩, ⟨⟨hx, huo⟩, hv⟩, hs⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
K : Set X
Y : Type u_2
l : Filter Y
s : Set (X × Y)
hK : IsCompact K
hs_1 : ∀ x ∈ K, s ∈ 𝓝 x ×ˢ l
x : X
hx_1 : x ∈ K
u : Set X
v : Set Y
hs : (u, v).1 ×ˢ id (u, v).2 ⊆ s
hv : (u, v).2 ∈ l
hx : x ∈ (u, v).1
huo : IsOpen[inst] (u, v).1
⊢ ∃ t ∈ 𝓝[K] x, s ∈ 𝓝ˢ t ×ˢ l
have refine_3 : (u, v).1 ×ˢ id (u, v).2 ∈ 𝓝ˢ u ×ˢ l
Tactic: refine ⟨u, nhdsWithin_le_nhds (huo.mem_nhds hx), mem_of_superset ?_ hs⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
K : Set X
hK : IsCompact K
l : Filter X
⊢ 𝓝ˢ K ⊓ l = ⨆ x ∈ K, 𝓝 x ⊓ l
have this : ∀ (f : Filter X), f ⊓ l = comap (fun (x : X) ↦ (x, x)) (f ×ˢ l)
Tactic: have : ∀ f : Filter X, f ⊓ l = comap (fun x ↦ (x, x)) (f ×ˢ l) := fun f ↦ by
    simpa only [comap_prod] using congrArg₂ (· ⊓ ·) comap_id.symm comap_id.symm
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
K : Set X
hK : IsCompact K
l : Filter X
this : ∀ (f : Filter X), f ⊓ l = comap (fun (x : X) ↦ (x, x)) (f ×ˢ l)
⊢ 𝓝ˢ K ⊓ l = ⨆ x ∈ K, 𝓝 x ⊓ l
have simp_rw : Eq (α := Filter X) (comap (fun (x : X) ↦ (x, x)) (𝓝ˢ K ×ˢ l)) (⨆ x ∈ K, comap (fun (x : X) ↦ (x, x)) (𝓝 x ×ˢ l))
Tactic: simp_rw [this, ← comap_iSup, hK.nhdsSet_prod_eq_biSup]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
K : Set X
hK : IsCompact K
l : Filter X
this : ∀ (f : Filter X), f ⊓ l = comap (fun (x : X) ↦ (x, x)) (f ×ˢ l)
simp_rw :
  Eq (α := Filter X) (comap (fun (x : X) ↦ (x, x)) (𝓝ˢ K ×ˢ l)) (⨆ x ∈ K, comap (fun (x : X) ↦ (x, x)) (𝓝 x ×ˢ l))
⊢ 𝓝ˢ K ⊓ l = ⨆ x ∈ K, 𝓝 x ⊓ l
have simp_rw₁ : Eq (α := Filter X) (comap (fun (x : X) ↦ (x, x)) (𝓝ˢ K ×ˢ l))
  (comap (β := X × X) (fun (x : X) ↦ (x, x)) (⨆ i ∈ K, 𝓝 i ×ˢ l))
Tactic: simp_rw [this, ← comap_iSup, hK.nhdsSet_prod_eq_biSup]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (hypothesis)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ : X
K : Set Y
hK : IsCompact K
P : X → Y → Prop
hP : ∀ y ∈ K, ∀ᶠ (z : X × Y) in 𝓝 (x₀, y), P z.1 z.2
⊢ ∀ᶠ (x : X) in 𝓝 x₀, ∀ y ∈ K, P x y
have hP₁ : ∀ᶠ (z : X × Y) in 𝓝 x₀ ×ˢ 𝓝ˢ K, P z.1 z.2
Tactic: simp only [nhds_prod_eq, ← eventually_iSup, ← hK.prod_nhdsSet_eq_biSup] at hP
Cleared hypotheses: hP
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (hypothesis)
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Finite
hf : ∀ i ∈ s, IsCompact (f i)
l : Ultrafilter X
hl : ⋃ i ∈ s, f i ∈ l
⊢ ∃ (x : X), Membership.mem (γ := Set X) (⋃ i ∈ s, f i) x ∧ (↑l : Filter X) ≤ 𝓝 x
have hl₁ : ∃ i ∈ s, f i ∈ l
Tactic: rw [Ultrafilter.finite_biUnion_mem_iff hs] at hl
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Finite
hf : ∀ i ∈ s, IsCompact (f i)
l : Ultrafilter X
hl : ∃ i ∈ s, f i ∈ l
⊢ ∃ (x : X), Membership.mem (γ := Set X) (⋃ i ∈ s, f i) x ∧ (↑l : Filter X) ≤ 𝓝 x
have rcases : ∀ (i : ι) (his : i ∈ s) (hi : f i ∈ l), ∃ (x : X), Membership.mem (γ := Set X) (⋃ i ∈ s, f i) x ∧ (↑l : Filter X) ≤ 𝓝 x
Tactic: rcases hl with ⟨i, his, hi⟩
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Finite
hf : ∀ i ∈ s, IsCompact (f i)
l : Ultrafilter X
i : ι
his : i ∈ s
hi : f i ∈ l
⊢ ∃ (x : X), Membership.mem (γ := Set X) (⋃ i ∈ s, f i) x ∧ (↑l : Filter X) ≤ 𝓝 x
have rcases : ∀ (x : X) (hxi : x ∈ f i) (hlx : (↑l : Filter X) ≤ 𝓝 x),
  ∃ (x : X), Membership.mem (γ := Set X) (⋃ i ∈ s, f i) x ∧ (↑l : Filter X) ≤ 𝓝 x
Tactic: rcases (hf i his).ultrafilter_le_nhds _ (le_principal_iff.2 hi) with ⟨x, hxi, hlx⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
S : Set (Set X)
hf : S.Finite
hc : ∀ s ∈ S, IsCompact s
⊢ IsCompact (⋃₀ S)
have rw : IsCompact.{u} (X := X) (⋃ i ∈ S, i)
Tactic: rw [sUnion_eq_biUnion]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
inst_1 : DiscreteTopology X
hs : IsCompact s
⊢ s.Finite
have this : ∀ (x : X), {x} ∈ 𝓝 x
Tactic: have : ∀ x : X, ({x} : Set X) ∈ 𝓝 x := by simp [nhds_discrete]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
inst_1 : DiscreteTopology X
hs : IsCompact s
this : ∀ (x : X), {x} ∈ 𝓝 x
⊢ s.Finite
have rcases : ∀ (t : Finset X), (∀ x ∈ t, x ∈ s) → ∀ (hst : s ⊆ ⋃ x ∈ t, {x}), s.Finite
Tactic: rcases hs.elim_nhds_subcover (fun x => {x}) fun x _ => this x with ⟨t, _, hst⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
inst_1 : DiscreteTopology X
hs : IsCompact s
this : ∀ (x : X), {x} ∈ 𝓝 x
t : Finset X
left : ∀ x ∈ t, x ∈ s
hst : s ⊆ ⋃ x ∈ t, {x}
⊢ s.Finite
have hst₁ : s ⊆ (↑t : Set X)
Tactic: simp only [← t.set_biUnion_coe, biUnion_of_singleton] at hst
Cleared hypotheses: hst
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hs : IsCompact s
ht : IsCompact t
⊢ IsCompact (s ∪ t)
have rw : IsCompact.{u} (X := X) (⋃ (b : Bool), bif b then s else t)
Tactic: rw [union_eq_iUnion]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hs : IsCompact s
ht : IsCompact t
b : Bool
⊢ IsCompact (bif b then s else t)
have false : IsCompact (bif false then s else t)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hs : IsCompact s
ht : IsCompact t
b : Bool
false : IsCompact (bif Bool.false then s else t)
⊢ IsCompact (bif b then s else t)
have true : IsCompact (bif true then s else t)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
inst_1 : Nonempty ι
V : ι → Set X
hV : Directed (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed[inst] (V i)
U : Set X
hU : ∀ (x : X), Membership.mem (γ := Set X) (⋂ (i : ι), V i) x → U ∈ 𝓝 x
⊢ ∃ (i : ι), V i ⊆ U
have obtain : ∀ (W : Set X) (hsubW : ⋂ (i : ι), V i ⊆ W) (W_op : IsOpen[inst] W) (hWU : W ⊆ U), ∃ (i : ι), V i ⊆ U
Tactic: obtain ⟨W, hsubW, W_op, hWU⟩ := exists_open_set_nhds hU
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
inst_1 : Nonempty ι
V : ι → Set X
hV : Directed (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed[inst] (V i)
U : Set X
hU : ∀ (x : X), Membership.mem (γ := Set X) (⋂ (i : ι), V i) x → U ∈ 𝓝 x
W : Set X
hsubW : ⋂ (i : ι), V i ⊆ W
W_op : IsOpen[inst] W
hWU : W ⊆ U
⊢ ∃ (i : ι), V i ⊆ U
have suffices : ∃ (i : ι), V i ⊆ W
Tactic: suffices ∃ i, V i ⊆ W from this.imp fun i hi => hi.trans hWU
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
inst_1 : Nonempty ι
V : ι → Set X
hV : Directed (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed[inst] (V i)
U : Set X
hU : ∀ (x : X), Membership.mem (γ := Set X) (⋂ (i : ι), V i) x → U ∈ 𝓝 x
W : Set X
hsubW : ⋂ (i : ι), V i ⊆ W
W_op : IsOpen[inst] W
hWU : W ⊆ U
⊢ ∃ (i : ι), V i ⊆ W
have by_contra! : ∀ (H : ∀ (i : ι), ¬V i ⊆ W), False
Tactic: by_contra! H
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (hypothesis)
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
inst_1 : Nonempty ι
V : ι → Set X
hV : Directed (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed[inst] (V i)
U : Set X
hU : ∀ (x : X), Membership.mem (γ := Set X) (⋂ (i : ι), V i) x → U ∈ 𝓝 x
W : Set X
hsubW : ⋂ (i : ι), V i ⊆ W
W_op : IsOpen[inst] W
hWU : W ⊆ U
H : ∀ (i : ι), ¬V i ⊆ W
⊢ False
have H₁ : ∀ (i : ι), (V i ∩ Wᶜ).Nonempty
Tactic: replace H : ∀ i, (V i ∩ Wᶜ).Nonempty := fun i => Set.inter_compl_nonempty_iff.mpr (H i)
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
inst_1 : Nonempty ι
V : ι → Set X
hV : Directed (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed[inst] (V i)
U : Set X
hU : ∀ (x : X), Membership.mem (γ := Set X) (⋂ (i : ι), V i) x → U ∈ 𝓝 x
W : Set X
hsubW : ⋂ (i : ι), V i ⊆ W
W_op : IsOpen[inst] W
hWU : W ⊆ U
H : ∀ (i : ι), (V i ∩ Wᶜ).Nonempty
⊢ Set.Nonempty.{u} (α := X) (⋂ (i : ι), V i ∩ Wᶜ)
have _ : ∀ (i j : ι),
  ∃ (z : ι),
    (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) (V i ∩ Wᶜ) (V z ∩ Wᶜ) ∧ (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) (V j ∩ Wᶜ) (V z ∩ Wᶜ)
Tactic: refine
      IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed _ (fun i j => ?_) H
        (fun i => (hV_cpct i).inter_right W_op.isClosed_compl) fun i =>
        (hV_closed i).inter W_op.isClosed_compl
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
inst_1 : Nonempty ι
V : ι → Set X
hV : Directed (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed[inst] (V i)
U : Set X
hU : ∀ (x : X), Membership.mem (γ := Set X) (⋂ (i : ι), V i) x → U ∈ 𝓝 x
W : Set X
hsubW : ⋂ (i : ι), V i ⊆ W
W_op : IsOpen[inst] W
hWU : W ⊆ U
H : ∀ (i : ι), (V i ∩ Wᶜ).Nonempty
i j : ι
⊢ ∃ (z : ι),
    (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) (V i ∩ Wᶜ) (V z ∩ Wᶜ) ∧ (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) (V j ∩ Wᶜ) (V z ∩ Wᶜ)
have rcases : ∀ (k : ι) (hki : V i ⊇ V k) (hkj : V j ⊇ V k),
  ∃ (z : ι),
    (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) (V i ∩ Wᶜ) (V z ∩ Wᶜ) ∧ (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) (V j ∩ Wᶜ) (V z ∩ Wᶜ)
Tactic: rcases hV i j with ⟨k, hki, hkj⟩