awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Filter.Germ.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f_1 g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f_2 : l.Germ M
f : α → M
⊢ HSMul.hSMul (α := R) (β := l.Germ M) 0 (↑f : l.Germ M) = 0
have norm_cast : HSMul.hSMul (α := R) 0 f =ᶠ[l] 0
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Order.Filter.Germ.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f_1 g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
c₁_1 c₂_1 : l.Germ R
f_2 : l.Germ M
c₁ c₂ : α → R
f : α → M
⊢ HSMul.hSMul (β := l.Germ M) (HAdd.hAdd (α := l.Germ R) (↑c₁ : l.Germ R) (↑c₂ : l.Germ R)) (↑f : l.Germ M) =
    HSMul.hSMul (α := l.Germ R) (β := l.Germ M) (↑c₁ : l.Germ R) (↑f : l.Germ M) +
      HSMul.hSMul (α := l.Germ R) (β := l.Germ M) (↑c₂ : l.Germ R) (↑f : l.Germ M)
have norm_cast : (c₁ + c₂) • f =ᶠ[l] c₁ • f + c₂ • f
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Order.Filter.Germ.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f_1 g_1 h_1 : α → β
inst : Mul β
inst_1 : LE β
inst_2 : ExistsMulOfLE β
x y : l.Germ β
f g : α → β
h : f ≤ᶠ[l] g
⊢ ∃ (c : l.Germ β), (↑g : l.Germ β) = (↑f : l.Germ β) * c
have choose : ∀ (c : (x : α) → (hx : f x ≤ g x) → β) (hc : ∀ (x : α) (hx : f x ≤ g x), g x = f x * c x hx),
  ∃ (c : l.Germ β), (↑g : l.Germ β) = (↑f : l.Germ β) * c
Tactic: choose c hc using fun x (hx : f x ≤ g x) ↦ exists_mul_of_le hx
-- Lean 4 proof step from Mathlib.Order.Filter.Germ.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f_1 g_1 h_1 : α → β
inst : Mul β
inst_1 : LE β
inst_2 : ExistsMulOfLE β
x y : l.Germ β
f g : α → β
h : f ≤ᶠ[l] g
c : (x : α) → (hx : f x ≤ g x) → β
hc : ∀ (x : α) (hx : f x ≤ g x), g x = f x * c x hx
⊢ ∃ (c : l.Germ β), (↑g : l.Germ β) = (↑f : l.Germ β) * c
have refine : g =ᶠ[l]
  (fun (f g : α → β) (x : α) ↦ ((fun (x1 x2 : β) ↦ x1 * x2) (f x) (g x) : β)) f fun (x : α) ↦
    if hx : f x ≤ g x then c x hx else f x
Tactic: refine ⟨ofFun fun x ↦ if hx : f x ≤ g x then c x hx else f x, coe_eq.2 ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Germ.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f_1 g_1 h_1 : α → β
inst : Mul β
inst_1 : LE β
inst_2 : ExistsMulOfLE β
x y : l.Germ β
f g : α → β
h : f ≤ᶠ[l] g
c : (x : α) → (hx : f x ≤ g x) → β
hc : ∀ (x : α) (hx : f x ≤ g x), g x = f x * c x hx
⊢ g =ᶠ[l]
    (fun (f g : α → β) (x : α) ↦ ((fun (x1 x2 : β) ↦ x1 * x2) (f x) (g x) : β)) f fun (x : α) ↦
      if hx : f x ≤ g x then c x hx else f x
have h₁ : ∀ (x : α) (hx : f x ≤ g x), g x = f x * if hx : f x ≤ g x then c x hx else f x
Tactic: filter_upwards [h] with x hx
-- Lean 4 proof step from Mathlib.Order.Filter.Germ.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f_1 g_1 h_1 : α → β
inst : Mul β
inst_1 : LE β
inst_2 : ExistsMulOfLE β
x_1 y : l.Germ β
f g : α → β
h : f ≤ᶠ[l] g
c : (x : α) → (hx : f x ≤ g x) → β
hc : ∀ (x : α) (hx : f x ≤ g x), g x = f x * c x hx
x : α
hx : f x ≤ g x
⊢ g x = f x * if hx : f x ≤ g x then c x hx else f x
have h₁ : g x = f x * c x hx
Tactic: rw [dif_pos hx, hc]
-- Lean 4 proof step from Mathlib.Order.Filter.Germ.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f_1 g_1 h_1 : α → β
inst : Mul β
inst_1 : LE β
inst_2 : ExistsMulOfLE β
x_1 y : l.Germ β
f g : α → β
h : f ≤ᶠ[l] g
c : (x : α) → (hx : f x ≤ g x) → β
hc : ∀ (x : α) (hx : f x ≤ g x), g x = f x * c x hx
x : α
hx : f x ≤ g x
h₁ : g x = f x * c x hx
⊢ g x = f x * if hx : f x ≤ g x then c x hx else f x
have h₂ : f x * c x hx = f x * c x hx
Tactic: rw [dif_pos hx, hc]
-- Lean 4 proof step from Mathlib.Order.Filter.Germ.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f_1 g_1 h_1 : α → β
inst : Mul β
inst_1 : LE β
inst_2 : ExistsMulOfLE β
x y : l.Germ β
f g : α → β
h : f ≤ᶠ[l] g
⊢ ∃ (c : l.Germ β), (↑g : l.Germ β) = (↑f : l.Germ β) * c
have choose : ∀ (c : (x : α) → (hx : f x ≤ g x) → β) (hc : ∀ (x : α) (hx : f x ≤ g x), g x = f x * c x hx),
  ∃ (c : l.Germ β), (↑g : l.Germ β) = (↑f : l.Germ β) * c
Tactic: classical
    choose c hc using fun x (hx : f x ≤ g x) ↦ exists_mul_of_le hx
    refine ⟨ofFun fun x ↦ if hx : f x ≤ g x then c x hx else f x, coe_eq.2 ?_⟩
    filter_upwards [h] with x hx
    rw [dif_pos hx, hc]
-- Lean 4 proof step from Mathlib.Order.Filter.Germ.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f_1 g_1 h_1 : α → β
inst : Mul β
inst_1 : LE β
inst_2 : ExistsMulOfLE β
x y : l.Germ β
f g : α → β
h : f ≤ᶠ[l] g
choose :
  ∀ (c : (x : α) → (hx : f x ≤ g x) → β) (hc : ∀ (x : α) (hx : f x ≤ g x), g x = f x * c x hx),
    ∃ (c : l.Germ β), (↑g : l.Germ β) = (↑f : l.Germ β) * c
⊢ ∃ (c : l.Germ β), (↑g : l.Germ β) = (↑f : l.Germ β) * c
have choose₁ : ∀ (c : (x : α) → (hx : f x ≤ g x) → β) (hc : ∀ (x : α) (hx : f x ≤ g x), g x = f x * c x hx),
  g =ᶠ[l]
    (fun (f g : α → β) (x : α) ↦ ((fun (x1 x2 : β) ↦ x1 * x2) (f x) (g x) : β)) f fun (x : α) ↦
      if hx : f x ≤ g x then c x hx else f x
Tactic: classical
    choose c hc using fun x (hx : f x ≤ g x) ↦ exists_mul_of_le hx
    refine ⟨ofFun fun x ↦ if hx : f x ≤ g x then c x hx else f x, coe_eq.2 ?_⟩
    filter_upwards [h] with x hx
    rw [dif_pos hx, hc]
-- Lean 4 proof step from Mathlib.Order.Filter.Germ.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f_1 g_1 h_1 : α → β
inst : Mul β
inst_1 : LE β
inst_2 : ExistsMulOfLE β
x y : l.Germ β
f g : α → β
h : f ≤ᶠ[l] g
choose :
  ∀ (c : (x : α) → (hx : f x ≤ g x) → β) (hc : ∀ (x : α) (hx : f x ≤ g x), g x = f x * c x hx),
    ∃ (c : l.Germ β), (↑g : l.Germ β) = (↑f : l.Germ β) * c
choose₁ :
  ∀ (c : (x : α) → (hx : f x ≤ g x) → β) (hc : ∀ (x : α) (hx : f x ≤ g x), g x = f x * c x hx),
    g =ᶠ[l]
      (fun (f g : α → β) (x : α) ↦ ((fun (x1 x2 : β) ↦ x1 * x2) (f x) (g x) : β)) f fun (x : α) ↦
        if hx : f x ≤ g x then c x hx else f x
⊢ ∃ (c : l.Germ β), (↑g : l.Germ β) = (↑f : l.Germ β) * c
have h₁ : ∀ (c : (x : α) → (hx : f x ≤ g x) → β) (hc : ∀ (x : α) (hx : f x ≤ g x), g x = f x * c x hx) (x : α) (hx : f x ≤ g x),
  g x = f x * if hx : f x ≤ g x then c x hx else f x
Tactic: classical
    choose c hc using fun x (hx : f x ≤ g x) ↦ exists_mul_of_le hx
    refine ⟨ofFun fun x ↦ if hx : f x ≤ g x then c x hx else f x, coe_eq.2 ?_⟩
    filter_upwards [h] with x hx
    rw [dif_pos hx, hc]
-- Lean 4 proof step from Mathlib.Order.Filter.IndicatorFunction (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_5
inst : One β
s : ι → Set α
f : α → β
a : α
⊢ EventuallyEq.{u_5, u_2} (β := β) atTop (fun (n : Finset ι) ↦ mulIndicator (⋃ i ∈ n, s i) f a) fun (x : Finset ι) ↦
    (iUnion s).mulIndicator f a
have rw : EventuallyEq.{u_5, u_2} (β := β) atTop (fun (n : Finset ι) ↦ mulIndicator (⋃ i ∈ n, s i) f a) fun (x : Finset ι) ↦
  mulIndicator (⋃ (t : Finset ι), ⋃ i ∈ t, s i) f a
Tactic: rw [iUnion_eq_iUnion_finset s]
-- Lean 4 proof step from Mathlib.Order.Filter.IndicatorFunction (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_5
inst : One β
s : ι → Set α
f : α → β
a : α
⊢ EventuallyEq.{u_5, u_2} (β := β) atTop (fun (n : Finset ι) ↦ mulIndicator (⋃ i ∈ n, s i) f a) fun (x : Finset ι) ↦
    mulIndicator (⋃ (t : Finset ι), ⋃ i ∈ t, s i) f a
have hs : Monotone.{u_5, u_1} (β := Set α) fun (i : Finset ι) ↦ ⋃ i_1 ∈ i, s i_1
Tactic: apply Monotone.mulIndicator_eventuallyEq_iUnion
-- Lean 4 proof step from Mathlib.Order.Filter.IndicatorFunction (goal)
Goal:
α : Type u_1
β : Type u_2
inst : One β
l : Filter α
f : α → β
s : Set α
hf : f =ᶠ[l] 1
⊢ EventuallyEq.{u_1, u_2} (β := β) l (s.mulIndicator 1) 1
have rw : EventuallyEq.{u_1, u_2} (β := β) l 1 1
Tactic: rw [mulIndicator_one']
-- Lean 4 proof step from Mathlib.Order.Filter.IndicatorFunction (goal)
Goal:
α : Type u_1
β : Type u_2
inst : One β
l : Filter α
f : α → β
hf : ∀ᶠ (x : α) in l, f x ≠ 1
s_1 t : Set α
h : s_1.mulIndicator f =ᶠ[l] t.mulIndicator f
s : Set α
⊢ Function.mulSupport (s.mulIndicator f) =ᶠ[l] s
have rw : s ∩ Function.mulSupport f =ᶠ[l] s
Tactic: rw [mulSupport_mulIndicator]
-- Lean 4 proof step from Mathlib.Order.Filter.IndicatorFunction (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : One β
l : Filter α
f : α → β
hf : ∀ᶠ (x : α) in l, f x ≠ 1
s t : Set α
h : s.mulIndicator f =ᶠ[l] t.mulIndicator f
⊢ s =ᶠ[l] t
have this : ∀ {s : Set α}, Function.mulSupport (s.mulIndicator f) =ᶠ[l] s
Tactic: have : ∀ {s : Set α}, Function.mulSupport (s.mulIndicator f) =ᶠ[l] s := fun {s} ↦ by
    rw [mulSupport_mulIndicator]
    exact (hf.mono fun x hx ↦ and_iff_left hx).set_eq
-- Lean 4 proof step from Mathlib.Order.Filter.Interval (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
a : α
⊢ TendstoIxxClass Icc (pure a) (pure a)
have rw : TendstoIxxClass (α := α) Icc (𝓟 {a}) (𝓟 {a})
Tactic: rw [← principal_singleton]
-- Lean 4 proof step from Mathlib.Order.Filter.Interval (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
l : Filter α
inst_1 : TendstoIxxClass Icc l l
⊢ TendstoIxxClass uIcc l l
have refine : ∀ (s : Set (Set α)) (hs : s ∈ l.smallSets), ∃ t ∈ l, t ×ˢ t ⊆ (fun (p : α × α) ↦ [[p.1, p.2]]) ⁻¹' s
Tactic: refine ⟨fun s hs => mem_map.2 <| mem_prod_self_iff.2 ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Interval (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
l : Filter α
inst_1 : TendstoIxxClass Icc l l
s : Set (Set α)
hs : s ∈ l.smallSets
⊢ ∃ t ∈ l, t ×ˢ t ⊆ (fun (p : α × α) ↦ [[p.1, p.2]]) ⁻¹' s
have obtain : ∀ (t : Set α) (htl : t ∈ l) (hts : ∀ p ∈ t ×ˢ t, Icc p.1 p.2 ∈ s),
  ∃ t ∈ l, t ×ˢ t ⊆ (fun (p : α × α) ↦ [[p.1, p.2]]) ⁻¹' s
Tactic: obtain ⟨t, htl, hts⟩ : ∃ t ∈ l, ∀ p ∈ (t : Set α) ×ˢ t, Icc (p : α × α).1 p.2 ∈ s :=
    mem_prod_self_iff.1 (mem_map.1 (tendsto_fst.Icc tendsto_snd hs))
-- Lean 4 proof step from Mathlib.Order.Filter.Interval (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
l : Filter α
inst_1 : TendstoIxxClass Icc l l
s : Set (Set α)
hs : s ∈ l.smallSets
t : Set α
htl : t ∈ l
hts : ∀ p ∈ t ×ˢ t, Icc p.1 p.2 ∈ s
⊢ ∃ t ∈ l, t ×ˢ t ⊆ (fun (p : α × α) ↦ [[p.1, p.2]]) ⁻¹' s
have refine : ∀ (p : α × α) (hp : p ∈ t ×ˢ t), Membership.mem (γ := Set (α × α)) ((fun (p : α × α) ↦ [[p.1, p.2]]) ⁻¹' s) p
Tactic: refine ⟨t, htl, fun p hp => ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Interval (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
l : Filter α
inst_1 : TendstoIxxClass Icc l l
s : Set (Set α)
hs : s ∈ l.smallSets
t : Set α
htl : t ∈ l
hts : ∀ p ∈ t ×ˢ t, Icc p.1 p.2 ∈ s
p : α × α
hp : p ∈ t ×ˢ t
⊢ Membership.mem (γ := Set (α × α)) ((fun (p : α × α) ↦ [[p.1, p.2]]) ⁻¹' s) p
have inl : ∀ (h : p.1 ≤ p.2), Membership.mem (γ := Set (α × α)) ((fun (p : α × α) ↦ [[p.1, p.2]]) ⁻¹' s) p
Tactic: rcases le_total p.1 p.2 with h | h
-- Lean 4 proof step from Mathlib.Order.Filter.Interval (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
l : Filter α
inst_1 : TendstoIxxClass Icc l l
s : Set (Set α)
hs : s ∈ l.smallSets
t : Set α
htl : t ∈ l
hts : ∀ p ∈ t ×ˢ t, Icc p.1 p.2 ∈ s
p : α × α
hp : p ∈ t ×ˢ t
inl : ∀ (h : p.1 ≤ p.2), Membership.mem (γ := Set (α × α)) ((fun (p : α × α) ↦ [[p.1, p.2]]) ⁻¹' s) p
⊢ Membership.mem (γ := Set (α × α)) ((fun (p : α × α) ↦ [[p.1, p.2]]) ⁻¹' s) p
have inr : ∀ (h : p.2 ≤ p.1), Membership.mem (γ := Set (α × α)) ((fun (p : α × α) ↦ [[p.1, p.2]]) ⁻¹' s) p
Tactic: rcases le_total p.1 p.2 with h | h
-- Lean 4 proof step from Mathlib.Order.Filter.Interval (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
l : Filter α
inst_1 : TendstoIxxClass Icc l l
s : Set (Set α)
hs : s ∈ l.smallSets
t : Set α
htl : t ∈ l
hts : ∀ p ∈ t ×ˢ t, Icc p.1 p.2 ∈ s
p : α × α
hp : p ∈ t ×ˢ t
h : p.1 ≤ p.2
⊢ Membership.mem (γ := Set (α × α)) ((fun (p : α × α) ↦ [[p.1, p.2]]) ⁻¹' s) p
have inl : Icc p.1 p.2 ∈ s
Tactic: rw [mem_preimage, uIcc_of_le h]
-- Lean 4 proof step from Mathlib.Order.Filter.Interval (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
l : Filter α
inst_1 : TendstoIxxClass Icc l l
s : Set (Set α)
hs : s ∈ l.smallSets
t : Set α
htl : t ∈ l
hts : ∀ p ∈ t ×ˢ t, Icc p.1 p.2 ∈ s
p : α × α
hp : p ∈ t ×ˢ t
h : p.2 ≤ p.1
⊢ Membership.mem (γ := Set (α × α)) ((fun (p : α × α) ↦ [[p.1, p.2]]) ⁻¹' s) p
have inr : Icc p.2 p.1 ∈ s
Tactic: rw [mem_preimage, uIcc_of_ge h]
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
l : Filter α
u v : α → β
hu : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) l u
hv : v ≤ᶠ[l] u
⊢ IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) l v
have apply : ∀ (a : β),
  (∀ᶠ (x : β) in map u l, (fun (x1 x2 : β) ↦ x1 ≤ x2) x a) → ∀ᶠ (x : β) in map v l, (fun (x1 x2 : β) ↦ x1 ≤ x2) x a
Tactic: apply hu.imp
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
f : Filter β
u : β → α
⊢ IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u ↔ ∃ (s : Set β), BddAbove (u '' s) ∧ ∀ᶠ (x : β) in f, x ∈ s
have mp : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u → ∃ (s : Set β), BddAbove (u '' s) ∧ ∀ᶠ (x : β) in f, x ∈ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
f : Filter β
u : β → α
mp : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u → ∃ (s : Set β), BddAbove (u '' s) ∧ ∀ᶠ (x : β) in f, x ∈ s
⊢ IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u ↔ ∃ (s : Set β), BddAbove (u '' s) ∧ ∀ᶠ (x : β) in f, x ∈ s
have mpr : (∃ (s : Set β), BddAbove (u '' s) ∧ ∀ᶠ (x : β) in f, x ∈ s) → IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
inst_1 : NoMaxOrder β
f : α → β
l : Filter α
inst_2 : l.NeBot
hf : Tendsto f l atTop
b : β
hb : ∀ᶠ (x : β) in map f l, (fun (x1 x2 : β) ↦ x1 ≤ x2) x b
⊢ False
have hb₁ : ∀ᶠ (a : α) in l, (fun (x1 x2 : β) ↦ x1 ≤ x2) (f a) b
Tactic: rw [eventually_map] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
inst_1 : NoMaxOrder β
f : α → β
l : Filter α
inst_2 : l.NeBot
hf : Tendsto f l atTop
b : β
hb : ∀ᶠ (a : α) in l, (fun (x1 x2 : β) ↦ x1 ≤ x2) (f a) b
⊢ False
have obtain : ∀ (b' : β) (h : b < b'), False
Tactic: obtain ⟨b', h⟩ := exists_gt b
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
inst_1 : NoMaxOrder β
f : α → β
l : Filter α
inst_2 : l.NeBot
hf : Tendsto f l atTop
b : β
hb : ∀ᶠ (a : α) in l, (fun (x1 x2 : β) ↦ x1 ≤ x2) (f a) b
b' : β
h : b < b'
⊢ False
have hb' : ∀ᶠ (a : α) in l, b' ≤ f a
Tactic: have hb' := (tendsto_atTop.mp hf) b'
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
inst_1 : NoMaxOrder β
f : α → β
l : Filter α
inst_2 : l.NeBot
hf : Tendsto f l atTop
b : β
hb : ∀ᶠ (a : α) in l, (fun (x1 x2 : β) ↦ x1 ≤ x2) (f a) b
b' : β
h : b < b'
hb' : ∀ᶠ (a : α) in l, b' ≤ f a
⊢ False
have this : Eq.{u_1 + 1} (α := Set α) ({x : α | f x ≤ b} ∩ {x : α | b' ≤ f x}) ∅
Tactic: have : { x : α | f x ≤ b } ∩ { x : α | b' ≤ f x } = ∅ :=
    eq_empty_of_subset_empty fun x hx => (not_le_of_gt h) (le_trans hx.2 hx.1)
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
inst_1 : IsDirectedOrder β
f : α → β
hf : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) cofinite f
⊢ BddAbove (range f)
have rcases : ∀ (b : β) (hb : ∀ᶠ (x : β) in map f cofinite, (fun (x1 x2 : β) ↦ x1 ≤ x2) x b), BddAbove (range f)
Tactic: rcases hf with ⟨b, hb⟩
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
inst_1 : IsDirectedOrder β
f : α → β
b : β
hb : ∀ᶠ (x : β) in map f cofinite, (fun (x1 x2 : β) ↦ x1 ≤ x2) x b
⊢ BddAbove (range f)
have this : Nonempty β
Tactic: haveI : Nonempty β := ⟨b⟩
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
inst_1 : IsDirectedOrder β
f : α → β
b : β
hb : ∀ᶠ (x : β) in map f cofinite, (fun (x1 x2 : β) ↦ x1 ≤ x2) x b
this : Nonempty β
⊢ BddAbove (range f)
have rw : BddAbove (f '' {x : α | f x ≤ b}) ∧ BddAbove (f '' {x : α | f x ≤ b}ᶜ)
Tactic: rw [← image_univ, ← union_compl_self { x | f x ≤ b }, image_union, bddAbove_union]
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (hypothesis)
Goal:
β : Type u_2
inst : Preorder β
inst_1 : IsDirectedOrder β
f : ℕ → β
hf : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) atTop f
⊢ BddAbove (range f)
have hf₁ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) cofinite f
Tactic: rw [← Nat.cofinite_eq_atTop] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_1
f : Filter α
inst : LinearOrder α
inst_1 : f.NeBot
cobdd : IsCobounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f
⊢ ∃ (l : α), ∃ᶠ (x : α) in f, l ≤ x
have obtain : ∀ (t : α) (ht : ∀ (a : α), (∀ᶠ (x : α) in f, (fun (x1 x2 : α) ↦ x1 ≤ x2) x a) → (fun (x1 x2 : α) ↦ x1 ≤ x2) t a),
  ∃ (l : α), ∃ᶠ (x : α) in f, l ≤ x
Tactic: obtain ⟨t, ht⟩ := cobdd
Cleared hypotheses: cobdd
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_1
f : Filter α
inst : LinearOrder α
inst_1 : f.NeBot
t : α
ht : ∀ (a : α), (∀ᶠ (x : α) in f, (fun (x1 x2 : α) ↦ x1 ≤ x2) x a) → (fun (x1 x2 : α) ↦ x1 ≤ x2) t a
⊢ ∃ (l : α), ∃ᶠ (x : α) in f, l ≤ x
have inl : ∀ (tbot : IsBot t), ∃ (l : α), ∃ᶠ (x : α) in f, l ≤ x
Tactic: rcases isBot_or_exists_lt t with tbot | ⟨t', ht'⟩
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_1
f : Filter α
inst : LinearOrder α
inst_1 : f.NeBot
t : α
ht : ∀ (a : α), (∀ᶠ (x : α) in f, (fun (x1 x2 : α) ↦ x1 ≤ x2) x a) → (fun (x1 x2 : α) ↦ x1 ≤ x2) t a
inl : ∀ (tbot : IsBot t), ∃ (l : α), ∃ᶠ (x : α) in f, l ≤ x
⊢ ∃ (l : α), ∃ᶠ (x : α) in f, l ≤ x
have inr : ∀ (t' : α) (ht' : t' < t), ∃ (l : α), ∃ᶠ (x : α) in f, l ≤ x
Tactic: rcases isBot_or_exists_lt t with tbot | ⟨t', ht'⟩
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_1
f : Filter α
inst : LinearOrder α
inst_1 : f.NeBot
t : α
ht : ∀ (a : α), (∀ᶠ (x : α) in f, (fun (x1 x2 : α) ↦ x1 ≤ x2) x a) → (fun (x1 x2 : α) ↦ x1 ≤ x2) t a
t' : α
ht' : t' < t
⊢ ∃ (l : α), ∃ᶠ (x : α) in f, l ≤ x
have inr : ∀ (ev : ∀ᶠ (x : α) in f, ¬(fun (x : α) ↦ t' ≤ x) x), False
Tactic: refine ⟨t', fun ev ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_1
f : Filter α
inst : LinearOrder α
inst_1 : f.NeBot
t : α
ht : ∀ (a : α), (∀ᶠ (x : α) in f, (fun (x1 x2 : α) ↦ x1 ≤ x2) x a) → (fun (x1 x2 : α) ↦ x1 ≤ x2) t a
t' : α
ht' : t' < t
ev : ∀ᶠ (x : α) in f, ¬(fun (x : α) ↦ t' ≤ x) x
⊢ ∀ᶠ (x : α) in f, (fun (x1 x2 : α) ↦ x1 ≤ x2) x t'
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ ¬(fun (x : α) ↦ t' ≤ x) x) x} x →
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ ((fun (x1 x2 : α) ↦ x1 ≤ x2) x t' : Prop)) x} x}
    a
Tactic: filter_upwards [ev] with _ h using (not_le.mp h).le
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_1
f : Filter α
inst : LinearOrder α
inst_1 : f.NeBot
t : α
ht : ∀ (a : α), (∀ᶠ (x : α) in f, (fun (x1 x2 : α) ↦ x1 ≤ x2) x a) → (fun (x1 x2 : α) ↦ x1 ≤ x2) t a
t' : α
ht' : t' < t
ev : ∀ᶠ (x : α) in f, ¬(fun (x : α) ↦ t' ≤ x) x
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ ¬(fun (x : α) ↦ t' ≤ x) x) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ ((fun (x1 x2 : α) ↦ x1 ≤ x2) x t' : Prop)) x} x}
      a
⊢ ∀ᶠ (x : α) in f, (fun (x1 x2 : α) ↦ x1 ≤ x2) x t'
have h₁ : ∀ (a : α), ¬t' ≤ a → a ≤ t'
Tactic: filter_upwards [ev] with _ h using (not_le.mp h).le
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (hypothesis)
Goal:
α : Type u_1
f : Filter α
inst : LinearOrder α
inst_1 : f.NeBot
t : α
ht : ∀ (a : α), (∀ᶠ (x : α) in f, (fun (x1 x2 : α) ↦ x1 ≤ x2) x a) → (fun (x1 x2 : α) ↦ x1 ≤ x2) t a
t' : α
ht' : t' < t
ev : ∀ᶠ (x : α) in f, ¬(fun (x : α) ↦ t' ≤ x) x
⊢ False
have ht₁ : t ≤ t'
Tactic: specialize ht t' (by filter_upwards [ev] with _ h using (not_le.mp h).le)
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_1
f : Filter α
inst : LinearOrder α
l : α
freq_ge : ∃ᶠ (x : α) in f, l ≤ x
⊢ IsCobounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f
have inl : ∀ (lbot : IsBot l), IsCobounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f
Tactic: rcases isBot_or_exists_lt l with lbot | ⟨l', hl'⟩
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_1
f : Filter α
inst : LinearOrder α
l : α
freq_ge : ∃ᶠ (x : α) in f, l ≤ x
inl : ∀ (lbot : IsBot l), IsCobounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f
⊢ IsCobounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f
have inr : ∀ (l' : α) (hl' : l' < l), IsCobounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f
Tactic: rcases isBot_or_exists_lt l with lbot | ⟨l', hl'⟩
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_1
f : Filter α
inst : LinearOrder α
l : α
freq_ge : ∃ᶠ (x : α) in f, l ≤ x
l' : α
hl' : l' < l
⊢ IsCobounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f
have inr : ∀ (u : α) (hu : ∀ᶠ (x : α) in f, (fun (x1 x2 : α) ↦ x1 ≤ x2) x u), (fun (x1 x2 : α) ↦ x1 ≤ x2) l' u
Tactic: refine ⟨l', fun u hu ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_1
f : Filter α
inst : LinearOrder α
l : α
freq_ge : ∃ᶠ (x : α) in f, l ≤ x
l' : α
hl' : l' < l
u : α
hu : ∀ᶠ (x : α) in f, (fun (x1 x2 : α) ↦ x1 ≤ x2) x u
⊢ (fun (x1 x2 : α) ↦ x1 ≤ x2) l' u
have inr : ∀ (w : α) (l_le_w : l ≤ w) (w_le_u : w ≤ u), l' ≤ u
Tactic: obtain ⟨w, l_le_w, w_le_u⟩ := (freq_ge.and_eventually hu).exists
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_5
f : Filter α
R : Type u_6
κ : Type u_7
inst : AddCommMonoid R
r : R → R → Prop
hr : ∀ (v₁ v₂ : α → R), IsBoundedUnder r f v₁ → IsBoundedUnder r f v₂ → IsBoundedUnder r f (v₁ + v₂)
hr₀ : r 0 0
u : κ → α → R
s : Finset κ
h : ∀ k ∈ s, IsBoundedUnder r f (u k)
⊢ IsBoundedUnder r f (∑ k ∈ s, u k)
have induction : ∀ (h : ∀ (k : κ), Membership.mem (γ := Finset κ) ∅ k → IsBoundedUnder r f (u k)), IsBoundedUnder r f (∑ k ∈ ∅, u k)
Tactic: induction s using Finset.cons_induction
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_5
f : Filter α
R : Type u_6
κ : Type u_7
inst : AddCommMonoid R
r : R → R → Prop
hr : ∀ (v₁ v₂ : α → R), IsBoundedUnder r f v₁ → IsBoundedUnder r f v₂ → IsBoundedUnder r f (v₁ + v₂)
hr₀ : r 0 0
u : κ → α → R
s : Finset κ
h : ∀ k ∈ s, IsBoundedUnder r f (u k)
induction :
  ∀ (h : ∀ (k : κ), Membership.mem (γ := Finset κ) ∅ k → IsBoundedUnder r f (u k)), IsBoundedUnder r f (∑ k ∈ ∅, u k)
⊢ IsBoundedUnder r f (∑ k ∈ s, u k)
have cons : ∀ (a : κ) (s : Finset κ) (h : a ∉ s),
  (∀ (h : ∀ k ∈ s, IsBoundedUnder r f (u k)), IsBoundedUnder r f (∑ k ∈ s, u k)) →
    ∀ (h_1 : ∀ k ∈ Finset.cons a s h, IsBoundedUnder r f (u k)), IsBoundedUnder r f (∑ k ∈ Finset.cons a s h, u k)
Tactic: induction s using Finset.cons_induction
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (hypothesis)
Goal:
α : Type u_5
f : Filter α
R : Type u_6
κ : Type u_7
inst : AddCommMonoid R
r : R → R → Prop
hr : ∀ (v₁ v₂ : α → R), IsBoundedUnder r f v₁ → IsBoundedUnder r f v₂ → IsBoundedUnder r f (v₁ + v₂)
hr₀ : r 0 0
u : κ → α → R
k₀ : κ
s : Finset κ
k₀_notin_s : k₀ ∉ s
ih : ∀ (h : ∀ k ∈ s, IsBoundedUnder r f (u k)), IsBoundedUnder r f (∑ k ∈ s, u k)
h : ∀ k ∈ Finset.cons k₀ s k₀_notin_s, IsBoundedUnder r f (u k)
⊢ IsBoundedUnder r f (∑ k ∈ Finset.cons k₀ s k₀_notin_s, u k)
have h₁ : IsBoundedUnder r f (u k₀) ∧ ∀ x ∈ s, IsBoundedUnder r f (u x)
Tactic: simp only [Finset.forall_mem_cons] at *
Cleared hypotheses: h