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

State before:
x A : ℝ
hA : √2 < A
⊢ IsGood x A ↔ x = (A / 2) ^ 2 + 1 / 2
Tactic:
have : 0 < A := lt_trans (by simp) hA
State after:
x A : ℝ
hA : √2 < A
this : 0 < A
⊢ IsGood x A ↔ x = (A / 2) ^ 2 + 1 / 2

State before:
x A : ℝ
hA : √2 < A
this : 0 < A
⊢ IsGood x A ↔ x = (A / 2) ^ 2 + 1 / 2
Tactic:
constructor
State after:
case mp
x A : ℝ
hA : √2 < A
this : 0 < A
⊢ IsGood x A → x = (A / 2) ^ 2 + 1 / 2

case mpr
x A : ℝ
hA : √2 < A
this : 0 < A
⊢ x = (A / 2) ^ 2 + 1 / 2 → IsGood x A

State before:
x A : ℝ
hA : √2 < A
⊢ 0 < √2
Tactic:
simp
State after:
no goals

State before:
case mp
x A : ℝ
hA : √2 < A
this : 0 < A
⊢ IsGood x A → x = (A / 2) ^ 2 + 1 / 2
Tactic:
intro h
State after:
case mp
x A : ℝ
hA : √2 < A
this : 0 < A
h : IsGood x A
⊢ x = (A / 2) ^ 2 + 1 / 2

State before:
case mp
x A : ℝ
hA : √2 < A
this : 0 < A
h : IsGood x A
⊢ x = (A / 2) ^ 2 + 1 / 2
Tactic:
have hx : 1 < x := by rwa [h.sqrt_two_lt_iff_one_lt] at hA
State after:
case mp
x A : ℝ
hA : √2 < A
this : 0 < A
h : IsGood x A
hx : 1 < x
⊢ x = (A / 2) ^ 2 + 1 / 2

State before:
case mp
x A : ℝ
hA : √2 < A
this : 0 < A
h : IsGood x A
hx : 1 < x
⊢ x = (A / 2) ^ 2 + 1 / 2
Tactic:
rw [isGood_iff_eq_sqrt hx, eq_comm, sqrt_eq_iff_sq_eq] at h <;> linarith
State after:
no goals

State before:
x A : ℝ
hA : √2 < A
this : 0 < A
h : IsGood x A
⊢ 1 < x
Tactic:
rwa [h.sqrt_two_lt_iff_one_lt] at hA
State after:
no goals

State before:
case mpr
x A : ℝ
hA : √2 < A
this : 0 < A
⊢ x = (A / 2) ^ 2 + 1 / 2 → IsGood x A
Tactic:
rintro rfl
State after:
case mpr
A : ℝ
hA : √2 < A
this : 0 < A
⊢ IsGood ((A / 2) ^ 2 + 1 / 2) A

State before:
case mpr
A : ℝ
hA : √2 < A
this : 0 < A
⊢ IsGood ((A / 2) ^ 2 + 1 / 2) A
Tactic:
rw [isGood_iff_eq_sqrt]
State after:
case mpr
A : ℝ
hA : √2 < A
this : 0 < A
⊢ A = √(4 * ((A / 2) ^ 2 + 1 / 2) - 2)

case mpr
A : ℝ
hA : √2 < A
this : 0 < A
⊢ 1 < (A / 2) ^ 2 + 1 / 2

State before:
case mpr
A : ℝ
hA : √2 < A
this : 0 < A
⊢ A = √(4 * ((A / 2) ^ 2 + 1 / 2) - 2)
Tactic:
conv_lhs => rw [← sqrt_sq this.le]
State after:
case mpr
A : ℝ
hA : √2 < A
this : 0 < A
⊢ √(A ^ 2) = √(4 * ((A / 2) ^ 2 + 1 / 2) - 2)

State before:
case mpr
A : ℝ
hA : √2 < A
this : 0 < A
⊢ √(A ^ 2) = √(4 * ((A / 2) ^ 2 + 1 / 2) - 2)
Tactic:
ring_nf
State after:
no goals

State before:
case mpr
A : ℝ
hA : √2 < A
this : 0 < A
⊢ 1 < (A / 2) ^ 2 + 1 / 2
Tactic:
rw [sqrt_lt' this] at hA
State after:
case mpr
A : ℝ
hA : 2 < A ^ 2
this : 0 < A
⊢ 1 < (A / 2) ^ 2 + 1 / 2

State before:
case mpr
A : ℝ
hA : 2 < A ^ 2
this : 0 < A
⊢ 1 < (A / 2) ^ 2 + 1 / 2
Tactic:
linarith
State after:
no goals