awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Basic (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
inst_1 : Finite G
ι : Type
hι : Fintype ι
p : ι → ℕ
hp : ∀ (i : ι), Nat.Prime (p i)
n : ι → ℕ
e : G ≃+ ⨁ (i : ι), ZMod (p i ^ n i)
⊢ ∃ (ι : Type) (x : Fintype ι) (n : ι → ℕ),
    (∀ (i : ι), 1 < n i) ∧ Nonempty.{max 1 (u_1 + 1)} (G ≃+ ⨁ (i : ι), ZMod (n i))
have refine : ∀ (i : { i : ι // n i ≠ 0 }), LT.lt (α := ℕ) 1 ((fun (i : { i : ι // n i ≠ 0 }) ↦ p (↑i : ι) ^ n (↑i : ι)) i)
Tactic: refine ⟨{i : ι // n i ≠ 0}, inferInstance, fun i ↦ p i ^ n i, ?_,
    ⟨e.trans (directSumNeZeroMulEquiv ι _ _).symm⟩⟩
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Basic (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
inst_1 : Finite G
⊢ ∃ (ι : Type) (x : Fintype ι) (n : ι → ℕ),
    (∀ (i : ι), 1 < n i) ∧ Nonempty.{max 1 (u_1 + 1)} (G ≃+ ⨁ (i : ι), ZMod (n i))
have obtain : ∀ (ι : Type) (hι : Fintype ι) (p : ι → ℕ) (hp : ∀ (i : ι), Nat.Prime (p i)) (n : ι → ℕ)
  (e : G ≃+ ⨁ (i : ι), ZMod (p i ^ n i)),
  ∃ (ι : Type) (x : Fintype ι) (n : ι → ℕ),
    (∀ (i : ι), 1 < n i) ∧ Nonempty.{max 1 (u_1 + 1)} (G ≃+ ⨁ (i : ι), ZMod (n i))
Tactic: classical
  obtain ⟨ι, hι, p, hp, n, ⟨e⟩⟩ := AddCommGroup.equiv_directSum_zmod_of_finite G
  refine ⟨{i : ι // n i ≠ 0}, inferInstance, fun i ↦ p i ^ n i, ?_,
    ⟨e.trans (directSumNeZeroMulEquiv ι _ _).symm⟩⟩
  rintro ⟨i, hi⟩
  exact one_lt_pow₀ (hp _).one_lt hi
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Basic (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
inst_1 : Finite G
obtain :
  ∀ (ι : Type) (hι : Fintype ι) (p : ι → ℕ) (hp : ∀ (i : ι), Nat.Prime (p i)) (n : ι → ℕ)
    (e : G ≃+ ⨁ (i : ι), ZMod (p i ^ n i)),
    ∃ (ι : Type) (x : Fintype ι) (n : ι → ℕ),
      (∀ (i : ι), 1 < n i) ∧ Nonempty.{max 1 (u_1 + 1)} (G ≃+ ⨁ (i : ι), ZMod (n i))
⊢ ∃ (ι : Type) (x : Fintype ι) (n : ι → ℕ),
    (∀ (i : ι), 1 < n i) ∧ Nonempty.{max 1 (u_1 + 1)} (G ≃+ ⨁ (i : ι), ZMod (n i))
have obtain₁ : ∀ (ι : Type) (hι : Fintype ι) (p : ι → ℕ) (hp : ∀ (i : ι), Nat.Prime (p i)) (n : ι → ℕ)
  (e : G ≃+ ⨁ (i : ι), ZMod (p i ^ n i)) (i : { i : ι // n i ≠ 0 }),
  LT.lt (α := ℕ) 1 ((fun (i : { i : ι // n i ≠ 0 }) ↦ p (↑i : ι) ^ n (↑i : ι)) i)
Tactic: classical
  obtain ⟨ι, hι, p, hp, n, ⟨e⟩⟩ := AddCommGroup.equiv_directSum_zmod_of_finite G
  refine ⟨{i : ι // n i ≠ 0}, inferInstance, fun i ↦ p i ^ n i, ?_,
    ⟨e.trans (directSumNeZeroMulEquiv ι _ _).symm⟩⟩
  rintro ⟨i, hi⟩
  exact one_lt_pow₀ (hp _).one_lt hi
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Basic (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
inst_1 : Finite G
obtain :
  ∀ (ι : Type) (hι : Fintype ι) (p : ι → ℕ) (hp : ∀ (i : ι), Nat.Prime (p i)) (n : ι → ℕ)
    (e : G ≃+ ⨁ (i : ι), ZMod (p i ^ n i)),
    ∃ (ι : Type) (x : Fintype ι) (n : ι → ℕ),
      (∀ (i : ι), 1 < n i) ∧ Nonempty.{max 1 (u_1 + 1)} (G ≃+ ⨁ (i : ι), ZMod (n i))
obtain₁ :
  ∀ (ι : Type) (hι : Fintype ι) (p : ι → ℕ) (hp : ∀ (i : ι), Nat.Prime (p i)) (n : ι → ℕ)
    (e : G ≃+ ⨁ (i : ι), ZMod (p i ^ n i)) (i : { i : ι // n i ≠ 0 }),
    LT.lt (α := ℕ) 1 ((fun (i : { i : ι // n i ≠ 0 }) ↦ p (↑i : ι) ^ n (↑i : ι)) i)
⊢ ∃ (ι : Type) (x : Fintype ι) (n : ι → ℕ),
    (∀ (i : ι), 1 < n i) ∧ Nonempty.{max 1 (u_1 + 1)} (G ≃+ ⨁ (i : ι), ZMod (n i))
have obtain₂ : ∀ (ι : Type) (hι : Fintype ι) (p : ι → ℕ) (hp : ∀ (i : ι), Nat.Prime (p i)) (n : ι → ℕ)
  (e : G ≃+ ⨁ (i : ι), ZMod (p i ^ n i)) (i : ι) (hi : n i ≠ 0),
  LT.lt (α := ℕ) 1
    ((fun (i : { i : ι // n i ≠ 0 }) ↦ p (↑i : ι) ^ n (↑i : ι)) (Subtype.mk (p := fun (i : ι) ↦ n i ≠ 0) i hi))
Tactic: classical
  obtain ⟨ι, hι, p, hp, n, ⟨e⟩⟩ := AddCommGroup.equiv_directSum_zmod_of_finite G
  refine ⟨{i : ι // n i ≠ 0}, inferInstance, fun i ↦ p i ^ n i, ?_,
    ⟨e.trans (directSumNeZeroMulEquiv ι _ _).symm⟩⟩
  rintro ⟨i, hi⟩
  exact one_lt_pow₀ (hp _).one_lt hi
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Basic (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : Finite G
⊢ ∃ (ι : Type) (x : Fintype ι) (n : ι → ℕ),
    (∀ (i : ι), 1 < n i) ∧ Nonempty.{max 1 (u_1 + 1)} (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))
have obtain : ∀ (ι : Type) (inst_2 : Fintype ι) (n : ι → ℕ) (h₁ : ∀ (i : ι), 1 < n i)
  (h₂ : Nonempty.{u_1 + 1} (Additive G ≃+ ⨁ (i : ι), ZMod (n i))),
  ∃ (ι : Type) (x : Fintype ι) (n : ι → ℕ),
    (∀ (i : ι), 1 < n i) ∧ Nonempty.{max 1 (u_1 + 1)} (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))
Tactic: obtain ⟨ι, inst, n, h₁, h₂⟩ := AddCommGroup.equiv_directSum_zmod_of_finite' (Additive G)
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Basic (goal)
Goal:
G : Type u_1
inst : CommGroup G
hG : Group.FG G
⊢ ∃ (ι : Type) (j : Type) (x : Fintype ι) (x : Fintype j) (p : ι → ℕ) (_ : ∀ (i : ι), Nat.Prime (p i)) (e : ι → ℕ),
    Nonempty.{max 1 (u_1 + 1)} (G ≃* (j → Multiplicative ℤ) × ((i : ι) → Multiplicative (ZMod (p i ^ e i))))
have obtain : ∀ (n : ℕ) (ι : Type) (inst_1 : Fintype ι) (x : ι → ℕ) (p : ∀ (i : ι), Nat.Prime (x i)) (e : ι → ℕ)
  (equiv : Nonempty.{u_1 + 1} (Additive G ≃+ (Fin n →₀ ℤ) × ⨁ (i : ι), ZMod (x i ^ e i))),
  ∃ (ι : Type) (j : Type) (x : Fintype ι) (x : Fintype j) (p : ι → ℕ) (_ : ∀ (i : ι), Nat.Prime (p i)) (e : ι → ℕ),
    Nonempty.{max 1 (u_1 + 1)} (G ≃* (j → Multiplicative ℤ) × ((i : ι) → Multiplicative (ZMod (p i ^ e i))))
Tactic: obtain ⟨n, ι, inst, x, p, e, equiv⟩ := AddCommGroup.equiv_free_prod_directSum_zmod (Additive G)
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Basic (goal)
Goal:
A : Type u_1
inst : CommGroup A
B : Subgroup A
hB : B.FG
n : ℕ
hn : n ≠ 0
⊢ IsFiniteRelIndex (map (powMonoidHom n) B) B
have rw : (subgroupOf (map (powMonoidHom n) B) B).FiniteIndex
Tactic: rw [isFiniteRelIndex_iff_finiteIndex]
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Basic (goal)
Goal:
A : Type u_1
inst : CommGroup A
B : Subgroup A
hB : B.FG
n : ℕ
hn : n ≠ 0
⊢ subgroupOf (map (powMonoidHom n) B) B = MonoidHom.range (powMonoidHom n)
have h : ∀ (x : ↥B),
  x ∈ subgroupOf (map (powMonoidHom n) B) B ↔ Membership.mem (γ := Subgroup ↥B) (MonoidHom.range (powMonoidHom n)) x
Tactic: ext1
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Basic (hypothesis)
Goal:
A : Type u_1
inst : CommGroup A
B : Subgroup A
hB : B.FG
n : ℕ
hn : n ≠ 0
⊢ (subgroupOf (map (powMonoidHom n) B) B).FiniteIndex
have this : subgroupOf (map (powMonoidHom n) B) B = MonoidHom.range (powMonoidHom n)
Tactic: have : (map (powMonoidHom (α := A) n) B).subgroupOf B = (powMonoidHom (α := B) n).range := by
    ext1
    simp [mem_subgroupOf, Subtype.ext_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Basic (goal)
Goal:
A : Type u_1
inst : CommGroup A
B : Subgroup A
hB : B.FG
n : ℕ
hn : n ≠ 0
this : subgroupOf (map (powMonoidHom n) B) B = MonoidHom.range (powMonoidHom n)
⊢ (subgroupOf (map (powMonoidHom n) B) B).FiniteIndex
have rw : FiniteIndex.{u_1} (G := ↥B) (MonoidHom.range (powMonoidHom n))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Basic (hypothesis)
Goal:
A : Type u_1
inst : CommGroup A
B : Subgroup A
hB : B.FG
n : ℕ
hn : n ≠ 0
this : subgroupOf (map (powMonoidHom n) B) B = MonoidHom.range (powMonoidHom n)
⊢ FiniteIndex.{u_1} (G := ↥B) (MonoidHom.range (powMonoidHom n))
have this₁ : Group.FG.{u_1} ↥B
Tactic: have := (Group.fg_iff_subgroup_fg B).mpr hB
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Basic (goal)
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : Module.Finite ℤ R
inst_2 : AddCommGroup M
inst_3 : Module R M
A : Submodule R M
hfg : A.FG
⊢ A.toAddSubgroup.FG
have rw : FG.{0, u_3} (R := ℤ) (M := M) ((AddSubgroup.toIntSubmodule : (a : AddSubgroup M) → Submodule ℤ M) A.toAddSubgroup)
Tactic: rw [← AddSubgroup.toIntSubmodule_toAddSubgroup A.toAddSubgroup, ← fg_iff_addSubgroup_fg]
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Basic (hypothesis)
Goal:
R : Type u_1
K : Type u_2
inst : CommRing R
inst_1 : CommRing K
inst_2 : Algebra R K
inst_3 : Module.Finite ℤ R
A B : Submodule R K
n : ℕ
hn : n ≠ 0
hfg : A.FG
h : map (LinearMap.mulLeft R (↑n : K)) A ≤ B
⊢ IsFiniteRelIndex.{u_2} (G := K) B.toAddSubgroup A.toAddSubgroup
have this : AddSubgroup.FG.{u_2} (G := K) A.toAddSubgroup
Tactic: have := fg_toAddSubgroup hfg
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Basic (hypothesis)
Goal:
R : Type u_1
K : Type u_2
inst : CommRing R
inst_1 : CommRing K
inst_2 : Algebra R K
inst_3 : Module.Finite ℤ R
A B : Submodule R K
n : ℕ
hn : n ≠ 0
hfg : A.FG
h : map (LinearMap.mulLeft R (↑n : K)) A ≤ B
this : AddSubgroup.FG.{u_2} (G := K) A.toAddSubgroup
⊢ IsFiniteRelIndex.{u_2} (G := K) B.toAddSubgroup A.toAddSubgroup
have this₁ : IsFiniteRelIndex.{u_2} (G := K) (AddSubgroup.map (G := K) (nsmulAddMonoidHom n) A.toAddSubgroup) A.toAddSubgroup
Tactic: have := isFiniteRelIndex_map_nsmulAddMonoidHom_of_fg this hn
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Basic (goal)
Goal:
R : Type u_1
K : Type u_2
inst : CommRing R
inst_1 : CommRing K
inst_2 : Algebra R K
inst_3 : Module.Finite ℤ R
A B : Submodule R K
n : ℕ
hn : n ≠ 0
hfg : A.FG
h : map (LinearMap.mulLeft R (↑n : K)) A ≤ B
this_1 : AddSubgroup.FG.{u_2} (G := K) A.toAddSubgroup
this : IsFiniteRelIndex.{u_2} (G := K) (AddSubgroup.map (G := K) (nsmulAddMonoidHom n) A.toAddSubgroup) A.toAddSubgroup
⊢ IsFiniteRelIndex.{u_2} (G := K) B.toAddSubgroup A.toAddSubgroup
have refine : LE.le.{u_2} (α := AddSubgroup K) (AddSubgroup.map (G := K) (nsmulAddMonoidHom n) A.toAddSubgroup) B.toAddSubgroup
Tactic: refine isFiniteRelIndex_of_le_left (H := A.toAddSubgroup.map (nsmulAddMonoidHom n))
    A.toAddSubgroup ?_
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Basic (hypothesis)
Goal:
R : Type u_1
K : Type u_2
inst : CommRing R
inst_1 : CommRing K
inst_2 : Algebra R K
inst_3 : Module.Finite ℤ R
A B : Submodule R K
n : ℕ
hn : n ≠ 0
hfg : A.FG
h : map (LinearMap.mulLeft R (↑n : K)) A ≤ B
this_1 : AddSubgroup.FG.{u_2} (G := K) A.toAddSubgroup
this : IsFiniteRelIndex.{u_2} (G := K) (AddSubgroup.map (G := K) (nsmulAddMonoidHom n) A.toAddSubgroup) A.toAddSubgroup
⊢ LE.le.{u_2} (α := AddSubgroup K) (AddSubgroup.map (G := K) (nsmulAddMonoidHom n) A.toAddSubgroup) B.toAddSubgroup
have h₁ : ∀ ⦃x : K⦄, x ∈ map (LinearMap.mulLeft R (↑n : K)) A → x ∈ B
Tactic: rw [SetLike.le_def] at h ⊢
Cleared hypotheses: h, this_1, this
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Duality (hypothesis)
Goal:
ι : Type u_1
G : Type u_2
inst : Finite ι
inst_1 : Monoid G
n : ι → ℕ
e : MulEquiv.{u_2, u_1} G ((i : ι) → Multiplicative (ZMod (n i)))
i : ι
⊢ n i ∣ Monoid.exponent G
have this : n i =
  orderOf.{u_2} (G := G)
    ((e.symm : (a : (i : ι) → Multiplicative (ZMod (n i))) → G)
        (Pi.mulSingle (M := fun (i : ι) ↦ Multiplicative (ZMod (n i))) i
          ((Multiplicative.ofAdd : (a : ZMod (n i)) → Multiplicative (ZMod (n i))) 1)) :
      G)
Tactic: have : n i = orderOf (e.symm <| Pi.mulSingle i <| .ofAdd 1) := by
    simpa only [MulEquiv.orderOf_eq, orderOf_piMulSingle, orderOf_ofAdd_eq_addOrderOf]
      using (ZMod.addOrderOf_one (n i)).symm
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Duality (goal)
Goal:
ι : Type u_1
G : Type u_2
inst : Finite ι
inst_1 : Monoid G
n : ι → ℕ
e : MulEquiv.{u_2, u_1} G ((i : ι) → Multiplicative (ZMod (n i)))
i : ι
⊢ n i ∣ Monoid.exponent G
have classical : n i =
  orderOf.{u_2} (G := G)
    ((e.symm : (a : (i : ι) → Multiplicative (ZMod (n i))) → G)
        (Pi.mulSingle (M := fun (i : ι) ↦ Multiplicative (ZMod (n i))) i
          ((Multiplicative.ofAdd : (a : ZMod (n i)) → Multiplicative (ZMod (n i))) 1)) :
      G)
Tactic: classical -- to get `DecidableEq ι`
  have : n i = orderOf (e.symm <| Pi.mulSingle i <| .ofAdd 1) := by
    simpa only [MulEquiv.orderOf_eq, orderOf_piMulSingle, orderOf_ofAdd_eq_addOrderOf]
      using (ZMod.addOrderOf_one (n i)).symm
  exact this ▸ Monoid.order_dvd_exponent _
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Duality (goal)
Goal:
ι : Type u_1
G : Type u_2
inst : Finite ι
inst_1 : Monoid G
n : ι → ℕ
e : MulEquiv.{u_2, u_1} G ((i : ι) → Multiplicative (ZMod (n i)))
i : ι
classical :
  n i =
    orderOf.{u_2} (G := G)
      ((e.symm : (a : (i : ι) → Multiplicative (ZMod (n i))) → G)
          (Pi.mulSingle (M := fun (i : ι) ↦ Multiplicative (ZMod (n i))) i
            ((Multiplicative.ofAdd : (a : ZMod (n i)) → Multiplicative (ZMod (n i))) 1)) :
        G)
⊢ n i ∣ Monoid.exponent G
have classical₁ : ∀
  (this :
    n i =
      orderOf.{u_2} (G := G)
        ((e.symm : (a : (i : ι) → Multiplicative (ZMod (n i))) → G)
            (Pi.mulSingle (M := fun (i : ι) ↦ Multiplicative (ZMod (n i))) i
              ((Multiplicative.ofAdd : (a : ZMod (n i)) → Multiplicative (ZMod (n i))) 1)) :
          G)),
  n i ∣ Monoid.exponent G
Tactic: classical -- to get `DecidableEq ι`
  have : n i = orderOf (e.symm <| Pi.mulSingle i <| .ofAdd 1) := by
    simpa only [MulEquiv.orderOf_eq, orderOf_piMulSingle, orderOf_ofAdd_eq_addOrderOf]
      using (ZMod.addOrderOf_one (n i)).symm
  exact this ▸ Monoid.order_dvd_exponent _
-- 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
H :
  ∀ (n : ℕ),
    n ∣ Monoid.exponent G →
      ∀ (a : ZMod n),
        a ≠ 0 →
          ∃ (φ : 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)
a : G
ha : a ≠ 1
⊢ ∃ (φ : G →* M), Ne.{u_2 + 1} (α := M) ((φ : (a : G) → M) a : M) (1 : M)
have obtain : ∀ (ι : Type) (w : Fintype ι) (n : ι → ℕ),
  (∀ (i : ι), 1 < n i) →
    ∀ (h : Nonempty.{u_1 + 1} (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))),
      ∃ (φ : G →* M), Ne.{u_2 + 1} (α := M) ((φ : (a : G) → M) a : M) (1 : M)
Tactic: obtain ⟨ι, _, n, _, h⟩ := CommGroup.equiv_prod_multiplicative_zmod_of_finite G
-- 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
H :
  ∀ (n : ℕ),
    n ∣ Monoid.exponent G →
      ∀ (a : ZMod n),
        a ≠ 0 →
          ∃ (φ : 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)
a : G
ha : a ≠ 1
ι : Type
w : Fintype ι
n : ι → ℕ
left : ∀ (i : ι), 1 < n i
h : Nonempty.{u_1 + 1} (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))
e : G ≃* ((i : ι) → Multiplicative (ZMod (n i))) := h.some
⊢ ∃ (i : ι),
    Ne (α := Multiplicative (ZMod (n i)))
      ((e : (a : G) → (i : ι) → Multiplicative (ZMod (n i))) a i : Multiplicative (ZMod (n i)))
      (1 : Multiplicative (ZMod (n i)))
have contrapose! : ∀
  (ha :
    ∀ (i : ι),
      Eq (α := Multiplicative (ZMod (n i)))
        ((e : (a : G) → (i : ι) → Multiplicative (ZMod (n i))) a i : Multiplicative (ZMod (n i)))
        (1 : Multiplicative (ZMod (n i)))),
  a = 1
Tactic: contrapose! ha
Cleared hypotheses: ha
-- 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
H :
  ∀ (n : ℕ),
    n ∣ Monoid.exponent G →
      ∀ (a : ZMod n),
        a ≠ 0 →
          ∃ (φ : 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)
a : G
ha : a ≠ 1
ι : Type
w : Fintype ι
n : ι → ℕ
left : ∀ (i : ι), 1 < n i
h : Nonempty.{u_1 + 1} (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))
e : G ≃* ((i : ι) → Multiplicative (ZMod (n i))) := h.some
⊢ ∃ (φ : G →* M), Ne.{u_2 + 1} (α := M) ((φ : (a : G) → M) a : M) (1 : M)
have obtain : ∀ (i : ι)
  (hi :
    Ne (α := Multiplicative (ZMod (n i)))
      ((e : (a : G) → (i : ι) → Multiplicative (ZMod (n i))) a i : Multiplicative (ZMod (n i)))
      (1 : Multiplicative (ZMod (n i)))),
  ∃ (φ : G →* M), Ne.{u_2 + 1} (α := M) ((φ : (a : G) → M) a : M) (1 : M)
Tactic: obtain ⟨i, hi⟩ : ∃ i : ι, e a i ≠ 1 := by
    contrapose! ha
    exact (MulEquiv.map_eq_one_iff e).mp <| funext ha
-- 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
H :
  ∀ (n : ℕ),
    n ∣ Monoid.exponent G →
      ∀ (a : ZMod n),
        a ≠ 0 →
          ∃ (φ : 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)
a : G
ha : a ≠ 1
ι : Type
w : Fintype ι
n : ι → ℕ
left : ∀ (i : ι), 1 < n i
h : Nonempty.{u_1 + 1} (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))
e : G ≃* ((i : ι) → Multiplicative (ZMod (n i))) := h.some
i : ι
hi :
  Ne (α := Multiplicative (ZMod (n i)))
    ((e : (a : G) → (i : ι) → Multiplicative (ZMod (n i))) a i : Multiplicative (ZMod (n i)))
    (1 : Multiplicative (ZMod (n i)))
⊢ ∃ (φ : G →* M), Ne.{u_2 + 1} (α := M) ((φ : (a : G) → M) a : M) (1 : M)
have obtain : ∀ (φi : Multiplicative (ZMod (n i)) →* M)
  (hφi :
    Ne (α := M)
      ((φi : (a : Multiplicative (ZMod (n i))) → M)
          ((Multiplicative.ofAdd : (a : ZMod (n i)) → Multiplicative (ZMod (n i)))
              ((Multiplicative.toAdd : (a : Multiplicative (ZMod (n i))) → ZMod (n i))
                ((e : (a : G) → (i : ι) → Multiplicative (ZMod (n i))) a i)) :
            Multiplicative (ZMod (n i))) :
        M)
      (1 : M)),
  ∃ (φ : G →* M), Ne.{u_2 + 1} (α := M) ((φ : (a : G) → M) a : M) (1 : M)
Tactic: obtain ⟨φi, hφi⟩ := H (n i) (dvd_exponent e i) ((e a i).toAdd) hi
-- 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
H :
  ∀ (n : ℕ),
    n ∣ Monoid.exponent G →
      ∀ (a : ZMod n),
        a ≠ 0 →
          ∃ (φ : 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)
a : G
ha : a ≠ 1
ι : Type
w : Fintype ι
n : ι → ℕ
left : ∀ (i : ι), 1 < n i
h : Nonempty.{u_1 + 1} (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))
e : G ≃* ((i : ι) → Multiplicative (ZMod (n i))) := h.some
i : ι
hi :
  Ne (α := Multiplicative (ZMod (n i)))
    ((e : (a : G) → (i : ι) → Multiplicative (ZMod (n i))) a i : Multiplicative (ZMod (n i)))
    (1 : Multiplicative (ZMod (n i)))
φi : Multiplicative (ZMod (n i)) →* M
hφi :
  Ne (α := M)
    ((φi : (a : Multiplicative (ZMod (n i))) → M)
        ((Multiplicative.ofAdd : (a : ZMod (n i)) → Multiplicative (ZMod (n i)))
            ((Multiplicative.toAdd : (a : Multiplicative (ZMod (n i))) → ZMod (n i))
              ((e : (a : G) → (i : ι) → Multiplicative (ZMod (n i))) a i)) :
          Multiplicative (ZMod (n i))) :
      M)
    (1 : M)
⊢ ∃ (φ : G →* M), Ne.{u_2 + 1} (α := M) ((φ : (a : G) → M) a : M) (1 : M)
have h₁ : Ne.{u_2 + 1} (α := M)
  ((comp (φi.comp (Pi.evalMonoidHom (fun (i : ι) ↦ Multiplicative (ZMod (n i))) i))
          (↑e : G →* (i : ι) → Multiplicative (ZMod (n i))) :
        (a : G) → M)
      a :
    M)
  (1 : M)
Tactic: use (φi.comp (Pi.evalMonoidHom (fun (i : ι) ↦ Multiplicative (ZMod (n i))) i)).comp e
-- 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)
a : G
ha : a ≠ 1
⊢ ∃ (φ : MonoidHom.{u_1, u_2} G Mˣ), Ne.{u_2 + 1} (α := Mˣ) ((φ : (a : G) → Mˣ) a : Mˣ) (1 : Mˣ)
have refine : ∀ (n : ℕ) (hn : n ∣ Monoid.exponent G) (a : ZMod n) (ha₀ : a ≠ 0),
  ∃ (φ : 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: refine exists_apply_ne_one_aux G Mˣ (fun n hn a ha₀ ↦ ?_) ha
-- 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)
a_1 : G
ha : a_1 ≠ 1
n : ℕ
hn : n ∣ Monoid.exponent G
a : ZMod n
ha₀ : a ≠ 0
⊢ ∃ (φ : 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ˣ)
have this : NeZero n
Tactic: have : NeZero n := ⟨fun H ↦ NeZero.ne _ <| Nat.eq_zero_of_zero_dvd (H ▸ hn)⟩
-- 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)
a_1 : G
ha : a_1 ≠ 1
n : ℕ
hn : n ∣ Monoid.exponent G
a : ZMod n
ha₀ : a ≠ 0
this : NeZero 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ˣ)
have this₁ : HasEnoughRootsOfUnity M n
Tactic: have := HasEnoughRootsOfUnity.of_dvd M hn
-- 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)
g 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'
have 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'
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ by simp [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)
⊢ Nonempty (MonoidHom.{u_1, u_2} G Mˣ ≃* G)
have 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)
Tactic: obtain ⟨ι, _, n, ⟨h₁, h₂⟩⟩ := equiv_prod_multiplicative_zmod_of_finite G
-- 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ˣ
⊢ Nonempty (MonoidHom.{u_1, u_2} G Mˣ ≃* G)
have this : ∀ (i : ι), NeZero (n i)
Tactic: have : ∀ i, NeZero (n i) := fun i ↦ NeZero.of_gt (h₁ i)