-- Mathlib/NumberTheory/Fermat.lean
theorem prime_of_pow_sub_one_prime {a n : ℕ} (hn1 : n ≠ 1) (hP : (a ^ n - 1).Prime) :
    a = 2 ∧ n.Prime

Proof state:
a n : ℕ
hn1 : n ≠ 1
hP : Prime (a ^ n - 1)
han1 : 1 < a ^ n
hn0 : n ≠ 0
ha1 : 1 < a
⊢ a = 2 ∧ Prime n

Tactic:
have ha0 : 0 < a := one_pos.trans ha1

Result:
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 ∧ Prime n

Proof state:
a n : ℕ
hn1 : n ≠ 1
hP : Prime (a ^ n - 1)
han1 : 1 < a ^ n
hn0 : n ≠ 0
⊢ a = 2 ∧ Prime n

Tactic:
have ha1 : 1 < a := (Nat.one_lt_pow_iff hn0).mp han1

Result:
a n : ℕ
hn1 : n ≠ 1
hP : Prime (a ^ n - 1)
han1 : 1 < a ^ n
hn0 : n ≠ 0
ha1 : 1 < a
⊢ a = 2 ∧ Prime n

Proof state:
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 := nat_sub_dvd_pow_sub_pow a 1 n
⊢ 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

Result:
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

Proof state:
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

Result:
no goals

Proof state:
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:
contrapose! hn1

Result:
a n : ℕ
hP : Prime (a ^ n - 1)
han1 : 1 < a ^ n
hn0 : n ≠ 0
ha1 : 1 < a
ha0 : 0 < a
hn1 : a ≠ 2
⊢ n = 1

Proof state:
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
⊢ a = 2 ∧ Prime n

Tactic:
subst ha2

Result:
n : ℕ
hn1 : n ≠ 1
hn0 : n ≠ 0
hP : Prime (2 ^ n - 1)
han1 : 1 < 2 ^ n
ha1 : 1 < 2
ha0 : 0 < 2
⊢ 2 = 2 ∧ Prime n

Proof state:
a n : ℕ
hn1 : n ≠ 1
hP : Prime (a ^ n - 1)
han1 : 1 < a ^ n
⊢ a = 2 ∧ Prime n

Tactic:
have hn0 : n ≠ 0 := fun h ↦ (h ▸ han1).ne' rfl

Result:
a n : ℕ
hn1 : n ≠ 1
hP : Prime (a ^ n - 1)
han1 : 1 < a ^ n
hn0 : n ≠ 0
⊢ a = 2 ∧ Prime n

Proof state:
a n : ℕ
hP : Prime (a ^ n - 1)
han1 : 1 < a ^ n
hn0 : n ≠ 0
ha1 : 1 < a
ha0 : 0 < a
hn1 : a ≠ 2
⊢ n = 1

Tactic:
let h := nat_sub_dvd_pow_sub_pow a 1 n

Result:
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 := nat_sub_dvd_pow_sub_pow a 1 n
⊢ n = 1

Proof state:
n : ℕ
hn1 : n ≠ 1
hn0 : n ≠ 0
hP : Prime (2 ^ n - 1)
han1 : 1 < 2 ^ n
ha1 : 1 < 2
ha0 : 0 < 2
d : ℕ
hdn : d ∣ n
⊢ d = 1 ∨ d = n

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)

Result:
n : ℕ
hn1 : n ≠ 1
hn0 : n ≠ 0
hP : Prime (2 ^ n - 1)
han1 : 1 < 2 ^ n
ha1 : 1 < 2
ha0 : 0 < 2
d : ℕ
hdn : d ∣ n
hinj : ∀ (x y : ℕ), 2 ^ x - 1 = 2 ^ y - 1 → x = y
⊢ d = 1 ∨ d = n

Proof state:
n : ℕ
hn1 : n ≠ 1
hn0 : n ≠ 0
hP : Prime (2 ^ n - 1)
han1 : 1 < 2 ^ n
ha1 : 1 < 2
ha0 : 0 < 2
⊢ 2 = 2 ∧ Prime n

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

Result:
n : ℕ
hn1 : n ≠ 1
hn0 : n ≠ 0
hP : Prime (2 ^ n - 1)
han1 : 1 < 2 ^ n
ha1 : 1 < 2
ha0 : 0 < 2
d : ℕ
hdn : d ∣ n
⊢ d = 1 ∨ d = n

Proof state:
n : ℕ
hn1 : n ≠ 1
hn0 : n ≠ 0
hP : Prime (2 ^ n - 1)
han1 : 1 < 2 ^ n
ha1 : 1 < 2
ha0 : 0 < 2
d : ℕ
hdn : d ∣ n
hinj : ∀ (x y : ℕ), 2 ^ x - 1 = 2 ^ y - 1 → x = y
h : 2 ^ d - 1 ∣ 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)

Result:
no goals

Proof state:
n : ℕ
hn1 : n ≠ 1
hn0 : n ≠ 0
hP : Prime (2 ^ n - 1)
han1 : 1 < 2 ^ n
ha1 : 1 < 2
ha0 : 0 < 2
d : ℕ
hdn : d ∣ n
hinj : ∀ (x y : ℕ), 2 ^ x - 1 = 2 ^ y - 1 → x = y
⊢ d = 1 ∨ d = n

Tactic:
let h := nat_sub_dvd_pow_sub_pow (2 ^ d) 1 (n / d)

Result:
n : ℕ
hn1 : n ≠ 1
hn0 : n ≠ 0
hP : Prime (2 ^ n - 1)
han1 : 1 < 2 ^ n
ha1 : 1 < 2
ha0 : 0 < 2
d : ℕ
hdn : d ∣ n
hinj : ∀ (x y : ℕ), 2 ^ x - 1 = 2 ^ y - 1 → x = y
h : 2 ^ d - 1 ∣ (2 ^ d) ^ (n / d) - 1 ^ (n / d) := nat_sub_dvd_pow_sub_pow (2 ^ d) 1 (n / d)
⊢ d = 1 ∨ d = n

Proof state:
n : ℕ
hn1 : n ≠ 1
hn0 : n ≠ 0
hP : Prime (2 ^ n - 1)
han1 : 1 < 2 ^ n
ha1 : 1 < 2
ha0 : 0 < 2
d : ℕ
hdn : d ∣ n
hinj : ∀ (x y : ℕ), 2 ^ x - 1 = 2 ^ y - 1 → x = y
h : 2 ^ d - 1 ∣ (2 ^ d) ^ (n / d) - 1 ^ (n / d) := nat_sub_dvd_pow_sub_pow (2 ^ d) 1 (n / d)
⊢ d = 1 ∨ d = n

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

Result:
n : ℕ
hn1 : n ≠ 1
hn0 : n ≠ 0
hP : Prime (2 ^ n - 1)
han1 : 1 < 2 ^ n
ha1 : 1 < 2
ha0 : 0 < 2
d : ℕ
hdn : d ∣ n
hinj : ∀ (x y : ℕ), 2 ^ x - 1 = 2 ^ y - 1 → x = y
h : 2 ^ d - 1 ∣ 2 ^ n - 1
⊢ d = 1 ∨ d = n

Proof state:
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 ∧ Prime n

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

Result:
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
⊢ a = 2 ∧ Prime n

Proof state:
a n : ℕ
hn1 : n ≠ 1
hP : Prime (a ^ n - 1)
⊢ a = 2 ∧ Prime n

Tactic:
have han1 : 1 < a ^ n := tsub_pos_iff_lt.mp hP.pos

Result:
a n : ℕ
hn1 : n ≠ 1
hP : Prime (a ^ n - 1)
han1 : 1 < a ^ n
⊢ a = 2 ∧ Prime n