Theorem: sqrt17 (meetings/ex1.lean)

State before:
⊢ {x | x ^ 2 = 17} = {Real.sqrt 17, -Real.sqrt 17}
Tactic:
ext x
State after:
case h
x : ℝ
⊢ x ∈ {x | x ^ 2 = 17} ↔ x ∈ {Real.sqrt 17, -Real.sqrt 17}

State before:
case h
x : ℝ
⊢ x ∈ {x | x ^ 2 = 17} ↔ x ∈ {Real.sqrt 17, -Real.sqrt 17}
Tactic:
simp
State after:
case h
x : ℝ
⊢ x ^ 2 = 17 ↔ x = Real.sqrt 17 ∨ x = -Real.sqrt 17

State before:
case h
x : ℝ
⊢ x ^ 2 = 17 ↔ x = Real.sqrt 17 ∨ x = -Real.sqrt 17
Tactic:
constructor
State after:
case h.mp
x : ℝ
⊢ x ^ 2 = 17 → x = Real.sqrt 17 ∨ x = -Real.sqrt 17

case h.mpr
x : ℝ
⊢ x = Real.sqrt 17 ∨ x = -Real.sqrt 17 → x ^ 2 = 17

State before:
case h.mp
x : ℝ
⊢ x ^ 2 = 17 → x = Real.sqrt 17 ∨ x = -Real.sqrt 17
Tactic:
intro hsq
State after:
case h.mp
x : ℝ
hsq : x ^ 2 = 17
⊢ x = Real.sqrt 17 ∨ x = -Real.sqrt 17

State before:
case h.mp
x : ℝ
hsq : x ^ 2 = 17
⊢ x = Real.sqrt 17 ∨ x = -Real.sqrt 17
Tactic:
apply_fun (λ eq => Real.sqrt eq) at hsq
State after:
case h.mp
x : ℝ
hsq : Real.sqrt (x ^ 2) = Real.sqrt 17
⊢ x = Real.sqrt 17 ∨ x = -Real.sqrt 17

State before:
case h.mp
x : ℝ
hsq : Real.sqrt (x ^ 2) = Real.sqrt 17
⊢ x = Real.sqrt 17 ∨ x = -Real.sqrt 17
Tactic:
rw [Real.sqrt_sq_eq_abs] at hsq
State after:
case h.mp
x : ℝ
hsq : |x| = Real.sqrt 17
⊢ x = Real.sqrt 17 ∨ x = -Real.sqrt 17

State before:
case h.mp
x : ℝ
hsq : |x| = Real.sqrt 17
⊢ x = Real.sqrt 17 ∨ x = -Real.sqrt 17
Tactic:
exact eq_or_eq_neg_of_abs_eq hsq
State after:
no goals

State before:
case h.mpr
x : ℝ
⊢ x = Real.sqrt 17 ∨ x = -Real.sqrt 17 → x ^ 2 = 17
Tactic:
intro hor
State after:
case h.mpr
x : ℝ
hor : x = Real.sqrt 17 ∨ x = -Real.sqrt 17
⊢ x ^ 2 = 17

State before:
case h.mpr
x : ℝ
hor : x = Real.sqrt 17 ∨ x = -Real.sqrt 17
⊢ x ^ 2 = 17
Tactic:
rcases hor with (hpos | hneg)
State after:
case h.mpr.inl
x : ℝ
hpos : x = Real.sqrt 17
⊢ x ^ 2 = 17

case h.mpr.inr
x : ℝ
hneg : x = -Real.sqrt 17
⊢ x ^ 2 = 17

State before:
case h.mpr.inl
x : ℝ
hpos : x = Real.sqrt 17
⊢ x ^ 2 = 17
Tactic:
rw [hpos]
State after:
case h.mpr.inl
x : ℝ
hpos : x = Real.sqrt 17
⊢ Real.sqrt 17 ^ 2 = 17

State before:
case h.mpr.inl
x : ℝ
hpos : x = Real.sqrt 17
⊢ Real.sqrt 17 ^ 2 = 17
Tactic:
exact Real.sq_sqrt (by norm_num)
State after:
no goals

State before:
x : ℝ
hpos : x = Real.sqrt 17
⊢ 0 ≤ 17
Tactic:
norm_num
State after:
no goals

State before:
case h.mpr.inr
x : ℝ
hneg : x = -Real.sqrt 17
⊢ x ^ 2 = 17
Tactic:
rw [hneg, neg_sq]
State after:
case h.mpr.inr
x : ℝ
hneg : x = -Real.sqrt 17
⊢ Real.sqrt 17 ^ 2 = 17

State before:
case h.mpr.inr
x : ℝ
hneg : x = -Real.sqrt 17
⊢ Real.sqrt 17 ^ 2 = 17
Tactic:
exact Real.sq_sqrt (by norm_num)
State after:
no goals

State before:
x : ℝ
hneg : x = -Real.sqrt 17
⊢ 0 ≤ 17
Tactic:
norm_num
State after:
no goals