awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hb : -(d * (z.im * z.im)) = 0
mp : z.re = re (d := d) 0
mp₁ : z.im = im (d := d) 0
⊢ z = 0

Tactic:
ext
-- 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
hb : -(d * (z.im * z.im)) = 0
mp : z.re * z.re = 0
⊢ z.re = re (d := d) 0

Tactic:
apply eq_zero_of_mul_self_eq_zero

Premises used: eq_zero_of_mul_self_eq_zero
-- 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
hb : -(d * (z.im * z.im)) = 0
mp : z.im * z.im = 0
⊢ z.im = im (d := d) 0

Tactic:
apply eq_zero_of_mul_self_eq_zero

Premises used: eq_zero_of_mul_self_eq_zero
-- 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
hb : -(d * (z.im * z.im)) = 0
⊢ z.re * z.re = 0

Tactic:
ha
-- 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
hb : -(d * (z.im * z.im)) = 0
⊢ z.re * z.re = 0

Tactic:
exact ha
-- 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
hb : -(d * (z.im * z.im)) = 0
⊢ d = 0 ∨ z.im * z.im = 0

Tactic:
rw [neg_eq_zero, mul_eq_zero] at hb

Premises used: neg_eq_zero, mul_eq_zero
-- 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
hb : d = 0 ∨ z.im * z.im = 0
⊢ z.im * z.im = 0

Tactic:
hb.resolve_left hd.ne

Premises used: Or.resolve_left, LT.lt.ne
-- 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
hb : d = 0 ∨ z.im * z.im = 0
⊢ z.im * z.im = 0

Tactic:
exact hb.resolve_left hd.ne

Premises used: Or.resolve_left, LT.lt.ne
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
hd : d < 0
⊢ norm (d := d) 0 = 0

Tactic:
norm_zero

Premises used: Zsqrtd.norm_zero
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
hd : d < 0
⊢ norm (d := d) 0 = 0

Tactic:
exact norm_zero

Premises used: Zsqrtd.norm_zero
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
hd : d ≤ 0
x y : ℤ√d
h : Associated x y
obtain : ∀ (u : (ℤ√d)ˣ), x.norm = (x * (↑u : ℤ√d)).norm
⊢ x.norm = y.norm

Tactic:
obtain ⟨u, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
hd : d ≤ 0
x : ℤ√d
u : (ℤ√d)ˣ
rw : x.norm = x.norm * (↑u : ℤ√d).norm
rw₁ : x.norm = x.norm * 1
rw₂ rw₃ : x.norm = x.norm
⊢ x.norm = (x * (↑u : ℤ√d)).norm

Tactic:
rw [norm_mul, (norm_eq_one_iff' hd _).mpr u.isUnit, mul_one]

Premises used: Iff.mpr, Zsqrtd.norm_eq_one_iff', Zsqrtd.norm_mul, Units.isUnit, mul_one
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y z w : ℕ
xy_1 : Nonneg (d := d) { re := (↑x : ℤ), im := -(↑y : ℤ) }
zw_1 : Nonneg (d := d) { re := -(↑z : ℤ), im := (↑w : ℤ) }
j k m n : ℕ
xy : SqLe (n + m + 1) d k 1
zw : SqLe (k + j + 1) 1 n d
t : 1 * (k + j + 1) * (k + j + 1) ≤ 1 * k * k := ⋯
⊢ (k + j + 1) * (k + j + 1) ≤ k * k

Tactic:
simpa [one_mul] using t

Premises used: one_mul
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y z w : ℕ
xy : Nonneg (d := d) { re := (↑x : ℤ), im := -(↑y : ℤ) }
zw : Nonneg (d := d) { re := -(↑z : ℤ), im := (↑w : ℤ) }
⊢ Nonneg (d := d) { re := subNatNat x z, im := subNatNat w y }

Tactic:
have : Nonneg ⟨Int.subNatNat x z, Int.subNatNat w y⟩ :=
    Int.subNatNat_elim x z
      (fun m n i => SqLe y d m 1 → SqLe n 1 w d → Nonneg ⟨i, Int.subNatNat w y⟩)
      (fun j k =>
        Int.subNatNat_elim w y
          (fun m n i => SqLe n d (k + j) 1 → SqLe k 1 m d → Nonneg ⟨Int.ofNat j, i⟩)
          (fun _ _ _ _ => trivial) fun m n xy zw => sqLe_cancel zw xy)
      (fun j k =>
        Int.subNatNat_elim w y
          (fun m n i => SqLe n d k 1 → SqLe (k + j + 1) 1 m d → Nonneg ⟨-[j+1], i⟩)
          (fun m n xy zw => sqLe_cancel xy zw) fun m n xy zw =>
          let t := Nat.le_trans zw (sqLe_of_le (Nat.le_add_right n (m + 1)) le_rfl xy)
          have : k + j + 1 ≤ k :=
            Nat.mul_self_le_mul_self_iff.1 (by simpa [one_mul] using t)
          absurd this (not_le_of_gt <| Nat.succ_le_succ <| Nat.le_add_right _ _))
      (nonnegg_pos_neg.1 xy) (nonnegg_neg_pos.1 zw)
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y z w : ℕ
xy : Nonneg (d := d) { re := (↑x : ℤ), im := -(↑y : ℤ) }
zw : Nonneg (d := d) { re := -(↑z : ℤ), im := (↑w : ℤ) }
this : Nonneg (d := d) { re := subNatNat x z, im := subNatNat w y }
rw : Nonneg (d := d) { re := HAdd.hAdd (α := ℤ) (↑x : ℤ) (-(↑z : ℤ)), im := HSub.hSub (α := ℤ) (↑w : ℤ) (↑y : ℤ) }
⊢ (HAdd.hAdd (α := ℤ√(↑d : ℤ)) { re := (↑x : ℤ), im := -(↑y : ℤ) : ℤ√(↑d : ℤ) }
      { re := -(↑z : ℤ), im := (↑w : ℤ) : ℤ√(↑d : ℤ) }).Nonneg

Tactic:
rw [add_def, neg_add_eq_sub]

Premises used: neg_add_eq_sub, Zsqrtd.add_def
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y z w : ℕ
xy : Nonneg (d := d) { re := (↑x : ℤ), im := -(↑y : ℤ) }
zw : Nonneg (d := d) { re := -(↑z : ℤ), im := (↑w : ℤ) }
this : Nonneg (d := d) { re := subNatNat x z, im := subNatNat w y }
rwa :
  ∀ (this : Nonneg (d := d) { re := HSub.hSub (α := ℤ) (↑x : ℤ) (↑z : ℤ), im := subNatNat w y }),
    Nonneg (d := d) { re := HAdd.hAdd (α := ℤ) (↑x : ℤ) (-(↑z : ℤ)), im := HSub.hSub (α := ℤ) (↑w : ℤ) (↑y : ℤ) }
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (this : Nonneg (d := d) { re := HSub.hSub (α := ℤ) (↑x : ℤ) (↑z : ℤ), im := HSub.hSub (α := ℤ) (↑w : ℤ) (↑y : ℤ) }),
    Nonneg (d := d) { re := HAdd.hAdd (α := ℤ) (↑x : ℤ) (-(↑z : ℤ)), im := HSub.hSub (α := ℤ) (↑w : ℤ) (↑y : ℤ) }
⊢ Nonneg (d := d) { re := HAdd.hAdd (α := ℤ) (↑x : ℤ) (-(↑z : ℤ)), im := HSub.hSub (α := ℤ) (↑w : ℤ) (↑y : ℤ) }

Tactic:
rwa [Int.subNatNat_eq_coe, Int.subNatNat_eq_coe] at this

Premises used: Int.subNatNat_eq_coe
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
a b : ℤ√(↑d : ℤ)
ha : a.Nonneg
hb : b.Nonneg
inl :
  ∀ (x y : ℕ) (ha : Nonneg (d := d) { re := (↑x : ℤ), im := (↑y : ℤ) }),
    ({ re := (↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) } + b).Nonneg
inr :
  ∀ (x y : ℕ) (ha : Nonneg (d := d) { re := (↑x : ℤ), im := -(↑y : ℤ) }),
    ({ re := (↑x : ℤ), im := -(↑y : ℤ) : ℤ√(↑d : ℤ) } + b).Nonneg
inr₁ :
  ∀ (x y : ℕ) (ha : Nonneg (d := d) { re := -(↑x : ℤ), im := (↑y : ℤ) }),
    ({ re := -(↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) } + b).Nonneg
⊢ (a + b).Nonneg

Tactic:
rcases nonneg_cases ha with ⟨x, y, rfl | rfl | rfl⟩

Premises used: rfl, Zsqrtd.nonneg_cases
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
b : ℤ√(↑d : ℤ)
hb : b.Nonneg
x y : ℕ
ha : Nonneg (d := d) { re := (↑x : ℤ), im := (↑y : ℤ) }
inl :
  ∀ (z w : ℕ) (hb : Nonneg (d := d) { re := (↑z : ℤ), im := (↑w : ℤ) }),
    (HAdd.hAdd (α := ℤ√(↑d : ℤ)) { re := (↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) }
        { re := (↑z : ℤ), im := (↑w : ℤ) : ℤ√(↑d : ℤ) }).Nonneg
inl₁ :
  ∀ (z w : ℕ) (hb : Nonneg (d := d) { re := (↑z : ℤ), im := -(↑w : ℤ) }),
    (HAdd.hAdd (α := ℤ√(↑d : ℤ)) { re := (↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) }
        { re := (↑z : ℤ), im := -(↑w : ℤ) : ℤ√(↑d : ℤ) }).Nonneg
inl₂ :
  ∀ (z w : ℕ) (hb : Nonneg (d := d) { re := -(↑z : ℤ), im := (↑w : ℤ) }),
    (HAdd.hAdd (α := ℤ√(↑d : ℤ)) { re := (↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) }
        { re := -(↑z : ℤ), im := (↑w : ℤ) : ℤ√(↑d : ℤ) }).Nonneg
⊢ ({ re := (↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) } + b).Nonneg

Tactic:
rcases nonneg_cases hb with ⟨z, w, rfl | rfl | rfl⟩

Premises used: rfl, Zsqrtd.nonneg_cases
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
b : ℤ√(↑d : ℤ)
hb : b.Nonneg
x y : ℕ
ha : Nonneg (d := d) { re := (↑x : ℤ), im := -(↑y : ℤ) }
inr :
  ∀ (z w : ℕ) (hb : Nonneg (d := d) { re := (↑z : ℤ), im := (↑w : ℤ) }),
    (HAdd.hAdd (α := ℤ√(↑d : ℤ)) { re := (↑x : ℤ), im := -(↑y : ℤ) : ℤ√(↑d : ℤ) }
        { re := (↑z : ℤ), im := (↑w : ℤ) : ℤ√(↑d : ℤ) }).Nonneg
inr₁ :
  ∀ (z w : ℕ) (hb : Nonneg (d := d) { re := (↑z : ℤ), im := -(↑w : ℤ) }),
    (HAdd.hAdd (α := ℤ√(↑d : ℤ)) { re := (↑x : ℤ), im := -(↑y : ℤ) : ℤ√(↑d : ℤ) }
        { re := (↑z : ℤ), im := -(↑w : ℤ) : ℤ√(↑d : ℤ) }).Nonneg
inr₂ :
  ∀ (z w : ℕ) (hb : Nonneg (d := d) { re := -(↑z : ℤ), im := (↑w : ℤ) }),
    (HAdd.hAdd (α := ℤ√(↑d : ℤ)) { re := (↑x : ℤ), im := -(↑y : ℤ) : ℤ√(↑d : ℤ) }
        { re := -(↑z : ℤ), im := (↑w : ℤ) : ℤ√(↑d : ℤ) }).Nonneg
⊢ ({ re := (↑x : ℤ), im := -(↑y : ℤ) : ℤ√(↑d : ℤ) } + b).Nonneg

Tactic:
rcases nonneg_cases hb with ⟨z, w, rfl | rfl | rfl⟩

Premises used: rfl, Zsqrtd.nonneg_cases
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
b : ℤ√(↑d : ℤ)
hb : b.Nonneg
x y : ℕ
ha : Nonneg (d := d) { re := -(↑x : ℤ), im := (↑y : ℤ) }
inr :
  ∀ (z w : ℕ) (hb : Nonneg (d := d) { re := (↑z : ℤ), im := (↑w : ℤ) }),
    (HAdd.hAdd (α := ℤ√(↑d : ℤ)) { re := -(↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) }
        { re := (↑z : ℤ), im := (↑w : ℤ) : ℤ√(↑d : ℤ) }).Nonneg
inr₁ :
  ∀ (z w : ℕ) (hb : Nonneg (d := d) { re := (↑z : ℤ), im := -(↑w : ℤ) }),
    (HAdd.hAdd (α := ℤ√(↑d : ℤ)) { re := -(↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) }
        { re := (↑z : ℤ), im := -(↑w : ℤ) : ℤ√(↑d : ℤ) }).Nonneg
inr₂ :
  ∀ (z w : ℕ) (hb : Nonneg (d := d) { re := -(↑z : ℤ), im := (↑w : ℤ) }),
    (HAdd.hAdd (α := ℤ√(↑d : ℤ)) { re := -(↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) }
        { re := -(↑z : ℤ), im := (↑w : ℤ) : ℤ√(↑d : ℤ) }).Nonneg
⊢ ({ re := -(↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) } + b).Nonneg

Tactic:
rcases nonneg_cases hb with ⟨z, w, rfl | rfl | rfl⟩

Premises used: rfl, Zsqrtd.nonneg_cases
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y : ℕ
ha : Nonneg (d := d) { re := (↑x : ℤ), im := (↑y : ℤ) }
z w : ℕ
hb : Nonneg (d := d) { re := (↑z : ℤ), im := (↑w : ℤ) }
⊢ (HAdd.hAdd (α := ℤ√(↑d : ℤ)) { re := (↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) }
      { re := (↑z : ℤ), im := (↑w : ℤ) : ℤ√(↑d : ℤ) }).Nonneg

Tactic:
trivial
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y : ℕ
ha : Nonneg (d := d) { re := (↑x : ℤ), im := (↑y : ℤ) }
z w : ℕ
hb : Nonneg (d := d) { re := (↑z : ℤ), im := -(↑w : ℤ) }
⊢ (HAdd.hAdd (α := ℤ√(↑d : ℤ)) { re := (↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) }
      { re := (↑z : ℤ), im := -(↑w : ℤ) : ℤ√(↑d : ℤ) }).Nonneg

Tactic:
nonnegg_cases_right fun i h => sqLe_of_le ?_ ?_ (nonnegg_pos_neg.1 hb)

Premises used: Zsqrtd.sqLe_of_le, Zsqrtd.nonnegg_cases_right, Iff.mp, Zsqrtd.nonnegg_pos_neg, Zsqrtd.Nonneg, Int.add
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y : ℕ
ha : Nonneg (d := d) { re := (↑x : ℤ), im := (↑y : ℤ) }
z w : ℕ
hb : Nonneg (d := d) { re := (↑z : ℤ), im := -(↑w : ℤ) }
inl :
  ∀ (i : ℕ)
    (h :
      im (d := (↑d : ℤ)) { re := (↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) } +
          im (d := (↑d : ℤ)) { re := (↑z : ℤ), im := -(↑w : ℤ) : ℤ√(↑d : ℤ) } =
        -(↑i : ℤ)),
    i ≤ w
inl₁ :
  ∀ (i : ℕ)
    (h :
      im (d := (↑d : ℤ)) { re := (↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) } +
          im (d := (↑d : ℤ)) { re := (↑z : ℤ), im := -(↑w : ℤ) : ℤ√(↑d : ℤ) } =
        -(↑i : ℤ)),
    z ≤ x + z
⊢ (HAdd.hAdd (α := ℤ√(↑d : ℤ)) { re := (↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) }
      { re := (↑z : ℤ), im := -(↑w : ℤ) : ℤ√(↑d : ℤ) }).Nonneg

Tactic:
refine nonnegg_cases_right fun i h => sqLe_of_le ?_ ?_ (nonnegg_pos_neg.1 hb)

Premises used: Zsqrtd.sqLe_of_le, Zsqrtd.nonnegg_cases_right, Iff.mp, Zsqrtd.nonnegg_pos_neg
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y : ℕ
ha : Nonneg (d := d) { re := (↑x : ℤ), im := (↑y : ℤ) }
z w : ℕ
hb : Nonneg (d := d) { re := (↑z : ℤ), im := -(↑w : ℤ) }
i : ℕ
h : HAdd.hAdd (α := ℤ) (↑y : ℤ) (-(↑w : ℤ)) = -(↑i : ℤ)
⊢ HAdd.hAdd (α := ℤ) (-(↑w : ℤ)) (↑y : ℤ) = -(↑i : ℤ)

Tactic:
simp [add_comm, *]

Premises used: add_comm
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y : ℕ
ha : Nonneg (d := d) { re := (↑x : ℤ), im := (↑y : ℤ) }
z w : ℕ
hb : Nonneg (d := d) { re := (↑z : ℤ), im := -(↑w : ℤ) }
i : ℕ
h : HAdd.hAdd (α := ℤ) (↑y : ℤ) (-(↑w : ℤ)) = -(↑i : ℤ)
⊢ i ≤ w

Tactic:
exact Int.ofNat_le.1 (le_of_neg_le_neg (Int.le.intro y (by simp [add_comm, *])))

Premises used: le_of_neg_le_neg, Int.le.intro, Iff.mp, Int.ofNat_le
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y : ℕ
ha : Nonneg (d := d) { re := (↑x : ℤ), im := (↑y : ℤ) }
z w : ℕ
hb : Nonneg (d := d) { re := (↑z : ℤ), im := -(↑w : ℤ) }
i : ℕ
h :
  im (d := (↑d : ℤ)) { re := (↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) } +
      im (d := (↑d : ℤ)) { re := (↑z : ℤ), im := -(↑w : ℤ) : ℤ√(↑d : ℤ) } =
    -(↑i : ℤ)
⊢ z ≤ x + z

Tactic:
apply Nat.le_add_left

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

Tactic:
nonnegg_cases_left fun i h => sqLe_of_le ?_ ?_ (nonnegg_neg_pos.1 hb)

Premises used: Zsqrtd.nonnegg_cases_left, Zsqrtd.sqLe_of_le, Zsqrtd.nonnegg_neg_pos, Iff.mp, Zsqrtd.Nonneg, Int.add
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y : ℕ
ha : Nonneg (d := d) { re := (↑x : ℤ), im := (↑y : ℤ) }
z w : ℕ
hb : Nonneg (d := d) { re := -(↑z : ℤ), im := (↑w : ℤ) }
inl :
  ∀ (i : ℕ)
    (h :
      re (d := (↑d : ℤ)) { re := (↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) } +
          re (d := (↑d : ℤ)) { re := -(↑z : ℤ), im := (↑w : ℤ) : ℤ√(↑d : ℤ) } =
        -(↑i : ℤ)),
    i ≤ z
inl₁ :
  ∀ (i : ℕ)
    (h :
      re (d := (↑d : ℤ)) { re := (↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) } +
          re (d := (↑d : ℤ)) { re := -(↑z : ℤ), im := (↑w : ℤ) : ℤ√(↑d : ℤ) } =
        -(↑i : ℤ)),
    w ≤ y + w
⊢ (HAdd.hAdd (α := ℤ√(↑d : ℤ)) { re := (↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) }
      { re := -(↑z : ℤ), im := (↑w : ℤ) : ℤ√(↑d : ℤ) }).Nonneg

Tactic:
refine nonnegg_cases_left fun i h => sqLe_of_le ?_ ?_ (nonnegg_neg_pos.1 hb)

Premises used: Zsqrtd.nonnegg_cases_left, Zsqrtd.sqLe_of_le, Zsqrtd.nonnegg_neg_pos, Iff.mp
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y : ℕ
ha : Nonneg (d := d) { re := (↑x : ℤ), im := (↑y : ℤ) }
z w : ℕ
hb : Nonneg (d := d) { re := -(↑z : ℤ), im := (↑w : ℤ) }
i : ℕ
h : HAdd.hAdd (α := ℤ) (↑x : ℤ) (-(↑z : ℤ)) = -(↑i : ℤ)
⊢ HAdd.hAdd (α := ℤ) (-(↑z : ℤ)) (↑x : ℤ) = -(↑i : ℤ)

Tactic:
simp [add_comm, *]

Premises used: add_comm
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y : ℕ
ha : Nonneg (d := d) { re := (↑x : ℤ), im := (↑y : ℤ) }
z w : ℕ
hb : Nonneg (d := d) { re := -(↑z : ℤ), im := (↑w : ℤ) }
i : ℕ
h : HAdd.hAdd (α := ℤ) (↑x : ℤ) (-(↑z : ℤ)) = -(↑i : ℤ)
⊢ i ≤ z

Tactic:
exact Int.ofNat_le.1 (le_of_neg_le_neg (Int.le.intro x (by simp [add_comm, *])))

Premises used: le_of_neg_le_neg, Int.le.intro, Iff.mp, Int.ofNat_le
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y : ℕ
ha : Nonneg (d := d) { re := (↑x : ℤ), im := (↑y : ℤ) }
z w : ℕ
hb : Nonneg (d := d) { re := -(↑z : ℤ), im := (↑w : ℤ) }
i : ℕ
h :
  re (d := (↑d : ℤ)) { re := (↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) } +
      re (d := (↑d : ℤ)) { re := -(↑z : ℤ), im := (↑w : ℤ) : ℤ√(↑d : ℤ) } =
    -(↑i : ℤ)
⊢ w ≤ y + w

Tactic:
apply Nat.le_add_left

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

Tactic:
nonnegg_cases_right fun i h => sqLe_of_le ?_ ?_ (nonnegg_pos_neg.1 ha)

Premises used: Zsqrtd.sqLe_of_le, Zsqrtd.nonnegg_cases_right, Iff.mp, Zsqrtd.nonnegg_pos_neg, Zsqrtd.Nonneg, Int.add
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y : ℕ
ha : Nonneg (d := d) { re := (↑x : ℤ), im := -(↑y : ℤ) }
z w : ℕ
hb : Nonneg (d := d) { re := (↑z : ℤ), im := (↑w : ℤ) }
inr :
  ∀ (i : ℕ)
    (h :
      im (d := (↑d : ℤ)) { re := (↑x : ℤ), im := -(↑y : ℤ) : ℤ√(↑d : ℤ) } +
          im (d := (↑d : ℤ)) { re := (↑z : ℤ), im := (↑w : ℤ) : ℤ√(↑d : ℤ) } =
        -(↑i : ℤ)),
    i ≤ y
inr₁ :
  ∀ (i : ℕ)
    (h :
      im (d := (↑d : ℤ)) { re := (↑x : ℤ), im := -(↑y : ℤ) : ℤ√(↑d : ℤ) } +
          im (d := (↑d : ℤ)) { re := (↑z : ℤ), im := (↑w : ℤ) : ℤ√(↑d : ℤ) } =
        -(↑i : ℤ)),
    x ≤ x + z
⊢ (HAdd.hAdd (α := ℤ√(↑d : ℤ)) { re := (↑x : ℤ), im := -(↑y : ℤ) : ℤ√(↑d : ℤ) }
      { re := (↑z : ℤ), im := (↑w : ℤ) : ℤ√(↑d : ℤ) }).Nonneg

Tactic:
refine nonnegg_cases_right fun i h => sqLe_of_le ?_ ?_ (nonnegg_pos_neg.1 ha)

Premises used: Zsqrtd.sqLe_of_le, Zsqrtd.nonnegg_cases_right, Iff.mp, Zsqrtd.nonnegg_pos_neg
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y : ℕ
ha : Nonneg (d := d) { re := (↑x : ℤ), im := -(↑y : ℤ) }
z w : ℕ
hb : Nonneg (d := d) { re := (↑z : ℤ), im := (↑w : ℤ) }
i : ℕ
h : HAdd.hAdd (α := ℤ) (-(↑y : ℤ)) (↑w : ℤ) = -(↑i : ℤ)
⊢ HAdd.hAdd (α := ℤ) (-(↑y : ℤ)) (↑w : ℤ) = -(↑i : ℤ)

Tactic:
simp [*]
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y : ℕ
ha : Nonneg (d := d) { re := (↑x : ℤ), im := -(↑y : ℤ) }
z w : ℕ
hb : Nonneg (d := d) { re := (↑z : ℤ), im := (↑w : ℤ) }
i : ℕ
h : HAdd.hAdd (α := ℤ) (-(↑y : ℤ)) (↑w : ℤ) = -(↑i : ℤ)
⊢ i ≤ y

Tactic:
exact Int.ofNat_le.1 (le_of_neg_le_neg (Int.le.intro w (by simp [*])))

Premises used: le_of_neg_le_neg, Int.le.intro, Iff.mp, Int.ofNat_le
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y : ℕ
ha : Nonneg (d := d) { re := (↑x : ℤ), im := -(↑y : ℤ) }
z w : ℕ
hb : Nonneg (d := d) { re := (↑z : ℤ), im := (↑w : ℤ) }
i : ℕ
h :
  im (d := (↑d : ℤ)) { re := (↑x : ℤ), im := -(↑y : ℤ) : ℤ√(↑d : ℤ) } +
      im (d := (↑d : ℤ)) { re := (↑z : ℤ), im := (↑w : ℤ) : ℤ√(↑d : ℤ) } =
    -(↑i : ℤ)
⊢ x ≤ x + z

Tactic:
apply Nat.le_add_right

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

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

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

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

Tactic:
rwa [add_def]

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

Tactic:
nonneg_add_lem ha hb

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

Tactic:
exact nonneg_add_lem ha hb

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

Tactic:
nonnegg_cases_left fun i h => sqLe_of_le ?_ ?_ (nonnegg_neg_pos.1 ha)

Premises used: Zsqrtd.nonnegg_cases_left, Zsqrtd.sqLe_of_le, Zsqrtd.nonnegg_neg_pos, Iff.mp, Zsqrtd.Nonneg, Int.add
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y : ℕ
ha : Nonneg (d := d) { re := -(↑x : ℤ), im := (↑y : ℤ) }
z w : ℕ
hb : Nonneg (d := d) { re := (↑z : ℤ), im := (↑w : ℤ) }
inr :
  ∀ (i : ℕ)
    (h :
      re (d := (↑d : ℤ)) { re := -(↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) } +
          re (d := (↑d : ℤ)) { re := (↑z : ℤ), im := (↑w : ℤ) : ℤ√(↑d : ℤ) } =
        -(↑i : ℤ)),
    i ≤ x
inr₁ :
  ∀ (i : ℕ)
    (h :
      re (d := (↑d : ℤ)) { re := -(↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) } +
          re (d := (↑d : ℤ)) { re := (↑z : ℤ), im := (↑w : ℤ) : ℤ√(↑d : ℤ) } =
        -(↑i : ℤ)),
    y ≤ y + w
⊢ (HAdd.hAdd (α := ℤ√(↑d : ℤ)) { re := -(↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) }
      { re := (↑z : ℤ), im := (↑w : ℤ) : ℤ√(↑d : ℤ) }).Nonneg

Tactic:
refine nonnegg_cases_left fun i h => sqLe_of_le ?_ ?_ (nonnegg_neg_pos.1 ha)

Premises used: Zsqrtd.nonnegg_cases_left, Zsqrtd.sqLe_of_le, Zsqrtd.nonnegg_neg_pos, Iff.mp
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y : ℕ
ha : Nonneg (d := d) { re := -(↑x : ℤ), im := (↑y : ℤ) }
z w : ℕ
hb : Nonneg (d := d) { re := (↑z : ℤ), im := (↑w : ℤ) }
i : ℕ
h : HAdd.hAdd (α := ℤ) (-(↑x : ℤ)) (↑z : ℤ) = -(↑i : ℤ)
⊢ i ≤ x

Tactic:
Int.ofNat_le.1 (le_of_neg_le_neg (Int.le.intro _ h))

Premises used: le_of_neg_le_neg, Int.le.intro, Iff.mp, Int.ofNat_le
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y : ℕ
ha : Nonneg (d := d) { re := -(↑x : ℤ), im := (↑y : ℤ) }
z w : ℕ
hb : Nonneg (d := d) { re := (↑z : ℤ), im := (↑w : ℤ) }
i : ℕ
h : HAdd.hAdd (α := ℤ) (-(↑x : ℤ)) (↑z : ℤ) = -(↑i : ℤ)
⊢ i ≤ x

Tactic:
exact Int.ofNat_le.1 (le_of_neg_le_neg (Int.le.intro _ h))

Premises used: le_of_neg_le_neg, Int.le.intro, Iff.mp, Int.ofNat_le
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y : ℕ
ha : Nonneg (d := d) { re := -(↑x : ℤ), im := (↑y : ℤ) }
z w : ℕ
hb : Nonneg (d := d) { re := (↑z : ℤ), im := (↑w : ℤ) }
i : ℕ
h :
  re (d := (↑d : ℤ)) { re := -(↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) } +
      re (d := (↑d : ℤ)) { re := (↑z : ℤ), im := (↑w : ℤ) : ℤ√(↑d : ℤ) } =
    -(↑i : ℤ)
⊢ y ≤ y + w

Tactic:
apply Nat.le_add_right

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

Tactic:
rw [add_comm, add_comm (y : ℤ)]

Premises used: Nat.cast, add_comm
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y : ℕ
ha : Nonneg (d := d) { re := -(↑x : ℤ), im := (↑y : ℤ) }
z w : ℕ
hb : Nonneg (d := d) { re := (↑z : ℤ), im := -(↑w : ℤ) }
⊢ Nonneg (d := d) { re := HAdd.hAdd (α := ℤ) (↑z : ℤ) (-(↑x : ℤ)), im := HAdd.hAdd (α := ℤ) (-(↑w : ℤ)) (↑y : ℤ) }

Tactic:
nonneg_add_lem hb ha

Premises used: Zsqrtd.nonneg_add_lem