-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Duality (goal)
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
⊢ 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
have 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
Tactic: rw [MulEquiv.coe_mapSubgroup, Subgroup.mem_map_equiv, MonoidHom.mem_ker]