awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
t : Set Y
hs : IsCompact s
ht : IsCompact t
⊢ 𝓝ˢ (s ×ˢ t) = 𝓝ˢ s ×ˢ 𝓝ˢ t
have simp_rw : 𝓝ˢ (s ×ˢ t) = ⨆ x ∈ s, 𝓝 x ×ˢ 𝓝ˢ t
Tactic: simp_rw [hs.nhdsSet_prod_eq_biSup, ht.prod_nhdsSet_eq_biSup, nhdsSet, sSup_image, biSup_prod,
    nhds_prod_eq]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
t : Set Y
hs : IsCompact s
ht : IsCompact t
simp_rw : 𝓝ˢ (s ×ˢ t) = ⨆ x ∈ s, 𝓝 x ×ˢ 𝓝ˢ t
⊢ 𝓝ˢ (s ×ˢ t) = 𝓝ˢ s ×ˢ 𝓝ˢ t
have simp_rw₁ : 𝓝ˢ (s ×ˢ t) = ⨆ x ∈ s, ⨆ y ∈ t, 𝓝 x ×ˢ 𝓝 y
Tactic: simp_rw [hs.nhdsSet_prod_eq_biSup, ht.prod_nhdsSet_eq_biSup, nhdsSet, sSup_image, biSup_prod,
    nhds_prod_eq]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
t : Set Y
hs : IsCompact s
ht : IsCompact t
simp_rw : 𝓝ˢ (s ×ˢ t) = ⨆ x ∈ s, 𝓝 x ×ˢ 𝓝ˢ t
simp_rw₁ : 𝓝ˢ (s ×ˢ t) = ⨆ x ∈ s, ⨆ y ∈ t, 𝓝 x ×ˢ 𝓝 y
⊢ 𝓝ˢ (s ×ˢ t) = 𝓝ˢ s ×ˢ 𝓝ˢ t
have simp_rw₂ : sSup (𝓝 '' s ×ˢ t) = ⨆ x ∈ s, ⨆ y ∈ t, 𝓝 x ×ˢ 𝓝 y
Tactic: simp_rw [hs.nhdsSet_prod_eq_biSup, ht.prod_nhdsSet_eq_biSup, nhdsSet, sSup_image, biSup_prod,
    nhds_prod_eq]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
t : Set Y
hs : IsCompact s
ht : IsCompact t
simp_rw : 𝓝ˢ (s ×ˢ t) = ⨆ x ∈ s, 𝓝 x ×ˢ 𝓝ˢ t
simp_rw₁ : 𝓝ˢ (s ×ˢ t) = ⨆ x ∈ s, ⨆ y ∈ t, 𝓝 x ×ˢ 𝓝 y
simp_rw₂ : sSup (𝓝 '' s ×ˢ t) = ⨆ x ∈ s, ⨆ y ∈ t, 𝓝 x ×ˢ 𝓝 y
⊢ 𝓝ˢ (s ×ˢ t) = 𝓝ˢ s ×ˢ 𝓝ˢ t
have simp_rw₃ : Eq (α := Filter (X × Y)) (⨆ a ∈ s ×ˢ t, 𝓝 a) (⨆ x ∈ s, ⨆ y ∈ t, 𝓝 x ×ˢ 𝓝 y)
Tactic: simp_rw [hs.nhdsSet_prod_eq_biSup, ht.prod_nhdsSet_eq_biSup, nhdsSet, sSup_image, biSup_prod,
    nhds_prod_eq]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
t : Set Y
hs : IsCompact s
ht : IsCompact t
simp_rw : 𝓝ˢ (s ×ˢ t) = ⨆ x ∈ s, 𝓝 x ×ˢ 𝓝ˢ t
simp_rw₁ : 𝓝ˢ (s ×ˢ t) = ⨆ x ∈ s, ⨆ y ∈ t, 𝓝 x ×ˢ 𝓝 y
simp_rw₂ : sSup (𝓝 '' s ×ˢ t) = ⨆ x ∈ s, ⨆ y ∈ t, 𝓝 x ×ˢ 𝓝 y
simp_rw₃ : Eq (α := Filter (X × Y)) (⨆ a ∈ s ×ˢ t, 𝓝 a) (⨆ x ∈ s, ⨆ y ∈ t, 𝓝 x ×ˢ 𝓝 y)
⊢ 𝓝ˢ (s ×ˢ t) = 𝓝ˢ s ×ˢ 𝓝ˢ t
have simp_rw₄ : Eq (α := Filter (X × Y)) (⨆ a ∈ s, ⨆ b ∈ t, 𝓝 (a, b)) (⨆ x ∈ s, ⨆ y ∈ t, 𝓝 x ×ˢ 𝓝 y)
Tactic: simp_rw [hs.nhdsSet_prod_eq_biSup, ht.prod_nhdsSet_eq_biSup, nhdsSet, sSup_image, biSup_prod,
    nhds_prod_eq]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : Filter Y
hs : IsCompact s
hf : Disjoint f (cocompact Y)
⊢ 𝓝ˢ s ×ˢ f ≤ 𝓝ˢ (SProd.sprod (β := Set Y) s univ)
have obtain : ∀ (K : Set Y) (hKf : K ∈ f) (hK : IsCompact K), 𝓝ˢ s ×ˢ f ≤ 𝓝ˢ (SProd.sprod (β := Set Y) s univ)
Tactic: obtain ⟨K, hKf, hK⟩ := (disjoint_cocompact_right f).mp hf
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
t : Set Y
f : Filter X
ht : IsCompact t
hf : Disjoint f (cocompact X)
⊢ f ×ˢ 𝓝ˢ t ≤ 𝓝ˢ (SProd.sprod (α := Set X) univ t)
have obtain : ∀ (K : Set X) (hKf : K ∈ f) (hK : IsCompact K), f ×ˢ 𝓝ˢ t ≤ 𝓝ˢ (SProd.sprod (α := Set X) univ t)
Tactic: obtain ⟨K, hKf, hK⟩ := (disjoint_cocompact_right f).mp hf
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (hypothesis)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
hs : IsCompact s
t : Set Y
ht : IsCompact t
n : Set (X × Y)
hn : IsOpen[instTopologicalSpaceProd] n
hp : s ×ˢ t ⊆ n
⊢ ∃ (u : Set X) (v : Set Y), IsOpen[inst] u ∧ IsOpen[inst_1] v ∧ s ⊆ u ∧ t ⊆ v ∧ u ×ˢ v ⊆ n
have hp₁ : ∃ (i : Prod.{u, v} (Set X) (Set Y)), ((IsOpen[inst] i.1 ∧ s ⊆ i.1) ∧ IsOpen[inst_1] i.2 ∧ t ⊆ i.2) ∧ i.1 ×ˢ i.2 ⊆ n
Tactic: rw [← hn.mem_nhdsSet, hs.nhdsSet_prod_eq ht,
    ((hasBasis_nhdsSet _).prod (hasBasis_nhdsSet _)).mem_iff] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
hs : IsCompact s
t : Set Y
ht : IsCompact t
n : Set (X × Y)
hn : IsOpen[instTopologicalSpaceProd] n
hp : ∃ (i : Prod.{u, v} (Set X) (Set Y)), ((IsOpen[inst] i.1 ∧ s ⊆ i.1) ∧ IsOpen[inst_1] i.2 ∧ t ⊆ i.2) ∧ i.1 ×ˢ i.2 ⊆ n
⊢ ∃ (u : Set X) (v : Set Y), IsOpen[inst] u ∧ IsOpen[inst_1] v ∧ s ⊆ u ∧ t ⊆ v ∧ u ×ˢ v ⊆ n
have rcases : ∀ (u : Set X) (v : Set Y) (hn : (u, v).1 ×ˢ (u, v).2 ⊆ n) (huo : IsOpen[inst] (u, v).1) (hsu : s ⊆ (u, v).1)
  (hvo : IsOpen[inst_1] (u, v).2) (htv : t ⊆ (u, v).2),
  ∃ (u : Set X) (v : Set Y), IsOpen[inst] u ∧ IsOpen[inst_1] v ∧ s ⊆ u ∧ t ⊆ v ∧ u ×ˢ v ⊆ n
Tactic: rcases hp with ⟨⟨u, v⟩, ⟨⟨huo, hsu⟩, hvo, htv⟩, hn⟩
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s s' : Set X
hs : IsCompact s
t t' : Set Y
ht : IsCompact t
n : Set (X × Y)
hn : n ∈ 𝓝ˢ[s' ×ˢ t'] (s ×ˢ t)
⊢ ∃ u ∈ 𝓝ˢ[s'] s, ∃ v ∈ 𝓝ˢ[t'] t, u ×ˢ v ⊆ n
have rwa : ∀ (hn : n ∈ 𝓝ˢ[s'] s ×ˢ 𝓝ˢ[t'] t), ∃ u ∈ 𝓝ˢ[s'] s, ∃ v ∈ 𝓝ˢ[t'] t, u ×ˢ v ⊆ n
Tactic: rwa [hs.nhdsSetWithin_prod_eq ht, Filter.mem_prod_iff] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s s' : Set X
hs : IsCompact s
t t' : Set Y
ht : IsCompact t
n : Set (X × Y)
hn : n ∈ 𝓝ˢ[s' ×ˢ t'] (s ×ˢ t)
rwa : ∀ (hn : n ∈ 𝓝ˢ[s'] s ×ˢ 𝓝ˢ[t'] t), ∃ u ∈ 𝓝ˢ[s'] s, ∃ v ∈ 𝓝ˢ[t'] t, u ×ˢ v ⊆ n
⊢ ∃ u ∈ 𝓝ˢ[s'] s, ∃ v ∈ 𝓝ˢ[t'] t, u ×ˢ v ⊆ n
have rwa₁ : ∀ (hn : ∃ t₁ ∈ 𝓝ˢ[s'] s, ∃ t₂ ∈ 𝓝ˢ[t'] t, t₁ ×ˢ t₂ ⊆ n), ∃ u ∈ 𝓝ˢ[s'] s, ∃ v ∈ 𝓝ˢ[t'] t, u ×ˢ v ⊆ n
Tactic: rwa [hs.nhdsSetWithin_prod_eq ht, Filter.mem_prod_iff] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (hypothesis)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s s' : Set X
hs : IsCompact s
t : Set Y
ht : IsCompact t
n : Set (X × Y)
hn : n ∈ 𝓝ˢ[s' ×ˢ t] (s ×ˢ t)
⊢ ∃ u ∈ 𝓝ˢ[s'] s, u ×ˢ t ⊆ n
have hn₁ : {a : X | ∀ b ∈ t, (a, b) ∈ n} ∈ 𝓝ˢ[s'] s
Tactic: rw [hs.nhdsSetWithin_prod_eq ht, nhdsSetWithin_self, Filter.mem_prod_principal] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (hypothesis)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
hs : IsCompact s
t t' : Set Y
ht : IsCompact t
n : Set (X × Y)
hn : n ∈ 𝓝ˢ[s ×ˢ t'] (s ×ˢ t)
⊢ ∃ u ∈ 𝓝ˢ[t'] t, s ×ˢ u ⊆ n
have hn₁ : ∃ t₁ ∈ 𝓟 s, ∃ t₂ ∈ 𝓝ˢ[t'] t, t₁ ×ˢ t₂ ⊆ n
Tactic: rw [hs.nhdsSetWithin_prod_eq ht, nhdsSetWithin_self, Filter.mem_prod_iff] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
hs : IsCompact s
t t' : Set Y
ht : IsCompact t
n : Set (X × Y)
hn : ∃ t₁ ∈ 𝓟 s, ∃ t₂ ∈ 𝓝ˢ[t'] t, t₁ ×ˢ t₂ ⊆ n
⊢ ∃ u ∈ 𝓝ˢ[t'] t, s ×ˢ u ⊆ n
have obtain : ∀ (s' : Set X) (hs' : s' ∈ 𝓟 s) (u : Set Y) (hu : u ∈ 𝓝ˢ[t'] t) (h : s' ×ˢ u ⊆ n), ∃ u ∈ 𝓝ˢ[t'] t, s ×ˢ u ⊆ n
Tactic: obtain ⟨s', hs', u, hu, h⟩ := hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
T : TopologicalSpace X
𝔅 : Set (Set X)
hT : T = generateFrom 𝔅
h𝔅 : ∀ s ∈ 𝔅, sᶜ ∈ 𝔅
h : ∀ P ⊆ 𝔅, (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) → (⋂₀ P).Nonempty
⊢ CompactSpace X
have refine : ∀ (P : Set (Set X)) (hP𝔅 : P ⊆ 𝔅) (hP : ⋃₀ P = univ), ∃ Q ⊆ P, Q.Finite ∧ ⋃₀ Q = univ
Tactic: refine compactSpace_generateFrom hT fun P hP𝔅 hP ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
T : TopologicalSpace X
𝔅 : Set (Set X)
hT : T = generateFrom 𝔅
h𝔅 : ∀ s ∈ 𝔅, sᶜ ∈ 𝔅
h : ∀ P ⊆ 𝔅, (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) → (⋂₀ P).Nonempty
P : Set (Set X)
hP𝔅 : P ⊆ 𝔅
hP : ⋃₀ P = univ
⊢ ∃ Q ⊆ P, Q.Finite ∧ ⋃₀ Q = univ
have contrapose! : ∀ (hP : ∀ (Q : Set (Set X)) (_ : Q ⊆ P) (_ : Q.Finite), ⋃₀ Q ≠ univ), ⋃₀ P ≠ univ
Tactic: contrapose! hP
Cleared hypotheses: hP
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
T : TopologicalSpace X
𝔅 : Set (Set X)
hT : T = generateFrom 𝔅
h𝔅 : ∀ s ∈ 𝔅, sᶜ ∈ 𝔅
h : ∀ P ⊆ 𝔅, (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) → (⋂₀ P).Nonempty
P : Set (Set X)
hP𝔅 : P ⊆ 𝔅
hP : ∀ (Q : Set (Set X)) (_ : Q ⊆ P) (_ : Q.Finite), ⋃₀ Q ≠ univ
⊢ ⋃₀ P ≠ univ
have simp_rw : ∀ (hP : ∀ (Q : Set (Set X)) (_ : Q ⊆ P) (_ : Q.Finite), (⋂₀ (compl '' Q)).Nonempty), (⋂₀ (compl '' P)).Nonempty
Tactic: simp_rw [← Set.nonempty_compl, Set.compl_sUnion] at hP ⊢
Cleared hypotheses: hP
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
T : TopologicalSpace X
𝔅 : Set (Set X)
hT : T = generateFrom 𝔅
h𝔅 : ∀ s ∈ 𝔅, sᶜ ∈ 𝔅
h : ∀ P ⊆ 𝔅, (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) → (⋂₀ P).Nonempty
P : Set (Set X)
hP𝔅 : P ⊆ 𝔅
hP : ∀ (Q : Set (Set X)) (_ : Q ⊆ P) (_ : Q.Finite), (⋂₀ (compl '' Q)).Nonempty
⊢ (⋂₀ (compl '' P)).Nonempty
have refine_1 : compl '' P ⊆ 𝔅
Tactic: refine h _ ?_ fun Q hQP hQ ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
T : TopologicalSpace X
𝔅 : Set (Set X)
hT : T = generateFrom 𝔅
h𝔅 : ∀ s ∈ 𝔅, sᶜ ∈ 𝔅
h : ∀ P ⊆ 𝔅, (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) → (⋂₀ P).Nonempty
P : Set (Set X)
hP𝔅 : P ⊆ 𝔅
hP : ∀ (Q : Set (Set X)) (_ : Q ⊆ P) (_ : Q.Finite), (⋂₀ (compl '' Q)).Nonempty
refine_1 : compl '' P ⊆ 𝔅
⊢ (⋂₀ (compl '' P)).Nonempty
have refine_2 : ∀ (Q : Set (Set X)) (hQP : Q ⊆ compl '' P) (hQ : Q.Finite), (⋂₀ Q).Nonempty
Tactic: refine h _ ?_ fun Q hQP hQ ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (hypothesis)
Goal:
X : Type u
T : TopologicalSpace X
𝔅 : Set (Set X)
hT : T = generateFrom 𝔅
h𝔅 : ∀ s ∈ 𝔅, sᶜ ∈ 𝔅
h : ∀ P ⊆ 𝔅, (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) → (⋂₀ P).Nonempty
P : Set (Set X)
hP𝔅 : P ⊆ 𝔅
hP : ∀ (Q : Set (Set X)) (_ : Q ⊆ P) (_ : Q.Finite), (⋂₀ (compl '' Q)).Nonempty
Q : Set (Set X)
hQP : Q ⊆ compl '' P
hQ : Q.Finite
⊢ (⋂₀ Q).Nonempty
have hP₁ : Q ⊆ compl '' P → (compl '' Q).Finite → (⋂₀ Q).Nonempty
Tactic: replace hP : Q ⊆ compl '' P → (compl '' Q).Finite → (⋂₀ Q).Nonempty := by
      simpa [← compl_involutive.image_eq_preimage_symm] using hP (compl '' Q)
Cleared hypotheses: hP
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
f : X → Y
inst_2 : NoncompactSpace X
⊢ (cocompact X).NeBot
have refine : ∀ {i : Set X} (hs : IsCompact i), iᶜ.Nonempty
Tactic: refine Filter.hasBasis_cocompact.neBot_iff.2 fun hs => ?_
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
f : X → Y
inst_2 : NoncompactSpace X
i : Set X
hs : IsCompact i
⊢ iᶜ.Nonempty
have contrapose : ∀ (hs : ¬iᶜ.Nonempty), ¬IsCompact i
Tactic: contrapose hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (hypothesis)
Goal:
X : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
f : X → Y
inst_2 : NoncompactSpace X
i : Set X
hs : ¬iᶜ.Nonempty
⊢ ¬IsCompact i
have hs₁ : i = univ
Tactic: rw [not_nonempty_iff_eq_empty, compl_empty_iff] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
f : X → Y
inst_2 : NoncompactSpace X
i : Set X
hs : i = univ
⊢ ¬IsCompact i
have rw : ¬IsCompact.{u} (X := X) univ
Tactic: rw [hs]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s K : Set X
hs : s.Infinite
hK : IsCompact K
hsub : s ⊆ K
x : X
hx : x ∈ K ∧ ClusterPt x (cofinite ⊓ 𝓟 s)
⊢ x ∈ K ∧ AccPt x (cofinite ⊓ 𝓟 s)
have rwa : x ∈ K ∧ ClusterPt x (𝓟 {x}ᶜ ⊓ (cofinite ⊓ 𝓟 s))
Tactic: rwa [accPt_iff_clusterPt, inf_comm, inf_right_comm,
      (finite_singleton _).cofinite_inf_principal_compl]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s K : Set X
hs : s.Infinite
hK : IsCompact K
hsub : s ⊆ K
x : X
hx : x ∈ K ∧ ClusterPt x (cofinite ⊓ 𝓟 s)
rwa : x ∈ K ∧ ClusterPt x (𝓟 {x}ᶜ ⊓ (cofinite ⊓ 𝓟 s))
⊢ x ∈ K ∧ AccPt x (cofinite ⊓ 𝓟 s)
have rwa₁ : x ∈ K ∧ ClusterPt x (cofinite ⊓ 𝓟 s ⊓ 𝓟 {x}ᶜ)
Tactic: rwa [accPt_iff_clusterPt, inf_comm, inf_right_comm,
      (finite_singleton _).cofinite_inf_principal_compl]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s K : Set X
hs : s.Infinite
hK : IsCompact K
hsub : s ⊆ K
x : X
hx : x ∈ K ∧ ClusterPt x (cofinite ⊓ 𝓟 s)
rwa : x ∈ K ∧ ClusterPt x (𝓟 {x}ᶜ ⊓ (cofinite ⊓ 𝓟 s))
rwa₁ : x ∈ K ∧ ClusterPt x (cofinite ⊓ 𝓟 s ⊓ 𝓟 {x}ᶜ)
⊢ x ∈ K ∧ AccPt x (cofinite ⊓ 𝓟 s)
have rwa₂ : x ∈ K ∧ ClusterPt x (cofinite ⊓ 𝓟 {x}ᶜ ⊓ 𝓟 s)
Tactic: rwa [accPt_iff_clusterPt, inf_comm, inf_right_comm,
      (finite_singleton _).cofinite_inf_principal_compl]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : Continuous[inst, inst_1] f
⊢ comap f (cocompact Y) ≤ cocompact X
have rw : ∀ (i' : Set X), IsCompact i' → ∃ (i : Set Y), IsCompact i ∧ f ⁻¹' iᶜ ⊆ i'ᶜ
Tactic: rw [(Filter.hasBasis_cocompact.comap f).le_basis_iff Filter.hasBasis_cocompact]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : Continuous[inst, inst_1] f
t : Set X
ht : IsCompact t
⊢ ∃ (i : Set Y), IsCompact i ∧ f ⁻¹' iᶜ ⊆ tᶜ
have refine : f ⁻¹' (f '' t)ᶜ ⊆ tᶜ
Tactic: refine ⟨f '' t, ht.image hf, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
g : X → Y
f : Filter X
hg : Continuous[inst, inst_1] g
hf : Disjoint f (cocompact X)
⊢ Disjoint (map g f) (cocompact Y)
have rw : f ⊓ comap g (cocompact Y) ≤ ⊥
Tactic: rw [← Filter.disjoint_comap_iff_map, disjoint_iff_inf_le]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace X
f : X → Y
hf : Continuous[inst, inst_1] f
⊢ IsCompact (range f)
have rw : IsCompact (f '' univ)
Tactic: rw [← image_univ]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
hf : IsInducing f
⊢ IsCompact s ↔ IsCompact (f '' s)
have refine : ∀ (hs : IsCompact (f '' s)) (F : Filter X) (F_ne_bot : F.NeBot) (F_le : F ≤ 𝓟 s), ∃ x ∈ s, ClusterPt x F
Tactic: refine ⟨fun hs => hs.image hf.continuous, fun hs F F_ne_bot F_le => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
hf : IsInducing f
hs : IsCompact (f '' s)
F : Filter X
F_ne_bot : F.NeBot
F_le : F ≤ 𝓟 s
⊢ ∃ x ∈ s, ClusterPt x F
have obtain : ∀ (x : X) (x_in : x ∈ s) (hx : ClusterPt (f x) (map f F)), ∃ x ∈ s, ClusterPt x F
Tactic: obtain ⟨_, ⟨x, x_in : x ∈ s, rfl⟩, hx : ClusterPt (f x) (map f F)⟩ :=
    hs ((map_mono F_le).trans_eq map_principal)
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (hypothesis)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsInducing f
hf' : IsClosed[inst_1] (range f)
K : Set Y
hK : IsCompact K
⊢ IsCompact (f ⁻¹' K)
have hK₁ : IsCompact (K ∩ range f)
Tactic: replace hK := hK.inter_right hf'
Cleared hypotheses: hK
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsInducing f
hf' : IsClosed[inst_1] (range f)
K : Set Y
hK : IsCompact (K ∩ range f)
⊢ IsCompact (f ⁻¹' K)
have rwa : IsCompact (f '' f ⁻¹' K)
Tactic: rwa [hf.isCompact_iff, image_preimage_eq_inter_range]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsInducing f
K : Set Y
Kf : K ⊆ range f
⊢ IsCompact (f ⁻¹' K) ↔ IsCompact K
have rw : IsCompact (f '' f ⁻¹' K) ↔ IsCompact K
Tactic: rw [hf.isCompact_iff, image_preimage_eq_of_subset Kf]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsInducing f
K : Set Y
Kf : K ⊆ range f
rw : IsCompact (f '' f ⁻¹' K) ↔ IsCompact K
⊢ IsCompact (f ⁻¹' K) ↔ IsCompact K
have rw₁ : IsCompact K ↔ IsCompact K
Tactic: rw [hf.isCompact_iff, image_preimage_eq_of_subset Kf]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ IsCompact s ↔ IsCompact.{u} (X := (↑s : Type u)) univ
have rw : IsCompact s ↔ IsCompact.{u} (X := X) (image (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) univ)
Tactic: rw [Subtype.isCompact_iff, image_univ, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
rw :
  IsCompact s ↔ IsCompact.{u} (X := X) (image (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) univ)
⊢ IsCompact s ↔ IsCompact.{u} (X := (↑s : Type u)) univ
have rw₁ : IsCompact s ↔ IsCompact.{u} (X := X) (range (ι := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)))
Tactic: rw [Subtype.isCompact_iff, image_univ, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
rw :
  IsCompact s ↔ IsCompact.{u} (X := X) (image (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) univ)
rw₁ : IsCompact s ↔ IsCompact.{u} (X := X) (range (ι := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)))
⊢ IsCompact s ↔ IsCompact.{u} (X := (↑s : Type u)) univ
have rw₂ : IsCompact s ↔ IsCompact s
Tactic: rw [Subtype.isCompact_iff, image_univ, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
ks : IsCompact s
ι : Type u_3
t : ι → Set X
I : Set ι
htc : ∀ i ∈ I, IsClosed[instTopologicalSpaceSubtype] (s ↓∩ t i)
hst : s ∩ ⋂ i ∈ I, t i = ∅
⊢ ∃ (u : Finset (↑I : Type u_3)), s ∩ ⋂ i ∈ u, t (↑i : ι) = ∅
have suffices : Eq.{u_2 + 1} (α := Set (↑s : Type u_2))
  (univ ∩ ⋂ (i : (↑I : Type u_3)), (fun (i : (↑I : Type u_3)) ↦ (s ↓∩ t (↑i : ι) : Set (↑s : Type u_2))) i) ∅
Tactic: suffices univ ∩ ⋂ i, (fun i : I ↦ s ↓∩ t i) i = ∅ by
    simpa [eq_empty_iff_forall_notMem] using
      (isCompact_iff_isCompact_univ.mp ks).elim_finite_subfamily_closed
      (fun i : I ↦ s ↓∩ t i) (fun i ↦ htc i.val i.prop) this
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : CompactSpace Y
f : X → Y
hf : IsClosedEmbedding f
⊢ IsCompact.{u} (X := X) univ
have rw : IsCompact (range f)
Tactic: rw [hf.isInducing.isCompact_iff, image_univ]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
t : Set Y
hs : IsCompact s
ht : IsCompact t
⊢ IsCompact (s ×ˢ t)
have rw : ∀ (hs : ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, (↑f : Filter X) ≤ 𝓝 x)
  (ht : ∀ (f : Ultrafilter Y), t ∈ f → ∃ x ∈ t, (↑f : Filter Y) ≤ 𝓝 x) (f : Ultrafilter (X × Y)),
  s ×ˢ t ∈ f → ∃ x ∈ s ×ˢ t, (↑f : Filter (X × Y)) ≤ 𝓝 x
Tactic: rw [isCompact_iff_ultrafilter_le_nhds'] at hs ht ⊢
Cleared hypotheses: hs, ht
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
t : Set Y
hs : ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, (↑f : Filter X) ≤ 𝓝 x
ht : ∀ (f : Ultrafilter Y), t ∈ f → ∃ x ∈ t, (↑f : Filter Y) ≤ 𝓝 x
f : Ultrafilter (X × Y)
hfs : s ×ˢ t ∈ f
⊢ ∃ x ∈ s ×ˢ t, (↑f : Filter (X × Y)) ≤ 𝓝 x
have obtain : ∀ (x : X) (sx : x ∈ s) (hx : map Prod.fst (↑f : Filter (X × Y)) ≤ 𝓝 x), ∃ x ∈ s ×ˢ t, (↑f : Filter (X × Y)) ≤ 𝓝 x
Tactic: obtain ⟨x : X, sx : x ∈ s, hx : map Prod.fst f.1 ≤ 𝓝 x⟩ :=
    hs (f.map Prod.fst) (mem_map.2 <| mem_of_superset hfs fun x => And.left)
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
t : Set Y
hs : ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, (↑f : Filter X) ≤ 𝓝 x
ht : ∀ (f : Ultrafilter Y), t ∈ f → ∃ x ∈ t, (↑f : Filter Y) ≤ 𝓝 x
f : Ultrafilter (X × Y)
hfs : s ×ˢ t ∈ f
x : X
sx : x ∈ s
hx : map Prod.fst (↑f : Filter (X × Y)) ≤ 𝓝 x
⊢ ∃ x ∈ s ×ˢ t, (↑f : Filter (X × Y)) ≤ 𝓝 x
have obtain : ∀ (y : Y) (ty : y ∈ t) (hy : map Prod.snd (↑f : Filter (X × Y)) ≤ 𝓝 y), ∃ x ∈ s ×ˢ t, (↑f : Filter (X × Y)) ≤ 𝓝 x
Tactic: obtain ⟨y : Y, ty : y ∈ t, hy : map Prod.snd f.1 ≤ 𝓝 y⟩ :=
    ht (f.map Prod.snd) (mem_map.2 <| mem_of_superset hfs fun x => And.right)
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
t : Set Y
hs : ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, (↑f : Filter X) ≤ 𝓝 x
ht : ∀ (f : Ultrafilter Y), t ∈ f → ∃ x ∈ t, (↑f : Filter Y) ≤ 𝓝 x
f : Ultrafilter (X × Y)
hfs : s ×ˢ t ∈ f
x : X
sx : x ∈ s
hx : map Prod.fst (↑f : Filter (X × Y)) ≤ 𝓝 x
y : Y
ty : y ∈ t
hy : map Prod.snd (↑f : Filter (X × Y)) ≤ 𝓝 y
⊢ ∃ x ∈ s ×ˢ t, (↑f : Filter (X × Y)) ≤ 𝓝 x
have rw : ∀ (hx : (↑f : Filter (X × Y)) ≤ comap Prod.fst (𝓝 x)) (y : Y) (ty : y ∈ t)
  (hy : (↑f : Filter (X × Y)) ≤ comap Prod.snd (𝓝 y)), ∃ x ∈ s ×ˢ t, (↑f : Filter (X × Y)) ≤ 𝓝 x
Tactic: rw [map_le_iff_le_comap] at hx hy
Cleared hypotheses: hx, y, ty, hy
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
t : Set Y
hs : ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, (↑f : Filter X) ≤ 𝓝 x
ht : ∀ (f : Ultrafilter Y), t ∈ f → ∃ x ∈ t, (↑f : Filter Y) ≤ 𝓝 x
f : Ultrafilter (X × Y)
hfs : s ×ˢ t ∈ f
x : X
sx : x ∈ s
hx : (↑f : Filter (X × Y)) ≤ comap Prod.fst (𝓝 x)
y : Y
ty : y ∈ t
hy : (↑f : Filter (X × Y)) ≤ comap Prod.snd (𝓝 y)
⊢ ∃ x ∈ s ×ˢ t, (↑f : Filter (X × Y)) ≤ 𝓝 x
have refine : (↑f : Filter (X × Y)) ≤ 𝓝 (x, y)
Tactic: refine ⟨⟨x, y⟩, ⟨sx, ty⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
t : Set Y
hs : ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, (↑f : Filter X) ≤ 𝓝 x
ht : ∀ (f : Ultrafilter Y), t ∈ f → ∃ x ∈ t, (↑f : Filter Y) ≤ 𝓝 x
f : Ultrafilter (X × Y)
hfs : s ×ˢ t ∈ f
x : X
sx : x ∈ s
hx : (↑f : Filter (X × Y)) ≤ comap Prod.fst (𝓝 x)
y : Y
ty : y ∈ t
hy : (↑f : Filter (X × Y)) ≤ comap Prod.snd (𝓝 y)
⊢ (↑f : Filter (X × Y)) ≤ 𝓝 (x, y)
have rw : (↑f : Filter (X × Y)) ≤ 𝓝 x ×ˢ 𝓝 y
Tactic: rw [nhds_prod_eq]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
f : X → Y
inst_2 : CompactSpace X
inst_3 : CompactSpace Y
⊢ IsCompact (X := X × Y) univ
have rw : IsCompact (SProd.sprod (α := Set X) (β := Set Y) univ univ)
Tactic: rw [← univ_prod_univ]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
f : X → Y
inst_2 : CompactSpace X
inst_3 : CompactSpace Y
⊢ IsCompact (X := X ⊕ Y) univ
have rw : IsCompact (X := X ⊕ Y) (range Sum.inl ∪ range Sum.inr)
Tactic: rw [← range_inl_union_range_inr]