awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 β
⊢ ∀ (x : Set α) (x_1 : ι), x ∈ f x_1 → s ∈ g x → Membership.mem (γ := Filter β) (⨅ (i : ι), (f i).lift g) s

Tactic:
fun t i ht hs => mem_iInf_of_mem i <| mem_lift ht hs

Premises used: Filter.mem_lift, Filter.mem_iInf_of_mem
-- 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 β
⊢ ∀ (x : Set α) (x_1 : ι), x ∈ f x_1 → s ∈ g x → Membership.mem (γ := Filter β) (⨅ (i : ι), (f i).lift g) s

Tactic:
exact fun t i ht hs => mem_iInf_of_mem i <| mem_lift ht hs

Premises used: Filter.mem_lift, Filter.mem_iInf_of_mem
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
hg' : g univ = ⊤
inl : IsEmpty ι → (iInf f).lift g = ⨅ (i : ι), (f i).lift g
inr : Nonempty ι → (iInf f).lift g = ⨅ (i : ι), (f i).lift g
⊢ (iInf f).lift g = ⨅ (i : ι), (f i).lift g

Tactic:
cases isEmpty_or_nonempty ι

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
hg' : g univ = ⊤
h : IsEmpty ι
⊢ (iInf f).lift g = ⨅ (i : ι), (f i).lift g

Tactic:
simp [iInf_of_empty, hg']

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

Tactic:
lift_iInf hg

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

Tactic:
exact lift_iInf hg

Premises used: Filter.lift_iInf
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
h : Set α → Set β
⊢ Filter.lift' ⊤ h = 𝓟 (h univ)

Tactic:
lift_top _

Premises used: Filter.lift_top, Filter.lift', Filter.principal
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
f : Filter α
h : Set α → Set β
t : Set α
ht : t ∈ f
⊢ h t ∈ f.lift' h

Tactic:
le_principal_iff.mp <| show f.lift' h ≤ 𝓟 (h t) from iInf_le_of_le t <| iInf_le_of_le ht <| le_rfl

Premises used: le_rfl, Filter.le_principal_iff, Iff.mp, iInf_le_of_le
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
h : Set α → Set β
m : γ → β
l : Filter γ
⊢ Tendsto m l (f.lift' h) ↔ ∀ s ∈ f, ∀ᶠ (a : γ) in l, m a ∈ h s

Tactic:
simp only [Filter.lift', tendsto_lift, tendsto_principal, comp]

Premises used: Function.comp, Filter.tendsto_principal, Filter.lift', Filter.tendsto_lift
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
f : Filter α
h : Set α → Set β
ι : Sort u_5
p : ι → Prop
s : ι → Set α
hf : f.HasBasis p s
hh : Monotone h
t : Set β
⊢ (∃ (i : ι), p i ∧ ∃ (x : Unit), True ∧ h (s i) ⊆ t) ↔ ∃ (i : ι), p i ∧ (h ∘ s) i ⊆ t

Tactic:
simp only [exists_const, true_and, comp]

Premises used: Function.comp, exists_const, true_and
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
f : Filter α
h : Set α → Set β
hh : Monotone h
s : Set β
⊢ s ∈ f.lift' h ↔ ∃ t ∈ f, h t ⊆ s

Tactic:
mem_lift_sets <| monotone_principal.comp hh

Premises used: Set.Mem, setOf, Monotone.comp, Set.Subset, Filter.mem_lift_sets, Filter.monotone_principal
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
f : Filter α
h : Set α → Set β
hh : Monotone h
p : β → Prop
⊢ (∀ᶠ (y : β) in f.lift' h, p y) ↔ ∃ t ∈ f, ∀ y ∈ h t, p y

Tactic:
mem_lift'_sets hh

Premises used: Set.Mem, Filter.Eventually, setOf, Filter.mem_lift'_sets, Set.Subset
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
f : Filter α
h : Set α → Set β
hh : Monotone h
⊢ Eq.{u_2 + 1} (α := Set β) (⋂₀ {s : Set β | s ∈ f.lift' h}) (⋂ s ∈ f, h s)

Tactic:
(sInter_lift_sets (monotone_principal.comp hh)).trans <| iInter₂_congr fun _ _ => csInf_Ici

Premises used: Set.Mem, setOf, Monotone.comp, Filter.sInter_lift_sets, csInf_Ici, Set.iInter₂_congr, Eq.trans, Filter.monotone_principal
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Set α → Set β
h : Filter β
s : Set α
hs : s ∈ f
hg : 𝓟 (g s) ≤ h
⊢ f.lift' g ≤ h

Tactic:
lift_le hs hg

Premises used: Set.Mem, Filter.lift_le
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
h₁ h₂ : Set α → Set β
hf : f₁ ≤ f₂
hh : h₁ ≤ h₂
⊢ f₁.lift' h₁ ≤ f₂.lift' h₂

Tactic:
lift_mono hf fun s => principal_mono.mpr <| hh s

Premises used: Iff.mpr, Filter.principal_mono, Set.Mem, Filter.lift_mono
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
f : Filter α
h₁ h₂ : Set α → Set β
hh : ∀ s ∈ f, h₁ s ⊆ h₂ s
⊢ f.lift' h₁ ≤ f.lift' h₂

Tactic:
iInf₂_mono fun s hs => principal_mono.mpr <| hh s hs

Premises used: Iff.mpr, Filter.principal_mono, Set.Mem, setOf, iInf₂_mono
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
f : Filter α
h₁ h₂ : Set α → Set β
hh : ∀ s ∈ f, h₁ s = h₂ s
⊢ f.lift' h₁ = f.lift' h₂

Tactic:
le_antisymm (lift'_mono' fun s hs => le_of_eq <| hh s hs)
    (lift'_mono' fun s hs => le_of_eq <| (hh s hs).symm)

Premises used: Filter.lift'_mono', le_antisymm, le_of_eq, Eq.symm
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
h : Set α → Set β
m : β → γ
hh : Monotone h
⊢ f.lift (map m ∘ 𝓟 ∘ h) = f.lift' (image m ∘ h)

Tactic:
simp only [comp_def, Filter.lift', map_principal]

Premises used: Function.comp_def, Filter.lift', Filter.map_principal
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Set β → Set γ
m : α → β
⊢ (map m f).lift' g ≤ f.lift' (g ∘ image m)

Tactic:
lift_map_le

Premises used: Set.Mem, setOf, Filter.lift_map_le, Filter.principal
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Set β → Set γ
m : α → β
hg : Monotone g
⊢ (map m f).lift' g = f.lift' (g ∘ image m)

Tactic:
map_lift_eq2 <| monotone_principal.comp hg

Premises used: setOf, Monotone.comp, Filter.lift', Filter.principal, Filter.map_lift_eq2, Filter.monotone_principal
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
h : Set α → Set β
m : γ → β
⊢ comap m (f.lift' h) = f.lift' (preimage m ∘ h)

Tactic:
simp only [Filter.lift', comap_lift_eq, comp_def, comap_principal]

Premises used: Function.comp_def, Filter.lift', Filter.comap_principal, Filter.comap_lift_eq
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
m : β → α
g : Set β → Set γ
hg : Monotone g
⊢ (comap m f).lift' g = f.lift' (g ∘ preimage m)

Tactic:
comap_lift_eq2 <| monotone_principal.comp hg

Premises used: setOf, Monotone.comp, Filter.comap_lift_eq2, Filter.lift', Filter.principal, Filter.monotone_principal
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
h : Set α → Set β
s : Set α
hh : Monotone h
⊢ (𝓟 s).lift' h = 𝓟 (h s)

Tactic:
lift_principal <| monotone_principal.comp hh

Premises used: Monotone.comp, Filter.lift_principal, Filter.lift', Filter.principal, Filter.monotone_principal
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
h : Set α → Set β
a : α
hh : Monotone h
rw : Filter.lift' (𝓟 {a}) h = 𝓟 (h {a})
rw₁ rw₂ : 𝓟 (h {a}) = 𝓟 (h {a})
⊢ Filter.lift' (pure a) h = 𝓟 (h {a})

Tactic:
rw [← principal_singleton, lift'_principal hh]

Premises used: Filter.lift'_principal, Filter.principal_singleton
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
h : Set α → Set β
hh : Monotone h
rw : Filter.lift' (𝓟 ∅) h = 𝓟 (h ∅)
rw₁ rw₂ : 𝓟 (h ∅) = 𝓟 (h ∅)
⊢ Filter.lift' ⊥ h = 𝓟 (h ∅)

Tactic:
rw [← principal_empty, lift'_principal hh]

Premises used: Filter.lift'_principal, Filter.principal_empty
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
f : Filter α
h : Set α → Set β
g : Filter β
⊢ g ≤ f.lift' h ↔ ∀ s ∈ f, h s ∈ g

Tactic:
le_lift.trans <| forall₂_congr fun _ _ => le_principal_iff

Premises used: Filter.le_principal_iff, Set.Mem, Filter.le_lift, forall₂_congr, Iff.trans
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
f : Filter α
h : Set α → Set β
t : Set β
⊢ 𝓟 t ≤ f.lift' h ↔ ∀ s ∈ f, t ⊆ h s

Tactic:
le_lift'

Premises used: Set.Mem, setOf, Set.Subset, Filter.le_lift'
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder γ
f : γ → Filter α
g : γ → Set α → Set β
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, Filter.lift'_mono, Monotone
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Set α → Set β
h : Set β → Filter γ
hg : Monotone g
hh : Monotone h
⊢ Eq.{u_3 + 1} (α := Filter γ) (f.lift fun (s : Set α) ↦ (𝓟 (g s)).lift h) (f.lift fun (s : Set α) ↦ h (g s))

Tactic:
simp only [lift_principal, hh]

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

Tactic:
lift_lift'_assoc hg (monotone_principal.comp hh)

Premises used: Monotone.comp, Filter.lift_lift'_assoc, Filter.lift', Filter.monotone_principal
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Set α → Filter β
h : Set β → Set γ
hg : Monotone g
⊢ (f.lift g).lift' h = f.lift fun (s : Set α) ↦ (g s).lift' h

Tactic:
lift_assoc hg

Premises used: Filter.lift_assoc, Filter.lift'
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Set α → Set α → Set β
⊢ LE.le.{u_2} (α := Filter β) (f.lift fun (s : Set α) ↦ f.lift' (g s)) (f.lift' fun (s : Set α) ↦ g s s)

Tactic:
lift_lift_same_le_lift

Premises used: Set.Mem, setOf, Filter.lift', Filter.lift_lift_same_le_lift
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Set α → Set α → Set β
hg₁ : ∀ (s : Set α), Monotone.{u_1, u_2} (β := Set β) fun (t : Set α) ↦ g s t
hg₂ : ∀ (t : Set α), Monotone.{u_1, u_2} (β := Set β) 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_eq_lift (fun s => monotone_principal.comp (hg₁ s)) fun t =>
    monotone_principal.comp (hg₂ t)

Premises used: Filter.lift_lift_same_eq_lift, Monotone.comp, Filter.lift', Filter.monotone_principal
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
f : Filter α
h : Set α → Set β
s : Set β
⊢ f.lift' h ⊓ 𝓟 s = f.lift' fun (t : Set α) ↦ h t ∩ s

Tactic:
simp only [Filter.lift', Filter.lift, (· ∘ ·), ← inf_principal, iInf_subtype', ← iInf_inf]

Premises used: iInf_inf, Filter.inf_principal, Function.comp, iInf_subtype', Filter.lift', Filter.lift
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
f : Filter α
h : Set α → Set β
hh : Monotone h
⊢ (∀ s ∈ f, (𝓟 (h s)).NeBot) ↔ ∀ s ∈ f, (h s).Nonempty

Tactic:
simp only [principal_neBot_iff]

Premises used: Filter.principal_neBot_iff
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
f : Filter α
⊢ f.lift' id = f

Tactic:
lift_principal2

Premises used: setOf, Filter.lift', Filter.principal, Filter.lift_principal2
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : Nonempty ι
f : ι → Filter α
g : Set α → Set β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ∩ g t
s t : Set α
⊢ (𝓟 ∘ g) (s ∩ t) = (𝓟 ∘ g) s ⊓ (𝓟 ∘ g) t

Tactic:
simp only [inf_principal, comp, hg]

Premises used: Filter.inf_principal, Function.comp
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
f : ι → Filter α
g : Set α → Set β
hg : ∀ {s t : Set α}, g (s ∩ t) = g s ∩ g t
hg' : g univ = univ
s t : Set α
⊢ (𝓟 ∘ g) (s ∩ t) = (𝓟 ∘ g) s ⊓ (𝓟 ∘ g) t

Tactic:
simp only [inf_principal, comp, hg]

Premises used: Filter.inf_principal, Function.comp
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
f : ι → Filter α
g : Set α → Set β
hg : ∀ {s t : Set α}, g (s ∩ t) = g s ∩ g t
hg' : g univ = univ
rw : 𝓟 (g univ) = ⊤
rw₁ : Eq.{u_2 + 1} (α := Filter β) (𝓟 univ) ⊤
rw₂ rw₃ : Eq.{u_2 + 1} (α := Filter β) ⊤ ⊤
⊢ (𝓟 ∘ g) univ = ⊤

Tactic:
rw [Function.comp_apply, hg', principal_univ]

Premises used: Filter.principal_univ, Function.comp_apply
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
f g : Filter α
s : Set α → Set β
hs : ∀ (t₁ t₂ : Set α), s (t₁ ∩ t₂) = s t₁ ∩ s t₂
rw :
  Eq.{u_2 + 1} (α := Filter β) (⨅ (i : Bool), (bif i then f else g).lift' s)
    (⨅ (b : Bool), bif b then f.lift' s else g.lift' s)
⊢ (f ⊓ g).lift' s = f.lift' s ⊓ g.lift' s

Tactic:
rw [inf_eq_iInf, inf_eq_iInf, lift'_iInf hs]

Premises used: inf_eq_iInf, Filter.lift'_iInf
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
f g : Filter α
s : Set α → Set β
hs : ∀ (t₁ t₂ : Set α), s (t₁ ∩ t₂) = s t₁ ∩ s t₂
⊢ Eq.{u_2 + 1} (α := Filter β) (⨅ (i : Bool), (bif i then f else g).lift' s)
    (⨅ (b : Bool), bif b then f.lift' s else g.lift' s)

Tactic:
iInf_congr ?_

Premises used: iInf_congr
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
f g : Filter α
s : Set α → Set β
hs : ∀ (t₁ t₂ : Set α), s (t₁ ∩ t₂) = s t₁ ∩ s t₂
refine : ∀ (i : Bool), (bif i then f else g).lift' s = bif i then f.lift' s else g.lift' s
⊢ Eq.{u_2 + 1} (α := Filter β) (⨅ (i : Bool), (bif i then f else g).lift' s)
    (⨅ (b : Bool), bif b then f.lift' s else g.lift' s)

Tactic:
refine iInf_congr ?_

Premises used: iInf_congr
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
f g : Filter α
s : Set α → Set β
hs : ∀ (t₁ t₂ : Set α), s (t₁ ∩ t₂) = s t₁ ∩ s t₂
⊢ (bif false then f else g).lift' s = bif false then f.lift' s else g.lift' s

Tactic:
rfl
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
f g : Filter α
s : Set α → Set β
hs : ∀ (t₁ t₂ : Set α), s (t₁ ∩ t₂) = s t₁ ∩ s t₂
⊢ (bif true then f else g).lift' s = bif true then f.lift' s else g.lift' s

Tactic:
rfl
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
f g : Filter α
s : Set α → Set β
⊢ (f ⊓ g).lift' s ≤ f.lift' s ⊓ g.lift' s

Tactic:
le_inf (lift'_mono inf_le_left le_rfl) (lift'_mono inf_le_right le_rfl)

Premises used: le_rfl, Set.Mem, Filter.lift'_mono, inf_le_right, le_inf, inf_le_left
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
⊢ comap m f = f.lift' (preimage m)

Tactic:
Filter.ext fun _ => (mem_lift'_sets monotone_preimage).symm

Premises used: Filter.ext, Filter.mem_lift'_sets, Set.monotone_preimage, Iff.symm
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ f ×ˢ g = f.lift fun (s : Set α) ↦ g.lift' fun (t : Set β) ↦ s ×ˢ t

Tactic:
simpa only [Filter.lift', Filter.lift, (f.basis_sets.prod g.basis_sets).eq_biInf,
    iInf_prod, iInf_and] using iInf_congr fun i => iInf_comm

Premises used: iInf_congr, Filter.HasBasis.eq_biInf, Filter.basis_sets, Filter.lift', Filter.lift, iInf_and, iInf_comm, iInf_prod, Filter.HasBasis.prod
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
f : Filter α
⊢ f ×ˢ f = f.lift' fun (t : Set α) ↦ t ×ˢ t

Tactic:
f.basis_sets.prod_self.eq_biInf

Premises used: Filter.HasBasis.prod_self, setOf, Filter.HasBasis.eq_biInf, Filter.basis_sets, Filter.lift', Filter.lift, Filter.principal
-- Module: Mathlib.Order.Filter.Lift
Goal:
α : Type u_1
β : Type u_2
f : α × α → β
x : Filter α
y : Filter β
⊢ Tendsto f (x ×ˢ x) y ↔ ∀ W ∈ y, ∃ U ∈ x, ∀ (x x' : α), x ∈ U → x' ∈ U → f (x, x') ∈ W

Tactic:
simp only [tendsto_def, mem_prod_same_iff, prod_sub_preimage_iff]

Premises used: Filter.tendsto_def, Set.prod_sub_preimage_iff, Filter.mem_prod_same_iff
-- Module: Mathlib.Order.Filter.Lift
Goal:
α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
f₁ : Filter α₁
f₂ : Filter α₂
g₁ : Set α₁ → Filter β₁
g₂ : Set α₂ → Filter β₂
hg₁ : Monotone g₁
hg₂ : Monotone g₂
simp :
  Eq (α := Filter (β₁ × β₂))
    (f₁.lift fun (s : Set α₁) ↦ (g₁ s).lift fun (s : Set β₁) ↦ (f₂.lift g₂).lift' fun (t : Set β₂) ↦ s ×ˢ t)
    (f₁.lift fun (s : Set α₁) ↦
      f₂.lift fun (t : Set α₂) ↦ (g₁ s).lift fun (s : Set β₁) ↦ (g₂ t).lift' fun (t : Set β₂) ↦ s ×ˢ t)
⊢ f₁.lift g₁ ×ˢ f₂.lift g₂ = f₁.lift fun (s : Set α₁) ↦ f₂.lift fun (t : Set α₂) ↦ g₁ s ×ˢ g₂ t

Tactic:
simp only [prod_def, lift_assoc hg₁]

Premises used: Filter.lift_assoc, Filter.prod_def
-- Module: Mathlib.Order.Filter.Lift
Goal:
α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
f₁ : Filter α₁
f₂ : Filter α₂
g₁ : Set α₁ → Filter β₁
g₂ : Set α₂ → Filter β₂
hg₁ : Monotone g₁
hg₂ : Monotone g₂
h :
  Eq (α := (s : Set α₁) → Filter (β₁ × β₂))
    (fun (s : Set α₁) ↦ (g₁ s).lift fun (s : Set β₁) ↦ (f₂.lift g₂).lift' fun (t : Set β₂) ↦ s ×ˢ t) fun (s : Set α₁) ↦
    f₂.lift fun (t : Set α₂) ↦ (g₁ s).lift fun (s : Set β₁) ↦ (g₂ t).lift' fun (t : Set β₂) ↦ s ×ˢ t
⊢ Eq (α := Filter (β₁ × β₂))
    (f₁.lift fun (s : Set α₁) ↦ (g₁ s).lift fun (s : Set β₁) ↦ (f₂.lift g₂).lift' fun (t : Set β₂) ↦ s ×ˢ t)
    (f₁.lift fun (s : Set α₁) ↦
      f₂.lift fun (t : Set α₂) ↦ (g₁ s).lift fun (s : Set β₁) ↦ (g₂ t).lift' fun (t : Set β₂) ↦ s ×ˢ t)

Tactic:
apply congr_arg

Premises used: congr_arg
-- Module: Mathlib.Order.Filter.Lift
Goal:
α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
f₁ : Filter α₁
f₂ : Filter α₂
g₁ : Set α₁ → Filter β₁
g₂ : Set α₂ → Filter β₂
hg₁ : Monotone g₁
hg₂ : Monotone g₂
h :
  ∀ (x : Set α₁),
    Eq (α := Filter (β₁ × β₂)) ((g₁ x).lift fun (s : Set β₁) ↦ (f₂.lift g₂).lift' fun (t : Set β₂) ↦ s ×ˢ t)
      (f₂.lift fun (t : Set α₂) ↦ (g₁ x).lift fun (s : Set β₁) ↦ (g₂ t).lift' fun (t : Set β₂) ↦ s ×ˢ t)
⊢ Eq (α := (s : Set α₁) → Filter (β₁ × β₂))
    (fun (s : Set α₁) ↦ (g₁ s).lift fun (s : Set β₁) ↦ (f₂.lift g₂).lift' fun (t : Set β₂) ↦ s ×ˢ t) fun (s : Set α₁) ↦
    f₂.lift fun (t : Set α₂) ↦ (g₁ s).lift fun (s : Set β₁) ↦ (g₂ t).lift' fun (t : Set β₂) ↦ s ×ˢ t

Tactic:
funext x
-- Module: Mathlib.Order.Filter.Lift
Goal:
α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
f₁ : Filter α₁
f₂ : Filter α₂
g₁ : Set α₁ → Filter β₁
g₂ : Set α₂ → Filter β₂
hg₁ : Monotone g₁
hg₂ : Monotone g₂
x : Set α₁
h :
  Eq (α := Filter (β₁ × β₂)) ((g₁ x).lift fun (s : Set β₁) ↦ (f₂.lift g₂).lift' fun (t : Set β₂) ↦ s ×ˢ t)
    ((g₁ x).lift fun (t : Set β₁) ↦ f₂.lift fun (s : Set α₂) ↦ (g₂ s).lift' fun (t_1 : Set β₂) ↦ t ×ˢ t_1)
⊢ Eq (α := Filter (β₁ × β₂)) ((g₁ x).lift fun (s : Set β₁) ↦ (f₂.lift g₂).lift' fun (t : Set β₂) ↦ s ×ˢ t)
    (f₂.lift fun (t : Set α₂) ↦ (g₁ x).lift fun (s : Set β₁) ↦ (g₂ t).lift' fun (t : Set β₂) ↦ s ×ˢ t)

Tactic:
rw [lift_comm]

Premises used: Filter.lift_comm
-- Module: Mathlib.Order.Filter.Lift
Goal:
α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
f₁ : Filter α₁
f₂ : Filter α₂
g₁ : Set α₁ → Filter β₁
g₂ : Set α₂ → Filter β₂
hg₁ : Monotone g₁
hg₂ : Monotone g₂
x : Set α₁
h :
  Eq (α := (s : Set β₁) → Filter (β₁ × β₂)) (fun (s : Set β₁) ↦ (f₂.lift g₂).lift' fun (t : Set β₂) ↦ s ×ˢ t)
    fun (t : Set β₁) ↦ f₂.lift fun (s : Set α₂) ↦ (g₂ s).lift' fun (t_1 : Set β₂) ↦ t ×ˢ t_1
⊢ Eq (α := Filter (β₁ × β₂)) ((g₁ x).lift fun (s : Set β₁) ↦ (f₂.lift g₂).lift' fun (t : Set β₂) ↦ s ×ˢ t)
    ((g₁ x).lift fun (t : Set β₁) ↦ f₂.lift fun (s : Set α₂) ↦ (g₂ s).lift' fun (t_1 : Set β₂) ↦ t ×ˢ t_1)

Tactic:
apply congr_arg

Premises used: congr_arg
-- Module: Mathlib.Order.Filter.Lift
Goal:
α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
f₁ : Filter α₁
f₂ : Filter α₂
g₁ : Set α₁ → Filter β₁
g₂ : Set α₂ → Filter β₂
hg₁ : Monotone g₁
hg₂ : Monotone g₂
x : Set α₁
h :
  ∀ (y : Set β₁),
    Eq (α := Filter (β₁ × β₂)) ((f₂.lift g₂).lift' fun (t : Set β₂) ↦ y ×ˢ t)
      (f₂.lift fun (s : Set α₂) ↦ (g₂ s).lift' fun (t : Set β₂) ↦ y ×ˢ t)
⊢ Eq (α := (s : Set β₁) → Filter (β₁ × β₂)) (fun (s : Set β₁) ↦ (f₂.lift g₂).lift' fun (t : Set β₂) ↦ s ×ˢ t)
    fun (t : Set β₁) ↦ f₂.lift fun (s : Set α₂) ↦ (g₂ s).lift' fun (t_1 : Set β₂) ↦ t ×ˢ t_1

Tactic:
funext y
-- Module: Mathlib.Order.Filter.Lift
Goal:
α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
f₁ : Filter α₁
f₂ : Filter α₂
g₁ : Set α₁ → Filter β₁
g₂ : Set α₂ → Filter β₂
hg₁ : Monotone g₁
hg₂ : Monotone g₂
x : Set α₁
y : Set β₁
⊢ Eq (α := Filter (β₁ × β₂)) ((f₂.lift g₂).lift' fun (t : Set β₂) ↦ y ×ˢ t)
    (f₂.lift fun (s : Set α₂) ↦ (g₂ s).lift' fun (t : Set β₂) ↦ y ×ˢ t)

Tactic:
apply lift'_lift_assoc hg₂

Premises used: Filter.lift'_lift_assoc
-- Module: Mathlib.Order.Filter.Lift
Goal:
α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
f₁ : Filter α₁
f₂ : Filter α₂
g₁ : Set α₁ → Set β₁
g₂ : Set α₂ → Set β₂
hg₁ : Monotone g₁
hg₂ : Monotone g₂
⊢ Eq (α := Filter (β₁ × β₂)) (f₁.lift fun (s : Set α₁) ↦ f₂.lift fun (t : Set α₂) ↦ 𝓟 (g₁ s) ×ˢ 𝓟 (g₂ t))
    (f₁.lift fun (s : Set α₁) ↦ f₂.lift fun (t : Set α₂) ↦ 𝓟 (g₁ s ×ˢ g₂ t))

Tactic:
simp only [prod_principal_principal]

Premises used: Filter.prod_principal_principal
-- Module: Mathlib.Order.Filter.Lift
Goal:
α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
f₁ : Filter α₁
f₂ : Filter α₂
g₁ : Set α₁ → Set β₁
g₂ : Set α₂ → Set β₂
hg₁ : Monotone g₁
hg₂ : Monotone g₂
⊢ Eq (α := Filter (β₁ × β₂)) (f₁.lift fun (s : Set α₁) ↦ f₂.lift fun (t : Set α₂) ↦ 𝓟 (g₁ s) ×ˢ 𝓟 (g₂ t))
    (f₁.lift fun (s : Set α₁) ↦ f₂.lift fun (t : Set α₂) ↦ 𝓟 (g₁ s ×ˢ g₂ t))

Tactic:
{ simp only [prod_principal_principal] }

Premises used: Filter.prod_principal_principal
-- Module: Mathlib.Order.Filter.ListTraverse
Goal:
α β : Type u
f : β → Filter α
fs : List β
t : Set (List α)
mp : t ∈ traverse f fs → ∃ (us : List (Set α)), Forall₂ (fun (b : β) (s : Set α) ↦ s ∈ f b) fs us ∧ sequence us ⊆ t
mpr : (∃ (us : List (Set α)), Forall₂ (fun (b : β) (s : Set α) ↦ s ∈ f b) fs us ∧ sequence us ⊆ t) → t ∈ traverse f fs
⊢ t ∈ traverse f fs ↔ ∃ (us : List (Set α)), Forall₂ (fun (b : β) (s : Set α) ↦ s ∈ f b) fs us ∧ sequence us ⊆ t

Tactic:
constructor
-- Module: Mathlib.Order.Filter.ListTraverse
Goal:
α β : Type u
f : β → Filter α
t : Set (List α)
⊢ t ∈ traverse f [] → ∃ (us : List (Set α)), Forall₂ (fun (b : β) (s : Set α) ↦ s ∈ f b) [] us ∧ sequence us ⊆ t

Tactic:
simp only [sequence, mem_pure, imp_self, forall₂_nil_left_iff, exists_eq_left, Set.pure_def,
        singleton_subset_iff, traverse_nil]

Premises used: Set.singleton_subset_iff, Set.pure_def, List.forall₂_nil_left_iff, exists_eq_left, imp_self, List.traverse_nil, sequence, Filter.mem_pure
-- Module: Mathlib.Order.Filter.ListTraverse
Goal:
α β : Type u
f : β → Filter α
b : β
fs : List β
ih : ∀ t ∈ traverse f fs, ∃ (us : List (Set α)), Forall₂ (fun (b : β) (s : Set α) ↦ s ∈ f b) fs us ∧ sequence us ⊆ t
t : Set (List α)
ht : t ∈ traverse f (b :: fs)
mp :
  ∀ (u : Set (List α → List α)) (hu : u ∈ cons <$> f b) (v : Set (List α))
    (hv : Membership.mem (γ := Filter (List α)) ((fun (x : Unit) ↦ List.traverse f fs) ()) v) (ht : u.seq v ⊆ t),
    ∃ (us : List (Set α)), Forall₂ (fun (b : β) (s : Set α) ↦ s ∈ f b) (b :: fs) us ∧ sequence us ⊆ t
⊢ ∃ (us : List (Set α)), Forall₂ (fun (b : β) (s : Set α) ↦ s ∈ f b) (b :: fs) us ∧ sequence us ⊆ t

Tactic:
rcases mem_seq_iff.1 ht with ⟨u, hu, v, hv, ht⟩

Premises used: Filter.mem_seq_iff, Iff.mp