awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
Goal:
p : ℕ
G : Type u_1
inst : Group G
H : Subgroup G
hH : IsPGroup.{u_1} p ↥H
K : Type u_2
inst_1 : Group K
ϕ : K →* G
hϕ : IsPGroup.{u_2} p ↥ϕ.ker
g : ↥(Subgroup.comap ϕ H)
j : ℕ
hj : Eq.{u_1 + 1} (α := G) ((ϕ : (a : K) → G) ((↑g : K) ^ p ^ j) : G) ((↑1 : G) : G)
k : ℕ
hk : (↑g : K) ^ p ^ (j + k) = (↑1 : K)
rwa : (↑(g ^ p ^ (j + k)) : K) = (↑1 : K)
⊢ g ^ p ^ (j + k) = 1
have rwa₁ : (↑g : K) ^ p ^ (j + k) = (↑1 : K)
Tactic: rwa [Subtype.ext_iff, (H.comap ϕ).coe_pow]
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
Goal:
p : ℕ
G : Type u_1
inst : Group G
H K : Subgroup G
hH : IsPGroup.{u_1} p ↥H
hK : IsPGroup.{u_1} p ↥K
inst_1 : K.Normal
⊢ IsPGroup.{u_1} p ↥(H ⊔ K)
have rw : IsPGroup.{u_1} p ↥(Subgroup.comap (QuotientGroup.mk' K) (Subgroup.map (QuotientGroup.mk' K) H))
Tactic: rw [← QuotientGroup.ker_mk' K, ← Subgroup.comap_map_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
Goal:
p : ℕ
G : Type u_1
inst : Group G
H K : Subgroup G
hH : IsPGroup.{u_1} p ↥H
hK : IsPGroup.{u_1} p ↥K
inst_1 : K.Normal
⊢ IsPGroup.{u_1} p ↥(Subgroup.comap (QuotientGroup.mk' K) (Subgroup.map (QuotientGroup.mk' K) H))
have hϕ : IsPGroup.{u_1} p ↥(MonoidHom.ker (QuotientGroup.mk' K))
Tactic: apply (hH.map (QuotientGroup.mk' K)).comap_of_ker_isPGroup
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
Goal:
G : Type u_1
inst : Group G
G₂ : Type u_2
inst_1 : Group G₂
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ : Subgroup G
H₂ : Subgroup G₂
inst_2 : Finite.{u_1 + 1} ↥H₁
inst_3 : Finite.{u_2 + 1} ↥H₂
hH₁ : IsPGroup.{u_1} p₁ ↥H₁
hH₂ : IsPGroup.{u_2} p₂ ↥H₂
⊢ (Nat.card.{u_1} ↥H₁).Coprime (Nat.card.{u_2} ↥H₂)
have obtain : ∀ (n₁ : ℕ) (heq₁ : Nat.card.{u_1} ↥H₁ = p₁ ^ n₁), (Nat.card.{u_1} ↥H₁).Coprime (Nat.card.{u_2} ↥H₂)
Tactic: obtain ⟨n₁, heq₁⟩ := iff_card.mp hH₁
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
Goal:
G : Type u_1
inst : Group G
G₂ : Type u_2
inst_1 : Group G₂
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ : Subgroup G
H₂ : Subgroup G₂
inst_2 : Finite.{u_1 + 1} ↥H₁
inst_3 : Finite.{u_2 + 1} ↥H₂
hH₁ : IsPGroup.{u_1} p₁ ↥H₁
hH₂ : IsPGroup.{u_2} p₂ ↥H₂
n₁ : ℕ
heq₁ : Nat.card.{u_1} ↥H₁ = p₁ ^ n₁
⊢ (Nat.card.{u_1} ↥H₁).Coprime (Nat.card.{u_2} ↥H₂)
have rw : (p₁ ^ n₁).Coprime (Nat.card.{u_2} ↥H₂)
Tactic: rw [heq₁]
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
Goal:
G : Type u_1
inst : Group G
G₂ : Type u_2
inst_1 : Group G₂
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ : Subgroup G
H₂ : Subgroup G₂
inst_2 : Finite.{u_1 + 1} ↥H₁
inst_3 : Finite.{u_2 + 1} ↥H₂
hH₁ : IsPGroup.{u_1} p₁ ↥H₁
hH₂ : IsPGroup.{u_2} p₂ ↥H₂
n₁ : ℕ
⊢ (p₁ ^ n₁).Coprime (Nat.card.{u_2} ↥H₂)
have obtain : ∀ (n₂ : ℕ) (heq₂ : Nat.card.{u_2} ↥H₂ = p₂ ^ n₂), (p₁ ^ n₁).Coprime (Nat.card.{u_2} ↥H₂)
Tactic: obtain ⟨n₂, heq₂⟩ := iff_card.mp hH₂
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
Goal:
G : Type u_1
inst : Group G
G₂ : Type u_2
inst_1 : Group G₂
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ : Subgroup G
H₂ : Subgroup G₂
inst_2 : Finite.{u_1 + 1} ↥H₁
inst_3 : Finite.{u_2 + 1} ↥H₂
hH₁ : IsPGroup.{u_1} p₁ ↥H₁
hH₂ : IsPGroup.{u_2} p₂ ↥H₂
n₁ n₂ : ℕ
heq₂ : Nat.card.{u_2} ↥H₂ = p₂ ^ n₂
⊢ (p₁ ^ n₁).Coprime (Nat.card.{u_2} ↥H₂)
have rw : (p₁ ^ n₁).Coprime (p₂ ^ n₂)
Tactic: rw [heq₂]
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
Goal:
G : Type u_1
inst : Group G
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ H₂ : Subgroup G
hH₁ : IsPGroup.{u_1} p₁ ↥H₁
hH₂ : IsPGroup.{u_1} p₂ ↥H₂
⊢ Disjoint H₁ H₂
have rw : ∀ {x : G}, x ∈ H₁ → x ∈ H₂ → x = 1
Tactic: rw [Subgroup.disjoint_def]
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
Goal:
G : Type u_1
inst : Group G
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ H₂ : Subgroup G
hH₁ : IsPGroup.{u_1} p₁ ↥H₁
hH₂ : IsPGroup.{u_1} p₂ ↥H₂
x : G
hx₁ : x ∈ H₁
hx₂ : x ∈ H₂
⊢ x = 1
have obtain : ∀ (n₁ : ℕ) (hn₁ : orderOf (Subtype.mk (p := fun (x : G) ↦ x ∈ H₁) x hx₁) = p₁ ^ n₁), x = 1
Tactic: obtain ⟨n₁, hn₁⟩ := iff_orderOf.mp hH₁ ⟨x, hx₁⟩
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
Goal:
G : Type u_1
inst : Group G
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ H₂ : Subgroup G
hH₁ : IsPGroup.{u_1} p₁ ↥H₁
hH₂ : IsPGroup.{u_1} p₂ ↥H₂
x : G
hx₁ : x ∈ H₁
hx₂ : x ∈ H₂
n₁ : ℕ
hn₁ : orderOf (Subtype.mk (p := fun (x : G) ↦ x ∈ H₁) x hx₁) = p₁ ^ n₁
⊢ x = 1
have obtain : ∀ (n₂ : ℕ) (hn₂ : orderOf (Subtype.mk (p := fun (x : G) ↦ x ∈ H₂) x hx₂) = p₂ ^ n₂), x = 1
Tactic: obtain ⟨n₂, hn₂⟩ := iff_orderOf.mp hH₂ ⟨x, hx₂⟩
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
Goal:
G : Type u_1
inst : Group G
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ H₂ : Subgroup G
hH₁ : IsPGroup.{u_1} p₁ ↥H₁
hH₂ : IsPGroup.{u_1} p₂ ↥H₂
x : G
hx₁ : x ∈ H₁
hx₂ : x ∈ H₂
n₁ : ℕ
hn₁ : orderOf (Subtype.mk (p := fun (x : G) ↦ x ∈ H₁) x hx₁) = p₁ ^ n₁
n₂ : ℕ
hn₂ : orderOf (Subtype.mk (p := fun (x : G) ↦ x ∈ H₂) x hx₂) = p₂ ^ n₂
⊢ x = 1
have rw : ∀ (hn₁ : orderOf x = p₁ ^ n₁) (n₂ : ℕ) (hn₂ : orderOf x = p₂ ^ n₂), x = 1
Tactic: rw [Subgroup.orderOf_mk] at hn₁ hn₂
Cleared hypotheses: hn₁, n₂, hn₂
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
Goal:
G : Type u_1
inst : Group G
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ H₂ : Subgroup G
hH₁ : IsPGroup.{u_1} p₁ ↥H₁
hH₂ : IsPGroup.{u_1} p₂ ↥H₂
x : G
hx₁ : x ∈ H₁
hx₂ : x ∈ H₂
n₁ : ℕ
hn₁ : orderOf x = p₁ ^ n₁
n₂ : ℕ
hn₂ rw : orderOf x = p₂ ^ n₂
⊢ p₁ ^ n₁ = p₂ ^ n₂
have rw₁ : orderOf x = orderOf x
Tactic: rw [← hn₁, ← hn₂]
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (hypothesis)
Goal:
G : Type u_1
inst : Group G
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ H₂ : Subgroup G
hH₁ : IsPGroup.{u_1} p₁ ↥H₁
hH₂ : IsPGroup.{u_1} p₂ ↥H₂
x : G
hx₁ : x ∈ H₁
hx₂ : x ∈ H₂
n₁ : ℕ
hn₁ : orderOf x = p₁ ^ n₁
n₂ : ℕ
hn₂ : orderOf x = p₂ ^ n₂
⊢ x = 1
have this : p₁ ^ n₁ = p₂ ^ n₂
Tactic: have : p₁ ^ n₁ = p₂ ^ n₂ := by rw [← hn₁, ← hn₂]
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
Goal:
G : Type u_1
inst : Group G
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ H₂ : Subgroup G
hH₁ : IsPGroup.{u_1} p₁ ↥H₁
hH₂ : IsPGroup.{u_1} p₂ ↥H₂
x : G
hx₁ : x ∈ H₁
hx₂ : x ∈ H₂
n₁ : ℕ
hn₁ : orderOf x = p₁ ^ n₁
n₂ : ℕ
hn₂ : orderOf x = p₂ ^ n₂
this : p₁ ^ n₁ = p₂ ^ n₂
⊢ x = 1
have inl : ∀ (hn₁ : orderOf x = HPow.hPow (β := ℕ) p₁ 0) (this : HPow.hPow (β := ℕ) p₁ 0 = p₂ ^ n₂), x = 1
Tactic: rcases n₁.eq_zero_or_pos with (rfl | hn₁)
Cleared hypotheses: n₁, hn₁, this
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
Goal:
G : Type u_1
inst : Group G
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ H₂ : Subgroup G
hH₁ : IsPGroup.{u_1} p₁ ↥H₁
hH₂ : IsPGroup.{u_1} p₂ ↥H₂
x : G
hx₁ : x ∈ H₁
hx₂ : x ∈ H₂
n₁ : ℕ
hn₁ : orderOf x = p₁ ^ n₁
n₂ : ℕ
hn₂ : orderOf x = p₂ ^ n₂
this : p₁ ^ n₁ = p₂ ^ n₂
inl : ∀ (hn₁ : orderOf x = HPow.hPow (β := ℕ) p₁ 0) (this : HPow.hPow (β := ℕ) p₁ 0 = p₂ ^ n₂), x = 1
⊢ x = 1
have inr : ∀ (hn₁ : n₁ > 0), x = 1
Tactic: rcases n₁.eq_zero_or_pos with (rfl | hn₁)
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
Goal:
p : ℕ
G : Type u_1
inst : Group G
hp : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup.{u_1} p ↥P
H : Subgroup G
inst_1 : H.Normal
h_cop : (Nat.card.{u_1} ↥H).Coprime H.index
⊢ P ≤ H ∨ Disjoint H P
have pos : ∀ (h1 : Nat.card.{u_1} ↥H = 0), P ≤ H ∨ Disjoint H P
Tactic: by_cases h1 : Nat.card H = 0
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
Goal:
p : ℕ
G : Type u_1
inst : Group G
hp : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup.{u_1} p ↥P
H : Subgroup G
inst_1 : H.Normal
h_cop : (Nat.card.{u_1} ↥H).Coprime H.index
pos : ∀ (h1 : Nat.card.{u_1} ↥H = 0), P ≤ H ∨ Disjoint H P
⊢ P ≤ H ∨ Disjoint H P
have neg : ∀ (h1 : ¬Nat.card.{u_1} ↥H = 0), P ≤ H ∨ Disjoint H P
Tactic: by_cases h1 : Nat.card H = 0
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (hypothesis)
Goal:
p : ℕ
G : Type u_1
inst : Group G
hp : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup.{u_1} p ↥P
H : Subgroup G
inst_1 : H.Normal
h_cop : (Nat.card.{u_1} ↥H).Coprime H.index
h1 : Nat.card.{u_1} ↥H = 0
⊢ P ≤ H ∨ Disjoint H P
have h_cop₁ : H = ⊤
Tactic: rw [h1, Nat.coprime_zero_left, Subgroup.index_eq_one] at h_cop
Cleared hypotheses: h_cop, h1
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
Goal:
p : ℕ
G : Type u_1
inst : Group G
hp : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup.{u_1} p ↥P
H : Subgroup G
inst_1 : H.Normal
h_cop : H = ⊤
h1 : Nat.card.{u_1} ↥H = 0
⊢ P ≤ H ∨ Disjoint H P
have pos : P ≤ ⊤ ∨ Disjoint ⊤ P
Tactic: rw [h_cop]
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
Goal:
p : ℕ
G : Type u_1
inst : Group G
hp : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup.{u_1} p ↥P
H : Subgroup G
inst_1 : H.Normal
h_cop : (Nat.card.{u_1} ↥H).Coprime H.index
h1 : ¬Nat.card.{u_1} ↥H = 0
⊢ P ≤ H ∨ Disjoint H P
have pos : ∀ (h2 : H.index = 0), P ≤ H ∨ Disjoint H P
Tactic: by_cases h2 : H.index = 0
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
Goal:
p : ℕ
G : Type u_1
inst : Group G
hp : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup.{u_1} p ↥P
H : Subgroup G
inst_1 : H.Normal
h_cop : (Nat.card.{u_1} ↥H).Coprime H.index
h1 : ¬Nat.card.{u_1} ↥H = 0
pos : ∀ (h2 : H.index = 0), P ≤ H ∨ Disjoint H P
⊢ P ≤ H ∨ Disjoint H P
have neg : ∀ (h2 : ¬H.index = 0), P ≤ H ∨ Disjoint H P
Tactic: by_cases h2 : H.index = 0
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (hypothesis)
Goal:
p : ℕ
G : Type u_1
inst : Group G
hp : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup.{u_1} p ↥P
H : Subgroup G
inst_1 : H.Normal
h_cop : (Nat.card.{u_1} ↥H).Coprime H.index
h1 : ¬Nat.card.{u_1} ↥H = 0
h2 : H.index = 0
⊢ P ≤ H ∨ Disjoint H P
have h_cop₁ : H = ⊥
Tactic: rw [h2, Nat.coprime_zero_right, Subgroup.card_eq_one] at h_cop
Cleared hypotheses: h_cop, h1, h2
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
Goal:
p : ℕ
G : Type u_1
inst : Group G
hp : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup.{u_1} p ↥P
H : Subgroup G
inst_1 : H.Normal
h_cop : H = ⊥
h1 : ¬Nat.card.{u_1} ↥H = 0
h2 : H.index = 0
⊢ P ≤ H ∨ Disjoint H P
have pos : P ≤ ⊥ ∨ Disjoint ⊥ P
Tactic: rw [h_cop]
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
Goal:
p : ℕ
G : Type u_1
inst : Group G
hp : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup.{u_1} p ↥P
H : Subgroup G
inst_1 : H.Normal
h_cop : (Nat.card.{u_1} ↥H).Coprime H.index
h1 : ¬Nat.card.{u_1} ↥H = 0
h2 : ¬H.index = 0
⊢ Finite G
have h : Nat.card G ≠ 0
Tactic: apply Nat.finite_of_card_ne_zero
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
Goal:
p : ℕ
G : Type u_1
inst : Group G
hp : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup.{u_1} p ↥P
H : Subgroup G
inst_1 : H.Normal
h_cop : (Nat.card.{u_1} ↥H).Coprime H.index
h1 : ¬Nat.card.{u_1} ↥H = 0
h2 : ¬H.index = 0
⊢ Nat.card G ≠ 0
have h : Nat.card.{u_1} ↥H * H.index ≠ 0
Tactic: rw [← H.card_mul_index]
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (hypothesis)
Goal:
p : ℕ
G : Type u_1
inst : Group G
hp : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup.{u_1} p ↥P
H : Subgroup G
inst_1 : H.Normal
h_cop : (Nat.card.{u_1} ↥H).Coprime H.index
h1 : ¬Nat.card.{u_1} ↥H = 0
h2 : ¬H.index = 0
⊢ P ≤ H ∨ Disjoint H P
have this : Finite G
Tactic: have : Finite G := by
    apply Nat.finite_of_card_ne_zero
    rw [← H.card_mul_index]
    exact mul_ne_zero h1 h2
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
Goal:
p : ℕ
G : Type u_1
inst : Group G
hp : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup.{u_1} p ↥P
H : Subgroup G
inst_1 : H.Normal
h_cop : (Nat.card.{u_1} ↥H).Coprime H.index
h1 : ¬Nat.card.{u_1} ↥H = 0
h2 : ¬H.index = 0
this : Finite G
⊢ (Nat.card.{u_1} ↥H).Coprime (Nat.card.{u_1} ↥P) ∨ H.index.Coprime (Nat.card.{u_1} ↥P)
have obtain : ∀ (k : ℕ) (hk : Nat.card.{u_1} ↥P = p ^ k),
  (Nat.card.{u_1} ↥H).Coprime (Nat.card.{u_1} ↥P) ∨ H.index.Coprime (Nat.card.{u_1} ↥P)
Tactic: obtain ⟨k, hk⟩ := hP.exists_card_eq
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
Goal:
p : ℕ
G : Type u_1
inst : Group G
hp : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup.{u_1} p ↥P
H : Subgroup G
inst_1 : H.Normal
h_cop : (Nat.card.{u_1} ↥H).Coprime H.index
h1 : ¬Nat.card.{u_1} ↥H = 0
h2 : ¬H.index = 0
this : Finite G
k : ℕ
hk : Nat.card.{u_1} ↥P = p ^ k
⊢ (Nat.card.{u_1} ↥H).Coprime (Nat.card.{u_1} ↥P) ∨ H.index.Coprime (Nat.card.{u_1} ↥P)
have refine : ¬p ∣ Nat.card.{u_1} ↥H ∨ ¬p ∣ H.index
Tactic: refine hk ▸ Or.imp hp.out.coprime_pow_of_not_dvd hp.out.coprime_pow_of_not_dvd ?_
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
Goal:
p : ℕ
G : Type u_1
inst : Group G
hp : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup.{u_1} p ↥P
H : Subgroup G
inst_1 : H.Normal
h_cop : (Nat.card.{u_1} ↥H).Coprime H.index
h1 : ¬Nat.card.{u_1} ↥H = 0
h2 : ¬H.index = 0
this : Finite G
k : ℕ
hk : Nat.card.{u_1} ↥P = p ^ k
⊢ ¬p ∣ Nat.card.{u_1} ↥H ∨ ¬p ∣ H.index
have contrapose! : ∀ (h_cop : p ∣ Nat.card.{u_1} ↥H ∧ p ∣ H.index), (Nat.card.{u_1} ↥H).gcd H.index ≠ 1
Tactic: contrapose! h_cop
Cleared hypotheses: h_cop
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (hypothesis)
Goal:
p : ℕ
G : Type u_1
inst : Group G
hp : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup.{u_1} p ↥P
H : Subgroup G
inst_1 : H.Normal
h_cop : (Nat.card.{u_1} ↥H).Coprime H.index
h1 : ¬Nat.card.{u_1} ↥H = 0
h2 : ¬H.index = 0
this : Finite G
⊢ P ≤ H ∨ Disjoint H P
have h3 : (Nat.card.{u_1} ↥H).Coprime (Nat.card.{u_1} ↥P) ∨ H.index.Coprime (Nat.card.{u_1} ↥P)
Tactic: have h3 : (Nat.card H).Coprime (Nat.card P) ∨ H.index.Coprime (Nat.card P) := by
    obtain ⟨k, hk⟩ := hP.exists_card_eq
    refine hk ▸ Or.imp hp.out.coprime_pow_of_not_dvd hp.out.coprime_pow_of_not_dvd ?_
    contrapose! h_cop
    exact Nat.Prime.not_coprime_iff_dvd.mpr ⟨p, hp.out, h_cop⟩
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
Goal:
p : ℕ
G : Type u_1
inst : Group G
hp : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup.{u_1} p ↥P
H : Subgroup G
inst_1 : H.Normal
h_cop : (Nat.card.{u_1} ↥H).Coprime H.index
h1 : ¬Nat.card.{u_1} ↥H = 0
h2 : ¬H.index = 0
this : Finite G
h3 : (Nat.card.{u_1} ↥H).Coprime (Nat.card.{u_1} ↥P) ∨ H.index.Coprime (Nat.card.{u_1} ↥P)
⊢ P ≤ H ∨ Disjoint H P
have neg : ∀ (h4 : H.index.Coprime (Nat.card.{u_1} ↥P)), P ≤ H
Tactic: refine h3.symm.imp (fun h4 ↦ ?_) (fun h4 ↦ ?_)
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
Goal:
p : ℕ
G : Type u_1
inst : Group G
hp : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup.{u_1} p ↥P
H : Subgroup G
inst_1 : H.Normal
h_cop : (Nat.card.{u_1} ↥H).Coprime H.index
h1 : ¬Nat.card.{u_1} ↥H = 0
h2 : ¬H.index = 0
this : Finite G
h3 : (Nat.card.{u_1} ↥H).Coprime (Nat.card.{u_1} ↥P) ∨ H.index.Coprime (Nat.card.{u_1} ↥P)
neg : ∀ (h4 : H.index.Coprime (Nat.card.{u_1} ↥P)), P ≤ H
⊢ P ≤ H ∨ Disjoint H P
have neg₁ : ∀ (h4 : (Nat.card.{u_1} ↥H).Coprime (Nat.card.{u_1} ↥P)), Disjoint H P
Tactic: refine h3.symm.imp (fun h4 ↦ ?_) (fun h4 ↦ ?_)
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
Goal:
p : ℕ
G : Type u_1
inst : Group G
hp : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup.{u_1} p ↥P
H : Subgroup G
inst_1 : H.Normal
h_cop : (Nat.card.{u_1} ↥H).Coprime H.index
h1 : ¬Nat.card.{u_1} ↥H = 0
h2 : ¬H.index = 0
this : Finite G
h3 : (Nat.card.{u_1} ↥H).Coprime (Nat.card.{u_1} ↥P) ∨ H.index.Coprime (Nat.card.{u_1} ↥P)
h4 : H.index.Coprime (Nat.card.{u_1} ↥P)
⊢ P ≤ H
have neg : H.relIndex P = 1
Tactic: rw [← Subgroup.relIndex_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (hypothesis)
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
n : ℕ
hGpn : Nat.card G = p ^ n
hn : 0 < n
⊢ ∃ k > 0, Nat.card.{u_1} ↥(center G) = p ^ k
have this : Finite G
Tactic: have : Finite G := Nat.finite_of_card_ne_zero (hGpn ▸ pow_ne_zero n (NeZero.ne p))
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (hypothesis)
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
n : ℕ
hGpn : Nat.card G = p ^ n
hn : 0 < n
this : Finite G
⊢ ∃ k > 0, Nat.card.{u_1} ↥(center G) = p ^ k
have hcG : IsPGroup.{u_1} p ↥(center G)
Tactic: have hcG := to_subgroup (of_card hGpn) (center G)
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (hypothesis)
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
n : ℕ
hGpn : Nat.card G = p ^ n
hn : 0 < n
this : Finite G
hcG : IsPGroup.{u_1} p ↥(center G)
⊢ ∃ k > 0, Nat.card.{u_1} ↥(center G) = p ^ k
have x : ∃ (n : ℕ), Nat.card.{u_1} ↥(center G) = p ^ n
Tactic: rcases iff_card.1 hcG with _
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (hypothesis)
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
n : ℕ
hGpn : Nat.card G = p ^ n
hn : 0 < n
this : Finite G
hcG : IsPGroup.{u_1} p ↥(center G)
h : ∃ (n : ℕ), Nat.card.{u_1} ↥(center G) = p ^ n
⊢ ∃ k > 0, Nat.card.{u_1} ↥(center G) = p ^ k
have this₁ : Nontrivial G
Tactic: haveI : Nontrivial G := (nontrivial_iff_card <| of_card hGpn).2 ⟨n, hn, hGpn⟩
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
hG : Nat.card G = HPow.hPow (β := ℕ) p 2
⊢ IsCyclic.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G))
have apply : Nat.card.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) ∣ p
Tactic: apply isCyclic_of_card_dvd_prime (p := p)
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
hG : Nat.card G = HPow.hPow (β := ℕ) p 2
⊢ Nat.card.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) ∣ p
have rw : p * Nat.card.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) ∣
  Nat.card.{u_1} ↥(center G) * Subgroup.index (center G)
Tactic: rw [← mul_dvd_mul_iff_left (NeZero.ne p), ← sq, ← hG, ← (center G).card_mul_index]
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
hG : Nat.card G = HPow.hPow (β := ℕ) p 2
⊢ p * Nat.card.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) ∣
    Nat.card.{u_1} ↥(center G) * Subgroup.index (center G)
have h : p ∣ Nat.card.{u_1} ↥(center G)
Tactic: apply mul_dvd_mul_right
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
hG : Nat.card G = HPow.hPow (β := ℕ) p 2
⊢ p ∣ Nat.card.{u_1} ↥(center G)
have h : ∀ (k : ℕ) (hk0 : k > 0) (hk : Nat.card.{u_1} ↥(center G) = p ^ k), p ∣ Nat.card.{u_1} ↥(center G)
Tactic: rcases card_center_eq_prime_pow hG zero_lt_two with ⟨k, hk0, hk⟩
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
hG : Nat.card G = HPow.hPow (β := ℕ) p 2
k : ℕ
hk0 : k > 0
hk : Nat.card.{u_1} ↥(center G) = p ^ k
⊢ p ∣ Nat.card.{u_1} ↥(center G)
have h : p ∣ p ^ k
Tactic: rw [hk]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Basic (goal)
Goal:
α : Type u_1
f : Perm α
s : Set α
⊢ MapsTo (⇑f : (a : α) → α) s s → ∀ (n : ℕ), MapsTo (⇑(f ^ n) : (a : α) → α) s s
have simp_rw : MapsTo (⇑f : (a : α) → α) s s → ∀ (n : ℕ), MapsTo (⇑f : (a : α) → α)^[n] s s
Tactic: simp_rw [Equiv.Perm.coe_pow]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Basic (goal)
Goal:
α : Type u_1
f : Perm α
s : Set α
⊢ SurjOn (⇑f : (a : α) → α) s s → ∀ (n : ℕ), SurjOn (⇑(f ^ n) : (a : α) → α) s s
have simp_rw : SurjOn (⇑f : (a : α) → α) s s → ∀ (n : ℕ), SurjOn (⇑f : (a : α) → α)^[n] s s
Tactic: simp_rw [Equiv.Perm.coe_pow]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Basic (goal)
Goal:
α : Type u_1
f : Perm α
s : Set α
⊢ BijOn (⇑f : (a : α) → α) s s → ∀ (n : ℕ), BijOn (⇑(f ^ n) : (a : α) → α) s s
have simp_rw : BijOn (⇑f : (a : α) → α) s s → ∀ (n : ℕ), BijOn (⇑f : (a : α) → α)^[n] s s
Tactic: simp_rw [Equiv.Perm.coe_pow]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g k c : Perm α
k_mem : Membership.mem (γ := Subgroup (Perm α)) (centralizer {g}) k
c_mem : c ∈ g.cycleFactorsFinset
this :
  (↑g.cycleFactorsFinset : Set (Perm α)) =
    HSMul.hSMul (α := ConjAct (Perm α)) ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) k : ConjAct (Perm α))
      (↑g.cycleFactorsFinset : Set (Perm α))
⊢ HSMul.hSMul (α := ConjAct (Perm α)) ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) k : ConjAct (Perm α)) c ∈
    g.cycleFactorsFinset
have rw : HSMul.hSMul (α := ConjAct (Perm α)) ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) k : ConjAct (Perm α)) c ∈
  HSMul.hSMul (α := ConjAct (Perm α)) ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) k : ConjAct (Perm α))
    (↑g.cycleFactorsFinset : Set (Perm α))
Tactic: rw [← Finset.mem_coe, this]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g k c : Perm α
k_mem : Membership.mem (γ := Subgroup (Perm α)) (centralizer {g}) k
c_mem : c ∈ g.cycleFactorsFinset
⊢ HSMul.hSMul (α := ConjAct (Perm α)) ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) k : ConjAct (Perm α)) c ∈
    g.cycleFactorsFinset
have suffices : (↑g.cycleFactorsFinset : Set (Perm α)) =
  HSMul.hSMul (α := ConjAct (Perm α)) ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) k : ConjAct (Perm α))
    (↑g.cycleFactorsFinset : Set (Perm α))
Tactic: suffices (g.cycleFactorsFinset : Set (Perm α)) =
    (ConjAct.toConjAct k) • g.cycleFactorsFinset by
    rw [← Finset.mem_coe, this]
    simp only [Set.smul_mem_smul_set_iff, Finset.mem_coe, c_mem]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g k c : Perm α
k_mem : Membership.mem (γ := Subgroup (Perm α)) (centralizer {g}) k
c_mem : c ∈ g.cycleFactorsFinset
⊢ (↑g.cycleFactorsFinset : Set (Perm α)) =
    HSMul.hSMul (α := ConjAct (Perm α)) ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) k : ConjAct (Perm α))
      (↑g.cycleFactorsFinset : Set (Perm α))
have this : (HSMul.hSMul (α := ConjAct (Perm α)) ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) k : ConjAct (Perm α))
      g).cycleFactorsFinset =
  HSMul.hSMul (α := ConjAct (Perm α)) ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) k : ConjAct (Perm α))
    g.cycleFactorsFinset
Tactic: have this := cycleFactorsFinset_conj_eq (ConjAct.toConjAct (k : Perm α)) g
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g k c : Perm α
k_mem : Membership.mem (γ := Subgroup (Perm α)) (centralizer {g}) k
c_mem : c ∈ g.cycleFactorsFinset
this :
  (HSMul.hSMul (α := ConjAct (Perm α)) ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) k : ConjAct (Perm α))
        g).cycleFactorsFinset =
    HSMul.hSMul (α := ConjAct (Perm α)) ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) k : ConjAct (Perm α))
      g.cycleFactorsFinset
⊢ (↑g.cycleFactorsFinset : Set (Perm α)) =
    HSMul.hSMul (α := ConjAct (Perm α)) ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) k : ConjAct (Perm α))
      (↑g.cycleFactorsFinset : Set (Perm α))
have this₁ : (g * (k * k⁻¹)).cycleFactorsFinset =
  HSMul.hSMul (α := ConjAct (Perm α)) ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) k : ConjAct (Perm α))
    g.cycleFactorsFinset
Tactic: rw [ConjAct.toConjAct_smul, mem_centralizer_singleton_iff.mp k_mem, mul_assoc] at this
Cleared hypotheses: this