awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (α → γ)
hs_1 : Membership.mem (γ := Filter (α → γ)) (seq (map (fun (x1 : β → γ) (x2 : α → β) ↦ x1 ∘ x2) h) g) s
t : Set α
ht : t ∈ x
u : Set ((α → β) → α → γ)
hu_1 : Membership.mem (γ := Filter ((α → β) → α → γ)) (map (fun (x1 : β → γ) (x2 : α → β) ↦ x1 ∘ x2) h) u
v : Set (α → β)
hv : v ∈ g
hs : u.seq v ⊆ s
w : Set (β → γ)
hw : w ∈ h
hu : (fun (x1 : β → γ) (x2 : α → β) ↦ x1 ∘ x2) '' w ⊆ u
⊢ w.seq (v.seq t) ∈ h.seq (g.seq x)

Tactic:
exact seq_mem_seq hw (seq_mem_seq hv ht)

Premises used: Filter.seq_mem_seq
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (β → γ)
hs : s ∈ h
t : Set β
ht : t ∈ g.seq x
refine_2 :
  ∀ (u : Set (α → β)) (hu : u ∈ g) (v : Set α) (hv : v ∈ x) (ht : u.seq v ⊆ t),
    Membership.mem (γ := Filter γ) (seq (seq (map (fun (x1 : β → γ) (x2 : α → β) ↦ x1 ∘ x2) h) g) x) (s.seq t)
⊢ Membership.mem (γ := Filter γ) (seq (seq (map (fun (x1 : β → γ) (x2 : α → β) ↦ x1 ∘ x2) h) g) x) (s.seq t)

Tactic:
rcases mem_seq_iff.1 ht with ⟨u, hu, v, hv, ht⟩

Premises used: Filter.mem_seq_iff, Iff.mp
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (β → γ)
hs : s ∈ h
t : Set β
ht_1 : t ∈ g.seq x
u : Set (α → β)
hu : u ∈ g
v : Set α
hv : v ∈ x
ht : u.seq v ⊆ t
refine_2 :
  Membership.mem (γ := Filter γ) (seq (seq (map (fun (x1 : β → γ) (x2 : α → β) ↦ x1 ∘ x2) h) g) x) (s.seq (u.seq v))
⊢ Membership.mem (γ := Filter γ) (seq (seq (map (fun (x1 : β → γ) (x2 : α → β) ↦ x1 ∘ x2) h) g) x) (s.seq t)

Tactic:
grw [← ht]
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (β → γ)
hs : s ∈ h
t : Set β
ht_1 : t ∈ g.seq x
u : Set (α → β)
hu : u ∈ g
v : Set α
hv : v ∈ x
ht : u.seq v ⊆ t
refine_2 :
  Membership.mem (γ := Filter γ) (seq (seq (map (fun (x1 : β → γ) (x2 : α → β) ↦ x1 ∘ x2) h) g) x)
    (Set.seq (Set.seq ((fun (x1 : β → γ) (x2 : α → β) ↦ x1 ∘ x2) '' s) u) v)
⊢ Membership.mem (γ := Filter γ) (seq (seq (map (fun (x1 : β → γ) (x2 : α → β) ↦ x1 ∘ x2) h) g) x) (s.seq (u.seq v))

Tactic:
rw [Set.seq_seq]

Premises used: Set.seq_seq
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (β → γ)
hs : s ∈ h
t : Set β
ht_1 : t ∈ g.seq x
u : Set (α → β)
hu : u ∈ g
v : Set α
hv : v ∈ x
ht : u.seq v ⊆ t
⊢ Membership.mem (γ := Filter γ) (seq (seq (map (fun (x1 : β → γ) (x2 : α → β) ↦ x1 ∘ x2) h) g) x)
    (Set.seq (Set.seq ((fun (x1 : β → γ) (x2 : α → β) ↦ x1 ∘ x2) '' s) u) v)

Tactic:
seq_mem_seq (seq_mem_seq (image_mem_map hs) hu) hv

Premises used: Filter.image_mem_map, Filter.seq_mem_seq
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (β → γ)
hs : s ∈ h
t : Set β
ht_1 : t ∈ g.seq x
u : Set (α → β)
hu : u ∈ g
v : Set α
hv : v ∈ x
ht : u.seq v ⊆ t
⊢ Membership.mem (γ := Filter γ) (seq (seq (map (fun (x1 : β → γ) (x2 : α → β) ↦ x1 ∘ x2) h) g) x)
    (Set.seq (Set.seq ((fun (x1 : β → γ) (x2 : α → β) ↦ x1 ∘ x2) '' s) u) v)

Tactic:
exact seq_mem_seq (seq_mem_seq (image_mem_map hs) hu) hv

Premises used: Filter.image_mem_map, Filter.seq_mem_seq
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ seq (map Prod.mk f) g = seq (map (fun (b : β) (a : α) ↦ (a, b)) g) f

Tactic:
le_antisymm (le_seq fun s hs t ht => ?_) (le_seq fun s hs t ht => ?_)

Premises used: Filter.le_seq, le_antisymm
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
refine_1 :
  ∀ (s : Set (α → α × β)) (hs : Membership.mem (γ := Filter (α → α × β)) (map (fun (b : β) (a : α) ↦ (a, b)) g) s)
    (t : Set α) (ht : t ∈ f), s.seq t ∈ seq (map Prod.mk f) g
refine_2 :
  ∀ (s : Set (β → α × β)) (hs : Membership.mem (γ := Filter (β → α × β)) (map Prod.mk f) s) (t : Set β) (ht : t ∈ g),
    Membership.mem (γ := Filter (α × β)) (seq (map (fun (b : β) (a : α) ↦ (a, b)) g) f) (s.seq t)
⊢ seq (map Prod.mk f) g = seq (map (fun (b : β) (a : α) ↦ (a, b)) g) f

Tactic:
refine le_antisymm (le_seq fun s hs t ht => ?_) (le_seq fun s hs t ht => ?_)

Premises used: Filter.le_seq, le_antisymm
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (α → α × β)
hs : Membership.mem (γ := Filter (α → α × β)) (map (fun (b : β) (a : α) ↦ (a, b)) g) s
t : Set α
ht : t ∈ f
refine_1 : ∀ (u : Set β) (hu : u ∈ g) (hs : (fun (b : β) (a : α) ↦ (a, b)) '' u ⊆ s), s.seq t ∈ seq (map Prod.mk f) g
⊢ s.seq t ∈ seq (map Prod.mk f) g

Tactic:
rcases mem_map_iff_exists_image.1 hs with ⟨u, hu, hs⟩

Premises used: Iff.mp, Filter.mem_map_iff_exists_image
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (α → α × β)
hs_1 : Membership.mem (γ := Filter (α → α × β)) (map (fun (b : β) (a : α) ↦ (a, b)) g) s
t : Set α
ht : t ∈ f
u : Set β
hu : u ∈ g
hs : (fun (b : β) (a : α) ↦ (a, b)) '' u ⊆ s
refine_1 : Set.seq ((fun (b : β) (a : α) ↦ (a, b)) '' u) t ∈ seq (map Prod.mk f) g
⊢ s.seq t ∈ seq (map Prod.mk f) g

Tactic:
grw [← hs]
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (α → α × β)
hs_1 : Membership.mem (γ := Filter (α → α × β)) (map (fun (b : β) (a : α) ↦ (a, b)) g) s
t : Set α
ht : t ∈ f
u : Set β
hu : u ∈ g
hs : (fun (b : β) (a : α) ↦ (a, b)) '' u ⊆ s
refine_1 : Set.seq (Prod.mk '' t) u ∈ seq (map Prod.mk f) g
⊢ Set.seq ((fun (b : β) (a : α) ↦ (a, b)) '' u) t ∈ seq (map Prod.mk f) g

Tactic:
rw [← Set.prod_image_seq_comm]

Premises used: Set.prod_image_seq_comm
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (α → α × β)
hs_1 : Membership.mem (γ := Filter (α → α × β)) (map (fun (b : β) (a : α) ↦ (a, b)) g) s
t : Set α
ht : t ∈ f
u : Set β
hu : u ∈ g
hs : (fun (b : β) (a : α) ↦ (a, b)) '' u ⊆ s
⊢ Set.seq (Prod.mk '' t) u ∈ seq (map Prod.mk f) g

Tactic:
seq_mem_seq (image_mem_map ht) hu

Premises used: Filter.image_mem_map, Filter.seq_mem_seq
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (α → α × β)
hs_1 : Membership.mem (γ := Filter (α → α × β)) (map (fun (b : β) (a : α) ↦ (a, b)) g) s
t : Set α
ht : t ∈ f
u : Set β
hu : u ∈ g
hs : (fun (b : β) (a : α) ↦ (a, b)) '' u ⊆ s
⊢ Set.seq (Prod.mk '' t) u ∈ seq (map Prod.mk f) g

Tactic:
exact seq_mem_seq (image_mem_map ht) hu

Premises used: Filter.image_mem_map, Filter.seq_mem_seq
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (β → α × β)
hs : Membership.mem (γ := Filter (β → α × β)) (map Prod.mk f) s
t : Set β
ht : t ∈ g
refine_2 :
  ∀ (u : Set α) (hu : u ∈ f) (hs : Prod.mk '' u ⊆ s),
    Membership.mem (γ := Filter (α × β)) (seq (map (fun (b : β) (a : α) ↦ (a, b)) g) f) (s.seq t)
⊢ Membership.mem (γ := Filter (α × β)) (seq (map (fun (b : β) (a : α) ↦ (a, b)) g) f) (s.seq t)

Tactic:
rcases mem_map_iff_exists_image.1 hs with ⟨u, hu, hs⟩

Premises used: Iff.mp, Filter.mem_map_iff_exists_image
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (β → α × β)
hs_1 : Membership.mem (γ := Filter (β → α × β)) (map Prod.mk f) s
t : Set β
ht : t ∈ g
u : Set α
hu : u ∈ f
hs : Prod.mk '' u ⊆ s
refine_2 :
  Membership.mem (γ := Filter (α × β)) (seq (map (fun (b : β) (a : α) ↦ (a, b)) g) f) (Set.seq (Prod.mk '' u) t)
⊢ Membership.mem (γ := Filter (α × β)) (seq (map (fun (b : β) (a : α) ↦ (a, b)) g) f) (s.seq t)

Tactic:
grw [← hs]
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (β → α × β)
hs_1 : Membership.mem (γ := Filter (β → α × β)) (map Prod.mk f) s
t : Set β
ht : t ∈ g
u : Set α
hu : u ∈ f
hs : Prod.mk '' u ⊆ s
refine_2 :
  Membership.mem (γ := Filter (α × β)) (seq (map (fun (b : β) (a : α) ↦ (a, b)) g) f)
    (Set.seq ((fun (b : β) (a : α) ↦ (a, b)) '' t) u)
⊢ Membership.mem (γ := Filter (α × β)) (seq (map (fun (b : β) (a : α) ↦ (a, b)) g) f) (Set.seq (Prod.mk '' u) t)

Tactic:
rw [Set.prod_image_seq_comm]

Premises used: Set.prod_image_seq_comm
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (β → α × β)
hs_1 : Membership.mem (γ := Filter (β → α × β)) (map Prod.mk f) s
t : Set β
ht : t ∈ g
u : Set α
hu : u ∈ f
hs : Prod.mk '' u ⊆ s
⊢ Membership.mem (γ := Filter (α × β)) (seq (map (fun (b : β) (a : α) ↦ (a, b)) g) f)
    (Set.seq ((fun (b : β) (a : α) ↦ (a, b)) '' t) u)

Tactic:
seq_mem_seq (image_mem_map ht) hu

Premises used: Set.Mem, setOf, Filter.image_mem_map, Filter.seq_mem_seq
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (β → α × β)
hs_1 : Membership.mem (γ := Filter (β → α × β)) (map Prod.mk f) s
t : Set β
ht : t ∈ g
u : Set α
hu : u ∈ f
hs : Prod.mk '' u ⊆ s
⊢ Membership.mem (γ := Filter (α × β)) (seq (map (fun (b : β) (a : α) ↦ (a, b)) g) f)
    (Set.seq ((fun (b : β) (a : α) ↦ (a, b)) '' t) u)

Tactic:
exact seq_mem_seq (image_mem_map ht) hu

Premises used: Filter.image_mem_map, Filter.seq_mem_seq
-- Module: Mathlib.Order.Filter.Map
Goal:
α β : Type u
f : Filter (α → β)
g : Filter α
⊢ f <*> g = f.seq g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
F : Filter α
G : Filter β
⊢ CommApplicative Filter

Tactic:
⟨fun f g => prod_map_seq_comm f g⟩

Premises used: CommApplicative.mk, Filter.prod_map_seq_comm
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter α
m : α → Filter β
p : β → Prop
⊢ (∀ᶠ (y : β) in f.bind m, p y) ↔ ∀ᶠ (x : α) in f, ∀ᶠ (y : β) in m x, p y

Tactic:
Iff.rfl

Premises used: Set.Mem, Filter.Eventually, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter α
m : α → Filter β
p : β → Prop
rw : (¬∃ᶠ (y : β) in f.bind m, p y) ↔ ¬∃ᶠ (x : α) in f, ∃ᶠ (y : β) in m x, p y
⊢ (∃ᶠ (y : β) in f.bind m, p y) ↔ ∃ᶠ (x : α) in f, ∃ᶠ (y : β) in m x, p y

Tactic:
rw [← not_iff_not]

Premises used: not_iff_not
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter α
m : α → Filter β
p : β → Prop
⊢ (¬∃ᶠ (y : β) in f.bind m, p y) ↔ ¬∃ᶠ (x : α) in f, ∃ᶠ (y : β) in m x, p y

Tactic:
simp only [not_frequently, eventually_bind]

Premises used: Filter.eventually_bind, Filter.not_frequently
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
m : α → Filter β
g₁ g₂ : β → γ
⊢ g₁ =ᶠ[f.bind m] g₂ ↔ ∀ᶠ (x : α) in f, g₁ =ᶠ[m x] g₂

Tactic:
Iff.rfl

Premises used: Set.Mem, Filter.Eventually, Iff.rfl, setOf, Filter.EventuallyEq, Set.preimage
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LE γ
f : Filter α
m : α → Filter β
g₁ g₂ : β → γ
⊢ g₁ ≤ᶠ[f.bind m] g₂ ↔ ∀ᶠ (x : α) in f, g₁ ≤ᶠ[m x] g₂

Tactic:
Iff.rfl

Premises used: Set.Mem, Filter.Eventually, Iff.rfl, setOf, Set.preimage, Filter.EventuallyLE
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
s : Set β
f : Filter α
m : α → Filter β
⊢ s ∈ f.bind m ↔ {a : α | s ∈ m a} ∈ f

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
s : Set β
f : Filter α
m : α → Filter β
⊢ s ∈ f.bind m ↔ ∃ t ∈ f, ∀ x ∈ t, s ∈ m x

Tactic:
calc
    s ∈ bind f m ↔ { a | s ∈ m a } ∈ f := Iff.rfl
    _ ↔ ∃ t ∈ f, t ⊆ { a | s ∈ m a } := exists_mem_subset_iff.symm
    _ ↔ ∃ t ∈ f, ∀ x ∈ t, s ∈ m x := Iff.rfl

Premises used: Trans.trans, Iff.rfl, Filter.exists_mem_subset_iff, Iff.symm
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : α → Filter β
l : Filter β
h : ∀ᶠ (x : α) in f, g x ≤ l
⊢ f.bind g ≤ l

Tactic:
join_le <| eventually_map.2 h

Premises used: Iff.mpr, Set.Mem, Filter.eventually_map, Filter.join_le
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : α → Filter β
hf : f₁ ≤ f₂
hg : g₁ ≤ᶠ[f₁] g₂
⊢ f₁.bind g₁ ≤ f₂.bind g₂

Tactic:
le_trans (fun s hs => ?_) (join_mono <| map_mono hf)

Premises used: Filter.map_mono, Filter.join_mono, le_trans
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : α → Filter β
hf : f₁ ≤ f₂
hg : g₁ ≤ᶠ[f₁] g₂
refine : ∀ (s : Set β) (hs : s ∈ (map g₂ f₁).join), s ∈ f₁.bind g₁
⊢ f₁.bind g₁ ≤ f₂.bind g₂

Tactic:
refine le_trans (fun s hs => ?_) (join_mono <| map_mono hf)

Premises used: Filter.map_mono, Filter.join_mono, le_trans
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : α → Filter β
hf : f₁ ≤ f₂
hg : g₁ ≤ᶠ[f₁] g₂
s : Set β
hs : s ∈ (map g₂ f₁).join
simp : ∀ (hs : g₂ ⁻¹' {t : Filter β | s ∈ t} ∈ f₁), {a : α | s ∈ g₁ a} ∈ f₁
⊢ s ∈ f₁.bind g₁

Tactic:
simp only [mem_join, mem_bind', mem_map] at hs ⊢

Premises used: Filter.mem_bind', Filter.mem_map, Filter.mem_join
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : α → Filter β
hf : f₁ ≤ f₂
hg : g₁ ≤ᶠ[f₁] g₂
s : Set β
hs_1 : g₂ ⁻¹' {t : Filter β | s ∈ t} ∈ f₁
a : α
hx : g₁ a ≤ g₂ a
hs : a ∈ g₂ ⁻¹' {t : Filter β | s ∈ t}
⊢ s ∈ g₁ a

Tactic:
hx hs
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : α → Filter β
hf : f₁ ≤ f₂
hg : g₁ ≤ᶠ[f₁] g₂
s : Set β
hs : g₂ ⁻¹' {t : Filter β | s ∈ t} ∈ f₁
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ g₁ x ≤ g₂ x) x} x →
          Membership.mem (γ := Set α)
            {x : α | x ∈ g₂ ⁻¹' {t : Filter β | s ∈ t} → Membership.mem (γ := Set α) {a : α | s ∈ g₁ a} x} x}
      a
h₁ h₂ : ∀ (a : α) (hx : g₁ a ≤ g₂ a) (hs : a ∈ g₂ ⁻¹' {t : Filter β | s ∈ t}), s ∈ g₁ a
⊢ {a : α | s ∈ g₁ a} ∈ f₁

Tactic:
filter_upwards [hg, hs] with _ hx hs using hx hs
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : α → Filter β
s_1 s : Set β
⊢ Membership.mem (γ := Filter β) (f.bind fun (x : α) ↦ g x ⊓ 𝓟 s_1) s ↔ s ∈ f.bind g ⊓ 𝓟 s_1

Tactic:
simp only [mem_bind, mem_inf_principal]

Premises used: Filter.mem_bind, Filter.mem_inf_principal
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f g : Filter α
h : α → Filter β
⊢ (f ⊔ g).bind h = f.bind h ⊔ g.bind h

Tactic:
rfl

Premises used: Set.Mem, Filter.bind, setOf, Set.preimage, Filter.copy, Filter.join, rfl
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → Filter β
⊢ (map f (𝓟 s)).join = ⨆ x ∈ s, f x

Tactic:
simp only [sSup_image, join_principal_eq_sSup, map_principal]

Premises used: Filter.join_principal_eq_sSup, sSup_image, Filter.map_principal
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
F : Filter α
G : Filter β
m : α → β
⊢ SurjOn (map m) (Iic F) (Iic G) ↔ G ≤ map m F

Tactic:
⟨fun hm ↦ ?_, fun hm ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
F : Filter α
G : Filter β
m : α → β
refine_1 : ∀ (hm : SurjOn (map m) (Iic F) (Iic G)), G ≤ map m F
refine_2 : ∀ (hm : G ≤ map m F), SurjOn (map m) (Iic F) (Iic G)
⊢ SurjOn (map m) (Iic F) (Iic G) ↔ G ≤ map m F

Tactic:
refine ⟨fun hm ↦ ?_, fun hm ↦ ?_⟩
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
F : Filter α
G : Filter β
m : α → β
hm : SurjOn (map m) (Iic F) (Iic G)
refine_1 : ∀ (H : Filter α) (hHF : H ≤ F) (hm : SurjOn (map m) (Iic F) (Iic (map m H))), map m H ≤ map m F
⊢ G ≤ map m F

Tactic:
rcases hm self_mem_Iic with ⟨H, (hHF : H ≤ F), rfl⟩

Premises used: Set.self_mem_Iic, rfl
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
F : Filter α
m : α → β
H : Filter α
hHF : H ≤ F
hm : SurjOn (map m) (Iic F) (Iic (map m H))
⊢ map m H ≤ map m F

Tactic:
map_mono hHF

Premises used: Filter.map_mono
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
F : Filter α
m : α → β
H : Filter α
hHF : H ≤ F
hm : SurjOn (map m) (Iic F) (Iic (map m H))
⊢ map m H ≤ map m F

Tactic:
exact map_mono hHF

Premises used: Filter.map_mono
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
F : Filter α
G : Filter β
m : α → β
hm : G ≤ map m F
H : Filter β
hHG : H ≤ G
⊢ map m ((fun (x : Filter β) ↦ F ⊓ comap m x) H) = H

Tactic:
simpa [Filter.push_pull] using hHG.trans hm

Premises used: Filter.push_pull, LE.le.trans
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
F : Filter α
G : Filter β
m : α → β
hm : G ≤ map m F
⊢ RightInvOn (fun (x : Filter β) ↦ F ⊓ comap m x) (map m) (Iic G)

Tactic:
have : RightInvOn (F ⊓ comap m ·) (map m) (Iic G) :=
      fun H (hHG : H ≤ G) ↦ by simpa [Filter.push_pull] using hHG.trans hm
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
F : Filter α
G : Filter β
m : α → β
hm : G ≤ map m F
this : RightInvOn (fun (x : Filter β) ↦ F ⊓ comap m x) (map m) (Iic G)
⊢ SurjOn (map m) (Iic F) (Iic G)

Tactic:
this.surjOn fun H _ ↦ mem_Iic.mpr inf_le_left

Premises used: Iff.mpr, Set.RightInvOn.surjOn, Set.mem_Iic, inf_le_left
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
F : Filter α
G : Filter β
m : α → β
hm : G ≤ map m F
this : RightInvOn (fun (x : Filter β) ↦ F ⊓ comap m x) (map m) (Iic G)
⊢ SurjOn (map m) (Iic F) (Iic G)

Tactic:
exact this.surjOn fun H _ ↦ mem_Iic.mpr inf_le_left

Premises used: Iff.mpr, Set.RightInvOn.surjOn, Set.mem_Iic, inf_le_left
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
m : α → β
rw : 𝓟 t ≤ map m (𝓟 s) ↔ SurjOn m s t
rw₁ : 𝓟 t ≤ 𝓟 (m '' s) ↔ SurjOn m s t
rw₂ : t ⊆ m '' s ↔ SurjOn m s t
rw₃ rw₄ : t ⊆ m '' s ↔ t ⊆ m '' s
⊢ SurjOn (map m) (Iic (𝓟 s)) (Iic (𝓟 t)) ↔ SurjOn m s t

Tactic:
rw [map_surjOn_Iic_iff_le_map, map_principal, principal_mono, SurjOn]

Premises used: Filter.principal_mono, Set.SurjOn, Filter.map_surjOn_Iic_iff_le_map, Filter.map_principal
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
s : Set α
m : α → β
⊢ InjOn (map m) (Iic (𝓟 s)) ↔ InjOn m s

Tactic:
⟨fun hm x hx y hy hxy ↦ ?_, fun hm F hF G hG ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
s : Set α
m : α → β
refine_1 : ∀ (hm : InjOn (map m) (Iic (𝓟 s))) (x : α) (hx : x ∈ s) (y : α) (hy : y ∈ s) (hxy : m x = m y), x = y
refine_2 :
  ∀ (hm : InjOn m s) (F : Filter α) (hF : F ∈ Iic (𝓟 s)) (G : Filter α) (hG : G ∈ Iic (𝓟 s)), map m F = map m G → F = G
⊢ InjOn (map m) (Iic (𝓟 s)) ↔ InjOn m s

Tactic:
refine ⟨fun hm x hx y hy hxy ↦ ?_, fun hm F hF G hG ↦ ?_⟩
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
s : Set α
m : α → β
hm : InjOn (map m) (Iic (𝓟 s))
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : m x = m y
refine_1 : ∀ (hxy : map m (pure x) = map m (pure y)), pure x ∈ Iic (𝓟 s)
refine_1₁ : ∀ (hxy : map m (pure x) = map m (pure y)), pure y ∈ Iic (𝓟 s)
⊢ x = y

Tactic:
rwa [← pure_injective.eq_iff, ← map_pure, ← map_pure, hm.eq_iff, pure_injective.eq_iff]
      at hxy

Premises used: Set.InjOn.eq_iff, Filter.pure_injective, Function.Injective.eq_iff, Filter.map_pure
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
s : Set α
m : α → β
hm : InjOn (map m) (Iic (𝓟 s))
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : map m (pure x) = map m (pure y)
refine_1 : pure x ≤ 𝓟 s
refine_1₁ refine_1₂ refine_1₃ refine_1₄ : x ∈ s
⊢ pure x ∈ Iic (𝓟 s)

Tactic:
rwa [mem_Iic, pure_le_principal]

Premises used: Filter.pure_le_principal, Set.mem_Iic
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
s : Set α
m : α → β
hm : InjOn (map m) (Iic (𝓟 s))
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : map m (pure x) = map m (pure y)
refine_1 : pure y ≤ 𝓟 s
refine_1₁ refine_1₂ refine_1₃ refine_1₄ : y ∈ s
⊢ pure y ∈ Iic (𝓟 s)

Tactic:
rwa [mem_Iic, pure_le_principal]

Premises used: Filter.pure_le_principal, Set.mem_Iic
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
s : Set α
m : α → β
hm : InjOn m s
F : Filter α
hF : F ∈ Iic (𝓟 s)
G : Filter α
hG : G ∈ Iic (𝓟 s)
⊢ map m F = map m G → F = G

Tactic:
simp [map_eq_map_iff_of_injOn (le_principal_iff.mp hF) (le_principal_iff.mp hG) hm]

Premises used: Filter.le_principal_iff, Filter.map_eq_map_iff_of_injOn, Iff.mp
-- 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_1 : α → β → γ
f_1 f₁ f₂ : Filter α
g_1 g₁ g₂ : Filter β
h : Filter γ
s : Set α
t : Set β
u : Set γ
a : α
b : β
m : α → β → γ
f : Filter α
g : Filter β
x : Set γ
simp :
  Membership.mem (γ := Set (Set γ)) {s : Set γ | ∃ u ∈ f, ∃ v ∈ g, ∀ x ∈ u, ∀ y ∈ v, m x y ∈ s} x ↔
    ∃ t₁ ∈ f, ∃ t₂ ∈ g, ∀ x_1 ∈ t₁, ∀ y ∈ t₂, (x_1, y) ∈ uncurry m ⁻¹' x
⊢ Membership.mem (γ := Set (Set γ)) {s : Set γ | ∃ u ∈ f, ∃ v ∈ g, image2 m u v ⊆ s} x ↔ x ∈ map (uncurry m) (f ×ˢ g)

Tactic:
simp only [mem_map, mem_prod_iff, image2_subset_iff, prod_subset_iff]

Premises used: Set.prod_subset_iff, Set.image2_subset_iff, Filter.mem_prod_iff, Filter.mem_map
-- 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_1 : α → β → γ
f_1 f₁ f₂ : Filter α
g_1 g₁ g₂ : Filter β
h : Filter γ
s : Set α
t : Set β
u : Set γ
a : α
b : β
m : α → β → γ
f : Filter α
g : Filter β
x : Set γ
⊢ Membership.mem (γ := Set (Set γ)) {s : Set γ | ∃ u ∈ f, ∃ v ∈ g, ∀ x ∈ u, ∀ y ∈ v, m x y ∈ s} x ↔
    ∃ t₁ ∈ f, ∃ t₂ ∈ g, ∀ x_1 ∈ t₁, ∀ y ∈ t₂, (x_1, y) ∈ uncurry m ⁻¹' x

Tactic:
rfl
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
g : Filter β
u : Set γ
⊢ u ∈ map₂ m f g ↔ ∃ s ∈ f, ∃ t ∈ g, image2 m s t ⊆ u

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
g : Filter β
s : Set α
t : Set β
hs : s ∈ f
ht : t ∈ g
⊢ image2 m s t ∈ map₂ m f g

Tactic:
⟨_, hs, _, ht, Subset.rfl⟩

Premises used: Set.Mem, setOf, Set.Subset.rfl, And.intro, Exists.intro
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
g : Filter β
rw :
  map (fun (p : α × β) ↦ m p.1 p.2) (f ×ˢ g) =
    (map (uncurry m) (f ×ˢ g)).copy {s : Set γ | ∃ u ∈ f, ∃ v ∈ g, image2 m u v ⊆ s} ⋯
rw₁ : map (fun (p : α × β) ↦ m p.1 p.2) (f ×ˢ g) = map (uncurry m) (f ×ˢ g)
rw₂ rw₃ :
  Eq.{u_5 + 1} (α := Filter γ) (map (fun (p : α × β) ↦ m p.1 p.2) (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

Tactic:
rw [map₂, copy_eq, uncurry_def]

Premises used: Function.uncurry_def, Filter.copy_eq, Filter.map₂
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α × β → γ
f : Filter α
g : Filter β
⊢ map m (f ×ˢ g) = map₂ (fun (a : α) (b : β) ↦ m (a, b)) f g

Tactic:
map_prod_eq_map₂ m.curry f g

Premises used: Function.curry, Filter.map_prod_eq_map₂
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
β : Type u_3
f : Filter α
g : Filter β
⊢ map₂ Prod.mk f g = f ×ˢ g

Tactic:
simp only [← map_prod_eq_map₂, map_id']

Premises used: Filter.map_prod_eq_map₂, Filter.map_id'
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : Filter α
g : Filter β
ι : Type u_11
ι' : Type u_12
p : ι → Prop
q : ι' → Prop
s : ι → Set α
t : ι' → Set β
m : α → β → γ
hf : f.HasBasis p s
hg : g.HasBasis q t
⊢ (map₂ m f g).HasBasis (fun (i : ι × ι') ↦ p i.1 ∧ q i.2) fun (i : ι × ι') ↦ image2 m (s i.1) (t i.2)

Tactic:
simpa only [← map_prod_eq_map₂, ← image_prod] using (hf.prod hg).map _

Premises used: Set.image_prod, Filter.HasBasis.map, Filter.map_prod_eq_map₂, Filter.HasBasis.prod
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f₁ f₂ : Filter α
g₁ g₂ : Filter β
hf : f₁ ≤ f₂
hg : g₁ ≤ g₂
⊢ map₂ m f₁ g₁ ≤ map₂ m f₂ g₂

Tactic:
fun _ ⟨s, hs, t, ht, hst⟩ => ⟨s, hf hs, t, hg ht, hst⟩

Premises used: Membership.mem, And.intro, Exists.intro, Filter.map₂, _private.0.Filter.map₂_mono.match_1