-- 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_right : ∫ (x : α) in 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ᶜ, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ =
    ∫ (x : α) in s, inner c (↑↑f x) ∂μ

Tactic:
rw [h_left, h_right, add_zero]

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 : α) in sᶜ, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ = 0

Tactic:
suffices h_ae_eq : ∀ᵐ x ∂μ, x ∉ s → ⟪indicatorConstLp 2 hs hμs c x, f x⟫ = 0 by
  simp_rw [← Set.mem_compl_iff] at h_ae_eq
  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
  exact setIntegral_congr_ae hs.compl h_ae_eq

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) ∂μ
⊢ ∀ᵐ (x : α) ∂μ, x ∉ s → inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑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 ≠ ⊤
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) = inner c (↑↑f x)

Tactic:
have h_indicator : ∀ᵐ x : α ∂μ, x ∈ s → indicatorConstLp 2 hs hμs c x = c :=
  indicatorConstLp_coeFn_mem

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_indicator : ∀ᵐ (x : α) ∂μ, x ∈ s → ↑↑(indicatorConstLp 2 hs hμs c) x = c
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) = inner 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 0 (↑↑f x) = 0

Tactic:
exact inner_zero_left _

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) ∂μ
h_ae_eq : ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) = 0
h_int_zero : ∫ (x : α) in sᶜ, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ = ∫ (x : α) in sᶜ, 0 ∂μ
⊢ ∫ (x : α) in sᶜ, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ = 0

Tactic:
rw [h_int_zero]

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
h_int_zero : ∫ (x : α) in sᶜ, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ = ∫ (x : α) in sᶜ, 0 ∂μ
⊢ ∫ (x : α) in sᶜ, 0 ∂μ = 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 ≠ ⊤
⊢ inner (indicatorConstLp 2 hs hμs c) f = ∫ (x : α) in s, inner c (↑↑f x) ∂μ

Tactic:
rw [inner_def, ← integral_add_compl hs (L2.integrable_inner _ f)]

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 ≠ ⊤
⊢ ∫ (x : α) in s, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ +
      ∫ (x : α) in sᶜ, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ =
    ∫ (x : α) in s, inner 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) ∂μ
⊢ ∫ (x : α) in s, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ +
      ∫ (x : α) in sᶜ, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ =
    ∫ (x : α) in s, inner c (↑↑f x) ∂μ

Tactic:
have h_right : (∫ x in sᶜ, ⟪(indicatorConstLp 2 hs hμs c) x, f x⟫ ∂μ) = 0 := by
  suffices h_ae_eq : ∀ᵐ x ∂μ, x ∉ s → ⟪indicatorConstLp 2 hs hμs c x, f x⟫ = 0 by
    simp_rw [← Set.mem_compl_iff] at h_ae_eq
    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
    exact setIntegral_congr_ae hs.compl h_ae_eq
  have h_indicator : ∀ᵐ x : α ∂μ, x ∉ s → indicatorConstLp 2 hs hμs c x = 0 :=
    indicatorConstLp_coeFn_nmem
  refine h_indicator.mono fun x hx hxs => ?_
  rw [hx hxs]
  exact inner_zero_left _

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_right : ∫ (x : α) in 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ᶜ, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ =
    ∫ (x : α) in s, inner c (↑↑f x) ∂μ