-- Module: Mathlib.Topology.FiberPartition
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
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) ⋯) :
          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) ⋯)
          (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_2) ⋯)
          (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) ⋯) :
                Set S))
            val_2 hy))
⊢ 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))

Tactic:
rw [Set.mem_preimage, Set.mem_singleton_iff] at hx hy

Premises used: Set.mem_singleton_iff, Set.mem_preimage