awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℕ
a b : ℤ√(↑d : ℤ)
ha_1 : a.Nonneg
hb_1 : b.Nonneg
x y z w : ℕ
ha : Nonneg (d := d) { re := -(↑x : ℤ), im := (↑y : ℤ) }
hb : Nonneg (d := d) { re := -(↑z : ℤ), im := (↑w : ℤ) }
⊢ (HMul.hMul (α := ℤ√(↑d : ℤ)) { re := -(↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) }
      { re := -(↑z : ℤ), im := (↑w : ℤ) : ℤ√(↑d : ℤ) }).Nonneg
have rw : Nonneg (d := d)
  { re := HMul.hMul (α := ℤ) (↑x : ℤ) (↑z : ℤ) + HMul.hMul (α := ℤ) (↑d : ℤ) (↑y : ℤ) * (↑w : ℤ),
    im := -(HMul.hMul (α := ℤ) (↑x : ℤ) (↑w : ℤ) + HMul.hMul (α := ℤ) (↑y : ℤ) (↑z : ℤ)) }
Tactic: rw [calc
          (⟨-x, y⟩ * ⟨-z, w⟩ : ℤ√d) = ⟨_, _⟩ := rfl
          _ = ⟨x * z + d * y * w, -(x * w + y * z)⟩ := by simp [add_comm]]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℕ
a b : ℤ√(↑d : ℤ)
ha_1 : a.Nonneg
hb_1 : b.Nonneg
x y z w : ℕ
ha : Nonneg (d := d) { re := -(↑x : ℤ), im := (↑y : ℤ) }
hb : Nonneg (d := d) { re := (↑z : ℤ), im := -(↑w : ℤ) }
⊢ (HMul.hMul (α := ℤ√(↑d : ℤ)) { re := -(↑x : ℤ), im := (↑y : ℤ) : ℤ√(↑d : ℤ) }
      { re := (↑z : ℤ), im := -(↑w : ℤ) : ℤ√(↑d : ℤ) }).Nonneg
have rw : Nonneg (d := d)
  { re := -(HMul.hMul (α := ℤ) (↑x : ℤ) (↑z : ℤ) + HMul.hMul (α := ℤ) (↑d : ℤ) (↑y : ℤ) * (↑w : ℤ)),
    im := HMul.hMul (α := ℤ) (↑x : ℤ) (↑w : ℤ) + HMul.hMul (α := ℤ) (↑y : ℤ) (↑z : ℤ) }
Tactic: rw [calc
          (⟨-x, y⟩ * ⟨z, -w⟩ : ℤ√d) = ⟨_, _⟩ := rfl
          _ = ⟨-(x * z + d * y * w), x * w + y * z⟩ := by simp [add_comm]]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℕ
a b : ℤ√(↑d : ℤ)
ha_1 : a.Nonneg
hb_1 : b.Nonneg
x y z w : ℕ
ha : Nonneg (d := d) { re := (↑x : ℤ), im := -(↑y : ℤ) }
hb : Nonneg (d := d) { re := -(↑z : ℤ), im := (↑w : ℤ) }
⊢ (HMul.hMul (α := ℤ√(↑d : ℤ)) { re := (↑x : ℤ), im := -(↑y : ℤ) : ℤ√(↑d : ℤ) }
      { re := -(↑z : ℤ), im := (↑w : ℤ) : ℤ√(↑d : ℤ) }).Nonneg
have rw : Nonneg (d := d)
  { re := -(HMul.hMul (α := ℤ) (↑x : ℤ) (↑z : ℤ) + HMul.hMul (α := ℤ) (↑d : ℤ) (↑y : ℤ) * (↑w : ℤ)),
    im := HMul.hMul (α := ℤ) (↑x : ℤ) (↑w : ℤ) + HMul.hMul (α := ℤ) (↑y : ℤ) (↑z : ℤ) }
Tactic: rw [calc
          (⟨x, -y⟩ * ⟨-z, w⟩ : ℤ√d) = ⟨_, _⟩ := rfl
          _ = ⟨-(x * z + d * y * w), x * w + y * z⟩ := by simp [add_comm]]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℕ
a b : ℤ√(↑d : ℤ)
ha_1 : a.Nonneg
hb_1 : b.Nonneg
x y z w : ℕ
ha : Nonneg (d := d) { re := (↑x : ℤ), im := -(↑y : ℤ) }
hb : Nonneg (d := d) { re := (↑z : ℤ), im := -(↑w : ℤ) }
⊢ (HMul.hMul (α := ℤ√(↑d : ℤ)) { re := (↑x : ℤ), im := -(↑y : ℤ) : ℤ√(↑d : ℤ) }
      { re := (↑z : ℤ), im := -(↑w : ℤ) : ℤ√(↑d : ℤ) }).Nonneg
have rw : Nonneg (d := d)
  { re := HMul.hMul (α := ℤ) (↑x : ℤ) (↑z : ℤ) + HMul.hMul (α := ℤ) (↑d : ℤ) (↑y : ℤ) * (↑w : ℤ),
    im := -(HMul.hMul (α := ℤ) (↑x : ℤ) (↑w : ℤ) + HMul.hMul (α := ℤ) (↑y : ℤ) (↑z : ℤ)) }
Tactic: rw [calc
          (⟨x, -y⟩ * ⟨z, -w⟩ : ℤ√d) = ⟨_, _⟩ := rfl
          _ = ⟨x * z + d * y * w, -(x * w + y * z)⟩ := by simp [add_comm]]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℕ
a b : ℤ√(↑d : ℤ)
⊢ 0 ≤ a → 0 ≤ b → 0 ≤ a * b
have simp_rw : a.Nonneg → b.Nonneg → (a * b).Nonneg
Tactic: simp_rw [← nonneg_iff_zero_le]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
h : x * x = d * y * y
g : ℕ := x.gcd y
gpos : g > 0
⊢ False
have let : ∀ (m n : ℕ) (co : m.Coprime n) (hx : x = m * g) (hy : y = n * g), False
Tactic: let ⟨m, n, co, (hx : x = m * g), (hy : y = n * g)⟩ := Nat.exists_coprime _ _
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
h : x * x = d * y * y
g : ℕ := x.gcd y
gpos : g > 0
m n : ℕ
co : m.Coprime n
hx : x = m * g
hy : y = n * g
⊢ False
have rw : ∀ (n : ℕ) (h : m * g * (m * g) = d * (n * g) * (n * g)) (co : m.Coprime n) (hx : x = m * g) (hy : y = n * g), False
Tactic: rw [hx, hy] at h
Cleared hypotheses: h, n, co, hx, hy
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
g : ℕ := x.gcd y
gpos : g > 0
m n : ℕ
h : m * g * (m * g) = d * (n * g) * (n * g)
co : m.Coprime n
hx : x = m * g
hy : y = n * g
⊢ m * m = d * (n * n)
have refine : g * g * (m * m) = g * g * (d * (n * n))
Tactic: refine mul_left_cancel₀ (mul_pos gpos gpos).ne' ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (hypothesis)
Goal:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
g : ℕ := x.gcd y
gpos : g > 0
m n : ℕ
h : m * g * (m * g) = d * (n * g) * (n * g)
co : m.Coprime n
hx : x = m * g
hy : y = n * g
⊢ False
have this : m * m = d * (n * n)
Tactic: have : m * m = d * (n * n) := by
        refine mul_left_cancel₀ (mul_pos gpos gpos).ne' ?_
        simpa [mul_comm, mul_left_comm, mul_assoc] using h
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (hypothesis)
Goal:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
g : ℕ := x.gcd y
gpos : g > 0
m n : ℕ
h : m * g * (m * g) = d * (n * g) * (n * g)
co : m.Coprime n
hx : x = m * g
hy : y = n * g
this : m * m = d * (n * n)
⊢ False
have co2 : (m * m).Coprime (n * n)
Tactic: have co2 :=
        let co1 := co.mul_right co
        co1.mul_left co1
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
g : ℕ := x.gcd y
gpos : g > 0
m n : ℕ
h : m * g * (m * g) = d * (n * g) * (n * g)
co : m.Coprime n
hx : x = m * g
hy : y = n * g
this : m * m = d * (n * n)
co2 : (m * m).Coprime (n * n)
⊢ d ∣ m * m
have rw : d ∣ d * (n * n)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (hypothesis)
Goal:
d : ℕ
dnsq : Nonsquare d
x y : ℤ
h : x * x = (↑d : ℤ) * y * y
⊢ x = 0 ∧ y = 0
have h₁ : Eq (α := ℤ) (↑(x.natAbs * x.natAbs) : ℤ) (↑(d * y.natAbs * y.natAbs) : ℤ)
Tactic: rw [mul_assoc, ← Int.natAbs_mul_self, ← Int.natAbs_mul_self, ← Int.natCast_mul, ← mul_assoc] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (hypothesis)
Goal:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
e : (x + 1) * (x + 1) = d * (y + 1) * (y + 1)
⊢ False
have t : x + 1 = 0
Tactic: have t := (divides_sq_eq_zero e).left
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (hypothesis)
Goal:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
xy : SqLe (y + 1) d (x + 1) 1
yx : SqLe (x + 1) 1 y.succ d
t : 1 * (x + 1) * (x + 1) = d * y.succ * y.succ := ⋯
⊢ Eq (α := ℤ√(↑d : ℤ)) { re := (↑(x + 1) : ℤ), im := -[y+1] } 0
have t₁ : (x + 1) * (x + 1) = d * y.succ * y.succ
Tactic: rw [one_mul] at t
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (hypothesis)
Goal:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
xy : SqLe (x + 1) 1 (y + 1) d
yx : SqLe (y + 1) d x.succ 1
t : 1 * (x + 1) * (x + 1) = d * (y + 1) * (y + 1) := ⋯
⊢ Eq (α := ℤ√(↑d : ℤ)) { re := -[x+1], im := (↑(y + 1) : ℤ) } 0
have t₁ : (x + 1) * (x + 1) = d * (y + 1) * (y + 1)
Tactic: rw [one_mul] at t
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℕ
dnsq : Nonsquare d
a b : ℤ√(↑d : ℤ)
ab : a ≤ b
ba : b ≤ a
⊢ (-(a - b)).Nonneg
have rwa : (b - a).Nonneg
Tactic: rwa [neg_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℕ
dnsq : Nonsquare d
x x_1 : ℤ√(↑d : ℤ)
ab : x ≤ x_1
ba : x_1 ≤ x
⊢ (-(x - x_1)).Nonneg
have rwa : (x_1 - x).Nonneg
Tactic: rwa [neg_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (hypothesis)
Goal:
d : ℕ
dnsq : Nonsquare 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 : ℕ
dnsq : Nonsquare 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 (hypothesis)
Goal:
d : ℕ
dnsq : Nonsquare d
x y z w : ℤ
h : HMul.hMul (α := ℤ√(↑d : ℤ)) { re := x, im := y : ℤ√(↑d : ℤ) } { re := z, im := w : ℤ√(↑d : ℤ) } = 0
⊢ Eq (α := ℤ√(↑d : ℤ)) { re := x, im := y } 0 ∨ Eq (α := ℤ√(↑d : ℤ)) { re := z, im := w } 0
have h1 : re (d := (↑d : ℤ)) { re := x, im := y : ℤ√(↑d : ℤ) } * re (d := (↑d : ℤ)) { re := z, im := w : ℤ√(↑d : ℤ) } +
    (↑d : ℤ) * im (d := (↑d : ℤ)) { re := x, im := y : ℤ√(↑d : ℤ) } *
      im (d := (↑d : ℤ)) { re := z, im := w : ℤ√(↑d : ℤ) } =
  0
Tactic: injection h with h1 h2
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (hypothesis)
Goal:
d : ℕ
dnsq : Nonsquare d
x y z w : ℤ
h : HMul.hMul (α := ℤ√(↑d : ℤ)) { re := x, im := y : ℤ√(↑d : ℤ) } { re := z, im := w : ℤ√(↑d : ℤ) } = 0
h1 :
  re (d := (↑d : ℤ)) { re := x, im := y : ℤ√(↑d : ℤ) } * re (d := (↑d : ℤ)) { re := z, im := w : ℤ√(↑d : ℤ) } +
      (↑d : ℤ) * im (d := (↑d : ℤ)) { re := x, im := y : ℤ√(↑d : ℤ) } *
        im (d := (↑d : ℤ)) { re := z, im := w : ℤ√(↑d : ℤ) } =
    0
⊢ Eq (α := ℤ√(↑d : ℤ)) { re := x, im := y } 0 ∨ Eq (α := ℤ√(↑d : ℤ)) { re := z, im := w } 0
have h2 : re (d := (↑d : ℤ)) { re := x, im := y : ℤ√(↑d : ℤ) } * im (d := (↑d : ℤ)) { re := z, im := w : ℤ√(↑d : ℤ) } +
    im (d := (↑d : ℤ)) { re := x, im := y : ℤ√(↑d : ℤ) } * re (d := (↑d : ℤ)) { re := z, im := w : ℤ√(↑d : ℤ) } =
  0
Tactic: injection h with h1 h2
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (hypothesis)
Goal:
d : ℕ
dnsq : Nonsquare d
x y z w : ℤ
h1 :
  re (d := (↑d : ℤ)) { re := x, im := y : ℤ√(↑d : ℤ) } * re (d := (↑d : ℤ)) { re := z, im := w : ℤ√(↑d : ℤ) } +
      (↑d : ℤ) * im (d := (↑d : ℤ)) { re := x, im := y : ℤ√(↑d : ℤ) } *
        im (d := (↑d : ℤ)) { re := z, im := w : ℤ√(↑d : ℤ) } =
    0
h2 :
  re (d := (↑d : ℤ)) { re := x, im := y : ℤ√(↑d : ℤ) } * im (d := (↑d : ℤ)) { re := z, im := w : ℤ√(↑d : ℤ) } +
      im (d := (↑d : ℤ)) { re := x, im := y : ℤ√(↑d : ℤ) } * re (d := (↑d : ℤ)) { re := z, im := w : ℤ√(↑d : ℤ) } =
    0
⊢ Eq (α := ℤ√(↑d : ℤ)) { re := x, im := y } 0 ∨ Eq (α := ℤ√(↑d : ℤ)) { re := z, im := w } 0
have h1₁ : x * z = -((↑d : ℤ) * y * w)
Tactic: have h1 : x * z = -(d * y * w) := eq_neg_of_add_eq_zero_left h1
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (hypothesis)
Goal:
d : ℕ
dnsq : Nonsquare d
x y z w : ℤ
h1_1 :
  re (d := (↑d : ℤ)) { re := x, im := y : ℤ√(↑d : ℤ) } * re (d := (↑d : ℤ)) { re := z, im := w : ℤ√(↑d : ℤ) } +
      (↑d : ℤ) * im (d := (↑d : ℤ)) { re := x, im := y : ℤ√(↑d : ℤ) } *
        im (d := (↑d : ℤ)) { re := z, im := w : ℤ√(↑d : ℤ) } =
    0
h2 :
  re (d := (↑d : ℤ)) { re := x, im := y : ℤ√(↑d : ℤ) } * im (d := (↑d : ℤ)) { re := z, im := w : ℤ√(↑d : ℤ) } +
      im (d := (↑d : ℤ)) { re := x, im := y : ℤ√(↑d : ℤ) } * re (d := (↑d : ℤ)) { re := z, im := w : ℤ√(↑d : ℤ) } =
    0
h1 : x * z = -((↑d : ℤ) * y * w)
⊢ Eq (α := ℤ√(↑d : ℤ)) { re := x, im := y } 0 ∨ Eq (α := ℤ√(↑d : ℤ)) { re := z, im := w } 0
have h2₁ : x * w = -(y * z)
Tactic: have h2 : x * w = -(y * z) := eq_neg_of_add_eq_zero_left h2
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (hypothesis)
Goal:
d : ℕ
dnsq : Nonsquare d
x y z w : ℤ
h1_1 :
  re (d := (↑d : ℤ)) { re := x, im := y : ℤ√(↑d : ℤ) } * re (d := (↑d : ℤ)) { re := z, im := w : ℤ√(↑d : ℤ) } +
      (↑d : ℤ) * im (d := (↑d : ℤ)) { re := x, im := y : ℤ√(↑d : ℤ) } *
        im (d := (↑d : ℤ)) { re := z, im := w : ℤ√(↑d : ℤ) } =
    0
h2_1 :
  re (d := (↑d : ℤ)) { re := x, im := y : ℤ√(↑d : ℤ) } * im (d := (↑d : ℤ)) { re := z, im := w : ℤ√(↑d : ℤ) } +
      im (d := (↑d : ℤ)) { re := x, im := y : ℤ√(↑d : ℤ) } * re (d := (↑d : ℤ)) { re := z, im := w : ℤ√(↑d : ℤ) } =
    0
h1 : x * z = -((↑d : ℤ) * y * w)
h2 : x * w = -(y * z)
⊢ Eq (α := ℤ√(↑d : ℤ)) { re := x, im := y } 0 ∨ Eq (α := ℤ√(↑d : ℤ)) { re := z, im := w } 0
have fin : x * x = (↑d : ℤ) * y * y → Eq (α := ℤ√(↑d : ℤ)) { re := x, im := y } 0
Tactic: have fin : x * x = d * y * y → (⟨x, y⟩ : ℤ√d) = 0 := fun e =>
      match x, y, divides_sq_eq_zero_z e with
      | _, _, ⟨rfl, rfl⟩ => rfl
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℕ
dnsq : Nonsquare 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 : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
h : a = 0
⊢ a.norm = 0
have rw : norm (d := d) 0 = 0
Tactic: rw [h, norm_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
h : a = 0
rw : norm (d := d) 0 = 0
⊢ a.norm = 0
have rw₁ : Eq (α := ℤ) 0 0
Tactic: rw [h, norm_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
⊢ a.norm = 0 ↔ a = 0
have refine : ∀ (ha : a.norm = 0), a.re = re (d := d) 0 ∧ a.im = im (d := d) 0
Tactic: refine ⟨fun ha => Zsqrtd.ext_iff.mpr ?_, fun h => by rw [h, norm_zero]⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (hypothesis)
Goal:
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : a.re * a.re - d * a.im * a.im = 0
⊢ a.re = re (d := d) 0 ∧ a.im = im (d := d) 0
have ha₁ : a.re * a.re = d * a.im * a.im
Tactic: rw [sub_eq_zero] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : a.re * a.re = d * a.im * a.im
⊢ a.re = re (d := d) 0 ∧ a.im = im (d := d) 0
have pos : ∀ (h : 0 ≤ d), a.re = re (d := d) 0 ∧ a.im = im (d := d) 0
Tactic: by_cases! h : 0 ≤ d
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : a.re * a.re = d * a.im * a.im
pos : ∀ (h : 0 ≤ d), a.re = re (d := d) 0 ∧ a.im = im (d := d) 0
⊢ a.re = re (d := d) 0 ∧ a.im = im (d := d) 0
have neg : ∀ (h : d < 0), a.re = re (d := d) 0 ∧ a.im = im (d := d) 0
Tactic: by_cases! h : 0 ≤ d
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : a.re * a.re = d * a.im * a.im
h : 0 ≤ d
⊢ a.re = re (d := d) 0 ∧ a.im = im (d := d) 0
have pos : ∀ (d' : ℕ) (h_nonsquare : ∀ (n : ℤ), (↑d' : ℤ) ≠ n * n) (a : ℤ√(↑d' : ℤ)) (ha : a.re * a.re = (↑d' : ℤ) * a.im * a.im)
  (h : LE.le (α := ℤ) 0 (↑d' : ℤ)), a.re = re (d := (↑d' : ℤ)) 0 ∧ a.im = im (d := (↑d' : ℤ)) 0
Tactic: obtain ⟨d', rfl⟩ := Int.eq_ofNat_of_zero_le h
Cleared hypotheses: d, h_nonsquare, a, ha, h
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (hypothesis)
Goal:
d' : ℕ
h_nonsquare : ∀ (n : ℤ), (↑d' : ℤ) ≠ n * n
a : ℤ√(↑d' : ℤ)
ha : a.re * a.re = (↑d' : ℤ) * a.im * a.im
h : LE.le (α := ℤ) 0 (↑d' : ℤ)
⊢ a.re = re (d := (↑d' : ℤ)) 0 ∧ a.im = im (d := (↑d' : ℤ)) 0
have this : Nonsquare d'
Tactic: haveI : Nonsquare d' := ⟨fun n h => h_nonsquare n <| mod_cast h⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : a.re * a.re = d * a.im * a.im
h : d < 0
this : a.re * a.re = 0
⊢ a.re = re (d := d) 0 ∧ a.im = im (d := d) 0
have rw : ∀ (ha : HMul.hMul (α := ℤ) 0 0 = d * a.im * a.im) (h : d < 0) (this : a.re * a.re = 0),
  0 = re (d := d) 0 ∧ a.im = im (d := d) 0
Tactic: rw [eq_zero_of_mul_self_eq_zero this] at ha ⊢
Cleared hypotheses: ha, h, this
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : a.re * a.re = d * a.im * a.im
h : d < 0
⊢ a.re = re (d := d) 0 ∧ a.im = im (d := d) 0
have neg : a.re * a.re = 0
Tactic: suffices a.re * a.re = 0 by
      rw [eq_zero_of_mul_self_eq_zero this] at ha ⊢
      simpa only [true_and, or_self_right, re_zero, im_zero, eq_self_iff_true, zero_eq_mul,
        mul_zero, mul_eq_zero, h.ne, false_or, or_self_iff] using ha
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : a.re * a.re = d * a.im * a.im
h : d < 0
⊢ a.re * a.re = 0
have apply : a.re * a.re ≤ 0
Tactic: apply _root_.le_antisymm _ (mul_self_nonneg _)
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : a.re * a.re = d * a.im * a.im
h : d < 0
⊢ a.re * a.re ≤ 0
have rw : d * (a.im * a.im) ≤ 0
Tactic: rw [ha, mul_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
d : ℤ
f g : ℤ√d →+* R
h : Eq (α := R) ((f : (a : ℤ√d) → R) sqrtd : R) ((g : (a : ℤ√d) → R) sqrtd : R)
⊢ f = g
have a : ∀ (re_x im_x : ℤ),
  Eq (α := R) ((f : (a : ℤ√d) → R) { re := re_x, im := im_x } : R) ((g : (a : ℤ√d) → R) { re := re_x, im := im_x } : R)
Tactic: ext ⟨re_x, im_x⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
d : ℤ
r : { r : R // r * r = (↑d : R) }
a b : ℤ√d
⊢ (↑(a * b).re : R) + (↑(a * b).im : R) * (↑r : R) =
    ((↑a.re : R) + (↑a.im : R) * (↑r : R)) * ((↑b.re : R) + (↑b.im : R) * (↑r : R))
have this : ((↑a.re : R) + (↑a.im : R) * (↑r : R)) * ((↑b.re : R) + (↑b.im : R) * (↑r : R)) =
  HMul.hMul (α := R) (↑a.re : R) (↑b.re : R) +
      (HMul.hMul (α := R) (↑a.re : R) (↑b.im : R) + HMul.hMul (α := R) (↑a.im : R) (↑b.re : R)) * (↑r : R) +
    HMul.hMul (α := R) (↑a.im : R) (↑b.im : R) * ((↑r : R) * (↑r : R))
Tactic: have :
          (a.re + a.im * r : R) * (b.re + b.im * r) =
            a.re * b.re + (a.re * b.im + a.im * b.re) * r + a.im * b.im * (r * r) := by
          ring
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
d : ℤ
r : { r : R // r * r = (↑d : R) }
a b : ℤ√d
this :
  ((↑a.re : R) + (↑a.im : R) * (↑r : R)) * ((↑b.re : R) + (↑b.im : R) * (↑r : R)) =
    HMul.hMul (α := R) (↑a.re : R) (↑b.re : R) +
        (HMul.hMul (α := R) (↑a.re : R) (↑b.im : R) + HMul.hMul (α := R) (↑a.im : R) (↑b.re : R)) * (↑r : R) +
      HMul.hMul (α := R) (↑a.im : R) (↑b.im : R) * ((↑r : R) * (↑r : R))
⊢ (↑(a * b).re : R) + (↑(a * b).im : R) * (↑r : R) =
    ((↑a.re : R) + (↑a.im : R) * (↑r : R)) * ((↑b.re : R) + (↑b.im : R) * (↑r : R))
have simp : HMul.hMul (α := R) (↑a.re : R) (↑b.re : R) + HMul.hMul (α := R) (↑d : R) (↑a.im : R) * (↑b.im : R) +
    (HMul.hMul (α := R) (↑a.re : R) (↑b.im : R) + HMul.hMul (α := R) (↑a.im : R) (↑b.re : R)) * (↑r : R) =
  HMul.hMul (α := R) (↑a.re : R) (↑b.re : R) +
      (HMul.hMul (α := R) (↑a.re : R) (↑b.im : R) + HMul.hMul (α := R) (↑a.im : R) (↑b.re : R)) * (↑r : R) +
    HMul.hMul (α := R) (↑a.im : R) (↑b.im : R) * (↑d : R)
Tactic: simp only [re_mul, Int.cast_add, Int.cast_mul, im_mul, this, r.prop]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
d : ℤ
r : { r : R // r * r = (↑d : R) }
a b : ℤ√d
⊢ (↑(a + b).re : R) + (↑(a + b).im : R) * (↑r : R) =
    (↑a.re : R) + (↑a.im : R) * (↑r : R) + ((↑b.re : R) + (↑b.im : R) * (↑r : R))
have simp : HAdd.hAdd (α := R) (↑a.re : R) (↑b.re : R) + HAdd.hAdd (α := R) (↑a.im : R) (↑b.im : R) * (↑r : R) =
  (↑a.re : R) + (↑a.im : R) * (↑r : R) + ((↑b.re : R) + (↑b.im : R) * (↑r : R))
Tactic: simp only [re_add, Int.cast_add, im_add]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
d : ℤ
f : ℤ√d →+* R
⊢ HMul.hMul (α := R) (β := R) ((f : (a : ℤ√d) → R) sqrtd : R) ((f : (a : ℤ√d) → R) sqrtd : R) = (↑d : R)
have rw : Eq (α := R) ((f : (a : ℤ√d) → R) (HMul.hMul (α := ℤ√d) sqrtd sqrtd) : R) ((↑d : R) : R)
Tactic: rw [← f.map_mul, dmuld, map_intCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
d : ℤ
f : ℤ√d →+* R
rw : Eq (α := R) ((f : (a : ℤ√d) → R) (HMul.hMul (α := ℤ√d) sqrtd sqrtd) : R) ((↑d : R) : R)
⊢ HMul.hMul (α := R) (β := R) ((f : (a : ℤ√d) → R) sqrtd : R) ((f : (a : ℤ√d) → R) sqrtd : R) = (↑d : R)
have rw₁ : Eq (α := R) ((f : (a : ℤ√d) → R) (↑d : ℤ√d) : R) ((↑d : R) : R)
Tactic: rw [← f.map_mul, dmuld, map_intCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
d : ℤ
f : ℤ√d →+* R
rw : Eq (α := R) ((f : (a : ℤ√d) → R) (HMul.hMul (α := ℤ√d) sqrtd sqrtd) : R) ((↑d : R) : R)
rw₁ : Eq (α := R) ((f : (a : ℤ√d) → R) (↑d : ℤ√d) : R) ((↑d : R) : R)
⊢ HMul.hMul (α := R) (β := R) ((f : (a : ℤ√d) → R) sqrtd : R) ((f : (a : ℤ√d) → R) sqrtd : R) = (↑d : R)
have rw₂ : Eq.{u_1 + 1} (α := R) (↑d : R) (↑d : R)
Tactic: rw [← f.map_mul, dmuld, map_intCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
d : ℤ
f : ℤ√d →+* R
⊢ (fun (r : { r : R // r * r = (↑d : R) }) ↦
        ({ toFun := fun (a : ℤ√d) ↦ (↑a.re : R) + (↑a.im : R) * (↑r : R), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
            map_add' := ⋯ } :
          ℤ√d →+* R))
      ((fun (f : ℤ√d →+* R) ↦
          (Subtype.mk (p := fun (r : R) ↦ r * r = (↑d : R)) ((f : (a : ℤ√d) → R) sqrtd) ⋯ :
            { r : R // r * r = (↑d : R) }))
        f) =
    f
have h : Eq (α := R)
  (((fun (r : { r : R // r * r = (↑d : R) }) ↦
            ({ toFun := fun (a : ℤ√d) ↦ (↑a.re : R) + (↑a.im : R) * (↑r : R), map_one' := sorry, map_mul' := sorry,
                map_zero' := sorry, map_add' := sorry } :
              ℤ√d →+* R))
          ((fun (f : ℤ√d →+* R) ↦
              (Subtype.mk (p := fun (r : R) ↦ r * r = (↑d : R)) ((f : (a : ℤ√d) → R) sqrtd) sorry :
                { r : R // r * r = (↑d : R) }))
            f) :
        (a : ℤ√d) → R)
      sqrtd :
    R)
  ((f : (a : ℤ√d) → R) sqrtd : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
d : ℤ
r : { r : R // r * r = (↑d : R) }
hd : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha :
  Eq (α := R) ((((lift : (a : { r : R // r * r = (↑d : R) }) → ℤ√d →+* R) r : ℤ√d →+* R) : (a : ℤ√d) → R) a : R) (0 : R)
⊢ a = 0
have h_inj : Function.Injective.{1, u_1 + 1} (β := R) Int.cast
Tactic: have h_inj : Function.Injective ((↑) : ℤ → R) := Int.cast_injective
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
d : ℤ
r : { r : R // r * r = (↑d : R) }
hd : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha :
  Eq (α := R) ((((lift : (a : { r : R // r * r = (↑d : R) }) → ℤ√d →+* R) r : ℤ√d →+* R) : (a : ℤ√d) → R) a : R) (0 : R)
h_inj : Function.Injective.{1, u_1 + 1} (β := R) Int.cast
this :
  Eq (α := R)
    ((((lift : (a : { r : R // r * r = (↑d : R) }) → ℤ√d →+* R) r : ℤ√d →+* R) : (a : ℤ√d) → R) (↑a.norm : ℤ√d) : R)
    (0 : R)
⊢ a = 0
have this₁ : Eq.{u_1 + 1} (α := R) (↑a.norm : R) 0
Tactic: simp only [re_intCast, add_zero, lift_apply_apply, im_intCast, Int.cast_zero,
        zero_mul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
d : ℤ
r : { r : R // r * r = (↑d : R) }
hd : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha :
  Eq (α := R) ((((lift : (a : { r : R // r * r = (↑d : R) }) → ℤ√d →+* R) r : ℤ√d →+* R) : (a : ℤ√d) → R) a : R) (0 : R)
h_inj : Function.Injective.{1, u_1 + 1} (β := R) Int.cast
this : Eq.{u_1 + 1} (α := R) (↑a.norm : R) 0
⊢ a = 0
have rwa : ∀ (this : Eq.{u_1 + 1} (α := R) (↑a.norm : R) (↑0 : R)), a = 0
Tactic: rwa [← Int.cast_zero, h_inj.eq_iff, norm_eq_zero hd] at this
Cleared hypotheses: this