Theorem: List.take_isInfix_take (One.lean)

State before:
n m : ℕ
α✝ : Type u_1
l : List α✝
h : n ≤ m
⊢ take n l <:+: take m l
Tactic:
rw [← Nat.add_sub_of_le h]
State after:
n m : ℕ
α✝ : Type u_1
l : List α✝
h : n ≤ m
⊢ take n l <:+: take (n + (m - n)) l

State before:
n m : ℕ
α✝ : Type u_1
l : List α✝
h : n ≤ m
⊢ take n l <:+: take (n + (m - n)) l
Tactic:
simp only [List.take_add, ge_iff_le, isInfix_append_left]
State after:
no goals