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

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
⊢ ∀ (n i : Nat) {x : n < Array.size maskTable}, UInt.getBit maskTable[n] i = (decide (i < length α) && Nat.getBit i n)
Tactic:
intro n i h
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n i : Nat
h : n < Array.size maskTable
⊢ UInt.getBit maskTable[n] i = (decide (i < length α) && Nat.getBit i n)

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n i : Nat
h : n < Array.size maskTable
⊢ UInt.getBit maskTable[n] i = (decide (i < length α) && Nat.getBit i n)
Tactic:
have : n < Nat.log2RU (length α) := maskTable_size (α:=α) ▸ h
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n i : Nat
h : n < Array.size maskTable
this : n < Nat.log2RU (length α)
⊢ UInt.getBit maskTable[n] i = (decide (i < length α) && Nat.getBit i n)

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n i : Nat
h : n < Array.size maskTable
this : n < Nat.log2RU (length α)
⊢ UInt.getBit maskTable[n] i = (decide (i < length α) && Nat.getBit i n)
Tactic:
have := calc
  n < Nat.log2RU (length α) := this
  _ ≤ length α := Nat.log2RU_le_self (length α)
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n i : Nat
h : n < Array.size maskTable
this✝ : n < Nat.log2RU (length α)
this : n < length α
⊢ UInt.getBit maskTable[n] i = (decide (i < length α) && Nat.getBit i n)

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n i : Nat
h : n < Array.size maskTable
this✝ : n < Nat.log2RU (length α)
this : n < length α
⊢ UInt.getBit maskTable[n] i = (decide (i < length α) && Nat.getBit i n)
Tactic:
have := calc
  n < length α := this
  _ < 2^(length α) := Nat.exp_lt_pow (length α) .refl
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n i : Nat
h : n < Array.size maskTable
this✝¹ : n < Nat.log2RU (length α)
this✝ : n < length α
this : n < 2 ^ length α
⊢ UInt.getBit maskTable[n] i = (decide (i < length α) && Nat.getBit i n)

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n i : Nat
h : n < Array.size maskTable
this✝¹ : n < Nat.log2RU (length α)
this✝ : n < length α
this : n < 2 ^ length α
⊢ UInt.getBit maskTable[n] i = (decide (i < length α) && Nat.getBit i n)
Tactic:
unfold maskTable
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n i : Nat
h : n < Array.size maskTable
this✝¹ : n < Nat.log2RU (length α)
this✝ : n < length α
this : n < 2 ^ length α
⊢ UInt.getBit (Array.ofFn fun i => bitmask (OfNat.ofNat ↑i))[n] i = (decide (i < length α) && Nat.getBit i n)

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n i : Nat
h : n < Array.size maskTable
this✝¹ : n < Nat.log2RU (length α)
this✝ : n < length α
this : n < 2 ^ length α
⊢ UInt.getBit (Array.ofFn fun i => bitmask (OfNat.ofNat ↑i))[n] i = (decide (i < length α) && Nat.getBit i n)
Tactic:
rw [Array.getElem_ofFn', getBit_bitmask (OfNat.ofNat n) i (toNat_ofNat (α:=α) n ▸ (Nat.mod_eq_of_lt ‹n < 2^length α›).symm ▸ ‹_›)]
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n i : Nat
h : n < Array.size maskTable
this✝¹ : n < Nat.log2RU (length α)
this✝ : n < length α
this : n < 2 ^ length α
⊢ (decide (i < length α) && Nat.getBit i (toNat (OfNat.ofNat n))) = (decide (i < length α) && Nat.getBit i n)

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n i : Nat
h : n < Array.size maskTable
this✝¹ : n < Nat.log2RU (length α)
this✝ : n < length α
this : n < 2 ^ length α
⊢ (decide (i < length α) && Nat.getBit i (toNat (OfNat.ofNat n))) = (decide (i < length α) && Nat.getBit i n)
Tactic:
rw [toNat_ofNat (α:=α), Nat.mod_eq_of_lt ‹n < 2^length α›]
State after:
no goals