-- Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean
lemma isBounded_range_integral
    {ι : Type*} (μs : ι → Measure X) [∀ i, IsProbabilityMeasure (μs i)] (f : X →ᵇ E) :
    Bornology.IsBounded (Set.range (fun i ↦ ∫ x, f x ∂ (μs i)))

Proof state:
case intro
X : Type u_1
inst✝⁸ : MeasurableSpace X
inst✝⁷ : TopologicalSpace X
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : OpensMeasurableSpace X
inst✝⁴ : SecondCountableTopology E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ E
ι : Type u_3
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
f : X →ᵇ E
v : E
i : ι
hi : (fun i => ∫ (x : X), f x ∂μs i) i = v
⊢ ‖v‖ ≤ ‖f‖

Tactic:
rw [← hi]

Result:
case intro
X : Type u_1
inst✝⁸ : MeasurableSpace X
inst✝⁷ : TopologicalSpace X
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : OpensMeasurableSpace X
inst✝⁴ : SecondCountableTopology E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ E
ι : Type u_3
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
f : X →ᵇ E
v : E
i : ι
hi : (fun i => ∫ (x : X), f x ∂μs i) i = v
⊢ ‖(fun i => ∫ (x : X), f x ∂μs i) i‖ ≤ ‖f‖

Proof state:
case intro
X : Type u_1
inst✝⁸ : MeasurableSpace X
inst✝⁷ : TopologicalSpace X
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : OpensMeasurableSpace X
inst✝⁴ : SecondCountableTopology E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ E
ι : Type u_3
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
f : X →ᵇ E
v : E
i : ι
hi : (fun i => ∫ (x : X), f x ∂μs i) i = v
⊢ ‖(fun i => ∫ (x : X), f x ∂μs i) i‖ ≤ ‖f‖

Tactic:
apply f.norm_integral_le_norm (μs i)

Result:
no goals

Proof state:
X : Type u_1
inst✝⁸ : MeasurableSpace X
inst✝⁷ : TopologicalSpace X
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : OpensMeasurableSpace X
inst✝⁴ : SecondCountableTopology E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ E
ι : Type u_3
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
f : X →ᵇ E
⊢ Bornology.IsBounded (Set.range fun i => ∫ (x : X), f x ∂μs i)

Tactic:
apply isBounded_iff_forall_norm_le.mpr ⟨‖f‖, fun v hv ↦ ?_⟩

Result:
X : Type u_1
inst✝⁸ : MeasurableSpace X
inst✝⁷ : TopologicalSpace X
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : OpensMeasurableSpace X
inst✝⁴ : SecondCountableTopology E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ E
ι : Type u_3
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
f : X →ᵇ E
v : E
hv : v ∈ Set.range fun i => ∫ (x : X), f x ∂μs i
⊢ ‖v‖ ≤ ‖f‖

Proof state:
X : Type u_1
inst✝⁸ : MeasurableSpace X
inst✝⁷ : TopologicalSpace X
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : OpensMeasurableSpace X
inst✝⁴ : SecondCountableTopology E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ E
ι : Type u_3
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
f : X →ᵇ E
v : E
hv : v ∈ Set.range fun i => ∫ (x : X), f x ∂μs i
⊢ ‖v‖ ≤ ‖f‖

Tactic:
obtain ⟨i, hi⟩ := hv

Result:
case intro
X : Type u_1
inst✝⁸ : MeasurableSpace X
inst✝⁷ : TopologicalSpace X
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : OpensMeasurableSpace X
inst✝⁴ : SecondCountableTopology E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ E
ι : Type u_3
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
f : X →ᵇ E
v : E
i : ι
hi : (fun i => ∫ (x : X), f x ∂μs i) i = v
⊢ ‖v‖ ≤ ‖f‖