Theorem: ENat.infty_mul (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 [mul_add]
State after:
no goals