Theorem: SubMulAction.add_card_ofStabilizer_eq (Jordan/SubMulActions.lean)

State before:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
⊢ 1 + PartENat.card ↥(ofStabilizer M a) = PartENat.card α
Tactic:
unfold PartENat.card
State after:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
⊢ 1 + Cardinal.toPartENat (Cardinal.mk ↥(ofStabilizer M a)) = Cardinal.toPartENat (Cardinal.mk α)

State before:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
⊢ 1 + Cardinal.toPartENat (Cardinal.mk ↥(ofStabilizer M a)) = Cardinal.toPartENat (Cardinal.mk α)
Tactic:
rw [← Cardinal.mk_sum_compl {a}, map_add]
State after:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
⊢ 1 + Cardinal.toPartENat (Cardinal.mk ↥(ofStabilizer M a)) =
    Cardinal.toPartENat (Cardinal.mk ↑{a}) + Cardinal.toPartENat (Cardinal.mk ↑{a}ᶜ)

State before:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
⊢ 1 + Cardinal.toPartENat (Cardinal.mk ↥(ofStabilizer M a)) =
    Cardinal.toPartENat (Cardinal.mk ↑{a}) + Cardinal.toPartENat (Cardinal.mk ↑{a}ᶜ)
Tactic:
congr
State after:
case e_a
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
⊢ 1 = Cardinal.toPartENat (Cardinal.mk ↑{a})

State before:
case e_a
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
⊢ 1 = Cardinal.toPartENat (Cardinal.mk ↑{a})
Tactic:
simp only [Cardinal.mk_fintype, Fintype.card_ofSubsingleton, Nat.cast_one]
State after:
case e_a
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
⊢ 1 = Cardinal.toPartENat 1

State before:
case e_a
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
⊢ 1 = Cardinal.toPartENat 1
Tactic:
conv_lhs => rw [← Nat.cast_one]
State after:
case e_a
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
⊢ ↑1 = Cardinal.toPartENat 1

State before:
case e_a
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
⊢ ↑1 = Cardinal.toPartENat 1
Tactic:
apply symm
State after:
case e_a.a
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
⊢ Cardinal.toPartENat 1 = ↑1

State before:
case e_a.a
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
⊢ Cardinal.toPartENat 1 = ↑1
Tactic:
exact Iff.mpr Cardinal.toPartENat_eq_natCast_iff rfl
State after:
no goals