awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n : ℕ
⊢ n ! ≠ 0

Tactic:
ne_of_gt (factorial_pos _)

Premises used: Nat.factorial_pos, Nat.ne_of_gt
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
m n : ℕ
⊢ m ! ∣ m !

Tactic:
Nat.dvd_refl _

Premises used: Nat.dvd_refl
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
m n : ℕ
⊢ m ! ∣ m !

Tactic:
exact Nat.dvd_refl _

Premises used: Nat.dvd_refl
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
m n m_1 : ℕ
h : m.le m_1
ih : m ! ∣ m_1 !
⊢ m ! ∣ m_1.succ !

Tactic:
Nat.dvd_trans ih (Nat.dvd_mul_left _ _)

Premises used: Nat.dvd_trans, Nat.dvd_mul_left
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
m n m_1 : ℕ
h : m.le m_1
ih : m ! ∣ m_1 !
⊢ m ! ∣ m_1.succ !

Tactic:
exact Nat.dvd_trans ih (Nat.dvd_mul_left _ _)

Premises used: Nat.dvd_trans, Nat.dvd_mul_left
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
m n : ℕ
h : m ≤ n
refl : m ! ∣ m !
step : ∀ {m_1 : ℕ}, m.le m_1 → ∀ (ih : m ! ∣ m_1 !), m ! ∣ m_1.succ !
⊢ m ! ∣ n !

Tactic:
induction h with
  | refl => exact Nat.dvd_refl _
  | step _ ih => exact Nat.dvd_trans ih (Nat.dvd_mul_left _ _)

Premises used: Nat.dvd_refl, refl
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
m n : ℕ
h : m ≤ n
⊢ m ! ≤ n !

Tactic:
le_of_dvd (factorial_pos _) (factorial_dvd_factorial h)

Premises used: Nat.factorial_dvd_factorial, Nat.le_of_dvd, Nat.factorial_pos
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
m : ℕ
⊢ m ! * HPow.hPow (β := ℕ) (m + 1) 0 ≤ (m + 0)!

Tactic:
simp
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
m n : ℕ
rw : m ! * (m + 1) ^ n * (m + 1) ≤ (m + n)! * (m + n + 1)
⊢ m ! * (m + 1) ^ (n + 1) ≤ (m + (n + 1))!

Tactic:
rw [← Nat.add_assoc, factorial_succ, Nat.mul_comm (_ + 1), Nat.pow_succ, ← Nat.mul_assoc]

Premises used: Nat.factorial_succ, Nat.pow_succ, Nat.mul_comm, Nat.mul_assoc, HAdd.hAdd, Nat.add_assoc, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
m n : ℕ
⊢ m ! * (m + 1) ^ n * (m + 1) ≤ (m + n)! * (m + n + 1)

Tactic:
Nat.mul_le_mul factorial_mul_pow_le_factorial (succ_le_succ (le_add_right _ _))

Premises used: Nat.le_add_right, Nat.mul_le_mul, Nat.succ_le_succ
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
m n : ℕ
⊢ m ! * (m + 1) ^ n * (m + 1) ≤ (m + n)! * (m + n + 1)

Tactic:
exact Nat.mul_le_mul factorial_mul_pow_le_factorial (succ_le_succ (le_add_right _ _))

Premises used: Nat.le_add_right, Nat.mul_le_mul, Nat.succ_le_succ
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
m n : ℕ
hn : 0 < n
⊢ n ! < m ! ↔ n < m

Tactic:
⟨fun h => not_le.mp fun hmn => Nat.not_le_of_gt h (factorial_le hmn), fun h => ?_⟩

Premises used: not_le, Iff.intro, Nat.not_le_of_gt, Iff.mp, Nat.factorial_le
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
m n : ℕ
hn : 0 < n
refine : ∀ (h : n < m), n ! < m !
⊢ n ! < m ! ↔ n < m

Tactic:
refine ⟨fun h => not_le.mp fun hmn => Nat.not_le_of_gt h (factorial_le hmn), fun h => ?_⟩
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
m n : ℕ
hn : 0 < n
h : n < m
k : ℕ
hk : 0 < k
rw : 0 < k * k !
⊢ k ! < (k + 1)!

Tactic:
rw [factorial_succ, succ_mul, Nat.lt_add_left_iff_pos]

Premises used: Nat.factorial_succ, Nat.lt_add_left_iff_pos, Nat.succ_mul
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
m n : ℕ
hn : 0 < n
h : n < m
k : ℕ
hk : 0 < k
⊢ 0 < k * k !

Tactic:
Nat.mul_pos hk k.factorial_pos

Premises used: Nat.mul_pos, Nat.factorial_pos
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
m n : ℕ
hn : 0 < n
h : n < m
k : ℕ
hk : 0 < k
⊢ 0 < k * k !

Tactic:
exact Nat.mul_pos hk k.factorial_pos

Premises used: Nat.mul_pos, Nat.factorial_pos
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
m n : ℕ
hn : 0 < n
h : n < m
⊢ ∀ {n : ℕ}, 0 < n → n ! < (n + 1)!

Tactic:
have : ∀ {n}, 0 < n → n ! < (n + 1)! := by
    intro k hk
    rw [factorial_succ, succ_mul, Nat.lt_add_left_iff_pos]
    exact Nat.mul_pos hk k.factorial_pos
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
m n : ℕ
this : ∀ {n : ℕ}, 0 < n → n ! < (n + 1)!
hn : 0 < n
⊢ n ! < n.succ !

Tactic:
this hn
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
m n : ℕ
this : ∀ {n : ℕ}, 0 < n → n ! < (n + 1)!
hn : 0 < n
⊢ n ! < n.succ !

Tactic:
exact this hn
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
m n : ℕ
this : ∀ {n : ℕ}, 0 < n → n ! < (n + 1)!
m_1 : ℕ
hnk : n.succ.le m_1
ih : ∀ (hn : 0 < n), n ! < m_1 !
hn : 0 < n
⊢ n ! < m_1.succ !

Tactic:
lt_trans (ih hn) <| this <| lt_trans hn <| lt_of_succ_le hnk

Premises used: lt_trans, Nat.lt_of_succ_le
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
m n : ℕ
this : ∀ {n : ℕ}, 0 < n → n ! < (n + 1)!
m_1 : ℕ
hnk : n.succ.le m_1
ih : ∀ (hn : 0 < n), n ! < m_1 !
hn : 0 < n
⊢ n ! < m_1.succ !

Tactic:
exact lt_trans (ih hn) <| this <| lt_trans hn <| lt_of_succ_le hnk

Premises used: lt_trans, Nat.lt_of_succ_le
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
m n : ℕ
hn : 0 < n
h : n < m
this : ∀ {n : ℕ}, 0 < n → n ! < (n + 1)!
refl : ∀ (hn : 0 < n), n ! < n.succ !
step : ∀ {m : ℕ} (hnk : n.succ.le m) (ih : ∀ (hn : 0 < n), n ! < m !) (hn : 0 < n), n ! < m.succ !
⊢ n ! < m !

Tactic:
induction h generalizing hn with
  | refl => exact this hn
  | step hnk ih => exact lt_trans (ih hn) <| this <| lt_trans hn <| lt_of_succ_le hnk

Premises used: lt_trans, refl
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
m n : ℕ
hn : 0 < n
h : n < m
⊢ n ! < m !

Tactic:
(factorial_lt hn).mpr h

Premises used: Iff.mpr, Nat.factorial_lt
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n : ℕ
⊢ 1 < n ! ↔ 1 < n

Tactic:
factorial_lt Nat.one_pos

Premises used: Nat.one_pos, Nat.factorial, Nat.factorial_lt
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n : ℕ
mp : n ! = 1 → n ≤ 1
mpr : n ≤ 1 → n ! = 1
⊢ n ! = 1 ↔ n ≤ 1

Tactic:
constructor
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n : ℕ
h : n ! = 1
mp : ¬LT.lt (α := ℕ) 1 1
⊢ n ≤ 1

Tactic:
rw [← not_lt, ← one_lt_factorial, h]

Premises used: Nat.one_lt_factorial, not_lt
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n : ℕ
h : n ! = 1
⊢ ¬LT.lt (α := ℕ) 1 1

Tactic:
apply lt_irrefl

Premises used: lt_irrefl
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
⊢ 1! = 1

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
⊢ 0! = 1

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
m n : ℕ
hn : 1 < n
⊢ n ! = m ! ↔ n = m

Tactic:
⟨fun h => ?_, congr_arg _⟩

Premises used: congr_arg, Iff.intro
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
m n : ℕ
hn : 1 < n
refine : ∀ (h : n ! = m !), n = m
⊢ n ! = m ! ↔ n = m

Tactic:
refine ⟨fun h => ?_, congr_arg _⟩
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
m n : ℕ
hn : 1 < n
h : n ! = m !
inl : ∀ (hnm : n < m), n = m
inr : ∀ (h : n ! = n !), n = n
inr₁ : ∀ (hnm : m < n), n = m
⊢ n = m

Tactic:
obtain hnm | rfl | hnm := lt_trichotomy n m

Premises used: rfl, lt_trichotomy
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
m n : ℕ
hn : 1 < n
h : n ! = m !
hnm : n < m
⊢ m ! < m !

Tactic:
rw [← factorial_lt <| lt_of_succ_lt hn, h] at hnm

Premises used: Nat.lt_of_succ_lt, Nat.factorial_lt
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
m n : ℕ
hn : 1 < n
h : n ! = m !
hnm : m ! < m !
⊢ n = m

Tactic:
cases lt_irrefl _ hnm

Premises used: lt_irrefl
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n : ℕ
hn : 1 < n
h : n ! = n !
⊢ n = n

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
m n : ℕ
hn : 1 < n
h : n ! = m !
hnm : m < n
⊢ 1 < m

Tactic:
rw [← one_lt_factorial, h, one_lt_factorial] at hn

Premises used: Nat.one_lt_factorial
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
m n : ℕ
hn : 1 < n
h : n ! = m !
hnm : m < n
hn₁ : 1 < m
⊢ n ! = m !

Tactic:
rw [← one_lt_factorial, h, one_lt_factorial] at hn

Premises used: Nat.one_lt_factorial
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
m n : ℕ
hn : 1 < n
h : n ! = m !
hnm : m < n
hn₁ : 1 < m
h₁ : n ! = m !
⊢ m < n

Tactic:
rw [← one_lt_factorial, h, one_lt_factorial] at hn

Premises used: Nat.one_lt_factorial
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
m n : ℕ
hn : 1 < m
h : n ! = m !
hnm : m < n
⊢ m ! < m !

Tactic:
rw [← factorial_lt <| lt_of_succ_lt hn, h] at hnm

Premises used: Nat.lt_of_succ_lt, Nat.factorial_lt
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
m n : ℕ
hn : 1 < m
h : n ! = m !
hnm : m ! < m !
⊢ n = m

Tactic:
cases lt_irrefl _ hnm

Premises used: lt_irrefl
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
m n : ℕ
h : 1 < n ∨ 1 < m
inl : ∀ (hn : 1 < n), n ! = m ! ↔ n = m
inr : ∀ (hm : 1 < m), n ! = m ! ↔ n = m
⊢ n ! = m ! ↔ n = m

Tactic:
obtain hn | hm := h
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
m n : ℕ
hn : 1 < n
⊢ n ! = m ! ↔ n = m

Tactic:
factorial_inj hn

Premises used: Nat.factorial_inj
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
m n : ℕ
hn : 1 < n
⊢ n ! = m ! ↔ n = m

Tactic:
exact factorial_inj hn

Premises used: Nat.factorial_inj
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
m n : ℕ
hm : 1 < m
inr : m ! = n ! ↔ n = m
inr₁ : m = n ↔ n = m
inr₂ inr₃ : n = m ↔ n = m
⊢ n ! = m ! ↔ n = m

Tactic:
rw [eq_comm, factorial_inj hm, eq_comm]

Premises used: eq_comm, Nat.factorial_inj
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n : ℕ
hi : 3 ≤ n
⊢ 0 < n

Tactic:
lia
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n : ℕ
hi : 3 ≤ n
⊢ 0 < n

Tactic:
have : 0 < n := by lia
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n : ℕ
hi : 3 ≤ n
this : 0 < n
⊢ 1 < n.pred

Tactic:
have hn : 1 < pred n := le_pred_of_lt (succ_le_iff.mp hi)
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n : ℕ
hi : 3 ≤ n
this : 0 < n
hn : 1 < n.pred
rw : n.pred.succ < (n.pred + 1) * n.pred !
⊢ n < n !

Tactic:
rw [← succ_pred_eq_of_pos ‹0 < n›, factorial_succ]

Premises used: Nat.succ_pred_eq_of_pos, Nat.factorial_succ
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n : ℕ
hi : 3 ≤ n
this : 0 < n
hn : 1 < n.pred
⊢ n.pred.succ < (n.pred + 1) * n.pred !

Tactic:
(Nat.lt_mul_iff_one_lt_right (pred n).succ_pos).2
    ((Nat.lt_of_lt_of_le hn (self_le_factorial _)))

Premises used: Iff.mpr, Nat.lt_mul_iff_one_lt_right, Nat.succ_pos, Nat.self_le_factorial, Nat.lt_of_lt_of_le, Nat.pred
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n : ℕ
hi : 3 ≤ n
this : 0 < n
hn : 1 < n.pred
⊢ n.pred.succ < (n.pred + 1) * n.pred !

Tactic:
exact (Nat.lt_mul_iff_one_lt_right (pred n).succ_pos).2
    ((Nat.lt_of_lt_of_le hn (self_le_factorial _)))

Premises used: Iff.mpr, Nat.lt_mul_iff_one_lt_right, Nat.succ_pos, Nat.self_le_factorial, Nat.lt_of_lt_of_le, Nat.pred
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
i n : ℕ
hi : 2 ≤ i
rw : i + (n + 1)! < (i + n) * (i + n)! + (i + n)!
⊢ i + (n + 1)! < (i + n + 1)!

Tactic:
rw [factorial_succ (i + _), Nat.add_mul, Nat.one_mul]

Premises used: Nat.factorial_succ, HAdd.hAdd, Nat.one_mul, Nat.add_mul
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
i n : ℕ
hi : 2 ≤ i
⊢ i + n ≤ (i + n)!

Tactic:
have := (i + n).self_le_factorial
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
i n : ℕ
hi : 2 ≤ i
this : i + n ≤ (i + n)!
⊢ i + (n + 1)! < (i + n) * (i + n)! + (i + n)!

Tactic:
Nat.add_lt_add_of_lt_of_le (Nat.lt_of_le_of_lt ?_ ((Nat.lt_mul_iff_one_lt_right ?_).2 ?_))
    (factorial_le ?_)

Premises used: Iff.mpr, Nat.lt_of_le_of_lt, Nat.lt_mul_iff_one_lt_right, Nat.factorial_le, Nat.add_lt_add_of_lt_of_le
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
i n : ℕ
hi : 2 ≤ i
this : i + n ≤ (i + n)!
refine_1 : i ≤ i + n
refine_2 : 0 < i + n
refine_3 : 1 < (i + n)!
refine_4 : n + 1 ≤ i + n
⊢ i + (n + 1)! < (i + n) * (i + n)! + (i + n)!

Tactic:
refine Nat.add_lt_add_of_lt_of_le (Nat.lt_of_le_of_lt ?_ ((Nat.lt_mul_iff_one_lt_right ?_).2 ?_))
    (factorial_le ?_)

Premises used: Iff.mpr, Nat.lt_of_le_of_lt, Nat.lt_mul_iff_one_lt_right, Nat.factorial_le, Nat.add_lt_add_of_lt_of_le
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
i n : ℕ
hi : 2 ≤ i
this : i + n ≤ (i + n)!
⊢ i ≤ i + n

Tactic:
lia
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
i n : ℕ
hi : 2 ≤ i
this : i + n ≤ (i + n)!
⊢ 0 < i + n

Tactic:
lia
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
i n : ℕ
hi : 2 ≤ i
this : i + n ≤ (i + n)!
⊢ 1 < (i + n)!

Tactic:
lia
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
i n : ℕ
hi : 2 ≤ i
this : i + n ≤ (i + n)!
⊢ n + 1 ≤ i + n

Tactic:
lia
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
i n : ℕ
hi : 2 ≤ i
hn : 1 ≤ n
refl : i + 1! < (i + 1)!
step : ∀ {m : ℕ}, Nat.le 1 m → i + m.succ ! < (i + m.succ)!
⊢ i + n ! < (i + n)!

Tactic:
cases hn
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
i : ℕ
hi : 2 ≤ i
⊢ i + 1 < (i + 1)!

Tactic:
lt_factorial_self (succ_le_succ hi)

Premises used: Nat.lt_factorial_self, Nat.succ_le_succ
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
i : ℕ
hi : 2 ≤ i
⊢ i + 1 < (i + 1)!

Tactic:
exact lt_factorial_self (succ_le_succ hi)

Premises used: Nat.lt_factorial_self, Nat.succ_le_succ
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
i : ℕ
hi : 2 ≤ i
m : ℕ
h : Nat.le 1 m
⊢ i + m.succ ! < (i + m.succ)!

Tactic:
add_factorial_succ_lt_factorial_add_succ _ hi

Premises used: Nat.add_factorial_succ_lt_factorial_add_succ
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
i : ℕ
hi : 2 ≤ i
m : ℕ
h : Nat.le 1 m
⊢ i + m.succ ! < (i + m.succ)!

Tactic:
exact add_factorial_succ_lt_factorial_add_succ _ hi

Premises used: Nat.add_factorial_succ_lt_factorial_add_succ
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
i n : ℕ
inl : 2 ≤ i → i + (n + 1)! ≤ (i + (n + 1))!
inr : i < 2 → i + (n + 1)! ≤ (i + (n + 1))!
⊢ i + (n + 1)! ≤ (i + (n + 1))!

Tactic:
cases (le_or_gt (2 : ℕ) i)

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
i n : ℕ
h : 2 ≤ i
inl : i + (n + 1)! ≤ (i + n + 1)!
⊢ i + (n + 1)! ≤ (i + (n + 1))!

Tactic:
rw [← Nat.add_assoc]

Premises used: Nat.add_assoc
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
i n : ℕ
h : 2 ≤ i
inl : i + (n + 1)! < (i + n + 1)!
⊢ i + (n + 1)! ≤ (i + n + 1)!

Tactic:
apply Nat.le_of_lt

Premises used: Nat.le_of_lt
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
i n : ℕ
h : 2 ≤ i
inl : 2 ≤ i
⊢ i + (n + 1)! < (i + n + 1)!

Tactic:
apply add_factorial_succ_lt_factorial_add_succ

Premises used: Nat.add_factorial_succ_lt_factorial_add_succ
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
i n : ℕ
h : 2 ≤ i
⊢ 2 ≤ i

Tactic:
assumption
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
i n : ℕ
h : LT.lt (α := ℕ) 0 2
⊢ 0 + (n + 1)! ≤ (0 + (n + 1))!

Tactic:
simp
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
i n : ℕ
h : LT.lt (α := ℕ) 1 2
rw : 1 ≤ (n + 1) * (n + 1)!
⊢ 1 + (n + 1)! ≤ (1 + (n + 1))!

Tactic:
rw [← Nat.add_assoc, factorial_succ (1 + n), Nat.add_mul, Nat.one_mul, Nat.add_comm 1 n,
        Nat.add_le_add_iff_right]

Premises used: Nat.add_le_add_iff_right, Nat.factorial_succ, HAdd.hAdd, Nat.add_assoc, OfNat.ofNat, Nat.one_mul, Nat.add_mul, Nat.add_comm
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
i n : ℕ
h : LT.lt (α := ℕ) 1 2
⊢ 1 ≤ (n + 1) * (n + 1)!

Tactic:
Nat.mul_pos n.succ_pos n.succ.factorial_pos

Premises used: Nat.mul_pos, Nat.succ_pos, Nat.factorial_pos, Nat.succ, Nat.lt
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
i n : ℕ
h : LT.lt (α := ℕ) 1 2
⊢ 1 ≤ (n + 1) * (n + 1)!

Tactic:
exact Nat.mul_pos n.succ_pos n.succ.factorial_pos

Premises used: Nat.mul_pos, Nat.succ_pos, Nat.factorial_pos, Nat.succ
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
i n_1 n : ℕ
h : n.succ.succ < 2
⊢ n.succ.succ + (n_1 + 1)! ≤ (n.succ.succ + (n_1 + 1))!

Tactic:
contradiction
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
i n : ℕ
h : i < 2
⊢ i + (n + 1)! ≤ (i + (n + 1))!

Tactic:
match i with
    | 0 => simp
    | 1 =>
      rw [← Nat.add_assoc, factorial_succ (1 + n), Nat.add_mul, Nat.one_mul, Nat.add_comm 1 n,
        Nat.add_le_add_iff_right]
      exact Nat.mul_pos n.succ_pos n.succ.factorial_pos
    | succ (succ n) => contradiction
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
i n : ℕ
n1 : 1 ≤ n
refl : i + 1! ≤ (i + 1)!
step : ∀ {h : ℕ}, Nat.le 1 h → i + h.succ ! ≤ (i + h.succ)!
⊢ i + n ! ≤ (i + n)!

Tactic:
rcases n1 with - | @h
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
i : ℕ
⊢ i + 1! ≤ (i + 1)!

Tactic:
self_le_factorial _

Premises used: Nat.factorial, Nat.self_le_factorial
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
i : ℕ
⊢ i + 1! ≤ (i + 1)!

Tactic:
exact self_le_factorial _

Premises used: Nat.self_le_factorial
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
i h : ℕ
h_1 : Nat.le 1 h
⊢ i + h.succ ! ≤ (i + h.succ)!

Tactic:
add_factorial_succ_le_factorial_add_succ i h

Premises used: Nat.add_factorial_succ_le_factorial_add_succ
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
i h : ℕ
h_1 : Nat.le 1 h
⊢ i + h.succ ! ≤ (i + h.succ)!

Tactic:
exact add_factorial_succ_le_factorial_add_succ i h

Premises used: Nat.add_factorial_succ_le_factorial_add_succ
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n m : ℕ
hnm : n ≤ m
⊢ n ! * n ^ (m - n) ≤ n ! * (n + 1) ^ (m - n)

Tactic:
Nat.mul_le_mul_left _ (Nat.pow_le_pow_left n.le_succ _)

Premises used: Nat.mul_le_mul_left, Nat.le_succ, Nat.pow_le_pow_left
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n m : ℕ
hnm : n ≤ m
⊢ n ! * (n + 1) ^ (m - n) ≤ m !

Tactic:
simpa [hnm] using @Nat.factorial_mul_pow_le_factorial n (m - n)

Premises used: Nat.factorial_mul_pow_le_factorial
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n m : ℕ
hnm : n ≤ m
_ : n ! * (n + 1) ^ (m - n) ≤ m !
⊢ n ! * n ^ (m - n) ≤ m !

Tactic:
calc
    _ ≤ n ! * (n + 1) ^ (m - n) := Nat.mul_le_mul_left _ (Nat.pow_le_pow_left n.le_succ _)
    _ ≤ _ := by simpa [hnm] using @Nat.factorial_mul_pow_le_factorial n (m - n)

Premises used: HSub.hSub, Nat.mul_le_mul_left, Nat.le_succ, HAdd.hAdd, OfNat.ofNat, Nat.pow_le_pow_left
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n : ℕ
rw rw₁ : (n + 1) * (n + 1) ^ n = (n + 1) * (n + 1) ^ n
⊢ (n + 1) * (n + 1) ^ n = (n + 1) ^ (n + 1)

Tactic:
rw [pow_succ']

Premises used: Nat.pow_succ'
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n : ℕ
⊢ n.ascFactorial 0 = 1

Tactic:
rfl

Premises used: Nat.ascFactorial, rfl
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n k : ℕ
⊢ n.ascFactorial k.succ = (n + k) * n.ascFactorial k

Tactic:
rfl

Premises used: Nat.ascFactorial, rfl
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
rw : HAdd.hAdd (α := ℕ) 0 0 * ascFactorial 0 0 = 0
rw₁ : HAdd.hAdd (α := ℕ) 0 0 * 1 = 0
rw₂ : HMul.hMul (α := ℕ) 0 1 = 0
rw₃ rw₄ : Eq (α := ℕ) 0 0
⊢ ascFactorial 0 (succ 0) = 0

Tactic:
rw [ascFactorial_succ, ascFactorial_zero, Nat.zero_add, Nat.zero_mul]

Premises used: Nat.ascFactorial_zero, Nat.ascFactorial_succ, Nat.zero_mul, Nat.zero_add
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
k : ℕ
rw : (0 + (k + 1)) * ascFactorial 0 (k + 1) = 0
rw₁ : (0 + (k + 1)) * 0 = 0
rw₂ rw₃ : Eq (α := ℕ) 0 0
⊢ ascFactorial 0 (k + 1).succ = 0

Tactic:
rw [ascFactorial_succ, zero_ascFactorial k, Nat.mul_zero]

Premises used: Nat.ascFactorial_succ, Nat.mul_zero
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
k : ℕ
rw : (1 + k) * ascFactorial 1 k = (k + 1)!
rw₁ : (1 + k) * k ! = (k + 1)!
rw₂ : (k + 1) * k ! = (k + 1)!
rw₃ rw₄ : (k + 1) * k ! = (k + 1) * k !
⊢ ascFactorial 1 (k + 1) = (k + 1)!

Tactic:
rw [ascFactorial_succ, one_ascFactorial k, Nat.add_comm, factorial_succ]

Premises used: Nat.factorial_succ, Nat.ascFactorial_succ, Nat.add_comm
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n : ℕ
rw : n * n.succ.ascFactorial 0 = n * n.ascFactorial 0
rw₁ : n * 1 = n * n.ascFactorial 0
rw₂ rw₃ : n * 1 = n * 1
⊢ n * n.succ.ascFactorial 0 = (n + 0) * n.ascFactorial 0

Tactic:
rw [Nat.add_zero, ascFactorial_zero, ascFactorial_zero]

Premises used: Nat.ascFactorial_zero, Nat.add_zero
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n k : ℕ
rw : n * ((n.succ + k) * n.succ.ascFactorial k) = (n + (k + 1)) * n.ascFactorial (k + 1)
rw₁ : (n.succ + k) * (n * n.succ.ascFactorial k) = (n + (k + 1)) * n.ascFactorial (k + 1)
rw₂ : (n.succ + k) * ((n + k) * n.ascFactorial k) = (n + (k + 1)) * n.ascFactorial (k + 1)
rw₃ : (n.succ + k) * ((n + k) * n.ascFactorial k) = (n + (k + 1)) * ((n + k) * n.ascFactorial k)
rw₄ : (n + k).succ * ((n + k) * n.ascFactorial k) = (n + (k + 1)) * ((n + k) * n.ascFactorial k)
rw₅ rw₆ : (n + k).succ * ((n + k) * n.ascFactorial k) = (n + k + 1) * ((n + k) * n.ascFactorial k)
⊢ n * n.succ.ascFactorial (k + 1) = (n + (k + 1)) * n.ascFactorial (k + 1)

Tactic:
rw [ascFactorial, Nat.mul_left_comm, succ_ascFactorial n k, ascFactorial, succ_add,
    ← Nat.add_assoc]

Premises used: Nat.mul_left_comm, Nat.ascFactorial, Nat.add_assoc, Nat.succ_add
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n : ℕ
rw : n ! * 1 = (n + 0)!
rw₁ : n ! * 1 = n !
rw₂ rw₃ : n ! = n !
⊢ n ! * (n + 1).ascFactorial 0 = (n + 0)!

Tactic:
rw [ascFactorial_zero, Nat.add_zero, Nat.mul_one]

Premises used: Nat.mul_one, Nat.ascFactorial_zero, Nat.add_zero
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n k : ℕ
rw : n ! * ((n + 1 + k) * (n + 1).ascFactorial k) = (n + (k + 1))!
rw₁ : n ! * ((n + 1 + k) * (n + 1).ascFactorial k) = (n + k + 1)!
rw₂ : n ! * ((n + 1 + k) * (n + 1).ascFactorial k) = (n + k + 1) * (n + k)!
rw₃ : n ! * ((n + 1).ascFactorial k * (n + 1 + k)) = (n + k + 1) * (n + k)!
rw₄ : n ! * (n + 1).ascFactorial k * (n + 1 + k) = (n + k + 1) * (n + k)!
rw₅ : (n + k)! * (n + 1 + k) = (n + k + 1) * (n + k)!
rw₆ : (n + 1 + k) * (n + k)! = (n + k + 1) * (n + k)!
rw₇ rw₈ : (n + k + 1) * (n + k)! = (n + k + 1) * (n + k)!
⊢ n ! * (n + 1).ascFactorial (k + 1) = (n + (k + 1))!

Tactic:
rw [ascFactorial_succ, ← Nat.add_assoc, factorial_succ, Nat.mul_comm (n + 1 + k),
      ← Nat.mul_assoc, factorial_mul_ascFactorial n k, Nat.mul_comm, Nat.add_right_comm]

Premises used: Nat.factorial_succ, Nat.ascFactorial_succ, Nat.mul_comm, Nat.mul_assoc, HAdd.hAdd, Nat.add_assoc, OfNat.ofNat, Nat.add_right_comm
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n k : ℕ
h : 0 < n
rw : n.pred ! * n.ascFactorial k = (n.pred + k)!
⊢ (n - 1)! * n.ascFactorial k = (n + k - 1)!

Tactic:
rw [Nat.sub_add_comm h, Nat.sub_one]

Premises used: Nat.sub_add_comm, Nat.sub_one
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n k : ℕ
h : 0 < n
nth_rw : n.pred ! * (n - succ 0 + succ 0).ascFactorial k = (n.pred + k)!
⊢ n.pred ! * n.ascFactorial k = (n.pred + k)!

Tactic:
nth_rw 2 [Nat.eq_add_of_sub_eq h rfl]

Premises used: Nat.eq_add_of_sub_eq, rfl
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n k : ℕ
h : 0 < n
rw : n.pred ! * (n.pred + succ 0).ascFactorial k = (n.pred + k)!
rw₁ rw₂ : (n.pred + k)! = (n.pred + k)!
⊢ n.pred ! * (n - succ 0 + succ 0).ascFactorial k = (n.pred + k)!

Tactic:
rw [Nat.sub_one, factorial_mul_ascFactorial]

Premises used: Nat.factorial_mul_ascFactorial, Nat.sub_one
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
l k : ℕ
zero : ascFactorial 0 0 * (HAdd.hAdd (α := ℕ) 0 0).ascFactorial k = ascFactorial 0 (0 + k)
zero₁ : ∀ (n : ℕ), ascFactorial 0 (n + 1) * (0 + (n + 1)).ascFactorial k = ascFactorial 0 (n + 1 + k)
⊢ ascFactorial 0 l * (0 + l).ascFactorial k = ascFactorial 0 (l + k)

Tactic:
cases l
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
k : ℕ
⊢ ascFactorial 0 0 * (HAdd.hAdd (α := ℕ) 0 0).ascFactorial k = ascFactorial 0 (0 + k)

Tactic:
simp only [ascFactorial_zero, Nat.add_zero, Nat.one_mul, Nat.zero_add]

Premises used: Nat.ascFactorial_zero, Nat.add_zero, Nat.zero_add, Nat.one_mul
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
k n : ℕ
⊢ ascFactorial 0 (n + 1) * (0 + (n + 1)).ascFactorial k = ascFactorial 0 (n + 1 + k)

Tactic:
simp only [Nat.add_right_comm, zero_ascFactorial, Nat.zero_add, Nat.zero_mul]

Premises used: Nat.zero_mul, Nat.zero_ascFactorial, Nat.zero_add, Nat.add_right_comm
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
l k n' : ℕ
succ : n' ! * ((n' + 1).ascFactorial l * (n' + 1 + l).ascFactorial k) = n' ! * (n' + 1).ascFactorial (l + k)
⊢ (n' + 1).ascFactorial l * (n' + 1 + l).ascFactorial k = (n' + 1).ascFactorial (l + k)

Tactic:
apply Nat.mul_left_cancel (factorial_pos n')

Premises used: Nat.mul_left_cancel, Nat.factorial_pos
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
l k n' : ℕ
succ : (n' + l)! * (n' + (1 + l)).ascFactorial k = (n' + (l + k))!
⊢ n' ! * ((n' + 1).ascFactorial l * (n' + 1 + l).ascFactorial k) = n' ! * (n' + 1).ascFactorial (l + k)

Tactic:
simp only [Nat.add_assoc, ← Nat.mul_assoc, factorial_mul_ascFactorial]

Premises used: Nat.factorial_mul_ascFactorial, Nat.mul_assoc, Nat.add_assoc