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

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

State before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ toNat (a - a) = toNat 0
Tactic:
simp [toNat_sub, toNat_zero]
State after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ (toNat a + (2 ^ length α - toNat a)) % 2 ^ length α = 0

State before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ (toNat a + (2 ^ length α - toNat a)) % 2 ^ length α = 0
Tactic:
rw [ ←Nat.add_sub_assoc (Nat.le_of_lt (toNat_lt a))]
State after:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ (toNat a + 2 ^ length α - toNat a) % 2 ^ length α = 0

State before:
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ (toNat a + 2 ^ length α - toNat a) % 2 ^ length α = 0
Tactic:
rw [Nat.add_comm, Nat.add_sub_cancel, Nat.mod_self]
State after:
no goals