mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Separation.LinearUpperLowerSetTopology

Goal state before:
pp: case inr
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : Topology.IsUpperSet α
s t : Set α
hcst : Disjoint (closure s) t
hsct : Disjoint s (closure t)
a : α
ha : a ∈ s
⊢ Disjoint (nhdsSet s) (nhdsSet t)

Tactic:
obtain (rfl | ⟨b, hb⟩) := t.eq_empty_or_nonempty

Goal state after:
case inr.inl
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : Topology.IsUpperSet α
s : Set α
a : α
ha : a ∈ s
hcst : Disjoint (closure s) ∅
hsct : Disjoint s (closure ∅)
⊢ Disjoint (nhdsSet s) (nhdsSet ∅)

case inr.inr
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : Topology.IsUpperSet α
s t : Set α
hcst : Disjoint (closure s) t
hsct : Disjoint s (closure t)
a : α
ha : a ∈ s
b : α
hb : b ∈ t
⊢ Disjoint (nhdsSet s) (nhdsSet t)
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: x y : GHSpace
hxy : dist x y = 0
Φ : x.Rep → ↥(lp (fun n ↦ ℝ) ∞)
Ψ : y.Rep → ↥(lp (fun n ↦ ℝ) ∞)
Φisom : Isometry Φ
Ψisom : Isometry Ψ
DΦΨ : ghDist x.Rep y.Rep = hausdorffDist (range Φ) (range Ψ)
⊢ x = y

Tactic:
rw [← dist_ghDist, hxy] at DΦΨ

Goal state after:
x y : GHSpace
hxy : dist x y = 0
Φ : x.Rep → ↥(lp (fun n ↦ ℝ) ∞)
Ψ : y.Rep → ↥(lp (fun n ↦ ℝ) ∞)
Φisom : Isometry Φ
Ψisom : Isometry Ψ
DΦΨ : 0 = hausdorffDist (range Φ) (range Ψ)
⊢ x = y
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: x y : GHSpace
hxy : dist x y = 0
Φ : x.Rep → ↥(lp (fun n ↦ ℝ) ∞)
Ψ : y.Rep → ↥(lp (fun n ↦ ℝ) ∞)
Φisom : Isometry Φ
Ψisom : Isometry Ψ
DΦΨ : 0 = hausdorffDist (range Φ) (range Ψ)
this : range Φ = range Ψ
⊢ (↑(range Ψ) ≃ᵢ y.Rep) = (↑(range Φ) ≃ᵢ y.Rep)

Tactic:
rw [this]

Goal state after:
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: δ : ℝ
δpos : δ > 0
ε : ℝ := 2 / 5 * δ
εpos : 0 < ε
s : (p : GHSpace) → Set p.Rep
hs : ∀ (p : GHSpace), (s p).Finite ∧ univ ⊆ ⋃ x ∈ s p, ball x ε
N : GHSpace → ℕ := fun p ↦ Nat.card ↑(s p)
E : (p : GHSpace) → ↑(s p) ≃ Fin (Nat.card ↑(s p)) := fun p ↦ Finite.equivFin ↑(s p)
F : GHSpace → (n : ℕ) × (Fin n → Fin n → ℤ) := fun p ↦ ⟨N p, fun a b ↦ ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋⟩
p q : GHSpace
hpq : F p = F q
Npq : N p = N q
Ψ : ↑(s p) → ↑(s q) := fun x ↦ (E q).symm (Fin.cast Npq ((E p) x))
⊢ dist p q ≤ δ

Tactic:
let Φ : s p → q.Rep := fun x => Ψ x

Goal state after:
δ : ℝ
δpos : δ > 0
ε : ℝ := 2 / 5 * δ
εpos : 0 < ε
s : (p : GHSpace) → Set p.Rep
hs : ∀ (p : GHSpace), (s p).Finite ∧ univ ⊆ ⋃ x ∈ s p, ball x ε
N : GHSpace → ℕ := fun p ↦ Nat.card ↑(s p)
E : (p : GHSpace) → ↑(s p) ≃ Fin (Nat.card ↑(s p)) := fun p ↦ Finite.equivFin ↑(s p)
F : GHSpace → (n : ℕ) × (Fin n → Fin n → ℤ) := fun p ↦ ⟨N p, fun a b ↦ ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋⟩
p q : GHSpace
hpq : F p = F q
Npq : N p = N q
Ψ : ↑(s p) → ↑(s q) := fun x ↦ (E q).symm (Fin.cast Npq ((E p) x))
Φ : ↑(s p) → q.Rep := fun x ↦ ↑(Ψ x)
⊢ dist p q ≤ δ
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: case h
δ : ℝ
δpos : δ > 0
ε : ℝ := 2 / 5 * δ
εpos : 0 < ε
s : (p : GHSpace) → Set p.Rep
hs : ∀ (p : GHSpace), (s p).Finite ∧ univ ⊆ ⋃ x ∈ s p, ball x ε
N : GHSpace → ℕ := fun p ↦ Nat.card ↑(s p)
E : (p : GHSpace) → ↑(s p) ≃ Fin (Nat.card ↑(s p)) := fun p ↦ Finite.equivFin ↑(s p)
F : GHSpace → (n : ℕ) × (Fin n → Fin n → ℤ) := fun p ↦ ⟨N p, fun a b ↦ ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋⟩
p q : GHSpace
hpq : F p = F q
Npq : N p = N q
Ψ : ↑(s p) → ↑(s q) := fun x ↦ (E q).symm (Fin.cast Npq ((E p) x))
Φ : ↑(s p) → q.Rep := fun x ↦ ↑(Ψ x)
x : q.Rep
this✝ : x ∈ ⋃ y ∈ s q, ball y ε
y : q.Rep
ys : y ∈ s q
hy : x ∈ ball y ε
i : ℕ := ↑((E q) ⟨y, ys⟩)
hi : ↑((E q) ⟨y, ys⟩) < Nat.card ↑(s q) := Fin.is_lt ((E q) ⟨y, ys⟩)
ihi_eq : ⟨i, hi⟩ = (E q) ⟨y, ys⟩
hiq : i < N q
hip : i < N p
z : ↑(s p) := (E p).symm ⟨i, hip⟩
C1 : (E p) z = ⟨i, hip⟩
C2 : Fin.cast Npq ⟨i, hip⟩ = ⟨i, hi⟩
C3 : (E q).symm ⟨i, hi⟩ = ⟨y, ys⟩
this : Φ z = y
⊢ dist x (Φ z) ≤ ε

Tactic:
rw [this]

Goal state after:
case h
δ : ℝ
δpos : δ > 0
ε : ℝ := 2 / 5 * δ
εpos : 0 < ε
s : (p : GHSpace) → Set p.Rep
hs : ∀ (p : GHSpace), (s p).Finite ∧ univ ⊆ ⋃ x ∈ s p, ball x ε
N : GHSpace → ℕ := fun p ↦ Nat.card ↑(s p)
E : (p : GHSpace) → ↑(s p) ≃ Fin (Nat.card ↑(s p)) := fun p ↦ Finite.equivFin ↑(s p)
F : GHSpace → (n : ℕ) × (Fin n → Fin n → ℤ) := fun p ↦ ⟨N p, fun a b ↦ ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋⟩
p q : GHSpace
hpq : F p = F q
Npq : N p = N q
Ψ : ↑(s p) → ↑(s q) := fun x ↦ (E q).symm (Fin.cast Npq ((E p) x))
Φ : ↑(s p) → q.Rep := fun x ↦ ↑(Ψ x)
x : q.Rep
this✝ : x ∈ ⋃ y ∈ s q, ball y ε
y : q.Rep
ys : y ∈ s q
hy : x ∈ ball y ε
i : ℕ := ↑((E q) ⟨y, ys⟩)
hi : ↑((E q) ⟨y, ys⟩) < Nat.card ↑(s q) := Fin.is_lt ((E q) ⟨y, ys⟩)
ihi_eq : ⟨i, hi⟩ = (E q) ⟨y, ys⟩
hiq : i < N q
hip : i < N p
z : ↑(s p) := (E p).symm ⟨i, hip⟩
C1 : (E p) z = ⟨i, hip⟩
C2 : Fin.cast Npq ⟨i, hip⟩ = ⟨i, hi⟩
C3 : (E q).symm ⟨i, hi⟩ = ⟨y, ys⟩
this : Φ z = y
⊢ dist x y ≤ ε
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: case refine_2
t : Set GHSpace
C : ℝ
u : ℕ → ℝ
K : ℕ → ℕ
ulim : Tendsto u atTop (𝓝 0)
hdiam : ∀ p ∈ t, diam univ ≤ C
hcov : ∀ p ∈ t, ∀ (n : ℕ), ∃ s, #↑s ≤ ↑(K n) ∧ univ ⊆ ⋃ x ∈ s, ball x (u n)
δ : ℝ
δpos : δ > 0
ε : ℝ := 1 / 5 * δ
εpos : 0 < ε
n : ℕ
hn : ∀ n_1 ≥ n, dist (u n_1) 0 < ε
u_le_ε : u n ≤ ε
s : (p : GHSpace) → Set p.Rep
N : GHSpace → ℕ
hN : ∀ (p : GHSpace), N p ≤ K n
E : (p : GHSpace) → ↑(s p) ≃ Fin (N p)
hs : ∀ p ∈ t, univ ⊆ ⋃ x ∈ s p, ball x (u n)
M : ℕ := ⌊ε⁻¹ * max C 0⌋₊
F : GHSpace → (k : Fin (K n).succ) × (Fin ↑k → Fin ↑k → Fin M.succ) :=
  fun p ↦ ⟨⟨N p, ⋯⟩, fun a b ↦ ⟨min M ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋₊, ⋯⟩⟩
p : GHSpace
pt : p ∈ t
q : GHSpace
qt : q ∈ t
hpq : (fun p ↦ F ↑p) ⟨p, pt⟩ = (fun p ↦ F ↑p) ⟨q, qt⟩
Npq : N p = N q
Ψ : ↑(s p) → ↑(s q) := fun x ↦ (E q).symm (Fin.cast Npq ((E p) x))
⊢ dist ↑⟨p, pt⟩ ↑⟨q, qt⟩ < δ

Tactic:
let Φ : s p → q.Rep := fun x => Ψ x

Goal state after:
case refine_2
t : Set GHSpace
C : ℝ
u : ℕ → ℝ
K : ℕ → ℕ
ulim : Tendsto u atTop (𝓝 0)
hdiam : ∀ p ∈ t, diam univ ≤ C
hcov : ∀ p ∈ t, ∀ (n : ℕ), ∃ s, #↑s ≤ ↑(K n) ∧ univ ⊆ ⋃ x ∈ s, ball x (u n)
δ : ℝ
δpos : δ > 0
ε : ℝ := 1 / 5 * δ
εpos : 0 < ε
n : ℕ
hn : ∀ n_1 ≥ n, dist (u n_1) 0 < ε
u_le_ε : u n ≤ ε
s : (p : GHSpace) → Set p.Rep
N : GHSpace → ℕ
hN : ∀ (p : GHSpace), N p ≤ K n
E : (p : GHSpace) → ↑(s p) ≃ Fin (N p)
hs : ∀ p ∈ t, univ ⊆ ⋃ x ∈ s p, ball x (u n)
M : ℕ := ⌊ε⁻¹ * max C 0⌋₊
F : GHSpace → (k : Fin (K n).succ) × (Fin ↑k → Fin ↑k → Fin M.succ) :=
  fun p ↦ ⟨⟨N p, ⋯⟩, fun a b ↦ ⟨min M ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋₊, ⋯⟩⟩
p : GHSpace
pt : p ∈ t
q : GHSpace
qt : q ∈ t
hpq : (fun p ↦ F ↑p) ⟨p, pt⟩ = (fun p ↦ F ↑p) ⟨q, qt⟩
Npq : N p = N q
Ψ : ↑(s p) → ↑(s q) := fun x ↦ (E q).symm (Fin.cast Npq ((E p) x))
Φ : ↑(s p) → q.Rep := fun x ↦ ↑(Ψ x)
⊢ dist ↑⟨p, pt⟩ ↑⟨q, qt⟩ < δ
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: case h
t : Set GHSpace
C : ℝ
u : ℕ → ℝ
K : ℕ → ℕ
ulim : Tendsto u atTop (𝓝 0)
hdiam : ∀ p ∈ t, diam univ ≤ C
hcov : ∀ p ∈ t, ∀ (n : ℕ), ∃ s, #↑s ≤ ↑(K n) ∧ univ ⊆ ⋃ x ∈ s, ball x (u n)
δ : ℝ
δpos : δ > 0
ε : ℝ := 1 / 5 * δ
εpos : 0 < ε
n : ℕ
hn : ∀ n_1 ≥ n, dist (u n_1) 0 < ε
u_le_ε : u n ≤ ε
s : (p : GHSpace) → Set p.Rep
N : GHSpace → ℕ
hN : ∀ (p : GHSpace), N p ≤ K n
E : (p : GHSpace) → ↑(s p) ≃ Fin (N p)
hs : ∀ p ∈ t, univ ⊆ ⋃ x ∈ s p, ball x (u n)
M : ℕ := ⌊ε⁻¹ * max C 0⌋₊
F : GHSpace → (k : Fin (K n).succ) × (Fin ↑k → Fin ↑k → Fin M.succ) :=
  fun p ↦ ⟨⟨N p, ⋯⟩, fun a b ↦ ⟨min M ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋₊, ⋯⟩⟩
p : GHSpace
pt : p ∈ t
q : GHSpace
qt : q ∈ t
hpq : (fun p ↦ F ↑p) ⟨p, pt⟩ = (fun p ↦ F ↑p) ⟨q, qt⟩
Npq : N p = N q
Ψ : ↑(s p) → ↑(s q) := fun x ↦ (E q).symm (Fin.cast Npq ((E p) x))
Φ : ↑(s p) → q.Rep := fun x ↦ ↑(Ψ x)
x : q.Rep
this✝ : x ∈ ⋃ y ∈ s q, ball y (u n)
y : q.Rep
ys : y ∈ s q
hy : x ∈ ball y (u n)
i : ℕ := ↑((E q) ⟨y, ys⟩)
hi : ↑((E q) ⟨y, ys⟩) < N q := ((E q) ⟨y, ys⟩).isLt
ihi_eq : ⟨i, hi⟩ = (E q) ⟨y, ys⟩
hiq : i < N q
hip : i < N p
z : ↑(s p) := (E p).symm ⟨i, hip⟩
C1 : (E p) z = ⟨i, hip⟩
C2 : Fin.cast Npq ⟨i, hip⟩ = ⟨i, hi⟩
C3 : (E q).symm ⟨i, hi⟩ = ⟨y, ys⟩
this : Φ z = y
⊢ dist x (Φ z) ≤ ε

Tactic:
rw [this]

Goal state after:
case h
t : Set GHSpace
C : ℝ
u : ℕ → ℝ
K : ℕ → ℕ
ulim : Tendsto u atTop (𝓝 0)
hdiam : ∀ p ∈ t, diam univ ≤ C
hcov : ∀ p ∈ t, ∀ (n : ℕ), ∃ s, #↑s ≤ ↑(K n) ∧ univ ⊆ ⋃ x ∈ s, ball x (u n)
δ : ℝ
δpos : δ > 0
ε : ℝ := 1 / 5 * δ
εpos : 0 < ε
n : ℕ
hn : ∀ n_1 ≥ n, dist (u n_1) 0 < ε
u_le_ε : u n ≤ ε
s : (p : GHSpace) → Set p.Rep
N : GHSpace → ℕ
hN : ∀ (p : GHSpace), N p ≤ K n
E : (p : GHSpace) → ↑(s p) ≃ Fin (N p)
hs : ∀ p ∈ t, univ ⊆ ⋃ x ∈ s p, ball x (u n)
M : ℕ := ⌊ε⁻¹ * max C 0⌋₊
F : GHSpace → (k : Fin (K n).succ) × (Fin ↑k → Fin ↑k → Fin M.succ) :=
  fun p ↦ ⟨⟨N p, ⋯⟩, fun a b ↦ ⟨min M ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋₊, ⋯⟩⟩
p : GHSpace
pt : p ∈ t
q : GHSpace
qt : q ∈ t
hpq : (fun p ↦ F ↑p) ⟨p, pt⟩ = (fun p ↦ F ↑p) ⟨q, qt⟩
Npq : N p = N q
Ψ : ↑(s p) → ↑(s q) := fun x ↦ (E q).symm (Fin.cast Npq ((E p) x))
Φ : ↑(s p) → q.Rep := fun x ↦ ↑(Ψ x)
x : q.Rep
this✝ : x ∈ ⋃ y ∈ s q, ball y (u n)
y : q.Rep
ys : y ∈ s q
hy : x ∈ ball y (u n)
i : ℕ := ↑((E q) ⟨y, ys⟩)
hi : ↑((E q) ⟨y, ys⟩) < N q := ((E q) ⟨y, ys⟩).isLt
ihi_eq : ⟨i, hi⟩ = (E q) ⟨y, ys⟩
hiq : i < N q
hip : i < N p
z : ↑(s p) := (E p).symm ⟨i, hip⟩
C1 : (E p) z = ⟨i, hip⟩
C2 : Fin.cast Npq ⟨i, hip⟩ = ⟨i, hi⟩
C3 : (E q).symm ⟨i, hi⟩ = ⟨y, ys⟩
this : Φ z = y
⊢ dist x y ≤ ε
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: case refine_3
t : Set GHSpace
C : ℝ
u : ℕ → ℝ
K : ℕ → ℕ
ulim : Tendsto u atTop (𝓝 0)
hdiam : ∀ p ∈ t, diam univ ≤ C
hcov : ∀ p ∈ t, ∀ (n : ℕ), ∃ s, #↑s ≤ ↑(K n) ∧ univ ⊆ ⋃ x ∈ s, ball x (u n)
δ : ℝ
δpos : δ > 0
ε : ℝ := 1 / 5 * δ
εpos : 0 < ε
n : ℕ
hn : ∀ n_1 ≥ n, dist (u n_1) 0 < ε
u_le_ε : u n ≤ ε
s : (p : GHSpace) → Set p.Rep
N : GHSpace → ℕ
hN : ∀ (p : GHSpace), N p ≤ K n
E : (p : GHSpace) → ↑(s p) ≃ Fin (N p)
hs : ∀ p ∈ t, univ ⊆ ⋃ x ∈ s p, ball x (u n)
M : ℕ := ⌊ε⁻¹ * max C 0⌋₊
F : GHSpace → (k : Fin (K n).succ) × (Fin ↑k → Fin ↑k → Fin M.succ) :=
  fun p ↦ ⟨⟨N p, ⋯⟩, fun a b ↦ ⟨min M ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋₊, ⋯⟩⟩
p : GHSpace
pt : p ∈ t
q : GHSpace
qt : q ∈ t
hpq : (fun p ↦ F ↑p) ⟨p, pt⟩ = (fun p ↦ F ↑p) ⟨q, qt⟩
Npq : N p = N q
Ψ : ↑(s p) → ↑(s q) := fun x ↦ (E q).symm (Fin.cast Npq ((E p) x))
Φ : ↑(s p) → q.Rep := fun x ↦ ↑(Ψ x)
x y : ↑(s p)
this : dist (Φ x) (Φ y) = dist (Ψ x) (Ψ y)
⊢ |dist x y - dist (Φ x) (Φ y)| ≤ ε

Tactic:
rw [this]

Goal state after:
case refine_3
t : Set GHSpace
C : ℝ
u : ℕ → ℝ
K : ℕ → ℕ
ulim : Tendsto u atTop (𝓝 0)
hdiam : ∀ p ∈ t, diam univ ≤ C
hcov : ∀ p ∈ t, ∀ (n : ℕ), ∃ s, #↑s ≤ ↑(K n) ∧ univ ⊆ ⋃ x ∈ s, ball x (u n)
δ : ℝ
δpos : δ > 0
ε : ℝ := 1 / 5 * δ
εpos : 0 < ε
n : ℕ
hn : ∀ n_1 ≥ n, dist (u n_1) 0 < ε
u_le_ε : u n ≤ ε
s : (p : GHSpace) → Set p.Rep
N : GHSpace → ℕ
hN : ∀ (p : GHSpace), N p ≤ K n
E : (p : GHSpace) → ↑(s p) ≃ Fin (N p)
hs : ∀ p ∈ t, univ ⊆ ⋃ x ∈ s p, ball x (u n)
M : ℕ := ⌊ε⁻¹ * max C 0⌋₊
F : GHSpace → (k : Fin (K n).succ) × (Fin ↑k → Fin ↑k → Fin M.succ) :=
  fun p ↦ ⟨⟨N p, ⋯⟩, fun a b ↦ ⟨min M ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋₊, ⋯⟩⟩
p : GHSpace
pt : p ∈ t
q : GHSpace
qt : q ∈ t
hpq : (fun p ↦ F ↑p) ⟨p, pt⟩ = (fun p ↦ F ↑p) ⟨q, qt⟩
Npq : N p = N q
Ψ : ↑(s p) → ↑(s q) := fun x ↦ (E q).symm (Fin.cast Npq ((E p) x))
Φ : ↑(s p) → q.Rep := fun x ↦ ↑(Ψ x)
x y : ↑(s p)
this : dist (Φ x) (Φ y) = dist (Ψ x) (Ψ y)
⊢ |dist x y - dist (Ψ x) (Ψ y)| ≤ ε
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: X : Type u
Y : Type v
inst✝³ : MetricSpace X
inst✝² : MetricSpace Y
inst✝¹ : Nonempty X
inst✝ : Nonempty Y
f g : Cb X Y
⊢ ⨆ y, ⨅ x, f (inl x, inr y) ≤ (⨆ y, ⨅ x, g (inl x, inr y)) + dist f g

Tactic:
obtain ⟨cg, hcg⟩ := g.isBounded_range.bddBelow
  have Hcg : ∀ x, cg ≤ g x := fun x => hcg (mem_range_self x)
  obtain ⟨cf, hcf⟩ := f.isBounded_range.bddBelow
  have Hcf : ∀ x, cf ≤ f x := fun x => hcf (mem_range_self x)
  -- prove the inequality but with `dist f g` inside, by using inequalities comparing
  -- iSup to iSup and iInf to iInf
  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
  -- move the `dist f g` out of the infimum and the supremum, arguing that continuous monotone maps
  -- (here the addition of `dist f g`) preserve infimum and supremum
  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 _⟩
  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
  -- deduce the result from the above two steps
  simpa [E2, E1]

Goal state after:
Module: Mathlib.Topology.Subpath

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ t₂ x✝ : ↑I
⊢ ((γ.subpath t₀ (Icc.convexComb t₁ t₂ (0, x✝).1)).trans (γ.subpath (Icc.convexComb t₁ t₂ (0, x✝).1) t₂)) (0, x✝).2 =
    ((γ.subpath t₀ t₁).trans (γ.subpath t₁ t₂)).toContinuousMap x✝

Tactic:
by rw [Icc.convexComb_zero, coe_toContinuousMap]

Goal state after:
Module: Mathlib.Topology.Subpath

Goal state before:
pp: case succ
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
n✝ n : ℕ
ih :
  (p : Fin (n + 1) → X) →
    (F G : (k : Fin n) → Path (p k.castSucc) (p k.succ)) →
      ((k : Fin n) → (F k).Homotopy (G k)) → (concat p F).Homotopy (concat p G)
p : Fin (n + 1 + 1) → X
F G : (k : Fin (n + 1)) → Path (p k.castSucc) (p k.succ)
H : (k : Fin (n + 1)) → (F k).Homotopy (G k)
⊢ (concat p F).Homotopy (concat p G)

Tactic:
rw [concat_succ, concat_succ]

Goal state after:
case succ
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
n✝ n : ℕ
ih :
  (p : Fin (n + 1) → X) →
    (F G : (k : Fin n) → Path (p k.castSucc) (p k.succ)) →
      ((k : Fin n) → (F k).Homotopy (G k)) → (concat p F).Homotopy (concat p G)
p : Fin (n + 1 + 1) → X
F G : (k : Fin (n + 1)) → Path (p k.castSucc) (p k.succ)
H : (k : Fin (n + 1)) → (F k).Homotopy (G k)
⊢ ((concat (p ∘ castSucc) fun k ↦ F k.castSucc).trans (F (last n))).Homotopy
    ((concat (p ∘ castSucc) fun k ↦ G k.castSucc).trans (G (last n)))