awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y : ℕ
ha : Nonneg (d := d) { re := -(↑x : ℤ), im := (↑y : ℤ) }
z w : ℕ
hb : Nonneg (d := d) { re := (↑z : ℤ), im := -(↑w : ℤ) }
⊢ Nonneg (d := d) { re := HAdd.hAdd (α := ℤ) (↑z : ℤ) (-(↑x : ℤ)), im := HAdd.hAdd (α := ℤ) (-(↑w : ℤ)) (↑y : ℤ) }

Tactic:
exact nonneg_add_lem hb ha

Premises used: Zsqrtd.nonneg_add_lem
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y : ℕ
ha : Nonneg (d := d) { re := -(↑x : ℤ), im := (↑y : ℤ) }
z w : ℕ
hb : Nonneg (d := d) { re := -(↑z : ℤ), im := (↑w : ℤ) }
⊢ Nonneg (d := d) { re := -(↑(x + z) : ℤ), im := (↑(y + w) : ℤ) }

Tactic:
have : Nonneg ⟨_, _⟩ :=
      nonnegg_neg_pos.2 (sqLe_add (nonnegg_neg_pos.1 ha) (nonnegg_neg_pos.1 hb))
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y : ℕ
ha : Nonneg (d := d) { re := -(↑x : ℤ), im := (↑y : ℤ) }
z w : ℕ
hb : Nonneg (d := d) { re := -(↑z : ℤ), im := (↑w : ℤ) }
this : Nonneg (d := d) { re := -(↑(x + z) : ℤ), im := (↑(y + w) : ℤ) }
⊢ Nonneg (d := d) { re := HAdd.hAdd (α := ℤ) (-(↑x : ℤ)) (-(↑z : ℤ)), im := HAdd.hAdd (α := ℤ) (↑y : ℤ) (↑w : ℤ) }

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

Premises used: neg_add, Nat.cast_add
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y : ℕ
ha : Nonneg (d := d) { re := -(↑x : ℤ), im := (↑y : ℤ) }
z w : ℕ
hb : Nonneg (d := d) { re := -(↑z : ℤ), im := (↑w : ℤ) }
this : Nonneg (d := d) { re := HAdd.hAdd (α := ℤ) (-(↑x : ℤ)) (-(↑z : ℤ)), im := HAdd.hAdd (α := ℤ) (↑y : ℤ) (↑w : ℤ) }
inr inr₁ inr₂ inr₃ :
  Nonneg (d := d) { re := HAdd.hAdd (α := ℤ) (-(↑x : ℤ)) (-(↑z : ℤ)), im := HAdd.hAdd (α := ℤ) (↑y : ℤ) (↑w : ℤ) }
⊢ (HAdd.hAdd (α := ℤ√(↑d : ℤ)) { re := -(↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) }
      { re := -(↑z : ℤ), im := (↑w : ℤ) : ℤ√(↑d : ℤ) }).Nonneg

Tactic:
rwa [add_def]

Premises used: Zsqrtd.add_def
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
a : ℤ√(↑d : ℤ)
⊢ a.Nonneg ↔ (a - 0).Nonneg

Tactic:
simp
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
x y z w : ℤ
xz : x ≤ z
yw : y ≤ w
⊢ LE.le (α := ℤ√(↑d : ℤ)) { re := x, im := y } { re := z, im := w }

Tactic:
show Nonneg ⟨z - x, w - y⟩ from
    match z - x, w - y, Int.le.dest_sub xz, Int.le.dest_sub yw with
    | _, _, ⟨_, rfl⟩, ⟨_, rfl⟩ => trivial

Premises used: trivial, HSub.hSub, Int.le.dest_sub, Int.sub, Zsqrtd.mk, _private.0.Zsqrtd.le_of_le_le.match_1, Zsqrtd.Nonneg
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
a b : ℤ√(↑d : ℤ)
⊢ (b - a).Nonneg ∨ (-(b - a)).Nonneg

Tactic:
have t := (b - a).nonneg_total
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
a b : ℤ√(↑d : ℤ)
t : (b - a).Nonneg ∨ (-(b - a)).Nonneg
rwa rwa₁ rwa₂ rwa₃ : ∀ (t : (b - a).Nonneg ∨ (a - b).Nonneg), a ≤ b ∨ b ≤ a
⊢ a ≤ b ∨ b ≤ a

Tactic:
rwa [neg_sub] at t

Premises used: neg_sub
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
a : ℤ√(↑d : ℤ)
simp : Nonneg (d := d) 0
⊢ (a - a).Nonneg

Tactic:
simp only [sub_self]

Premises used: sub_self
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
a : ℤ√(↑d : ℤ)
⊢ Nonneg (d := d) 0

Tactic:
trivial
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
a b c : ℤ√(↑d : ℤ)
hab : a ≤ b
hbc : b ≤ c
⊢ a ≤ c

Tactic:
simpa [sub_add_sub_cancel'] using hab.add hbc

Premises used: sub_add_sub_cancel', Zsqrtd.Nonneg.add
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
a b : ℤ√(↑d : ℤ)
⊢ (a - b).Nonneg ∨ (-(a - b)).Nonneg

Tactic:
have t := (a - b).nonneg_total
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
a b : ℤ√(↑d : ℤ)
t : (a - b).Nonneg ∨ (-(a - b)).Nonneg
rwa rwa₁ rwa₂ rwa₃ : ∀ (t : (a - b).Nonneg ∨ (b - a).Nonneg), b ≤ a ∨ a ≤ b
⊢ b ≤ a ∨ a ≤ b

Tactic:
rwa [neg_sub] at t

Premises used: neg_sub
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
a b : ℤ√(↑d : ℤ)
⊢ b ≤ a ∨ a ≤ b

Tactic:
have ht : b ≤ a ∨ a ≤ b := by
      have t := (a - b).nonneg_total
      rwa [neg_sub] at t
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
a b : ℤ√(↑d : ℤ)
ht : b ≤ a ∨ a ≤ b
⊢ a < b ↔ a ≤ b ∧ ¬b ≤ a

Tactic:
(and_iff_right_of_imp ht.resolve_left).symm

Premises used: Or.resolve_left, and_iff_right_of_imp, Iff.symm
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
a b : ℤ√(↑d : ℤ)
ht : b ≤ a ∨ a ≤ b
⊢ a < b ↔ a ≤ b ∧ ¬b ≤ a

Tactic:
exact (and_iff_right_of_imp ht.resolve_left).symm

Premises used: Or.resolve_left, and_iff_right_of_imp, Iff.symm
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
a : ℤ√(↑d : ℤ)
x y : ℕ
⊢ (HAdd.hAdd (α := ℤ√(↑d : ℤ)) { re := (↑0 : ℤ), im := (↑0 : ℤ) : ℤ√(↑d : ℤ) }
      { re := ofNat x, im := ofNat y : ℤ√(↑d : ℤ) }).Nonneg

Tactic:
trivial
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
a : ℤ√(↑d : ℤ)
x y : ℕ
⊢ (HAdd.hAdd (α := ℤ√(↑d : ℤ)) { re := (↑0 : ℤ), im := (↑(y + 1) : ℤ) : ℤ√(↑d : ℤ) }
      { re := ofNat x, im := -[y+1] : ℤ√(↑d : ℤ) }).Nonneg

Tactic:
simp [Int.negSucc_eq, add_assoc, Nonneg, Nonnegg]

Premises used: add_assoc, Zsqrtd.Nonnegg, Int.negSucc_eq, Zsqrtd.Nonneg
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
a : ℤ√(↑d : ℤ)
x y : ℕ
⊢ (HAdd.hAdd (α := ℤ√(↑d : ℤ)) { re := (↑(x + 1) : ℤ), im := (↑0 : ℤ) : ℤ√(↑d : ℤ) }
      { re := -[x+1], im := ofNat y : ℤ√(↑d : ℤ) }).Nonneg

Tactic:
simp [Int.negSucc_eq, add_assoc, Nonneg, Nonnegg]

Premises used: add_assoc, Zsqrtd.Nonnegg, Int.negSucc_eq, Zsqrtd.Nonneg
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
a : ℤ√(↑d : ℤ)
x y : ℕ
⊢ (HAdd.hAdd (α := ℤ√(↑d : ℤ)) { re := (↑(x + 1) : ℤ), im := (↑(y + 1) : ℤ) : ℤ√(↑d : ℤ) }
      { re := -[x+1], im := -[y+1] : ℤ√(↑d : ℤ) }).Nonneg

Tactic:
simp [Int.negSucc_eq, add_assoc, Nonneg, Nonnegg]

Premises used: add_assoc, Zsqrtd.Nonnegg, Int.negSucc_eq, Zsqrtd.Nonneg
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
a : ℤ√(↑d : ℤ)
obtain : ∀ (x y : ℕ) (h : a ≤ { re := (↑x : ℤ), im := (↑y : ℤ) }), ∃ (n : ℕ), a ≤ (↑n : ℤ√(↑d : ℤ))
⊢ ∃ (n : ℕ), a ≤ (↑n : ℤ√(↑d : ℤ))

Tactic:
obtain ⟨x, y, (h : a ≤ ⟨x, y⟩)⟩ : ∃ x y : ℕ, Nonneg (⟨x, y⟩ + -a) :=
    match -a with
    | ⟨Int.ofNat x, Int.ofNat y⟩ => ⟨0, 0, by trivial⟩
    | ⟨Int.ofNat x, -[y+1]⟩ => ⟨0, y + 1, by simp [Int.negSucc_eq, add_assoc, Nonneg, Nonnegg]⟩
    | ⟨-[x+1], Int.ofNat y⟩ => ⟨x + 1, 0, by simp [Int.negSucc_eq, add_assoc, Nonneg, Nonnegg]⟩
    | ⟨-[x+1], -[y+1]⟩ => ⟨x + 1, y + 1, by simp [Int.negSucc_eq, add_assoc, Nonneg, Nonnegg]⟩

Premises used: HAdd.hAdd, Zsqrtd.Nonneg, Neg.neg
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
a : ℤ√(↑d : ℤ)
x y : ℕ
h : a ≤ { re := (↑x : ℤ), im := (↑y : ℤ) }
⊢ ∃ (n : ℕ), a ≤ (↑n : ℤ√(↑d : ℤ))

Tactic:
⟨x + d * y, h.trans ?_⟩

Premises used: HMul.hMul, HAdd.hAdd, Exists.intro, LE.le.trans
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
a : ℤ√(↑d : ℤ)
x y : ℕ
h : a ≤ { re := (↑x : ℤ), im := (↑y : ℤ) }
refine : LE.le (α := ℤ√(↑d : ℤ)) { re := (↑x : ℤ), im := (↑y : ℤ) } (↑(x + d * y) : ℤ√(↑d : ℤ))
⊢ ∃ (n : ℕ), a ≤ (↑n : ℤ√(↑d : ℤ))

Tactic:
refine ⟨x + d * y, h.trans ?_⟩
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
a : ℤ√(↑d : ℤ)
x y : ℕ
h : a ≤ { re := (↑x : ℤ), im := (↑y : ℤ) }
zero :
  ∀ (h : a ≤ { re := (↑x : ℤ), im := (↑0 : ℤ) }),
    Nonneg (d := d)
      { re := (↑x : ℤ) + HMul.hMul (α := ℤ) (↑d : ℤ) (↑0 : ℤ) - (↑x : ℤ), im := HSub.hSub (α := ℤ) 0 (↑0 : ℤ) }
succ :
  ∀ (y : ℕ) (h : a ≤ { re := (↑x : ℤ), im := (↑(y + 1) : ℤ) }),
    Nonneg (d := d)
      { re := (↑x : ℤ) + HMul.hMul (α := ℤ) (↑d : ℤ) (↑(y + 1) : ℤ) - (↑x : ℤ),
        im := HSub.hSub (α := ℤ) 0 (↑(y + 1) : ℤ) }
⊢ Nonneg (d := d)
    { re := (↑x : ℤ) + HMul.hMul (α := ℤ) (↑d : ℤ) (↑y : ℤ) - (↑x : ℤ), im := HSub.hSub (α := ℤ) 0 (↑y : ℤ) }

Tactic:
rcases y with - | y
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
a : ℤ√(↑d : ℤ)
x : ℕ
h : a ≤ { re := (↑x : ℤ), im := (↑0 : ℤ) }
zero : Nonneg (d := d) { re := 0, im := 0 }
⊢ Nonneg (d := d)
    { re := (↑x : ℤ) + HMul.hMul (α := ℤ) (↑d : ℤ) (↑0 : ℤ) - (↑x : ℤ), im := HSub.hSub (α := ℤ) 0 (↑0 : ℤ) }

Tactic:
simp only [Nat.cast_zero, mul_zero, add_zero, sub_self]

Premises used: sub_self, MulZeroClass.mul_zero, Nat.cast_zero, add_zero
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
a : ℤ√(↑d : ℤ)
x : ℕ
h : a ≤ { re := (↑x : ℤ), im := (↑0 : ℤ) }
⊢ Nonneg (d := d) { re := 0, im := 0 }

Tactic:
trivial
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
a : ℤ√(↑d : ℤ)
x y_1 : ℕ
h : a ≤ { re := (↑x : ℤ), im := (↑(y_1 + 1) : ℤ) }
y : ℕ
⊢ SqLe y d (d * y) 1

Tactic:
simpa [SqLe, mul_comm, mul_left_comm] using Nat.mul_le_mul_right (y * y) (Nat.le_mul_self d)

Premises used: HMul.hMul, Nat.mul_le_mul_right, mul_left_comm, mul_comm, Nat.le_mul_self, Zsqrtd.SqLe
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
a : ℤ√(↑d : ℤ)
x y : ℕ
h : a ≤ { re := (↑x : ℤ), im := (↑(y + 1) : ℤ) }
⊢ ∀ (y : ℕ), SqLe y d (d * y) 1

Tactic:
have h : ∀ y, SqLe y d (d * y) 1 := fun y => by
    simpa [SqLe, mul_comm, mul_left_comm] using Nat.mul_le_mul_right (y * y) (Nat.le_mul_self d)
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
a : ℤ√(↑d : ℤ)
x y : ℕ
h_1 : a ≤ { re := (↑x : ℤ), im := (↑(y + 1) : ℤ) }
h : ∀ (y : ℕ), SqLe y d (d * y) 1
⊢ (↑x : ℤ) + HMul.hMul (α := ℤ) (↑d : ℤ) (↑y.succ : ℤ) - (↑x : ℤ) = HMul.hMul (α := ℤ) (↑d : ℤ) (↑y.succ : ℤ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
a : ℤ√(↑d : ℤ)
x y : ℕ
h_1 : a ≤ { re := (↑x : ℤ), im := (↑(y + 1) : ℤ) }
h : ∀ (y : ℕ), SqLe y d (d * y) 1
succ : Nonneg (d := d) { re := HMul.hMul (α := ℤ) (↑d : ℤ) (↑y.succ : ℤ), im := HSub.hSub (α := ℤ) 0 (↑(y + 1) : ℤ) }
⊢ Nonneg (d := d)
    { re := (↑x : ℤ) + HMul.hMul (α := ℤ) (↑d : ℤ) (↑(y + 1) : ℤ) - (↑x : ℤ),
      im := HSub.hSub (α := ℤ) 0 (↑(y + 1) : ℤ) }

Tactic:
rw [show (x : ℤ) + d * Nat.succ y - x = d * Nat.succ y by simp]
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
a : ℤ√(↑d : ℤ)
x y : ℕ
h_1 : a ≤ { re := (↑x : ℤ), im := (↑(y + 1) : ℤ) }
h : ∀ (y : ℕ), SqLe y d (d * y) 1
⊢ Nonneg (d := d) { re := HMul.hMul (α := ℤ) (↑d : ℤ) (↑y.succ : ℤ), im := HSub.hSub (α := ℤ) 0 (↑(y + 1) : ℤ) }

Tactic:
h (y + 1)

Premises used: Zsqrtd.Nonnegg, HAdd.hAdd, Zsqrtd.Nonneg, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
a : ℤ√(↑d : ℤ)
x y : ℕ
h_1 : a ≤ { re := (↑x : ℤ), im := (↑(y + 1) : ℤ) }
h : ∀ (y : ℕ), SqLe y d (d * y) 1
⊢ Nonneg (d := d) { re := HMul.hMul (α := ℤ) (↑d : ℤ) (↑y.succ : ℤ), im := HSub.hSub (α := ℤ) 0 (↑(y + 1) : ℤ) }

Tactic:
exact h (y + 1)

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
a b : ℤ√(↑d : ℤ)
ab : a ≤ b
c : ℤ√(↑d : ℤ)
rwa rwa₁ rwa₂ rwa₃ : (b - a).Nonneg
⊢ (b + c - (a + c)).Nonneg

Tactic:
rwa [add_sub_add_right_eq_sub]

Premises used: add_sub_add_right_eq_sub
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
a : ℤ√(↑d : ℤ)
n : ℕ
ha : a.Nonneg
x y : ℕ
h : Nonneg (d := d) { re := (↑x : ℤ), im := (↑y : ℤ) }
rw : Nonneg (d := d) { re := HMul.hMul (α := ℤ) (↑n : ℤ) (↑x : ℤ), im := HMul.hMul (α := ℤ) (↑n : ℤ) (↑y : ℤ) }
⊢ (HMul.hMul (α := ℤ√(↑d : ℤ)) (↑(↑n : ℤ) : ℤ√(↑d : ℤ)) { re := (↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) }).Nonneg

Tactic:
rw [smul_val]

Premises used: Zsqrtd.smul_val
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
a : ℤ√(↑d : ℤ)
n : ℕ
ha : a.Nonneg
x y : ℕ
h : Nonneg (d := d) { re := (↑x : ℤ), im := (↑y : ℤ) }
⊢ Nonneg (d := d) { re := HMul.hMul (α := ℤ) (↑n : ℤ) (↑x : ℤ), im := HMul.hMul (α := ℤ) (↑n : ℤ) (↑y : ℤ) }

Tactic:
trivial
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
a : ℤ√(↑d : ℤ)
n : ℕ
ha_1 : a.Nonneg
x y : ℕ
ha : Nonneg (d := d) { re := (↑x : ℤ), im := -(↑y : ℤ) }
rw : Nonneg (d := d) { re := HMul.hMul (α := ℤ) (↑n : ℤ) (↑x : ℤ), im := HMul.hMul (α := ℤ) (↑n : ℤ) (-(↑y : ℤ)) }
⊢ (HMul.hMul (α := ℤ√(↑d : ℤ)) (↑(↑n : ℤ) : ℤ√(↑d : ℤ)) { re := (↑x : ℤ), im := -(↑y : ℤ) : ℤ√(↑d : ℤ) }).Nonneg

Tactic:
rw [smul_val]

Premises used: Zsqrtd.smul_val
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
a : ℤ√(↑d : ℤ)
n : ℕ
ha_1 : a.Nonneg
x y : ℕ
ha : Nonneg (d := d) { re := (↑x : ℤ), im := -(↑y : ℤ) }
⊢ Nonneg (d := d) { re := HMul.hMul (α := ℤ) (↑n : ℤ) (↑x : ℤ), im := HMul.hMul (α := ℤ) (↑n : ℤ) (-(↑y : ℤ)) }

Tactic:
simpa using nonnegg_pos_neg.2 (sqLe_smul n <| nonnegg_pos_neg.1 ha)

Premises used: Iff.mpr, Zsqrtd.sqLe_smul, Iff.mp, Zsqrtd.nonnegg_pos_neg
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
a : ℤ√(↑d : ℤ)
n : ℕ
ha_1 : a.Nonneg
x y : ℕ
ha : Nonneg (d := d) { re := -(↑x : ℤ), im := (↑y : ℤ) }
rw : Nonneg (d := d) { re := HMul.hMul (α := ℤ) (↑n : ℤ) (-(↑x : ℤ)), im := HMul.hMul (α := ℤ) (↑n : ℤ) (↑y : ℤ) }
⊢ (HMul.hMul (α := ℤ√(↑d : ℤ)) (↑(↑n : ℤ) : ℤ√(↑d : ℤ)) { re := -(↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) }).Nonneg

Tactic:
rw [smul_val]

Premises used: Zsqrtd.smul_val
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
a : ℤ√(↑d : ℤ)
n : ℕ
ha_1 : a.Nonneg
x y : ℕ
ha : Nonneg (d := d) { re := -(↑x : ℤ), im := (↑y : ℤ) }
⊢ Nonneg (d := d) { re := HMul.hMul (α := ℤ) (↑n : ℤ) (-(↑x : ℤ)), im := HMul.hMul (α := ℤ) (↑n : ℤ) (↑y : ℤ) }

Tactic:
simpa using nonnegg_neg_pos.2 (sqLe_smul n <| nonnegg_neg_pos.1 ha)

Premises used: Iff.mpr, Zsqrtd.nonnegg_neg_pos, Zsqrtd.sqLe_smul, Iff.mp
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
a : ℤ√(↑d : ℤ)
n : ℕ
ha : a.Nonneg
⊢ ((↑(↑n : ℤ) : ℤ√(↑d : ℤ)) * a).Nonneg

Tactic:
exact
    match a, nonneg_cases ha, ha with
    | _, ⟨x, y, Or.inl rfl⟩, _ => by rw [smul_val]; trivial
    | _, ⟨x, y, Or.inr <| Or.inl rfl⟩, ha => by
      rw [smul_val]; simpa using nonnegg_pos_neg.2 (sqLe_smul n <| nonnegg_pos_neg.1 ha)
    | _, ⟨x, y, Or.inr <| Or.inr rfl⟩, ha => by
      rw [smul_val]; simpa using nonnegg_neg_pos.2 (sqLe_smul n <| nonnegg_neg_pos.1 ha)
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
a : ℤ√(↑d : ℤ)
ha_1 : a.Nonneg
x y : ℕ
ha : Nonneg (d := d) { re := (↑x : ℤ), im := -(↑y : ℤ) }
simp : Nonneg (d := d) { re := -HMul.hMul (α := ℤ) (↑d : ℤ) (↑y : ℤ), im := (↑x : ℤ) }
⊢ (HMul.hMul (α := ℤ√(↑d : ℤ)) sqrtd { re := (↑x : ℤ), im := -(↑y : ℤ) : ℤ√(↑d : ℤ) }).Nonneg

Tactic:
simp only [muld_val, mul_neg]

Premises used: Zsqrtd.muld_val, mul_neg
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
a : ℤ√(↑d : ℤ)
ha_1 : a.Nonneg
x y : ℕ
ha : Nonneg (d := d) { re := (↑x : ℤ), im := -(↑y : ℤ) }
apply : SqLe (d * y) 1 x d
⊢ Nonneg (d := d) { re := -HMul.hMul (α := ℤ) (↑d : ℤ) (↑y : ℤ), im := (↑x : ℤ) }

Tactic:
apply nonnegg_neg_pos.2

Premises used: Iff.mpr, Zsqrtd.nonnegg_neg_pos
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
a : ℤ√(↑d : ℤ)
ha_1 : a.Nonneg
x y : ℕ
ha : Nonneg (d := d) { re := (↑x : ℤ), im := -(↑y : ℤ) }
⊢ SqLe (d * y) 1 x d

Tactic:
simpa [SqLe, mul_comm, mul_left_comm] using Nat.mul_le_mul_left d (nonnegg_pos_neg.1 ha)

Premises used: Nat.mul_le_mul_left, mul_left_comm, Iff.mp, mul_comm, Zsqrtd.SqLe, Zsqrtd.nonnegg_pos_neg
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
a : ℤ√(↑d : ℤ)
ha_1 : a.Nonneg
x y : ℕ
ha : Nonneg (d := d) { re := -(↑x : ℤ), im := (↑y : ℤ) }
simp : Nonneg (d := d) { re := HMul.hMul (α := ℤ) (↑d : ℤ) (↑y : ℤ), im := -(↑x : ℤ) }
⊢ (HMul.hMul (α := ℤ√(↑d : ℤ)) sqrtd { re := -(↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) }).Nonneg

Tactic:
simp only [muld_val]

Premises used: Zsqrtd.muld_val
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
a : ℤ√(↑d : ℤ)
ha_1 : a.Nonneg
x y : ℕ
ha : Nonneg (d := d) { re := -(↑x : ℤ), im := (↑y : ℤ) }
apply : SqLe x d (d * y) 1
⊢ Nonneg (d := d) { re := HMul.hMul (α := ℤ) (↑d : ℤ) (↑y : ℤ), im := -(↑x : ℤ) }

Tactic:
apply nonnegg_pos_neg.2

Premises used: Iff.mpr, Zsqrtd.nonnegg_pos_neg
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
a : ℤ√(↑d : ℤ)
ha_1 : a.Nonneg
x y : ℕ
ha : Nonneg (d := d) { re := -(↑x : ℤ), im := (↑y : ℤ) }
⊢ SqLe x d (d * y) 1

Tactic:
simpa [SqLe, mul_comm, mul_left_comm] using Nat.mul_le_mul_left d (nonnegg_neg_pos.1 ha)

Premises used: Nat.mul_le_mul_left, mul_left_comm, Zsqrtd.nonnegg_neg_pos, Iff.mp, mul_comm, Zsqrtd.SqLe
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y : ℕ
a : ℤ√(↑d : ℤ)
ha : a.Nonneg
rw :
  ((↑(↑x : ℤ) : ℤ√(↑d : ℤ)) + HMul.hMul (α := ℤ√(↑d : ℤ)) sqrtd (↑(↑y : ℤ) : ℤ√(↑d : ℤ))) * a =
    (↑x : ℤ√(↑d : ℤ)) * a + sqrtd * ((↑y : ℤ√(↑d : ℤ)) * a)
rw₁ :
  (↑(↑x : ℤ) : ℤ√(↑d : ℤ)) * a + HMul.hMul (α := ℤ√(↑d : ℤ)) sqrtd (↑(↑y : ℤ) : ℤ√(↑d : ℤ)) * a =
    (↑x : ℤ√(↑d : ℤ)) * a + sqrtd * ((↑y : ℤ√(↑d : ℤ)) * a)
rw₂ :
  (↑(↑x : ℤ) : ℤ√(↑d : ℤ)) * a + sqrtd * ((↑(↑y : ℤ) : ℤ√(↑d : ℤ)) * a) =
    (↑x : ℤ√(↑d : ℤ)) * a + sqrtd * ((↑y : ℤ√(↑d : ℤ)) * a)
rw₃ :
  (↑x : ℤ√(↑d : ℤ)) * a + sqrtd * ((↑(↑y : ℤ) : ℤ√(↑d : ℤ)) * a) =
    (↑x : ℤ√(↑d : ℤ)) * a + sqrtd * ((↑y : ℤ√(↑d : ℤ)) * a)
rw₄ rw₅ :
  (↑x : ℤ√(↑d : ℤ)) * a + sqrtd * ((↑y : ℤ√(↑d : ℤ)) * a) = (↑x : ℤ√(↑d : ℤ)) * a + sqrtd * ((↑y : ℤ√(↑d : ℤ)) * a)
⊢ { re := (↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) } * a = (↑x : ℤ√(↑d : ℤ)) * a + sqrtd * ((↑y : ℤ√(↑d : ℤ)) * a)

Tactic:
rw [decompose, right_distrib, mul_assoc, Int.cast_natCast, Int.cast_natCast]

Premises used: Int.cast_natCast, mul_assoc, Zsqrtd.decompose, right_distrib
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y : ℕ
a : ℤ√(↑d : ℤ)
ha : a.Nonneg
⊢ { re := (↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) } * a = (↑x : ℤ√(↑d : ℤ)) * a + sqrtd * ((↑y : ℤ√(↑d : ℤ)) * a)

Tactic:
have : (⟨x, y⟩ * a : ℤ√d) = (x : ℤ√d) * a + sqrtd * ((y : ℤ√d) * a) := by
    rw [decompose, right_distrib, mul_assoc, Int.cast_natCast, Int.cast_natCast]
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y : ℕ
a : ℤ√(↑d : ℤ)
ha : a.Nonneg
this : { re := (↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) } * a = (↑x : ℤ√(↑d : ℤ)) * a + sqrtd * ((↑y : ℤ√(↑d : ℤ)) * a)
rw : ((↑x : ℤ√(↑d : ℤ)) * a + sqrtd * ((↑y : ℤ√(↑d : ℤ)) * a)).Nonneg
⊢ ({ re := (↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) } * a).Nonneg

Tactic:
rw [this]
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y : ℕ
a : ℤ√(↑d : ℤ)
ha : a.Nonneg
this : { re := (↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) } * a = (↑x : ℤ√(↑d : ℤ)) * a + sqrtd * ((↑y : ℤ√(↑d : ℤ)) * a)
⊢ ((↑x : ℤ√(↑d : ℤ)) * a + sqrtd * ((↑y : ℤ√(↑d : ℤ)) * a)).Nonneg

Tactic:
(nonneg_smul ha).add (nonneg_muld <| nonneg_smul ha)

Premises used: Zsqrtd.nonneg_smul, Zsqrtd.Nonneg.add, Zsqrtd.nonneg_muld
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y : ℕ
a : ℤ√(↑d : ℤ)
ha : a.Nonneg
this : { re := (↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) } * a = (↑x : ℤ√(↑d : ℤ)) * a + sqrtd * ((↑y : ℤ√(↑d : ℤ)) * a)
⊢ ((↑x : ℤ√(↑d : ℤ)) * a + sqrtd * ((↑y : ℤ√(↑d : ℤ)) * a)).Nonneg

Tactic:
exact (nonneg_smul ha).add (nonneg_muld <| nonneg_smul ha)

Premises used: Zsqrtd.nonneg_smul, Zsqrtd.Nonneg.add, Zsqrtd.nonneg_muld
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
a b : ℤ√(↑d : ℤ)
ha_1 : a.Nonneg
hb : b.Nonneg
x y z w : ℕ
ha : Nonneg (d := d) { re := -(↑x : ℤ), im := (↑y : ℤ) }
h : Nonneg (d := d) { re := (↑z : ℤ), im := (↑w : ℤ) }
rw :
  (HMul.hMul (α := ℤ√(↑d : ℤ)) { re := (↑z : ℤ), im := (↑w : ℤ) : ℤ√(↑d : ℤ) }
      { re := -(↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) }).Nonneg
⊢ (HMul.hMul (α := ℤ√(↑d : ℤ)) { re := -(↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) }
      { re := (↑z : ℤ), im := (↑w : ℤ) : ℤ√(↑d : ℤ) }).Nonneg

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
a b : ℤ√(↑d : ℤ)
ha_1 : a.Nonneg
hb : b.Nonneg
x y z w : ℕ
ha : Nonneg (d := d) { re := -(↑x : ℤ), im := (↑y : ℤ) }
h : Nonneg (d := d) { re := (↑z : ℤ), im := (↑w : ℤ) }
⊢ (HMul.hMul (α := ℤ√(↑d : ℤ)) { re := (↑z : ℤ), im := (↑w : ℤ) : ℤ√(↑d : ℤ) }
      { re := -(↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) }).Nonneg

Tactic:
nonneg_mul_lem ha

Premises used: Zsqrtd.nonneg_mul_lem
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
a b : ℤ√(↑d : ℤ)
ha_1 : a.Nonneg
hb : b.Nonneg
x y z w : ℕ
ha : Nonneg (d := d) { re := -(↑x : ℤ), im := (↑y : ℤ) }
h : Nonneg (d := d) { re := (↑z : ℤ), im := (↑w : ℤ) }
⊢ (HMul.hMul (α := ℤ√(↑d : ℤ)) { re := (↑z : ℤ), im := (↑w : ℤ) : ℤ√(↑d : ℤ) }
      { re := -(↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) }).Nonneg

Tactic:
exact nonneg_mul_lem ha

Premises used: Zsqrtd.nonneg_mul_lem
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
a b : ℤ√(↑d : ℤ)
ha_1 : a.Nonneg
hb : b.Nonneg
x y z w : ℕ
ha : Nonneg (d := d) { re := (↑x : ℤ), im := -(↑y : ℤ) }
h : Nonneg (d := d) { re := (↑z : ℤ), im := (↑w : ℤ) }
rw :
  (HMul.hMul (α := ℤ√(↑d : ℤ)) { re := (↑z : ℤ), im := (↑w : ℤ) : ℤ√(↑d : ℤ) }
      { re := (↑x : ℤ), im := -(↑y : ℤ) : ℤ√(↑d : ℤ) }).Nonneg
⊢ (HMul.hMul (α := ℤ√(↑d : ℤ)) { re := (↑x : ℤ), im := -(↑y : ℤ) : ℤ√(↑d : ℤ) }
      { re := (↑z : ℤ), im := (↑w : ℤ) : ℤ√(↑d : ℤ) }).Nonneg

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
a b : ℤ√(↑d : ℤ)
ha_1 : a.Nonneg
hb : b.Nonneg
x y z w : ℕ
ha : Nonneg (d := d) { re := (↑x : ℤ), im := -(↑y : ℤ) }
h : Nonneg (d := d) { re := (↑z : ℤ), im := (↑w : ℤ) }
⊢ (HMul.hMul (α := ℤ√(↑d : ℤ)) { re := (↑z : ℤ), im := (↑w : ℤ) : ℤ√(↑d : ℤ) }
      { re := (↑x : ℤ), im := -(↑y : ℤ) : ℤ√(↑d : ℤ) }).Nonneg

Tactic:
nonneg_mul_lem ha

Premises used: Zsqrtd.nonneg_mul_lem
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
a b : ℤ√(↑d : ℤ)
ha_1 : a.Nonneg
hb : b.Nonneg
x y z w : ℕ
ha : Nonneg (d := d) { re := (↑x : ℤ), im := -(↑y : ℤ) }
h : Nonneg (d := d) { re := (↑z : ℤ), im := (↑w : ℤ) }
⊢ (HMul.hMul (α := ℤ√(↑d : ℤ)) { re := (↑z : ℤ), im := (↑w : ℤ) : ℤ√(↑d : ℤ) }
      { re := (↑x : ℤ), im := -(↑y : ℤ) : ℤ√(↑d : ℤ) }).Nonneg

Tactic:
exact nonneg_mul_lem ha

Premises used: Zsqrtd.nonneg_mul_lem
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
a b : ℤ√(↑d : ℤ)
ha_1 : a.Nonneg
hb_1 : b.Nonneg
x y z w : ℕ
ha : Nonneg (d := d) { re := -(↑x : ℤ), im := (↑y : ℤ) }
hb : Nonneg (d := d) { re := -(↑z : ℤ), im := (↑w : ℤ) }
⊢ Eq (α := ℤ√(↑d : ℤ))
    {
      re :=
        re (d := (↑d : ℤ)) { re := -(↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) } *
            re (d := (↑d : ℤ)) { re := -(↑z : ℤ), im := (↑w : ℤ) : ℤ√(↑d : ℤ) } +
          (↑d : ℤ) * im (d := (↑d : ℤ)) { re := -(↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) } *
            im (d := (↑d : ℤ)) { re := -(↑z : ℤ), im := (↑w : ℤ) : ℤ√(↑d : ℤ) },
      im :=
        re (d := (↑d : ℤ)) { re := -(↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) } *
            im (d := (↑d : ℤ)) { re := -(↑z : ℤ), im := (↑w : ℤ) : ℤ√(↑d : ℤ) } +
          im (d := (↑d : ℤ)) { re := -(↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) } *
            re (d := (↑d : ℤ)) { re := -(↑z : ℤ), im := (↑w : ℤ) : ℤ√(↑d : ℤ) } }
    { re := HMul.hMul (α := ℤ) (↑x : ℤ) (↑z : ℤ) + HMul.hMul (α := ℤ) (↑d : ℤ) (↑y : ℤ) * (↑w : ℤ),
      im := -(HMul.hMul (α := ℤ) (↑x : ℤ) (↑w : ℤ) + HMul.hMul (α := ℤ) (↑y : ℤ) (↑z : ℤ)) }

Tactic:
simp [add_comm]

Premises used: add_comm
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
a b : ℤ√(↑d : ℤ)
ha_1 : a.Nonneg
hb_1 : b.Nonneg
x y z w : ℕ
ha : Nonneg (d := d) { re := -(↑x : ℤ), im := (↑y : ℤ) }
hb : Nonneg (d := d) { re := -(↑z : ℤ), im := (↑w : ℤ) }
rw :
  Nonneg (d := d)
    { re := HMul.hMul (α := ℤ) (↑x : ℤ) (↑z : ℤ) + HMul.hMul (α := ℤ) (↑d : ℤ) (↑y : ℤ) * (↑w : ℤ),
      im := -(HMul.hMul (α := ℤ) (↑x : ℤ) (↑w : ℤ) + HMul.hMul (α := ℤ) (↑y : ℤ) (↑z : ℤ)) }
⊢ (HMul.hMul (α := ℤ√(↑d : ℤ)) { re := -(↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) }
      { re := -(↑z : ℤ), im := (↑w : ℤ) : ℤ√(↑d : ℤ) }).Nonneg

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

Premises used: HMul.hMul, rfl
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
a b : ℤ√(↑d : ℤ)
ha_1 : a.Nonneg
hb_1 : b.Nonneg
x y z w : ℕ
ha : Nonneg (d := d) { re := -(↑x : ℤ), im := (↑y : ℤ) }
hb : Nonneg (d := d) { re := -(↑z : ℤ), im := (↑w : ℤ) }
⊢ Nonneg (d := d)
    { re := HMul.hMul (α := ℤ) (↑x : ℤ) (↑z : ℤ) + HMul.hMul (α := ℤ) (↑d : ℤ) (↑y : ℤ) * (↑w : ℤ),
      im := -(HMul.hMul (α := ℤ) (↑x : ℤ) (↑w : ℤ) + HMul.hMul (α := ℤ) (↑y : ℤ) (↑z : ℤ)) }

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

Premises used: Iff.mpr, Zsqrtd.sqLe_mul, And.left, Zsqrtd.nonnegg_neg_pos, Iff.mp, Zsqrtd.nonnegg_pos_neg, Zsqrtd.Nonneg, Int.add