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
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
h : IsComplement' H K
⊢ IsComplement' K H
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 _)
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
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
let ψ : G ≃ G := Equiv.mk (fun g : G => g⁻¹) (fun g : G => g⁻¹) inv_inv inv_inv
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) ∘ ↑ϕ
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
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]
no goals
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) ∘ ↑ϕ
exact funext fun x => mul_inv_rev _ _
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) ∘ ↑ϕ)
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
rw [isComplement'_def, IsComplement, ← Equiv.bijective_comp ϕ]
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)
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) ∘ ↑ϕ)
apply (congr_arg Function.Bijective hf).mp
no goals
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)
rwa [ψ.comp_bijective]