-- Module: Mathlib.GroupTheory.FiniteAbelian.Duality
Goal:
G : Type u_1
M : Type u_2
inst : CommGroup G
inst_1 : Finite G
inst_2 : CommMonoid M
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
H : Subgroup G
x : G
h :
  Eq (α :=
      ↥((OrderDual.ofDual : (a : (Subgroup (G →* Mˣ))ᵒᵈ) → Subgroup (G →* Mˣ))
            ((fun (H : Subgroup G) ↦
                ((OrderDual.toDual : (a : Subgroup (G →* Mˣ)) → (Subgroup (G →* Mˣ))ᵒᵈ)
                    (ker (M := MonoidHom.{u_1, u_2} (↥H) Mˣ) (restrictHom H Mˣ)) :
                  (Subgroup (MonoidHom.{u_1, u_2} G Mˣ))ᵒᵈ))
              H)) →*
        Mˣ)
      ((restrictHom
              ((OrderDual.ofDual : (a : (Subgroup (G →* Mˣ))ᵒᵈ) → Subgroup (G →* Mˣ))
                ((fun (H : Subgroup G) ↦
                    ((OrderDual.toDual : (a : Subgroup (G →* Mˣ)) → (Subgroup (G →* Mˣ))ᵒᵈ)
                        (ker (M := MonoidHom.{u_1, u_2} (↥H) Mˣ) (restrictHom H Mˣ)) :
                      (Subgroup (MonoidHom.{u_1, u_2} G Mˣ))ᵒᵈ))
                  H))
              Mˣ :
            (a : (G →* Mˣ) →* Mˣ) →
              ↥((OrderDual.ofDual : (a : (Subgroup (G →* Mˣ))ᵒᵈ) → Subgroup (G →* Mˣ))
                    ((fun (H : Subgroup G) ↦
                        (OrderDual.toDual : (a : Subgroup (G →* Mˣ)) → (Subgroup (G →* Mˣ))ᵒᵈ) (restrictHom H Mˣ).ker)
                      H)) →*
                Mˣ)
          ((MulEquiv.symm (monoidHomMonoidHomEquiv G M) : (a : G) → (G →* Mˣ) →* Mˣ) x) :
        ↥((OrderDual.ofDual : (a : (Subgroup (G →* Mˣ))ᵒᵈ) → Subgroup (G →* Mˣ))
              ((fun (H : Subgroup G) ↦
                  ((OrderDual.toDual : (a : Subgroup (G →* Mˣ)) → (Subgroup (G →* Mˣ))ᵒᵈ)
                      (ker (M := MonoidHom.{u_1, u_2} (↥H) Mˣ) (restrictHom H Mˣ)) :
                    (Subgroup (MonoidHom.{u_1, u_2} G Mˣ))ᵒᵈ))
                H)) →*
          Mˣ)
      (1 :
        ↥((OrderDual.ofDual : (a : (Subgroup (G →* Mˣ))ᵒᵈ) → Subgroup (G →* Mˣ))
              ((fun (H : Subgroup G) ↦
                  ((OrderDual.toDual : (a : Subgroup (G →* Mˣ)) → (Subgroup (G →* Mˣ))ᵒᵈ)
                      (ker (M := MonoidHom.{u_1, u_2} (↥H) Mˣ) (restrictHom H Mˣ)) :
                    (Subgroup (MonoidHom.{u_1, u_2} G Mˣ))ᵒᵈ))
                H)) →*
          Mˣ) ↔
    x ∈ H
⊢ Membership.mem (γ := Subgroup G)
      ((fun (Φ : (Subgroup (MonoidHom.{u_1, u_2} G Mˣ))ᵒᵈ) ↦
          ((MulEquiv.mapSubgroup (monoidHomMonoidHomEquiv G M) : (a : Subgroup ((G →* Mˣ) →* Mˣ)) → Subgroup G)
              (ker (M :=
                ↥((OrderDual.ofDual : (a : (Subgroup (G →* Mˣ))ᵒᵈ) → Subgroup (G →* Mˣ)) Φ :
                      Subgroup (MonoidHom.{u_1, u_2} G Mˣ)) →*
                  Mˣ)
                (restrictHom ((OrderDual.ofDual : (a : (Subgroup (G →* Mˣ))ᵒᵈ) → Subgroup (G →* Mˣ)) Φ) Mˣ :
                  (MonoidHom.{u_1, u_2} G Mˣ →* Mˣ) →*
                    ↥((OrderDual.ofDual : (a : (Subgroup (G →* Mˣ))ᵒᵈ) → Subgroup (G →* Mˣ)) Φ :
                          Subgroup (MonoidHom.{u_1, u_2} G Mˣ)) →*
                      Mˣ)) :
            Subgroup G))
        ((fun (H : Subgroup G) ↦
            ((OrderDual.toDual : (a : Subgroup (G →* Mˣ)) → (Subgroup (G →* Mˣ))ᵒᵈ)
                (ker (M := MonoidHom.{u_1, u_2} (↥H) Mˣ) (restrictHom H Mˣ)) :
              (Subgroup (MonoidHom.{u_1, u_2} G Mˣ))ᵒᵈ))
          H))
      x ↔
    x ∈ H

Tactic:
rw [MulEquiv.coe_mapSubgroup, Subgroup.mem_map_equiv, MonoidHom.mem_ker]

Premises used: Subgroup.mem_map_equiv, MonoidHom.mem_ker, MulEquiv.coe_mapSubgroup