awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) : ℝ)})
x_1 x : X ⊕ Y
⊢ IsClosed (X := Cb X Y)
    (⋂ (z : X ⊕ Y),
      {f : Cb X Y |
        (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x_1, z) ≤
          HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x_1, x) : ℝ)
            ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, z) : ℝ)})
have apply : ∀ (i : X ⊕ Y),
  IsClosed (X := Cb X Y)
    {f : Cb X Y |
      (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x_1, i) ≤
        HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x_1, x) : ℝ)
          ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, i) : ℝ)}
Tactic: first
      | apply IsClosed.inter _ _
      | apply isClosed_iInter _
      | apply I1 _ _ | apply I2 _ _ | apply I3 _ _ | apply I4 _ _ _ | apply I5 _ | apply I6 _ _
      | intro x
-- 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) : ℝ)})
⊢ IsClosed (X := Cb X Y)
    (⋂ (x : X ⊕ Y), ⋂ (y : X ⊕ Y), {f : Cb X Y | (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, y) ≤ (↑(maxVar X Y) : ℝ)})
have apply : ∀ (i : X ⊕ Y),
  IsClosed (X := Cb X Y) (⋂ (y : X ⊕ Y), {f : Cb X Y | (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (i, y) ≤ (↑(maxVar X Y) : ℝ)})
Tactic: apply isClosed_iInter _
-- 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) : ℝ)})
⊢ IsClosed (X := Cb X Y)
    (⋂ (x : X ⊕ Y), ⋂ (y : X ⊕ Y), {f : Cb X Y | (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, y) ≤ (↑(maxVar X Y) : ℝ)})
have apply : ∀ (i : X ⊕ Y),
  IsClosed (X := Cb X Y) (⋂ (y : X ⊕ Y), {f : Cb X Y | (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (i, y) ≤ (↑(maxVar X Y) : ℝ)})
Tactic: first
      | apply IsClosed.inter _ _
      | apply isClosed_iInter _
      | apply I1 _ _ | apply I2 _ _ | apply I3 _ _ | apply I4 _ _ _ | apply I5 _ | apply I6 _ _
      | intro x
-- 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) : ℝ)})
x : X ⊕ Y
⊢ IsClosed (X := Cb X Y) (⋂ (y : X ⊕ Y), {f : Cb X Y | (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, y) ≤ (↑(maxVar X Y) : ℝ)})
have apply : ∀ (i : X ⊕ Y), IsClosed (X := Cb X Y) {f : Cb X Y | (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, i) ≤ (↑(maxVar X Y) : ℝ)}
Tactic: apply isClosed_iInter _
-- 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) : ℝ)})
x : X ⊕ Y
⊢ IsClosed (X := Cb X Y) (⋂ (y : X ⊕ Y), {f : Cb X Y | (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, y) ≤ (↑(maxVar X Y) : ℝ)})
have apply : ∀ (i : X ⊕ Y), IsClosed (X := Cb X Y) {f : Cb X Y | (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, i) ≤ (↑(maxVar X Y) : ℝ)}
Tactic: first
      | apply IsClosed.inter _ _
      | apply isClosed_iInter _
      | apply I1 _ _ | apply I2 _ _ | apply I3 _ _ | apply I4 _ _ _ | apply I5 _ | apply I6 _ _
      | intro x
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorffRealized (goal)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
f : Cb X Y
C : ℝ
x : X
cf : ℝ
hcf : Membership.mem (γ := Set ℝ) (lowerBounds (range (ι := (X ⊕ Y) × (X ⊕ Y)) (⇑f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ))) cf
x_1 : Y
⊢ cf + C ≤ HAdd.hAdd (α := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr x_1) : ℝ) C
have grw : HAdd.hAdd (α := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr x_1) : ℝ) C ≤
  HAdd.hAdd (α := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr x_1) : ℝ) C
Tactic: grw [hcf (mem_range_self _)]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorffRealized (goal)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
f : Cb X Y
C : ℝ
x : X
cf : ℝ
hcf : Membership.mem (γ := Set ℝ) (lowerBounds (range (ι := (X ⊕ Y) × (X ⊕ Y)) (⇑f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ))) cf
x_1 : Y
grw :
  HAdd.hAdd (α := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr x_1) : ℝ) C ≤
    HAdd.hAdd (α := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr x_1) : ℝ) C
⊢ cf + C ≤ HAdd.hAdd (α := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr x_1) : ℝ) C
have grw₁ : (X ⊕ Y) × (X ⊕ Y)
Tactic: grw [hcf (mem_range_self _)]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorffRealized (goal)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty Y
f : Cb X Y
C : ℝ
⊢ BddAbove (α := ℝ)
    (range fun (x : X) ↦ ⨅ (y : Y), HAdd.hAdd (α := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ) C)
have obtain : ∀ (Cf : ℝ)
  (hCf :
    Membership.mem (γ := Set ℝ) (upperBounds (range (ι := (X ⊕ Y) × (X ⊕ Y)) (⇑f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ))) Cf),
  BddAbove (α := ℝ)
    (range fun (x : X) ↦ ⨅ (y : Y), HAdd.hAdd (α := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ) C)
Tactic: obtain ⟨Cf, hCf⟩ := f.isBounded_range.bddAbove
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorffRealized (goal)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty Y
f : Cb X Y
C Cf : ℝ
hCf : Membership.mem (γ := Set ℝ) (upperBounds (range (ι := (X ⊕ Y) × (X ⊕ Y)) (⇑f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ))) Cf
⊢ BddAbove (α := ℝ)
    (range fun (x : X) ↦ ⨅ (y : Y), HAdd.hAdd (α := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ) C)
have refine : ∀ (x : X), ⨅ (y : Y), HAdd.hAdd (α := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ) C ≤ Cf + C
Tactic: refine ⟨Cf + C, forall_mem_range.2 fun x => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorffRealized (goal)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
f : Cb X Y
C : ℝ
y : Y
cf : ℝ
hcf : Membership.mem (γ := Set ℝ) (lowerBounds (range (ι := (X ⊕ Y) × (X ⊕ Y)) (⇑f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ))) cf
x : X
⊢ cf + C ≤ HAdd.hAdd (α := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ) C
have grw : HAdd.hAdd (α := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ) C ≤
  HAdd.hAdd (α := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ) C
Tactic: grw [hcf (mem_range_self _)]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorffRealized (goal)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
f : Cb X Y
C : ℝ
y : Y
cf : ℝ
hcf : Membership.mem (γ := Set ℝ) (lowerBounds (range (ι := (X ⊕ Y) × (X ⊕ Y)) (⇑f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ))) cf
x : X
grw :
  HAdd.hAdd (α := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ) C ≤
    HAdd.hAdd (α := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ) C
⊢ cf + C ≤ HAdd.hAdd (α := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ) C
have grw₁ : (X ⊕ Y) × (X ⊕ Y)
Tactic: grw [hcf (mem_range_self _)]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorffRealized (goal)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty X
f : Cb X Y
C : ℝ
⊢ BddAbove (α := ℝ)
    (range fun (y : Y) ↦ ⨅ (x : X), HAdd.hAdd (α := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ) C)
have obtain : ∀ (Cf : ℝ)
  (hCf :
    Membership.mem (γ := Set ℝ) (upperBounds (range (ι := (X ⊕ Y) × (X ⊕ Y)) (⇑f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ))) Cf),
  BddAbove (α := ℝ)
    (range fun (y : Y) ↦ ⨅ (x : X), HAdd.hAdd (α := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ) C)
Tactic: obtain ⟨Cf, hCf⟩ := f.isBounded_range.bddAbove
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorffRealized (goal)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty X
f : Cb X Y
C Cf : ℝ
hCf : Membership.mem (γ := Set ℝ) (upperBounds (range (ι := (X ⊕ Y) × (X ⊕ Y)) (⇑f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ))) Cf
⊢ BddAbove (α := ℝ)
    (range fun (y : Y) ↦ ⨅ (x : X), HAdd.hAdd (α := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ) C)
have refine : ∀ (y : Y), ⨅ (x : X), HAdd.hAdd (α := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ) C ≤ Cf + C
Tactic: refine ⟨Cf + C, forall_mem_range.2 fun y => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorffRealized (goal)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty X
inst_3 : Nonempty Y
f g : Cb X Y
⊢ ⨆ (x : X), ⨅ (y : Y), (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) ≤
    (⨆ (x : X), ⨅ (y : Y), (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y)) + dist f g
have obtain : ∀ (cg : ℝ)
  (hcg :
    Membership.mem (γ := Set ℝ) (lowerBounds (range (ι := (X ⊕ Y) × (X ⊕ Y)) (⇑g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ))) cg),
  ⨆ (x : X), ⨅ (y : Y), (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) ≤
    (⨆ (x : X), ⨅ (y : Y), (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y)) + dist f g
Tactic: obtain ⟨cg, hcg⟩ := g.isBounded_range.bddBelow
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorffRealized (hypothesis)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty X
inst_3 : Nonempty Y
f g : Cb X Y
cg : ℝ
hcg : Membership.mem (γ := Set ℝ) (lowerBounds (range (ι := (X ⊕ Y) × (X ⊕ Y)) (⇑g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ))) cg
⊢ ⨆ (x : X), ⨅ (y : Y), (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) ≤
    (⨆ (x : X), ⨅ (y : Y), (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y)) + dist f g
have Hcg : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cg ≤ (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) x
Tactic: have Hcg : ∀ x, cg ≤ g x := fun x => hcg (mem_range_self x)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorffRealized (goal)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty X
inst_3 : Nonempty Y
f g : Cb X Y
cg : ℝ
hcg : Membership.mem (γ := Set ℝ) (lowerBounds (range (ι := (X ⊕ Y) × (X ⊕ Y)) (⇑g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ))) cg
Hcg : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cg ≤ (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) x
⊢ ⨆ (x : X), ⨅ (y : Y), (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) ≤
    (⨆ (x : X), ⨅ (y : Y), (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y)) + dist f g
have obtain : ∀ (cf : ℝ)
  (hcf :
    Membership.mem (γ := Set ℝ) (lowerBounds (range (ι := (X ⊕ Y) × (X ⊕ Y)) (⇑f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ))) cf),
  ⨆ (x : X), ⨅ (y : Y), (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) ≤
    (⨆ (x : X), ⨅ (y : Y), (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y)) + dist f g
Tactic: obtain ⟨cf, hcf⟩ := f.isBounded_range.bddBelow
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorffRealized (hypothesis)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty X
inst_3 : Nonempty Y
f g : Cb X Y
cg : ℝ
hcg : Membership.mem (γ := Set ℝ) (lowerBounds (range (ι := (X ⊕ Y) × (X ⊕ Y)) (⇑g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ))) cg
Hcg : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cg ≤ (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) x
cf : ℝ
hcf : Membership.mem (γ := Set ℝ) (lowerBounds (range (ι := (X ⊕ Y) × (X ⊕ Y)) (⇑f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ))) cf
⊢ ⨆ (x : X), ⨅ (y : Y), (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) ≤
    (⨆ (x : X), ⨅ (y : Y), (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y)) + dist f g
have Hcf : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cf ≤ (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) x
Tactic: have Hcf : ∀ x, cf ≤ f x := fun x => hcf (mem_range_self x)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorffRealized (hypothesis)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty X
inst_3 : Nonempty Y
f g : Cb X Y
cg : ℝ
hcg : Membership.mem (γ := Set ℝ) (lowerBounds (range (ι := (X ⊕ Y) × (X ⊕ Y)) (⇑g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ))) cg
Hcg : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cg ≤ (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) x
cf : ℝ
hcf : Membership.mem (γ := Set ℝ) (lowerBounds (range (ι := (X ⊕ Y) × (X ⊕ Y)) (⇑f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ))) cf
Hcf : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cf ≤ (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) x
⊢ ⨆ (x : X), ⨅ (y : Y), (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) ≤
    (⨆ (x : X), ⨅ (y : Y), (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y)) + dist f g
have Z : LE.le (α := ℝ) (⨆ (x : X), ⨅ (y : Y), (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y))
  (⨆ (x : X), ⨅ (y : Y), HAdd.hAdd (α := ℝ) ((g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ) (dist f g))
Tactic: have Z : (⨆ x, ⨅ y, f (inl x, inr y)) ≤ ⨆ x, ⨅ y, g (inl x, inr y) + dist f g :=
    ciSup_mono (HD_bound_aux1 _ (dist f g)) fun x =>
      ciInf_mono ⟨cf, forall_mem_range.2 fun i => Hcf _⟩ fun y => coe_le_coe_add_dist
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorffRealized (goal)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty X
inst_3 : Nonempty Y
f g : Cb X Y
cg : ℝ
hcg : Membership.mem (γ := Set ℝ) (lowerBounds (range (ι := (X ⊕ Y) × (X ⊕ Y)) (⇑g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ))) cg
Hcg : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cg ≤ (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) x
cf : ℝ
hcf : Membership.mem (γ := Set ℝ) (lowerBounds (range (ι := (X ⊕ Y) × (X ⊕ Y)) (⇑f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ))) cf
Hcf : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cf ≤ (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) x
Z :
  LE.le (α := ℝ) (⨆ (x : X), ⨅ (y : Y), (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y))
    (⨆ (x : X), ⨅ (y : Y), HAdd.hAdd (α := ℝ) ((g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ) (dist f g))
x : X
⊢ (⨅ (y : Y), (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y)) + dist f g =
    ⨅ (y : Y), HAdd.hAdd (α := ℝ) ((g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ) (dist f g)
have refine_1 : Monotone (HAdd.hAdd (α := ℝ → ℝ) id fun (x : ℝ) ↦ dist f g)
Tactic: refine Monotone.map_ciInf_of_continuousAt (continuousAt_id.add continuousAt_const) ?_ ?_