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
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
s : Set α
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty} s →
    ∃ (v : Set (Set α)),
      Membership.mem (γ := Set (Set (Set α)))
          ((fun (p : Set α × Set (Set α)) ↦ {s : Set α | s ⊆ p.1 ∧ ∀ U ∈ p.2, (s ∩ U).Nonempty}) ''
            {p : Set α × Set (Set α) | IsOpen[inst] p.1 ∧ p.2.Finite ∧ p.2 ⊆ B ∧ ∀ U ∈ p.2, U ⊆ p.1})
          v ∧
        s ∈ v ∧ v ⊆ {s : Set α | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
have refine_2 : ∀ (hs₁ : s ⊆ ⋃₀ u) (hs₂ : ∀ U ∈ u, (s ∩ U).Nonempty),
  ∃ (v : Set (Set α)),
    Membership.mem (γ := Set (Set (Set α)))
        ((fun (p : Set α × Set (Set α)) ↦ {s : Set α | s ⊆ p.1 ∧ ∀ U ∈ p.2, (s ∩ U).Nonempty}) ''
          {p : Set α × Set (Set α) | IsOpen[inst] p.1 ∧ p.2.Finite ∧ p.2 ⊆ B ∧ ∀ U ∈ p.2, U ⊆ p.1})
        v ∧
      s ∈ v ∧ v ⊆ {s : Set α | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
Tactic: ⟨hs₁, hs₂⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
s : Set α
hs₁ : s ⊆ ⋃₀ u
hs₂ : ∀ U ∈ u, (s ∩ U).Nonempty
U : Set α
hU : U ∈ u
⊢ ∃ W ∈ B, W ⊆ U ∧ (s ∩ W).Nonempty
have obtain : ∀ (x : α) (hxs : x ∈ s) (hxU : x ∈ U), ∃ W ∈ B, W ⊆ U ∧ (s ∩ W).Nonempty
Tactic: obtain ⟨x, hxs, hxU⟩ := hs₂ U hU
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
s : Set α
hs₁ : s ⊆ ⋃₀ u
hs₂ : ∀ U ∈ u, (s ∩ U).Nonempty
U : Set α
hU : U ∈ u
x : α
hxs : x ∈ s
hxU : x ∈ U
⊢ ∃ W ∈ B, W ⊆ U ∧ (s ∩ W).Nonempty
have obtain : ∀ (W : Set α) (hWB : W ∈ B) (hxW : x ∈ W) (hW : W ⊆ U), ∃ W ∈ B, W ⊆ U ∧ (s ∩ W).Nonempty
Tactic: obtain ⟨W, hWB, hxW, hW⟩ := hB.exists_subset_of_mem_open hxU <| hu₂ U hU
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
s : Set α
hs₁ : s ⊆ ⋃₀ u
hs₂ : ∀ U ∈ u, (s ∩ U).Nonempty
⊢ ∃ (v : Set (Set α)),
    Membership.mem (γ := Set (Set (Set α)))
        ((fun (p : Set α × Set (Set α)) ↦ {s : Set α | s ⊆ p.1 ∧ ∀ U ∈ p.2, (s ∩ U).Nonempty}) ''
          {p : Set α × Set (Set α) | IsOpen[inst] p.1 ∧ p.2.Finite ∧ p.2 ⊆ B ∧ ∀ U ∈ p.2, U ⊆ p.1})
        v ∧
      s ∈ v ∧ v ⊆ {s : Set α | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
have refine_2 : ∀ (f : (U : Set α) → Set α) (hfB : ∀ U ∈ u, f U ∈ B) (hfU : ∀ U ∈ u, f U ⊆ U) (hfs : ∀ U ∈ u, (s ∩ f U).Nonempty),
  ∃ (v : Set (Set α)),
    Membership.mem (γ := Set (Set (Set α)))
        ((fun (p : Set α × Set (Set α)) ↦ {s : Set α | s ⊆ p.1 ∧ ∀ U ∈ p.2, (s ∩ U).Nonempty}) ''
          {p : Set α × Set (Set α) | IsOpen[inst] p.1 ∧ p.2.Finite ∧ p.2 ⊆ B ∧ ∀ U ∈ p.2, U ⊆ p.1})
        v ∧
      s ∈ v ∧ v ⊆ {s : Set α | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
Tactic: choose! f hfB hfU hfs using show ∀ U ∈ u, ∃ W ∈ B, W ⊆ U ∧ (s ∩ W).Nonempty by
      intro U hU
      obtain ⟨x, hxs, hxU⟩ := hs₂ U hU
      obtain ⟨W, hWB, hxW, hW⟩ := hB.exists_subset_of_mem_open hxU <| hu₂ U hU
      exact ⟨W, hWB, hW, x, hxs, hxW⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
s : Set α
hs₁ : s ⊆ ⋃₀ u
hs₂ : ∀ U ∈ u, (s ∩ U).Nonempty
f : (U : Set α) → Set α
hfB : ∀ U ∈ u, f U ∈ B
hfU : ∀ U ∈ u, f U ⊆ U
hfs : ∀ U ∈ u, (s ∩ f U).Nonempty
⊢ ∃ (v : Set (Set α)),
    Membership.mem (γ := Set (Set (Set α)))
        ((fun (p : Set α × Set (Set α)) ↦ {s : Set α | s ⊆ p.1 ∧ ∀ U ∈ p.2, (s ∩ U).Nonempty}) ''
          {p : Set α × Set (Set α) | IsOpen[inst] p.1 ∧ p.2.Finite ∧ p.2 ⊆ B ∧ ∀ U ∈ p.2, U ⊆ p.1})
        v ∧
      s ∈ v ∧ v ⊆ {s : Set α | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
have refine_2 : ∃ (x : Set α × Set (Set α)),
  Membership.mem (γ := Set (Set α × Set (Set α)))
      {p : Set α × Set (Set α) | IsOpen[inst] p.1 ∧ p.2.Finite ∧ p.2 ⊆ B ∧ ∀ U ∈ p.2, U ⊆ p.1} x ∧
    Membership.mem (γ := Set (Set α)) {s : Set α | s ⊆ x.1 ∧ ∀ U ∈ x.2, (s ∩ U).Nonempty} s ∧
      Subset.{u_1} (α := Set (Set α)) {s : Set α | s ⊆ x.1 ∧ ∀ U ∈ x.2, (s ∩ U).Nonempty}
        {s : Set α | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
Tactic: rw [exists_mem_image]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
s : Set α
hs₁ : s ⊆ ⋃₀ u
hs₂ : ∀ U ∈ u, (s ∩ U).Nonempty
f : (U : Set α) → Set α
hfB : ∀ U ∈ u, f U ∈ B
hfU : ∀ U ∈ u, f U ⊆ U
hfs : ∀ U ∈ u, (s ∩ f U).Nonempty
⊢ ∃ (x : Set α × Set (Set α)),
    Membership.mem (γ := Set (Set α × Set (Set α)))
        {p : Set α × Set (Set α) | IsOpen[inst] p.1 ∧ p.2.Finite ∧ p.2 ⊆ B ∧ ∀ U ∈ p.2, U ⊆ p.1} x ∧
      Membership.mem (γ := Set (Set α)) {s : Set α | s ⊆ x.1 ∧ ∀ U ∈ x.2, (s ∩ U).Nonempty} s ∧
        Subset.{u_1} (α := Set (Set α)) {s : Set α | s ⊆ x.1 ∧ ∀ U ∈ x.2, (s ∩ U).Nonempty}
          {s : Set α | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
have refine_2 : ∀ (t : Set α),
  Membership.mem (γ := Set (Set α)) {s : Set α | s ⊆ (⋃₀ u, f '' u).1 ∧ ∀ U ∈ (⋃₀ u, f '' u).2, (s ∩ U).Nonempty} t →
    ∀ (ht₁ : t ⊆ (⋃₀ u, f '' u).1) (ht₂ : ∀ U ∈ (⋃₀ u, f '' u).2, (t ∩ U).Nonempty) (U : Set α) (hU : U ∈ u),
      (t ∩ U).Nonempty
Tactic: refine ⟨⟨⋃₀ u, f '' u⟩, ⟨isOpen_sUnion hu₂, hu₁.image _, by grind⟩, by grind,
      fun t ⟨ht₁, ht₂⟩ => ⟨ht₁, fun U hU => ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
s : Set α
hs₁ : s ⊆ ⋃₀ u
hs₂ : ∀ U ∈ u, (s ∩ U).Nonempty
f : (U : Set α) → Set α
hfB : ∀ U ∈ u, f U ∈ B
hfU : ∀ U ∈ u, f U ⊆ U
hfs : ∀ U ∈ u, (s ∩ f U).Nonempty
t : Set α
h : Membership.mem (γ := Set (Set α)) {s : Set α | s ⊆ (⋃₀ u, f '' u).1 ∧ ∀ U ∈ (⋃₀ u, f '' u).2, (s ∩ U).Nonempty} t
ht₁ : t ⊆ (⋃₀ u, f '' u).1
ht₂ : ∀ U ∈ (⋃₀ u, f '' u).2, (t ∩ U).Nonempty
U : Set α
hU : U ∈ u
⊢ (t ∩ U).Nonempty
have refine_2 : ∀ (ht₂ : ∀ ⦃x : Set α⦄, x ∈ u → (t ∩ f x).Nonempty) (U : Set α) (hU : U ∈ u), (t ∩ U).Nonempty
Tactic: rw [forall_mem_image] at ht₂
Cleared hypotheses: ht₂, U, hU
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
s : Set α
hs₁ : s ⊆ ⋃₀ u
hs₂ : ∀ U ∈ u, (s ∩ U).Nonempty
f : (U : Set α) → Set α
hfB : ∀ U ∈ u, f U ∈ B
hfU : ∀ U ∈ u, f U ⊆ U
hfs : ∀ U ∈ u, (s ∩ f U).Nonempty
t : Set α
h : Membership.mem (γ := Set (Set α)) {s : Set α | s ⊆ (⋃₀ u, f '' u).1 ∧ ∀ U ∈ (⋃₀ u, f '' u).2, (s ∩ U).Nonempty} t
ht₁ : t ⊆ (⋃₀ u, f '' u).1
ht₂ : ∀ ⦃x : Set α⦄, x ∈ u → (t ∩ f x).Nonempty
U : Set α
hU : U ∈ u
⊢ (t ∩ U).Nonempty
have refine_2 : (t ∩ f U).Nonempty
Tactic: grw [← hfU U hU]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
⊢ Continuous[inst, TopologicalSpace.vietoris β] f ↔
    (∀ (U : Set β), IsOpen[inst_1] U → IsOpen[inst] (f ⁻¹' 𝒫 U)) ∧
      ∀ (F : Set β), IsClosed[inst_1] F → IsClosed[inst] (f ⁻¹' 𝒫 F)
have refine : ((∀ (U : Set β), IsOpen[inst_1] U → IsOpen[inst] (f ⁻¹' 𝒫 U)) ∧
    ∀ (F : Set β), IsClosed[inst_1] F → IsClosed[inst] (f ⁻¹' 𝒫 F)) →
  ∀ (h₁ : ∀ (U : Set β), IsOpen[inst_1] U → IsOpen[inst] (f ⁻¹' 𝒫 U))
    (h₂ : ∀ (F : Set β), IsClosed[inst_1] F → IsClosed[inst] (f ⁻¹' 𝒫 F)),
    Continuous[inst, TopologicalSpace.vietoris β] f
Tactic: refine ⟨fun hf =>
      ⟨fun U hU => hU.powerset_vietoris.preimage hf, fun F hF => hF.powerset_vietoris.preimage hf⟩,
    fun ⟨h₁, h₂⟩ => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
h :
  (∀ (U : Set β), IsOpen[inst_1] U → IsOpen[inst] (f ⁻¹' 𝒫 U)) ∧
    ∀ (F : Set β), IsClosed[inst_1] F → IsClosed[inst] (f ⁻¹' 𝒫 F)
h₁ : ∀ (U : Set β), IsOpen[inst_1] U → IsOpen[inst] (f ⁻¹' 𝒫 U)
h₂ : ∀ (F : Set β), IsClosed[inst_1] F → IsClosed[inst] (f ⁻¹' 𝒫 F)
⊢ Continuous[inst, TopologicalSpace.vietoris β] f
have rw : ∀ (s : Set (Set β)),
  Membership.mem (γ := Set (Set (Set β)))
      (powerset '' {U : Set β | IsOpen[inst_1] U} ∪
        (fun (V : Set β) ↦ {s : Set β | (s ∩ V).Nonempty}) '' {V : Set β | IsOpen[inst_1] V})
      s →
    IsOpen[inst] (f ⁻¹' s)
Tactic: rw [continuous_generateFrom_iff]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
h :
  (∀ (U : Set β), IsOpen[inst_1] U → IsOpen[inst] (f ⁻¹' 𝒫 U)) ∧
    ∀ (F : Set β), IsClosed[inst_1] F → IsClosed[inst] (f ⁻¹' 𝒫 F)
h₁ : ∀ (U : Set β), IsOpen[inst_1] U → IsOpen[inst] (f ⁻¹' 𝒫 U)
h₂ : ∀ (F : Set β), IsClosed[inst_1] F → IsClosed[inst] (f ⁻¹' 𝒫 F)
U : Set β
hU : Membership.mem (γ := Set (Set β)) {V : Set β | IsOpen[inst_1] V} U
⊢ IsOpen[inst] (f ⁻¹' (fun (V : Set β) ↦ ({s : Set β | (s ∩ V).Nonempty} : Set (Set β))) U)
have inr : IsClosed[inst] {a : α | f a ⊆ Uᶜ}
Tactic: simp_rw [preimage_setOf_eq, ← not_disjoint_iff_nonempty_inter, ← compl_setOf, isOpen_compl_iff,
      ← subset_compl_iff_disjoint_right]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ inst = induced (fun (x : α) ↦ {x}) (TopologicalSpace.vietoris α)
have simp_rw : inst =
  induced (Y := Set α) (fun (x : α) ↦ {x})
    (generateFrom
      (powerset '' {U : Set α | IsOpen[inst] U} ∪
        (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {U : Set α | IsOpen[inst] U}))
Tactic: simp_rw [TopologicalSpace.vietoris, induced_generateFrom_eq, image_union, image_image,
      powerset, preimage_setOf_eq, singleton_subset_iff, singleton_inter_nonempty, union_self,
      setOf_mem_eq, image_id', generateFrom_setOf_isOpen]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
simp_rw :
  inst =
    induced (Y := Set α) (fun (x : α) ↦ {x})
      (generateFrom
        (powerset '' {U : Set α | IsOpen[inst] U} ∪
          (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {U : Set α | IsOpen[inst] U}))
⊢ inst = induced (fun (x : α) ↦ {x}) (TopologicalSpace.vietoris α)
have simp_rw₁ : inst =
  generateFrom
    (image (α := Set (Set α)) (preimage fun (x : α) ↦ {x})
      (powerset '' {U : Set α | IsOpen[inst] U} ∪
        (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {U : Set α | IsOpen[inst] U}))
Tactic: simp_rw [TopologicalSpace.vietoris, induced_generateFrom_eq, image_union, image_image,
      powerset, preimage_setOf_eq, singleton_subset_iff, singleton_inter_nonempty, union_self,
      setOf_mem_eq, image_id', generateFrom_setOf_isOpen]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
simp_rw :
  inst =
    induced (Y := Set α) (fun (x : α) ↦ {x})
      (generateFrom
        (powerset '' {U : Set α | IsOpen[inst] U} ∪
          (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {U : Set α | IsOpen[inst] U}))
simp_rw₁ :
  inst =
    generateFrom
      (image (α := Set (Set α)) (preimage fun (x : α) ↦ {x})
        (powerset '' {U : Set α | IsOpen[inst] U} ∪
          (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {U : Set α | IsOpen[inst] U}))
⊢ inst = induced (fun (x : α) ↦ {x}) (TopologicalSpace.vietoris α)
have simp_rw₂ : inst =
  generateFrom
    (image (α := Set (Set α)) (preimage fun (x : α) ↦ {x}) (powerset '' {U : Set α | IsOpen[inst] U}) ∪
      image (α := Set (Set α)) (preimage fun (x : α) ↦ {x})
        ((fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {U : Set α | IsOpen[inst] U}))
Tactic: simp_rw [TopologicalSpace.vietoris, induced_generateFrom_eq, image_union, image_image,
      powerset, preimage_setOf_eq, singleton_subset_iff, singleton_inter_nonempty, union_self,
      setOf_mem_eq, image_id', generateFrom_setOf_isOpen]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
simp_rw :
  inst =
    induced (Y := Set α) (fun (x : α) ↦ {x})
      (generateFrom
        (powerset '' {U : Set α | IsOpen[inst] U} ∪
          (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {U : Set α | IsOpen[inst] U}))
simp_rw₁ :
  inst =
    generateFrom
      (image (α := Set (Set α)) (preimage fun (x : α) ↦ {x})
        (powerset '' {U : Set α | IsOpen[inst] U} ∪
          (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {U : Set α | IsOpen[inst] U}))
simp_rw₂ :
  inst =
    generateFrom
      (image (α := Set (Set α)) (preimage fun (x : α) ↦ {x}) (powerset '' {U : Set α | IsOpen[inst] U}) ∪
        image (α := Set (Set α)) (preimage fun (x : α) ↦ {x})
          ((fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {U : Set α | IsOpen[inst] U}))
⊢ inst = induced (fun (x : α) ↦ {x}) (TopologicalSpace.vietoris α)
have simp_rw₃ : inst =
  generateFrom
    ((fun (x : Set α) ↦ (fun (x : α) ↦ {x}) ⁻¹' 𝒫 x) '' {U : Set α | IsOpen[inst] U} ∪
      (fun (x : Set α) ↦ preimage (β := Set α) (fun (x : α) ↦ {x}) {s : Set α | (s ∩ x).Nonempty}) ''
        {U : Set α | IsOpen[inst] U})
Tactic: simp_rw [TopologicalSpace.vietoris, induced_generateFrom_eq, image_union, image_image,
      powerset, preimage_setOf_eq, singleton_subset_iff, singleton_inter_nonempty, union_self,
      setOf_mem_eq, image_id', generateFrom_setOf_isOpen]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
simp_rw :
  inst =
    induced (Y := Set α) (fun (x : α) ↦ {x})
      (generateFrom
        (powerset '' {U : Set α | IsOpen[inst] U} ∪
          (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {U : Set α | IsOpen[inst] U}))
simp_rw₁ :
  inst =
    generateFrom
      (image (α := Set (Set α)) (preimage fun (x : α) ↦ {x})
        (powerset '' {U : Set α | IsOpen[inst] U} ∪
          (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {U : Set α | IsOpen[inst] U}))
simp_rw₂ :
  inst =
    generateFrom
      (image (α := Set (Set α)) (preimage fun (x : α) ↦ {x}) (powerset '' {U : Set α | IsOpen[inst] U}) ∪
        image (α := Set (Set α)) (preimage fun (x : α) ↦ {x})
          ((fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {U : Set α | IsOpen[inst] U}))
simp_rw₃ :
  inst =
    generateFrom
      ((fun (x : Set α) ↦ (fun (x : α) ↦ {x}) ⁻¹' 𝒫 x) '' {U : Set α | IsOpen[inst] U} ∪
        (fun (x : Set α) ↦ preimage (β := Set α) (fun (x : α) ↦ {x}) {s : Set α | (s ∩ x).Nonempty}) ''
          {U : Set α | IsOpen[inst] U})
⊢ inst = induced (fun (x : α) ↦ {x}) (TopologicalSpace.vietoris α)
have simp_rw₄ : inst =
  generateFrom
    ((fun (a : Set α) ↦ preimage (β := Set α) (fun (x : α) ↦ {x}) {t : Set α | t ⊆ a}) '' {U : Set α | IsOpen[inst] U} ∪
      (fun (x : Set α) ↦ preimage (β := Set α) (fun (x : α) ↦ {x}) {s : Set α | (s ∩ x).Nonempty}) ''
        {U : Set α | IsOpen[inst] U})
Tactic: simp_rw [TopologicalSpace.vietoris, induced_generateFrom_eq, image_union, image_image,
      powerset, preimage_setOf_eq, singleton_subset_iff, singleton_inter_nonempty, union_self,
      setOf_mem_eq, image_id', generateFrom_setOf_isOpen]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
simp_rw :
  inst =
    induced (Y := Set α) (fun (x : α) ↦ {x})
      (generateFrom
        (powerset '' {U : Set α | IsOpen[inst] U} ∪
          (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {U : Set α | IsOpen[inst] U}))
simp_rw₁ :
  inst =
    generateFrom
      (image (α := Set (Set α)) (preimage fun (x : α) ↦ {x})
        (powerset '' {U : Set α | IsOpen[inst] U} ∪
          (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {U : Set α | IsOpen[inst] U}))
simp_rw₂ :
  inst =
    generateFrom
      (image (α := Set (Set α)) (preimage fun (x : α) ↦ {x}) (powerset '' {U : Set α | IsOpen[inst] U}) ∪
        image (α := Set (Set α)) (preimage fun (x : α) ↦ {x})
          ((fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {U : Set α | IsOpen[inst] U}))
simp_rw₃ :
  inst =
    generateFrom
      ((fun (x : Set α) ↦ (fun (x : α) ↦ {x}) ⁻¹' 𝒫 x) '' {U : Set α | IsOpen[inst] U} ∪
        (fun (x : Set α) ↦ preimage (β := Set α) (fun (x : α) ↦ {x}) {s : Set α | (s ∩ x).Nonempty}) ''
          {U : Set α | IsOpen[inst] U})
simp_rw₄ :
  inst =
    generateFrom
      ((fun (a : Set α) ↦ preimage (β := Set α) (fun (x : α) ↦ {x}) {t : Set α | t ⊆ a}) ''
          {U : Set α | IsOpen[inst] U} ∪
        (fun (x : Set α) ↦ preimage (β := Set α) (fun (x : α) ↦ {x}) {s : Set α | (s ∩ x).Nonempty}) ''
          {U : Set α | IsOpen[inst] U})
⊢ inst = induced (fun (x : α) ↦ {x}) (TopologicalSpace.vietoris α)
have simp_rw₅ : inst =
  generateFrom
    ((fun (a : Set α) ↦ {a_1 : α | {a_1} ⊆ a}) '' {U : Set α | IsOpen[inst] U} ∪
      (fun (a : Set α) ↦ {a_1 : α | ({a_1} ∩ a).Nonempty}) '' {U : Set α | IsOpen[inst] U})
Tactic: simp_rw [TopologicalSpace.vietoris, induced_generateFrom_eq, image_union, image_image,
      powerset, preimage_setOf_eq, singleton_subset_iff, singleton_inter_nonempty, union_self,
      setOf_mem_eq, image_id', generateFrom_setOf_isOpen]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
simp_rw :
  inst =
    induced (Y := Set α) (fun (x : α) ↦ {x})
      (generateFrom
        (powerset '' {U : Set α | IsOpen[inst] U} ∪
          (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {U : Set α | IsOpen[inst] U}))
simp_rw₁ :
  inst =
    generateFrom
      (image (α := Set (Set α)) (preimage fun (x : α) ↦ {x})
        (powerset '' {U : Set α | IsOpen[inst] U} ∪
          (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {U : Set α | IsOpen[inst] U}))
simp_rw₂ :
  inst =
    generateFrom
      (image (α := Set (Set α)) (preimage fun (x : α) ↦ {x}) (powerset '' {U : Set α | IsOpen[inst] U}) ∪
        image (α := Set (Set α)) (preimage fun (x : α) ↦ {x})
          ((fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {U : Set α | IsOpen[inst] U}))
simp_rw₃ :
  inst =
    generateFrom
      ((fun (x : Set α) ↦ (fun (x : α) ↦ {x}) ⁻¹' 𝒫 x) '' {U : Set α | IsOpen[inst] U} ∪
        (fun (x : Set α) ↦ preimage (β := Set α) (fun (x : α) ↦ {x}) {s : Set α | (s ∩ x).Nonempty}) ''
          {U : Set α | IsOpen[inst] U})
simp_rw₄ :
  inst =
    generateFrom
      ((fun (a : Set α) ↦ preimage (β := Set α) (fun (x : α) ↦ {x}) {t : Set α | t ⊆ a}) ''
          {U : Set α | IsOpen[inst] U} ∪
        (fun (x : Set α) ↦ preimage (β := Set α) (fun (x : α) ↦ {x}) {s : Set α | (s ∩ x).Nonempty}) ''
          {U : Set α | IsOpen[inst] U})
simp_rw₅ :
  inst =
    generateFrom
      ((fun (a : Set α) ↦ {a_1 : α | {a_1} ⊆ a}) '' {U : Set α | IsOpen[inst] U} ∪
        (fun (a : Set α) ↦ {a_1 : α | ({a_1} ∩ a).Nonempty}) '' {U : Set α | IsOpen[inst] U})
⊢ inst = induced (fun (x : α) ↦ {x}) (TopologicalSpace.vietoris α)
have simp_rw₆ : inst =
  generateFrom
    ((fun (a : Set α) ↦ {a_1 : α | a_1 ∈ a}) '' {U : Set α | IsOpen[inst] U} ∪
      (fun (a : Set α) ↦ {a_1 : α | ({a_1} ∩ a).Nonempty}) '' {U : Set α | IsOpen[inst] U})
Tactic: simp_rw [TopologicalSpace.vietoris, induced_generateFrom_eq, image_union, image_image,
      powerset, preimage_setOf_eq, singleton_subset_iff, singleton_inter_nonempty, union_self,
      setOf_mem_eq, image_id', generateFrom_setOf_isOpen]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
simp_rw :
  inst =
    induced (Y := Set α) (fun (x : α) ↦ {x})
      (generateFrom
        (powerset '' {U : Set α | IsOpen[inst] U} ∪
          (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {U : Set α | IsOpen[inst] U}))
simp_rw₁ :
  inst =
    generateFrom
      (image (α := Set (Set α)) (preimage fun (x : α) ↦ {x})
        (powerset '' {U : Set α | IsOpen[inst] U} ∪
          (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {U : Set α | IsOpen[inst] U}))
simp_rw₂ :
  inst =
    generateFrom
      (image (α := Set (Set α)) (preimage fun (x : α) ↦ {x}) (powerset '' {U : Set α | IsOpen[inst] U}) ∪
        image (α := Set (Set α)) (preimage fun (x : α) ↦ {x})
          ((fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {U : Set α | IsOpen[inst] U}))
simp_rw₃ :
  inst =
    generateFrom
      ((fun (x : Set α) ↦ (fun (x : α) ↦ {x}) ⁻¹' 𝒫 x) '' {U : Set α | IsOpen[inst] U} ∪
        (fun (x : Set α) ↦ preimage (β := Set α) (fun (x : α) ↦ {x}) {s : Set α | (s ∩ x).Nonempty}) ''
          {U : Set α | IsOpen[inst] U})
simp_rw₄ :
  inst =
    generateFrom
      ((fun (a : Set α) ↦ preimage (β := Set α) (fun (x : α) ↦ {x}) {t : Set α | t ⊆ a}) ''
          {U : Set α | IsOpen[inst] U} ∪
        (fun (x : Set α) ↦ preimage (β := Set α) (fun (x : α) ↦ {x}) {s : Set α | (s ∩ x).Nonempty}) ''
          {U : Set α | IsOpen[inst] U})
simp_rw₅ :
  inst =
    generateFrom
      ((fun (a : Set α) ↦ {a_1 : α | {a_1} ⊆ a}) '' {U : Set α | IsOpen[inst] U} ∪
        (fun (a : Set α) ↦ {a_1 : α | ({a_1} ∩ a).Nonempty}) '' {U : Set α | IsOpen[inst] U})
simp_rw₆ :
  inst =
    generateFrom
      ((fun (a : Set α) ↦ {a_1 : α | a_1 ∈ a}) '' {U : Set α | IsOpen[inst] U} ∪
        (fun (a : Set α) ↦ {a_1 : α | ({a_1} ∩ a).Nonempty}) '' {U : Set α | IsOpen[inst] U})
⊢ inst = induced (fun (x : α) ↦ {x}) (TopologicalSpace.vietoris α)
have simp_rw₇ : inst =
  generateFrom
    ((fun (a : Set α) ↦ {a_1 : α | a_1 ∈ a}) '' {U : Set α | IsOpen[inst] U} ∪
      (fun (a : Set α) ↦ {a_1 : α | a_1 ∈ a}) '' {U : Set α | IsOpen[inst] U})
Tactic: simp_rw [TopologicalSpace.vietoris, induced_generateFrom_eq, image_union, image_image,
      powerset, preimage_setOf_eq, singleton_subset_iff, singleton_inter_nonempty, union_self,
      setOf_mem_eq, image_id', generateFrom_setOf_isOpen]