awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
H : Subgroup G
h_1 : H ≠ ⊥
hH : IsCyclic.{u_1} ↥(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H))
x : CommGroup (MulAut ↥(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H))) :=
  MonoidHom.commGroupOfInjective
    (MulEquiv.toMonoidHom
      (IsCyclic.mulAutMulEquiv ↥(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H))))
    ⋯
h :
  LE.le.{u_1} (α :=
    Subgroup ↥(Subgroup.normalizer (↑(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H)) : Set ↥H)))
    (commutator ↥(Subgroup.normalizer (↑(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H)) : Set ↥H)))
    (MonoidHom.ker (Subgroup.normalizerMonoidHom (Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H))))
ind :
  ∀
    (h :
      LE.le (α :=
        Subgroup
          ↥(Subgroup.normalizer (↑(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H)) : Set ↥H)))
        (commutator
          ↥(Subgroup.normalizer (↑(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H)) : Set ↥H)))
        (Subgroup.subgroupOf
          (Subgroup.centralizer (↑(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H)) : Set ↥H))
          (Subgroup.normalizer (↑(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H)) : Set ↥H)))),
    LE.le (α := Subgroup ↥H) (commutator ↥H)
      (Subgroup.centralizer (↑(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H)) : Set ↥H))
ind₁ :
  ∀
    (h :
      LE.le (α := Subgroup ↥⊤) (commutator ↥⊤)
        (Subgroup.subgroupOf
          (Subgroup.centralizer (↑(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H)) : Set ↥H)) ⊤)),
    LE.le (α := Subgroup ↥H) (commutator ↥H)
      (Subgroup.centralizer (↑(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H)) : Set ↥H))
⊢ LE.le (α := Subgroup ↥H) (commutator ↥H)
    (Subgroup.centralizer (↑(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H)) : Set ↥H))
have ind₂ : ∀
  (h :
    LE.le (α := Subgroup ↥H) (Subgroup.map (G := ↥⊤) (Subgroup.subtype ⊤) (commutator ↥⊤))
      (Subgroup.map (G := ↥⊤) (Subgroup.subtype ⊤)
        (Subgroup.subgroupOf
          (Subgroup.centralizer (↑(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H)) : Set ↥H)) ⊤))),
  LE.le (α := Subgroup ↥H) (commutator ↥H)
    (Subgroup.centralizer (↑(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H)) : Set ↥H))
Tactic: rwa [Subgroup.normalizerMonoidHom_ker, Subgroup.normalizer_eq_top,
      ← Subgroup.map_subtype_le_map_subtype, Subgroup.map_subtype_commutator,
        Subgroup.map_subgroupOf_eq_of_le le_top] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : IsCyclic G
hG : IsPGroup p G
K : Type u_4
inst_3 : Group K
inst_4 : MulDistribMulAction K G
hGK : (Nat.card G).Coprime (Nat.card K)
⊢ (∀ (g : G) (k : K), k • g * g⁻¹ = 1) ∨ ∀ (g : G), ∃ (k : K) (q : G), k • q * q⁻¹ = g
have pos : ∀ (hc : Nat.card G = 0), (∀ (g : G) (k : K), k • g * g⁻¹ = 1) ∨ ∀ (g : G), ∃ (k : K) (q : G), k • q * q⁻¹ = g
Tactic: by_cases hc : Nat.card G = 0
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : IsCyclic G
hG : IsPGroup p G
K : Type u_4
inst_3 : Group K
inst_4 : MulDistribMulAction K G
hGK : (Nat.card G).Coprime (Nat.card K)
pos : ∀ (hc : Nat.card G = 0), (∀ (g : G) (k : K), k • g * g⁻¹ = 1) ∨ ∀ (g : G), ∃ (k : K) (q : G), k • q * q⁻¹ = g
⊢ (∀ (g : G) (k : K), k • g * g⁻¹ = 1) ∨ ∀ (g : G), ∃ (k : K) (q : G), k • q * q⁻¹ = g
have neg : ∀ (hc : ¬Nat.card G = 0), (∀ (g : G) (k : K), k • g * g⁻¹ = 1) ∨ ∀ (g : G), ∃ (k : K) (q : G), k • q * q⁻¹ = g
Tactic: by_cases hc : Nat.card G = 0
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (hypothesis)
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : IsCyclic G
hG : IsPGroup p G
K : Type u_4
inst_3 : Group K
inst_4 : MulDistribMulAction K G
hGK : (Nat.card G).Coprime (Nat.card K)
hc : Nat.card G = 0
⊢ (∀ (g : G) (k : K), k • g * g⁻¹ = 1) ∨ ∀ (g : G), ∃ (k : K) (q : G), k • q * q⁻¹ = g
have hGK₁ : Subsingleton K ∧ Nonempty K
Tactic: rw [hc, Nat.coprime_zero_left, Nat.card_eq_one_iff_unique] at hGK
Cleared hypotheses: hGK, hc
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (hypothesis)
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : IsCyclic G
hG : IsPGroup p G
K : Type u_4
inst_3 : Group K
inst_4 : MulDistribMulAction K G
hGK : (Nat.card G).Coprime (Nat.card K)
hc : ¬Nat.card G = 0
⊢ (∀ (g : G) (k : K), k • g * g⁻¹ = 1) ∨ ∀ (g : G), ∃ (k : K) (q : G), k • q * q⁻¹ = g
have this : Finite G
Tactic: have := Nat.finite_of_card_ne_zero hc
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (hypothesis)
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : IsCyclic G
hG : IsPGroup p G
K : Type u_4
inst_3 : Group K
inst_4 : MulDistribMulAction K G
hGK : (Nat.card G).Coprime (Nat.card K)
hc : ¬Nat.card G = 0
this : Finite G
ϕ : K →* ZMod (Nat.card G) := MulDistribMulAction.toMonoidHomZModOfIsCyclic G K ⋯
g : G
k : K
n : ℤ
h :
  HSub.hSub (α := ZMod (Nat.card G)) (β := ZMod (Nat.card G)) ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G))
      (1 : ZMod (Nat.card G)) =
    (↑n : ZMod (Nat.card G))
⊢ k • g * g⁻¹ = g ^ n
have h₁ : Eq (α := ZMod (Nat.card G)) ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G))
  ((↑(n + 1) : ZMod (Nat.card G)) : ZMod (Nat.card G))
Tactic: rw [sub_eq_iff_eq_add, ← Int.cast_one, ← Int.cast_add] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : IsCyclic G
hG : IsPGroup p G
K : Type u_4
inst_3 : Group K
inst_4 : MulDistribMulAction K G
hGK : (Nat.card G).Coprime (Nat.card K)
hc : ¬Nat.card G = 0
this : Finite G
ϕ : K →* ZMod (Nat.card G) := MulDistribMulAction.toMonoidHomZModOfIsCyclic G K ⋯
g : G
k : K
n : ℤ
h :
  Eq (α := ZMod (Nat.card G)) ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G))
    ((↑(n + 1) : ZMod (Nat.card G)) : ZMod (Nat.card G))
⊢ k • g * g⁻¹ = g ^ n
have rw : g ^ (n + 1) * g⁻¹ = g ^ n
Tactic: rw [MulDistribMulAction.toMonoidHomZModOfIsCyclic_apply rfl k g (n + 1) h,
      zpow_add_one, mul_inv_cancel_right]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : IsCyclic G
hG : IsPGroup p G
K : Type u_4
inst_3 : Group K
inst_4 : MulDistribMulAction K G
hGK : (Nat.card G).Coprime (Nat.card K)
hc : ¬Nat.card G = 0
this : Finite G
ϕ : K →* ZMod (Nat.card G) := MulDistribMulAction.toMonoidHomZModOfIsCyclic G K ⋯
g : G
k : K
n : ℤ
h :
  Eq (α := ZMod (Nat.card G)) ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G))
    ((↑(n + 1) : ZMod (Nat.card G)) : ZMod (Nat.card G))
rw : g ^ (n + 1) * g⁻¹ = g ^ n
⊢ k • g * g⁻¹ = g ^ n
have rw₁ : g ^ n * g * g⁻¹ = g ^ n
Tactic: rw [MulDistribMulAction.toMonoidHomZModOfIsCyclic_apply rfl k g (n + 1) h,
      zpow_add_one, mul_inv_cancel_right]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : IsCyclic G
hG : IsPGroup p G
K : Type u_4
inst_3 : Group K
inst_4 : MulDistribMulAction K G
hGK : (Nat.card G).Coprime (Nat.card K)
hc : ¬Nat.card G = 0
this : Finite G
ϕ : K →* ZMod (Nat.card G) := MulDistribMulAction.toMonoidHomZModOfIsCyclic G K ⋯
g : G
k : K
n : ℤ
h :
  Eq (α := ZMod (Nat.card G)) ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G))
    ((↑(n + 1) : ZMod (Nat.card G)) : ZMod (Nat.card G))
rw : g ^ (n + 1) * g⁻¹ = g ^ n
rw₁ : g ^ n * g * g⁻¹ = g ^ n
⊢ k • g * g⁻¹ = g ^ n
have rw₂ : g ^ n = g ^ n
Tactic: rw [MulDistribMulAction.toMonoidHomZModOfIsCyclic_apply rfl k g (n + 1) h,
      zpow_add_one, mul_inv_cancel_right]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (hypothesis)
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : IsCyclic G
hG : IsPGroup p G
K : Type u_4
inst_3 : Group K
inst_4 : MulDistribMulAction K G
hGK : (Nat.card G).Coprime (Nat.card K)
hc : ¬Nat.card G = 0
this : Finite G
ϕ : K →* ZMod (Nat.card G) := MulDistribMulAction.toMonoidHomZModOfIsCyclic G K ⋯
⊢ (∀ (g : G) (k : K), k • g * g⁻¹ = 1) ∨ ∀ (g : G), ∃ (k : K) (q : G), k • q * q⁻¹ = g
have h : ∀ (g : G) (k : K) (n : ℤ)
  (h :
    HSub.hSub (α := ZMod (Nat.card G)) (β := ZMod (Nat.card G))
        ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G)) =
      (↑n : ZMod (Nat.card G))),
  k • g * g⁻¹ = g ^ n
Tactic: have h (g : G) (k : K) (n : ℤ) (h : ϕ k - 1 = n) : k • g * g⁻¹ = g ^ n := by
    rw [sub_eq_iff_eq_add, ← Int.cast_one, ← Int.cast_add] at h
    rw [MulDistribMulAction.toMonoidHomZModOfIsCyclic_apply rfl k g (n + 1) h,
      zpow_add_one, mul_inv_cancel_right]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : IsCyclic G
hG : IsPGroup p G
K : Type u_4
inst_3 : Group K
inst_4 : MulDistribMulAction K G
hGK : (Nat.card G).Coprime (Nat.card K)
hc : ¬Nat.card G = 0
this : Finite G
ϕ : K →* ZMod (Nat.card G) := MulDistribMulAction.toMonoidHomZModOfIsCyclic G K ⋯
h :
  ∀ (g : G) (k : K) (n : ℤ)
    (h :
      HSub.hSub (α := ZMod (Nat.card G)) (β := ZMod (Nat.card G))
          ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G)) =
        (↑n : ZMod (Nat.card G))),
    k • g * g⁻¹ = g ^ n
k : K
⊢ Eq (α := ZMod (Nat.card G)) ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G)) ∨
    IsUnit
      (HSub.hSub (α := ZMod (Nat.card G)) (β := ZMod (Nat.card G))
        ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G)))
have obtain : ∀ (n : ℕ) (hn : Nat.card G = p ^ n),
  Eq (α := ZMod (Nat.card G)) ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G)) ∨
    IsUnit
      (HSub.hSub (α := ZMod (Nat.card G)) (β := ZMod (Nat.card G))
        ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G)))
Tactic: obtain ⟨n, hn⟩ := hG.exists_card_eq
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (hypothesis)
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : IsCyclic G
hG : IsPGroup p G
K : Type u_4
inst_3 : Group K
inst_4 : MulDistribMulAction K G
hGK : (Nat.card G).Coprime (Nat.card K)
hc : ¬Nat.card G = 0
this : Finite G
ϕ : K →* ZMod (Nat.card G) := MulDistribMulAction.toMonoidHomZModOfIsCyclic G K ⋯
h :
  ∀ (g : G) (k : K) (n : ℤ)
    (h :
      HSub.hSub (α := ZMod (Nat.card G)) (β := ZMod (Nat.card G))
          ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G)) =
        (↑n : ZMod (Nat.card G))),
    k • g * g⁻¹ = g ^ n
⊢ (∀ (g : G) (k : K), k • g * g⁻¹ = 1) ∨ ∀ (g : G), ∃ (k : K) (q : G), k • q * q⁻¹ = g
have hG₁ : ∀ (k : K),
  Eq (α := ZMod (Nat.card G)) ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G)) ∨
    IsUnit
      (HSub.hSub (α := ZMod (Nat.card G)) (β := ZMod (Nat.card G))
        ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G)))
Tactic: replace hG k : ϕ k = 1 ∨ IsUnit (ϕ k - 1) := by
    obtain ⟨n, hn⟩ := hG.exists_card_eq
    exact ZMod.eq_one_or_isUnit_sub_one hn (ϕ k)
      (hGK.symm.coprime_dvd_left ((orderOf_map_dvd ϕ k).trans (orderOf_dvd_natCard k)))
Cleared hypotheses: hG
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : IsCyclic G
K : Type u_4
inst_3 : Group K
inst_4 : MulDistribMulAction K G
hGK : (Nat.card G).Coprime (Nat.card K)
hc : ¬Nat.card G = 0
this : Finite G
ϕ : K →* ZMod (Nat.card G) := MulDistribMulAction.toMonoidHomZModOfIsCyclic G K ⋯
h :
  ∀ (g : G) (k : K) (n : ℤ)
    (h :
      HSub.hSub (α := ZMod (Nat.card G)) (β := ZMod (Nat.card G))
          ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G)) =
        (↑n : ZMod (Nat.card G))),
    k • g * g⁻¹ = g ^ n
hG :
  ∀ (k : K),
    Eq (α := ZMod (Nat.card G)) ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G)) ∨
      IsUnit
        (HSub.hSub (α := ZMod (Nat.card G)) (β := ZMod (Nat.card G))
          ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G)))
⊢ (∀ (g : G) (k : K), k • g * g⁻¹ = 1) ∨ ∀ (g : G), ∃ (k : K) (q : G), k • q * q⁻¹ = g
have neg : ∀
  (hϕ :
    ∀ (a : K),
      Eq (α := ZMod (Nat.card G)) ((ϕ : (a : K) → ZMod (Nat.card G)) a : ZMod (Nat.card G)) (1 : ZMod (Nat.card G))),
  (∀ (g : G) (k : K), k • g * g⁻¹ = 1) ∨ ∀ (g : G), ∃ (k : K) (q : G), k • q * q⁻¹ = g
Tactic: rcases forall_or_exists_not (fun k : K ↦ ϕ k = 1) with hϕ | ⟨k, hk⟩
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : IsCyclic G
K : Type u_4
inst_3 : Group K
inst_4 : MulDistribMulAction K G
hGK : (Nat.card G).Coprime (Nat.card K)
hc : ¬Nat.card G = 0
this : Finite G
ϕ : K →* ZMod (Nat.card G) := MulDistribMulAction.toMonoidHomZModOfIsCyclic G K ⋯
h :
  ∀ (g : G) (k : K) (n : ℤ)
    (h :
      HSub.hSub (α := ZMod (Nat.card G)) (β := ZMod (Nat.card G))
          ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G)) =
        (↑n : ZMod (Nat.card G))),
    k • g * g⁻¹ = g ^ n
hG :
  ∀ (k : K),
    Eq (α := ZMod (Nat.card G)) ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G)) ∨
      IsUnit
        (HSub.hSub (α := ZMod (Nat.card G)) (β := ZMod (Nat.card G))
          ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G)))
neg :
  ∀
    (hϕ :
      ∀ (a : K),
        Eq (α := ZMod (Nat.card G)) ((ϕ : (a : K) → ZMod (Nat.card G)) a : ZMod (Nat.card G)) (1 : ZMod (Nat.card G))),
    (∀ (g : G) (k : K), k • g * g⁻¹ = 1) ∨ ∀ (g : G), ∃ (k : K) (q : G), k • q * q⁻¹ = g
⊢ (∀ (g : G) (k : K), k • g * g⁻¹ = 1) ∨ ∀ (g : G), ∃ (k : K) (q : G), k • q * q⁻¹ = g
have neg₁ : ∀ (k : K)
  (hk : ¬Eq (α := ZMod (Nat.card G)) ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G))),
  (∀ (g : G) (k : K), k • g * g⁻¹ = 1) ∨ ∀ (g : G), ∃ (k : K) (q : G), k • q * q⁻¹ = g
Tactic: rcases forall_or_exists_not (fun k : K ↦ ϕ k = 1) with hϕ | ⟨k, hk⟩
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
Goal:
G : Type u_1
inst : Group G
p_1 : ℕ
inst_1 : Fact (Nat.Prime p_1)
inst_2 : IsCyclic G
K : Type u_4
inst_3 : Group K
inst_4 : MulDistribMulAction K G
hGK : (Nat.card G).Coprime (Nat.card K)
hc : ¬Nat.card G = 0
this : Finite G
ϕ : K →* ZMod (Nat.card G) := MulDistribMulAction.toMonoidHomZModOfIsCyclic G K ⋯
h :
  ∀ (g : G) (k : K) (n : ℤ)
    (h :
      HSub.hSub (α := ZMod (Nat.card G)) (β := ZMod (Nat.card G))
          ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G)) =
        (↑n : ZMod (Nat.card G))),
    k • g * g⁻¹ = g ^ n
hG :
  ∀ (k : K),
    Eq (α := ZMod (Nat.card G)) ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G)) ∨
      IsUnit
        (HSub.hSub (α := ZMod (Nat.card G)) (β := ZMod (Nat.card G))
          ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G)))
hϕ :
  ∀ (a : K),
    Eq (α := ZMod (Nat.card G)) ((ϕ : (a : K) → ZMod (Nat.card G)) a : ZMod (Nat.card G)) (1 : ZMod (Nat.card G))
p : G
k : K
⊢ HSub.hSub (α := ZMod (Nat.card G)) (β := ZMod (Nat.card G)) ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G))
      (1 : ZMod (Nat.card G)) =
    (↑0 : ZMod (Nat.card G))
have rw : HSub.hSub (α := ZMod (Nat.card G)) 1 1 = (↑0 : ZMod (Nat.card G))
Tactic: rw [hϕ, sub_self, Int.cast_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
Goal:
G : Type u_1
inst : Group G
p_1 : ℕ
inst_1 : Fact (Nat.Prime p_1)
inst_2 : IsCyclic G
K : Type u_4
inst_3 : Group K
inst_4 : MulDistribMulAction K G
hGK : (Nat.card G).Coprime (Nat.card K)
hc : ¬Nat.card G = 0
this : Finite G
ϕ : K →* ZMod (Nat.card G) := MulDistribMulAction.toMonoidHomZModOfIsCyclic G K ⋯
h :
  ∀ (g : G) (k : K) (n : ℤ)
    (h :
      HSub.hSub (α := ZMod (Nat.card G)) (β := ZMod (Nat.card G))
          ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G)) =
        (↑n : ZMod (Nat.card G))),
    k • g * g⁻¹ = g ^ n
hG :
  ∀ (k : K),
    Eq (α := ZMod (Nat.card G)) ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G)) ∨
      IsUnit
        (HSub.hSub (α := ZMod (Nat.card G)) (β := ZMod (Nat.card G))
          ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G)))
hϕ :
  ∀ (a : K),
    Eq (α := ZMod (Nat.card G)) ((ϕ : (a : K) → ZMod (Nat.card G)) a : ZMod (Nat.card G)) (1 : ZMod (Nat.card G))
p : G
k : K
rw : HSub.hSub (α := ZMod (Nat.card G)) 1 1 = (↑0 : ZMod (Nat.card G))
⊢ HSub.hSub (α := ZMod (Nat.card G)) (β := ZMod (Nat.card G)) ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G))
      (1 : ZMod (Nat.card G)) =
    (↑0 : ZMod (Nat.card G))
have rw₁ : Eq (α := ZMod (Nat.card G)) 0 (↑0 : ZMod (Nat.card G))
Tactic: rw [hϕ, sub_self, Int.cast_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
Goal:
G : Type u_1
inst : Group G
p_1 : ℕ
inst_1 : Fact (Nat.Prime p_1)
inst_2 : IsCyclic G
K : Type u_4
inst_3 : Group K
inst_4 : MulDistribMulAction K G
hGK : (Nat.card G).Coprime (Nat.card K)
hc : ¬Nat.card G = 0
this : Finite G
ϕ : K →* ZMod (Nat.card G) := MulDistribMulAction.toMonoidHomZModOfIsCyclic G K ⋯
h :
  ∀ (g : G) (k : K) (n : ℤ)
    (h :
      HSub.hSub (α := ZMod (Nat.card G)) (β := ZMod (Nat.card G))
          ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G)) =
        (↑n : ZMod (Nat.card G))),
    k • g * g⁻¹ = g ^ n
hG :
  ∀ (k : K),
    Eq (α := ZMod (Nat.card G)) ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G)) ∨
      IsUnit
        (HSub.hSub (α := ZMod (Nat.card G)) (β := ZMod (Nat.card G))
          ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G)))
hϕ :
  ∀ (a : K),
    Eq (α := ZMod (Nat.card G)) ((ϕ : (a : K) → ZMod (Nat.card G)) a : ZMod (Nat.card G)) (1 : ZMod (Nat.card G))
p : G
k : K
rw : HSub.hSub (α := ZMod (Nat.card G)) 1 1 = (↑0 : ZMod (Nat.card G))
rw₁ : Eq (α := ZMod (Nat.card G)) 0 (↑0 : ZMod (Nat.card G))
⊢ HSub.hSub (α := ZMod (Nat.card G)) (β := ZMod (Nat.card G)) ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G))
      (1 : ZMod (Nat.card G)) =
    (↑0 : ZMod (Nat.card G))
have rw₂ : Eq (α := ZMod (Nat.card G)) 0 0
Tactic: rw [hϕ, sub_self, Int.cast_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
Goal:
G : Type u_1
inst : Group G
p_1 : ℕ
inst_1 : Fact (Nat.Prime p_1)
inst_2 : IsCyclic G
K : Type u_4
inst_3 : Group K
inst_4 : MulDistribMulAction K G
hGK : (Nat.card G).Coprime (Nat.card K)
hc : ¬Nat.card G = 0
this : Finite G
ϕ : K →* ZMod (Nat.card G) := MulDistribMulAction.toMonoidHomZModOfIsCyclic G K ⋯
h :
  ∀ (g : G) (k : K) (n : ℤ)
    (h :
      HSub.hSub (α := ZMod (Nat.card G)) (β := ZMod (Nat.card G))
          ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G)) =
        (↑n : ZMod (Nat.card G))),
    k • g * g⁻¹ = g ^ n
hG :
  ∀ (k : K),
    Eq (α := ZMod (Nat.card G)) ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G)) ∨
      IsUnit
        (HSub.hSub (α := ZMod (Nat.card G)) (β := ZMod (Nat.card G))
          ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G)))
hϕ :
  ∀ (a : K),
    Eq (α := ZMod (Nat.card G)) ((ϕ : (a : K) → ZMod (Nat.card G)) a : ZMod (Nat.card G)) (1 : ZMod (Nat.card G))
p : G
k : K
⊢ k • p * p⁻¹ = 1
have rw : HPow.hPow (β := ℤ) p 0 = 1
Tactic: rw [h p k 0 (by rw [hϕ, sub_self, Int.cast_zero]), zpow_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
Goal:
G : Type u_1
inst : Group G
p_1 : ℕ
inst_1 : Fact (Nat.Prime p_1)
inst_2 : IsCyclic G
K : Type u_4
inst_3 : Group K
inst_4 : MulDistribMulAction K G
hGK : (Nat.card G).Coprime (Nat.card K)
hc : ¬Nat.card G = 0
this : Finite G
ϕ : K →* ZMod (Nat.card G) := MulDistribMulAction.toMonoidHomZModOfIsCyclic G K ⋯
h :
  ∀ (g : G) (k : K) (n : ℤ)
    (h :
      HSub.hSub (α := ZMod (Nat.card G)) (β := ZMod (Nat.card G))
          ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G)) =
        (↑n : ZMod (Nat.card G))),
    k • g * g⁻¹ = g ^ n
hG :
  ∀ (k : K),
    Eq (α := ZMod (Nat.card G)) ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G)) ∨
      IsUnit
        (HSub.hSub (α := ZMod (Nat.card G)) (β := ZMod (Nat.card G))
          ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G)))
hϕ :
  ∀ (a : K),
    Eq (α := ZMod (Nat.card G)) ((ϕ : (a : K) → ZMod (Nat.card G)) a : ZMod (Nat.card G)) (1 : ZMod (Nat.card G))
p : G
k : K
rw : HPow.hPow (β := ℤ) p 0 = 1
⊢ k • p * p⁻¹ = 1
have rw₁ : Eq.{u_1 + 1} (α := G) 1 1
Tactic: rw [h p k 0 (by rw [hϕ, sub_self, Int.cast_zero]), zpow_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : IsCyclic G
K : Type u_4
inst_3 : Group K
inst_4 : MulDistribMulAction K G
hGK : (Nat.card G).Coprime (Nat.card K)
hc : ¬Nat.card G = 0
this : Finite G
ϕ : K →* ZMod (Nat.card G) := MulDistribMulAction.toMonoidHomZModOfIsCyclic G K ⋯
h :
  ∀ (g : G) (k : K) (n : ℤ)
    (h :
      HSub.hSub (α := ZMod (Nat.card G)) (β := ZMod (Nat.card G))
          ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G)) =
        (↑n : ZMod (Nat.card G))),
    k • g * g⁻¹ = g ^ n
hG :
  ∀ (k : K),
    Eq (α := ZMod (Nat.card G)) ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G)) ∨
      IsUnit
        (HSub.hSub (α := ZMod (Nat.card G)) (β := ZMod (Nat.card G))
          ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G)))
k : K
hk : ¬Eq (α := ZMod (Nat.card G)) ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G))
⊢ (∀ (g : G) (k : K), k • g * g⁻¹ = 1) ∨ ∀ (g : G), ∃ (k : K) (q : G), k • q * q⁻¹ = g
have neg : ∀ (u v : ZMod (Nat.card G)) (hvu : v * u = 1)
  (hu :
    u =
      HSub.hSub (α := ZMod (Nat.card G)) (β := ZMod (Nat.card G))
        ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G))),
  (∀ (g : G) (k : K), k • g * g⁻¹ = 1) ∨ ∀ (g : G), ∃ (k : K) (q : G), k • q * q⁻¹ = g
Tactic: obtain ⟨⟨u, v, -, hvu⟩, hu : u = ϕ k - 1⟩ := (hG k).resolve_left hk