-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MapIdx.lean
theorem mapIdx_reverse {l : List α} {f : Nat → α → β} :
    l.reverse.mapIdx f = (mapIdx (fun i => f (l.length - 1 - i)) l).reverse

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : Nat → α → β
i : Nat
h : l.length ≤ i
⊢ (mapIdx (fun i => f (l.length - 1 - i)) l).reverse.length ≤ i

Tactic:
simp [h]

Result:
no goals

Proof state:
case neg
α : Type u_1
β : Type u_2
l : List α
f : Nat → α → β
i : Nat
h : l.length ≤ i
⊢ none = Option.map (f i) none

Tactic:
simp

Result:
no goals

Proof state:
case neg
α : Type u_1
β : Type u_2
l : List α
f : Nat → α → β
i : Nat
h : ¬i < l.length
⊢ (mapIdx (fun i => f (l.length - 1 - i)) l).reverse[i]? = Option.map (f i) l.reverse[i]?

Tactic:
simp at h

Result:
case neg
α : Type u_1
β : Type u_2
l : List α
f : Nat → α → β
i : Nat
h : l.length ≤ i
⊢ (mapIdx (fun i => f (l.length - 1 - i)) l).reverse[i]? = Option.map (f i) l.reverse[i]?

Proof state:
case neg
α : Type u_1
β : Type u_2
l : List α
f : Nat → α → β
i : Nat
h : l.length ≤ i
⊢ (mapIdx (fun i => f (l.length - 1 - i)) l).reverse[i]? = Option.map (f i) l.reverse[i]?

Tactic:
rw [getElem?_eq_none (by simp [h]), getElem?_eq_none (by simp [h])]

Result:
case neg
α : Type u_1
β : Type u_2
l : List α
f : Nat → α → β
i : Nat
h : l.length ≤ i
⊢ none = Option.map (f i) none

Proof state:
case pos.e_a
α : Type u_1
β : Type u_2
l : List α
f : Nat → α → β
i : Nat
h : i < l.length
⊢ l.length - 1 - (l.length - 1 - i) = i

Tactic:
omega

Result:
no goals

Proof state:
case pos
α : Type u_1
β : Type u_2
l : List α
f : Nat → α → β
i : Nat
h : i < l.length
⊢ (mapIdx (fun i => f (l.length - 1 - i)) l).reverse[i]? = Option.map (f i) l.reverse[i]?

Tactic:
simp [getElem?_reverse, h]

Result:
case pos
α : Type u_1
β : Type u_2
l : List α
f : Nat → α → β
i : Nat
h : i < l.length
⊢ f (l.length - 1 - (l.length - 1 - i)) l[l.length - 1 - i] = f i l[l.length - 1 - i]

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : Nat → α → β
⊢ mapIdx f l.reverse = (mapIdx (fun i => f (l.length - 1 - i)) l).reverse

Tactic:
simp [mapIdx_eq_iff]

Result:
α : Type u_1
β : Type u_2
l : List α
f : Nat → α → β
⊢ ∀ (i : Nat), (mapIdx (fun i => f (l.length - 1 - i)) l).reverse[i]? = Option.map (f i) l.reverse[i]?

Proof state:
case pos
α : Type u_1
β : Type u_2
l : List α
f : Nat → α → β
i : Nat
h : i < l.length
⊢ f (l.length - 1 - (l.length - 1 - i)) l[l.length - 1 - i] = f i l[l.length - 1 - i]

Tactic:
congr

Result:
case pos.e_a
α : Type u_1
β : Type u_2
l : List α
f : Nat → α → β
i : Nat
h : i < l.length
⊢ l.length - 1 - (l.length - 1 - i) = i

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : Nat → α → β
⊢ ∀ (i : Nat), (mapIdx (fun i => f (l.length - 1 - i)) l).reverse[i]? = Option.map (f i) l.reverse[i]?

Tactic:
intro i

Result:
α : Type u_1
β : Type u_2
l : List α
f : Nat → α → β
i : Nat
⊢ (mapIdx (fun i => f (l.length - 1 - i)) l).reverse[i]? = Option.map (f i) l.reverse[i]?

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : Nat → α → β
i : Nat
h : l.length ≤ i
⊢ l.reverse.length ≤ i

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : Nat → α → β
i : Nat
⊢ (mapIdx (fun i => f (l.length - 1 - i)) l).reverse[i]? = Option.map (f i) l.reverse[i]?

Tactic:
by_cases h : i < l.length

Result:
case pos
α : Type u_1
β : Type u_2
l : List α
f : Nat → α → β
i : Nat
h : i < l.length
⊢ (mapIdx (fun i => f (l.length - 1 - i)) l).reverse[i]? = Option.map (f i) l.reverse[i]?

case neg
α : Type u_1
β : Type u_2
l : List α
f : Nat → α → β
i : Nat
h : ¬i < l.length
⊢ (mapIdx (fun i => f (l.length - 1 - i)) l).reverse[i]? = Option.map (f i) l.reverse[i]?