-- Mathlib/Data/Nat/Totient.lean
theorem totient_div_of_dvd {n d : ℕ} (hnd : d ∣ n) :
    φ (n / d) = #{k ∈ range n | n.gcd k = d}

Proof state:
case inr.intro.hi
d : ℕ
hd0 : d > 0
x : ℕ
⊢ ∀ a < x, x.gcd a = 1 → d * a < d * x ∧ (d * x).gcd (d * a) = d

Tactic:
refine fun a ha1 ha2 => ⟨(mul_lt_mul_left hd0).2 ha1, ?_⟩

Result:
case inr.intro.hi
d : ℕ
hd0 : d > 0
x a : ℕ
ha1 : a < x
ha2 : x.gcd a = 1
⊢ (d * x).gcd (d * a) = d

Proof state:
n d : ℕ
hnd : d ∣ n
⊢ φ (n / d) = #(filter (fun k => n.gcd k = d) (range n))

Tactic:
rcases d.eq_zero_or_pos with (rfl | hd0)

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

case inr
n d : ℕ
hnd : d ∣ n
hd0 : d > 0
⊢ φ (n / d) = #(filter (fun k => n.gcd k = d) (range n))

Proof state:
case inr
n d : ℕ
hnd : d ∣ n
hd0 : d > 0
⊢ φ (n / d) = #(filter (fun k => n.gcd k = d) (range n))

Tactic:
rcases hnd with ⟨x, rfl⟩

Result:
case inr.intro
d : ℕ
hd0 : d > 0
x : ℕ
⊢ φ (d * x / d) = #(filter (fun k => (d * x).gcd k = d) (range (d * x)))

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

Tactic:
simp [eq_zero_of_zero_dvd hnd]

Result:
no goals

Proof state:
case inr.intro
d : ℕ
hd0 : d > 0
x : ℕ
⊢ φ (d * x / d) = #(filter (fun k => (d * x).gcd k = d) (range (d * x)))

Tactic:
rw [Nat.mul_div_cancel_left x hd0]

Result:
case inr.intro
d : ℕ
hd0 : d > 0
x : ℕ
⊢ φ x = #(filter (fun k => (d * x).gcd k = d) (range (d * x)))

Proof state:
case inr.intro.i_surj.intro
d : ℕ
hd0 : d > 0
x q : ℕ
hb1 : d * q < d * x
hb2 : (d * x).gcd (d * q) = d
⊢ x.Coprime q

Tactic:
rwa [gcd_mul_left, mul_right_eq_self_iff hd0] at hb2

Result:
no goals

Proof state:
case inr.intro.i_surj
d : ℕ
hd0 : d > 0
x b : ℕ
hb1 : b < d * x
hb2 : (d * x).gcd b = d
this : d ∣ b
⊢ ∃ a, (a < x ∧ x.Coprime a) ∧ d * a = b

Tactic:
rcases this with ⟨q, rfl⟩

Result:
case inr.intro.i_surj.intro
d : ℕ
hd0 : d > 0
x q : ℕ
hb1 : d * q < d * x
hb2 : (d * x).gcd (d * q) = d
⊢ ∃ a, (a < x ∧ x.Coprime a) ∧ d * a = d * q

Proof state:
case inr.intro.hi
d : ℕ
hd0 : d > 0
x : ℕ
⊢ ∀ a ∈ filter (fun a => x.Coprime a) (range x), d * a ∈ filter (fun k => (d * x).gcd k = d) (range (d * x))

Tactic:
simp only [mem_filter, mem_range, and_imp, Coprime]

Result:
case inr.intro.hi
d : ℕ
hd0 : d > 0
x : ℕ
⊢ ∀ a < x, x.gcd a = 1 → d * a < d * x ∧ (d * x).gcd (d * a) = d

Proof state:
case inr.intro.hi
d : ℕ
hd0 : d > 0
x a : ℕ
ha1 : a < x
ha2 : x.gcd a = 1
⊢ (d * x).gcd (d * a) = d

Tactic:
rw [gcd_mul_left, ha2, mul_one]

Result:
no goals

Proof state:
d : ℕ
hd0 : d > 0
x b : ℕ
hb1 : b < d * x
hb2 : (d * x).gcd b = d
⊢ d ∣ b

Tactic:
rw [← hb2]

Result:
d : ℕ
hd0 : d > 0
x b : ℕ
hb1 : b < d * x
hb2 : (d * x).gcd b = d
⊢ (d * x).gcd b ∣ b

Proof state:
d : ℕ
hd0 : d > 0
x b : ℕ
hb1 : b < d * x
hb2 : (d * x).gcd b = d
⊢ (d * x).gcd b ∣ b

Tactic:
apply gcd_dvd_right

Result:
no goals

Proof state:
case inr.intro.i_inj
d : ℕ
hd0 : d > 0
x : ℕ
⊢ ∀ a₁ ∈ filter (fun a => x.Coprime a) (range x),
    ∀ a₂ ∈ filter (fun a => x.Coprime a) (range x), d * a₁ = d * a₂ → a₁ = a₂

Tactic:
simp [hd0.ne']

Result:
no goals

Proof state:
case inr.intro.i_surj
d : ℕ
hd0 : d > 0
x : ℕ
⊢ ∀ b < d * x, (d * x).gcd b = d → ∃ a, (a < x ∧ x.Coprime a) ∧ d * a = b

Tactic:
refine fun b hb1 hb2 => ?_

Result:
case inr.intro.i_surj
d : ℕ
hd0 : d > 0
x b : ℕ
hb1 : b < d * x
hb2 : (d * x).gcd b = d
⊢ ∃ a, (a < x ∧ x.Coprime a) ∧ d * a = b

Proof state:
case inr.intro.i_surj
d : ℕ
hd0 : d > 0
x b : ℕ
hb1 : b < d * x
hb2 : (d * x).gcd b = d
⊢ ∃ a, (a < x ∧ x.Coprime a) ∧ d * a = b

Tactic:
have : d ∣ b := by
  rw [← hb2]
  apply gcd_dvd_right

Result:
case inr.intro.i_surj
d : ℕ
hd0 : d > 0
x b : ℕ
hb1 : b < d * x
hb2 : (d * x).gcd b = d
this : d ∣ b
⊢ ∃ a, (a < x ∧ x.Coprime a) ∧ d * a = b

Proof state:
case inr.intro
d : ℕ
hd0 : d > 0
x : ℕ
⊢ φ x = #(filter (fun k => (d * x).gcd k = d) (range (d * x)))

Tactic:
apply Finset.card_bij fun k _ => d * k

Result:
case inr.intro.hi
d : ℕ
hd0 : d > 0
x : ℕ
⊢ ∀ a ∈ filter (fun a => x.Coprime a) (range x), d * a ∈ filter (fun k => (d * x).gcd k = d) (range (d * x))

case inr.intro.i_inj
d : ℕ
hd0 : d > 0
x : ℕ
⊢ ∀ a₁ ∈ filter (fun a => x.Coprime a) (range x),
    ∀ a₂ ∈ filter (fun a => x.Coprime a) (range x), d * a₁ = d * a₂ → a₁ = a₂

case inr.intro.i_surj
d : ℕ
hd0 : d > 0
x : ℕ
⊢ ∀ b ∈ filter (fun k => (d * x).gcd k = d) (range (d * x)),
    ∃ a, ∃ (_ : a ∈ filter (fun a => x.Coprime a) (range x)), d * a = b

Proof state:
case inr.intro.i_surj
d : ℕ
hd0 : d > 0
x : ℕ
⊢ ∀ b ∈ filter (fun k => (d * x).gcd k = d) (range (d * x)),
    ∃ a, ∃ (_ : a ∈ filter (fun a => x.Coprime a) (range x)), d * a = b

Tactic:
simp only [mem_filter, mem_range, exists_prop, and_imp]

Result:
case inr.intro.i_surj
d : ℕ
hd0 : d > 0
x : ℕ
⊢ ∀ b < d * x, (d * x).gcd b = d → ∃ a, (a < x ∧ x.Coprime a) ∧ d * a = b

Proof state:
case inr.intro.i_surj.intro
d : ℕ
hd0 : d > 0
x q : ℕ
hb1 : d * q < d * x
hb2 : (d * x).gcd (d * q) = d
⊢ ∃ a, (a < x ∧ x.Coprime a) ∧ d * a = d * q

Tactic:
refine ⟨q, ⟨⟨(mul_lt_mul_left hd0).1 hb1, ?_⟩, rfl⟩⟩

Result:
case inr.intro.i_surj.intro
d : ℕ
hd0 : d > 0
x q : ℕ
hb1 : d * q < d * x
hb2 : (d * x).gcd (d * q) = d
⊢ x.Coprime q