awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter α
h : ∀ (s : Set β), Membership.mem (γ := Filter β) (comap inr (map inl f)) s ↔ Membership.mem (γ := Filter β) ⊥ s
⊢ Eq.{u_2 + 1} (α := Filter β) (comap inr (map inl f)) ⊥

Tactic:
ext
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter α
s : Set β
h : Membership.mem (γ := Filter (α ⊕ β)) (map inl f) (inr '' sᶜ)ᶜ ↔ Membership.mem (γ := Filter β) ⊥ s
⊢ Membership.mem (γ := Filter β) (comap inr (map inl f)) 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
f : Filter α
s : Set β
⊢ Membership.mem (γ := Filter (α ⊕ β)) (map inl f) (inr '' sᶜ)ᶜ ↔ Membership.mem (γ := Filter β) ⊥ s

Tactic:
simp
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
apply : map inl f ⊓ map inr g ≤ ⊥
⊢ map inl f ⊓ map inr g = ⊥

Tactic:
apply le_bot_iff.mp

Premises used: le_bot_iff, Iff.mp
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
trans : map inl f ⊓ map inr g ≤ map inl ⊤ ⊓ map inr ⊤
trans₁ : LE.le (α := Filter (α ⊕ β)) (map inl ⊤ ⊓ map inr ⊤) ⊥
⊢ map inl f ⊓ map inr g ≤ ⊥

Tactic:
trans map inl ⊤ ⊓ map inr ⊤

Premises used: Filter.map, Sum.inl, Sum.inr, Top.top
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
h₁ : LE.le (α := Filter (α ⊕ β)) (map inl f) (map inl ⊤)
h₂ : LE.le (α := Filter (α ⊕ β)) (map inr g) (map inr ⊤)
⊢ map inl f ⊓ map inr g ≤ map inl ⊤ ⊓ map inr ⊤

Tactic:
apply inf_le_inf

Premises used: inf_le_inf
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ LE.le (α := Filter (α ⊕ β)) (map inl f) (map inl ⊤)

Tactic:
simp
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ LE.le (α := Filter (α ⊕ β)) (map inr g) (map inr ⊤)

Tactic:
simp
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ LE.le (α := Filter (α ⊕ β)) (map inl ⊤ ⊓ map inr ⊤) ⊥

Tactic:
simp
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
rw : map inl g ⊓ map inr f = ⊥
rw₁ rw₂ : Eq (α := Filter (β ⊕ α)) ⊥ ⊥
⊢ map inr f ⊓ map inl g = ⊥

Tactic:
rw [inf_comm, map_inl_inf_map_inr]

Premises used: Filter.map_inl_inf_map_inr, inf_comm
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
l : Filter γ
m₁ : α → γ
m₂ : β → γ
h : ∀ (s : Set (α ⊕ β)), s ∈ comap (Sum.elim m₁ m₂) l ↔ s ∈ map inl (comap m₁ l) ⊔ map inr (comap m₂ l)
⊢ comap (Sum.elim m₁ m₂) l = map inl (comap m₁ l) ⊔ map inr (comap m₂ l)

Tactic:
ext s
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
l : Filter γ
m₁ : α → γ
m₂ : β → γ
s : Set (α ⊕ β)
h : (Sum.elim m₁ m₂ '' sᶜ)ᶜ ∈ l ↔ (m₁ '' (inl ⁻¹' s)ᶜ)ᶜ ∈ l ∧ (m₂ '' (inr ⁻¹' s)ᶜ)ᶜ ∈ l
⊢ s ∈ comap (Sum.elim m₁ m₂) l ↔ s ∈ map inl (comap m₁ l) ⊔ map inr (comap m₂ l)

Tactic:
simp_rw [mem_sup, mem_map, mem_comap_iff_compl]

Premises used: Filter.mem_comap_iff_compl, Filter.mem_sup, Filter.mem_map
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
l : Filter γ
m₁ : α → γ
m₂ : β → γ
s : Set (α ⊕ β)
⊢ (Sum.elim m₁ m₂ '' sᶜ)ᶜ ∈ l ↔ (m₁ '' (inl ⁻¹' s)ᶜ)ᶜ ∈ l ∧ (m₂ '' (inr ⁻¹' s)ᶜ)ᶜ ∈ l

Tactic:
simp [image_sumElim]

Premises used: Set.image_sumElim
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
l : Filter (α ⊕ β)
rw : comap (Sum.elim inl inr) l = l
rw₁ : comap id l = l
rw₂ rw₃ : l = l
⊢ map inl (comap inl l) ⊔ map inr (comap inr l) = l

Tactic:
rw [← comap_sumElim_eq, Sum.elim_inl_inr, comap_id]

Premises used: Filter.comap_sumElim_eq, Filter.comap_id, Sum.elim_inl_inr
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
l : Filter (α ⊕ β)
m₁ : α → γ
m₂ : β → γ
rw :
  map (Sum.elim m₁ m₂) (map inl (comap inl l) ⊔ map inr (comap inr l)) =
    map m₁ (comap inl (map inl (comap inl l) ⊔ map inr (comap inr l))) ⊔
      map m₂ (comap inr (map inl (comap inl l) ⊔ map inr (comap inr l)))
⊢ map (Sum.elim m₁ m₂) l = map m₁ (comap inl l) ⊔ map m₂ (comap inr l)

Tactic:
rw [← map_comap_inl_sup_map_comap_inr l]

Premises used: Filter.map_comap_inl_sup_map_comap_inr
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
l : Filter (α ⊕ β)
m₁ : α → γ
m₂ : β → γ
⊢ map (Sum.elim m₁ m₂) (map inl (comap inl l) ⊔ map inr (comap inr l)) =
    map m₁ (comap inl (map inl (comap inl l) ⊔ map inr (comap inr l))) ⊔
      map m₂ (comap inr (map inl (comap inl l) ⊔ map inr (comap inr l)))

Tactic:
simp [map_sup, map_map, comap_sup, (gc_map_comap _).u_l_u_eq_u]

Premises used: Filter.map_map, Filter.comap_sup, Filter.map_sup, Filter.gc_map_comap, GaloisConnection.u_l_u_eq_u
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter α
inl : IsEmpty β → (NeBot (α := α × β) (comap Prod.fst f) ↔ f.NeBot ∧ Nonempty β)
inr : Nonempty β → (NeBot (α := α × β) (comap Prod.fst f) ↔ f.NeBot ∧ Nonempty β)
⊢ NeBot (α := α × β) (comap Prod.fst f) ↔ f.NeBot ∧ Nonempty β

Tactic:
cases isEmpty_or_nonempty β

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter α
h : IsEmpty β
inl : ¬NeBot (α := α × β) ⊥ ↔ ¬(f.NeBot ∧ Nonempty β)
⊢ NeBot (α := α × β) (comap Prod.fst f) ↔ f.NeBot ∧ Nonempty β

Tactic:
rw [filter_eq_bot_of_isEmpty (f.comap _), ← not_iff_not]

Premises used: not_iff_not, Filter.filter_eq_bot_of_isEmpty, Filter.comap
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter α
h : IsEmpty β
⊢ ¬NeBot (α := α × β) ⊥ ↔ ¬(f.NeBot ∧ Nonempty β)

Tactic:
simp [*]
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter α
h : Nonempty β
⊢ NeBot (α := α × β) (comap Prod.fst f) ↔ f.NeBot ∧ Nonempty β

Tactic:
simp [comap_neBot_iff_frequently, *]

Premises used: Filter.comap_neBot_iff_frequently
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty β
f : Filter α
inst_1 : f.NeBot
⊢ NeBot (α := α × β) (comap Prod.fst f)

Tactic:
comap_fst_neBot_iff.2 ⟨‹_›, ‹_›⟩

Premises used: Iff.mpr, Filter.comap_fst_neBot_iff, And.intro
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter β
inl : ∀ (hα : IsEmpty α), NeBot (α := α × β) (comap Prod.snd f) ↔ Nonempty α ∧ f.NeBot
inr : ∀ (hα : Nonempty α), NeBot (α := α × β) (comap Prod.snd f) ↔ Nonempty α ∧ f.NeBot
⊢ NeBot (α := α × β) (comap Prod.snd f) ↔ Nonempty α ∧ f.NeBot

Tactic:
rcases isEmpty_or_nonempty α with hα | hα

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter β
hα : IsEmpty α
inl : ¬NeBot (α := α × β) ⊥ ↔ ¬(Nonempty α ∧ f.NeBot)
⊢ NeBot (α := α × β) (comap Prod.snd f) ↔ Nonempty α ∧ f.NeBot

Tactic:
rw [filter_eq_bot_of_isEmpty (f.comap _), ← not_iff_not]

Premises used: not_iff_not, Filter.filter_eq_bot_of_isEmpty, Filter.comap
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter β
hα : IsEmpty α
⊢ ¬NeBot (α := α × β) ⊥ ↔ ¬(Nonempty α ∧ f.NeBot)

Tactic:
simp
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter β
hα : Nonempty α
⊢ NeBot (α := α × β) (comap Prod.snd f) ↔ Nonempty α ∧ f.NeBot

Tactic:
simp [comap_neBot_iff_frequently, hα]

Premises used: Filter.comap_neBot_iff_frequently
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty α
f : Filter β
inst_1 : f.NeBot
⊢ NeBot (α := α × β) (comap Prod.snd f)

Tactic:
comap_snd_neBot_iff.2 ⟨‹_›, ‹_›⟩

Premises used: Iff.mpr, Filter.comap_snd_neBot_iff, And.intro
-- Module: Mathlib.Order.Filter.Map
Goal:
ι : Type u_6
α : ι → Type u_7
i : ι
f : Filter (α i)
inl :
  ∀ (H : IsEmpty ((j : ι) → α j)), (comap (eval (β := α) i) f).NeBot ↔ (∀ (j : ι), Nonempty.{u_7 + 1} (α j)) ∧ f.NeBot
inr :
  ∀ (H : Nonempty ((j : ι) → α j)), (comap (eval (β := α) i) f).NeBot ↔ (∀ (j : ι), Nonempty.{u_7 + 1} (α j)) ∧ f.NeBot
⊢ (comap (eval (β := α) i) f).NeBot ↔ (∀ (j : ι), Nonempty.{u_7 + 1} (α j)) ∧ f.NeBot

Tactic:
rcases isEmpty_or_nonempty (∀ j, α j) with H | H

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Order.Filter.Map
Goal:
ι : Type u_6
α : ι → Type u_7
i : ι
f : Filter (α i)
H : IsEmpty ((j : ι) → α j)
inl : ¬NeBot (α := (x : ι) → α x) ⊥ ↔ ¬((∀ (j : ι), Nonempty.{u_7 + 1} (α j)) ∧ f.NeBot)
⊢ (comap (eval (β := α) i) f).NeBot ↔ (∀ (j : ι), Nonempty.{u_7 + 1} (α j)) ∧ f.NeBot

Tactic:
rw [filter_eq_bot_of_isEmpty (f.comap _), ← not_iff_not]

Premises used: not_iff_not, Filter.filter_eq_bot_of_isEmpty, Filter.comap
-- Module: Mathlib.Order.Filter.Map
Goal:
ι : Type u_6
α : ι → Type u_7
i : ι
f : Filter (α i)
H : IsEmpty ((j : ι) → α j)
⊢ ¬NeBot (α := (x : ι) → α x) ⊥ ↔ ¬((∀ (j : ι), Nonempty.{u_7 + 1} (α j)) ∧ f.NeBot)

Tactic:
simp [← Classical.nonempty_pi]

Premises used: Classical.nonempty_pi
-- Module: Mathlib.Order.Filter.Map
Goal:
ι : Type u_6
α : ι → Type u_7
i : ι
f : Filter (α i)
H : Nonempty ((j : ι) → α j)
⊢ ∀ (j : ι), Nonempty.{u_7 + 1} (α j)

Tactic:
have : ∀ j, Nonempty (α j) := Classical.nonempty_pi.1 H
-- Module: Mathlib.Order.Filter.Map
Goal:
ι : Type u_6
α : ι → Type u_7
i : ι
f : Filter (α i)
H : Nonempty ((j : ι) → α j)
this : ∀ (j : ι), Nonempty.{u_7 + 1} (α j)
⊢ (comap (eval (β := α) i) f).NeBot ↔ (∀ (j : ι), Nonempty.{u_7 + 1} (α j)) ∧ f.NeBot

Tactic:
simp [comap_neBot_iff_frequently, *]

Premises used: Filter.comap_neBot_iff_frequently
-- Module: Mathlib.Order.Filter.Map
Goal:
ι : Type u_6
α : ι → Type u_7
inst : ∀ (j : ι), Nonempty.{u_7 + 1} (α j)
i : ι
f : Filter (α i)
⊢ (comap (eval (β := α) i) f).NeBot ↔ f.NeBot

Tactic:
simp [comap_eval_neBot_iff', *]

Premises used: Filter.comap_eval_neBot_iff'
-- Module: Mathlib.Order.Filter.Map
Goal:
ι : Type u_6
α : ι → Type u_7
inst : ∀ (j : ι), Nonempty.{u_7 + 1} (α j)
i : ι
f : Filter (α i)
inst_1 : f.NeBot
⊢ (comap (eval (β := α) i) f).NeBot

Tactic:
comap_eval_neBot_iff.2 ‹_›

Premises used: Iff.mpr, Filter.comap_eval_neBot_iff
-- Module: Mathlib.Order.Filter.Map
Goal:
γ : Type u_3
s : Set γ
l : Filter γ
h : l.NeBot
h' : l ≤ 𝓟 s
⊢ NeBot (α := { x : γ // x ∈ s }) (comap (Subtype.val (p := fun (x : γ) ↦ x ∈ s)) l)

Tactic:
h.comap_of_range_mem <| (@Subtype.range_coe γ s).symm ▸ h' (mem_principal_self s)

Premises used: Filter.mem_principal_self, Eq.rec, Subtype.range_coe, Eq.symm, Filter.NeBot.comap_of_range_mem
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
hf : f.NeBot
hm : Surjective m
⊢ (comap m f).NeBot

Tactic:
hf.comap_of_range_mem <| univ_mem' hm

Premises used: Filter.univ_mem', Filter.NeBot.comap_of_range_mem
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
hf : f.NeBot
s : Set α
hs : m '' s ∈ f
⊢ (comap m f).NeBot

Tactic:
hf.comap_of_range_mem <| mem_of_superset hs (image_subset_range _ _)

Premises used: Set.image_subset_range, Filter.NeBot.comap_of_range_mem, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter α
m : α → β
rw : ∅ ∈ map m f → ∅ ∈ f
⊢ map m f = ⊥ → f = ⊥

Tactic:
rw [← empty_mem_iff_bot, ← empty_mem_iff_bot]

Premises used: Filter.empty_mem_iff_bot
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter α
m : α → β
⊢ ∅ ∈ map m f → ∅ ∈ f

Tactic:
id

Premises used: Set.Mem, setOf, id, Set.preimage
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter α
m : α → β
⊢ ∅ ∈ map m f → ∅ ∈ f

Tactic:
exact id

Premises used: id
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter α
m : α → β
h : f = ⊥
⊢ map m f = ⊥

Tactic:
simp only [h, map_bot]

Premises used: Filter.map_bot
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter α
m : α → β
rw : map m f = ⊥ ↔ f = ⊥
rw₁ rw₂ : f = ⊥ ↔ f = ⊥
⊢ ⊥ = map m f ↔ f = ⊥

Tactic:
rw [eq_comm, map_eq_bot_iff]

Premises used: eq_comm, Filter.map_eq_bot_iff
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
F : Filter α
⊢ (map f F).NeBot ↔ F.NeBot

Tactic:
simp only [neBot_iff, Ne, map_eq_bot_iff]

Premises used: Filter.neBot_iff, Ne, Filter.map_eq_bot_iff
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter α
hf : f.NeBot
m : α → β
⊢ (Filter.map m f).NeBot

Tactic:
(map_neBot_iff m).2 hf

Premises used: Iff.mpr, Filter.map_neBot_iff
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter α
m : α → β
⊢ (Filter.map m f).NeBot → f.NeBot

Tactic:
(map_neBot_iff m).1

Premises used: Iff.mp, Filter.map_neBot_iff
-- 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 f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m : α → β
m' : β → γ
s : Set α
t : Set β
hf : f.NeBot
⊢ (map m f).NeBot

Tactic:
hf.map m

Premises used: Filter.NeBot.map
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
F : Filter β
h : ∀ (x : α), x ∈ ⋂₀ (comap f F).sets ↔ Membership.mem (γ := Set α) (⋂ U ∈ F, f ⁻¹' U) x
⊢ ⋂₀ (comap f F).sets = ⋂ U ∈ F, f ⁻¹' U

Tactic:
ext x
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
F : Filter β
x : α
this : (∀ (A : Set α), ∀ B ∈ F, f ⁻¹' B ⊆ A → x ∈ A) ↔ ∀ B ∈ F, f x ∈ B
⊢ x ∈ ⋂₀ (comap f F).sets ↔ Membership.mem (γ := Set α) (⋂ U ∈ F, f ⁻¹' U) x

Tactic:
simp only [mem_sInter, mem_iInter, Filter.mem_sets, mem_comap, this, and_imp,
      mem_preimage, exists_imp]

Premises used: Filter.mem_sets, and_imp, Set.mem_iInter, Filter.mem_comap, Set.mem_sInter, exists_imp, Set.mem_preimage
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
F : Filter β
x : α
h : (∀ (A : Set α), ∀ B ∈ F, f ⁻¹' B ⊆ A → x ∈ A) ↔ ∀ B ∈ F, f x ∈ B
⊢ x ∈ ⋂₀ (comap f F).sets ↔ Membership.mem (γ := Set α) (⋂ U ∈ F, f ⁻¹' U) x

Tactic:
suffices (∀ (A : Set α) (B : Set β), B ∈ F → f ⁻¹' B ⊆ A → x ∈ A) ↔
      ∀ B : Set β, B ∈ F → f x ∈ B by
    simp only [mem_sInter, mem_iInter, Filter.mem_sets, mem_comap, this, and_imp,
      mem_preimage, exists_imp]
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
F : Filter β
x : α
h : (∀ (A : Set α), ∀ B ∈ F, f ⁻¹' B ⊆ A → x ∈ A) → ∀ B ∈ F, f x ∈ B
h₁ : (∀ B ∈ F, f x ∈ B) → ∀ (A : Set α), ∀ B ∈ F, f ⁻¹' B ⊆ A → x ∈ A
⊢ (∀ (A : Set α), ∀ B ∈ F, f ⁻¹' B ⊆ A → x ∈ A) ↔ ∀ B ∈ F, f x ∈ B

Tactic:
constructor
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
F : Filter β
x : α
h : ∀ (A : Set α), ∀ B ∈ F, f ⁻¹' B ⊆ A → x ∈ A
U : Set β
U_in : U ∈ F
⊢ f x ∈ U

Tactic:
simpa only [Subset.rfl, forall_prop_of_true, mem_preimage] using h (f ⁻¹' U) U U_in

Premises used: Set.Subset.rfl, Set.preimage, forall_prop_of_true, Set.mem_preimage
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
F : Filter β
x : α
h : ∀ B ∈ F, f x ∈ B
V : Set α
U : Set β
U_in : U ∈ F
f_U_V : f ⁻¹' U ⊆ V
⊢ x ∈ V

Tactic:
f_U_V (h U U_in)
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
F : Filter β
x : α
h : ∀ B ∈ F, f x ∈ B
V : Set α
U : Set β
U_in : U ∈ F
f_U_V : f ⁻¹' U ⊆ V
⊢ x ∈ V

Tactic:
exact f_U_V (h U U_in)
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : ι → Filter α
m : α → β
⊢ map m (iInf f) ≤ ⨅ (i : ι), map m (f i)

Tactic:
le_iInf fun _ => map_mono <| iInf_le _ _

Premises used: Filter.map_mono, Set.Mem, le_iInf, iInf_le
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : ι → Filter α
m : α → β
hf : Directed (fun (x1 x2 : Filter α) ↦ x1 ≥ x2) f
inst : Nonempty ι
s : Set β
hs : m ⁻¹' s ∈ iInf f
i : ι
hi : m ⁻¹' s ∈ f i
⊢ map m (f i) ≤ 𝓟 s

Tactic:
simpa only [le_principal_iff, mem_map]

Premises used: Filter.le_principal_iff, Filter.mem_map
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
ι : Type w
f : ι → Filter α
m : α → β
p : ι → Prop
h : DirectedOn (f ⁻¹'o fun (x1 x2 : Filter α) ↦ x1 ≥ x2) {x : ι | p x}
ne : ∃ (i : ι), p i
⊢ Nonempty.{max 1 (w + 1)} (Subtype p)

Tactic:
haveI := nonempty_subtype.2 ne
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
ι : Type w
f : ι → Filter α
m : α → β
p : ι → Prop
h : DirectedOn (f ⁻¹'o fun (x1 x2 : Filter α) ↦ x1 ≥ x2) {x : ι | p x}
ne : ∃ (i : ι), p i
this : Nonempty.{max 1 (w + 1)} (Subtype p)
simp : map m (⨅ (x : Subtype p), f (↑x : ι)) = ⨅ (x : Subtype p), map m (f (↑x : ι))
⊢ map m (⨅ (i : ι), ⨅ (_ : p i), f i) = ⨅ (i : ι), ⨅ (_ : p i), map m (f i)

Tactic:
simp only [iInf_subtype']

Premises used: iInf_subtype'
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
ι : Type w
f : ι → Filter α
m : α → β
p : ι → Prop
h : DirectedOn (f ⁻¹'o fun (x1 x2 : Filter α) ↦ x1 ≥ x2) {x : ι | p x}
ne : ∃ (i : ι), p i
this : Nonempty.{max 1 (w + 1)} (Subtype p)
⊢ map m (⨅ (x : Subtype p), f (↑x : ι)) = ⨅ (x : Subtype p), map m (f (↑x : ι))

Tactic:
map_iInf_eq h.directed_val

Premises used: Filter.map_iInf_eq, DirectedOn.directed_val
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
ι : Type w
f : ι → Filter α
m : α → β
p : ι → Prop
h : DirectedOn (f ⁻¹'o fun (x1 x2 : Filter α) ↦ x1 ≥ x2) {x : ι | p x}
ne : ∃ (i : ι), p i
this : Nonempty.{max 1 (w + 1)} (Subtype p)
⊢ map m (⨅ (x : Subtype p), f (↑x : ι)) = ⨅ (x : Subtype p), map m (f (↑x : ι))

Tactic:
exact map_iInf_eq h.directed_val
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f g : Filter α
m : α → β
⊢ map m (f ⊓ g) ≤ map m f ⊓ map m g

Tactic:
(@map_mono _ _ m).map_inf_le f g

Premises used: Filter.map_mono, Set.Mem, Monotone.map_inf_le
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f g : Filter α
m : α → β
h : Injective m
⊢ map m (f ⊓ g) = map m f ⊓ map m g

Tactic:
map_inf_le.antisymm ?_

Premises used: Filter.map_inf_le, LE.le.antisymm
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f g : Filter α
m : α → β
h : Injective m
refine : map m f ⊓ map m g ≤ map m (f ⊓ g)
⊢ map m (f ⊓ g) = map m f ⊓ map m g

Tactic:
refine map_inf_le.antisymm ?_

Premises used: Filter.map_inf_le, LE.le.antisymm
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f g : Filter α
m : α → β
h : Injective m
t : Set β
s₁ : Set α
hs₁ : s₁ ∈ f
s₂ : Set α
hs₂ : s₂ ∈ g
ht : m ⁻¹' t = s₁ ∩ s₂
⊢ t ∈ map m f ⊓ map m g

Tactic:
mem_inf_of_inter (image_mem_map hs₁) (image_mem_map hs₂) ?_

Premises used: Filter.mem_inf_of_inter, Filter.image_mem_map
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f g : Filter α
m : α → β
h : Injective m
t : Set β
s₁ : Set α
hs₁ : s₁ ∈ f
s₂ : Set α
hs₂ : s₂ ∈ g
ht : m ⁻¹' t = s₁ ∩ s₂
refine : m '' s₁ ∩ m '' s₂ ⊆ t
⊢ t ∈ map m f ⊓ map m g

Tactic:
refine mem_inf_of_inter (image_mem_map hs₁) (image_mem_map hs₂) ?_

Premises used: Filter.mem_inf_of_inter, Filter.image_mem_map
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f g : Filter α
m : α → β
h : Injective m
t : Set β
s₁ : Set α
hs₁ : s₁ ∈ f
s₂ : Set α
hs₂ : s₂ ∈ g
ht : m ⁻¹' t = s₁ ∩ s₂
rw : m '' (s₁ ∩ s₂) ⊆ t
rw₁ : s₁ ∩ s₂ ⊆ m ⁻¹' t
rw₂ rw₃ : s₁ ∩ s₂ ⊆ s₁ ∩ s₂
⊢ m '' s₁ ∩ m '' s₂ ⊆ t

Tactic:
rw [← image_inter h, image_subset_iff, ht]

Premises used: Set.image_inter, Set.image_subset_iff
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f g : Filter α
m : α → β
t : Set α
htf : t ∈ f
htg : t ∈ g
h : InjOn m t
⊢ ∀ᶠ (x : α) in f, x ∈ t

Tactic:
htf

Premises used: Set.Mem, Filter.Eventually, setOf
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f g : Filter α
m : α → β
t : Set α
htf : t ∈ f
htg : t ∈ g
h : InjOn m t
lift :
  ∀ (f : Filter (↑t : Type u_1)),
    map m (map (Subtype.val (p := fun (x : α) ↦ x ∈ t)) f ⊓ g) =
      map m (map (Subtype.val (p := fun (x : α) ↦ x ∈ t)) f) ⊓ map m g
⊢ map m (f ⊓ g) = map m f ⊓ map m g

Tactic:
lift f to Filter t using htf

Premises used: Set.Elem, Filter
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
g : Filter α
m : α → β
t : Set α
htg : t ∈ g
h : InjOn m t
f : Filter (↑t : Type u_1)
⊢ ∀ᶠ (x : α) in g, x ∈ t

Tactic:
htg

Premises used: Set.Mem, Filter.Eventually, setOf
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
g : Filter α
m : α → β
t : Set α
htg : t ∈ g
h : InjOn m t
f : Filter (↑t : Type u_1)
lift :
  ∀ (g : Filter (↑t : Type u_1)),
    map m (map (Subtype.val (p := fun (x : α) ↦ x ∈ t)) f ⊓ map (Subtype.val (p := fun (x : α) ↦ x ∈ t)) g) =
      map m (map (Subtype.val (p := fun (x : α) ↦ x ∈ t)) f) ⊓ map m (map (Subtype.val (p := fun (x : α) ↦ x ∈ t)) g)
⊢ map m (map (Subtype.val (p := fun (x : α) ↦ x ∈ t)) f ⊓ g) =
    map m (map (Subtype.val (p := fun (x : α) ↦ x ∈ t)) f) ⊓ map m g

Tactic:
lift g to Filter t using htg

Premises used: Set.Elem, Filter
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
m : α → β
t : Set α
h : InjOn m t
f g : Filter (↑t : Type u_1)
⊢ Injective (α := { x : α // x ∈ t }) (m ∘ Subtype.val (p := fun (x : α) ↦ x ∈ t))

Tactic:
replace h : Injective (m ∘ ((↑) : t → α)) := h.injective
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
m : α → β
t : Set α
f g : Filter (↑t : Type u_1)
h : Injective (α := { x : α // x ∈ t }) (m ∘ Subtype.val (p := fun (x : α) ↦ x ∈ t))
⊢ map m (map (Subtype.val (p := fun (x : α) ↦ x ∈ t)) f ⊓ map (Subtype.val (p := fun (x : α) ↦ x ∈ t)) g) =
    map m (map (Subtype.val (p := fun (x : α) ↦ x ∈ t)) f) ⊓ map m (map (Subtype.val (p := fun (x : α) ↦ x ∈ t)) g)

Tactic:
simp only [map_map, ← map_inf Subtype.coe_injective, map_inf h]

Premises used: Filter.map_inf, Filter.map_map, Subtype.coe_injective
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_6
β : Type u_7
F G : Filter α
f : α → β
h : Disjoint (map f F) (map f G)
⊢ Disjoint F G

Tactic:
disjoint_iff.mpr <| map_eq_bot_iff.mp <| le_bot_iff.mp <| trans map_inf_le (disjoint_iff.mp h)

Premises used: le_bot_iff, Iff.mpr, Trans.trans, disjoint_iff, Filter.map_inf_le, Filter.map_eq_bot_iff, Iff.mp
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
m : α → β
hm : Injective m
f₁ f₂ : Filter α
⊢ Disjoint (map m f₁) (map m f₂) ↔ Disjoint f₁ f₂

Tactic:
simp only [disjoint_iff, ← map_inf hm, map_eq_bot_iff]

Premises used: Filter.map_inf, disjoint_iff, Filter.map_eq_bot_iff
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
f : Filter β
rw :
  Eq (α := Filter β) (map (comp.{u_2 + 1, u_1 + 1, u_2 + 1} (β := α) (⇑e : (a : α) → β) (⇑e.symm : (a : β) → α)) f)
    (map.{u_1, u_2} (α := α) (⇑e : (a : α) → β) (comap (⇑e : (a : α) → β) f))
rw₁ : map id f = map.{u_1, u_2} (α := α) (⇑e : (a : α) → β) (comap (⇑e : (a : α) → β) f)
rw₂ : f = map.{u_1, u_2} (α := α) (⇑e : (a : α) → β) (comap (⇑e : (a : α) → β) f)
rw₃ rw₄ : f = f
⊢ Eq.{u_2 + 1} (α := Filter β) (map.{u_1, u_2} (α := α) (⇑e : (a : α) → β) (map (⇑e.symm : (a : β) → α) f))
    (map.{u_1, u_2} (α := α) (⇑e : (a : α) → β) (comap (⇑e : (a : α) → β) f))

Tactic:
rw [map_map, e.self_comp_symm, map_id, map_comap_of_surjective e.surjective]

Premises used: Filter.map_map, Filter.map_comap_of_surjective, Equiv.self_comp_symm, Filter.map_id, Equiv.surjective
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter α
m : α → β
n : β → α
h₁ : m ∘ n = id
h₂ : n ∘ m = id
⊢ map m f = comap n f

Tactic:
map_equiv_symm ⟨n, m, congr_fun h₁, congr_fun h₂⟩ f

Premises used: Equiv.mk, congr_fun, Filter.map_equiv_symm
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
f : Filter α
⊢ Eq.{u_2 + 1} (α := Filter β) (comap (⇑e.symm : (a : β) → α) f) (map (⇑e : (a : α) → β) f)

Tactic:
(map_eq_comap_of_inverse e.self_comp_symm e.symm_comp_self).symm

Premises used: Equiv.symm_comp_self, Filter.map_eq_comap_of_inverse, Equiv.self_comp_symm, Eq.symm
-- Module: Mathlib.Order.Filter.Map
Goal:
α : Type u_1
β : Type u_2
f : Filter (α × β)
⊢ map Prod.swap f = comap Prod.swap f

Tactic:
map_eq_comap_of_inverse Prod.swap_swap_eq Prod.swap_swap_eq

Premises used: Prod.swap_swap_eq, Filter.map_eq_comap_of_inverse