α : 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_eq_map_coe, ← 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)