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

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ (a &&& b) <<< c = a <<< c &&& b <<< c
Tactic:
apply toNat_inj
State after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ toNat ((a &&& b) <<< c) = toNat (a <<< c &&& b <<< c)

State before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ toNat ((a &&& b) <<< c) = toNat (a <<< c &&& b <<< c)
Tactic:
simp only [toNat_shiftLeft, toNat_land]
State after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ (toNat a &&& toNat b) <<< (toNat c % length α) % 2 ^ length α =
    toNat a <<< (toNat c % length α) % 2 ^ length α &&& toNat b <<< (toNat c % length α) % 2 ^ length α

State before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ (toNat a &&& toNat b) <<< (toNat c % length α) % 2 ^ length α =
    toNat a <<< (toNat c % length α) % 2 ^ length α &&& toNat b <<< (toNat c % length α) % 2 ^ length α
Tactic:
conv =>
  lhs; change (toNat a &&& toNat b) <<< (toNat c % length α) % 2^length α
  rw [Nat.land_shiftLeft]
State after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ (toNat a <<< (toNat c % length α) &&& toNat b <<< (toNat c % length α)) % 2 ^ length α =
    toNat a <<< (toNat c % length α) % 2 ^ length α &&& toNat b <<< (toNat c % length α) % 2 ^ length α

State before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ (toNat a <<< (toNat c % length α) &&& toNat b <<< (toNat c % length α)) % 2 ^ length α =
    toNat a <<< (toNat c % length α) % 2 ^ length α &&& toNat b <<< (toNat c % length α) % 2 ^ length α
Tactic:
simp [Nat.land_mod_two_pow]
State after:
no goals