-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem integral_comp_comm (L : E ≃L[𝕜] F) (φ : X → E) : ∫ x, L (φ x) ∂μ = L (∫ x, φ x ∂μ)

Proof state:
X : Type u_1
E : Type u_3
F : Type u_4
inst✝⁷ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ E
L : E ≃L[𝕜] F
φ : X → E
⊢ ∫ (x : X), L (φ x) ∂μ = L (∫ (x : X), φ x ∂μ)

Tactic:
have : CompleteSpace E ↔ CompleteSpace F :=
  completeSpace_congr (e := L.toEquiv) L.isUniformEmbedding

Result:
X : Type u_1
E : Type u_3
F : Type u_4
inst✝⁷ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ E
L : E ≃L[𝕜] F
φ : X → E
this : CompleteSpace E ↔ CompleteSpace F
⊢ ∫ (x : X), L (φ x) ∂μ = L (∫ (x : X), φ x ∂μ)

Proof state:
case inl.intro
X : Type u_1
E : Type u_3
F : Type u_4
inst✝⁷ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ E
L : E ≃L[𝕜] F
φ : X → E
this : CompleteSpace E ↔ CompleteSpace F
left✝ : CompleteSpace E
right✝ : CompleteSpace F
⊢ ∫ (x : X), L (φ x) ∂μ = L (∫ (x : X), φ x ∂μ)

Tactic:
exact L.toContinuousLinearMap.integral_comp_comm' L.antilipschitz _

Result:
no goals

Proof state:
case inr.intro
X : Type u_1
E : Type u_3
F : Type u_4
inst✝⁷ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ E
L : E ≃L[𝕜] F
φ : X → E
this : CompleteSpace E ↔ CompleteSpace F
left✝ : ¬CompleteSpace E
right✝ : ¬CompleteSpace F
⊢ ∫ (x : X), L (φ x) ∂μ = L (∫ (x : X), φ x ∂μ)

Tactic:
simp [integral, *]

Result:
no goals

Proof state:
X : Type u_1
E : Type u_3
F : Type u_4
inst✝⁷ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ E
L : E ≃L[𝕜] F
φ : X → E
this : CompleteSpace E ↔ CompleteSpace F
⊢ ∫ (x : X), L (φ x) ∂μ = L (∫ (x : X), φ x ∂μ)

Tactic:
obtain ⟨_, _⟩|⟨_, _⟩ := iff_iff_and_or_not_and_not.mp this

Result:
case inl.intro
X : Type u_1
E : Type u_3
F : Type u_4
inst✝⁷ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ E
L : E ≃L[𝕜] F
φ : X → E
this : CompleteSpace E ↔ CompleteSpace F
left✝ : CompleteSpace E
right✝ : CompleteSpace F
⊢ ∫ (x : X), L (φ x) ∂μ = L (∫ (x : X), φ x ∂μ)

case inr.intro
X : Type u_1
E : Type u_3
F : Type u_4
inst✝⁷ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ E
L : E ≃L[𝕜] F
φ : X → E
this : CompleteSpace E ↔ CompleteSpace F
left✝ : ¬CompleteSpace E
right✝ : ¬CompleteSpace F
⊢ ∫ (x : X), L (φ x) ∂μ = L (∫ (x : X), φ x ∂μ)