Theorem: UInt.lor_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_lor]
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.lor_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.lor_mod_two_pow]
State after:
no goals