α : Type u_1
l : List α
x : Multiset α × Multiset α
h : ∃ a, a ∈ revzip (sublists' l) ∧ Prod.map ofList ofList a = x
⊢ x.fst + x.snd = ↑l
α : Type u_1
l : List α
x : Multiset α × Multiset α
h : x ∈ revzip (powersetAux' l)
⊢ x.fst + x.snd = ↑l
rw [revzip, powersetAux', ← map_reverse, zip_map, ← revzip, List.mem_map] at h
α : Type u_1
l : List α
x : Multiset α × Multiset α
h : ∃ a b, (a, b) ∈ revzip (sublists' l) ∧ (↑a, ↑b) = x
⊢ x.fst + x.snd = ↑l
α : Type u_1
l : List α
x : Multiset α × Multiset α
h : ∃ a, a ∈ revzip (sublists' l) ∧ Prod.map ofList ofList a = x
⊢ x.fst + x.snd = ↑l
simp only [Prod_map, Prod.exists] at h
case intro.intro.intro.refl
α : Type u_1
l l₁ l₂ : List α
h : (l₁, l₂) ∈ revzip (sublists' l)
⊢ (↑l₁, ↑l₂).fst + (↑l₁, ↑l₂).snd = ↑l
α : Type u_1
l : List α
x : Multiset α × Multiset α
h : ∃ a b, (a, b) ∈ revzip (sublists' l) ∧ (↑a, ↑b) = x
⊢ x.fst + x.snd = ↑l
rcases h with ⟨l₁, l₂, h, rfl, rfl⟩
no goals
case intro.intro.intro.refl
α : Type u_1
l l₁ l₂ : List α
h : (l₁, l₂) ∈ revzip (sublists' l)
⊢ (↑l₁, ↑l₂).fst + (↑l₁, ↑l₂).snd = ↑l
exact Quot.sound (revzip_sublists' _ _ _ h)