Theorem: isEmpty_eq_size_beq_zero (Algorithm/Data/Classes/Size.lean)

State before:
C : Type u_1
α : Type ?u.736
inst✝ : Size C
c : C
⊢ isEmpty c = (size c == 0)
Tactic:
rw [isEmpty_eq_decide_size]
State after:
C : Type u_1
α : Type ?u.736
inst✝ : Size C
c : C
⊢ decide (size c = 0) = (size c == 0)

State before:
C : Type u_1
α : Type ?u.736
inst✝ : Size C
c : C
⊢ decide (size c = 0) = (size c == 0)
Tactic:
cases size c <;> rfl
State after:
no goals