awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : Filter ((α × β) × γ × δ)
⊢ Eq (α := Filter ((α × γ) × β × δ)) (map (fun (p : (α × β) × γ × δ) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) f)
    (comap (fun (p : (α × γ) × β × δ) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) f)

Tactic:
map_eq_comap_of_inverse (funext fun ⟨⟨_, _⟩, ⟨_, _⟩⟩ => rfl) (funext fun ⟨⟨_, _⟩, ⟨_, _⟩⟩ => rfl)

Premises used: Function.comp, id, Prod.mk, _private.0.Filter.map_swap4_eq_comap.match_2, Prod.fst, funext, _private.0.Filter.map_swap4_eq_comap.match_1, Filter.map_eq_comap_of_inverse, Eq, Prod.snd, rfl
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter α
m : α → β
g : Filter β
h : ∀ s ∈ f, m '' s ∈ g
⊢ g ≤ map m f

Tactic:
fun _ hs => mem_of_superset (h _ hs) <| image_preimage_subset _ _

Premises used: Set.preimage, Set.image_preimage_subset, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter α
m : α → β
g : Filter β
⊢ g ≤ map m f ↔ ∀ s ∈ f, m '' s ∈ g

Tactic:
⟨fun h _ hs => h (image_mem_map hs), le_map⟩

Premises used: Filter.image_mem_map, Iff.intro, Filter.le_map
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
a : map f (F ⊓ comap f G) ≤ map f F ⊓ G
a₁ : map f F ⊓ G ≤ map f (F ⊓ comap f G)
⊢ map f (F ⊓ comap f G) = map f F ⊓ G

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
⊢ map f (F ⊓ comap f G) ≤ map f F ⊓ map f (comap f G)

Tactic:
map_inf_le

Premises used: Filter.map_inf_le
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
⊢ map f F ⊓ map f (comap f G) ≤ map f F ⊓ G

Tactic:
inf_le_inf_left (map f F) map_comap_le

Premises used: Set.Mem, Filter.map, inf_le_inf_left, Filter.map_comap_le
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
⊢ map f (F ⊓ comap f G) ≤ map f F ⊓ G

Tactic:
calc
      map f (F ⊓ comap f G) ≤ map f F ⊓ (map f <| comap f G) := map_inf_le
      _ ≤ map f F ⊓ G := inf_le_inf_left (map f F) map_comap_le

Premises used: Filter.map, Filter.map_inf_le, inf_le_inf_left, Filter.map_comap_le, Min.min, Filter.comap
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
U : Set β
V : Set α
V_in : V ∈ F
W : Set α
h : f ⁻¹' U = V ∩ W
Z : Set β
Z_in : Z ∈ G
hZ : f ⁻¹' Z ⊆ W
a : f '' V ∩ Z ⊆ U
⊢ U ∈ map f F ⊓ G

Tactic:
apply mem_inf_of_inter (image_mem_map V_in) Z_in

Premises used: Filter.mem_inf_of_inter, Filter.image_mem_map
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
U : Set β
V : Set α
V_in : V ∈ F
W : Set α
h : f ⁻¹' U = V ∩ W
Z : Set β
Z_in : Z ∈ G
hZ : f ⁻¹' Z ⊆ W
rw rw₁ : f '' V ∩ Z = f '' V ∩ Z
⊢ f '' V ∩ Z = f '' (V ∩ f ⁻¹' Z)

Tactic:
rw [image_inter_preimage]

Premises used: Set.image_inter_preimage
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
U : Set β
V : Set α
V_in : V ∈ F
W : Set α
h : f ⁻¹' U = V ∩ W
Z : Set β
Z_in : Z ∈ G
hZ : f ⁻¹' Z ⊆ W
⊢ f '' (V ∩ f ⁻¹' Z) ⊆ f '' (V ∩ W)

Tactic:
gcongr
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
U : Set β
V : Set α
V_in : V ∈ F
W : Set α
h : f ⁻¹' U = V ∩ W
Z : Set β
Z_in : Z ∈ G
hZ : f ⁻¹' Z ⊆ W
rw rw₁ : f '' (V ∩ W) = f '' (V ∩ W)
⊢ f '' (V ∩ W) = f '' f ⁻¹' U

Tactic:
rw [h]
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
U : Set β
V : Set α
V_in : V ∈ F
W : Set α
h : f ⁻¹' U = V ∩ W
Z : Set β
Z_in : Z ∈ G
hZ : f ⁻¹' Z ⊆ W
⊢ f '' f ⁻¹' U ⊆ U

Tactic:
image_preimage_subset f U

Premises used: Set.image_preimage_subset
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
U : Set β
V : Set α
V_in : V ∈ F
W : Set α
h : f ⁻¹' U = V ∩ W
Z : Set β
Z_in : Z ∈ G
hZ : f ⁻¹' Z ⊆ W
f₁ : f '' V ∩ Z = f '' (V ∩ f ⁻¹' Z)
f₂ : f '' (V ∩ f ⁻¹' Z) ⊆ f '' (V ∩ W)
f₃ : f '' (V ∩ W) = f '' f ⁻¹' U
⊢ f '' V ∩ Z ⊆ U

Tactic:
calc
      f '' V ∩ Z = f '' (V ∩ f ⁻¹' Z) := by rw [image_inter_preimage]
      _ ⊆ f '' (V ∩ W) := by gcongr
      _ = f '' f ⁻¹' U := by rw [h]
      _ ⊆ U := image_preimage_subset f U

Premises used: Inter.inter, Set.preimage, Set.image_preimage_subset
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
⊢ map f (comap f G ⊓ F) = G ⊓ map f F

Tactic:
simp only [Filter.push_pull, inf_comm]

Premises used: inf_comm, Filter.push_pull
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
⊢ Disjoint F (comap f G) ↔ Disjoint (map f F) G

Tactic:
simp only [disjoint_iff, ← Filter.push_pull, map_eq_bot_iff]

Premises used: disjoint_iff, Filter.map_eq_bot_iff, Filter.push_pull
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
⊢ Disjoint (comap f G) F ↔ Disjoint G (map f F)

Tactic:
simp only [disjoint_iff, ← Filter.push_pull', map_eq_bot_iff]

Premises used: Filter.push_pull', disjoint_iff, Filter.map_eq_bot_iff
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
rw : (map f (F ⊓ comap f G)).NeBot ↔ (map f F ⊓ G).NeBot
f₁ : α → β
rw₁ : Type u_2
rw₂ rw₃ : (map f F ⊓ G).NeBot ↔ (map f F ⊓ G).NeBot
⊢ (F ⊓ comap f G).NeBot ↔ (map f F ⊓ G).NeBot

Tactic:
rw [← map_neBot_iff, Filter.push_pull]

Premises used: Filter.push_pull, Filter.map_neBot_iff
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
rw : (map f (comap f G ⊓ F)).NeBot ↔ (G ⊓ map f F).NeBot
f₁ : α → β
rw₁ : Type u_2
rw₂ rw₃ : (G ⊓ map f F).NeBot ↔ (G ⊓ map f F).NeBot
⊢ (comap f G ⊓ F).NeBot ↔ (G ⊓ map f F).NeBot

Tactic:
rw [← map_neBot_iff, Filter.push_pull']

Premises used: Filter.push_pull', Filter.map_neBot_iff
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
hf : f.NeBot
s : Set α
hs : m '' s ∈ f
rw : ∃ᶠ (x : β) in f, x ∈ m '' s
⊢ (comap m f ⊓ 𝓟 s).NeBot

Tactic:
rw [neBot_inf_comap_iff_map', map_principal, ← frequently_mem_iff_neBot]

Premises used: Filter.neBot_inf_comap_iff_map', Filter.map_principal, Filter.frequently_mem_iff_neBot
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
hf : f.NeBot
s : Set α
hs : m '' s ∈ f
⊢ ∃ᶠ (x : β) in f, x ∈ m '' s

Tactic:
Eventually.frequently hs

Premises used: Filter.Eventually.frequently
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
hf : f.NeBot
s : Set α
hs : m '' s ∈ f
⊢ ∃ᶠ (x : β) in f, x ∈ m '' s

Tactic:
exact Eventually.frequently hs

Premises used: Filter.Eventually.frequently
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
s : Set α
⊢ 𝓟 s = map (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) ⊤

Tactic:
simp
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
F : Filter α
s : Set α
rw :
  F ⊓ map (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) ⊤ = ⊥ ↔
    Eq (α := Filter { x : α // x ∈ s }) (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) F) ⊥
rw₁ :
  map (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
        (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) F ⊓ ⊤) =
      ⊥ ↔
    Eq (α := Filter { x : α // x ∈ s }) (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) F) ⊥
rw₂ :
  map (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
        (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) F) =
      ⊥ ↔
    Eq (α := Filter { x : α // x ∈ s }) (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) F) ⊥
rw₃ rw₄ :
  Eq (α := Filter { x : α // x ∈ s }) (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) F) ⊥ ↔
    Eq (α := Filter { x : α // x ∈ s }) (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) F) ⊥
⊢ F ⊓ 𝓟 s = ⊥ ↔ Eq (α := Filter { x : α // x ∈ s }) (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) F) ⊥

Tactic:
rw [principal_eq_map_coe_top s, ← Filter.push_pull', inf_top_eq, map_eq_bot_iff]

Premises used: Filter.push_pull', inf_top_eq, Filter.map_eq_bot_iff, Filter.principal_eq_map_coe_top
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
U : Set (Set β)
f : β → α
rw : (fun (x : Set α) ↦ f ⁻¹' x) ⁻¹' U ⊆ (map f (generate U)).sets
⊢ map f (generate U) ≤ generate ((fun (x : Set α) ↦ f ⁻¹' x) ⁻¹' U)

Tactic:
rw [le_generate_iff]

Premises used: Filter.le_generate_iff
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
U : Set (Set β)
f : β → α
⊢ (fun (x : Set α) ↦ f ⁻¹' x) ⁻¹' U ⊆ (map f (generate U)).sets

Tactic:
fun u hu ↦ mem_generate_of_mem hu

Premises used: Set.Mem, setOf, Filter.mem_generate_of_mem, Set.Subset, Set.preimage
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
U : Set (Set β)
f : β → α
⊢ (fun (x : Set α) ↦ f ⁻¹' x) ⁻¹' U ⊆ (map f (generate U)).sets

Tactic:
exact fun u hu ↦ mem_generate_of_mem hu

Premises used: Filter.mem_generate_of_mem
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
U : Set (Set α)
f : β → α
rw : U ⊆ (map f (generate ((fun (x : Set α) ↦ f ⁻¹' x) '' U))).sets
⊢ generate ((fun (x : Set α) ↦ f ⁻¹' x) '' U) ≤ comap f (generate U)

Tactic:
rw [← map_le_iff_le_comap, le_generate_iff]

Premises used: Filter.le_generate_iff, Filter.map_le_iff_le_comap
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
U : Set (Set α)
f : β → α
⊢ U ⊆ (map f (generate ((fun (x : Set α) ↦ f ⁻¹' x) '' U))).sets

Tactic:
fun u hu ↦ mem_generate_of_mem ⟨u, hu, rfl⟩

Premises used: Set.Mem, setOf, Filter.mem_generate_of_mem, Set.Subset, Set.preimage, And.intro, Exists.intro, rfl
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
U : Set (Set α)
f : β → α
⊢ U ⊆ (map f (generate ((fun (x : Set α) ↦ f ⁻¹' x) '' U))).sets

Tactic:
exact fun u hu ↦ mem_generate_of_mem ⟨u, hu, rfl⟩
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
a : α
⊢ Membership.mem (γ := Filter α) (pure a) {a}

Tactic:
mem_singleton a

Premises used: Set.mem_singleton, Set.Mem, setOf, Set.singleton
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
⊢ Injective.{u_1 + 1, u_1 + 1} (α := α) (β := Filter α) pure

Tactic:
fun a _ hab =>
  (Filter.ext_iff.1 hab { x | a = x }).1 rfl

Premises used: Set.Mem, setOf, Filter.ext_iff, Iff.mp, Function.Injective, Eq, rfl
-- Module: Mathlib.Order.Filter.Map
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
F : Filter α_1
G : Filter β
α : Type u
a : α
⊢ NeBot (pure a)

Tactic:
⟨mt empty_mem_iff_bot.2 <| notMem_empty a⟩

Premises used: Iff.mpr, mt, Filter.NeBot.mk, Filter.empty_mem_iff_bot, Set.notMem_empty
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
f : Filter α
a : α
rw : f ≤ 𝓟 {a} ↔ {a} ∈ f
rw₁ rw₂ : {a} ∈ f ↔ {a} ∈ f
⊢ f ≤ pure a ↔ {a} ∈ f

Tactic:
rw [← principal_singleton, le_principal_iff]

Premises used: Filter.le_principal_iff, Filter.principal_singleton
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter (α → β)
g : Filter α
s : Set β
⊢ s ∈ f.seq g ↔ ∃ u ∈ f, ∃ t ∈ g, ∀ x ∈ u, ∀ y ∈ t, x y ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter (α → β)
g : Filter α
s : Set β
⊢ s ∈ f.seq g ↔ ∃ u ∈ f, ∃ t ∈ g, u.seq t ⊆ s

Tactic:
simp only [mem_seq_def, seq_subset]

Premises used: Set.seq_subset, Filter.mem_seq_def
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Filter β
m : α → β → γ
s : Set γ
⊢ s ∈ (map m f).seq g ↔ ∃ (t : Set β) (u : Set α), t ∈ g ∧ u ∈ f ∧ ∀ x ∈ u, ∀ y ∈ t, m x y ∈ s

Tactic:
Iff.intro (fun ⟨t, ht, s, hs, hts⟩ => ⟨s, m ⁻¹' t, hs, ht, fun _ => hts _⟩)
    fun ⟨t, s, ht, hs, hts⟩ =>
    ⟨m '' s, image_mem_map hs, t, ht, fun _ ⟨_, has, Eq⟩ => Eq ▸ hts _ has⟩

Premises used: _private.0.Filter.mem_map_seq_iff.match_3, Filter.map, Filter.seq, Membership.mem, Exists, Eq.rec, Filter.image_mem_map, And, Set.preimage, _private.0.Filter.mem_map_seq_iff.match_2, And.intro, Iff.intro, Exists.intro, Set.image, _private.0.Filter.mem_map_seq_iff.match_1
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter (α → β)
g : Filter α
s : Set (α → β)
t : Set α
hs : s ∈ f
ht : t ∈ g
⊢ s.seq t ∈ f.seq g

Tactic:
⟨s, hs, t, ht, fun f hf a ha => ⟨f, hf, a, ha, rfl⟩⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, rfl
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter (α → β)
g : Filter α
h : Filter β
hh : ∀ t ∈ f, ∀ u ∈ g, t.seq u ∈ h
⊢ h ≤ f.seq g

Tactic:
fun _ ⟨_, ht, _, hu, hs⟩ =>
  mem_of_superset (hh _ ht _ hu) fun _ ⟨_, hm, _, ha, eq⟩ => eq ▸ hs _ hm _ ha

Premises used: _private.0.Filter.le_seq.match_1, Membership.mem, Eq.rec, _private.0.Filter.le_seq.match_2, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f₁ f₂ : Filter (α → β)
g₁ g₂ : Filter α
hf : f₁ ≤ f₂
hg : g₁ ≤ g₂
⊢ f₁.seq g₁ ≤ f₂.seq g₂

Tactic:
le_seq fun _ hs _ ht => seq_mem_seq (hf hs) (hg ht)

Premises used: Filter.le_seq, Filter.seq_mem_seq
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
g : α → β
f : Filter α
⊢ seq (pure g) f = map g f

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

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

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

Premises used: Filter.le_seq, le_antisymm, Filter.le_map
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
g : α → β
f : Filter α
s : Set α
hs : s ∈ f
refine_1 : Set.seq {g} s ∈ seq (pure g) f
⊢ g '' s ∈ seq (pure g) f

Tactic:
rw [← singleton_seq]

Premises used: Set.singleton_seq
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
g : α → β
f : Filter α
s : Set α
hs : s ∈ f
apply : Membership.mem (γ := Filter (α → β)) (pure g) {g}
⊢ Set.seq {g} s ∈ seq (pure g) f

Tactic:
apply seq_mem_seq _ hs

Premises used: Filter.seq_mem_seq
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
g : α → β
f : Filter α
s : Set α
hs : s ∈ f
⊢ Membership.mem (γ := Filter (α → β)) (pure g) {g}

Tactic:
singleton_mem_pure

Premises used: Set.Mem, Filter.singleton_mem_pure
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
g : α → β
f : Filter α
s : Set α
hs : s ∈ f
⊢ Membership.mem (γ := Filter (α → β)) (pure g) {g}

Tactic:
exact singleton_mem_pure

Premises used: Filter.singleton_mem_pure
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
g : α → β
f : Filter α
s : Set (α → β)
hs : Membership.mem (γ := Filter (α → β)) (pure g) s
t : Set α
ht : t ∈ f
⊢ s.seq t ∈ map g f

Tactic:
sets_of_superset (map g f) (image_mem_map ht) ?_

Premises used: Filter.map, Filter.image_mem_map, Filter.sets_of_superset
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
g : α → β
f : Filter α
s : Set (α → β)
hs : Membership.mem (γ := Filter (α → β)) (pure g) s
t : Set α
ht : t ∈ f
refine_2 : g '' t ⊆ s.seq t
⊢ s.seq t ∈ map g f

Tactic:
refine sets_of_superset (map g f) (image_mem_map ht) ?_

Premises used: Filter.map, Filter.image_mem_map, Filter.sets_of_superset
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
g : α → β
f : Filter α
s : Set (α → β)
hs : Membership.mem (γ := Filter (α → β)) (pure g) s
t : Set α
ht : t ∈ f
a : α
ha : a ∈ t
⊢ g a ∈ s.seq t

Tactic:
⟨g, hs, a, ha, rfl⟩

Premises used: Set.Mem, setOf, Set.image2, And.intro, Exists.intro, rfl, Set.seq
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
g : α → β
f : Filter α
s : Set (α → β)
hs : Membership.mem (γ := Filter (α → β)) (pure g) s
t : Set α
ht : t ∈ f
a : α
ha : a ∈ t
⊢ g a ∈ s.seq t

Tactic:
exact ⟨g, hs, a, ha, rfl⟩
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter (α → β)
a : α
⊢ f.seq (pure a) = map (fun (g : α → β) ↦ g a) f

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

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

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

Premises used: Filter.le_seq, le_antisymm, Filter.le_map
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter (α → β)
a : α
s : Set (α → β)
hs : s ∈ f
refine_1 : s.seq {a} ∈ f.seq (pure a)
⊢ (fun (g : α → β) ↦ g a) '' s ∈ f.seq (pure a)

Tactic:
rw [← seq_singleton]

Premises used: Set.seq_singleton
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter (α → β)
a : α
s : Set (α → β)
hs : s ∈ f
⊢ s.seq {a} ∈ f.seq (pure a)

Tactic:
seq_mem_seq hs singleton_mem_pure

Premises used: Filter.singleton_mem_pure, Filter.seq_mem_seq
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter (α → β)
a : α
s : Set (α → β)
hs : s ∈ f
⊢ s.seq {a} ∈ f.seq (pure a)

Tactic:
exact seq_mem_seq hs singleton_mem_pure

Premises used: Filter.singleton_mem_pure, Filter.seq_mem_seq
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter (α → β)
a : α
s : Set (α → β)
hs : s ∈ f
t : Set α
ht : Membership.mem (γ := Filter α) (pure a) t
⊢ Membership.mem (γ := Filter β) (map (fun (g : α → β) ↦ g a) f) (s.seq t)

Tactic:
sets_of_superset (map (fun g : α → β => g a) f) (image_mem_map hs) ?_

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

Tactic:
refine sets_of_superset (map (fun g : α → β => g a) f) (image_mem_map hs) ?_

Premises used: Filter.map, Filter.image_mem_map, Filter.sets_of_superset
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter (α → β)
a : α
s : Set (α → β)
hs : s ∈ f
t : Set α
ht : Membership.mem (γ := Filter α) (pure a) t
g : α → β
hg : g ∈ s
⊢ (fun (g : α → β) ↦ g a) g ∈ s.seq t

Tactic:
⟨g, hg, a, ht, rfl⟩

Premises used: Set.Mem, setOf, Set.image2, And.intro, Exists.intro, rfl, Set.seq
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter (α → β)
a : α
s : Set (α → β)
hs : s ∈ f
t : Set α
ht : Membership.mem (γ := Filter α) (pure a) t
g : α → β
hg : g ∈ s
⊢ (fun (g : α → β) ↦ g a) g ∈ s.seq t

Tactic:
exact ⟨g, hg, a, ht, rfl⟩
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
⊢ h.seq (g.seq x) = seq (seq (map (fun (x1 : β → γ) (x2 : α → β) ↦ x1 ∘ x2) h) g) x

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
γ : Type u_3
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
refine_1 :
  ∀ (s : Set (α → γ))
    (hs : Membership.mem (γ := Filter (α → γ)) (seq (map (fun (x1 : β → γ) (x2 : α → β) ↦ x1 ∘ x2) h) g) s) (t : Set α)
    (ht : t ∈ x), s.seq t ∈ h.seq (g.seq x)
refine_2 :
  ∀ (s : Set (β → γ)) (hs : s ∈ h) (t : Set β) (ht : t ∈ g.seq x),
    Membership.mem (γ := Filter γ) (seq (seq (map (fun (x1 : β → γ) (x2 : α → β) ↦ x1 ∘ x2) h) g) x) (s.seq t)
⊢ h.seq (g.seq x) = seq (seq (map (fun (x1 : β → γ) (x2 : α → β) ↦ x1 ∘ x2) h) g) x

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
γ : Type u_3
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (α → γ)
hs : Membership.mem (γ := Filter (α → γ)) (seq (map (fun (x1 : β → γ) (x2 : α → β) ↦ x1 ∘ x2) h) g) s
t : Set α
ht : t ∈ x
refine_1 :
  ∀ (u : Set ((α → β) → α → γ))
    (hu : Membership.mem (γ := Filter ((α → β) → α → γ)) (map (fun (x1 : β → γ) (x2 : α → β) ↦ x1 ∘ x2) h) u)
    (v : Set (α → β)) (hv : v ∈ g) (hs : u.seq v ⊆ s), s.seq t ∈ h.seq (g.seq x)
⊢ s.seq t ∈ h.seq (g.seq x)

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

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_1 : Membership.mem (γ := Filter (α → γ)) (seq (map (fun (x1 : β → γ) (x2 : α → β) ↦ x1 ∘ x2) h) g) s
t : Set α
ht : t ∈ x
u : Set ((α → β) → α → γ)
hu : Membership.mem (γ := Filter ((α → β) → α → γ)) (map (fun (x1 : β → γ) (x2 : α → β) ↦ x1 ∘ x2) h) u
v : Set (α → β)
hv : v ∈ g
hs : u.seq v ⊆ s
refine_1 :
  ∀ (w : Set (β → γ)) (hw : w ∈ h) (hu : (fun (x1 : β → γ) (x2 : α → β) ↦ x1 ∘ x2) '' w ⊆ u), s.seq t ∈ h.seq (g.seq x)
⊢ s.seq t ∈ h.seq (g.seq x)

Tactic:
rcases mem_map_iff_exists_image.1 hu with ⟨w, hw, hu⟩

Premises used: Iff.mp, Filter.mem_map_iff_exists_image
-- 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
refine_1 : Set.seq (Set.seq ((fun (x1 : β → γ) (x2 : α → β) ↦ x1 ∘ x2) '' w) v) t ∈ h.seq (g.seq x)
⊢ s.seq t ∈ h.seq (g.seq x)

Tactic:
grw [← hs, ← hu]
-- 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
refine_1 : w.seq (v.seq t) ∈ h.seq (g.seq x)
⊢ Set.seq (Set.seq ((fun (x1 : β → γ) (x2 : α → β) ↦ x1 ∘ x2) '' w) v) t ∈ h.seq (g.seq x)

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_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:
seq_mem_seq hw (seq_mem_seq hv ht)

Premises used: Filter.seq_mem_seq