-- 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 : val = val_1
⊢ 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) ⋯)
        (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)) =
    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) ⋯)
        (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))
have rw : ∀ (hx_1 : f val = (↑w : Y)) (w_2 : (↑(Set.range f) : Type u_2)) (val_2 : S)
  (hy :
    val_2 ∈
      (↑(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_2) sorry) :
        Set S))
  (hy_1 : f val_2 = (↑w_2 : Y)) (h : val = val_2),
  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_2) 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_2) sorry) :
              Set S))
          val_2 hy))
Tactic: rw [Set.mem_preimage, Set.mem_singleton_iff] at hx hy
Cleared hypotheses: w_1, val_1, hy, h