internlm/Lean-Github huggingface dataset:
Theorem: fastCycleMin_eq_min_cycleAtTo
Proof state before:
case succ.refine'_4
α : Type u
inst✝² : DecidableEq α
π : Perm α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
i : ℕ
hi : ∀ {x : α}, FastCycleMin i π x = (CycleAtTo π (2 ^ i) x).min' ⋯
x : α
b : ℕ
hb : b < 2 ^ i
⊢ (π ^ (b + 2 ^ i)) x ∈ CycleAtTo π (2 ^ i + 2 ^ i) x
Tactic:
exact apply_pow_mem_cycleAtTo_of_lt ((add_lt_add_iff_right _).mpr hb)
Proof state after:
no goals
Theorem: cycleMin_eq_fastCycleMin
Proof state before:
α : Type u
inst✝² : DecidableEq α
π : Perm α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
x : α
i : ℕ
h : orderOf (π.cycleOf x) ≤ 2 ^ i
⊢ FastCycleMin i π x = CycleMin π x
Tactic:
rw [fastCycleMin_eq_min_cycleAtTo, cycleMin_eq_min_cycleAtTo_ge h]
Proof state after:
no goals
Theorem: cycleMin_eq_cycleMin_apply
Proof state before:
α : Type u
inst✝² : DecidableEq α
π : Perm α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
x : α
⊢ CycleMin π x = CycleMin π (π x)
Tactic:
simp_rw [cycleMin_def, cycleAt_apply_eq_cycleAt]
Proof state after:
no goals
Theorem: cycleMin_eq_cycleMin_apply_inv
Proof state before:
α : Type u
inst✝² : DecidableEq α
π : Perm α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
x : α
⊢ CycleMin π x = CycleMin π (π⁻¹ x)
Tactic:
rw [cycleMin_eq_cycleMin_apply (x := (π⁻¹ x)), Equiv.Perm.apply_inv_self]
Proof state after:
no goals
Theorem: getBitRes_apply_zero
Proof state before:
a✝ : ℕ
i : Fin (a✝ + 1)
⊢ (getBitRes i) 0 = (false, 0)
Tactic:
ext <;> simp only [getBitRes_apply, finFunctionFinEquiv, Equiv.ofRightInverseOfCardLE_symm_apply,
  Fin.val_zero', Nat.zero_div, Nat.zero_mod, Fin.zero_eta, finTwoEquiv_apply, zero_ne_one,
  decide_False, Equiv.ofRightInverseOfCardLE_apply, Fin.val_zero, zero_mul, Finset.sum_const_zero]
Proof state after:
no goals
Theorem: getBit_apply_zero
Proof state before:
a✝ : ℕ
i : Fin (a✝ + 1)
⊢ getBit i 0 = false
Tactic:
rw [getBit_apply, getBitRes_apply_zero]
Proof state after:
no goals
Theorem: getRes_apply_zero
Proof state before:
a✝ : ℕ
i : Fin (a✝ + 1)
⊢ getRes i 0 = 0
Tactic:
rw [getRes_apply, getBitRes_apply_zero]
Proof state after:
no goals
Theorem: mergeBitRes_apply_false_zero
Proof state before:
a✝ : ℕ
i : Fin (a✝ + 1)
⊢ mergeBitRes i false 0 = 0
Tactic:
rw [mergeBitRes_apply, ← getBitRes_apply_zero (i := i), Equiv.symm_apply_apply]
Proof state after:
no goals
Theorem: getBitRes_apply_two_pow
Proof state before:
m : ℕ
i : Fin (m + 1)
⊢ (getBitRes i) ⟨2 ^ ↑i, ⋯⟩ = (true, 0)
Tactic:
ext
Proof state after:
case a
m : ℕ
i : Fin (m + 1)
⊢ ((getBitRes i) ⟨2 ^ ↑i, ⋯⟩).1 = (true, 0).1

case a.h
m : ℕ
i : Fin (m + 1)
⊢ ↑((getBitRes i) ⟨2 ^ ↑i, ⋯⟩).2 = ↑(true, 0).2
Theorem: getBitRes_apply_two_pow
Proof state before:
case a
m : ℕ
i : Fin (m + 1)
⊢ ((getBitRes i) ⟨2 ^ ↑i, ⋯⟩).1 = (true, 0).1
Tactic:
simp only [getBitRes_apply, finFunctionFinEquiv, Equiv.ofRightInverseOfCardLE_symm_apply,
gt_iff_lt, zero_lt_two, pow_pos, Nat.div_self, Nat.one_mod, Fin.mk_one, finTwoEquiv_apply,
decide_True, Equiv.ofRightInverseOfCardLE_apply]
Proof state after:
no goals
Theorem: getBitRes_apply_two_pow
Proof state before:
case a.h
m : ℕ
i : Fin (m + 1)
⊢ ↑((getBitRes i) ⟨2 ^ ↑i, ⋯⟩).2 = ↑(true, 0).2
Tactic:
simp only [getBitRes_apply, finFunctionFinEquiv_apply_val, finFunctionFinEquiv_symm_apply_val,
Fin.val_zero', Finset.sum_eq_zero_iff, Finset.mem_univ, mul_eq_zero, forall_true_left]
Proof state after:
case a.h
m : ℕ
i : Fin (m + 1)
⊢ ∀ (x : Fin m), 2 ^ ↑i / 2 ^ ↑(i.succAbove x) % 2 = 0 ∨ 2 ^ ↑x = 0
Theorem: getBitRes_apply_two_pow
Proof state before:
case a.h
m : ℕ
i : Fin (m + 1)
⊢ ∀ (x : Fin m), 2 ^ ↑i / 2 ^ ↑(i.succAbove x) % 2 = 0 ∨ 2 ^ ↑x = 0
Tactic:
refine' fun x => Or.inl _
Proof state after:
case a.h
m : ℕ
i : Fin (m + 1)
x : Fin m
⊢ 2 ^ ↑i / 2 ^ ↑(i.succAbove x) % 2 = 0
Theorem: getBitRes_apply_two_pow
Proof state before:
case a.h
m : ℕ
i : Fin (m + 1)
x : Fin m
⊢ 2 ^ ↑i / 2 ^ ↑(i.succAbove x) % 2 = 0
Tactic:
rcases (Fin.succAbove_ne i x).lt_or_lt with h | h <;> rw [Fin.lt_iff_val_lt_val] at h
Proof state after:
case a.h.inl
m : ℕ
i : Fin (m + 1)
x : Fin m
h : ↑(i.succAbove x) < ↑i
⊢ 2 ^ ↑i / 2 ^ ↑(i.succAbove x) % 2 = 0

case a.h.inr
m : ℕ
i : Fin (m + 1)
x : Fin m
h : ↑i < ↑(i.succAbove x)
⊢ 2 ^ ↑i / 2 ^ ↑(i.succAbove x) % 2 = 0
Theorem: getBitRes_apply_two_pow
Proof state before:
case a.h.inl
m : ℕ
i : Fin (m + 1)
x : Fin m
h : ↑(i.succAbove x) < ↑i
⊢ 2 ^ ↑i / 2 ^ ↑(i.succAbove x) % 2 = 0
Tactic:
rw [Nat.pow_div h.le zero_lt_two, Nat.pow_mod, Nat.mod_self,
  Nat.zero_pow (Nat.sub_pos_of_lt h), Nat.zero_mod]
Proof state after:
no goals
Theorem: getBitRes_apply_two_pow
Proof state before:
case a.h.inr
m : ℕ
i : Fin (m + 1)
x : Fin m
h : ↑i < ↑(i.succAbove x)
⊢ 2 ^ ↑i / 2 ^ ↑(i.succAbove x) % 2 = 0
Tactic:
rw [Nat.div_eq_of_lt (pow_lt_pow_right one_lt_two h), Nat.zero_mod]
Proof state after:
no goals
Theorem: getBit_apply_two_pow
Proof state before:
m : ℕ
i : Fin (m + 1)
⊢ getBit i ⟨2 ^ ↑i, ⋯⟩ = true
Tactic:
rw [getBit_apply, getBitRes_apply_two_pow]
Proof state after:
no goals
Theorem: getBit_apply_zero_one
Proof state before:
m : ℕ
⊢ getBit 0 1 = true
Tactic:
convert getBit_apply_two_pow
Proof state after:
case h.e'_2.h.e'_3.h.h.e'_2
m : ℕ
⊢ ↑1 = 2 ^ ↑0
Theorem: getBit_apply_zero_one
Proof state before:
case h.e'_2.h.e'_3.h.h.e'_2
m : ℕ
⊢ ↑1 = 2 ^ ↑0
Tactic:
rw [Fin.val_one', Nat.mod_eq_of_lt (Nat.one_lt_pow' _ _ ), Fin.val_zero, pow_zero]
Proof state after:
no goals
Theorem: getRes_apply_two_pow
Proof state before:
m : ℕ
i : Fin (m + 1)
⊢ getRes i ⟨2 ^ ↑i, ⋯⟩ = 0
Tactic:
rw [getRes_apply, getBitRes_apply_two_pow]
Proof state after:
no goals
Theorem: mergeBitRes_apply_true_zero
Proof state before:
m : ℕ
i : Fin (m + 1)
⊢ mergeBitRes i true 0 = ⟨2 ^ ↑i, ⋯⟩
Tactic:
rw [mergeBitRes_apply, ← getBitRes_apply_two_pow (i := i), Equiv.symm_apply_apply]
Proof state after:
no goals
Theorem: mergeBitRes_apply'
Proof state before:
m : ℕ
i : Fin (m + 1)
b : Bool
p : BV m
⊢ mergeBitRes i b p =
    ∑ i' : Fin (m + 1), i.insertNth (bif b then 1 else 0) (fun b => Fin.castLE ⋯ p / 2 ^ ↑b % 2) i' * 2 ^ ↑i'
Tactic:
unfold mergeBitRes getBitRes
Proof state after:
m : ℕ
i : Fin (m + 1)
b : Bool
p : BV m
⊢ Function.curry
      (⇑(Trans.trans (Trans.trans finFunctionFinEquiv.symm (Equiv.piFinSuccAbove (fun a => Fin 2) i))
            (finTwoEquiv.prodCongr finFunctionFinEquiv)).symm)
      b p =
    ∑ i' : Fin (m + 1), i.insertNth (bif b then 1 else 0) (fun b => Fin.castLE ⋯ p / 2 ^ ↑b % 2) i' * 2 ^ ↑i'
Theorem: mergeBitRes_apply'
Proof state before:
m : ℕ
i : Fin (m + 1)
b : Bool
p : BV m
⊢ Function.curry
      (⇑(Trans.trans (Trans.trans finFunctionFinEquiv.symm (Equiv.piFinSuccAbove (fun a => Fin 2) i))
            (finTwoEquiv.prodCongr finFunctionFinEquiv)).symm)
      b p =
    ∑ i' : Fin (m + 1), i.insertNth (bif b then 1 else 0) (fun b => Fin.castLE ⋯ p / 2 ^ ↑b % 2) i' * 2 ^ ↑i'
Tactic:
simp [finFunctionFinEquiv]
Proof state after:
m : ℕ
i : Fin (m + 1)
b : Bool
p : BV m
⊢ ⟨∑ i_1 : Fin (m + 1), ↑(i.insertNth (bif b then 1 else 0) (fun b => ⟨↑p / 2 ^ ↑b % 2, ⋯⟩) i_1) * 2 ^ ↑i_1, ⋯⟩ =
    ∑ i' : Fin (m + 1), i.insertNth (bif b then 1 else 0) (fun b => Fin.castLE ⋯ p / 2 ^ ↑b % 2) i' * 2 ^ ↑i'
Theorem: mergeBitRes_apply'
Proof state before:
m : ℕ
i : Fin (m + 1)
b : Bool
p : BV m
⊢ ⟨∑ i_1 : Fin (m + 1), ↑(i.insertNth (bif b then 1 else 0) (fun b => ⟨↑p / 2 ^ ↑b % 2, ⋯⟩) i_1) * 2 ^ ↑i_1, ⋯⟩ =
    ∑ i' : Fin (m + 1), i.insertNth (bif b then 1 else 0) (fun b => Fin.castLE ⋯ p / 2 ^ ↑b % 2) i' * 2 ^ ↑i'
Tactic:
norm_cast
Proof state after:
m : ℕ
i : Fin (m + 1)
b : Bool
p : BV m
⊢ ⟨∑ x : Fin (m + 1), ↑(i.insertNth (bif b then 1 else 0) (fun b => ⟨↑p / 2 ^ ↑b % 2, ⋯⟩) x) * 2 ^ ↑x, ⋯⟩ =
    ∑ x : Fin (m + 1), i.insertNth (bif b then 1 else 0) (fun b => Fin.castLE ⋯ p / ↑(2 ^ ↑b) % 2) x * ↑(2 ^ ↑x)
Theorem: mergeBitRes_apply'
Proof state before:
m : ℕ
i : Fin (m + 1)
b : Bool
p : BV m
⊢ ⟨∑ x : Fin (m + 1), ↑(i.insertNth (bif b then 1 else 0) (fun b => ⟨↑p / 2 ^ ↑b % 2, ⋯⟩) x) * 2 ^ ↑x, ⋯⟩ =
    ∑ x : Fin (m + 1), i.insertNth (bif b then 1 else 0) (fun b => Fin.castLE ⋯ p / ↑(2 ^ ↑b) % 2) x * ↑(2 ^ ↑x)
Tactic:
ext
Proof state after:
case h
m : ℕ
i : Fin (m + 1)
b : Bool
p : BV m
⊢ ↑⟨∑ x : Fin (m + 1), ↑(i.insertNth (bif b then 1 else 0) (fun b => ⟨↑p / 2 ^ ↑b % 2, ⋯⟩) x) * 2 ^ ↑x, ⋯⟩ =
    ↑(∑ x : Fin (m + 1), i.insertNth (bif b then 1 else 0) (fun b => Fin.castLE ⋯ p / ↑(2 ^ ↑b) % 2) x * ↑(2 ^ ↑x))
Theorem: mergeBitRes_apply'
Proof state before:
case h
m : ℕ
i : Fin (m + 1)
b : Bool
p : BV m
⊢ ↑⟨∑ x : Fin (m + 1), ↑(i.insertNth (bif b then 1 else 0) (fun b => ⟨↑p / 2 ^ ↑b % 2, ⋯⟩) x) * 2 ^ ↑x, ⋯⟩ =
    ↑(∑ x : Fin (m + 1), i.insertNth (bif b then 1 else 0) (fun b => Fin.castLE ⋯ p / ↑(2 ^ ↑b) % 2) x * ↑(2 ^ ↑x))
Tactic:
simp
Proof state after:
case h
m : ℕ
i : Fin (m + 1)
b : Bool
p : BV m
⊢ ∑ x : Fin (m + 1), ↑(i.insertNth (bif b then 1 else 0) (fun b => ⟨↑p / 2 ^ ↑b % 2, ⋯⟩) x) * 2 ^ ↑x =
    ↑(∑ x : Fin (m + 1), i.insertNth (bif b then 1 else 0) (fun b => Fin.castLE ⋯ p / 2 ^ ↑b % 2) x * 2 ^ ↑x)
Theorem: mergeBitRes_apply'
Proof state before:
case h
m : ℕ
i : Fin (m + 1)
b : Bool
p : BV m
⊢ ∑ x : Fin (m + 1), ↑(i.insertNth (bif b then 1 else 0) (fun b => ⟨↑p / 2 ^ ↑b % 2, ⋯⟩) x) * 2 ^ ↑x =
    ↑(∑ x : Fin (m + 1), i.insertNth (bif b then 1 else 0) (fun b => Fin.castLE ⋯ p / 2 ^ ↑b % 2) x * 2 ^ ↑x)
Tactic:
norm_cast
Proof state after:
case h
m : ℕ
i : Fin (m + 1)
b : Bool
p : BV m
⊢ ∑ x : Fin (m + 1), ↑(i.insertNth (bif b then 1 else 0) (fun b => ⟨↑p / 2 ^ ↑b % 2, ⋯⟩) x) * 2 ^ ↑x =
    ↑(∑ x : Fin (m + 1), i.insertNth (bif b then 1 else 0) (fun b => Fin.castLE ⋯ p / ↑(2 ^ ↑b) % 2) x * ↑(2 ^ ↑x))
Theorem: mergeBitRes_apply_true_eq_apply_false_add_apply_true_zero
Proof state before:
m : ℕ
p : BV m
i : Fin (m + 1)
⊢ mergeBitRes i true p = mergeBitRes i false p + mergeBitRes i true 0
Tactic:
unfold mergeBitRes getBitRes
Proof state after:
m : ℕ
p : BV m
i : Fin (m + 1)
⊢ Function.curry
      (⇑(Trans.trans (Trans.trans finFunctionFinEquiv.symm (Equiv.piFinSuccAbove (fun a => Fin 2) i))
            (finTwoEquiv.prodCongr finFunctionFinEquiv)).symm)
      true p =
    Function.curry
        (⇑(Trans.trans (Trans.trans finFunctionFinEquiv.symm (Equiv.piFinSuccAbove (fun a => Fin 2) i))
              (finTwoEquiv.prodCongr finFunctionFinEquiv)).symm)
        false p +
      Function.curry
        (⇑(Trans.trans (Trans.trans finFunctionFinEquiv.symm (Equiv.piFinSuccAbove (fun a => Fin 2) i))
              (finTwoEquiv.prodCongr finFunctionFinEquiv)).symm)
        true 0
Theorem: mergeBitRes_apply_true_eq_apply_false_add_apply_true_zero
Proof state before:
m : ℕ
p : BV m
i : Fin (m + 1)
⊢ Function.curry
      (⇑(Trans.trans (Trans.trans finFunctionFinEquiv.symm (Equiv.piFinSuccAbove (fun a => Fin 2) i))
            (finTwoEquiv.prodCongr finFunctionFinEquiv)).symm)
      true p =
    Function.curry
        (⇑(Trans.trans (Trans.trans finFunctionFinEquiv.symm (Equiv.piFinSuccAbove (fun a => Fin 2) i))
              (finTwoEquiv.prodCongr finFunctionFinEquiv)).symm)
        false p +
      Function.curry
        (⇑(Trans.trans (Trans.trans finFunctionFinEquiv.symm (Equiv.piFinSuccAbove (fun a => Fin 2) i))
              (finTwoEquiv.prodCongr finFunctionFinEquiv)).symm)
        true 0
Tactic:
simp [finFunctionFinEquiv]
Proof state after:
m : ℕ
p : BV m
i : Fin (m + 1)
⊢ ⟨∑ i_1 : Fin (m + 1), ↑(i.insertNth 1 (fun b => ⟨↑p / 2 ^ ↑b % 2, ⋯⟩) i_1) * 2 ^ ↑i_1, ⋯⟩ =
    ⟨∑ i_1 : Fin (m + 1), ↑(i.insertNth 0 (fun b => ⟨↑p / 2 ^ ↑b % 2, ⋯⟩) i_1) * 2 ^ ↑i_1, ⋯⟩ +
      ⟨∑ i_1 : Fin (m + 1), ↑(i.insertNth 1 (fun b => 0) i_1) * 2 ^ ↑i_1, ⋯⟩
Theorem: mergeBitRes_apply_true_eq_apply_false_add_apply_true_zero
Proof state before:
m : ℕ
p : BV m
i : Fin (m + 1)
⊢ ⟨∑ i_1 : Fin (m + 1), ↑(i.insertNth 1 (fun b => ⟨↑p / 2 ^ ↑b % 2, ⋯⟩) i_1) * 2 ^ ↑i_1, ⋯⟩ =
    ⟨∑ i_1 : Fin (m + 1), ↑(i.insertNth 0 (fun b => ⟨↑p / 2 ^ ↑b % 2, ⋯⟩) i_1) * 2 ^ ↑i_1, ⋯⟩ +
      ⟨∑ i_1 : Fin (m + 1), ↑(i.insertNth 1 (fun b => 0) i_1) * 2 ^ ↑i_1, ⋯⟩
Tactic:
norm_cast
Proof state after:
m : ℕ
p : BV m
i : Fin (m + 1)
⊢ ⟨∑ x : Fin (m + 1), ↑(i.insertNth 1 (fun b => ⟨↑p / 2 ^ ↑b % 2, ⋯⟩) x) * 2 ^ ↑x, ⋯⟩ =
    ⟨∑ x : Fin (m + 1), ↑(i.insertNth 0 (fun b => ⟨↑p / 2 ^ ↑b % 2, ⋯⟩) x) * 2 ^ ↑x, ⋯⟩ +
      ⟨∑ x : Fin (m + 1), ↑(i.insertNth 1 (fun b => 0) x) * 2 ^ ↑x, ⋯⟩
Theorem: mergeBitRes_apply_true_eq_apply_false_add_apply_true_zero
Proof state before:
m : ℕ
p : BV m
i : Fin (m + 1)
⊢ ⟨∑ x : Fin (m + 1), ↑(i.insertNth 1 (fun b => ⟨↑p / 2 ^ ↑b % 2, ⋯⟩) x) * 2 ^ ↑x, ⋯⟩ =
    ⟨∑ x : Fin (m + 1), ↑(i.insertNth 0 (fun b => ⟨↑p / 2 ^ ↑b % 2, ⋯⟩) x) * 2 ^ ↑x, ⋯⟩ +
      ⟨∑ x : Fin (m + 1), ↑(i.insertNth 1 (fun b => 0) x) * 2 ^ ↑x, ⋯⟩
Tactic:
simp_rw [Fin.add_def]
Proof state after:
m : ℕ
p : BV m
i : Fin (m + 1)
⊢ ⟨∑ x : Fin (m + 1), ↑(i.insertNth 1 (fun b => ⟨↑p / 2 ^ ↑b % 2, ⋯⟩) x) * 2 ^ ↑x, ⋯⟩ =
    ⟨(∑ x : Fin (m + 1), ↑(i.insertNth 0 (fun b => ⟨↑p / 2 ^ ↑b % 2, ⋯⟩) x) * 2 ^ ↑x +
          ∑ x : Fin (m + 1), ↑(i.insertNth 1 (fun b => 0) x) * 2 ^ ↑x) %
        2 ^ (m + 1),
      ⋯⟩
Theorem: mergeBitRes_apply_true_eq_apply_false_add_apply_true_zero
Proof state before:
m : ℕ
p : BV m
i : Fin (m + 1)
⊢ ⟨∑ x : Fin (m + 1), ↑(i.insertNth 1 (fun b => ⟨↑p / 2 ^ ↑b % 2, ⋯⟩) x) * 2 ^ ↑x, ⋯⟩ =
    ⟨(∑ x : Fin (m + 1), ↑(i.insertNth 0 (fun b => ⟨↑p / 2 ^ ↑b % 2, ⋯⟩) x) * 2 ^ ↑x +
          ∑ x : Fin (m + 1), ↑(i.insertNth 1 (fun b => 0) x) * 2 ^ ↑x) %
        2 ^ (m + 1),
      ⋯⟩
Tactic:
ext : 1
Proof state after:
case h
m : ℕ
p : BV m
i : Fin (m + 1)
⊢ ↑⟨∑ x : Fin (m + 1), ↑(i.insertNth 1 (fun b => ⟨↑p / 2 ^ ↑b % 2, ⋯⟩) x) * 2 ^ ↑x, ⋯⟩ =
    ↑⟨(∑ x : Fin (m + 1), ↑(i.insertNth 0 (fun b => ⟨↑p / 2 ^ ↑b % 2, ⋯⟩) x) * 2 ^ ↑x +
            ∑ x : Fin (m + 1), ↑(i.insertNth 1 (fun b => 0) x) * 2 ^ ↑x) %
          2 ^ (m + 1),
        ⋯⟩
Theorem: mergeBitRes_apply_true_eq_apply_false_add_apply_true_zero
Proof state before:
case h
m : ℕ
p : BV m
i : Fin (m + 1)
⊢ ↑⟨∑ x : Fin (m + 1), ↑(i.insertNth 1 (fun b => ⟨↑p / 2 ^ ↑b % 2, ⋯⟩) x) * 2 ^ ↑x, ⋯⟩ =
    ↑⟨(∑ x : Fin (m + 1), ↑(i.insertNth 0 (fun b => ⟨↑p / 2 ^ ↑b % 2, ⋯⟩) x) * 2 ^ ↑x +
            ∑ x : Fin (m + 1), ↑(i.insertNth 1 (fun b => 0) x) * 2 ^ ↑x) %
          2 ^ (m + 1),
        ⋯⟩
Tactic:
simp
Proof state after:
case h
m : ℕ
p : BV m
i : Fin (m + 1)
⊢ ∑ x : Fin (m + 1), ↑(i.insertNth 1 (fun b => ⟨↑p / 2 ^ ↑b % 2, ⋯⟩) x) * 2 ^ ↑x =
    (∑ x : Fin (m + 1), ↑(i.insertNth 0 (fun b => ⟨↑p / 2 ^ ↑b % 2, ⋯⟩) x) * 2 ^ ↑x +
        ∑ x : Fin (m + 1), ↑(i.insertNth 1 (fun b => 0) x) * 2 ^ ↑x) %
      2 ^ (m + 1)
Theorem: mergeBitRes_apply_true_eq_apply_false_add_apply_true_zero
Proof state before:
case h
m : ℕ
p : BV m
i : Fin (m + 1)
⊢ ∑ x : Fin (m + 1), ↑(i.insertNth 1 (fun b => ⟨↑p / 2 ^ ↑b % 2, ⋯⟩) x) * 2 ^ ↑x =
    (∑ x : Fin (m + 1), ↑(i.insertNth 0 (fun b => ⟨↑p / 2 ^ ↑b % 2, ⋯⟩) x) * 2 ^ ↑x +
        ∑ x : Fin (m + 1), ↑(i.insertNth 1 (fun b => 0) x) * 2 ^ ↑x) %
      2 ^ (m + 1)
Tactic:
rw [← Finset.sum_add_distrib, Finset.sum_nat_mod, Finset.sum_congr]
Proof state after:
case h
m : ℕ
p : BV m
i : Fin (m + 1)
⊢ ?m.88623.sum ?m.88625 =
    (∑ i_1 : Fin (m + 1),
        (↑(i.insertNth 0 (fun b => ⟨↑p / 2 ^ ↑b % 2, ⋯⟩) i_1) * 2 ^ ↑i_1 +
            ↑(i.insertNth 1 (fun b => 0) i_1) * 2 ^ ↑i_1) %
          2 ^ (m + 1)) %
      2 ^ (m + 1)

case h.h
m : ℕ
p : BV m
i : Fin (m + 1)
⊢ Finset.univ = ?m.88623

case h.a
m : ℕ
p : BV m
i : Fin (m + 1)
⊢ ∀ x ∈ ?m.88623, ↑(i.insertNth 1 (fun b => ⟨↑p / 2 ^ ↑b % 2, ⋯⟩) x) * 2 ^ ↑x = ?m.88625 x

m : ℕ
p : BV m
i : Fin (m + 1)
⊢ Finset (Fin (m + 1))

m : ℕ
p : BV m
i : Fin (m + 1)
⊢ Fin (m + 1) → ℕ
Theorem: getBitResZero_symm_apply
Proof state before:
b : Bool
a✝ : ℕ
p : BV a✝
⊢ getBitResZero.symm (b, p) = finProdFinEquiv (p, bif b then 1 else 0)
Tactic:
cases b <;> rfl
Proof state after:
no goals
Theorem: getBitRes_zero
Proof state before:
m : ℕ
⊢ getBitRes 0 = getBitResZero
Tactic:
ext q : 1
Proof state after:
case H
m : ℕ
q : BV (m + 1)
⊢ (getBitRes 0) q = getBitResZero q
Theorem: getBitRes_zero
Proof state before:
case H
m : ℕ
q : BV (m + 1)
⊢ (getBitRes 0) q = getBitResZero q
Tactic:
simp_rw [getBitRes_apply, getBitResZero_apply, Fin.zero_succAbove, finFunctionFinEquiv,
  Equiv.ofRightInverseOfCardLE_symm_apply, Fin.val_zero, pow_zero, Nat.div_one,
  finTwoEquiv_apply, Fin.val_succ, Equiv.ofRightInverseOfCardLE_apply,
  Nat.pow_eq, Prod.mk.injEq, decide_eq_decide, Fin.ext_iff, Fin.val_one, Fin.coe_modNat,
  Finset.sum_fin_eq_sum_range, dite_eq_ite, Fin.coe_divNat, true_and]
Proof state after:
case H
m : ℕ
q : BV (m + 1)
⊢ (∑ x ∈ Finset.range m, if x < m then ↑q / 2 ^ (x + 1) % 2 * 2 ^ x else 0) = ↑q / 2
Theorem: getBitRes_zero
Proof state before:
case H
m : ℕ
q : BV (m + 1)
⊢ (∑ x ∈ Finset.range m, if x < m then ↑q / 2 ^ (x + 1) % 2 * 2 ^ x else 0) = ↑q / 2
Tactic:
rw [Finset.sum_ite_of_true (h := fun _ H => (Finset.mem_range.mp H))]
Proof state after:
case H
m : ℕ
q : BV (m + 1)
⊢ ∑ x ∈ Finset.range m, ↑q / 2 ^ (x + 1) % 2 * 2 ^ x = ↑q / 2
Theorem: getBitRes_zero
Proof state before:
case H
m : ℕ
q : BV (m + 1)
⊢ ∑ x ∈ Finset.range m, ↑q / 2 ^ (x + 1) % 2 * 2 ^ x = ↑q / 2
Tactic:
refine' Nat.eq_of_mul_eq_mul_left (zero_lt_two)
  (add_right_cancel (b := (q : ℕ) / 2 ^ 0 % 2 * 2 ^ 0) _)
Proof state after:
case H
m : ℕ
q : BV (m + 1)
⊢ 2 * ∑ x ∈ Finset.range m, ↑q / 2 ^ (x + 1) % 2 * 2 ^ x + ↑q / 2 ^ 0 % 2 * 2 ^ 0 =
    2 * (↑q / 2) + ↑q / 2 ^ 0 % 2 * 2 ^ 0
Theorem: getBitRes_zero
Proof state before:
case H
m : ℕ
q : BV (m + 1)
⊢ 2 * ∑ x ∈ Finset.range m, ↑q / 2 ^ (x + 1) % 2 * 2 ^ x + ↑q / 2 ^ 0 % 2 * 2 ^ 0 =
    2 * (↑q / 2) + ↑q / 2 ^ 0 % 2 * 2 ^ 0
Tactic:
simp_rw [Finset.mul_sum, mul_left_comm (2 : ℕ), ← Nat.pow_succ', Nat.succ_eq_add_one,
← Finset.sum_range_succ' (fun x => (q : ℕ) / 2 ^ x % 2 * 2 ^ x), pow_zero, Nat.div_one,
  mul_one, Nat.div_add_mod, Finset.sum_range, ← finFunctionFinEquiv_symm_apply_val,
  ← finFunctionFinEquiv_apply_val, Equiv.apply_symm_apply]
Proof state after:
no goals
Theorem: getBitRes_zero_apply
Proof state before:
m : ℕ
q : BV (m + 1)
⊢ (getBitRes 0) q = (finTwoEquiv q.modNat, q.divNat)
Tactic:
simp_rw [getBitRes_zero, getBitResZero_apply]
Proof state after:
no goals
Theorem: getBitRes_zero_symm_apply
Proof state before:
m : ℕ
b : Bool
p : BV m
⊢ (getBitRes 0).symm (b, p) = finProdFinEquiv (p, bif b then 1 else 0)
Tactic:
simp_rw [getBitRes_zero, getBitResZero_symm_apply]
Proof state after:
no goals
Theorem: getBit_zero
Proof state before:
a✝ : ℕ
q : BV (a✝ + 1)
⊢ getBit 0 q = finTwoEquiv q.modNat
Tactic:
simp_rw [getBit_apply, getBitRes_zero_apply]
Proof state after:
no goals
Theorem: getRes_zero
Proof state before:
a✝ : ℕ
q : BV (a✝ + 1)
⊢ getRes 0 q = q.divNat
Tactic:
simp_rw [getRes_apply, getBitRes_zero_apply]
Proof state after:
no goals
Theorem: mergeBitRes_zero
Proof state before:
b : Bool
a✝ : ℕ
p : BV a✝
⊢ mergeBitRes 0 b p = finProdFinEquiv (p, bif b then 1 else 0)
Tactic:
simp_rw [mergeBitRes_apply, getBitRes_zero_symm_apply]
Proof state after:
no goals
Theorem: mergeBitRes_zero_divNat_modNat
Proof state before:
b : Bool
a✝ : ℕ
p : BV a✝
⊢ ((mergeBitRes 0 b p).divNat, (mergeBitRes 0 b p).modNat) = (p, bif b then 1 else 0)
Tactic:
simp_rw [← finProdFinEquiv_symm_apply, Equiv.symm_apply_eq]
Proof state after:
b : Bool
a✝ : ℕ
p : BV a✝
⊢ mergeBitRes 0 b p = finProdFinEquiv (p, bif b then 1 else 0)
Theorem: mergeBitRes_zero_divNat_modNat
Proof state before:
b : Bool
a✝ : ℕ
p : BV a✝
⊢ mergeBitRes 0 b p = finProdFinEquiv (p, bif b then 1 else 0)
Tactic:
exact mergeBitRes_zero
Proof state after:
no goals
Theorem: mergeBitRes_zero_apply_true_zero_eq_one
Proof state before:
m : ℕ
⊢ mergeBitRes 0 true 0 = 1
Tactic:
simp_rw [mergeBitRes_zero, Fin.ext_iff, finProdFinEquiv_apply_val, Fin.val_zero', mul_zero,
add_zero, Bool.cond_true, Fin.val_one, Fin.val_one', ← Nat.pow_succ,
Nat.mod_eq_of_lt (Nat.one_lt_pow' _ _ )]
Proof state after:
no goals
Theorem: mergeBitRes_base_true
Proof state before:
i : Fin (0 + 1)
p : BV 0
⊢ mergeBitRes i true p = 1
Tactic:
rw [Fin.eq_zero p, Fin.eq_zero i]
Proof state after:
i : Fin (0 + 1)
p : BV 0
⊢ mergeBitRes 0 true 0 = 1
Theorem: mergeBitRes_base_true
Proof state before:
i : Fin (0 + 1)
p : BV 0
⊢ mergeBitRes 0 true 0 = 1
Tactic:
exact mergeBitRes_zero_apply_true_zero_eq_one
Proof state after:
no goals
Theorem: mergeBitRes_base_false
Proof state before:
i : Fin (0 + 1)
p : BV 0
⊢ mergeBitRes i false p = 0
Tactic:
rw [Fin.eq_zero p]
Proof state after:
i : Fin (0 + 1)
p : BV 0
⊢ mergeBitRes i false 0 = 0
Theorem: mergeBitRes_base_false
Proof state before:
i : Fin (0 + 1)
p : BV 0
⊢ mergeBitRes i false 0 = 0
Tactic:
exact mergeBitRes_apply_false_zero
Proof state after:
no goals
Theorem: getBit_base
Proof state before:
i : Fin (0 + 1)
q : BV (0 + 1)
⊢ getBit i q = decide (q = 1)
Tactic:
rw [Fin.eq_zero i]
Proof state after:
i : Fin (0 + 1)
q : BV (0 + 1)
⊢ getBit 0 q = decide (q = 1)
Theorem: getBit_base
Proof state before:
i : Fin (0 + 1)
q : BV (0 + 1)
⊢ getBit 0 q = decide (q = 1)
Tactic:
rcases Fin.exists_fin_two.mp ⟨q, rfl⟩ with (rfl | rfl) <;> rfl
Proof state after:
no goals
Theorem: getRes_base
Proof state before:
i : Fin (0 + 1)
q : BV (0 + 1)
⊢ getRes i q = 0
Tactic:
rw [Fin.eq_zero i]
Proof state after:
i : Fin (0 + 1)
q : BV (0 + 1)
⊢ getRes 0 q = 0
Theorem: getRes_base
Proof state before:
i : Fin (0 + 1)
q : BV (0 + 1)
⊢ getRes 0 q = 0
Tactic:
rcases Fin.exists_fin_two.mp ⟨q, rfl⟩ with (rfl | rfl) <;> rfl
Proof state after:
no goals
Theorem: getBitRes_succ
Proof state before:
m : ℕ
i : Fin (m + 1)
⊢ getBitRes i.succ = getBitResSucc i
Tactic:
simp_rw [Equiv.ext_iff, getBitResSucc_apply,
  getBitRes_apply, getBitRes_symm_apply, Equiv.symm_apply_apply,
  Prod.mk.injEq, EmbeddingLike.apply_eq_iff_eq,
  Fin.eq_insertNth_iff, Fin.succAbove_zero, Fin.succ_succAbove_zero,
  Fin.succ_succAbove_succ, true_and, implies_true]
Proof state after:
no goals
Theorem: getBitRes_succ_apply
Proof state before:
m : ℕ
q : BV (m + 1 + 1)
i : Fin (m + 1)
⊢ (getBitRes i.succ) q =
    (((getBitRes i) ((getBitRes 0) q).2).1,
      (getBitRes 0).symm (((getBitRes 0) q).1, ((getBitRes i) ((getBitRes 0) q).2).2))
Tactic:
rw [getBitRes_succ, getBitResSucc_apply]
Proof state after:
no goals
Theorem: getBitRes_succ_symm_apply
Proof state before:
m : ℕ
b : Bool
p : BV (m + 1)
i : Fin (m + 1)
⊢ (getBitRes i.succ).symm (b, p) = (getBitRes 0).symm (((getBitRes 0) p).1, (getBitRes i).symm (b, ((getBitRes 0) p).2))
Tactic:
rw [getBitRes_succ, getBitResSucc_symm_apply]
Proof state after:
no goals
Theorem: getRes_succ
Proof state before:
m : ℕ
q : BV (m + 1 + 1)
i : Fin (m + 1)
⊢ getRes i.succ q = mergeBitRes 0 (getBit 0 q) (getRes i (getRes 0 q))
Tactic:
simp_rw [getRes_apply, mergeBitRes_apply, getBit_apply, getBitRes_succ_apply]
Proof state after:
no goals
Theorem: getBit_succ
Proof state before:
m : ℕ
q : BV (m + 1 + 1)
i : Fin (m + 1)
⊢ getBit i.succ q = getBit i (getRes 0 q)
Tactic:
simp_rw [getRes_apply, getBit_apply, getBitRes_succ_apply]
Proof state after:
no goals
Theorem: mergeBitRes_succ
Proof state before:
m : ℕ
b : Bool
q : BV (m + 1)
i : Fin (m + 1)
⊢ mergeBitRes i.succ b q = mergeBitRes 0 (getBit 0 q) (mergeBitRes i b (getRes 0 q))
Tactic:
simp_rw [mergeBitRes_apply, getBit_apply, getRes_apply, getBitRes_succ_symm_apply]
Proof state after:
no goals
Theorem: getBitResLast_symm_apply
Proof state before:
b : Bool
a✝ : ℕ
p : BV a✝
⊢ getBitResZero.symm (b, p) = finProdFinEquiv (p, bif b then 1 else 0)
Tactic:
cases b <;> rfl
Proof state after:
no goals
Theorem: getBitRes_castSucc
Proof state before:
m : ℕ
i : Fin (m + 1)
⊢ getBitRes i.castSucc = getBitResCastSucc i
Tactic:
simp_rw [Equiv.ext_iff, getBitResCastSucc_apply,
  getBitRes_apply, getBitRes_symm_apply, Equiv.symm_apply_apply,
  Prod.mk.injEq, EmbeddingLike.apply_eq_iff_eq,
  Fin.eq_insertNth_iff, Fin.succAbove_last, Fin.castSucc_succAbove_last,
  Fin.castSucc_succAbove_castSucc, true_and, implies_true]
Proof state after:
no goals
Theorem: getBitRes_castSucc_apply
Proof state before:
m : ℕ
q : BV (m + 1 + 1)
i : Fin (m + 1)
⊢ (getBitRes i.castSucc) q =
    (((getBitRes i) ((getBitRes (Fin.last (m + 1))) q).2).1,
      (getBitRes (Fin.last m)).symm
        (((getBitRes (Fin.last (m + 1))) q).1, ((getBitRes i) ((getBitRes (Fin.last (m + 1))) q).2).2))
Tactic:
rw [getBitRes_castSucc, getBitResCastSucc_apply]
Proof state after:
no goals