α : Type u_1
β : Type u_2
γ : Type ?u.274965
ι : Sort ?u.274968
ι' : Sort ?u.274971
ι₂ : Sort ?u.274974
κ : ι → Sort ?u.274979
κ₁ : ι → Sort ?u.274984
κ₂ : ι → Sort ?u.274989
κ' : ι' → Sort ?u.274994
s : Set α
t : Set β
⊢ seq ((fun x x_1 => x ∘ x_1) Prod.swap ∘ Prod.mk '' t) s = seq ((fun b a => (a, b)) '' t) s
α : Type u_1
β : Type u_2
γ : Type ?u.274965
ι : Sort ?u.274968
ι' : Sort ?u.274971
ι₂ : Sort ?u.274974
κ : ι → Sort ?u.274979
κ₁ : ι → Sort ?u.274984
κ₂ : ι → Sort ?u.274989
κ' : ι' → Sort ?u.274994
s : Set α
t : Set β
⊢ seq (Prod.mk '' s) t = seq ((fun b a => (a, b)) '' t) s
rw [← prod_eq_seq, ← image_swap_prod, prod_eq_seq, image_seq, ← image_comp]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.274965
ι : Sort ?u.274968
ι' : Sort ?u.274971
ι₂ : Sort ?u.274974
κ : ι → Sort ?u.274979
κ₁ : ι → Sort ?u.274984
κ₂ : ι → Sort ?u.274989
κ' : ι' → Sort ?u.274994
s : Set α
t : Set β
⊢ seq ((fun x x_1 => x ∘ x_1) Prod.swap ∘ Prod.mk '' t) s = seq ((fun b a => (a, b)) '' t) s
rfl