[GOAL]
d x y x' y' : ℤ
h : { re := x, im := y } = { re := x', im := y' }
⊢ { re := x, im := y }.re = { re := x', im := y' }.re ∧ { re := x, im := y }.im = { re := x', im := y' }.im
[PROOFSTEP]
injection h
[GOAL]
d x y x' y' : ℤ
re_eq✝ : x = x'
im_eq✝ : y = y'
⊢ { re := x, im := y }.re = { re := x', im := y' }.re ∧ { re := x, im := y }.im = { re := x', im := y' }.im
[PROOFSTEP]
constructor
[GOAL]
case left
d x y x' y' : ℤ
re_eq✝ : x = x'
im_eq✝ : y = y'
⊢ { re := x, im := y }.re = { re := x', im := y' }.re
[PROOFSTEP]
assumption
[GOAL]
case right
d x y x' y' : ℤ
re_eq✝ : x = x'
im_eq✝ : y = y'
⊢ { re := x, im := y }.im = { re := x', im := y' }.im
[PROOFSTEP]
assumption
[GOAL]
d x y x' y' : ℤ
x✝ : { re := x, im := y }.re = { re := x', im := y' }.re ∧ { re := x, im := y }.im = { re := x', im := y' }.im
h₁ : { re := x, im := y }.re = { re := x', im := y' }.re
h₂ : { re := x, im := y }.im = { re := x', im := y' }.im
⊢ { re := x, im := y } = { re := x', im := y' }
[PROOFSTEP]
congr
[GOAL]
d : ℤ
z : ℤ√d
⊢ (bit1 z).im = bit0 z.im
[PROOFSTEP]
simp [bit1]
[GOAL]
d : ℤ
⊢ AddCommGroup (ℤ√d)
[PROOFSTEP]
refine
  { add := (· + ·)
    zero := (0 : ℤ√d)
    sub := fun a b => a + -b
    neg := Neg.neg
    zsmul := @zsmulRec (ℤ√d) ⟨0⟩ ⟨(· + ·)⟩ ⟨Neg.neg⟩
    nsmul := @nsmulRec (ℤ√d) ⟨0⟩ ⟨(· + ·)⟩
    add_assoc := ?_
    zero_add := ?_
    add_zero := ?_
    add_left_neg := ?_
    add_comm := ?_ }
[GOAL]
case refine_1
d : ℤ
⊢ ∀ (a b c : ℤ√d), a + b + c = a + (b + c)
[PROOFSTEP]
intros
[GOAL]
case refine_2
d : ℤ
⊢ ∀ (a : ℤ√d), 0 + a = a
[PROOFSTEP]
intros
[GOAL]
case refine_3
d : ℤ
⊢ ∀ (a : ℤ√d), a + 0 = a
[PROOFSTEP]
intros
[GOAL]
case refine_4
d : ℤ
⊢ ∀ (a : ℤ√d), -a + a = 0
[PROOFSTEP]
intros
[GOAL]
case refine_5
d : ℤ
⊢ ∀ (a b : ℤ√d), a + b = b + a
[PROOFSTEP]
intros
[GOAL]
case refine_1
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ a✝ + b✝ + c✝ = a✝ + (b✝ + c✝)
[PROOFSTEP]
simp [ext, add_comm, add_left_comm]
[GOAL]
case refine_2
d : ℤ
a✝ : ℤ√d
⊢ 0 + a✝ = a✝
[PROOFSTEP]
simp [ext, add_comm, add_left_comm]
[GOAL]
case refine_3
d : ℤ
a✝ : ℤ√d
⊢ a✝ + 0 = a✝
[PROOFSTEP]
simp [ext, add_comm, add_left_comm]
[GOAL]
case refine_4
d : ℤ
a✝ : ℤ√d
⊢ -a✝ + a✝ = 0
[PROOFSTEP]
simp [ext, add_comm, add_left_comm]
[GOAL]
case refine_5
d : ℤ
a✝ b✝ : ℤ√d
⊢ a✝ + b✝ = b✝ + a✝
[PROOFSTEP]
simp [ext, add_comm, add_left_comm]
[GOAL]
d : ℤ
⊢ CommRing (ℤ√d)
[PROOFSTEP]
refine
  { Zsqrtd.addGroupWithOne with
    add := (· + ·)
    zero := (0 : ℤ√d)
    mul := (· * ·)
    one := 1
    npow := @npowRec (ℤ√d) ⟨1⟩ ⟨(· * ·)⟩, add_comm := ?_
    left_distrib := ?_
    right_distrib := ?_
    zero_mul := ?_
    mul_zero := ?_
    mul_assoc := ?_
    one_mul := ?_
    mul_one := ?_
    mul_comm := ?_ }
[GOAL]
case refine_1
d : ℤ
src✝ : AddGroupWithOne (ℤ√d) := addGroupWithOne
⊢ ∀ (a b : ℤ√d), a + b = b + a
[PROOFSTEP]
intros
[GOAL]
case refine_2
d : ℤ
src✝ : AddGroupWithOne (ℤ√d) := addGroupWithOne
⊢ ∀ (a b c : ℤ√d), a * (b + c) = a * b + a * c
[PROOFSTEP]
intros
[GOAL]
case refine_3
d : ℤ
src✝ : AddGroupWithOne (ℤ√d) := addGroupWithOne
⊢ ∀ (a b c : ℤ√d), (a + b) * c = a * c + b * c
[PROOFSTEP]
intros
[GOAL]
case refine_4
d : ℤ
src✝ : AddGroupWithOne (ℤ√d) := addGroupWithOne
⊢ ∀ (a : ℤ√d), 0 * a = 0
[PROOFSTEP]
intros
[GOAL]
case refine_5
d : ℤ
src✝ : AddGroupWithOne (ℤ√d) := addGroupWithOne
⊢ ∀ (a : ℤ√d), a * 0 = 0
[PROOFSTEP]
intros
[GOAL]
case refine_6
d : ℤ
src✝ : AddGroupWithOne (ℤ√d) := addGroupWithOne
⊢ ∀ (a b c : ℤ√d), a * b * c = a * (b * c)
[PROOFSTEP]
intros
[GOAL]
case refine_7
d : ℤ
src✝ : AddGroupWithOne (ℤ√d) := addGroupWithOne
⊢ ∀ (a : ℤ√d), 1 * a = a
[PROOFSTEP]
intros
[GOAL]
case refine_8
d : ℤ
src✝ : AddGroupWithOne (ℤ√d) := addGroupWithOne
⊢ ∀ (a : ℤ√d), a * 1 = a
[PROOFSTEP]
intros
[GOAL]
case refine_9
d : ℤ
src✝ : AddGroupWithOne (ℤ√d) := addGroupWithOne
⊢ ∀ (a b : ℤ√d), a * b = b * a
[PROOFSTEP]
intros
[GOAL]
case refine_1
d : ℤ
src✝ : AddGroupWithOne (ℤ√d) := addGroupWithOne
a✝ b✝ : ℤ√d
⊢ a✝ + b✝ = b✝ + a✝
[PROOFSTEP]
refine ext.mpr ⟨?_, ?_⟩
[GOAL]
case refine_2
d : ℤ
src✝ : AddGroupWithOne (ℤ√d) := addGroupWithOne
a✝ b✝ c✝ : ℤ√d
⊢ a✝ * (b✝ + c✝) = a✝ * b✝ + a✝ * c✝
[PROOFSTEP]
refine ext.mpr ⟨?_, ?_⟩
[GOAL]
case refine_3
d : ℤ
src✝ : AddGroupWithOne (ℤ√d) := addGroupWithOne
a✝ b✝ c✝ : ℤ√d
⊢ (a✝ + b✝) * c✝ = a✝ * c✝ + b✝ * c✝
[PROOFSTEP]
refine ext.mpr ⟨?_, ?_⟩
[GOAL]
case refine_4
d : ℤ
src✝ : AddGroupWithOne (ℤ√d) := addGroupWithOne
a✝ : ℤ√d
⊢ 0 * a✝ = 0
[PROOFSTEP]
refine ext.mpr ⟨?_, ?_⟩
[GOAL]
case refine_5
d : ℤ
src✝ : AddGroupWithOne (ℤ√d) := addGroupWithOne
a✝ : ℤ√d
⊢ a✝ * 0 = 0
[PROOFSTEP]
refine ext.mpr ⟨?_, ?_⟩
[GOAL]
case refine_6
d : ℤ
src✝ : AddGroupWithOne (ℤ√d) := addGroupWithOne
a✝ b✝ c✝ : ℤ√d
⊢ a✝ * b✝ * c✝ = a✝ * (b✝ * c✝)
[PROOFSTEP]
refine ext.mpr ⟨?_, ?_⟩
[GOAL]
case refine_7
d : ℤ
src✝ : AddGroupWithOne (ℤ√d) := addGroupWithOne
a✝ : ℤ√d
⊢ 1 * a✝ = a✝
[PROOFSTEP]
refine ext.mpr ⟨?_, ?_⟩
[GOAL]
case refine_8
d : ℤ
src✝ : AddGroupWithOne (ℤ√d) := addGroupWithOne
a✝ : ℤ√d
⊢ a✝ * 1 = a✝
[PROOFSTEP]
refine ext.mpr ⟨?_, ?_⟩
[GOAL]
case refine_9
d : ℤ
src✝ : AddGroupWithOne (ℤ√d) := addGroupWithOne
a✝ b✝ : ℤ√d
⊢ a✝ * b✝ = b✝ * a✝
[PROOFSTEP]
refine ext.mpr ⟨?_, ?_⟩
[GOAL]
case refine_1.refine_1
d : ℤ
src✝ : AddGroupWithOne (ℤ√d) := addGroupWithOne
a✝ b✝ : ℤ√d
⊢ (a✝ + b✝).re = (b✝ + a✝).re
[PROOFSTEP]
simp
[GOAL]
case refine_1.refine_2
d : ℤ
src✝ : AddGroupWithOne (ℤ√d) := addGroupWithOne
a✝ b✝ : ℤ√d
⊢ (a✝ + b✝).im = (b✝ + a✝).im
[PROOFSTEP]
simp
[GOAL]
case refine_2.refine_1
d : ℤ
src✝ : AddGroupWithOne (ℤ√d) := addGroupWithOne
a✝ b✝ c✝ : ℤ√d
⊢ (a✝ * (b✝ + c✝)).re = (a✝ * b✝ + a✝ * c✝).re
[PROOFSTEP]
simp
[GOAL]
case refine_2.refine_2
d : ℤ
src✝ : AddGroupWithOne (ℤ√d) := addGroupWithOne
a✝ b✝ c✝ : ℤ√d
⊢ (a✝ * (b✝ + c✝)).im = (a✝ * b✝ + a✝ * c✝).im
[PROOFSTEP]
simp
[GOAL]
case refine_3.refine_1
d : ℤ
src✝ : AddGroupWithOne (ℤ√d) := addGroupWithOne
a✝ b✝ c✝ : ℤ√d
⊢ ((a✝ + b✝) * c✝).re = (a✝ * c✝ + b✝ * c✝).re
[PROOFSTEP]
simp
[GOAL]
case refine_3.refine_2
d : ℤ
src✝ : AddGroupWithOne (ℤ√d) := addGroupWithOne
a✝ b✝ c✝ : ℤ√d
⊢ ((a✝ + b✝) * c✝).im = (a✝ * c✝ + b✝ * c✝).im
[PROOFSTEP]
simp
[GOAL]
case refine_4.refine_1
d : ℤ
src✝ : AddGroupWithOne (ℤ√d) := addGroupWithOne
a✝ : ℤ√d
⊢ (0 * a✝).re = 0.re
[PROOFSTEP]
simp
[GOAL]
case refine_4.refine_2
d : ℤ
src✝ : AddGroupWithOne (ℤ√d) := addGroupWithOne
a✝ : ℤ√d
⊢ (0 * a✝).im = 0.im
[PROOFSTEP]
simp
[GOAL]
case refine_5.refine_1
d : ℤ
src✝ : AddGroupWithOne (ℤ√d) := addGroupWithOne
a✝ : ℤ√d
⊢ (a✝ * 0).re = 0.re
[PROOFSTEP]
simp
[GOAL]
case refine_5.refine_2
d : ℤ
src✝ : AddGroupWithOne (ℤ√d) := addGroupWithOne
a✝ : ℤ√d
⊢ (a✝ * 0).im = 0.im
[PROOFSTEP]
simp
[GOAL]
case refine_6.refine_1
d : ℤ
src✝ : AddGroupWithOne (ℤ√d) := addGroupWithOne
a✝ b✝ c✝ : ℤ√d
⊢ (a✝ * b✝ * c✝).re = (a✝ * (b✝ * c✝)).re
[PROOFSTEP]
simp
[GOAL]
case refine_6.refine_2
d : ℤ
src✝ : AddGroupWithOne (ℤ√d) := addGroupWithOne
a✝ b✝ c✝ : ℤ√d
⊢ (a✝ * b✝ * c✝).im = (a✝ * (b✝ * c✝)).im
[PROOFSTEP]
simp
[GOAL]
case refine_7.refine_1
d : ℤ
src✝ : AddGroupWithOne (ℤ√d) := addGroupWithOne
a✝ : ℤ√d
⊢ (1 * a✝).re = a✝.re
[PROOFSTEP]
simp
[GOAL]
case refine_7.refine_2
d : ℤ
src✝ : AddGroupWithOne (ℤ√d) := addGroupWithOne
a✝ : ℤ√d
⊢ (1 * a✝).im = a✝.im
[PROOFSTEP]
simp
[GOAL]
case refine_8.refine_1
d : ℤ
src✝ : AddGroupWithOne (ℤ√d) := addGroupWithOne
a✝ : ℤ√d
⊢ (a✝ * 1).re = a✝.re
[PROOFSTEP]
simp
[GOAL]
case refine_8.refine_2
d : ℤ
src✝ : AddGroupWithOne (ℤ√d) := addGroupWithOne
a✝ : ℤ√d
⊢ (a✝ * 1).im = a✝.im
[PROOFSTEP]
simp
[GOAL]
case refine_9.refine_1
d : ℤ
src✝ : AddGroupWithOne (ℤ√d) := addGroupWithOne
a✝ b✝ : ℤ√d
⊢ (a✝ * b✝).re = (b✝ * a✝).re
[PROOFSTEP]
simp
[GOAL]
case refine_9.refine_2
d : ℤ
src✝ : AddGroupWithOne (ℤ√d) := addGroupWithOne
a✝ b✝ : ℤ√d
⊢ (a✝ * b✝).im = (b✝ * a✝).im
[PROOFSTEP]
simp
[GOAL]
case refine_1.refine_1
d : ℤ
src✝ : AddGroupWithOne (ℤ√d) := addGroupWithOne
a✝ b✝ : ℤ√d
⊢ a✝.re + b✝.re = b✝.re + a✝.re
[PROOFSTEP]
ring
[GOAL]
case refine_1.refine_2
d : ℤ
src✝ : AddGroupWithOne (ℤ√d) := addGroupWithOne
a✝ b✝ : ℤ√d
⊢ a✝.im + b✝.im = b✝.im + a✝.im
[PROOFSTEP]
ring
[GOAL]
case refine_2.refine_1
d : ℤ
src✝ : AddGroupWithOne (ℤ√d) := addGroupWithOne
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)
[PROOFSTEP]
ring
[GOAL]
case refine_2.refine_2
d : ℤ
src✝ : AddGroupWithOne (ℤ√d) := addGroupWithOne
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)
[PROOFSTEP]
ring
[GOAL]
case refine_3.refine_1
d : ℤ
src✝ : AddGroupWithOne (ℤ√d) := addGroupWithOne
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)
[PROOFSTEP]
ring
[GOAL]
case refine_3.refine_2
d : ℤ
src✝ : AddGroupWithOne (ℤ√d) := addGroupWithOne
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)
[PROOFSTEP]
ring
[GOAL]
case refine_6.refine_1
d : ℤ
src✝ : AddGroupWithOne (ℤ√d) := addGroupWithOne
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)
[PROOFSTEP]
ring
[GOAL]
case refine_6.refine_2
d : ℤ
src✝ : AddGroupWithOne (ℤ√d) := addGroupWithOne
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)
[PROOFSTEP]
ring
[GOAL]
case refine_9.refine_1
d : ℤ
src✝ : AddGroupWithOne (ℤ√d) := addGroupWithOne
a✝ b✝ : ℤ√d
⊢ a✝.re * b✝.re + d * a✝.im * b✝.im = b✝.re * a✝.re + d * b✝.im * a✝.im
[PROOFSTEP]
ring
[GOAL]
case refine_9.refine_2
d : ℤ
src✝ : AddGroupWithOne (ℤ√d) := addGroupWithOne
a✝ b✝ : ℤ√d
⊢ a✝.re * b✝.im + a✝.im * b✝.re = b✝.re * a✝.im + b✝.im * a✝.re
[PROOFSTEP]
ring
[GOAL]
d : ℤ
⊢ AddMonoid (ℤ√d)
[PROOFSTEP]
infer_instance
[GOAL]
d : ℤ
⊢ Monoid (ℤ√d)
[PROOFSTEP]
infer_instance
[GOAL]
d : ℤ
⊢ CommMonoid (ℤ√d)
[PROOFSTEP]
infer_instance
[GOAL]
d : ℤ
⊢ CommSemigroup (ℤ√d)
[PROOFSTEP]
infer_instance
[GOAL]
d : ℤ
⊢ Semigroup (ℤ√d)
[PROOFSTEP]
infer_instance
[GOAL]
d : ℤ
⊢ AddCommSemigroup (ℤ√d)
[PROOFSTEP]
infer_instance
[GOAL]
d : ℤ
⊢ AddSemigroup (ℤ√d)
[PROOFSTEP]
infer_instance
[GOAL]
d : ℤ
⊢ CommSemiring (ℤ√d)
[PROOFSTEP]
infer_instance
[GOAL]
d : ℤ
⊢ Semiring (ℤ√d)
[PROOFSTEP]
infer_instance
[GOAL]
d : ℤ
⊢ Ring (ℤ√d)
[PROOFSTEP]
infer_instance
[GOAL]
d : ℤ
⊢ Distrib (ℤ√d)
[PROOFSTEP]
infer_instance
[GOAL]
d : ℤ
a b : ℤ√d
⊢ (star (a * b)).re = (star b * star a).re
[PROOFSTEP]
simp
[GOAL]
d : ℤ
a b : ℤ√d
⊢ a.re * b.re + d * a.im * b.im = b.re * a.re + d * b.im * a.im
[PROOFSTEP]
ring
[GOAL]
d : ℤ
a b : ℤ√d
⊢ (star (a * b)).im = (star b * star a).im
[PROOFSTEP]
simp
[GOAL]
d : ℤ
a b : ℤ√d
⊢ -(a.im * b.re) + -(a.re * b.im) = -(b.re * a.im) + -(b.im * a.re)
[PROOFSTEP]
ring
[GOAL]
d : ℤ
⊢ ¬(0.re = 1.re ∧ 0.im = 1.im)
[PROOFSTEP]
simp
[GOAL]
d n : ℤ
⊢ (↑n).re = n
[PROOFSTEP]
cases n
[GOAL]
case ofNat
d : ℤ
a✝ : ℕ
⊢ (↑(Int.ofNat a✝)).re = Int.ofNat a✝
[PROOFSTEP]
rfl
[GOAL]
case negSucc
d : ℤ
a✝ : ℕ
⊢ (↑(Int.negSucc a✝)).re = Int.negSucc a✝
[PROOFSTEP]
rfl
[GOAL]
d n : ℤ
⊢ (↑n).im = 0
[PROOFSTEP]
cases n
[GOAL]
case ofNat
d : ℤ
a✝ : ℕ
⊢ (↑(Int.ofNat a✝)).im = 0
[PROOFSTEP]
rfl
[GOAL]
case negSucc
d : ℤ
a✝ : ℕ
⊢ (↑(Int.negSucc a✝)).im = 0
[PROOFSTEP]
rfl
[GOAL]
d n : ℤ
⊢ ↑n = { re := n, im := 0 }
[PROOFSTEP]
simp [ext]
[GOAL]
d : ℤ
m n : ℕ
⊢ ↑m = ↑n → m = n
[PROOFSTEP]
simp [ext]
[GOAL]
d n : ℤ
⊢ ofInt n = ↑n
[PROOFSTEP]
simp [ext, ofInt_re, ofInt_im]
[GOAL]
d n x y : ℤ
⊢ ↑n * { re := x, im := y } = { re := n * x, im := n * y }
[PROOFSTEP]
simp [ext]
[GOAL]
d a : ℤ
b : ℤ√d
⊢ (↑a * b).re = a * b.re
[PROOFSTEP]
simp
[GOAL]
d a : ℤ
b : ℤ√d
⊢ (↑a * b).im = a * b.im
[PROOFSTEP]
simp
[GOAL]
d x y : ℤ
⊢ sqrtd * { re := x, im := y } = { re := d * y, im := x }
[PROOFSTEP]
simp [ext]
[GOAL]
d : ℤ
⊢ sqrtd * sqrtd = ↑d
[PROOFSTEP]
simp [ext]
[GOAL]
d n x y : ℤ
⊢ sqrtd * ↑n * { re := x, im := y } = { re := d * n * y, im := n * x }
[PROOFSTEP]
simp [ext]
[GOAL]
d x y : ℤ
⊢ { re := x, im := y } = ↑x + sqrtd * ↑y
[PROOFSTEP]
simp [ext]
[GOAL]
d x y : ℤ
⊢ { re := x, im := y } * star { re := x, im := y } = ↑x * ↑x - ↑d * ↑y * ↑y
[PROOFSTEP]
simp [ext, sub_eq_add_neg, mul_comm]
[GOAL]
d m n : ℤ
h : ↑m = ↑n
⊢ m = n
[PROOFSTEP]
simpa using congr_arg re h
[GOAL]
d z : ℤ
a : ℤ√d
⊢ ↑z ∣ a ↔ z ∣ a.re ∧ z ∣ a.im
[PROOFSTEP]
constructor
[GOAL]
case mp
d z : ℤ
a : ℤ√d
⊢ ↑z ∣ a → z ∣ a.re ∧ z ∣ a.im
[PROOFSTEP]
rintro ⟨x, rfl⟩
[GOAL]
case mp.intro
d z : ℤ
x : ℤ√d
⊢ z ∣ (↑z * x).re ∧ z ∣ (↑z * x).im
[PROOFSTEP]
simp only [add_zero, coe_int_re, zero_mul, mul_im, dvd_mul_right, and_self_iff, mul_re, mul_zero, coe_int_im]
[GOAL]
case mpr
d z : ℤ
a : ℤ√d
⊢ z ∣ a.re ∧ z ∣ a.im → ↑z ∣ a
[PROOFSTEP]
rintro ⟨⟨r, hr⟩, ⟨i, hi⟩⟩
[GOAL]
case mpr.intro.intro.intro
d z : ℤ
a : ℤ√d
r : ℤ
hr : a.re = z * r
i : ℤ
hi : a.im = z * i
⊢ ↑z ∣ a
[PROOFSTEP]
use⟨r, i⟩
[GOAL]
case h
d z : ℤ
a : ℤ√d
r : ℤ
hr : a.re = z * r
i : ℤ
hi : a.im = z * i
⊢ a = ↑z * { re := r, im := i }
[PROOFSTEP]
rw [smul_val, ext]
[GOAL]
case h
d z : ℤ
a : ℤ√d
r : ℤ
hr : a.re = z * r
i : ℤ
hi : a.im = z * i
⊢ a.re = { re := z * r, im := z * i }.re ∧ a.im = { re := z * r, im := z * i }.im
[PROOFSTEP]
exact ⟨hr, hi⟩
[GOAL]
d a b : ℤ
⊢ ↑a ∣ ↑b ↔ a ∣ b
[PROOFSTEP]
rw [coe_int_dvd_iff]
[GOAL]
d a b : ℤ
⊢ a ∣ (↑b).re ∧ a ∣ (↑b).im ↔ a ∣ b
[PROOFSTEP]
constructor
[GOAL]
case mp
d a b : ℤ
⊢ a ∣ (↑b).re ∧ a ∣ (↑b).im → a ∣ b
[PROOFSTEP]
rintro ⟨hre, -⟩
[GOAL]
case mp.intro
d a b : ℤ
hre : a ∣ (↑b).re
⊢ a ∣ b
[PROOFSTEP]
rwa [coe_int_re] at hre 
[GOAL]
case mpr
d a b : ℤ
⊢ a ∣ b → a ∣ (↑b).re ∧ a ∣ (↑b).im
[PROOFSTEP]
rw [coe_int_re, coe_int_im]
[GOAL]
case mpr
d a b : ℤ
⊢ a ∣ b → a ∣ b ∧ a ∣ 0
[PROOFSTEP]
exact fun hc => ⟨hc, dvd_zero a⟩
[GOAL]
d a : ℤ
b c : ℤ√d
ha : a ≠ 0
h : ↑a * b = ↑a * c
⊢ b = c
[PROOFSTEP]
rw [ext] at h ⊢
[GOAL]
d a : ℤ
b c : ℤ√d
ha : a ≠ 0
h : (↑a * b).re = (↑a * c).re ∧ (↑a * b).im = (↑a * c).im
⊢ b.re = c.re ∧ b.im = c.im
[PROOFSTEP]
apply And.imp _ _ h
[GOAL]
d a : ℤ
b c : ℤ√d
ha : a ≠ 0
h : (↑a * b).re = (↑a * c).re ∧ (↑a * b).im = (↑a * c).im
⊢ (↑a * b).re = (↑a * c).re → b.re = c.re
[PROOFSTEP]
simpa only [smul_re, smul_im] using mul_left_cancel₀ ha
[GOAL]
d a : ℤ
b c : ℤ√d
ha : a ≠ 0
h : (↑a * b).re = (↑a * c).re ∧ (↑a * b).im = (↑a * c).im
⊢ (↑a * b).im = (↑a * c).im → b.im = c.im
[PROOFSTEP]
simpa only [smul_re, smul_im] using mul_left_cancel₀ ha
[GOAL]
d : ℤ
a : ℤ√d
⊢ Int.gcd a.re a.im = 0 ↔ a = 0
[PROOFSTEP]
simp only [Int.gcd_eq_zero_iff, ext, eq_self_iff_true, zero_im, zero_re]
[GOAL]
d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
⊢ IsCoprime b.re b.im
[PROOFSTEP]
apply isCoprime_of_dvd
[GOAL]
case nonzero
d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
⊢ ¬(b.re = 0 ∧ b.im = 0)
[PROOFSTEP]
rintro ⟨hre, him⟩
[GOAL]
case nonzero.intro
d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
hre : b.re = 0
him : b.im = 0
⊢ False
[PROOFSTEP]
obtain rfl : b = 0 := by simp only [ext, hre, eq_self_iff_true, zero_im, him, and_self_iff, zero_re]
[GOAL]
d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
hre : b.re = 0
him : b.im = 0
⊢ b = 0
[PROOFSTEP]
simp only [ext, hre, eq_self_iff_true, zero_im, him, and_self_iff, zero_re]
[GOAL]
case nonzero.intro
d : ℤ
a : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : 0 ∣ a
hre : 0.re = 0
him : 0.im = 0
⊢ False
[PROOFSTEP]
rw [zero_dvd_iff] at hdvd 
[GOAL]
case nonzero.intro
d : ℤ
a : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : a = 0
hre : 0.re = 0
him : 0.im = 0
⊢ False
[PROOFSTEP]
simp [hdvd, zero_im, zero_re, not_isCoprime_zero_zero] at hcoprime 
[GOAL]
case H
d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
⊢ ∀ (z : ℤ), z ∈ nonunits ℤ → z ≠ 0 → z ∣ b.re → ¬z ∣ b.im
[PROOFSTEP]
rintro z hz - hzdvdu hzdvdv
[GOAL]
case H
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
[PROOFSTEP]
apply hz
[GOAL]
case H
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
[PROOFSTEP]
obtain ⟨ha, hb⟩ : z ∣ a.re ∧ z ∣ a.im := by
  rw [← coe_int_dvd_iff]
  apply dvd_trans _ hdvd
  rw [coe_int_dvd_iff]
  exact ⟨hzdvdu, hzdvdv⟩
[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
[PROOFSTEP]
rw [← coe_int_dvd_iff]
[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
[PROOFSTEP]
apply dvd_trans _ hdvd
[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 ∣ b
[PROOFSTEP]
rw [coe_int_dvd_iff]
[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 ∣ b.re ∧ z ∣ b.im
[PROOFSTEP]
exact ⟨hzdvdu, hzdvdv⟩
[GOAL]
case H.intro
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
hb : z ∣ a.im
⊢ IsUnit z
[PROOFSTEP]
exact hcoprime.isUnit_of_dvd' ha hb
[GOAL]
d : ℤ
a : ℤ√d
hgcd : 0 < Int.gcd a.re a.im
⊢ ∃ b, a = ↑↑(Int.gcd a.re a.im) * b ∧ IsCoprime b.re b.im
[PROOFSTEP]
obtain ⟨re, im, H1, Hre, Him⟩ := Int.exists_gcd_one hgcd
[GOAL]
case intro.intro.intro.intro
d : ℤ
a : ℤ√d
hgcd : 0 < Int.gcd a.re a.im
re im : ℤ
H1 : Int.gcd re im = 1
Hre : a.re = re * ↑(Int.gcd a.re a.im)
Him : a.im = im * ↑(Int.gcd a.re a.im)
⊢ ∃ b, a = ↑↑(Int.gcd a.re a.im) * b ∧ IsCoprime b.re b.im
[PROOFSTEP]
rw [mul_comm] at Hre Him 
[GOAL]
case intro.intro.intro.intro
d : ℤ
a : ℤ√d
hgcd : 0 < Int.gcd a.re a.im
re im : ℤ
H1 : Int.gcd re im = 1
Hre : a.re = ↑(Int.gcd a.re a.im) * re
Him : a.im = ↑(Int.gcd a.re a.im) * im
⊢ ∃ b, a = ↑↑(Int.gcd a.re a.im) * b ∧ IsCoprime b.re b.im
[PROOFSTEP]
refine' ⟨⟨re, im⟩, _, _⟩
[GOAL]
case intro.intro.intro.intro.refine'_1
d : ℤ
a : ℤ√d
hgcd : 0 < Int.gcd a.re a.im
re im : ℤ
H1 : Int.gcd re im = 1
Hre : a.re = ↑(Int.gcd a.re a.im) * re
Him : a.im = ↑(Int.gcd a.re a.im) * im
⊢ a = ↑↑(Int.gcd a.re a.im) * { re := re, im := im }
[PROOFSTEP]
rw [smul_val, ext, ← Hre, ← Him]
[GOAL]
case intro.intro.intro.intro.refine'_1
d : ℤ
a : ℤ√d
hgcd : 0 < Int.gcd a.re a.im
re im : ℤ
H1 : Int.gcd re im = 1
Hre : a.re = ↑(Int.gcd a.re a.im) * re
Him : a.im = ↑(Int.gcd a.re a.im) * im
⊢ a.re = { re := a.re, im := a.im }.re ∧ a.im = { re := a.re, im := a.im }.im
[PROOFSTEP]
constructor
[GOAL]
case intro.intro.intro.intro.refine'_1.left
d : ℤ
a : ℤ√d
hgcd : 0 < Int.gcd a.re a.im
re im : ℤ
H1 : Int.gcd re im = 1
Hre : a.re = ↑(Int.gcd a.re a.im) * re
Him : a.im = ↑(Int.gcd a.re a.im) * im
⊢ a.re = { re := a.re, im := a.im }.re
[PROOFSTEP]
rfl
[GOAL]
case intro.intro.intro.intro.refine'_1.right
d : ℤ
a : ℤ√d
hgcd : 0 < Int.gcd a.re a.im
re im : ℤ
H1 : Int.gcd re im = 1
Hre : a.re = ↑(Int.gcd a.re a.im) * re
Him : a.im = ↑(Int.gcd a.re a.im) * im
⊢ a.im = { re := a.re, im := a.im }.im
[PROOFSTEP]
rfl
[GOAL]
case intro.intro.intro.intro.refine'_2
d : ℤ
a : ℤ√d
hgcd : 0 < Int.gcd a.re a.im
re im : ℤ
H1 : Int.gcd re im = 1
Hre : a.re = ↑(Int.gcd a.re a.im) * re
Him : a.im = ↑(Int.gcd a.re a.im) * im
⊢ IsCoprime { re := re, im := im }.re { re := re, im := im }.im
[PROOFSTEP]
rw [← Int.gcd_eq_one_iff_coprime, H1]
[GOAL]
d✝ : ℤ
c d x y z w : ℕ
xy : SqLe x c y d
zw : SqLe z c w d
⊢ c * (x * z) * (c * (x * z)) ≤ d * (y * w) * (d * (y * w))
[PROOFSTEP]
simpa [mul_comm, mul_left_comm] using mul_le_mul xy zw (Nat.zero_le _) (Nat.zero_le _)
[GOAL]
d✝ : ℤ
c d x y z w : ℕ
xy : SqLe x c y d
zw : SqLe z c w d
⊢ SqLe (x + z) c (y + w) d
[PROOFSTEP]
have xz := sqLe_add_mixed xy zw
[GOAL]
d✝ : ℤ
c d x y z w : ℕ
xy : SqLe x c y d
zw : SqLe z c w d
xz : c * (x * z) ≤ d * (y * w)
⊢ SqLe (x + z) c (y + w) d
[PROOFSTEP]
simp [SqLe, mul_assoc] at xy zw 
[GOAL]
d✝ : ℤ
c d x y z w : ℕ
xz : c * (x * z) ≤ d * (y * w)
xy : c * (x * x) ≤ d * (y * y)
zw : c * (z * z) ≤ d * (w * w)
⊢ SqLe (x + z) c (y + w) d
[PROOFSTEP]
simp [SqLe, mul_add, mul_comm, mul_left_comm, add_le_add, *]
[GOAL]
d✝ : ℤ
c d x y z w : ℕ
zw : SqLe y d x c
h : SqLe (x + z) c (y + w) d
⊢ SqLe z c w d
[PROOFSTEP]
apply le_of_not_gt
[GOAL]
case a
d✝ : ℤ
c d x y z w : ℕ
zw : SqLe y d x c
h : SqLe (x + z) c (y + w) d
⊢ ¬c * z * z > d * w * w
[PROOFSTEP]
intro l
[GOAL]
case a
d✝ : ℤ
c d x y z w : ℕ
zw : SqLe y d x c
h : SqLe (x + z) c (y + w) d
l : c * z * z > d * w * w
⊢ False
[PROOFSTEP]
refine' not_le_of_gt _ h
[GOAL]
case a
d✝ : ℤ
c d x y z w : ℕ
zw : SqLe y d x c
h : SqLe (x + z) c (y + w) d
l : c * z * z > d * w * w
⊢ c * (x + z) * (x + z) > d * (y + w) * (y + w)
[PROOFSTEP]
simp only [SqLe, mul_add, mul_comm, mul_left_comm, add_assoc, gt_iff_lt]
[GOAL]
case a
d✝ : ℤ
c d x y z w : ℕ
zw : SqLe y d x c
h : SqLe (x + z) c (y + w) d
l : c * z * z > d * w * w
⊢ d * (y * y) + (d * (y * w) + (d * (y * w) + d * (w * w))) < c * (x * x) + (c * (x * z) + (c * (x * z) + c * (z * z)))
[PROOFSTEP]
have hm := sqLe_add_mixed zw (le_of_lt l)
[GOAL]
case a
d✝ : ℤ
c d x y z w : ℕ
zw : SqLe y d x c
h : SqLe (x + z) c (y + w) d
l : c * z * z > d * w * w
hm : d * (y * w) ≤ c * (x * z)
⊢ d * (y * y) + (d * (y * w) + (d * (y * w) + d * (w * w))) < c * (x * x) + (c * (x * z) + (c * (x * z) + c * (z * z)))
[PROOFSTEP]
simp only [SqLe, mul_assoc, gt_iff_lt] at l zw 
[GOAL]
case a
d✝ : ℤ
c d x y z w : ℕ
h : SqLe (x + z) c (y + w) d
hm : d * (y * w) ≤ c * (x * z)
l : d * (w * w) < c * (z * z)
zw : d * (y * y) ≤ c * (x * x)
⊢ d * (y * y) + (d * (y * w) + (d * (y * w) + d * (w * w))) < c * (x * x) + (c * (x * z) + (c * (x * z) + c * (z * z)))
[PROOFSTEP]
exact
  lt_of_le_of_lt (add_le_add_right zw _) (add_lt_add_left (add_lt_add_of_le_of_lt hm (add_lt_add_of_le_of_lt hm l)) _)
[GOAL]
d✝ : ℤ
c d x y n : ℕ
xy : SqLe x c y d
⊢ SqLe (n * x) c (n * y) d
[PROOFSTEP]
simpa [SqLe, mul_left_comm, mul_assoc] using Nat.mul_le_mul_left (n * n) xy
[GOAL]
d✝ : ℤ
d x y z w : ℕ
⊢ (SqLe x 1 y d → SqLe z 1 w d → SqLe (x * w + y * z) d (x * z + d * y * w) 1) ∧
    (SqLe x 1 y d → SqLe w d z 1 → SqLe (x * z + d * y * w) 1 (x * w + y * z) d) ∧
      (SqLe y d x 1 → SqLe z 1 w d → SqLe (x * z + d * y * w) 1 (x * w + y * z) d) ∧
        (SqLe y d x 1 → SqLe w d z 1 → SqLe (x * w + y * z) d (x * z + d * y * w) 1)
[PROOFSTEP]
refine' ⟨_, _, _, _⟩
[GOAL]
case refine'_1
d✝ : ℤ
d x y z w : ℕ
⊢ SqLe x 1 y d → SqLe z 1 w d → SqLe (x * w + y * z) d (x * z + d * y * w) 1
[PROOFSTEP]
intro xy zw
[GOAL]
case refine'_1
d✝ : ℤ
d x y z w : ℕ
xy : SqLe x 1 y d
zw : SqLe z 1 w d
⊢ SqLe (x * w + y * z) d (x * z + d * y * w) 1
[PROOFSTEP]
have := Int.mul_nonneg (sub_nonneg_of_le (Int.ofNat_le_ofNat_of_le xy)) (sub_nonneg_of_le (Int.ofNat_le_ofNat_of_le zw))
[GOAL]
case refine'_1
d✝ : ℤ
d x y z w : ℕ
xy : SqLe x 1 y d
zw : SqLe z 1 w d
this : 0 ≤ (↑(d * y * y) - ↑(1 * x * x)) * (↑(d * w * w) - ↑(1 * z * z))
⊢ SqLe (x * w + y * z) d (x * z + d * y * w) 1
[PROOFSTEP]
refine' Int.le_of_ofNat_le_ofNat (le_of_sub_nonneg _)
[GOAL]
case refine'_1
d✝ : ℤ
d x y z w : ℕ
xy : SqLe x 1 y d
zw : SqLe z 1 w d
this : 0 ≤ (↑(d * y * y) - ↑(1 * x * x)) * (↑(d * w * w) - ↑(1 * z * z))
⊢ 0 ≤ ↑(1 * (x * z + d * y * w) * (x * z + d * y * w)) - ↑(d * (x * w + y * z) * (x * w + y * z))
[PROOFSTEP]
convert this using 1
[GOAL]
case h.e'_4
d✝ : ℤ
d x y z w : ℕ
xy : SqLe x 1 y d
zw : SqLe z 1 w d
this : 0 ≤ (↑(d * y * y) - ↑(1 * x * x)) * (↑(d * w * w) - ↑(1 * z * z))
⊢ ↑(1 * (x * z + d * y * w) * (x * z + d * y * w)) - ↑(d * (x * w + y * z) * (x * w + y * z)) =
    (↑(d * y * y) - ↑(1 * x * x)) * (↑(d * w * w) - ↑(1 * z * z))
[PROOFSTEP]
simp only [one_mul, Int.ofNat_add, Int.ofNat_mul]
[GOAL]
case h.e'_4
d✝ : ℤ
d x y z w : ℕ
xy : SqLe x 1 y d
zw : SqLe z 1 w d
this : 0 ≤ (↑(d * y * y) - ↑(1 * x * x)) * (↑(d * w * w) - ↑(1 * z * z))
⊢ (↑x * ↑z + ↑d * ↑y * ↑w) * (↑x * ↑z + ↑d * ↑y * ↑w) - ↑d * (↑x * ↑w + ↑y * ↑z) * (↑x * ↑w + ↑y * ↑z) =
    (↑d * ↑y * ↑y - ↑x * ↑x) * (↑d * ↑w * ↑w - ↑z * ↑z)
[PROOFSTEP]
ring
[GOAL]
case refine'_2
d✝ : ℤ
d x y z w : ℕ
⊢ SqLe x 1 y d → SqLe w d z 1 → SqLe (x * z + d * y * w) 1 (x * w + y * z) d
[PROOFSTEP]
intro xy zw
[GOAL]
case refine'_2
d✝ : ℤ
d x y z w : ℕ
xy : SqLe x 1 y d
zw : SqLe w d z 1
⊢ SqLe (x * z + d * y * w) 1 (x * w + y * z) d
[PROOFSTEP]
have := Int.mul_nonneg (sub_nonneg_of_le (Int.ofNat_le_ofNat_of_le xy)) (sub_nonneg_of_le (Int.ofNat_le_ofNat_of_le zw))
[GOAL]
case refine'_2
d✝ : ℤ
d x y z w : ℕ
xy : SqLe x 1 y d
zw : SqLe w d z 1
this : 0 ≤ (↑(d * y * y) - ↑(1 * x * x)) * (↑(1 * z * z) - ↑(d * w * w))
⊢ SqLe (x * z + d * y * w) 1 (x * w + y * z) d
[PROOFSTEP]
refine' Int.le_of_ofNat_le_ofNat (le_of_sub_nonneg _)
[GOAL]
case refine'_2
d✝ : ℤ
d x y z w : ℕ
xy : SqLe x 1 y d
zw : SqLe w d z 1
this : 0 ≤ (↑(d * y * y) - ↑(1 * x * x)) * (↑(1 * z * z) - ↑(d * w * w))
⊢ 0 ≤ ↑(d * (x * w + y * z) * (x * w + y * z)) - ↑(1 * (x * z + d * y * w) * (x * z + d * y * w))
[PROOFSTEP]
convert this using 1
[GOAL]
case h.e'_4
d✝ : ℤ
d x y z w : ℕ
xy : SqLe x 1 y d
zw : SqLe w d z 1
this : 0 ≤ (↑(d * y * y) - ↑(1 * x * x)) * (↑(1 * z * z) - ↑(d * w * w))
⊢ ↑(d * (x * w + y * z) * (x * w + y * z)) - ↑(1 * (x * z + d * y * w) * (x * z + d * y * w)) =
    (↑(d * y * y) - ↑(1 * x * x)) * (↑(1 * z * z) - ↑(d * w * w))
[PROOFSTEP]
simp only [one_mul, Int.ofNat_add, Int.ofNat_mul]
[GOAL]
case h.e'_4
d✝ : ℤ
d x y z w : ℕ
xy : SqLe x 1 y d
zw : SqLe w d z 1
this : 0 ≤ (↑(d * y * y) - ↑(1 * x * x)) * (↑(1 * z * z) - ↑(d * w * w))
⊢ ↑d * (↑x * ↑w + ↑y * ↑z) * (↑x * ↑w + ↑y * ↑z) - (↑x * ↑z + ↑d * ↑y * ↑w) * (↑x * ↑z + ↑d * ↑y * ↑w) =
    (↑d * ↑y * ↑y - ↑x * ↑x) * (↑z * ↑z - ↑d * ↑w * ↑w)
[PROOFSTEP]
ring
[GOAL]
case refine'_3
d✝ : ℤ
d x y z w : ℕ
⊢ SqLe y d x 1 → SqLe z 1 w d → SqLe (x * z + d * y * w) 1 (x * w + y * z) d
[PROOFSTEP]
intro xy zw
[GOAL]
case refine'_3
d✝ : ℤ
d x y z w : ℕ
xy : SqLe y d x 1
zw : SqLe z 1 w d
⊢ SqLe (x * z + d * y * w) 1 (x * w + y * z) d
[PROOFSTEP]
have := Int.mul_nonneg (sub_nonneg_of_le (Int.ofNat_le_ofNat_of_le xy)) (sub_nonneg_of_le (Int.ofNat_le_ofNat_of_le zw))
[GOAL]
case refine'_3
d✝ : ℤ
d x y z w : ℕ
xy : SqLe y d x 1
zw : SqLe z 1 w d
this : 0 ≤ (↑(1 * x * x) - ↑(d * y * y)) * (↑(d * w * w) - ↑(1 * z * z))
⊢ SqLe (x * z + d * y * w) 1 (x * w + y * z) d
[PROOFSTEP]
refine' Int.le_of_ofNat_le_ofNat (le_of_sub_nonneg _)
[GOAL]
case refine'_3
d✝ : ℤ
d x y z w : ℕ
xy : SqLe y d x 1
zw : SqLe z 1 w d
this : 0 ≤ (↑(1 * x * x) - ↑(d * y * y)) * (↑(d * w * w) - ↑(1 * z * z))
⊢ 0 ≤ ↑(d * (x * w + y * z) * (x * w + y * z)) - ↑(1 * (x * z + d * y * w) * (x * z + d * y * w))
[PROOFSTEP]
convert this using 1
[GOAL]
case h.e'_4
d✝ : ℤ
d x y z w : ℕ
xy : SqLe y d x 1
zw : SqLe z 1 w d
this : 0 ≤ (↑(1 * x * x) - ↑(d * y * y)) * (↑(d * w * w) - ↑(1 * z * z))
⊢ ↑(d * (x * w + y * z) * (x * w + y * z)) - ↑(1 * (x * z + d * y * w) * (x * z + d * y * w)) =
    (↑(1 * x * x) - ↑(d * y * y)) * (↑(d * w * w) - ↑(1 * z * z))
[PROOFSTEP]
simp only [one_mul, Int.ofNat_add, Int.ofNat_mul]
[GOAL]
case h.e'_4
d✝ : ℤ
d x y z w : ℕ
xy : SqLe y d x 1
zw : SqLe z 1 w d
this : 0 ≤ (↑(1 * x * x) - ↑(d * y * y)) * (↑(d * w * w) - ↑(1 * z * z))
⊢ ↑d * (↑x * ↑w + ↑y * ↑z) * (↑x * ↑w + ↑y * ↑z) - (↑x * ↑z + ↑d * ↑y * ↑w) * (↑x * ↑z + ↑d * ↑y * ↑w) =
    (↑x * ↑x - ↑d * ↑y * ↑y) * (↑d * ↑w * ↑w - ↑z * ↑z)
[PROOFSTEP]
ring
[GOAL]
case refine'_4
d✝ : ℤ
d x y z w : ℕ
⊢ SqLe y d x 1 → SqLe w d z 1 → SqLe (x * w + y * z) d (x * z + d * y * w) 1
[PROOFSTEP]
intro xy zw
[GOAL]
case refine'_4
d✝ : ℤ
d x y z w : ℕ
xy : SqLe y d x 1
zw : SqLe w d z 1
⊢ SqLe (x * w + y * z) d (x * z + d * y * w) 1
[PROOFSTEP]
have := Int.mul_nonneg (sub_nonneg_of_le (Int.ofNat_le_ofNat_of_le xy)) (sub_nonneg_of_le (Int.ofNat_le_ofNat_of_le zw))
[GOAL]
case refine'_4
d✝ : ℤ
d x y z w : ℕ
xy : SqLe y d x 1
zw : SqLe w d z 1
this : 0 ≤ (↑(1 * x * x) - ↑(d * y * y)) * (↑(1 * z * z) - ↑(d * w * w))
⊢ SqLe (x * w + y * z) d (x * z + d * y * w) 1
[PROOFSTEP]
refine' Int.le_of_ofNat_le_ofNat (le_of_sub_nonneg _)
[GOAL]
case refine'_4
d✝ : ℤ
d x y z w : ℕ
xy : SqLe y d x 1
zw : SqLe w d z 1
this : 0 ≤ (↑(1 * x * x) - ↑(d * y * y)) * (↑(1 * z * z) - ↑(d * w * w))
⊢ 0 ≤ ↑(1 * (x * z + d * y * w) * (x * z + d * y * w)) - ↑(d * (x * w + y * z) * (x * w + y * z))
[PROOFSTEP]
convert this using 1
[GOAL]
case h.e'_4
d✝ : ℤ
d x y z w : ℕ
xy : SqLe y d x 1
zw : SqLe w d z 1
this : 0 ≤ (↑(1 * x * x) - ↑(d * y * y)) * (↑(1 * z * z) - ↑(d * w * w))
⊢ ↑(1 * (x * z + d * y * w) * (x * z + d * y * w)) - ↑(d * (x * w + y * z) * (x * w + y * z)) =
    (↑(1 * x * x) - ↑(d * y * y)) * (↑(1 * z * z) - ↑(d * w * w))
[PROOFSTEP]
simp only [one_mul, Int.ofNat_add, Int.ofNat_mul]
[GOAL]
case h.e'_4
d✝ : ℤ
d x y z w : ℕ
xy : SqLe y d x 1
zw : SqLe w d z 1
this : 0 ≤ (↑(1 * x * x) - ↑(d * y * y)) * (↑(1 * z * z) - ↑(d * w * w))
⊢ (↑x * ↑z + ↑d * ↑y * ↑w) * (↑x * ↑z + ↑d * ↑y * ↑w) - ↑d * (↑x * ↑w + ↑y * ↑z) * (↑x * ↑w + ↑y * ↑z) =
    (↑x * ↑x - ↑d * ↑y * ↑y) * (↑z * ↑z - ↑d * ↑w * ↑w)
[PROOFSTEP]
ring
[GOAL]
d✝ : ℤ
c d : ℕ
x y : ℤ
⊢ Nonnegg c d x y = Nonnegg d c y x
[PROOFSTEP]
induction x
[GOAL]
case ofNat
d✝ : ℤ
c d : ℕ
y : ℤ
a✝ : ℕ
⊢ Nonnegg c d (Int.ofNat a✝) y = Nonnegg d c y (Int.ofNat a✝)
[PROOFSTEP]
induction y
[GOAL]
case negSucc
d✝ : ℤ
c d : ℕ
y : ℤ
a✝ : ℕ
⊢ Nonnegg c d (Int.negSucc a✝) y = Nonnegg d c y (Int.negSucc a✝)
[PROOFSTEP]
induction y
[GOAL]
case ofNat.ofNat
d✝ : ℤ
c d a✝¹ a✝ : ℕ
⊢ Nonnegg c d (Int.ofNat a✝¹) (Int.ofNat a✝) = Nonnegg d c (Int.ofNat a✝) (Int.ofNat a✝¹)
[PROOFSTEP]
rfl
[GOAL]
case ofNat.negSucc
d✝ : ℤ
c d a✝¹ a✝ : ℕ
⊢ Nonnegg c d (Int.ofNat a✝¹) (Int.negSucc a✝) = Nonnegg d c (Int.negSucc a✝) (Int.ofNat a✝¹)
[PROOFSTEP]
rfl
[GOAL]
case negSucc.ofNat
d✝ : ℤ
c d a✝¹ a✝ : ℕ
⊢ Nonnegg c d (Int.negSucc a✝¹) (Int.ofNat a✝) = Nonnegg d c (Int.ofNat a✝) (Int.negSucc a✝¹)
[PROOFSTEP]
rfl
[GOAL]
case negSucc.negSucc
d✝ : ℤ
c d a✝¹ a✝ : ℕ
⊢ Nonnegg c d (Int.negSucc a✝¹) (Int.negSucc a✝) = Nonnegg d c (Int.negSucc a✝) (Int.negSucc a✝¹)
[PROOFSTEP]
rfl
[GOAL]
d✝ : ℤ
c d b : ℕ
⊢ Nonnegg c d (-↑0) ↑b → SqLe 0 d b c
[PROOFSTEP]
simp [SqLe, Nat.zero_le]
[GOAL]
d✝ : ℤ
c d a b : ℕ
⊢ Nonnegg c d (-↑(a + 1)) ↑b ↔ SqLe (a + 1) d b c
[PROOFSTEP]
rw [← Int.negSucc_coe]
[GOAL]
d✝ : ℤ
c d a b : ℕ
⊢ Nonnegg c d (Int.negSucc a) ↑b ↔ SqLe (a + 1) d b c
[PROOFSTEP]
rfl
[GOAL]
d✝ : ℤ
c d a b : ℕ
⊢ Nonnegg c d (↑a) (-↑b) ↔ SqLe b c a d
[PROOFSTEP]
rw [nonnegg_comm]
[GOAL]
d✝ : ℤ
c d a b : ℕ
⊢ Nonnegg d c (-↑b) ↑a ↔ SqLe b c a d
[PROOFSTEP]
exact nonnegg_neg_pos
[GOAL]
d : ℤ
⊢ norm 0 = 0
[PROOFSTEP]
simp [norm]
[GOAL]
d : ℤ
⊢ norm 1 = 1
[PROOFSTEP]
simp [norm]
[GOAL]
d n : ℤ
⊢ norm ↑n = n * n
[PROOFSTEP]
simp [norm]
[GOAL]
d : ℤ
n m : ℤ√d
⊢ norm (n * m) = norm n * norm m
[PROOFSTEP]
simp only [norm, mul_im, mul_re]
[GOAL]
d : ℤ
n m : ℤ√d
⊢ (n.re * m.re + d * n.im * m.im) * (n.re * m.re + d * n.im * m.im) -
      d * (n.re * m.im + n.im * m.re) * (n.re * m.im + n.im * m.re) =
    (n.re * n.re - d * n.im * n.im) * (m.re * m.re - d * m.im * m.im)
[PROOFSTEP]
ring
[GOAL]
d : ℤ
n : ℤ√d
⊢ ↑(norm n) = n * star n
[PROOFSTEP]
cases n
[GOAL]
case mk
d re✝ im✝ : ℤ
⊢ ↑(norm { re := re✝, im := im✝ }) = { re := re✝, im := im✝ } * star { re := re✝, im := im✝ }
[PROOFSTEP]
simp [norm, star, Zsqrtd.ext, mul_comm, sub_eq_add_neg]
[GOAL]
d : ℤ
x : ℤ√d
⊢ ↑(norm (-x)) = ↑(norm x)
[PROOFSTEP]
rw [norm_eq_mul_conj, star_neg, neg_mul_neg, norm_eq_mul_conj]
[GOAL]
d : ℤ
x : ℤ√d
⊢ ↑(norm (star x)) = ↑(norm x)
[PROOFSTEP]
rw [norm_eq_mul_conj, star_star, mul_comm, norm_eq_mul_conj]
[GOAL]
d : ℤ
hd : d ≤ 0
n : ℤ√d
⊢ 0 ≤ -(d * n.im * n.im)
[PROOFSTEP]
rw [mul_assoc, neg_mul_eq_neg_mul]
[GOAL]
d : ℤ
hd : d ≤ 0
n : ℤ√d
⊢ 0 ≤ -d * (n.im * n.im)
[PROOFSTEP]
exact mul_nonneg (neg_nonneg.2 hd) (mul_self_nonneg _)
[GOAL]
d : ℤ
x : ℤ√d
h : Int.natAbs (norm x) = 1
hx : 0 ≤ norm x
⊢ 1 = x * star x
[PROOFSTEP]
rwa [← Int.coe_nat_inj', Int.natAbs_of_nonneg hx, ← @Int.cast_inj (ℤ√d) _ _, norm_eq_mul_conj, eq_comm] at h 
[GOAL]
d : ℤ
x : ℤ√d
h : Int.natAbs (norm x) = 1
hx : norm x ≤ 0
⊢ 1 = x * -star x
[PROOFSTEP]
rwa [← Int.coe_nat_inj', Int.ofNat_natAbs_of_nonpos hx, ← @Int.cast_inj (ℤ√d) _ _, Int.cast_neg, norm_eq_mul_conj,
  neg_mul_eq_mul_neg, eq_comm] at h 
[GOAL]
d : ℤ
x : ℤ√d
h : IsUnit x
⊢ Int.natAbs (norm x) = 1
[PROOFSTEP]
let ⟨y, hy⟩ := isUnit_iff_dvd_one.1 h
[GOAL]
d : ℤ
x : ℤ√d
h : IsUnit x
y : ℤ√d
hy : 1 = x * y
⊢ Int.natAbs (norm x) = 1
[PROOFSTEP]
have := congr_arg (Int.natAbs ∘ norm) hy
[GOAL]
d : ℤ
x : ℤ√d
h : IsUnit x
y : ℤ√d
hy : 1 = x * y
this : (Int.natAbs ∘ norm) 1 = (Int.natAbs ∘ norm) (x * y)
⊢ Int.natAbs (norm x) = 1
[PROOFSTEP]
rw [Function.comp_apply, Function.comp_apply, norm_mul, Int.natAbs_mul, norm_one, Int.natAbs_one, eq_comm,
  mul_eq_one] at this 
[GOAL]
d : ℤ
x : ℤ√d
h : IsUnit x
y : ℤ√d
hy : 1 = x * y
this : Int.natAbs (norm x) = 1 ∧ Int.natAbs (norm y) = 1
⊢ Int.natAbs (norm x) = 1
[PROOFSTEP]
exact this.1
[GOAL]
d✝ d : ℤ
z : ℤ√d
⊢ IsUnit z ↔ IsUnit (norm z)
[PROOFSTEP]
rw [Int.isUnit_iff_natAbs_eq, norm_eq_one_iff]
[GOAL]
d✝ d : ℤ
hd : d ≤ 0
z : ℤ√d
⊢ norm z = 1 ↔ IsUnit z
[PROOFSTEP]
rw [← norm_eq_one_iff, ← Int.coe_nat_inj', Int.natAbs_of_nonneg (norm_nonneg hd z), Int.ofNat_one]
[GOAL]
d✝ d : ℤ
hd : d < 0
z : ℤ√d
⊢ norm z = 0 ↔ z = 0
[PROOFSTEP]
constructor
[GOAL]
case mp
d✝ d : ℤ
hd : d < 0
z : ℤ√d
⊢ norm z = 0 → z = 0
[PROOFSTEP]
intro h
[GOAL]
case mp
d✝ d : ℤ
hd : d < 0
z : ℤ√d
h : norm z = 0
⊢ z = 0
[PROOFSTEP]
rw [ext, zero_re, zero_im]
[GOAL]
case mp
d✝ d : ℤ
hd : d < 0
z : ℤ√d
h : norm z = 0
⊢ z.re = 0 ∧ z.im = 0
[PROOFSTEP]
rw [norm_def, sub_eq_add_neg, mul_assoc] at h 
[GOAL]
case mp
d✝ d : ℤ
hd : d < 0
z : ℤ√d
h : z.re * z.re + -(d * (z.im * z.im)) = 0
⊢ z.re = 0 ∧ z.im = 0
[PROOFSTEP]
have left := mul_self_nonneg z.re
[GOAL]
case mp
d✝ d : ℤ
hd : d < 0
z : ℤ√d
h : z.re * z.re + -(d * (z.im * z.im)) = 0
left : 0 ≤ z.re * z.re
⊢ z.re = 0 ∧ z.im = 0
[PROOFSTEP]
have right := neg_nonneg.mpr (mul_nonpos_of_nonpos_of_nonneg hd.le (mul_self_nonneg z.im))
[GOAL]
case mp
d✝ d : ℤ
hd : d < 0
z : ℤ√d
h : z.re * z.re + -(d * (z.im * z.im)) = 0
left : 0 ≤ z.re * z.re
right : 0 ≤ -(d * (z.im * z.im))
⊢ z.re = 0 ∧ z.im = 0
[PROOFSTEP]
obtain ⟨ha, hb⟩ := (add_eq_zero_iff' left right).mp h
[GOAL]
case mp.intro
d✝ d : ℤ
hd : d < 0
z : ℤ√d
h : z.re * z.re + -(d * (z.im * z.im)) = 0
left : 0 ≤ z.re * z.re
right : 0 ≤ -(d * (z.im * z.im))
ha : z.re * z.re = 0
hb : -(d * (z.im * z.im)) = 0
⊢ z.re = 0 ∧ z.im = 0
[PROOFSTEP]
constructor
[GOAL]
case mp.intro.left
d✝ d : ℤ
hd : d < 0
z : ℤ√d
h : z.re * z.re + -(d * (z.im * z.im)) = 0
left : 0 ≤ z.re * z.re
right : 0 ≤ -(d * (z.im * z.im))
ha : z.re * z.re = 0
hb : -(d * (z.im * z.im)) = 0
⊢ z.re = 0
[PROOFSTEP]
apply eq_zero_of_mul_self_eq_zero
[GOAL]
case mp.intro.right
d✝ d : ℤ
hd : d < 0
z : ℤ√d
h : z.re * z.re + -(d * (z.im * z.im)) = 0
left : 0 ≤ z.re * z.re
right : 0 ≤ -(d * (z.im * z.im))
ha : z.re * z.re = 0
hb : -(d * (z.im * z.im)) = 0
⊢ z.im = 0
[PROOFSTEP]
apply eq_zero_of_mul_self_eq_zero
[GOAL]
case mp.intro.left.h
d✝ d : ℤ
hd : d < 0
z : ℤ√d
h : z.re * z.re + -(d * (z.im * z.im)) = 0
left : 0 ≤ z.re * z.re
right : 0 ≤ -(d * (z.im * z.im))
ha : z.re * z.re = 0
hb : -(d * (z.im * z.im)) = 0
⊢ z.re * z.re = 0
[PROOFSTEP]
exact ha
[GOAL]
case mp.intro.right.h
d✝ d : ℤ
hd : d < 0
z : ℤ√d
h : z.re * z.re + -(d * (z.im * z.im)) = 0
left : 0 ≤ z.re * z.re
right : 0 ≤ -(d * (z.im * z.im))
ha : z.re * z.re = 0
hb : -(d * (z.im * z.im)) = 0
⊢ z.im * z.im = 0
[PROOFSTEP]
rw [neg_eq_zero, mul_eq_zero] at hb 
[GOAL]
case mp.intro.right.h
d✝ d : ℤ
hd : d < 0
z : ℤ√d
h : z.re * z.re + -(d * (z.im * z.im)) = 0
left : 0 ≤ z.re * z.re
right : 0 ≤ -(d * (z.im * z.im))
ha : z.re * z.re = 0
hb : d = 0 ∨ z.im * z.im = 0
⊢ z.im * z.im = 0
[PROOFSTEP]
exact hb.resolve_left hd.ne
[GOAL]
case mpr
d✝ d : ℤ
hd : d < 0
z : ℤ√d
⊢ z = 0 → norm z = 0
[PROOFSTEP]
rintro rfl
[GOAL]
case mpr
d✝ d : ℤ
hd : d < 0
⊢ norm 0 = 0
[PROOFSTEP]
exact norm_zero
[GOAL]
d✝ d : ℤ
hd : d ≤ 0
x y : ℤ√d
h : Associated x y
⊢ norm x = norm y
[PROOFSTEP]
obtain ⟨u, rfl⟩ := h
[GOAL]
case intro
d✝ d : ℤ
hd : d ≤ 0
x : ℤ√d
u : (ℤ√d)ˣ
⊢ norm x = norm (x * ↑u)
[PROOFSTEP]
rw [norm_mul, (norm_eq_one_iff' hd _).mpr u.isUnit, mul_one]
[GOAL]
d✝ c d : ℕ
a b : ℤ
⊢ Decidable (Nonnegg c d a b)
[PROOFSTEP]
cases a
[GOAL]
case ofNat
d✝ c d : ℕ
b : ℤ
a✝ : ℕ
⊢ Decidable (Nonnegg c d (Int.ofNat a✝) b)
[PROOFSTEP]
cases b
[GOAL]
case negSucc
d✝ c d : ℕ
b : ℤ
a✝ : ℕ
⊢ Decidable (Nonnegg c d (Int.negSucc a✝) b)
[PROOFSTEP]
cases b
[GOAL]
case ofNat.ofNat
d✝ c d a✝¹ a✝ : ℕ
⊢ Decidable (Nonnegg c d (Int.ofNat a✝¹) (Int.ofNat a✝))
[PROOFSTEP]
unfold Nonnegg SqLe
[GOAL]
case ofNat.negSucc
d✝ c d a✝¹ a✝ : ℕ
⊢ Decidable (Nonnegg c d (Int.ofNat a✝¹) (Int.negSucc a✝))
[PROOFSTEP]
unfold Nonnegg SqLe
[GOAL]
case negSucc.ofNat
d✝ c d a✝¹ a✝ : ℕ
⊢ Decidable (Nonnegg c d (Int.negSucc a✝¹) (Int.ofNat a✝))
[PROOFSTEP]
unfold Nonnegg SqLe
[GOAL]
case negSucc.negSucc
d✝ c d a✝¹ a✝ : ℕ
⊢ Decidable (Nonnegg c d (Int.negSucc a✝¹) (Int.negSucc a✝))
[PROOFSTEP]
unfold Nonnegg SqLe
[GOAL]
case ofNat.ofNat
d✝ c d a✝¹ a✝ : ℕ
⊢ Decidable
    (match Int.ofNat a✝¹, Int.ofNat a✝ with
    | Int.ofNat a, Int.ofNat b => True
    | Int.ofNat a, Int.negSucc b => c * (b + 1) * (b + 1) ≤ d * a * a
    | Int.negSucc a, Int.ofNat b => d * (a + 1) * (a + 1) ≤ c * b * b
    | Int.negSucc a, Int.negSucc a_1 => False)
[PROOFSTEP]
infer_instance
[GOAL]
case ofNat.negSucc
d✝ c d a✝¹ a✝ : ℕ
⊢ Decidable
    (match Int.ofNat a✝¹, Int.negSucc a✝ with
    | Int.ofNat a, Int.ofNat b => True
    | Int.ofNat a, Int.negSucc b => c * (b + 1) * (b + 1) ≤ d * a * a
    | Int.negSucc a, Int.ofNat b => d * (a + 1) * (a + 1) ≤ c * b * b
    | Int.negSucc a, Int.negSucc a_1 => False)
[PROOFSTEP]
infer_instance
[GOAL]
case negSucc.ofNat
d✝ c d a✝¹ a✝ : ℕ
⊢ Decidable
    (match Int.negSucc a✝¹, Int.ofNat a✝ with
    | Int.ofNat a, Int.ofNat b => True
    | Int.ofNat a, Int.negSucc b => c * (b + 1) * (b + 1) ≤ d * a * a
    | Int.negSucc a, Int.ofNat b => d * (a + 1) * (a + 1) ≤ c * b * b
    | Int.negSucc a, Int.negSucc a_1 => False)
[PROOFSTEP]
infer_instance
[GOAL]
case negSucc.negSucc
d✝ c d a✝¹ a✝ : ℕ
⊢ Decidable
    (match Int.negSucc a✝¹, Int.negSucc a✝ with
    | Int.ofNat a, Int.ofNat b => True
    | Int.ofNat a, Int.negSucc b => c * (b + 1) * (b + 1) ≤ d * a * a
    | Int.negSucc a, Int.ofNat b => d * (a + 1) * (a + 1) ≤ c * b * b
    | Int.negSucc a, Int.negSucc a_1 => False)
[PROOFSTEP]
infer_instance
[GOAL]
d x y z w : ℕ
xy : Nonneg { re := ↑x, im := -↑y }
zw : Nonneg { re := -↑z, im := ↑w }
⊢ Nonneg ({ re := ↑x, im := -↑y } + { re := -↑z, im := ↑w })
[PROOFSTEP]
have : Nonneg ⟨Int.subNatNat x z, Int.subNatNat w y⟩ :=
  Int.subNatNat_elim x z (fun m n i => SqLe y d m 1 → SqLe n 1 w d → Nonneg ⟨i, Int.subNatNat w y⟩)
    (fun j k =>
      Int.subNatNat_elim w y (fun m n i => SqLe n d (k + j) 1 → SqLe k 1 m d → Nonneg ⟨Int.ofNat j, i⟩)
        (fun _ _ _ _ => trivial) fun m n xy zw => sqLe_cancel zw xy)
    (fun j k =>
      Int.subNatNat_elim w y (fun m n i => SqLe n d k 1 → SqLe (k + j + 1) 1 m d → Nonneg ⟨-[j+1], i⟩)
        (fun m n xy zw => sqLe_cancel xy zw) fun m n xy zw =>
        let t := Nat.le_trans zw (sqLe_of_le (Nat.le_add_right n (m + 1)) le_rfl xy)
        have : k + j + 1 ≤ k := Nat.mul_self_le_mul_self_iff.2 (by simpa [one_mul] using t)
        absurd this (not_le_of_gt <| Nat.succ_le_succ <| Nat.le_add_right _ _))
    (nonnegg_pos_neg.1 xy) (nonnegg_neg_pos.1 zw)
[GOAL]
d x y z w : ℕ
xy✝ : Nonneg { re := ↑x, im := -↑y }
zw✝ : Nonneg { re := -↑z, im := ↑w }
j k m n : ℕ
xy : SqLe (n + m + 1) d k 1
zw : SqLe (k + j + 1) 1 n d
t : 1 * (k + j + 1) * (k + j + 1) ≤ 1 * k * k := Nat.le_trans zw (sqLe_of_le (Nat.le_add_right n (m + 1)) le_rfl xy)
⊢ (k + j + 1) * (k + j + 1) ≤ k * k
[PROOFSTEP]
simpa [one_mul] using t
[GOAL]
d x y z w : ℕ
xy : Nonneg { re := ↑x, im := -↑y }
zw : Nonneg { re := -↑z, im := ↑w }
this : Nonneg { re := subNatNat x z, im := subNatNat w y }
⊢ Nonneg ({ re := ↑x, im := -↑y } + { re := -↑z, im := ↑w })
[PROOFSTEP]
rw [add_def, neg_add_eq_sub]
[GOAL]
d x y z w : ℕ
xy : Nonneg { re := ↑x, im := -↑y }
zw : Nonneg { re := -↑z, im := ↑w }
this : Nonneg { re := subNatNat x z, im := subNatNat w y }
⊢ Nonneg { re := ↑x + -↑z, im := ↑w - ↑y }
[PROOFSTEP]
rwa [Int.subNatNat_eq_coe, Int.subNatNat_eq_coe] at this 
[GOAL]
d : ℕ
a b : ℤ√↑d
ha : Nonneg a
hb : Nonneg b
⊢ Nonneg (a + b)
[PROOFSTEP]
rcases nonneg_cases ha with ⟨x, y, rfl | rfl | rfl⟩
[GOAL]
case intro.intro.inl
d : ℕ
b : ℤ√↑d
hb : Nonneg b
x y : ℕ
ha : Nonneg { re := ↑x, im := ↑y }
⊢ Nonneg ({ re := ↑x, im := ↑y } + b)
[PROOFSTEP]
rcases nonneg_cases hb with ⟨z, w, rfl | rfl | rfl⟩
[GOAL]
case intro.intro.inr.inl
d : ℕ
b : ℤ√↑d
hb : Nonneg b
x y : ℕ
ha : Nonneg { re := ↑x, im := -↑y }
⊢ Nonneg ({ re := ↑x, im := -↑y } + b)
[PROOFSTEP]
rcases nonneg_cases hb with ⟨z, w, rfl | rfl | rfl⟩
[GOAL]
case intro.intro.inr.inr
d : ℕ
b : ℤ√↑d
hb : Nonneg b
x y : ℕ
ha : Nonneg { re := -↑x, im := ↑y }
⊢ Nonneg ({ re := -↑x, im := ↑y } + b)
[PROOFSTEP]
rcases nonneg_cases hb with ⟨z, w, rfl | rfl | rfl⟩
[GOAL]
case intro.intro.inl.intro.intro.inl
d x y : ℕ
ha : Nonneg { re := ↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := ↑w }
⊢ Nonneg ({ re := ↑x, im := ↑y } + { re := ↑z, im := ↑w })
[PROOFSTEP]
trivial
[GOAL]
case intro.intro.inl.intro.intro.inr.inl
d x y : ℕ
ha : Nonneg { re := ↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := -↑w }
⊢ Nonneg ({ re := ↑x, im := ↑y } + { re := ↑z, im := -↑w })
[PROOFSTEP]
refine' nonnegg_cases_right fun i h => sqLe_of_le _ _ (nonnegg_pos_neg.1 hb)
[GOAL]
case intro.intro.inl.intro.intro.inr.inl.refine'_1
d x y : ℕ
ha : Nonneg { re := ↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := -↑w }
i : ℕ
h : { re := ↑x, im := ↑y }.im + { re := ↑z, im := -↑w }.im = -↑i
⊢ i ≤ w
[PROOFSTEP]
dsimp only at h 
[GOAL]
case intro.intro.inl.intro.intro.inr.inl.refine'_1
d x y : ℕ
ha : Nonneg { re := ↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := -↑w }
i : ℕ
h : ↑y + -↑w = -↑i
⊢ i ≤ w
[PROOFSTEP]
exact Int.ofNat_le.1 (le_of_neg_le_neg (Int.le.intro y (by simp [add_comm, *])))
[GOAL]
d x y : ℕ
ha : Nonneg { re := ↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := -↑w }
i : ℕ
h : ↑y + -↑w = -↑i
⊢ -↑w + ↑y = -↑i
[PROOFSTEP]
simp [add_comm, *]
[GOAL]
case intro.intro.inl.intro.intro.inr.inl.refine'_2
d x y : ℕ
ha : Nonneg { re := ↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := -↑w }
i : ℕ
h : { re := ↑x, im := ↑y }.im + { re := ↑z, im := -↑w }.im = -↑i
⊢ z ≤ x + z
[PROOFSTEP]
apply Nat.le_add_left
[GOAL]
case intro.intro.inl.intro.intro.inr.inr
d x y : ℕ
ha : Nonneg { re := ↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := -↑z, im := ↑w }
⊢ Nonneg ({ re := ↑x, im := ↑y } + { re := -↑z, im := ↑w })
[PROOFSTEP]
refine' nonnegg_cases_left fun i h => sqLe_of_le _ _ (nonnegg_neg_pos.1 hb)
[GOAL]
case intro.intro.inl.intro.intro.inr.inr.refine'_1
d x y : ℕ
ha : Nonneg { re := ↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := -↑z, im := ↑w }
i : ℕ
h : { re := ↑x, im := ↑y }.re + { re := -↑z, im := ↑w }.re = -↑i
⊢ i ≤ z
[PROOFSTEP]
dsimp only at h 
[GOAL]
case intro.intro.inl.intro.intro.inr.inr.refine'_1
d x y : ℕ
ha : Nonneg { re := ↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := -↑z, im := ↑w }
i : ℕ
h : ↑x + -↑z = -↑i
⊢ i ≤ z
[PROOFSTEP]
exact Int.ofNat_le.1 (le_of_neg_le_neg (Int.le.intro x (by simp [add_comm, *])))
[GOAL]
d x y : ℕ
ha : Nonneg { re := ↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := -↑z, im := ↑w }
i : ℕ
h : ↑x + -↑z = -↑i
⊢ -↑z + ↑x = -↑i
[PROOFSTEP]
simp [add_comm, *]
[GOAL]
case intro.intro.inl.intro.intro.inr.inr.refine'_2
d x y : ℕ
ha : Nonneg { re := ↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := -↑z, im := ↑w }
i : ℕ
h : { re := ↑x, im := ↑y }.re + { re := -↑z, im := ↑w }.re = -↑i
⊢ w ≤ y + w
[PROOFSTEP]
apply Nat.le_add_left
[GOAL]
case intro.intro.inr.inl.intro.intro.inl
d x y : ℕ
ha : Nonneg { re := ↑x, im := -↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := ↑w }
⊢ Nonneg ({ re := ↑x, im := -↑y } + { re := ↑z, im := ↑w })
[PROOFSTEP]
refine' nonnegg_cases_right fun i h => sqLe_of_le _ _ (nonnegg_pos_neg.1 ha)
[GOAL]
case intro.intro.inr.inl.intro.intro.inl.refine'_1
d x y : ℕ
ha : Nonneg { re := ↑x, im := -↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := ↑w }
i : ℕ
h : { re := ↑x, im := -↑y }.im + { re := ↑z, im := ↑w }.im = -↑i
⊢ i ≤ y
[PROOFSTEP]
dsimp only at h 
[GOAL]
case intro.intro.inr.inl.intro.intro.inl.refine'_1
d x y : ℕ
ha : Nonneg { re := ↑x, im := -↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := ↑w }
i : ℕ
h : -↑y + ↑w = -↑i
⊢ i ≤ y
[PROOFSTEP]
exact Int.ofNat_le.1 (le_of_neg_le_neg (Int.le.intro w (by simp [*])))
[GOAL]
d x y : ℕ
ha : Nonneg { re := ↑x, im := -↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := ↑w }
i : ℕ
h : -↑y + ↑w = -↑i
⊢ -↑y + ↑w = -↑i
[PROOFSTEP]
simp [*]
[GOAL]
case intro.intro.inr.inl.intro.intro.inl.refine'_2
d x y : ℕ
ha : Nonneg { re := ↑x, im := -↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := ↑w }
i : ℕ
h : { re := ↑x, im := -↑y }.im + { re := ↑z, im := ↑w }.im = -↑i
⊢ x ≤ x + z
[PROOFSTEP]
apply Nat.le_add_right
[GOAL]
case intro.intro.inr.inl.intro.intro.inr.inl
d x y : ℕ
ha : Nonneg { re := ↑x, im := -↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := -↑w }
⊢ Nonneg ({ re := ↑x, im := -↑y } + { re := ↑z, im := -↑w })
[PROOFSTEP]
have : Nonneg ⟨_, _⟩ := nonnegg_pos_neg.2 (sqLe_add (nonnegg_pos_neg.1 ha) (nonnegg_pos_neg.1 hb))
[GOAL]
case intro.intro.inr.inl.intro.intro.inr.inl
d x y : ℕ
ha : Nonneg { re := ↑x, im := -↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := -↑w }
this : Nonneg { re := ↑(x + z), im := -↑(y + w) }
⊢ Nonneg ({ re := ↑x, im := -↑y } + { re := ↑z, im := -↑w })
[PROOFSTEP]
rw [Nat.cast_add, Nat.cast_add, neg_add] at this 
[GOAL]
case intro.intro.inr.inl.intro.intro.inr.inl
d x y : ℕ
ha : Nonneg { re := ↑x, im := -↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := -↑w }
this : Nonneg { re := ↑x + ↑z, im := -↑y + -↑w }
⊢ Nonneg ({ re := ↑x, im := -↑y } + { re := ↑z, im := -↑w })
[PROOFSTEP]
rwa [add_def]
  -- Porting note: was
      -- simpa [add_comm] using
      --   nonnegg_pos_neg.2 (sqLe_add (nonnegg_pos_neg.1 ha) (nonnegg_pos_neg.1 hb))
[GOAL]
case intro.intro.inr.inl.intro.intro.inr.inr
d x y : ℕ
ha : Nonneg { re := ↑x, im := -↑y }
z w : ℕ
hb : Nonneg { re := -↑z, im := ↑w }
⊢ Nonneg ({ re := ↑x, im := -↑y } + { re := -↑z, im := ↑w })
[PROOFSTEP]
exact nonneg_add_lem ha hb
[GOAL]
case intro.intro.inr.inr.intro.intro.inl
d x y : ℕ
ha : Nonneg { re := -↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := ↑w }
⊢ Nonneg ({ re := -↑x, im := ↑y } + { re := ↑z, im := ↑w })
[PROOFSTEP]
refine' nonnegg_cases_left fun i h => sqLe_of_le _ _ (nonnegg_neg_pos.1 ha)
[GOAL]
case intro.intro.inr.inr.intro.intro.inl.refine'_1
d x y : ℕ
ha : Nonneg { re := -↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := ↑w }
i : ℕ
h : { re := -↑x, im := ↑y }.re + { re := ↑z, im := ↑w }.re = -↑i
⊢ i ≤ x
[PROOFSTEP]
dsimp only at h 
[GOAL]
case intro.intro.inr.inr.intro.intro.inl.refine'_1
d x y : ℕ
ha : Nonneg { re := -↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := ↑w }
i : ℕ
h : -↑x + ↑z = -↑i
⊢ i ≤ x
[PROOFSTEP]
exact Int.ofNat_le.1 (le_of_neg_le_neg (Int.le.intro _ h))
[GOAL]
case intro.intro.inr.inr.intro.intro.inl.refine'_2
d x y : ℕ
ha : Nonneg { re := -↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := ↑w }
i : ℕ
h : { re := -↑x, im := ↑y }.re + { re := ↑z, im := ↑w }.re = -↑i
⊢ y ≤ y + w
[PROOFSTEP]
apply Nat.le_add_right
[GOAL]
case intro.intro.inr.inr.intro.intro.inr.inl
d x y : ℕ
ha : Nonneg { re := -↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := -↑w }
⊢ Nonneg ({ re := -↑x, im := ↑y } + { re := ↑z, im := -↑w })
[PROOFSTEP]
dsimp
[GOAL]
case intro.intro.inr.inr.intro.intro.inr.inl
d x y : ℕ
ha : Nonneg { re := -↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := -↑w }
⊢ Nonneg { re := -↑x + ↑z, im := ↑y + -↑w }
[PROOFSTEP]
rw [add_comm, add_comm (y : ℤ)]
[GOAL]
case intro.intro.inr.inr.intro.intro.inr.inl
d x y : ℕ
ha : Nonneg { re := -↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := ↑z, im := -↑w }
⊢ Nonneg { re := ↑z + -↑x, im := -↑w + ↑y }
[PROOFSTEP]
exact nonneg_add_lem hb ha
[GOAL]
case intro.intro.inr.inr.intro.intro.inr.inr
d x y : ℕ
ha : Nonneg { re := -↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := -↑z, im := ↑w }
⊢ Nonneg ({ re := -↑x, im := ↑y } + { re := -↑z, im := ↑w })
[PROOFSTEP]
have : Nonneg ⟨_, _⟩ := nonnegg_neg_pos.2 (sqLe_add (nonnegg_neg_pos.1 ha) (nonnegg_neg_pos.1 hb))
[GOAL]
case intro.intro.inr.inr.intro.intro.inr.inr
d x y : ℕ
ha : Nonneg { re := -↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := -↑z, im := ↑w }
this : Nonneg { re := -↑(x + z), im := ↑(y + w) }
⊢ Nonneg ({ re := -↑x, im := ↑y } + { re := -↑z, im := ↑w })
[PROOFSTEP]
rw [Nat.cast_add, Nat.cast_add, neg_add] at this 
[GOAL]
case intro.intro.inr.inr.intro.intro.inr.inr
d x y : ℕ
ha : Nonneg { re := -↑x, im := ↑y }
z w : ℕ
hb : Nonneg { re := -↑z, im := ↑w }
this : Nonneg { re := -↑x + -↑z, im := ↑y + ↑w }
⊢ Nonneg ({ re := -↑x, im := ↑y } + { re := -↑z, im := ↑w })
[PROOFSTEP]
rwa [add_def]
  -- Porting note: was
      -- simpa [add_comm] using
      --   nonnegg_neg_pos.2 (sqLe_add (nonnegg_neg_pos.1 ha) (nonnegg_neg_pos.1 hb))
[GOAL]
d : ℕ
a : ℤ√↑d
⊢ Nonneg a ↔ Nonneg (a - 0)
[PROOFSTEP]
simp
[GOAL]
d : ℕ
a b : ℤ√↑d
⊢ a ≤ b ∨ b ≤ a
[PROOFSTEP]
have t := (b - a).nonneg_total
[GOAL]
d : ℕ
a b : ℤ√↑d
t : Nonneg (b - a) ∨ Nonneg (-(b - a))
⊢ a ≤ b ∨ b ≤ a
[PROOFSTEP]
rwa [neg_sub] at t 
[GOAL]
d : ℕ
a : ℤ√↑d
⊢ Nonneg (a - a)
[PROOFSTEP]
simp only [sub_self]
[GOAL]
d : ℕ
a : ℤ√↑d
⊢ Nonneg 0
[PROOFSTEP]
trivial
[GOAL]
d : ℕ
a b c : ℤ√↑d
hab : a ≤ b
hbc : b ≤ c
⊢ a ≤ c
[PROOFSTEP]
simpa [sub_add_sub_cancel'] using hab.add hbc
[GOAL]
d : ℕ
a : ℤ√↑d
⊢ ∃ n, a ≤ ↑n
[PROOFSTEP]
obtain ⟨x, y, (h : a ≤ ⟨x, y⟩)⟩ : ∃ x y : ℕ, Nonneg (⟨x, y⟩ + -a) :=
  match -a with
  | ⟨Int.ofNat x, Int.ofNat y⟩ => ⟨0, 0, by trivial⟩
  | ⟨Int.ofNat x, -[y+1]⟩ => ⟨0, y + 1, by simp [add_def, Int.negSucc_coe, add_assoc]; trivial⟩
  | ⟨-[x+1], Int.ofNat y⟩ => ⟨x + 1, 0, by simp [Int.negSucc_coe, add_assoc]; trivial⟩
  | ⟨-[x+1], -[y+1]⟩ => ⟨x + 1, y + 1, by simp [Int.negSucc_coe, add_assoc]; trivial⟩
[GOAL]
d : ℕ
a : ℤ√↑d
x y : ℕ
⊢ Nonneg ({ re := ↑0, im := ↑0 } + { re := ofNat x, im := ofNat y })
[PROOFSTEP]
trivial
[GOAL]
d : ℕ
a : ℤ√↑d
x y : ℕ
⊢ Nonneg ({ re := ↑0, im := ↑(y + 1) } + { re := ofNat x, im := -[y+1] })
[PROOFSTEP]
simp [add_def, Int.negSucc_coe, add_assoc]
[GOAL]
d : ℕ
a : ℤ√↑d
x y : ℕ
⊢ Nonneg { re := ↑x, im := 0 }
[PROOFSTEP]
trivial
[GOAL]
d : ℕ
a : ℤ√↑d
x y : ℕ
⊢ Nonneg ({ re := ↑(x + 1), im := ↑0 } + { re := -[x+1], im := ofNat y })
[PROOFSTEP]
simp [Int.negSucc_coe, add_assoc]
[GOAL]
d : ℕ
a : ℤ√↑d
x y : ℕ
⊢ Nonneg { re := 0, im := ↑y }
[PROOFSTEP]
trivial
[GOAL]
d : ℕ
a : ℤ√↑d
x y : ℕ
⊢ Nonneg ({ re := ↑(x + 1), im := ↑(y + 1) } + { re := -[x+1], im := -[y+1] })
[PROOFSTEP]
simp [Int.negSucc_coe, add_assoc]
[GOAL]
d : ℕ
a : ℤ√↑d
x y : ℕ
⊢ Nonneg { re := 0, im := 0 }
[PROOFSTEP]
trivial
[GOAL]
case intro.intro
d : ℕ
a : ℤ√↑d
x y : ℕ
h : a ≤ { re := ↑x, im := ↑y }
⊢ ∃ n, a ≤ ↑n
[PROOFSTEP]
refine' ⟨x + d * y, h.trans _⟩
[GOAL]
case intro.intro
d : ℕ
a : ℤ√↑d
x y : ℕ
h : a ≤ { re := ↑x, im := ↑y }
⊢ { re := ↑x, im := ↑y } ≤ ↑(x + d * y)
[PROOFSTEP]
change Nonneg ⟨↑x + d * y - ↑x, 0 - ↑y⟩
[GOAL]
case intro.intro
d : ℕ
a : ℤ√↑d
x y : ℕ
h : a ≤ { re := ↑x, im := ↑y }
⊢ Nonneg { re := ↑x + ↑d * ↑y - ↑x, im := 0 - ↑y }
[PROOFSTEP]
cases' y with y
[GOAL]
case intro.intro.zero
d : ℕ
a : ℤ√↑d
x : ℕ
h : a ≤ { re := ↑x, im := ↑Nat.zero }
⊢ Nonneg { re := ↑x + ↑d * ↑Nat.zero - ↑x, im := 0 - ↑Nat.zero }
[PROOFSTEP]
simp
[GOAL]
case intro.intro.zero
d : ℕ
a : ℤ√↑d
x : ℕ
h : a ≤ { re := ↑x, im := ↑Nat.zero }
⊢ Nonneg { re := 0, im := 0 }
[PROOFSTEP]
trivial
[GOAL]
case intro.intro.succ
d : ℕ
a : ℤ√↑d
x y : ℕ
h : a ≤ { re := ↑x, im := ↑(Nat.succ y) }
⊢ Nonneg { re := ↑x + ↑d * ↑(Nat.succ y) - ↑x, im := 0 - ↑(Nat.succ y) }
[PROOFSTEP]
have h : ∀ y, SqLe y d (d * y) 1 := fun y => by
  simpa [SqLe, mul_comm, mul_left_comm] using Nat.mul_le_mul_right (y * y) (Nat.le_mul_self d)
[GOAL]
d : ℕ
a : ℤ√↑d
x y✝ : ℕ
h : a ≤ { re := ↑x, im := ↑(Nat.succ y✝) }
y : ℕ
⊢ SqLe y d (d * y) 1
[PROOFSTEP]
simpa [SqLe, mul_comm, mul_left_comm] using Nat.mul_le_mul_right (y * y) (Nat.le_mul_self d)
[GOAL]
case intro.intro.succ
d : ℕ
a : ℤ√↑d
x y : ℕ
h✝ : a ≤ { re := ↑x, im := ↑(Nat.succ y) }
h : ∀ (y : ℕ), SqLe y d (d * y) 1
⊢ Nonneg { re := ↑x + ↑d * ↑(Nat.succ y) - ↑x, im := 0 - ↑(Nat.succ y) }
[PROOFSTEP]
rw [show (x : ℤ) + d * Nat.succ y - x = d * Nat.succ y by simp]
[GOAL]
d : ℕ
a : ℤ√↑d
x y : ℕ
h✝ : a ≤ { re := ↑x, im := ↑(Nat.succ y) }
h : ∀ (y : ℕ), SqLe y d (d * y) 1
⊢ ↑x + ↑d * ↑(Nat.succ y) - ↑x = ↑d * ↑(Nat.succ y)
[PROOFSTEP]
simp
[GOAL]
case intro.intro.succ
d : ℕ
a : ℤ√↑d
x y : ℕ
h✝ : a ≤ { re := ↑x, im := ↑(Nat.succ y) }
h : ∀ (y : ℕ), SqLe y d (d * y) 1
⊢ Nonneg { re := ↑d * ↑(Nat.succ y), im := 0 - ↑(Nat.succ y) }
[PROOFSTEP]
exact h (y + 1)
[GOAL]
d : ℕ
a b : ℤ√↑d
ab : a ≤ b
c : ℤ√↑d
⊢ Nonneg (c + b - (c + a))
[PROOFSTEP]
rw [add_sub_add_left_eq_sub]
[GOAL]
d : ℕ
a b : ℤ√↑d
ab : a ≤ b
c : ℤ√↑d
⊢ Nonneg (b - a)
[PROOFSTEP]
exact ab
[GOAL]
d : ℕ
a b c : ℤ√↑d
h : c + a ≤ c + b
⊢ a ≤ b
[PROOFSTEP]
simpa using Zsqrtd.add_le_add_left _ _ h (-c)
[GOAL]
d : ℕ
a : ℤ√↑d
n : ℕ
ha : Nonneg a
⊢ Nonneg (↑n * a)
[PROOFSTEP]
rw [← Int.cast_ofNat n]
[GOAL]
d : ℕ
a : ℤ√↑d
n : ℕ
ha : Nonneg a
⊢ Nonneg (↑↑n * a)
[PROOFSTEP]
exact
  match a, nonneg_cases ha, ha with
  | _, ⟨x, y, Or.inl rfl⟩, _ => by rw [smul_val]; trivial
  | _, ⟨x, y, Or.inr <| Or.inl rfl⟩, ha => by rw [smul_val];
    simpa using nonnegg_pos_neg.2 (sqLe_smul n <| nonnegg_pos_neg.1 ha)
  | _, ⟨x, y, Or.inr <| Or.inr rfl⟩, ha => by rw [smul_val];
    simpa using nonnegg_neg_pos.2 (sqLe_smul n <| nonnegg_neg_pos.1 ha)
[GOAL]
d : ℕ
a : ℤ√↑d
n : ℕ
ha : Nonneg a
x y : ℕ
x✝ : Nonneg { re := ↑x, im := ↑y }
⊢ Nonneg (↑↑n * { re := ↑x, im := ↑y })
[PROOFSTEP]
rw [smul_val]
[GOAL]
d : ℕ
a : ℤ√↑d
n : ℕ
ha : Nonneg a
x y : ℕ
x✝ : Nonneg { re := ↑x, im := ↑y }
⊢ Nonneg { re := ↑n * ↑x, im := ↑n * ↑y }
[PROOFSTEP]
trivial
[GOAL]
d : ℕ
a : ℤ√↑d
n : ℕ
ha✝ : Nonneg a
x y : ℕ
ha : Nonneg { re := ↑x, im := -↑y }
⊢ Nonneg (↑↑n * { re := ↑x, im := -↑y })
[PROOFSTEP]
rw [smul_val]
[GOAL]
d : ℕ
a : ℤ√↑d
n : ℕ
ha✝ : Nonneg a
x y : ℕ
ha : Nonneg { re := ↑x, im := -↑y }
⊢ Nonneg { re := ↑n * ↑x, im := ↑n * -↑y }
[PROOFSTEP]
simpa using nonnegg_pos_neg.2 (sqLe_smul n <| nonnegg_pos_neg.1 ha)
[GOAL]
d : ℕ
a : ℤ√↑d
n : ℕ
ha✝ : Nonneg a
x y : ℕ
ha : Nonneg { re := -↑x, im := ↑y }
⊢ Nonneg (↑↑n * { re := -↑x, im := ↑y })
[PROOFSTEP]
rw [smul_val]
[GOAL]
d : ℕ
a : ℤ√↑d
n : ℕ
ha✝ : Nonneg a
x y : ℕ
ha : Nonneg { re := -↑x, im := ↑y }
⊢ Nonneg { re := ↑n * -↑x, im := ↑n * ↑y }
[PROOFSTEP]
simpa using nonnegg_neg_pos.2 (sqLe_smul n <| nonnegg_neg_pos.1 ha)
[GOAL]
d : ℕ
a : ℤ√↑d
ha✝ : Nonneg a
x y : ℕ
ha : Nonneg { re := ↑x, im := -↑y }
⊢ Nonneg (sqrtd * { re := ↑x, im := -↑y })
[PROOFSTEP]
simp only [muld_val, mul_neg]
[GOAL]
d : ℕ
a : ℤ√↑d
ha✝ : Nonneg a
x y : ℕ
ha : Nonneg { re := ↑x, im := -↑y }
⊢ Nonneg { re := -(↑d * ↑y), im := ↑x }
[PROOFSTEP]
apply nonnegg_neg_pos.2
[GOAL]
d : ℕ
a : ℤ√↑d
ha✝ : Nonneg a
x y : ℕ
ha : Nonneg { re := ↑x, im := -↑y }
⊢ SqLe (d * y) 1 x d
[PROOFSTEP]
simpa [SqLe, mul_comm, mul_left_comm] using Nat.mul_le_mul_left d (nonnegg_pos_neg.1 ha)
[GOAL]
d : ℕ
a : ℤ√↑d
ha✝ : Nonneg a
x y : ℕ
ha : Nonneg { re := -↑x, im := ↑y }
⊢ Nonneg (sqrtd * { re := -↑x, im := ↑y })
[PROOFSTEP]
simp only [muld_val]
[GOAL]
d : ℕ
a : ℤ√↑d
ha✝ : Nonneg a
x y : ℕ
ha : Nonneg { re := -↑x, im := ↑y }
⊢ Nonneg { re := ↑d * ↑y, im := -↑x }
[PROOFSTEP]
apply nonnegg_pos_neg.2
[GOAL]
d : ℕ
a : ℤ√↑d
ha✝ : Nonneg a
x y : ℕ
ha : Nonneg { re := -↑x, im := ↑y }
⊢ SqLe x d (d * y) 1
[PROOFSTEP]
simpa [SqLe, mul_comm, mul_left_comm] using Nat.mul_le_mul_left d (nonnegg_neg_pos.1 ha)
[GOAL]
d x y : ℕ
a : ℤ√↑d
ha : Nonneg a
⊢ Nonneg ({ re := ↑x, im := ↑y } * a)
[PROOFSTEP]
have : (⟨x, y⟩ * a : ℤ√d) = (x : ℤ√d) * a + sqrtd * ((y : ℤ√d) * a) := by
  rw [decompose, right_distrib, mul_assoc, Int.cast_ofNat, Int.cast_ofNat]
[GOAL]
d x y : ℕ
a : ℤ√↑d
ha : Nonneg a
⊢ { re := ↑x, im := ↑y } * a = ↑x * a + sqrtd * (↑y * a)
[PROOFSTEP]
rw [decompose, right_distrib, mul_assoc, Int.cast_ofNat, Int.cast_ofNat]
[GOAL]
d x y : ℕ
a : ℤ√↑d
ha : Nonneg a
this : { re := ↑x, im := ↑y } * a = ↑x * a + sqrtd * (↑y * a)
⊢ Nonneg ({ re := ↑x, im := ↑y } * a)
[PROOFSTEP]
rw [this]
[GOAL]
d x y : ℕ
a : ℤ√↑d
ha : Nonneg a
this : { re := ↑x, im := ↑y } * a = ↑x * a + sqrtd * (↑y * a)
⊢ Nonneg (↑x * a + sqrtd * (↑y * a))
[PROOFSTEP]
exact (nonneg_smul ha).add (nonneg_muld <| nonneg_smul ha)
[GOAL]
d : ℕ
a b : ℤ√↑d
ha✝ : Nonneg a
hb : Nonneg b
x y z w : ℕ
ha : Nonneg { re := -↑x, im := ↑y }
x✝ : Nonneg { re := ↑z, im := ↑w }
⊢ Nonneg ({ re := -↑x, im := ↑y } * { re := ↑z, im := ↑w })
[PROOFSTEP]
rw [mul_comm]
[GOAL]
d : ℕ
a b : ℤ√↑d
ha✝ : Nonneg a
hb : Nonneg b
x y z w : ℕ
ha : Nonneg { re := -↑x, im := ↑y }
x✝ : Nonneg { re := ↑z, im := ↑w }
⊢ Nonneg ({ re := ↑z, im := ↑w } * { re := -↑x, im := ↑y })
[PROOFSTEP]
exact nonneg_mul_lem ha
[GOAL]
d : ℕ
a b : ℤ√↑d
ha✝ : Nonneg a
hb : Nonneg b
x y z w : ℕ
ha : Nonneg { re := ↑x, im := -↑y }
x✝ : Nonneg { re := ↑z, im := ↑w }
⊢ Nonneg ({ re := ↑x, im := -↑y } * { re := ↑z, im := ↑w })
[PROOFSTEP]
rw [mul_comm]
[GOAL]
d : ℕ
a b : ℤ√↑d
ha✝ : Nonneg a
hb : Nonneg b
x y z w : ℕ
ha : Nonneg { re := ↑x, im := -↑y }
x✝ : Nonneg { re := ↑z, im := ↑w }
⊢ Nonneg ({ re := ↑z, im := ↑w } * { re := ↑x, im := -↑y })
[PROOFSTEP]
exact nonneg_mul_lem ha
[GOAL]
d : ℕ
a b : ℤ√↑d
ha✝ : Nonneg a
hb✝ : Nonneg b
x y z w : ℕ
ha : Nonneg { re := -↑x, im := ↑y }
hb : Nonneg { re := -↑z, im := ↑w }
⊢ Nonneg ({ re := -↑x, im := ↑y } * { re := -↑z, im := ↑w })
[PROOFSTEP]
rw [calc
    (⟨-x, y⟩ * ⟨-z, w⟩ : ℤ√d) = ⟨_, _⟩ := rfl
    _ = ⟨x * z + d * y * w, -(x * w + y * z)⟩ := by simp [add_comm]]
[GOAL]
d : ℕ
a b : ℤ√↑d
ha✝ : Nonneg a
hb✝ : Nonneg b
x y z w : ℕ
ha : Nonneg { re := -↑x, im := ↑y }
hb : Nonneg { re := -↑z, im := ↑w }
⊢ {
      re :=
        { re := -↑x, im := ↑y }.re * { re := -↑z, im := ↑w }.re +
          ↑d * { re := -↑x, im := ↑y }.im * { re := -↑z, im := ↑w }.im,
      im :=
        { re := -↑x, im := ↑y }.re * { re := -↑z, im := ↑w }.im +
          { re := -↑x, im := ↑y }.im * { re := -↑z, im := ↑w }.re } =
    { re := ↑x * ↑z + ↑d * ↑y * ↑w, im := -(↑x * ↑w + ↑y * ↑z) }
[PROOFSTEP]
simp [add_comm]
[GOAL]
d : ℕ
a b : ℤ√↑d
ha✝ : Nonneg a
hb✝ : Nonneg b
x y z w : ℕ
ha : Nonneg { re := -↑x, im := ↑y }
hb : Nonneg { re := -↑z, im := ↑w }
⊢ Nonneg { re := ↑x * ↑z + ↑d * ↑y * ↑w, im := -(↑x * ↑w + ↑y * ↑z) }
[PROOFSTEP]
exact nonnegg_pos_neg.2 (sqLe_mul.left (nonnegg_neg_pos.1 ha) (nonnegg_neg_pos.1 hb))
[GOAL]
d : ℕ
a b : ℤ√↑d
ha✝ : Nonneg a
hb✝ : Nonneg b
x y z w : ℕ
ha : Nonneg { re := -↑x, im := ↑y }
hb : Nonneg { re := ↑z, im := -↑w }
⊢ Nonneg ({ re := -↑x, im := ↑y } * { re := ↑z, im := -↑w })
[PROOFSTEP]
rw [calc
    (⟨-x, y⟩ * ⟨z, -w⟩ : ℤ√d) = ⟨_, _⟩ := rfl
    _ = ⟨-(x * z + d * y * w), x * w + y * z⟩ := by simp [add_comm]]
[GOAL]
d : ℕ
a b : ℤ√↑d
ha✝ : Nonneg a
hb✝ : Nonneg b
x y z w : ℕ
ha : Nonneg { re := -↑x, im := ↑y }
hb : Nonneg { re := ↑z, im := -↑w }
⊢ {
      re :=
        { re := -↑x, im := ↑y }.re * { re := ↑z, im := -↑w }.re +
          ↑d * { re := -↑x, im := ↑y }.im * { re := ↑z, im := -↑w }.im,
      im :=
        { re := -↑x, im := ↑y }.re * { re := ↑z, im := -↑w }.im +
          { re := -↑x, im := ↑y }.im * { re := ↑z, im := -↑w }.re } =
    { re := -(↑x * ↑z + ↑d * ↑y * ↑w), im := ↑x * ↑w + ↑y * ↑z }
[PROOFSTEP]
simp [add_comm]
[GOAL]
d : ℕ
a b : ℤ√↑d
ha✝ : Nonneg a
hb✝ : Nonneg b
x y z w : ℕ
ha : Nonneg { re := -↑x, im := ↑y }
hb : Nonneg { re := ↑z, im := -↑w }
⊢ Nonneg { re := -(↑x * ↑z + ↑d * ↑y * ↑w), im := ↑x * ↑w + ↑y * ↑z }
[PROOFSTEP]
exact nonnegg_neg_pos.2 (sqLe_mul.right.left (nonnegg_neg_pos.1 ha) (nonnegg_pos_neg.1 hb))
[GOAL]
d : ℕ
a b : ℤ√↑d
ha✝ : Nonneg a
hb✝ : Nonneg b
x y z w : ℕ
ha : Nonneg { re := ↑x, im := -↑y }
hb : Nonneg { re := -↑z, im := ↑w }
⊢ Nonneg ({ re := ↑x, im := -↑y } * { re := -↑z, im := ↑w })
[PROOFSTEP]
rw [calc
    (⟨x, -y⟩ * ⟨-z, w⟩ : ℤ√d) = ⟨_, _⟩ := rfl
    _ = ⟨-(x * z + d * y * w), x * w + y * z⟩ := by simp [add_comm]]
[GOAL]
d : ℕ
a b : ℤ√↑d
ha✝ : Nonneg a
hb✝ : Nonneg b
x y z w : ℕ
ha : Nonneg { re := ↑x, im := -↑y }
hb : Nonneg { re := -↑z, im := ↑w }
⊢ {
      re :=
        { re := ↑x, im := -↑y }.re * { re := -↑z, im := ↑w }.re +
          ↑d * { re := ↑x, im := -↑y }.im * { re := -↑z, im := ↑w }.im,
      im :=
        { re := ↑x, im := -↑y }.re * { re := -↑z, im := ↑w }.im +
          { re := ↑x, im := -↑y }.im * { re := -↑z, im := ↑w }.re } =
    { re := -(↑x * ↑z + ↑d * ↑y * ↑w), im := ↑x * ↑w + ↑y * ↑z }
[PROOFSTEP]
simp [add_comm]
[GOAL]
d : ℕ
a b : ℤ√↑d
ha✝ : Nonneg a
hb✝ : Nonneg b
x y z w : ℕ
ha : Nonneg { re := ↑x, im := -↑y }
hb : Nonneg { re := -↑z, im := ↑w }
⊢ Nonneg { re := -(↑x * ↑z + ↑d * ↑y * ↑w), im := ↑x * ↑w + ↑y * ↑z }
[PROOFSTEP]
exact nonnegg_neg_pos.2 (sqLe_mul.right.right.left (nonnegg_pos_neg.1 ha) (nonnegg_neg_pos.1 hb))
[GOAL]
d : ℕ
a b : ℤ√↑d
ha✝ : Nonneg a
hb✝ : Nonneg b
x y z w : ℕ
ha : Nonneg { re := ↑x, im := -↑y }
hb : Nonneg { re := ↑z, im := -↑w }
⊢ Nonneg ({ re := ↑x, im := -↑y } * { re := ↑z, im := -↑w })
[PROOFSTEP]
rw [calc
    (⟨x, -y⟩ * ⟨z, -w⟩ : ℤ√d) = ⟨_, _⟩ := rfl
    _ = ⟨x * z + d * y * w, -(x * w + y * z)⟩ := by simp [add_comm]]
[GOAL]
d : ℕ
a b : ℤ√↑d
ha✝ : Nonneg a
hb✝ : Nonneg b
x y z w : ℕ
ha : Nonneg { re := ↑x, im := -↑y }
hb : Nonneg { re := ↑z, im := -↑w }
⊢ {
      re :=
        { re := ↑x, im := -↑y }.re * { re := ↑z, im := -↑w }.re +
          ↑d * { re := ↑x, im := -↑y }.im * { re := ↑z, im := -↑w }.im,
      im :=
        { re := ↑x, im := -↑y }.re * { re := ↑z, im := -↑w }.im +
          { re := ↑x, im := -↑y }.im * { re := ↑z, im := -↑w }.re } =
    { re := ↑x * ↑z + ↑d * ↑y * ↑w, im := -(↑x * ↑w + ↑y * ↑z) }
[PROOFSTEP]
simp [add_comm]
[GOAL]
d : ℕ
a b : ℤ√↑d
ha✝ : Nonneg a
hb✝ : Nonneg b
x y z w : ℕ
ha : Nonneg { re := ↑x, im := -↑y }
hb : Nonneg { re := ↑z, im := -↑w }
⊢ Nonneg { re := ↑x * ↑z + ↑d * ↑y * ↑w, im := -(↑x * ↑w + ↑y * ↑z) }
[PROOFSTEP]
exact nonnegg_pos_neg.2 (sqLe_mul.right.right.right (nonnegg_pos_neg.1 ha) (nonnegg_pos_neg.1 hb))
[GOAL]
d : ℕ
a b : ℤ√↑d
⊢ 0 ≤ a → 0 ≤ b → 0 ≤ a * b
[PROOFSTEP]
simp_rw [← nonneg_iff_zero_le]
[GOAL]
d : ℕ
a b : ℤ√↑d
⊢ Nonneg a → Nonneg b → Nonneg (a * b)
[PROOFSTEP]
exact nonneg_mul
[GOAL]
d : ℕ
dnsq : Nonsquare d
x y : ℕ
h : x * x = d * y * y
g : ℕ := Nat.gcd x y
gpos : g > 0
⊢ False
[PROOFSTEP]
let ⟨m, n, co, (hx : x = m * g), (hy : y = n * g)⟩ := Nat.exists_coprime gpos
[GOAL]
d : ℕ
dnsq : Nonsquare d
x y : ℕ
h : x * x = d * y * y
g : ℕ := Nat.gcd x y
gpos : g > 0
m n : ℕ
co : Nat.coprime m n
hx : x = m * g
hy : y = n * g
⊢ False
[PROOFSTEP]
rw [hx, hy] at h 
[GOAL]
d : ℕ
dnsq : Nonsquare d
x y : ℕ
g : ℕ := Nat.gcd x y
gpos : g > 0
m n : ℕ
h : m * g * (m * g) = d * (n * g) * (n * g)
co : Nat.coprime m n
hx : x = m * g
hy : y = n * g
⊢ False
[PROOFSTEP]
have : m * m = d * (n * n) :=
  by
  refine
    mul_left_cancel₀ (mul_pos gpos gpos).ne'
      ?_
        -- Porting note: was `simpa [mul_comm, mul_left_comm] using h`
  calc
    g * g * (m * m)
    _ = m * g * (m * g) := by ring
    _ = d * (n * g) * (n * g) := h
    _ = g * g * (d * (n * n)) := by ring
[GOAL]
d : ℕ
dnsq : Nonsquare d
x y : ℕ
g : ℕ := Nat.gcd x y
gpos : g > 0
m n : ℕ
h : m * g * (m * g) = d * (n * g) * (n * g)
co : Nat.coprime m n
hx : x = m * g
hy : y = n * g
⊢ m * m = d * (n * n)
[PROOFSTEP]
refine
  mul_left_cancel₀ (mul_pos gpos gpos).ne'
    ?_
      -- Porting note: was `simpa [mul_comm, mul_left_comm] using h`
[GOAL]
d : ℕ
dnsq : Nonsquare d
x y : ℕ
g : ℕ := Nat.gcd x y
gpos : g > 0
m n : ℕ
h : m * g * (m * g) = d * (n * g) * (n * g)
co : Nat.coprime m n
hx : x = m * g
hy : y = n * g
⊢ g * g * (m * m) = g * g * (d * (n * n))
[PROOFSTEP]
calc
  g * g * (m * m)
  _ = m * g * (m * g) := by ring
  _ = d * (n * g) * (n * g) := h
  _ = g * g * (d * (n * n)) := by ring
[GOAL]
d : ℕ
dnsq : Nonsquare d
x y : ℕ
g : ℕ := Nat.gcd x y
gpos : g > 0
m n : ℕ
h : m * g * (m * g) = d * (n * g) * (n * g)
co : Nat.coprime m n
hx : x = m * g
hy : y = n * g
⊢ g * g * (m * m) = m * g * (m * g)
[PROOFSTEP]
ring
[GOAL]
d : ℕ
dnsq : Nonsquare d
x y : ℕ
g : ℕ := Nat.gcd x y
gpos : g > 0
m n : ℕ
h : m * g * (m * g) = d * (n * g) * (n * g)
co : Nat.coprime m n
hx : x = m * g
hy : y = n * g
⊢ d * (n * g) * (n * g) = g * g * (d * (n * n))
[PROOFSTEP]
ring
[GOAL]
d : ℕ
dnsq : Nonsquare d
x y : ℕ
g : ℕ := Nat.gcd x y
gpos : g > 0
m n : ℕ
h : m * g * (m * g) = d * (n * g) * (n * g)
co : Nat.coprime m n
hx : x = m * g
hy : y = n * g
this : m * m = d * (n * n)
⊢ False
[PROOFSTEP]
have co2 :=
  let co1 := co.mul_right co
  co1.mul co1
[GOAL]
d : ℕ
dnsq : Nonsquare d
x y : ℕ
g : ℕ := Nat.gcd x y
gpos : g > 0
m n : ℕ
h : m * g * (m * g) = d * (n * g) * (n * g)
co : Nat.coprime m n
hx : x = m * g
hy : y = n * g
this : m * m = d * (n * n)
co2 : Nat.coprime (m * m) (n * n)
⊢ False
[PROOFSTEP]
exact
  Nonsquare.ns d m (Nat.dvd_antisymm (by rw [this]; apply dvd_mul_right) <| co2.dvd_of_dvd_mul_right <| by simp [this])
[GOAL]
d : ℕ
dnsq : Nonsquare d
x y : ℕ
g : ℕ := Nat.gcd x y
gpos : g > 0
m n : ℕ
h : m * g * (m * g) = d * (n * g) * (n * g)
co : Nat.coprime m n
hx : x = m * g
hy : y = n * g
this : m * m = d * (n * n)
co2 : Nat.coprime (m * m) (n * n)
⊢ d ∣ m * m
[PROOFSTEP]
rw [this]
[GOAL]
d : ℕ
dnsq : Nonsquare d
x y : ℕ
g : ℕ := Nat.gcd x y
gpos : g > 0
m n : ℕ
h : m * g * (m * g) = d * (n * g) * (n * g)
co : Nat.coprime m n
hx : x = m * g
hy : y = n * g
this : m * m = d * (n * n)
co2 : Nat.coprime (m * m) (n * n)
⊢ d ∣ d * (n * n)
[PROOFSTEP]
apply dvd_mul_right
[GOAL]
d : ℕ
dnsq : Nonsquare d
x y : ℕ
g : ℕ := Nat.gcd x y
gpos : g > 0
m n : ℕ
h : m * g * (m * g) = d * (n * g) * (n * g)
co : Nat.coprime m n
hx : x = m * g
hy : y = n * g
this : m * m = d * (n * n)
co2 : Nat.coprime (m * m) (n * n)
⊢ m * m ∣ d * (n * n)
[PROOFSTEP]
simp [this]
[GOAL]
d : ℕ
dnsq : Nonsquare d
x y : ℤ
h : x * x = ↑d * y * y
⊢ x = 0 ∧ y = 0
[PROOFSTEP]
rw [mul_assoc, ← Int.natAbs_mul_self, ← Int.natAbs_mul_self, ← Int.ofNat_mul, ← mul_assoc] at h 
[GOAL]
d : ℕ
dnsq : Nonsquare d
x y : ℤ
h : ↑(Int.natAbs x * Int.natAbs x) = ↑(d * Int.natAbs y * Int.natAbs y)
⊢ x = 0 ∧ y = 0
[PROOFSTEP]
exact
  let ⟨h1, h2⟩ := divides_sq_eq_zero (Int.ofNat.inj h)
  ⟨Int.natAbs_eq_zero.mp h1, Int.natAbs_eq_zero.mp h2⟩
[GOAL]
d : ℕ
dnsq : Nonsquare d
x y : ℕ
e : (x + 1) * (x + 1) = d * (y + 1) * (y + 1)
⊢ False
[PROOFSTEP]
have t := (divides_sq_eq_zero e).left
[GOAL]
d : ℕ
dnsq : Nonsquare d
x y : ℕ
e : (x + 1) * (x + 1) = d * (y + 1) * (y + 1)
t : x + 1 = 0
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
d : ℕ
dnsq : Nonsquare d
x : ℕ
xy : Nonneg { re := -[x+1], im := 0 }
x✝ : Nonneg (-{ re := -[x+1], im := 0 })
⊢ 0 < 1
[PROOFSTEP]
decide
[GOAL]
d : ℕ
dnsq : Nonsquare d
x : ℕ
x✝ : Nonneg { re := ↑(x + 1), im := 0 }
yx : Nonneg (-{ re := ↑(x + 1), im := 0 })
⊢ 0 < 1
[PROOFSTEP]
decide
[GOAL]
d : ℕ
dnsq : Nonsquare d
x y : ℕ
xy : SqLe (y + 1) d (x + 1) 1
yx : SqLe (Nat.add x 0 + 1) 1 (Nat.succ y) d
⊢ { re := ↑(x + 1), im := -[y+1] } = 0
[PROOFSTEP]
let t := le_antisymm yx xy
[GOAL]
d : ℕ
dnsq : Nonsquare d
x y : ℕ
xy : SqLe (y + 1) d (x + 1) 1
yx : SqLe (Nat.add x 0 + 1) 1 (Nat.succ y) d
t : 1 * (Nat.add x 0 + 1) * (Nat.add x 0 + 1) = d * Nat.succ y * Nat.succ y := le_antisymm yx xy
⊢ { re := ↑(x + 1), im := -[y+1] } = 0
[PROOFSTEP]
rw [one_mul] at t 
[GOAL]
d : ℕ
dnsq : Nonsquare d
x y : ℕ
xy : SqLe (y + 1) d (x + 1) 1
yx : SqLe (Nat.add x 0 + 1) 1 (Nat.succ y) d
t : (Nat.add x 0 + 1) * (Nat.add x 0 + 1) = d * Nat.succ y * Nat.succ y
⊢ { re := ↑(x + 1), im := -[y+1] } = 0
[PROOFSTEP]
exact absurd t (not_divides_sq _ _)
[GOAL]
d : ℕ
dnsq : Nonsquare d
x y : ℕ
xy : SqLe (x + 1) 1 (y + 1) d
yx : SqLe (Nat.add y 0 + 1) d (Nat.succ x) 1
⊢ { re := -[x+1], im := ↑(y + 1) } = 0
[PROOFSTEP]
let t := le_antisymm xy yx
[GOAL]
d : ℕ
dnsq : Nonsquare d
x y : ℕ
xy : SqLe (x + 1) 1 (y + 1) d
yx : SqLe (Nat.add y 0 + 1) d (Nat.succ x) 1
t : 1 * (x + 1) * (x + 1) = d * (y + 1) * (y + 1) := le_antisymm xy yx
⊢ { re := -[x+1], im := ↑(y + 1) } = 0
[PROOFSTEP]
rw [one_mul] at t 
[GOAL]
d : ℕ
dnsq : Nonsquare d
x y : ℕ
xy : SqLe (x + 1) 1 (y + 1) d
yx : SqLe (Nat.add y 0 + 1) d (Nat.succ x) 1
t : (x + 1) * (x + 1) = d * (y + 1) * (y + 1)
⊢ { re := -[x+1], im := ↑(y + 1) } = 0
[PROOFSTEP]
exact absurd t (not_divides_sq _ _)
[GOAL]
d : ℕ
dnsq : Nonsquare d
a b : ℤ√↑d
ab : a ≤ b
ba : b ≤ a
⊢ Nonneg (-(a - b))
[PROOFSTEP]
rwa [neg_sub]
[GOAL]
d : ℕ
dnsq : Nonsquare d
x y z w : ℤ
h : { re := x, im := y } * { re := z, im := w } = 0
⊢ { re := x, im := y } = 0 ∨ { re := z, im := w } = 0
[PROOFSTEP]
injection h with h1 h2
[GOAL]
d : ℕ
dnsq : Nonsquare d
x y z w : ℤ
h1 : { re := x, im := y }.re * { re := z, im := w }.re + ↑d * { re := x, im := y }.im * { re := z, im := w }.im = 0
h2 : { re := x, im := y }.re * { re := z, im := w }.im + { re := x, im := y }.im * { re := z, im := w }.re = 0
⊢ { re := x, im := y } = 0 ∨ { re := z, im := w } = 0
[PROOFSTEP]
have h1 : x * z = -(d * y * w) := eq_neg_of_add_eq_zero_left h1
[GOAL]
d : ℕ
dnsq : Nonsquare d
x y z w : ℤ
h1✝ : { re := x, im := y }.re * { re := z, im := w }.re + ↑d * { re := x, im := y }.im * { re := z, im := w }.im = 0
h2 : { re := x, im := y }.re * { re := z, im := w }.im + { re := x, im := y }.im * { re := z, im := w }.re = 0
h1 : x * z = -(↑d * y * w)
⊢ { re := x, im := y } = 0 ∨ { re := z, im := w } = 0
[PROOFSTEP]
have h2 : x * w = -(y * z) := eq_neg_of_add_eq_zero_left h2
[GOAL]
d : ℕ
dnsq : Nonsquare d
x y z w : ℤ
h1✝ : { re := x, im := y }.re * { re := z, im := w }.re + ↑d * { re := x, im := y }.im * { re := z, im := w }.im = 0
h2✝ : { re := x, im := y }.re * { re := z, im := w }.im + { re := x, im := y }.im * { re := z, im := w }.re = 0
h1 : x * z = -(↑d * y * w)
h2 : x * w = -(y * z)
⊢ { re := x, im := y } = 0 ∨ { re := z, im := w } = 0
[PROOFSTEP]
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
[GOAL]
d : ℕ
dnsq : Nonsquare d
x y z w : ℤ
h1✝ : { re := x, im := y }.re * { re := z, im := w }.re + ↑d * { re := x, im := y }.im * { re := z, im := w }.im = 0
h2✝ : { re := x, im := y }.re * { re := z, im := w }.im + { re := x, im := y }.im * { re := z, im := w }.re = 0
h1 : x * z = -(↑d * y * w)
h2 : x * w = -(y * z)
fin : x * x = ↑d * y * y → { re := x, im := y } = 0
⊢ { re := x, im := y } = 0 ∨ { re := z, im := w } = 0
[PROOFSTEP]
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]
[GOAL]
d : ℕ
dnsq : Nonsquare d
x y z w : ℤ
h1✝ : { re := x, im := y }.re * { re := z, im := w }.re + ↑d * { re := x, im := y }.im * { re := z, im := w }.im = 0
h2✝ : { re := x, im := y }.re * { re := z, im := w }.im + { re := x, im := y }.im * { re := z, im := w }.re = 0
h1 : x * z = -(↑d * y * w)
h2 : x * w = -(y * z)
fin : x * x = ↑d * y * y → { re := x, im := y } = 0
z0 : z = 0
w0 : ¬w = 0
⊢ x * x * w = -y * (x * z)
[PROOFSTEP]
simp [h2, mul_assoc, mul_left_comm]
[GOAL]
d : ℕ
dnsq : Nonsquare d
x y z w : ℤ
h1✝ : { re := x, im := y }.re * { re := z, im := w }.re + ↑d * { re := x, im := y }.im * { re := z, im := w }.im = 0
h2✝ : { re := x, im := y }.re * { re := z, im := w }.im + { re := x, im := y }.im * { re := z, im := w }.re = 0
h1 : x * z = -(↑d * y * w)
h2 : x * w = -(y * z)
fin : x * x = ↑d * y * y → { re := x, im := y } = 0
z0 : z = 0
w0 : ¬w = 0
⊢ -y * (x * z) = ↑d * y * y * w
[PROOFSTEP]
simp [h1, mul_assoc, mul_left_comm]
[GOAL]
d : ℕ
dnsq : Nonsquare d
x y z w : ℤ
h1✝ : { re := x, im := y }.re * { re := z, im := w }.re + ↑d * { re := x, im := y }.im * { re := z, im := w }.im = 0
h2✝ : { re := x, im := y }.re * { re := z, im := w }.im + { re := x, im := y }.im * { re := z, im := w }.re = 0
h1 : x * z = -(↑d * y * w)
h2 : x * w = -(y * z)
fin : x * x = ↑d * y * y → { re := x, im := y } = 0
z0 : ¬z = 0
⊢ x * x * z = ↑d * -y * (x * w)
[PROOFSTEP]
simp [h1, mul_assoc, mul_left_comm]
[GOAL]
d : ℕ
dnsq : Nonsquare d
x y z w : ℤ
h1✝ : { re := x, im := y }.re * { re := z, im := w }.re + ↑d * { re := x, im := y }.im * { re := z, im := w }.im = 0
h2✝ : { re := x, im := y }.re * { re := z, im := w }.im + { re := x, im := y }.im * { re := z, im := w }.re = 0
h1 : x * z = -(↑d * y * w)
h2 : x * w = -(y * z)
fin : x * x = ↑d * y * y → { re := x, im := y } = 0
z0 : ¬z = 0
⊢ ↑d * -y * (x * w) = ↑d * y * y * z
[PROOFSTEP]
simp [h2, mul_assoc, mul_left_comm]
[GOAL]
d : ℕ
dnsq : Nonsquare d
src✝² : CommRing (ℤ√↑d) := commRing
src✝¹ : LinearOrder (ℤ√↑d) := linearOrder
src✝ : Nontrivial (ℤ√↑d) := nontrivial
⊢ 0 ≤ 1
[PROOFSTEP]
trivial
[GOAL]
d : ℕ
dnsq : Nonsquare d
⊢ LinearOrderedRing (ℤ√↑d)
[PROOFSTEP]
infer_instance
[GOAL]
d : ℕ
dnsq : Nonsquare d
⊢ OrderedRing (ℤ√↑d)
[PROOFSTEP]
infer_instance
[GOAL]
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
⊢ norm a = 0 ↔ a = 0
[PROOFSTEP]
refine' ⟨fun ha => ext.mpr _, fun h => by rw [h, norm_zero]⟩
[GOAL]
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
h : a = 0
⊢ norm a = 0
[PROOFSTEP]
rw [h, norm_zero]
[GOAL]
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : norm a = 0
⊢ a.re = 0.re ∧ a.im = 0.im
[PROOFSTEP]
dsimp only [norm] at ha 
[GOAL]
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : a.re * a.re - d * a.im * a.im = 0
⊢ a.re = 0.re ∧ a.im = 0.im
[PROOFSTEP]
rw [sub_eq_zero] at ha 
[GOAL]
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : a.re * a.re = d * a.im * a.im
⊢ a.re = 0.re ∧ a.im = 0.im
[PROOFSTEP]
by_cases h : 0 ≤ d
[GOAL]
case pos
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : a.re * a.re = d * a.im * a.im
h : 0 ≤ d
⊢ a.re = 0.re ∧ a.im = 0.im
[PROOFSTEP]
obtain ⟨d', rfl⟩ := Int.eq_ofNat_of_zero_le h
[GOAL]
case pos.intro
d' : ℕ
h_nonsquare : ∀ (n : ℤ), ↑d' ≠ n * n
a : ℤ√↑d'
ha : a.re * a.re = ↑d' * a.im * a.im
h : 0 ≤ ↑d'
⊢ a.re = 0.re ∧ a.im = 0.im
[PROOFSTEP]
haveI : Nonsquare d' := ⟨fun n h => h_nonsquare n <| by exact_mod_cast h⟩
[GOAL]
d' : ℕ
h_nonsquare : ∀ (n : ℤ), ↑d' ≠ n * n
a : ℤ√↑d'
ha : a.re * a.re = ↑d' * a.im * a.im
h✝ : 0 ≤ ↑d'
n : ℕ
h : d' = n * n
⊢ ↑d' = ↑n * ↑n
[PROOFSTEP]
exact_mod_cast h
[GOAL]
case pos.intro
d' : ℕ
h_nonsquare : ∀ (n : ℤ), ↑d' ≠ n * n
a : ℤ√↑d'
ha : a.re * a.re = ↑d' * a.im * a.im
h : 0 ≤ ↑d'
this : Nonsquare d'
⊢ a.re = 0.re ∧ a.im = 0.im
[PROOFSTEP]
exact divides_sq_eq_zero_z ha
[GOAL]
case neg
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : a.re * a.re = d * a.im * a.im
h : ¬0 ≤ d
⊢ a.re = 0.re ∧ a.im = 0.im
[PROOFSTEP]
push_neg at h 
[GOAL]
case neg
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : a.re * a.re = d * a.im * a.im
h : d < 0
⊢ a.re = 0.re ∧ a.im = 0.im
[PROOFSTEP]
suffices a.re * a.re = 0 by
  rw [eq_zero_of_mul_self_eq_zero this] at ha ⊢
  simpa only [true_and_iff, or_self_right, zero_re, zero_im, eq_self_iff_true, zero_eq_mul, mul_zero, mul_eq_zero, h.ne,
    false_or_iff, or_self_iff] using ha
[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 = 0.re ∧ a.im = 0.im
[PROOFSTEP]
rw [eq_zero_of_mul_self_eq_zero this] at ha ⊢
[GOAL]
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : 0 * 0 = d * a.im * a.im
h : d < 0
this : a.re * a.re = 0
⊢ 0 = 0.re ∧ a.im = 0.im
[PROOFSTEP]
simpa only [true_and_iff, or_self_right, zero_re, zero_im, eq_self_iff_true, zero_eq_mul, mul_zero, mul_eq_zero, h.ne,
  false_or_iff, or_self_iff] using ha
[GOAL]
case neg
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
[PROOFSTEP]
apply _root_.le_antisymm _ (mul_self_nonneg _)
[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
[PROOFSTEP]
rw [ha, mul_assoc]
[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
[PROOFSTEP]
exact mul_nonpos_of_nonpos_of_nonneg h.le (mul_self_nonneg _)
[GOAL]
R : Type
inst✝ : Ring R
d : ℤ
f g : ℤ√d →+* R
h : ↑f sqrtd = ↑g sqrtd
⊢ f = g
[PROOFSTEP]
ext ⟨x_re, x_im⟩
[GOAL]
case a.mk
R : Type
inst✝ : Ring R
d : ℤ
f g : ℤ√d →+* R
h : ↑f sqrtd = ↑g sqrtd
x_re x_im : ℤ
⊢ ↑f { re := x_re, im := x_im } = ↑g { re := x_re, im := x_im }
[PROOFSTEP]
simp [decompose, h]
[GOAL]
R : Type
inst✝ : CommRing R
d : ℤ
r : { r // r * r = ↑d }
⊢ (fun a => ↑a.re + ↑a.im * ↑r) 1 = 1
[PROOFSTEP]
simp
[GOAL]
R : Type
inst✝ : CommRing R
d : ℤ
r : { r // r * r = ↑d }
a b : ℤ√d
⊢ OneHom.toFun { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) } (a * b) =
    OneHom.toFun { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) } a *
      OneHom.toFun { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) } b
[PROOFSTEP]
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
[GOAL]
R : Type
inst✝ : CommRing R
d : ℤ
r : { r // r * r = ↑d }
a b : ℤ√d
⊢ (↑a.re + ↑a.im * ↑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)
[PROOFSTEP]
ring
[GOAL]
R : Type
inst✝ : CommRing R
d : ℤ
r : { r // r * r = ↑d }
a b : ℤ√d
this :
  (↑a.re + ↑a.im * ↑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)
⊢ OneHom.toFun { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) } (a * b) =
    OneHom.toFun { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) } a *
      OneHom.toFun { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) } b
[PROOFSTEP]
simp [this, r.prop]
[GOAL]
R : Type
inst✝ : CommRing R
d : ℤ
r : { r // r * r = ↑d }
a b : ℤ√d
this :
  (↑a.re + ↑a.im * ↑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)
⊢ ↑a.re * ↑b.re + ↑d * ↑a.im * ↑b.im + (↑a.re * ↑b.im + ↑a.im * ↑b.re) * ↑r =
    ↑a.re * ↑b.re + (↑a.re * ↑b.im + ↑a.im * ↑b.re) * ↑r + ↑a.im * ↑b.im * ↑d
[PROOFSTEP]
ring
[GOAL]
R : Type
inst✝ : CommRing R
d : ℤ
r : { r // r * r = ↑d }
⊢ OneHom.toFun
      (↑{ toOneHom := { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) },
          map_mul' :=
            (_ :
              ∀ (a b : ℤ√d),
                OneHom.toFun { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) } (a * b) =
                  OneHom.toFun { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) } a *
                    OneHom.toFun { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) } b) })
      0 =
    0
[PROOFSTEP]
simp
[GOAL]
R : Type
inst✝ : CommRing R
d : ℤ
r : { r // r * r = ↑d }
a b : ℤ√d
⊢ OneHom.toFun
      (↑{ toOneHom := { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) },
          map_mul' :=
            (_ :
              ∀ (a b : ℤ√d),
                OneHom.toFun { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) } (a * b) =
                  OneHom.toFun { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) } a *
                    OneHom.toFun { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) } b) })
      (a + b) =
    OneHom.toFun
        (↑{ toOneHom := { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) },
            map_mul' :=
              (_ :
                ∀ (a b : ℤ√d),
                  OneHom.toFun { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) } (a * b) =
                    OneHom.toFun { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) } a *
                      OneHom.toFun { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) } b) })
        a +
      OneHom.toFun
        (↑{ toOneHom := { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) },
            map_mul' :=
              (_ :
                ∀ (a b : ℤ√d),
                  OneHom.toFun { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) } (a * b) =
                    OneHom.toFun { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) } a *
                      OneHom.toFun { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) } b) })
        b
[PROOFSTEP]
simp
[GOAL]
R : Type
inst✝ : CommRing R
d : ℤ
r : { r // r * r = ↑d }
a b : ℤ√d
⊢ ↑a.re + ↑b.re + (↑a.im + ↑b.im) * ↑r = ↑a.re + ↑a.im * ↑r + (↑b.re + ↑b.im * ↑r)
[PROOFSTEP]
ring
[GOAL]
R : Type
inst✝ : CommRing R
d : ℤ
f : ℤ√d →+* R
⊢ ↑f sqrtd * ↑f sqrtd = ↑d
[PROOFSTEP]
rw [← f.map_mul, dmuld, map_intCast]
[GOAL]
R : Type
inst✝ : CommRing R
d : ℤ
r : { r // r * r = ↑d }
⊢ (fun f => { val := ↑f sqrtd, property := (_ : ↑f sqrtd * ↑f sqrtd = ↑d) })
      ((fun r =>
          {
            toMonoidHom :=
              { toOneHom := { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) },
                map_mul' :=
                  (_ :
                    ∀ (a b : ℤ√d),
                      OneHom.toFun { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) }
                          (a * b) =
                        OneHom.toFun { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) } a *
                          OneHom.toFun { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) }
                            b) },
            map_zero' := (_ : ↑0 + ↑0 * ↑r = 0),
            map_add' :=
              (_ :
                ∀ (a b : ℤ√d),
                  OneHom.toFun
                      (↑{ toOneHom := { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) },
                          map_mul' :=
                            (_ :
                              ∀ (a b : ℤ√d),
                                OneHom.toFun
                                    { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) }
                                    (a * b) =
                                  OneHom.toFun
                                      { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) } a *
                                    OneHom.toFun
                                      { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) } b) })
                      (a + b) =
                    OneHom.toFun
                        (↑{ toOneHom := { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) },
                            map_mul' :=
                              (_ :
                                ∀ (a b : ℤ√d),
                                  OneHom.toFun
                                      { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) }
                                      (a * b) =
                                    OneHom.toFun
                                        { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) } a *
                                      OneHom.toFun
                                        { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) }
                                        b) })
                        a +
                      OneHom.toFun
                        (↑{ toOneHom := { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) },
                            map_mul' :=
                              (_ :
                                ∀ (a b : ℤ√d),
                                  OneHom.toFun
                                      { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) }
                                      (a * b) =
                                    OneHom.toFun
                                        { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) } a *
                                      OneHom.toFun
                                        { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) }
                                        b) })
                        b) })
        r) =
    r
[PROOFSTEP]
ext
[GOAL]
case a
R : Type
inst✝ : CommRing R
d : ℤ
r : { r // r * r = ↑d }
⊢ ↑((fun f => { val := ↑f sqrtd, property := (_ : ↑f sqrtd * ↑f sqrtd = ↑d) })
        ((fun r =>
            {
              toMonoidHom :=
                { toOneHom := { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) },
                  map_mul' :=
                    (_ :
                      ∀ (a b : ℤ√d),
                        OneHom.toFun { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) }
                            (a * b) =
                          OneHom.toFun { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) } a *
                            OneHom.toFun { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) }
                              b) },
              map_zero' := (_ : ↑0 + ↑0 * ↑r = 0),
              map_add' :=
                (_ :
                  ∀ (a b : ℤ√d),
                    OneHom.toFun
                        (↑{ toOneHom := { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) },
                            map_mul' :=
                              (_ :
                                ∀ (a b : ℤ√d),
                                  OneHom.toFun
                                      { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) }
                                      (a * b) =
                                    OneHom.toFun
                                        { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) } a *
                                      OneHom.toFun
                                        { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) }
                                        b) })
                        (a + b) =
                      OneHom.toFun
                          (↑{ toOneHom := { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) },
                              map_mul' :=
                                (_ :
                                  ∀ (a b : ℤ√d),
                                    OneHom.toFun
                                        { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) }
                                        (a * b) =
                                      OneHom.toFun
                                          { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) }
                                          a *
                                        OneHom.toFun
                                          { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) }
                                          b) })
                          a +
                        OneHom.toFun
                          (↑{ toOneHom := { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) },
                              map_mul' :=
                                (_ :
                                  ∀ (a b : ℤ√d),
                                    OneHom.toFun
                                        { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) }
                                        (a * b) =
                                      OneHom.toFun
                                          { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) }
                                          a *
                                        OneHom.toFun
                                          { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) }
                                          b) })
                          b) })
          r)) =
    ↑r
[PROOFSTEP]
simp
[GOAL]
R : Type
inst✝ : CommRing R
d : ℤ
f : ℤ√d →+* R
⊢ (fun r =>
        {
          toMonoidHom :=
            { toOneHom := { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) },
              map_mul' :=
                (_ :
                  ∀ (a b : ℤ√d),
                    OneHom.toFun { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) } (a * b) =
                      OneHom.toFun { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) } a *
                        OneHom.toFun { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) } b) },
          map_zero' := (_ : ↑0 + ↑0 * ↑r = 0),
          map_add' :=
            (_ :
              ∀ (a b : ℤ√d),
                OneHom.toFun
                    (↑{ toOneHom := { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) },
                        map_mul' :=
                          (_ :
                            ∀ (a b : ℤ√d),
                              OneHom.toFun { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) }
                                  (a * b) =
                                OneHom.toFun
                                    { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) } a *
                                  OneHom.toFun
                                    { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) } b) })
                    (a + b) =
                  OneHom.toFun
                      (↑{ toOneHom := { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) },
                          map_mul' :=
                            (_ :
                              ∀ (a b : ℤ√d),
                                OneHom.toFun
                                    { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) }
                                    (a * b) =
                                  OneHom.toFun
                                      { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) } a *
                                    OneHom.toFun
                                      { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) } b) })
                      a +
                    OneHom.toFun
                      (↑{ toOneHom := { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) },
                          map_mul' :=
                            (_ :
                              ∀ (a b : ℤ√d),
                                OneHom.toFun
                                    { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) }
                                    (a * b) =
                                  OneHom.toFun
                                      { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) } a *
                                    OneHom.toFun
                                      { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) } b) })
                      b) })
      ((fun f => { val := ↑f sqrtd, property := (_ : ↑f sqrtd * ↑f sqrtd = ↑d) }) f) =
    f
[PROOFSTEP]
refine hom_ext _ _ ?_
[GOAL]
R : Type
inst✝ : CommRing R
d : ℤ
f : ℤ√d →+* R
⊢ ↑((fun r =>
            {
              toMonoidHom :=
                { toOneHom := { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) },
                  map_mul' :=
                    (_ :
                      ∀ (a b : ℤ√d),
                        OneHom.toFun { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) }
                            (a * b) =
                          OneHom.toFun { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) } a *
                            OneHom.toFun { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) }
                              b) },
              map_zero' := (_ : ↑0 + ↑0 * ↑r = 0),
              map_add' :=
                (_ :
                  ∀ (a b : ℤ√d),
                    OneHom.toFun
                        (↑{ toOneHom := { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) },
                            map_mul' :=
                              (_ :
                                ∀ (a b : ℤ√d),
                                  OneHom.toFun
                                      { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) }
                                      (a * b) =
                                    OneHom.toFun
                                        { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) } a *
                                      OneHom.toFun
                                        { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) }
                                        b) })
                        (a + b) =
                      OneHom.toFun
                          (↑{ toOneHom := { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) },
                              map_mul' :=
                                (_ :
                                  ∀ (a b : ℤ√d),
                                    OneHom.toFun
                                        { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) }
                                        (a * b) =
                                      OneHom.toFun
                                          { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) }
                                          a *
                                        OneHom.toFun
                                          { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) }
                                          b) })
                          a +
                        OneHom.toFun
                          (↑{ toOneHom := { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) },
                              map_mul' :=
                                (_ :
                                  ∀ (a b : ℤ√d),
                                    OneHom.toFun
                                        { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) }
                                        (a * b) =
                                      OneHom.toFun
                                          { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) }
                                          a *
                                        OneHom.toFun
                                          { toFun := fun a => ↑a.re + ↑a.im * ↑r, map_one' := (_ : ↑1 + ↑0 * ↑r = 1) }
                                          b) })
                          b) })
          ((fun f => { val := ↑f sqrtd, property := (_ : ↑f sqrtd * ↑f sqrtd = ↑d) }) f))
      sqrtd =
    ↑f sqrtd
[PROOFSTEP]
simp
[GOAL]
R : Type
inst✝¹ : CommRing R
inst✝ : CharZero R
d : ℤ
r : { r // r * r = ↑d }
hd : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : ↑(↑lift r) a = 0
⊢ a = 0
[PROOFSTEP]
have h_inj : Function.Injective ((↑) : ℤ → R) := Int.cast_injective
[GOAL]
R : Type
inst✝¹ : CommRing R
inst✝ : CharZero R
d : ℤ
r : { r // r * r = ↑d }
hd : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : ↑(↑lift r) a = 0
h_inj : Function.Injective Int.cast
⊢ a = 0
[PROOFSTEP]
suffices lift r a.norm = 0
  by
  simp only [coe_int_re, add_zero, lift_apply_apply, coe_int_im, Int.cast_zero, zero_mul] at this 
  rwa [← Int.cast_zero, h_inj.eq_iff, norm_eq_zero hd] at this 
[GOAL]
R : Type
inst✝¹ : CommRing R
inst✝ : CharZero R
d : ℤ
r : { r // r * r = ↑d }
hd : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : ↑(↑lift r) a = 0
h_inj : Function.Injective Int.cast
this : ↑(↑lift r) ↑(norm a) = 0
⊢ a = 0
[PROOFSTEP]
simp only [coe_int_re, add_zero, lift_apply_apply, coe_int_im, Int.cast_zero, zero_mul] at this 
[GOAL]
R : Type
inst✝¹ : CommRing R
inst✝ : CharZero R
d : ℤ
r : { r // r * r = ↑d }
hd : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : ↑(↑lift r) a = 0
h_inj : Function.Injective Int.cast
this : ↑(norm a) = 0
⊢ a = 0
[PROOFSTEP]
rwa [← Int.cast_zero, h_inj.eq_iff, norm_eq_zero hd] at this 
[GOAL]
R : Type
inst✝¹ : CommRing R
inst✝ : CharZero R
d : ℤ
r : { r // r * r = ↑d }
hd : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : ↑(↑lift r) a = 0
h_inj : Function.Injective Int.cast
⊢ ↑(↑lift r) ↑(norm a) = 0
[PROOFSTEP]
rw [norm_eq_mul_conj, RingHom.map_mul, ha, zero_mul]
[GOAL]
R : Type
inst✝ : CommRing R
d : ℤ
a : ℤ√d
⊢ norm a = 1 ↔ a ∈ unitary (ℤ√d)
[PROOFSTEP]
rw [unitary.mem_iff_self_mul_star, ← norm_eq_mul_conj]
[GOAL]
R : Type
inst✝ : CommRing R
d : ℤ
a : ℤ√d
⊢ norm a = 1 ↔ ↑(norm a) = 1
[PROOFSTEP]
norm_cast
