Theorem: FltRegular.ab_coprime (FltRegular/CaseI/Statement.lean)

State before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
⊢ IsCoprime a b
Tactic:
rw [← gcd_eq_one_iff_coprime]
State after:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
⊢ a.gcd b = 1

State before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
⊢ a.gcd b = 1
Tactic:
by_contra! h
State after:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
⊢ False

State before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
⊢ False
Tactic:
obtain ⟨q, hqpri, hq⟩ := exists_prime_and_dvd h
State after:
case intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : q.Prime
hq : q ∣ a.gcd b
⊢ False

State before:
case intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : q.Prime
hq : q ∣ a.gcd b
⊢ False
Tactic:
replace hqpri : Prime (q : ℤ) := prime_iff_natAbs_prime.2 (by simp [hqpri])
State after:
case intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hq : q ∣ a.gcd b
hqpri : _root_.Prime ↑q
⊢ False

State before:
case intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hq : q ∣ a.gcd b
hqpri : _root_.Prime ↑q
⊢ False
Tactic:
obtain ⟨n, hn⟩ := hq
State after:
case intro.intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
⊢ False

State before:
case intro.intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
⊢ False
Tactic:
have haq : ↑q ∣ a := by
  obtain ⟨m, hm⟩ := @Int.gcd_dvd_left a b
  exact ⟨n * m, by rw [hm, hn]; simp [mul_assoc]⟩
State after:
case intro.intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
haq : ↑q ∣ a
⊢ False

State before:
case intro.intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
haq : ↑q ∣ a
⊢ False
Tactic:
have hbq : ↑q ∣ b := by
  obtain ⟨m, hm⟩ := @Int.gcd_dvd_right a b
  exact ⟨n * m, by rw [hm, hn]; simp [mul_assoc]⟩
State after:
case intro.intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
haq : ↑q ∣ a
hbq : ↑q ∣ b
⊢ False

State before:
case intro.intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
haq : ↑q ∣ a
hbq : ↑q ∣ b
⊢ False
Tactic:
have hcq : ↑q ∣ c := by
  suffices ↑q ∣ c ^ p by exact hqpri.dvd_of_dvd_pow this
  rw [← H]
  exact dvd_add (dvd_pow haq hpzero) (dvd_pow hbq hpzero)
State after:
case intro.intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
haq : ↑q ∣ a
hbq : ↑q ∣ b
hcq : ↑q ∣ c
⊢ False

State before:
case intro.intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
haq : ↑q ∣ a
hbq : ↑q ∣ b
hcq : ↑q ∣ c
⊢ False
Tactic:
have Hq : ↑q ∣ ({a, b, c} : Finset ℤ).gcd id := by
  refine' dvd_gcd fun x hx => _
  simp only [mem_insert, mem_singleton] at hx
  rcases hx with (H | H | H) <;> simpa [H]
State after:
case intro.intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
haq : ↑q ∣ a
hbq : ↑q ∣ b
hcq : ↑q ∣ c
Hq : ↑q ∣ {a, b, c}.gcd id
⊢ False

State before:
case intro.intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
haq : ↑q ∣ a
hbq : ↑q ∣ b
hcq : ↑q ∣ c
Hq : ↑q ∣ {a, b, c}.gcd id
⊢ False
Tactic:
rw [hgcd] at Hq
State after:
case intro.intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
haq : ↑q ∣ a
hbq : ↑q ∣ b
hcq : ↑q ∣ c
Hq : ↑q ∣ 1
⊢ False

State before:
case intro.intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
haq : ↑q ∣ a
hbq : ↑q ∣ b
hcq : ↑q ∣ c
Hq : ↑q ∣ 1
⊢ False
Tactic:
exact hqpri.not_unit (isUnit_of_dvd_one Hq)
State after:
no goals

State before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : q.Prime
hq : q ∣ a.gcd b
⊢ (↑q).natAbs.Prime
Tactic:
simp [hqpri]
State after:
no goals

State before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
⊢ ↑q ∣ a
Tactic:
obtain ⟨m, hm⟩ := @Int.gcd_dvd_left a b
State after:
case intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
m : ℤ
hm : a = ↑(a.gcd b) * m
⊢ ↑q ∣ a

State before:
case intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
m : ℤ
hm : a = ↑(a.gcd b) * m
⊢ ↑q ∣ a
Tactic:
exact ⟨n * m, by rw [hm, hn]; simp [mul_assoc]⟩
State after:
no goals

State before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
m : ℤ
hm : a = ↑(a.gcd b) * m
⊢ a = ↑q * (↑n * m)
Tactic:
rw [hm, hn]
State after:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
m : ℤ
hm : a = ↑(a.gcd b) * m
⊢ ↑(q * n) * m = ↑q * (↑n * m)

State before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
m : ℤ
hm : a = ↑(a.gcd b) * m
⊢ ↑(q * n) * m = ↑q * (↑n * m)
Tactic:
simp [mul_assoc]
State after:
no goals

State before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
haq : ↑q ∣ a
⊢ ↑q ∣ b
Tactic:
obtain ⟨m, hm⟩ := @Int.gcd_dvd_right a b
State after:
case intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
haq : ↑q ∣ a
m : ℤ
hm : b = ↑(a.gcd b) * m
⊢ ↑q ∣ b

State before:
case intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
haq : ↑q ∣ a
m : ℤ
hm : b = ↑(a.gcd b) * m
⊢ ↑q ∣ b
Tactic:
exact ⟨n * m, by rw [hm, hn]; simp [mul_assoc]⟩
State after:
no goals

State before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
haq : ↑q ∣ a
m : ℤ
hm : b = ↑(a.gcd b) * m
⊢ b = ↑q * (↑n * m)
Tactic:
rw [hm, hn]
State after:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
haq : ↑q ∣ a
m : ℤ
hm : b = ↑(a.gcd b) * m
⊢ ↑(q * n) * m = ↑q * (↑n * m)

State before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
haq : ↑q ∣ a
m : ℤ
hm : b = ↑(a.gcd b) * m
⊢ ↑(q * n) * m = ↑q * (↑n * m)
Tactic:
simp [mul_assoc]
State after:
no goals

State before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
haq : ↑q ∣ a
hbq : ↑q ∣ b
⊢ ↑q ∣ c
Tactic:
suffices ↑q ∣ c ^ p by exact hqpri.dvd_of_dvd_pow this
State after:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
haq : ↑q ∣ a
hbq : ↑q ∣ b
⊢ ↑q ∣ c ^ p

State before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
haq : ↑q ∣ a
hbq : ↑q ∣ b
⊢ ↑q ∣ c ^ p
Tactic:
rw [← H]
State after:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
haq : ↑q ∣ a
hbq : ↑q ∣ b
⊢ ↑q ∣ a ^ p + b ^ p

State before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
haq : ↑q ∣ a
hbq : ↑q ∣ b
⊢ ↑q ∣ a ^ p + b ^ p
Tactic:
exact dvd_add (dvd_pow haq hpzero) (dvd_pow hbq hpzero)
State after:
no goals

State before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
haq : ↑q ∣ a
hbq : ↑q ∣ b
this : ↑q ∣ c ^ p
⊢ ↑q ∣ c
Tactic:
exact hqpri.dvd_of_dvd_pow this
State after:
no goals

State before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
haq : ↑q ∣ a
hbq : ↑q ∣ b
hcq : ↑q ∣ c
⊢ ↑q ∣ {a, b, c}.gcd id
Tactic:
refine' dvd_gcd fun x hx => _
State after:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
haq : ↑q ∣ a
hbq : ↑q ∣ b
hcq : ↑q ∣ c
x : ℤ
hx : x ∈ {a, b, c}
⊢ ↑q ∣ id x

State before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
haq : ↑q ∣ a
hbq : ↑q ∣ b
hcq : ↑q ∣ c
x : ℤ
hx : x ∈ {a, b, c}
⊢ ↑q ∣ id x
Tactic:
simp only [mem_insert, mem_singleton] at hx
State after:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
haq : ↑q ∣ a
hbq : ↑q ∣ b
hcq : ↑q ∣ c
x : ℤ
hx : x = a ∨ x = b ∨ x = c
⊢ ↑q ∣ id x

State before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
haq : ↑q ∣ a
hbq : ↑q ∣ b
hcq : ↑q ∣ c
x : ℤ
hx : x = a ∨ x = b ∨ x = c
⊢ ↑q ∣ id x
Tactic:
rcases hx with (H | H | H) <;> simpa [H]
State after:
no goals