case intro
R✝ : Type ?u.957555
inst✝³ : NonAssocRing R✝
inst✝² : Fintype R✝
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Fintype R
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : Fintype.card R = p ^ n
hR : ∀ (i : ℕ), i ≤ n → ↑(p ^ i) = 0 → i = n
c : ℕ
hc : CharP R c
⊢ CharP R (p ^ n)
R✝ : Type ?u.957555
inst✝³ : NonAssocRing R✝
inst✝² : Fintype R✝
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Fintype R
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : Fintype.card R = p ^ n
hR : ∀ (i : ℕ), i ≤ n → ↑(p ^ i) = 0 → i = n
⊢ CharP R (p ^ n)
obtain ⟨c, hc⟩ := CharP.exists R
case intro
R✝ : Type ?u.957555
inst✝³ : NonAssocRing R✝
inst✝² : Fintype R✝
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Fintype R
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : Fintype.card R = p ^ n
hR : ∀ (i : ℕ), i ≤ n → ↑(p ^ i) = 0 → i = n
c : ℕ
hc : CharP R c
⊢ CharP R (p ^ n)
case intro
R✝ : Type ?u.957555
inst✝³ : NonAssocRing R✝
inst✝² : Fintype R✝
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Fintype R
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : Fintype.card R = p ^ n
hR : ∀ (i : ℕ), i ≤ n → ↑(p ^ i) = 0 → i = n
c : ℕ
hc : CharP R c
⊢ CharP R (p ^ n)
skip
case intro
R✝ : Type ?u.957555
inst✝³ : NonAssocRing R✝
inst✝² : Fintype R✝
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Fintype R
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : Fintype.card R = p ^ n
hR : ∀ (i : ℕ), i ≤ n → ↑(p ^ i) = 0 → i = n
c : ℕ
hc : CharP R c
hcpn : c ∣ p ^ n
⊢ CharP R (p ^ n)
case intro
R✝ : Type ?u.957555
inst✝³ : NonAssocRing R✝
inst✝² : Fintype R✝
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Fintype R
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : Fintype.card R = p ^ n
hR : ∀ (i : ℕ), i ≤ n → ↑(p ^ i) = 0 → i = n
c : ℕ
hc : CharP R c
⊢ CharP R (p ^ n)
have hcpn : c ∣ p ^ n := by rw [← CharP.cast_eq_zero_iff R c, ← hn, CharP.cast_card_eq_zero]
case intro.intro.intro
R✝ : Type ?u.957555
inst✝³ : NonAssocRing R✝
inst✝² : Fintype R✝
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Fintype R
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : Fintype.card R = p ^ n
hR : ∀ (i : ℕ), i ≤ n → ↑(p ^ i) = 0 → i = n
c : ℕ
hc✝ : CharP R c
hcpn : c ∣ p ^ n
i : ℕ
hi : i ≤ n
hc : c = p ^ i
⊢ CharP R (p ^ n)
case intro
R✝ : Type ?u.957555
inst✝³ : NonAssocRing R✝
inst✝² : Fintype R✝
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Fintype R
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : Fintype.card R = p ^ n
hR : ∀ (i : ℕ), i ≤ n → ↑(p ^ i) = 0 → i = n
c : ℕ
hc : CharP R c
hcpn : c ∣ p ^ n
⊢ CharP R (p ^ n)
obtain ⟨i, hi, hc⟩ : ∃ i ≤ n, c = p ^ i := by rwa [Nat.dvd_prime_pow hp.1] at hcpn
case intro.intro.intro
R✝ : Type ?u.957555
inst✝³ : NonAssocRing R✝
inst✝² : Fintype R✝
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Fintype R
p : ℕ
hp : Fact (Nat.Prime p)
c : ℕ
hc✝ : CharP R c
i : ℕ
hc : c = p ^ i
hn : Fintype.card R = p ^ i
hR : ∀ (i_1 : ℕ), i_1 ≤ i → ↑(p ^ i_1) = 0 → i_1 = i
hcpn : c ∣ p ^ i
hi : i ≤ i
⊢ CharP R (p ^ i)
case intro.intro.intro
R✝ : Type ?u.957555
inst✝³ : NonAssocRing R✝
inst✝² : Fintype R✝
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Fintype R
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : Fintype.card R = p ^ n
hR : ∀ (i : ℕ), i ≤ n → ↑(p ^ i) = 0 → i = n
c : ℕ
hc✝ : CharP R c
hcpn : c ∣ p ^ n
i : ℕ
hi : i ≤ n
hc : c = p ^ i
⊢ CharP R (p ^ n)
obtain rfl : i = n := by
  apply hR i hi
  rw [← hc, CharP.cast_eq_zero]
no goals
case intro.intro.intro
R✝ : Type ?u.957555
inst✝³ : NonAssocRing R✝
inst✝² : Fintype R✝
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Fintype R
p : ℕ
hp : Fact (Nat.Prime p)
c : ℕ
hc✝ : CharP R c
i : ℕ
hc : c = p ^ i
hn : Fintype.card R = p ^ i
hR : ∀ (i_1 : ℕ), i_1 ≤ i → ↑(p ^ i_1) = 0 → i_1 = i
hcpn : c ∣ p ^ i
hi : i ≤ i
⊢ CharP R (p ^ i)
rwa [← hc]
no goals
R✝ : Type ?u.957555
inst✝³ : NonAssocRing R✝
inst✝² : Fintype R✝
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Fintype R
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : Fintype.card R = p ^ n
hR : ∀ (i : ℕ), i ≤ n → ↑(p ^ i) = 0 → i = n
c : ℕ
hc : CharP R c
⊢ c ∣ p ^ n
rw [← CharP.cast_eq_zero_iff R c, ← hn, CharP.cast_card_eq_zero]
no goals
R✝ : Type ?u.957555
inst✝³ : NonAssocRing R✝
inst✝² : Fintype R✝
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Fintype R
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : Fintype.card R = p ^ n
hR : ∀ (i : ℕ), i ≤ n → ↑(p ^ i) = 0 → i = n
c : ℕ
hc : CharP R c
hcpn : c ∣ p ^ n
⊢ ∃ i, i ≤ n ∧ c = p ^ i
rwa [Nat.dvd_prime_pow hp.1] at hcpn
R✝ : Type ?u.957555
inst✝³ : NonAssocRing R✝
inst✝² : Fintype R✝
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Fintype R
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : Fintype.card R = p ^ n
hR : ∀ (i : ℕ), i ≤ n → ↑(p ^ i) = 0 → i = n
c : ℕ
hc✝ : CharP R c
hcpn : c ∣ p ^ n
i : ℕ
hi : i ≤ n
hc : c = p ^ i
⊢ ↑(p ^ i) = 0
R✝ : Type ?u.957555
inst✝³ : NonAssocRing R✝
inst✝² : Fintype R✝
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Fintype R
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : Fintype.card R = p ^ n
hR : ∀ (i : ℕ), i ≤ n → ↑(p ^ i) = 0 → i = n
c : ℕ
hc✝ : CharP R c
hcpn : c ∣ p ^ n
i : ℕ
hi : i ≤ n
hc : c = p ^ i
⊢ i = n
apply hR i hi
no goals
R✝ : Type ?u.957555
inst✝³ : NonAssocRing R✝
inst✝² : Fintype R✝
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Fintype R
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : Fintype.card R = p ^ n
hR : ∀ (i : ℕ), i ≤ n → ↑(p ^ i) = 0 → i = n
c : ℕ
hc✝ : CharP R c
hcpn : c ∣ p ^ n
i : ℕ
hi : i ≤ n
hc : c = p ^ i
⊢ ↑(p ^ i) = 0
rw [← hc, CharP.cast_eq_zero]