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
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ↑(AddSubgroup.index (Submodule.toAddSubgroup I)) = 0
rw [AddSubgroup.index, Nat.card_eq]
case inl
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hq : Finite (R ⧸ Submodule.toAddSubgroup I)
⊢ ↑(Fintype.card (R ⧸ Submodule.toAddSubgroup I)) = 0

case inr
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hq : ¬Finite (R ⧸ Submodule.toAddSubgroup I)
⊢ ↑0 = 0
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
split_ifs with hq
case inr
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hq : ¬Finite (R ⧸ Submodule.toAddSubgroup I)
⊢ ↑0 = 0

case inl
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hq : Finite (R ⧸ Submodule.toAddSubgroup I)
⊢ ↑(Fintype.card (R ⧸ Submodule.toAddSubgroup I)) = 0
case inl
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hq : Finite (R ⧸ Submodule.toAddSubgroup I)
⊢ ↑(Fintype.card (R ⧸ Submodule.toAddSubgroup I)) = 0

case inr
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hq : ¬Finite (R ⧸ Submodule.toAddSubgroup I)
⊢ ↑0 = 0
swap
case inl
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hq : Finite (R ⧸ Submodule.toAddSubgroup I)
⊢ ↑(Fintype.card (R ⧸ Submodule.toAddSubgroup I)) = 0
case inr
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hq : ¬Finite (R ⧸ Submodule.toAddSubgroup I)
⊢ ↑0 = 0

case inl
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hq : Finite (R ⧸ Submodule.toAddSubgroup I)
⊢ ↑(Fintype.card (R ⧸ Submodule.toAddSubgroup I)) = 0
simp
case inl
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
case inl
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hq : Finite (R ⧸ Submodule.toAddSubgroup I)
⊢ ↑(Fintype.card (R ⧸ Submodule.toAddSubgroup I)) = 0
by_contra h
case inl
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
case inl
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
letI : Fintype (R ⧸ I) := @Fintype.ofFinite _ hq
case inl
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
case inl
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
have h : (Fintype.card (R ⧸ I) : R ⧸ I) ≠ 0 := h
no goals
case inl
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
simp at h