case nil
α : Type u_1
β : Type u_2
l₂ : List β
⊢ length ([] ×ˢ l₂) = length [] * length l₂

case cons
α : Type u_1
β : Type u_2
l₂ : List β
x : α
l₁ : List α
IH : length (l₁ ×ˢ l₂) = length l₁ * length l₂
⊢ length ((x :: l₁) ×ˢ l₂) = length (x :: l₁) * length l₂
α : Type u_1
β : Type u_2
l₁ : List α
l₂ : List β
⊢ length (l₁ ×ˢ l₂) = length l₁ * length l₂
induction' l₁ with x l₁ IH
no goals
case nil
α : Type u_1
β : Type u_2
l₂ : List β
⊢ length ([] ×ˢ l₂) = length [] * length l₂
exact (zero_mul _).symm
no goals
case cons
α : Type u_1
β : Type u_2
l₂ : List β
x : α
l₁ : List α
IH : length (l₁ ×ˢ l₂) = length l₁ * length l₂
⊢ length ((x :: l₁) ×ˢ l₂) = length (x :: l₁) * length l₂
simp only [length, product_cons, length_append, IH, right_distrib, one_mul, length_map,
  add_comm]