awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
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) ⋯
have simp : Classical.choose (p := fun (x_1 : ℤ) ↦ g ^ x_1 = x * y) sorry ≡
  Classical.choose (p := fun (x_1 : ℤ) ↦ g ^ x_1 = x) sorry + Classical.choose (p := fun (x : ℤ) ↦ g ^ x = y) sorry [ZMOD
  (↑(orderOf g') : ℤ)]
Tactic: simp only [← zpow_add, zpow_eq_zpow_iff_modEq]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
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
⊢ 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') : ℤ)]
have apply : Classical.choose (p := fun (x_1 : ℤ) ↦ g ^ x_1 = x * y) sorry ≡
  Classical.choose (p := fun (x_1 : ℤ) ↦ g ^ x_1 = x) sorry + Classical.choose (p := fun (x : ℤ) ↦ g ^ x = y) sorry [ZMOD
  (↑(orderOf g) : ℤ)]
Tactic: apply Int.ModEq.of_dvd (Int.natCast_dvd_natCast.mpr hg')
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
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
⊢ 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) : ℤ)]
have rw : g ^ Classical.choose (p := fun (x_1 : ℤ) ↦ g ^ x_1 = x * y) sorry =
  g ^ Classical.choose (p := fun (x_1 : ℤ) ↦ g ^ x_1 = x) sorry * g ^ Classical.choose (p := fun (x : ℤ) ↦ g ^ x = y) sorry
Tactic: rw [← zpow_eq_zpow_iff_modEq, zpow_add]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
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
⊢ (monoidHomOfForallMemZpowers hg hg' : (a : G) → G') g = g'
have simp : g' ^ Classical.choose (p := fun (x : ℤ) ↦ g ^ x = g) sorry = g'
Tactic: simp only [monoidHomOfForallMemZpowers, MonoidHom.coe_mk, OneHom.coe_mk]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
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'
have nth_rw : g' ^ Classical.choose (p := fun (x : ℤ) ↦ g ^ x = g) sorry = HPow.hPow (β := ℤ) g' 1
Tactic: nth_rw 2 [← zpow_one g']
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
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) ⋯ = HPow.hPow (β := ℤ) g' 1
have rw : Classical.choose (p := fun (x : ℤ) ↦ g ^ x = g) sorry ≡ 1 [ZMOD (↑(orderOf g') : ℤ)]
Tactic: rw [zpow_eq_zpow_iff_modEq]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
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
⊢ Classical.choose (p := fun (x : ℤ) ↦ g ^ x = g) ⋯ ≡ 1 [ZMOD (↑(orderOf g') : ℤ)]
have apply : Classical.choose (p := fun (x : ℤ) ↦ g ^ x = g) sorry ≡ 1 [ZMOD (↑(orderOf g) : ℤ)]
Tactic: apply Int.ModEq.of_dvd (Int.natCast_dvd_natCast.mpr hg')
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
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
⊢ Classical.choose (p := fun (x : ℤ) ↦ g ^ x = g) ⋯ ≡ 1 [ZMOD (↑(orderOf g) : ℤ)]
have rw : g ^ Classical.choose (p := fun (x : ℤ) ↦ g ^ x = g) sorry = g
Tactic: rw [← zpow_eq_zpow_iff_modEq, zpow_one]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
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')
have 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')
Tactic: rw [DFunLike.ext_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
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')
have 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')
Tactic: refine ⟨fun H ↦ H g, fun H x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
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
⊢ Eq.{u_3 + 1} (α := G') ((f₁ : (a : G) → G') x : G') ((f₂ : (a : G) → G') x : G')
have obtain : ∀ (n : ℤ) (hn : g ^ n = x), 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
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
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
⊢ Eq.{u_3 + 1} (α := G') ((f₁ : (a : G) → G') x : G') ((f₂ : (a : G) → G') x : G')
have rw : Eq.{u_3 + 1} (α := G') ((f₁ : (a : G) → G') (g ^ n) : G') ((f₂ : (a : G) → G') (g ^ n) : G')
Tactic: rw [← hn, map_zpow, map_zpow, H]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
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')
⊢ Eq.{u_3 + 1} (α := G') ((f₁ : (a : G) → G') x : G') ((f₂ : (a : G) → G') x : G')
have rw₁ : HPow.hPow (α := G') ((f₁ : (a : G) → G') g : G') n = (f₂ : (a : G) → G') (g ^ n)
Tactic: rw [← hn, map_zpow, map_zpow, H]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
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)
⊢ Eq.{u_3 + 1} (α := G') ((f₁ : (a : G) → G') x : G') ((f₂ : (a : G) → G') x : G')
have rw₂ : HPow.hPow (α := G') ((f₁ : (a : G) → G') g : G') n = HPow.hPow (α := G') ((f₂ : (a : G) → G') g : G') n
Tactic: rw [← hn, map_zpow, map_zpow, H]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
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
⊢ Eq.{u_3 + 1} (α := G') ((f₁ : (a : G) → G') x : G') ((f₂ : (a : G) → G') x : G')
have rw₃ : HPow.hPow (α := G') ((f₂ : (a : G) → G') g : G') n = HPow.hPow (α := G') ((f₂ : (a : G) → G') g : G') n
Tactic: rw [← hn, map_zpow, map_zpow, H]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
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
⊢ IsCyclic M
have inl : Infinite.{u_4 + 1} ↥f.ker → IsCyclic M
Tactic: cases (finite_or_infinite f.ker).symm
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
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
⊢ IsCyclic M
have inr : Finite.{u_4 + 1} ↥f.ker → IsCyclic M
Tactic: cases (finite_or_infinite f.ker).symm
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (hypothesis)
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
⊢ IsCyclic M
have h₁ : Nat.card.{u_5} ↥f.range = 1
Tactic: rw [Nat.card_eq_zero_of_infinite, Nat.coprime_zero_left] at h
Cleared hypotheses: h, inst_2, inst_3, h_1
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (hypothesis)
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
⊢ IsCyclic M
have h₁ : f.ker = ⊤
Tactic: rw [← f.range.eq_bot_iff_card, f.range_eq_bot_iff, ← f.ker_eq_top_iff] at h
Cleared hypotheses: h, inst_2, inst_3, h_1
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
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
⊢ IsCyclic M
have inl : IsCyclic.{u_4} ↥⊤
Tactic: rwa [← Subgroup.topEquiv.isCyclic, ← h]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
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
⊢ IsCyclic M
have inr : Infinite.{u_5 + 1} ↥f.range → IsCyclic M
Tactic: cases (finite_or_infinite f.range).symm
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
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
⊢ IsCyclic M
have inr₁ : Finite.{u_5 + 1} ↥f.range → IsCyclic M
Tactic: cases (finite_or_infinite f.range).symm
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (hypothesis)
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
⊢ IsCyclic M
have h₁ : Nat.card.{u_4} ↥f.ker = 1
Tactic: rw [Nat.card_eq_zero_of_infinite (α := f.range), Nat.coprime_zero_right] at h
Cleared hypotheses: h, inst_2, inst_3, h_1, h_2
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (hypothesis)
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
⊢ IsCyclic M
have this : Finite M
Tactic: have := f.finite_iff_finite_ker_range.mpr ⟨‹_›, ‹_›⟩
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
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
⊢ IsCyclic M
have inr : Monoid.exponent M = Nat.card M
Tactic: rw [IsCyclic.iff_exponent_eq_card]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
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 M = Nat.card M
have inr : Nat.card M ∣ Monoid.exponent M
Tactic: apply dvd_antisymm Group.exponent_dvd_nat_card
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
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
⊢ Nat.card M ∣ Monoid.exponent M
have inr : Nat.card.{u_4} ↥f.ker * Nat.card.{u_5} ↥f.range ∣ Monoid.exponent M
Tactic: rw [← f.ker.card_mul_index, Subgroup.index_ker]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
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
⊢ Nat.card.{u_4} ↥f.ker * Nat.card.{u_5} ↥f.range ∣ Monoid.exponent M
have inr : Nat.card.{u_4} ↥f.ker ∣ Monoid.exponent M
Tactic: apply h.mul_dvd_of_dvd_of_dvd
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
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
⊢ Nat.card.{u_4} ↥f.ker * Nat.card.{u_5} ↥f.range ∣ Monoid.exponent M
have inr₁ : Nat.card.{u_5} ↥f.range ∣ Monoid.exponent M
Tactic: apply h.mul_dvd_of_dvd_of_dvd
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
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
⊢ Nat.card.{u_4} ↥f.ker ∣ Monoid.exponent M
have inr : Monoid.exponent.{u_4} ↥f.ker ∣ Monoid.exponent M
Tactic: rw [← IsCyclic.exponent_eq_card]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
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
⊢ Nat.card.{u_5} ↥f.range ∣ Monoid.exponent M
have inr : Monoid.exponent.{u_5} ↥f.range ∣ Monoid.exponent M
Tactic: rw [← IsCyclic.exponent_eq_card]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (hypothesis)
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 M
have hN₁ : IsCyclic.{u_5} ↥f.range
Tactic: rw [← Subgroup.topEquiv.isCyclic, ← f.range_eq_top.mpr hf] at hN
Cleared hypotheses: hN, hf
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (hypothesis)
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)
⊢ IsCyclic M
have h₁ : (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
Cleared hypotheses: h, inst_2, hN, hf
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (hypothesis)
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
⊢ (Nat.card M).Coprime (Nat.card N)
have hM : IsCyclic M
Tactic: have hM := isCyclic_left_of_prod M N
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (hypothesis)
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
⊢ (Nat.card M).Coprime (Nat.card N)
have hN : IsCyclic N
Tactic: have hN := isCyclic_right_of_prod M N
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (hypothesis)
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
⊢ (Nat.card M).Coprime (Nat.card N)
have cyc₁ : (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 *
Cleared hypotheses: x_1, x_2
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (hypothesis)
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
⊢ (Nat.card M).Coprime (Nat.card N)
have hM₁ : 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 *
Cleared hypotheses: x_1, x_2
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (hypothesis)
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
⊢ (Nat.card M).Coprime (Nat.card N)
have hN₁ : 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 *
Cleared hypotheses: x_1, x_2
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (hypothesis)
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)
⊢ False
have hMN₁ : 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
Cleared hypotheses: hMN
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
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))
⊢ False
have inl : Infinite N → False
Tactic: cases (finite_or_infinite N).symm
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
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
⊢ False
have inr : Finite N → False
Tactic: cases (finite_or_infinite N).symm
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (hypothesis)
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
⊢ False
have hMN₁ : IsAddCyclic (ZMod 0 × ZMod 0)
Tactic: rw [Nat.card_eq_zero_of_infinite] at hMN
Cleared hypotheses: hMN, h
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (hypothesis)
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))
⊢ False
have hf : Function.Surjective (α := ZMod 0) (β := ZMod 2) (⇑(ZMod.castHom sorry (ZMod 2)) : (a : ZMod 0) → ZMod 2)
Tactic: have hf := ZMod.castHom_surjective (dvd_zero 2)
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (hypothesis)
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)
⊢ False
have this : IsAddCyclic (ZMod 2 × ZMod 2)
Tactic: have := isAddCyclic_of_surjective (f.prodMap f) (Prod.map_surjective.mpr ⟨hf, hf⟩)
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (hypothesis)
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)
⊢ False
have this : NeZero (Nat.card N)
Tactic: have : NeZero (Nat.card N) := ⟨Nat.card_pos.ne'⟩
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (hypothesis)
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)
⊢ False
have this₁ : 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⟩)
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
M : Type u_4
N : Type u_5
inst : Group M
inst_1 : Group N
inst_2 : Infinite M
inst_3 : Nontrivial N
⊢ ¬IsCyclic (M × N)
have rw : ¬IsAddCyclic (Prod.{u_4, u_5} (Additive M) (Additive N))
Tactic: rw [← isAddCyclic_additive_iff, (AddEquiv.prodAdditive ..).isAddCyclic]