case a
α✝ β✝ : Type u
inst✝ : (P : Prop) → Decidable P
α β γ : Type u_1
f : α → β → γ
s : Finset α
t : Finset β
a✝ : γ
⊢ a✝ ∈ image₂ f s t ↔ a✝ ∈ Seq.seq (f <$> s) fun x => t
α✝ β✝ : Type u
inst✝ : (P : Prop) → Decidable P
α β γ : Type u_1
f : α → β → γ
s : Finset α
t : Finset β
⊢ image₂ f s t = Seq.seq (f <$> s) fun x => t
ext
no goals
case a
α✝ β✝ : Type u
inst✝ : (P : Prop) → Decidable P
α β γ : Type u_1
f : α → β → γ
s : Finset α
t : Finset β
a✝ : γ
⊢ a✝ ∈ image₂ f s t ↔ a✝ ∈ Seq.seq (f <$> s) fun x => t
simp [mem_sup]