Theorem: Hilbert_kernel_regularity_main_part
Proof state before:
y y' : ℝ
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' ≤ 1
⊢ ‖(1 - ↑|(-y)|) / (1 - (Complex.I * ↑(-y)).exp) - (1 - ↑|(-y')|) / (1 - (Complex.I * ↑(-y')).exp)‖ ≤
    2 ^ 6 * (1 / |y|) * (|y - y'| / |y|)

y y' : ℝ
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' ≤ 1
⊢ |(-y')| ≤ 1

y y' : ℝ
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' ≤ 1
⊢ |(-y)| ≤ 1
Tactic:
. simp only [abs_neg, Complex.ofReal_neg, mul_neg, ge_iff_le]
  rw [abs_of_nonneg yy'nonneg.1, abs_of_nonneg yy'nonneg.2]
  let f : ℝ → ℂ := fun t ↦ (1 - t) / (1 - Complex.exp (-(Complex.I * t)))
  set f' : ℝ → ℂ := fun t ↦ (-1 + Complex.exp (-(Complex.I * t)) + Complex.I * (t - 1) * Complex.exp (-(Complex.I * t))) / (1 - Complex.exp (-(Complex.I * t))) ^ 2 with f'def
  
  set c : ℝ → ℂ := fun t ↦ (1 - t) with cdef
  set c' : ℝ → ℂ := fun t ↦ -1 with c'def
  set d : ℝ → ℂ := fun t ↦ (1 - Complex.exp (-(Complex.I * t))) with ddef
  set d' : ℝ → ℂ := fun t ↦ Complex.I * Complex.exp (-(Complex.I * t)) with d'def
  have d_nonzero {t : ℝ} (ht : t ∈ Set.uIcc y' y) : d t ≠ 0 := by
    rw [Set.mem_uIcc] at ht
    have ht' : 0 < t ∧ t ≤ 1 := by
      rcases ht with ht | ht <;> (constructor <;> linarith)
    rw [ddef]
    simp
    rw [←norm_eq_zero]
    apply ne_of_gt
    calc ‖1 - Complex.exp (-(Complex.I * ↑t))‖
      _ ≥ |(1 - Complex.exp (-(Complex.I * ↑t))).im| := by
        simp only [Complex.norm_eq_abs, ge_iff_le]
        apply Complex.abs_im_le_abs
      _ = Real.sin t := by
        simp
        rw [Complex.exp_im]
        simp
        apply Real.sin_nonneg_of_nonneg_of_le_pi
        . linarith
        . linarith [Real.two_le_pi]
      _ > 0 := by
        apply Real.sin_pos_of_pos_of_lt_pi
        . linarith
        . linarith [Real.two_le_pi]
  have f_deriv : ∀ t ∈ Set.uIcc y' y, HasDerivAt f (f' t) t := by
    intro t ht
    have : f = fun t ↦ c t / d t := by simp
    rw [this]
    have : f' = fun t ↦ ((c' t * d t - c t * d' t) / d t ^ 2) := by
      ext t
      rw [f'def, cdef, c'def, ddef, d'def]
      simp
      congr
      ring
    rw [this]
    apply HasDerivAt.div
    . rw [cdef, c'def]
      simp
      apply HasDerivAt.const_sub
      apply HasDerivAt.ofReal_comp
      apply hasDerivAt_id'
    . rw [ddef, d'def]
      simp
      rw [←neg_neg (Complex.I * Complex.exp (-(Complex.I * ↑t)))]
      apply HasDerivAt.const_sub
      rw [←neg_mul, mul_comm]
      apply HasDerivAt.cexp
      apply HasDerivAt.neg
      conv in fun (x : ℝ) ↦ Complex.I * (x : ℝ) =>
        ext
        rw [mul_comm]
      set e : ℂ → ℂ := fun t ↦ t * Complex.I with edef
      have : (fun (t : ℝ) ↦ t * Complex.I) = fun (t : ℝ) ↦ e t := by
        rw [edef]
      rw [this]
      apply HasDerivAt.comp_ofReal
      rw [edef]
      apply hasDerivAt_mul_const
    . exact d_nonzero ht
  have f'_cont : ContinuousOn (fun t ↦ f' t) (Set.uIcc y' y) := by
    apply ContinuousOn.div
    . apply Continuous.continuousOn
      continuity
    . 
      apply Continuous.continuousOn
      apply Continuous.pow
      apply Continuous.sub
      . apply continuous_const
      . apply Continuous.cexp
        apply Continuous.neg
        apply Continuous.mul
        . apply continuous_const
        . apply Complex.continuous_ofReal
    . intro t ht
      simp
      apply d_nonzero ht
  calc ‖(1 - ↑y) / (1 - Complex.exp (-(Complex.I * ↑y))) - (1 - ↑y') / (1 - Complex.exp (-(Complex.I * ↑y')))‖
    _ = ‖f y - f y'‖ := by simp
    _ = ‖∫ (t : ℝ) in y'..y, f' t‖ := by
      congr 1
      rw [intervalIntegral.integral_eq_sub_of_hasDerivAt]
      . exact f_deriv
      . apply f'_cont.intervalIntegrable
    _ = ‖∫ (t : ℝ) in Ι y' y, f' t‖ := by
      apply intervalIntegral.norm_intervalIntegral_eq
    _ ≤ ∫ (t : ℝ) in Ι y' y, ‖f' t‖ := by
      apply MeasureTheory.norm_integral_le_integral_norm
    _ ≤ ∫ (t : ℝ) in Ι y' y, 3 / ((y / 2) / 2) ^ 2 := by
      apply MeasureTheory.setIntegral_mono_on
      . apply f'_cont.norm.integrableOn_uIcc.mono_set
        apply Set.Ioc_subset_Icc_self
      . apply MeasureTheory.integrableOn_const.mpr
        right
        rw [Real.volume_uIoc]
        apply ENNReal.ofReal_lt_top
      . apply measurableSet_uIoc
      . intro t ht
        rw [Set.mem_uIoc] at ht
        have ht' : 0 < t ∧ t ≤ 1 := by
          rcases ht with ht | ht <;> (constructor <;> linarith)
        rw [f'def]
        simp only [norm_div, Complex.norm_eq_abs, norm_pow]
        gcongr
        . calc Complex.abs (-1 + Complex.exp (-(Complex.I * ↑t)) + Complex.I * (↑t - 1) * Complex.exp (-(Complex.I * ↑t)))
            _ ≤ Complex.abs (-1 + Complex.exp (-(Complex.I * ↑t))) + Complex.abs (Complex.I * (↑t - 1) * Complex.exp (-(Complex.I * ↑t))) := by
              apply Complex.abs.isAbsoluteValue.abv_add
            _ ≤ Complex.abs (-1) + Complex.abs (Complex.exp (-(Complex.I * ↑t))) + Complex.abs (Complex.I * (↑t - 1) * Complex.exp (-(Complex.I * ↑t))) := by
              gcongr
              apply Complex.abs.isAbsoluteValue.abv_add
            _ ≤ 1 + 1 + 1 := by
              gcongr
              . simp
              . rw [mul_comm, ←neg_mul]
                norm_cast
                apply le_of_eq
                apply Complex.abs_exp_ofReal_mul_I
              . simp
                apply mul_le_one
                norm_cast
                rw [abs_of_nonpos] <;> linarith
                simp
                rw [mul_comm, ←neg_mul]
                norm_cast
                apply le_of_eq
                apply Complex.abs_exp_ofReal_mul_I
            _ = 3 := by norm_num
        . rw [mul_comm, ←neg_mul, mul_comm]
          norm_cast
          apply lower_secant_bound
          . simp only [neg_mul, Set.mem_Icc, neg_add_le_iff_le_add, le_add_neg_iff_add_le,
            neg_le_sub_iff_le_add]
            constructor <;> linarith [Real.two_le_pi, Real.two_pi_pos]
          . rw [abs_neg, le_abs]
            left
            rcases ht with ht | ht <;> linarith [ht.1]
    _ = (MeasureTheory.volume (Ι y' y)).toReal * (3 / ((y / 2) / 2) ^ 2) := by
      apply MeasureTheory.setIntegral_const
    _ = |y - y'| * (3 / ((y / 2) / 2) ^ 2) := by
      congr
      rw [Real.volume_uIoc, ENNReal.toReal_ofReal (abs_nonneg (y - y'))]
    _ = (3 * (2 * 2) ^ 2) * (1 / y) * (|y - y'| / y) := by
      ring
    _ ≤ 2 ^ 6 * (1 / y) * (|y - y'| / y) := by
      gcongr
      norm_num
Proof state after:
y y' : ℝ
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' ≤ 1
⊢ |(-y')| ≤ 1

y y' : ℝ
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' ≤ 1
⊢ |(-y)| ≤ 1