A010: ∫₀^{π/4} x² tan² x dx = -G + π²/16 - π³/192 + (π/4) log 2

On [0, π/4] the function H x = x² tan x + 2x log cos x - x³/3 has derivative x² tan² x + 2 log cos x, because 1/cos² x - 1 = tan² x. Hence ∫₀^{π/4} x² tan² x dx = H(π/4) - H(0) - 2 ∫₀^{π/4} log cos x dx, and A006 gives the last integral.

theorem LeanPolyLog.Proofs.A010 : ∫ (x : ℝ) in 0..Real.pi / 4, x ^ 2 * Real.tan x ^ 2 = -G + Real.pi ^ 2 / 16 - Real.pi ^ 3 / 192 + Real.pi / 4 * Real.log 2

A010: ∫₀^{π/4} x² tan² x dx = -G + π²/16 - π³/192 + (π/4) log 2.