case h
α : Type u_1
α' : Type ?u.30846
β : Type u_2
β' : Type ?u.30852
γ : Type u_3
γ' : Type ?u.30858
δ : Type u_4
δ' : Type ?u.30864
ε : Type ?u.30867
ε' : Type ?u.30870
ζ : Type ?u.30873
ζ' : Type ?u.30876
ν : Type ?u.30879
f f' : α → β → γ
g g' : α → β → γ → δ
s s' : Set α
t t' : Set β
u u' : Set γ
v : Set δ
a a' : α
b b' : β
c c' : γ
d d' : δ
h : ∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → ∀ (c : γ), c ∈ u → g a b c = g' a b c
x : δ
⊢ x ∈ image3 g s t u ↔ x ∈ image3 g' s t u
α : Type u_1
α' : Type ?u.30846
β : Type u_2
β' : Type ?u.30852
γ : Type u_3
γ' : Type ?u.30858
δ : Type u_4
δ' : Type ?u.30864
ε : Type ?u.30867
ε' : Type ?u.30870
ζ : Type ?u.30873
ζ' : Type ?u.30876
ν : Type ?u.30879
f f' : α → β → γ
g g' : α → β → γ → δ
s s' : Set α
t t' : Set β
u u' : Set γ
v : Set δ
a a' : α
b b' : β
c c' : γ
d d' : δ
h : ∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → ∀ (c : γ), c ∈ u → g a b c = g' a b c
⊢ image3 g s t u = image3 g' s t u
ext x
no goals
case h
α : Type u_1
α' : Type ?u.30846
β : Type u_2
β' : Type ?u.30852
γ : Type u_3
γ' : Type ?u.30858
δ : Type u_4
δ' : Type ?u.30864
ε : Type ?u.30867
ε' : Type ?u.30870
ζ : Type ?u.30873
ζ' : Type ?u.30876
ν : Type ?u.30879
f f' : α → β → γ
g g' : α → β → γ → δ
s s' : Set α
t t' : Set β
u u' : Set γ
v : Set δ
a a' : α
b b' : β
c c' : γ
d d' : δ
h : ∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → ∀ (c : γ), c ∈ u → g a b c = g' a b c
x : δ
⊢ x ∈ image3 g s t u ↔ x ∈ image3 g' s t u
constructor <;> rintro ⟨a, b, c, ha, hb, hc, rfl⟩ <;>
  exact ⟨a, b, c, ha, hb, hc, by rw [h a ha b hb c hc]⟩
no goals
α : Type u_1
α' : Type ?u.30846
β : Type u_2
β' : Type ?u.30852
γ : Type u_3
γ' : Type ?u.30858
δ : Type u_4
δ' : Type ?u.30864
ε : Type ?u.30867
ε' : Type ?u.30870
ζ : Type ?u.30873
ζ' : Type ?u.30876
ν : Type ?u.30879
f f' : α → β → γ
g g' : α → β → γ → δ
s s' : Set α
t t' : Set β
u u' : Set γ
v : Set δ
a✝ a' : α
b✝ b' : β
c✝ c' : γ
d d' : δ
h : ∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → ∀ (c : γ), c ∈ u → g a b c = g' a b c
a : α
b : β
c : γ
ha : a ∈ s
hb : b ∈ t
hc : c ∈ u
⊢ g a b c = g' a b c
rw [h a ha b hb c hc]