Theorem: mean_squeeze (Ray/Misc/Measure.lean)

State before:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
lo : b ≤ ⨍ (x : X) in s, f x
hi : ∀ x ∈ s, f x ≤ b
⊢ ∀ x ∈ s, f x = b
Tactic:
contrapose lo
State after:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
lo : ¬∀ x ∈ s, f x = b
⊢ ¬b ≤ ⨍ (x : X) in s, f x

State before:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
lo : ¬∀ x ∈ s, f x = b
⊢ ¬b ≤ ⨍ (x : X) in s, f x
Tactic:
rw [average_eq]
State after:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
lo : ¬∀ x ∈ s, f x = b
⊢ ¬b ≤ (↑(volume.restrict s) Set.univ).toReal⁻¹ • ∫ (x : X) in s, f x

State before:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
lo : ¬∀ x ∈ s, f x = b
⊢ ¬b ≤ (↑(volume.restrict s) Set.univ).toReal⁻¹ • ∫ (x : X) in s, f x
Tactic:
simp only [Algebra.id.smul_eq_mul, not_le]
State after:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
lo : ¬∀ x ∈ s, f x = b
⊢ (↑(volume.restrict s) Set.univ).toReal⁻¹ * ∫ (x : X) in s, f x < b

State before:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
lo : ¬∀ x ∈ s, f x = b
⊢ (↑(volume.restrict s) Set.univ).toReal⁻¹ * ∫ (x : X) in s, f x < b
Tactic:
simp only [not_forall] at lo
State after:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
lo : ∃ x, ∃ (_ : x ∈ s), ¬f x = b
⊢ (↑(volume.restrict s) Set.univ).toReal⁻¹ * ∫ (x : X) in s, f x < b

State before:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
lo : ∃ x, ∃ (_ : x ∈ s), ¬f x = b
⊢ (↑(volume.restrict s) Set.univ).toReal⁻¹ * ∫ (x : X) in s, f x < b
Tactic:
rcases lo with ⟨x, xs, fx'⟩
State after:
case intro.intro
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx' : ¬f x = b
⊢ (↑(volume.restrict s) Set.univ).toReal⁻¹ * ∫ (x : X) in s, f x < b

State before:
case intro.intro
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx' : ¬f x = b
⊢ (↑(volume.restrict s) Set.univ).toReal⁻¹ * ∫ (x : X) in s, f x < b
Tactic:
have fx := lt_of_le_of_ne (hi x xs) fx'
State after:
case intro.intro
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx' : ¬f x = b
fx : f x < b
⊢ (↑(volume.restrict s) Set.univ).toReal⁻¹ * ∫ (x : X) in s, f x < b

State before:
case intro.intro
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx' : ¬f x = b
fx : f x < b
⊢ (↑(volume.restrict s) Set.univ).toReal⁻¹ * ∫ (x : X) in s, f x < b
Tactic:
clear fx'
State after:
case intro.intro
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
⊢ (↑(volume.restrict s) Set.univ).toReal⁻¹ * ∫ (x : X) in s, f x < b

State before:
case intro.intro
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
⊢ (↑(volume.restrict s) Set.univ).toReal⁻¹ * ∫ (x : X) in s, f x < b
Tactic:
rcases Metric.continuousOn_iff.mp fc x xs ((b - f x) / 2) (by linarith) with ⟨e, ep, he⟩
State after:
case intro.intro.intro.intro
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
⊢ (↑(volume.restrict s) Set.univ).toReal⁻¹ * ∫ (x : X) in s, f x < b

State before:
case intro.intro.intro.intro
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
⊢ (↑(volume.restrict s) Set.univ).toReal⁻¹ * ∫ (x : X) in s, f x < b
Tactic:
have vtp' := lv x e xs ep
State after:
case intro.intro.intro.intro
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
vtp' : 0 < ↑volume (s ∩ ball x e)
⊢ (↑(volume.restrict s) Set.univ).toReal⁻¹ * ∫ (x : X) in s, f x < b

State before:
case intro.intro.intro.intro
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
vtp' : 0 < ↑volume (s ∩ ball x e)
⊢ (↑(volume.restrict s) Set.univ).toReal⁻¹ * ∫ (x : X) in s, f x < b
Tactic:
generalize ht : s ∩ ball x e = t
State after:
case intro.intro.intro.intro
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
vtp' : 0 < ↑volume (s ∩ ball x e)
t : Set X
ht : s ∩ ball x e = t
⊢ (↑(volume.restrict s) Set.univ).toReal⁻¹ * ∫ (x : X) in s, f x < b

State before:
case intro.intro.intro.intro
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
vtp' : 0 < ↑volume (s ∩ ball x e)
t : Set X
ht : s ∩ ball x e = t
⊢ (↑(volume.restrict s) Set.univ).toReal⁻¹ * ∫ (x : X) in s, f x < b
Tactic:
rw [ht] at vtp'
State after:
case intro.intro.intro.intro
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
⊢ (↑(volume.restrict s) Set.univ).toReal⁻¹ * ∫ (x : X) in s, f x < b

State before:
case intro.intro.intro.intro
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
⊢ (↑(volume.restrict s) Set.univ).toReal⁻¹ * ∫ (x : X) in s, f x < b
Tactic:
have ts : t ⊆ s := by rw [← ht]; exact Set.inter_subset_left _ _
State after:
case intro.intro.intro.intro
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
⊢ (↑(volume.restrict s) Set.univ).toReal⁻¹ * ∫ (x : X) in s, f x < b

State before:
case intro.intro.intro.intro
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
⊢ (↑(volume.restrict s) Set.univ).toReal⁻¹ * ∫ (x : X) in s, f x < b
Tactic:
have tf : volume t < ⊤ := lt_of_le_of_lt (measure_mono ts) sn.finite
State after:
case intro.intro.intro.intro
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
⊢ (↑(volume.restrict s) Set.univ).toReal⁻¹ * ∫ (x : X) in s, f x < b

State before:
case intro.intro.intro.intro
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
⊢ (↑(volume.restrict s) Set.univ).toReal⁻¹ * ∫ (x : X) in s, f x < b
Tactic:
have tm : MeasurableSet t := by
  rw [← ht]; exact MeasurableSet.inter sn.measurable measurableSet_ball
State after:
case intro.intro.intro.intro
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
⊢ (↑(volume.restrict s) Set.univ).toReal⁻¹ * ∫ (x : X) in s, f x < b

State before:
case intro.intro.intro.intro
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
⊢ (↑(volume.restrict s) Set.univ).toReal⁻¹ * ∫ (x : X) in s, f x < b
Tactic:
have sc : s \ t ∪ t = s := Set.diff_union_of_subset ts
State after:
case intro.intro.intro.intro
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
⊢ (↑(volume.restrict s) Set.univ).toReal⁻¹ * ∫ (x : X) in s, f x < b

State before:
case intro.intro.intro.intro
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
⊢ (↑(volume.restrict s) Set.univ).toReal⁻¹ * ∫ (x : X) in s, f x < b
Tactic:
nth_rw 2 [← sc]
State after:
case intro.intro.intro.intro
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
⊢ (↑(volume.restrict s) Set.univ).toReal⁻¹ * ∫ (x : X) in s \ t ∪ t, f x < b

State before:
case intro.intro.intro.intro
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
⊢ (↑(volume.restrict s) Set.univ).toReal⁻¹ * ∫ (x : X) in s \ t ∪ t, f x < b
Tactic:
rw [integral_union]
State after:
case intro.intro.intro.intro
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
⊢ (↑(volume.restrict s) Set.univ).toReal⁻¹ * ((∫ (x : X) in s \ t, f x) + ∫ (x : X) in t, f x) < b

case intro.intro.intro.intro.hst
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
⊢ Disjoint (s \ t) t

case intro.intro.intro.intro.ht
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
⊢ MeasurableSet t

case intro.intro.intro.intro.hfs
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
⊢ IntegrableOn (fun x => f x) (s \ t) volume

case intro.intro.intro.intro.hft
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
⊢ IntegrableOn (fun x => f x) t volume

State before:
case intro.intro.intro.intro
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
⊢ (↑(volume.restrict s) Set.univ).toReal⁻¹ * ((∫ (x : X) in s \ t, f x) + ∫ (x : X) in t, f x) < b

case intro.intro.intro.intro.hst
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
⊢ Disjoint (s \ t) t

case intro.intro.intro.intro.ht
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
⊢ MeasurableSet t

case intro.intro.intro.intro.hfs
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
⊢ IntegrableOn (fun x => f x) (s \ t) volume

case intro.intro.intro.intro.hft
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
⊢ IntegrableOn (fun x => f x) t volume
Tactic:
simp only [MeasurableSet.univ, Measure.restrict_apply, Set.univ_inter, gt_iff_lt]
State after:
case intro.intro.intro.intro
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
⊢ (↑volume s).toReal⁻¹ * ((∫ (x : X) in s \ t, f x) + ∫ (x : X) in t, f x) < b

case intro.intro.intro.intro.hst
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
⊢ Disjoint (s \ t) t

case intro.intro.intro.intro.ht
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
⊢ MeasurableSet t

case intro.intro.intro.intro.hfs
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
⊢ IntegrableOn (fun x => f x) (s \ t) volume

case intro.intro.intro.intro.hft
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
⊢ IntegrableOn (fun x => f x) t volume

State before:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
⊢ (b - f x) / 2 > 0
Tactic:
linarith
State after:
no goals

State before:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
⊢ t ⊆ s
Tactic:
rw [← ht]
State after:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
⊢ s ∩ ball x e ⊆ s

State before:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
⊢ s ∩ ball x e ⊆ s
Tactic:
exact Set.inter_subset_left _ _
State after:
no goals

State before:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
⊢ MeasurableSet t
Tactic:
rw [← ht]
State after:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
⊢ MeasurableSet (s ∩ ball x e)

State before:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
⊢ MeasurableSet (s ∩ ball x e)
Tactic:
exact MeasurableSet.inter sn.measurable measurableSet_ball
State after:
no goals

State before:
case intro.intro.intro.intro
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
⊢ (↑volume s).toReal⁻¹ * ((∫ (x : X) in s \ t, f x) + ∫ (x : X) in t, f x) < b
Tactic:
set m := (b + f x) / 2
State after:
case intro.intro.intro.intro
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
⊢ (↑volume s).toReal⁻¹ * ((∫ (x : X) in s \ t, f x) + ∫ (x : X) in t, f x) < b

State before:
case intro.intro.intro.intro
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
⊢ (↑volume s).toReal⁻¹ * ((∫ (x : X) in s \ t, f x) + ∫ (x : X) in t, f x) < b
Tactic:
set vs := (volume s).toReal
State after:
case intro.intro.intro.intro
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
⊢ vs⁻¹ * ((∫ (x : X) in s \ t, f x) + ∫ (x : X) in t, f x) < b

State before:
case intro.intro.intro.intro
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
⊢ vs⁻¹ * ((∫ (x : X) in s \ t, f x) + ∫ (x : X) in t, f x) < b
Tactic:
set vt := (volume t).toReal
State after:
case intro.intro.intro.intro
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
⊢ vs⁻¹ * ((∫ (x : X) in s \ t, f x) + ∫ (x : X) in t, f x) < b

State before:
case intro.intro.intro.intro
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
⊢ vs⁻¹ * ((∫ (x : X) in s \ t, f x) + ∫ (x : X) in t, f x) < b
Tactic:
have vsp : vs > 0 := sn.real_pos
State after:
case intro.intro.intro.intro
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
⊢ vs⁻¹ * ((∫ (x : X) in s \ t, f x) + ∫ (x : X) in t, f x) < b

State before:
case intro.intro.intro.intro
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
⊢ vs⁻¹ * ((∫ (x : X) in s \ t, f x) + ∫ (x : X) in t, f x) < b
Tactic:
have vtp : vt > 0 := ENNReal.toReal_pos (vtp'.ne') (lt_top_iff_ne_top.mp tf)
State after:
case intro.intro.intro.intro
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
⊢ vs⁻¹ * ((∫ (x : X) in s \ t, f x) + ∫ (x : X) in t, f x) < b

State before:
case intro.intro.intro.intro
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
⊢ vs⁻¹ * ((∫ (x : X) in s \ t, f x) + ∫ (x : X) in t, f x) < b
Tactic:
rw [inv_mul_lt_iff' vsp]
State after:
case intro.intro.intro.intro
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
⊢ (∫ (x : X) in s \ t, f x) + ∫ (x : X) in t, f x < b * vs

State before:
case intro.intro.intro.intro
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
⊢ (∫ (x : X) in s \ t, f x) + ∫ (x : X) in t, f x < b * vs
Tactic:
have mb : m < b := by
  calc (b + f x) / 2
    _ < (b + b) / 2 := (div_lt_div_right (by norm_num)).mpr (by bound)
    _ = b := by ring
State after:
case intro.intro.intro.intro
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
mb : m < b
⊢ (∫ (x : X) in s \ t, f x) + ∫ (x : X) in t, f x < b * vs

State before:
case intro.intro.intro.intro
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
mb : m < b
⊢ (∫ (x : X) in s \ t, f x) + ∫ (x : X) in t, f x < b * vs
Tactic:
have i0 : ∫ x in s \ t, f x ≤ (vs - vt) * b := by
  have df : volume (s \ t) < ⊤ := lt_of_le_of_lt (measure_mono (Set.diff_subset _ _)) sn.finite
  have dm : MeasurableSet (s \ t) := MeasurableSet.diff sn.measurable tm
  have fb := @setIntegral_mono_on _ _ volume f (fun _ ↦ b) (s \ t)
    (fi.mono (Set.diff_subset _ _) (le_refl _)) (integrableOn_const.mpr (Or.inr df)) dm ?_
  simp [measure_diff ts tm (lt_top_iff_ne_top.mp tf),
    ENNReal.toReal_sub_of_le (measure_mono ts) (lt_top_iff_ne_top.mp sn.finite)] at fb
  exact fb
  intro y yd; simp at yd; exact hi y yd.left
State after:
case intro.intro.intro.intro
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
mb : m < b
i0 : ∫ (x : X) in s \ t, f x ≤ (vs - vt) * b
⊢ (∫ (x : X) in s \ t, f x) + ∫ (x : X) in t, f x < b * vs

State before:
case intro.intro.intro.intro
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
mb : m < b
i0 : ∫ (x : X) in s \ t, f x ≤ (vs - vt) * b
⊢ (∫ (x : X) in s \ t, f x) + ∫ (x : X) in t, f x < b * vs
Tactic:
have i1 : ∫ x in t, f x ≤ vt * m := by
  have fm := @setIntegral_mono_on _ _ volume f (fun _ ↦ m) t (fi.mono ts (le_refl _))
    (integrableOn_const.mpr (Or.inr tf)) tm ?_
  simp at fm; exact fm
  intro y yt
  rw [← ht] at yt; simp at ht yt
  specialize he y yt.left yt.right
  simp [Real.dist_eq] at he
  calc f y
    _ = f x + (f y - f x) := by ring
    _ ≤ f x + |f y - f x| := by bound
    _ ≤ f x + (b - f x) / 2 := by bound
    _ = (b + f x) / 2 := by ring
State after:
case intro.intro.intro.intro
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
mb : m < b
i0 : ∫ (x : X) in s \ t, f x ≤ (vs - vt) * b
i1 : ∫ (x : X) in t, f x ≤ vt * m
⊢ (∫ (x : X) in s \ t, f x) + ∫ (x : X) in t, f x < b * vs

State before:
case intro.intro.intro.intro
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
mb : m < b
i0 : ∫ (x : X) in s \ t, f x ≤ (vs - vt) * b
i1 : ∫ (x : X) in t, f x ≤ vt * m
⊢ (∫ (x : X) in s \ t, f x) + ∫ (x : X) in t, f x < b * vs
Tactic:
calc (∫ x : X in s \ t, f x) + ∫ x : X in t, f x
  _ ≤ (vs - vt) * b + vt * m := by bound
  _ = vs * b - vt * (b - m) := by ring
  _ < vs * b - 0 := (sub_lt_sub_left (by bound) _)
  _ = b * vs := by ring
State after:
no goals

State before:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
⊢ m < b
Tactic:
calc (b + f x) / 2
  _ < (b + b) / 2 := (div_lt_div_right (by norm_num)).mpr (by bound)
  _ = b := by ring
State after:
no goals

State before:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
⊢ 0 < 2
Tactic:
norm_num
State after:
no goals

State before:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
⊢ b + f x < b + b
Tactic:
bound
State after:
no goals

State before:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
⊢ (b + b) / 2 = b
Tactic:
ring
State after:
no goals

State before:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
mb : m < b
⊢ ∫ (x : X) in s \ t, f x ≤ (vs - vt) * b
Tactic:
have df : volume (s \ t) < ⊤ := lt_of_le_of_lt (measure_mono (Set.diff_subset _ _)) sn.finite
State after:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
mb : m < b
df : ↑volume (s \ t) < ⊤
⊢ ∫ (x : X) in s \ t, f x ≤ (vs - vt) * b

State before:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
mb : m < b
df : ↑volume (s \ t) < ⊤
⊢ ∫ (x : X) in s \ t, f x ≤ (vs - vt) * b
Tactic:
have dm : MeasurableSet (s \ t) := MeasurableSet.diff sn.measurable tm
State after:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
mb : m < b
df : ↑volume (s \ t) < ⊤
dm : MeasurableSet (s \ t)
⊢ ∫ (x : X) in s \ t, f x ≤ (vs - vt) * b

State before:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
mb : m < b
df : ↑volume (s \ t) < ⊤
dm : MeasurableSet (s \ t)
⊢ ∫ (x : X) in s \ t, f x ≤ (vs - vt) * b
Tactic:
have fb := @setIntegral_mono_on _ _ volume f (fun _ ↦ b) (s \ t)
  (fi.mono (Set.diff_subset _ _) (le_refl _)) (integrableOn_const.mpr (Or.inr df)) dm ?_
State after:
case refine_2
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
mb : m < b
df : ↑volume (s \ t) < ⊤
dm : MeasurableSet (s \ t)
fb : ∫ (x : X) in s \ t, f x ≤ ∫ (x : X) in s \ t, (fun x => b) x
⊢ ∫ (x : X) in s \ t, f x ≤ (vs - vt) * b

case refine_1
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
mb : m < b
df : ↑volume (s \ t) < ⊤
dm : MeasurableSet (s \ t)
⊢ ∀ x ∈ s \ t, f x ≤ (fun x => b) x

State before:
case refine_2
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
mb : m < b
df : ↑volume (s \ t) < ⊤
dm : MeasurableSet (s \ t)
fb : ∫ (x : X) in s \ t, f x ≤ ∫ (x : X) in s \ t, (fun x => b) x
⊢ ∫ (x : X) in s \ t, f x ≤ (vs - vt) * b

case refine_1
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
mb : m < b
df : ↑volume (s \ t) < ⊤
dm : MeasurableSet (s \ t)
⊢ ∀ x ∈ s \ t, f x ≤ (fun x => b) x
Tactic:
simp [measure_diff ts tm (lt_top_iff_ne_top.mp tf),
  ENNReal.toReal_sub_of_le (measure_mono ts) (lt_top_iff_ne_top.mp sn.finite)] at fb
State after:
case refine_2
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
mb : m < b
df : ↑volume (s \ t) < ⊤
dm : MeasurableSet (s \ t)
fb : ∫ (x : X) in s \ t, f x ≤ ((↑volume s).toReal - (↑volume t).toReal) * b
⊢ ∫ (x : X) in s \ t, f x ≤ (vs - vt) * b

case refine_1
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
mb : m < b
df : ↑volume (s \ t) < ⊤
dm : MeasurableSet (s \ t)
⊢ ∀ x ∈ s \ t, f x ≤ (fun x => b) x

State before:
case refine_2
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
mb : m < b
df : ↑volume (s \ t) < ⊤
dm : MeasurableSet (s \ t)
fb : ∫ (x : X) in s \ t, f x ≤ ((↑volume s).toReal - (↑volume t).toReal) * b
⊢ ∫ (x : X) in s \ t, f x ≤ (vs - vt) * b

case refine_1
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
mb : m < b
df : ↑volume (s \ t) < ⊤
dm : MeasurableSet (s \ t)
⊢ ∀ x ∈ s \ t, f x ≤ (fun x => b) x
Tactic:
exact fb
State after:
case refine_1
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
mb : m < b
df : ↑volume (s \ t) < ⊤
dm : MeasurableSet (s \ t)
⊢ ∀ x ∈ s \ t, f x ≤ (fun x => b) x

State before:
case refine_1
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
mb : m < b
df : ↑volume (s \ t) < ⊤
dm : MeasurableSet (s \ t)
⊢ ∀ x ∈ s \ t, f x ≤ (fun x => b) x
Tactic:
intro y yd
State after:
case refine_1
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
mb : m < b
df : ↑volume (s \ t) < ⊤
dm : MeasurableSet (s \ t)
y : X
yd : y ∈ s \ t
⊢ f y ≤ (fun x => b) y

State before:
case refine_1
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
mb : m < b
df : ↑volume (s \ t) < ⊤
dm : MeasurableSet (s \ t)
y : X
yd : y ∈ s \ t
⊢ f y ≤ (fun x => b) y
Tactic:
simp at yd
State after:
case refine_1
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
mb : m < b
df : ↑volume (s \ t) < ⊤
dm : MeasurableSet (s \ t)
y : X
yd : y ∈ s ∧ y ∉ t
⊢ f y ≤ (fun x => b) y

State before:
case refine_1
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
mb : m < b
df : ↑volume (s \ t) < ⊤
dm : MeasurableSet (s \ t)
y : X
yd : y ∈ s ∧ y ∉ t
⊢ f y ≤ (fun x => b) y
Tactic:
exact hi y yd.left
State after:
no goals

State before:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
mb : m < b
i0 : ∫ (x : X) in s \ t, f x ≤ (vs - vt) * b
⊢ ∫ (x : X) in t, f x ≤ vt * m
Tactic:
have fm := @setIntegral_mono_on _ _ volume f (fun _ ↦ m) t (fi.mono ts (le_refl _))
  (integrableOn_const.mpr (Or.inr tf)) tm ?_
State after:
case refine_2
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
mb : m < b
i0 : ∫ (x : X) in s \ t, f x ≤ (vs - vt) * b
fm : ∫ (x : X) in t, f x ≤ ∫ (x : X) in t, (fun x => m) x
⊢ ∫ (x : X) in t, f x ≤ vt * m

case refine_1
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
mb : m < b
i0 : ∫ (x : X) in s \ t, f x ≤ (vs - vt) * b
⊢ ∀ x ∈ t, f x ≤ (fun x => m) x

State before:
case refine_2
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
mb : m < b
i0 : ∫ (x : X) in s \ t, f x ≤ (vs - vt) * b
fm : ∫ (x : X) in t, f x ≤ ∫ (x : X) in t, (fun x => m) x
⊢ ∫ (x : X) in t, f x ≤ vt * m

case refine_1
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
mb : m < b
i0 : ∫ (x : X) in s \ t, f x ≤ (vs - vt) * b
⊢ ∀ x ∈ t, f x ≤ (fun x => m) x
Tactic:
simp at fm
State after:
case refine_2
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
mb : m < b
i0 : ∫ (x : X) in s \ t, f x ≤ (vs - vt) * b
fm : ∫ (x : X) in t, f x ≤ (↑volume t).toReal * m
⊢ ∫ (x : X) in t, f x ≤ vt * m

case refine_1
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
mb : m < b
i0 : ∫ (x : X) in s \ t, f x ≤ (vs - vt) * b
⊢ ∀ x ∈ t, f x ≤ (fun x => m) x

State before:
case refine_2
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
mb : m < b
i0 : ∫ (x : X) in s \ t, f x ≤ (vs - vt) * b
fm : ∫ (x : X) in t, f x ≤ (↑volume t).toReal * m
⊢ ∫ (x : X) in t, f x ≤ vt * m

case refine_1
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
mb : m < b
i0 : ∫ (x : X) in s \ t, f x ≤ (vs - vt) * b
⊢ ∀ x ∈ t, f x ≤ (fun x => m) x
Tactic:
exact fm
State after:
case refine_1
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
mb : m < b
i0 : ∫ (x : X) in s \ t, f x ≤ (vs - vt) * b
⊢ ∀ x ∈ t, f x ≤ (fun x => m) x

State before:
case refine_1
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
mb : m < b
i0 : ∫ (x : X) in s \ t, f x ≤ (vs - vt) * b
⊢ ∀ x ∈ t, f x ≤ (fun x => m) x
Tactic:
intro y yt
State after:
case refine_1
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
mb : m < b
i0 : ∫ (x : X) in s \ t, f x ≤ (vs - vt) * b
y : X
yt : y ∈ t
⊢ f y ≤ (fun x => m) y

State before:
case refine_1
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
mb : m < b
i0 : ∫ (x : X) in s \ t, f x ≤ (vs - vt) * b
y : X
yt : y ∈ t
⊢ f y ≤ (fun x => m) y
Tactic:
rw [← ht] at yt
State after:
case refine_1
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
mb : m < b
i0 : ∫ (x : X) in s \ t, f x ≤ (vs - vt) * b
y : X
yt : y ∈ s ∩ ball x e
⊢ f y ≤ (fun x => m) y

State before:
case refine_1
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
mb : m < b
i0 : ∫ (x : X) in s \ t, f x ≤ (vs - vt) * b
y : X
yt : y ∈ s ∩ ball x e
⊢ f y ≤ (fun x => m) y
Tactic:
simp at ht yt
State after:
case refine_1
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
mb : m < b
i0 : ∫ (x : X) in s \ t, f x ≤ (vs - vt) * b
y : X
yt : y ∈ s ∧ dist y x < e
⊢ f y ≤ (fun x => m) y

State before:
case refine_1
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
mb : m < b
i0 : ∫ (x : X) in s \ t, f x ≤ (vs - vt) * b
y : X
yt : y ∈ s ∧ dist y x < e
⊢ f y ≤ (fun x => m) y
Tactic:
specialize he y yt.left yt.right
State after:
case refine_1
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
mb : m < b
i0 : ∫ (x : X) in s \ t, f x ≤ (vs - vt) * b
y : X
yt : y ∈ s ∧ dist y x < e
he : dist (f y) (f x) < (b - f x) / 2
⊢ f y ≤ (fun x => m) y

State before:
case refine_1
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
mb : m < b
i0 : ∫ (x : X) in s \ t, f x ≤ (vs - vt) * b
y : X
yt : y ∈ s ∧ dist y x < e
he : dist (f y) (f x) < (b - f x) / 2
⊢ f y ≤ (fun x => m) y
Tactic:
simp [Real.dist_eq] at he
State after:
case refine_1
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
mb : m < b
i0 : ∫ (x : X) in s \ t, f x ≤ (vs - vt) * b
y : X
yt : y ∈ s ∧ dist y x < e
he : |f y - f x| < (b - f x) / 2
⊢ f y ≤ (fun x => m) y

State before:
case refine_1
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
mb : m < b
i0 : ∫ (x : X) in s \ t, f x ≤ (vs - vt) * b
y : X
yt : y ∈ s ∧ dist y x < e
he : |f y - f x| < (b - f x) / 2
⊢ f y ≤ (fun x => m) y
Tactic:
calc f y
  _ = f x + (f y - f x) := by ring
  _ ≤ f x + |f y - f x| := by bound
  _ ≤ f x + (b - f x) / 2 := by bound
  _ = (b + f x) / 2 := by ring
State after:
no goals

State before:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
mb : m < b
i0 : ∫ (x : X) in s \ t, f x ≤ (vs - vt) * b
y : X
yt : y ∈ s ∧ dist y x < e
he : |f y - f x| < (b - f x) / 2
⊢ f y = f x + (f y - f x)
Tactic:
ring
State after:
no goals

State before:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
mb : m < b
i0 : ∫ (x : X) in s \ t, f x ≤ (vs - vt) * b
y : X
yt : y ∈ s ∧ dist y x < e
he : |f y - f x| < (b - f x) / 2
⊢ f x + (f y - f x) ≤ f x + |f y - f x|
Tactic:
bound
State after:
no goals

State before:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
mb : m < b
i0 : ∫ (x : X) in s \ t, f x ≤ (vs - vt) * b
y : X
yt : y ∈ s ∧ dist y x < e
he : |f y - f x| < (b - f x) / 2
⊢ f x + |f y - f x| ≤ f x + (b - f x) / 2
Tactic:
bound
State after:
no goals

State before:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
mb : m < b
i0 : ∫ (x : X) in s \ t, f x ≤ (vs - vt) * b
y : X
yt : y ∈ s ∧ dist y x < e
he : |f y - f x| < (b - f x) / 2
⊢ f x + (b - f x) / 2 = (b + f x) / 2
Tactic:
ring
State after:
no goals

State before:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
mb : m < b
i0 : ∫ (x : X) in s \ t, f x ≤ (vs - vt) * b
i1 : ∫ (x : X) in t, f x ≤ vt * m
⊢ (∫ (x : X) in s \ t, f x) + ∫ (x : X) in t, f x ≤ (vs - vt) * b + vt * m
Tactic:
bound
State after:
no goals

State before:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
mb : m < b
i0 : ∫ (x : X) in s \ t, f x ≤ (vs - vt) * b
i1 : ∫ (x : X) in t, f x ≤ vt * m
⊢ (vs - vt) * b + vt * m = vs * b - vt * (b - m)
Tactic:
ring
State after:
no goals

State before:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
mb : m < b
i0 : ∫ (x : X) in s \ t, f x ≤ (vs - vt) * b
i1 : ∫ (x : X) in t, f x ≤ vt * m
⊢ 0 < vt * (b - m)
Tactic:
bound
State after:
no goals

State before:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
m : ℝ := (b + f x) / 2
vs : ℝ := (↑volume s).toReal
vt : ℝ := (↑volume t).toReal
vsp : vs > 0
vtp : vt > 0
mb : m < b
i0 : ∫ (x : X) in s \ t, f x ≤ (vs - vt) * b
i1 : ∫ (x : X) in t, f x ≤ vt * m
⊢ vs * b - 0 = b * vs
Tactic:
ring
State after:
no goals

State before:
case intro.intro.intro.intro.hst
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
⊢ Disjoint (s \ t) t
Tactic:
rw [disjoint_comm]
State after:
case intro.intro.intro.intro.hst
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
⊢ Disjoint t (s \ t)

State before:
case intro.intro.intro.intro.hst
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
⊢ Disjoint t (s \ t)
Tactic:
exact Set.disjoint_sdiff_right
State after:
no goals

State before:
case intro.intro.intro.intro.ht
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
⊢ MeasurableSet t
Tactic:
exact tm
State after:
no goals

State before:
case intro.intro.intro.intro.hfs
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
⊢ IntegrableOn (fun x => f x) (s \ t) volume
Tactic:
exact fi.mono (Set.diff_subset _ _) (le_refl _)
State after:
no goals

State before:
case intro.intro.intro.intro.hft
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ
s : Set X
b : ℝ
sn : NiceVolume s
lv : LocalVolumeSet s
fc : ContinuousOn f s
fi : IntegrableOn f s volume
hi : ∀ x ∈ s, f x ≤ b
x : X
xs : x ∈ s
fx : f x < b
e : ℝ
ep : e > 0
he : ∀ a ∈ s, dist a x < e → dist (f a) (f x) < (b - f x) / 2
t : Set X
vtp' : 0 < ↑volume t
ht : s ∩ ball x e = t
ts : t ⊆ s
tf : ↑volume t < ⊤
tm : MeasurableSet t
sc : s \ t ∪ t = s
⊢ IntegrableOn (fun x => f x) t volume
Tactic:
exact fi.mono ts (le_refl _)
State after:
no goals