Theorem: UInt.getBit_zero (Algdata/Classes/UInt.lean)

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
⊢ ∀ (i : Nat), UInt.getBit 0 i = false
Tactic:
unfold UInt.getBit
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
⊢ ∀ (i : Nat), Nat.getBit (toNat 0) i = false

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
⊢ ∀ (i : Nat), Nat.getBit (toNat 0) i = false
Tactic:
simp [toNat_zero]
State after:
no goals