awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Fermat
Goal:
a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ HPow.hPow (α := ℕ) 2 n + 1
this_1 : Fact (2 < p)
this : Fact (Prime p)
ha1 : HPow.hPow (α := ZMod p) (↑a : ZMod p) (HPow.hPow (α := ℕ) 2 n) = -1
h : Eq (α := ZMod p) (↑a : ZMod p) 0
⊢ Eq (α := ZMod p) 1 0

Tactic:
rw [h, zero_pow (pow_ne_zero n two_ne_zero), zero_eq_neg] at ha1

Premises used: zero_eq_neg, pow_ne_zero, two_ne_zero, zero_pow
-- Module: Mathlib.NumberTheory.Fermat
Goal:
a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ HPow.hPow (α := ℕ) 2 n + 1
this_1 : Fact (2 < p)
this : Fact (Prime p)
ha1 : HPow.hPow (α := ZMod p) (↑a : ZMod p) (HPow.hPow (α := ℕ) 2 n) = -1
h : Eq (α := ZMod p) (↑a : ZMod p) 0
ha1₁ : Eq (α := ZMod p) 1 0
⊢ Eq (α := ZMod p) (↑a : ZMod p) 0

Tactic:
rw [h, zero_pow (pow_ne_zero n two_ne_zero), zero_eq_neg] at ha1

Premises used: zero_eq_neg, pow_ne_zero, two_ne_zero, zero_pow
-- Module: Mathlib.NumberTheory.Fermat
Goal:
a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ HPow.hPow (α := ℕ) 2 n + 1
this_1 : Fact (2 < p)
this : Fact (Prime p)
ha1 : Eq (α := ZMod p) 1 0
h : Eq (α := ZMod p) (↑a : ZMod p) 0
⊢ False

Tactic:
one_ne_zero ha1

Premises used: one_ne_zero
-- Module: Mathlib.NumberTheory.Fermat
Goal:
a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ HPow.hPow (α := ℕ) 2 n + 1
this_1 : Fact (2 < p)
this : Fact (Prime p)
ha1 : Eq (α := ZMod p) 1 0
h : Eq (α := ZMod p) (↑a : ZMod p) 0
⊢ False

Tactic:
exact one_ne_zero ha1

Premises used: one_ne_zero
-- Module: Mathlib.NumberTheory.Fermat
Goal:
a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ HPow.hPow (α := ℕ) 2 n + 1
this_1 : Fact (2 < p)
this : Fact (Prime p)
ha1 : HPow.hPow (α := ZMod p) (↑a : ZMod p) (HPow.hPow (α := ℕ) 2 n) = -1
⊢ Ne (α := ZMod p) (↑a : ZMod p) 0

Tactic:
have ha0 : (a : ZMod p) ≠ 0 := by
    intro h
    rw [h, zero_pow (pow_ne_zero n two_ne_zero), zero_eq_neg] at ha1
    exact one_ne_zero ha1
-- Module: Mathlib.NumberTheory.Fermat
Goal:
a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ HPow.hPow (α := ℕ) 2 n + 1
this_1 : Fact (2 < p)
this : Fact (Prime p)
ha1 : HPow.hPow (α := ZMod p) (↑a : ZMod p) (HPow.hPow (α := ℕ) 2 n) = -1
ha0 : Ne (α := ZMod p) (↑a : ZMod p) 0
hnot : ¬HPow.hPow (α := ZMod p) (↑a : ZMod p) (HPow.hPow (α := ℕ) 2 n) = 1
hfin : HPow.hPow (α := ZMod p) (↑a : ZMod p) (HPow.hPow (α := ℕ) 2 (n + 1)) = 1
⊢ orderOf (G := ZMod p) (↑a : ZMod p) = HPow.hPow (α := ℕ) 2 (n + 1)

Tactic:
apply orderOf_eq_prime_pow

Premises used: orderOf_eq_prime_pow
-- Module: Mathlib.NumberTheory.Fermat
Goal:
a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ HPow.hPow (α := ℕ) 2 n + 1
this_1 : Fact (2 < p)
this : Fact (Prime p)
ha1 : HPow.hPow (α := ZMod p) (↑a : ZMod p) (HPow.hPow (α := ℕ) 2 n) = -1
ha0 : Ne (α := ZMod p) (↑a : ZMod p) 0
hnot : ¬Eq (α := ZMod p) (-1) 1
⊢ ¬HPow.hPow (α := ZMod p) (↑a : ZMod p) (HPow.hPow (α := ℕ) 2 n) = 1

Tactic:
rw [ha1]
-- Module: Mathlib.NumberTheory.Fermat
Goal:
a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ HPow.hPow (α := ℕ) 2 n + 1
this_1 : Fact (2 < p)
this : Fact (Prime p)
ha1 : HPow.hPow (α := ZMod p) (↑a : ZMod p) (HPow.hPow (α := ℕ) 2 n) = -1
ha0 : Ne (α := ZMod p) (↑a : ZMod p) 0
⊢ ¬Eq (α := ZMod p) (-1) 1

Tactic:
neg_one_ne_one

Premises used: ZMod.neg_one_ne_one
-- Module: Mathlib.NumberTheory.Fermat
Goal:
a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ HPow.hPow (α := ℕ) 2 n + 1
this_1 : Fact (2 < p)
this : Fact (Prime p)
ha1 : HPow.hPow (α := ZMod p) (↑a : ZMod p) (HPow.hPow (α := ℕ) 2 n) = -1
ha0 : Ne (α := ZMod p) (↑a : ZMod p) 0
⊢ ¬Eq (α := ZMod p) (-1) 1

Tactic:
exact neg_one_ne_one

Premises used: ZMod.neg_one_ne_one
-- Module: Mathlib.NumberTheory.Fermat
Goal:
a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ HPow.hPow (α := ℕ) 2 n + 1
this_1 : Fact (2 < p)
this : Fact (Prime p)
ha1 : HPow.hPow (α := ZMod p) (↑a : ZMod p) (HPow.hPow (α := ℕ) 2 n) = -1
ha0 : Ne (α := ZMod p) (↑a : ZMod p) 0
hfin : HPow.hPow (α := ZMod p) (↑a : ZMod p) (HPow.hPow (α := ℕ) 2 n * 2) = 1
hfin₁ : HPow.hPow (β := ℕ) (HPow.hPow (α := ZMod p) (↑a : ZMod p) (HPow.hPow (α := ℕ) 2 n)) 2 = 1
hfin₂ : HPow.hPow (α := ZMod p) (β := ℕ) (-1) 2 = 1
hfin₃ hfin₄ : Eq (α := ZMod p) 1 1
⊢ HPow.hPow (α := ZMod p) (↑a : ZMod p) (HPow.hPow (α := ℕ) 2 (n + 1)) = 1

Tactic:
rw [pow_succ, pow_mul, ha1, neg_one_sq]

Premises used: neg_one_sq, pow_succ, pow_mul
-- Module: Mathlib.NumberTheory.Fermat
Goal:
a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ HPow.hPow (α := ℕ) 2 n + 1
this_1 : Fact (2 < p)
this : Fact (Prime p)
ha1 : HPow.hPow (α := ZMod p) (↑a : ZMod p) (HPow.hPow (α := ℕ) 2 n) = -1
ha0 : Ne (α := ZMod p) (↑a : ZMod p) 0
⊢ orderOf (G := ZMod p) (↑a : ZMod p) = HPow.hPow (α := ℕ) 2 (n + 1)

Tactic:
have ha : orderOf (a : ZMod p) = 2 ^ (n + 1) := by
    apply orderOf_eq_prime_pow
    · rw [ha1]
      exact neg_one_ne_one
    · rw [pow_succ, pow_mul, ha1, neg_one_sq]
-- Module: Mathlib.NumberTheory.Fermat
Goal:
a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ HPow.hPow (α := ℕ) 2 n + 1
this_1 : Fact (2 < p)
this : Fact (Prime p)
ha1 : HPow.hPow (α := ZMod p) (↑a : ZMod p) (HPow.hPow (α := ℕ) 2 n) = -1
ha0 : Ne (α := ZMod p) (↑a : ZMod p) 0
ha : orderOf (G := ZMod p) (↑a : ZMod p) = HPow.hPow (α := ℕ) 2 (n + 1)
⊢ ∃ (k : ℕ), p = k * HPow.hPow (α := ℕ) 2 (n + 1) + 1

Tactic:
simpa [ha, dvd_def, Nat.sub_eq_iff_eq_add hp.one_le, mul_comm] using orderOf_dvd_card_sub_one ha0

Premises used: dvd_def, Nat.sub_eq_iff_eq_add, Nat.Prime.one_le, ZMod.orderOf_dvd_card_sub_one, mul_comm
-- Module: Mathlib.NumberTheory.Fermat
Goal:
n p : ℕ
hn : 1 < n
hp : Prime p
hpdvd : p ∣ n.fermatNumber
⊢ Fact (Prime p)

Tactic:
have : Fact p.Prime := Fact.mk hp
-- Module: Mathlib.NumberTheory.Fermat
Goal:
n p : ℕ
hn : 1 < n
hp : Prime p
hpdvd : p ∣ n.fermatNumber
this : Fact (Prime p)
⊢ p ≠ 2

Tactic:
((even_pow.mpr ⟨even_two, pow_ne_zero n two_ne_zero⟩).add_one).ne_two_of_dvd_nat hpdvd

Premises used: Iff.mpr, Even.add_one, even_two, Odd.ne_two_of_dvd_nat, pow_ne_zero, Nat.even_pow, two_ne_zero, And.intro
-- Module: Mathlib.NumberTheory.Fermat
Goal:
n p : ℕ
hn : 1 < n
hp : Prime p
hpdvd : p ∣ n.fermatNumber
this : Fact (Prime p)
⊢ p ≠ 2

Tactic:
exact ((even_pow.mpr ⟨even_two, pow_ne_zero n two_ne_zero⟩).add_one).ne_two_of_dvd_nat hpdvd

Premises used: Iff.mpr, Even.add_one, even_two, Odd.ne_two_of_dvd_nat, pow_ne_zero, Nat.even_pow, two_ne_zero, And.intro
-- Module: Mathlib.NumberTheory.Fermat
Goal:
n p : ℕ
hn : 1 < n
hp : Prime p
hpdvd : p ∣ n.fermatNumber
this : Fact (Prime p)
⊢ p ≠ 2

Tactic:
have hp2 : p ≠ 2 := by
    exact ((even_pow.mpr ⟨even_two, pow_ne_zero n two_ne_zero⟩).add_one).ne_two_of_dvd_nat hpdvd
-- Module: Mathlib.NumberTheory.Fermat
Goal:
n p : ℕ
hn : 1 < n
hp : Prime p
hpdvd : p ∣ n.fermatNumber
this : Fact (Prime p)
hp2 : p ≠ 2
obtain :
  ∀ (k : ℕ) (hp : Prime (k * HPow.hPow (α := ℕ) 2 (n + 1) + 1))
    (hpdvd : k * HPow.hPow (α := ℕ) 2 (n + 1) + 1 ∣ n.fermatNumber)
    (this : Fact (Prime (k * HPow.hPow (α := ℕ) 2 (n + 1) + 1))) (hp2 : k * HPow.hPow (α := ℕ) 2 (n + 1) + 1 ≠ 2),
    (k * HPow.hPow (α := ℕ) 2 (n + 1) + 1) % 8 = 1
⊢ p % 8 = 1

Tactic:
obtain ⟨k, rfl⟩ := pow_pow_add_primeFactors_one_lt hp hp2 hpdvd

Premises used: Nat.pow_pow_add_primeFactors_one_lt, rfl
-- Module: Mathlib.NumberTheory.Fermat
Goal:
n : ℕ
hn : 1 < n
k : ℕ
hp : Prime (k * HPow.hPow (α := ℕ) 2 (n + 1) + 1)
hpdvd : k * HPow.hPow (α := ℕ) 2 (n + 1) + 1 ∣ n.fermatNumber
this : Fact (Prime (k * HPow.hPow (α := ℕ) 2 (n + 1) + 1))
hp2 : k * HPow.hPow (α := ℕ) 2 (n + 1) + 1 ≠ 2
obtain :
  ∀ (n : ℕ) (hn : 1 < n + succ 1) (hp : Prime (k * HPow.hPow (α := ℕ) 2 (n + succ 1 + 1) + 1))
    (hpdvd : k * HPow.hPow (α := ℕ) 2 (n + succ 1 + 1) + 1 ∣ (n + succ 1).fermatNumber)
    (this : Fact (Prime (k * HPow.hPow (α := ℕ) 2 (n + succ 1 + 1) + 1)))
    (hp2 : k * HPow.hPow (α := ℕ) 2 (n + succ 1 + 1) + 1 ≠ 2), (k * HPow.hPow (α := ℕ) 2 (n + succ 1 + 1) + 1) % 8 = 1
⊢ (k * HPow.hPow (α := ℕ) 2 (n + 1) + 1) % 8 = 1

Tactic:
obtain ⟨n, rfl⟩ := Nat.exists_eq_add_of_le' hn

Premises used: Nat.exists_eq_add_of_le', rfl
-- Module: Mathlib.NumberTheory.Fermat
Goal:
k n : ℕ
hn : 1 < n + succ 1
hp : Prime (k * HPow.hPow (α := ℕ) 2 (n + succ 1 + 1) + 1)
hpdvd : k * HPow.hPow (α := ℕ) 2 (n + succ 1 + 1) + 1 ∣ (n + succ 1).fermatNumber
this : Fact (Prime (k * HPow.hPow (α := ℕ) 2 (n + succ 1 + 1) + 1))
hp2 : k * HPow.hPow (α := ℕ) 2 (n + succ 1 + 1) + 1 ≠ 2
rw : (k * HPow.hPow (α := ℕ) 2 n % 8 * (HPow.hPow (α := ℕ) 2 (succ 1 + 1) % 8) % 8 + 1) % 8 = 1
⊢ (k * HPow.hPow (α := ℕ) 2 (n + succ 1 + 1) + 1) % 8 = 1

Tactic:
rw [add_assoc, pow_add, ← mul_assoc, ← mod_add_mod, mul_mod]

Premises used: add_assoc, mul_assoc, pow_add, Nat.mul_mod, Nat.mod_add_mod
-- Module: Mathlib.NumberTheory.Fermat
Goal:
k n : ℕ
hn : 1 < n + succ 1
hp : Prime (k * HPow.hPow (α := ℕ) 2 (n + succ 1 + 1) + 1)
hpdvd : k * HPow.hPow (α := ℕ) 2 (n + succ 1 + 1) + 1 ∣ (n + succ 1).fermatNumber
this : Fact (Prime (k * HPow.hPow (α := ℕ) 2 (n + succ 1 + 1) + 1))
hp2 : k * HPow.hPow (α := ℕ) 2 (n + succ 1 + 1) + 1 ≠ 2
⊢ (k * HPow.hPow (α := ℕ) 2 n % 8 * (HPow.hPow (α := ℕ) 2 (succ 1 + 1) % 8) % 8 + 1) % 8 = 1

Tactic:
simp
-- Module: Mathlib.NumberTheory.Fermat
Goal:
n p : ℕ
hn : 1 < n
hp : Prime p
hpdvd : p ∣ n.fermatNumber
this : Fact (Prime p)
hp2 : p ≠ 2
⊢ p % 8 = 1

Tactic:
have hp8 : p % 8 = 1 := by
    obtain ⟨k, rfl⟩ := pow_pow_add_primeFactors_one_lt hp hp2 hpdvd
    obtain ⟨n, rfl⟩ := Nat.exists_eq_add_of_le' hn
    rw [add_assoc, pow_add, ← mul_assoc, ← mod_add_mod, mul_mod]
    simp
-- Module: Mathlib.NumberTheory.Fermat
Goal:
n p : ℕ
hn : 1 < n
hp : Prime p
hpdvd : p ∣ n.fermatNumber
this : Fact (Prime p)
hp2 : p ≠ 2
hp8 : p % 8 = 1
obtain : ∀ (a : ZMod p) (ha : 2 = a * a), ∃ (k : ℕ), p = k * HPow.hPow (α := ℕ) 2 (n + 2) + 1
⊢ ∃ (k : ℕ), p = k * HPow.hPow (α := ℕ) 2 (n + 2) + 1

Tactic:
obtain ⟨a, ha⟩ := (exists_sq_eq_two_iff hp2).mpr (Or.inl hp8)

Premises used: Iff.mpr, ZMod.exists_sq_eq_two_iff, Or.inl
-- Module: Mathlib.NumberTheory.Fermat
Goal:
n p : ℕ
hn : 1 < n
hp : Prime p
hpdvd : p ∣ n.fermatNumber
this : Fact (Prime p)
hp2 : p ≠ 2
hp8 : p % 8 = 1
a : ZMod p
ha : 2 = a * a
h : p ∣ a.val ^ HPow.hPow (α := ℕ) 2 (n + 1) + 1
⊢ ∃ (k : ℕ), p = k * HPow.hPow (α := ℕ) 2 (n + 2) + 1

Tactic:
pow_pow_add_primeFactors_one_lt hp hp2 h

Premises used: Nat.pow_pow_add_primeFactors_one_lt
-- Module: Mathlib.NumberTheory.Fermat
Goal:
n p : ℕ
hn : 1 < n
hp : Prime p
hpdvd : p ∣ n.fermatNumber
this : Fact (Prime p)
hp2 : p ≠ 2
hp8 : p % 8 = 1
a : ZMod p
ha : 2 = a * a
h : p ∣ a.val ^ HPow.hPow (α := ℕ) 2 (n + 1) + 1
⊢ ∃ (k : ℕ), p = k * HPow.hPow (α := ℕ) 2 (n + 2) + 1

Tactic:
exact pow_pow_add_primeFactors_one_lt hp hp2 h

Premises used: Nat.pow_pow_add_primeFactors_one_lt
-- Module: Mathlib.NumberTheory.Fermat
Goal:
n p : ℕ
hn : 1 < n
hp : Prime p
hpdvd : p ∣ n.fermatNumber
this : Fact (Prime p)
hp2 : p ≠ 2
hp8 : p % 8 = 1
a : ZMod p
ha : 2 = a * a
suffices : p ∣ a.val ^ HPow.hPow (α := ℕ) 2 (n + 1) + 1
⊢ ∃ (k : ℕ), p = k * HPow.hPow (α := ℕ) 2 (n + 2) + 1

Tactic:
suffices h : p ∣ a.val ^ (2 ^ (n + 1)) + 1 by
    exact pow_pow_add_primeFactors_one_lt hp hp2 h
-- Module: Mathlib.NumberTheory.Fermat
Goal:
n p : ℕ
hn : 1 < n
hp : Prime p
hpdvd : p ∣ n.fermatNumber
this : Fact (Prime p)
hp2 : p ≠ 2
hp8 : p % 8 = 1
a : ZMod p
ha : 2 = a * a
rw :
  ∀ (hpdvd : p ∣ HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1) (this : Fact (Prime p)) (hp2 : p ≠ 2)
    (hp8 : p % 8 = 1) (a : ZMod p) (ha : 2 = a * a), p ∣ a.val ^ HPow.hPow (α := ℕ) 2 (n + 1) + 1
⊢ p ∣ a.val ^ HPow.hPow (α := ℕ) 2 (n + 1) + 1

Tactic:
rw [fermatNumber] at hpdvd

Premises used: Nat.fermatNumber
-- Module: Mathlib.NumberTheory.Fermat
Goal:
n p : ℕ
hn : 1 < n
hp : Prime p
hpdvd : p ∣ HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1
this : Fact (Prime p)
hp2 : p ≠ 2
hp8 : p % 8 = 1
a : ZMod p
ha : 2 = a * a
rw :
  ∀ (this : Fact (Prime p)) (hpdvd : HPow.hPow (α := ZMod p) (↑2 : ZMod p) (HPow.hPow (α := ℕ) 2 n) + 1 = 0)
    (hp2 : p ≠ 2) (hp8 : p % 8 = 1) (a : ZMod p) (ha : 2 = a * a),
    HPow.hPow (α := ZMod p) (↑a.val : ZMod p) (HPow.hPow (α := ℕ) 2 (n + 1)) + 1 = 0
⊢ p ∣ a.val ^ HPow.hPow (α := ℕ) 2 (n + 1) + 1

Tactic:
rw [← natCast_eq_zero_iff, Nat.cast_add _ 1, Nat.cast_one, Nat.cast_pow] at hpdvd ⊢

Premises used: ZMod.natCast_eq_zero_iff, Nat.cast_add, Nat.cast_pow, OfNat.ofNat, Nat.cast_one
-- Module: Mathlib.NumberTheory.Fermat
Goal:
n p : ℕ
hn : 1 < n
hp : Prime p
this : Fact (Prime p)
hpdvd : HPow.hPow (α := ZMod p) (↑2 : ZMod p) (HPow.hPow (α := ℕ) 2 n) + 1 = 0
hp2 : p ≠ 2
hp8 : p % 8 = 1
a : ZMod p
ha : 2 = a * a
rwa : HPow.hPow (α := ZMod p) a.cast (HPow.hPow (α := ℕ) 2 (n + 1)) + 1 = 0
rwa₁ : a ^ HPow.hPow (α := ℕ) 2 (n + 1) + 1 = 0
rwa₂ : a ^ (2 * HPow.hPow (α := ℕ) 2 n) + 1 = 0
rwa₃ : HPow.hPow (β := ℕ) a 2 ^ HPow.hPow (α := ℕ) 2 n + 1 = 0
rwa₄ : (a * a) ^ HPow.hPow (α := ℕ) 2 n + 1 = 0
rwa₅ rwa₆ rwa₇ rwa₈ : HPow.hPow (α := ZMod p) 2 (HPow.hPow (α := ℕ) 2 n) + 1 = 0
⊢ HPow.hPow (α := ZMod p) (↑a.val : ZMod p) (HPow.hPow (α := ℕ) 2 (n + 1)) + 1 = 0

Tactic:
rwa [natCast_val, ZMod.cast_id, pow_succ', pow_mul, sq, ← ha]

Premises used: Nat.pow_succ', ZMod.natCast_val, sq, pow_mul, ZMod.cast_id
-- Module: Mathlib.NumberTheory.Fermat
Goal:
a n : ℕ
hn1 : n ≠ 1
hP : Prime (a ^ n - 1)
⊢ 1 < a ^ n

Tactic:
have han1 : 1 < a ^ n := tsub_pos_iff_lt.mp hP.pos
-- Module: Mathlib.NumberTheory.Fermat
Goal:
a n : ℕ
hn1 : n ≠ 1
hP : Prime (a ^ n - 1)
han1 : 1 < a ^ n
⊢ n ≠ 0

Tactic:
have hn0 : n ≠ 0 := fun h ↦ (h ▸ han1).ne' rfl
-- Module: Mathlib.NumberTheory.Fermat
Goal:
a n : ℕ
hn1 : n ≠ 1
hP : Prime (a ^ n - 1)
han1 : 1 < a ^ n
hn0 : n ≠ 0
⊢ 1 < a

Tactic:
have ha1 : 1 < a := (Nat.one_lt_pow_iff hn0).mp han1
-- Module: Mathlib.NumberTheory.Fermat
Goal:
a n : ℕ
hn1 : n ≠ 1
hP : Prime (a ^ n - 1)
han1 : 1 < a ^ n
hn0 : n ≠ 0
ha1 : 1 < a
⊢ 0 < a

Tactic:
have ha0 : 0 < a := one_pos.trans ha1
-- Module: Mathlib.NumberTheory.Fermat
Goal:
a n : ℕ
hn1 : n ≠ 1
hP : Prime (a ^ n - 1)
han1 : 1 < a ^ n
hn0 : n ≠ 0
ha1 : 1 < a
ha0 : 0 < a
contrapose! : ∀ (hn1 : a ≠ 2), n = 1
⊢ a = 2

Tactic:
contrapose! hn1
-- Module: Mathlib.NumberTheory.Fermat
Goal:
a n : ℕ
hP : Prime (a ^ n - 1)
han1 : 1 < a ^ n
hn0 : n ≠ 0
ha1 : 1 < a
ha0 : 0 < a
hn1 : a ≠ 2
h : a - 1 ∣ a ^ n - HPow.hPow (α := ℕ) 1 n := ⋯
⊢ a - 1 = a ^ n - 1

Tactic:
rw [one_pow, hP.dvd_iff_eq (mt (Nat.sub_eq_iff_eq_add ha1.le).mp hn1), eq_comm] at h

Premises used: one_pow, mt, Nat.Prime.dvd_iff_eq, LT.lt.le, Nat.sub_eq_iff_eq_add, eq_comm, Iff.mp
-- Module: Mathlib.NumberTheory.Fermat
Goal:
a n : ℕ
hP : Prime (a ^ n - 1)
han1 : 1 < a ^ n
hn0 : n ≠ 0
ha1 : 1 < a
ha0 : 0 < a
hn1 : a ≠ 2
h : a - 1 = a ^ n - 1
⊢ n = 1

Tactic:
(pow_eq_self_iff ha1).mp (Nat.sub_one_cancel ha0 (pow_pos ha0 n) h).symm

Premises used: pow_pos, Nat.sub_one_cancel, Nat.pow_eq_self_iff, Iff.mp, Eq.symm
-- Module: Mathlib.NumberTheory.Fermat
Goal:
a n : ℕ
hP : Prime (a ^ n - 1)
han1 : 1 < a ^ n
hn0 : n ≠ 0
ha1 : 1 < a
ha0 : 0 < a
hn1 : a ≠ 2
h : a - 1 = a ^ n - 1
⊢ n = 1

Tactic:
exact (pow_eq_self_iff ha1).mp (Nat.sub_one_cancel ha0 (pow_pos ha0 n) h).symm

Premises used: pow_pos, Nat.sub_one_cancel, Nat.pow_eq_self_iff, Iff.mp, Eq.symm
-- Module: Mathlib.NumberTheory.Fermat
Goal:
a n : ℕ
hn1 : n ≠ 1
hP : Prime (a ^ n - 1)
han1 : 1 < a ^ n
hn0 : n ≠ 0
ha1 : 1 < a
ha0 : 0 < a
⊢ a = 2

Tactic:
have ha2 : a = 2 := by
    contrapose! hn1
    let h := Nat.sub_dvd_pow_sub_pow a 1 n
    rw [one_pow, hP.dvd_iff_eq (mt (Nat.sub_eq_iff_eq_add ha1.le).mp hn1), eq_comm] at h
    exact (pow_eq_self_iff ha1).mp (Nat.sub_one_cancel ha0 (pow_pos ha0 n) h).symm
-- Module: Mathlib.NumberTheory.Fermat
Goal:
a n : ℕ
hn1 : n ≠ 1
hP : Prime (a ^ n - 1)
han1 : 1 < a ^ n
hn0 : n ≠ 0
ha1 : 1 < a
ha0 : 0 < a
ha2 : a = 2
subst :
  ∀ (hP : Prime (HPow.hPow (α := ℕ) 2 n - 1)) (han1 : 1 < HPow.hPow (α := ℕ) 2 n) (ha1 : LT.lt (α := ℕ) 1 2)
    (ha0 : LT.lt (α := ℕ) 0 2), Eq (α := ℕ) 2 2 ∧ Prime n
⊢ a = 2 ∧ Prime n

Tactic:
subst ha2
-- Module: Mathlib.NumberTheory.Fermat
Goal:
n : ℕ
hn1 : n ≠ 1
hn0 : n ≠ 0
hP : Prime (HPow.hPow (α := ℕ) 2 n - 1)
han1 : 1 < HPow.hPow (α := ℕ) 2 n
ha1 : LT.lt (α := ℕ) 1 2
ha0 : LT.lt (α := ℕ) 0 2
⊢ Eq (α := ℕ) 2 2 ∧ Prime n

Tactic:
⟨rfl, Nat.prime_def.mpr ⟨(two_le_iff n).mpr ⟨hn0, hn1⟩, fun d hdn ↦ ?_⟩⟩

Premises used: Iff.mpr, Nat.two_le_iff, Nat.prime_def, And.intro, rfl
-- Module: Mathlib.NumberTheory.Fermat
Goal:
n : ℕ
hn1 : n ≠ 1
hn0 : n ≠ 0
hP : Prime (HPow.hPow (α := ℕ) 2 n - 1)
han1 : 1 < HPow.hPow (α := ℕ) 2 n
ha1 : LT.lt (α := ℕ) 1 2
ha0 : LT.lt (α := ℕ) 0 2
refine : ∀ (d : ℕ) (hdn : d ∣ n), d = 1 ∨ d = n
⊢ Eq (α := ℕ) 2 2 ∧ Prime n

Tactic:
refine ⟨rfl, Nat.prime_def.mpr ⟨(two_le_iff n).mpr ⟨hn0, hn1⟩, fun d hdn ↦ ?_⟩⟩
-- Module: Mathlib.NumberTheory.Fermat
Goal:
n : ℕ
hn1 : n ≠ 1
hn0 : n ≠ 0
hP : Prime (HPow.hPow (α := ℕ) 2 n - 1)
han1 : 1 < HPow.hPow (α := ℕ) 2 n
ha1 : LT.lt (α := ℕ) 1 2
ha0 : LT.lt (α := ℕ) 0 2
d : ℕ
hdn : d ∣ n
⊢ ∀ (x y : ℕ), HPow.hPow (α := ℕ) 2 x - 1 = HPow.hPow (α := ℕ) 2 y - 1 → x = y

Tactic:
have hinj : ∀ x y, 2 ^ x - 1 = 2 ^ y - 1 → x = y :=
    fun x y h ↦ Nat.pow_right_injective le_rfl (sub_one_cancel (pow_pos ha0 x) (pow_pos ha0 y) h)
-- Module: Mathlib.NumberTheory.Fermat
Goal:
n : ℕ
hn1 : n ≠ 1
hn0 : n ≠ 0
hP : Prime (HPow.hPow (α := ℕ) 2 n - 1)
han1 : 1 < HPow.hPow (α := ℕ) 2 n
ha1 : LT.lt (α := ℕ) 1 2
ha0 : LT.lt (α := ℕ) 0 2
d : ℕ
hdn : d ∣ n
hinj : ∀ (x y : ℕ), HPow.hPow (α := ℕ) 2 x - 1 = HPow.hPow (α := ℕ) 2 y - 1 → x = y
h : HPow.hPow (α := ℕ) 2 d - 1 ∣ HPow.hPow (α := ℕ) 2 d ^ (n / d) - HPow.hPow (α := ℕ) 1 (n / d) := ⋯
⊢ HPow.hPow (α := ℕ) 2 d - 1 ∣ HPow.hPow (α := ℕ) 2 n - 1

Tactic:
rw [one_pow, ← pow_mul, Nat.mul_div_cancel' hdn] at h

Premises used: one_pow, pow_mul, Nat.mul_div_cancel'
-- Module: Mathlib.NumberTheory.Fermat
Goal:
n : ℕ
hn1 : n ≠ 1
hn0 : n ≠ 0
hP : Prime (HPow.hPow (α := ℕ) 2 n - 1)
han1 : 1 < HPow.hPow (α := ℕ) 2 n
ha1 : LT.lt (α := ℕ) 1 2
ha0 : LT.lt (α := ℕ) 0 2
d : ℕ
hdn : d ∣ n
hinj : ∀ (x y : ℕ), HPow.hPow (α := ℕ) 2 x - 1 = HPow.hPow (α := ℕ) 2 y - 1 → x = y
h : HPow.hPow (α := ℕ) 2 d - 1 ∣ HPow.hPow (α := ℕ) 2 n - 1
⊢ d = 1 ∨ d = n

Tactic:
(hP.eq_one_or_self_of_dvd (2 ^ d - 1) h).imp (hinj d 1) (hinj d n)

Premises used: HSub.hSub, Nat.Prime.eq_one_or_self_of_dvd, HPow.hPow, Or.imp, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Fermat
Goal:
n : ℕ
hn1 : n ≠ 1
hn0 : n ≠ 0
hP : Prime (HPow.hPow (α := ℕ) 2 n - 1)
han1 : 1 < HPow.hPow (α := ℕ) 2 n
ha1 : LT.lt (α := ℕ) 1 2
ha0 : LT.lt (α := ℕ) 0 2
d : ℕ
hdn : d ∣ n
hinj : ∀ (x y : ℕ), HPow.hPow (α := ℕ) 2 x - 1 = HPow.hPow (α := ℕ) 2 y - 1 → x = y
h : HPow.hPow (α := ℕ) 2 d - 1 ∣ HPow.hPow (α := ℕ) 2 n - 1
⊢ d = 1 ∨ d = n

Tactic:
exact (hP.eq_one_or_self_of_dvd (2 ^ d - 1) h).imp (hinj d 1) (hinj d n)

Premises used: HSub.hSub, Nat.Prime.eq_one_or_self_of_dvd, HPow.hPow, Or.imp, OfNat.ofNat
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
n b : ℕ
h : n.ProbablePrime b
h₁ : 1 ≤ n
h₂ : 1 ≤ b
pos : ∀ (h₃ : 2 ≤ n), n.Coprime b
neg : ∀ (h₃ : ¬2 ≤ n), n.Coprime b
⊢ n.Coprime b

Tactic:
by_cases h₃ : 2 ≤ n
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
n b : ℕ
h : n.ProbablePrime b
h₁ : 1 ≤ n
h₂ : 1 ≤ b
h₃ : 2 ≤ n
pos : ∀ (k : ℕ), Prime k → k ∣ n → ¬k ∣ b
⊢ n.Coprime b

Tactic:
apply Nat.coprime_of_dvd

Premises used: Nat.coprime_of_dvd
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
k : ℕ
hk : Prime k
m : ℕ
h₁ : 1 ≤ k * m
h₃ : 2 ≤ k * m
j : ℕ
h₂ : 1 ≤ k * j
h : (k * m).ProbablePrime (k * j)
pos : k ∣ 1
⊢ False

Tactic:
apply Nat.Prime.not_dvd_one hk

Premises used: Nat.Prime.not_dvd_one
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
k : ℕ
hk : Prime k
m : ℕ
h₁ : 1 ≤ k * m
h₃ : 2 ≤ k * m
j : ℕ
h₂ : 1 ≤ k * j
h : (k * m).ProbablePrime (k * j)
⊢ k ∣ (k * j) ^ (k * m - 1) - 1

Tactic:
replace h := dvd_of_mul_right_dvd h
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
k : ℕ
hk : Prime k
m : ℕ
h₁ : 1 ≤ k * m
h₃ : 2 ≤ k * m
j : ℕ
h₂ : 1 ≤ k * j
h : k ∣ (k * j) ^ (k * m - 1) - 1
pos : k ∣ (k * j) ^ (k * m - 1)
⊢ k ∣ 1

Tactic:
rw [Nat.dvd_add_iff_right h, Nat.sub_add_cancel (Nat.one_le_pow _ _ h₂)]

Premises used: Nat.sub_add_cancel, Nat.one_le_pow, Nat.dvd_add_iff_right
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
k : ℕ
hk : Prime k
m : ℕ
h₁ : 1 ≤ k * m
h₃ : 2 ≤ k * m
j : ℕ
h₂ : 1 ≤ k * j
h : k ∣ (k * j) ^ (k * m - 1) - 1
⊢ k ∣ (k * j) ^ (k * m - 1)

Tactic:
dvd_of_mul_right_dvd (dvd_pow_self (k * j) ?_)

Premises used: HMul.hMul, dvd_of_mul_right_dvd, dvd_pow_self
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
k : ℕ
hk : Prime k
m : ℕ
h₁ : 1 ≤ k * m
h₃ : 2 ≤ k * m
j : ℕ
h₂ : 1 ≤ k * j
h : k ∣ (k * j) ^ (k * m - 1) - 1
pos : k * m - 1 ≠ 0
⊢ k ∣ (k * j) ^ (k * m - 1)

Tactic:
refine dvd_of_mul_right_dvd (dvd_pow_self (k * j) ?_)

Premises used: HMul.hMul, dvd_of_mul_right_dvd, dvd_pow_self
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
k : ℕ
hk : Prime k
m : ℕ
h₁ : 1 ≤ k * m
h₃ : 2 ≤ k * m
j : ℕ
h₂ : 1 ≤ k * j
h : k ∣ (k * j) ^ (k * m - 1) - 1
⊢ k * m - 1 ≠ 0

Tactic:
lia
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
n b : ℕ
h : n.ProbablePrime b
h₁ : 1 ≤ n
h₂ : 1 ≤ b
h₃ : ¬2 ≤ n
⊢ n = 1

Tactic:
lia
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
n b : ℕ
h : n.ProbablePrime b
h₁ : 1 ≤ n
h₂ : 1 ≤ b
h₃ : ¬2 ≤ n
neg : Coprime 1 b
⊢ n.Coprime b

Tactic:
rw [show n = 1 by lia]
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
n b : ℕ
h : n.ProbablePrime b
h₁ : 1 ≤ n
h₂ : 1 ≤ b
h₃ : ¬2 ≤ n
⊢ Coprime 1 b

Tactic:
simp
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
n b : ℕ
h : 1 ≤ b
⊢ 1 ≤ b ^ (n - 1)

Tactic:
have : 1 ≤ b ^ (n - 1) := one_le_pow₀ h
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
n b : ℕ
h : 1 ≤ b
this : 1 ≤ b ^ (n - 1)
rw : n.ProbablePrime b ↔ 1 ≡ b ^ (n - 1) [MOD n]
⊢ n.ProbablePrime b ↔ b ^ (n - 1) ≡ 1 [MOD n]

Tactic:
rw [Nat.ModEq.comm]

Premises used: Nat.ModEq.comm
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
n b : ℕ
h : 1 ≤ b
this : 1 ≤ b ^ (n - 1)
mp : n.ProbablePrime b → 1 ≡ b ^ (n - 1) [MOD n]
mpr : 1 ≡ b ^ (n - 1) [MOD n] → n.ProbablePrime b
⊢ n.ProbablePrime b ↔ 1 ≡ b ^ (n - 1) [MOD n]

Tactic:
constructor
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
n b : ℕ
h : 1 ≤ b
this : 1 ≤ b ^ (n - 1)
h₁ : n.ProbablePrime b
mp : (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑(b ^ (n - 1)) : ℤ) (↑1 : ℤ)
⊢ 1 ≡ b ^ (n - 1) [MOD n]

Tactic:
apply Nat.modEq_of_dvd

Premises used: Nat.modEq_of_dvd
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
n b : ℕ
h : 1 ≤ b
this : 1 ≤ b ^ (n - 1)
h₁ : n.ProbablePrime b
⊢ (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑(b ^ (n - 1)) : ℤ) (↑1 : ℤ)

Tactic:
mod_cast h₁

Premises used: Dvd.dvd, congrArg, Nat.cast_sub._simp_1, cast, Nat.cast, Eq.symm, Eq.trans, Int.ofNat_dvd._simp_1
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
n b : ℕ
h : 1 ≤ b
this : 1 ≤ b ^ (n - 1)
h₁ : n.ProbablePrime b
⊢ (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑(b ^ (n - 1)) : ℤ) (↑1 : ℤ)

Tactic:
exact mod_cast h₁
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
n b : ℕ
h : 1 ≤ b
this : 1 ≤ b ^ (n - 1)
h₁ : 1 ≡ b ^ (n - 1) [MOD n]
⊢ n.ProbablePrime b

Tactic:
mod_cast Nat.ModEq.dvd h₁

Premises used: Dvd.dvd, congrArg, Nat.cast_sub._simp_1, cast, Nat.cast, Nat.ProbablePrime, Eq.trans, Int.ofNat_dvd._simp_1, Nat.ModEq.dvd
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
n b : ℕ
h : 1 ≤ b
this : 1 ≤ b ^ (n - 1)
h₁ : 1 ≡ b ^ (n - 1) [MOD n]
⊢ n.ProbablePrime b

Tactic:
exact mod_cast Nat.ModEq.dvd h₁

Premises used: Nat.ModEq.dvd
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
n b : ℕ
h : n.FermatPsp b
h₁ : 1 ≤ b
⊢ n.ProbablePrime b

Tactic:
rcases h with ⟨hp, _, hn₂⟩
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
n b : ℕ
h : n.FermatPsp b
h₁ : 1 ≤ b
hp : n.ProbablePrime b
⊢ ¬Prime n

Tactic:
rcases h with ⟨hp, _, hn₂⟩
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
n b : ℕ
h : n.FermatPsp b
h₁ : 1 ≤ b
hp : n.ProbablePrime b
left : ¬Prime n
⊢ 1 < n

Tactic:
rcases h with ⟨hp, _, hn₂⟩
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
n b : ℕ
h₁ : 1 ≤ b
hp : n.ProbablePrime b
left : ¬Prime n
hn₂ : 1 < n
⊢ 1 ≤ n

Tactic:
lia
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
n b : ℕ
h₁ : 1 ≤ b
hp : n.ProbablePrime b
left : ¬Prime n
hn₂ : 1 < n
⊢ n.Coprime b

Tactic:
exact coprime_of_probablePrime hp (by lia) h₁

Premises used: Nat.coprime_of_probablePrime
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
n : ℕ
h₁ : 1 < n
h₂ : ¬Prime n
⊢ n.FermatPsp 1

Tactic:
⟨show n ∣ 1 ^ (n - 1) - 1 from ?_, h₂, h₁⟩

Premises used: Nat.FermatPsp, And.intro