-- 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 refine_1
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
⊢ Sorted (fun x1 x2 => x1 < x2) (map (fun x => x - (a + 1)) L)

Tactic:
rwa [Sorted, pairwise_map, Pairwise.and_mem,
  Pairwise.iff (S := fun x y ↦ x ∈ L ∧ y ∈ L ∧ x < y), ← Pairwise.and_mem]

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 ∈ L ∧ b ∈ L ∧ 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
⊢ ((fun x => x + a + 1) ∘ fun x => x - (a + 1)) x = x

Tactic:
simp only [add_assoc, Function.comp_apply]

Result:
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

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
⊢ L = map (fun x => x + a + 1) (map (fun x => x - (a + 1)) L)

Tactic:
have h' : ∀ x ∈ L, ((fun x ↦ x + a + 1) ∘ (fun x ↦ x - (a + 1))) x = x := fun x hx ↦ by
  simp only [add_assoc, Function.comp_apply]; rw [tsub_add_cancel_of_le (haL _ hx)]

Result:
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)

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 + 2 ^ a * (2 * (map (HPow.hPow 2) L₀).sum)).bitIndices = a :: map (fun x => x + a + 1) L₀

Tactic:
nth_rw 1 [← mul_one (a := 2^a)]

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)
⊢ (2 ^ a * 1 + 2 ^ a * (2 * (map (HPow.hPow 2) L₀).sum)).bitIndices = a :: map (fun x => x + a + 1) 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)
⊢ map (fun x => x + a) (0 :: map (fun x => x + 1) L₀) = a :: map (fun x => x + a + 1) L₀

Tactic:
simp [add_comm (a := 1), add_assoc]

Result:
no goals

Proof state:
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

Tactic:
simp_rw [Nat.lt_iff_add_one_le] at haL

Result:
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
⊢ (map (fun i => 2 ^ i) (a :: L)).sum.bitIndices = a :: 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)
⊢ (map (fun i => 2 ^ i) (a :: map (fun x => x + a + 1) L₀)).sum.bitIndices = a :: map (fun x => x + a + 1) L₀

Tactic:
simp only [List.map_cons, List.map_map, List.sum_map_mul_left, List.sum_cons, hrw]

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)
⊢ (2 ^ a + 2 ^ a * (2 * (map (HPow.hPow 2) L₀).sum)).bitIndices = a :: map (fun x => x + a + 1) L₀

Proof state:
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
⊢ ((fun x => 2 ^ x) ∘ fun x => x + a + 1) = fun i => 2 ^ a * (2 * 2 ^ i)

Tactic:
ext x

Result:
case h
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
x : ℕ
⊢ ((fun x => 2 ^ x) ∘ fun x => x + a + 1) x = 2 ^ a * (2 * 2 ^ x)

Proof state:
case h
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
x : ℕ
⊢ ((fun x => 2 ^ x) ∘ fun x => x + a + 1) x = 2 ^ a * (2 * 2 ^ x)

Tactic:
simp only [Function.comp_apply, pow_add, pow_one]

Result:
case h
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
x : ℕ
⊢ 2 ^ x * 2 ^ a * 2 = 2 ^ a * (2 * 2 ^ x)

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 y : ℕ
hx : x ∈ L
x✝ : y ∈ L
⊢ x - (a + 1) < y - (a + 1) ↔ x < y

Tactic:
rw [tsub_lt_tsub_iff_right (haL _ hx)]

Result:
no goals

Proof state:
case h
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
x : ℕ
⊢ 2 ^ x * 2 ^ a * 2 = 2 ^ a * (2 * 2 ^ x)

Tactic:
ac_rfl

Result:
no goals

Proof state:
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
⊢ L₀.length < (a :: map (fun x => x + a + 1) L₀).length

Tactic:
simp

Result:
no goals

Proof state:
case nil
hL : Sorted (fun x1 x2 => x1 < x2) []
⊢ (map (fun i => 2 ^ i) []).sum.bitIndices = []

Tactic:
simp

Result:
no goals