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 : HasEnoughRootsOfUnity M (Monoid.exponent G)
a_1 : G
ha : a_1 ≠ 1
n : ℕ
hn : n ∣ Monoid.exponent G
a : ZMod n
ha₀ : a ≠ 0
⊢ NeZero n

Tactic:
have : NeZero n := ⟨fun H ↦ NeZero.ne _ <| Nat.eq_zero_of_zero_dvd (H ▸ hn)⟩
-- 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)
a_1 : G
ha : a_1 ≠ 1
n : ℕ
hn : n ∣ Monoid.exponent G
a : ZMod n
ha₀ : a ≠ 0
this : NeZero n
⊢ HasEnoughRootsOfUnity M n

Tactic:
have := HasEnoughRootsOfUnity.of_dvd M hn
-- 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)
a_1 : G
ha : a_1 ≠ 1
n : ℕ
hn : n ∣ Monoid.exponent G
a : ZMod n
ha₀ : a ≠ 0
this_1 : NeZero n
this : HasEnoughRootsOfUnity M n
⊢ ∃ (φ : Multiplicative (ZMod n) →* Mˣ),
    Ne (α := Mˣ)
      ((φ : (a : Multiplicative (ZMod n)) → Mˣ)
          ((Multiplicative.ofAdd : (a : ZMod n) → Multiplicative (ZMod n)) a : Multiplicative (ZMod n)) :
        Mˣ)
      (1 : Mˣ)

Tactic:
ZMod.exists_monoidHom_apply_ne_one (HasEnoughRootsOfUnity.exists_primitiveRoot M n) ha₀

Premises used: HasEnoughRootsOfUnity.exists_primitiveRoot, ZMod.exists_monoidHom_apply_ne_one
-- 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)
a_1 : G
ha : a_1 ≠ 1
n : ℕ
hn : n ∣ Monoid.exponent G
a : ZMod n
ha₀ : a ≠ 0
this_1 : NeZero n
this : HasEnoughRootsOfUnity M n
⊢ ∃ (φ : Multiplicative (ZMod n) →* Mˣ),
    Ne (α := Mˣ)
      ((φ : (a : Multiplicative (ZMod n)) → Mˣ)
          ((Multiplicative.ofAdd : (a : ZMod n) → Multiplicative (ZMod n)) a : Multiplicative (ZMod n)) :
        Mˣ)
      (1 : Mˣ)

Tactic:
exact ZMod.exists_monoidHom_apply_ne_one (HasEnoughRootsOfUnity.exists_primitiveRoot M n) ha₀

Premises used: HasEnoughRootsOfUnity.exists_primitiveRoot, ZMod.exists_monoidHom_apply_ne_one
-- 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)
g g' : G
h : g = g'
⊢ ∀ (φ : MonoidHom.{u_1, u_2} G Mˣ), Eq.{u_2 + 1} (α := Mˣ) ((φ : (a : G) → Mˣ) g : Mˣ) ((φ : (a : G) → Mˣ) g' : Mˣ)

Tactic:
simp [h]
-- 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)
g g' : G
refine :
  ∀
    (h :
      ∀ (φ : MonoidHom.{u_1, u_2} G Mˣ),
        Eq.{u_2 + 1} (α := Mˣ) ((φ : (a : G) → Mˣ) g : Mˣ) ((φ : (a : G) → Mˣ) g' : Mˣ)),
    g = g'
⊢ (∀ (φ : MonoidHom.{u_1, u_2} G Mˣ), Eq.{u_2 + 1} (α := Mˣ) ((φ : (a : G) → Mˣ) g : Mˣ) ((φ : (a : G) → Mˣ) g' : Mˣ)) ↔
    g = g'

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
-- 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)
g g' : G
h : ∀ (φ : MonoidHom.{u_1, u_2} G Mˣ), Eq.{u_2 + 1} (α := Mˣ) ((φ : (a : G) → Mˣ) g : Mˣ) ((φ : (a : G) → Mˣ) g' : Mˣ)
⊢ g = g'

Tactic:
simpa [← not_forall, not_imp_not, mul_inv_eq_one, h] using
    exists_apply_ne_one_of_hasEnoughRootsOfUnity G M (a := g * g'⁻¹)

Premises used: mul_inv_eq_one, CommGroup.exists_apply_ne_one_of_hasEnoughRootsOfUnity, Classical.not_forall, not_imp_not
-- 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)
obtain :
  ∀ (ι : Type) (w : Fintype ι) (n : ι → ℕ) (h₁ : ∀ (i : ι), 1 < n i)
    (h₂ : Nonempty.{u_1 + 1} (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))), Nonempty (MonoidHom.{u_1, u_2} G Mˣ ≃* G)
⊢ Nonempty (MonoidHom.{u_1, u_2} G Mˣ ≃* G)

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

Premises used: CommGroup.equiv_prod_multiplicative_zmod_of_finite
-- 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)
ι : Type
w : Fintype ι
n : ι → ℕ
h₁ : ∀ (i : ι), 1 < n i
h₂ : Nonempty.{u_1 + 1} (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ˣ
⊢ ∀ (i : ι), NeZero (n i)

Tactic:
have : ∀ i, NeZero (n i) := fun i ↦ NeZero.of_gt (h₁ i)
-- 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)
ι : Type
w : Fintype ι
n : ι → ℕ
h₁ : ∀ (i : ι), 1 < n i
h₂ : Nonempty.{u_1 + 1} (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ˣ
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

Premises used: _private.0.CommGroup.dvd_exponent, Fintype.card_multiplicative, ZMod.card, Nat.card_eq_fintype_card
-- 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)
ι : Type
w : Fintype ι
n : ι → ℕ
h₁ : ∀ (i : ι), 1 < n i
h₂ : Nonempty.{u_1 + 1} (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ˣ
this : ∀ (i : ι), NeZero (n i)
i : ι
⊢ Nat.card (Multiplicative (ZMod (n i))) ∣ Monoid.exponent G

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
-- 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)
ι : Type
w : Fintype ι
n : ι → ℕ
h₁ : ∀ (i : ι), 1 < n i
h₂ : Nonempty.{u_1 + 1} (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ˣ
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:
HasEnoughRootsOfUnity.of_dvd M hdvd

Premises used: HasEnoughRootsOfUnity.of_dvd
-- 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)
ι : Type
w : Fintype ι
n : ι → ℕ
h₁ : ∀ (i : ι), 1 < n i
h₂ : Nonempty.{u_1 + 1} (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ˣ
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

Premises used: HasEnoughRootsOfUnity.of_dvd
-- 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)
ι : Type
w : Fintype ι
n : ι → ℕ
h₁ : ∀ (i : ι), 1 < n i
h₂ : Nonempty.{u_1 + 1} (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ˣ
this : ∀ (i : ι), NeZero (n i)
⊢ ∀ (i : ι), HasEnoughRootsOfUnity M (Nat.card (Multiplicative (ZMod (n i))))

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
-- Module: Mathlib.GroupTheory.FiniteAbelian.Duality
Goal:
G : Type u_1
M : Type u_2
inst_1 : CommGroup G
inst_2 : Finite G
inst_3 : CommMonoid M
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
ι : Type
w : Fintype ι
n : ι → ℕ
h₁ : ∀ (i : ι), 1 < n i
h₂ : Nonempty.{u_1 + 1} (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ˣ
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 : ι) ↦ Nonempty.some ⋯
⊢ Nonempty (MonoidHom.{u_1, u_2} G Mˣ ≃* G)

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

Premises used: MulEquiv.trans, Nonempty.intro, MulEquiv.piCongrRight, MulEquiv.symm, MulEquiv.monoidHomCongrLeft
-- Module: Mathlib.GroupTheory.FiniteAbelian.Duality
Goal:
G : Type u_1
M : Type u_2
inst_1 : CommGroup G
inst_2 : Finite G
inst_3 : CommMonoid M
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
ι : Type
w : Fintype ι
n : ι → ℕ
h₁ : ∀ (i : ι), 1 < n i
h₂ : Nonempty.{u_1 + 1} (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ˣ
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 : ι) ↦ Nonempty.some ⋯
⊢ Nonempty (MonoidHom.{u_1, u_2} G Mˣ ≃* G)

Tactic:
exact ⟨e.monoidHomCongrLeft.trans <| e'.trans <| .trans (.piCongrRight E) e.symm⟩
-- 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)
classical :
  ∀ (ι : Type) (w : Fintype ι) (n : ι → ℕ) (h₁ : ∀ (i : ι), 1 < n i)
    (h₂ : Nonempty.{u_1 + 1} (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))), Nonempty (MonoidHom.{u_1, u_2} G Mˣ ≃* G)
classical₁ classical₂ :
  ∀ (ι : Type) (w : Fintype ι) (n : ι → ℕ) (h₁ : ∀ (i : ι), 1 < n i)
    (h₂ : Nonempty.{u_1 + 1} (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))), Nonempty (MonoidHom.{u_1, u_2} G Mˣ ≃* G)
classical₃ :
  ∀ (ι : Type) (w : Fintype ι) (n : ι → ℕ) (h₁ : ∀ (i : ι), 1 < n i)
    (h₂ : Nonempty.{u_1 + 1} (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))) (this : ∀ (i : ι), NeZero (n i)),
    Nonempty (MonoidHom.{u_1, u_2} G Mˣ ≃* G)
classical₄ classical₅ :
  ∀ (ι : Type) (w : Fintype ι) (n : ι → ℕ) (h₁ : ∀ (i : ι), 1 < n i)
    (h₂ : Nonempty.{u_1 + 1} (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))) (this : ∀ (i : ι), NeZero (n i))
    (inst_3 : ∀ (i : ι), HasEnoughRootsOfUnity M (Nat.card (Multiplicative (ZMod (n i))))),
    Nonempty (MonoidHom.{u_1, u_2} G Mˣ ≃* G)
⊢ Nonempty (MonoidHom.{u_1, u_2} G Mˣ ≃* G)

Tactic:
classical -- to get `DecidableEq ι`
  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ˣ
  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.monoidHomCongrLeft.trans <| e'.trans <| .trans (.piCongrRight E) e.symm⟩

Premises used: CommGroup.equiv_prod_multiplicative_zmod_of_finite
-- 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)
⊢ Nat.card (MonoidHom.{u_1, u_2} G Mˣ) = Nat.card G

Tactic:
Nat.card_congr (monoidHom_mulEquiv_of_hasEnoughRootsOfUnity G M).some.toEquiv

Premises used: CommGroup.monoidHom_mulEquiv_of_hasEnoughRootsOfUnity, Nonempty.some, MulEquiv.toEquiv, Nat.card_congr
-- 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
have :
  ∀ (this : Fintype ↥H),
    Function.Surjective (α := MonoidHom.{u_1, u_2} G Mˣ) (β := MonoidHom.{u_1, u_2} (↥H) Mˣ)
      (⇑(restrictHom H Mˣ) : (a : G →* Mˣ) → ↥H →* Mˣ)
⊢ Function.Surjective (α := MonoidHom.{u_1, u_2} G Mˣ) (β := MonoidHom.{u_1, u_2} (↥H) Mˣ)
    (⇑(restrictHom H Mˣ) : (a : G →* Mˣ) → ↥H →* Mˣ)

Tactic:
have : Fintype H := Fintype.ofFinite H
-- 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
this : Fintype ↥H
⊢ HasEnoughRootsOfUnity M (Monoid.exponent.{u_1} ↥H)

Tactic:
have : HasEnoughRootsOfUnity M (Monoid.exponent H) :=
    hM.of_dvd M <| Monoid.exponent_submonoid_dvd H.toSubmonoid
-- 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
this_1 : Fintype ↥H
this : HasEnoughRootsOfUnity M (Monoid.exponent.{u_1} ↥H)
⊢ HasEnoughRootsOfUnity M (Monoid.exponent.{u_1} (G ⧸ H))

Tactic:
have : HasEnoughRootsOfUnity M (Monoid.exponent (G ⧸ H)) :=
    hM.of_dvd M <| Group.exponent_quotient_dvd H
-- 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
this_1 : Fintype ↥H
this_2 : HasEnoughRootsOfUnity M (Monoid.exponent.{u_1} ↥H)
this : HasEnoughRootsOfUnity M (Monoid.exponent.{u_1} (G ⧸ H))
⊢ Function.Surjective (α := MonoidHom.{u_1, u_2} G Mˣ) (β := MonoidHom.{u_1, u_2} (↥H) Mˣ)
    (⇑(restrictHom H Mˣ) : (a : G →* Mˣ) → ↥H →* Mˣ)

Tactic:
MonoidHom.surjective_of_card_ker_le_div _ (le_of_eq ?_)

Premises used: le_of_eq, MonoidHom.surjective_of_card_ker_le_div
-- 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
this_1 : Fintype ↥H
this_2 : HasEnoughRootsOfUnity M (Monoid.exponent.{u_1} ↥H)
this : HasEnoughRootsOfUnity M (Monoid.exponent.{u_1} (G ⧸ H))
refine :
  Nat.card ↥(ker (M := MonoidHom.{u_1, u_2} (↥H) Mˣ) (restrictHom H Mˣ)) =
    Nat.card (MonoidHom.{u_1, u_2} G Mˣ) / Nat.card (MonoidHom.{u_1, u_2} (↥H) Mˣ)
⊢ Function.Surjective (α := MonoidHom.{u_1, u_2} G Mˣ) (β := MonoidHom.{u_1, u_2} (↥H) Mˣ)
    (⇑(restrictHom H Mˣ) : (a : G →* Mˣ) → ↥H →* Mˣ)

Tactic:
refine MonoidHom.surjective_of_card_ker_le_div _ (le_of_eq ?_)

Premises used: le_of_eq, MonoidHom.surjective_of_card_ker_le_div
-- 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
this_1 : Fintype ↥H
this_2 : HasEnoughRootsOfUnity M (Monoid.exponent.{u_1} ↥H)
this : HasEnoughRootsOfUnity M (Monoid.exponent.{u_1} (G ⧸ H))
rw :
  Nat.card ↥(ker (M := MonoidHom.{u_1, u_2} (↥H) Mˣ) (restrictHom H Mˣ)) =
    Nat.card G / Nat.card (MonoidHom.{u_1, u_2} (↥H) Mˣ)
rw₁ : Nat.card ↥(ker (M := MonoidHom.{u_1, u_2} (↥H) Mˣ) (restrictHom H Mˣ)) = Nat.card G / Nat.card.{u_1} ↥H
rw₂ :
  Nat.card ↥(ker (M := MonoidHom.{u_1, u_2} (↥H) Mˣ) (restrictHom H Mˣ)) =
    Nat.card.{u_1} (G ⧸ H) * Nat.card.{u_1} ↥H / Nat.card.{u_1} ↥H
rw₃ : Nat.card ↥(ker (M := MonoidHom.{u_1, u_2} (↥H) Mˣ) (restrictHom H Mˣ)) = Nat.card.{u_1} (G ⧸ H)
rw₄ :
  Nat.card ↥(ker (M := MonoidHom.{u_1, u_2} (↥H) Mˣ) (restrictHom H Mˣ)) = Nat.card (MonoidHom.{u_1, u_2} (G ⧸ H) Mˣ)
rw₅ rw₆ : Nat.card (MonoidHom.{u_1, u_2} (G ⧸ H) Mˣ) = Nat.card (MonoidHom.{u_1, u_2} (G ⧸ H) Mˣ)
⊢ Nat.card ↥(ker (M := MonoidHom.{u_1, u_2} (↥H) Mˣ) (restrictHom H Mˣ)) =
    Nat.card (MonoidHom.{u_1, u_2} G Mˣ) / Nat.card (MonoidHom.{u_1, u_2} (↥H) Mˣ)

Tactic:
rw [card_monoidHom_of_hasEnoughRootsOfUnity, card_monoidHom_of_hasEnoughRootsOfUnity,
    H.card_eq_card_quotient_mul_card_subgroup,
    mul_div_cancel_right₀ _ (Fintype.card_eq_nat_card ▸ Fintype.card_ne_zero),
    ← card_monoidHom_of_hasEnoughRootsOfUnity (G ⧸ H) M,
    Nat.card_congr (restrictHomKerEquiv Mˣ H).toEquiv]

Premises used: Subgroup.card_eq_card_quotient_mul_card_subgroup, CommGroup.card_monoidHom_of_hasEnoughRootsOfUnity, Units, MulEquiv.toEquiv, mul_div_cancel_right₀, HasQuotient.Quotient, MonoidHom.restrictHomKerEquiv, Nat.card_congr
-- 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
⊢ HasEnoughRootsOfUnity M (Monoid.exponent.{u_1} (G ⧸ H))

Tactic:
have : HasEnoughRootsOfUnity M (Monoid.exponent (G ⧸ H)) :=
    hM.of_dvd M <| Group.exponent_quotient_dvd H
-- 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
this : HasEnoughRootsOfUnity M (Monoid.exponent.{u_1} (G ⧸ H))
⊢ (∀ (φ : MonoidHom.{u_1, u_2} G Mˣ),
      (∀ y ∈ H, Eq.{u_2 + 1} (α := Mˣ) ((φ : (a : G) → Mˣ) y : Mˣ) (1 : Mˣ)) →
        Eq.{u_2 + 1} (α := Mˣ) ((φ : (a : G) → Mˣ) x : Mˣ) (1 : Mˣ)) ↔
    x ∈ H

Tactic:
⟨fun h ↦ ?_, fun hx φ hφ ↦ hφ x hx⟩

Premises used: Iff.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)
H : Subgroup G
x : G
this : HasEnoughRootsOfUnity M (Monoid.exponent.{u_1} (G ⧸ H))
refine :
  ∀
    (h :
      ∀ (φ : MonoidHom.{u_1, u_2} G Mˣ),
        (∀ y ∈ H, Eq.{u_2 + 1} (α := Mˣ) ((φ : (a : G) → Mˣ) y : Mˣ) (1 : Mˣ)) →
          Eq.{u_2 + 1} (α := Mˣ) ((φ : (a : G) → Mˣ) x : Mˣ) (1 : Mˣ)),
    x ∈ H
⊢ (∀ (φ : MonoidHom.{u_1, u_2} G Mˣ),
      (∀ y ∈ H, Eq.{u_2 + 1} (α := Mˣ) ((φ : (a : G) → Mˣ) y : Mˣ) (1 : Mˣ)) →
        Eq.{u_2 + 1} (α := Mˣ) ((φ : (a : G) → Mˣ) x : Mˣ) (1 : Mˣ)) ↔
    x ∈ H

Tactic:
refine ⟨fun h ↦ ?_, fun hx φ hφ ↦ hφ x hx⟩
-- 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
this : HasEnoughRootsOfUnity M (Monoid.exponent.{u_1} (G ⧸ H))
h :
  ∀ (φ : MonoidHom.{u_1, u_2} G Mˣ),
    (∀ y ∈ H, Eq.{u_2 + 1} (α := Mˣ) ((φ : (a : G) → Mˣ) y : Mˣ) (1 : Mˣ)) →
      Eq.{u_2 + 1} (α := Mˣ) ((φ : (a : G) → Mˣ) x : Mˣ) (1 : Mˣ)
simp :
  ∀
    (h :
      ∀ (φ : MonoidHom.{u_1, u_2} G Mˣ),
        (∀ (y : G),
            (∀ (φ : MonoidHom.{u_1, u_2} (G ⧸ H) Mˣ),
                Eq.{u_2 + 1} (α := Mˣ) ((φ : (a : G ⧸ H) → Mˣ) (↑y : G ⧸ H) : Mˣ) (1 : Mˣ)) →
              Eq.{u_2 + 1} (α := Mˣ) ((φ : (a : G) → Mˣ) y : Mˣ) (1 : Mˣ)) →
          Eq.{u_2 + 1} (α := Mˣ) ((φ : (a : G) → Mˣ) x : Mˣ) (1 : Mˣ))
    (φ : MonoidHom.{u_1, u_2} (G ⧸ H) Mˣ), Eq.{u_2 + 1} (α := Mˣ) ((φ : (a : G ⧸ H) → Mˣ) (↑x : G ⧸ H) : Mˣ) (1 : Mˣ)
⊢ x ∈ H

Tactic:
simp only [← QuotientGroup.eq_one_iff, ← forall_apply_eq_apply_iff _ (M := M), map_one] at h ⊢

Premises used: map_one, CommGroup.forall_apply_eq_apply_iff, QuotientGroup.eq_one_iff
-- 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
this : HasEnoughRootsOfUnity M (Monoid.exponent.{u_1} (G ⧸ H))
h :
  ∀ (φ : MonoidHom.{u_1, u_2} G Mˣ),
    (∀ (y : G),
        (∀ (φ : MonoidHom.{u_1, u_2} (G ⧸ H) Mˣ),
            Eq.{u_2 + 1} (α := Mˣ) ((φ : (a : G ⧸ H) → Mˣ) (↑y : G ⧸ H) : Mˣ) (1 : Mˣ)) →
          Eq.{u_2 + 1} (α := Mˣ) ((φ : (a : G) → Mˣ) y : Mˣ) (1 : Mˣ)) →
      Eq.{u_2 + 1} (α := Mˣ) ((φ : (a : G) → Mˣ) x : Mˣ) (1 : Mˣ)
⊢ ∀ (φ : MonoidHom.{u_1, u_2} (G ⧸ H) Mˣ), Eq.{u_2 + 1} (α := Mˣ) ((φ : (a : G ⧸ H) → Mˣ) (↑x : G ⧸ H) : Mˣ) (1 : Mˣ)

Tactic:
fun φ ↦ h (φ.comp (QuotientGroup.mk' H)) fun y hy ↦ hy φ

Premises used: MonoidHom.comp, QuotientGroup.mk'
-- 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
this : HasEnoughRootsOfUnity M (Monoid.exponent.{u_1} (G ⧸ H))
h :
  ∀ (φ : MonoidHom.{u_1, u_2} G Mˣ),
    (∀ (y : G),
        (∀ (φ : MonoidHom.{u_1, u_2} (G ⧸ H) Mˣ),
            Eq.{u_2 + 1} (α := Mˣ) ((φ : (a : G ⧸ H) → Mˣ) (↑y : G ⧸ H) : Mˣ) (1 : Mˣ)) →
          Eq.{u_2 + 1} (α := Mˣ) ((φ : (a : G) → Mˣ) y : Mˣ) (1 : Mˣ)) →
      Eq.{u_2 + 1} (α := Mˣ) ((φ : (a : G) → Mˣ) x : Mˣ) (1 : Mˣ)
⊢ ∀ (φ : MonoidHom.{u_1, u_2} (G ⧸ H) Mˣ), Eq.{u_2 + 1} (α := Mˣ) ((φ : (a : G ⧸ H) → Mˣ) (↑x : G ⧸ H) : Mˣ) (1 : Mˣ)

Tactic:
exact fun φ ↦ h (φ.comp (QuotientGroup.mk' H)) fun y hy ↦ hy φ
-- 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
⊢ HasEnoughRootsOfUnity M (Monoid.exponent.{u_1} (G ⧸ H))

Tactic:
have : HasEnoughRootsOfUnity M (Monoid.exponent (G ⧸ H)) :=
    hM.of_dvd M <| Group.exponent_quotient_dvd H
-- 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
this : HasEnoughRootsOfUnity M (Monoid.exponent.{u_1} (G ⧸ H))
rw : Nat.card (MonoidHom.{u_1, u_2} (G ⧸ H) Mˣ) = Nat.card.{u_1} (G ⧸ H)
rw₁ rw₂ : Nat.card.{u_1} (G ⧸ H) = Nat.card.{u_1} (G ⧸ H)
⊢ Nat.card ↥(ker (M := MonoidHom.{u_1, u_2} (↥H) Mˣ) (restrictHom H Mˣ)) = Nat.card.{u_1} (G ⧸ H)

Tactic:
rw [Nat.card_congr (MonoidHom.restrictHomKerEquiv Mˣ H).toEquiv,
    card_monoidHom_of_hasEnoughRootsOfUnity]

Premises used: CommGroup.card_monoidHom_of_hasEnoughRootsOfUnity, Units, MulEquiv.toEquiv, MonoidHom.restrictHomKerEquiv, Nat.card_congr