[GOAL]
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : CharP R p
I : Ideal R
h : ∀ (x : ℕ), ↑x ∈ I → ↑x = 0
x : ℕ
⊢ ↑x = 0 ↔ p ∣ x
[PROOFSTEP]
rw [← cast_eq_zero_iff R p x, ← map_natCast (Ideal.Quotient.mk I)]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : CharP R p
I : Ideal R
h : ∀ (x : ℕ), ↑x ∈ I → ↑x = 0
x : ℕ
⊢ ↑(Ideal.Quotient.mk I) ↑x = 0 ↔ ↑x = 0
[PROOFSTEP]
refine' Ideal.Quotient.eq.trans (_ : ↑x - 0 ∈ I ↔ _)
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : CharP R p
I : Ideal R
h : ∀ (x : ℕ), ↑x ∈ I → ↑x = 0
x : ℕ
⊢ ↑x - 0 ∈ I ↔ ↑x = 0
[PROOFSTEP]
rw [sub_zero]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : CharP R p
I : Ideal R
h : ∀ (x : ℕ), ↑x ∈ I → ↑x = 0
x : ℕ
⊢ ↑x ∈ I ↔ ↑x = 0
[PROOFSTEP]
exact ⟨h x, fun h' => h'.symm ▸ I.zero_mem⟩
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ↑(AddSubgroup.index (Submodule.toAddSubgroup I)) = 0
[PROOFSTEP]
rw [AddSubgroup.index, Nat.card_eq]
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ↑(if h : Finite (R ⧸ Submodule.toAddSubgroup I) then Fintype.card (R ⧸ Submodule.toAddSubgroup I) else 0) = 0
[PROOFSTEP]
split_ifs with hq
[GOAL]
case pos
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hq : Finite (R ⧸ Submodule.toAddSubgroup I)
⊢ ↑(Fintype.card (R ⧸ Submodule.toAddSubgroup I)) = 0
case neg R : Type u_1 inst✝ : CommRing R I : Ideal R hq : ¬Finite (R ⧸ Submodule.toAddSubgroup I) ⊢ ↑0 = 0
[PROOFSTEP]
swap
[GOAL]
case neg
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hq : ¬Finite (R ⧸ Submodule.toAddSubgroup I)
⊢ ↑0 = 0
case pos
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hq : Finite (R ⧸ Submodule.toAddSubgroup I)
⊢ ↑(Fintype.card (R ⧸ Submodule.toAddSubgroup I)) = 0
[PROOFSTEP]
simp
[GOAL]
case pos
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hq : Finite (R ⧸ Submodule.toAddSubgroup I)
⊢ ↑(Fintype.card (R ⧸ Submodule.toAddSubgroup I)) = 0
[PROOFSTEP]
by_contra h
[GOAL]
case pos
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hq : Finite (R ⧸ Submodule.toAddSubgroup I)
h : ¬↑(Fintype.card (R ⧸ Submodule.toAddSubgroup I)) = 0
⊢ False
[PROOFSTEP]
letI : Fintype (R ⧸ I) := @Fintype.ofFinite _ hq
[GOAL]
case pos
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hq : Finite (R ⧸ Submodule.toAddSubgroup I)
h : ¬↑(Fintype.card (R ⧸ Submodule.toAddSubgroup I)) = 0
this : Fintype (R ⧸ I) := Fintype.ofFinite (R ⧸ I)
⊢ False
[PROOFSTEP]
have h : (Fintype.card (R ⧸ I) : R ⧸ I) ≠ 0 := h
[GOAL]
case pos
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hq : Finite (R ⧸ Submodule.toAddSubgroup I)
h✝ : ¬↑(Fintype.card (R ⧸ Submodule.toAddSubgroup I)) = 0
this : Fintype (R ⧸ I) := Fintype.ofFinite (R ⧸ I)
h : ↑(Fintype.card (R ⧸ I)) ≠ 0
⊢ False
[PROOFSTEP]
simp at h 
