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