Construct witness of a product in a subtype proof

Stream: lean4

[Malcolm Langfield]

Consider the following two examples. In the first, we construct a witness by providing a proof of True, and so Lean "learns" that C = fun _ _ => True. I want to do something similar in the second case.

lemma infant : { C : Nat → Nat → Prop // ∀ {m n : Nat}, C m n } := by
  constructor
  intros _ _
  refine' True.intro

lemma baby : { C : (Nat → Nat → Prop) × Nat // ∀ {m n : Nat}, (Prod.fst C) m n } := by
  constructor
  intros m n
  refine' True.intro
  sorry

Instead, I get this error:

▶ 2 goals
case property
s₀ s₁ : State
fuel m n : ℕ
⊢ ?val.1 m n

case val
s₀ s₁ : State
fuel : ℕ
⊢ (ℕ → ℕ → Prop) × ℕ

▶ expected type (482:11-482:21)
s₀ s₁ : State
fuel m n : ℕ
⊢ ?val.1 m n

▶ 482:3-482:21: error:
type mismatch
  True.intro
has type
  True : Prop
but is expected to have type
  ?val.1 m n : Prop

The motivation for this is during a long subtype proof that begins with constructor, I would like to reference intermediate values constructed in the proof within the witness for C, but I don't want to prove that they can be expressed in terms of only constants and the arguments to C, and so instead I would like to assert the existence of these intermediate values and construct them, but I do not know how to do this.