case h.e'_7
E : Type ?u.20531
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.20627
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ K ε x a : ℝ
⊢ K * gronwallBound δ K ε (x - a) + ε = (K * gronwallBound δ K ε (id x - a) + ε) * 1
E : Type ?u.20531
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.20627
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ K ε x a : ℝ
⊢ HasDerivAt (fun y => gronwallBound δ K ε (y - a)) (K * gronwallBound δ K ε (x - a) + ε) x
convert (hasDerivAt_gronwallBound δ K ε _).comp x ((hasDerivAt_id x).sub_const a) using 1
no goals
case h.e'_7
E : Type ?u.20531
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.20627
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ K ε x a : ℝ
⊢ K * gronwallBound δ K ε (x - a) + ε = (K * gronwallBound δ K ε (id x - a) + ε) * 1
rw [id, mul_one]