row_electron_ae_leading_lower

proof body

Tactic-mode proof.

  64  rw [row_electron_ae_leading_eq]
  65  rw [lt_div_iff₀ ae_den_pos]
  66  have hpiUB : (Real.pi : ℝ) < 3.142 := by
  67    linarith [Real.pi_lt_d6, Real.pi_pos]
  68  have h2piUB : (2 : ℝ) * Real.pi < 2 * 3.142 := by
  69    exact mul_lt_mul_of_pos_left hpiUB (by norm_num)
  70  have hden1 : (2 : ℝ) * Real.pi * alphaInv < (2 * 3.142) * alphaInv := by
  71    exact mul_lt_mul_of_pos_right h2piUB alphaInv_pos
  72  have hden2 : (2 * 3.142 : ℝ) * alphaInv < (2 * 3.142) * (137.039 : ℝ) := by
  73    exact mul_lt_mul_of_pos_left alphaInv_lt (by norm_num)
  74  have hnum : (0.001161 : ℝ) * ((2 * 3.142 : ℝ) * (137.039 : ℝ)) < 1 := by
  75    norm_num
  76  have hLpos : (0 : ℝ) < 0.001161 := by norm_num
  77  have hden : (2 : ℝ) * Real.pi * alphaInv < (2 * 3.142 : ℝ) * (137.039 : ℝ) := by
  78    linarith
  79  have hmul : (0.001161 : ℝ) * ((2 : ℝ) * Real.pi * alphaInv) <
  80      (0.001161 : ℝ) * ((2 * 3.142 : ℝ) * (137.039 : ℝ)) := by
  81    exact mul_lt_mul_of_pos_left hden hLpos
  82  linarith
  83