-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem Nonneg.add {a b : ℤ√d} (ha : Nonneg a) (hb : Nonneg b) : Nonneg (a + b)

Proof state:
case intro.intro.inl.intro.intro.inr.inr.refine_1
d x y : ℕ
ha : { re := ↑x, im := ↑y }.Nonneg
z w : ℕ
hb : { re := -↑z, im := ↑w }.Nonneg
i : ℕ
h : ↑x + -↑z = -↑i
⊢ i ≤ z

Tactic:
exact Int.ofNat_le.1 (le_of_neg_le_neg (Int.le.intro x (by simp [add_comm, *])))

Result:
no goals

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

Tactic:
refine nonnegg_cases_right fun i h => sqLe_of_le ?_ ?_ (nonnegg_pos_neg.1 hb)

Result:
case intro.intro.inl.intro.intro.inr.inl.refine_1
d x y : ℕ
ha : { re := ↑x, im := ↑y }.Nonneg
z w : ℕ
hb : { re := ↑z, im := -↑w }.Nonneg
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 : { re := ↑x, im := ↑y }.Nonneg
z w : ℕ
hb : { re := ↑z, im := -↑w }.Nonneg
i : ℕ
h : { re := ↑x, im := ↑y }.im + { re := ↑z, im := -↑w }.im = -↑i
⊢ z ≤ x + z

Proof state:
case intro.intro.inr.inr.intro.intro.inl.refine_2
d x y : ℕ
ha : { re := -↑x, im := ↑y }.Nonneg
z w : ℕ
hb : { re := ↑z, im := ↑w }.Nonneg
i : ℕ
h : { re := -↑x, im := ↑y }.re + { re := ↑z, im := ↑w }.re = -↑i
⊢ y ≤ y + w

Tactic:
apply Nat.le_add_right

Result:
no goals

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

Tactic:
exact nonneg_add_lem ha hb

Result:
no goals

Proof state:
case intro.intro.inl.intro.intro.inr.inl.refine_2
d x y : ℕ
ha : { re := ↑x, im := ↑y }.Nonneg
z w : ℕ
hb : { re := ↑z, im := -↑w }.Nonneg
i : ℕ
h : { re := ↑x, im := ↑y }.im + { re := ↑z, im := -↑w }.im = -↑i
⊢ z ≤ x + z

Tactic:
apply Nat.le_add_left

Result:
no goals

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

Tactic:
refine nonnegg_cases_left fun i h => sqLe_of_le ?_ ?_ (nonnegg_neg_pos.1 hb)

Result:
case intro.intro.inl.intro.intro.inr.inr.refine_1
d x y : ℕ
ha : { re := ↑x, im := ↑y }.Nonneg
z w : ℕ
hb : { re := -↑z, im := ↑w }.Nonneg
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 : { re := ↑x, im := ↑y }.Nonneg
z w : ℕ
hb : { re := -↑z, im := ↑w }.Nonneg
i : ℕ
h : { re := ↑x, im := ↑y }.re + { re := -↑z, im := ↑w }.re = -↑i
⊢ w ≤ y + w

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

Tactic:
exact nonneg_add_lem hb ha

Result:
no goals

Proof state:
case intro.intro.inr.inr.intro.intro.inl.refine_1
d x y : ℕ
ha : { re := -↑x, im := ↑y }.Nonneg
z w : ℕ
hb : { re := ↑z, im := ↑w }.Nonneg
i : ℕ
h : { re := -↑x, im := ↑y }.re + { re := ↑z, im := ↑w }.re = -↑i
⊢ i ≤ x

Tactic:
dsimp only at h

Result:
case intro.intro.inr.inr.intro.intro.inl.refine_1
d x y : ℕ
ha : { re := -↑x, im := ↑y }.Nonneg
z w : ℕ
hb : { re := ↑z, im := ↑w }.Nonneg
i : ℕ
h : -↑x + ↑z = -↑i
⊢ i ≤ x

Proof state:
case intro.intro.inr.inl.intro.intro.inl.refine_1
d x y : ℕ
ha : { re := ↑x, im := -↑y }.Nonneg
z w : ℕ
hb : { re := ↑z, im := ↑w }.Nonneg
i : ℕ
h : -↑y + ↑w = -↑i
⊢ i ≤ y

Tactic:
exact Int.ofNat_le.1 (le_of_neg_le_neg (Int.le.intro w (by simp [*])))

Result:
no goals

Proof state:
case intro.intro.inl.intro.intro.inr.inr.refine_2
d x y : ℕ
ha : { re := ↑x, im := ↑y }.Nonneg
z w : ℕ
hb : { re := -↑z, im := ↑w }.Nonneg
i : ℕ
h : { re := ↑x, im := ↑y }.re + { re := -↑z, im := ↑w }.re = -↑i
⊢ w ≤ y + w

Tactic:
apply Nat.le_add_left

Result:
no goals

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

Tactic:
have : Nonneg ⟨_, _⟩ :=
  nonnegg_neg_pos.2 (sqLe_add (nonnegg_neg_pos.1 ha) (nonnegg_neg_pos.1 hb))

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

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

Tactic:
have : Nonneg ⟨_, _⟩ :=
  nonnegg_pos_neg.2 (sqLe_add (nonnegg_pos_neg.1 ha) (nonnegg_pos_neg.1 hb))

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

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

Tactic:
dsimp

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

Proof state:
case intro.intro.inr.inl.intro.intro.inl.refine_2
d x y : ℕ
ha : { re := ↑x, im := -↑y }.Nonneg
z w : ℕ
hb : { re := ↑z, im := ↑w }.Nonneg
i : ℕ
h : { re := ↑x, im := -↑y }.im + { re := ↑z, im := ↑w }.im = -↑i
⊢ x ≤ x + z

Tactic:
apply Nat.le_add_right

Result:
no goals

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

Tactic:
rw [Nat.cast_add, Nat.cast_add, neg_add] at this

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