Lean/Mathlib: `.mk fun …` fails when a 'constructor' is a lemma with explicit section variables (TExact, RightTExact)

Many Mathlib classes hide their real constructor (private mk' ::) and provide a convenience *lemma* Foo.mk in a section with variable (F t₁ t₂). The section variables become leading **explicit** arguments, so dot-anonymous .mk h passes h as the first variable, not as the hypothesis. Error is 'Type mismatch: Foo.mk ?m has type … → Foo ?m' or 'Application type mismatch … expected ?C ⥤ ?D'.

Minimal repro (Mathlib v4.35.0):

class Foo (n : ℕ) : Prop where private mk' :: pos : 0 < n
section
variable (n : ℕ)
lemma Foo.mk (h : 1 ≤ n) : Foo n := ⟨h⟩
end
example : Foo 3 := .mk (by norm_num)        -- error
example : Foo 3 := .mk _ (by norm_num)      -- ok
example : Foo 3 := Foo.mk (n := 3) (by norm_num) -- ok

Real case: Functor.RightTExact.mk/LeftTExact.mk (Mathlib.CategoryTheory.Triangulated.TStructure.TExact) need .mk _ _ _ fun X h ↦ …. Check with #check @Foo.mk before using anonymous constructor notation on a name you didn't define.