-- Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean
theorem condExpInd_of_measurable (hs : MeasurableSet[m] s) (hμs : μ s ≠ ∞) (c : G) :
    condExpInd G hm μ s c = indicatorConstLp 1 (hm s hs) hμs c

Proof state:
case h
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : G
⊢ (fun a => ↑↑(indicatorConstLp 2 ⋯ hμs 1) a • c) =ᶠ[ae μ] s.indicator fun x => c

Tactic:
refine (@indicatorConstLp_coeFn α _ _ 2 μ _ s (hm s hs) hμs (1 : ℝ)).mono fun x hx => ?_

Result:
case h
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : G
x : α
hx : ↑↑(indicatorConstLp 2 ⋯ hμs 1) x = s.indicator (fun x => 1) x
⊢ (fun a => ↑↑(indicatorConstLp 2 ⋯ hμs 1) a • c) x = s.indicator (fun x => c) x

Proof state:
case h
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : G
⊢ ↑↑((condExpInd G hm μ s) c) =ᶠ[ae μ] ↑↑(indicatorConstLp 1 ⋯ hμs c)

Tactic:
refine EventuallyEq.trans ?_ indicatorConstLp_coeFn.symm

Result:
case h
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : G
⊢ ↑↑((condExpInd G hm μ s) c) =ᶠ[ae μ] s.indicator fun x => c

Proof state:
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : G
⊢ (condExpInd G hm μ s) c = indicatorConstLp 1 ⋯ hμs c

Tactic:
ext1

Result:
case h
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : G
⊢ ↑↑((condExpInd G hm μ s) c) =ᶠ[ae μ] ↑↑(indicatorConstLp 1 ⋯ hμs c)

Proof state:
case h
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : G
x : α
hx : ↑↑(indicatorConstLp 2 ⋯ hμs 1) x = s.indicator (fun x => 1) x
⊢ (fun a => ↑↑(indicatorConstLp 2 ⋯ hμs 1) a • c) x = s.indicator (fun x => c) x

Tactic:
dsimp only

Result:
case h
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : G
x : α
hx : ↑↑(indicatorConstLp 2 ⋯ hμs 1) x = s.indicator (fun x => 1) x
⊢ ↑↑(indicatorConstLp 2 ⋯ hμs 1) x • c = s.indicator (fun x => c) x

Proof state:
case h
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : G
x : α
hx : ↑↑(indicatorConstLp 2 ⋯ hμs 1) x = s.indicator (fun x => 1) x
⊢ s.indicator (fun x => 1) x • c = s.indicator (fun x => c) x

Tactic:
by_cases hx_mem : x ∈ s <;> simp [hx_mem]

Result:
no goals

Proof state:
case h
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : G
⊢ (fun a => ↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 ⋯ hμs 1)) a • c) =ᶠ[ae μ] s.indicator fun x => c

Tactic:
rw [condExpL2_indicator_of_measurable hm hs hμs (1 : ℝ)]

Result:
case h
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : G
⊢ (fun a => ↑↑(indicatorConstLp 2 ⋯ hμs 1) a • c) =ᶠ[ae μ] s.indicator fun x => c

Proof state:
case h
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : G
⊢ ↑↑((condExpInd G hm μ s) c) =ᶠ[ae μ] s.indicator fun x => c

Tactic:
refine (condExpInd_ae_eq_condExpIndSMul hm (hm s hs) hμs c).trans ?_

Result:
case h
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : G
⊢ ↑↑(condExpIndSMul hm ⋯ hμs c) =ᶠ[ae μ] s.indicator fun x => c

Proof state:
case h
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : G
⊢ ↑↑(condExpIndSMul hm ⋯ hμs c) =ᶠ[ae μ] s.indicator fun x => c

Tactic:
refine (condExpIndSMul_ae_eq_smul hm (hm s hs) hμs c).trans ?_

Result:
case h
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : G
⊢ (fun a => ↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 ⋯ hμs 1)) a • c) =ᶠ[ae μ] s.indicator fun x => c

Proof state:
case h
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : G
x : α
hx : ↑↑(indicatorConstLp 2 ⋯ hμs 1) x = s.indicator (fun x => 1) x
⊢ ↑↑(indicatorConstLp 2 ⋯ hμs 1) x • c = s.indicator (fun x => c) x

Tactic:
rw [hx]

Result:
case h
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : G
x : α
hx : ↑↑(indicatorConstLp 2 ⋯ hμs 1) x = s.indicator (fun x => 1) x
⊢ s.indicator (fun x => 1) x • c = s.indicator (fun x => c) x