awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
apply :
  Eq (α := ℕ → ℝ)
    (fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ) (↑n : ℝ) (HMul.hMul (α := ℕ) 2 1 + 1) * Real.sin (2 * π * (↑n : ℝ) * (1 / 4)))
    fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 3 * Real.sin (π * (↑n : ℝ) / 2)
apply₁ :
  HPow.hPow (α := ℝ) (-1) (HAdd.hAdd (α := ℕ) 1 1) * (2 * π) ^ (HMul.hMul (α := ℕ) 2 1 + 1) / 2 /
        (↑(HMul.hMul (α := ℕ) 2 1 + 1)! : ℝ) *
      Polynomial.eval (1 / 4) (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (HMul.hMul (α := ℕ) 2 1 + 1))) =
    HPow.hPow (β := ℕ) π 3 / 32
apply₂ : Membership.mem (γ := Set ℝ) (Icc 0 1) (1 / 4)
⊢ HasSum (fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 3 * Real.sin (π * (↑n : ℝ) / 2))
    (HPow.hPow (β := ℕ) π 3 / 32)

Tactic:
apply (congr_arg₂ HasSum ?_ ?_).to_iff.mp <|
    hasSum_one_div_nat_pow_mul_sin one_ne_zero (?_ : 1 / 4 ∈ Icc (0 : ℝ) 1)

Premises used: Eq.to_iff, HasSum, hasSum_one_div_nat_pow_mul_sin, Iff.mp, one_ne_zero, SummationFilter.unconditional, congr_arg₂
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
h :
  ∀ (n : ℕ),
    1 / HPow.hPow (α := ℝ) (↑n : ℝ) (HMul.hMul (α := ℕ) 2 1 + 1) * Real.sin (2 * π * (↑n : ℝ) * (1 / 4)) =
      1 / HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 3 * Real.sin (π * (↑n : ℝ) / 2)
⊢ Eq (α := ℕ → ℝ)
    (fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ) (↑n : ℝ) (HMul.hMul (α := ℕ) 2 1 + 1) * Real.sin (2 * π * (↑n : ℝ) * (1 / 4)))
    fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 3 * Real.sin (π * (↑n : ℝ) / 2)

Tactic:
ext1 n
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
n : ℕ
⊢ 1 / HPow.hPow (α := ℝ) (↑n : ℝ) (HMul.hMul (α := ℕ) 2 1 + 1) * Real.sin (2 * π * (↑n : ℝ) * (1 / 4)) =
    1 / HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 3 * Real.sin (π * (↑n : ℝ) / 2)

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
⊢ 1 / 4 = (algebraMap ℚ ℝ : (a : ℚ) → ℝ) (1 / 4)

Tactic:
simp
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
⊢ 1 / 4 = (algebraMap ℚ ℝ : (a : ℚ) → ℝ) (1 / 4)

Tactic:
have : (1 / 4 : ℝ) = (algebraMap ℚ ℝ) (1 / 4 : ℚ) := by simp
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
this : 1 / 4 = (algebraMap ℚ ℝ : (a : ℚ) → ℝ) (1 / 4)
⊢ HMul.hMul (α := ℕ) 2 1 + 1 = 3

Tactic:
decide
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
this : 1 / 4 = (algebraMap ℚ ℝ : (a : ℚ) → ℝ) (1 / 4)
rw :
  HMul.hMul (β := ℝ)
      (HPow.hPow (α := ℝ) (-1) (HAdd.hAdd (α := ℕ) 1 1) * (HPow.hPow (α := ℝ) (β := ℕ) 2 3 * HPow.hPow (β := ℕ) π 3) /
          2 /
        (↑3! : ℝ))
      ((algebraMap ℚ ℝ : (a : ℚ) → ℝ) (3 / 64) : ℝ) =
    HPow.hPow (β := ℕ) π 3 / 32
⊢ HPow.hPow (α := ℝ) (-1) (HAdd.hAdd (α := ℕ) 1 1) * (2 * π) ^ (HMul.hMul (α := ℕ) 2 1 + 1) / 2 /
        (↑(HMul.hMul (α := ℕ) 2 1 + 1)! : ℝ) *
      Polynomial.eval (1 / 4) (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (HMul.hMul (α := ℕ) 2 1 + 1))) =
    HPow.hPow (β := ℕ) π 3 / 32

Tactic:
rw [this, mul_pow, Polynomial.eval_map, Polynomial.eval₂_at_apply, (by decide : 2 * 1 + 1 = 3),
      Polynomial.bernoulli_three_eval_one_quarter]

Premises used: Polynomial.eval_map, Polynomial.eval₂_at_apply, mul_pow, Polynomial.bernoulli_three_eval_one_quarter
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
this : 1 / 4 = (algebraMap ℚ ℝ : (a : ℚ) → ℝ) (1 / 4)
simp :
  HPow.hPow (α := ℝ) (β := ℕ) 2 3 * HPow.hPow (β := ℕ) π 3 / 2 / 6 * HDiv.hDiv (α := ℝ) 3 64 =
    HPow.hPow (β := ℕ) π 3 / 32
⊢ HMul.hMul (β := ℝ)
      (HPow.hPow (α := ℝ) (-1) (HAdd.hAdd (α := ℕ) 1 1) * (HPow.hPow (α := ℝ) (β := ℕ) 2 3 * HPow.hPow (β := ℕ) π 3) /
          2 /
        (↑3! : ℝ))
      ((algebraMap ℚ ℝ : (a : ℚ) → ℝ) (3 / 64) : ℝ) =
    HPow.hPow (β := ℕ) π 3 / 32

Tactic:
simp [Nat.factorial]

Premises used: Nat.factorial
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
this : 1 / 4 = (algebraMap ℚ ℝ : (a : ℚ) → ℝ) (1 / 4)
⊢ HPow.hPow (α := ℝ) (β := ℕ) 2 3 * HPow.hPow (β := ℕ) π 3 / 2 / 6 * HDiv.hDiv (α := ℝ) 3 64 =
    HPow.hPow (β := ℕ) π 3 / 32

Tactic:
ring
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
left : 0 ≤ 1 / 4
right : 1 / 4 ≤ 1
⊢ 0 ≤ 1 / 4 ∧ 1 / 4 ≤ 1

Tactic:
constructor
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
linarith : 1 / 4 < 0 → 4 / 4 = 1
linarith₁ : 1 / 4 < 0 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₂ : 1 / 4 < 0 → GT.gt (α := ℝ) 4 0
linarith₃ : 1 / 4 < 0 → -1 + HMul.hMul (α := ℝ) 1 1 = 0
⊢ 0 ≤ 1 / 4

Tactic:
linarith
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
linarith : 1 < 1 / 4 → 4 / 4 = 1
linarith₁ : 1 < 1 / 4 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₂ : 1 < 1 / 4 → GT.gt (α := ℝ) 4 0
linarith₃ : 1 < 1 / 4 → HMul.hMul (α := ℝ) 3 (-1) + HMul.hMul (α := ℝ) 1 3 = 0
linarith₄ : 1 < 1 / 4 → GT.gt (α := ℝ) 3 0
⊢ 1 / 4 ≤ 1

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d n : ℤ
⊢ re (d := d) (ofInt n) = n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d n : ℤ
⊢ im (d := d) (ofInt n) = 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
⊢ re (d := d) 0 = 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
⊢ im (d := d) 0 = 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
⊢ re (d := d) 1 = 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
⊢ im (d := d) 1 = 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
⊢ re (d := d) sqrtd = 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
⊢ im (d := d) sqrtd = 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y x' y' : ℤ
⊢ HAdd.hAdd (α := ℤ√d) { re := x, im := y : ℤ√d } { re := x', im := y' : ℤ√d } = { re := x + x', im := y + y' }

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
z w : ℤ√d
⊢ (z + w).re = z.re + w.re

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
z w : ℤ√d
⊢ (z + w).im = z.im + w.im

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
z : ℤ√d
⊢ (-z).re = -z.re

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
z : ℤ√d
⊢ (-z).im = -z.im

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
z w : ℤ√d
⊢ (z * w).re = z.re * w.re + d * z.im * w.im

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
z w : ℤ√d
⊢ (z * w).im = z.re * w.im + z.im * w.re

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
refine_1 : ∀ (a b c : ℤ√d), a + b + c = a + (b + c)
refine_2 : ∀ (a : ℤ√d), 0 + a = a
refine_3 : ∀ (a : ℤ√d), a + 0 = a
refine_4 : ∀ (a : ℤ√d), -a + a = 0
refine_5 : ∀ (a b : ℤ√d), a + b = b + a
⊢ AddCommGroup (ℤ√d)

Tactic:
refine
  { sub := fun a b => a + -b
    nsmul := @nsmulRec (ℤ√d) ⟨0⟩ ⟨(· + ·)⟩
    zsmul := @zsmulRec (ℤ√d) ⟨0⟩ ⟨(· + ·)⟩ ⟨Neg.neg⟩ (@nsmulRec (ℤ√d) ⟨0⟩ ⟨(· + ·)⟩)
    add_assoc := ?_
    zero_add := ?_
    add_zero := ?_
    neg_add_cancel := ?_
    add_comm := ?_ }
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a b c : ℤ√d
refine_1 : (a + b + c).re = (a + (b + c)).re
refine_1₁ : (a + b + c).im = (a + (b + c)).im
⊢ a + b + c = a + (b + c)

Tactic:
ext
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a : ℤ√d
refine_2 : (0 + a).re = a.re
refine_2₁ : (0 + a).im = a.im
⊢ 0 + a = a

Tactic:
ext
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a : ℤ√d
refine_3 : (a + 0).re = a.re
refine_3₁ : (a + 0).im = a.im
⊢ a + 0 = a

Tactic:
ext
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a : ℤ√d
refine_4 : (-a + a).re = re (d := d) 0
refine_4₁ : (-a + a).im = im (d := d) 0
⊢ -a + a = 0

Tactic:
ext
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a b : ℤ√d
refine_5 : (a + b).re = (b + a).re
refine_5₁ : (a + b).im = (b + a).im
⊢ a + b = b + a

Tactic:
ext
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a b c : ℤ√d
⊢ (a + b + c).re = (a + (b + c)).re

Tactic:
simp [add_comm, add_left_comm]

Premises used: add_left_comm, add_comm
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a b c : ℤ√d
⊢ (a + b + c).im = (a + (b + c)).im

Tactic:
simp [add_comm, add_left_comm]

Premises used: add_left_comm, add_comm
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a : ℤ√d
⊢ (0 + a).re = a.re

Tactic:
simp [add_comm, add_left_comm]

Premises used: add_left_comm, add_comm
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a : ℤ√d
⊢ (0 + a).im = a.im

Tactic:
simp [add_comm, add_left_comm]

Premises used: add_left_comm, add_comm
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a : ℤ√d
⊢ (a + 0).re = a.re

Tactic:
simp [add_comm, add_left_comm]

Premises used: add_left_comm, add_comm
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a : ℤ√d
⊢ (a + 0).im = a.im

Tactic:
simp [add_comm, add_left_comm]

Premises used: add_left_comm, add_comm
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a : ℤ√d
⊢ (-a + a).re = re (d := d) 0

Tactic:
simp [add_comm, add_left_comm]

Premises used: add_left_comm, add_comm
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a : ℤ√d
⊢ (-a + a).im = im (d := d) 0

Tactic:
simp [add_comm, add_left_comm]

Premises used: add_left_comm, add_comm
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a b : ℤ√d
⊢ (a + b).re = (b + a).re

Tactic:
simp [add_comm, add_left_comm]

Premises used: add_left_comm, add_comm
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a b : ℤ√d
⊢ (a + b).im = (b + a).im

Tactic:
simp [add_comm, add_left_comm]

Premises used: add_left_comm, add_comm
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
z w : ℤ√d
⊢ (z - w).re = z.re - w.re

Tactic:
rfl

Premises used: Int.sub, rfl
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
z w : ℤ√d
⊢ (z - w).im = z.im - w.im

Tactic:
rfl

Premises used: Int.sub, rfl
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
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
refine_9 : ∀ (a b : ℤ√d), a * b = b * a
⊢ CommRing (ℤ√d)

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 := ?_ }

Premises used: Zsqrtd.addGroupWithOne
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a b : ℤ√d
refine_1 : (a + b).re = (b + a).re
refine_1₁ : (a + b).im = (b + a).im
⊢ a + b = b + a

Tactic:
ext
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a b c : ℤ√d
refine_2 : (a * b * c).re = (a * (b * c)).re
refine_2₁ : (a * b * c).im = (a * (b * c)).im
⊢ a * b * c = a * (b * c)

Tactic:
ext
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a : ℤ√d
refine_3 : (1 * a).re = a.re
refine_3₁ : (1 * a).im = a.im
⊢ 1 * a = a

Tactic:
ext
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a : ℤ√d
refine_4 : (a * 1).re = a.re
refine_4₁ : (a * 1).im = a.im
⊢ a * 1 = a

Tactic:
ext
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a : ℤ√d
refine_5 : (0 * a).re = re (d := d) 0
refine_5₁ : (0 * a).im = im (d := d) 0
⊢ 0 * a = 0

Tactic:
ext
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a : ℤ√d
refine_6 : (a * 0).re = re (d := d) 0
refine_6₁ : (a * 0).im = im (d := d) 0
⊢ a * 0 = 0

Tactic:
ext
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a b c : ℤ√d
refine_7 : (a * (b + c)).re = (a * b + a * c).re
refine_7₁ : (a * (b + c)).im = (a * b + a * c).im
⊢ a * (b + c) = a * b + a * c

Tactic:
ext
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a b c : ℤ√d
refine_8 : ((a + b) * c).re = (a * c + b * c).re
refine_8₁ : ((a + b) * c).im = (a * c + b * c).im
⊢ (a + b) * c = a * c + b * c

Tactic:
ext
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a b : ℤ√d
refine_9 : (a * b).re = (b * a).re
refine_9₁ : (a * b).im = (b * a).im
⊢ a * b = b * a

Tactic:
ext
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a : ℤ√d
⊢ (1 * a).re = a.re

Tactic:
simp
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a : ℤ√d
⊢ (1 * a).im = a.im

Tactic:
simp
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a : ℤ√d
⊢ (a * 1).re = a.re

Tactic:
simp
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a : ℤ√d
⊢ (a * 1).im = a.im

Tactic:
simp
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a : ℤ√d
⊢ (0 * a).re = re (d := d) 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a : ℤ√d
⊢ (0 * a).im = im (d := d) 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a : ℤ√d
⊢ (a * 0).re = re (d := d) 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a : ℤ√d
⊢ (a * 0).im = im (d := d) 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a b : ℤ√d
⊢ a.re + b.re = b.re + a.re

Tactic:
ring
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a b : ℤ√d
⊢ a.im + b.im = b.im + a.im

Tactic:
ring
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a b c : ℤ√d
⊢ (a.re * b.re + d * a.im * b.im) * c.re + d * (a.re * b.im + a.im * b.re) * c.im =
    a.re * (b.re * c.re + d * b.im * c.im) + d * a.im * (b.re * c.im + b.im * c.re)

Tactic:
ring
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a b c : ℤ√d
⊢ (a.re * b.re + d * a.im * b.im) * c.im + (a.re * b.im + a.im * b.re) * c.re =
    a.re * (b.re * c.im + b.im * c.re) + a.im * (b.re * c.re + d * b.im * c.im)

Tactic:
ring
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a b c : ℤ√d
⊢ a.re * (b.re + c.re) + d * a.im * (b.im + c.im) = a.re * b.re + d * a.im * b.im + (a.re * c.re + d * a.im * c.im)

Tactic:
ring
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a b c : ℤ√d
⊢ a.re * (b.im + c.im) + a.im * (b.re + c.re) = a.re * b.im + a.im * b.re + (a.re * c.im + a.im * c.re)

Tactic:
ring
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a b c : ℤ√d
⊢ (a.re + b.re) * c.re + d * (a.im + b.im) * c.im = a.re * c.re + d * a.im * c.im + (b.re * c.re + d * b.im * c.im)

Tactic:
ring
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a b c : ℤ√d
⊢ (a.re + b.re) * c.im + (a.im + b.im) * c.re = a.re * c.im + a.im * c.re + (b.re * c.im + b.im * c.re)

Tactic:
ring
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a b : ℤ√d
⊢ a.re * b.re + d * a.im * b.im = b.re * a.re + d * b.im * a.im

Tactic:
ring
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a b : ℤ√d
⊢ a.re * b.im + a.im * b.re = b.re * a.im + b.im * a.re

Tactic:
ring
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
⊢ AddMonoid (ℤ√d)

Tactic:
infer_instance
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
⊢ Monoid (ℤ√d)

Tactic:
infer_instance
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
⊢ CommMonoid (ℤ√d)

Tactic:
infer_instance
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
⊢ CommSemigroup (ℤ√d)

Tactic:
infer_instance
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
⊢ Semigroup (ℤ√d)

Tactic:
infer_instance
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
⊢ AddCommSemigroup (ℤ√d)

Tactic:
infer_instance
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
⊢ AddSemigroup (ℤ√d)

Tactic:
infer_instance
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
⊢ CommSemiring (ℤ√d)

Tactic:
infer_instance
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
⊢ Semiring (ℤ√d)

Tactic:
infer_instance
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
⊢ Ring (ℤ√d)

Tactic:
infer_instance
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
⊢ Distrib (ℤ√d)

Tactic:
infer_instance
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y : ℤ
⊢ Eq (α := ℤ√d) (star { re := x, im := y }) { re := x, im := -y }

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
z : ℤ√d
⊢ (star z).re = z.re

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
z : ℤ√d
⊢ (star z).im = -z.im

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a b : ℤ√d
re : (star (a * b)).re = (star b * star a).re
im : (star (a * b)).im = (star b * star a).im
⊢ star (a * b) = star b * star a

Tactic:
ext
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a b : ℤ√d
re : a.re * b.re + d * a.im * b.im = b.re * a.re + d * b.im * a.im
⊢ (star (a * b)).re = (star b * star a).re

Tactic:
simp
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a b : ℤ√d
im : -(a.im * b.re) + -(a.re * b.im) = -(b.re * a.im) + -(b.im * a.re)
⊢ (star (a * b)).im = (star b * star a).im

Tactic:
simp
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a b : ℤ√d
⊢ -(a.im * b.re) + -(a.re * b.im) = -(b.re * a.im) + -(b.im * a.re)

Tactic:
ring
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
⊢ ¬(re (d := d) 0 = re (d := d) 1 ∧ im (d := d) 0 = im (d := d) 1)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
n : ℕ
⊢ re (d := d) (↑n : ℤ√d) = (↑n : ℤ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
n : ℕ
inst : n.AtLeastTwo
⊢ re (d := d) (OfNat.ofNat n) = (↑n : ℤ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
n : ℕ
⊢ im (d := d) (↑n : ℤ√d) = 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
n : ℕ
inst : n.AtLeastTwo
⊢ im (d := d) (OfNat.ofNat n) = 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
n : ℕ
⊢ Eq (α := ℤ√d) (↑n : ℤ√d) { re := (↑n : ℤ), im := 0 }

Tactic:
rfl

Premises used: Zsqrtd.ofInt, rfl
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d n : ℤ
ofNat : ∀ (a : ℕ), re (d := d) (↑(Int.ofNat a) : ℤ√d) = Int.ofNat a
negSucc : ∀ (a : ℕ), re (d := d) (↑(Int.negSucc a) : ℤ√d) = Int.negSucc a
⊢ re (d := d) (↑n : ℤ√d) = n

Tactic:
cases n
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a : ℕ
⊢ re (d := d) (↑(Int.ofNat a) : ℤ√d) = Int.ofNat a

Tactic:
rfl
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a : ℕ
⊢ re (d := d) (↑(Int.negSucc a) : ℤ√d) = Int.negSucc a

Tactic:
rfl
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d n : ℤ
ofNat : ∀ (a : ℕ), im (d := d) (↑(Int.ofNat a) : ℤ√d) = 0
negSucc : ∀ (a : ℕ), im (d := d) (↑(Int.negSucc a) : ℤ√d) = 0
⊢ im (d := d) (↑n : ℤ√d) = 0

Tactic:
cases n
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a : ℕ
⊢ im (d := d) (↑(Int.ofNat a) : ℤ√d) = 0

Tactic:
rfl
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a : ℕ
⊢ im (d := d) (↑(Int.negSucc a) : ℤ√d) = 0

Tactic:
rfl
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d n : ℤ
re : Zsqrtd.re (d := d) (↑n : ℤ√d) = Zsqrtd.re (d := d) { re := n, im := 0 }
im : Zsqrtd.im (d := d) (↑n : ℤ√d) = Zsqrtd.im (d := d) { re := n, im := 0 }
⊢ Eq (α := ℤ√d) (↑n : ℤ√d) { re := n, im := 0 }

Tactic:
ext
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d n : ℤ
⊢ re (d := d) (↑n : ℤ√d) = re (d := d) { re := n, im := 0 }

Tactic:
simp
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d n : ℤ
⊢ im (d := d) (↑n : ℤ√d) = im (d := d) { re := n, im := 0 }

Tactic:
simp
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
m n : ℕ
⊢ Eq (α := ℤ√d) (↑m : ℤ√d) (↑n : ℤ√d) → m = n

Tactic:
simp [Zsqrtd.ext_iff]

Premises used: Zsqrtd.ext_iff
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d n : ℤ
re : Zsqrtd.re (d := d) (ofInt n) = Zsqrtd.re (d := d) (↑n : ℤ√d)
im : Zsqrtd.im (d := d) (ofInt n) = Zsqrtd.im (d := d) (↑n : ℤ√d)
⊢ Eq (α := ℤ√d) (ofInt n) (↑n : ℤ√d)

Tactic:
ext
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d n : ℤ
⊢ re (d := d) (ofInt n) = re (d := d) (↑n : ℤ√d)

Tactic:
simp [re_ofInt, im_ofInt]

Premises used: Zsqrtd.re_ofInt, Zsqrtd.im_ofInt
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d n : ℤ
⊢ im (d := d) (ofInt n) = im (d := d) (↑n : ℤ√d)

Tactic:
simp [re_ofInt, im_ofInt]

Premises used: Zsqrtd.re_ofInt, Zsqrtd.im_ofInt
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
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 }
im :
  (HMul.hMul (α := ℤ√d) (↑n : ℤ√d) { re := x, im := y : ℤ√d }).im =
    Zsqrtd.im (d := d) { re := (↑n : ℤ) * x, im := (↑n : ℤ) * y }
⊢ HMul.hMul (α := ℤ√d) (↑n : ℤ√d) { re := x, im := y : ℤ√d } = { re := (↑n : ℤ) * x, im := (↑n : ℤ) * y }

Tactic:
ext
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
n : ℕ
x y : ℤ
⊢ (HMul.hMul (α := ℤ√d) (↑n : ℤ√d) { re := x, im := y : ℤ√d }).re =
    re (d := d) { re := (↑n : ℤ) * x, im := (↑n : ℤ) * y }

Tactic:
simp
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
n : ℕ
x y : ℤ
⊢ (HMul.hMul (α := ℤ√d) (↑n : ℤ√d) { re := x, im := y : ℤ√d }).im =
    im (d := d) { re := (↑n : ℤ) * x, im := (↑n : ℤ) * y }

Tactic:
simp
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
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 }
im : (HMul.hMul (α := ℤ√d) (↑n : ℤ√d) { re := x, im := y : ℤ√d }).im = Zsqrtd.im (d := d) { re := n * x, im := n * y }
⊢ HMul.hMul (α := ℤ√d) (↑n : ℤ√d) { re := x, im := y : ℤ√d } = { re := n * x, im := n * y }

Tactic:
ext
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d n x y : ℤ
⊢ (HMul.hMul (α := ℤ√d) (↑n : ℤ√d) { re := x, im := y : ℤ√d }).re = re (d := d) { re := n * x, im := n * y }

Tactic:
simp
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d n x y : ℤ
⊢ (HMul.hMul (α := ℤ√d) (↑n : ℤ√d) { re := x, im := y : ℤ√d }).im = im (d := d) { re := n * x, im := n * y }

Tactic:
simp
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d a : ℤ
b : ℤ√d
⊢ ((↑a : ℤ√d) * b).re = a * b.re

Tactic:
simp
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d a : ℤ
b : ℤ√d
⊢ ((↑a : ℤ√d) * b).im = a * b.im

Tactic:
simp
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y : ℤ
re : (HMul.hMul (α := ℤ√d) sqrtd { re := x, im := y : ℤ√d }).re = Zsqrtd.re (d := d) { re := d * y, im := x }
im : (HMul.hMul (α := ℤ√d) sqrtd { re := x, im := y : ℤ√d }).im = Zsqrtd.im (d := d) { re := d * y, im := x }
⊢ HMul.hMul (α := ℤ√d) sqrtd { re := x, im := y : ℤ√d } = { re := d * y, im := x }

Tactic:
ext
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y : ℤ
⊢ (HMul.hMul (α := ℤ√d) sqrtd { re := x, im := y : ℤ√d }).re = re (d := d) { re := d * y, im := x }

Tactic:
simp
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d x y : ℤ
⊢ (HMul.hMul (α := ℤ√d) sqrtd { re := x, im := y : ℤ√d }).im = im (d := d) { re := d * y, im := x }

Tactic:
simp
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
re : (HMul.hMul (α := ℤ√d) sqrtd sqrtd).re = Zsqrtd.re (d := d) (↑d : ℤ√d)
im : (HMul.hMul (α := ℤ√d) sqrtd sqrtd).im = Zsqrtd.im (d := d) (↑d : ℤ√d)
⊢ HMul.hMul (α := ℤ√d) sqrtd sqrtd = (↑d : ℤ√d)

Tactic:
ext
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
⊢ (HMul.hMul (α := ℤ√d) sqrtd sqrtd).re = re (d := d) (↑d : ℤ√d)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
⊢ (HMul.hMul (α := ℤ√d) sqrtd sqrtd).im = im (d := d) (↑d : ℤ√d)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
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 }
im :
  (HMul.hMul (α := ℤ√d) sqrtd (↑n : ℤ√d) * { re := x, im := y : ℤ√d }).im =
    Zsqrtd.im (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 }

Tactic:
ext
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d n x y : ℤ
⊢ (HMul.hMul (α := ℤ√d) sqrtd (↑n : ℤ√d) * { re := x, im := y : ℤ√d }).re = re (d := d) { re := d * n * y, im := n * x }

Tactic:
simp
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d n x y : ℤ
⊢ (HMul.hMul (α := ℤ√d) sqrtd (↑n : ℤ√d) * { re := x, im := y : ℤ√d }).im = im (d := d) { re := d * n * y, im := n * x }

Tactic:
simp