-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem setToL1_mono_left' {T T' : Set α → E →L[ℝ] G''} {C C' : ℝ}
    (hT : DominatedFinMeasAdditive μ T C) (hT' : DominatedFinMeasAdditive μ T' C')
    (hTT' : ∀ s, MeasurableSet s → μ s < ∞ → ∀ x, T s x ≤ T' s x) (f : α →₁[μ] E) :
    setToL1 hT f ≤ setToL1 hT' f

Proof state:
case h_ind
α : Type u_1
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
G'' : Type u_8
inst✝² : NormedLatticeAddCommGroup G''
inst✝¹ : NormedSpace ℝ G''
inst✝ : CompleteSpace G''
T T' : Set α → E →L[ℝ] G''
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
hTT' : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : E), (T s) x ≤ (T' s) x
c : E
s : Set α
hs : MeasurableSet s
hμs : μ s < ⊤
⊢ (setToL1 hT) ↑(indicatorConst 1 hs ⋯ c) ≤ (setToL1 hT') ↑(indicatorConst 1 hs ⋯ c)

Tactic:
rw [setToL1_simpleFunc_indicatorConst hT hs hμs, setToL1_simpleFunc_indicatorConst hT' hs hμs]

Result:
case h_ind
α : Type u_1
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
G'' : Type u_8
inst✝² : NormedLatticeAddCommGroup G''
inst✝¹ : NormedSpace ℝ G''
inst✝ : CompleteSpace G''
T T' : Set α → E →L[ℝ] G''
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
hTT' : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : E), (T s) x ≤ (T' s) x
c : E
s : Set α
hs : MeasurableSet s
hμs : μ s < ⊤
⊢ (T s) c ≤ (T' s) c

Proof state:
case h_ind
α : Type u_1
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
G'' : Type u_8
inst✝² : NormedLatticeAddCommGroup G''
inst✝¹ : NormedSpace ℝ G''
inst✝ : CompleteSpace G''
T T' : Set α → E →L[ℝ] G''
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
hTT' : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : E), (T s) x ≤ (T' s) x
c : E
s : Set α
hs : MeasurableSet s
hμs : μ s < ⊤
⊢ (T s) c ≤ (T' s) c

Tactic:
exact hTT' s hs hμs c

Result:
no goals

Proof state:
case h_closed
α : Type u_1
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
G'' : Type u_8
inst✝² : NormedLatticeAddCommGroup G''
inst✝¹ : NormedSpace ℝ G''
inst✝ : CompleteSpace G''
T T' : Set α → E →L[ℝ] G''
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
hTT' : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : E), (T s) x ≤ (T' s) x
⊢ IsClosed {f | (setToL1 hT) f ≤ (setToL1 hT') f}

Tactic:
exact isClosed_le (setToL1 hT).continuous (setToL1 hT').continuous

Result:
no goals

Proof state:
case h_add
α : Type u_1
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
G'' : Type u_8
inst✝² : NormedLatticeAddCommGroup G''
inst✝¹ : NormedSpace ℝ G''
inst✝ : CompleteSpace G''
T T' : Set α → E →L[ℝ] G''
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
hTT' : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : E), (T s) x ≤ (T' s) x
f g : α → E
hf : MemLp f 1 μ
hg : MemLp g 1 μ
a✝ : Disjoint (Function.support f) (Function.support g)
hf_le : (setToL1 hT) (MemLp.toLp f hf) ≤ (setToL1 hT') (MemLp.toLp f hf)
hg_le : (setToL1 hT) (MemLp.toLp g hg) ≤ (setToL1 hT') (MemLp.toLp g hg)
⊢ (setToL1 hT) (MemLp.toLp f hf) + (setToL1 hT) (MemLp.toLp g hg) ≤
    (setToL1 hT') (MemLp.toLp f hf) + (setToL1 hT') (MemLp.toLp g hg)

Tactic:
exact add_le_add hf_le hg_le

Result:
no goals

Proof state:
case h_add
α : Type u_1
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
G'' : Type u_8
inst✝² : NormedLatticeAddCommGroup G''
inst✝¹ : NormedSpace ℝ G''
inst✝ : CompleteSpace G''
T T' : Set α → E →L[ℝ] G''
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
hTT' : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : E), (T s) x ≤ (T' s) x
f g : α → E
hf : MemLp f 1 μ
hg : MemLp g 1 μ
a✝ : Disjoint (Function.support f) (Function.support g)
hf_le : (setToL1 hT) (MemLp.toLp f hf) ≤ (setToL1 hT') (MemLp.toLp f hf)
hg_le : (setToL1 hT) (MemLp.toLp g hg) ≤ (setToL1 hT') (MemLp.toLp g hg)
⊢ (setToL1 hT) (MemLp.toLp f hf + MemLp.toLp g hg) ≤ (setToL1 hT') (MemLp.toLp f hf + MemLp.toLp g hg)

Tactic:
rw [(setToL1 hT).map_add, (setToL1 hT').map_add]

Result:
case h_add
α : Type u_1
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
G'' : Type u_8
inst✝² : NormedLatticeAddCommGroup G''
inst✝¹ : NormedSpace ℝ G''
inst✝ : CompleteSpace G''
T T' : Set α → E →L[ℝ] G''
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
hTT' : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : E), (T s) x ≤ (T' s) x
f g : α → E
hf : MemLp f 1 μ
hg : MemLp g 1 μ
a✝ : Disjoint (Function.support f) (Function.support g)
hf_le : (setToL1 hT) (MemLp.toLp f hf) ≤ (setToL1 hT') (MemLp.toLp f hf)
hg_le : (setToL1 hT) (MemLp.toLp g hg) ≤ (setToL1 hT') (MemLp.toLp g hg)
⊢ (setToL1 hT) (MemLp.toLp f hf) + (setToL1 hT) (MemLp.toLp g hg) ≤
    (setToL1 hT') (MemLp.toLp f hf) + (setToL1 hT') (MemLp.toLp g hg)

Proof state:
α : Type u_1
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
G'' : Type u_8
inst✝² : NormedLatticeAddCommGroup G''
inst✝¹ : NormedSpace ℝ G''
inst✝ : CompleteSpace G''
T T' : Set α → E →L[ℝ] G''
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
hTT' : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : E), (T s) x ≤ (T' s) x
f : ↥(Lp E 1 μ)
⊢ (setToL1 hT) f ≤ (setToL1 hT') f

Tactic:
induction f using Lp.induction (hp_ne_top := one_ne_top) with
| @h_ind c s hs hμs =>
  rw [setToL1_simpleFunc_indicatorConst hT hs hμs, setToL1_simpleFunc_indicatorConst hT' hs hμs]
  exact hTT' s hs hμs c
| @h_add f g hf hg _ hf_le hg_le =>
  rw [(setToL1 hT).map_add, (setToL1 hT').map_add]
  exact add_le_add hf_le hg_le
| h_closed => exact isClosed_le (setToL1 hT).continuous (setToL1 hT').continuous

Result:
no goals