internlm/Lean-Github huggingface dataset:
Theorem: UInt.bitcnt_eq
Proof 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 α›
Proof 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
Theorem: UInt.bitcnt_eq
Proof 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]
Proof 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
Theorem: UInt.bitcnt_eq
Proof 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
Proof 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
Theorem: UInt.bitcnt_eq
Proof 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
Proof 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
Theorem: UInt.bitcnt_eq
Proof 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)
Proof 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
Theorem: UInt.bitcnt_eq
Proof 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 _
Proof 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
Theorem: UInt.bitcnt_eq
Proof 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
Proof state after:
no goals
Theorem: UInt.bitcnt_eq
Proof 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
Proof 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
Theorem: UInt.bitcnt_eq
Proof 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
Proof 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
Theorem: UInt.bitcnt_eq
Proof 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]
Proof 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
Theorem: UInt.bitcnt_eq
Proof 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
Proof state after:
no goals
Theorem: UInt.bitcnt_eq
Proof 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
Proof 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))
Theorem: UInt.bitcnt_eq
Proof 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]
Proof state after:
no goals
Theorem: UInt.bitcnt_eq
Proof 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 α›
Proof state after:
no goals
Theorem: UInt.bitcnt_eq
Proof 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
Proof 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))
Theorem: UInt.bitcnt_eq
Proof 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]
Proof state after:
no goals
Theorem: UInt.bitcnt_eq
Proof 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
Proof 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))
Theorem: UInt.bitcnt_eq
Proof 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 α›
Proof state after:
no goals
Theorem: UInt.bitcnt_eq
Proof 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
Proof 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))
Theorem: UInt.bitcnt_eq
Proof 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 _)
Proof 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)