Theorem: UInt.xor_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_xor]
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.xor_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.xor_mod_two_pow]
State after:
no goals