awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y z w : ℕ
xy : SqLe x 1 y d
zw : SqLe w d z 1
⊢ 0 ≤
    HSub.hSub (α := ℤ) (↑(d * y * y) : ℤ) (↑(1 * x * x) : ℤ) * HSub.hSub (α := ℤ) (↑(1 * z * z) : ℤ) (↑(d * w * w) : ℤ)

Tactic:
have :=
        Int.mul_nonneg (sub_nonneg_of_le (Int.ofNat_le_ofNat_of_le xy))
          (sub_nonneg_of_le (Int.ofNat_le_ofNat_of_le zw))
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y z w : ℕ
xy : SqLe x 1 y d
zw : SqLe w d z 1
this :
  0 ≤
    HSub.hSub (α := ℤ) (↑(d * y * y) : ℤ) (↑(1 * x * x) : ℤ) * HSub.hSub (α := ℤ) (↑(1 * z * z) : ℤ) (↑(d * w * w) : ℤ)
⊢ SqLe (x * z + d * y * w) 1 (x * w + y * z) d

Tactic:
Int.le_of_ofNat_le_ofNat (le_of_sub_nonneg ?_)

Premises used: le_of_sub_nonneg, Int.le_of_ofNat_le_ofNat, Zsqrtd.SqLe
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y z w : ℕ
xy : SqLe x 1 y d
zw : SqLe w d z 1
this :
  0 ≤
    HSub.hSub (α := ℤ) (↑(d * y * y) : ℤ) (↑(1 * x * x) : ℤ) * HSub.hSub (α := ℤ) (↑(1 * z * z) : ℤ) (↑(d * w * w) : ℤ)
refine_2 :
  0 ≤
    HSub.hSub (α := ℤ) (↑(d * (x * w + y * z) * (x * w + y * z)) : ℤ)
      (↑(1 * (x * z + d * y * w) * (x * z + d * y * w)) : ℤ)
⊢ SqLe (x * z + d * y * w) 1 (x * w + y * z) d

Tactic:
refine Int.le_of_ofNat_le_ofNat (le_of_sub_nonneg ?_)

Premises used: le_of_sub_nonneg, Int.le_of_ofNat_le_ofNat
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y z w : ℕ
xy : SqLe x 1 y d
zw : SqLe w d z 1
this :
  0 ≤
    HSub.hSub (α := ℤ) (↑(d * y * y) : ℤ) (↑(1 * x * x) : ℤ) * HSub.hSub (α := ℤ) (↑(1 * z * z) : ℤ) (↑(d * w * w) : ℤ)
⊢ 0 ≤
    HSub.hSub (α := ℤ) (↑(d * y * y) : ℤ) (↑(1 * x * x) : ℤ) * HSub.hSub (α := ℤ) (↑(1 * z * z) : ℤ) (↑(d * w * w) : ℤ)

Tactic:
this
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y z w : ℕ
xy : SqLe x 1 y d
zw : SqLe w d z 1
this :
  0 ≤
    HSub.hSub (α := ℤ) (↑(d * y * y) : ℤ) (↑(1 * x * x) : ℤ) * HSub.hSub (α := ℤ) (↑(1 * z * z) : ℤ) (↑(d * w * w) : ℤ)
h :
  HSub.hSub (α := ℤ) (↑(d * (x * w + y * z) * (x * w + y * z)) : ℤ)
      (↑(1 * (x * z + d * y * w) * (x * z + d * y * w)) : ℤ) =
    HSub.hSub (α := ℤ) (↑(d * y * y) : ℤ) (↑(1 * x * x) : ℤ) * HSub.hSub (α := ℤ) (↑(1 * z * z) : ℤ) (↑(d * w * w) : ℤ)
⊢ 0 ≤
    HSub.hSub (α := ℤ) (↑(d * (x * w + y * z) * (x * w + y * z)) : ℤ)
      (↑(1 * (x * z + d * y * w) * (x * z + d * y * w)) : ℤ)

Tactic:
convert! this using 1
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y z w : ℕ
xy : SqLe x 1 y d
zw : SqLe w d z 1
this :
  0 ≤
    HSub.hSub (α := ℤ) (↑(d * y * y) : ℤ) (↑(1 * x * x) : ℤ) * HSub.hSub (α := ℤ) (↑(1 * z * z) : ℤ) (↑(d * w * w) : ℤ)
h :
  (↑d : ℤ) * (HMul.hMul (α := ℤ) (↑x : ℤ) (↑w : ℤ) + HMul.hMul (α := ℤ) (↑y : ℤ) (↑z : ℤ)) *
        (HMul.hMul (α := ℤ) (↑x : ℤ) (↑w : ℤ) + HMul.hMul (α := ℤ) (↑y : ℤ) (↑z : ℤ)) -
      (HMul.hMul (α := ℤ) (↑x : ℤ) (↑z : ℤ) + HMul.hMul (α := ℤ) (↑d : ℤ) (↑y : ℤ) * (↑w : ℤ)) *
        (HMul.hMul (α := ℤ) (↑x : ℤ) (↑z : ℤ) + HMul.hMul (α := ℤ) (↑d : ℤ) (↑y : ℤ) * (↑w : ℤ)) =
    (HMul.hMul (α := ℤ) (↑d : ℤ) (↑y : ℤ) * (↑y : ℤ) - HMul.hMul (α := ℤ) (↑x : ℤ) (↑x : ℤ)) *
      (HMul.hMul (α := ℤ) (↑z : ℤ) (↑z : ℤ) - HMul.hMul (α := ℤ) (↑d : ℤ) (↑w : ℤ) * (↑w : ℤ))
⊢ HSub.hSub (α := ℤ) (↑(d * (x * w + y * z) * (x * w + y * z)) : ℤ)
      (↑(1 * (x * z + d * y * w) * (x * z + d * y * w)) : ℤ) =
    HSub.hSub (α := ℤ) (↑(d * y * y) : ℤ) (↑(1 * x * x) : ℤ) * HSub.hSub (α := ℤ) (↑(1 * z * z) : ℤ) (↑(d * w * w) : ℤ)

Tactic:
simp only [one_mul, Int.natCast_add, Int.natCast_mul]

Premises used: Int.natCast_add, Int.natCast_mul, one_mul
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y z w : ℕ
xy : SqLe x 1 y d
zw : SqLe w d z 1
this :
  0 ≤
    HSub.hSub (α := ℤ) (↑(d * y * y) : ℤ) (↑(1 * x * x) : ℤ) * HSub.hSub (α := ℤ) (↑(1 * z * z) : ℤ) (↑(d * w * w) : ℤ)
⊢ (↑d : ℤ) * (HMul.hMul (α := ℤ) (↑x : ℤ) (↑w : ℤ) + HMul.hMul (α := ℤ) (↑y : ℤ) (↑z : ℤ)) *
        (HMul.hMul (α := ℤ) (↑x : ℤ) (↑w : ℤ) + HMul.hMul (α := ℤ) (↑y : ℤ) (↑z : ℤ)) -
      (HMul.hMul (α := ℤ) (↑x : ℤ) (↑z : ℤ) + HMul.hMul (α := ℤ) (↑d : ℤ) (↑y : ℤ) * (↑w : ℤ)) *
        (HMul.hMul (α := ℤ) (↑x : ℤ) (↑z : ℤ) + HMul.hMul (α := ℤ) (↑d : ℤ) (↑y : ℤ) * (↑w : ℤ)) =
    (HMul.hMul (α := ℤ) (↑d : ℤ) (↑y : ℤ) * (↑y : ℤ) - HMul.hMul (α := ℤ) (↑x : ℤ) (↑x : ℤ)) *
      (HMul.hMul (α := ℤ) (↑z : ℤ) (↑z : ℤ) - HMul.hMul (α := ℤ) (↑d : ℤ) (↑w : ℤ) * (↑w : ℤ))

Tactic:
ring
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y z w : ℕ
xy : SqLe y d x 1
zw : SqLe z 1 w d
⊢ 0 ≤
    HSub.hSub (α := ℤ) (↑(1 * x * x) : ℤ) (↑(d * y * y) : ℤ) * HSub.hSub (α := ℤ) (↑(d * w * w) : ℤ) (↑(1 * z * z) : ℤ)

Tactic:
have :=
        Int.mul_nonneg (sub_nonneg_of_le (Int.ofNat_le_ofNat_of_le xy))
          (sub_nonneg_of_le (Int.ofNat_le_ofNat_of_le zw))
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y z w : ℕ
xy : SqLe y d x 1
zw : SqLe z 1 w d
this :
  0 ≤
    HSub.hSub (α := ℤ) (↑(1 * x * x) : ℤ) (↑(d * y * y) : ℤ) * HSub.hSub (α := ℤ) (↑(d * w * w) : ℤ) (↑(1 * z * z) : ℤ)
⊢ SqLe (x * z + d * y * w) 1 (x * w + y * z) d

Tactic:
Int.le_of_ofNat_le_ofNat (le_of_sub_nonneg ?_)

Premises used: le_of_sub_nonneg, Int.le_of_ofNat_le_ofNat, Zsqrtd.SqLe
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y z w : ℕ
xy : SqLe y d x 1
zw : SqLe z 1 w d
this :
  0 ≤
    HSub.hSub (α := ℤ) (↑(1 * x * x) : ℤ) (↑(d * y * y) : ℤ) * HSub.hSub (α := ℤ) (↑(d * w * w) : ℤ) (↑(1 * z * z) : ℤ)
refine_3 :
  0 ≤
    HSub.hSub (α := ℤ) (↑(d * (x * w + y * z) * (x * w + y * z)) : ℤ)
      (↑(1 * (x * z + d * y * w) * (x * z + d * y * w)) : ℤ)
⊢ SqLe (x * z + d * y * w) 1 (x * w + y * z) d

Tactic:
refine Int.le_of_ofNat_le_ofNat (le_of_sub_nonneg ?_)

Premises used: le_of_sub_nonneg, Int.le_of_ofNat_le_ofNat
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y z w : ℕ
xy : SqLe y d x 1
zw : SqLe z 1 w d
this :
  0 ≤
    HSub.hSub (α := ℤ) (↑(1 * x * x) : ℤ) (↑(d * y * y) : ℤ) * HSub.hSub (α := ℤ) (↑(d * w * w) : ℤ) (↑(1 * z * z) : ℤ)
⊢ 0 ≤
    HSub.hSub (α := ℤ) (↑(1 * x * x) : ℤ) (↑(d * y * y) : ℤ) * HSub.hSub (α := ℤ) (↑(d * w * w) : ℤ) (↑(1 * z * z) : ℤ)

Tactic:
this
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y z w : ℕ
xy : SqLe y d x 1
zw : SqLe z 1 w d
this :
  0 ≤
    HSub.hSub (α := ℤ) (↑(1 * x * x) : ℤ) (↑(d * y * y) : ℤ) * HSub.hSub (α := ℤ) (↑(d * w * w) : ℤ) (↑(1 * z * z) : ℤ)
h :
  HSub.hSub (α := ℤ) (↑(d * (x * w + y * z) * (x * w + y * z)) : ℤ)
      (↑(1 * (x * z + d * y * w) * (x * z + d * y * w)) : ℤ) =
    HSub.hSub (α := ℤ) (↑(1 * x * x) : ℤ) (↑(d * y * y) : ℤ) * HSub.hSub (α := ℤ) (↑(d * w * w) : ℤ) (↑(1 * z * z) : ℤ)
⊢ 0 ≤
    HSub.hSub (α := ℤ) (↑(d * (x * w + y * z) * (x * w + y * z)) : ℤ)
      (↑(1 * (x * z + d * y * w) * (x * z + d * y * w)) : ℤ)

Tactic:
convert! this using 1
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y z w : ℕ
xy : SqLe y d x 1
zw : SqLe z 1 w d
this :
  0 ≤
    HSub.hSub (α := ℤ) (↑(1 * x * x) : ℤ) (↑(d * y * y) : ℤ) * HSub.hSub (α := ℤ) (↑(d * w * w) : ℤ) (↑(1 * z * z) : ℤ)
h :
  (↑d : ℤ) * (HMul.hMul (α := ℤ) (↑x : ℤ) (↑w : ℤ) + HMul.hMul (α := ℤ) (↑y : ℤ) (↑z : ℤ)) *
        (HMul.hMul (α := ℤ) (↑x : ℤ) (↑w : ℤ) + HMul.hMul (α := ℤ) (↑y : ℤ) (↑z : ℤ)) -
      (HMul.hMul (α := ℤ) (↑x : ℤ) (↑z : ℤ) + HMul.hMul (α := ℤ) (↑d : ℤ) (↑y : ℤ) * (↑w : ℤ)) *
        (HMul.hMul (α := ℤ) (↑x : ℤ) (↑z : ℤ) + HMul.hMul (α := ℤ) (↑d : ℤ) (↑y : ℤ) * (↑w : ℤ)) =
    (HMul.hMul (α := ℤ) (↑x : ℤ) (↑x : ℤ) - HMul.hMul (α := ℤ) (↑d : ℤ) (↑y : ℤ) * (↑y : ℤ)) *
      (HMul.hMul (α := ℤ) (↑d : ℤ) (↑w : ℤ) * (↑w : ℤ) - HMul.hMul (α := ℤ) (↑z : ℤ) (↑z : ℤ))
⊢ HSub.hSub (α := ℤ) (↑(d * (x * w + y * z) * (x * w + y * z)) : ℤ)
      (↑(1 * (x * z + d * y * w) * (x * z + d * y * w)) : ℤ) =
    HSub.hSub (α := ℤ) (↑(1 * x * x) : ℤ) (↑(d * y * y) : ℤ) * HSub.hSub (α := ℤ) (↑(d * w * w) : ℤ) (↑(1 * z * z) : ℤ)

Tactic:
simp only [one_mul, Int.natCast_add, Int.natCast_mul]

Premises used: Int.natCast_add, Int.natCast_mul, one_mul
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y z w : ℕ
xy : SqLe y d x 1
zw : SqLe z 1 w d
this :
  0 ≤
    HSub.hSub (α := ℤ) (↑(1 * x * x) : ℤ) (↑(d * y * y) : ℤ) * HSub.hSub (α := ℤ) (↑(d * w * w) : ℤ) (↑(1 * z * z) : ℤ)
⊢ (↑d : ℤ) * (HMul.hMul (α := ℤ) (↑x : ℤ) (↑w : ℤ) + HMul.hMul (α := ℤ) (↑y : ℤ) (↑z : ℤ)) *
        (HMul.hMul (α := ℤ) (↑x : ℤ) (↑w : ℤ) + HMul.hMul (α := ℤ) (↑y : ℤ) (↑z : ℤ)) -
      (HMul.hMul (α := ℤ) (↑x : ℤ) (↑z : ℤ) + HMul.hMul (α := ℤ) (↑d : ℤ) (↑y : ℤ) * (↑w : ℤ)) *
        (HMul.hMul (α := ℤ) (↑x : ℤ) (↑z : ℤ) + HMul.hMul (α := ℤ) (↑d : ℤ) (↑y : ℤ) * (↑w : ℤ)) =
    (HMul.hMul (α := ℤ) (↑x : ℤ) (↑x : ℤ) - HMul.hMul (α := ℤ) (↑d : ℤ) (↑y : ℤ) * (↑y : ℤ)) *
      (HMul.hMul (α := ℤ) (↑d : ℤ) (↑w : ℤ) * (↑w : ℤ) - HMul.hMul (α := ℤ) (↑z : ℤ) (↑z : ℤ))

Tactic:
ring
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y z w : ℕ
xy : SqLe y d x 1
zw : SqLe w d z 1
⊢ 0 ≤
    HSub.hSub (α := ℤ) (↑(1 * x * x) : ℤ) (↑(d * y * y) : ℤ) * HSub.hSub (α := ℤ) (↑(1 * z * z) : ℤ) (↑(d * w * w) : ℤ)

Tactic:
have :=
        Int.mul_nonneg (sub_nonneg_of_le (Int.ofNat_le_ofNat_of_le xy))
          (sub_nonneg_of_le (Int.ofNat_le_ofNat_of_le zw))
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y z w : ℕ
xy : SqLe y d x 1
zw : SqLe w d z 1
this :
  0 ≤
    HSub.hSub (α := ℤ) (↑(1 * x * x) : ℤ) (↑(d * y * y) : ℤ) * HSub.hSub (α := ℤ) (↑(1 * z * z) : ℤ) (↑(d * w * w) : ℤ)
⊢ SqLe (x * w + y * z) d (x * z + d * y * w) 1

Tactic:
Int.le_of_ofNat_le_ofNat (le_of_sub_nonneg ?_)

Premises used: le_of_sub_nonneg, Int.le_of_ofNat_le_ofNat, Zsqrtd.SqLe
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y z w : ℕ
xy : SqLe y d x 1
zw : SqLe w d z 1
this :
  0 ≤
    HSub.hSub (α := ℤ) (↑(1 * x * x) : ℤ) (↑(d * y * y) : ℤ) * HSub.hSub (α := ℤ) (↑(1 * z * z) : ℤ) (↑(d * w * w) : ℤ)
refine_4 :
  0 ≤
    HSub.hSub (α := ℤ) (↑(1 * (x * z + d * y * w) * (x * z + d * y * w)) : ℤ)
      (↑(d * (x * w + y * z) * (x * w + y * z)) : ℤ)
⊢ SqLe (x * w + y * z) d (x * z + d * y * w) 1

Tactic:
refine Int.le_of_ofNat_le_ofNat (le_of_sub_nonneg ?_)

Premises used: le_of_sub_nonneg, Int.le_of_ofNat_le_ofNat
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y z w : ℕ
xy : SqLe y d x 1
zw : SqLe w d z 1
this :
  0 ≤
    HSub.hSub (α := ℤ) (↑(1 * x * x) : ℤ) (↑(d * y * y) : ℤ) * HSub.hSub (α := ℤ) (↑(1 * z * z) : ℤ) (↑(d * w * w) : ℤ)
⊢ 0 ≤
    HSub.hSub (α := ℤ) (↑(1 * x * x) : ℤ) (↑(d * y * y) : ℤ) * HSub.hSub (α := ℤ) (↑(1 * z * z) : ℤ) (↑(d * w * w) : ℤ)

Tactic:
this
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y z w : ℕ
xy : SqLe y d x 1
zw : SqLe w d z 1
this :
  0 ≤
    HSub.hSub (α := ℤ) (↑(1 * x * x) : ℤ) (↑(d * y * y) : ℤ) * HSub.hSub (α := ℤ) (↑(1 * z * z) : ℤ) (↑(d * w * w) : ℤ)
h :
  HSub.hSub (α := ℤ) (↑(1 * (x * z + d * y * w) * (x * z + d * y * w)) : ℤ)
      (↑(d * (x * w + y * z) * (x * w + y * z)) : ℤ) =
    HSub.hSub (α := ℤ) (↑(1 * x * x) : ℤ) (↑(d * y * y) : ℤ) * HSub.hSub (α := ℤ) (↑(1 * z * z) : ℤ) (↑(d * w * w) : ℤ)
⊢ 0 ≤
    HSub.hSub (α := ℤ) (↑(1 * (x * z + d * y * w) * (x * z + d * y * w)) : ℤ)
      (↑(d * (x * w + y * z) * (x * w + y * z)) : ℤ)

Tactic:
convert! this using 1
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y z w : ℕ
xy : SqLe y d x 1
zw : SqLe w d z 1
this :
  0 ≤
    HSub.hSub (α := ℤ) (↑(1 * x * x) : ℤ) (↑(d * y * y) : ℤ) * HSub.hSub (α := ℤ) (↑(1 * z * z) : ℤ) (↑(d * w * w) : ℤ)
h :
  (HMul.hMul (α := ℤ) (↑x : ℤ) (↑z : ℤ) + HMul.hMul (α := ℤ) (↑d : ℤ) (↑y : ℤ) * (↑w : ℤ)) *
        (HMul.hMul (α := ℤ) (↑x : ℤ) (↑z : ℤ) + HMul.hMul (α := ℤ) (↑d : ℤ) (↑y : ℤ) * (↑w : ℤ)) -
      (↑d : ℤ) * (HMul.hMul (α := ℤ) (↑x : ℤ) (↑w : ℤ) + HMul.hMul (α := ℤ) (↑y : ℤ) (↑z : ℤ)) *
        (HMul.hMul (α := ℤ) (↑x : ℤ) (↑w : ℤ) + HMul.hMul (α := ℤ) (↑y : ℤ) (↑z : ℤ)) =
    (HMul.hMul (α := ℤ) (↑x : ℤ) (↑x : ℤ) - HMul.hMul (α := ℤ) (↑d : ℤ) (↑y : ℤ) * (↑y : ℤ)) *
      (HMul.hMul (α := ℤ) (↑z : ℤ) (↑z : ℤ) - HMul.hMul (α := ℤ) (↑d : ℤ) (↑w : ℤ) * (↑w : ℤ))
⊢ HSub.hSub (α := ℤ) (↑(1 * (x * z + d * y * w) * (x * z + d * y * w)) : ℤ)
      (↑(d * (x * w + y * z) * (x * w + y * z)) : ℤ) =
    HSub.hSub (α := ℤ) (↑(1 * x * x) : ℤ) (↑(d * y * y) : ℤ) * HSub.hSub (α := ℤ) (↑(1 * z * z) : ℤ) (↑(d * w * w) : ℤ)

Tactic:
simp only [one_mul, Int.natCast_add, Int.natCast_mul]

Premises used: Int.natCast_add, Int.natCast_mul, one_mul
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y z w : ℕ
xy : SqLe y d x 1
zw : SqLe w d z 1
this :
  0 ≤
    HSub.hSub (α := ℤ) (↑(1 * x * x) : ℤ) (↑(d * y * y) : ℤ) * HSub.hSub (α := ℤ) (↑(1 * z * z) : ℤ) (↑(d * w * w) : ℤ)
⊢ (HMul.hMul (α := ℤ) (↑x : ℤ) (↑z : ℤ) + HMul.hMul (α := ℤ) (↑d : ℤ) (↑y : ℤ) * (↑w : ℤ)) *
        (HMul.hMul (α := ℤ) (↑x : ℤ) (↑z : ℤ) + HMul.hMul (α := ℤ) (↑d : ℤ) (↑y : ℤ) * (↑w : ℤ)) -
      (↑d : ℤ) * (HMul.hMul (α := ℤ) (↑x : ℤ) (↑w : ℤ) + HMul.hMul (α := ℤ) (↑y : ℤ) (↑z : ℤ)) *
        (HMul.hMul (α := ℤ) (↑x : ℤ) (↑w : ℤ) + HMul.hMul (α := ℤ) (↑y : ℤ) (↑z : ℤ)) =
    (HMul.hMul (α := ℤ) (↑x : ℤ) (↑x : ℤ) - HMul.hMul (α := ℤ) (↑d : ℤ) (↑y : ℤ) * (↑y : ℤ)) *
      (HMul.hMul (α := ℤ) (↑z : ℤ) (↑z : ℤ) - HMul.hMul (α := ℤ) (↑d : ℤ) (↑w : ℤ) * (↑w : ℤ))

Tactic:
ring
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
c d : ℕ
x y : ℤ
ofNat : ∀ (a : ℕ), Nonnegg c d (Int.ofNat a) y = Nonnegg d c y (Int.ofNat a)
negSucc : ∀ (a : ℕ), Nonnegg c d (Int.negSucc a) y = Nonnegg d c y (Int.negSucc a)
⊢ Nonnegg c d x y = Nonnegg d c y x

Tactic:
cases x
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
c d : ℕ
y : ℤ
a : ℕ
ofNat : ∀ (a_1 : ℕ), Nonnegg c d (Int.ofNat a) (Int.ofNat a_1) = Nonnegg d c (Int.ofNat a_1) (Int.ofNat a)
ofNat₁ : ∀ (a_1 : ℕ), Nonnegg c d (Int.ofNat a) (Int.negSucc a_1) = Nonnegg d c (Int.negSucc a_1) (Int.ofNat a)
⊢ Nonnegg c d (Int.ofNat a) y = Nonnegg d c y (Int.ofNat a)

Tactic:
cases y
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
c d : ℕ
y : ℤ
a : ℕ
negSucc : ∀ (a_1 : ℕ), Nonnegg c d (Int.negSucc a) (Int.ofNat a_1) = Nonnegg d c (Int.ofNat a_1) (Int.negSucc a)
negSucc₁ : ∀ (a_1 : ℕ), Nonnegg c d (Int.negSucc a) (Int.negSucc a_1) = Nonnegg d c (Int.negSucc a_1) (Int.negSucc a)
⊢ Nonnegg c d (Int.negSucc a) y = Nonnegg d c y (Int.negSucc a)

Tactic:
cases y
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
c d a a_1 : ℕ
⊢ Nonnegg c d (Int.ofNat a) (Int.ofNat a_1) = Nonnegg d c (Int.ofNat a_1) (Int.ofNat a)

Tactic:
rfl
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
c d a a_1 : ℕ
⊢ Nonnegg c d (Int.ofNat a) (Int.negSucc a_1) = Nonnegg d c (Int.negSucc a_1) (Int.ofNat a)

Tactic:
rfl
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
c d a a_1 : ℕ
⊢ Nonnegg c d (Int.negSucc a) (Int.ofNat a_1) = Nonnegg d c (Int.ofNat a_1) (Int.negSucc a)

Tactic:
rfl
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
c d a a_1 : ℕ
⊢ Nonnegg c d (Int.negSucc a) (Int.negSucc a_1) = Nonnegg d c (Int.negSucc a_1) (Int.negSucc a)

Tactic:
rfl
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
c d b : ℕ
⊢ Nonnegg c d (-(↑0 : ℤ)) (↑b : ℤ) → SqLe 0 d b c

Tactic:
simp [SqLe]

Premises used: Zsqrtd.SqLe
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
c d a b : ℕ
⊢ Nonnegg c d (-(↑(a + 1) : ℤ)) (↑b : ℤ) ↔ SqLe (a + 1) d b c

Tactic:
rfl
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
c d a b : ℕ
rw : Nonnegg d c (-(↑b : ℤ)) (↑a : ℤ) ↔ SqLe b c a d
⊢ Nonnegg c d (↑a : ℤ) (-(↑b : ℤ)) ↔ SqLe b c a d

Tactic:
rw [nonnegg_comm]

Premises used: Zsqrtd.nonnegg_comm
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
c d a b : ℕ
⊢ Nonnegg d c (-(↑b : ℤ)) (↑a : ℤ) ↔ SqLe b c a d

Tactic:
nonnegg_neg_pos

Premises used: Zsqrtd.nonnegg_neg_pos
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
c d a b : ℕ
⊢ Nonnegg d c (-(↑b : ℤ)) (↑a : ℤ) ↔ SqLe b c a d

Tactic:
exact nonnegg_neg_pos

Premises used: Zsqrtd.nonnegg_neg_pos
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
c d b : ℕ
a : ℤ
h : ∀ (x : ℕ), a = -(↑x : ℤ) → SqLe x d b c
⊢ Nonnegg c d a (↑b : ℤ)

Tactic:
cast nonnegg_comm (nonnegg_cases_right h)

Premises used: Zsqrtd.nonnegg_comm, cast, Zsqrtd.nonnegg_cases_right
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
n : ℤ√d
⊢ n.norm = n.re * n.re - d * n.im * n.im

Tactic:
rfl

Premises used: Zsqrtd.norm, rfl
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
⊢ norm (d := d) 0 = 0

Tactic:
simp [norm]

Premises used: Zsqrtd.norm
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
⊢ norm (d := d) 1 = 1

Tactic:
simp [norm]

Premises used: Zsqrtd.norm
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d n : ℤ
⊢ norm (d := d) (↑n : ℤ√d) = n * n

Tactic:
simp [norm]

Premises used: Zsqrtd.norm
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
n : ℕ
⊢ norm (d := d) (↑n : ℤ√d) = HMul.hMul (α := ℤ) (↑n : ℤ) (↑n : ℤ)

Tactic:
norm_intCast n

Premises used: Nat.cast, Zsqrtd.norm_intCast
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
n m : ℤ√d
⊢ (n.re * m.re + d * n.im * m.im) * (n.re * m.re + d * n.im * m.im) -
      d * (n.re * m.im + n.im * m.re) * (n.re * m.im + n.im * m.re) =
    (n.re * n.re - d * n.im * n.im) * (m.re * m.re - d * m.im * m.im)

Tactic:
ring
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
n : ℤ√d
re : Zsqrtd.re (d := d) (↑n.norm : ℤ√d) = (n * star n).re
im : Zsqrtd.im (d := d) (↑n.norm : ℤ√d) = (n * star n).im
⊢ (↑n.norm : ℤ√d) = n * star n

Tactic:
ext
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
n : ℤ√d
⊢ re (d := d) (↑n.norm : ℤ√d) = (n * star n).re

Tactic:
simp [norm, star, mul_comm, sub_eq_add_neg]

Premises used: sub_eq_add_neg, mul_comm, Zsqrtd.norm, Star.star
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
n : ℤ√d
⊢ im (d := d) (↑n.norm : ℤ√d) = (n * star n).im

Tactic:
simp [norm, star, mul_comm, sub_eq_add_neg]

Premises used: sub_eq_add_neg, mul_comm, Zsqrtd.norm, Star.star
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
x : ℤ√d
⊢ Eq (α := ℤ√d) (↑(-x).norm : ℤ√d) (↑x.norm : ℤ√d)

Tactic:
simp [norm_eq_mul_conj]

Premises used: Zsqrtd.norm_eq_mul_conj
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
x : ℤ√d
⊢ Eq (α := ℤ√d) (↑(star x).norm : ℤ√d) (↑x.norm : ℤ√d)

Tactic:
simp [norm_eq_mul_conj, mul_comm]

Premises used: Zsqrtd.norm_eq_mul_conj, mul_comm
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
hd : d ≤ 0
n : ℤ√d
rw : 0 ≤ -d * (n.im * n.im)
⊢ 0 ≤ -(d * n.im * n.im)

Tactic:
rw [mul_assoc, neg_mul_eq_neg_mul]

Premises used: mul_assoc, neg_mul_eq_neg_mul
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
hd : d ≤ 0
n : ℤ√d
⊢ 0 ≤ -d * (n.im * n.im)

Tactic:
mul_nonneg (neg_nonneg.2 hd) (mul_self_nonneg _)

Premises used: mul_self_nonneg, Iff.mpr, mul_nonneg, neg_nonneg
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
hd : d ≤ 0
n : ℤ√d
⊢ 0 ≤ -d * (n.im * n.im)

Tactic:
exact mul_nonneg (neg_nonneg.2 hd) (mul_self_nonneg _)

Premises used: mul_self_nonneg, Iff.mpr, mul_nonneg, neg_nonneg
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
hd : d ≤ 0
n : ℤ√d
⊢ |n.norm| = n.norm

Tactic:
abs_of_nonneg <| norm_nonneg hd n

Premises used: abs_of_nonneg, Zsqrtd.norm_nonneg
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
x : ℤ√d
h : x.norm.natAbs = 1
hx : 0 ≤ x.norm
rwa : ∀ (h : Eq (α := ℤ) (↑x.norm.natAbs : ℤ) (↑1 : ℤ)) (hx : 0 ≤ x.norm), 1 = x * star x
rwa₁ : ∀ (h : x.norm = (↑1 : ℤ)) (hx : 0 ≤ x.norm), 1 = x * star x
rwa₂ : ∀ (h : Eq (α := ℤ√d) (↑x.norm : ℤ√d) (↑(↑1 : ℤ) : ℤ√d)) (hx : 0 ≤ x.norm), 1 = x * star x
rwa₃ : ∀ (h : x * star x = (↑(↑1 : ℤ) : ℤ√d)) (hx : 0 ≤ x.norm), 1 = x * star x
rwa₄ rwa₅ rwa₆ rwa₇ : ∀ (h : (↑(↑1 : ℤ) : ℤ√d) = x * star x) (hx : 0 ≤ x.norm), 1 = x * star x
⊢ 1 = x * star x

Tactic:
rwa [← Int.natCast_inj, Int.natAbs_of_nonneg hx, ← @Int.cast_inj (ℤ√d) _ _,
              norm_eq_mul_conj, eq_comm] at h

Premises used: Int.cast_inj, eq_comm, Int.natAbs_of_nonneg, Zsqrtd.norm_eq_mul_conj, Int.natCast_inj
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
x : ℤ√d
h : x.norm.natAbs = 1
hx : x.norm ≤ 0
rwa : ∀ (h : Eq (α := ℤ) (↑x.norm.natAbs : ℤ) (↑1 : ℤ)) (hx : x.norm ≤ 0), 1 = x * -star x
rwa₁ : ∀ (h : -x.norm = (↑1 : ℤ)) (hx : x.norm ≤ 0), 1 = x * -star x
rwa₂ : ∀ (h : Eq (α := ℤ√d) (↑(-x.norm) : ℤ√d) (↑(↑1 : ℤ) : ℤ√d)) (hx : x.norm ≤ 0), 1 = x * -star x
rwa₃ : ∀ (h : Eq (α := ℤ√d) (-(↑x.norm : ℤ√d)) (↑(↑1 : ℤ) : ℤ√d)) (hx : x.norm ≤ 0), 1 = x * -star x
rwa₄ : ∀ (h : -(x * star x) = (↑(↑1 : ℤ) : ℤ√d)) (hx : x.norm ≤ 0), 1 = x * -star x
rwa₅ : ∀ (h : x * -star x = (↑(↑1 : ℤ) : ℤ√d)) (hx : x.norm ≤ 0), 1 = x * -star x
rwa₆ rwa₇ rwa₈ rwa₉ : ∀ (h : (↑(↑1 : ℤ) : ℤ√d) = x * -star x) (hx : x.norm ≤ 0), 1 = x * -star x
⊢ 1 = x * -star x

Tactic:
rwa [← Int.natCast_inj, Int.ofNat_natAbs_of_nonpos hx, ← @Int.cast_inj (ℤ√d) _ _,
              Int.cast_neg, norm_eq_mul_conj, neg_mul_eq_mul_neg, eq_comm] at h

Premises used: Int.cast_neg, Int.cast_inj, eq_comm, Zsqrtd.norm_eq_mul_conj, neg_mul_eq_mul_neg, Int.ofNat_natAbs_of_nonpos, Int.natCast_inj
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
x : ℤ√d
h : IsUnit x
let : ∀ (y : ℤ√d) (hy : 1 = x * y), x.norm.natAbs = 1
⊢ x.norm.natAbs = 1

Tactic:
let ⟨y, hy⟩ := isUnit_iff_dvd_one.1 h
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
x : ℤ√d
h : IsUnit x
y : ℤ√d
hy : 1 = x * y
⊢ Function.comp (α := ℤ√d) Int.natAbs norm 1 = (Int.natAbs ∘ norm) (x * y)

Tactic:
have := congr_arg (Int.natAbs ∘ norm) hy
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
x : ℤ√d
h : IsUnit x
y : ℤ√d
hy : 1 = x * y
this : Function.comp (α := ℤ√d) Int.natAbs norm 1 = (Int.natAbs ∘ norm) (x * y)
⊢ x.norm.natAbs = 1 ∧ y.norm.natAbs = 1

Tactic:
rw [Function.comp_apply, Function.comp_apply, norm_mul, Int.natAbs_mul, norm_one,
      Int.natAbs_one, eq_comm, mul_eq_one] at this

Premises used: Zsqrtd.norm_one, Int.natAbs_one, Int.natAbs_mul, Zsqrtd.norm_mul, eq_comm, mul_eq_one, Function.comp_apply
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
x : ℤ√d
h : IsUnit x
y : ℤ√d
hy : 1 = x * y
this : x.norm.natAbs = 1 ∧ y.norm.natAbs = 1
⊢ x.norm.natAbs = 1

Tactic:
this.1

Premises used: And.left
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
x : ℤ√d
h : IsUnit x
y : ℤ√d
hy : 1 = x * y
this : x.norm.natAbs = 1 ∧ y.norm.natAbs = 1
⊢ x.norm.natAbs = 1

Tactic:
exact this.1

Premises used: And.left
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
z : ℤ√d
rw : IsUnit z ↔ z.norm.natAbs = 1
rw₁ rw₂ : IsUnit z ↔ IsUnit z
⊢ IsUnit z ↔ IsUnit z.norm

Tactic:
rw [Int.isUnit_iff_natAbs_eq, norm_eq_one_iff]

Premises used: Zsqrtd.norm_eq_one_iff, Int.isUnit_iff_natAbs_eq
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
hd : d ≤ 0
z : ℤ√d
rw : z.norm = 1 ↔ z.norm.natAbs = 1
rw₁ : z.norm = 1 ↔ Eq (α := ℤ) (↑z.norm.natAbs : ℤ) (↑1 : ℤ)
rw₂ : z.norm = 1 ↔ z.norm = (↑1 : ℤ)
rw₃ rw₄ : z.norm = 1 ↔ z.norm = 1
⊢ z.norm = 1 ↔ IsUnit z

Tactic:
rw [← norm_eq_one_iff, ← Int.natCast_inj, Int.natAbs_of_nonneg (norm_nonneg hd z), Int.ofNat_one]

Premises used: Zsqrtd.norm_eq_one_iff, Int.natAbs_of_nonneg, Int.ofNat_one, Zsqrtd.norm_nonneg, Int.natCast_inj
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
hd : d < 0
z : ℤ√d
mp : z.norm = 0 → z = 0
mpr : z = 0 → z.norm = 0
⊢ z.norm = 0 ↔ z = 0

Tactic:
constructor
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
hd : d < 0
z : ℤ√d
h : z.norm = 0
⊢ z.re * z.re + -(d * (z.im * z.im)) = 0

Tactic:
rw [norm_def, sub_eq_add_neg, mul_assoc] at h

Premises used: Zsqrtd.norm_def, mul_assoc, sub_eq_add_neg
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
hd : d < 0
z : ℤ√d
h : z.re * z.re + -(d * (z.im * z.im)) = 0
⊢ 0 ≤ z.re * z.re

Tactic:
have left := mul_self_nonneg z.re
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
hd : d < 0
z : ℤ√d
h : z.re * z.re + -(d * (z.im * z.im)) = 0
left : 0 ≤ z.re * z.re
⊢ 0 ≤ -(d * (z.im * z.im))

Tactic:
have right := neg_nonneg.mpr (mul_nonpos_of_nonpos_of_nonneg hd.le (mul_self_nonneg z.im))
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
hd : d < 0
z : ℤ√d
h : z.re * z.re + -(d * (z.im * z.im)) = 0
left : 0 ≤ z.re * z.re
right : 0 ≤ -(d * (z.im * z.im))
⊢ z.re * z.re = 0

Tactic:
obtain ⟨ha, hb⟩ := (add_eq_zero_iff_of_nonneg left right).mp h

Premises used: add_eq_zero_iff_of_nonneg, Iff.mp
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
hd : d < 0
z : ℤ√d
h : z.re * z.re + -(d * (z.im * z.im)) = 0
left : 0 ≤ z.re * z.re
right : 0 ≤ -(d * (z.im * z.im))
ha : z.re * z.re = 0
⊢ -(d * (z.im * z.im)) = 0

Tactic:
obtain ⟨ha, hb⟩ := (add_eq_zero_iff_of_nonneg left right).mp h

Premises used: add_eq_zero_iff_of_nonneg, Iff.mp