-- Mathlib/Data/List/Sublists.lean
theorem sublistsLen_sublist_of_sublist (n) {l₁ l₂ : List α} (h : l₁ <+ l₂) :
    sublistsLen n l₁ <+ sublistsLen n l₂

Proof state:
case succ.cons
α : Type u
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → sublistsLen n l₁ <+ sublistsLen n l₂
l₁✝ l₂✝ l₁ l₂ : List α
a : α
a✝ : l₁ <+ l₂
IH : sublistsLen (n + 1) l₁ <+ sublistsLen (n + 1) l₂
⊢ sublistsLen (n + 1) l₂ <+ sublistsLen (n + 1) l₂ ++ map (cons a) (sublistsLen n l₂)

Tactic:
apply sublist_append_left

Result:
no goals

Proof state:
α : Type u
n : ℕ
l₁ l₂ : List α
h : l₁ <+ l₂
⊢ sublistsLen n l₁ <+ sublistsLen n l₂

Tactic:
induction' n with n IHn generalizing l₁ l₂

Result:
case zero
α : Type u
l₁ l₂ : List α
h : l₁ <+ l₂
⊢ sublistsLen 0 l₁ <+ sublistsLen 0 l₂

case succ
α : Type u
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → sublistsLen n l₁ <+ sublistsLen n l₂
l₁ l₂ : List α
h : l₁ <+ l₂
⊢ sublistsLen (n + 1) l₁ <+ sublistsLen (n + 1) l₂

Proof state:
case succ.cons₂
α : Type u
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → sublistsLen n l₁ <+ sublistsLen n l₂
l₁✝ l₂✝ l₁ l₂ : List α
a : α
s : l₁ <+ l₂
IH : sublistsLen (n + 1) l₁ <+ sublistsLen (n + 1) l₂
⊢ sublistsLen (n + 1) (a :: l₁) <+ sublistsLen (n + 1) (a :: l₂)

Tactic:
simpa only [sublistsLen_succ_cons] using IH.append ((IHn s).map _)

Result:
no goals

Proof state:
case succ.cons
α : Type u
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → sublistsLen n l₁ <+ sublistsLen n l₂
l₁✝ l₂✝ l₁ l₂ : List α
a : α
a✝ : l₁ <+ l₂
IH : sublistsLen (n + 1) l₁ <+ sublistsLen (n + 1) l₂
⊢ sublistsLen (n + 1) l₂ <+ sublistsLen (n + 1) (a :: l₂)

Tactic:
rw [sublistsLen_succ_cons]

Result:
case succ.cons
α : Type u
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → sublistsLen n l₁ <+ sublistsLen n l₂
l₁✝ l₂✝ l₁ l₂ : List α
a : α
a✝ : l₁ <+ l₂
IH : sublistsLen (n + 1) l₁ <+ sublistsLen (n + 1) l₂
⊢ sublistsLen (n + 1) l₂ <+ sublistsLen (n + 1) l₂ ++ map (cons a) (sublistsLen n l₂)

Proof state:
case succ.slnil
α : Type u
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → sublistsLen n l₁ <+ sublistsLen n l₂
l₁ l₂ : List α
⊢ sublistsLen (n + 1) [] <+ sublistsLen (n + 1) []

Tactic:
rfl

Result:
no goals

Proof state:
case succ
α : Type u
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → sublistsLen n l₁ <+ sublistsLen n l₂
l₁ l₂ : List α
h : l₁ <+ l₂
⊢ sublistsLen (n + 1) l₁ <+ sublistsLen (n + 1) l₂

Tactic:
induction' h with l₁ l₂ a _ IH l₁ l₂ a s IH

Result:
case succ.slnil
α : Type u
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → sublistsLen n l₁ <+ sublistsLen n l₂
l₁ l₂ : List α
⊢ sublistsLen (n + 1) [] <+ sublistsLen (n + 1) []

case succ.cons
α : Type u
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → sublistsLen n l₁ <+ sublistsLen n l₂
l₁✝ l₂✝ l₁ l₂ : List α
a : α
a✝ : l₁ <+ l₂
IH : sublistsLen (n + 1) l₁ <+ sublistsLen (n + 1) l₂
⊢ sublistsLen (n + 1) l₁ <+ sublistsLen (n + 1) (a :: l₂)

case succ.cons₂
α : Type u
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → sublistsLen n l₁ <+ sublistsLen n l₂
l₁✝ l₂✝ l₁ l₂ : List α
a : α
s : l₁ <+ l₂
IH : sublistsLen (n + 1) l₁ <+ sublistsLen (n + 1) l₂
⊢ sublistsLen (n + 1) (a :: l₁) <+ sublistsLen (n + 1) (a :: l₂)

Proof state:
case zero
α : Type u
l₁ l₂ : List α
h : l₁ <+ l₂
⊢ sublistsLen 0 l₁ <+ sublistsLen 0 l₂

Tactic:
simp

Result:
no goals

Proof state:
case succ.cons
α : Type u
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → sublistsLen n l₁ <+ sublistsLen n l₂
l₁✝ l₂✝ l₁ l₂ : List α
a : α
a✝ : l₁ <+ l₂
IH : sublistsLen (n + 1) l₁ <+ sublistsLen (n + 1) l₂
⊢ sublistsLen (n + 1) l₁ <+ sublistsLen (n + 1) (a :: l₂)

Tactic:
refine IH.trans ?_

Result:
case succ.cons
α : Type u
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → sublistsLen n l₁ <+ sublistsLen n l₂
l₁✝ l₂✝ l₁ l₂ : List α
a : α
a✝ : l₁ <+ l₂
IH : sublistsLen (n + 1) l₁ <+ sublistsLen (n + 1) l₂
⊢ sublistsLen (n + 1) l₂ <+ sublistsLen (n + 1) (a :: l₂)