-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Pairwise.lean
theorem map_getElem_sublist {l : List α} {is : List (Fin l.length)} (h : is.Pairwise (· < ·)) :
    is.map (l[·]) <+ l

Proof state:
case cons
α : Type u_1
l : List α
hd : Fin l.length
tl : List (Fin l.length)
IH :
  Pairwise (fun x1 x2 => x1 < x2) tl →
    ∀ (n : Nat), (∀ (i : Fin l.length), i ∈ tl → n ≤ ↑i) → map (fun x => l[x]) tl <+ drop n l
h : Pairwise (fun x1 x2 => x1 < x2) (hd :: tl)
n : Nat
his : ∀ (i : Fin l.length), i ∈ hd :: tl → n ≤ ↑i
this : map (fun x => l[x]) tl <+ drop (↑hd + 1) l
⊢ l[↑hd] :: map (fun x => l[↑x]) tl <+ drop n l

Tactic:
specialize his hd (.head _)

Result:
case cons
α : Type u_1
l : List α
hd : Fin l.length
tl : List (Fin l.length)
IH :
  Pairwise (fun x1 x2 => x1 < x2) tl →
    ∀ (n : Nat), (∀ (i : Fin l.length), i ∈ tl → n ≤ ↑i) → map (fun x => l[x]) tl <+ drop n l
h : Pairwise (fun x1 x2 => x1 < x2) (hd :: tl)
n : Nat
this : map (fun x => l[x]) tl <+ drop (↑hd + 1) l
his : n ≤ ↑hd
⊢ l[↑hd] :: map (fun x => l[↑x]) tl <+ drop n l

Proof state:
case cons
α : Type u_1
l : List α
hd : Fin l.length
tl : List (Fin l.length)
IH :
  Pairwise (fun x1 x2 => x1 < x2) tl →
    ∀ (n : Nat), (∀ (i : Fin l.length), i ∈ tl → n ≤ ↑i) → map (fun x => l[x]) tl <+ drop n l
h : Pairwise (fun x1 x2 => x1 < x2) (hd :: tl)
n : Nat
this✝¹ : map (fun x => l[x]) tl <+ drop (↑hd + 1) l
his : n ≤ ↑hd
this✝ : l.get hd :: map (fun x => l[x]) tl <+ drop (↑hd) l
this : [] ++ l.get hd :: map (fun x => l[x]) tl <+ drop n (take (↑hd) l) ++ drop (↑hd) l
⊢ l[↑hd] :: map (fun x => l[↑x]) tl <+ drop n l

Tactic:
rwa [nil_append, ← (drop_append_of_le_length ?_), take_append_drop] at this

Result:
α : Type u_1
l : List α
hd : Fin l.length
tl : List (Fin l.length)
IH :
  Pairwise (fun x1 x2 => x1 < x2) tl →
    ∀ (n : Nat), (∀ (i : Fin l.length), i ∈ tl → n ≤ ↑i) → map (fun x => l[x]) tl <+ drop n l
h : Pairwise (fun x1 x2 => x1 < x2) (hd :: tl)
n : Nat
this✝¹ : map (fun x => l[x]) tl <+ drop (↑hd + 1) l
his : n ≤ ↑hd
this✝ : l.get hd :: map (fun x => l[x]) tl <+ drop (↑hd) l
this : l.get hd :: map (fun x => l[x]) tl <+ drop n (take (↑hd) l) ++ drop (↑hd) l
⊢ n ≤ (take (↑hd) l).length

Proof state:
case cons
α : Type u_1
l : List α
hd : Fin l.length
tl : List (Fin l.length)
IH :
  Pairwise (fun x1 x2 => x1 < x2) tl →
    ∀ (n : Nat), (∀ (i : Fin l.length), i ∈ tl → n ≤ ↑i) → map (fun x => l[x]) tl <+ drop n l
h : Pairwise (fun x1 x2 => x1 < x2) (hd :: tl)
n : Nat
his : ∀ (i : Fin l.length), i ∈ hd :: tl → n ≤ ↑i
⊢ map (fun x => l[x]) (hd :: tl) <+ drop n l

Tactic:
simp only [Fin.getElem_fin, map_cons]

Result:
case cons
α : Type u_1
l : List α
hd : Fin l.length
tl : List (Fin l.length)
IH :
  Pairwise (fun x1 x2 => x1 < x2) tl →
    ∀ (n : Nat), (∀ (i : Fin l.length), i ∈ tl → n ≤ ↑i) → map (fun x => l[x]) tl <+ drop n l
h : Pairwise (fun x1 x2 => x1 < x2) (hd :: tl)
n : Nat
his : ∀ (i : Fin l.length), i ∈ hd :: tl → n ≤ ↑i
⊢ l[↑hd] :: map (fun x => l[↑x]) tl <+ drop n l

Proof state:
α : Type u_1
l : List α
hd : Fin l.length
tl : List (Fin l.length)
IH :
  Pairwise (fun x1 x2 => x1 < x2) tl →
    ∀ (n : Nat), (∀ (i : Fin l.length), i ∈ tl → n ≤ ↑i) → map (fun x => l[x]) tl <+ drop n l
h : Pairwise (fun x1 x2 => x1 < x2) (hd :: tl)
n : Nat
this✝¹ : map (fun x => l[x]) tl <+ drop (↑hd + 1) l
his : n ≤ ↑hd
this✝ : l.get hd :: map (fun x => l[x]) tl <+ drop (↑hd) l
this : l.get hd :: map (fun x => l[x]) tl <+ drop n (take (↑hd) l) ++ drop (↑hd) l
⊢ n ≤ (take (↑hd) l).length

Tactic:
simp [Nat.min_eq_left (Nat.le_of_lt hd.isLt), his]

Result:
no goals

Proof state:
α : Type u_1
l : List α
is : List (Fin l.length)
h : Pairwise (fun x1 x2 => x1 < x2) is
this : ∀ (n : Nat) (l' : List α), l' = drop n l → (∀ (i : Fin l.length), i ∈ is → n ≤ ↑i) → map (fun x => l[x]) is <+ l'
⊢ l = drop 0 l

Tactic:
simp

Result:
no goals

Proof state:
case nil
α : Type u_1
l : List α
h : Pairwise (fun x1 x2 => x1 < x2) []
n : Nat
his : ∀ (i : Fin l.length), i ∈ [] → n ≤ ↑i
⊢ map (fun x => l[x]) [] <+ drop n l

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_1
l : List α
hd : Fin l.length
tl : List (Fin l.length)
IH :
  Pairwise (fun x1 x2 => x1 < x2) tl →
    ∀ (n : Nat), (∀ (i : Fin l.length), i ∈ tl → n ≤ ↑i) → map (fun x => l[x]) tl <+ drop n l
h : Pairwise (fun x1 x2 => x1 < x2) (hd :: tl)
n : Nat
this✝ : map (fun x => l[x]) tl <+ drop (↑hd + 1) l
his : n ≤ ↑hd
this : l.get hd :: map (fun x => l[x]) tl <+ drop (↑hd) l
⊢ l[↑hd] :: map (fun x => l[↑x]) tl <+ drop n l

Tactic:
have := Sublist.append (nil_sublist (take hd l |>.drop n)) this

Result:
case cons
α : Type u_1
l : List α
hd : Fin l.length
tl : List (Fin l.length)
IH :
  Pairwise (fun x1 x2 => x1 < x2) tl →
    ∀ (n : Nat), (∀ (i : Fin l.length), i ∈ tl → n ≤ ↑i) → map (fun x => l[x]) tl <+ drop n l
h : Pairwise (fun x1 x2 => x1 < x2) (hd :: tl)
n : Nat
this✝¹ : map (fun x => l[x]) tl <+ drop (↑hd + 1) l
his : n ≤ ↑hd
this✝ : l.get hd :: map (fun x => l[x]) tl <+ drop (↑hd) l
this : [] ++ l.get hd :: map (fun x => l[x]) tl <+ drop n (take (↑hd) l) ++ drop (↑hd) l
⊢ l[↑hd] :: map (fun x => l[↑x]) tl <+ drop n l

Proof state:
α : Type u_1
l : List α
is : List (Fin l.length)
h : Pairwise (fun x1 x2 => x1 < x2) is
⊢ ∀ (n : Nat) (l' : List α), l' = drop n l → (∀ (i : Fin l.length), i ∈ is → n ≤ ↑i) → map (fun x => l[x]) is <+ l'

Tactic:
rintro n l' rfl his

Result:
α : Type u_1
l : List α
is : List (Fin l.length)
h : Pairwise (fun x1 x2 => x1 < x2) is
n : Nat
his : ∀ (i : Fin l.length), i ∈ is → n ≤ ↑i
⊢ map (fun x => l[x]) is <+ drop n l

Proof state:
case cons
α : Type u_1
l : List α
hd : Fin l.length
tl : List (Fin l.length)
IH :
  Pairwise (fun x1 x2 => x1 < x2) tl →
    ∀ (n : Nat), (∀ (i : Fin l.length), i ∈ tl → n ≤ ↑i) → map (fun x => l[x]) tl <+ drop n l
h : Pairwise (fun x1 x2 => x1 < x2) (hd :: tl)
n : Nat
his : ∀ (i : Fin l.length), i ∈ hd :: tl → n ≤ ↑i
⊢ l[↑hd] :: map (fun x => l[↑x]) tl <+ drop n l

Tactic:
have := IH h.of_cons (hd+1) (pairwise_cons.mp h).1

Result:
case cons
α : Type u_1
l : List α
hd : Fin l.length
tl : List (Fin l.length)
IH :
  Pairwise (fun x1 x2 => x1 < x2) tl →
    ∀ (n : Nat), (∀ (i : Fin l.length), i ∈ tl → n ≤ ↑i) → map (fun x => l[x]) tl <+ drop n l
h : Pairwise (fun x1 x2 => x1 < x2) (hd :: tl)
n : Nat
his : ∀ (i : Fin l.length), i ∈ hd :: tl → n ≤ ↑i
this : map (fun x => l[x]) tl <+ drop (↑hd + 1) l
⊢ l[↑hd] :: map (fun x => l[↑x]) tl <+ drop n l

Proof state:
α : Type u_1
l : List α
is : List (Fin l.length)
h : Pairwise (fun x1 x2 => x1 < x2) is
this : ∀ (n : Nat) (l' : List α), l' = drop n l → (∀ (i : Fin l.length), i ∈ is → n ≤ ↑i) → map (fun x => l[x]) is <+ l'
⊢ ∀ (i : Fin l.length), i ∈ is → 0 ≤ ↑i

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
l : List α
is : List (Fin l.length)
h : Pairwise (fun x1 x2 => x1 < x2) is
n : Nat
his : ∀ (i : Fin l.length), i ∈ is → n ≤ ↑i
⊢ map (fun x => l[x]) is <+ drop n l

Tactic:
induction is generalizing n with
| nil => simp
| cons hd tl IH =>
  simp only [Fin.getElem_fin, map_cons]
  have := IH h.of_cons (hd+1) (pairwise_cons.mp h).1
  specialize his hd (.head _)
  have := (drop_eq_getElem_cons ..).symm ▸ this.cons₂ (get l hd)
  have := Sublist.append (nil_sublist (take hd l |>.drop n)) this
  rwa [nil_append, ← (drop_append_of_le_length ?_), take_append_drop] at this
  simp [Nat.min_eq_left (Nat.le_of_lt hd.isLt), his]

Result:
no goals