Theorem: Int.gcd1_coprime23 (Flt/Euler.lean)

State before:
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
⊢ IsCoprime (u - 3 * v) (u + 3 * v)
Tactic:
apply isCoprime_of_prime_dvd
State after:
case nonzero
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
⊢ ¬(u - 3 * v = 0 ∧ u + 3 * v = 0)

case H
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
⊢ ∀ (z : ℤ), Prime z → z ∣ u - 3 * v → ¬z ∣ u + 3 * v

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

State before:
case H
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - 3 * v
hkdvdright : k ∣ u + 3 * v
⊢ False
Tactic:
apply hkprime.not_unit
State after:
case H
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - 3 * v
hkdvdright : k ∣ u + 3 * v
⊢ IsUnit k

State before:
case H
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - 3 * v
hkdvdright : k ∣ u + 3 * v
⊢ IsUnit k
Tactic:
apply huvcoprime.isUnit_of_dvd'
State after:
case H.ha
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - 3 * v
hkdvdright : k ∣ u + 3 * v
⊢ k ∣ u

case H.hb
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - 3 * v
hkdvdright : k ∣ u + 3 * v
⊢ k ∣ v

State before:
case nonzero
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
⊢ ¬(u - 3 * v = 0 ∧ u + 3 * v = 0)
Tactic:
rintro ⟨h1, -⟩
State after:
case nonzero.intro
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
h1 : u - 3 * v = 0
⊢ False

State before:
case nonzero.intro
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
h1 : u - 3 * v = 0
⊢ False
Tactic:
rw [h1] at notdvd_2_2
State after:
case nonzero.intro
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ 0
notdvd_3_3 : ¬3 ∣ u + 3 * v
h1 : u - 3 * v = 0
⊢ False

State before:
case nonzero.intro
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ 0
notdvd_3_3 : ¬3 ∣ u + 3 * v
h1 : u - 3 * v = 0
⊢ False
Tactic:
norm_num at notdvd_2_2
State after:
no goals

State before:
case H.ha
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - 3 * v
hkdvdright : k ∣ u + 3 * v
⊢ k ∣ u
Tactic:
apply Int.dvd_mul_cancel_prime' notdvd_2_2 hkdvdleft Int.prime_two
State after:
case H.ha
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - 3 * v
hkdvdright : k ∣ u + 3 * v
⊢ k ∣ 2 * u

State before:
case H.ha
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - 3 * v
hkdvdright : k ∣ u + 3 * v
⊢ k ∣ 2 * u
Tactic:
convert dvd_add hkdvdleft hkdvdright using 1
State after:
case h.e'_4
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - 3 * v
hkdvdright : k ∣ u + 3 * v
⊢ 2 * u = u - 3 * v + (u + 3 * v)

State before:
case h.e'_4
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - 3 * v
hkdvdright : k ∣ u + 3 * v
⊢ 2 * u = u - 3 * v + (u + 3 * v)
Tactic:
ring
State after:
no goals

State before:
case H.hb
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - 3 * v
hkdvdright : k ∣ u + 3 * v
⊢ k ∣ v
Tactic:
apply Int.dvd_mul_cancel_prime' notdvd_3_3 hkdvdright Int.prime_three
State after:
case H.hb
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - 3 * v
hkdvdright : k ∣ u + 3 * v
⊢ k ∣ 3 * v

State before:
case H.hb
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - 3 * v
hkdvdright : k ∣ u + 3 * v
⊢ k ∣ 3 * v
Tactic:
apply Int.dvd_mul_cancel_prime' notdvd_2_2 hkdvdleft Int.prime_two
State after:
case H.hb
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - 3 * v
hkdvdright : k ∣ u + 3 * v
⊢ k ∣ 2 * (3 * v)

State before:
case H.hb
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - 3 * v
hkdvdright : k ∣ u + 3 * v
⊢ k ∣ 2 * (3 * v)
Tactic:
convert dvd_sub hkdvdright hkdvdleft using 1
State after:
case h.e'_4
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - 3 * v
hkdvdright : k ∣ u + 3 * v
⊢ 2 * (3 * v) = u + 3 * v - (u - 3 * v)

State before:
case h.e'_4
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - 3 * v
hkdvdright : k ∣ u + 3 * v
⊢ 2 * (3 * v) = u + 3 * v - (u - 3 * v)
Tactic:
ring
State after:
no goals