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) = PartENat.card α
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}ᶜ) = PartENat.card α

State before:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
⊢ 1 + ↑(Set.encard {a}ᶜ) = PartENat.card α
Tactic:
rw [← Nat.cast_one]
State after:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
⊢ ↑1 + ↑(Set.encard {a}ᶜ) = PartENat.card α

State before:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
⊢ ↑1 + ↑(Set.encard {a}ᶜ) = PartENat.card α
Tactic:
apply PartENat.withTopAddEquiv.injective
State after:
case a
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
⊢ PartENat.withTopAddEquiv (↑1 + ↑(Set.encard {a}ᶜ)) = PartENat.withTopAddEquiv (PartENat.card α)

State before:
case a
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
⊢ PartENat.withTopAddEquiv (↑1 + ↑(Set.encard {a}ᶜ)) = PartENat.withTopAddEquiv (PartENat.card α)
Tactic:
rw [map_add]
State after:
case a
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
⊢ PartENat.withTopAddEquiv ↑1 + PartENat.withTopAddEquiv ↑(Set.encard {a}ᶜ) = PartENat.withTopAddEquiv (PartENat.card α)

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

case h.e'_2.h.e'_6
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
⊢ PartENat.withTopAddEquiv ↑(Set.encard {a}ᶜ) = Set.encard {a}ᶜ

case h.e'_3
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
⊢ PartENat.withTopAddEquiv (PartENat.card α) = Set.encard Set.univ

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

State before:
case h.e'_2.h.e'_5
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
⊢ PartENat.withTopAddEquiv ↑1 = 1
Tactic:
apply PartENat.toWithTop_natCast'
State after:
no goals

State before:
case h.e'_2.h.e'_6
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
⊢ PartENat.withTopAddEquiv ↑(Set.encard {a}ᶜ) = Set.encard {a}ᶜ
Tactic:
rw [← AddEquiv.eq_symm_apply]
State after:
case h.e'_2.h.e'_6
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
⊢ ↑(Set.encard {a}ᶜ) = (AddEquiv.symm PartENat.withTopAddEquiv) (Set.encard {a}ᶜ)

State before:
case h.e'_2.h.e'_6
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
⊢ ↑(Set.encard {a}ᶜ) = (AddEquiv.symm PartENat.withTopAddEquiv) (Set.encard {a}ᶜ)
Tactic:
rfl
State after:
no goals

State before:
case h.e'_3
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
⊢ PartENat.withTopAddEquiv (PartENat.card α) = Set.encard Set.univ
Tactic:
convert (Set.encard_univ α).symm
State after:
no goals