-- Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL2.lean
theorem integrable_condExpIndSMul (hm : m ≤ m0) [SigmaFinite (μ.trim hm)] (hs : MeasurableSet s)
    (hμs : μ s ≠ ∞) (x : G) : Integrable (condExpIndSMul hm hs hμs x) μ

Proof state:
case refine_2
α : Type u_1
G : Type u_5
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 ≠ ⊤
x : G
t : Set α
ht : MeasurableSet t
hμt : μ t ≠ ⊤
⊢ μ (s ∩ t) * ↑‖x‖₊ ≤ μ s * ↑‖x‖₊

Tactic:
gcongr

Result:
case refine_2.bc.h
α : Type u_1
G : Type u_5
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 ≠ ⊤
x : G
t : Set α
ht : MeasurableSet t
hμt : μ t ≠ ⊤
⊢ s ∩ t ⊆ s

Proof state:
case refine_2
α : Type u_1
G : Type u_5
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 ≠ ⊤
x : G
⊢ ∀ (s_1 : Set α),
    MeasurableSet s_1 → μ s_1 ≠ ⊤ → ∫⁻ (x_1 : α) in s_1, ‖↑↑(condExpIndSMul hm hs hμs x) x_1‖ₑ ∂μ ≤ μ s * ↑‖x‖₊

Tactic:
refine fun t ht hμt => (setLIntegral_nnnorm_condExpIndSMul_le hm hs hμs x ht hμt).trans ?_

Result:
case refine_2
α : Type u_1
G : Type u_5
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 ≠ ⊤
x : G
t : Set α
ht : MeasurableSet t
hμt : μ t ≠ ⊤
⊢ μ (s ∩ t) * ↑‖x‖₊ ≤ μ s * ↑‖x‖₊

Proof state:
α : Type u_1
G : Type u_5
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 ≠ ⊤
x : G
⊢ Integrable (↑↑(condExpIndSMul hm hs hμs x)) μ

Tactic:
refine integrable_of_forall_fin_meas_le' hm (μ s * ‖x‖₊)
  (ENNReal.mul_lt_top hμs.lt_top ENNReal.coe_lt_top) ?_ ?_

Result:
case refine_1
α : Type u_1
G : Type u_5
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 ≠ ⊤
x : G
⊢ AEStronglyMeasurable (↑↑(condExpIndSMul hm hs hμs x)) μ

case refine_2
α : Type u_1
G : Type u_5
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 ≠ ⊤
x : G
⊢ ∀ (s_1 : Set α),
    MeasurableSet s_1 → μ s_1 ≠ ⊤ → ∫⁻ (x_1 : α) in s_1, ‖↑↑(condExpIndSMul hm hs hμs x) x_1‖ₑ ∂μ ≤ μ s * ↑‖x‖₊

Proof state:
case refine_1
α : Type u_1
G : Type u_5
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 ≠ ⊤
x : G
⊢ AEStronglyMeasurable (↑↑(condExpIndSMul hm hs hμs x)) μ

Tactic:
exact Lp.aestronglyMeasurable _

Result:
no goals

Proof state:
case refine_2.bc.h
α : Type u_1
G : Type u_5
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 ≠ ⊤
x : G
t : Set α
ht : MeasurableSet t
hμt : μ t ≠ ⊤
⊢ s ∩ t ⊆ s

Tactic:
apply Set.inter_subset_left

Result:
no goals