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

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

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
⊢ (2 ^ length α - (toNat a + toNat 1) % 2 ^ length α) % 2 ^ length α = 2 ^ length α - (toNat a + 1)
Tactic:
have : toNat (1 : α) = 1 % 2^length α := toNat_ofNat 1
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
this : toNat 1 = 1 % 2 ^ length α
⊢ (2 ^ length α - (toNat a + toNat 1) % 2 ^ length α) % 2 ^ length α = 2 ^ length α - (toNat a + 1)

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
this : toNat 1 = 1 % 2 ^ length α
⊢ (2 ^ length α - (toNat a + toNat 1) % 2 ^ length α) % 2 ^ length α = 2 ^ length α - (toNat a + 1)
Tactic:
rw [this, Nat.add_mod_mod]
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
this : toNat 1 = 1 % 2 ^ length α
⊢ (2 ^ length α - (toNat a + 1) % 2 ^ length α) % 2 ^ length α = 2 ^ length α - (toNat a + 1)

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
this : toNat 1 = 1 % 2 ^ length α
⊢ (2 ^ length α - (toNat a + 1) % 2 ^ length α) % 2 ^ length α = 2 ^ length α - (toNat a + 1)
Tactic:
cases Nat.lt_or_eq_of_le (toNat_lt a)
State after:
case inl
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
this : toNat 1 = 1 % 2 ^ length α
h✝ : Nat.succ (toNat a) < 2 ^ length α
⊢ (2 ^ length α - (toNat a + 1) % 2 ^ length α) % 2 ^ length α = 2 ^ length α - (toNat a + 1)

case inr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
this : toNat 1 = 1 % 2 ^ length α
h✝ : Nat.succ (toNat a) = 2 ^ length α
⊢ (2 ^ length α - (toNat a + 1) % 2 ^ length α) % 2 ^ length α = 2 ^ length α - (toNat a + 1)

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
this : toNat 1 = 1 % 2 ^ length α
h : Nat.succ (toNat a) < 2 ^ length α
⊢ (2 ^ length α - (toNat a + 1) % 2 ^ length α) % 2 ^ length α = 2 ^ length α - (toNat a + 1)
Tactic:
case inl h =>
  have : toNat a + 1 < 2^length α := h
  have : 2^length α - (toNat a + 1) < 2^length α :=
    Nat.sub_lt_self (Nat.zero_lt_succ _) (toNat_lt a)
  rw [
    Nat.mod_eq_of_lt ‹toNat a + 1 < 2^length α›,
    Nat.mod_eq_of_lt ‹2^length α - (toNat a + 1) < 2^length α›
  ]
State after:
no goals

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
this : toNat 1 = 1 % 2 ^ length α
h : Nat.succ (toNat a) = 2 ^ length α
⊢ (2 ^ length α - (toNat a + 1) % 2 ^ length α) % 2 ^ length α = 2 ^ length α - (toNat a + 1)
Tactic:
case inr h =>
  have : toNat a + 1 = 2^length α := h
  simp [this]
State after:
no goals

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
this : toNat 1 = 1 % 2 ^ length α
h : Nat.succ (toNat a) < 2 ^ length α
⊢ (2 ^ length α - (toNat a + 1) % 2 ^ length α) % 2 ^ length α = 2 ^ length α - (toNat a + 1)
Tactic:
have : toNat a + 1 < 2^length α := h
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
this✝ : toNat 1 = 1 % 2 ^ length α
h : Nat.succ (toNat a) < 2 ^ length α
this : toNat a + 1 < 2 ^ length α
⊢ (2 ^ length α - (toNat a + 1) % 2 ^ length α) % 2 ^ length α = 2 ^ length α - (toNat a + 1)

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
this✝ : toNat 1 = 1 % 2 ^ length α
h : Nat.succ (toNat a) < 2 ^ length α
this : toNat a + 1 < 2 ^ length α
⊢ (2 ^ length α - (toNat a + 1) % 2 ^ length α) % 2 ^ length α = 2 ^ length α - (toNat a + 1)
Tactic:
have : 2^length α - (toNat a + 1) < 2^length α :=
  Nat.sub_lt_self (Nat.zero_lt_succ _) (toNat_lt a)
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
this✝¹ : toNat 1 = 1 % 2 ^ length α
h : Nat.succ (toNat a) < 2 ^ length α
this✝ : toNat a + 1 < 2 ^ length α
this : 2 ^ length α - (toNat a + 1) < 2 ^ length α
⊢ (2 ^ length α - (toNat a + 1) % 2 ^ length α) % 2 ^ length α = 2 ^ length α - (toNat a + 1)

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
this✝¹ : toNat 1 = 1 % 2 ^ length α
h : Nat.succ (toNat a) < 2 ^ length α
this✝ : toNat a + 1 < 2 ^ length α
this : 2 ^ length α - (toNat a + 1) < 2 ^ length α
⊢ (2 ^ length α - (toNat a + 1) % 2 ^ length α) % 2 ^ length α = 2 ^ length α - (toNat a + 1)
Tactic:
rw [
  Nat.mod_eq_of_lt ‹toNat a + 1 < 2^length α›,
  Nat.mod_eq_of_lt ‹2^length α - (toNat a + 1) < 2^length α›
]
State after:
no goals

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
this : toNat 1 = 1 % 2 ^ length α
h : Nat.succ (toNat a) = 2 ^ length α
⊢ (2 ^ length α - (toNat a + 1) % 2 ^ length α) % 2 ^ length α = 2 ^ length α - (toNat a + 1)
Tactic:
have : toNat a + 1 = 2^length α := h
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
this✝ : toNat 1 = 1 % 2 ^ length α
h : Nat.succ (toNat a) = 2 ^ length α
this : toNat a + 1 = 2 ^ length α
⊢ (2 ^ length α - (toNat a + 1) % 2 ^ length α) % 2 ^ length α = 2 ^ length α - (toNat a + 1)

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
this✝ : toNat 1 = 1 % 2 ^ length α
h : Nat.succ (toNat a) = 2 ^ length α
this : toNat a + 1 = 2 ^ length α
⊢ (2 ^ length α - (toNat a + 1) % 2 ^ length α) % 2 ^ length α = 2 ^ length α - (toNat a + 1)
Tactic:
simp [this]
State after:
no goals