awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsInducing f
this :
  Eq.{u_1 + 1} (α := Set (Set α)) {U : Set α | IsOpen[inst] U}
    ((fun (x : Set β) ↦ f ⁻¹' x) '' {V : Set β | IsOpen[inst_1] V})
eq_induced :
  Eq.{u_1 + 1} (α := TopologicalSpace (Set α))
    (generateFrom
      (powerset '' {U : Set α | IsOpen[inst] U} ∪
        (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {U : Set α | IsOpen[inst] U}))
    (induced.{u_1, u_2} (Y := Set β) (fun (x : Set α) ↦ f '' x)
      (generateFrom
        (powerset '' {U : Set β | IsOpen[inst_1] U} ∪
          (fun (V : Set β) ↦ {s : Set β | (s ∩ V).Nonempty}) '' {U : Set β | IsOpen[inst_1] U})))
eq_induced₁ :
  Eq.{u_1 + 1} (α := TopologicalSpace (Set α))
    (generateFrom
      (powerset '' (fun (x : Set β) ↦ f ⁻¹' x) '' {V : Set β | IsOpen[inst_1] V} ∪
        (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) ''
          (fun (x : Set β) ↦ f ⁻¹' x) '' {V : Set β | IsOpen[inst_1] V}))
    (induced.{u_1, u_2} (Y := Set β) (fun (x : Set α) ↦ f '' x)
      (generateFrom
        (powerset '' {V : Set β | IsOpen[inst_1] V} ∪
          (fun (V : Set β) ↦ {s : Set β | (s ∩ V).Nonempty}) '' {V : Set β | IsOpen[inst_1] V})))
eq_induced₂ :
  Eq.{u_1 + 1} (α := TopologicalSpace (Set α))
    (generateFrom
      (powerset '' (fun (x : Set β) ↦ f ⁻¹' x) '' {V : Set β | IsOpen[inst_1] V} ∪
        (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) ''
          (fun (x : Set β) ↦ f ⁻¹' x) '' {V : Set β | IsOpen[inst_1] V}))
    (generateFrom
      (image.{u_2, u_1} (α := Set (Set β)) (preimage fun (x : Set α) ↦ f '' x)
        (powerset '' {V : Set β | IsOpen[inst_1] V} ∪
          (fun (V : Set β) ↦ {s : Set β | (s ∩ V).Nonempty}) '' {V : Set β | IsOpen[inst_1] V})))
⊢ TopologicalSpace.vietoris α = induced (fun (x : Set α) ↦ f '' x) (TopologicalSpace.vietoris β)
have eq_induced₃ : Eq.{u_1 + 1} (α := TopologicalSpace (Set α))
  (generateFrom
    (powerset '' (fun (x : Set β) ↦ f ⁻¹' x) '' {V : Set β | IsOpen[inst_1] V} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) ''
        (fun (x : Set β) ↦ f ⁻¹' x) '' {V : Set β | IsOpen[inst_1] V}))
  (generateFrom
    (image.{u_2, u_1} (α := Set (Set β)) (preimage fun (x : Set α) ↦ f '' x)
        (powerset '' {V : Set β | IsOpen[inst_1] V}) ∪
      image.{u_2, u_1} (α := Set (Set β)) (preimage fun (x : Set α) ↦ f '' x)
        ((fun (V : Set β) ↦ {s : Set β | (s ∩ V).Nonempty}) '' {V : Set β | IsOpen[inst_1] V})))
Tactic: simp_rw [TopologicalSpace.vietoris, this, induced_generateFrom_eq, image_union, image_image,
    powerset, preimage_setOf_eq, image_subset_iff, image_inter_nonempty_iff]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
⊢ IsCompact.{u_1} (X := Set α) {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty}
have refine : ∀ (S : Set (Set (Set α)))
  (hS :
    S ⊆
      powerset '' {U : Set α | IsOpen[inst] U} ∪
        (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V})
  (hKS : {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S),
  ∃ Q ⊆ S, Q.Finite ∧ {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ Q
Tactic: refine isCompact_generateFrom rfl fun S hS hKS => ?_
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS :
  S ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
hKS : {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
u : Set (Set α) := {U : Set α | IsOpen[inst] U ∧ {s : Set α | (s ∩ U).Nonempty} ∈ S}
⊢ ∃ Q ⊆ S, Q.Finite ∧ {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ Q
have pos : ∀ (hsu : ∃ L ∈ s, L ⊆ ⋃₀ u), ∃ Q ⊆ S, Q.Finite ∧ {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ Q
Tactic: by_cases! hsu : ∃ L ∈ s, L ⊆ ⋃₀ u
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS :
  S ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
hKS : {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
u : Set (Set α) := {U : Set α | IsOpen[inst] U ∧ {s : Set α | (s ∩ U).Nonempty} ∈ S}
pos : ∀ (hsu : ∃ L ∈ s, L ⊆ ⋃₀ u), ∃ Q ⊆ S, Q.Finite ∧ {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ Q
⊢ ∃ Q ⊆ S, Q.Finite ∧ {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ Q
have neg : ∀ (hsu : ∀ (L : Set α) (_ : L ∈ s), ¬L ⊆ ⋃₀ u),
  ∃ Q ⊆ S, Q.Finite ∧ {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ Q
Tactic: by_cases! hsu : ∃ L ∈ s, L ⊆ ⋃₀ u
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS :
  S ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
hKS : {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
u : Set (Set α) := {U : Set α | IsOpen[inst] U ∧ {s : Set α | (s ∩ U).Nonempty} ∈ S}
hsu : ∃ L ∈ s, L ⊆ ⋃₀ u
⊢ ∃ Q ⊆ S, Q.Finite ∧ {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ Q
have pos : ∀ (L : Set α) (hL : L ∈ s) (hLu : L ⊆ ⋃₀ u), ∃ Q ⊆ S, Q.Finite ∧ {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ Q
Tactic: obtain ⟨L, hL, hLu⟩ := hsu
Cleared hypotheses: hsu
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS :
  S ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
hKS : {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
u : Set (Set α) := {U : Set α | IsOpen[inst] U ∧ {s : Set α | (s ∩ U).Nonempty} ∈ S}
L : Set α
hL : L ∈ s
hLu : L ⊆ ⋃₀ u
⊢ ∃ Q ⊆ S, Q.Finite ∧ {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ Q
have hLu₁ : L ⊆ ⋃ i ∈ u, i
Tactic: rw [sUnion_eq_biUnion] at hLu
Cleared hypotheses: hLu
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS :
  S ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
hKS : {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
u : Set (Set α) := {U : Set α | IsOpen[inst] U ∧ {s : Set α | (s ∩ U).Nonempty} ∈ S}
L : Set α
hL : L ∈ s
hLu : L ⊆ ⋃ i ∈ u, i
⊢ ∃ Q ⊆ S, Q.Finite ∧ {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ Q
have pos : ∀ (T : Set (Set α)) (hTS : T ⊆ u) (hT : T.Finite) (hLT : L ⊆ ⋃ i ∈ T, i),
  ∃ Q ⊆ S, Q.Finite ∧ {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ Q
Tactic: obtain ⟨T, hTS, hT, hLT⟩ := (hs L hL).elim_finite_subcover_image (fun _ h => h.1) hLu
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS :
  S ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
hKS : {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
u : Set (Set α) := {U : Set α | IsOpen[inst] U ∧ {s : Set α | (s ∩ U).Nonempty} ∈ S}
L : Set α
hL : L ∈ s
hLu : L ⊆ ⋃ i ∈ u, i
T : Set (Set α)
hTS : T ⊆ u
hT : T.Finite
hLT : L ⊆ ⋃ i ∈ T, i
⊢ ∃ Q ⊆ S, Q.Finite ∧ {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ Q
have pos : Subset (α := Set (Set α)) {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty}
  (⋃₀ ((fun (U : Set α) ↦ {s : Set α | (s ∩ U).Nonempty}) '' T))
Tactic: refine ⟨(fun U => {s | (s ∩ U).Nonempty}) '' T, by grind [image_subset_iff], hT.image _, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS :
  S ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
hKS : {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
u : Set (Set α) := {U : Set α | IsOpen[inst] U ∧ {s : Set α | (s ∩ U).Nonempty} ∈ S}
L : Set α
hL : L ∈ s
hLu : L ⊆ ⋃ i ∈ u, i
T : Set (Set α)
hTS : T ⊆ u
hT : T.Finite
hLT : L ⊆ ⋃ i ∈ T, i
⊢ Subset (α := Set (Set α)) {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty}
    (⋃₀ ((fun (U : Set α) ↦ {s : Set α | (s ∩ U).Nonempty}) '' T))
have pos : Subset.{u_1} (α := Set (Set α)) {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} {x : Set α | (x ∩ ⋃ i ∈ T, i).Nonempty}
Tactic: simp_rw [sUnion_image, ← setOf_exists, ← nonempty_iUnion, ← inter_iUnion]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS :
  S ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
hKS : {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
u : Set (Set α) := {U : Set α | IsOpen[inst] U ∧ {s : Set α | (s ∩ U).Nonempty} ∈ S}
L : Set α
hL : L ∈ s
hLu : L ⊆ ⋃ i ∈ u, i
T : Set (Set α)
hTS : T ⊆ u
hT : T.Finite
hLT : L ⊆ ⋃ i ∈ T, i
⊢ Subset.{u_1} (α := Set (Set α)) {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty}
    {x : Set α | (x ∩ ⋃ i ∈ T, i).Nonempty}
have pos : Subset.{u_1} (α := Set (Set α)) {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} {x : Set α | (x ∩ L).Nonempty}
Tactic: grw [← hLT]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS :
  S ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
hKS : {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
u : Set (Set α) := {U : Set α | IsOpen[inst] U ∧ {s : Set α | (s ∩ U).Nonempty} ∈ S}
hsu : ∀ (L : Set α) (_ : L ∈ s), ¬L ⊆ ⋃₀ u
⊢ ∃ Q ⊆ S, Q.Finite ∧ {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ Q
have hsu₁ : ∀ (L : Set α) (_ : L ∈ s), (L \ ⋃₀ u).Nonempty
Tactic: simp_rw [← diff_nonempty] at hsu
Cleared hypotheses: hsu
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS :
  S ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
hKS : {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
u : Set (Set α) := {U : Set α | IsOpen[inst] U ∧ {s : Set α | (s ∩ U).Nonempty} ∈ S}
hsu : ∀ (L : Set α) (_ : L ∈ s), (L \ ⋃₀ u).Nonempty
⊢ ∃ Q ⊆ S, Q.Finite ∧ {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ Q
have hsu₁ : ∀ (L : Set α) (h : L ∈ s), (K \ ⋃₀ u ∩ L).Nonempty
Tactic: replace hsu L (h : L ∈ s) : (K \ ⋃₀ u ∩ L).Nonempty := (hsu L h).mono <| by grind
Cleared hypotheses: hsu
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS :
  S ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
hKS : {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
u : Set (Set α) := {U : Set α | IsOpen[inst] U ∧ {s : Set α | (s ∩ U).Nonempty} ∈ S}
hsu : ∀ (L : Set α) (h : L ∈ s), (K \ ⋃₀ u ∩ L).Nonempty
⊢ ∃ Q ⊆ S, Q.Finite ∧ {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ Q
have neg : ∀ (w : Set (Set α)) (hUS : w ∈ S) (hUu : K \ ⋃₀ u ∈ w),
  ∃ Q ⊆ S, Q.Finite ∧ {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ Q
Tactic: obtain ⟨_, hUS, hUu⟩ := mem_sUnion.mp <| hKS ⟨diff_subset, hsu⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS :
  S ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
hKS : {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
u : Set (Set α) := {U : Set α | IsOpen[inst] U ∧ {s : Set α | (s ∩ U).Nonempty} ∈ S}
hsu : ∀ (L : Set α) (h : L ∈ s), (K \ ⋃₀ u ∩ L).Nonempty
w : Set (Set α)
hUS : w ∈ S
hUu : K \ ⋃₀ u ∈ w
⊢ ∃ Q ⊆ S, Q.Finite ∧ {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ Q
have neg : ∀ (U : Set α) (hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U) (hUS : 𝒫 U ∈ S)
  (hUu : K \ ⋃₀ u ∈ 𝒫 U), ∃ Q ⊆ S, Q.Finite ∧ {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ Q
Tactic: rcases hS hUS with ⟨U, hU, rfl⟩ | ⟨U, hU, rfl⟩
Cleared hypotheses: w, hUS, hUu
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS :
  S ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
hKS : {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
u : Set (Set α) := {U : Set α | IsOpen[inst] U ∧ {s : Set α | (s ∩ U).Nonempty} ∈ S}
hsu : ∀ (L : Set α) (h : L ∈ s), (K \ ⋃₀ u ∩ L).Nonempty
w : Set (Set α)
hUS : w ∈ S
hUu : K \ ⋃₀ u ∈ w
neg :
  ∀ (U : Set α) (hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U) (hUS : 𝒫 U ∈ S)
    (hUu : K \ ⋃₀ u ∈ 𝒫 U), ∃ Q ⊆ S, Q.Finite ∧ {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ Q
⊢ ∃ Q ⊆ S, Q.Finite ∧ {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ Q
have neg₁ : ∀ (U : Set α) (hU : Membership.mem (γ := Set (Set α)) {V : Set α | IsOpen[inst] V} U)
  (hUS : (fun (V : Set α) ↦ ({s : Set α | (s ∩ V).Nonempty} : Set (Set α))) U ∈ S)
  (hUu :
    Membership.mem (γ := Set (Set α)) ((fun (V : Set α) ↦ ({s : Set α | (s ∩ V).Nonempty} : Set (Set α))) U)
      (K \ ⋃₀ u)),
  ∃ Q ⊆ S, Q.Finite ∧ {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ Q
Tactic: rcases hS hUS with ⟨U, hU, rfl⟩ | ⟨U, hU, rfl⟩
Cleared hypotheses: w, hUS, hUu
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS :
  S ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
hKS : {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
u : Set (Set α) := {U : Set α | IsOpen[inst] U ∧ {s : Set α | (s ∩ U).Nonempty} ∈ S}
hsu : ∀ (L : Set α) (h : L ∈ s), (K \ ⋃₀ u ∩ L).Nonempty
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U
hUS : 𝒫 U ∈ S
hUu : K \ ⋃₀ u ∈ 𝒫 U
⊢ ∃ Q ⊆ S, Q.Finite ∧ {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ Q
have hUu₁ : K \ U ⊆ ⋃ i ∈ u, i
Tactic: rw [mem_powerset_iff, diff_subset_comm, sUnion_eq_biUnion] at hUu
Cleared hypotheses: hUu
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS :
  S ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
hKS : {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
u : Set (Set α) := {U : Set α | IsOpen[inst] U ∧ {s : Set α | (s ∩ U).Nonempty} ∈ S}
hsu : ∀ (L : Set α) (h : L ∈ s), (K \ ⋃₀ u ∩ L).Nonempty
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U
hUS : 𝒫 U ∈ S
hUu : K \ U ⊆ ⋃ i ∈ u, i
⊢ ∃ Q ⊆ S, Q.Finite ∧ {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ Q
have neg : ∀ (T : Set (Set α)) (hTS : T ⊆ u) (hT : T.Finite) (hKT : K \ U ⊆ ⋃ i ∈ T, i),
  ∃ Q ⊆ S, Q.Finite ∧ {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ Q
Tactic: obtain ⟨T, hTS, hT, hKT⟩ := (hK.diff hU).elim_finite_subcover_image (fun _ h => h.1) hUu
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS :
  S ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
hKS : {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
u : Set (Set α) := {U : Set α | IsOpen[inst] U ∧ {s : Set α | (s ∩ U).Nonempty} ∈ S}
hsu : ∀ (L : Set α) (h : L ∈ s), (K \ ⋃₀ u ∩ L).Nonempty
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U
hUS : 𝒫 U ∈ S
hUu : K \ U ⊆ ⋃ i ∈ u, i
T : Set (Set α)
hTS : T ⊆ u
hT : T.Finite
hKT : K \ U ⊆ ⋃ i ∈ T, i
⊢ ∃ Q ⊆ S, Q.Finite ∧ {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ Q
have neg : Subset (α := Set (Set α)) {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty}
  (⋃₀ insert (𝒫 U) ((fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' T))
Tactic: refine ⟨insert U.powerset ((fun V => {s | (s ∩ V).Nonempty}) '' T),
        insert_subset hUS <| Set.image_subset_iff.mpr <| hTS.trans fun _ h => h.2,
        (hT.image _).insert _, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS :
  S ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
hKS : {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
u : Set (Set α) := {U : Set α | IsOpen[inst] U ∧ {s : Set α | (s ∩ U).Nonempty} ∈ S}
hsu : ∀ (L : Set α) (h : L ∈ s), (K \ ⋃₀ u ∩ L).Nonempty
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U
hUS : 𝒫 U ∈ S
hUu : K \ U ⊆ ⋃ i ∈ u, i
T : Set (Set α)
hTS : T ⊆ u
hT : T.Finite
hKT : K \ U ⊆ ⋃ i ∈ T, i
⊢ Subset (α := Set (Set α)) {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty}
    (⋃₀ insert (𝒫 U) ((fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' T))
have neg : {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} \ 𝒫 U ⊆ ⋃ a ∈ T, {s : Set α | (s ∩ a).Nonempty}
Tactic: rw [sUnion_insert, ← diff_subset_iff, sUnion_image]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS :
  S ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
hKS : {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
u : Set (Set α) := {U : Set α | IsOpen[inst] U ∧ {s : Set α | (s ∩ U).Nonempty} ∈ S}
hsu : ∀ (L : Set α) (h : L ∈ s), (K \ ⋃₀ u ∩ L).Nonempty
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U
hUS : 𝒫 U ∈ S
hUu : K \ U ⊆ ⋃ i ∈ u, i
T : Set (Set α)
hTS : T ⊆ u
hT : T.Finite
hKT : K \ U ⊆ ⋃ i ∈ T, i
t : Set α
htU : t ∉ 𝒫 U
htK : t ⊆ K
⊢ Membership.mem (γ := Set (Set α)) (⋃ a ∈ T, {s : Set α | (s ∩ a).Nonempty}) t
have htU₁ : ∃ a ∈ t, a ∉ U
Tactic: rw [mem_powerset_iff, not_subset] at htU
Cleared hypotheses: htU, htK
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS :
  S ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
hKS : {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
u : Set (Set α) := {U : Set α | IsOpen[inst] U ∧ {s : Set α | (s ∩ U).Nonempty} ∈ S}
hsu : ∀ (L : Set α) (h : L ∈ s), (K \ ⋃₀ u ∩ L).Nonempty
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U
hUS : 𝒫 U ∈ S
hUu : K \ U ⊆ ⋃ i ∈ u, i
T : Set (Set α)
hTS : T ⊆ u
hT : T.Finite
hKT : K \ U ⊆ ⋃ i ∈ T, i
t : Set α
htU : ∃ a ∈ t, a ∉ U
htK : t ⊆ K
⊢ Membership.mem (γ := Set (Set α)) (⋃ a ∈ T, {s : Set α | (s ∩ a).Nonempty}) t
have neg : ∀ (x : α) (hxt : x ∈ t) (hxU : x ∉ U), Membership.mem (γ := Set (Set α)) (⋃ a ∈ T, {s : Set α | (s ∩ a).Nonempty}) t
Tactic: obtain ⟨x, hxt, hxU⟩ := htU
Cleared hypotheses: htU
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS :
  S ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
hKS : {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
u : Set (Set α) := {U : Set α | IsOpen[inst] U ∧ {s : Set α | (s ∩ U).Nonempty} ∈ S}
hsu : ∀ (L : Set α) (h : L ∈ s), (K \ ⋃₀ u ∩ L).Nonempty
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U
hUS : 𝒫 U ∈ S
hUu : K \ U ⊆ ⋃ i ∈ u, i
T : Set (Set α)
hTS : T ⊆ u
hT : T.Finite
hKT : K \ U ⊆ ⋃ i ∈ T, i
t : Set α
htK : t ⊆ K
x : α
hxt : x ∈ t
hxU : x ∉ U
⊢ Membership.mem (γ := Set (Set α)) (⋃ a ∈ T, {s : Set α | (s ∩ a).Nonempty}) t
have neg : ∀ (V : Set α) (hVT : V ∈ T) (hxV : x ∈ V), Membership.mem (γ := Set (Set α)) (⋃ a ∈ T, {s : Set α | (s ∩ a).Nonempty}) t
Tactic: obtain ⟨V, hVT, hxV⟩ := mem_iUnion₂.mp <| hKT ⟨htK hxt, hxU⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS :
  S ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
hKS : {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
u : Set (Set α) := {U : Set α | IsOpen[inst] U ∧ {s : Set α | (s ∩ U).Nonempty} ∈ S}
hsu : ∀ (L : Set α) (h : L ∈ s), (K \ ⋃₀ u ∩ L).Nonempty
U : Set α
hU : Membership.mem (γ := Set (Set α)) {V : Set α | IsOpen[inst] V} U
hUS : (fun (V : Set α) ↦ ({s : Set α | (s ∩ V).Nonempty} : Set (Set α))) U ∈ S
hUu :
  Membership.mem (γ := Set (Set α)) ((fun (V : Set α) ↦ ({s : Set α | (s ∩ V).Nonempty} : Set (Set α))) U) (K \ ⋃₀ u)
⊢ ∃ Q ⊆ S, Q.Finite ∧ {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ Q
have neg : ∀ (x : α) (hxu : x ∈ K \ ⋃₀ u) (hxU : x ∈ U), ∃ Q ⊆ S, Q.Finite ∧ {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ Q
Tactic: obtain ⟨x, hxu, hxU⟩ := hUu
Cleared hypotheses: hUu
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
⊢ s ⤳ t ↔ (∀ x ∈ s, ∃ y ∈ t, x ⤳ y) ∧ t ⊆ closure[inst] s
have refine_1 : ∀ (h : s ⤳ t) (x : α) (hx : x ∈ s), ∃ y ∈ t, x ⤳ y
Tactic: refine ⟨fun h => ⟨fun x hx => ?_, subset_closure_of_specializes h⟩, fun ⟨hst, hts⟩ => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
refine_1 : ∀ (h : s ⤳ t) (x : α) (hx : x ∈ s), ∃ y ∈ t, x ⤳ y
⊢ s ⤳ t ↔ (∀ x ∈ s, ∃ y ∈ t, x ⤳ y) ∧ t ⊆ closure[inst] s
have refine_2 : (∀ x ∈ s, ∃ y ∈ t, x ⤳ y) ∧ t ⊆ closure[inst] s → ∀ (hst : ∀ x ∈ s, ∃ y ∈ t, x ⤳ y) (hts : t ⊆ closure[inst] s), s ⤳ t
Tactic: refine ⟨fun h => ⟨fun x hx => ?_, subset_closure_of_specializes h⟩, fun ⟨hst, hts⟩ => ?_⟩