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

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ ~~~~~~a = a
Tactic:
apply toNat_inj
State after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ toNat (~~~~~~a) = toNat a

State before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ toNat (~~~~~~a) = toNat a
Tactic:
simp [toNat_complement]
State after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ 2 ^ length α - (2 ^ length α - (toNat a + 1) + 1) = toNat a

State before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ 2 ^ length α - (2 ^ length α - (toNat a + 1) + 1) = toNat a
Tactic:
calc
  2^length α - (2^length α - (toNat a + 1) + 1)
    = 2^length α - (2^length α - toNat a - 1 + 1) := rfl
  _ = 2^length α - (2^length α - toNat a) := by rw [Nat.sub_add_cancel (Nat.sub_pos_of_lt (toNat_lt a))]
  _ = toNat a := Nat.sub_sub_self (Nat.le_of_lt (toNat_lt a))
State after:
no goals

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ 2 ^ length α - (2 ^ length α - toNat a - 1 + 1) = 2 ^ length α - (2 ^ length α - toNat a)
Tactic:
rw [Nat.sub_add_cancel (Nat.sub_pos_of_lt (toNat_lt a))]
State after:
no goals