Theorem: exercise3_9 (LeanCourse/Assignments/Solutions/Solutions3.lean)

State before:
⊢ (fun x => x ^ 2) ⁻¹' {y | y ≥ 4} = {x | x ≤ -2} ∪ {x | x ≥ 2}
Tactic:
ext x
State after:
case h
x : ℝ
⊢ x ∈ (fun x => x ^ 2) ⁻¹' {y | y ≥ 4} ↔ x ∈ {x | x ≤ -2} ∪ {x | x ≥ 2}

State before:
case h
x : ℝ
⊢ x ∈ (fun x => x ^ 2) ⁻¹' {y | y ≥ 4} ↔ x ∈ {x | x ≤ -2} ∪ {x | x ≥ 2}
Tactic:
simp [show (4 : ℝ) = 2 ^ 2 by norm_num, sq_le_sq, le_abs']
State after:
no goals

State before:
x : ℝ
⊢ 4 = 2 ^ 2
Tactic:
norm_num
State after:
no goals