case inl
𝕜 : Type u_1
B : Type ?u.287307
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
⊢ Nat.card { u // addOrderOf u = 0 } = Nat.totient 0

case inr
𝕜 : Type u_1
B : Type ?u.287307
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n : ℕ
hn : n > 0
⊢ Nat.card { u // addOrderOf u = n } = Nat.totient n
𝕜 : Type u_1
B : Type ?u.287307
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n : ℕ
⊢ Nat.card { u // addOrderOf u = n } = Nat.totient n
rcases n.eq_zero_or_pos with (rfl | hn)
case inl
𝕜 : Type u_1
B : Type ?u.287307
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
⊢ Nat.card { u // ¬IsOfFinAddOrder u } = 0
case inl
𝕜 : Type u_1
B : Type ?u.287307
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
⊢ Nat.card { u // addOrderOf u = 0 } = Nat.totient 0
simp only [Nat.totient_zero, addOrderOf_eq_zero_iff]
case inl.inl.intro
𝕜 : Type u_1
B : Type ?u.287307
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
u : AddCircle p
hu : ¬IsOfFinAddOrder u
⊢ Nat.card { u // ¬IsOfFinAddOrder u } = 0

case inl.inr
𝕜 : Type u_1
B : Type ?u.287307
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
h : ¬∃ u, ¬IsOfFinAddOrder u
⊢ Nat.card { u // ¬IsOfFinAddOrder u } = 0
case inl
𝕜 : Type u_1
B : Type ?u.287307
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
⊢ Nat.card { u // ¬IsOfFinAddOrder u } = 0
rcases em (∃ u : AddCircle p, ¬IsOfFinAddOrder u) with (⟨u, hu⟩ | h)
case inl.inl.intro
𝕜 : Type u_1
B : Type ?u.287307
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
u : AddCircle p
hu : ¬IsOfFinAddOrder u
this : Infinite { u // ¬IsOfFinAddOrder u }
⊢ Nat.card { u // ¬IsOfFinAddOrder u } = 0
case inl.inl.intro
𝕜 : Type u_1
B : Type ?u.287307
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
u : AddCircle p
hu : ¬IsOfFinAddOrder u
⊢ Nat.card { u // ¬IsOfFinAddOrder u } = 0
have : Infinite { u : AddCircle p // ¬IsOfFinAddOrder u } := by
  erw [infinite_coe_iff]
  exact infinite_not_isOfFinAddOrder hu
no goals
case inl.inl.intro
𝕜 : Type u_1
B : Type ?u.287307
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
u : AddCircle p
hu : ¬IsOfFinAddOrder u
this : Infinite { u // ¬IsOfFinAddOrder u }
⊢ Nat.card { u // ¬IsOfFinAddOrder u } = 0
exact Nat.card_eq_zero_of_infinite
𝕜 : Type u_1
B : Type ?u.287307
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
u : AddCircle p
hu : ¬IsOfFinAddOrder u
⊢ Set.Infinite fun u => IsOfFinAddOrder u → False
𝕜 : Type u_1
B : Type ?u.287307
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
u : AddCircle p
hu : ¬IsOfFinAddOrder u
⊢ Infinite { u // ¬IsOfFinAddOrder u }
erw [infinite_coe_iff]
no goals
𝕜 : Type u_1
B : Type ?u.287307
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
u : AddCircle p
hu : ¬IsOfFinAddOrder u
⊢ Set.Infinite fun u => IsOfFinAddOrder u → False
exact infinite_not_isOfFinAddOrder hu
case inl.inr
𝕜 : Type u_1
B : Type ?u.287307
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
h : ¬∃ u, ¬IsOfFinAddOrder u
this : IsEmpty { u // ¬IsOfFinAddOrder u }
⊢ Nat.card { u // ¬IsOfFinAddOrder u } = 0
case inl.inr
𝕜 : Type u_1
B : Type ?u.287307
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
h : ¬∃ u, ¬IsOfFinAddOrder u
⊢ Nat.card { u // ¬IsOfFinAddOrder u } = 0
have : IsEmpty { u : AddCircle p // ¬IsOfFinAddOrder u } := by simpa using h
no goals
case inl.inr
𝕜 : Type u_1
B : Type ?u.287307
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
h : ¬∃ u, ¬IsOfFinAddOrder u
this : IsEmpty { u // ¬IsOfFinAddOrder u }
⊢ Nat.card { u // ¬IsOfFinAddOrder u } = 0
exact Nat.card_of_isEmpty
no goals
𝕜 : Type u_1
B : Type ?u.287307
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
h : ¬∃ u, ¬IsOfFinAddOrder u
⊢ IsEmpty { u // ¬IsOfFinAddOrder u }
simpa using h
case inr
𝕜 : Type u_1
B : Type ?u.287307
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n : ℕ
hn : n > 0
⊢ Nat.card ↑{m | m < n ∧ Nat.gcd m n = 1} = Nat.card ↑{m | m < n ∧ Nat.coprime n m}
case inr
𝕜 : Type u_1
B : Type ?u.287307
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n : ℕ
hn : n > 0
⊢ Nat.card { u // addOrderOf u = n } = Nat.totient n
rw [← coe_setOf, Nat.card_congr (setAddOrderOfEquiv p hn),
  n.totient_eq_card_lt_and_coprime]
no goals
case inr
𝕜 : Type u_1
B : Type ?u.287307
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n : ℕ
hn : n > 0
⊢ Nat.card ↑{m | m < n ∧ Nat.gcd m n = 1} = Nat.card ↑{m | m < n ∧ Nat.coprime n m}
simp only [Nat.gcd_comm]