awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.ListTraverse
Goal:
α β : Type u
f : β → Filter α
b : β
fs : List β
ih : ∀ t ∈ traverse f fs, ∃ (us : List (Set α)), Forall₂ (fun (b : β) (s : Set α) ↦ s ∈ f b) fs us ∧ sequence us ⊆ t
t : Set (List α)
ht_1 : t ∈ traverse f (b :: fs)
u : Set (List α → List α)
hu : u ∈ cons <$> f b
v : Set (List α)
hv : Membership.mem (γ := Filter (List α)) ((fun (x : Unit) ↦ List.traverse f fs) ()) v
ht : u.seq v ⊆ t
mp :
  ∀ (w : Set α) (hw : w ∈ f b) (hwu : cons '' w ⊆ u),
    ∃ (us : List (Set α)), Forall₂ (fun (b : β) (s : Set α) ↦ s ∈ f b) (b :: fs) us ∧ sequence us ⊆ t
⊢ ∃ (us : List (Set α)), Forall₂ (fun (b : β) (s : Set α) ↦ s ∈ f b) (b :: fs) us ∧ sequence us ⊆ t

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

Premises used: Iff.mp, Filter.mem_map_iff_exists_image
-- Module: Mathlib.Order.Filter.ListTraverse
Goal:
α β : Type u
f : β → Filter α
b : β
fs : List β
ih : ∀ t ∈ traverse f fs, ∃ (us : List (Set α)), Forall₂ (fun (b : β) (s : Set α) ↦ s ∈ f b) fs us ∧ sequence us ⊆ t
t : Set (List α)
ht_1 : t ∈ traverse f (b :: fs)
u : Set (List α → List α)
hu : u ∈ cons <$> f b
v : Set (List α)
hv : Membership.mem (γ := Filter (List α)) ((fun (x : Unit) ↦ List.traverse f fs) ()) v
ht : u.seq v ⊆ t
w : Set α
hw : w ∈ f b
hwu : cons '' w ⊆ u
mp :
  ∀ (us : List (Set α)) (hus : Forall₂ (fun (b : β) (s : Set α) ↦ s ∈ f b) fs us) (hu : sequence us ⊆ v),
    ∃ (us : List (Set α)), Forall₂ (fun (b : β) (s : Set α) ↦ s ∈ f b) (b :: fs) us ∧ sequence us ⊆ t
⊢ ∃ (us : List (Set α)), Forall₂ (fun (b : β) (s : Set α) ↦ s ∈ f b) (b :: fs) us ∧ sequence us ⊆ t

Tactic:
rcases ih v hv with ⟨us, hus, hu⟩
-- Module: Mathlib.Order.Filter.ListTraverse
Goal:
α β : Type u
f : β → Filter α
b : β
fs : List β
ih : ∀ t ∈ traverse f fs, ∃ (us : List (Set α)), Forall₂ (fun (b : β) (s : Set α) ↦ s ∈ f b) fs us ∧ sequence us ⊆ t
t : Set (List α)
ht_1 : t ∈ traverse f (b :: fs)
u : Set (List α → List α)
hu_1 : u ∈ cons <$> f b
v : Set (List α)
hv : Membership.mem (γ := Filter (List α)) ((fun (x : Unit) ↦ List.traverse f fs) ()) v
ht : u.seq v ⊆ t
w : Set α
hw : w ∈ f b
hwu : cons '' w ⊆ u
us : List (Set α)
hus : Forall₂ (fun (b : β) (s : Set α) ↦ s ∈ f b) fs us
hu : sequence us ⊆ v
⊢ ∃ (us : List (Set α)), Forall₂ (fun (b : β) (s : Set α) ↦ s ∈ f b) (b :: fs) us ∧ sequence us ⊆ t

Tactic:
⟨w::us, Forall₂.cons hw hus, (Set.seq_mono hwu hu).trans ht⟩

Premises used: List.Forall₂.cons, HasSubset.Subset.trans, List.cons, And.intro, Exists.intro, Set.seq_mono
-- Module: Mathlib.Order.Filter.ListTraverse
Goal:
α β : Type u
f : β → Filter α
b : β
fs : List β
ih : ∀ t ∈ traverse f fs, ∃ (us : List (Set α)), Forall₂ (fun (b : β) (s : Set α) ↦ s ∈ f b) fs us ∧ sequence us ⊆ t
t : Set (List α)
ht_1 : t ∈ traverse f (b :: fs)
u : Set (List α → List α)
hu_1 : u ∈ cons <$> f b
v : Set (List α)
hv : Membership.mem (γ := Filter (List α)) ((fun (x : Unit) ↦ List.traverse f fs) ()) v
ht : u.seq v ⊆ t
w : Set α
hw : w ∈ f b
hwu : cons '' w ⊆ u
us : List (Set α)
hus : Forall₂ (fun (b : β) (s : Set α) ↦ s ∈ f b) fs us
hu : sequence us ⊆ v
⊢ ∃ (us : List (Set α)), Forall₂ (fun (b : β) (s : Set α) ↦ s ∈ f b) (b :: fs) us ∧ sequence us ⊆ t

Tactic:
exact ⟨w::us, Forall₂.cons hw hus, (Set.seq_mono hwu hu).trans ht⟩
-- Module: Mathlib.Order.Filter.ListTraverse
Goal:
α β : Type u
f : β → Filter α
fs : List β
t : Set (List α)
mp : ∀ t ∈ traverse f [], ∃ (us : List (Set α)), Forall₂ (fun (b : β) (s : Set α) ↦ s ∈ f b) [] us ∧ sequence us ⊆ t
mp₁ :
  ∀ (b : β) (fs : List β)
    (ih :
      ∀ t ∈ traverse f fs, ∃ (us : List (Set α)), Forall₂ (fun (b : β) (s : Set α) ↦ s ∈ f b) fs us ∧ sequence us ⊆ t),
    ∀ t ∈ traverse f (b :: fs),
      ∃ (us : List (Set α)), Forall₂ (fun (b : β) (s : Set α) ↦ s ∈ f b) (b :: fs) us ∧ sequence us ⊆ t
⊢ t ∈ traverse f fs → ∃ (us : List (Set α)), Forall₂ (fun (b : β) (s : Set α) ↦ s ∈ f b) fs us ∧ sequence us ⊆ t

Tactic:
induction fs generalizing t with
    | nil =>
      simp only [sequence, mem_pure, imp_self, forall₂_nil_left_iff, exists_eq_left, Set.pure_def,
        singleton_subset_iff, traverse_nil]
    | cons b fs ih =>
      intro ht
      rcases mem_seq_iff.1 ht with ⟨u, hu, v, hv, ht⟩
      rcases mem_map_iff_exists_image.1 hu with ⟨w, hw, hwu⟩
      rcases ih v hv with ⟨us, hus, hu⟩
      exact ⟨w::us, Forall₂.cons hw hus, (Set.seq_mono hwu hu).trans ht⟩

Premises used: Set.singleton_subset_iff, Set.pure_def, List.forall₂_nil_left_iff, exists_eq_left, List.cons, imp_self, List.traverse_nil, sequence, List.nil, Filter.mem_pure
-- Module: Mathlib.Order.Filter.ListTraverse
Goal:
α β : Type u
f : β → Filter α
fs : List β
t : Set (List α)
us : List (Set α)
hus : Forall₂ (fun (b : β) (s : Set α) ↦ s ∈ f b) fs us
hs : sequence us ⊆ t
⊢ t ∈ traverse f fs

Tactic:
mem_of_superset (mem_traverse _ _ hus) hs

Premises used: Filter.mem_traverse, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.ListTraverse
Goal:
α β : Type u
f : β → Filter α
fs : List β
t : Set (List α)
us : List (Set α)
hus : Forall₂ (fun (b : β) (s : Set α) ↦ s ∈ f b) fs us
hs : sequence us ⊆ t
⊢ t ∈ traverse f fs

Tactic:
exact mem_of_superset (mem_traverse _ _ hus) hs

Premises used: Filter.mem_traverse, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
⊢ map f (𝓟 s) = 𝓟 (f '' s)

Tactic:
Filter.ext fun _ => image_subset_iff.symm

Premises used: Filter.ext, Set.image_subset_iff, Iff.symm
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter α
m : α → β
P : β → Prop
⊢ (∀ᶠ (b : β) in map m f, P b) ↔ ∀ᶠ (a : α) in f, P (m a)

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 : α → β
P : β → Prop
⊢ (∃ᶠ (b : β) in map m f, P b) ↔ ∃ᶠ (a : α) in f, P (m a)

Tactic:
Iff.rfl

Premises used: Set.Mem, Filter.Eventually, Iff.rfl, setOf, Filter.Frequently, Set.preimage, Not
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
m : α → β
f₁ f₂ : β → γ
⊢ f₁ =ᶠ[map m f] f₂ ↔ f₁ ∘ m =ᶠ[f] f₂ ∘ m

Tactic:
.rfl

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

Tactic:
.rfl

Premises used: Set.Mem, Filter.map, Filter.Eventually, Iff.rfl, setOf, Set.preimage, Filter.EventuallyLE
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter α
m : α → β
t : Set β
⊢ t ∈ map m f ↔ m ⁻¹' t ∈ 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
f : Filter α
m : α → β
t : Set β
⊢ t ∈ map m f ↔ {x : α | m x ∈ t} ∈ 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
f : Filter α
m : α → β
s : Set α
hs : s ∈ f
⊢ m '' s ∈ map m f

Tactic:
f.sets_of_superset hs <| subset_preimage_image m s

Premises used: Set.Mem, setOf, Filter.sets_of_superset, Set.preimage, Set.subset_preimage_image
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter α
m : α → β
s : Set α
hf : Injective m
h : m '' s ∈ map m f
rwa rwa₁ rwa₂ rwa₃ : m ⁻¹' m '' s ∈ f
⊢ s ∈ f

Tactic:
rwa [← preimage_image_eq s hf]

Premises used: Set.preimage_image_eq
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter α
m : α → β
rw : m '' univ ∈ map m f
⊢ range m ∈ map m f

Tactic:
rw [← image_univ]

Premises used: Set.image_univ
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter α
m : α → β
⊢ m '' univ ∈ map m f

Tactic:
image_mem_map univ_mem

Premises used: Filter.image_mem_map, Filter.univ_mem
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter α
m : α → β
⊢ m '' univ ∈ map m f

Tactic:
exact image_mem_map univ_mem

Premises used: Filter.image_mem_map, Filter.univ_mem
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter α
m : α → β
t : Set β
⊢ t ∈ map m f ↔ ∃ s ∈ f, m '' s ⊆ t

Tactic:
⟨fun ht => ⟨m ⁻¹' t, ht, image_preimage_subset _ _⟩, fun ⟨_, hs, ht⟩ =>
    mem_of_superset (image_mem_map hs) ht⟩

Premises used: Filter.map, Membership.mem, Filter.image_mem_map, Set.preimage, And.intro, Iff.intro, Set.image_preimage_subset, Exists.intro, _private.0.Filter.mem_map_iff_exists_image.match_1, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
f : Filter α
⊢ map id f = f

Tactic:
filter_eq <| rfl

Premises used: Filter.filter_eq, rfl
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
f : Filter α
⊢ map (fun (x : α) ↦ x) f = f

Tactic:
map_id

Premises used: Filter.map_id
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : α → β
m' : β → γ
⊢ map m' ∘ map m = map (m' ∘ m)

Tactic:
funext fun _ => filter_eq <| rfl

Premises used: funext, Filter.filter_eq, rfl
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
m : α → β
m' : β → γ
⊢ map m' (map m f) = map (m' ∘ m) f

Tactic:
congr_fun Filter.map_compose f

Premises used: Filter.map, congr_fun, Filter.map_compose
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
m₁ m₂ : α → β
f : Filter α
h : m₁ =ᶠ[f] m₂
⊢ map m₁ f = map m₂ f

Tactic:
Filter.ext' fun _ => eventually_congr (h.mono fun _ hx => hx ▸ Iff.rfl)

Premises used: Filter.ext', Filter.Eventually.mono, Filter.eventually_congr
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
l : Filter β
s : Set α
h : s ∈ comap f l
t : Set β
ht : t ∈ l
hts : f ⁻¹' t ⊆ s
y : β
hy : y ∈ t
x : α
hx : f x = y
rwa rwa₁ rwa₂ rwa₃ : y ∈ t
⊢ f x ∈ t

Tactic:
rwa [hx]
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
l : Filter β
s : Set α
⊢ s ∈ comap f l ↔ kernImage f s ∈ l

Tactic:
mem_comap'

Premises used: Set.kernImage, Set.Mem, Filter.mem_comap'
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
x : α
s : Set β
F : Filter (α × β)
simp_rw : {y : α × β | ∀ ⦃x_1 : β⦄, (x, x_1) = y → x_1 ∈ s} ∈ F ↔ {p : α × β | p.1 = x → p.2 ∈ s} ∈ F
simp_rw₁ : {y : α × β | ∀ ⦃x_1 : β⦄, x = y.1 ∧ x_1 = y.2 → x_1 ∈ s} ∈ F ↔ {p : α × β | p.1 = x → p.2 ∈ s} ∈ F
simp_rw₂ : {y : α × β | ∀ ⦃x_1 : β⦄, x = y.1 → x_1 = y.2 → x_1 ∈ s} ∈ F ↔ {p : α × β | p.1 = x → p.2 ∈ s} ∈ F
simp_rw₃ : {y : α × β | ∀ (b : x = y.1) (a : β), a = y.2 → a ∈ s} ∈ F ↔ {p : α × β | p.1 = x → p.2 ∈ s} ∈ F
simp_rw₄ : {y : α × β | ∀ (b : x = y.1), y.2 ∈ s} ∈ F ↔ {p : α × β | p.1 = x → p.2 ∈ s} ∈ F
⊢ s ∈ comap (Prod.mk x) F ↔ {p : α × β | p.1 = x → p.2 ∈ s} ∈ F

Tactic:
simp_rw [mem_comap', Prod.ext_iff, and_imp, @forall_comm β (_ = _), forall_eq, eq_comm]

Premises used: and_imp, forall_eq, forall_comm, Prod.ext_iff, eq_comm, Filter.mem_comap'
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
l : Filter β
p : α → Prop
⊢ (∀ᶠ (a : α) in comap f l, p a) ↔ ∀ᶠ (b : β) in l, ∀ (a : α), f a = b → p a

Tactic:
mem_comap'

Premises used: Set.Mem, Filter.Eventually, setOf, Filter.mem_comap'
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
l : Filter β
p : α → Prop
⊢ (∃ᶠ (a : α) in comap f l, p a) ↔ ∃ᶠ (b : β) in l, ∃ (a : α), f a = b ∧ p a

Tactic:
simp only [Filter.Frequently, eventually_comap, not_exists, _root_.not_and]

Premises used: not_exists, Filter.Frequently, Filter.eventually_comap, not_and
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
l : Filter β
s : Set α
⊢ s ∈ comap f l ↔ (f '' sᶜ)ᶜ ∈ l

Tactic:
simp only [mem_comap'', kernImage_eq_compl]

Premises used: Filter.mem_comap'', Set.kernImage_eq_compl
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
l : Filter β
s : Set α
rw : (f '' sᶜᶜ)ᶜ ∈ l ↔ (f '' s)ᶜ ∈ l
rw₁ rw₂ : (f '' s)ᶜ ∈ l ↔ (f '' s)ᶜ ∈ l
⊢ sᶜ ∈ comap f l ↔ (f '' s)ᶜ ∈ l

Tactic:
rw [mem_comap_iff_compl, compl_compl]

Premises used: compl_compl, Filter.mem_comap_iff_compl
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
a : α
⊢ sets (pure a) = {s : Set α | a ∈ s}

Tactic:
rfl

Premises used: setOf, rfl
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
a : α
p : α → Prop
⊢ (∀ᶠ (x : α) in pure a, p x) ↔ p a

Tactic:
Iff.rfl

Premises used: Set.Mem, Filter.Eventually, Iff.rfl, setOf
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
a : α
p : α → Prop
⊢ (∃ᶠ (x : α) in pure a, p x) ↔ p a

Tactic:
simp [Filter.Frequently]

Premises used: Filter.Frequently
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
a : α
s : Set α
⊢ Membership.mem (γ := Filter α) (𝓟 {a}) s ↔ Membership.mem (γ := Filter α) (pure a) s

Tactic:
simp only [mem_pure, mem_principal, singleton_subset_iff]

Premises used: Set.singleton_subset_iff, Filter.mem_principal, Filter.mem_pure
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
s_1 s : Set α
⊢ Membership.mem (γ := Filter α) (⨆ a ∈ s_1, pure a) s ↔ s ∈ 𝓟 s_1

Tactic:
simp [Set.subset_def]

Premises used: Set.subset_def
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
rw : Eq.{u_1 + 1} (α := Filter α) (⨆ (a : α), pure a) (𝓟 univ)
rw₁ : Eq.{u_1 + 1} (α := Filter α) (⨆ (a : α), pure a) (⨆ (a : α), ⨆ (_ : Membership.mem (γ := Set α) univ a), pure a)
rw₂ rw₃ : Eq.{u_1 + 1} (α := Filter α) (⨆ (a : α), pure a) (⨆ (x : α), pure x)
⊢ Eq.{u_1 + 1} (α := Filter α) (⨆ (a : α), pure a) ⊤

Tactic:
rw [← principal_univ, ← biSup_pure_eq_principal, iSup_univ]

Premises used: Filter.biSup_pure_eq_principal, Filter.principal_univ, iSup_univ
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
a : α
⊢ map f (pure a) = pure (f a)

Tactic:
rfl

Premises used: Set.Mem, Filter.map, setOf, Set.preimage, Filter.copy, rfl
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
s : Set α
a : α
⊢ pure a ≤ 𝓟 s ↔ a ∈ s

Tactic:
simp
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
f : Filter α
⊢ join (pure f) = f

Tactic:
rfl

Premises used: Set.Mem, setOf, Filter.join, rfl
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
a : α
m : α → Filter β
⊢ bind (pure a) m = m a

Tactic:
simp only [bind, map_pure, join_pure]

Premises used: Filter.bind, Filter.map_pure, Filter.join_pure
-- Module: Mathlib.Order.Filter.Map
Goal:
γ : Type u_3
α : Type u_6
β : Type u_7
m : β → γ
f : Filter α
g : α → Filter β
⊢ map m (f.bind g) = f.bind (map m ∘ g)

Tactic:
rfl

Premises used: Set.Mem, Filter.map, Filter.bind, setOf, Set.preimage, Filter.join, rfl
-- Module: Mathlib.Order.Filter.Map
Goal:
γ : Type u_3
α : Type u_6
β : Type u_7
m : α → β
f : Filter α
g : β → Filter γ
⊢ (map m f).bind g = f.bind (g ∘ m)

Tactic:
rfl

Premises used: Set.Mem, Filter.map, Filter.bind, setOf, Set.preimage, rfl
-- Module: Mathlib.Order.Filter.Map
Goal:
α β : Type u_6
m : α → β
f : Filter α
⊢ m <$> f = map m f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Filter.Map
Goal:
α β : Type u_6
f : Filter α
m : α → Filter β
⊢ f >>= m = f.bind m

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
g : Filter β
m : α → β
s : Set α
⊢ s ∈ comap m g ↔ ∃ t ∈ g, m ⁻¹' t ⊆ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
g : Filter β
m : α → β
t : Set β
ht : t ∈ g
⊢ m ⁻¹' t ∈ comap m g

Tactic:
⟨t, ht, Subset.rfl⟩

Premises used: Set.Mem, setOf, Set.Subset.rfl, And.intro, Exists.intro
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
g : Filter β
p : β → Prop
hf : ∀ᶠ (b : β) in g, p b
f : α → β
⊢ ∀ᶠ (a : α) in Filter.comap f g, p (f a)

Tactic:
preimage_mem_comap hf

Premises used: Set.Mem, Filter.Eventually, setOf, Set.preimage, Filter.preimage_mem_comap
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
F : Filter β
f g : β → γ
h : α → β
hfg : f =ᶠ[F] g
⊢ f ∘ h =ᶠ[comap h F] g ∘ h

Tactic:
hfg.comap _

Premises used: Filter.EventuallyEq, Filter.Eventually.comap
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
f : Filter α
⊢ comap id f = f

Tactic:
le_antisymm (fun _ => preimage_mem_comap) fun _ ⟨_, ht, hst⟩ => mem_of_superset ht hst

Premises used: _private.0.Filter.comap_id.match_1, Membership.mem, le_antisymm, Filter.preimage_mem_comap, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
f : Filter α
⊢ comap (fun (x : α) ↦ x) f = f

Tactic:
comap_id

Premises used: Filter.comap_id
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
g : Filter β
t : Set β
x : β
ht : t ∈ g
hx : x ∉ t
⊢ Eq.{u_1 + 1} (α := Filter α) (comap (fun (x_1 : α) ↦ x) g) ⊥

Tactic:
empty_mem_iff_bot.1 <| mem_comap'.2 <| mem_of_superset ht fun _ hx' _ h => hx <| h.symm ▸ hx'

Premises used: Iff.mpr, Eq.rec, Filter.empty_mem_iff_bot, Iff.mp, Filter.mem_comap', Eq.symm, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
g : Filter β
x : β
h : ∀ t ∈ g, x ∈ t
⊢ Eq.{u_1 + 1} (α := Filter α) (comap (fun (x_1 : α) ↦ x) g) ⊤

Tactic:
top_unique fun _ hs => univ_mem' fun _ => h _ (mem_comap'.1 hs) rfl

Premises used: setOf, top_unique, Iff.mp, Filter.mem_comap', rfl, Filter.univ_mem'
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter α
inst : f.NeBot
c : β
h :
  ∀ (s : Set β), Membership.mem (γ := Filter β) (map (fun (x : α) ↦ c) f) s ↔ Membership.mem (γ := Filter β) (pure c) s
⊢ map (fun (x : α) ↦ c) f = pure c

Tactic:
ext s
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter α
inst : f.NeBot
c : β
s : Set β
pos :
  ∀ (h : c ∈ s), Membership.mem (γ := Filter β) (map (fun (x : α) ↦ c) f) s ↔ Membership.mem (γ := Filter β) (pure c) s
neg :
  ∀ (h : c ∉ s), Membership.mem (γ := Filter β) (map (fun (x : α) ↦ c) f) s ↔ Membership.mem (γ := Filter β) (pure c) s
⊢ Membership.mem (γ := Filter β) (map (fun (x : α) ↦ c) f) s ↔ Membership.mem (γ := Filter β) (pure c) s

Tactic:
by_cases h : c ∈ s
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter α
inst : f.NeBot
c : β
s : Set β
h : c ∈ s
⊢ Membership.mem (γ := Filter β) (map (fun (x : α) ↦ c) f) s ↔ Membership.mem (γ := Filter β) (pure c) s

Tactic:
simp [h]
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter α
inst : f.NeBot
c : β
s : Set β
h : c ∉ s
⊢ Membership.mem (γ := Filter β) (map (fun (x : α) ↦ c) f) s ↔ Membership.mem (γ := Filter β) (pure c) s

Tactic:
simp [h]
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
m : γ → β
n : β → α
s : Set γ
⊢ sᶜ ∈ comap m (comap n f) ↔ sᶜ ∈ comap (n ∘ m) f

Tactic:
simp only [compl_mem_comap, image_image, (· ∘ ·)]

Premises used: Set.image_image, Function.comp, Filter.compl_mem_comap
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
φ : α → β
θ : α → γ
ψ : β → δ
ρ : γ → δ
H : ψ ∘ φ = ρ ∘ θ
F : Filter α
rw : map (ψ ∘ φ) F = map ρ (map θ F)
rw₁ : map (ρ ∘ θ) F = map ρ (map θ F)
rw₂ rw₃ : map ρ (map θ F) = map ρ (map θ F)
⊢ map ψ (map φ F) = map ρ (map θ F)

Tactic:
rw [Filter.map_map, H, ← Filter.map_map]

Premises used: Filter.map_map
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
φ : α → β
θ : α → γ
ψ : β → δ
ρ : γ → δ
H : ψ ∘ φ = ρ ∘ θ
G : Filter δ
rw : comap (ψ ∘ φ) G = comap θ (comap ρ G)
rw₁ : comap (ρ ∘ θ) G = comap θ (comap ρ G)
rw₂ rw₃ : comap θ (comap ρ G) = comap θ (comap ρ G)
⊢ comap φ (comap ψ G) = comap θ (comap ρ G)

Tactic:
rw [Filter.comap_comap, H, ← Filter.comap_comap]

Premises used: Filter.comap_comap
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
ga : α → α
gb : β → β
h : Semiconj f ga gb
⊢ Semiconj (map f) (map ga) (map gb)

Tactic:
map_comm h.comp_eq

Premises used: Function.Semiconj.comp_eq, Function.Semiconj, Filter.map_comm
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
f g : α → α
h : Function.Commute f g
⊢ Function.Commute (map f) (map g)

Tactic:
h.semiconj.filter_map

Premises used: Function.Commute, Function.Semiconj.filter_map, Function.Commute.semiconj
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
ga : α → α
gb : β → β
h : Semiconj f ga gb
⊢ Semiconj (comap f) (comap gb) (comap ga)

Tactic:
comap_comm h.comp_eq.symm

Premises used: Function.Semiconj.comp_eq, Filter.comap_comm, Function.Semiconj, Eq.symm
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
f g : α → α
h : Function.Commute f g
⊢ Function.Commute (comap f) (comap g)

Tactic:
h.semiconj.filter_comap

Premises used: Function.Commute, Function.Semiconj.filter_comap, Function.Commute.semiconj
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
hfg : LeftInverse g f
F : Filter α
rw : map (g ∘ f) F = F
rw₁ : map id F = F
rw₂ rw₃ : F = F
⊢ map g (map f F) = F

Tactic:
rw [map_map, hfg.comp_eq_id, map_id]

Premises used: Filter.map_map, Filter.map_id, Function.LeftInverse.comp_eq_id
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
hfg : LeftInverse g f
F : Filter α
rw : comap (g ∘ f) F = F
rw₁ : comap id F = F
rw₂ rw₃ : F = F
⊢ comap f (comap g F) = F

Tactic:
rw [comap_comap, hfg.comp_eq_id, comap_id]

Premises used: Filter.comap_comap, Filter.comap_id, Function.LeftInverse.comp_eq_id
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
hfg : RightInverse g f
⊢ RightInverse (map g) (map f)

Tactic:
hfg.filter_map

Premises used: Function.RightInverse, Function.LeftInverse.filter_map
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
hfg : RightInverse g f
⊢ LeftInverse (comap g) (comap f)

Tactic:
hfg.filter_comap

Premises used: Function.RightInverse, Function.LeftInverse.filter_comap
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
g : β → α
hfg : LeftInvOn g f s
F : Filter α
hF : F ≤ 𝓟 s
⊢ g ∘ f =ᶠ[𝓟 s] id

Tactic:
simpa only [eventuallyEq_principal] using hfg

Premises used: Filter.eventuallyEq_principal
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
g : β → α
hfg : LeftInvOn g f s
F : Filter α
hF : F ≤ 𝓟 s
⊢ g ∘ f =ᶠ[𝓟 s] id

Tactic:
have : (g ∘ f) =ᶠ[𝓟 s] id := by simpa only [eventuallyEq_principal] using hfg
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
g : β → α
hfg : LeftInvOn g f s
F : Filter α
hF : F ≤ 𝓟 s
this : g ∘ f =ᶠ[𝓟 s] id
rw : map (g ∘ f) F = F
rw₁ : map id F = F
rw₂ rw₃ : F = F
⊢ map g (map f F) = F

Tactic:
rw [map_map, map_congr (this.filter_mono hF), map_id]

Premises used: Filter.EventuallyEq.filter_mono, Filter.map_congr, Filter.map_map, Filter.map_id
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
t : Set β
f : α → β
g : β → α
hfg : RightInvOn g f t
⊢ RightInvOn (map g) (map f) (Iic (𝓟 t))

Tactic:
hfg.filter_map_Iic

Premises used: Set.LeftInvOn.filter_map_Iic
-- 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 β
f_1 f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m_1 : α → β
m' : β → γ
s : Set α
t : Set β
m : α → β
f : Filter α
⊢ kernImage m univ = univ

Tactic:
simp [kernImage_eq_compl]

Premises used: Set.kernImage_eq_compl
-- 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 β
f_1 f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m_1 : α → β
m' : β → γ
s_1 : Set α
t_1 : Set β
m : α → β
f : Filter α
t : Set β
s : Set α
hs : s ∈ f.sets
hst : kernImage m s ⊆ t
⊢ t ∈ kernImage m '' f.sets

Tactic:
⟨s ∪ m ⁻¹' t, mem_of_superset hs subset_union_left, ?_⟩

Premises used: Set.Mem, setOf, Set.subset_union_left, Set.preimage, And.intro, Exists.intro, Set.image, Union.union, Filter.mem_of_superset
-- 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 β
f_1 f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m_1 : α → β
m' : β → γ
s_1 : Set α
t_1 : Set β
m : α → β
f : Filter α
t : Set β
s : Set α
hs : s ∈ f.sets
hst : kernImage m s ⊆ t
refine : kernImage m (s ∪ m ⁻¹' t) = t
⊢ t ∈ kernImage m '' f.sets

Tactic:
refine ⟨s ∪ m ⁻¹' t, mem_of_superset hs subset_union_left, ?_⟩