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

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x y : α
⊢ ∀ (i : Nat),
    UInt.getBit (x <<< y) i =
      (decide (i < length α) && decide (i ≥ toNat y % length α) && UInt.getBit x (i - toNat y % length α))
Tactic:
intro i
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x y : α
i : Nat
⊢ UInt.getBit (x <<< y) i =
    (decide (i < length α) && decide (i ≥ toNat y % length α) && UInt.getBit x (i - toNat y % length α))

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x y : α
i : Nat
⊢ UInt.getBit (x <<< y) i =
    (decide (i < length α) && decide (i ≥ toNat y % length α) && UInt.getBit x (i - toNat y % length α))
Tactic:
unfold UInt.getBit
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x y : α
i : Nat
⊢ Nat.getBit (toNat (x <<< y)) i =
    (decide (i < length α) && decide (i ≥ toNat y % length α) && Nat.getBit (toNat x) (i - toNat y % length α))

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x y : α
i : Nat
⊢ Nat.getBit (toNat (x <<< y)) i =
    (decide (i < length α) && decide (i ≥ toNat y % length α) && Nat.getBit (toNat x) (i - toNat y % length α))
Tactic:
rw [UInt.toNat_shiftLeft, Nat.getBit_mod_two_pow, Nat.shiftLeft_getBit, Bool.and_assoc]
State after:
no goals