Theorem: Real.abs_le_of_sqrt_sq_add_nonneg_le (CvxLean/Lib/Math/Data/Real.lean)

State before:
a b c : ℝ
hb : 0 ≤ b
h : (a ^ 2 + b).sqrt ≤ c
⊢ |a| ≤ c
Tactic:
rw [sqrt_le_iff] at h
State after:
a b c : ℝ
hb : 0 ≤ b
h : 0 ≤ c ∧ a ^ 2 + b ≤ c ^ 2
⊢ |a| ≤ c

State before:
a b c : ℝ
hb : 0 ≤ b
h : 0 ≤ c ∧ a ^ 2 + b ≤ c ^ 2
⊢ |a| ≤ c
Tactic:
replace ⟨hc, h⟩ := h
State after:
a b c : ℝ
hb : 0 ≤ b
hc : 0 ≤ c
h : a ^ 2 + b ≤ c ^ 2
⊢ |a| ≤ c

State before:
a b c : ℝ
hb : 0 ≤ b
hc : 0 ≤ c
h : a ^ 2 + b ≤ c ^ 2
⊢ |a| ≤ c
Tactic:
replace h := le_trans (le_add_of_nonneg_right hb) h
State after:
a b c : ℝ
hb : 0 ≤ b
hc : 0 ≤ c
h : a ^ 2 ≤ c ^ 2
⊢ |a| ≤ c

State before:
a b c : ℝ
hb : 0 ≤ b
hc : 0 ≤ c
h : a ^ 2 ≤ c ^ 2
⊢ |a| ≤ c
Tactic:
rwa [rpow_two, sq_le_sq, abs_of_nonneg hc] at h
State after:
no goals