Theorem: Hilbert_kernel_regularity_main_part
Proof state before:
case h
y y' : ℝ
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' ≤ 1
f : ℝ → ℂ := fun t => (1 - ↑t) / (1 - (-(Complex.I * ↑t)).exp)
f' : ℝ → ℂ :=
  fun t =>
    (-1 + (-(Complex.I * ↑t)).exp + Complex.I * (↑t - 1) * (-(Complex.I * ↑t)).exp) / (1 - (-(Complex.I * ↑t)).exp) ^ 2
f'def :
  f' = fun t =>
    (-1 + (-(Complex.I * ↑t)).exp + Complex.I * (↑t - 1) * (-(Complex.I * ↑t)).exp) / (1 - (-(Complex.I * ↑t)).exp) ^ 2
c : ℝ → ℂ := fun t => 1 - ↑t
cdef : c = fun t => 1 - ↑t
c' : ℝ → ℂ := fun t => -1
c'def : c' = fun t => -1
d : ℝ → ℂ := fun t => 1 - (-(Complex.I * ↑t)).exp
ddef : d = fun t => 1 - (-(Complex.I * ↑t)).exp
d' : ℝ → ℂ := fun t => Complex.I * (-(Complex.I * ↑t)).exp
d'def : d' = fun t => Complex.I * (-(Complex.I * ↑t)).exp
d_nonzero : ∀ {t : ℝ}, t ∈ Set.uIcc y' y → d t ≠ 0
f_deriv : ∀ t ∈ Set.uIcc y' y, HasDerivAt f (f' t) t
f'_cont : ContinuousOn (fun t => f' t) (Set.uIcc y' y)
t : ℝ
ht : y' < t ∧ t ≤ y ∨ y < t ∧ t ≤ y'
ht' : 0 < t ∧ t ≤ 1
⊢ Complex.abs (-1 + (-(Complex.I * ↑t)).exp + Complex.I * (↑t - 1) * (-(Complex.I * ↑t)).exp) /
      Complex.abs (1 - (-(Complex.I * ↑t)).exp) ^ 2 ≤
    3 / (y / 2 / 2) ^ 2
Tactic:
gcongr
Proof state after:
case h.hac
y y' : ℝ
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' ≤ 1
f : ℝ → ℂ := fun t => (1 - ↑t) / (1 - (-(Complex.I * ↑t)).exp)
f' : ℝ → ℂ :=
  fun t =>
    (-1 + (-(Complex.I * ↑t)).exp + Complex.I * (↑t - 1) * (-(Complex.I * ↑t)).exp) / (1 - (-(Complex.I * ↑t)).exp) ^ 2
f'def :
  f' = fun t =>
    (-1 + (-(Complex.I * ↑t)).exp + Complex.I * (↑t - 1) * (-(Complex.I * ↑t)).exp) / (1 - (-(Complex.I * ↑t)).exp) ^ 2
c : ℝ → ℂ := fun t => 1 - ↑t
cdef : c = fun t => 1 - ↑t
c' : ℝ → ℂ := fun t => -1
c'def : c' = fun t => -1
d : ℝ → ℂ := fun t => 1 - (-(Complex.I * ↑t)).exp
ddef : d = fun t => 1 - (-(Complex.I * ↑t)).exp
d' : ℝ → ℂ := fun t => Complex.I * (-(Complex.I * ↑t)).exp
d'def : d' = fun t => Complex.I * (-(Complex.I * ↑t)).exp
d_nonzero : ∀ {t : ℝ}, t ∈ Set.uIcc y' y → d t ≠ 0
f_deriv : ∀ t ∈ Set.uIcc y' y, HasDerivAt f (f' t) t
f'_cont : ContinuousOn (fun t => f' t) (Set.uIcc y' y)
t : ℝ
ht : y' < t ∧ t ≤ y ∨ y < t ∧ t ≤ y'
ht' : 0 < t ∧ t ≤ 1
⊢ Complex.abs (-1 + (-(Complex.I * ↑t)).exp + Complex.I * (↑t - 1) * (-(Complex.I * ↑t)).exp) ≤ 3

case h.hbd.hab
y y' : ℝ
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' ≤ 1
f : ℝ → ℂ := fun t => (1 - ↑t) / (1 - (-(Complex.I * ↑t)).exp)
f' : ℝ → ℂ :=
  fun t =>
    (-1 + (-(Complex.I * ↑t)).exp + Complex.I * (↑t - 1) * (-(Complex.I * ↑t)).exp) / (1 - (-(Complex.I * ↑t)).exp) ^ 2
f'def :
  f' = fun t =>
    (-1 + (-(Complex.I * ↑t)).exp + Complex.I * (↑t - 1) * (-(Complex.I * ↑t)).exp) / (1 - (-(Complex.I * ↑t)).exp) ^ 2
c : ℝ → ℂ := fun t => 1 - ↑t
cdef : c = fun t => 1 - ↑t
c' : ℝ → ℂ := fun t => -1
c'def : c' = fun t => -1
d : ℝ → ℂ := fun t => 1 - (-(Complex.I * ↑t)).exp
ddef : d = fun t => 1 - (-(Complex.I * ↑t)).exp
d' : ℝ → ℂ := fun t => Complex.I * (-(Complex.I * ↑t)).exp
d'def : d' = fun t => Complex.I * (-(Complex.I * ↑t)).exp
d_nonzero : ∀ {t : ℝ}, t ∈ Set.uIcc y' y → d t ≠ 0
f_deriv : ∀ t ∈ Set.uIcc y' y, HasDerivAt f (f' t) t
f'_cont : ContinuousOn (fun t => f' t) (Set.uIcc y' y)
t : ℝ
ht : y' < t ∧ t ≤ y ∨ y < t ∧ t ≤ y'
ht' : 0 < t ∧ t ≤ 1
⊢ y / 2 / 2 ≤ Complex.abs (1 - (-(Complex.I * ↑t)).exp)