-- Module: Mathlib.Topology.Sets.Closeds
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : β → α
h : IsOpenEmbedding f
a b : IrreducibleCloseds β
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 ⋯ 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
⊢ 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

Tactic:
refine ⟨fun hle ↦ ?_, fun hle ↦ map_mono h.continuous hle⟩