-- Mathlib/GroupTheory/FiniteAbelian/Duality.lean
theorem monoidHom_mulEquiv_of_hasEnoughRootsOfUnity : Nonempty ((G →* Mˣ) ≃* G)

Proof state:
case intro.intro.intro.intro
G : Type u_1
M : Type u_2
inst✝³ : CommGroup G
inst✝² : Finite G
inst✝¹ : CommMonoid M
inst✝ : HasEnoughRootsOfUnity M (Monoid.exponent G)
ι : Type
w✝ : Fintype ι
n : ι → ℕ
h₁ : ∀ (i : ι), 1 < n i
h₂ : Nonempty (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))
e : G ≃* ((i : ι) → Multiplicative (ZMod (n i))) := h₂.some
e' : (((i : ι) → Multiplicative (ZMod (n i))) →* Mˣ) ≃* ((i : ι) → Multiplicative (ZMod (n i)) →* Mˣ) :=
  Pi.monoidHomMulEquiv (fun i => Multiplicative (ZMod (n i))) Mˣ
⊢ Nonempty ((G →* Mˣ) ≃* G)

Tactic:
let e'' := MulEquiv.monoidHomCongr e (.refl Mˣ)

Result:
case intro.intro.intro.intro
G : Type u_1
M : Type u_2
inst✝³ : CommGroup G
inst✝² : Finite G
inst✝¹ : CommMonoid M
inst✝ : HasEnoughRootsOfUnity M (Monoid.exponent G)
ι : Type
w✝ : Fintype ι
n : ι → ℕ
h₁ : ∀ (i : ι), 1 < n i
h₂ : Nonempty (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))
e : G ≃* ((i : ι) → Multiplicative (ZMod (n i))) := h₂.some
e' : (((i : ι) → Multiplicative (ZMod (n i))) →* Mˣ) ≃* ((i : ι) → Multiplicative (ZMod (n i)) →* Mˣ) :=
  Pi.monoidHomMulEquiv (fun i => Multiplicative (ZMod (n i))) Mˣ
e'' : (G →* Mˣ) ≃* (((i : ι) → Multiplicative (ZMod (n i))) →* Mˣ) := e.monoidHomCongr (MulEquiv.refl Mˣ)
⊢ Nonempty ((G →* Mˣ) ≃* G)

Proof state:
case intro.intro.intro.intro
G : Type u_1
M : Type u_2
inst✝³ : CommGroup G
inst✝² : Finite G
inst✝¹ : CommMonoid M
inst✝ : HasEnoughRootsOfUnity M (Monoid.exponent G)
ι : Type
w✝ : Fintype ι
n : ι → ℕ
h₁ : ∀ (i : ι), 1 < n i
h₂ : Nonempty (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))
e : G ≃* ((i : ι) → Multiplicative (ZMod (n i))) := h₂.some
e' : (((i : ι) → Multiplicative (ZMod (n i))) →* Mˣ) ≃* ((i : ι) → Multiplicative (ZMod (n i)) →* Mˣ) :=
  Pi.monoidHomMulEquiv (fun i => Multiplicative (ZMod (n i))) Mˣ
e'' : (G →* Mˣ) ≃* (((i : ι) → Multiplicative (ZMod (n i))) →* Mˣ) := e.monoidHomCongr (MulEquiv.refl Mˣ)
this : ∀ (i : ι), NeZero (n i)
inst : ∀ (i : ι), HasEnoughRootsOfUnity M (Nat.card (Multiplicative (ZMod (n i))))
E : (i : ι) → (Multiplicative (ZMod (n i)) →* Mˣ) ≃* Multiplicative (ZMod (n i)) := fun i => ⋯.some
⊢ Nonempty ((G →* Mˣ) ≃* G)

Tactic:
exact ⟨e''.trans <| e'.trans <| (MulEquiv.piCongrRight E).trans e.symm⟩

Result:
no goals

Proof state:
case intro.intro.intro.intro
G : Type u_1
M : Type u_2
inst✝³ : CommGroup G
inst✝² : Finite G
inst✝¹ : CommMonoid M
inst✝ : HasEnoughRootsOfUnity M (Monoid.exponent G)
ι : Type
w✝ : Fintype ι
n : ι → ℕ
h₁ : ∀ (i : ι), 1 < n i
h₂ : Nonempty (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))
e : G ≃* ((i : ι) → Multiplicative (ZMod (n i))) := h₂.some
⊢ Nonempty ((G →* Mˣ) ≃* G)

Tactic:
let e' := Pi.monoidHomMulEquiv (fun i ↦ Multiplicative (ZMod (n i))) Mˣ

Result:
case intro.intro.intro.intro
G : Type u_1
M : Type u_2
inst✝³ : CommGroup G
inst✝² : Finite G
inst✝¹ : CommMonoid M
inst✝ : HasEnoughRootsOfUnity M (Monoid.exponent G)
ι : Type
w✝ : Fintype ι
n : ι → ℕ
h₁ : ∀ (i : ι), 1 < n i
h₂ : Nonempty (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))
e : G ≃* ((i : ι) → Multiplicative (ZMod (n i))) := h₂.some
e' : (((i : ι) → Multiplicative (ZMod (n i))) →* Mˣ) ≃* ((i : ι) → Multiplicative (ZMod (n i)) →* Mˣ) :=
  Pi.monoidHomMulEquiv (fun i => Multiplicative (ZMod (n i))) Mˣ
⊢ Nonempty ((G →* Mˣ) ≃* G)

Proof state:
case intro.intro.intro.intro
G : Type u_1
M : Type u_2
inst✝³ : CommGroup G
inst✝² : Finite G
inst✝¹ : CommMonoid M
inst✝ : HasEnoughRootsOfUnity M (Monoid.exponent G)
ι : Type
w✝ : Fintype ι
n : ι → ℕ
h₁ : ∀ (i : ι), 1 < n i
h₂ : Nonempty (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))
e : G ≃* ((i : ι) → Multiplicative (ZMod (n i))) := h₂.some
e' : (((i : ι) → Multiplicative (ZMod (n i))) →* Mˣ) ≃* ((i : ι) → Multiplicative (ZMod (n i)) →* Mˣ) :=
  Pi.monoidHomMulEquiv (fun i => Multiplicative (ZMod (n i))) Mˣ
e'' : (G →* Mˣ) ≃* (((i : ι) → Multiplicative (ZMod (n i))) →* Mˣ) := e.monoidHomCongr (MulEquiv.refl Mˣ)
⊢ Nonempty ((G →* Mˣ) ≃* G)

Tactic:
have : ∀ i, NeZero (n i) := fun i ↦ NeZero.of_gt (h₁ i)

Result:
case intro.intro.intro.intro
G : Type u_1
M : Type u_2
inst✝³ : CommGroup G
inst✝² : Finite G
inst✝¹ : CommMonoid M
inst✝ : HasEnoughRootsOfUnity M (Monoid.exponent G)
ι : Type
w✝ : Fintype ι
n : ι → ℕ
h₁ : ∀ (i : ι), 1 < n i
h₂ : Nonempty (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))
e : G ≃* ((i : ι) → Multiplicative (ZMod (n i))) := h₂.some
e' : (((i : ι) → Multiplicative (ZMod (n i))) →* Mˣ) ≃* ((i : ι) → Multiplicative (ZMod (n i)) →* Mˣ) :=
  Pi.monoidHomMulEquiv (fun i => Multiplicative (ZMod (n i))) Mˣ
e'' : (G →* Mˣ) ≃* (((i : ι) → Multiplicative (ZMod (n i))) →* Mˣ) := e.monoidHomCongr (MulEquiv.refl Mˣ)
this : ∀ (i : ι), NeZero (n i)
⊢ Nonempty ((G →* Mˣ) ≃* G)

Proof state:
G : Type u_1
M : Type u_2
inst✝³ : CommGroup G
inst✝² : Finite G
inst✝¹ : CommMonoid M
inst✝ : HasEnoughRootsOfUnity M (Monoid.exponent G)
⊢ Nonempty ((G →* Mˣ) ≃* G)

Tactic:
obtain ⟨ι, _, n, ⟨h₁, h₂⟩⟩ := equiv_prod_multiplicative_zmod_of_finite G

Result:
case intro.intro.intro.intro
G : Type u_1
M : Type u_2
inst✝³ : CommGroup G
inst✝² : Finite G
inst✝¹ : CommMonoid M
inst✝ : HasEnoughRootsOfUnity M (Monoid.exponent G)
ι : Type
w✝ : Fintype ι
n : ι → ℕ
h₁ : ∀ (i : ι), 1 < n i
h₂ : Nonempty (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))
⊢ Nonempty ((G →* Mˣ) ≃* G)

Proof state:
G : Type u_1
M : Type u_2
inst✝³ : CommGroup G
inst✝² : Finite G
inst✝¹ : CommMonoid M
inst✝ : HasEnoughRootsOfUnity M (Monoid.exponent G)
ι : Type
w✝ : Fintype ι
n : ι → ℕ
h₁ : ∀ (i : ι), 1 < n i
h₂ : Nonempty (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))
e : G ≃* ((i : ι) → Multiplicative (ZMod (n i))) := h₂.some
e' : (((i : ι) → Multiplicative (ZMod (n i))) →* Mˣ) ≃* ((i : ι) → Multiplicative (ZMod (n i)) →* Mˣ) :=
  Pi.monoidHomMulEquiv (fun i => Multiplicative (ZMod (n i))) Mˣ
e'' : (G →* Mˣ) ≃* (((i : ι) → Multiplicative (ZMod (n i))) →* Mˣ) := e.monoidHomCongr (MulEquiv.refl Mˣ)
this : ∀ (i : ι), NeZero (n i)
i : ι
⊢ Nat.card (Multiplicative (ZMod (n i))) ∣ Monoid.exponent G

Tactic:
simpa only [Nat.card_eq_fintype_card, Fintype.card_multiplicative, ZMod.card]
  using dvd_exponent e i

Result:
no goals