α : Type u_4
α' : Type ?u.41691
β : Type u_5
β' : Type ?u.41697
γ : Type u_3
γ' : Type ?u.41703
δ : Type u_2
δ' : Type u_6
ε : Type u_1
ε' : Type ?u.41715
ζ : Type ?u.41718
ζ' : Type ?u.41721
ν : Type ?u.41724
f✝ f'✝ : α → β → γ
g✝ g'✝ : α → β → γ → δ
s s' : Set α
t t' : Set β
u u' : Set γ
v : Set δ
a a' : α
b b' : β
c c' : γ
d d' : δ
f : δ → γ → ε
g : α → β → δ
f' : α → γ → δ'
g' : δ' → β → ε
h_right_comm : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b
⊢ image2 f (image2 (fun a b => g b a) t s) u = image2 (fun a b => g' b a) t (image2 f' s u)
α : Type u_4
α' : Type ?u.41691
β : Type u_5
β' : Type ?u.41697
γ : Type u_3
γ' : Type ?u.41703
δ : Type u_2
δ' : Type u_6
ε : Type u_1
ε' : Type ?u.41715
ζ : Type ?u.41718
ζ' : Type ?u.41721
ν : Type ?u.41724
f✝ f'✝ : α → β → γ
g✝ g'✝ : α → β → γ → δ
s s' : Set α
t t' : Set β
u u' : Set γ
v : Set δ
a a' : α
b b' : β
c c' : γ
d d' : δ
f : δ → γ → ε
g : α → β → δ
f' : α → γ → δ'
g' : δ' → β → ε
h_right_comm : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b
⊢ image2 f (image2 g s t) u = image2 g' (image2 f' s u) t
rw [image2_swap g, image2_swap g']
no goals
α : Type u_4
α' : Type ?u.41691
β : Type u_5
β' : Type ?u.41697
γ : Type u_3
γ' : Type ?u.41703
δ : Type u_2
δ' : Type u_6
ε : Type u_1
ε' : Type ?u.41715
ζ : Type ?u.41718
ζ' : Type ?u.41721
ν : Type ?u.41724
f✝ f'✝ : α → β → γ
g✝ g'✝ : α → β → γ → δ
s s' : Set α
t t' : Set β
u u' : Set γ
v : Set δ
a a' : α
b b' : β
c c' : γ
d d' : δ
f : δ → γ → ε
g : α → β → δ
f' : α → γ → δ'
g' : δ' → β → ε
h_right_comm : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b
⊢ image2 f (image2 (fun a b => g b a) t s) u = image2 (fun a b => g' b a) t (image2 f' s u)
exact image2_assoc fun _ _ _ => h_right_comm _ _ _