p : ℕ
hp : 0 < p
h : φ p = p - 1
⊢ Prime p
p : ℕ
hp : 0 < p
⊢ φ p = p - 1 ↔ Prime p
refine' ⟨fun h => _, totient_prime⟩
case hp
p : ℕ
hp : 0 < p
h : φ p = p - 1
⊢ 1 < p

p : ℕ
h : φ p = p - 1
hp : 1 < p
⊢ Prime p
p : ℕ
hp : 0 < p
h : φ p = p - 1
⊢ Prime p
replace hp : 1 < p
p : ℕ
h : Finset.card (filter (coprime p) (Ico (succ 0) p)) = Finset.card (Ico 1 p)
hp : 1 < p
⊢ Prime p
p : ℕ
h : φ p = p - 1
hp : 1 < p
⊢ Prime p
rw [totient_eq_card_coprime, range_eq_Ico, ← Ico_insert_succ_left hp.le, Finset.filter_insert,
  if_neg (not_coprime_of_dvd_of_dvd hp (dvd_refl p) (dvd_zero p)), ← Nat.card_Ico 1 p] at h
p : ℕ
h : Finset.card (filter (coprime p) (Ico (succ 0) p)) = Finset.card (Ico 1 p)
hp : 1 < p
n : ℕ
hn : n < p
hnz : n ≠ 0
⊢ succ 0 ≤ n
p : ℕ
h : Finset.card (filter (coprime p) (Ico (succ 0) p)) = Finset.card (Ico 1 p)
hp : 1 < p
⊢ Prime p
refine'
  p.prime_of_coprime hp fun n hn hnz => Finset.filter_card_eq h n <| Finset.mem_Ico.mpr ⟨_, hn⟩
no goals
p : ℕ
h : Finset.card (filter (coprime p) (Ico (succ 0) p)) = Finset.card (Ico 1 p)
hp : 1 < p
n : ℕ
hn : n < p
hnz : n ≠ 0
⊢ succ 0 ≤ n
rwa [succ_le_iff, pos_iff_ne_zero]
case hp.a
p : ℕ
hp : 0 < p
h : φ p = p - 1
⊢ 1 ≤ p

case hp.a
p : ℕ
hp : 0 < p
h : φ p = p - 1
⊢ 1 ≠ p
case hp
p : ℕ
hp : 0 < p
h : φ p = p - 1
⊢ 1 < p
apply lt_of_le_of_ne
no goals
case hp.a
p : ℕ
hp : 0 < p
h : φ p = p - 1
⊢ 1 ≤ p
rwa [succ_le_iff]
case hp.a
hp : 0 < 1
h : φ 1 = 1 - 1
⊢ False
case hp.a
p : ℕ
hp : 0 < p
h : φ p = p - 1
⊢ 1 ≠ p
rintro rfl
case hp.a
hp : 0 < 1
h✝ : 1 = 1 - 1
h : 1 = 0
⊢ False
case hp.a
hp : 0 < 1
h : φ 1 = 1 - 1
⊢ False
rw [totient_one, tsub_self] at h
no goals
case hp.a
hp : 0 < 1
h✝ : 1 = 1 - 1
h : 1 = 0
⊢ False
exact one_ne_zero h