Place for IsPrefix.map_iff

Stream: mathlib4

[Elazar Gershuni]

Where does this lemma belong? Is it Init.Data.List.Sublist or Mathlib.Data.List.Infix or something else?

lemma IsPrefix.map_iff {f : α → β} (hf : Function.Injective f) :
    l₁.map f <+: l₂.map f ↔ l₁ <+: l₂ := by
  constructor <;> intro h
  · apply List.prefix_iff_eq_take.mpr
    apply (Function.Injective.list_map hf)
    simpa using List.prefix_iff_eq_take.mp h
  · exact map f h

[Snir Broshi]

Probably next to docs#List.IsPrefix.map (Init.Data.List.Sublist), but it's not in mathlib, so I guess it depends on whether you want to PR to mathlib or lean-core.

[Kim Morrison]

PRing this to lean4 directly is fine, as long as you do the suffix version too. Please ping me (here) if you do.

[Eric Wieser]

The docs#Function.Injective.list_map lemma you use is currently in Mathlib, so I'd suggest putting this in mathlib for now

[Eric Wieser]

Here's a shorter proof:

lemma IsPrefix.map_iff {f : α → β} (hf : Function.Injective f) :
    l₁.map f <+: l₂.map f ↔ l₁ <+: l₂ := by
  simp_rw [List.prefix_iff_eq_take, ← List.map_take, List.length_map, hf.list_map.eq_iff]

[Robin Arnez]

Here's also a mathlib-free proof:

theorem IsPrefix.map_iff {f : α → β} (hf : Function.Injective f) :
    l₁.map f <+: l₂.map f ↔ l₁ <+: l₂ := by
  simp [List.prefix_iff_eq_take, ← List.map_take, List.length_map, List.map_inj_right hf]

using List.map_inj_right instead of Function.Injective.list_map

[Elazar Gershuni]

Kim Morrison said:

PRing this to lean4 directly is fine, as long as you do the suffix version too. Please ping me (here) if you do.

Opened PR #12108 for Init/Data/List/Nat/Sublist.lean:

theorem prefix_map_iff_of_injective {f : α → β} (hf : Function.Injective f) :
    l₁.map f <+: l₂.map f ↔ l₁ <+: l₂ := by
  simp [prefix_iff_eq_take, ← map_take, map_inj_right hf]

theorem suffix_map_iff_of_injective {f : α → β} (hf : Function.Injective f) :
    l₁.map f <:+ l₂.map f ↔ l₁ <:+ l₂ := by
  simp [suffix_iff_eq_drop, ← map_drop, map_inj_right hf]

@Robin Arnez thanks for the proof!