-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem of_measure_le {μ' : Measure α} (h : μ ≤ μ') (hT : DominatedFinMeasAdditive μ T C)
    (hC : 0 ≤ C) : DominatedFinMeasAdditive μ' T C

Proof state:
case h.hb
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : SeminormedAddCommGroup β
T : Set α → β
C : ℝ
μ' : Measure α
h : μ ≤ μ'
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
h' : ∀ (s : Set α), μ s = ⊤ → μ' s = ⊤
s : Set α
hs : MeasurableSet s
hμ's : μ' s < ⊤
hμs : μ s < ⊤
⊢ μ' s ≠ ⊤

case h.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : SeminormedAddCommGroup β
T : Set α → β
C : ℝ
μ' : Measure α
h : μ ≤ μ'
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
h' : ∀ (s : Set α), μ s = ⊤ → μ' s = ⊤
s : Set α
hs : MeasurableSet s
hμ's : μ' s < ⊤
hμs : μ s < ⊤
⊢ μ s ≤ μ' s

Tactic:
exacts [hμ's.ne, h _]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : SeminormedAddCommGroup β
T : Set α → β
C : ℝ
μ' : Measure α
h : μ ≤ μ'
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
h' : ∀ (s : Set α), μ s = ⊤ → μ' s = ⊤
⊢ DominatedFinMeasAdditive μ' T C

Tactic:
refine ⟨hT.1.of_eq_top_imp_eq_top fun s _ ↦ h' s, fun s hs hμ's ↦ ?_⟩

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : SeminormedAddCommGroup β
T : Set α → β
C : ℝ
μ' : Measure α
h : μ ≤ μ'
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
h' : ∀ (s : Set α), μ s = ⊤ → μ' s = ⊤
s : Set α
hs : MeasurableSet s
hμ's : μ' s < ⊤
⊢ ‖T s‖ ≤ C * (μ' s).toReal

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : SeminormedAddCommGroup β
T : Set α → β
C : ℝ
μ' : Measure α
h : μ ≤ μ'
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
h' : ∀ (s : Set α), μ s = ⊤ → μ' s = ⊤
s : Set α
hs : MeasurableSet s
hμ's : μ' s < ⊤
⊢ ‖T s‖ ≤ C * (μ' s).toReal

Tactic:
have hμs : μ s < ∞ := (h s).trans_lt hμ's

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : SeminormedAddCommGroup β
T : Set α → β
C : ℝ
μ' : Measure α
h : μ ≤ μ'
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
h' : ∀ (s : Set α), μ s = ⊤ → μ' s = ⊤
s : Set α
hs : MeasurableSet s
hμ's : μ' s < ⊤
hμs : μ s < ⊤
⊢ ‖T s‖ ≤ C * (μ' s).toReal

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : SeminormedAddCommGroup β
T : Set α → β
C : ℝ
μ' : Measure α
h : μ ≤ μ'
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
⊢ DominatedFinMeasAdditive μ' T C

Tactic:
have h' : ∀ s, μ s = ∞ → μ' s = ∞ := fun s hs ↦ top_unique <| hs.symm.trans_le (h _)

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : SeminormedAddCommGroup β
T : Set α → β
C : ℝ
μ' : Measure α
h : μ ≤ μ'
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
h' : ∀ (s : Set α), μ s = ⊤ → μ' s = ⊤
⊢ DominatedFinMeasAdditive μ' T C

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : SeminormedAddCommGroup β
T : Set α → β
C : ℝ
μ' : Measure α
h : μ ≤ μ'
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
h' : ∀ (s : Set α), μ s = ⊤ → μ' s = ⊤
s : Set α
hs : MeasurableSet s
hμ's : μ' s < ⊤
hμs : μ s < ⊤
⊢ C * (μ s).toReal ≤ C * (μ' s).toReal

Tactic:
gcongr

Result:
case h.hb
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : SeminormedAddCommGroup β
T : Set α → β
C : ℝ
μ' : Measure α
h : μ ≤ μ'
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
h' : ∀ (s : Set α), μ s = ⊤ → μ' s = ⊤
s : Set α
hs : MeasurableSet s
hμ's : μ' s < ⊤
hμs : μ s < ⊤
⊢ μ' s ≠ ⊤

case h.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : SeminormedAddCommGroup β
T : Set α → β
C : ℝ
μ' : Measure α
h : μ ≤ μ'
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
h' : ∀ (s : Set α), μ s = ⊤ → μ' s = ⊤
s : Set α
hs : MeasurableSet s
hμ's : μ' s < ⊤
hμs : μ s < ⊤
⊢ μ s ≤ μ' s

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : SeminormedAddCommGroup β
T : Set α → β
C : ℝ
μ' : Measure α
h : μ ≤ μ'
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
h' : ∀ (s : Set α), μ s = ⊤ → μ' s = ⊤
s : Set α
hs : MeasurableSet s
hμ's : μ' s < ⊤
hμs : μ s < ⊤
⊢ ‖T s‖ ≤ C * (μ' s).toReal

Tactic:
calc
  ‖T s‖ ≤ C * (μ s).toReal := hT.2 s hs hμs
  _ ≤ C * (μ' s).toReal := by gcongr; exacts [hμ's.ne, h _]

Result:
no goals