[GOAL]
α : Type u_1
β : Type u_2
head✝ : α
l : List α
⊢ (head✝ :: l) ×ˢ [] = []
[PROOFSTEP]
simp [product_cons, product_nil]
[GOAL]
α : Type u_1
β : Type u_2
l₁ : List α
l₂ : List β
a : α
b : β
⊢ (a, b) ∈ l₁ ×ˢ l₂ ↔ a ∈ l₁ ∧ b ∈ l₂
[PROOFSTEP]
simp_all [SProd.sprod, product, mem_bind, mem_map, Prod.ext_iff, exists_prop, and_left_comm, exists_and_left,
  exists_eq_left, exists_eq_right]
[GOAL]
α : Type u_1
β : Type u_2
l₁ : List α
l₂ : List β
⊢ length (l₁ ×ˢ l₂) = length l₁ * length l₂
[PROOFSTEP]
induction' l₁ with x l₁ IH
[GOAL]
case nil
α : Type u_1
β : Type u_2
l₂ : List β
⊢ length ([] ×ˢ l₂) = length [] * length l₂
[PROOFSTEP]
exact (zero_mul _).symm
[GOAL]
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₂
[PROOFSTEP]
simp only [length, product_cons, length_append, IH, right_distrib, one_mul, length_map, add_comm]
[GOAL]
α : Type u_1
β : Type u_2
σ : α → Type u_3
head✝ : α
l : List α
⊢ (List.sigma (head✝ :: l) fun a => []) = []
[PROOFSTEP]
simp [sigma_cons, sigma_nil]
[GOAL]
α : Type u_1
β : Type u_2
σ : α → Type u_3
l₁ : List α
l₂ : (a : α) → List (σ a)
a : α
b : σ a
⊢ { fst := a, snd := b } ∈ List.sigma l₁ l₂ ↔ a ∈ l₁ ∧ b ∈ l₂ a
[PROOFSTEP]
simp [List.sigma, mem_bind, mem_map, exists_prop, exists_and_left, and_left_comm, exists_eq_left, heq_iff_eq,
  exists_eq_right]
[GOAL]
α : Type u_1
β : Type u_2
σ : α → Type u_3
l₁ : List α
l₂ : (a : α) → List (σ a)
⊢ length (List.sigma l₁ l₂) = sum (map (fun a => length (l₂ a)) l₁)
[PROOFSTEP]
induction' l₁ with x l₁ IH
[GOAL]
case nil
α : Type u_1
β : Type u_2
σ : α → Type u_3
l₂ : (a : α) → List (σ a)
⊢ length (List.sigma [] l₂) = sum (map (fun a => length (l₂ a)) [])
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u_1
β : Type u_2
σ : α → Type u_3
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₁))
[PROOFSTEP]
simp only [map, sigma_cons, length_append, length_map, IH, sum_cons]
