-- Mathlib/Data/Nat/Multiplicity.lean
theorem emultiplicity_two_factorial_lt : ∀ {n : ℕ} (_ : n ≠ 0), emultiplicity 2 n ! < n

Proof state:
⊢ ∀ {n : ℕ}, n ≠ 0 → emultiplicity 2 n ! < ↑n

Tactic:
have h2 := prime_two.prime

Result:
h2 : _root_.Prime 2
⊢ ∀ {n : ℕ}, n ≠ 0 → emultiplicity 2 n ! < ↑n

Proof state:
case pos
h2 : _root_.Prime 2
b : Bool
ih : 0 ≠ 0 → emultiplicity 2 0! < ↑0
h : b = true
⊢ emultiplicity 2 1 < ↑1

Tactic:
rw [Prime.emultiplicity_one]

Result:
case pos
h2 : _root_.Prime 2
b : Bool
ih : 0 ≠ 0 → emultiplicity 2 0! < ↑0
h : b = true
⊢ 0 < ↑1

case pos
h2 : _root_.Prime 2
b : Bool
ih : 0 ≠ 0 → emultiplicity 2 0! < ↑0
h : b = true
⊢ Prime 2

Proof state:
h2 : _root_.Prime 2
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
hn : ¬n = 0
this✝ : emultiplicity 2 (2 * n)! < ↑(2 * n)
h : bit true n ≠ 0
this : emultiplicity 2 (2 * n + 1) + emultiplicity 2 (2 * n)! < ↑(2 * n) + 1
⊢ emultiplicity 2 (bit true n)! < ↑(bit true n)

Tactic:
simpa [emultiplicity_mul, h2, prime_two, bit, factorial]

Result:
no goals

Proof state:
case neg.true
h2 : _root_.Prime 2
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
hn : ¬n = 0
this : emultiplicity 2 (2 * n)! < ↑(2 * n)
h : bit true n ≠ 0
⊢ emultiplicity 2 (bit true n)! < ↑(bit true n)

Tactic:
suffices emultiplicity 2 (2 * n + 1) + emultiplicity 2 (2 * n)! < ↑(2 * n) + 1 by
  simpa [emultiplicity_mul, h2, prime_two, bit, factorial]

Result:
case neg.true
h2 : _root_.Prime 2
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
hn : ¬n = 0
this : emultiplicity 2 (2 * n)! < ↑(2 * n)
h : bit true n ≠ 0
⊢ emultiplicity 2 (2 * n + 1) + emultiplicity 2 (2 * n)! < ↑(2 * n) + 1

Proof state:
case neg
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
h : bit b n ≠ 0
hn : ¬n = 0
this : emultiplicity 2 (2 * n)! < ↑(2 * n)
⊢ emultiplicity 2 (bit b n)! < ↑(bit b n)

Tactic:
cases b

Result:
case neg.false
h2 : _root_.Prime 2
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
hn : ¬n = 0
this : emultiplicity 2 (2 * n)! < ↑(2 * n)
h : bit false n ≠ 0
⊢ emultiplicity 2 (bit false n)! < ↑(bit false n)

case neg.true
h2 : _root_.Prime 2
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
hn : ¬n = 0
this : emultiplicity 2 (2 * n)! < ↑(2 * n)
h : bit true n ≠ 0
⊢ emultiplicity 2 (bit true n)! < ↑(bit true n)

Proof state:
case neg.true
h2 : _root_.Prime 2
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
hn : ¬n = 0
this : emultiplicity 2 (2 * n)! < ↑(2 * n)
h : bit true n ≠ 0
⊢ ↑(2 * n) < ↑(2 * n) + 1

Tactic:
exact mod_cast lt_succ_self _

Result:
no goals

Proof state:
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
h : bit b n ≠ 0
hn : ¬n = 0
⊢ emultiplicity 2 n ! + ↑n < ↑n + ↑n

Tactic:
apply WithTop.add_lt_add_right _ (ih hn)

Result:
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
h : bit b n ≠ 0
hn : ¬n = 0
⊢ ↑n ≠ ⊤

Proof state:
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
h : bit b n ≠ 0
hn : ¬n = 0
⊢ emultiplicity 2 n ! + ↑n < ↑(2 * n)

Tactic:
rw [two_mul]

Result:
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
h : bit b n ≠ 0
hn : ¬n = 0
⊢ emultiplicity 2 n ! + ↑n < ↑(n + n)

Proof state:
case neg.true
h2 : _root_.Prime 2
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
hn : ¬n = 0
this : emultiplicity 2 (2 * n)! < ↑(2 * n)
h : bit true n ≠ 0
⊢ emultiplicity 2 (2 * n + 1) + emultiplicity 2 (2 * n)! < ↑(2 * n) + 1

Tactic:
rw [emultiplicity_eq_zero.2 (two_not_dvd_two_mul_add_one n), zero_add]

Result:
case neg.true
h2 : _root_.Prime 2
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
hn : ¬n = 0
this : emultiplicity 2 (2 * n)! < ↑(2 * n)
h : bit true n ≠ 0
⊢ emultiplicity 2 (2 * n)! < ↑(2 * n) + 1

Proof state:
case refine_2
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
h : bit b n ≠ 0
⊢ emultiplicity 2 (bit b n)! < ↑(bit b n)

Tactic:
by_cases hn : n = 0

Result:
case pos
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
h : bit b n ≠ 0
hn : n = 0
⊢ emultiplicity 2 (bit b n)! < ↑(bit b n)

case neg
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
h : bit b n ≠ 0
hn : ¬n = 0
⊢ emultiplicity 2 (bit b n)! < ↑(bit b n)

Proof state:
case neg.false
h2 : _root_.Prime 2
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
hn : ¬n = 0
this : emultiplicity 2 (2 * n)! < ↑(2 * n)
h : bit false n ≠ 0
⊢ emultiplicity 2 (bit false n)! < ↑(bit false n)

Tactic:
simpa

Result:
no goals

Proof state:
case pos
h2 : _root_.Prime 2
b : Bool
ih : 0 ≠ 0 → emultiplicity 2 0! < ↑0
h : b = true
⊢ Prime 2

Tactic:
decide

Result:
no goals

Proof state:
case pos
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
h : bit b n ≠ 0
hn : n = 0
⊢ emultiplicity 2 (bit b n)! < ↑(bit b n)

Tactic:
subst hn

Result:
case pos
h2 : _root_.Prime 2
b : Bool
ih : 0 ≠ 0 → emultiplicity 2 0! < ↑0
h : bit b 0 ≠ 0
⊢ emultiplicity 2 (bit b 0)! < ↑(bit b 0)

Proof state:
case neg
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
h : bit b n ≠ 0
hn : ¬n = 0
⊢ emultiplicity 2 (bit b n)! < ↑(bit b n)

Tactic:
have : emultiplicity 2 (2 * n)! < (2 * n : ℕ) := by
  rw [prime_two.emultiplicity_factorial_mul]
  rw [two_mul]
  push_cast
  apply WithTop.add_lt_add_right _ (ih hn)
  exact Ne.symm nofun

Result:
case neg
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
h : bit b n ≠ 0
hn : ¬n = 0
this : emultiplicity 2 (2 * n)! < ↑(2 * n)
⊢ emultiplicity 2 (bit b n)! < ↑(bit b n)

Proof state:
case pos
h2 : _root_.Prime 2
b : Bool
ih : 0 ≠ 0 → emultiplicity 2 0! < ↑0
h : b = true
⊢ 0 < ↑1

Tactic:
exact zero_lt_one

Result:
no goals

Proof state:
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
h : bit b n ≠ 0
hn : ¬n = 0
⊢ emultiplicity 2 n ! + ↑n < ↑(n + n)

Tactic:
push_cast

Result:
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
h : bit b n ≠ 0
hn : ¬n = 0
⊢ emultiplicity 2 n ! + ↑n < ↑n + ↑n

Proof state:
case pos
h2 : _root_.Prime 2
b : Bool
ih : 0 ≠ 0 → emultiplicity 2 0! < ↑0
h : b = true
⊢ emultiplicity 2 (bit b 0)! < ↑(bit b 0)

Tactic:
simp only [bit, h, cond_true, mul_zero, zero_add, factorial_one]

Result:
case pos
h2 : _root_.Prime 2
b : Bool
ih : 0 ≠ 0 → emultiplicity 2 0! < ↑0
h : b = true
⊢ emultiplicity 2 1 < ↑1

Proof state:
case pos
h2 : _root_.Prime 2
b : Bool
ih : 0 ≠ 0 → emultiplicity 2 0! < ↑0
h : bit b 0 ≠ 0
⊢ emultiplicity 2 (bit b 0)! < ↑(bit b 0)

Tactic:
simp only [ne_eq, bit_eq_zero_iff, true_and, Bool.not_eq_false] at h

Result:
case pos
h2 : _root_.Prime 2
b : Bool
ih : 0 ≠ 0 → emultiplicity 2 0! < ↑0
h : b = true
⊢ emultiplicity 2 (bit b 0)! < ↑(bit b 0)

Proof state:
case refine_2
h2 : _root_.Prime 2
⊢ ∀ (b : Bool) (n : ℕ), (n ≠ 0 → emultiplicity 2 n ! < ↑n) → bit b n ≠ 0 → emultiplicity 2 (bit b n)! < ↑(bit b n)

Tactic:
intro b n ih h

Result:
case refine_2
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
h : bit b n ≠ 0
⊢ emultiplicity 2 (bit b n)! < ↑(bit b n)

Proof state:
h2 : _root_.Prime 2
⊢ ∀ {n : ℕ}, n ≠ 0 → emultiplicity 2 n ! < ↑n

Tactic:
refine binaryRec ?_ ?_

Result:
case refine_1
h2 : _root_.Prime 2
⊢ 0 ≠ 0 → emultiplicity 2 0! < ↑0

case refine_2
h2 : _root_.Prime 2
⊢ ∀ (b : Bool) (n : ℕ), (n ≠ 0 → emultiplicity 2 n ! < ↑n) → bit b n ≠ 0 → emultiplicity 2 (bit b n)! < ↑(bit b n)

Proof state:
case refine_1
h2 : _root_.Prime 2
⊢ 0 ≠ 0 → emultiplicity 2 0! < ↑0

Tactic:
exact fun h => False.elim <| h rfl

Result:
no goals

Proof state:
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
h : bit b n ≠ 0
hn : ¬n = 0
⊢ ↑n ≠ ⊤

Tactic:
exact Ne.symm nofun

Result:
no goals

Proof state:
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
h : bit b n ≠ 0
hn : ¬n = 0
⊢ emultiplicity 2 (2 * n)! < ↑(2 * n)

Tactic:
rw [prime_two.emultiplicity_factorial_mul]

Result:
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
h : bit b n ≠ 0
hn : ¬n = 0
⊢ emultiplicity 2 n ! + ↑n < ↑(2 * n)