awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y : ℤ
re : Zsqrtd.re (d := d) { re := x, im := y : ℤ√d } = ((↑x : ℤ√d) + HMul.hMul (α := ℤ√d) sqrtd (↑y : ℤ√d)).re
im : Zsqrtd.im (d := d) { re := x, im := y : ℤ√d } = ((↑x : ℤ√d) + HMul.hMul (α := ℤ√d) sqrtd (↑y : ℤ√d)).im
⊢ { re := x, im := y } = (↑x : ℤ√d) + HMul.hMul (α := ℤ√d) sqrtd (↑y : ℤ√d)

Tactic:
ext
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y : ℤ
⊢ re (d := d) { re := x, im := y : ℤ√d } = ((↑x : ℤ√d) + HMul.hMul (α := ℤ√d) sqrtd (↑y : ℤ√d)).re

Tactic:
simp
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y : ℤ
⊢ im (d := d) { re := x, im := y : ℤ√d } = ((↑x : ℤ√d) + HMul.hMul (α := ℤ√d) sqrtd (↑y : ℤ√d)).im

Tactic:
simp
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y : ℤ
re :
  (HMul.hMul (α := ℤ√d) { re := x, im := y : ℤ√d } (star { re := x, im := y : ℤ√d })).re =
    (HMul.hMul (α := ℤ√d) (↑x : ℤ√d) (↑x : ℤ√d) - HMul.hMul (α := ℤ√d) (↑d : ℤ√d) (↑y : ℤ√d) * (↑y : ℤ√d)).re
im :
  (HMul.hMul (α := ℤ√d) { re := x, im := y : ℤ√d } (star { re := x, im := y : ℤ√d })).im =
    (HMul.hMul (α := ℤ√d) (↑x : ℤ√d) (↑x : ℤ√d) - HMul.hMul (α := ℤ√d) (↑d : ℤ√d) (↑y : ℤ√d) * (↑y : ℤ√d)).im
⊢ HMul.hMul (α := ℤ√d) { re := x, im := y : ℤ√d } (star { re := x, im := y : ℤ√d }) =
    HMul.hMul (α := ℤ√d) (↑x : ℤ√d) (↑x : ℤ√d) - HMul.hMul (α := ℤ√d) (↑d : ℤ√d) (↑y : ℤ√d) * (↑y : ℤ√d)

Tactic:
ext
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y : ℤ
⊢ (HMul.hMul (α := ℤ√d) { re := x, im := y : ℤ√d } (star { re := x, im := y : ℤ√d })).re =
    (HMul.hMul (α := ℤ√d) (↑x : ℤ√d) (↑x : ℤ√d) - HMul.hMul (α := ℤ√d) (↑d : ℤ√d) (↑y : ℤ√d) * (↑y : ℤ√d)).re

Tactic:
simp [sub_eq_add_neg, mul_comm]

Premises used: sub_eq_add_neg, mul_comm
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y : ℤ
⊢ (HMul.hMul (α := ℤ√d) { re := x, im := y : ℤ√d } (star { re := x, im := y : ℤ√d })).im =
    (HMul.hMul (α := ℤ√d) (↑x : ℤ√d) (↑x : ℤ√d) - HMul.hMul (α := ℤ√d) (↑d : ℤ√d) (↑y : ℤ√d) * (↑y : ℤ√d)).im

Tactic:
simp [sub_eq_add_neg, mul_comm]

Premises used: sub_eq_add_neg, mul_comm
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d z : ℤ
a : ℤ√d
mp : (↑z : ℤ√d) ∣ a → z ∣ a.re ∧ z ∣ a.im
mpr : z ∣ a.re ∧ z ∣ a.im → (↑z : ℤ√d) ∣ a
⊢ (↑z : ℤ√d) ∣ a ↔ z ∣ a.re ∧ z ∣ a.im

Tactic:
constructor
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d z : ℤ
x : ℤ√d
⊢ z ∣ ((↑z : ℤ√d) * x).re ∧ z ∣ ((↑z : ℤ√d) * x).im

Tactic:
simp
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d z : ℤ
a : ℤ√d
r : ℤ
hr : a.re = z * r
i : ℤ
hi : a.im = z * i
h : a = HMul.hMul (α := ℤ√d) (↑z : ℤ√d) { re := r, im := i }
⊢ (↑z : ℤ√d) ∣ a

Tactic:
use ⟨r, i⟩
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d z : ℤ
a : ℤ√d
r : ℤ
hr : a.re = z * r
i : ℤ
hi : a.im = z * i
h : a.re = re (d := d) { re := z * r, im := z * i } ∧ a.im = im (d := d) { re := z * r, im := z * i }
⊢ a = HMul.hMul (α := ℤ√d) (↑z : ℤ√d) { re := r, im := i }

Tactic:
rw [smul_val, Zsqrtd.ext_iff]

Premises used: Zsqrtd.smul_val, Zsqrtd.ext_iff
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d z : ℤ
a : ℤ√d
r : ℤ
hr : a.re = z * r
i : ℤ
hi : a.im = z * i
⊢ a.re = re (d := d) { re := z * r, im := z * i } ∧ a.im = im (d := d) { re := z * r, im := z * i }

Tactic:
⟨hr, hi⟩

Premises used: And.intro
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d z : ℤ
a : ℤ√d
r : ℤ
hr : a.re = z * r
i : ℤ
hi : a.im = z * i
⊢ a.re = re (d := d) { re := z * r, im := z * i } ∧ a.im = im (d := d) { re := z * r, im := z * i }

Tactic:
exact ⟨hr, hi⟩
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d a b : ℤ
rw : a ∣ re (d := d) (↑b : ℤ√d) ∧ a ∣ im (d := d) (↑b : ℤ√d) ↔ a ∣ b
⊢ Dvd.dvd (α := ℤ√d) (↑a : ℤ√d) (↑b : ℤ√d) ↔ a ∣ b

Tactic:
rw [intCast_dvd]

Premises used: Zsqrtd.intCast_dvd
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d a b : ℤ
⊢ a ∣ re (d := d) (↑b : ℤ√d) ∧ a ∣ im (d := d) (↑b : ℤ√d) ↔ a ∣ b

Tactic:
simp
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d a : ℤ
b c : ℤ√d
ha : a ≠ 0
h : (↑a : ℤ√d) * b = (↑a : ℤ√d) * c
rw :
  ∀ (h : ((↑a : ℤ√d) * b).re = ((↑a : ℤ√d) * c).re ∧ ((↑a : ℤ√d) * b).im = ((↑a : ℤ√d) * c).im),
    b.re = c.re ∧ b.im = c.im
⊢ b = c

Tactic:
rw [Zsqrtd.ext_iff] at h ⊢

Premises used: Zsqrtd.ext_iff
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d a : ℤ
b c : ℤ√d
ha : a ≠ 0
h : ((↑a : ℤ√d) * b).re = ((↑a : ℤ√d) * c).re ∧ ((↑a : ℤ√d) * b).im = ((↑a : ℤ√d) * c).im
apply : ((↑a : ℤ√d) * b).re = ((↑a : ℤ√d) * c).re → b.re = c.re
apply₁ : ((↑a : ℤ√d) * b).im = ((↑a : ℤ√d) * c).im → b.im = c.im
⊢ b.re = c.re ∧ b.im = c.im

Tactic:
apply And.imp _ _ h

Premises used: And.imp
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d a : ℤ
b c : ℤ√d
ha : a ≠ 0
h : ((↑a : ℤ√d) * b).re = ((↑a : ℤ√d) * c).re ∧ ((↑a : ℤ√d) * b).im = ((↑a : ℤ√d) * c).im
⊢ ((↑a : ℤ√d) * b).re = ((↑a : ℤ√d) * c).re → b.re = c.re

Tactic:
simpa only [re_smul, im_smul] using mul_left_cancel₀ ha

Premises used: Zsqrtd.im_smul, Zsqrtd.re_smul, mul_left_cancel₀
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d a : ℤ
b c : ℤ√d
ha : a ≠ 0
h : ((↑a : ℤ√d) * b).re = ((↑a : ℤ√d) * c).re ∧ ((↑a : ℤ√d) * b).im = ((↑a : ℤ√d) * c).im
⊢ ((↑a : ℤ√d) * b).im = ((↑a : ℤ√d) * c).im → b.im = c.im

Tactic:
simpa only [re_smul, im_smul] using mul_left_cancel₀ ha

Premises used: Zsqrtd.im_smul, Zsqrtd.re_smul, mul_left_cancel₀
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a : ℤ√d
⊢ a.re.gcd a.im = 0 ↔ a = 0

Tactic:
simp only [Int.gcd_eq_zero_iff, Zsqrtd.ext_iff, im_zero, re_zero]

Premises used: Zsqrtd.re_zero, Int.gcd_eq_zero_iff, Zsqrtd.im_zero, Zsqrtd.ext_iff
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a : ℤ√d
⊢ 0 < a.re.gcd a.im ↔ a ≠ 0

Tactic:
pos_iff_ne_zero.trans <| not_congr a.gcd_eq_zero_iff

Premises used: Iff.trans, Zsqrtd.gcd_eq_zero_iff, pos_iff_ne_zero, not_congr
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
nonzero : ¬(b.re = 0 ∧ b.im = 0)
H : ∀ z ∈ nonunits ℤ, z ≠ 0 → z ∣ b.re → ¬z ∣ b.im
⊢ IsCoprime b.re b.im

Tactic:
apply isCoprime_of_dvd

Premises used: isCoprime_of_dvd
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
hre : b.re = 0
him : b.im = 0
⊢ b = 0

Tactic:
Zsqrtd.ext hre him

Premises used: Zsqrtd.ext
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
hre : b.re = 0
him : b.im = 0
⊢ 0 ∣ a

Tactic:
obtain rfl : b = 0 := Zsqrtd.ext hre him

Premises used: Zsqrtd.ext, rfl
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
hre : b.re = 0
him : b.im = 0
hdvd₁ : 0 ∣ a
⊢ re (d := d) 0 = 0

Tactic:
obtain rfl : b = 0 := Zsqrtd.ext hre him

Premises used: Zsqrtd.ext, rfl
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
hre : b.re = 0
him : b.im = 0
hdvd₁ : 0 ∣ a
hre₁ : re (d := d) 0 = 0
⊢ im (d := d) 0 = 0

Tactic:
obtain rfl : b = 0 := Zsqrtd.ext hre him

Premises used: Zsqrtd.ext, rfl
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : 0 ∣ a
hre : re (d := d) 0 = 0
him : im (d := d) 0 = 0
⊢ a = 0

Tactic:
rw [zero_dvd_iff] at hdvd

Premises used: zero_dvd_iff
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : 0 ∣ a
hre : re (d := d) 0 = 0
him : im (d := d) 0 = 0
hdvd₁ : a = 0
⊢ re (d := d) 0 = 0

Tactic:
rw [zero_dvd_iff] at hdvd

Premises used: zero_dvd_iff
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : 0 ∣ a
hre : re (d := d) 0 = 0
him : im (d := d) 0 = 0
hdvd₁ : a = 0
hre₁ : re (d := d) 0 = 0
⊢ im (d := d) 0 = 0

Tactic:
rw [zero_dvd_iff] at hdvd

Premises used: zero_dvd_iff
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : a = 0
hre : re (d := d) 0 = 0
him : im (d := d) 0 = 0
⊢ False

Tactic:
simp [hdvd, im_zero, re_zero, not_isCoprime_zero_zero] at hcoprime

Premises used: Zsqrtd.re_zero, not_isCoprime_zero_zero, Zsqrtd.im_zero
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
z : ℤ
hz : z ∈ nonunits ℤ
hzdvdu : z ∣ b.re
hzdvdv : z ∣ b.im
H : IsUnit z
⊢ False

Tactic:
apply hz
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
z : ℤ
hz : z ∈ nonunits ℤ
hzdvdu : z ∣ b.re
hzdvdv : z ∣ b.im
rw : (↑z : ℤ√d) ∣ a
⊢ z ∣ a.re ∧ z ∣ a.im

Tactic:
rw [← intCast_dvd]

Premises used: Zsqrtd.intCast_dvd
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
z : ℤ
hz : z ∈ nonunits ℤ
hzdvdu : z ∣ b.re
hzdvdv : z ∣ b.im
apply : (↑z : ℤ√d) ∣ b
⊢ (↑z : ℤ√d) ∣ a

Tactic:
apply dvd_trans _ hdvd

Premises used: dvd_trans
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
z : ℤ
hz : z ∈ nonunits ℤ
hzdvdu : z ∣ b.re
hzdvdv : z ∣ b.im
rw : z ∣ b.re ∧ z ∣ b.im
⊢ (↑z : ℤ√d) ∣ b

Tactic:
rw [intCast_dvd]

Premises used: Zsqrtd.intCast_dvd
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
z : ℤ
hz : z ∈ nonunits ℤ
hzdvdu : z ∣ b.re
hzdvdv : z ∣ b.im
⊢ z ∣ b.re ∧ z ∣ b.im

Tactic:
⟨hzdvdu, hzdvdv⟩

Premises used: And.intro
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
z : ℤ
hz : z ∈ nonunits ℤ
hzdvdu : z ∣ b.re
hzdvdv : z ∣ b.im
⊢ z ∣ b.re ∧ z ∣ b.im

Tactic:
exact ⟨hzdvdu, hzdvdv⟩
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
z : ℤ
hz : z ∈ nonunits ℤ
hzdvdu : z ∣ b.re
hzdvdv : z ∣ b.im
⊢ z ∣ a.re

Tactic:
obtain ⟨ha, hb⟩ : z ∣ a.re ∧ z ∣ a.im := by
      rw [← intCast_dvd]
      apply dvd_trans _ hdvd
      rw [intCast_dvd]
      exact ⟨hzdvdu, hzdvdv⟩

Premises used: Zsqrtd.re, Zsqrtd.im
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
z : ℤ
hz : z ∈ nonunits ℤ
hzdvdu : z ∣ b.re
hzdvdv : z ∣ b.im
ha : z ∣ a.re
⊢ z ∣ a.im

Tactic:
obtain ⟨ha, hb⟩ : z ∣ a.re ∧ z ∣ a.im := by
      rw [← intCast_dvd]
      apply dvd_trans _ hdvd
      rw [intCast_dvd]
      exact ⟨hzdvdu, hzdvdv⟩

Premises used: Zsqrtd.re, Zsqrtd.im
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
z : ℤ
hz : z ∈ nonunits ℤ
hzdvdu : z ∣ b.re
hzdvdv : z ∣ b.im
ha : z ∣ a.re
hb : z ∣ a.im
⊢ IsUnit z

Tactic:
hcoprime.isUnit_of_dvd' ha hb

Premises used: IsCoprime.isUnit_of_dvd'
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
z : ℤ
hz : z ∈ nonunits ℤ
hzdvdu : z ∣ b.re
hzdvdv : z ∣ b.im
ha : z ∣ a.re
hb : z ∣ a.im
⊢ IsUnit z

Tactic:
exact hcoprime.isUnit_of_dvd' ha hb

Premises used: IsCoprime.isUnit_of_dvd'
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a : ℤ√d
hgcd : 0 < a.re.gcd a.im
obtain :
  ∀ (re im : ℤ) (H1 : re.gcd im = 1) (Hre : a.re = re * (↑(a.re.gcd a.im) : ℤ))
    (Him : a.im = im * (↑(a.re.gcd a.im) : ℤ)),
    ∃ (b : ℤ√d), a = (↑(↑(a.re.gcd a.im) : ℤ) : ℤ√d) * b ∧ IsCoprime b.re b.im
⊢ ∃ (b : ℤ√d), a = (↑(↑(a.re.gcd a.im) : ℤ) : ℤ√d) * b ∧ IsCoprime b.re b.im

Tactic:
obtain ⟨re, im, H1, Hre, Him⟩ := Int.exists_gcd_one hgcd

Premises used: Zsqrtd.re, Int.exists_gcd_one, Zsqrtd.im
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a : ℤ√d
hgcd : 0 < a.re.gcd a.im
re im : ℤ
H1 : re.gcd im = 1
Hre : a.re = re * (↑(a.re.gcd a.im) : ℤ)
Him : a.im = im * (↑(a.re.gcd a.im) : ℤ)
⊢ a.re = (↑(a.re.gcd a.im) : ℤ) * re

Tactic:
rw [mul_comm] at Hre Him

Premises used: mul_comm
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a : ℤ√d
hgcd : 0 < a.re.gcd a.im
re im : ℤ
H1 : re.gcd im = 1
Hre : a.re = re * (↑(a.re.gcd a.im) : ℤ)
Him : a.im = im * (↑(a.re.gcd a.im) : ℤ)
Hre₁ : a.re = (↑(a.re.gcd a.im) : ℤ) * re
⊢ a.im = (↑(a.re.gcd a.im) : ℤ) * im

Tactic:
rw [mul_comm] at Hre Him

Premises used: mul_comm
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a : ℤ√d
hgcd : 0 < a.re.gcd a.im
re im : ℤ
H1 : re.gcd im = 1
Hre : a.re = (↑(a.re.gcd a.im) : ℤ) * re
Him : a.im = (↑(a.re.gcd a.im) : ℤ) * im
⊢ ∃ (b : ℤ√d), a = (↑(↑(a.re.gcd a.im) : ℤ) : ℤ√d) * b ∧ IsCoprime b.re b.im

Tactic:
⟨⟨re, im⟩, ?_, ?_⟩

Premises used: And.intro, Zsqrtd.mk, Exists.intro
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a : ℤ√d
hgcd : 0 < a.re.gcd a.im
re im : ℤ
H1 : re.gcd im = 1
Hre : a.re = (↑(a.re.gcd a.im) : ℤ) * re
Him : a.im = (↑(a.re.gcd a.im) : ℤ) * im
refine_1 : a = HMul.hMul (α := ℤ√d) (↑(↑(a.re.gcd a.im) : ℤ) : ℤ√d) { re := re, im := im }
refine_2 : IsCoprime (Zsqrtd.re (d := d) { re := re, im := im : ℤ√d }) (Zsqrtd.im (d := d) { re := re, im := im })
⊢ ∃ (b : ℤ√d), a = (↑(↑(a.re.gcd a.im) : ℤ) : ℤ√d) * b ∧ IsCoprime b.re b.im

Tactic:
refine ⟨⟨re, im⟩, ?_, ?_⟩
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a : ℤ√d
hgcd : 0 < a.re.gcd a.im
re im : ℤ
H1 : re.gcd im = 1
Hre : a.re = (↑(a.re.gcd a.im) : ℤ) * re
Him : a.im = (↑(a.re.gcd a.im) : ℤ) * im
refine_1 : a = { re := (↑(a.re.gcd a.im) : ℤ) * re, im := (↑(a.re.gcd a.im) : ℤ) * im }
refine_1₁ : a = { re := a.re, im := (↑(a.re.gcd a.im) : ℤ) * im }
refine_1₂ refine_1₃ : a = { re := a.re, im := a.im }
⊢ a = HMul.hMul (α := ℤ√d) (↑(↑(a.re.gcd a.im) : ℤ) : ℤ√d) { re := re, im := im }

Tactic:
rw [smul_val, ← Hre, ← Him]

Premises used: Zsqrtd.smul_val
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a : ℤ√d
hgcd : 0 < a.re.gcd a.im
re im : ℤ
H1 : re.gcd im = 1
Hre : a.re = (↑(a.re.gcd a.im) : ℤ) * re
Him : a.im = (↑(a.re.gcd a.im) : ℤ) * im
refine_2 : (Zsqrtd.re (d := d) { re := re, im := im : ℤ√d }).gcd (Zsqrtd.im (d := d) { re := re, im := im : ℤ√d }) = 1
refine_2₁ refine_2₂ : Eq (α := ℕ) 1 1
⊢ IsCoprime (Zsqrtd.re (d := d) { re := re, im := im : ℤ√d }) (Zsqrtd.im (d := d) { re := re, im := im })

Tactic:
rw [Int.isCoprime_iff_gcd_eq_one, H1]

Premises used: Int.isCoprime_iff_gcd_eq_one
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
c d x y z w : ℕ
xz : z ≤ x
yw : y ≤ w
xy : SqLe x c y d
⊢ c * z * z ≤ c * x * x

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
c d x y z w : ℕ
xz : z ≤ x
yw : y ≤ w
xy : SqLe x c y d
⊢ d * y * y ≤ d * w * w

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
c d x y z w : ℕ
xy : SqLe x c y d
zw : SqLe z c w d
⊢ c * (x * z) * (c * (x * z)) ≤ d * (y * w) * (d * (y * w))

Tactic:
simpa [mul_comm, mul_left_comm] using Nat.mul_le_mul xy zw

Premises used: mul_left_comm, Nat.mul_le_mul, mul_comm
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
c d x y z w : ℕ
xy : SqLe x c y d
zw : SqLe z c w d
⊢ c * (x * z) ≤ d * (y * w)

Tactic:
have xz := sqLe_add_mixed xy zw
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
c d x y z w : ℕ
xy : SqLe x c y d
zw : SqLe z c w d
xz : c * (x * z) ≤ d * (y * w)
⊢ c * (x * x) ≤ d * (y * y)

Tactic:
simp only [SqLe, mul_assoc] at xy zw

Premises used: mul_assoc, Zsqrtd.SqLe
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
c d x y z w : ℕ
xy : SqLe x c y d
zw : SqLe z c w d
xz : c * (x * z) ≤ d * (y * w)
xy₁ : c * (x * x) ≤ d * (y * y)
⊢ c * (z * z) ≤ d * (w * w)

Tactic:
simp only [SqLe, mul_assoc] at xy zw

Premises used: mul_assoc, Zsqrtd.SqLe
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
c d x y z w : ℕ
xz : c * (x * z) ≤ d * (y * w)
xy : c * (x * x) ≤ d * (y * y)
zw : c * (z * z) ≤ d * (w * w)
⊢ SqLe (x + z) c (y + w) d

Tactic:
simp [SqLe, mul_add, mul_comm, mul_left_comm, add_le_add, *]

Premises used: add_le_add, mul_left_comm, mul_comm, Zsqrtd.SqLe, mul_add
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
c d x y z w : ℕ
zw : SqLe y d x c
h : SqLe (x + z) c (y + w) d
h₁ : ¬d * w * w < c * z * z
⊢ SqLe z c w d

Tactic:
apply le_of_not_gt

Premises used: le_of_not_gt
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
c d x y z w : ℕ
zw : SqLe y d x c
h : SqLe (x + z) c (y + w) d
l : d * w * w < c * z * z
⊢ False

Tactic:
not_le_of_gt ?_ h

Premises used: not_le_of_gt
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
c d x y z w : ℕ
zw : SqLe y d x c
h : SqLe (x + z) c (y + w) d
l : d * w * w < c * z * z
h₁ : d * (y + w) * (y + w) < c * (x + z) * (x + z)
⊢ False

Tactic:
refine not_le_of_gt ?_ h

Premises used: not_le_of_gt
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
c d x y z w : ℕ
zw : SqLe y d x c
h : SqLe (x + z) c (y + w) d
l : d * w * w < c * z * z
h₁ :
  d * (y * y) + (d * (y * w) + (d * (y * w) + d * (w * w))) < c * (x * x) + (c * (x * z) + (c * (x * z) + c * (z * z)))
⊢ d * (y + w) * (y + w) < c * (x + z) * (x + z)

Tactic:
simp only [mul_add, mul_comm, mul_left_comm, add_assoc]

Premises used: add_assoc, mul_left_comm, mul_comm, mul_add
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
c d x y z w : ℕ
zw : SqLe y d x c
h : SqLe (x + z) c (y + w) d
l : d * w * w < c * z * z
⊢ d * (y * w) ≤ c * (x * z)

Tactic:
have hm := sqLe_add_mixed zw (le_of_lt l)
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
c d x y z w : ℕ
zw : SqLe y d x c
h : SqLe (x + z) c (y + w) d
l : d * w * w < c * z * z
hm : d * (y * w) ≤ c * (x * z)
⊢ d * (w * w) < c * (z * z)

Tactic:
simp only [SqLe, mul_assoc] at l zw

Premises used: mul_assoc, Zsqrtd.SqLe
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
c d x y z w : ℕ
zw : SqLe y d x c
h : SqLe (x + z) c (y + w) d
l : d * w * w < c * z * z
hm : d * (y * w) ≤ c * (x * z)
l₁ : d * (w * w) < c * (z * z)
⊢ d * (y * y) ≤ c * (x * x)

Tactic:
simp only [SqLe, mul_assoc] at l zw

Premises used: mul_assoc, Zsqrtd.SqLe
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
c d x y z w : ℕ
h : SqLe (x + z) c (y + w) d
hm : d * (y * w) ≤ c * (x * z)
l : d * (w * w) < c * (z * z)
zw : d * (y * y) ≤ c * (x * x)
h₁ :
  c * (x * x) + (c * (x * z) + (c * (x * z) + d * (w * w))) < c * (x * x) + (c * (x * z) + (c * (x * z) + c * (z * z)))
⊢ d * (y * y) + (d * (y * w) + (d * (y * w) + d * (w * w))) < c * (x * x) + (c * (x * z) + (c * (x * z) + c * (z * z)))

Tactic:
grw [zw, hm]
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
c d x y z w : ℕ
h : SqLe (x + z) c (y + w) d
hm : d * (y * w) ≤ c * (x * z)
l : d * (w * w) < c * (z * z)
zw : d * (y * y) ≤ c * (x * x)
⊢ c * (x * x) + (c * (x * z) + (c * (x * z) + d * (w * w))) < c * (x * x) + (c * (x * z) + (c * (x * z) + c * (z * z)))

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
c d x y n : ℕ
xy : SqLe x c y d
⊢ SqLe (n * x) c (n * y) d

Tactic:
simpa [SqLe, mul_left_comm, mul_assoc] using Nat.mul_le_mul_left (n * n) xy

Premises used: HMul.hMul, mul_assoc, Nat.mul_le_mul_left, mul_left_comm, Zsqrtd.SqLe
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y z w : ℕ
⊢ (SqLe x 1 y d → SqLe z 1 w d → SqLe (x * w + y * z) d (x * z + d * y * w) 1) ∧
    (SqLe x 1 y d → SqLe w d z 1 → SqLe (x * z + d * y * w) 1 (x * w + y * z) d) ∧
      (SqLe y d x 1 → SqLe z 1 w d → SqLe (x * z + d * y * w) 1 (x * w + y * z) d) ∧
        (SqLe y d x 1 → SqLe w d z 1 → SqLe (x * w + y * z) d (x * z + d * y * w) 1)

Tactic:
⟨?_, ?_, ?_, ?_⟩

Premises used: And.intro
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y z w : ℕ
refine_1 : SqLe x 1 y d → SqLe z 1 w d → SqLe (x * w + y * z) d (x * z + d * y * w) 1
refine_2 : SqLe x 1 y d → SqLe w d z 1 → SqLe (x * z + d * y * w) 1 (x * w + y * z) d
refine_3 : SqLe y d x 1 → SqLe z 1 w d → SqLe (x * z + d * y * w) 1 (x * w + y * z) d
refine_4 : SqLe y d x 1 → SqLe w d z 1 → SqLe (x * w + y * z) d (x * z + d * y * w) 1
⊢ (SqLe x 1 y d → SqLe z 1 w d → SqLe (x * w + y * z) d (x * z + d * y * w) 1) ∧
    (SqLe x 1 y d → SqLe w d z 1 → SqLe (x * z + d * y * w) 1 (x * w + y * z) d) ∧
      (SqLe y d x 1 → SqLe z 1 w d → SqLe (x * z + d * y * w) 1 (x * w + y * z) d) ∧
        (SqLe y d x 1 → SqLe w d z 1 → SqLe (x * w + y * z) d (x * z + d * y * w) 1)

Tactic:
refine ⟨?_, ?_, ?_, ?_⟩
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y z w : ℕ
xy : SqLe x 1 y d
zw : SqLe z 1 w d
⊢ 0 ≤
    HSub.hSub (α := ℤ) (↑(d * y * y) : ℤ) (↑(1 * x * x) : ℤ) * 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 x 1 y d
zw : SqLe z 1 w d
this :
  0 ≤
    HSub.hSub (α := ℤ) (↑(d * y * y) : ℤ) (↑(1 * x * x) : ℤ) * HSub.hSub (α := ℤ) (↑(d * w * w) : ℤ) (↑(1 * z * z) : ℤ)
⊢ 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 x 1 y d
zw : SqLe z 1 w d
this :
  0 ≤
    HSub.hSub (α := ℤ) (↑(d * y * y) : ℤ) (↑(1 * x * x) : ℤ) * HSub.hSub (α := ℤ) (↑(d * w * w) : ℤ) (↑(1 * z * z) : ℤ)
refine_1 :
  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 x 1 y d
zw : SqLe z 1 w d
this :
  0 ≤
    HSub.hSub (α := ℤ) (↑(d * y * y) : ℤ) (↑(1 * x * x) : ℤ) * HSub.hSub (α := ℤ) (↑(d * w * w) : ℤ) (↑(1 * z * z) : ℤ)
⊢ 0 ≤
    HSub.hSub (α := ℤ) (↑(d * y * y) : ℤ) (↑(1 * x * x) : ℤ) * HSub.hSub (α := ℤ) (↑(d * w * w) : ℤ) (↑(1 * z * z) : ℤ)

Tactic:
this
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y z w : ℕ
xy : SqLe x 1 y d
zw : SqLe z 1 w d
this :
  0 ≤
    HSub.hSub (α := ℤ) (↑(d * y * y) : ℤ) (↑(1 * x * x) : ℤ) * HSub.hSub (α := ℤ) (↑(d * w * w) : ℤ) (↑(1 * z * z) : ℤ)
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 (α := ℤ) (↑(d * y * y) : ℤ) (↑(1 * x * x) : ℤ) * HSub.hSub (α := ℤ) (↑(d * w * w) : ℤ) (↑(1 * z * z) : ℤ)
⊢ 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 x 1 y d
zw : SqLe z 1 w d
this :
  0 ≤
    HSub.hSub (α := ℤ) (↑(d * y * y) : ℤ) (↑(1 * x * x) : ℤ) * HSub.hSub (α := ℤ) (↑(d * w * w) : ℤ) (↑(1 * z * z) : ℤ)
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 (α := ℤ) (↑d : ℤ) (↑y : ℤ) * (↑y : ℤ) - HMul.hMul (α := ℤ) (↑x : ℤ) (↑x : ℤ)) *
      (HMul.hMul (α := ℤ) (↑d : ℤ) (↑w : ℤ) * (↑w : ℤ) - HMul.hMul (α := ℤ) (↑z : ℤ) (↑z : ℤ))
⊢ HSub.hSub (α := ℤ) (↑(1 * (x * z + d * y * w) * (x * z + d * y * w)) : ℤ)
      (↑(d * (x * w + y * z) * (x * w + y * z)) : ℤ) =
    HSub.hSub (α := ℤ) (↑(d * y * y) : ℤ) (↑(1 * x * x) : ℤ) * 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 x 1 y d
zw : SqLe z 1 w d
this :
  0 ≤
    HSub.hSub (α := ℤ) (↑(d * y * y) : ℤ) (↑(1 * x * x) : ℤ) * HSub.hSub (α := ℤ) (↑(d * w * w) : ℤ) (↑(1 * z * z) : ℤ)
⊢ (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 (α := ℤ) (↑d : ℤ) (↑y : ℤ) * (↑y : ℤ) - HMul.hMul (α := ℤ) (↑x : ℤ) (↑x : ℤ)) *
      (HMul.hMul (α := ℤ) (↑d : ℤ) (↑w : ℤ) * (↑w : ℤ) - HMul.hMul (α := ℤ) (↑z : ℤ) (↑z : ℤ))

Tactic:
ring