α : Type u_7
α' : Type ?u.76425
β : Type u_8
β' : Type ?u.76431
γ✝ : Type ?u.76434
γ' : Type ?u.76437
δ✝ : Type ?u.76440
δ' : Type ?u.76443
ε : Type u_6
ε' : Type u_9
ζ : Type u_3
ζ' : Type u_4
ν : Type u_5
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
δ : Type u_2
u : Finset γ
v : Finset δ
inst✝² : DecidableEq ζ
inst✝¹ : DecidableEq ζ'
inst✝ : DecidableEq ν
f : ε → ζ → ν
g : α → β → ε
h : γ → δ → ζ
f' : ε' → ζ' → ν
g' : α → γ → ε'
h' : β → δ → ζ'
h_comm : ∀ (a : α) (b : β) (c : γ) (d : δ), f (g a b) (h c d) = f' (g' a c) (h' b d)
⊢ image2 f (image2 g ↑s ↑t) (image2 h ↑u ↑v) = image2 f' (image2 g' ↑s ↑u) (image2 h' ↑t ↑v)
α : Type u_7
α' : Type ?u.76425
β : Type u_8
β' : Type ?u.76431
γ✝ : Type ?u.76434
γ' : Type ?u.76437
δ✝ : Type ?u.76440
δ' : Type ?u.76443
ε : Type u_6
ε' : Type u_9
ζ : Type u_3
ζ' : Type u_4
ν : Type u_5
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
δ : Type u_2
u : Finset γ
v : Finset δ
inst✝² : DecidableEq ζ
inst✝¹ : DecidableEq ζ'
inst✝ : DecidableEq ν
f : ε → ζ → ν
g : α → β → ε
h : γ → δ → ζ
f' : ε' → ζ' → ν
g' : α → γ → ε'
h' : β → δ → ζ'
h_comm : ∀ (a : α) (b : β) (c : γ) (d : δ), f (g a b) (h c d) = f' (g' a c) (h' b d)
⊢ ↑(image₂ f (image₂ g s t) (image₂ h u v)) = ↑(image₂ f' (image₂ g' s u) (image₂ h' t v))
push_cast
no goals
α : Type u_7
α' : Type ?u.76425
β : Type u_8
β' : Type ?u.76431
γ✝ : Type ?u.76434
γ' : Type ?u.76437
δ✝ : Type ?u.76440
δ' : Type ?u.76443
ε : Type u_6
ε' : Type u_9
ζ : Type u_3
ζ' : Type u_4
ν : Type u_5
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
δ : Type u_2
u : Finset γ
v : Finset δ
inst✝² : DecidableEq ζ
inst✝¹ : DecidableEq ζ'
inst✝ : DecidableEq ν
f : ε → ζ → ν
g : α → β → ε
h : γ → δ → ζ
f' : ε' → ζ' → ν
g' : α → γ → ε'
h' : β → δ → ζ'
h_comm : ∀ (a : α) (b : β) (c : γ) (d : δ), f (g a b) (h c d) = f' (g' a c) (h' b d)
⊢ image2 f (image2 g ↑s ↑t) (image2 h ↑u ↑v) = image2 f' (image2 g' ↑s ↑u) (image2 h' ↑t ↑v)
exact image2_image2_image2_comm h_comm