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

State before:
x A : ℝ
hx : x ∈ Icc (1 / 2) 1
⊢ IsGood x A ↔ A = √2
Tactic:
have : sqrt (2 * x - 1) ≤ 1 := sqrt_two_mul_sub_one_le_one.2 hx.2
State after:
x A : ℝ
hx : x ∈ Icc (1 / 2) 1
this : √(2 * x - 1) ≤ 1
⊢ IsGood x A ↔ A = √2

State before:
x A : ℝ
hx : x ∈ Icc (1 / 2) 1
this : √(2 * x - 1) ≤ 1
⊢ IsGood x A ↔ A = √2
Tactic:
simp only [isGood_iff, hx.1, abs_sub_comm _ (1 : ℝ), abs_of_nonneg (sub_nonneg.2 this), and_true]
State after:
x A : ℝ
hx : x ∈ Icc (1 / 2) 1
this : √(2 * x - 1) ≤ 1
⊢ √(2 * x - 1) + 1 + (1 - √(2 * x - 1)) = A * √2 ↔ A = √2

State before:
x A : ℝ
hx : x ∈ Icc (1 / 2) 1
this : √(2 * x - 1) ≤ 1
⊢ √(2 * x - 1) + 1 + (1 - √(2 * x - 1)) = A * √2 ↔ A = √2
Tactic:
suffices 2 = A * sqrt 2 ↔ A = sqrt 2 by convert this using 2; ring
State after:
x A : ℝ
hx : x ∈ Icc (1 / 2) 1
this : √(2 * x - 1) ≤ 1
⊢ 2 = A * √2 ↔ A = √2

State before:
x A : ℝ
hx : x ∈ Icc (1 / 2) 1
this : √(2 * x - 1) ≤ 1
⊢ 2 = A * √2 ↔ A = √2
Tactic:
rw [← div_eq_iff, div_sqrt, eq_comm]
State after:
x A : ℝ
hx : x ∈ Icc (1 / 2) 1
this : √(2 * x - 1) ≤ 1
⊢ √2 ≠ 0

State before:
x A : ℝ
hx : x ∈ Icc (1 / 2) 1
this : √(2 * x - 1) ≤ 1
⊢ √2 ≠ 0
Tactic:
positivity
State after:
no goals

State before:
x A : ℝ
hx : x ∈ Icc (1 / 2) 1
this✝ : √(2 * x - 1) ≤ 1
this : 2 = A * √2 ↔ A = √2
⊢ √(2 * x - 1) + 1 + (1 - √(2 * x - 1)) = A * √2 ↔ A = √2
Tactic:
convert this using 2
State after:
case h.e'_1.h.e'_2
x A : ℝ
hx : x ∈ Icc (1 / 2) 1
this✝ : √(2 * x - 1) ≤ 1
this : 2 = A * √2 ↔ A = √2
⊢ √(2 * x - 1) + 1 + (1 - √(2 * x - 1)) = 2

State before:
case h.e'_1.h.e'_2
x A : ℝ
hx : x ∈ Icc (1 / 2) 1
this✝ : √(2 * x - 1) ≤ 1
this : 2 = A * √2 ↔ A = √2
⊢ √(2 * x - 1) + 1 + (1 - √(2 * x - 1)) = 2
Tactic:
ring
State after:
no goals