Theorem: Imo1959P2.isGood_iff_eq_sqrt (Compfiles/Imo1959P2.lean)

State before:
x A : ℝ
hx : 1 < x
⊢ IsGood x A ↔ A = √(4 * x - 2)
Tactic:
have h₁ : 1 < sqrt (2 * x - 1) := by simpa only [← not_le, sqrt_two_mul_sub_one_le_one] using hx
State after:
x A : ℝ
hx : 1 < x
h₁ : 1 < √(2 * x - 1)
⊢ IsGood x A ↔ A = √(4 * x - 2)

State before:
x A : ℝ
hx : 1 < x
h₁ : 1 < √(2 * x - 1)
⊢ IsGood x A ↔ A = √(4 * x - 2)
Tactic:
have h₂ : 1 / 2 ≤ x := by linarith
State after:
x A : ℝ
hx : 1 < x
h₁ : 1 < √(2 * x - 1)
h₂ : 1 / 2 ≤ x
⊢ IsGood x A ↔ A = √(4 * x - 2)

State before:
x A : ℝ
hx : 1 < x
h₁ : 1 < √(2 * x - 1)
h₂ : 1 / 2 ≤ x
⊢ IsGood x A ↔ A = √(4 * x - 2)
Tactic:
simp only [isGood_iff, h₂, abs_of_pos (sub_pos.2 h₁), add_add_sub_cancel, and_true]
State after:
x A : ℝ
hx : 1 < x
h₁ : 1 < √(2 * x - 1)
h₂ : 1 / 2 ≤ x
⊢ √(2 * x - 1) + √(2 * x - 1) = A * √2 ↔ A = √(4 * x - 2)

State before:
x A : ℝ
hx : 1 < x
h₁ : 1 < √(2 * x - 1)
h₂ : 1 / 2 ≤ x
⊢ √(2 * x - 1) + √(2 * x - 1) = A * √2 ↔ A = √(4 * x - 2)
Tactic:
rw [← mul_two, ← div_eq_iff (by positivity), mul_div_assoc, div_sqrt, ← sqrt_mul' _ zero_le_two,
  eq_comm]
State after:
x A : ℝ
hx : 1 < x
h₁ : 1 < √(2 * x - 1)
h₂ : 1 / 2 ≤ x
⊢ A = √((2 * x - 1) * 2) ↔ A = √(4 * x - 2)

State before:
x A : ℝ
hx : 1 < x
h₁ : 1 < √(2 * x - 1)
h₂ : 1 / 2 ≤ x
⊢ A = √((2 * x - 1) * 2) ↔ A = √(4 * x - 2)
Tactic:
ring_nf
State after:
no goals

State before:
x A : ℝ
hx : 1 < x
⊢ 1 < √(2 * x - 1)
Tactic:
simpa only [← not_le, sqrt_two_mul_sub_one_le_one] using hx
State after:
no goals

State before:
x A : ℝ
hx : 1 < x
h₁ : 1 < √(2 * x - 1)
⊢ 1 / 2 ≤ x
Tactic:
linarith
State after:
no goals

State before:
x A : ℝ
hx : 1 < x
h₁ : 1 < √(2 * x - 1)
h₂ : 1 / 2 ≤ x
⊢ √2 ≠ 0
Tactic:
positivity
State after:
no goals