[GOAL]
z w : ℂ
⊢ z < w ↔ z ≤ w ∧ ¬w ≤ z
[PROOFSTEP]
dsimp
[GOAL]
z w : ℂ
⊢ z.re < w.re ∧ z.im = w.im ↔ (z.re ≤ w.re ∧ z.im = w.im) ∧ ¬(w.re ≤ z.re ∧ w.im = z.im)
[PROOFSTEP]
rw [lt_iff_le_not_le]
[GOAL]
z w : ℂ
⊢ (z.re ≤ w.re ∧ ¬w.re ≤ z.re) ∧ z.im = w.im ↔ (z.re ≤ w.re ∧ z.im = w.im) ∧ ¬(w.re ≤ z.re ∧ w.im = z.im)
[PROOFSTEP]
tauto
[GOAL]
x y : ℝ
⊢ ↑x ≤ ↑y ↔ x ≤ y
[PROOFSTEP]
simp [le_def, ofReal']
[GOAL]
x y : ℝ
⊢ ↑x < ↑y ↔ x < y
[PROOFSTEP]
simp [lt_def, ofReal']
[GOAL]
z w : ℂ
⊢ ¬z ≤ w ↔ w.re < z.re ∨ z.im ≠ w.im
[PROOFSTEP]
rw [le_def, not_and_or, not_le]
[GOAL]
z w : ℂ
⊢ ¬z < w ↔ w.re ≤ z.re ∨ z.im ≠ w.im
[PROOFSTEP]
rw [lt_def, not_and_or, not_lt]
[GOAL]
r : ℝ
z : ℂ
hz : ↑r ≤ z
⊢ z = ↑z.re
[PROOFSTEP]
ext
[GOAL]
case a
r : ℝ
z : ℂ
hz : ↑r ≤ z
⊢ z.re = (↑z.re).re
case a r : ℝ z : ℂ hz : ↑r ≤ z ⊢ z.im = (↑z.re).im
[PROOFSTEP]
rfl
[GOAL]
case a
r : ℝ
z : ℂ
hz : ↑r ≤ z
⊢ z.im = (↑z.re).im
[PROOFSTEP]
simp only [← (Complex.le_def.1 hz).2, Complex.zero_im, Complex.ofReal_im]
