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

Proof state:
d : ℕ
a b : ℤ√↑d
ha : a.Nonneg
hb : b.Nonneg
⊢ (a + b).Nonneg

Tactic:
rcases nonneg_cases ha with ⟨x, y, rfl | rfl | rfl⟩ <;>
  rcases nonneg_cases hb with ⟨z, w, rfl | rfl | rfl⟩

Result:
case intro.intro.inl.intro.intro.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

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

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

case intro.intro.inr.inl.intro.intro.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

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

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

case intro.intro.inr.inr.intro.intro.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

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

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

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

Tactic:
simp [add_comm, *]

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 : -↑x + ↑z = -↑i
⊢ i ≤ x

Tactic:
exact Int.ofNat_le.1 (le_of_neg_le_neg (Int.le.intro _ h))

Result:
no goals

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 + ↑z, im := ↑y + -↑w }.Nonneg

Tactic:
rw [add_comm, add_comm (y : ℤ)]

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 := ↑z + -↑x, im := -↑w + ↑y }.Nonneg

Proof state:
case intro.intro.inr.inl.intro.intro.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 ha)

Result:
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 : { 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 : { 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

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 : { re := ↑x, im := -↑y }.im + { re := ↑z, im := ↑w }.im = -↑i
⊢ i ≤ y

Tactic:
dsimp only at h

Result:
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

Proof state:
case intro.intro.inl.intro.intro.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:
trivial

Result:
no goals

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

Tactic:
simp [add_comm, *]

Result:
no goals

Proof state:
case intro.intro.inr.inr.intro.intro.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_left fun i h => sqLe_of_le ?_ ?_ (nonnegg_neg_pos.1 ha)

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 : { 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 : { 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

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

Tactic:
simp [*]

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:
rwa [add_def]

Result:
no goals

Proof state:
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

Tactic:
dsimp only at h

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 : ↑y + -↑w = -↑i
⊢ i ≤ w

Proof state:
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 : ↑y + -↑w = -↑i
⊢ i ≤ w

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

Result:
no goals

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
this : { re := ↑x + ↑z, im := -↑y + -↑w }.Nonneg
⊢ ({ re := ↑x, im := -↑y } + { re := ↑z, im := -↑w }).Nonneg

Tactic:
rwa [add_def]

Result:
no goals

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 : { re := ↑x, im := ↑y }.re + { re := -↑z, im := ↑w }.re = -↑i
⊢ i ≤ z

Tactic:
dsimp only at h

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 : ↑x + -↑z = -↑i
⊢ i ≤ z