c y : ℝ
x✝ : y ∈ Iic 0
⊢ (∫ (x : ℝ) in id y..c, ‖exp x‖) ≤ exp c
c : ℝ
⊢ IntegrableOn exp (Iic c)
refine'
  integrableOn_Iic_of_intervalIntegral_norm_bounded (exp c) c
    (fun y => intervalIntegrable_exp.1) tendsto_id
    (eventually_of_mem (Iic_mem_atBot 0) fun y _ => _)
c y : ℝ
x✝ : y ∈ Iic 0
⊢ 0 ≤ exp (id y)
c y : ℝ
x✝ : y ∈ Iic 0
⊢ (∫ (x : ℝ) in id y..c, ‖exp x‖) ≤ exp c
simp_rw [norm_of_nonneg (exp_pos _).le, integral_exp, sub_le_self_iff]
no goals
c y : ℝ
x✝ : y ∈ Iic 0
⊢ 0 ≤ exp (id y)
exact (exp_pos _).le