Theorem: SubMulAction.add_encard_ofStabilizer_eq' (Jordan/Jordan.lean)

State before:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
⊢ 1 + Set.encard (SubMulAction.ofStabilizer G a).carrier = Set.encard Set.univ
Tactic:
rw [SubMulAction.ofStabilizer_carrier]
State after:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
⊢ 1 + Set.encard {a}ᶜ = Set.encard Set.univ

State before:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
⊢ 1 + Set.encard {a}ᶜ = Set.encard Set.univ
Tactic:
convert Set.encard_add_encard_compl _
State after:
case h.e'_2.h.e'_5
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
⊢ 1 = Set.encard {a}

State before:
case h.e'_2.h.e'_5
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
⊢ 1 = Set.encard {a}
Tactic:
simp only [Set.encard_singleton]
State after:
no goals