Theorem: mem_slitPlane_of_near_one (Ray/Misc/Bounds.lean)

State before:
z : ℂ
⊢ Complex.abs (z - 1) < 1 → z ∈ slitPlane
Tactic:
intro h
State after:
z : ℂ
h : Complex.abs (z - 1) < 1
⊢ z ∈ slitPlane

State before:
z : ℂ
h : Complex.abs (z - 1) < 1
⊢ z ∈ slitPlane
Tactic:
apply Or.inl
State after:
case h
z : ℂ
h : Complex.abs (z - 1) < 1
⊢ 0 < z.re

State before:
case h
z : ℂ
h : Complex.abs (z - 1) < 1
⊢ 0 < z.re
Tactic:
have hr : (1 - z).re < 1 := by
  calc
    (1 - z).re ≤ |(1 - z).re| := le_abs_self (1 - z).re
    _ ≤ abs (1 - z) := (Complex.abs_re_le_abs _)
    _ = abs (z - 1) := by rw [←Complex.abs.map_neg (1 - z)]; simp only [neg_sub]
    _ < 1 := h
State after:
case h
z : ℂ
h : Complex.abs (z - 1) < 1
hr : (1 - z).re < 1
⊢ 0 < z.re

State before:
case h
z : ℂ
h : Complex.abs (z - 1) < 1
hr : (1 - z).re < 1
⊢ 0 < z.re
Tactic:
simp only [Complex.sub_re, Complex.one_re, sub_lt_self_iff] at hr
State after:
case h
z : ℂ
h : Complex.abs (z - 1) < 1
hr : 0 < z.re
⊢ 0 < z.re

State before:
case h
z : ℂ
h : Complex.abs (z - 1) < 1
hr : 0 < z.re
⊢ 0 < z.re
Tactic:
assumption
State after:
no goals

State before:
z : ℂ
h : Complex.abs (z - 1) < 1
⊢ (1 - z).re < 1
Tactic:
calc
  (1 - z).re ≤ |(1 - z).re| := le_abs_self (1 - z).re
  _ ≤ abs (1 - z) := (Complex.abs_re_le_abs _)
  _ = abs (z - 1) := by rw [←Complex.abs.map_neg (1 - z)]; simp only [neg_sub]
  _ < 1 := h
State after:
no goals

State before:
z : ℂ
h : Complex.abs (z - 1) < 1
⊢ Complex.abs (1 - z) = Complex.abs (z - 1)
Tactic:
rw [←Complex.abs.map_neg (1 - z)]
State after:
z : ℂ
h : Complex.abs (z - 1) < 1
⊢ Complex.abs (-(1 - z)) = Complex.abs (z - 1)

State before:
z : ℂ
h : Complex.abs (z - 1) < 1
⊢ Complex.abs (-(1 - z)) = Complex.abs (z - 1)
Tactic:
simp only [neg_sub]
State after:
no goals