Dependent rewrite

Stream: lean4

[James Gallicchio]

Newbie question about rewriting functions with dependencies -- I know I should do an explicit generalization here, but I have no clue what generalization to do:

opaque map' (L : List τ) (f : (x : τ) → x ∈ L → τ') : List τ'

example (L1 L2 : List τ) (hL : L2 = L1) (f : (x : τ) → x ∈ L1 → τ')
  : map' L1 f = map' L2 (fun x h => f x (hL.subst h))
  := by
  sorry

[James Gallicchio]

help would be sorely appreciated; I keep guessing what to generalize, and failing :joy:

[James Gallicchio]

wait a minute, casing on hL is enough

[James Gallicchio]

okay, new question: will eliminating on eq always work if it's between two variables? is the goal of doing explicit generalizations to make an equality be between two variables so you can eliminate on it?

[James Gallicchio]

this actually makes substantially more sense now. hm.

[Reid Barton]

Or even if just one side is a variable