case nil
α : Type u_1
β : Type ?u.16166
σ : α → Type u_2
l₂ : (a : α) → List (σ a)
⊢ length (List.sigma [] l₂) = sum (map (fun a => length (l₂ a)) [])

case cons
α : Type u_1
β : Type ?u.16166
σ : α → Type u_2
l₂ : (a : α) → List (σ a)
x : α
l₁ : List α
IH : length (List.sigma l₁ l₂) = sum (map (fun a => length (l₂ a)) l₁)
⊢ length (List.sigma (x :: l₁) l₂) = sum (map (fun a => length (l₂ a)) (x :: l₁))
α : Type u_1
β : Type ?u.16166
σ : α → Type u_2
l₁ : List α
l₂ : (a : α) → List (σ a)
⊢ length (List.sigma l₁ l₂) = sum (map (fun a => length (l₂ a)) l₁)
induction' l₁ with x l₁ IH
no goals
case nil
α : Type u_1
β : Type ?u.16166
σ : α → Type u_2
l₂ : (a : α) → List (σ a)
⊢ length (List.sigma [] l₂) = sum (map (fun a => length (l₂ a)) [])
rfl
no goals
case cons
α : Type u_1
β : Type ?u.16166
σ : α → Type u_2
l₂ : (a : α) → List (σ a)
x : α
l₁ : List α
IH : length (List.sigma l₁ l₂) = sum (map (fun a => length (l₂ a)) l₁)
⊢ length (List.sigma (x :: l₁) l₂) = sum (map (fun a => length (l₂ a)) (x :: l₁))
simp only [map, sigma_cons, length_append, length_map, IH, sum_cons]