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

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x y : α
⊢ ∀ (i : Nat), UInt.getBit (x ||| y) i = (UInt.getBit x i || UInt.getBit y i)
Tactic:
intro i
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x y : α
i : Nat
⊢ UInt.getBit (x ||| y) i = (UInt.getBit x i || UInt.getBit y i)

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x y : α
i : Nat
⊢ UInt.getBit (x ||| y) i = (UInt.getBit x i || UInt.getBit y i)
Tactic:
unfold UInt.getBit
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x y : α
i : Nat
⊢ Nat.getBit (toNat (x ||| y)) i = (Nat.getBit (toNat x) i || Nat.getBit (toNat y) i)

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x y : α
i : Nat
⊢ Nat.getBit (toNat (x ||| y)) i = (Nat.getBit (toNat x) i || Nat.getBit (toNat y) i)
Tactic:
rw [toNat_lor]
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x y : α
i : Nat
⊢ Nat.getBit (toNat x ||| toNat y) i = (Nat.getBit (toNat x) i || Nat.getBit (toNat y) i)

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x y : α
i : Nat
⊢ Nat.getBit (toNat x ||| toNat y) i = (Nat.getBit (toNat x) i || Nat.getBit (toNat y) i)
Tactic:
conv => lhs; change (Nat.bitwise or (toNat x) (toNat y)).getBit i; rw [Nat.bitwise_getBit]
State after:
no goals