case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_2
α' : Type ?u.46266
β : Type u_4
β' : Type u_6
γ : Type u_5
γ' : Type u_7
δ : Type u_3
δ' : Type ?u.46284
ε : Type u_1
ε' : Type ?u.46290
ζ : Type ?u.46293
ζ' : Type ?u.46296
ν : Type ?u.46299
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₁ : α → β → β'
f₂ : α → γ → γ'
g' : β' → γ' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' (f₁ a b) (f₂ a c)
a : α
ha : a ∈ s
b : β
c : γ
hb : b ∈ t
hc : c ∈ u
⊢ f a (g b c) ∈ image2 g' (image2 f₁ s t) (image2 f₂ s u)
α : Type u_2
α' : Type ?u.46266
β : Type u_4
β' : Type u_6
γ : Type u_5
γ' : Type u_7
δ : Type u_3
δ' : Type ?u.46284
ε : Type u_1
ε' : Type ?u.46290
ζ : Type ?u.46293
ζ' : Type ?u.46296
ν : Type ?u.46299
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₁ : α → β → β'
f₂ : α → γ → γ'
g' : β' → γ' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' (f₁ a b) (f₂ a c)
⊢ image2 f s (image2 g t u) ⊆ image2 g' (image2 f₁ s t) (image2 f₂ s u)
rintro _ ⟨a, _, ha, ⟨b, c, hb, hc, rfl⟩, rfl⟩
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_2
α' : Type ?u.46266
β : Type u_4
β' : Type u_6
γ : Type u_5
γ' : Type u_7
δ : Type u_3
δ' : Type ?u.46284
ε : Type u_1
ε' : Type ?u.46290
ζ : Type ?u.46293
ζ' : Type ?u.46296
ν : Type ?u.46299
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₁ : α → β → β'
f₂ : α → γ → γ'
g' : β' → γ' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' (f₁ a b) (f₂ a c)
a : α
ha : a ∈ s
b : β
c : γ
hb : b ∈ t
hc : c ∈ u
⊢ g' (f₁ a b) (f₂ a c) ∈ image2 g' (image2 f₁ s t) (image2 f₂ s u)
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_2
α' : Type ?u.46266
β : Type u_4
β' : Type u_6
γ : Type u_5
γ' : Type u_7
δ : Type u_3
δ' : Type ?u.46284
ε : Type u_1
ε' : Type ?u.46290
ζ : Type ?u.46293
ζ' : Type ?u.46296
ν : Type ?u.46299
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₁ : α → β → β'
f₂ : α → γ → γ'
g' : β' → γ' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' (f₁ a b) (f₂ a c)
a : α
ha : a ∈ s
b : β
c : γ
hb : b ∈ t
hc : c ∈ u
⊢ f a (g b c) ∈ image2 g' (image2 f₁ s t) (image2 f₂ s u)
rw [h_distrib]
no goals
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_2
α' : Type ?u.46266
β : Type u_4
β' : Type u_6
γ : Type u_5
γ' : Type u_7
δ : Type u_3
δ' : Type ?u.46284
ε : Type u_1
ε' : Type ?u.46290
ζ : Type ?u.46293
ζ' : Type ?u.46296
ν : Type ?u.46299
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₁ : α → β → β'
f₂ : α → γ → γ'
g' : β' → γ' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' (f₁ a b) (f₂ a c)
a : α
ha : a ∈ s
b : β
c : γ
hb : b ∈ t
hc : c ∈ u
⊢ g' (f₁ a b) (f₂ a c) ∈ image2 g' (image2 f₁ s t) (image2 f₂ s u)
exact mem_image2_of_mem (mem_image2_of_mem ha hb) (mem_image2_of_mem ha hc)