[GOAL]
R : Type u_1
inst✝ : CommRing R
P : Prop
⊢ (∀ (p : ℕ), p > 0 → MixedCharZero R p → P) ↔ ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
[PROOFSTEP]
constructor
[GOAL]
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
[PROOFSTEP]
intro h q q_prime q_mixedChar
[GOAL]
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
[PROOFSTEP]
exact h q (Nat.Prime.pos q_prime) q_mixedChar
[GOAL]
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
[PROOFSTEP]
intro h q q_pos q_mixedChar
[GOAL]
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
[PROOFSTEP]
rcases q_mixedChar.charP_quotient with
  ⟨I, hI_ne_top, _⟩
    -- Krull's Thm: There exists a prime ideal `P` such that `I ≤ P`
[GOAL]
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
[PROOFSTEP]
rcases Ideal.exists_le_maximal I hI_ne_top with ⟨M, hM_max, h_IM⟩
[GOAL]
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
[PROOFSTEP]
let r := ringChar (R ⧸ M)
[GOAL]
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
[PROOFSTEP]
have r_pos : r ≠ 0
[GOAL]
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
[PROOFSTEP]
have q_zero := congr_arg (Ideal.Quotient.factor I M h_IM) (CharP.cast_eq_zero (R ⧸ I) q)
[GOAL]
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
[PROOFSTEP]
simp only [map_natCast, map_zero] at q_zero
[GOAL]
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
[PROOFSTEP]
apply ne_zero_of_dvd_ne_zero (ne_of_gt q_pos)
[GOAL]
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
[PROOFSTEP]
exact (CharP.cast_eq_zero_iff (R ⧸ M) r q).mp q_zero
[GOAL]
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
[PROOFSTEP]
have r_prime : Nat.Prime r := or_iff_not_imp_right.1 (CharP.char_is_prime_or_zero (R ⧸ M) r) r_pos
[GOAL]
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
[PROOFSTEP]
apply h r r_prime
[GOAL]
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
[PROOFSTEP]
have : CharZero R := q_mixedChar.toCharZero
[GOAL]
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
[PROOFSTEP]
exact ⟨⟨M, hM_max.ne_top, ringChar.of_eq rfl⟩⟩
[GOAL]
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
[PROOFSTEP]
constructor
[GOAL]
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
[PROOFSTEP]
intro g
[GOAL]
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
[PROOFSTEP]
rcases g with
  ⟨I, ⟨hI_not_top, _⟩⟩
    -- Krull's Thm: There exists a prime ideal `M` such that `I ≤ M`.
[GOAL]
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
[PROOFSTEP]
rcases Ideal.exists_le_maximal I hI_not_top with ⟨M, ⟨hM_max, hM_ge⟩⟩
[GOAL]
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
[PROOFSTEP]
use M
[GOAL]
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 : Ideal.IsMaximal M
hM_ge : I ≤ M
⊢ Ideal.IsMaximal M ∧ CharP (R ⧸ M) p
[PROOFSTEP]
constructor
[GOAL]
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 : Ideal.IsMaximal M
hM_ge : I ≤ M
⊢ Ideal.IsMaximal M
[PROOFSTEP]
exact hM_max
[GOAL]
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 : Ideal.IsMaximal M
hM_ge : I ≤ M
⊢ CharP (R ⧸ M) p
[PROOFSTEP]
cases CharP.exists (R ⧸ M) with
| intro r hr =>
  -- Porting note: This is odd. Added `have hr := hr`.
          -- Without this it seems that lean does not find `hr` as an instance.
  have hr := hr
  convert hr
  have r_dvd_p : r ∣ p
  · rw [← CharP.cast_eq_zero_iff (R ⧸ M) r p]
    convert congr_arg (Ideal.Quotient.factor I M 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
[GOAL]
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 : Ideal.IsMaximal M
hM_ge : I ≤ M
x✝ : ∃ p, CharP (R ⧸ M) p
⊢ CharP (R ⧸ M) p
[PROOFSTEP]
cases CharP.exists (R ⧸ M) with
| intro r hr =>
  -- Porting note: This is odd. Added `have hr := hr`.
          -- Without this it seems that lean does not find `hr` as an instance.
  have hr := hr
  convert hr
  have r_dvd_p : r ∣ p
  · rw [← CharP.cast_eq_zero_iff (R ⧸ M) r p]
    convert congr_arg (Ideal.Quotient.factor I M 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
[GOAL]
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 : Ideal.IsMaximal M
hM_ge : I ≤ M
r : ℕ
hr : CharP (R ⧸ M) r
⊢ CharP (R ⧸ M) p
[PROOFSTEP]

| intro r hr =>
  -- Porting note: This is odd. Added `have hr := hr`.
          -- Without this it seems that lean does not find `hr` as an instance.
  have hr := hr
  convert hr
  have r_dvd_p : r ∣ p
  · rw [← CharP.cast_eq_zero_iff (R ⧸ M) r p]
    convert congr_arg (Ideal.Quotient.factor I M 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
[GOAL]
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 : Ideal.IsMaximal M
hM_ge : I ≤ M
r : ℕ
hr : CharP (R ⧸ M) r
⊢ CharP (R ⧸ M) p
[PROOFSTEP]
have hr := hr
[GOAL]
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 : Ideal.IsMaximal M
hM_ge : I ≤ M
r : ℕ
hr✝ hr : CharP (R ⧸ M) r
⊢ CharP (R ⧸ M) p
[PROOFSTEP]
convert hr
[GOAL]
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
[PROOFSTEP]
have r_dvd_p : r ∣ p
[GOAL]
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
[PROOFSTEP]
rw [← CharP.cast_eq_zero_iff (R ⧸ M) r p]
[GOAL]
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
[PROOFSTEP]
convert congr_arg (Ideal.Quotient.factor I M hM_ge) (CharP.cast_eq_zero (R ⧸ I) p)
[GOAL]
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
[PROOFSTEP]
symm
[GOAL]
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
[PROOFSTEP]
apply (Nat.Prime.eq_one_or_self_of_dvd hp r r_dvd_p).resolve_left
[GOAL]
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
[PROOFSTEP]
exact CharP.char_ne_one (R ⧸ M) r
[GOAL]
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
[PROOFSTEP]
intro ⟨I, hI_max, h_charP⟩
[GOAL]
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
[PROOFSTEP]
use I
[GOAL]
case h
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
[PROOFSTEP]
exact ⟨Ideal.IsMaximal.ne_top hI_max, h_charP⟩
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra ℚ R
⊢ ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
[PROOFSTEP]
intro I hI
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra ℚ R
I : Ideal R
hI : I ≠ ⊤
⊢ CharZero (R ⧸ I)
[PROOFSTEP]
constructor
[GOAL]
case cast_injective
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra ℚ R
I : Ideal R
hI : I ≠ ⊤
⊢ Function.Injective Nat.cast
[PROOFSTEP]
intro a b h_ab
[GOAL]
case cast_injective
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra ℚ R
I : Ideal R
hI : I ≠ ⊤
a b : ℕ
h_ab : ↑a = ↑b
⊢ a = b
[PROOFSTEP]
contrapose! hI
[GOAL]
case cast_injective
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra ℚ R
I : Ideal R
a b : ℕ
h_ab : ↑a = ↑b
hI : a ≠ b
⊢ I = ⊤
[PROOFSTEP]
refine' I.eq_top_of_isUnit_mem _ (IsUnit.map (algebraMap ℚ R) (IsUnit.mk0 (a - b : ℚ) _))
[GOAL]
case cast_injective.refine'_1
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra ℚ R
I : Ideal R
a b : ℕ
h_ab : ↑a = ↑b
hI : a ≠ b
⊢ ↑(algebraMap ℚ R) (↑a - ↑b) ∈ I
[PROOFSTEP]
simpa only [← Ideal.Quotient.eq_zero_iff_mem, map_sub, sub_eq_zero, map_natCast]
[GOAL]
case cast_injective.refine'_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra ℚ R
I : Ideal R
a b : ℕ
h_ab : ↑a = ↑b
hI : a ≠ b
⊢ ↑a - ↑b ≠ 0
[PROOFSTEP]
simpa only [Ne.def, sub_eq_zero] using (@Nat.cast_injective ℚ _ _).ne hI
[GOAL]
R : Type u_1
inst✝ : CommRing R
h : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
n : ℕ+
⊢ IsUnit ↑↑n
[PROOFSTEP]
rw [← Ideal.span_singleton_eq_top]
  -- So by contrapositive, we should show the quotient does not have characteristic zero.
[GOAL]
R : Type u_1
inst✝ : CommRing R
h : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
n : ℕ+
⊢ Ideal.span {↑↑n} = ⊤
[PROOFSTEP]
apply not_imp_comm.mp (h.elim (Ideal.span {↑n}))
[GOAL]
R : Type u_1
inst✝ : CommRing R
h : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
n : ℕ+
⊢ ¬CharZero (R ⧸ Ideal.span {↑↑n})
[PROOFSTEP]
intro h_char_zero
[GOAL]
R : Type u_1
inst✝ : CommRing R
h : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
n : ℕ+
h_char_zero : CharZero (R ⧸ Ideal.span {↑↑n})
⊢ False
[PROOFSTEP]
apply h_char_zero.cast_injective.ne n.ne_zero
[GOAL]
R : Type u_1
inst✝ : CommRing R
h : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
n : ℕ+
h_char_zero : CharZero (R ⧸ Ideal.span {↑↑n})
⊢ ↑↑n = ↑0
[PROOFSTEP]
rw [← map_natCast (Ideal.Quotient.mk _), Nat.cast_zero, Ideal.Quotient.eq_zero_iff_mem]
[GOAL]
R : Type u_1
inst✝ : CommRing R
h : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
n : ℕ+
h_char_zero : CharZero (R ⧸ Ideal.span {↑↑n})
⊢ ↑↑n ∈ Ideal.span {↑↑n}
[PROOFSTEP]
exact Ideal.subset_span (Set.mem_singleton _)
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
⊢ ↑1 = 1
[PROOFSTEP]
apply Units.ext
[GOAL]
case a
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
⊢ ↑↑1 = ↑1
[PROOFSTEP]
rw [Units.val_one]
[GOAL]
case a
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
⊢ ↑↑1 = 1
[PROOFSTEP]
change ((PNat.isUnit_natCast (R := R) 1).unit : R) = 1
[GOAL]
case a
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
⊢ ↑(IsUnit.unit (_ : IsUnit ↑↑1)) = 1
[PROOFSTEP]
rw [IsUnit.unit_spec (PNat.isUnit_natCast 1)]
[GOAL]
case a
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
⊢ ↑↑1 = 1
[PROOFSTEP]
rw [PNat.one_coe, Nat.cast_one]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
n : ℕ+
⊢ ↑↑n = ↑↑n
[PROOFSTEP]
change ((PNat.isUnit_natCast (R := R) n).unit : R) = ↑n
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
n : ℕ+
⊢ ↑(IsUnit.unit (_ : IsUnit ↑↑n)) = ↑↑n
[PROOFSTEP]
simp only [IsUnit.unit_spec]
[GOAL]
R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
this : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
⊢ (fun x => ↑x.num /ₚ ↑(Rat.pnatDen x)) 1 = 1
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
this : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
⊢ ∀ (x y : ℚ),
    OneHom.toFun { toFun := fun x => ↑x.num /ₚ ↑(Rat.pnatDen x), map_one' := (_ : ↑1 /ₚ ↑1 = 1) } (x * y) =
      OneHom.toFun { toFun := fun x => ↑x.num /ₚ ↑(Rat.pnatDen x), map_one' := (_ : ↑1 /ₚ ↑1 = 1) } x *
        OneHom.toFun { toFun := fun x => ↑x.num /ₚ ↑(Rat.pnatDen x), map_one' := (_ : ↑1 /ₚ ↑1 = 1) } y
[PROOFSTEP]
intro a b
[GOAL]
R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
this : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
a b : ℚ
⊢ OneHom.toFun { toFun := fun x => ↑x.num /ₚ ↑(Rat.pnatDen x), map_one' := (_ : ↑1 /ₚ ↑1 = 1) } (a * b) =
    OneHom.toFun { toFun := fun x => ↑x.num /ₚ ↑(Rat.pnatDen x), map_one' := (_ : ↑1 /ₚ ↑1 = 1) } a *
      OneHom.toFun { toFun := fun x => ↑x.num /ₚ ↑(Rat.pnatDen x), map_one' := (_ : ↑1 /ₚ ↑1 = 1) } b
[PROOFSTEP]
field_simp
[GOAL]
R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
this : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
a b : ℚ
⊢ ↑(a * b).num * (↑b.den * ↑a.den) = ↑a.num * ↑b.num * ↑(a * b).den
[PROOFSTEP]
trans (↑((a * b).num * a.den * b.den) : R)
[GOAL]
R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
this : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
a b : ℚ
⊢ ↑(a * b).num * (↑b.den * ↑a.den) = ↑((a * b).num * ↑a.den * ↑b.den)
[PROOFSTEP]
simp_rw [Int.cast_mul, Int.cast_ofNat]
[GOAL]
R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
this : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
a b : ℚ
⊢ ↑(a * b).num * (↑b.den * ↑a.den) = ↑(a * b).num * ↑a.den * ↑b.den
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
this : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
a b : ℚ
⊢ ↑((a * b).num * ↑a.den * ↑b.den) = ↑a.num * ↑b.num * ↑(a * b).den
[PROOFSTEP]
rw [Rat.mul_num_den' a b]
[GOAL]
R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
this : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
a b : ℚ
⊢ ↑(a.num * b.num * ↑(a * b).den) = ↑a.num * ↑b.num * ↑(a * b).den
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
this : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
⊢ OneHom.toFun
      (↑{ toOneHom := { toFun := fun x => ↑x.num /ₚ ↑(Rat.pnatDen x), map_one' := (_ : ↑1 /ₚ ↑1 = 1) },
          map_mul' :=
            (_ :
              ∀ (a b : ℚ),
                OneHom.toFun { toFun := fun x => ↑x.num /ₚ ↑(Rat.pnatDen x), map_one' := (_ : ↑1 /ₚ ↑1 = 1) } (a * b) =
                  OneHom.toFun { toFun := fun x => ↑x.num /ₚ ↑(Rat.pnatDen x), map_one' := (_ : ↑1 /ₚ ↑1 = 1) } a *
                    OneHom.toFun { toFun := fun x => ↑x.num /ₚ ↑(Rat.pnatDen x), map_one' := (_ : ↑1 /ₚ ↑1 = 1) } b) })
      0 =
    0
[PROOFSTEP]
simp [divp]
[GOAL]
R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
this : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
⊢ ∀ (x y : ℚ),
    OneHom.toFun
        (↑{ toOneHom := { toFun := fun x => ↑x.num /ₚ ↑(Rat.pnatDen x), map_one' := (_ : ↑1 /ₚ ↑1 = 1) },
            map_mul' :=
              (_ :
                ∀ (a b : ℚ),
                  OneHom.toFun { toFun := fun x => ↑x.num /ₚ ↑(Rat.pnatDen x), map_one' := (_ : ↑1 /ₚ ↑1 = 1) }
                      (a * b) =
                    OneHom.toFun { toFun := fun x => ↑x.num /ₚ ↑(Rat.pnatDen x), map_one' := (_ : ↑1 /ₚ ↑1 = 1) } a *
                      OneHom.toFun { toFun := fun x => ↑x.num /ₚ ↑(Rat.pnatDen x), map_one' := (_ : ↑1 /ₚ ↑1 = 1) }
                        b) })
        (x + y) =
      OneHom.toFun
          (↑{ toOneHom := { toFun := fun x => ↑x.num /ₚ ↑(Rat.pnatDen x), map_one' := (_ : ↑1 /ₚ ↑1 = 1) },
              map_mul' :=
                (_ :
                  ∀ (a b : ℚ),
                    OneHom.toFun { toFun := fun x => ↑x.num /ₚ ↑(Rat.pnatDen x), map_one' := (_ : ↑1 /ₚ ↑1 = 1) }
                        (a * b) =
                      OneHom.toFun { toFun := fun x => ↑x.num /ₚ ↑(Rat.pnatDen x), map_one' := (_ : ↑1 /ₚ ↑1 = 1) } a *
                        OneHom.toFun { toFun := fun x => ↑x.num /ₚ ↑(Rat.pnatDen x), map_one' := (_ : ↑1 /ₚ ↑1 = 1) }
                          b) })
          x +
        OneHom.toFun
          (↑{ toOneHom := { toFun := fun x => ↑x.num /ₚ ↑(Rat.pnatDen x), map_one' := (_ : ↑1 /ₚ ↑1 = 1) },
              map_mul' :=
                (_ :
                  ∀ (a b : ℚ),
                    OneHom.toFun { toFun := fun x => ↑x.num /ₚ ↑(Rat.pnatDen x), map_one' := (_ : ↑1 /ₚ ↑1 = 1) }
                        (a * b) =
                      OneHom.toFun { toFun := fun x => ↑x.num /ₚ ↑(Rat.pnatDen x), map_one' := (_ : ↑1 /ₚ ↑1 = 1) } a *
                        OneHom.toFun { toFun := fun x => ↑x.num /ₚ ↑(Rat.pnatDen x), map_one' := (_ : ↑1 /ₚ ↑1 = 1) }
                          b) })
          y
[PROOFSTEP]
intro a b
[GOAL]
R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
this : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
a b : ℚ
⊢ OneHom.toFun
      (↑{ toOneHom := { toFun := fun x => ↑x.num /ₚ ↑(Rat.pnatDen x), map_one' := (_ : ↑1 /ₚ ↑1 = 1) },
          map_mul' :=
            (_ :
              ∀ (a b : ℚ),
                OneHom.toFun { toFun := fun x => ↑x.num /ₚ ↑(Rat.pnatDen x), map_one' := (_ : ↑1 /ₚ ↑1 = 1) } (a * b) =
                  OneHom.toFun { toFun := fun x => ↑x.num /ₚ ↑(Rat.pnatDen x), map_one' := (_ : ↑1 /ₚ ↑1 = 1) } a *
                    OneHom.toFun { toFun := fun x => ↑x.num /ₚ ↑(Rat.pnatDen x), map_one' := (_ : ↑1 /ₚ ↑1 = 1) } b) })
      (a + b) =
    OneHom.toFun
        (↑{ toOneHom := { toFun := fun x => ↑x.num /ₚ ↑(Rat.pnatDen x), map_one' := (_ : ↑1 /ₚ ↑1 = 1) },
            map_mul' :=
              (_ :
                ∀ (a b : ℚ),
                  OneHom.toFun { toFun := fun x => ↑x.num /ₚ ↑(Rat.pnatDen x), map_one' := (_ : ↑1 /ₚ ↑1 = 1) }
                      (a * b) =
                    OneHom.toFun { toFun := fun x => ↑x.num /ₚ ↑(Rat.pnatDen x), map_one' := (_ : ↑1 /ₚ ↑1 = 1) } a *
                      OneHom.toFun { toFun := fun x => ↑x.num /ₚ ↑(Rat.pnatDen x), map_one' := (_ : ↑1 /ₚ ↑1 = 1) }
                        b) })
        a +
      OneHom.toFun
        (↑{ toOneHom := { toFun := fun x => ↑x.num /ₚ ↑(Rat.pnatDen x), map_one' := (_ : ↑1 /ₚ ↑1 = 1) },
            map_mul' :=
              (_ :
                ∀ (a b : ℚ),
                  OneHom.toFun { toFun := fun x => ↑x.num /ₚ ↑(Rat.pnatDen x), map_one' := (_ : ↑1 /ₚ ↑1 = 1) }
                      (a * b) =
                    OneHom.toFun { toFun := fun x => ↑x.num /ₚ ↑(Rat.pnatDen x), map_one' := (_ : ↑1 /ₚ ↑1 = 1) } a *
                      OneHom.toFun { toFun := fun x => ↑x.num /ₚ ↑(Rat.pnatDen x), map_one' := (_ : ↑1 /ₚ ↑1 = 1) }
                        b) })
        b
[PROOFSTEP]
field_simp
[GOAL]
R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
this : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
a b : ℚ
⊢ ↑(a + b).num * (↑b.den * ↑a.den) = (↑a.num * ↑b.den + ↑b.num * ↑a.den) * ↑(a + b).den
[PROOFSTEP]
trans (↑((a + b).num * a.den * b.den) : R)
[GOAL]
R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
this : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
a b : ℚ
⊢ ↑(a + b).num * (↑b.den * ↑a.den) = ↑((a + b).num * ↑a.den * ↑b.den)
[PROOFSTEP]
simp_rw [Int.cast_mul, Int.cast_ofNat]
[GOAL]
R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
this : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
a b : ℚ
⊢ ↑(a + b).num * (↑b.den * ↑a.den) = ↑(a + b).num * ↑a.den * ↑b.den
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
this : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
a b : ℚ
⊢ ↑((a + b).num * ↑a.den * ↑b.den) = (↑a.num * ↑b.den + ↑b.num * ↑a.den) * ↑(a + b).den
[PROOFSTEP]
rw [Rat.add_num_den' a b]
[GOAL]
R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
this : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
a b : ℚ
⊢ ↑((a.num * ↑b.den + b.num * ↑a.den) * ↑(a + b).den) = (↑a.num * ↑b.den + ↑b.num * ↑a.den) * ↑(a + b).den
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
h : ∀ (p : ℕ), p > 0 → ¬MixedCharZero R p
⊢ ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
[PROOFSTEP]
intro I hI_ne_top
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
h : ∀ (p : ℕ), p > 0 → ¬MixedCharZero R p
I : Ideal R
hI_ne_top : I ≠ ⊤
⊢ CharZero (R ⧸ I)
[PROOFSTEP]
suffices h_charP : CharP (R ⧸ I) 0
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
h : ∀ (p : ℕ), p > 0 → ¬MixedCharZero R p
I : Ideal R
hI_ne_top : I ≠ ⊤
h_charP : CharP (R ⧸ I) 0
⊢ CharZero (R ⧸ I)
[PROOFSTEP]
apply CharP.charP_to_charZero
[GOAL]
case h_charP
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
h : ∀ (p : ℕ), p > 0 → ¬MixedCharZero R p
I : Ideal R
hI_ne_top : I ≠ ⊤
⊢ CharP (R ⧸ I) 0
[PROOFSTEP]
cases CharP.exists (R ⧸ I) with
| intro p hp =>
  cases p with
  | zero => exact hp
  | succ p =>
    have h_mixed : MixedCharZero R p.succ := ⟨⟨I, ⟨hI_ne_top, hp⟩⟩⟩
    exact absurd h_mixed (h p.succ p.succ_pos)
[GOAL]
case h_charP
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
h : ∀ (p : ℕ), p > 0 → ¬MixedCharZero R p
I : Ideal R
hI_ne_top : I ≠ ⊤
x✝ : ∃ p, CharP (R ⧸ I) p
⊢ CharP (R ⧸ I) 0
[PROOFSTEP]
cases CharP.exists (R ⧸ I) with
| intro p hp =>
  cases p with
  | zero => exact hp
  | succ p =>
    have h_mixed : MixedCharZero R p.succ := ⟨⟨I, ⟨hI_ne_top, hp⟩⟩⟩
    exact absurd h_mixed (h p.succ p.succ_pos)
[GOAL]
case h_charP.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
h : ∀ (p : ℕ), p > 0 → ¬MixedCharZero R p
I : Ideal R
hI_ne_top : I ≠ ⊤
p : ℕ
hp : CharP (R ⧸ I) p
⊢ CharP (R ⧸ I) 0
[PROOFSTEP]

| intro p hp =>
  cases p with
  | zero => exact hp
  | succ p =>
    have h_mixed : MixedCharZero R p.succ := ⟨⟨I, ⟨hI_ne_top, hp⟩⟩⟩
    exact absurd h_mixed (h p.succ p.succ_pos)
[GOAL]
case h_charP.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
h : ∀ (p : ℕ), p > 0 → ¬MixedCharZero R p
I : Ideal R
hI_ne_top : I ≠ ⊤
p : ℕ
hp : CharP (R ⧸ I) p
⊢ CharP (R ⧸ I) 0
[PROOFSTEP]
cases p with
| zero => exact hp
| succ p =>
  have h_mixed : MixedCharZero R p.succ := ⟨⟨I, ⟨hI_ne_top, hp⟩⟩⟩
  exact absurd h_mixed (h p.succ p.succ_pos)
[GOAL]
case h_charP.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
h : ∀ (p : ℕ), p > 0 → ¬MixedCharZero R p
I : Ideal R
hI_ne_top : I ≠ ⊤
p : ℕ
hp : CharP (R ⧸ I) p
⊢ CharP (R ⧸ I) 0
[PROOFSTEP]
cases p with
| zero => exact hp
| succ p =>
  have h_mixed : MixedCharZero R p.succ := ⟨⟨I, ⟨hI_ne_top, hp⟩⟩⟩
  exact absurd h_mixed (h p.succ p.succ_pos)
[GOAL]
case h_charP.intro.zero
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
h : ∀ (p : ℕ), p > 0 → ¬MixedCharZero R p
I : Ideal R
hI_ne_top : I ≠ ⊤
hp : CharP (R ⧸ I) Nat.zero
⊢ CharP (R ⧸ I) 0
[PROOFSTEP]

| zero => exact hp
[GOAL]
case h_charP.intro.zero
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
h : ∀ (p : ℕ), p > 0 → ¬MixedCharZero R p
I : Ideal R
hI_ne_top : I ≠ ⊤
hp : CharP (R ⧸ I) Nat.zero
⊢ CharP (R ⧸ I) 0
[PROOFSTEP]
exact hp
[GOAL]
case h_charP.intro.succ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
h : ∀ (p : ℕ), p > 0 → ¬MixedCharZero R p
I : Ideal R
hI_ne_top : I ≠ ⊤
p : ℕ
hp : CharP (R ⧸ I) (Nat.succ p)
⊢ CharP (R ⧸ I) 0
[PROOFSTEP]

| succ p =>
  have h_mixed : MixedCharZero R p.succ := ⟨⟨I, ⟨hI_ne_top, hp⟩⟩⟩
  exact absurd h_mixed (h p.succ p.succ_pos)
[GOAL]
case h_charP.intro.succ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
h : ∀ (p : ℕ), p > 0 → ¬MixedCharZero R p
I : Ideal R
hI_ne_top : I ≠ ⊤
p : ℕ
hp : CharP (R ⧸ I) (Nat.succ p)
⊢ CharP (R ⧸ I) 0
[PROOFSTEP]
have h_mixed : MixedCharZero R p.succ := ⟨⟨I, ⟨hI_ne_top, hp⟩⟩⟩
[GOAL]
case h_charP.intro.succ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
h : ∀ (p : ℕ), p > 0 → ¬MixedCharZero R p
I : Ideal R
hI_ne_top : I ≠ ⊤
p : ℕ
hp : CharP (R ⧸ I) (Nat.succ p)
h_mixed : MixedCharZero R (Nat.succ p)
⊢ CharP (R ⧸ I) 0
[PROOFSTEP]
exact absurd h_mixed (h p.succ p.succ_pos)
[GOAL]
R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
⊢ ∀ (p : ℕ), p > 0 → ¬MixedCharZero R p
[PROOFSTEP]
intro p p_pos
[GOAL]
R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
p : ℕ
p_pos : p > 0
⊢ ¬MixedCharZero R p
[PROOFSTEP]
by_contra hp_mixedChar
[GOAL]
R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
p : ℕ
p_pos : p > 0
hp_mixedChar : MixedCharZero R p
⊢ False
[PROOFSTEP]
rcases hp_mixedChar.charP_quotient with ⟨I, hI_ne_top, hI_p⟩
[GOAL]
case intro.intro
R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
p : ℕ
p_pos : p > 0
hp_mixedChar : MixedCharZero R p
I : Ideal R
hI_ne_top : I ≠ ⊤
hI_p : CharP (R ⧸ I) p
⊢ False
[PROOFSTEP]
replace hI_zero : CharP (R ⧸ I) 0 := @CharP.ofCharZero _ _ (h I hI_ne_top)
[GOAL]
case intro.intro
R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
p : ℕ
p_pos : p > 0
hp_mixedChar : MixedCharZero R p
I : Ideal R
hI_ne_top : I ≠ ⊤
hI_p : CharP (R ⧸ I) p
hI_zero : CharP (R ⧸ I) 0
⊢ False
[PROOFSTEP]
exact absurd (CharP.eq (R ⧸ I) hI_p hI_zero) (ne_of_gt p_pos)
[GOAL]
R : Type u_1
inst✝ : CommRing R
⊢ Nonempty (Algebra ℚ R) ↔ ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
inst✝ : CommRing R
⊢ Nonempty (Algebra ℚ R) → ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
[PROOFSTEP]
intro h_alg
[GOAL]
case mp
R : Type u_1
inst✝ : CommRing R
h_alg : Nonempty (Algebra ℚ R)
⊢ ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
[PROOFSTEP]
haveI h_alg' : Algebra ℚ R := h_alg.some
[GOAL]
case mp
R : Type u_1
inst✝ : CommRing R
h_alg : Nonempty (Algebra ℚ R)
h_alg' : Algebra ℚ R
⊢ ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
[PROOFSTEP]
apply of_algebraRat
[GOAL]
case mpr
R : Type u_1
inst✝ : CommRing R
⊢ (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)) → Nonempty (Algebra ℚ R)
[PROOFSTEP]
intro h
[GOAL]
case mpr
R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
⊢ Nonempty (Algebra ℚ R)
[PROOFSTEP]
apply Nonempty.intro
[GOAL]
case mpr.val
R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
⊢ Algebra ℚ R
[PROOFSTEP]
exact algebraRat h
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
⊢ IsEmpty (Algebra ℚ R) ↔ ∃ p, p > 0 ∧ MixedCharZero R p
[PROOFSTEP]
rw [← not_iff_not]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
⊢ ¬IsEmpty (Algebra ℚ R) ↔ ¬∃ p, p > 0 ∧ MixedCharZero R p
[PROOFSTEP]
push_neg
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
⊢ ¬IsEmpty (Algebra ℚ R) ↔ ∀ (p : ℕ), p > 0 → ¬MixedCharZero R p
[PROOFSTEP]
rw [not_isEmpty_iff, ← EqualCharZero.iff_not_mixedCharZero]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
⊢ Nonempty (Algebra ℚ R) ↔ ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
[PROOFSTEP]
apply EqualCharZero.nonempty_algebraRat_iff
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : CharZero R
h_equal : Algebra ℚ R → P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
⊢ P
[PROOFSTEP]
by_cases h : ∃ p > 0, MixedCharZero R p
[GOAL]
case pos
R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : CharZero R
h_equal : Algebra ℚ R → P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
h : ∃ p, p > 0 ∧ MixedCharZero R p
⊢ P
[PROOFSTEP]
rcases h with ⟨p, ⟨H, hp⟩⟩
[GOAL]
case pos.intro.intro
R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : CharZero R
h_equal : Algebra ℚ R → P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
p : ℕ
H : p > 0
hp : MixedCharZero R p
⊢ P
[PROOFSTEP]
rw [← MixedCharZero.reduce_to_p_prime] at h_mixed
[GOAL]
case pos.intro.intro
R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : CharZero R
h_equal : Algebra ℚ R → P
h_mixed : ∀ (p : ℕ), p > 0 → MixedCharZero R p → P
p : ℕ
H : p > 0
hp : MixedCharZero R p
⊢ P
[PROOFSTEP]
exact h_mixed p H hp
[GOAL]
case neg
R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : CharZero R
h_equal : Algebra ℚ R → P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
h : ¬∃ p, p > 0 ∧ MixedCharZero R p
⊢ P
[PROOFSTEP]
apply h_equal
[GOAL]
case neg
R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : CharZero R
h_equal : Algebra ℚ R → P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
h : ¬∃ p, p > 0 ∧ MixedCharZero R p
⊢ Algebra ℚ R
[PROOFSTEP]
rw [← isEmpty_algebraRat_iff_mixedCharZero, not_isEmpty_iff] at h
[GOAL]
case neg
R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : CharZero R
h_equal : Algebra ℚ R → P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
h : Nonempty (Algebra ℚ R)
⊢ Algebra ℚ R
[PROOFSTEP]
exact h.some
[GOAL]
R : Type u_1
inst✝ : CommRing R
P : Prop
h_pos : ∀ (p : ℕ), p ≠ 0 → CharP R p → P
h_equal : Algebra ℚ R → P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
⊢ P
[PROOFSTEP]
cases CharP.exists R with
| intro p p_charP =>
  by_cases p = 0
  · rw [h] at p_charP
    haveI h0 : CharZero R := CharP.charP_to_charZero R
    exact split_equalCharZero_mixedCharZero R h_equal h_mixed
  · exact h_pos p h p_charP
[GOAL]
R : Type u_1
inst✝ : CommRing R
P : Prop
h_pos : ∀ (p : ℕ), p ≠ 0 → CharP R p → P
h_equal : Algebra ℚ R → P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
x✝ : ∃ p, CharP R p
⊢ P
[PROOFSTEP]
cases CharP.exists R with
| intro p p_charP =>
  by_cases p = 0
  · rw [h] at p_charP
    haveI h0 : CharZero R := CharP.charP_to_charZero R
    exact split_equalCharZero_mixedCharZero R h_equal h_mixed
  · exact h_pos p h p_charP
[GOAL]
case intro
R : Type u_1
inst✝ : CommRing R
P : Prop
h_pos : ∀ (p : ℕ), p ≠ 0 → CharP R p → P
h_equal : Algebra ℚ R → P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
p : ℕ
p_charP : CharP R p
⊢ P
[PROOFSTEP]

| intro p p_charP =>
  by_cases p = 0
  · rw [h] at p_charP
    haveI h0 : CharZero R := CharP.charP_to_charZero R
    exact split_equalCharZero_mixedCharZero R h_equal h_mixed
  · exact h_pos p h p_charP
[GOAL]
case intro
R : Type u_1
inst✝ : CommRing R
P : Prop
h_pos : ∀ (p : ℕ), p ≠ 0 → CharP R p → P
h_equal : Algebra ℚ R → P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
p : ℕ
p_charP : CharP R p
⊢ P
[PROOFSTEP]
by_cases p = 0
[GOAL]
case intro
R : Type u_1
inst✝ : CommRing R
P : Prop
h_pos : ∀ (p : ℕ), p ≠ 0 → CharP R p → P
h_equal : Algebra ℚ R → P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
p : ℕ
p_charP : CharP R p
⊢ P
[PROOFSTEP]
by_cases p = 0
[GOAL]
case pos
R : Type u_1
inst✝ : CommRing R
P : Prop
h_pos : ∀ (p : ℕ), p ≠ 0 → CharP R p → P
h_equal : Algebra ℚ R → P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
p : ℕ
p_charP : CharP R p
h : p = 0
⊢ P
[PROOFSTEP]
rw [h] at p_charP
[GOAL]
case pos
R : Type u_1
inst✝ : CommRing R
P : Prop
h_pos : ∀ (p : ℕ), p ≠ 0 → CharP R p → P
h_equal : Algebra ℚ R → P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
p : ℕ
p_charP : CharP R 0
h : p = 0
⊢ P
[PROOFSTEP]
haveI h0 : CharZero R := CharP.charP_to_charZero R
[GOAL]
case pos
R : Type u_1
inst✝ : CommRing R
P : Prop
h_pos : ∀ (p : ℕ), p ≠ 0 → CharP R p → P
h_equal : Algebra ℚ R → P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
p : ℕ
p_charP : CharP R 0
h : p = 0
h0 : CharZero R
⊢ P
[PROOFSTEP]
exact split_equalCharZero_mixedCharZero R h_equal h_mixed
[GOAL]
case neg
R : Type u_1
inst✝ : CommRing R
P : Prop
h_pos : ∀ (p : ℕ), p ≠ 0 → CharP R p → P
h_equal : Algebra ℚ R → P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
p : ℕ
p_charP : CharP R p
h : ¬p = 0
⊢ P
[PROOFSTEP]
exact h_pos p h p_charP
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : IsDomain R
h_pos : ∀ (p : ℕ), Nat.Prime p → CharP R p → P
h_equal : Algebra ℚ R → P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
⊢ P
[PROOFSTEP]
refine split_by_characteristic R ?_ h_equal h_mixed
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : IsDomain R
h_pos : ∀ (p : ℕ), Nat.Prime p → CharP R p → P
h_equal : Algebra ℚ R → P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
⊢ ∀ (p : ℕ), p ≠ 0 → CharP R p → P
[PROOFSTEP]
intro p p_pos p_char
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : IsDomain R
h_pos : ∀ (p : ℕ), Nat.Prime p → CharP R p → P
h_equal : Algebra ℚ R → P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
p : ℕ
p_pos : p ≠ 0
p_char : CharP R p
⊢ P
[PROOFSTEP]
have p_prime : Nat.Prime p := or_iff_not_imp_right.mp (CharP.char_is_prime_or_zero R p) p_pos
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : IsDomain R
h_pos : ∀ (p : ℕ), Nat.Prime p → CharP R p → P
h_equal : Algebra ℚ R → P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
p : ℕ
p_pos : p ≠ 0
p_char : CharP R p
p_prime : Nat.Prime p
⊢ P
[PROOFSTEP]
exact h_pos p p_prime p_char
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : LocalRing R
h_pos : ∀ (p : ℕ), IsPrimePow p → CharP R p → P
h_equal : Algebra ℚ R → P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
⊢ P
[PROOFSTEP]
refine' split_by_characteristic R _ h_equal h_mixed
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : LocalRing R
h_pos : ∀ (p : ℕ), IsPrimePow p → CharP R p → P
h_equal : Algebra ℚ R → P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
⊢ ∀ (p : ℕ), p ≠ 0 → CharP R p → P
[PROOFSTEP]
intro p p_pos p_char
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : LocalRing R
h_pos : ∀ (p : ℕ), IsPrimePow p → CharP R p → P
h_equal : Algebra ℚ R → P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
p : ℕ
p_pos : p ≠ 0
p_char : CharP R p
⊢ P
[PROOFSTEP]
have p_ppow : IsPrimePow (p : ℕ) := or_iff_not_imp_left.mp (charP_zero_or_prime_power R p) p_pos
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : LocalRing R
h_pos : ∀ (p : ℕ), IsPrimePow p → CharP R p → P
h_equal : Algebra ℚ R → P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
p : ℕ
p_pos : p ≠ 0
p_char : CharP R p
p_ppow : IsPrimePow p
⊢ P
[PROOFSTEP]
exact h_pos p p_ppow p_char