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
d : ℕ
dnsq : Nonsquare d
x y : ℕ
h : x * x = d * y * y
g : ℕ := Nat.gcd x y
gpos : g > 0
⊢ False
let ⟨m, n, co, (hx : x = m * g), (hy : y = n * g)⟩ := Nat.exists_coprime gpos
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
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
rw [hx, hy] at h
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
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
have : m * m = d * (n * n) := by
  refine mul_left_cancel₀ (mul_pos gpos gpos).ne' ?_
  calc
    g * g * (m * m)
    _ = m * g * (m * g) := by ring
    _ = d * (n * g) * (n * g) := h
    _ = g * g * (d * (n * n)) := by ring
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
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
have co2 :=
  let co1 := co.mul_right co
  co1.mul co1
no goals
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
exact
  Nonsquare.ns d m
    (Nat.dvd_antisymm (by rw [this]; apply dvd_mul_right) <|
      co2.dvd_of_dvd_mul_right <| by simp [this])
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))
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)
refine mul_left_cancel₀ (mul_pos gpos gpos).ne' ?_
no goals
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))
calc
  g * g * (m * m)
  _ = m * g * (m * g) := by ring
  _ = d * (n * g) * (n * g) := h
  _ = g * g * (d * (n * n)) := by ring
no goals
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)
ring
no goals
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))
ring
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)
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
rw [this]
no goals
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)
apply dvd_mul_right
no goals
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)
simp [this]