-- Mathlib/Topology/Instances/AddCircle.lean
theorem card_addOrderOf_eq_totient {n : ℕ} :
    Nat.card { u : AddCircle p // addOrderOf u = n } = n.totient

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
n : ℕ
⊢ Nat.card { u // addOrderOf u = n } = n.totient

Tactic:
rcases n.eq_zero_or_pos with (rfl | hn)

Result:
case inl
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
⊢ Nat.card { u // addOrderOf u = 0 } = Nat.totient 0

case inr
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
n : ℕ
hn : n > 0
⊢ Nat.card { u // addOrderOf u = n } = n.totient

Proof state:
case inl.inr
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
h : ¬∃ u, ¬IsOfFinAddOrder u
this : IsEmpty { u // ¬IsOfFinAddOrder u }
⊢ Nat.card { u // ¬IsOfFinAddOrder u } = 0

Tactic:
exact Nat.card_of_isEmpty

Result:
no goals

Proof state:
case inl.inr
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
h : ¬∃ u, ¬IsOfFinAddOrder u
⊢ Nat.card { u // ¬IsOfFinAddOrder u } = 0

Tactic:
have : IsEmpty { u : AddCircle p // ¬IsOfFinAddOrder u } := by simpa [isEmpty_subtype] using h

Result:
case inl.inr
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
h : ¬∃ u, ¬IsOfFinAddOrder u
this : IsEmpty { u // ¬IsOfFinAddOrder u }
⊢ Nat.card { u // ¬IsOfFinAddOrder u } = 0

Proof state:
case inr
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
n : ℕ
hn : n > 0
⊢ Nat.card { u // addOrderOf u = n } = n.totient

Tactic:
rw [← coe_setOf, Nat.card_congr (setAddOrderOfEquiv p hn),
  n.totient_eq_card_lt_and_coprime]

Result:
case inr
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
n : ℕ
hn : n > 0
⊢ Nat.card ↑{m | m < n ∧ m.gcd n = 1} = Nat.card ↑{m | m < n ∧ n.Coprime m}

Proof state:
case inl.inl.intro
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
u : AddCircle p
hu : ¬IsOfFinAddOrder u
this : Infinite { u // ¬IsOfFinAddOrder u }
⊢ Nat.card { u // ¬IsOfFinAddOrder u } = 0

Tactic:
exact Nat.card_eq_zero_of_infinite

Result:
no goals

Proof state:
case inr
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
n : ℕ
hn : n > 0
⊢ Nat.card ↑{m | m < n ∧ m.gcd n = 1} = Nat.card ↑{m | m < n ∧ n.Coprime m}

Tactic:
simp only [Nat.gcd_comm]

Result:
no goals

Proof state:
case inl
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
⊢ Nat.card { u // addOrderOf u = 0 } = Nat.totient 0

Tactic:
simp only [Nat.totient_zero, addOrderOf_eq_zero_iff]

Result:
case inl
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
⊢ Nat.card { u // ¬IsOfFinAddOrder u } = 0

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
u : AddCircle p
hu : ¬IsOfFinAddOrder u
⊢ Infinite { u // ¬IsOfFinAddOrder u }

Tactic:
erw [infinite_coe_iff]

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
u : AddCircle p
hu : ¬IsOfFinAddOrder u
⊢ Set.Infinite fun u => IsOfFinAddOrder u → False

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
u : AddCircle p
hu : ¬IsOfFinAddOrder u
⊢ Set.Infinite fun u => IsOfFinAddOrder u → False

Tactic:
exact infinite_not_isOfFinAddOrder hu

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
h : ¬∃ u, ¬IsOfFinAddOrder u
⊢ IsEmpty { u // ¬IsOfFinAddOrder u }

Tactic:
simpa [isEmpty_subtype] using h

Result:
no goals

Proof state:
case inl
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
⊢ Nat.card { u // ¬IsOfFinAddOrder u } = 0

Tactic:
rcases em (∃ u : AddCircle p, ¬IsOfFinAddOrder u) with (⟨u, hu⟩ | h)

Result:
case inl.inl.intro
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
u : AddCircle p
hu : ¬IsOfFinAddOrder u
⊢ Nat.card { u // ¬IsOfFinAddOrder u } = 0

case inl.inr
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
h : ¬∃ u, ¬IsOfFinAddOrder u
⊢ Nat.card { u // ¬IsOfFinAddOrder u } = 0

Proof state:
case inl.inl.intro
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
u : AddCircle p
hu : ¬IsOfFinAddOrder u
⊢ Nat.card { u // ¬IsOfFinAddOrder u } = 0

Tactic:
have : Infinite { u : AddCircle p // ¬IsOfFinAddOrder u } := by
  erw [infinite_coe_iff]
  exact infinite_not_isOfFinAddOrder hu

Result:
case inl.inl.intro
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
u : AddCircle p
hu : ¬IsOfFinAddOrder u
this : Infinite { u // ¬IsOfFinAddOrder u }
⊢ Nat.card { u // ¬IsOfFinAddOrder u } = 0