Theorem: LocalVolume.closure_interior (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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
⊢ LocalVolumeSet s
Tactic:
intro x r xs rp
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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
⊢ 0 < ↑volume (s ∩ ball x r)

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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
⊢ 0 < ↑volume (s ∩ ball x r)
Tactic:
have xci := ci xs
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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
xci : x ∈ closure (interior s)
⊢ 0 < ↑volume (s ∩ ball x r)

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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
xci : x ∈ closure (interior s)
⊢ 0 < ↑volume (s ∩ ball x r)
Tactic:
rcases Metric.mem_closure_iff.mp xci r rp with ⟨y, ys, xy⟩
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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
xci : x ∈ closure (interior s)
y : X
ys : y ∈ interior s
xy : dist x y < r
⊢ 0 < ↑volume (s ∩ ball x r)

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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
xci : x ∈ closure (interior s)
y : X
ys : y ∈ interior s
xy : dist x y < r
⊢ 0 < ↑volume (s ∩ ball x r)
Tactic:
rcases Metric.isOpen_iff.mp isOpen_interior y ys with ⟨e, ep, ye⟩
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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
xci : x ∈ closure (interior s)
y : X
ys : y ∈ interior s
xy : dist x y < r
e : ℝ
ep : e > 0
ye : ball y e ⊆ interior s
⊢ 0 < ↑volume (s ∩ ball x r)

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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
xci : x ∈ closure (interior s)
y : X
ys : y ∈ interior s
xy : dist x y < r
e : ℝ
ep : e > 0
ye : ball y e ⊆ interior s
⊢ 0 < ↑volume (s ∩ ball x r)
Tactic:
set t := min e (r - dist x y)
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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
xci : x ∈ closure (interior s)
y : X
ys : y ∈ interior s
xy : dist x y < r
e : ℝ
ep : e > 0
ye : ball y e ⊆ interior s
t : ℝ := min e (r - dist x y)
⊢ 0 < ↑volume (s ∩ ball x r)

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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
xci : x ∈ closure (interior s)
y : X
ys : y ∈ interior s
xy : dist x y < r
e : ℝ
ep : e > 0
ye : ball y e ⊆ interior s
t : ℝ := min e (r - dist x y)
⊢ 0 < ↑volume (s ∩ ball x r)
Tactic:
have es : ball y t ⊆ s ∩ ball x r := by
  simp only [Set.subset_inter_iff]; constructor
  exact _root_.trans (Metric.ball_subset_ball (by bound)) (_root_.trans ye interior_subset)
  apply Metric.ball_subset_ball'
  trans r - dist x y + dist y x; bound; simp [dist_comm]
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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
xci : x ∈ closure (interior s)
y : X
ys : y ∈ interior s
xy : dist x y < r
e : ℝ
ep : e > 0
ye : ball y e ⊆ interior s
t : ℝ := min e (r - dist x y)
es : ball y t ⊆ s ∩ ball x r
⊢ 0 < ↑volume (s ∩ ball x r)

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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
xci : x ∈ closure (interior s)
y : X
ys : y ∈ interior s
xy : dist x y < r
e : ℝ
ep : e > 0
ye : ball y e ⊆ interior s
t : ℝ := min e (r - dist x y)
es : ball y t ⊆ s ∩ ball x r
⊢ 0 < ↑volume (s ∩ ball x r)
Tactic:
exact lt_of_lt_of_le (bp y t (by bound)) (measure_mono es)
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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
xci : x ∈ closure (interior s)
y : X
ys : y ∈ interior s
xy : dist x y < r
e : ℝ
ep : e > 0
ye : ball y e ⊆ interior s
t : ℝ := min e (r - dist x y)
⊢ ball y t ⊆ s ∩ ball x r
Tactic:
simp only [Set.subset_inter_iff]
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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
xci : x ∈ closure (interior s)
y : X
ys : y ∈ interior s
xy : dist x y < r
e : ℝ
ep : e > 0
ye : ball y e ⊆ interior s
t : ℝ := min e (r - dist x y)
⊢ ball y t ⊆ s ∧ ball y t ⊆ ball x r

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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
xci : x ∈ closure (interior s)
y : X
ys : y ∈ interior s
xy : dist x y < r
e : ℝ
ep : e > 0
ye : ball y e ⊆ interior s
t : ℝ := min e (r - dist x y)
⊢ ball y t ⊆ s ∧ ball y t ⊆ ball x r
Tactic:
constructor
State after:
case left
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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
xci : x ∈ closure (interior s)
y : X
ys : y ∈ interior s
xy : dist x y < r
e : ℝ
ep : e > 0
ye : ball y e ⊆ interior s
t : ℝ := min e (r - dist x y)
⊢ ball y t ⊆ s

case right
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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
xci : x ∈ closure (interior s)
y : X
ys : y ∈ interior s
xy : dist x y < r
e : ℝ
ep : e > 0
ye : ball y e ⊆ interior s
t : ℝ := min e (r - dist x y)
⊢ ball y t ⊆ ball x r

State before:
case left
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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
xci : x ∈ closure (interior s)
y : X
ys : y ∈ interior s
xy : dist x y < r
e : ℝ
ep : e > 0
ye : ball y e ⊆ interior s
t : ℝ := min e (r - dist x y)
⊢ ball y t ⊆ s

case right
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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
xci : x ∈ closure (interior s)
y : X
ys : y ∈ interior s
xy : dist x y < r
e : ℝ
ep : e > 0
ye : ball y e ⊆ interior s
t : ℝ := min e (r - dist x y)
⊢ ball y t ⊆ ball x r
Tactic:
exact _root_.trans (Metric.ball_subset_ball (by bound)) (_root_.trans ye interior_subset)
State after:
case right
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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
xci : x ∈ closure (interior s)
y : X
ys : y ∈ interior s
xy : dist x y < r
e : ℝ
ep : e > 0
ye : ball y e ⊆ interior s
t : ℝ := min e (r - dist x y)
⊢ ball y t ⊆ ball x r

State before:
case right
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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
xci : x ∈ closure (interior s)
y : X
ys : y ∈ interior s
xy : dist x y < r
e : ℝ
ep : e > 0
ye : ball y e ⊆ interior s
t : ℝ := min e (r - dist x y)
⊢ ball y t ⊆ ball x r
Tactic:
apply Metric.ball_subset_ball'
State after:
case right.h
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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
xci : x ∈ closure (interior s)
y : X
ys : y ∈ interior s
xy : dist x y < r
e : ℝ
ep : e > 0
ye : ball y e ⊆ interior s
t : ℝ := min e (r - dist x y)
⊢ t + dist y x ≤ r

State before:
case right.h
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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
xci : x ∈ closure (interior s)
y : X
ys : y ∈ interior s
xy : dist x y < r
e : ℝ
ep : e > 0
ye : ball y e ⊆ interior s
t : ℝ := min e (r - dist x y)
⊢ t + dist y x ≤ r
Tactic:
trans r - dist x y + dist y x
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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
xci : x ∈ closure (interior s)
y : X
ys : y ∈ interior s
xy : dist x y < r
e : ℝ
ep : e > 0
ye : ball y e ⊆ interior s
t : ℝ := min e (r - dist x y)
⊢ t + dist y x ≤ r - dist x y + dist y x

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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
xci : x ∈ closure (interior s)
y : X
ys : y ∈ interior s
xy : dist x y < r
e : ℝ
ep : e > 0
ye : ball y e ⊆ interior s
t : ℝ := min e (r - dist x y)
⊢ r - dist x y + dist y x ≤ r

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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
xci : x ∈ closure (interior s)
y : X
ys : y ∈ interior s
xy : dist x y < r
e : ℝ
ep : e > 0
ye : ball y e ⊆ interior s
t : ℝ := min e (r - dist x y)
⊢ t + dist y x ≤ r - dist x y + dist y x

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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
xci : x ∈ closure (interior s)
y : X
ys : y ∈ interior s
xy : dist x y < r
e : ℝ
ep : e > 0
ye : ball y e ⊆ interior s
t : ℝ := min e (r - dist x y)
⊢ r - dist x y + dist y x ≤ r
Tactic:
bound
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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
xci : x ∈ closure (interior s)
y : X
ys : y ∈ interior s
xy : dist x y < r
e : ℝ
ep : e > 0
ye : ball y e ⊆ interior s
t : ℝ := min e (r - dist x y)
⊢ r - dist x y + dist y x ≤ r

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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
xci : x ∈ closure (interior s)
y : X
ys : y ∈ interior s
xy : dist x y < r
e : ℝ
ep : e > 0
ye : ball y e ⊆ interior s
t : ℝ := min e (r - dist x y)
⊢ r - dist x y + dist y x ≤ r
Tactic:
simp [dist_comm]
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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
xci : x ∈ closure (interior s)
y : X
ys : y ∈ interior s
xy : dist x y < r
e : ℝ
ep : e > 0
ye : ball y e ⊆ interior s
t : ℝ := min e (r - dist x y)
⊢ t ≤ e
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
s : Set X
bp : ∀ (x : X), ∀ r > 0, ↑volume (ball x r) > 0
ci : s ⊆ closure (interior s)
x : X
r : ℝ
xs : x ∈ s
rp : 0 < r
xci : x ∈ closure (interior s)
y : X
ys : y ∈ interior s
xy : dist x y < r
e : ℝ
ep : e > 0
ye : ball y e ⊆ interior s
t : ℝ := min e (r - dist x y)
es : ball y t ⊆ s ∩ ball x r
⊢ t > 0
Tactic:
bound
State after:
no goals