awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
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))
h :
  LE.le (α := Subgroup ↥H)
    (Subgroup.map (G := ↥(commutator ↥H)) (Subgroup.subtype (commutator ↥H)) (commutator ↥(commutator ↥H)))
    (Subgroup.centralizer (↑(commutator ↥H) : Set ↥H))
⊢ LE.le.{u_1} (α := Subgroup ↥(commutator ↥H)) (commutator ↥(commutator ↥H)) (Subgroup.center ↥(commutator ↥H))

Tactic:
simpa [SetLike.le_def, Subgroup.mem_center_iff, Subgroup.mem_centralizer_iff] using h

Premises used: Subgroup.mem_centralizer_iff, SetLike.le_def, Subgroup.mem_center_iff
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
H : Subgroup G
h : H ≠ ⊥
hH : IsCyclic.{u_1} ↥(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H))
ind :
  LE.le (α := Subgroup ↥H)
    (Subgroup.map (G := ↥(commutator ↥H)) (Subgroup.subtype (commutator ↥H)) (commutator ↥(commutator ↥H)))
    (Subgroup.centralizer (↑(commutator ↥H) : Set ↥H))
⊢ LE.le.{u_1} (α := Subgroup ↥(commutator ↥H)) (commutator ↥(commutator ↥H)) (Subgroup.center ↥(commutator ↥H))

Tactic:
suffices h : (commutator (commutator H)).map (commutator H).subtype ≤
        Subgroup.centralizer (commutator H) by
      simpa [SetLike.le_def, Subgroup.mem_center_iff, Subgroup.mem_centralizer_iff] using h
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
H : Subgroup G
h : H ≠ ⊥
hH : IsCyclic.{u_1} ↥(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H))
ind :
  LE.le (α := Subgroup ↥H) (commutator ↥H)
    (Subgroup.centralizer (↑(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H)) : Set ↥H))
⊢ LE.le (α := Subgroup ↥H)
    (Subgroup.map (G := ↥(commutator ↥H)) (Subgroup.subtype (commutator ↥H)) (commutator ↥(commutator ↥H)))
    (Subgroup.centralizer (↑(commutator ↥H) : Set ↥H))

Tactic:
rw [Subgroup.map_subtype_commutator, Subgroup.le_centralizer_iff]

Premises used: Subgroup.le_centralizer_iff, Subgroup.map_subtype_commutator
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
H : Subgroup G
h : 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))))
    ⋯
⊢ 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))))

Tactic:
have h := Abelianization.commutator_subset_ker ⁅commutator H, commutator H⁆.normalizerMonoidHom
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
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
neg : ∀ (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

Tactic:
by_cases hc : Nat.card G = 0

Premises used: Nat.card
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
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
⊢ Subsingleton K ∧ Nonempty K

Tactic:
rw [hc, Nat.coprime_zero_left, Nat.card_eq_one_iff_unique] at hGK

Premises used: Nat.card_eq_one_iff_unique, Nat.coprime_zero_left
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
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
hGK₁ : Subsingleton K ∧ Nonempty K
⊢ Nat.card G = 0

Tactic:
rw [hc, Nat.coprime_zero_left, Nat.card_eq_one_iff_unique] at hGK

Premises used: Nat.card_eq_one_iff_unique, Nat.coprime_zero_left
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
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 : Subsingleton K ∧ Nonempty K
hc : Nat.card G = 0
⊢ (∀ (g : G) (k : K), k • g * g⁻¹ = 1) ∨ ∀ (g : G), ∃ (k : K) (q : G), k • q * q⁻¹ = g

Tactic:
simp [← hGK.1.elim 1]

Premises used: Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
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
⊢ Finite G

Tactic:
have := Nat.finite_of_card_ne_zero hc
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
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))
⊢ 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

Premises used: Int.cast_add, sub_eq_iff_eq_add, Int.cast_one
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
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
rw₂ rw₃ : g ^ n = g ^ n
⊢ k • g * g⁻¹ = g ^ n

Tactic:
rw [MulDistribMulAction.toMonoidHomZModOfIsCyclic_apply rfl k g (n + 1) h,
      zpow_add_one, mul_inv_cancel_right]

Premises used: mul_inv_cancel_right, zpow_add_one, HAdd.hAdd, MulDistribMulAction.toMonoidHomZModOfIsCyclic_apply, OfNat.ofNat, rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
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

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]
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
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
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)))
⊢ 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

Premises used: IsPGroup.exists_card_eq
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
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
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:
ZMod.eq_one_or_isUnit_sub_one hn (ϕ k)
      (hGK.symm.coprime_dvd_left ((orderOf_map_dvd ϕ k).trans (orderOf_dvd_natCard k)))

Premises used: orderOf_map_dvd, Nat.Coprime.symm, Nat.Coprime.coprime_dvd_left, orderOf_dvd_natCard, ZMod.eq_one_or_isUnit_sub_one, DFunLike.coe, Dvd.dvd.trans
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
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
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:
exact ZMod.eq_one_or_isUnit_sub_one hn (ϕ k)
      (hGK.symm.coprime_dvd_left ((orderOf_map_dvd ϕ k).trans (orderOf_dvd_natCard k)))

Premises used: orderOf_map_dvd, Nat.Coprime.symm, Nat.Coprime.coprime_dvd_left, orderOf_dvd_natCard, ZMod.eq_one_or_isUnit_sub_one, DFunLike.coe, Dvd.dvd.trans
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
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)))

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)))
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
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
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
⊢ (∀ (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⟩

Premises used: forall_or_exists_not, OfNat.ofNat, Eq, DFunLike.coe
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
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))
rw₂ rw₃ : Eq (α := ZMod (Nat.card G)) 0 0
⊢ 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))

Tactic:
rw [hϕ, sub_self, Int.cast_zero]

Premises used: sub_self, Int.cast_zero
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
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
rw₁ rw₂ : Eq.{u_1 + 1} (α := G) 1 1
⊢ k • p * p⁻¹ = 1

Tactic:
rw [h p k 0 (by rw [hϕ, sub_self, Int.cast_zero]), zpow_zero]

Premises used: zpow_zero, OfNat.ofNat
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
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)))
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:
exact Or.inl fun p k ↦ by rw [h p k 0 (by rw [hϕ, sub_self, Int.cast_zero]), zpow_zero]

Premises used: Or.inl
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
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))
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
⊢ (∀ (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

Premises used: Or.resolve_left, DFunLike.coe
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
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))
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))
⊢ v * (↑u.cast : ZMod (Nat.card G)) = 1

Tactic:
rw [← u.intCast_zmod_cast] at hu hvu

Premises used: ZMod.intCast_zmod_cast
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
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))
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))
hvu₁ : v * (↑u.cast : ZMod (Nat.card G)) = 1
⊢ (↑u.cast : 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))

Tactic:
rw [← u.intCast_zmod_cast] at hu hvu

Premises used: ZMod.intCast_zmod_cast