list.fin_range_succ

Stream: Is there code for X?

[Eric Wieser]

Do we have something like this?

lemma fin_range_succ (n : ℕ) : list.fin_range n.succ = 0 :: (list.fin_range n).map fin.succ :=
begin
  simp_rw [list.fin_range, list.range_succ_eq_map, list.pmap, list.pmap_map, list.map_pmap],
  refine ⟨rfl, _⟩,
  simp,
  sorry
end

docs#list.fin_range_succ doesn't exist

[Yaël Dillies]

Eh, this should be covered by branch#fin_range

[Yaël Dillies]

If you wait two weeks, my locally listable orders PR will be out

[Eric Rodriguez]

I did just make docs#finset.range_sdiff_zero so i'd be quite surprised

[Eric Wieser]

Got there in the end:

lemma _root_.list.map_coe_fin_range (n : ℕ) : (list.fin_range n).map coe = list.range n :=
begin
  simp_rw [list.fin_range, list.map_pmap, fin.mk, subtype.coe_mk, list.pmap_eq_map],
  exact list.map_id _
end

lemma _root_.list.fin_range_succ (n : ℕ) : list.fin_range n.succ = 0 :: (list.fin_range n).map fin.succ :=
begin
  apply list.map_injective_iff.mpr subtype.coe_injective,
  rw [list.map_cons, list.map_coe_fin_range, list.range_succ_eq_map, fin.coe_zero,
    list.map_map],
  have : coe ∘ (fin.succ : fin n → fin n.succ) = nat.succ ∘ coe,
  { ext ⟨x, hx⟩, refl },
  rw [this, ←list.map_map nat.succ coe, list.map_coe_fin_range],
end

[Yaël Dillies]

This is not fun :confused:

[Eric Wieser]

This is far from the most not fun of the stuff I'm dealing with...

[Yakov Pechersky]

Can you go through docs#list.ext_le?

[Eric Wieser]

Maybe. It would be slightly less bad if fin.coe_succ were true by rfl

[Eric Wieser]

PR'd as #10654, let's move golfing there