no goals
⊢ φ 0 = 1 ↔ 0 = 1 ∨ 0 = 2
simp
no goals
⊢ φ 1 = 1 ↔ 1 = 1 ∨ 1 = 2
simp
no goals
⊢ φ 2 = 1 ↔ 2 = 1 ∨ 2 = 2
simp
n : ℕ
this : 3 ≤ n + 3
⊢ φ (n + 3) = 1 ↔ n + 3 = 1 ∨ n + 3 = 2
n : ℕ
⊢ φ (n + 3) = 1 ↔ n + 3 = 1 ∨ n + 3 = 2
have : 3 ≤ n + 3 := le_add_self
n : ℕ
this : 3 ≤ n + 3
⊢ φ (n + 3) = 1 ↔ n + 3 = 2
n : ℕ
this : 3 ≤ n + 3
⊢ φ (n + 3) = 1 ↔ n + 3 = 1 ∨ n + 3 = 2
simp only [succ_succ_ne_one, false_or_iff]
no goals
n : ℕ
this : 3 ≤ n + 3
⊢ φ (n + 3) = 1 ↔ n + 3 = 2
exact ⟨fun h => not_even_one.elim <| h ▸ totient_even this, by rintro ⟨⟩⟩
no goals
n : ℕ
this : 3 ≤ n + 3
⊢ n + 3 = 2 → φ (n + 3) = 1
rintro ⟨⟩