a b c : ℤ
h : gcd a b = 1
heq : a * b = c ^ 2
h' : IsUnit (GCDMonoid.gcd a b)
⊢ ∃ a0, a = a0 ^ 2 ∨ a = -a0 ^ 2
a b c : ℤ
h : gcd a b = 1
heq : a * b = c ^ 2
⊢ ∃ a0, a = a0 ^ 2 ∨ a = -a0 ^ 2
have h' : IsUnit (GCDMonoid.gcd a b) := by
  rw [← coe_gcd, h, Int.ofNat_one]
  exact isUnit_one
case intro.intro
a b c : ℤ
h : gcd a b = 1
heq : a * b = c ^ 2
h' : IsUnit (GCDMonoid.gcd a b)
d : ℤ
u : ℤˣ
hu : d ^ 2 * ↑u = a
⊢ ∃ a0, a = a0 ^ 2 ∨ a = -a0 ^ 2
a b c : ℤ
h : gcd a b = 1
heq : a * b = c ^ 2
h' : IsUnit (GCDMonoid.gcd a b)
⊢ ∃ a0, a = a0 ^ 2 ∨ a = -a0 ^ 2
obtain ⟨d, ⟨u, hu⟩⟩ := exists_associated_pow_of_mul_eq_pow h' heq
case intro.intro
a b c : ℤ
h : gcd a b = 1
heq : a * b = c ^ 2
h' : IsUnit (GCDMonoid.gcd a b)
d : ℤ
u : ℤˣ
hu : d ^ 2 * ↑u = a
⊢ a = d ^ 2 ∨ a = -d ^ 2
case intro.intro
a b c : ℤ
h : gcd a b = 1
heq : a * b = c ^ 2
h' : IsUnit (GCDMonoid.gcd a b)
d : ℤ
u : ℤˣ
hu : d ^ 2 * ↑u = a
⊢ ∃ a0, a = a0 ^ 2 ∨ a = -a0 ^ 2
use d
case intro.intro
a b c : ℤ
h : gcd a b = 1
heq : a * b = c ^ 2
h' : IsUnit (GCDMonoid.gcd a b)
d : ℤ
u : ℤˣ
hu : d ^ 2 * ↑u = a
⊢ d ^ 2 * ↑u = d ^ 2 ∨ d ^ 2 * ↑u = -d ^ 2
case intro.intro
a b c : ℤ
h : gcd a b = 1
heq : a * b = c ^ 2
h' : IsUnit (GCDMonoid.gcd a b)
d : ℤ
u : ℤˣ
hu : d ^ 2 * ↑u = a
⊢ a = d ^ 2 ∨ a = -d ^ 2
rw [← hu]
a b c : ℤ
h : gcd a b = 1
heq : a * b = c ^ 2
⊢ IsUnit 1
a b c : ℤ
h : gcd a b = 1
heq : a * b = c ^ 2
⊢ IsUnit (GCDMonoid.gcd a b)
rw [← coe_gcd, h, Int.ofNat_one]
no goals
a b c : ℤ
h : gcd a b = 1
heq : a * b = c ^ 2
⊢ IsUnit 1
exact isUnit_one
case intro.intro.inr
a b c : ℤ
h : gcd a b = 1
heq : a * b = c ^ 2
h' : IsUnit (GCDMonoid.gcd a b)
d : ℤ
u : ℤˣ
hu : d ^ 2 * ↑u = a
hu' : u = -1
⊢ d ^ 2 * ↑(-1) = d ^ 2 ∨ d ^ 2 * ↑(-1) = -d ^ 2
case intro.intro.inr
a b c : ℤ
h : gcd a b = 1
heq : a * b = c ^ 2
h' : IsUnit (GCDMonoid.gcd a b)
d : ℤ
u : ℤˣ
hu : d ^ 2 * ↑u = a
hu' : u = -1
⊢ d ^ 2 * ↑u = d ^ 2 ∨ d ^ 2 * ↑u = -d ^ 2
rw [hu']
no goals
case intro.intro.inr
a b c : ℤ
h : gcd a b = 1
heq : a * b = c ^ 2
h' : IsUnit (GCDMonoid.gcd a b)
d : ℤ
u : ℤˣ
hu : d ^ 2 * ↑u = a
hu' : u = -1
⊢ d ^ 2 * ↑(-1) = d ^ 2 ∨ d ^ 2 * ↑(-1) = -d ^ 2
simp