@affeldt-aist @t6s @IshiguroYoshihiro
As I mentioned here, I am formalizing a substitution (change-of-variable) formula for Lebesgue integral. Here is the blueprint.
Theorem
Let $a, b \in \mathbb{R}$ with $a \leq b$. Let $f : [a, b] \to \mathbb{R}$ be of class $C^1$, and let $g : \mathbb{R} \to \mathbb{R}$ be a bounded Borel measurable function. Then
$$(g \circ f) \cdot f' : [a, b] \to \mathbb{R}; \quad t \mapsto g(f(t)) \cdot f'(t)$$
is Lebesgue integrable, and the following identity holds:
$$\int_{f(a)}^{f(b)} g(x) \, dx = \int_a^b g(f(t)) f'(t) \, dt.$$
Here both sides are oriented Lebesgue integrals (i.e. sign is taken into account).
Proof
Since $g$ is bounded, $g \circ f$ is also bounded. Moreover, since $f$ is $C^1$ on $[a, b]$, $f'$ is continuous on $[a, b]$, hence in particular bounded and Borel measurable. Therefore $(g \circ f) \cdot f'$ is Lebesgue integrable on $[a, b]$.
Define functions $F, G : [a, b] \to \mathbb{R}$ by
$$F(s) := \int_a^s g(f(t)) f'(t) \, dt,$$
$$G(s) := \int_{f(a)}^{f(s)} g(x) \, dx.$$
By the Fundamental Theorem of Calculus lemma FTC1,
$$F'(t) = g(f(t)) f'(t) \quad \text{for a.e.\ } t \in [a, b].$$
Furthermore, viewing $G$ as the composition of $s \mapsto f(s)$ and $r \mapsto \int_{f(a)}^{r} g$, an application of lemma FTC1 (with the chain rule for the derivative of the composite functions) gives
$$G'(s) = g(f(s)) f'(s) \quad \text{for a.e.\ } s \in [a, b].$$
Hence $F'(s) = G'(s)$ for a.e. $s \in [a, b]$. Moreover,
$$F(a) = G(a) = 0.$$
By lemma ae_eq_integral we have
$$F = G \quad \text{on\ } [a, b].$$
In particular, evaluating at $s = b$ gives $F(b) = G(b)$, i.e.,
$$\int_a^b g(f(t))\, f'(t)\, dt \;=\; \int_{f(a)}^{f(b)} g(x)\, dx.$$
Observation
I think the bottleneck is to introduce the oriented Lebesgue integral, which we have yet to formalize.
Disclaimer
The idea of the proof is inspired by Claude and ChatGPT, but I wrote down the proof and checked its accuracy by myself. Therefore, I am responsible for any trouble coming from this formalization.
