Theorem: List.getD_reverse (One.lean)

State before:
i : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < length l
⊢ getD (reverse l) i d = l[length l - 1 - i]
Tactic:
unfold List.getD
State after:
i : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < length l
⊢ Option.getD (get? (reverse l) i) d = l[length l - 1 - i]

State before:
i : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < length l
⊢ Option.getD (get? (reverse l) i) d = l[length l - 1 - i]
Tactic:
rw [List.get?_reverse, List.get?_eq_get]
State after:
i : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < length l
⊢ Option.getD (some (get l { val := length l - 1 - i, isLt := ?m.112638 })) d = l[length l - 1 - i]

i : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < length l
⊢ length l - 1 - i < length l

case h
i : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < length l
⊢ i < length l

State before:
i : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < length l
⊢ Option.getD (some (get l { val := length l - 1 - i, isLt := ?m.112638 })) d = l[length l - 1 - i]

i : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < length l
⊢ length l - 1 - i < length l

case h
i : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < length l
⊢ i < length l
Tactic:
simp only [tsub_le_iff_right, ge_iff_le, Option.getD_some, getElem_eq_get]
State after:
i : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < length l
⊢ length l - 1 - i < length l

case h
i : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < length l
⊢ i < length l

State before:
i : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < length l
⊢ length l - 1 - i < length l

case h
i : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < length l
⊢ i < length l
Tactic:
. exact Nat.sub_one_sub_lt P
State after:
case h
i : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < length l
⊢ i < length l

State before:
case h
i : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < length l
⊢ i < length l
Tactic:
. exact P
State after:
no goals