case zero
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
l₁✝ l₂✝ : List α
h✝ : l₁✝ <+ l₂✝
l₁ l₂ : List α
h : l₁ <+ l₂
⊢ sublistsLen zero l₁ <+ sublistsLen zero l₂

case succ
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
l₁✝ l₂✝ : List α
h✝ : l₁✝ <+ l₂✝
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → sublistsLen n l₁ <+ sublistsLen n l₂
l₁ l₂ : List α
h : l₁ <+ l₂
⊢ sublistsLen (succ n) l₁ <+ sublistsLen (succ n) l₂
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
n : ℕ
l₁ l₂ : List α
h : l₁ <+ l₂
⊢ sublistsLen n l₁ <+ sublistsLen n l₂
induction' n with n IHn generalizing l₁ l₂
case succ.slnil
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
l₁✝ l₂✝ : List α
h : l₁✝ <+ l₂✝
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → sublistsLen n l₁ <+ sublistsLen n l₂
l₁ l₂ : List α
⊢ sublistsLen (succ n) [] <+ sublistsLen (succ n) []

case succ.cons
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
l₁✝¹ l₂✝¹ : List α
h : l₁✝¹ <+ l₂✝¹
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → sublistsLen n l₁ <+ sublistsLen n l₂
l₁✝ l₂✝ l₁ l₂ : List α
a : α
a✝ : l₁ <+ l₂
IH : sublistsLen (succ n) l₁ <+ sublistsLen (succ n) l₂
⊢ sublistsLen (succ n) l₁ <+ sublistsLen (succ n) (a :: l₂)

case succ.cons₂
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
l₁✝¹ l₂✝¹ : List α
h : l₁✝¹ <+ l₂✝¹
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → sublistsLen n l₁ <+ sublistsLen n l₂
l₁✝ l₂✝ l₁ l₂ : List α
a : α
s : l₁ <+ l₂
IH : sublistsLen (succ n) l₁ <+ sublistsLen (succ n) l₂
⊢ sublistsLen (succ n) (a :: l₁) <+ sublistsLen (succ n) (a :: l₂)
case succ
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
l₁✝ l₂✝ : List α
h✝ : l₁✝ <+ l₂✝
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → sublistsLen n l₁ <+ sublistsLen n l₂
l₁ l₂ : List α
h : l₁ <+ l₂
⊢ sublistsLen (succ n) l₁ <+ sublistsLen (succ n) l₂
induction' h with l₁ l₂ a _ IH l₁ l₂ a s IH
no goals
case zero
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
l₁✝ l₂✝ : List α
h✝ : l₁✝ <+ l₂✝
l₁ l₂ : List α
h : l₁ <+ l₂
⊢ sublistsLen zero l₁ <+ sublistsLen zero l₂
simp
no goals
case succ.slnil
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
l₁✝ l₂✝ : List α
h : l₁✝ <+ l₂✝
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → sublistsLen n l₁ <+ sublistsLen n l₂
l₁ l₂ : List α
⊢ sublistsLen (succ n) [] <+ sublistsLen (succ n) []
rfl
case succ.cons
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
l₁✝¹ l₂✝¹ : List α
h : l₁✝¹ <+ l₂✝¹
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → sublistsLen n l₁ <+ sublistsLen n l₂
l₁✝ l₂✝ l₁ l₂ : List α
a : α
a✝ : l₁ <+ l₂
IH : sublistsLen (succ n) l₁ <+ sublistsLen (succ n) l₂
⊢ sublistsLen (succ n) l₂ <+ sublistsLen (succ n) (a :: l₂)
case succ.cons
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
l₁✝¹ l₂✝¹ : List α
h : l₁✝¹ <+ l₂✝¹
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → sublistsLen n l₁ <+ sublistsLen n l₂
l₁✝ l₂✝ l₁ l₂ : List α
a : α
a✝ : l₁ <+ l₂
IH : sublistsLen (succ n) l₁ <+ sublistsLen (succ n) l₂
⊢ sublistsLen (succ n) l₁ <+ sublistsLen (succ n) (a :: l₂)
refine' IH.trans _
case succ.cons
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
l₁✝¹ l₂✝¹ : List α
h : l₁✝¹ <+ l₂✝¹
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → sublistsLen n l₁ <+ sublistsLen n l₂
l₁✝ l₂✝ l₁ l₂ : List α
a : α
a✝ : l₁ <+ l₂
IH : sublistsLen (succ n) l₁ <+ sublistsLen (succ n) l₂
⊢ sublistsLen (succ n) l₂ <+ sublistsLen (n + 1) l₂ ++ map (cons a) (sublistsLen n l₂)
case succ.cons
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
l₁✝¹ l₂✝¹ : List α
h : l₁✝¹ <+ l₂✝¹
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → sublistsLen n l₁ <+ sublistsLen n l₂
l₁✝ l₂✝ l₁ l₂ : List α
a : α
a✝ : l₁ <+ l₂
IH : sublistsLen (succ n) l₁ <+ sublistsLen (succ n) l₂
⊢ sublistsLen (succ n) l₂ <+ sublistsLen (succ n) (a :: l₂)
rw [sublistsLen_succ_cons]
no goals
case succ.cons
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
l₁✝¹ l₂✝¹ : List α
h : l₁✝¹ <+ l₂✝¹
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → sublistsLen n l₁ <+ sublistsLen n l₂
l₁✝ l₂✝ l₁ l₂ : List α
a : α
a✝ : l₁ <+ l₂
IH : sublistsLen (succ n) l₁ <+ sublistsLen (succ n) l₂
⊢ sublistsLen (succ n) l₂ <+ sublistsLen (n + 1) l₂ ++ map (cons a) (sublistsLen n l₂)
apply sublist_append_left
case succ.cons₂
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
l₁✝¹ l₂✝¹ : List α
h : l₁✝¹ <+ l₂✝¹
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → sublistsLen n l₁ <+ sublistsLen n l₂
l₁✝ l₂✝ l₁ l₂ : List α
a : α
s : l₁ <+ l₂
IH : sublistsLen (succ n) l₁ <+ sublistsLen (succ n) l₂
⊢ sublistsLen (n + 1) l₁ ++ map (cons a) (sublistsLen n l₁) <+ sublistsLen (n + 1) l₂ ++ map (cons a) (sublistsLen n l₂)
case succ.cons₂
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
l₁✝¹ l₂✝¹ : List α
h : l₁✝¹ <+ l₂✝¹
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → sublistsLen n l₁ <+ sublistsLen n l₂
l₁✝ l₂✝ l₁ l₂ : List α
a : α
s : l₁ <+ l₂
IH : sublistsLen (succ n) l₁ <+ sublistsLen (succ n) l₂
⊢ sublistsLen (succ n) (a :: l₁) <+ sublistsLen (succ n) (a :: l₂)
simp [sublistsLen_succ_cons]
no goals
case succ.cons₂
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
l₁✝¹ l₂✝¹ : List α
h : l₁✝¹ <+ l₂✝¹
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → sublistsLen n l₁ <+ sublistsLen n l₂
l₁✝ l₂✝ l₁ l₂ : List α
a : α
s : l₁ <+ l₂
IH : sublistsLen (succ n) l₁ <+ sublistsLen (succ n) l₂
⊢ sublistsLen (n + 1) l₁ ++ map (cons a) (sublistsLen n l₁) <+ sublistsLen (n + 1) l₂ ++ map (cons a) (sublistsLen n l₂)
exact IH.append ((IHn s).map _)