awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
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)
rw : FiniteIndex.{u_1} (G := ↥B) (MonoidHom.range (powMonoidHom n))
⊢ (subgroupOf (map (powMonoidHom n) B) B).FiniteIndex

Tactic:
rw [this]
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
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)
⊢ Group.FG.{u_1} ↥B

Tactic:
have := (Group.fg_iff_subgroup_fg B).mpr hB
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
Goal:
A : Type u_1
inst : CommGroup A
B : Subgroup A
hB : B.FG
n : ℕ
hn : n ≠ 0
this_1 : subgroupOf (map (powMonoidHom n) B) B = MonoidHom.range (powMonoidHom n)
this : Group.FG.{u_1} ↥B
⊢ FiniteIndex.{u_1} (G := ↥B) (MonoidHom.range (powMonoidHom n))

Tactic:
finiteIndex_range_powMonoidHom_of_fg B hn

Premises used: Membership.mem, Subtype, Subgroup.finiteIndex_range_powMonoidHom_of_fg
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
Goal:
A : Type u_1
inst : CommGroup A
B : Subgroup A
hB : B.FG
n : ℕ
hn : n ≠ 0
this_1 : subgroupOf (map (powMonoidHom n) B) B = MonoidHom.range (powMonoidHom n)
this : Group.FG.{u_1} ↥B
⊢ FiniteIndex.{u_1} (G := ↥B) (MonoidHom.range (powMonoidHom n))

Tactic:
exact finiteIndex_range_powMonoidHom_of_fg B hn

Premises used: Membership.mem, Subtype, Subgroup.finiteIndex_range_powMonoidHom_of_fg
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
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
rw : FG.{0, u_3} (R := ℤ) (M := M) ((AddSubgroup.toIntSubmodule : (a : AddSubgroup M) → Submodule ℤ M) A.toAddSubgroup)
⊢ A.toAddSubgroup.FG

Tactic:
rw [← AddSubgroup.toIntSubmodule_toAddSubgroup A.toAddSubgroup, ← fg_iff_addSubgroup_fg]

Premises used: Submodule.fg_iff_addSubgroup_fg, Submodule.toAddSubgroup, AddSubgroup.toIntSubmodule_toAddSubgroup
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
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
⊢ FG.{0, u_3} (R := ℤ) (M := M) ((AddSubgroup.toIntSubmodule : (a : AddSubgroup M) → Submodule ℤ M) A.toAddSubgroup)

Tactic:
FG.restrictScalars hfg

Premises used: Submodule.FG.restrictScalars, Submodule.restrictScalars
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
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
⊢ FG.{0, u_3} (R := ℤ) (M := M) ((AddSubgroup.toIntSubmodule : (a : AddSubgroup M) → Submodule ℤ M) A.toAddSubgroup)

Tactic:
exact FG.restrictScalars hfg

Premises used: Submodule.FG.restrictScalars
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
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
⊢ AddSubgroup.FG.{u_2} (G := K) A.toAddSubgroup

Tactic:
have := fg_toAddSubgroup hfg
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
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) (AddSubgroup.map (G := K) (nsmulAddMonoidHom n) A.toAddSubgroup) A.toAddSubgroup

Tactic:
have := isFiniteRelIndex_map_nsmulAddMonoidHom_of_fg this hn
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
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

Tactic:
isFiniteRelIndex_of_le_left (H := A.toAddSubgroup.map (nsmulAddMonoidHom n))
    A.toAddSubgroup ?_

Premises used: AddSubgroup.isFiniteRelIndex_of_le_left, Submodule.toAddSubgroup
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
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
refine :
  LE.le.{u_2} (α := AddSubgroup K) (AddSubgroup.map (G := K) (nsmulAddMonoidHom n) A.toAddSubgroup) B.toAddSubgroup
⊢ IsFiniteRelIndex.{u_2} (G := K) B.toAddSubgroup A.toAddSubgroup

Tactic:
refine isFiniteRelIndex_of_le_left (H := A.toAddSubgroup.map (nsmulAddMonoidHom n))
    A.toAddSubgroup ?_

Premises used: AddSubgroup.isFiniteRelIndex_of_le_left, Submodule.toAddSubgroup
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
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
⊢ ∀ ⦃x : K⦄, x ∈ map (LinearMap.mulLeft R (↑n : K)) A → x ∈ B

Tactic:
rw [SetLike.le_def] at h ⊢

Premises used: SetLike.le_def
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
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
h₁ : ∀ ⦃x : K⦄, x ∈ map (LinearMap.mulLeft R (↑n : K)) A → x ∈ B
⊢ AddSubgroup.FG.{u_2} (G := K) A.toAddSubgroup

Tactic:
rw [SetLike.le_def] at h ⊢

Premises used: SetLike.le_def
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
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
h₁ : ∀ ⦃x : K⦄, x ∈ map (LinearMap.mulLeft R (↑n : K)) A → x ∈ B
this₁ : AddSubgroup.FG.{u_2} (G := K) A.toAddSubgroup
⊢ IsFiniteRelIndex.{u_2} (G := K) (AddSubgroup.map (G := K) (nsmulAddMonoidHom n) A.toAddSubgroup) A.toAddSubgroup

Tactic:
rw [SetLike.le_def] at h ⊢

Premises used: SetLike.le_def
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
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 : ∀ ⦃x : K⦄, x ∈ map (LinearMap.mulLeft R (↑n : K)) A → x ∈ 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
⊢ ∀ ⦃x : K⦄,
    Membership.mem (γ := AddSubgroup K) (AddSubgroup.map (G := K) (nsmulAddMonoidHom n) A.toAddSubgroup) x →
      Membership.mem (γ := AddSubgroup K) B.toAddSubgroup x

Tactic:
simpa using h
-- Module: Mathlib.GroupTheory.FiniteAbelian.Duality
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 =
    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:
simpa only [MulEquiv.orderOf_eq, orderOf_piMulSingle, orderOf_ofAdd_eq_addOrderOf]
      using (ZMod.addOrderOf_one (n i)).symm

Premises used: orderOf_ofAdd_eq_addOrderOf, orderOf_piMulSingle, MulEquiv.orderOf_eq, ZMod.addOrderOf_one, Eq.symm
-- Module: Mathlib.GroupTheory.FiniteAbelian.Duality
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 =
    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
-- Module: Mathlib.GroupTheory.FiniteAbelian.Duality
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 : ι
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:
this ▸ Monoid.order_dvd_exponent _

Premises used: Monoid.order_dvd_exponent, Eq.rec, Eq.symm
-- Module: Mathlib.GroupTheory.FiniteAbelian.Duality
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 : ι
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:
exact this ▸ Monoid.order_dvd_exponent _
-- Module: Mathlib.GroupTheory.FiniteAbelian.Duality
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)
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
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)
classical₃ 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
⊢ 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 _
-- 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
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
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)
⊢ ∃ (φ : 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

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
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
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
⊢ ∃ (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)))

Tactic:
contrapose! ha
-- 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
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
ι : 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
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:
(MulEquiv.map_eq_one_iff e).mp <| funext ha

Premises used: MulEquiv.map_eq_one_iff, funext, Iff.mp
-- 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
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
ι : 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
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:
exact (MulEquiv.map_eq_one_iff e).mp <| funext ha

Premises used: MulEquiv.map_eq_one_iff, funext, Iff.mp
-- 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
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
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)
⊢ ∃ (φ : 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
-- 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
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)))
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)
⊢ ∃ (φ : 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

Premises used: Multiplicative.toAdd, _private.0.CommGroup.dvd_exponent, DFunLike.coe
-- 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
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)
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)
⊢ ∃ (φ : G →* M), Ne.{u_2 + 1} (α := M) ((φ : (a : G) → M) a : M) (1 : M)

Tactic:
use (φi.comp (Pi.evalMonoidHom (fun (i : ι) ↦ Multiplicative (ZMod (n i))) i)).comp e

Premises used: MonoidHom.comp, ZMod, Multiplicative, Pi.evalMonoidHom
-- 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
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)
⊢ 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:
simpa only [coe_comp, coe_coe, Function.comp_apply, Pi.evalMonoidHom_apply, ne_eq] using hφi

Premises used: MonoidHom.coe_comp, Pi.evalMonoidHom_apply, MonoidHom.coe_coe, ne_eq, Function.comp_apply
-- 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 : G
ha : a ≠ 1
⊢ ∃ (φ : MonoidHom.{u_1, u_2} G Mˣ), Ne.{u_2 + 1} (α := Mˣ) ((φ : (a : G) → Mˣ) a : Mˣ) (1 : Mˣ)

Tactic:
exists_apply_ne_one_aux G Mˣ (fun n hn a ha₀ ↦ ?_) ha

Premises used: _private.0.CommGroup.exists_apply_ne_one_aux, Units
-- 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 : G
ha : a ≠ 1
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ˣ)
⊢ ∃ (φ : MonoidHom.{u_1, u_2} G Mˣ), Ne.{u_2 + 1} (α := Mˣ) ((φ : (a : G) → Mˣ) a : Mˣ) (1 : Mˣ)

Tactic:
refine exists_apply_ne_one_aux G Mˣ (fun n hn a ha₀ ↦ ?_) ha

Premises used: _private.0.CommGroup.exists_apply_ne_one_aux, Units