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