case pos
E : Type ?u.30194
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.30290
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ K x : ℝ
hK : K = 0
⊢ gronwallBound δ K 0 x = δ * exp (K * x)

case neg
E : Type ?u.30194
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.30290
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ K x : ℝ
hK : ¬K = 0
⊢ gronwallBound δ K 0 x = δ * exp (K * x)
E : Type ?u.30194
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.30290
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ K x : ℝ
⊢ gronwallBound δ K 0 x = δ * exp (K * x)
by_cases hK : K = 0
no goals
case pos
E : Type ?u.30194
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.30290
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ K x : ℝ
hK : K = 0
⊢ gronwallBound δ K 0 x = δ * exp (K * x)
simp only [gronwallBound_K0, hK, MulZeroClass.zero_mul, exp_zero, add_zero, mul_one]
no goals
case neg
E : Type ?u.30194
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.30290
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ K x : ℝ
hK : ¬K = 0
⊢ gronwallBound δ K 0 x = δ * exp (K * x)
simp only [gronwallBound_of_K_ne_0 hK, zero_div, MulZeroClass.zero_mul, add_zero]