awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
R : Type u_2
inst : CommSemiring R
inst_1 : IsDomain R
inst_2 : DecidableEq R
inst_3 : NormalizedGCDMonoid R
hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → Eq (α := R) (Finset.gcd {a, b, c} id) 1 → a ^ n + b ^ n ≠ c ^ n
a b c : R
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
s : Finset R := {a, b, c}
d : R := s.gcd id
A : R
hA : a = d * A
B : R
hB : b = d * B
⊢ c ∈ s

Tactic:
simp [s]
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
R : Type u_2
inst : CommSemiring R
inst_1 : IsDomain R
inst_2 : DecidableEq R
inst_3 : NormalizedGCDMonoid R
hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → Eq (α := R) (Finset.gcd {a, b, c} id) 1 → a ^ n + b ^ n ≠ c ^ n
a b c : R
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
s : Finset R := {a, b, c}
d : R := s.gcd id
A : R
hA : a = d * A
B : R
hB : b = d * B
obtain : ∀ (C : R) (hC : c = d * C), False
⊢ False

Tactic:
obtain ⟨C, hC⟩ : d ∣ c := gcd_dvd (by simp [s])

Premises used: Finset.gcd_dvd
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
R : Type u_2
inst : CommSemiring R
inst_1 : IsDomain R
inst_2 : DecidableEq R
inst_3 : NormalizedGCDMonoid R
hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → Eq (α := R) (Finset.gcd {a, b, c} id) 1 → a ^ n + b ^ n ≠ c ^ n
a b c : R
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
s : Finset R := {a, b, c}
d : R := s.gcd id
A : R
hA : a = d * A
B : R
hB : b = d * B
C : R
hC : c = d * C
⊢ d ≠ 0 ∧ A ≠ 0

Tactic:
simp only [hA, hB, hC, mul_ne_zero_iff, mul_pow] at ha hb hc habc

Premises used: mul_pow, mul_ne_zero_iff
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
R : Type u_2
inst : CommSemiring R
inst_1 : IsDomain R
inst_2 : DecidableEq R
inst_3 : NormalizedGCDMonoid R
hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → Eq (α := R) (Finset.gcd {a, b, c} id) 1 → a ^ n + b ^ n ≠ c ^ n
a b c : R
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
s : Finset R := {a, b, c}
d : R := s.gcd id
A : R
hA : a = d * A
B : R
hB : b = d * B
C : R
hC : c = d * C
ha₁ : d ≠ 0 ∧ A ≠ 0
⊢ d ≠ 0 ∧ B ≠ 0

Tactic:
simp only [hA, hB, hC, mul_ne_zero_iff, mul_pow] at ha hb hc habc

Premises used: mul_pow, mul_ne_zero_iff
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
R : Type u_2
inst : CommSemiring R
inst_1 : IsDomain R
inst_2 : DecidableEq R
inst_3 : NormalizedGCDMonoid R
hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → Eq (α := R) (Finset.gcd {a, b, c} id) 1 → a ^ n + b ^ n ≠ c ^ n
a b c : R
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
s : Finset R := {a, b, c}
d : R := s.gcd id
A : R
hA : a = d * A
B : R
hB : b = d * B
C : R
hC : c = d * C
ha₁ : d ≠ 0 ∧ A ≠ 0
hb₁ : d ≠ 0 ∧ B ≠ 0
⊢ d ≠ 0 ∧ C ≠ 0

Tactic:
simp only [hA, hB, hC, mul_ne_zero_iff, mul_pow] at ha hb hc habc

Premises used: mul_pow, mul_ne_zero_iff
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
R : Type u_2
inst : CommSemiring R
inst_1 : IsDomain R
inst_2 : DecidableEq R
inst_3 : NormalizedGCDMonoid R
hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → Eq (α := R) (Finset.gcd {a, b, c} id) 1 → a ^ n + b ^ n ≠ c ^ n
a b c : R
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
s : Finset R := {a, b, c}
d : R := s.gcd id
A : R
hA : a = d * A
B : R
hB : b = d * B
C : R
hC : c = d * C
ha₁ : d ≠ 0 ∧ A ≠ 0
hb₁ : d ≠ 0 ∧ B ≠ 0
hc₁ : d ≠ 0 ∧ C ≠ 0
⊢ d ^ n * A ^ n + d ^ n * B ^ n = d ^ n * C ^ n

Tactic:
simp only [hA, hB, hC, mul_ne_zero_iff, mul_pow] at ha hb hc habc

Premises used: mul_pow, mul_ne_zero_iff
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
R : Type u_2
inst : CommSemiring R
inst_1 : IsDomain R
inst_2 : DecidableEq R
inst_3 : NormalizedGCDMonoid R
hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → Eq (α := R) (Finset.gcd {a, b, c} id) 1 → a ^ n + b ^ n ≠ c ^ n
a b c : R
s : Finset R := {a, b, c}
d : R := s.gcd id
A : R
hA : a = d * A
B : R
hB : b = d * B
C : R
hC : c = d * C
ha : d ≠ 0 ∧ A ≠ 0
hb : d ≠ 0 ∧ B ≠ 0
hc : d ≠ 0 ∧ C ≠ 0
habc : d ^ n * A ^ n + d ^ n * B ^ n = d ^ n * C ^ n
⊢ A ^ n + B ^ n = C ^ n

Tactic:
rw [← mul_add, mul_right_inj' (pow_ne_zero n ha.1)] at habc

Premises used: pow_ne_zero, And.left, mul_add, mul_right_inj'
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
R : Type u_2
inst : CommSemiring R
inst_1 : IsDomain R
inst_2 : DecidableEq R
inst_3 : NormalizedGCDMonoid R
hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → Eq (α := R) (Finset.gcd {a, b, c} id) 1 → a ^ n + b ^ n ≠ c ^ n
a b c : R
s : Finset R := {a, b, c}
d : R := s.gcd id
A : R
hA : a = d * A
B : R
hB : b = d * B
C : R
hC : c = d * C
ha : d ≠ 0 ∧ A ≠ 0
hb : d ≠ 0 ∧ B ≠ 0
hc : d ≠ 0 ∧ C ≠ 0
habc : A ^ n + B ^ n = C ^ n
⊢ False

Tactic:
hn A B C ha.2 hb.2 hc.2 ?_ habc

Premises used: And.right
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
R : Type u_2
inst : CommSemiring R
inst_1 : IsDomain R
inst_2 : DecidableEq R
inst_3 : NormalizedGCDMonoid R
hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → Eq (α := R) (Finset.gcd {a, b, c} id) 1 → a ^ n + b ^ n ≠ c ^ n
a b c : R
s : Finset R := {a, b, c}
d : R := s.gcd id
A : R
hA : a = d * A
B : R
hB : b = d * B
C : R
hC : c = d * C
ha : d ≠ 0 ∧ A ≠ 0
hb : d ≠ 0 ∧ B ≠ 0
hc : d ≠ 0 ∧ C ≠ 0
habc : A ^ n + B ^ n = C ^ n
refine : Eq (α := R) (Finset.gcd {A, B, C} id) 1
⊢ False

Tactic:
refine hn A B C ha.2 hb.2 hc.2 ?_ habc

Premises used: And.right
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
R : Type u_2
inst : CommSemiring R
inst_1 : IsDomain R
inst_2 : DecidableEq R
inst_3 : NormalizedGCDMonoid R
hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → Eq (α := R) (Finset.gcd {a, b, c} id) 1 → a ^ n + b ^ n ≠ c ^ n
a b c : R
s : Finset R := {a, b, c}
d : R := s.gcd id
A : R
hA : a = d * A
B : R
hB : b = d * B
C : R
hC : c = d * C
ha : d ≠ 0 ∧ A ≠ 0
hb : d ≠ 0 ∧ B ≠ 0
hc : d ≠ 0 ∧ C ≠ 0
habc : A ^ n + B ^ n = C ^ n
rw : IsUnit (M := R) (Finset.gcd {A, B, C} id)
⊢ Eq (α := R) (Finset.gcd {A, B, C} id) 1

Tactic:
rw [← Finset.normalize_gcd, normalize_eq_one]

Premises used: normalize_eq_one, Finset.normalize_gcd
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
R : Type u_2
inst : CommSemiring R
inst_1 : IsDomain R
inst_2 : DecidableEq R
inst_3 : NormalizedGCDMonoid R
hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → Eq (α := R) (Finset.gcd {a, b, c} id) 1 → a ^ n + b ^ n ≠ c ^ n
a b c : R
s : Finset R := {a, b, c}
d : R := s.gcd id
A : R
hA : a = d * A
B : R
hB : b = d * B
C : R
hC : c = d * C
ha : d ≠ 0 ∧ A ≠ 0
hb : d ≠ 0 ∧ B ≠ 0
hc : d ≠ 0 ∧ C ≠ 0
habc : A ^ n + B ^ n = C ^ n
obtain :
  ∀ (u : Rˣ) (hu : HMul.hMul (α := R) ((normalize : (a : R) → R) d : R) (↑u : R) = d),
    IsUnit (M := R) (Finset.gcd {A, B, C} id)
⊢ IsUnit (M := R) (Finset.gcd {A, B, C} id)

Tactic:
obtain ⟨u, hu⟩ := normalize_associated d

Premises used: normalize_associated
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
R : Type u_2
inst : CommSemiring R
inst_1 : IsDomain R
inst_2 : DecidableEq R
inst_3 : NormalizedGCDMonoid R
hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → Eq (α := R) (Finset.gcd {a, b, c} id) 1 → a ^ n + b ^ n ≠ c ^ n
a b c : R
s : Finset R := {a, b, c}
d : R := s.gcd id
A : R
hA : a = d * A
B : R
hB : b = d * B
C : R
hC : c = d * C
ha : d ≠ 0 ∧ A ≠ 0
hb : d ≠ 0 ∧ B ≠ 0
hc : d ≠ 0 ∧ C ≠ 0
habc : A ^ n + B ^ n = C ^ n
u : Rˣ
hu : HMul.hMul (α := R) ((normalize : (a : R) → R) d : R) (↑u : R) = d
⊢ IsUnit (M := R) (Finset.gcd {A, B, C} id)

Tactic:
⟨u, mul_left_cancel₀ (mt normalize_eq_zero.mp ha.1) (hu.symm ▸ ?_)⟩

Premises used: IsUnit, mt, normalize_eq_zero, mul_left_cancel₀, And.left, Exists.intro, Iff.mp
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
R : Type u_2
inst : CommSemiring R
inst_1 : IsDomain R
inst_2 : DecidableEq R
inst_3 : NormalizedGCDMonoid R
hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → Eq (α := R) (Finset.gcd {a, b, c} id) 1 → a ^ n + b ^ n ≠ c ^ n
a b c : R
s : Finset R := {a, b, c}
d : R := s.gcd id
A : R
hA : a = d * A
B : R
hB : b = d * B
C : R
hC : c = d * C
ha : d ≠ 0 ∧ A ≠ 0
hb : d ≠ 0 ∧ B ≠ 0
hc : d ≠ 0 ∧ C ≠ 0
habc : A ^ n + B ^ n = C ^ n
u : Rˣ
hu : HMul.hMul (α := R) ((normalize : (a : R) → R) d : R) (↑u : R) = d
refine : d = HMul.hMul (α := R) (β := R) ((normalize : (a : R) → R) d : R) (Finset.gcd {A, B, C} id : R)
⊢ IsUnit (M := R) (Finset.gcd {A, B, C} id)

Tactic:
refine ⟨u, mul_left_cancel₀ (mt normalize_eq_zero.mp ha.1) (hu.symm ▸ ?_)⟩
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
R : Type u_2
inst : CommSemiring R
inst_1 : IsDomain R
inst_2 : DecidableEq R
inst_3 : NormalizedGCDMonoid R
hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → Eq (α := R) (Finset.gcd {a, b, c} id) 1 → a ^ n + b ^ n ≠ c ^ n
a b c : R
s : Finset R := {a, b, c}
d : R := s.gcd id
A : R
hA : a = d * A
B : R
hB : b = d * B
C : R
hC : c = d * C
ha : d ≠ 0 ∧ A ≠ 0
hb : d ≠ 0 ∧ B ≠ 0
hc : d ≠ 0 ∧ C ≠ 0
habc : A ^ n + B ^ n = C ^ n
u : Rˣ
hu : HMul.hMul (α := R) ((normalize : (a : R) → R) d : R) (↑u : R) = d
rw : d = Finset.gcd {A, B, C} fun (x : R) ↦ d * id x
rw₁ : d = Finset.gcd (image (fun (x : R) ↦ d * id x) {A, B, C}) id
rw₂ : d = Finset.gcd (insert (d * id A) (image (fun (x : R) ↦ d * id x) {B, C})) id
rw₃ : d = Finset.gcd (insert (d * id A) (insert (d * id B) (image (fun (x : R) ↦ d * id x) {C}))) id
rw₄ : d = Finset.gcd {d * id A, d * id B, d * id C} id
rw₅ : d = Finset.gcd {d * A, d * id B, d * id C} id
rw₆ : d = Finset.gcd {d * A, d * B, d * id C} id
rw₇ : d = Finset.gcd {d * A, d * B, d * C} id
rw₈ : d = Finset.gcd {a, d * B, d * C} id
rw₉ : d = Finset.gcd {a, b, d * C} id
rw₁₀ rw₁₁ : d = Finset.gcd {a, b, c} id
⊢ d = HMul.hMul (α := R) (β := R) ((normalize : (a : R) → R) d : R) (Finset.gcd {A, B, C} id : R)

Tactic:
rw [← Finset.gcd_mul_left, gcd_eq_gcd_image, image_insert, image_insert, image_singleton,
      id_eq, id_eq, id_eq, ← hA, ← hB, ← hC]

Premises used: Finset.gcd_mul_left, Finset.image_singleton, Finset.gcd_eq_gcd_image, Finset.image_insert, id_eq
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
p : ℤ
hp : Prime p
a b c : ℤ
hpa : p ∣ a
hpb : p ∣ b
HF : a ^ n + b ^ n + c ^ n = 0
inl : ∀ (HF : HPow.hPow (β := ℕ) a 0 + HPow.hPow (β := ℕ) b 0 + HPow.hPow (β := ℕ) c 0 = 0), p ∣ c
inr : ∀ (hn : n ≠ 0), p ∣ c
⊢ p ∣ c

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
p : ℤ
hp : Prime p
a b c : ℤ
hpa : p ∣ a
hpb : p ∣ b
HF : HPow.hPow (β := ℕ) a 0 + HPow.hPow (β := ℕ) b 0 + HPow.hPow (β := ℕ) c 0 = 0
⊢ p ∣ c

Tactic:
simp at HF
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
p : ℤ
hp : Prime p
a b c : ℤ
hpa : p ∣ a
hpb : p ∣ b
HF : a ^ n + b ^ n + c ^ n = 0
hn : n ≠ 0
⊢ p ∣ c

Tactic:
hp.dvd_of_dvd_pow (n := n) (dvd_neg.1 ?_)

Premises used: dvd_neg, Iff.mp, Prime.dvd_of_dvd_pow
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
p : ℤ
hp : Prime p
a b c : ℤ
hpa : p ∣ a
hpb : p ∣ b
HF : a ^ n + b ^ n + c ^ n = 0
hn : n ≠ 0
inr : p ∣ -c ^ n
⊢ p ∣ c

Tactic:
refine hp.dvd_of_dvd_pow (n := n) (dvd_neg.1 ?_)

Premises used: dvd_neg, Iff.mp, Prime.dvd_of_dvd_pow
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
p : ℤ
hp : Prime p
a b c : ℤ
hpa : p ∣ a
hpb : p ∣ b
HF : a ^ n + b ^ n + c ^ n = 0
hn : n ≠ 0
⊢ a ^ n + b ^ n = -c ^ n

Tactic:
rw [add_eq_zero_iff_eq_neg] at HF

Premises used: add_eq_zero_iff_eq_neg
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
p : ℤ
hp : Prime p
a b c : ℤ
hpa : p ∣ a
hpb : p ∣ b
HF : a ^ n + b ^ n + c ^ n = 0
hn : n ≠ 0
HF₁ : a ^ n + b ^ n = -c ^ n
⊢ n ≠ 0

Tactic:
rw [add_eq_zero_iff_eq_neg] at HF

Premises used: add_eq_zero_iff_eq_neg
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
p : ℤ
hp : Prime p
a b c : ℤ
hpa : p ∣ a
hpb : p ∣ b
HF : a ^ n + b ^ n = -c ^ n
hn : n ≠ 0
⊢ p ∣ -c ^ n

Tactic:
HF.symm ▸ dvd_add (dvd_pow hpa hn) (dvd_pow hpb hn)

Premises used: Eq.rec, dvd_pow, Eq.symm, dvd_add
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
p : ℤ
hp : Prime p
a b c : ℤ
hpa : p ∣ a
hpb : p ∣ b
HF : a ^ n + b ^ n = -c ^ n
hn : n ≠ 0
⊢ p ∣ -c ^ n

Tactic:
exact HF.symm ▸ dvd_add (dvd_pow hpa hn) (dvd_pow hpb hn)
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
a b c : ℤ
Hgcd : Eq (α := ℤ) (Finset.gcd {a, b, c} id) 1
HF : a ^ n + b ^ n + c ^ n = 0
inl : ∀ (HF : HPow.hPow (β := ℕ) a 0 + HPow.hPow (β := ℕ) b 0 + HPow.hPow (β := ℕ) c 0 = 0), IsCoprime a b
inr : ∀ (hn : n ≠ 0), IsCoprime a b
⊢ IsCoprime a b

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
a b c : ℤ
Hgcd : Eq (α := ℤ) (Finset.gcd {a, b, c} id) 1
HF : HPow.hPow (β := ℕ) a 0 + HPow.hPow (β := ℕ) b 0 + HPow.hPow (β := ℕ) c 0 = 0
⊢ IsCoprime a b

Tactic:
simp only [pow_zero, Int.reduceAdd, OfNat.ofNat_ne_zero] at HF

Premises used: Int.reduceAdd, OfNat.ofNat_ne_zero, pow_zero
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
a b c : ℤ
Hgcd : Eq (α := ℤ) (Finset.gcd {a, b, c} id) 1
HF : a ^ n + b ^ n + c ^ n = 0
hn : n ≠ 0
⊢ IsCoprime a b

Tactic:
isCoprime_of_prime_dvd ?_ <| (fun p hp hpa hpb ↦ hp.not_dvd_one ?_)

Premises used: Prime.not_dvd_one, isCoprime_of_prime_dvd
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
a b c : ℤ
Hgcd : Eq (α := ℤ) (Finset.gcd {a, b, c} id) 1
HF : a ^ n + b ^ n + c ^ n = 0
hn : n ≠ 0
inr : ¬(a = 0 ∧ b = 0)
inr₁ : ∀ (p : ℤ) (hp : Prime p) (hpa : p ∣ a) (hpb : p ∣ b), p ∣ 1
⊢ IsCoprime a b

Tactic:
refine isCoprime_of_prime_dvd ?_ <| (fun p hp hpa hpb ↦ hp.not_dvd_one ?_)

Premises used: isCoprime_of_prime_dvd
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
c : ℤ
hn : n ≠ 0
Hgcd : Eq (α := ℤ) (Finset.gcd {0, 0, c} id) 1
HF : HPow.hPow (α := ℤ) 0 n + HPow.hPow (α := ℤ) 0 n + c ^ n = 0
⊢ c = 0

Tactic:
simp only [ne_eq, hn, not_false_eq_true, zero_pow, add_zero, zero_add, pow_eq_zero_iff]
      at HF

Premises used: pow_eq_zero_iff, zero_add, ne_eq, add_zero, not_false_eq_true, zero_pow
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
c : ℤ
hn : n ≠ 0
Hgcd : Eq (α := ℤ) (Finset.gcd {0, 0, c} id) 1
HF : c = 0
⊢ False

Tactic:
simp only [HF, Finset.mem_singleton, Finset.insert_eq_of_mem, Finset.gcd_singleton, id_eq,
      map_zero, zero_ne_one] at Hgcd

Premises used: Finset.mem_singleton, map_zero, zero_ne_one, Finset.gcd_singleton, Finset.insert_eq_of_mem, id_eq
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
a b c : ℤ
Hgcd : Eq (α := ℤ) (Finset.gcd {a, b, c} id) 1
HF : a ^ n + b ^ n + c ^ n = 0
hn : n ≠ 0
p : ℤ
hp : Prime p
hpa : p ∣ a
hpb : p ∣ b
inr : p ∣ Finset.gcd {a, b, c} id
⊢ p ∣ 1

Tactic:
rw [← Hgcd]
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
a b c : ℤ
Hgcd : Eq (α := ℤ) (Finset.gcd {a, b, c} id) 1
HF : a ^ n + b ^ n + c ^ n = 0
hn : n ≠ 0
p : ℤ
hp : Prime p
hpa : p ∣ a
hpb : p ∣ b
⊢ p ∣ Finset.gcd {a, b, c} id

Tactic:
Finset.dvd_gcd_iff.mpr fun x hx ↦ ?_

Premises used: Iff.mpr, Finset.dvd_gcd_iff
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
a b c : ℤ
Hgcd : Eq (α := ℤ) (Finset.gcd {a, b, c} id) 1
HF : a ^ n + b ^ n + c ^ n = 0
hn : n ≠ 0
p : ℤ
hp : Prime p
hpa : p ∣ a
hpb : p ∣ b
inr : ∀ (x : ℤ) (hx : Membership.mem (γ := Finset ℤ) {a, b, c} x), p ∣ id x
⊢ p ∣ Finset.gcd {a, b, c} id

Tactic:
refine Finset.dvd_gcd_iff.mpr fun x hx ↦ ?_

Premises used: Iff.mpr, Finset.dvd_gcd_iff
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
a b c : ℤ
Hgcd : Eq (α := ℤ) (Finset.gcd {a, b, c} id) 1
HF : a ^ n + b ^ n + c ^ n = 0
hn : n ≠ 0
p : ℤ
hp : Prime p
hpa : p ∣ a
hpb : p ∣ b
x : ℤ
hx : Membership.mem (γ := Finset ℤ) {a, b, c} x
⊢ x = a ∨ x = b ∨ x = c

Tactic:
simp only [Finset.mem_insert, Finset.mem_singleton] at hx

Premises used: Finset.mem_singleton, Finset.mem_insert
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
a b c : ℤ
Hgcd : Eq (α := ℤ) (Finset.gcd {a, b, c} id) 1
HF : a ^ n + b ^ n + c ^ n = 0
hn : n ≠ 0
p : ℤ
hp : Prime p
hpa : p ∣ a
hpb : p ∣ b
x : ℤ
hx : x = a ∨ x = b ∨ x = c
inr : ∀ (hx : x = a), p ∣ id x
inr₁ : ∀ (hx : x = b), p ∣ id x
inr₂ : ∀ (hx : x = c), p ∣ id x
⊢ p ∣ id x

Tactic:
rcases hx with hx | hx | hx
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
a b c : ℤ
Hgcd : Eq (α := ℤ) (Finset.gcd {a, b, c} id) 1
HF : a ^ n + b ^ n + c ^ n = 0
hn : n ≠ 0
p : ℤ
hp : Prime p
hpa : p ∣ a
hpb : p ∣ b
x : ℤ
hx : x = a
⊢ p ∣ id x

Tactic:
simp only [id_eq, hx, hpa, hpb,
      dvd_c_of_prime_of_dvd_a_of_dvd_b_of_FLT hp hpa hpb HF]

Premises used: dvd_c_of_prime_of_dvd_a_of_dvd_b_of_FLT, id_eq
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
a b c : ℤ
Hgcd : Eq (α := ℤ) (Finset.gcd {a, b, c} id) 1
HF : a ^ n + b ^ n + c ^ n = 0
hn : n ≠ 0
p : ℤ
hp : Prime p
hpa : p ∣ a
hpb : p ∣ b
x : ℤ
hx : x = b
⊢ p ∣ id x

Tactic:
simp only [id_eq, hx, hpa, hpb,
      dvd_c_of_prime_of_dvd_a_of_dvd_b_of_FLT hp hpa hpb HF]

Premises used: dvd_c_of_prime_of_dvd_a_of_dvd_b_of_FLT, id_eq
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
a b c : ℤ
Hgcd : Eq (α := ℤ) (Finset.gcd {a, b, c} id) 1
HF : a ^ n + b ^ n + c ^ n = 0
hn : n ≠ 0
p : ℤ
hp : Prime p
hpa : p ∣ a
hpb : p ∣ b
x : ℤ
hx : x = c
⊢ p ∣ id x

Tactic:
simp only [id_eq, hx, hpa, hpb,
      dvd_c_of_prime_of_dvd_a_of_dvd_b_of_FLT hp hpa hpb HF]

Premises used: dvd_c_of_prime_of_dvd_a_of_dvd_b_of_FLT, id_eq
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c : ℤ
rw :
  a ≠ 0 ∧ b ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 ↔
    b ≠ 0 ∧ a ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2
⊢ a ≠ 0 ∧ b ≠ 0 ∧ HPow.hPow (β := ℕ) a 4 + HPow.hPow (β := ℕ) b 4 = HPow.hPow (β := ℕ) c 2 ↔
    b ≠ 0 ∧ a ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2

Tactic:
rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c : ℤ
mp :
  a ≠ 0 ∧ b ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 →
    b ≠ 0 ∧ a ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2
mpr :
  b ≠ 0 ∧ a ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 →
    a ≠ 0 ∧ b ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2
mp₁ mp₂ :
  a ≠ 0 →
    b ≠ 0 →
      HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 →
        b ≠ 0 ∧ a ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2
mp₃ : a ≠ 0 → b ≠ 0 → HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 → b ≠ 0
mp₄ : a ≠ 0 → b ≠ 0 → HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 → a ≠ 0
mp₅ :
  a ≠ 0 →
    b ≠ 0 →
      HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 →
        HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2
mpr₁ mpr₂ :
  b ≠ 0 →
    a ≠ 0 →
      HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 →
        a ≠ 0 ∧ b ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2
mpr₃ : b ≠ 0 → a ≠ 0 → HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 → a ≠ 0
mpr₄ : b ≠ 0 → a ≠ 0 → HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 → b ≠ 0
mpr₅ :
  b ≠ 0 →
    a ≠ 0 →
      HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 →
        HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2
⊢ a ≠ 0 ∧ b ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2 ↔
    b ≠ 0 ∧ a ≠ 0 ∧ HPow.hPow (β := ℕ) b 4 + HPow.hPow (β := ℕ) a 4 = HPow.hPow (β := ℕ) c 2

Tactic:
tauto
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c k : ℤ
hk0 : k ≠ 0
mp :
  a ≠ 0 ∧ b ≠ 0 ∧ HPow.hPow (β := ℕ) a 4 + HPow.hPow (β := ℕ) b 4 = HPow.hPow (β := ℕ) c 2 →
    k * a ≠ 0 ∧
      k * b ≠ 0 ∧
        HPow.hPow (β := ℕ) (k * a) 4 + HPow.hPow (β := ℕ) (k * b) 4 = HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) k 2 * c) 2
mpr :
  k * a ≠ 0 ∧
      k * b ≠ 0 ∧
        HPow.hPow (β := ℕ) (k * a) 4 + HPow.hPow (β := ℕ) (k * b) 4 =
          HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) k 2 * c) 2 →
    a ≠ 0 ∧ b ≠ 0 ∧ HPow.hPow (β := ℕ) a 4 + HPow.hPow (β := ℕ) b 4 = HPow.hPow (β := ℕ) c 2
⊢ a ≠ 0 ∧ b ≠ 0 ∧ HPow.hPow (β := ℕ) a 4 + HPow.hPow (β := ℕ) b 4 = HPow.hPow (β := ℕ) c 2 ↔
    k * a ≠ 0 ∧
      k * b ≠ 0 ∧
        HPow.hPow (β := ℕ) (k * a) 4 + HPow.hPow (β := ℕ) (k * b) 4 = HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) k 2 * c) 2

Tactic:
constructor
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c k : ℤ
hk0 : k ≠ 0
⊢ a ≠ 0 ∧ b ≠ 0 ∧ HPow.hPow (β := ℕ) a 4 + HPow.hPow (β := ℕ) b 4 = HPow.hPow (β := ℕ) c 2 →
    k * a ≠ 0 ∧
      k * b ≠ 0 ∧
        HPow.hPow (β := ℕ) (k * a) 4 + HPow.hPow (β := ℕ) (k * b) 4 = HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) k 2 * c) 2

Tactic:
grind [mul_eq_zero]

Premises used: mul_eq_zero
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c k : ℤ
hk0 : k ≠ 0
f42 :
  k * a ≠ 0 ∧
    k * b ≠ 0 ∧
      HPow.hPow (β := ℕ) (k * a) 4 + HPow.hPow (β := ℕ) (k * b) 4 = HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) k 2 * c) 2
mpr : a ≠ 0
mpr₁ : b ≠ 0 ∧ HPow.hPow (β := ℕ) a 4 + HPow.hPow (β := ℕ) b 4 = HPow.hPow (β := ℕ) c 2
⊢ a ≠ 0 ∧ b ≠ 0 ∧ HPow.hPow (β := ℕ) a 4 + HPow.hPow (β := ℕ) b 4 = HPow.hPow (β := ℕ) c 2

Tactic:
constructor
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c k : ℤ
hk0 : k ≠ 0
f42 :
  k * a ≠ 0 ∧
    k * b ≠ 0 ∧
      HPow.hPow (β := ℕ) (k * a) 4 + HPow.hPow (β := ℕ) (k * b) 4 = HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) k 2 * c) 2
⊢ a ≠ 0

Tactic:
right_ne_zero_of_mul f42.1

Premises used: right_ne_zero_of_mul, And.left
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c k : ℤ
hk0 : k ≠ 0
f42 :
  k * a ≠ 0 ∧
    k * b ≠ 0 ∧
      HPow.hPow (β := ℕ) (k * a) 4 + HPow.hPow (β := ℕ) (k * b) 4 = HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) k 2 * c) 2
⊢ a ≠ 0

Tactic:
exact right_ne_zero_of_mul f42.1

Premises used: right_ne_zero_of_mul, And.left
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c k : ℤ
hk0 : k ≠ 0
f42 :
  k * a ≠ 0 ∧
    k * b ≠ 0 ∧
      HPow.hPow (β := ℕ) (k * a) 4 + HPow.hPow (β := ℕ) (k * b) 4 = HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) k 2 * c) 2
mpr : b ≠ 0
mpr₁ : HPow.hPow (β := ℕ) a 4 + HPow.hPow (β := ℕ) b 4 = HPow.hPow (β := ℕ) c 2
⊢ b ≠ 0 ∧ HPow.hPow (β := ℕ) a 4 + HPow.hPow (β := ℕ) b 4 = HPow.hPow (β := ℕ) c 2

Tactic:
constructor
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c k : ℤ
hk0 : k ≠ 0
f42 :
  k * a ≠ 0 ∧
    k * b ≠ 0 ∧
      HPow.hPow (β := ℕ) (k * a) 4 + HPow.hPow (β := ℕ) (k * b) 4 = HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) k 2 * c) 2
⊢ b ≠ 0

Tactic:
right_ne_zero_of_mul f42.2.1

Premises used: right_ne_zero_of_mul, And.right, And.left
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c k : ℤ
hk0 : k ≠ 0
f42 :
  k * a ≠ 0 ∧
    k * b ≠ 0 ∧
      HPow.hPow (β := ℕ) (k * a) 4 + HPow.hPow (β := ℕ) (k * b) 4 = HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) k 2 * c) 2
⊢ b ≠ 0

Tactic:
exact right_ne_zero_of_mul f42.2.1

Premises used: right_ne_zero_of_mul, And.right, And.left
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c k : ℤ
hk0 : k ≠ 0
f42 :
  k * a ≠ 0 ∧
    k * b ≠ 0 ∧
      HPow.hPow (β := ℕ) (k * a) 4 + HPow.hPow (β := ℕ) (k * b) 4 = HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) k 2 * c) 2
mpr :
  HPow.hPow (β := ℕ) k 4 * (HPow.hPow (β := ℕ) a 4 + HPow.hPow (β := ℕ) b 4) =
    HPow.hPow (β := ℕ) k 4 * HPow.hPow (β := ℕ) c 2
⊢ HPow.hPow (β := ℕ) a 4 + HPow.hPow (β := ℕ) b 4 = HPow.hPow (β := ℕ) c 2

Tactic:
apply (mul_right_inj' (pow_ne_zero 4 hk0)).mp

Premises used: pow_ne_zero, Iff.mp, mul_right_inj', OfNat.ofNat
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c k : ℤ
hk0 : k ≠ 0
f42 :
  k * a ≠ 0 ∧
    k * b ≠ 0 ∧
      HPow.hPow (β := ℕ) (k * a) 4 + HPow.hPow (β := ℕ) (k * b) 4 = HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) k 2 * c) 2
⊢ HPow.hPow (β := ℕ) k 4 * (HPow.hPow (β := ℕ) a 4 + HPow.hPow (β := ℕ) b 4) =
    HPow.hPow (β := ℕ) k 4 * HPow.hPow (β := ℕ) c 2

Tactic:
linear_combination f42.2.2

Premises used: And.right
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c : ℤ
h : Fermat42 a b c
apply : HPow.hPow (β := ℕ) c 2 ≠ 0
⊢ c ≠ 0

Tactic:
apply ne_zero_pow two_ne_zero _

Premises used: two_ne_zero, ne_zero_pow
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c : ℤ
h : Fermat42 a b c
h₁ : 0 < HPow.hPow (β := ℕ) c 2
⊢ HPow.hPow (β := ℕ) c 2 ≠ 0

Tactic:
apply ne_of_gt

Premises used: ne_of_gt
-- Module: Mathlib.NumberTheory.FLT.Four
Goal:
a b c : ℤ
h : Fermat42 a b c
⊢ HPow.hPow (β := ℕ) a 4 + HPow.hPow (β := ℕ) b 4 =
    HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) a 2) 2 + HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) b 2) 2

Tactic:
ring