G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
hU : closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)) ≤ H
⊢ closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)) = H
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
⊢ closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)) = H
have hU : closure ((R * S).image fun g => g * (toFun hR g : G)⁻¹) ≤ H := by
  rw [closure_le]
  rintro - ⟨g, -, rfl⟩
  exact mul_inv_toFun_mem hR g
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
hU : closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)) ≤ H
h : G
hh : h ∈ H
⊢ h ∈ closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S))
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
hU : closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)) ≤ H
⊢ closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)) = H
refine' le_antisymm hU fun h hh => _
case intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
hU : closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)) ≤ H
g r : G
hg : g ∈ ↑(closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)))
hr : r ∈ R
hh : (fun x x_1 => x * x_1) g r ∈ H
⊢ (fun x x_1 => x * x_1) g r ∈ closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S))
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
hU : closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)) ≤ H
h : G
hh : h ∈ H
⊢ h ∈ closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S))
obtain ⟨g, r, hg, hr, rfl⟩ :=
  show h ∈ _ from eq_top_iff.mp (closure_mul_image_mul_eq_top hR hR1 hS) (mem_top h)
case intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
hU : closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)) ≤ H
g r : G
hg : g ∈ ↑(closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)))
hr : r ∈ R
hh : (fun x x_1 => x * x_1) g r ∈ H
⊢ { val := r, property := hr } = { val := 1, property := hR1 }
case intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
hU : closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)) ≤ H
g r : G
hg : g ∈ ↑(closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)))
hr : r ∈ R
hh : (fun x x_1 => x * x_1) g r ∈ H
⊢ (fun x x_1 => x * x_1) g r ∈ closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S))
suffices (⟨r, hr⟩ : R) = (⟨1, hR1⟩ : R) by
  simpa only [show r = 1 from Subtype.ext_iff.mp this, mul_one]
case intro.intro.intro.intro.py₁
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
hU : closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)) ≤ H
g r : G
hg : g ∈ ↑(closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)))
hr : r ∈ R
hh : (fun x x_1 => x * x_1) g r ∈ H
⊢ r * (↑{ val := r, property := hr })⁻¹ ∈ ↑H

case intro.intro.intro.intro.py₂
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
hU : closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)) ≤ H
g r : G
hg : g ∈ ↑(closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)))
hr : r ∈ R
hh : (fun x x_1 => x * x_1) g r ∈ H
⊢ r * (↑{ val := 1, property := hR1 })⁻¹ ∈ ↑H
case intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
hU : closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)) ≤ H
g r : G
hg : g ∈ ↑(closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)))
hr : r ∈ R
hh : (fun x x_1 => x * x_1) g r ∈ H
⊢ { val := r, property := hr } = { val := 1, property := hR1 }
apply (mem_rightTransversals_iff_existsUnique_mul_inv_mem.mp hR r).unique
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
⊢ (fun g => g * (↑(toFun hR g))⁻¹) '' (R * S) ⊆ ↑H
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
⊢ closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)) ≤ H
rw [closure_le]
case intro.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
g : G
⊢ (fun g => g * (↑(toFun hR g))⁻¹) g ∈ ↑H
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
⊢ (fun g => g * (↑(toFun hR g))⁻¹) '' (R * S) ⊆ ↑H
rintro - ⟨g, -, rfl⟩
no goals
case intro.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
g : G
⊢ (fun g => g * (↑(toFun hR g))⁻¹) g ∈ ↑H
exact mul_inv_toFun_mem hR g
no goals
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
hU : closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)) ≤ H
g r : G
hg : g ∈ ↑(closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)))
hr : r ∈ R
hh : (fun x x_1 => x * x_1) g r ∈ H
this : { val := r, property := hr } = { val := 1, property := hR1 }
⊢ (fun x x_1 => x * x_1) g r ∈ closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S))
simpa only [show r = 1 from Subtype.ext_iff.mp this, mul_one]
case intro.intro.intro.intro.py₁
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
hU : closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)) ≤ H
g r : G
hg : g ∈ ↑(closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)))
hr : r ∈ R
hh : (fun x x_1 => x * x_1) g r ∈ H
⊢ 1 ∈ ↑H
case intro.intro.intro.intro.py₁
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
hU : closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)) ≤ H
g r : G
hg : g ∈ ↑(closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)))
hr : r ∈ R
hh : (fun x x_1 => x * x_1) g r ∈ H
⊢ r * (↑{ val := r, property := hr })⁻¹ ∈ ↑H
rw [Subtype.coe_mk, mul_inv_self]
no goals
case intro.intro.intro.intro.py₁
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
hU : closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)) ≤ H
g r : G
hg : g ∈ ↑(closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)))
hr : r ∈ R
hh : (fun x x_1 => x * x_1) g r ∈ H
⊢ 1 ∈ ↑H
exact H.one_mem
case intro.intro.intro.intro.py₂
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
hU : closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)) ≤ H
g r : G
hg : g ∈ ↑(closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)))
hr : r ∈ R
hh : (fun x x_1 => x * x_1) g r ∈ H
⊢ r ∈ ↑H
case intro.intro.intro.intro.py₂
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
hU : closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)) ≤ H
g r : G
hg : g ∈ ↑(closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)))
hr : r ∈ R
hh : (fun x x_1 => x * x_1) g r ∈ H
⊢ r * (↑{ val := 1, property := hR1 })⁻¹ ∈ ↑H
rw [Subtype.coe_mk, inv_one, mul_one]
no goals
case intro.intro.intro.intro.py₂
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
hU : closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)) ≤ H
g r : G
hg : g ∈ ↑(closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)))
hr : r ∈ R
hh : (fun x x_1 => x * x_1) g r ∈ H
⊢ r ∈ ↑H
exact (H.mul_mem_cancel_left (hU hg)).mp hh