-- 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})))
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})))
eq_induced₄ :
  Eq.{u_1 + 1} (α := TopologicalSpace (Set α))
    (generateFrom
      ((fun (x : Set β) ↦ 𝒫 (f ⁻¹' x)) '' {V : Set β | IsOpen[inst_1] V} ∪
        (fun (x : Set β) ↦ {s : Set α | (s ∩ f ⁻¹' x).Nonempty}) '' {V : Set β | IsOpen[inst_1] V}))
    (generateFrom
      ((fun (x : Set β) ↦ (fun (x : Set α) ↦ f '' x) ⁻¹' 𝒫 x) '' {V : Set β | IsOpen[inst_1] V} ∪
        (fun (x : Set β) ↦
            preimage.{u_1, u_2} (β := Set β) (fun (x : Set α) ↦ f '' x) {s : Set β | (s ∩ x).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
    ((fun (a : Set β) ↦ {t : Set α | t ⊆ f ⁻¹' a}) '' {V : Set β | IsOpen[inst_1] V} ∪
      (fun (x : Set β) ↦ {s : Set α | (s ∩ f ⁻¹' x).Nonempty}) '' {V : Set β | IsOpen[inst_1] V}))
  (generateFrom
    ((fun (a : Set β) ↦ preimage.{u_1, u_2} (β := Set β) (fun (x : Set α) ↦ f '' x) {t : Set β | t ⊆ a}) ''
        {V : Set β | IsOpen[inst_1] V} ∪
      (fun (x : Set β) ↦ preimage.{u_1, u_2} (β := Set β) (fun (x : Set α) ↦ f '' x) {s : Set β | (s ∩ x).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]