Help: Can't find a used theorem in ConstantInfo.value

Stream: general

[Yifeng Sun]

When I was analyzing the constant dependency of Mathlib.Algebra.Polynomial.Degree.Definitions, I noticed that theorem "natDegree_zero" did not appear in the constant dependency of theorem "natDegree_monomial". But If I delete the codes for "natDegree_zero", the simp tactic in "natDegree_monomial" will fail.

The mwe is provided:

import Mathlib

variable {R : Type u}

section Semiring

open Polynomial

variable [Semiring R]

theorem test [DecidableEq R] (i : ℕ) (r : R) :
    natDegree (monomial i r) = if r = 0 then 0 else i := by
  split_ifs with hr
  · simp only [hr, monomial_zero_right, natDegree_zero]
  · rw [← C_mul_X_pow_eq_monomial, natDegree_C_mul_X_pow i r hr]

open Lean in
run_cmd do
  let env ← getEnv
  match env.find? ``test with
  | some info =>
    match info.value? with
    | some value =>
      IO.println s! "{value}"
    | none => IO.println "none"
  | none => IO.println "none"

Here test is a modified version of theorem "natDegree_monomial". Now searching in the command output(value), we don't find "natDegree_zero". Anyone knows the reason?

[Yifeng Sun]

Also, here lean version is v4.19.0.