no goals
α : Type u_1
α' : Type ?u.65130
β : Type u_2
β' : Type ?u.65136
γ : Type u_3
γ' : Type ?u.65142
δ : Type ?u.65145
δ' : Type ?u.65148
ε : Type ?u.65151
ε' : Type ?u.65154
ζ : Type ?u.65157
ζ' : Type ?u.65160
ν : Type ?u.65163
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 : γ
f : α × β → γ
s : Finset α
t : Finset β
⊢ image₂ (curry f) s t = image f (s ×ˢ t)
classical rw [← image₂_mk_eq_product, image_image₂]; dsimp [curry]
α : Type u_1
α' : Type ?u.65130
β : Type u_2
β' : Type ?u.65136
γ : Type u_3
γ' : Type ?u.65142
δ : Type ?u.65145
δ' : Type ?u.65148
ε : Type ?u.65151
ε' : Type ?u.65154
ζ : Type ?u.65157
ζ' : Type ?u.65160
ν : Type ?u.65163
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 : γ
f : α × β → γ
s : Finset α
t : Finset β
⊢ image₂ (curry f) s t = image₂ (fun a b => f (a, b)) s t
α : Type u_1
α' : Type ?u.65130
β : Type u_2
β' : Type ?u.65136
γ : Type u_3
γ' : Type ?u.65142
δ : Type ?u.65145
δ' : Type ?u.65148
ε : Type ?u.65151
ε' : Type ?u.65154
ζ : Type ?u.65157
ζ' : Type ?u.65160
ν : Type ?u.65163
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 : γ
f : α × β → γ
s : Finset α
t : Finset β
⊢ image₂ (curry f) s t = image f (s ×ˢ t)
rw [← image₂_mk_eq_product, image_image₂]
no goals
α : Type u_1
α' : Type ?u.65130
β : Type u_2
β' : Type ?u.65136
γ : Type u_3
γ' : Type ?u.65142
δ : Type ?u.65145
δ' : Type ?u.65148
ε : Type ?u.65151
ε' : Type ?u.65154
ζ : Type ?u.65157
ζ' : Type ?u.65160
ν : Type ?u.65163
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 : γ
f : α × β → γ
s : Finset α
t : Finset β
⊢ image₂ (curry f) s t = image₂ (fun a b => f (a, b)) s t
dsimp [curry]