awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : LinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
i : ι
i_s : i ∈ s
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in Filter.map (F i) f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x a) → (fun (x1 x2 : β) ↦ x1 ≤ x2) b a
h :
  ∀ (a : β),
    (∀ᶠ (x : β) in Filter.map (fun (a : α) ↦ s.sup' hs fun (i : ι) ↦ F i a) f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x a) →
      (fun (x1 x2 : β) ↦ x1 ≤ x2) b a
⊢ IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ s.sup' hs fun (i : ι) ↦ F i a

Tactic:
use b
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : LinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
i : ι
i_s : i ∈ s
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in Filter.map (F i) f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x a) → (fun (x1 x2 : β) ↦ x1 ≤ x2) b a
⊢ ∀ (a : β),
    (∀ᶠ (x : β) in Filter.map (fun (a : α) ↦ s.sup' hs fun (i : ι) ↦ F i a) f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x a) →
      (fun (x1 x2 : β) ↦ x1 ≤ x2) b a

Tactic:
fun c hc ↦ hb c ?_
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : LinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
i : ι
i_s : i ∈ s
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in Filter.map (F i) f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x a) → (fun (x1 x2 : β) ↦ x1 ≤ x2) b a
h :
  ∀ (c : β)
    (hc : ∀ᶠ (x : β) in Filter.map (fun (a : α) ↦ s.sup' hs fun (i : ι) ↦ F i a) f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x c),
    ∀ᶠ (x : β) in Filter.map (F i) f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x c
⊢ ∀ (a : β),
    (∀ᶠ (x : β) in Filter.map (fun (a : α) ↦ s.sup' hs fun (i : ι) ↦ F i a) f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x a) →
      (fun (x1 x2 : β) ↦ x1 ≤ x2) b a

Tactic:
refine fun c hc ↦ hb c ?_
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : LinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
i : ι
i_s : i ∈ s
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in Filter.map (F i) f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x a) → (fun (x1 x2 : β) ↦ x1 ≤ x2) b a
c : β
hc : ∀ᶠ (x : β) in Filter.map (fun (a : α) ↦ s.sup' hs fun (i : ι) ↦ F i a) f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x c
h :
  ∀ (hc : ∀ᶠ (a : α) in f, (fun (x1 x2 : β) ↦ x1 ≤ x2) (s.sup' hs fun (i : ι) ↦ F i a) c),
    ∀ᶠ (a : α) in f, (fun (x1 x2 : β) ↦ x1 ≤ x2) (F i a) c
⊢ ∀ᶠ (x : β) in Filter.map (F i) f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x c

Tactic:
rw [eventually_map] at hc ⊢

Premises used: Filter.eventually_map
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : LinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
i : ι
i_s : i ∈ s
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in Filter.map (F i) f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x a) → (fun (x1 x2 : β) ↦ x1 ≤ x2) b a
c : β
hc : ∀ᶠ (a : α) in f, (fun (x1 x2 : β) ↦ x1 ≤ x2) (s.sup' hs fun (i : ι) ↦ F i a) c
⊢ ∀ᶠ (a : α) in f, (fun (x1 x2 : β) ↦ x1 ≤ x2) (F i a) c

Tactic:
hc.mono fun a h ↦ ?_

Premises used: Filter.Eventually.mono
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : LinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
i : ι
i_s : i ∈ s
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in Filter.map (F i) f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x a) → (fun (x1 x2 : β) ↦ x1 ≤ x2) b a
c : β
hc : ∀ᶠ (a : α) in f, (fun (x1 x2 : β) ↦ x1 ≤ x2) (s.sup' hs fun (i : ι) ↦ F i a) c
h : ∀ (a : α) (h : (fun (x1 x2 : β) ↦ x1 ≤ x2) (s.sup' hs fun (i : ι) ↦ F i a) c), (fun (x1 x2 : β) ↦ x1 ≤ x2) (F i a) c
⊢ ∀ᶠ (a : α) in f, (fun (x1 x2 : β) ↦ x1 ≤ x2) (F i a) c

Tactic:
refine hc.mono fun a h ↦ ?_

Premises used: Filter.Eventually.mono
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : LinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
i : ι
i_s : i ∈ s
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in Filter.map (F i) f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x a) → (fun (x1 x2 : β) ↦ x1 ≤ x2) b a
c : β
hc : ∀ᶠ (a : α) in f, (fun (x1 x2 : β) ↦ x1 ≤ x2) (s.sup' hs fun (i : ι) ↦ F i a) c
a : α
h : (fun (x1 x2 : β) ↦ x1 ≤ x2) (s.sup' hs fun (i : ι) ↦ F i a) c
⊢ ∀ b ∈ s, F b a ≤ c

Tactic:
simp only [sup'_le_iff] at h ⊢

Premises used: Finset.sup'_le_iff
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : LinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
i : ι
i_s : i ∈ s
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in Filter.map (F i) f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x a) → (fun (x1 x2 : β) ↦ x1 ≤ x2) b a
c : β
hc : ∀ᶠ (a : α) in f, (fun (x1 x2 : β) ↦ x1 ≤ x2) (s.sup' hs fun (i : ι) ↦ F i a) c
a : α
h : ∀ b ∈ s, F b a ≤ c
⊢ F i a ≤ c

Tactic:
h i i_s
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : LinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
i : ι
i_s : i ∈ s
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in Filter.map (F i) f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x a) → (fun (x1 x2 : β) ↦ x1 ≤ x2) b a
c : β
hc : ∀ᶠ (a : α) in f, (fun (x1 x2 : β) ↦ x1 ≤ x2) (s.sup' hs fun (i : ι) ↦ F i a) c
a : α
h : ∀ b ∈ s, F b a ≤ c
⊢ F i a ≤ c

Tactic:
exact h i i_s
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : LinearOrder β
inst_1 : OrderBot β
f : Filter α
F : ι → α → β
s : Finset ι
h : ∀ i ∈ s, IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
choose! :
  ∀ (m : (i : ι) → β) (hm : ∀ i ∈ s, ∀ᶠ (x : β) in Filter.map (F i) f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x (m i)),
    IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ s.sup fun (i : ι) ↦ F i a
⊢ IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ s.sup fun (i : ι) ↦ F i a

Tactic:
choose! m hm using h
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : LinearOrder β
inst_1 : OrderBot β
f : Filter α
F : ι → α → β
s : Finset ι
m : (i : ι) → β
hm : ∀ i ∈ s, ∀ᶠ (x : β) in Filter.map (F i) f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x (m i)
h : ∀ᶠ (x : β) in Filter.map (fun (a : α) ↦ s.sup fun (i : ι) ↦ F i a) f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x (s.sup m)
⊢ IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ s.sup fun (i : ι) ↦ F i a

Tactic:
use sup s m

Premises used: Finset.sup
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : LinearOrder β
inst_1 : OrderBot β
f : Filter α
F : ι → α → β
s : Finset ι
m : (i : ι) → β
hm : ∀ i ∈ s, ∀ᶠ (x : β) in Filter.map (F i) f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x (m i)
h : ∀ (hm : ∀ i ∈ s, ∀ᶠ (a : α) in f, F i a ≤ m i), ∀ᶠ (a : α) in f, (s.sup fun (i : ι) ↦ F i a) ≤ s.sup m
⊢ ∀ᶠ (x : β) in Filter.map (fun (a : α) ↦ s.sup fun (i : ι) ↦ F i a) f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x (s.sup m)

Tactic:
simp only [eventually_map] at hm ⊢

Premises used: Filter.eventually_map
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : LinearOrder β
inst_1 : OrderBot β
f : Filter α
F : ι → α → β
s : Finset ι
m : (i : ι) → β
hm : ∀ i ∈ s, ∀ᶠ (a : α) in f, F i a ≤ m i
⊢ ∀ᶠ (x : α) in f, ∀ i ∈ s, F i x ≤ m i

Tactic:
rw [← eventually_all_finset s] at hm

Premises used: Filter.eventually_all_finset
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : LinearOrder β
inst_1 : OrderBot β
f : Filter α
F : ι → α → β
s : Finset ι
m : (i : ι) → β
hm : ∀ᶠ (x : α) in f, ∀ i ∈ s, F i x ≤ m i
⊢ ∀ᶠ (a : α) in f, (s.sup fun (i : ι) ↦ F i a) ≤ s.sup m

Tactic:
hm.mono fun _ h ↦ sup_mono_fun h

Premises used: Filter.Eventually.mono, Finset.sup_mono_fun
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : LinearOrder β
inst_1 : OrderBot β
f : Filter α
F : ι → α → β
s : Finset ι
m : (i : ι) → β
hm : ∀ᶠ (x : α) in f, ∀ i ∈ s, F i x ≤ m i
⊢ ∀ᶠ (a : α) in f, (s.sup fun (i : ι) ↦ F i a) ≤ s.sup m

Tactic:
exact hm.mono fun _ h ↦ sup_mono_fun h

Premises used: Filter.Eventually.mono, Finset.sup_mono_fun
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : LinearOrder β
inst_1 : Nonempty β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
h : ∀ i ∈ s, IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f (F i)
⊢ IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f fun (a : α) ↦ s.inf' hs fun (i : ι) ↦ F i a

Tactic:
isBoundedUnder_le_finset_sup' (β := βᵒᵈ) hs h

Premises used: Finset.inf', isBoundedUnder_le_finset_sup', WithTop.some, WithTop.untop, OrderDual, Finset.inf, WithTop
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : LinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
h : ∃ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f (F i)
⊢ IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f fun (a : α) ↦ s.inf' hs fun (i : ι) ↦ F i a

Tactic:
isCoboundedUnder_le_finset_sup' (β := βᵒᵈ) hs h

Premises used: Finset.inf', WithTop.some, WithTop.untop, isCoboundedUnder_le_finset_sup', OrderDual, Finset.inf, WithTop
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : LinearOrder β
inst_1 : OrderTop β
f : Filter α
F : ι → α → β
s : Finset ι
h : ∀ i ∈ s, IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f (F i)
⊢ IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f fun (a : α) ↦ s.inf fun (i : ι) ↦ F i a

Tactic:
isBoundedUnder_le_finset_sup (β := βᵒᵈ) h

Premises used: isBoundedUnder_le_finset_sup, OrderDual, Finset.inf
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
R : Type u_5
S : Type u_6
F : Filter R
inst : LinearOrder R
inst_1 : LinearOrder S
f : R → S
f_incr : Monotone f
l : R
freq_ge : ∃ᶠ (x : R) in F, l ≤ x
⊢ ∃ᶠ (x' : S) in map f F, f l ≤ x'

Tactic:
fun ev ↦ freq_ge ?_

Premises used: Filter.Frequently, Not
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
R : Type u_5
S : Type u_6
F : Filter R
inst : LinearOrder R
inst_1 : LinearOrder S
f : R → S
f_incr : Monotone f
l : R
freq_ge : ∃ᶠ (x : R) in F, l ≤ x
refine : ∀ (ev : ∀ᶠ (x : S) in map f F, ¬(fun (x' : S) ↦ f l ≤ x') x), ∀ᶠ (x : R) in F, ¬(fun (x : R) ↦ l ≤ x) x
⊢ ∃ᶠ (x' : S) in map f F, f l ≤ x'

Tactic:
refine fun ev ↦ freq_ge ?_
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
R : Type u_5
S : Type u_6
F : Filter R
inst : LinearOrder R
inst_1 : LinearOrder S
f : R → S
f_incr : Monotone f
l : R
freq_ge : ∃ᶠ (x : R) in F, l ≤ x
ev : ∀ᶠ (x : S) in map f F, ¬(fun (x' : S) ↦ f l ≤ x') x
simp : ∀ (ev : ∀ᶠ (x : S) in map f F, x < f l), ∀ᶠ (x : R) in F, x < l
⊢ ∀ᶠ (x : R) in F, ¬(fun (x : R) ↦ l ≤ x) x

Tactic:
simp only [not_le] at ev freq_ge ⊢

Premises used: not_le
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
R : Type u_5
S : Type u_6
F : Filter R
inst : LinearOrder R
inst_1 : LinearOrder S
f : R → S
f_incr : Monotone f
l : R
freq_ge : ∃ᶠ (x : R) in F, l ≤ x
ev : ∀ᶠ (x : S) in map f F, x < f l
h : ∀ (z : R) (hz : z ∈ f ⁻¹' {x : S | x < f l}), z < l
⊢ ∀ᶠ (x : R) in F, x < l

Tactic:
filter_upwards [ev] with z hz
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
R : Type u_5
S : Type u_6
F : Filter R
inst : LinearOrder R
inst_1 : LinearOrder S
f : R → S
f_incr : Monotone f
l : R
freq_ge : ∃ᶠ (x : R) in F, l ≤ x
ev : ∀ᶠ (x : S) in map f F, x < f l
z : R
hz : z ∈ f ⁻¹' {x : S | x < f l}
h : ∀ (con : ¬z < l), False
⊢ z < l

Tactic:
by_contra con
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
R : Type u_5
S : Type u_6
F : Filter R
inst : LinearOrder R
inst_1 : LinearOrder S
f : R → S
f_incr : Monotone f
l : R
freq_ge : ∃ᶠ (x : R) in F, l ≤ x
ev : ∀ᶠ (x : S) in map f F, x < f l
z : R
hz : z ∈ f ⁻¹' {x : S | x < f l}
con : ¬z < l
⊢ False

Tactic:
lt_irrefl (f l) <| lt_of_le_of_lt (f_incr <| not_lt.mp con) hz

Premises used: lt_of_le_of_lt, lt_irrefl, not_lt, Iff.mp
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
R : Type u_5
S : Type u_6
F : Filter R
inst : LinearOrder R
inst_1 : LinearOrder S
f : R → S
f_incr : Monotone f
l : R
freq_ge : ∃ᶠ (x : R) in F, l ≤ x
ev : ∀ᶠ (x : S) in map f F, x < f l
z : R
hz : z ∈ f ⁻¹' {x : S | x < f l}
con : ¬z < l
⊢ False

Tactic:
exact lt_irrefl (f l) <| lt_of_le_of_lt (f_incr <| not_lt.mp con) hz

Premises used: lt_of_le_of_lt, lt_irrefl, not_lt, Iff.mp
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
R : Type u_5
S : Type u_6
F : Filter R
inst : LinearOrder R
inst_1 : LinearOrder S
f : R → S
f_incr : Monotone f
u : R
freq_le : ∃ᶠ (x : R) in F, x ≤ u
⊢ ∃ᶠ (y : S) in map f F, y ≤ f u

Tactic:
fun ev ↦ freq_le ?_

Premises used: Filter.Frequently, Not
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
R : Type u_5
S : Type u_6
F : Filter R
inst : LinearOrder R
inst_1 : LinearOrder S
f : R → S
f_incr : Monotone f
u : R
freq_le : ∃ᶠ (x : R) in F, x ≤ u
refine : ∀ (ev : ∀ᶠ (x : S) in map f F, ¬(fun (y : S) ↦ y ≤ f u) x), ∀ᶠ (x : R) in F, ¬(fun (x : R) ↦ x ≤ u) x
⊢ ∃ᶠ (y : S) in map f F, y ≤ f u

Tactic:
refine fun ev ↦ freq_le ?_
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
R : Type u_5
S : Type u_6
F : Filter R
inst : LinearOrder R
inst_1 : LinearOrder S
f : R → S
f_incr : Monotone f
u : R
freq_le : ∃ᶠ (x : R) in F, x ≤ u
ev : ∀ᶠ (x : S) in map f F, ¬(fun (y : S) ↦ y ≤ f u) x
simp : ∀ (ev : ∀ᶠ (x : S) in map f F, f u < x), ∀ᶠ (x : R) in F, u < x
⊢ ∀ᶠ (x : R) in F, ¬(fun (x : R) ↦ x ≤ u) x

Tactic:
simp only [not_le] at ev freq_le ⊢

Premises used: not_le
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
R : Type u_5
S : Type u_6
F : Filter R
inst : LinearOrder R
inst_1 : LinearOrder S
f : R → S
f_incr : Monotone f
u : R
freq_le : ∃ᶠ (x : R) in F, x ≤ u
ev : ∀ᶠ (x : S) in map f F, f u < x
h : ∀ (z : R) (hz : z ∈ f ⁻¹' {x : S | f u < x}), u < z
⊢ ∀ᶠ (x : R) in F, u < x

Tactic:
filter_upwards [ev] with z hz
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
R : Type u_5
S : Type u_6
F : Filter R
inst : LinearOrder R
inst_1 : LinearOrder S
f : R → S
f_incr : Monotone f
u : R
freq_le : ∃ᶠ (x : R) in F, x ≤ u
ev : ∀ᶠ (x : S) in map f F, f u < x
z : R
hz : z ∈ f ⁻¹' {x : S | f u < x}
h : ∀ (con : ¬u < z), False
⊢ u < z

Tactic:
by_contra con
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
R : Type u_5
S : Type u_6
F : Filter R
inst : LinearOrder R
inst_1 : LinearOrder S
f : R → S
f_incr : Monotone f
u : R
freq_le : ∃ᶠ (x : R) in F, x ≤ u
ev : ∀ᶠ (x : S) in map f F, f u < x
z : R
hz : z ∈ f ⁻¹' {x : S | f u < x}
con : ¬u < z
⊢ False

Tactic:
apply lt_irrefl (f u) <| lt_of_lt_of_le hz <| f_incr (not_lt.mp con)

Premises used: lt_irrefl, not_lt, Iff.mp, lt_of_lt_of_le
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
R : Type u_5
S : Type u_6
F : Filter R
inst : LinearOrder R
inst_1 : LinearOrder S
f : R → S
f_decr : Antitone f
l : R
frbdd : ∃ᶠ (x : R) in F, l ≤ x
⊢ ∃ᶠ (y : S) in map f F, y ≤ f l

Tactic:
Monotone.frequently_ge_map_of_frequently_ge (S := Sᵒᵈ) f_decr frbdd

Premises used: Monotone.frequently_ge_map_of_frequently_ge, OrderDual
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
R : Type u_5
S : Type u_6
F : Filter R
inst : LinearOrder R
inst_1 : LinearOrder S
f : R → S
f_decr : Antitone f
u : R
frbdd : ∃ᶠ (x : R) in F, x ≤ u
⊢ ∃ᶠ (y : S) in map f F, f u ≤ y

Tactic:
Monotone.frequently_le_map_of_frequently_le (S := Sᵒᵈ) f_decr frbdd

Premises used: Monotone.frequently_le_map_of_frequently_le, OrderDual
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
R : Type u_5
S : Type u_6
F : Filter R
inst : LinearOrder R
inst_1 : LinearOrder S
f : R → S
f_incr : Monotone f
inst_2 : F.NeBot
cobdd : IsCobounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
obtain : ∀ (l : R) (hl : ∃ᶠ (x : R) in F, l ≤ x), IsCoboundedUnder (fun (x1 x2 : S) ↦ x1 ≤ x2) F f
⊢ IsCoboundedUnder (fun (x1 x2 : S) ↦ x1 ≤ x2) F f

Tactic:
obtain ⟨l, hl⟩ := IsCobounded.frequently_ge cobdd

Premises used: Filter.IsCobounded.frequently_ge
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
R : Type u_5
S : Type u_6
F : Filter R
inst : LinearOrder R
inst_1 : LinearOrder S
f : R → S
f_incr : Monotone f
inst_2 : F.NeBot
cobdd : IsCobounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
l : R
hl : ∃ᶠ (x : R) in F, l ≤ x
⊢ IsCoboundedUnder (fun (x1 x2 : S) ↦ x1 ≤ x2) F f

Tactic:
IsCobounded.of_frequently_ge <| f_incr.frequently_ge_map_of_frequently_ge hl

Premises used: Filter.IsCobounded.of_frequently_ge, Filter.IsCoboundedUnder, Monotone.frequently_ge_map_of_frequently_ge
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
R : Type u_5
S : Type u_6
F : Filter R
inst : LinearOrder R
inst_1 : LinearOrder S
f : R → S
f_incr : Monotone f
inst_2 : F.NeBot
cobdd : IsCobounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
l : R
hl : ∃ᶠ (x : R) in F, l ≤ x
⊢ IsCoboundedUnder (fun (x1 x2 : S) ↦ x1 ≤ x2) F f

Tactic:
exact IsCobounded.of_frequently_ge <| f_incr.frequently_ge_map_of_frequently_ge hl

Premises used: Filter.IsCobounded.of_frequently_ge, Monotone.frequently_ge_map_of_frequently_ge
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
R : Type u_5
S : Type u_6
F : Filter R
inst : LinearOrder R
inst_1 : LinearOrder S
f : R → S
f_incr : Monotone f
inst_2 : F.NeBot
cobdd : IsCobounded (fun (x1 x2 : R) ↦ x1 ≥ x2) F
⊢ IsCoboundedUnder (fun (x1 x2 : S) ↦ x1 ≥ x2) F f

Tactic:
Monotone.isCoboundedUnder_le_of_isCobounded (R := Rᵒᵈ) (S := Sᵒᵈ) f_incr.dual cobdd

Premises used: Monotone.dual, OrderDual, Monotone.isCoboundedUnder_le_of_isCobounded
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
R : Type u_5
S : Type u_6
F : Filter R
inst : LinearOrder R
inst_1 : LinearOrder S
f : R → S
f_decr : Antitone f
inst_2 : F.NeBot
cobdd : IsCobounded (fun (x1 x2 : R) ↦ x1 ≥ x2) F
⊢ IsCoboundedUnder (fun (x1 x2 : S) ↦ x1 ≤ x2) F f

Tactic:
Monotone.isCoboundedUnder_le_of_isCobounded (R := Rᵒᵈ) f_decr.dual cobdd

Premises used: Antitone.dual, OrderDual, Monotone.isCoboundedUnder_le_of_isCobounded
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
R : Type u_5
S : Type u_6
F : Filter R
inst : LinearOrder R
inst_1 : LinearOrder S
f : R → S
f_decr : Antitone f
inst_2 : F.NeBot
cobdd : IsCobounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
⊢ IsCoboundedUnder (fun (x1 x2 : S) ↦ x1 ≥ x2) F f

Tactic:
Monotone.isCoboundedUnder_le_of_isCobounded (S := Sᵒᵈ) f_decr cobdd

Premises used: OrderDual, Monotone.isCoboundedUnder_le_of_isCobounded
-- Module: Mathlib.Order.Filter.Ker
Goal:
α : Type u_2
f : Filter α
⊢ f.ker = ⋂ s ∈ f, s

Tactic:
sInter_eq_biInter

Premises used: Set.sInter_eq_biInter, Filter.ker
-- Module: Mathlib.Order.Filter.Ker
Goal:
α : Type u_2
f : Filter α
a : α
⊢ a ∈ f.ker ↔ ∀ s ∈ f, a ∈ s

Tactic:
mem_sInter

Premises used: Set.Mem, Set.mem_sInter, Filter.ker
-- Module: Mathlib.Order.Filter.Ker
Goal:
α : Type u_2
f : Filter α
s : Set α
⊢ s ⊆ f.ker ↔ ∀ t ∈ f, s ⊆ t

Tactic:
subset_sInter_iff

Premises used: Set.subset_sInter_iff, Filter.ker
-- Module: Mathlib.Order.Filter.Ker
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
f_1 g : Filter α
s_1 : Set α
a : α
s : Set α
f : Filter α
⊢ 𝓟 s ≤ f ↔ s ≤ f.ker

Tactic:
simp [principal_le_iff]

Premises used: Filter.principal_le_iff
-- Module: Mathlib.Order.Filter.Ker
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
f g : Filter α
s : Set α
a : α
⊢ ∀ (b : Set α) (x : α), (∀ (s : Set α), (∀ x ∈ b, x ∈ s) → x ∈ s) → x ∈ b

Tactic:
aesop
-- Module: Mathlib.Order.Filter.Ker
Goal:
α : Type u_2
⊢ Monotone.{u_2, u_2} (α := Filter α) ker

Tactic:
gi_principal_ker.gc.monotone_u

Premises used: GaloisConnection.monotone_u, GaloisCoinsertion.gc, Filter.gi_principal_ker
-- Module: Mathlib.Order.Filter.Ker
Goal:
α : Type u_2
⊢ Surjective.{u_2 + 1, u_2 + 1} (α := Filter α) ker

Tactic:
gi_principal_ker.u_surjective

Premises used: Filter.gi_principal_ker, GaloisCoinsertion.u_surjective
-- Module: Mathlib.Order.Filter.Ker
Goal:
α : Type u_2
⊢ Eq.{u_2 + 1} (α := Set α) (ker ⊥) ∅

Tactic:
sInter_eq_empty_iff.2 fun _ ↦ ⟨∅, trivial, id⟩

Premises used: Iff.mpr, trivial, id, And.intro, Exists.intro, EmptyCollection.emptyCollection, Set.sInter_eq_empty_iff, Filter.ker
-- Module: Mathlib.Order.Filter.Ker
Goal:
α : Type u_2
⊢ Eq.{u_2 + 1} (α := Set α) (ker ⊤) univ

Tactic:
gi_principal_ker.gc.u_top

Premises used: GaloisConnection.u_top, GaloisCoinsertion.gc, Filter.gi_principal_ker
-- Module: Mathlib.Order.Filter.Ker
Goal:
α : Type u_2
f : Filter α
⊢ 𝓟 ⊤ ≤ f ↔ f = ⊤

Tactic:
simp
-- Module: Mathlib.Order.Filter.Ker
Goal:
α : Type u_2
f g : Filter α
⊢ (f ⊓ g).ker = f.ker ∩ g.ker

Tactic:
gi_principal_ker.gc.u_inf

Premises used: GaloisConnection.u_inf, GaloisCoinsertion.gc, Filter.gi_principal_ker
-- Module: Mathlib.Order.Filter.Ker
Goal:
ι : Sort u_1
α : Type u_2
f : ι → Filter α
⊢ Eq.{u_2 + 1} (α := Set α) (ker (⨅ (i : ι), f i)) (⋂ (i : ι), (f i).ker)

Tactic:
gi_principal_ker.gc.u_iInf

Premises used: Set.iInter, GaloisConnection.u_iInf, GaloisCoinsertion.gc, Filter.gi_principal_ker
-- Module: Mathlib.Order.Filter.Ker
Goal:
α : Type u_2
S : Set (Filter α)
⊢ (sInf S).ker = ⋂ f ∈ S, f.ker

Tactic:
gi_principal_ker.gc.u_sInf

Premises used: Set.iInter, GaloisCoinsertion.gc, Filter.gi_principal_ker, GaloisConnection.u_sInf
-- Module: Mathlib.Order.Filter.Ker
Goal:
α : Type u_2
s : Set α
⊢ (𝓟 s).ker = s

Tactic:
gi_principal_ker.u_l_eq _

Premises used: Filter.gi_principal_ker, GaloisCoinsertion.u_l_eq
-- Module: Mathlib.Order.Filter.Ker
Goal:
α : Type u_2
a : α
rw : Eq (α := Set α) (ker (𝓟 {a})) {a}
rw₁ rw₂ : Eq (α := Set α) {a} {a}
⊢ ker (pure a) = {a}

Tactic:
rw [← principal_singleton, ker_principal]

Premises used: Filter.ker_principal, Filter.principal_singleton
-- Module: Mathlib.Order.Filter.Ker
Goal:
α : Type u_2
β : Type u_3
m : α → β
f : Filter β
h : ∀ (a : α), a ∈ (comap m f).ker ↔ a ∈ m ⁻¹' f.ker
⊢ (comap m f).ker = m ⁻¹' f.ker

Tactic:
ext a
-- Module: Mathlib.Order.Filter.Ker
Goal:
α : Type u_2
β : Type u_3
m : α → β
f : Filter β
a : α
h : (∀ (b : Set β) (b_1 : b ∈ f) (a_1 : Set α), m ⁻¹' b ⊆ a_1 → a ∈ a_1) ↔ ∀ s ∈ f, m a ∈ s
⊢ a ∈ (comap m f).ker ↔ a ∈ m ⁻¹' f.ker

Tactic:
simp only [mem_ker, mem_comap, forall_exists_index, and_imp, @forall_comm (Set α), mem_preimage]

Premises used: and_imp, forall_comm, forall_exists_index, Filter.mem_ker, Filter.mem_comap, Set.mem_preimage
-- Module: Mathlib.Order.Filter.Ker
Goal:
α : Type u_2
β : Type u_3
m : α → β
f : Filter β
a : α
⊢ (∀ (b : Set β) (b_1 : b ∈ f) (a_1 : Set α), m ⁻¹' b ⊆ a_1 → a ∈ a_1) ↔ ∀ s ∈ f, m a ∈ s

Tactic:
forall₂_congr fun s _ ↦ ⟨fun h ↦ h _ Subset.rfl, fun ha t ht ↦ ht ha⟩

Premises used: Set.Subset.rfl, forall₂_congr, Set.preimage, Iff.intro
-- Module: Mathlib.Order.Filter.Ker
Goal:
α : Type u_2
β : Type u_3
m : α → β
f : Filter β
a : α
⊢ (∀ (b : Set β) (b_1 : b ∈ f) (a_1 : Set α), m ⁻¹' b ⊆ a_1 → a ∈ a_1) ↔ ∀ s ∈ f, m a ∈ s

Tactic:
exact forall₂_congr fun s _ ↦ ⟨fun h ↦ h _ Subset.rfl, fun ha t ht ↦ ht ha⟩

Premises used: forall₂_congr, Iff.intro
-- Module: Mathlib.Order.Filter.Ker
Goal:
ι : Sort u_1
α : Type u_2
f : ι → Filter α
⊢ Eq.{u_2 + 1} (α := Set α) (ker (⨆ (i : ι), f i)) (⋃ (i : ι), (f i).ker)

Tactic:
subset_antisymm (fun x hx ↦ ?_) ker_mono.le_map_iSup

Premises used: Monotone.le_map_iSup, subset_antisymm, Filter.ker_mono
-- Module: Mathlib.Order.Filter.Ker
Goal:
ι : Sort u_1
α : Type u_2
f : ι → Filter α
refine :
  ∀ (x : α) (hx : Membership.mem (γ := Set α) (ker (⨆ (i : ι), f i)) x),
    Membership.mem (γ := Set α) (⋃ (i : ι), (f i).ker) x
⊢ Eq.{u_2 + 1} (α := Set α) (ker (⨆ (i : ι), f i)) (⋃ (i : ι), (f i).ker)

Tactic:
refine subset_antisymm (fun x hx ↦ ?_) ker_mono.le_map_iSup

Premises used: subset_antisymm
-- Module: Mathlib.Order.Filter.Ker
Goal:
ι : Sort u_1
α : Type u_2
f : ι → Filter α
x : α
hx : Membership.mem (γ := Set α) (ker (⨆ (i : ι), f i)) x
simp : ∀ (hx : ∀ (s : Set α), Membership.mem (γ := Filter α) (⨆ (i : ι), f i) s → x ∈ s), ∃ (i : ι), ∀ s ∈ f i, x ∈ s
⊢ Membership.mem (γ := Set α) (⋃ (i : ι), (f i).ker) x

Tactic:
simp only [mem_iUnion, mem_ker] at hx ⊢

Premises used: Set.mem_iUnion, Filter.mem_ker
-- Module: Mathlib.Order.Filter.Ker
Goal:
ι : Sort u_1
α : Type u_2
f : ι → Filter α
x : α
hx : ∀ (s : Set α), Membership.mem (γ := Filter α) (⨆ (i : ι), f i) s → x ∈ s
contrapose! :
  ∀ (hx : ∀ (i : ι), ∃ s ∈ f i, x ∉ s), ∃ (s : Set α), Membership.mem (γ := Filter α) (⨆ (i : ι), f i) s ∧ x ∉ s
⊢ ∃ (i : ι), ∀ s ∈ f i, x ∈ s

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

Tactic:
choose s hsf hxs using hx