awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
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)
fin : x * x = (↑d : ℤ) * y * y → Eq (α := ℤ√(↑d : ℤ)) { re := x, im := y } 0
z0 : z = 0
w0 : ¬w = 0
⊢ x * x * w = -y * (x * z)

Tactic:
simp [h2, mul_assoc, mul_left_comm]

Premises used: mul_assoc, mul_left_comm
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
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)
fin : x * x = (↑d : ℤ) * y * y → Eq (α := ℤ√(↑d : ℤ)) { re := x, im := y } 0
z0 : z = 0
w0 : ¬w = 0
⊢ -y * (x * z) = (↑d : ℤ) * y * y * w

Tactic:
simp [h1, mul_assoc, mul_left_comm]

Premises used: mul_assoc, mul_left_comm
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
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)
fin : x * x = (↑d : ℤ) * y * y → Eq (α := ℤ√(↑d : ℤ)) { re := x, im := y } 0
z0 : ¬z = 0
⊢ x * x * z = (↑d : ℤ) * -y * (x * w)

Tactic:
simp [h1, mul_assoc, mul_left_comm]

Premises used: mul_assoc, mul_left_comm
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
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)
fin : x * x = (↑d : ℤ) * y * y → Eq (α := ℤ√(↑d : ℤ)) { re := x, im := y } 0
z0 : ¬z = 0
⊢ (↑d : ℤ) * -y * (x * w) = (↑d : ℤ) * y * y * z

Tactic:
simp [h2, mul_assoc, mul_left_comm]

Premises used: mul_assoc, mul_left_comm
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
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)
fin : x * x = (↑d : ℤ) * y * y → Eq (α := ℤ√(↑d : ℤ)) { re := x, im := y } 0
⊢ Eq (α := ℤ√(↑d : ℤ)) { re := x, im := y } 0 ∨ Eq (α := ℤ√(↑d : ℤ)) { re := z, im := w } 0

Tactic:
exact
      if z0 : z = 0 then
        if w0 : w = 0 then
          Or.inr
            (match z, w, z0, w0 with
            | _, _, rfl, rfl => rfl)
        else
          Or.inl <|
            fin <|
              mul_right_cancel₀ w0 <|
                calc
                  x * x * w = -y * (x * z) := by simp [h2, mul_assoc, mul_left_comm]
                  _ = d * y * y * w := by simp [h1, mul_assoc, mul_left_comm]
      else
        Or.inl <|
          fin <|
            mul_right_cancel₀ z0 <|
              calc
                x * x * z = d * -y * (x * w) := by simp [h1, mul_assoc, mul_left_comm]
                _ = d * y * y * z := by simp [h2, mul_assoc, mul_left_comm]

Premises used: HMul.hMul, Or.inl, Or.inr
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
dnsq : Nonsquare d
⊢ IsDomain (ℤ√(↑d : ℤ))

Tactic:
NoZeroDivisors.to_isDomain _

Premises used: NoZeroDivisors.to_isDomain
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
dnsq : Nonsquare d
a b : ℤ√(↑d : ℤ)
a0 : 0 < a
b0 : 0 < b
⊢ 0 < a * b

Tactic:
fun ab =>
  Or.elim
    (eq_zero_or_eq_zero_of_mul_eq_zero
      (_root_.le_antisymm ab (Zsqrtd.mul_nonneg _ _ (le_of_lt a0) (le_of_lt b0))))
    (fun e => ne_of_gt a0 e) fun e => ne_of_gt b0 e

Premises used: le_of_lt, ne_of_gt, le_antisymm, Or.elim, Not, NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero, Zsqrtd.mul_nonneg
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
dnsq : Nonsquare d
⊢ LE.le (α := ℤ√(↑d : ℤ)) 0 1

Tactic:
trivial
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
dnsq : Nonsquare d
a b : ℤ√(↑d : ℤ)
ab : a ≤ b
c : ℤ√(↑d : ℤ)
rwa rwa₁ rwa₂ rwa₃ : (b - a).Nonneg
⊢ (b + c - (a + c)).Nonneg

Tactic:
rwa [add_sub_add_right_eq_sub]

Premises used: add_sub_add_right_eq_sub
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
dnsq : Nonsquare d
a b c : ℤ√(↑d : ℤ)
h : c + a ≤ c + b
⊢ a ≤ b

Tactic:
_root_.le_of_add_le_add_left h

Premises used: le_of_add_le_add_left
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
dnsq : Nonsquare d
a b c : ℤ√(↑d : ℤ)
h : c + a ≤ c + b
⊢ a ≤ b

Tactic:
exact _root_.le_of_add_le_add_left h

Premises used: le_of_add_le_add_left
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
dnsq : Nonsquare d
a b : ℤ√(↑d : ℤ)
h : a < b
c : ℤ√(↑d : ℤ)
⊢ c + a < c + b

Tactic:
fun h' =>
  h (_root_.le_of_add_le_add_left h')

Premises used: le_of_add_le_add_left, Not
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℕ
dnsq : Nonsquare d
⊢ IsStrictOrderedRing (ℤ√(↑d : ℤ))

Tactic:
.of_mul_pos Zsqrtd.mul_pos

Premises used: Zsqrtd.mul_pos, IsStrictOrderedRing.of_mul_pos
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
h : a = 0
rw : norm (d := d) 0 = 0
rw₁ rw₂ : Eq (α := ℤ) 0 0
⊢ a.norm = 0

Tactic:
rw [h, norm_zero]

Premises used: Zsqrtd.norm_zero
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
refine : ∀ (ha : a.norm = 0), a.re = re (d := d) 0 ∧ a.im = im (d := d) 0
⊢ a.norm = 0 ↔ a = 0

Tactic:
refine ⟨fun ha => Zsqrtd.ext_iff.mpr ?_, fun h => by rw [h, norm_zero]⟩
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : a.re * a.re - d * a.im * a.im = 0
⊢ a.re * a.re = d * a.im * a.im

Tactic:
rw [sub_eq_zero] at ha

Premises used: sub_eq_zero
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
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
neg : ∀ (h : d < 0), a.re = re (d := d) 0 ∧ a.im = im (d := d) 0
⊢ a.re = re (d := d) 0 ∧ a.im = im (d := d) 0

Tactic:
by_cases! h : 0 ≤ d
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : a.re * a.re = d * a.im * a.im
h : 0 ≤ d
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
⊢ a.re = re (d := d) 0 ∧ a.im = im (d := d) 0

Tactic:
obtain ⟨d', rfl⟩ := Int.eq_ofNat_of_zero_le h

Premises used: Int.eq_ofNat_of_zero_le, rfl
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
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' : ℤ)
⊢ Nonsquare d'

Tactic:
haveI : Nonsquare d' := ⟨fun n h => h_nonsquare n <| mod_cast h⟩
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
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' : ℤ)
this : Nonsquare d'
⊢ a.re = re (d := (↑d' : ℤ)) 0 ∧ a.im = im (d := (↑d' : ℤ)) 0

Tactic:
divides_sq_eq_zero_z ha

Premises used: Zsqrtd.divides_sq_eq_zero_z
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
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' : ℤ)
this : Nonsquare d'
⊢ a.re = re (d := (↑d' : ℤ)) 0 ∧ a.im = im (d := (↑d' : ℤ)) 0

Tactic:
exact divides_sq_eq_zero_z ha

Premises used: Zsqrtd.divides_sq_eq_zero_z
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
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
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
⊢ a.re = re (d := d) 0 ∧ a.im = im (d := d) 0

Tactic:
rw [eq_zero_of_mul_self_eq_zero this] at ha ⊢

Premises used: eq_zero_of_mul_self_eq_zero
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
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:
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

Premises used: Zsqrtd.re_zero, or_self_iff, zero_eq_mul, false_or, mul_eq_zero, MulZeroClass.mul_zero, Zsqrtd.im_zero, eq_self_iff_true, true_and, LT.lt.ne, or_self_right
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : a.re * a.re = d * a.im * a.im
h : d < 0
neg : a.re * a.re = 0
⊢ a.re = re (d := d) 0 ∧ a.im = im (d := d) 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
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : a.re * a.re = d * a.im * a.im
h : d < 0
apply : a.re * a.re ≤ 0
⊢ a.re * a.re = 0

Tactic:
apply _root_.le_antisymm _ (mul_self_nonneg _)

Premises used: mul_self_nonneg, le_antisymm
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : a.re * a.re = d * a.im * a.im
h : d < 0
rw : d * (a.im * a.im) ≤ 0
⊢ a.re * a.re ≤ 0

Tactic:
rw [ha, mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : a.re * a.re = d * a.im * a.im
h : d < 0
⊢ d * (a.im * a.im) ≤ 0

Tactic:
mul_nonpos_of_nonpos_of_nonneg h.le (mul_self_nonneg _)

Premises used: mul_self_nonneg, mul_nonpos_of_nonpos_of_nonneg, LT.lt.le
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : a.re * a.re = d * a.im * a.im
h : d < 0
⊢ d * (a.im * a.im) ≤ 0

Tactic:
exact mul_nonpos_of_nonpos_of_nonneg h.le (mul_self_nonneg _)

Premises used: mul_self_nonneg, mul_nonpos_of_nonpos_of_nonneg, LT.lt.le
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
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)
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)
⊢ f = g

Tactic:
ext ⟨re_x, im_x⟩
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
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)
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:
simp [decompose, h]

Premises used: Zsqrtd.decompose
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
R : Type u_1
inst : CommRing R
d : ℤ
r : { r : R // r * r = (↑d : R) }
⊢ (↑(re (d := d) 1) : R) + (↑(im (d := d) 1) : R) * (↑r : R) = 1

Tactic:
simp
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
R : Type u_1
inst : CommRing R
d : ℤ
r : { r : R // r * r = (↑d : R) }
a b : ℤ√d
⊢ ((↑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:
ring
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
R : Type u_1
inst : CommRing R
d : ℤ
r : { r : R // r * r = (↑d : R) }
a b : ℤ√d
⊢ ((↑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
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
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))
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)
⊢ (↑(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))

Tactic:
simp only [re_mul, Int.cast_add, Int.cast_mul, im_mul, this, r.prop]

Premises used: Zsqrtd.re_mul, Int.cast_add, Int.cast_mul, Subtype.prop, Zsqrtd.im_mul
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
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))
⊢ 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:
ring
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
R : Type u_1
inst : CommRing R
d : ℤ
r : { r : R // r * r = (↑d : R) }
⊢ (↑(re (d := d) 0) : R) + (↑(im (d := d) 0) : R) * (↑r : R) = 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
R : Type u_1
inst : CommRing R
d : ℤ
r : { r : R // r * r = (↑d : R) }
a b : ℤ√d
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))
⊢ (↑(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))

Tactic:
simp only [re_add, Int.cast_add, im_add]

Premises used: Zsqrtd.im_add, Int.cast_add, Zsqrtd.re_add
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
R : Type u_1
inst : CommRing R
d : ℤ
r : { r : R // r * r = (↑d : R) }
a b : ℤ√d
⊢ 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:
ring
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
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)
rw₂ rw₃ : Eq.{u_1 + 1} (α := R) (↑d : R) (↑d : R)
⊢ HMul.hMul (α := R) (β := R) ((f : (a : ℤ√d) → R) sqrtd : R) ((f : (a : ℤ√d) → R) sqrtd : R) = (↑d : R)

Tactic:
rw [← f.map_mul, dmuld, map_intCast]

Premises used: map_intCast, RingHom.map_mul, Zsqrtd.dmuld
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
R : Type u_1
inst : CommRing R
d : ℤ
r : { r : R // r * r = (↑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) }))
      ((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))
        r) =
    r

Tactic:
simp
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
R : Type u_1
inst : CommRing R
d : ℤ
f : ℤ√d →+* R
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' := ⋯, 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) :
          (a : ℤ√d) → R)
        sqrtd :
      R)
    ((f : (a : ℤ√d) → R) sqrtd : 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

Tactic:
ext
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
R : Type u_1
inst : CommRing R
d : ℤ
f : ℤ√d →+* R
⊢ Eq (α := 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) :
          (a : ℤ√d) → R)
        sqrtd :
      R)
    ((f : (a : ℤ√d) → R) sqrtd : R)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
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)
⊢ Function.Injective.{1, u_1 + 1} (β := R) Int.cast

Tactic:
have h_inj : Function.Injective ((↑) : ℤ → R) := Int.cast_injective
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
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)
⊢ 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

Premises used: Int.cast_zero, MulZeroClass.zero_mul, Zsqrtd.re_intCast, Zsqrtd.lift_apply_apply, Zsqrtd.im_intCast, add_zero
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
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
rwa : ∀ (this : Eq.{u_1 + 1} (α := R) (↑a.norm : R) (↑0 : R)), a = 0
rwa₁ : ∀ (this : a.norm = 0), a = 0
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (this : a = 0), a = 0
⊢ a = 0

Tactic:
rwa [← Int.cast_zero, h_inj.eq_iff, norm_eq_zero hd] at this

Premises used: Zsqrtd.norm_eq_zero, Int.cast_zero, Function.Injective.eq_iff
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
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
suffices :
  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

Tactic:
suffices lift r a.norm = 0 by
      simp only [re_intCast, add_zero, lift_apply_apply, im_intCast, Int.cast_zero,
        zero_mul] at this
      rwa [← Int.cast_zero, h_inj.eq_iff, norm_eq_zero hd] at this
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
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
rw :
  Eq (α := R)
    ((((lift : (a : { r : R // r * r = (↑d : R) }) → ℤ√d →+* R) r : ℤ√d →+* R) : (a : ℤ√d) → R) (a * star a) : R)
    (0 : R)
rw₁ :
  HMul.hMul (α := R) (β := R)
      ((((lift : (a : { r : R // r * r = (↑d : R) }) → ℤ√d →+* R) r : ℤ√d →+* R) : (a : ℤ√d) → R) a : R)
      ((((lift : (a : { r : R // r * r = (↑d : R) }) → ℤ√d →+* R) r : ℤ√d →+* R) : (a : ℤ√d) → R) (star a) : R) =
    0
rw₂ :
  HMul.hMul (α := R) (β := R) (0 : R)
      ((((lift : (a : { r : R // r * r = (↑d : R) }) → ℤ√d →+* R) r : ℤ√d →+* R) : (a : ℤ√d) → R) (star a) : R) =
    0
rw₃ rw₄ : Eq.{u_1 + 1} (α := R) 0 0
⊢ Eq (α := R)
    ((((lift : (a : { r : R // r * r = (↑d : R) }) → ℤ√d →+* R) r : ℤ√d →+* R) : (a : ℤ√d) → R) (↑a.norm : ℤ√d) : R)
    (0 : R)

Tactic:
rw [norm_eq_mul_conj, map_mul, ha, zero_mul]

Premises used: MulZeroClass.zero_mul, Zsqrtd.norm_eq_mul_conj, map_mul
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a : ℤ√d
rw : a.norm = 1 ↔ Eq (α := ℤ√d) (↑a.norm : ℤ√d) 1
⊢ a.norm = 1 ↔ Membership.mem (γ := Submonoid (ℤ√d)) (unitary (ℤ√d)) a

Tactic:
rw [Unitary.mem_iff_self_mul_star, ← norm_eq_mul_conj]

Premises used: Unitary.mem_iff_self_mul_star, Zsqrtd.norm_eq_mul_conj