-- Mathlib/Data/Set/NAry.lean
theorem image2_image2_image2_comm {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)

Proof state:
case h.mpr
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
ε : Type u_9
ε' : Type u_10
ζ : Type u_11
ζ' : Type u_12
ν : Type u_13
s : Set α
t : Set β
u : Set γ
v : Set δ
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)
x✝ : ν
⊢ x✝ ∈ image2 f' (image2 g' s u) (image2 h' t v) → x✝ ∈ image2 f (image2 g s t) (image2 h u v)

Tactic:
rintro ⟨_, ⟨a, ha, c, hc, rfl⟩, _, ⟨b, hb, d, hd, rfl⟩, rfl⟩

Result:
case h.mpr.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
ε : Type u_9
ε' : Type u_10
ζ : Type u_11
ζ' : Type u_12
ν : Type u_13
s : Set α
t : Set β
u : Set γ
v : Set δ
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)
a : α
ha : a ∈ s
c : γ
hc : c ∈ u
b : β
hb : b ∈ t
d : δ
hd : d ∈ v
⊢ f' (g' a c) (h' b d) ∈ image2 f (image2 g s t) (image2 h u v)

Proof state:
case h.mp
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
ε : Type u_9
ε' : Type u_10
ζ : Type u_11
ζ' : Type u_12
ν : Type u_13
s : Set α
t : Set β
u : Set γ
v : Set δ
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)
x✝ : ν
⊢ x✝ ∈ image2 f (image2 g s t) (image2 h u v) → x✝ ∈ image2 f' (image2 g' s u) (image2 h' t v)

Tactic:
rintro ⟨_, ⟨a, ha, b, hb, rfl⟩, _, ⟨c, hc, d, hd, rfl⟩, rfl⟩

Result:
case h.mp.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
ε : Type u_9
ε' : Type u_10
ζ : Type u_11
ζ' : Type u_12
ν : Type u_13
s : Set α
t : Set β
u : Set γ
v : Set δ
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)
a : α
ha : a ∈ s
b : β
hb : b ∈ t
c : γ
hc : c ∈ u
d : δ
hd : d ∈ v
⊢ f (g a b) (h c d) ∈ image2 f' (image2 g' s u) (image2 h' t v)

Proof state:
case h.mpr.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
ε : Type u_9
ε' : Type u_10
ζ : Type u_11
ζ' : Type u_12
ν : Type u_13
s : Set α
t : Set β
u : Set γ
v : Set δ
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)
a : α
ha : a ∈ s
c : γ
hc : c ∈ u
b : β
hb : b ∈ t
d : δ
hd : d ∈ v
⊢ f' (g' a c) (h' b d) ∈ image2 f (image2 g s t) (image2 h u v)

Tactic:
exact ⟨_, ⟨a, ha, b, hb, rfl⟩, _, ⟨c, hc, d, hd, rfl⟩, h_comm _ _ _ _⟩

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
ε : Type u_9
ε' : Type u_10
ζ : Type u_11
ζ' : Type u_12
ν : Type u_13
s : Set α
t : Set β
u : Set γ
v : Set δ
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)
x✝ : ν
⊢ x✝ ∈ image2 f (image2 g s t) (image2 h u v) ↔ x✝ ∈ image2 f' (image2 g' s u) (image2 h' t v)

Tactic:
constructor

Result:
case h.mp
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
ε : Type u_9
ε' : Type u_10
ζ : Type u_11
ζ' : Type u_12
ν : Type u_13
s : Set α
t : Set β
u : Set γ
v : Set δ
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)
x✝ : ν
⊢ x✝ ∈ image2 f (image2 g s t) (image2 h u v) → x✝ ∈ image2 f' (image2 g' s u) (image2 h' t v)

case h.mpr
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
ε : Type u_9
ε' : Type u_10
ζ : Type u_11
ζ' : Type u_12
ν : Type u_13
s : Set α
t : Set β
u : Set γ
v : Set δ
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)
x✝ : ν
⊢ x✝ ∈ image2 f' (image2 g' s u) (image2 h' t v) → x✝ ∈ image2 f (image2 g s t) (image2 h u v)

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
ε : Type u_9
ε' : Type u_10
ζ : Type u_11
ζ' : Type u_12
ν : Type u_13
s : Set α
t : Set β
u : Set γ
v : Set δ
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)

Tactic:
ext

Result:
case h
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
ε : Type u_9
ε' : Type u_10
ζ : Type u_11
ζ' : Type u_12
ν : Type u_13
s : Set α
t : Set β
u : Set γ
v : Set δ
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)
x✝ : ν
⊢ x✝ ∈ image2 f (image2 g s t) (image2 h u v) ↔ x✝ ∈ image2 f' (image2 g' s u) (image2 h' t v)

Proof state:
case h.mp.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
ε : Type u_9
ε' : Type u_10
ζ : Type u_11
ζ' : Type u_12
ν : Type u_13
s : Set α
t : Set β
u : Set γ
v : Set δ
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)
a : α
ha : a ∈ s
b : β
hb : b ∈ t
c : γ
hc : c ∈ u
d : δ
hd : d ∈ v
⊢ f (g a b) (h c d) ∈ image2 f' (image2 g' s u) (image2 h' t v)

Tactic:
exact ⟨_, ⟨a, ha, c, hc, rfl⟩, _, ⟨b, hb, d, hd, rfl⟩, (h_comm _ _ _ _).symm⟩

Result:
no goals