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

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
⊢ bitcnt x =
    Nat.fold (fun i x => (x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i))
      (Nat.log2RU (length α)) x
Tactic:
have : bitcnt x = (Prod.fst $ (x,1) |> Fin.foldAll λ (i : Fin (Nat.log2RU (length α))) ((x,k) : α × α) => ((x &&& ~~~ bitmask (OfNat.ofNat i.1)) + ((x &&& bitmask (OfNat.ofNat i.1)) >>> k), k <<< 1)) := by
  unfold bitcnt; unfold maskTable
  simp only [Array.foldl_ofFn_eq]; rfl
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
this :
  bitcnt x =
    (Fin.foldAll
        (fun i x =>
          match x with
          | (x, k) => ((x &&& ~~~bitmask (OfNat.ofNat ↑i)) + (x &&& bitmask (OfNat.ofNat ↑i)) >>> k, k <<< 1))
        (x, 1)).fst
⊢ bitcnt x =
    Nat.fold (fun i x => (x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i))
      (Nat.log2RU (length α)) x

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
this :
  bitcnt x =
    (Fin.foldAll
        (fun i x =>
          match x with
          | (x, k) => ((x &&& ~~~bitmask (OfNat.ofNat ↑i)) + (x &&& bitmask (OfNat.ofNat ↑i)) >>> k, k <<< 1))
        (x, 1)).fst
⊢ bitcnt x =
    Nat.fold (fun i x => (x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i))
      (Nat.log2RU (length α)) x
Tactic:
rw [this]
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
this :
  bitcnt x =
    (Fin.foldAll
        (fun i x =>
          match x with
          | (x, k) => ((x &&& ~~~bitmask (OfNat.ofNat ↑i)) + (x &&& bitmask (OfNat.ofNat ↑i)) >>> k, k <<< 1))
        (x, 1)).fst
⊢ (Fin.foldAll
        (fun i x =>
          match x with
          | (x, k) => ((x &&& ~~~bitmask (OfNat.ofNat ↑i)) + (x &&& bitmask (OfNat.ofNat ↑i)) >>> k, k <<< 1))
        (x, 1)).fst =
    Nat.fold (fun i x => (x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i))
      (Nat.log2RU (length α)) x

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
this :
  bitcnt x =
    (Fin.foldAll
        (fun i x =>
          match x with
          | (x, k) => ((x &&& ~~~bitmask (OfNat.ofNat ↑i)) + (x &&& bitmask (OfNat.ofNat ↑i)) >>> k, k <<< 1))
        (x, 1)).fst
⊢ (Fin.foldAll
        (fun i x =>
          match x with
          | (x, k) => ((x &&& ~~~bitmask (OfNat.ofNat ↑i)) + (x &&& bitmask (OfNat.ofNat ↑i)) >>> k, k <<< 1))
        (x, 1)).fst =
    Nat.fold (fun i x => (x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i))
      (Nat.log2RU (length α)) x
Tactic:
clear this
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
⊢ (Fin.foldAll
        (fun i x =>
          match x with
          | (x, k) => ((x &&& ~~~bitmask (OfNat.ofNat ↑i)) + (x &&& bitmask (OfNat.ofNat ↑i)) >>> k, k <<< 1))
        (x, 1)).fst =
    Nat.fold (fun i x => (x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i))
      (Nat.log2RU (length α)) x

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
⊢ (Fin.foldAll
        (fun i x =>
          match x with
          | (x, k) => ((x &&& ~~~bitmask (OfNat.ofNat ↑i)) + (x &&& bitmask (OfNat.ofNat ↑i)) >>> k, k <<< 1))
        (x, 1)).fst =
    Nat.fold (fun i x => (x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i))
      (Nat.log2RU (length α)) x
Tactic:
apply Eq.trans $ congrArg Prod.fst $ Fin.foldAll_comp_val (n:=Nat.log2RU (length α)) (f:=λ (i : Nat) ((x,k) : α × α) => ((x &&& ~~~ bitmask (OfNat.ofNat i)) + ((x &&& bitmask (OfNat.ofNat i)) >>> k), k <<< 1)) (init:=(x,1))
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
⊢ (Nat.fold
        (fun i x =>
          match x with
          | (x, k) => ((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> k, k <<< 1))
        (Nat.log2RU (length α)) (x, 1)).fst =
    Nat.fold (fun i x => (x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i))
      (Nat.log2RU (length α)) x

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
⊢ (Nat.fold
        (fun i x =>
          match x with
          | (x, k) => ((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> k, k <<< 1))
        (Nat.log2RU (length α)) (x, 1)).fst =
    Nat.fold (fun i x => (x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i))
      (Nat.log2RU (length α)) x
Tactic:
generalize hn : Nat.log2RU (length α) = n
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
n : Nat
hn : Nat.log2RU (length α) = n
⊢ (Nat.fold
        (fun i x =>
          match x with
          | (x, k) => ((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> k, k <<< 1))
        n (x, 1)).fst =
    Nat.fold (fun i x => (x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i))
      n x

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
n : Nat
hn : Nat.log2RU (length α) = n
⊢ (Nat.fold
        (fun i x =>
          match x with
          | (x, k) => ((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> k, k <<< 1))
        n (x, 1)).fst =
    Nat.fold (fun i x => (x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i))
      n x
Tactic:
have : Nat.fold (λ i ((x,k) : α × α) => ((x &&& ~~~ bitmask (OfNat.ofNat i)) + ((x &&& bitmask (OfNat.ofNat i)) >>> k), k <<< 1)) n (x,1) = Nat.fold (λ i ((x,_) : α × α) => ((x &&& ~~~ bitmask (α:=α) (OfNat.ofNat i)) + ((x &&& bitmask (α:=α) (OfNat.ofNat i)) >>> ((1 : α) <<< OfNat.ofNat i)), (1 : α) <<< OfNat.ofNat (i+1))) n (x,1) := by
  apply Nat.fold_congr
  case zero => dsimp; rw [UInt.shiftLeft_zero]
  case succ =>
    intro i a h; cases a with | mk x k =>
    dsimp
    apply congrArg (Prod.mk _)
    rw [UInt.shiftLeft_shiftLeft 1 (OfNat.ofNat (i+1)) 1, UInt.ofNat_add]
    . simp only [UInt.toNat_ofNat, UInt.toNat_ofNat 1]
      have : length α > 0 :=
        hn |> (length α).rec (λ (hn : 0 = n) => nomatch (trans h hn.symm)) (λ l _ _ => l.zero_lt_succ)
      have : n < length α := hn ▸ Nat.log2RU_lt_self _ ‹length α > 0›
      have : n < 2^length α := trans this (Nat.exp_lt_pow (length α) .refl)
      rw [
          Nat.mod_eq_of_lt (trans h this),
          Nat.mod_eq_of_lt (trans (trans (Nat.le_add_left 1 i) h) this)
      ]
      exact trans (r:=LE.le) (h : i+2 ≤ n) ‹n < length α›
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
n : Nat
hn : Nat.log2RU (length α) = n
this :
  Nat.fold
      (fun i x =>
        match x with
        | (x, k) => ((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> k, k <<< 1))
      n (x, 1) =
    Nat.fold
      (fun i x =>
        match x with
        | (x, snd) =>
          ((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i),
            1 <<< OfNat.ofNat (i + 1)))
      n (x, 1)
⊢ (Nat.fold
        (fun i x =>
          match x with
          | (x, k) => ((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> k, k <<< 1))
        n (x, 1)).fst =
    Nat.fold (fun i x => (x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i))
      n x

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
n : Nat
hn : Nat.log2RU (length α) = n
this :
  Nat.fold
      (fun i x =>
        match x with
        | (x, k) => ((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> k, k <<< 1))
      n (x, 1) =
    Nat.fold
      (fun i x =>
        match x with
        | (x, snd) =>
          ((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i),
            1 <<< OfNat.ofNat (i + 1)))
      n (x, 1)
⊢ (Nat.fold
        (fun i x =>
          match x with
          | (x, k) => ((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> k, k <<< 1))
        n (x, 1)).fst =
    Nat.fold (fun i x => (x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i))
      n x
Tactic:
rw [this]
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
n : Nat
hn : Nat.log2RU (length α) = n
this :
  Nat.fold
      (fun i x =>
        match x with
        | (x, k) => ((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> k, k <<< 1))
      n (x, 1) =
    Nat.fold
      (fun i x =>
        match x with
        | (x, snd) =>
          ((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i),
            1 <<< OfNat.ofNat (i + 1)))
      n (x, 1)
⊢ (Nat.fold
        (fun i x =>
          match x with
          | (x, snd) =>
            ((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i),
              1 <<< OfNat.ofNat (i + 1)))
        n (x, 1)).fst =
    Nat.fold (fun i x => (x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i))
      n x

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
n : Nat
hn : Nat.log2RU (length α) = n
this :
  Nat.fold
      (fun i x =>
        match x with
        | (x, k) => ((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> k, k <<< 1))
      n (x, 1) =
    Nat.fold
      (fun i x =>
        match x with
        | (x, snd) =>
          ((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i),
            1 <<< OfNat.ofNat (i + 1)))
      n (x, 1)
⊢ (Nat.fold
        (fun i x =>
          match x with
          | (x, snd) =>
            ((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i),
              1 <<< OfNat.ofNat (i + 1)))
        n (x, 1)).fst =
    Nat.fold (fun i x => (x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i))
      n x
Tactic:
clear this
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
n : Nat
hn : Nat.log2RU (length α) = n
⊢ (Nat.fold
        (fun i x =>
          match x with
          | (x, snd) =>
            ((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i),
              1 <<< OfNat.ofNat (i + 1)))
        n (x, 1)).fst =
    Nat.fold (fun i x => (x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i))
      n x

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
n : Nat
hn : Nat.log2RU (length α) = n
⊢ (Nat.fold
        (fun i x =>
          match x with
          | (x, snd) =>
            ((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i),
              1 <<< OfNat.ofNat (i + 1)))
        n (x, 1)).fst =
    Nat.fold (fun i x => (x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i))
      n x
Tactic:
apply Eq.symm
State after:
case h
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
n : Nat
hn : Nat.log2RU (length α) = n
⊢ Nat.fold (fun i x => (x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i)) n
      x =
    (Nat.fold
        (fun i x =>
          match x with
          | (x, snd) =>
            ((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i),
              1 <<< OfNat.ofNat (i + 1)))
        n (x, 1)).fst

State before:
case h
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
n : Nat
hn : Nat.log2RU (length α) = n
⊢ Nat.fold (fun i x => (x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i)) n
      x =
    (Nat.fold
        (fun i x =>
          match x with
          | (x, snd) =>
            ((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i),
              1 <<< OfNat.ofNat (i + 1)))
        n (x, 1)).fst
Tactic:
apply Nat.fold_hom Prod.fst _ _ _ (x,1)
State after:
case h
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
n : Nat
hn : Nat.log2RU (length α) = n
⊢ ∀ (i : Nat) (a : α × α),
    i < n →
      (a.fst &&& ~~~bitmask (OfNat.ofNat i)) + (a.fst &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i) =
        (match a with
          | (x, snd) =>
            ((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i),
              1 <<< OfNat.ofNat (i + 1))).fst

State before:
case h
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
n : Nat
hn : Nat.log2RU (length α) = n
⊢ ∀ (i : Nat) (a : α × α),
    i < n →
      (a.fst &&& ~~~bitmask (OfNat.ofNat i)) + (a.fst &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i) =
        (match a with
          | (x, snd) =>
            ((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i),
              1 <<< OfNat.ofNat (i + 1))).fst
Tactic:
intro i z _
State after:
case h
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
n : Nat
hn : Nat.log2RU (length α) = n
i : Nat
z : α × α
a✝ : i < n
⊢ (z.fst &&& ~~~bitmask (OfNat.ofNat i)) + (z.fst &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i) =
    (match z with
      | (x, snd) =>
        ((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i),
          1 <<< OfNat.ofNat (i + 1))).fst

State before:
case h
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
n : Nat
hn : Nat.log2RU (length α) = n
i : Nat
z : α × α
a✝ : i < n
⊢ (z.fst &&& ~~~bitmask (OfNat.ofNat i)) + (z.fst &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i) =
    (match z with
      | (x, snd) =>
        ((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i),
          1 <<< OfNat.ofNat (i + 1))).fst
Tactic:
cases z with | mk x k => rfl
State after:
no goals

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
⊢ bitcnt x =
    (Fin.foldAll
        (fun i x =>
          match x with
          | (x, k) => ((x &&& ~~~bitmask (OfNat.ofNat ↑i)) + (x &&& bitmask (OfNat.ofNat ↑i)) >>> k, k <<< 1))
        (x, 1)).fst
Tactic:
unfold bitcnt
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
⊢ (Array.foldl
        (fun x mask =>
          match x with
          | (x, k) => ((x &&& ~~~mask) + (x &&& mask) >>> k, k <<< 1))
        (x, 1) maskTable 0 (Array.size maskTable)).fst =
    (Fin.foldAll
        (fun i x =>
          match x with
          | (x, k) => ((x &&& ~~~bitmask (OfNat.ofNat ↑i)) + (x &&& bitmask (OfNat.ofNat ↑i)) >>> k, k <<< 1))
        (x, 1)).fst

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
⊢ (Array.foldl
        (fun x mask =>
          match x with
          | (x, k) => ((x &&& ~~~mask) + (x &&& mask) >>> k, k <<< 1))
        (x, 1) maskTable 0 (Array.size maskTable)).fst =
    (Fin.foldAll
        (fun i x =>
          match x with
          | (x, k) => ((x &&& ~~~bitmask (OfNat.ofNat ↑i)) + (x &&& bitmask (OfNat.ofNat ↑i)) >>> k, k <<< 1))
        (x, 1)).fst
Tactic:
unfold maskTable
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
⊢ (Array.foldl
        (fun x mask =>
          match x with
          | (x, k) => ((x &&& ~~~mask) + (x &&& mask) >>> k, k <<< 1))
        (x, 1) (Array.ofFn fun i => bitmask (OfNat.ofNat ↑i)) 0
        (Array.size (Array.ofFn fun i => bitmask (OfNat.ofNat ↑i)))).fst =
    (Fin.foldAll
        (fun i x =>
          match x with
          | (x, k) => ((x &&& ~~~bitmask (OfNat.ofNat ↑i)) + (x &&& bitmask (OfNat.ofNat ↑i)) >>> k, k <<< 1))
        (x, 1)).fst

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
⊢ (Array.foldl
        (fun x mask =>
          match x with
          | (x, k) => ((x &&& ~~~mask) + (x &&& mask) >>> k, k <<< 1))
        (x, 1) (Array.ofFn fun i => bitmask (OfNat.ofNat ↑i)) 0
        (Array.size (Array.ofFn fun i => bitmask (OfNat.ofNat ↑i)))).fst =
    (Fin.foldAll
        (fun i x =>
          match x with
          | (x, k) => ((x &&& ~~~bitmask (OfNat.ofNat ↑i)) + (x &&& bitmask (OfNat.ofNat ↑i)) >>> k, k <<< 1))
        (x, 1)).fst
Tactic:
simp only [Array.foldl_ofFn_eq]
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
⊢ (Fin.foldAll
        ((flip fun x mask => ((x.fst &&& ~~~mask) + (x.fst &&& mask) >>> x.snd, x.snd <<< 1)) ∘ fun i =>
          bitmask (OfNat.ofNat ↑i))
        (x, 1)).fst =
    (Fin.foldAll
        (fun i x =>
          ((x.fst &&& ~~~bitmask (OfNat.ofNat ↑i)) + (x.fst &&& bitmask (OfNat.ofNat ↑i)) >>> x.snd, x.snd <<< 1))
        (x, 1)).fst

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
⊢ (Fin.foldAll
        ((flip fun x mask => ((x.fst &&& ~~~mask) + (x.fst &&& mask) >>> x.snd, x.snd <<< 1)) ∘ fun i =>
          bitmask (OfNat.ofNat ↑i))
        (x, 1)).fst =
    (Fin.foldAll
        (fun i x =>
          ((x.fst &&& ~~~bitmask (OfNat.ofNat ↑i)) + (x.fst &&& bitmask (OfNat.ofNat ↑i)) >>> x.snd, x.snd <<< 1))
        (x, 1)).fst
Tactic:
rfl
State after:
no goals

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
n : Nat
hn : Nat.log2RU (length α) = n
⊢ Nat.fold
      (fun i x =>
        match x with
        | (x, k) => ((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> k, k <<< 1))
      n (x, 1) =
    Nat.fold
      (fun i x =>
        match x with
        | (x, snd) =>
          ((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i),
            1 <<< OfNat.ofNat (i + 1)))
      n (x, 1)
Tactic:
apply Nat.fold_congr
State after:
case zero
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
n : Nat
hn : Nat.log2RU (length α) = n
⊢ (match (x, 1) with
    | (x, k) => ((x &&& ~~~bitmask (OfNat.ofNat 0)) + (x &&& bitmask (OfNat.ofNat 0)) >>> k, k <<< 1)) =
    match (x, 1) with
    | (x, snd) =>
      ((x &&& ~~~bitmask (OfNat.ofNat 0)) + (x &&& bitmask (OfNat.ofNat 0)) >>> (1 <<< OfNat.ofNat 0),
        1 <<< OfNat.ofNat (0 + 1))

case succ
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
n : Nat
hn : Nat.log2RU (length α) = n
⊢ ∀ (i : Nat) (a : α × α),
    i + 1 < n →
      (match
          match a with
          | (x, snd) =>
            ((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i),
              1 <<< OfNat.ofNat (i + 1)) with
        | (x, k) => ((x &&& ~~~bitmask (OfNat.ofNat (i + 1))) + (x &&& bitmask (OfNat.ofNat (i + 1))) >>> k, k <<< 1)) =
        match
          match a with
          | (x, snd) =>
            ((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i),
              1 <<< OfNat.ofNat (i + 1)) with
        | (x, snd) =>
          ((x &&& ~~~bitmask (OfNat.ofNat (i + 1))) +
              (x &&& bitmask (OfNat.ofNat (i + 1))) >>> (1 <<< OfNat.ofNat (i + 1)),
            1 <<< OfNat.ofNat (i + 1 + 1))

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
n : Nat
hn : Nat.log2RU (length α) = n
⊢ (match (x, 1) with
    | (x, k) => ((x &&& ~~~bitmask (OfNat.ofNat 0)) + (x &&& bitmask (OfNat.ofNat 0)) >>> k, k <<< 1)) =
    match (x, 1) with
    | (x, snd) =>
      ((x &&& ~~~bitmask (OfNat.ofNat 0)) + (x &&& bitmask (OfNat.ofNat 0)) >>> (1 <<< OfNat.ofNat 0),
        1 <<< OfNat.ofNat (0 + 1))
Tactic:
case zero => dsimp; rw [UInt.shiftLeft_zero]
State after:
no goals

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
n : Nat
hn : Nat.log2RU (length α) = n
⊢ ∀ (i : Nat) (a : α × α),
    i + 1 < n →
      (match
          match a with
          | (x, snd) =>
            ((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i),
              1 <<< OfNat.ofNat (i + 1)) with
        | (x, k) => ((x &&& ~~~bitmask (OfNat.ofNat (i + 1))) + (x &&& bitmask (OfNat.ofNat (i + 1))) >>> k, k <<< 1)) =
        match
          match a with
          | (x, snd) =>
            ((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i),
              1 <<< OfNat.ofNat (i + 1)) with
        | (x, snd) =>
          ((x &&& ~~~bitmask (OfNat.ofNat (i + 1))) +
              (x &&& bitmask (OfNat.ofNat (i + 1))) >>> (1 <<< OfNat.ofNat (i + 1)),
            1 <<< OfNat.ofNat (i + 1 + 1))
Tactic:
case succ =>
  intro i a h; cases a with | mk x k =>
  dsimp
  apply congrArg (Prod.mk _)
  rw [UInt.shiftLeft_shiftLeft 1 (OfNat.ofNat (i+1)) 1, UInt.ofNat_add]
  . simp only [UInt.toNat_ofNat, UInt.toNat_ofNat 1]
    have : length α > 0 :=
      hn |> (length α).rec (λ (hn : 0 = n) => nomatch (trans h hn.symm)) (λ l _ _ => l.zero_lt_succ)
    have : n < length α := hn ▸ Nat.log2RU_lt_self _ ‹length α > 0›
    have : n < 2^length α := trans this (Nat.exp_lt_pow (length α) .refl)
    rw [
        Nat.mod_eq_of_lt (trans h this),
        Nat.mod_eq_of_lt (trans (trans (Nat.le_add_left 1 i) h) this)
    ]
    exact trans (r:=LE.le) (h : i+2 ≤ n) ‹n < length α›
State after:
no goals

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
n : Nat
hn : Nat.log2RU (length α) = n
⊢ (match (x, 1) with
    | (x, k) => ((x &&& ~~~bitmask (OfNat.ofNat 0)) + (x &&& bitmask (OfNat.ofNat 0)) >>> k, k <<< 1)) =
    match (x, 1) with
    | (x, snd) =>
      ((x &&& ~~~bitmask (OfNat.ofNat 0)) + (x &&& bitmask (OfNat.ofNat 0)) >>> (1 <<< OfNat.ofNat 0),
        1 <<< OfNat.ofNat (0 + 1))
Tactic:
dsimp
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
n : Nat
hn : Nat.log2RU (length α) = n
⊢ ((x &&& ~~~bitmask (OfNat.ofNat 0)) + (x &&& bitmask (OfNat.ofNat 0)) >>> 1, 1 <<< 1) =
    ((x &&& ~~~bitmask (OfNat.ofNat 0)) + (x &&& bitmask (OfNat.ofNat 0)) >>> (1 <<< OfNat.ofNat 0),
      1 <<< OfNat.ofNat (0 + 1))

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
n : Nat
hn : Nat.log2RU (length α) = n
⊢ ((x &&& ~~~bitmask (OfNat.ofNat 0)) + (x &&& bitmask (OfNat.ofNat 0)) >>> 1, 1 <<< 1) =
    ((x &&& ~~~bitmask (OfNat.ofNat 0)) + (x &&& bitmask (OfNat.ofNat 0)) >>> (1 <<< OfNat.ofNat 0),
      1 <<< OfNat.ofNat (0 + 1))
Tactic:
rw [UInt.shiftLeft_zero]
State after:
no goals

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
n : Nat
hn : Nat.log2RU (length α) = n
⊢ ∀ (i : Nat) (a : α × α),
    i + 1 < n →
      (match
          match a with
          | (x, snd) =>
            ((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i),
              1 <<< OfNat.ofNat (i + 1)) with
        | (x, k) => ((x &&& ~~~bitmask (OfNat.ofNat (i + 1))) + (x &&& bitmask (OfNat.ofNat (i + 1))) >>> k, k <<< 1)) =
        match
          match a with
          | (x, snd) =>
            ((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i),
              1 <<< OfNat.ofNat (i + 1)) with
        | (x, snd) =>
          ((x &&& ~~~bitmask (OfNat.ofNat (i + 1))) +
              (x &&& bitmask (OfNat.ofNat (i + 1))) >>> (1 <<< OfNat.ofNat (i + 1)),
            1 <<< OfNat.ofNat (i + 1 + 1))
Tactic:
intro i a h
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
n : Nat
hn : Nat.log2RU (length α) = n
i : Nat
a : α × α
h : i + 1 < n
⊢ (match
      match a with
      | (x, snd) =>
        ((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i),
          1 <<< OfNat.ofNat (i + 1)) with
    | (x, k) => ((x &&& ~~~bitmask (OfNat.ofNat (i + 1))) + (x &&& bitmask (OfNat.ofNat (i + 1))) >>> k, k <<< 1)) =
    match
      match a with
      | (x, snd) =>
        ((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i),
          1 <<< OfNat.ofNat (i + 1)) with
    | (x, snd) =>
      ((x &&& ~~~bitmask (OfNat.ofNat (i + 1))) + (x &&& bitmask (OfNat.ofNat (i + 1))) >>> (1 <<< OfNat.ofNat (i + 1)),
        1 <<< OfNat.ofNat (i + 1 + 1))

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
n : Nat
hn : Nat.log2RU (length α) = n
i : Nat
a : α × α
h : i + 1 < n
⊢ (match
      match a with
      | (x, snd) =>
        ((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i),
          1 <<< OfNat.ofNat (i + 1)) with
    | (x, k) => ((x &&& ~~~bitmask (OfNat.ofNat (i + 1))) + (x &&& bitmask (OfNat.ofNat (i + 1))) >>> k, k <<< 1)) =
    match
      match a with
      | (x, snd) =>
        ((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i),
          1 <<< OfNat.ofNat (i + 1)) with
    | (x, snd) =>
      ((x &&& ~~~bitmask (OfNat.ofNat (i + 1))) + (x &&& bitmask (OfNat.ofNat (i + 1))) >>> (1 <<< OfNat.ofNat (i + 1)),
        1 <<< OfNat.ofNat (i + 1 + 1))
Tactic:
cases a with | mk x k =>
dsimp
apply congrArg (Prod.mk _)
rw [UInt.shiftLeft_shiftLeft 1 (OfNat.ofNat (i+1)) 1, UInt.ofNat_add]
. simp only [UInt.toNat_ofNat, UInt.toNat_ofNat 1]
have : length α > 0 :=
hn |> (length α).rec (λ (hn : 0 = n) => nomatch (trans h hn.symm)) (λ l _ _ => l.zero_lt_succ)
have : n < length α := hn ▸ Nat.log2RU_lt_self _ ‹length α > 0›
have : n < 2^length α := trans this (Nat.exp_lt_pow (length α) .refl)
rw [
Nat.mod_eq_of_lt (trans h this),
Nat.mod_eq_of_lt (trans (trans (Nat.le_add_left 1 i) h) this)
]
exact trans (r:=LE.le) (h : i+2 ≤ n) ‹n < length α›
State after:
no goals

State before:
case mk
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x✝ : α
n : Nat
hn : Nat.log2RU (length α) = n
i : Nat
h : i + 1 < n
x k : α
⊢ (match
      match (x, k) with
      | (x, snd) =>
        ((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i),
          1 <<< OfNat.ofNat (i + 1)) with
    | (x, k) => ((x &&& ~~~bitmask (OfNat.ofNat (i + 1))) + (x &&& bitmask (OfNat.ofNat (i + 1))) >>> k, k <<< 1)) =
    match
      match (x, k) with
      | (x, snd) =>
        ((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i),
          1 <<< OfNat.ofNat (i + 1)) with
    | (x, snd) =>
      ((x &&& ~~~bitmask (OfNat.ofNat (i + 1))) + (x &&& bitmask (OfNat.ofNat (i + 1))) >>> (1 <<< OfNat.ofNat (i + 1)),
        1 <<< OfNat.ofNat (i + 1 + 1))
Tactic:
dsimp
State after:
case mk
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x✝ : α
n : Nat
hn : Nat.log2RU (length α) = n
i : Nat
h : i + 1 < n
x k : α
⊢ (((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i) &&&
          ~~~bitmask (OfNat.ofNat (i + 1))) +
        ((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i) &&&
            bitmask (OfNat.ofNat (i + 1))) >>>
          (1 <<< OfNat.ofNat (i + 1)),
      1 <<< OfNat.ofNat (i + 1) <<< 1) =
    (((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i) &&&
          ~~~bitmask (OfNat.ofNat (i + 1))) +
        ((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i) &&&
            bitmask (OfNat.ofNat (i + 1))) >>>
          (1 <<< OfNat.ofNat (i + 1)),
      1 <<< OfNat.ofNat (i + 1 + 1))

State before:
case mk
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x✝ : α
n : Nat
hn : Nat.log2RU (length α) = n
i : Nat
h : i + 1 < n
x k : α
⊢ (((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i) &&&
          ~~~bitmask (OfNat.ofNat (i + 1))) +
        ((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i) &&&
            bitmask (OfNat.ofNat (i + 1))) >>>
          (1 <<< OfNat.ofNat (i + 1)),
      1 <<< OfNat.ofNat (i + 1) <<< 1) =
    (((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i) &&&
          ~~~bitmask (OfNat.ofNat (i + 1))) +
        ((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i) &&&
            bitmask (OfNat.ofNat (i + 1))) >>>
          (1 <<< OfNat.ofNat (i + 1)),
      1 <<< OfNat.ofNat (i + 1 + 1))
Tactic:
apply congrArg (Prod.mk _)
State after:
case mk
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x✝ : α
n : Nat
hn : Nat.log2RU (length α) = n
i : Nat
h : i + 1 < n
x k : α
⊢ 1 <<< OfNat.ofNat (i + 1) <<< 1 = 1 <<< OfNat.ofNat (i + 1 + 1)

State before:
case mk
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x✝ : α
n : Nat
hn : Nat.log2RU (length α) = n
i : Nat
h : i + 1 < n
x k : α
⊢ 1 <<< OfNat.ofNat (i + 1) <<< 1 = 1 <<< OfNat.ofNat (i + 1 + 1)
Tactic:
rw [UInt.shiftLeft_shiftLeft 1 (OfNat.ofNat (i+1)) 1, UInt.ofNat_add]
State after:
case mk
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x✝ : α
n : Nat
hn : Nat.log2RU (length α) = n
i : Nat
h : i + 1 < n
x k : α
⊢ toNat (OfNat.ofNat (i + 1)) + toNat 1 < length α

State before:
case mk
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x✝ : α
n : Nat
hn : Nat.log2RU (length α) = n
i : Nat
h : i + 1 < n
x k : α
⊢ toNat (OfNat.ofNat (i + 1)) + toNat 1 < length α
Tactic:
. simp only [UInt.toNat_ofNat, UInt.toNat_ofNat 1]
  have : length α > 0 :=
    hn |> (length α).rec (λ (hn : 0 = n) => nomatch (trans h hn.symm)) (λ l _ _ => l.zero_lt_succ)
  have : n < length α := hn ▸ Nat.log2RU_lt_self _ ‹length α > 0›
  have : n < 2^length α := trans this (Nat.exp_lt_pow (length α) .refl)
  rw [
      Nat.mod_eq_of_lt (trans h this),
      Nat.mod_eq_of_lt (trans (trans (Nat.le_add_left 1 i) h) this)
  ]
  exact trans (r:=LE.le) (h : i+2 ≤ n) ‹n < length α›
State after:
no goals

State before:
case mk
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x✝ : α
n : Nat
hn : Nat.log2RU (length α) = n
i : Nat
h : i + 1 < n
x k : α
⊢ toNat (OfNat.ofNat (i + 1)) + toNat 1 < length α
Tactic:
simp only [UInt.toNat_ofNat, UInt.toNat_ofNat 1]
State after:
case mk
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x✝ : α
n : Nat
hn : Nat.log2RU (length α) = n
i : Nat
h : i + 1 < n
x k : α
⊢ (i + 1) % 2 ^ length α + 1 % 2 ^ length α < length α

State before:
case mk
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x✝ : α
n : Nat
hn : Nat.log2RU (length α) = n
i : Nat
h : i + 1 < n
x k : α
⊢ (i + 1) % 2 ^ length α + 1 % 2 ^ length α < length α
Tactic:
have : length α > 0 :=
  hn |> (length α).rec (λ (hn : 0 = n) => nomatch (trans h hn.symm)) (λ l _ _ => l.zero_lt_succ)
State after:
case mk
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x✝ : α
n : Nat
hn : Nat.log2RU (length α) = n
i : Nat
h : i + 1 < n
x k : α
this : length α > 0
⊢ (i + 1) % 2 ^ length α + 1 % 2 ^ length α < length α

State before:
case mk
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x✝ : α
n : Nat
hn : Nat.log2RU (length α) = n
i : Nat
h : i + 1 < n
x k : α
this : length α > 0
⊢ (i + 1) % 2 ^ length α + 1 % 2 ^ length α < length α
Tactic:
have : n < length α := hn ▸ Nat.log2RU_lt_self _ ‹length α > 0›
State after:
case mk
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x✝ : α
n : Nat
hn : Nat.log2RU (length α) = n
i : Nat
h : i + 1 < n
x k : α
this✝ : length α > 0
this : n < length α
⊢ (i + 1) % 2 ^ length α + 1 % 2 ^ length α < length α

State before:
case mk
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x✝ : α
n : Nat
hn : Nat.log2RU (length α) = n
i : Nat
h : i + 1 < n
x k : α
this✝ : length α > 0
this : n < length α
⊢ (i + 1) % 2 ^ length α + 1 % 2 ^ length α < length α
Tactic:
have : n < 2^length α := trans this (Nat.exp_lt_pow (length α) .refl)
State after:
case mk
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x✝ : α
n : Nat
hn : Nat.log2RU (length α) = n
i : Nat
h : i + 1 < n
x k : α
this✝¹ : length α > 0
this✝ : n < length α
this : n < 2 ^ length α
⊢ (i + 1) % 2 ^ length α + 1 % 2 ^ length α < length α

State before:
case mk
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x✝ : α
n : Nat
hn : Nat.log2RU (length α) = n
i : Nat
h : i + 1 < n
x k : α
this✝¹ : length α > 0
this✝ : n < length α
this : n < 2 ^ length α
⊢ (i + 1) % 2 ^ length α + 1 % 2 ^ length α < length α
Tactic:
rw [
    Nat.mod_eq_of_lt (trans h this),
    Nat.mod_eq_of_lt (trans (trans (Nat.le_add_left 1 i) h) this)
]
State after:
case mk
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x✝ : α
n : Nat
hn : Nat.log2RU (length α) = n
i : Nat
h : i + 1 < n
x k : α
this✝¹ : length α > 0
this✝ : n < length α
this : n < 2 ^ length α
⊢ i + 1 + 1 < length α

State before:
case mk
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x✝ : α
n : Nat
hn : Nat.log2RU (length α) = n
i : Nat
h : i + 1 < n
x k : α
this✝¹ : length α > 0
this✝ : n < length α
this : n < 2 ^ length α
⊢ i + 1 + 1 < length α
Tactic:
exact trans (r:=LE.le) (h : i+2 ≤ n) ‹n < length α›
State after:
no goals

State before:
case h.mk
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x✝ : α
n : Nat
hn : Nat.log2RU (length α) = n
i : Nat
a✝ : i < n
x k : α
⊢ ((x, k).fst &&& ~~~bitmask (OfNat.ofNat i)) + ((x, k).fst &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i) =
    (match (x, k) with
      | (x, snd) =>
        ((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i),
          1 <<< OfNat.ofNat (i + 1))).fst
Tactic:
rfl
State after:
no goals