From d7992bd8884974f7cd00a2b64d511430c8075c09 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Sat, 16 Dec 2023 13:39:08 +0000
Subject: [PATCH 1/2] feat: The double factorial is positive and other basic
 results. Also include a positivity extension to encode that new result.

From LeanAPAP
---
 Mathlib/Data/Nat/Factorial/Basic.lean         | 12 +++++++++
 Mathlib/Data/Nat/Factorial/BigOperators.lean  | 11 +++-----
 .../Data/Nat/Factorial/DoubleFactorial.lean   | 27 +++++++++++++++++++
 3 files changed, 43 insertions(+), 7 deletions(-)

diff --git a/Mathlib/Data/Nat/Factorial/Basic.lean b/Mathlib/Data/Nat/Factorial/Basic.lean
index 0d7f963f8dda6..ec643a6748320 100644
--- a/Mathlib/Data/Nat/Factorial/Basic.lean
+++ b/Mathlib/Data/Nat/Factorial/Basic.lean
@@ -456,4 +456,16 @@ theorem descFactorial_lt_pow {n : ℕ} (hn : 1 ≤ n) : ∀ {k : ℕ}, 2 ≤ k 
 
 end DescFactorial
 
+lemma factorial_two_mul_le (n : ℕ) : (2 * n)! ≤ (2 * n) ^ n * n ! := by
+  rw [two_mul, ←factorial_mul_ascFactorial, mul_comm]
+  exact mul_le_mul_right' (ascFactorial_le_pow_add _ _) _
+
+lemma two_pow_mul_factorial_le_factorial_two_mul (n : ℕ) : 2 ^ n * n ! ≤ (2 * n) ! := by
+  obtain _ | n := n
+  · simp
+  rw [mul_comm, two_mul]
+  calc
+    _ ≤ (n + 1)! * (n + 2) ^ (n + 1) := mul_le_mul_left' (pow_le_pow_of_le_left le_add_self _) _
+    _ ≤ _ := Nat.factorial_mul_pow_le_factorial
+
 end Nat
diff --git a/Mathlib/Data/Nat/Factorial/BigOperators.lean b/Mathlib/Data/Nat/Factorial/BigOperators.lean
index 642ba3f562abb..bfb6a8406ef8b 100644
--- a/Mathlib/Data/Nat/Factorial/BigOperators.lean
+++ b/Mathlib/Data/Nat/Factorial/BigOperators.lean
@@ -30,13 +30,10 @@ theorem prod_factorial_pos : 0 < ∏ i in s, (f i)! :=
 #align nat.prod_factorial_pos Nat.prod_factorial_pos
 
 theorem prod_factorial_dvd_factorial_sum : (∏ i in s, (f i)!) ∣ (∑ i in s, f i)! := by
-  classical
-    induction' s using Finset.induction with a' s' has ih
-    · simp only [prod_empty, factorial, dvd_refl]
-    · simp only [Finset.prod_insert has, Finset.sum_insert has]
-      refine' dvd_trans (mul_dvd_mul_left (f a')! ih) _
-      apply Nat.factorial_mul_factorial_dvd_factorial_add
-#align nat.prod_factorial_dvd_factorial_sum Nat.prod_factorial_dvd_factorial_sum
+  induction' s using Finset.cons_induction_on with a s has ih
+  · simp
+  · rw [prod_cons, Finset.sum_cons]
+    exact (mul_dvd_mul_left _ ih).trans (Nat.factorial_mul_factorial_dvd_factorial_add _ _)
 
 theorem descFactorial_eq_prod_range (n : ℕ) : ∀ k, n.descFactorial k = ∏ i in range k, (n - i)
   | 0 => rfl
diff --git a/Mathlib/Data/Nat/Factorial/DoubleFactorial.lean b/Mathlib/Data/Nat/Factorial/DoubleFactorial.lean
index a023aca76229f..1bda3a8a658b5 100644
--- a/Mathlib/Data/Nat/Factorial/DoubleFactorial.lean
+++ b/Mathlib/Data/Nat/Factorial/DoubleFactorial.lean
@@ -36,6 +36,10 @@ def doubleFactorial : ℕ → ℕ
 -- This notation is `\!!` not two !'s
 scoped notation:10000 n "‼" => Nat.doubleFactorial n
 
+lemma doubleFactorial_pos : ∀ n, 0 < n‼
+  | 0 | 1 => zero_lt_one
+  | _n + 2 => mul_pos (succ_pos _) (doubleFactorial_pos _)
+
 theorem doubleFactorial_add_two (n : ℕ) : (n + 2)‼ = (n + 2) * n‼ :=
   rfl
 #align nat.double_factorial_add_two Nat.doubleFactorial_add_two
@@ -50,6 +54,11 @@ theorem factorial_eq_mul_doubleFactorial : ∀ n : ℕ, (n + 1)! = (n + 1)‼ *
       mul_assoc]
 #align nat.factorial_eq_mul_double_factorial Nat.factorial_eq_mul_doubleFactorial
 
+lemma doubleFactorial_le_factorial : ∀ n, n‼ ≤ n !
+  | 0 => le_rfl
+  | n + 1 => by
+    rw [factorial_eq_mul_doubleFactorial]; exact le_mul_of_pos_right n.doubleFactorial_pos
+
 theorem doubleFactorial_two_mul : ∀ n : ℕ, (2 * n)‼ = 2 ^ n * n !
   | 0 => rfl
   | n + 1 => by
@@ -78,3 +87,21 @@ theorem doubleFactorial_eq_prod_odd :
 #align nat.double_factorial_eq_prod_odd Nat.doubleFactorial_eq_prod_odd
 
 end Nat
+
+namespace Mathlib.Meta.Positivity
+open Lean Meta Qq
+
+/-- Extension for `Nat.doubleFactorial`. -/
+@[positivity Nat.doubleFactorial _]
+def evalDoubleFactorial : PositivityExt where eval {u α} _ _ e := do
+  if let 0 := u then -- lean4#3060 means we can't combine this with the match below
+    match α, e with
+    | ~q(ℕ), ~q(Nat.doubleFactorial $n) =>
+      assumeInstancesCommute
+      return .positive q(Nat.doubleFactorial_pos $n)
+    | _, _ => throwError "not Nat.doubleFactorial"
+  else throwError "not Nat.doubleFactorial"
+
+example (n : ℕ) : 0 < n‼ := by positivity
+
+end Mathlib.Meta.Positivity

From 1425514f75ee694c2748c5f976b086caf12d5505 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Sat, 16 Dec 2023 13:42:16 +0000
Subject: [PATCH 2/2] style

---
 Mathlib/Data/Nat/Factorial/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Data/Nat/Factorial/Basic.lean b/Mathlib/Data/Nat/Factorial/Basic.lean
index ec643a6748320..5bb949b00547b 100644
--- a/Mathlib/Data/Nat/Factorial/Basic.lean
+++ b/Mathlib/Data/Nat/Factorial/Basic.lean
@@ -457,7 +457,7 @@ theorem descFactorial_lt_pow {n : ℕ} (hn : 1 ≤ n) : ∀ {k : ℕ}, 2 ≤ k 
 end DescFactorial
 
 lemma factorial_two_mul_le (n : ℕ) : (2 * n)! ≤ (2 * n) ^ n * n ! := by
-  rw [two_mul, ←factorial_mul_ascFactorial, mul_comm]
+  rw [two_mul, ← factorial_mul_ascFactorial, mul_comm]
   exact mul_le_mul_right' (ascFactorial_le_pow_add _ _) _
 
 lemma two_pow_mul_factorial_le_factorial_two_mul (n : ℕ) : 2 ^ n * n ! ≤ (2 * n) ! := by