awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Duality (hypothesis)
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))))
have hdvd : 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
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Duality (hypothesis)
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)
⊢ Nonempty (MonoidHom.{u_1, u_2} G Mˣ ≃* G)
have inst : ∀ (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
-- 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)
⊢ Nonempty (MonoidHom.{u_1, u_2} G Mˣ ≃* G)
have 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)
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⟩
-- 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)
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)
⊢ Nonempty (MonoidHom.{u_1, u_2} G Mˣ ≃* G)
have 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)
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⟩
-- 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)
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)
⊢ Nonempty (MonoidHom.{u_1, u_2} G Mˣ ≃* G)
have 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)
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⟩
-- 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
⊢ Function.Surjective (α := MonoidHom.{u_1, u_2} G Mˣ) (β := MonoidHom.{u_1, u_2} (↥H) Mˣ)
    (⇑(restrictHom H Mˣ) : (a : G →* Mˣ) → ↥H →* Mˣ)
have 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ˣ)
Tactic: have : Fintype H := Fintype.ofFinite H
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Duality (hypothesis)
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
⊢ Function.Surjective (α := MonoidHom.{u_1, u_2} G Mˣ) (β := MonoidHom.{u_1, u_2} (↥H) Mˣ)
    (⇑(restrictHom H Mˣ) : (a : G →* Mˣ) → ↥H →* Mˣ)
have this₁ : HasEnoughRootsOfUnity M (Monoid.exponent.{u_1} ↥H)
Tactic: have : HasEnoughRootsOfUnity M (Monoid.exponent H) :=
    hM.of_dvd M <| Monoid.exponent_submonoid_dvd H.toSubmonoid
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Duality (hypothesis)
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)
⊢ Function.Surjective (α := MonoidHom.{u_1, u_2} G Mˣ) (β := MonoidHom.{u_1, u_2} (↥H) Mˣ)
    (⇑(restrictHom H Mˣ) : (a : G →* Mˣ) → ↥H →* Mˣ)
have this₁ : 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
-- 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
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ˣ)
have 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ˣ)
Tactic: refine MonoidHom.surjective_of_card_ker_le_div _ (le_of_eq ?_)
-- 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
this_1 : Fintype ↥H
this_2 : HasEnoughRootsOfUnity M (Monoid.exponent.{u_1} ↥H)
this : HasEnoughRootsOfUnity M (Monoid.exponent.{u_1} (G ⧸ H))
⊢ 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ˣ)
have 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ˣ)
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]
-- 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
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ˣ)
⊢ 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ˣ)
have rw₁ : Nat.card ↥(ker (M := MonoidHom.{u_1, u_2} (↥H) Mˣ) (restrictHom H Mˣ)) = Nat.card G / Nat.card.{u_1} ↥H
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]
-- 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
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
⊢ 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ˣ)
have 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
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]
-- 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
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
⊢ 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ˣ)
have rw₃ : Nat.card ↥(ker (M := MonoidHom.{u_1, u_2} (↥H) Mˣ) (restrictHom H Mˣ)) = Nat.card.{u_1} (G ⧸ H)
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]
-- 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
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)
⊢ 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ˣ)
have 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ˣ)
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]
-- 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
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ˣ)
⊢ 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ˣ)
have rw₅ : Nat.card (MonoidHom.{u_1, u_2} (G ⧸ H) Mˣ) = Nat.card (MonoidHom.{u_1, u_2} (G ⧸ 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]
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Duality (hypothesis)
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
⊢ (∀ (φ : 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
have this : 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
-- 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
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
have 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
Tactic: refine ⟨fun h ↦ ?_, fun hx φ hφ ↦ hφ x hx⟩
-- 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
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ˣ)
⊢ x ∈ H
have 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ˣ)
Tactic: simp only [← QuotientGroup.eq_one_iff, ← forall_apply_eq_apply_iff _ (M := M), map_one] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Duality (hypothesis)
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
⊢ Nat.card ↥(ker (M := MonoidHom.{u_1, u_2} (↥H) Mˣ) (restrictHom H Mˣ)) = Nat.card.{u_1} (G ⧸ H)
have this : 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
-- 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
this : HasEnoughRootsOfUnity M (Monoid.exponent.{u_1} (G ⧸ H))
⊢ Nat.card ↥(ker (M := MonoidHom.{u_1, u_2} (↥H) Mˣ) (restrictHom H Mˣ)) = Nat.card.{u_1} (G ⧸ H)
have rw : Nat.card (MonoidHom.{u_1, u_2} (G ⧸ H) Mˣ) = Nat.card.{u_1} (G ⧸ H)
Tactic: rw [Nat.card_congr (MonoidHom.restrictHomKerEquiv Mˣ H).toEquiv,
    card_monoidHom_of_hasEnoughRootsOfUnity]
-- 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
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)
⊢ Nat.card ↥(ker (M := MonoidHom.{u_1, u_2} (↥H) Mˣ) (restrictHom H Mˣ)) = Nat.card.{u_1} (G ⧸ H)
have rw₁ : Nat.card.{u_1} (G ⧸ H) = Nat.card.{u_1} (G ⧸ H)
Tactic: rw [Nat.card_congr (MonoidHom.restrictHomKerEquiv Mˣ H).toEquiv,
    card_monoidHom_of_hasEnoughRootsOfUnity]
-- 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)
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' := ⋯ }
have 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' := sorry, map_mul' := sorry } :
            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' := sorry, map_mul' := sorry } :
            MonoidHom.{u_1, u_2} G Mˣ →* Mˣ))
        x_1)),
  x = x_1
Tactic: refine (Nat.bijective_iff_injective_and_card _).mpr ⟨fun _ _ h ↦ ?_, ?_⟩
-- 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)
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
⊢ 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' := ⋯ }
have refine_2 : Nat.card G = Nat.card (MonoidHom.{u_1, u_2} G Mˣ →* Mˣ)
Tactic: refine (Nat.bijective_iff_injective_and_card _).mpr ⟨fun _ _ h ↦ ?_, ?_⟩