Theorem: ENat.mul_infty (ECTate/Data/Nat/Enat.lean)

State before:
case top
R : Type u
inst✝ : CommRing R
x : R
I : Ideal R
J : Ideal (R ⧸ I)
⊢ ⊤ * ⊤ = if ⊤ = 0 then 0 else ⊤
Tactic:
simp
State after:
no goals

State before:
case nat
R : Type u
inst✝ : CommRing R
x : R
I : Ideal R
J : Ideal (R ⧸ I)
n : ℕ
⊢ ↑n * ⊤ = if ↑n = 0 then 0 else ⊤
Tactic:
cases n
State after:
case nat.zero
R : Type u
inst✝ : CommRing R
x : R
I : Ideal R
J : Ideal (R ⧸ I)
⊢ ↑Nat.zero * ⊤ = if ↑Nat.zero = 0 then 0 else ⊤

case nat.succ
R : Type u
inst✝ : CommRing R
x : R
I : Ideal R
J : Ideal (R ⧸ I)
n✝ : ℕ
⊢ ↑(Nat.succ n✝) * ⊤ = if ↑(Nat.succ n✝) = 0 then 0 else ⊤

State before:
case nat.zero
R : Type u
inst✝ : CommRing R
x : R
I : Ideal R
J : Ideal (R ⧸ I)
⊢ ↑Nat.zero * ⊤ = if ↑Nat.zero = 0 then 0 else ⊤
Tactic:
simp
State after:
no goals

State before:
case nat.succ
R : Type u
inst✝ : CommRing R
x : R
I : Ideal R
J : Ideal (R ⧸ I)
n✝ : ℕ
⊢ ↑(Nat.succ n✝) * ⊤ = if ↑(Nat.succ n✝) = 0 then 0 else ⊤
Tactic:
simp [add_mul]
State after:
no goals