case inl
n : ℕ
hnd : 0 ∣ n
⊢ φ (n / 0) = Finset.card (filter (fun k => gcd n k = 0) (range n))

case inr
n d : ℕ
hnd : d ∣ n
hd0 : d > 0
⊢ φ (n / d) = Finset.card (filter (fun k => gcd n k = d) (range n))
n d : ℕ
hnd : d ∣ n
⊢ φ (n / d) = Finset.card (filter (fun k => gcd n k = d) (range n))
rcases d.eq_zero_or_pos with (rfl | hd0)
case inr.intro
d : ℕ
hd0 : d > 0
x : ℕ
⊢ φ (d * x / d) = Finset.card (filter (fun k => gcd (d * x) k = d) (range (d * x)))
case inr
n d : ℕ
hnd : d ∣ n
hd0 : d > 0
⊢ φ (n / d) = Finset.card (filter (fun k => gcd n k = d) (range n))
rcases hnd with ⟨x, rfl⟩
case inr.intro
d : ℕ
hd0 : d > 0
x : ℕ
⊢ φ x = Finset.card (filter (fun k => gcd (d * x) k = d) (range (d * x)))
case inr.intro
d : ℕ
hd0 : d > 0
x : ℕ
⊢ φ (d * x / d) = Finset.card (filter (fun k => gcd (d * x) k = d) (range (d * x)))
rw [Nat.mul_div_cancel_left x hd0]
case inr.intro.h₁
d : ℕ
hd0 : d > 0
x : ℕ
⊢ ∀ (a : ℕ), a ∈ filter (coprime x) (range x) → d * a ∈ filter (fun k => gcd (d * x) k = d) (range (d * x))

case inr.intro.h₂
d : ℕ
hd0 : d > 0
x : ℕ
⊢ ∀ (a b : ℕ), a ∈ filter (coprime x) (range x) → b ∈ filter (coprime x) (range x) → d * a = d * b → a = b

case inr.intro.h₃
d : ℕ
hd0 : d > 0
x : ℕ
⊢ ∀ (b : ℕ), b ∈ filter (fun k => gcd (d * x) k = d) (range (d * x)) → ∃ a ha, d * a = b
case inr.intro
d : ℕ
hd0 : d > 0
x : ℕ
⊢ φ x = Finset.card (filter (fun k => gcd (d * x) k = d) (range (d * x)))
apply Finset.card_congr fun k _ => d * k
no goals
case inl
n : ℕ
hnd : 0 ∣ n
⊢ φ (n / 0) = Finset.card (filter (fun k => gcd n k = 0) (range n))
simp [eq_zero_of_zero_dvd hnd]
case inr.intro.h₁
d : ℕ
hd0 : d > 0
x : ℕ
⊢ ∀ (a : ℕ), a < x → gcd x a = 1 → d * a < d * x ∧ gcd (d * x) (d * a) = d
case inr.intro.h₁
d : ℕ
hd0 : d > 0
x : ℕ
⊢ ∀ (a : ℕ), a ∈ filter (coprime x) (range x) → d * a ∈ filter (fun k => gcd (d * x) k = d) (range (d * x))
simp only [mem_filter, mem_range, and_imp, coprime]
case inr.intro.h₁
d : ℕ
hd0 : d > 0
x a : ℕ
ha1 : a < x
ha2 : gcd x a = 1
⊢ gcd (d * x) (d * a) = d
case inr.intro.h₁
d : ℕ
hd0 : d > 0
x : ℕ
⊢ ∀ (a : ℕ), a < x → gcd x a = 1 → d * a < d * x ∧ gcd (d * x) (d * a) = d
refine' fun a ha1 ha2 => ⟨(mul_lt_mul_left hd0).2 ha1, _⟩
no goals
case inr.intro.h₁
d : ℕ
hd0 : d > 0
x a : ℕ
ha1 : a < x
ha2 : gcd x a = 1
⊢ gcd (d * x) (d * a) = d
rw [gcd_mul_left, ha2, mul_one]
no goals
case inr.intro.h₂
d : ℕ
hd0 : d > 0
x : ℕ
⊢ ∀ (a b : ℕ), a ∈ filter (coprime x) (range x) → b ∈ filter (coprime x) (range x) → d * a = d * b → a = b
simp [hd0.ne']
case inr.intro.h₃
d : ℕ
hd0 : d > 0
x : ℕ
⊢ ∀ (b : ℕ), b < d * x → gcd (d * x) b = d → ∃ a, (a < x ∧ coprime x a) ∧ d * a = b
case inr.intro.h₃
d : ℕ
hd0 : d > 0
x : ℕ
⊢ ∀ (b : ℕ), b ∈ filter (fun k => gcd (d * x) k = d) (range (d * x)) → ∃ a ha, d * a = b
simp only [mem_filter, mem_range, exists_prop, and_imp]
case inr.intro.h₃
d : ℕ
hd0 : d > 0
x b : ℕ
hb1 : b < d * x
hb2 : gcd (d * x) b = d
⊢ ∃ a, (a < x ∧ coprime x a) ∧ d * a = b
case inr.intro.h₃
d : ℕ
hd0 : d > 0
x : ℕ
⊢ ∀ (b : ℕ), b < d * x → gcd (d * x) b = d → ∃ a, (a < x ∧ coprime x a) ∧ d * a = b
refine' fun b hb1 hb2 => _
case inr.intro.h₃
d : ℕ
hd0 : d > 0
x b : ℕ
hb1 : b < d * x
hb2 : gcd (d * x) b = d
this : d ∣ b
⊢ ∃ a, (a < x ∧ coprime x a) ∧ d * a = b
case inr.intro.h₃
d : ℕ
hd0 : d > 0
x b : ℕ
hb1 : b < d * x
hb2 : gcd (d * x) b = d
⊢ ∃ a, (a < x ∧ coprime x a) ∧ d * a = b
have : d ∣ b := by
  rw [← hb2]
  apply gcd_dvd_right
case inr.intro.h₃.intro
d : ℕ
hd0 : d > 0
x q : ℕ
hb1 : d * q < d * x
hb2 : gcd (d * x) (d * q) = d
⊢ ∃ a, (a < x ∧ coprime x a) ∧ d * a = d * q
case inr.intro.h₃
d : ℕ
hd0 : d > 0
x b : ℕ
hb1 : b < d * x
hb2 : gcd (d * x) b = d
this : d ∣ b
⊢ ∃ a, (a < x ∧ coprime x a) ∧ d * a = b
rcases this with ⟨q, rfl⟩
case inr.intro.h₃.intro
d : ℕ
hd0 : d > 0
x q : ℕ
hb1 : d * q < d * x
hb2 : gcd (d * x) (d * q) = d
⊢ coprime x q
case inr.intro.h₃.intro
d : ℕ
hd0 : d > 0
x q : ℕ
hb1 : d * q < d * x
hb2 : gcd (d * x) (d * q) = d
⊢ ∃ a, (a < x ∧ coprime x a) ∧ d * a = d * q
refine' ⟨q, ⟨⟨(mul_lt_mul_left hd0).1 hb1, _⟩, rfl⟩⟩
no goals
case inr.intro.h₃.intro
d : ℕ
hd0 : d > 0
x q : ℕ
hb1 : d * q < d * x
hb2 : gcd (d * x) (d * q) = d
⊢ coprime x q
rwa [gcd_mul_left, mul_right_eq_self_iff hd0] at hb2
d : ℕ
hd0 : d > 0
x b : ℕ
hb1 : b < d * x
hb2 : gcd (d * x) b = d
⊢ gcd (d * x) b ∣ b
d : ℕ
hd0 : d > 0
x b : ℕ
hb1 : b < d * x
hb2 : gcd (d * x) b = d
⊢ d ∣ b
rw [← hb2]
no goals
d : ℕ
hd0 : d > 0
x b : ℕ
hb1 : b < d * x
hb2 : gcd (d * x) b = d
⊢ gcd (d * x) b ∣ b
apply gcd_dvd_right