awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : IsCyclic G
inst_2 : Finite G
d : ℕ
rw : Nat.card.{u_2} ↥(MonoidHom.range (G := G) (powMonoidHom d)) = Nat.card G / (Nat.card G).gcd d
rw₁ rw₂ : Nat.card G / (Nat.card G).gcd d = Nat.card G / (Nat.card G).gcd d
⊢ Subgroup.index.{u_2} (G := G) (MonoidHom.ker (M := G) (powMonoidHom d)) = Nat.card G / (Nat.card G).gcd d

Tactic:
rw [Subgroup.index_ker, card_powMonoidHom_range]

Premises used: Subgroup.index_ker, IsCyclic.card_powMonoidHom_range
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : IsCyclic G
inst_2 : Finite G
d : ℕ
⊢ Subgroup.index.{u_2} (G := G) (MonoidHom.ker (M := G) (powMonoidHom d)) ≠ 0

Tactic:
have h : (powMonoidHom d : G →* G).ker.index ≠ 0 := Subgroup.index_ne_zero_of_finite
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : IsCyclic G
inst_2 : Finite G
d : ℕ
h : Subgroup.index.{u_2} (G := G) (MonoidHom.ker (M := G) (powMonoidHom d)) ≠ 0
rw : (Nat.card G).gcd d ∣ Nat.card G
⊢ Nat.card.{u_2} ↥(MonoidHom.ker (M := G) (powMonoidHom d)) = (Nat.card G).gcd d

Tactic:
rw [← mul_left_inj' h, Subgroup.card_mul_index, index_powMonoidHom_ker, Nat.mul_div_cancel']

Premises used: IsCyclic.index_powMonoidHom_ker, mul_left_inj', Subgroup.card_mul_index, Nat.mul_div_cancel'
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : IsCyclic G
inst_2 : Finite G
d : ℕ
h : Subgroup.index.{u_2} (G := G) (MonoidHom.ker (M := G) (powMonoidHom d)) ≠ 0
⊢ (Nat.card G).gcd d ∣ Nat.card G

Tactic:
Nat.gcd_dvd_left (Nat.card G) d

Premises used: Nat.gcd_dvd_left, Nat.card
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : IsCyclic G
inst_2 : Finite G
d : ℕ
h : Subgroup.index.{u_2} (G := G) (MonoidHom.ker (M := G) (powMonoidHom d)) ≠ 0
⊢ (Nat.card G).gcd d ∣ Nat.card G

Tactic:
exact Nat.gcd_dvd_left (Nat.card G) d

Premises used: Nat.gcd_dvd_left, Nat.card
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : IsCyclic G
inst_2 : Finite G
d : ℕ
rw : Nat.card.{u_2} ↥(MonoidHom.ker (M := G) (powMonoidHom d)) = (Nat.card G).gcd d
rw₁ rw₂ : (Nat.card G).gcd d = (Nat.card G).gcd d
⊢ Subgroup.index.{u_2} (G := G) (MonoidHom.range (G := G) (powMonoidHom d)) = (Nat.card G).gcd d

Tactic:
rw [Subgroup.index_range, card_powMonoidHom_ker]

Premises used: IsCyclic.card_powMonoidHom_ker, Subgroup.index_range
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst : Group G
inst_1 : Group G'
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (zpowers g) x
g' : G'
hg' : orderOf g' ∣ orderOf g
x y : G
simp :
  Classical.choose (p := fun (x_1 : ℤ) ↦ g ^ x_1 = x * y) ⋯ ≡
    Classical.choose (p := fun (x_1 : ℤ) ↦ g ^ x_1 = x) ⋯ + Classical.choose (p := fun (x : ℤ) ↦ g ^ x = y) ⋯ [ZMOD
    (↑(orderOf g') : ℤ)]
⊢ g' ^ Classical.choose (p := fun (x_1 : ℤ) ↦ g ^ x_1 = x * y) ⋯ =
    g' ^ Classical.choose (p := fun (x_1 : ℤ) ↦ g ^ x_1 = x) ⋯ * g' ^ Classical.choose (p := fun (x : ℤ) ↦ g ^ x = y) ⋯

Tactic:
simp only [← zpow_add, zpow_eq_zpow_iff_modEq]

Premises used: zpow_add, zpow_eq_zpow_iff_modEq
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst : Group G
inst_1 : Group G'
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (zpowers g) x
g' : G'
hg' : orderOf g' ∣ orderOf g
x y : G
apply :
  Classical.choose (p := fun (x_1 : ℤ) ↦ g ^ x_1 = x * y) ⋯ ≡
    Classical.choose (p := fun (x_1 : ℤ) ↦ g ^ x_1 = x) ⋯ + Classical.choose (p := fun (x : ℤ) ↦ g ^ x = y) ⋯ [ZMOD
    (↑(orderOf g) : ℤ)]
⊢ Classical.choose (p := fun (x_1 : ℤ) ↦ g ^ x_1 = x * y) ⋯ ≡
    Classical.choose (p := fun (x_1 : ℤ) ↦ g ^ x_1 = x) ⋯ + Classical.choose (p := fun (x : ℤ) ↦ g ^ x = y) ⋯ [ZMOD
    (↑(orderOf g') : ℤ)]

Tactic:
apply Int.ModEq.of_dvd (Int.natCast_dvd_natCast.mpr hg')

Premises used: Iff.mpr, Int.ModEq.of_dvd, Int.natCast_dvd_natCast
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst : Group G
inst_1 : Group G'
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (zpowers g) x
g' : G'
hg' : orderOf g' ∣ orderOf g
x y : G
rw :
  g ^ Classical.choose (p := fun (x_1 : ℤ) ↦ g ^ x_1 = x * y) ⋯ =
    g ^ Classical.choose (p := fun (x_1 : ℤ) ↦ g ^ x_1 = x) ⋯ * g ^ Classical.choose (p := fun (x : ℤ) ↦ g ^ x = y) ⋯
⊢ Classical.choose (p := fun (x_1 : ℤ) ↦ g ^ x_1 = x * y) ⋯ ≡
    Classical.choose (p := fun (x_1 : ℤ) ↦ g ^ x_1 = x) ⋯ + Classical.choose (p := fun (x : ℤ) ↦ g ^ x = y) ⋯ [ZMOD
    (↑(orderOf g) : ℤ)]

Tactic:
rw [← zpow_eq_zpow_iff_modEq, zpow_add]

Premises used: zpow_add, zpow_eq_zpow_iff_modEq
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst : Group G
inst_1 : Group G'
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (zpowers g) x
g' : G'
hg' : orderOf g' ∣ orderOf g
x y : G
⊢ g ^ Classical.choose (p := fun (x_1 : ℤ) ↦ g ^ x_1 = x * y) ⋯ =
    g ^ Classical.choose (p := fun (x_1 : ℤ) ↦ g ^ x_1 = x) ⋯ * g ^ Classical.choose (p := fun (x : ℤ) ↦ g ^ x = y) ⋯

Tactic:
simp only [fun x ↦ Classical.choose_spec <| mem_zpowers_iff.mp <| hg x]

Premises used: Classical.choose_spec, Iff.mp, Subgroup.mem_zpowers_iff
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
G : Type u_2
G' : Type u_3
inst : Group G
inst_1 : Group G'
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (zpowers g) x
g' : G'
hg' : orderOf g' ∣ orderOf g
simp : g' ^ Classical.choose (p := fun (x : ℤ) ↦ g ^ x = g) ⋯ = g'
⊢ (monoidHomOfForallMemZpowers hg hg' : (a : G) → G') g = g'

Tactic:
simp only [monoidHomOfForallMemZpowers, MonoidHom.coe_mk, OneHom.coe_mk]

Premises used: monoidHomOfForallMemZpowers, OneHom.coe_mk, MonoidHom.coe_mk
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
G : Type u_2
G' : Type u_3
inst : Group G
inst_1 : Group G'
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (zpowers g) x
g' : G'
hg' : orderOf g' ∣ orderOf g
nth_rw : g' ^ Classical.choose (p := fun (x : ℤ) ↦ g ^ x = g) ⋯ = HPow.hPow (β := ℤ) g' 1
⊢ g' ^ Classical.choose (p := fun (x : ℤ) ↦ g ^ x = g) ⋯ = g'

Tactic:
nth_rw 2 [← zpow_one g']

Premises used: zpow_one
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
G : Type u_2
G' : Type u_3
inst : Group G
inst_1 : Group G'
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (zpowers g) x
g' : G'
hg' : orderOf g' ∣ orderOf g
rw : Classical.choose (p := fun (x : ℤ) ↦ g ^ x = g) ⋯ ≡ 1 [ZMOD (↑(orderOf g') : ℤ)]
⊢ g' ^ Classical.choose (p := fun (x : ℤ) ↦ g ^ x = g) ⋯ = HPow.hPow (β := ℤ) g' 1

Tactic:
rw [zpow_eq_zpow_iff_modEq]

Premises used: zpow_eq_zpow_iff_modEq
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
G : Type u_2
G' : Type u_3
inst : Group G
inst_1 : Group G'
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (zpowers g) x
g' : G'
hg' : orderOf g' ∣ orderOf g
apply : Classical.choose (p := fun (x : ℤ) ↦ g ^ x = g) ⋯ ≡ 1 [ZMOD (↑(orderOf g) : ℤ)]
⊢ Classical.choose (p := fun (x : ℤ) ↦ g ^ x = g) ⋯ ≡ 1 [ZMOD (↑(orderOf g') : ℤ)]

Tactic:
apply Int.ModEq.of_dvd (Int.natCast_dvd_natCast.mpr hg')

Premises used: Iff.mpr, Int.ModEq.of_dvd, Int.natCast_dvd_natCast
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
G : Type u_2
G' : Type u_3
inst : Group G
inst_1 : Group G'
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (zpowers g) x
g' : G'
hg' : orderOf g' ∣ orderOf g
rw : g ^ Classical.choose (p := fun (x : ℤ) ↦ g ^ x = g) ⋯ = g
⊢ Classical.choose (p := fun (x : ℤ) ↦ g ^ x = g) ⋯ ≡ 1 [ZMOD (↑(orderOf g) : ℤ)]

Tactic:
rw [← zpow_eq_zpow_iff_modEq, zpow_one]

Premises used: zpow_one, zpow_eq_zpow_iff_modEq
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
G : Type u_2
G' : Type u_3
inst : Group G
inst_1 : Group G'
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (zpowers g) x
g' : G'
hg' : orderOf g' ∣ orderOf g
⊢ g ^ Classical.choose (p := fun (x : ℤ) ↦ g ^ x = g) ⋯ = g

Tactic:
Classical.choose_spec <| mem_zpowers_iff.mp <| hg g

Premises used: Classical.choose_spec, Iff.mp, Subgroup.mem_zpowers_iff
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
G : Type u_2
G' : Type u_3
inst : Group G
inst_1 : Group G'
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (zpowers g) x
g' : G'
hg' : orderOf g' ∣ orderOf g
⊢ g ^ Classical.choose (p := fun (x : ℤ) ↦ g ^ x = g) ⋯ = g

Tactic:
exact Classical.choose_spec <| mem_zpowers_iff.mp <| hg g

Premises used: Classical.choose_spec, Iff.mp, Subgroup.mem_zpowers_iff
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
G : Type u_2
G' : Type u_3
inst : Group G
inst_1 : Group G'
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (zpowers g) x
f₁ f₂ : G →* G'
rw :
  (∀ (x : G), Eq.{u_3 + 1} (α := G') ((f₁ : (a : G) → G') x : G') ((f₂ : (a : G) → G') x : G')) ↔
    Eq.{u_3 + 1} (α := G') ((f₁ : (a : G) → G') g : G') ((f₂ : (a : G) → G') g : G')
⊢ f₁ = f₂ ↔ Eq.{u_3 + 1} (α := G') ((f₁ : (a : G) → G') g : G') ((f₂ : (a : G) → G') g : G')

Tactic:
rw [DFunLike.ext_iff]

Premises used: DFunLike.ext_iff
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
G : Type u_2
G' : Type u_3
inst : Group G
inst_1 : Group G'
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (zpowers g) x
f₁ f₂ : G →* G'
⊢ (∀ (x : G), Eq.{u_3 + 1} (α := G') ((f₁ : (a : G) → G') x : G') ((f₂ : (a : G) → G') x : G')) ↔
    Eq.{u_3 + 1} (α := G') ((f₁ : (a : G) → G') g : G') ((f₂ : (a : G) → G') g : G')

Tactic:
⟨fun H ↦ H g, fun H x ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
G : Type u_2
G' : Type u_3
inst : Group G
inst_1 : Group G'
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (zpowers g) x
f₁ f₂ : G →* G'
refine :
  ∀ (H : Eq.{u_3 + 1} (α := G') ((f₁ : (a : G) → G') g : G') ((f₂ : (a : G) → G') g : G')) (x : G),
    Eq.{u_3 + 1} (α := G') ((f₁ : (a : G) → G') x : G') ((f₂ : (a : G) → G') x : G')
⊢ (∀ (x : G), Eq.{u_3 + 1} (α := G') ((f₁ : (a : G) → G') x : G') ((f₂ : (a : G) → G') x : G')) ↔
    Eq.{u_3 + 1} (α := G') ((f₁ : (a : G) → G') g : G') ((f₂ : (a : G) → G') g : G')

Tactic:
refine ⟨fun H ↦ H g, fun H x ↦ ?_⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
G : Type u_2
G' : Type u_3
inst : Group G
inst_1 : Group G'
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (zpowers g) x
f₁ f₂ : G →* G'
H : Eq.{u_3 + 1} (α := G') ((f₁ : (a : G) → G') g : G') ((f₂ : (a : G) → G') g : G')
x : G
obtain : ∀ (n : ℤ) (hn : g ^ n = x), Eq.{u_3 + 1} (α := G') ((f₁ : (a : G) → G') x : G') ((f₂ : (a : G) → G') x : G')
⊢ Eq.{u_3 + 1} (α := G') ((f₁ : (a : G) → G') x : G') ((f₂ : (a : G) → G') x : G')

Tactic:
obtain ⟨n, hn⟩ := mem_zpowers_iff.mp <| hg x

Premises used: Iff.mp, Subgroup.mem_zpowers_iff
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
G : Type u_2
G' : Type u_3
inst : Group G
inst_1 : Group G'
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (zpowers g) x
f₁ f₂ : G →* G'
H : Eq.{u_3 + 1} (α := G') ((f₁ : (a : G) → G') g : G') ((f₂ : (a : G) → G') g : G')
x : G
n : ℤ
hn : g ^ n = x
rw : Eq.{u_3 + 1} (α := G') ((f₁ : (a : G) → G') (g ^ n) : G') ((f₂ : (a : G) → G') (g ^ n) : G')
rw₁ : HPow.hPow (α := G') ((f₁ : (a : G) → G') g : G') n = (f₂ : (a : G) → G') (g ^ n)
rw₂ : HPow.hPow (α := G') ((f₁ : (a : G) → G') g : G') n = HPow.hPow (α := G') ((f₂ : (a : G) → G') g : G') n
rw₃ rw₄ : HPow.hPow (α := G') ((f₂ : (a : G) → G') g : G') n = HPow.hPow (α := G') ((f₂ : (a : G) → G') g : G') n
⊢ Eq.{u_3 + 1} (α := G') ((f₁ : (a : G) → G') x : G') ((f₂ : (a : G) → G') x : G')

Tactic:
rw [← hn, map_zpow, map_zpow, H]

Premises used: map_zpow
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
G : Type u_2
G' : Type u_3
inst : Group G
inst_1 : Group G'
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (zpowers g) x
f₁ f₂ : G ≃* G'
⊢ f₁ = f₂ ↔ Eq.{u_3 + 1} (α := G') ((f₁ : (a : G) → G') g : G') ((f₂ : (a : G) → G') g : G')

Tactic:
(Function.Injective.eq_iff toMonoidHom_injective).symm.trans <|
    MonoidHom.eq_iff_eq_on_generator hg ..

Premises used: Function.Injective.eq_iff, MonoidHom.eq_iff_eq_on_generator, MulEquiv.toMonoidHom_injective, Iff.trans, Iff.symm
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst : Group G
inst_1 : Group G'
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (zpowers g) x
g' : G'
hg' : ∀ (x : G'), Membership.mem (γ := Subgroup G') (zpowers g') x
h : orderOf g = orderOf g'
⊢ (monoidHomOfForallMemZpowers hg' ⋯).comp (monoidHomOfForallMemZpowers hg ⋯) = MonoidHom.id G

Tactic:
simp [MonoidHom.eq_iff_eq_on_generator hg]

Premises used: MonoidHom.eq_iff_eq_on_generator
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst : Group G
inst_1 : Group G'
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (zpowers g) x
g' : G'
hg' : ∀ (x : G'), Membership.mem (γ := Subgroup G') (zpowers g') x
h : orderOf g = orderOf g'
⊢ (monoidHomOfForallMemZpowers hg ⋯).comp (monoidHomOfForallMemZpowers hg' ⋯) = MonoidHom.id G'

Tactic:
simp [MonoidHom.eq_iff_eq_on_generator hg']

Premises used: MonoidHom.eq_iff_eq_on_generator
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
G : Type u_2
G' : Type u_3
inst : Group G
inst_1 : Group G'
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (zpowers g) x
g' : G'
hg' : ∀ (x : G'), Membership.mem (γ := Subgroup G') (zpowers g') x
h : orderOf g = orderOf g'
⊢ (mulEquivOfOrderOfEq hg hg' h : (a : G) → G') g = g'

Tactic:
monoidHomOfForallMemZpowers_apply_gen hg h.symm.dvd

Premises used: monoidHomOfForallMemZpowers_apply_gen, Eq.dvd, Eq.symm
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
G : Type u_2
G' : Type u_3
inst : Group G
inst_1 : Group G'
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (zpowers g) x
g' : G'
hg' : ∀ (x : G'), Membership.mem (γ := Subgroup G') (zpowers g') x
h : orderOf g = orderOf g'
⊢ (mulEquivOfOrderOfEq hg hg' h).symm = mulEquivOfOrderOfEq hg' hg ⋯

Tactic:
rfl

Premises used: MonoidHom.toMulEquiv, mulEquivOfOrderOfEq, Equiv.symm, MulEquiv.symm, rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
G : Type u_2
G' : Type u_3
inst : Group G
inst_1 : Group G'
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (zpowers g) x
g' : G'
hg' : ∀ (x : G'), Membership.mem (γ := Subgroup G') (zpowers g') x
h : orderOf g = orderOf g'
⊢ ((mulEquivOfOrderOfEq hg hg' h).symm : (a : G') → G) g' = g

Tactic:
monoidHomOfForallMemZpowers_apply_gen hg' h.dvd

Premises used: monoidHomOfForallMemZpowers_apply_gen, Eq.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
inl : Infinite.{u_4 + 1} ↥f.ker → IsCyclic M
inr : Finite.{u_4 + 1} ↥f.ker → IsCyclic M
⊢ IsCyclic M

Tactic:
cases (finite_or_infinite f.ker).symm

Premises used: finite_or_infinite, Membership.mem, Subtype, MonoidHom.ker, Or.symm
-- 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 : Infinite.{u_4 + 1} ↥f.ker
⊢ Nat.card.{u_5} ↥f.range = 1

Tactic:
rw [Nat.card_eq_zero_of_infinite, Nat.coprime_zero_left] at h

Premises used: Nat.card_eq_zero_of_infinite, Nat.coprime_zero_left
-- 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 : Infinite.{u_4 + 1} ↥f.ker
h₁ : Nat.card.{u_5} ↥f.range = 1
⊢ IsCyclic.{u_4} ↥f.ker

Tactic:
rw [Nat.card_eq_zero_of_infinite, Nat.coprime_zero_left] at h

Premises used: Nat.card_eq_zero_of_infinite, Nat.coprime_zero_left
-- 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.{u_5} ↥f.range)
inst_3 : IsCyclic.{u_4} ↥f.ker
inst_4 : IsCyclic.{u_5} ↥f.range
h_1 : Infinite.{u_4 + 1} ↥f.ker
h₁ : Nat.card.{u_5} ↥f.range = 1
inst : IsCyclic.{u_4} ↥f.ker
⊢ IsCyclic.{u_5} ↥f.range

Tactic:
rw [Nat.card_eq_zero_of_infinite, Nat.coprime_zero_left] at h

Premises used: Nat.card_eq_zero_of_infinite, Nat.coprime_zero_left
-- 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.{u_5} ↥f.range)
inst_3 : IsCyclic.{u_4} ↥f.ker
inst_4 : IsCyclic.{u_5} ↥f.range
h_1 : Infinite.{u_4 + 1} ↥f.ker
h₁ : Nat.card.{u_5} ↥f.range = 1
inst : IsCyclic.{u_4} ↥f.ker
inst₁ : IsCyclic.{u_5} ↥f.range
⊢ Infinite.{u_4 + 1} ↥f.ker

Tactic:
rw [Nat.card_eq_zero_of_infinite, Nat.coprime_zero_left] at h

Premises used: Nat.card_eq_zero_of_infinite, Nat.coprime_zero_left
-- 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_5} ↥f.range = 1
inst_2 : IsCyclic.{u_4} ↥f.ker
inst_3 : IsCyclic.{u_5} ↥f.range
h_1 : Infinite.{u_4 + 1} ↥f.ker
⊢ f.ker = ⊤

Tactic:
rw [← f.range.eq_bot_iff_card, f.range_eq_bot_iff, ← f.ker_eq_top_iff] at h

Premises used: MonoidHom.range, MonoidHom.ker_eq_top_iff, Subgroup.eq_bot_iff_card, MonoidHom.range_eq_bot_iff
-- 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_5} ↥f.range = 1
inst_2 : IsCyclic.{u_4} ↥f.ker
inst_3 : IsCyclic.{u_5} ↥f.range
h_1 : Infinite.{u_4 + 1} ↥f.ker
h₁ : f.ker = ⊤
⊢ IsCyclic.{u_4} ↥f.ker

Tactic:
rw [← f.range.eq_bot_iff_card, f.range_eq_bot_iff, ← f.ker_eq_top_iff] at h

Premises used: MonoidHom.range, MonoidHom.ker_eq_top_iff, Subgroup.eq_bot_iff_card, MonoidHom.range_eq_bot_iff
-- 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_5} ↥f.range = 1
inst_3 : IsCyclic.{u_4} ↥f.ker
inst_4 : IsCyclic.{u_5} ↥f.range
h_1 : Infinite.{u_4 + 1} ↥f.ker
h₁ : f.ker = ⊤
inst : IsCyclic.{u_4} ↥f.ker
⊢ IsCyclic.{u_5} ↥f.range

Tactic:
rw [← f.range.eq_bot_iff_card, f.range_eq_bot_iff, ← f.ker_eq_top_iff] at h

Premises used: MonoidHom.range, MonoidHom.ker_eq_top_iff, Subgroup.eq_bot_iff_card, MonoidHom.range_eq_bot_iff
-- 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_5} ↥f.range = 1
inst_3 : IsCyclic.{u_4} ↥f.ker
inst_4 : IsCyclic.{u_5} ↥f.range
h_1 : Infinite.{u_4 + 1} ↥f.ker
h₁ : f.ker = ⊤
inst : IsCyclic.{u_4} ↥f.ker
inst₁ : IsCyclic.{u_5} ↥f.range
⊢ Infinite.{u_4 + 1} ↥f.ker

Tactic:
rw [← f.range.eq_bot_iff_card, f.range_eq_bot_iff, ← f.ker_eq_top_iff] at h

Premises used: MonoidHom.range, MonoidHom.ker_eq_top_iff, Subgroup.eq_bot_iff_card, MonoidHom.range_eq_bot_iff
-- 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 : f.ker = ⊤
inst_2 : IsCyclic.{u_4} ↥f.ker
inst_3 : IsCyclic.{u_5} ↥f.range
h_1 : Infinite.{u_4 + 1} ↥f.ker
inl : IsCyclic.{u_4} ↥⊤
inl₁ inl₂ inl₃ inl₄ : IsCyclic.{u_4} ↥f.ker
⊢ IsCyclic M

Tactic:
rwa [← Subgroup.topEquiv.isCyclic, ← h]

Premises used: 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.{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
inr : Infinite.{u_5 + 1} ↥f.range → IsCyclic M
inr₁ : Finite.{u_5 + 1} ↥f.range → IsCyclic M
⊢ IsCyclic M

Tactic:
cases (finite_or_infinite f.range).symm

Premises used: MonoidHom.range, finite_or_infinite, Membership.mem, Subtype, Or.symm
-- 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 : Infinite.{u_5 + 1} ↥f.range
⊢ Nat.card.{u_4} ↥f.ker = 1

Tactic:
rw [Nat.card_eq_zero_of_infinite (α := f.range), Nat.coprime_zero_right] at h

Premises used: Nat.coprime_zero_right, Nat.card_eq_zero_of_infinite
-- 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 : Infinite.{u_5 + 1} ↥f.range
h₁ : Nat.card.{u_4} ↥f.ker = 1
⊢ IsCyclic.{u_4} ↥f.ker

Tactic:
rw [Nat.card_eq_zero_of_infinite (α := f.range), Nat.coprime_zero_right] at h

Premises used: Nat.coprime_zero_right, Nat.card_eq_zero_of_infinite
-- 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.{u_5} ↥f.range)
inst_3 : IsCyclic.{u_4} ↥f.ker
inst_4 : IsCyclic.{u_5} ↥f.range
h_1 : Finite.{u_4 + 1} ↥f.ker
h_2 : Infinite.{u_5 + 1} ↥f.range
h₁ : Nat.card.{u_4} ↥f.ker = 1
inst : IsCyclic.{u_4} ↥f.ker
⊢ IsCyclic.{u_5} ↥f.range

Tactic:
rw [Nat.card_eq_zero_of_infinite (α := f.range), Nat.coprime_zero_right] at h

Premises used: Nat.coprime_zero_right, Nat.card_eq_zero_of_infinite
-- 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.{u_5} ↥f.range)
inst_3 : IsCyclic.{u_4} ↥f.ker
inst_4 : IsCyclic.{u_5} ↥f.range
h_1 : Finite.{u_4 + 1} ↥f.ker
h_2 : Infinite.{u_5 + 1} ↥f.range
h₁ : Nat.card.{u_4} ↥f.ker = 1
inst : IsCyclic.{u_4} ↥f.ker
inst₁ : IsCyclic.{u_5} ↥f.range
⊢ Finite.{u_4 + 1} ↥f.ker

Tactic:
rw [Nat.card_eq_zero_of_infinite (α := f.range), Nat.coprime_zero_right] at h

Premises used: Nat.coprime_zero_right, Nat.card_eq_zero_of_infinite
-- 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.{u_5} ↥f.range)
inst_3 : IsCyclic.{u_4} ↥f.ker
inst_4 : IsCyclic.{u_5} ↥f.range
h_1 : Finite.{u_4 + 1} ↥f.ker
h_2 : Infinite.{u_5 + 1} ↥f.range
h₁ : Nat.card.{u_4} ↥f.ker = 1
inst : IsCyclic.{u_4} ↥f.ker
inst₁ : IsCyclic.{u_5} ↥f.range
h₂ : Finite.{u_4 + 1} ↥f.ker
⊢ Infinite.{u_5 + 1} ↥f.range

Tactic:
rw [Nat.card_eq_zero_of_infinite (α := f.range), Nat.coprime_zero_right] at h

Premises used: Nat.coprime_zero_right, Nat.card_eq_zero_of_infinite
-- 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 = 1
inst_2 : IsCyclic.{u_4} ↥f.ker
inst_3 : IsCyclic.{u_5} ↥f.range
h_1 : Finite.{u_4 + 1} ↥f.ker
h_2 : Infinite.{u_5 + 1} ↥f.range
inr inr₁ inr₂ inr₃ : IsCyclic.{u_5} ↥f.range
⊢ IsCyclic M

Tactic:
rwa [(f.ofInjective (f.ker_eq_bot_iff.mp (f.ker.eq_bot_of_card_eq h))).isCyclic]

Premises used: MonoidHom.ker, MonoidHom.ker_eq_bot_iff, Iff.mp, Subgroup.eq_bot_of_card_eq, MonoidHom.ofInjective, 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.{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
⊢ Finite M

Tactic:
have := f.finite_iff_finite_ker_range.mpr ⟨‹_›, ‹_›⟩