Use "if" condition within "then" output

Stream: new members

[Abhimanyu Pallavi Sudhir]

I'm trying to write something like this:

theorem bob (a : ℕ → ℝ) (rad : ℝ)
(
  hc : ∀ x, -rad < x ∧ x < rad → is_cau_seq abs (λ (n : ℕ), finset.sum (finset.range n) (λ (k : ℕ), a k * x ^ k))
)
(
  f : ℝ → ℝ := λ x,
  if (hr : - rad < x ∧ x < rad) then
    cau_seq.lim ((⟨λ n, (finset.range n).sum (λ k, a k * x ^ k) , (λ x, hc x hr)   ⟩) : cau_seq ℝ abs)
  else 0
)
: sorry

Of course, this doesn't work because I can only put a proposition in the if condition, not a proof -- but shouldn't there be some way of achieving this -- of referring to the condition for the if in the output for then?

French brackets don't work either because the condition isn't recorded as an assumption at all.

Is this where dite comes in?

[Reid Barton]

try deleting those parentheses?

[Reid Barton]

around hr : - rad < x ∧ x < rad