α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
h' : 1 < p
⊢ Nontrivial α
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
⊢ Nontrivial α
have h' := Nat.Prime.one_lt (Fact.out (p := p.Prime))
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
h' : 1 < Fintype.card α
⊢ Nontrivial α
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
h' : 1 < p
⊢ Nontrivial α
rw [← h] at h'
no goals
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
h' : 1 < Fintype.card α
⊢ Nontrivial α
exact Fintype.one_lt_card_iff_nontrivial.1 h'
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
this : Nontrivial α
H : Subgroup α
x✝ : Normal H
hcard : Fintype.card { x // x ∈ H } ∣ Fintype.card α
⊢ H = ⊥ ∨ H = ⊤
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
this : Nontrivial α
H : Subgroup α
x✝ : Normal H
⊢ H = ⊥ ∨ H = ⊤
have hcard := card_subgroup_dvd_card H
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
this : Nontrivial α
H : Subgroup α
x✝ : Normal H
hcard : Fintype.card { x // x ∈ H } = 1 ∨ Fintype.card { x // x ∈ H } = p
⊢ H = ⊥ ∨ H = ⊤
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
this : Nontrivial α
H : Subgroup α
x✝ : Normal H
hcard : Fintype.card { x // x ∈ H } ∣ Fintype.card α
⊢ H = ⊥ ∨ H = ⊤
rw [h, dvd_prime (Fact.out (p := p.Prime))] at hcard
case refine'_1
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
this : Nontrivial α
H : Subgroup α
x✝ : Normal H
hcard : Fintype.card { x // x ∈ H } = 1 ∨ Fintype.card { x // x ∈ H } = p
h1 : Fintype.card { x // x ∈ H } = 1
⊢ H = ⊥

case refine'_2
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp✝ : Fact (Nat.Prime p)
h : Fintype.card α = p
this : Nontrivial α
H : Subgroup α
x✝ : Normal H
hcard : Fintype.card { x // x ∈ H } = 1 ∨ Fintype.card { x // x ∈ H } = p
hp : Fintype.card { x // x ∈ H } = p
⊢ H = ⊤
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
this : Nontrivial α
H : Subgroup α
x✝ : Normal H
hcard : Fintype.card { x // x ∈ H } = 1 ∨ Fintype.card { x // x ∈ H } = p
⊢ H = ⊥ ∨ H = ⊤
refine' hcard.imp (fun h1 => _) fun hp => _
case refine'_1
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
this✝ : Nontrivial α
H : Subgroup α
x✝ : Normal H
hcard : Fintype.card { x // x ∈ H } = 1 ∨ Fintype.card { x // x ∈ H } = p
h1 : Fintype.card { x // x ∈ H } = 1
this : Subsingleton { x // x ∈ H }
⊢ H = ⊥
case refine'_1
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
this : Nontrivial α
H : Subgroup α
x✝ : Normal H
hcard : Fintype.card { x // x ∈ H } = 1 ∨ Fintype.card { x // x ∈ H } = p
h1 : Fintype.card { x // x ∈ H } = 1
⊢ H = ⊥
haveI := Fintype.card_le_one_iff_subsingleton.1 (le_of_eq h1)
no goals
case refine'_1
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
this✝ : Nontrivial α
H : Subgroup α
x✝ : Normal H
hcard : Fintype.card { x // x ∈ H } = 1 ∨ Fintype.card { x // x ∈ H } = p
h1 : Fintype.card { x // x ∈ H } = 1
this : Subsingleton { x // x ∈ H }
⊢ H = ⊥
apply eq_bot_of_subsingleton
no goals
case refine'_2
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp✝ : Fact (Nat.Prime p)
h : Fintype.card α = p
this : Nontrivial α
H : Subgroup α
x✝ : Normal H
hcard : Fintype.card { x // x ∈ H } = 1 ∨ Fintype.card { x // x ∈ H } = p
hp : Fintype.card { x // x ∈ H } = p
⊢ H = ⊤
exact eq_top_of_card_eq _ (hp.trans h.symm)