-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Sublist.lean
theorem prefix_take_le_iff {L : List α} (hm : m < L.length) :
    L.take m <+: L.take n ↔ m ≤ n

Proof state:
case succ
α : Type u_1
m : Nat
IH : ∀ {n : Nat} {L : List α}, m < L.length → (take m L = take (min m L.length) (take n L) ↔ m ≤ n)
n : Nat
L : List α
hm : m + 1 < L.length
⊢ take (m + 1) L = take (min (m + 1) L.length) (take n L) ↔ m + 1 ≤ n

Tactic:
cases L with
| nil => simp_all
| cons l ls =>
  cases n with
  | zero =>
    simp
  | succ n =>
    simp only [length_cons, Nat.succ_eq_add_one, Nat.add_lt_add_iff_right] at hm
    simp [← @IH n ls hm, Nat.min_eq_left, Nat.le_of_lt hm]

Result:
no goals

Proof state:
case succ.cons.succ
α : Type u_1
m : Nat
IH : ∀ {n : Nat} {L : List α}, m < L.length → (take m L = take (min m L.length) (take n L) ↔ m ≤ n)
l : α
ls : List α
hm : m + 1 < (l :: ls).length
n : Nat
⊢ take (m + 1) (l :: ls) = take (min (m + 1) (l :: ls).length) (take (n + 1) (l :: ls)) ↔ m + 1 ≤ n + 1

Tactic:
simp only [length_cons, Nat.succ_eq_add_one, Nat.add_lt_add_iff_right] at hm

Result:
case succ.cons.succ
α : Type u_1
m : Nat
IH : ∀ {n : Nat} {L : List α}, m < L.length → (take m L = take (min m L.length) (take n L) ↔ m ≤ n)
l : α
ls : List α
n : Nat
hm : m < ls.length
⊢ take (m + 1) (l :: ls) = take (min (m + 1) (l :: ls).length) (take (n + 1) (l :: ls)) ↔ m + 1 ≤ n + 1

Proof state:
α : Type u_1
m n : Nat
L : List α
hm : m < L.length
⊢ take m L <+: take n L ↔ m ≤ n

Tactic:
simp only [prefix_iff_eq_take, length_take]

Result:
α : Type u_1
m n : Nat
L : List α
hm : m < L.length
⊢ take m L = take (min m L.length) (take n L) ↔ m ≤ n

Proof state:
case succ.nil
α : Type u_1
m : Nat
IH : ∀ {n : Nat} {L : List α}, m < L.length → (take m L = take (min m L.length) (take n L) ↔ m ≤ n)
n : Nat
hm : m + 1 < [].length
⊢ take (m + 1) [] = take (min (m + 1) [].length) (take n []) ↔ m + 1 ≤ n

Tactic:
simp_all

Result:
no goals

Proof state:
case zero
α : Type u_1
n : Nat
L : List α
hm : 0 < L.length
⊢ take 0 L = take (min 0 L.length) (take n L) ↔ 0 ≤ n

Tactic:
simp [Nat.min_eq_left, eq_self_iff_true, Nat.zero_le, take]

Result:
no goals

Proof state:
case succ.cons.succ
α : Type u_1
m : Nat
IH : ∀ {n : Nat} {L : List α}, m < L.length → (take m L = take (min m L.length) (take n L) ↔ m ≤ n)
l : α
ls : List α
n : Nat
hm : m < ls.length
⊢ take (m + 1) (l :: ls) = take (min (m + 1) (l :: ls).length) (take (n + 1) (l :: ls)) ↔ m + 1 ≤ n + 1

Tactic:
simp [← @IH n ls hm, Nat.min_eq_left, Nat.le_of_lt hm]

Result:
no goals

Proof state:
case succ.cons.zero
α : Type u_1
m : Nat
IH : ∀ {n : Nat} {L : List α}, m < L.length → (take m L = take (min m L.length) (take n L) ↔ m ≤ n)
l : α
ls : List α
hm : m + 1 < (l :: ls).length
⊢ take (m + 1) (l :: ls) = take (min (m + 1) (l :: ls).length) (take 0 (l :: ls)) ↔ m + 1 ≤ 0

Tactic:
simp

Result:
no goals

Proof state:
case succ.cons
α : Type u_1
m : Nat
IH : ∀ {n : Nat} {L : List α}, m < L.length → (take m L = take (min m L.length) (take n L) ↔ m ≤ n)
n : Nat
l : α
ls : List α
hm : m + 1 < (l :: ls).length
⊢ take (m + 1) (l :: ls) = take (min (m + 1) (l :: ls).length) (take n (l :: ls)) ↔ m + 1 ≤ n

Tactic:
cases n with
| zero =>
  simp
| succ n =>
  simp only [length_cons, Nat.succ_eq_add_one, Nat.add_lt_add_iff_right] at hm
  simp [← @IH n ls hm, Nat.min_eq_left, Nat.le_of_lt hm]

Result:
no goals

Proof state:
α : Type u_1
m n : Nat
L : List α
hm : m < L.length
⊢ take m L = take (min m L.length) (take n L) ↔ m ≤ n

Tactic:
induction m generalizing L n with
| zero => simp [Nat.min_eq_left, eq_self_iff_true, Nat.zero_le, take]
| succ m IH =>
  cases L with
  | nil => simp_all
  | cons l ls =>
    cases n with
    | zero =>
      simp
    | succ n =>
      simp only [length_cons, Nat.succ_eq_add_one, Nat.add_lt_add_iff_right] at hm
      simp [← @IH n ls hm, Nat.min_eq_left, Nat.le_of_lt hm]

Result:
no goals