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
ι : 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
rw : kernImage m s ∪ t = t
rw₁ rw₂ : t = t
⊢ kernImage m (s ∪ m ⁻¹' t) = t

Tactic:
rw [kernImage_union_preimage, union_eq_right.mpr hst]

Premises used: Iff.mpr, Set.kernImage_union_preimage, Set.union_eq_right
-- 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 α
s₁ : Set α
h₁ : s₁ ∈ f.sets
s₂ : Set α
h₂ : s₂ ∈ f.sets
⊢ kernImage m s₁ ∩ kernImage m s₂ ∈ kernImage m '' f.sets

Tactic:
⟨s₁ ∩ s₂, f.inter_sets h₁ h₂, Set.preimage_kernImage.u_inf⟩

Premises used: Set.preimage_kernImage, Set.Mem, setOf, Filter.inter_sets, Inter.inter, GaloisConnection.u_inf, And.intro, Exists.intro, Set.image
-- 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 α
s₁ : Set α
h₁ : s₁ ∈ f.sets
s₂ : Set α
h₂ : s₂ ∈ f.sets
⊢ kernImage m s₁ ∩ kernImage m s₂ ∈ kernImage m '' f.sets

Tactic:
exact ⟨s₁ ∩ s₂, f.inter_sets h₁ h₂, Set.preimage_kernImage.u_inf⟩
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
m : α → β
f : Filter α
s : Set β
⊢ s ∈ kernMap m f ↔ ∃ t ∈ f, kernImage m t = s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.image
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
m : α → β
f : Filter α
s : Set β
rw : (∃ (x : Set α), xᶜ ∈ f ∧ kernImage m xᶜ = s) ↔ ∃ (t : Set α), tᶜ ∈ f ∧ m '' t = sᶜ
⊢ s ∈ kernMap m f ↔ ∃ (t : Set α), tᶜ ∈ f ∧ m '' t = sᶜ

Tactic:
rw [mem_kernMap, compl_surjective.exists]

Premises used: Function.Surjective.exists, compl_surjective, Filter.mem_kernMap
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
m : α → β
f : Filter α
s : Set β
⊢ (∃ (x : Set α), xᶜ ∈ f ∧ kernImage m xᶜ = s) ↔ ∃ (t : Set α), tᶜ ∈ f ∧ m '' t = sᶜ

Tactic:
exists_congr (fun x ↦ and_congr_right fun _ ↦ ?_)

Premises used: and_congr_right, exists_congr
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
m : α → β
f : Filter α
s : Set β
refine : ∀ (x : Set α), xᶜ ∈ f → (kernImage m xᶜ = s ↔ m '' x = sᶜ)
⊢ (∃ (x : Set α), xᶜ ∈ f ∧ kernImage m xᶜ = s) ↔ ∃ (t : Set α), tᶜ ∈ f ∧ m '' t = sᶜ

Tactic:
refine exists_congr (fun x ↦ and_congr_right fun _ ↦ ?_)

Premises used: and_congr_right, exists_congr
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
m : α → β
f : Filter α
s : Set β
x : Set α
h : xᶜ ∈ f
rw : (m '' x)ᶜ = s ↔ m '' x = sᶜ
rw₁ : sᶜ = m '' x ↔ m '' x = sᶜ
rw₂ rw₃ : m '' x = sᶜ ↔ m '' x = sᶜ
⊢ kernImage m xᶜ = s ↔ m '' x = sᶜ

Tactic:
rw [kernImage_compl, compl_eq_comm, eq_comm]

Premises used: Set.kernImage_compl, eq_comm, compl_eq_comm
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
m : α → β
f : Filter α
s : Set β
simp_rw : (∃ (t : Set α), tᶜ ∈ f ∧ m '' t = sᶜᶜ) ↔ ∃ (t : Set α), tᶜ ∈ f ∧ m '' t = s
⊢ sᶜ ∈ kernMap m f ↔ ∃ (t : Set α), tᶜ ∈ f ∧ m '' t = s

Tactic:
simp_rw [mem_kernMap_iff_compl, compl_compl]

Premises used: compl_compl, Filter.mem_kernMap_iff_compl
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
g : Filter β
m : α → β
f : Filter α
⊢ comap m g ≤ f ↔ g ≤ kernMap m f

Tactic:
simp [Filter.le_def, mem_comap'', mem_kernMap, -mem_comap]

Premises used: Filter.mem_comap'', Filter.mem_comap, Filter.mem_kernMap, Filter.le_def
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
m : α → β
⊢ GaloisConnection (comap m) (kernMap m)

Tactic:
fun _ _ ↦ comap_le_iff_le_kernMap

Premises used: Filter.comap_le_iff_le_kernMap, GaloisConnection
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
m : α → β
s : Set α
⊢ kernMap m (𝓟 s) = 𝓟 (kernImage m s)

Tactic:
eq_of_forall_le_iff (fun g ↦ ?_)

Premises used: eq_of_forall_le_iff
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
m : α → β
s : Set α
refine : ∀ (g : Filter β), g ≤ kernMap m (𝓟 s) ↔ g ≤ 𝓟 (kernImage m s)
⊢ kernMap m (𝓟 s) = 𝓟 (kernImage m s)

Tactic:
refine eq_of_forall_le_iff (fun g ↦ ?_)

Premises used: eq_of_forall_le_iff
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
m : α → β
s : Set α
g : Filter β
rw : comap m g ≤ 𝓟 s ↔ g ≤ 𝓟 (kernImage m s)
rw₁ : s ∈ comap m g ↔ g ≤ 𝓟 (kernImage m s)
rw₂ : s ∈ comap m g ↔ kernImage m s ∈ g
rw₃ rw₄ : kernImage m s ∈ g ↔ kernImage m s ∈ g
⊢ g ≤ kernMap m (𝓟 s) ↔ g ≤ 𝓟 (kernImage m s)

Tactic:
rw [← comap_le_iff_le_kernMap, le_principal_iff, le_principal_iff, mem_comap'']

Premises used: Filter.le_principal_iff, Filter.mem_comap'', Filter.comap_le_iff_le_kernMap
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
m : α → β
t : Set β
⊢ comap m (𝓟 t) = 𝓟 (m ⁻¹' t)

Tactic:
Filter.ext fun _ => ⟨fun ⟨_u, hu, b⟩ => (preimage_mono hu).trans b,
    fun h => ⟨t, Subset.rfl, h⟩⟩

Premises used: _private.0.Filter.comap_principal.match_1, Membership.mem, Filter.ext, HasSubset.Subset.trans, Set.preimage_mono, Set.Subset.rfl, Set.preimage, And.intro, Iff.intro, Exists.intro, Filter.principal
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_6
s : Set α
t : Set (↑s : Type u_6)
rw : 𝓟 t = 𝓟 (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t)
rw₁ rw₂ : 𝓟 t = 𝓟 t
⊢ 𝓟 t = comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓟 (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t))

Tactic:
rw [comap_principal, preimage_image_eq _ Subtype.coe_injective]

Premises used: Subtype.coe_injective, Filter.comap_principal, Set.preimage_image_eq
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
m : α → β
b : β
rw : comap m (𝓟 {b}) = 𝓟 (m ⁻¹' {b})
rw₁ rw₂ : 𝓟 (m ⁻¹' {b}) = 𝓟 (m ⁻¹' {b})
⊢ comap m (pure b) = 𝓟 (m ⁻¹' {b})

Tactic:
rw [← principal_singleton, comap_principal]

Premises used: Filter.principal_singleton, Filter.comap_principal
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
m : α → β
⊢ map m f ≤ g ↔ f ≤ comap m g

Tactic:
⟨fun h _ ⟨_, ht, hts⟩ => mem_of_superset (h ht) hts, fun h _ ht => h ⟨_, ht, Subset.rfl⟩⟩

Premises used: _private.0.Filter.map_le_iff_le_comap.match_1, Membership.mem, Set.Subset.rfl, And.intro, Iff.intro, Exists.intro, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
m : α → β
⊢ GaloisConnection (map m) (comap m)

Tactic:
fun _ _ => map_le_iff_le_comap

Premises used: Filter.map_le_iff_le_comap, GaloisConnection
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
m : α → β
⊢ Monotone (map m)

Tactic:
(gc_map_comap m).monotone_l

Premises used: Filter.gc_map_comap, GaloisConnection.monotone_l
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
m : α → β
⊢ Monotone (comap m)

Tactic:
(gc_map_comap m).monotone_u

Premises used: GaloisConnection.monotone_u, Filter.gc_map_comap
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
m : α → β
⊢ map m ⊥ = ⊥

Tactic:
(gc_map_comap m).l_bot

Premises used: GaloisConnection.l_bot, Filter.gc_map_comap
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
m : α → β
⊢ map m (f₁ ⊔ f₂) = map m f₁ ⊔ map m f₂

Tactic:
(gc_map_comap m).l_sup

Premises used: Filter.gc_map_comap, GaloisConnection.l_sup
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
m : α → β
f : ι → Filter α
⊢ map m (⨆ (i : ι), f i) = ⨆ (i : ι), map m (f i)

Tactic:
(gc_map_comap m).l_iSup

Premises used: GaloisConnection.l_iSup, Filter.gc_map_comap
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
rw : map f (𝓟 univ) = 𝓟 (range f)
rw₁ : 𝓟 (f '' univ) = 𝓟 (range f)
rw₂ rw₃ : 𝓟 (range f) = 𝓟 (range f)
⊢ map f ⊤ = 𝓟 (range f)

Tactic:
rw [← principal_univ, map_principal, image_univ]

Premises used: Set.image_univ, Filter.principal_univ, Filter.map_principal
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
m : α → β
⊢ comap m ⊤ = ⊤

Tactic:
(gc_map_comap m).u_top

Premises used: GaloisConnection.u_top, Filter.gc_map_comap
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
g₁ g₂ : Filter β
m : α → β
⊢ comap m (g₁ ⊓ g₂) = comap m g₁ ⊓ comap m g₂

Tactic:
(gc_map_comap m).u_inf

Premises used: GaloisConnection.u_inf, Filter.gc_map_comap
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
m : α → β
f : ι → Filter β
⊢ comap m (⨅ (i : ι), f i) = ⨅ (i : ι), comap m (f i)

Tactic:
(gc_map_comap m).u_iInf

Premises used: GaloisConnection.u_iInf, Filter.gc_map_comap
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
l : Filter α
rw : l ≤ ⊤
⊢ l ≤ comap f ⊤

Tactic:
rw [comap_top]

Premises used: Filter.comap_top
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
l : Filter α
⊢ l ≤ ⊤

Tactic:
le_top

Premises used: Set.Mem, le_top
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
l : Filter α
⊢ l ≤ ⊤

Tactic:
exact le_top

Premises used: le_top
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
g : Filter β
m : α → β
⊢ map m (comap m g) ≤ g

Tactic:
(gc_map_comap m).l_u_le _

Premises used: Filter.gc_map_comap, GaloisConnection.l_u_le
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter α
m : α → β
⊢ f ≤ comap m (map m f)

Tactic:
(gc_map_comap m).le_u_l _

Premises used: GaloisConnection.le_u_l, Filter.gc_map_comap
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
m : α → β
s : Set α
h : Membership.mem (γ := Filter α) ⊥ s
⊢ m ⁻¹' ∅ ⊆ s

Tactic:
simp only [empty_subset, preimage_empty]

Premises used: Set.preimage_empty, Set.empty_subset
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
g : Filter β
m : α → β
h : (comap m g).NeBot
rw : ∀ (h : comap m g ≠ ⊥), g ≠ ⊥
⊢ g.NeBot

Tactic:
rw [neBot_iff] at *

Premises used: Filter.neBot_iff
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
g : Filter β
m : α → β
h : comap m g ≠ ⊥
contrapose : ∀ (h : g = ⊥), comap m g = ⊥
⊢ g ≠ ⊥

Tactic:
contrapose h
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
g : Filter β
m : α → β
h : g = ⊥
rw : comap m ⊥ = ⊥
⊢ comap m g = ⊥

Tactic:
rw [h]
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
g : Filter β
m : α → β
h : g = ⊥
⊢ comap m ⊥ = ⊥

Tactic:
comap_bot

Premises used: Filter.comap_bot
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
g : Filter β
m : α → β
h : g = ⊥
⊢ comap m ⊥ = ⊥

Tactic:
exact comap_bot

Premises used: Filter.comap_bot
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
g : Filter β
m : α → β
⊢ comap m (g ⊓ 𝓟 (range m)) = comap m g

Tactic:
simp
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
g₁ g₂ : Filter β
m : α → β
h : Disjoint g₁ g₂
⊢ Disjoint (comap m g₁) (comap m g₂)

Tactic:
simp only [disjoint_iff, ← comap_inf, h.eq_bot, comap_bot]

Premises used: disjoint_iff, Filter.comap_inf, Filter.comap_bot, Disjoint.eq_bot
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_6
f : ι → Filter β
m : α → β
⊢ comap m (iSup f) = ⨆ (i : ι), comap m (f i)

Tactic:
(gc_comap_kernMap m).l_iSup

Premises used: Filter.gc_comap_kernMap, GaloisConnection.l_iSup
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
s : Set (Filter β)
m : α → β
⊢ comap m (sSup s) = ⨆ f ∈ s, comap m f

Tactic:
simp only [sSup_eq_iSup, comap_iSup]

Premises used: sSup_eq_iSup, Filter.comap_iSup
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
g₁ g₂ : Filter β
m : α → β
rw : comap m (⨆ (b : Bool), bif b then g₁ else g₂) = comap m g₁ ⊔ comap m g₂
rw₁ : ⨆ (i : Bool), comap m (bif i then g₁ else g₂) = comap m g₁ ⊔ comap m g₂
rw₂ : comap m (bif true then g₁ else g₂) ⊔ comap m (bif false then g₁ else g₂) = comap m g₁ ⊔ comap m g₂
rw₃ : comap m g₁ ⊔ comap m (bif false then g₁ else g₂) = comap m g₁ ⊔ comap m g₂
rw₄ rw₅ : comap m g₁ ⊔ comap m g₂ = comap m g₁ ⊔ comap m g₂
⊢ comap m (g₁ ⊔ g₂) = comap m g₁ ⊔ comap m g₂

Tactic:
rw [sup_eq_iSup, comap_iSup, iSup_bool_eq, Bool.cond_true, Bool.cond_false]

Premises used: iSup_bool_eq, Bool.cond_true, sup_eq_iSup, Filter.comap_iSup, Bool.cond_false
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
⊢ map m (comap m f) = f ⊓ 𝓟 (range m)

Tactic:
le_antisymm (le_inf map_comap_le <| le_principal_iff.2 range_mem_map) ?_

Premises used: Iff.mpr, Filter.le_principal_iff, le_inf, le_antisymm, Filter.range_mem_map, Filter.map_comap_le
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
refine : f ⊓ 𝓟 (range m) ≤ map m (comap m f)
⊢ map m (comap m f) = f ⊓ 𝓟 (range m)

Tactic:
refine le_antisymm (le_inf map_comap_le <| le_principal_iff.2 range_mem_map) ?_

Premises used: Iff.mpr, Filter.le_principal_iff, le_inf, le_antisymm, Filter.range_mem_map, Filter.map_comap_le
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
t' t : Set β
ht : t ∈ f
sub : m ⁻¹' t ⊆ m ⁻¹' t'
⊢ t' ∈ f ⊓ 𝓟 (range m)

Tactic:
mem_inf_principal.2 (mem_of_superset ht ?_)

Premises used: Iff.mpr, Filter.mem_inf_principal, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
t' t : Set β
ht : t ∈ f
sub : m ⁻¹' t ⊆ m ⁻¹' t'
refine : t ⊆ {x : β | x ∈ range m → x ∈ t'}
⊢ t' ∈ f ⊓ 𝓟 (range m)

Tactic:
refine mem_inf_principal.2 (mem_of_superset ht ?_)

Premises used: Iff.mpr, Filter.mem_inf_principal, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
t' t : Set β
ht : t ∈ f
sub : m ⁻¹' t ⊆ m ⁻¹' t'
x : α
hxt : m x ∈ t
⊢ m x ∈ t'

Tactic:
sub hxt

Premises used: Set.Mem, setOf, Set.preimage
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
t' t : Set β
ht : t ∈ f
sub : m ⁻¹' t ⊆ m ⁻¹' t'
x : α
hxt : m x ∈ t
⊢ m x ∈ t'

Tactic:
exact sub hxt
-- Module: Mathlib.Order.Filter.Map
Goal:
β : Type u_2
f : Filter β
s : Set β
rw : f ⊓ 𝓟 (range (ι := { x : β // x ∈ s }) (Subtype.val (p := fun (x : β) ↦ x ∈ s))) = f ⊓ 𝓟 s
rw₁ rw₂ : f ⊓ 𝓟 s = f ⊓ 𝓟 s
⊢ map (α := { x : β // x ∈ s }) (Subtype.val (p := fun (x : β) ↦ x ∈ s))
      (comap (Subtype.val (p := fun (x : β) ↦ x ∈ s)) f) =
    f ⊓ 𝓟 s

Tactic:
rw [map_comap, Subtype.range_val]

Premises used: Filter.map_comap, Subtype.range_val
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
hf : range m ∈ f
rw : f ⊓ 𝓟 (range m) = f
rw₁ rw₂ : f = f
⊢ map m (comap m f) = f

Tactic:
rw [map_comap, inf_eq_left.2 (le_principal_iff.2 hf)]

Premises used: Iff.mpr, Filter.le_principal_iff, Filter.map_comap, inf_eq_left
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f g : Filter β
m : α → β
hf : range m ∈ f
⊢ comap m f ≤ comap m g ↔ f ≤ g

Tactic:
⟨fun h => map_comap_of_mem hf ▸ (map_mono h).trans map_comap_le, fun h => comap_mono h⟩

Premises used: Filter.map_mono, Eq.rec, Filter.comap_mono, Filter.map_comap_of_mem, Iff.intro, LE.le.trans, Filter.map_comap_le
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
l : Filter β
⊢ range f ∈ l

Tactic:
simp only [hf.range_eq, univ_mem]

Premises used: Function.Surjective.range_eq, Filter.univ_mem
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
⊢ Injective (comap f)

Tactic:
LeftInverse.injective <| map_comap_of_surjective hf

Premises used: Function.LeftInverse.injective, Filter.map_comap_of_surjective
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
⊢ map f ⊤ = ⊤

Tactic:
(congr_arg _ comap_top).symm.trans <| map_comap_of_surjective hf ⊤

Premises used: Filter.map_comap_of_surjective, congr_arg, Filter.comap_top, Top.top, Eq.symm, Eq.trans
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
s : Set α
f : Filter α
rw : f ⊓ 𝓟 (range (ι := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))) = f ⊓ 𝓟 s
rw₁ rw₂ : f ⊓ 𝓟 s = f ⊓ 𝓟 s
⊢ map (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
      (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) f) =
    f ⊓ 𝓟 s

Tactic:
rw [map_comap, Subtype.range_coe]

Premises used: Filter.map_comap, Subtype.range_coe
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter α
c : β → α
h : range c ∈ f
W : Set β
W_in : W ∈ comap c f
rw : c '' W ∈ map c (comap c f)
⊢ c '' W ∈ f

Tactic:
rw [← map_comap_of_mem h]

Premises used: Filter.map_comap_of_mem
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter α
c : β → α
h : range c ∈ f
W : Set β
W_in : W ∈ comap c f
⊢ c '' W ∈ map c (comap c f)

Tactic:
image_mem_map W_in

Premises used: Filter.image_mem_map
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter α
c : β → α
h : range c ∈ f
W : Set β
W_in : W ∈ comap c f
⊢ c '' W ∈ map c (comap c f)

Tactic:
exact image_mem_map W_in

Premises used: Filter.image_mem_map
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
f : Filter α
U : Set α
h : U ∈ f
W : Set (↑U : Type u_1)
W_in : Membership.mem (γ := Filter { x : α // x ∈ U }) (comap (Subtype.val (p := fun (x : α) ↦ x ∈ U)) f) W
⊢ range (ι := (↑U : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ U)) ∈ f

Tactic:
simp [h]
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter α
m : α → β
h : Injective m
s : Set α
hs : s ∈ f
⊢ m ⁻¹' m '' s ⊆ s

Tactic:
simp only [preimage_image_eq s h, Subset.rfl]

Premises used: Set.Subset.rfl, Set.preimage_image_eq
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
inj : Injective m
large : range m ∈ f
S : Set α
rw : m '' S ∈ map m (comap m f) ↔ m '' S ∈ f
rw₁ rw₂ : m '' S ∈ f ↔ m '' S ∈ f
⊢ S ∈ comap m f ↔ m '' S ∈ f

Tactic:
rw [← image_mem_map_iff inj, map_comap_of_mem large]

Premises used: Filter.image_mem_map_iff, Filter.map_comap_of_mem
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
l₁ l₂ : Filter α
f : α → β
s : Set α
h₁ : s ∈ l₁
h₂ : s ∈ l₂
hinj : InjOn f s
⊢ map f l₁ ≤ map f l₂ ↔ l₁ ≤ l₂

Tactic:
⟨fun h _t ht =>
    mp_mem h₁ <|
      mem_of_superset (h <| image_mem_map (inter_mem h₂ ht)) fun _y ⟨_x, ⟨hxs, hxt⟩, hxy⟩ hys =>
        hinj hxs hys hxy ▸ hxt,
    fun h => map_mono h⟩

Premises used: Filter.map_mono, Filter.inter_mem, Membership.mem, Eq.rec, Filter.mp_mem, Filter.image_mem_map, _private.0.Filter.map_le_map_iff_of_injOn.match_1, Iff.intro, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f g : Filter α
m : α → β
hm : Injective m
rw : f ≤ comap m (map m g) ↔ f ≤ g
rw₁ rw₂ : f ≤ g ↔ f ≤ g
⊢ map m f ≤ map m g ↔ f ≤ g

Tactic:
rw [map_le_iff_le_comap, comap_map hm]

Premises used: Filter.comap_map, Filter.map_le_iff_le_comap
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f g : Filter α
m : α → β
s : Set α
hsf : s ∈ f
hsg : s ∈ g
hm : InjOn m s
⊢ map m f = map m g ↔ f = g

Tactic:
simp only [le_antisymm_iff, map_le_map_iff_of_injOn hsf hsg hm,
    map_le_map_iff_of_injOn hsg hsf hm]

Premises used: le_antisymm_iff, Filter.map_le_map_iff_of_injOn
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f g : Filter α
m : α → β
hm : Injective m
⊢ map m f = map m g ↔ f = g

Tactic:
map_eq_map_iff_of_injOn univ_mem univ_mem hm.injOn

Premises used: Function.Injective.injOn, Filter.map_eq_map_iff_of_injOn, Filter.univ_mem
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
m : α → β
hm : Injective m
⊢ Injective (map m)

Tactic:
fun _ _ =>
  (map_inj hm).1

Premises used: Iff.mp, Function.Injective, Filter.map_inj
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
simp : (∀ (s : Set α), ∀ x ∈ f, m ⁻¹' x ⊆ s → s.Nonempty) ↔ ∀ t ∈ f, ∃ (a : α), m a ∈ t
⊢ (comap m f).NeBot ↔ ∀ t ∈ f, ∃ (a : α), m a ∈ t

Tactic:
simp only [← forall_mem_nonempty_iff_neBot, mem_comap, forall_exists_index, and_imp]

Premises used: Filter.forall_mem_nonempty_iff_neBot, and_imp, forall_exists_index, Filter.mem_comap
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
⊢ (∀ (s : Set α), ∀ x ∈ f, m ⁻¹' x ⊆ s → s.Nonempty) ↔ ∀ t ∈ f, ∃ (a : α), m a ∈ t

Tactic:
⟨fun h t t_in => h (m ⁻¹' t) t t_in Subset.rfl, fun h s t ht hst => (h t ht).imp hst⟩

Premises used: Exists.imp, Set.Subset.rfl, Set.preimage, Iff.intro
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
⊢ (∀ (s : Set α), ∀ x ∈ f, m ⁻¹' x ⊆ s → s.Nonempty) ↔ ∀ t ∈ f, ∃ (a : α), m a ∈ t

Tactic:
exact ⟨fun h t t_in => h (m ⁻¹' t) t t_in Subset.rfl, fun h s t ht hst => (h t ht).imp hst⟩
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
hm : ∀ t ∈ f, ∃ (a : α), m a ∈ t
⊢ (comap m f).NeBot

Tactic:
comap_neBot_iff.mpr hm

Premises used: Iff.mpr, Filter.comap_neBot_iff
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
⊢ (comap m f).NeBot ↔ ∃ᶠ (y : β) in f, y ∈ range m

Tactic:
simp only [comap_neBot_iff, frequently_iff, mem_range, @and_comm (_ ∈ _), exists_exists_eq_and]

Premises used: Set.mem_range, Filter.frequently_iff, and_comm, exists_exists_eq_and, Filter.comap_neBot_iff
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
⊢ (comap m f).NeBot ↔ (range m)ᶜ ∉ f

Tactic:
comap_neBot_iff_frequently

Premises used: Set.Mem, Filter.Eventually, setOf, Filter.Frequently, Filter.comap_neBot_iff_frequently
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
⊢ comap m f = ⊥ ↔ (range m)ᶜ ∈ f

Tactic:
not_iff_not.mp <| neBot_iff.symm.trans comap_neBot_iff_compl_range

Premises used: not_iff_not, Filter.neBot_iff, Iff.mp, Iff.trans, Filter.comap_neBot_iff_compl_range, Iff.symm
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
hm : Surjective m
rw : (range m)ᶜ ∈ f ↔ f = ⊥
rw₁ : univᶜ ∈ f ↔ f = ⊥
rw₂ : ∅ ∈ f ↔ f = ⊥
rw₃ rw₄ : f = ⊥ ↔ f = ⊥
⊢ comap m f = ⊥ ↔ f = ⊥

Tactic:
rw [comap_eq_bot_iff_compl_range, hm.range_eq, compl_univ, empty_mem_iff_bot]

Premises used: Set.compl_univ, Function.Surjective.range_eq, Filter.comap_eq_bot_iff_compl_range, Filter.empty_mem_iff_bot
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
g₁ g₂ : Filter β
m : α → β
h : Surjective m
rw : comap m g₁ ⊓ comap m g₂ = ⊥ ↔ Disjoint g₁ g₂
rw₁ : comap m g₁ ⊓ comap m g₂ = ⊥ ↔ g₁ ⊓ g₂ = ⊥
rw₂ : comap m (g₁ ⊓ g₂) = ⊥ ↔ g₁ ⊓ g₂ = ⊥
rw₃ rw₄ : g₁ ⊓ g₂ = ⊥ ↔ g₁ ⊓ g₂ = ⊥
⊢ Disjoint (comap m g₁) (comap m g₂) ↔ Disjoint g₁ g₂

Tactic:
rw [disjoint_iff, disjoint_iff, ← comap_inf, comap_surjective_eq_bot h]

Premises used: disjoint_iff, Filter.comap_inf, Filter.comap_surjective_eq_bot
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
h : f.NeBot
hm : range m ∈ f
⊢ (comap m f).NeBot

Tactic:
comap_neBot_iff_frequently.2 <| Eventually.frequently hm

Premises used: Iff.mpr, Filter.Eventually.frequently, Filter.comap_neBot_iff_frequently
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
g : Filter β
h : ∀ (s : Set α), Membership.mem (γ := Filter α) (comap inl (map inr g)) s ↔ Membership.mem (γ := Filter α) ⊥ s
⊢ Eq.{u_1 + 1} (α := Filter α) (comap inl (map inr g)) ⊥

Tactic:
ext
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
g : Filter β
s : Set α
h : Membership.mem (γ := Filter (α ⊕ β)) (map inr g) (inl '' sᶜ)ᶜ ↔ Membership.mem (γ := Filter α) ⊥ s
⊢ Membership.mem (γ := Filter α) (comap inl (map inr g)) s ↔ Membership.mem (γ := Filter α) ⊥ s

Tactic:
rw [mem_comap_iff_compl]

Premises used: Filter.mem_comap_iff_compl
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
g : Filter β
s : Set α
⊢ Membership.mem (γ := Filter (α ⊕ β)) (map inr g) (inl '' sᶜ)ᶜ ↔ Membership.mem (γ := Filter α) ⊥ s

Tactic:
simp