awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℕ
b : ℤ√(↑d : ℤ)
hb : b.Nonneg
x y : ℕ
ha : Nonneg (d := d) { re := -(↑x : ℤ), im := (↑y : ℤ) }
⊢ ({ re := -(↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) } + b).Nonneg
have 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
Tactic: rcases nonneg_cases hb with ⟨z, w, rfl | rfl | rfl⟩
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
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
⊢ ({ re := -(↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) } + b).Nonneg
have 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
Tactic: rcases nonneg_cases hb with ⟨z, w, rfl | rfl | rfl⟩
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
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
⊢ ({ re := -(↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) } + b).Nonneg
have 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
Tactic: rcases nonneg_cases hb with ⟨z, w, rfl | rfl | rfl⟩
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
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
have inl : ∀ (i : ℕ)
  (h :
    im (d := (↑d : ℤ)) { re := (↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) } +
        im (d := (↑d : ℤ)) { re := (↑z : ℤ), im := -(↑w : ℤ) : ℤ√(↑d : ℤ) } =
      -(↑i : ℤ)),
  i ≤ w
Tactic: refine nonnegg_cases_right fun i h => sqLe_of_le ?_ ?_ (nonnegg_pos_neg.1 hb)
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
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
⊢ (HAdd.hAdd (α := ℤ√(↑d : ℤ)) { re := (↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) }
      { re := (↑z : ℤ), im := -(↑w : ℤ) : ℤ√(↑d : ℤ) }).Nonneg
have inl₁ : ∀ (i : ℕ)
  (h :
    im (d := (↑d : ℤ)) { re := (↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) } +
        im (d := (↑d : ℤ)) { re := (↑z : ℤ), im := -(↑w : ℤ) : ℤ√(↑d : ℤ) } =
      -(↑i : ℤ)),
  z ≤ x + z
Tactic: refine nonnegg_cases_right fun i h => sqLe_of_le ?_ ?_ (nonnegg_pos_neg.1 hb)
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
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
have inl : ∀ (i : ℕ)
  (h :
    re (d := (↑d : ℤ)) { re := (↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) } +
        re (d := (↑d : ℤ)) { re := -(↑z : ℤ), im := (↑w : ℤ) : ℤ√(↑d : ℤ) } =
      -(↑i : ℤ)),
  i ≤ z
Tactic: refine nonnegg_cases_left fun i h => sqLe_of_le ?_ ?_ (nonnegg_neg_pos.1 hb)
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
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
⊢ (HAdd.hAdd (α := ℤ√(↑d : ℤ)) { re := (↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) }
      { re := -(↑z : ℤ), im := (↑w : ℤ) : ℤ√(↑d : ℤ) }).Nonneg
have inl₁ : ∀ (i : ℕ)
  (h :
    re (d := (↑d : ℤ)) { re := (↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) } +
        re (d := (↑d : ℤ)) { re := -(↑z : ℤ), im := (↑w : ℤ) : ℤ√(↑d : ℤ) } =
      -(↑i : ℤ)),
  w ≤ y + w
Tactic: refine nonnegg_cases_left fun i h => sqLe_of_le ?_ ?_ (nonnegg_neg_pos.1 hb)
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
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
have inr : ∀ (i : ℕ)
  (h :
    im (d := (↑d : ℤ)) { re := (↑x : ℤ), im := -(↑y : ℤ) : ℤ√(↑d : ℤ) } +
        im (d := (↑d : ℤ)) { re := (↑z : ℤ), im := (↑w : ℤ) : ℤ√(↑d : ℤ) } =
      -(↑i : ℤ)),
  i ≤ y
Tactic: refine nonnegg_cases_right fun i h => sqLe_of_le ?_ ?_ (nonnegg_pos_neg.1 ha)
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
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
⊢ (HAdd.hAdd (α := ℤ√(↑d : ℤ)) { re := (↑x : ℤ), im := -(↑y : ℤ) : ℤ√(↑d : ℤ) }
      { re := (↑z : ℤ), im := (↑w : ℤ) : ℤ√(↑d : ℤ) }).Nonneg
have inr₁ : ∀ (i : ℕ)
  (h :
    im (d := (↑d : ℤ)) { re := (↑x : ℤ), im := -(↑y : ℤ) : ℤ√(↑d : ℤ) } +
        im (d := (↑d : ℤ)) { re := (↑z : ℤ), im := (↑w : ℤ) : ℤ√(↑d : ℤ) } =
      -(↑i : ℤ)),
  x ≤ x + z
Tactic: refine nonnegg_cases_right fun i h => sqLe_of_le ?_ ?_ (nonnegg_pos_neg.1 ha)
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (hypothesis)
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
have this : 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))
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (hypothesis)
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) : ℤ) }
⊢ (HAdd.hAdd (α := ℤ√(↑d : ℤ)) { re := (↑x : ℤ), im := -(↑y : ℤ) : ℤ√(↑d : ℤ) }
      { re := (↑z : ℤ), im := -(↑w : ℤ) : ℤ√(↑d : ℤ) }).Nonneg
have this₁ : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
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
have inr : ∀ (i : ℕ)
  (h :
    re (d := (↑d : ℤ)) { re := -(↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) } +
        re (d := (↑d : ℤ)) { re := (↑z : ℤ), im := (↑w : ℤ) : ℤ√(↑d : ℤ) } =
      -(↑i : ℤ)),
  i ≤ x
Tactic: refine nonnegg_cases_left fun i h => sqLe_of_le ?_ ?_ (nonnegg_neg_pos.1 ha)
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
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
⊢ (HAdd.hAdd (α := ℤ√(↑d : ℤ)) { re := -(↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) }
      { re := (↑z : ℤ), im := (↑w : ℤ) : ℤ√(↑d : ℤ) }).Nonneg
have inr₁ : ∀ (i : ℕ)
  (h :
    re (d := (↑d : ℤ)) { re := -(↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) } +
        re (d := (↑d : ℤ)) { re := (↑z : ℤ), im := (↑w : ℤ) : ℤ√(↑d : ℤ) } =
      -(↑i : ℤ)),
  y ≤ y + w
Tactic: refine nonnegg_cases_left fun i h => sqLe_of_le ?_ ?_ (nonnegg_neg_pos.1 ha)
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
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 (α := ℤ) (-(↑x : ℤ)) (↑z : ℤ), im := HAdd.hAdd (α := ℤ) (↑y : ℤ) (-(↑w : ℤ)) }
have inr : Nonneg (d := d) { re := HAdd.hAdd (α := ℤ) (↑z : ℤ) (-(↑x : ℤ)), im := HAdd.hAdd (α := ℤ) (-(↑w : ℤ)) (↑y : ℤ) }
Tactic: rw [add_comm, add_comm (y : ℤ)]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (hypothesis)
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
have this : Nonneg (d := d) { re := -(↑(x + z) : ℤ), im := (↑(y + w) : ℤ) }
Tactic: have : Nonneg ⟨_, _⟩ :=
      nonnegg_neg_pos.2 (sqLe_add (nonnegg_neg_pos.1 ha) (nonnegg_neg_pos.1 hb))
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (hypothesis)
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) : ℤ) }
⊢ (HAdd.hAdd (α := ℤ√(↑d : ℤ)) { re := -(↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) }
      { re := -(↑z : ℤ), im := (↑w : ℤ) : ℤ√(↑d : ℤ) }).Nonneg
have this₁ : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (hypothesis)
Goal:
d : ℕ
a b : ℤ√(↑d : ℤ)
⊢ a ≤ b ∨ b ≤ a
have t : (b - a).Nonneg ∨ (-(b - a)).Nonneg
Tactic: have t := (b - a).nonneg_total
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℕ
a b : ℤ√(↑d : ℤ)
t : (b - a).Nonneg ∨ (-(b - a)).Nonneg
⊢ a ≤ b ∨ b ≤ a
have rwa : ∀ (t : (b - a).Nonneg ∨ (a - b).Nonneg), a ≤ b ∨ b ≤ a
Tactic: rwa [neg_sub] at t
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℕ
a : ℤ√(↑d : ℤ)
⊢ (a - a).Nonneg
have simp : Nonneg (d := d) 0
Tactic: simp only [sub_self]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (hypothesis)
Goal:
d : ℕ
a b : ℤ√(↑d : ℤ)
⊢ b ≤ a ∨ a ≤ b
have t : (a - b).Nonneg ∨ (-(a - b)).Nonneg
Tactic: have t := (a - b).nonneg_total
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℕ
a b : ℤ√(↑d : ℤ)
t : (a - b).Nonneg ∨ (-(a - b)).Nonneg
⊢ b ≤ a ∨ a ≤ b
have rwa : ∀ (t : (a - b).Nonneg ∨ (b - a).Nonneg), b ≤ a ∨ a ≤ b
Tactic: rwa [neg_sub] at t
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (hypothesis)
Goal:
d : ℕ
a b : ℤ√(↑d : ℤ)
⊢ a < b ↔ a ≤ b ∧ ¬b ≤ a
have ht : b ≤ a ∨ a ≤ b
Tactic: have ht : b ≤ a ∨ a ≤ b := by
      have t := (a - b).nonneg_total
      rwa [neg_sub] at t
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℕ
a : ℤ√(↑d : ℤ)
⊢ ∃ (n : ℕ), a ≤ (↑n : ℤ√(↑d : ℤ))
have obtain : ∀ (x y : ℕ) (h : a ≤ { re := (↑x : ℤ), im := (↑y : ℤ) }), ∃ (n : ℕ), a ≤ (↑n : ℤ√(↑d : ℤ))
Tactic: obtain ⟨x, y, (h : a ≤ ⟨x, y⟩)⟩ : ∃ x y : ℕ, Nonneg (⟨x, y⟩ + -a) :=
    match -a with
    | ⟨Int.ofNat x, Int.ofNat y⟩ => ⟨0, 0, by trivial⟩
    | ⟨Int.ofNat x, -[y+1]⟩ => ⟨0, y + 1, by simp [Int.negSucc_eq, add_assoc, Nonneg, Nonnegg]⟩
    | ⟨-[x+1], Int.ofNat y⟩ => ⟨x + 1, 0, by simp [Int.negSucc_eq, add_assoc, Nonneg, Nonnegg]⟩
    | ⟨-[x+1], -[y+1]⟩ => ⟨x + 1, y + 1, by simp [Int.negSucc_eq, add_assoc, Nonneg, Nonnegg]⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℕ
a : ℤ√(↑d : ℤ)
x y : ℕ
h : a ≤ { re := (↑x : ℤ), im := (↑y : ℤ) }
⊢ ∃ (n : ℕ), a ≤ (↑n : ℤ√(↑d : ℤ))
have refine : LE.le (α := ℤ√(↑d : ℤ)) { re := (↑x : ℤ), im := (↑y : ℤ) } (↑(x + d * y) : ℤ√(↑d : ℤ))
Tactic: refine ⟨x + d * y, h.trans ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℕ
a : ℤ√(↑d : ℤ)
x y : ℕ
h : a ≤ { re := (↑x : ℤ), im := (↑y : ℤ) }
⊢ Nonneg (d := d)
    { re := (↑x : ℤ) + HMul.hMul (α := ℤ) (↑d : ℤ) (↑y : ℤ) - (↑x : ℤ), im := HSub.hSub (α := ℤ) 0 (↑y : ℤ) }
have zero : ∀ (h : a ≤ { re := (↑x : ℤ), im := (↑0 : ℤ) }),
  Nonneg (d := d)
    { re := (↑x : ℤ) + HMul.hMul (α := ℤ) (↑d : ℤ) (↑0 : ℤ) - (↑x : ℤ), im := HSub.hSub (α := ℤ) 0 (↑0 : ℤ) }
Tactic: rcases y with - | y
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℕ
a : ℤ√(↑d : ℤ)
x y : ℕ
h : a ≤ { re := (↑x : ℤ), im := (↑y : ℤ) }
zero :
  ∀ (h : a ≤ { re := (↑x : ℤ), im := (↑0 : ℤ) }),
    Nonneg (d := d)
      { re := (↑x : ℤ) + HMul.hMul (α := ℤ) (↑d : ℤ) (↑0 : ℤ) - (↑x : ℤ), im := HSub.hSub (α := ℤ) 0 (↑0 : ℤ) }
⊢ Nonneg (d := d)
    { re := (↑x : ℤ) + HMul.hMul (α := ℤ) (↑d : ℤ) (↑y : ℤ) - (↑x : ℤ), im := HSub.hSub (α := ℤ) 0 (↑y : ℤ) }
have succ : ∀ (y : ℕ) (h : a ≤ { re := (↑x : ℤ), im := (↑(y + 1) : ℤ) }),
  Nonneg (d := d)
    { re := (↑x : ℤ) + HMul.hMul (α := ℤ) (↑d : ℤ) (↑(y + 1) : ℤ) - (↑x : ℤ),
      im := HSub.hSub (α := ℤ) 0 (↑(y + 1) : ℤ) }
Tactic: rcases y with - | y
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℕ
a : ℤ√(↑d : ℤ)
x : ℕ
h : a ≤ { re := (↑x : ℤ), im := (↑0 : ℤ) }
⊢ Nonneg (d := d)
    { re := (↑x : ℤ) + HMul.hMul (α := ℤ) (↑d : ℤ) (↑0 : ℤ) - (↑x : ℤ), im := HSub.hSub (α := ℤ) 0 (↑0 : ℤ) }
have zero : Nonneg (d := d) { re := 0, im := 0 }
Tactic: simp only [Nat.cast_zero, mul_zero, add_zero, sub_self]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (hypothesis)
Goal:
d : ℕ
a : ℤ√(↑d : ℤ)
x y : ℕ
h : a ≤ { re := (↑x : ℤ), im := (↑(y + 1) : ℤ) }
⊢ Nonneg (d := d)
    { re := (↑x : ℤ) + HMul.hMul (α := ℤ) (↑d : ℤ) (↑(y + 1) : ℤ) - (↑x : ℤ),
      im := HSub.hSub (α := ℤ) 0 (↑(y + 1) : ℤ) }
have h₁ : ∀ (y : ℕ), SqLe y d (d * y) 1
Tactic: have h : ∀ y, SqLe y d (d * y) 1 := fun y => by
    simpa [SqLe, mul_comm, mul_left_comm] using Nat.mul_le_mul_right (y * y) (Nat.le_mul_self d)
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℕ
a : ℤ√(↑d : ℤ)
x y : ℕ
h_1 : a ≤ { re := (↑x : ℤ), im := (↑(y + 1) : ℤ) }
h : ∀ (y : ℕ), SqLe y d (d * y) 1
⊢ Nonneg (d := d)
    { re := (↑x : ℤ) + HMul.hMul (α := ℤ) (↑d : ℤ) (↑(y + 1) : ℤ) - (↑x : ℤ),
      im := HSub.hSub (α := ℤ) 0 (↑(y + 1) : ℤ) }
have succ : Nonneg (d := d) { re := HMul.hMul (α := ℤ) (↑d : ℤ) (↑y.succ : ℤ), im := HSub.hSub (α := ℤ) 0 (↑(y + 1) : ℤ) }
Tactic: rw [show (x : ℤ) + d * Nat.succ y - x = d * Nat.succ y by simp]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℕ
a b : ℤ√(↑d : ℤ)
ab : a ≤ b
c : ℤ√(↑d : ℤ)
⊢ (b + c - (a + c)).Nonneg
have rwa : (b - a).Nonneg
Tactic: rwa [add_sub_add_right_eq_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℕ
a : ℤ√(↑d : ℤ)
n : ℕ
ha : a.Nonneg
x y : ℕ
h : Nonneg (d := d) { re := (↑x : ℤ), im := (↑y : ℤ) }
⊢ (HMul.hMul (α := ℤ√(↑d : ℤ)) (↑(↑n : ℤ) : ℤ√(↑d : ℤ)) { re := (↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) }).Nonneg
have rw : Nonneg (d := d) { re := HMul.hMul (α := ℤ) (↑n : ℤ) (↑x : ℤ), im := HMul.hMul (α := ℤ) (↑n : ℤ) (↑y : ℤ) }
Tactic: rw [smul_val]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℕ
a : ℤ√(↑d : ℤ)
n : ℕ
ha_1 : a.Nonneg
x y : ℕ
ha : Nonneg (d := d) { re := (↑x : ℤ), im := -(↑y : ℤ) }
⊢ (HMul.hMul (α := ℤ√(↑d : ℤ)) (↑(↑n : ℤ) : ℤ√(↑d : ℤ)) { re := (↑x : ℤ), im := -(↑y : ℤ) : ℤ√(↑d : ℤ) }).Nonneg
have rw : Nonneg (d := d) { re := HMul.hMul (α := ℤ) (↑n : ℤ) (↑x : ℤ), im := HMul.hMul (α := ℤ) (↑n : ℤ) (-(↑y : ℤ)) }
Tactic: rw [smul_val]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℕ
a : ℤ√(↑d : ℤ)
n : ℕ
ha_1 : a.Nonneg
x y : ℕ
ha : Nonneg (d := d) { re := -(↑x : ℤ), im := (↑y : ℤ) }
⊢ (HMul.hMul (α := ℤ√(↑d : ℤ)) (↑(↑n : ℤ) : ℤ√(↑d : ℤ)) { re := -(↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) }).Nonneg
have rw : Nonneg (d := d) { re := HMul.hMul (α := ℤ) (↑n : ℤ) (-(↑x : ℤ)), im := HMul.hMul (α := ℤ) (↑n : ℤ) (↑y : ℤ) }
Tactic: rw [smul_val]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℕ
a : ℤ√(↑d : ℤ)
ha_1 : a.Nonneg
x y : ℕ
ha : Nonneg (d := d) { re := (↑x : ℤ), im := -(↑y : ℤ) }
⊢ (HMul.hMul (α := ℤ√(↑d : ℤ)) sqrtd { re := (↑x : ℤ), im := -(↑y : ℤ) : ℤ√(↑d : ℤ) }).Nonneg
have simp : Nonneg (d := d) { re := -HMul.hMul (α := ℤ) (↑d : ℤ) (↑y : ℤ), im := (↑x : ℤ) }
Tactic: simp only [muld_val, mul_neg]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℕ
a : ℤ√(↑d : ℤ)
ha_1 : a.Nonneg
x y : ℕ
ha : Nonneg (d := d) { re := (↑x : ℤ), im := -(↑y : ℤ) }
⊢ Nonneg (d := d) { re := -HMul.hMul (α := ℤ) (↑d : ℤ) (↑y : ℤ), im := (↑x : ℤ) }
have apply : SqLe (d * y) 1 x d
Tactic: apply nonnegg_neg_pos.2
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℕ
a : ℤ√(↑d : ℤ)
ha_1 : a.Nonneg
x y : ℕ
ha : Nonneg (d := d) { re := -(↑x : ℤ), im := (↑y : ℤ) }
⊢ (HMul.hMul (α := ℤ√(↑d : ℤ)) sqrtd { re := -(↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) }).Nonneg
have simp : Nonneg (d := d) { re := HMul.hMul (α := ℤ) (↑d : ℤ) (↑y : ℤ), im := -(↑x : ℤ) }
Tactic: simp only [muld_val]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℕ
a : ℤ√(↑d : ℤ)
ha_1 : a.Nonneg
x y : ℕ
ha : Nonneg (d := d) { re := -(↑x : ℤ), im := (↑y : ℤ) }
⊢ Nonneg (d := d) { re := HMul.hMul (α := ℤ) (↑d : ℤ) (↑y : ℤ), im := -(↑x : ℤ) }
have apply : SqLe x d (d * y) 1
Tactic: apply nonnegg_pos_neg.2
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d x y : ℕ
a : ℤ√(↑d : ℤ)
ha : a.Nonneg
⊢ { re := (↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) } * a = (↑x : ℤ√(↑d : ℤ)) * a + sqrtd * ((↑y : ℤ√(↑d : ℤ)) * a)
have rw : ((↑(↑x : ℤ) : ℤ√(↑d : ℤ)) + HMul.hMul (α := ℤ√(↑d : ℤ)) sqrtd (↑(↑y : ℤ) : ℤ√(↑d : ℤ))) * a =
  (↑x : ℤ√(↑d : ℤ)) * a + sqrtd * ((↑y : ℤ√(↑d : ℤ)) * a)
Tactic: rw [decompose, right_distrib, mul_assoc, Int.cast_natCast, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d x y : ℕ
a : ℤ√(↑d : ℤ)
ha : a.Nonneg
rw :
  ((↑(↑x : ℤ) : ℤ√(↑d : ℤ)) + HMul.hMul (α := ℤ√(↑d : ℤ)) sqrtd (↑(↑y : ℤ) : ℤ√(↑d : ℤ))) * a =
    (↑x : ℤ√(↑d : ℤ)) * a + sqrtd * ((↑y : ℤ√(↑d : ℤ)) * a)
⊢ { re := (↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) } * a = (↑x : ℤ√(↑d : ℤ)) * a + sqrtd * ((↑y : ℤ√(↑d : ℤ)) * a)
have rw₁ : (↑(↑x : ℤ) : ℤ√(↑d : ℤ)) * a + HMul.hMul (α := ℤ√(↑d : ℤ)) sqrtd (↑(↑y : ℤ) : ℤ√(↑d : ℤ)) * a =
  (↑x : ℤ√(↑d : ℤ)) * a + sqrtd * ((↑y : ℤ√(↑d : ℤ)) * a)
Tactic: rw [decompose, right_distrib, mul_assoc, Int.cast_natCast, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d x y : ℕ
a : ℤ√(↑d : ℤ)
ha : a.Nonneg
rw :
  ((↑(↑x : ℤ) : ℤ√(↑d : ℤ)) + HMul.hMul (α := ℤ√(↑d : ℤ)) sqrtd (↑(↑y : ℤ) : ℤ√(↑d : ℤ))) * a =
    (↑x : ℤ√(↑d : ℤ)) * a + sqrtd * ((↑y : ℤ√(↑d : ℤ)) * a)
rw₁ :
  (↑(↑x : ℤ) : ℤ√(↑d : ℤ)) * a + HMul.hMul (α := ℤ√(↑d : ℤ)) sqrtd (↑(↑y : ℤ) : ℤ√(↑d : ℤ)) * a =
    (↑x : ℤ√(↑d : ℤ)) * a + sqrtd * ((↑y : ℤ√(↑d : ℤ)) * a)
⊢ { re := (↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) } * a = (↑x : ℤ√(↑d : ℤ)) * a + sqrtd * ((↑y : ℤ√(↑d : ℤ)) * a)
have rw₂ : (↑(↑x : ℤ) : ℤ√(↑d : ℤ)) * a + sqrtd * ((↑(↑y : ℤ) : ℤ√(↑d : ℤ)) * a) =
  (↑x : ℤ√(↑d : ℤ)) * a + sqrtd * ((↑y : ℤ√(↑d : ℤ)) * a)
Tactic: rw [decompose, right_distrib, mul_assoc, Int.cast_natCast, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d x y : ℕ
a : ℤ√(↑d : ℤ)
ha : a.Nonneg
rw :
  ((↑(↑x : ℤ) : ℤ√(↑d : ℤ)) + HMul.hMul (α := ℤ√(↑d : ℤ)) sqrtd (↑(↑y : ℤ) : ℤ√(↑d : ℤ))) * a =
    (↑x : ℤ√(↑d : ℤ)) * a + sqrtd * ((↑y : ℤ√(↑d : ℤ)) * a)
rw₁ :
  (↑(↑x : ℤ) : ℤ√(↑d : ℤ)) * a + HMul.hMul (α := ℤ√(↑d : ℤ)) sqrtd (↑(↑y : ℤ) : ℤ√(↑d : ℤ)) * a =
    (↑x : ℤ√(↑d : ℤ)) * a + sqrtd * ((↑y : ℤ√(↑d : ℤ)) * a)
rw₂ :
  (↑(↑x : ℤ) : ℤ√(↑d : ℤ)) * a + sqrtd * ((↑(↑y : ℤ) : ℤ√(↑d : ℤ)) * a) =
    (↑x : ℤ√(↑d : ℤ)) * a + sqrtd * ((↑y : ℤ√(↑d : ℤ)) * a)
⊢ { re := (↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) } * a = (↑x : ℤ√(↑d : ℤ)) * a + sqrtd * ((↑y : ℤ√(↑d : ℤ)) * a)
have rw₃ : (↑x : ℤ√(↑d : ℤ)) * a + sqrtd * ((↑(↑y : ℤ) : ℤ√(↑d : ℤ)) * a) = (↑x : ℤ√(↑d : ℤ)) * a + sqrtd * ((↑y : ℤ√(↑d : ℤ)) * a)
Tactic: rw [decompose, right_distrib, mul_assoc, Int.cast_natCast, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d x y : ℕ
a : ℤ√(↑d : ℤ)
ha : a.Nonneg
rw :
  ((↑(↑x : ℤ) : ℤ√(↑d : ℤ)) + HMul.hMul (α := ℤ√(↑d : ℤ)) sqrtd (↑(↑y : ℤ) : ℤ√(↑d : ℤ))) * a =
    (↑x : ℤ√(↑d : ℤ)) * a + sqrtd * ((↑y : ℤ√(↑d : ℤ)) * a)
rw₁ :
  (↑(↑x : ℤ) : ℤ√(↑d : ℤ)) * a + HMul.hMul (α := ℤ√(↑d : ℤ)) sqrtd (↑(↑y : ℤ) : ℤ√(↑d : ℤ)) * a =
    (↑x : ℤ√(↑d : ℤ)) * a + sqrtd * ((↑y : ℤ√(↑d : ℤ)) * a)
rw₂ :
  (↑(↑x : ℤ) : ℤ√(↑d : ℤ)) * a + sqrtd * ((↑(↑y : ℤ) : ℤ√(↑d : ℤ)) * a) =
    (↑x : ℤ√(↑d : ℤ)) * a + sqrtd * ((↑y : ℤ√(↑d : ℤ)) * a)
rw₃ :
  (↑x : ℤ√(↑d : ℤ)) * a + sqrtd * ((↑(↑y : ℤ) : ℤ√(↑d : ℤ)) * a) =
    (↑x : ℤ√(↑d : ℤ)) * a + sqrtd * ((↑y : ℤ√(↑d : ℤ)) * a)
⊢ { re := (↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) } * a = (↑x : ℤ√(↑d : ℤ)) * a + sqrtd * ((↑y : ℤ√(↑d : ℤ)) * a)
have rw₄ : (↑x : ℤ√(↑d : ℤ)) * a + sqrtd * ((↑y : ℤ√(↑d : ℤ)) * a) = (↑x : ℤ√(↑d : ℤ)) * a + sqrtd * ((↑y : ℤ√(↑d : ℤ)) * a)
Tactic: rw [decompose, right_distrib, mul_assoc, Int.cast_natCast, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (hypothesis)
Goal:
d x y : ℕ
a : ℤ√(↑d : ℤ)
ha : a.Nonneg
⊢ ({ re := (↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) } * a).Nonneg
have this : { re := (↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) } * a = (↑x : ℤ√(↑d : ℤ)) * a + sqrtd * ((↑y : ℤ√(↑d : ℤ)) * a)
Tactic: have : (⟨x, y⟩ * a : ℤ√d) = (x : ℤ√d) * a + sqrtd * ((y : ℤ√d) * a) := by
    rw [decompose, right_distrib, mul_assoc, Int.cast_natCast, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d x y : ℕ
a : ℤ√(↑d : ℤ)
ha : a.Nonneg
this : { re := (↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) } * a = (↑x : ℤ√(↑d : ℤ)) * a + sqrtd * ((↑y : ℤ√(↑d : ℤ)) * a)
⊢ ({ re := (↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) } * a).Nonneg
have rw : ((↑x : ℤ√(↑d : ℤ)) * a + sqrtd * ((↑y : ℤ√(↑d : ℤ)) * a)).Nonneg
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℕ
a b : ℤ√(↑d : ℤ)
ha_1 : a.Nonneg
hb : b.Nonneg
x y z w : ℕ
ha : Nonneg (d := d) { re := -(↑x : ℤ), im := (↑y : ℤ) }
h : Nonneg (d := d) { re := (↑z : ℤ), im := (↑w : ℤ) }
⊢ (HMul.hMul (α := ℤ√(↑d : ℤ)) { re := -(↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) }
      { re := (↑z : ℤ), im := (↑w : ℤ) : ℤ√(↑d : ℤ) }).Nonneg
have rw : (HMul.hMul (α := ℤ√(↑d : ℤ)) { re := (↑z : ℤ), im := (↑w : ℤ) : ℤ√(↑d : ℤ) }
    { re := -(↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) }).Nonneg
Tactic: rw [mul_comm]