awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X_1 : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s t : Set X_1
f : X_1 → Y
X : ι → Type u_2
inst_2 : Finite ι
inst_3 : (i : ι) → TopologicalSpace (X i)
inst_4 : ∀ (i : ι), CompactSpace.{u_2} (X i)
⊢ CompactSpace ((i : ι) × X i)
have refine : IsCompact (X := (i : ι) × X i) univ
Tactic: refine ⟨?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X_1 : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s t : Set X_1
f : X_1 → Y
X : ι → Type u_2
inst_2 : Finite ι
inst_3 : (i : ι) → TopologicalSpace (X i)
inst_4 : ∀ (i : ι), CompactSpace.{u_2} (X i)
⊢ IsCompact (X := (i : ι) × X i) univ
have rw : IsCompact (X := (i : ι) × X i) (⋃ (a : ι), range (Sigma.mk (β := fun (a : ι) ↦ X a) a))
Tactic: rw [Sigma.univ]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : Set ι
t : (i : ι) → Set (X i)
hs : s.Finite
ht : ∀ i ∈ s, IsCompact (t i)
⊢ IsCompact (s.sigma (α := X) t)
have rw : IsCompact (X := (i : ι) × X i) (⋃ i ∈ s, Sigma.mk (β := X) i '' t i)
Tactic: rw [Set.sigma_eq_biUnion]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
u : Set ((i : ι) × X i)
hu : IsCompact u
⊢ ∃ (s : Set ι) (t : (i : ι) → Set (X i)), s.Finite ∧ (∀ (i : ι), IsCompact (t i)) ∧ s.sigma (α := X) t = u
have obtain : ∀ (s : Finset ι) (hs : u ⊆ ⋃ i ∈ s, Sigma.mk (β := fun (i : ι) ↦ X i) i '' Sigma.mk (β := X) i ⁻¹' univ),
  ∃ (s : Set ι) (t : (i : ι) → Set (X i)), s.Finite ∧ (∀ (i : ι), IsCompact (t i)) ∧ s.sigma (α := X) t = u
Tactic: obtain ⟨s, hs⟩ := hu.elim_finite_subcover (fun i : ι ↦ Sigma.mk i '' Sigma.mk i ⁻¹' Set.univ)
    (fun i ↦ isOpenMap_sigmaMk _ <| isOpen_univ.preimage continuous_sigmaMk)
    fun x hx ↦ (by simp)
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
u : Set ((i : ι) × X i)
hu : IsCompact u
s : Finset ι
hs : u ⊆ ⋃ i ∈ s, Sigma.mk (β := fun (i : ι) ↦ X i) i '' Sigma.mk (β := X) i ⁻¹' univ
⊢ ∃ (s : Set ι) (t : (i : ι) → Set (X i)), s.Finite ∧ (∀ (i : ι), IsCompact (t i)) ∧ s.sigma (α := X) t = u
have left : ∀ (i : ι), IsCompact (Sigma.mk (β := X) i ⁻¹' u)
Tactic: use s, fun i ↦ Sigma.mk i ⁻¹' u, s.finite_toSet, fun i ↦ ?_, ?_
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
u : Set ((i : ι) × X i)
hu : IsCompact u
s : Finset ι
hs : u ⊆ ⋃ i ∈ s, Sigma.mk (β := fun (i : ι) ↦ X i) i '' Sigma.mk (β := X) i ⁻¹' univ
left : ∀ (i : ι), IsCompact (Sigma.mk (β := X) i ⁻¹' u)
⊢ ∃ (s : Set ι) (t : (i : ι) → Set (X i)), s.Finite ∧ (∀ (i : ι), IsCompact (t i)) ∧ s.sigma (α := X) t = u
have right : ((↑s : Set ι).sigma (α := X) fun (i : ι) ↦ Sigma.mk (β := X) i ⁻¹' u) = u
Tactic: use s, fun i ↦ Sigma.mk i ⁻¹' u, s.finite_toSet, fun i ↦ ?_, ?_
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
u : Set ((i : ι) × X i)
hu : IsCompact u
s : Finset ι
hs : u ⊆ ⋃ i ∈ s, Sigma.mk (β := fun (i : ι) ↦ X i) i '' Sigma.mk (β := X) i ⁻¹' univ
⊢ ((↑s : Set ι).sigma (α := X) fun (i : ι) ↦ Sigma.mk (β := X) i ⁻¹' u) = u
have right : ∀ (x : (i : ι) × X i),
  Membership.mem (γ := Set ((i : ι) × X i)) ((↑s : Set ι).sigma (α := X) fun (i : ι) ↦ Sigma.mk (β := X) i ⁻¹' u) x ↔
    x ∈ u
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
u : Set ((i : ι) × X i)
hu : IsCompact u
s : Finset ι
hs : u ⊆ ⋃ i ∈ s, Sigma.mk (β := fun (i : ι) ↦ X i) i '' Sigma.mk (β := X) i ⁻¹' univ
x : (i : ι) × X i
⊢ Membership.mem (γ := Set ((i : ι) × X i)) ((↑s : Set ι).sigma (α := X) fun (i : ι) ↦ Sigma.mk (β := X) i ⁻¹' u) x ↔
    x ∈ u
have right : Sigma.mk (β := X) (x.fst (β := fun (i : ι) ↦ X i)) (x.snd (β := fun (i : ι) ↦ X i)) ∈ u →
  x.fst (β := fun (i : ι) ↦ X i) ∈ s
Tactic: simp only [Set.mem_sigma_iff, Finset.mem_coe, Set.mem_preimage, and_iff_right_iff_imp]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
u : Set ((i : ι) × X i)
hu : IsCompact u
s : Finset ι
hs : u ⊆ ⋃ i ∈ s, Sigma.mk (β := fun (i : ι) ↦ X i) i '' Sigma.mk (β := X) i ⁻¹' univ
x : (i : ι) × X i
hx : Sigma.mk (β := X) (x.fst (β := fun (i : ι) ↦ X i)) (x.snd (β := fun (i : ι) ↦ X i)) ∈ u
⊢ x.fst (β := fun (i : ι) ↦ X i) ∈ s
have right : ∀ (i : ι)
  (hi :
    Membership.mem (γ := Set ((i : ι) × X i))
      (⋃ (_ : i ∈ s), Sigma.mk (β := fun (i : ι) ↦ X i) i '' Sigma.mk (β := X) i ⁻¹' univ)
      (Sigma.mk (β := X) (x.fst (β := fun (i : ι) ↦ X i)) (x.snd (β := fun (i : ι) ↦ X i)))),
  x.fst (β := fun (i : ι) ↦ X i) ∈ s
Tactic: obtain ⟨i, hi⟩ := Set.mem_iUnion.mp (hs hx)
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ (cocompact X).coprod (cocompact Y) = cocompact (X × Y)
have a : (cocompact X).coprod (cocompact Y) ≤ cocompact (X × Y)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
a : (cocompact X).coprod (cocompact Y) ≤ cocompact (X × Y)
⊢ (cocompact X).coprod (cocompact Y) = cocompact (X × Y)
have a₁ : cocompact (X × Y) ≤ (cocompact X).coprod (cocompact Y)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ cocompact (X × Y) ≤ (cocompact X).coprod (cocompact Y)
have a : ∀ (K : Prod.{u, v} (Set X) (Set Y)) (hK : IsCompact K.1 ∧ IsCompact K.2),
  Membership.mem (γ := Filter (X × Y)) (cocompact (X × Y)) (Prod.fst ⁻¹' K.1ᶜ ∪ Prod.snd ⁻¹' K.2ᶜ)
Tactic: refine (hasBasis_cocompact.coprod hasBasis_cocompact).ge_iff.2 fun K 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
K : Prod.{u, v} (Set X) (Set Y)
hK : IsCompact K.1 ∧ IsCompact K.2
⊢ Membership.mem (γ := Filter (X × Y)) (cocompact (X × Y)) (Prod.fst ⁻¹' K.1ᶜ ∪ Prod.snd ⁻¹' K.2ᶜ)
have a : Membership.mem (γ := Filter (X × Y)) (cocompact (X × Y)) (K.1 ×ˢ K.2)ᶜ
Tactic: rw [← univ_prod, ← prod_univ, ← compl_prod_eq_union]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
⊢ (∀ (i : ι), IsCompact (s i)) → IsCompact (X := (i : ι) → X i) {x : (i : ι) → X i | ∀ (i : ι), x i ∈ s i}
have simp : (∀ (i : ι) (f : Ultrafilter (X i)), s i ∈ (↑f : Filter (X i)) → ∃ x ∈ s i, (↑f : Filter (X i)) ≤ 𝓝 x) →
  ∀ (f : Ultrafilter ((i : ι) → X i)),
    {x : (i : ι) → X i | ∀ (i : ι), x i ∈ s i} ∈ (↑f : Filter ((i : ι) → X i)) →
      ∃ (x : (i : ι) → X i),
        Membership.mem (γ := Set ((i : ι) → X i)) {x : (i : ι) → X i | ∀ (i : ι), x i ∈ s i} x ∧
          ∀ (i : ι), Tendsto (eval (β := X) i) (↑f : Filter ((i : ι) → X i)) (𝓝 (x i))
Tactic: simp only [isCompact_iff_ultrafilter_le_nhds, nhds_pi, le_pi, le_principal_iff]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
h : ∀ (i : ι) (f : Ultrafilter (X i)), s i ∈ (↑f : Filter (X i)) → ∃ x ∈ s i, (↑f : Filter (X i)) ≤ 𝓝 x
f : Ultrafilter ((i : ι) → X i)
hfs : {x : (i : ι) → X i | ∀ (i : ι), x i ∈ s i} ∈ (↑f : Filter ((i : ι) → X i))
⊢ ∀ (i : ι), ∃ x ∈ s i, Tendsto (eval (β := X) i) (↑f : Filter ((i : ι) → X i)) (𝓝 x)
have refine : ∀ (i : ι), eval (β := X) i ⁻¹' s i ∈ (↑f : Filter ((i : ι) → X i))
Tactic: refine fun i => h i (f.map _) (mem_map.2 ?_)
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (hypothesis)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
h : ∀ (i : ι) (f : Ultrafilter (X i)), s i ∈ (↑f : Filter (X i)) → ∃ x ∈ s i, (↑f : Filter (X i)) ≤ 𝓝 x
f : Ultrafilter ((i : ι) → X i)
hfs : {x : (i : ι) → X i | ∀ (i : ι), x i ∈ s i} ∈ (↑f : Filter ((i : ι) → X i))
⊢ ∃ (x : (i : ι) → X i),
    Membership.mem (γ := Set ((i : ι) → X i)) {x : (i : ι) → X i | ∀ (i : ι), x i ∈ s i} x ∧
      ∀ (i : ι), Tendsto (eval (β := X) i) (↑f : Filter ((i : ι) → X i)) (𝓝 (x i))
have this : ∀ (i : ι), ∃ x ∈ s i, Tendsto (eval (β := X) i) (↑f : Filter ((i : ι) → X i)) (𝓝 x)
Tactic: have : ∀ i : ι, ∃ x, x ∈ s i ∧ Tendsto (Function.eval i) f (𝓝 x) := by
    refine fun i => h i (f.map _) (mem_map.2 ?_)
    exact mem_of_superset hfs fun x hx => hx i
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
h : ∀ (i : ι) (f : Ultrafilter (X i)), s i ∈ (↑f : Filter (X i)) → ∃ x ∈ s i, (↑f : Filter (X i)) ≤ 𝓝 x
f : Ultrafilter ((i : ι) → X i)
hfs : {x : (i : ι) → X i | ∀ (i : ι), x i ∈ s i} ∈ (↑f : Filter ((i : ι) → X i))
this : ∀ (i : ι), ∃ x ∈ s i, Tendsto (eval (β := X) i) (↑f : Filter ((i : ι) → X i)) (𝓝 x)
⊢ ∃ (x : (i : ι) → X i),
    Membership.mem (γ := Set ((i : ι) → X i)) {x : (i : ι) → X i | ∀ (i : ι), x i ∈ s i} x ∧
      ∀ (i : ι), Tendsto (eval (β := X) i) (↑f : Filter ((i : ι) → X i)) (𝓝 (x i))
have choose : ∀ (x : (i : ι) → X i) (hx : ∀ (i : ι), x i ∈ s i ∧ Tendsto (eval (β := X) i) (↑f : Filter ((i : ι) → X i)) (𝓝 (x i))),
  ∃ (x : (i : ι) → X i),
    Membership.mem (γ := Set ((i : ι) → X i)) {x : (i : ι) → X i | ∀ (i : ι), x i ∈ s i} x ∧
      ∀ (i : ι), Tendsto (eval (β := X) i) (↑f : Filter ((i : ι) → X i)) (𝓝 (x i))
Tactic: choose x hx using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
h : ∀ (i : ι), IsCompact (s i)
⊢ IsCompact (Set.pi (α := X) univ s)
have h₁ : Set.pi (α := X) univ s = {x : (i : ι) → X i | ∀ (i : ι), x i ∈ s i}
Tactic: convert! isCompact_pi_infinite h
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X_1 : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s t : Set X_1
f : X_1 → Y
X : ι → Type u_2
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), CompactSpace.{u_2} (X i)
⊢ IsCompact (X := (i : ι) → X i) univ
have rw : IsCompact (X := (i : ι) → X i) (Set.pi (α := X) univ fun (i : ι) ↦ univ)
Tactic: rw [← pi_univ univ]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) → X i)
hs : IsClosed[topologicalSpace] s
⊢ IsCompact s ↔ ∀ (i : ι), IsCompact (eval (β := X) i '' s)
have mp : IsCompact s → ∀ (i : ι), IsCompact (eval (β := X) i '' s)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) → X i)
hs : IsClosed[topologicalSpace] s
mp : IsCompact s → ∀ (i : ι), IsCompact (eval (β := X) i '' s)
⊢ IsCompact s ↔ ∀ (i : ι), IsCompact (eval (β := X) i '' s)
have mpr : (∀ (i : ι), IsCompact (eval (β := X) i '' s)) → IsCompact s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) → X i)
⊢ (∃ (K : Set ((i : ι) → X i)), IsCompact K ∧ s ⊆ K) ↔
    ∀ (i : ι), ∃ (Ki : Set (X i)), IsCompact Ki ∧ s ⊆ eval (β := X) i ⁻¹' Ki
have mp : (∃ (K : Set ((i : ι) → X i)), IsCompact K ∧ s ⊆ K) →
  ∀ (i : ι), ∃ (Ki : Set (X i)), IsCompact Ki ∧ s ⊆ eval (β := X) i ⁻¹' Ki
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) → X i)
mp :
  (∃ (K : Set ((i : ι) → X i)), IsCompact K ∧ s ⊆ K) →
    ∀ (i : ι), ∃ (Ki : Set (X i)), IsCompact Ki ∧ s ⊆ eval (β := X) i ⁻¹' Ki
⊢ (∃ (K : Set ((i : ι) → X i)), IsCompact K ∧ s ⊆ K) ↔
    ∀ (i : ι), ∃ (Ki : Set (X i)), IsCompact Ki ∧ s ⊆ eval (β := X) i ⁻¹' Ki
have mpr : (∀ (i : ι), ∃ (Ki : Set (X i)), IsCompact Ki ∧ s ⊆ eval (β := X) i ⁻¹' Ki) →
  ∃ (K : Set ((i : ι) → X i)), IsCompact K ∧ s ⊆ K
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) → X i)
H : ∀ (i : ι), ∃ (Ki : Set (X i)), IsCompact Ki ∧ s ⊆ eval (β := X) i ⁻¹' Ki
⊢ ∃ (K : Set ((i : ι) → X i)), IsCompact K ∧ s ⊆ K
have mpr : ∀ (K : (i : ι) → Set (X i)) (hK : ∀ (i : ι), IsCompact (K i)) (hsK : ∀ (i : ι), s ⊆ eval (β := X) i ⁻¹' K i),
  ∃ (K : Set ((i : ι) → X i)), IsCompact K ∧ s ⊆ K
Tactic: choose K hK hsK using H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
ι : Type u_1
X : ι → Type u_3
inst : (d : ι) → TopologicalSpace (X d)
⊢ Eq (α := Filter ((i : ι) → X i)) (Filter.coprodᵢ (α := X) fun (d : ι) ↦ cocompact (X d)) (cocompact ((d : ι) → X d))
have refine : LE.le (α := Filter ((i : ι) → X i)) (cocompact ((d : ι) → X d)) (Filter.coprodᵢ (α := X) fun (d : ι) ↦ cocompact (X d))
Tactic: refine le_antisymm (iSup_le fun i => Filter.comap_cocompact_le (continuous_apply i)) ?_
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
ι : Type u_1
X : ι → Type u_3
inst : (d : ι) → TopologicalSpace (X d)
⊢ LE.le (α := Filter ((i : ι) → X i)) (cocompact ((d : ι) → X d))
    (Filter.coprodᵢ (α := X) fun (d : ι) ↦ cocompact (X d))
have refine : ∀ (s : Set ((i : ι) → X i))
  (H : Membership.mem (γ := Filter ((i : ι) → X i)) (Filter.coprodᵢ (α := X) fun (d : ι) ↦ cocompact (X d)) sᶜ),
  Membership.mem (γ := Filter ((i : ι) → X i)) (cocompact ((d : ι) → X d)) sᶜ
Tactic: refine compl_surjective.forall.2 fun s H => ?_
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
ι : Type u_1
X : ι → Type u_3
inst : (d : ι) → TopologicalSpace (X d)
s : Set ((i : ι) → X i)
H : Membership.mem (γ := Filter ((i : ι) → X i)) (Filter.coprodᵢ (α := X) fun (d : ι) ↦ cocompact (X d)) sᶜ
⊢ Membership.mem (γ := Filter ((i : ι) → X i)) (cocompact ((d : ι) → X d)) sᶜ
have simp : ∀ (H : ∀ (i : ι), ∃ (t : Set (X i)), IsCompact t ∧ s ⊆ eval (β := X) i ⁻¹' t),
  ∃ (t : Set ((d : ι) → X d)), IsCompact t ∧ s ⊆ t
Tactic: simp only [compl_mem_coprodᵢ, Filter.mem_cocompact, compl_subset_compl, image_subset_iff] at H ⊢
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
ι : Type u_1
X : ι → Type u_3
inst : (d : ι) → TopologicalSpace (X d)
s : Set ((i : ι) → X i)
H : ∀ (i : ι), ∃ (t : Set (X i)), IsCompact t ∧ s ⊆ eval (β := X) i ⁻¹' t
⊢ ∃ (t : Set ((d : ι) → X d)), IsCompact t ∧ s ⊆ t
have choose : ∀ (K : (i : ι) → Set (X i)) (hKc : ∀ (i : ι), IsCompact (K i)) (htK : ∀ (i : ι), s ⊆ eval (β := X) i ⁻¹' K i),
  ∃ (t : Set ((d : ι) → X d)), IsCompact t ∧ s ⊆ t
Tactic: choose K hKc htK using H
Cleared hypotheses: H
-- 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
r : X → X → Prop
inst_2 : CompactSpace X
⊢ IsCompact.{u} (X := Quot r) univ
have rw : IsCompact (range (mk r))
Tactic: rw [← range_quot_mk]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
S : Set X
hS : IsClosed[inst] S
hne : S.Nonempty
opens : Set (Set X) := {U : Set X | Sᶜ ⊆ U ∧ IsOpen[inst] U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun (x1 x2 : Set X) ↦ x1 ⊆ x2) c
⊢ ∃ ub ∈ opens, ∀ s ∈ c, s ⊆ ub
have pos : ∀ (hcne : c.Nonempty), ∃ ub ∈ opens, ∀ s ∈ c, s ⊆ ub
Tactic: by_cases hcne : c.Nonempty
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
S : Set X
hS : IsClosed[inst] S
hne : S.Nonempty
opens : Set (Set X) := {U : Set X | Sᶜ ⊆ U ∧ IsOpen[inst] U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun (x1 x2 : Set X) ↦ x1 ⊆ x2) c
pos : ∀ (hcne : c.Nonempty), ∃ ub ∈ opens, ∀ s ∈ c, s ⊆ ub
⊢ ∃ ub ∈ opens, ∀ s ∈ c, s ⊆ ub
have neg : ∀ (hcne : ¬c.Nonempty), ∃ ub ∈ opens, ∀ s ∈ c, s ⊆ ub
Tactic: by_cases hcne : c.Nonempty
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
S : Set X
hS : IsClosed[inst] S
hne : S.Nonempty
opens : Set (Set X) := {U : Set X | Sᶜ ⊆ U ∧ IsOpen[inst] U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun (x1 x2 : Set X) ↦ x1 ⊆ x2) c
hcne : c.Nonempty
⊢ ∃ ub ∈ opens, ∀ s ∈ c, s ⊆ ub
have pos : ∀ (U₀ : Set X) (hU₀ : U₀ ∈ c), ∃ ub ∈ opens, ∀ s ∈ c, s ⊆ ub
Tactic: obtain ⟨U₀, hU₀⟩ := hcne
Cleared hypotheses: hcne
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
S : Set X
hS : IsClosed[inst] S
hne : S.Nonempty
opens : Set (Set X) := {U : Set X | Sᶜ ⊆ U ∧ IsOpen[inst] U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun (x1 x2 : Set X) ↦ x1 ⊆ x2) c
U₀ : Set X
hU₀ : U₀ ∈ c
⊢ ∃ ub ∈ opens, ∀ s ∈ c, s ⊆ ub
have this : Nonempty.{max 1 (u + 1)} { U : Set X // U ∈ c }
Tactic: haveI : Nonempty { U // U ∈ c } := ⟨⟨U₀, hU₀⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
S : Set X
hS : IsClosed[inst] S
hne : S.Nonempty
opens : Set (Set X) := {U : Set X | Sᶜ ⊆ U ∧ IsOpen[inst] U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun (x1 x2 : Set X) ↦ x1 ⊆ x2) c
U₀ : Set X
hU₀ : U₀ ∈ c
this : Nonempty.{max 1 (u + 1)} { U : Set X // U ∈ c }
⊢ ∃ ub ∈ opens, ∀ s ∈ c, s ⊆ ub
have U₀compl : Sᶜ ⊆ U₀
Tactic: obtain ⟨U₀compl, -, -⟩ := hc hU₀
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
S : Set X
hS : IsClosed[inst] S
hne : S.Nonempty
opens : Set (Set X) := {U : Set X | Sᶜ ⊆ U ∧ IsOpen[inst] U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun (x1 x2 : Set X) ↦ x1 ⊆ x2) c
U₀ : Set X
hU₀ : U₀ ∈ c
this : Nonempty.{max 1 (u + 1)} { U : Set X // U ∈ c }
U₀compl : Sᶜ ⊆ U₀
⊢ ∃ ub ∈ opens, ∀ s ∈ c, s ⊆ ub
have h : ⋃₀ c ∈ opens ∧ ∀ s ∈ c, s ⊆ ⋃₀ c
Tactic: use ⋃₀ c
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
S : Set X
hS : IsClosed[inst] S
hne : S.Nonempty
opens : Set (Set X) := {U : Set X | Sᶜ ⊆ U ∧ IsOpen[inst] U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun (x1 x2 : Set X) ↦ x1 ⊆ x2) c
U₀ : Set X
hU₀ : U₀ ∈ c
this : Nonempty.{max 1 (u + 1)} { U : Set X // U ∈ c }
U₀compl : Sᶜ ⊆ U₀
⊢ ⋃₀ c ∈ opens ∧ ∀ s ∈ c, s ⊆ ⋃₀ c
have h : Sᶜ ⊆ ⋃₀ c
Tactic: refine ⟨⟨?_, ?_, ?_⟩, fun U hU _ hx => ⟨U, hU, hx⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
S : Set X
hS : IsClosed[inst] S
hne : S.Nonempty
opens : Set (Set X) := {U : Set X | Sᶜ ⊆ U ∧ IsOpen[inst] U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun (x1 x2 : Set X) ↦ x1 ⊆ x2) c
U₀ : Set X
hU₀ : U₀ ∈ c
this : Nonempty.{max 1 (u + 1)} { U : Set X // U ∈ c }
U₀compl : Sᶜ ⊆ U₀
h : Sᶜ ⊆ ⋃₀ c
⊢ ⋃₀ c ∈ opens ∧ ∀ s ∈ c, s ⊆ ⋃₀ c
have h₁ : IsOpen[inst] (⋃₀ c)
Tactic: refine ⟨⟨?_, ?_, ?_⟩, fun U hU _ hx => ⟨U, hU, hx⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
S : Set X
hS : IsClosed[inst] S
hne : S.Nonempty
opens : Set (Set X) := {U : Set X | Sᶜ ⊆ U ∧ IsOpen[inst] U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun (x1 x2 : Set X) ↦ x1 ⊆ x2) c
U₀ : Set X
hU₀ : U₀ ∈ c
this : Nonempty.{max 1 (u + 1)} { U : Set X // U ∈ c }
U₀compl : Sᶜ ⊆ U₀
h : Sᶜ ⊆ ⋃₀ c
h₁ : IsOpen[inst] (⋃₀ c)
⊢ ⋃₀ c ∈ opens ∧ ∀ s ∈ c, s ⊆ ⋃₀ c
have h₂ : (⋃₀ c)ᶜ.Nonempty
Tactic: refine ⟨⟨?_, ?_, ?_⟩, fun U hU _ hx => ⟨U, hU, hx⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
S : Set X
hS : IsClosed[inst] S
hne : S.Nonempty
opens : Set (Set X) := {U : Set X | Sᶜ ⊆ U ∧ IsOpen[inst] U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun (x1 x2 : Set X) ↦ x1 ⊆ x2) c
U₀ : Set X
hU₀ : U₀ ∈ c
this : Nonempty.{max 1 (u + 1)} { U : Set X // U ∈ c }
U₀compl : Sᶜ ⊆ U₀
⊢ (⋃₀ c)ᶜ.Nonempty
have h : (⋃₀ c)ᶜ = ⋂ (U : { U : Set X // U ∈ c }), (↑U : Set X)ᶜ
Tactic: convert_to (⋂ U : { U // U ∈ c }, U.1ᶜ).Nonempty
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
S : Set X
hS : IsClosed[inst] S
hne : S.Nonempty
opens : Set (Set X) := {U : Set X | Sᶜ ⊆ U ∧ IsOpen[inst] U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun (x1 x2 : Set X) ↦ x1 ⊆ x2) c
U₀ : Set X
hU₀ : U₀ ∈ c
this : Nonempty.{max 1 (u + 1)} { U : Set X // U ∈ c }
U₀compl : Sᶜ ⊆ U₀
h : (⋃₀ c)ᶜ = ⋂ (U : { U : Set X // U ∈ c }), (↑U : Set X)ᶜ
⊢ (⋃₀ c)ᶜ.Nonempty
have h₁ : Set.Nonempty.{u} (α := X) (⋂ (U : { U : Set X // U ∈ c }), (↑U : Set X)ᶜ)
Tactic: convert_to (⋂ U : { U // U ∈ c }, U.1ᶜ).Nonempty
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
S : Set X
hS : IsClosed[inst] S
hne : S.Nonempty
opens : Set (Set X) := {U : Set X | Sᶜ ⊆ U ∧ IsOpen[inst] U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun (x1 x2 : Set X) ↦ x1 ⊆ x2) c
U₀ : Set X
hU₀ : U₀ ∈ c
this : Nonempty.{max 1 (u + 1)} { U : Set X // U ∈ c }
U₀compl : Sᶜ ⊆ U₀
⊢ (⋃₀ c)ᶜ = ⋂ (U : { U : Set X // U ∈ c }), (↑U : Set X)ᶜ
have h : ∀ (x : X), x ∈ (⋃₀ c)ᶜ ↔ Membership.mem (γ := Set X) (⋂ (U : { U : Set X // U ∈ c }), (↑U : Set X)ᶜ) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
S : Set X
hS : IsClosed[inst] S
hne : S.Nonempty
opens : Set (Set X) := {U : Set X | Sᶜ ⊆ U ∧ IsOpen[inst] U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun (x1 x2 : Set X) ↦ x1 ⊆ x2) c
U₀ : Set X
hU₀ : U₀ ∈ c
this : Nonempty.{max 1 (u + 1)} { U : Set X // U ∈ c }
U₀compl : Sᶜ ⊆ U₀
⊢ Set.Nonempty.{u} (α := X) (⋂ (U : { U : Set X // U ∈ c }), (↑U : Set X)ᶜ)
have h : Directed (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) fun (i : { U : Set X // U ∈ c }) ↦ (↑i : Set X)ᶜ
Tactic: apply IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
S : Set X
hS : IsClosed[inst] S
hne : S.Nonempty
opens : Set (Set X) := {U : Set X | Sᶜ ⊆ U ∧ IsOpen[inst] U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun (x1 x2 : Set X) ↦ x1 ⊆ x2) c
U₀ : Set X
hU₀ : U₀ ∈ c
this : Nonempty.{max 1 (u + 1)} { U : Set X // U ∈ c }
U₀compl : Sᶜ ⊆ U₀
h : Directed (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) fun (i : { U : Set X // U ∈ c }) ↦ (↑i : Set X)ᶜ
⊢ Set.Nonempty.{u} (α := X) (⋂ (U : { U : Set X // U ∈ c }), (↑U : Set X)ᶜ)
have h₁ : ∀ (i : { U : Set X // U ∈ c }), (↑i : Set X)ᶜ.Nonempty
Tactic: apply IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed