awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
g₁ g₂ : Filter β
h : g₁ ≤ g₂
⊢ map₂ m f g₁ ≤ map₂ m f g₂

Tactic:
map₂_mono Subset.rfl h

Premises used: Set.Subset.rfl, Filter.map₂_mono
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f₁ f₂ : Filter α
g : Filter β
h : f₁ ≤ f₂
⊢ map₂ m f₁ g ≤ map₂ m f₂ g

Tactic:
map₂_mono h Subset.rfl

Premises used: Set.Subset.rfl, Filter.map₂_mono
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
g : Filter β
h : Filter γ
⊢ h ≤ map₂ m f g ↔ ∀ ⦃s : Set α⦄, s ∈ f → ∀ ⦃t : Set β⦄, t ∈ g → image2 m s t ∈ h

Tactic:
⟨fun H _ hs _ ht => H <| image2_mem_map₂ hs ht, fun H _ ⟨_, hs, _, ht, hu⟩ =>
    mem_of_superset (H hs ht) hu⟩

Premises used: Filter.image2_mem_map₂, _private.0.Filter.le_map₂_iff.match_1, Membership.mem, Iff.intro, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
g : Filter β
⊢ map₂ m f g = ⊥ ↔ f = ⊥ ∨ g = ⊥

Tactic:
simp [← map_prod_eq_map₂]

Premises used: Filter.map_prod_eq_map₂
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
g : Filter β
⊢ map₂ m ⊥ g = ⊥

Tactic:
map₂_eq_bot_iff.2 <| .inl rfl

Premises used: Iff.mpr, Filter.map₂_eq_bot_iff, Or.inl, rfl
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
⊢ map₂ m f ⊥ = ⊥

Tactic:
map₂_eq_bot_iff.2 <| .inr rfl

Premises used: Iff.mpr, Filter.map₂_eq_bot_iff, Or.inr, rfl
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
g : Filter β
⊢ (map₂ m f g).NeBot ↔ f.NeBot ∧ g.NeBot

Tactic:
simp [neBot_iff, not_or]

Premises used: Filter.neBot_iff, not_or
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
g : Filter β
hf : f.NeBot
hg : g.NeBot
⊢ (map₂ m f g).NeBot

Tactic:
map₂_neBot_iff.2 ⟨hf, hg⟩

Premises used: Iff.mpr, Filter.map₂_neBot_iff, And.intro
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m : α → β → γ
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h : Filter γ
s : Set α
t : Set β
u : Set γ
a : α
b : β
inst : f.NeBot
inst_1 : g.NeBot
⊢ (map₂ m f g).NeBot

Tactic:
.map₂ ‹_› ‹_›

Premises used: Filter.NeBot.map₂
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
g : Filter β
h : (map₂ m f g).NeBot
⊢ f.NeBot

Tactic:
(map₂_neBot_iff.1 h).1

Premises used: Filter.map₂_neBot_iff, And.left, Iff.mp
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
g : Filter β
h : (map₂ m f g).NeBot
⊢ g.NeBot

Tactic:
(map₂_neBot_iff.1 h).2

Premises used: Filter.map₂_neBot_iff, And.right, Iff.mp
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f₁ f₂ : Filter α
g : Filter β
simp_rw :
  Eq.{u_5 + 1} (α := Filter γ) (map (fun (p : α × β) ↦ m p.1 p.2) ((f₁ ⊔ f₂) ×ˢ g))
    (map (fun (p : α × β) ↦ m p.1 p.2) (f₁ ×ˢ g) ⊔ map (fun (p : α × β) ↦ m p.1 p.2) (f₂ ×ˢ g))
simp_rw₁ :
  Eq.{u_5 + 1} (α := Filter γ) (map (fun (p : α × β) ↦ m p.1 p.2) (f₁ ×ˢ g ⊔ f₂ ×ˢ g))
    (map (fun (p : α × β) ↦ m p.1 p.2) (f₁ ×ˢ g) ⊔ map (fun (p : α × β) ↦ m p.1 p.2) (f₂ ×ˢ g))
⊢ map₂ m (f₁ ⊔ f₂) g = map₂ m f₁ g ⊔ map₂ m f₂ g

Tactic:
simp_rw [← map_prod_eq_map₂, sup_prod, map_sup]

Premises used: Filter.map_sup, Filter.map_prod_eq_map₂, Filter.sup_prod
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
g₁ g₂ : Filter β
simp_rw :
  Eq.{u_5 + 1} (α := Filter γ) (map (fun (p : α × β) ↦ m p.1 p.2) (f ×ˢ (g₁ ⊔ g₂)))
    (map (fun (p : α × β) ↦ m p.1 p.2) (f ×ˢ g₁) ⊔ map (fun (p : α × β) ↦ m p.1 p.2) (f ×ˢ g₂))
simp_rw₁ :
  Eq.{u_5 + 1} (α := Filter γ) (map (fun (p : α × β) ↦ m p.1 p.2) (f ×ˢ g₁ ⊔ f ×ˢ g₂))
    (map (fun (p : α × β) ↦ m p.1 p.2) (f ×ˢ g₁) ⊔ map (fun (p : α × β) ↦ m p.1 p.2) (f ×ˢ g₂))
⊢ map₂ m f (g₁ ⊔ g₂) = map₂ m f g₁ ⊔ map₂ m f g₂

Tactic:
simp_rw [← map_prod_eq_map₂, prod_sup, map_sup]

Premises used: Filter.map_sup, Filter.map_prod_eq_map₂, Filter.prod_sup
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f₁ f₂ : Filter α
g : Filter β
⊢ map₂ m (f₁ ⊓ f₂) g ≤ map₂ m f₁ g ⊓ map₂ m f₂ g

Tactic:
Monotone.map_inf_le (fun _ _ ↦ map₂_mono_right) f₁ f₂

Premises used: Set.Mem, setOf, Filter.map₂_mono_right, Monotone.map_inf_le
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
g₁ g₂ : Filter β
⊢ map₂ m f (g₁ ⊓ g₂) ≤ map₂ m f g₁ ⊓ map₂ m f g₂

Tactic:
Monotone.map_inf_le (fun _ _ ↦ map₂_mono_left) g₁ g₂

Premises used: Set.Mem, setOf, Monotone.map_inf_le, Filter.map₂_mono_left
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
g : Filter β
a : α
rw : map ((fun (p : α × β) ↦ m p.1 p.2) ∘ Prod.mk a) g = map (m a) g
⊢ map₂ m (pure a) g = map (m a) g

Tactic:
rw [← map_prod_eq_map₂, pure_prod, map_map]

Premises used: Filter.map_map, Filter.pure_prod, Filter.map_prod_eq_map₂
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
g : Filter β
a : α
⊢ map ((fun (p : α × β) ↦ m p.1 p.2) ∘ Prod.mk a) g = map (m a) g

Tactic:
rfl
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
b : β
rw :
  Eq.{u_5 + 1} (α := Filter γ) (map ((fun (p : α × β) ↦ m p.1 p.2) ∘ fun (a : α) ↦ (a, b)) f)
    (map (fun (x : α) ↦ m x b) f)
⊢ map₂ m f (pure b) = map (fun (x : α) ↦ m x b) f

Tactic:
rw [← map_prod_eq_map₂, prod_pure, map_map]

Premises used: Filter.map_map, Filter.map_prod_eq_map₂, Filter.prod_pure
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
b : β
⊢ Eq.{u_5 + 1} (α := Filter γ) (map ((fun (p : α × β) ↦ m p.1 p.2) ∘ fun (a : α) ↦ (a, b)) f)
    (map (fun (x : α) ↦ m x b) f)

Tactic:
rfl
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
a : α
b : β
rw : map (fun (x : α) ↦ m x b) (pure a) = pure (m a b)
rw₁ rw₂ : Eq (α := Filter γ) (pure (m a b)) (pure (m a b))
⊢ map₂ m (pure a) (pure b) = pure (m a b)

Tactic:
rw [map₂_pure_right, map_pure]

Premises used: Filter.map₂_pure_right, Filter.map_pure
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
g : Filter β
rw :
  Eq.{u_5 + 1} (α := Filter γ) (map (fun (x : β × α) ↦ m x.swap.1 x.swap.2) (g ×ˢ f))
    (map (fun (p : β × α) ↦ m p.2 p.1) (g ×ˢ f))
⊢ map₂ m f g = map₂ (fun (a : β) (b : α) ↦ m b a) g f

Tactic:
rw [← map_prod_eq_map₂, prod_comm, map_map, ← map_prod_eq_map₂, Function.comp_def]

Premises used: Filter.map_map, Filter.prod_comm, Filter.map_prod_eq_map₂, Function.comp_def
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
g : Filter β
⊢ Eq.{u_5 + 1} (α := Filter γ) (map (fun (x : β × α) ↦ m x.swap.1 x.swap.2) (g ×ˢ f))
    (map (fun (p : β × α) ↦ m p.2 p.1) (g ×ˢ f))

Tactic:
simp
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
β : Type u_3
f : Filter α
g : Filter β
inst : g.NeBot
rw : map (fun (p : α × β) ↦ p.1) (f ×ˢ g) = f
rw₁ rw₂ : f = f
⊢ map₂ (fun (x : α) (x_1 : β) ↦ x) f g = f

Tactic:
rw [← map_prod_eq_map₂, map_fst_prod]

Premises used: Filter.map_prod_eq_map₂, Filter.map_fst_prod
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
β : Type u_3
f : Filter α
g : Filter β
inst : f.NeBot
rw : map₂ (fun (a : β) (b : α) ↦ a) g f = g
rw₁ rw₂ : g = g
⊢ map₂ (fun (x : α) (y : β) ↦ y) f g = g

Tactic:
rw [map₂_swap, map₂_left]

Premises used: Filter.map₂_left, Filter.map₂_swap
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
f : Filter α
g : Filter β
m : α → β → γ
n : γ → δ
rw : map (n ∘ fun (p : α × β) ↦ m p.1 p.2) (f ×ˢ g) = map (fun (p : α × β) ↦ n (m p.1 p.2)) (f ×ˢ g)
⊢ map n (map₂ m f g) = map₂ (fun (a : α) (b : β) ↦ n (m a b)) f g

Tactic:
rw [← map_prod_eq_map₂, ← map_prod_eq_map₂, map_map]

Premises used: Filter.map_map, Filter.map_prod_eq_map₂
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
f : Filter α
g : Filter β
m : α → β → γ
n : γ → δ
⊢ map (n ∘ fun (p : α × β) ↦ m p.1 p.2) (f ×ˢ g) = map (fun (p : α × β) ↦ n (m p.1 p.2)) (f ×ˢ g)

Tactic:
rfl
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
f : Filter α
g : Filter β
m : γ → β → δ
n : α → γ
rw :
  Eq.{u_7 + 1} (α := Filter δ) (map ((fun (p : γ × β) ↦ m p.1 p.2) ∘ fun (p : α × β) ↦ (n p.1, id p.2)) (f ×ˢ g))
    (map (fun (p : α × β) ↦ m (n p.1) p.2) (f ×ˢ g))
⊢ map₂ m (map n f) g = map₂ (fun (a : α) (b : β) ↦ m (n a) b) f g

Tactic:
rw [← map_prod_eq_map₂, ← map_prod_eq_map₂, ← @map_id _ g, prod_map_map_eq, map_map, map_id]

Premises used: Filter.map_map, Filter.map_prod_eq_map₂, Filter.map_id, Filter.prod_map_map_eq
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
f : Filter α
g : Filter β
m : γ → β → δ
n : α → γ
⊢ Eq.{u_7 + 1} (α := Filter δ) (map ((fun (p : γ × β) ↦ m p.1 p.2) ∘ fun (p : α × β) ↦ (n p.1, id p.2)) (f ×ˢ g))
    (map (fun (p : α × β) ↦ m (n p.1) p.2) (f ×ˢ g))

Tactic:
rfl
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
f : Filter α
g : Filter β
m : α → γ → δ
n : β → γ
rw :
  Eq.{u_7 + 1} (α := Filter δ) (map₂ (fun (a : γ) (b : α) ↦ m b a) (map n g) f)
    (map₂ (fun (a : α) (b : β) ↦ m a (n b)) f g)
rw₁ :
  Eq.{u_7 + 1} (α := Filter δ) (map₂ (fun (a : β) (b : α) ↦ m b (n a)) g f) (map₂ (fun (a : α) (b : β) ↦ m a (n b)) f g)
rw₂ rw₃ :
  Eq.{u_7 + 1} (α := Filter δ) (map₂ (fun (a : α) (b : β) ↦ m a (n b)) f g) (map₂ (fun (a : α) (b : β) ↦ m a (n b)) f g)
⊢ map₂ m f (map n g) = map₂ (fun (a : α) (b : β) ↦ m a (n b)) f g

Tactic:
rw [map₂_swap, map₂_map_left, map₂_swap]

Premises used: Filter.map₂_map_left, Filter.map₂_swap
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α × β → γ
f : Filter α
g : Filter β
⊢ map₂ (Function.curry m) f g = map m (f ×ˢ g)

Tactic:
(map_prod_eq_map₂' _ _ _).symm

Premises used: Filter.map_prod_eq_map₂', Eq.symm
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
g : Filter β
⊢ map (uncurry m) (f ×ˢ g) = map₂ m f g

Tactic:
(map₂_curry (uncurry m) f g).symm

Premises used: Filter.map₂_curry, Function.uncurry, Eq.symm
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
ε : Type u_9
ε' : Type u_10
f : Filter α
g : Filter β
m : δ → γ → ε
n : α → β → δ
m' : α → ε' → ε
n' : β → γ → ε'
h : Filter γ
h_assoc : ∀ (a : α) (b : β) (c : γ), m (n a b) c = m' a (n' b c)
rw :
  Eq.{u_9 + 1} (α := Filter ε) (map (fun (p : (α × β) × γ) ↦ m (n p.1.1 p.1.2) p.2) ((f ×ˢ g) ×ˢ h))
    (map ((fun (p : α × β × γ) ↦ m' p.1 (n' p.2.1 p.2.2)) ∘ (⇑(Equiv.prodAssoc α β γ) : (a : (α × β) × γ) → α × β × γ))
      ((f ×ˢ g) ×ˢ h))
⊢ map₂ m (map₂ n f g) h = map₂ m' f (map₂ n' g h)

Tactic:
rw [← map_prod_eq_map₂ n, ← map_prod_eq_map₂ n', map₂_map_left, map₂_map_right,
    ← map_prod_eq_map₂, ← map_prod_eq_map₂, ← prod_assoc, map_map]

Premises used: Filter.map₂_map_right, Filter.map₂_map_left, Filter.map_map, Filter.map_prod_eq_map₂, Filter.prod_assoc
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
ε : Type u_9
ε' : Type u_10
f : Filter α
g : Filter β
m : δ → γ → ε
n : α → β → δ
m' : α → ε' → ε
n' : β → γ → ε'
h : Filter γ
h_assoc : ∀ (a : α) (b : β) (c : γ), m (n a b) c = m' a (n' b c)
⊢ Eq.{u_9 + 1} (α := Filter ε) (map (fun (p : (α × β) × γ) ↦ m (n p.1.1 p.1.2) p.2) ((f ×ˢ g) ×ˢ h))
    (map ((fun (p : α × β × γ) ↦ m' p.1 (n' p.2.1 p.2.2)) ∘ (⇑(Equiv.prodAssoc α β γ) : (a : (α × β) × γ) → α × β × γ))
      ((f ×ˢ g) ×ˢ h))

Tactic:
simp only [h_assoc, Function.comp_def, Equiv.prodAssoc_apply]

Premises used: Equiv.prodAssoc_apply, Function.comp_def
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
g : Filter β
n : β → α → γ
h_comm : ∀ (a : α) (b : β), m a b = n b a
⊢ map₂ (fun (a : β) (b : α) ↦ m b a) g f = map₂ n g f

Tactic:
simp_rw [h_comm]
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
δ' : Type u_8
ε : Type u_9
f : Filter α
g : Filter β
h : Filter γ
m : α → δ → ε
n : β → γ → δ
m' : α → γ → δ'
n' : β → δ' → ε
h_left_comm : ∀ (a : α) (b : β) (c : γ), m a (n b c) = n' b (m' a c)
rw : map₂ (fun (a : δ) (b : α) ↦ m b a) (map₂ n g h) f = map₂ n' g (map₂ (fun (a : γ) (b : α) ↦ m' b a) h f)
⊢ map₂ m f (map₂ n g h) = map₂ n' g (map₂ m' f h)

Tactic:
rw [map₂_swap m', map₂_swap m]

Premises used: Filter.map₂_swap
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
δ' : Type u_8
ε : Type u_9
f : Filter α
g : Filter β
h : Filter γ
m : α → δ → ε
n : β → γ → δ
m' : α → γ → δ'
n' : β → δ' → ε
h_left_comm : ∀ (a : α) (b : β) (c : γ), m a (n b c) = n' b (m' a c)
⊢ map₂ (fun (a : δ) (b : α) ↦ m b a) (map₂ n g h) f = map₂ n' g (map₂ (fun (a : γ) (b : α) ↦ m' b a) h f)

Tactic:
map₂_assoc fun _ _ _ => h_left_comm _ _ _

Premises used: Filter.map₂_assoc
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
δ' : Type u_8
ε : Type u_9
f : Filter α
g : Filter β
h : Filter γ
m : α → δ → ε
n : β → γ → δ
m' : α → γ → δ'
n' : β → δ' → ε
h_left_comm : ∀ (a : α) (b : β) (c : γ), m a (n b c) = n' b (m' a c)
⊢ map₂ (fun (a : δ) (b : α) ↦ m b a) (map₂ n g h) f = map₂ n' g (map₂ (fun (a : γ) (b : α) ↦ m' b a) h f)

Tactic:
exact map₂_assoc fun _ _ _ => h_left_comm _ _ _

Premises used: Filter.map₂_assoc
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
δ' : Type u_8
ε : Type u_9
f : Filter α
g : Filter β
h : Filter γ
m : δ → γ → ε
n : α → β → δ
m' : α → γ → δ'
n' : δ' → β → ε
h_right_comm : ∀ (a : α) (b : β) (c : γ), m (n a b) c = n' (m' a c) b
rw : map₂ m (map₂ (fun (a : β) (b : α) ↦ n b a) g f) h = map₂ (fun (a : β) (b : δ') ↦ n' b a) g (map₂ m' f h)
⊢ map₂ m (map₂ n f g) h = map₂ n' (map₂ m' f h) g

Tactic:
rw [map₂_swap n, map₂_swap n']

Premises used: Filter.map₂_swap
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
δ' : Type u_8
ε : Type u_9
f : Filter α
g : Filter β
h : Filter γ
m : δ → γ → ε
n : α → β → δ
m' : α → γ → δ'
n' : δ' → β → ε
h_right_comm : ∀ (a : α) (b : β) (c : γ), m (n a b) c = n' (m' a c) b
⊢ map₂ m (map₂ (fun (a : β) (b : α) ↦ n b a) g f) h = map₂ (fun (a : β) (b : δ') ↦ n' b a) g (map₂ m' f h)

Tactic:
map₂_assoc fun _ _ _ => h_right_comm _ _ _

Premises used: Filter.map₂_assoc
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
δ' : Type u_8
ε : Type u_9
f : Filter α
g : Filter β
h : Filter γ
m : δ → γ → ε
n : α → β → δ
m' : α → γ → δ'
n' : δ' → β → ε
h_right_comm : ∀ (a : α) (b : β) (c : γ), m (n a b) c = n' (m' a c) b
⊢ map₂ m (map₂ (fun (a : β) (b : α) ↦ n b a) g f) h = map₂ (fun (a : β) (b : δ') ↦ n' b a) g (map₂ m' f h)

Tactic:
exact map₂_assoc fun _ _ _ => h_right_comm _ _ _

Premises used: Filter.map₂_assoc
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
m : α → β → γ
f : Filter α
g : Filter β
n : γ → δ
m' : α' → β' → δ
n₁ : α → α'
n₂ : β → β'
h_distrib : ∀ (a : α) (b : β), n (m a b) = m' (n₁ a) (n₂ b)
simp_rw : map₂ (fun (a : α) (b : β) ↦ n (m a b)) f g = map₂ m' (map n₁ f) (map n₂ g)
simp_rw₁ :
  Eq.{u_7 + 1} (α := Filter δ) (map₂ (fun (a : α) (b : β) ↦ n (m a b)) f g)
    (map₂ (fun (a : α) (b : β') ↦ m' (n₁ a) b) f (map n₂ g))
simp_rw₂ :
  Eq.{u_7 + 1} (α := Filter δ) (map₂ (fun (a : α) (b : β) ↦ n (m a b)) f g)
    (map₂ (fun (a : α) (b : β) ↦ m' (n₁ a) (n₂ b)) f g)
⊢ map n (map₂ m f g) = map₂ m' (map n₁ f) (map n₂ g)

Tactic:
simp_rw [map_map₂, map₂_map_left, map₂_map_right, h_distrib]

Premises used: Filter.map₂_map_right, Filter.map₂_map_left, Filter.map_map₂
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
γ : Type u_5
δ : Type u_7
m : α → β → γ
f : Filter α
g : Filter β
n : γ → δ
m' : α' → β → δ
n' : α → α'
h_distrib : ∀ (a : α) (b : β), n (m a b) = m' (n' a) b
⊢ map n (map₂ m f g) = map₂ m' (map n' f) g

Tactic:
map_map₂_distrib h_distrib

Premises used: Set.Mem, Filter.map, setOf, Filter.map_map₂_distrib, Set.preimage
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
m : α → β → γ
f : Filter α
g : Filter β
n : γ → δ
m' : α → β' → δ
n' : β → β'
h_distrib : ∀ (a : α) (b : β), n (m a b) = m' a (n' b)
⊢ map n (map₂ m f g) = map₂ m' f (map n' g)

Tactic:
map_map₂_distrib h_distrib

Premises used: Set.Mem, Filter.map, setOf, Filter.map_map₂_distrib, Set.preimage
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
γ : Type u_5
δ : Type u_7
f : Filter α
g : Filter β
m : α' → β → γ
n : α → α'
m' : α → β → δ
n' : δ → γ
h_left_comm : ∀ (a : α) (b : β), m (n a) b = n' (m' a b)
⊢ map₂ m (map n f) g = map n' (map₂ m' f g)

Tactic:
(map_map₂_distrib_left fun a b => (h_left_comm a b).symm).symm

Premises used: Filter.map_map₂_distrib_left, Eq.symm
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
f : Filter α
g : Filter β
m : α → β' → γ
n : β → β'
m' : α → β → δ
n' : δ → γ
h_right_comm : ∀ (a : α) (b : β), m a (n b) = n' (m' a b)
⊢ map₂ m f (map n g) = map n' (map₂ m' f g)

Tactic:
(map_map₂_distrib_right fun a b => (h_right_comm a b).symm).symm

Premises used: Filter.map_map₂_distrib_right, Eq.symm
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
ε : Type u_9
f : Filter α
g : Filter β
h : Filter γ
m : α → δ → ε
n : β → γ → δ
m₁ : α → β → β'
m₂ : α → γ → γ'
n' : β' → γ' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), m a (n b c) = n' (m₁ a b) (m₂ a c)
s : Set ε
t₁ : Set β'
u₁ : Set α
hu₁ : u₁ ∈ f
v : Set β
hv : v ∈ g
ht₁ : image2 m₁ u₁ v ⊆ t₁
t₂ : Set γ'
hs : image2 n' t₁ t₂ ⊆ s
u₂ : Set α
hu₂ : u₂ ∈ f
w : Set γ
hw : w ∈ h
ht₂ : image2 m₂ u₂ w ⊆ t₂
⊢ s ∈ map₂ m f (map₂ n g h)

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

Premises used: Filter.image2_mem_map₂, Set.Mem, Filter.inter_mem, setOf, Inter.inter, And.intro, Exists.intro
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
ε : Type u_9
f : Filter α
g : Filter β
h : Filter γ
m : α → δ → ε
n : β → γ → δ
m₁ : α → β → β'
m₂ : α → γ → γ'
n' : β' → γ' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), m a (n b c) = n' (m₁ a b) (m₂ a c)
s : Set ε
t₁ : Set β'
u₁ : Set α
hu₁ : u₁ ∈ f
v : Set β
hv : v ∈ g
ht₁ : image2 m₁ u₁ v ⊆ t₁
t₂ : Set γ'
hs : image2 n' t₁ t₂ ⊆ s
u₂ : Set α
hu₂ : u₂ ∈ f
w : Set γ
hw : w ∈ h
ht₂ : image2 m₂ u₂ w ⊆ t₂
refine : image2 m (u₁ ∩ u₂) (image2 n v w) ⊆ s
⊢ s ∈ map₂ m f (map₂ n g h)

Tactic:
refine ⟨u₁ ∩ u₂, inter_mem hu₁ hu₂, _, image2_mem_map₂ hv hw, ?_⟩
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
ε : Type u_9
f : Filter α
g : Filter β
h : Filter γ
m : α → δ → ε
n : β → γ → δ
m₁ : α → β → β'
m₂ : α → γ → γ'
n' : β' → γ' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), m a (n b c) = n' (m₁ a b) (m₂ a c)
s : Set ε
t₁ : Set β'
u₁ : Set α
hu₁ : u₁ ∈ f
v : Set β
hv : v ∈ g
ht₁ : image2 m₁ u₁ v ⊆ t₁
t₂ : Set γ'
hs : image2 n' t₁ t₂ ⊆ s
u₂ : Set α
hu₂ : u₂ ∈ f
w : Set γ
hw : w ∈ h
ht₂ : image2 m₂ u₂ w ⊆ t₂
⊢ image2 m (u₁ ∩ u₂) (image2 n v w) ⊆ s

Tactic:
(image2_distrib_subset_left h_distrib).trans ((image2_subset ?_ ?_).trans hs)

Premises used: Set.image2_subset, Set.image2_distrib_subset_left, HasSubset.Subset.trans
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
ε : Type u_9
f : Filter α
g : Filter β
h : Filter γ
m : α → δ → ε
n : β → γ → δ
m₁ : α → β → β'
m₂ : α → γ → γ'
n' : β' → γ' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), m a (n b c) = n' (m₁ a b) (m₂ a c)
s : Set ε
t₁ : Set β'
u₁ : Set α
hu₁ : u₁ ∈ f
v : Set β
hv : v ∈ g
ht₁ : image2 m₁ u₁ v ⊆ t₁
t₂ : Set γ'
hs : image2 n' t₁ t₂ ⊆ s
u₂ : Set α
hu₂ : u₂ ∈ f
w : Set γ
hw : w ∈ h
ht₂ : image2 m₂ u₂ w ⊆ t₂
refine_1 : image2 m₁ (u₁ ∩ u₂) v ⊆ t₁
refine_2 : image2 m₂ (u₁ ∩ u₂) w ⊆ t₂
⊢ image2 m (u₁ ∩ u₂) (image2 n v w) ⊆ s

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

Premises used: Set.image2_subset, Set.image2_distrib_subset_left, HasSubset.Subset.trans
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
ε : Type u_9
f : Filter α
g : Filter β
h : Filter γ
m : α → δ → ε
n : β → γ → δ
m₁ : α → β → β'
m₂ : α → γ → γ'
n' : β' → γ' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), m a (n b c) = n' (m₁ a b) (m₂ a c)
s : Set ε
t₁ : Set β'
u₁ : Set α
hu₁ : u₁ ∈ f
v : Set β
hv : v ∈ g
ht₁ : image2 m₁ u₁ v ⊆ t₁
t₂ : Set γ'
hs : image2 n' t₁ t₂ ⊆ s
u₂ : Set α
hu₂ : u₂ ∈ f
w : Set γ
hw : w ∈ h
ht₂ : image2 m₂ u₂ w ⊆ t₂
⊢ image2 m₁ (u₁ ∩ u₂) v ⊆ t₁

Tactic:
(image2_subset_right inter_subset_left).trans ht₁

Premises used: HasSubset.Subset.trans, Set.inter_subset_left, Set.image2_subset_right
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
ε : Type u_9
f : Filter α
g : Filter β
h : Filter γ
m : α → δ → ε
n : β → γ → δ
m₁ : α → β → β'
m₂ : α → γ → γ'
n' : β' → γ' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), m a (n b c) = n' (m₁ a b) (m₂ a c)
s : Set ε
t₁ : Set β'
u₁ : Set α
hu₁ : u₁ ∈ f
v : Set β
hv : v ∈ g
ht₁ : image2 m₁ u₁ v ⊆ t₁
t₂ : Set γ'
hs : image2 n' t₁ t₂ ⊆ s
u₂ : Set α
hu₂ : u₂ ∈ f
w : Set γ
hw : w ∈ h
ht₂ : image2 m₂ u₂ w ⊆ t₂
⊢ image2 m₁ (u₁ ∩ u₂) v ⊆ t₁

Tactic:
exact (image2_subset_right inter_subset_left).trans ht₁

Premises used: HasSubset.Subset.trans, Set.inter_subset_left, Set.image2_subset_right
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
ε : Type u_9
f : Filter α
g : Filter β
h : Filter γ
m : α → δ → ε
n : β → γ → δ
m₁ : α → β → β'
m₂ : α → γ → γ'
n' : β' → γ' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), m a (n b c) = n' (m₁ a b) (m₂ a c)
s : Set ε
t₁ : Set β'
u₁ : Set α
hu₁ : u₁ ∈ f
v : Set β
hv : v ∈ g
ht₁ : image2 m₁ u₁ v ⊆ t₁
t₂ : Set γ'
hs : image2 n' t₁ t₂ ⊆ s
u₂ : Set α
hu₂ : u₂ ∈ f
w : Set γ
hw : w ∈ h
ht₂ : image2 m₂ u₂ w ⊆ t₂
⊢ image2 m₂ (u₁ ∩ u₂) w ⊆ t₂

Tactic:
(image2_subset_right inter_subset_right).trans ht₂

Premises used: HasSubset.Subset.trans, Set.image2_subset_right, Set.inter_subset_right
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
ε : Type u_9
f : Filter α
g : Filter β
h : Filter γ
m : α → δ → ε
n : β → γ → δ
m₁ : α → β → β'
m₂ : α → γ → γ'
n' : β' → γ' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), m a (n b c) = n' (m₁ a b) (m₂ a c)
s : Set ε
t₁ : Set β'
u₁ : Set α
hu₁ : u₁ ∈ f
v : Set β
hv : v ∈ g
ht₁ : image2 m₁ u₁ v ⊆ t₁
t₂ : Set γ'
hs : image2 n' t₁ t₂ ⊆ s
u₂ : Set α
hu₂ : u₂ ∈ f
w : Set γ
hw : w ∈ h
ht₂ : image2 m₂ u₂ w ⊆ t₂
⊢ image2 m₂ (u₁ ∩ u₂) w ⊆ t₂

Tactic:
exact (image2_subset_right inter_subset_right).trans ht₂

Premises used: HasSubset.Subset.trans, Set.image2_subset_right, Set.inter_subset_right