awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
p : ℕ → Prop
n : ℕ
hn : n ≠ 0
N : (k : ℕ) → ℕ
hN : ∀ k < n, ∀ b ≥ N k, p (n * b + k)
b : ℕ
hb : b ≥ (Finset.range n).sup fun (x : ℕ) ↦ n * N x
hlt : b % n < n
⊢ p (n * (b / n) + b % n)

Tactic:
hN _ hlt _ ?_
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
p : ℕ → Prop
n : ℕ
hn : n ≠ 0
N : (k : ℕ) → ℕ
hN : ∀ k < n, ∀ b ≥ N k, p (n * b + k)
b : ℕ
hb : b ≥ (Finset.range n).sup fun (x : ℕ) ↦ n * N x
hlt : b % n < n
refine : b / n ≥ N (b % n)
⊢ p (n * (b / n) + b % n)

Tactic:
refine hN _ hlt _ ?_
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
p : ℕ → Prop
n : ℕ
hn : n ≠ 0
N : (k : ℕ) → ℕ
hN : ∀ k < n, ∀ b ≥ N k, p (n * b + k)
b : ℕ
hb : b ≥ (Finset.range n).sup fun (x : ℕ) ↦ n * N x
hlt : b % n < n
rw : n * N (b % n) ≤ b
⊢ b / n ≥ N (b % n)

Tactic:
rw [ge_iff_le, Nat.le_div_iff_mul_le hn.bot_lt, mul_comm]

Premises used: ge_iff_le, mul_comm, Nat.le_div_iff_mul_le, Ne.bot_lt
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
p : ℕ → Prop
n : ℕ
hn : n ≠ 0
N : (k : ℕ) → ℕ
hN : ∀ k < n, ∀ b ≥ N k, p (n * b + k)
b : ℕ
hb : b ≥ (Finset.range n).sup fun (x : ℕ) ↦ n * N x
hlt : b % n < n
⊢ n * N (b % n) ≤ b

Tactic:
(Finset.le_sup (f := (n * N ·)) (Finset.mem_range.2 hlt)).trans hb

Premises used: Iff.mpr, Finset.mem_range, LE.le.trans, Finset.le_sup
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
p : ℕ → Prop
n : ℕ
hn : n ≠ 0
N : (k : ℕ) → ℕ
hN : ∀ k < n, ∀ b ≥ N k, p (n * b + k)
b : ℕ
hb : b ≥ (Finset.range n).sup fun (x : ℕ) ↦ n * N x
hlt : b % n < n
⊢ n * N (b % n) ≤ b

Tactic:
exact (Finset.le_sup (f := (n * N ·)) (Finset.mem_range.2 hlt)).trans hb

Premises used: Iff.mpr, Finset.mem_range, LE.le.trans, Finset.le_sup
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
α : Type u_3
f : Filter α
s : ℕ → Set α
hs : f.HasAntitoneBasis s
r : ℕ → ℕ → Prop
hr : ∀ (m : ℕ), ∀ᶠ (n : ℕ) in atTop, r m n
rsuffices :
  ∀ (φ : ℕ → ℕ) (hφ : StrictMono φ) (hrφ : ∀ (m n : ℕ), m < n → r (φ m) (φ n)),
    ∃ (φ : ℕ → ℕ), StrictMono φ ∧ (∀ ⦃m n : ℕ⦄, m < n → r (φ m) (φ n)) ∧ f.HasAntitoneBasis (s ∘ φ)
rsuffices₁ : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (m n : ℕ), m < n → r (φ m) (φ n)
⊢ ∃ (φ : ℕ → ℕ), StrictMono φ ∧ (∀ ⦃m n : ℕ⦄, m < n → r (φ m) (φ n)) ∧ f.HasAntitoneBasis (s ∘ φ)

Tactic:
rsuffices ⟨φ, hφ, hrφ⟩ : ∃ φ : ℕ → ℕ, StrictMono φ ∧ ∀ m n, m < n → r (φ m) (φ n)
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
α : Type u_3
f : Filter α
s : ℕ → Set α
hs : f.HasAntitoneBasis s
r : ℕ → ℕ → Prop
hr : ∀ (m : ℕ), ∀ᶠ (n : ℕ) in atTop, r m n
φ : ℕ → ℕ
hφ : StrictMono φ
hrφ : ∀ (m n : ℕ), m < n → r (φ m) (φ n)
⊢ ∃ (φ : ℕ → ℕ), StrictMono φ ∧ (∀ ⦃m n : ℕ⦄, m < n → r (φ m) (φ n)) ∧ f.HasAntitoneBasis (s ∘ φ)

Tactic:
⟨φ, hφ, hrφ, hs.comp_strictMono hφ⟩

Premises used: And.intro, Exists.intro, Filter.HasAntitoneBasis.comp_strictMono
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
α : Type u_3
f : Filter α
s : ℕ → Set α
hs : f.HasAntitoneBasis s
r : ℕ → ℕ → Prop
hr : ∀ (m : ℕ), ∀ᶠ (n : ℕ) in atTop, r m n
φ : ℕ → ℕ
hφ : StrictMono φ
hrφ : ∀ (m n : ℕ), m < n → r (φ m) (φ n)
⊢ ∃ (φ : ℕ → ℕ), StrictMono φ ∧ (∀ ⦃m n : ℕ⦄, m < n → r (φ m) (φ n)) ∧ f.HasAntitoneBasis (s ∘ φ)

Tactic:
exact ⟨φ, hφ, hrφ, hs.comp_strictMono hφ⟩
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
α : Type u_3
f : Filter α
s : ℕ → Set α
hs : f.HasAntitoneBasis s
r : ℕ → ℕ → Prop
hr : ∀ (m : ℕ), ∀ᶠ (n : ℕ) in atTop, r m n
⊢ ∀ (t : Set ℕ), t.Finite → ∀ᶠ (n : ℕ) in atTop, ∀ m ∈ t, m < n ∧ r m n

Tactic:
have : ∀ t : Set ℕ, t.Finite → ∀ᶠ n in atTop, ∀ m ∈ t, m < n ∧ r m n := fun t ht =>
    (eventually_all_finite ht).2 fun m _ => (eventually_gt_atTop m).and (hr _)
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
α : Type u_3
f : Filter α
s : ℕ → Set α
hs : f.HasAntitoneBasis s
r : ℕ → ℕ → Prop
hr : ∀ (m : ℕ), ∀ᶠ (n : ℕ) in atTop, r m n
this : ∀ (t : Set ℕ), t.Finite → ∀ᶠ (n : ℕ) in atTop, ∀ m ∈ t, m < n ∧ r m n
rcases :
  ∀ (φ : ℕ → ℕ) (hφ : ∀ (n m : ℕ), m ∈ φ '' Iio n → m < φ n ∧ r m (φ n)),
    ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (m n : ℕ), m < n → r (φ m) (φ n)
⊢ ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (m n : ℕ), m < n → r (φ m) (φ n)

Tactic:
rcases seq_of_forall_finite_exists fun t ht => (this t ht).exists with ⟨φ, hφ⟩

Premises used: Filter.Eventually.exists, Set.seq_of_forall_finite_exists
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
α : Type u_3
f : Filter α
s : ℕ → Set α
hs : f.HasAntitoneBasis s
r : ℕ → ℕ → Prop
hr : ∀ (m : ℕ), ∀ᶠ (n : ℕ) in atTop, r m n
this : ∀ (t : Set ℕ), t.Finite → ∀ᶠ (n : ℕ) in atTop, ∀ m ∈ t, m < n ∧ r m n
φ : ℕ → ℕ
hφ : ∀ (n m : ℕ), m ∈ φ '' Iio n → m < φ n ∧ r m (φ n)
⊢ (∀ (x : ℕ) ⦃x_1 : ℕ⦄, x_1 < x → φ x_1 < φ x) ∧ ∀ (x : ℕ) ⦃x_1 : ℕ⦄, x_1 < x → r (φ x_1) (φ x)

Tactic:
simp only [forall_mem_image, forall_and, mem_Iio] at hφ

Premises used: Set.mem_Iio, Set.forall_mem_image, forall_and
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
α : Type u_3
f : Filter α
s : ℕ → Set α
hs : f.HasAntitoneBasis s
r : ℕ → ℕ → Prop
hr : ∀ (m : ℕ), ∀ᶠ (n : ℕ) in atTop, r m n
this : ∀ (t : Set ℕ), t.Finite → ∀ᶠ (n : ℕ) in atTop, ∀ m ∈ t, m < n ∧ r m n
φ : ℕ → ℕ
hφ : (∀ (x : ℕ) ⦃x_1 : ℕ⦄, x_1 < x → φ x_1 < φ x) ∧ ∀ (x : ℕ) ⦃x_1 : ℕ⦄, x_1 < x → r (φ x_1) (φ x)
⊢ ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (m n : ℕ), m < n → r (φ m) (φ n)

Tactic:
⟨φ, forall_comm.2 hφ.1, forall_comm.2 hφ.2⟩

Premises used: Iff.mpr, forall_comm, And.right, And.left, And.intro, Exists.intro
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
α : Type u_3
f : Filter α
s : ℕ → Set α
hs : f.HasAntitoneBasis s
r : ℕ → ℕ → Prop
hr : ∀ (m : ℕ), ∀ᶠ (n : ℕ) in atTop, r m n
this : ∀ (t : Set ℕ), t.Finite → ∀ᶠ (n : ℕ) in atTop, ∀ m ∈ t, m < n ∧ r m n
φ : ℕ → ℕ
hφ : (∀ (x : ℕ) ⦃x_1 : ℕ⦄, x_1 < x → φ x_1 < φ x) ∧ ∀ (x : ℕ) ⦃x_1 : ℕ⦄, x_1 < x → r (φ x_1) (φ x)
⊢ ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (m n : ℕ), m < n → r (φ m) (φ n)

Tactic:
exact ⟨φ, forall_comm.2 hφ.1, forall_comm.2 hφ.2⟩
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
c d : ℕ
rw : ∃ (a : ℕ), ∀ b ≥ a, c ^ b < (b - d)!
⊢ ∀ᶠ (n : ℕ) in atTop, c ^ n < (n - d)!

Tactic:
rw [eventually_atTop]

Premises used: Filter.eventually_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
c d : ℕ
⊢ ∃ (a : ℕ), ∀ b ≥ a, c ^ b < (b - d)!

Tactic:
⟨2 * (c ^ 2 + d + 1), ?_⟩

Premises used: HMul.hMul, HPow.hPow, HAdd.hAdd, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
c d : ℕ
refine : ∀ b ≥ 2 * (HPow.hPow (β := ℕ) c 2 + d + 1), c ^ b < (b - d)!
⊢ ∃ (a : ℕ), ∀ b ≥ a, c ^ b < (b - d)!

Tactic:
refine ⟨2 * (c ^ 2 + d + 1), ?_⟩
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
c d n : ℕ
hn : n ≥ 2 * (HPow.hPow (β := ℕ) c 2 + d + 1)
obtain :
  ∀ (d' : ℕ) (hn : 2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d' ≥ 2 * (HPow.hPow (β := ℕ) c 2 + d + 1)),
    c ^ (2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d') < (2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d' - d)!
⊢ c ^ n < (n - d)!

Tactic:
obtain ⟨d', rfl⟩ := Nat.exists_eq_add_of_le hn

Premises used: Nat.exists_eq_add_of_le, rfl
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
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)!
inr : ∀ (c0 : c > 0), c ^ (2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d') < (2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d' - d)!
⊢ 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

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
d d' : ℕ
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)!

Tactic:
simp [Nat.two_mul, ← Nat.add_assoc, Nat.add_right_comm _ 1, Nat.factorial_pos]

Premises used: Nat.add_assoc, Nat.two_mul, OfNat.ofNat, Nat.factorial_pos, Nat.add_right_comm
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
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)!

Tactic:
(Nat.le_mul_of_pos_right _ (Nat.pow_pos (n := d') c0)).trans_lt ?_

Premises used: Nat.le_mul_of_pos_right, Nat.pow_pos, LE.le.trans_lt
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
c d d' : ℕ
hn : 2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d' ≥ 2 * (HPow.hPow (β := ℕ) c 2 + d + 1)
c0 : c > 0
inr : c ^ (2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d') * c ^ d' < (2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d' - d)!
⊢ c ^ (2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + 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 ?_

Premises used: Nat.le_mul_of_pos_right, Nat.pow_pos, LE.le.trans_lt
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
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)!
inr :
  HPow.hPow (β := ℕ) c 2 ^ (HPow.hPow (β := ℕ) c 2 + d' + d + 1) <
    (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)!

Tactic:
convert_to (c ^ 2) ^ (c ^ 2 + d' + d + 1) < (c ^ 2 + (c ^ 2 + d' + d + 1) + 1)!

Premises used: HPow.hPow, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
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' + d') = c ^ (2 * (HPow.hPow (β := ℕ) c 2 + d' + d + 1))
⊢ c ^ (2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d') * c ^ d' =
    HPow.hPow (β := ℕ) c 2 ^ (HPow.hPow (β := ℕ) c 2 + d' + d + 1)

Tactic:
rw [← pow_mul, ← pow_add]

Premises used: pow_add, pow_mul
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
c d d' : ℕ
hn : 2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d' ≥ 2 * (HPow.hPow (β := ℕ) c 2 + d + 1)
c0 : c > 0
h : 2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d' + d' = 2 * (HPow.hPow (β := ℕ) c 2 + d' + d + 1)
⊢ c ^ (2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d' + d') = c ^ (2 * (HPow.hPow (β := ℕ) c 2 + d' + d + 1))

Tactic:
congr 1
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
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' = 2 * (HPow.hPow (β := ℕ) c 2 + d' + d + 1)

Tactic:
lia
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
c d d' : ℕ
hn : 2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d' ≥ 2 * (HPow.hPow (β := ℕ) c 2 + d + 1)
c0 : c > 0
h : 2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d' - d = HPow.hPow (β := ℕ) c 2 + (HPow.hPow (β := ℕ) c 2 + d' + d + 1) + 1
⊢ (2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d' - d)! =
    (HPow.hPow (β := ℕ) c 2 + (HPow.hPow (β := ℕ) c 2 + d' + d + 1) + 1)!

Tactic:
congr 1
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
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

Tactic:
lia
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
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)!

Tactic:
(lt_of_lt_of_le ?_ Nat.factorial_mul_pow_le_factorial).trans_le <|
    (factorial_le (Nat.le_succ _))

Premises used: Nat.le_succ, Nat.factorial_mul_pow_le_factorial, LT.lt.trans_le, Nat.factorial_le, lt_of_lt_of_le
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
c d d' : ℕ
hn : 2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d' ≥ 2 * (HPow.hPow (β := ℕ) c 2 + d + 1)
c0 : c > 0
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)
⊢ HPow.hPow (β := ℕ) c 2 ^ (HPow.hPow (β := ℕ) c 2 + d' + d + 1) <
    (HPow.hPow (β := ℕ) c 2 + (HPow.hPow (β := ℕ) c 2 + d' + d + 1) + 1)!

Tactic:
refine (lt_of_lt_of_le ?_ Nat.factorial_mul_pow_le_factorial).trans_le <|
    (factorial_le (Nat.le_succ _))

Premises used: Nat.le_succ, Nat.factorial_mul_pow_le_factorial, LT.lt.trans_le, Nat.factorial_le, lt_of_lt_of_le
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
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 ^ (HPow.hPow (β := ℕ) c 2 + d' + d + 1) <
    (HPow.hPow (β := ℕ) c 2)! * (HPow.hPow (β := ℕ) c 2 + 1) ^ (HPow.hPow (β := ℕ) c 2 + d' + d + 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 (_ ^ _ : ℕ)]

Premises used: HPow.hPow, one_mul
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
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)
inr₂ : 0 < (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)

Tactic:
apply Nat.mul_lt_mul_of_le_of_lt

Premises used: Nat.mul_lt_mul_of_le_of_lt
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
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)!

Tactic:
Nat.one_le_of_lt (Nat.factorial_pos _)

Premises used: Nat.one_le_of_lt, Nat.factorial_pos
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
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)!

Tactic:
exact Nat.one_le_of_lt (Nat.factorial_pos _)

Premises used: Nat.one_le_of_lt, Nat.factorial_pos
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
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 + 1) ^ (HPow.hPow (β := ℕ) c 2 + d' + d + 1)

Tactic:
Nat.pow_lt_pow_left (Nat.lt_succ_self _) (Nat.succ_ne_zero _)

Premises used: Nat.lt_succ_self, Nat.succ_ne_zero, Nat.pow_lt_pow_left
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
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 + 1) ^ (HPow.hPow (β := ℕ) c 2 + d' + d + 1)

Tactic:
exact Nat.pow_lt_pow_left (Nat.lt_succ_self _) (Nat.succ_ne_zero _)

Premises used: Nat.lt_succ_self, Nat.succ_ne_zero, Nat.pow_lt_pow_left
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
c d d' : ℕ
hn : 2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d' ≥ 2 * (HPow.hPow (β := ℕ) c 2 + d + 1)
c0 : c > 0
⊢ 0 < (HPow.hPow (β := ℕ) c 2)!

Tactic:
(Nat.factorial_pos _)

Premises used: Nat.factorial_pos
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
c d d' : ℕ
hn : 2 * (HPow.hPow (β := ℕ) c 2 + d + 1) + d' ≥ 2 * (HPow.hPow (β := ℕ) c 2 + d + 1)
c0 : c > 0
⊢ 0 < (HPow.hPow (β := ℕ) c 2)!

Tactic:
exact (Nat.factorial_pos _)

Premises used: Nat.factorial_pos
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
a c d : ℕ
h : ∀ (n : ℕ) (hn : (a * c) ^ n < (n - d)!) (hn0 : 0 < n), a * c ^ n < (n - d)!
⊢ ∀ᶠ (n : ℕ) in atTop, 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

Premises used: HMul.hMul, Nat.eventually_pow_lt_factorial_sub, OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
a c d n : ℕ
hn : (a * c) ^ n < (n - d)!
hn0 : 0 < n
⊢ a ^ n * c ^ n < (n - d)!

Tactic:
rw [mul_pow] at hn

Premises used: mul_pow
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
a c d n : ℕ
hn : (a * c) ^ n < (n - d)!
hn0 : 0 < n
hn₁ : a ^ n * c ^ n < (n - d)!
⊢ 0 < n

Tactic:
rw [mul_pow] at hn

Premises used: mul_pow
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
a c d n : ℕ
hn : a ^ n * c ^ n < (n - d)!
hn0 : 0 < n
⊢ a * c ^ n < (n - d)!

Tactic:
(Nat.mul_le_mul_right _ (Nat.le_self_pow hn0.ne' _)).trans_lt hn

Premises used: Nat.le_self_pow, Nat.mul_le_mul_right, LT.lt.ne', LE.le.trans_lt
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
a c d n : ℕ
hn : a ^ n * c ^ n < (n - d)!
hn0 : 0 < n
⊢ a * c ^ n < (n - d)!

Tactic:
exact (Nat.mul_le_mul_right _ (Nat.le_self_pow hn0.ne' _)).trans_lt hn

Premises used: Nat.le_self_pow, Nat.mul_le_mul_right, LT.lt.ne', LE.le.trans_lt
-- Module: Mathlib.Order.Filter.AtTopBot.Finset
Goal:
⊢ Tendsto Finset.range atTop atTop

Tactic:
Finset.range_mono.tendsto_atTop_atTop Finset.exists_nat_subset_range

Premises used: Finset.range_mono, Monotone.tendsto_atTop_atTop, Finset.exists_nat_subset_range
-- Module: Mathlib.Order.Filter.AtTopBot.Finset
Goal:
α : Type u_3
⊢ Eq.{u_3 + 1} (α := Filter (Finset α)) atTop (⨅ (x : α), 𝓟 (Ici {x}))

Tactic:
le_antisymm (le_iInf fun i => le_principal_iff.2 <| mem_atTop ({i} : Finset α)) ?_

Premises used: Iff.mpr, Filter.le_principal_iff, Filter.mem_atTop, le_iInf, le_antisymm, Singleton.singleton
-- Module: Mathlib.Order.Filter.AtTopBot.Finset
Goal:
α : Type u_3
refine : LE.le.{u_3} (α := Filter (Finset α)) (⨅ (x : α), 𝓟 (Ici {x})) atTop
⊢ Eq.{u_3 + 1} (α := Filter (Finset α)) atTop (⨅ (x : α), 𝓟 (Ici {x}))

Tactic:
refine le_antisymm (le_iInf fun i => le_principal_iff.2 <| mem_atTop ({i} : Finset α)) ?_

Premises used: Iff.mpr, Filter.le_principal_iff, Filter.mem_atTop, le_iInf, le_antisymm, Singleton.singleton
-- Module: Mathlib.Order.Filter.AtTopBot.Finset
Goal:
α : Type u_3
⊢ LE.le.{u_3} (α := Filter (Finset α)) (⨅ (x : α), 𝓟 (Ici {x})) atTop

Tactic:
le_iInf fun s =>
      le_principal_iff.2 <| mem_iInf_of_iInter s.finite_toSet (fun i => mem_principal_self _) ?_

Premises used: Iff.mpr, Filter.mem_principal_self, Set.Ici, Filter.le_principal_iff, Set.Mem, Filter.mem_iInf_of_iInter, le_iInf, Finset.finite_toSet, Singleton.singleton, Subtype.val
-- Module: Mathlib.Order.Filter.AtTopBot.Finset
Goal:
α : Type u_3
le_iInf : ∀ (s : Finset α), ⋂ (i : (↑(↑s : Set α) : Type u_3)), Ici {(↑i : α)} ⊆ Ici s
⊢ LE.le.{u_3} (α := Filter (Finset α)) (⨅ (x : α), 𝓟 (Ici {x})) atTop

Tactic:
refine
    le_iInf fun s =>
      le_principal_iff.2 <| mem_iInf_of_iInter s.finite_toSet (fun i => mem_principal_self _) ?_

Premises used: Iff.mpr, Filter.mem_principal_self, Filter.le_principal_iff, Filter.mem_iInf_of_iInter, le_iInf, Subtype.val
-- Module: Mathlib.Order.Filter.AtTopBot.Finset
Goal:
α : Type u_3
s : Finset α
simp : ∀ (x : Finset α), (∀ (x_1 : α) (h : x_1 ∈ (↑s : Set α)), x_1 ∈ x) → ∀ ⦃x_1 : α⦄, x_1 ∈ s → x_1 ∈ x
⊢ ⋂ (i : (↑(↑s : Set α) : Type u_3)), Ici {(↑i : α)} ⊆ Ici s

Tactic:
simp only [subset_def, mem_iInter, SetCoe.forall, mem_Ici, Finset.le_iff_subset,
    Finset.mem_singleton, Finset.subset_iff, forall_eq]

Premises used: Finset.mem_singleton, Set.subset_def, forall_eq, Set.mem_iInter, Finset.subset_iff, Set.mem_Ici, Finset.le_iff_subset, SetCoe.forall
-- Module: Mathlib.Order.Filter.AtTopBot.Finset
Goal:
α : Type u_3
s : Finset α
⊢ ∀ (x : Finset α), (∀ (x_1 : α) (h : x_1 ∈ (↑s : Set α)), x_1 ∈ x) → ∀ ⦃x_1 : α⦄, x_1 ∈ s → x_1 ∈ x

Tactic:
fun t => id

Premises used: id
-- Module: Mathlib.Order.Filter.AtTopBot.Finset
Goal:
α : Type u_3
s : Finset α
⊢ ∀ (x : Finset α), (∀ (x_1 : α) (h : x_1 ∈ (↑s : Set α)), x_1 ∈ x) → ∀ ⦃x_1 : α⦄, x_1 ∈ s → x_1 ∈ x

Tactic:
exact fun t => id

Premises used: id
-- Module: Mathlib.Order.Filter.AtTopBot.Finset
Goal:
α : Type u_3
β : Type u_4
inst : Preorder β
f : β → Finset α
h : Monotone f
h' : ∀ (x : α), ∃ (n : β), x ∈ f n
simp : ∀ (i : α), ∀ᶠ (a : β) in atTop, Membership.mem (γ := Set (Finset α)) (Ici {i}) (f a)
⊢ Tendsto f atTop atTop

Tactic:
simp only [atTop_finset_eq_iInf, tendsto_iInf, tendsto_principal]

Premises used: Filter.tendsto_principal, Filter.atTop_finset_eq_iInf, Filter.tendsto_iInf
-- Module: Mathlib.Order.Filter.AtTopBot.Finset
Goal:
α : Type u_3
β : Type u_4
inst : Preorder β
f : β → Finset α
h : Monotone f
h' : ∀ (x : α), ∃ (n : β), x ∈ f n
a : α
rcases : ∀ (b : β) (hb : a ∈ f b), ∀ᶠ (a_1 : β) in atTop, Membership.mem (γ := Set (Finset α)) (Ici {a}) (f a_1)
⊢ ∀ᶠ (a_1 : β) in atTop, Membership.mem (γ := Set (Finset α)) (Ici {a}) (f a_1)

Tactic:
rcases h' a with ⟨b, hb⟩
-- Module: Mathlib.Order.Filter.AtTopBot.Finset
Goal:
α : Type u_3
β : Type u_4
inst : Preorder β
f : β → Finset α
h : Monotone f
h' : ∀ (x : α), ∃ (n : β), x ∈ f n
a : α
b : β
hb : a ∈ f b
⊢ ∀ᶠ (a_1 : β) in atTop, Membership.mem (γ := Set (Finset α)) (Ici {a}) (f a_1)

Tactic:
(eventually_ge_atTop b).mono fun b' hb' => (Finset.singleton_subset_iff.2 hb).trans (h hb')

Premises used: Iff.mpr, Finset.singleton_subset_iff, HasSubset.Subset.trans, Filter.Eventually.mono, Filter.eventually_ge_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Finset
Goal:
α : Type u_3
β : Type u_4
inst : Preorder β
f : β → Finset α
h : Monotone f
h' : ∀ (x : α), ∃ (n : β), x ∈ f n
a : α
b : β
hb : a ∈ f b
⊢ ∀ᶠ (a_1 : β) in atTop, Membership.mem (γ := Set (Finset α)) (Ici {a}) (f a_1)

Tactic:
exact (eventually_ge_atTop b).mono fun b' hb' => (Finset.singleton_subset_iff.2 hb).trans (h hb')

Premises used: Iff.mpr, Finset.singleton_subset_iff, HasSubset.Subset.trans, Filter.Eventually.mono, Filter.eventually_ge_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Finset
Goal:
β : Type u_4
γ : Type u_5
inst : DecidableEq β
i : β → γ
j : γ → β
h : Function.LeftInverse j i
a : β
⊢ a ∈ Finset.image j {i a}

Tactic:
simp only [Finset.image_singleton, h a, Finset.mem_singleton]

Premises used: Finset.mem_singleton, Finset.image_singleton
-- Module: Mathlib.Order.Filter.AtTopBot.Finset
Goal:
α : Type u_3
β : Type u_4
f : α → β
hf : Function.Injective f
⊢ Tendsto.{u_4, u_3} (β := Finset α) (fun (s : Finset β) ↦ s.preimage f ⋯) atTop atTop

Tactic:
(Finset.monotone_preimage hf).tendsto_atTop_finset fun x =>
    ⟨{f x}, Finset.mem_preimage.2 <| Finset.mem_singleton_self _⟩

Premises used: Iff.mpr, Finset.mem_singleton_self, Monotone.tendsto_atTop_finset, Finset.mem_preimage, Exists.intro, Singleton.singleton, Finset.monotone_preimage
-- 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.toLeft ∈ s
⊢ Membership.mem (γ := Filter (Finset α)) (map (α := Finset (α ⊕ β)) Finset.toLeft 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.toLeft ∈ s
⊢ ∃ (a : Finset (α ⊕ β)), ∀ b ≥ a, b.toLeft ∈ 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 ≥ t.disjSum ∅
⊢ b.toLeft ≥ t

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

Premises used: Set.subset_def, Finset.coe_subset