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
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
obtain ⟨re, im, H1, Hre, Him⟩ := Int.exists_gcd_one hgcd
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
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
rw [mul_comm] at Hre Him
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 }

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
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
refine' ⟨⟨re, im⟩, _, _⟩
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
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 }
rw [smul_val, ext, ← Hre, ← Him]
no goals
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
constructor <;> rfl
no goals
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
rw [← Int.gcd_eq_one_iff_coprime, H1]