awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Nat.card G
H : Subgroup G
hH : Nat.card.{u} ↥H = p ^ n
s : ℕ
hs : Nat.card G = s * p ^ (n + 1)
hcard : Nat.card.{u} (G ⧸ H) = s * p
hm :
  s * p % p =
    Nat.card.{u}
        (HasQuotient.Quotient ↥(normalizer (↑H : Set G)) (B := Subgroup ↥(normalizer (↑H : Set G)))
          (H.subgroupOf (normalizer (↑H : Set G)))) %
      p
hm' :
  p ∣
    Nat.card.{u}
      (HasQuotient.Quotient ↥(normalizer (↑H : Set G)) (B := Subgroup ↥(normalizer (↑H : Set G)))
        (H.subgroupOf (normalizer (↑H : Set G))))
x :
  HasQuotient.Quotient ↥(normalizer (↑H : Set G)) (B := Subgroup ↥(normalizer (↑H : Set G)))
    (H.subgroupOf (normalizer (↑H : Set G)))
hx : orderOf x = p
hequiv : ↥H ≃ ↥(H.subgroupOf (normalizer (↑H : Set G)))
this :
  Nat.card.{u}
      (↑(Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (normalizer (↑H : Set G)) x) ''
            (↑(comap (mk' (H.subgroupOf (normalizer (↑H : Set G)))) (zpowers x)) : Set ↥(normalizer (↑H : Set G)))) :
        Type u) =
    p ^ (n + 1)
⊢ Nat.card.{u}
      ↥(Subgroup.map (Subgroup.subtype (normalizer (↑H : Set G)))
          (comap (mk' (H.subgroupOf (normalizer (↑H : Set G)))) (zpowers x))) =
    p ^ (n + 1)

Tactic:
convert! this using 2
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Nat.card G
H : Subgroup G
hH : Nat.card.{u} ↥H = p ^ n
s : ℕ
hs : Nat.card G = s * p ^ (n + 1)
hcard : Nat.card.{u} (G ⧸ H) = s * p
hm :
  s * p % p =
    Nat.card.{u}
        (HasQuotient.Quotient ↥(normalizer (↑H : Set G)) (B := Subgroup ↥(normalizer (↑H : Set G)))
          (H.subgroupOf (normalizer (↑H : Set G)))) %
      p
hm' :
  p ∣
    Nat.card.{u}
      (HasQuotient.Quotient ↥(normalizer (↑H : Set G)) (B := Subgroup ↥(normalizer (↑H : Set G)))
        (H.subgroupOf (normalizer (↑H : Set G))))
x :
  HasQuotient.Quotient ↥(normalizer (↑H : Set G)) (B := Subgroup ↥(normalizer (↑H : Set G)))
    (H.subgroupOf (normalizer (↑H : Set G)))
hx : orderOf x = p
hequiv : ↥H ≃ ↥(H.subgroupOf (normalizer (↑H : Set G)))
suffices :
  Nat.card.{u}
      (↑(Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (normalizer (↑H : Set G)) x) ''
            (↑(comap (mk' (H.subgroupOf (normalizer (↑H : Set G)))) (zpowers x)) : Set ↥(normalizer (↑H : Set G)))) :
        Type u) =
    p ^ (n + 1)
⊢ Nat.card.{u}
      ↥(Subgroup.map (Subgroup.subtype (normalizer (↑H : Set G)))
          (comap (mk' (H.subgroupOf (normalizer (↑H : Set G)))) (zpowers x))) =
    p ^ (n + 1)

Tactic:
suffices Nat.card (Subtype.val ''
      ((zpowers x).comap (mk' (H.subgroupOf (normalizer H))) : Set (normalizer H))) = p ^ (n + 1)
      by convert! this using 2
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Nat.card G
H : Subgroup G
hH : Nat.card.{u} ↥H = p ^ n
s : ℕ
hs : Nat.card G = s * p ^ (n + 1)
hcard : Nat.card.{u} (G ⧸ H) = s * p
hm :
  s * p % p =
    Nat.card.{u}
        (HasQuotient.Quotient ↥(normalizer (↑H : Set G)) (B := Subgroup ↥(normalizer (↑H : Set G)))
          (H.subgroupOf (normalizer (↑H : Set G)))) %
      p
hm' :
  p ∣
    Nat.card.{u}
      (HasQuotient.Quotient ↥(normalizer (↑H : Set G)) (B := Subgroup ↥(normalizer (↑H : Set G)))
        (H.subgroupOf (normalizer (↑H : Set G))))
x :
  HasQuotient.Quotient ↥(normalizer (↑H : Set G)) (B := Subgroup ↥(normalizer (↑H : Set G)))
    (H.subgroupOf (normalizer (↑H : Set G)))
hx : orderOf x = p
hequiv : ↥H ≃ ↥(H.subgroupOf (normalizer (↑H : Set G)))
rw :
  Nat.card.{u}
      (↑(↑(comap (mk' (H.subgroupOf (normalizer (↑H : Set G)))) (zpowers x)) : Set ↥(normalizer (↑H : Set G))) :
        Type u) =
    Nat.card.{u} (↥(H.subgroupOf (normalizer (↑H : Set G))) × ↥(zpowers x))
⊢ Nat.card.{u}
      (↑(Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (normalizer (↑H : Set G)) x) ''
            (↑(comap (mk' (H.subgroupOf (normalizer (↑H : Set G)))) (zpowers x)) : Set ↥(normalizer (↑H : Set G)))) :
        Type u) =
    p ^ (n + 1)

Tactic:
rw [Nat.card_image_of_injective Subtype.val_injective
        ((zpowers x).comap (mk' (H.subgroupOf (normalizer H))) : Set (normalizer (H : Set G))),
      pow_succ, ← hH, Nat.card_congr hequiv, ← hx, ← Nat.card_zpowers, ← Nat.card_prod]

Premises used: Subgroup.subgroupOf, Subtype.val_injective, pow_succ, Nat.card_image_of_injective, Subgroup.normalizer, Nat.card_congr, QuotientGroup.mk', SetLike.coe, Nat.card_zpowers, Subgroup.zpowers, Nat.card_prod, Subgroup.comap
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Nat.card G
H : Subgroup G
hH : Nat.card.{u} ↥H = p ^ n
s : ℕ
hs : Nat.card G = s * p ^ (n + 1)
hcard : Nat.card.{u} (G ⧸ H) = s * p
hm :
  s * p % p =
    Nat.card.{u}
        (HasQuotient.Quotient ↥(normalizer (↑H : Set G)) (B := Subgroup ↥(normalizer (↑H : Set G)))
          (H.subgroupOf (normalizer (↑H : Set G)))) %
      p
hm' :
  p ∣
    Nat.card.{u}
      (HasQuotient.Quotient ↥(normalizer (↑H : Set G)) (B := Subgroup ↥(normalizer (↑H : Set G)))
        (H.subgroupOf (normalizer (↑H : Set G))))
x :
  HasQuotient.Quotient ↥(normalizer (↑H : Set G)) (B := Subgroup ↥(normalizer (↑H : Set G)))
    (H.subgroupOf (normalizer (↑H : Set G)))
hx : orderOf x = p
hequiv : ↥H ≃ ↥(H.subgroupOf (normalizer (↑H : Set G)))
⊢ Nat.card.{u}
      (↑(↑(comap (mk' (H.subgroupOf (normalizer (↑H : Set G)))) (zpowers x)) : Set ↥(normalizer (↑H : Set G))) :
        Type u) =
    Nat.card.{u} (↥(H.subgroupOf (normalizer (↑H : Set G))) × ↥(zpowers x))

Tactic:
Nat.card_congr
      (preimageMkEquivSubgroupProdSet (H.subgroupOf (normalizer H)) (zpowers x))

Premises used: Subgroup.subgroupOf, Subgroup.normalizer, Nat.card_congr, QuotientGroup.preimageMkEquivSubgroupProdSet, SetLike.coe, Subgroup.zpowers
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Nat.card G
H : Subgroup G
hH : Nat.card.{u} ↥H = p ^ n
s : ℕ
hs : Nat.card G = s * p ^ (n + 1)
hcard : Nat.card.{u} (G ⧸ H) = s * p
hm :
  s * p % p =
    Nat.card.{u}
        (HasQuotient.Quotient ↥(normalizer (↑H : Set G)) (B := Subgroup ↥(normalizer (↑H : Set G)))
          (H.subgroupOf (normalizer (↑H : Set G)))) %
      p
hm' :
  p ∣
    Nat.card.{u}
      (HasQuotient.Quotient ↥(normalizer (↑H : Set G)) (B := Subgroup ↥(normalizer (↑H : Set G)))
        (H.subgroupOf (normalizer (↑H : Set G))))
x :
  HasQuotient.Quotient ↥(normalizer (↑H : Set G)) (B := Subgroup ↥(normalizer (↑H : Set G)))
    (H.subgroupOf (normalizer (↑H : Set G)))
hx : orderOf x = p
hequiv : ↥H ≃ ↥(H.subgroupOf (normalizer (↑H : Set G)))
⊢ Nat.card.{u}
      (↑(↑(comap (mk' (H.subgroupOf (normalizer (↑H : Set G)))) (zpowers x)) : Set ↥(normalizer (↑H : Set G))) :
        Type u) =
    Nat.card.{u} (↥(H.subgroupOf (normalizer (↑H : Set G))) × ↥(zpowers x))

Tactic:
exact Nat.card_congr
      (preimageMkEquivSubgroupProdSet (H.subgroupOf (normalizer H)) (zpowers x))

Premises used: Subgroup.subgroupOf, Subgroup.normalizer, Nat.card_congr, QuotientGroup.preimageMkEquivSubgroupProdSet, SetLike.coe, Subgroup.zpowers
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Nat.card G
H : Subgroup G
hH : Nat.card.{u} ↥H = p ^ n
s : ℕ
hs : Nat.card G = s * p ^ (n + 1)
hcard : Nat.card.{u} (G ⧸ H) = s * p
hm :
  s * p % p =
    Nat.card.{u}
        (HasQuotient.Quotient ↥(normalizer (↑H : Set G)) (B := Subgroup ↥(normalizer (↑H : Set G)))
          (H.subgroupOf (normalizer (↑H : Set G)))) %
      p
hm' :
  p ∣
    Nat.card.{u}
      (HasQuotient.Quotient ↥(normalizer (↑H : Set G)) (B := Subgroup ↥(normalizer (↑H : Set G)))
        (H.subgroupOf (normalizer (↑H : Set G))))
x :
  HasQuotient.Quotient ↥(normalizer (↑H : Set G)) (B := Subgroup ↥(normalizer (↑H : Set G)))
    (H.subgroupOf (normalizer (↑H : Set G)))
hx : orderOf x = p
hequiv : ↥H ≃ ↥(H.subgroupOf (normalizer (↑H : Set G)))
y : G
hy : y ∈ H
simp :
  ∃ (x_1 : ↥(normalizer (↑H : Set G))),
    Membership.mem (γ :=
        Subgroup
          (HasQuotient.Quotient ↥(normalizer (↑H : Set G)) (B := Subgroup ↥(normalizer (↑H : Set G)))
            (H.subgroupOf (normalizer (↑H : Set G)))))
        (zpowers x) (↑x_1 : ↥(normalizer (↑H : Set G)) ⧸ H.subgroupOf (normalizer (↑H : Set G))) ∧
      (↑x_1 : G) = y
⊢ y ∈
    Subgroup.map (Subgroup.subtype (normalizer (↑H : Set G)))
      (comap (mk' (H.subgroupOf (normalizer (↑H : Set G)))) (zpowers x))

Tactic:
simp only [Subgroup.coe_subtype, mk'_apply, Subgroup.mem_map, Subgroup.mem_comap]

Premises used: Subgroup.coe_subtype, QuotientGroup.mk'_apply, Subgroup.mem_comap, Subgroup.mem_map
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Nat.card G
H : Subgroup G
hH : Nat.card.{u} ↥H = p ^ n
s : ℕ
hs : Nat.card G = s * p ^ (n + 1)
hcard : Nat.card.{u} (G ⧸ H) = s * p
hm :
  s * p % p =
    Nat.card.{u}
        (HasQuotient.Quotient ↥(normalizer (↑H : Set G)) (B := Subgroup ↥(normalizer (↑H : Set G)))
          (H.subgroupOf (normalizer (↑H : Set G)))) %
      p
hm' :
  p ∣
    Nat.card.{u}
      (HasQuotient.Quotient ↥(normalizer (↑H : Set G)) (B := Subgroup ↥(normalizer (↑H : Set G)))
        (H.subgroupOf (normalizer (↑H : Set G))))
x :
  HasQuotient.Quotient ↥(normalizer (↑H : Set G)) (B := Subgroup ↥(normalizer (↑H : Set G)))
    (H.subgroupOf (normalizer (↑H : Set G)))
hx : orderOf x = p
hequiv : ↥H ≃ ↥(H.subgroupOf (normalizer (↑H : Set G)))
y : G
hy : y ∈ H
⊢ ∃ (x_1 : ↥(normalizer (↑H : Set G))),
    Membership.mem (γ :=
        Subgroup
          (HasQuotient.Quotient ↥(normalizer (↑H : Set G)) (B := Subgroup ↥(normalizer (↑H : Set G)))
            (H.subgroupOf (normalizer (↑H : Set G)))))
        (zpowers x) (↑x_1 : ↥(normalizer (↑H : Set G)) ⧸ H.subgroupOf (normalizer (↑H : Set G))) ∧
      (↑x_1 : G) = y

Tactic:
⟨⟨y, le_normalizer hy⟩, ⟨0, ?_⟩, rfl⟩

Premises used: Subgroup.le_normalizer, Subtype.mk, And.intro, Exists.intro, OfNat.ofNat, rfl
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Nat.card G
H : Subgroup G
hH : Nat.card.{u} ↥H = p ^ n
s : ℕ
hs : Nat.card G = s * p ^ (n + 1)
hcard : Nat.card.{u} (G ⧸ H) = s * p
hm :
  s * p % p =
    Nat.card.{u}
        (HasQuotient.Quotient ↥(normalizer (↑H : Set G)) (B := Subgroup ↥(normalizer (↑H : Set G)))
          (H.subgroupOf (normalizer (↑H : Set G)))) %
      p
hm' :
  p ∣
    Nat.card.{u}
      (HasQuotient.Quotient ↥(normalizer (↑H : Set G)) (B := Subgroup ↥(normalizer (↑H : Set G)))
        (H.subgroupOf (normalizer (↑H : Set G))))
x :
  HasQuotient.Quotient ↥(normalizer (↑H : Set G)) (B := Subgroup ↥(normalizer (↑H : Set G)))
    (H.subgroupOf (normalizer (↑H : Set G)))
hx : orderOf x = p
hequiv : ↥H ≃ ↥(H.subgroupOf (normalizer (↑H : Set G)))
y : G
hy : y ∈ H
refine :
  Eq (α :=
    HasQuotient.Quotient ↥(normalizer (↑H : Set G)) (B := Subgroup ↥(normalizer (↑H : Set G)))
      (H.subgroupOf (normalizer (↑H : Set G))))
    ((fun (x_1 : ℤ) ↦ x ^ x_1) 0)
    (↑(Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (normalizer (↑H : Set G)) x) y ⋯) :
      ↥(normalizer (↑H : Set G)) ⧸ H.subgroupOf (normalizer (↑H : Set G)))
⊢ ∃ (x_1 : ↥(normalizer (↑H : Set G))),
    Membership.mem (γ :=
        Subgroup
          (HasQuotient.Quotient ↥(normalizer (↑H : Set G)) (B := Subgroup ↥(normalizer (↑H : Set G)))
            (H.subgroupOf (normalizer (↑H : Set G)))))
        (zpowers x) (↑x_1 : ↥(normalizer (↑H : Set G)) ⧸ H.subgroupOf (normalizer (↑H : Set G))) ∧
      (↑x_1 : G) = y

Tactic:
refine ⟨⟨y, le_normalizer hy⟩, ⟨0, ?_⟩, rfl⟩
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Nat.card G
H : Subgroup G
hH : Nat.card.{u} ↥H = p ^ n
s : ℕ
hs : Nat.card G = s * p ^ (n + 1)
hcard : Nat.card.{u} (G ⧸ H) = s * p
hm :
  s * p % p =
    Nat.card.{u}
        (HasQuotient.Quotient ↥(normalizer (↑H : Set G)) (B := Subgroup ↥(normalizer (↑H : Set G)))
          (H.subgroupOf (normalizer (↑H : Set G)))) %
      p
hm' :
  p ∣
    Nat.card.{u}
      (HasQuotient.Quotient ↥(normalizer (↑H : Set G)) (B := Subgroup ↥(normalizer (↑H : Set G)))
        (H.subgroupOf (normalizer (↑H : Set G))))
x :
  HasQuotient.Quotient ↥(normalizer (↑H : Set G)) (B := Subgroup ↥(normalizer (↑H : Set G)))
    (H.subgroupOf (normalizer (↑H : Set G)))
hx : orderOf x = p
hequiv : ↥H ≃ ↥(H.subgroupOf (normalizer (↑H : Set G)))
y : G
hy : y ∈ H
rw :
  Membership.mem (γ := Subgroup ↥(normalizer (↑H : Set G))) (H.subgroupOf (normalizer (↑H : Set G)))
    (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (normalizer (↑H : Set G)) x) y ⋯)
⊢ HPow.hPow (β := ℤ) x 0 =
    (↑(Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (normalizer (↑H : Set G)) x) y ⋯) :
      ↥(normalizer (↑H : Set G)) ⧸ H.subgroupOf (normalizer (↑H : Set G)))

Tactic:
rw [zpow_zero, eq_comm, QuotientGroup.eq_one_iff]

Premises used: zpow_zero, eq_comm, QuotientGroup.eq_one_iff
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Nat.card G
H : Subgroup G
hH : Nat.card.{u} ↥H = p ^ n
s : ℕ
hs : Nat.card G = s * p ^ (n + 1)
hcard : Nat.card.{u} (G ⧸ H) = s * p
hm :
  s * p % p =
    Nat.card.{u}
        (HasQuotient.Quotient ↥(normalizer (↑H : Set G)) (B := Subgroup ↥(normalizer (↑H : Set G)))
          (H.subgroupOf (normalizer (↑H : Set G)))) %
      p
hm' :
  p ∣
    Nat.card.{u}
      (HasQuotient.Quotient ↥(normalizer (↑H : Set G)) (B := Subgroup ↥(normalizer (↑H : Set G)))
        (H.subgroupOf (normalizer (↑H : Set G))))
x :
  HasQuotient.Quotient ↥(normalizer (↑H : Set G)) (B := Subgroup ↥(normalizer (↑H : Set G)))
    (H.subgroupOf (normalizer (↑H : Set G)))
hx : orderOf x = p
hequiv : ↥H ≃ ↥(H.subgroupOf (normalizer (↑H : Set G)))
y : G
hy : y ∈ H
⊢ Membership.mem (γ := Subgroup ↥(normalizer (↑H : Set G))) (H.subgroupOf (normalizer (↑H : Set G)))
    (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (normalizer (↑H : Set G)) x) y ⋯)

Tactic:
simpa using hy
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
p : ℕ
_hp : Fact (Nat.Prime p)
n m : ℕ
hdvd : p ^ m ∣ Nat.card G
H : Subgroup G
hH : Nat.card.{u} ↥H = p ^ n
hnm_1 : n ≤ m
hnm : n < m
h0m : 0 < m
hnm1 : n ≤ m - 1
K : Subgroup G
hK : Nat.card.{u} ↥K = p ^ (m - 1) ∧ H ≤ K
rwa rwa₁ rwa₂ rwa₃ : p ^ m ∣ Nat.card G
⊢ p ^ (m - 1 + 1) ∣ Nat.card G

Tactic:
rwa [tsub_add_cancel_of_le h0m.nat_succ_le]

Premises used: LT.lt.nat_succ_le, tsub_add_cancel_of_le
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
p : ℕ
_hp : Fact (Nat.Prime p)
n m : ℕ
hdvd : p ^ m ∣ Nat.card G
H : Subgroup G
hH : Nat.card.{u} ↥H = p ^ n
hnm_1 : n ≤ m
hnm : n < m
h0m : 0 < m
hnm1 : n ≤ m - 1
K : Subgroup G
hK : Nat.card.{u} ↥K = p ^ (m - 1) ∧ H ≤ K
hdvd' : p ^ (m - 1 + 1) ∣ Nat.card G
K' : Subgroup G
hK' : Nat.card.{u} ↥K' = p ^ (m - 1 + 1) ∧ K ≤ K'
rw : p ^ (m - 1 + 1) = p ^ m
rw₁ rw₂ : p ^ m = p ^ m
⊢ Nat.card.{u} ↥K' = p ^ m

Tactic:
rw [hK'.1, tsub_add_cancel_of_le h0m.nat_succ_le]

Premises used: LT.lt.nat_succ_le, tsub_add_cancel_of_le, And.left
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
p : ℕ
_hp : Fact (Nat.Prime p)
n m : ℕ
hdvd : p ^ m ∣ Nat.card G
H : Subgroup G
hH : Nat.card.{u} ↥H = p ^ n
hnm_1 : n ≤ m
hnm : n = m
⊢ Nat.card.{u} ↥H = p ^ m ∧ H ≤ H

Tactic:
simp [hH, hnm]
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
p n : ℕ
inst_2 : Fact (Nat.Prime p)
hdvd : p ^ n ∣ Nat.card G
rw : 1 = HPow.hPow (β := ℕ) p 0
rw₁ rw₂ : Eq (α := ℕ) 1 1
⊢ Nat.card.{u} ↥⊥ = HPow.hPow (β := ℕ) p 0

Tactic:
rw [card_bot, pow_zero]

Premises used: Subgroup.card_bot, pow_zero
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
hn : p ^ n ≤ Nat.card G
⊢ Fact (Nat.Prime p)

Tactic:
have : Fact p.Prime := ⟨hp⟩
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
hn : p ^ n ≤ Nat.card G
this : Fact (Nat.Prime p)
linarith :
  Nat.card G = 0 →
    -1 + (HPow.hPow (α := ℤ) (↑p : ℤ) n - (↑(Nat.card G) : ℤ)) + HSub.hSub (α := ℤ) (↑(Nat.card G) : ℤ) 0 +
        (1 - HPow.hPow (α := ℤ) (↑p : ℤ) n) =
      0
⊢ Nat.card G ≠ 0

Tactic:
linarith [Nat.one_le_pow n p hp.pos]

Premises used: Nat.Prime.pos, Nat.one_le_pow
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
hn : p ^ n ≤ Nat.card G
this : Fact (Nat.Prime p)
⊢ Finite G

Tactic:
have : Finite G := Nat.finite_of_card_ne_zero <| by linarith [Nat.one_le_pow n p hp.pos]
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
hn : p ^ n ≤ Nat.card G
this_1 : Fact (Nat.Prime p)
this : Finite G
obtain : ∀ (m : ℕ) (hm : Nat.card G = p ^ m), ∃ (H : Subgroup G), Nat.card.{u} ↥H = p ^ n
⊢ ∃ (H : Subgroup G), Nat.card.{u} ↥H = p ^ n

Tactic:
obtain ⟨m, hm⟩ := h.exists_card_eq

Premises used: IsPGroup.exists_card_eq
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
hn : p ^ n ≤ Nat.card G
this_1 : Fact (Nat.Prime p)
this : Finite G
m : ℕ
hm : Nat.card G = p ^ m
⊢ ∃ (H : Subgroup G), Nat.card.{u} ↥H = p ^ n

Tactic:
exists_subgroup_card_pow_prime _ ?_

Premises used: Sylow.exists_subgroup_card_pow_prime
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
hn : p ^ n ≤ Nat.card G
this_1 : Fact (Nat.Prime p)
this : Finite G
m : ℕ
hm : Nat.card G = p ^ m
refine : p ^ n ∣ Nat.card G
⊢ ∃ (H : Subgroup G), Nat.card.{u} ↥H = p ^ n

Tactic:
refine exists_subgroup_card_pow_prime _ ?_

Premises used: Sylow.exists_subgroup_card_pow_prime
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
hn : p ^ n ≤ Nat.card G
this_1 : Fact (Nat.Prime p)
this : Finite G
m : ℕ
hm : Nat.card G = p ^ m
rw : ∀ (hn : p ^ n ≤ p ^ m) (hm : Nat.card G = p ^ m), p ^ n ∣ p ^ m
⊢ p ^ n ∣ Nat.card G

Tactic:
rw [hm] at hn ⊢
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
this_1 : Fact (Nat.Prime p)
this : Finite G
m : ℕ
hn : p ^ n ≤ p ^ m
hm : Nat.card G = p ^ m
⊢ p ^ n ∣ p ^ m

Tactic:
pow_dvd_pow _ <| (Nat.pow_le_pow_iff_right hp.one_lt).1 hn

Premises used: Nat.Prime.one_lt, pow_dvd_pow, Iff.mp, Nat.pow_le_pow_iff_right
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
this_1 : Fact (Nat.Prime p)
this : Finite G
m : ℕ
hn : p ^ n ≤ p ^ m
hm : Nat.card G = p ^ m
⊢ p ^ n ∣ p ^ m

Tactic:
exact pow_dvd_pow _ <| (Nat.pow_le_pow_iff_right hp.one_lt).1 hn

Premises used: Nat.Prime.one_lt, pow_dvd_pow, Iff.mp, Nat.pow_le_pow_iff_right
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
H : Subgroup G
hn : p ^ n ≤ Nat.card.{u} ↥H
obtain : ∀ (H' : Subgroup ↥H) (H'card : Nat.card.{u} ↥H' = p ^ n), ∃ H' ≤ H, Nat.card.{u} ↥H' = p ^ n
⊢ ∃ H' ≤ H, Nat.card.{u} ↥H' = p ^ n

Tactic:
obtain ⟨H', H'card⟩ := exists_subgroup_card_pow_prime_of_le_card hp (h.to_subgroup H) hn

Premises used: Sylow.exists_subgroup_card_pow_prime_of_le_card, IsPGroup.to_subgroup
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
H : Subgroup G
hn : p ^ n ≤ Nat.card.{u} ↥H
H' : Subgroup ↥H
H'card : Nat.card.{u} ↥H' = p ^ n
⊢ ∃ H' ≤ H, Nat.card.{u} ↥H' = p ^ n

Tactic:
⟨H'.map H.subtype, map_subtype_le _, ?_⟩

Premises used: Subgroup.map, Subgroup.subtype, Subgroup.map_subtype_le, And.intro, Exists.intro
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
H : Subgroup G
hn : p ^ n ≤ Nat.card.{u} ↥H
H' : Subgroup ↥H
H'card : Nat.card.{u} ↥H' = p ^ n
refine : Nat.card.{u} ↥(Subgroup.map H.subtype H') = p ^ n
⊢ ∃ H' ≤ H, Nat.card.{u} ↥H' = p ^ n

Tactic:
refine ⟨H'.map H.subtype, map_subtype_le _, ?_⟩
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
H : Subgroup G
hn : p ^ n ≤ Nat.card.{u} ↥H
H' : Subgroup ↥H
H'card : Nat.card.{u} ↥H' = p ^ n
rw : Nat.card.{u} ↥(Subgroup.map H.subtype H') = Nat.card.{u} ↥H'
⊢ Nat.card.{u} ↥(Subgroup.map H.subtype H') = p ^ n

Tactic:
rw [← H'card]
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
H : Subgroup G
hn : p ^ n ≤ Nat.card.{u} ↥H
H' : Subgroup ↥H
H'card : Nat.card.{u} ↥H' = p ^ n
e : ↥H' ≃* ↥(Subgroup.map H.subtype H') := H'.equivMapOfInjective H.subtype ⋯
⊢ Nat.card.{u} ↥(Subgroup.map H.subtype H') = Nat.card.{u} ↥H'

Tactic:
Nat.card_congr e.symm.toEquiv

Premises used: MulEquiv.toEquiv, Nat.card_congr, MulEquiv.symm
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
H : Subgroup G
hn : p ^ n ≤ Nat.card.{u} ↥H
H' : Subgroup ↥H
H'card : Nat.card.{u} ↥H' = p ^ n
e : ↥H' ≃* ↥(Subgroup.map H.subtype H') := H'.equivMapOfInjective H.subtype ⋯
⊢ Nat.card.{u} ↥(Subgroup.map H.subtype H') = Nat.card.{u} ↥H'

Tactic:
exact Nat.card_congr e.symm.toEquiv

Premises used: MulEquiv.toEquiv, Nat.card_congr, MulEquiv.symm
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
k p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
H : Subgroup G
hk : k ≤ Nat.card.{u} ↥H
hk₀ : k ≠ 0
⊢ ∃ (s : ℕ), p ^ s ≤ k ∧ k < p ^ (s + 1)

Tactic:
exists_nat_pow_near (Nat.one_le_iff_ne_zero.2 hk₀) hp.one_lt

Premises used: Iff.mpr, Nat.Prime.one_lt, exists_nat_pow_near, Nat.one_le_iff_ne_zero
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
k p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
H : Subgroup G
hk : k ≤ Nat.card.{u} ↥H
hk₀ : k ≠ 0
obtain : ∀ (m : ℕ) (hmk : p ^ m ≤ k) (hkm : k < p ^ (m + 1)), ∃ H' ≤ H, Nat.card.{u} ↥H' ≤ k ∧ k < p * Nat.card.{u} ↥H'
⊢ ∃ H' ≤ H, Nat.card.{u} ↥H' ≤ k ∧ k < p * Nat.card.{u} ↥H'

Tactic:
obtain ⟨m, hmk, hkm⟩ : ∃ s, p ^ s ≤ k ∧ k < p ^ (s + 1) :=
    exists_nat_pow_near (Nat.one_le_iff_ne_zero.2 hk₀) hp.one_lt

Premises used: Iff.mpr, Nat.Prime.one_lt, exists_nat_pow_near, Nat.one_le_iff_ne_zero
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
k p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
H : Subgroup G
hk : k ≤ Nat.card.{u} ↥H
hk₀ : k ≠ 0
m : ℕ
hmk : p ^ m ≤ k
hkm : k < p ^ (m + 1)
obtain :
  ∀ (H' : Subgroup G) (H'H : H' ≤ H) (H'card : Nat.card.{u} ↥H' = p ^ m),
    ∃ H' ≤ H, Nat.card.{u} ↥H' ≤ k ∧ k < p * Nat.card.{u} ↥H'
⊢ ∃ H' ≤ H, Nat.card.{u} ↥H' ≤ k ∧ k < p * Nat.card.{u} ↥H'

Tactic:
obtain ⟨H', H'H, H'card⟩ := exists_subgroup_le_card_pow_prime_of_le_card hp h (hmk.trans hk)

Premises used: Sylow.exists_subgroup_le_card_pow_prime_of_le_card, LE.le.trans
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
k p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
H : Subgroup G
hk : k ≤ Nat.card.{u} ↥H
hk₀ : k ≠ 0
m : ℕ
hmk : p ^ m ≤ k
hkm : k < p ^ (m + 1)
H' : Subgroup G
H'H : H' ≤ H
H'card : Nat.card.{u} ↥H' = p ^ m
⊢ ∃ H' ≤ H, Nat.card.{u} ↥H' ≤ k ∧ k < p * Nat.card.{u} ↥H'

Tactic:
⟨H', H'H, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
k p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
H : Subgroup G
hk : k ≤ Nat.card.{u} ↥H
hk₀ : k ≠ 0
m : ℕ
hmk : p ^ m ≤ k
hkm : k < p ^ (m + 1)
H' : Subgroup G
H'H : H' ≤ H
H'card : Nat.card.{u} ↥H' = p ^ m
refine : Nat.card.{u} ↥H' ≤ k ∧ k < p * Nat.card.{u} ↥H'
⊢ ∃ H' ≤ H, Nat.card.{u} ↥H' ≤ k ∧ k < p * Nat.card.{u} ↥H'

Tactic:
refine ⟨H', H'H, ?_⟩