case mp
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
⊢ (∃ I, I ≠ ⊤ ∧ CharP (R ⧸ I) p) → ∃ I, Ideal.IsMaximal I ∧ CharP (R ⧸ I) p

case mpr
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
⊢ (∃ I, Ideal.IsMaximal I ∧ CharP (R ⧸ I) p) → ∃ I, I ≠ ⊤ ∧ CharP (R ⧸ I) p
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
⊢ (∃ I, I ≠ ⊤ ∧ CharP (R ⧸ I) p) ↔ ∃ I, Ideal.IsMaximal I ∧ CharP (R ⧸ I) p
constructor
case mp
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
g : ∃ I, I ≠ ⊤ ∧ CharP (R ⧸ I) p
⊢ ∃ I, Ideal.IsMaximal I ∧ CharP (R ⧸ I) p
case mp
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
⊢ (∃ I, I ≠ ⊤ ∧ CharP (R ⧸ I) p) → ∃ I, Ideal.IsMaximal I ∧ CharP (R ⧸ I) p
intro g
case mp.intro.intro
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
I : Ideal R
hI_not_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) p
⊢ ∃ I, Ideal.IsMaximal I ∧ CharP (R ⧸ I) p
case mp
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
g : ∃ I, I ≠ ⊤ ∧ CharP (R ⧸ I) p
⊢ ∃ I, Ideal.IsMaximal I ∧ CharP (R ⧸ I) p
rcases g with ⟨I, ⟨hI_not_top, _⟩⟩
case mp.intro.intro.intro.intro
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
I : Ideal R
hI_not_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) p
M : Ideal R
hM_max : Ideal.IsMaximal M
hM_ge : I ≤ M
⊢ ∃ I, Ideal.IsMaximal I ∧ CharP (R ⧸ I) p
case mp.intro.intro
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
I : Ideal R
hI_not_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) p
⊢ ∃ I, Ideal.IsMaximal I ∧ CharP (R ⧸ I) p
rcases Ideal.exists_le_maximal I hI_not_top with ⟨M, ⟨hM_max, hM_ge⟩⟩
case mp.intro.intro.intro.intro
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
I : Ideal R
hI_not_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) p
M : Ideal R
hM_max : Ideal.IsMaximal M
hM_ge : I ≤ M
⊢ Ideal.IsMaximal M ∧ CharP (R ⧸ M) p
case mp.intro.intro.intro.intro
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
I : Ideal R
hI_not_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) p
M : Ideal R
hM_max : Ideal.IsMaximal M
hM_ge : I ≤ M
⊢ ∃ I, Ideal.IsMaximal I ∧ CharP (R ⧸ I) p
use M
case mp.intro.intro.intro.intro.left
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
I : Ideal R
hI_not_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) p
M : Ideal R
hM_max : Ideal.IsMaximal M
hM_ge : I ≤ M
⊢ Ideal.IsMaximal M

case mp.intro.intro.intro.intro.right
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
I : Ideal R
hI_not_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) p
M : Ideal R
hM_max : Ideal.IsMaximal M
hM_ge : I ≤ M
⊢ CharP (R ⧸ M) p
case mp.intro.intro.intro.intro
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
I : Ideal R
hI_not_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) p
M : Ideal R
hM_max : Ideal.IsMaximal M
hM_ge : I ≤ M
⊢ Ideal.IsMaximal M ∧ CharP (R ⧸ M) p
constructor
no goals
case mp.intro.intro.intro.intro.left
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
I : Ideal R
hI_not_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) p
M : Ideal R
hM_max : Ideal.IsMaximal M
hM_ge : I ≤ M
⊢ Ideal.IsMaximal M
exact hM_max
case mp.intro.intro.intro.intro.right.intro
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
I : Ideal R
hI_not_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) p
M : Ideal R
hM_max : Ideal.IsMaximal M
hM_ge : I ≤ M
r : ℕ
hr✝ hr : CharP (R ⧸ M) r
⊢ CharP (R ⧸ M) p
case mp.intro.intro.intro.intro.right.intro
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
I : Ideal R
hI_not_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) p
M : Ideal R
hM_max : Ideal.IsMaximal M
hM_ge : I ≤ M
r : ℕ
hr : CharP (R ⧸ M) r
⊢ CharP (R ⧸ M) p
have hr := hr
case h.e'_3
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
I : Ideal R
hI_not_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) p
M : Ideal R
hM_max : Ideal.IsMaximal M
hM_ge : I ≤ M
r : ℕ
hr✝ hr : CharP (R ⧸ M) r
⊢ p = r
case mp.intro.intro.intro.intro.right.intro
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
I : Ideal R
hI_not_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) p
M : Ideal R
hM_max : Ideal.IsMaximal M
hM_ge : I ≤ M
r : ℕ
hr✝ hr : CharP (R ⧸ M) r
⊢ CharP (R ⧸ M) p
convert hr
case r_dvd_p
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
I : Ideal R
hI_not_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) p
M : Ideal R
hM_max : Ideal.IsMaximal M
hM_ge : I ≤ M
r : ℕ
hr✝ hr : CharP (R ⧸ M) r
⊢ r ∣ p

case h.e'_3
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
I : Ideal R
hI_not_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) p
M : Ideal R
hM_max : Ideal.IsMaximal M
hM_ge : I ≤ M
r : ℕ
hr✝ hr : CharP (R ⧸ M) r
r_dvd_p : r ∣ p
⊢ p = r
case h.e'_3
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
I : Ideal R
hI_not_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) p
M : Ideal R
hM_max : Ideal.IsMaximal M
hM_ge : I ≤ M
r : ℕ
hr✝ hr : CharP (R ⧸ M) r
⊢ p = r
have r_dvd_p : r ∣ p
case h.e'_3
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
I : Ideal R
hI_not_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) p
M : Ideal R
hM_max : Ideal.IsMaximal M
hM_ge : I ≤ M
r : ℕ
hr✝ hr : CharP (R ⧸ M) r
r_dvd_p : r ∣ p
⊢ r = p
case h.e'_3
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
I : Ideal R
hI_not_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) p
M : Ideal R
hM_max : Ideal.IsMaximal M
hM_ge : I ≤ M
r : ℕ
hr✝ hr : CharP (R ⧸ M) r
r_dvd_p : r ∣ p
⊢ p = r
symm
case h.e'_3
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
I : Ideal R
hI_not_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) p
M : Ideal R
hM_max : Ideal.IsMaximal M
hM_ge : I ≤ M
r : ℕ
hr✝ hr : CharP (R ⧸ M) r
r_dvd_p : r ∣ p
⊢ ¬r = 1
case h.e'_3
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
I : Ideal R
hI_not_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) p
M : Ideal R
hM_max : Ideal.IsMaximal M
hM_ge : I ≤ M
r : ℕ
hr✝ hr : CharP (R ⧸ M) r
r_dvd_p : r ∣ p
⊢ r = p
apply (Nat.Prime.eq_one_or_self_of_dvd hp r r_dvd_p).resolve_left
no goals
case h.e'_3
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
I : Ideal R
hI_not_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) p
M : Ideal R
hM_max : Ideal.IsMaximal M
hM_ge : I ≤ M
r : ℕ
hr✝ hr : CharP (R ⧸ M) r
r_dvd_p : r ∣ p
⊢ ¬r = 1
exact CharP.char_ne_one (R ⧸ M) r
case r_dvd_p
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
I : Ideal R
hI_not_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) p
M : Ideal R
hM_max : Ideal.IsMaximal M
hM_ge : I ≤ M
r : ℕ
hr✝ hr : CharP (R ⧸ M) r
⊢ ↑p = 0
case r_dvd_p
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
I : Ideal R
hI_not_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) p
M : Ideal R
hM_max : Ideal.IsMaximal M
hM_ge : I ≤ M
r : ℕ
hr✝ hr : CharP (R ⧸ M) r
⊢ r ∣ p
rw [← CharP.cast_eq_zero_iff (R ⧸ M) r p]
no goals
case r_dvd_p
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
I : Ideal R
hI_not_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) p
M : Ideal R
hM_max : Ideal.IsMaximal M
hM_ge : I ≤ M
r : ℕ
hr✝ hr : CharP (R ⧸ M) r
⊢ ↑p = 0
convert congr_arg (Ideal.Quotient.factor I M hM_ge) (CharP.cast_eq_zero (R ⧸ I) p)
case mpr
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
I : Ideal R
hI_max : Ideal.IsMaximal I
h_charP : CharP (R ⧸ I) p
⊢ ∃ I, I ≠ ⊤ ∧ CharP (R ⧸ I) p
case mpr
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
⊢ (∃ I, Ideal.IsMaximal I ∧ CharP (R ⧸ I) p) → ∃ I, I ≠ ⊤ ∧ CharP (R ⧸ I) p
intro ⟨I, hI_max, h_charP⟩
case mpr
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
I : Ideal R
hI_max : Ideal.IsMaximal I
h_charP : CharP (R ⧸ I) p
⊢ I ≠ ⊤ ∧ CharP (R ⧸ I) p
case mpr
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
I : Ideal R
hI_max : Ideal.IsMaximal I
h_charP : CharP (R ⧸ I) p
⊢ ∃ I, I ≠ ⊤ ∧ CharP (R ⧸ I) p
use I
no goals
case mpr
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
I : Ideal R
hI_max : Ideal.IsMaximal I
h_charP : CharP (R ⧸ I) p
⊢ I ≠ ⊤ ∧ CharP (R ⧸ I) p
exact ⟨Ideal.IsMaximal.ne_top hI_max, h_charP⟩