Theorem: Imo1959P2.IsGood.sqrt_two_lt_of_one_lt (Compfiles/Imo1959P2.lean)

State before:
x A : ℝ
h : IsGood x A
hx : 1 < x
⊢ √2 < A
Tactic:
rw [(isGood_iff_eq_sqrt hx).1 h]
State after:
x A : ℝ
h : IsGood x A
hx : 1 < x
⊢ √2 < √(4 * x - 2)

State before:
x A : ℝ
h : IsGood x A
hx : 1 < x
⊢ √2 < √(4 * x - 2)
Tactic:
refine sqrt_lt_sqrt zero_le_two ?_
State after:
x A : ℝ
h : IsGood x A
hx : 1 < x
⊢ 2 < 4 * x - 2

State before:
x A : ℝ
h : IsGood x A
hx : 1 < x
⊢ 2 < 4 * x - 2
Tactic:
linarith
State after:
no goals