awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.AtTopBot.Finset
Goal:
α : Type u_3
β : Type u_4
s : Set (Finset α)
t : Finset α
H : ∀ b ≥ t, b ∈ s
⊢ ∃ (a : Finset (α ⊕ β)), ∀ b ≥ a, b.toLeft ∈ s

Tactic:
exact ⟨t.disjSum ∅, fun b hb ↦ H _ (by simpa [← Finset.coe_subset, Set.subset_def] using hb)⟩
-- Module: Mathlib.Order.Filter.AtTopBot.Finset
Goal:
α : Type u_3
β : Type u_4
s : Set (Finset β)
hs : Membership.mem (γ := Filter (Finset β)) atTop s
simp : ∀ (hs : ∃ (a : Finset β), ∀ b ≥ a, b ∈ s), ∃ (a : Finset (α ⊕ β)), ∀ b ≥ a, b.toRight ∈ s
⊢ Membership.mem (γ := Filter (Finset β)) (map (α := Finset (α ⊕ β)) Finset.toRight atTop) s

Tactic:
simp only [mem_atTop_sets, Filter.mem_map, Set.mem_preimage] at hs ⊢

Premises used: Filter.mem_atTop_sets, Filter.mem_map, Set.mem_preimage
-- Module: Mathlib.Order.Filter.AtTopBot.Finset
Goal:
α : Type u_3
β : Type u_4
s : Set (Finset β)
hs : ∃ (a : Finset β), ∀ b ≥ a, b ∈ s
obtain : ∀ (t : Finset β) (H : ∀ b ≥ t, b ∈ s), ∃ (a : Finset (α ⊕ β)), ∀ b ≥ a, b.toRight ∈ s
⊢ ∃ (a : Finset (α ⊕ β)), ∀ b ≥ a, b.toRight ∈ s

Tactic:
obtain ⟨t, H⟩ := hs
-- Module: Mathlib.Order.Filter.AtTopBot.Finset
Goal:
α : Type u_3
β : Type u_4
s : Set (Finset β)
t : Finset β
H : ∀ b ≥ t, b ∈ s
b : Finset (α ⊕ β)
hb : b ≥ Finset.disjSum ∅ t
⊢ b.toRight ≥ t

Tactic:
simpa [← Finset.coe_subset, Set.subset_def] using hb

Premises used: Set.subset_def, Finset.coe_subset
-- Module: Mathlib.Order.Filter.AtTopBot.Finset
Goal:
α : Type u_3
β : Type u_4
s : Set (Finset β)
t : Finset β
H : ∀ b ≥ t, b ∈ s
⊢ ∃ (a : Finset (α ⊕ β)), ∀ b ≥ a, b.toRight ∈ s

Tactic:
exact ⟨.disjSum ∅ t, fun b hb ↦ H _ (by simpa [← Finset.coe_subset, Set.subset_def] using hb)⟩
-- Module: Mathlib.Order.Filter.AtTopBot.Finset
Goal:
α : Type u_3
⊢ Tendsto.{u_3, u_3} (α := Finset α) Finset.powerset atTop atTop

Tactic:
tendsto_atTop_atTop.mpr fun t ↦ ⟨t.sup id, fun _ hu _ hv ↦ ?_⟩

Premises used: Iff.mpr, id, Filter.tendsto_atTop_atTop, Exists.intro, Finset.sup
-- Module: Mathlib.Order.Filter.AtTopBot.Finset
Goal:
α : Type u_3
refine : ∀ (t : Finset (Finset α)) (x : Finset α) (hu : t.sup id ≤ x) (x_1 : Finset α) (hv : x_1 ∈ t), x_1 ∈ x.powerset
⊢ Tendsto.{u_3, u_3} (α := Finset α) Finset.powerset atTop atTop

Tactic:
refine tendsto_atTop_atTop.mpr fun t ↦ ⟨t.sup id, fun _ hu _ hv ↦ ?_⟩

Premises used: Iff.mpr, Filter.tendsto_atTop_atTop, Exists.intro
-- Module: Mathlib.Order.Filter.AtTopBot.Finset
Goal:
α : Type u_3
t : Finset (Finset α)
x : Finset α
hu : t.sup id ≤ x
x_1 : Finset α
hv : x_1 ∈ t
⊢ x_1 ∈ x.powerset

Tactic:
Finset.mem_powerset.mpr <| (Finset.le_sup_of_le hv fun _ h ↦ h).trans hu

Premises used: Iff.mpr, Finset.mem_powerset, Finset.le_sup_of_le, LE.le.trans
-- Module: Mathlib.Order.Filter.AtTopBot.Finset
Goal:
α : Type u_3
t : Finset (Finset α)
x : Finset α
hu : t.sup id ≤ x
x_1 : Finset α
hv : x_1 ∈ t
⊢ x_1 ∈ x.powerset

Tactic:
exact Finset.mem_powerset.mpr <| (Finset.le_sup_of_le hv fun _ h ↦ h).trans hu

Premises used: Iff.mpr, Finset.mem_powerset, Finset.le_sup_of_le, LE.le.trans
-- Module: Mathlib.Order.Filter.AtTopBot.Finset
Goal:
α : Type u_3
refine : ∀ (t : Finset (Finset α)) (x : Finset α) (hu : t.sup id ≤ x) (x_1 : Finset α) (hv : x_1 ∈ t), x_1 ∈ x.powerset
⊢ Tendsto.{u_3, u_3} (α := Finset α) Finset.powerset atTop atTop

Tactic:
classical
  refine tendsto_atTop_atTop.mpr fun t ↦ ⟨t.sup id, fun _ hu _ hv ↦ ?_⟩
  exact Finset.mem_powerset.mpr <| (Finset.le_sup_of_le hv fun _ h ↦ h).trans hu

Premises used: Iff.mpr, Finset.mem_powerset, Filter.tendsto_atTop_atTop, Exists.intro
-- Module: Mathlib.Order.Filter.AtTopBot.Finset
Goal:
α : Type u_3
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
inl : IsEmpty α → Tendsto.{u_3, u_3} (α := α) Finset.Iic atTop atTop
inr : Nonempty α → Tendsto.{u_3, u_3} (α := α) Finset.Iic atTop atTop
⊢ Tendsto.{u_3, u_3} (α := α) Finset.Iic atTop atTop

Tactic:
rcases isEmpty_or_nonempty α with _ | _

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Order.Filter.AtTopBot.Finset
Goal:
α : Type u_3
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
h : IsEmpty α
⊢ Tendsto.{u_3, u_3} (α := α) Finset.Iic atTop atTop

Tactic:
tendsto_of_isEmpty

Premises used: Filter.tendsto_of_isEmpty
-- Module: Mathlib.Order.Filter.AtTopBot.Finset
Goal:
α : Type u_3
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
h : IsEmpty α
⊢ Tendsto.{u_3, u_3} (α := α) Finset.Iic atTop atTop

Tactic:
exact tendsto_of_isEmpty

Premises used: Filter.tendsto_of_isEmpty
-- Module: Mathlib.Order.Filter.AtTopBot.Finset
Goal:
α : Type u_3
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
h : Nonempty α
pos : ∀ (h : IsDirectedOrder α), Tendsto.{u_3, u_3} (α := α) Finset.Iic atTop atTop
neg : ∀ (h : ¬IsDirectedOrder α), Tendsto.{u_3, u_3} (α := α) Finset.Iic atTop atTop
⊢ Tendsto.{u_3, u_3} (α := α) Finset.Iic atTop atTop

Tactic:
by_cases h : IsDirectedOrder α

Premises used: IsDirectedOrder
-- Module: Mathlib.Order.Filter.AtTopBot.Finset
Goal:
α : Type u_3
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
h_1 : Nonempty α
h : IsDirectedOrder α
⊢ Tendsto.{u_3, u_3} (α := α) Finset.Iic atTop atTop

Tactic:
tendsto_atTop_atTop.mpr fun s ↦ ?_

Premises used: Iff.mpr, Filter.tendsto_atTop_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Finset
Goal:
α : Type u_3
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
h_1 : Nonempty α
h : IsDirectedOrder α
pos : ∀ (s : Finset α), ∃ (i : α), ∀ (a : α), i ≤ a → s ≤ Finset.Iic a
⊢ Tendsto.{u_3, u_3} (α := α) Finset.Iic atTop atTop

Tactic:
refine tendsto_atTop_atTop.mpr fun s ↦ ?_

Premises used: Iff.mpr, Filter.tendsto_atTop_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Finset
Goal:
α : Type u_3
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
h_1 : Nonempty α
h : IsDirectedOrder α
s : Finset α
pos : ∀ (a : α) (ha : ∀ i ∈ s, i ≤ a), ∃ (i : α), ∀ (a : α), i ≤ a → s ≤ Finset.Iic a
⊢ ∃ (i : α), ∀ (a : α), i ≤ a → s ≤ Finset.Iic a

Tactic:
obtain ⟨a, ha⟩ := Finset.exists_le s

Premises used: Finset.exists_le
-- Module: Mathlib.Order.Filter.AtTopBot.Finset
Goal:
α : Type u_3
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
h_1 : Nonempty α
h : IsDirectedOrder α
s : Finset α
a : α
ha : ∀ i ∈ s, i ≤ a
b : α
hb : a ≤ b
c : α
hc : c ∈ s
⊢ c ∈ Finset.Iic b

Tactic:
simpa using (ha c hc).trans hb

Premises used: LE.le.trans
-- Module: Mathlib.Order.Filter.AtTopBot.Finset
Goal:
α : Type u_3
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
h_1 : Nonempty α
h : IsDirectedOrder α
s : Finset α
a : α
ha : ∀ i ∈ s, i ≤ a
⊢ ∃ (i : α), ∀ (a : α), i ≤ a → s ≤ Finset.Iic a

Tactic:
exact ⟨a, fun b hb c hc ↦ by simpa using (ha c hc).trans hb⟩
-- Module: Mathlib.Order.Filter.AtTopBot.Finset
Goal:
α : Type u_3
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
h_1 : Nonempty α
h : ¬IsDirectedOrder α
⊢ ¬NeBot.{u_3} (α := α) atTop

Tactic:
obtain h := Filter.atTop_neBot_iff.not.mpr (fun h' ↦ h h'.2)

Premises used: Iff.mpr, Iff.not, And.right, Filter.atTop_neBot_iff
-- Module: Mathlib.Order.Filter.AtTopBot.Finset
Goal:
α : Type u_3
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
h_1 : Nonempty α
h_2 : ¬IsDirectedOrder α
h : ¬NeBot.{u_3} (α := α) atTop
⊢ Tendsto.{u_3, u_3} (α := α) Finset.Iic atTop atTop

Tactic:
simp [not_ne_iff.mp <| Filter.neBot_iff.not.mp h]

Premises used: Filter.neBot_iff, Iff.not, not_ne_iff, Iff.mp
-- Module: Mathlib.Order.Filter.AtTopBot.Finset
Goal:
α : Type u_3
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
⊢ Tendsto.{u_3, u_3} (α := α) Finset.Ici atBot atTop

Tactic:
tendsto_finset_Iic_atTop_atTop (α := αᵒᵈ)

Premises used: setOf, Finset.Ici, Filter.atBot, Set.Iic, OrderDual, Filter.tendsto_finset_Iic_atTop_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Finset
Goal:
α : Type u_3
i : Finset α
⊢ ∀ᶠ (s : Finset α) in atTop, i ⊆ s

Tactic:
eventually_ge_atTop _

Premises used: Filter.eventually_ge_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Finset
Goal:
α : Type u_3
i : α
⊢ ∀ᶠ (s : Finset α) in atTop, i ∈ s

Tactic:
simpa using eventually_finset_atTop_subset {i}

Premises used: Filter.eventually_finset_atTop_subset, Singleton.singleton
-- Module: Mathlib.Order.Filter.AtTopBot.Finset
Goal:
α : Type u_3
inst : Infinite α
rw :
  Eq (α := Filter ℕ) (⨅ (a : Finset α), 𝓟 (image.{u_3, 0} (α := Finset α) Finset.card {a' : Finset α | a ≤ a'}))
    (⨅ (a : ℕ), 𝓟 (Ici a))
⊢ map.{u_3, 0} (α := Finset α) Finset.card atTop = atTop

Tactic:
rw [map_atTop_eq, atTop]

Premises used: Filter.atTop, Filter.map_atTop_eq
-- Module: Mathlib.Order.Filter.AtTopBot.Finset
Goal:
α : Type u_3
inst : Infinite α
⊢ Eq (α := Filter ℕ) (⨅ (a : Finset α), 𝓟 (image.{u_3, 0} (α := Finset α) Finset.card {a' : Finset α | a ≤ a'}))
    (⨅ (a : ℕ), 𝓟 (Ici a))

Tactic:
Function.Surjective.iInf_congr Finset.card Finset.exists_card_eq fun s ↦ congr(𝓟 $(?_))

Premises used: congrArg, Finset.exists_card_eq, id, Finset.card, Filter.principal, Function.Surjective.iInf_congr
-- Module: Mathlib.Order.Filter.AtTopBot.Finset
Goal:
α : Type u_3
inst : Infinite α
refine : ∀ (s : Finset α), Ici s.card = image.{u_3, 0} (α := Finset α) Finset.card {a' : Finset α | s ≤ a'}
⊢ Eq (α := Filter ℕ) (⨅ (a : Finset α), 𝓟 (image.{u_3, 0} (α := Finset α) Finset.card {a' : Finset α | a ≤ a'}))
    (⨅ (a : ℕ), 𝓟 (Ici a))

Tactic:
refine Function.Surjective.iInf_congr Finset.card Finset.exists_card_eq fun s ↦ congr(𝓟 $(?_))
-- Module: Mathlib.Order.Filter.AtTopBot.Finset
Goal:
α : Type u_3
inst : Infinite α
s : Finset α
h : ∀ (x : ℕ), x ∈ Ici s.card ↔ x ∈ image.{u_3, 0} (α := Finset α) Finset.card {a' : Finset α | s ≤ a'}
⊢ Ici s.card = image.{u_3, 0} (α := Finset α) Finset.card {a' : Finset α | s ≤ a'}

Tactic:
ext
-- Module: Mathlib.Order.Filter.AtTopBot.Finset
Goal:
α : Type u_3
inst : Infinite α
s : Finset α
x : ℕ
⊢ x ∈ Ici s.card ↔ x ∈ image.{u_3, 0} (α := Finset α) Finset.card {a' : Finset α | s ≤ a'}

Tactic:
⟨Infinite.exists_superset_card_eq _ _, ?_⟩

Premises used: Infinite.exists_superset_card_eq, Iff.intro
-- Module: Mathlib.Order.Filter.AtTopBot.Finset
Goal:
α : Type u_3
inst : Infinite α
s : Finset α
x : ℕ
h : x ∈ image.{u_3, 0} (α := Finset α) Finset.card {a' : Finset α | s ≤ a'} → x ∈ Ici s.card
⊢ x ∈ Ici s.card ↔ x ∈ image.{u_3, 0} (α := Finset α) Finset.card {a' : Finset α | s ≤ a'}

Tactic:
refine ⟨Infinite.exists_superset_card_eq _ _, ?_⟩
-- Module: Mathlib.Order.Filter.AtTopBot.Finset
Goal:
α : Type u_3
inst : Infinite α
s : Finset α
x : ℕ
⊢ x ∈ image.{u_3, 0} (α := Finset α) Finset.card {a' : Finset α | s ≤ a'} → x ∈ Ici s.card

Tactic:
aesop (add safe apply Finset.card_le_card)

Premises used: Finset.card_le_card
-- Module: Mathlib.Order.Filter.AtTopBot.Finset
Goal:
α : Type u_3
inst : Fintype α
⊢ map.{u_3, 0} (α := Finset α) Finset.card atTop = pure (Fintype.card α)

Tactic:
simp [OrderTop.atTop_eq]

Premises used: Filter.OrderTop.atTop_eq
-- Module: Mathlib.Order.Filter.AtTopBot.Finset
Goal:
α : Type u_3
inst : Infinite α
rw : map.{u_3, 0} (α := Finset α) Finset.card atTop ≤ atTop
rw₁ rw₂ : LE.le (α := Filter ℕ) atTop atTop
⊢ Tendsto.{u_3, 0} (α := Finset α) Finset.card atTop atTop

Tactic:
rw [Tendsto, map_card_atTop]

Premises used: Filter.map_card_atTop, Filter.Tendsto
-- Module: Mathlib.Order.Filter.AtTopBot.Finset
Goal:
α : Type u_3
inst : Fintype α
rw : map.{u_3, 0} (α := Finset α) Finset.card atTop ≤ pure (Fintype.card α)
rw₁ rw₂ : LE.le (α := Filter ℕ) (pure (Fintype.card α)) (pure (Fintype.card α))
⊢ Tendsto.{u_3, 0} (α := Finset α) Finset.card atTop (pure (Fintype.card α))

Tactic:
rw [Tendsto, map_card_atTop_of_fintype]

Premises used: Filter.map_card_atTop_of_fintype, Filter.Tendsto
-- Module: Mathlib.Order.Filter.AtTopBot.Finset
Goal:
α : Type u_3
β : Type u_4
inst : Infinite α
f : ℕ → β
l : Filter β
rw : Tendsto (fun (s : Finset α) ↦ f s.card) atTop l ↔ Tendsto.{u_3, u_4} (α := Finset α) (f ∘ Finset.card) atTop l
⊢ Tendsto (fun (s : Finset α) ↦ f s.card) atTop l ↔ Tendsto f atTop l

Tactic:
rw [← map_card_atTop (α := α), tendsto_map'_iff]

Premises used: Filter.map_card_atTop, Filter.tendsto_map'_iff
-- Module: Mathlib.Order.Filter.AtTopBot.Finset
Goal:
α : Type u_3
β : Type u_4
inst : Infinite α
f : ℕ → β
l : Filter β
⊢ Tendsto (fun (s : Finset α) ↦ f s.card) atTop l ↔ Tendsto.{u_3, u_4} (α := Finset α) (f ∘ Finset.card) atTop l

Tactic:
rfl
-- Module: Mathlib.Order.Filter.AtTopBot.Finset
Goal:
α : Type u_3
β : Type u_4
inst : Fintype α
f : ℕ → β
l : Filter β
rw : Tendsto (fun (s : Finset α) ↦ f s.card) atTop l ↔ Tendsto.{u_3, u_4} (α := Finset α) (f ∘ Finset.card) atTop l
⊢ Tendsto (fun (s : Finset α) ↦ f s.card) atTop l ↔ Tendsto f (pure (Fintype.card α)) l

Tactic:
rw [← map_card_atTop_of_fintype, tendsto_map'_iff]

Premises used: Filter.map_card_atTop_of_fintype, Filter.tendsto_map'_iff
-- Module: Mathlib.Order.Filter.AtTopBot.Finset
Goal:
α : Type u_3
β : Type u_4
inst : Fintype α
f : ℕ → β
l : Filter β
⊢ Tendsto (fun (s : Finset α) ↦ f s.card) atTop l ↔ Tendsto.{u_3, u_4} (α := Finset α) (f ∘ Finset.card) atTop l

Tactic:
rfl
-- Module: Mathlib.Order.Filter.AtTopBot.Floor
Goal:
K : Type u_1
inst : Ring K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorSemiring K
a c : K
d : ℕ
h : ∀ (n : ℕ) (h : ⌈|a|⌉₊ * ⌈|c|⌉₊ ^ n < (n - d)!), a * c ^ n < (↑(n - d)! : K)
⊢ ∀ᶠ (n : ℕ) in atTop, a * c ^ n < (↑(n - d)! : K)

Tactic:
filter_upwards [Nat.eventually_mul_pow_lt_factorial_sub ⌈|a|⌉₊ ⌈|c|⌉₊ d] with n h

Premises used: abs, Nat.ceil, Nat.eventually_mul_pow_lt_factorial_sub
-- Module: Mathlib.Order.Filter.AtTopBot.Floor
Goal:
K : Type u_1
inst : Ring K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorSemiring K
a c : K
d n : ℕ
h : ⌈|a|⌉₊ * ⌈|c|⌉₊ ^ n < (n - d)!
⊢ a * c ^ n ≤ |a * c ^ n|

Tactic:
le_abs_self _

Premises used: le_abs_self
-- Module: Mathlib.Order.Filter.AtTopBot.Floor
Goal:
K : Type u_1
inst : Ring K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorSemiring K
a c : K
d n : ℕ
h : ⌈|a|⌉₊ * ⌈|c|⌉₊ ^ n < (n - d)!
⊢ |a * c ^ n| ≤ (↑⌈|a|⌉₊ : K) * HPow.hPow (α := K) (↑⌈|c|⌉₊ : K) n

Tactic:
?_
-- Module: Mathlib.Order.Filter.AtTopBot.Floor
Goal:
K : Type u_1
inst : Ring K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorSemiring K
a c : K
d n : ℕ
h : ⌈|a|⌉₊ * ⌈|c|⌉₊ ^ n < (n - d)!
⊢ (↑⌈|a|⌉₊ : K) * HPow.hPow (α := K) (↑⌈|c|⌉₊ : K) n = (↑(⌈|a|⌉₊ * ⌈|c|⌉₊ ^ n) : K)

Tactic:
?_
-- Module: Mathlib.Order.Filter.AtTopBot.Floor
Goal:
K : Type u_1
inst : Ring K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorSemiring K
a c : K
d n : ℕ
h : ⌈|a|⌉₊ * ⌈|c|⌉₊ ^ n < (n - d)!
⊢ LT.lt.{u_1} (α := K) (↑(⌈|a|⌉₊ * ⌈|c|⌉₊ ^ n) : K) (↑(n - d)! : K)

Tactic:
Nat.cast_lt.mpr h

Premises used: Iff.mpr, Nat.cast_lt
-- Module: Mathlib.Order.Filter.AtTopBot.Floor
Goal:
K : Type u_1
inst : Ring K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorSemiring K
a c : K
d n : ℕ
h : ⌈|a|⌉₊ * ⌈|c|⌉₊ ^ n < (n - d)!
h₁ : |a * c ^ n| ≤ (↑⌈|a|⌉₊ : K) * HPow.hPow (α := K) (↑⌈|c|⌉₊ : K) n
h₂ : (↑⌈|a|⌉₊ : K) * HPow.hPow (α := K) (↑⌈|c|⌉₊ : K) n = (↑(⌈|a|⌉₊ * ⌈|c|⌉₊ ^ n) : K)
⊢ a * c ^ n < (↑(n - d)! : K)

Tactic:
calc a * c ^ n
    _ ≤ |a * c ^ n| := le_abs_self _
    _ ≤ ⌈|a|⌉₊ * (⌈|c|⌉₊ : K) ^ n := ?_
    _ = ↑(⌈|a|⌉₊ * ⌈|c|⌉₊ ^ n) := ?_
    _ < (n - d)! := Nat.cast_lt.mpr h

Premises used: Iff.mpr, le_abs_self, HMul.hMul, abs, HSub.hSub, Nat.cast, HPow.hPow, Nat.ceil, Nat.cast_lt
-- Module: Mathlib.Order.Filter.AtTopBot.Floor
Goal:
K : Type u_1
inst : Ring K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorSemiring K
a c : K
d n : ℕ
h : ⌈|a|⌉₊ * ⌈|c|⌉₊ ^ n < (n - d)!
h₁ : |a| * |c| ^ n ≤ (↑⌈|a|⌉₊ : K) * HPow.hPow (α := K) (↑⌈|c|⌉₊ : K) n
⊢ |a * c ^ n| ≤ (↑⌈|a|⌉₊ : K) * HPow.hPow (α := K) (↑⌈|c|⌉₊ : K) n

Tactic:
rw [abs_mul, abs_pow]

Premises used: abs_mul, abs_pow
-- Module: Mathlib.Order.Filter.AtTopBot.Floor
Goal:
K : Type u_1
inst : Ring K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorSemiring K
a c : K
d n : ℕ
h : ⌈|a|⌉₊ * ⌈|c|⌉₊ ^ n < (n - d)!
h₁ : |a| ≤ (↑⌈|a|⌉₊ : K)
h₂ : |c| ≤ (↑⌈|c|⌉₊ : K)
⊢ |a| * |c| ^ n ≤ (↑⌈|a|⌉₊ : K) * HPow.hPow (α := K) (↑⌈|c|⌉₊ : K) n

Tactic:
gcongr
-- Module: Mathlib.Order.Filter.AtTopBot.Floor
Goal:
K : Type u_1
inst : Ring K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorSemiring K
a c : K
d n : ℕ
h : ⌈|a|⌉₊ * ⌈|c|⌉₊ ^ n < (n - d)!
⊢ |a| ≤ (↑⌈|a|⌉₊ : K)

Tactic:
apply Nat.le_ceil

Premises used: Nat.le_ceil
-- Module: Mathlib.Order.Filter.AtTopBot.Floor
Goal:
K : Type u_1
inst : Ring K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorSemiring K
a c : K
d n : ℕ
h : ⌈|a|⌉₊ * ⌈|c|⌉₊ ^ n < (n - d)!
⊢ |a| ≤ (↑⌈|a|⌉₊ : K)

Tactic:
first | positivity | apply Nat.le_ceil

Premises used: Nat.le_ceil
-- Module: Mathlib.Order.Filter.AtTopBot.Floor
Goal:
K : Type u_1
inst : Ring K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorSemiring K
a c : K
d n : ℕ
h : ⌈|a|⌉₊ * ⌈|c|⌉₊ ^ n < (n - d)!
⊢ |a| ≤ (↑⌈|a|⌉₊ : K)

Tactic:
try first | positivity | apply Nat.le_ceil

Premises used: Nat.le_ceil
-- Module: Mathlib.Order.Filter.AtTopBot.Floor
Goal:
K : Type u_1
inst : Ring K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorSemiring K
a c : K
d n : ℕ
h : ⌈|a|⌉₊ * ⌈|c|⌉₊ ^ n < (n - d)!
⊢ |c| ≤ (↑⌈|c|⌉₊ : K)

Tactic:
apply Nat.le_ceil

Premises used: Nat.le_ceil
-- Module: Mathlib.Order.Filter.AtTopBot.Floor
Goal:
K : Type u_1
inst : Ring K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorSemiring K
a c : K
d n : ℕ
h : ⌈|a|⌉₊ * ⌈|c|⌉₊ ^ n < (n - d)!
⊢ |c| ≤ (↑⌈|c|⌉₊ : K)

Tactic:
first | positivity | apply Nat.le_ceil

Premises used: Nat.le_ceil
-- Module: Mathlib.Order.Filter.AtTopBot.Floor
Goal:
K : Type u_1
inst : Ring K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorSemiring K
a c : K
d n : ℕ
h : ⌈|a|⌉₊ * ⌈|c|⌉₊ ^ n < (n - d)!
⊢ |c| ≤ (↑⌈|c|⌉₊ : K)

Tactic:
try first | positivity | apply Nat.le_ceil

Premises used: Nat.le_ceil
-- Module: Mathlib.Order.Filter.AtTopBot.Floor
Goal:
K : Type u_1
inst : Ring K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorSemiring K
a c : K
d n : ℕ
h : ⌈|a|⌉₊ * ⌈|c|⌉₊ ^ n < (n - d)!
h₁ : (↑⌈|a|⌉₊ : K) * HPow.hPow (α := K) (↑⌈|c|⌉₊ : K) n = HMul.hMul (α := K) (↑⌈|a|⌉₊ : K) (↑(⌈|c|⌉₊ ^ n) : K)
⊢ (↑⌈|a|⌉₊ : K) * HPow.hPow (α := K) (↑⌈|c|⌉₊ : K) n = (↑(⌈|a|⌉₊ * ⌈|c|⌉₊ ^ n) : K)

Tactic:
simp_rw [Nat.cast_mul, Nat.cast_pow]

Premises used: Nat.cast_mul, Nat.cast_pow
-- Module: Mathlib.Order.Filter.AtTopBot.Group
Goal:
α : Type u_1
G : Type u_2
inst : CommGroup G
inst_1 : PartialOrder G
inst_2 : IsOrderedMonoid G
l : Filter α
f g : α → G
C : G
hf : ∀ᶠ (x : α) in l, C ≤ f x
hg : Tendsto g l atTop
⊢ ∀ᶠ (x : G) in map f⁻¹ l, (fun (x1 x2 : G) ↦ x1 ≤ x2) x C⁻¹

Tactic:
simpa
-- Module: Mathlib.Order.Filter.AtTopBot.Group
Goal:
α : Type u_1
G : Type u_2
inst : CommGroup G
inst_1 : PartialOrder G
inst_2 : IsOrderedMonoid G
l : Filter α
f g : α → G
C : G
hf : ∀ᶠ (x : α) in l, C ≤ f x
hg : Tendsto g l atTop
⊢ Tendsto.{u_1, u_2} (β := G) (fun (x : α) ↦ f⁻¹ x * (f x * g x)) l atTop

Tactic:
simpa
-- Module: Mathlib.Order.Filter.AtTopBot.Group
Goal:
α : Type u_1
G : Type u_2
inst : CommGroup G
inst_1 : PartialOrder G
inst_2 : IsOrderedMonoid G
l : Filter α
f g : α → G
C : G
hf : ∀ᶠ (x : α) in l, f x ≤ C
hg : Tendsto g l atBot
⊢ Tendsto.{u_1, u_2} (β := G) (fun (x : α) ↦ f x * g x) l atBot

Tactic:
tendsto_atTop_mul_left_of_le' (G := Gᵒᵈ) _ C hf hg

Premises used: setOf, Filter.atBot, Set.Iic, Filter.tendsto_atTop_mul_left_of_le', OrderDual
-- Module: Mathlib.Order.Filter.AtTopBot.Group
Goal:
α : Type u_1
G : Type u_2
inst : CommGroup G
inst_1 : PartialOrder G
inst_2 : IsOrderedMonoid G
l : Filter α
f g : α → G
C : G
hf : ∀ (x : α), C ≤ f x
hg : Tendsto g l atTop
⊢ Tendsto.{u_1, u_2} (β := G) (fun (x : α) ↦ f x * g x) l atTop

Tactic:
tendsto_atTop_mul_left_of_le' l C (univ_mem' hf) hg

Premises used: Filter.tendsto_atTop_mul_left_of_le', Filter.univ_mem'
-- Module: Mathlib.Order.Filter.AtTopBot.Group
Goal:
α : Type u_1
G : Type u_2
inst : CommGroup G
inst_1 : PartialOrder G
inst_2 : IsOrderedMonoid G
l : Filter α
f g : α → G
C : G
hf : ∀ (x : α), f x ≤ C
hg : Tendsto g l atBot
⊢ Tendsto.{u_1, u_2} (β := G) (fun (x : α) ↦ f x * g x) l atBot

Tactic:
tendsto_atTop_mul_left_of_le (G := Gᵒᵈ) _ C hf hg

Premises used: setOf, Filter.tendsto_atTop_mul_left_of_le, Filter.atBot, Set.Iic, OrderDual
-- Module: Mathlib.Order.Filter.AtTopBot.Group
Goal:
α : Type u_1
G : Type u_2
inst : CommGroup G
inst_1 : PartialOrder G
inst_2 : IsOrderedMonoid G
l : Filter α
f g : α → G
C : G
hf : Tendsto f l atTop
hg : ∀ᶠ (x : α) in l, C ≤ g x
⊢ ∀ᶠ (x : G) in map g⁻¹ l, (fun (x1 x2 : G) ↦ x1 ≤ x2) x C⁻¹

Tactic:
simpa
-- Module: Mathlib.Order.Filter.AtTopBot.Group
Goal:
α : Type u_1
G : Type u_2
inst : CommGroup G
inst_1 : PartialOrder G
inst_2 : IsOrderedMonoid G
l : Filter α
f g : α → G
C : G
hf : Tendsto f l atTop
hg : ∀ᶠ (x : α) in l, C ≤ g x
⊢ Tendsto.{u_1, u_2} (β := G) (fun (x : α) ↦ f x * g x * g⁻¹ x) l atTop

Tactic:
simpa
-- Module: Mathlib.Order.Filter.AtTopBot.Group
Goal:
α : Type u_1
G : Type u_2
inst : CommGroup G
inst_1 : PartialOrder G
inst_2 : IsOrderedMonoid G
l : Filter α
f g : α → G
C : G
hf : Tendsto f l atBot
hg : ∀ᶠ (x : α) in l, g x ≤ C
⊢ Tendsto.{u_1, u_2} (β := G) (fun (x : α) ↦ f x * g x) l atBot

Tactic:
tendsto_atTop_mul_right_of_le' (G := Gᵒᵈ) _ C hf hg

Premises used: setOf, Filter.tendsto_atTop_mul_right_of_le', Filter.atBot, Set.Iic, OrderDual
-- Module: Mathlib.Order.Filter.AtTopBot.Group
Goal:
α : Type u_1
G : Type u_2
inst : CommGroup G
inst_1 : PartialOrder G
inst_2 : IsOrderedMonoid G
l : Filter α
f g : α → G
C : G
hf : Tendsto f l atTop
hg : ∀ (x : α), C ≤ g x
⊢ Tendsto.{u_1, u_2} (β := G) (fun (x : α) ↦ f x * g x) l atTop

Tactic:
tendsto_atTop_mul_right_of_le' l C hf (univ_mem' hg)

Premises used: Filter.tendsto_atTop_mul_right_of_le', Filter.univ_mem'
-- Module: Mathlib.Order.Filter.AtTopBot.Group
Goal:
α : Type u_1
G : Type u_2
inst : CommGroup G
inst_1 : PartialOrder G
inst_2 : IsOrderedMonoid G
l : Filter α
f g : α → G
C : G
hf : Tendsto f l atBot
hg : ∀ (x : α), g x ≤ C
⊢ Tendsto.{u_1, u_2} (β := G) (fun (x : α) ↦ f x * g x) l atBot

Tactic:
tendsto_atTop_mul_right_of_le (G := Gᵒᵈ) _ C hf hg

Premises used: setOf, Filter.atBot, Set.Iic, OrderDual, Filter.tendsto_atTop_mul_right_of_le
-- Module: Mathlib.Order.Filter.AtTopBot.Group
Goal:
α : Type u_1
G : Type u_2
inst : CommGroup G
inst_1 : PartialOrder G
inst_2 : IsOrderedMonoid G
l : Filter α
f : α → G
C : G
hf : Tendsto f l atTop
⊢ Tendsto.{u_1, u_2} (β := G) (fun (x : α) ↦ C * f x) l atTop

Tactic:
tendsto_atTop_mul_left_of_le' l C (univ_mem' fun _ => le_refl C) hf

Premises used: le_refl, Filter.tendsto_atTop_mul_left_of_le', Filter.univ_mem'
-- Module: Mathlib.Order.Filter.AtTopBot.Group
Goal:
α : Type u_1
G : Type u_2
inst : CommGroup G
inst_1 : PartialOrder G
inst_2 : IsOrderedMonoid G
l : Filter α
f : α → G
C : G
hf : Tendsto f l atBot
⊢ Tendsto.{u_1, u_2} (β := G) (fun (x : α) ↦ C * f x) l atBot

Tactic:
tendsto_atTop_mul_const_left (G := Gᵒᵈ) _ C hf

Premises used: setOf, Filter.tendsto_atTop_mul_const_left, Filter.atBot, Set.Iic, OrderDual
-- Module: Mathlib.Order.Filter.AtTopBot.Group
Goal:
α : Type u_1
G : Type u_2
inst : CommGroup G
inst_1 : PartialOrder G
inst_2 : IsOrderedMonoid G
l : Filter α
f : α → G
C : G
hf : Tendsto f l atTop
⊢ Tendsto.{u_1, u_2} (β := G) (fun (x : α) ↦ f x * C) l atTop

Tactic:
tendsto_atTop_mul_right_of_le' l C hf (univ_mem' fun _ => le_refl C)

Premises used: le_refl, Filter.tendsto_atTop_mul_right_of_le', Filter.univ_mem'
-- Module: Mathlib.Order.Filter.AtTopBot.Group
Goal:
α : Type u_1
G : Type u_2
inst : CommGroup G
inst_1 : PartialOrder G
inst_2 : IsOrderedMonoid G
l : Filter α
f : α → G
C : G
hf : Tendsto f l atBot
⊢ Tendsto.{u_1, u_2} (β := G) (fun (x : α) ↦ f x * C) l atBot

Tactic:
tendsto_atTop_mul_const_right (G := Gᵒᵈ) _ C hf

Premises used: Filter.tendsto_atTop_mul_const_right, setOf, Filter.atBot, Set.Iic, OrderDual
-- Module: Mathlib.Order.Filter.AtTopBot.Group
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : PartialOrder G
inst_2 : IsOrderedMonoid G
⊢ Eq.{u_2 + 1} (α := Filter G) (map Inv.inv atBot) atTop

Tactic:
(OrderIso.inv G).map_atBot

Premises used: Set.Ici, OrderIso.inv, setOf, OrderIso.map_atBot, Filter.atTop, OrderDual