no goals
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
_hp✝ : Fact (Nat.Prime p)
n m : ℕ
hdvd : p ^ m ∣ Fintype.card G
H : Subgroup G
hH : Fintype.card { x // x ∈ H } = p ^ n
hnm✝ : n ≤ m
hnm : n < m
h0m : 0 < m
_wf : m - 1 < m
hnm1 : n ≤ m - 1
K : Subgroup G
hK : Fintype.card { x // x ∈ K } = p ^ (m - 1) ∧ H ≤ K
⊢ p ^ (m - 1 + 1) ∣ Fintype.card G
rwa [tsub_add_cancel_of_le h0m.nat_succ_le]
no goals
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
_hp✝ : Fact (Nat.Prime p)
n m : ℕ
hdvd : p ^ m ∣ Fintype.card G
H : Subgroup G
hH : Fintype.card { x // x ∈ H } = p ^ n
hnm✝ : n ≤ m
hnm : n < m
h0m : 0 < m
_wf : m - 1 < m
hnm1 : n ≤ m - 1
K : Subgroup G
hK : Fintype.card { x // x ∈ K } = p ^ (m - 1) ∧ H ≤ K
hdvd' : p ^ (m - 1 + 1) ∣ Fintype.card G
K' : Subgroup G
hK' : Fintype.card { x // x ∈ K' } = p ^ (m - 1 + 1) ∧ K ≤ K'
⊢ Fintype.card { x // x ∈ K' } = p ^ m
rw [hK'.1, tsub_add_cancel_of_le h0m.nat_succ_le]
no goals
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
_hp✝ : Fact (Nat.Prime p)
n m : ℕ
hdvd : p ^ m ∣ Fintype.card G
H : Subgroup G
hH : Fintype.card { x // x ∈ H } = p ^ n
hnm✝ : n ≤ m
hnm : n = m
⊢ Fintype.card { x // x ∈ H } = p ^ m ∧ H ≤ H
simp [hH, hnm]