internlm/Lean-Github huggingface dataset:
Theorem: FltRegular.p_dvd_c_of_ab_of_anegc
Proof state before:
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
hab : a ≡ b [ZMOD ↑p]
hbc : b ≡ -c [ZMOD ↑p]
this : Fact p.Prime := { out := hpri }
h : (fun n => ↑n) (a ^ p + b ^ p) = (fun n => ↑n) (c ^ p)
⊢ ↑p ∣ c
Tactic:
simp only [Int.natCast_pow, Int.cast_add, Int.cast_pow, ZMod.pow_card] at h
Proof state after:
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
hab : a ≡ b [ZMOD ↑p]
hbc : b ≡ -c [ZMOD ↑p]
this : Fact p.Prime := { out := hpri }
h : ↑a + ↑b = ↑c
⊢ ↑p ∣ c
Theorem: FltRegular.p_dvd_c_of_ab_of_anegc
Proof state before:
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
hab : a ≡ b [ZMOD ↑p]
hbc : b ≡ -c [ZMOD ↑p]
this : Fact p.Prime := { out := hpri }
h : ↑a + ↑b = ↑c
⊢ ↑p ∣ c
Tactic:
simp only [← ZMod.intCast_eq_intCast_iff, Int.cast_neg] at hbc hab
Proof state after:
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
this : Fact p.Prime := { out := hpri }
h : ↑a + ↑b = ↑c
hbc : ↑b = -↑c
hab : ↑a = ↑b
⊢ ↑p ∣ c
Theorem: FltRegular.p_dvd_c_of_ab_of_anegc
Proof state before:
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
this : Fact p.Prime := { out := hpri }
h : ↑a + ↑b = ↑c
hbc : ↑b = -↑c
hab : ↑a = ↑b
⊢ ↑p ∣ c
Tactic:
rw [hab, hbc, ← sub_eq_zero, ← sub_eq_add_neg, ← Int.cast_neg, ← Int.cast_sub,
  ← Int.cast_sub] at h
Proof state after:
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
this : Fact p.Prime := { out := hpri }
h : ↑(-c - c - c) = 0
hbc : ↑b = -↑c
hab : ↑a = ↑b
⊢ ↑p ∣ c
Theorem: FltRegular.p_dvd_c_of_ab_of_anegc
Proof state before:
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
this : Fact p.Prime := { out := hpri }
h : ↑(-c - c - c) = 0
hbc : ↑b = -↑c
hab : ↑a = ↑b
⊢ ↑p ∣ c
Tactic:
ring_nf at h
Proof state after:
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
this : Fact p.Prime := { out := hpri }
hbc : ↑b = -↑c
hab : ↑a = ↑b
h : ↑(-(c * 3)) = 0
⊢ ↑p ∣ c
Theorem: FltRegular.p_dvd_c_of_ab_of_anegc
Proof state before:
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
this : Fact p.Prime := { out := hpri }
hbc : ↑b = -↑c
hab : ↑a = ↑b
h : ↑(-(c * 3)) = 0
⊢ ↑p ∣ c
Tactic:
simp only [Int.cast_neg, Int.cast_mul, Int.cast_one, Int.cast_ofNat, neg_eq_zero,
  mul_eq_zero] at h
Proof state after:
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
this : Fact p.Prime := { out := hpri }
hbc : ↑b = -↑c
hab : ↑a = ↑b
h : ↑c = 0 ∨ 3 = 0
⊢ ↑p ∣ c
Theorem: FltRegular.p_dvd_c_of_ab_of_anegc
Proof state before:
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
this : Fact p.Prime := { out := hpri }
hbc : ↑b = -↑c
hab : ↑a = ↑b
h : ↑c = 0 ∨ 3 = 0
⊢ ↑p ∣ c
Tactic:
rw [← ZMod.intCast_zmod_eq_zero_iff_dvd]
Proof state after:
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
this : Fact p.Prime := { out := hpri }
hbc : ↑b = -↑c
hab : ↑a = ↑b
h : ↑c = 0 ∨ 3 = 0
⊢ ↑c = 0
Theorem: FltRegular.p_dvd_c_of_ab_of_anegc
Proof state before:
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
this : Fact p.Prime := { out := hpri }
hbc : ↑b = -↑c
hab : ↑a = ↑b
h : ↑c = 0 ∨ 3 = 0
⊢ ↑c = 0
Tactic:
refine' Or.resolve_right h fun h3 => _
Proof state after:
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
this : Fact p.Prime := { out := hpri }
hbc : ↑b = -↑c
hab : ↑a = ↑b
h : ↑c = 0 ∨ 3 = 0
h3 : 3 = 0
⊢ False
Theorem: FltRegular.p_dvd_c_of_ab_of_anegc
Proof state before:
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
this : Fact p.Prime := { out := hpri }
hbc : ↑b = -↑c
hab : ↑a = ↑b
h : ↑c = 0 ∨ 3 = 0
h3 : 3 = 0
⊢ False
Tactic:
rw [show (3 : ZMod p) = ((3 : ℕ) : ZMod p) by simp, ZMod.natCast_zmod_eq_zero_iff_dvd,
  Nat.dvd_prime Nat.prime_three] at h3
Proof state after:
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
this : Fact p.Prime := { out := hpri }
hbc : ↑b = -↑c
hab : ↑a = ↑b
h : ↑c = 0 ∨ 3 = 0
h3 : p = 1 ∨ p = 3
⊢ False
Theorem: FltRegular.p_dvd_c_of_ab_of_anegc
Proof state before:
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
this : Fact p.Prime := { out := hpri }
hbc : ↑b = -↑c
hab : ↑a = ↑b
h : ↑c = 0 ∨ 3 = 0
h3 : p = 1 ∨ p = 3
⊢ False
Tactic:
cases' h3 with H₁ H₂
Proof state after:
case inl
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
this : Fact p.Prime := { out := hpri }
hbc : ↑b = -↑c
hab : ↑a = ↑b
h : ↑c = 0 ∨ 3 = 0
H₁ : p = 1
⊢ False

case inr
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
this : Fact p.Prime := { out := hpri }
hbc : ↑b = -↑c
hab : ↑a = ↑b
h : ↑c = 0 ∨ 3 = 0
H₂ : p = 3
⊢ False
Theorem: FltRegular.p_dvd_c_of_ab_of_anegc
Proof state before:
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
this : Fact p.Prime := { out := hpri }
hbc : ↑b = -↑c
hab : ↑a = ↑b
h : ↑c = 0 ∨ 3 = 0
h3 : 3 = 0
⊢ 3 = ↑3
Tactic:
simp
Proof state after:
no goals
Theorem: FltRegular.p_dvd_c_of_ab_of_anegc
Proof state before:
case inl
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
this : Fact p.Prime := { out := hpri }
hbc : ↑b = -↑c
hab : ↑a = ↑b
h : ↑c = 0 ∨ 3 = 0
H₁ : p = 1
⊢ False
Tactic:
exact hpri.ne_one H₁
Proof state after:
no goals
Theorem: FltRegular.p_dvd_c_of_ab_of_anegc
Proof state before:
case inr
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
this : Fact p.Prime := { out := hpri }
hbc : ↑b = -↑c
hab : ↑a = ↑b
h : ↑c = 0 ∨ 3 = 0
H₂ : p = 3
⊢ False
Tactic:
exact hp H₂
Proof state after:
no goals
Theorem: FltRegular.a_not_cong_b
Proof state before:
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
⊢ ∃ x y z, x ^ p + y ^ p = z ^ p ∧ {x, y, z}.gcd id = 1 ∧ ¬x ≡ y [ZMOD ↑p] ∧ x * y * z ≠ 0 ∧ ¬↑p ∣ x * y * z
Tactic:
by_cases H : a ≡ b [ZMOD p]
Proof state after:
case pos
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
⊢ ∃ x y z, x ^ p + y ^ p = z ^ p ∧ {x, y, z}.gcd id = 1 ∧ ¬x ≡ y [ZMOD ↑p] ∧ x * y * z ≠ 0 ∧ ¬↑p ∣ x * y * z

case neg
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : ¬a ≡ b [ZMOD ↑p]
⊢ ∃ x y z, x ^ p + y ^ p = z ^ p ∧ {x, y, z}.gcd id = 1 ∧ ¬x ≡ y [ZMOD ↑p] ∧ x * y * z ≠ 0 ∧ ¬↑p ∣ x * y * z
Theorem: FltRegular.a_not_cong_b
Proof state before:
case pos
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
⊢ ∃ x y z, x ^ p + y ^ p = z ^ p ∧ {x, y, z}.gcd id = 1 ∧ ¬x ≡ y [ZMOD ↑p] ∧ x * y * z ≠ 0 ∧ ¬↑p ∣ x * y * z

case neg
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : ¬a ≡ b [ZMOD ↑p]
⊢ ∃ x y z, x ^ p + y ^ p = z ^ p ∧ {x, y, z}.gcd id = 1 ∧ ¬x ≡ y [ZMOD ↑p] ∧ x * y * z ≠ 0 ∧ ¬↑p ∣ x * y * z
Tactic:
swap
Proof state after:
case neg
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : ¬a ≡ b [ZMOD ↑p]
⊢ ∃ x y z, x ^ p + y ^ p = z ^ p ∧ {x, y, z}.gcd id = 1 ∧ ¬x ≡ y [ZMOD ↑p] ∧ x * y * z ≠ 0 ∧ ¬↑p ∣ x * y * z

case pos
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
⊢ ∃ x y z, x ^ p + y ^ p = z ^ p ∧ {x, y, z}.gcd id = 1 ∧ ¬x ≡ y [ZMOD ↑p] ∧ x * y * z ≠ 0 ∧ ¬↑p ∣ x * y * z
Theorem: FltRegular.a_not_cong_b
Proof state before:
case pos
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
⊢ ∃ x y z, x ^ p + y ^ p = z ^ p ∧ {x, y, z}.gcd id = 1 ∧ ¬x ≡ y [ZMOD ↑p] ∧ x * y * z ≠ 0 ∧ ¬↑p ∣ x * y * z
Tactic:
refine' ⟨a, -c, -b, ⟨_, _, fun habs => _, _, _⟩⟩
Proof state after:
case pos.refine'_1
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
⊢ a ^ p + (-c) ^ p = (-b) ^ p

case pos.refine'_2
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
⊢ {a, -c, -b}.gcd id = 1

case pos.refine'_3
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
habs : a ≡ -c [ZMOD ↑p]
⊢ False

case pos.refine'_4
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
⊢ a * -c * -b ≠ 0

case pos.refine'_5
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
⊢ ¬↑p ∣ a * -c * -b
Theorem: FltRegular.a_not_cong_b
Proof state before:
case neg
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : ¬a ≡ b [ZMOD ↑p]
⊢ ∃ x y z, x ^ p + y ^ p = z ^ p ∧ {x, y, z}.gcd id = 1 ∧ ¬x ≡ y [ZMOD ↑p] ∧ x * y * z ≠ 0 ∧ ¬↑p ∣ x * y * z
Tactic:
exact ⟨a, b, c, ⟨h, hgcd, H, hprod, caseI⟩⟩
Proof state after:
no goals
Theorem: FltRegular.a_not_cong_b
Proof state before:
case pos.refine'_1
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
⊢ a ^ p + (-c) ^ p = (-b) ^ p
Tactic:
have hpodd : p ≠ 2 := by linarith
Proof state after:
case pos.refine'_1
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
hpodd : p ≠ 2
⊢ a ^ p + (-c) ^ p = (-b) ^ p
Theorem: FltRegular.a_not_cong_b
Proof state before:
case pos.refine'_1
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
hpodd : p ≠ 2
⊢ a ^ p + (-c) ^ p = (-b) ^ p
Tactic:
rw [neg_pow, (Or.resolve_left hpri.eq_two_or_odd' hpodd).neg_one_pow, neg_pow,
  (Or.resolve_left hpri.eq_two_or_odd' hpodd).neg_one_pow]
Proof state after:
case pos.refine'_1
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
hpodd : p ≠ 2
⊢ a ^ p + -1 * c ^ p = -1 * b ^ p
Theorem: FltRegular.a_not_cong_b
Proof state before:
case pos.refine'_1
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
hpodd : p ≠ 2
⊢ a ^ p + -1 * c ^ p = -1 * b ^ p
Tactic:
simp only [← sub_eq_add_neg, sub_eq_iff_eq_add, neg_mul, one_mul]
Proof state after:
case pos.refine'_1
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
hpodd : p ≠ 2
⊢ a ^ p = -b ^ p + c ^ p
Theorem: FltRegular.a_not_cong_b
Proof state before:
case pos.refine'_1
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
hpodd : p ≠ 2
⊢ a ^ p = -b ^ p + c ^ p
Tactic:
symm
Proof state after:
case pos.refine'_1
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
hpodd : p ≠ 2
⊢ -b ^ p + c ^ p = a ^ p
Theorem: FltRegular.a_not_cong_b
Proof state before:
case pos.refine'_1
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
hpodd : p ≠ 2
⊢ -b ^ p + c ^ p = a ^ p
Tactic:
rw [neg_add_eq_iff_eq_add, add_comm]
Proof state after:
case pos.refine'_1
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
hpodd : p ≠ 2
⊢ c ^ p = a ^ p + b ^ p
Theorem: FltRegular.a_not_cong_b
Proof state before:
case pos.refine'_1
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
hpodd : p ≠ 2
⊢ c ^ p = a ^ p + b ^ p
Tactic:
exact h.symm
Proof state after:
no goals
Theorem: FltRegular.a_not_cong_b
Proof state before:
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
⊢ p ≠ 2
Tactic:
linarith
Proof state after:
no goals
Theorem: FltRegular.a_not_cong_b
Proof state before:
case pos.refine'_2
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
⊢ {a, -c, -b}.gcd id = 1
Tactic:
convert hgcd using 1
Proof state after:
case h.e'_2
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
⊢ {a, -c, -b}.gcd id = {a, b, c}.gcd id
Theorem: FltRegular.a_not_cong_b
Proof state before:
case h.e'_2
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
this : {a, -c, -b} = {a, -b, -c}
⊢ {a, -c, -b}.gcd id = {a, b, c}.gcd id
Tactic:
rw [this]
Proof state after:
case h.e'_2
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
this : {a, -c, -b} = {a, -b, -c}
⊢ {a, -b, -c}.gcd id = {a, b, c}.gcd id
Theorem: FltRegular.a_not_cong_b
Proof state before:
case h.e'_2
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
this : {a, -c, -b} = {a, -b, -c}
⊢ {a, -b, -c}.gcd id = {a, b, c}.gcd id
Tactic:
simp only [gcd_insert, id, gcd_singleton, normalize_apply, neg_mul]
Proof state after:
case h.e'_2
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
this : {a, -c, -b} = {a, -b, -c}
⊢ GCDMonoid.gcd a (GCDMonoid.gcd (-b) (-(c * ↑(normUnit (-c))))) = GCDMonoid.gcd a (GCDMonoid.gcd b (c * ↑(normUnit c)))
Theorem: FltRegular.a_not_cong_b
Proof state before:
case h.e'_2
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
this : {a, -c, -b} = {a, -b, -c}
⊢ GCDMonoid.gcd a (GCDMonoid.gcd (-b) (-(c * ↑(normUnit (-c))))) = GCDMonoid.gcd a (GCDMonoid.gcd b (c * ↑(normUnit c)))
Tactic:
congr 1
Proof state after:
case h.e'_2.e_a
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
this : {a, -c, -b} = {a, -b, -c}
⊢ GCDMonoid.gcd (-b) (-(c * ↑(normUnit (-c)))) = GCDMonoid.gcd b (c * ↑(normUnit c))
Theorem: FltRegular.a_not_cong_b
Proof state before:
case h.e'_2.e_a
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
this : {a, -c, -b} = {a, -b, -c}
⊢ GCDMonoid.gcd (-b) (-(c * ↑(normUnit (-c)))) = GCDMonoid.gcd b (c * ↑(normUnit c))
Tactic:
rw [← coe_gcd, ← coe_gcd, Int.gcd_eq_natAbs, Int.gcd_eq_natAbs]
Proof state after:
case h.e'_2.e_a
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
this : {a, -c, -b} = {a, -b, -c}
⊢ ↑((-b).natAbs.gcd (-(c * ↑(normUnit (-c)))).natAbs) = ↑(b.natAbs.gcd (c * ↑(normUnit c)).natAbs)
Theorem: FltRegular.a_not_cong_b
Proof state before:
case h.e'_2.e_a
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
this : {a, -c, -b} = {a, -b, -c}
⊢ ↑((-b).natAbs.gcd (-(c * ↑(normUnit (-c)))).natAbs) = ↑(b.natAbs.gcd (c * ↑(normUnit c)).natAbs)
Tactic:
simp only [natAbs_neg, Nat.cast_inj]
Proof state after:
case h.e'_2.e_a
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
this : {a, -c, -b} = {a, -b, -c}
⊢ b.natAbs.gcd (c * ↑(normUnit (-c))).natAbs = b.natAbs.gcd (c * ↑(normUnit c)).natAbs
Theorem: FltRegular.a_not_cong_b
Proof state before:
case h.e'_2.e_a
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
this : {a, -c, -b} = {a, -b, -c}
⊢ b.natAbs.gcd (c * ↑(normUnit (-c))).natAbs = b.natAbs.gcd (c * ↑(normUnit c)).natAbs
Tactic:
rcases Int.isUnit_iff.1 (normUnit (-c)).isUnit, Int.isUnit_iff.1 (normUnit c).isUnit with
  ⟨H₁ | H₂, H₃ | H₄⟩
Proof state after:
case h.e'_2.e_a.inl.inl
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
this : {a, -c, -b} = {a, -b, -c}
H₁ : ↑(normUnit (-c)) = 1
H₃ : ↑(normUnit c) = 1
⊢ b.natAbs.gcd (c * ↑(normUnit (-c))).natAbs = b.natAbs.gcd (c * ↑(normUnit c)).natAbs

case h.e'_2.e_a.inl.inr
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
this : {a, -c, -b} = {a, -b, -c}
H₁ : ↑(normUnit (-c)) = 1
H₄ : ↑(normUnit c) = -1
⊢ b.natAbs.gcd (c * ↑(normUnit (-c))).natAbs = b.natAbs.gcd (c * ↑(normUnit c)).natAbs

case h.e'_2.e_a.inr.inl
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
this : {a, -c, -b} = {a, -b, -c}
H₂ : ↑(normUnit (-c)) = -1
H₃ : ↑(normUnit c) = 1
⊢ b.natAbs.gcd (c * ↑(normUnit (-c))).natAbs = b.natAbs.gcd (c * ↑(normUnit c)).natAbs

case h.e'_2.e_a.inr.inr
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
this : {a, -c, -b} = {a, -b, -c}
H₂ : ↑(normUnit (-c)) = -1
H₄ : ↑(normUnit c) = -1
⊢ b.natAbs.gcd (c * ↑(normUnit (-c))).natAbs = b.natAbs.gcd (c * ↑(normUnit c)).natAbs
Theorem: FltRegular.a_not_cong_b
Proof state before:
case refine'_2
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
x : ℤ
hx : x ∈ {a, -b, -c}
⊢ x ∈ {a, -c, -b}
Tactic:
simp only [mem_insert, mem_singleton] at hx
Proof state after:
case refine'_2
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
x : ℤ
hx : x = a ∨ x = -b ∨ x = -c
⊢ x ∈ {a, -c, -b}
Theorem: FltRegular.a_not_cong_b
Proof state before:
case refine'_2
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
x : ℤ
hx : x = a ∨ x = -b ∨ x = -c
⊢ x ∈ {a, -c, -b}
Tactic:
rcases hx with (H | H | H) <;> simp [H]
Proof state after:
no goals
Theorem: FltRegular.a_not_cong_b
Proof state before:
case h.e'_2.e_a.inl.inl
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
this : {a, -c, -b} = {a, -b, -c}
H₁ : ↑(normUnit (-c)) = 1
H₃ : ↑(normUnit c) = 1
⊢ b.natAbs.gcd (c * ↑(normUnit (-c))).natAbs = b.natAbs.gcd (c * ↑(normUnit c)).natAbs
Tactic:
simp [H₁, H₃]
Proof state after:
no goals
Theorem: FltRegular.a_not_cong_b
Proof state before:
case h.e'_2.e_a.inl.inr
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
this : {a, -c, -b} = {a, -b, -c}
H₁ : ↑(normUnit (-c)) = 1
H₄ : ↑(normUnit c) = -1
⊢ b.natAbs.gcd (c * ↑(normUnit (-c))).natAbs = b.natAbs.gcd (c * ↑(normUnit c)).natAbs
Tactic:
simp [H₁, H₄]
Proof state after:
no goals
Theorem: FltRegular.a_not_cong_b
Proof state before:
case h.e'_2.e_a.inr.inl
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
this : {a, -c, -b} = {a, -b, -c}
H₂ : ↑(normUnit (-c)) = -1
H₃ : ↑(normUnit c) = 1
⊢ b.natAbs.gcd (c * ↑(normUnit (-c))).natAbs = b.natAbs.gcd (c * ↑(normUnit c)).natAbs
Tactic:
simp [H₂, H₃]
Proof state after:
no goals
Theorem: FltRegular.a_not_cong_b
Proof state before:
case h.e'_2.e_a.inr.inr
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
this : {a, -c, -b} = {a, -b, -c}
H₂ : ↑(normUnit (-c)) = -1
H₄ : ↑(normUnit c) = -1
⊢ b.natAbs.gcd (c * ↑(normUnit (-c))).natAbs = b.natAbs.gcd (c * ↑(normUnit c)).natAbs
Tactic:
simp [H₂, H₄]
Proof state after:
no goals
Theorem: FltRegular.a_not_cong_b
Proof state before:
case pos.refine'_3
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
habs : a ≡ -c [ZMOD ↑p]
⊢ False
Tactic:
have hp3 : p ≠ 3 := by linarith
Proof state after:
case pos.refine'_3
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
habs : a ≡ -c [ZMOD ↑p]
hp3 : p ≠ 3
⊢ False
Theorem: FltRegular.a_not_cong_b
Proof state before:
case pos.refine'_3
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
habs : a ≡ -c [ZMOD ↑p]
hp3 : p ≠ 3
⊢ False
Tactic:
rw [← ZMod.intCast_eq_intCast_iff] at habs H
Proof state after:
case pos.refine'_3
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : ↑a = ↑b
habs : ↑a = ↑(-c)
hp3 : p ≠ 3
⊢ False
Theorem: FltRegular.a_not_cong_b
Proof state before:
case pos.refine'_3
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : ↑a = ↑b
habs : ↑a = ↑(-c)
hp3 : p ≠ 3
⊢ False
Tactic:
rw [H] at habs
Proof state after:
case pos.refine'_3
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : ↑a = ↑b
habs : ↑b = ↑(-c)
hp3 : p ≠ 3
⊢ False
Theorem: FltRegular.a_not_cong_b
Proof state before:
case pos.refine'_3
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : ↑a = ↑b
habs : ↑b = ↑(-c)
hp3 : p ≠ 3
⊢ False
Tactic:
rw [ZMod.intCast_eq_intCast_iff] at habs H
Proof state after:
case pos.refine'_3
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
habs : b ≡ -c [ZMOD ↑p]
hp3 : p ≠ 3
⊢ False
Theorem: FltRegular.a_not_cong_b
Proof state before:
case pos.refine'_3
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
habs : b ≡ -c [ZMOD ↑p]
hp3 : p ≠ 3
⊢ False
Tactic:
obtain ⟨n, hn⟩ := p_dvd_c_of_ab_of_anegc hpri hp3 h H habs
Proof state after:
case pos.refine'_3.intro
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
habs : b ≡ -c [ZMOD ↑p]
hp3 : p ≠ 3
n : ℤ
hn : c = ↑p * n
⊢ False