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

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

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

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