## Stream: general

### Topic: Very dependent product

#### Patrick Massot (May 30 2020 at 13:08):

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 (May 30 2020 at 13:11):

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 (May 30 2020 at 13:12):

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

#### Johan Commelin (May 30 2020 at 13:12):

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

#### Sebastien Gouezel (May 30 2020 at 13:16):

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 (May 30 2020 at 13:17):

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 (May 30 2020 at 13:19):

Yes, this is what crec does

#### Patrick Massot (May 30 2020 at 13:21):

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 (May 30 2020 at 13:21): I hope I kept enough information to make this correct and relevant. #### Patrick Massot (May 30 2020 at 13:43): @Sebastien Gouezel do you think you could try to unsorry the above proof? #### Sebastien Gouezel (May 30 2020 at 13:52): 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 (May 30 2020 at 13:53): Enjoy! #### Yury G. Kudryashov (May 30 2020 at 14:43): 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 (May 30 2020 at 14:44):

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 (May 30 2020 at 15:32):

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

#### Yury G. Kudryashov (May 30 2020 at 15:40):

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

#### Sebastien Gouezel (May 30 2020 at 19:01):

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 _,
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 (May 30 2020 at 19:06):

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

#### Patrick Massot (May 30 2020 at 19:12):

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 (May 30 2020 at 23:13):

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

#### Reid Barton (May 30 2020 at 23:14):

Meanwhile I will distract Patrick with #2879

#### Patrick Massot (May 31 2020 at 09:02):

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 (May 31 2020 at 09:05):

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 (May 31 2020 at 09:06):

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 (May 31 2020 at 09:09):

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 (May 31 2020 at 09:10):

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

#### Mario Carneiro (May 31 2020 at 09:12):

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

#### Patrick Massot (May 31 2020 at 09:12):

Sure I can state it

#### Patrick Massot (May 31 2020 at 09:13):

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 (May 31 2020 at 09:14):

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

#### Patrick Massot (May 31 2020 at 09:15):

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 (May 31 2020 at 09:36):

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 (May 31 2020 at 09:38):

I've converted 1 sorry into 5 sorrys

#### Kenny Lau (May 31 2020 at 09:38):

surely this must mean progress

#### Mario Carneiro (May 31 2020 at 09:44):

I used classical.epsilon instead of classical.some there

#### Patrick Massot (May 31 2020 at 09:46):

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)⟩
begin
by_cases hx : P x,
finish,
use x,
end
-/


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

#### Mario Carneiro (May 31 2020 at 09:48):

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 (May 31 2020 at 09:48):

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

#### Mario Carneiro (May 31 2020 at 09:48):

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 (May 31 2020 at 09:50):

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?

the former

#### Kenny Lau (May 31 2020 at 09:51):

left to right elaboration

#### Patrick Massot (May 31 2020 at 09:53):

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

#### David Wärn (May 31 2020 at 09:53):

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 (May 31 2020 at 09:55):

Indeed, the proof here looks very similar to BCT

#### Patrick Massot (May 31 2020 at 09:56):

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

#### Patrick Massot (May 31 2020 at 09:57):

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 (May 31 2020 at 10:11):

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 (May 31 2020 at 10:11):

for which sorry?

#### Kenny Lau (May 31 2020 at 10:12):

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

#### Kenny Lau (May 31 2020 at 10:12):

up to indexing error

#### Patrick Massot (May 31 2020 at 10:16):

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

#### Reid Barton (May 31 2020 at 11:22):

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
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 (May 31 2020 at 11:25):

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 (May 31 2020 at 11:26):

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

#### Patrick Massot (May 31 2020 at 12:03):

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 (May 31 2020 at 13:12):

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)