Theorem: Imo1968P2.lemma0 (Compfiles/Imo1968P2.lean)

State before:
α β : Type
f : ℕ → α → β
l : List α
h2 : l ≠ []
⊢ (List.mapIdx f l).getLast ⋯ = f l.dropLast.length (l.getLast h2)
Tactic:
simp_rw [List.mapIdx_eq_enum_map]
State after:
α β : Type
f : ℕ → α → β
l : List α
h2 : l ≠ []
⊢ (List.map (Function.uncurry f) l.enum).getLast ⋯ = f l.dropLast.length (l.getLast h2)

State before:
α β : Type
f : ℕ → α → β
l : List α
h2 : l ≠ []
⊢ (List.map (Function.uncurry f) l.enum).getLast ⋯ = f l.dropLast.length (l.getLast h2)
Tactic:
rw [List.getLast_eq_get, List.get_map, List.get_enum]
State after:
α β : Type
f : ℕ → α → β
l : List α
h2 : l ≠ []
⊢ Function.uncurry f
      (↑⟨↑⟨(List.map (Function.uncurry f) l.enum).length - 1, ⋯⟩, ⋯⟩,
        l.get (Fin.cast ⋯ ⟨↑⟨(List.map (Function.uncurry f) l.enum).length - 1, ⋯⟩, ⋯⟩)) =
    f l.dropLast.length (l.getLast h2)

State before:
α β : Type
f : ℕ → α → β
l : List α
h2 : l ≠ []
⊢ Function.uncurry f
      (↑⟨↑⟨(List.map (Function.uncurry f) l.enum).length - 1, ⋯⟩, ⋯⟩,
        l.get (Fin.cast ⋯ ⟨↑⟨(List.map (Function.uncurry f) l.enum).length - 1, ⋯⟩, ⋯⟩)) =
    f l.dropLast.length (l.getLast h2)
Tactic:
simp only [List.length_map, List.enum_length, Function.uncurry_apply_pair, List.length_dropLast]
State after:
α β : Type
f : ℕ → α → β
l : List α
h2 : l ≠ []
⊢ f (l.length - 1) (l.get (Fin.cast ⋯ ⟨l.length - 1, ⋯⟩)) = f (l.length - 1) (l.getLast h2)

State before:
α β : Type
f : ℕ → α → β
l : List α
h2 : l ≠ []
⊢ f (l.length - 1) (l.get (Fin.cast ⋯ ⟨l.length - 1, ⋯⟩)) = f (l.length - 1) (l.getLast h2)
Tactic:
congr
State after:
case e_a
α β : Type
f : ℕ → α → β
l : List α
h2 : l ≠ []
⊢ l.get (Fin.cast ⋯ ⟨l.length - 1, ⋯⟩) = l.getLast h2

State before:
case e_a
α β : Type
f : ℕ → α → β
l : List α
h2 : l ≠ []
⊢ l.get (Fin.cast ⋯ ⟨l.length - 1, ⋯⟩) = l.getLast h2
Tactic:
exact List.get_length_sub_one _
State after:
no goals