awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Map (goal)
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : Preorder α
inst_1 : Preorder β
l : Filter γ
f : γ → α
e : α ≃o β
rw :
  Tendsto.{u_5, u_4} (β := β) (fun (x : γ) ↦ (e : (a : α) → β) (f x)) l atTop ↔
    Tendsto f l (comap.{u_3, u_4} (β := β) (⇑e : (a : α) → β) atTop)
⊢ Tendsto.{u_5, u_4} (β := β) (fun (x : γ) ↦ (e : (a : α) → β) (f x)) l atTop ↔ Tendsto f l atTop
have rw₁ : Tendsto.{u_5, u_4} (β := β) (fun (x : γ) ↦ (e : (a : α) → β) (f x)) l atTop ↔
  Tendsto.{u_5, u_4} (β := β) ((⇑e : (a : α) → β) ∘ f) l atTop
Tactic: rw [← e.comap_atTop, tendsto_comap_iff, Function.comp_def]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Map (goal)
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : Preorder α
inst_1 : Preorder β
l : Filter γ
f : γ → α
e : α ≃o β
rw :
  Tendsto.{u_5, u_4} (β := β) (fun (x : γ) ↦ (e : (a : α) → β) (f x)) l atTop ↔
    Tendsto f l (comap.{u_3, u_4} (β := β) (⇑e : (a : α) → β) atTop)
rw₁ :
  Tendsto.{u_5, u_4} (β := β) (fun (x : γ) ↦ (e : (a : α) → β) (f x)) l atTop ↔
    Tendsto.{u_5, u_4} (β := β) ((⇑e : (a : α) → β) ∘ f) l atTop
⊢ Tendsto.{u_5, u_4} (β := β) (fun (x : γ) ↦ (e : (a : α) → β) (f x)) l atTop ↔ Tendsto f l atTop
have rw₂ : Tendsto.{u_5, u_4} (β := β) (fun (x : γ) ↦ (e : (a : α) → β) (f x)) l atTop ↔
  Tendsto.{u_5, u_4} (β := β) (fun (x : γ) ↦ (e : (a : α) → β) (f x)) l atTop
Tactic: rw [← e.comap_atTop, tendsto_comap_iff, Function.comp_def]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Monoid (goal)
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedMonoid M
l : Filter α
f : α → M
hf : Tendsto f l atTop
n : ℕ
hn : 0 < n
⊢ Tendsto.{u_1, u_2} (β := M) (fun (x : α) ↦ f x ^ n) l atTop
have refine : ∀ (x : α) (hx : 1 ≤ f x), f x ≤ (fun (x : α) ↦ f x ^ n) x
Tactic: refine tendsto_atTop_mono' _ ((hf.eventually_ge_atTop 1).mono fun x hx ↦ ?_) hf
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Monoid (goal)
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedCancelMonoid M
l : Filter α
f g : α → M
hf : IsBoundedUnder (fun (x1 x2 : M) ↦ x1 ≤ x2) l f
hfg : Tendsto.{u_1, u_2} (β := M) (fun (x : α) ↦ f x * g x) l atTop
⊢ Tendsto g l atTop
have obtain : ∀ (C : M) (hC : ∀ᶠ (x : M) in map f l, (fun (x1 x2 : M) ↦ x1 ≤ x2) x C), Tendsto g l atTop
Tactic: obtain ⟨C, hC⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Monoid (goal)
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedCancelMonoid M
l : Filter α
f g : α → M
hfg : Tendsto.{u_1, u_2} (β := M) (fun (x : α) ↦ f x * g x) l atTop
C : M
hC : ∀ᶠ (x : M) in map f l, (fun (x1 x2 : M) ↦ x1 ≤ x2) x C
⊢ Tendsto g l atTop
have refine : EventuallyLE.{u_1, u_2} (β := M) l (fun (x : α) ↦ f x * g x) fun (x : α) ↦ C * g x
Tactic: refine .atTop_of_const_mul C <| tendsto_atTop_mono' l ?_ hfg
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Monoid (goal)
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedCancelMonoid M
l : Filter α
f g : α → M
hg : IsBoundedUnder (fun (x1 x2 : M) ↦ x1 ≤ x2) l g
h : Tendsto.{u_1, u_2} (β := M) (fun (x : α) ↦ f x * g x) l atTop
⊢ Tendsto f l atTop
have obtain : ∀ (C : M) (hC : ∀ᶠ (x : M) in map g l, (fun (x1 x2 : M) ↦ x1 ≤ x2) x C), Tendsto f l atTop
Tactic: obtain ⟨C, hC⟩ := hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Monoid (goal)
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedCancelMonoid M
l : Filter α
f g : α → M
h : Tendsto.{u_1, u_2} (β := M) (fun (x : α) ↦ f x * g x) l atTop
C : M
hC : ∀ᶠ (x : M) in map g l, (fun (x1 x2 : M) ↦ x1 ≤ x2) x C
⊢ Tendsto f l atTop
have refine : EventuallyLE.{u_1, u_2} (β := M) l (fun (x : α) ↦ f x * g x) fun (x : α) ↦ f x * C
Tactic: refine .atTop_of_mul_const C <| tendsto_atTop_mono' l ?_ h
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Prod (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
⊢ SProd.sprod (α := Filter α) (β := Filter β) atTop atTop = atTop
have inl : IsEmpty α → SProd.sprod (α := Filter α) (β := Filter β) atTop atTop = atTop
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Prod (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
inl : IsEmpty α → SProd.sprod (α := Filter α) (β := Filter β) atTop atTop = atTop
⊢ SProd.sprod (α := Filter α) (β := Filter β) atTop atTop = atTop
have inr : Nonempty α → SProd.sprod (α := Filter α) (β := Filter β) atTop atTop = atTop
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Prod (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
h : Nonempty α
⊢ SProd.sprod (α := Filter α) (β := Filter β) atTop atTop = atTop
have inr : IsEmpty β → SProd.sprod (α := Filter α) (β := Filter β) atTop atTop = atTop
Tactic: cases isEmpty_or_nonempty β
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Prod (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
h : Nonempty α
inr : IsEmpty β → SProd.sprod (α := Filter α) (β := Filter β) atTop atTop = atTop
⊢ SProd.sprod (α := Filter α) (β := Filter β) atTop atTop = atTop
have inr₁ : Nonempty β → SProd.sprod (α := Filter α) (β := Filter β) atTop atTop = atTop
Tactic: cases isEmpty_or_nonempty β
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Prod (goal)
Goal:
ι : Type u_1
ι' : Type u_2
⊢ Tendsto (β := Finset (ι × ι')) (fun (p : Prod.{u_1, u_2} (Finset ι) (Finset ι')) ↦ p.1 ×ˢ p.2) atTop atTop
have hf : Monotone (β := Finset (ι × ι')) fun (p : Prod.{u_1, u_2} (Finset ι) (Finset ι')) ↦ p.1 ×ˢ p.2
Tactic: apply Monotone.tendsto_atTop_atTop
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Prod (goal)
Goal:
ι : Type u_1
ι' : Type u_2
hf : Monotone (β := Finset (ι × ι')) fun (p : Prod.{u_1, u_2} (Finset ι) (Finset ι')) ↦ p.1 ×ˢ p.2
⊢ Tendsto (β := Finset (ι × ι')) (fun (p : Prod.{u_1, u_2} (Finset ι) (Finset ι')) ↦ p.1 ×ˢ p.2) atTop atTop
have h : ∀ (b : Finset (ι × ι')), ∃ (a : Prod.{u_1, u_2} (Finset ι) (Finset ι')), b ≤ a.1 ×ˢ a.2
Tactic: apply Monotone.tendsto_atTop_atTop
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Prod (goal)
Goal:
ι : Type u_1
ι' : Type u_2
b : Finset (ι × ι')
⊢ ∃ (a : Prod.{u_1, u_2} (Finset ι) (Finset ι')), b ≤ a.1 ×ˢ a.2
have h : b ≤ (Finset.image Prod.fst b, Finset.image Prod.snd b).1 ×ˢ (Finset.image Prod.fst b, Finset.image Prod.snd b).2
Tactic: use (Finset.image Prod.fst b, Finset.image Prod.snd b)
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Prod (goal)
Goal:
ι : Type u_1
ι' : Type u_2
⊢ Tendsto (β := Finset (ι × ι')) (fun (p : Prod.{u_1, u_2} (Finset ι) (Finset ι')) ↦ p.1 ×ˢ p.2) atTop atTop
have hf : Monotone (β := Finset (ι × ι')) fun (p : Prod.{u_1, u_2} (Finset ι) (Finset ι')) ↦ p.1 ×ˢ p.2
Tactic: classical
  apply Monotone.tendsto_atTop_atTop
  · intro p q hpq
    simpa using Finset.product_subset_product hpq.1 hpq.2
  · intro b
    use (Finset.image Prod.fst b, Finset.image Prod.snd b)
    exact Finset.subset_product
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Prod (goal)
Goal:
ι : Type u_1
ι' : Type u_2
hf : Monotone (β := Finset (ι × ι')) fun (p : Prod.{u_1, u_2} (Finset ι) (Finset ι')) ↦ p.1 ×ˢ p.2
⊢ Tendsto (β := Finset (ι × ι')) (fun (p : Prod.{u_1, u_2} (Finset ι) (Finset ι')) ↦ p.1 ×ˢ p.2) atTop atTop
have h : ∀ (b : Finset (ι × ι')), ∃ (a : Prod.{u_1, u_2} (Finset ι) (Finset ι')), b ≤ a.1 ×ˢ a.2
Tactic: classical
  apply Monotone.tendsto_atTop_atTop
  · intro p q hpq
    simpa using Finset.product_subset_product hpq.1 hpq.2
  · intro b
    use (Finset.image Prod.fst b, Finset.image Prod.snd b)
    exact Finset.subset_product
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Prod (goal)
Goal:
α₁ : Type u_6
α₂ : Type u_7
β₁ : Type u_8
β₂ : Type u_9
inst : Preorder β₁
inst_1 : Preorder β₂
u₁ : β₁ → α₁
u₂ : β₂ → α₂
⊢ map u₁ atTop ×ˢ map u₂ atTop = map (Prod.map u₁ u₂) atTop
have rw : map (fun (p : β₁ × β₂) ↦ (u₁ p.1, u₂ p.2)) (SProd.sprod (α := Filter β₁) (β := Filter β₂) atTop atTop) =
  map (Prod.map u₁ u₂) atTop
Tactic: rw [prod_map_map_eq, prod_atTop_atTop_eq, Prod.map_def]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Prod (goal)
Goal:
α₁ : Type u_6
α₂ : Type u_7
β₁ : Type u_8
β₂ : Type u_9
inst : Preorder β₁
inst_1 : Preorder β₂
u₁ : β₁ → α₁
u₂ : β₂ → α₂
rw :
  map (fun (p : β₁ × β₂) ↦ (u₁ p.1, u₂ p.2)) (SProd.sprod (α := Filter β₁) (β := Filter β₂) atTop atTop) =
    map (Prod.map u₁ u₂) atTop
⊢ map u₁ atTop ×ˢ map u₂ atTop = map (Prod.map u₁ u₂) atTop
have rw₁ : map (fun (p : β₁ × β₂) ↦ (u₁ p.1, u₂ p.2)) atTop = map (Prod.map u₁ u₂) atTop
Tactic: rw [prod_map_map_eq, prod_atTop_atTop_eq, Prod.map_def]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Prod (goal)
Goal:
α₁ : Type u_6
α₂ : Type u_7
β₁ : Type u_8
β₂ : Type u_9
inst : Preorder β₁
inst_1 : Preorder β₂
u₁ : β₁ → α₁
u₂ : β₂ → α₂
rw :
  map (fun (p : β₁ × β₂) ↦ (u₁ p.1, u₂ p.2)) (SProd.sprod (α := Filter β₁) (β := Filter β₂) atTop atTop) =
    map (Prod.map u₁ u₂) atTop
rw₁ : map (fun (p : β₁ × β₂) ↦ (u₁ p.1, u₂ p.2)) atTop = map (Prod.map u₁ u₂) atTop
⊢ map u₁ atTop ×ˢ map u₂ atTop = map (Prod.map u₁ u₂) atTop
have rw₂ : Eq (α := Filter (α₁ × α₂)) (map (fun (p : β₁ × β₂) ↦ (u₁ p.1, u₂ p.2)) atTop)
  (map (fun (p : β₁ × β₂) ↦ (u₁ p.1, u₂ p.2)) atTop)
Tactic: rw [prod_map_map_eq, prod_atTop_atTop_eq, Prod.map_def]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Prod (goal)
Goal:
α : Type u_3
inst : Preorder α
⊢ Tendsto (β := α × α) (fun (a : α) ↦ (a, a)) atBot atBot
have rw : Tendsto (fun (a : α) ↦ (a, a)) atBot (SProd.sprod (α := Filter α) (β := Filter α) atBot atBot)
Tactic: rw [← prod_atBot_atBot_eq]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Prod (goal)
Goal:
α : Type u_3
inst : Preorder α
⊢ Tendsto (β := α × α) (fun (a : α) ↦ (a, a)) atTop atTop
have rw : Tendsto (fun (a : α) ↦ (a, a)) atTop (SProd.sprod (α := Filter α) (β := Filter α) atTop atTop)
Tactic: rw [← prod_atTop_atTop_eq]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Prod (goal)
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : Preorder γ
F : Filter α
G : Filter β
f : α → γ
g : β → γ
hf : Tendsto f F atBot
hg : Tendsto g G atBot
⊢ Tendsto (Prod.map f g) (F ×ˢ G) atBot
have rw : Tendsto (Prod.map f g) (F ×ˢ G) (SProd.sprod (α := Filter γ) (β := Filter γ) atBot atBot)
Tactic: rw [← prod_atBot_atBot_eq]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Prod (goal)
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : Preorder γ
F : Filter α
G : Filter β
f : α → γ
g : β → γ
hf : Tendsto f F atTop
hg : Tendsto g G atTop
⊢ Tendsto (Prod.map f g) (F ×ˢ G) atTop
have rw : Tendsto (Prod.map f g) (F ×ˢ G) (SProd.sprod (α := Filter γ) (β := Filter γ) atTop atTop)
Tactic: rw [← prod_atTop_atTop_eq]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Prod (goal)
Goal:
α : Type u_3
γ : Type u_5
inst : Preorder α
inst_1 : Preorder γ
f g : α → γ
hf : Tendsto f atBot atBot
hg : Tendsto g atBot atBot
⊢ Tendsto (Prod.map f g) atBot atBot
have rw : Tendsto (Prod.map f g) (SProd.sprod (α := Filter α) (β := Filter α) atBot atBot) atBot
Tactic: rw [← prod_atBot_atBot_eq]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Prod (goal)
Goal:
α : Type u_3
γ : Type u_5
inst : Preorder α
inst_1 : Preorder γ
f g : α → γ
hf : Tendsto f atTop atTop
hg : Tendsto g atTop atTop
⊢ Tendsto (Prod.map f g) atTop atTop
have rw : Tendsto (Prod.map f g) (SProd.sprod (α := Filter α) (β := Filter α) atTop atTop) atTop
Tactic: rw [← prod_atTop_atTop_eq]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Prod (hypothesis)
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
p : α × β → Prop
hp : ∀ᶠ (x : α × β) in atTop, p x
⊢ ∀ᶠ (k : α) in atTop, ∀ᶠ (l : β) in atTop, p (k, l)
have hp₁ : ∀ᶠ (x : α × β) in SProd.sprod (α := Filter α) (β := Filter β) atTop atTop, p x
Tactic: rw [← prod_atTop_atTop_eq] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Ring (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
l : Filter β
f g : β → α
hf : Tendsto f l atTop
hg : Tendsto g l atTop
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ f x * g x) l atTop
have refine : g ≤ᶠ[l] fun (x : β) ↦ f x * g x
Tactic: refine tendsto_atTop_mono' _ ?_ hg
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Ring (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
l : Filter β
f g : β → α
hf : Tendsto f l atTop
hg : Tendsto g l atTop
⊢ g ≤ᶠ[l] fun (x : β) ↦ f x * g x
have h : ∀ (a : β),
  Membership.mem (γ := Set β)
    {x : β |
      Membership.mem (γ := Set β) {x : β | (fun (x : β) ↦ 0 ≤ g x) x} x →
        Membership.mem (γ := Set β)
          {x : β |
            Membership.mem (γ := Set β) {x : β | (fun (x : β) ↦ 1 ≤ f x) x} x →
              Membership.mem (γ := Set β) {x : β | (fun (x : β) ↦ g x ≤ (fun (x : β) ↦ f x * g x) x) x} x}
          x}
    a
Tactic: filter_upwards [hg.eventually (eventually_ge_atTop 0),
    hf.eventually (eventually_ge_atTop 1)] with _ using le_mul_of_one_le_left
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Ring (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
l : Filter β
f g : β → α
hf : Tendsto f l atTop
hg : Tendsto g l atTop
h :
  ∀ (a : β),
    Membership.mem (γ := Set β)
      {x : β |
        Membership.mem (γ := Set β) {x : β | (fun (x : β) ↦ 0 ≤ g x) x} x →
          Membership.mem (γ := Set β)
            {x : β |
              Membership.mem (γ := Set β) {x : β | (fun (x : β) ↦ 1 ≤ f x) x} x →
                Membership.mem (γ := Set β) {x : β | (fun (x : β) ↦ g x ≤ (fun (x : β) ↦ f x * g x) x) x} x}
            x}
      a
⊢ g ≤ᶠ[l] fun (x : β) ↦ f x * g x
have h₁ : ∀ (a : β), 0 ≤ g a → 1 ≤ f a → g a ≤ f a * g a
Tactic: filter_upwards [hg.eventually (eventually_ge_atTop 0),
    hf.eventually (eventually_ge_atTop 1)] with _ using le_mul_of_one_le_left
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Ring (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
l : Filter β
f g : β → α
hf : Tendsto f l atTop
hg : Tendsto g l atBot
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ f x * g x) l atBot
have this : Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ f x * (Neg.neg ∘ g) x) l atTop
Tactic: have := hf.atTop_mul_atTop₀ <| tendsto_neg_atBot_atTop.comp hg
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Ring (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
l : Filter β
f g : β → α
hf : Tendsto f l atBot
hg : Tendsto g l atTop
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ f x * g x) l atBot
have this : Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ -f x * g x) l atTop
Tactic: have : Tendsto (fun x => -f x * g x) l atTop :=
    (tendsto_neg_atBot_atTop.comp hf).atTop_mul_atTop₀ hg
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Ring (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
l : Filter β
f g : β → α
hf : Tendsto f l atBot
hg : Tendsto g l atBot
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ f x * g x) l atTop
have this : Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ -f x * -g x) l atTop
Tactic: have : Tendsto (fun x => -f x * -g x) l atTop :=
    (tendsto_neg_atBot_atTop.comp hf).atTop_mul_atTop₀ (tendsto_neg_atBot_atTop.comp hg)
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Tendsto (goal)
Goal:
α : Type u_6
inst : PartialOrder α
inst_1 : OrderTop α
⊢ Eq.{u_6 + 1} (α := Filter α) atTop (pure ⊤)
have rw : Eq.{u_6 + 1} (α := Filter α) (𝓟 (Ici ⊤)) (pure ⊤)
Tactic: rw [isTop_top.atTop_eq, Ici_top, principal_singleton]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Tendsto (goal)
Goal:
α : Type u_6
inst : PartialOrder α
inst_1 : OrderTop α
rw : Eq.{u_6 + 1} (α := Filter α) (𝓟 (Ici ⊤)) (pure ⊤)
⊢ Eq.{u_6 + 1} (α := Filter α) atTop (pure ⊤)
have rw₁ : Eq (α := Filter α) (𝓟 {⊤}) (pure ⊤)
Tactic: rw [isTop_top.atTop_eq, Ici_top, principal_singleton]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Tendsto (goal)
Goal:
α : Type u_6
inst : PartialOrder α
inst_1 : OrderTop α
rw : Eq.{u_6 + 1} (α := Filter α) (𝓟 (Ici ⊤)) (pure ⊤)
rw₁ : Eq (α := Filter α) (𝓟 {⊤}) (pure ⊤)
⊢ Eq.{u_6 + 1} (α := Filter α) atTop (pure ⊤)
have rw₂ : Eq.{u_6 + 1} (α := Filter α) (pure ⊤) (pure ⊤)
Tactic: rw [isTop_top.atTop_eq, Ici_top, principal_singleton]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Tendsto (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Preorder β
l : Filter α
f₁ f₂ : α → β
h : f₁ ≤ᶠ[l] f₂
h₁ : Tendsto f₁ l atTop
b : β
⊢ ∀ᶠ (a : α) in l, b ≤ f₂ a
have h₂ : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ b ≤ f₁ a) x} x →
        Membership.mem (γ := Set α)
          {x : α |
            Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f₁ x ≤ f₂ x) x} x →
              Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ b ≤ f₂ a) x} x}
          x}
    a
Tactic: filter_upwards [tendsto_atTop.1 h₁ b, h] with x using le_trans
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Tendsto (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Preorder β
l : Filter α
f₁ f₂ : α → β
h : f₁ ≤ᶠ[l] f₂
h₁ : Tendsto f₁ l atTop
b : β
h₂ :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ b ≤ f₁ a) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f₁ x ≤ f₂ x) x} x →
                Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ b ≤ f₂ a) x} x}
            x}
      a
⊢ ∀ᶠ (a : α) in l, b ≤ f₂ a
have h₃ : ∀ (a : α), b ≤ f₁ a → f₁ a ≤ f₂ a → b ≤ f₂ a
Tactic: filter_upwards [tendsto_atTop.1 h₁ b, h] with x using le_trans
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Tendsto (goal)
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : Preorder β
inst_1 : Preorder γ
l : Filter α
inst_2 : l.NeBot
f : β → γ
hf : Monotone f
g : α → β
hg : Tendsto g l atTop
⊢ upperBounds (range (f ∘ g)) = upperBounds (range f)
have refine : upperBounds (range (f ∘ g)) ⊆ upperBounds (range f)
Tactic: refine Subset.antisymm ?_ (upperBounds_mono_set <| range_comp_subset_range _ _)
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Tendsto (goal)
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : Preorder β
inst_1 : Preorder γ
l : Filter α
inst_2 : l.NeBot
f : β → γ
hf : Monotone f
g : α → β
hg : Tendsto g l atTop
c : γ
hc : c ∈ upperBounds (range (f ∘ g))
b : β
⊢ f b ≤ c
have obtain : ∀ (a : α) (ha : b ≤ g a), f b ≤ c
Tactic: obtain ⟨a, ha⟩ : ∃ a, b ≤ g a := (hg.eventually_ge_atTop b).exists
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Tendsto (goal)
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : Preorder β
inst_1 : Preorder γ
f : α → β
e : β → γ
l : Filter α
hm : ∀ (b₁ b₂ : β), e b₁ ≤ e b₂ ↔ b₁ ≤ b₂
hu : ∀ (c : γ), ∃ (b : β), c ≤ e b
⊢ Tendsto (e ∘ f) l atTop ↔ Tendsto f l atTop
have rw : Tendsto (e ∘ f) l atTop ↔ Tendsto f l (comap e atTop)
Tactic: rw [← comap_embedding_atTop hm hu, tendsto_comap_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Tendsto (goal)
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : Preorder β
inst_1 : Preorder γ
f : α → β
e : β → γ
l : Filter α
hm : ∀ (b₁ b₂ : β), e b₁ ≤ e b₂ ↔ b₁ ≤ b₂
hu : ∀ (c : γ), ∃ (b : β), c ≤ e b
rw : Tendsto (e ∘ f) l atTop ↔ Tendsto f l (comap e atTop)
⊢ Tendsto (e ∘ f) l atTop ↔ Tendsto f l atTop
have rw₁ : Tendsto (e ∘ f) l atTop ↔ Tendsto (e ∘ f) l atTop
Tactic: rw [← comap_embedding_atTop hm hu, tendsto_comap_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Tendsto (goal)
Goal:
ι : Type u_1
α : Type u_3
inst : Preorder ι
inst_1 : LinearOrder α
u : ι → α
h : Monotone u
H : ¬BddAbove (range u)
⊢ Tendsto u atTop atTop
have apply : ∀ (b : α), ∃ (a : ι), b ≤ u a
Tactic: apply h.tendsto_atTop_atTop
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Tendsto (goal)
Goal:
ι : Type u_1
α : Type u_3
inst : Preorder ι
inst_1 : LinearOrder α
u : ι → α
h : Monotone u
H : ¬BddAbove (range u)
b : α
⊢ ∃ (a : ι), b ≤ u a
have rcases : ∀ (N : ι) (hN : b < u N), ∃ (a : ι), b ≤ u a
Tactic: rcases not_bddAbove_iff.1 H b with ⟨_, ⟨N, rfl⟩, hN⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
p : ι → Prop
s : ι → Set α
h : IsBasis p s
i : ι
hi : p i
j : ι
hj : p j
⊢ ∃ (z : Set α), Membership.mem (γ := Set (Set α)) {t : Set α | ∃ (i : ι), p i ∧ s i = t} z ∧ z ⊆ s i ∩ s j
have rcases : ∀ (k : ι) (hk : p k) (hk' : s k ⊆ s i ∩ s j),
  ∃ (z : Set α), Membership.mem (γ := Set (Set α)) {t : Set α | ∃ (i : ι), p i ∧ s i = t} z ∧ z ⊆ s i ∩ s j
Tactic: rcases h.inter hi hj with ⟨k, hk, hk'⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
B : FilterBasis α
U : Set α
U_in : U ∈ B.sets
V : Set α
V_in : V ∈ B.sets
⊢ ∃ (z : (↑B.sets : Type u_1)),
    (fun (x1 x2 : Filter α) ↦ x1 ≥ x2)
        ((fun (s : (↑B.sets : Type u_1)) ↦ 𝓟 (↑s : Set α)) (Subtype.mk (p := fun (x : Set α) ↦ x ∈ B.sets) U U_in))
        ((fun (s : (↑B.sets : Type u_1)) ↦ 𝓟 (↑s : Set α)) z) ∧
      (fun (x1 x2 : Filter α) ↦ x1 ≥ x2)
        ((fun (s : (↑B.sets : Type u_1)) ↦ 𝓟 (↑s : Set α)) (Subtype.mk (p := fun (x : Set α) ↦ x ∈ B.sets) V V_in))
        ((fun (s : (↑B.sets : Type u_1)) ↦ 𝓟 (↑s : Set α)) z)
have rcases : ∀ (W : Set α) (W_in : W ∈ B.sets) (W_sub : W ⊆ U ∩ V),
  ∃ (z : (↑B.sets : Type u_1)),
    (fun (x1 x2 : Filter α) ↦ x1 ≥ x2)
        ((fun (s : (↑B.sets : Type u_1)) ↦ 𝓟 (↑s : Set α)) (Subtype.mk (p := fun (x : Set α) ↦ x ∈ B.sets) U U_in))
        ((fun (s : (↑B.sets : Type u_1)) ↦ 𝓟 (↑s : Set α)) z) ∧
      (fun (x1 x2 : Filter α) ↦ x1 ≥ x2)
        ((fun (s : (↑B.sets : Type u_1)) ↦ 𝓟 (↑s : Set α)) (Subtype.mk (p := fun (x : Set α) ↦ x ∈ B.sets) V V_in))
        ((fun (s : (↑B.sets : Type u_1)) ↦ 𝓟 (↑s : Set α)) z)
Tactic: rcases B.inter_sets U_in V_in with ⟨W, W_in, W_sub⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
B : FilterBasis α
U : Set α
U_in : U ∈ B.sets
V : Set α
V_in : V ∈ B.sets
W : Set α
W_in : W ∈ B.sets
W_sub : W ⊆ U ∩ V
⊢ ∃ (z : (↑B.sets : Type u_1)),
    (fun (x1 x2 : Filter α) ↦ x1 ≥ x2)
        ((fun (s : (↑B.sets : Type u_1)) ↦ 𝓟 (↑s : Set α)) (Subtype.mk (p := fun (x : Set α) ↦ x ∈ B.sets) U U_in))
        ((fun (s : (↑B.sets : Type u_1)) ↦ 𝓟 (↑s : Set α)) z) ∧
      (fun (x1 x2 : Filter α) ↦ x1 ≥ x2)
        ((fun (s : (↑B.sets : Type u_1)) ↦ 𝓟 (↑s : Set α)) (Subtype.mk (p := fun (x : Set α) ↦ x ∈ B.sets) V V_in))
        ((fun (s : (↑B.sets : Type u_1)) ↦ 𝓟 (↑s : Set α)) z)
have h : (fun (x1 x2 : Filter α) ↦ x1 ≥ x2)
    ((fun (s : (↑B.sets : Type u_1)) ↦ 𝓟 (↑s : Set α)) (Subtype.mk (p := fun (x : Set α) ↦ x ∈ B.sets) U U_in))
    ((fun (s : (↑B.sets : Type u_1)) ↦ 𝓟 (↑s : Set α)) (Subtype.mk (p := fun (x : Set α) ↦ x ∈ B.sets) W W_in)) ∧
  (fun (x1 x2 : Filter α) ↦ x1 ≥ x2)
    ((fun (s : (↑B.sets : Type u_1)) ↦ 𝓟 (↑s : Set α)) (Subtype.mk (p := fun (x : Set α) ↦ x ∈ B.sets) V V_in))
    ((fun (s : (↑B.sets : Type u_1)) ↦ 𝓟 (↑s : Set α)) (Subtype.mk (p := fun (x : Set α) ↦ x ∈ B.sets) W W_in))
Tactic: use ⟨W, W_in⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Bases.Basic (goal)
Goal:
α : Type u_1
B : FilterBasis α
U : Set α
U_in : U ∈ B.sets
V : Set α
V_in : V ∈ B.sets
W : Set α
W_in : W ∈ B.sets
W_sub : W ⊆ U ∩ V
⊢ (fun (x1 x2 : Filter α) ↦ x1 ≥ x2)
      ((fun (s : (↑B.sets : Type u_1)) ↦ 𝓟 (↑s : Set α)) (Subtype.mk (p := fun (x : Set α) ↦ x ∈ B.sets) U U_in))
      ((fun (s : (↑B.sets : Type u_1)) ↦ 𝓟 (↑s : Set α)) (Subtype.mk (p := fun (x : Set α) ↦ x ∈ B.sets) W W_in)) ∧
    (fun (x1 x2 : Filter α) ↦ x1 ≥ x2)
      ((fun (s : (↑B.sets : Type u_1)) ↦ 𝓟 (↑s : Set α)) (Subtype.mk (p := fun (x : Set α) ↦ x ∈ B.sets) V V_in))
      ((fun (s : (↑B.sets : Type u_1)) ↦ 𝓟 (↑s : Set α)) (Subtype.mk (p := fun (x : Set α) ↦ x ∈ B.sets) W W_in))
have h : W ⊆ U ∧ W ⊆ V
Tactic: simp only [le_principal_iff, mem_principal]