α : Type u_4
α' : Type u_6
β : Type u_5
β' : Type u_7
γ✝ : Type ?u.89133
γ' : Type ?u.89136
δ : Type u_3
δ' : Type ?u.89142
ε : Type u_2
ε' : Type ?u.89148
ζ : Type ?u.89151
ζ' : Type ?u.89154
ν : Type ?u.89157
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 : γ✝
γ : Type u_1
u : Finset γ
f : δ → γ → ε
g : α → β → δ
f₁ : α → γ → α'
f₂ : β → γ → β'
g' : α' → β' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f₁ a c) (f₂ b c)
⊢ image2 f (image2 g ↑s ↑t) ↑u ⊆ image2 g' (image2 f₁ ↑s ↑u) (image2 f₂ ↑t ↑u)
α : Type u_4
α' : Type u_6
β : Type u_5
β' : Type u_7
γ✝ : Type ?u.89133
γ' : Type ?u.89136
δ : Type u_3
δ' : Type ?u.89142
ε : Type u_2
ε' : Type ?u.89148
ζ : Type ?u.89151
ζ' : Type ?u.89154
ν : Type ?u.89157
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 : γ✝
γ : Type u_1
u : Finset γ
f : δ → γ → ε
g : α → β → δ
f₁ : α → γ → α'
f₂ : β → γ → β'
g' : α' → β' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f₁ a c) (f₂ b c)
⊢ ↑(image₂ f (image₂ g s t) u) ⊆ ↑(image₂ g' (image₂ f₁ s u) (image₂ f₂ t u))
push_cast
no goals
α : Type u_4
α' : Type u_6
β : Type u_5
β' : Type u_7
γ✝ : Type ?u.89133
γ' : Type ?u.89136
δ : Type u_3
δ' : Type ?u.89142
ε : Type u_2
ε' : Type ?u.89148
ζ : Type ?u.89151
ζ' : Type ?u.89154
ν : Type ?u.89157
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 : γ✝
γ : Type u_1
u : Finset γ
f : δ → γ → ε
g : α → β → δ
f₁ : α → γ → α'
f₂ : β → γ → β'
g' : α' → β' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f₁ a c) (f₂ b c)
⊢ image2 f (image2 g ↑s ↑t) ↑u ⊆ image2 g' (image2 f₁ ↑s ↑u) (image2 f₂ ↑t ↑u)
exact Set.image2_distrib_subset_right h_distrib