case mp
R : Type u_1
inst✝ : CommRing R
P : Prop
⊢ (∀ (p : ℕ), p > 0 → MixedCharZero R p → P) → ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P

case mpr
R : Type u_1
inst✝ : CommRing R
P : Prop
⊢ (∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P) → ∀ (p : ℕ), p > 0 → MixedCharZero R p → P
R : Type u_1
inst✝ : CommRing R
P : Prop
⊢ (∀ (p : ℕ), p > 0 → MixedCharZero R p → P) ↔ ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
constructor
case mp
R : Type u_1
inst✝ : CommRing R
P : Prop
h : ∀ (p : ℕ), p > 0 → MixedCharZero R p → P
q : ℕ
q_prime : Nat.Prime q
q_mixedChar : MixedCharZero R q
⊢ P
case mp
R : Type u_1
inst✝ : CommRing R
P : Prop
⊢ (∀ (p : ℕ), p > 0 → MixedCharZero R p → P) → ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
intro h q q_prime q_mixedChar
no goals
case mp
R : Type u_1
inst✝ : CommRing R
P : Prop
h : ∀ (p : ℕ), p > 0 → MixedCharZero R p → P
q : ℕ
q_prime : Nat.Prime q
q_mixedChar : MixedCharZero R q
⊢ P
exact h q (Nat.Prime.pos q_prime) q_mixedChar
case mpr
R : Type u_1
inst✝ : CommRing R
P : Prop
h : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
q : ℕ
q_pos : q > 0
q_mixedChar : MixedCharZero R q
⊢ P
case mpr
R : Type u_1
inst✝ : CommRing R
P : Prop
⊢ (∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P) → ∀ (p : ℕ), p > 0 → MixedCharZero R p → P
intro h q q_pos q_mixedChar
case mpr.intro.intro
R : Type u_1
inst✝ : CommRing R
P : Prop
h : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
q : ℕ
q_pos : q > 0
q_mixedChar : MixedCharZero R q
I : Ideal R
hI_ne_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) q
⊢ P
case mpr
R : Type u_1
inst✝ : CommRing R
P : Prop
h : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
q : ℕ
q_pos : q > 0
q_mixedChar : MixedCharZero R q
⊢ P
rcases q_mixedChar.charP_quotient with ⟨I, hI_ne_top, _⟩
case mpr.intro.intro.intro.intro
R : Type u_1
inst✝ : CommRing R
P : Prop
h : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
q : ℕ
q_pos : q > 0
q_mixedChar : MixedCharZero R q
I : Ideal R
hI_ne_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) q
M : Ideal R
hM_max : Ideal.IsMaximal M
h_IM : I ≤ M
⊢ P
case mpr.intro.intro
R : Type u_1
inst✝ : CommRing R
P : Prop
h : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
q : ℕ
q_pos : q > 0
q_mixedChar : MixedCharZero R q
I : Ideal R
hI_ne_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) q
⊢ P
rcases Ideal.exists_le_maximal I hI_ne_top with ⟨M, hM_max, h_IM⟩
case mpr.intro.intro.intro.intro
R : Type u_1
inst✝ : CommRing R
P : Prop
h : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
q : ℕ
q_pos : q > 0
q_mixedChar : MixedCharZero R q
I : Ideal R
hI_ne_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) q
M : Ideal R
hM_max : Ideal.IsMaximal M
h_IM : I ≤ M
r : ℕ := ringChar (R ⧸ M)
⊢ P
case mpr.intro.intro.intro.intro
R : Type u_1
inst✝ : CommRing R
P : Prop
h : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
q : ℕ
q_pos : q > 0
q_mixedChar : MixedCharZero R q
I : Ideal R
hI_ne_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) q
M : Ideal R
hM_max : Ideal.IsMaximal M
h_IM : I ≤ M
⊢ P
let r := ringChar (R ⧸ M)
case r_pos
R : Type u_1
inst✝ : CommRing R
P : Prop
h : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
q : ℕ
q_pos : q > 0
q_mixedChar : MixedCharZero R q
I : Ideal R
hI_ne_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) q
M : Ideal R
hM_max : Ideal.IsMaximal M
h_IM : I ≤ M
r : ℕ := ringChar (R ⧸ M)
⊢ r ≠ 0

case mpr.intro.intro.intro.intro
R : Type u_1
inst✝ : CommRing R
P : Prop
h : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
q : ℕ
q_pos : q > 0
q_mixedChar : MixedCharZero R q
I : Ideal R
hI_ne_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) q
M : Ideal R
hM_max : Ideal.IsMaximal M
h_IM : I ≤ M
r : ℕ := ringChar (R ⧸ M)
r_pos : r ≠ 0
⊢ P
case mpr.intro.intro.intro.intro
R : Type u_1
inst✝ : CommRing R
P : Prop
h : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
q : ℕ
q_pos : q > 0
q_mixedChar : MixedCharZero R q
I : Ideal R
hI_ne_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) q
M : Ideal R
hM_max : Ideal.IsMaximal M
h_IM : I ≤ M
r : ℕ := ringChar (R ⧸ M)
⊢ P
have r_pos : r ≠ 0
case mpr.intro.intro.intro.intro
R : Type u_1
inst✝ : CommRing R
P : Prop
h : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
q : ℕ
q_pos : q > 0
q_mixedChar : MixedCharZero R q
I : Ideal R
hI_ne_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) q
M : Ideal R
hM_max : Ideal.IsMaximal M
h_IM : I ≤ M
r : ℕ := ringChar (R ⧸ M)
r_pos : r ≠ 0
r_prime : Nat.Prime r
⊢ P
case mpr.intro.intro.intro.intro
R : Type u_1
inst✝ : CommRing R
P : Prop
h : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
q : ℕ
q_pos : q > 0
q_mixedChar : MixedCharZero R q
I : Ideal R
hI_ne_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) q
M : Ideal R
hM_max : Ideal.IsMaximal M
h_IM : I ≤ M
r : ℕ := ringChar (R ⧸ M)
r_pos : r ≠ 0
⊢ P
have r_prime : Nat.Prime r :=
  or_iff_not_imp_right.1 (CharP.char_is_prime_or_zero (R ⧸ M) r) r_pos
case mpr.intro.intro.intro.intro
R : Type u_1
inst✝ : CommRing R
P : Prop
h : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
q : ℕ
q_pos : q > 0
q_mixedChar : MixedCharZero R q
I : Ideal R
hI_ne_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) q
M : Ideal R
hM_max : Ideal.IsMaximal M
h_IM : I ≤ M
r : ℕ := ringChar (R ⧸ M)
r_pos : r ≠ 0
r_prime : Nat.Prime r
⊢ MixedCharZero R r
case mpr.intro.intro.intro.intro
R : Type u_1
inst✝ : CommRing R
P : Prop
h : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
q : ℕ
q_pos : q > 0
q_mixedChar : MixedCharZero R q
I : Ideal R
hI_ne_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) q
M : Ideal R
hM_max : Ideal.IsMaximal M
h_IM : I ≤ M
r : ℕ := ringChar (R ⧸ M)
r_pos : r ≠ 0
r_prime : Nat.Prime r
⊢ P
apply h r r_prime
case mpr.intro.intro.intro.intro
R : Type u_1
inst✝ : CommRing R
P : Prop
h : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
q : ℕ
q_pos : q > 0
q_mixedChar : MixedCharZero R q
I : Ideal R
hI_ne_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) q
M : Ideal R
hM_max : Ideal.IsMaximal M
h_IM : I ≤ M
r : ℕ := ringChar (R ⧸ M)
r_pos : r ≠ 0
r_prime : Nat.Prime r
this : CharZero R
⊢ MixedCharZero R r
case mpr.intro.intro.intro.intro
R : Type u_1
inst✝ : CommRing R
P : Prop
h : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
q : ℕ
q_pos : q > 0
q_mixedChar : MixedCharZero R q
I : Ideal R
hI_ne_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) q
M : Ideal R
hM_max : Ideal.IsMaximal M
h_IM : I ≤ M
r : ℕ := ringChar (R ⧸ M)
r_pos : r ≠ 0
r_prime : Nat.Prime r
⊢ MixedCharZero R r
have : CharZero R := q_mixedChar.toCharZero
no goals
case mpr.intro.intro.intro.intro
R : Type u_1
inst✝ : CommRing R
P : Prop
h : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
q : ℕ
q_pos : q > 0
q_mixedChar : MixedCharZero R q
I : Ideal R
hI_ne_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) q
M : Ideal R
hM_max : Ideal.IsMaximal M
h_IM : I ≤ M
r : ℕ := ringChar (R ⧸ M)
r_pos : r ≠ 0
r_prime : Nat.Prime r
this : CharZero R
⊢ MixedCharZero R r
exact ⟨⟨M, hM_max.ne_top, ringChar.of_eq rfl⟩⟩
case r_pos
R : Type u_1
inst✝ : CommRing R
P : Prop
h : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
q : ℕ
q_pos : q > 0
q_mixedChar : MixedCharZero R q
I : Ideal R
hI_ne_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) q
M : Ideal R
hM_max : Ideal.IsMaximal M
h_IM : I ≤ M
r : ℕ := ringChar (R ⧸ M)
q_zero : ↑(Ideal.Quotient.factor I M h_IM) ↑q = ↑(Ideal.Quotient.factor I M h_IM) 0
⊢ r ≠ 0
case r_pos
R : Type u_1
inst✝ : CommRing R
P : Prop
h : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
q : ℕ
q_pos : q > 0
q_mixedChar : MixedCharZero R q
I : Ideal R
hI_ne_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) q
M : Ideal R
hM_max : Ideal.IsMaximal M
h_IM : I ≤ M
r : ℕ := ringChar (R ⧸ M)
⊢ r ≠ 0
have q_zero :=
  congr_arg (Ideal.Quotient.factor I M h_IM) (CharP.cast_eq_zero (R ⧸ I) q)
case r_pos
R : Type u_1
inst✝ : CommRing R
P : Prop
h : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
q : ℕ
q_pos : q > 0
q_mixedChar : MixedCharZero R q
I : Ideal R
hI_ne_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) q
M : Ideal R
hM_max : Ideal.IsMaximal M
h_IM : I ≤ M
r : ℕ := ringChar (R ⧸ M)
q_zero : ↑q = 0
⊢ r ≠ 0
case r_pos
R : Type u_1
inst✝ : CommRing R
P : Prop
h : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
q : ℕ
q_pos : q > 0
q_mixedChar : MixedCharZero R q
I : Ideal R
hI_ne_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) q
M : Ideal R
hM_max : Ideal.IsMaximal M
h_IM : I ≤ M
r : ℕ := ringChar (R ⧸ M)
q_zero : ↑(Ideal.Quotient.factor I M h_IM) ↑q = ↑(Ideal.Quotient.factor I M h_IM) 0
⊢ r ≠ 0
simp only [map_natCast, map_zero] at q_zero
case r_pos
R : Type u_1
inst✝ : CommRing R
P : Prop
h : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
q : ℕ
q_pos : q > 0
q_mixedChar : MixedCharZero R q
I : Ideal R
hI_ne_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) q
M : Ideal R
hM_max : Ideal.IsMaximal M
h_IM : I ≤ M
r : ℕ := ringChar (R ⧸ M)
q_zero : ↑q = 0
⊢ r ∣ q
case r_pos
R : Type u_1
inst✝ : CommRing R
P : Prop
h : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
q : ℕ
q_pos : q > 0
q_mixedChar : MixedCharZero R q
I : Ideal R
hI_ne_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) q
M : Ideal R
hM_max : Ideal.IsMaximal M
h_IM : I ≤ M
r : ℕ := ringChar (R ⧸ M)
q_zero : ↑q = 0
⊢ r ≠ 0
apply ne_zero_of_dvd_ne_zero (ne_of_gt q_pos)
no goals
case r_pos
R : Type u_1
inst✝ : CommRing R
P : Prop
h : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
q : ℕ
q_pos : q > 0
q_mixedChar : MixedCharZero R q
I : Ideal R
hI_ne_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) q
M : Ideal R
hM_max : Ideal.IsMaximal M
h_IM : I ≤ M
r : ℕ := ringChar (R ⧸ M)
q_zero : ↑q = 0
⊢ r ∣ q
exact (CharP.cast_eq_zero_iff (R ⧸ M) r q).mp q_zero