awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
a b : ℤ√d
⊢ a + b = b + a
have refine_5 : (a + b).re = (b + a).re
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
a b : ℤ√d
refine_5 : (a + b).re = (b + a).re
⊢ a + b = b + a
have refine_5₁ : (a + b).im = (b + a).im
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
⊢ CommRing (ℤ√d)
have refine_1 : ∀ (a b : ℤ√d), a + b = b + a
Tactic: refine
  { Zsqrtd.addGroupWithOne with
    npow := @npowRec (ℤ√d) ⟨1⟩ ⟨(· * ·)⟩,
    add_comm := ?_
    left_distrib := ?_
    right_distrib := ?_
    zero_mul := ?_
    mul_zero := ?_
    mul_assoc := ?_
    one_mul := ?_
    mul_one := ?_
    mul_comm := ?_ }
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
refine_1 : ∀ (a b : ℤ√d), a + b = b + a
⊢ CommRing (ℤ√d)
have refine_2 : ∀ (a b c : ℤ√d), a * b * c = a * (b * c)
Tactic: refine
  { Zsqrtd.addGroupWithOne with
    npow := @npowRec (ℤ√d) ⟨1⟩ ⟨(· * ·)⟩,
    add_comm := ?_
    left_distrib := ?_
    right_distrib := ?_
    zero_mul := ?_
    mul_zero := ?_
    mul_assoc := ?_
    one_mul := ?_
    mul_one := ?_
    mul_comm := ?_ }
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
refine_1 : ∀ (a b : ℤ√d), a + b = b + a
refine_2 : ∀ (a b c : ℤ√d), a * b * c = a * (b * c)
⊢ CommRing (ℤ√d)
have refine_3 : ∀ (a : ℤ√d), 1 * a = a
Tactic: refine
  { Zsqrtd.addGroupWithOne with
    npow := @npowRec (ℤ√d) ⟨1⟩ ⟨(· * ·)⟩,
    add_comm := ?_
    left_distrib := ?_
    right_distrib := ?_
    zero_mul := ?_
    mul_zero := ?_
    mul_assoc := ?_
    one_mul := ?_
    mul_one := ?_
    mul_comm := ?_ }
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
refine_1 : ∀ (a b : ℤ√d), a + b = b + a
refine_2 : ∀ (a b c : ℤ√d), a * b * c = a * (b * c)
refine_3 : ∀ (a : ℤ√d), 1 * a = a
⊢ CommRing (ℤ√d)
have refine_4 : ∀ (a : ℤ√d), a * 1 = a
Tactic: refine
  { Zsqrtd.addGroupWithOne with
    npow := @npowRec (ℤ√d) ⟨1⟩ ⟨(· * ·)⟩,
    add_comm := ?_
    left_distrib := ?_
    right_distrib := ?_
    zero_mul := ?_
    mul_zero := ?_
    mul_assoc := ?_
    one_mul := ?_
    mul_one := ?_
    mul_comm := ?_ }
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
refine_1 : ∀ (a b : ℤ√d), a + b = b + a
refine_2 : ∀ (a b c : ℤ√d), a * b * c = a * (b * c)
refine_3 : ∀ (a : ℤ√d), 1 * a = a
refine_4 : ∀ (a : ℤ√d), a * 1 = a
⊢ CommRing (ℤ√d)
have refine_5 : ∀ (a : ℤ√d), 0 * a = 0
Tactic: refine
  { Zsqrtd.addGroupWithOne with
    npow := @npowRec (ℤ√d) ⟨1⟩ ⟨(· * ·)⟩,
    add_comm := ?_
    left_distrib := ?_
    right_distrib := ?_
    zero_mul := ?_
    mul_zero := ?_
    mul_assoc := ?_
    one_mul := ?_
    mul_one := ?_
    mul_comm := ?_ }
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
refine_1 : ∀ (a b : ℤ√d), a + b = b + a
refine_2 : ∀ (a b c : ℤ√d), a * b * c = a * (b * c)
refine_3 : ∀ (a : ℤ√d), 1 * a = a
refine_4 : ∀ (a : ℤ√d), a * 1 = a
refine_5 : ∀ (a : ℤ√d), 0 * a = 0
⊢ CommRing (ℤ√d)
have refine_6 : ∀ (a : ℤ√d), a * 0 = 0
Tactic: refine
  { Zsqrtd.addGroupWithOne with
    npow := @npowRec (ℤ√d) ⟨1⟩ ⟨(· * ·)⟩,
    add_comm := ?_
    left_distrib := ?_
    right_distrib := ?_
    zero_mul := ?_
    mul_zero := ?_
    mul_assoc := ?_
    one_mul := ?_
    mul_one := ?_
    mul_comm := ?_ }
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
refine_1 : ∀ (a b : ℤ√d), a + b = b + a
refine_2 : ∀ (a b c : ℤ√d), a * b * c = a * (b * c)
refine_3 : ∀ (a : ℤ√d), 1 * a = a
refine_4 : ∀ (a : ℤ√d), a * 1 = a
refine_5 : ∀ (a : ℤ√d), 0 * a = 0
refine_6 : ∀ (a : ℤ√d), a * 0 = 0
⊢ CommRing (ℤ√d)
have refine_7 : ∀ (a b c : ℤ√d), a * (b + c) = a * b + a * c
Tactic: refine
  { Zsqrtd.addGroupWithOne with
    npow := @npowRec (ℤ√d) ⟨1⟩ ⟨(· * ·)⟩,
    add_comm := ?_
    left_distrib := ?_
    right_distrib := ?_
    zero_mul := ?_
    mul_zero := ?_
    mul_assoc := ?_
    one_mul := ?_
    mul_one := ?_
    mul_comm := ?_ }
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
refine_1 : ∀ (a b : ℤ√d), a + b = b + a
refine_2 : ∀ (a b c : ℤ√d), a * b * c = a * (b * c)
refine_3 : ∀ (a : ℤ√d), 1 * a = a
refine_4 : ∀ (a : ℤ√d), a * 1 = a
refine_5 : ∀ (a : ℤ√d), 0 * a = 0
refine_6 : ∀ (a : ℤ√d), a * 0 = 0
refine_7 : ∀ (a b c : ℤ√d), a * (b + c) = a * b + a * c
⊢ CommRing (ℤ√d)
have refine_8 : ∀ (a b c : ℤ√d), (a + b) * c = a * c + b * c
Tactic: refine
  { Zsqrtd.addGroupWithOne with
    npow := @npowRec (ℤ√d) ⟨1⟩ ⟨(· * ·)⟩,
    add_comm := ?_
    left_distrib := ?_
    right_distrib := ?_
    zero_mul := ?_
    mul_zero := ?_
    mul_assoc := ?_
    one_mul := ?_
    mul_one := ?_
    mul_comm := ?_ }
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
refine_1 : ∀ (a b : ℤ√d), a + b = b + a
refine_2 : ∀ (a b c : ℤ√d), a * b * c = a * (b * c)
refine_3 : ∀ (a : ℤ√d), 1 * a = a
refine_4 : ∀ (a : ℤ√d), a * 1 = a
refine_5 : ∀ (a : ℤ√d), 0 * a = 0
refine_6 : ∀ (a : ℤ√d), a * 0 = 0
refine_7 : ∀ (a b c : ℤ√d), a * (b + c) = a * b + a * c
refine_8 : ∀ (a b c : ℤ√d), (a + b) * c = a * c + b * c
⊢ CommRing (ℤ√d)
have refine_9 : ∀ (a b : ℤ√d), a * b = b * a
Tactic: refine
  { Zsqrtd.addGroupWithOne with
    npow := @npowRec (ℤ√d) ⟨1⟩ ⟨(· * ·)⟩,
    add_comm := ?_
    left_distrib := ?_
    right_distrib := ?_
    zero_mul := ?_
    mul_zero := ?_
    mul_assoc := ?_
    one_mul := ?_
    mul_one := ?_
    mul_comm := ?_ }
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
a b : ℤ√d
⊢ a + b = b + a
have refine_1 : (a + b).re = (b + a).re
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
a b : ℤ√d
refine_1 : (a + b).re = (b + a).re
⊢ a + b = b + a
have refine_1₁ : (a + b).im = (b + a).im
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
a b c : ℤ√d
⊢ a * b * c = a * (b * c)
have refine_2 : (a * b * c).re = (a * (b * c)).re
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
a b c : ℤ√d
refine_2 : (a * b * c).re = (a * (b * c)).re
⊢ a * b * c = a * (b * c)
have refine_2₁ : (a * b * c).im = (a * (b * c)).im
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
a : ℤ√d
⊢ 1 * a = a
have refine_3 : (1 * a).re = a.re
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
a : ℤ√d
refine_3 : (1 * a).re = a.re
⊢ 1 * a = a
have refine_3₁ : (1 * a).im = a.im
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
a : ℤ√d
⊢ a * 1 = a
have refine_4 : (a * 1).re = a.re
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
a : ℤ√d
refine_4 : (a * 1).re = a.re
⊢ a * 1 = a
have refine_4₁ : (a * 1).im = a.im
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
a : ℤ√d
⊢ 0 * a = 0
have refine_5 : (0 * a).re = re (d := d) 0
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
a : ℤ√d
refine_5 : (0 * a).re = re (d := d) 0
⊢ 0 * a = 0
have refine_5₁ : (0 * a).im = im (d := d) 0
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
a : ℤ√d
⊢ a * 0 = 0
have refine_6 : (a * 0).re = re (d := d) 0
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
a : ℤ√d
refine_6 : (a * 0).re = re (d := d) 0
⊢ a * 0 = 0
have refine_6₁ : (a * 0).im = im (d := d) 0
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
a b c : ℤ√d
⊢ a * (b + c) = a * b + a * c
have refine_7 : (a * (b + c)).re = (a * b + a * c).re
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
a b c : ℤ√d
refine_7 : (a * (b + c)).re = (a * b + a * c).re
⊢ a * (b + c) = a * b + a * c
have refine_7₁ : (a * (b + c)).im = (a * b + a * c).im
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
a b c : ℤ√d
⊢ (a + b) * c = a * c + b * c
have refine_8 : ((a + b) * c).re = (a * c + b * c).re
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
a b c : ℤ√d
refine_8 : ((a + b) * c).re = (a * c + b * c).re
⊢ (a + b) * c = a * c + b * c
have refine_8₁ : ((a + b) * c).im = (a * c + b * c).im
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
a b : ℤ√d
⊢ a * b = b * a
have refine_9 : (a * b).re = (b * a).re
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
a b : ℤ√d
refine_9 : (a * b).re = (b * a).re
⊢ a * b = b * a
have refine_9₁ : (a * b).im = (b * a).im
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
a b : ℤ√d
⊢ star (a * b) = star b * star a
have re : (star (a * b)).re = (star b * star a).re
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
a b : ℤ√d
re : (star (a * b)).re = (star b * star a).re
⊢ star (a * b) = star b * star a
have im : (star (a * b)).im = (star b * star a).im
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
a b : ℤ√d
⊢ (star (a * b)).re = (star b * star a).re
have re : a.re * b.re + d * a.im * b.im = b.re * a.re + d * b.im * a.im
Tactic: simp
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
a b : ℤ√d
⊢ (star (a * b)).im = (star b * star a).im
have im : -(a.im * b.re) + -(a.re * b.im) = -(b.re * a.im) + -(b.im * a.re)
Tactic: simp
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d n : ℤ
⊢ re (d := d) (↑n : ℤ√d) = n
have ofNat : ∀ (a : ℕ), re (d := d) (↑(Int.ofNat a) : ℤ√d) = Int.ofNat a
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d n : ℤ
ofNat : ∀ (a : ℕ), re (d := d) (↑(Int.ofNat a) : ℤ√d) = Int.ofNat a
⊢ re (d := d) (↑n : ℤ√d) = n
have negSucc : ∀ (a : ℕ), re (d := d) (↑(Int.negSucc a) : ℤ√d) = Int.negSucc a
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d n : ℤ
⊢ im (d := d) (↑n : ℤ√d) = 0
have ofNat : ∀ (a : ℕ), im (d := d) (↑(Int.ofNat a) : ℤ√d) = 0
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d n : ℤ
ofNat : ∀ (a : ℕ), im (d := d) (↑(Int.ofNat a) : ℤ√d) = 0
⊢ im (d := d) (↑n : ℤ√d) = 0
have negSucc : ∀ (a : ℕ), im (d := d) (↑(Int.negSucc a) : ℤ√d) = 0
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d n : ℤ
⊢ Eq (α := ℤ√d) (↑n : ℤ√d) { re := n, im := 0 }
have re : re (d := d) (↑n : ℤ√d) = re (d := d) { re := n, im := 0 }
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d n : ℤ
re : Zsqrtd.re (d := d) (↑n : ℤ√d) = Zsqrtd.re (d := d) { re := n, im := 0 }
⊢ Eq (α := ℤ√d) (↑n : ℤ√d) { re := n, im := 0 }
have im : im (d := d) (↑n : ℤ√d) = im (d := d) { re := n, im := 0 }
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d n : ℤ
⊢ Eq (α := ℤ√d) (ofInt n) (↑n : ℤ√d)
have re : re (d := d) (ofInt n) = re (d := d) (↑n : ℤ√d)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d n : ℤ
re : Zsqrtd.re (d := d) (ofInt n) = Zsqrtd.re (d := d) (↑n : ℤ√d)
⊢ Eq (α := ℤ√d) (ofInt n) (↑n : ℤ√d)
have im : im (d := d) (ofInt n) = im (d := d) (↑n : ℤ√d)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
n : ℕ
x y : ℤ
⊢ HMul.hMul (α := ℤ√d) (↑n : ℤ√d) { re := x, im := y : ℤ√d } = { re := (↑n : ℤ) * x, im := (↑n : ℤ) * y }
have re : (HMul.hMul (α := ℤ√d) (↑n : ℤ√d) { re := x, im := y : ℤ√d }).re = re (d := d) { re := (↑n : ℤ) * x, im := (↑n : ℤ) * y }
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
n : ℕ
x y : ℤ
re :
  (HMul.hMul (α := ℤ√d) (↑n : ℤ√d) { re := x, im := y : ℤ√d }).re =
    Zsqrtd.re (d := d) { re := (↑n : ℤ) * x, im := (↑n : ℤ) * y }
⊢ HMul.hMul (α := ℤ√d) (↑n : ℤ√d) { re := x, im := y : ℤ√d } = { re := (↑n : ℤ) * x, im := (↑n : ℤ) * y }
have im : (HMul.hMul (α := ℤ√d) (↑n : ℤ√d) { re := x, im := y : ℤ√d }).im = im (d := d) { re := (↑n : ℤ) * x, im := (↑n : ℤ) * y }
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d n x y : ℤ
⊢ HMul.hMul (α := ℤ√d) (↑n : ℤ√d) { re := x, im := y : ℤ√d } = { re := n * x, im := n * y }
have re : (HMul.hMul (α := ℤ√d) (↑n : ℤ√d) { re := x, im := y : ℤ√d }).re = re (d := d) { re := n * x, im := n * y }
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d n x y : ℤ
re : (HMul.hMul (α := ℤ√d) (↑n : ℤ√d) { re := x, im := y : ℤ√d }).re = Zsqrtd.re (d := d) { re := n * x, im := n * y }
⊢ HMul.hMul (α := ℤ√d) (↑n : ℤ√d) { re := x, im := y : ℤ√d } = { re := n * x, im := n * y }
have im : (HMul.hMul (α := ℤ√d) (↑n : ℤ√d) { re := x, im := y : ℤ√d }).im = im (d := d) { re := n * x, im := n * y }
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d x y : ℤ
⊢ HMul.hMul (α := ℤ√d) sqrtd { re := x, im := y : ℤ√d } = { re := d * y, im := x }
have re : (HMul.hMul (α := ℤ√d) sqrtd { re := x, im := y : ℤ√d }).re = re (d := d) { re := d * y, im := x }
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d x y : ℤ
re : (HMul.hMul (α := ℤ√d) sqrtd { re := x, im := y : ℤ√d }).re = Zsqrtd.re (d := d) { re := d * y, im := x }
⊢ HMul.hMul (α := ℤ√d) sqrtd { re := x, im := y : ℤ√d } = { re := d * y, im := x }
have im : (HMul.hMul (α := ℤ√d) sqrtd { re := x, im := y : ℤ√d }).im = im (d := d) { re := d * y, im := x }
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
⊢ HMul.hMul (α := ℤ√d) sqrtd sqrtd = (↑d : ℤ√d)
have re : (HMul.hMul (α := ℤ√d) sqrtd sqrtd).re = re (d := d) (↑d : ℤ√d)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
re : (HMul.hMul (α := ℤ√d) sqrtd sqrtd).re = Zsqrtd.re (d := d) (↑d : ℤ√d)
⊢ HMul.hMul (α := ℤ√d) sqrtd sqrtd = (↑d : ℤ√d)
have im : (HMul.hMul (α := ℤ√d) sqrtd sqrtd).im = im (d := d) (↑d : ℤ√d)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d n x y : ℤ
⊢ HMul.hMul (α := ℤ√d) sqrtd (↑n : ℤ√d) * { re := x, im := y : ℤ√d } = { re := d * n * y, im := n * x }
have re : (HMul.hMul (α := ℤ√d) sqrtd (↑n : ℤ√d) * { re := x, im := y : ℤ√d }).re = re (d := d) { re := d * n * y, im := n * x }
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d n x y : ℤ
re :
  (HMul.hMul (α := ℤ√d) sqrtd (↑n : ℤ√d) * { re := x, im := y : ℤ√d }).re =
    Zsqrtd.re (d := d) { re := d * n * y, im := n * x }
⊢ HMul.hMul (α := ℤ√d) sqrtd (↑n : ℤ√d) * { re := x, im := y : ℤ√d } = { re := d * n * y, im := n * x }
have im : (HMul.hMul (α := ℤ√d) sqrtd (↑n : ℤ√d) * { re := x, im := y : ℤ√d }).im = im (d := d) { re := d * n * y, im := n * x }
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d x y : ℤ
⊢ { re := x, im := y } = (↑x : ℤ√d) + HMul.hMul (α := ℤ√d) sqrtd (↑y : ℤ√d)
have re : re (d := d) { re := x, im := y : ℤ√d } = ((↑x : ℤ√d) + HMul.hMul (α := ℤ√d) sqrtd (↑y : ℤ√d)).re
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d x y : ℤ
re : Zsqrtd.re (d := d) { re := x, im := y : ℤ√d } = ((↑x : ℤ√d) + HMul.hMul (α := ℤ√d) sqrtd (↑y : ℤ√d)).re
⊢ { re := x, im := y } = (↑x : ℤ√d) + HMul.hMul (α := ℤ√d) sqrtd (↑y : ℤ√d)
have im : im (d := d) { re := x, im := y : ℤ√d } = ((↑x : ℤ√d) + HMul.hMul (α := ℤ√d) sqrtd (↑y : ℤ√d)).im
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d x y : ℤ
⊢ HMul.hMul (α := ℤ√d) { re := x, im := y : ℤ√d } (star { re := x, im := y : ℤ√d }) =
    HMul.hMul (α := ℤ√d) (↑x : ℤ√d) (↑x : ℤ√d) - HMul.hMul (α := ℤ√d) (↑d : ℤ√d) (↑y : ℤ√d) * (↑y : ℤ√d)
have re : (HMul.hMul (α := ℤ√d) { re := x, im := y : ℤ√d } (star { re := x, im := y : ℤ√d })).re =
  (HMul.hMul (α := ℤ√d) (↑x : ℤ√d) (↑x : ℤ√d) - HMul.hMul (α := ℤ√d) (↑d : ℤ√d) (↑y : ℤ√d) * (↑y : ℤ√d)).re
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d x y : ℤ
re :
  (HMul.hMul (α := ℤ√d) { re := x, im := y : ℤ√d } (star { re := x, im := y : ℤ√d })).re =
    (HMul.hMul (α := ℤ√d) (↑x : ℤ√d) (↑x : ℤ√d) - HMul.hMul (α := ℤ√d) (↑d : ℤ√d) (↑y : ℤ√d) * (↑y : ℤ√d)).re
⊢ HMul.hMul (α := ℤ√d) { re := x, im := y : ℤ√d } (star { re := x, im := y : ℤ√d }) =
    HMul.hMul (α := ℤ√d) (↑x : ℤ√d) (↑x : ℤ√d) - HMul.hMul (α := ℤ√d) (↑d : ℤ√d) (↑y : ℤ√d) * (↑y : ℤ√d)
have im : (HMul.hMul (α := ℤ√d) { re := x, im := y : ℤ√d } (star { re := x, im := y : ℤ√d })).im =
  (HMul.hMul (α := ℤ√d) (↑x : ℤ√d) (↑x : ℤ√d) - HMul.hMul (α := ℤ√d) (↑d : ℤ√d) (↑y : ℤ√d) * (↑y : ℤ√d)).im
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d z : ℤ
a : ℤ√d
⊢ (↑z : ℤ√d) ∣ a ↔ z ∣ a.re ∧ z ∣ a.im
have mp : (↑z : ℤ√d) ∣ a → z ∣ a.re ∧ z ∣ a.im
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d z : ℤ
a : ℤ√d
mp : (↑z : ℤ√d) ∣ a → z ∣ a.re ∧ z ∣ a.im
⊢ (↑z : ℤ√d) ∣ a ↔ z ∣ a.re ∧ z ∣ a.im
have mpr : z ∣ a.re ∧ z ∣ a.im → (↑z : ℤ√d) ∣ a
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d z : ℤ
a : ℤ√d
r : ℤ
hr : a.re = z * r
i : ℤ
hi : a.im = z * i
⊢ (↑z : ℤ√d) ∣ a
have h : a = HMul.hMul (α := ℤ√d) (↑z : ℤ√d) { re := r, im := i }
Tactic: use ⟨r, i⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d z : ℤ
a : ℤ√d
r : ℤ
hr : a.re = z * r
i : ℤ
hi : a.im = z * i
⊢ a = HMul.hMul (α := ℤ√d) (↑z : ℤ√d) { re := r, im := i }
have h : a.re = re (d := d) { re := z * r, im := z * i } ∧ a.im = im (d := d) { re := z * r, im := z * i }
Tactic: rw [smul_val, Zsqrtd.ext_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d a b : ℤ
⊢ Dvd.dvd (α := ℤ√d) (↑a : ℤ√d) (↑b : ℤ√d) ↔ a ∣ b
have rw : a ∣ re (d := d) (↑b : ℤ√d) ∧ a ∣ im (d := d) (↑b : ℤ√d) ↔ a ∣ b
Tactic: rw [intCast_dvd]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d a : ℤ
b c : ℤ√d
ha : a ≠ 0
h : (↑a : ℤ√d) * b = (↑a : ℤ√d) * c
⊢ b = c
have rw : ∀ (h : ((↑a : ℤ√d) * b).re = ((↑a : ℤ√d) * c).re ∧ ((↑a : ℤ√d) * b).im = ((↑a : ℤ√d) * c).im), b.re = c.re ∧ b.im = c.im
Tactic: rw [Zsqrtd.ext_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d a : ℤ
b c : ℤ√d
ha : a ≠ 0
h : ((↑a : ℤ√d) * b).re = ((↑a : ℤ√d) * c).re ∧ ((↑a : ℤ√d) * b).im = ((↑a : ℤ√d) * c).im
⊢ b.re = c.re ∧ b.im = c.im
have apply : ((↑a : ℤ√d) * b).re = ((↑a : ℤ√d) * c).re → b.re = c.re
Tactic: apply And.imp _ _ h
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d a : ℤ
b c : ℤ√d
ha : a ≠ 0
h : ((↑a : ℤ√d) * b).re = ((↑a : ℤ√d) * c).re ∧ ((↑a : ℤ√d) * b).im = ((↑a : ℤ√d) * c).im
apply : ((↑a : ℤ√d) * b).re = ((↑a : ℤ√d) * c).re → b.re = c.re
⊢ b.re = c.re ∧ b.im = c.im
have apply₁ : ((↑a : ℤ√d) * b).im = ((↑a : ℤ√d) * c).im → b.im = c.im
Tactic: apply And.imp _ _ h
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
⊢ IsCoprime b.re b.im
have nonzero : ¬(b.re = 0 ∧ b.im = 0)
Tactic: apply isCoprime_of_dvd
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
nonzero : ¬(b.re = 0 ∧ b.im = 0)
⊢ IsCoprime b.re b.im
have H : ∀ z ∈ nonunits ℤ, z ≠ 0 → z ∣ b.re → ¬z ∣ b.im
Tactic: apply isCoprime_of_dvd
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (hypothesis)
Goal:
d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
hre : b.re = 0
him : b.im = 0
⊢ False
have hdvd₁ : 0 ∣ a
Tactic: obtain rfl : b = 0 := Zsqrtd.ext hre him
Cleared hypotheses: b, hdvd, hre, him
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (hypothesis)
Goal:
d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
hre : b.re = 0
him : b.im = 0
hdvd₁ : 0 ∣ a
⊢ False
have hre₁ : re (d := d) 0 = 0
Tactic: obtain rfl : b = 0 := Zsqrtd.ext hre him
Cleared hypotheses: b, hdvd, hre, him
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (hypothesis)
Goal:
d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
hre : b.re = 0
him : b.im = 0
hdvd₁ : 0 ∣ a
hre₁ : re (d := d) 0 = 0
⊢ False
have him₁ : im (d := d) 0 = 0
Tactic: obtain rfl : b = 0 := Zsqrtd.ext hre him
Cleared hypotheses: b, hdvd, hre, him
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (hypothesis)
Goal:
d : ℤ
a : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : 0 ∣ a
hre : re (d := d) 0 = 0
him : im (d := d) 0 = 0
⊢ False
have hdvd₁ : a = 0
Tactic: rw [zero_dvd_iff] at hdvd
Cleared hypotheses: hdvd, hre, him
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
z : ℤ
hz : z ∈ nonunits ℤ
hzdvdu : z ∣ b.re
hzdvdv : z ∣ b.im
⊢ False
have H : IsUnit z
Tactic: apply hz
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
z : ℤ
hz : z ∈ nonunits ℤ
hzdvdu : z ∣ b.re
hzdvdv : z ∣ b.im
⊢ z ∣ a.re ∧ z ∣ a.im
have rw : (↑z : ℤ√d) ∣ a
Tactic: rw [← intCast_dvd]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
z : ℤ
hz : z ∈ nonunits ℤ
hzdvdu : z ∣ b.re
hzdvdv : z ∣ b.im
⊢ (↑z : ℤ√d) ∣ a
have apply : (↑z : ℤ√d) ∣ b
Tactic: apply dvd_trans _ hdvd
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
z : ℤ
hz : z ∈ nonunits ℤ
hzdvdu : z ∣ b.re
hzdvdv : z ∣ b.im
⊢ (↑z : ℤ√d) ∣ b
have rw : z ∣ b.re ∧ z ∣ b.im
Tactic: rw [intCast_dvd]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (hypothesis)
Goal:
d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
z : ℤ
hz : z ∈ nonunits ℤ
hzdvdu : z ∣ b.re
hzdvdv : z ∣ b.im
⊢ IsUnit z
have ha : z ∣ a.re
Tactic: obtain ⟨ha, hb⟩ : z ∣ a.re ∧ z ∣ a.im := by
      rw [← intCast_dvd]
      apply dvd_trans _ hdvd
      rw [intCast_dvd]
      exact ⟨hzdvdu, hzdvdv⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (hypothesis)
Goal:
d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
z : ℤ
hz : z ∈ nonunits ℤ
hzdvdu : z ∣ b.re
hzdvdv : z ∣ b.im
ha : z ∣ a.re
⊢ IsUnit z
have hb : z ∣ a.im
Tactic: obtain ⟨ha, hb⟩ : z ∣ a.re ∧ z ∣ a.im := by
      rw [← intCast_dvd]
      apply dvd_trans _ hdvd
      rw [intCast_dvd]
      exact ⟨hzdvdu, hzdvdv⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
a : ℤ√d
hgcd : 0 < a.re.gcd a.im
⊢ ∃ (b : ℤ√d), a = (↑(↑(a.re.gcd a.im) : ℤ) : ℤ√d) * b ∧ IsCoprime b.re b.im
have obtain : ∀ (re im : ℤ) (H1 : re.gcd im = 1) (Hre : a.re = re * (↑(a.re.gcd a.im) : ℤ))
  (Him : a.im = im * (↑(a.re.gcd a.im) : ℤ)), ∃ (b : ℤ√d), a = (↑(↑(a.re.gcd a.im) : ℤ) : ℤ√d) * b ∧ IsCoprime b.re b.im
Tactic: obtain ⟨re, im, H1, Hre, Him⟩ := Int.exists_gcd_one hgcd
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (hypothesis)
Goal:
d : ℤ
a : ℤ√d
hgcd : 0 < a.re.gcd a.im
re im : ℤ
H1 : re.gcd im = 1
Hre : a.re = re * (↑(a.re.gcd a.im) : ℤ)
Him : a.im = im * (↑(a.re.gcd a.im) : ℤ)
⊢ ∃ (b : ℤ√d), a = (↑(↑(a.re.gcd a.im) : ℤ) : ℤ√d) * b ∧ IsCoprime b.re b.im
have Hre₁ : a.re = (↑(a.re.gcd a.im) : ℤ) * re
Tactic: rw [mul_comm] at Hre Him
Cleared hypotheses: Hre, Him
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (hypothesis)
Goal:
d : ℤ
a : ℤ√d
hgcd : 0 < a.re.gcd a.im
re im : ℤ
H1 : re.gcd im = 1
Hre : a.re = re * (↑(a.re.gcd a.im) : ℤ)
Him : a.im = im * (↑(a.re.gcd a.im) : ℤ)
Hre₁ : a.re = (↑(a.re.gcd a.im) : ℤ) * re
⊢ ∃ (b : ℤ√d), a = (↑(↑(a.re.gcd a.im) : ℤ) : ℤ√d) * b ∧ IsCoprime b.re b.im
have Him₁ : a.im = (↑(a.re.gcd a.im) : ℤ) * im
Tactic: rw [mul_comm] at Hre Him
Cleared hypotheses: Hre, Him