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
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
injection h with h1 h2
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
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
have h1 : x * z = -(d * y * w) := eq_neg_of_add_eq_zero_left h1
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
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
have h2 : x * w = -(y * z) := eq_neg_of_add_eq_zero_left h2
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
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
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
no goals
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
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]
no goals
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)
simp [h2, mul_assoc, mul_left_comm]
no goals
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
simp [h1, mul_assoc, mul_left_comm]
no goals
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)
simp [h1, mul_assoc, mul_left_comm]
no goals
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
simp [h2, mul_assoc, mul_left_comm]