-- Mathlib/Algebra/CharP/MixedCharZero.lean
theorem reduce_to_maximal_ideal {p : ℕ} (hp : Nat.Prime p) :
    (∃ I : Ideal R, I ≠ ⊤ ∧ CharP (R ⧸ I) p) ↔ ∃ I : Ideal R, I.IsMaximal ∧ CharP (R ⧸ I) p

Proof state:
case h.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 : M.IsMaximal
hM_ge : I ≤ M
⊢ M.IsMaximal

Tactic:
exact hM_max

Result:
no goals

Proof state:
case h.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 : M.IsMaximal
hM_ge : I ≤ M
r : ℕ
hr : CharP (R ⧸ M) r
⊢ CharP (R ⧸ M) p

Tactic:
convert hr

Result:
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 : M.IsMaximal
hM_ge : I ≤ M
r : ℕ
hr : CharP (R ⧸ M) r
⊢ p = r

Proof state:
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 : M.IsMaximal
hM_ge : I ≤ M
⊢ ∃ I, I.IsMaximal ∧ CharP (R ⧸ I) p

Tactic:
use M

Result:
case h
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 : M.IsMaximal
hM_ge : I ≤ M
⊢ M.IsMaximal ∧ CharP (R ⧸ M) p

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
I : Ideal R
hI_max : I.IsMaximal
h_charP : CharP (R ⧸ I) p
⊢ I ≠ ⊤ ∧ CharP (R ⧸ I) p

Tactic:
exact ⟨Ideal.IsMaximal.ne_top hI_max, h_charP⟩

Result:
no goals

Proof state:
case mpr
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
I : Ideal R
hI_max : I.IsMaximal
h_charP : CharP (R ⧸ I) p
⊢ ∃ I, I ≠ ⊤ ∧ CharP (R ⧸ I) p

Tactic:
use I

Result:
case h
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
I : Ideal R
hI_max : I.IsMaximal
h_charP : CharP (R ⧸ I) p
⊢ I ≠ ⊤ ∧ CharP (R ⧸ I) p

Proof state:
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 : M.IsMaximal
hM_ge : I ≤ M
r : ℕ
hr : CharP (R ⧸ M) r
⊢ p = r

Tactic:
have r_dvd_p : r ∣ p := by
  rw [← CharP.cast_eq_zero_iff (R ⧸ M) r p]
  convert congr_arg (Ideal.Quotient.factor hM_ge) (CharP.cast_eq_zero (R ⧸ I) p)

Result:
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 : M.IsMaximal
hM_ge : I ≤ M
r : ℕ
hr : CharP (R ⧸ M) r
r_dvd_p : r ∣ p
⊢ p = r

Proof state:
case h.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 : M.IsMaximal
hM_ge : I ≤ M
⊢ CharP (R ⧸ M) p

Tactic:
cases CharP.exists (R ⧸ M) with
| intro r hr =>
  convert hr
  have r_dvd_p : r ∣ p := by
    rw [← CharP.cast_eq_zero_iff (R ⧸ M) r p]
    convert congr_arg (Ideal.Quotient.factor hM_ge) (CharP.cast_eq_zero (R ⧸ I) p)
  symm
  apply (Nat.Prime.eq_one_or_self_of_dvd hp r r_dvd_p).resolve_left
  exact CharP.char_ne_one (R ⧸ M) r

Result:
no goals

Proof state:
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 : M.IsMaximal
hM_ge : I ≤ M
r : ℕ
hr : CharP (R ⧸ M) r
r_dvd_p : r ∣ p
⊢ ¬r = 1

Tactic:
exact CharP.char_ne_one (R ⧸ M) r

Result:
no goals

Proof state:
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 : M.IsMaximal
hM_ge : I ≤ M
r : ℕ
hr : CharP (R ⧸ M) r
r_dvd_p : r ∣ p
⊢ r = p

Tactic:
apply (Nat.Prime.eq_one_or_self_of_dvd hp r r_dvd_p).resolve_left

Result:
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 : M.IsMaximal
hM_ge : I ≤ M
r : ℕ
hr : CharP (R ⧸ M) r
r_dvd_p : r ∣ p
⊢ ¬r = 1

Proof state:
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
⊢ (∃ I, I ≠ ⊤ ∧ CharP (R ⧸ I) p) ↔ ∃ I, I.IsMaximal ∧ CharP (R ⧸ I) p

Tactic:
constructor

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

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

Proof state:
case h
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 : M.IsMaximal
hM_ge : I ≤ M
⊢ M.IsMaximal ∧ CharP (R ⧸ M) p

Tactic:
constructor

Result:
case h.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 : M.IsMaximal
hM_ge : I ≤ M
⊢ M.IsMaximal

case h.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 : M.IsMaximal
hM_ge : I ≤ M
⊢ CharP (R ⧸ M) p

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

Tactic:
rcases g with ⟨I, ⟨hI_not_top, _⟩⟩

Result:
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, I.IsMaximal ∧ CharP (R ⧸ I) p

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

Tactic:
intro g

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

Proof state:
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, I.IsMaximal ∧ CharP (R ⧸ I) p

Tactic:
rcases Ideal.exists_le_maximal I hI_not_top with ⟨M, ⟨hM_max, hM_ge⟩⟩

Result:
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 : M.IsMaximal
hM_ge : I ≤ M
⊢ ∃ I, I.IsMaximal ∧ CharP (R ⧸ I) p

Proof state:
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 : M.IsMaximal
hM_ge : I ≤ M
r : ℕ
hr : CharP (R ⧸ M) r
r_dvd_p : r ∣ p
⊢ p = r

Tactic:
symm

Result:
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 : M.IsMaximal
hM_ge : I ≤ M
r : ℕ
hr : CharP (R ⧸ M) r
r_dvd_p : r ∣ p
⊢ r = p

Proof state:
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 : M.IsMaximal
hM_ge : I ≤ M
r : ℕ
hr : CharP (R ⧸ M) r
⊢ r ∣ p

Tactic:
rw [← CharP.cast_eq_zero_iff (R ⧸ M) r p]

Result:
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 : M.IsMaximal
hM_ge : I ≤ M
r : ℕ
hr : CharP (R ⧸ M) r
⊢ ↑p = 0

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

Tactic:
intro ⟨I, hI_max, h_charP⟩

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

Proof state:
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 : M.IsMaximal
hM_ge : I ≤ M
r : ℕ
hr : CharP (R ⧸ M) r
⊢ ↑p = 0

Tactic:
convert congr_arg (Ideal.Quotient.factor hM_ge) (CharP.cast_eq_zero (R ⧸ I) p)

Result:
no goals