awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
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
have refine_1 : a = HMul.hMul (α := ℤ√d) (↑(↑(a.re.gcd a.im) : ℤ) : ℤ√d) { re := re, im := im }
Tactic: refine ⟨⟨re, im⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
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 }
⊢ ∃ (b : ℤ√d), a = (↑(↑(a.re.gcd a.im) : ℤ) : ℤ√d) * b ∧ IsCoprime b.re b.im
have refine_2 : IsCoprime (Zsqrtd.re (d := d) { re := re, im := im : ℤ√d }) (Zsqrtd.im (d := d) { re := re, im := im })
Tactic: refine ⟨⟨re, im⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
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
⊢ a = HMul.hMul (α := ℤ√d) (↑(↑(a.re.gcd a.im) : ℤ) : ℤ√d) { re := re, im := im }
have refine_1 : a = { re := (↑(a.re.gcd a.im) : ℤ) * re, im := (↑(a.re.gcd a.im) : ℤ) * im }
Tactic: rw [smul_val, ← Hre, ← Him]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
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 }
⊢ a = HMul.hMul (α := ℤ√d) (↑(↑(a.re.gcd a.im) : ℤ) : ℤ√d) { re := re, im := im }
have refine_1₁ : a = { re := a.re, im := (↑(a.re.gcd a.im) : ℤ) * im }
Tactic: rw [smul_val, ← Hre, ← Him]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
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 }
⊢ a = HMul.hMul (α := ℤ√d) (↑(↑(a.re.gcd a.im) : ℤ) : ℤ√d) { re := re, im := im }
have refine_1₂ : a = { re := a.re, im := a.im }
Tactic: rw [smul_val, ← Hre, ← Him]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
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
⊢ IsCoprime (Zsqrtd.re (d := d) { re := re, im := im : ℤ√d }) (Zsqrtd.im (d := d) { re := re, im := im })
have refine_2 : (Zsqrtd.re (d := d) { re := re, im := im : ℤ√d }).gcd (Zsqrtd.im (d := d) { re := re, im := im : ℤ√d }) = 1
Tactic: rw [Int.isCoprime_iff_gcd_eq_one, H1]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
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
⊢ IsCoprime (Zsqrtd.re (d := d) { re := re, im := im : ℤ√d }) (Zsqrtd.im (d := d) { re := re, im := im })
have refine_2₁ : Eq (α := ℕ) 1 1
Tactic: rw [Int.isCoprime_iff_gcd_eq_one, H1]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (hypothesis)
Goal:
c d x y z w : ℕ
xy : SqLe x c y d
zw : SqLe z c w d
⊢ SqLe (x + z) c (y + w) d
have xz : c * (x * z) ≤ d * (y * w)
Tactic: have xz := sqLe_add_mixed xy zw
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (hypothesis)
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)
⊢ SqLe (x + z) c (y + w) d
have xy₁ : c * (x * x) ≤ d * (y * y)
Tactic: simp only [SqLe, mul_assoc] at xy zw
Cleared hypotheses: xy, zw
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (hypothesis)
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)
⊢ SqLe (x + z) c (y + w) d
have zw₁ : c * (z * z) ≤ d * (w * w)
Tactic: simp only [SqLe, mul_assoc] at xy zw
Cleared hypotheses: xy, zw
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
c d x y z w : ℕ
zw : SqLe y d x c
h : SqLe (x + z) c (y + w) d
⊢ SqLe z c w d
have h₁ : ¬d * w * w < c * z * z
Tactic: apply le_of_not_gt
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
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
have h₁ : d * (y + w) * (y + w) < c * (x + z) * (x + z)
Tactic: refine not_le_of_gt ?_ h
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
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) * (y + w) < c * (x + z) * (x + z)
have 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)))
Tactic: simp only [mul_add, mul_comm, mul_left_comm, add_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (hypothesis)
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 * y) + (d * (y * w) + (d * (y * w) + d * (w * w))) < c * (x * x) + (c * (x * z) + (c * (x * z) + c * (z * z)))
have hm : d * (y * w) ≤ c * (x * z)
Tactic: have hm := sqLe_add_mixed zw (le_of_lt l)
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (hypothesis)
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 * (y * y) + (d * (y * w) + (d * (y * w) + d * (w * w))) < c * (x * x) + (c * (x * z) + (c * (x * z) + c * (z * z)))
have l₁ : d * (w * w) < c * (z * z)
Tactic: simp only [SqLe, mul_assoc] at l zw
Cleared hypotheses: zw, l
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (hypothesis)
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) + (d * (y * w) + (d * (y * w) + d * (w * w))) < c * (x * x) + (c * (x * z) + (c * (x * z) + c * (z * z)))
have zw₁ : d * (y * y) ≤ c * (x * x)
Tactic: simp only [SqLe, mul_assoc] at l zw
Cleared hypotheses: zw, l
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
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)
⊢ d * (y * y) + (d * (y * w) + (d * (y * w) + d * (w * w))) < c * (x * x) + (c * (x * z) + (c * (x * z) + c * (z * z)))
have 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)))
Tactic: grw [zw, hm]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
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)
have refine_1 : SqLe x 1 y d → SqLe z 1 w d → SqLe (x * w + y * z) d (x * z + d * y * w) 1
Tactic: refine ⟨?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
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
⊢ (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)
have refine_2 : SqLe x 1 y d → SqLe w d z 1 → SqLe (x * z + d * y * w) 1 (x * w + y * z) d
Tactic: refine ⟨?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
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
⊢ (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)
have refine_3 : SqLe y d x 1 → SqLe z 1 w d → SqLe (x * z + d * y * w) 1 (x * w + y * z) d
Tactic: refine ⟨?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
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
⊢ (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)
have refine_4 : SqLe y d x 1 → SqLe w d z 1 → SqLe (x * w + y * z) d (x * z + d * y * w) 1
Tactic: refine ⟨?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (hypothesis)
Goal:
d x y z w : ℕ
xy : SqLe x 1 y d
zw : SqLe z 1 w d
⊢ SqLe (x * w + y * z) d (x * z + d * y * w) 1
have this : 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))
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
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
have 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)) : ℤ)
Tactic: refine Int.le_of_ofNat_le_ofNat (le_of_sub_nonneg ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
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 (α := ℤ) (↑(1 * (x * z + d * y * w) * (x * z + d * y * w)) : ℤ)
      (↑(d * (x * w + y * z) * (x * w + y * z)) : ℤ)
have 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) : ℤ)
Tactic: convert! this using 1
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
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) : ℤ)
⊢ 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) : ℤ)
have 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 : ℤ))
Tactic: simp only [one_mul, Int.natCast_add, Int.natCast_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (hypothesis)
Goal:
d x y z w : ℕ
xy : SqLe x 1 y d
zw : SqLe w d z 1
⊢ SqLe (x * z + d * y * w) 1 (x * w + y * z) d
have this : 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))
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
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
have 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)) : ℤ)
Tactic: refine Int.le_of_ofNat_le_ofNat (le_of_sub_nonneg ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
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 * (x * w + y * z) * (x * w + y * z)) : ℤ)
      (↑(1 * (x * z + d * y * w) * (x * z + d * y * w)) : ℤ)
have 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) : ℤ)
Tactic: convert! this using 1
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
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) : ℤ)
⊢ 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) : ℤ)
have 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 : ℤ))
Tactic: simp only [one_mul, Int.natCast_add, Int.natCast_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (hypothesis)
Goal:
d x y z w : ℕ
xy : SqLe y d x 1
zw : SqLe z 1 w d
⊢ SqLe (x * z + d * y * w) 1 (x * w + y * z) d
have this : 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))
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
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
have 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)) : ℤ)
Tactic: refine Int.le_of_ofNat_le_ofNat (le_of_sub_nonneg ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
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 (α := ℤ) (↑(d * (x * w + y * z) * (x * w + y * z)) : ℤ)
      (↑(1 * (x * z + d * y * w) * (x * z + d * y * w)) : ℤ)
have 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) : ℤ)
Tactic: convert! this using 1
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
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) : ℤ)
⊢ 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) : ℤ)
have 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 : ℤ))
Tactic: simp only [one_mul, Int.natCast_add, Int.natCast_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (hypothesis)
Goal:
d x y z w : ℕ
xy : SqLe y d x 1
zw : SqLe w d z 1
⊢ SqLe (x * w + y * z) d (x * z + d * y * w) 1
have this : 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))
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
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
have 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)) : ℤ)
Tactic: refine Int.le_of_ofNat_le_ofNat (le_of_sub_nonneg ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
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 * z + d * y * w) * (x * z + d * y * w)) : ℤ)
      (↑(d * (x * w + y * z) * (x * w + y * z)) : ℤ)
have 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) : ℤ)
Tactic: convert! this using 1
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
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) : ℤ)
⊢ 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) : ℤ)
have 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 : ℤ))
Tactic: simp only [one_mul, Int.natCast_add, Int.natCast_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
c d : ℕ
x y : ℤ
⊢ Nonnegg c d x y = Nonnegg d c y x
have ofNat : ∀ (a : ℕ), Nonnegg c d (Int.ofNat a) y = Nonnegg d c y (Int.ofNat a)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
c d : ℕ
x y : ℤ
ofNat : ∀ (a : ℕ), Nonnegg c d (Int.ofNat a) y = Nonnegg d c y (Int.ofNat a)
⊢ Nonnegg c d x y = Nonnegg d c y x
have negSucc : ∀ (a : ℕ), Nonnegg c d (Int.negSucc a) y = Nonnegg d c y (Int.negSucc a)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
c d : ℕ
y : ℤ
a : ℕ
⊢ Nonnegg c d (Int.ofNat a) y = Nonnegg d c y (Int.ofNat a)
have ofNat : ∀ (a_1 : ℕ), Nonnegg c d (Int.ofNat a) (Int.ofNat a_1) = Nonnegg d c (Int.ofNat a_1) (Int.ofNat a)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
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)
⊢ Nonnegg c d (Int.ofNat a) y = Nonnegg d c y (Int.ofNat a)
have ofNat₁ : ∀ (a_1 : ℕ), Nonnegg c d (Int.ofNat a) (Int.negSucc a_1) = Nonnegg d c (Int.negSucc a_1) (Int.ofNat a)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
c d : ℕ
y : ℤ
a : ℕ
⊢ Nonnegg c d (Int.negSucc a) y = Nonnegg d c y (Int.negSucc a)
have negSucc : ∀ (a_1 : ℕ), Nonnegg c d (Int.negSucc a) (Int.ofNat a_1) = Nonnegg d c (Int.ofNat a_1) (Int.negSucc a)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
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)
⊢ Nonnegg c d (Int.negSucc a) y = Nonnegg d c y (Int.negSucc a)
have negSucc₁ : ∀ (a_1 : ℕ), Nonnegg c d (Int.negSucc a) (Int.negSucc a_1) = Nonnegg d c (Int.negSucc a_1) (Int.negSucc a)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
c d a b : ℕ
⊢ Nonnegg c d (↑a : ℤ) (-(↑b : ℤ)) ↔ SqLe b c a d
have rw : Nonnegg d c (-(↑b : ℤ)) (↑a : ℤ) ↔ SqLe b c a d
Tactic: rw [nonnegg_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
n : ℤ√d
⊢ (↑n.norm : ℤ√d) = n * star n
have re : re (d := d) (↑n.norm : ℤ√d) = (n * star n).re
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
n : ℤ√d
re : Zsqrtd.re (d := d) (↑n.norm : ℤ√d) = (n * star n).re
⊢ (↑n.norm : ℤ√d) = n * star n
have im : im (d := d) (↑n.norm : ℤ√d) = (n * star n).im
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
hd : d ≤ 0
n : ℤ√d
⊢ 0 ≤ -(d * n.im * n.im)
have rw : 0 ≤ -d * (n.im * n.im)
Tactic: rw [mul_assoc, neg_mul_eq_neg_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
x : ℤ√d
h : x.norm.natAbs = 1
hx : 0 ≤ x.norm
⊢ 1 = x * star x
have rwa : ∀ (h : Eq (α := ℤ) (↑x.norm.natAbs : ℤ) (↑1 : ℤ)) (hx : 0 ≤ x.norm), 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
Cleared hypotheses: h, hx