-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem indicatorConstLp_eq_toSpanSingleton_compLp {s : Set α} [NormedSpace ℝ F]
    (hs : MeasurableSet s) (hμs : μ s ≠ ∞) (x : F) :
    indicatorConstLp 2 hs hμs x =
      (ContinuousLinearMap.toSpanSingleton ℝ x).compLp (indicatorConstLp 2 hs hμs (1 : ℝ))

Proof state:
case h
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup F
s : Set α
inst✝ : NormedSpace ℝ F
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : F
⊢ (s.indicator fun x_1 => x) =ᶠ[ae μ] ↑↑((ContinuousLinearMap.toSpanSingleton ℝ x).compLp (indicatorConstLp 2 hs hμs 1))

Tactic:
have h_compLp :=
  (ContinuousLinearMap.toSpanSingleton ℝ x).coeFn_compLp (indicatorConstLp 2 hs hμs (1 : ℝ))

Result:
case h
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup F
s : Set α
inst✝ : NormedSpace ℝ F
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : F
h_compLp :
  ∀ᵐ (a : α) ∂μ,
    ↑↑((ContinuousLinearMap.toSpanSingleton ℝ x).compLp (indicatorConstLp 2 hs hμs 1)) a =
      (ContinuousLinearMap.toSpanSingleton ℝ x) (↑↑(indicatorConstLp 2 hs hμs 1) a)
⊢ (s.indicator fun x_1 => x) =ᶠ[ae μ] ↑↑((ContinuousLinearMap.toSpanSingleton ℝ x).compLp (indicatorConstLp 2 hs hμs 1))

Proof state:
case h
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup F
s : Set α
inst✝ : NormedSpace ℝ F
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : F
h_compLp :
  ↑↑((ContinuousLinearMap.toSpanSingleton ℝ x).compLp (indicatorConstLp 2 hs hμs 1)) =ᶠ[ae μ] fun a =>
    (ContinuousLinearMap.toSpanSingleton ℝ x) (↑↑(indicatorConstLp 2 hs hμs 1) a)
⊢ (s.indicator fun x_1 => x) =ᶠ[ae μ] ↑↑((ContinuousLinearMap.toSpanSingleton ℝ x).compLp (indicatorConstLp 2 hs hμs 1))

Tactic:
refine EventuallyEq.trans ?_ h_compLp.symm

Result:
case h
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup F
s : Set α
inst✝ : NormedSpace ℝ F
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : F
h_compLp :
  ↑↑((ContinuousLinearMap.toSpanSingleton ℝ x).compLp (indicatorConstLp 2 hs hμs 1)) =ᶠ[ae μ] fun a =>
    (ContinuousLinearMap.toSpanSingleton ℝ x) (↑↑(indicatorConstLp 2 hs hμs 1) a)
⊢ (s.indicator fun x_1 => x) =ᶠ[ae μ] fun a =>
    (ContinuousLinearMap.toSpanSingleton ℝ x) (↑↑(indicatorConstLp 2 hs hμs 1) a)

Proof state:
case h
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup F
s : Set α
inst✝ : NormedSpace ℝ F
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : F
h_compLp :
  ↑↑((ContinuousLinearMap.toSpanSingleton ℝ x).compLp (indicatorConstLp 2 hs hμs 1)) =ᶠ[ae μ] fun a =>
    (ContinuousLinearMap.toSpanSingleton ℝ x) (↑↑(indicatorConstLp 2 hs hμs 1) a)
⊢ (s.indicator fun x_1 => x) =ᶠ[ae μ] fun a =>
    (ContinuousLinearMap.toSpanSingleton ℝ x) (↑↑(indicatorConstLp 2 hs hμs 1) a)

Tactic:
refine (@indicatorConstLp_coeFn _ _ _ 2 μ _ s hs hμs (1 : ℝ)).mono fun y hy => ?_

Result:
case h
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup F
s : Set α
inst✝ : NormedSpace ℝ F
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : F
h_compLp :
  ↑↑((ContinuousLinearMap.toSpanSingleton ℝ x).compLp (indicatorConstLp 2 hs hμs 1)) =ᶠ[ae μ] fun a =>
    (ContinuousLinearMap.toSpanSingleton ℝ x) (↑↑(indicatorConstLp 2 hs hμs 1) a)
y : α
hy : ↑↑(indicatorConstLp 2 hs hμs 1) y = s.indicator (fun x => 1) y
⊢ s.indicator (fun x_1 => x) y =
    (fun a => (ContinuousLinearMap.toSpanSingleton ℝ x) (↑↑(indicatorConstLp 2 hs hμs 1) a)) y

Proof state:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup F
s : Set α
inst✝ : NormedSpace ℝ F
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : F
⊢ indicatorConstLp 2 hs hμs x = (ContinuousLinearMap.toSpanSingleton ℝ x).compLp (indicatorConstLp 2 hs hμs 1)

Tactic:
ext1

Result:
case h
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup F
s : Set α
inst✝ : NormedSpace ℝ F
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : F
⊢ ↑↑(indicatorConstLp 2 hs hμs x) =ᶠ[ae μ]
    ↑↑((ContinuousLinearMap.toSpanSingleton ℝ x).compLp (indicatorConstLp 2 hs hμs 1))

Proof state:
case h
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup F
s : Set α
inst✝ : NormedSpace ℝ F
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : F
h_compLp :
  ↑↑((ContinuousLinearMap.toSpanSingleton ℝ x).compLp (indicatorConstLp 2 hs hμs 1)) =ᶠ[ae μ] fun a =>
    (ContinuousLinearMap.toSpanSingleton ℝ x) (↑↑(indicatorConstLp 2 hs hμs 1) a)
y : α
hy : ↑↑(indicatorConstLp 2 hs hμs 1) y = s.indicator (fun x => 1) y
⊢ s.indicator (fun x_1 => x) y = s.indicator (fun x => 1) y • x

Tactic:
by_cases hy_mem : y ∈ s <;> simp [hy_mem]

Result:
no goals

Proof state:
case h
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup F
s : Set α
inst✝ : NormedSpace ℝ F
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : F
⊢ ↑↑(indicatorConstLp 2 hs hμs x) =ᶠ[ae μ]
    ↑↑((ContinuousLinearMap.toSpanSingleton ℝ x).compLp (indicatorConstLp 2 hs hμs 1))

Tactic:
refine indicatorConstLp_coeFn.trans ?_

Result:
case h
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup F
s : Set α
inst✝ : NormedSpace ℝ F
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : F
⊢ (s.indicator fun x_1 => x) =ᶠ[ae μ] ↑↑((ContinuousLinearMap.toSpanSingleton ℝ x).compLp (indicatorConstLp 2 hs hμs 1))

Proof state:
case h
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup F
s : Set α
inst✝ : NormedSpace ℝ F
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : F
h_compLp :
  ↑↑((ContinuousLinearMap.toSpanSingleton ℝ x).compLp (indicatorConstLp 2 hs hμs 1)) =ᶠ[ae μ] fun a =>
    (ContinuousLinearMap.toSpanSingleton ℝ x) (↑↑(indicatorConstLp 2 hs hμs 1) a)
y : α
hy : ↑↑(indicatorConstLp 2 hs hμs 1) y = s.indicator (fun x => 1) y
⊢ s.indicator (fun x_1 => x) y =
    (fun a => (ContinuousLinearMap.toSpanSingleton ℝ x) (↑↑(indicatorConstLp 2 hs hμs 1) a)) y

Tactic:
dsimp only

Result:
case h
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup F
s : Set α
inst✝ : NormedSpace ℝ F
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : F
h_compLp :
  ↑↑((ContinuousLinearMap.toSpanSingleton ℝ x).compLp (indicatorConstLp 2 hs hμs 1)) =ᶠ[ae μ] fun a =>
    (ContinuousLinearMap.toSpanSingleton ℝ x) (↑↑(indicatorConstLp 2 hs hμs 1) a)
y : α
hy : ↑↑(indicatorConstLp 2 hs hμs 1) y = s.indicator (fun x => 1) y
⊢ s.indicator (fun x_1 => x) y = (ContinuousLinearMap.toSpanSingleton ℝ x) (↑↑(indicatorConstLp 2 hs hμs 1) y)

Proof state:
case h
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup F
s : Set α
inst✝ : NormedSpace ℝ F
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : F
h_compLp :
  ↑↑((ContinuousLinearMap.toSpanSingleton ℝ x).compLp (indicatorConstLp 2 hs hμs 1)) =ᶠ[ae μ] fun a =>
    (ContinuousLinearMap.toSpanSingleton ℝ x) (↑↑(indicatorConstLp 2 hs hμs 1) a)
y : α
hy : ↑↑(indicatorConstLp 2 hs hμs 1) y = s.indicator (fun x => 1) y
⊢ s.indicator (fun x_1 => x) y = (ContinuousLinearMap.toSpanSingleton ℝ x) (s.indicator (fun x => 1) y)

Tactic:
simp_rw [ContinuousLinearMap.toSpanSingleton_apply]

Result:
case h
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup F
s : Set α
inst✝ : NormedSpace ℝ F
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : F
h_compLp :
  ↑↑((ContinuousLinearMap.toSpanSingleton ℝ x).compLp (indicatorConstLp 2 hs hμs 1)) =ᶠ[ae μ] fun a =>
    (ContinuousLinearMap.toSpanSingleton ℝ x) (↑↑(indicatorConstLp 2 hs hμs 1) a)
y : α
hy : ↑↑(indicatorConstLp 2 hs hμs 1) y = s.indicator (fun x => 1) y
⊢ s.indicator (fun x_1 => x) y = s.indicator (fun x => 1) y • x