awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : Filter α
u v : α → β
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in map u 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) (max (u a) (v a)) c
⊢ ∀ᶠ (a : α) in f, (fun (x1 x2 : β) ↦ x1 ≤ x2) (u a) c
have h : ∀ (x : α), (fun (x1 x2 : β) ↦ x1 ≤ x2) (max (u x) (v x)) c → (fun (x1 x2 : β) ↦ x1 ≤ x2) (u x) c
Tactic: refine hc.mono (fun _ ↦ ?_)
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : Filter α
u v : α → β
h' : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
⊢ IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ max (u a) (v a)
have inr : ∀ (b : β) (hb : ∀ (a : β), (∀ᶠ (x : β) in map v f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x a) → (fun (x1 x2 : β) ↦ x1 ≤ x2) b a),
  IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ max (u a) (v a)
Tactic: rcases h' with ⟨b, hb⟩
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : Filter α
u v : α → β
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in map v f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x a) → (fun (x1 x2 : β) ↦ x1 ≤ x2) b a
⊢ IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ max (u a) (v a)
have h : ∀ (a : β),
  (∀ᶠ (x : β) in map (fun (a : α) ↦ max (u a) (v a)) f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x a) →
    (fun (x1 x2 : β) ↦ x1 ≤ x2) b a
Tactic: use b
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : Filter α
u v : α → β
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in map v f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x a) → (fun (x1 x2 : β) ↦ x1 ≤ x2) b a
c : β
hc : ∀ᶠ (x : β) in map (fun (a : α) ↦ max (u a) (v a)) f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x c
⊢ b ≤ c
have h : ∀ᶠ (x : β) in map v f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x c
Tactic: apply hb c
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : Filter α
u v : α → β
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in map v f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x a) → (fun (x1 x2 : β) ↦ x1 ≤ x2) b a
c : β
hc : ∀ᶠ (x : β) in map (fun (a : α) ↦ max (u a) (v a)) f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x c
⊢ ∀ᶠ (x : β) in map v f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x c
have h : ∀ (hc : ∀ᶠ (a : α) in f, (fun (x1 x2 : β) ↦ x1 ≤ x2) (max (u a) (v a)) c),
  ∀ᶠ (a : α) in f, (fun (x1 x2 : β) ↦ x1 ≤ x2) (v a) c
Tactic: rw [eventually_map] at hc ⊢
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : Filter α
u v : α → β
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in map v 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) (max (u a) (v a)) c
⊢ ∀ᶠ (a : α) in f, (fun (x1 x2 : β) ↦ x1 ≤ x2) (v a) c
have h : ∀ (x : α), (fun (x1 x2 : β) ↦ x1 ≤ x2) (max (u x) (v x)) c → (fun (x1 x2 : β) ↦ x1 ≤ x2) (v x) c
Tactic: refine hc.mono (fun _ ↦ ?_)
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
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.sup' hs fun (i : ι) ↦ F i a
have 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' hs fun (i : ι) ↦ F i a
Tactic: choose! m hm using h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : LinearOrder β
inst_1 : Nonempty β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
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' hs fun (i : ι) ↦ F i a
have h : ∀ᶠ (x : β) in Filter.map (fun (a : α) ↦ s.sup' hs fun (i : ι) ↦ F i a) f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x (s.sup' hs m)
Tactic: use sup' s hs m
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : LinearOrder β
inst_1 : Nonempty β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
m : (i : ι) → β
hm : ∀ i ∈ s, ∀ᶠ (x : β) in Filter.map (F i) f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x (m i)
⊢ ∀ᶠ (x : β) in Filter.map (fun (a : α) ↦ s.sup' hs fun (i : ι) ↦ F i a) f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x (s.sup' hs m)
have h : ∀ (hm : ∀ i ∈ s, ∀ᶠ (a : α) in f, F i a ≤ m i), ∀ᶠ (a : α) in f, (s.sup' hs fun (i : ι) ↦ F i a) ≤ s.sup' hs m
Tactic: simp only [eventually_map] at hm ⊢
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : LinearOrder β
inst_1 : Nonempty β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
m : (i : ι) → β
hm : ∀ i ∈ s, ∀ᶠ (a : α) in f, F i a ≤ m i
⊢ ∀ᶠ (a : α) in f, (s.sup' hs fun (i : ι) ↦ F i a) ≤ s.sup' hs m
have hm₁ : ∀ᶠ (x : α) in f, ∀ i ∈ s, F i x ≤ m i
Tactic: rw [← eventually_all_finset s] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : LinearOrder β
inst_1 : Nonempty β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
m : (i : ι) → β
hm : ∀ᶠ (x : α) in f, ∀ i ∈ s, F i x ≤ m i
⊢ ∀ᶠ (a : α) in f, (s.sup' hs fun (i : ι) ↦ F i a) ≤ s.sup' hs m
have h : ∀ (a : α) (h : ∀ i ∈ s, F i a ≤ m i), (s.sup' hs fun (i : ι) ↦ F i a) ≤ s.sup' hs m
Tactic: refine hm.mono fun a h ↦ ?_
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : LinearOrder β
inst_1 : Nonempty β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
m : (i : ι) → β
hm : ∀ᶠ (x : α) in f, ∀ i ∈ s, F i x ≤ m i
a : α
h : ∀ i ∈ s, F i a ≤ m i
⊢ (s.sup' hs fun (i : ι) ↦ F i a) ≤ s.sup' hs m
have h₁ : ∀ b ∈ s, F b a ≤ s.sup' hs m
Tactic: simp only [sup'_le_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
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.sup' hs fun (i : ι) ↦ F i a
have rcases : ∀ (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),
  IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ s.sup' hs fun (i : ι) ↦ F i a
Tactic: rcases h with ⟨i, i_s, b, hb⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
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
⊢ IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ s.sup' hs fun (i : ι) ↦ F i a
have 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
Tactic: use b
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
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
have 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
Tactic: refine fun c hc ↦ hb c ?_
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
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
⊢ ∀ᶠ (x : β) in Filter.map (F i) f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x c
have 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
Tactic: rw [eventually_map] at hc ⊢
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
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
have 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
Tactic: refine hc.mono fun a h ↦ ?_
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (hypothesis)
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
⊢ (fun (x1 x2 : β) ↦ x1 ≤ x2) (F i a) c
have h₁ : ∀ b ∈ s, F b a ≤ c
Tactic: simp only [sup'_le_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
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)
⊢ IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ s.sup fun (i : ι) ↦ F i a
have 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
Tactic: choose! m hm using h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
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)
⊢ IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ s.sup fun (i : ι) ↦ F i a
have h : ∀ᶠ (x : β) in Filter.map (fun (a : α) ↦ s.sup fun (i : ι) ↦ F i a) f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x (s.sup m)
Tactic: use sup s m
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
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)
⊢ ∀ᶠ (x : β) in Filter.map (fun (a : α) ↦ s.sup fun (i : ι) ↦ F i a) f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x (s.sup m)
have 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
Tactic: simp only [eventually_map] at hm ⊢
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (hypothesis)
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
⊢ ∀ᶠ (a : α) in f, (s.sup fun (i : ι) ↦ F i a) ≤ s.sup m
have hm₁ : ∀ᶠ (x : α) in f, ∀ i ∈ s, F i x ≤ m i
Tactic: rw [← eventually_all_finset s] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
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'
have 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
Tactic: refine fun ev ↦ freq_ge ?_
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
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
⊢ ∀ᶠ (x : R) in F, ¬(fun (x : R) ↦ l ≤ x) x
have simp : ∀ (ev : ∀ᶠ (x : S) in map f F, x < f l), ∀ᶠ (x : R) in F, x < l
Tactic: simp only [not_le] at ev freq_ge ⊢
Cleared hypotheses: ev
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
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
⊢ ∀ᶠ (x : R) in F, x < l
have h : ∀ (z : R) (hz : z ∈ f ⁻¹' {x : S | x < f l}), z < l
Tactic: filter_upwards [ev] with z hz
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
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}
⊢ z < l
have h : ∀ (con : ¬z < l), False
Tactic: by_contra con
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
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
have 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
Tactic: refine fun ev ↦ freq_le ?_
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
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
⊢ ∀ᶠ (x : R) in F, ¬(fun (x : R) ↦ x ≤ u) x
have simp : ∀ (ev : ∀ᶠ (x : S) in map f F, f u < x), ∀ᶠ (x : R) in F, u < x
Tactic: simp only [not_le] at ev freq_le ⊢
Cleared hypotheses: ev
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
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
⊢ ∀ᶠ (x : R) in F, u < x
have h : ∀ (z : R) (hz : z ∈ f ⁻¹' {x : S | f u < x}), u < z
Tactic: filter_upwards [ev] with z hz
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
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}
⊢ u < z
have h : ∀ (con : ¬u < z), False
Tactic: by_contra con
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
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
have obtain : ∀ (l : R) (hl : ∃ᶠ (x : R) in F, l ≤ x), IsCoboundedUnder (fun (x1 x2 : S) ↦ x1 ≤ x2) F f
Tactic: obtain ⟨l, hl⟩ := IsCobounded.frequently_ge cobdd
-- Lean 4 proof step from Mathlib.Order.Filter.Ker (goal)
Goal:
α : Type u_2
a : α
⊢ ker (pure a) = {a}
have rw : Eq (α := Set α) (ker (𝓟 {a})) {a}
Tactic: rw [← principal_singleton, ker_principal]
-- Lean 4 proof step from Mathlib.Order.Filter.Ker (goal)
Goal:
α : Type u_2
a : α
rw : Eq (α := Set α) (ker (𝓟 {a})) {a}
⊢ ker (pure a) = {a}
have rw₁ : Eq (α := Set α) {a} {a}
Tactic: rw [← principal_singleton, ker_principal]
-- Lean 4 proof step from Mathlib.Order.Filter.Ker (goal)
Goal:
α : Type u_2
β : Type u_3
m : α → β
f : Filter β
⊢ (comap m f).ker = m ⁻¹' f.ker
have h : ∀ (a : α), a ∈ (comap m f).ker ↔ a ∈ m ⁻¹' f.ker
Tactic: ext a
-- Lean 4 proof step from Mathlib.Order.Filter.Ker (goal)
Goal:
α : Type u_2
β : Type u_3
m : α → β
f : Filter β
a : α
⊢ a ∈ (comap m f).ker ↔ a ∈ m ⁻¹' f.ker
have h : (∀ (b : Set β) (b_1 : b ∈ f) (a_1 : Set α), m ⁻¹' b ⊆ a_1 → a ∈ a_1) ↔ ∀ s ∈ f, m a ∈ s
Tactic: simp only [mem_ker, mem_comap, forall_exists_index, and_imp, @forall_comm (Set α), mem_preimage]
-- Lean 4 proof step from Mathlib.Order.Filter.Ker (goal)
Goal:
ι : Sort u_1
α : Type u_2
f : ι → Filter α
⊢ Eq.{u_2 + 1} (α := Set α) (ker (⨆ (i : ι), f i)) (⋃ (i : ι), (f i).ker)
have refine : ∀ (x : α) (hx : Membership.mem (γ := Set α) (ker (⨆ (i : ι), f i)) x),
  Membership.mem (γ := Set α) (⋃ (i : ι), (f i).ker) x
Tactic: refine subset_antisymm (fun x hx ↦ ?_) ker_mono.le_map_iSup
-- Lean 4 proof step from Mathlib.Order.Filter.Ker (goal)
Goal:
ι : Sort u_1
α : Type u_2
f : ι → Filter α
x : α
hx : Membership.mem (γ := Set α) (ker (⨆ (i : ι), f i)) x
⊢ Membership.mem (γ := Set α) (⋃ (i : ι), (f i).ker) x
have simp : ∀ (hx : ∀ (s : Set α), Membership.mem (γ := Filter α) (⨆ (i : ι), f i) s → x ∈ s), ∃ (i : ι), ∀ s ∈ f i, x ∈ s
Tactic: simp only [mem_iUnion, mem_ker] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Order.Filter.Ker (goal)
Goal:
ι : Sort u_1
α : Type u_2
f : ι → Filter α
x : α
hx : ∀ (s : Set α), Membership.mem (γ := Filter α) (⨆ (i : ι), f i) s → x ∈ s
⊢ ∃ (i : ι), ∀ s ∈ f i, x ∈ s
have contrapose! : ∀ (hx : ∀ (i : ι), ∃ s ∈ f i, x ∉ s), ∃ (s : Set α), Membership.mem (γ := Filter α) (⨆ (i : ι), f i) s ∧ x ∉ s
Tactic: contrapose! hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Order.Filter.Ker (goal)
Goal:
ι : Sort u_1
α : Type u_2
f : ι → Filter α
x : α
hx : ∀ (i : ι), ∃ s ∈ f i, x ∉ s
⊢ ∃ (s : Set α), Membership.mem (γ := Filter α) (⨆ (i : ι), f i) s ∧ x ∉ s
have 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
Tactic: choose s hsf hxs using hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Order.Filter.Ker (goal)
Goal:
ι : Sort u_1
α : Type u_2
f : ι → Filter α
x : α
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
have refine : Membership.mem (γ := Filter α) (⨆ (i : ι), f i) (⋃ (i : ι), s i)
Tactic: refine ⟨⋃ i, s i, ?_, by simpa⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Ker (goal)
Goal:
α : Type u_2
f g : Filter α
⊢ (f ⊔ g).ker = f.ker ∪ g.ker
have rw : ker (sSup {f, g}) = f.ker ∪ g.ker
Tactic: rw [← sSup_pair, ker_sSup, biUnion_pair]
-- Lean 4 proof step from Mathlib.Order.Filter.Ker (goal)
Goal:
α : Type u_2
f g : Filter α
rw : ker (sSup {f, g}) = f.ker ∪ g.ker
⊢ (f ⊔ g).ker = f.ker ∪ g.ker
have rw₁ : ⋃ (f_1 : Filter α), ⋃ (_ : Membership.mem (γ := Set (Filter α)) {f, g} f_1), f_1.ker = f.ker ∪ g.ker
Tactic: rw [← sSup_pair, ker_sSup, biUnion_pair]
-- Lean 4 proof step from Mathlib.Order.Filter.Ker (goal)
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
⊢ (f ⊔ g).ker = f.ker ∪ g.ker
have rw₂ : f.ker ∪ g.ker = f.ker ∪ g.ker
Tactic: rw [← sSup_pair, ker_sSup, biUnion_pair]
-- Lean 4 proof step from Mathlib.Order.Filter.Lift (goal)
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
have refine_1 : DirectedOn (g ⁻¹'o fun (x1 x2 : Filter γ) ↦ x1 ≥ x2) f.sets
Tactic: refine (mem_biInf_of_directed ?_ ⟨univ, univ_sets _⟩).trans ?_
-- Lean 4 proof step from Mathlib.Order.Filter.Lift (goal)
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
⊢ s ∈ f.lift g ↔ ∃ (i : ι), p i ∧ ∃ (x : β i), pg i x ∧ sg i x ⊆ s
have refine_2 : (∃ i ∈ f.sets, s ∈ g i) ↔ ∃ (i : ι), p i ∧ ∃ (x : β i), pg i x ∧ sg i x ⊆ s
Tactic: refine (mem_biInf_of_directed ?_ ⟨univ, univ_sets _⟩).trans ?_
-- Lean 4 proof step from Mathlib.Order.Filter.Lift (goal)
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 ∧ ∃ (x : β i), pg i x ∧ sg i x ⊆ s
have refine_2 : (∃ i ∈ f.sets, s ∈ g i) ↔ ∃ (i : ι), p i ∧ s ∈ g (s_1 i)
Tactic: simp only [← (hg _).mem_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.Lift (goal)
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))
have 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
Tactic: refine ⟨fun t => (hf.mem_lift_iff hg gm).trans ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Lift (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Set α → Filter β
m : γ → β
⊢ comap m (f.lift g) = f.lift (comap m ∘ g)
have simp : Eq.{u_3 + 1} (α := Filter γ) (⨅ i ∈ f, comap m (g i)) (⨅ s ∈ f, (comap m ∘ g) s)
Tactic: simp only [Filter.lift, comap_iInf]
-- Lean 4 proof step from Mathlib.Order.Filter.Lift (goal)
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
have refine : ∀ s ∈ (iInf f).lift g, Membership.mem (γ := Filter β) (⨅ (i : ι), (f i).lift g) s
Tactic: refine lift_iInf_le.antisymm fun s => ?_
-- Lean 4 proof step from Mathlib.Order.Filter.Lift (goal)
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
have refine_1 : ⨅ (i : ι), (f i).lift g ≤ g univ
Tactic: refine iInf_sets_induct ht ?_ fun hs ht => ?_
-- Lean 4 proof step from Mathlib.Order.Filter.Lift (goal)
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
⊢ ⨅ (i : ι), (f i).lift g ≤ g t
have 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₂)
Tactic: refine iInf_sets_induct ht ?_ fun hs ht => ?_