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

State before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
h : ↑t * ↑s = ↑t
⊢ Nat.card ↥s * (image QuotientGroup.mk t).card = t.card
Tactic:
have := s.subgroup_mul_card_eq_mul t
State after:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
h : ↑t * ↑s = ↑t
this : Nat.card ↥s * Nat.card ↑(QuotientGroup.mk '' ↑t) = Nat.card ↑(↑t * ↑s)
⊢ Nat.card ↥s * (image QuotientGroup.mk t).card = t.card

State before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
h : ↑t * ↑s = ↑t
this : Nat.card ↥s * Nat.card ↑(QuotientGroup.mk '' ↑t) = Nat.card ↑(↑t * ↑s)
⊢ Nat.card ↥s * (image QuotientGroup.mk t).card = t.card
Tactic:
rw [h] at this
State after:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
h : ↑t * ↑s = ↑t
this : Nat.card ↥s * Nat.card ↑(QuotientGroup.mk '' ↑t) = Nat.card ↑↑t
⊢ Nat.card ↥s * (image QuotientGroup.mk t).card = t.card

State before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
h : ↑t * ↑s = ↑t
this : Nat.card ↥s * Nat.card ↑(QuotientGroup.mk '' ↑t) = Nat.card ↑↑t
⊢ Nat.card ↥s * (image QuotientGroup.mk t).card = t.card
Tactic:
simpa
State after:
no goals

State before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
⊢ ↑t * ↑s = ↑t
Tactic:
apply Set.Subset.antisymm (Set.Subset.trans (Set.mul_subset_mul_left hst) _)
State after:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
⊢ ↑t ⊆ ↑t * ↑s

ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
⊢ ↑t * ↑t.mulStab ⊆ ↑t

State before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
⊢ ↑t ⊆ ↑t * ↑s
Tactic:
intro x
State after:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
x : α
⊢ x ∈ ↑t → x ∈ ↑t * ↑s

State before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
x : α
⊢ x ∈ ↑t → x ∈ ↑t * ↑s
Tactic:
rw [Set.mem_mul]
State after:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
x : α
⊢ x ∈ ↑t → ∃ x_1 ∈ ↑t, ∃ y ∈ ↑s, x_1 * y = x

State before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
x : α
⊢ x ∈ ↑t → ∃ x_1 ∈ ↑t, ∃ y ∈ ↑s, x_1 * y = x
Tactic:
aesop
State after:
no goals

State before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
⊢ ↑t * ↑t.mulStab ⊆ ↑t
Tactic:
rw [← coe_mul, mul_mulStab]
State after:
no goals