α✝ : Type u
β✝ : Type v
γ✝ : Type w
α : Type u_1
β : Type u_2
γ : Type u_3
l : List α
f : List α → β
g : β → γ
r : List β
s : List γ
⊢ (g ∘ f) [] :: (map g r ++ s) = map g (f [] :: r) ++ s
α✝ : Type u
β✝ : Type v
γ✝ : Type w
α : Type u_1
β : Type u_2
γ : Type u_3
l : List α
f : List α → β
g : β → γ
r : List β
s : List γ
⊢ sublistsLenAux 0 l (g ∘ f) (map g r ++ s) = map g (sublistsLenAux 0 l f r) ++ s
unfold sublistsLenAux
no goals
α✝ : Type u
β✝ : Type v
γ✝ : Type w
α : Type u_1
β : Type u_2
γ : Type u_3
l : List α
f : List α → β
g : β → γ
r : List β
s : List γ
⊢ (g ∘ f) [] :: (map g r ++ s) = map g (f [] :: r) ++ s
simp
α✝ : Type u
β✝ : Type v
γ✝ : Type w
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
a : α
l : List α
f : List α → β
g : β → γ
r : List β
s : List γ
⊢ sublistsLenAux (Nat.add n 0 + 1) l (g ∘ f) (sublistsLenAux (Nat.add n 0) l ((g ∘ f) ∘ cons a) (map g r ++ s)) =
    map g (sublistsLenAux (Nat.add n 0 + 1) l f (sublistsLenAux (Nat.add n 0) l (f ∘ cons a) r)) ++ s
α✝ : Type u
β✝ : Type v
γ✝ : Type w
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
a : α
l : List α
f : List α → β
g : β → γ
r : List β
s : List γ
⊢ sublistsLenAux (n + 1) (a :: l) (g ∘ f) (map g r ++ s) = map g (sublistsLenAux (n + 1) (a :: l) f r) ++ s
unfold sublistsLenAux
no goals
α✝ : Type u
β✝ : Type v
γ✝ : Type w
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
a : α
l : List α
f : List α → β
g : β → γ
r : List β
s : List γ
⊢ sublistsLenAux (Nat.add n 0 + 1) l (g ∘ f) (sublistsLenAux (Nat.add n 0) l ((g ∘ f) ∘ cons a) (map g r ++ s)) =
    map g (sublistsLenAux (Nat.add n 0 + 1) l f (sublistsLenAux (Nat.add n 0) l (f ∘ cons a) r)) ++ s
simp only [show (g ∘ f) ∘ List.cons a = g ∘ f ∘ List.cons a by rfl, sublistsLenAux_append,
  sublistsLenAux_append]
no goals
α✝ : Type u
β✝ : Type v
γ✝ : Type w
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
a : α
l : List α
f : List α → β
g : β → γ
r : List β
s : List γ
⊢ (g ∘ f) ∘ cons a = g ∘ f ∘ cons a
rfl