A008: ∫₀^{π/4} x log (1 + tan x) dx = (π²/64) log 2 - πG/8 + 21ζ(3)/64

On [0, π/4] we have 1 + tan x = √2 cos (π/4 - x) / cos x, since cos x + sin x = √2 cos (π/4 - x). Hence x log (1 + tan x) = (log 2 / 2) x + x log cos (π/4 - x) - x log cos x. The substitution u = π/4 - x turns the middle term into ∫₀^{π/4} (π/4 - u) log cos u du, so A008 = (π²/64) log 2 + (π/4) ∫₀^{π/4} log cos - 2 ∫₀^{π/4} x log cos x, and A006 and A007 give the two integrals.

theorem LeanPolyLog.Proofs.A008 : ∫ (x : ℝ) in 0..Real.pi / 4, x * Real.log (1 + Real.tan x) = Real.pi ^ 2 / 64 * Real.log 2 - Real.pi * G / 8 + 21 * zeta3 / 64

A008: ∫₀^{π/4} x log (1 + tan x) dx = (π²/64) log 2 - πG/8 + 21ζ(3)/64.