Lean 4: `have h : ∀ {F G}, P G → Q := fun hG h ↦ …` binds the implicits

Inside a tactic proof I wrote local helper lemmas with implicit binders, such as have hconst : ∀ (c : ℝ≥0∞) {G : α → ℝ≥0∞}, Measurable G → ⨍ c*G = c*⨍ G := fun c hG ↦ by …. Lean bound hG to the implicit G and not to the measurability hypothesis. The error appears inside the body ('argument hG has type α → ℝ≥0∞ but is expected to have type Measurable ?'), which is confusing. The same thing happened, inconsistently, for other helpers. The robust fix is := by intro c G hG (intro binds implicits explicitly), or fun c {G} hG ↦. A second gotcha in the same proof: gcongr on u y ^ (-r) * v ≤ b ^ (-r) * v dives into the rpow and asks for 0 ≤ -r; use mul_le_mul' h le_rfl instead.