-- Mathlib/Order/Filter/NAry.lean
theorem map₂_distrib_le_right {m : δ → γ → ε} {n : α → β → δ} {m₁ : α → γ → α'} {m₂ : β → γ → β'}
    {n' : α' → β' → ε} (h_distrib : ∀ a b c, m (n a b) c = n' (m₁ a c) (m₂ b c)) :
    map₂ m (map₂ n f g) h ≤ map₂ n' (map₂ m₁ f h) (map₂ m₂ g h)

Proof state:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
ε : Type u_9
f : Filter α
g : Filter β
h : Filter γ
m : δ → γ → ε
n : α → β → δ
m₁ : α → γ → α'
m₂ : β → γ → β'
n' : α' → β' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), m (n a b) c = n' (m₁ a c) (m₂ b c)
⊢ map₂ m (map₂ n f g) h ≤ map₂ n' (map₂ m₁ f h) (map₂ m₂ g h)

Tactic:
rintro s ⟨t₁, ⟨u, hu, w₁, hw₁, ht₁⟩, t₂, ⟨v, hv, w₂, hw₂, ht₂⟩, hs⟩

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
ε : Type u_9
f : Filter α
g : Filter β
h : Filter γ
m : δ → γ → ε
n : α → β → δ
m₁ : α → γ → α'
m₂ : β → γ → β'
n' : α' → β' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), m (n a b) c = n' (m₁ a c) (m₂ b c)
s : Set ε
t₁ : Set α'
u : Set α
hu : u ∈ f
w₁ : Set γ
hw₁ : w₁ ∈ h
ht₁ : image2 m₁ u w₁ ⊆ t₁
t₂ : Set β'
hs : image2 n' t₁ t₂ ⊆ s
v : Set β
hv : v ∈ g
w₂ : Set γ
hw₂ : w₂ ∈ h
ht₂ : image2 m₂ v w₂ ⊆ t₂
⊢ s ∈ map₂ m (map₂ n f g) h

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
ε : Type u_9
f : Filter α
g : Filter β
h : Filter γ
m : δ → γ → ε
n : α → β → δ
m₁ : α → γ → α'
m₂ : β → γ → β'
n' : α' → β' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), m (n a b) c = n' (m₁ a c) (m₂ b c)
s : Set ε
t₁ : Set α'
u : Set α
hu : u ∈ f
w₁ : Set γ
hw₁ : w₁ ∈ h
ht₁ : image2 m₁ u w₁ ⊆ t₁
t₂ : Set β'
hs : image2 n' t₁ t₂ ⊆ s
v : Set β
hv : v ∈ g
w₂ : Set γ
hw₂ : w₂ ∈ h
ht₂ : image2 m₂ v w₂ ⊆ t₂
⊢ image2 m (image2 n u v) (w₁ ∩ w₂) ⊆ s

Tactic:
refine (image2_distrib_subset_right h_distrib).trans ((image2_subset ?_ ?_).trans hs)

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
ε : Type u_9
f : Filter α
g : Filter β
h : Filter γ
m : δ → γ → ε
n : α → β → δ
m₁ : α → γ → α'
m₂ : β → γ → β'
n' : α' → β' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), m (n a b) c = n' (m₁ a c) (m₂ b c)
s : Set ε
t₁ : Set α'
u : Set α
hu : u ∈ f
w₁ : Set γ
hw₁ : w₁ ∈ h
ht₁ : image2 m₁ u w₁ ⊆ t₁
t₂ : Set β'
hs : image2 n' t₁ t₂ ⊆ s
v : Set β
hv : v ∈ g
w₂ : Set γ
hw₂ : w₂ ∈ h
ht₂ : image2 m₂ v w₂ ⊆ t₂
⊢ image2 m₁ u (w₁ ∩ w₂) ⊆ t₁

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
ε : Type u_9
f : Filter α
g : Filter β
h : Filter γ
m : δ → γ → ε
n : α → β → δ
m₁ : α → γ → α'
m₂ : β → γ → β'
n' : α' → β' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), m (n a b) c = n' (m₁ a c) (m₂ b c)
s : Set ε
t₁ : Set α'
u : Set α
hu : u ∈ f
w₁ : Set γ
hw₁ : w₁ ∈ h
ht₁ : image2 m₁ u w₁ ⊆ t₁
t₂ : Set β'
hs : image2 n' t₁ t₂ ⊆ s
v : Set β
hv : v ∈ g
w₂ : Set γ
hw₂ : w₂ ∈ h
ht₂ : image2 m₂ v w₂ ⊆ t₂
⊢ image2 m₂ v (w₁ ∩ w₂) ⊆ t₂

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
ε : Type u_9
f : Filter α
g : Filter β
h : Filter γ
m : δ → γ → ε
n : α → β → δ
m₁ : α → γ → α'
m₂ : β → γ → β'
n' : α' → β' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), m (n a b) c = n' (m₁ a c) (m₂ b c)
s : Set ε
t₁ : Set α'
u : Set α
hu : u ∈ f
w₁ : Set γ
hw₁ : w₁ ∈ h
ht₁ : image2 m₁ u w₁ ⊆ t₁
t₂ : Set β'
hs : image2 n' t₁ t₂ ⊆ s
v : Set β
hv : v ∈ g
w₂ : Set γ
hw₂ : w₂ ∈ h
ht₂ : image2 m₂ v w₂ ⊆ t₂
⊢ image2 m₁ u (w₁ ∩ w₂) ⊆ t₁

Tactic:
exact (image2_subset_left inter_subset_left).trans ht₁

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
ε : Type u_9
f : Filter α
g : Filter β
h : Filter γ
m : δ → γ → ε
n : α → β → δ
m₁ : α → γ → α'
m₂ : β → γ → β'
n' : α' → β' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), m (n a b) c = n' (m₁ a c) (m₂ b c)
s : Set ε
t₁ : Set α'
u : Set α
hu : u ∈ f
w₁ : Set γ
hw₁ : w₁ ∈ h
ht₁ : image2 m₁ u w₁ ⊆ t₁
t₂ : Set β'
hs : image2 n' t₁ t₂ ⊆ s
v : Set β
hv : v ∈ g
w₂ : Set γ
hw₂ : w₂ ∈ h
ht₂ : image2 m₂ v w₂ ⊆ t₂
⊢ s ∈ map₂ m (map₂ n f g) h

Tactic:
refine ⟨_, image2_mem_map₂ hu hv, w₁ ∩ w₂, inter_mem hw₁ hw₂, ?_⟩

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
ε : Type u_9
f : Filter α
g : Filter β
h : Filter γ
m : δ → γ → ε
n : α → β → δ
m₁ : α → γ → α'
m₂ : β → γ → β'
n' : α' → β' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), m (n a b) c = n' (m₁ a c) (m₂ b c)
s : Set ε
t₁ : Set α'
u : Set α
hu : u ∈ f
w₁ : Set γ
hw₁ : w₁ ∈ h
ht₁ : image2 m₁ u w₁ ⊆ t₁
t₂ : Set β'
hs : image2 n' t₁ t₂ ⊆ s
v : Set β
hv : v ∈ g
w₂ : Set γ
hw₂ : w₂ ∈ h
ht₂ : image2 m₂ v w₂ ⊆ t₂
⊢ image2 m (image2 n u v) (w₁ ∩ w₂) ⊆ s

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
ε : Type u_9
f : Filter α
g : Filter β
h : Filter γ
m : δ → γ → ε
n : α → β → δ
m₁ : α → γ → α'
m₂ : β → γ → β'
n' : α' → β' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), m (n a b) c = n' (m₁ a c) (m₂ b c)
s : Set ε
t₁ : Set α'
u : Set α
hu : u ∈ f
w₁ : Set γ
hw₁ : w₁ ∈ h
ht₁ : image2 m₁ u w₁ ⊆ t₁
t₂ : Set β'
hs : image2 n' t₁ t₂ ⊆ s
v : Set β
hv : v ∈ g
w₂ : Set γ
hw₂ : w₂ ∈ h
ht₂ : image2 m₂ v w₂ ⊆ t₂
⊢ image2 m₂ v (w₁ ∩ w₂) ⊆ t₂

Tactic:
exact (image2_subset_left inter_subset_right).trans ht₂

Result:
no goals