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

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
⊢ UInt.getBit (UInt.lsb a) i = true ↔ UInt.getBit a i = true ∧ ∀ (j : Nat), j < i → UInt.getBit a j = false
Tactic:
unfold UInt.getBit
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
⊢ Nat.getBit (toNat (UInt.lsb a)) i = true ↔
    Nat.getBit (toNat a) i = true ∧ ∀ (j : Nat), j < i → Nat.getBit (toNat a) j = false

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
⊢ Nat.getBit (toNat (UInt.lsb a)) i = true ↔
    Nat.getBit (toNat a) i = true ∧ ∀ (j : Nat), j < i → Nat.getBit (toNat a) j = false
Tactic:
rw [UInt.toNat_lsb]
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
⊢ Nat.getBit (Nat.lsb (toNat a)) i = true ↔
    Nat.getBit (toNat a) i = true ∧ ∀ (j : Nat), j < i → Nat.getBit (toNat a) j = false

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
⊢ Nat.getBit (Nat.lsb (toNat a)) i = true ↔
    Nat.getBit (toNat a) i = true ∧ ∀ (j : Nat), j < i → Nat.getBit (toNat a) j = false
Tactic:
exact Nat.lsb_getBit_iff ..
State after:
no goals