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 Y
f : Cb X Y
C Cf : ℝ
hCf : Membership.mem (γ := Set ℝ) (upperBounds (range (ι := (X ⊕ Y) × (X ⊕ Y)) (⇑f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ))) Cf
x : X
⊢ ⨅ (y : Y), HAdd.hAdd (α := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ) C ≤ Cf + C

Tactic:
calc
    ⨅ y, f (inl x, inr y) + C ≤ f (inl x, inr default) + C := ciInf_le (HD_below_aux1 C) default
    _ ≤ Cf + C := add_le_add ((fun x => hCf (mem_range_self x)) _) le_rfl

Premises used: Set.mem_range_self, Inhabited.default, le_rfl, add_le_add, Prod.mk, Sum.inl, ciInf_le, Sum.inr, DFunLike.coe, GromovHausdorff.HD_below_aux1
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
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
grw₁ : (X ⊕ Y) × (X ⊕ Y)
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
grw₃ : (X ⊕ Y) × (X ⊕ Y)
⊢ cf + C ≤ HAdd.hAdd (α := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ) C

Tactic:
grw [hcf (mem_range_self _)]

Premises used: Set.mem_range_self
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty X
f : Cb X Y
C : ℝ
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)
⊢ 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

Premises used: BoundedContinuousFunction.isBounded_range, Bornology.IsBounded.bddAbove
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
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)

Tactic:
⟨Cf + C, forall_mem_range.2 fun y => ?_⟩

Premises used: Iff.mpr, Set.forall_mem_range, BddAbove, Set.Nonempty, HAdd.hAdd, 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
f : Cb X Y
C Cf : ℝ
hCf : Membership.mem (γ := Set ℝ) (upperBounds (range (ι := (X ⊕ Y) × (X ⊕ Y)) (⇑f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ))) Cf
refine : ∀ (y : Y), ⨅ (x : X), HAdd.hAdd (α := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ) C ≤ Cf + C
⊢ BddAbove (α := ℝ)
    (range fun (y : Y) ↦ ⨅ (x : X), HAdd.hAdd (α := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ) C)

Tactic:
refine ⟨Cf + C, forall_mem_range.2 fun y => ?_⟩
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
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
y : Y
⊢ ⨅ (x : X), HAdd.hAdd (α := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ) C ≤
    HAdd.hAdd (α := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl default, inr y) : ℝ) C

Tactic:
ciInf_le (HD_below_aux2 C) default

Premises used: Inhabited.default, ciInf_le, GromovHausdorff.HD_below_aux2
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
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
y : Y
⊢ HAdd.hAdd (α := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl default, inr y) : ℝ) C ≤ Cf + C

Tactic:
add_le_add ((fun x => hCf (mem_range_self x)) _) le_rfl

Premises used: Set.mem_range_self, le_rfl, add_le_add
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
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
y : Y
⊢ ⨅ (x : X), HAdd.hAdd (α := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ) C ≤ Cf + C

Tactic:
calc
    ⨅ x, f (inl x, inr y) + C ≤ f (inl default, inr y) + C := ciInf_le (HD_below_aux2 C) default
    _ ≤ Cf + C := add_le_add ((fun x => hCf (mem_range_self x)) _) le_rfl

Premises used: Set.mem_range_self, Inhabited.default, le_rfl, add_le_add, Prod.mk, Sum.inl, ciInf_le, GromovHausdorff.HD_below_aux2, Sum.inr, DFunLike.coe
-- 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),
    ⨆ (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
⊢ ⨆ (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

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
⊢ ∀ (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)
-- 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),
    ⨆ (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
⊢ ⨆ (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

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
⊢ ∀ (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)
-- 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 (α := ℝ) (⨆ (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
-- 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 (α := ℝ) (⨆ (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)

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 (α := ℝ) (⨆ (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
refine_1 : Monotone (HAdd.hAdd (α := ℝ → ℝ) id fun (x : ℝ) ↦ dist f g)
refine_2 : BddBelow (α := ℝ) (range fun (y : Y) ↦ (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y))
⊢ (⨅ (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)

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 (α := ℝ) (⨆ (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_1 : X
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 (α := ℝ) (⨆ (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
⊢ BddBelow (α := ℝ) (range fun (y : Y) ↦ (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 (α := ℝ) (⨆ (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
⊢ BddBelow (α := ℝ) (range fun (y : Y) ↦ (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 (α := ℝ) (⨆ (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)

Tactic:
have E1 : ∀ x, (⨅ y, g (inl x, inr y)) + dist f g = ⨅ y, g (inl x, inr y) + dist f g := by
    intro x
    refine Monotone.map_ciInf_of_continuousAt (continuousAt_id.add continuousAt_const) ?_ ?_
    · intro x y hx
      simpa
    · change BddBelow (range fun y : Y => 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 (α := ℝ) (⨆ (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))
E1 :
  ∀ (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)
⊢ (⨆ (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

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 (α := ℝ) (⨆ (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))
E1 :
  ∀ (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)
refine_1 : Monotone (HAdd.hAdd (α := ℝ → ℝ) id fun (x : ℝ) ↦ dist f g)
refine_2 : BddAbove (α := ℝ) (range fun (x : X) ↦ ⨅ (y : Y), (g : (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 =
    ⨆ (x : X), (⨅ (y : Y), (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 (α := ℝ) (⨆ (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))
E1 :
  ∀ (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)
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 (α := ℝ) (⨆ (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))
E1 :
  ∀ (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)
⊢ BddAbove (α := ℝ) (range fun (x : X) ↦ ⨅ (y : Y), (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y))

Tactic:
simpa using HD_bound_aux1 _ 0

Premises used: _private.0.GromovHausdorff.HD_bound_aux1, 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 (α := ℝ) (⨆ (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))
E1 :
  ∀ (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)
⊢ (⨆ (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

Tactic:
have E2 : (⨆ x, ⨅ y, g (inl x, inr y)) + dist f g = ⨆ x, (⨅ y, 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_aux1 _ 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 (α := ℝ) (⨆ (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))
E1 :
  ∀ (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)
E2 :
  (⨆ (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) ≤
    (⨆ (x : X), ⨅ (y : Y), (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y)) + dist f g

Tactic:
simpa [E2, E1, Function.comp]

Premises used: Function.comp