9.5. Slices are Bi-Lipschitz Homeomorphisms🔗

Fix (t,p) and let g(x) := u(t,p,x), an L_g-Lipschitz map X \to P. The time-t slice of the homotopy is \Phi(x) \;:=\; f\bigl(g(x), x\bigr) \;=\; \mathrm{slice}(g(x))(x).

Proposition 9.5.1🔗

Proposition 9.5.1. Since L^2 L_g < 1 (and L > 0), the map \Phi is a homeomorphism X \to T; moreover \Phi is L(1 + L_g)-Lipschitz and \Phi^{-1} is \bigl(L / (1 - L^2 L_g)\bigr)-Lipschitz.

Proof. Upper bound. For x, y: d(\Phi x, \Phi y) \le d\bigl(\mathrm{slice}(g x)(x), \mathrm{slice}(g x)(y)\bigr) + d\bigl(\mathrm{slice}(g x)(y), \mathrm{slice}(g y)(y)\bigr) \le L\,d(x,y) + L\,\|g x - g y\| \le L(1 + L_g)\,d(x,y).

In particular \Phi is continuous.

Lower bound. Since \mathrm{slice}(gy)^{-1} is L-Lipschitz, d(\mathrm{slice}(gy)(x), \mathrm{slice}(gy)(y)) \ge \tfrac1L d(x,y). Hence d(\Phi x, \Phi y) \;\ge\; d\bigl(\mathrm{slice}(g y)(x), \mathrm{slice}(g y)(y)\bigr) - d\bigl(\mathrm{slice}(g x)(x), \mathrm{slice}(g y)(x)\bigr) \;\ge\; \Bigl(\tfrac1L - L\,L_g\Bigr)\, d(x,y),

and \tfrac1L - L L_g = \tfrac{1 - L^2 L_g}{L} > 0. In particular \Phi is injective.

Surjectivity (Banach fixed point). We may assume X \ne \emptyset (the empty case was dispatched in 9.1). Fix a target \tau \in T and consider \Psi(x) := \mathrm{slice}(g(x))^{-1}(\tau), a self-map of X. It is a contraction: d(\Psi x, \Psi y) = d\bigl(\mathrm{slice}(gx)^{-1}\tau,\, \mathrm{slice}(gy)^{-1}\tau\bigr) \le L\, d\bigl(\tau,\, \mathrm{slice}(gx)\bigl(\mathrm{slice}(gy)^{-1} \tau\bigr)\bigr)

(rewrite \tau = \mathrm{slice}(gy)\bigl(\mathrm{slice}(gy)^{-1}\tau\bigr) and apply the L-Lipschitz map \mathrm{slice}(gx)^{-1}), and the remaining distance is d(\mathrm{slice}(gy)(z), \mathrm{slice}(gx)(z)) at the point z := \mathrm{slice}(gy)^{-1}\tau, which is \le L\,\|gx - gy\| \le L\,L_g\,d(x,y). Altogether d(\Psi x, \Psi y) \le L^2 L_g\, d(x,y) with L^2 L_g < 1. The compact metric space X is complete, so \Psi has a fixed point x^\ast: \mathrm{slice}(g(x^\ast))^{-1}(\tau) = x^\ast, i.e. \Phi(x^\ast) = \tau.

So \Phi is a continuous bijection from a compact space to a Hausdorff (metric) space, hence a homeomorphism. The Lipschitz bound for \Phi^{-1} follows from the lower bound: d(\Phi^{-1}a, \Phi^{-1}b) \le \tfrac{L}{1 - L^2 L_g}\, d(a,b). \blacksquare

Setting L' \;:=\; L(1 + L_g) \;+\; \frac{L}{1 - L^2 L_g}, a single constant independent of (t,p), every slice \mathrm{Slice}(t,p) := \Phi (for the parameters (t,p)) and its inverse is L'-Lipschitz. Together with the properties of u from 9.4 and the reduction 9.1, this proves Theorem B. \blacksquare

In Lean, surjectivity via the Banach fixed point and the assembled slice homeomorphism are:

open scoped NNReal Topology

namespace Submission
namespace FamiliesOfMapsB01

variable {X T P : Type*} [MetricSpace X] [MetricSpace T] [PseudoMetricSpace P]

/-
**Surjectivity of the perturbed slice** via the Banach fixed-point theorem.
-/
lemma slice_surjective
    [CompleteSpace X] [Nonempty X]
    (slc : P → (X ≃ₜ T)) (L Lg : ℝ≥0)
    (hslcInv : ∀ p, LipschitzWith L (slc p).symm)
    (hjoint : ∀ (x : X) (p p' : P), dist (slc p x) (slc p' x) ≤ (L : ℝ) * dist p p')
    (g : X → P) (hg : LipschitzWith Lg g)
    (hsmall : (L : ℝ) * L * Lg < 1) :
    Function.Surjective (fun x => slc (g x) x) := byX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompleteSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1⊢ Function.Surjective fun x => (slc (g x)) x
  intro τX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompleteSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1τ:T⊢ ∃ a, (fun x => (slc (g x)) x) a = τ
  set Ψ : X → X := fun x => (slc (g x)).symm τX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompleteSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1τ:TΨ:X → X := fun x => (slc (g x)).symm τ⊢ ∃ a, (fun x => (slc (g x)) x) a = τ;
  have h_fixed_point : ∃ x, Ψ x = x := byX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompleteSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1⊢ Function.Surjective fun x => (slc (g x)) x
    have h_contractive : ContractingWith (L * L * Lg) Ψ := byX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompleteSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1⊢ Function.Surjective fun x => (slc (g x)) x
      refine' ⟨ hsmall, _ ⟩X:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompleteSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1τ:TΨ:X → X := fun x => (slc (g x)).symm τ⊢ LipschitzWith (L * L * Lg) Ψ;
      rw [ lipschitzWith_iff_dist_le_mul ] at *X:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompleteSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:∀ (x y : X), dist (g x) (g y) ≤ ↑Lg * dist x yhsmall:↑L * ↑L * ↑Lg < 1τ:TΨ:X → X := fun x => (slc (g x)).symm τ⊢ ∀ (x y : X), dist (Ψ x) (Ψ y) ≤ ↑(L * L * Lg) * dist x y;
      intro x yX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompleteSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:∀ (x y : X), dist (g x) (g y) ≤ ↑Lg * dist x yhsmall:↑L * ↑L * ↑Lg < 1τ:TΨ:X → X := fun x => (slc (g x)).symm τx:Xy:X⊢ dist (Ψ x) (Ψ y) ≤ ↑(L * L * Lg) * dist x y
      have h_dist : dist ((slc (g y)).symm τ) ((slc (g x)).symm τ) ≤ L * dist ((slc (g y)) ((slc (g y)).symm τ)) ((slc (g x)) ((slc (g y)).symm τ)) := byX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompleteSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1⊢ Function.Surjective fun x => (slc (g x)) x
        convert hslcInv ( g x ) |> fun h => h.dist_le_mul _ _ using 1h.e'_3X:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompleteSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:∀ (x y : X), dist (g x) (g y) ≤ ↑Lg * dist x yhsmall:↑L * ↑L * ↑Lg < 1τ:TΨ:X → X := fun x => (slc (g x)).symm τx:Xy:X⊢ dist ((slc (g y)).symm τ) ((slc (g x)).symm τ) =
  dist ((slc (g x)).symm ((slc (g y)) ((slc (g y)).symm τ))) ((slc (g x)).symm ((slc (g x)) ((slc (g y)).symm τ)));
        simp +decide [ dist_comm ]All goals completed! 🐙;
      rw [ dist_comm ] at h_distX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompleteSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:∀ (x y : X), dist (g x) (g y) ≤ ↑Lg * dist x yhsmall:↑L * ↑L * ↑Lg < 1τ:TΨ:X → X := fun x => (slc (g x)).symm τx:Xy:Xh_dist:dist ((slc (g x)).symm τ) ((slc (g y)).symm τ) ≤
  ↑L * dist ((slc (g y)) ((slc (g y)).symm τ)) ((slc (g x)) ((slc (g y)).symm τ))⊢ dist (Ψ x) (Ψ y) ≤ ↑(L * L * Lg) * dist x y;
      refine' le_trans h_dist _X:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompleteSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:∀ (x y : X), dist (g x) (g y) ≤ ↑Lg * dist x yhsmall:↑L * ↑L * ↑Lg < 1τ:TΨ:X → X := fun x => (slc (g x)).symm τx:Xy:Xh_dist:dist ((slc (g x)).symm τ) ((slc (g y)).symm τ) ≤
  ↑L * dist ((slc (g y)) ((slc (g y)).symm τ)) ((slc (g x)) ((slc (g y)).symm τ))⊢ ↑L * dist ((slc (g y)) ((slc (g y)).symm τ)) ((slc (g x)) ((slc (g y)).symm τ)) ≤ ↑(L * L * Lg) * dist x y;
      refine' le_trans ( mul_le_mul_of_nonneg_left ( hjoint _ _ _ ) ( NNReal.coe_nonneg _ ) ) _X:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompleteSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:∀ (x y : X), dist (g x) (g y) ≤ ↑Lg * dist x yhsmall:↑L * ↑L * ↑Lg < 1τ:TΨ:X → X := fun x => (slc (g x)).symm τx:Xy:Xh_dist:dist ((slc (g x)).symm τ) ((slc (g y)).symm τ) ≤
  ↑L * dist ((slc (g y)) ((slc (g y)).symm τ)) ((slc (g x)) ((slc (g y)).symm τ))⊢ ↑L * (↑L * dist (g y) (g x)) ≤ ↑(L * L * Lg) * dist x y;
      simpa [ mul_assoc, dist_comm ] using mul_le_mul_of_nonneg_left ( hg y x ) ( byX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompleteSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:∀ (x y : X), dist (g x) (g y) ≤ ↑Lg * dist x yhsmall:↑L * ↑L * ↑Lg < 1τ:TΨ:X → X := fun x => (slc (g x)).symm τx:Xy:Xh_dist:dist ((slc (g x)).symm τ) ((slc (g y)).symm τ) ≤
  ↑L * dist ((slc (g y)) ((slc (g y)).symm τ)) ((slc (g x)) ((slc (g y)).symm τ))⊢ 0 ≤ ↑L * ↑L positivityAll goals completed! 🐙 : ( 0 : ℝ ) ≤ L * L );
    have := h_contractive.fixedPoint_isFixedPtX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompleteSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1τ:TΨ:X → X := fun x => (slc (g x)).symm τh_contractive:ContractingWith (L * L * Lg) Ψthis:Function.IsFixedPt Ψ (ContractingWith.fixedPoint Ψ h_contractive)⊢ ∃ x, Ψ x = x; aesopAll goals completed! 🐙;
  grind +suggestionsAll goals completed! 🐙

/-
**The perturbed slice is a bi-Lipschitz homeomorphism.**
-/
lemma exists_slice_homeo
    [CompactSpace X] [Nonempty X]
    (slc : P → (X ≃ₜ T)) (L Lg : ℝ≥0)
    (hslcLip : ∀ p, LipschitzWith L (slc p))
    (hslcInv : ∀ p, LipschitzWith L (slc p).symm)
    (hjoint : ∀ (x : X) (p p' : P), dist (slc p x) (slc p' x) ≤ (L : ℝ) * dist p p')
    (g : X → P) (hg : LipschitzWith Lg g)
    (hsmall : (L : ℝ) * L * Lg < 1)
    (L' : ℝ≥0)
    (hL'lip : (L : ℝ) * (1 + Lg) ≤ L')
    (hL'inv : (L : ℝ) ≤ L' * (1 - (L : ℝ) * L * Lg)) :
    ∃ Φ : X ≃ₜ T, (∀ x, Φ x = slc (g x) x) ∧
      LipschitzWith L' (Φ : X → T) ∧ LipschitzWith L' (Φ.symm : T → X) := byX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)⊢ ∃ Φ, (∀ (x : X), Φ x = (slc (g x)) x) ∧ LipschitzWith L' ⇑Φ ∧ LipschitzWith L' ⇑Φ.symm
  -- Let `Φ₀ : X → T := fun x => slc (g x) x`. We need to show that `Φ₀` is a bi-Lipschitz homeomorphism.
  obtain ⟨Φ₀, hΦ₀⟩ : ∃ (Φ₀ : X ≃ₜ T), (∀ x, Φ₀ x = (slc (g x)) x) := byX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)⊢ ∃ Φ₀, ∀ (x : X), Φ₀ x = (slc (g x)) x
    have h_cont : Continuous (fun x => (slc (g x)) x) := byX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)⊢ ∃ Φ₀, ∀ (x : X), Φ₀ x = (slc (g x)) x
      refine' continuous_iff_continuousAt.2 fun x => _X:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)x:X⊢ ContinuousAt (fun x => (slc (g x)) x) x;
      refine' tendsto_iff_dist_tendsto_zero.mpr _X:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)x:X⊢ Filter.Tendsto (fun b => dist ((slc (g b)) b) ((fun x => (slc (g x)) x) x)) (𝓝 x) (𝓝 0);
      -- By the properties of the Lipschitz functions and the continuity of $g$, we can bound the distance.
      have h_bound : ∀ b, dist ((slc (g b)) b) ((slc (g x)) x) ≤ L * dist b x + L * Lg * dist b x := byX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)⊢ ∃ Φ₀, ∀ (x : X), Φ₀ x = (slc (g x)) x
        intro bX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)x:Xb:X⊢ dist ((slc (g b)) b) ((slc (g x)) x) ≤ ↑L * dist b x + ↑L * ↑Lg * dist b x
        have h_bound : dist ((slc (g b)) b) ((slc (g x)) x) ≤ dist ((slc (g b)) b) ((slc (g b)) x) + dist ((slc (g b)) x) ((slc (g x)) x) := byX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)⊢ ∃ Φ₀, ∀ (x : X), Φ₀ x = (slc (g x)) x
          exact dist_triangle _ _ _All goals completed! 🐙;
        exact h_bound.trans ( add_le_add ( hslcLip _ |> LipschitzWith.dist_le_mul |> fun h => h _ _ ) ( hjoint _ _ _ |> le_trans <| mul_le_mul_of_nonneg_left ( hg.dist_le_mul _ _ ) <| byX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)x:Xb:Xh_bound:dist ((slc (g b)) b) ((slc (g x)) x) ≤ dist ((slc (g b)) b) ((slc (g b)) x) + dist ((slc (g b)) x) ((slc (g x)) x)⊢ 0 ≤ ↑L positivityAll goals completed! 🐙 ) ) |> le_trans <| byX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)x:Xb:Xh_bound:dist ((slc (g b)) b) ((slc (g x)) x) ≤ dist ((slc (g b)) b) ((slc (g b)) x) + dist ((slc (g b)) x) ((slc (g x)) x)⊢ ↑L * dist b x + ↑L * (↑Lg * dist b x) ≤ ↑L * dist b x + ↑L * ↑Lg * dist b x simp +decide [ mul_assoc, mul_comm, mul_left_comm ]All goals completed! 🐙 ;
      exact squeeze_zero ( fun _ => dist_nonneg ) h_bound ( Continuous.tendsto' ( byX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)x:Xh_bound:∀ (b : X), dist ((slc (g b)) b) ((slc (g x)) x) ≤ ↑L * dist b x + ↑L * ↑Lg * dist b x⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun t => ↑L * dist t x + ↑L * ↑Lg * dist t x continuityAll goals completed! 🐙 ) _ _ ( byX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)x:Xh_bound:∀ (b : X), dist ((slc (g b)) b) ((slc (g x)) x) ≤ ↑L * dist b x + ↑L * ↑Lg * dist b x⊢ ↑L * dist x x + ↑L * ↑Lg * dist x x = 0 simp +decideAll goals completed! 🐙 ) );
    have h_inj : Function.Injective (fun x => (slc (g x)) x) := byX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)⊢ ∃ Φ₀, ∀ (x : X), Φ₀ x = (slc (g x)) x
      have h_lower_bound : ∀ x y : X, dist ((slc (g x)) x) ((slc (g y)) y) ≥ ((1 / L : ℝ) - L * Lg) * dist x y := byX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)⊢ ∃ Φ₀, ∀ (x : X), Φ₀ x = (slc (g x)) x
        intro x yX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)h_cont:Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  fun x => (slc (g x)) xx:Xy:X⊢ dist ((slc (g x)) x) ((slc (g y)) y) ≥ (1 / ↑L - ↑L * ↑Lg) * dist x y
        have h_lower_bound_step : dist ((slc (g y)) x) ((slc (g y)) y) ≥ (1 / L : ℝ) * dist x y := byX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)⊢ ∃ Φ₀, ∀ (x : X), Φ₀ x = (slc (g x)) x
          have := hslcInv ( g y )X:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)h_cont:Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  fun x => (slc (g x)) xx:Xy:Xthis:LipschitzWith L ⇑(slc (g y)).symm⊢ dist ((slc (g y)) x) ((slc (g y)) y) ≥ 1 / ↑L * dist x y;
          have := this.dist_le_mul ( ( slc ( g y ) ) x ) ( ( slc ( g y ) ) y )X:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)h_cont:Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  fun x => (slc (g x)) xx:Xy:Xthis✝:LipschitzWith L ⇑(slc (g y)).symmthis:dist ((slc (g y)).symm ((slc (g y)) x)) ((slc (g y)).symm ((slc (g y)) y)) ≤ ↑L * dist ((slc (g y)) x) ((slc (g y)) y)⊢ dist ((slc (g y)) x) ((slc (g y)) y) ≥ 1 / ↑L * dist x y ; simp_all +decideX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)h_cont:Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  fun x => (slc (g x)) xx:Xy:Xthis:dist x y ≤ ↑L * dist ((slc (g y)) x) ((slc (g y)) y)⊢ (↑L)⁻¹ * dist x y ≤ dist ((slc (g y)) x) ((slc (g y)) y) ;
          by_cases hL : L = 0posX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)h_cont:Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  fun x => (slc (g x)) xx:Xy:Xthis:dist x y ≤ ↑L * dist ((slc (g y)) x) ((slc (g y)) y)hL:L = 0⊢ (↑L)⁻¹ * dist x y ≤ dist ((slc (g y)) x) ((slc (g y)) y)negX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)h_cont:Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  fun x => (slc (g x)) xx:Xy:Xthis:dist x y ≤ ↑L * dist ((slc (g y)) x) ((slc (g y)) y)hL:¬L = 0⊢ (↑L)⁻¹ * dist x y ≤ dist ((slc (g y)) x) ((slc (g y)) y) <;>posX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)h_cont:Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  fun x => (slc (g x)) xx:Xy:Xthis:dist x y ≤ ↑L * dist ((slc (g y)) x) ((slc (g y)) y)hL:L = 0⊢ (↑L)⁻¹ * dist x y ≤ dist ((slc (g y)) x) ((slc (g y)) y)negX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)h_cont:Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  fun x => (slc (g x)) xx:Xy:Xthis:dist x y ≤ ↑L * dist ((slc (g y)) x) ((slc (g y)) y)hL:¬L = 0⊢ (↑L)⁻¹ * dist x y ≤ dist ((slc (g y)) x) ((slc (g y)) y) simp_all +decide [ mul_comm ]negX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmg:X → PL':ℝ≥0x:Xy:Xhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ dist p p' * ↑Lhg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)h_cont:Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  fun x => (slc (g x)) xthis:dist x y ≤ ↑L * dist ((slc (g y)) x) ((slc (g y)) y)hL:¬L = 0⊢ dist x y * (↑L)⁻¹ ≤ dist ((slc (g y)) x) ((slc (g y)) y);
          rwa [ ← div_eq_mul_inv, div_le_iff₀' ( byX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmg:X → PL':ℝ≥0x:Xy:Xhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ dist p p' * ↑Lhg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)h_cont:Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  fun x => (slc (g x)) xthis:dist x y ≤ ↑L * dist ((slc (g y)) x) ((slc (g y)) y)hL:¬L = 0⊢ 0 < ↑L positivityAll goals completed! 🐙 ) ]negX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmg:X → PL':ℝ≥0x:Xy:Xhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ dist p p' * ↑Lhg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)h_cont:Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  fun x => (slc (g x)) xthis:dist x y ≤ ↑L * dist ((slc (g y)) x) ((slc (g y)) y)hL:¬L = 0⊢ dist x y ≤ ↑L * dist ((slc (g y)) x) ((slc (g y)) y);
        have h_lower_bound_step2 : dist ((slc (g x)) x) ((slc (g y)) x) ≤ L * Lg * dist x y := byX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)⊢ ∃ Φ₀, ∀ (x : X), Φ₀ x = (slc (g x)) x
          exact le_trans ( hjoint x _ _ ) ( byX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)h_cont:Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  fun x => (slc (g x)) xx:Xy:Xh_lower_bound_step:dist ((slc (g y)) x) ((slc (g y)) y) ≥ 1 / ↑L * dist x y⊢ ↑L * dist (g x) (g y) ≤ ↑L * ↑Lg * dist x y simpa [ mul_assoc ] using mul_le_mul_of_nonneg_left ( hg.dist_le_mul x y ) ( NNReal.coe_nonneg L )All goals completed! 🐙 );
        linarith [ dist_triangle_left ( ( slc ( g y ) ) x ) ( ( slc ( g y ) ) y ) ( ( slc ( g x ) ) x ) ]All goals completed! 🐙;
      intro x yX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)h_cont:Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  fun x => (slc (g x)) xh_lower_bound:∀ (x y : X), dist ((slc (g x)) x) ((slc (g y)) y) ≥ (1 / ↑L - ↑L * ↑Lg) * dist x yx:Xy:X⊢ (fun x => (slc (g x)) x) x = (fun x => (slc (g x)) x) y → x = y hxyX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)h_cont:Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  fun x => (slc (g x)) xh_lower_bound:∀ (x y : X), dist ((slc (g x)) x) ((slc (g y)) y) ≥ (1 / ↑L - ↑L * ↑Lg) * dist x yx:Xy:Xhxy:(fun x => (slc (g x)) x) x = (fun x => (slc (g x)) x) y⊢ x = y
      have h_dist : dist x y = 0 := byX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)⊢ ∃ Φ₀, ∀ (x : X), Φ₀ x = (slc (g x)) x
        by_cases hL : L = 0posX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)h_cont:Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  fun x => (slc (g x)) xh_lower_bound:∀ (x y : X), dist ((slc (g x)) x) ((slc (g y)) y) ≥ (1 / ↑L - ↑L * ↑Lg) * dist x yx:Xy:Xhxy:(fun x => (slc (g x)) x) x = (fun x => (slc (g x)) x) yhL:L = 0⊢ dist x y = 0negX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)h_cont:Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  fun x => (slc (g x)) xh_lower_bound:∀ (x y : X), dist ((slc (g x)) x) ((slc (g y)) y) ≥ (1 / ↑L - ↑L * ↑Lg) * dist x yx:Xy:Xhxy:(fun x => (slc (g x)) x) x = (fun x => (slc (g x)) x) yhL:¬L = 0⊢ dist x y = 0 <;>posX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)h_cont:Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  fun x => (slc (g x)) xh_lower_bound:∀ (x y : X), dist ((slc (g x)) x) ((slc (g y)) y) ≥ (1 / ↑L - ↑L * ↑Lg) * dist x yx:Xy:Xhxy:(fun x => (slc (g x)) x) x = (fun x => (slc (g x)) x) yhL:L = 0⊢ dist x y = 0negX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)h_cont:Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  fun x => (slc (g x)) xh_lower_bound:∀ (x y : X), dist ((slc (g x)) x) ((slc (g y)) y) ≥ (1 / ↑L - ↑L * ↑Lg) * dist x yx:Xy:Xhxy:(fun x => (slc (g x)) x) x = (fun x => (slc (g x)) x) yhL:¬L = 0⊢ dist x y = 0 simp_all +decide [ div_eq_mul_inv ]negX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)h_cont:Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  fun x => (slc (g x)) xx:Xy:Xh_lower_bound:∀ (x y : X), ((↑L)⁻¹ - ↑L * ↑Lg) * dist x y ≤ dist ((slc (g x)) x) ((slc (g y)) y)hxy:(slc (g x)) x = (slc (g y)) yhL:¬L = 0⊢ x = y;
        ·posX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0g:X → PL':ℝ≥0x:Xy:XhslcLip:∀ (p : P) (x y : X), x = yhslcInv:∀ (p : P) (x y : T), x = yhjoint:∀ (x : X) (p p' : P), (slc p) x = (slc p') xhg:LipschitzWith Lg gh_cont:Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  fun x => (slc (g x)) xhxy:(slc (g x)) x = (slc (g y)) yhL:L = 0⊢ x = y exact hslcLip ( g x ) x yAll goals completed! 🐙;
        ·negX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)h_cont:Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  fun x => (slc (g x)) xx:Xy:Xh_lower_bound:∀ (x y : X), ((↑L)⁻¹ - ↑L * ↑Lg) * dist x y ≤ dist ((slc (g x)) x) ((slc (g y)) y)hxy:(slc (g x)) x = (slc (g y)) yhL:¬L = 0⊢ x = y contrapose! h_lower_boundnegX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)h_cont:Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  fun x => (slc (g x)) xx:Xy:Xhxy:(slc (g x)) x = (slc (g y)) yhL:¬L = 0h_lower_bound:x ≠ y⊢ ∃ x y, dist ((slc (g x)) x) ((slc (g y)) y) < ((↑L)⁻¹ - ↑L * ↑Lg) * dist x y;
          refine' ⟨ x, y, _ ⟩negX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)h_cont:Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  fun x => (slc (g x)) xx:Xy:Xhxy:(slc (g x)) x = (slc (g y)) yhL:¬L = 0h_lower_bound:x ≠ y⊢ dist ((slc (g x)) x) ((slc (g y)) y) < ((↑L)⁻¹ - ↑L * ↑Lg) * dist x y ; simp_all +decidenegX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)h_cont:Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  fun x => (slc (g x)) xx:Xy:Xhxy:(slc (g x)) x = (slc (g y)) yhL:¬L = 0h_lower_bound:¬x = y⊢ ↑L * ↑Lg < (↑L)⁻¹;
          rw [ inv_eq_one_div, lt_div_iff₀ ]negX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)h_cont:Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  fun x => (slc (g x)) xx:Xy:Xhxy:(slc (g x)) x = (slc (g y)) yhL:¬L = 0h_lower_bound:¬x = y⊢ ↑L * ↑Lg * ↑L < 1negX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)h_cont:Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  fun x => (slc (g x)) xx:Xy:Xhxy:(slc (g x)) x = (slc (g y)) yhL:¬L = 0h_lower_bound:¬x = y⊢ 0 < ↑L <;>negX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)h_cont:Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  fun x => (slc (g x)) xx:Xy:Xhxy:(slc (g x)) x = (slc (g y)) yhL:¬L = 0h_lower_bound:¬x = y⊢ ↑L * ↑Lg * ↑L < 1negX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)h_cont:Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  fun x => (slc (g x)) xx:Xy:Xhxy:(slc (g x)) x = (slc (g y)) yhL:¬L = 0h_lower_bound:¬x = y⊢ 0 < ↑L first | positivityAll goals completed! 🐙 | nlinarith [ show ( L : ℝ ) > 0 from NNReal.coe_pos.mpr ( pos_iff_ne_zero.mpr hL ) ]All goals completed! 🐙 ;
      exact dist_eq_zero.mp h_distAll goals completed! 🐙;
    have h_surj : Function.Surjective (fun x => (slc (g x)) x) := byX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)⊢ ∃ Φ₀, ∀ (x : X), Φ₀ x = (slc (g x)) x
      apply slice_surjective slc L Lg hslcInv hjoint g hg hsmallAll goals completed! 🐙;
    refine' ⟨ _, _ ⟩refine'_1X:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)h_cont:Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  fun x => (slc (g x)) xh_inj:Function.Injective fun x => (slc (g x)) xh_surj:Function.Surjective fun x => (slc (g x)) x⊢ X ≃ₜ Trefine'_2X:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)h_cont:Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  fun x => (slc (g x)) xh_inj:Function.Injective fun x => (slc (g x)) xh_surj:Function.Surjective fun x => (slc (g x)) x⊢ ∀ (x : X), ?refine'_1 x = (slc (g x)) x;
    fapply Homeomorph.mkrefine'_1.toEquivX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)h_cont:Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  fun x => (slc (g x)) xh_inj:Function.Injective fun x => (slc (g x)) xh_surj:Function.Surjective fun x => (slc (g x)) x⊢ X ≃ Trefine'_1.continuous_toFunX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)h_cont:Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  fun x => (slc (g x)) xh_inj:Function.Injective fun x => (slc (g x)) xh_surj:Function.Surjective fun x => (slc (g x)) x⊢ autoParam
  (Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (Equiv.toFun ?refine'_1.toEquiv))
  Homeomorph.continuous_toFun._autoParamrefine'_1.continuous_invFunX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)h_cont:Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  fun x => (slc (g x)) xh_inj:Function.Injective fun x => (slc (g x)) xh_surj:Function.Surjective fun x => (slc (g x)) x⊢ autoParam
  (Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (Equiv.invFun ?refine'_1.toEquiv))
  Homeomorph.continuous_invFun._autoParamrefine'_2X:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)h_cont:Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  fun x => (slc (g x)) xh_inj:Function.Injective fun x => (slc (g x)) xh_surj:Function.Surjective fun x => (slc (g x)) x⊢ ∀ (x : X),
  { toEquiv := ?refine'_1.toEquiv, continuous_toFun := ?refine'_1.continuous_toFun,
        continuous_invFun := ?refine'_1.continuous_invFun }
      x =
    (slc (g x)) x;
    exact Equiv.ofBijective _ ⟨ h_inj, h_surj ⟩refine'_1.continuous_toFunX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)h_cont:Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  fun x => (slc (g x)) xh_inj:Function.Injective fun x => (slc (g x)) xh_surj:Function.Surjective fun x => (slc (g x)) x⊢ autoParam
  (Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (Equiv.ofBijective (fun x => (slc (g x)) x) ⋯).toFun)
  Homeomorph.continuous_toFun._autoParamrefine'_1.continuous_invFunX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)h_cont:Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  fun x => (slc (g x)) xh_inj:Function.Injective fun x => (slc (g x)) xh_surj:Function.Surjective fun x => (slc (g x)) x⊢ autoParam
  (Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (Equiv.ofBijective (fun x => (slc (g x)) x) ⋯).invFun)
  Homeomorph.continuous_invFun._autoParamrefine'_2X:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)h_cont:Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  fun x => (slc (g x)) xh_inj:Function.Injective fun x => (slc (g x)) xh_surj:Function.Surjective fun x => (slc (g x)) x⊢ ∀ (x : X),
  { toEquiv := Equiv.ofBijective (fun x => (slc (g x)) x) ⋯, continuous_toFun := ?refine'_1.continuous_toFun,
        continuous_invFun := ?refine'_1.continuous_invFun }
      x =
    (slc (g x)) x;
    all_goals norm_numAll goals completed! 🐙;
    ·refine'_1.continuous_toFunX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)h_cont:Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  fun x => (slc (g x)) xh_inj:Function.Injective fun x => (slc (g x)) xh_surj:Function.Surjective fun x => (slc (g x)) x⊢ autoParam
  (Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    fun x => (slc (g x)) x)
  Homeomorph.continuous_toFun._autoParam exact h_contAll goals completed! 🐙;
    ·refine'_1.continuous_invFunX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)h_cont:Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  fun x => (slc (g x)) xh_inj:Function.Injective fun x => (slc (g x)) xh_surj:Function.Surjective fun x => (slc (g x)) x⊢ autoParam
  (Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    ⇑(Equiv.ofBijective (fun x => (slc (g x)) x) ⋯).symm)
  Homeomorph.continuous_invFun._autoParam exact Continuous.continuous_symm_of_equiv_compact_to_t2 h_contAll goals completed! 🐙
  refine' ⟨ Φ₀, hΦ₀, _, _ ⟩refine'_1X:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)Φ₀:X ≃ₜ ThΦ₀:∀ (x : X), Φ₀ x = (slc (g x)) x⊢ LipschitzWith L' ⇑Φ₀refine'_2X:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)Φ₀:X ≃ₜ ThΦ₀:∀ (x : X), Φ₀ x = (slc (g x)) x⊢ LipschitzWith L' ⇑Φ₀.symm;
  ·refine'_1X:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)Φ₀:X ≃ₜ ThΦ₀:∀ (x : X), Φ₀ x = (slc (g x)) x⊢ LipschitzWith L' ⇑Φ₀ rw [ lipschitzWith_iff_dist_le_mul ]refine'_1X:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)Φ₀:X ≃ₜ ThΦ₀:∀ (x : X), Φ₀ x = (slc (g x)) x⊢ ∀ (x y : X), dist (Φ₀ x) (Φ₀ y) ≤ ↑L' * dist x y;
    intro x yrefine'_1X:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)Φ₀:X ≃ₜ ThΦ₀:∀ (x : X), Φ₀ x = (slc (g x)) xx:Xy:X⊢ dist (Φ₀ x) (Φ₀ y) ≤ ↑L' * dist x y
    have h_dist : dist (slc (g x) x) (slc (g y) y) ≤ L * dist x y + L * Lg * dist x y := byX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)⊢ ∃ Φ, (∀ (x : X), Φ x = (slc (g x)) x) ∧ LipschitzWith L' ⇑Φ ∧ LipschitzWith L' ⇑Φ.symm
      have h_dist : dist (slc (g x) x) (slc (g y) y) ≤ dist (slc (g x) x) (slc (g x) y) + dist (slc (g x) y) (slc (g y) y) := byX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)⊢ ∃ Φ, (∀ (x : X), Φ x = (slc (g x)) x) ∧ LipschitzWith L' ⇑Φ ∧ LipschitzWith L' ⇑Φ.symm
        exact dist_triangle _ _ _All goals completed! 🐙;
      exact h_dist.trans ( add_le_add ( hslcLip _ |> fun h => h.dist_le_mul _ _ ) ( hjoint _ _ _ |> le_trans <| mul_le_mul_of_nonneg_left ( hg.dist_le_mul _ _ ) <| NNReal.coe_nonneg _ ) ) |> le_trans <| byX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)Φ₀:X ≃ₜ ThΦ₀:∀ (x : X), Φ₀ x = (slc (g x)) xx:Xy:Xh_dist:dist ((slc (g x)) x) ((slc (g y)) y) ≤ dist ((slc (g x)) x) ((slc (g x)) y) + dist ((slc (g x)) y) ((slc (g y)) y)⊢ ↑L * dist x y + ↑L * (↑Lg * dist x y) ≤ ↑L * dist x y + ↑L * ↑Lg * dist x y ring_nfX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)Φ₀:X ≃ₜ ThΦ₀:∀ (x : X), Φ₀ x = (slc (g x)) xx:Xy:Xh_dist:dist ((slc (g x)) x) ((slc (g y)) y) ≤ dist ((slc (g x)) x) ((slc (g x)) y) + dist ((slc (g x)) y) ((slc (g y)) y)⊢ ↑L * dist x y + ↑L * dist x y * ↑Lg ≤ ↑L * dist x y + ↑L * dist x y * ↑Lg; norm_numAll goals completed! 🐙;
    simpa only [ hΦ₀ ] using h_dist.trans ( byX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)Φ₀:X ≃ₜ ThΦ₀:∀ (x : X), Φ₀ x = (slc (g x)) xx:Xy:Xh_dist:dist ((slc (g x)) x) ((slc (g y)) y) ≤ ↑L * dist x y + ↑L * ↑Lg * dist x y⊢ ↑L * dist x y + ↑L * ↑Lg * dist x y ≤ ↑L' * dist x y nlinarith [ @dist_nonneg _ _ x y ]All goals completed! 🐙 );
  ·refine'_2X:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)Φ₀:X ≃ₜ ThΦ₀:∀ (x : X), Φ₀ x = (slc (g x)) x⊢ LipschitzWith L' ⇑Φ₀.symm -- For any `a b : T`, set `x := Φ.symm a`, `y := Φ.symm b` (so `Φ x = a`, `Φ y = b`). The lower bound gives `dist a b ≥ ((1 - L*L*Lg)/L)*dist x y`, hence `dist (Φ.symm a) (Φ.symm b) = dist x y ≤ (L/(1 - L*L*Lg))*dist a b ≤ L'*dist a b` (from `hL'inv` and `1 - L*L*Lg > 0`).
    have h_lower_bound : ∀ x y : X, dist (Φ₀ x) (Φ₀ y) ≥ ((1 - L * L * Lg) / L) * dist x y := byX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)⊢ ∃ Φ, (∀ (x : X), Φ x = (slc (g x)) x) ∧ LipschitzWith L' ⇑Φ ∧ LipschitzWith L' ⇑Φ.symm
      intro x yX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)Φ₀:X ≃ₜ ThΦ₀:∀ (x : X), Φ₀ x = (slc (g x)) xx:Xy:X⊢ dist (Φ₀ x) (Φ₀ y) ≥ (1 - ↑L * ↑L * ↑Lg) / ↑L * dist x y;
      have h_lower_bound : dist (slc (g y) x) (slc (g y) y) ≥ (1 / L : ℝ) * dist x y := byX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)⊢ ∃ Φ, (∀ (x : X), Φ x = (slc (g x)) x) ∧ LipschitzWith L' ⇑Φ ∧ LipschitzWith L' ⇑Φ.symm
        by_cases hL : L = 0posX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)Φ₀:X ≃ₜ ThΦ₀:∀ (x : X), Φ₀ x = (slc (g x)) xx:Xy:XhL:L = 0⊢ dist ((slc (g y)) x) ((slc (g y)) y) ≥ 1 / ↑L * dist x ynegX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)Φ₀:X ≃ₜ ThΦ₀:∀ (x : X), Φ₀ x = (slc (g x)) xx:Xy:XhL:¬L = 0⊢ dist ((slc (g y)) x) ((slc (g y)) y) ≥ 1 / ↑L * dist x y <;>posX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)Φ₀:X ≃ₜ ThΦ₀:∀ (x : X), Φ₀ x = (slc (g x)) xx:Xy:XhL:L = 0⊢ dist ((slc (g y)) x) ((slc (g y)) y) ≥ 1 / ↑L * dist x ynegX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)Φ₀:X ≃ₜ ThΦ₀:∀ (x : X), Φ₀ x = (slc (g x)) xx:Xy:XhL:¬L = 0⊢ dist ((slc (g y)) x) ((slc (g y)) y) ≥ 1 / ↑L * dist x y simp_all +decide [ div_eq_inv_mul ]negX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)Φ₀:X ≃ₜ ThΦ₀:∀ (x : X), Φ₀ x = (slc (g x)) xx:Xy:XhL:¬L = 0⊢ (↑L)⁻¹ * dist x y ≤ dist ((slc (g y)) x) ((slc (g y)) y);
        rw [ inv_mul_le_iff₀ ( by positivity ) ]negX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)Φ₀:X ≃ₜ ThΦ₀:∀ (x : X), Φ₀ x = (slc (g x)) xx:Xy:XhL:¬L = 0⊢ dist x y ≤ ↑L * dist ((slc (g y)) x) ((slc (g y)) y);
        simpa using hslcInv ( g y ) |> fun h => h.dist_le_mul ( slc ( g y ) x ) ( slc ( g y ) y )All goals completed! 🐙;
      have h_lower_bound : dist (slc (g x) x) (slc (g y) x) ≤ L * Lg * dist x y := byX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)⊢ ∃ Φ, (∀ (x : X), Φ x = (slc (g x)) x) ∧ LipschitzWith L' ⇑Φ ∧ LipschitzWith L' ⇑Φ.symm
        exact le_trans ( hjoint x _ _ ) ( byX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)Φ₀:X ≃ₜ ThΦ₀:∀ (x : X), Φ₀ x = (slc (g x)) xx:Xy:Xh_lower_bound:dist ((slc (g y)) x) ((slc (g y)) y) ≥ 1 / ↑L * dist x y⊢ ↑L * dist (g x) (g y) ≤ ↑L * ↑Lg * dist x y simpa [ mul_assoc ] using mul_le_mul_of_nonneg_left ( hg.dist_le_mul x y ) ( NNReal.coe_nonneg L )All goals completed! 🐙 );
      by_cases hL : L = 0posX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)Φ₀:X ≃ₜ ThΦ₀:∀ (x : X), Φ₀ x = (slc (g x)) xx:Xy:Xh_lower_bound✝:dist ((slc (g y)) x) ((slc (g y)) y) ≥ 1 / ↑L * dist x yh_lower_bound:dist ((slc (g x)) x) ((slc (g y)) x) ≤ ↑L * ↑Lg * dist x yhL:L = 0⊢ dist (Φ₀ x) (Φ₀ y) ≥ (1 - ↑L * ↑L * ↑Lg) / ↑L * dist x ynegX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)Φ₀:X ≃ₜ ThΦ₀:∀ (x : X), Φ₀ x = (slc (g x)) xx:Xy:Xh_lower_bound✝:dist ((slc (g y)) x) ((slc (g y)) y) ≥ 1 / ↑L * dist x yh_lower_bound:dist ((slc (g x)) x) ((slc (g y)) x) ≤ ↑L * ↑Lg * dist x yhL:¬L = 0⊢ dist (Φ₀ x) (Φ₀ y) ≥ (1 - ↑L * ↑L * ↑Lg) / ↑L * dist x y <;>posX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)Φ₀:X ≃ₜ ThΦ₀:∀ (x : X), Φ₀ x = (slc (g x)) xx:Xy:Xh_lower_bound✝:dist ((slc (g y)) x) ((slc (g y)) y) ≥ 1 / ↑L * dist x yh_lower_bound:dist ((slc (g x)) x) ((slc (g y)) x) ≤ ↑L * ↑Lg * dist x yhL:L = 0⊢ dist (Φ₀ x) (Φ₀ y) ≥ (1 - ↑L * ↑L * ↑Lg) / ↑L * dist x ynegX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)Φ₀:X ≃ₜ ThΦ₀:∀ (x : X), Φ₀ x = (slc (g x)) xx:Xy:Xh_lower_bound✝:dist ((slc (g y)) x) ((slc (g y)) y) ≥ 1 / ↑L * dist x yh_lower_bound:dist ((slc (g x)) x) ((slc (g y)) x) ≤ ↑L * ↑Lg * dist x yhL:¬L = 0⊢ dist (Φ₀ x) (Φ₀ y) ≥ (1 - ↑L * ↑L * ↑Lg) / ↑L * dist x y simp_all +decide [ div_eq_inv_mul, mul_assoc ]negX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg gL':ℝ≥0Φ₀:X ≃ₜ Tx:Xy:Xhsmall:↑L * (↑L * ↑Lg) < 1hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * (↑L * ↑Lg))hΦ₀:∀ (x : X), Φ₀ x = (slc (g x)) xh_lower_bound✝:(↑L)⁻¹ * dist x y ≤ dist ((slc (g y)) x) ((slc (g y)) y)h_lower_bound:dist ((slc (g x)) x) ((slc (g y)) x) ≤ ↑L * (↑Lg * dist x y)hL:¬L = 0⊢ (↑L)⁻¹ * ((1 - ↑L * (↑L * ↑Lg)) * dist x y) ≤ dist ((slc (g x)) x) ((slc (g y)) y);
      have := dist_triangle_left ( slc ( g y ) x ) ( slc ( g y ) y ) ( slc ( g x ) x )negX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg gL':ℝ≥0Φ₀:X ≃ₜ Tx:Xy:Xhsmall:↑L * (↑L * ↑Lg) < 1hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * (↑L * ↑Lg))hΦ₀:∀ (x : X), Φ₀ x = (slc (g x)) xh_lower_bound✝:(↑L)⁻¹ * dist x y ≤ dist ((slc (g y)) x) ((slc (g y)) y)h_lower_bound:dist ((slc (g x)) x) ((slc (g y)) x) ≤ ↑L * (↑Lg * dist x y)hL:¬L = 0this:dist ((slc (g y)) x) ((slc (g y)) y) ≤ dist ((slc (g x)) x) ((slc (g y)) x) + dist ((slc (g x)) x) ((slc (g y)) y)⊢ (↑L)⁻¹ * ((1 - ↑L * (↑L * ↑Lg)) * dist x y) ≤ dist ((slc (g x)) x) ((slc (g y)) y) ; simp_all +decide [ mul_comm ]negX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmg:X → PL':ℝ≥0Φ₀:X ≃ₜ Tx:Xy:Xhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ dist p p' * ↑Lhg:LipschitzWith Lg ghsmall:↑L * (↑L * ↑Lg) < 1hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * (↑L * ↑Lg))hΦ₀:∀ (x : X), Φ₀ x = (slc (g x)) xh_lower_bound✝:dist x y * (↑L)⁻¹ ≤ dist ((slc (g y)) x) ((slc (g y)) y)h_lower_bound:dist ((slc (g x)) x) ((slc (g y)) x) ≤ ↑L * (dist x y * ↑Lg)hL:¬L = 0this:dist ((slc (g y)) x) ((slc (g y)) y) ≤ dist ((slc (g x)) x) ((slc (g y)) x) + dist ((slc (g x)) x) ((slc (g y)) y)⊢ (↑L)⁻¹ * (dist x y * (1 - ↑L * (↑L * ↑Lg))) ≤ dist ((slc (g x)) x) ((slc (g y)) y);
      nlinarith [ show 0 < ( L : ℝ ) byX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)⊢ ∃ Φ, (∀ (x : X), Φ x = (slc (g x)) x) ∧ LipschitzWith L' ⇑Φ ∧ LipschitzWith L' ⇑Φ.symm positivityAll goals completed! 🐙, inv_mul_cancel_left₀ ( show ( L : ℝ ) ≠ 0 byX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)⊢ ∃ Φ, (∀ (x : X), Φ x = (slc (g x)) x) ∧ LipschitzWith L' ⇑Φ ∧ LipschitzWith L' ⇑Φ.symm positivityAll goals completed! 🐙 ) ( dist x y ) ];
    rw [ lipschitzWith_iff_dist_le_mul ]refine'_2X:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)Φ₀:X ≃ₜ ThΦ₀:∀ (x : X), Φ₀ x = (slc (g x)) xh_lower_bound:∀ (x y : X), dist (Φ₀ x) (Φ₀ y) ≥ (1 - ↑L * ↑L * ↑Lg) / ↑L * dist x y⊢ ∀ (x y : T), dist (Φ₀.symm x) (Φ₀.symm y) ≤ ↑L' * dist x y;
    intro x yrefine'_2X:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)Φ₀:X ≃ₜ ThΦ₀:∀ (x : X), Φ₀ x = (slc (g x)) xh_lower_bound:∀ (x y : X), dist (Φ₀ x) (Φ₀ y) ≥ (1 - ↑L * ↑L * ↑Lg) / ↑L * dist x yx:Ty:T⊢ dist (Φ₀.symm x) (Φ₀.symm y) ≤ ↑L' * dist x y; specialize h_lower_bound ( Φ₀.symm x ) ( Φ₀.symm y )refine'_2X:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)Φ₀:X ≃ₜ ThΦ₀:∀ (x : X), Φ₀ x = (slc (g x)) xx:Ty:Th_lower_bound:dist (Φ₀ (Φ₀.symm x)) (Φ₀ (Φ₀.symm y)) ≥ (1 - ↑L * ↑L * ↑Lg) / ↑L * dist (Φ₀.symm x) (Φ₀.symm y)⊢ dist (Φ₀.symm x) (Φ₀.symm y) ≤ ↑L' * dist x y ; simp_all +decide [ div_mul_eq_mul_div ]refine'_2X:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)Φ₀:X ≃ₜ ThΦ₀:∀ (x : X), Φ₀ x = (slc (g x)) xx:Ty:Th_lower_bound:(1 - ↑L * ↑L * ↑Lg) * dist (Φ₀.symm x) (Φ₀.symm y) / ↑L ≤
  dist ((slc (g (Φ₀.symm x))) (Φ₀.symm x)) ((slc (g (Φ₀.symm y))) (Φ₀.symm y))⊢ dist (Φ₀.symm x) (Φ₀.symm y) ≤ ↑L' * dist x y ;
    by_cases hL : L = 0posX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)Φ₀:X ≃ₜ ThΦ₀:∀ (x : X), Φ₀ x = (slc (g x)) xx:Ty:Th_lower_bound:(1 - ↑L * ↑L * ↑Lg) * dist (Φ₀.symm x) (Φ₀.symm y) / ↑L ≤
  dist ((slc (g (Φ₀.symm x))) (Φ₀.symm x)) ((slc (g (Φ₀.symm y))) (Φ₀.symm y))hL:L = 0⊢ dist (Φ₀.symm x) (Φ₀.symm y) ≤ ↑L' * dist x ynegX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)Φ₀:X ≃ₜ ThΦ₀:∀ (x : X), Φ₀ x = (slc (g x)) xx:Ty:Th_lower_bound:(1 - ↑L * ↑L * ↑Lg) * dist (Φ₀.symm x) (Φ₀.symm y) / ↑L ≤
  dist ((slc (g (Φ₀.symm x))) (Φ₀.symm x)) ((slc (g (Φ₀.symm y))) (Φ₀.symm y))hL:¬L = 0⊢ dist (Φ₀.symm x) (Φ₀.symm y) ≤ ↑L' * dist x y <;>posX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)Φ₀:X ≃ₜ ThΦ₀:∀ (x : X), Φ₀ x = (slc (g x)) xx:Ty:Th_lower_bound:(1 - ↑L * ↑L * ↑Lg) * dist (Φ₀.symm x) (Φ₀.symm y) / ↑L ≤
  dist ((slc (g (Φ₀.symm x))) (Φ₀.symm x)) ((slc (g (Φ₀.symm y))) (Φ₀.symm y))hL:L = 0⊢ dist (Φ₀.symm x) (Φ₀.symm y) ≤ ↑L' * dist x ynegX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)Φ₀:X ≃ₜ ThΦ₀:∀ (x : X), Φ₀ x = (slc (g x)) xx:Ty:Th_lower_bound:(1 - ↑L * ↑L * ↑Lg) * dist (Φ₀.symm x) (Φ₀.symm y) / ↑L ≤
  dist ((slc (g (Φ₀.symm x))) (Φ₀.symm x)) ((slc (g (Φ₀.symm y))) (Φ₀.symm y))hL:¬L = 0⊢ dist (Φ₀.symm x) (Φ₀.symm y) ≤ ↑L' * dist x y simp_all +decide [ mul_assoc, mul_comm ]negX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmg:X → PL':ℝ≥0Φ₀:X ≃ₜ Tx:Ty:Thjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ dist p p' * ↑Lhg:LipschitzWith Lg ghsmall:↑L * (↑L * ↑Lg) < 1hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * (↑L * ↑Lg))hΦ₀:∀ (x : X), Φ₀ x = (slc (g x)) xh_lower_bound:(1 - ↑L * (↑L * ↑Lg)) * dist (Φ₀.symm x) (Φ₀.symm y) / ↑L ≤
  dist ((slc (g (Φ₀.symm x))) (Φ₀.symm x)) ((slc (g (Φ₀.symm y))) (Φ₀.symm y))hL:¬L = 0⊢ dist (Φ₀.symm x) (Φ₀.symm y) ≤ dist x y * ↑L';
    ·posX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0g:X → PL':ℝ≥0Φ₀:X ≃ₜ Tx:Ty:ThslcLip:∀ (p : P) (x y : X), x = yhslcInv:∀ (p : P) (x y : T), x = yhjoint:∀ (x : X) (p p' : P), (slc p) x = (slc p') xhg:LipschitzWith Lg ghΦ₀:∀ (x : X), Φ₀ x = (slc (g x)) xhL:L = 0⊢ dist (Φ₀.symm x) (Φ₀.symm y) ≤ dist x y * ↑L' cases hslcInv ( g ( Classical.arbitrary X ) ) x ypos.reflX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0g:X → PL':ℝ≥0Φ₀:X ≃ₜ Tx:ThslcLip:∀ (p : P) (x y : X), x = yhslcInv:∀ (p : P) (x y : T), x = yhjoint:∀ (x : X) (p p' : P), (slc p) x = (slc p') xhg:LipschitzWith Lg ghΦ₀:∀ (x : X), Φ₀ x = (slc (g x)) xhL:L = 0⊢ dist (Φ₀.symm x) (Φ₀.symm x) ≤ dist x x * ↑L' ; aesopAll goals completed! 🐙;
    ·negX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmg:X → PL':ℝ≥0Φ₀:X ≃ₜ Tx:Ty:Thjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ dist p p' * ↑Lhg:LipschitzWith Lg ghsmall:↑L * (↑L * ↑Lg) < 1hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * (↑L * ↑Lg))hΦ₀:∀ (x : X), Φ₀ x = (slc (g x)) xh_lower_bound:(1 - ↑L * (↑L * ↑Lg)) * dist (Φ₀.symm x) (Φ₀.symm y) / ↑L ≤
  dist ((slc (g (Φ₀.symm x))) (Φ₀.symm x)) ((slc (g (Φ₀.symm y))) (Φ₀.symm y))hL:¬L = 0⊢ dist (Φ₀.symm x) (Φ₀.symm y) ≤ dist x y * ↑L' rw [ div_le_iff₀ ( by positivity ) ] at h_lower_boundnegX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmg:X → PL':ℝ≥0Φ₀:X ≃ₜ Tx:Ty:Thjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ dist p p' * ↑Lhg:LipschitzWith Lg ghsmall:↑L * (↑L * ↑Lg) < 1hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * (↑L * ↑Lg))hΦ₀:∀ (x : X), Φ₀ x = (slc (g x)) xh_lower_bound:(1 - ↑L * (↑L * ↑Lg)) * dist (Φ₀.symm x) (Φ₀.symm y) ≤
  dist ((slc (g (Φ₀.symm x))) (Φ₀.symm x)) ((slc (g (Φ₀.symm y))) (Φ₀.symm y)) * ↑LhL:¬L = 0⊢ dist (Φ₀.symm x) (Φ₀.symm y) ≤ dist x y * ↑L';
      simp_all +decide [ ← hΦ₀ ]negX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmg:X → PL':ℝ≥0Φ₀:X ≃ₜ Tx:Ty:Thjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ dist p p' * ↑Lhg:LipschitzWith Lg ghsmall:↑L * (↑L * ↑Lg) < 1hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * (↑L * ↑Lg))h_lower_bound:(1 - ↑L * (↑L * ↑Lg)) * dist (Φ₀.symm x) (Φ₀.symm y) ≤ dist x y * ↑LhL:¬L = 0⊢ dist (Φ₀.symm x) (Φ₀.symm y) ≤ dist x y * ↑L';
      nlinarith [ show 0 < ( L : ℝ ) byX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)⊢ ∃ Φ, (∀ (x : X), Φ x = (slc (g x)) x) ∧ LipschitzWith L' ⇑Φ ∧ LipschitzWith L' ⇑Φ.symm positivityAll goals completed! 🐙, show 0 ≤ dist x y byX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)⊢ ∃ Φ, (∀ (x : X), Φ x = (slc (g x)) x) ∧ LipschitzWith L' ⇑Φ ∧ LipschitzWith L' ⇑Φ.symm positivityAll goals completed! 🐙, show 0 ≤ dist ( Φ₀.symm x ) ( Φ₀.symm y ) byX:Type u_1T:Type u_2P:Type u_3inst✝⁴:MetricSpace Xinst✝³:MetricSpace Tinst✝²:PseudoMetricSpace Pinst✝¹:CompactSpace Xinst✝:Nonempty Xslc:P → X ≃ₜ TL:ℝ≥0Lg:ℝ≥0hslcLip:∀ (p : P), LipschitzWith L ⇑(slc p)hslcInv:∀ (p : P), LipschitzWith L ⇑(slc p).symmhjoint:∀ (x : X) (p p' : P), dist ((slc p) x) ((slc p') x) ≤ ↑L * dist p p'g:X → Phg:LipschitzWith Lg ghsmall:↑L * ↑L * ↑Lg < 1L':ℝ≥0hL'lip:↑L * (1 + ↑Lg) ≤ ↑L'hL'inv:↑L ≤ ↑L' * (1 - ↑L * ↑L * ↑Lg)⊢ ∃ Φ, (∀ (x : X), Φ x = (slc (g x)) x) ∧ LipschitzWith L' ⇑Φ ∧ LipschitzWith L' ⇑Φ.symm positivityAll goals completed! 🐙 ]

end FamiliesOfMapsB01
end Submission

(The Lean statement takes the target constant L' as an input constrained by L(1 + L_g) \le L' and L \le L'(1 - L^2 L_g); the choice of L' displayed above is made at the call site in the main construction.)