awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.TendstoCofinite
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TendstoCofinite f
x : β →₀ ℕ
s : Finset α := x.support.sup fun (t : β) ↦ ⋯.toFinset (s := f ⁻¹' {t})
e : ↥s ↪ α := Function.Embedding.subtype fun (u : α) ↦ u ∈ s
⊢ Set.Finite (α := α →₀ ℕ) (mapDomain f ⁻¹' {x})

Tactic:
Set.Finite.subset (Set.Finite.image (embDomain e) <| finite_of_degree_le (degree x)) ?_

Premises used: Finsupp.finite_of_degree_le, Finsupp.degree, Set.Finite.subset, Set.Finite.image, Finsupp.embDomain, DFunLike.coe
-- Module: Mathlib.Order.Filter.TendstoCofinite
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TendstoCofinite f
x : β →₀ ℕ
s : Finset α := x.support.sup fun (t : β) ↦ ⋯.toFinset (s := f ⁻¹' {t})
e : ↥s ↪ α := Function.Embedding.subtype fun (u : α) ↦ u ∈ s
refine :
  Subset (α := Set (α →₀ ℕ)) (mapDomain f ⁻¹' {x})
    (embDomain e ''
      {f : ↥s →₀ ℕ | LE.le (α := ℕ) ((degree : (a : ↥s →₀ ℕ) → ℕ) f : ℕ) ((degree : (a : β →₀ ℕ) → ℕ) x : ℕ)})
⊢ Set.Finite (α := α →₀ ℕ) (mapDomain f ⁻¹' {x})

Tactic:
refine Set.Finite.subset (Set.Finite.image (embDomain e) <| finite_of_degree_le (degree x)) ?_

Premises used: Finsupp.finite_of_degree_le, Finsupp.degree, Set.Finite.subset, Set.Finite.image, Finsupp.embDomain, DFunLike.coe
-- Module: Mathlib.Order.Filter.TendstoCofinite
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TendstoCofinite f
x : β →₀ ℕ
s : Finset α := x.support.sup fun (t : β) ↦ ⋯.toFinset (s := f ⁻¹' {t})
e : ↥s ↪ α := Function.Embedding.subtype fun (u : α) ↦ u ∈ s
⊢ ∀ (x_1 : α →₀ ℕ),
    mapDomain f x_1 = x →
      ∃ (x_2 : ↥s →₀ ℕ),
        LE.le (α := ℕ) ((degree : (a : ↥s →₀ ℕ) → ℕ) x_2 : ℕ) ((degree : (a : β →₀ ℕ) → ℕ) x : ℕ) ∧
          embDomain e x_2 = x_1

Tactic:
fun y hy ↦ ⟨y.comapDomain e e.injective.injOn, ?_, embDomain_comapDomain ?_⟩

Premises used: Function.Injective.injOn, Finsupp.embDomain_comapDomain, And.intro, Exists.intro, Function.Embedding.injective, Finsupp.comapDomain, DFunLike.coe
-- Module: Mathlib.Order.Filter.TendstoCofinite
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TendstoCofinite f
x : β →₀ ℕ
s : Finset α := x.support.sup fun (t : β) ↦ ⋯.toFinset (s := f ⁻¹' {t})
e : ↥s ↪ α := Function.Embedding.subtype fun (u : α) ↦ u ∈ s
refine_1 :
  ∀ (y : α →₀ ℕ) (hy : mapDomain f y = x),
    LE.le (α := ℕ) ((degree : (a : ↥s →₀ ℕ) → ℕ) (comapDomain (⇑e : (a : ↥s) → α) y ⋯) : ℕ)
      ((degree : (a : β →₀ ℕ) → ℕ) x : ℕ)
refine_2 : ∀ (y : α →₀ ℕ) (hy : mapDomain f y = x), (↑y.support : Set α) ⊆ range (ι := ↥s) (⇑e : (a : ↥s) → α)
⊢ ∀ (x_1 : α →₀ ℕ),
    mapDomain f x_1 = x →
      ∃ (x_2 : ↥s →₀ ℕ),
        LE.le (α := ℕ) ((degree : (a : ↥s →₀ ℕ) → ℕ) x_2 : ℕ) ((degree : (a : β →₀ ℕ) → ℕ) x : ℕ) ∧
          embDomain e x_2 = x_1

Tactic:
refine fun y hy ↦ ⟨y.comapDomain e e.injective.injOn, ?_, embDomain_comapDomain ?_⟩
-- Module: Mathlib.Order.Filter.TendstoCofinite
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TendstoCofinite f
x : β →₀ ℕ
s : Finset α := x.support.sup fun (t : β) ↦ ⋯.toFinset (s := f ⁻¹' {t})
e : ↥s ↪ α := Function.Embedding.subtype fun (u : α) ↦ u ∈ s
y : α →₀ ℕ
hy : mapDomain f y = x
refine_1 :
  LE.le (α := ℕ) ((degree : (a : ↥s →₀ ℕ) → ℕ) (comapDomain (⇑e : (a : ↥s) → α) y ⋯) : ℕ)
    ((degree : (a : α →₀ ℕ) → ℕ) y : ℕ)
⊢ LE.le (α := ℕ) ((degree : (a : ↥s →₀ ℕ) → ℕ) (comapDomain (⇑e : (a : ↥s) → α) y ⋯) : ℕ)
    ((degree : (a : β →₀ ℕ) → ℕ) x : ℕ)

Tactic:
rw [← hy, degree_mapDomain]

Premises used: Finsupp.degree_mapDomain
-- Module: Mathlib.Order.Filter.TendstoCofinite
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TendstoCofinite f
x : β →₀ ℕ
s : Finset α := x.support.sup fun (t : β) ↦ ⋯.toFinset (s := f ⁻¹' {t})
e : ↥s ↪ α := Function.Embedding.subtype fun (u : α) ↦ u ∈ s
y : α →₀ ℕ
hy : mapDomain f y = x
⊢ LE.le (α := ℕ) ((degree : (a : ↥s →₀ ℕ) → ℕ) (comapDomain (⇑e : (a : ↥s) → α) y ⋯) : ℕ)
    ((degree : (a : α →₀ ℕ) → ℕ) y : ℕ)

Tactic:
degree_comapDomain_le_of_canonicallyOrderedAdd ..

Premises used: Finsupp.degree_comapDomain_le_of_canonicallyOrderedAdd
-- Module: Mathlib.Order.Filter.TendstoCofinite
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TendstoCofinite f
x : β →₀ ℕ
s : Finset α := x.support.sup fun (t : β) ↦ ⋯.toFinset (s := f ⁻¹' {t})
e : ↥s ↪ α := Function.Embedding.subtype fun (u : α) ↦ u ∈ s
y : α →₀ ℕ
hy : mapDomain f y = x
⊢ LE.le (α := ℕ) ((degree : (a : ↥s →₀ ℕ) → ℕ) (comapDomain (⇑e : (a : ↥s) → α) y ⋯) : ℕ)
    ((degree : (a : α →₀ ℕ) → ℕ) y : ℕ)

Tactic:
exact degree_comapDomain_le_of_canonicallyOrderedAdd ..

Premises used: Finsupp.degree_comapDomain_le_of_canonicallyOrderedAdd
-- Module: Mathlib.Order.Filter.TendstoCofinite
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TendstoCofinite f
x : β →₀ ℕ
s : Finset α := x.support.sup fun (t : β) ↦ ⋯.toFinset (s := f ⁻¹' {t})
e : ↥s ↪ α := Function.Embedding.subtype fun (u : α) ↦ u ∈ s
y : α →₀ ℕ
hy : mapDomain f y = x
this : y.support ⊆ s
⊢ (↑y.support : Set α) ⊆ range (ι := ↥s) (⇑e : (a : ↥s) → α)

Tactic:
simpa [e]
-- Module: Mathlib.Order.Filter.TendstoCofinite
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TendstoCofinite f
x : β →₀ ℕ
s : Finset α := x.support.sup fun (t : β) ↦ ⋯.toFinset (s := f ⁻¹' {t})
e : ↥s ↪ α := Function.Embedding.subtype fun (u : α) ↦ u ∈ s
y : α →₀ ℕ
hy : mapDomain f y = x
refine_2 : y.support ⊆ s
⊢ (↑y.support : Set α) ⊆ range (ι := ↥s) (⇑e : (a : ↥s) → α)

Tactic:
suffices y.support ⊆ s by simpa [e]
-- Module: Mathlib.Order.Filter.TendstoCofinite
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TendstoCofinite f
x : β →₀ ℕ
s : Finset α := x.support.sup fun (t : β) ↦ ⋯.toFinset (s := f ⁻¹' {t})
e : ↥s ↪ α := Function.Embedding.subtype fun (u : α) ↦ u ∈ s
y : α →₀ ℕ
hy : mapDomain f y = x
i : α
hi : ¬Eq (α := ℕ) ((y : (a : α) → ℕ) i : ℕ) (0 : ℕ)
⊢ ¬Eq (α := ℕ) ((y : (a : α) → ℕ) i : ℕ) (0 : ℕ) ∧ f i = f i ∧ ¬Eq (α := ℕ) ((y : (a : α) → ℕ) i : ℕ) (0 : ℕ)

Tactic:
simp [hi]
-- Module: Mathlib.Order.Filter.TendstoCofinite
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TendstoCofinite f
x : β →₀ ℕ
s : Finset α := x.support.sup fun (t : β) ↦ ⋯.toFinset (s := f ⁻¹' {t})
e : ↥s ↪ α := Function.Embedding.subtype fun (u : α) ↦ u ∈ s
y : α →₀ ℕ
hy : mapDomain f y = x
⊢ y.support ⊆ s

Tactic:
simpa [← hy, mapDomain, sum, Finset.subset_iff, single_apply, s] using
      fun i hi ↦ ⟨i, by simp [hi]⟩

Premises used: Finsupp.mapDomain, Finsupp.sum, Finset.subset_iff, Finsupp.single_apply
-- Module: Mathlib.Order.Filter.TendstoCofinite
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TendstoCofinite f
refine : ∀ (x : β →₀ ℕ), Set.Finite (α := α →₀ ℕ) (mapDomain f ⁻¹' {x})
refine₁ refine₂ : ∀ (x : β →₀ ℕ), Set.Finite (α := α →₀ ℕ) (mapDomain f ⁻¹' {x})
refine₃ :
  ∀ (x : β →₀ ℕ),
    let s : Finset α := x.support.sup fun (t : β) ↦ ⋯.toFinset (s := f ⁻¹' {t});
    let e : ↥s ↪ α := Function.Embedding.subtype fun (u : α) ↦ u ∈ s;
    Subset (α := Set (α →₀ ℕ)) (mapDomain f ⁻¹' {x})
      (embDomain e ''
        {f : ↥s →₀ ℕ | LE.le (α := ℕ) ((degree : (a : ↥s →₀ ℕ) → ℕ) f : ℕ) ((degree : (a : β →₀ ℕ) → ℕ) x : ℕ)})
refine₄ :
  ∀ (x : β →₀ ℕ),
    let s : Finset α := x.support.sup fun (t : β) ↦ ⋯.toFinset (s := f ⁻¹' {t});
    let e : ↥s ↪ α := Function.Embedding.subtype fun (u : α) ↦ u ∈ s;
    ∀ (x_1 : α →₀ ℕ),
      mapDomain f x_1 = x →
        ∃ (x_2 : ↥s →₀ ℕ),
          LE.le (α := ℕ) ((degree : (a : ↥s →₀ ℕ) → ℕ) x_2 : ℕ) ((degree : (a : β →₀ ℕ) → ℕ) x : ℕ) ∧
            embDomain e x_2 = x_1
refine_1 :
  ∀ (x : β →₀ ℕ),
    let s : Finset α := x.support.sup fun (t : β) ↦ ⋯.toFinset (s := f ⁻¹' {t});
    let e : ↥s ↪ α := Function.Embedding.subtype fun (u : α) ↦ u ∈ s;
    ∀ (y : α →₀ ℕ) (hy : mapDomain f y = x),
      LE.le (α := ℕ) ((degree : (a : ↥s →₀ ℕ) → ℕ) (comapDomain (⇑e : (a : ↥s) → α) y ⋯) : ℕ)
        ((degree : (a : β →₀ ℕ) → ℕ) x : ℕ)
refine_2 refine_2₁ :
  ∀ (x : β →₀ ℕ),
    let s : Finset α := x.support.sup fun (t : β) ↦ ⋯.toFinset (s := f ⁻¹' {t});
    let e : ↥s ↪ α := Function.Embedding.subtype fun (u : α) ↦ u ∈ s;
    ∀ (y : α →₀ ℕ) (hy : mapDomain f y = x), (↑y.support : Set α) ⊆ range (ι := ↥s) (⇑e : (a : ↥s) → α)
⊢ TendstoCofinite (α := α →₀ ℕ) (mapDomain f)

Tactic:
classical
  refine (tendstoCofinite_iff_finite_preimage_singleton _).mpr fun x ↦ ?_
  let s := Finset.sup x.support (fun t ↦ (TendstoCofinite.finite_preimage_singleton f t).toFinset)
  let e : s ↪ α := Function.Embedding.subtype (fun u ↦ u ∈ s)
  refine Set.Finite.subset (Set.Finite.image (embDomain e) <| finite_of_degree_le (degree x)) ?_
  simp only [Set.subset_def, Set.mem_preimage, Set.mem_singleton_iff, Set.mem_image,
    Set.mem_setOf_eq]
  refine fun y hy ↦ ⟨y.comapDomain e e.injective.injOn, ?_, embDomain_comapDomain ?_⟩
  · rw [← hy, degree_mapDomain]
    exact degree_comapDomain_le_of_canonicallyOrderedAdd ..
  · suffices y.support ⊆ s by simpa [e]
    simpa [← hy, mapDomain, sum, Finset.subset_iff, single_apply, s] using
      fun i hi ↦ ⟨i, by simp [hi]⟩

Premises used: Iff.mpr, Finsupp.degree_mapDomain, Set.subset_def, Finsupp.mapDomain, Finsupp.sum, Set.mem_image, Filter.tendstoCofinite_iff_finite_preimage_singleton, Set.mem_setOf_eq, Finsupp.degree_comapDomain_le_of_canonicallyOrderedAdd, Set.mem_singleton_iff, Finset.subset_iff, Finsupp.single_apply, Set.mem_preimage
-- Module: Mathlib.Order.Filter.Ultrafilter.Basic
Goal:
α : Type u
f : Ultrafilter α
s : Set (Set α)
⊢ ⋃₀ ∅ ∈ f ↔ ∃ (t : Set α), Membership.mem (γ := Set (Set α)) ∅ t ∧ t ∈ f

Tactic:
simp
-- Module: Mathlib.Order.Filter.Ultrafilter.Basic
Goal:
α : Type u
f : Ultrafilter α
s : Set (Set α)
a : Set α
s_1 : Set (Set α)
h : a ∉ s_1
hs : s_1.Finite
his : ⋃₀ s_1 ∈ f ↔ ∃ t ∈ s_1, t ∈ f
⊢ ⋃₀ insert a s_1 ∈ f ↔ ∃ t ∈ insert a s_1, t ∈ f

Tactic:
simp [union_mem_iff, his, or_and_right, exists_or]

Premises used: exists_or, Ultrafilter.union_mem_iff, or_and_right
-- Module: Mathlib.Order.Filter.Ultrafilter.Basic
Goal:
α : Type u
f : Ultrafilter α
s : Set (Set α)
hs : s.Finite
empty : ⋃₀ ∅ ∈ f ↔ ∃ (t : Set α), Membership.mem (γ := Set (Set α)) ∅ t ∧ t ∈ f
insert :
  ∀ {a : Set α} {s : Set (Set α)},
    a ∉ s → s.Finite → ∀ (his : ⋃₀ s ∈ f ↔ ∃ t ∈ s, t ∈ f), ⋃₀ Insert.insert a s ∈ f ↔ ∃ t ∈ Insert.insert a s, t ∈ f
⊢ ⋃₀ s ∈ f ↔ ∃ t ∈ s, t ∈ f

Tactic:
induction s, hs using Set.Finite.induction_on with
  | empty => simp
  | insert _ _ his => simp [union_mem_iff, his, or_and_right, exists_or]

Premises used: exists_or, Ultrafilter.union_mem_iff, Insert.insert, or_and_right
-- Module: Mathlib.Order.Filter.Ultrafilter.Basic
Goal:
α : Type u
β : Type v
f : Ultrafilter α
is : Set β
s : β → Set α
his : is.Finite
⊢ ⋃ i ∈ is, s i ∈ f ↔ ∃ i ∈ is, s i ∈ f

Tactic:
simp only [← sUnion_image, finite_sUnion_mem_iff (his.image s), exists_mem_image]

Premises used: Set.Finite.image, Set.sUnion_image, Set.exists_mem_image, Ultrafilter.finite_sUnion_mem_iff
-- Module: Mathlib.Order.Filter.Ultrafilter.Basic
Goal:
α : Type u
β : Type v
f : Ultrafilter α
is : Set β
P : β → α → Prop
his : is.Finite
simp : {x : α | ∃ a ∈ is, P a x} ∈ f ↔ ∃ a ∈ is, {x : α | P a x} ∈ f
⊢ (∀ᶠ (i : α) in (↑f : Filter α), ∃ a ∈ is, P a i) ↔ ∃ a ∈ is, ∀ᶠ (i : α) in (↑f : Filter α), P a i

Tactic:
simp only [Filter.Eventually, Ultrafilter.mem_coe]

Premises used: Filter.Eventually, Ultrafilter.mem_coe
-- Module: Mathlib.Order.Filter.Ultrafilter.Basic
Goal:
α : Type u
β : Type v
f : Ultrafilter α
is : Set β
P : β → α → Prop
his : is.Finite
⊢ ⋃ i ∈ is, P i ∈ f ↔ ∃ i ∈ is, P i ∈ f

Tactic:
f.finite_biUnion_mem_iff his (s := P)

Premises used: Ultrafilter.finite_biUnion_mem_iff
-- Module: Mathlib.Order.Filter.Ultrafilter.Basic
Goal:
α : Type u
β : Type v
f : Ultrafilter α
is : Set β
P : β → α → Prop
his : is.Finite
h : Eq.{u + 1} (α := Set α) {x : α | ∃ a ∈ is, P a x} (⋃ i ∈ is, P i)
⊢ {x : α | ∃ a ∈ is, P a x} ∈ f ↔ ∃ a ∈ is, {x : α | P a x} ∈ f

Tactic:
convert! f.finite_biUnion_mem_iff his (s := P) with i

Premises used: Ultrafilter.finite_biUnion_mem_iff
-- Module: Mathlib.Order.Filter.Ultrafilter.Basic
Goal:
α : Type u
β : Type v
f : Ultrafilter α
is : Set β
P : β → α → Prop
his : is.Finite
⊢ Eq.{u + 1} (α := Set α) {x : α | ∃ a ∈ is, P a x} (⋃ i ∈ is, P i)

Tactic:
aesop
-- Module: Mathlib.Order.Filter.Ultrafilter.Basic
Goal:
α : Type u
β : Type v
f : Ultrafilter α
inst : Finite β
P : β → α → Prop
⊢ (∀ᶠ (i : α) in (↑f : Filter α), ∃ (a : β), P a i) ↔ ∃ (a : β), ∀ᶠ (i : α) in (↑f : Filter α), P a i

Tactic:
simpa using eventually_exists_mem_iff (f := f) (P := P) Set.finite_univ

Premises used: Ultrafilter.eventually_exists_mem_iff, Set.finite_univ
-- Module: Mathlib.Order.Filter.Ultrafilter.Basic
Goal:
α : Type u
f : Ultrafilter α
s : Set α
h : s.Finite
h' : s ∈ f
⊢ ⋃ x ∈ s, {x} ∈ f

Tactic:
rw [← biUnion_of_singleton s] at h'

Premises used: Set.biUnion_of_singleton
-- Module: Mathlib.Order.Filter.Ultrafilter.Basic
Goal:
α : Type u
f : Ultrafilter α
s : Set α
h : s.Finite
h' : ⋃ x ∈ s, {x} ∈ f
rcases : ∀ (a : α) (has : a ∈ s) (haf : {a} ∈ f), ∃ x ∈ s, f = pure x
⊢ ∃ x ∈ s, f = pure x

Tactic:
rcases (Ultrafilter.finite_biUnion_mem_iff h).mp h' with ⟨a, has, haf⟩

Premises used: Ultrafilter.finite_biUnion_mem_iff, Iff.mp
-- Module: Mathlib.Order.Filter.Ultrafilter.Basic
Goal:
α : Type u
f : Ultrafilter α
s : Set α
h : s.Finite
h' : ⋃ x ∈ s, {x} ∈ f
a : α
has : a ∈ s
haf : {a} ∈ f
⊢ ∃ x ∈ s, f = pure x

Tactic:
⟨a, has, eq_of_le (Filter.le_pure_iff.2 haf)⟩

Premises used: Iff.mpr, Filter.le_pure_iff, And.intro, Exists.intro, Ultrafilter.eq_of_le
-- Module: Mathlib.Order.Filter.Ultrafilter.Basic
Goal:
α : Type u
f : Ultrafilter α
s : Set α
h : s.Finite
h' : ⋃ x ∈ s, {x} ∈ f
a : α
has : a ∈ s
haf : {a} ∈ f
⊢ ∃ x ∈ s, f = pure x

Tactic:
exact ⟨a, has, eq_of_le (Filter.le_pure_iff.2 haf)⟩
-- Module: Mathlib.Order.Filter.Ultrafilter.Basic
Goal:
α : Type u
inst : Finite α
f : Ultrafilter α
⊢ ∃ (a : α), f = pure a

Tactic:
(eq_pure_of_finite_mem finite_univ univ_mem).imp fun _ ⟨_, ha⟩ => ha

Premises used: Exists.imp, Set.finite_univ, Filter.univ_mem, Ultrafilter.eq_pure_of_finite_mem
-- Module: Mathlib.Order.Filter.Ultrafilter.Basic
Goal:
α : Type u
f : Ultrafilter α
⊢ (↑f : Filter α) ≤ cofinite ∨ ∃ (a : α), f = pure a

Tactic:
or_iff_not_imp_left.2 fun h =>
    let ⟨_, hs, hfin⟩ := Filter.disjoint_cofinite_right.1 (disjoint_iff_not_le.2 h)
    let ⟨a, _, hf⟩ := eq_pure_of_finite_mem hfin hs
    ⟨a, hf⟩

Premises used: Pure.pure, Iff.mpr, Exists, Filter.disjoint_cofinite_right, Classical.or_iff_not_imp_left, _private.0.Ultrafilter.le_cofinite_or_eq_pure.match_2, Exists.intro, Iff.mp, _private.0.Ultrafilter.le_cofinite_or_eq_pure.match_1, Ultrafilter.eq_pure_of_finite_mem, Eq, Ultrafilter.disjoint_iff_not_le
-- Module: Mathlib.Order.Filter.Ultrafilter.Basic
Goal:
α : Type u
S : Set (Set α)
cond : ∀ (T : Finset (Set α)), (↑T : Set (Set α)) ⊆ S → (⋂₀ (↑T : Set (Set α))).Nonempty
⊢ ∃ (F : Ultrafilter α), S ⊆ (↑F : Filter α).sets

Tactic:
haveI : NeBot (generate S) :=
    generate_neBot_iff.2 fun _ hts ht =>
      ht.coe_toFinset ▸ cond ht.toFinset (ht.coe_toFinset.symm ▸ hts)
  ⟨of (generate S), fun _ ht => (of_le <| generate S) <| GenerateSets.basic ht⟩

Premises used: Ultrafilter.of_le, Ultrafilter.of, Exists.intro, Filter.GenerateSets.basic, Filter.generate
-- Module: Mathlib.Order.Filter.Ultrafilter.Basic
Goal:
α : Type u
inst : PartialOrder α
x : α
hx : IsTop x
⊢ atTop = pure x

Tactic:
{ top := x, le_top := hx : OrderTop α }.atTop_eq

Premises used: Set.Mem, setOf, Filter.OrderTop.atTop_eq
-- Module: Mathlib.Order.Filter.Ultrafilter.Basic
Goal:
α : Type u
β : Type v
f : α → β
l₁ : Filter α
l₂ : Filter β
⊢ Tendsto f l₁ l₂ ↔ ∀ (g : Ultrafilter α), (↑g : Filter α) ≤ l₁ → Tendsto f (↑g : Filter α) l₂

Tactic:
simpa only [tendsto_iff_comap] using le_iff_ultrafilter

Premises used: Filter.tendsto_iff_comap, Filter.le_iff_ultrafilter
-- Module: Mathlib.Order.Filter.Ultrafilter.Basic
Goal:
α : Type u
inst : Infinite α
⊢ (↑(hyperfilter α) : Filter α) ≤ cofinite

Tactic:
Ultrafilter.of_le cofinite

Premises used: Set.Mem, Ultrafilter.of_le, Filter.cofinite
-- Module: Mathlib.Order.Filter.Ultrafilter.Basic
Goal:
⊢ (↑(hyperfilter ℕ) : Filter ℕ) ≤ atTop

Tactic:
hyperfilter_le_cofinite.trans_eq Nat.cofinite_eq_atTop

Premises used: LE.le.trans_eq, Nat.cofinite_eq_atTop, Filter.hyperfilter_le_cofinite
-- Module: Mathlib.Order.Filter.Ultrafilter.Basic
Goal:
α : Type u
inst : Infinite α
⊢ ⊥ ≠ (↑(hyperfilter α) : Filter α)

Tactic:
(NeBot.ne inferInstance).symm

Premises used: Filter.NeBot.ne, inferInstance, Ne.symm
-- Module: Mathlib.Order.Filter.Ultrafilter.Basic
Goal:
α : Type u
inst : Infinite α
s : Set α
hf : s.Finite
⊢ s ∉ hyperfilter α

Tactic:
fun hy =>
  compl_notMem hy <| hyperfilter_le_cofinite hf.compl_mem_cofinite

Premises used: Set.Finite.compl_mem_cofinite, Filter.hyperfilter_le_cofinite, Not, Filter.compl_notMem
-- Module: Mathlib.Order.Filter.Ultrafilter.Basic
Goal:
α : Type u
inst : Infinite α
s : Set α
hf : s.Finite
⊢ sᶜ ∈ hyperfilter α

Tactic:
compl_mem_iff_notMem.2 hf.notMem_hyperfilter

Premises used: Iff.mpr, Set.Finite.notMem_hyperfilter, Ultrafilter.compl_mem_iff_notMem
-- Module: Mathlib.Order.Filter.Ultrafilter.Basic
Goal:
α : Type u
inst : Infinite α
s : Set α
hf : sᶜ.Finite
⊢ s ∈ hyperfilter α

Tactic:
compl_compl s ▸ hf.compl_mem_hyperfilter

Premises used: compl_compl, Set.Finite.compl_mem_hyperfilter, Eq.rec
-- Module: Mathlib.Order.Filter.ZeroAndBoundedAtFilter
Goal:
α : Type u_2
β : Type u_3
inst : Zero β
inst_1 : TopologicalSpace β
l : Filter α
⊢ ZeroAtFilter.{u_2, u_3} (β := β) l 0

Tactic:
tendsto_const_nhds

Premises used: tendsto_const_nhds, Filter.ZeroAtFilter
-- Module: Mathlib.Order.Filter.ZeroAndBoundedAtFilter
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
inst_1 : AddZeroClass β
inst_2 : ContinuousAdd β
l : Filter α
f g : α → β
hf : l.ZeroAtFilter f
hg : l.ZeroAtFilter g
⊢ l.ZeroAtFilter (f + g)

Tactic:
simpa using hf.add hg

Premises used: Filter.ZeroAtFilter.add
-- Module: Mathlib.Order.Filter.ZeroAndBoundedAtFilter
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
inst_1 : SubtractionMonoid β
inst_2 : ContinuousNeg β
l : Filter α
f : α → β
hf : l.ZeroAtFilter f
⊢ l.ZeroAtFilter (-f)

Tactic:
simpa using hf.neg

Premises used: Filter.ZeroAtFilter.neg
-- Module: Mathlib.Order.Filter.ZeroAndBoundedAtFilter
Goal:
𝕜 : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
inst_1 : Zero β
inst_2 : SMulZeroClass 𝕜 β
inst_3 : ContinuousConstSMul 𝕜 β
l : Filter α
f : α → β
c : 𝕜
hf : l.ZeroAtFilter f
⊢ l.ZeroAtFilter (c • f)

Tactic:
simpa using hf.const_smul c

Premises used: Filter.Tendsto.const_smul
-- Module: Mathlib.Order.Filter.ZeroAndBoundedAtFilter
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddGroup β
l : Filter α
f : α → β
hf : l.ZeroAtFilter f
⊢ l.BoundedAtFilter f

Tactic:
((Asymptotics.isLittleO_one_iff _).mpr hf).isBigO

Premises used: Iff.mpr, Filter.BoundedAtFilter, Asymptotics.IsLittleO.isBigO, Asymptotics.isLittleO_one_iff
-- Module: Mathlib.Order.Filter.ZeroAndBoundedAtFilter
Goal:
α : Type u_2
β : Type u_3
inst : Norm β
l : Filter α
c : β
⊢ l.BoundedAtFilter (Function.const α c)

Tactic:
Asymptotics.isBigO_const_const c one_ne_zero l

Premises used: Filter.BoundedAtFilter, Asymptotics.isBigO_const_const, one_ne_zero
-- Module: Mathlib.Order.Filter.ZeroAndBoundedAtFilter
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup β
l : Filter α
f g : α → β
hf : l.BoundedAtFilter f
hg : l.BoundedAtFilter g
⊢ l.BoundedAtFilter (f + g)

Tactic:
simpa using hf.add hg

Premises used: Filter.BoundedAtFilter.add
-- Module: Mathlib.Order.Filter.ZeroAndBoundedAtFilter
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup β
l : Filter α
f : α → β
hf : l.BoundedAtFilter f
⊢ l.BoundedAtFilter (-f)

Tactic:
hf.neg_left

Premises used: Asymptotics.IsBigO.neg_left, Filter.BoundedAtFilter
-- Module: Mathlib.Order.Filter.ZeroAndBoundedAtFilter
Goal:
𝕜 : Type u_1
α : Type u_2
β : Type u_3
inst : SeminormedRing 𝕜
inst_1 : SeminormedAddCommGroup β
inst_2 : Module 𝕜 β
inst_3 : IsBoundedSMul 𝕜 β
l : Filter α
f : α → β
c : 𝕜
hf : l.BoundedAtFilter f
⊢ l.BoundedAtFilter (c • f)

Tactic:
hf.const_smul_left c

Premises used: Asymptotics.IsBigO.const_smul_left, Filter.BoundedAtFilter
-- Module: Mathlib.Order.Filter.ZeroAndBoundedAtFilter
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedRing β
l : Filter α
f g : α → β
hf : l.ZeroAtFilter f
hg : l.BoundedAtFilter g
rw :
  ∀ (hf : Asymptotics.IsLittleO (F := ℝ) l f fun (_x : α) ↦ 1) (hg : l.BoundedAtFilter g),
    Asymptotics.IsLittleO (F := ℝ) l (f * g) fun (_x : α) ↦ 1
⊢ l.ZeroAtFilter (f * g)

Tactic:
rw [ZeroAtFilter, ← Asymptotics.isLittleO_one_iff (F := ℝ)] at hf ⊢

Premises used: Real, Filter.ZeroAtFilter, Asymptotics.isLittleO_one_iff
-- Module: Mathlib.Order.Filter.ZeroAndBoundedAtFilter
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedRing β
l : Filter α
f g : α → β
hf : Asymptotics.IsLittleO (F := ℝ) l f fun (_x : α) ↦ 1
hg : l.BoundedAtFilter g
⊢ Asymptotics.IsLittleO (F := ℝ) l (f * g) fun (_x : α) ↦ 1

Tactic:
simpa using hf.mul_isBigO hg

Premises used: Asymptotics.IsLittleO.mul_isBigO
-- Module: Mathlib.Order.Filter.ZeroAndBoundedAtFilter
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedRing β
l : Filter α
f g : α → β
hf : l.BoundedAtFilter f
hg : l.ZeroAtFilter g
rw :
  ∀ (hg : Asymptotics.IsLittleO (F := ℝ) l g fun (_x : α) ↦ 1),
    Asymptotics.IsLittleO (F := ℝ) l (f * g) fun (_x : α) ↦ 1
⊢ l.ZeroAtFilter (f * g)

Tactic:
rw [ZeroAtFilter, ← Asymptotics.isLittleO_one_iff (F := ℝ)] at hg ⊢

Premises used: Real, Filter.ZeroAtFilter, Asymptotics.isLittleO_one_iff
-- Module: Mathlib.Order.Filter.ZeroAndBoundedAtFilter
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedRing β
l : Filter α
f g : α → β
hf : l.BoundedAtFilter f
hg : Asymptotics.IsLittleO (F := ℝ) l g fun (_x : α) ↦ 1
⊢ Asymptotics.IsLittleO (F := ℝ) l (f * g) fun (_x : α) ↦ 1

Tactic:
simpa using hf.mul_isLittleO hg

Premises used: Asymptotics.IsBigO.mul_isLittleO
-- Module: Mathlib.Order.Filter.ZeroAndBoundedAtFilter
Goal:
𝕜 : Type u_1
α : Type u_2
β : Type u_3
inst : SeminormedCommRing 𝕜
inst_1 : SeminormedRing β
inst_2 : Algebra 𝕜 β
inst_3 : IsBoundedSMul 𝕜 β
l : Filter α
f g : α → β
hf : Membership.mem (γ := Submodule 𝕜 (α → β)) (boundedFilterSubmodule 𝕜 l : Submodule 𝕜 (α → β)) f
hg : Membership.mem (γ := Submodule 𝕜 (α → β)) (boundedFilterSubmodule 𝕜 l : Submodule 𝕜 (α → β)) g
⊢ Membership.mem (γ := Submodule 𝕜 (α → β)) (boundedFilterSubmodule 𝕜 l : Submodule 𝕜 (α → β)) (f * g)

Tactic:
simpa only [Pi.one_apply, mul_one, norm_mul] using hf.mul hg

Premises used: Filter.BoundedAtFilter.mul, Pi.one_apply, norm_mul, mul_one
-- Module: Mathlib.Order.Filter.ZeroAndBoundedAtFilter
Goal:
α : Type u_2
β : Type u_3
ι : Type
s : Finset ι
inst : SeminormedCommRing β
l : Filter α
f : ι → α → β
h : ∀ i ∈ s, l.BoundedAtFilter (f i)
⊢ BoundedAtFilter.{u_2, u_3} (β := β) l (∏ i ∈ s, f i)

Tactic:
(boundedFilterSubalgebra β l).prod_mem (f := f) h

Premises used: Set.Mem, Filter.BoundedAtFilter, Subalgebra.prod_mem
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
a b : Fin n
⊢ (↑(a ⊔ b) : ℕ) = max (↑a : ℕ) (↑b : ℕ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
a b : Fin n
⊢ (↑(a ⊓ b) : ℕ) = min (↑a : ℕ) (↑b : ℕ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
a b : Fin n
⊢ compare a b = compare (↑a : ℕ) (↑b : ℕ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
inst : NeZero n
⊢ Eq (α := Fin n) ⊥ 0

Tactic:
_root_.bot_eq_zero

Premises used: bot_eq_zero
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
⊢ ⊤ = last n

Tactic:
rfl

Premises used: Nat.pred, rfl
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
inst : NeZero n
⊢ Eq (α := Fin n) (rev ⊥) ⊤

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
inst : NeZero n
⊢ Eq (α := Fin n) (rev ⊤) ⊥

Tactic:
rev_rev _

Premises used: Fin.rev_rev
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
inst : NeZero n
⊢ Eq (α := Fin n) (rev 0) ⊤

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
rw : Eq (α := Fin (n + 1)) 0 ⊥
rw₁ rw₂ : Eq (α := Fin (n + 1)) 0 0
⊢ (last n).rev = ⊥

Tactic:
rw [rev_last, bot_eq_zero]

Premises used: Fin.rev_last, bot_eq_zero