awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact 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
-- 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_neg_pos.2 (sqLe_mul.right.left (nonnegg_neg_pos.1 ha) (nonnegg_pos_neg.1 hb))

Premises used: Iff.mpr, Zsqrtd.sqLe_mul, And.right, And.left, Zsqrtd.nonnegg_neg_pos, Iff.mp, Zsqrtd.nonnegg_pos_neg, Zsqrtd.Nonneg, Int.add
-- 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:
exact nonnegg_neg_pos.2 (sqLe_mul.right.left (nonnegg_neg_pos.1 ha) (nonnegg_pos_neg.1 hb))

Premises used: Iff.mpr, Zsqrtd.sqLe_mul, And.right, And.left, Zsqrtd.nonnegg_neg_pos, Iff.mp, Zsqrtd.nonnegg_pos_neg
-- 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_neg_pos.2 (sqLe_mul.right.right.left (nonnegg_pos_neg.1 ha) (nonnegg_neg_pos.1 hb))

Premises used: Iff.mpr, Zsqrtd.sqLe_mul, And.right, And.left, Zsqrtd.nonnegg_neg_pos, Iff.mp, Zsqrtd.nonnegg_pos_neg, Zsqrtd.Nonneg, Int.add
-- 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:
exact
        nonnegg_neg_pos.2 (sqLe_mul.right.right.left (nonnegg_pos_neg.1 ha) (nonnegg_neg_pos.1 hb))

Premises used: Iff.mpr, Zsqrtd.sqLe_mul, And.right, And.left, Zsqrtd.nonnegg_neg_pos, Iff.mp, Zsqrtd.nonnegg_pos_neg
-- 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.right.right.right (nonnegg_pos_neg.1 ha) (nonnegg_pos_neg.1 hb))

Premises used: Iff.mpr, Zsqrtd.sqLe_mul, And.right, Iff.mp, Zsqrtd.nonnegg_pos_neg, Zsqrtd.Nonneg, Int.add
-- 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:
exact
        nonnegg_pos_neg.2
          (sqLe_mul.right.right.right (nonnegg_pos_neg.1 ha) (nonnegg_pos_neg.1 hb))

Premises used: Iff.mpr, Zsqrtd.sqLe_mul, And.right, Iff.mp, Zsqrtd.nonnegg_pos_neg
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
a b : ℤ√(↑d : ℤ)
simp_rw : a.Nonneg → b.Nonneg → (a * b).Nonneg
⊢ 0 ≤ a → 0 ≤ b → 0 ≤ a * b

Tactic:
simp_rw [← nonneg_iff_zero_le]

Premises used: Zsqrtd.nonneg_iff_zero_le
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
a b : ℤ√(↑d : ℤ)
⊢ a.Nonneg → b.Nonneg → (a * b).Nonneg

Tactic:
nonneg_mul

Premises used: Zsqrtd.nonneg_mul
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
a b : ℤ√(↑d : ℤ)
⊢ a.Nonneg → b.Nonneg → (a * b).Nonneg

Tactic:
exact nonneg_mul

Premises used: Zsqrtd.nonneg_mul
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
c d y : ℕ
h : 0 < c
⊢ ¬SqLe (y + 1) c 0 d

Tactic:
not_le_of_gt <| mul_pos (mul_pos h <| Nat.succ_pos _) <| Nat.succ_pos _

Premises used: mul_pos, Nat.succ_pos, Zsqrtd.SqLe, not_le_of_gt
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
dnsq : Nonsquare d
⊢ 0 < d

Tactic:
lt_of_le_of_ne (Nat.zero_le _) <| Ne.symm <| Nonsquare.ns d 0

Premises used: Nat.zero_le, Zsqrtd.Nonsquare.ns, Ne.symm, OfNat.ofNat, lt_of_le_of_ne
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
h : x * x = d * y * y
g : ℕ := x.gcd y
gpos : g > 0
let : ∀ (m n : ℕ) (co : m.Coprime n) (hx : x = m * g) (hy : y = n * g), False
⊢ False

Tactic:
let ⟨m, n, co, (hx : x = m * g), (hy : y = n * g)⟩ := Nat.exists_coprime _ _
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
h : x * x = d * y * y
g : ℕ := x.gcd y
gpos : g > 0
m n : ℕ
co : m.Coprime n
hx : x = m * g
hy : y = n * g
rw : ∀ (n : ℕ) (h : m * g * (m * g) = d * (n * g) * (n * g)) (co : m.Coprime n) (hx : x = m * g) (hy : y = n * g), False
⊢ False

Tactic:
rw [hx, hy] at h
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
g : ℕ := x.gcd y
gpos : g > 0
m n : ℕ
h : m * g * (m * g) = d * (n * g) * (n * g)
co : m.Coprime n
hx : x = m * g
hy : y = n * g
⊢ m * m = d * (n * n)

Tactic:
mul_left_cancel₀ (mul_pos gpos gpos).ne' ?_

Premises used: mul_left_cancel₀, LT.lt.ne', mul_pos
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
g : ℕ := x.gcd y
gpos : g > 0
m n : ℕ
h : m * g * (m * g) = d * (n * g) * (n * g)
co : m.Coprime n
hx : x = m * g
hy : y = n * g
refine : g * g * (m * m) = g * g * (d * (n * n))
⊢ m * m = d * (n * n)

Tactic:
refine mul_left_cancel₀ (mul_pos gpos gpos).ne' ?_

Premises used: mul_left_cancel₀, LT.lt.ne', mul_pos
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
g : ℕ := x.gcd y
gpos : g > 0
m n : ℕ
h : m * g * (m * g) = d * (n * g) * (n * g)
co : m.Coprime n
hx : x = m * g
hy : y = n * g
⊢ g * g * (m * m) = g * g * (d * (n * n))

Tactic:
simpa [mul_comm, mul_left_comm, mul_assoc] using h

Premises used: mul_assoc, mul_left_comm, mul_comm
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
g : ℕ := x.gcd y
gpos : g > 0
m n : ℕ
h : m * g * (m * g) = d * (n * g) * (n * g)
co : m.Coprime n
hx : x = m * g
hy : y = n * g
⊢ m * m = d * (n * n)

Tactic:
have : m * m = d * (n * n) := by
        refine mul_left_cancel₀ (mul_pos gpos gpos).ne' ?_
        simpa [mul_comm, mul_left_comm, mul_assoc] using h
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
g : ℕ := x.gcd y
gpos : g > 0
m n : ℕ
h : m * g * (m * g) = d * (n * g) * (n * g)
co : m.Coprime n
hx : x = m * g
hy : y = n * g
this : m * m = d * (n * n)
⊢ (m * m).Coprime (n * n)

Tactic:
have co2 :=
        let co1 := co.mul_right co
        co1.mul_left co1
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
g : ℕ := x.gcd y
gpos : g > 0
m n : ℕ
h : m * g * (m * g) = d * (n * g) * (n * g)
co : m.Coprime n
hx : x = m * g
hy : y = n * g
this : m * m = d * (n * n)
co2 : (m * m).Coprime (n * n)
rw : d ∣ d * (n * n)
⊢ d ∣ m * m

Tactic:
rw [this]
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
g : ℕ := x.gcd y
gpos : g > 0
m n : ℕ
h : m * g * (m * g) = d * (n * g) * (n * g)
co : m.Coprime n
hx : x = m * g
hy : y = n * g
this : m * m = d * (n * n)
co2 : (m * m).Coprime (n * n)
⊢ d ∣ d * (n * n)

Tactic:
apply dvd_mul_right

Premises used: dvd_mul_right
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
g : ℕ := x.gcd y
gpos : g > 0
m n : ℕ
h : m * g * (m * g) = d * (n * g) * (n * g)
co : m.Coprime n
hx : x = m * g
hy : y = n * g
this : m * m = d * (n * n)
co2 : (m * m).Coprime (n * n)
⊢ m * m ∣ d * (n * n)

Tactic:
simp [this]
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
g : ℕ := x.gcd y
gpos : g > 0
m n : ℕ
h : m * g * (m * g) = d * (n * g) * (n * g)
co : m.Coprime n
hx : x = m * g
hy : y = n * g
this : m * m = d * (n * n)
co2 : (m * m).Coprime (n * n)
⊢ False

Tactic:
exact
        Nonsquare.ns d m
          (Nat.dvd_antisymm (by rw [this]; apply dvd_mul_right) <|
            co2.dvd_of_dvd_mul_right <| by simp [this])

Premises used: Zsqrtd.Nonsquare.ns, Nat.Coprime.dvd_of_dvd_mul_right, Nat.dvd_antisymm
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
dnsq : Nonsquare d
x y : ℤ
h : x * x = (↑d : ℤ) * y * y
⊢ Eq (α := ℤ) (↑(x.natAbs * x.natAbs) : ℤ) (↑(d * y.natAbs * y.natAbs) : ℤ)

Tactic:
rw [mul_assoc, ← Int.natAbs_mul_self, ← Int.natAbs_mul_self, ← Int.natCast_mul, ← mul_assoc] at h

Premises used: Int.natAbs_mul_self, mul_assoc, Int.natCast_mul
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
dnsq : Nonsquare d
x y : ℤ
h : Eq (α := ℤ) (↑(x.natAbs * x.natAbs) : ℤ) (↑(d * y.natAbs * y.natAbs) : ℤ)
⊢ x = 0 ∧ y = 0

Tactic:
let ⟨h1, h2⟩ := divides_sq_eq_zero (Int.ofNat.inj h)
    ⟨Int.natAbs_eq_zero.mp h1, Int.natAbs_eq_zero.mp h2⟩

Premises used: Zsqrtd.divides_sq_eq_zero, Int.ofNat.inj, _private.0.Zsqrtd.divides_sq_eq_zero_z.match_1, Int.natAbs_eq_zero, And, And.intro, Iff.mp, OfNat.ofNat, Eq
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
dnsq : Nonsquare d
x y : ℤ
h : Eq (α := ℤ) (↑(x.natAbs * x.natAbs) : ℤ) (↑(d * y.natAbs * y.natAbs) : ℤ)
⊢ x = 0 ∧ y = 0

Tactic:
exact
    let ⟨h1, h2⟩ := divides_sq_eq_zero (Int.ofNat.inj h)
    ⟨Int.natAbs_eq_zero.mp h1, Int.natAbs_eq_zero.mp h2⟩
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
e : (x + 1) * (x + 1) = d * (y + 1) * (y + 1)
⊢ x + 1 = 0

Tactic:
have t := (divides_sq_eq_zero e).left
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
e : (x + 1) * (x + 1) = d * (y + 1) * (y + 1)
t : x + 1 = 0
⊢ False

Tactic:
contradiction
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
dnsq : Nonsquare d
a : ℕ
xy : Nonneg (d := d) { re := -[a+1], im := 0 }
h : Nonneg (d := d) (-{ re := -[a+1], im := 0 })
⊢ LT.lt (α := ℕ) 0 1

Tactic:
decide
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
dnsq : Nonsquare d
n : ℕ
h : Nonneg (d := d) { re := (↑(n + 1) : ℤ), im := 0 }
yx : Nonneg (d := d) (-{ re := (↑(n + 1) : ℤ), im := 0 })
⊢ LT.lt (α := ℕ) 0 1

Tactic:
decide
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
xy : SqLe (y + 1) d (x + 1) 1
yx : SqLe (x + 1) 1 y.succ d
t : 1 * (x + 1) * (x + 1) = d * y.succ * y.succ := ⋯
⊢ (x + 1) * (x + 1) = d * y.succ * y.succ

Tactic:
rw [one_mul] at t

Premises used: one_mul
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
xy : SqLe (y + 1) d (x + 1) 1
yx : SqLe (x + 1) 1 y.succ d
t : (x + 1) * (x + 1) = d * y.succ * y.succ
⊢ Eq (α := ℤ√(↑d : ℤ)) { re := (↑(x + 1) : ℤ), im := -[y+1] } 0

Tactic:
absurd t (not_divides_sq _ _)

Premises used: absurd, Zsqrtd.not_divides_sq
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
xy : SqLe (y + 1) d (x + 1) 1
yx : SqLe (x + 1) 1 y.succ d
t : (x + 1) * (x + 1) = d * y.succ * y.succ
⊢ Eq (α := ℤ√(↑d : ℤ)) { re := (↑(x + 1) : ℤ), im := -[y+1] } 0

Tactic:
exact absurd t (not_divides_sq _ _)

Premises used: absurd, Zsqrtd.not_divides_sq
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
xy : SqLe (x + 1) 1 (y + 1) d
yx : SqLe (y + 1) d x.succ 1
t : 1 * (x + 1) * (x + 1) = d * (y + 1) * (y + 1) := ⋯
⊢ (x + 1) * (x + 1) = d * (y + 1) * (y + 1)

Tactic:
rw [one_mul] at t

Premises used: one_mul
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
xy : SqLe (x + 1) 1 (y + 1) d
yx : SqLe (y + 1) d x.succ 1
t : (x + 1) * (x + 1) = d * (y + 1) * (y + 1)
⊢ Eq (α := ℤ√(↑d : ℤ)) { re := -[x+1], im := (↑(y + 1) : ℤ) } 0

Tactic:
absurd t (not_divides_sq _ _)

Premises used: absurd, Zsqrtd.not_divides_sq
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
xy : SqLe (x + 1) 1 (y + 1) d
yx : SqLe (y + 1) d x.succ 1
t : (x + 1) * (x + 1) = d * (y + 1) * (y + 1)
⊢ Eq (α := ℤ√(↑d : ℤ)) { re := -[x+1], im := (↑(y + 1) : ℤ) } 0

Tactic:
exact absurd t (not_divides_sq _ _)

Premises used: absurd, Zsqrtd.not_divides_sq
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
dnsq : Nonsquare d
a b : ℤ√(↑d : ℤ)
ab : a ≤ b
ba : b ≤ a
rwa rwa₁ rwa₂ rwa₃ : (b - a).Nonneg
⊢ (-(a - b)).Nonneg

Tactic:
rwa [neg_sub]

Premises used: neg_sub
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
dnsq : Nonsquare d
x x_1 : ℤ√(↑d : ℤ)
ab : x ≤ x_1
ba : x_1 ≤ x
rwa rwa₁ rwa₂ rwa₃ : (x_1 - x).Nonneg
⊢ (-(x - x_1)).Nonneg

Tactic:
rwa [neg_sub]

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

Tactic:
have t := (b - a).nonneg_total
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
dnsq : Nonsquare 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 : ℕ
dnsq : Nonsquare d
x y z w : ℤ
h : HMul.hMul (α := ℤ√(↑d : ℤ)) { re := x, im := y : ℤ√(↑d : ℤ) } { re := z, im := w : ℤ√(↑d : ℤ) } = 0
⊢ 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 : ℤ) } =
    0

Tactic:
injection h with h1 h2
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
dnsq : Nonsquare d
x y z w : ℤ
h : HMul.hMul (α := ℤ√(↑d : ℤ)) { re := x, im := y : ℤ√(↑d : ℤ) } { re := z, im := w : ℤ√(↑d : ℤ) } = 0
h1 :
  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 : ℤ) } =
    0
⊢ 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 : ℤ) } =
    0

Tactic:
injection h with h1 h2
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
dnsq : Nonsquare d
x y z w : ℤ
h1 :
  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 : ℤ) } =
    0
h2 :
  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 : ℤ) } =
    0
⊢ x * z = -((↑d : ℤ) * y * w)

Tactic:
have h1 : x * z = -(d * y * w) := eq_neg_of_add_eq_zero_left h1
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
dnsq : Nonsquare d
x y z w : ℤ
h1_1 :
  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 : ℤ) } =
    0
h2 :
  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 : ℤ) } =
    0
h1 : x * z = -((↑d : ℤ) * y * w)
⊢ x * w = -(y * z)

Tactic:
have h2 : x * w = -(y * z) := eq_neg_of_add_eq_zero_left h2
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
dnsq : Nonsquare d
x y z w : ℤ
h1_1 :
  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 : ℤ) } =
    0
h2_1 :
  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 : ℤ) } =
    0
h1 : x * z = -((↑d : ℤ) * y * w)
h2 : x * w = -(y * z)
⊢ x * x = (↑d : ℤ) * y * y → Eq (α := ℤ√(↑d : ℤ)) { re := x, im := y } 0

Tactic:
have fin : x * x = d * y * y → (⟨x, y⟩ : ℤ√d) = 0 := fun e =>
      match x, y, divides_sq_eq_zero_z e with
      | _, _, ⟨rfl, rfl⟩ => rfl