awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.PGroup
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ϕ : Function.Injective.{u_2 + 1, u_1 + 1} (α := K) (β := G) (⇑ϕ : (a : K) → G)
⊢ IsPGroup.{u_2} p ↥(Subgroup.comap ϕ H)

Tactic:
hH.comap_of_ker_isPGroup ϕ (ker_isPGroup_of_injective hϕ)

Premises used: IsPGroup.comap_of_ker_isPGroup, IsPGroup.ker_isPGroup_of_injective
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
H : Subgroup G
hH : IsPGroup.{u_1} p ↥H
K : Subgroup G
⊢ IsPGroup.{u_1} p ↥(Subgroup.comap K.subtype H)

Tactic:
hH.comap_of_injective K.subtype Subtype.coe_injective

Premises used: Subgroup.subtype, Subtype.coe_injective, IsPGroup.comap_of_injective
-- Module: Mathlib.GroupTheory.PGroup
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
rw : IsPGroup.{u_1} p ↥(Subgroup.comap (QuotientGroup.mk' K) (Subgroup.map (QuotientGroup.mk' K) H))
⊢ IsPGroup.{u_1} p ↥(H ⊔ K)

Tactic:
rw [← QuotientGroup.ker_mk' K, ← Subgroup.comap_map_eq]

Premises used: Subgroup.comap_map_eq, QuotientGroup.ker_mk'
-- Module: Mathlib.GroupTheory.PGroup
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
hϕ : IsPGroup.{u_1} p ↥(MonoidHom.ker (QuotientGroup.mk' K))
⊢ IsPGroup.{u_1} p ↥(Subgroup.comap (QuotientGroup.mk' K) (Subgroup.map (QuotientGroup.mk' K) H))

Tactic:
apply (hH.map (QuotientGroup.mk' K)).comap_of_ker_isPGroup

Premises used: IsPGroup.comap_of_ker_isPGroup, QuotientGroup.mk', IsPGroup.map
-- Module: Mathlib.GroupTheory.PGroup
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
hϕ hϕ₁ hϕ₂ hϕ₃ : IsPGroup.{u_1} p ↥K
⊢ IsPGroup.{u_1} p ↥(MonoidHom.ker (QuotientGroup.mk' K))

Tactic:
rwa [QuotientGroup.ker_mk']

Premises used: QuotientGroup.ker_mk'
-- Module: Mathlib.GroupTheory.PGroup
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 : H.Normal
⊢ IsPGroup.{u_1} p ↥(H ⊔ K)

Tactic:
sup_comm H K ▸ to_sup_of_normal_right hK hH

Premises used: Eq.rec, IsPGroup.to_sup_of_normal_right, sup_comm, Eq.symm
-- Module: Mathlib.GroupTheory.PGroup
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
hHK : H ≤ Subgroup.normalizer (↑K : Set G)
⊢ IsPGroup.{u_1} p ↥(H ⊔ K)

Tactic:
let hHK' :=
    to_sup_of_normal_right (hH.of_equiv (Subgroup.subgroupOfEquivOfLe hHK).symm)
      (hK.of_equiv (Subgroup.subgroupOfEquivOfLe Subgroup.le_normalizer).symm)
  ((congr_arg (fun H : Subgroup (Subgroup.normalizer K) => IsPGroup p H)
            ((Subgroup.subgroupOf_sup hHK Subgroup.le_normalizer).symm)).mp
        hHK').of_equiv
    (Subgroup.subgroupOfEquivOfLe (sup_le hHK Subgroup.le_normalizer))

Premises used: IsPGroup, Membership.mem, Eq.mp, Subtype, Subgroup.le_normalizer, IsPGroup.to_sup_of_normal_right, congr_arg, IsPGroup.of_equiv, Subgroup.subgroupOfEquivOfLe, sup_le, MulEquiv.symm
-- Module: Mathlib.GroupTheory.PGroup
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
hHK : K ≤ Subgroup.normalizer (↑H : Set G)
⊢ IsPGroup.{u_1} p ↥(H ⊔ K)

Tactic:
sup_comm H K ▸ to_sup_of_normal_right' hK hH hHK

Premises used: Eq.rec, sup_comm, IsPGroup.to_sup_of_normal_right', Eq.symm
-- Module: Mathlib.GroupTheory.PGroup
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₂
obtain : ∀ (n₁ : ℕ) (heq₁ : Nat.card.{u_1} ↥H₁ = p₁ ^ n₁), (Nat.card.{u_1} ↥H₁).Coprime (Nat.card.{u_2} ↥H₂)
⊢ (Nat.card.{u_1} ↥H₁).Coprime (Nat.card.{u_2} ↥H₂)

Tactic:
obtain ⟨n₁, heq₁⟩ := iff_card.mp hH₁

Premises used: IsPGroup.iff_card, Iff.mp
-- Module: Mathlib.GroupTheory.PGroup
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₁
rw : (p₁ ^ n₁).Coprime (Nat.card.{u_2} ↥H₂)
⊢ (Nat.card.{u_1} ↥H₁).Coprime (Nat.card.{u_2} ↥H₂)

Tactic:
rw [heq₁]
-- Module: Mathlib.GroupTheory.PGroup
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₁ : ℕ
obtain : ∀ (n₂ : ℕ) (heq₂ : Nat.card.{u_2} ↥H₂ = p₂ ^ n₂), (p₁ ^ n₁).Coprime (Nat.card.{u_2} ↥H₂)
⊢ (p₁ ^ n₁).Coprime (Nat.card.{u_2} ↥H₂)

Tactic:
obtain ⟨n₂, heq₂⟩ := iff_card.mp hH₂

Premises used: IsPGroup.iff_card, Iff.mp
-- Module: Mathlib.GroupTheory.PGroup
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₂
rw : (p₁ ^ n₁).Coprime (p₂ ^ n₂)
⊢ (p₁ ^ n₁).Coprime (Nat.card.{u_2} ↥H₂)

Tactic:
rw [heq₂]
-- Module: Mathlib.GroupTheory.PGroup
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₂ : ℕ
⊢ (p₁ ^ n₁).Coprime (p₂ ^ n₂)

Tactic:
Nat.coprime_pow_primes _ _ hp₁.elim hp₂.elim hne

Premises used: Fact.elim, Nat.coprime_pow_primes
-- Module: Mathlib.GroupTheory.PGroup
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₂ : ℕ
⊢ (p₁ ^ n₁).Coprime (p₂ ^ n₂)

Tactic:
exact Nat.coprime_pow_primes _ _ hp₁.elim hp₂.elim hne

Premises used: Fact.elim, Nat.coprime_pow_primes
-- Module: Mathlib.GroupTheory.PGroup
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₂
rw : ∀ {x : G}, x ∈ H₁ → x ∈ H₂ → x = 1
⊢ Disjoint H₁ H₂

Tactic:
rw [Subgroup.disjoint_def]

Premises used: Subgroup.disjoint_def
-- Module: Mathlib.GroupTheory.PGroup
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₂
obtain : ∀ (n₁ : ℕ) (hn₁ : orderOf (Subtype.mk (p := fun (x : G) ↦ x ∈ H₁) x hx₁) = p₁ ^ n₁), x = 1
⊢ x = 1

Tactic:
obtain ⟨n₁, hn₁⟩ := iff_orderOf.mp hH₁ ⟨x, hx₁⟩

Premises used: Subtype.mk, Iff.mp, IsPGroup.iff_orderOf
-- Module: Mathlib.GroupTheory.PGroup
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₁
obtain : ∀ (n₂ : ℕ) (hn₂ : orderOf (Subtype.mk (p := fun (x : G) ↦ x ∈ H₂) x hx₂) = p₂ ^ n₂), x = 1
⊢ x = 1

Tactic:
obtain ⟨n₂, hn₂⟩ := iff_orderOf.mp hH₂ ⟨x, hx₂⟩

Premises used: Subtype.mk, Iff.mp, IsPGroup.iff_orderOf
-- Module: Mathlib.GroupTheory.PGroup
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₂
rw : ∀ (hn₁ : orderOf x = p₁ ^ n₁) (n₂ : ℕ) (hn₂ : orderOf x = p₂ ^ n₂), x = 1
⊢ x = 1

Tactic:
rw [Subgroup.orderOf_mk] at hn₁ hn₂

Premises used: Subgroup.orderOf_mk
-- Module: Mathlib.GroupTheory.PGroup
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₂
rw₁ rw₂ : orderOf x = orderOf x
⊢ p₁ ^ n₁ = p₂ ^ n₂

Tactic:
rw [← hn₁, ← hn₂]
-- Module: Mathlib.GroupTheory.PGroup
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₂
⊢ p₁ ^ n₁ = p₂ ^ n₂

Tactic:
have : p₁ ^ n₁ = p₂ ^ n₂ := by rw [← hn₁, ← hn₂]
-- Module: Mathlib.GroupTheory.PGroup
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
inr : ∀ (hn₁ : n₁ > 0), x = 1
⊢ x = 1

Tactic:
rcases n₁.eq_zero_or_pos with (rfl | hn₁)

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.GroupTheory.PGroup
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₂
hn₁ : orderOf x = HPow.hPow (β := ℕ) p₁ 0
this : HPow.hPow (β := ℕ) p₁ 0 = p₂ ^ n₂
⊢ x = 1

Tactic:
simpa using hn₁
-- Module: Mathlib.GroupTheory.PGroup
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₁_1 : orderOf x = p₁ ^ n₁
n₂ : ℕ
hn₂ : orderOf x = p₂ ^ n₂
this : p₁ ^ n₁ = p₂ ^ n₂
hn₁ : n₁ > 0
⊢ x = 1

Tactic:
absurd (eq_of_prime_pow_eq hp₁.out.prime hp₂.out.prime hn₁ this) hne

Premises used: Nat.Prime.prime, eq_of_prime_pow_eq, absurd, Fact.out
-- Module: Mathlib.GroupTheory.PGroup
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₁_1 : orderOf x = p₁ ^ n₁
n₂ : ℕ
hn₂ : orderOf x = p₂ ^ n₂
this : p₁ ^ n₁ = p₂ ^ n₂
hn₁ : n₁ > 0
⊢ x = 1

Tactic:
exact absurd (eq_of_prime_pow_eq hp₁.out.prime hp₂.out.prime hn₁ this) hne

Premises used: Nat.Prime.prime, eq_of_prime_pow_eq, absurd, Fact.out
-- Module: Mathlib.GroupTheory.PGroup
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
neg : ∀ (h1 : ¬Nat.card.{u_1} ↥H = 0), P ≤ H ∨ Disjoint H P
⊢ P ≤ H ∨ Disjoint H P

Tactic:
by_cases h1 : Nat.card H = 0

Premises used: Membership.mem, Subtype, Nat.card
-- Module: Mathlib.GroupTheory.PGroup
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
⊢ H = ⊤

Tactic:
rw [h1, Nat.coprime_zero_left, Subgroup.index_eq_one] at h_cop

Premises used: Nat.coprime_zero_left, Subgroup.index_eq_one
-- Module: Mathlib.GroupTheory.PGroup
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
h_cop₁ : H = ⊤
⊢ Nat.card.{u_1} ↥H = 0

Tactic:
rw [h1, Nat.coprime_zero_left, Subgroup.index_eq_one] at h_cop

Premises used: Nat.coprime_zero_left, Subgroup.index_eq_one
-- Module: Mathlib.GroupTheory.PGroup
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
pos : P ≤ ⊤ ∨ Disjoint ⊤ P
⊢ P ≤ H ∨ Disjoint H P

Tactic:
rw [h_cop]
-- Module: Mathlib.GroupTheory.PGroup
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 ≤ ⊤ ∨ Disjoint ⊤ P

Tactic:
Or.inl le_top

Premises used: le_top, Or.inl
-- Module: Mathlib.GroupTheory.PGroup
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 ≤ ⊤ ∨ Disjoint ⊤ P

Tactic:
exact Or.inl le_top

Premises used: le_top, Or.inl
-- Module: Mathlib.GroupTheory.PGroup
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
neg : ∀ (h2 : ¬H.index = 0), P ≤ H ∨ Disjoint H P
⊢ P ≤ H ∨ Disjoint H P

Tactic:
by_cases h2 : H.index = 0

Premises used: Subgroup.index
-- Module: Mathlib.GroupTheory.PGroup
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
⊢ H = ⊥

Tactic:
rw [h2, Nat.coprime_zero_right, Subgroup.card_eq_one] at h_cop

Premises used: Nat.coprime_zero_right, Subgroup.card_eq_one
-- Module: Mathlib.GroupTheory.PGroup
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
h_cop₁ : H = ⊥
⊢ ¬Nat.card.{u_1} ↥H = 0

Tactic:
rw [h2, Nat.coprime_zero_right, Subgroup.card_eq_one] at h_cop

Premises used: Nat.coprime_zero_right, Subgroup.card_eq_one
-- Module: Mathlib.GroupTheory.PGroup
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
h_cop₁ : H = ⊥
h1₁ : ¬Nat.card.{u_1} ↥H = 0
⊢ H.index = 0

Tactic:
rw [h2, Nat.coprime_zero_right, Subgroup.card_eq_one] at h_cop

Premises used: Nat.coprime_zero_right, Subgroup.card_eq_one
-- Module: Mathlib.GroupTheory.PGroup
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
pos : P ≤ ⊥ ∨ Disjoint ⊥ P
⊢ P ≤ H ∨ Disjoint H P

Tactic:
rw [h_cop]
-- Module: Mathlib.GroupTheory.PGroup
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 ≤ ⊥ ∨ Disjoint ⊥ P

Tactic:
Or.inr disjoint_bot_left

Premises used: disjoint_bot_left, Or.inr
-- Module: Mathlib.GroupTheory.PGroup
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 ≤ ⊥ ∨ Disjoint ⊥ P

Tactic:
exact Or.inr disjoint_bot_left

Premises used: disjoint_bot_left, Or.inr
-- Module: Mathlib.GroupTheory.PGroup
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
h : Nat.card G ≠ 0
⊢ Finite G

Tactic:
apply Nat.finite_of_card_ne_zero

Premises used: Nat.finite_of_card_ne_zero
-- Module: Mathlib.GroupTheory.PGroup
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
h : Nat.card.{u_1} ↥H * H.index ≠ 0
⊢ Nat.card G ≠ 0

Tactic:
rw [← H.card_mul_index]

Premises used: Subgroup.card_mul_index
-- Module: Mathlib.GroupTheory.PGroup
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.{u_1} ↥H * H.index ≠ 0

Tactic:
mul_ne_zero h1 h2

Premises used: mul_ne_zero
-- Module: Mathlib.GroupTheory.PGroup
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.{u_1} ↥H * H.index ≠ 0

Tactic:
exact mul_ne_zero h1 h2

Premises used: mul_ne_zero
-- Module: Mathlib.GroupTheory.PGroup
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

Tactic:
have : Finite G := by
    apply Nat.finite_of_card_ne_zero
    rw [← H.card_mul_index]
    exact mul_ne_zero h1 h2
-- Module: Mathlib.GroupTheory.PGroup
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
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)
⊢ (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

Premises used: IsPGroup.exists_card_eq
-- Module: Mathlib.GroupTheory.PGroup
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)

Tactic:
hk ▸ Or.imp hp.out.coprime_pow_of_not_dvd hp.out.coprime_pow_of_not_dvd ?_

Premises used: Eq.rec, Or.imp, Eq.symm, Fact.out, Nat.Prime.coprime_pow_of_not_dvd
-- Module: Mathlib.GroupTheory.PGroup
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
refine : ¬p ∣ Nat.card.{u_1} ↥H ∨ ¬p ∣ H.index
⊢ (Nat.card.{u_1} ↥H).Coprime (Nat.card.{u_1} ↥P) ∨ H.index.Coprime (Nat.card.{u_1} ↥P)

Tactic:
refine hk ▸ Or.imp hp.out.coprime_pow_of_not_dvd hp.out.coprime_pow_of_not_dvd ?_
-- Module: Mathlib.GroupTheory.PGroup
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
contrapose! : ∀ (h_cop : p ∣ Nat.card.{u_1} ↥H ∧ p ∣ H.index), (Nat.card.{u_1} ↥H).gcd H.index ≠ 1
⊢ ¬p ∣ Nat.card.{u_1} ↥H ∨ ¬p ∣ H.index

Tactic:
contrapose! h_cop
-- Module: Mathlib.GroupTheory.PGroup
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
h1 : ¬Nat.card.{u_1} ↥H = 0
h2 : ¬H.index = 0
this : Finite G
k : ℕ
hk : Nat.card.{u_1} ↥P = p ^ k
h_cop : p ∣ Nat.card.{u_1} ↥H ∧ p ∣ H.index
⊢ (Nat.card.{u_1} ↥H).gcd H.index ≠ 1

Tactic:
Nat.Prime.not_coprime_iff_dvd.mpr ⟨p, hp.out, h_cop⟩

Premises used: Iff.mpr, And.intro, Exists.intro, Fact.out, Nat.Prime.not_coprime_iff_dvd
-- Module: Mathlib.GroupTheory.PGroup
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
h1 : ¬Nat.card.{u_1} ↥H = 0
h2 : ¬H.index = 0
this : Finite G
k : ℕ
hk : Nat.card.{u_1} ↥P = p ^ k
h_cop : p ∣ Nat.card.{u_1} ↥H ∧ p ∣ H.index
⊢ (Nat.card.{u_1} ↥H).gcd H.index ≠ 1

Tactic:
exact Nat.Prime.not_coprime_iff_dvd.mpr ⟨p, hp.out, h_cop⟩

Premises used: Iff.mpr, And.intro, Exists.intro, Fact.out, Nat.Prime.not_coprime_iff_dvd
-- Module: Mathlib.GroupTheory.PGroup
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)

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⟩
-- Module: Mathlib.GroupTheory.PGroup
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

Tactic:
h3.symm.imp (fun h4 ↦ ?_) (fun h4 ↦ ?_)

Premises used: Or.symm, Or.imp
-- Module: Mathlib.GroupTheory.PGroup
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
neg₁ : ∀ (h4 : (Nat.card.{u_1} ↥H).Coprime (Nat.card.{u_1} ↥P)), Disjoint H P
⊢ P ≤ H ∨ Disjoint H P

Tactic:
refine h3.symm.imp (fun h4 ↦ ?_) (fun h4 ↦ ?_)

Premises used: Or.symm, Or.imp
-- Module: Mathlib.GroupTheory.PGroup
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)
neg : H.relIndex P = 1
⊢ P ≤ H

Tactic:
rw [← Subgroup.relIndex_eq_one]

Premises used: Subgroup.relIndex_eq_one
-- Module: Mathlib.GroupTheory.PGroup
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)
⊢ H.relIndex P = 1

Tactic:
Nat.eq_one_of_dvd_coprimes h4 (H.relIndex_dvd_index_of_normal P)
      (Subgroup.relIndex_dvd_card H P)

Premises used: Subgroup.relIndex_dvd_index_of_normal, Nat.eq_one_of_dvd_coprimes, Subgroup.relIndex_dvd_card