-- Mathlib/Data/Nat/BitIndices.lean
theorem bitIndices_twoPowsum {L : List ℕ} (hL : List.Sorted (· < ·) L) :
    (L.map (fun i ↦ 2^i)).sum.bitIndices = L

Proof state:
case cons.intro.intro.intro
a : ℕ
L₀ : List ℕ
hL₀ : Sorted (fun x1 x2 => x1 < x2) L₀
hL✝ : Sorted (fun x1 x2 => x1 < x2) (a :: map (fun x => x + a + 1) L₀)
hL : Sorted (fun x1 x2 => x1 < x2) (map (fun x => x + a + 1) L₀)
haL : ∀ b ∈ map (fun x => x + a + 1) L₀, a + 1 ≤ b
x✝ : L₀.length < (a :: map (fun x => x + a + 1) L₀).length
hrw : ((fun x => 2 ^ x) ∘ fun x => x + a + 1) = fun i => 2 ^ a * (2 * 2 ^ i)
⊢ (2 ^ a * 1 + 2 ^ a * (2 * (map (HPow.hPow 2) L₀).sum)).bitIndices = a :: map (fun x => x + a + 1) L₀

Tactic:
rw [← mul_add, bitIndices_two_pow_mul, add_comm, bitIndices_two_mul_add_one,
  bitIndices_twoPowsum hL₀]

Result:
case cons.intro.intro.intro
a : ℕ
L₀ : List ℕ
hL₀ : Sorted (fun x1 x2 => x1 < x2) L₀
hL✝ : Sorted (fun x1 x2 => x1 < x2) (a :: map (fun x => x + a + 1) L₀)
hL : Sorted (fun x1 x2 => x1 < x2) (map (fun x => x + a + 1) L₀)
haL : ∀ b ∈ map (fun x => x + a + 1) L₀, a + 1 ≤ b
x✝ : L₀.length < (a :: map (fun x => x + a + 1) L₀).length
hrw : ((fun x => 2 ^ x) ∘ fun x => x + a + 1) = fun i => 2 ^ a * (2 * 2 ^ i)
⊢ map (fun x => x + a) (0 :: map (fun x => x + 1) L₀) = a :: map (fun x => x + a + 1) L₀

Proof state:
case cons
a : ℕ
L : List ℕ
hL : Sorted (fun x1 x2 => x1 < x2) (a :: L)
⊢ (map (fun i => 2 ^ i) (a :: L)).sum.bitIndices = a :: L

Tactic:
obtain ⟨haL, hL⟩ := sorted_cons.1 hL

Result:
case cons.intro
a : ℕ
L : List ℕ
hL✝ : Sorted (fun x1 x2 => x1 < x2) (a :: L)
haL : ∀ b ∈ L, a < b
hL : Sorted (fun x1 x2 => x1 < x2) L
⊢ (map (fun i => 2 ^ i) (a :: L)).sum.bitIndices = a :: L

Proof state:
case refine_1.H
a : ℕ
L : List ℕ
hL✝ : Sorted (fun x1 x2 => x1 < x2) (a :: L)
hL : Sorted (fun x1 x2 => x1 < x2) L
haL : ∀ b ∈ L, a + 1 ≤ b
⊢ ∀ (a_1 b : ℕ), a_1 ∈ L → b ∈ L → (a_1 - (a + 1) < b - (a + 1) ↔ a_1 < b)

Tactic:
exact fun x y hx _ ↦ by rw [tsub_lt_tsub_iff_right (haL _ hx)]

Result:
no goals

Proof state:
case cons.intro
a : ℕ
L : List ℕ
hL✝ : Sorted (fun x1 x2 => x1 < x2) (a :: L)
hL : Sorted (fun x1 x2 => x1 < x2) L
haL : ∀ b ∈ L, a + 1 ≤ b
h' : ∃ L₀, Sorted (fun x1 x2 => x1 < x2) L₀ ∧ L = map (fun x => x + a + 1) L₀
⊢ (map (fun i => 2 ^ i) (a :: L)).sum.bitIndices = a :: L

Tactic:
obtain ⟨L₀, hL₀, rfl⟩ := h'

Result:
case cons.intro.intro.intro
a : ℕ
L₀ : List ℕ
hL₀ : Sorted (fun x1 x2 => x1 < x2) L₀
hL✝ : Sorted (fun x1 x2 => x1 < x2) (a :: map (fun x => x + a + 1) L₀)
hL : Sorted (fun x1 x2 => x1 < x2) (map (fun x => x + a + 1) L₀)
haL : ∀ b ∈ map (fun x => x + a + 1) L₀, a + 1 ≤ b
⊢ (map (fun i => 2 ^ i) (a :: map (fun x => x + a + 1) L₀)).sum.bitIndices = a :: map (fun x => x + a + 1) L₀

Proof state:
case refine_2
a : ℕ
L : List ℕ
hL✝ : Sorted (fun x1 x2 => x1 < x2) (a :: L)
hL : Sorted (fun x1 x2 => x1 < x2) L
haL : ∀ b ∈ L, a + 1 ≤ b
h' : ∀ x ∈ L, ((fun x => x + a + 1) ∘ fun x => x - (a + 1)) x = x
⊢ L = map (fun x => x + a + 1) (map (fun x => x - (a + 1)) L)

Tactic:
simp [List.map_congr_left h']

Result:
no goals

Proof state:
case refine_1.H
a : ℕ
L : List ℕ
hL✝ : Sorted (fun x1 x2 => x1 < x2) (a :: L)
hL : Sorted (fun x1 x2 => x1 < x2) L
haL : ∀ b ∈ L, a + 1 ≤ b
⊢ ∀ (a_1 b : ℕ), a_1 ∈ L ∧ b ∈ L ∧ a_1 - (a + 1) < b - (a + 1) ↔ a_1 ∈ L ∧ b ∈ L ∧ a_1 < b

Tactic:
simp only [and_congr_right_iff]

Result:
case refine_1.H
a : ℕ
L : List ℕ
hL✝ : Sorted (fun x1 x2 => x1 < x2) (a :: L)
hL : Sorted (fun x1 x2 => x1 < x2) L
haL : ∀ b ∈ L, a + 1 ≤ b
⊢ ∀ (a_1 b : ℕ), a_1 ∈ L → b ∈ L → (a_1 - (a + 1) < b - (a + 1) ↔ a_1 < b)

Proof state:
a : ℕ
L : List ℕ
hL✝ : Sorted (fun x1 x2 => x1 < x2) (a :: L)
hL : Sorted (fun x1 x2 => x1 < x2) L
haL : ∀ b ∈ L, a + 1 ≤ b
x : ℕ
hx : x ∈ L
⊢ x - (a + 1) + (a + 1) = x

Tactic:
rw [tsub_add_cancel_of_le (haL _ hx)]

Result:
no goals