Theorem: Finset.card_mulStab_dvd_card_mulStab (LeanCamCombi/Kneser/MulStab.lean)

State before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
h : s.mulStab ⊆ t.mulStab
⊢ s.mulStab.card ∣ t.mulStab.card
Tactic:
obtain rfl | ht := t.eq_empty_or_nonempty
State after:
case inl
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s : Finset α
a : α
hs : s.Nonempty
h : s.mulStab ⊆ ∅.mulStab
⊢ s.mulStab.card ∣ ∅.mulStab.card

case inr
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
h : s.mulStab ⊆ t.mulStab
ht : t.Nonempty
⊢ s.mulStab.card ∣ t.mulStab.card

State before:
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
h : s.mulStab ⊆ t.mulStab
ht : t.Nonempty
⊢ s.mulStab.card ∣ t.mulStab.card
Tactic:
rw [← coe_subset, coe_mulStab hs, coe_mulStab ht, SetLike.coe_subset_coe] at h
State after:
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
h : stabilizer α s ≤ stabilizer α t
ht : t.Nonempty
⊢ s.mulStab.card ∣ t.mulStab.card

State before:
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
h : stabilizer α s ≤ stabilizer α t
ht : t.Nonempty
⊢ s.mulStab.card ∣ t.mulStab.card
Tactic:
letI : Fintype (stabilizer α s) := fintypeStabilizerOfMulStab hs
State after:
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
h : stabilizer α s ≤ stabilizer α t
ht : t.Nonempty
this : Fintype ↥(stabilizer α s) := Finset.fintypeStabilizerOfMulStab hs
⊢ s.mulStab.card ∣ t.mulStab.card

State before:
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
h : stabilizer α s ≤ stabilizer α t
ht : t.Nonempty
this : Fintype ↥(stabilizer α s) := Finset.fintypeStabilizerOfMulStab hs
⊢ s.mulStab.card ∣ t.mulStab.card
Tactic:
letI : Fintype (stabilizer α t) := fintypeStabilizerOfMulStab ht
State after:
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
h : stabilizer α s ≤ stabilizer α t
ht : t.Nonempty
this✝ : Fintype ↥(stabilizer α s) := Finset.fintypeStabilizerOfMulStab hs
this : Fintype ↥(stabilizer α t) := Finset.fintypeStabilizerOfMulStab ht
⊢ s.mulStab.card ∣ t.mulStab.card

State before:
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
h : stabilizer α s ≤ stabilizer α t
ht : t.Nonempty
this✝ : Fintype ↥(stabilizer α s) := Finset.fintypeStabilizerOfMulStab hs
this : Fintype ↥(stabilizer α t) := Finset.fintypeStabilizerOfMulStab ht
⊢ s.mulStab.card ∣ t.mulStab.card
Tactic:
convert Subgroup.card_dvd_of_le h using 1
State after:
case h.e'_3
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
h : stabilizer α s ≤ stabilizer α t
ht : t.Nonempty
this✝ : Fintype ↥(stabilizer α s) := Finset.fintypeStabilizerOfMulStab hs
this : Fintype ↥(stabilizer α t) := Finset.fintypeStabilizerOfMulStab ht
⊢ s.mulStab.card = Nat.card ↥(stabilizer α s)

case h.e'_4
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
h : stabilizer α s ≤ stabilizer α t
ht : t.Nonempty
this✝ : Fintype ↥(stabilizer α s) := Finset.fintypeStabilizerOfMulStab hs
this : Fintype ↥(stabilizer α t) := Finset.fintypeStabilizerOfMulStab ht
⊢ t.mulStab.card = Nat.card ↥(stabilizer α t)

State before:
case h.e'_3
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
h : stabilizer α s ≤ stabilizer α t
ht : t.Nonempty
this✝ : Fintype ↥(stabilizer α s) := Finset.fintypeStabilizerOfMulStab hs
this : Fintype ↥(stabilizer α t) := Finset.fintypeStabilizerOfMulStab ht
⊢ s.mulStab.card = Nat.card ↥(stabilizer α s)

case h.e'_4
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
h : stabilizer α s ≤ stabilizer α t
ht : t.Nonempty
this✝ : Fintype ↥(stabilizer α s) := Finset.fintypeStabilizerOfMulStab hs
this : Fintype ↥(stabilizer α t) := Finset.fintypeStabilizerOfMulStab ht
⊢ t.mulStab.card = Nat.card ↥(stabilizer α t)
Tactic:
simp [-mem_stabilizer_iff]
State after:
case h.e'_3
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
h : stabilizer α s ≤ stabilizer α t
ht : t.Nonempty
this✝ : Fintype ↥(stabilizer α s) := Finset.fintypeStabilizerOfMulStab hs
this : Fintype ↥(stabilizer α t) := Finset.fintypeStabilizerOfMulStab ht
⊢ s.mulStab.card = Fintype.card ↥(stabilizer α s)

case h.e'_4
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
h : stabilizer α s ≤ stabilizer α t
ht : t.Nonempty
this✝ : Fintype ↥(stabilizer α s) := Finset.fintypeStabilizerOfMulStab hs
this : Fintype ↥(stabilizer α t) := Finset.fintypeStabilizerOfMulStab ht
⊢ t.mulStab.card = Nat.card ↥(stabilizer α t)

State before:
case h.e'_3
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
h : stabilizer α s ≤ stabilizer α t
ht : t.Nonempty
this✝ : Fintype ↥(stabilizer α s) := Finset.fintypeStabilizerOfMulStab hs
this : Fintype ↥(stabilizer α t) := Finset.fintypeStabilizerOfMulStab ht
⊢ s.mulStab.card = Fintype.card ↥(stabilizer α s)

case h.e'_4
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
h : stabilizer α s ≤ stabilizer α t
ht : t.Nonempty
this✝ : Fintype ↥(stabilizer α s) := Finset.fintypeStabilizerOfMulStab hs
this : Fintype ↥(stabilizer α t) := Finset.fintypeStabilizerOfMulStab ht
⊢ t.mulStab.card = Nat.card ↥(stabilizer α t)
Tactic:
change _ = (s.mulStab.attach.map
  ⟨Subtype.map id fun _ ↦ (mem_mulStab hs).1, Subtype.map_injective _ injective_id⟩).card
State after:
case h.e'_3
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
h : stabilizer α s ≤ stabilizer α t
ht : t.Nonempty
this✝ : Fintype ↥(stabilizer α s) := Finset.fintypeStabilizerOfMulStab hs
this : Fintype ↥(stabilizer α t) := Finset.fintypeStabilizerOfMulStab ht
⊢ s.mulStab.card = (map { toFun := Subtype.map id ⋯, inj' := ⋯ } s.mulStab.attach).card

case h.e'_4
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
h : stabilizer α s ≤ stabilizer α t
ht : t.Nonempty
this✝ : Fintype ↥(stabilizer α s) := Finset.fintypeStabilizerOfMulStab hs
this : Fintype ↥(stabilizer α t) := Finset.fintypeStabilizerOfMulStab ht
⊢ t.mulStab.card = Nat.card ↥(stabilizer α t)

State before:
case h.e'_3
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
h : stabilizer α s ≤ stabilizer α t
ht : t.Nonempty
this✝ : Fintype ↥(stabilizer α s) := Finset.fintypeStabilizerOfMulStab hs
this : Fintype ↥(stabilizer α t) := Finset.fintypeStabilizerOfMulStab ht
⊢ s.mulStab.card = (map { toFun := Subtype.map id ⋯, inj' := ⋯ } s.mulStab.attach).card

case h.e'_4
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
h : stabilizer α s ≤ stabilizer α t
ht : t.Nonempty
this✝ : Fintype ↥(stabilizer α s) := Finset.fintypeStabilizerOfMulStab hs
this : Fintype ↥(stabilizer α t) := Finset.fintypeStabilizerOfMulStab ht
⊢ t.mulStab.card = Nat.card ↥(stabilizer α t)
Tactic:
simp
State after:
case h.e'_4
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
h : stabilizer α s ≤ stabilizer α t
ht : t.Nonempty
this✝ : Fintype ↥(stabilizer α s) := Finset.fintypeStabilizerOfMulStab hs
this : Fintype ↥(stabilizer α t) := Finset.fintypeStabilizerOfMulStab ht
⊢ t.mulStab.card = Nat.card ↥(stabilizer α t)

State before:
case h.e'_4
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
h : stabilizer α s ≤ stabilizer α t
ht : t.Nonempty
this✝ : Fintype ↥(stabilizer α s) := Finset.fintypeStabilizerOfMulStab hs
this : Fintype ↥(stabilizer α t) := Finset.fintypeStabilizerOfMulStab ht
⊢ t.mulStab.card = Nat.card ↥(stabilizer α t)
Tactic:
simp [-mem_stabilizer_iff]
State after:
case h.e'_4
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
h : stabilizer α s ≤ stabilizer α t
ht : t.Nonempty
this✝ : Fintype ↥(stabilizer α s) := Finset.fintypeStabilizerOfMulStab hs
this : Fintype ↥(stabilizer α t) := Finset.fintypeStabilizerOfMulStab ht
⊢ t.mulStab.card = Fintype.card ↥(stabilizer α t)

State before:
case h.e'_4
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
h : stabilizer α s ≤ stabilizer α t
ht : t.Nonempty
this✝ : Fintype ↥(stabilizer α s) := Finset.fintypeStabilizerOfMulStab hs
this : Fintype ↥(stabilizer α t) := Finset.fintypeStabilizerOfMulStab ht
⊢ t.mulStab.card = Fintype.card ↥(stabilizer α t)
Tactic:
change _ = (t.mulStab.attach.map
  ⟨Subtype.map id fun _ ↦ (mem_mulStab ht).1, Subtype.map_injective _ injective_id⟩).card
State after:
case h.e'_4
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
h : stabilizer α s ≤ stabilizer α t
ht : t.Nonempty
this✝ : Fintype ↥(stabilizer α s) := Finset.fintypeStabilizerOfMulStab hs
this : Fintype ↥(stabilizer α t) := Finset.fintypeStabilizerOfMulStab ht
⊢ t.mulStab.card = (map { toFun := Subtype.map id ⋯, inj' := ⋯ } t.mulStab.attach).card

State before:
case h.e'_4
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
h : stabilizer α s ≤ stabilizer α t
ht : t.Nonempty
this✝ : Fintype ↥(stabilizer α s) := Finset.fintypeStabilizerOfMulStab hs
this : Fintype ↥(stabilizer α t) := Finset.fintypeStabilizerOfMulStab ht
⊢ t.mulStab.card = (map { toFun := Subtype.map id ⋯, inj' := ⋯ } t.mulStab.attach).card
Tactic:
simp
State after:
no goals

State before:
case inl
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s : Finset α
a : α
hs : s.Nonempty
h : s.mulStab ⊆ ∅.mulStab
⊢ s.mulStab.card ∣ ∅.mulStab.card
Tactic:
simp
State after:
no goals