Lcm.Criterion.val_two_L'

lemma Criterion.val_two_L' (c : Criterion) : (c.L').factorization 2 = Nat.log 2 c.n := by  have h_lcm : ∀ n : ℕ, n ≥ 1 → Nat.factorization (L n) 2 = Nat.log 2 n := by    have h_lcm_exp : ∀ n : ℕ, n ≥ 1 → (Nat.factorization (Finset.lcm (Finset.Icc 1 n)        (fun x ↦ x)) 2) = Finset.sup (Finset.Icc 1 n) (fun x ↦ Nat.factorization x 2) := by      intros n hn      have h_lcm_exp : ∀ {S : Finset ℕ}, (∀ x ∈ S, x ≠ 0) → (Nat.factorization (Finset.lcm S          (fun x ↦ x)) 2) = Finset.sup S (fun x ↦ Nat.factorization x 2) := by        intro S hS        induction S using Finset.induction with        | empty => simp        | insert x S hxS ih =>            simp_all only [lcm_insert]            erw [Nat.factorization_lcm] <;> simp_all      exact h_lcm_exp fun x hx ↦ by linarith [Finset.mem_Icc.mp hx]    have h_sup : ∀ n : ℕ, n ≥ 1 → Finset.sup (Finset.Icc 1 n) (fun x ↦ Nat.factorization x 2) =       Nat.log 2 n := fun n hn ↦ by      apply le_antisymm      · exact Finset.sup_le fun x hx ↦ Nat.le_log_of_pow_le (by decide) <|          Nat.le_trans (Nat.le_of_dvd (by linarith [Finset.mem_Icc.mp hx])          <| Nat.ordProj_dvd _ _) <| by linarith [Finset.mem_Icc.mp hx]      · refine le_trans ?_ (Finset.le_sup <| Finset.mem_Icc.mpr ⟨Nat.one_le_pow _ _ zero_lt_two,          Nat.pow_log_le_self 2 <| by linarith⟩)        norm_num [Nat.Prime.factorization_self (prime_two)]    aesop  rw [show c.L' = L c.n / (∏ i, c.q i) by rfl, Nat.factorization_div] <;> norm_num [h_lcm, c.hn]  · rw [Nat.factorization_eq_zero_of_not_dvd] <;> norm_num [Fin.prod_univ_three]    norm_num [Nat.mul_mod, Nat.mod_mod, Nat.odd_iff.mp (Nat.Prime.odd_of_ne_two (c.hq 0)      (by linarith [c.p_gt_two 0, c.q_gt_two 0])), Nat.odd_iff.mp (Nat.Prime.odd_of_ne_two (c.hq 1)      (by linarith [c.p_gt_two 1, c.q_gt_two 1])), Nat.odd_iff.mp (Nat.Prime.odd_of_ne_two (c.hq 2)      (by linarith [c.p_gt_two 2, c.q_gt_two 2]))]  · exact prod_q_dvd_L c