h2 : _root_.Prime 2
⊢ ∀ {n : ℕ}, n ≠ 0 → multiplicity 2 n ! < ↑n
⊢ ∀ {n : ℕ}, n ≠ 0 → multiplicity 2 n ! < ↑n
have h2 := prime_two.prime
case refine'_1
h2 : _root_.Prime 2
⊢ 0 ≠ 0 → multiplicity 2 0! < ↑0

case refine'_2
h2 : _root_.Prime 2
⊢ ∀ (b : Bool) (n : ℕ), (n ≠ 0 → multiplicity 2 n ! < ↑n) → bit b n ≠ 0 → multiplicity 2 (bit b n)! < ↑(bit b n)
h2 : _root_.Prime 2
⊢ ∀ {n : ℕ}, n ≠ 0 → multiplicity 2 n ! < ↑n
refine' binaryRec _ _
no goals
case refine'_1
h2 : _root_.Prime 2
⊢ 0 ≠ 0 → multiplicity 2 0! < ↑0
exact fun h => False.elim <| h rfl
case refine'_2
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → multiplicity 2 n ! < ↑n
h : bit b n ≠ 0
⊢ multiplicity 2 (bit b n)! < ↑(bit b n)
case refine'_2
h2 : _root_.Prime 2
⊢ ∀ (b : Bool) (n : ℕ), (n ≠ 0 → multiplicity 2 n ! < ↑n) → bit b n ≠ 0 → multiplicity 2 (bit b n)! < ↑(bit b n)
intro b n ih h
case pos
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → multiplicity 2 n ! < ↑n
h : bit b n ≠ 0
hn : n = 0
⊢ multiplicity 2 (bit b n)! < ↑(bit b n)

case neg
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → multiplicity 2 n ! < ↑n
h : bit b n ≠ 0
hn : ¬n = 0
⊢ multiplicity 2 (bit b n)! < ↑(bit b n)
case refine'_2
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → multiplicity 2 n ! < ↑n
h : bit b n ≠ 0
⊢ multiplicity 2 (bit b n)! < ↑(bit b n)
by_cases hn : n = 0
case neg
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → multiplicity 2 n ! < ↑n
h : bit b n ≠ 0
hn : ¬n = 0
this : multiplicity 2 (2 * n)! < ↑(2 * n)
⊢ multiplicity 2 (bit b n)! < ↑(bit b n)
case neg
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → multiplicity 2 n ! < ↑n
h : bit b n ≠ 0
hn : ¬n = 0
⊢ multiplicity 2 (bit b n)! < ↑(bit b n)
have : multiplicity 2 (2 * n)! < (2 * n : ℕ) := by
  rw [prime_two.multiplicity_factorial_mul]
  refine' (PartENat.add_lt_add_right (ih hn) (PartENat.natCast_ne_top _)).trans_le _
  rw [two_mul]
  norm_cast
case neg.false
h2 : _root_.Prime 2
n : ℕ
ih : n ≠ 0 → multiplicity 2 n ! < ↑n
hn : ¬n = 0
this : multiplicity 2 (2 * n)! < ↑(2 * n)
h : bit false n ≠ 0
⊢ multiplicity 2 (bit false n)! < ↑(bit false n)

case neg.true
h2 : _root_.Prime 2
n : ℕ
ih : n ≠ 0 → multiplicity 2 n ! < ↑n
hn : ¬n = 0
this : multiplicity 2 (2 * n)! < ↑(2 * n)
h : bit true n ≠ 0
⊢ multiplicity 2 (bit true n)! < ↑(bit true n)
case neg
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → multiplicity 2 n ! < ↑n
h : bit b n ≠ 0
hn : ¬n = 0
this : multiplicity 2 (2 * n)! < ↑(2 * n)
⊢ multiplicity 2 (bit b n)! < ↑(bit b n)
cases b
case pos
h2 : _root_.Prime 2
b : Bool
ih : 0 ≠ 0 → multiplicity 2 0! < ↑0
h : bit b 0 ≠ 0
⊢ multiplicity 2 (bit b 0)! < ↑(bit b 0)
case pos
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → multiplicity 2 n ! < ↑n
h : bit b n ≠ 0
hn : n = 0
⊢ multiplicity 2 (bit b n)! < ↑(bit b n)
subst hn
case pos
h2 : _root_.Prime 2
b : Bool
ih : 0 ≠ 0 → multiplicity 2 0! < ↑0
h : b = true
⊢ multiplicity 2 (bit b 0)! < ↑(bit b 0)
case pos
h2 : _root_.Prime 2
b : Bool
ih : 0 ≠ 0 → multiplicity 2 0! < ↑0
h : bit b 0 ≠ 0
⊢ multiplicity 2 (bit b 0)! < ↑(bit b 0)
simp only [ne_eq, bit_eq_zero, true_and, Bool.not_eq_false] at h
case pos
h2 : _root_.Prime 2
b : Bool
ih : 0 ≠ 0 → multiplicity 2 0! < ↑0
h : b = true
⊢ multiplicity 2 (succ 0) < 1
case pos
h2 : _root_.Prime 2
b : Bool
ih : 0 ≠ 0 → multiplicity 2 0! < ↑0
h : b = true
⊢ multiplicity 2 (bit b 0)! < ↑(bit b 0)
simp only [h, bit_true, bit1_zero, factorial, mul_one, Nat.isUnit_iff, cast_one]
case pos
h2 : _root_.Prime 2
b : Bool
ih : 0 ≠ 0 → multiplicity 2 0! < ↑0
h : b = true
⊢ 0 < 1

case pos
h2 : _root_.Prime 2
b : Bool
ih : 0 ≠ 0 → multiplicity 2 0! < ↑0
h : b = true
⊢ Prime 2
case pos
h2 : _root_.Prime 2
b : Bool
ih : 0 ≠ 0 → multiplicity 2 0! < ↑0
h : b = true
⊢ multiplicity 2 (succ 0) < 1
rw [Prime.multiplicity_one]
case pos
h2 : _root_.Prime 2
b : Bool
ih : 0 ≠ 0 → multiplicity 2 0! < ↑0
h : b = true
⊢ Prime 2
case pos
h2 : _root_.Prime 2
b : Bool
ih : 0 ≠ 0 → multiplicity 2 0! < ↑0
h : b = true
⊢ 0 < 1

case pos
h2 : _root_.Prime 2
b : Bool
ih : 0 ≠ 0 → multiplicity 2 0! < ↑0
h : b = true
⊢ Prime 2
simp only [zero_lt_one]
no goals
case pos
h2 : _root_.Prime 2
b : Bool
ih : 0 ≠ 0 → multiplicity 2 0! < ↑0
h : b = true
⊢ Prime 2
decide
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → multiplicity 2 n ! < ↑n
h : bit b n ≠ 0
hn : ¬n = 0
⊢ multiplicity 2 n ! + ↑n < ↑(2 * n)
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → multiplicity 2 n ! < ↑n
h : bit b n ≠ 0
hn : ¬n = 0
⊢ multiplicity 2 (2 * n)! < ↑(2 * n)
rw [prime_two.multiplicity_factorial_mul]
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → multiplicity 2 n ! < ↑n
h : bit b n ≠ 0
hn : ¬n = 0
⊢ ↑n + ↑n ≤ ↑(2 * n)
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → multiplicity 2 n ! < ↑n
h : bit b n ≠ 0
hn : ¬n = 0
⊢ multiplicity 2 n ! + ↑n < ↑(2 * n)
refine' (PartENat.add_lt_add_right (ih hn) (PartENat.natCast_ne_top _)).trans_le _
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → multiplicity 2 n ! < ↑n
h : bit b n ≠ 0
hn : ¬n = 0
⊢ ↑n + ↑n ≤ ↑(n + n)
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → multiplicity 2 n ! < ↑n
h : bit b n ≠ 0
hn : ¬n = 0
⊢ ↑n + ↑n ≤ ↑(2 * n)
rw [two_mul]
no goals
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → multiplicity 2 n ! < ↑n
h : bit b n ≠ 0
hn : ¬n = 0
⊢ ↑n + ↑n ≤ ↑(n + n)
norm_cast
no goals
case neg.false
h2 : _root_.Prime 2
n : ℕ
ih : n ≠ 0 → multiplicity 2 n ! < ↑n
hn : ¬n = 0
this : multiplicity 2 (2 * n)! < ↑(2 * n)
h : bit false n ≠ 0
⊢ multiplicity 2 (bit false n)! < ↑(bit false n)
simpa [bit0_eq_two_mul n]
case neg.true
h2 : _root_.Prime 2
n : ℕ
ih : n ≠ 0 → multiplicity 2 n ! < ↑n
hn : ¬n = 0
this : multiplicity 2 (2 * n)! < ↑(2 * n)
h : bit true n ≠ 0
⊢ multiplicity 2 (2 * n + 1) + multiplicity 2 (2 * n)! < ↑(2 * n) + 1
case neg.true
h2 : _root_.Prime 2
n : ℕ
ih : n ≠ 0 → multiplicity 2 n ! < ↑n
hn : ¬n = 0
this : multiplicity 2 (2 * n)! < ↑(2 * n)
h : bit true n ≠ 0
⊢ multiplicity 2 (bit true n)! < ↑(bit true n)
suffices multiplicity 2 (2 * n + 1) + multiplicity 2 (2 * n)! < ↑(2 * n) + 1 by
  simpa [succ_eq_add_one, multiplicity.mul, h2, prime_two, Nat.bit1_eq_succ_bit0,
    bit0_eq_two_mul n]
case neg.true
h2 : _root_.Prime 2
n : ℕ
ih : n ≠ 0 → multiplicity 2 n ! < ↑n
hn : ¬n = 0
this : multiplicity 2 (2 * n)! < ↑(2 * n)
h : bit true n ≠ 0
⊢ multiplicity 2 (2 * n)! < ↑(2 * n) + 1
case neg.true
h2 : _root_.Prime 2
n : ℕ
ih : n ≠ 0 → multiplicity 2 n ! < ↑n
hn : ¬n = 0
this : multiplicity 2 (2 * n)! < ↑(2 * n)
h : bit true n ≠ 0
⊢ multiplicity 2 (2 * n + 1) + multiplicity 2 (2 * n)! < ↑(2 * n) + 1
rw [multiplicity_eq_zero.2 (two_not_dvd_two_mul_add_one n), zero_add]
case neg.true
h2 : _root_.Prime 2
n : ℕ
ih : n ≠ 0 → multiplicity 2 n ! < ↑n
hn : ¬n = 0
this : multiplicity 2 (2 * n)! < ↑(2 * n)
h : bit true n ≠ 0
⊢ ↑(2 * n) < ↑(2 * n) + 1
case neg.true
h2 : _root_.Prime 2
n : ℕ
ih : n ≠ 0 → multiplicity 2 n ! < ↑n
hn : ¬n = 0
this : multiplicity 2 (2 * n)! < ↑(2 * n)
h : bit true n ≠ 0
⊢ multiplicity 2 (2 * n)! < ↑(2 * n) + 1
refine' this.trans _
no goals
case neg.true
h2 : _root_.Prime 2
n : ℕ
ih : n ≠ 0 → multiplicity 2 n ! < ↑n
hn : ¬n = 0
this : multiplicity 2 (2 * n)! < ↑(2 * n)
h : bit true n ≠ 0
⊢ ↑(2 * n) < ↑(2 * n) + 1
exact_mod_cast lt_succ_self _
no goals
h2 : _root_.Prime 2
n : ℕ
ih : n ≠ 0 → multiplicity 2 n ! < ↑n
hn : ¬n = 0
this✝ : multiplicity 2 (2 * n)! < ↑(2 * n)
h : bit true n ≠ 0
this : multiplicity 2 (2 * n + 1) + multiplicity 2 (2 * n)! < ↑(2 * n) + 1
⊢ multiplicity 2 (bit true n)! < ↑(bit true n)
simpa [succ_eq_add_one, multiplicity.mul, h2, prime_two, Nat.bit1_eq_succ_bit0,
  bit0_eq_two_mul n]