-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Lemmas (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
h : X ≃ₜ Y
x : X
hx : x ∈ s
this :
  Subset.{u_1} (α := Set X)
    (image.{u_2, u_1} (α := Y) ((⇑h.symm : (a : Y) → X) : (a : Y) → X)
        (connectedComponentIn ((⇑h : (a : X) → Y) '' s) ((h : (a : X) → Y) x) : Set Y) :
      Set X)
    (connectedComponentIn (image.{u_2, u_1} (α := Y) (⇑h.symm : (a : Y) → X) ((⇑h : (a : X) → Y) '' s))
        ((h.symm : (a : Y) → X) ((h : (a : X) → Y) x : Y)) :
      Set X)
rwa :
  ∀
    (this :
      Subset.{u_2} (α := Set Y) (connectedComponentIn ((⇑h : (a : X) → Y) '' s) ((h : (a : X) → Y) x) : Set Y)
        (preimage.{u_2, u_1} (β := X) ((⇑h.symm : (a : Y) → X) : (a : Y) → X)
            (connectedComponentIn (image.{u_2, u_1} (α := Y) (⇑h.symm : (a : Y) → X) ((⇑h : (a : X) → Y) '' s))
                ((h.symm : (a : Y) → X) ((h : (a : X) → Y) x : Y)) :
              Set X) :
          Set Y)),
    Subset.{u_2} (α := Set Y) (connectedComponentIn ((⇑h : (a : X) → Y) '' s) ((h : (a : X) → Y) x) : Set Y)
      ((⇑h : (a : X) → Y) '' connectedComponentIn s x : Set Y)
rwa₁ :
  ∀
    (this :
      Subset.{u_2} (α := Set Y) (connectedComponentIn ((⇑h : (a : X) → Y) '' s) ((h : (a : X) → Y) x) : Set Y)
        (image.{u_1, u_2} (α := X) ((⇑h : (a : X) → Y) : (a : X) → Y)
            (connectedComponentIn (image.{u_2, u_1} (α := Y) (⇑h.symm : (a : Y) → X) ((⇑h : (a : X) → Y) '' s))
                ((h.symm : (a : Y) → X) ((h : (a : X) → Y) x : Y)) :
              Set X) :
          Set Y)),
    Subset.{u_2} (α := Set Y) (connectedComponentIn ((⇑h : (a : X) → Y) '' s) ((h : (a : X) → Y) x) : Set Y)
      ((⇑h : (a : X) → Y) '' connectedComponentIn s x : Set Y)
rwa₂ :
  ∀
    (this :
      Subset.{u_2} (α := Set Y) (connectedComponentIn ((⇑h : (a : X) → Y) '' s) ((h : (a : X) → Y) x) : Set Y)
        (image.{u_1, u_2} (α := X) ((⇑h : (a : X) → Y) : (a : X) → Y)
            (connectedComponentIn (preimage.{u_1, u_2} (β := Y) (⇑h : (a : X) → Y) ((⇑h : (a : X) → Y) '' s))
                ((h.symm : (a : Y) → X) ((h : (a : X) → Y) x : Y)) :
              Set X) :
          Set Y)),
    Subset.{u_2} (α := Set Y) (connectedComponentIn ((⇑h : (a : X) → Y) '' s) ((h : (a : X) → Y) x) : Set Y)
      ((⇑h : (a : X) → Y) '' connectedComponentIn s x : Set Y)
rwa₃ :
  ∀
    (this :
      Subset.{u_2} (α := Set Y) (connectedComponentIn ((⇑h : (a : X) → Y) '' s) ((h : (a : X) → Y) x) : Set Y)
        ((⇑h : (a : X) → Y) '' connectedComponentIn s ((h.symm : (a : Y) → X) ((h : (a : X) → Y) x : Y)) : Set Y)),
    Subset.{u_2} (α := Set Y) (connectedComponentIn ((⇑h : (a : X) → Y) '' s) ((h : (a : X) → Y) x) : Set Y)
      ((⇑h : (a : X) → Y) '' connectedComponentIn s x : Set Y)
⊢ Subset.{u_2} (α := Set Y) (connectedComponentIn ((⇑h : (a : X) → Y) '' s) ((h : (a : X) → Y) x) : Set Y)
    ((⇑h : (a : X) → Y) '' connectedComponentIn s x : Set Y)
have rwa₄ : ∀
  (this :
    Subset.{u_2} (α := Set Y) (connectedComponentIn ((⇑h : (a : X) → Y) '' s) ((h : (a : X) → Y) x) : Set Y)
      ((⇑h : (a : X) → Y) '' connectedComponentIn s x : Set Y)),
  Subset.{u_2} (α := Set Y) (connectedComponentIn ((⇑h : (a : X) → Y) '' s) ((h : (a : X) → Y) x) : Set Y)
    ((⇑h : (a : X) → Y) '' connectedComponentIn s x : Set Y)
Tactic: rwa [image_subset_iff, h.preimage_symm, h.image_symm, h.preimage_image, h.symm_apply_apply]
    at this
Cleared hypotheses: this