-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorffRealized (goal)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
I1 : ∀ (x y : X), IsClosed (X := Cb X Y) {f : Cb X Y | (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inl y) = dist x y}
I2 : ∀ (x y : Y), IsClosed (X := Cb X Y) {f : Cb X Y | (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inr x, inr y) = dist x y}
I3 :
  ∀ (x y : X ⊕ Y),
    IsClosed (X := Cb X Y)
      {f : Cb X Y |
        Eq (α := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, y) : ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (y, x) : ℝ)}
I4 :
  ∀ (x y z : X ⊕ Y),
    IsClosed (X := Cb X Y)
      {f : Cb X Y |
        (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, z) ≤
          HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, y) : ℝ)
            ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (y, z) : ℝ)}
I5 :
  ∀ (x : X ⊕ Y),
    IsClosed (X := Cb X Y) {f : Cb X Y | Eq (α := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, x) : ℝ) (0 : ℝ)}
I6 :
  ∀ (x y : X ⊕ Y), IsClosed (X := Cb X Y) {f : Cb X Y | (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, y) ≤ (↑(maxVar X Y) : ℝ)}
this :
  Eq (α := Set (Cb X Y)) (candidatesB X Y)
    ((((((⋂ (x : X), ⋂ (y : X), {f : Cb X Y | (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inl y) = dist x y}) ∩
              ⋂ (x : Y), ⋂ (y : Y), {f : Cb X Y | (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inr x, inr y) = dist x y}) ∩
            ⋂ (x : X ⊕ Y),
              ⋂ (y : X ⊕ Y),
                {f : Cb X Y |
                  Eq (α := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, y) : ℝ)
                    ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (y, x) : ℝ)}) ∩
          ⋂ (x : X ⊕ Y),
            ⋂ (y : X ⊕ Y),
              ⋂ (z : X ⊕ Y),
                {f : Cb X Y |
                  (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, z) ≤
                    HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, y) : ℝ)
                      ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (y, z) : ℝ)}) ∩
        ⋂ (x : X ⊕ Y), {f : Cb X Y | Eq (α := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, x) : ℝ) (0 : ℝ)}) ∩
      ⋂ (x : X ⊕ Y), ⋂ (y : X ⊕ Y), {f : Cb X Y | (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, y) ≤ (↑(maxVar X Y) : ℝ)})
apply :
  IsClosed (X := Cb X Y)
    (((⋂ (x : X), ⋂ (y : X), {f : Cb X Y | (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inl y) = dist x y}) ∩
        ⋂ (x : Y), ⋂ (y : Y), {f : Cb X Y | (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inr x, inr y) = dist x y}) ∩
      ⋂ (x : X ⊕ Y),
        ⋂ (y : X ⊕ Y),
          {f : Cb X Y |
            Eq (α := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, y) : ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (y, x) : ℝ)})
⊢ IsClosed (X := Cb X Y)
    ((((⋂ (x : X), ⋂ (y : X), {f : Cb X Y | (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inl y) = dist x y}) ∩
          ⋂ (x : Y), ⋂ (y : Y), {f : Cb X Y | (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inr x, inr y) = dist x y}) ∩
        ⋂ (x : X ⊕ Y),
          ⋂ (y : X ⊕ Y),
            {f : Cb X Y |
              Eq (α := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, y) : ℝ)
                ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (y, x) : ℝ)}) ∩
      ⋂ (x : X ⊕ Y),
        ⋂ (y : X ⊕ Y),
          ⋂ (z : X ⊕ Y),
            {f : Cb X Y |
              (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, z) ≤
                HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, y) : ℝ)
                  ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (y, z) : ℝ)})
have apply₁ : IsClosed (X := Cb X Y)
  (⋂ (x : X ⊕ Y),
    ⋂ (y : X ⊕ Y),
      ⋂ (z : X ⊕ Y),
        {f : Cb X Y |
          (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, z) ≤
            HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, y) : ℝ)
              ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (y, z) : ℝ)})
Tactic: first
      | apply IsClosed.inter _ _
      | apply isClosed_iInter _
      | apply I1 _ _ | apply I2 _ _ | apply I3 _ _ | apply I4 _ _ _ | apply I5 _ | apply I6 _ _
      | intro x