case intro.intro.inl.intro.intro.inl
d x y : ℕ
ha : Nonneg { re := ↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := ↑w }
⊢ Nonneg ({ re := ↑x, im := ↑y } + { re := ↑z, im := ↑w })

case intro.intro.inl.intro.intro.inr.inl
d x y : ℕ
ha : Nonneg { re := ↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := -↑w }
⊢ Nonneg ({ re := ↑x, im := ↑y } + { re := ↑z, im := -↑w })

case intro.intro.inl.intro.intro.inr.inr
d x y : ℕ
ha : Nonneg { re := ↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := -↑z, im := ↑w }
⊢ Nonneg ({ re := ↑x, im := ↑y } + { re := -↑z, im := ↑w })

case intro.intro.inr.inl.intro.intro.inl
d x y : ℕ
ha : Nonneg { re := ↑x, im := -↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := ↑w }
⊢ Nonneg ({ re := ↑x, im := -↑y } + { re := ↑z, im := ↑w })

case intro.intro.inr.inl.intro.intro.inr.inl
d x y : ℕ
ha : Nonneg { re := ↑x, im := -↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := -↑w }
⊢ Nonneg ({ re := ↑x, im := -↑y } + { re := ↑z, im := -↑w })

case intro.intro.inr.inl.intro.intro.inr.inr
d x y : ℕ
ha : Nonneg { re := ↑x, im := -↑y }
z w : ℕ
hb : Nonneg { re := -↑z, im := ↑w }
⊢ Nonneg ({ re := ↑x, im := -↑y } + { re := -↑z, im := ↑w })

case intro.intro.inr.inr.intro.intro.inl
d x y : ℕ
ha : Nonneg { re := -↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := ↑w }
⊢ Nonneg ({ re := -↑x, im := ↑y } + { re := ↑z, im := ↑w })

case intro.intro.inr.inr.intro.intro.inr.inl
d x y : ℕ
ha : Nonneg { re := -↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := -↑w }
⊢ Nonneg ({ re := -↑x, im := ↑y } + { re := ↑z, im := -↑w })

case intro.intro.inr.inr.intro.intro.inr.inr
d x y : ℕ
ha : Nonneg { re := -↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := -↑z, im := ↑w }
⊢ Nonneg ({ re := -↑x, im := ↑y } + { re := -↑z, im := ↑w })
d : ℕ
a b : ℤ√↑d
ha : Nonneg a
hb : Nonneg b
⊢ Nonneg (a + b)
rcases nonneg_cases ha with ⟨x, y, rfl | rfl | rfl⟩ <;>
  rcases nonneg_cases hb with ⟨z, w, rfl | rfl | rfl⟩
no goals
case intro.intro.inl.intro.intro.inl
d x y : ℕ
ha : Nonneg { re := ↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := ↑w }
⊢ Nonneg ({ re := ↑x, im := ↑y } + { re := ↑z, im := ↑w })
trivial
case intro.intro.inl.intro.intro.inr.inl.refine'_1
d x y : ℕ
ha : Nonneg { re := ↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := -↑w }
i : ℕ
h : { re := ↑x, im := ↑y }.im + { re := ↑z, im := -↑w }.im = -↑i
⊢ i ≤ w

case intro.intro.inl.intro.intro.inr.inl.refine'_2
d x y : ℕ
ha : Nonneg { re := ↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := -↑w }
i : ℕ
h : { re := ↑x, im := ↑y }.im + { re := ↑z, im := -↑w }.im = -↑i
⊢ z ≤ x + z
case intro.intro.inl.intro.intro.inr.inl
d x y : ℕ
ha : Nonneg { re := ↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := -↑w }
⊢ Nonneg ({ re := ↑x, im := ↑y } + { re := ↑z, im := -↑w })
refine' nonnegg_cases_right fun i h => sqLe_of_le _ _ (nonnegg_pos_neg.1 hb)
case intro.intro.inl.intro.intro.inr.inl.refine'_1
d x y : ℕ
ha : Nonneg { re := ↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := -↑w }
i : ℕ
h : ↑y + -↑w = -↑i
⊢ i ≤ w
case intro.intro.inl.intro.intro.inr.inl.refine'_1
d x y : ℕ
ha : Nonneg { re := ↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := -↑w }
i : ℕ
h : { re := ↑x, im := ↑y }.im + { re := ↑z, im := -↑w }.im = -↑i
⊢ i ≤ w
dsimp only at h
no goals
case intro.intro.inl.intro.intro.inr.inl.refine'_1
d x y : ℕ
ha : Nonneg { re := ↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := -↑w }
i : ℕ
h : ↑y + -↑w = -↑i
⊢ i ≤ w
exact Int.ofNat_le.1 (le_of_neg_le_neg (Int.le.intro y (by simp [add_comm, *])))
no goals
d x y : ℕ
ha : Nonneg { re := ↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := -↑w }
i : ℕ
h : ↑y + -↑w = -↑i
⊢ -↑w + ↑y = -↑i
simp [add_comm, *]
no goals
case intro.intro.inl.intro.intro.inr.inl.refine'_2
d x y : ℕ
ha : Nonneg { re := ↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := -↑w }
i : ℕ
h : { re := ↑x, im := ↑y }.im + { re := ↑z, im := -↑w }.im = -↑i
⊢ z ≤ x + z
apply Nat.le_add_left
case intro.intro.inl.intro.intro.inr.inr.refine'_1
d x y : ℕ
ha : Nonneg { re := ↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := -↑z, im := ↑w }
i : ℕ
h : { re := ↑x, im := ↑y }.re + { re := -↑z, im := ↑w }.re = -↑i
⊢ i ≤ z

case intro.intro.inl.intro.intro.inr.inr.refine'_2
d x y : ℕ
ha : Nonneg { re := ↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := -↑z, im := ↑w }
i : ℕ
h : { re := ↑x, im := ↑y }.re + { re := -↑z, im := ↑w }.re = -↑i
⊢ w ≤ y + w
case intro.intro.inl.intro.intro.inr.inr
d x y : ℕ
ha : Nonneg { re := ↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := -↑z, im := ↑w }
⊢ Nonneg ({ re := ↑x, im := ↑y } + { re := -↑z, im := ↑w })
refine' nonnegg_cases_left fun i h => sqLe_of_le _ _ (nonnegg_neg_pos.1 hb)
case intro.intro.inl.intro.intro.inr.inr.refine'_1
d x y : ℕ
ha : Nonneg { re := ↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := -↑z, im := ↑w }
i : ℕ
h : ↑x + -↑z = -↑i
⊢ i ≤ z
case intro.intro.inl.intro.intro.inr.inr.refine'_1
d x y : ℕ
ha : Nonneg { re := ↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := -↑z, im := ↑w }
i : ℕ
h : { re := ↑x, im := ↑y }.re + { re := -↑z, im := ↑w }.re = -↑i
⊢ i ≤ z
dsimp only at h
no goals
case intro.intro.inl.intro.intro.inr.inr.refine'_1
d x y : ℕ
ha : Nonneg { re := ↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := -↑z, im := ↑w }
i : ℕ
h : ↑x + -↑z = -↑i
⊢ i ≤ z
exact Int.ofNat_le.1 (le_of_neg_le_neg (Int.le.intro x (by simp [add_comm, *])))
no goals
d x y : ℕ
ha : Nonneg { re := ↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := -↑z, im := ↑w }
i : ℕ
h : ↑x + -↑z = -↑i
⊢ -↑z + ↑x = -↑i
simp [add_comm, *]
no goals
case intro.intro.inl.intro.intro.inr.inr.refine'_2
d x y : ℕ
ha : Nonneg { re := ↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := -↑z, im := ↑w }
i : ℕ
h : { re := ↑x, im := ↑y }.re + { re := -↑z, im := ↑w }.re = -↑i
⊢ w ≤ y + w
apply Nat.le_add_left
case intro.intro.inr.inl.intro.intro.inl.refine'_1
d x y : ℕ
ha : Nonneg { re := ↑x, im := -↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := ↑w }
i : ℕ
h : { re := ↑x, im := -↑y }.im + { re := ↑z, im := ↑w }.im = -↑i
⊢ i ≤ y

case intro.intro.inr.inl.intro.intro.inl.refine'_2
d x y : ℕ
ha : Nonneg { re := ↑x, im := -↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := ↑w }
i : ℕ
h : { re := ↑x, im := -↑y }.im + { re := ↑z, im := ↑w }.im = -↑i
⊢ x ≤ x + z
case intro.intro.inr.inl.intro.intro.inl
d x y : ℕ
ha : Nonneg { re := ↑x, im := -↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := ↑w }
⊢ Nonneg ({ re := ↑x, im := -↑y } + { re := ↑z, im := ↑w })
refine' nonnegg_cases_right fun i h => sqLe_of_le _ _ (nonnegg_pos_neg.1 ha)
case intro.intro.inr.inl.intro.intro.inl.refine'_1
d x y : ℕ
ha : Nonneg { re := ↑x, im := -↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := ↑w }
i : ℕ
h : -↑y + ↑w = -↑i
⊢ i ≤ y
case intro.intro.inr.inl.intro.intro.inl.refine'_1
d x y : ℕ
ha : Nonneg { re := ↑x, im := -↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := ↑w }
i : ℕ
h : { re := ↑x, im := -↑y }.im + { re := ↑z, im := ↑w }.im = -↑i
⊢ i ≤ y
dsimp only at h
no goals
case intro.intro.inr.inl.intro.intro.inl.refine'_1
d x y : ℕ
ha : Nonneg { re := ↑x, im := -↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := ↑w }
i : ℕ
h : -↑y + ↑w = -↑i
⊢ i ≤ y
exact Int.ofNat_le.1 (le_of_neg_le_neg (Int.le.intro w (by simp [*])))
no goals
d x y : ℕ
ha : Nonneg { re := ↑x, im := -↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := ↑w }
i : ℕ
h : -↑y + ↑w = -↑i
⊢ -↑y + ↑w = -↑i
simp [*]
no goals
case intro.intro.inr.inl.intro.intro.inl.refine'_2
d x y : ℕ
ha : Nonneg { re := ↑x, im := -↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := ↑w }
i : ℕ
h : { re := ↑x, im := -↑y }.im + { re := ↑z, im := ↑w }.im = -↑i
⊢ x ≤ x + z
apply Nat.le_add_right
case intro.intro.inr.inl.intro.intro.inr.inl
d x y : ℕ
ha : Nonneg { re := ↑x, im := -↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := -↑w }
this : Nonneg { re := ↑(x + z), im := -↑(y + w) }
⊢ Nonneg ({ re := ↑x, im := -↑y } + { re := ↑z, im := -↑w })
case intro.intro.inr.inl.intro.intro.inr.inl
d x y : ℕ
ha : Nonneg { re := ↑x, im := -↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := -↑w }
⊢ Nonneg ({ re := ↑x, im := -↑y } + { re := ↑z, im := -↑w })
have : Nonneg ⟨_, _⟩ :=
  nonnegg_pos_neg.2 (sqLe_add (nonnegg_pos_neg.1 ha) (nonnegg_pos_neg.1 hb))
case intro.intro.inr.inl.intro.intro.inr.inl
d x y : ℕ
ha : Nonneg { re := ↑x, im := -↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := -↑w }
this : Nonneg { re := ↑x + ↑z, im := -↑y + -↑w }
⊢ Nonneg ({ re := ↑x, im := -↑y } + { re := ↑z, im := -↑w })
case intro.intro.inr.inl.intro.intro.inr.inl
d x y : ℕ
ha : Nonneg { re := ↑x, im := -↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := -↑w }
this : Nonneg { re := ↑(x + z), im := -↑(y + w) }
⊢ Nonneg ({ re := ↑x, im := -↑y } + { re := ↑z, im := -↑w })
rw [Nat.cast_add, Nat.cast_add, neg_add] at this
no goals
case intro.intro.inr.inl.intro.intro.inr.inl
d x y : ℕ
ha : Nonneg { re := ↑x, im := -↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := -↑w }
this : Nonneg { re := ↑x + ↑z, im := -↑y + -↑w }
⊢ Nonneg ({ re := ↑x, im := -↑y } + { re := ↑z, im := -↑w })
rwa [add_def]
no goals
case intro.intro.inr.inl.intro.intro.inr.inr
d x y : ℕ
ha : Nonneg { re := ↑x, im := -↑y }
z w : ℕ
hb : Nonneg { re := -↑z, im := ↑w }
⊢ Nonneg ({ re := ↑x, im := -↑y } + { re := -↑z, im := ↑w })
exact nonneg_add_lem ha hb
case intro.intro.inr.inr.intro.intro.inl.refine'_1
d x y : ℕ
ha : Nonneg { re := -↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := ↑w }
i : ℕ
h : { re := -↑x, im := ↑y }.re + { re := ↑z, im := ↑w }.re = -↑i
⊢ i ≤ x

case intro.intro.inr.inr.intro.intro.inl.refine'_2
d x y : ℕ
ha : Nonneg { re := -↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := ↑w }
i : ℕ
h : { re := -↑x, im := ↑y }.re + { re := ↑z, im := ↑w }.re = -↑i
⊢ y ≤ y + w
case intro.intro.inr.inr.intro.intro.inl
d x y : ℕ
ha : Nonneg { re := -↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := ↑w }
⊢ Nonneg ({ re := -↑x, im := ↑y } + { re := ↑z, im := ↑w })
refine' nonnegg_cases_left fun i h => sqLe_of_le _ _ (nonnegg_neg_pos.1 ha)
case intro.intro.inr.inr.intro.intro.inl.refine'_1
d x y : ℕ
ha : Nonneg { re := -↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := ↑w }
i : ℕ
h : -↑x + ↑z = -↑i
⊢ i ≤ x
case intro.intro.inr.inr.intro.intro.inl.refine'_1
d x y : ℕ
ha : Nonneg { re := -↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := ↑w }
i : ℕ
h : { re := -↑x, im := ↑y }.re + { re := ↑z, im := ↑w }.re = -↑i
⊢ i ≤ x
dsimp only at h
no goals
case intro.intro.inr.inr.intro.intro.inl.refine'_1
d x y : ℕ
ha : Nonneg { re := -↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := ↑w }
i : ℕ
h : -↑x + ↑z = -↑i
⊢ i ≤ x
exact Int.ofNat_le.1 (le_of_neg_le_neg (Int.le.intro _ h))
no goals
case intro.intro.inr.inr.intro.intro.inl.refine'_2
d x y : ℕ
ha : Nonneg { re := -↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := ↑w }
i : ℕ
h : { re := -↑x, im := ↑y }.re + { re := ↑z, im := ↑w }.re = -↑i
⊢ y ≤ y + w
apply Nat.le_add_right
case intro.intro.inr.inr.intro.intro.inr.inl
d x y : ℕ
ha : Nonneg { re := -↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := -↑w }
⊢ Nonneg { re := -↑x + ↑z, im := ↑y + -↑w }
case intro.intro.inr.inr.intro.intro.inr.inl
d x y : ℕ
ha : Nonneg { re := -↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := -↑w }
⊢ Nonneg ({ re := -↑x, im := ↑y } + { re := ↑z, im := -↑w })
dsimp
case intro.intro.inr.inr.intro.intro.inr.inl
d x y : ℕ
ha : Nonneg { re := -↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := -↑w }
⊢ Nonneg { re := ↑z + -↑x, im := -↑w + ↑y }
case intro.intro.inr.inr.intro.intro.inr.inl
d x y : ℕ
ha : Nonneg { re := -↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := -↑w }
⊢ Nonneg { re := -↑x + ↑z, im := ↑y + -↑w }
rw [add_comm, add_comm (y : ℤ)]
no goals
case intro.intro.inr.inr.intro.intro.inr.inl
d x y : ℕ
ha : Nonneg { re := -↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := -↑w }
⊢ Nonneg { re := ↑z + -↑x, im := -↑w + ↑y }
exact nonneg_add_lem hb ha
case intro.intro.inr.inr.intro.intro.inr.inr
d x y : ℕ
ha : Nonneg { re := -↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := -↑z, im := ↑w }
this : Nonneg { re := -↑(x + z), im := ↑(y + w) }
⊢ Nonneg ({ re := -↑x, im := ↑y } + { re := -↑z, im := ↑w })
case intro.intro.inr.inr.intro.intro.inr.inr
d x y : ℕ
ha : Nonneg { re := -↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := -↑z, im := ↑w }
⊢ Nonneg ({ re := -↑x, im := ↑y } + { re := -↑z, im := ↑w })
have : Nonneg ⟨_, _⟩ :=
  nonnegg_neg_pos.2 (sqLe_add (nonnegg_neg_pos.1 ha) (nonnegg_neg_pos.1 hb))
case intro.intro.inr.inr.intro.intro.inr.inr
d x y : ℕ
ha : Nonneg { re := -↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := -↑z, im := ↑w }
this : Nonneg { re := -↑x + -↑z, im := ↑y + ↑w }
⊢ Nonneg ({ re := -↑x, im := ↑y } + { re := -↑z, im := ↑w })
case intro.intro.inr.inr.intro.intro.inr.inr
d x y : ℕ
ha : Nonneg { re := -↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := -↑z, im := ↑w }
this : Nonneg { re := -↑(x + z), im := ↑(y + w) }
⊢ Nonneg ({ re := -↑x, im := ↑y } + { re := -↑z, im := ↑w })
rw [Nat.cast_add, Nat.cast_add, neg_add] at this
no goals
case intro.intro.inr.inr.intro.intro.inr.inr
d x y : ℕ
ha : Nonneg { re := -↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := -↑z, im := ↑w }
this : Nonneg { re := -↑x + -↑z, im := ↑y + ↑w }
⊢ Nonneg ({ re := -↑x, im := ↑y } + { re := -↑z, im := ↑w })
rwa [add_def]