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

State before:
x A : ℝ
⊢ IsGood x A ↔ √(2 * x - 1) + 1 + |√(2 * x - 1) - 1| = A * √2 ∧ 1 / 2 ≤ x
Tactic:
cases le_or_lt (1 / 2) x with
| inl hx =>
  have hx' : 0 ≤ 2 * x - 1 := by linarith
  have h₁ : x + sqrt (2 * x - 1) = (sqrt (2 * x - 1) + 1) ^ 2 / 2 := by
    rw [add_sq, sq_sqrt hx']; field_simp; ring
  have h₂ : x - sqrt (2 * x - 1) = (sqrt (2 * x - 1) - 1) ^ 2 / 2 := by
    rw [sub_sq, sq_sqrt hx']; field_simp; ring
  simp only [IsGood, *, div_nonneg (sq_nonneg _) (zero_le_two (α := ℝ)), sqrt_div (sq_nonneg _),
    and_true]
  rw [sqrt_sq, sqrt_sq_eq_abs] <;> [skip; positivity]
  field_simp
| inr hx =>
  have : 2 * x - 1 < 0 := by linarith
  simp only [IsGood, this.not_le, hx.not_le]; simp
State after:
no goals

State before:
case inl
x A : ℝ
hx : 1 / 2 ≤ x
⊢ IsGood x A ↔ √(2 * x - 1) + 1 + |√(2 * x - 1) - 1| = A * √2 ∧ 1 / 2 ≤ x
Tactic:
have hx' : 0 ≤ 2 * x - 1 := by linarith
State after:
case inl
x A : ℝ
hx : 1 / 2 ≤ x
hx' : 0 ≤ 2 * x - 1
⊢ IsGood x A ↔ √(2 * x - 1) + 1 + |√(2 * x - 1) - 1| = A * √2 ∧ 1 / 2 ≤ x

State before:
case inl
x A : ℝ
hx : 1 / 2 ≤ x
hx' : 0 ≤ 2 * x - 1
⊢ IsGood x A ↔ √(2 * x - 1) + 1 + |√(2 * x - 1) - 1| = A * √2 ∧ 1 / 2 ≤ x
Tactic:
have h₁ : x + sqrt (2 * x - 1) = (sqrt (2 * x - 1) + 1) ^ 2 / 2 := by
  rw [add_sq, sq_sqrt hx']; field_simp; ring
State after:
case inl
x A : ℝ
hx : 1 / 2 ≤ x
hx' : 0 ≤ 2 * x - 1
h₁ : x + √(2 * x - 1) = (√(2 * x - 1) + 1) ^ 2 / 2
⊢ IsGood x A ↔ √(2 * x - 1) + 1 + |√(2 * x - 1) - 1| = A * √2 ∧ 1 / 2 ≤ x

State before:
case inl
x A : ℝ
hx : 1 / 2 ≤ x
hx' : 0 ≤ 2 * x - 1
h₁ : x + √(2 * x - 1) = (√(2 * x - 1) + 1) ^ 2 / 2
⊢ IsGood x A ↔ √(2 * x - 1) + 1 + |√(2 * x - 1) - 1| = A * √2 ∧ 1 / 2 ≤ x
Tactic:
have h₂ : x - sqrt (2 * x - 1) = (sqrt (2 * x - 1) - 1) ^ 2 / 2 := by
  rw [sub_sq, sq_sqrt hx']; field_simp; ring
State after:
case inl
x A : ℝ
hx : 1 / 2 ≤ x
hx' : 0 ≤ 2 * x - 1
h₁ : x + √(2 * x - 1) = (√(2 * x - 1) + 1) ^ 2 / 2
h₂ : x - √(2 * x - 1) = (√(2 * x - 1) - 1) ^ 2 / 2
⊢ IsGood x A ↔ √(2 * x - 1) + 1 + |√(2 * x - 1) - 1| = A * √2 ∧ 1 / 2 ≤ x

State before:
case inl
x A : ℝ
hx : 1 / 2 ≤ x
hx' : 0 ≤ 2 * x - 1
h₁ : x + √(2 * x - 1) = (√(2 * x - 1) + 1) ^ 2 / 2
h₂ : x - √(2 * x - 1) = (√(2 * x - 1) - 1) ^ 2 / 2
⊢ IsGood x A ↔ √(2 * x - 1) + 1 + |√(2 * x - 1) - 1| = A * √2 ∧ 1 / 2 ≤ x
Tactic:
simp only [IsGood, *, div_nonneg (sq_nonneg _) (zero_le_two (α := ℝ)), sqrt_div (sq_nonneg _),
  and_true]
State after:
case inl
x A : ℝ
hx : 1 / 2 ≤ x
hx' : 0 ≤ 2 * x - 1
h₁ : x + √(2 * x - 1) = (√(2 * x - 1) + 1) ^ 2 / 2
h₂ : x - √(2 * x - 1) = (√(2 * x - 1) - 1) ^ 2 / 2
⊢ √((√(2 * x - 1) + 1) ^ 2) / √2 + √((√(2 * x - 1) - 1) ^ 2) / √2 = A ↔ √(2 * x - 1) + 1 + |√(2 * x - 1) - 1| = A * √2

State before:
case inl
x A : ℝ
hx : 1 / 2 ≤ x
hx' : 0 ≤ 2 * x - 1
h₁ : x + √(2 * x - 1) = (√(2 * x - 1) + 1) ^ 2 / 2
h₂ : x - √(2 * x - 1) = (√(2 * x - 1) - 1) ^ 2 / 2
⊢ √((√(2 * x - 1) + 1) ^ 2) / √2 + √((√(2 * x - 1) - 1) ^ 2) / √2 = A ↔ √(2 * x - 1) + 1 + |√(2 * x - 1) - 1| = A * √2
Tactic:
rw [sqrt_sq, sqrt_sq_eq_abs] <;> [skip; positivity]
State after:
case inl
x A : ℝ
hx : 1 / 2 ≤ x
hx' : 0 ≤ 2 * x - 1
h₁ : x + √(2 * x - 1) = (√(2 * x - 1) + 1) ^ 2 / 2
h₂ : x - √(2 * x - 1) = (√(2 * x - 1) - 1) ^ 2 / 2
⊢ (√(2 * x - 1) + 1) / √2 + |√(2 * x - 1) - 1| / √2 = A ↔ √(2 * x - 1) + 1 + |√(2 * x - 1) - 1| = A * √2

State before:
case inl
x A : ℝ
hx : 1 / 2 ≤ x
hx' : 0 ≤ 2 * x - 1
h₁ : x + √(2 * x - 1) = (√(2 * x - 1) + 1) ^ 2 / 2
h₂ : x - √(2 * x - 1) = (√(2 * x - 1) - 1) ^ 2 / 2
⊢ (√(2 * x - 1) + 1) / √2 + |√(2 * x - 1) - 1| / √2 = A ↔ √(2 * x - 1) + 1 + |√(2 * x - 1) - 1| = A * √2
Tactic:
field_simp
State after:
no goals

State before:
x A : ℝ
hx : 1 / 2 ≤ x
⊢ 0 ≤ 2 * x - 1
Tactic:
linarith
State after:
no goals

State before:
x A : ℝ
hx : 1 / 2 ≤ x
hx' : 0 ≤ 2 * x - 1
⊢ x + √(2 * x - 1) = (√(2 * x - 1) + 1) ^ 2 / 2
Tactic:
rw [add_sq, sq_sqrt hx']
State after:
x A : ℝ
hx : 1 / 2 ≤ x
hx' : 0 ≤ 2 * x - 1
⊢ x + √(2 * x - 1) = (2 * x - 1 + 2 * √(2 * x - 1) * 1 + 1 ^ 2) / 2

State before:
x A : ℝ
hx : 1 / 2 ≤ x
hx' : 0 ≤ 2 * x - 1
⊢ x + √(2 * x - 1) = (2 * x - 1 + 2 * √(2 * x - 1) * 1 + 1 ^ 2) / 2
Tactic:
field_simp
State after:
x A : ℝ
hx : 1 / 2 ≤ x
hx' : 0 ≤ 2 * x - 1
⊢ (x + √(2 * x - 1)) * 2 = 2 * x - 1 + 2 * √(2 * x - 1) + 1

State before:
x A : ℝ
hx : 1 / 2 ≤ x
hx' : 0 ≤ 2 * x - 1
⊢ (x + √(2 * x - 1)) * 2 = 2 * x - 1 + 2 * √(2 * x - 1) + 1
Tactic:
ring
State after:
no goals

State before:
x A : ℝ
hx : 1 / 2 ≤ x
hx' : 0 ≤ 2 * x - 1
h₁ : x + √(2 * x - 1) = (√(2 * x - 1) + 1) ^ 2 / 2
⊢ x - √(2 * x - 1) = (√(2 * x - 1) - 1) ^ 2 / 2
Tactic:
rw [sub_sq, sq_sqrt hx']
State after:
x A : ℝ
hx : 1 / 2 ≤ x
hx' : 0 ≤ 2 * x - 1
h₁ : x + √(2 * x - 1) = (√(2 * x - 1) + 1) ^ 2 / 2
⊢ x - √(2 * x - 1) = (2 * x - 1 - 2 * √(2 * x - 1) * 1 + 1 ^ 2) / 2

State before:
x A : ℝ
hx : 1 / 2 ≤ x
hx' : 0 ≤ 2 * x - 1
h₁ : x + √(2 * x - 1) = (√(2 * x - 1) + 1) ^ 2 / 2
⊢ x - √(2 * x - 1) = (2 * x - 1 - 2 * √(2 * x - 1) * 1 + 1 ^ 2) / 2
Tactic:
field_simp
State after:
x A : ℝ
hx : 1 / 2 ≤ x
hx' : 0 ≤ 2 * x - 1
h₁ : x + √(2 * x - 1) = (√(2 * x - 1) + 1) ^ 2 / 2
⊢ (x - √(2 * x - 1)) * 2 = 2 * x - 1 - 2 * √(2 * x - 1) + 1

State before:
x A : ℝ
hx : 1 / 2 ≤ x
hx' : 0 ≤ 2 * x - 1
h₁ : x + √(2 * x - 1) = (√(2 * x - 1) + 1) ^ 2 / 2
⊢ (x - √(2 * x - 1)) * 2 = 2 * x - 1 - 2 * √(2 * x - 1) + 1
Tactic:
ring
State after:
no goals

State before:
case inr
x A : ℝ
hx : x < 1 / 2
⊢ IsGood x A ↔ √(2 * x - 1) + 1 + |√(2 * x - 1) - 1| = A * √2 ∧ 1 / 2 ≤ x
Tactic:
have : 2 * x - 1 < 0 := by linarith
State after:
case inr
x A : ℝ
hx : x < 1 / 2
this : 2 * x - 1 < 0
⊢ IsGood x A ↔ √(2 * x - 1) + 1 + |√(2 * x - 1) - 1| = A * √2 ∧ 1 / 2 ≤ x

State before:
case inr
x A : ℝ
hx : x < 1 / 2
this : 2 * x - 1 < 0
⊢ IsGood x A ↔ √(2 * x - 1) + 1 + |√(2 * x - 1) - 1| = A * √2 ∧ 1 / 2 ≤ x
Tactic:
simp only [IsGood, this.not_le, hx.not_le]
State after:
case inr
x A : ℝ
hx : x < 1 / 2
this : 2 * x - 1 < 0
⊢ √(x + √(2 * x - 1)) + √(x - √(2 * x - 1)) = A ∧ False ∧ 0 ≤ x + √(2 * x - 1) ∧ 0 ≤ x - √(2 * x - 1) ↔
    √(2 * x - 1) + 1 + |√(2 * x - 1) - 1| = A * √2 ∧ False

State before:
case inr
x A : ℝ
hx : x < 1 / 2
this : 2 * x - 1 < 0
⊢ √(x + √(2 * x - 1)) + √(x - √(2 * x - 1)) = A ∧ False ∧ 0 ≤ x + √(2 * x - 1) ∧ 0 ≤ x - √(2 * x - 1) ↔
    √(2 * x - 1) + 1 + |√(2 * x - 1) - 1| = A * √2 ∧ False
Tactic:
simp
State after:
no goals

State before:
x A : ℝ
hx : x < 1 / 2
⊢ 2 * x - 1 < 0
Tactic:
linarith
State after:
no goals