[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]


[GOAL]
α : Type u_1
M : Type ?u.8804
N : Type ?u.8800
inst✝² : Mul N
inst✝¹ : SMul M N
inst✝ : IsScalarTower M N N
x : M
y : Nᵐᵒᵖ
z : N
⊢ x • y • z = y • x • z
[PROOFSTEP]
induction y using MulOpposite.rec'
[GOAL]
case h
α : Type u_1
M : Type ?u.8804
N : Type ?u.8800
inst✝² : Mul N
inst✝¹ : SMul M N
inst✝ : IsScalarTower M N N
x : M
z X✝ : N
⊢ x • op X✝ • z = op X✝ • x • z
[PROOFSTEP]
simp only [smul_mul_assoc, MulOpposite.smul_eq_mul_unop]


[GOAL]
M : Type u_1
N : Type u_2
α : Type u_3
inst✝³ : SMul M α
inst✝² : SMul N α
a✝ : M
b✝ : α
x✝ : Option α
inst✝¹ : SMul M N
inst✝ : IsScalarTower M N α
a : M
b : N
x : Option α
⊢ (a • b) • x = a • b • x
[PROOFSTEP]
cases x
[GOAL]
case none
M : Type u_1
N : Type u_2
α : Type u_3
inst✝³ : SMul M α
inst✝² : SMul N α
a✝ : M
b✝ : α
x : Option α
inst✝¹ : SMul M N
inst✝ : IsScalarTower M N α
a : M
b : N
⊢ (a • b) • none = a • b • none
case some
M : Type u_1
N : Type u_2
α : Type u_3
inst✝³ : SMul M α
inst✝² : SMul N α
a✝ : M
b✝ : α
x : Option α
inst✝¹ : SMul M N
inst✝ : IsScalarTower M N α
a : M
b : N
val✝ : α
⊢ (a • b) • some val✝ = a • b • some val✝
[PROOFSTEP]
exacts [rfl, congr_arg some (smul_assoc _ _ _)]
[GOAL]
M : Type u_1
N : Type u_2
α : Type u_3
inst✝³ : SMul M α
inst✝² : SMul N α
a✝ : M
b : α
x✝ : Option α
inst✝¹ : SMul Mᵐᵒᵖ α
inst✝ : IsCentralScalar M α
a : M
x : Option α
⊢ MulOpposite.op a • x = a • x
[PROOFSTEP]
cases x
[GOAL]
case none
M : Type u_1
N : Type u_2
α : Type u_3
inst✝³ : SMul M α
inst✝² : SMul N α
a✝ : M
b : α
x : Option α
inst✝¹ : SMul Mᵐᵒᵖ α
inst✝ : IsCentralScalar M α
a : M
⊢ MulOpposite.op a • none = a • none
case some
M : Type u_1
N : Type u_2
α : Type u_3
inst✝³ : SMul M α
inst✝² : SMul N α
a✝ : M
b : α
x : Option α
inst✝¹ : SMul Mᵐᵒᵖ α
inst✝ : IsCentralScalar M α
a : M
val✝ : α
⊢ MulOpposite.op a • some val✝ = a • some val✝
[PROOFSTEP]
exacts [rfl, congr_arg some (op_smul_eq_smul _ _)]
[GOAL]
M : Type u_1
N : Type u_2
α : Type u_3
inst✝² : SMul M α
inst✝¹ : SMul N α
a : M
b✝ : α
x : Option α
inst✝ : FaithfulSMul M α
m₁✝ m₂✝ : M
h : ∀ (a : Option α), m₁✝ • a = m₂✝ • a
b : α
⊢ m₁✝ • b = m₂✝ • b
[PROOFSTEP]
injection h (some b)
[GOAL]
M : Type u_1
N : Type u_2
α : Type u_3
inst✝¹ : Monoid M
inst✝ : MulAction M α
b : Option α
⊢ 1 • b = b
[PROOFSTEP]
cases b
[GOAL]
case none
M : Type u_1
N : Type u_2
α : Type u_3
inst✝¹ : Monoid M
inst✝ : MulAction M α
⊢ 1 • none = none
case some
M : Type u_1
N : Type u_2
α : Type u_3
inst✝¹ : Monoid M
inst✝ : MulAction M α
val✝ : α
⊢ 1 • some val✝ = some val✝
[PROOFSTEP]
exacts [rfl, congr_arg some (one_smul _ _)]
[GOAL]
M : Type u_1
N : Type u_2
α : Type u_3
inst✝¹ : Monoid M
inst✝ : MulAction M α
a₁ a₂ : M
b : Option α
⊢ (a₁ * a₂) • b = a₁ • a₂ • b
[PROOFSTEP]
cases b
[GOAL]
case none
M : Type u_1
N : Type u_2
α : Type u_3
inst✝¹ : Monoid M
inst✝ : MulAction M α
a₁ a₂ : M
⊢ (a₁ * a₂) • none = a₁ • a₂ • none
case some
M : Type u_1
N : Type u_2
α : Type u_3
inst✝¹ : Monoid M
inst✝ : MulAction M α
a₁ a₂ : M
val✝ : α
⊢ (a₁ * a₂) • some val✝ = a₁ • a₂ • some val✝
[PROOFSTEP]
exacts [rfl, congr_arg some (mul_smul _ _ _)]


[GOAL]
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
α : Type u_5
inst✝⁴ : Group G
inst✝³ : Monoid M
inst✝² : MulAction G M
inst✝¹ : SMulCommClass G M M
inst✝ : IsScalarTower G M M
g : G
m : Mˣ
⊢ g • ↑m * g⁻¹ • ↑m⁻¹ = 1
[PROOFSTEP]
rw [smul_mul_smul, Units.mul_inv, mul_right_inv, one_smul]
[GOAL]
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
α : Type u_5
inst✝⁴ : Group G
inst✝³ : Monoid M
inst✝² : MulAction G M
inst✝¹ : SMulCommClass G M M
inst✝ : IsScalarTower G M M
g : G
m : Mˣ
⊢ g⁻¹ • ↑m⁻¹ * g • ↑m = 1
[PROOFSTEP]
rw [smul_mul_smul, Units.inv_mul, mul_left_inv, one_smul]


[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α✝ : Type u_5
β : Type u_6
inst✝⁶ : SMul M α✝
inst✝⁵ : SMul M β
inst✝⁴ : SMul N α✝
inst✝³ : SMul N β
a✝ : M
x : α✝ × β
α : Type u_7
inst✝² : Monoid M
inst✝¹ : AddMonoid α
inst✝ : DistribMulAction M α
a : M
c : β
⊢ a • (0, c) = (0, a • c)
[PROOFSTEP]
rw [Prod.smul_mk, smul_zero]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β✝ : Type u_6
inst✝⁶ : SMul M α
inst✝⁵ : SMul M β✝
inst✝⁴ : SMul N α
inst✝³ : SMul N β✝
a✝ : M
x : α × β✝
β : Type u_7
inst✝² : Monoid M
inst✝¹ : AddMonoid β
inst✝ : DistribMulAction M β
a : M
b : α
⊢ a • (b, 0) = (a • b, 0)
[PROOFSTEP]
rw [Prod.smul_mk, smul_zero]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝⁷ : SMul M α
inst✝⁶ : SMul M β
inst✝⁵ : SMul N α
inst✝⁴ : SMul N β
a✝ : M
x : α × β
inst✝³ : Pow α E
inst✝² : Pow β E
inst✝¹ : FaithfulSMul M α
inst✝ : Nonempty β
m₁✝ m₂✝ : M
h : ∀ (a : α × β), m₁✝ • a = m₂✝ • a
b : β
a : α
⊢ m₁✝ • a = m₂✝ • a
[PROOFSTEP]
injection h (a, b)
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝⁷ : SMul M α
inst✝⁶ : SMul M β
inst✝⁵ : SMul N α
inst✝⁴ : SMul N β
a✝ : M
x : α × β
inst✝³ : Pow α E
inst✝² : Pow β E
inst✝¹ : Nonempty α
inst✝ : FaithfulSMul M β
m₁✝ m₂✝ : M
h : ∀ (a : α × β), m₁✝ • a = m₂✝ • a
a : α
b : β
⊢ m₁✝ • b = m₂✝ • b
[PROOFSTEP]
injection h (a, b)
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Mul N
inst✝⁴ : Mul P
inst✝³ : SMul M N
inst✝² : SMul M P
inst✝¹ : SMulCommClass M N N
inst✝ : SMulCommClass M P P
c : M
x y : N × P
⊢ c • x • y = x • c • y
[PROOFSTEP]
simp [smul_def, mul_def, mul_smul_comm]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Mul N
inst✝⁴ : Mul P
inst✝³ : SMul M N
inst✝² : SMul M P
inst✝¹ : IsScalarTower M N N
inst✝ : IsScalarTower M P P
c : M
x y : N × P
⊢ (c • x) • y = c • x • y
[PROOFSTEP]
simp [smul_def, mul_def, smul_mul_assoc]


[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : { x // x ∈ H } →* A
R S T : ↑(leftTransversals ↑H)
inst✝ : FiniteIndex H
q : G ⧸ H
x✝ : q ∈ univ
⊢ {
        val :=
          (↑(↑(MemLeftTransversals.toEquiv (_ : ↑R ∈ leftTransversals ↑H)) q))⁻¹ *
            ↑(↑(MemLeftTransversals.toEquiv (_ : ↑S ∈ leftTransversals ↑H)) q),
        property :=
          (_ :
            (↑(↑(MemLeftTransversals.toEquiv (_ : ↑R ∈ leftTransversals ↑H)) q))⁻¹ *
                ↑(↑(MemLeftTransversals.toEquiv (_ : ↑S ∈ leftTransversals ↑H)) q) ∈
              H) } *
      {
        val :=
          (↑(↑(MemLeftTransversals.toEquiv (_ : ↑S ∈ leftTransversals ↑H)) q))⁻¹ *
            ↑(↑(MemLeftTransversals.toEquiv (_ : ↑T ∈ leftTransversals ↑H)) q),
        property :=
          (_ :
            (↑(↑(MemLeftTransversals.toEquiv (_ : ↑S ∈ leftTransversals ↑H)) q))⁻¹ *
                ↑(↑(MemLeftTransversals.toEquiv (_ : ↑T ∈ leftTransversals ↑H)) q) ∈
              H) } =
    {
      val :=
        (↑(↑(MemLeftTransversals.toEquiv (_ : ↑R ∈ leftTransversals ↑H)) q))⁻¹ *
          ↑(↑(MemLeftTransversals.toEquiv (_ : ↑T ∈ leftTransversals ↑H)) q),
      property :=
        (_ :
          (↑(↑(MemLeftTransversals.toEquiv (_ : ↑R ∈ leftTransversals ↑H)) q))⁻¹ *
              ↑(↑(MemLeftTransversals.toEquiv (_ : ↑T ∈ leftTransversals ↑H)) q) ∈
            H) }
[PROOFSTEP]
simp_rw [Subtype.ext_iff, coe_mul, mul_assoc, mul_inv_cancel_left]
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : { x // x ∈ H } →* A
R S T : ↑(leftTransversals ↑H)
inst✝ : FiniteIndex H
g : G
x✝² : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
x✝¹ : G ⧸ H
x✝ : x✝¹ ∈ univ
⊢ {
      val :=
        (↑(↑(MemLeftTransversals.toEquiv (_ : ↑(g • S) ∈ leftTransversals ↑H)) x✝¹))⁻¹ *
          ↑(↑(MemLeftTransversals.toEquiv (_ : ↑(g • T) ∈ leftTransversals ↑H)) x✝¹),
      property :=
        (_ :
          (↑(↑(MemLeftTransversals.toEquiv (_ : ↑(g • S) ∈ leftTransversals ↑H)) x✝¹))⁻¹ *
              ↑(↑(MemLeftTransversals.toEquiv (_ : ↑(g • T) ∈ leftTransversals ↑H)) x✝¹) ∈
            H) } =
    {
      val :=
        (↑(↑(MemLeftTransversals.toEquiv (_ : ↑S ∈ leftTransversals ↑H)) ((fun q x => g⁻¹ • q) x✝¹ x✝)))⁻¹ *
          ↑(↑(MemLeftTransversals.toEquiv (_ : ↑T ∈ leftTransversals ↑H)) ((fun q x => g⁻¹ • q) x✝¹ x✝)),
      property :=
        (_ :
          (↑(↑(MemLeftTransversals.toEquiv (_ : ↑S ∈ leftTransversals ↑H)) ((fun q x => g⁻¹ • q) x✝¹ x✝)))⁻¹ *
              ↑(↑(MemLeftTransversals.toEquiv (_ : ↑T ∈ leftTransversals ↑H)) ((fun q x => g⁻¹ • q) x✝¹ x✝)) ∈
            H) }
[PROOFSTEP]
simp_rw [smul_apply_eq_smul_apply_inv_smul, smul_eq_mul, mul_inv_rev, mul_assoc, inv_mul_cancel_left]
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : { x // x ∈ H } →* A
inst✝ : FiniteIndex H
T : ↑(leftTransversals ↑H) := default
⊢ (fun g => diff ϕ T (g • T)) 1 = 1
[PROOFSTEP]
simp only
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : { x // x ∈ H } →* A
inst✝ : FiniteIndex H
T : ↑(leftTransversals ↑H) := default
⊢ diff ϕ default (1 • default) = 1
[PROOFSTEP]
rw [one_smul, diff_self]
  -- porting note: added `simp only`
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : { x // x ∈ H } →* A
inst✝ : FiniteIndex H
T : ↑(leftTransversals ↑H) := default
g h : G
⊢ OneHom.toFun { toFun := fun g => diff ϕ T (g • T), map_one' := (_ : (fun g => diff ϕ T (g • T)) 1 = 1) } (g * h) =
    OneHom.toFun { toFun := fun g => diff ϕ T (g • T), map_one' := (_ : (fun g => diff ϕ T (g • T)) 1 = 1) } g *
      OneHom.toFun { toFun := fun g => diff ϕ T (g • T), map_one' := (_ : (fun g => diff ϕ T (g • T)) 1 = 1) } h
[PROOFSTEP]
simp only
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : { x // x ∈ H } →* A
inst✝ : FiniteIndex H
T : ↑(leftTransversals ↑H) := default
g h : G
⊢ diff ϕ default ((g * h) • default) = diff ϕ default (g • default) * diff ϕ default (h • default)
[PROOFSTEP]
rw [mul_smul, ← diff_mul_diff, smul_diff_smul]
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
inst✝ : FiniteIndex H
g : G
⊢ ↑(transfer ϕ) g = diff ϕ T (g • T)
[PROOFSTEP]
rw [transfer, ← diff_mul_diff, ← smul_diff_smul, mul_comm, diff_mul_diff]
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
inst✝ : FiniteIndex H
g : G
⊢ ↑(let T := default;
        {
          toOneHom :=
            { toFun := fun g => diff ϕ T (g • T), map_one' := (_ : (fun g => diff ϕ default (g • default)) 1 = 1) },
          map_mul' :=
            (_ :
              ∀ (g h : G),
                OneHom.toFun
                    { toFun := fun g => diff ϕ default (g • default),
                      map_one' := (_ : (fun g => diff ϕ default (g • default)) 1 = 1) }
                    (g * h) =
                  OneHom.toFun
                      { toFun := fun g => diff ϕ default (g • default),
                        map_one' := (_ : (fun g => diff ϕ default (g • default)) 1 = 1) }
                      g *
                    OneHom.toFun
                      { toFun := fun g => diff ϕ default (g • default),
                        map_one' := (_ : (fun g => diff ϕ default (g • default)) 1 = 1) }
                      h) })
      g =
    diff ϕ ?R (g • ?R)
[PROOFSTEP]
rfl
[GOAL]
G : Type u_1
inst✝³ : Group G
H : Subgroup G
A : Type u_2
inst✝² : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
inst✝¹ : FiniteIndex H
g : G
inst✝ : Fintype (Quotient (orbitRel { x // x ∈ zpowers g } (G ⧸ H)))
⊢ ↑(transfer ϕ) g =
    ∏ q : Quotient (orbitRel { x // x ∈ zpowers g } (G ⧸ H)),
      ↑ϕ
        {
          val :=
            (Quotient.out' (Quotient.out' q))⁻¹ *
                g ^ Function.minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q) *
              Quotient.out' (Quotient.out' q),
          property :=
            (_ :
              (Quotient.out' (Quotient.out' q))⁻¹ *
                    g ^ Function.minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q) *
                  Quotient.out' (Quotient.out' q) ∈
                H) }
[PROOFSTEP]
classical
letI := H.fintypeQuotientOfFiniteIndex
calc
  transfer ϕ g = ∏ q : G ⧸ H, _ := transfer_def ϕ (transferTransversal H g) g
  _ = _ := ((quotientEquivSigmaZMod H g).symm.prod_comp _).symm
  _ = _ := (Finset.prod_sigma _ _ _)
  _ = _ := by
    refine' Fintype.prod_congr _ _ (fun q => _)
    simp only [quotientEquivSigmaZMod_symm_apply, transferTransversal_apply', transferTransversal_apply'']
    rw [Fintype.prod_eq_single (0 : ZMod (Function.minimalPeriod ((· • ·) g) q.out')) _]
    · simp only [if_pos, ZMod.cast_zero, zpow_zero, one_mul, mul_assoc]
    · intro k hk
      simp only [if_neg hk, inv_mul_self]
      exact map_one ϕ
[GOAL]
G : Type u_1
inst✝³ : Group G
H : Subgroup G
A : Type u_2
inst✝² : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
inst✝¹ : FiniteIndex H
g : G
inst✝ : Fintype (Quotient (orbitRel { x // x ∈ zpowers g } (G ⧸ H)))
⊢ ↑(transfer ϕ) g =
    ∏ q : Quotient (orbitRel { x // x ∈ zpowers g } (G ⧸ H)),
      ↑ϕ
        {
          val :=
            (Quotient.out' (Quotient.out' q))⁻¹ *
                g ^ Function.minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q) *
              Quotient.out' (Quotient.out' q),
          property :=
            (_ :
              (Quotient.out' (Quotient.out' q))⁻¹ *
                    g ^ Function.minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q) *
                  Quotient.out' (Quotient.out' q) ∈
                H) }
[PROOFSTEP]
letI := H.fintypeQuotientOfFiniteIndex
[GOAL]
G : Type u_1
inst✝³ : Group G
H : Subgroup G
A : Type u_2
inst✝² : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
inst✝¹ : FiniteIndex H
g : G
inst✝ : Fintype (Quotient (orbitRel { x // x ∈ zpowers g } (G ⧸ H)))
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
⊢ ↑(transfer ϕ) g =
    ∏ q : Quotient (orbitRel { x // x ∈ zpowers g } (G ⧸ H)),
      ↑ϕ
        {
          val :=
            (Quotient.out' (Quotient.out' q))⁻¹ *
                g ^ Function.minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q) *
              Quotient.out' (Quotient.out' q),
          property :=
            (_ :
              (Quotient.out' (Quotient.out' q))⁻¹ *
                    g ^ Function.minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q) *
                  Quotient.out' (Quotient.out' q) ∈
                H) }
[PROOFSTEP]
calc
  transfer ϕ g = ∏ q : G ⧸ H, _ := transfer_def ϕ (transferTransversal H g) g
  _ = _ := ((quotientEquivSigmaZMod H g).symm.prod_comp _).symm
  _ = _ := (Finset.prod_sigma _ _ _)
  _ = _ := by
    refine' Fintype.prod_congr _ _ (fun q => _)
    simp only [quotientEquivSigmaZMod_symm_apply, transferTransversal_apply', transferTransversal_apply'']
    rw [Fintype.prod_eq_single (0 : ZMod (Function.minimalPeriod ((· • ·) g) q.out')) _]
    · simp only [if_pos, ZMod.cast_zero, zpow_zero, one_mul, mul_assoc]
    · intro k hk
      simp only [if_neg hk, inv_mul_self]
      exact map_one ϕ
[GOAL]
G : Type u_1
inst✝³ : Group G
H : Subgroup G
A : Type u_2
inst✝² : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
inst✝¹ : FiniteIndex H
g : G
inst✝ : Fintype (Quotient (orbitRel { x // x ∈ zpowers g } (G ⧸ H)))
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
⊢ ∏ a : orbitRel.Quotient { x // x ∈ zpowers g } (G ⧸ H),
      ∏ s in (fun x => Finset.univ) a,
        ↑ϕ
          {
            val :=
              (↑(↑(MemLeftTransversals.toEquiv (_ : ↑(transferTransversal H g) ∈ leftTransversals ↑H))
                      (↑(quotientEquivSigmaZMod H g).symm { fst := a, snd := s })))⁻¹ *
                ↑(↑(MemLeftTransversals.toEquiv (_ : ↑(g • transferTransversal H g) ∈ leftTransversals ↑H))
                    (↑(quotientEquivSigmaZMod H g).symm { fst := a, snd := s })),
            property :=
              (_ :
                (↑(↑(MemLeftTransversals.toEquiv (_ : ↑(transferTransversal H g) ∈ leftTransversals ↑H))
                          (↑(quotientEquivSigmaZMod H g).symm { fst := a, snd := s })))⁻¹ *
                    ↑(↑(MemLeftTransversals.toEquiv (_ : ↑(g • transferTransversal H g) ∈ leftTransversals ↑H))
                        (↑(quotientEquivSigmaZMod H g).symm { fst := a, snd := s })) ∈
                  H) } =
    ∏ q : Quotient (orbitRel { x // x ∈ zpowers g } (G ⧸ H)),
      ↑ϕ
        {
          val :=
            (Quotient.out' (Quotient.out' q))⁻¹ *
                g ^ Function.minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q) *
              Quotient.out' (Quotient.out' q),
          property :=
            (_ :
              (Quotient.out' (Quotient.out' q))⁻¹ *
                    g ^ Function.minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q) *
                  Quotient.out' (Quotient.out' q) ∈
                H) }
[PROOFSTEP]
refine' Fintype.prod_congr _ _ (fun q => _)
[GOAL]
G : Type u_1
inst✝³ : Group G
H : Subgroup G
A : Type u_2
inst✝² : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
inst✝¹ : FiniteIndex H
g : G
inst✝ : Fintype (Quotient (orbitRel { x // x ∈ zpowers g } (G ⧸ H)))
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
q : orbitRel.Quotient { x // x ∈ zpowers g } (G ⧸ H)
⊢ ∏ s in (fun x => Finset.univ) q,
      ↑ϕ
        {
          val :=
            (↑(↑(MemLeftTransversals.toEquiv (_ : ↑(transferTransversal H g) ∈ leftTransversals ↑H))
                    (↑(quotientEquivSigmaZMod H g).symm { fst := q, snd := s })))⁻¹ *
              ↑(↑(MemLeftTransversals.toEquiv (_ : ↑(g • transferTransversal H g) ∈ leftTransversals ↑H))
                  (↑(quotientEquivSigmaZMod H g).symm { fst := q, snd := s })),
          property :=
            (_ :
              (↑(↑(MemLeftTransversals.toEquiv (_ : ↑(transferTransversal H g) ∈ leftTransversals ↑H))
                        (↑(quotientEquivSigmaZMod H g).symm { fst := q, snd := s })))⁻¹ *
                  ↑(↑(MemLeftTransversals.toEquiv (_ : ↑(g • transferTransversal H g) ∈ leftTransversals ↑H))
                      (↑(quotientEquivSigmaZMod H g).symm { fst := q, snd := s })) ∈
                H) } =
    ↑ϕ
      {
        val :=
          (Quotient.out' (Quotient.out' q))⁻¹ *
              g ^ Function.minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q) *
            Quotient.out' (Quotient.out' q),
        property :=
          (_ :
            (Quotient.out' (Quotient.out' q))⁻¹ *
                  g ^ Function.minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q) *
                Quotient.out' (Quotient.out' q) ∈
              H) }
[PROOFSTEP]
simp only [quotientEquivSigmaZMod_symm_apply, transferTransversal_apply', transferTransversal_apply'']
[GOAL]
G : Type u_1
inst✝³ : Group G
H : Subgroup G
A : Type u_2
inst✝² : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
inst✝¹ : FiniteIndex H
g : G
inst✝ : Fintype (Quotient (orbitRel { x // x ∈ zpowers g } (G ⧸ H)))
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
q : orbitRel.Quotient { x // x ∈ zpowers g } (G ⧸ H)
⊢ ∏ x : ZMod (Function.minimalPeriod (fun x => g • x) (Quotient.out' q)),
      ↑ϕ
        {
          val :=
            (g ^ ↑x * Quotient.out' (Quotient.out' q))⁻¹ *
              if x = 0 then
                g ^ Function.minimalPeriod (fun x => g • x) (Quotient.out' q) * Quotient.out' (Quotient.out' q)
              else g ^ ↑x * Quotient.out' (Quotient.out' q),
          property :=
            (_ :
              (fun x => x ∈ H)
                ((g ^ ↑x * Quotient.out' (Quotient.out' q))⁻¹ *
                  if x = 0 then
                    g ^ Function.minimalPeriod (fun x => g • x) (Quotient.out' q) * Quotient.out' (Quotient.out' q)
                  else g ^ ↑x * Quotient.out' (Quotient.out' q))) } =
    ↑ϕ
      {
        val :=
          (Quotient.out' (Quotient.out' q))⁻¹ * g ^ Function.minimalPeriod (fun x => g • x) (Quotient.out' q) *
            Quotient.out' (Quotient.out' q),
        property :=
          (_ :
            (Quotient.out' (Quotient.out' q))⁻¹ *
                  g ^ Function.minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q) *
                Quotient.out' (Quotient.out' q) ∈
              H) }
[PROOFSTEP]
rw [Fintype.prod_eq_single (0 : ZMod (Function.minimalPeriod ((· • ·) g) q.out')) _]
[GOAL]
G : Type u_1
inst✝³ : Group G
H : Subgroup G
A : Type u_2
inst✝² : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
inst✝¹ : FiniteIndex H
g : G
inst✝ : Fintype (Quotient (orbitRel { x // x ∈ zpowers g } (G ⧸ H)))
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
q : orbitRel.Quotient { x // x ∈ zpowers g } (G ⧸ H)
⊢ ↑ϕ
      {
        val :=
          (g ^ ↑0 * Quotient.out' (Quotient.out' q))⁻¹ *
            if 0 = 0 then
              g ^ Function.minimalPeriod (fun x => g • x) (Quotient.out' q) * Quotient.out' (Quotient.out' q)
            else g ^ ↑0 * Quotient.out' (Quotient.out' q),
        property :=
          (_ :
            (fun x => x ∈ H)
              ((g ^ ↑0 * Quotient.out' (Quotient.out' q))⁻¹ *
                if 0 = 0 then
                  g ^ Function.minimalPeriod (fun x => g • x) (Quotient.out' q) * Quotient.out' (Quotient.out' q)
                else g ^ ↑0 * Quotient.out' (Quotient.out' q))) } =
    ↑ϕ
      {
        val :=
          (Quotient.out' (Quotient.out' q))⁻¹ * g ^ Function.minimalPeriod (fun x => g • x) (Quotient.out' q) *
            Quotient.out' (Quotient.out' q),
        property :=
          (_ :
            (Quotient.out' (Quotient.out' q))⁻¹ *
                  g ^ Function.minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q) *
                Quotient.out' (Quotient.out' q) ∈
              H) }
[PROOFSTEP]
simp only [if_pos, ZMod.cast_zero, zpow_zero, one_mul, mul_assoc]
[GOAL]
G : Type u_1
inst✝³ : Group G
H : Subgroup G
A : Type u_2
inst✝² : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
inst✝¹ : FiniteIndex H
g : G
inst✝ : Fintype (Quotient (orbitRel { x // x ∈ zpowers g } (G ⧸ H)))
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
q : orbitRel.Quotient { x // x ∈ zpowers g } (G ⧸ H)
⊢ ∀ (x : ZMod (Function.minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q))),
    x ≠ 0 →
      ↑ϕ
          {
            val :=
              (g ^ ↑x * Quotient.out' (Quotient.out' q))⁻¹ *
                if x = 0 then
                  g ^ Function.minimalPeriod (fun x => g • x) (Quotient.out' q) * Quotient.out' (Quotient.out' q)
                else g ^ ↑x * Quotient.out' (Quotient.out' q),
            property :=
              (_ :
                (fun x => x ∈ H)
                  ((g ^ ↑x * Quotient.out' (Quotient.out' q))⁻¹ *
                    if x = 0 then
                      g ^ Function.minimalPeriod (fun x => g • x) (Quotient.out' q) * Quotient.out' (Quotient.out' q)
                    else g ^ ↑x * Quotient.out' (Quotient.out' q))) } =
        1
[PROOFSTEP]
intro k hk
[GOAL]
G : Type u_1
inst✝³ : Group G
H : Subgroup G
A : Type u_2
inst✝² : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
inst✝¹ : FiniteIndex H
g : G
inst✝ : Fintype (Quotient (orbitRel { x // x ∈ zpowers g } (G ⧸ H)))
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
q : orbitRel.Quotient { x // x ∈ zpowers g } (G ⧸ H)
k : ZMod (Function.minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q))
hk : k ≠ 0
⊢ ↑ϕ
      {
        val :=
          (g ^ ↑k * Quotient.out' (Quotient.out' q))⁻¹ *
            if k = 0 then
              g ^ Function.minimalPeriod (fun x => g • x) (Quotient.out' q) * Quotient.out' (Quotient.out' q)
            else g ^ ↑k * Quotient.out' (Quotient.out' q),
        property :=
          (_ :
            (fun x => x ∈ H)
              ((g ^ ↑k * Quotient.out' (Quotient.out' q))⁻¹ *
                if k = 0 then
                  g ^ Function.minimalPeriod (fun x => g • x) (Quotient.out' q) * Quotient.out' (Quotient.out' q)
                else g ^ ↑k * Quotient.out' (Quotient.out' q))) } =
    1
[PROOFSTEP]
simp only [if_neg hk, inv_mul_self]
[GOAL]
G : Type u_1
inst✝³ : Group G
H : Subgroup G
A : Type u_2
inst✝² : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
inst✝¹ : FiniteIndex H
g : G
inst✝ : Fintype (Quotient (orbitRel { x // x ∈ zpowers g } (G ⧸ H)))
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
q : orbitRel.Quotient { x // x ∈ zpowers g } (G ⧸ H)
k : ZMod (Function.minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q))
hk : k ≠ 0
⊢ ↑ϕ { val := 1, property := (_ : (fun x => x ∈ H) 1) } = 1
[PROOFSTEP]
exact map_one ϕ
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
A : Type u_2
inst✝ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
g : G
key : ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g₀⁻¹ * g ^ k * g₀ = g ^ k
⊢ g ^ index H ∈ H
[PROOFSTEP]
by_cases hH : H.index = 0
[GOAL]
case pos
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
A : Type u_2
inst✝ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
g : G
key : ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g₀⁻¹ * g ^ k * g₀ = g ^ k
hH : index H = 0
⊢ g ^ index H ∈ H
[PROOFSTEP]
rw [hH, pow_zero]
[GOAL]
case pos
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
A : Type u_2
inst✝ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
g : G
key : ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g₀⁻¹ * g ^ k * g₀ = g ^ k
hH : index H = 0
⊢ 1 ∈ H
[PROOFSTEP]
exact H.one_mem
[GOAL]
case neg
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
A : Type u_2
inst✝ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
g : G
key : ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g₀⁻¹ * g ^ k * g₀ = g ^ k
hH : ¬index H = 0
⊢ g ^ index H ∈ H
[PROOFSTEP]
letI := fintypeOfIndexNeZero hH
[GOAL]
case neg
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
A : Type u_2
inst✝ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
g : G
key : ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g₀⁻¹ * g ^ k * g₀ = g ^ k
hH : ¬index H = 0
this : Fintype (G ⧸ H) := fintypeOfIndexNeZero hH
⊢ g ^ index H ∈ H
[PROOFSTEP]
classical
replace key : ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g ^ k ∈ H := fun k g₀ hk =>
  (_root_.congr_arg (· ∈ H) (key k g₀ hk)).mp hk
replace key : ∀ q : G ⧸ H, g ^ Function.minimalPeriod ((· • ·) g) q ∈ H := fun q =>
  key (Function.minimalPeriod ((· • ·) g) q) q.out' (QuotientGroup.out'_conj_pow_minimalPeriod_mem H g q)
let f : Quotient (orbitRel (zpowers g) (G ⧸ H)) → zpowers g := fun q =>
  (⟨g, mem_zpowers g⟩ : zpowers g) ^ Function.minimalPeriod ((· • ·) g) q.out'
have hf : ∀ q, f q ∈ H.subgroupOf (zpowers g) := fun q => key q.out'
replace key := Subgroup.prod_mem (H.subgroupOf (zpowers g)) fun q (_ : q ∈ Finset.univ) => hf q
simpa only [minimalPeriod_eq_card, Finset.prod_pow_eq_pow_sum, Fintype.card_sigma,
  Fintype.card_congr (selfEquivSigmaOrbits (zpowers g) (G ⧸ H)), index_eq_card] using key
[GOAL]
case neg
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
A : Type u_2
inst✝ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
g : G
key : ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g₀⁻¹ * g ^ k * g₀ = g ^ k
hH : ¬index H = 0
this : Fintype (G ⧸ H) := fintypeOfIndexNeZero hH
⊢ g ^ index H ∈ H
[PROOFSTEP]
replace key : ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g ^ k ∈ H := fun k g₀ hk =>
  (_root_.congr_arg (· ∈ H) (key k g₀ hk)).mp hk
[GOAL]
case neg
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
A : Type u_2
inst✝ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
g : G
hH : ¬index H = 0
this : Fintype (G ⧸ H) := fintypeOfIndexNeZero hH
key : ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g ^ k ∈ H
⊢ g ^ index H ∈ H
[PROOFSTEP]
replace key : ∀ q : G ⧸ H, g ^ Function.minimalPeriod ((· • ·) g) q ∈ H := fun q =>
  key (Function.minimalPeriod ((· • ·) g) q) q.out' (QuotientGroup.out'_conj_pow_minimalPeriod_mem H g q)
[GOAL]
case neg
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
A : Type u_2
inst✝ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
g : G
hH : ¬index H = 0
this : Fintype (G ⧸ H) := fintypeOfIndexNeZero hH
key : ∀ (q : G ⧸ H), g ^ Function.minimalPeriod ((fun x x_1 => x • x_1) g) q ∈ H
⊢ g ^ index H ∈ H
[PROOFSTEP]
let f : Quotient (orbitRel (zpowers g) (G ⧸ H)) → zpowers g := fun q =>
  (⟨g, mem_zpowers g⟩ : zpowers g) ^ Function.minimalPeriod ((· • ·) g) q.out'
[GOAL]
case neg
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
A : Type u_2
inst✝ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
g : G
hH : ¬index H = 0
this : Fintype (G ⧸ H) := fintypeOfIndexNeZero hH
key : ∀ (q : G ⧸ H), g ^ Function.minimalPeriod ((fun x x_1 => x • x_1) g) q ∈ H
f : Quotient (orbitRel { x // x ∈ zpowers g } (G ⧸ H)) → { x // x ∈ zpowers g } :=
  fun q =>
    { val := g, property := (_ : g ∈ zpowers g) } ^ Function.minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q)
⊢ g ^ index H ∈ H
[PROOFSTEP]
have hf : ∀ q, f q ∈ H.subgroupOf (zpowers g) := fun q => key q.out'
[GOAL]
case neg
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
A : Type u_2
inst✝ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
g : G
hH : ¬index H = 0
this : Fintype (G ⧸ H) := fintypeOfIndexNeZero hH
key : ∀ (q : G ⧸ H), g ^ Function.minimalPeriod ((fun x x_1 => x • x_1) g) q ∈ H
f : Quotient (orbitRel { x // x ∈ zpowers g } (G ⧸ H)) → { x // x ∈ zpowers g } :=
  fun q =>
    { val := g, property := (_ : g ∈ zpowers g) } ^ Function.minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q)
hf : ∀ (q : Quotient (orbitRel { x // x ∈ zpowers g } (G ⧸ H))), f q ∈ subgroupOf H (zpowers g)
⊢ g ^ index H ∈ H
[PROOFSTEP]
replace key := Subgroup.prod_mem (H.subgroupOf (zpowers g)) fun q (_ : q ∈ Finset.univ) => hf q
[GOAL]
case neg
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
A : Type u_2
inst✝ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
g : G
hH : ¬index H = 0
this : Fintype (G ⧸ H) := fintypeOfIndexNeZero hH
f : Quotient (orbitRel { x // x ∈ zpowers g } (G ⧸ H)) → { x // x ∈ zpowers g } :=
  fun q =>
    { val := g, property := (_ : g ∈ zpowers g) } ^ Function.minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q)
hf : ∀ (q : Quotient (orbitRel { x // x ∈ zpowers g } (G ⧸ H))), f q ∈ subgroupOf H (zpowers g)
key : ∏ c : Quotient (orbitRel { x // x ∈ zpowers g } (G ⧸ H)), f c ∈ subgroupOf H (zpowers g)
⊢ g ^ index H ∈ H
[PROOFSTEP]
simpa only [minimalPeriod_eq_card, Finset.prod_pow_eq_pow_sum, Fintype.card_sigma,
  Fintype.card_congr (selfEquivSigmaOrbits (zpowers g) (G ⧸ H)), index_eq_card] using key
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
inst✝ : FiniteIndex H
g : G
key : ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g₀⁻¹ * g ^ k * g₀ = g ^ k
⊢ ↑(transfer ϕ) g = ↑ϕ { val := g ^ index H, property := (_ : g ^ index H ∈ H) }
[PROOFSTEP]
classical
letI := H.fintypeQuotientOfFiniteIndex
change ∀ (k g₀) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H), ↑(⟨g₀⁻¹ * g ^ k * g₀, hk⟩ : H) = g ^ k at key
rw [transfer_eq_prod_quotient_orbitRel_zpowers_quot, ← Finset.prod_to_list]
refine'
  (List.prod_map_hom _ _ _).trans
    _
      -- porting note: this used to be in the `rw`
refine' congrArg ϕ (Subtype.coe_injective _)
simp only
  -- porting note: added `simp only`
rw [H.coe_mk, ← (zpowers g).coe_mk g (mem_zpowers g), ← (zpowers g).coe_pow, index_eq_card,
  Fintype.card_congr (selfEquivSigmaOrbits (zpowers g) (G ⧸ H)), Fintype.card_sigma, ← Finset.prod_pow_eq_pow_sum, ←
  Finset.prod_to_list]
simp only [Subgroup.val_list_prod, List.map_map, ← minimalPeriod_eq_card]
congr
funext
apply key
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
inst✝ : FiniteIndex H
g : G
key : ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g₀⁻¹ * g ^ k * g₀ = g ^ k
⊢ ↑(transfer ϕ) g = ↑ϕ { val := g ^ index H, property := (_ : g ^ index H ∈ H) }
[PROOFSTEP]
letI := H.fintypeQuotientOfFiniteIndex
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
inst✝ : FiniteIndex H
g : G
key : ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g₀⁻¹ * g ^ k * g₀ = g ^ k
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
⊢ ↑(transfer ϕ) g = ↑ϕ { val := g ^ index H, property := (_ : g ^ index H ∈ H) }
[PROOFSTEP]
change ∀ (k g₀) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H), ↑(⟨g₀⁻¹ * g ^ k * g₀, hk⟩ : H) = g ^ k at key
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
inst✝ : FiniteIndex H
g : G
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
key : ∀ (k : ℕ) (g₀ : G) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H), ↑{ val := g₀⁻¹ * g ^ k * g₀, property := hk } = g ^ k
⊢ ↑(transfer ϕ) g = ↑ϕ { val := g ^ index H, property := (_ : g ^ index H ∈ H) }
[PROOFSTEP]
rw [transfer_eq_prod_quotient_orbitRel_zpowers_quot, ← Finset.prod_to_list]
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
inst✝ : FiniteIndex H
g : G
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
key : ∀ (k : ℕ) (g₀ : G) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H), ↑{ val := g₀⁻¹ * g ^ k * g₀, property := hk } = g ^ k
⊢ List.prod
      (List.map
        (fun q =>
          ↑ϕ
            {
              val :=
                (Quotient.out' (Quotient.out' q))⁻¹ *
                    g ^ Function.minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q) *
                  Quotient.out' (Quotient.out' q),
              property :=
                (_ :
                  (Quotient.out' (Quotient.out' q))⁻¹ *
                        g ^ Function.minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q) *
                      Quotient.out' (Quotient.out' q) ∈
                    H) })
        (Finset.toList Finset.univ)) =
    ↑ϕ { val := g ^ index H, property := (_ : g ^ index H ∈ H) }
[PROOFSTEP]
refine'
  (List.prod_map_hom _ _ _).trans
    _
      -- porting note: this used to be in the `rw`
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
inst✝ : FiniteIndex H
g : G
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
key : ∀ (k : ℕ) (g₀ : G) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H), ↑{ val := g₀⁻¹ * g ^ k * g₀, property := hk } = g ^ k
⊢ ↑ϕ
      (List.prod
        (List.map
          (fun q =>
            {
              val :=
                (Quotient.out' (Quotient.out' q))⁻¹ *
                    g ^ Function.minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q) *
                  Quotient.out' (Quotient.out' q),
              property :=
                (_ :
                  (Quotient.out' (Quotient.out' q))⁻¹ *
                        g ^ Function.minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q) *
                      Quotient.out' (Quotient.out' q) ∈
                    H) })
          (Finset.toList Finset.univ))) =
    ↑ϕ { val := g ^ index H, property := (_ : g ^ index H ∈ H) }
[PROOFSTEP]
refine' congrArg ϕ (Subtype.coe_injective _)
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
inst✝ : FiniteIndex H
g : G
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
key : ∀ (k : ℕ) (g₀ : G) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H), ↑{ val := g₀⁻¹ * g ^ k * g₀, property := hk } = g ^ k
⊢ (fun a => ↑a)
      (List.prod
        (List.map
          (fun q =>
            {
              val :=
                (Quotient.out' (Quotient.out' q))⁻¹ *
                    g ^ Function.minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q) *
                  Quotient.out' (Quotient.out' q),
              property :=
                (_ :
                  (Quotient.out' (Quotient.out' q))⁻¹ *
                        g ^ Function.minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q) *
                      Quotient.out' (Quotient.out' q) ∈
                    H) })
          (Finset.toList Finset.univ))) =
    (fun a => ↑a) { val := g ^ index H, property := (_ : g ^ index H ∈ H) }
[PROOFSTEP]
simp only
  -- porting note: added `simp only`
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
inst✝ : FiniteIndex H
g : G
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
key : ∀ (k : ℕ) (g₀ : G) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H), ↑{ val := g₀⁻¹ * g ^ k * g₀, property := hk } = g ^ k
⊢ ↑(List.prod
        (List.map
          (fun q =>
            {
              val :=
                (Quotient.out' (Quotient.out' q))⁻¹ * g ^ Function.minimalPeriod (fun x => g • x) (Quotient.out' q) *
                  Quotient.out' (Quotient.out' q),
              property :=
                (_ :
                  (Quotient.out' (Quotient.out' q))⁻¹ *
                        g ^ Function.minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q) *
                      Quotient.out' (Quotient.out' q) ∈
                    H) })
          (Finset.toList Finset.univ))) =
    g ^ index H
[PROOFSTEP]
rw [H.coe_mk, ← (zpowers g).coe_mk g (mem_zpowers g), ← (zpowers g).coe_pow, index_eq_card,
  Fintype.card_congr (selfEquivSigmaOrbits (zpowers g) (G ⧸ H)), Fintype.card_sigma, ← Finset.prod_pow_eq_pow_sum, ←
  Finset.prod_to_list]
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
inst✝ : FiniteIndex H
g : G
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
key : ∀ (k : ℕ) (g₀ : G) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H), ↑{ val := g₀⁻¹ * g ^ k * g₀, property := hk } = g ^ k
⊢ ↑(List.prod
        (List.map
          (fun q =>
            {
              val :=
                (Quotient.out' (Quotient.out' q))⁻¹ *
                    ↑{ val := g, property := (_ : g ∈ zpowers g) } ^
                      Function.minimalPeriod (fun x => ↑{ val := g, property := (_ : g ∈ zpowers g) } • x)
                        (Quotient.out' q) *
                  Quotient.out' (Quotient.out' q),
              property :=
                (_ :
                  (Quotient.out' (Quotient.out' q))⁻¹ *
                        ↑{ val := g, property := (_ : g ∈ zpowers g) } ^
                          Function.minimalPeriod ((fun x x_1 => x • x_1) ↑{ val := g, property := (_ : g ∈ zpowers g) })
                            (Quotient.out' q) *
                      Quotient.out' (Quotient.out' q) ∈
                    H) })
          (Finset.toList Finset.univ))) =
    ↑(List.prod
        (List.map
          (fun i =>
            { val := g, property := (_ : g ∈ zpowers g) } ^
              Fintype.card ↑(orbit { x // x ∈ zpowers g } (Quotient.out' i)))
          (Finset.toList Finset.univ)))
[PROOFSTEP]
simp only [Subgroup.val_list_prod, List.map_map, ← minimalPeriod_eq_card]
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
inst✝ : FiniteIndex H
g : G
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
key : ∀ (k : ℕ) (g₀ : G) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H), ↑{ val := g₀⁻¹ * g ^ k * g₀, property := hk } = g ^ k
⊢ List.prod
      (List.map
        (Subtype.val ∘ fun q =>
          {
            val :=
              (Quotient.out' (Quotient.out' q))⁻¹ * g ^ Function.minimalPeriod (fun x => g • x) (Quotient.out' q) *
                Quotient.out' (Quotient.out' q),
            property :=
              (_ :
                (Quotient.out' (Quotient.out' q))⁻¹ *
                      ↑{ val := g, property := (_ : g ∈ zpowers g) } ^
                        Function.minimalPeriod ((fun x x_1 => x • x_1) ↑{ val := g, property := (_ : g ∈ zpowers g) })
                          (Quotient.out' q) *
                    Quotient.out' (Quotient.out' q) ∈
                  H) })
        (Finset.toList Finset.univ)) =
    List.prod
      (List.map
        (Subtype.val ∘ fun i =>
          { val := g, property := (_ : g ∈ zpowers g) } ^ Function.minimalPeriod (fun x => g • x) (Quotient.out' i))
        (Finset.toList Finset.univ))
[PROOFSTEP]
congr
[GOAL]
case e_a.e_f
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
inst✝ : FiniteIndex H
g : G
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
key : ∀ (k : ℕ) (g₀ : G) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H), ↑{ val := g₀⁻¹ * g ^ k * g₀, property := hk } = g ^ k
⊢ (Subtype.val ∘ fun q =>
      {
        val :=
          (Quotient.out' (Quotient.out' q))⁻¹ * g ^ Function.minimalPeriod (fun x => g • x) (Quotient.out' q) *
            Quotient.out' (Quotient.out' q),
        property :=
          (_ :
            (Quotient.out' (Quotient.out' q))⁻¹ *
                  ↑{ val := g, property := (_ : g ∈ zpowers g) } ^
                    Function.minimalPeriod ((fun x x_1 => x • x_1) ↑{ val := g, property := (_ : g ∈ zpowers g) })
                      (Quotient.out' q) *
                Quotient.out' (Quotient.out' q) ∈
              H) }) =
    Subtype.val ∘ fun i =>
      { val := g, property := (_ : g ∈ zpowers g) } ^ Function.minimalPeriod (fun x => g • x) (Quotient.out' i)
[PROOFSTEP]
funext
[GOAL]
case e_a.e_f.h
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
inst✝ : FiniteIndex H
g : G
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
key : ∀ (k : ℕ) (g₀ : G) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H), ↑{ val := g₀⁻¹ * g ^ k * g₀, property := hk } = g ^ k
x✝ : Quotient (orbitRel { x // x ∈ zpowers g } (G ⧸ H))
⊢ (Subtype.val ∘ fun q =>
        {
          val :=
            (Quotient.out' (Quotient.out' q))⁻¹ * g ^ Function.minimalPeriod (fun x => g • x) (Quotient.out' q) *
              Quotient.out' (Quotient.out' q),
          property :=
            (_ :
              (Quotient.out' (Quotient.out' q))⁻¹ *
                    ↑{ val := g, property := (_ : g ∈ zpowers g) } ^
                      Function.minimalPeriod ((fun x x_1 => x • x_1) ↑{ val := g, property := (_ : g ∈ zpowers g) })
                        (Quotient.out' q) *
                  Quotient.out' (Quotient.out' q) ∈
                H) })
      x✝ =
    (Subtype.val ∘ fun i =>
        { val := g, property := (_ : g ∈ zpowers g) } ^ Function.minimalPeriod (fun x => g • x) (Quotient.out' i))
      x✝
[PROOFSTEP]
apply key
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
inst✝ : FiniteIndex (center G)
g : G
k : ℕ
x✝ : G
hk : x✝⁻¹ * g ^ k * x✝ ∈ center G
⊢ x✝⁻¹ * g ^ k * x✝ = g ^ k
[PROOFSTEP]
rw [← mul_right_inj, hk, mul_inv_cancel_right]
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
inst✝ : FiniteIndex (center G)
a b : G
⊢ OneHom.toFun
      { toFun := fun g => { val := g ^ index (center G), property := (_ : g ^ index (center G) ∈ center G) },
        map_one' :=
          (_ : (fun g => { val := g ^ index (center G), property := (_ : g ^ index (center G) ∈ center G) }) 1 = 1) }
      (a * b) =
    OneHom.toFun
        { toFun := fun g => { val := g ^ index (center G), property := (_ : g ^ index (center G) ∈ center G) },
          map_one' :=
            (_ : (fun g => { val := g ^ index (center G), property := (_ : g ^ index (center G) ∈ center G) }) 1 = 1) }
        a *
      OneHom.toFun
        { toFun := fun g => { val := g ^ index (center G), property := (_ : g ^ index (center G) ∈ center G) },
          map_one' :=
            (_ : (fun g => { val := g ^ index (center G), property := (_ : g ^ index (center G) ∈ center G) }) 1 = 1) }
        b
[PROOFSTEP]
simp_rw [← show ∀ _, (_ : center G) = _ from transfer_center_eq_pow, map_mul]
[GOAL]
G : Type u_1
inst✝³ : Group G
H : Subgroup G
A : Type u_2
inst✝² : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
p : ℕ
P : Sylow p G
hP : normalizer ↑P ≤ centralizer ↑P
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
g : G
hg : g ∈ P
k : ℕ
g₀ : G
h : g₀⁻¹ * g ^ k * g₀ ∈ P
⊢ g₀⁻¹ * g ^ k * g₀ = g ^ k
[PROOFSTEP]
haveI : (P : Subgroup G).IsCommutative := ⟨⟨fun a b => Subtype.ext (hP (le_normalizer b.2) a a.2)⟩⟩
[GOAL]
G : Type u_1
inst✝³ : Group G
H : Subgroup G
A : Type u_2
inst✝² : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
p : ℕ
P : Sylow p G
hP : normalizer ↑P ≤ centralizer ↑P
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
g : G
hg : g ∈ P
k : ℕ
g₀ : G
h : g₀⁻¹ * g ^ k * g₀ ∈ P
this : Subgroup.IsCommutative ↑P
⊢ g₀⁻¹ * g ^ k * g₀ = g ^ k
[PROOFSTEP]
replace hg := (P : Subgroup G).pow_mem hg k
[GOAL]
G : Type u_1
inst✝³ : Group G
H : Subgroup G
A : Type u_2
inst✝² : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
p : ℕ
P : Sylow p G
hP : normalizer ↑P ≤ centralizer ↑P
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
g : G
k : ℕ
g₀ : G
h : g₀⁻¹ * g ^ k * g₀ ∈ P
this : Subgroup.IsCommutative ↑P
hg : g ^ k ∈ ↑P
⊢ g₀⁻¹ * g ^ k * g₀ = g ^ k
[PROOFSTEP]
obtain ⟨n, hn, h⟩ := P.conj_eq_normalizer_conj_of_mem (g ^ k) g₀ hg h
[GOAL]
case intro.intro
G : Type u_1
inst✝³ : Group G
H : Subgroup G
A : Type u_2
inst✝² : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
p : ℕ
P : Sylow p G
hP : normalizer ↑P ≤ centralizer ↑P
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
g : G
k : ℕ
g₀ : G
h✝ : g₀⁻¹ * g ^ k * g₀ ∈ P
this : Subgroup.IsCommutative ↑P
hg : g ^ k ∈ ↑P
n : G
hn : n ∈ normalizer ↑P
h : g₀⁻¹ * g ^ k * g₀ = n⁻¹ * g ^ k * n
⊢ g₀⁻¹ * g ^ k * g₀ = g ^ k
[PROOFSTEP]
exact h.trans (Commute.inv_mul_cancel (hP hn (g ^ k) hg).symm)
[GOAL]
G : Type u_1
inst✝⁴ : Group G
H : Subgroup G
A : Type u_2
inst✝³ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
p : ℕ
P : Sylow p G
hP : normalizer ↑P ≤ centralizer ↑P
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite (Sylow p G)
inst✝ : FiniteIndex ↑P
⊢ IsComplement' (ker (transferSylow P hP)) ↑P
[PROOFSTEP]
have hf : Function.Bijective ((transferSylow P hP).restrict (P : Subgroup G)) :=
  (transferSylow_restrict_eq_pow P hP).symm ▸
    (P.2.powEquiv' (not_dvd_index_sylow P (mt index_eq_zero_of_relindex_eq_zero index_ne_zero_of_finite))).bijective
[GOAL]
G : Type u_1
inst✝⁴ : Group G
H : Subgroup G
A : Type u_2
inst✝³ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
p : ℕ
P : Sylow p G
hP : normalizer ↑P ≤ centralizer ↑P
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite (Sylow p G)
inst✝ : FiniteIndex ↑P
hf : Function.Bijective ↑(restrict (transferSylow P hP) ↑P)
⊢ IsComplement' (ker (transferSylow P hP)) ↑P
[PROOFSTEP]
rw [Function.Bijective, ← range_top_iff_surjective, restrict_range] at hf
[GOAL]
G : Type u_1
inst✝⁴ : Group G
H : Subgroup G
A : Type u_2
inst✝³ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
p : ℕ
P : Sylow p G
hP : normalizer ↑P ≤ centralizer ↑P
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite (Sylow p G)
inst✝ : FiniteIndex ↑P
hf : Function.Injective ↑(restrict (transferSylow P hP) ↑P) ∧ map (transferSylow P hP) ↑P = ⊤
⊢ IsComplement' (ker (transferSylow P hP)) ↑P
[PROOFSTEP]
have := range_top_iff_surjective.mp (top_le_iff.mp (hf.2.ge.trans (map_le_range (transferSylow P hP) P)))
[GOAL]
G : Type u_1
inst✝⁴ : Group G
H : Subgroup G
A : Type u_2
inst✝³ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
p : ℕ
P : Sylow p G
hP : normalizer ↑P ≤ centralizer ↑P
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite (Sylow p G)
inst✝ : FiniteIndex ↑P
hf : Function.Injective ↑(restrict (transferSylow P hP) ↑P) ∧ map (transferSylow P hP) ↑P = ⊤
this : Function.Surjective ↑(transferSylow P hP)
⊢ IsComplement' (ker (transferSylow P hP)) ↑P
[PROOFSTEP]
rw [← (comap_injective this).eq_iff, comap_top, comap_map_eq, sup_comm, SetLike.ext'_iff, normal_mul, ← ker_eq_bot_iff,
  ← (map_injective (P : Subgroup G).subtype_injective).eq_iff, ker_restrict, subgroupOf_map_subtype, Subgroup.map_bot,
  coe_top] at hf
[GOAL]
G : Type u_1
inst✝⁴ : Group G
H : Subgroup G
A : Type u_2
inst✝³ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
p : ℕ
P : Sylow p G
hP : normalizer ↑P ≤ centralizer ↑P
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite (Sylow p G)
inst✝ : FiniteIndex ↑P
hf✝ : Function.Injective ↑(restrict (transferSylow P hP) ↑P) ∧ ker (transferSylow P hP) ⊔ ↑P = ⊤
hf : ker (transferSylow P hP) ⊓ ↑P = ⊥ ∧ ↑(ker (transferSylow P hP)) * ↑↑P = Set.univ
this : Function.Surjective ↑(transferSylow P hP)
⊢ IsComplement' (ker (transferSylow P hP)) ↑P
[PROOFSTEP]
exact isComplement'_of_disjoint_and_mul_eq_univ (disjoint_iff.2 hf.1) hf.2