-- Lean 4 proof step from Mathlib.Topology.FiberPartition (goal)
Goal:
S : Type u_1
Y : Type u_2
f : S → Y
inst : TopologicalSpace S
w : (↑(Set.range f) : Type u_2)
val : S
hx :
  val ∈
    (↑(Subtype.mk (p := fun (x : Set S) ↦
          Membership.mem (γ := Set (Set S)) (Set.range fun (x : (↑(Set.range f) : Type u_2)) ↦ f ⁻¹' {(↑x : Y)}) x)
          ((fun (x : (↑(Set.range f) : Type u_2)) ↦ f ⁻¹' {(↑x : Y)}) w) ⋯) :
      Set S)
w_1 : (↑(Set.range f) : Type u_2)
val_1 : S
hy :
  val_1 ∈
    (↑(Subtype.mk (p := fun (x : Set S) ↦
          Membership.mem (γ := Set (Set S)) (Set.range fun (x : (↑(Set.range f) : Type u_2)) ↦ f ⁻¹' {(↑x : Y)}) x)
          ((fun (x : (↑(Set.range f) : Type u_2)) ↦ f ⁻¹' {(↑x : Y)}) w_1) ⋯) :
      Set S)
h :
  Eq (α := S)
    ((sigmaIsoHom f : (a : (x : Fiber f) × (↑(↑x : Set S) : Type u_1)) → S)
        (Sigma.mk (β := fun (x : Fiber f) ↦ (↑(↑x : Set S) : Type u_1))
          (Subtype.mk (p := fun (x : Set S) ↦
            Membership.mem (γ := Set (Set S)) (Set.range fun (x : (↑(Set.range f) : Type u_2)) ↦ f ⁻¹' {(↑x : Y)}) x)
            ((fun (x : (↑(Set.range f) : Type u_2)) ↦ f ⁻¹' {(↑x : Y)}) w) ⋯)
          (Subtype.mk (p := fun (x : S) ↦
            x ∈
              (↑(Subtype.mk (p := fun (x : Set S) ↦
                    Membership.mem (γ := Set (Set S))
                      (Set.range fun (x : (↑(Set.range f) : Type u_2)) ↦ f ⁻¹' {(↑x : Y)}) x)
                    ((fun (x : (↑(Set.range f) : Type u_2)) ↦ f ⁻¹' {(↑x : Y)}) w) ⋯) :
                Set S))
            val hx)) :
      S)
    ((sigmaIsoHom f : (a : (x : Fiber f) × (↑(↑x : Set S) : Type u_1)) → S)
        (Sigma.mk (β := fun (x : Fiber f) ↦ (↑(↑x : Set S) : Type u_1))
          (Subtype.mk (p := fun (x : Set S) ↦
            Membership.mem (γ := Set (Set S)) (Set.range fun (x : (↑(Set.range f) : Type u_2)) ↦ f ⁻¹' {(↑x : Y)}) x)
            ((fun (x : (↑(Set.range f) : Type u_2)) ↦ f ⁻¹' {(↑x : Y)}) w_1) ⋯)
          (Subtype.mk (p := fun (x : S) ↦
            x ∈
              (↑(Subtype.mk (p := fun (x : Set S) ↦
                    Membership.mem (γ := Set (Set S))
                      (Set.range fun (x : (↑(Set.range f) : Type u_2)) ↦ f ⁻¹' {(↑x : Y)}) x)
                    ((fun (x : (↑(Set.range f) : Type u_2)) ↦ f ⁻¹' {(↑x : Y)}) w_1) ⋯) :
                Set S))
            val_1 hy)) :
      S)
⊢ Eq (α := (x : Fiber f) × (↑(↑x : Set S) : Type u_1))
    (Sigma.mk (β := fun (x : Fiber f) ↦ (↑(↑x : Set S) : Type u_1))
        (Subtype.mk (p := fun (x : Set S) ↦
          Membership.mem (γ := Set (Set S)) (Set.range fun (x : (↑(Set.range f) : Type u_2)) ↦ f ⁻¹' {(↑x : Y)}) x)
          ((fun (x : (↑(Set.range f) : Type u_2)) ↦ f ⁻¹' {(↑x : Y)}) w) ⋯)
        (Subtype.mk (p := fun (x : S) ↦
          x ∈
            (↑(Subtype.mk (p := fun (x : Set S) ↦
                  Membership.mem (γ := Set (Set S)) (Set.range fun (x : (↑(Set.range f) : Type u_2)) ↦ f ⁻¹' {(↑x : Y)})
                    x)
                  ((fun (x : (↑(Set.range f) : Type u_2)) ↦ f ⁻¹' {(↑x : Y)}) w) ⋯) :
              Set S))
          val hx) :
      (x : Fiber f) × (↑(↑x : Set S) : Type u_1))
    (Sigma.mk (β := fun (x : Fiber f) ↦ (↑(↑x : Set S) : Type u_1))
        (Subtype.mk (p := fun (x : Set S) ↦
          Membership.mem (γ := Set (Set S)) (Set.range fun (x : (↑(Set.range f) : Type u_2)) ↦ f ⁻¹' {(↑x : Y)}) x)
          ((fun (x : (↑(Set.range f) : Type u_2)) ↦ f ⁻¹' {(↑x : Y)}) w_1) ⋯)
        (Subtype.mk (p := fun (x : S) ↦
          x ∈
            (↑(Subtype.mk (p := fun (x : Set S) ↦
                  Membership.mem (γ := Set (Set S)) (Set.range fun (x : (↑(Set.range f) : Type u_2)) ↦ f ⁻¹' {(↑x : Y)})
                    x)
                  ((fun (x : (↑(Set.range f) : Type u_2)) ↦ f ⁻¹' {(↑x : Y)}) w_1) ⋯) :
              Set S))
          val_1 hy) :
      (x : Fiber f) × (↑(↑x : Set S) : Type u_1))
have refine : Sigma.fst (β := fun (a : Fiber f) ↦ { x : S // x ∈ (↑a : Set S) })
    (Sigma.mk (β := fun (x : Fiber f) ↦ (↑(↑x : Set S) : Type u_1))
      (Subtype.mk (p := fun (x : Set S) ↦
        Membership.mem (γ := Set (Set S)) (Set.range fun (x : (↑(Set.range f) : Type u_2)) ↦ f ⁻¹' {(↑x : Y)}) x)
        ((fun (x : (↑(Set.range f) : Type u_2)) ↦ f ⁻¹' {(↑x : Y)}) w) sorry)
      (Subtype.mk (p := fun (x : S) ↦
        x ∈
          (↑(Subtype.mk (p := fun (x : Set S) ↦
                Membership.mem (γ := Set (Set S)) (Set.range fun (x : (↑(Set.range f) : Type u_2)) ↦ f ⁻¹' {(↑x : Y)})
                  x)
                ((fun (x : (↑(Set.range f) : Type u_2)) ↦ f ⁻¹' {(↑x : Y)}) w) sorry) :
            Set S))
        val hx)) =
  Sigma.fst (β := fun (a : Fiber f) ↦ { x : S // x ∈ (↑a : Set S) })
    (Sigma.mk (β := fun (x : Fiber f) ↦ (↑(↑x : Set S) : Type u_1))
      (Subtype.mk (p := fun (x : Set S) ↦
        Membership.mem (γ := Set (Set S)) (Set.range fun (x : (↑(Set.range f) : Type u_2)) ↦ f ⁻¹' {(↑x : Y)}) x)
        ((fun (x : (↑(Set.range f) : Type u_2)) ↦ f ⁻¹' {(↑x : Y)}) w_1) sorry)
      (Subtype.mk (p := fun (x : S) ↦
        x ∈
          (↑(Subtype.mk (p := fun (x : Set S) ↦
                Membership.mem (γ := Set (Set S)) (Set.range fun (x : (↑(Set.range f) : Type u_2)) ↦ f ⁻¹' {(↑x : Y)})
                  x)
                ((fun (x : (↑(Set.range f) : Type u_2)) ↦ f ⁻¹' {(↑x : Y)}) w_1) sorry) :
            Set S))
        val_1 hy))
Tactic: refine Sigma.subtype_ext ?_ h