doc: code comments about reflection support (#5235)

I found that the kernel has special support for `e =?= true`, and will
in this case aggressively whnf `e`. This explains the following behavior
(for a `sqrt` function with fuel):

```lean
theorem foo : sqrt 100000000000000000002 == 10000000000 := rfl       -- fast
theorem foo : sqrt 100000000000000000002 =  10000000000 := rfl       -- slow
theorem foo : sqrt 100000000000000000002 =  10000000000 := by decide -- fast
```

The special support in the kernel only applies for closed `e` and `true`
on the RHS. It could be generlized (also open terms, also `false`, other
data type's constructors, different orientation). But maybe I should
wait for evidence that this generaziation really matters, or whether
all applications (proof by reflection) can be made to have this form.

src/Lean/Elab/Tactic/ElabTerm.lean

@@ -405,7 +405,8 @@ private partial def blameDecideReductionFailure (inst : Expr) : MetaM Expr := do
     if r.isAppOf ``isTrue then
       -- Success!
       -- While we have a proof from reduction, we do not embed it in the proof term,
-      -- and instead we let the kernel recompute it during type checking from the following more efficient term.
+      -- and instead we let the kernel recompute it during type checking from the following more
+      -- efficient term. The kernel handles the unification `e =?= true` specially.
       let rflPrf ← mkEqRefl (toExpr true)
       return mkApp3 (Lean.mkConst ``of_decide_eq_true) expectedType s rflPrf
     else

src/kernel/type_checker.cpp

@@ -1072,7 +1072,8 @@ bool type_checker::is_def_eq_core(expr const & t, expr const & s) {
 
     // Very basic support for proofs by reflection. If `t` has no free variables and `s` is `Bool.true`,
     // we fully reduce `t` and check whether result is `s`.
-    // TODO: add metadata to control whether this optimization is used or not.
+    // This code path is taken in particular when using the `decide` tactic, which produces
+    // proof terms of the form `Eq.refl true : decide p = true`.
     if (!has_fvar(t) && is_constant(s, *g_bool_true)) {
         if (is_constant(whnf(t), *g_bool_true)) {
             return true;