case intro
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
f✝ : GromovHausdorff.ProdSpaceFun X Y
x y z t : X ⊕ Y
f g : GromovHausdorff.Cb X Y
cg : ℝ
hcg : cg ∈ lowerBounds (range ↑g)
⊢ (⨆ (x : X), ⨅ (y : Y), ↑f (inl x, inr y)) ≤ (⨆ (x : X), ⨅ (y : Y), ↑g (inl x, inr y)) + dist f g
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
f✝ : GromovHausdorff.ProdSpaceFun X Y
x y z t : X ⊕ Y
f g : GromovHausdorff.Cb X Y
⊢ (⨆ (x : X), ⨅ (y : Y), ↑f (inl x, inr y)) ≤ (⨆ (x : X), ⨅ (y : Y), ↑g (inl x, inr y)) + dist f g
rcases (Real.bounded_iff_bddBelow_bddAbove.1 g.bounded_range).1 with ⟨cg, hcg⟩
case intro
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
f✝ : GromovHausdorff.ProdSpaceFun X Y
x y z t : X ⊕ Y
f g : GromovHausdorff.Cb X Y
cg : ℝ
hcg : cg ∈ lowerBounds (range ↑g)
Hcg : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cg ≤ ↑g x
⊢ (⨆ (x : X), ⨅ (y : Y), ↑f (inl x, inr y)) ≤ (⨆ (x : X), ⨅ (y : Y), ↑g (inl x, inr y)) + dist f g
case intro
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
f✝ : GromovHausdorff.ProdSpaceFun X Y
x y z t : X ⊕ Y
f g : GromovHausdorff.Cb X Y
cg : ℝ
hcg : cg ∈ lowerBounds (range ↑g)
⊢ (⨆ (x : X), ⨅ (y : Y), ↑f (inl x, inr y)) ≤ (⨆ (x : X), ⨅ (y : Y), ↑g (inl x, inr y)) + dist f g
have Hcg : ∀ x, cg ≤ g x := fun x => hcg (mem_range_self x)
case intro.intro
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
f✝ : GromovHausdorff.ProdSpaceFun X Y
x y z t : X ⊕ Y
f g : GromovHausdorff.Cb X Y
cg : ℝ
hcg : cg ∈ lowerBounds (range ↑g)
Hcg : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cg ≤ ↑g x
cf : ℝ
hcf : cf ∈ lowerBounds (range ↑f)
⊢ (⨆ (x : X), ⨅ (y : Y), ↑f (inl x, inr y)) ≤ (⨆ (x : X), ⨅ (y : Y), ↑g (inl x, inr y)) + dist f g
case intro
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
f✝ : GromovHausdorff.ProdSpaceFun X Y
x y z t : X ⊕ Y
f g : GromovHausdorff.Cb X Y
cg : ℝ
hcg : cg ∈ lowerBounds (range ↑g)
Hcg : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cg ≤ ↑g x
⊢ (⨆ (x : X), ⨅ (y : Y), ↑f (inl x, inr y)) ≤ (⨆ (x : X), ⨅ (y : Y), ↑g (inl x, inr y)) + dist f g
rcases (Real.bounded_iff_bddBelow_bddAbove.1 f.bounded_range).1 with ⟨cf, hcf⟩
case intro.intro
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
f✝ : GromovHausdorff.ProdSpaceFun X Y
x y z t : X ⊕ Y
f g : GromovHausdorff.Cb X Y
cg : ℝ
hcg : cg ∈ lowerBounds (range ↑g)
Hcg : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cg ≤ ↑g x
cf : ℝ
hcf : cf ∈ lowerBounds (range ↑f)
Hcf : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cf ≤ ↑f x
⊢ (⨆ (x : X), ⨅ (y : Y), ↑f (inl x, inr y)) ≤ (⨆ (x : X), ⨅ (y : Y), ↑g (inl x, inr y)) + dist f g
case intro.intro
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
f✝ : GromovHausdorff.ProdSpaceFun X Y
x y z t : X ⊕ Y
f g : GromovHausdorff.Cb X Y
cg : ℝ
hcg : cg ∈ lowerBounds (range ↑g)
Hcg : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cg ≤ ↑g x
cf : ℝ
hcf : cf ∈ lowerBounds (range ↑f)
⊢ (⨆ (x : X), ⨅ (y : Y), ↑f (inl x, inr y)) ≤ (⨆ (x : X), ⨅ (y : Y), ↑g (inl x, inr y)) + dist f g
have Hcf : ∀ x, cf ≤ f x := fun x => hcf (mem_range_self x)
case intro.intro
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
f✝ : GromovHausdorff.ProdSpaceFun X Y
x y z t : X ⊕ Y
f g : GromovHausdorff.Cb X Y
cg : ℝ
hcg : cg ∈ lowerBounds (range ↑g)
Hcg : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cg ≤ ↑g x
cf : ℝ
hcf : cf ∈ lowerBounds (range ↑f)
Hcf : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cf ≤ ↑f x
Z : (⨆ (x : X), ⨅ (y : Y), ↑f (inl x, inr y)) ≤ ⨆ (x : X), ⨅ (y : Y), ↑g (inl x, inr y) + dist f g
⊢ (⨆ (x : X), ⨅ (y : Y), ↑f (inl x, inr y)) ≤ (⨆ (x : X), ⨅ (y : Y), ↑g (inl x, inr y)) + dist f g
case intro.intro
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
f✝ : GromovHausdorff.ProdSpaceFun X Y
x y z t : X ⊕ Y
f g : GromovHausdorff.Cb X Y
cg : ℝ
hcg : cg ∈ lowerBounds (range ↑g)
Hcg : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cg ≤ ↑g x
cf : ℝ
hcf : cf ∈ lowerBounds (range ↑f)
Hcf : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cf ≤ ↑f x
⊢ (⨆ (x : X), ⨅ (y : Y), ↑f (inl x, inr y)) ≤ (⨆ (x : X), ⨅ (y : Y), ↑g (inl x, inr y)) + dist f g
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_range_iff.2 fun i => Hcf _⟩ fun y => coe_le_coe_add_dist
no goals
case intro.intro
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
f✝ : GromovHausdorff.ProdSpaceFun X Y
x y z t : X ⊕ Y
f g : GromovHausdorff.Cb X Y
cg : ℝ
hcg : cg ∈ lowerBounds (range ↑g)
Hcg : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cg ≤ ↑g x
cf : ℝ
hcf : cf ∈ lowerBounds (range ↑f)
Hcf : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cf ≤ ↑f x
Z : (⨆ (x : X), ⨅ (y : Y), ↑f (inl x, inr y)) ≤ ⨆ (x : X), ⨅ (y : Y), ↑g (inl x, inr y) + dist f g
E1 : ∀ (x : X), (⨅ (y : Y), ↑g (inl x, inr y)) + dist f g = ⨅ (y : Y), ↑g (inl x, inr y) + dist f g
E2 : (⨆ (x : X), ⨅ (y : Y), ↑g (inl x, inr y)) + dist f g = ⨆ (x : X), (⨅ (y : Y), ↑g (inl x, inr y)) + dist f g
⊢ (⨆ (x : X), ⨅ (y : Y), ↑f (inl x, inr y)) ≤ (⨆ (x : X), ⨅ (y : Y), ↑g (inl x, inr y)) + dist f g
simpa [E2, E1, Function.comp]
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
f✝ : GromovHausdorff.ProdSpaceFun X Y
x✝ y z t : X ⊕ Y
f g : GromovHausdorff.Cb X Y
cg : ℝ
hcg : cg ∈ lowerBounds (range ↑g)
Hcg : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cg ≤ ↑g x
cf : ℝ
hcf : cf ∈ lowerBounds (range ↑f)
Hcf : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cf ≤ ↑f x
Z : (⨆ (x : X), ⨅ (y : Y), ↑f (inl x, inr y)) ≤ ⨆ (x : X), ⨅ (y : Y), ↑g (inl x, inr y) + dist f g
x : X
⊢ (⨅ (y : Y), ↑g (inl x, inr y)) + dist f g = ⨅ (y : Y), ↑g (inl x, inr y) + dist f g
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
f✝ : GromovHausdorff.ProdSpaceFun X Y
x y z t : X ⊕ Y
f g : GromovHausdorff.Cb X Y
cg : ℝ
hcg : cg ∈ lowerBounds (range ↑g)
Hcg : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cg ≤ ↑g x
cf : ℝ
hcf : cf ∈ lowerBounds (range ↑f)
Hcf : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cf ≤ ↑f x
Z : (⨆ (x : X), ⨅ (y : Y), ↑f (inl x, inr y)) ≤ ⨆ (x : X), ⨅ (y : Y), ↑g (inl x, inr y) + dist f g
⊢ ∀ (x : X), (⨅ (y : Y), ↑g (inl x, inr y)) + dist f g = ⨅ (y : Y), ↑g (inl x, inr y) + dist f g
intro x
case refine'_1
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
f✝ : GromovHausdorff.ProdSpaceFun X Y
x✝ y z t : X ⊕ Y
f g : GromovHausdorff.Cb X Y
cg : ℝ
hcg : cg ∈ lowerBounds (range ↑g)
Hcg : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cg ≤ ↑g x
cf : ℝ
hcf : cf ∈ lowerBounds (range ↑f)
Hcf : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cf ≤ ↑f x
Z : (⨆ (x : X), ⨅ (y : Y), ↑f (inl x, inr y)) ≤ ⨆ (x : X), ⨅ (y : Y), ↑g (inl x, inr y) + dist f g
x : X
⊢ Monotone fun x => id x + dist f g

case refine'_2
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
f✝ : GromovHausdorff.ProdSpaceFun X Y
x✝ y z t : X ⊕ Y
f g : GromovHausdorff.Cb X Y
cg : ℝ
hcg : cg ∈ lowerBounds (range ↑g)
Hcg : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cg ≤ ↑g x
cf : ℝ
hcf : cf ∈ lowerBounds (range ↑f)
Hcf : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cf ≤ ↑f x
Z : (⨆ (x : X), ⨅ (y : Y), ↑f (inl x, inr y)) ≤ ⨆ (x : X), ⨅ (y : Y), ↑g (inl x, inr y) + dist f g
x : X
⊢ BddBelow (range fun y => ↑g (inl x, inr y))
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
f✝ : GromovHausdorff.ProdSpaceFun X Y
x✝ y z t : X ⊕ Y
f g : GromovHausdorff.Cb X Y
cg : ℝ
hcg : cg ∈ lowerBounds (range ↑g)
Hcg : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cg ≤ ↑g x
cf : ℝ
hcf : cf ∈ lowerBounds (range ↑f)
Hcf : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cf ≤ ↑f x
Z : (⨆ (x : X), ⨅ (y : Y), ↑f (inl x, inr y)) ≤ ⨆ (x : X), ⨅ (y : Y), ↑g (inl x, inr y) + dist f g
x : X
⊢ (⨅ (y : Y), ↑g (inl x, inr y)) + dist f g = ⨅ (y : Y), ↑g (inl x, inr y) + dist f g
refine' Monotone.map_ciInf_of_continuousAt (continuousAt_id.add continuousAt_const) _ _
case refine'_1
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
f✝ : GromovHausdorff.ProdSpaceFun X Y
x✝¹ y✝ z t : X ⊕ Y
f g : GromovHausdorff.Cb X Y
cg : ℝ
hcg : cg ∈ lowerBounds (range ↑g)
Hcg : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cg ≤ ↑g x
cf : ℝ
hcf : cf ∈ lowerBounds (range ↑f)
Hcf : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cf ≤ ↑f x
Z : (⨆ (x : X), ⨅ (y : Y), ↑f (inl x, inr y)) ≤ ⨆ (x : X), ⨅ (y : Y), ↑g (inl x, inr y) + dist f g
x✝ : X
x y : ℝ
hx : x ≤ y
⊢ (fun x => id x + dist f g) x ≤ (fun x => id x + dist f g) y
case refine'_1
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
f✝ : GromovHausdorff.ProdSpaceFun X Y
x✝ y z t : X ⊕ Y
f g : GromovHausdorff.Cb X Y
cg : ℝ
hcg : cg ∈ lowerBounds (range ↑g)
Hcg : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cg ≤ ↑g x
cf : ℝ
hcf : cf ∈ lowerBounds (range ↑f)
Hcf : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cf ≤ ↑f x
Z : (⨆ (x : X), ⨅ (y : Y), ↑f (inl x, inr y)) ≤ ⨆ (x : X), ⨅ (y : Y), ↑g (inl x, inr y) + dist f g
x : X
⊢ Monotone fun x => id x + dist f g
intro x y hx
no goals
case refine'_1
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
f✝ : GromovHausdorff.ProdSpaceFun X Y
x✝¹ y✝ z t : X ⊕ Y
f g : GromovHausdorff.Cb X Y
cg : ℝ
hcg : cg ∈ lowerBounds (range ↑g)
Hcg : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cg ≤ ↑g x
cf : ℝ
hcf : cf ∈ lowerBounds (range ↑f)
Hcf : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cf ≤ ↑f x
Z : (⨆ (x : X), ⨅ (y : Y), ↑f (inl x, inr y)) ≤ ⨆ (x : X), ⨅ (y : Y), ↑g (inl x, inr y) + dist f g
x✝ : X
x y : ℝ
hx : x ≤ y
⊢ (fun x => id x + dist f g) x ≤ (fun x => id x + dist f g) y
simpa
case refine'_2
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
f✝ : GromovHausdorff.ProdSpaceFun X Y
x✝ y z t : X ⊕ Y
f g : GromovHausdorff.Cb X Y
cg : ℝ
hcg : cg ∈ lowerBounds (range ↑g)
Hcg : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cg ≤ ↑g x
cf : ℝ
hcf : cf ∈ lowerBounds (range ↑f)
Hcf : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cf ≤ ↑f x
Z : (⨆ (x : X), ⨅ (y : Y), ↑f (inl x, inr y)) ≤ ⨆ (x : X), ⨅ (y : Y), ↑g (inl x, inr y) + dist f g
x : X
⊢ BddBelow (range fun y => ↑g (inl x, inr y))
case refine'_2
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
f✝ : GromovHausdorff.ProdSpaceFun X Y
x✝ y z t : X ⊕ Y
f g : GromovHausdorff.Cb X Y
cg : ℝ
hcg : cg ∈ lowerBounds (range ↑g)
Hcg : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cg ≤ ↑g x
cf : ℝ
hcf : cf ∈ lowerBounds (range ↑f)
Hcf : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cf ≤ ↑f x
Z : (⨆ (x : X), ⨅ (y : Y), ↑f (inl x, inr y)) ≤ ⨆ (x : X), ⨅ (y : Y), ↑g (inl x, inr y) + dist f g
x : X
⊢ BddBelow (range fun y => ↑g (inl x, inr y))
show BddBelow (range fun y : Y => g (inl x, inr y))
no goals
case refine'_2
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
f✝ : GromovHausdorff.ProdSpaceFun X Y
x✝ y z t : X ⊕ Y
f g : GromovHausdorff.Cb X Y
cg : ℝ
hcg : cg ∈ lowerBounds (range ↑g)
Hcg : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cg ≤ ↑g x
cf : ℝ
hcf : cf ∈ lowerBounds (range ↑f)
Hcf : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cf ≤ ↑f x
Z : (⨆ (x : X), ⨅ (y : Y), ↑f (inl x, inr y)) ≤ ⨆ (x : X), ⨅ (y : Y), ↑g (inl x, inr y) + dist f g
x : X
⊢ BddBelow (range fun y => ↑g (inl x, inr y))
exact ⟨cg, forall_range_iff.2 fun i => Hcg _⟩
case refine'_1
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
f✝ : GromovHausdorff.ProdSpaceFun X Y
x y z t : X ⊕ Y
f g : GromovHausdorff.Cb X Y
cg : ℝ
hcg : cg ∈ lowerBounds (range ↑g)
Hcg : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cg ≤ ↑g x
cf : ℝ
hcf : cf ∈ lowerBounds (range ↑f)
Hcf : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cf ≤ ↑f x
Z : (⨆ (x : X), ⨅ (y : Y), ↑f (inl x, inr y)) ≤ ⨆ (x : X), ⨅ (y : Y), ↑g (inl x, inr y) + dist f g
E1 : ∀ (x : X), (⨅ (y : Y), ↑g (inl x, inr y)) + dist f g = ⨅ (y : Y), ↑g (inl x, inr y) + dist f g
⊢ Monotone fun x => id x + dist f g

case refine'_2
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
f✝ : GromovHausdorff.ProdSpaceFun X Y
x y z t : X ⊕ Y
f g : GromovHausdorff.Cb X Y
cg : ℝ
hcg : cg ∈ lowerBounds (range ↑g)
Hcg : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cg ≤ ↑g x
cf : ℝ
hcf : cf ∈ lowerBounds (range ↑f)
Hcf : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cf ≤ ↑f x
Z : (⨆ (x : X), ⨅ (y : Y), ↑f (inl x, inr y)) ≤ ⨆ (x : X), ⨅ (y : Y), ↑g (inl x, inr y) + dist f g
E1 : ∀ (x : X), (⨅ (y : Y), ↑g (inl x, inr y)) + dist f g = ⨅ (y : Y), ↑g (inl x, inr y) + dist f g
⊢ BddAbove (range fun x => ⨅ (y : Y), ↑g (inl x, inr y))
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
f✝ : GromovHausdorff.ProdSpaceFun X Y
x y z t : X ⊕ Y
f g : GromovHausdorff.Cb X Y
cg : ℝ
hcg : cg ∈ lowerBounds (range ↑g)
Hcg : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cg ≤ ↑g x
cf : ℝ
hcf : cf ∈ lowerBounds (range ↑f)
Hcf : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cf ≤ ↑f x
Z : (⨆ (x : X), ⨅ (y : Y), ↑f (inl x, inr y)) ≤ ⨆ (x : X), ⨅ (y : Y), ↑g (inl x, inr y) + dist f g
E1 : ∀ (x : X), (⨅ (y : Y), ↑g (inl x, inr y)) + dist f g = ⨅ (y : Y), ↑g (inl x, inr y) + dist f g
⊢ (⨆ (x : X), ⨅ (y : Y), ↑g (inl x, inr y)) + dist f g = ⨆ (x : X), (⨅ (y : Y), ↑g (inl x, inr y)) + dist f g
refine' Monotone.map_ciSup_of_continuousAt (continuousAt_id.add continuousAt_const) _ _
case refine'_1
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
f✝ : GromovHausdorff.ProdSpaceFun X Y
x✝ y✝ z t : X ⊕ Y
f g : GromovHausdorff.Cb X Y
cg : ℝ
hcg : cg ∈ lowerBounds (range ↑g)
Hcg : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cg ≤ ↑g x
cf : ℝ
hcf : cf ∈ lowerBounds (range ↑f)
Hcf : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cf ≤ ↑f x
Z : (⨆ (x : X), ⨅ (y : Y), ↑f (inl x, inr y)) ≤ ⨆ (x : X), ⨅ (y : Y), ↑g (inl x, inr y) + dist f g
E1 : ∀ (x : X), (⨅ (y : Y), ↑g (inl x, inr y)) + dist f g = ⨅ (y : Y), ↑g (inl x, inr y) + dist f g
x y : ℝ
hx : x ≤ y
⊢ (fun x => id x + dist f g) x ≤ (fun x => id x + dist f g) y
case refine'_1
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
f✝ : GromovHausdorff.ProdSpaceFun X Y
x y z t : X ⊕ Y
f g : GromovHausdorff.Cb X Y
cg : ℝ
hcg : cg ∈ lowerBounds (range ↑g)
Hcg : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cg ≤ ↑g x
cf : ℝ
hcf : cf ∈ lowerBounds (range ↑f)
Hcf : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cf ≤ ↑f x
Z : (⨆ (x : X), ⨅ (y : Y), ↑f (inl x, inr y)) ≤ ⨆ (x : X), ⨅ (y : Y), ↑g (inl x, inr y) + dist f g
E1 : ∀ (x : X), (⨅ (y : Y), ↑g (inl x, inr y)) + dist f g = ⨅ (y : Y), ↑g (inl x, inr y) + dist f g
⊢ Monotone fun x => id x + dist f g
intro x y hx
no goals
case refine'_1
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
f✝ : GromovHausdorff.ProdSpaceFun X Y
x✝ y✝ z t : X ⊕ Y
f g : GromovHausdorff.Cb X Y
cg : ℝ
hcg : cg ∈ lowerBounds (range ↑g)
Hcg : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cg ≤ ↑g x
cf : ℝ
hcf : cf ∈ lowerBounds (range ↑f)
Hcf : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cf ≤ ↑f x
Z : (⨆ (x : X), ⨅ (y : Y), ↑f (inl x, inr y)) ≤ ⨆ (x : X), ⨅ (y : Y), ↑g (inl x, inr y) + dist f g
E1 : ∀ (x : X), (⨅ (y : Y), ↑g (inl x, inr y)) + dist f g = ⨅ (y : Y), ↑g (inl x, inr y) + dist f g
x y : ℝ
hx : x ≤ y
⊢ (fun x => id x + dist f g) x ≤ (fun x => id x + dist f g) y
simpa
no goals
case refine'_2
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
f✝ : GromovHausdorff.ProdSpaceFun X Y
x y z t : X ⊕ Y
f g : GromovHausdorff.Cb X Y
cg : ℝ
hcg : cg ∈ lowerBounds (range ↑g)
Hcg : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cg ≤ ↑g x
cf : ℝ
hcf : cf ∈ lowerBounds (range ↑f)
Hcf : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cf ≤ ↑f x
Z : (⨆ (x : X), ⨅ (y : Y), ↑f (inl x, inr y)) ≤ ⨆ (x : X), ⨅ (y : Y), ↑g (inl x, inr y) + dist f g
E1 : ∀ (x : X), (⨅ (y : Y), ↑g (inl x, inr y)) + dist f g = ⨅ (y : Y), ↑g (inl x, inr y) + dist f g
⊢ BddAbove (range fun x => ⨅ (y : Y), ↑g (inl x, inr y))
simpa using HD_bound_aux1 _ 0