-- Lean 4 proof step from Mathlib.Order.LiminfLimsup (goal)
Goal:
α : Type u_1
ι : Type u_4
ι' : Type u_5
inst : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst_1 : Countable.{max 1 (u_5 + 1)} (Subtype p)
inst_2 : Nonempty.{max 1 (u_5 + 1)} (Subtype p)
hv : v.HasBasis p s
f : ι → α
hs : ∀ (j : Subtype p), (s (↑j : ι')).Nonempty
j0 : Subtype p
hj0 : BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j0 : ι')) : Type u_4)) ↦ f (↑i : ι))
m : Set (Subtype p) :=
  {j : Subtype p | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))}
this : ∀ (j : Subtype p), Nonempty.{u_4 + 1} (↑(s (↑j : ι')) : Type u_4)
A :
  Eq.{u_1 + 1} (α := Set α) (⋃ (j : Subtype p), ⋂ (i : (↑(s (↑j : ι')) : Type u_4)), Iic (f (↑i : ι)))
    (⋃ (j : Subtype p), ⋂ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), Iic (f (↑i : ι)))
j : Subtype p
Hj : j ∉ m
Z :
  ∃ (n : ℕ),
    Membership.mem (α := Subtype p) m (Exists.choose (p := Surjective) ⋯ n : Subtype p) ∨ ∀ (j : Subtype p), j ∉ m
neg :
  ∀
    (hZ :
      Membership.mem (α := Subtype p) m
        (Exists.choose (p := Surjective) ⋯
            (Nat.find (p := fun (n : ℕ) ↦
              Membership.mem (α := Subtype p) m (Exists.choose (p := Surjective) ⋯ n : Subtype p) ∨
                ∀ (j : Subtype p), j ∉ m)
              Z) :
          Subtype p)),
    Membership.mem (γ := Set (Subtype p))
      {j : Subtype p | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))}
      (⋯.choose (p := Surjective)
        (Nat.find (p := fun (n : ℕ) ↦
          Membership.mem (γ := Set (Subtype p))
              {j : Subtype p | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))}
              (⋯.choose (p := Surjective) n) ∨
            ∀ (j : Subtype p),
              j ∉ {j : Subtype p | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))})
          ⋯))
⊢ Membership.mem (γ := Set (Subtype p))
    {j : Subtype p | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))}
    (⋯.choose (p := Surjective)
      (Nat.find (p := fun (n : ℕ) ↦
        Membership.mem (γ := Set (Subtype p))
            {j : Subtype p | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))}
            (⋯.choose (p := Surjective) n) ∨
          ∀ (j : Subtype p),
            j ∉ {j : Subtype p | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))})
        ⋯))
have neg₁ : ∀ (hZ : ∀ (j : Subtype p), j ∉ m),
  Membership.mem (γ := Set (Subtype p))
    {j : Subtype p | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))}
    (sorry.choose (p := Surjective)
      (Nat.find (p := fun (n : ℕ) ↦
        Membership.mem (γ := Set (Subtype p))
            {j : Subtype p | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))}
            (sorry.choose (p := Surjective) n) ∨
          ∀ (j : Subtype p),
            j ∉ {j : Subtype p | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))})
        sorry))
Tactic: rcases Nat.find_spec Z with hZ | hZ