Theorem: volume_ball_four_le_same (Carleson/HomogeneousType.lean)

State before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r : ℝ
⊢ volume.real (ball x (4 * r)) ≤ A ^ 2 * volume.real (ball x r)
Tactic:
calc volume.real (ball x (4 * r))
    = volume.real (ball x (2 * (2 * r))) := by ring_nf
  _ ≤ A * volume.real (ball x (2 * r)) := by apply volume_ball_two_le_same
  _ ≤ A * (A * volume.real (ball x r)) := by gcongr; apply volume_ball_two_le_same
  _ = A ^ 2 * volume.real (ball x r) := by ring_nf
State after:
no goals

State before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r : ℝ
⊢ volume.real (ball x (4 * r)) = volume.real (ball x (2 * (2 * r)))
Tactic:
ring_nf
State after:
no goals

State before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r : ℝ
⊢ volume.real (ball x (2 * (2 * r))) ≤ A * volume.real (ball x (2 * r))
Tactic:
apply volume_ball_two_le_same
State after:
no goals

State before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r : ℝ
⊢ A * volume.real (ball x (2 * r)) ≤ A * (A * volume.real (ball x r))
Tactic:
gcongr
State after:
case h
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r : ℝ
⊢ volume.real (ball x (2 * r)) ≤ A * volume.real (ball x r)

State before:
case h
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r : ℝ
⊢ volume.real (ball x (2 * r)) ≤ A * volume.real (ball x r)
Tactic:
apply volume_ball_two_le_same
State after:
no goals

State before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r : ℝ
⊢ A * (A * volume.real (ball x r)) = A ^ 2 * volume.real (ball x r)
Tactic:
ring_nf
State after:
no goals