case inl
m n : ℤ
h : Int.gcd m n = 1
h1 : m % 2 = 0 ∧ n % 2 = 1
⊢ Int.gcd (m ^ 2 - n ^ 2) (2 * m * n) = 1

case inr
m n : ℤ
h : Int.gcd m n = 1
h2 : m % 2 = 1 ∧ n % 2 = 0
⊢ Int.gcd (m ^ 2 - n ^ 2) (2 * m * n) = 1
m n : ℤ
h : Int.gcd m n = 1
hmn : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
⊢ Int.gcd (m ^ 2 - n ^ 2) (2 * m * n) = 1
cases' hmn with h1 h2
no goals
case inl
m n : ℤ
h : Int.gcd m n = 1
h1 : m % 2 = 0 ∧ n % 2 = 1
⊢ Int.gcd (m ^ 2 - n ^ 2) (2 * m * n) = 1
exact coprime_sq_sub_mul_of_even_odd h h1.left h1.right
no goals
case inr
m n : ℤ
h : Int.gcd m n = 1
h2 : m % 2 = 1 ∧ n % 2 = 0
⊢ Int.gcd (m ^ 2 - n ^ 2) (2 * m * n) = 1
exact coprime_sq_sub_mul_of_odd_even h h2.left h2.right