awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.Ker
Goal:
ι : Sort u_1
α : Type u_2
f : ι → Filter α
x : α
s : (i : ι) → Set α
hsf : ∀ (i : ι), s i ∈ f i
hxs : ∀ (i : ι), x ∉ s i
⊢ x ∉ ⋃ (i : ι), s i

Tactic:
simpa
-- Module: Mathlib.Order.Filter.Ker
Goal:
ι : Sort u_1
α : Type u_2
f : ι → Filter α
x : α
s : (i : ι) → Set α
hsf : ∀ (i : ι), s i ∈ f i
hxs : ∀ (i : ι), x ∉ s i
refine : Membership.mem (γ := Filter α) (⨆ (i : ι), f i) (⋃ (i : ι), s i)
⊢ ∃ (s : Set α), Membership.mem (γ := Filter α) (⨆ (i : ι), f i) s ∧ x ∉ s

Tactic:
refine ⟨⋃ i, s i, ?_, by simpa⟩
-- Module: Mathlib.Order.Filter.Ker
Goal:
ι : Sort u_1
α : Type u_2
f : ι → Filter α
x : α
s : (i : ι) → Set α
hsf : ∀ (i : ι), s i ∈ f i
hxs : ∀ (i : ι), x ∉ s i
⊢ Membership.mem (γ := Filter α) (⨆ (i : ι), f i) (⋃ (i : ι), s i)

Tactic:
mem_iSup.2 fun i ↦ mem_of_superset (hsf i) (subset_iUnion s i)

Premises used: Iff.mpr, Filter.mem_iSup, Set.subset_iUnion, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.Ker
Goal:
ι : Sort u_1
α : Type u_2
f : ι → Filter α
x : α
s : (i : ι) → Set α
hsf : ∀ (i : ι), s i ∈ f i
hxs : ∀ (i : ι), x ∉ s i
⊢ Membership.mem (γ := Filter α) (⨆ (i : ι), f i) (⋃ (i : ι), s i)

Tactic:
exact mem_iSup.2 fun i ↦ mem_of_superset (hsf i) (subset_iUnion s i)

Premises used: Iff.mpr, Filter.mem_iSup, Set.subset_iUnion, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.Ker
Goal:
α : Type u_2
S : Set (Filter α)
⊢ (sSup S).ker = ⋃ f ∈ S, f.ker

Tactic:
simp [sSup_eq_iSup]

Premises used: sSup_eq_iSup
-- Module: Mathlib.Order.Filter.Ker
Goal:
α : Type u_2
f g : Filter α
rw : ker (sSup {f, g}) = f.ker ∪ g.ker
rw₁ : ⋃ (f_1 : Filter α), ⋃ (_ : Membership.mem (γ := Set (Filter α)) {f, g} f_1), f_1.ker = f.ker ∪ g.ker
rw₂ rw₃ : f.ker ∪ g.ker = f.ker ∪ g.ker
⊢ (f ⊔ g).ker = f.ker ∪ g.ker

Tactic:
rw [← sSup_pair, ker_sSup, biUnion_pair]

Premises used: sSup_pair, Filter.ker_sSup, Set.biUnion_pair
-- Module: Mathlib.Order.Filter.Ker
Goal:
α : Type u_2
β : Type u_3
f : Filter α
g : Filter β
⊢ (f ×ˢ g).ker = f.ker ×ˢ g.ker

Tactic:
simp [Set.prod_eq, Filter.prod_eq_inf]

Premises used: Filter.prod_eq_inf, Set.prod_eq
-- Module: Mathlib.Order.Filter.Ker
Goal:
ι : Type u_4
α : ι → Type u_5
f : (i : ι) → Filter (α i)
⊢ (pi (α := α) f).ker = Set.pi (α := α) univ fun (i : ι) ↦ (f i).ker

Tactic:
simp [Set.pi_def, Filter.pi]

Premises used: Filter.pi, Set.pi_def
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
g : Set α → Filter β
⊢ Filter.lift ⊤ g = g univ

Tactic:
simp [Filter.lift]

Premises used: Filter.lift
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
γ : Type u_3
ι : Sort u_6
p : ι → Prop
s_1 : ι → Set α
f : Filter α
hf : f.HasBasis p s_1
β : ι → Type u_5
pg : (i : ι) → β i → Prop
sg : (i : ι) → β i → Set γ
g : Set α → Filter γ
hg : ∀ (i : ι), (g (s_1 i)).HasBasis (pg i) (sg i)
gm : Monotone g
s : Set γ
⊢ s ∈ f.lift g ↔ ∃ (i : ι), p i ∧ ∃ (x : β i), pg i x ∧ sg i x ⊆ s

Tactic:
(mem_biInf_of_directed ?_ ⟨univ, univ_sets _⟩).trans ?_

Premises used: Set.Mem, Set.univ, Filter.mem_biInf_of_directed, setOf, Exists.intro, Iff.trans, Filter.univ_sets
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
γ : Type u_3
ι : Sort u_6
p : ι → Prop
s_1 : ι → Set α
f : Filter α
hf : f.HasBasis p s_1
β : ι → Type u_5
pg : (i : ι) → β i → Prop
sg : (i : ι) → β i → Set γ
g : Set α → Filter γ
hg : ∀ (i : ι), (g (s_1 i)).HasBasis (pg i) (sg i)
gm : Monotone g
s : Set γ
refine_1 : DirectedOn (g ⁻¹'o fun (x1 x2 : Filter γ) ↦ x1 ≥ x2) f.sets
refine_2 : (∃ i ∈ f.sets, s ∈ g i) ↔ ∃ (i : ι), p i ∧ ∃ (x : β i), pg i x ∧ sg i x ⊆ s
⊢ s ∈ f.lift g ↔ ∃ (i : ι), p i ∧ ∃ (x : β i), pg i x ∧ sg i x ⊆ s

Tactic:
refine (mem_biInf_of_directed ?_ ⟨univ, univ_sets _⟩).trans ?_

Premises used: Set.univ, Filter.mem_biInf_of_directed, Exists.intro, Iff.trans, Filter.univ_sets
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
γ : Type u_3
ι : Sort u_6
p : ι → Prop
s_1 : ι → Set α
f : Filter α
hf : f.HasBasis p s_1
β : ι → Type u_5
pg : (i : ι) → β i → Prop
sg : (i : ι) → β i → Set γ
g : Set α → Filter γ
hg : ∀ (i : ι), (g (s_1 i)).HasBasis (pg i) (sg i)
gm : Monotone g
s : Set γ
t₁ : Set α
ht₁ : t₁ ∈ f.sets
t₂ : Set α
ht₂ : t₂ ∈ f.sets
⊢ ∃ z ∈ f.sets, (g ⁻¹'o fun (x1 x2 : Filter γ) ↦ x1 ≥ x2) t₁ z ∧ (g ⁻¹'o fun (x1 x2 : Filter γ) ↦ x1 ≥ x2) t₂ z

Tactic:
⟨t₁ ∩ t₂, inter_mem ht₁ ht₂, gm inter_subset_left, gm inter_subset_right⟩

Premises used: Filter.inter_mem, Set.inter_subset_left, Inter.inter, And.intro, Exists.intro, Set.inter_subset_right
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
γ : Type u_3
ι : Sort u_6
p : ι → Prop
s_1 : ι → Set α
f : Filter α
hf : f.HasBasis p s_1
β : ι → Type u_5
pg : (i : ι) → β i → Prop
sg : (i : ι) → β i → Set γ
g : Set α → Filter γ
hg : ∀ (i : ι), (g (s_1 i)).HasBasis (pg i) (sg i)
gm : Monotone g
s : Set γ
t₁ : Set α
ht₁ : t₁ ∈ f.sets
t₂ : Set α
ht₂ : t₂ ∈ f.sets
⊢ ∃ z ∈ f.sets, (g ⁻¹'o fun (x1 x2 : Filter γ) ↦ x1 ≥ x2) t₁ z ∧ (g ⁻¹'o fun (x1 x2 : Filter γ) ↦ x1 ≥ x2) t₂ z

Tactic:
exact ⟨t₁ ∩ t₂, inter_mem ht₁ ht₂, gm inter_subset_left, gm inter_subset_right⟩
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
γ : Type u_3
ι : Sort u_6
p : ι → Prop
s_1 : ι → Set α
f : Filter α
hf : f.HasBasis p s_1
β : ι → Type u_5
pg : (i : ι) → β i → Prop
sg : (i : ι) → β i → Set γ
g : Set α → Filter γ
hg : ∀ (i : ι), (g (s_1 i)).HasBasis (pg i) (sg i)
gm : Monotone g
s : Set γ
refine_2 : (∃ i ∈ f.sets, s ∈ g i) ↔ ∃ (i : ι), p i ∧ s ∈ g (s_1 i)
⊢ (∃ i ∈ f.sets, s ∈ g i) ↔ ∃ (i : ι), p i ∧ ∃ (x : β i), pg i x ∧ sg i x ⊆ s

Tactic:
simp only [← (hg _).mem_iff]

Premises used: Filter.HasBasis.mem_iff
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
γ : Type u_3
ι : Sort u_6
p : ι → Prop
s_1 : ι → Set α
f : Filter α
hf : f.HasBasis p s_1
β : ι → Type u_5
pg : (i : ι) → β i → Prop
sg : (i : ι) → β i → Set γ
g : Set α → Filter γ
hg : ∀ (i : ι), (g (s_1 i)).HasBasis (pg i) (sg i)
gm : Monotone g
s : Set γ
⊢ (∃ i ∈ f.sets, s ∈ g i) ↔ ∃ (i : ι), p i ∧ s ∈ g (s_1 i)

Tactic:
hf.exists_iff fun t₁ t₂ ht H => gm ht H

Premises used: Filter.HasBasis.exists_iff
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
γ : Type u_3
ι : Sort u_6
p : ι → Prop
s_1 : ι → Set α
f : Filter α
hf : f.HasBasis p s_1
β : ι → Type u_5
pg : (i : ι) → β i → Prop
sg : (i : ι) → β i → Set γ
g : Set α → Filter γ
hg : ∀ (i : ι), (g (s_1 i)).HasBasis (pg i) (sg i)
gm : Monotone g
s : Set γ
⊢ (∃ i ∈ f.sets, s ∈ g i) ↔ ∃ (i : ι), p i ∧ s ∈ g (s_1 i)

Tactic:
exact hf.exists_iff fun t₁ t₂ ht H => gm ht H

Premises used: Filter.HasBasis.exists_iff
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
γ : Type u_3
ι : Type u_6
p : ι → Prop
s : ι → Set α
f : Filter α
hf : f.HasBasis p s
β : ι → Type u_5
pg : (i : ι) → β i → Prop
sg : (i : ι) → β i → Set γ
g : Set α → Filter γ
hg : ∀ (i : ι), (g (s i)).HasBasis (pg i) (sg i)
gm : Monotone g
⊢ (f.lift g).HasBasis
    (fun (i : (i : ι) × β i) ↦
      p (i.fst (β := fun (i : ι) ↦ β i)) ∧ pg (i.fst (β := fun (i : ι) ↦ β i)) (i.snd (β := fun (i : ι) ↦ β i)))
    fun (i : (i : ι) × β i) ↦ sg (i.fst (β := fun (i : ι) ↦ β i)) (i.snd (β := fun (i : ι) ↦ β i))

Tactic:
⟨fun t => (hf.mem_lift_iff hg gm).trans ?_⟩

Premises used: Filter.HasBasis.mk, Iff.trans, Filter.HasBasis.mem_lift_iff
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
γ : Type u_3
ι : Type u_6
p : ι → Prop
s : ι → Set α
f : Filter α
hf : f.HasBasis p s
β : ι → Type u_5
pg : (i : ι) → β i → Prop
sg : (i : ι) → β i → Set γ
g : Set α → Filter γ
hg : ∀ (i : ι), (g (s i)).HasBasis (pg i) (sg i)
gm : Monotone g
refine :
  ∀ (t : Set γ),
    (∃ (i : ι), p i ∧ ∃ (x : β i), pg i x ∧ sg i x ⊆ t) ↔
      ∃ (i : (i : ι) × β i),
        (p (i.fst (β := fun (i : ι) ↦ β i)) ∧ pg (i.fst (β := fun (i : ι) ↦ β i)) (i.snd (β := fun (i : ι) ↦ β i))) ∧
          sg (i.fst (β := fun (i : ι) ↦ β i)) (i.snd (β := fun (i : ι) ↦ β i)) ⊆ t
⊢ (f.lift g).HasBasis
    (fun (i : (i : ι) × β i) ↦
      p (i.fst (β := fun (i : ι) ↦ β i)) ∧ pg (i.fst (β := fun (i : ι) ↦ β i)) (i.snd (β := fun (i : ι) ↦ β i)))
    fun (i : (i : ι) × β i) ↦ sg (i.fst (β := fun (i : ι) ↦ β i)) (i.snd (β := fun (i : ι) ↦ β i))

Tactic:
refine ⟨fun t => (hf.mem_lift_iff hg gm).trans ?_⟩
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
γ : Type u_3
ι : Type u_6
p : ι → Prop
s : ι → Set α
f : Filter α
hf : f.HasBasis p s
β : ι → Type u_5
pg : (i : ι) → β i → Prop
sg : (i : ι) → β i → Set γ
g : Set α → Filter γ
hg : ∀ (i : ι), (g (s i)).HasBasis (pg i) (sg i)
gm : Monotone g
t : Set γ
⊢ (∃ (i : ι), p i ∧ ∃ (x : β i), pg i x ∧ sg i x ⊆ t) ↔
    ∃ (i : (i : ι) × β i),
      (p (i.fst (β := fun (i : ι) ↦ β i)) ∧ pg (i.fst (β := fun (i : ι) ↦ β i)) (i.snd (β := fun (i : ι) ↦ β i))) ∧
        sg (i.fst (β := fun (i : ι) ↦ β i)) (i.snd (β := fun (i : ι) ↦ β i)) ⊆ t

Tactic:
simp [Sigma.exists, and_assoc, exists_and_left]

Premises used: Sigma.exists, exists_and_left, and_assoc
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Set α → Filter β
hg : Monotone g
s : Set β
⊢ (∃ i ∈ f, ∃ x ∈ g i, id x ⊆ s) ↔ ∃ t ∈ f, s ∈ g t

Tactic:
simp only [id, exists_mem_subset_iff]

Premises used: Filter.exists_mem_subset_iff, id
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Set α → Filter β
hg : Monotone g
⊢ Eq.{u_2 + 1} (α := Set β) (⋂₀ {s : Set β | s ∈ f.lift g}) (⋂ s ∈ f, ⋂₀ {t : Set β | t ∈ g s})

Tactic:
simp only [sInter_eq_biInter, mem_setOf_eq, mem_lift_sets hg, iInter_exists,
    iInter_and, @iInter_comm _ (Set β)]

Premises used: Set.mem_setOf_eq, Set.sInter_eq_biInter, Set.iInter_exists, Filter.mem_lift_sets, Set.iInter_comm, Set.iInter_and
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Set α → Filter β
s : Set β
t : Set α
ht : t ∈ f
hs : s ∈ g t
⊢ s ∈ f.lift g

Tactic:
le_principal_iff.mp <|
    show f.lift g ≤ 𝓟 s from iInf_le_of_le t <| iInf_le_of_le ht <| le_principal_iff.mpr hs

Premises used: Iff.mpr, Filter.le_principal_iff, Iff.mp, iInf_le_of_le
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Set α → Filter β
h : Filter β
s : Set α
hs : s ∈ f
hg : g s ≤ h
⊢ f.lift g ≤ h

Tactic:
iInf₂_le_of_le s hs hg

Premises used: Set.Mem, setOf, iInf₂_le_of_le
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Set α → Filter β
h : Filter β
⊢ h ≤ f.lift g ↔ ∀ s ∈ f, h ≤ g s

Tactic:
le_iInf₂_iff

Premises used: Set.Mem, setOf, le_iInf₂_iff
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : Set α → Filter β
hf : f₁ ≤ f₂
hg : g₁ ≤ g₂
⊢ f₁.lift g₁ ≤ f₂.lift g₂

Tactic:
iInf_mono fun s => iInf_mono' fun hs => ⟨hf hs, hg s⟩

Premises used: Set.Mem, iInf_mono, Exists.intro, iInf_mono'
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g₁ g₂ : Set α → Filter β
hg : ∀ s ∈ f, g₁ s ≤ g₂ s
⊢ f.lift g₁ ≤ f.lift g₂

Tactic:
iInf₂_mono hg

Premises used: Set.Mem, setOf, iInf₂_mono
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Set α → Filter β
m : γ → β
l : Filter γ
⊢ Tendsto m l (f.lift g) ↔ ∀ s ∈ f, Tendsto m l (g s)

Tactic:
simp only [Filter.lift, tendsto_iInf]

Premises used: Filter.lift, Filter.tendsto_iInf
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Set α → Filter β
m : β → γ
hg : Monotone g
this : Monotone (map m ∘ g)
s : Set γ
⊢ s ∈ map m (f.lift g) ↔ s ∈ f.lift (map m ∘ g)

Tactic:
simp only [mem_lift_sets hg, mem_lift_sets this, mem_map, Function.comp_apply]

Premises used: Filter.mem_lift_sets, Function.comp_apply, Filter.mem_map
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Set α → Filter β
m : γ → β
simp : Eq.{u_3 + 1} (α := Filter γ) (⨅ i ∈ f, comap m (g i)) (⨅ s ∈ f, (comap m ∘ g) s)
⊢ comap m (f.lift g) = f.lift (comap m ∘ g)

Tactic:
simp only [Filter.lift, comap_iInf]

Premises used: Filter.comap_iInf, Filter.lift
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Set α → Filter β
m : γ → β
⊢ Eq.{u_3 + 1} (α := Filter γ) (⨅ i ∈ f, comap m (g i)) (⨅ s ∈ f, (comap m ∘ g) s)

Tactic:
rfl
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
m : β → α
g : Set β → Filter γ
hg : Monotone g
⊢ (comap m f).lift g = f.lift (g ∘ preimage m)

Tactic:
le_antisymm (le_iInf₂ fun s hs => iInf₂_le (m ⁻¹' s) ⟨s, hs, Subset.rfl⟩)
    (le_iInf₂ fun _s ⟨s', hs', h_sub⟩ => iInf₂_le_of_le s' hs' <| hg h_sub)

Premises used: iInf₂_le, Function.comp, iInf₂_le_of_le, LE.le, le_iInf₂, le_antisymm, _private.0.Filter.comap_lift_eq2.match_1, Set.preimage, Filter.lift
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Set β → Filter γ
m : α → β
⊢ (map m f).lift g ≤ f.lift (g ∘ image m)

Tactic:
le_lift.2 fun _s hs => lift_le (image_mem_map hs) le_rfl

Premises used: Iff.mpr, le_rfl, Filter.lift_le, Filter.image_mem_map, Filter.le_lift
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Set β → Filter γ
m : α → β
hg : Monotone g
⊢ (map m f).lift g = f.lift (g ∘ image m)

Tactic:
lift_map_le.antisymm <| le_lift.2 fun _s hs => lift_le hs <| hg <| image_preimage_subset _ _

Premises used: Iff.mpr, Filter.lift_le, LE.le.antisymm, Filter.le_lift, Filter.lift_map_le, Set.image_preimage_subset
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Filter β
h : Set α → Set β → Filter γ
⊢ Eq.{u_3 + 1} (α := Filter γ) (f.lift fun (s : Set α) ↦ g.lift (h s))
    (g.lift fun (t : Set β) ↦ f.lift fun (s : Set α) ↦ h s t)

Tactic:
le_antisymm
    (le_iInf fun i => le_iInf fun hi => le_iInf fun j => le_iInf fun hj =>
      iInf_le_of_le j <| iInf_le_of_le hj <| iInf_le_of_le i <| iInf_le _ hi)
    (le_iInf fun i => le_iInf fun hi => le_iInf fun j => le_iInf fun hj =>
      iInf_le_of_le j <| iInf_le_of_le hj <| iInf_le_of_le i <| iInf_le _ hi)

Premises used: le_iInf, le_antisymm, iInf_le_of_le, iInf_le
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Set α → Filter β
h : Set β → Filter γ
hg : Monotone g
⊢ (f.lift g).lift h = f.lift fun (s : Set α) ↦ (g s).lift h

Tactic:
le_antisymm
    (le_iInf₂ fun _s hs => le_iInf₂ fun t ht =>
      iInf_le_of_le t <| iInf_le _ <| (mem_lift_sets hg).mpr ⟨_, hs, ht⟩)
    (le_iInf₂ fun t ht =>
      let ⟨s, hs, h'⟩ := (mem_lift_sets hg).mp ht
      iInf_le_of_le s <| iInf_le_of_le hs <| iInf_le_of_le t <| iInf_le _ h')

Premises used: Iff.mpr, LE.le, le_iInf₂, le_antisymm, Filter.mem_lift_sets, _private.0.Filter.lift_assoc.match_1, Filter.lift, And.intro, Exists.intro, Iff.mp, iInf_le_of_le, iInf_le
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Set α → Set α → Filter β
⊢ LE.le.{u_2} (α := Filter β) (f.lift fun (s : Set α) ↦ f.lift (g s)) (f.lift fun (s : Set α) ↦ g s s)

Tactic:
le_lift.2 fun _s hs => lift_le hs <| lift_le hs le_rfl

Premises used: Iff.mpr, le_rfl, Filter.lift_le, Filter.le_lift
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Set α → Set α → Filter β
hg₁ : ∀ (s : Set α), Monotone.{u_1, u_2} (β := Filter β) fun (t : Set α) ↦ g s t
hg₂ : ∀ (t : Set α), Monotone.{u_1, u_2} (β := Filter β) fun (s : Set α) ↦ g s t
⊢ Eq.{u_2 + 1} (α := Filter β) (f.lift fun (s : Set α) ↦ f.lift (g s)) (f.lift fun (s : Set α) ↦ g s s)

Tactic:
lift_lift_same_le_lift.antisymm <|
    le_lift.2 fun s hs => le_lift.2 fun t ht => lift_le (inter_mem hs ht) <|
      calc
        g (s ∩ t) (s ∩ t) ≤ g s (s ∩ t) := hg₂ (s ∩ t) inter_subset_left
        _ ≤ g s t := hg₁ s inter_subset_right

Premises used: Iff.mpr, Trans.trans, Filter.inter_mem, Filter.lift_le, LE.le.antisymm, Set.inter_subset_left, Filter.le_lift, Inter.inter, Filter.lift_lift_same_le_lift, Set.inter_subset_right
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
g : Set α → Filter β
s : Set α
hg : Monotone g
⊢ (𝓟 s).lift g = g s

Tactic:
(lift_le (mem_principal_self _) le_rfl).antisymm (le_lift.2 fun _t ht => hg ht)

Premises used: Iff.mpr, Filter.mem_principal_self, le_rfl, Filter.lift_le, LE.le.antisymm, Filter.le_lift
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder γ
f : γ → Filter α
g : γ → Set α → Filter β
hf : Monotone f
hg : Monotone g
⊢ Monotone.{u_3, u_2} (β := Filter β) fun (c : γ) ↦ (f c).lift (g c)

Tactic:
fun _ _ h => lift_mono (hf h) (hg h)

Premises used: Set.Mem, Monotone, Filter.lift_mono
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Set α → Filter β
hm : Monotone g
⊢ (f.lift g).NeBot ↔ ∀ s ∈ f, (g s).NeBot

Tactic:
simp only [neBot_iff, Ne, ← empty_mem_iff_bot, mem_lift_sets hm, not_exists, not_and]

Premises used: not_exists, Filter.neBot_iff, Ne, Filter.mem_lift_sets, Filter.empty_mem_iff_bot, not_and
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ (f.lift fun (x : Set α) ↦ g) = g

Tactic:
iInf_subtype'.trans iInf_const

Premises used: iInf_subtype', Filter.lift, iInf_const, Eq.trans
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g h : Set α → Filter β
⊢ (f.lift fun (x : Set α) ↦ g x ⊓ h x) = f.lift g ⊓ f.lift h

Tactic:
simp only [Filter.lift, iInf_inf_eq]

Premises used: Filter.lift, iInf_inf_eq
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
f : Filter α
s : Set α
hs : s ∈ f
⊢ f ≤ 𝓟 s

Tactic:
simp only [hs, le_principal_iff]

Premises used: Filter.le_principal_iff
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
f : ι → Filter α
g : Set α → Filter β
⊢ (iInf f).lift g ≤ ⨅ (i : ι), (f i).lift g

Tactic:
le_iInf fun _ => lift_mono (iInf_le _ _) le_rfl

Premises used: le_rfl, Set.Mem, le_iInf, iInf_le, Filter.lift_mono
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
⊢ (iInf f).lift g = ⨅ (i : ι), (f i).lift g

Tactic:
lift_iInf_le.antisymm fun s => ?_

Premises used: Filter.lift_iInf_le, LE.le.antisymm
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
refine : ∀ s ∈ (iInf f).lift g, Membership.mem (γ := Filter β) (⨅ (i : ι), (f i).lift g) s
⊢ (iInf f).lift g = ⨅ (i : ι), (f i).lift g

Tactic:
refine lift_iInf_le.antisymm fun s => ?_

Premises used: Filter.lift_iInf_le, LE.le.antisymm
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
s : Set β
t : Set α
ht : t ∈ iInf f
⊢ ⨅ (i : ι), (f i).lift g ≤ g t

Tactic:
iInf_sets_induct ht ?_ fun hs ht => ?_

Premises used: Filter.iInf_sets_induct
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
s : Set β
t : Set α
ht : t ∈ iInf f
refine_1 : ⨅ (i : ι), (f i).lift g ≤ g univ
refine_2 :
  ∀ {i : ι} {s₁ s₂ : Set α} (hs : s₁ ∈ f i) (ht : ⨅ (i : ι), (f i).lift g ≤ g s₂), ⨅ (i : ι), (f i).lift g ≤ g (s₁ ∩ s₂)
⊢ ⨅ (i : ι), (f i).lift g ≤ g t

Tactic:
refine iInf_sets_induct ht ?_ fun hs ht => ?_
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
s : Set β
t : Set α
ht : t ∈ iInf f
refine_1 : ∀ (inhabited_h : Inhabited ι), ⨅ (i : ι), (f i).lift g ≤ g univ
⊢ ⨅ (i : ι), (f i).lift g ≤ g univ

Tactic:
inhabit ι
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
s : Set β
t : Set α
ht : t ∈ iInf f
inhabited_h : Inhabited ι
⊢ ⨅ (i : ι), (f i).lift g ≤ g univ

Tactic:
iInf₂_le_of_le default univ (iInf_le _ univ_mem)

Premises used: Inhabited.default, Set.Mem, Set.univ, setOf, iInf₂_le_of_le, Filter.lift, Filter.univ_mem, iInf_le
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
s : Set β
t : Set α
ht : t ∈ iInf f
inhabited_h : Inhabited ι
⊢ ⨅ (i : ι), (f i).lift g ≤ g univ

Tactic:
exact iInf₂_le_of_le default univ (iInf_le _ univ_mem)

Premises used: Inhabited.default, Set.univ, iInf₂_le_of_le
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
s : Set β
t : Set α
ht_1 : t ∈ iInf f
i : ι
s₁ s₂ : Set α
hs : s₁ ∈ f i
ht : ⨅ (i : ι), (f i).lift g ≤ g s₂
refine_2 : ⨅ (i : ι), (f i).lift g ≤ g s₁ ⊓ g s₂
⊢ ⨅ (i : ι), (f i).lift g ≤ g (s₁ ∩ s₂)

Tactic:
rw [hg]
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
s : Set β
t : Set α
ht_1 : t ∈ iInf f
i : ι
s₁ s₂ : Set α
hs : s₁ ∈ f i
ht : ⨅ (i : ι), (f i).lift g ≤ g s₂
⊢ ⨅ (i : ι), (f i).lift g ≤ g s₁ ⊓ g s₂

Tactic:
le_inf (iInf₂_le_of_le _ _ <| iInf_le _ hs) ht

Premises used: Set.Mem, iInf₂_le_of_le, le_inf, iInf_le
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
s : Set β
t : Set α
ht_1 : t ∈ iInf f
i : ι
s₁ s₂ : Set α
hs : s₁ ∈ f i
ht : ⨅ (i : ι), (f i).lift g ≤ g s₂
⊢ ⨅ (i : ι), (f i).lift g ≤ g s₁ ⊓ g s₂

Tactic:
exact le_inf (iInf₂_le_of_le _ _ <| iInf_le _ hs) ht

Premises used: le_inf
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
s : Set β
⊢ ∀ t ∈ iInf f, ⨅ (i : ι), (f i).lift g ≤ g t

Tactic:
have H : ∀ t ∈ iInf f, ⨅ i, (f i).lift g ≤ g t := by
    intro t ht
    refine iInf_sets_induct ht ?_ fun hs ht => ?_
    · inhabit ι
      exact iInf₂_le_of_le default univ (iInf_le _ univ_mem)
    · rw [hg]
      exact le_inf (iInf₂_le_of_le _ _ <| iInf_le _ hs) ht
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
s : Set β
H : ∀ t ∈ iInf f, ⨅ (i : ι), (f i).lift g ≤ g t
simp : ∀ x ∈ iInf f, s ∈ g x → Membership.mem (γ := Filter β) (⨅ (i : ι), (f i).lift g) s
⊢ s ∈ (iInf f).lift g → Membership.mem (γ := Filter β) (⨅ (i : ι), (f i).lift g) s

Tactic:
simp only [mem_lift_sets (Monotone.of_map_inf hg), exists_imp, and_imp]

Premises used: Monotone.of_map_inf, and_imp, Filter.mem_lift_sets, exists_imp
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
s : Set β
H : ∀ t ∈ iInf f, ⨅ (i : ι), (f i).lift g ≤ g t
⊢ ∀ x ∈ iInf f, s ∈ g x → Membership.mem (γ := Filter β) (⨅ (i : ι), (f i).lift g) s

Tactic:
fun t ht hs => H t ht hs
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
s : Set β
H : ∀ t ∈ iInf f, ⨅ (i : ι), (f i).lift g ≤ g t
⊢ ∀ x ∈ iInf f, s ∈ g x → Membership.mem (γ := Filter β) (⨅ (i : ι), (f i).lift g) s

Tactic:
exact fun t ht hs => H t ht hs
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hf : Directed (fun (x1 x2 : Filter α) ↦ x1 ≥ x2) f
hg : Monotone g
s : Set β
simp : ∀ (x : Set α) (x_1 : ι), x ∈ f x_1 → s ∈ g x → Membership.mem (γ := Filter β) (⨅ (i : ι), (f i).lift g) s
⊢ s ∈ (iInf f).lift g → Membership.mem (γ := Filter β) (⨅ (i : ι), (f i).lift g) s

Tactic:
simp only [mem_lift_sets hg, exists_imp, and_imp, mem_iInf_of_directed hf]

Premises used: and_imp, Filter.mem_lift_sets, Filter.mem_iInf_of_directed, exists_imp