case mk
x y : ℝ
⊢ ↑abs { re := x, im := y } ≤ Real.sqrt 2 * max (Abs.abs { re := x, im := y }.re) (Abs.abs { re := x, im := y }.im)
z : ℂ
⊢ ↑abs z ≤ Real.sqrt 2 * max (Abs.abs z.re) (Abs.abs z.im)
cases' z with x y
case mk
x y : ℝ
⊢ Real.sqrt (x ^ 2 + y ^ 2) ≤ Real.sqrt 2 * max (Abs.abs x) (Abs.abs y)
case mk
x y : ℝ
⊢ ↑abs { re := x, im := y } ≤ Real.sqrt 2 * max (Abs.abs { re := x, im := y }.re) (Abs.abs { re := x, im := y }.im)
simp only [abs_apply, normSq_mk, ← sq]
case pos
x y : ℝ
hle : Abs.abs x ≤ Abs.abs y
⊢ Real.sqrt (x ^ 2 + y ^ 2) ≤ Real.sqrt 2 * max (Abs.abs x) (Abs.abs y)

case neg
x y : ℝ
hle : ¬Abs.abs x ≤ Abs.abs y
⊢ Real.sqrt (x ^ 2 + y ^ 2) ≤ Real.sqrt 2 * max (Abs.abs x) (Abs.abs y)
case mk
x y : ℝ
⊢ Real.sqrt (x ^ 2 + y ^ 2) ≤ Real.sqrt 2 * max (Abs.abs x) (Abs.abs y)
by_cases hle : |x| ≤ |y|
no goals
case pos
x y : ℝ
hle : Abs.abs x ≤ Abs.abs y
⊢ Real.sqrt (x ^ 2 + y ^ 2) ≤ Real.sqrt 2 * max (Abs.abs x) (Abs.abs y)
calc
  Real.sqrt (x ^ 2 + y ^ 2) ≤ Real.sqrt (y ^ 2 + y ^ 2) :=
    Real.sqrt_le_sqrt (add_le_add_right (sq_le_sq.2 hle) _)
  _ = Real.sqrt 2 * max (|x|) (|y|) := by
    rw [max_eq_right hle, ← two_mul, Real.sqrt_mul two_pos.le, Real.sqrt_sq_eq_abs]
no goals
x y : ℝ
hle : Abs.abs x ≤ Abs.abs y
⊢ Real.sqrt (y ^ 2 + y ^ 2) = Real.sqrt 2 * max (Abs.abs x) (Abs.abs y)
rw [max_eq_right hle, ← two_mul, Real.sqrt_mul two_pos.le, Real.sqrt_sq_eq_abs]
case neg
x y : ℝ
hle : ¬Abs.abs x ≤ Abs.abs y
hle' : Abs.abs y ≤ Abs.abs x
⊢ Real.sqrt (x ^ 2 + y ^ 2) ≤ Real.sqrt 2 * max (Abs.abs x) (Abs.abs y)
case neg
x y : ℝ
hle : ¬Abs.abs x ≤ Abs.abs y
⊢ Real.sqrt (x ^ 2 + y ^ 2) ≤ Real.sqrt 2 * max (Abs.abs x) (Abs.abs y)
have hle' := le_of_not_le hle
case neg
x y : ℝ
hle : ¬Abs.abs x ≤ Abs.abs y
hle' : Abs.abs y ≤ Abs.abs x
⊢ Real.sqrt (y ^ 2 + x ^ 2) ≤ Real.sqrt 2 * max (Abs.abs x) (Abs.abs y)
case neg
x y : ℝ
hle : ¬Abs.abs x ≤ Abs.abs y
hle' : Abs.abs y ≤ Abs.abs x
⊢ Real.sqrt (x ^ 2 + y ^ 2) ≤ Real.sqrt 2 * max (Abs.abs x) (Abs.abs y)
rw [add_comm]
no goals
case neg
x y : ℝ
hle : ¬Abs.abs x ≤ Abs.abs y
hle' : Abs.abs y ≤ Abs.abs x
⊢ Real.sqrt (y ^ 2 + x ^ 2) ≤ Real.sqrt 2 * max (Abs.abs x) (Abs.abs y)
calc
  Real.sqrt (y ^ 2 + x ^ 2) ≤ Real.sqrt (x ^ 2 + x ^ 2) :=
    Real.sqrt_le_sqrt (add_le_add_right (sq_le_sq.2 hle') _)
  _ = Real.sqrt 2 * max (|x|) (|y|) := by
    rw [max_eq_left hle', ← two_mul, Real.sqrt_mul two_pos.le, Real.sqrt_sq_eq_abs]
no goals
x y : ℝ
hle : ¬Abs.abs x ≤ Abs.abs y
hle' : Abs.abs y ≤ Abs.abs x
⊢ Real.sqrt (x ^ 2 + x ^ 2) = Real.sqrt 2 * max (Abs.abs x) (Abs.abs y)
rw [max_eq_left hle', ← two_mul, Real.sqrt_mul two_pos.le, Real.sqrt_sq_eq_abs]