awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
h : Eq (α := Finset ℤ) {b, c, a} {a, b, c}
⊢ Eq (α := ℤ) (Finset.gcd {b, c, a} id) 1

Tactic:
convert! Hgcd using 2
-- 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
h : Eq (α := Finset ℤ) {b, a, c} {a, b, c}
h₁ h₂ : Eq (α := Finset ℤ) {a, b, c} {a, b, c}
⊢ Eq (α := Finset ℤ) {b, c, a} {a, b, c}

Tactic:
rw [Finset.pair_comm, Finset.insert_comm]

Premises used: Finset.pair_comm, Finset.insert_comm
-- 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:
have hbc : IsCoprime (-b) (-c) := by
    refine IsCoprime.neg_neg ?_
    rw [add_comm (a ^ 3), add_assoc, add_comm (a ^ 3), ← add_assoc] at HF
    refine isCoprime_of_gcd_eq_one_of_FLT ?_ HF
    convert! Hgcd using 2
    rw [Finset.pair_comm, Finset.insert_comm]
-- 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
hbc : IsCoprime (-b) (-c)
by_contra! : ∀ (h3b : ¬3 ∣ b), False
⊢ 3 ∣ b

Tactic:
by_contra! h3b
-- 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
hbc : IsCoprime (-b) (-c)
h3b : ¬3 ∣ b
pos : ∀ (h3c : 3 ∣ c), False
neg : ∀ (h3c : ¬3 ∣ c), False
⊢ False

Tactic:
by_cases h3c : 3 ∣ c
-- 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
hbc : IsCoprime (-b) (-c)
h3b : ¬3 ∣ b
h3c : 3 ∣ c
pos : 3 ∣ b
⊢ False

Tactic:
apply h3b
-- 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
hbc : IsCoprime (-b) (-c)
h3b : ¬3 ∣ b
h3c : 3 ∣ c
⊢ HPow.hPow (β := ℕ) a 3 + HPow.hPow (β := ℕ) c 3 + HPow.hPow (β := ℕ) b 3 = 0

Tactic:
rw [add_assoc, add_comm (b ^ 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
hbc : IsCoprime (-b) (-c)
h3b : ¬3 ∣ b
h3c : 3 ∣ c
HF₁ : HPow.hPow (β := ℕ) a 3 + HPow.hPow (β := ℕ) c 3 + HPow.hPow (β := ℕ) b 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_assoc, add_comm (b ^ 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
hbc : IsCoprime (-b) (-c)
h3b : ¬3 ∣ b
h3c : 3 ∣ c
HF₁ : HPow.hPow (β := ℕ) a 3 + HPow.hPow (β := ℕ) c 3 + HPow.hPow (β := ℕ) b 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:
rw [add_assoc, add_comm (b ^ 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
hbc : IsCoprime (-b) (-c)
h3b : ¬3 ∣ b
h3c : 3 ∣ c
HF₁ : HPow.hPow (β := ℕ) a 3 + HPow.hPow (β := ℕ) c 3 + HPow.hPow (β := ℕ) b 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
hbc₁ : IsCoprime (-b) (-c)
⊢ ¬3 ∣ b

Tactic:
rw [add_assoc, add_comm (b ^ 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
hbc : IsCoprime (-b) (-c)
h3b : ¬3 ∣ b
h3c : 3 ∣ c
HF₁ : HPow.hPow (β := ℕ) a 3 + HPow.hPow (β := ℕ) c 3 + HPow.hPow (β := ℕ) b 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
hbc₁ : IsCoprime (-b) (-c)
h3b₁ : ¬3 ∣ b
⊢ 3 ∣ c

Tactic:
rw [add_assoc, add_comm (b ^ 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 (β := ℕ) c 3 + HPow.hPow (β := ℕ) b 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
hbc : IsCoprime (-b) (-c)
h3b : ¬3 ∣ b
h3c : 3 ∣ c
⊢ 3 ∣ b

Tactic:
dvd_c_of_prime_of_dvd_a_of_dvd_b_of_FLT Int.prime_three h3a h3c HF

Premises used: Int.prime_three, dvd_c_of_prime_of_dvd_a_of_dvd_b_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 (β := ℕ) a 3 + HPow.hPow (β := ℕ) c 3 + HPow.hPow (β := ℕ) b 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
hbc : IsCoprime (-b) (-c)
h3b : ¬3 ∣ b
h3c : 3 ∣ c
⊢ 3 ∣ b

Tactic:
exact dvd_c_of_prime_of_dvd_a_of_dvd_b_of_FLT Int.prime_three h3a h3c HF

Premises used: Int.prime_three, dvd_c_of_prime_of_dvd_a_of_dvd_b_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 (β := ℕ) 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
hbc : IsCoprime (-b) (-c)
h3b : ¬3 ∣ b
h3c : ¬3 ∣ c
⊢ ¬3 ∣ -b

Tactic:
simp [h3b]
-- 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
hbc : IsCoprime (-b) (-c)
h3b : ¬3 ∣ b
h3c : ¬3 ∣ c
⊢ ¬3 ∣ -c

Tactic:
simp [h3c]
-- 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
hbc : IsCoprime (-b) (-c)
h3b : ¬3 ∣ b
h3c : ¬3 ∣ c
neg : HPow.hPow (β := ℕ) (-b) 3 + HPow.hPow (β := ℕ) (-c) 3 = HPow.hPow (β := ℕ) a 3
⊢ False

Tactic:
refine H (-b) (-c) a ha (by simp [h3b]) (by simp [h3c]) h3a hbc ?_

Premises used: 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
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
hbc : IsCoprime (-b) (-c)
h3b : ¬3 ∣ b
h3c : ¬3 ∣ c
⊢ Odd (α := ℕ) 3

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
hbc : IsCoprime (-b) (-c)
h3b : ¬3 ∣ b
h3c : ¬3 ∣ c
⊢ HPow.hPow (β := ℕ) a 3 + HPow.hPow (β := ℕ) b 3 = HPow.hPow (β := ℕ) (-c) 3

Tactic:
rw [add_eq_zero_iff_eq_neg, ← (show Odd 3 by decide).neg_pow] at HF

Premises used: Odd.neg_pow, add_eq_zero_iff_eq_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
hbc : IsCoprime (-b) (-c)
h3b : ¬3 ∣ b
h3c : ¬3 ∣ c
HF₁ : HPow.hPow (β := ℕ) a 3 + HPow.hPow (β := ℕ) b 3 = HPow.hPow (β := ℕ) (-c) 3
⊢ ∀ (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_eq_zero_iff_eq_neg, ← (show Odd 3 by decide).neg_pow] at HF

Premises used: Odd.neg_pow, add_eq_zero_iff_eq_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
hbc : IsCoprime (-b) (-c)
h3b : ¬3 ∣ b
h3c : ¬3 ∣ c
HF₁ : HPow.hPow (β := ℕ) a 3 + HPow.hPow (β := ℕ) b 3 = HPow.hPow (β := ℕ) (-c) 3
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:
rw [add_eq_zero_iff_eq_neg, ← (show Odd 3 by decide).neg_pow] at HF

Premises used: Odd.neg_pow, add_eq_zero_iff_eq_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
hbc : IsCoprime (-b) (-c)
h3b : ¬3 ∣ b
h3c : ¬3 ∣ c
HF₁ : HPow.hPow (β := ℕ) a 3 + HPow.hPow (β := ℕ) b 3 = HPow.hPow (β := ℕ) (-c) 3
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
hbc₁ : IsCoprime (-b) (-c)
⊢ ¬3 ∣ b

Tactic:
rw [add_eq_zero_iff_eq_neg, ← (show Odd 3 by decide).neg_pow] at HF

Premises used: Odd.neg_pow, add_eq_zero_iff_eq_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
hbc : IsCoprime (-b) (-c)
h3b : ¬3 ∣ b
h3c : ¬3 ∣ c
HF₁ : HPow.hPow (β := ℕ) a 3 + HPow.hPow (β := ℕ) b 3 = HPow.hPow (β := ℕ) (-c) 3
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
hbc₁ : IsCoprime (-b) (-c)
h3b₁ : ¬3 ∣ b
⊢ ¬3 ∣ c

Tactic:
rw [add_eq_zero_iff_eq_neg, ← (show Odd 3 by decide).neg_pow] at HF

Premises used: Odd.neg_pow, add_eq_zero_iff_eq_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
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
hbc : IsCoprime (-b) (-c)
h3b : ¬3 ∣ b
h3c : ¬3 ∣ c
neg : HPow.hPow (β := ℕ) (-b) 3 + (HPow.hPow (β := ℕ) a 3 + HPow.hPow (β := ℕ) b 3) = HPow.hPow (β := ℕ) a 3
⊢ HPow.hPow (β := ℕ) (-b) 3 + HPow.hPow (β := ℕ) (-c) 3 = HPow.hPow (β := ℕ) a 3

Tactic:
rw [← HF]
-- 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
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
hbc : IsCoprime (-b) (-c)
h3b : ¬3 ∣ b
h3c : ¬3 ∣ c
⊢ HPow.hPow (β := ℕ) (-b) 3 + (HPow.hPow (β := ℕ) a 3 + HPow.hPow (β := ℕ) b 3) = HPow.hPow (β := ℕ) a 3

Tactic:
ring
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
a b c : ℤ
ha : a ≠ 0
h3a : 3 ∣ a
Hgcd : Eq (α := ℤ) (Finset.gcd {a, b, c} id) 1
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 (β := ℕ) a 3 + HPow.hPow (β := ℕ) b 3 + HPow.hPow (β := ℕ) c 3 = 0
⊢ ¬Dvd.dvd (α := ℤ) 3 1

Tactic:
decide
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
a b c : ℤ
ha : a ≠ 0
h3a : 3 ∣ a
Hgcd : Eq (α := ℤ) (Finset.gcd {a, b, c} id) 1
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 (β := ℕ) a 3 + HPow.hPow (β := ℕ) b 3 + HPow.hPow (β := ℕ) c 3 = 0
apply : Dvd.dvd (α := ℤ) 3 1
⊢ False

Tactic:
apply (show ¬(3 ∣ (1 : ℤ)) by decide)
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
a b c : ℤ
ha : a ≠ 0
h3a : 3 ∣ a
Hgcd : Eq (α := ℤ) (Finset.gcd {a, b, c} id) 1
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 (β := ℕ) a 3 + HPow.hPow (β := ℕ) b 3 + HPow.hPow (β := ℕ) c 3 = 0
rw : Dvd.dvd (α := ℤ) 3 (Finset.gcd {a, b, c} id)
⊢ Dvd.dvd (α := ℤ) 3 1

Tactic:
rw [← Hgcd]
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
a b c : ℤ
ha : a ≠ 0
h3a : 3 ∣ a
Hgcd : Eq (α := ℤ) (Finset.gcd {a, b, c} id) 1
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 (β := ℕ) a 3 + HPow.hPow (β := ℕ) b 3 + HPow.hPow (β := ℕ) c 3 = 0
⊢ Dvd.dvd (α := ℤ) 3 (Finset.gcd {a, b, c} id)

Tactic:
dvd_gcd (fun x hx ↦ ?_)

Premises used: Finset.dvd_gcd
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
a b c : ℤ
ha : a ≠ 0
h3a : 3 ∣ a
Hgcd : Eq (α := ℤ) (Finset.gcd {a, b, c} id) 1
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 (β := ℕ) a 3 + HPow.hPow (β := ℕ) b 3 + HPow.hPow (β := ℕ) c 3 = 0
refine : ∀ (x : ℤ) (hx : Membership.mem (γ := Finset ℤ) {a, b, c} x), 3 ∣ id x
⊢ Dvd.dvd (α := ℤ) 3 (Finset.gcd {a, b, c} id)

Tactic:
refine dvd_gcd (fun x hx ↦ ?_)

Premises used: Finset.dvd_gcd
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
a b c : ℤ
ha : a ≠ 0
h3a : 3 ∣ a
Hgcd : Eq (α := ℤ) (Finset.gcd {a, b, c} id) 1
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 (β := ℕ) a 3 + HPow.hPow (β := ℕ) b 3 + HPow.hPow (β := ℕ) c 3 = 0
x : ℤ
hx : Membership.mem (γ := Finset ℤ) {a, b, c} x
⊢ x = a ∨ x = b ∨ x = c

Tactic:
simp only [mem_insert, mem_singleton] at hx

Premises used: Finset.mem_singleton, Finset.mem_insert
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
a b c : ℤ
ha : a ≠ 0
h3a : 3 ∣ a
Hgcd : Eq (α := ℤ) (Finset.gcd {a, b, c} id) 1
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 (β := ℕ) a 3 + HPow.hPow (β := ℕ) b 3 + HPow.hPow (β := ℕ) c 3 = 0
x : ℤ
hx : x = a ∨ x = b ∨ x = c
⊢ 3 ∣ b

Tactic:
three_dvd_b_of_dvd_a_of_gcd_eq_one_of_case2 ha ?_ h3a HF H

Premises used: _private.0.three_dvd_b_of_dvd_a_of_gcd_eq_one_of_case2
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
a b c : ℤ
ha : a ≠ 0
h3a : 3 ∣ a
Hgcd : Eq (α := ℤ) (Finset.gcd {a, b, c} id) 1
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 (β := ℕ) a 3 + HPow.hPow (β := ℕ) b 3 + HPow.hPow (β := ℕ) c 3 = 0
x : ℤ
hx : x = a ∨ x = b ∨ x = c
refine : Eq (α := ℤ) (Finset.gcd {a, b, c} id) 1
⊢ 3 ∣ b

Tactic:
refine three_dvd_b_of_dvd_a_of_gcd_eq_one_of_case2 ha ?_ h3a HF H

Premises used: _private.0.three_dvd_b_of_dvd_a_of_gcd_eq_one_of_case2
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
a b c : ℤ
ha : a ≠ 0
h3a : 3 ∣ a
Hgcd : Eq (α := ℤ) (Finset.gcd {a, b, c} id) 1
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 (β := ℕ) a 3 + HPow.hPow (β := ℕ) b 3 + HPow.hPow (β := ℕ) c 3 = 0
x : ℤ
hx : x = a ∨ x = b ∨ x = c
⊢ Eq (α := ℤ) (Finset.gcd {a, b, c} id) 1

Tactic:
simp only [← Hgcd, gcd_insert, gcd_singleton, id_eq, ← Int.abs_eq_normalize]

Premises used: Finset.gcd_singleton, Finset.gcd_insert, Int.abs_eq_normalize, id_eq
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
a b c : ℤ
ha : a ≠ 0
h3a : 3 ∣ a
Hgcd : Eq (α := ℤ) (Finset.gcd {a, b, c} id) 1
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 (β := ℕ) a 3 + HPow.hPow (β := ℕ) b 3 + HPow.hPow (β := ℕ) c 3 = 0
x : ℤ
hx : x = a ∨ x = b ∨ x = c
⊢ 3 ∣ b

Tactic:
have h3b : 3 ∣ b := by
    refine three_dvd_b_of_dvd_a_of_gcd_eq_one_of_case2 ha ?_ h3a HF H
    simp only [← Hgcd, gcd_insert, gcd_singleton, id_eq, ← Int.abs_eq_normalize]
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
a b c : ℤ
ha : a ≠ 0
h3a : 3 ∣ a
Hgcd : Eq (α := ℤ) (Finset.gcd {a, b, c} id) 1
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 (β := ℕ) a 3 + HPow.hPow (β := ℕ) b 3 + HPow.hPow (β := ℕ) c 3 = 0
x : ℤ
hx : x = a ∨ x = b ∨ x = c
h3b : 3 ∣ b
inl : ∀ (hx : x = a), 3 ∣ id x
inr : ∀ (hx : x = b), 3 ∣ id x
inr₁ : ∀ (hx : x = c), 3 ∣ id x
⊢ 3 ∣ id x

Tactic:
rcases hx with hx | hx | hx
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
a b c : ℤ
ha : a ≠ 0
h3a : 3 ∣ a
Hgcd : Eq (α := ℤ) (Finset.gcd {a, b, c} id) 1
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 (β := ℕ) a 3 + HPow.hPow (β := ℕ) b 3 + HPow.hPow (β := ℕ) c 3 = 0
x : ℤ
h3b : 3 ∣ b
hx : x = a
⊢ 3 ∣ id x

Tactic:
hx ▸ h3a

Premises used: Eq.rec, Eq.symm
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
a b c : ℤ
ha : a ≠ 0
h3a : 3 ∣ a
Hgcd : Eq (α := ℤ) (Finset.gcd {a, b, c} id) 1
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 (β := ℕ) a 3 + HPow.hPow (β := ℕ) b 3 + HPow.hPow (β := ℕ) c 3 = 0
x : ℤ
h3b : 3 ∣ b
hx : x = a
⊢ 3 ∣ id x

Tactic:
exact hx ▸ h3a
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
a b c : ℤ
ha : a ≠ 0
h3a : 3 ∣ a
Hgcd : Eq (α := ℤ) (Finset.gcd {a, b, c} id) 1
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 (β := ℕ) a 3 + HPow.hPow (β := ℕ) b 3 + HPow.hPow (β := ℕ) c 3 = 0
x : ℤ
h3b : 3 ∣ b
hx : x = b
⊢ 3 ∣ id x

Tactic:
hx ▸ h3b

Premises used: Eq.rec, Eq.symm
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
a b c : ℤ
ha : a ≠ 0
h3a : 3 ∣ a
Hgcd : Eq (α := ℤ) (Finset.gcd {a, b, c} id) 1
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 (β := ℕ) a 3 + HPow.hPow (β := ℕ) b 3 + HPow.hPow (β := ℕ) c 3 = 0
x : ℤ
h3b : 3 ∣ b
hx : x = b
⊢ 3 ∣ id x

Tactic:
exact hx ▸ h3b
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
a b c : ℤ
ha : a ≠ 0
h3a : 3 ∣ a
Hgcd : Eq (α := ℤ) (Finset.gcd {a, b, c} id) 1
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 (β := ℕ) a 3 + HPow.hPow (β := ℕ) b 3 + HPow.hPow (β := ℕ) c 3 = 0
x : ℤ
h3b : 3 ∣ b
hx : x = c
⊢ 3 ∣ id x

Tactic:
simpa [hx] using dvd_c_of_prime_of_dvd_a_of_dvd_b_of_FLT Int.prime_three h3a h3b HF

Premises used: Int.prime_three, dvd_c_of_prime_of_dvd_a_of_dvd_b_of_FLT
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
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
rw : FermatLastTheoremWith ℤ 3
⊢ FermatLastTheoremFor 3

Tactic:
rw [fermatLastTheoremFor_iff_int]

Premises used: fermatLastTheoremFor_iff_int
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
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
⊢ FermatLastTheoremWith ℤ 3

Tactic:
fermatLastTheoremWith_of_fermatLastTheoremWith_coprime (fun a b c ha hb hc Hgcd hF ↦ ?_)

Premises used: fermatLastTheoremWith_of_fermatLastTheoremWith_coprime