-- 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ˣ
e'' : (G →* Mˣ) ≃* (((i : ι) → Multiplicative (ZMod (n i))) →* Mˣ) := e.monoidHomCongr (MulEquiv.refl Mˣ)
this : ∀ (i : ι), NeZero (n i)
⊢ Nonempty ((G →* Mˣ) ≃* G)

Tactic:
have inst i : HasEnoughRootsOfUnity M <| Nat.card <| Multiplicative <| ZMod (n i) := by
  have hdvd : Nat.card (Multiplicative (ZMod (n i))) ∣ Monoid.exponent G := by
    simpa only [Nat.card_eq_fintype_card, Fintype.card_multiplicative, ZMod.card]
      using dvd_exponent e i
  exact HasEnoughRootsOfUnity.of_dvd M hdvd

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)
inst : ∀ (i : ι), HasEnoughRootsOfUnity M (Nat.card (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 : ι
hdvd : Nat.card (Multiplicative (ZMod (n i))) ∣ Monoid.exponent G
⊢ HasEnoughRootsOfUnity M (Nat.card (Multiplicative (ZMod (n i))))

Tactic:
exact HasEnoughRootsOfUnity.of_dvd M hdvd

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
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))))
⊢ Nonempty ((G →* Mˣ) ≃* G)

Tactic:
let E i := (IsCyclic.monoidHom_equiv_self (Multiplicative (ZMod (n i))) M).some

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)
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)

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:
classical obtain ⟨ι, _, n, ⟨h₁, h₂⟩⟩ := equiv_prod_multiplicative_zmod_of_finite G
let e := h₂.some
let e' := Pi.monoidHomMulEquiv (fun i ↦ Multiplicative (ZMod (n i))) Mˣ
let e'' := MulEquiv.monoidHomCongr e (.refl Mˣ)
have : ∀ i, NeZero (n i) := fun i ↦ NeZero.of_gt (h₁ i)
have inst i : HasEnoughRootsOfUnity M <| Nat.card <| Multiplicative <| ZMod (n i) := by
  have hdvd : Nat.card (Multiplicative (ZMod (n i))) ∣ Monoid.exponent G := by
    simpa only [Nat.card_eq_fintype_card, Fintype.card_multiplicative, ZMod.card]
      using dvd_exponent e i
  exact HasEnoughRootsOfUnity.of_dvd M hdvd
let E i := (IsCyclic.monoidHom_equiv_self (Multiplicative (ZMod (n i))) M).some
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))))
⊢ Nonempty ((G →* Mˣ) ≃* G)

Tactic:
let e := h₂.some

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
⊢ 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 : ι
⊢ HasEnoughRootsOfUnity M (Nat.card (Multiplicative (ZMod (n i))))

Tactic:
have hdvd : Nat.card (Multiplicative (ZMod (n i))) ∣ Monoid.exponent G := by
  simpa only [Nat.card_eq_fintype_card, Fintype.card_multiplicative, ZMod.card]
    using dvd_exponent e i

Result:
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 : ι
hdvd : Nat.card (Multiplicative (ZMod (n i))) ∣ Monoid.exponent G
⊢ HasEnoughRootsOfUnity M (Nat.card (Multiplicative (ZMod (n i))))