case pos
E : Type ?u.1814
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.1910
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ K ε x : ℝ
hK : K = 0
⊢ HasDerivAt (gronwallBound δ K ε) (K * gronwallBound δ K ε x + ε) x

case neg
E : Type ?u.1814
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.1910
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ K ε x : ℝ
hK : ¬K = 0
⊢ HasDerivAt (gronwallBound δ K ε) (K * gronwallBound δ K ε x + ε) x
E : Type ?u.1814
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.1910
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ K ε x : ℝ
⊢ HasDerivAt (gronwallBound δ K ε) (K * gronwallBound δ K ε x + ε) x
by_cases hK : K = 0
case pos
E : Type ?u.1814
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.1910
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ ε x : ℝ
⊢ HasDerivAt (gronwallBound δ 0 ε) (0 * gronwallBound δ 0 ε x + ε) x
case pos
E : Type ?u.1814
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.1910
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ K ε x : ℝ
hK : K = 0
⊢ HasDerivAt (gronwallBound δ K ε) (K * gronwallBound δ K ε x + ε) x
subst K
case pos
E : Type ?u.1814
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.1910
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ ε x : ℝ
⊢ HasDerivAt (fun x => δ + ε * x) ε x
case pos
E : Type ?u.1814
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.1910
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ ε x : ℝ
⊢ HasDerivAt (gronwallBound δ 0 ε) (0 * gronwallBound δ 0 ε x + ε) x
simp only [gronwallBound_K0, MulZeroClass.zero_mul, zero_add]
case h.e'_7
E : Type ?u.1814
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.1910
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ ε x : ℝ
⊢ ε = ε * 1
case pos
E : Type ?u.1814
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.1910
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ ε x : ℝ
⊢ HasDerivAt (fun x => δ + ε * x) ε x
convert ((hasDerivAt_id x).const_mul ε).const_add δ
no goals
case h.e'_7
E : Type ?u.1814
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.1910
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ ε x : ℝ
⊢ ε = ε * 1
rw [mul_one]
case neg
E : Type ?u.1814
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.1910
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ K ε x : ℝ
hK : ¬K = 0
⊢ HasDerivAt (fun x => δ * exp (K * x) + ε / K * (exp (K * x) - 1))
    (K * (δ * exp (K * x) + ε / K * (exp (K * x) - 1)) + ε) x
case neg
E : Type ?u.1814
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.1910
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ K ε x : ℝ
hK : ¬K = 0
⊢ HasDerivAt (gronwallBound δ K ε) (K * gronwallBound δ K ε x + ε) x
simp only [gronwallBound_of_K_ne_0 hK]
case h.e'_7
E : Type ?u.1814
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.1910
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ K ε x : ℝ
hK : ¬K = 0
⊢ K * (δ * exp (K * x) + ε / K * (exp (K * x) - 1)) + ε =
    δ * (exp (K * id x) * (K * 1)) + ε / K * (exp (K * id x) * (K * 1))
case neg
E : Type ?u.1814
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.1910
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ K ε x : ℝ
hK : ¬K = 0
⊢ HasDerivAt (fun x => δ * exp (K * x) + ε / K * (exp (K * x) - 1))
    (K * (δ * exp (K * x) + ε / K * (exp (K * x) - 1)) + ε) x
convert (((hasDerivAt_id x).const_mul K).exp.const_mul δ).add
  ((((hasDerivAt_id x).const_mul K).exp.sub_const 1).const_mul (ε / K)) using 1
case h.e'_7
E : Type ?u.1814
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.1910
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ K ε x : ℝ
hK : ¬K = 0
⊢ K * δ * exp (K * x) + ε * (exp (K * x) - 1) + ε = K * δ * exp (K * x) * 1 + ε * exp (K * x) * 1
case h.e'_7
E : Type ?u.1814
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.1910
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ K ε x : ℝ
hK : ¬K = 0
⊢ K * (δ * exp (K * x) + ε / K * (exp (K * x) - 1)) + ε =
    δ * (exp (K * id x) * (K * 1)) + ε / K * (exp (K * id x) * (K * 1))
simp only [id, mul_add, (mul_assoc _ _ _).symm, mul_comm _ K, mul_div_cancel' _ hK]
no goals
case h.e'_7
E : Type ?u.1814
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.1910
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ K ε x : ℝ
hK : ¬K = 0
⊢ K * δ * exp (K * x) + ε * (exp (K * x) - 1) + ε = K * δ * exp (K * x) * 1 + ε * exp (K * x) * 1
ring