Theorem: FltRegular.a_not_cong_b (FltRegular/MayAssume/Lemmas.lean)

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]
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

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
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

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 => _, _, _⟩⟩
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

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⟩⟩
State after:
no goals

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
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

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]
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

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]
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

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
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

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]
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

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
State after:
no goals

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
State after:
no goals

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
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

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]
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

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]
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)))

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
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))

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]
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)

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]
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

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₄⟩
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

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
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}

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]
State after:
no goals

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₃]
State after:
no goals

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₄]
State after:
no goals

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₃]
State after:
no goals

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₄]
State after:
no goals

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
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

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
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

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
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

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
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

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
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

State before:
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
Tactic:
refine' caseI ⟨a * b * n, _⟩
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
⊢ a * b * c = ↑p * (a * b * n)

State before:
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
⊢ a * b * c = ↑p * (a * b * n)
Tactic:
rw [hn]
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
⊢ a * b * (↑p * n) = ↑p * (a * b * n)

State before:
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
⊢ a * b * (↑p * n) = ↑p * (a * b * n)
Tactic:
ring
State after:
no goals

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]
habs : a ≡ -c [ZMOD ↑p]
⊢ p ≠ 3
Tactic:
linarith
State after:
no goals

State before:
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
Tactic:
convert hprod using 1
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 = a * b * c

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]
⊢ a * -c * -b = a * b * c
Tactic:
ring
State after:
no goals

State before:
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
Tactic:
ring_nf at caseI ⊢
State after:
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 * b * c

State before:
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 * b * c
Tactic:
exact caseI
State after:
no goals