Theorem: ball_subset_ball_of_le (Carleson/HomogeneousType.lean)

State before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x x' : X
r r' : ℝ
hr : dist x x' + r' ≤ r
⊢ ball x' r' ⊆ ball x r
Tactic:
intro y h
State after:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x x' : X
r r' : ℝ
hr : dist x x' + r' ≤ r
y : X
h : y ∈ ball x' r'
⊢ y ∈ ball x r

State before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x x' : X
r r' : ℝ
hr : dist x x' + r' ≤ r
y : X
h : y ∈ ball x' r'
⊢ y ∈ ball x r
Tactic:
have h1 : dist x y < r := by
  calc dist x y ≤ dist x x' + dist x' y := by apply dist_triangle
      _ < dist x x' + r' := by gcongr; apply mem_ball'.mp h
      _ ≤ r := by apply hr
State after:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x x' : X
r r' : ℝ
hr : dist x x' + r' ≤ r
y : X
h : y ∈ ball x' r'
h1 : dist x y < r
⊢ y ∈ ball x r

State before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x x' : X
r r' : ℝ
hr : dist x x' + r' ≤ r
y : X
h : y ∈ ball x' r'
h1 : dist x y < r
⊢ y ∈ ball x r
Tactic:
exact mem_ball'.mpr h1
State after:
no goals

State before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x x' : X
r r' : ℝ
hr : dist x x' + r' ≤ r
y : X
h : y ∈ ball x' r'
⊢ dist x y < r
Tactic:
calc dist x y ≤ dist x x' + dist x' y := by apply dist_triangle
    _ < dist x x' + r' := by gcongr; apply mem_ball'.mp h
    _ ≤ r := by apply hr
State after:
no goals

State before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x x' : X
r r' : ℝ
hr : dist x x' + r' ≤ r
y : X
h : y ∈ ball x' r'
⊢ dist x y ≤ dist x x' + dist x' y
Tactic:
apply dist_triangle
State after:
no goals

State before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x x' : X
r r' : ℝ
hr : dist x x' + r' ≤ r
y : X
h : y ∈ ball x' r'
⊢ dist x x' + dist x' y < dist x x' + r'
Tactic:
gcongr
State after:
case bc
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x x' : X
r r' : ℝ
hr : dist x x' + r' ≤ r
y : X
h : y ∈ ball x' r'
⊢ dist x' y < r'

State before:
case bc
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x x' : X
r r' : ℝ
hr : dist x x' + r' ≤ r
y : X
h : y ∈ ball x' r'
⊢ dist x' y < r'
Tactic:
apply mem_ball'.mp h
State after:
no goals

State before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x x' : X
r r' : ℝ
hr : dist x x' + r' ≤ r
y : X
h : y ∈ ball x' r'
⊢ dist x x' + r' ≤ r
Tactic:
apply hr
State after:
no goals