[GOAL]
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
h : IsComplement' H K
⊢ IsComplement' K H
[PROOFSTEP]
let ϕ : H × K ≃ K × H :=
  Equiv.mk (fun x => ⟨x.2⁻¹, x.1⁻¹⟩) (fun x => ⟨x.2⁻¹, x.1⁻¹⟩) (fun x => Prod.ext (inv_inv _) (inv_inv _)) fun x =>
    Prod.ext (inv_inv _) (inv_inv _)
[GOAL]
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
h : IsComplement' H K
ϕ : { x // x ∈ H } × { x // x ∈ K } ≃ { x // x ∈ K } × { x // x ∈ H } :=
  { toFun := fun x => (x.snd⁻¹, x.fst⁻¹), invFun := fun x => (x.snd⁻¹, x.fst⁻¹),
    left_inv :=
      (_ :
        ∀ (x : { x // x ∈ H } × { x // x ∈ K }), (fun x => (x.snd⁻¹, x.fst⁻¹)) ((fun x => (x.snd⁻¹, x.fst⁻¹)) x) = x),
    right_inv :=
      (_ :
        ∀ (x : { x // x ∈ K } × { x // x ∈ H }), (fun x => (x.snd⁻¹, x.fst⁻¹)) ((fun x => (x.snd⁻¹, x.fst⁻¹)) x) = x) }
⊢ IsComplement' K H
[PROOFSTEP]
let ψ : G ≃ G := Equiv.mk (fun g : G => g⁻¹) (fun g : G => g⁻¹) inv_inv inv_inv
[GOAL]
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
h : IsComplement' H K
ϕ : { x // x ∈ H } × { x // x ∈ K } ≃ { x // x ∈ K } × { x // x ∈ H } :=
  { toFun := fun x => (x.snd⁻¹, x.fst⁻¹), invFun := fun x => (x.snd⁻¹, x.fst⁻¹),
    left_inv :=
      (_ :
        ∀ (x : { x // x ∈ H } × { x // x ∈ K }), (fun x => (x.snd⁻¹, x.fst⁻¹)) ((fun x => (x.snd⁻¹, x.fst⁻¹)) x) = x),
    right_inv :=
      (_ :
        ∀ (x : { x // x ∈ K } × { x // x ∈ H }), (fun x => (x.snd⁻¹, x.fst⁻¹)) ((fun x => (x.snd⁻¹, x.fst⁻¹)) x) = x) }
ψ : G ≃ G :=
  { toFun := fun g => g⁻¹, invFun := fun g => g⁻¹, left_inv := (_ : ∀ (a : G), a⁻¹⁻¹ = a),
    right_inv := (_ : ∀ (a : G), a⁻¹⁻¹ = a) }
⊢ IsComplement' K H
[PROOFSTEP]
suffices hf : (ψ ∘ fun x : H × K => x.1.1 * x.2.1) = (fun x : K × H => x.1.1 * x.2.1) ∘ ϕ
  by
  rw [isComplement'_def, IsComplement, ← Equiv.bijective_comp ϕ]
  apply (congr_arg Function.Bijective hf).mp
  rwa [ψ.comp_bijective]
[GOAL]
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
h : IsComplement' H K
ϕ : { x // x ∈ H } × { x // x ∈ K } ≃ { x // x ∈ K } × { x // x ∈ H } :=
  { toFun := fun x => (x.snd⁻¹, x.fst⁻¹), invFun := fun x => (x.snd⁻¹, x.fst⁻¹),
    left_inv :=
      (_ :
        ∀ (x : { x // x ∈ H } × { x // x ∈ K }), (fun x => (x.snd⁻¹, x.fst⁻¹)) ((fun x => (x.snd⁻¹, x.fst⁻¹)) x) = x),
    right_inv :=
      (_ :
        ∀ (x : { x // x ∈ K } × { x // x ∈ H }), (fun x => (x.snd⁻¹, x.fst⁻¹)) ((fun x => (x.snd⁻¹, x.fst⁻¹)) x) = x) }
ψ : G ≃ G :=
  { toFun := fun g => g⁻¹, invFun := fun g => g⁻¹, left_inv := (_ : ∀ (a : G), a⁻¹⁻¹ = a),
    right_inv := (_ : ∀ (a : G), a⁻¹⁻¹ = a) }
hf : (↑ψ ∘ fun x => ↑x.fst * ↑x.snd) = (fun x => ↑x.fst * ↑x.snd) ∘ ↑ϕ
⊢ IsComplement' K H
[PROOFSTEP]
rw [isComplement'_def, IsComplement, ← Equiv.bijective_comp ϕ]
[GOAL]
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
h : IsComplement' H K
ϕ : { x // x ∈ H } × { x // x ∈ K } ≃ { x // x ∈ K } × { x // x ∈ H } :=
  { toFun := fun x => (x.snd⁻¹, x.fst⁻¹), invFun := fun x => (x.snd⁻¹, x.fst⁻¹),
    left_inv :=
      (_ :
        ∀ (x : { x // x ∈ H } × { x // x ∈ K }), (fun x => (x.snd⁻¹, x.fst⁻¹)) ((fun x => (x.snd⁻¹, x.fst⁻¹)) x) = x),
    right_inv :=
      (_ :
        ∀ (x : { x // x ∈ K } × { x // x ∈ H }), (fun x => (x.snd⁻¹, x.fst⁻¹)) ((fun x => (x.snd⁻¹, x.fst⁻¹)) x) = x) }
ψ : G ≃ G :=
  { toFun := fun g => g⁻¹, invFun := fun g => g⁻¹, left_inv := (_ : ∀ (a : G), a⁻¹⁻¹ = a),
    right_inv := (_ : ∀ (a : G), a⁻¹⁻¹ = a) }
hf : (↑ψ ∘ fun x => ↑x.fst * ↑x.snd) = (fun x => ↑x.fst * ↑x.snd) ∘ ↑ϕ
⊢ Function.Bijective ((fun x => ↑x.fst * ↑x.snd) ∘ ↑ϕ)
[PROOFSTEP]
apply (congr_arg Function.Bijective hf).mp
[GOAL]
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
h : IsComplement' H K
ϕ : { x // x ∈ H } × { x // x ∈ K } ≃ { x // x ∈ K } × { x // x ∈ H } :=
  { toFun := fun x => (x.snd⁻¹, x.fst⁻¹), invFun := fun x => (x.snd⁻¹, x.fst⁻¹),
    left_inv :=
      (_ :
        ∀ (x : { x // x ∈ H } × { x // x ∈ K }), (fun x => (x.snd⁻¹, x.fst⁻¹)) ((fun x => (x.snd⁻¹, x.fst⁻¹)) x) = x),
    right_inv :=
      (_ :
        ∀ (x : { x // x ∈ K } × { x // x ∈ H }), (fun x => (x.snd⁻¹, x.fst⁻¹)) ((fun x => (x.snd⁻¹, x.fst⁻¹)) x) = x) }
ψ : G ≃ G :=
  { toFun := fun g => g⁻¹, invFun := fun g => g⁻¹, left_inv := (_ : ∀ (a : G), a⁻¹⁻¹ = a),
    right_inv := (_ : ∀ (a : G), a⁻¹⁻¹ = a) }
hf : (↑ψ ∘ fun x => ↑x.fst * ↑x.snd) = (fun x => ↑x.fst * ↑x.snd) ∘ ↑ϕ
⊢ Function.Bijective (↑ψ ∘ fun x => ↑x.fst * ↑x.snd)
[PROOFSTEP]
rwa [ψ.comp_bijective]
[GOAL]
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
h : IsComplement' H K
ϕ : { x // x ∈ H } × { x // x ∈ K } ≃ { x // x ∈ K } × { x // x ∈ H } :=
  { toFun := fun x => (x.snd⁻¹, x.fst⁻¹), invFun := fun x => (x.snd⁻¹, x.fst⁻¹),
    left_inv :=
      (_ :
        ∀ (x : { x // x ∈ H } × { x // x ∈ K }), (fun x => (x.snd⁻¹, x.fst⁻¹)) ((fun x => (x.snd⁻¹, x.fst⁻¹)) x) = x),
    right_inv :=
      (_ :
        ∀ (x : { x // x ∈ K } × { x // x ∈ H }), (fun x => (x.snd⁻¹, x.fst⁻¹)) ((fun x => (x.snd⁻¹, x.fst⁻¹)) x) = x) }
ψ : G ≃ G :=
  { toFun := fun g => g⁻¹, invFun := fun g => g⁻¹, left_inv := (_ : ∀ (a : G), a⁻¹⁻¹ = a),
    right_inv := (_ : ∀ (a : G), a⁻¹⁻¹ = a) }
⊢ (↑ψ ∘ fun x => ↑x.fst * ↑x.snd) = (fun x => ↑x.fst * ↑x.snd) ∘ ↑ϕ
[PROOFSTEP]
exact funext fun x => mul_inv_rev _ _
[GOAL]
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
g : G
⊢ IsComplement {g} S ↔ S = ⊤
[PROOFSTEP]
refine' ⟨fun h => top_le_iff.mp fun x _ => _, fun h => (congr_arg _ h).mpr isComplement_singleton_top⟩
[GOAL]
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
g : G
h : IsComplement {g} S
x : G
x✝ : x ∈ ⊤
⊢ x ∈ S
[PROOFSTEP]
obtain ⟨⟨⟨z, rfl : z = g⟩, y, _⟩, hy⟩ := h.2 (g * x)
[GOAL]
case intro.mk.mk.mk
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
x : G
x✝ : x ∈ ⊤
z : G
h : IsComplement {z} S
y : G
property✝ : y ∈ S
hy : (fun x => ↑x.fst * ↑x.snd) ({ val := z, property := (_ : z = z) }, { val := y, property := property✝ }) = z * x
⊢ x ∈ S
[PROOFSTEP]
rwa [← mul_left_cancel hy]
[GOAL]
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
g : G
⊢ IsComplement S {g} ↔ S = ⊤
[PROOFSTEP]
refine' ⟨fun h => top_le_iff.mp fun x _ => _, fun h => h ▸ isComplement_top_singleton⟩
[GOAL]
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
g : G
h : IsComplement S {g}
x : G
x✝ : x ∈ ⊤
⊢ x ∈ S
[PROOFSTEP]
obtain ⟨y, hy⟩ := h.2 (x * g)
[GOAL]
case intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
g : G
h : IsComplement S {g}
x : G
x✝ : x ∈ ⊤
y : ↑S × ↑{g}
hy : (fun x => ↑x.fst * ↑x.snd) y = x * g
⊢ x ∈ S
[PROOFSTEP]
conv_rhs at hy => rw [← show y.2.1 = g from y.2.2]
[GOAL]
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
g : G
h : IsComplement S {g}
x : G
x✝ : x ∈ ⊤
y : ↑S × ↑{g}
hy : (fun x => ↑x.fst * ↑x.snd) y = x * g
| x * g
[PROOFSTEP]
rw [← show y.2.1 = g from y.2.2]
[GOAL]
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
g : G
h : IsComplement S {g}
x : G
x✝ : x ∈ ⊤
y : ↑S × ↑{g}
hy : (fun x => ↑x.fst * ↑x.snd) y = x * g
| x * g
[PROOFSTEP]
rw [← show y.2.1 = g from y.2.2]
[GOAL]
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
g : G
h : IsComplement S {g}
x : G
x✝ : x ∈ ⊤
y : ↑S × ↑{g}
hy : (fun x => ↑x.fst * ↑x.snd) y = x * g
| x * g
[PROOFSTEP]
rw [← show y.2.1 = g from y.2.2]
[GOAL]
case intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
g : G
h : IsComplement S {g}
x : G
x✝ : x ∈ ⊤
y : ↑S × ↑{g}
hy : (fun x => ↑x.fst * ↑x.snd) y = x * ↑y.snd
⊢ x ∈ S
[PROOFSTEP]
rw [← mul_right_cancel hy]
[GOAL]
case intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
g : G
h : IsComplement S {g}
x : G
x✝ : x ∈ ⊤
y : ↑S × ↑{g}
hy : (fun x => ↑x.fst * ↑x.snd) y = x * ↑y.snd
⊢ ↑y.fst ∈ S
[PROOFSTEP]
exact y.1.2
[GOAL]
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
⊢ IsComplement ⊤ S ↔ ∃ g, S = {g}
[PROOFSTEP]
refine' ⟨fun h => Set.exists_eq_singleton_iff_nonempty_subsingleton.mpr ⟨_, fun a ha b hb => _⟩, _⟩
[GOAL]
case refine'_1
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
h : IsComplement ⊤ S
⊢ Set.Nonempty S
[PROOFSTEP]
obtain ⟨a, _⟩ := h.2 1
[GOAL]
case refine'_1.intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
h : IsComplement ⊤ S
a : ↑⊤ × ↑S
h✝ : (fun x => ↑x.fst * ↑x.snd) a = 1
⊢ Set.Nonempty S
[PROOFSTEP]
exact ⟨a.2.1, a.2.2⟩
[GOAL]
case refine'_2
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
h : IsComplement ⊤ S
a : G
ha : a ∈ S
b : G
hb : b ∈ S
⊢ a = b
[PROOFSTEP]
have : (⟨⟨_, mem_top a⁻¹⟩, ⟨a, ha⟩⟩ : (⊤ : Set G) × S) = ⟨⟨_, mem_top b⁻¹⟩, ⟨b, hb⟩⟩ :=
  h.1 ((inv_mul_self a).trans (inv_mul_self b).symm)
[GOAL]
case refine'_2
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
h : IsComplement ⊤ S
a : G
ha : a ∈ S
b : G
hb : b ∈ S
this :
  ({ val := a⁻¹, property := (_ : a⁻¹ ∈ ⊤) }, { val := a, property := ha }) =
    ({ val := b⁻¹, property := (_ : b⁻¹ ∈ ⊤) }, { val := b, property := hb })
⊢ a = b
[PROOFSTEP]
exact Subtype.ext_iff.mp (Prod.ext_iff.mp this).2
[GOAL]
case refine'_3
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
⊢ (∃ g, S = {g}) → IsComplement ⊤ S
[PROOFSTEP]
rintro ⟨g, rfl⟩
[GOAL]
case refine'_3.intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
T : Set G
g : G
⊢ IsComplement ⊤ {g}
[PROOFSTEP]
exact isComplement_top_singleton
[GOAL]
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
⊢ IsComplement S ⊤ ↔ ∃ g, S = {g}
[PROOFSTEP]
refine' ⟨fun h => Set.exists_eq_singleton_iff_nonempty_subsingleton.mpr ⟨_, fun a ha b hb => _⟩, _⟩
[GOAL]
case refine'_1
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
h : IsComplement S ⊤
⊢ Set.Nonempty S
[PROOFSTEP]
obtain ⟨a, _⟩ := h.2 1
[GOAL]
case refine'_1.intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
h : IsComplement S ⊤
a : ↑S × ↑⊤
h✝ : (fun x => ↑x.fst * ↑x.snd) a = 1
⊢ Set.Nonempty S
[PROOFSTEP]
exact ⟨a.1.1, a.1.2⟩
[GOAL]
case refine'_2
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
h : IsComplement S ⊤
a : G
ha : a ∈ S
b : G
hb : b ∈ S
⊢ a = b
[PROOFSTEP]
have : (⟨⟨a, ha⟩, ⟨_, mem_top a⁻¹⟩⟩ : S × (⊤ : Set G)) = ⟨⟨b, hb⟩, ⟨_, mem_top b⁻¹⟩⟩ :=
  h.1 ((mul_inv_self a).trans (mul_inv_self b).symm)
[GOAL]
case refine'_2
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
h : IsComplement S ⊤
a : G
ha : a ∈ S
b : G
hb : b ∈ S
this :
  ({ val := a, property := ha }, { val := a⁻¹, property := (_ : a⁻¹ ∈ ⊤) }) =
    ({ val := b, property := hb }, { val := b⁻¹, property := (_ : b⁻¹ ∈ ⊤) })
⊢ a = b
[PROOFSTEP]
exact Subtype.ext_iff.mp (Prod.ext_iff.mp this).1
[GOAL]
case refine'_3
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
⊢ (∃ g, S = {g}) → IsComplement S ⊤
[PROOFSTEP]
rintro ⟨g, rfl⟩
[GOAL]
case refine'_3.intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
T : Set G
g : G
⊢ IsComplement {g} ⊤
[PROOFSTEP]
exact isComplement_singleton_top
[GOAL]
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
⊢ S ∈ leftTransversals T ↔ ∀ (g : G), ∃! s, (↑s)⁻¹ * g ∈ T
[PROOFSTEP]
rw [leftTransversals, Set.mem_setOf_eq, isComplement_iff_existsUnique]
[GOAL]
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
⊢ (∀ (g : G), ∃! x, ↑x.fst * ↑x.snd = g) ↔ ∀ (g : G), ∃! s, (↑s)⁻¹ * g ∈ T
[PROOFSTEP]
refine' ⟨fun h g => _, fun h g => _⟩
[GOAL]
case refine'_1
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
h : ∀ (g : G), ∃! x, ↑x.fst * ↑x.snd = g
g : G
⊢ ∃! s, (↑s)⁻¹ * g ∈ T
[PROOFSTEP]
obtain ⟨x, h1, h2⟩ := h g
[GOAL]
case refine'_1.intro.intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
h : ∀ (g : G), ∃! x, ↑x.fst * ↑x.snd = g
g : G
x : ↑S × ↑T
h1 : ↑x.fst * ↑x.snd = g
h2 : ∀ (y : ↑S × ↑T), (fun x => ↑x.fst * ↑x.snd = g) y → y = x
⊢ ∃! s, (↑s)⁻¹ * g ∈ T
[PROOFSTEP]
exact
  ⟨x.1, (congr_arg (· ∈ T) (eq_inv_mul_of_mul_eq h1)).mp x.2.2, fun y hy =>
    (Prod.ext_iff.mp (h2 ⟨y, (↑y)⁻¹ * g, hy⟩ (mul_inv_cancel_left (↑y) g))).1⟩
[GOAL]
case refine'_2
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
h : ∀ (g : G), ∃! s, (↑s)⁻¹ * g ∈ T
g : G
⊢ ∃! x, ↑x.fst * ↑x.snd = g
[PROOFSTEP]
obtain ⟨x, h1, h2⟩ := h g
[GOAL]
case refine'_2.intro.intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
h : ∀ (g : G), ∃! s, (↑s)⁻¹ * g ∈ T
g : G
x : ↑S
h1 : (↑x)⁻¹ * g ∈ T
h2 : ∀ (y : ↑S), (fun s => (↑s)⁻¹ * g ∈ T) y → y = x
⊢ ∃! x, ↑x.fst * ↑x.snd = g
[PROOFSTEP]
refine' ⟨⟨x, (↑x)⁻¹ * g, h1⟩, mul_inv_cancel_left (↑x) g, fun y hy => _⟩
[GOAL]
case refine'_2.intro.intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
h : ∀ (g : G), ∃! s, (↑s)⁻¹ * g ∈ T
g : G
x : ↑S
h1 : (↑x)⁻¹ * g ∈ T
h2 : ∀ (y : ↑S), (fun s => (↑s)⁻¹ * g ∈ T) y → y = x
y : ↑S × ↑T
hy : (fun x => ↑x.fst * ↑x.snd = g) y
⊢ y = (x, { val := (↑x)⁻¹ * g, property := h1 })
[PROOFSTEP]
have hf := h2 y.1 ((congr_arg (· ∈ T) (eq_inv_mul_of_mul_eq hy)).mp y.2.2)
[GOAL]
case refine'_2.intro.intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
h : ∀ (g : G), ∃! s, (↑s)⁻¹ * g ∈ T
g : G
x : ↑S
h1 : (↑x)⁻¹ * g ∈ T
h2 : ∀ (y : ↑S), (fun s => (↑s)⁻¹ * g ∈ T) y → y = x
y : ↑S × ↑T
hy : (fun x => ↑x.fst * ↑x.snd = g) y
hf : y.fst = x
⊢ y = (x, { val := (↑x)⁻¹ * g, property := h1 })
[PROOFSTEP]
exact Prod.ext hf (Subtype.ext (eq_inv_mul_of_mul_eq (hf ▸ hy)))
[GOAL]
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
⊢ S ∈ rightTransversals T ↔ ∀ (g : G), ∃! s, g * (↑s)⁻¹ ∈ T
[PROOFSTEP]
rw [rightTransversals, Set.mem_setOf_eq, isComplement_iff_existsUnique]
[GOAL]
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
⊢ (∀ (g : G), ∃! x, ↑x.fst * ↑x.snd = g) ↔ ∀ (g : G), ∃! s, g * (↑s)⁻¹ ∈ T
[PROOFSTEP]
refine' ⟨fun h g => _, fun h g => _⟩
[GOAL]
case refine'_1
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
h : ∀ (g : G), ∃! x, ↑x.fst * ↑x.snd = g
g : G
⊢ ∃! s, g * (↑s)⁻¹ ∈ T
[PROOFSTEP]
obtain ⟨x, h1, h2⟩ := h g
[GOAL]
case refine'_1.intro.intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
h : ∀ (g : G), ∃! x, ↑x.fst * ↑x.snd = g
g : G
x : ↑T × ↑S
h1 : ↑x.fst * ↑x.snd = g
h2 : ∀ (y : ↑T × ↑S), (fun x => ↑x.fst * ↑x.snd = g) y → y = x
⊢ ∃! s, g * (↑s)⁻¹ ∈ T
[PROOFSTEP]
exact
  ⟨x.2, (congr_arg (· ∈ T) (eq_mul_inv_of_mul_eq h1)).mp x.1.2, fun y hy =>
    (Prod.ext_iff.mp (h2 ⟨⟨g * (↑y)⁻¹, hy⟩, y⟩ (inv_mul_cancel_right g y))).2⟩
[GOAL]
case refine'_2
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
h : ∀ (g : G), ∃! s, g * (↑s)⁻¹ ∈ T
g : G
⊢ ∃! x, ↑x.fst * ↑x.snd = g
[PROOFSTEP]
obtain ⟨x, h1, h2⟩ := h g
[GOAL]
case refine'_2.intro.intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
h : ∀ (g : G), ∃! s, g * (↑s)⁻¹ ∈ T
g : G
x : ↑S
h1 : g * (↑x)⁻¹ ∈ T
h2 : ∀ (y : ↑S), (fun s => g * (↑s)⁻¹ ∈ T) y → y = x
⊢ ∃! x, ↑x.fst * ↑x.snd = g
[PROOFSTEP]
refine' ⟨⟨⟨g * (↑x)⁻¹, h1⟩, x⟩, inv_mul_cancel_right g x, fun y hy => _⟩
[GOAL]
case refine'_2.intro.intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
h : ∀ (g : G), ∃! s, g * (↑s)⁻¹ ∈ T
g : G
x : ↑S
h1 : g * (↑x)⁻¹ ∈ T
h2 : ∀ (y : ↑S), (fun s => g * (↑s)⁻¹ ∈ T) y → y = x
y : ↑T × ↑S
hy : (fun x => ↑x.fst * ↑x.snd = g) y
⊢ y = ({ val := g * (↑x)⁻¹, property := h1 }, x)
[PROOFSTEP]
have hf := h2 y.2 ((congr_arg (· ∈ T) (eq_mul_inv_of_mul_eq hy)).mp y.1.2)
[GOAL]
case refine'_2.intro.intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
h : ∀ (g : G), ∃! s, g * (↑s)⁻¹ ∈ T
g : G
x : ↑S
h1 : g * (↑x)⁻¹ ∈ T
h2 : ∀ (y : ↑S), (fun s => g * (↑s)⁻¹ ∈ T) y → y = x
y : ↑T × ↑S
hy : (fun x => ↑x.fst * ↑x.snd = g) y
hf : y.snd = x
⊢ y = ({ val := g * (↑x)⁻¹, property := h1 }, x)
[PROOFSTEP]
exact Prod.ext (Subtype.ext (eq_mul_inv_of_mul_eq (hf ▸ hy))) hf
[GOAL]
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
⊢ S ∈ leftTransversals ↑H ↔ ∀ (q : Quotient (QuotientGroup.leftRel H)), ∃! s, Quotient.mk'' ↑s = q
[PROOFSTEP]
simp_rw [mem_leftTransversals_iff_existsUnique_inv_mul_mem, SetLike.mem_coe, ← QuotientGroup.eq']
[GOAL]
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
⊢ (∀ (g : G), ∃! s, ↑↑s = ↑g) ↔ ∀ (q : Quotient (QuotientGroup.leftRel H)), ∃! s, Quotient.mk'' ↑s = q
[PROOFSTEP]
exact ⟨fun h q => Quotient.inductionOn' q h, fun h g => h (Quotient.mk'' g)⟩
[GOAL]
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
⊢ S ∈ rightTransversals ↑H ↔ ∀ (q : Quotient (QuotientGroup.rightRel H)), ∃! s, Quotient.mk'' ↑s = q
[PROOFSTEP]
simp_rw [mem_rightTransversals_iff_existsUnique_mul_inv_mem, SetLike.mem_coe, ← QuotientGroup.rightRel_apply, ←
  Quotient.eq'']
[GOAL]
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
⊢ (∀ (g : G), ∃! s, Quotient.mk'' ↑s = Quotient.mk'' g) ↔
    ∀ (q : Quotient (QuotientGroup.rightRel H)), ∃! s, Quotient.mk'' ↑s = q
[PROOFSTEP]
exact ⟨fun h q => Quotient.inductionOn' q h, fun h g => h (Quotient.mk'' g)⟩
[GOAL]
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
f : G ⧸ H → G
hf : ∀ (q : G ⧸ H), ↑(f q) = q
⊢ Function.Injective (Set.restrict (Set.range f) Quotient.mk'')
[PROOFSTEP]
rintro ⟨-, q₁, rfl⟩ ⟨-, q₂, rfl⟩ h
[GOAL]
case mk.intro.mk.intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
f : G ⧸ H → G
hf : ∀ (q : G ⧸ H), ↑(f q) = q
q₁ q₂ : G ⧸ H
h :
  Set.restrict (Set.range f) Quotient.mk'' { val := f q₁, property := (_ : ∃ y, f y = f q₁) } =
    Set.restrict (Set.range f) Quotient.mk'' { val := f q₂, property := (_ : ∃ y, f y = f q₂) }
⊢ { val := f q₁, property := (_ : ∃ y, f y = f q₁) } = { val := f q₂, property := (_ : ∃ y, f y = f q₂) }
[PROOFSTEP]
exact Subtype.ext $ congr_arg f $ ((hf q₁).symm.trans h).trans (hf q₂)
[GOAL]
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
f : Quotient (QuotientGroup.rightRel H) → G
hf : ∀ (q : Quotient (QuotientGroup.rightRel H)), Quotient.mk'' (f q) = q
⊢ Function.Injective (Set.restrict (Set.range f) Quotient.mk'')
[PROOFSTEP]
rintro ⟨-, q₁, rfl⟩ ⟨-, q₂, rfl⟩ h
[GOAL]
case mk.intro.mk.intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
f : Quotient (QuotientGroup.rightRel H) → G
hf : ∀ (q : Quotient (QuotientGroup.rightRel H)), Quotient.mk'' (f q) = q
q₁ q₂ : Quotient (QuotientGroup.rightRel H)
h :
  Set.restrict (Set.range f) Quotient.mk'' { val := f q₁, property := (_ : ∃ y, f y = f q₁) } =
    Set.restrict (Set.range f) Quotient.mk'' { val := f q₂, property := (_ : ∃ y, f y = f q₂) }
⊢ { val := f q₁, property := (_ : ∃ y, f y = f q₁) } = { val := f q₂, property := (_ : ∃ y, f y = f q₂) }
[PROOFSTEP]
exact Subtype.ext $ congr_arg f $ ((hf q₁).symm.trans h).trans (hf q₂)
[GOAL]
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
g : G
⊢ ∃ S, S ∈ leftTransversals ↑H ∧ g ∈ S
[PROOFSTEP]
classical
refine'
  ⟨Set.range (Function.update Quotient.out' _ g), range_mem_leftTransversals fun q => _, Quotient.mk'' g,
    Function.update_same (Quotient.mk'' g) g Quotient.out'⟩
by_cases hq : q = Quotient.mk'' g
· exact hq.symm ▸ congr_arg _ (Function.update_same (Quotient.mk'' g) g Quotient.out')
· refine' (Function.update_noteq _ g Quotient.out') ▸ q.out_eq'
  exact hq
[GOAL]
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
g : G
⊢ ∃ S, S ∈ leftTransversals ↑H ∧ g ∈ S
[PROOFSTEP]
refine'
  ⟨Set.range (Function.update Quotient.out' _ g), range_mem_leftTransversals fun q => _, Quotient.mk'' g,
    Function.update_same (Quotient.mk'' g) g Quotient.out'⟩
[GOAL]
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
g : G
q : G ⧸ H
⊢ ↑(Function.update Quotient.out' (Quotient.mk'' g) g q) = q
[PROOFSTEP]
by_cases hq : q = Quotient.mk'' g
[GOAL]
case pos
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
g : G
q : G ⧸ H
hq : q = Quotient.mk'' g
⊢ ↑(Function.update Quotient.out' (Quotient.mk'' g) g q) = q
[PROOFSTEP]
exact hq.symm ▸ congr_arg _ (Function.update_same (Quotient.mk'' g) g Quotient.out')
[GOAL]
case neg
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
g : G
q : G ⧸ H
hq : ¬q = Quotient.mk'' g
⊢ ↑(Function.update Quotient.out' (Quotient.mk'' g) g q) = q
[PROOFSTEP]
refine' (Function.update_noteq _ g Quotient.out') ▸ q.out_eq'
[GOAL]
case neg
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
g : G
q : G ⧸ H
hq : ¬q = Quotient.mk'' g
⊢ q ≠ Quotient.mk'' g
[PROOFSTEP]
exact hq
[GOAL]
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
g : G
⊢ ∃ S, S ∈ rightTransversals ↑H ∧ g ∈ S
[PROOFSTEP]
classical
refine'
  ⟨Set.range (Function.update Quotient.out' _ g), range_mem_rightTransversals fun q => _, Quotient.mk'' g,
    Function.update_same (Quotient.mk'' g) g Quotient.out'⟩
by_cases hq : q = Quotient.mk'' g
· exact hq.symm ▸ congr_arg _ (Function.update_same (Quotient.mk'' g) g Quotient.out')
· exact Eq.trans (congr_arg _ (Function.update_noteq hq g Quotient.out')) q.out_eq'
[GOAL]
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
g : G
⊢ ∃ S, S ∈ rightTransversals ↑H ∧ g ∈ S
[PROOFSTEP]
refine'
  ⟨Set.range (Function.update Quotient.out' _ g), range_mem_rightTransversals fun q => _, Quotient.mk'' g,
    Function.update_same (Quotient.mk'' g) g Quotient.out'⟩
[GOAL]
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
g : G
q : Quotient (QuotientGroup.rightRel H)
⊢ Quotient.mk'' (Function.update Quotient.out' (Quotient.mk'' g) g q) = q
[PROOFSTEP]
by_cases hq : q = Quotient.mk'' g
[GOAL]
case pos
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
g : G
q : Quotient (QuotientGroup.rightRel H)
hq : q = Quotient.mk'' g
⊢ Quotient.mk'' (Function.update Quotient.out' (Quotient.mk'' g) g q) = q
[PROOFSTEP]
exact hq.symm ▸ congr_arg _ (Function.update_same (Quotient.mk'' g) g Quotient.out')
[GOAL]
case neg
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
g : G
q : Quotient (QuotientGroup.rightRel H)
hq : ¬q = Quotient.mk'' g
⊢ Quotient.mk'' (Function.update Quotient.out' (Quotient.mk'' g) g q) = q
[PROOFSTEP]
exact Eq.trans (congr_arg _ (Function.update_noteq hq g Quotient.out')) q.out_eq'
[GOAL]
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
f : G ⧸ H → G
hf : ∀ (q : G ⧸ H), ↑(f q) = q
q : G ⧸ H
⊢ ↑(↑(toEquiv (_ : (Set.range fun q => f q) ∈ leftTransversals ↑H)) q) = f q
[PROOFSTEP]
refine' (Subtype.ext_iff.mp _).trans (Subtype.coe_mk (f q) ⟨q, rfl⟩)
[GOAL]
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
f : G ⧸ H → G
hf : ∀ (q : G ⧸ H), ↑(f q) = q
q : G ⧸ H
⊢ ↑(toEquiv (_ : (Set.range fun q => f q) ∈ leftTransversals ↑H)) q =
    { val := f q, property := (_ : ∃ y, (fun q => f q) y = f q) }
[PROOFSTEP]
exact (toEquiv (range_mem_leftTransversals hf)).apply_eq_iff_eq_symm_apply.mpr (hf q).symm
[GOAL]
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
hS : S ∈ leftTransversals ↑H
g : G
⊢ ((↑(toFun hS g))⁻¹ * g)⁻¹ = g⁻¹ * ↑(toFun hS g)
[PROOFSTEP]
rw [mul_inv_rev, inv_inv]
[GOAL]
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
f : Quotient (QuotientGroup.rightRel H) → G
hf : ∀ (q : Quotient (QuotientGroup.rightRel H)), Quotient.mk'' (f q) = q
q : Quotient (QuotientGroup.rightRel H)
⊢ ↑(↑(toEquiv (_ : (Set.range fun q => f q) ∈ rightTransversals ↑H)) q) = f q
[PROOFSTEP]
refine' (Subtype.ext_iff.mp _).trans (Subtype.coe_mk (f q) ⟨q, rfl⟩)
[GOAL]
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
f : Quotient (QuotientGroup.rightRel H) → G
hf : ∀ (q : Quotient (QuotientGroup.rightRel H)), Quotient.mk'' (f q) = q
q : Quotient (QuotientGroup.rightRel H)
⊢ ↑(toEquiv (_ : (Set.range fun q => f q) ∈ rightTransversals ↑H)) q =
    { val := f q, property := (_ : ∃ y, (fun q => f q) y = f q) }
[PROOFSTEP]
exact (toEquiv (range_mem_rightTransversals hf)).apply_eq_iff_eq_symm_apply.mpr (hf q).symm
[GOAL]
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
hS : S ∈ rightTransversals ↑H
g : G
⊢ (g * (↑(toFun hS g))⁻¹)⁻¹ = ↑(toFun hS g) * g⁻¹
[PROOFSTEP]
rw [mul_inv_rev, inv_inv]
[GOAL]
G : Type u_1
inst✝³ : Group G
H K : Subgroup G
S T✝ : Set G
F : Type u_2
inst✝² : Group F
inst✝¹ : MulAction F G
inst✝ : QuotientAction F H
f : F
T : ↑(leftTransversals ↑H)
⊢ f • ↑T ∈ leftTransversals ↑H
[PROOFSTEP]
refine' mem_leftTransversals_iff_existsUnique_inv_mul_mem.mpr fun g => _
[GOAL]
G : Type u_1
inst✝³ : Group G
H K : Subgroup G
S T✝ : Set G
F : Type u_2
inst✝² : Group F
inst✝¹ : MulAction F G
inst✝ : QuotientAction F H
f : F
T : ↑(leftTransversals ↑H)
g : G
⊢ ∃! s, (↑s)⁻¹ * g ∈ ↑H
[PROOFSTEP]
obtain ⟨t, ht1, ht2⟩ := mem_leftTransversals_iff_existsUnique_inv_mul_mem.mp T.2 (f⁻¹ • g)
[GOAL]
case intro.intro
G : Type u_1
inst✝³ : Group G
H K : Subgroup G
S T✝ : Set G
F : Type u_2
inst✝² : Group F
inst✝¹ : MulAction F G
inst✝ : QuotientAction F H
f : F
T : ↑(leftTransversals ↑H)
g : G
t : ↑↑T
ht1 : (↑t)⁻¹ * f⁻¹ • g ∈ ↑H
ht2 : ∀ (y : ↑↑T), (fun s => (↑s)⁻¹ * f⁻¹ • g ∈ ↑H) y → y = t
⊢ ∃! s, (↑s)⁻¹ * g ∈ ↑H
[PROOFSTEP]
refine' ⟨⟨f • (t : G), Set.smul_mem_smul_set t.2⟩, _, _⟩
[GOAL]
case intro.intro.refine'_1
G : Type u_1
inst✝³ : Group G
H K : Subgroup G
S T✝ : Set G
F : Type u_2
inst✝² : Group F
inst✝¹ : MulAction F G
inst✝ : QuotientAction F H
f : F
T : ↑(leftTransversals ↑H)
g : G
t : ↑↑T
ht1 : (↑t)⁻¹ * f⁻¹ • g ∈ ↑H
ht2 : ∀ (y : ↑↑T), (fun s => (↑s)⁻¹ * f⁻¹ • g ∈ ↑H) y → y = t
⊢ (fun s => (↑s)⁻¹ * g ∈ ↑H) { val := f • ↑t, property := (_ : f • ↑t ∈ f • ↑T) }
[PROOFSTEP]
exact smul_inv_smul f g ▸ QuotientAction.inv_mul_mem f ht1
[GOAL]
case intro.intro.refine'_2
G : Type u_1
inst✝³ : Group G
H K : Subgroup G
S T✝ : Set G
F : Type u_2
inst✝² : Group F
inst✝¹ : MulAction F G
inst✝ : QuotientAction F H
f : F
T : ↑(leftTransversals ↑H)
g : G
t : ↑↑T
ht1 : (↑t)⁻¹ * f⁻¹ • g ∈ ↑H
ht2 : ∀ (y : ↑↑T), (fun s => (↑s)⁻¹ * f⁻¹ • g ∈ ↑H) y → y = t
⊢ ∀ (y : ↑(f • ↑T)), (fun s => (↑s)⁻¹ * g ∈ ↑H) y → y = { val := f • ↑t, property := (_ : f • ↑t ∈ f • ↑T) }
[PROOFSTEP]
rintro ⟨-, t', ht', rfl⟩ h
[GOAL]
case intro.intro.refine'_2.mk.intro.intro
G : Type u_1
inst✝³ : Group G
H K : Subgroup G
S T✝ : Set G
F : Type u_2
inst✝² : Group F
inst✝¹ : MulAction F G
inst✝ : QuotientAction F H
f : F
T : ↑(leftTransversals ↑H)
g : G
t : ↑↑T
ht1 : (↑t)⁻¹ * f⁻¹ • g ∈ ↑H
ht2 : ∀ (y : ↑↑T), (fun s => (↑s)⁻¹ * f⁻¹ • g ∈ ↑H) y → y = t
t' : G
ht' : t' ∈ ↑T
h :
  (↑{ val := (fun x => f • x) t', property := (_ : ∃ a, a ∈ ↑T ∧ (fun x => f • x) a = (fun x => f • x) t') })⁻¹ * g ∈ ↑H
⊢ { val := (fun x => f • x) t', property := (_ : ∃ a, a ∈ ↑T ∧ (fun x => f • x) a = (fun x => f • x) t') } =
    { val := f • ↑t, property := (_ : f • ↑t ∈ f • ↑T) }
[PROOFSTEP]
replace h := QuotientAction.inv_mul_mem f⁻¹ h
[GOAL]
case intro.intro.refine'_2.mk.intro.intro
G : Type u_1
inst✝³ : Group G
H K : Subgroup G
S T✝ : Set G
F : Type u_2
inst✝² : Group F
inst✝¹ : MulAction F G
inst✝ : QuotientAction F H
f : F
T : ↑(leftTransversals ↑H)
g : G
t : ↑↑T
ht1 : (↑t)⁻¹ * f⁻¹ • g ∈ ↑H
ht2 : ∀ (y : ↑↑T), (fun s => (↑s)⁻¹ * f⁻¹ • g ∈ ↑H) y → y = t
t' : G
ht' : t' ∈ ↑T
h :
  (f⁻¹ • ↑{ val := (fun x => f • x) t', property := (_ : ∃ a, a ∈ ↑T ∧ (fun x => f • x) a = (fun x => f • x) t') })⁻¹ *
      f⁻¹ • g ∈
    H
⊢ { val := (fun x => f • x) t', property := (_ : ∃ a, a ∈ ↑T ∧ (fun x => f • x) a = (fun x => f • x) t') } =
    { val := f • ↑t, property := (_ : f • ↑t ∈ f • ↑T) }
[PROOFSTEP]
simp only [Subtype.ext_iff, Subtype.coe_mk, smul_left_cancel_iff, inv_smul_smul] at h ⊢
[GOAL]
case intro.intro.refine'_2.mk.intro.intro
G : Type u_1
inst✝³ : Group G
H K : Subgroup G
S T✝ : Set G
F : Type u_2
inst✝² : Group F
inst✝¹ : MulAction F G
inst✝ : QuotientAction F H
f : F
T : ↑(leftTransversals ↑H)
g : G
t : ↑↑T
ht1 : (↑t)⁻¹ * f⁻¹ • g ∈ ↑H
ht2 : ∀ (y : ↑↑T), (fun s => (↑s)⁻¹ * f⁻¹ • g ∈ ↑H) y → y = t
t' : G
ht' : t' ∈ ↑T
h : t'⁻¹ * f⁻¹ • g ∈ H
⊢ t' = ↑t
[PROOFSTEP]
exact Subtype.ext_iff.mp (ht2 ⟨t', ht'⟩ h)
[GOAL]
G : Type u_1
inst✝³ : Group G
H K : Subgroup G
S T✝ : Set G
F : Type u_2
inst✝² : Group F
inst✝¹ : MulAction F G
inst✝ : QuotientAction F H
f : F
T : ↑(leftTransversals ↑H)
q : G ⧸ H
⊢ ↑(↑(toEquiv (_ : ↑(f • T) ∈ leftTransversals ↑H)) q) = f • ↑(↑(toEquiv (_ : ↑T ∈ leftTransversals ↑H)) (f⁻¹ • q))
[PROOFSTEP]
rw [smul_toEquiv, smul_inv_smul]
[GOAL]
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
h : IsComplement' H K
⊢ IsCompl H K
[PROOFSTEP]
refine'
  ⟨disjoint_iff_inf_le.mpr fun g ⟨p, q⟩ =>
      let x : H × K := ⟨⟨g, p⟩, 1⟩
      let y : H × K := ⟨1, g, q⟩
      Subtype.ext_iff.mp (Prod.ext_iff.mp (show x = y from h.1 ((mul_one g).trans (one_mul g).symm))).1,
    codisjoint_iff_le_sup.mpr fun g _ => _⟩
[GOAL]
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
h : IsComplement' H K
g : G
x✝ : g ∈ ⊤
⊢ g ∈ H ⊔ K
[PROOFSTEP]
obtain ⟨⟨h, k⟩, rfl⟩ := h.2 g
[GOAL]
case intro.mk
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
h✝ : IsComplement' H K
h : ↑↑H
k : ↑↑K
x✝ : (fun x => ↑x.fst * ↑x.snd) (h, k) ∈ ⊤
⊢ (fun x => ↑x.fst * ↑x.snd) (h, k) ∈ H ⊔ K
[PROOFSTEP]
exact Subgroup.mul_mem_sup h.2 k.2
[GOAL]
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
h1 : Disjoint H K
h2 : ↑H * ↑K = Set.univ
⊢ IsComplement' H K
[PROOFSTEP]
refine' ⟨mul_injective_of_disjoint h1, fun g => _⟩
[GOAL]
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
h1 : Disjoint H K
h2 : ↑H * ↑K = Set.univ
g : G
⊢ ∃ a, (fun x => ↑x.fst * ↑x.snd) a = g
[PROOFSTEP]
obtain ⟨h, k, hh, hk, hg⟩ := Set.eq_univ_iff_forall.mp h2 g
[GOAL]
case intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
h1 : Disjoint H K
h2 : ↑H * ↑K = Set.univ
g h k : G
hh : h ∈ ↑H
hk : k ∈ ↑K
hg : (fun x x_1 => x * x_1) h k = g
⊢ ∃ a, (fun x => ↑x.fst * ↑x.snd) a = g
[PROOFSTEP]
exact ⟨(⟨h, hh⟩, ⟨k, hk⟩), hg⟩
[GOAL]
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
S T : Set G
α : Type u_2
inst✝ : MulAction G α
a : α
h1 : ∀ (h : { x // x ∈ H }), h • a = a → h = 1
h2 : ∀ (g : G), ∃ h, h • g • a = a
⊢ IsComplement' H (MulAction.stabilizer G a)
[PROOFSTEP]
refine' isComplement_iff_existsUnique.mpr fun g => _
[GOAL]
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
S T : Set G
α : Type u_2
inst✝ : MulAction G α
a : α
h1 : ∀ (h : { x // x ∈ H }), h • a = a → h = 1
h2 : ∀ (g : G), ∃ h, h • g • a = a
g : G
⊢ ∃! x, ↑x.fst * ↑x.snd = g
[PROOFSTEP]
obtain ⟨h, hh⟩ := h2 g
[GOAL]
case intro
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
S T : Set G
α : Type u_2
inst✝ : MulAction G α
a : α
h1 : ∀ (h : { x // x ∈ H }), h • a = a → h = 1
h2 : ∀ (g : G), ∃ h, h • g • a = a
g : G
h : { x // x ∈ H }
hh : h • g • a = a
⊢ ∃! x, ↑x.fst * ↑x.snd = g
[PROOFSTEP]
have hh' : (↑h * g) • a = a := by rwa [mul_smul]
[GOAL]
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
S T : Set G
α : Type u_2
inst✝ : MulAction G α
a : α
h1 : ∀ (h : { x // x ∈ H }), h • a = a → h = 1
h2 : ∀ (g : G), ∃ h, h • g • a = a
g : G
h : { x // x ∈ H }
hh : h • g • a = a
⊢ (↑h * g) • a = a
[PROOFSTEP]
rwa [mul_smul]
[GOAL]
case intro
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
S T : Set G
α : Type u_2
inst✝ : MulAction G α
a : α
h1 : ∀ (h : { x // x ∈ H }), h • a = a → h = 1
h2 : ∀ (g : G), ∃ h, h • g • a = a
g : G
h : { x // x ∈ H }
hh : h • g • a = a
hh' : (↑h * g) • a = a
⊢ ∃! x, ↑x.fst * ↑x.snd = g
[PROOFSTEP]
refine' ⟨⟨h⁻¹, h * g, hh'⟩, inv_mul_cancel_left (↑h) g, _⟩
[GOAL]
case intro
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
S T : Set G
α : Type u_2
inst✝ : MulAction G α
a : α
h1 : ∀ (h : { x // x ∈ H }), h • a = a → h = 1
h2 : ∀ (g : G), ∃ h, h • g • a = a
g : G
h : { x // x ∈ H }
hh : h • g • a = a
hh' : (↑h * g) • a = a
⊢ ∀ (y : ↑↑H × ↑↑(MulAction.stabilizer G a)),
    (fun x => ↑x.fst * ↑x.snd = g) y → y = (h⁻¹, { val := ↑h * g, property := hh' })
[PROOFSTEP]
rintro ⟨h', g, hg : g • a = a⟩ rfl
[GOAL]
case intro.mk.mk
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
S T : Set G
α : Type u_2
inst✝ : MulAction G α
a : α
h1 : ∀ (h : { x // x ∈ H }), h • a = a → h = 1
h2 : ∀ (g : G), ∃ h, h • g • a = a
h : { x // x ∈ H }
h' : ↑↑H
g : G
hg : g • a = a
hh : h • (↑(h', { val := g, property := hg }).fst * ↑(h', { val := g, property := hg }).snd) • a = a
hh' : (↑h * (↑(h', { val := g, property := hg }).fst * ↑(h', { val := g, property := hg }).snd)) • a = a
⊢ (h', { val := g, property := hg }) =
    (h⁻¹,
      { val := ↑h * (↑(h', { val := g, property := hg }).fst * ↑(h', { val := g, property := hg }).snd),
        property := hh' })
[PROOFSTEP]
specialize h1 (h * h') (by rwa [mul_smul, smul_def h', ← hg, ← mul_smul, hg])
[GOAL]
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
S T : Set G
α : Type u_2
inst✝ : MulAction G α
a : α
h1 : ∀ (h : { x // x ∈ H }), h • a = a → h = 1
h2 : ∀ (g : G), ∃ h, h • g • a = a
h : { x // x ∈ H }
h' : ↑↑H
g : G
hg : g • a = a
hh : h • (↑(h', { val := g, property := hg }).fst * ↑(h', { val := g, property := hg }).snd) • a = a
hh' : (↑h * (↑(h', { val := g, property := hg }).fst * ↑(h', { val := g, property := hg }).snd)) • a = a
⊢ (h * h') • a = a
[PROOFSTEP]
rwa [mul_smul, smul_def h', ← hg, ← mul_smul, hg]
[GOAL]
case intro.mk.mk
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
S T : Set G
α : Type u_2
inst✝ : MulAction G α
a : α
h2 : ∀ (g : G), ∃ h, h • g • a = a
h : { x // x ∈ H }
h' : ↑↑H
g : G
hg : g • a = a
hh : h • (↑(h', { val := g, property := hg }).fst * ↑(h', { val := g, property := hg }).snd) • a = a
hh' : (↑h * (↑(h', { val := g, property := hg }).fst * ↑(h', { val := g, property := hg }).snd)) • a = a
h1 : h * h' = 1
⊢ (h', { val := g, property := hg }) =
    (h⁻¹,
      { val := ↑h * (↑(h', { val := g, property := hg }).fst * ↑(h', { val := g, property := hg }).snd),
        property := hh' })
[PROOFSTEP]
refine' Prod.ext (eq_inv_of_mul_eq_one_right h1) (Subtype.ext _)
[GOAL]
case intro.mk.mk
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
S T : Set G
α : Type u_2
inst✝ : MulAction G α
a : α
h2 : ∀ (g : G), ∃ h, h • g • a = a
h : { x // x ∈ H }
h' : ↑↑H
g : G
hg : g • a = a
hh : h • (↑(h', { val := g, property := hg }).fst * ↑(h', { val := g, property := hg }).snd) • a = a
hh' : (↑h * (↑(h', { val := g, property := hg }).fst * ↑(h', { val := g, property := hg }).snd)) • a = a
h1 : h * h' = 1
⊢ ↑(h', { val := g, property := hg }).snd =
    ↑(h⁻¹,
          { val := ↑h * (↑(h', { val := g, property := hg }).fst * ↑(h', { val := g, property := hg }).snd),
            property := hh' }).snd
[PROOFSTEP]
rwa [Subtype.ext_iff, coe_one, coe_mul, ← self_eq_mul_left, mul_assoc (↑h) (↑h') g] at h1 
[GOAL]
G : Type u
inst✝ : Group G
H : Subgroup G
g : G
q : orbitRel.Quotient { x // x ∈ zpowers g } (G ⧸ H)
k : ℤ
⊢ ↑(quotientEquivSigmaZMod H g) (g ^ k • Quotient.out' q) = { fst := q, snd := ↑k }
[PROOFSTEP]
rw [apply_eq_iff_eq_symm_apply, quotientEquivSigmaZMod_symm_apply, ZMod.coe_int_cast, zpow_smul_mod_minimalPeriod]
[GOAL]
G : Type u
inst✝ : Group G
H : Subgroup G
g : G
q : G ⧸ H
⊢ ↑(transferFunction H g q) = q
[PROOFSTEP]
rw [transferFunction_apply, ← smul_eq_mul, Quotient.coe_smul_out', ← quotientEquivSigmaZMod_symm_apply, Sigma.eta,
  symm_apply_apply]
[GOAL]
G : Type u
inst✝ : Group G
H : Subgroup G
g : G
q : orbitRel.Quotient { x // x ∈ zpowers g } (G ⧸ H)
k : ZMod (minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q))
⊢ ↑(↑(toEquiv (_ : ↑(transferTransversal H g) ∈ leftTransversals ↑H)) (g ^ ↑k • Quotient.out' q)) =
    g ^ ↑k * Quotient.out' (Quotient.out' q)
[PROOFSTEP]
rw [transferTransversal_apply, transferFunction_apply, ← quotientEquivSigmaZMod_symm_apply, apply_symm_apply]
[GOAL]
G : Type u
inst✝ : Group G
H : Subgroup G
g : G
q : orbitRel.Quotient { x // x ∈ zpowers g } (G ⧸ H)
k : ZMod (minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q))
⊢ ↑(↑(toEquiv (_ : ↑(g • transferTransversal H g) ∈ leftTransversals ↑H)) (g ^ ↑k • Quotient.out' q)) =
    if k = 0 then g ^ minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q) * Quotient.out' (Quotient.out' q)
    else g ^ ↑k * Quotient.out' (Quotient.out' q)
[PROOFSTEP]
rw [smul_apply_eq_smul_apply_inv_smul, transferTransversal_apply, transferFunction_apply, ← mul_smul, ← zpow_neg_one, ←
  zpow_add, quotientEquivSigmaZMod_apply, smul_eq_mul, ← mul_assoc, ← zpow_one_add, Int.cast_add, Int.cast_neg,
  Int.cast_one, int_cast_cast, cast_id', id.def, ← sub_eq_neg_add, cast_sub_one, add_sub_cancel'_right]
[GOAL]
G : Type u
inst✝ : Group G
H : Subgroup G
g : G
q : orbitRel.Quotient { x // x ∈ zpowers g } (G ⧸ H)
k : ZMod (minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q))
⊢ (g ^
        if k = 0 then ↑(minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' { fst := q, snd := k - 1 }.fst))
        else ↑k) *
      Quotient.out' (Quotient.out' { fst := q, snd := k - 1 }.fst) =
    if k = 0 then g ^ minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q) * Quotient.out' (Quotient.out' q)
    else g ^ ↑k * Quotient.out' (Quotient.out' q)
[PROOFSTEP]
by_cases hk : k = 0
[GOAL]
case pos
G : Type u
inst✝ : Group G
H : Subgroup G
g : G
q : orbitRel.Quotient { x // x ∈ zpowers g } (G ⧸ H)
k : ZMod (minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q))
hk : k = 0
⊢ (g ^
        if k = 0 then ↑(minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' { fst := q, snd := k - 1 }.fst))
        else ↑k) *
      Quotient.out' (Quotient.out' { fst := q, snd := k - 1 }.fst) =
    if k = 0 then g ^ minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q) * Quotient.out' (Quotient.out' q)
    else g ^ ↑k * Quotient.out' (Quotient.out' q)
[PROOFSTEP]
rw [if_pos hk, if_pos hk, zpow_ofNat]
[GOAL]
case neg
G : Type u
inst✝ : Group G
H : Subgroup G
g : G
q : orbitRel.Quotient { x // x ∈ zpowers g } (G ⧸ H)
k : ZMod (minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q))
hk : ¬k = 0
⊢ (g ^
        if k = 0 then ↑(minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' { fst := q, snd := k - 1 }.fst))
        else ↑k) *
      Quotient.out' (Quotient.out' { fst := q, snd := k - 1 }.fst) =
    if k = 0 then g ^ minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q) * Quotient.out' (Quotient.out' q)
    else g ^ ↑k * Quotient.out' (Quotient.out' q)
[PROOFSTEP]
rw [if_neg hk, if_neg hk]
