awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : CommGroup M
inst_1 : Group N
f : M →* N
h : (Nat.card.{u_4} ↥f.ker).Coprime (Nat.card.{u_5} ↥f.range)
inst_2 : IsCyclic.{u_4} ↥f.ker
inst_3 : IsCyclic.{u_5} ↥f.range
h_1 : Finite.{u_4 + 1} ↥f.ker
h_2 : Finite.{u_5 + 1} ↥f.range
this : Finite M
inr : Monoid.exponent M = Nat.card M
⊢ IsCyclic M

Tactic:
rw [IsCyclic.iff_exponent_eq_card]

Premises used: IsCyclic.iff_exponent_eq_card
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : CommGroup M
inst_1 : Group N
f : M →* N
h : (Nat.card.{u_4} ↥f.ker).Coprime (Nat.card.{u_5} ↥f.range)
inst_2 : IsCyclic.{u_4} ↥f.ker
inst_3 : IsCyclic.{u_5} ↥f.range
h_1 : Finite.{u_4 + 1} ↥f.ker
h_2 : Finite.{u_5 + 1} ↥f.range
this : Finite M
inr : Nat.card M ∣ Monoid.exponent M
⊢ Monoid.exponent M = Nat.card M

Tactic:
apply dvd_antisymm Group.exponent_dvd_nat_card

Premises used: dvd_antisymm, Group.exponent_dvd_nat_card
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : CommGroup M
inst_1 : Group N
f : M →* N
h : (Nat.card.{u_4} ↥f.ker).Coprime (Nat.card.{u_5} ↥f.range)
inst_2 : IsCyclic.{u_4} ↥f.ker
inst_3 : IsCyclic.{u_5} ↥f.range
h_1 : Finite.{u_4 + 1} ↥f.ker
h_2 : Finite.{u_5 + 1} ↥f.range
this : Finite M
inr : Nat.card.{u_4} ↥f.ker * Nat.card.{u_5} ↥f.range ∣ Monoid.exponent M
⊢ Nat.card M ∣ Monoid.exponent M

Tactic:
rw [← f.ker.card_mul_index, Subgroup.index_ker]

Premises used: Subgroup.index_ker, MonoidHom.ker, Subgroup.card_mul_index
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : CommGroup M
inst_1 : Group N
f : M →* N
h : (Nat.card.{u_4} ↥f.ker).Coprime (Nat.card.{u_5} ↥f.range)
inst_2 : IsCyclic.{u_4} ↥f.ker
inst_3 : IsCyclic.{u_5} ↥f.range
h_1 : Finite.{u_4 + 1} ↥f.ker
h_2 : Finite.{u_5 + 1} ↥f.range
this : Finite M
inr : Nat.card.{u_4} ↥f.ker ∣ Monoid.exponent M
inr₁ : Nat.card.{u_5} ↥f.range ∣ Monoid.exponent M
⊢ Nat.card.{u_4} ↥f.ker * Nat.card.{u_5} ↥f.range ∣ Monoid.exponent M

Tactic:
apply h.mul_dvd_of_dvd_of_dvd

Premises used: Nat.Coprime.mul_dvd_of_dvd_of_dvd
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : CommGroup M
inst_1 : Group N
f : M →* N
h : (Nat.card.{u_4} ↥f.ker).Coprime (Nat.card.{u_5} ↥f.range)
inst_2 : IsCyclic.{u_4} ↥f.ker
inst_3 : IsCyclic.{u_5} ↥f.range
h_1 : Finite.{u_4 + 1} ↥f.ker
h_2 : Finite.{u_5 + 1} ↥f.range
this : Finite M
inr : Monoid.exponent.{u_4} ↥f.ker ∣ Monoid.exponent M
⊢ Nat.card.{u_4} ↥f.ker ∣ Monoid.exponent M

Tactic:
rw [← IsCyclic.exponent_eq_card]

Premises used: IsCyclic.exponent_eq_card
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : CommGroup M
inst_1 : Group N
f : M →* N
h : (Nat.card.{u_4} ↥f.ker).Coprime (Nat.card.{u_5} ↥f.range)
inst_2 : IsCyclic.{u_4} ↥f.ker
inst_3 : IsCyclic.{u_5} ↥f.range
h_1 : Finite.{u_4 + 1} ↥f.ker
h_2 : Finite.{u_5 + 1} ↥f.range
this : Finite M
inr : Monoid.exponent.{u_5} ↥f.range ∣ Monoid.exponent M
⊢ Nat.card.{u_5} ↥f.range ∣ Monoid.exponent M

Tactic:
rw [← IsCyclic.exponent_eq_card]

Premises used: IsCyclic.exponent_eq_card
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : CommGroup M
inst_1 : Group N
f : M →* N
h : (Nat.card.{u_4} ↥f.ker).Coprime (Nat.card.{u_5} ↥f.range)
inst_2 : IsCyclic.{u_4} ↥f.ker
inst_3 : IsCyclic.{u_5} ↥f.range
h_1 : Finite.{u_4 + 1} ↥f.ker
h_2 : Finite.{u_5 + 1} ↥f.range
this : Finite M
⊢ Monoid.exponent.{u_4} ↥f.ker ∣ Monoid.exponent M

Tactic:
Monoid.exponent_dvd_of_monoidHom _ f.ker.subtype_injective

Premises used: Subgroup.subtype_injective, MonoidHom.ker, Monoid.exponent_dvd_of_monoidHom
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : CommGroup M
inst_1 : Group N
f : M →* N
h : (Nat.card.{u_4} ↥f.ker).Coprime (Nat.card.{u_5} ↥f.range)
inst_2 : IsCyclic.{u_4} ↥f.ker
inst_3 : IsCyclic.{u_5} ↥f.range
h_1 : Finite.{u_4 + 1} ↥f.ker
h_2 : Finite.{u_5 + 1} ↥f.range
this : Finite M
⊢ Monoid.exponent.{u_4} ↥f.ker ∣ Monoid.exponent M

Tactic:
exact Monoid.exponent_dvd_of_monoidHom _ f.ker.subtype_injective

Premises used: Subgroup.subtype_injective, MonoidHom.ker, Monoid.exponent_dvd_of_monoidHom
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : CommGroup M
inst_1 : Group N
f : M →* N
h : (Nat.card.{u_4} ↥f.ker).Coprime (Nat.card.{u_5} ↥f.range)
inst_2 : IsCyclic.{u_4} ↥f.ker
inst_3 : IsCyclic.{u_5} ↥f.range
h_1 : Finite.{u_4 + 1} ↥f.ker
h_2 : Finite.{u_5 + 1} ↥f.range
this : Finite M
⊢ Monoid.exponent.{u_5} ↥f.range ∣ Monoid.exponent M

Tactic:
MonoidHom.exponent_dvd f.rangeRestrict_surjective

Premises used: MonoidHom.exponent_dvd, MonoidHom.rangeRestrict_surjective
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : CommGroup M
inst_1 : Group N
f : M →* N
h : (Nat.card.{u_4} ↥f.ker).Coprime (Nat.card.{u_5} ↥f.range)
inst_2 : IsCyclic.{u_4} ↥f.ker
inst_3 : IsCyclic.{u_5} ↥f.range
h_1 : Finite.{u_4 + 1} ↥f.ker
h_2 : Finite.{u_5 + 1} ↥f.range
this : Finite M
⊢ Monoid.exponent.{u_5} ↥f.range ∣ Monoid.exponent M

Tactic:
exact MonoidHom.exponent_dvd f.rangeRestrict_surjective

Premises used: MonoidHom.exponent_dvd, MonoidHom.rangeRestrict_surjective
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : CommGroup M
inst_1 : Group N
f : M →* N
h : (Nat.card.{u_4} ↥f.ker).Coprime (Nat.card N)
inst_2 : IsCyclic.{u_4} ↥f.ker
hN : IsCyclic N
hf : Function.Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ IsCyclic.{u_5} ↥f.range

Tactic:
rw [← Subgroup.topEquiv.isCyclic, ← f.range_eq_top.mpr hf] at hN

Premises used: Iff.mpr, MonoidHom.range_eq_top, Subgroup.topEquiv, MulEquiv.isCyclic
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : CommGroup M
inst_1 : Group N
f : M →* N
h : (Nat.card.{u_4} ↥f.ker).Coprime (Nat.card N)
inst_2 : IsCyclic.{u_4} ↥f.ker
hN : IsCyclic N
hf : Function.Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
hN₁ : IsCyclic.{u_5} ↥f.range
⊢ Function.Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := N) (⇑f : (a : M) → N)

Tactic:
rw [← Subgroup.topEquiv.isCyclic, ← f.range_eq_top.mpr hf] at hN

Premises used: Iff.mpr, MonoidHom.range_eq_top, Subgroup.topEquiv, MulEquiv.isCyclic
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : CommGroup M
inst_1 : Group N
f : M →* N
h : (Nat.card.{u_4} ↥f.ker).Coprime (Nat.card N)
inst_2 : IsCyclic.{u_4} ↥f.ker
hN : IsCyclic.{u_5} ↥f.range
hf : Function.Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ (Nat.card.{u_4} ↥f.ker).Coprime (Nat.card.{u_5} ↥f.range)

Tactic:
rw [← Subgroup.card_top (G := N), ← f.range_eq_top.mpr hf] at h

Premises used: Iff.mpr, Subgroup.card_top, MonoidHom.range_eq_top
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : CommGroup M
inst_1 : Group N
f : M →* N
h : (Nat.card.{u_4} ↥f.ker).Coprime (Nat.card N)
inst_2 : IsCyclic.{u_4} ↥f.ker
hN : IsCyclic.{u_5} ↥f.range
hf : Function.Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
h₁ : (Nat.card.{u_4} ↥f.ker).Coprime (Nat.card.{u_5} ↥f.range)
⊢ IsCyclic.{u_4} ↥f.ker

Tactic:
rw [← Subgroup.card_top (G := N), ← f.range_eq_top.mpr hf] at h

Premises used: Iff.mpr, Subgroup.card_top, MonoidHom.range_eq_top
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst_1 : CommGroup M
inst_2 : Group N
f : M →* N
h : (Nat.card.{u_4} ↥f.ker).Coprime (Nat.card N)
inst_3 : IsCyclic.{u_4} ↥f.ker
hN : IsCyclic.{u_5} ↥f.range
hf : Function.Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
h₁ : (Nat.card.{u_4} ↥f.ker).Coprime (Nat.card.{u_5} ↥f.range)
inst : IsCyclic.{u_4} ↥f.ker
⊢ IsCyclic.{u_5} ↥f.range

Tactic:
rw [← Subgroup.card_top (G := N), ← f.range_eq_top.mpr hf] at h

Premises used: Iff.mpr, Subgroup.card_top, MonoidHom.range_eq_top
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst_1 : CommGroup M
inst_2 : Group N
f : M →* N
h : (Nat.card.{u_4} ↥f.ker).Coprime (Nat.card N)
inst_3 : IsCyclic.{u_4} ↥f.ker
hN : IsCyclic.{u_5} ↥f.range
hf : Function.Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
h₁ : (Nat.card.{u_4} ↥f.ker).Coprime (Nat.card.{u_5} ↥f.range)
inst : IsCyclic.{u_4} ↥f.ker
hN₁ : IsCyclic.{u_5} ↥f.range
⊢ Function.Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := N) (⇑f : (a : M) → N)

Tactic:
rw [← Subgroup.card_top (G := N), ← f.range_eq_top.mpr hf] at h

Premises used: Iff.mpr, Subgroup.card_top, MonoidHom.range_eq_top
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : CommGroup M
inst_1 : Group N
f : M →* N
h : (Nat.card.{u_4} ↥f.ker).Coprime (Nat.card.{u_5} ↥f.range)
inst_2 : IsCyclic.{u_4} ↥f.ker
hN : IsCyclic.{u_5} ↥f.range
hf : Function.Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ IsCyclic M

Tactic:
isCyclic_of_coprime_card_range_card_ker f h

Premises used: Group.isCyclic_of_coprime_card_range_card_ker
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : CommGroup M
inst_1 : Group N
f : M →* N
h : (Nat.card.{u_4} ↥f.ker).Coprime (Nat.card.{u_5} ↥f.range)
inst_2 : IsCyclic.{u_4} ↥f.ker
hN : IsCyclic.{u_5} ↥f.range
hf : Function.Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ IsCyclic M

Tactic:
exact isCyclic_of_coprime_card_range_card_ker f h

Premises used: Group.isCyclic_of_coprime_card_range_card_ker
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : Group M
inst_1 : Group N
cyc : IsCyclic (M × N)
⊢ IsCyclic M

Tactic:
isCyclic_of_surjective (MonoidHom.fst M N) Prod.fst_surjective

Premises used: isCyclic_of_surjective, Prod.fst_surjective, MonoidHom.fst
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : Group M
inst_1 : Group N
cyc : IsCyclic (M × N)
⊢ IsCyclic N

Tactic:
isCyclic_of_surjective (MonoidHom.snd M N) Prod.snd_surjective

Premises used: isCyclic_of_surjective, Prod.snd_surjective, MonoidHom.snd
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : Group M
inst_1 : Group N
cyc : IsCyclic (M × N)
inst_2 : Finite M
inst_3 : Finite N
⊢ IsCyclic M

Tactic:
have hM := isCyclic_left_of_prod M N
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : Group M
inst_1 : Group N
cyc : IsCyclic (M × N)
inst_2 : Finite M
inst_3 : Finite N
hM : IsCyclic M
⊢ IsCyclic N

Tactic:
have hN := isCyclic_right_of_prod M N
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : Group M
inst_1 : Group N
cyc : IsCyclic (M × N)
inst_2 : Finite M
inst_3 : Finite N
hM : IsCyclic M
hN : IsCyclic N
x : CommGroup (M × N) := IsCyclic.commGroup
x_1 : CommGroup M := IsCyclic.commGroup
x_2 : CommGroup N := IsCyclic.commGroup
⊢ (Monoid.exponent M).lcm (Monoid.exponent N) = Nat.card M * Nat.card N

Tactic:
rw [IsCyclic.iff_exponent_eq_card, Monoid.exponent_prod, Nat.card_prod, lcm_eq_nat_lcm] at *

Premises used: IsCyclic.iff_exponent_eq_card, Monoid.exponent_prod, lcm_eq_nat_lcm, Nat.card_prod
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : Group M
inst_1 : Group N
cyc : IsCyclic (M × N)
inst_2 : Finite M
inst_3 : Finite N
hM : IsCyclic M
hN : IsCyclic N
x : CommGroup (M × N) := IsCyclic.commGroup
x_1 : CommGroup M := IsCyclic.commGroup
x_2 : CommGroup N := IsCyclic.commGroup
cyc₁ : (Monoid.exponent M).lcm (Monoid.exponent N) = Nat.card M * Nat.card N
⊢ let x : CommGroup M := IsCyclic.commGroup;
  Monoid.exponent M = Nat.card M

Tactic:
rw [IsCyclic.iff_exponent_eq_card, Monoid.exponent_prod, Nat.card_prod, lcm_eq_nat_lcm] at *

Premises used: IsCyclic.iff_exponent_eq_card, Monoid.exponent_prod, lcm_eq_nat_lcm, Nat.card_prod
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : Group M
inst_1 : Group N
cyc : IsCyclic (M × N)
inst_2 : Finite M
inst_3 : Finite N
hM : IsCyclic M
hN : IsCyclic N
x : CommGroup (M × N) := IsCyclic.commGroup
x_1 : CommGroup M := IsCyclic.commGroup
x_2 : CommGroup N := IsCyclic.commGroup
cyc₁ : (Monoid.exponent M).lcm (Monoid.exponent N) = Nat.card M * Nat.card N
hM₁ :
  let x : CommGroup M := IsCyclic.commGroup;
  Monoid.exponent M = Nat.card M
⊢ let x : CommGroup N := IsCyclic.commGroup;
  Monoid.exponent N = Nat.card N

Tactic:
rw [IsCyclic.iff_exponent_eq_card, Monoid.exponent_prod, Nat.card_prod, lcm_eq_nat_lcm] at *

Premises used: IsCyclic.iff_exponent_eq_card, Monoid.exponent_prod, lcm_eq_nat_lcm, Nat.card_prod
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : Group M
inst_1 : Group N
cyc_1 : IsCyclic (M × N)
inst_2 : Finite M
inst_3 : Finite N
hM_1 : IsCyclic M
hN_1 : IsCyclic N
x : CommGroup (M × N) := IsCyclic.commGroup
cyc : (Monoid.exponent M).lcm (Monoid.exponent N) = Nat.card M * Nat.card N
x_1 : CommGroup M := IsCyclic.commGroup
hM : Monoid.exponent M = Nat.card M
x_2 : CommGroup N := IsCyclic.commGroup
hN : Monoid.exponent N = Nat.card N
⊢ (Nat.card M).Coprime (Nat.card N)

Tactic:
simpa only [hM, hN, Nat.lcm_eq_mul_iff, Nat.card_pos.ne', false_or] using cyc

Premises used: Nat.card_pos, false_or, LT.lt.ne', Nat.lcm_eq_mul_iff
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : AddGroup M
inst_1 : AddGroup N
inst_2 : Infinite M
inst_3 : Nontrivial N
hMN : IsAddCyclic (M × N)
⊢ IsAddCyclic (ZMod 0 × ZMod (Nat.card N))

Tactic:
rw [← ((zmodAddCyclicAddEquiv <| isAddCyclic_left_of_prod M N).prodCongr (zmodAddCyclicAddEquiv <|
    isAddCyclic_right_of_prod M N)).isAddCyclic, Nat.card_eq_zero_of_infinite] at hMN

Premises used: isAddCyclic_left_of_prod, Nat.card_eq_zero_of_infinite, AddEquiv.isAddCyclic, zmodAddCyclicAddEquiv, AddEquiv.prodCongr, isAddCyclic_right_of_prod
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : AddGroup M
inst_1 : AddGroup N
inst_2 : Infinite M
inst_3 : Nontrivial N
hMN : IsAddCyclic (ZMod 0 × ZMod (Nat.card N))
inl : Infinite N → False
inr : Finite N → False
⊢ False

Tactic:
cases (finite_or_infinite N).symm

Premises used: finite_or_infinite, Or.symm
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : AddGroup M
inst_1 : AddGroup N
inst_2 : Infinite M
inst_3 : Nontrivial N
hMN : IsAddCyclic (ZMod 0 × ZMod (Nat.card N))
h : Infinite N
⊢ IsAddCyclic (ZMod 0 × ZMod 0)

Tactic:
rw [Nat.card_eq_zero_of_infinite] at hMN

Premises used: Nat.card_eq_zero_of_infinite
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : AddGroup M
inst_1 : AddGroup N
inst_2 : Infinite M
inst_3 : Nontrivial N
hMN : IsAddCyclic (ZMod 0 × ZMod (Nat.card N))
h : Infinite N
hMN₁ : IsAddCyclic (ZMod 0 × ZMod 0)
⊢ Infinite N

Tactic:
rw [Nat.card_eq_zero_of_infinite] at hMN

Premises used: Nat.card_eq_zero_of_infinite
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : AddGroup M
inst_1 : AddGroup N
inst_2 : Infinite M
inst_3 : Nontrivial N
hMN : IsAddCyclic (ZMod 0 × ZMod 0)
h : Infinite N
f : ZMod 0 →+ ZMod 2 := RingHom.toAddMonoidHom (ZMod.castHom ⋯ (ZMod 2))
⊢ Function.Surjective (α := ZMod 0) (β := ZMod 2) (⇑(ZMod.castHom ⋯ (ZMod 2)) : (a : ZMod 0) → ZMod 2)

Tactic:
have hf := ZMod.castHom_surjective (dvd_zero 2)
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : AddGroup M
inst_1 : AddGroup N
inst_2 : Infinite M
inst_3 : Nontrivial N
hMN : IsAddCyclic (ZMod 0 × ZMod 0)
h : Infinite N
f : ZMod 0 →+ ZMod 2 := RingHom.toAddMonoidHom (ZMod.castHom ⋯ (ZMod 2))
hf : Function.Surjective (α := ZMod 0) (β := ZMod 2) (⇑(ZMod.castHom ⋯ (ZMod 2)) : (a : ZMod 0) → ZMod 2)
⊢ IsAddCyclic (ZMod 2 × ZMod 2)

Tactic:
have := isAddCyclic_of_surjective (f.prodMap f) (Prod.map_surjective.mpr ⟨hf, hf⟩)
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : AddGroup M
inst_1 : AddGroup N
inst_2 : Infinite M
inst_3 : Nontrivial N
hMN : IsAddCyclic (ZMod 0 × ZMod 0)
h : Infinite N
f : ZMod 0 →+ ZMod 2 := RingHom.toAddMonoidHom (ZMod.castHom ⋯ (ZMod 2))
hf : Function.Surjective (α := ZMod 0) (β := ZMod 2) (⇑(ZMod.castHom ⋯ (ZMod 2)) : (a : ZMod 0) → ZMod 2)
this : IsAddCyclic (ZMod 2 × ZMod 2)
⊢ False

Tactic:
simpa using coprime_card_of_isAddCyclic_prod (ZMod 2) (ZMod 2)

Premises used: ZMod, OfNat.ofNat, coprime_card_of_isAddCyclic_prod
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : AddGroup M
inst_1 : AddGroup N
inst_2 : Infinite M
inst_3 : Nontrivial N
hMN : IsAddCyclic (ZMod 0 × ZMod (Nat.card N))
h : Finite N
ZN : Type := ZMod (Nat.card N)
⊢ NeZero (Nat.card N)

Tactic:
have : NeZero (Nat.card N) := ⟨Nat.card_pos.ne'⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : AddGroup M
inst_1 : AddGroup N
inst_2 : Infinite M
inst_3 : Nontrivial N
hMN : IsAddCyclic (ZMod 0 × ZMod (Nat.card N))
h : Finite N
ZN : Type := ZMod (Nat.card N)
this : NeZero (Nat.card N)
⊢ IsAddCyclic (ZMod (Nat.card N) × ZN)

Tactic:
have := isAddCyclic_of_surjective ((ZMod.castHom (dvd_zero _) ZN).toAddMonoidHom.prodMap (.id ZN))
    (Prod.map_surjective.mpr ⟨ZMod.castHom_surjective (dvd_zero _), Function.surjective_id⟩)
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : AddGroup M
inst_1 : AddGroup N
inst_2 : Infinite M
inst_3 : Nontrivial N
hMN : IsAddCyclic (ZMod 0 × ZMod (Nat.card N))
h : Finite N
ZN : Type := ZMod (Nat.card N)
this_1 : NeZero (Nat.card N)
this : IsAddCyclic (ZMod (Nat.card N) × ZN)
⊢ Nat.card N = 1

Tactic:
simpa [ZN] using coprime_card_of_isAddCyclic_prod ZN ZN

Premises used: coprime_card_of_isAddCyclic_prod
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : AddGroup M
inst_1 : AddGroup N
inst_2 : Infinite M
inst_3 : Nontrivial N
hMN : IsAddCyclic (ZMod 0 × ZMod (Nat.card N))
h : Finite N
ZN : Type := ZMod (Nat.card N)
this_1 : NeZero (Nat.card N)
this : IsAddCyclic (ZMod (Nat.card N) × ZN)
⊢ False

Tactic:
exact Finite.one_lt_card (α := N).ne' (by simpa [ZN] using coprime_card_of_isAddCyclic_prod ZN ZN)

Premises used: LT.lt.ne', Finite.one_lt_card
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : Group M
inst_1 : Group N
inst_2 : Infinite M
inst_3 : Nontrivial N
rw : ¬IsAddCyclic (Prod.{u_4, u_5} (Additive M) (Additive N))
⊢ ¬IsCyclic (M × N)

Tactic:
rw [← isAddCyclic_additive_iff, (AddEquiv.prodAdditive ..).isAddCyclic]

Premises used: AddEquiv.isAddCyclic, isAddCyclic_additive_iff
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : Group M
inst_1 : Group N
inst_2 : Infinite M
inst_3 : Nontrivial N
⊢ ¬IsAddCyclic (Prod.{u_4, u_5} (Additive M) (Additive N))

Tactic:
apply not_isAddCyclic_prod_of_infinite_nontrivial

Premises used: not_isAddCyclic_prod_of_infinite_nontrivial
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : Group M
inst_1 : Group N
⊢ IsCyclic (M × N) ↔ IsCyclic M ∧ IsCyclic N ∧ (Nat.card M).Coprime (Nat.card N)

Tactic:
⟨fun h ↦ ⟨isCyclic_left_of_prod M N, isCyclic_right_of_prod M N, ?_⟩, fun ⟨hM, hN, h⟩ ↦ ?_⟩

Premises used: _private.0.Group.isCyclic_prod_iff.match_1, isCyclic_left_of_prod, And.intro, Iff.intro, Prod, IsCyclic, isCyclic_right_of_prod
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : Group M
inst_1 : Group N
refine_1 : ∀ (h : IsCyclic (M × N)), (Nat.card M).Coprime (Nat.card N)
refine_2 :
  IsCyclic M ∧ IsCyclic N ∧ (Nat.card M).Coprime (Nat.card N) →
    ∀ (hM : IsCyclic M) (hN : IsCyclic N) (h : (Nat.card M).Coprime (Nat.card N)), IsCyclic (M × N)
⊢ IsCyclic (M × N) ↔ IsCyclic M ∧ IsCyclic N ∧ (Nat.card M).Coprime (Nat.card N)

Tactic:
refine ⟨fun h ↦ ⟨isCyclic_left_of_prod M N, isCyclic_right_of_prod M N, ?_⟩, fun ⟨hM, hN, h⟩ ↦ ?_⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : Group M
inst_1 : Group N
h : IsCyclic (M × N)
refine_1 : Infinite M → (Nat.card M).Coprime (Nat.card N)
refine_1₁ : Finite M → (Nat.card M).Coprime (Nat.card N)
⊢ (Nat.card M).Coprime (Nat.card N)

Tactic:
cases (finite_or_infinite M).symm

Premises used: finite_or_infinite, Or.symm
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : Group M
inst_1 : Group N
h : IsCyclic (M × N)
h_1 : Infinite M
refine_1 : Subsingleton N → (Nat.card M).Coprime (Nat.card N)
refine_1₁ : Nontrivial N → (Nat.card M).Coprime (Nat.card N)
⊢ (Nat.card M).Coprime (Nat.card N)

Tactic:
cases subsingleton_or_nontrivial N

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : Group M
inst_1 : Group N
h : IsCyclic (M × N)
h_1 : Infinite M
h_2 : Subsingleton N
⊢ (Nat.card M).Coprime (Nat.card N)

Tactic:
simp
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : Group M
inst_1 : Group N
h : IsCyclic (M × N)
h_1 : Infinite M
h_2 : Nontrivial N
⊢ (Nat.card M).Coprime (Nat.card N)

Tactic:
(not_isCyclic_prod_of_infinite_nontrivial M N h).elim

Premises used: False.elim, not_isCyclic_prod_of_infinite_nontrivial
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : Group M
inst_1 : Group N
h : IsCyclic (M × N)
h_1 : Infinite M
h_2 : Nontrivial N
⊢ (Nat.card M).Coprime (Nat.card N)

Tactic:
exact (not_isCyclic_prod_of_infinite_nontrivial M N h).elim

Premises used: False.elim, not_isCyclic_prod_of_infinite_nontrivial
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : Group M
inst_1 : Group N
h : IsCyclic (M × N)
h_1 : Finite M
refine_1 : Infinite N → (Nat.card M).Coprime (Nat.card N)
refine_1₁ : Finite N → (Nat.card M).Coprime (Nat.card N)
⊢ (Nat.card M).Coprime (Nat.card N)

Tactic:
cases (finite_or_infinite N).symm

Premises used: finite_or_infinite, Or.symm
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : Group M
inst_1 : Group N
h : IsCyclic (M × N)
h_1 : Finite M
h_2 : Infinite N
refine_1 : Subsingleton M → (Nat.card M).Coprime (Nat.card N)
refine_1₁ : Nontrivial M → (Nat.card M).Coprime (Nat.card N)
⊢ (Nat.card M).Coprime (Nat.card N)

Tactic:
cases subsingleton_or_nontrivial M

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : Group M
inst_1 : Group N
h : IsCyclic (M × N)
h_1 : Finite M
h_2 : Infinite N
h_3 : Subsingleton M
⊢ (Nat.card M).Coprime (Nat.card N)

Tactic:
simp
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : Group M
inst_1 : Group N
h : IsCyclic (M × N)
h_1 : Finite M
h_2 : Infinite N
h_3 : Nontrivial M
⊢ IsCyclic (N × M)

Tactic:
rw [(MulEquiv.prodComm ..).isCyclic] at h

Premises used: MulEquiv.isCyclic
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : Group M
inst_1 : Group N
h : IsCyclic (M × N)
h_1 : Finite M
h_2 : Infinite N
h_3 : Nontrivial M
h₁ : IsCyclic (N × M)
⊢ Finite M

Tactic:
rw [(MulEquiv.prodComm ..).isCyclic] at h

Premises used: MulEquiv.isCyclic
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : Group M
inst_1 : Group N
h : IsCyclic (M × N)
h_1 : Finite M
h_2 : Infinite N
h_3 : Nontrivial M
h₁ : IsCyclic (N × M)
h₂ : Finite M
⊢ Infinite N

Tactic:
rw [(MulEquiv.prodComm ..).isCyclic] at h

Premises used: MulEquiv.isCyclic
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : Group M
inst_1 : Group N
h : IsCyclic (M × N)
h_1 : Finite M
h_2 : Infinite N
h_3 : Nontrivial M
h₁ : IsCyclic (N × M)
h₂ : Finite M
h₃ : Infinite N
⊢ Nontrivial M

Tactic:
rw [(MulEquiv.prodComm ..).isCyclic] at h

Premises used: MulEquiv.isCyclic