How can do "rcases" on a (not computable?) exists statement

Stream: maths

[Kent Van Vels]

I am trying to show that the termwise product of two Cauchy sequences of ratioanl numbers is a Cauchy sequence. A standard part of the proof is a lemma that a Cauchy sequence is bounded, i.e. there exists a constant $M\in \mathbb{Q}$ such that for all $n\in \mathbb{N}$ we have $|u_n| \le M$. I can do this part fine. But I can't the extract the upper bound using rcases or anything else I have tried. What follows is my Minimal (non) Working example.

import tactic
abbreviation seqQ :=  ℕ → ℚ

def isCauchy : seqQ → Prop :=
begin
  intro u,
  exact (∀ (ε : ℚ) (ε_pos : 0 < ε), ∃ N : ℕ, ∀ (n ≥ N) (m ≥ N), abs (u n - u m) ≤ ε )
end

namespace cauchyQ

lemma cauchy_sequences_bounded (u0 : seqQ) (h1 : isCauchy u0) :
 ∃ (M : ℚ), ∀ n : ℕ, |u0 n| ≤ M := sorry

structure cauchyQ :=
mk :: (z : seqQ) (h1 : isCauchy z)

protected def mul : cauchyQ → cauchyQ →  cauchyQ :=
begin
  rintros ⟨az,ha⟩ ⟨bz,hb⟩,
  have hMA := (cauchy_sequences_bounded az ha),
  --I want to exact the maximum in the next line and use.
  --I suspect it won't let me because the upper_bound isn't computable,
--but I don't really know.
  rcases hMA with ⟨upper_bound_of_az, hMA⟩,
end

end cauchyQ

I appreciate any help.

[Mario Carneiro]

You should construct the sequence before extracting the max

[Mario Carneiro]

you can use rcases to extract the max only in the proof of isCauchy

[Kent Van Vels]

Ok, i think i found a previous conversation that also ran into this. I will report back. I think I understand it.

[Kent Van Vels]

It is working. I really appreciate the help.