English
The standard logarithm log coincides with logC: log = logC.
Русский
Стандартный логарифм совпадает с logC: log = logC.
LaTeX
$$$ \\log = \\logC $$$
Lean4
/-- The result of `Nat.log` agrees with the result of `Nat.logC`. The latter will be computed more
efficiently, but the former is easier to prove things about and has more lemmas.
This lemma is tagged @[csimp] so that the code generated for `Nat.log` uses `Nat.logC` instead.
-/
@[csimp]
theorem log_eq_logC : log = logC := by
ext b m
rcases le_or_gt b 1 with hb | hb
case inl => rw [logC_of_left_le_one hb, Nat.log_of_left_le_one hb]
case inr =>
rcases eq_or_ne m 0 with rfl | hm
case inl => rw [Nat.log_zero_right, logC_zero]
case inr =>
rw [Nat.log_eq_iff (Or.inr ⟨hb, hm⟩)]
exact logC_spec hb (zero_lt_of_ne_zero hm)
