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

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
⊢ ∀ (i : Nat), UInt.getBit (~~~x) i = (UInt.getBit x i != decide (i < length α))
Tactic:
intro i
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
i : Nat
⊢ UInt.getBit (~~~x) i = (UInt.getBit x i != decide (i < length α))

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
i : Nat
⊢ UInt.getBit (~~~x) i = (UInt.getBit x i != decide (i < length α))
Tactic:
unfold UInt.getBit
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
i : Nat
⊢ Nat.getBit (toNat (~~~x)) i = (Nat.getBit (toNat x) i != decide (i < length α))

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
i : Nat
⊢ Nat.getBit (toNat (~~~x)) i = (Nat.getBit (toNat x) i != decide (i < length α))
Tactic:
rw [UInt.toNat_complement, Nat.add_comm, Nat.sub_add_eq]
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
i : Nat
⊢ Nat.getBit (2 ^ length α - 1 - toNat x) i = (Nat.getBit (toNat x) i != decide (i < length α))

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
i : Nat
⊢ Nat.getBit (2 ^ length α - 1 - toNat x) i = (Nat.getBit (toNat x) i != decide (i < length α))
Tactic:
have : 2^length α - 1 - UInt.toNat x = (2^length α - 1) ^^^ UInt.toNat x := by
  apply Nat.sub_eq_xor
  rw [Nat.land_comm, Nat.land_exp2_sub_one, Nat.mod_eq_of_lt (UInt.toNat_lt x)]
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
i : Nat
this : 2 ^ length α - 1 - toNat x = 2 ^ length α - 1 ^^^ toNat x
⊢ Nat.getBit (2 ^ length α - 1 - toNat x) i = (Nat.getBit (toNat x) i != decide (i < length α))

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
i : Nat
this : 2 ^ length α - 1 - toNat x = 2 ^ length α - 1 ^^^ toNat x
⊢ Nat.getBit (2 ^ length α - 1 - toNat x) i = (Nat.getBit (toNat x) i != decide (i < length α))
Tactic:
rw [this, Nat.xor_getBit, Nat.getBit_pred_two_pow, Bool.bne_comm]
State after:
no goals

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
i : Nat
⊢ 2 ^ length α - 1 - toNat x = 2 ^ length α - 1 ^^^ toNat x
Tactic:
apply Nat.sub_eq_xor
State after:
case incl
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
i : Nat
⊢ 2 ^ length α - 1 &&& toNat x = toNat x

State before:
case incl
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
i : Nat
⊢ 2 ^ length α - 1 &&& toNat x = toNat x
Tactic:
rw [Nat.land_comm, Nat.land_exp2_sub_one, Nat.mod_eq_of_lt (UInt.toNat_lt x)]
State after:
no goals