awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
x : ℤ√d
h : x.norm.natAbs = 1
hx : 0 ≤ x.norm
rwa : ∀ (h : Eq (α := ℤ) (↑x.norm.natAbs : ℤ) (↑1 : ℤ)) (hx : 0 ≤ x.norm), 1 = x * star x
⊢ 1 = x * star x
have rwa₁ : ∀ (h : x.norm = (↑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
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
x : ℤ√d
h : x.norm.natAbs = 1
hx : 0 ≤ x.norm
rwa : ∀ (h : Eq (α := ℤ) (↑x.norm.natAbs : ℤ) (↑1 : ℤ)) (hx : 0 ≤ x.norm), 1 = x * star x
rwa₁ : ∀ (h : x.norm = (↑1 : ℤ)) (hx : 0 ≤ x.norm), 1 = x * star x
⊢ 1 = x * star x
have rwa₂ : ∀ (h : Eq (α := ℤ√d) (↑x.norm : ℤ√d) (↑(↑1 : ℤ) : ℤ√d)) (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
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
x : ℤ√d
h : x.norm.natAbs = 1
hx : 0 ≤ x.norm
rwa : ∀ (h : Eq (α := ℤ) (↑x.norm.natAbs : ℤ) (↑1 : ℤ)) (hx : 0 ≤ x.norm), 1 = x * star x
rwa₁ : ∀ (h : x.norm = (↑1 : ℤ)) (hx : 0 ≤ x.norm), 1 = x * star x
rwa₂ : ∀ (h : Eq (α := ℤ√d) (↑x.norm : ℤ√d) (↑(↑1 : ℤ) : ℤ√d)) (hx : 0 ≤ x.norm), 1 = x * star x
⊢ 1 = x * star x
have rwa₃ : ∀ (h : x * star x = (↑(↑1 : ℤ) : ℤ√d)) (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
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
x : ℤ√d
h : x.norm.natAbs = 1
hx : 0 ≤ x.norm
rwa : ∀ (h : Eq (α := ℤ) (↑x.norm.natAbs : ℤ) (↑1 : ℤ)) (hx : 0 ≤ x.norm), 1 = x * star x
rwa₁ : ∀ (h : x.norm = (↑1 : ℤ)) (hx : 0 ≤ x.norm), 1 = x * star x
rwa₂ : ∀ (h : Eq (α := ℤ√d) (↑x.norm : ℤ√d) (↑(↑1 : ℤ) : ℤ√d)) (hx : 0 ≤ x.norm), 1 = x * star x
rwa₃ : ∀ (h : x * star x = (↑(↑1 : ℤ) : ℤ√d)) (hx : 0 ≤ x.norm), 1 = x * star x
⊢ 1 = x * star x
have rwa₄ : ∀ (h : (↑(↑1 : ℤ) : ℤ√d) = x * star x) (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
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
x : ℤ√d
h : x.norm.natAbs = 1
hx : x.norm ≤ 0
⊢ 1 = x * -star x
have rwa : ∀ (h : Eq (α := ℤ) (↑x.norm.natAbs : ℤ) (↑1 : ℤ)) (hx : x.norm ≤ 0), 1 = x * -star x
Tactic: rwa [← Int.natCast_inj, Int.ofNat_natAbs_of_nonpos hx, ← @Int.cast_inj (ℤ√d) _ _,
              Int.cast_neg, norm_eq_mul_conj, neg_mul_eq_mul_neg, eq_comm] at h
Cleared hypotheses: h, hx
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
x : ℤ√d
h : x.norm.natAbs = 1
hx : x.norm ≤ 0
rwa : ∀ (h : Eq (α := ℤ) (↑x.norm.natAbs : ℤ) (↑1 : ℤ)) (hx : x.norm ≤ 0), 1 = x * -star x
⊢ 1 = x * -star x
have rwa₁ : ∀ (h : -x.norm = (↑1 : ℤ)) (hx : x.norm ≤ 0), 1 = x * -star x
Tactic: rwa [← Int.natCast_inj, Int.ofNat_natAbs_of_nonpos hx, ← @Int.cast_inj (ℤ√d) _ _,
              Int.cast_neg, norm_eq_mul_conj, neg_mul_eq_mul_neg, eq_comm] at h
Cleared hypotheses: h, hx
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
x : ℤ√d
h : x.norm.natAbs = 1
hx : x.norm ≤ 0
rwa : ∀ (h : Eq (α := ℤ) (↑x.norm.natAbs : ℤ) (↑1 : ℤ)) (hx : x.norm ≤ 0), 1 = x * -star x
rwa₁ : ∀ (h : -x.norm = (↑1 : ℤ)) (hx : x.norm ≤ 0), 1 = x * -star x
⊢ 1 = x * -star x
have rwa₂ : ∀ (h : Eq (α := ℤ√d) (↑(-x.norm) : ℤ√d) (↑(↑1 : ℤ) : ℤ√d)) (hx : x.norm ≤ 0), 1 = x * -star x
Tactic: rwa [← Int.natCast_inj, Int.ofNat_natAbs_of_nonpos hx, ← @Int.cast_inj (ℤ√d) _ _,
              Int.cast_neg, norm_eq_mul_conj, neg_mul_eq_mul_neg, eq_comm] at h
Cleared hypotheses: h, hx
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
x : ℤ√d
h : x.norm.natAbs = 1
hx : x.norm ≤ 0
rwa : ∀ (h : Eq (α := ℤ) (↑x.norm.natAbs : ℤ) (↑1 : ℤ)) (hx : x.norm ≤ 0), 1 = x * -star x
rwa₁ : ∀ (h : -x.norm = (↑1 : ℤ)) (hx : x.norm ≤ 0), 1 = x * -star x
rwa₂ : ∀ (h : Eq (α := ℤ√d) (↑(-x.norm) : ℤ√d) (↑(↑1 : ℤ) : ℤ√d)) (hx : x.norm ≤ 0), 1 = x * -star x
⊢ 1 = x * -star x
have rwa₃ : ∀ (h : Eq (α := ℤ√d) (-(↑x.norm : ℤ√d)) (↑(↑1 : ℤ) : ℤ√d)) (hx : x.norm ≤ 0), 1 = x * -star x
Tactic: rwa [← Int.natCast_inj, Int.ofNat_natAbs_of_nonpos hx, ← @Int.cast_inj (ℤ√d) _ _,
              Int.cast_neg, norm_eq_mul_conj, neg_mul_eq_mul_neg, eq_comm] at h
Cleared hypotheses: h, hx
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
x : ℤ√d
h : x.norm.natAbs = 1
hx : x.norm ≤ 0
rwa : ∀ (h : Eq (α := ℤ) (↑x.norm.natAbs : ℤ) (↑1 : ℤ)) (hx : x.norm ≤ 0), 1 = x * -star x
rwa₁ : ∀ (h : -x.norm = (↑1 : ℤ)) (hx : x.norm ≤ 0), 1 = x * -star x
rwa₂ : ∀ (h : Eq (α := ℤ√d) (↑(-x.norm) : ℤ√d) (↑(↑1 : ℤ) : ℤ√d)) (hx : x.norm ≤ 0), 1 = x * -star x
rwa₃ : ∀ (h : Eq (α := ℤ√d) (-(↑x.norm : ℤ√d)) (↑(↑1 : ℤ) : ℤ√d)) (hx : x.norm ≤ 0), 1 = x * -star x
⊢ 1 = x * -star x
have rwa₄ : ∀ (h : -(x * star x) = (↑(↑1 : ℤ) : ℤ√d)) (hx : x.norm ≤ 0), 1 = x * -star x
Tactic: rwa [← Int.natCast_inj, Int.ofNat_natAbs_of_nonpos hx, ← @Int.cast_inj (ℤ√d) _ _,
              Int.cast_neg, norm_eq_mul_conj, neg_mul_eq_mul_neg, eq_comm] at h
Cleared hypotheses: h, hx
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
x : ℤ√d
h : x.norm.natAbs = 1
hx : x.norm ≤ 0
rwa : ∀ (h : Eq (α := ℤ) (↑x.norm.natAbs : ℤ) (↑1 : ℤ)) (hx : x.norm ≤ 0), 1 = x * -star x
rwa₁ : ∀ (h : -x.norm = (↑1 : ℤ)) (hx : x.norm ≤ 0), 1 = x * -star x
rwa₂ : ∀ (h : Eq (α := ℤ√d) (↑(-x.norm) : ℤ√d) (↑(↑1 : ℤ) : ℤ√d)) (hx : x.norm ≤ 0), 1 = x * -star x
rwa₃ : ∀ (h : Eq (α := ℤ√d) (-(↑x.norm : ℤ√d)) (↑(↑1 : ℤ) : ℤ√d)) (hx : x.norm ≤ 0), 1 = x * -star x
rwa₄ : ∀ (h : -(x * star x) = (↑(↑1 : ℤ) : ℤ√d)) (hx : x.norm ≤ 0), 1 = x * -star x
⊢ 1 = x * -star x
have rwa₅ : ∀ (h : x * -star x = (↑(↑1 : ℤ) : ℤ√d)) (hx : x.norm ≤ 0), 1 = x * -star x
Tactic: rwa [← Int.natCast_inj, Int.ofNat_natAbs_of_nonpos hx, ← @Int.cast_inj (ℤ√d) _ _,
              Int.cast_neg, norm_eq_mul_conj, neg_mul_eq_mul_neg, eq_comm] at h
Cleared hypotheses: h, hx
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
x : ℤ√d
h : x.norm.natAbs = 1
hx : x.norm ≤ 0
rwa : ∀ (h : Eq (α := ℤ) (↑x.norm.natAbs : ℤ) (↑1 : ℤ)) (hx : x.norm ≤ 0), 1 = x * -star x
rwa₁ : ∀ (h : -x.norm = (↑1 : ℤ)) (hx : x.norm ≤ 0), 1 = x * -star x
rwa₂ : ∀ (h : Eq (α := ℤ√d) (↑(-x.norm) : ℤ√d) (↑(↑1 : ℤ) : ℤ√d)) (hx : x.norm ≤ 0), 1 = x * -star x
rwa₃ : ∀ (h : Eq (α := ℤ√d) (-(↑x.norm : ℤ√d)) (↑(↑1 : ℤ) : ℤ√d)) (hx : x.norm ≤ 0), 1 = x * -star x
rwa₄ : ∀ (h : -(x * star x) = (↑(↑1 : ℤ) : ℤ√d)) (hx : x.norm ≤ 0), 1 = x * -star x
rwa₅ : ∀ (h : x * -star x = (↑(↑1 : ℤ) : ℤ√d)) (hx : x.norm ≤ 0), 1 = x * -star x
⊢ 1 = x * -star x
have rwa₆ : ∀ (h : (↑(↑1 : ℤ) : ℤ√d) = x * -star x) (hx : x.norm ≤ 0), 1 = x * -star x
Tactic: rwa [← Int.natCast_inj, Int.ofNat_natAbs_of_nonpos hx, ← @Int.cast_inj (ℤ√d) _ _,
              Int.cast_neg, norm_eq_mul_conj, neg_mul_eq_mul_neg, eq_comm] at h
Cleared hypotheses: h, hx
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
x : ℤ√d
h : IsUnit x
⊢ x.norm.natAbs = 1
have let : ∀ (y : ℤ√d) (hy : 1 = x * y), x.norm.natAbs = 1
Tactic: let ⟨y, hy⟩ := isUnit_iff_dvd_one.1 h
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (hypothesis)
Goal:
d : ℤ
x : ℤ√d
h : IsUnit x
y : ℤ√d
hy : 1 = x * y
⊢ x.norm.natAbs = 1
have this : Function.comp (α := ℤ√d) Int.natAbs norm 1 = (Int.natAbs ∘ norm) (x * y)
Tactic: have := congr_arg (Int.natAbs ∘ norm) hy
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (hypothesis)
Goal:
d : ℤ
x : ℤ√d
h : IsUnit x
y : ℤ√d
hy : 1 = x * y
this : Function.comp (α := ℤ√d) Int.natAbs norm 1 = (Int.natAbs ∘ norm) (x * y)
⊢ x.norm.natAbs = 1
have this₁ : x.norm.natAbs = 1 ∧ y.norm.natAbs = 1
Tactic: rw [Function.comp_apply, Function.comp_apply, norm_mul, Int.natAbs_mul, norm_one,
      Int.natAbs_one, eq_comm, mul_eq_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
z : ℤ√d
⊢ IsUnit z ↔ IsUnit z.norm
have rw : IsUnit z ↔ z.norm.natAbs = 1
Tactic: rw [Int.isUnit_iff_natAbs_eq, norm_eq_one_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
z : ℤ√d
rw : IsUnit z ↔ z.norm.natAbs = 1
⊢ IsUnit z ↔ IsUnit z.norm
have rw₁ : IsUnit z ↔ IsUnit z
Tactic: rw [Int.isUnit_iff_natAbs_eq, norm_eq_one_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
hd : d ≤ 0
z : ℤ√d
⊢ z.norm = 1 ↔ IsUnit z
have rw : z.norm = 1 ↔ z.norm.natAbs = 1
Tactic: rw [← norm_eq_one_iff, ← Int.natCast_inj, Int.natAbs_of_nonneg (norm_nonneg hd z), Int.ofNat_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
hd : d ≤ 0
z : ℤ√d
rw : z.norm = 1 ↔ z.norm.natAbs = 1
⊢ z.norm = 1 ↔ IsUnit z
have rw₁ : z.norm = 1 ↔ Eq (α := ℤ) (↑z.norm.natAbs : ℤ) (↑1 : ℤ)
Tactic: rw [← norm_eq_one_iff, ← Int.natCast_inj, Int.natAbs_of_nonneg (norm_nonneg hd z), Int.ofNat_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
hd : d ≤ 0
z : ℤ√d
rw : z.norm = 1 ↔ z.norm.natAbs = 1
rw₁ : z.norm = 1 ↔ Eq (α := ℤ) (↑z.norm.natAbs : ℤ) (↑1 : ℤ)
⊢ z.norm = 1 ↔ IsUnit z
have rw₂ : z.norm = 1 ↔ z.norm = (↑1 : ℤ)
Tactic: rw [← norm_eq_one_iff, ← Int.natCast_inj, Int.natAbs_of_nonneg (norm_nonneg hd z), Int.ofNat_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
hd : d ≤ 0
z : ℤ√d
rw : z.norm = 1 ↔ z.norm.natAbs = 1
rw₁ : z.norm = 1 ↔ Eq (α := ℤ) (↑z.norm.natAbs : ℤ) (↑1 : ℤ)
rw₂ : z.norm = 1 ↔ z.norm = (↑1 : ℤ)
⊢ z.norm = 1 ↔ IsUnit z
have rw₃ : z.norm = 1 ↔ z.norm = 1
Tactic: rw [← norm_eq_one_iff, ← Int.natCast_inj, Int.natAbs_of_nonneg (norm_nonneg hd z), Int.ofNat_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
hd : d < 0
z : ℤ√d
⊢ z.norm = 0 ↔ z = 0
have mp : z.norm = 0 → z = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
hd : d < 0
z : ℤ√d
mp : z.norm = 0 → z = 0
⊢ z.norm = 0 ↔ z = 0
have mpr : z = 0 → z.norm = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (hypothesis)
Goal:
d : ℤ
hd : d < 0
z : ℤ√d
h : z.norm = 0
⊢ z = 0
have h₁ : z.re * z.re + -(d * (z.im * z.im)) = 0
Tactic: rw [norm_def, sub_eq_add_neg, mul_assoc] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (hypothesis)
Goal:
d : ℤ
hd : d < 0
z : ℤ√d
h : z.re * z.re + -(d * (z.im * z.im)) = 0
⊢ z = 0
have left : 0 ≤ z.re * z.re
Tactic: have left := mul_self_nonneg z.re
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (hypothesis)
Goal:
d : ℤ
hd : d < 0
z : ℤ√d
h : z.re * z.re + -(d * (z.im * z.im)) = 0
left : 0 ≤ z.re * z.re
⊢ z = 0
have right : 0 ≤ -(d * (z.im * z.im))
Tactic: have right := neg_nonneg.mpr (mul_nonpos_of_nonpos_of_nonneg hd.le (mul_self_nonneg z.im))
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (hypothesis)
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))
⊢ z = 0
have ha : z.re * z.re = 0
Tactic: obtain ⟨ha, hb⟩ := (add_eq_zero_iff_of_nonneg left right).mp h
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (hypothesis)
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
⊢ z = 0
have hb : -(d * (z.im * z.im)) = 0
Tactic: obtain ⟨ha, hb⟩ := (add_eq_zero_iff_of_nonneg left right).mp h
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
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 = 0
have mp : z.re = re (d := d) 0
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
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
⊢ z = 0
have mp₁ : z.im = im (d := d) 0
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
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.im = im (d := d) 0
have mp : z.im * z.im = 0
Tactic: apply eq_zero_of_mul_self_eq_zero
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (hypothesis)
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.im * z.im = 0
have hb₁ : d = 0 ∨ z.im * z.im = 0
Tactic: rw [neg_eq_zero, mul_eq_zero] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
hd : d ≤ 0
x y : ℤ√d
h : Associated x y
⊢ x.norm = y.norm
have obtain : ∀ (u : (ℤ√d)ˣ), x.norm = (x * (↑u : ℤ√d)).norm
Tactic: obtain ⟨u, rfl⟩ := h
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
hd : d ≤ 0
x : ℤ√d
u : (ℤ√d)ˣ
⊢ x.norm = (x * (↑u : ℤ√d)).norm
have rw : x.norm = x.norm * (↑u : ℤ√d).norm
Tactic: rw [norm_mul, (norm_eq_one_iff' hd _).mpr u.isUnit, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
hd : d ≤ 0
x : ℤ√d
u : (ℤ√d)ˣ
rw : x.norm = x.norm * (↑u : ℤ√d).norm
⊢ x.norm = (x * (↑u : ℤ√d)).norm
have rw₁ : x.norm = x.norm * 1
Tactic: rw [norm_mul, (norm_eq_one_iff' hd _).mpr u.isUnit, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
hd : d ≤ 0
x : ℤ√d
u : (ℤ√d)ˣ
rw : x.norm = x.norm * (↑u : ℤ√d).norm
rw₁ : x.norm = x.norm * 1
⊢ x.norm = (x * (↑u : ℤ√d)).norm
have rw₂ : x.norm = x.norm
Tactic: rw [norm_mul, (norm_eq_one_iff' hd _).mpr u.isUnit, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (hypothesis)
Goal:
d x y z w : ℕ
xy : Nonneg (d := d) { re := (↑x : ℤ), im := -(↑y : ℤ) }
zw : 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 := 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)
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
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 }
⊢ (HAdd.hAdd (α := ℤ√(↑d : ℤ)) { re := (↑x : ℤ), im := -(↑y : ℤ) : ℤ√(↑d : ℤ) }
      { re := -(↑z : ℤ), im := (↑w : ℤ) : ℤ√(↑d : ℤ) }).Nonneg
have rw : Nonneg (d := d) { re := HAdd.hAdd (α := ℤ) (↑x : ℤ) (-(↑z : ℤ)), im := HSub.hSub (α := ℤ) (↑w : ℤ) (↑y : ℤ) }
Tactic: rw [add_def, neg_add_eq_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
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 }
⊢ Nonneg (d := d) { re := HAdd.hAdd (α := ℤ) (↑x : ℤ) (-(↑z : ℤ)), im := HSub.hSub (α := ℤ) (↑w : ℤ) (↑y : ℤ) }
have 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 : ℤ) }
Tactic: rwa [Int.subNatNat_eq_coe, Int.subNatNat_eq_coe] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
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 : ℤ) }
⊢ Nonneg (d := d) { re := HAdd.hAdd (α := ℤ) (↑x : ℤ) (-(↑z : ℤ)), im := HSub.hSub (α := ℤ) (↑w : ℤ) (↑y : ℤ) }
have 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 : ℤ) }
Tactic: rwa [Int.subNatNat_eq_coe, Int.subNatNat_eq_coe] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℕ
a b : ℤ√(↑d : ℤ)
ha : a.Nonneg
hb : b.Nonneg
⊢ (a + b).Nonneg
have inl : ∀ (x y : ℕ) (ha : Nonneg (d := d) { re := (↑x : ℤ), im := (↑y : ℤ) }),
  ({ re := (↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) } + b).Nonneg
Tactic: rcases nonneg_cases ha with ⟨x, y, rfl | rfl | rfl⟩
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
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
⊢ (a + b).Nonneg
have inr : ∀ (x y : ℕ) (ha : Nonneg (d := d) { re := (↑x : ℤ), im := -(↑y : ℤ) }),
  ({ re := (↑x : ℤ), im := -(↑y : ℤ) : ℤ√(↑d : ℤ) } + b).Nonneg
Tactic: rcases nonneg_cases ha with ⟨x, y, rfl | rfl | rfl⟩
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
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
⊢ (a + b).Nonneg
have inr₁ : ∀ (x y : ℕ) (ha : Nonneg (d := d) { re := -(↑x : ℤ), im := (↑y : ℤ) }),
  ({ re := -(↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) } + b).Nonneg
Tactic: rcases nonneg_cases ha with ⟨x, y, rfl | rfl | rfl⟩
Cleared hypotheses: a, ha
-- 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 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
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 : ℤ) }
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
have 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
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 : ℤ) }
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
have 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
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 : ℤ) }
⊢ ({ 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