-- Mathlib/MeasureTheory/Function/L2Space.lean
theorem inner_indicatorConstLp_eq_setIntegral_inner (f : Lp E 2 μ) (hs : MeasurableSet s) (c : E)
    (hμs : μ s ≠ ∞) : (⟪indicatorConstLp 2 hs hμs c, f⟫ : 𝕜) = ∫ x in s, ⟪c, f x⟫ ∂μ

Proof state:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
s : Set α
f : ↥(Lp E 2 μ)
hs : MeasurableSet s
c : E
hμs : μ s ≠ ⊤
h_left : ∫ (x : α) in s, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ = ∫ (x : α) in s, inner c (↑↑f x) ∂μ
h_indicator : ∀ᵐ (x : α) ∂μ, x ∉ s → ↑↑(indicatorConstLp 2 hs hμs c) x = 0
x : α
hx : x ∉ s → ↑↑(indicatorConstLp 2 hs hμs c) x = 0
hxs : x ∉ s
⊢ inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) = 0

Tactic:
rw [hx hxs]

Result:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
s : Set α
f : ↥(Lp E 2 μ)
hs : MeasurableSet s
c : E
hμs : μ s ≠ ⊤
h_left : ∫ (x : α) in s, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ = ∫ (x : α) in s, inner c (↑↑f x) ∂μ
h_indicator : ∀ᵐ (x : α) ∂μ, x ∉ s → ↑↑(indicatorConstLp 2 hs hμs c) x = 0
x : α
hx : x ∉ s → ↑↑(indicatorConstLp 2 hs hμs c) x = 0
hxs : x ∉ s
⊢ inner 0 (↑↑f x) = 0

Proof state:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
s : Set α
f : ↥(Lp E 2 μ)
hs : MeasurableSet s
c : E
hμs : μ s ≠ ⊤
h_left : ∫ (x : α) in s, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ = ∫ (x : α) in s, inner c (↑↑f x) ∂μ
h_ae_eq : ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) = 0
⊢ ∫ (x : α) in sᶜ, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ = 0

Tactic:
suffices h_int_zero :
    (∫ x in sᶜ, inner (indicatorConstLp 2 hs hμs c x) (f x) ∂μ) = ∫ _ in sᶜ, (0 : 𝕜) ∂μ by
  rw [h_int_zero]
  simp

Result:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
s : Set α
f : ↥(Lp E 2 μ)
hs : MeasurableSet s
c : E
hμs : μ s ≠ ⊤
h_left : ∫ (x : α) in s, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ = ∫ (x : α) in s, inner c (↑↑f x) ∂μ
h_ae_eq : ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) = 0
⊢ ∫ (x : α) in sᶜ, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ = ∫ (x : α) in sᶜ, 0 ∂μ

Proof state:
case e_a
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
s : Set α
f : ↥(Lp E 2 μ)
hs : MeasurableSet s
c : E
hμs : μ s ≠ ⊤
h_indicator : ∀ᵐ (x : α) ∂μ, x ∈ s → ↑↑(indicatorConstLp 2 hs hμs c) x = c
x : α
hx : x ∈ s → ↑↑(indicatorConstLp 2 hs hμs c) x = c
hxs : x ∈ s
⊢ ↑↑(indicatorConstLp 2 hs hμs c) x = c

Tactic:
exact hx hxs

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
s : Set α
f : ↥(Lp E 2 μ)
hs : MeasurableSet s
c : E
hμs : μ s ≠ ⊤
h_left : ∫ (x : α) in s, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ = ∫ (x : α) in s, inner c (↑↑f x) ∂μ
⊢ ∀ᵐ (x : α) ∂μ, x ∉ s → inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) = 0

Tactic:
have h_indicator : ∀ᵐ x : α ∂μ, x ∉ s → indicatorConstLp 2 hs hμs c x = 0 :=
  indicatorConstLp_coeFn_nmem

Result:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
s : Set α
f : ↥(Lp E 2 μ)
hs : MeasurableSet s
c : E
hμs : μ s ≠ ⊤
h_left : ∫ (x : α) in s, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ = ∫ (x : α) in s, inner c (↑↑f x) ∂μ
h_indicator : ∀ᵐ (x : α) ∂μ, x ∉ s → ↑↑(indicatorConstLp 2 hs hμs c) x = 0
⊢ ∀ᵐ (x : α) ∂μ, x ∉ s → inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) = 0