awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.FLT.Polynomial
Goal:
k : Type u_1
inst : Field k
n : ℕ
hn : 3 ≤ n
chn : Ne.{u_1 + 1} (α := k) (↑n : k) 0
a b c a' b' : k[X]
d : k[X] := @gcd _ CommSemiring.toCommMonoidWithZero _ a b
hb : d ≠ 0 ∧ b' ≠ 0
ha : d ≠ 0 ∧ a' ≠ 0
eq_a : a = a' * d
eq_b : b = b' * d
hd : d ≠ 0
c' : k[X]
heq : a' ^ n + b' ^ n = c' ^ n
hc : d ≠ 0 ∧ c' ≠ 0
eq_c : c = c' * d
⊢ IsCoprime (a / @gcd _ CommSemiring.toCommMonoidWithZero _ a b) (b / @gcd _ CommSemiring.toCommMonoidWithZero _ a b)

Tactic:
isCoprime_div_gcd_div_gcd _

Premises used: isCoprime_div_gcd_div_gcd
-- Module: Mathlib.NumberTheory.FLT.Polynomial
Goal:
k : Type u_1
inst : Field k
n : ℕ
hn : 3 ≤ n
chn : Ne.{u_1 + 1} (α := k) (↑n : k) 0
a b c a' b' : k[X]
d : k[X] := @gcd _ CommSemiring.toCommMonoidWithZero _ a b
hb : d ≠ 0 ∧ b' ≠ 0
ha : d ≠ 0 ∧ a' ≠ 0
eq_a : a = a' * d
eq_b : b = b' * d
hd : d ≠ 0
c' : k[X]
heq : a' ^ n + b' ^ n = c' ^ n
hc : d ≠ 0 ∧ c' ≠ 0
eq_c : c = c' * d
h : a' = a / @gcd _ CommSemiring.toCommMonoidWithZero _ a b
h₁ : b' = b / @gcd _ CommSemiring.toCommMonoidWithZero _ a b
convert_3 : GCDMonoid k[X]
convert_4 convert_5 : k[X]
convert_6 : b ≠ 0
⊢ IsCoprime a' b'

Tactic:
convert! isCoprime_div_gcd_div_gcd _

Premises used: isCoprime_div_gcd_div_gcd
-- Module: Mathlib.NumberTheory.FLT.Polynomial
Goal:
k : Type u_1
inst : Field k
n : ℕ
hn : 3 ≤ n
chn : Ne.{u_1 + 1} (α := k) (↑n : k) 0
a b c a' b' : k[X]
d : k[X] := @gcd _ CommSemiring.toCommMonoidWithZero _ a b
hb : d ≠ 0 ∧ b' ≠ 0
ha : d ≠ 0 ∧ a' ≠ 0
eq_a : a = a' * d
eq_b : b = b' * d
hd : d ≠ 0
c' : k[X]
heq : a' ^ n + b' ^ n = c' ^ n
hc : d ≠ 0 ∧ c' ≠ 0
eq_c : c = c' * d
⊢ a' = a / @gcd _ CommSemiring.toCommMonoidWithZero _ a b

Tactic:
EuclideanDomain.eq_div_of_mul_eq_left ha.left eq_a.symm

Premises used: EuclideanDomain.eq_div_of_mul_eq_left, And.left, Eq.symm
-- Module: Mathlib.NumberTheory.FLT.Polynomial
Goal:
k : Type u_1
inst : Field k
n : ℕ
hn : 3 ≤ n
chn : Ne.{u_1 + 1} (α := k) (↑n : k) 0
a b c a' b' : k[X]
d : k[X] := @gcd _ CommSemiring.toCommMonoidWithZero _ a b
hb : d ≠ 0 ∧ b' ≠ 0
ha : d ≠ 0 ∧ a' ≠ 0
eq_a : a = a' * d
eq_b : b = b' * d
hd : d ≠ 0
c' : k[X]
heq : a' ^ n + b' ^ n = c' ^ n
hc : d ≠ 0 ∧ c' ≠ 0
eq_c : c = c' * d
⊢ a' = a / @gcd _ CommSemiring.toCommMonoidWithZero _ a b

Tactic:
exact EuclideanDomain.eq_div_of_mul_eq_left ha.left eq_a.symm

Premises used: EuclideanDomain.eq_div_of_mul_eq_left, And.left, Eq.symm
-- Module: Mathlib.NumberTheory.FLT.Polynomial
Goal:
k : Type u_1
inst : Field k
n : ℕ
hn : 3 ≤ n
chn : Ne.{u_1 + 1} (α := k) (↑n : k) 0
a b c a' b' : k[X]
d : k[X] := @gcd _ CommSemiring.toCommMonoidWithZero _ a b
hb : d ≠ 0 ∧ b' ≠ 0
ha : d ≠ 0 ∧ a' ≠ 0
eq_a : a = a' * d
eq_b : b = b' * d
hd : d ≠ 0
c' : k[X]
heq : a' ^ n + b' ^ n = c' ^ n
hc : d ≠ 0 ∧ c' ≠ 0
eq_c : c = c' * d
⊢ b' = b / @gcd _ CommSemiring.toCommMonoidWithZero _ a b

Tactic:
EuclideanDomain.eq_div_of_mul_eq_left ha.left eq_b.symm

Premises used: EuclideanDomain.eq_div_of_mul_eq_left, And.left, Eq.symm
-- Module: Mathlib.NumberTheory.FLT.Polynomial
Goal:
k : Type u_1
inst : Field k
n : ℕ
hn : 3 ≤ n
chn : Ne.{u_1 + 1} (α := k) (↑n : k) 0
a b c a' b' : k[X]
d : k[X] := @gcd _ CommSemiring.toCommMonoidWithZero _ a b
hb : d ≠ 0 ∧ b' ≠ 0
ha : d ≠ 0 ∧ a' ≠ 0
eq_a : a = a' * d
eq_b : b = b' * d
hd : d ≠ 0
c' : k[X]
heq : a' ^ n + b' ^ n = c' ^ n
hc : d ≠ 0 ∧ c' ≠ 0
eq_c : c = c' * d
⊢ b' = b / @gcd _ CommSemiring.toCommMonoidWithZero _ a b

Tactic:
exact EuclideanDomain.eq_div_of_mul_eq_left ha.left eq_b.symm

Premises used: EuclideanDomain.eq_div_of_mul_eq_left, And.left, Eq.symm
-- Module: Mathlib.NumberTheory.FLT.Polynomial
Goal:
k : Type u_1
inst : Field k
n : ℕ
hn : 3 ≤ n
chn : Ne.{u_1 + 1} (α := k) (↑n : k) 0
a b c a' b' : k[X]
d : k[X] := @gcd _ CommSemiring.toCommMonoidWithZero _ a b
hb : d ≠ 0 ∧ b' ≠ 0
ha : d ≠ 0 ∧ a' ≠ 0
eq_a : a = a' * d
eq_b : b = b' * d
hd : d ≠ 0
c' : k[X]
heq : a' ^ n + b' ^ n = c' ^ n
hc : d ≠ 0 ∧ c' ≠ 0
eq_c : c = c' * d
convert_6 : b' * d ≠ 0
⊢ b ≠ 0

Tactic:
rw [eq_b]
-- Module: Mathlib.NumberTheory.FLT.Polynomial
Goal:
k : Type u_1
inst : Field k
n : ℕ
hn : 3 ≤ n
chn : Ne.{u_1 + 1} (α := k) (↑n : k) 0
a b c a' b' : k[X]
d : k[X] := @gcd _ CommSemiring.toCommMonoidWithZero _ a b
hb : d ≠ 0 ∧ b' ≠ 0
ha : d ≠ 0 ∧ a' ≠ 0
eq_a : a = a' * d
eq_b : b = b' * d
hd : d ≠ 0
c' : k[X]
heq : a' ^ n + b' ^ n = c' ^ n
hc : d ≠ 0 ∧ c' ≠ 0
eq_c : c = c' * d
⊢ b' * d ≠ 0

Tactic:
mul_ne_zero hb.right hb.left

Premises used: And.right, And.left, mul_ne_zero
-- Module: Mathlib.NumberTheory.FLT.Polynomial
Goal:
k : Type u_1
inst : Field k
n : ℕ
hn : 3 ≤ n
chn : Ne.{u_1 + 1} (α := k) (↑n : k) 0
a b c a' b' : k[X]
d : k[X] := @gcd _ CommSemiring.toCommMonoidWithZero _ a b
hb : d ≠ 0 ∧ b' ≠ 0
ha : d ≠ 0 ∧ a' ≠ 0
eq_a : a = a' * d
eq_b : b = b' * d
hd : d ≠ 0
c' : k[X]
heq : a' ^ n + b' ^ n = c' ^ n
hc : d ≠ 0 ∧ c' ≠ 0
eq_c : c = c' * d
⊢ b' * d ≠ 0

Tactic:
exact mul_ne_zero hb.right hb.left

Premises used: And.right, And.left, mul_ne_zero
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
n : ZMod 9
⊢ Dvd.dvd (α := ℕ) 3 9

Tactic:
simp
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
n : ZMod 9
revert :
  ∀ {n : ZMod 9},
    Ne (α := ZMod 3) ((castHom ⋯ (ZMod 3) : (a : ZMod 9) → ZMod 3) n : ZMod 3) (0 : ZMod 3) →
      HPow.hPow (β := ℕ) n 3 = 1 ∨ HPow.hPow (β := ℕ) n 3 = 8
⊢ Ne (α := ZMod 3) ((castHom ⋯ (ZMod 3) : (a : ZMod 9) → ZMod 3) n : ZMod 3) (0 : ZMod 3) →
    HPow.hPow (β := ℕ) n 3 = 1 ∨ HPow.hPow (β := ℕ) n 3 = 8

Tactic:
revert n
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
⊢ ∀ {n : ZMod 9},
    Ne (α := ZMod 3) ((castHom ⋯ (ZMod 3) : (a : ZMod 9) → ZMod 3) n : ZMod 3) (0 : ZMod 3) →
      HPow.hPow (β := ℕ) n 3 = 1 ∨ HPow.hPow (β := ℕ) n 3 = 8

Tactic:
decide
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
n : ℤ
h : ¬3 ∣ n
a : Ne (α := ZMod 3) ((castHom ⋯ (ZMod 3) : (a : ZMod 9) → ZMod 3) (↑n : ZMod 9)) 0
⊢ HPow.hPow (α := ZMod 9) (β := ℕ) (↑n : ZMod 9) 3 = 1 ∨ HPow.hPow (α := ZMod 9) (β := ℕ) (↑n : ZMod 9) 3 = 8

Tactic:
apply cube_of_castHom_ne_zero

Premises used: _private.0.cube_of_castHom_ne_zero
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
n : ℤ
h : ¬3 ∣ n
a : Ne (α := ZMod 3) (↑n : ZMod 3) 0
a₁ : ¬Eq (α := ZMod 3) (↑n : ZMod 3) 0
a₂ a₃ a₄ a₅ : ¬(↑3 : ℤ) ∣ n
⊢ Ne (α := ZMod 3) ((castHom ⋯ (ZMod 3) : (a : ZMod 9) → ZMod 3) (↑n : ZMod 9)) 0

Tactic:
rwa [map_intCast, Ne, ZMod.intCast_zmod_eq_zero_iff_dvd]

Premises used: map_intCast, Ne, ZMod.intCast_zmod_eq_zero_iff_dvd
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
a b c : ℤ
hdvd : ¬3 ∣ a * b * c
⊢ (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c

Tactic:
simp_rw [Int.prime_three.dvd_mul, not_or] at hdvd

Premises used: Prime.dvd_mul, Int.prime_three, not_or
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
apply :
  ¬Eq (α := ZMod 9) (↑(HPow.hPow (β := ℕ) a 3 + HPow.hPow (β := ℕ) b 3) : ZMod 9) (↑(HPow.hPow (β := ℕ) c 3) : ZMod 9)
⊢ HPow.hPow (β := ℕ) a 3 + HPow.hPow (β := ℕ) b 3 ≠ HPow.hPow (β := ℕ) c 3

Tactic:
apply mt (congrArg (Int.cast : ℤ → ZMod 9))

Premises used: Int.cast, congrArg, mt
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
simp_rw :
  ¬HPow.hPow (α := ZMod 9) (β := ℕ) (↑a : ZMod 9) 3 + HPow.hPow (α := ZMod 9) (β := ℕ) (↑b : ZMod 9) 3 =
      HPow.hPow (α := ZMod 9) (β := ℕ) (↑c : ZMod 9) 3
⊢ ¬Eq (α := ZMod 9) (↑(HPow.hPow (β := ℕ) a 3 + HPow.hPow (β := ℕ) b 3) : ZMod 9) (↑(HPow.hPow (β := ℕ) c 3) : ZMod 9)

Tactic:
simp_rw [Int.cast_add, Int.cast_pow]

Premises used: Int.cast_pow, Int.cast_add
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
inl :
  ∀ (ha : HPow.hPow (α := ZMod 9) (β := ℕ) (↑a : ZMod 9) 3 = 1),
    ¬HPow.hPow (α := ZMod 9) (β := ℕ) (↑a : ZMod 9) 3 + HPow.hPow (α := ZMod 9) (β := ℕ) (↑b : ZMod 9) 3 =
        HPow.hPow (α := ZMod 9) (β := ℕ) (↑c : ZMod 9) 3
inr :
  ∀ (ha : HPow.hPow (α := ZMod 9) (β := ℕ) (↑a : ZMod 9) 3 = 8),
    ¬HPow.hPow (α := ZMod 9) (β := ℕ) (↑a : ZMod 9) 3 + HPow.hPow (α := ZMod 9) (β := ℕ) (↑b : ZMod 9) 3 =
        HPow.hPow (α := ZMod 9) (β := ℕ) (↑c : ZMod 9) 3
⊢ ¬HPow.hPow (α := ZMod 9) (β := ℕ) (↑a : ZMod 9) 3 + HPow.hPow (α := ZMod 9) (β := ℕ) (↑b : ZMod 9) 3 =
      HPow.hPow (α := ZMod 9) (β := ℕ) (↑c : ZMod 9) 3

Tactic:
rcases cube_of_not_dvd hdvd.1.1 with ha | ha

Premises used: _private.0.cube_of_not_dvd, And.left
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : HPow.hPow (α := ZMod 9) (β := ℕ) (↑a : ZMod 9) 3 = 1
inl :
  ∀ (hb : HPow.hPow (α := ZMod 9) (β := ℕ) (↑b : ZMod 9) 3 = 1),
    ¬HPow.hPow (α := ZMod 9) (β := ℕ) (↑a : ZMod 9) 3 + HPow.hPow (α := ZMod 9) (β := ℕ) (↑b : ZMod 9) 3 =
        HPow.hPow (α := ZMod 9) (β := ℕ) (↑c : ZMod 9) 3
inl₁ :
  ∀ (hb : HPow.hPow (α := ZMod 9) (β := ℕ) (↑b : ZMod 9) 3 = 8),
    ¬HPow.hPow (α := ZMod 9) (β := ℕ) (↑a : ZMod 9) 3 + HPow.hPow (α := ZMod 9) (β := ℕ) (↑b : ZMod 9) 3 =
        HPow.hPow (α := ZMod 9) (β := ℕ) (↑c : ZMod 9) 3
⊢ ¬HPow.hPow (α := ZMod 9) (β := ℕ) (↑a : ZMod 9) 3 + HPow.hPow (α := ZMod 9) (β := ℕ) (↑b : ZMod 9) 3 =
      HPow.hPow (α := ZMod 9) (β := ℕ) (↑c : ZMod 9) 3

Tactic:
rcases cube_of_not_dvd hdvd.1.2 with hb | hb

Premises used: _private.0.cube_of_not_dvd, And.right, And.left
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : HPow.hPow (α := ZMod 9) (β := ℕ) (↑a : ZMod 9) 3 = 8
inr :
  ∀ (hb : HPow.hPow (α := ZMod 9) (β := ℕ) (↑b : ZMod 9) 3 = 1),
    ¬HPow.hPow (α := ZMod 9) (β := ℕ) (↑a : ZMod 9) 3 + HPow.hPow (α := ZMod 9) (β := ℕ) (↑b : ZMod 9) 3 =
        HPow.hPow (α := ZMod 9) (β := ℕ) (↑c : ZMod 9) 3
inr₁ :
  ∀ (hb : HPow.hPow (α := ZMod 9) (β := ℕ) (↑b : ZMod 9) 3 = 8),
    ¬HPow.hPow (α := ZMod 9) (β := ℕ) (↑a : ZMod 9) 3 + HPow.hPow (α := ZMod 9) (β := ℕ) (↑b : ZMod 9) 3 =
        HPow.hPow (α := ZMod 9) (β := ℕ) (↑c : ZMod 9) 3
⊢ ¬HPow.hPow (α := ZMod 9) (β := ℕ) (↑a : ZMod 9) 3 + HPow.hPow (α := ZMod 9) (β := ℕ) (↑b : ZMod 9) 3 =
      HPow.hPow (α := ZMod 9) (β := ℕ) (↑c : ZMod 9) 3

Tactic:
rcases cube_of_not_dvd hdvd.1.2 with hb | hb

Premises used: _private.0.cube_of_not_dvd, And.right, And.left
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : HPow.hPow (α := ZMod 9) (β := ℕ) (↑a : ZMod 9) 3 = 1
hb : HPow.hPow (α := ZMod 9) (β := ℕ) (↑b : ZMod 9) 3 = 1
inl :
  ∀ (hc : HPow.hPow (α := ZMod 9) (β := ℕ) (↑c : ZMod 9) 3 = 1),
    ¬HPow.hPow (α := ZMod 9) (β := ℕ) (↑a : ZMod 9) 3 + HPow.hPow (α := ZMod 9) (β := ℕ) (↑b : ZMod 9) 3 =
        HPow.hPow (α := ZMod 9) (β := ℕ) (↑c : ZMod 9) 3
inl₁ :
  ∀ (hc : HPow.hPow (α := ZMod 9) (β := ℕ) (↑c : ZMod 9) 3 = 8),
    ¬HPow.hPow (α := ZMod 9) (β := ℕ) (↑a : ZMod 9) 3 + HPow.hPow (α := ZMod 9) (β := ℕ) (↑b : ZMod 9) 3 =
        HPow.hPow (α := ZMod 9) (β := ℕ) (↑c : ZMod 9) 3
⊢ ¬HPow.hPow (α := ZMod 9) (β := ℕ) (↑a : ZMod 9) 3 + HPow.hPow (α := ZMod 9) (β := ℕ) (↑b : ZMod 9) 3 =
      HPow.hPow (α := ZMod 9) (β := ℕ) (↑c : ZMod 9) 3

Tactic:
rcases cube_of_not_dvd hdvd.2 with hc | hc

Premises used: _private.0.cube_of_not_dvd, And.right
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : HPow.hPow (α := ZMod 9) (β := ℕ) (↑a : ZMod 9) 3 = 1
hb : HPow.hPow (α := ZMod 9) (β := ℕ) (↑b : ZMod 9) 3 = 8
inl :
  ∀ (hc : HPow.hPow (α := ZMod 9) (β := ℕ) (↑c : ZMod 9) 3 = 1),
    ¬HPow.hPow (α := ZMod 9) (β := ℕ) (↑a : ZMod 9) 3 + HPow.hPow (α := ZMod 9) (β := ℕ) (↑b : ZMod 9) 3 =
        HPow.hPow (α := ZMod 9) (β := ℕ) (↑c : ZMod 9) 3
inl₁ :
  ∀ (hc : HPow.hPow (α := ZMod 9) (β := ℕ) (↑c : ZMod 9) 3 = 8),
    ¬HPow.hPow (α := ZMod 9) (β := ℕ) (↑a : ZMod 9) 3 + HPow.hPow (α := ZMod 9) (β := ℕ) (↑b : ZMod 9) 3 =
        HPow.hPow (α := ZMod 9) (β := ℕ) (↑c : ZMod 9) 3
⊢ ¬HPow.hPow (α := ZMod 9) (β := ℕ) (↑a : ZMod 9) 3 + HPow.hPow (α := ZMod 9) (β := ℕ) (↑b : ZMod 9) 3 =
      HPow.hPow (α := ZMod 9) (β := ℕ) (↑c : ZMod 9) 3

Tactic:
rcases cube_of_not_dvd hdvd.2 with hc | hc

Premises used: _private.0.cube_of_not_dvd, And.right
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : HPow.hPow (α := ZMod 9) (β := ℕ) (↑a : ZMod 9) 3 = 8
hb : HPow.hPow (α := ZMod 9) (β := ℕ) (↑b : ZMod 9) 3 = 1
inr :
  ∀ (hc : HPow.hPow (α := ZMod 9) (β := ℕ) (↑c : ZMod 9) 3 = 1),
    ¬HPow.hPow (α := ZMod 9) (β := ℕ) (↑a : ZMod 9) 3 + HPow.hPow (α := ZMod 9) (β := ℕ) (↑b : ZMod 9) 3 =
        HPow.hPow (α := ZMod 9) (β := ℕ) (↑c : ZMod 9) 3
inr₁ :
  ∀ (hc : HPow.hPow (α := ZMod 9) (β := ℕ) (↑c : ZMod 9) 3 = 8),
    ¬HPow.hPow (α := ZMod 9) (β := ℕ) (↑a : ZMod 9) 3 + HPow.hPow (α := ZMod 9) (β := ℕ) (↑b : ZMod 9) 3 =
        HPow.hPow (α := ZMod 9) (β := ℕ) (↑c : ZMod 9) 3
⊢ ¬HPow.hPow (α := ZMod 9) (β := ℕ) (↑a : ZMod 9) 3 + HPow.hPow (α := ZMod 9) (β := ℕ) (↑b : ZMod 9) 3 =
      HPow.hPow (α := ZMod 9) (β := ℕ) (↑c : ZMod 9) 3

Tactic:
rcases cube_of_not_dvd hdvd.2 with hc | hc

Premises used: _private.0.cube_of_not_dvd, And.right
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : HPow.hPow (α := ZMod 9) (β := ℕ) (↑a : ZMod 9) 3 = 8
hb : HPow.hPow (α := ZMod 9) (β := ℕ) (↑b : ZMod 9) 3 = 8
inr :
  ∀ (hc : HPow.hPow (α := ZMod 9) (β := ℕ) (↑c : ZMod 9) 3 = 1),
    ¬HPow.hPow (α := ZMod 9) (β := ℕ) (↑a : ZMod 9) 3 + HPow.hPow (α := ZMod 9) (β := ℕ) (↑b : ZMod 9) 3 =
        HPow.hPow (α := ZMod 9) (β := ℕ) (↑c : ZMod 9) 3
inr₁ :
  ∀ (hc : HPow.hPow (α := ZMod 9) (β := ℕ) (↑c : ZMod 9) 3 = 8),
    ¬HPow.hPow (α := ZMod 9) (β := ℕ) (↑a : ZMod 9) 3 + HPow.hPow (α := ZMod 9) (β := ℕ) (↑b : ZMod 9) 3 =
        HPow.hPow (α := ZMod 9) (β := ℕ) (↑c : ZMod 9) 3
⊢ ¬HPow.hPow (α := ZMod 9) (β := ℕ) (↑a : ZMod 9) 3 + HPow.hPow (α := ZMod 9) (β := ℕ) (↑b : ZMod 9) 3 =
      HPow.hPow (α := ZMod 9) (β := ℕ) (↑c : ZMod 9) 3

Tactic:
rcases cube_of_not_dvd hdvd.2 with hc | hc

Premises used: _private.0.cube_of_not_dvd, And.right
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : HPow.hPow (α := ZMod 9) (β := ℕ) (↑a : ZMod 9) 3 = 1
hb : HPow.hPow (α := ZMod 9) (β := ℕ) (↑b : ZMod 9) 3 = 1
hc : HPow.hPow (α := ZMod 9) (β := ℕ) (↑c : ZMod 9) 3 = 1
inl : ¬HAdd.hAdd (α := ZMod 9) 1 1 = 1
⊢ ¬HPow.hPow (α := ZMod 9) (β := ℕ) (↑a : ZMod 9) 3 + HPow.hPow (α := ZMod 9) (β := ℕ) (↑b : ZMod 9) 3 =
      HPow.hPow (α := ZMod 9) (β := ℕ) (↑c : ZMod 9) 3

Tactic:
rw [ha, hb, hc]
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : HPow.hPow (α := ZMod 9) (β := ℕ) (↑a : ZMod 9) 3 = 1
hb : HPow.hPow (α := ZMod 9) (β := ℕ) (↑b : ZMod 9) 3 = 1
hc : HPow.hPow (α := ZMod 9) (β := ℕ) (↑c : ZMod 9) 3 = 8
inl : ¬HAdd.hAdd (α := ZMod 9) 1 1 = 8
⊢ ¬HPow.hPow (α := ZMod 9) (β := ℕ) (↑a : ZMod 9) 3 + HPow.hPow (α := ZMod 9) (β := ℕ) (↑b : ZMod 9) 3 =
      HPow.hPow (α := ZMod 9) (β := ℕ) (↑c : ZMod 9) 3

Tactic:
rw [ha, hb, hc]
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : HPow.hPow (α := ZMod 9) (β := ℕ) (↑a : ZMod 9) 3 = 1
hb : HPow.hPow (α := ZMod 9) (β := ℕ) (↑b : ZMod 9) 3 = 8
hc : HPow.hPow (α := ZMod 9) (β := ℕ) (↑c : ZMod 9) 3 = 1
inl : ¬HAdd.hAdd (α := ZMod 9) 1 8 = 1
⊢ ¬HPow.hPow (α := ZMod 9) (β := ℕ) (↑a : ZMod 9) 3 + HPow.hPow (α := ZMod 9) (β := ℕ) (↑b : ZMod 9) 3 =
      HPow.hPow (α := ZMod 9) (β := ℕ) (↑c : ZMod 9) 3

Tactic:
rw [ha, hb, hc]
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : HPow.hPow (α := ZMod 9) (β := ℕ) (↑a : ZMod 9) 3 = 1
hb : HPow.hPow (α := ZMod 9) (β := ℕ) (↑b : ZMod 9) 3 = 8
hc : HPow.hPow (α := ZMod 9) (β := ℕ) (↑c : ZMod 9) 3 = 8
inl : ¬HAdd.hAdd (α := ZMod 9) 1 8 = 8
⊢ ¬HPow.hPow (α := ZMod 9) (β := ℕ) (↑a : ZMod 9) 3 + HPow.hPow (α := ZMod 9) (β := ℕ) (↑b : ZMod 9) 3 =
      HPow.hPow (α := ZMod 9) (β := ℕ) (↑c : ZMod 9) 3

Tactic:
rw [ha, hb, hc]
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : HPow.hPow (α := ZMod 9) (β := ℕ) (↑a : ZMod 9) 3 = 8
hb : HPow.hPow (α := ZMod 9) (β := ℕ) (↑b : ZMod 9) 3 = 1
hc : HPow.hPow (α := ZMod 9) (β := ℕ) (↑c : ZMod 9) 3 = 1
inr : ¬HAdd.hAdd (α := ZMod 9) 8 1 = 1
⊢ ¬HPow.hPow (α := ZMod 9) (β := ℕ) (↑a : ZMod 9) 3 + HPow.hPow (α := ZMod 9) (β := ℕ) (↑b : ZMod 9) 3 =
      HPow.hPow (α := ZMod 9) (β := ℕ) (↑c : ZMod 9) 3

Tactic:
rw [ha, hb, hc]
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : HPow.hPow (α := ZMod 9) (β := ℕ) (↑a : ZMod 9) 3 = 8
hb : HPow.hPow (α := ZMod 9) (β := ℕ) (↑b : ZMod 9) 3 = 1
hc : HPow.hPow (α := ZMod 9) (β := ℕ) (↑c : ZMod 9) 3 = 8
inr : ¬HAdd.hAdd (α := ZMod 9) 8 1 = 8
⊢ ¬HPow.hPow (α := ZMod 9) (β := ℕ) (↑a : ZMod 9) 3 + HPow.hPow (α := ZMod 9) (β := ℕ) (↑b : ZMod 9) 3 =
      HPow.hPow (α := ZMod 9) (β := ℕ) (↑c : ZMod 9) 3

Tactic:
rw [ha, hb, hc]
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : HPow.hPow (α := ZMod 9) (β := ℕ) (↑a : ZMod 9) 3 = 8
hb : HPow.hPow (α := ZMod 9) (β := ℕ) (↑b : ZMod 9) 3 = 8
hc : HPow.hPow (α := ZMod 9) (β := ℕ) (↑c : ZMod 9) 3 = 1
inr : ¬HAdd.hAdd (α := ZMod 9) 8 8 = 1
⊢ ¬HPow.hPow (α := ZMod 9) (β := ℕ) (↑a : ZMod 9) 3 + HPow.hPow (α := ZMod 9) (β := ℕ) (↑b : ZMod 9) 3 =
      HPow.hPow (α := ZMod 9) (β := ℕ) (↑c : ZMod 9) 3

Tactic:
rw [ha, hb, hc]
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : HPow.hPow (α := ZMod 9) (β := ℕ) (↑a : ZMod 9) 3 = 8
hb : HPow.hPow (α := ZMod 9) (β := ℕ) (↑b : ZMod 9) 3 = 8
hc : HPow.hPow (α := ZMod 9) (β := ℕ) (↑c : ZMod 9) 3 = 8
inr : ¬HAdd.hAdd (α := ZMod 9) 8 8 = 8
⊢ ¬HPow.hPow (α := ZMod 9) (β := ℕ) (↑a : ZMod 9) 3 + HPow.hPow (α := ZMod 9) (β := ℕ) (↑b : ZMod 9) 3 =
      HPow.hPow (α := ZMod 9) (β := ℕ) (↑c : ZMod 9) 3

Tactic:
rw [ha, hb, hc]
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : HPow.hPow (α := ZMod 9) (β := ℕ) (↑a : ZMod 9) 3 = 1
hb : HPow.hPow (α := ZMod 9) (β := ℕ) (↑b : ZMod 9) 3 = 1
hc : HPow.hPow (α := ZMod 9) (β := ℕ) (↑c : ZMod 9) 3 = 1
⊢ ¬HAdd.hAdd (α := ZMod 9) 1 1 = 1

Tactic:
decide
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : HPow.hPow (α := ZMod 9) (β := ℕ) (↑a : ZMod 9) 3 = 1
hb : HPow.hPow (α := ZMod 9) (β := ℕ) (↑b : ZMod 9) 3 = 1
hc : HPow.hPow (α := ZMod 9) (β := ℕ) (↑c : ZMod 9) 3 = 8
⊢ ¬HAdd.hAdd (α := ZMod 9) 1 1 = 8

Tactic:
decide
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : HPow.hPow (α := ZMod 9) (β := ℕ) (↑a : ZMod 9) 3 = 1
hb : HPow.hPow (α := ZMod 9) (β := ℕ) (↑b : ZMod 9) 3 = 8
hc : HPow.hPow (α := ZMod 9) (β := ℕ) (↑c : ZMod 9) 3 = 1
⊢ ¬HAdd.hAdd (α := ZMod 9) 1 8 = 1

Tactic:
decide
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : HPow.hPow (α := ZMod 9) (β := ℕ) (↑a : ZMod 9) 3 = 1
hb : HPow.hPow (α := ZMod 9) (β := ℕ) (↑b : ZMod 9) 3 = 8
hc : HPow.hPow (α := ZMod 9) (β := ℕ) (↑c : ZMod 9) 3 = 8
⊢ ¬HAdd.hAdd (α := ZMod 9) 1 8 = 8

Tactic:
decide
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : HPow.hPow (α := ZMod 9) (β := ℕ) (↑a : ZMod 9) 3 = 8
hb : HPow.hPow (α := ZMod 9) (β := ℕ) (↑b : ZMod 9) 3 = 1
hc : HPow.hPow (α := ZMod 9) (β := ℕ) (↑c : ZMod 9) 3 = 1
⊢ ¬HAdd.hAdd (α := ZMod 9) 8 1 = 1

Tactic:
decide
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : HPow.hPow (α := ZMod 9) (β := ℕ) (↑a : ZMod 9) 3 = 8
hb : HPow.hPow (α := ZMod 9) (β := ℕ) (↑b : ZMod 9) 3 = 1
hc : HPow.hPow (α := ZMod 9) (β := ℕ) (↑c : ZMod 9) 3 = 8
⊢ ¬HAdd.hAdd (α := ZMod 9) 8 1 = 8

Tactic:
decide
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : HPow.hPow (α := ZMod 9) (β := ℕ) (↑a : ZMod 9) 3 = 8
hb : HPow.hPow (α := ZMod 9) (β := ℕ) (↑b : ZMod 9) 3 = 8
hc : HPow.hPow (α := ZMod 9) (β := ℕ) (↑c : ZMod 9) 3 = 1
⊢ ¬HAdd.hAdd (α := ZMod 9) 8 8 = 1

Tactic:
decide
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : HPow.hPow (α := ZMod 9) (β := ℕ) (↑a : ZMod 9) 3 = 8
hb : HPow.hPow (α := ZMod 9) (β := ℕ) (↑b : ZMod 9) 3 = 8
hc : HPow.hPow (α := ZMod 9) (β := ℕ) (↑c : ZMod 9) 3 = 8
⊢ ¬HAdd.hAdd (α := ZMod 9) 8 8 = 8

Tactic:
decide
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
a b c : ℤ
ha : a ≠ 0
Hgcd : Eq (α := ℤ) (Finset.gcd {a, b, c} id) 1
h3a : 3 ∣ a
HF : HPow.hPow (β := ℕ) a 3 + HPow.hPow (β := ℕ) b 3 + HPow.hPow (β := ℕ) c 3 = 0
H :
  ∀ (a b c : ℤ),
    c ≠ 0 →
      ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → HPow.hPow (β := ℕ) a 3 + HPow.hPow (β := ℕ) b 3 ≠ HPow.hPow (β := ℕ) c 3
⊢ IsCoprime (-b) (-c)

Tactic:
IsCoprime.neg_neg ?_

Premises used: IsCoprime.neg_neg
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
a b c : ℤ
ha : a ≠ 0
Hgcd : Eq (α := ℤ) (Finset.gcd {a, b, c} id) 1
h3a : 3 ∣ a
HF : HPow.hPow (β := ℕ) a 3 + HPow.hPow (β := ℕ) b 3 + HPow.hPow (β := ℕ) c 3 = 0
H :
  ∀ (a b c : ℤ),
    c ≠ 0 →
      ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → HPow.hPow (β := ℕ) a 3 + HPow.hPow (β := ℕ) b 3 ≠ HPow.hPow (β := ℕ) c 3
refine : IsCoprime b c
⊢ IsCoprime (-b) (-c)

Tactic:
refine IsCoprime.neg_neg ?_

Premises used: IsCoprime.neg_neg
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
a b c : ℤ
ha : a ≠ 0
Hgcd : Eq (α := ℤ) (Finset.gcd {a, b, c} id) 1
h3a : 3 ∣ a
HF : HPow.hPow (β := ℕ) a 3 + HPow.hPow (β := ℕ) b 3 + HPow.hPow (β := ℕ) c 3 = 0
H :
  ∀ (a b c : ℤ),
    c ≠ 0 →
      ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → HPow.hPow (β := ℕ) a 3 + HPow.hPow (β := ℕ) b 3 ≠ HPow.hPow (β := ℕ) c 3
⊢ HPow.hPow (β := ℕ) b 3 + HPow.hPow (β := ℕ) c 3 + HPow.hPow (β := ℕ) a 3 = 0

Tactic:
rw [add_comm (a ^ 3), add_assoc, add_comm (a ^ 3), ← add_assoc] at HF

Premises used: add_assoc, add_comm, HPow.hPow, OfNat.ofNat
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
a b c : ℤ
ha : a ≠ 0
Hgcd : Eq (α := ℤ) (Finset.gcd {a, b, c} id) 1
h3a : 3 ∣ a
HF : HPow.hPow (β := ℕ) a 3 + HPow.hPow (β := ℕ) b 3 + HPow.hPow (β := ℕ) c 3 = 0
H :
  ∀ (a b c : ℤ),
    c ≠ 0 →
      ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → HPow.hPow (β := ℕ) a 3 + HPow.hPow (β := ℕ) b 3 ≠ HPow.hPow (β := ℕ) c 3
HF₁ : HPow.hPow (β := ℕ) b 3 + HPow.hPow (β := ℕ) c 3 + HPow.hPow (β := ℕ) a 3 = 0
⊢ ∀ (a b c : ℤ),
    c ≠ 0 →
      ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → HPow.hPow (β := ℕ) a 3 + HPow.hPow (β := ℕ) b 3 ≠ HPow.hPow (β := ℕ) c 3

Tactic:
rw [add_comm (a ^ 3), add_assoc, add_comm (a ^ 3), ← add_assoc] at HF

Premises used: add_assoc, add_comm, HPow.hPow, OfNat.ofNat
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
a b c : ℤ
ha : a ≠ 0
Hgcd : Eq (α := ℤ) (Finset.gcd {a, b, c} id) 1
h3a : 3 ∣ a
HF : HPow.hPow (β := ℕ) b 3 + HPow.hPow (β := ℕ) c 3 + HPow.hPow (β := ℕ) a 3 = 0
H :
  ∀ (a b c : ℤ),
    c ≠ 0 →
      ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → HPow.hPow (β := ℕ) a 3 + HPow.hPow (β := ℕ) b 3 ≠ HPow.hPow (β := ℕ) c 3
⊢ IsCoprime b c

Tactic:
isCoprime_of_gcd_eq_one_of_FLT ?_ HF

Premises used: isCoprime_of_gcd_eq_one_of_FLT
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
a b c : ℤ
ha : a ≠ 0
Hgcd : Eq (α := ℤ) (Finset.gcd {a, b, c} id) 1
h3a : 3 ∣ a
HF : HPow.hPow (β := ℕ) b 3 + HPow.hPow (β := ℕ) c 3 + HPow.hPow (β := ℕ) a 3 = 0
H :
  ∀ (a b c : ℤ),
    c ≠ 0 →
      ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → HPow.hPow (β := ℕ) a 3 + HPow.hPow (β := ℕ) b 3 ≠ HPow.hPow (β := ℕ) c 3
refine : Eq (α := ℤ) (Finset.gcd {b, c, a} id) 1
⊢ IsCoprime b c

Tactic:
refine isCoprime_of_gcd_eq_one_of_FLT ?_ HF

Premises used: isCoprime_of_gcd_eq_one_of_FLT
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
a b c : ℤ
ha : a ≠ 0
Hgcd : Eq (α := ℤ) (Finset.gcd {a, b, c} id) 1
h3a : 3 ∣ a
HF : HPow.hPow (β := ℕ) b 3 + HPow.hPow (β := ℕ) c 3 + HPow.hPow (β := ℕ) a 3 = 0
H :
  ∀ (a b c : ℤ),
    c ≠ 0 →
      ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → HPow.hPow (β := ℕ) a 3 + HPow.hPow (β := ℕ) b 3 ≠ HPow.hPow (β := ℕ) c 3
⊢ Eq (α := ℤ) (Finset.gcd {a, b, c} id) 1

Tactic:
Hgcd