-- Mathlib/GroupTheory/Schreier.lean
theorem closure_mul_image_eq (hR : IsComplement H R) (hR1 : (1 : G) ∈ R)
    (hS : closure S = ⊤) : closure ((R * S).image fun g => g * (hR.toRightFun g : G)⁻¹) = H

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H) R
hR1 : 1 ∈ R
hS : closure S = ⊤
hU : closure ((fun g => g * (↑(hR.toRightFun g))⁻¹) '' (R * S)) ≤ H
⊢ closure ((fun g => g * (↑(hR.toRightFun g))⁻¹) '' (R * S)) = H

Tactic:
refine le_antisymm hU fun h hh => ?_

Result:
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H) R
hR1 : 1 ∈ R
hS : closure S = ⊤
hU : closure ((fun g => g * (↑(hR.toRightFun g))⁻¹) '' (R * S)) ≤ H
h : G
hh : h ∈ H
⊢ h ∈ closure ((fun g => g * (↑(hR.toRightFun g))⁻¹) '' (R * S))

Proof state:
case intro.intro.intro.intro.py₁
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H) R
hR1 : 1 ∈ R
hS : closure S = ⊤
hU : closure ((fun g => g * (↑(hR.toRightFun g))⁻¹) '' (R * S)) ≤ H
g : G
hg : g ∈ ↑(closure ((fun g => g * (↑(hR.toRightFun g))⁻¹) '' (R * S)))
r : G
hr : r ∈ R
hh : (fun x1 x2 => x1 * x2) g r ∈ H
⊢ r * (↑⟨r, hr⟩)⁻¹ ∈ ↑H

Tactic:
rw [Subtype.coe_mk, mul_inv_cancel]

Result:
case intro.intro.intro.intro.py₁
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H) R
hR1 : 1 ∈ R
hS : closure S = ⊤
hU : closure ((fun g => g * (↑(hR.toRightFun g))⁻¹) '' (R * S)) ≤ H
g : G
hg : g ∈ ↑(closure ((fun g => g * (↑(hR.toRightFun g))⁻¹) '' (R * S)))
r : G
hr : r ∈ R
hh : (fun x1 x2 => x1 * x2) g r ∈ H
⊢ 1 ∈ ↑H

Proof state:
case intro.intro.intro.intro.py₂
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H) R
hR1 : 1 ∈ R
hS : closure S = ⊤
hU : closure ((fun g => g * (↑(hR.toRightFun g))⁻¹) '' (R * S)) ≤ H
g : G
hg : g ∈ ↑(closure ((fun g => g * (↑(hR.toRightFun g))⁻¹) '' (R * S)))
r : G
hr : r ∈ R
hh : (fun x1 x2 => x1 * x2) g r ∈ H
⊢ r * (↑⟨1, hR1⟩)⁻¹ ∈ ↑H

Tactic:
rw [Subtype.coe_mk, inv_one, mul_one]

Result:
case intro.intro.intro.intro.py₂
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H) R
hR1 : 1 ∈ R
hS : closure S = ⊤
hU : closure ((fun g => g * (↑(hR.toRightFun g))⁻¹) '' (R * S)) ≤ H
g : G
hg : g ∈ ↑(closure ((fun g => g * (↑(hR.toRightFun g))⁻¹) '' (R * S)))
r : G
hr : r ∈ R
hh : (fun x1 x2 => x1 * x2) g r ∈ H
⊢ r ∈ ↑H

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H) R
hR1 : 1 ∈ R
hS : closure S = ⊤
hU : closure ((fun g => g * (↑(hR.toRightFun g))⁻¹) '' (R * S)) ≤ H
g : G
hg : g ∈ ↑(closure ((fun g => g * (↑(hR.toRightFun g))⁻¹) '' (R * S)))
r : G
hr : r ∈ R
hh : (fun x1 x2 => x1 * x2) g r ∈ H
this : ⟨r, hr⟩ = ⟨1, hR1⟩
⊢ (fun x1 x2 => x1 * x2) g r ∈ closure ((fun g => g * (↑(hR.toRightFun g))⁻¹) '' (R * S))

Tactic:
simpa only [show r = 1 from Subtype.ext_iff.mp this, mul_one]

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H) R
hR1 : 1 ∈ R
hS : closure S = ⊤
⊢ closure ((fun g => g * (↑(hR.toRightFun g))⁻¹) '' (R * S)) = H

Tactic:
have hU : closure ((R * S).image fun g => g * (hR.toRightFun g : G)⁻¹) ≤ H := by
  rw [closure_le]
  rintro - ⟨g, -, rfl⟩
  exact hR.mul_inv_toRightFun_mem g

Result:
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H) R
hR1 : 1 ∈ R
hS : closure S = ⊤
hU : closure ((fun g => g * (↑(hR.toRightFun g))⁻¹) '' (R * S)) ≤ H
⊢ closure ((fun g => g * (↑(hR.toRightFun g))⁻¹) '' (R * S)) = H

Proof state:
case intro.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H) R
hR1 : 1 ∈ R
hS : closure S = ⊤
g : G
⊢ (fun g => g * (↑(hR.toRightFun g))⁻¹) g ∈ ↑H

Tactic:
exact hR.mul_inv_toRightFun_mem g

Result:
no goals

Proof state:
case intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H) R
hR1 : 1 ∈ R
hS : closure S = ⊤
hU : closure ((fun g => g * (↑(hR.toRightFun g))⁻¹) '' (R * S)) ≤ H
g : G
hg : g ∈ ↑(closure ((fun g => g * (↑(hR.toRightFun g))⁻¹) '' (R * S)))
r : G
hr : r ∈ R
hh : (fun x1 x2 => x1 * x2) g r ∈ H
⊢ (fun x1 x2 => x1 * x2) g r ∈ closure ((fun g => g * (↑(hR.toRightFun g))⁻¹) '' (R * S))

Tactic:
suffices (⟨r, hr⟩ : R) = (⟨1, hR1⟩ : R) by
  simpa only [show r = 1 from Subtype.ext_iff.mp this, mul_one]

Result:
case intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H) R
hR1 : 1 ∈ R
hS : closure S = ⊤
hU : closure ((fun g => g * (↑(hR.toRightFun g))⁻¹) '' (R * S)) ≤ H
g : G
hg : g ∈ ↑(closure ((fun g => g * (↑(hR.toRightFun g))⁻¹) '' (R * S)))
r : G
hr : r ∈ R
hh : (fun x1 x2 => x1 * x2) g r ∈ H
⊢ ⟨r, hr⟩ = ⟨1, hR1⟩

Proof state:
case intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H) R
hR1 : 1 ∈ R
hS : closure S = ⊤
hU : closure ((fun g => g * (↑(hR.toRightFun g))⁻¹) '' (R * S)) ≤ H
g : G
hg : g ∈ ↑(closure ((fun g => g * (↑(hR.toRightFun g))⁻¹) '' (R * S)))
r : G
hr : r ∈ R
hh : (fun x1 x2 => x1 * x2) g r ∈ H
⊢ ⟨r, hr⟩ = ⟨1, hR1⟩

Tactic:
apply (isComplement_iff_existsUnique_mul_inv_mem.mp hR r).unique

Result:
case intro.intro.intro.intro.py₁
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H) R
hR1 : 1 ∈ R
hS : closure S = ⊤
hU : closure ((fun g => g * (↑(hR.toRightFun g))⁻¹) '' (R * S)) ≤ H
g : G
hg : g ∈ ↑(closure ((fun g => g * (↑(hR.toRightFun g))⁻¹) '' (R * S)))
r : G
hr : r ∈ R
hh : (fun x1 x2 => x1 * x2) g r ∈ H
⊢ r * (↑⟨r, hr⟩)⁻¹ ∈ ↑H

case intro.intro.intro.intro.py₂
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H) R
hR1 : 1 ∈ R
hS : closure S = ⊤
hU : closure ((fun g => g * (↑(hR.toRightFun g))⁻¹) '' (R * S)) ≤ H
g : G
hg : g ∈ ↑(closure ((fun g => g * (↑(hR.toRightFun g))⁻¹) '' (R * S)))
r : G
hr : r ∈ R
hh : (fun x1 x2 => x1 * x2) g r ∈ H
⊢ r * (↑⟨1, hR1⟩)⁻¹ ∈ ↑H

Proof state:
case intro.intro.intro.intro.py₂
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H) R
hR1 : 1 ∈ R
hS : closure S = ⊤
hU : closure ((fun g => g * (↑(hR.toRightFun g))⁻¹) '' (R * S)) ≤ H
g : G
hg : g ∈ ↑(closure ((fun g => g * (↑(hR.toRightFun g))⁻¹) '' (R * S)))
r : G
hr : r ∈ R
hh : (fun x1 x2 => x1 * x2) g r ∈ H
⊢ r ∈ ↑H

Tactic:
exact (H.mul_mem_cancel_left (hU hg)).mp hh

Result:
no goals

Proof state:
case intro.intro.intro.intro.py₁
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H) R
hR1 : 1 ∈ R
hS : closure S = ⊤
hU : closure ((fun g => g * (↑(hR.toRightFun g))⁻¹) '' (R * S)) ≤ H
g : G
hg : g ∈ ↑(closure ((fun g => g * (↑(hR.toRightFun g))⁻¹) '' (R * S)))
r : G
hr : r ∈ R
hh : (fun x1 x2 => x1 * x2) g r ∈ H
⊢ 1 ∈ ↑H

Tactic:
exact H.one_mem

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H) R
hR1 : 1 ∈ R
hS : closure S = ⊤
⊢ (fun g => g * (↑(hR.toRightFun g))⁻¹) '' (R * S) ⊆ ↑H

Tactic:
rintro - ⟨g, -, rfl⟩

Result:
case intro.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H) R
hR1 : 1 ∈ R
hS : closure S = ⊤
g : G
⊢ (fun g => g * (↑(hR.toRightFun g))⁻¹) g ∈ ↑H

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H) R
hR1 : 1 ∈ R
hS : closure S = ⊤
hU : closure ((fun g => g * (↑(hR.toRightFun g))⁻¹) '' (R * S)) ≤ H
h : G
hh : h ∈ H
⊢ h ∈ closure ((fun g => g * (↑(hR.toRightFun g))⁻¹) '' (R * S))

Tactic:
obtain ⟨g, hg, r, hr, rfl⟩ :=
  show h ∈ _ from eq_top_iff.mp (closure_mul_image_mul_eq_top hR hR1 hS) (mem_top h)

Result:
case intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H) R
hR1 : 1 ∈ R
hS : closure S = ⊤
hU : closure ((fun g => g * (↑(hR.toRightFun g))⁻¹) '' (R * S)) ≤ H
g : G
hg : g ∈ ↑(closure ((fun g => g * (↑(hR.toRightFun g))⁻¹) '' (R * S)))
r : G
hr : r ∈ R
hh : (fun x1 x2 => x1 * x2) g r ∈ H
⊢ (fun x1 x2 => x1 * x2) g r ∈ closure ((fun g => g * (↑(hR.toRightFun g))⁻¹) '' (R * S))