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
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)
⊢ (⨅ (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_2 : BddBelow (α := ℝ) (range fun (y : Y) ↦ (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y))
Tactic: refine Monotone.map_ciInf_of_continuousAt (continuousAt_id.add continuousAt_const) ?_ ?_
-- 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
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), (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 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)
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 _⟩
-- 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))
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
have refine_1 : Monotone (HAdd.hAdd (α := ℝ → ℝ) id fun (x : ℝ) ↦ dist f g)
Tactic: refine Monotone.map_ciSup_of_continuousAt (continuousAt_id.add continuousAt_const) ?_ ?_
-- 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))
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)
⊢ (⨆ (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
have refine_2 : BddAbove (α := ℝ) (range fun (x : X) ↦ ⨅ (y : Y), (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y))
Tactic: refine Monotone.map_ciSup_of_continuousAt (continuousAt_id.add continuousAt_const) ?_ ?_
-- 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
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), (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 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
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
-- 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
⊢ ⨆ (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
have 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
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
⊢ ⨆ (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
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
⊢ ⨆ (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
have 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
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
⊢ ⨆ (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
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
⊢ ⨆ (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
have 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))
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
-- 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 (α := ℝ) (⨆ (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)
have refine_1 : Monotone (HAdd.hAdd (α := ℝ → ℝ) id fun (x : ℝ) ↦ dist f g)
Tactic: refine Monotone.map_ciInf_of_continuousAt (continuousAt_id.add continuousAt_const) ?_ ?_
-- 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 (α := ℝ) (⨆ (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)
⊢ (⨅ (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)
have refine_2 : BddBelow (α := ℝ) (range fun (x : X) ↦ (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y))
Tactic: refine Monotone.map_ciInf_of_continuousAt (continuousAt_id.add continuousAt_const) ?_ ?_
-- 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
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), (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
have 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)
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 _⟩
-- 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 (α := ℝ) (⨆ (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
have refine_1 : Monotone (HAdd.hAdd (α := ℝ → ℝ) id fun (x : ℝ) ↦ dist f g)
Tactic: refine Monotone.map_ciSup_of_continuousAt (continuousAt_id.add continuousAt_const) ?_ ?_
-- 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 (α := ℝ) (⨆ (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)
⊢ (⨆ (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
have refine_2 : BddAbove (α := ℝ) (range fun (y : Y) ↦ ⨅ (x : X), (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y))
Tactic: refine Monotone.map_ciSup_of_continuousAt (continuousAt_id.add continuousAt_const) ?_ ?_
-- 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
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), (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
have 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
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
-- 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) ≤ HD g + dist f g
have grw : (⨆ (x : X), ⨅ (y : Y), (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y)) + dist f g ≤ HD g + dist f g
Tactic: grw [HD_lipschitz_aux1 f g, HD, ← le_max_left]
-- 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
grw : (⨆ (x : X), ⨅ (y : Y), (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y)) + dist f g ≤ HD g + dist f g
⊢ ⨆ (x : X), ⨅ (y : Y), (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) ≤ HD g + dist f g
have 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
Tactic: grw [HD_lipschitz_aux1 f g, HD, ← le_max_left]
-- 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
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
⊢ ⨆ (x : X), ⨅ (y : Y), (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) ≤ HD g + dist f g
have 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
Tactic: grw [HD_lipschitz_aux1 f g, HD, ← le_max_left]
-- 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
⊢ ⨆ (y : Y), ⨅ (x : X), (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) ≤ HD g + dist f g
have grw : (⨆ (y : Y), ⨅ (x : X), (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y)) + dist f g ≤ HD g + dist f g
Tactic: grw [HD_lipschitz_aux2 f g, HD, ← le_max_right]
-- 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
grw : (⨆ (y : Y), ⨅ (x : X), (g : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y)) + dist f g ≤ HD g + dist f g
⊢ ⨆ (y : Y), ⨅ (x : X), (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) ≤ HD g + dist f g
have 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
Tactic: grw [HD_lipschitz_aux2 f g, HD, ← le_max_right]
-- 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
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
⊢ ⨆ (y : Y), ⨅ (x : X), (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) ≤ HD g + dist f g
have 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
Tactic: grw [HD_lipschitz_aux2 f g, HD, ← le_max_right]