awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
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) : ℝ)})
x_1 x : Y
⊢ IsClosed (X := Cb X Y) {f : Cb X Y | (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inr x_1, inr x) = dist x_1 x}

Tactic:
apply I2 _ _
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
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) : ℝ)})
x_1 x : Y
⊢ IsClosed (X := Cb X Y) {f : Cb X Y | (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inr x_1, inr x) = dist x_1 x}

Tactic:
first
      | apply IsClosed.inter _ _
      | apply isClosed_iInter _
      | apply I1 _ _ | apply I2 _ _ | apply I3 _ _ | apply I4 _ _ _ | apply I5 _ | apply I6 _ _
      | intro x

Premises used: IsClosed.inter, isClosed_iInter
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
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 :
  ∀ (i : X ⊕ Y),
    IsClosed (X := Cb X Y)
      (⋂ (y : X ⊕ Y),
        {f : Cb X Y |
          Eq (α := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (i, y) : ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (y, i) : ℝ)})
⊢ IsClosed (X := Cb 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) : ℝ)})

Tactic:
apply isClosed_iInter _

Premises used: isClosed_iInter
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
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 :
  ∀ (i : X ⊕ Y),
    IsClosed (X := Cb X Y)
      (⋂ (y : X ⊕ Y),
        {f : Cb X Y |
          Eq (α := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (i, y) : ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (y, i) : ℝ)})
⊢ IsClosed (X := Cb 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) : ℝ)})

Tactic:
first
      | apply IsClosed.inter _ _
      | apply isClosed_iInter _
      | apply I1 _ _ | apply I2 _ _ | apply I3 _ _ | apply I4 _ _ _ | apply I5 _ | apply I6 _ _
      | intro x

Premises used: IsClosed.inter, isClosed_iInter
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
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 :
  ∀ (x : X ⊕ Y),
    IsClosed (X := Cb 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) : ℝ)})
⊢ ∀ (i : X ⊕ Y),
    IsClosed (X := Cb X Y)
      (⋂ (y : X ⊕ Y),
        {f : Cb X Y |
          Eq (α := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (i, y) : ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (y, i) : ℝ)})

Tactic:
first
      | apply IsClosed.inter _ _
      | apply isClosed_iInter _
      | apply I1 _ _ | apply I2 _ _ | apply I3 _ _ | apply I4 _ _ _ | apply I5 _ | apply I6 _ _
      | intro x

Premises used: IsClosed.inter, isClosed_iInter
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
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) : ℝ)})
x : X ⊕ Y
apply :
  ∀ (i : X ⊕ Y),
    IsClosed (X := Cb X Y)
      {f : Cb X Y |
        Eq (α := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, i) : ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (i, x) : ℝ)}
⊢ IsClosed (X := Cb 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) : ℝ)})

Tactic:
apply isClosed_iInter _

Premises used: isClosed_iInter
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
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) : ℝ)})
x : X ⊕ Y
apply :
  ∀ (i : X ⊕ Y),
    IsClosed (X := Cb X Y)
      {f : Cb X Y |
        Eq (α := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, i) : ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (i, x) : ℝ)}
⊢ IsClosed (X := Cb 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) : ℝ)})

Tactic:
first
      | apply IsClosed.inter _ _
      | apply isClosed_iInter _
      | apply I1 _ _ | apply I2 _ _ | apply I3 _ _ | apply I4 _ _ _ | apply I5 _ | apply I6 _ _
      | intro x

Premises used: IsClosed.inter, isClosed_iInter
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
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) : ℝ)})
x : X ⊕ Y
apply :
  ∀ (x_1 : X ⊕ Y),
    IsClosed (X := Cb X Y)
      {f : Cb X Y |
        Eq (α := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, x_1) : ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x_1, x) : ℝ)}
⊢ ∀ (i : X ⊕ Y),
    IsClosed (X := Cb X Y)
      {f : Cb X Y |
        Eq (α := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, i) : ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (i, x) : ℝ)}

Tactic:
first
      | apply IsClosed.inter _ _
      | apply isClosed_iInter _
      | apply I1 _ _ | apply I2 _ _ | apply I3 _ _ | apply I4 _ _ _ | apply I5 _ | apply I6 _ _
      | intro x

Premises used: IsClosed.inter, isClosed_iInter
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
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) : ℝ)})
x_1 x : X ⊕ Y
⊢ IsClosed (X := Cb X Y)
    {f : Cb X Y |
      Eq (α := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x_1, x) : ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, x_1) : ℝ)}

Tactic:
apply I3 _ _