Theorem: UInt.getBit_land (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_land]
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 and (toNat x) (toNat y)).getBit i; rw [Nat.bitwise_getBit]
State after:
no goals