-- Lean 4 proof step from Mathlib.Topology.Sets.Closeds (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : β → α
h : IsOpenEmbedding f
a b : IrreducibleCloseds β
⊢ LE.le.{u_2} (α := (↑{V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} : Type u_2))
      (({
              toFun := fun (T : IrreducibleCloseds β) ↦
                Subtype.mk (p := fun (x : IrreducibleCloseds α) ↦
                  Membership.mem (γ := Set (IrreducibleCloseds α))
                    {V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} x)
                  (map f ⋯ T) ⋯,
              invFun := fun (V : (↑{V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} : Type u_2)) ↦
                { carrier := f ⁻¹' (↑(↑V : IrreducibleCloseds α) : Set α), isIrreducible' := ⋯, isClosed' := ⋯ },
              left_inv := ⋯, right_inv := ⋯ } :
            (a : IrreducibleCloseds β) → (↑{V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} : Type u_2))
          a :
        (↑{V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} : Type u_2))
      (({
              toFun := fun (T : IrreducibleCloseds β) ↦
                Subtype.mk (p := fun (x : IrreducibleCloseds α) ↦
                  Membership.mem (γ := Set (IrreducibleCloseds α))
                    {V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} x)
                  (map f ⋯ T) ⋯,
              invFun := fun (V : (↑{V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} : Type u_2)) ↦
                { carrier := f ⁻¹' (↑(↑V : IrreducibleCloseds α) : Set α), isIrreducible' := ⋯, isClosed' := ⋯ },
              left_inv := ⋯, right_inv := ⋯ } :
            (a : IrreducibleCloseds β) → (↑{V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} : Type u_2))
          b :
        (↑{V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} : Type u_2)) ↔
    a ≤ b
have refine : ∀
  (hle :
    LE.le.{u_2} (α := (↑{V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} : Type u_2))
      (({
              toFun := fun (T : IrreducibleCloseds β) ↦
                Subtype.mk (p := fun (x : IrreducibleCloseds α) ↦
                  Membership.mem (γ := Set (IrreducibleCloseds α))
                    {V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} x)
                  (map f sorry T) sorry,
              invFun := fun (V : (↑{V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} : Type u_2)) ↦
                { carrier := f ⁻¹' (↑(↑V : IrreducibleCloseds α) : Set α), isIrreducible' := sorry, isClosed' := sorry },
              left_inv := sorry, right_inv := sorry } :
            (a : IrreducibleCloseds β) → (↑{V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} : Type u_2))
          a :
        (↑{V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} : Type u_2))
      (({
              toFun := fun (T : IrreducibleCloseds β) ↦
                Subtype.mk (p := fun (x : IrreducibleCloseds α) ↦
                  Membership.mem (γ := Set (IrreducibleCloseds α))
                    {V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} x)
                  (map f sorry T) sorry,
              invFun := fun (V : (↑{V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} : Type u_2)) ↦
                { carrier := f ⁻¹' (↑(↑V : IrreducibleCloseds α) : Set α), isIrreducible' := sorry, isClosed' := sorry },
              left_inv := sorry, right_inv := sorry } :
            (a : IrreducibleCloseds β) → (↑{V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} : Type u_2))
          b :
        (↑{V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} : Type u_2))),
  a ≤ b
Tactic: refine ⟨fun hle ↦ ?_, fun hle ↦ map_mono h.continuous hle⟩