how to unfold a let expression inside a theorem?

Question

I'm trying to prove a theorem, and to do so I have to prove a lemma about a function I define during the proof. The issue is that I would like to unfold the definition of the function, but I get an error when I try to use the delta or unfold tactics. I've reproduced the issue in this snippet:

example : True := by
  let F : ℕ→ℕ := λ _ => 0
  have F_le_1 : ∀(n:ℕ), F n ≤ 1 := by
    intro n
    delta F

At this point, I get the error unknown constant '_root_.F'.

What am I missing?

(I should add that I don't get the same error if I define the function outside of the theorem, but I would prefer to know what I'm overlooking, rather than just patching up the problem).

Answer 1

You can use show statements instead:

example : 0 ≤ 1 :=
  let F : Nat → Nat := λ _ => 0
  have F_le_1 (n : Nat) : F n ≤ 1 := by
    show (λ _ => 0) n ≤ 1
    exact Nat.zero_le 1
  F_le_1 1

example : let F : Nat → Nat := λ _ => 0; ∀ (n : Nat), F n ≤ 1 := by
  show ∀ (n : Nat), (λ _ => 0) n ≤ 1
  intro _
  exact Nat.zero_le 1

In fact, you can prove these propositions without show statements.

example : 0 ≤ 1 :=
  let F : Nat → Nat := λ _ => 0
  have F_le_1 (n : Nat) : F n ≤ 1 := Nat.zero_le 1
  F_le_1 1

example : let F : Nat → Nat := λ _ => 0; ∀ (n : Nat), F n ≤ 1 := by
  intro _F _n
  exact Nat.zero_le 1

Answer 2

Mathlib has a tactic called unfold_let specifically for unfolding local definitions.

example : True := by
  let F : ℕ→ℕ := λ _ => 0
  have F_le_1 : ∀(n:ℕ), F n ≤ 1 := by
    intro n
    unfold_let F
    /-
    F: ℕ → ℕ := fun x ↦ 0
    n: ℕ
    ⊢ (fun x ↦ 0) n ≤ 1
    -/

In a recent version of Lean 4, now simp and dsimp can take local variables as arguments to specify that they should be unfolded.

example : True := by
  let F : ℕ→ℕ := λ _ => 0
  have F_le_1 : ∀(n:ℕ), F n ≤ 1 := by
    intro n
    dsimp only [F]
    /-
    F: ℕ → ℕ := fun x ↦ 0
    n: ℕ
    ⊢ 0 ≤ 1
    -/

(Note: if you are on a slightly older Lean 4 version, you might be able to get by with just dsimp only [] because it does zeta substitution by default.)