[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a b c x : R
e : ℕ
pq_pf : a + b = c
⊢ x ^ e * a + x ^ e * b = x ^ e * c
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a b x : R
e : ℕ
⊢ x ^ e * a + x ^ e * b = x ^ e * (a + b)
[PROOFSTEP]
simp [mul_add]
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a b x : R
e : ℕ
h : a + b = ↑0
⊢ x ^ e * a + x ^ e * b = ↑0
[PROOFSTEP]
simp [h, ← mul_add]
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
b : R
⊢ 0 + b = b
[PROOFSTEP]
simp
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a : R
⊢ a + 0 = a
[PROOFSTEP]
simp
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a₁ b₁ c₁ a₂ b₂ c₂ : R
x✝¹ : a₁ + b₁ = c₁
x✝ : a₂ + b₂ = c₂
⊢ a₁ + a₂ + (b₁ + b₂) = c₁ + c₂
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a₁ b₁ a₂ b₂ : R
⊢ a₁ + a₂ + (b₁ + b₂) = a₁ + b₁ + (a₂ + b₂)
[PROOFSTEP]
simp [add_assoc, add_left_comm]
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a₁ b₁ a₂ b₂ c : R
h : IsNat (a₁ + b₁) 0
h₄ : a₂ + b₂ = c
⊢ a₁ + a₂ + (b₁ + b₂) = c
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a₁ b₁ a₂ b₂ : R
h : IsNat (a₁ + b₁) 0
⊢ a₁ + a₂ + (b₁ + b₂) = a₂ + b₂
[PROOFSTEP]
rw [add_add_add_comm, h.1, Nat.cast_zero, add_pf_zero_add]
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a₂ b c a₁ : R
x✝ : a₂ + b = c
⊢ a₁ + a₂ + b = a₁ + c
[PROOFSTEP]
simp [*, add_assoc]
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a b₂ c b₁ : R
x✝ : a + b₂ = c
⊢ a + (b₁ + b₂) = b₁ + c
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a b₂ b₁ : R
⊢ a + (b₁ + b₂) = b₁ + (a + b₂)
[PROOFSTEP]
simp [add_left_comm]
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a : R
⊢ Nat.rawCast 1 * a = a
[PROOFSTEP]
simp [Nat.rawCast]
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a : R
⊢ a * Nat.rawCast 1 = a
[PROOFSTEP]
simp [Nat.rawCast]
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a₃ b c a₁ : R
a₂ : ℕ
x✝ : a₃ * b = c
⊢ a₁ ^ a₂ * a₃ * b = a₁ ^ a₂ * c
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a₃ b a₁ : R
a₂ : ℕ
⊢ a₁ ^ a₂ * a₃ * b = a₁ ^ a₂ * (a₃ * b)
[PROOFSTEP]
rw [mul_assoc]
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a b₃ c b₁ : R
b₂ : ℕ
x✝ : a * b₃ = c
⊢ a * (b₁ ^ b₂ * b₃) = b₁ ^ b₂ * c
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a b₃ b₁ : R
b₂ : ℕ
⊢ a * (b₁ ^ b₂ * b₃) = b₁ ^ b₂ * (a * b₃)
[PROOFSTEP]
rw [mul_left_comm]
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
ea eb e : ℕ
a₂ b₂ c x : R
x✝¹ : ea + eb = e
x✝ : a₂ * b₂ = c
⊢ x ^ ea * a₂ * (x ^ eb * b₂) = x ^ e * c
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
ea eb : ℕ
a₂ b₂ x : R
⊢ x ^ ea * a₂ * (x ^ eb * b₂) = x ^ (ea + eb) * (a₂ * b₂)
[PROOFSTEP]
simp [pow_add, mul_mul_mul_comm]
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a : R
⊢ a * 0 = 0
[PROOFSTEP]
simp
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a b₁ c₁ b₂ c₂ d : R
x✝² : a * b₁ = c₁
x✝¹ : a * b₂ = c₂
x✝ : c₁ + 0 + c₂ = d
⊢ a * (b₁ + b₂) = d
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a b₁ b₂ : R
⊢ a * (b₁ + b₂) = a * b₁ + 0 + a * b₂
[PROOFSTEP]
simp [_root_.mul_add]
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
b : R
⊢ 0 * b = 0
[PROOFSTEP]
simp
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a₁ b c₁ a₂ c₂ d : R
x✝² : a₁ * b = c₁
x✝¹ : a₂ * b = c₂
x✝ : c₁ + c₂ = d
⊢ (a₁ + a₂) * b = d
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a₁ b a₂ : R
⊢ (a₁ + a₂) * b = a₁ * b + a₂ * b
[PROOFSTEP]
simp [_root_.add_mul]
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
n : ℕ
⊢ ↑(Nat.rawCast n) = Nat.rawCast n
[PROOFSTEP]
simp
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a₁ : ℕ
b₁ : R
a₃ : ℕ
b₃ : R
a₂ : ℕ
x✝¹ : ↑a₁ = b₁
x✝ : ↑a₃ = b₃
⊢ ↑(a₁ ^ a₂ * a₃) = b₁ ^ a₂ * b₃
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a₁ a₃ a₂ : ℕ
⊢ ↑(a₁ ^ a₂ * a₃) = ↑a₁ ^ a₂ * ↑a₃
[PROOFSTEP]
simp
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a₁ : ℕ
b₁ : R
a₂ : ℕ
b₂ : R
x✝¹ : ↑a₁ = b₁
x✝ : ↑a₂ = b₂
⊢ ↑(a₁ + a₂) = b₁ + b₂
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a₁ a₂ : ℕ
⊢ ↑(a₁ + a₂) = ↑a₁ + ↑a₂
[PROOFSTEP]
simp
[GOAL]
u : Lean.Level
R : Type ?u.195007
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a b c : ℕ
x✝ : a * b = c
⊢ a • b = c
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R : Type ?u.195007
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a b : ℕ
⊢ a • b = a * b
[PROOFSTEP]
simp
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a : ℕ
a' b c : R
x✝¹ : ↑a = a'
x✝ : a' * b = c
⊢ a • b = c
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a : ℕ
b : R
⊢ a • b = ↑a * b
[PROOFSTEP]
simp
[GOAL]
u : Lean.Level
R✝ : Type ?u.203137
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : Ring R
a b : R
x✝ : Int.rawCast (Int.negOfNat 1) * a = b
⊢ -a = b
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R✝ : Type ?u.203137
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : Ring R
a : R
⊢ -a = Int.rawCast (Int.negOfNat 1) * a
[PROOFSTEP]
simp [Int.negOfNat]
[GOAL]
u : Lean.Level
R✝ : Type ?u.204069
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : Ring R
a₁ : R
a₂ : ℕ
a₃ b : R
x✝ : -a₃ = b
⊢ -(a₁ ^ a₂ * a₃) = a₁ ^ a₂ * b
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R✝ : Type ?u.204069
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : Ring R
a₁ : R
a₂ : ℕ
a₃ : R
⊢ -(a₁ ^ a₂ * a₃) = a₁ ^ a₂ * -a₃
[PROOFSTEP]
simp
[GOAL]
u : Lean.Level
R✝ : Type ?u.213000
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : Ring R
⊢ -0 = 0
[PROOFSTEP]
simp
[GOAL]
u : Lean.Level
R✝ : Type ?u.213479
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : Ring R
a₁ a₂ b₁ b₂ : R
x✝¹ : -a₁ = b₁
x✝ : -a₂ = b₂
⊢ -(a₁ + a₂) = b₁ + b₂
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R✝ : Type ?u.213479
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : Ring R
a₁ a₂ : R
⊢ -(a₁ + a₂) = -a₁ + -a₂
[PROOFSTEP]
simp [add_comm]
[GOAL]
u : Lean.Level
R✝ : Type ?u.219543
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : Ring R
a b c d : R
x✝¹ : -b = c
x✝ : a + c = d
⊢ a - b = d
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R✝ : Type ?u.219543
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : Ring R
a b : R
⊢ a - b = a + -b
[PROOFSTEP]
simp [sub_eq_add_neg]
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a : R
b : ℕ
⊢ a ^ b = (a + 0) ^ b * Nat.rawCast 1
[PROOFSTEP]
simp
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a : R
b : ℕ
⊢ a ^ b = a ^ b * Nat.rawCast 1 + 0
[PROOFSTEP]
simp
[GOAL]
u : Lean.Level
R : Type ?u.229716
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a✝ : Q(ℕ)
va : ExProd sℕ a✝
a : Q(ℕ)
value✝ : ℚ
hyp✝ : Option Expr
lit : Q(ℕ)
this : «$a» =Q Nat.rawCast «$lit»
p : Nat.ble 1 «$lit» =Q true
⊢ Option Q(0 < «$a»)
[PROOFSTEP]
exact some (q(const_pos $lit $p))
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a : R
⊢ a ^ 1 = a
[PROOFSTEP]
simp
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a : R
k : ℕ
b c : R
x✝¹ : a ^ k = b
x✝ : b * b = c
⊢ a ^ Nat.mul 2 k = c
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a : R
k : ℕ
⊢ a ^ Nat.mul 2 k = a ^ k * a ^ k
[PROOFSTEP]
simp [Nat.succ_mul, pow_add]
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a : R
k : ℕ
b c d : R
x✝² : a ^ k = b
x✝¹ : b * b = c
x✝ : c * a = d
⊢ a ^ Nat.add (Nat.mul 2 k) 1 = d
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a : R
k : ℕ
⊢ a ^ Nat.add (Nat.mul 2 k) 1 = a ^ k * a ^ k * a
[PROOFSTEP]
simp [Nat.succ_mul, pow_add]
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
b : ℕ
⊢ Nat.rawCast 1 ^ b = Nat.rawCast 1
[PROOFSTEP]
simp
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
ea₁ b c₁ : ℕ
a₂ c₂ xa₁ : R
x✝¹ : ea₁ * b = c₁
x✝ : a₂ ^ b = c₂
⊢ (xa₁ ^ ea₁ * a₂) ^ b = xa₁ ^ c₁ * c₂
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
ea₁ b : ℕ
a₂ xa₁ : R
⊢ (xa₁ ^ ea₁ * a₂) ^ b = xa₁ ^ (ea₁ * b) * a₂ ^ b
[PROOFSTEP]
simp [_root_.mul_pow, pow_mul]
[GOAL]
u : Lean.Level
R : Type ?u.271767
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
k : ℕ
⊢ Nat.rawCast k = Nat.rawCast 1 * k
[PROOFSTEP]
simp
[GOAL]
u : Lean.Level
R : Type ?u.272246
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a₃ c₂ k a₁ a₂ : ℕ
x✝ : a₃ = c₂ * k
⊢ a₁ ^ a₂ * a₃ = a₁ ^ a₂ * c₂ * k
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R : Type ?u.272246
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
c₂ k a₁ a₂ : ℕ
⊢ a₁ ^ a₂ * (c₂ * k) = a₁ ^ a₂ * c₂ * k
[PROOFSTEP]
rw [mul_assoc]
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a : R
⊢ a ^ Nat.rawCast 1 = a
[PROOFSTEP]
simp
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
b✝ b : ℕ
x✝ : 0 < b + 1
⊢ 0 ^ (b + 1) = 0
[PROOFSTEP]
simp [pow_succ]
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a : R
b : ℕ
c : R
x✝ : a ^ b = c
⊢ (a + 0) ^ b = c + 0
[PROOFSTEP]
simp [*]
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
b c k : ℕ
a d e : R
x✝² : b = c * k
x✝¹ : a ^ c = d
x✝ : d ^ k = e
⊢ a ^ b = e
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
c k : ℕ
a : R
⊢ a ^ (c * k) = (a ^ c) ^ k
[PROOFSTEP]
simp [pow_mul]
[GOAL]
u : Lean.Level
R : Type ?u.283538
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a✝ : Q(«$α»)
b : Q(ℕ)
va✝ : ExSum sα a✝
vb : ExProd sℕ b
a : Q(«$α»)
va : ExSum sα a
this : «$b» =Q Nat.rawCast 1
⊢ Q(«$a» ^ «$b» = «$a»)
[PROOFSTEP]
exact q(pow_one_cast $a)
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a : R
⊢ a ^ 0 = Nat.rawCast 1 + 0
[PROOFSTEP]
simp
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a : R
b₁ : ℕ
c₁ : R
b₂ : ℕ
c₂ d : R
x✝² : a ^ b₁ = c₁
x✝¹ : a ^ b₂ = c₂
x✝ : c₁ * c₂ = d
⊢ a ^ (b₁ + b₂) = d
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a : R
b₁ b₂ : ℕ
⊢ a ^ (b₁ + b₂) = a ^ b₁ * a ^ b₂
[PROOFSTEP]
simp [_root_.pow_add]
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a : R
n : ℕ
e : a = ↑n
⊢ a = Nat.rawCast n + 0
[PROOFSTEP]
simp [e]
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a : R
e : a = ↑0
⊢ a = 0
[PROOFSTEP]
simp [e]
[GOAL]
u : Lean.Level
R✝ : Type ?u.333286
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝¹ : CommSemiring R✝
n : ℕ
R : Type u_1
inst✝ : Ring R
a : R
e : a = ↑(Int.negOfNat n)
⊢ a = Int.rawCast (Int.negOfNat n) + 0
[PROOFSTEP]
simp [e]
[GOAL]
u : Lean.Level
R✝ : Type ?u.334205
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝¹ : CommSemiring R✝
n : ℤ
d : ℕ
R : Type u_1
inst✝ : DivisionRing R
a : R
inv✝ : Invertible ↑d
e : a = ↑n * ⅟↑d
⊢ a = Rat.rawCast n d + 0
[PROOFSTEP]
simp [e, div_eq_mul_inv]
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a a' : R
p : a = a'
⊢ a = a' ^ Nat.rawCast 1 * Nat.rawCast 1
[PROOFSTEP]
simp [*]
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a : R
⊢ a = a ^ Nat.rawCast 1 * Nat.rawCast 1 + 0
[PROOFSTEP]
simp
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a a' : R
p : a = a'
⊢ a = a' ^ Nat.rawCast 1 * Nat.rawCast 1 + 0
[PROOFSTEP]
simp [*]
[GOAL]
u : Lean.Level
R✝ : Type ?u.354097
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : DivisionRing R
a₁ : R
a₂ : ℕ
a₃ b₁ b₃ c : R
x✝² : a₁⁻¹ = b₁
x✝¹ : a₃⁻¹ = b₃
x✝ : b₃ * (b₁ ^ a₂ * Nat.rawCast 1) = c
⊢ (a₁ ^ a₂ * a₃)⁻¹ = c
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R✝ : Type ?u.354097
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : DivisionRing R
a₁ : R
a₂ : ℕ
a₃ : R
⊢ (a₁ ^ a₂ * a₃)⁻¹ = a₃⁻¹ * (a₁⁻¹ ^ a₂ * Nat.rawCast 1)
[PROOFSTEP]
simp
[GOAL]
u : Lean.Level
R✝ : Type ?u.357008
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : DivisionRing R
a b : R
x✝ : a⁻¹ = b
⊢ (a + 0)⁻¹ = b + 0
[PROOFSTEP]
simp [*]
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a₁ : ℕ
b₁ : R
a₂ : ℕ
b₂ : R
x✝¹ : ↑a₁ = b₁
x✝ : ↑a₂ = b₂
⊢ ↑(a₁ + a₂) = b₁ + b₂
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a₁ a₂ : ℕ
⊢ ↑(a₁ + a₂) = ↑a₁ + ↑a₂
[PROOFSTEP]
simp
[GOAL]
u : Lean.Level
R✝ : Type ?u.392566
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : DivisionRing R
a b c d : R
x✝¹ : b⁻¹ = c
x✝ : a * c = d
⊢ a / b = d
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R✝ : Type ?u.392566
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : DivisionRing R
a b : R
⊢ a / b = a * b⁻¹
[PROOFSTEP]
simp [div_eq_mul_inv]
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a a' b b' c : R
x✝² : a = a'
x✝¹ : b = b'
x✝ : a' + b' = c
⊢ a + b = c
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a' b' : R
⊢ a' + b' = a' + b'
[PROOFSTEP]
rfl
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a a' b b' c : R
x✝² : a = a'
x✝¹ : b = b'
x✝ : a' * b' = c
⊢ a * b = c
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a' b' : R
⊢ a' * b' = a' * b'
[PROOFSTEP]
rfl
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a a' : ℕ
b b' c : R
x✝² : a = a'
x✝¹ : b = b'
x✝ : a' • b' = c
⊢ a • b = c
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a' : ℕ
b' : R
⊢ a' • b' = a' • b'
[PROOFSTEP]
rfl
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a a' : R
b b' : ℕ
c : R
x✝² : a = a'
x✝¹ : b = b'
x✝ : a' ^ b' = c
⊢ a ^ b = c
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a' : R
b' : ℕ
⊢ a' ^ b' = a' ^ b'
[PROOFSTEP]
rfl
[GOAL]
u : Lean.Level
R✝ : Type ?u.398592
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : Ring R
a a' b : R
x✝¹ : a = a'
x✝ : -a' = b
⊢ -a = b
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R✝ : Type ?u.398592
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : Ring R
a' : R
⊢ -a' = -a'
[PROOFSTEP]
rfl
[GOAL]
u : Lean.Level
R✝ : Type ?u.398710
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : Ring R
a a' b b' c : R
x✝² : a = a'
x✝¹ : b = b'
x✝ : a' - b' = c
⊢ a - b = c
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R✝ : Type ?u.398710
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : Ring R
a' b' : R
⊢ a' - b' = a' - b'
[PROOFSTEP]
rfl
[GOAL]
u : Lean.Level
R✝ : Type ?u.398916
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : DivisionRing R
a a' b : R
x✝¹ : a = a'
x✝ : a'⁻¹ = b
⊢ a⁻¹ = b
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R✝ : Type ?u.398916
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : DivisionRing R
a' : R
⊢ a'⁻¹ = a'⁻¹
[PROOFSTEP]
rfl
[GOAL]
u : Lean.Level
R✝ : Type ?u.399091
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : DivisionRing R
a a' b b' c : R
x✝² : a = a'
x✝¹ : b = b'
x✝ : a' / b' = c
⊢ a / b = c
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R✝ : Type ?u.399091
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : DivisionRing R
a' b' : R
⊢ a' / b' = a' / b'
[PROOFSTEP]
rfl
[GOAL]
u : Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a c b : R
x✝¹ : a = c
x✝ : b = c
⊢ a = b
[PROOFSTEP]
subst_vars
[GOAL]
u : Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
b : R
⊢ b = b
[PROOFSTEP]
rfl


[GOAL]
p : ℕ
G : Type u_1
inst✝ : Group G
hp : Fact (Nat.Prime p)
g : G
k : ℕ
hk : orderOf g = p ^ k
⊢ g ^ p ^ k = 1
[PROOFSTEP]
rw [← hk, pow_orderOf_eq_one]
[GOAL]
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
n : ℕ
hG : card G = p ^ n
g : G
⊢ g ^ p ^ n = 1
[PROOFSTEP]
rw [← hG, pow_card_eq_one]
[GOAL]
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype G
⊢ IsPGroup p G ↔ ∃ n, card G = p ^ n
[PROOFSTEP]
have hG : card G ≠ 0 := card_ne_zero
[GOAL]
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype G
hG : card G ≠ 0
⊢ IsPGroup p G ↔ ∃ n, card G = p ^ n
[PROOFSTEP]
refine' ⟨fun h => _, fun ⟨n, hn⟩ => of_card hn⟩
[GOAL]
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype G
hG : card G ≠ 0
h : IsPGroup p G
⊢ ∃ n, card G = p ^ n
[PROOFSTEP]
suffices ∀ q ∈ Nat.factors (card G), q = p by
  use(card G).factors.length
  rw [← List.prod_replicate, ← List.eq_replicate_of_mem this, Nat.prod_factors hG]
[GOAL]
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype G
hG : card G ≠ 0
h : IsPGroup p G
this : ∀ (q : ℕ), q ∈ Nat.factors (card G) → q = p
⊢ ∃ n, card G = p ^ n
[PROOFSTEP]
use(card G).factors.length
[GOAL]
case h
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype G
hG : card G ≠ 0
h : IsPGroup p G
this : ∀ (q : ℕ), q ∈ Nat.factors (card G) → q = p
⊢ card G = p ^ List.length (Nat.factors (card G))
[PROOFSTEP]
rw [← List.prod_replicate, ← List.eq_replicate_of_mem this, Nat.prod_factors hG]
[GOAL]
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype G
hG : card G ≠ 0
h : IsPGroup p G
⊢ ∀ (q : ℕ), q ∈ Nat.factors (card G) → q = p
[PROOFSTEP]
intro q hq
[GOAL]
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype G
hG : card G ≠ 0
h : IsPGroup p G
q : ℕ
hq : q ∈ Nat.factors (card G)
⊢ q = p
[PROOFSTEP]
obtain ⟨hq1, hq2⟩ := (Nat.mem_factors hG).mp hq
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype G
hG : card G ≠ 0
h : IsPGroup p G
q : ℕ
hq : q ∈ Nat.factors (card G)
hq1 : Nat.Prime q
hq2 : q ∣ card G
⊢ q = p
[PROOFSTEP]
haveI : Fact q.Prime := ⟨hq1⟩
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype G
hG : card G ≠ 0
h : IsPGroup p G
q : ℕ
hq : q ∈ Nat.factors (card G)
hq1 : Nat.Prime q
hq2 : q ∣ card G
this : Fact (Nat.Prime q)
⊢ q = p
[PROOFSTEP]
obtain ⟨g, hg⟩ := exists_prime_orderOf_dvd_card q hq2
[GOAL]
case intro.intro
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype G
hG : card G ≠ 0
h : IsPGroup p G
q : ℕ
hq : q ∈ Nat.factors (card G)
hq1 : Nat.Prime q
hq2 : q ∣ card G
this : Fact (Nat.Prime q)
g : G
hg : orderOf g = q
⊢ q = p
[PROOFSTEP]
obtain ⟨k, hk⟩ := (iff_orderOf.mp h) g
[GOAL]
case intro.intro.intro
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype G
hG : card G ≠ 0
h : IsPGroup p G
q : ℕ
hq : q ∈ Nat.factors (card G)
hq1 : Nat.Prime q
hq2 : q ∣ card G
this : Fact (Nat.Prime q)
g : G
hg : orderOf g = q
k : ℕ
hk : orderOf g = p ^ k
⊢ q = p
[PROOFSTEP]
exact (hq1.pow_eq_iff.mp (hg.symm.trans hk).symm).1.symm
[GOAL]
p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
H : Type u_2
inst✝ : Group H
ϕ : H →* G
hϕ : Function.Injective ↑ϕ
⊢ IsPGroup p H
[PROOFSTEP]
simp_rw [IsPGroup, ← hϕ.eq_iff, ϕ.map_pow, ϕ.map_one]
[GOAL]
p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
H : Type u_2
inst✝ : Group H
ϕ : H →* G
hϕ : Function.Injective ↑ϕ
⊢ ∀ (g : H), ∃ k, ↑ϕ g ^ p ^ k = 1
[PROOFSTEP]
exact fun h => hG (ϕ h)
[GOAL]
p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
H : Type u_2
inst✝ : Group H
ϕ : G →* H
hϕ : Function.Surjective ↑ϕ
⊢ IsPGroup p H
[PROOFSTEP]
refine' fun h => Exists.elim (hϕ h) fun g hg => Exists.imp (fun k hk => _) (hG g)
[GOAL]
p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
H : Type u_2
inst✝ : Group H
ϕ : G →* H
hϕ : Function.Surjective ↑ϕ
h : H
g : G
hg : ↑ϕ g = h
k : ℕ
hk : g ^ p ^ k = 1
⊢ h ^ p ^ k = 1
[PROOFSTEP]
rw [← hg, ← ϕ.map_pow, hk, ϕ.map_one]
[GOAL]
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
n : ℕ
hn : Nat.coprime p n
g : G
⊢ ↑(powEquiv hG hn).symm g = g ^ Nat.gcdB (orderOf g) n
[PROOFSTEP]
rw [order_eq_card_zpowers']
[GOAL]
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
n : ℕ
hn : Nat.coprime p n
g : G
⊢ ↑(powEquiv hG hn).symm g = g ^ Nat.gcdB (Nat.card { x // x ∈ Subgroup.zpowers g }) n
[PROOFSTEP]
rfl
[GOAL]
p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
H : Subgroup G
inst✝ : Subgroup.FiniteIndex H
⊢ ∃ n, Subgroup.index H = p ^ n
[PROOFSTEP]
haveI := H.normalCore.fintypeQuotientOfFiniteIndex
[GOAL]
p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
H : Subgroup G
inst✝ : Subgroup.FiniteIndex H
this : Fintype (G ⧸ Subgroup.normalCore H)
⊢ ∃ n, Subgroup.index H = p ^ n
[PROOFSTEP]
obtain ⟨n, hn⟩ := iff_card.mp (hG.to_quotient H.normalCore)
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
H : Subgroup G
inst✝ : Subgroup.FiniteIndex H
this : Fintype (G ⧸ Subgroup.normalCore H)
n : ℕ
hn : card (G ⧸ Subgroup.normalCore H) = p ^ n
⊢ ∃ n, Subgroup.index H = p ^ n
[PROOFSTEP]
obtain ⟨k, _, hk2⟩ :=
  (Nat.dvd_prime_pow hp.out).mp
    ((congr_arg _ (H.normalCore.index_eq_card.trans hn)).mp (Subgroup.index_dvd_of_le H.normalCore_le))
[GOAL]
case intro.intro.intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
H : Subgroup G
inst✝ : Subgroup.FiniteIndex H
this : Fintype (G ⧸ Subgroup.normalCore H)
n : ℕ
hn : card (G ⧸ Subgroup.normalCore H) = p ^ n
k : ℕ
left✝ : k ≤ n
hk2 : Subgroup.index H = p ^ k
⊢ ∃ n, Subgroup.index H = p ^ n
[PROOFSTEP]
exact ⟨k, hk2⟩
[GOAL]
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
⊢ Nat.card G = 1 ∨ p ∣ Nat.card G
[PROOFSTEP]
cases fintypeOrInfinite G
[GOAL]
case inl
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
val✝ : Fintype G
⊢ Nat.card G = 1 ∨ p ∣ Nat.card G
[PROOFSTEP]
obtain ⟨n, hn⟩ := iff_card.mp hG
[GOAL]
case inl.intro
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
val✝ : Fintype G
n : ℕ
hn : card G = p ^ n
⊢ Nat.card G = 1 ∨ p ∣ Nat.card G
[PROOFSTEP]
rw [Nat.card_eq_fintype_card, hn]
[GOAL]
case inl.intro
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
val✝ : Fintype G
n : ℕ
hn : card G = p ^ n
⊢ p ^ n = 1 ∨ p ∣ p ^ n
[PROOFSTEP]
cases' n with n n
[GOAL]
case inl.intro.zero
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
val✝ : Fintype G
hn : card G = p ^ Nat.zero
⊢ p ^ Nat.zero = 1 ∨ p ∣ p ^ Nat.zero
[PROOFSTEP]
exact Or.inl rfl
[GOAL]
case inl.intro.succ
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
val✝ : Fintype G
n : ℕ
hn : card G = p ^ Nat.succ n
⊢ p ^ Nat.succ n = 1 ∨ p ∣ p ^ Nat.succ n
[PROOFSTEP]
exact Or.inr ⟨p ^ n, by rw [pow_succ]⟩
[GOAL]
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
val✝ : Fintype G
n : ℕ
hn : card G = p ^ Nat.succ n
⊢ p ^ Nat.succ n = p * p ^ n
[PROOFSTEP]
rw [pow_succ]
[GOAL]
case inr
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
val✝ : Infinite G
⊢ Nat.card G = 1 ∨ p ∣ Nat.card G
[PROOFSTEP]
rw [Nat.card_eq_zero_of_infinite]
[GOAL]
case inr
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
val✝ : Infinite G
⊢ 0 = 1 ∨ p ∣ 0
[PROOFSTEP]
exact Or.inr ⟨0, rfl⟩
[GOAL]
p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
inst✝ : Fintype G
hGnt : Nontrivial G
k : ℕ
hk : card G = p ^ k
hk0 : k = 0
⊢ False
[PROOFSTEP]
rw [hk0, pow_zero] at hk
[GOAL]
p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
inst✝ : Fintype G
hGnt : Nontrivial G
k : ℕ
hk : card G = 1
hk0 : k = 0
⊢ False
[PROOFSTEP]
exact Fintype.one_lt_card.ne' hk
[GOAL]
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
a : α
inst✝ : Fintype ↑(orbit G a)
⊢ ∃ n, card ↑(orbit G a) = p ^ n
[PROOFSTEP]
let ϕ := orbitEquivQuotientStabilizer G a
[GOAL]
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
a : α
inst✝ : Fintype ↑(orbit G a)
ϕ : ↑(orbit G a) ≃ G ⧸ stabilizer G a := orbitEquivQuotientStabilizer G a
⊢ ∃ n, card ↑(orbit G a) = p ^ n
[PROOFSTEP]
haveI := Fintype.ofEquiv (orbit G a) ϕ
[GOAL]
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
a : α
inst✝ : Fintype ↑(orbit G a)
ϕ : ↑(orbit G a) ≃ G ⧸ stabilizer G a := orbitEquivQuotientStabilizer G a
this : Fintype (G ⧸ stabilizer G a)
⊢ ∃ n, card ↑(orbit G a) = p ^ n
[PROOFSTEP]
haveI := (stabilizer G a).finiteIndex_of_finite_quotient
[GOAL]
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
a : α
inst✝ : Fintype ↑(orbit G a)
ϕ : ↑(orbit G a) ≃ G ⧸ stabilizer G a := orbitEquivQuotientStabilizer G a
this✝ : Fintype (G ⧸ stabilizer G a)
this : Subgroup.FiniteIndex (stabilizer G a)
⊢ ∃ n, card ↑(orbit G a) = p ^ n
[PROOFSTEP]
rw [card_congr ϕ, ← Subgroup.index_eq_card]
[GOAL]
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
a : α
inst✝ : Fintype ↑(orbit G a)
ϕ : ↑(orbit G a) ≃ G ⧸ stabilizer G a := orbitEquivQuotientStabilizer G a
this✝ : Fintype (G ⧸ stabilizer G a)
this : Subgroup.FiniteIndex (stabilizer G a)
⊢ ∃ n, Subgroup.index (stabilizer G a) = p ^ n
[PROOFSTEP]
exact hG.index (stabilizer G a)
[GOAL]
p : ℕ
G : Type u_1
inst✝³ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝² : MulAction G α
inst✝¹ : Fintype α
inst✝ : Fintype ↑(fixedPoints G α)
⊢ card α ≡ card ↑(fixedPoints G α) [MOD p]
[PROOFSTEP]
classical
calc
  card α = card (Σ y : Quotient (orbitRel G α), { x // Quotient.mk'' x = y }) :=
    card_congr (Equiv.sigmaFiberEquiv (@Quotient.mk'' _ (orbitRel G α))).symm
  _ = ∑ a : Quotient (orbitRel G α), card { x // Quotient.mk'' x = a } := (card_sigma _)
  _ ≡ ∑ _a : fixedPoints G α, 1 [MOD p] := ?_
  _ = _ := by simp; rfl
rw [← ZMod.eq_iff_modEq_nat p, Nat.cast_sum, Nat.cast_sum]
have key : ∀ x, card { y // (Quotient.mk'' y : Quotient (orbitRel G α)) = Quotient.mk'' x } = card (orbit G x) :=
  fun x => by simp only [Quotient.eq'']; congr
refine'
  Eq.symm
    (Finset.sum_bij_ne_zero (fun a _ _ => Quotient.mk'' a.1) (fun _ _ _ => Finset.mem_univ _)
      (fun a₁ a₂ _ _ _ _ h => Subtype.eq ((mem_fixedPoints' α).mp a₂.2 a₁.1 (Quotient.exact' h)))
      (fun b => Quotient.inductionOn' b fun b _ hb => _) fun a ha _ => by
      rw [key, mem_fixedPoints_iff_card_orbit_eq_one.mp a.2])
obtain ⟨k, hk⟩ := hG.card_orbit b
have : k = 0 :=
  le_zero_iff.1
    (Nat.le_of_lt_succ
      (lt_of_not_ge
        (mt (pow_dvd_pow p)
          (by rwa [pow_one, ← hk, ← Nat.modEq_zero_iff_dvd, ← ZMod.eq_iff_modEq_nat, ← key, Nat.cast_zero]))))
exact
  ⟨⟨b, mem_fixedPoints_iff_card_orbit_eq_one.2 <| by rw [hk, this, pow_zero]⟩, Finset.mem_univ _,
    ne_of_eq_of_ne Nat.cast_one one_ne_zero, rfl⟩
[GOAL]
p : ℕ
G : Type u_1
inst✝³ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝² : MulAction G α
inst✝¹ : Fintype α
inst✝ : Fintype ↑(fixedPoints G α)
⊢ card α ≡ card ↑(fixedPoints G α) [MOD p]
[PROOFSTEP]
calc
  card α = card (Σ y : Quotient (orbitRel G α), { x // Quotient.mk'' x = y }) :=
    card_congr (Equiv.sigmaFiberEquiv (@Quotient.mk'' _ (orbitRel G α))).symm
  _ = ∑ a : Quotient (orbitRel G α), card { x // Quotient.mk'' x = a } := (card_sigma _)
  _ ≡ ∑ _a : fixedPoints G α, 1 [MOD p] := ?_
  _ = _ := by simp; rfl
[GOAL]
p : ℕ
G : Type u_1
inst✝³ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝² : MulAction G α
inst✝¹ : Fintype α
inst✝ : Fintype ↑(fixedPoints G α)
⊢ ∑ _a : ↑(fixedPoints G α), 1 = card ↑(fixedPoints G α)
[PROOFSTEP]
simp
[GOAL]
p : ℕ
G : Type u_1
inst✝³ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝² : MulAction G α
inst✝¹ : Fintype α
inst✝ : Fintype ↑(fixedPoints G α)
⊢ Finset.card Finset.univ = card ↑(fixedPoints G α)
[PROOFSTEP]
rfl
[GOAL]
p : ℕ
G : Type u_1
inst✝³ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝² : MulAction G α
inst✝¹ : Fintype α
inst✝ : Fintype ↑(fixedPoints G α)
⊢ ∑ a : Quotient (orbitRel G α), card { x // Quotient.mk'' x = a } ≡ ∑ _a : ↑(fixedPoints G α), 1 [MOD p]
[PROOFSTEP]
rw [← ZMod.eq_iff_modEq_nat p, Nat.cast_sum, Nat.cast_sum]
[GOAL]
p : ℕ
G : Type u_1
inst✝³ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝² : MulAction G α
inst✝¹ : Fintype α
inst✝ : Fintype ↑(fixedPoints G α)
⊢ ∑ x : Quotient (orbitRel G α), ↑(card { x_1 // Quotient.mk'' x_1 = x }) = ∑ x : ↑(fixedPoints G α), ↑1
[PROOFSTEP]
have key : ∀ x, card { y // (Quotient.mk'' y : Quotient (orbitRel G α)) = Quotient.mk'' x } = card (orbit G x) :=
  fun x => by simp only [Quotient.eq'']; congr
[GOAL]
p : ℕ
G : Type u_1
inst✝³ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝² : MulAction G α
inst✝¹ : Fintype α
inst✝ : Fintype ↑(fixedPoints G α)
x : α
⊢ card { y // Quotient.mk'' y = Quotient.mk'' x } = card ↑(orbit G x)
[PROOFSTEP]
simp only [Quotient.eq'']
[GOAL]
p : ℕ
G : Type u_1
inst✝³ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝² : MulAction G α
inst✝¹ : Fintype α
inst✝ : Fintype ↑(fixedPoints G α)
x : α
⊢ card { y // Setoid.r y x } = card ↑(orbit G x)
[PROOFSTEP]
congr
[GOAL]
p : ℕ
G : Type u_1
inst✝³ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝² : MulAction G α
inst✝¹ : Fintype α
inst✝ : Fintype ↑(fixedPoints G α)
key : ∀ (x : α), card { y // Quotient.mk'' y = Quotient.mk'' x } = card ↑(orbit G x)
⊢ ∑ x : Quotient (orbitRel G α), ↑(card { x_1 // Quotient.mk'' x_1 = x }) = ∑ x : ↑(fixedPoints G α), ↑1
[PROOFSTEP]
refine'
  Eq.symm
    (Finset.sum_bij_ne_zero (fun a _ _ => Quotient.mk'' a.1) (fun _ _ _ => Finset.mem_univ _)
      (fun a₁ a₂ _ _ _ _ h => Subtype.eq ((mem_fixedPoints' α).mp a₂.2 a₁.1 (Quotient.exact' h)))
      (fun b => Quotient.inductionOn' b fun b _ hb => _) fun a ha _ => by
      rw [key, mem_fixedPoints_iff_card_orbit_eq_one.mp a.2])
[GOAL]
p : ℕ
G : Type u_1
inst✝³ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝² : MulAction G α
inst✝¹ : Fintype α
inst✝ : Fintype ↑(fixedPoints G α)
key : ∀ (x : α), card { y // Quotient.mk'' y = Quotient.mk'' x } = card ↑(orbit G x)
a : ↑(fixedPoints G α)
ha : a ∈ Finset.univ
x✝ : ↑1 ≠ 0
⊢ ↑1 = ↑(card { x // Quotient.mk'' x = (fun a x x => Quotient.mk'' ↑a) a ha x✝ })
[PROOFSTEP]
rw [key, mem_fixedPoints_iff_card_orbit_eq_one.mp a.2]
[GOAL]
p : ℕ
G : Type u_1
inst✝³ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝² : MulAction G α
inst✝¹ : Fintype α
inst✝ : Fintype ↑(fixedPoints G α)
key : ∀ (x : α), card { y // Quotient.mk'' y = Quotient.mk'' x } = card ↑(orbit G x)
b✝ : Quotient (orbitRel G α)
b : α
x✝ : Quotient.mk'' b ∈ Finset.univ
hb : ↑(card { x // Quotient.mk'' x = Quotient.mk'' b }) ≠ 0
⊢ ∃ a h₁ h₂, Quotient.mk'' b = (fun a x x => Quotient.mk'' ↑a) a h₁ h₂
[PROOFSTEP]
obtain ⟨k, hk⟩ := hG.card_orbit b
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝³ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝² : MulAction G α
inst✝¹ : Fintype α
inst✝ : Fintype ↑(fixedPoints G α)
key : ∀ (x : α), card { y // Quotient.mk'' y = Quotient.mk'' x } = card ↑(orbit G x)
b✝ : Quotient (orbitRel G α)
b : α
x✝ : Quotient.mk'' b ∈ Finset.univ
hb : ↑(card { x // Quotient.mk'' x = Quotient.mk'' b }) ≠ 0
k : ℕ
hk : card ↑(orbit G b) = p ^ k
⊢ ∃ a h₁ h₂, Quotient.mk'' b = (fun a x x => Quotient.mk'' ↑a) a h₁ h₂
[PROOFSTEP]
have : k = 0 :=
  le_zero_iff.1
    (Nat.le_of_lt_succ
      (lt_of_not_ge
        (mt (pow_dvd_pow p)
          (by rwa [pow_one, ← hk, ← Nat.modEq_zero_iff_dvd, ← ZMod.eq_iff_modEq_nat, ← key, Nat.cast_zero]))))
[GOAL]
p : ℕ
G : Type u_1
inst✝³ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝² : MulAction G α
inst✝¹ : Fintype α
inst✝ : Fintype ↑(fixedPoints G α)
key : ∀ (x : α), card { y // Quotient.mk'' y = Quotient.mk'' x } = card ↑(orbit G x)
b✝ : Quotient (orbitRel G α)
b : α
x✝ : Quotient.mk'' b ∈ Finset.univ
hb : ↑(card { x // Quotient.mk'' x = Quotient.mk'' b }) ≠ 0
k : ℕ
hk : card ↑(orbit G b) = p ^ k
⊢ ¬p ^ Nat.succ 0 ∣ p ^ k
[PROOFSTEP]
rwa [pow_one, ← hk, ← Nat.modEq_zero_iff_dvd, ← ZMod.eq_iff_modEq_nat, ← key, Nat.cast_zero]
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝³ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝² : MulAction G α
inst✝¹ : Fintype α
inst✝ : Fintype ↑(fixedPoints G α)
key : ∀ (x : α), card { y // Quotient.mk'' y = Quotient.mk'' x } = card ↑(orbit G x)
b✝ : Quotient (orbitRel G α)
b : α
x✝ : Quotient.mk'' b ∈ Finset.univ
hb : ↑(card { x // Quotient.mk'' x = Quotient.mk'' b }) ≠ 0
k : ℕ
hk : card ↑(orbit G b) = p ^ k
this : k = 0
⊢ ∃ a h₁ h₂, Quotient.mk'' b = (fun a x x => Quotient.mk'' ↑a) a h₁ h₂
[PROOFSTEP]
exact
  ⟨⟨b, mem_fixedPoints_iff_card_orbit_eq_one.2 <| by rw [hk, this, pow_zero]⟩, Finset.mem_univ _,
    ne_of_eq_of_ne Nat.cast_one one_ne_zero, rfl⟩
[GOAL]
p : ℕ
G : Type u_1
inst✝³ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝² : MulAction G α
inst✝¹ : Fintype α
inst✝ : Fintype ↑(fixedPoints G α)
key : ∀ (x : α), card { y // Quotient.mk'' y = Quotient.mk'' x } = card ↑(orbit G x)
b✝ : Quotient (orbitRel G α)
b : α
x✝ : Quotient.mk'' b ∈ Finset.univ
hb : ↑(card { x // Quotient.mk'' x = Quotient.mk'' b }) ≠ 0
k : ℕ
hk : card ↑(orbit G b) = p ^ k
this : k = 0
⊢ card ↑(orbit G b) = 1
[PROOFSTEP]
rw [hk, this, pow_zero]
[GOAL]
p : ℕ
G : Type u_1
inst✝³ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝² : MulAction G α
inst✝¹ : Fintype α
hpα : ¬p ∣ card α
inst✝ : Finite ↑(fixedPoints G α)
⊢ Nonempty ↑(fixedPoints G α)
[PROOFSTEP]
cases nonempty_fintype (fixedPoints G α)
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝³ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝² : MulAction G α
inst✝¹ : Fintype α
hpα : ¬p ∣ card α
inst✝ : Finite ↑(fixedPoints G α)
val✝ : Fintype ↑(fixedPoints G α)
⊢ Nonempty ↑(fixedPoints G α)
[PROOFSTEP]
rw [← card_pos_iff, pos_iff_ne_zero]
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝³ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝² : MulAction G α
inst✝¹ : Fintype α
hpα : ¬p ∣ card α
inst✝ : Finite ↑(fixedPoints G α)
val✝ : Fintype ↑(fixedPoints G α)
⊢ card ↑(fixedPoints G α) ≠ 0
[PROOFSTEP]
contrapose! hpα
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝³ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝² : MulAction G α
inst✝¹ : Fintype α
inst✝ : Finite ↑(fixedPoints G α)
val✝ : Fintype ↑(fixedPoints G α)
hpα : card ↑(fixedPoints G α) = 0
⊢ p ∣ card α
[PROOFSTEP]
rw [← Nat.modEq_zero_iff_dvd, ← hpα]
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝³ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝² : MulAction G α
inst✝¹ : Fintype α
inst✝ : Finite ↑(fixedPoints G α)
val✝ : Fintype ↑(fixedPoints G α)
hpα : card ↑(fixedPoints G α) = 0
⊢ card α ≡ card ↑(fixedPoints G α) [MOD p]
[PROOFSTEP]
exact hG.card_modEq_card_fixedPoints α
[GOAL]
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Fintype α
hpα : p ∣ card α
a : α
ha : a ∈ fixedPoints G α
⊢ ∃ b, b ∈ fixedPoints G α ∧ a ≠ b
[PROOFSTEP]
cases nonempty_fintype (fixedPoints G α)
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Fintype α
hpα : p ∣ card α
a : α
ha : a ∈ fixedPoints G α
val✝ : Fintype ↑(fixedPoints G α)
⊢ ∃ b, b ∈ fixedPoints G α ∧ a ≠ b
[PROOFSTEP]
have hpf : p ∣ card (fixedPoints G α) :=
  Nat.modEq_zero_iff_dvd.mp ((hG.card_modEq_card_fixedPoints α).symm.trans hpα.modEq_zero_nat)
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Fintype α
hpα : p ∣ card α
a : α
ha : a ∈ fixedPoints G α
val✝ : Fintype ↑(fixedPoints G α)
hpf : p ∣ card ↑(fixedPoints G α)
⊢ ∃ b, b ∈ fixedPoints G α ∧ a ≠ b
[PROOFSTEP]
have hα : 1 < card (fixedPoints G α) :=
  (Fact.out (p := p.Prime)).one_lt.trans_le (Nat.le_of_dvd (card_pos_iff.2 ⟨⟨a, ha⟩⟩) hpf)
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Fintype α
hpα : p ∣ card α
a : α
ha : a ∈ fixedPoints G α
val✝ : Fintype ↑(fixedPoints G α)
hpf : p ∣ card ↑(fixedPoints G α)
hα : 1 < card ↑(fixedPoints G α)
⊢ ∃ b, b ∈ fixedPoints G α ∧ a ≠ b
[PROOFSTEP]
exact
  let ⟨⟨b, hb⟩, hba⟩ := exists_ne_of_one_lt_card hα ⟨a, ha⟩
  ⟨b, hb, fun hab => hba (by simp_rw [hab])⟩
[GOAL]
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Fintype α
hpα : p ∣ card α
a : α
ha : a ∈ fixedPoints G α
val✝ : Fintype ↑(fixedPoints G α)
hpf : p ∣ card ↑(fixedPoints G α)
hα : 1 < card ↑(fixedPoints G α)
b : α
hb : b ∈ fixedPoints G α
hba : { val := b, property := hb } ≠ { val := a, property := ha }
hab : a = b
⊢ { val := b, property := hb } = { val := a, property := ha }
[PROOFSTEP]
simp_rw [hab]
[GOAL]
p : ℕ
G : Type u_1
inst✝⁴ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝³ : MulAction G α
inst✝² : Fintype α
inst✝¹ : Nontrivial G
inst✝ : Finite G
⊢ Nontrivial { x // x ∈ Subgroup.center G }
[PROOFSTEP]
classical
cases nonempty_fintype G
have := (hG.of_equiv ConjAct.toConjAct).exists_fixed_point_of_prime_dvd_card_of_fixed_point G
rw [ConjAct.fixedPoints_eq_center] at this
have dvd : p ∣ card G := by
  obtain ⟨n, hn0, hn⟩ := hG.nontrivial_iff_card.mp inferInstance
  exact hn.symm ▸ dvd_pow_self _ (ne_of_gt hn0)
obtain ⟨g, hg⟩ := this dvd (Subgroup.center G).one_mem
exact ⟨⟨1, ⟨g, hg.1⟩, mt Subtype.ext_iff.mp hg.2⟩⟩
[GOAL]
p : ℕ
G : Type u_1
inst✝⁴ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝³ : MulAction G α
inst✝² : Fintype α
inst✝¹ : Nontrivial G
inst✝ : Finite G
⊢ Nontrivial { x // x ∈ Subgroup.center G }
[PROOFSTEP]
cases nonempty_fintype G
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝⁴ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝³ : MulAction G α
inst✝² : Fintype α
inst✝¹ : Nontrivial G
inst✝ : Finite G
val✝ : Fintype G
⊢ Nontrivial { x // x ∈ Subgroup.center G }
[PROOFSTEP]
have := (hG.of_equiv ConjAct.toConjAct).exists_fixed_point_of_prime_dvd_card_of_fixed_point G
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝⁴ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝³ : MulAction G α
inst✝² : Fintype α
inst✝¹ : Nontrivial G
inst✝ : Finite G
val✝ : Fintype G
this : p ∣ card G → ∀ {a : G}, a ∈ fixedPoints (ConjAct G) G → ∃ b, b ∈ fixedPoints (ConjAct G) G ∧ a ≠ b
⊢ Nontrivial { x // x ∈ Subgroup.center G }
[PROOFSTEP]
rw [ConjAct.fixedPoints_eq_center] at this
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝⁴ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝³ : MulAction G α
inst✝² : Fintype α
inst✝¹ : Nontrivial G
inst✝ : Finite G
val✝ : Fintype G
this : p ∣ card G → ∀ {a : G}, a ∈ ↑(Subgroup.center G) → ∃ b, b ∈ ↑(Subgroup.center G) ∧ a ≠ b
⊢ Nontrivial { x // x ∈ Subgroup.center G }
[PROOFSTEP]
have dvd : p ∣ card G := by
  obtain ⟨n, hn0, hn⟩ := hG.nontrivial_iff_card.mp inferInstance
  exact hn.symm ▸ dvd_pow_self _ (ne_of_gt hn0)
[GOAL]
p : ℕ
G : Type u_1
inst✝⁴ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝³ : MulAction G α
inst✝² : Fintype α
inst✝¹ : Nontrivial G
inst✝ : Finite G
val✝ : Fintype G
this : p ∣ card G → ∀ {a : G}, a ∈ ↑(Subgroup.center G) → ∃ b, b ∈ ↑(Subgroup.center G) ∧ a ≠ b
⊢ p ∣ card G
[PROOFSTEP]
obtain ⟨n, hn0, hn⟩ := hG.nontrivial_iff_card.mp inferInstance
[GOAL]
case intro.intro
p : ℕ
G : Type u_1
inst✝⁴ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝³ : MulAction G α
inst✝² : Fintype α
inst✝¹ : Nontrivial G
inst✝ : Finite G
val✝ : Fintype G
this : p ∣ card G → ∀ {a : G}, a ∈ ↑(Subgroup.center G) → ∃ b, b ∈ ↑(Subgroup.center G) ∧ a ≠ b
n : ℕ
hn0 : n > 0
hn : card G = p ^ n
⊢ p ∣ card G
[PROOFSTEP]
exact hn.symm ▸ dvd_pow_self _ (ne_of_gt hn0)
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝⁴ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝³ : MulAction G α
inst✝² : Fintype α
inst✝¹ : Nontrivial G
inst✝ : Finite G
val✝ : Fintype G
this : p ∣ card G → ∀ {a : G}, a ∈ ↑(Subgroup.center G) → ∃ b, b ∈ ↑(Subgroup.center G) ∧ a ≠ b
dvd : p ∣ card G
⊢ Nontrivial { x // x ∈ Subgroup.center G }
[PROOFSTEP]
obtain ⟨g, hg⟩ := this dvd (Subgroup.center G).one_mem
[GOAL]
case intro.intro
p : ℕ
G : Type u_1
inst✝⁴ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝³ : MulAction G α
inst✝² : Fintype α
inst✝¹ : Nontrivial G
inst✝ : Finite G
val✝ : Fintype G
this : p ∣ card G → ∀ {a : G}, a ∈ ↑(Subgroup.center G) → ∃ b, b ∈ ↑(Subgroup.center G) ∧ a ≠ b
dvd : p ∣ card G
g : G
hg : g ∈ ↑(Subgroup.center G) ∧ 1 ≠ g
⊢ Nontrivial { x // x ∈ Subgroup.center G }
[PROOFSTEP]
exact ⟨⟨1, ⟨g, hg.1⟩, mt Subtype.ext_iff.mp hg.2⟩⟩
[GOAL]
p : ℕ
G : Type u_1
inst✝⁴ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝³ : MulAction G α
inst✝² : Fintype α
inst✝¹ : Nontrivial G
inst✝ : Finite G
⊢ ⊥ < Subgroup.center G
[PROOFSTEP]
haveI := center_nontrivial hG
[GOAL]
p : ℕ
G : Type u_1
inst✝⁴ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝³ : MulAction G α
inst✝² : Fintype α
inst✝¹ : Nontrivial G
inst✝ : Finite G
this : Nontrivial { x // x ∈ Subgroup.center G }
⊢ ⊥ < Subgroup.center G
[PROOFSTEP]
cases nonempty_fintype G
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝⁴ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝³ : MulAction G α
inst✝² : Fintype α
inst✝¹ : Nontrivial G
inst✝ : Finite G
this : Nontrivial { x // x ∈ Subgroup.center G }
val✝ : Fintype G
⊢ ⊥ < Subgroup.center G
[PROOFSTEP]
classical exact bot_lt_iff_ne_bot.mpr ((Subgroup.center G).one_lt_card_iff_ne_bot.mp Fintype.one_lt_card)
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝⁴ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝³ : MulAction G α
inst✝² : Fintype α
inst✝¹ : Nontrivial G
inst✝ : Finite G
this : Nontrivial { x // x ∈ Subgroup.center G }
val✝ : Fintype G
⊢ ⊥ < Subgroup.center G
[PROOFSTEP]
exact bot_lt_iff_ne_bot.mpr ((Subgroup.center G).one_lt_card_iff_ne_bot.mp Fintype.one_lt_card)
[GOAL]
p : ℕ
G : Type u_1
inst✝ : Group G
H K : Subgroup G
hK : IsPGroup p { x // x ∈ K }
hHK : H ≤ K
a b : { x // x ∈ H }
h : ↑(Subgroup.inclusion hHK) a = ↑(Subgroup.inclusion hHK) b
⊢ ↑a = ↑b
[PROOFSTEP]
change ((Subgroup.inclusion hHK) a : G) = (Subgroup.inclusion hHK) b
[GOAL]
p : ℕ
G : Type u_1
inst✝ : Group G
H K : Subgroup G
hK : IsPGroup p { x // x ∈ K }
hHK : H ≤ K
a b : { x // x ∈ H }
h : ↑(Subgroup.inclusion hHK) a = ↑(Subgroup.inclusion hHK) b
⊢ ↑(↑(Subgroup.inclusion hHK) a) = ↑(↑(Subgroup.inclusion hHK) b)
[PROOFSTEP]
apply Subtype.ext_iff.mp h
[GOAL]
p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p { x // x ∈ H }
K : Type u_2
inst✝ : Group K
ϕ : G →* K
⊢ IsPGroup p { x // x ∈ Subgroup.map ϕ H }
[PROOFSTEP]
rw [← H.subtype_range, MonoidHom.map_range]
[GOAL]
p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p { x // x ∈ H }
K : Type u_2
inst✝ : Group K
ϕ : G →* K
⊢ IsPGroup p { x // x ∈ MonoidHom.range (MonoidHom.comp ϕ (Subgroup.subtype H)) }
[PROOFSTEP]
exact hH.of_surjective (ϕ.restrict H).rangeRestrict (ϕ.restrict H).rangeRestrict_surjective
[GOAL]
p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p { x // x ∈ H }
K : Type u_2
inst✝ : Group K
ϕ : K →* G
hϕ : IsPGroup p { x // x ∈ MonoidHom.ker ϕ }
⊢ IsPGroup p { x // x ∈ Subgroup.comap ϕ H }
[PROOFSTEP]
intro g
[GOAL]
p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p { x // x ∈ H }
K : Type u_2
inst✝ : Group K
ϕ : K →* G
hϕ : IsPGroup p { x // x ∈ MonoidHom.ker ϕ }
g : { x // x ∈ Subgroup.comap ϕ H }
⊢ ∃ k, g ^ p ^ k = 1
[PROOFSTEP]
obtain ⟨j, hj⟩ := hH ⟨ϕ g.1, g.2⟩
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p { x // x ∈ H }
K : Type u_2
inst✝ : Group K
ϕ : K →* G
hϕ : IsPGroup p { x // x ∈ MonoidHom.ker ϕ }
g : { x // x ∈ Subgroup.comap ϕ H }
j : ℕ
hj : { val := ↑ϕ ↑g, property := (_ : ↑g ∈ Subgroup.comap ϕ H) } ^ p ^ j = 1
⊢ ∃ k, g ^ p ^ k = 1
[PROOFSTEP]
rw [Subtype.ext_iff, H.coe_pow, Subtype.coe_mk, ← ϕ.map_pow] at hj
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p { x // x ∈ H }
K : Type u_2
inst✝ : Group K
ϕ : K →* G
hϕ : IsPGroup p { x // x ∈ MonoidHom.ker ϕ }
g : { x // x ∈ Subgroup.comap ϕ H }
j : ℕ
hj : ↑ϕ (↑g ^ p ^ j) = ↑1
⊢ ∃ k, g ^ p ^ k = 1
[PROOFSTEP]
obtain ⟨k, hk⟩ := hϕ ⟨g.1 ^ p ^ j, hj⟩
[GOAL]
case intro.intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p { x // x ∈ H }
K : Type u_2
inst✝ : Group K
ϕ : K →* G
hϕ : IsPGroup p { x // x ∈ MonoidHom.ker ϕ }
g : { x // x ∈ Subgroup.comap ϕ H }
j : ℕ
hj : ↑ϕ (↑g ^ p ^ j) = ↑1
k : ℕ
hk : { val := ↑g ^ p ^ j, property := hj } ^ p ^ k = 1
⊢ ∃ k, g ^ p ^ k = 1
[PROOFSTEP]
rw [Subtype.ext_iff, ϕ.ker.coe_pow, Subtype.coe_mk, ← pow_mul, ← pow_add] at hk
[GOAL]
case intro.intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p { x // x ∈ H }
K : Type u_2
inst✝ : Group K
ϕ : K →* G
hϕ : IsPGroup p { x // x ∈ MonoidHom.ker ϕ }
g : { x // x ∈ Subgroup.comap ϕ H }
j : ℕ
hj : ↑ϕ (↑g ^ p ^ j) = ↑1
k : ℕ
hk : ↑g ^ p ^ (j + k) = ↑1
⊢ ∃ k, g ^ p ^ k = 1
[PROOFSTEP]
exact ⟨j + k, by rwa [Subtype.ext_iff, (H.comap ϕ).coe_pow]⟩
[GOAL]
p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p { x // x ∈ H }
K : Type u_2
inst✝ : Group K
ϕ : K →* G
hϕ : IsPGroup p { x // x ∈ MonoidHom.ker ϕ }
g : { x // x ∈ Subgroup.comap ϕ H }
j : ℕ
hj : ↑ϕ (↑g ^ p ^ j) = ↑1
k : ℕ
hk : ↑g ^ p ^ (j + k) = ↑1
⊢ g ^ p ^ (j + k) = 1
[PROOFSTEP]
rwa [Subtype.ext_iff, (H.comap ϕ).coe_pow]
[GOAL]
p : ℕ
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
hH : IsPGroup p { x // x ∈ H }
hK : IsPGroup p { x // x ∈ K }
inst✝ : Subgroup.Normal K
⊢ IsPGroup p { x // x ∈ H ⊔ K }
[PROOFSTEP]
rw [← QuotientGroup.ker_mk' K, ← Subgroup.comap_map_eq]
[GOAL]
p : ℕ
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
hH : IsPGroup p { x // x ∈ H }
hK : IsPGroup p { x // x ∈ K }
inst✝ : Subgroup.Normal K
⊢ IsPGroup p { x // x ∈ Subgroup.comap (QuotientGroup.mk' K) (Subgroup.map (QuotientGroup.mk' K) H) }
[PROOFSTEP]
apply (hH.map (QuotientGroup.mk' K)).comap_of_ker_isPGroup
[GOAL]
case hϕ
p : ℕ
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
hH : IsPGroup p { x // x ∈ H }
hK : IsPGroup p { x // x ∈ K }
inst✝ : Subgroup.Normal K
⊢ IsPGroup p { x // x ∈ MonoidHom.ker (QuotientGroup.mk' K) }
[PROOFSTEP]
rwa [QuotientGroup.ker_mk']
[GOAL]
p : ℕ
G : Type u_1
inst✝³ : Group G
G₂ : Type u_2
inst✝² : Group G₂
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ : Subgroup G
H₂ : Subgroup G₂
inst✝¹ : Fintype { x // x ∈ H₁ }
inst✝ : Fintype { x // x ∈ H₂ }
hH₁ : IsPGroup p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
⊢ Nat.coprime (card { x // x ∈ H₁ }) (card { x // x ∈ H₂ })
[PROOFSTEP]
obtain ⟨n₁, heq₁⟩ := iff_card.mp hH₁
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝³ : Group G
G₂ : Type u_2
inst✝² : Group G₂
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ : Subgroup G
H₂ : Subgroup G₂
inst✝¹ : Fintype { x // x ∈ H₁ }
inst✝ : Fintype { x // x ∈ H₂ }
hH₁ : IsPGroup p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
n₁ : ℕ
heq₁ : card { x // x ∈ H₁ } = p₁ ^ n₁
⊢ Nat.coprime (card { x // x ∈ H₁ }) (card { x // x ∈ H₂ })
[PROOFSTEP]
rw [heq₁]
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝³ : Group G
G₂ : Type u_2
inst✝² : Group G₂
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ : Subgroup G
H₂ : Subgroup G₂
inst✝¹ : Fintype { x // x ∈ H₁ }
inst✝ : Fintype { x // x ∈ H₂ }
hH₁ : IsPGroup p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
n₁ : ℕ
heq₁ : card { x // x ∈ H₁ } = p₁ ^ n₁
⊢ Nat.coprime (p₁ ^ n₁) (card { x // x ∈ H₂ })
[PROOFSTEP]
clear heq₁
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝³ : Group G
G₂ : Type u_2
inst✝² : Group G₂
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ : Subgroup G
H₂ : Subgroup G₂
inst✝¹ : Fintype { x // x ∈ H₁ }
inst✝ : Fintype { x // x ∈ H₂ }
hH₁ : IsPGroup p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
n₁ : ℕ
⊢ Nat.coprime (p₁ ^ n₁) (card { x // x ∈ H₂ })
[PROOFSTEP]
obtain ⟨n₂, heq₂⟩ := iff_card.mp hH₂
[GOAL]
case intro.intro
p : ℕ
G : Type u_1
inst✝³ : Group G
G₂ : Type u_2
inst✝² : Group G₂
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ : Subgroup G
H₂ : Subgroup G₂
inst✝¹ : Fintype { x // x ∈ H₁ }
inst✝ : Fintype { x // x ∈ H₂ }
hH₁ : IsPGroup p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
n₁ n₂ : ℕ
heq₂ : card { x // x ∈ H₂ } = p₂ ^ n₂
⊢ Nat.coprime (p₁ ^ n₁) (card { x // x ∈ H₂ })
[PROOFSTEP]
rw [heq₂]
[GOAL]
case intro.intro
p : ℕ
G : Type u_1
inst✝³ : Group G
G₂ : Type u_2
inst✝² : Group G₂
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ : Subgroup G
H₂ : Subgroup G₂
inst✝¹ : Fintype { x // x ∈ H₁ }
inst✝ : Fintype { x // x ∈ H₂ }
hH₁ : IsPGroup p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
n₁ n₂ : ℕ
heq₂ : card { x // x ∈ H₂ } = p₂ ^ n₂
⊢ Nat.coprime (p₁ ^ n₁) (p₂ ^ n₂)
[PROOFSTEP]
clear heq₂
[GOAL]
case intro.intro
p : ℕ
G : Type u_1
inst✝³ : Group G
G₂ : Type u_2
inst✝² : Group G₂
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ : Subgroup G
H₂ : Subgroup G₂
inst✝¹ : Fintype { x // x ∈ H₁ }
inst✝ : Fintype { x // x ∈ H₂ }
hH₁ : IsPGroup p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
n₁ n₂ : ℕ
⊢ Nat.coprime (p₁ ^ n₁) (p₂ ^ n₂)
[PROOFSTEP]
exact Nat.coprime_pow_primes _ _ hp₁.elim hp₂.elim hne
[GOAL]
p : ℕ
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 p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
⊢ Disjoint H₁ H₂
[PROOFSTEP]
rw [Subgroup.disjoint_def]
[GOAL]
p : ℕ
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 p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
⊢ ∀ {x : G}, x ∈ H₁ → x ∈ H₂ → x = 1
[PROOFSTEP]
intro x hx₁ hx₂
[GOAL]
p : ℕ
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 p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
x : G
hx₁ : x ∈ H₁
hx₂ : x ∈ H₂
⊢ x = 1
[PROOFSTEP]
obtain ⟨n₁, hn₁⟩ := iff_orderOf.mp hH₁ ⟨x, hx₁⟩
[GOAL]
case intro
p : ℕ
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 p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
x : G
hx₁ : x ∈ H₁
hx₂ : x ∈ H₂
n₁ : ℕ
hn₁ : orderOf { val := x, property := hx₁ } = p₁ ^ n₁
⊢ x = 1
[PROOFSTEP]
obtain ⟨n₂, hn₂⟩ := iff_orderOf.mp hH₂ ⟨x, hx₂⟩
[GOAL]
case intro.intro
p : ℕ
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 p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
x : G
hx₁ : x ∈ H₁
hx₂ : x ∈ H₂
n₁ : ℕ
hn₁ : orderOf { val := x, property := hx₁ } = p₁ ^ n₁
n₂ : ℕ
hn₂ : orderOf { val := x, property := hx₂ } = p₂ ^ n₂
⊢ x = 1
[PROOFSTEP]
rw [← orderOf_subgroup, Subgroup.coe_mk] at hn₁ hn₂
[GOAL]
case intro.intro
p : ℕ
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 p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
x : G
hx₁ : x ∈ H₁
hx₂ : x ∈ H₂
n₁ : ℕ
hn₁ : orderOf x = p₁ ^ n₁
n₂ : ℕ
hn₂ : orderOf x = p₂ ^ n₂
⊢ x = 1
[PROOFSTEP]
have : p₁ ^ n₁ = p₂ ^ n₂ := by rw [← hn₁, ← hn₂]
[GOAL]
p : ℕ
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 p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ 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₂
[PROOFSTEP]
rw [← hn₁, ← hn₂]
[GOAL]
case intro.intro
p : ℕ
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 p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ 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₂
⊢ x = 1
[PROOFSTEP]
rcases n₁.eq_zero_or_pos with (rfl | hn₁)
[GOAL]
case intro.intro.inl
p : ℕ
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 p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
x : G
hx₁ : x ∈ H₁
hx₂ : x ∈ H₂
n₂ : ℕ
hn₂ : orderOf x = p₂ ^ n₂
hn₁ : orderOf x = p₁ ^ 0
this : p₁ ^ 0 = p₂ ^ n₂
⊢ x = 1
[PROOFSTEP]
simpa using hn₁
[GOAL]
case intro.intro.inr
p : ℕ
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 p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ 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₂
hn₁ : n₁ > 0
⊢ x = 1
[PROOFSTEP]
exact absurd (eq_of_prime_pow_eq hp₁.out.prime hp₂.out.prime hn₁ this) hne
[GOAL]
p : ℕ
G : Type u_1
inst✝³ : Group G
inst✝² : Fintype G
inst✝¹ : Fact (Nat.Prime p)
n : ℕ
hGpn : card G = p ^ n
hn : 0 < n
inst✝ : Fintype { x // x ∈ center G }
⊢ ∃ k, k > 0 ∧ card { x // x ∈ center G } = p ^ k
[PROOFSTEP]
have hcG := to_subgroup (of_card hGpn) (center G)
[GOAL]
p : ℕ
G : Type u_1
inst✝³ : Group G
inst✝² : Fintype G
inst✝¹ : Fact (Nat.Prime p)
n : ℕ
hGpn : card G = p ^ n
hn : 0 < n
inst✝ : Fintype { x // x ∈ center G }
hcG : IsPGroup p { x // x ∈ center G }
⊢ ∃ k, k > 0 ∧ card { x // x ∈ center G } = p ^ k
[PROOFSTEP]
rcases iff_card.1 hcG with _
[GOAL]
p : ℕ
G : Type u_1
inst✝³ : Group G
inst✝² : Fintype G
inst✝¹ : Fact (Nat.Prime p)
n : ℕ
hGpn : card G = p ^ n
hn : 0 < n
inst✝ : Fintype { x // x ∈ center G }
hcG : IsPGroup p { x // x ∈ center G }
x✝ : ∃ n, card { x // x ∈ center G } = p ^ n
⊢ ∃ k, k > 0 ∧ card { x // x ∈ center G } = p ^ k
[PROOFSTEP]
haveI : Nontrivial G := (nontrivial_iff_card <| of_card hGpn).2 ⟨n, hn, hGpn⟩
[GOAL]
p : ℕ
G : Type u_1
inst✝³ : Group G
inst✝² : Fintype G
inst✝¹ : Fact (Nat.Prime p)
n : ℕ
hGpn : card G = p ^ n
hn : 0 < n
inst✝ : Fintype { x // x ∈ center G }
hcG : IsPGroup p { x // x ∈ center G }
x✝ : ∃ n, card { x // x ∈ center G } = p ^ n
this : Nontrivial G
⊢ ∃ k, k > 0 ∧ card { x // x ∈ center G } = p ^ k
[PROOFSTEP]
exact (nontrivial_iff_card hcG).mp (center_nontrivial (of_card hGpn))
[GOAL]
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Fact (Nat.Prime p)
n : ℕ
hGpn : card G = p ^ n
hG : card G = p ^ 2
⊢ IsCyclic (G ⧸ center G)
[PROOFSTEP]
classical
rcases card_center_eq_prime_pow hG zero_lt_two with ⟨k, hk0, hk⟩
rw [card_eq_card_quotient_mul_card_subgroup (center G), mul_comm, hk] at hG
have hk2 := (Nat.pow_dvd_pow_iff_le_right (Fact.out (p := p.Prime)).one_lt).1 ⟨_, hG.symm⟩
interval_cases k
· rw [sq, pow_one, mul_right_inj' (Fact.out (p := p.Prime)).ne_zero] at hG
  exact isCyclic_of_prime_card hG
·
  exact
    @isCyclic_of_subsingleton _ _
      ⟨Fintype.card_le_one_iff.1
          (mul_right_injective₀ (pow_ne_zero 2 (NeZero.ne p)) (hG.trans (mul_one (p ^ 2)).symm)).le⟩
[GOAL]
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Fact (Nat.Prime p)
n : ℕ
hGpn : card G = p ^ n
hG : card G = p ^ 2
⊢ IsCyclic (G ⧸ center G)
[PROOFSTEP]
rcases card_center_eq_prime_pow hG zero_lt_two with ⟨k, hk0, hk⟩
[GOAL]
case intro.intro
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Fact (Nat.Prime p)
n : ℕ
hGpn : card G = p ^ n
hG : card G = p ^ 2
k : ℕ
hk0 : k > 0
hk : card { x // x ∈ center G } = p ^ k
⊢ IsCyclic (G ⧸ center G)
[PROOFSTEP]
rw [card_eq_card_quotient_mul_card_subgroup (center G), mul_comm, hk] at hG
[GOAL]
case intro.intro
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Fact (Nat.Prime p)
n : ℕ
hGpn : card G = p ^ n
k : ℕ
hG : p ^ k * card (G ⧸ center G) = p ^ 2
hk0 : k > 0
hk : card { x // x ∈ center G } = p ^ k
⊢ IsCyclic (G ⧸ center G)
[PROOFSTEP]
have hk2 := (Nat.pow_dvd_pow_iff_le_right (Fact.out (p := p.Prime)).one_lt).1 ⟨_, hG.symm⟩
[GOAL]
case intro.intro
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Fact (Nat.Prime p)
n : ℕ
hGpn : card G = p ^ n
k : ℕ
hG : p ^ k * card (G ⧸ center G) = p ^ 2
hk0 : k > 0
hk : card { x // x ∈ center G } = p ^ k
hk2 : k ≤ 2
⊢ IsCyclic (G ⧸ center G)
[PROOFSTEP]
interval_cases k
[GOAL]
case intro.intro.«1»
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Fact (Nat.Prime p)
n : ℕ
hGpn : card G = p ^ n
k : ℕ
hG : p ^ 1 * card (G ⧸ center G) = p ^ 2
hk0 : 1 > 0
hk : card { x // x ∈ center G } = p ^ 1
hk2 : 1 ≤ 2
⊢ IsCyclic (G ⧸ center G)
[PROOFSTEP]
rw [sq, pow_one, mul_right_inj' (Fact.out (p := p.Prime)).ne_zero] at hG
[GOAL]
case intro.intro.«1»
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Fact (Nat.Prime p)
n : ℕ
hGpn : card G = p ^ n
k : ℕ
hG : card (G ⧸ center G) = p
hk0 : 1 > 0
hk : card { x // x ∈ center G } = p ^ 1
hk2 : 1 ≤ 2
⊢ IsCyclic (G ⧸ center G)
[PROOFSTEP]
exact isCyclic_of_prime_card hG
[GOAL]
case intro.intro.«2»
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Fact (Nat.Prime p)
n : ℕ
hGpn : card G = p ^ n
k : ℕ
hG : p ^ 2 * card (G ⧸ center G) = p ^ 2
hk0 : 2 > 0
hk : card { x // x ∈ center G } = p ^ 2
hk2 : 2 ≤ 2
⊢ IsCyclic (G ⧸ center G)
[PROOFSTEP]
exact
  @isCyclic_of_subsingleton _ _
    ⟨Fintype.card_le_one_iff.1
        (mul_right_injective₀ (pow_ne_zero 2 (NeZero.ne p)) (hG.trans (mul_one (p ^ 2)).symm)).le⟩