awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_6
ι' : ι → Type u_7
l : ι → Filter α
p : (i : ι) → ι' i → Prop
s : (i : ι) → ι' i → Set α
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
t : Set α
⊢ Membership.mem (γ := Filter α) (⨆ (i : ι), l i) t ↔
    ∃ (i : (i : ι) → ι' i), (∀ (i_1 : ι), p i_1 (i i_1)) ∧ ⋃ (i_1 : ι), s i_1 (i i_1) ⊆ t

Tactic:
simp only [(hl _).mem_iff, Classical.skolem, forall_and, iUnion_subset_iff,
      mem_iSup]

Premises used: Classical.skolem, Filter.HasBasis.mem_iff, Set.iUnion_subset_iff, Filter.mem_iSup, forall_and
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
t u : Set α
⊢ u ∈ l ⊔ 𝓟 t ↔ ∃ (i : ι), p i ∧ s i ∪ t ⊆ u

Tactic:
simp only [(hl.sup' (hasBasis_principal t)).mem_iff, PProd.exists, and_true,
      Unique.exists_iff]

Premises used: Filter.HasBasis.mem_iff, and_true, PProd.exists, Filter.hasBasis_principal, Unique.exists_iff, Filter.HasBasis.sup'
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
x : α
⊢ (l ⊔ pure x).HasBasis p fun (i : ι) ↦ s i ∪ {x}

Tactic:
simp only [← principal_singleton, hl.sup_principal]

Premises used: Filter.HasBasis.sup_principal, Filter.principal_singleton
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
s' t : Set α
⊢ t ∈ l ⊓ 𝓟 s' ↔ ∃ (i : ι), p i ∧ s i ∩ s' ⊆ t

Tactic:
simp only [mem_inf_principal, hl.mem_iff, subset_def, mem_setOf_eq, mem_inter_iff, and_imp]

Premises used: Filter.HasBasis.mem_iff, Set.subset_def, and_imp, Set.mem_inter_iff, Set.mem_setOf_eq, Filter.mem_inf_principal
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
s' : Set α
⊢ (𝓟 s' ⊓ l).HasBasis p fun (i : ι) ↦ s' ∩ s i

Tactic:
simpa only [inf_comm, inter_comm] using hl.inf_principal s'

Premises used: inf_comm, Set.inter_comm, Filter.HasBasis.inf_principal
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
⊢ (∀ {i : ι ×' ι'}, p i.fst ∧ p' i.snd → (s i.fst ∩ s' i.snd).Nonempty) ↔
    ∀ ⦃i : ι⦄, p i → ∀ ⦃i' : ι'⦄, p' i' → (s i ∩ s' i').Nonempty

Tactic:
simp [@forall_comm _ ι']

Premises used: forall_comm
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
l l' : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
⊢ (l ⊓ l').NeBot ↔ ∀ ⦃i : ι⦄, p i → ∀ ⦃s' : Set α⦄, s' ∈ l' → (s i ∩ s').Nonempty

Tactic:
hl.inf_basis_neBot_iff l'.basis_sets

Premises used: Filter.HasBasis.inf_basis_neBot_iff, Filter.basis_sets
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
t : Set α
⊢ (l ⊓ 𝓟 t).NeBot ↔ ∀ ⦃i : ι⦄, p i → (s i ∩ t).Nonempty

Tactic:
(hl.inf_principal t).neBot_iff

Premises used: Filter.HasBasis.neBot_iff, Filter.HasBasis.inf_principal
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
⊢ ¬Disjoint l l' ↔ ¬∃ (i : ι), p i ∧ ∃ (i' : ι'), p' i' ∧ Disjoint (s i) (s' i')

Tactic:
simp only [_root_.disjoint_iff, ← Ne.eq_def, ← neBot_iff, inf_eq_inter,
    hl.inf_basis_neBot_iff hl', not_exists, not_and, bot_eq_empty, ← nonempty_iff_ne_empty]

Premises used: Filter.HasBasis.inf_basis_neBot_iff, disjoint_iff, not_exists, Filter.neBot_iff, Ne.eq_def, Set.bot_eq_empty, Set.inf_eq_inter, Set.nonempty_iff_ne_empty, not_and
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
h : Disjoint l l'
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
⊢ ∃ (i : ι), p i ∧ ∃ (i' : ι'), p' i' ∧ Disjoint (s i) (s' i')

Tactic:
(hl.disjoint_iff hl').1 h

Premises used: Filter.HasBasis.disjoint_iff, Iff.mp
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
l l' : Filter α
⊢ (l ⊓ l').NeBot ↔ ∀ ⦃s : Set α⦄, s ∈ l → ∀ ⦃s' : Set α⦄, s' ∈ l' → (s ∩ s').Nonempty

Tactic:
l.basis_sets.inf_neBot_iff

Premises used: Filter.basis_sets, Filter.HasBasis.inf_neBot_iff
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
l : Filter α
s : Set α
⊢ (l ⊓ 𝓟 s).NeBot ↔ ∀ U ∈ l, (U ∩ s).Nonempty

Tactic:
l.basis_sets.inf_principal_neBot_iff

Premises used: Filter.basis_sets, Filter.HasBasis.inf_principal_neBot_iff
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
f : Filter α
s : Set α
⊢ s ∈ f ↔ f ⊓ 𝓟 sᶜ = ⊥

Tactic:
not_iff_not.1 ((inf_principal_neBot_iff.trans ?_).symm.trans neBot_iff)

Premises used: not_iff_not, Filter.neBot_iff, Iff.mp, Iff.trans, Iff.symm, Filter.inf_principal_neBot_iff
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
f : Filter α
s : Set α
refine : (∀ U ∈ f, (U ∩ sᶜ).Nonempty) ↔ s ∉ f
⊢ s ∈ f ↔ f ⊓ 𝓟 sᶜ = ⊥

Tactic:
refine not_iff_not.1 ((inf_principal_neBot_iff.trans ?_).symm.trans neBot_iff)

Premises used: not_iff_not, Filter.neBot_iff, Iff.mp, Iff.trans, Iff.symm, Filter.inf_principal_neBot_iff
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
f : Filter α
s : Set α
h : ∀ U ∈ f, (U ∩ sᶜ).Nonempty
hs : s ∈ f
⊢ False

Tactic:
simpa [Set.not_nonempty_empty] using h s hs

Premises used: Set.not_nonempty_empty
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
f : Filter α
s : Set α
⊢ (∀ U ∈ f, (U ∩ sᶜ).Nonempty) ↔ s ∉ f

Tactic:
exact
    ⟨fun h hs => by simpa [Set.not_nonempty_empty] using h s hs, fun hs t ht =>
      inter_compl_nonempty_iff.2 fun hts => hs <| mem_of_superset ht hts⟩
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
f : Filter α
s : Set α
⊢ s ∉ f ↔ (f ⊓ 𝓟 sᶜ).NeBot

Tactic:
(not_congr mem_iff_inf_principal_compl).trans neBot_iff.symm

Premises used: Filter.neBot_iff, Iff.trans, Filter.mem_iff_inf_principal_compl, Iff.symm, not_congr
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
f : Filter α
s : Set α
rw : Disjoint f (𝓟 s) ↔ f ⊓ 𝓟 sᶜᶜ = ⊥
rw₁ : Disjoint f (𝓟 s) ↔ f ⊓ 𝓟 s = ⊥
rw₂ rw₃ : f ⊓ 𝓟 s = ⊥ ↔ f ⊓ 𝓟 s = ⊥
⊢ Disjoint f (𝓟 s) ↔ sᶜ ∈ f

Tactic:
rw [mem_iff_inf_principal_compl, compl_compl, disjoint_iff]

Premises used: compl_compl, disjoint_iff, Filter.mem_iff_inf_principal_compl
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
f : Filter α
s : Set α
rw : Disjoint f (𝓟 s) ↔ sᶜ ∈ f
rw₁ rw₂ : sᶜ ∈ f ↔ sᶜ ∈ f
⊢ Disjoint (𝓟 s) f ↔ sᶜ ∈ f

Tactic:
rw [disjoint_comm, disjoint_principal_right]

Premises used: disjoint_comm, Filter.disjoint_principal_right
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
s t : Set α
rw : Disjoint (𝓟 s) (𝓟 t) ↔ t ⊆ sᶜ
rw₁ : sᶜ ∈ 𝓟 t ↔ t ⊆ sᶜ
rw₂ rw₃ : t ⊆ sᶜ ↔ t ⊆ sᶜ
⊢ Disjoint (𝓟 s) (𝓟 t) ↔ Disjoint s t

Tactic:
rw [← subset_compl_iff_disjoint_left, disjoint_principal_left, mem_principal]

Premises used: Filter.disjoint_principal_left, Set.subset_compl_iff_disjoint_left, Filter.mem_principal
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
x y : α
⊢ Disjoint (α := Filter α) (pure x) (pure y) ↔ x ≠ y

Tactic:
simp only [← principal_singleton, disjoint_principal_principal, disjoint_singleton]

Premises used: Set.disjoint_singleton, Filter.disjoint_principal_principal, Filter.principal_singleton
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
l l' : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
⊢ Disjoint l l' ↔ ∃ (i : ι), p i ∧ (s i)ᶜ ∈ l'

Tactic:
simp only [h.disjoint_iff l'.basis_sets, id, ← disjoint_principal_left,
    (hasBasis_principal _).disjoint_iff l'.basis_sets, true_and, Unique.exists_iff]

Premises used: Filter.disjoint_principal_left, id, Filter.HasBasis.disjoint_iff, Filter.basis_sets, Filter.hasBasis_principal, Unique.exists_iff, true_and
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
l l' : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
⊢ Disjoint l' l ↔ ∃ (i : ι), p i ∧ (s i)ᶜ ∈ l'

Tactic:
disjoint_comm.trans h.disjoint_iff_left

Premises used: disjoint_comm, Filter.HasBasis.disjoint_iff_left, Iff.trans
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
f g : Filter α
⊢ f ≤ g ↔ ∀ V ∈ g, f ⊓ 𝓟 Vᶜ = ⊥

Tactic:
forall₂_congr fun _ _ => mem_iff_inf_principal_compl

Premises used: forall₂_congr, Filter.mem_iff_inf_principal_compl
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
f g : Filter α
simp :
  (∀ ⦃s : Set α⦄, s ∈ f → ∀ ⦃s' : Set α⦄, s' ∈ g → (s ∩ s').Nonempty) ↔
    ∀ {p : α → Prop}, (∀ᶠ (x : α) in f, p x) → ∀ {U : Set α}, U ∈ g → ∃ (x : α), p x ∧ x ∈ U
⊢ (f ⊓ g).NeBot ↔ ∀ {p : α → Prop}, (∀ᶠ (x : α) in f, p x) → ∃ᶠ (x : α) in g, p x

Tactic:
simp only [inf_neBot_iff, frequently_iff, and_comm]

Premises used: Filter.frequently_iff, and_comm, Filter.inf_neBot_iff
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
f g : Filter α
⊢ (∀ ⦃s : Set α⦄, s ∈ f → ∀ ⦃s' : Set α⦄, s' ∈ g → (s ∩ s').Nonempty) ↔
    ∀ {p : α → Prop}, (∀ᶠ (x : α) in f, p x) → ∀ {U : Set α}, U ∈ g → ∃ (x : α), p x ∧ x ∈ U

Tactic:
rfl
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
f g : Filter α
rw : (g ⊓ f).NeBot ↔ ∀ {p : α → Prop}, (∀ᶠ (x : α) in g, p x) → ∃ᶠ (x : α) in f, p x
⊢ (f ⊓ g).NeBot ↔ ∀ {p : α → Prop}, (∀ᶠ (x : α) in g, p x) → ∃ᶠ (x : α) in f, p x

Tactic:
rw [inf_comm]

Premises used: inf_comm
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
f g : Filter α
⊢ (g ⊓ f).NeBot ↔ ∀ {p : α → Prop}, (∀ᶠ (x : α) in g, p x) → ∃ᶠ (x : α) in f, p x

Tactic:
inf_neBot_iff_frequently_left

Premises used: Filter.inf_neBot_iff_frequently_left
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
f g : Filter α
⊢ (g ⊓ f).NeBot ↔ ∀ {p : α → Prop}, (∀ᶠ (x : α) in g, p x) → ∃ᶠ (x : α) in f, p x

Tactic:
exact inf_neBot_iff_frequently_left

Premises used: Filter.inf_neBot_iff_frequently_left
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
x : Set α
⊢ x ∈ l ↔ ∃ (i : ι), p i ∧ x ∈ 𝓟 (s i)

Tactic:
simp only [h.mem_iff, mem_principal]

Premises used: Filter.HasBasis.mem_iff, Filter.mem_principal
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
l : Filter α
s : ι → Set α
h : l.HasBasis (fun (x : ι) ↦ True) s
⊢ l = ⨅ (i : ι), 𝓟 (s i)

Tactic:
simpa only [iInf_true] using h.eq_biInf

Premises used: Filter.HasBasis.eq_biInf, iInf_true
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
s : ι → Set α
h : Directed (fun (x1 x2 : Set α) ↦ x1 ≥ x2) s
inst : Nonempty ι
t : Set α
⊢ Membership.mem (γ := Filter α) (⨅ (i : ι), 𝓟 (s i)) t ↔ ∃ (i : ι), True ∧ s i ⊆ t

Tactic:
simpa only [true_and] using mem_iInf_of_directed (h.mono_comp _ monotone_principal.dual) t

Premises used: Directed.mono_comp, Monotone.dual, Filter.mem_iInf_of_directed, true_and, Filter.monotone_principal
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
β : Type u_2
s : β → Set α
S : Set β
h : DirectedOn (s ⁻¹'o fun (x1 x2 : Set α) ↦ x1 ≥ x2) S
ne : S.Nonempty
t : Set α
⊢ Membership.mem (γ := Filter α) (⨅ i ∈ S, 𝓟 (s i)) t ↔ ∃ i ∈ S, s i ⊆ t

Tactic:
mem_biInf_of_directed ?_ ne

Premises used: Set.Mem, Filter.mem_biInf_of_directed, setOf, Set.Subset
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
β : Type u_2
s : β → Set α
S : Set β
h : DirectedOn (s ⁻¹'o fun (x1 x2 : Set α) ↦ x1 ≥ x2) S
ne : S.Nonempty
t : Set α
refine : DirectedOn ((fun (i : β) ↦ 𝓟 (s i)) ⁻¹'o fun (x1 x2 : Filter α) ↦ x1 ≥ x2) S
⊢ Membership.mem (γ := Filter α) (⨅ i ∈ S, 𝓟 (s i)) t ↔ ∃ i ∈ S, s i ⊆ t

Tactic:
refine mem_biInf_of_directed ?_ ne

Premises used: Filter.mem_biInf_of_directed
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
β : Type u_2
s : β → Set α
S : Set β
h : DirectedOn (s ⁻¹'o fun (x1 x2 : Set α) ↦ x1 ≥ x2) S
ne : S.Nonempty
t : Set α
rw :
  ∀
    (h :
      Directed (ι := { x : β // x ∈ S }) (fun (x1 x2 : Set α) ↦ x1 ≥ x2) (s ∘ Subtype.val (p := fun (x : β) ↦ x ∈ S)))
    (ne : S.Nonempty) (t : Set α),
    Directed.{u_1, u_2 + 1} (ι := { x : β // x ∈ S }) (fun (x1 x2 : Filter α) ↦ x1 ≥ x2)
      ((fun (i : β) ↦ 𝓟 (s i)) ∘ Subtype.val (p := fun (x : β) ↦ x ∈ S))
⊢ DirectedOn ((fun (i : β) ↦ 𝓟 (s i)) ⁻¹'o fun (x1 x2 : Filter α) ↦ x1 ≥ x2) S

Tactic:
rw [directedOn_iff_directed, ← directed_comp] at h ⊢

Premises used: directedOn_iff_directed, directed_comp
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
β : Type u_2
s : β → Set α
S : Set β
h : Directed (ι := { x : β // x ∈ S }) (fun (x1 x2 : Set α) ↦ x1 ≥ x2) (s ∘ Subtype.val (p := fun (x : β) ↦ x ∈ S))
ne : S.Nonempty
t : Set α
⊢ Directed.{u_1, u_2 + 1} (ι := { x : β // x ∈ S }) (fun (x1 x2 : Filter α) ↦ x1 ≥ x2)
    ((fun (i : β) ↦ 𝓟 (s i)) ∘ Subtype.val (p := fun (x : β) ↦ x ∈ S))

Tactic:
h.mono_comp _ ?_

Premises used: Directed.mono_comp
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
β : Type u_2
s : β → Set α
S : Set β
h : Directed (ι := { x : β // x ∈ S }) (fun (x1 x2 : Set α) ↦ x1 ≥ x2) (s ∘ Subtype.val (p := fun (x : β) ↦ x ∈ S))
ne : S.Nonempty
t : Set α
refine : ∀ ⦃x y : Set α⦄, x ≥ y → 𝓟 x ≥ 𝓟 y
⊢ Directed.{u_1, u_2 + 1} (ι := { x : β // x ∈ S }) (fun (x1 x2 : Filter α) ↦ x1 ≥ x2)
    ((fun (i : β) ↦ 𝓟 (s i)) ∘ Subtype.val (p := fun (x : β) ↦ x ∈ S))

Tactic:
refine h.mono_comp _ ?_

Premises used: Directed.mono_comp
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
β : Type u_2
s : β → Set α
S : Set β
h : Directed (ι := { x : β // x ∈ S }) (fun (x1 x2 : Set α) ↦ x1 ≥ x2) (s ∘ Subtype.val (p := fun (x : β) ↦ x ∈ S))
ne : S.Nonempty
t : Set α
⊢ ∀ ⦃x y : Set α⦄, x ≥ y → 𝓟 x ≥ 𝓟 y

Tactic:
fun _ _ => principal_mono.2

Premises used: Iff.mpr, Filter.principal_mono
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
β : Type u_2
s : β → Set α
S : Set β
h : Directed (ι := { x : β // x ∈ S }) (fun (x1 x2 : Set α) ↦ x1 ≥ x2) (s ∘ Subtype.val (p := fun (x : β) ↦ x ∈ S))
ne : S.Nonempty
t : Set α
⊢ ∀ ⦃x y : Set α⦄, x ≥ y → 𝓟 x ≥ 𝓟 y

Tactic:
exact fun _ _ => principal_mono.2

Premises used: Iff.mpr, Filter.principal_mono
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Type u_6
p : ι → Prop
s : ι → Set α
h : ∀ (i : ι), p i → ∀ (j : ι), p j → ∃ (k : ι), p k ∧ s k ⊆ s i ∧ s k ⊆ s j
ne : ∃ (i : ι), p i
⊢ HasBasis (⨅ (i : ι), ⨅ (_ : p i), 𝓟 (s i)) p s

Tactic:
Filter.hasBasis_biInf_principal h ne

Premises used: Filter.hasBasis_biInf_principal, Set.Mem
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
f : α → β
hl : l.HasBasis p s
t : Set β
⊢ t ∈ Filter.map f l ↔ ∃ (i : ι), p i ∧ f '' s i ⊆ t

Tactic:
simp only [mem_map, image_subset_iff, hl.mem_iff, preimage]

Premises used: Filter.HasBasis.mem_iff, Set.preimage, Set.image_subset_iff, Filter.mem_map
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
f : β → α
hl : l.HasBasis p s
t : Set β
simp : (∃ (i : ι), p i ∧ s i ⊆ {y : α | ∀ ⦃x : β⦄, f x = y → x ∈ t}) ↔ ∃ (i : ι), p i ∧ f ⁻¹' s i ⊆ t
⊢ t ∈ Filter.comap f l ↔ ∃ (i : ι), p i ∧ f ⁻¹' s i ⊆ t

Tactic:
simp only [mem_comap', hl.mem_iff]

Premises used: Filter.HasBasis.mem_iff, Filter.mem_comap'
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
f : β → α
hl : l.HasBasis p s
t : Set β
⊢ (∃ (i : ι), p i ∧ s i ⊆ {y : α | ∀ ⦃x : β⦄, f x = y → x ∈ t}) ↔ ∃ (i : ι), p i ∧ f ⁻¹' s i ⊆ t

Tactic:
exists_congr (fun i => Iff.rfl.and ?_)

Premises used: Iff.rfl, exists_congr, Iff.and
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
f : β → α
hl : l.HasBasis p s
t : Set β
refine : ∀ (i : ι), s i ⊆ {y : α | ∀ ⦃x : β⦄, f x = y → x ∈ t} ↔ f ⁻¹' s i ⊆ t
⊢ (∃ (i : ι), p i ∧ s i ⊆ {y : α | ∀ ⦃x : β⦄, f x = y → x ∈ t}) ↔ ∃ (i : ι), p i ∧ f ⁻¹' s i ⊆ t

Tactic:
refine exists_congr (fun i => Iff.rfl.and ?_)

Premises used: Iff.rfl, exists_congr, Iff.and
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
f : β → α
hl : l.HasBasis p s
t : Set β
i : ι
h : f ⁻¹' s i ⊆ t
y : α
hy : y ∈ s i
x : β
hx : f x = y
rwa : f x ∈ s i
rwa₁ rwa₂ rwa₃ rwa₄ : y ∈ s i
⊢ x ∈ f ⁻¹' s i

Tactic:
rwa [mem_preimage, hx]

Premises used: Set.mem_preimage
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
f : β → α
hl : l.HasBasis p s
t : Set β
i : ι
⊢ s i ⊆ {y : α | ∀ ⦃x : β⦄, f x = y → x ∈ t} ↔ f ⁻¹' s i ⊆ t

Tactic:
exact ⟨fun h x hx => h hx rfl, fun h y hy x hx => h <| by rwa [mem_preimage, hx]⟩
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
l : Filter β
⊢ (comap f l).HasBasis (fun (s : Set β) ↦ s ∈ l) fun (s : Set β) ↦ f ⁻¹' s

Tactic:
⟨fun _ => mem_comap⟩

Premises used: Filter.mem_comap, Filter.HasBasis.mk
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
x : α
simp : (∀ (t : Set α) (x_1 : ι), p x_1 → s x_1 ⊆ t → x ∈ t) ↔ ∀ (i : ι), p i → x ∈ s i
⊢ (∀ t ∈ l, x ∈ t) ↔ ∀ (i : ι), p i → x ∈ s i

Tactic:
simp only [h.mem_iff, exists_imp, and_imp]

Premises used: Filter.HasBasis.mem_iff, and_imp, exists_imp
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
x : α
⊢ (∀ (t : Set α) (x_1 : ι), p x_1 → s x_1 ⊆ t → x ∈ t) ↔ ∀ (i : ι), p i → x ∈ s i

Tactic:
⟨fun h i hi => h (s i) i hi Subset.rfl, fun h t i hi ht => ht (h i hi)⟩

Premises used: Set.Subset.rfl, Iff.intro
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
x : α
⊢ (∀ (t : Set α) (x_1 : ι), p x_1 → s x_1 ⊆ t → x ∈ t) ↔ ∀ (i : ι), p i → x ∈ s i

Tactic:
exact ⟨fun h i hi => h (s i) i hi Subset.rfl, fun h t i hi ht => ht (h i hi)⟩
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
inst : CompleteLattice β
f : Set α → β
h : l.HasBasis p s
hf : Monotone f
⊢ Eq.{u_2 + 1} (α := β) (⨅ t ∈ l, f t) (⨅ (i : ι), ⨅ (_ : p i), f (s i))

Tactic:
le_antisymm (le_iInf₂ fun i hi => iInf₂_le (s i) (h.mem_of_mem hi)) <|
    le_iInf₂ fun _t ht =>
      let ⟨i, hpi, hi⟩ := h.mem_iff.1 ht
      iInf₂_le_of_le i hpi (hf hi)

Premises used: iInf, Filter.HasBasis.mem_iff, iInf₂_le, iInf₂_le_of_le, LE.le, le_iInf₂, le_antisymm, Iff.mp, _private.0.Filter.HasBasis.to_hasBasis'.match_1, Filter.HasBasis.mem_of_mem
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
f : Set α → Set β
h : l.HasBasis p s
hf : Monotone f
⊢ Eq.{u_2 + 1} (α := Set β) (⋂ t ∈ l, f t) (⋂ (i : ι), ⋂ (_ : p i), f (s i))

Tactic:
h.biInf_mem hf

Premises used: Filter.HasBasis.biInf_mem, Set.iInter
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
⊢ l.ker = ⋂ (i : ι), ⋂ (_ : p i), s i

Tactic:
sInter_eq_biInter.trans <| h.biInter_mem monotone_id

Premises used: monotone_id, Set.sInter_eq_biInter, Filter.HasBasis.biInter_mem, Filter.ker, Eq.trans
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
β : Type u_2
ι'' : Type u_6
inst : Preorder ι''
l : Filter α
s : ι'' → Set α
hf : l.HasAntitoneBasis s
m : α → β
⊢ (map m l).HasAntitoneBasis fun (x : ι'') ↦ m '' s x

Tactic:
⟨HasBasis.map _ hf.toHasBasis, fun _ _ h => image_mono <| hf.2 h⟩

Premises used: Filter.HasAntitoneBasis.toHasBasis, Set.image_mono, Filter.HasBasis.map, Filter.HasAntitoneBasis.mk, Filter.HasAntitoneBasis.antitone
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
β : Type u_2
ι'' : Type u_6
inst : Preorder ι''
l : Filter α
s : ι'' → Set α
hf : l.HasAntitoneBasis s
m : β → α
⊢ (comap m l).HasAntitoneBasis fun (x : ι'') ↦ m ⁻¹' s x

Tactic:
⟨hf.1.comap _, fun _ _ h ↦ preimage_mono (hf.2 h)⟩

Premises used: Filter.HasAntitoneBasis.toHasBasis, Filter.HasAntitoneBasis.mk, Filter.HasBasis.comap, Set.preimage_mono, Filter.HasAntitoneBasis.antitone
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Type u_7
inst : Preorder ι
inst_1 : Nonempty ι
inst_2 : IsDirectedOrder ι
s : ι → Set α
hs : Antitone s
⊢ HasAntitoneBasis (⨅ (i : ι), 𝓟 (s i)) s

Tactic:
⟨hasBasis_iInf_principal hs.directed_ge, hs⟩

Premises used: Antitone.directed_ge, Filter.HasAntitoneBasis.mk, Filter.hasBasis_iInf_principal
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
la : Filter α
pa : ι → Prop
sa : ι → Set α
lb : Filter β
f : α → β
hla : la.HasBasis pa sa
simp : (∀ t ∈ lb, ∃ (i : ι), pa i ∧ sa i ⊆ f ⁻¹' t) ↔ ∀ t ∈ lb, ∃ (i : ι), pa i ∧ MapsTo f (sa i) t
⊢ Tendsto f la lb ↔ ∀ t ∈ lb, ∃ (i : ι), pa i ∧ MapsTo f (sa i) t

Tactic:
simp only [Tendsto, (hla.map f).le_iff, image_subset_iff]

Premises used: Filter.HasBasis.map, Filter.Tendsto, Filter.HasBasis.le_iff, Set.image_subset_iff
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
la : Filter α
pa : ι → Prop
sa : ι → Set α
lb : Filter β
f : α → β
hla : la.HasBasis pa sa
⊢ (∀ t ∈ lb, ∃ (i : ι), pa i ∧ sa i ⊆ f ⁻¹' t) ↔ ∀ t ∈ lb, ∃ (i : ι), pa i ∧ MapsTo f (sa i) t

Tactic:
rfl
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
β : Type u_2
ι' : Sort u_5
la : Filter α
lb : Filter β
pb : ι' → Prop
sb : ι' → Set β
f : α → β
hlb : lb.HasBasis pb sb
⊢ Tendsto f la lb ↔ ∀ (i : ι'), pb i → ∀ᶠ (x : α) in la, f x ∈ sb i

Tactic:
simp only [Tendsto, hlb.ge_iff, mem_map', Filter.Eventually]

Premises used: Filter.Eventually, Filter.HasBasis.ge_iff, Filter.mem_map', Filter.Tendsto
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
ι' : Sort u_5
la : Filter α
pa : ι → Prop
sa : ι → Set α
lb : Filter β
pb : ι' → Prop
sb : ι' → Set β
f : α → β
hla : la.HasBasis pa sa
hlb : lb.HasBasis pb sb
⊢ Tendsto f la lb ↔ ∀ (ib : ι'), pb ib → ∃ (ia : ι), pa ia ∧ ∀ x ∈ sa ia, f x ∈ sb ib

Tactic:
simp [hlb.tendsto_right_iff, hla.eventually_iff]

Premises used: Filter.HasBasis.eventually_iff, Filter.HasBasis.tendsto_right_iff
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
la : Filter α
pa : ι → Prop
sa : ι → Set α
lb : Filter β
f : α → β
H : Tendsto f la lb
hla : la.HasBasis pa sa
⊢ ∀ t ∈ lb, ∃ (i : ι), pa i ∧ MapsTo f (sa i) t

Tactic:
hla.tendsto_left_iff.1 H

Premises used: Iff.mp, Filter.HasBasis.tendsto_left_iff
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
β : Type u_2
ι' : Sort u_5
la : Filter α
lb : Filter β
pb : ι' → Prop
sb : ι' → Set β
f : α → β
H : Tendsto f la lb
hlb : lb.HasBasis pb sb
⊢ ∀ (i : ι'), pb i → ∀ᶠ (x : α) in la, f x ∈ sb i

Tactic:
hlb.tendsto_right_iff.1 H

Premises used: Iff.mp, Filter.HasBasis.tendsto_right_iff
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
ι' : Sort u_5
la : Filter α
pa : ι → Prop
sa : ι → Set α
lb : Filter β
pb : ι' → Prop
sb : ι' → Set β
f : α → β
H : Tendsto f la lb
hla : la.HasBasis pa sa
hlb : lb.HasBasis pb sb
⊢ ∀ (ib : ι'), pb ib → ∃ (ia : ι), pa ia ∧ MapsTo f (sa ia) (sb ib)

Tactic:
(hla.tendsto_iff hlb).1 H

Premises used: Filter.HasBasis.tendsto_iff, Set.MapsTo, Iff.mp
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
ι' : Sort u_5
la : Filter α
pa : ι → Prop
sa : ι → Set α
lb : Filter β
pb : ι' → Prop
sb : ι' → Set β
hla : la.HasBasis pa sa
hlb : lb.HasBasis pb sb
⊢ (la ×ˢ lb).HasBasis (fun (i : ι ×' ι') ↦ pa i.fst ∧ pb i.snd) fun (i : ι ×' ι') ↦ sa i.fst ×ˢ sb i.snd

Tactic:
(hla.comap Prod.fst).inf' (hlb.comap Prod.snd)

Premises used: Set.Mem, setOf, Set.prod, Prod.fst, Filter.HasBasis.comap, Set.preimage, Filter.HasBasis.inf', Prod.snd