-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Sphere (goal)
Goal:
n : ℕ
t : Set (ULift.{u_1, 0} (↑(Metric.closedBall 0 1) : Type))
h_1 : IsOpen t
s : Set (↑(Metric.closedBall 0 1) : Type)
r : Set (EuclideanSpace ℝ (Fin n))
hro : IsOpen r
hrs :
  Subtype.val (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
        Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.closedBall 0 1) x) ⁻¹'
      r =
    s
hst : ULift.down ⁻¹' s = t
h :
  IsOpen (X := (↑(Metric.ball 0 1) : Type))
      (Subtype.val (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
          Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.ball 0 1) x) ⁻¹'
        r) ∧
    Eq.{u_1 + 1} (α := Set (ULift.{u_1, 0} (↑(Metric.ball 0 1) : Type)))
      (ULift.down ⁻¹'
        Subtype.val (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
            Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.ball 0 1) x) ⁻¹'
          r)
      (Set.preimage (β := ULift.{u_1, 0} (↑(Metric.closedBall 0 1) : Type))
        (fun (x : ULift.{u_1, 0} (↑(Metric.ball 0 1) : Type)) ↦
          match (motive :=
            ULift.{u_1, 0} (↑(Metric.ball 0 1) : Type) → ULift.{u_1, 0} (↑(Metric.closedBall 0 1) : Type)) x with
          | { down := ⟨p, hp⟩ } =>
            {
              down :=
                Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
                  Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.closedBall 0 1) x) p ⋯ })
        (ULift.down ⁻¹'
          Subtype.val (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
              Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.closedBall 0 1) x) ⁻¹'
            r))
w : Set (↑(Metric.ball 0 1) : Type)
h₁ :
  IsOpen (X := (↑(Metric.ball 0 1) : Type))
      (Subtype.val (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
          Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.ball 0 1) x) ⁻¹'
        r) ∧
    Eq.{u_1 + 1} (α := Set (ULift.{u_1, 0} (↑(Metric.ball 0 1) : Type)))
      (ULift.down ⁻¹'
        Subtype.val (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
            Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.ball 0 1) x) ⁻¹'
          r)
      (Set.preimage (β := ULift.{u_1, 0} (↑(Metric.closedBall 0 1) : Type))
        (fun (x : ULift.{u_1, 0} (↑(Metric.ball 0 1) : Type)) ↦
          match (motive :=
            ULift.{u_1, 0} (↑(Metric.ball 0 1) : Type) → ULift.{u_1, 0} (↑(Metric.closedBall 0 1) : Type)) x with
          | { down := ⟨p, hp⟩ } =>
            {
              down :=
                Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
                  Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.closedBall 0 1) x) p ⋯ })
        (ULift.down ⁻¹'
          Subtype.val (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
              Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.closedBall 0 1) x) ⁻¹'
            r))
w₁ : Set (↑(Metric.ball 0 1) : Type)
h₂ :
  IsOpen (X := (↑(Metric.ball 0 1) : Type))
    (Subtype.val (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
        Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.ball 0 1) x) ⁻¹'
      r)
⊢ ∃ (t : Set (↑(Metric.ball 0 1) : Type)),
    IsOpen t ∧
      ULift.down ⁻¹' t =
        Set.preimage (β := ULift.{u_1, 0} (↑(Metric.closedBall 0 1) : Type))
          (fun (x : ULift.{u_1, 0} (↑(Metric.ball 0 1) : Type)) ↦
            match (motive :=
              ULift.{u_1, 0} (↑(Metric.ball 0 1) : Type) → ULift.{u_1, 0} (↑(Metric.closedBall 0 1) : Type)) x with
            | { down := ⟨p, hp⟩ } =>
              {
                down :=
                  Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
                    Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.closedBall 0 1) x) p ⋯ })
          (ULift.down ⁻¹'
            Subtype.val (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
                Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.closedBall 0 1) x) ⁻¹'
              r)
have h₃ : Eq.{u_1 + 1} (α := Set (ULift.{u_1, 0} (↑(Metric.ball 0 1) : Type)))
  (ULift.down ⁻¹'
    Subtype.val (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
        Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.ball 0 1) x) ⁻¹'
      r)
  (Set.preimage (β := ULift.{u_1, 0} (↑(Metric.closedBall 0 1) : Type))
    (fun (x : ULift.{u_1, 0} (↑(Metric.ball 0 1) : Type)) ↦
      match (motive := ULift.{u_1, 0} (↑(Metric.ball 0 1) : Type) → ULift.{u_1, 0} (↑(Metric.closedBall 0 1) : Type))
        x with
      | { down := ⟨p, hp⟩ } =>
        {
          down :=
            Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
              Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.closedBall 0 1) x) p sorry })
    (ULift.down ⁻¹'
      Subtype.val (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
          Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.closedBall 0 1) x) ⁻¹'
        r))
Tactic: tauto