cor_5_1_rem'

theorem cor_5_1_rem' (b a₂b : ℝ) (m : ℕ)    (hb : (b, a₂b, m) ∈ table_cor_5_1) :    a₂ b ∈ Set.Icc a₂b (a₂b + 10 ^ (-m : ℝ)) := by  -- Unfold a₂ to (1+α) * max(f(exp b), f(2^(⌊b/log2⌋₊+1)))  unfold a₂ Inputs.a₂  rw [alpha_eq]  -- Case split on table membership  simp only [table_cor_5_1, List.mem_cons, Prod.mk.injEq, List.mem_nil_iff, or_false] at hb  rcases hb with    ⟨rfl, rfl, rfl⟩ | ⟨rfl, rfl, rfl⟩ |    ⟨rfl, rfl, rfl⟩ | ⟨rfl, rfl, rfl⟩ |    ⟨rfl, rfl, rfl⟩ | ⟨rfl, rfl, rfl⟩ |    ⟨rfl, rfl, rfl⟩ | ⟨rfl, rfl, rfl⟩ |    ⟨rfl, rfl, rfl⟩ | ⟨rfl, rfl, rfl⟩ |    ⟨rfl, rfl, rfl⟩  · rw [rpow_neg_nat]; exact a2_20_mem_Icc  · rw [rpow_neg_nat]; exact a2_25_mem_Icc  · rw [rpow_neg_nat]; exact a2_30_mem_Icc  · rw [rpow_neg_nat]; exact a2_35_mem_Icc  · rw [rpow_neg_nat]; exact a2_40_mem_Icc  · rw [rpow_neg_nat]; exact a2_43_mem_Icc  · rw [show (1 + 2.420e-4 : ℝ) = (1.0002420 : ℝ) from by norm_num, rpow_neg_nat]    exact a2_100_mem_Icc  · rw [show (1 + 3.748e-6 : ℝ) = (1.000003748 : ℝ) from by norm_num, rpow_neg_nat]    exact a2_150_mem_Icc  · rw [show (1 + 7.713e-8 : ℝ) = (1.00000007713 : ℝ) from by norm_num, rpow_neg_nat]    exact a2_200_mem_Icc  · rw [show (1 + 2.025e-8 : ℝ) = (1.00000002025 : ℝ) from by norm_num, rpow_neg_nat]    exact a2_250_mem_Icc  · rw [show (1 + 1.937e-8 : ℝ) = (1.00000001937 : ℝ) from by norm_num, rpow_neg_nat]    exact a2_300_mem_Icc