G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S✝ : Set G
inst✝ : FiniteIndex H
S : Finset G
hS : closure ↑S = ⊤
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
⊢ ∃ T, Finset.card T ≤ index H * Finset.card S ∧ closure ↑T = ⊤
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S✝ : Set G
inst✝ : FiniteIndex H
S : Finset G
hS : closure ↑S = ⊤
⊢ ∃ T, Finset.card T ≤ index H * Finset.card S ∧ closure ↑T = ⊤
letI := H.fintypeQuotientOfFiniteIndex
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S✝ : Set G
inst✝ : FiniteIndex H
S : Finset G
hS : closure ↑S = ⊤
this✝ : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
this : DecidableEq G
⊢ ∃ T, Finset.card T ≤ index H * Finset.card S ∧ closure ↑T = ⊤
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S✝ : Set G
inst✝ : FiniteIndex H
S : Finset G
hS : closure ↑S = ⊤
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
⊢ ∃ T, Finset.card T ≤ index H * Finset.card S ∧ closure ↑T = ⊤
haveI : DecidableEq G := Classical.decEq G
case intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S✝ : Set G
inst✝ : FiniteIndex H
S : Finset G
hS : closure ↑S = ⊤
this✝ : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
this : DecidableEq G
R₀ : Set G
hR : R₀ ∈ rightTransversals ↑H
hR1 : 1 ∈ R₀
⊢ ∃ T, Finset.card T ≤ index H * Finset.card S ∧ closure ↑T = ⊤
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S✝ : Set G
inst✝ : FiniteIndex H
S : Finset G
hS : closure ↑S = ⊤
this✝ : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
this : DecidableEq G
⊢ ∃ T, Finset.card T ≤ index H * Finset.card S ∧ closure ↑T = ⊤
obtain ⟨R₀, hR : R₀ ∈ rightTransversals (H : Set G), hR1⟩ := exists_right_transversal (1 : G)
case intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S✝ : Set G
inst✝ : FiniteIndex H
S : Finset G
hS : closure ↑S = ⊤
this✝¹ : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
this✝ : DecidableEq G
R₀ : Set G
hR : R₀ ∈ rightTransversals ↑H
hR1 : 1 ∈ R₀
this : Fintype ↑R₀
⊢ ∃ T, Finset.card T ≤ index H * Finset.card S ∧ closure ↑T = ⊤
case intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S✝ : Set G
inst✝ : FiniteIndex H
S : Finset G
hS : closure ↑S = ⊤
this✝ : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
this : DecidableEq G
R₀ : Set G
hR : R₀ ∈ rightTransversals ↑H
hR1 : 1 ∈ R₀
⊢ ∃ T, Finset.card T ≤ index H * Finset.card S ∧ closure ↑T = ⊤
haveI : Fintype R₀ := Fintype.ofEquiv _ (toEquiv hR)
case intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R✝ S✝ : Set G
inst✝ : FiniteIndex H
S : Finset G
hS : closure ↑S = ⊤
this✝¹ : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
this✝ : DecidableEq G
R₀ : Set G
hR : R₀ ∈ rightTransversals ↑H
hR1 : 1 ∈ R₀
this : Fintype ↑R₀
R : Finset G := Set.toFinset R₀
⊢ ∃ T, Finset.card T ≤ index H * Finset.card S ∧ closure ↑T = ⊤
case intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S✝ : Set G
inst✝ : FiniteIndex H
S : Finset G
hS : closure ↑S = ⊤
this✝¹ : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
this✝ : DecidableEq G
R₀ : Set G
hR : R₀ ∈ rightTransversals ↑H
hR1 : 1 ∈ R₀
this : Fintype ↑R₀
⊢ ∃ T, Finset.card T ≤ index H * Finset.card S ∧ closure ↑T = ⊤
let R : Finset G := Set.toFinset R₀
case intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R✝ S✝ : Set G
inst✝ : FiniteIndex H
S : Finset G
hS : closure ↑S = ⊤
this✝¹ : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
this✝ : DecidableEq G
R₀ : Set G
hR1 : 1 ∈ R₀
this : Fintype ↑R₀
R : Finset G := Set.toFinset R₀
hR : ↑R ∈ rightTransversals ↑H
⊢ ∃ T, Finset.card T ≤ index H * Finset.card S ∧ closure ↑T = ⊤
case intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R✝ S✝ : Set G
inst✝ : FiniteIndex H
S : Finset G
hS : closure ↑S = ⊤
this✝¹ : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
this✝ : DecidableEq G
R₀ : Set G
hR : R₀ ∈ rightTransversals ↑H
hR1 : 1 ∈ R₀
this : Fintype ↑R₀
R : Finset G := Set.toFinset R₀
⊢ ∃ T, Finset.card T ≤ index H * Finset.card S ∧ closure ↑T = ⊤
replace hR : (R : Set G) ∈ rightTransversals (H : Set G) := by rwa [Set.coe_toFinset]
case intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R✝ S✝ : Set G
inst✝ : FiniteIndex H
S : Finset G
hS : closure ↑S = ⊤
this✝¹ : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
this✝ : DecidableEq G
R₀ : Set G
this : Fintype ↑R₀
R : Finset G := Set.toFinset R₀
hR : ↑R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
⊢ ∃ T, Finset.card T ≤ index H * Finset.card S ∧ closure ↑T = ⊤
case intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R✝ S✝ : Set G
inst✝ : FiniteIndex H
S : Finset G
hS : closure ↑S = ⊤
this✝¹ : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
this✝ : DecidableEq G
R₀ : Set G
hR1 : 1 ∈ R₀
this : Fintype ↑R₀
R : Finset G := Set.toFinset R₀
hR : ↑R ∈ rightTransversals ↑H
⊢ ∃ T, Finset.card T ≤ index H * Finset.card S ∧ closure ↑T = ⊤
replace hR1 : (1 : G) ∈ R := by rwa [Set.mem_toFinset]
case intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R✝ S✝ : Set G
inst✝ : FiniteIndex H
S : Finset G
hS : closure ↑S = ⊤
this✝¹ : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
this✝ : DecidableEq G
R₀ : Set G
this : Fintype ↑R₀
R : Finset G := Set.toFinset R₀
hR : ↑R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
⊢ Finset.card
      (Finset.image (fun g => { val := g * (↑(toFun hR g))⁻¹, property := (_ : g * (↑(toFun hR g))⁻¹ ∈ H) }) (R * S)) ≤
    index H * Finset.card S
case intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R✝ S✝ : Set G
inst✝ : FiniteIndex H
S : Finset G
hS : closure ↑S = ⊤
this✝¹ : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
this✝ : DecidableEq G
R₀ : Set G
this : Fintype ↑R₀
R : Finset G := Set.toFinset R₀
hR : ↑R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
⊢ ∃ T, Finset.card T ≤ index H * Finset.card S ∧ closure ↑T = ⊤
refine' ⟨_, _, closure_mul_image_eq_top' hR hR1 hS⟩
no goals
case intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R✝ S✝ : Set G
inst✝ : FiniteIndex H
S : Finset G
hS : closure ↑S = ⊤
this✝¹ : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
this✝ : DecidableEq G
R₀ : Set G
this : Fintype ↑R₀
R : Finset G := Set.toFinset R₀
hR : ↑R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
⊢ Finset.card R = index H
calc
  R.card = Fintype.card R := (Fintype.card_coe R).symm
  _ = _ := (Fintype.card_congr (toEquiv hR)).symm
  _ = Fintype.card (G ⧸ H) := (QuotientGroup.card_quotient_rightRel H)
  _ = H.index := H.index_eq_card.symm
no goals
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R✝ S✝ : Set G
inst✝ : FiniteIndex H
S : Finset G
hS : closure ↑S = ⊤
this✝¹ : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
this✝ : DecidableEq G
R₀ : Set G
hR : R₀ ∈ rightTransversals ↑H
hR1 : 1 ∈ R₀
this : Fintype ↑R₀
R : Finset G := Set.toFinset R₀
⊢ ↑R ∈ rightTransversals ↑H
rwa [Set.coe_toFinset]
no goals
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R✝ S✝ : Set G
inst✝ : FiniteIndex H
S : Finset G
hS : closure ↑S = ⊤
this✝¹ : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
this✝ : DecidableEq G
R₀ : Set G
hR1 : 1 ∈ R₀
this : Fintype ↑R₀
R : Finset G := Set.toFinset R₀
hR : ↑R ∈ rightTransversals ↑H
⊢ 1 ∈ R
rwa [Set.mem_toFinset]