Very dependent product

Stream: general

[Patrick Massot]

Is there a trick to have a type which is like a dependent product Π k : ℕ, X k except the definition of X (k+1) depends on the value chosen in X k? I know this doesn't make sense, I'm asking how to get something which makes sense.

[Patrick Massot]

Let me try to avoid the #xy issue. The context is I try, again, to build inductively build a sequence u : ℕ → Y but recording many properties linking u k and u (k+1), so I thought maybe u should live in a sort of dependent product.

[Johan Commelin]

I think well_founded.fix is meant to be the solution to this problem.

[Johan Commelin]

But it is a thoroughly foreign concept for most mathematicians (like me).

[Sebastien Gouezel]

Can't you do it by using choose to assert the relationship between u k and u (k+1), and nat.rec_on to do the induction, like in the proof of Baire theorem https://github.com/leanprover-community/mathlib/blob/62cb7f2f34079df7c054239d467f72c61be4f63a/src/topology/metric_space/baire.lean#L123 ?

[Chris Hughes]

This sounds a bit like Reid's crec might help, but I might be completely wrong as I don't properly understand it.

[Reid Barton]

Yes, this is what crec does

[Patrick Massot]

Let me try a #mwe, especially since Sébastien and Reid are around:

import topology.metric_space.basic
import analysis.specific_limits

open_locale classical topological_space big_operators
open filter finset

example {X: Type} [metric_space X] (x : X) (ε : ℝ) (ε_pos : 0 < ε)
  {φ : X → ℝ}
  (h : ∀ k : ℕ, ∀ (x' : X),
        (dist x' x ≤ 2 * ε ∧ ε * φ x ≤ ε/2^k * φ x') → ∃ (y : X), dist x' y ≤ ε/2^k ∧ 2 * φ x' < φ y) :
∃ u : ℕ → X, u 0 = x ∧ ∀ k, dist (u k) (u $ k+1) ≤ ε/2^k ∧ ε * φ x ≤ ε/2^k * φ (u k) :=
begin
  /-
  Set u 0 = x. Assume u is constructed until rank k.
  In particular dist x (u k) ≤ ∑ j in range k, ε/2^j ≤ 2*ε
  Specialize h to k and u k and what we know about u k. The existential in h then gives u (k+1).
  -/
  sorry
end

[Patrick Massot]

I hope I kept enough information to make this correct and relevant.

[Patrick Massot]

@Sebastien Gouezel do you think you could try to unsorry the above proof?

[Sebastien Gouezel]

Yes, I will unsorry your proof, but not now as the kids want to go to the beach (nice week-end at < 100km from Rennes :)

[Johan Commelin]

Enjoy!

[Yury G. Kudryashov]

You can start with

example {X: Type} [metric_space X] (x : X) (ε : ℝ) (ε_pos : 0 < ε)
  {φ : X → ℝ}
  (h : ∀ k : ℕ, ∀ (x' : X),
        (dist x' x ≤ 2 * ε ∧ ε * φ x ≤ ε/2^k * φ x') → ∃ (y : X), dist x' y ≤ ε/2^k ∧ 2 * φ x' < φ y) :
∃ u : ℕ → X, u 0 = x ∧ ∀ k, dist (u k) (u $ k+1) ≤ ε/2^k ∧ ε * φ x ≤ ε/2^k * φ (u k) :=
begin
  replace h : ∀ (k : ℕ) (x' : X), ∃ y : X,
    ((dist x' x ≤ 2 * ε ∧ ε * φ x ≤ ε/2^k * φ x') → (dist x' y ≤ ε/2^k ∧ 2 * φ x' < φ y)) :=
  λ k x', ⟨@classical.epsilon X ⟨x⟩ (λ y, dist x' y ≤ ε/2^k ∧ 2 * φ x' < φ y),
    λ h', classical.epsilon_spec (h k x' h')⟩,
  choose u_step hu_step using h,
  let u : ℕ → X := λ n, nat.rec_on n x u_step,
  have u_succ : ∀ n, u (n + 1) = u_step n (u n) := λ n, rfl,
  refine ⟨u, rfl, _⟩,
  intro n,
  induction n using nat.strong_rec' with n ihn,

  /-
  Set u 0 = x. Assume u is constructed until rank k.
  In particular dist x (u k) ≤ ∑ j in range k, ε/2^j ≤ 2*ε
  Specialize h to k and u k and what we know about u k. The existential in h then gives u (k+1).
  -/
end

At this moment all type-related problems are solved.

[Yury G. Kudryashov]

And the proof state is

X : Type,
_inst_1 : metric_space X,
x : X,
ε : ℝ,
ε_pos : 0 < ε,
φ : X → ℝ,
u_step : ℕ → X → X,
hu_step :
  ∀ (k : ℕ) (x' : X),
    dist x' x ≤ 2 * ε ∧ ε * φ x ≤ ε / 2 ^ k * φ x' →
    dist x' (u_step k x') ≤ ε / 2 ^ k ∧ 2 * φ x' < φ (u_step k x'),
u : ℕ → X := λ (n : ℕ), n.rec_on x u_step,
u_succ : ∀ (n : ℕ), u (n + 1) = u_step n (u n),
n : ℕ,
ihn :
  ∀ (m : ℕ),
    m < n → (λ (n : ℕ), dist (u n) (u (n + 1)) ≤ ε / 2 ^ n ∧ ε * φ x ≤ ε / 2 ^ n * φ (u n)) m
⊢ dist (u n) (u (n + 1)) ≤ ε / 2 ^ n ∧ ε * φ x ≤ ε / 2 ^ n * φ (u n)

[Patrick Massot]

Thank you very much Yury! I'll study this. I'm still interested to see Sébastien's version anyway.

[Yury G. Kudryashov]

The first replace changes order of quantifiers to match what is in baire, then I do the trick suggested by Sébastien.

[Sebastien Gouezel]

Here is an (almost) working version, with just one sorry left:

import topology.metric_space.basic
import analysis.specific_limits
import tactic.ring_exp

open_locale classical topological_space big_operators
open filter finset

lemma dist_le_of_geometric_aux {X : Type} [metric_space X] {u : ℕ → X} {n : ℕ} {ε : ℝ}
  (h : ∀ m < n, dist (u m) (u (m+1)) ≤ ε/2^m) : dist (u 0) (u n) ≤ 2 * ε :=
sorry

example {X: Type} [metric_space X] (x : X) (ε : ℝ) (ε_pos : 0 < ε)
  {φ : X → ℝ}
  (h : ∀ k : ℕ, ∀ (x' : X),
        (dist x' x ≤ 2 * ε ∧ ε * φ x ≤ ε/2^k * φ x') → ∃ (y : X), dist x' y ≤ ε/2^k ∧ 2 * φ x' < φ y) :
∃ u : ℕ → X, u 0 = x ∧ ∀ k, dist (u k) (u $ k+1) ≤ ε/2^k ∧ ε * φ x ≤ ε/2^k * φ (u k) :=
begin
  /-
  Set u 0 = x. Assume u is constructed until rank k.
  In particular dist x (u k) ≤ ∑ j in range k, ε/2^j ≤ 2*ε
  Specialize h to k and u k and what we know about u k. The existential in h then gives u (k+1).
  -/
  have : ∀ (k : ℕ) (x' : X), ∃ (y : X),
    (dist x' x ≤ 2 * ε ∧ ε * φ x ≤ ε/2^k * φ x') → (dist x' y ≤ ε/2^k ∧ 2 * φ x' < φ y),
  { assume k x',
    by_cases H : dist x' x ≤ 2 * ε ∧ ε * φ x ≤ ε/2^k * φ x',
    { rcases h k x' H with ⟨y, hy⟩,
      exact ⟨y, λ _, hy⟩ },
    { use x } },
  choose F hF using this,
  let u : ℕ → X := λ n, nat.rec_on n x F,
  have u0 : u 0 = x := rfl,
  have un : ∀ (n : ℕ), u (n+1) = F n (u n) := λ n, rfl,
  refine ⟨u, u0, λ n, _⟩,
  induction n using nat.case_strong_induction_on with n IH,
  { simpa only [u0, le_refl, div_one', pow_zero, and_true] using (hF 0 x _).left,
    simp only [le_refl, and_true, div_one', pow_zero, dist_self],
    linarith },
  { rw un,
    have Dn : ∀ m ≤ n+1, dist (u m) x ≤ 2 * ε,
    { assume m hm,
      rw [dist_comm, ← u0],
      apply dist_le_of_geometric_aux (λ k hk, (IH k _).1),
      exact nat.lt_succ_iff.mp (lt_of_lt_of_le hk hm)},
    have A : ε * φ x ≤ ε / 2 ^ n.succ * φ (u n.succ),
    { apply le_trans (IH n (le_refl _)).2 _,
      rw [nat.succ_eq_add_one, un],
      have Z : 2 * φ (u n) ≤ φ (F n (u n)) :=
        le_of_lt ((hF n (u n) ⟨Dn _ (nat.le_succ n), (IH n (le_refl _)).2⟩).2),
      have : 0 ≤ ε / 2^(n+1),
      { apply div_nonneg (le_of_lt ε_pos) (pow_pos _ _), norm_num },
      convert mul_le_mul_of_nonneg_left Z this using 1,
      field_simp,
      ring_exp },
    exact ⟨(hF n.succ _ ⟨Dn _ (le_refl _), A⟩).1, A⟩ }
end

This is cheating a little bit, since using junk values in the definition of F one can define your sequence by induction, and then check its properties (i.e., separate the data from the proof). It would be possible to do it also mixing the data and the proof as nat.rec_on allows you to have a different type at each step, so it makes it possible to construct a sequence u such that u n belongs to the subtype {y // dist y x ≤ 2 * ε - ε / 2 ^ n ∧ ε * φ x ≤ ε/2^n * φ y}. But it means you have to do together the definition and the proof. This is definitely possible, but less convenient.

[Sebastien Gouezel]

I hadn't looked at Yury's suggestion. It is essentially the same, although he's clearly better at golf :)

[Patrick Massot]

Thank you very much Sébastien, I'll read both your code and Yury's carefully. Constructing a u in this dependent product is what I started doing, but it didn't sound fun.

[Reid Barton]

I'll try to get to crec tomorrow and try out this example

[Reid Barton]

Meanwhile I will distract Patrick with #2879

[Patrick Massot]

I don't know how I'm meant to be distracted. I'd love to have this tactic but I don't know how I could help.

[Patrick Massot]

I hope to return to the main topic of this thread today, maybe I should say what is the full context. What I'm formalizing is Lemma 5.21 on Page 179 of https://arxiv.org/abs/1011.1690.

[Patrick Massot]

Don't be worried by the title of this book, I'm really interested only in this lemma (at least until mathlib gets a long way in geometry and analysis).

[Patrick Massot]

Actually I think this is a very nice formalization challenge. Anyone can participate. You don't even need to know about metric spaces, this lemma is not easier when $X = \mathbb R$. I'd be interested to see @Mario Carneiro or @Kenny Lau golfing this (without necessarily following the "proof" from that book).

[Patrick Massot]

In case it's not clear, the name attached to this lemma also features on https://www.math.ias.edu/people/faculty.

[Mario Carneiro]

Would you care to state the theorem? Or is that part of the challenge

[Patrick Massot]

Sure I can state it

[Patrick Massot]

import topology.metric_space.basic
open_locale classical topological_space

lemma hofer {X: Type} [metric_space X] [complete_space X] (x : X) (ε : ℝ) (ε_pos : 0 < ε)
  {φ : X → ℝ} (cont : continuous φ) (nonneg : ∀ x, 0 ≤ φ x) :
∃ (ε' > 0) (x' : X), ε' ≤ ε ∧
                   dist x' x ≤ 2*ε ∧
                   ε * φ x ≤ ε' * φ x' ∧
                   ∀ y, dist x' y ≤ ε' → φ y ≤ 2*φ x' :=
sorry

[Patrick Massot]

The notations are slightly different because this is taken from the original paper, not the textbook.

[Patrick Massot]

I apologize for not having given the full context yesterday, but I'm really interested in learning how to build sequences by non trivial induction in Lean, since it is a very common proof scheme that doesn't translate easily.

[Kenny Lau]

import topology.metric_space.basic
open_locale classical topological_space

-- A non-negative sequence f(n) with 2f(n) < f(n+1) is unbounded.
lemma aux1 (f : ℕ → ℝ) (h1 : ∀ n, 0 ≤ f n) (h2 : ∀ n, 2 * f n < f (n + 1)) (N : ℝ) :
  ∃ n, N ≤ f n :=
sorry

lemma hofer {X: Type} [metric_space X] [complete_space X] (x : X) (ε : ℝ) (ε_pos : 0 < ε)
  {φ : X → ℝ} (cont : continuous φ) (nonneg : ∀ x, 0 ≤ φ x) :
∃ (ε' > 0) (x' : X), ε' ≤ ε ∧
                   dist x' x ≤ 2*ε ∧
                   ε * φ x ≤ ε' * φ x' ∧
                   ∀ y, dist x' y ≤ ε' → φ y ≤ 2*φ x' :=
begin
  let f : ℕ → X := λ n, nat.rec_on n x (λ n ih,
    if H : ∃ y : X, dist ih y ≤ ε / 2^n ∧ 2 * φ ih < φ y then classical.some H else ih),
  have h1 : cauchy_seq f := sorry,
  have h2 : ∃ p : X, ∀ δ : ℝ, 0 < δ → ∃ N : ℕ, ∀ n, N ≤ n → dist (f n) p < δ := sorry,
  have h3 : ¬∀ n, ∃ y : X, dist (f n) y ≤ ε / 2^n ∧ 2 * φ (f n) < φ y,
  { intro H,
    have := aux1 (φ ∘ f) (λ n, nonneg (f n)) (λ n,
      show 2 * φ (f n) < φ (if H : ∃ y : X, dist (f n) y ≤ ε / 2^n ∧ 2 * φ (f n) < φ y then classical.some H else f n),
      by { rw dif_pos (H n), exact (classical.some_spec (H n)).2 }),
    sorry },
  rw not_forall at h3, cases h3 with N HN,
  sorry
end

[Kenny Lau]

how about something like this

[Kenny Lau]

I've converted 1 sorry into 5 sorrys

[Kenny Lau]

surely this must mean progress

[Mario Carneiro]

I used classical.epsilon instead of classical.some there

[Patrick Massot]

I'll read Kenny's message next. But first I have a question. Sébastien and Yury both use a version of the following trick that I was missing:

open classical

example {X : Type*} (P : X → Prop) (Q : X → X → Prop) (h : ∀ x, P x → ∃ y, Q x y) :
∀ x, ∃ y, P x → Q x y :=
λ x, ⟨@epsilon X ⟨x⟩ (λ y, Q x y), λ hx, epsilon_spec (h x hx)⟩
/- with readable tactic state:
begin
  by_cases hx : P x,
  finish,
  use x,
end
-/

Is this part of a more general trick? Can this be avoided?

[Mario Carneiro]

It can be avoided, but it is a lot easier to take advantage of potential garbage results in order to delay the proof of properties of the sequence until you are done defining it

[Patrick Massot]

Defining Kenny's f sequence was my original plan, but then I thought I should start with by_contradiction

[Mario Carneiro]

I've made it this far:

begin
  by_contra H,
  haveI : nonempty X := ⟨x⟩,
  let xi : ℕ → X × ℝ :=
    λ n, nat.rec_on n (x, ε) (λ _ ⟨x, ε⟩,
      (classical.epsilon (λ x', dist x x' ≤ ε ∧ 2 * φ x < φ x'), ε/2)),

end

[Patrick Massot]

I'm also curious to see why we use all these λ n, nat.rec_on n ... instead of nat.rec. Is this purely a failure of the elaborator or are there deeper reasons?

[Kenny Lau]

the former

[Kenny Lau]

left to right elaboration

[Patrick Massot]

Mario's start looks very close to the informal proof, I'd be curious to see whether it is manageable.

[David Wärn]

Patrick Massot said:

I apologize for not having given the full context yesterday, but I'm really interested in learning how to build sequences by non trivial induction in Lean, since it is a very common proof scheme that doesn't translate easily.

#2850 is meant to do this sort of inductive construction, but I'm not sure how suitable it is here. Isn't "apply Baire category theorem" the canonical solution to this sort of question about complete metric spaces? In a sense #2850 is equivalent to BCT

[Mario Carneiro]

Indeed, the proof here looks very similar to BCT

[Patrick Massot]

David, I'd be curious to see whether you can prove this using #2850.

[Patrick Massot]

I also don't know a proof using Baire. But I can tell you this lemma is equivalent to $X$ being complete if you move everything but $X$ right of the colon.

[Patrick Massot]

Kenny's attempt seems pretty hard to complete. As I feared when I decided not to try that, you really need to reason about the first time you switch branch in the definition of f.

[Kenny Lau]

for which sorry?

[Kenny Lau]

you can prove dist (f n) (f (n+1)) <= \e / 2^n unconditionally

[Kenny Lau]

up to indexing error

[Patrick Massot]

This is the easy part. The issue is with ε * φ x ≤ ε / 2 ^ N * φ (f N)

[Reid Barton]

Here is my "crec style" attempt, where I've sorryed some of the boring inequality bits. This is not actually using crec, just the principle behind it. I still need to think about whether crec really helps in this case, but after breakfast.

import topology.metric_space.basic
import data.pfun
open_locale classical topological_space

/-- "Partial" choice, in the sense of pfun/roption:
choose a value `x` satisfying `p x` if there is one, otherwise fail. -/
noncomputable def pchoice {α : Sort*} (p : α → Prop) : roption α :=
{ dom := ∃ x, p x, get := λ H, classical.some H }

lemma div_le_self {α β : ℝ} (hα : α ≥ 0) (hβ : β > 0) : α / β ≤ α := sorry

lemma hofer {X: Type} [metric_space X] [complete_space X] (x : X) (ε : ℝ) (ε_pos : 0 < ε)
  {φ : X → ℝ} (cont : continuous φ) (nonneg : ∀ x, 0 ≤ φ x) :
∃ (ε' > 0) (x' : X), ε' ≤ ε ∧
                   dist x' x ≤ 2*ε ∧
                   ε * φ x ≤ ε' * φ x' ∧
                   ∀ y, dist x' y ≤ ε' → φ y ≤ 2*φ x' :=
-- Build the sequence x₀, x₁, ... as a partial function
let f : ℕ →. X :=
  λ n, nat.rec_on n
    (pure x)
    (λ n ih, do
      -- get the previous value (if defined)
      x' ← ih,
      -- choose a legal next value
      pchoice (λ (y : X), dist x' y ≤ ε / 2^n ∧ 2 * φ x' < φ y)) in
begin
  -- Establish some basic properties of the construction
  have def_of_succ_def : ∀ {n}, n + 1 ∈ f.dom → n ∈ f.dom := λ n hn, hn.fst,
  have dist_pair_bound : ∀ {n} (hn : n ∈ f.dom) (hn' : n+1 ∈ f.dom),
    dist ((f n).get hn) ((f (n+1)).get hn') ≤ ε / 2 ^ n,
  { intros n hn hn',
    let H := _,
    change dist ((f n).get hn) (classical.some H) ≤ ε / 2 ^ n,
    exact (classical.some_spec H).1 },
  have dist_x_bound : ∀ {n} (hn : n ∈ f.dom), dist ((f n).get hn) x ≤ 2 * ε,
  { suffices : ∀ {n} (hn : n ∈ f.dom), dist ((f n).get hn) x ≤ 2 * (1 - 1 / 2^n) * ε,
    { intros n hn,
      refine le_trans (this hn) _,
      sorry },
    intro n,
    induction n with n IH,
    { intro,
      change dist x x ≤ _,
      simp },
    { intro hn,
      have := dist_pair_bound (def_of_succ_def hn) hn,
      have := IH (def_of_succ_def hn),
      sorry } },
  have φ_pair_bound : ∀ {n} (hn : n ∈ f.dom) (hn' : n + 1 ∈ f.dom),
    2 * φ ((f n).get hn) < φ ((f (n+1)).get hn'),
  { intros n hn hn',
    let H := _,
    change 2 * φ ((f n).get hn) < φ (classical.some H),
    exact (classical.some_spec H).2 },
  have φ_bound : ∀ {n} (hn : n ∈ f.dom), 2 ^ n * φ x ≤ φ ((f n).get hn),
  { intro n,
    induction n with n IH,
    { intro,
      change 2 ^ 0 * φ x ≤ φ x,
      simp },
    { intro hn,
      have := φ_pair_bound (def_of_succ_def hn) hn,
      have := IH (def_of_succ_def hn),
      sorry } },
  -- If the construction stops, we can extract the required x'
  suffices H : ∃ n, n ∉ f.dom,
  { have hn₁ := nat.find_spec H,
    cases hn : nat.find H with n; rw hn at hn₁,
    { exact false.elim (hn₁ trivial) },
    have : n ∈ f.dom,
    { apply classical.not_not.mp,
      apply nat.find_min H,
      rw hn,
      apply nat.lt_succ_self },
    have pε : ε / 2^n > 0 := div_pos ε_pos (pow_pos two_pos _),
    let x' := (f n).get this,
    refine ⟨ε / 2^n, pε,
      x', div_le_self (le_of_lt ε_pos) (pow_pos two_pos _),
      dist_x_bound this, _, _⟩,
    { calc
        ε * φ x = ε / 2 ^ n * (2 ^ n * φ x) : by { field_simp, ring }
      ...       ≤ ε / 2 ^ n * φ _ : by { rw mul_le_mul_left pε, apply φ_bound } },
    have : ¬ ∃ y, dist x' y ≤ ε / 2^n ∧ 2 * φ x' < φ y,
    { -- otherwise, f (n+1) would be defined too, contradicting hn₁
      intro h,
      exact hn₁ ⟨this, h⟩ },
    intros y hy,
    apply le_of_not_lt,
    exact λ h, this ⟨y, hy, h⟩ },
  -- Otherwise, we use the construction to build a Cauchy sequence
  by_contradiction H,
  push_neg at H,
  let f' : ℕ → X := λ n, (f n).get (H n),
  have dist_pair_bound' : ∀ n, dist (f' n) (f' (n+1)) ≤ ε / 2 ^ n :=
    λ n, dist_pair_bound (H n) (H (n+1)),
  have φ_bound' : ∀ n, 2 ^ n * φ x ≤ φ (f' n) := λ n, φ_bound (H n),
  -- f' is a Cauchy sequence on which φ diverges
  sorry
end

[Reid Barton]

I tried to follow the order of the original proof. As such, this falls a bit outside the intended scope of crec because you have no reason to think that the construction of the sequence will always be successful. Probably more efficient is to prove the statement by contradiction, which tells you that building the sequence has to succeed.

[Reid Barton]

One annoyance: do notation seems not to work inside tactic mode (?)

[Patrick Massot]

Thank you very much Reid! I'll read that. I totally agree that proving the statement by contradiction from the beginning can only be more efficient. That's what gives the lemma I wrote yesterday.

[Mario Carneiro]

Proof complete, although not as elegant as I would have liked

import topology.metric_space.basic
open_locale classical topological_space

lemma hofer {X: Type} [metric_space X] [complete_space X] (x : X) (ε : ℝ) (ε_pos : 0 < ε)
  {φ : X → ℝ} (cont : continuous φ) (nonneg : ∀ x, 0 ≤ φ x) :
∃ (ε' > 0) (x' : X), ε' ≤ ε ∧
                   dist x' x ≤ 2*ε ∧
                   ε * φ x ≤ ε' * φ x' ∧
                   ∀ y, dist x' y ≤ ε' → φ y ≤ 2*φ x' :=
begin
  by_contra H,
  haveI : nonempty X := ⟨x⟩,
  let xi : ℕ → X × ℝ :=
    λ n, nat.rec_on n (x, ε) (λ _ ⟨x, ε⟩,
      (classical.epsilon (λ x', dist x x' ≤ ε ∧ 2 * φ x < φ x'), ε/2)),
  have two : 0 < (2:ℝ) := two_pos,
  have main : ∀ n x' ε', xi n = (x', ε') →
    ε' = ε / 2 ^ n ∧ (∀ m < n, φ (xi m).1 * 2 ^ n < φ x' * 2 ^ m) ∧
    (∀ m ≤ n, dist (xi m).1 x' / 2 + ε' ≤ ε / 2 ^ m),
  { intros, induction n with n IH generalizing x' ε',
    { cases a, simp, change (xi 0).1 with x, simp },
    have a' : (prod.rec _ (xi n) : X × ℝ) = _ := a,
    cases e : xi n with x₁ ε₁,
    rw e at a', injection a' with a₁ a₂, clear a',
    obtain ⟨h₁, h₂, h₃⟩ := IH _ _ e,
    have h₁' : ε' = ε / 2 ^ n.succ;
      simp [pow_succ', ← div_div_eq_div_mul, ← h₁, a₂],
    have hx₁ := classical.epsilon_spec _, rw a₁ at hx₁, clear a₁,
    swap, {
      subst h₁,
      by_contra h,
      have h0 := div_pos ε_pos (pow_pos two _),
      refine H ⟨ε / 2 ^ n, h0, x₁, _, _, _, λ y hy, _⟩,
      { refine div_le_of_le_mul (pow_pos two _) _,
        refine le_mul_of_ge_one_left (le_of_lt ε_pos) _,
        exact one_le_pow_of_one_le (by norm_num) _ },
      { have : dist x x₁ / 2 + ε / 2 ^ n ≤ ε / 2 ^ 0 := h₃ 0 (zero_le _),
        rw dist_comm at this, simp at this,
        linarith only [h0, this, ε_pos] },
      { obtain rfl | hn := nat.eq_zero_or_pos n,
        { injection e, subst x₁, simp },
        have := h₂ 0 hn, simp at this,
        rw [div_mul_eq_mul_div, le_div_iff (pow_pos two _), mul_assoc],
        exact le_of_lt ((mul_lt_mul_left ε_pos).2 this) },
      { exact le_of_not_gt (λ h', h ⟨y, hy, h'⟩) } },
    refine ⟨λ m hm, _, λ m hm, _⟩,
    { have hx' := (mul_lt_mul_right (pow_pos two _)).2 hx₁.2,
      obtain hm | rfl := nat.lt_succ_iff_lt_or_eq.1 hm,
      { have := (mul_lt_mul_right two).2 (h₂ _ hm),
        rw [mul_assoc, mul_right_comm, mul_comm (φ x₁)] at this,
        refine lt_trans this hx' },
      { rwa [e, ← mul_assoc, mul_comm, ← mul_assoc] } },
    { obtain hm | rfl := lt_or_eq_of_le hm,
      { refine le_trans _ (h₃ _ (nat.le_of_lt_succ hm)),
        linarith [dist_triangle (xi m).1 x₁ x'] },
      { simp [a, dist_self, h₁'] } } },
  have : cauchy_seq (prod.fst ∘ xi),
  { refine metric.uniformity_basis_dist.cauchy_seq_iff'.2 (λ δ hδ, _),
    obtain ⟨N, hN⟩ := pow_unbounded_of_one_lt (ε / (δ / 2)) one_lt_two,
    rw [div_lt_iff (div_pos hδ two), ← div_lt_iff' (pow_pos two N)] at hN,
    refine ⟨N, λ n hn, _⟩,
    dsimp,
    cases e : xi n with x' ε',
    obtain ⟨rfl, _, h⟩ := main _ _ _ e,
    rw dist_comm, simp,
    linarith [h N hn, div_pos ε_pos (pow_pos two n)] },
  obtain ⟨x₁, h₁⟩ := cauchy_seq_tendsto_of_complete this,
  have hx1 : 0 < φ (xi 1).1,
  { refine lt_of_le_of_lt (mul_nonneg (nonneg x) (le_of_lt two_pos)) _,
    cases e : xi 1 with x' ε',
    simpa using (main 1 _ _ e).2.1 0 dec_trivial },
  obtain ⟨N, hN⟩ := metric.tendsto_at_top.1 ((cont.tendsto _).comp h₁) _ hx1,
  obtain ⟨N₂, hN₂⟩ := pow_unbounded_of_one_lt ((φ (xi 1).1 + φ x₁) / φ (xi 1).1) one_lt_two,
  let M := max N N₂ + 2,
  specialize hN M (le_trans (le_max_left _ _) (nat.le_add_right _ _)),
  revert hN, apply not_lt_of_lt, simp,
  cases e : xi M with x' ε',
  have hM := (main M _ _ e).2.1,
  have := hM 1 (nat.le_add_left 2 (max N N₂)),
  replace hN₂ := lt_of_lt_of_le hN₂ (pow_le_pow (by norm_num)
    (le_add_of_le_of_nonneg (le_max_right N N₂) zero_le_one)),
  rw [div_lt_iff' hx1] at hN₂,
  rw [pow_succ, mul_left_comm, pow_one, mul_comm _ (2:ℝ), mul_lt_mul_left two] at this,
  exact lt_of_lt_of_le (lt_sub_iff_add_lt.2 (lt_trans hN₂ this)) (le_abs_self _)
end