α : Type u_1
β : Type ?u.716493
inst✝¹ : DecidableEq α
l✝ : List α
x✝ : α
inst✝ : Fintype α
l l' : List α
x : α
hx : x ∈ support (prod (zipWith swap l l'))
⊢ x ∈ toFinset l ⊔ toFinset l'
α : Type u_1
β : Type ?u.716493
inst✝¹ : DecidableEq α
l✝ : List α
x : α
inst✝ : Fintype α
l l' : List α
⊢ support (prod (zipWith swap l l')) ≤ toFinset l ⊔ toFinset l'
intro x hx
α : Type u_1
β : Type ?u.716493
inst✝¹ : DecidableEq α
l✝ : List α
x✝ : α
inst✝ : Fintype α
l l' : List α
x : α
hx : x ∈ support (prod (zipWith swap l l'))
hx' : x ∈ {x | ↑(prod (zipWith swap l l')) x ≠ x}
⊢ x ∈ toFinset l ⊔ toFinset l'
α : Type u_1
β : Type ?u.716493
inst✝¹ : DecidableEq α
l✝ : List α
x✝ : α
inst✝ : Fintype α
l l' : List α
x : α
hx : x ∈ support (prod (zipWith swap l l'))
⊢ x ∈ toFinset l ⊔ toFinset l'
have hx' : x ∈ { x | (zipWith swap l l').prod x ≠ x } := by simpa using hx
no goals
α : Type u_1
β : Type ?u.716493
inst✝¹ : DecidableEq α
l✝ : List α
x✝ : α
inst✝ : Fintype α
l l' : List α
x : α
hx : x ∈ support (prod (zipWith swap l l'))
hx' : x ∈ {x | ↑(prod (zipWith swap l l')) x ≠ x}
⊢ x ∈ toFinset l ⊔ toFinset l'
simpa using zipWith_swap_prod_support' _ _ hx'
no goals
α : Type u_1
β : Type ?u.716493
inst✝¹ : DecidableEq α
l✝ : List α
x✝ : α
inst✝ : Fintype α
l l' : List α
x : α
hx : x ∈ support (prod (zipWith swap l l'))
⊢ x ∈ {x | ↑(prod (zipWith swap l l')) x ≠ x}
simpa using hx