-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem nonneg_mul {a b : ℤ√d} (ha : Nonneg a) (hb : Nonneg b) : Nonneg (a * b) :=
  match a, b, nonneg_cases ha, nonneg_cases hb, ha, hb with
  | _, _, ⟨_, _, Or.inl rfl⟩, ⟨_, _, Or.inl rfl⟩, _, _ => trivial
  | _, _, ⟨x, y, Or.inl rfl⟩, ⟨z, w, Or.inr <| Or.inr rfl⟩, _, hb => nonneg_mul_lem hb
  | _, _, ⟨x, y, Or.inl rfl⟩, ⟨z, w, Or.inr <| Or.inl rfl⟩, _, hb => nonneg_mul_lem hb
  | _, _, ⟨x, y, Or.inr <| Or.inr rfl⟩, ⟨z, w, Or.inl rfl⟩, ha, _ => by
    rw [mul_comm]; exact nonneg_mul_lem ha
  | _, _, ⟨x, y, Or.inr <| Or.inl rfl⟩, ⟨z, w, Or.inl rfl⟩, ha, _ => by
    rw [mul_comm]; exact nonneg_mul_lem ha
  | _, _, ⟨x, y, Or.inr <| Or.inr rfl⟩, ⟨z, w, Or.inr <| Or.inr rfl⟩, ha, hb => by
    rw [calc
          (⟨-x, y⟩ * ⟨-z, w⟩ : ℤ√d) = ⟨_, _⟩ := rfl
          _ = ⟨x * z + d * y * w, -(x * w + y * z)⟩

Proof state:
d : ℕ
a b : ℤ√↑d
ha✝ : a.Nonneg
hb✝ : b.Nonneg
x y z w : ℕ
ha : { re := ↑x, im := -↑y }.Nonneg
hb : { re := ↑z, im := -↑w }.Nonneg
⊢ {
      re :=
        { re := ↑x, im := -↑y }.re * { re := ↑z, im := -↑w }.re +
          ↑d * { re := ↑x, im := -↑y }.im * { re := ↑z, im := -↑w }.im,
      im :=
        { re := ↑x, im := -↑y }.re * { re := ↑z, im := -↑w }.im +
          { re := ↑x, im := -↑y }.im * { re := ↑z, im := -↑w }.re } =
    { re := ↑x * ↑z + ↑d * ↑y * ↑w, im := -(↑x * ↑w + ↑y * ↑z) }

Tactic:
simp [add_comm]

Result:
no goals

Proof state:
d : ℕ
a b : ℤ√↑d
ha✝ : a.Nonneg
hb✝ : b.Nonneg
x y z w : ℕ
ha : { re := ↑x, im := -↑y }.Nonneg
hb : { re := ↑z, im := -↑w }.Nonneg
⊢ { re := ↑x * ↑z + ↑d * ↑y * ↑w, im := -(↑x * ↑w + ↑y * ↑z) }.Nonneg

Tactic:
exact
    nonnegg_pos_neg.2
      (sqLe_mul.right.right.right (nonnegg_pos_neg.1 ha) (nonnegg_pos_neg.1 hb))

Result:
no goals

Proof state:
d : ℕ
a b : ℤ√↑d
ha✝ : a.Nonneg
hb✝ : b.Nonneg
x y z w : ℕ
ha : { re := -↑x, im := ↑y }.Nonneg
hb : { re := ↑z, im := -↑w }.Nonneg
⊢ ({ re := -↑x, im := ↑y } * { re := ↑z, im := -↑w }).Nonneg

Tactic:
rw [calc
      (⟨-x, y⟩ * ⟨z, -w⟩ : ℤ√d) = ⟨_, _⟩ := rfl
      _ = ⟨-(x * z + d * y * w), x * w + y * z⟩ := by simp [add_comm]
      ]

Result:
d : ℕ
a b : ℤ√↑d
ha✝ : a.Nonneg
hb✝ : b.Nonneg
x y z w : ℕ
ha : { re := -↑x, im := ↑y }.Nonneg
hb : { re := ↑z, im := -↑w }.Nonneg
⊢ { re := -(↑x * ↑z + ↑d * ↑y * ↑w), im := ↑x * ↑w + ↑y * ↑z }.Nonneg

Proof state:
d : ℕ
a b : ℤ√↑d
ha✝ : a.Nonneg
hb✝ : b.Nonneg
x y z w : ℕ
ha : { re := -↑x, im := ↑y }.Nonneg
hb : { re := -↑z, im := ↑w }.Nonneg
⊢ {
      re :=
        { re := -↑x, im := ↑y }.re * { re := -↑z, im := ↑w }.re +
          ↑d * { re := -↑x, im := ↑y }.im * { re := -↑z, im := ↑w }.im,
      im :=
        { re := -↑x, im := ↑y }.re * { re := -↑z, im := ↑w }.im +
          { re := -↑x, im := ↑y }.im * { re := -↑z, im := ↑w }.re } =
    { re := ↑x * ↑z + ↑d * ↑y * ↑w, im := -(↑x * ↑w + ↑y * ↑z) }

Tactic:
simp [add_comm]

Result:
no goals

Proof state:
d : ℕ
a b : ℤ√↑d
ha✝ : a.Nonneg
hb✝ : b.Nonneg
x y z w : ℕ
ha : { re := ↑x, im := -↑y }.Nonneg
hb : { re := -↑z, im := ↑w }.Nonneg
⊢ ({ re := ↑x, im := -↑y } * { re := -↑z, im := ↑w }).Nonneg

Tactic:
rw [calc
      (⟨x, -y⟩ * ⟨-z, w⟩ : ℤ√d) = ⟨_, _⟩ := rfl
      _ = ⟨-(x * z + d * y * w), x * w + y * z⟩ := by simp [add_comm]
      ]

Result:
d : ℕ
a b : ℤ√↑d
ha✝ : a.Nonneg
hb✝ : b.Nonneg
x y z w : ℕ
ha : { re := ↑x, im := -↑y }.Nonneg
hb : { re := -↑z, im := ↑w }.Nonneg
⊢ { re := -(↑x * ↑z + ↑d * ↑y * ↑w), im := ↑x * ↑w + ↑y * ↑z }.Nonneg

Proof state:
d : ℕ
a b : ℤ√↑d
ha✝ : a.Nonneg
hb : b.Nonneg
x y z w : ℕ
ha : { re := -↑x, im := ↑y }.Nonneg
x✝ : { re := ↑z, im := ↑w }.Nonneg
⊢ ({ re := ↑z, im := ↑w } * { re := -↑x, im := ↑y }).Nonneg

Tactic:
exact nonneg_mul_lem ha

Result:
no goals

Proof state:
d : ℕ
a b : ℤ√↑d
ha✝ : a.Nonneg
hb : b.Nonneg
x y z w : ℕ
ha : { re := ↑x, im := -↑y }.Nonneg
x✝ : { re := ↑z, im := ↑w }.Nonneg
⊢ ({ re := ↑z, im := ↑w } * { re := ↑x, im := -↑y }).Nonneg

Tactic:
exact nonneg_mul_lem ha

Result:
no goals

Proof state:
d : ℕ
a b : ℤ√↑d
ha✝ : a.Nonneg
hb : b.Nonneg
x y z w : ℕ
ha : { re := -↑x, im := ↑y }.Nonneg
x✝ : { re := ↑z, im := ↑w }.Nonneg
⊢ ({ re := -↑x, im := ↑y } * { re := ↑z, im := ↑w }).Nonneg

Tactic:
rw [mul_comm]

Result:
d : ℕ
a b : ℤ√↑d
ha✝ : a.Nonneg
hb : b.Nonneg
x y z w : ℕ
ha : { re := -↑x, im := ↑y }.Nonneg
x✝ : { re := ↑z, im := ↑w }.Nonneg
⊢ ({ re := ↑z, im := ↑w } * { re := -↑x, im := ↑y }).Nonneg

Proof state:
d : ℕ
a b : ℤ√↑d
ha✝ : a.Nonneg
hb✝ : b.Nonneg
x y z w : ℕ
ha : { re := ↑x, im := -↑y }.Nonneg
hb : { re := -↑z, im := ↑w }.Nonneg
⊢ {
      re :=
        { re := ↑x, im := -↑y }.re * { re := -↑z, im := ↑w }.re +
          ↑d * { re := ↑x, im := -↑y }.im * { re := -↑z, im := ↑w }.im,
      im :=
        { re := ↑x, im := -↑y }.re * { re := -↑z, im := ↑w }.im +
          { re := ↑x, im := -↑y }.im * { re := -↑z, im := ↑w }.re } =
    { re := -(↑x * ↑z + ↑d * ↑y * ↑w), im := ↑x * ↑w + ↑y * ↑z }

Tactic:
simp [add_comm]

Result:
no goals

Proof state:
d : ℕ
a b : ℤ√↑d
ha✝ : a.Nonneg
hb✝ : b.Nonneg
x y z w : ℕ
ha : { re := -↑x, im := ↑y }.Nonneg
hb : { re := -↑z, im := ↑w }.Nonneg
⊢ ({ re := -↑x, im := ↑y } * { re := -↑z, im := ↑w }).Nonneg

Tactic:
rw [calc
      (⟨-x, y⟩ * ⟨-z, w⟩ : ℤ√d) = ⟨_, _⟩ := rfl
      _ = ⟨x * z + d * y * w, -(x * w + y * z)⟩ := by simp [add_comm]
      ]

Result:
d : ℕ
a b : ℤ√↑d
ha✝ : a.Nonneg
hb✝ : b.Nonneg
x y z w : ℕ
ha : { re := -↑x, im := ↑y }.Nonneg
hb : { re := -↑z, im := ↑w }.Nonneg
⊢ { re := ↑x * ↑z + ↑d * ↑y * ↑w, im := -(↑x * ↑w + ↑y * ↑z) }.Nonneg

Proof state:
d : ℕ
a b : ℤ√↑d
ha✝ : a.Nonneg
hb✝ : b.Nonneg
x y z w : ℕ
ha : { re := ↑x, im := -↑y }.Nonneg
hb : { re := ↑z, im := -↑w }.Nonneg
⊢ ({ re := ↑x, im := -↑y } * { re := ↑z, im := -↑w }).Nonneg

Tactic:
rw [calc
      (⟨x, -y⟩ * ⟨z, -w⟩ : ℤ√d) = ⟨_, _⟩ := rfl
      _ = ⟨x * z + d * y * w, -(x * w + y * z)⟩ := by simp [add_comm]
      ]

Result:
d : ℕ
a b : ℤ√↑d
ha✝ : a.Nonneg
hb✝ : b.Nonneg
x y z w : ℕ
ha : { re := ↑x, im := -↑y }.Nonneg
hb : { re := ↑z, im := -↑w }.Nonneg
⊢ { re := ↑x * ↑z + ↑d * ↑y * ↑w, im := -(↑x * ↑w + ↑y * ↑z) }.Nonneg

Proof state:
d : ℕ
a b : ℤ√↑d
ha✝ : a.Nonneg
hb✝ : b.Nonneg
x y z w : ℕ
ha : { re := -↑x, im := ↑y }.Nonneg
hb : { re := ↑z, im := -↑w }.Nonneg
⊢ { re := -(↑x * ↑z + ↑d * ↑y * ↑w), im := ↑x * ↑w + ↑y * ↑z }.Nonneg

Tactic:
exact nonnegg_neg_pos.2 (sqLe_mul.right.left (nonnegg_neg_pos.1 ha) (nonnegg_pos_neg.1 hb))

Result:
no goals

Proof state:
d : ℕ
a b : ℤ√↑d
ha✝ : a.Nonneg
hb✝ : b.Nonneg
x y z w : ℕ
ha : { re := -↑x, im := ↑y }.Nonneg
hb : { re := -↑z, im := ↑w }.Nonneg
⊢ { re := ↑x * ↑z + ↑d * ↑y * ↑w, im := -(↑x * ↑w + ↑y * ↑z) }.Nonneg

Tactic:
exact nonnegg_pos_neg.2 (sqLe_mul.left (nonnegg_neg_pos.1 ha) (nonnegg_neg_pos.1 hb))

Result:
no goals

Proof state:
d : ℕ
a b : ℤ√↑d
ha✝ : a.Nonneg
hb✝ : b.Nonneg
x y z w : ℕ
ha : { re := ↑x, im := -↑y }.Nonneg
hb : { re := -↑z, im := ↑w }.Nonneg
⊢ { re := -(↑x * ↑z + ↑d * ↑y * ↑w), im := ↑x * ↑w + ↑y * ↑z }.Nonneg

Tactic:
exact
    nonnegg_neg_pos.2 (sqLe_mul.right.right.left (nonnegg_pos_neg.1 ha) (nonnegg_neg_pos.1 hb))

Result:
no goals

Proof state:
d : ℕ
a b : ℤ√↑d
ha✝ : a.Nonneg
hb✝ : b.Nonneg
x y z w : ℕ
ha : { re := -↑x, im := ↑y }.Nonneg
hb : { re := ↑z, im := -↑w }.Nonneg
⊢ {
      re :=
        { re := -↑x, im := ↑y }.re * { re := ↑z, im := -↑w }.re +
          ↑d * { re := -↑x, im := ↑y }.im * { re := ↑z, im := -↑w }.im,
      im :=
        { re := -↑x, im := ↑y }.re * { re := ↑z, im := -↑w }.im +
          { re := -↑x, im := ↑y }.im * { re := ↑z, im := -↑w }.re } =
    { re := -(↑x * ↑z + ↑d * ↑y * ↑w), im := ↑x * ↑w + ↑y * ↑z }

Tactic:
simp [add_comm]

Result:
no goals