awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finite (goal)
Goal:
c d d' : ℕ
hn : 2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d' ≥ 2 * (HPow.hPow (β := ℕ) c 2 + d + 1)
inl :
  ∀ (hn : 2 * (HPow.hPow (α := ℕ) (β := ℕ) 0 2 + d + 1) + d' ≥ 2 * (HPow.hPow (α := ℕ) (β := ℕ) 0 2 + d + 1)),
    HPow.hPow (α := ℕ) 0 (2 * (HPow.hPow (α := ℕ) (β := ℕ) 0 2 + d + 1) + d') <
      (2 * (HPow.hPow (α := ℕ) (β := ℕ) 0 2 + d + 1) + d' - d)!
⊢ c ^ (2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d') < (2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d' - d)!
have inr : ∀ (c0 : c > 0), c ^ (2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d') < (2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d' - d)!
Tactic: obtain (rfl | c0) := c.eq_zero_or_pos
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finite (goal)
Goal:
c d d' : ℕ
hn : 2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d' ≥ 2 * (HPow.hPow (β := ℕ) c 2 + d + 1)
c0 : c > 0
⊢ c ^ (2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d') < (2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d' - d)!
have inr : c ^ (2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d') * c ^ d' < (2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d' - d)!
Tactic: refine (Nat.le_mul_of_pos_right _ (Nat.pow_pos (n := d') c0)).trans_lt ?_
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finite (goal)
Goal:
c d d' : ℕ
hn : 2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d' ≥ 2 * (HPow.hPow (β := ℕ) c 2 + d + 1)
c0 : c > 0
⊢ c ^ (2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d') * c ^ d' < (2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d' - d)!
have h : c ^ (2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d') * c ^ d' =
  HPow.hPow (β := ℕ) c 2 ^ (HPow.hPow (β := ℕ) c 2 + d' + d + 1)
Tactic: convert_to (c ^ 2) ^ (c ^ 2 + d' + d + 1) < (c ^ 2 + (c ^ 2 + d' + d + 1) + 1)!
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finite (goal)
Goal:
c d d' : ℕ
hn : 2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d' ≥ 2 * (HPow.hPow (β := ℕ) c 2 + d + 1)
c0 : c > 0
h :
  c ^ (2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d') * c ^ d' =
    HPow.hPow (β := ℕ) c 2 ^ (HPow.hPow (β := ℕ) c 2 + d' + d + 1)
⊢ c ^ (2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d') * c ^ d' < (2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d' - d)!
have h₁ : (2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d' - d)! = (HPow.hPow (β := ℕ) c 2 + (HPow.hPow (β := ℕ) c 2 + d' + d + 1) + 1)!
Tactic: convert_to (c ^ 2) ^ (c ^ 2 + d' + d + 1) < (c ^ 2 + (c ^ 2 + d' + d + 1) + 1)!
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finite (goal)
Goal:
c d d' : ℕ
hn : 2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d' ≥ 2 * (HPow.hPow (β := ℕ) c 2 + d + 1)
c0 : c > 0
h :
  c ^ (2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d') * c ^ d' =
    HPow.hPow (β := ℕ) c 2 ^ (HPow.hPow (β := ℕ) c 2 + d' + d + 1)
h₁ :
  (2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d' - d)! =
    (HPow.hPow (β := ℕ) c 2 + (HPow.hPow (β := ℕ) c 2 + d' + d + 1) + 1)!
⊢ c ^ (2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d') * c ^ d' < (2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d' - d)!
have inr : HPow.hPow (β := ℕ) c 2 ^ (HPow.hPow (β := ℕ) c 2 + d' + d + 1) <
  (HPow.hPow (β := ℕ) c 2 + (HPow.hPow (β := ℕ) c 2 + d' + d + 1) + 1)!
Tactic: convert_to (c ^ 2) ^ (c ^ 2 + d' + d + 1) < (c ^ 2 + (c ^ 2 + d' + d + 1) + 1)!
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finite (goal)
Goal:
c d d' : ℕ
hn : 2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d' ≥ 2 * (HPow.hPow (β := ℕ) c 2 + d + 1)
c0 : c > 0
⊢ c ^ (2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d') * c ^ d' =
    HPow.hPow (β := ℕ) c 2 ^ (HPow.hPow (β := ℕ) c 2 + d' + d + 1)
have h : c ^ (2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d' + d') = c ^ (2 * (HPow.hPow (β := ℕ) c 2 + d' + d + 1))
Tactic: rw [← pow_mul, ← pow_add]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finite (goal)
Goal:
c d d' : ℕ
hn : 2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d' ≥ 2 * (HPow.hPow (β := ℕ) c 2 + d + 1)
c0 : c > 0
⊢ c ^ (2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d' + d') = c ^ (2 * (HPow.hPow (β := ℕ) c 2 + d' + d + 1))
have h : 2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d' + d' = 2 * (HPow.hPow (β := ℕ) c 2 + d' + d + 1)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finite (goal)
Goal:
c d d' : ℕ
hn : 2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d' ≥ 2 * (HPow.hPow (β := ℕ) c 2 + d + 1)
c0 : c > 0
⊢ (2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d' - d)! =
    (HPow.hPow (β := ℕ) c 2 + (HPow.hPow (β := ℕ) c 2 + d' + d + 1) + 1)!
have h : 2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d' - d = HPow.hPow (β := ℕ) c 2 + (HPow.hPow (β := ℕ) c 2 + d' + d + 1) + 1
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finite (goal)
Goal:
c d d' : ℕ
hn : 2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d' ≥ 2 * (HPow.hPow (β := ℕ) c 2 + d + 1)
c0 : c > 0
⊢ HPow.hPow (β := ℕ) c 2 ^ (HPow.hPow (β := ℕ) c 2 + d' + d + 1) <
    (HPow.hPow (β := ℕ) c 2 + (HPow.hPow (β := ℕ) c 2 + d' + d + 1) + 1)!
have inr : HPow.hPow (β := ℕ) c 2 ^ (HPow.hPow (β := ℕ) c 2 + d' + d + 1) <
  (HPow.hPow (β := ℕ) c 2)! * (HPow.hPow (β := ℕ) c 2 + 1) ^ (HPow.hPow (β := ℕ) c 2 + d' + d + 1)
Tactic: refine (lt_of_lt_of_le ?_ Nat.factorial_mul_pow_le_factorial).trans_le <|
    (factorial_le (Nat.le_succ _))
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finite (goal)
Goal:
c d d' : ℕ
hn : 2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d' ≥ 2 * (HPow.hPow (β := ℕ) c 2 + d + 1)
c0 : c > 0
⊢ HPow.hPow (β := ℕ) c 2 ^ (HPow.hPow (β := ℕ) c 2 + d' + d + 1) <
    (HPow.hPow (β := ℕ) c 2)! * (HPow.hPow (β := ℕ) c 2 + 1) ^ (HPow.hPow (β := ℕ) c 2 + d' + d + 1)
have inr : 1 * HPow.hPow (β := ℕ) c 2 ^ (HPow.hPow (β := ℕ) c 2 + d' + d + 1) <
  (HPow.hPow (β := ℕ) c 2)! * (HPow.hPow (β := ℕ) c 2 + 1) ^ (HPow.hPow (β := ℕ) c 2 + d' + d + 1)
Tactic: rw [← one_mul (_ ^ _ : ℕ)]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finite (goal)
Goal:
c d d' : ℕ
hn : 2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d' ≥ 2 * (HPow.hPow (β := ℕ) c 2 + d + 1)
c0 : c > 0
⊢ 1 * HPow.hPow (β := ℕ) c 2 ^ (HPow.hPow (β := ℕ) c 2 + d' + d + 1) <
    (HPow.hPow (β := ℕ) c 2)! * (HPow.hPow (β := ℕ) c 2 + 1) ^ (HPow.hPow (β := ℕ) c 2 + d' + d + 1)
have inr : 1 ≤ (HPow.hPow (β := ℕ) c 2)!
Tactic: apply Nat.mul_lt_mul_of_le_of_lt
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finite (goal)
Goal:
c d d' : ℕ
hn : 2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d' ≥ 2 * (HPow.hPow (β := ℕ) c 2 + d + 1)
c0 : c > 0
inr : 1 ≤ (HPow.hPow (β := ℕ) c 2)!
⊢ 1 * HPow.hPow (β := ℕ) c 2 ^ (HPow.hPow (β := ℕ) c 2 + d' + d + 1) <
    (HPow.hPow (β := ℕ) c 2)! * (HPow.hPow (β := ℕ) c 2 + 1) ^ (HPow.hPow (β := ℕ) c 2 + d' + d + 1)
have inr₁ : HPow.hPow (β := ℕ) c 2 ^ (HPow.hPow (β := ℕ) c 2 + d' + d + 1) <
  (HPow.hPow (β := ℕ) c 2 + 1) ^ (HPow.hPow (β := ℕ) c 2 + d' + d + 1)
Tactic: apply Nat.mul_lt_mul_of_le_of_lt
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finite (goal)
Goal:
c d d' : ℕ
hn : 2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d' ≥ 2 * (HPow.hPow (β := ℕ) c 2 + d + 1)
c0 : c > 0
inr : 1 ≤ (HPow.hPow (β := ℕ) c 2)!
inr₁ :
  HPow.hPow (β := ℕ) c 2 ^ (HPow.hPow (β := ℕ) c 2 + d' + d + 1) <
    (HPow.hPow (β := ℕ) c 2 + 1) ^ (HPow.hPow (β := ℕ) c 2 + d' + d + 1)
⊢ 1 * HPow.hPow (β := ℕ) c 2 ^ (HPow.hPow (β := ℕ) c 2 + d' + d + 1) <
    (HPow.hPow (β := ℕ) c 2)! * (HPow.hPow (β := ℕ) c 2 + 1) ^ (HPow.hPow (β := ℕ) c 2 + d' + d + 1)
have inr₂ : 0 < (HPow.hPow (β := ℕ) c 2)!
Tactic: apply Nat.mul_lt_mul_of_le_of_lt
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finite (goal)
Goal:
a c d : ℕ
⊢ ∀ᶠ (n : ℕ) in atTop, a * c ^ n < (n - d)!
have h : ∀ (n : ℕ) (hn : (a * c) ^ n < (n - d)!) (hn0 : 0 < n), a * c ^ n < (n - d)!
Tactic: filter_upwards [Nat.eventually_pow_lt_factorial_sub (a * c) d, Filter.eventually_gt_atTop 0]
    with n hn hn0
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finite (hypothesis)
Goal:
a c d n : ℕ
hn : (a * c) ^ n < (n - d)!
hn0 : 0 < n
⊢ a * c ^ n < (n - d)!
have hn₁ : a ^ n * c ^ n < (n - d)!
Tactic: rw [mul_pow] at hn
Cleared hypotheses: hn, hn0
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finset (goal)
Goal:
α : Type u_3
⊢ Eq.{u_3 + 1} (α := Filter (Finset α)) atTop (⨅ (x : α), 𝓟 (Ici {x}))
have refine : LE.le.{u_3} (α := Filter (Finset α)) (⨅ (x : α), 𝓟 (Ici {x})) atTop
Tactic: refine le_antisymm (le_iInf fun i => le_principal_iff.2 <| mem_atTop ({i} : Finset α)) ?_
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finset (goal)
Goal:
α : Type u_3
⊢ LE.le.{u_3} (α := Filter (Finset α)) (⨅ (x : α), 𝓟 (Ici {x})) atTop
have le_iInf : ∀ (s : Finset α), ⋂ (i : (↑(↑s : Set α) : Type u_3)), Ici {(↑i : α)} ⊆ Ici s
Tactic: refine
    le_iInf fun s =>
      le_principal_iff.2 <| mem_iInf_of_iInter s.finite_toSet (fun i => mem_principal_self _) ?_
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finset (goal)
Goal:
α : Type u_3
s : Finset α
⊢ ⋂ (i : (↑(↑s : Set α) : Type u_3)), Ici {(↑i : α)} ⊆ Ici s
have simp : ∀ (x : Finset α), (∀ (x_1 : α) (h : x_1 ∈ (↑s : Set α)), x_1 ∈ x) → ∀ ⦃x_1 : α⦄, x_1 ∈ s → x_1 ∈ x
Tactic: simp only [subset_def, mem_iInter, SetCoe.forall, mem_Ici, Finset.le_iff_subset,
    Finset.mem_singleton, Finset.subset_iff, forall_eq]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finset (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Preorder β
f : β → Finset α
h : Monotone f
h' : ∀ (x : α), ∃ (n : β), x ∈ f n
⊢ Tendsto f atTop atTop
have simp : ∀ (i : α), ∀ᶠ (a : β) in atTop, Membership.mem (γ := Set (Finset α)) (Ici {i}) (f a)
Tactic: simp only [atTop_finset_eq_iInf, tendsto_iInf, tendsto_principal]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finset (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Preorder β
f : β → Finset α
h : Monotone f
h' : ∀ (x : α), ∃ (n : β), x ∈ f n
a : α
⊢ ∀ᶠ (a_1 : β) in atTop, Membership.mem (γ := Set (Finset α)) (Ici {a}) (f a_1)
have rcases : ∀ (b : β) (hb : a ∈ f b), ∀ᶠ (a_1 : β) in atTop, Membership.mem (γ := Set (Finset α)) (Ici {a}) (f a_1)
Tactic: rcases h' a with ⟨b, hb⟩
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finset (goal)
Goal:
α : Type u_3
β : Type u_4
s : Set (Finset α)
hs : Membership.mem (γ := Filter (Finset α)) atTop s
⊢ Membership.mem (γ := Filter (Finset α)) (map (α := Finset (α ⊕ β)) Finset.toLeft atTop) s
have simp : ∀ (hs : ∃ (a : Finset α), ∀ b ≥ a, b ∈ s), ∃ (a : Finset (α ⊕ β)), ∀ b ≥ a, b.toLeft ∈ s
Tactic: simp only [mem_atTop_sets, Filter.mem_map, Set.mem_preimage] at hs ⊢
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finset (goal)
Goal:
α : Type u_3
β : Type u_4
s : Set (Finset α)
hs : ∃ (a : Finset α), ∀ b ≥ a, b ∈ s
⊢ ∃ (a : Finset (α ⊕ β)), ∀ b ≥ a, b.toLeft ∈ s
have obtain : ∀ (t : Finset α) (H : ∀ b ≥ t, b ∈ s), ∃ (a : Finset (α ⊕ β)), ∀ b ≥ a, b.toLeft ∈ s
Tactic: obtain ⟨t, H⟩ := hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finset (goal)
Goal:
α : Type u_3
β : Type u_4
s : Set (Finset β)
hs : Membership.mem (γ := Filter (Finset β)) atTop s
⊢ Membership.mem (γ := Filter (Finset β)) (map (α := Finset (α ⊕ β)) Finset.toRight atTop) s
have simp : ∀ (hs : ∃ (a : Finset β), ∀ b ≥ a, b ∈ s), ∃ (a : Finset (α ⊕ β)), ∀ b ≥ a, b.toRight ∈ s
Tactic: simp only [mem_atTop_sets, Filter.mem_map, Set.mem_preimage] at hs ⊢
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finset (goal)
Goal:
α : Type u_3
β : Type u_4
s : Set (Finset β)
hs : ∃ (a : Finset β), ∀ b ≥ a, b ∈ s
⊢ ∃ (a : Finset (α ⊕ β)), ∀ b ≥ a, b.toRight ∈ s
have obtain : ∀ (t : Finset β) (H : ∀ b ≥ t, b ∈ s), ∃ (a : Finset (α ⊕ β)), ∀ b ≥ a, b.toRight ∈ s
Tactic: obtain ⟨t, H⟩ := hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finset (goal)
Goal:
α : Type u_3
⊢ Tendsto.{u_3, u_3} (α := Finset α) Finset.powerset atTop atTop
have refine : ∀ (t : Finset (Finset α)) (x : Finset α) (hu : t.sup id ≤ x) (x_1 : Finset α) (hv : x_1 ∈ t), x_1 ∈ x.powerset
Tactic: refine tendsto_atTop_atTop.mpr fun t ↦ ⟨t.sup id, fun _ hu _ hv ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finset (goal)
Goal:
α : Type u_3
⊢ Tendsto.{u_3, u_3} (α := Finset α) Finset.powerset atTop atTop
have refine : ∀ (t : Finset (Finset α)) (x : Finset α) (hu : t.sup id ≤ x) (x_1 : Finset α) (hv : x_1 ∈ t), x_1 ∈ x.powerset
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
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finset (goal)
Goal:
α : Type u_3
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
⊢ Tendsto.{u_3, u_3} (α := α) Finset.Iic atTop atTop
have inl : IsEmpty α → Tendsto.{u_3, u_3} (α := α) Finset.Iic atTop atTop
Tactic: rcases isEmpty_or_nonempty α with _ | _
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finset (goal)
Goal:
α : Type u_3
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
inl : IsEmpty α → Tendsto.{u_3, u_3} (α := α) Finset.Iic atTop atTop
⊢ Tendsto.{u_3, u_3} (α := α) Finset.Iic atTop atTop
have inr : Nonempty α → Tendsto.{u_3, u_3} (α := α) Finset.Iic atTop atTop
Tactic: rcases isEmpty_or_nonempty α with _ | _
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finset (goal)
Goal:
α : Type u_3
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
h : Nonempty α
⊢ Tendsto.{u_3, u_3} (α := α) Finset.Iic atTop atTop
have pos : ∀ (h : IsDirectedOrder α), Tendsto.{u_3, u_3} (α := α) Finset.Iic atTop atTop
Tactic: by_cases h : IsDirectedOrder α
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finset (goal)
Goal:
α : Type u_3
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
h : Nonempty α
pos : ∀ (h : IsDirectedOrder α), Tendsto.{u_3, u_3} (α := α) Finset.Iic atTop atTop
⊢ Tendsto.{u_3, u_3} (α := α) Finset.Iic atTop atTop
have neg : ∀ (h : ¬IsDirectedOrder α), Tendsto.{u_3, u_3} (α := α) Finset.Iic atTop atTop
Tactic: by_cases h : IsDirectedOrder α
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finset (goal)
Goal:
α : Type u_3
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
h_1 : Nonempty α
h : IsDirectedOrder α
⊢ Tendsto.{u_3, u_3} (α := α) Finset.Iic atTop atTop
have pos : ∀ (s : Finset α), ∃ (i : α), ∀ (a : α), i ≤ a → s ≤ Finset.Iic a
Tactic: refine tendsto_atTop_atTop.mpr fun s ↦ ?_
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finset (goal)
Goal:
α : Type u_3
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
h_1 : Nonempty α
h : IsDirectedOrder α
s : Finset α
⊢ ∃ (i : α), ∀ (a : α), i ≤ a → s ≤ Finset.Iic a
have pos : ∀ (a : α) (ha : ∀ i ∈ s, i ≤ a), ∃ (i : α), ∀ (a : α), i ≤ a → s ≤ Finset.Iic a
Tactic: obtain ⟨a, ha⟩ := Finset.exists_le s
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finset (hypothesis)
Goal:
α : Type u_3
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
h_1 : Nonempty α
h : ¬IsDirectedOrder α
⊢ Tendsto.{u_3, u_3} (α := α) Finset.Iic atTop atTop
have h₁ : ¬NeBot.{u_3} (α := α) atTop
Tactic: obtain h := Filter.atTop_neBot_iff.not.mpr (fun h' ↦ h h'.2)
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finset (goal)
Goal:
α : Type u_3
inst : Infinite α
⊢ map.{u_3, 0} (α := Finset α) Finset.card atTop = atTop
have rw : Eq (α := Filter ℕ) (⨅ (a : Finset α), 𝓟 (image.{u_3, 0} (α := Finset α) Finset.card {a' : Finset α | a ≤ a'}))
  (⨅ (a : ℕ), 𝓟 (Ici a))
Tactic: rw [map_atTop_eq, atTop]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finset (goal)
Goal:
α : Type u_3
inst : Infinite α
⊢ Eq (α := Filter ℕ) (⨅ (a : Finset α), 𝓟 (image.{u_3, 0} (α := Finset α) Finset.card {a' : Finset α | a ≤ a'}))
    (⨅ (a : ℕ), 𝓟 (Ici a))
have refine : ∀ (s : Finset α), Ici s.card = image.{u_3, 0} (α := Finset α) Finset.card {a' : Finset α | s ≤ a'}
Tactic: refine Function.Surjective.iInf_congr Finset.card Finset.exists_card_eq fun s ↦ congr(𝓟 $(?_))
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finset (goal)
Goal:
α : Type u_3
inst : Infinite α
s : Finset α
⊢ Ici s.card = image.{u_3, 0} (α := Finset α) Finset.card {a' : Finset α | s ≤ a'}
have h : ∀ (x : ℕ), x ∈ Ici s.card ↔ x ∈ image.{u_3, 0} (α := Finset α) Finset.card {a' : Finset α | s ≤ a'}
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finset (goal)
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'}
have h : x ∈ image.{u_3, 0} (α := Finset α) Finset.card {a' : Finset α | s ≤ a'} → x ∈ Ici s.card
Tactic: refine ⟨Infinite.exists_superset_card_eq _ _, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finset (goal)
Goal:
α : Type u_3
inst : Infinite α
⊢ Tendsto.{u_3, 0} (α := Finset α) Finset.card atTop atTop
have rw : map.{u_3, 0} (α := Finset α) Finset.card atTop ≤ atTop
Tactic: rw [Tendsto, map_card_atTop]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finset (goal)
Goal:
α : Type u_3
inst : Infinite α
rw : map.{u_3, 0} (α := Finset α) Finset.card atTop ≤ atTop
⊢ Tendsto.{u_3, 0} (α := Finset α) Finset.card atTop atTop
have rw₁ : LE.le (α := Filter ℕ) atTop atTop
Tactic: rw [Tendsto, map_card_atTop]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finset (goal)
Goal:
α : Type u_3
inst : Fintype α
⊢ Tendsto.{u_3, 0} (α := Finset α) Finset.card atTop (pure (Fintype.card α))
have rw : map.{u_3, 0} (α := Finset α) Finset.card atTop ≤ pure (Fintype.card α)
Tactic: rw [Tendsto, map_card_atTop_of_fintype]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finset (goal)
Goal:
α : Type u_3
inst : Fintype α
rw : map.{u_3, 0} (α := Finset α) Finset.card atTop ≤ pure (Fintype.card α)
⊢ Tendsto.{u_3, 0} (α := Finset α) Finset.card atTop (pure (Fintype.card α))
have rw₁ : LE.le (α := Filter ℕ) (pure (Fintype.card α)) (pure (Fintype.card α))
Tactic: rw [Tendsto, map_card_atTop_of_fintype]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finset (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Infinite α
f : ℕ → β
l : Filter β
⊢ Tendsto (fun (s : Finset α) ↦ f s.card) atTop l ↔ Tendsto f atTop l
have rw : Tendsto (fun (s : Finset α) ↦ f s.card) atTop l ↔ Tendsto.{u_3, u_4} (α := Finset α) (f ∘ Finset.card) atTop l
Tactic: rw [← map_card_atTop (α := α), tendsto_map'_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Finset (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Fintype α
f : ℕ → β
l : Filter β
⊢ Tendsto (fun (s : Finset α) ↦ f s.card) atTop l ↔ Tendsto f (pure (Fintype.card α)) l
have rw : Tendsto (fun (s : Finset α) ↦ f s.card) atTop l ↔ Tendsto.{u_3, u_4} (α := Finset α) (f ∘ Finset.card) atTop l
Tactic: rw [← map_card_atTop_of_fintype, tendsto_map'_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Floor (goal)
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 : ℕ) in atTop, a * c ^ n < (↑(n - d)! : K)
have h : ∀ (n : ℕ) (h : ⌈|a|⌉₊ * ⌈|c|⌉₊ ^ n < (n - d)!), a * c ^ n < (↑(n - d)! : K)
Tactic: filter_upwards [Nat.eventually_mul_pow_lt_factorial_sub ⌈|a|⌉₊ ⌈|c|⌉₊ d] with n h
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Floor (goal)
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 < (↑(n - d)! : K)
have h₁ : |a * c ^ n| ≤ (↑⌈|a|⌉₊ : K) * HPow.hPow (α := K) (↑⌈|c|⌉₊ : K) n
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
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Floor (goal)
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 < (↑(n - d)! : K)
have h₂ : (↑⌈|a|⌉₊ : K) * HPow.hPow (α := K) (↑⌈|c|⌉₊ : K) n = (↑(⌈|a|⌉₊ * ⌈|c|⌉₊ ^ n) : 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
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Floor (goal)
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
have h₁ : |a| * |c| ^ n ≤ (↑⌈|a|⌉₊ : K) * HPow.hPow (α := K) (↑⌈|c|⌉₊ : K) n
Tactic: rw [abs_mul, abs_pow]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Floor (goal)
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
have h₁ : |a| ≤ (↑⌈|a|⌉₊ : K)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Floor (goal)
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)
⊢ |a| * |c| ^ n ≤ (↑⌈|a|⌉₊ : K) * HPow.hPow (α := K) (↑⌈|c|⌉₊ : K) n
have h₂ : |c| ≤ (↑⌈|c|⌉₊ : K)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Floor (goal)
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)
have h₁ : (↑⌈|a|⌉₊ : K) * HPow.hPow (α := K) (↑⌈|c|⌉₊ : K) n = HMul.hMul (α := K) (↑⌈|a|⌉₊ : K) (↑(⌈|c|⌉₊ ^ n) : K)
Tactic: simp_rw [Nat.cast_mul, Nat.cast_pow]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Group (goal)
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
⊢ Eq.{u_2 + 1} (α := Filter G) (comap mabs atTop) (atBot ⊔ atTop)
have le_antisymm : ∀ (i' : G × G), True ∧ True → ∃ (i : G), True ∧ mabs ⁻¹' Ici i ⊆ Iic i'.1 ∪ Ici i'.2
Tactic: refine
    le_antisymm (((atTop_basis.comap _).le_basis_iff (atBot_basis.sup atTop_basis)).2 ?_)
      (sup_le tendsto_mabs_atBot_atTop.le_comap tendsto_mabs_atTop_atTop.le_comap)
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Group (goal)
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b : G
⊢ ∃ (i : G), True ∧ mabs ⁻¹' Ici i ⊆ Iic (a, b).1 ∪ Ici (a, b).2
have refine : ∀ (x : G) (hx : x ∈ mabs ⁻¹' Ici (max a⁻¹ b)), x ∈ Iic (a, b).1 ∪ Ici (a, b).2
Tactic: refine ⟨max (a⁻¹) b, trivial, fun x hx => ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Group (hypothesis)
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b x : G
hx : x ∈ mabs ⁻¹' Ici (max a⁻¹ b)
⊢ x ∈ Iic (a, b).1 ∪ Ici (a, b).2
have hx₁ : x ≤ a ∧ x ≤ b⁻¹ ∨ a⁻¹ ≤ x ∧ b ≤ x
Tactic: rw [mem_preimage, mem_Ici, le_mabs', max_le_iff, ← min_inv_inv', le_min_iff, inv_inv] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Map (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
e : α ≃o β
⊢ Eq.{u_4 + 1} (α := Filter β) (map.{u_3, u_4} (α := α) (⇑e : (a : α) → β) atTop) atTop
have rw : Eq.{u_4 + 1} (α := Filter β)
  (map.{u_3, u_4} (α := α) (⇑e : (a : α) → β) (comap.{u_3, u_4} (β := β) (⇑e : (a : α) → β) atTop)) atTop
Tactic: rw [← e.comap_atTop, map_comap_of_surjective e.surjective]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Map (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
e : α ≃o β
rw :
  Eq.{u_4 + 1} (α := Filter β)
    (map.{u_3, u_4} (α := α) (⇑e : (a : α) → β) (comap.{u_3, u_4} (β := β) (⇑e : (a : α) → β) atTop)) atTop
⊢ Eq.{u_4 + 1} (α := Filter β) (map.{u_3, u_4} (α := α) (⇑e : (a : α) → β) atTop) atTop
have rw₁ : Eq.{u_4 + 1} (α := Filter β) atTop atTop
Tactic: rw [← e.comap_atTop, map_comap_of_surjective e.surjective]
-- 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 β
⊢ 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 f l (comap.{u_3, u_4} (β := β) (⇑e : (a : α) → β) atTop)
Tactic: rw [← e.comap_atTop, tendsto_comap_iff, Function.comp_def]