awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
V : Set α
u : Set (Set α)
hV : IsOpen[inst] V
hu : u.Finite
huB : u ⊆ B
huV : ∀ U ∈ u, U ⊆ V
K : Compacts α
hKu : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
w : Set (Set α)
hKV : (↑K : Set α) ⊆ ⋃₀ w
hwB : w ⊆ B
hwV : ⋃₀ w ⊆ V
refine_2 :
  ∀
    (this :
      ∀ (w : Set (Set α)) (hKV : (↑K : Set α) ⊆ ⋃₀ w) (hwB : w ⊆ B) (hwV : ⋃₀ w ⊆ V)
        (hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty),
        ∃ (v : Set (Compacts α)),
          Membership.mem (γ := Set (Set (Compacts α)))
              ((fun (u : Set (Set α)) ↦
                  {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
                {u : Set (Set α) | u.Finite ∧ u ⊆ B})
              v ∧
            K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty})
    (hwK : ¬∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty),
    ∃ (v : Set (Compacts α)),
      Membership.mem (γ := Set (Set (Compacts α)))
          ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
            {u : Set (Set α) | u.Finite ∧ u ⊆ B})
          v ∧
        K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
⊢ ∃ (v : Set (Compacts α)),
    Membership.mem (γ := Set (Set (Compacts α)))
        ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
          {u : Set (Set α) | u.Finite ∧ u ⊆ B})
        v ∧
      K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
have wlog : ∀ (w : Set (Set α)) (hKV : (↑K : Set α) ⊆ ⋃₀ w) (hwB : w ⊆ B) (hwV : ⋃₀ w ⊆ V)
  (hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty),
  ∃ (v : Set (Compacts α)),
    Membership.mem (γ := Set (Set (Compacts α)))
        ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
          {u : Set (Set α) | u.Finite ∧ u ⊆ B})
        v ∧
      K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
Tactic: wlog hwK : ∀ W ∈ w, ((K : Set α) ∩ W).Nonempty generalizing w
Cleared hypotheses: w, hKV, hwB, hwV
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
V : Set α
u : Set (Set α)
hV : IsOpen[inst] V
hu : u.Finite
huB : u ⊆ B
huV : ∀ U ∈ u, U ⊆ V
K : Compacts α
hKu : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
w : Set (Set α)
hKV : (↑K : Set α) ⊆ ⋃₀ w
hwB : w ⊆ B
hwV : ⋃₀ w ⊆ V
this :
  ∀ (w : Set (Set α)) (hKV : (↑K : Set α) ⊆ ⋃₀ w) (hwB : w ⊆ B) (hwV : ⋃₀ w ⊆ V)
    (hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty),
    ∃ (v : Set (Compacts α)),
      Membership.mem (γ := Set (Set (Compacts α)))
          ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
            {u : Set (Set α) | u.Finite ∧ u ⊆ B})
          v ∧
        K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
hwK : ¬∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty
⊢ ∃ (v : Set (Compacts α)),
    Membership.mem (γ := Set (Set (Compacts α)))
        ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
          {u : Set (Set α) | u.Finite ∧ u ⊆ B})
        v ∧
      K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
have refine_2 : ∀ (x : α) (hx : x ∈ (↑K : Set α)), Membership.mem (γ := Set α) (⋃₀ {W : Set α | W ∈ w ∧ ((↑K : Set α) ∩ W).Nonempty}) x
Tactic: refine this {W ∈ w | (↑K ∩ W).Nonempty} (fun x hx => ?_) (by grind) (by grind) (by grind)
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
V : Set α
u : Set (Set α)
hV : IsOpen[inst] V
hu : u.Finite
huB : u ⊆ B
huV : ∀ U ∈ u, U ⊆ V
K : Compacts α
hKu : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
w : Set (Set α)
hKV : (↑K : Set α) ⊆ ⋃₀ w
hwB : w ⊆ B
hwV : ⋃₀ w ⊆ V
this :
  ∀ (w : Set (Set α)) (hKV : (↑K : Set α) ⊆ ⋃₀ w) (hwB : w ⊆ B) (hwV : ⋃₀ w ⊆ V)
    (hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty),
    ∃ (v : Set (Compacts α)),
      Membership.mem (γ := Set (Set (Compacts α)))
          ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
            {u : Set (Set α) | u.Finite ∧ u ⊆ B})
          v ∧
        K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
hwK : ¬∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty
x : α
hx : x ∈ (↑K : Set α)
⊢ Membership.mem (γ := Set α) (⋃₀ {W : Set α | W ∈ w ∧ ((↑K : Set α) ∩ W).Nonempty}) x
have refine_2 : ∀ (W : Set α) (hWw : W ∈ w) (hxW : x ∈ W),
  Membership.mem (γ := Set α) (⋃₀ {W : Set α | W ∈ w ∧ ((↑K : Set α) ∩ W).Nonempty}) x
Tactic: obtain ⟨W, hWw, hxW⟩ := mem_sUnion.mp (hKV hx)
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
V : Set α
u : Set (Set α)
hV : IsOpen[inst] V
hu : u.Finite
huB : u ⊆ B
huV : ∀ U ∈ u, U ⊆ V
K : Compacts α
hKu : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
w : Set (Set α)
hKV : (↑K : Set α) ⊆ ⋃₀ w
hwB : w ⊆ B
hwV : ⋃₀ w ⊆ V
hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty
⊢ ∃ (v : Set (Compacts α)),
    Membership.mem (γ := Set (Set (Compacts α)))
        ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
          {u : Set (Set α) | u.Finite ∧ u ⊆ B})
        v ∧
      K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
have inr : ∀
  (this :
    ∀ (w : Set (Set α)) (hKV : (↑K : Set α) ⊆ ⋃₀ w) (hwB : w ⊆ B) (hwV : ⋃₀ w ⊆ V)
      (hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty) (hw : w.Finite),
      ∃ (v : Set (Compacts α)),
        Membership.mem (γ := Set (Set (Compacts α)))
            ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
              {u : Set (Set α) | u.Finite ∧ u ⊆ B})
            v ∧
          K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty})
  (hw : ¬w.Finite),
  ∃ (v : Set (Compacts α)),
    Membership.mem (γ := Set (Set (Compacts α)))
        ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
          {u : Set (Set α) | u.Finite ∧ u ⊆ B})
        v ∧
      K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
Tactic: wlog hw : w.Finite generalizing w
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
V : Set α
u : Set (Set α)
hV : IsOpen[inst] V
hu : u.Finite
huB : u ⊆ B
huV : ∀ U ∈ u, U ⊆ V
K : Compacts α
hKu : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
w : Set (Set α)
hKV : (↑K : Set α) ⊆ ⋃₀ w
hwB : w ⊆ B
hwV : ⋃₀ w ⊆ V
hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty
inr :
  ∀
    (this :
      ∀ (w : Set (Set α)) (hKV : (↑K : Set α) ⊆ ⋃₀ w) (hwB : w ⊆ B) (hwV : ⋃₀ w ⊆ V)
        (hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty) (hw : w.Finite),
        ∃ (v : Set (Compacts α)),
          Membership.mem (γ := Set (Set (Compacts α)))
              ((fun (u : Set (Set α)) ↦
                  {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
                {u : Set (Set α) | u.Finite ∧ u ⊆ B})
              v ∧
            K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty})
    (hw : ¬w.Finite),
    ∃ (v : Set (Compacts α)),
      Membership.mem (γ := Set (Set (Compacts α)))
          ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
            {u : Set (Set α) | u.Finite ∧ u ⊆ B})
          v ∧
        K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
⊢ ∃ (v : Set (Compacts α)),
    Membership.mem (γ := Set (Set (Compacts α)))
        ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
          {u : Set (Set α) | u.Finite ∧ u ⊆ B})
        v ∧
      K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
have wlog : ∀ (w : Set (Set α)) (hKV : (↑K : Set α) ⊆ ⋃₀ w) (hwB : w ⊆ B) (hwV : ⋃₀ w ⊆ V)
  (hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty) (hw : w.Finite),
  ∃ (v : Set (Compacts α)),
    Membership.mem (γ := Set (Set (Compacts α)))
        ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
          {u : Set (Set α) | u.Finite ∧ u ⊆ B})
        v ∧
      K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
Tactic: wlog hw : w.Finite generalizing w
Cleared hypotheses: w, hKV, hwB, hwV, hwK
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
V : Set α
u : Set (Set α)
hV : IsOpen[inst] V
hu : u.Finite
huB : u ⊆ B
huV : ∀ U ∈ u, U ⊆ V
K : Compacts α
hKu : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
w : Set (Set α)
hKV : (↑K : Set α) ⊆ ⋃₀ w
hwB : w ⊆ B
hwV : ⋃₀ w ⊆ V
hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty
this :
  ∀ (w : Set (Set α)) (hKV : (↑K : Set α) ⊆ ⋃₀ w) (hwB : w ⊆ B) (hwV : ⋃₀ w ⊆ V)
    (hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty) (hw : w.Finite),
    ∃ (v : Set (Compacts α)),
      Membership.mem (γ := Set (Set (Compacts α)))
          ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
            {u : Set (Set α) | u.Finite ∧ u ⊆ B})
          v ∧
        K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
hw : ¬w.Finite
⊢ ∃ (v : Set (Compacts α)),
    Membership.mem (γ := Set (Set (Compacts α)))
        ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
          {u : Set (Set α) | u.Finite ∧ u ⊆ B})
        v ∧
      K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
have hKV₁ : (↑K : Set α) ⊆ ⋃ i ∈ w, i
Tactic: rw [sUnion_eq_biUnion] at hKV
Cleared hypotheses: hKV, hwB, hwV, hwK, this, hw
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
V : Set α
u : Set (Set α)
hV : IsOpen[inst] V
hu : u.Finite
huB : u ⊆ B
huV : ∀ U ∈ u, U ⊆ V
K : Compacts α
hKu : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
w : Set (Set α)
hKV : (↑K : Set α) ⊆ ⋃ i ∈ w, i
hwB : w ⊆ B
hwV : ⋃₀ w ⊆ V
hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty
this :
  ∀ (w : Set (Set α)) (hKV : (↑K : Set α) ⊆ ⋃₀ w) (hwB : w ⊆ B) (hwV : ⋃₀ w ⊆ V)
    (hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty) (hw : w.Finite),
    ∃ (v : Set (Compacts α)),
      Membership.mem (γ := Set (Set (Compacts α)))
          ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
            {u : Set (Set α) | u.Finite ∧ u ⊆ B})
          v ∧
        K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
hw : ¬w.Finite
⊢ ∃ (v : Set (Compacts α)),
    Membership.mem (γ := Set (Set (Compacts α)))
        ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
          {u : Set (Set α) | u.Finite ∧ u ⊆ B})
        v ∧
      K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
have inr : ∀ (w' : Set (Set α)),
  w' ⊆ w ∧ w'.Finite ∧ (↑K : Set α) ⊆ ⋃ i ∈ w', i →
    ∃ (v : Set (Compacts α)),
      Membership.mem (γ := Set (Set (Compacts α)))
          ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
            {u : Set (Set α) | u.Finite ∧ u ⊆ B})
          v ∧
        K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
Tactic: obtain ⟨w', _⟩ := K.isCompact.elim_finite_subcover_image (fun W hW => hB.isOpen (hwB hW)) hKV
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
V : Set α
u : Set (Set α)
hV : IsOpen[inst] V
hu : u.Finite
huB : u ⊆ B
huV : ∀ U ∈ u, U ⊆ V
K : Compacts α
hKu : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
w : Set (Set α)
hKV : (↑K : Set α) ⊆ ⋃ i ∈ w, i
hwB : w ⊆ B
hwV : ⋃₀ w ⊆ V
hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty
this :
  ∀ (w : Set (Set α)) (hKV : (↑K : Set α) ⊆ ⋃₀ w) (hwB : w ⊆ B) (hwV : ⋃₀ w ⊆ V)
    (hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty) (hw : w.Finite),
    ∃ (v : Set (Compacts α)),
      Membership.mem (γ := Set (Set (Compacts α)))
          ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
            {u : Set (Set α) | u.Finite ∧ u ⊆ B})
          v ∧
        K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
hw : ¬w.Finite
w' : Set (Set α)
h : w' ⊆ w ∧ w'.Finite ∧ (↑K : Set α) ⊆ ⋃ i ∈ w', i
⊢ ∃ (v : Set (Compacts α)),
    Membership.mem (γ := Set (Set (Compacts α)))
        ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
          {u : Set (Set α) | u.Finite ∧ u ⊆ B})
        v ∧
      K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
have inr : (↑K : Set α) ⊆ ⋃₀ w'
Tactic: apply this w'
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
V : Set α
u : Set (Set α)
hV : IsOpen[inst] V
hu : u.Finite
huB : u ⊆ B
huV : ∀ U ∈ u, U ⊆ V
K : Compacts α
hKu : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
w : Set (Set α)
hKV : (↑K : Set α) ⊆ ⋃ i ∈ w, i
hwB : w ⊆ B
hwV : ⋃₀ w ⊆ V
hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty
this :
  ∀ (w : Set (Set α)) (hKV : (↑K : Set α) ⊆ ⋃₀ w) (hwB : w ⊆ B) (hwV : ⋃₀ w ⊆ V)
    (hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty) (hw : w.Finite),
    ∃ (v : Set (Compacts α)),
      Membership.mem (γ := Set (Set (Compacts α)))
          ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
            {u : Set (Set α) | u.Finite ∧ u ⊆ B})
          v ∧
        K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
hw : ¬w.Finite
w' : Set (Set α)
h : w' ⊆ w ∧ w'.Finite ∧ (↑K : Set α) ⊆ ⋃ i ∈ w', i
inr : (↑K : Set α) ⊆ ⋃₀ w'
⊢ ∃ (v : Set (Compacts α)),
    Membership.mem (γ := Set (Set (Compacts α)))
        ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
          {u : Set (Set α) | u.Finite ∧ u ⊆ B})
        v ∧
      K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
have inr₁ : w' ⊆ B
Tactic: apply this w'
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
V : Set α
u : Set (Set α)
hV : IsOpen[inst] V
hu : u.Finite
huB : u ⊆ B
huV : ∀ U ∈ u, U ⊆ V
K : Compacts α
hKu : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
w : Set (Set α)
hKV : (↑K : Set α) ⊆ ⋃ i ∈ w, i
hwB : w ⊆ B
hwV : ⋃₀ w ⊆ V
hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty
this :
  ∀ (w : Set (Set α)) (hKV : (↑K : Set α) ⊆ ⋃₀ w) (hwB : w ⊆ B) (hwV : ⋃₀ w ⊆ V)
    (hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty) (hw : w.Finite),
    ∃ (v : Set (Compacts α)),
      Membership.mem (γ := Set (Set (Compacts α)))
          ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
            {u : Set (Set α) | u.Finite ∧ u ⊆ B})
          v ∧
        K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
hw : ¬w.Finite
w' : Set (Set α)
h : w' ⊆ w ∧ w'.Finite ∧ (↑K : Set α) ⊆ ⋃ i ∈ w', i
inr : (↑K : Set α) ⊆ ⋃₀ w'
inr₁ : w' ⊆ B
⊢ ∃ (v : Set (Compacts α)),
    Membership.mem (γ := Set (Set (Compacts α)))
        ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
          {u : Set (Set α) | u.Finite ∧ u ⊆ B})
        v ∧
      K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
have inr₂ : ⋃₀ w' ⊆ V
Tactic: apply this w'
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
V : Set α
u : Set (Set α)
hV : IsOpen[inst] V
hu : u.Finite
huB : u ⊆ B
huV : ∀ U ∈ u, U ⊆ V
K : Compacts α
hKu : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
w : Set (Set α)
hKV : (↑K : Set α) ⊆ ⋃ i ∈ w, i
hwB : w ⊆ B
hwV : ⋃₀ w ⊆ V
hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty
this :
  ∀ (w : Set (Set α)) (hKV : (↑K : Set α) ⊆ ⋃₀ w) (hwB : w ⊆ B) (hwV : ⋃₀ w ⊆ V)
    (hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty) (hw : w.Finite),
    ∃ (v : Set (Compacts α)),
      Membership.mem (γ := Set (Set (Compacts α)))
          ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
            {u : Set (Set α) | u.Finite ∧ u ⊆ B})
          v ∧
        K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
hw : ¬w.Finite
w' : Set (Set α)
h : w' ⊆ w ∧ w'.Finite ∧ (↑K : Set α) ⊆ ⋃ i ∈ w', i
inr : (↑K : Set α) ⊆ ⋃₀ w'
inr₁ : w' ⊆ B
inr₂ : ⋃₀ w' ⊆ V
⊢ ∃ (v : Set (Compacts α)),
    Membership.mem (γ := Set (Set (Compacts α)))
        ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
          {u : Set (Set α) | u.Finite ∧ u ⊆ B})
        v ∧
      K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
have inr₃ : ∀ W ∈ w', ((↑K : Set α) ∩ W).Nonempty
Tactic: apply this w'
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
V : Set α
u : Set (Set α)
hV : IsOpen[inst] V
hu : u.Finite
huB : u ⊆ B
huV : ∀ U ∈ u, U ⊆ V
K : Compacts α
hKu : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
w : Set (Set α)
hKV : (↑K : Set α) ⊆ ⋃ i ∈ w, i
hwB : w ⊆ B
hwV : ⋃₀ w ⊆ V
hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty
this :
  ∀ (w : Set (Set α)) (hKV : (↑K : Set α) ⊆ ⋃₀ w) (hwB : w ⊆ B) (hwV : ⋃₀ w ⊆ V)
    (hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty) (hw : w.Finite),
    ∃ (v : Set (Compacts α)),
      Membership.mem (γ := Set (Set (Compacts α)))
          ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
            {u : Set (Set α) | u.Finite ∧ u ⊆ B})
          v ∧
        K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
hw : ¬w.Finite
w' : Set (Set α)
h : w' ⊆ w ∧ w'.Finite ∧ (↑K : Set α) ⊆ ⋃ i ∈ w', i
inr : (↑K : Set α) ⊆ ⋃₀ w'
inr₁ : w' ⊆ B
inr₂ : ⋃₀ w' ⊆ V
inr₃ : ∀ W ∈ w', ((↑K : Set α) ∩ W).Nonempty
⊢ ∃ (v : Set (Compacts α)),
    Membership.mem (γ := Set (Set (Compacts α)))
        ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
          {u : Set (Set α) | u.Finite ∧ u ⊆ B})
        v ∧
      K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
have inr₄ : w'.Finite
Tactic: apply this w'
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
V : Set α
u : Set (Set α)
hV : IsOpen[inst] V
hu : u.Finite
huB : u ⊆ B
huV : ∀ U ∈ u, U ⊆ V
K : Compacts α
hKu : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
w : Set (Set α)
hKV : (↑K : Set α) ⊆ ⋃₀ w
hwB : w ⊆ B
hwV : ⋃₀ w ⊆ V
hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty
hw : w.Finite
⊢ ∃ (v : Set (Compacts α)),
    Membership.mem (γ := Set (Set (Compacts α)))
        ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
          {u : Set (Set α) | u.Finite ∧ u ⊆ B})
        v ∧
      K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
have inr : ∀
  (this :
    ∀ (w : Set (Set α)) (hKV : (↑K : Set α) ⊆ ⋃₀ w) (hwB : w ⊆ B) (hwV : ⋃₀ w ⊆ V)
      (hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty) (hw : w.Finite) (huw : u ⊆ w),
      ∃ (v : Set (Compacts α)),
        Membership.mem (γ := Set (Set (Compacts α)))
            ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
              {u : Set (Set α) | u.Finite ∧ u ⊆ B})
            v ∧
          K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty})
  (huw : ¬u ⊆ w),
  ∃ (v : Set (Compacts α)),
    Membership.mem (γ := Set (Set (Compacts α)))
        ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
          {u : Set (Set α) | u.Finite ∧ u ⊆ B})
        v ∧
      K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
Tactic: wlog huw : u ⊆ w generalizing w
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
V : Set α
u : Set (Set α)
hV : IsOpen[inst] V
hu : u.Finite
huB : u ⊆ B
huV : ∀ U ∈ u, U ⊆ V
K : Compacts α
hKu : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
w : Set (Set α)
hKV : (↑K : Set α) ⊆ ⋃₀ w
hwB : w ⊆ B
hwV : ⋃₀ w ⊆ V
hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty
hw : w.Finite
inr :
  ∀
    (this :
      ∀ (w : Set (Set α)) (hKV : (↑K : Set α) ⊆ ⋃₀ w) (hwB : w ⊆ B) (hwV : ⋃₀ w ⊆ V)
        (hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty) (hw : w.Finite) (huw : u ⊆ w),
        ∃ (v : Set (Compacts α)),
          Membership.mem (γ := Set (Set (Compacts α)))
              ((fun (u : Set (Set α)) ↦
                  {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
                {u : Set (Set α) | u.Finite ∧ u ⊆ B})
              v ∧
            K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty})
    (huw : ¬u ⊆ w),
    ∃ (v : Set (Compacts α)),
      Membership.mem (γ := Set (Set (Compacts α)))
          ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
            {u : Set (Set α) | u.Finite ∧ u ⊆ B})
          v ∧
        K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
⊢ ∃ (v : Set (Compacts α)),
    Membership.mem (γ := Set (Set (Compacts α)))
        ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
          {u : Set (Set α) | u.Finite ∧ u ⊆ B})
        v ∧
      K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
have wlog : ∀ (w : Set (Set α)) (hKV : (↑K : Set α) ⊆ ⋃₀ w) (hwB : w ⊆ B) (hwV : ⋃₀ w ⊆ V)
  (hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty) (hw : w.Finite) (huw : u ⊆ w),
  ∃ (v : Set (Compacts α)),
    Membership.mem (γ := Set (Set (Compacts α)))
        ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
          {u : Set (Set α) | u.Finite ∧ u ⊆ B})
        v ∧
      K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
Tactic: wlog huw : u ⊆ w generalizing w
Cleared hypotheses: w, hKV, hwB, hwV, hwK, hw