Theorem: HTPI.Example_3_5_4 (HTPILib/Chap3.lean)

State before:
x : ℝ
h1 : x ≤ x ^ 2
⊢ x ≤ 0 ∨ 1 ≤ x
Tactic:
or_right with h2
State after:
x : ℝ
h1 : x ≤ x ^ 2
h2 : ¬x ≤ 0
⊢ 1 ≤ x

State before:
x : ℝ
h1 : x ≤ x ^ 2
h2 : ¬x ≤ 0
⊢ 1 ≤ x
Tactic:
have h3 : 0 < x := lt_of_not_le h2
State after:
x : ℝ
h1 : x ≤ x ^ 2
h2 : ¬x ≤ 0
h3 : 0 < x
⊢ 1 ≤ x

State before:
x : ℝ
h1 : x ≤ x ^ 2
h2 : ¬x ≤ 0
h3 : 0 < x
⊢ 1 ≤ x
Tactic:
have h4 : 1 * x ≤ x * x :=
  calc 1 * x
    _ = x := one_mul x
    _ ≤ x ^ 2 := h1
    _ = x * x := by ring
State after:
x : ℝ
h1 : x ≤ x ^ 2
h2 : ¬x ≤ 0
h3 : 0 < x
h4 : 1 * x ≤ x * x
⊢ 1 ≤ x

State before:
x : ℝ
h1 : x ≤ x ^ 2
h2 : ¬x ≤ 0
h3 : 0 < x
h4 : 1 * x ≤ x * x
⊢ 1 ≤ x
Tactic:
show 1 ≤ x from le_of_mul_le_mul_right h4 h3
State after:
no goals

State before:
x : ℝ
h1 : x ≤ x ^ 2
h2 : ¬x ≤ 0
h3 : 0 < x
⊢ x ^ 2 = x * x
Tactic:
ring
State after:
no goals