-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem divides_sq_eq_zero {x y} (h : x * x = d * y * y) : x = 0 ∧ y = 0 :=
  let g := x.gcd y
  Or.elim g.eq_zero_or_pos
    (fun H => ⟨Nat.eq_zero_of_gcd_eq_zero_left H, Nat.eq_zero_of_gcd_eq_zero_right H⟩) fun gpos =>
    False.elim <| by
      let ⟨m, n, co, (hx : x = m * g), (hy : y = n * g)⟩ := Nat.exists_coprime _ _
      rw [hx, hy] at h
      have : m * m = d * (n * n)

Proof state:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
g : ℕ := x.gcd y
gpos : g > 0
m n : ℕ
h : m * g * (m * g) = d * (n * g) * (n * g)
co : m.Coprime n
hx : x = m * g
hy : y = n * g
this : m * m = d * (n * n)
co2 : (m * m).Coprime (n * n)
⊢ d ∣ d * (n * n)

Tactic:
apply dvd_mul_right

Result:
no goals

Proof state:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
g : ℕ := x.gcd y
gpos : g > 0
m n : ℕ
h : m * g * (m * g) = d * (n * g) * (n * g)
co : m.Coprime n
hx : x = m * g
hy : y = n * g
this : m * m = d * (n * n)
co2 : (m * m).Coprime (n * n)
⊢ False

Tactic:
exact
  Nonsquare.ns d m
    (Nat.dvd_antisymm (by rw [this]; apply dvd_mul_right) <|
      co2.dvd_of_dvd_mul_right <| by simp [this])

Result:
no goals

Proof state:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
h : x * x = d * y * y
g : ℕ := x.gcd y
gpos : g > 0
m n : ℕ
co : m.Coprime n
hx : x = m * g
hy : y = n * g
⊢ False

Tactic:
rw [hx, hy] at h

Result:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
g : ℕ := x.gcd y
gpos : g > 0
m n : ℕ
h : m * g * (m * g) = d * (n * g) * (n * g)
co : m.Coprime n
hx : x = m * g
hy : y = n * g
⊢ False

Proof state:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
g : ℕ := x.gcd y
gpos : g > 0
m n : ℕ
h : m * g * (m * g) = d * (n * g) * (n * g)
co : m.Coprime n
hx : x = m * g
hy : y = n * g
⊢ m * m = d * (n * n)

Tactic:
refine mul_left_cancel₀ (mul_pos gpos gpos).ne' ?_

Result:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
g : ℕ := x.gcd y
gpos : g > 0
m n : ℕ
h : m * g * (m * g) = d * (n * g) * (n * g)
co : m.Coprime n
hx : x = m * g
hy : y = n * g
⊢ g * g * (m * m) = g * g * (d * (n * n))

Proof state:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
g : ℕ := x.gcd y
gpos : g > 0
m n : ℕ
h : m * g * (m * g) = d * (n * g) * (n * g)
co : m.Coprime n
hx : x = m * g
hy : y = n * g
⊢ d * (n * g) * (n * g) = g * g * (d * (n * n))

Tactic:
ring

Result:
no goals

Proof state:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
g : ℕ := x.gcd y
gpos : g > 0
m n : ℕ
h : m * g * (m * g) = d * (n * g) * (n * g)
co : m.Coprime n
hx : x = m * g
hy : y = n * g
⊢ g * g * (m * m) = g * g * (d * (n * n))

Tactic:
calc
  g * g * (m * m)
  _ = m * g * (m * g) := by ring
  _ = d * (n * g) * (n * g) := h
  _ = g * g * (d * (n * n)) := by ring

Result:
no goals

Proof state:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
g : ℕ := x.gcd y
gpos : g > 0
m n : ℕ
h : m * g * (m * g) = d * (n * g) * (n * g)
co : m.Coprime n
hx : x = m * g
hy : y = n * g
this : m * m = d * (n * n)
co2 : (m * m).Coprime (n * n)
⊢ m * m ∣ d * (n * n)

Tactic:
simp [this]

Result:
no goals

Proof state:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
h : x * x = d * y * y
g : ℕ := x.gcd y
gpos : g > 0
⊢ False

Tactic:
let ⟨m, n, co, (hx : x = m * g), (hy : y = n * g)⟩ := Nat.exists_coprime _ _

Result:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
h : x * x = d * y * y
g : ℕ := x.gcd y
gpos : g > 0
m n : ℕ
co : m.Coprime n
hx : x = m * g
hy : y = n * g
⊢ False

Proof state:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
g : ℕ := x.gcd y
gpos : g > 0
m n : ℕ
h : m * g * (m * g) = d * (n * g) * (n * g)
co : m.Coprime n
hx : x = m * g
hy : y = n * g
this : m * m = d * (n * n)
co2 : (m * m).Coprime (n * n)
⊢ d ∣ m * m

Tactic:
rw [this]

Result:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
g : ℕ := x.gcd y
gpos : g > 0
m n : ℕ
h : m * g * (m * g) = d * (n * g) * (n * g)
co : m.Coprime n
hx : x = m * g
hy : y = n * g
this : m * m = d * (n * n)
co2 : (m * m).Coprime (n * n)
⊢ d ∣ d * (n * n)

Proof state:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
g : ℕ := x.gcd y
gpos : g > 0
m n : ℕ
h : m * g * (m * g) = d * (n * g) * (n * g)
co : m.Coprime n
hx : x = m * g
hy : y = n * g
⊢ g * g * (m * m) = m * g * (m * g)

Tactic:
ring

Result:
no goals

Proof state:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
g : ℕ := x.gcd y
gpos : g > 0
m n : ℕ
h : m * g * (m * g) = d * (n * g) * (n * g)
co : m.Coprime n
hx : x = m * g
hy : y = n * g
⊢ False

Tactic:
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

Result:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
g : ℕ := x.gcd y
gpos : g > 0
m n : ℕ
h : m * g * (m * g) = d * (n * g) * (n * g)
co : m.Coprime n
hx : x = m * g
hy : y = n * g
this : m * m = d * (n * n)
⊢ False

Proof state:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
g : ℕ := x.gcd y
gpos : g > 0
m n : ℕ
h : m * g * (m * g) = d * (n * g) * (n * g)
co : m.Coprime n
hx : x = m * g
hy : y = n * g
this : m * m = d * (n * n)
⊢ False

Tactic:
have co2 :=
  let co1 := co.mul_right co
  co1.mul co1

Result:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
g : ℕ := x.gcd y
gpos : g > 0
m n : ℕ
h : m * g * (m * g) = d * (n * g) * (n * g)
co : m.Coprime n
hx : x = m * g
hy : y = n * g
this : m * m = d * (n * n)
co2 : (m * m).Coprime (n * n)
⊢ False