Theorem: test_unknown_identifier (Ray/Tactic/BoundTests.lean)

State before:
f : ℕ → ℝ
le : ∀ (n : ℕ), f n ≤ ↑n
⊢ ∀ (n : ℕ), f n ≤ ↑n
Tactic:
intro n
State after:
f : ℕ → ℝ
le : ∀ (n : ℕ), f n ≤ ↑n
n : ℕ
⊢ f n ≤ ↑n

State before:
f : ℕ → ℝ
le : ∀ (n : ℕ), f n ≤ ↑n
n : ℕ
⊢ f n ≤ ↑n
Tactic:
bound [le n]
State after:
no goals