awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 rwa rwa₁ rwa₂ rwa₃ : HasEnoughRootsOfUnity M (Monoid.exponent G)
⊢ HasEnoughRootsOfUnity M (Monoid.exponent (MonoidHom.{u_1, u_2} G Mˣ))

Tactic:
rwa [Monoid.exponent_eq_of_mulEquiv (monoidHom_mulEquiv_of_hasEnoughRootsOfUnity G M).some]

Premises used: CommGroup.monoidHom_mulEquiv_of_hasEnoughRootsOfUnity, Nonempty.some, Monoid.exponent_eq_of_mulEquiv
-- 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)
this : HasEnoughRootsOfUnity M (Monoid.exponent (MonoidHom.{u_1, u_2} G Mˣ))
g : G
⊢ ∀ (x y : MonoidHom.{u_1, u_2} G Mˣ),
    OneHom.toFun { toFun := fun (φ : MonoidHom.{u_1, u_2} G Mˣ) ↦ (φ : (a : G) → Mˣ) g, map_one' := ⋯ } (x * y) =
      HMul.hMul (α := Mˣ)
        (OneHom.toFun
          { toFun := fun (φ : MonoidHom.{u_1, u_2} G Mˣ) ↦ (φ : (a : G) → Mˣ) g, map_one' := ⋯ :
            OneHom (MonoidHom.{u_1, u_2} G Mˣ) Mˣ }
          x)
        (OneHom.toFun
          { toFun := fun (φ : MonoidHom.{u_1, u_2} G Mˣ) ↦ (φ : (a : G) → Mˣ) g, map_one' := ⋯ :
            OneHom (MonoidHom.{u_1, u_2} G Mˣ) Mˣ }
          y)

Tactic:
simp
-- 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)
this : HasEnoughRootsOfUnity M (Monoid.exponent (MonoidHom.{u_1, u_2} G Mˣ))
⊢ Function.Bijective (β := MonoidHom.{u_1, u_2} G Mˣ →* Mˣ) fun (g : G) ↦
    { toFun := fun (φ : MonoidHom.{u_1, u_2} G Mˣ) ↦ (φ : (a : G) → Mˣ) g, map_one' := ⋯, map_mul' := ⋯ }

Tactic:
(Nat.bijective_iff_injective_and_card _).mpr ⟨fun _ _ h ↦ ?_, ?_⟩

Premises used: Iff.mpr, Nat.bijective_iff_injective_and_card, And.intro
-- 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)
this : HasEnoughRootsOfUnity M (Monoid.exponent (MonoidHom.{u_1, u_2} G Mˣ))
refine_1 :
  ∀ (x x_1 : G)
    (h :
      Eq (α := MonoidHom.{u_1, u_2} G Mˣ →* Mˣ)
        ((fun (g : G) ↦
            ({ toFun := fun (φ : MonoidHom.{u_1, u_2} G Mˣ) ↦ (φ : (a : G) → Mˣ) g, map_one' := ⋯, map_mul' := ⋯ } :
              MonoidHom.{u_1, u_2} G Mˣ →* Mˣ))
          x)
        ((fun (g : G) ↦
            ({ toFun := fun (φ : MonoidHom.{u_1, u_2} G Mˣ) ↦ (φ : (a : G) → Mˣ) g, map_one' := ⋯, map_mul' := ⋯ } :
              MonoidHom.{u_1, u_2} G Mˣ →* Mˣ))
          x_1)),
    x = x_1
refine_2 : Nat.card G = Nat.card (MonoidHom.{u_1, u_2} G Mˣ →* Mˣ)
⊢ Function.Bijective (β := MonoidHom.{u_1, u_2} G Mˣ →* Mˣ) fun (g : G) ↦
    { toFun := fun (φ : MonoidHom.{u_1, u_2} G Mˣ) ↦ (φ : (a : G) → Mˣ) g, map_one' := ⋯, map_mul' := ⋯ }

Tactic:
refine (Nat.bijective_iff_injective_and_card _).mpr ⟨fun _ _ h ↦ ?_, ?_⟩

Premises used: Iff.mpr, Nat.bijective_iff_injective_and_card, And.intro
-- 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)
this : HasEnoughRootsOfUnity M (Monoid.exponent (MonoidHom.{u_1, u_2} G Mˣ))
x x_1 : G
h :
  Eq (α := MonoidHom.{u_1, u_2} G Mˣ →* Mˣ)
    ((fun (g : G) ↦
        ({ toFun := fun (φ : MonoidHom.{u_1, u_2} G Mˣ) ↦ (φ : (a : G) → Mˣ) g, map_one' := ⋯, map_mul' := ⋯ } :
          MonoidHom.{u_1, u_2} G Mˣ →* Mˣ))
      x)
    ((fun (g : G) ↦
        ({ toFun := fun (φ : MonoidHom.{u_1, u_2} G Mˣ) ↦ (φ : (a : G) → Mˣ) g, map_one' := ⋯, map_mul' := ⋯ } :
          MonoidHom.{u_1, u_2} G Mˣ →* Mˣ))
      x_1)
refine_1 :
  ∀
    (h :
      Eq (α := OneHom (MonoidHom.{u_1, u_2} G Mˣ) Mˣ)
        { toFun := fun (φ : MonoidHom.{u_1, u_2} G Mˣ) ↦ (φ : (a : G) → Mˣ) x, map_one' := ⋯ }
        { toFun := fun (φ : MonoidHom.{u_1, u_2} G Mˣ) ↦ (φ : (a : G) → Mˣ) x_1, map_one' := ⋯ }),
    x = x_1
refine_1₁ :
  ∀
    (h :
      Eq (α := MonoidHom.{u_1, u_2} G Mˣ → Mˣ) (fun (φ : MonoidHom.{u_1, u_2} G Mˣ) ↦ (φ : (a : G) → Mˣ) x)
        fun (φ : MonoidHom.{u_1, u_2} G Mˣ) ↦ (φ : (a : G) → Mˣ) x_1),
    x = x_1
refine_1₂ :
  ∀
    (h :
      ∀ (x_2 : MonoidHom.{u_1, u_2} G Mˣ),
        Eq.{u_2 + 1} (α := Mˣ) ((x_2 : (a : G) → Mˣ) x : Mˣ) ((x_2 : (a : G) → Mˣ) x_1 : Mˣ)),
    x = x_1
refine_1₃ refine_1₄ refine_1₅ refine_1₆ : ∀ (h : x = x_1), x = x_1
⊢ x = x_1

Tactic:
rwa [mk.injEq, OneHom.mk.injEq, funext_iff, forall_apply_eq_apply_iff] at h

Premises used: OneHom.mk.injEq, funext_iff, CommGroup.forall_apply_eq_apply_iff, MonoidHom.mk.injEq
-- 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)
this : HasEnoughRootsOfUnity M (Monoid.exponent (MonoidHom.{u_1, u_2} G Mˣ))
refine_2 : Nat.card G = Nat.card (MonoidHom.{u_1, u_2} G Mˣ)
refine_2₁ refine_2₂ : Nat.card G = Nat.card G
⊢ Nat.card G = Nat.card (MonoidHom.{u_1, u_2} G Mˣ →* Mˣ)

Tactic:
rw [card_monoidHom_of_hasEnoughRootsOfUnity, card_monoidHom_of_hasEnoughRootsOfUnity]

Premises used: CommGroup.card_monoidHom_of_hasEnoughRootsOfUnity
-- 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)
this : HasEnoughRootsOfUnity M (Monoid.exponent (MonoidHom.{u_1, u_2} G Mˣ))
x x_1 : G
h :
  ∀ (x_2 : MonoidHom.{u_1, u_2} G Mˣ),
    Eq.{u_2 + 1} (α := M)
      (↑((((Equiv.ofBijective
                      (fun (g : G) ↦
                        { toFun := fun (φ : MonoidHom.{u_1, u_2} G Mˣ) ↦ (φ : (a : G) → Mˣ) g, map_one' := ⋯,
                          map_mul' := ⋯ : MonoidHom.{u_1, u_2} G Mˣ →* Mˣ })
                      ⋯ :
                    (a : G) → (G →* Mˣ) →* Mˣ)
                  (x * x_1) :
                MonoidHom.{u_1, u_2} G Mˣ →* Mˣ) :
              (a : G →* Mˣ) → Mˣ)
            x_2) :
        M)
      (↑((HMul.hMul (α := MonoidHom.{u_1, u_2} G Mˣ →* Mˣ) (β := MonoidHom.{u_1, u_2} G Mˣ →* Mˣ)
                ((Equiv.ofBijective
                        (fun (g : G) ↦
                          { toFun := fun (φ : MonoidHom.{u_1, u_2} G Mˣ) ↦ (φ : (a : G) → Mˣ) g, map_one' := ⋯,
                            map_mul' := ⋯ : MonoidHom.{u_1, u_2} G Mˣ →* Mˣ })
                        ⋯ :
                      (a : G) → (G →* Mˣ) →* Mˣ)
                    x :
                  MonoidHom.{u_1, u_2} G Mˣ →* Mˣ)
                ((Equiv.ofBijective
                        (fun (g : G) ↦
                          { toFun := fun (φ : MonoidHom.{u_1, u_2} G Mˣ) ↦ (φ : (a : G) → Mˣ) g, map_one' := ⋯,
                            map_mul' := ⋯ : MonoidHom.{u_1, u_2} G Mˣ →* Mˣ })
                        ⋯ :
                      (a : G) → (G →* Mˣ) →* Mˣ)
                    x_1 :
                  MonoidHom.{u_1, u_2} G Mˣ →* Mˣ) :
              (a : G →* Mˣ) → Mˣ)
            x_2) :
        M)
⊢ (Equiv.ofBijective
          (fun (g : G) ↦
            { toFun := fun (φ : MonoidHom.{u_1, u_2} G Mˣ) ↦ (φ : (a : G) → Mˣ) g, map_one' := ⋯, map_mul' := ⋯ :
              MonoidHom.{u_1, u_2} G Mˣ →* Mˣ })
          ⋯ :
        (a : G) → (G →* Mˣ) →* Mˣ)
      (x * x_1) =
    HMul.hMul (α := MonoidHom.{u_1, u_2} G Mˣ →* Mˣ) (β := MonoidHom.{u_1, u_2} G Mˣ →* Mˣ)
      ((Equiv.ofBijective
              (fun (g : G) ↦
                { toFun := fun (φ : MonoidHom.{u_1, u_2} G Mˣ) ↦ (φ : (a : G) → Mˣ) g, map_one' := ⋯, map_mul' := ⋯ :
                  MonoidHom.{u_1, u_2} G Mˣ →* Mˣ })
              ⋯ :
            (a : G) → (G →* Mˣ) →* Mˣ)
          x :
        MonoidHom.{u_1, u_2} G Mˣ →* Mˣ)
      ((Equiv.ofBijective
              (fun (g : G) ↦
                { toFun := fun (φ : MonoidHom.{u_1, u_2} G Mˣ) ↦ (φ : (a : G) → Mˣ) g, map_one' := ⋯, map_mul' := ⋯ :
                  MonoidHom.{u_1, u_2} G Mˣ →* Mˣ })
              ⋯ :
            (a : G) → (G →* Mˣ) →* Mˣ)
          x_1 :
        MonoidHom.{u_1, u_2} G Mˣ →* Mˣ)

Tactic:
ext
-- 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)
this : HasEnoughRootsOfUnity M (Monoid.exponent (MonoidHom.{u_1, u_2} G Mˣ))
x x_1 : G
x_2 : MonoidHom.{u_1, u_2} G Mˣ
⊢ Eq.{u_2 + 1} (α := M)
    (↑((((Equiv.ofBijective
                    (fun (g : G) ↦
                      { toFun := fun (φ : MonoidHom.{u_1, u_2} G Mˣ) ↦ (φ : (a : G) → Mˣ) g, map_one' := ⋯,
                        map_mul' := ⋯ : MonoidHom.{u_1, u_2} G Mˣ →* Mˣ })
                    ⋯ :
                  (a : G) → (G →* Mˣ) →* Mˣ)
                (x * x_1) :
              MonoidHom.{u_1, u_2} G Mˣ →* Mˣ) :
            (a : G →* Mˣ) → Mˣ)
          x_2) :
      M)
    (↑((HMul.hMul (α := MonoidHom.{u_1, u_2} G Mˣ →* Mˣ) (β := MonoidHom.{u_1, u_2} G Mˣ →* Mˣ)
              ((Equiv.ofBijective
                      (fun (g : G) ↦
                        { toFun := fun (φ : MonoidHom.{u_1, u_2} G Mˣ) ↦ (φ : (a : G) → Mˣ) g, map_one' := ⋯,
                          map_mul' := ⋯ : MonoidHom.{u_1, u_2} G Mˣ →* Mˣ })
                      ⋯ :
                    (a : G) → (G →* Mˣ) →* Mˣ)
                  x :
                MonoidHom.{u_1, u_2} G Mˣ →* Mˣ)
              ((Equiv.ofBijective
                      (fun (g : G) ↦
                        { toFun := fun (φ : MonoidHom.{u_1, u_2} G Mˣ) ↦ (φ : (a : G) → Mˣ) g, map_one' := ⋯,
                          map_mul' := ⋯ : MonoidHom.{u_1, u_2} G Mˣ →* Mˣ })
                      ⋯ :
                    (a : G) → (G →* Mˣ) →* Mˣ)
                  x_1 :
                MonoidHom.{u_1, u_2} G Mˣ →* Mˣ) :
            (a : G →* Mˣ) → Mˣ)
          x_2) :
      M)

Tactic:
simp
-- 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)
φ : MonoidHom.{u_1, u_2} G Mˣ
η : MonoidHom.{u_1, u_2} G Mˣ →* Mˣ
rw :
  Eq.{u_2 + 1} (α := Mˣ)
    ((((MulEquiv.symm (monoidHomMonoidHomEquiv G M) : (a : G) → (G →* Mˣ) →* Mˣ)
              ((monoidHomMonoidHomEquiv G M : (a : (G →* Mˣ) →* Mˣ) → G) η) :
            MonoidHom.{u_1, u_2} G Mˣ →* Mˣ) :
          (a : G →* Mˣ) → Mˣ)
        φ :
      Mˣ)
    ((η : (a : G →* Mˣ) → Mˣ) φ : Mˣ)
rw₁ rw₂ : Eq.{u_2 + 1} (α := Mˣ) ((η : (a : G →* Mˣ) → Mˣ) φ : Mˣ) ((η : (a : G →* Mˣ) → Mˣ) φ : Mˣ)
⊢ Eq.{u_2 + 1} (α := Mˣ) ((φ : (a : G) → Mˣ) ((monoidHomMonoidHomEquiv G M : (a : (G →* Mˣ) →* Mˣ) → G) η) : Mˣ)
    ((η : (a : G →* Mˣ) → Mˣ) φ : Mˣ)

Tactic:
rw [← monoidHomMonoidHomEquiv_symm_apply_apply G M (monoidHomMonoidHomEquiv G M η) φ,
    MulEquiv.symm_apply_apply]

Premises used: CommGroup.monoidHomMonoidHomEquiv_symm_apply_apply, DFunLike.coe, CommGroup.monoidHomMonoidHomEquiv, MulEquiv.symm_apply_apply
-- 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
h :
  ∀ (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
⊢ (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) =
    H

Tactic:
ext x
-- 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
⊢ 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:
simp
-- 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)
Φ : (Subgroup (MonoidHom.{u_1, u_2} G Mˣ))ᵒᵈ
rwa rwa₁ rwa₂ rwa₃ : HasEnoughRootsOfUnity M (Monoid.exponent G)
⊢ HasEnoughRootsOfUnity M (Monoid.exponent (MonoidHom.{u_1, u_2} G Mˣ))

Tactic:
rwa [Monoid.exponent_eq_of_mulEquiv (monoidHom_mulEquiv_of_hasEnoughRootsOfUnity G M).some]

Premises used: CommGroup.monoidHom_mulEquiv_of_hasEnoughRootsOfUnity, Nonempty.some, Monoid.exponent_eq_of_mulEquiv
-- 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)
Φ : (Subgroup (MonoidHom.{u_1, u_2} G Mˣ))ᵒᵈ
⊢ HasEnoughRootsOfUnity M (Monoid.exponent (MonoidHom.{u_1, u_2} G Mˣ))

Tactic:
have : HasEnoughRootsOfUnity M (Monoid.exponent (G →* Mˣ)) := by
      rwa [Monoid.exponent_eq_of_mulEquiv (monoidHom_mulEquiv_of_hasEnoughRootsOfUnity G M).some]
-- 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)
Φ : (Subgroup (MonoidHom.{u_1, u_2} G Mˣ))ᵒᵈ
this : HasEnoughRootsOfUnity M (Monoid.exponent (MonoidHom.{u_1, u_2} G Mˣ))
h :
  ∀ (φ : MonoidHom.{u_1, u_2} G Mˣ),
    Membership.mem (γ := Subgroup (MonoidHom.{u_1, u_2} G Mˣ))
        ((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ˣ))ᵒᵈ))
            ((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))
              Φ)))
        φ ↔
      Membership.mem (γ := Subgroup (MonoidHom.{u_1, u_2} G Mˣ))
        ((OrderDual.ofDual : (a : (Subgroup (G →* Mˣ))ᵒᵈ) → Subgroup (G →* Mˣ)) Φ :
          Subgroup (MonoidHom.{u_1, u_2} 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ˣ))ᵒᵈ))
      ((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))
        Φ) =
    Φ

Tactic:
ext φ
-- 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)
Φ : (Subgroup (MonoidHom.{u_1, u_2} G Mˣ))ᵒᵈ
this : HasEnoughRootsOfUnity M (Monoid.exponent (MonoidHom.{u_1, u_2} G Mˣ))
φ : MonoidHom.{u_1, u_2} G Mˣ
h :
  (∀ (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))
            Φ)
          x →
        Eq.{u_2 + 1} (α := Mˣ) ((φ : (a : G) → Mˣ) x : Mˣ) (1 : Mˣ)) ↔
    Membership.mem (γ := Subgroup (MonoidHom.{u_1, u_2} G Mˣ))
      ((OrderDual.ofDual : (a : (Subgroup (G →* Mˣ))ᵒᵈ) → Subgroup (G →* Mˣ)) Φ : Subgroup (MonoidHom.{u_1, u_2} G Mˣ))
      φ
⊢ Membership.mem (γ := Subgroup (MonoidHom.{u_1, u_2} G Mˣ))
      ((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ˣ))ᵒᵈ))
          ((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))
            Φ)))
      φ ↔
    Membership.mem (γ := Subgroup (MonoidHom.{u_1, u_2} G Mˣ))
      ((OrderDual.ofDual : (a : (Subgroup (G →* Mˣ))ᵒᵈ) → Subgroup (G →* Mˣ)) Φ : Subgroup (MonoidHom.{u_1, u_2} G Mˣ))
      φ

Tactic:
rw [OrderDual.ofDual_toDual, mem_ker, restrictHom_apply, restrict_eq_one_iff]

Premises used: MonoidHom.mem_ker, MonoidHom.restrict_eq_one_iff, MonoidHom.restrictHom_apply, OrderDual.ofDual_toDual
-- 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)
Φ : (Subgroup (MonoidHom.{u_1, u_2} G Mˣ))ᵒᵈ
this : HasEnoughRootsOfUnity M (Monoid.exponent (MonoidHom.{u_1, u_2} G Mˣ))
φ : MonoidHom.{u_1, u_2} G Mˣ
⊢ (∀ (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))
            Φ)
          x →
        Eq.{u_2 + 1} (α := Mˣ) ((φ : (a : G) → Mˣ) x : Mˣ) (1 : Mˣ)) ↔
    Membership.mem (γ := Subgroup (MonoidHom.{u_1, u_2} G Mˣ))
      ((OrderDual.ofDual : (a : (Subgroup (G →* Mˣ))ᵒᵈ) → Subgroup (G →* Mˣ)) Φ : Subgroup (MonoidHom.{u_1, u_2} G Mˣ))
      φ

Tactic:
simp