G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R✝ S✝ : Set G
inst✝ : DecidableEq G
R S : Finset G
hR : ↑R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure ↑S = ⊤
⊢ closure ((fun g => { val := g * (↑(toFun hR g))⁻¹, property := (_ : g * (↑(toFun hR g))⁻¹ ∈ H) }) '' (↑R * ↑S)) = ⊤
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R✝ S✝ : Set G
inst✝ : DecidableEq G
R S : Finset G
hR : ↑R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure ↑S = ⊤
⊢ closure
      ↑(Finset.image (fun g => { val := g * (↑(toFun hR g))⁻¹, property := (_ : g * (↑(toFun hR g))⁻¹ ∈ H) }) (R * S)) =
    ⊤
rw [Finset.coe_image, Finset.coe_mul]
no goals
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R✝ S✝ : Set G
inst✝ : DecidableEq G
R S : Finset G
hR : ↑R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure ↑S = ⊤
⊢ closure ((fun g => { val := g * (↑(toFun hR g))⁻¹, property := (_ : g * (↑(toFun hR g))⁻¹ ∈ H) }) '' (↑R * ↑S)) = ⊤
exact closure_mul_image_eq_top hR hR1 hS