Theorem: k_of_abs_le_one (Carleson/Theorem1_1/Hilbert_kernel.lean)

State before:
x : ℝ
abs_le_one : |x| ≤ 1
⊢ k x = (1 - ↑|x|) / (1 - (Complex.I * ↑x).exp)
Tactic:
rw [k, max_eq_left (by linarith)]
State after:
x : ℝ
abs_le_one : |x| ≤ 1
⊢ ↑(1 - |x|) / (1 - (Complex.I * ↑x).exp) = (1 - ↑|x|) / (1 - (Complex.I * ↑x).exp)

State before:
x : ℝ
abs_le_one : |x| ≤ 1
⊢ ↑(1 - |x|) / (1 - (Complex.I * ↑x).exp) = (1 - ↑|x|) / (1 - (Complex.I * ↑x).exp)
Tactic:
norm_cast
State after:
no goals

State before:
x : ℝ
abs_le_one : |x| ≤ 1
⊢ 0 ≤ 1 - |x|
Tactic:
linarith
State after:
no goals