case intro
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
g : α
hg : g ≠ 1
⊢ ∃ g, ∀ (x : α), x ∈ zpowers g
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
⊢ ∃ g, ∀ (x : α), x ∈ zpowers g
obtain ⟨g, hg⟩ : ∃ g : α, g ≠ 1 := Fintype.exists_ne_of_one_lt_card (h.symm ▸ hp.1.one_lt) 1
case intro
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
g : α
hg : g ≠ 1
this : Fintype.card { x // x ∈ zpowers g } ∣ p
⊢ ∃ g, ∀ (x : α), x ∈ zpowers g
case intro
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
g : α
hg : g ≠ 1
⊢ ∃ g, ∀ (x : α), x ∈ zpowers g
have : Fintype.card (Subgroup.zpowers g) ∣ p := by
  rw [← h]
  apply card_subgroup_dvd_card
case intro
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
g : α
hg : g ≠ 1
this : Fintype.card { x // x ∈ zpowers g } = 1 ∨ Fintype.card { x // x ∈ zpowers g } = p
⊢ ∃ g, ∀ (x : α), x ∈ zpowers g
case intro
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
g : α
hg : g ≠ 1
this : Fintype.card { x // x ∈ zpowers g } ∣ p
⊢ ∃ g, ∀ (x : α), x ∈ zpowers g
rw [Nat.dvd_prime hp.1] at this
case intro.inl
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
g : α
hg : g ≠ 1
that : Fintype.card { x // x ∈ zpowers g } = 1
⊢ ∃ g, ∀ (x : α), x ∈ zpowers g

case intro.inr
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
g : α
hg : g ≠ 1
that : Fintype.card { x // x ∈ zpowers g } = p
⊢ ∃ g, ∀ (x : α), x ∈ zpowers g
case intro
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
g : α
hg : g ≠ 1
this : Fintype.card { x // x ∈ zpowers g } = 1 ∨ Fintype.card { x // x ∈ zpowers g } = p
⊢ ∃ g, ∀ (x : α), x ∈ zpowers g
cases' this with that that
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
g : α
hg : g ≠ 1
⊢ Fintype.card { x // x ∈ zpowers g } ∣ Fintype.card α
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
g : α
hg : g ≠ 1
⊢ Fintype.card { x // x ∈ zpowers g } ∣ p
rw [← h]
no goals
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
g : α
hg : g ≠ 1
⊢ Fintype.card { x // x ∈ zpowers g } ∣ Fintype.card α
apply card_subgroup_dvd_card
case intro.inl
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
g : α
hg : g ≠ 1
that : ∃ x, ∀ (y : { x // x ∈ zpowers g }), y = x
⊢ ∃ g, ∀ (x : α), x ∈ zpowers g
case intro.inl
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
g : α
hg : g ≠ 1
that : Fintype.card { x // x ∈ zpowers g } = 1
⊢ ∃ g, ∀ (x : α), x ∈ zpowers g
rw [Fintype.card_eq_one_iff] at that
case intro.inl.intro
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
g : α
hg : g ≠ 1
t : { x // x ∈ zpowers g }
ht : ∀ (y : { x // x ∈ zpowers g }), y = t
⊢ ∃ g, ∀ (x : α), x ∈ zpowers g
case intro.inl
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
g : α
hg : g ≠ 1
that : ∃ x, ∀ (y : { x // x ∈ zpowers g }), y = x
⊢ ∃ g, ∀ (x : α), x ∈ zpowers g
cases' that with t ht
case intro.inl.intro
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
g : α
hg : g ≠ 1
t : { x // x ∈ zpowers g }
ht : ∀ (y : { x // x ∈ zpowers g }), y = t
⊢ g = 1
case intro.inl.intro
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
g : α
hg : g ≠ 1
t : { x // x ∈ zpowers g }
ht : ∀ (y : { x // x ∈ zpowers g }), y = t
⊢ ∃ g, ∀ (x : α), x ∈ zpowers g
suffices g = 1 by contradiction
case intro.inl.intro
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
g : α
hg : g ≠ 1
t : { x // x ∈ zpowers g }
ht : ∀ (y : { x // x ∈ zpowers g }), y = t
hgt : { val := g, property := (_ : g ∈ zpowers g) } = t
⊢ g = 1
case intro.inl.intro
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
g : α
hg : g ≠ 1
t : { x // x ∈ zpowers g }
ht : ∀ (y : { x // x ∈ zpowers g }), y = t
⊢ g = 1
have hgt :=
  ht
    ⟨g, by
      change g ∈ Subgroup.zpowers g
      exact Subgroup.mem_zpowers g⟩
case intro.inl.intro
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
g : α
hg : g ≠ 1
t : { x // x ∈ zpowers g }
ht : ∀ (y : { x // x ∈ zpowers g }), y = t
hgt : { val := g, property := (_ : g ∈ zpowers g) } = 1
⊢ g = 1
case intro.inl.intro
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
g : α
hg : g ≠ 1
t : { x // x ∈ zpowers g }
ht : ∀ (y : { x // x ∈ zpowers g }), y = t
hgt : { val := g, property := (_ : g ∈ zpowers g) } = t
⊢ g = 1
rw [← ht 1] at hgt
case intro.inl.intro
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
g : α
hg : g ≠ 1
t : { x // x ∈ zpowers g }
ht : ∀ (y : { x // x ∈ zpowers g }), y = t
hgt : { val := g, property := (_ : g ∈ zpowers g) } = { val := 1, property := (_ : 1 ∈ (zpowers g).toSubmonoid) }
⊢ g = 1
case intro.inl.intro
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
g : α
hg : g ≠ 1
t : { x // x ∈ zpowers g }
ht : ∀ (y : { x // x ∈ zpowers g }), y = t
hgt : { val := g, property := (_ : g ∈ zpowers g) } = 1
⊢ g = 1
change (⟨_, _⟩ : Subgroup.zpowers g) = ⟨_, _⟩ at hgt
no goals
case intro.inl.intro
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
g : α
hg : g ≠ 1
t : { x // x ∈ zpowers g }
ht : ∀ (y : { x // x ∈ zpowers g }), y = t
hgt : { val := g, property := (_ : g ∈ zpowers g) } = { val := 1, property := (_ : 1 ∈ (zpowers g).toSubmonoid) }
⊢ g = 1
simpa using hgt
no goals
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
g : α
hg : g ≠ 1
t : { x // x ∈ zpowers g }
ht : ∀ (y : { x // x ∈ zpowers g }), y = t
this : g = 1
⊢ ∃ g, ∀ (x : α), x ∈ zpowers g
contradiction
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
g : α
hg : g ≠ 1
t : { x // x ∈ zpowers g }
ht : ∀ (y : { x // x ∈ zpowers g }), y = t
⊢ g ∈ zpowers g
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
g : α
hg : g ≠ 1
t : { x // x ∈ zpowers g }
ht : ∀ (y : { x // x ∈ zpowers g }), y = t
⊢ g ∈ zpowers g
change g ∈ Subgroup.zpowers g
no goals
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
g : α
hg : g ≠ 1
t : { x // x ∈ zpowers g }
ht : ∀ (y : { x // x ∈ zpowers g }), y = t
⊢ g ∈ zpowers g
exact Subgroup.mem_zpowers g
case intro.inr
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
g : α
hg : g ≠ 1
that : Fintype.card { x // x ∈ zpowers g } = p
⊢ ∀ (x : α), x ∈ zpowers g
case intro.inr
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
g : α
hg : g ≠ 1
that : Fintype.card { x // x ∈ zpowers g } = p
⊢ ∃ g, ∀ (x : α), x ∈ zpowers g
use g
case intro.inr
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
g : α
hg : g ≠ 1
that : Fintype.card { x // x ∈ zpowers g } = p
x : α
⊢ x ∈ zpowers g
case intro.inr
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
g : α
hg : g ≠ 1
that : Fintype.card { x // x ∈ zpowers g } = p
⊢ ∀ (x : α), x ∈ zpowers g
intro x
case intro.inr
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
g : α
hg : g ≠ 1
that : Fintype.card { x // x ∈ zpowers g } = Fintype.card α
x : α
⊢ x ∈ zpowers g
case intro.inr
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
g : α
hg : g ≠ 1
that : Fintype.card { x // x ∈ zpowers g } = p
x : α
⊢ x ∈ zpowers g
rw [← h] at that
case intro.inr
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
g : α
hg : g ≠ 1
that : Fintype.card { x // x ∈ zpowers g } = Fintype.card α
x : α
⊢ x ∈ ⊤
case intro.inr
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
g : α
hg : g ≠ 1
that : Fintype.card { x // x ∈ zpowers g } = Fintype.card α
x : α
⊢ x ∈ zpowers g
rw [Subgroup.eq_top_of_card_eq _ that]
no goals
case intro.inr
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
g : α
hg : g ≠ 1
that : Fintype.card { x // x ∈ zpowers g } = Fintype.card α
x : α
⊢ x ∈ ⊤
exact Subgroup.mem_top _