case pos
E : Type ?u.29211
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.29307
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ K ε : ℝ
hK : K = 0
⊢ gronwallBound δ K ε 0 = δ

case neg
E : Type ?u.29211
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.29307
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ K ε : ℝ
hK : ¬K = 0
⊢ gronwallBound δ K ε 0 = δ
E : Type ?u.29211
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.29307
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ K ε : ℝ
⊢ gronwallBound δ K ε 0 = δ
by_cases hK : K = 0
no goals
case pos
E : Type ?u.29211
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.29307
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ K ε : ℝ
hK : K = 0
⊢ gronwallBound δ K ε 0 = δ
simp only [gronwallBound, if_pos hK, MulZeroClass.mul_zero, add_zero]
no goals
case neg
E : Type ?u.29211
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.29307
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ K ε : ℝ
hK : ¬K = 0
⊢ gronwallBound δ K ε 0 = δ
simp only [gronwallBound, if_neg hK, MulZeroClass.mul_zero, exp_zero, sub_self, mul_one,
  add_zero]