have h : c ∉ Icc a b := fun h ↦ by linarith [mem_Icc.mp h]
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
fSupp : Function.support f ⊆ Icc a b
c : ℝ
hc : b < c
⊢ f c = 0
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
fSupp : Function.support f ⊆ Icc a b
c : ℝ
hc : b < c
h : c ∉ Icc a b
⊢ f c = 0