awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
rw : ∀ (a : ℕ), ∃ (b : ℕ), Membership.mem (γ := Set ℕ) {n : ℕ | Even n ∧ n.Abundant} b ∧ a < b
⊢ Set.Infinite (α := ℕ) {n : ℕ | Even n ∧ n.Abundant}

Tactic:
rw [Set.infinite_iff_exists_gt]

Premises used: Set.infinite_iff_exists_gt
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
a : ℕ
⊢ Abundant 12

Tactic:
decide
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
a : ℕ
⊢ Abundant 12

Tactic:
have ha : Abundant 12 := by decide
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
a : ℕ
ha : Abundant 12
h : Membership.mem (γ := Set ℕ) {n : ℕ | Even n ∧ n.Abundant} (2 * (a + 1) * 12) ∧ a < 2 * (a + 1) * 12
⊢ ∃ (b : ℕ), Membership.mem (γ := Set ℕ) {n : ℕ | Even n ∧ n.Abundant} b ∧ a < b

Tactic:
use (2 * (a + 1)) * 12

Premises used: HMul.hMul, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
a : ℕ
ha : Abundant 12
⊢ 2 * (a + 1) ≠ 0

Tactic:
grind
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
a : ℕ
ha : Abundant 12
⊢ Membership.mem (γ := Set ℕ) {n : ℕ | Even n ∧ n.Abundant} (2 * (a + 1) * 12) ∧ a < 2 * (a + 1) * 12

Tactic:
grind [Abundant.mul_left ha (show 2 * (a + 1) ≠ 0 by grind)]

Premises used: Nat.Abundant.mul_left
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
rw : ∀ (a : ℕ), ∃ (b : ℕ), Membership.mem (γ := Set ℕ) {n : ℕ | Odd n ∧ n.Abundant} b ∧ a < b
⊢ Set.Infinite (α := ℕ) {n : ℕ | Odd n ∧ n.Abundant}

Tactic:
rw [Set.infinite_iff_exists_gt]

Premises used: Set.infinite_iff_exists_gt
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
a : ℕ
⊢ Abundant 945

Tactic:
decide +kernel
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
a : ℕ
⊢ Abundant 945

Tactic:
have ha : Abundant 945 := by decide +kernel
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
a : ℕ
ha : Abundant 945
h : Membership.mem (γ := Set ℕ) {n : ℕ | Odd n ∧ n.Abundant} ((2 * a + 1) * 945) ∧ a < (2 * a + 1) * 945
⊢ ∃ (b : ℕ), Membership.mem (γ := Set ℕ) {n : ℕ | Odd n ∧ n.Abundant} b ∧ a < b

Tactic:
use (2 * a + 1) * 945

Premises used: HMul.hMul, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
a : ℕ
ha : Abundant 945
⊢ 2 * a + 1 ≠ 0

Tactic:
grind
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
a : ℕ
ha : Abundant 945
⊢ Membership.mem (γ := Set ℕ) {n : ℕ | Odd n ∧ n.Abundant} ((2 * a + 1) * 945) ∧ a < (2 * a + 1) * 945

Tactic:
grind [Abundant.mul_left ha (show 2 * a + 1 ≠ 0 by grind)]

Premises used: Nat.Abundant.mul_left
-- Module: Mathlib.NumberTheory.Fermat
Goal:
⊢ fermatNumber 0 = 3

Tactic:
rfl

Premises used: Nat.fermatNumber, rfl
-- Module: Mathlib.NumberTheory.Fermat
Goal:
⊢ fermatNumber 1 = 5

Tactic:
rfl

Premises used: Nat.fermatNumber, rfl
-- Module: Mathlib.NumberTheory.Fermat
Goal:
⊢ fermatNumber 2 = 17

Tactic:
rfl

Premises used: Nat.fermatNumber, rfl
-- Module: Mathlib.NumberTheory.Fermat
Goal:
m n : ℕ
⊢ m < n → m.fermatNumber < n.fermatNumber

Tactic:
simp only [fermatNumber, add_lt_add_iff_right, Nat.pow_lt_pow_iff_right (one_lt_two : 1 < 2),
    imp_self]

Premises used: Nat.fermatNumber, imp_self, Nat.pow_lt_pow_iff_right, one_lt_two, add_lt_add_iff_right
-- Module: Mathlib.NumberTheory.Fermat
Goal:
⊢ Monotone fermatNumber

Tactic:
fermatNumber_strictMono.monotone

Premises used: StrictMono.monotone, Nat.fermatNumber_strictMono
-- Module: Mathlib.NumberTheory.Fermat
Goal:
⊢ Injective fermatNumber

Tactic:
fermatNumber_strictMono.injective

Premises used: StrictMono.injective, Nat.fermatNumber_strictMono
-- Module: Mathlib.NumberTheory.Fermat
Goal:
n : ℕ
⊢ 3 ≤ n.fermatNumber

Tactic:
fermatNumber_mono n.zero_le

Premises used: Nat.fermatNumber, Nat.zero_le, Nat.fermatNumber_mono
-- Module: Mathlib.NumberTheory.Fermat
Goal:
n : ℕ
⊢ 2 < n.fermatNumber

Tactic:
three_le_fermatNumber _

Premises used: Nat.three_le_fermatNumber, Nat.lt
-- Module: Mathlib.NumberTheory.Fermat
Goal:
n : ℕ
⊢ 3 ≤ n.fermatNumber

Tactic:
have := three_le_fermatNumber n
-- Module: Mathlib.NumberTheory.Fermat
Goal:
n : ℕ
this : 3 ≤ n.fermatNumber
⊢ n.fermatNumber ≠ 1

Tactic:
lia
-- Module: Mathlib.NumberTheory.Fermat
Goal:
n : ℕ
⊢ Odd n.fermatNumber

Tactic:
(even_pow.mpr ⟨even_two, (pow_pos two_pos n).ne'⟩).add_one

Premises used: Iff.mpr, Nat.fermatNumber, pow_pos, Even.add_one, even_two, Nat.even_pow, LT.lt.ne', And.intro
-- Module: Mathlib.NumberTheory.Fermat
Goal:
⊢ ∏ k ∈ range 0, k.fermatNumber = fermatNumber 0 - 2

Tactic:
rfl
-- Module: Mathlib.NumberTheory.Fermat
Goal:
n : ℕ
hn : ∏ k ∈ range n, k.fermatNumber = n.fermatNumber - 2
⊢ HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1 - 2 = HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) - 1

Tactic:
lia
-- Module: Mathlib.NumberTheory.Fermat
Goal:
n : ℕ
hn : ∏ k ∈ range n, k.fermatNumber = n.fermatNumber - 2
succ :
  HPow.hPow (β := ℕ) (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n)) 2 - HPow.hPow (α := ℕ) (β := ℕ) 1 2 =
    HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 (n + 1)) + 1 - 2
⊢ ∏ k ∈ range (n + 1), k.fermatNumber = (n + 1).fermatNumber - 2

Tactic:
rw [prod_range_succ, hn, fermatNumber, fermatNumber, mul_comm,
    (show 2 ^ 2 ^ n + 1 - 2 = 2 ^ 2 ^ n - 1 by lia), ← sq_sub_sq]

Premises used: Nat.fermatNumber, Nat.sq_sub_sq, mul_comm, Finset.prod_range_succ
-- Module: Mathlib.NumberTheory.Fermat
Goal:
n : ℕ
hn : ∏ k ∈ range n, k.fermatNumber = n.fermatNumber - 2
succ : HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n * 2) - 1 = 1 + HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n * 2) - 2
⊢ HPow.hPow (β := ℕ) (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n)) 2 - HPow.hPow (α := ℕ) (β := ℕ) 1 2 =
    HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 (n + 1)) + 1 - 2

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.Fermat
Goal:
n : ℕ
hn : ∏ k ∈ range n, k.fermatNumber = n.fermatNumber - 2
⊢ HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n * 2) - 1 = 1 + HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n * 2) - 2

Tactic:
lia
-- Module: Mathlib.NumberTheory.Fermat
Goal:
n : ℕ
zero : ∏ k ∈ range 0, k.fermatNumber = fermatNumber 0 - 2
succ :
  ∀ (n : ℕ) (hn : ∏ k ∈ range n, k.fermatNumber = n.fermatNumber - 2),
    ∏ k ∈ range (n + 1), k.fermatNumber = (n + 1).fermatNumber - 2
⊢ ∏ k ∈ range n, k.fermatNumber = n.fermatNumber - 2

Tactic:
induction n with | zero => rfl | succ n hn =>
  rw [prod_range_succ, hn, fermatNumber, fermatNumber, mul_comm,
    (show 2 ^ 2 ^ n + 1 - 2 = 2 ^ 2 ^ n - 1 by lia), ← sq_sub_sq]
  ring_nf
  lia

Premises used: Nat.fermatNumber, Nat.sq_sub_sq, mul_comm, Finset.prod_range_succ, Nat.zero, Nat.succ
-- Module: Mathlib.NumberTheory.Fermat
Goal:
n : ℕ
rw : 2 ≤ n.fermatNumber
⊢ n.fermatNumber = HAdd.hAdd (α := ℕ) (∏ k ∈ range n, k.fermatNumber) 2

Tactic:
rw [prod_fermatNumber, Nat.sub_add_cancel]

Premises used: Nat.prod_fermatNumber, Nat.sub_add_cancel
-- Module: Mathlib.NumberTheory.Fermat
Goal:
n : ℕ
⊢ 2 ≤ n.fermatNumber

Tactic:
le_of_lt <| two_lt_fermatNumber _

Premises used: le_of_lt, Nat.two_lt_fermatNumber
-- Module: Mathlib.NumberTheory.Fermat
Goal:
n : ℕ
⊢ 2 ≤ n.fermatNumber

Tactic:
exact le_of_lt <| two_lt_fermatNumber _

Premises used: le_of_lt, Nat.two_lt_fermatNumber
-- Module: Mathlib.NumberTheory.Fermat
Goal:
n : ℕ
rw : HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 (n + 1)) + 1 = HPow.hPow (β := ℕ) (n.fermatNumber - 1) 2 + 1
rw₁ : HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n * 2) + 1 = HPow.hPow (β := ℕ) (n.fermatNumber - 1) 2 + 1
rw₂ : HPow.hPow (α := ℕ) 2 (2 * HPow.hPow (α := ℕ) 2 n) + 1 = HPow.hPow (β := ℕ) (n.fermatNumber - 1) 2 + 1
rw₃ :
  HPow.hPow (β := ℕ) (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n)) 2 + 1 =
    HPow.hPow (β := ℕ) (n.fermatNumber - 1) 2 + 1
rw₄ :
  HPow.hPow (β := ℕ) (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n)) 2 + 1 =
    HPow.hPow (β := ℕ) (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1 - 1) 2 + 1
rw₅ rw₆ :
  HPow.hPow (β := ℕ) (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n)) 2 + 1 =
    HPow.hPow (β := ℕ) (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n)) 2 + 1
⊢ (n + 1).fermatNumber = HPow.hPow (β := ℕ) (n.fermatNumber - 1) 2 + 1

Tactic:
rw [fermatNumber, pow_succ, mul_comm, pow_mul', fermatNumber, add_tsub_cancel_right]

Premises used: Nat.fermatNumber, pow_succ, mul_comm, add_tsub_cancel_right, pow_mul'
-- Module: Mathlib.NumberTheory.Fermat
Goal:
n : ℕ
⊢ 0 ≤ 1 + HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n * 4)

Tactic:
have : 0 ≤ 1 + 2 ^ (2 ^ n * 4) := le_add_left _ _
-- Module: Mathlib.NumberTheory.Fermat
Goal:
n : ℕ
this : 0 ≤ 1 + HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n * 4)
ring_nf :
  HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n * 2) * 2 ≤
    1 + HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n * 2) * 2 + HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n * 4)
⊢ 2 * HPow.hPow (β := ℕ) (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n)) 2 ≤
    HPow.hPow (β := ℕ) (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 (n + 1)) + 1) 2

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.Fermat
Goal:
n : ℕ
this : 0 ≤ 1 + HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n * 4)
⊢ HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n * 2) * 2 ≤
    1 + HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n * 2) * 2 + HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n * 4)

Tactic:
lia
-- Module: Mathlib.NumberTheory.Fermat
Goal:
n : ℕ
rw :
  HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 (n + 2)) + 1 + 2 * HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 (n + 1)) -
      2 * HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 (n + 1)) =
    HPow.hPow (β := ℕ) (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 (n + 1)) + 1) 2 -
      2 * HPow.hPow (β := ℕ) (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n)) 2
⊢ HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 (n + 2)) + 1 =
    HPow.hPow (β := ℕ) (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 (n + 1)) + 1) 2 -
      2 * HPow.hPow (β := ℕ) (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n)) 2

Tactic:
rw [← add_sub_self_right (2 ^ 2 ^ (n + 2) + 1) <| 2 * 2 ^ 2 ^ (n + 1)]

Premises used: Nat.add_sub_self_right, HPow.hPow, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Fermat
Goal:
n : ℕ
⊢ HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 (n + 2)) + 1 + 2 * HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 (n + 1)) -
      2 * HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 (n + 1)) =
    HPow.hPow (β := ℕ) (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 (n + 1)) + 1) 2 -
      2 * HPow.hPow (β := ℕ) (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n)) 2

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.Fermat
Goal:
n : ℕ
rw :
  HSub.hSub (α := ℤ) (↑(HPow.hPow (β := ℕ) (n + 1).fermatNumber 2) : ℤ)
      (↑(2 * HPow.hPow (β := ℕ) (n.fermatNumber - 1) 2) : ℤ) =
    HPow.hPow (α := ℤ) (β := ℕ) (↑(n + 1).fermatNumber : ℤ) 2 -
      2 * HPow.hPow (β := ℕ) (HSub.hSub (α := ℤ) (↑n.fermatNumber : ℤ) 1) 2
⊢ (↑(n + 2).fermatNumber : ℤ) =
    HPow.hPow (α := ℤ) (β := ℕ) (↑(n + 1).fermatNumber : ℤ) 2 -
      2 * HPow.hPow (β := ℕ) (HSub.hSub (α := ℤ) (↑n.fermatNumber : ℤ) 1) 2

Tactic:
rw [Nat.fermatNumber_eq_fermatNumber_sq_sub_two_mul_fermatNumber_sub_one_sq,
    Nat.cast_sub <| two_mul_fermatNumber_sub_one_sq_le_fermatNumber_sq n]

Premises used: Nat.cast_sub, Nat.fermatNumber_eq_fermatNumber_sq_sub_two_mul_fermatNumber_sub_one_sq, Nat.two_mul_fermatNumber_sub_one_sq_le_fermatNumber_sq
-- Module: Mathlib.NumberTheory.Fermat
Goal:
n : ℕ
⊢ HSub.hSub (α := ℤ) (↑(HPow.hPow (β := ℕ) (n + 1).fermatNumber 2) : ℤ)
      (↑(2 * HPow.hPow (β := ℕ) (n.fermatNumber - 1) 2) : ℤ) =
    HPow.hPow (α := ℤ) (β := ℕ) (↑(n + 1).fermatNumber : ℤ) 2 -
      2 * HPow.hPow (β := ℕ) (HSub.hSub (α := ℤ) (↑n.fermatNumber : ℤ) 1) 2

Tactic:
simp only [fermatNumber, push_cast, add_tsub_cancel_right]

Premises used: Nat.fermatNumber, add_tsub_cancel_right
-- Module: Mathlib.NumberTheory.Fermat
Goal:
m n : ℕ
hmn : m ≠ n
inr :
  ∀ (this : ∀ {m n : ℕ} (hmn : m ≠ n) (hmn' : m < n), m.fermatNumber.Coprime n.fermatNumber) (hmn' : ¬m < n),
    m.fermatNumber.Coprime n.fermatNumber
wlog : ∀ {m n : ℕ} (hmn : m ≠ n) (hmn' : m < n), m.fermatNumber.Coprime n.fermatNumber
⊢ m.fermatNumber.Coprime n.fermatNumber

Tactic:
wlog hmn' : m < n
-- Module: Mathlib.NumberTheory.Fermat
Goal:
m n : ℕ
hmn : m ≠ n
this : ∀ {m n : ℕ} (hmn : m ≠ n) (hmn' : m < n), m.fermatNumber.Coprime n.fermatNumber
hmn' : ¬m < n
⊢ n < m

Tactic:
lia
-- Module: Mathlib.NumberTheory.Fermat
Goal:
m n : ℕ
hmn : m ≠ n
this : ∀ {m n : ℕ} (hmn : m ≠ n) (hmn' : m < n), m.fermatNumber.Coprime n.fermatNumber
hmn' : ¬m < n
⊢ m.fermatNumber.Coprime n.fermatNumber

Tactic:
simpa only [coprime_comm] using this hmn.symm (by lia)

Premises used: Ne.symm, Nat.coprime_comm
-- Module: Mathlib.NumberTheory.Fermat
Goal:
m n : ℕ
hmn : m ≠ n
hmn' : m < n
d : ℕ := m.fermatNumber.gcd n.fermatNumber
⊢ d ∣ n.fermatNumber

Tactic:
have h_n : d ∣ fermatNumber n := gcd_dvd_right ..
-- Module: Mathlib.NumberTheory.Fermat
Goal:
m n : ℕ
hmn : m ≠ n
hmn' : m < n
d : ℕ := m.fermatNumber.gcd n.fermatNumber
h_n : d ∣ n.fermatNumber
⊢ d ∣ 2

Tactic:
have h_m : d ∣ 2 := (Nat.dvd_add_right <| (gcd_dvd_left _ _).trans <| dvd_prod_of_mem _
    <| mem_range.mpr hmn').mp <| fermatNumber_eq_prod_add_two _ ▸ h_n
-- Module: Mathlib.NumberTheory.Fermat
Goal:
m n : ℕ
hmn : m ≠ n
hmn' : m < n
d : ℕ := m.fermatNumber.gcd n.fermatNumber
h_n : d ∣ n.fermatNumber
h_m : d ∣ 2
⊢ m.fermatNumber.Coprime n.fermatNumber

Tactic:
((dvd_prime prime_two).mp h_m).resolve_right fun h_two ↦ ?_

Premises used: Nat.dvd_prime, Nat.prime_two, Iff.mp, Or.resolve_right
-- Module: Mathlib.NumberTheory.Fermat
Goal:
m n : ℕ
hmn : m ≠ n
hmn' : m < n
d : ℕ := m.fermatNumber.gcd n.fermatNumber
h_n : d ∣ n.fermatNumber
h_m : d ∣ 2
refine : ∀ (h_two : d = 2), False
⊢ m.fermatNumber.Coprime n.fermatNumber

Tactic:
refine ((dvd_prime prime_two).mp h_m).resolve_right fun h_two ↦ ?_

Premises used: Nat.dvd_prime, Nat.prime_two, Iff.mp, Or.resolve_right
-- Module: Mathlib.NumberTheory.Fermat
Goal:
m n : ℕ
hmn : m ≠ n
hmn' : m < n
d : ℕ := m.fermatNumber.gcd n.fermatNumber
h_n : d ∣ n.fermatNumber
h_m : d ∣ 2
h_two : d = 2
⊢ False

Tactic:
(odd_fermatNumber _).not_two_dvd_nat (h_two ▸ h_n)

Premises used: Nat.odd_fermatNumber, Odd.not_two_dvd_nat
-- Module: Mathlib.NumberTheory.Fermat
Goal:
m n : ℕ
hmn : m ≠ n
hmn' : m < n
d : ℕ := m.fermatNumber.gcd n.fermatNumber
h_n : d ∣ n.fermatNumber
h_m : d ∣ 2
h_two : d = 2
⊢ False

Tactic:
exact (odd_fermatNumber _).not_two_dvd_nat (h_two ▸ h_n)

Premises used: Nat.odd_fermatNumber, Odd.not_two_dvd_nat
-- Module: Mathlib.NumberTheory.Fermat
Goal:
⊢ Pairwise fun (m n : ℕ) ↦ m.fermatNumber.Coprime n.fermatNumber

Tactic:
fun _m _n ↦ coprime_fermatNumber_fermatNumber

Premises used: Pairwise, Nat.coprime_fermatNumber_fermatNumber
-- Module: Mathlib.NumberTheory.Fermat
Goal:
a n : ℕ
ha : 1 < a
hn : n ≠ 0
hP : Prime (a ^ n + 1)
obtain :
  ∀ (k m : ℕ) (hm : Odd m) (hn : HPow.hPow (α := ℕ) 2 k * m ≠ 0) (hP : Prime (a ^ (HPow.hPow (α := ℕ) 2 k * m) + 1)),
    ∃ (m_1 : ℕ), HPow.hPow (α := ℕ) 2 k * m = HPow.hPow (α := ℕ) 2 m_1
⊢ ∃ (m : ℕ), n = HPow.hPow (α := ℕ) 2 m

Tactic:
obtain ⟨k, m, hm, rfl⟩ := exists_eq_two_pow_mul_odd hn

Premises used: Nat.exists_eq_two_pow_mul_odd, rfl
-- Module: Mathlib.NumberTheory.Fermat
Goal:
a : ℕ
ha : 1 < a
k m : ℕ
hm : Odd m
hn : HPow.hPow (α := ℕ) 2 k * m ≠ 0
hP : Prime (a ^ (HPow.hPow (α := ℕ) 2 k * m) + 1)
⊢ Prime ((a ^ HPow.hPow (α := ℕ) 2 k) ^ m + 1)

Tactic:
rw [pow_mul] at hP

Premises used: pow_mul
-- Module: Mathlib.NumberTheory.Fermat
Goal:
a : ℕ
ha : 1 < a
k m : ℕ
hm : Odd m
hn : HPow.hPow (α := ℕ) 2 k * m ≠ 0
hP : Prime ((a ^ HPow.hPow (α := ℕ) 2 k) ^ m + 1)
h : HPow.hPow (α := ℕ) 2 k * m = HPow.hPow (α := ℕ) 2 k
⊢ ∃ (m_1 : ℕ), HPow.hPow (α := ℕ) 2 k * m = HPow.hPow (α := ℕ) 2 m_1

Tactic:
use k
-- Module: Mathlib.NumberTheory.Fermat
Goal:
a : ℕ
ha : 1 < a
k m : ℕ
hm : Odd m
hn : HPow.hPow (α := ℕ) 2 k * m ≠ 0
hP : Prime ((a ^ HPow.hPow (α := ℕ) 2 k) ^ m + 1)
⊢ 1 < a ^ HPow.hPow (α := ℕ) 2 k

Tactic:
replace ha : 1 < a ^ 2 ^ k := one_lt_pow (pow_ne_zero k two_ne_zero) ha
-- Module: Mathlib.NumberTheory.Fermat
Goal:
a k m : ℕ
hm : Odd m
hn : HPow.hPow (α := ℕ) 2 k * m ≠ 0
hP : Prime ((a ^ HPow.hPow (α := ℕ) 2 k) ^ m + 1)
ha : 1 < a ^ HPow.hPow (α := ℕ) 2 k
h : a ^ HPow.hPow (α := ℕ) 2 k + 1 ∣ (a ^ HPow.hPow (α := ℕ) 2 k) ^ m + HPow.hPow (α := ℕ) 1 m := ⋯
⊢ m = 1

Tactic:
rw [one_pow, hP.dvd_iff_eq (Nat.lt_add_right 1 ha).ne', add_left_inj, pow_eq_self_iff ha] at h

Premises used: one_pow, Nat.Prime.dvd_iff_eq, add_left_inj, LT.lt.ne', Nat.pow_eq_self_iff, Nat.lt_add_right, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Fermat
Goal:
a k m : ℕ
hm : Odd m
hn : HPow.hPow (α := ℕ) 2 k * m ≠ 0
hP : Prime ((a ^ HPow.hPow (α := ℕ) 2 k) ^ m + 1)
ha : 1 < a ^ HPow.hPow (α := ℕ) 2 k
h : m = 1
h₁ : HPow.hPow (α := ℕ) 2 k * 1 = HPow.hPow (α := ℕ) 2 k
h₂ h₃ : HPow.hPow (α := ℕ) 2 k = HPow.hPow (α := ℕ) 2 k
⊢ HPow.hPow (α := ℕ) 2 k * m = HPow.hPow (α := ℕ) 2 k

Tactic:
rw [h, mul_one]

Premises used: mul_one
-- Module: Mathlib.NumberTheory.Fermat
Goal:
n : ℕ
h : HPow.hPow (α := ZMod n.fermatNumber) 3 (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1)) = -1
⊢ Fact (2 < n.fermatNumber)

Tactic:
have := Fact.mk (two_lt_fermatNumber n)
-- Module: Mathlib.NumberTheory.Fermat
Goal:
n : ℕ
h : HPow.hPow (α := ZMod n.fermatNumber) 3 (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1)) = -1
this : Fact (2 < n.fermatNumber)
⊢ HPow.hPow (α := ℕ) 2 n = HPow.hPow (α := ℕ) 2 n - 1 + 1

Tactic:
have key : 2 ^ n = 2 ^ n - 1 + 1 := (Nat.sub_add_cancel Nat.one_le_two_pow).symm
-- Module: Mathlib.NumberTheory.Fermat
Goal:
n : ℕ
h : HPow.hPow (α := ZMod n.fermatNumber) 3 (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1)) = -1
this : Fact (2 < n.fermatNumber)
key : HPow.hPow (α := ℕ) 2 n = HPow.hPow (α := ℕ) 2 n - 1 + 1
ha :
  HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1)) 3
      (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1 - 1) =
    1
hd :
  ∀ (q : ℕ),
    Prime q →
      q ∣ HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1 - 1 →
        HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1)) 3
            ((HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1 - 1) / q) ≠
          1
⊢ Prime n.fermatNumber

Tactic:
apply lucas_primality (p := 2 ^ (2 ^ n) + 1) (a := 3)

Premises used: lucas_primality, HPow.hPow, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Fermat
Goal:
n : ℕ
h : HPow.hPow (α := ZMod n.fermatNumber) 3 (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1)) = -1
this : Fact (2 < n.fermatNumber)
key : HPow.hPow (α := ℕ) 2 n = HPow.hPow (α := ℕ) 2 n - 1 + 1
ha :
  HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1)) 3
      (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n)) =
    1
ha₁ :
  HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1 + 1) + 1)) 3
      (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1 + 1)) =
    1
ha₂ :
  HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1) * 2 + 1)) 3
      (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1) * 2) =
    1
ha₃ :
  HPow.hPow (β := ℕ)
      (HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1) * 2 + 1)) 3
        (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1)))
      2 =
    1
ha₄ :
  HPow.hPow (β := ℕ)
      (HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1 + 1) + 1)) 3
        (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1)))
      2 =
    1
ha₅ :
  HPow.hPow (β := ℕ)
      (HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1)) 3
        (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1)))
      2 =
    1
ha₆ : HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1)) (β := ℕ) (-1) 2 = 1
ha₇ ha₈ : Eq (α := ZMod (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1)) 1 1
⊢ HPow.hPow (α := ZMod (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1)) 3
      (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1 - 1) =
    1

Tactic:
rw [Nat.add_sub_cancel, key, pow_succ, pow_mul, ← pow_succ, ← key, h, neg_one_sq]

Premises used: neg_one_sq, pow_succ, pow_mul, Nat.add_sub_cancel
-- Module: Mathlib.NumberTheory.Fermat
Goal:
n : ℕ
h : HPow.hPow (α := ZMod n.fermatNumber) 3 (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1)) = -1
this : Fact (2 < n.fermatNumber)
key : HPow.hPow (α := ℕ) 2 n = HPow.hPow (α := ℕ) 2 n - 1 + 1
p : ℕ
hp1 : Prime p
hp2 : p ∣ HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1 - 1
⊢ Ne (α := ZMod (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1)) (-1) 1

Tactic:
neg_one_ne_one

Premises used: Nat.fermatNumber, ZMod.neg_one_ne_one
-- Module: Mathlib.NumberTheory.Fermat
Goal:
n : ℕ
h : HPow.hPow (α := ZMod n.fermatNumber) 3 (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1)) = -1
this : Fact (2 < n.fermatNumber)
key : HPow.hPow (α := ℕ) 2 n = HPow.hPow (α := ℕ) 2 n - 1 + 1
p : ℕ
hp1 : Prime p
hp2 : p ∣ HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1 - 1
⊢ Ne (α := ZMod (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1)) (-1) 1

Tactic:
exact neg_one_ne_one

Premises used: ZMod.neg_one_ne_one
-- Module: Mathlib.NumberTheory.Fermat
Goal:
n : ℕ
h : HPow.hPow (α := ZMod n.fermatNumber) 3 ((n.fermatNumber - 1) / 2) = -1
h₁ : HPow.hPow (α := ZMod n.fermatNumber) 3 (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1)) = -1
⊢ Prime n.fermatNumber

Tactic:
apply pepin_primality

Premises used: Nat.pepin_primality
-- Module: Mathlib.NumberTheory.Fermat
Goal:
n : ℕ
h : HPow.hPow (α := ZMod n.fermatNumber) 3 ((n.fermatNumber - 1) / 2) = -1
h₁ :
  HPow.hPow (α := ZMod n.fermatNumber) 3 (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1)) =
    HPow.hPow (α := ZMod n.fermatNumber) 3 ((n.fermatNumber - 1) / 2)
⊢ HPow.hPow (α := ZMod n.fermatNumber) 3 (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1)) = -1

Tactic:
rw [← h]
-- Module: Mathlib.NumberTheory.Fermat
Goal:
n : ℕ
h : HPow.hPow (α := ZMod n.fermatNumber) 3 ((n.fermatNumber - 1) / 2) = -1
h₁ : HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1) = (n.fermatNumber - 1) / 2
⊢ HPow.hPow (α := ZMod n.fermatNumber) 3 (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1)) =
    HPow.hPow (α := ZMod n.fermatNumber) 3 ((n.fermatNumber - 1) / 2)

Tactic:
congr
-- Module: Mathlib.NumberTheory.Fermat
Goal:
n : ℕ
h : HPow.hPow (α := ZMod n.fermatNumber) 3 ((n.fermatNumber - 1) / 2) = -1
h₁ : HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1) = (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) + 1 - 1) / 2
h₂ : HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1) = HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n) / 2
h₃ h₄ : HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1) = HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1)
⊢ HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n - 1) = (n.fermatNumber - 1) / 2

Tactic:
rw [fermatNumber, add_tsub_cancel_right, Nat.pow_div Nat.one_le_two_pow Nat.zero_lt_two]

Premises used: Nat.fermatNumber, Nat.one_le_two_pow, Nat.zero_lt_two, add_tsub_cancel_right, Nat.pow_div
-- Module: Mathlib.NumberTheory.Fermat
Goal:
a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ HPow.hPow (α := ℕ) 2 n + 1
⊢ Fact (2 < p)

Tactic:
have : Fact (2 < p) := Fact.mk (lt_of_le_of_ne hp.two_le hp2.symm)
-- Module: Mathlib.NumberTheory.Fermat
Goal:
a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ HPow.hPow (α := ℕ) 2 n + 1
this : Fact (2 < p)
⊢ Fact (Prime p)

Tactic:
have : Fact p.Prime := Fact.mk hp
-- 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)
rw : HPow.hPow (α := ZMod p) (↑a : ZMod p) (HPow.hPow (α := ℕ) 2 n) + 1 = 0
⊢ HPow.hPow (α := ZMod p) (↑a : ZMod p) (HPow.hPow (α := ℕ) 2 n) = -1

Tactic:
rw [eq_neg_iff_add_eq_zero]

Premises used: eq_neg_iff_add_eq_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)
⊢ HPow.hPow (α := ZMod p) (↑a : ZMod p) (HPow.hPow (α := ℕ) 2 n) + 1 = 0

Tactic:
exact_mod_cast (natCast_eq_zero_iff (a ^ (2 ^ n) + 1) p).mpr hpdvd

Premises used: Iff.mpr, ZMod.natCast_eq_zero_iff, HPow.hPow, HAdd.hAdd, OfNat.ofNat
-- 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)
⊢ HPow.hPow (α := ZMod p) (↑a : ZMod p) (HPow.hPow (α := ℕ) 2 n) = -1

Tactic:
have ha1 : (a : ZMod p) ^ (2 ^ n) = -1 := by
    rw [eq_neg_iff_add_eq_zero]
    exact_mod_cast (natCast_eq_zero_iff (a ^ (2 ^ n) + 1) p).mpr hpdvd