Theorem: intervalIntegral.integral_conj' (Carleson/Theorem1_1/Control_Approximation_Effect.lean)

State before:
μ : MeasureTheory.Measure ℝ
𝕜 : Type
inst✝ : RCLike 𝕜
f : ℝ → 𝕜
a b : ℝ
⊢ ∫ (x : ℝ) in a..b, (starRingEnd 𝕜) (f x) ∂μ = (starRingEnd 𝕜) (∫ (x : ℝ) in a..b, f x ∂μ)
Tactic:
rw [intervalIntegral_eq_integral_uIoc, integral_conj, intervalIntegral_eq_integral_uIoc,
    RCLike.real_smul_eq_coe_mul, RCLike.real_smul_eq_coe_mul, map_mul]
State after:
μ : MeasureTheory.Measure ℝ
𝕜 : Type
inst✝ : RCLike 𝕜
f : ℝ → 𝕜
a b : ℝ
⊢ ↑(if a ≤ b then 1 else -1) * (starRingEnd 𝕜) (∫ (x : ℝ) in Ι a b, f x ∂μ) =
    (starRingEnd 𝕜) ↑(if a ≤ b then 1 else -1) * (starRingEnd 𝕜) (∫ (x : ℝ) in Ι a b, f x ∂μ)

State before:
μ : MeasureTheory.Measure ℝ
𝕜 : Type
inst✝ : RCLike 𝕜
f : ℝ → 𝕜
a b : ℝ
⊢ ↑(if a ≤ b then 1 else -1) * (starRingEnd 𝕜) (∫ (x : ℝ) in Ι a b, f x ∂μ) =
    (starRingEnd 𝕜) ↑(if a ≤ b then 1 else -1) * (starRingEnd 𝕜) (∫ (x : ℝ) in Ι a b, f x ∂μ)
Tactic:
congr
State after:
case e_a
μ : MeasureTheory.Measure ℝ
𝕜 : Type
inst✝ : RCLike 𝕜
f : ℝ → 𝕜
a b : ℝ
⊢ ↑(if a ≤ b then 1 else -1) = (starRingEnd 𝕜) ↑(if a ≤ b then 1 else -1)

State before:
case e_a
μ : MeasureTheory.Measure ℝ
𝕜 : Type
inst✝ : RCLike 𝕜
f : ℝ → 𝕜
a b : ℝ
⊢ ↑(if a ≤ b then 1 else -1) = (starRingEnd 𝕜) ↑(if a ≤ b then 1 else -1)
Tactic:
simp
State after:
no goals