No goals after `apply`

Stream: new members

[Vasily Ilin]

I see no goals after apply. When I remove sorry, I see the original goal. I thought that apply is like library_search -- either finds a theorem to close the proof or gives up. But it's doing something more mysterious here.

import Mathlib.MeasureTheory.Function.SimpleFunc
open MeasureTheory BigOperators
lemma coe_sum [MeasurableSpace Ω] (f : I → (SimpleFunc Ω ℝ)) [Fintype I] : (↑(∑ i, f i) : Ω → ℝ) = ∑ i, (f i : Ω → ℝ) := by
  apply -- No goals
  sorry

[Kyle Miller]

You must be thinking of the apply? tactic. Your current code is inadvertently doing apply sorry, which closes the goal using sorry.

[Vasily Ilin]

Oh I see. I think there should be a theorem to close this but apply? does not find one

[Vasily Ilin]

The closest I found is https://leanprover-community.github.io/mathlib4_docs/Mathlib/MeasureTheory/Function/SimpleFunc.html#MeasureTheory.SimpleFunc.coe_add