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

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b c : α
⊢ a <<< b <<< c = a <<< c <<< b
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)

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

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

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