case a
α : Type u_1
α' : Type ?u.62414
β : Type u_2
β' : Type ?u.62420
γ : Type ?u.62423
γ' : Type ?u.62426
δ : Type ?u.62429
δ' : Type ?u.62432
ε : Type ?u.62435
ε' : Type ?u.62438
ζ : Type ?u.62441
ζ' : Type ?u.62444
ν : Type ?u.62447
inst✝⁹ : DecidableEq α'
inst✝⁸ : DecidableEq β'
inst✝⁷ : DecidableEq γ
inst✝⁶ : DecidableEq γ'
inst✝⁵ : DecidableEq δ
inst✝⁴ : DecidableEq δ'
inst✝³ : DecidableEq ε
inst✝² : DecidableEq ε'
f f' : α → β → γ
g g' : α → β → γ → δ
s✝ s' : Finset α
t✝ t' : Finset β
u u' : Finset γ
a a' : α
b b' : β
c : γ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset α
t : Finset β
a✝ : α × β
⊢ a✝ ∈ image₂ Prod.mk s t ↔ a✝ ∈ s ×ˢ t
α : Type u_1
α' : Type ?u.62414
β : Type u_2
β' : Type ?u.62420
γ : Type ?u.62423
γ' : Type ?u.62426
δ : Type ?u.62429
δ' : Type ?u.62432
ε : Type ?u.62435
ε' : Type ?u.62438
ζ : Type ?u.62441
ζ' : Type ?u.62444
ν : Type ?u.62447
inst✝⁹ : DecidableEq α'
inst✝⁸ : DecidableEq β'
inst✝⁷ : DecidableEq γ
inst✝⁶ : DecidableEq γ'
inst✝⁵ : DecidableEq δ
inst✝⁴ : DecidableEq δ'
inst✝³ : DecidableEq ε
inst✝² : DecidableEq ε'
f f' : α → β → γ
g g' : α → β → γ → δ
s✝ s' : Finset α
t✝ t' : Finset β
u u' : Finset γ
a a' : α
b b' : β
c : γ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset α
t : Finset β
⊢ image₂ Prod.mk s t = s ×ˢ t
ext
no goals
case a
α : Type u_1
α' : Type ?u.62414
β : Type u_2
β' : Type ?u.62420
γ : Type ?u.62423
γ' : Type ?u.62426
δ : Type ?u.62429
δ' : Type ?u.62432
ε : Type ?u.62435
ε' : Type ?u.62438
ζ : Type ?u.62441
ζ' : Type ?u.62444
ν : Type ?u.62447
inst✝⁹ : DecidableEq α'
inst✝⁸ : DecidableEq β'
inst✝⁷ : DecidableEq γ
inst✝⁶ : DecidableEq γ'
inst✝⁵ : DecidableEq δ
inst✝⁴ : DecidableEq δ'
inst✝³ : DecidableEq ε
inst✝² : DecidableEq ε'
f f' : α → β → γ
g g' : α → β → γ → δ
s✝ s' : Finset α
t✝ t' : Finset β
u u' : Finset γ
a a' : α
b b' : β
c : γ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset α
t : Finset β
a✝ : α × β
⊢ a✝ ∈ image₂ Prod.mk s t ↔ a✝ ∈ s ×ˢ t
simp [Prod.ext_iff]