Theorem: gcd3_coprime (Flt/Euler.lean)

State before:
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
⊢ IsCoprime (2 * v) (u + v) ∧ IsCoprime (2 * v) (u - v) ∧ IsCoprime (u - v) (u + v)
Tactic:
have haddodd : ¬Even (u + v) := by simp [huvodd, parity_simps]
State after:
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
⊢ IsCoprime (2 * v) (u + v) ∧ IsCoprime (2 * v) (u - v) ∧ IsCoprime (u - v) (u + v)

State before:
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
⊢ IsCoprime (2 * v) (u + v) ∧ IsCoprime (2 * v) (u - v) ∧ IsCoprime (u - v) (u + v)
Tactic:
have hsubodd : ¬Even (u - v) := by simp [huvodd, parity_simps]
State after:
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
⊢ IsCoprime (2 * v) (u + v) ∧ IsCoprime (2 * v) (u - v) ∧ IsCoprime (u - v) (u + v)

State before:
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
hsubcoprime : IsCoprime (u - v) (2 * v)
haddsubcoprime : IsCoprime (u + v) (u - v)
⊢ IsCoprime (2 * v) (u + v) ∧ IsCoprime (2 * v) (u - v) ∧ IsCoprime (u - v) (u + v)
Tactic:
exact ⟨haddcoprime.symm, hsubcoprime.symm, haddsubcoprime.symm⟩
State after:
no goals

State before:
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
⊢ ¬Even (u + v)
Tactic:
simp [huvodd, parity_simps]
State after:
no goals

State before:
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
⊢ ¬Even (u - v)
Tactic:
simp [huvodd, parity_simps]
State after:
no goals

State before:
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
⊢ IsCoprime (u + v) (2 * v)
Tactic:
apply isCoprime_of_prime_dvd
State after:
case nonzero
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
⊢ ¬(u + v = 0 ∧ 2 * v = 0)

case H
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
⊢ ∀ (z : ℤ), Prime z → z ∣ u + v → ¬z ∣ 2 * v

State before:
case H
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
⊢ ∀ (z : ℤ), Prime z → z ∣ u + v → ¬z ∣ 2 * v
Tactic:
intro k hkprime hkdvdleft hkdvdright
State after:
case H
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u + v
hkdvdright : k ∣ 2 * v
⊢ False

State before:
case H
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u + v
hkdvdright : k ∣ 2 * v
⊢ False
Tactic:
apply hkprime.not_unit
State after:
case H
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u + v
hkdvdright : k ∣ 2 * v
⊢ IsUnit k

State before:
case H
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u + v
hkdvdright : k ∣ 2 * v
⊢ IsUnit k
Tactic:
have hkdvdright' : k ∣ v := by
  rw [even_iff_two_dvd] at haddodd
  exact Int.dvd_mul_cancel_prime' haddodd hkdvdleft Int.prime_two hkdvdright
State after:
case H
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u + v
hkdvdright : k ∣ 2 * v
hkdvdright' : k ∣ v
⊢ IsUnit k

State before:
case H
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u + v
hkdvdright : k ∣ 2 * v
hkdvdright' : k ∣ v
⊢ IsUnit k
Tactic:
apply huvcoprime.isUnit_of_dvd' _ hkdvdright'
State after:
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u + v
hkdvdright : k ∣ 2 * v
hkdvdright' : k ∣ v
⊢ k ∣ u

State before:
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u + v
hkdvdright : k ∣ 2 * v
hkdvdright' : k ∣ v
⊢ k ∣ u
Tactic:
rw [← add_sub_cancel u v]
State after:
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u + v
hkdvdright : k ∣ 2 * v
hkdvdright' : k ∣ v
⊢ k ∣ u + v - v

State before:
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u + v
hkdvdright : k ∣ 2 * v
hkdvdright' : k ∣ v
⊢ k ∣ u + v - v
Tactic:
apply dvd_sub hkdvdleft hkdvdright'
State after:
no goals

State before:
case nonzero
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
⊢ ¬(u + v = 0 ∧ 2 * v = 0)
Tactic:
rintro ⟨h1, -⟩
State after:
case nonzero.intro
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
h1 : u + v = 0
⊢ False

State before:
case nonzero.intro
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
h1 : u + v = 0
⊢ False
Tactic:
rw [h1] at haddodd
State after:
case nonzero.intro
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even 0
hsubodd : ¬Even (u - v)
h1 : u + v = 0
⊢ False

State before:
case nonzero.intro
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even 0
hsubodd : ¬Even (u - v)
h1 : u + v = 0
⊢ False
Tactic:
norm_num at haddodd
State after:
no goals

State before:
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u + v
hkdvdright : k ∣ 2 * v
⊢ k ∣ v
Tactic:
rw [even_iff_two_dvd] at haddodd
State after:
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬2 ∣ u + v
hsubodd : ¬Even (u - v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u + v
hkdvdright : k ∣ 2 * v
⊢ k ∣ v

State before:
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬2 ∣ u + v
hsubodd : ¬Even (u - v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u + v
hkdvdright : k ∣ 2 * v
⊢ k ∣ v
Tactic:
exact Int.dvd_mul_cancel_prime' haddodd hkdvdleft Int.prime_two hkdvdright
State after:
no goals

State before:
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
⊢ IsCoprime (u - v) (2 * v)
Tactic:
apply isCoprime_of_prime_dvd
State after:
case nonzero
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
⊢ ¬(u - v = 0 ∧ 2 * v = 0)

case H
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
⊢ ∀ (z : ℤ), Prime z → z ∣ u - v → ¬z ∣ 2 * v

State before:
case H
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
⊢ ∀ (z : ℤ), Prime z → z ∣ u - v → ¬z ∣ 2 * v
Tactic:
intro k hkprime hkdvdleft hkdvdright
State after:
case H
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - v
hkdvdright : k ∣ 2 * v
⊢ False

State before:
case H
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - v
hkdvdright : k ∣ 2 * v
⊢ False
Tactic:
apply hkprime.not_unit
State after:
case H
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - v
hkdvdright : k ∣ 2 * v
⊢ IsUnit k

State before:
case H
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - v
hkdvdright : k ∣ 2 * v
⊢ IsUnit k
Tactic:
have hkdvdright' : k ∣ v := by
  rw [even_iff_two_dvd] at hsubodd
  exact Int.dvd_mul_cancel_prime' hsubodd hkdvdleft Int.prime_two hkdvdright
State after:
case H
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - v
hkdvdright : k ∣ 2 * v
hkdvdright' : k ∣ v
⊢ IsUnit k

State before:
case H
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - v
hkdvdright : k ∣ 2 * v
hkdvdright' : k ∣ v
⊢ IsUnit k
Tactic:
apply huvcoprime.isUnit_of_dvd' _ hkdvdright'
State after:
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - v
hkdvdright : k ∣ 2 * v
hkdvdright' : k ∣ v
⊢ k ∣ u

State before:
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - v
hkdvdright : k ∣ 2 * v
hkdvdright' : k ∣ v
⊢ k ∣ u
Tactic:
rw [← sub_add_cancel u v]
State after:
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - v
hkdvdright : k ∣ 2 * v
hkdvdright' : k ∣ v
⊢ k ∣ u - v + v

State before:
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - v
hkdvdright : k ∣ 2 * v
hkdvdright' : k ∣ v
⊢ k ∣ u - v + v
Tactic:
exact dvd_add hkdvdleft hkdvdright'
State after:
no goals

State before:
case nonzero
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
⊢ ¬(u - v = 0 ∧ 2 * v = 0)
Tactic:
rintro ⟨h1, -⟩
State after:
case nonzero.intro
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
h1 : u - v = 0
⊢ False

State before:
case nonzero.intro
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
h1 : u - v = 0
⊢ False
Tactic:
rw [h1] at hsubodd
State after:
case nonzero.intro
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even 0
haddcoprime : IsCoprime (u + v) (2 * v)
h1 : u - v = 0
⊢ False

State before:
case nonzero.intro
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even 0
haddcoprime : IsCoprime (u + v) (2 * v)
h1 : u - v = 0
⊢ False
Tactic:
norm_num at hsubodd
State after:
no goals

State before:
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - v
hkdvdright : k ∣ 2 * v
⊢ k ∣ v
Tactic:
rw [even_iff_two_dvd] at hsubodd
State after:
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬2 ∣ u - v
haddcoprime : IsCoprime (u + v) (2 * v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - v
hkdvdright : k ∣ 2 * v
⊢ k ∣ v

State before:
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬2 ∣ u - v
haddcoprime : IsCoprime (u + v) (2 * v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - v
hkdvdright : k ∣ 2 * v
⊢ k ∣ v
Tactic:
exact Int.dvd_mul_cancel_prime' hsubodd hkdvdleft Int.prime_two hkdvdright
State after:
no goals

State before:
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
hsubcoprime : IsCoprime (u - v) (2 * v)
⊢ IsCoprime (u + v) (u - v)
Tactic:
apply isCoprime_of_prime_dvd
State after:
case nonzero
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
hsubcoprime : IsCoprime (u - v) (2 * v)
⊢ ¬(u + v = 0 ∧ u - v = 0)

case H
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
hsubcoprime : IsCoprime (u - v) (2 * v)
⊢ ∀ (z : ℤ), Prime z → z ∣ u + v → ¬z ∣ u - v

State before:
case H
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
hsubcoprime : IsCoprime (u - v) (2 * v)
⊢ ∀ (z : ℤ), Prime z → z ∣ u + v → ¬z ∣ u - v
Tactic:
intro k hkprime hkdvdleft hkdvdright
State after:
case H
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
hsubcoprime : IsCoprime (u - v) (2 * v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u + v
hkdvdright : k ∣ u - v
⊢ False

State before:
case H
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
hsubcoprime : IsCoprime (u - v) (2 * v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u + v
hkdvdright : k ∣ u - v
⊢ False
Tactic:
apply hkprime.not_unit
State after:
case H
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
hsubcoprime : IsCoprime (u - v) (2 * v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u + v
hkdvdright : k ∣ u - v
⊢ IsUnit k

State before:
case H
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
hsubcoprime : IsCoprime (u - v) (2 * v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u + v
hkdvdright : k ∣ u - v
⊢ IsUnit k
Tactic:
rw [even_iff_two_dvd] at haddodd
State after:
case H
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬2 ∣ u + v
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
hsubcoprime : IsCoprime (u - v) (2 * v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u + v
hkdvdright : k ∣ u - v
⊢ IsUnit k

State before:
case H
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬2 ∣ u + v
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
hsubcoprime : IsCoprime (u - v) (2 * v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u + v
hkdvdright : k ∣ u - v
⊢ IsUnit k
Tactic:
apply huvcoprime.isUnit_of_dvd' <;>
  apply Int.dvd_mul_cancel_prime' haddodd hkdvdleft Int.prime_two
State after:
case H.ha
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬2 ∣ u + v
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
hsubcoprime : IsCoprime (u - v) (2 * v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u + v
hkdvdright : k ∣ u - v
⊢ k ∣ 2 * u

case H.hb
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬2 ∣ u + v
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
hsubcoprime : IsCoprime (u - v) (2 * v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u + v
hkdvdright : k ∣ u - v
⊢ k ∣ 2 * v

State before:
case nonzero
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
hsubcoprime : IsCoprime (u - v) (2 * v)
⊢ ¬(u + v = 0 ∧ u - v = 0)
Tactic:
rintro ⟨h1, -⟩
State after:
case nonzero.intro
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
hsubcoprime : IsCoprime (u - v) (2 * v)
h1 : u + v = 0
⊢ False

State before:
case nonzero.intro
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
hsubcoprime : IsCoprime (u - v) (2 * v)
h1 : u + v = 0
⊢ False
Tactic:
rw [h1] at haddodd
State after:
case nonzero.intro
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even 0
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
hsubcoprime : IsCoprime (u - v) (2 * v)
h1 : u + v = 0
⊢ False

State before:
case nonzero.intro
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even 0
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
hsubcoprime : IsCoprime (u - v) (2 * v)
h1 : u + v = 0
⊢ False
Tactic:
norm_num at haddodd
State after:
no goals

State before:
case H.ha
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬2 ∣ u + v
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
hsubcoprime : IsCoprime (u - v) (2 * v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u + v
hkdvdright : k ∣ u - v
⊢ k ∣ 2 * u
Tactic:
convert dvd_add hkdvdleft hkdvdright using 1
State after:
case h.e'_4
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬2 ∣ u + v
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
hsubcoprime : IsCoprime (u - v) (2 * v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u + v
hkdvdright : k ∣ u - v
⊢ 2 * u = u + v + (u - v)

State before:
case h.e'_4
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬2 ∣ u + v
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
hsubcoprime : IsCoprime (u - v) (2 * v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u + v
hkdvdright : k ∣ u - v
⊢ 2 * u = u + v + (u - v)
Tactic:
ring
State after:
no goals

State before:
case H.hb
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬2 ∣ u + v
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
hsubcoprime : IsCoprime (u - v) (2 * v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u + v
hkdvdright : k ∣ u - v
⊢ k ∣ 2 * v
Tactic:
convert dvd_sub hkdvdleft hkdvdright using 1
State after:
case h.e'_4
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬2 ∣ u + v
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
hsubcoprime : IsCoprime (u - v) (2 * v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u + v
hkdvdright : k ∣ u - v
⊢ 2 * v = u + v - (u - v)

State before:
case h.e'_4
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬2 ∣ u + v
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
hsubcoprime : IsCoprime (u - v) (2 * v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u + v
hkdvdright : k ∣ u - v
⊢ 2 * v = u + v - (u - v)
Tactic:
ring
State after:
no goals