-- Mathlib/GroupTheory/Sylow.lean
theorem mem_fixedPoints_mul_left_cosets_iff_mem_normalizer {H : Subgroup G} [Finite (H : Set G)]
    {x : G} : (x : G ⧸ H) ∈ MulAction.fixedPoints H (G ⧸ H) ↔ x ∈ normalizer H :=
  ⟨fun hx =>
    have ha : ∀ {y : G ⧸ H}, y ∈ orbit H (x : G ⧸ H) → y = x := mem_fixedPoints'.1 hx _
    (inv_mem_iff (G := G)).1
      (mem_normalizer_fintype fun n (hn : n ∈ H) =>
        have : (n⁻¹ * x)⁻¹ * x ∈ H := QuotientGroup.eq.1 (ha ⟨⟨n⁻¹, inv_mem hn⟩, rfl⟩)
        show _ ∈ H by
          rw [mul_inv_rev, inv_inv] at this
          convert this
          rw [inv_inv]),
    fun hx : ∀ n : G, n ∈ H ↔ x * n * x⁻¹ ∈ H =>
    mem_fixedPoints'.2 fun y =>
      Quotient.inductionOn' y fun y hy =>
        QuotientGroup.eq.2
          (let ⟨⟨b, hb₁⟩, hb₂⟩ := hy
          have hb₂ : (b * x)⁻¹ * y ∈ H := QuotientGroup.eq.1 hb₂
          (inv_mem_iff (G := G)).1 <|
            (hx _).2 <|
              (mul_mem_cancel_left (inv_mem hb₁)).1 <| by
                rw [hx] at hb₂; simpa [mul_inv_rev, mul_assoc] using hb₂)⟩

Proof state:
G : Type u
inst✝¹ : Group G
H : Subgroup G
inst✝ : Finite ↑↑H
x : G
hx : ↑x ∈ MulAction.fixedPoints (↥H) (G ⧸ H)
ha : ∀ {y : G ⧸ H}, y ∈ orbit ↥H ↑x → y = ↑x
n : G
hn : n ∈ H
this : (n⁻¹ * x)⁻¹ * x ∈ H
⊢ x⁻¹ * n * x⁻¹⁻¹ ∈ H

Tactic:
rw [mul_inv_rev, inv_inv] at this

Result:
G : Type u
inst✝¹ : Group G
H : Subgroup G
inst✝ : Finite ↑↑H
x : G
hx : ↑x ∈ MulAction.fixedPoints (↥H) (G ⧸ H)
ha : ∀ {y : G ⧸ H}, y ∈ orbit ↥H ↑x → y = ↑x
n : G
hn : n ∈ H
this : x⁻¹ * n * x ∈ H
⊢ x⁻¹ * n * x⁻¹⁻¹ ∈ H

Proof state:
G : Type u
inst✝¹ : Group G
H : Subgroup G
inst✝ : Finite ↑↑H
x : G
hx : ↑x ∈ MulAction.fixedPoints (↥H) (G ⧸ H)
ha : ∀ {y : G ⧸ H}, y ∈ orbit ↥H ↑x → y = ↑x
n : G
hn : n ∈ H
this : x⁻¹ * n * x ∈ H
⊢ x⁻¹ * n * x⁻¹⁻¹ ∈ H

Tactic:
convert this

Result:
case h.e'_5.h.e'_6
G : Type u
inst✝¹ : Group G
H : Subgroup G
inst✝ : Finite ↑↑H
x : G
hx : ↑x ∈ MulAction.fixedPoints (↥H) (G ⧸ H)
ha : ∀ {y : G ⧸ H}, y ∈ orbit ↥H ↑x → y = ↑x
n : G
hn : n ∈ H
this : x⁻¹ * n * x ∈ H
⊢ x⁻¹⁻¹ = x

Proof state:
case h.e'_5.h.e'_6
G : Type u
inst✝¹ : Group G
H : Subgroup G
inst✝ : Finite ↑↑H
x : G
hx : ↑x ∈ MulAction.fixedPoints (↥H) (G ⧸ H)
ha : ∀ {y : G ⧸ H}, y ∈ orbit ↥H ↑x → y = ↑x
n : G
hn : n ∈ H
this : x⁻¹ * n * x ∈ H
⊢ x⁻¹⁻¹ = x

Tactic:
rw [inv_inv]

Result:
no goals

Proof state:
G : Type u
inst✝¹ : Group G
H : Subgroup G
inst✝ : Finite ↑↑H
x : G
hx : ∀ (n : G), n ∈ H ↔ x * n * x⁻¹ ∈ H
y✝ : G ⧸ H
y : G
hy : Quotient.mk'' y ∈ orbit ↥H ↑x
b : G
hb₁ : b ∈ H
hb₂✝ : (fun m => m • ↑x) ⟨b, hb₁⟩ = Quotient.mk'' y
hb₂ : (b * x)⁻¹ * y ∈ H
⊢ b⁻¹ * (x * (y⁻¹ * x)⁻¹ * x⁻¹) ∈ H

Tactic:
rw [hx] at hb₂

Result:
G : Type u
inst✝¹ : Group G
H : Subgroup G
inst✝ : Finite ↑↑H
x : G
hx : ∀ (n : G), n ∈ H ↔ x * n * x⁻¹ ∈ H
y✝ : G ⧸ H
y : G
hy : Quotient.mk'' y ∈ orbit ↥H ↑x
b : G
hb₁ : b ∈ H
hb₂✝ : (fun m => m • ↑x) ⟨b, hb₁⟩ = Quotient.mk'' y
hb₂ : x * ((b * x)⁻¹ * y) * x⁻¹ ∈ H
⊢ b⁻¹ * (x * (y⁻¹ * x)⁻¹ * x⁻¹) ∈ H

Proof state:
G : Type u
inst✝¹ : Group G
H : Subgroup G
inst✝ : Finite ↑↑H
x : G
hx : ∀ (n : G), n ∈ H ↔ x * n * x⁻¹ ∈ H
y✝ : G ⧸ H
y : G
hy : Quotient.mk'' y ∈ orbit ↥H ↑x
b : G
hb₁ : b ∈ H
hb₂✝ : (fun m => m • ↑x) ⟨b, hb₁⟩ = Quotient.mk'' y
hb₂ : x * ((b * x)⁻¹ * y) * x⁻¹ ∈ H
⊢ b⁻¹ * (x * (y⁻¹ * x)⁻¹ * x⁻¹) ∈ H

Tactic:
simpa [mul_inv_rev, mul_assoc] using hb₂

Result:
no goals