Theorem: Subgroup.subgroup_mul_card_eq_mul (LeanCamCombi/Kneser/Mathlib.lean)

State before:
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
⊢ Nat.card ↥s * Nat.card ↑(QuotientGroup.mk '' t) = Nat.card ↑(t * ↑s)
Tactic:
rw [← Nat.card_prod, Nat.card_congr]
State after:
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
⊢ ↥s × ↑(QuotientGroup.mk '' t) ≃ ↑(t * ↑s)

State before:
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
⊢ ↥s × ↑(QuotientGroup.mk '' t) ≃ ↑(t * ↑s)
Tactic:
apply Equiv.trans (QuotientGroup.preimageMkEquivSubgroupProdSet _ _).symm
State after:
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
⊢ ↑(QuotientGroup.mk ⁻¹' (QuotientGroup.mk '' t)) ≃ ↑(t * ↑s)

State before:
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
⊢ ↑(QuotientGroup.mk ⁻¹' (QuotientGroup.mk '' t)) ≃ ↑(t * ↑s)
Tactic:
rw [QuotientGroup.preimage_image_mk]
State after:
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
⊢ ↑(⋃ x, (fun x_1 => x_1 * ↑x) ⁻¹' t) ≃ ↑(t * ↑s)

State before:
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
⊢ ↑(⋃ x, (fun x_1 => x_1 * ↑x) ⁻¹' t) ≃ ↑(t * ↑s)
Tactic:
apply Set.BijOn.equiv id
State after:
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
⊢ Set.BijOn id (⋃ x, (fun x_1 => x_1 * ↑x) ⁻¹' t) (t * ↑s)

State before:
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
⊢ Set.BijOn id (⋃ x, (fun x_1 => x_1 * ↑x) ⁻¹' t) (t * ↑s)
Tactic:
convert Set.bijOn_id _
State after:
case h.e'_5
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
⊢ t * ↑s = ⋃ x, (fun x_1 => x_1 * ↑x) ⁻¹' t

State before:
case h.e'_5
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
⊢ t * ↑s = ⋃ x, (fun x_1 => x_1 * ↑x) ⁻¹' t
Tactic:
ext x
State after:
case h.e'_5.h
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
x : α
⊢ x ∈ t * ↑s ↔ x ∈ ⋃ x, (fun x_1 => x_1 * ↑x) ⁻¹' t

State before:
case h.e'_5.h
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
x : α
⊢ x ∈ t * ↑s ↔ x ∈ ⋃ x, (fun x_1 => x_1 * ↑x) ⁻¹' t
Tactic:
constructor
State after:
case h.e'_5.h.mp
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
x : α
⊢ x ∈ t * ↑s → x ∈ ⋃ x, (fun x_1 => x_1 * ↑x) ⁻¹' t

case h.e'_5.h.mpr
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
x : α
⊢ x ∈ ⋃ x, (fun x_1 => x_1 * ↑x) ⁻¹' t → x ∈ t * ↑s

State before:
case h.e'_5.h.mp
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
x : α
⊢ x ∈ t * ↑s → x ∈ ⋃ x, (fun x_1 => x_1 * ↑x) ⁻¹' t
Tactic:
simp only [Set.mem_iUnion, Set.mem_preimage, Subtype.exists, exists_prop, Set.mem_mul]
State after:
case h.e'_5.h.mp
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
x : α
⊢ (∃ x_1 ∈ t, ∃ y ∈ ↑s, x_1 * y = x) → ∃ a ∈ s, x * a ∈ t

State before:
case h.e'_5.h.mp
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
x : α
⊢ (∃ x_1 ∈ t, ∃ y ∈ ↑s, x_1 * y = x) → ∃ a ∈ s, x * a ∈ t
Tactic:
aesop
State after:
no goals

State before:
case h.e'_5.h.mpr
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
x : α
⊢ x ∈ ⋃ x, (fun x_1 => x_1 * ↑x) ⁻¹' t → x ∈ t * ↑s
Tactic:
simp only [Set.mem_iUnion, Set.mem_preimage, Subtype.exists, exists_prop, forall_exists_index,
and_imp]
State after:
case h.e'_5.h.mpr
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
x : α
⊢ ∀ x_1 ∈ s, x * x_1 ∈ t → x ∈ t * ↑s

State before:
case h.e'_5.h.mpr
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
x : α
⊢ ∀ x_1 ∈ s, x * x_1 ∈ t → x ∈ t * ↑s
Tactic:
intro y hys hxy
State after:
case h.e'_5.h.mpr
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
x y : α
hys : y ∈ s
hxy : x * y ∈ t
⊢ x ∈ t * ↑s

State before:
case h.e'_5.h.mpr
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
x y : α
hys : y ∈ s
hxy : x * y ∈ t
⊢ x ∈ t * ↑s
Tactic:
rw [← mul_inv_cancel_right x y]
State after:
case h.e'_5.h.mpr
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
x y : α
hys : y ∈ s
hxy : x * y ∈ t
⊢ x * y * y⁻¹ ∈ t * ↑s

State before:
case h.e'_5.h.mpr
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
x y : α
hys : y ∈ s
hxy : x * y ∈ t
⊢ x * y * y⁻¹ ∈ t * ↑s
Tactic:
apply Set.mul_mem_mul hxy (by simpa)
State after:
no goals

State before:
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
x y : α
hys : y ∈ s
hxy : x * y ∈ t
⊢ y⁻¹ ∈ ↑s
Tactic:
simpa
State after:
no goals