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
inst_2 : Nonempty X
inst_3 : Nonempty Y
f g : Cb X Y
obtain :
  ∀ (cg : ℝ)
    (hcg :
      Membership.mem (γ := Set ℝ) (lowerBounds (range (ι := (X ⊕ Y) × (X ⊕ Y)) (⇑g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ))) cg),
    ⨆ (y : Y), ⨅ (x : X), (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) ≤
      (⨆ (y : Y), ⨅ (x : X), (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y)) + dist f g
⊢ ⨆ (y : Y), ⨅ (x : X), (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) ≤
    (⨆ (y : Y), ⨅ (x : X), (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y)) + dist f g

Tactic:
obtain ⟨cg, hcg⟩ := g.isBounded_range.bddBelow

Premises used: Bornology.IsBounded.bddBelow, BoundedContinuousFunction.isBounded_range
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
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
obtain :
  ∀ (cf : ℝ)
    (hcf :
      Membership.mem (γ := Set ℝ) (lowerBounds (range (ι := (X ⊕ Y) × (X ⊕ Y)) (⇑f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ))) cf),
    ⨆ (y : Y), ⨅ (x : X), (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) ≤
      (⨆ (y : Y), ⨅ (x : X), (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y)) + dist f g
⊢ ⨆ (y : Y), ⨅ (x : X), (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) ≤
    (⨆ (y : Y), ⨅ (x : X), (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y)) + dist f g

Tactic:
obtain ⟨cf, hcf⟩ := f.isBounded_range.bddBelow

Premises used: Bornology.IsBounded.bddBelow, BoundedContinuousFunction.isBounded_range
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
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
⊢ LE.le (α := ℝ) (⨆ (y : Y), ⨅ (x : X), (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y))
    (⨆ (y : Y), ⨅ (x : X), HAdd.hAdd (α := ℝ) ((g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ) (dist f g))

Tactic:
have Z : (⨆ y, ⨅ x, f (inl x, inr y)) ≤ ⨆ y, ⨅ x, g (inl x, inr y) + dist f g :=
    ciSup_mono (HD_bound_aux2 _ (dist f g)) fun y =>
      ciInf_mono ⟨cf, forall_mem_range.2 fun i => Hcf _⟩ fun y => coe_le_coe_add_dist
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
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 (α := ℝ) (⨆ (y : Y), ⨅ (x : X), (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y))
    (⨆ (y : Y), ⨅ (x : X), HAdd.hAdd (α := ℝ) ((g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ) (dist f g))
y : Y
⊢ (⨅ (x : X), (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y)) + dist f g =
    ⨅ (x : X), HAdd.hAdd (α := ℝ) ((g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ) (dist f g)

Tactic:
Monotone.map_ciInf_of_continuousAt (continuousAt_id.add continuousAt_const) ?_ ?_

Premises used: iInf, ContinuousAt.add, continuousAt_const, continuousAt_id, Monotone.map_ciInf_of_continuousAt
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
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 (α := ℝ) (⨆ (y : Y), ⨅ (x : X), (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y))
    (⨆ (y : Y), ⨅ (x : X), HAdd.hAdd (α := ℝ) ((g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ) (dist f g))
y : Y
refine_1 : Monotone (HAdd.hAdd (α := ℝ → ℝ) id fun (x : ℝ) ↦ dist f g)
refine_2 : BddBelow (α := ℝ) (range fun (x : X) ↦ (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y))
⊢ (⨅ (x : X), (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y)) + dist f g =
    ⨅ (x : X), HAdd.hAdd (α := ℝ) ((g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ) (dist f g)

Tactic:
refine Monotone.map_ciInf_of_continuousAt (continuousAt_id.add continuousAt_const) ?_ ?_

Premises used: ContinuousAt.add, continuousAt_const, continuousAt_id, Monotone.map_ciInf_of_continuousAt
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
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 (α := ℝ) (⨆ (y : Y), ⨅ (x : X), (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y))
    (⨆ (y : Y), ⨅ (x : X), HAdd.hAdd (α := ℝ) ((g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ) (dist f g))
y_1 : Y
x y : ℝ
hx : x ≤ y
⊢ HAdd.hAdd (α := ℝ → ℝ) (β := ℝ → ℝ) id (fun (x : ℝ) ↦ dist f g) x ≤
    HAdd.hAdd (α := ℝ → ℝ) (β := ℝ → ℝ) id (fun (x : ℝ) ↦ dist f g) y

Tactic:
simpa
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
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 (α := ℝ) (⨆ (y : Y), ⨅ (x : X), (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y))
    (⨆ (y : Y), ⨅ (x : X), HAdd.hAdd (α := ℝ) ((g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ) (dist f g))
y : Y
⊢ BddBelow (α := ℝ) (range fun (x : X) ↦ (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y))

Tactic:
⟨cg, forall_mem_range.2 fun i => Hcg _⟩

Premises used: Iff.mpr, Set.forall_mem_range, Prod.mk, Sum.inl, Set.Nonempty, Sum.inr, BddBelow, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
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 (α := ℝ) (⨆ (y : Y), ⨅ (x : X), (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y))
    (⨆ (y : Y), ⨅ (x : X), HAdd.hAdd (α := ℝ) ((g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ) (dist f g))
y : Y
⊢ BddBelow (α := ℝ) (range fun (x : X) ↦ (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y))

Tactic:
exact ⟨cg, forall_mem_range.2 fun i => Hcg _⟩
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
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 (α := ℝ) (⨆ (y : Y), ⨅ (x : X), (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y))
    (⨆ (y : Y), ⨅ (x : X), HAdd.hAdd (α := ℝ) ((g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ) (dist f g))
⊢ ∀ (y : Y),
    (⨅ (x : X), (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y)) + dist f g =
      ⨅ (x : X), HAdd.hAdd (α := ℝ) ((g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ) (dist f g)

Tactic:
have E1 : ∀ y, (⨅ x, g (inl x, inr y)) + dist f g = ⨅ x, g (inl x, inr y) + dist f g := by
    intro y
    refine Monotone.map_ciInf_of_continuousAt (continuousAt_id.add continuousAt_const) ?_ ?_
    · intro x y hx
      simpa
    · change BddBelow (range fun x : X => g (inl x, inr y))
      exact ⟨cg, forall_mem_range.2 fun i => Hcg _⟩
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
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 (α := ℝ) (⨆ (y : Y), ⨅ (x : X), (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y))
    (⨆ (y : Y), ⨅ (x : X), HAdd.hAdd (α := ℝ) ((g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ) (dist f g))
E1 :
  ∀ (y : Y),
    (⨅ (x : X), (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y)) + dist f g =
      ⨅ (x : X), HAdd.hAdd (α := ℝ) ((g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ) (dist f g)
⊢ (⨆ (y : Y), ⨅ (x : X), (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y)) + dist f g =
    ⨆ (y : Y), (⨅ (x : X), (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y)) + dist f g

Tactic:
Monotone.map_ciSup_of_continuousAt (continuousAt_id.add continuousAt_const) ?_ ?_

Premises used: iInf, ContinuousAt.add, iSup, Monotone.map_ciSup_of_continuousAt, continuousAt_const, continuousAt_id
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
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 (α := ℝ) (⨆ (y : Y), ⨅ (x : X), (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y))
    (⨆ (y : Y), ⨅ (x : X), HAdd.hAdd (α := ℝ) ((g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ) (dist f g))
E1 :
  ∀ (y : Y),
    (⨅ (x : X), (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y)) + dist f g =
      ⨅ (x : X), HAdd.hAdd (α := ℝ) ((g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ) (dist f g)
refine_1 : Monotone (HAdd.hAdd (α := ℝ → ℝ) id fun (x : ℝ) ↦ dist f g)
refine_2 : BddAbove (α := ℝ) (range fun (y : Y) ↦ ⨅ (x : X), (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y))
⊢ (⨆ (y : Y), ⨅ (x : X), (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y)) + dist f g =
    ⨆ (y : Y), (⨅ (x : X), (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y)) + dist f g

Tactic:
refine Monotone.map_ciSup_of_continuousAt (continuousAt_id.add continuousAt_const) ?_ ?_

Premises used: ContinuousAt.add, Monotone.map_ciSup_of_continuousAt, continuousAt_const, continuousAt_id
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
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 (α := ℝ) (⨆ (y : Y), ⨅ (x : X), (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y))
    (⨆ (y : Y), ⨅ (x : X), HAdd.hAdd (α := ℝ) ((g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ) (dist f g))
E1 :
  ∀ (y : Y),
    (⨅ (x : X), (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y)) + dist f g =
      ⨅ (x : X), HAdd.hAdd (α := ℝ) ((g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ) (dist f g)
x y : ℝ
hx : x ≤ y
⊢ HAdd.hAdd (α := ℝ → ℝ) (β := ℝ → ℝ) id (fun (x : ℝ) ↦ dist f g) x ≤
    HAdd.hAdd (α := ℝ → ℝ) (β := ℝ → ℝ) id (fun (x : ℝ) ↦ dist f g) y

Tactic:
simpa
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
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 (α := ℝ) (⨆ (y : Y), ⨅ (x : X), (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y))
    (⨆ (y : Y), ⨅ (x : X), HAdd.hAdd (α := ℝ) ((g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ) (dist f g))
E1 :
  ∀ (y : Y),
    (⨅ (x : X), (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y)) + dist f g =
      ⨅ (x : X), HAdd.hAdd (α := ℝ) ((g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ) (dist f g)
⊢ BddAbove (α := ℝ) (range fun (y : Y) ↦ ⨅ (x : X), (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y))

Tactic:
simpa using HD_bound_aux2 _ 0

Premises used: _private.0.GromovHausdorff.HD_bound_aux2, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
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 (α := ℝ) (⨆ (y : Y), ⨅ (x : X), (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y))
    (⨆ (y : Y), ⨅ (x : X), HAdd.hAdd (α := ℝ) ((g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ) (dist f g))
E1 :
  ∀ (y : Y),
    (⨅ (x : X), (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y)) + dist f g =
      ⨅ (x : X), HAdd.hAdd (α := ℝ) ((g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ) (dist f g)
⊢ (⨆ (y : Y), ⨅ (x : X), (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y)) + dist f g =
    ⨆ (y : Y), (⨅ (x : X), (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y)) + dist f g

Tactic:
have E2 : (⨆ y, ⨅ x, g (inl x, inr y)) + dist f g = ⨆ y, (⨅ x, g (inl x, inr y)) + dist f g := by
    refine Monotone.map_ciSup_of_continuousAt (continuousAt_id.add continuousAt_const) ?_ ?_
    · intro x y hx
      simpa
    · simpa using HD_bound_aux2 _ 0
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
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 (α := ℝ) (⨆ (y : Y), ⨅ (x : X), (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y))
    (⨆ (y : Y), ⨅ (x : X), HAdd.hAdd (α := ℝ) ((g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ) (dist f g))
E1 :
  ∀ (y : Y),
    (⨅ (x : X), (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y)) + dist f g =
      ⨅ (x : X), HAdd.hAdd (α := ℝ) ((g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ) (dist f g)
E2 :
  (⨆ (y : Y), ⨅ (x : X), (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y)) + dist f g =
    ⨆ (y : Y), (⨅ (x : X), (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y)) + dist f g
⊢ ⨆ (y : Y), ⨅ (x : X), (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) ≤
    (⨆ (y : Y), ⨅ (x : X), (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y)) + dist f g

Tactic:
simpa [E2, E1]
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
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
grw : (⨆ (x : X), ⨅ (y : Y), (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y)) + dist f g ≤ HD g + dist f g
grw₁ :
  (⨆ (x : X), ⨅ (y : Y), (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y)) + dist f g ≤
    max (⨆ (x : X), ⨅ (y : Y), (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y))
        (⨆ (y : Y), ⨅ (x : X), (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y)) +
      dist f g
grw₂ grw₃ :
  (⨆ (x : X), ⨅ (y : Y), (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
⊢ ⨆ (x : X), ⨅ (y : Y), (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) ≤ HD g + dist f g

Tactic:
grw [HD_lipschitz_aux1 f g, HD, ← le_max_left]

Premises used: _private.0.GromovHausdorff.HD_lipschitz_aux1, GromovHausdorff.HD, le_max_left
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
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
grw : (⨆ (y : Y), ⨅ (x : X), (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y)) + dist f g ≤ HD g + dist f g
grw₁ :
  (⨆ (y : Y), ⨅ (x : X), (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y)) + dist f g ≤
    max (⨆ (x : X), ⨅ (y : Y), (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y))
        (⨆ (y : Y), ⨅ (x : X), (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y)) +
      dist f g
grw₂ grw₃ :
  (⨆ (y : Y), ⨅ (x : X), (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y)) + dist f g ≤
    (⨆ (y : Y), ⨅ (x : X), (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y)) + dist f g
⊢ ⨆ (y : Y), ⨅ (x : X), (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) ≤ HD g + dist f g

Tactic:
grw [HD_lipschitz_aux2 f g, HD, ← le_max_right]

Premises used: le_max_right, GromovHausdorff.HD, _private.0.GromovHausdorff.HD_lipschitz_aux2
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty X
inst_3 : Nonempty Y
⊢ Continuous (X := Cb X Y) HD

Tactic:
LipschitzWith.continuous (LipschitzWith.of_le_add HD_lipschitz_aux3)

Premises used: setOf, LipschitzWith.of_le_add, LipschitzWith.continuous, _private.0.GromovHausdorff.HD_lipschitz_aux3
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : CompactSpace X
inst_3 : CompactSpace Y
⊢ IsCompact (X := Cb X Y) (candidatesB X Y)

Tactic:
arzela_ascoli₂
      (Icc 0 (maxVar X Y) : Set ℝ) isCompact_Icc (candidatesB X Y) closed_candidatesB ?_ ?_

Premises used: _private.0.GromovHausdorff.candidatesB, CompactIccSpace.isCompact_Icc, Set.Icc, OfNat.ofNat, _private.0.GromovHausdorff.maxVar, NNReal.toReal, BoundedContinuousFunction.arzela_ascoli₂, _private.0.GromovHausdorff.closed_candidatesB
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : CompactSpace X
inst_3 : CompactSpace Y
refine_1 :
  ∀ (f : (X ⊕ Y) × (X ⊕ Y) →ᵇ ℝ) (x : (X ⊕ Y) × (X ⊕ Y)),
    Membership.mem (γ := Set ((X ⊕ Y) × (X ⊕ Y) →ᵇ ℝ)) (candidatesB X Y) f →
      Membership.mem (α := ℝ) (Icc 0 (↑(maxVar X Y) : ℝ)) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) x : ℝ)
refine_2 :
  Equicontinuous (X := (X ⊕ Y) × (X ⊕ Y)) (α := ℝ) fun (x : (↑(candidatesB X Y) : Type (max u v))) ↦
    (⇑(↑x : (X ⊕ Y) × (X ⊕ Y) →ᵇ ℝ) : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ)
⊢ IsCompact (X := Cb X Y) (candidatesB X Y)

Tactic:
refine arzela_ascoli₂
      (Icc 0 (maxVar X Y) : Set ℝ) isCompact_Icc (candidatesB X Y) closed_candidatesB ?_ ?_

Premises used: _private.0.GromovHausdorff.candidatesB, CompactIccSpace.isCompact_Icc, Set.Icc, OfNat.ofNat, _private.0.GromovHausdorff.maxVar, NNReal.toReal, BoundedContinuousFunction.arzela_ascoli₂, _private.0.GromovHausdorff.closed_candidatesB
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : CompactSpace X
inst_3 : CompactSpace Y
f : (X ⊕ Y) × (X ⊕ Y) →ᵇ ℝ
x1 x2 : X ⊕ Y
hf : Membership.mem (γ := Set ((X ⊕ Y) × (X ⊕ Y) →ᵇ ℝ)) (candidatesB X Y) f
⊢ LE.le (α := ℝ) (0 : ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x1, x2) : ℝ) ∧
    (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x1, x2) ≤ (↑(maxVar X Y) : ℝ)

Tactic:
⟨candidates_nonneg hf, candidates_le_maxVar hf⟩

Premises used: _private.0.GromovHausdorff.candidates_le_maxVar, And.intro, _private.0.GromovHausdorff.candidates_nonneg
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : CompactSpace X
inst_3 : CompactSpace Y
f : (X ⊕ Y) × (X ⊕ Y) →ᵇ ℝ
x1 x2 : X ⊕ Y
hf : Membership.mem (γ := Set ((X ⊕ Y) × (X ⊕ Y) →ᵇ ℝ)) (candidatesB X Y) f
⊢ LE.le (α := ℝ) (0 : ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x1, x2) : ℝ) ∧
    (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x1, x2) ≤ (↑(maxVar X Y) : ℝ)

Tactic:
exact ⟨candidates_nonneg hf, candidates_le_maxVar hf⟩
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : CompactSpace X
inst_3 : CompactSpace Y
⊢ Equicontinuous (X := (X ⊕ Y) × (X ⊕ Y)) (α := ℝ) fun (x : (↑(candidatesB X Y) : Type (max u v))) ↦
    (⇑(↑x : (X ⊕ Y) × (X ⊕ Y) →ᵇ ℝ) : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ)

Tactic:
equicontinuous_of_continuity_modulus (fun t => 2 * maxVar X Y * t) ?_ _ ?_

Premises used: HMul.hMul, setOf, Metric.equicontinuous_of_continuity_modulus, OfNat.ofNat, _private.0.GromovHausdorff.maxVar, NNReal.toReal