Theorem: le_of_ball_subset_closedBall (Ray/Hartogs/Hartogs.lean)

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0✝ z1✝ w0 w1 : ℂ
r r0✝ r1✝ b e : ℝ
z0 z1 : ℂ
r0 r1 : ℝ
r0p : r0 ≥ 0
r1p : r1 ≥ 0
⊢ ball z0 r0 ⊆ closedBall z1 r1 → r0 ≤ r1
Tactic:
intro s
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0✝ z1✝ w0 w1 : ℂ
r r0✝ r1✝ b e : ℝ
z0 z1 : ℂ
r0 r1 : ℝ
r0p : r0 ≥ 0
r1p : r1 ≥ 0
s : ball z0 r0 ⊆ closedBall z1 r1
⊢ r0 ≤ r1

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0✝ z1✝ w0 w1 : ℂ
r r0✝ r1✝ b e : ℝ
z0 z1 : ℂ
r0 r1 : ℝ
r0p : r0 ≥ 0
r1p : r1 ≥ 0
s : ball z0 r0 ⊆ closedBall z1 r1
⊢ r0 ≤ r1
Tactic:
have m := Metric.diam_mono s Metric.isBounded_closedBall
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0✝ z1✝ w0 w1 : ℂ
r r0✝ r1✝ b e : ℝ
z0 z1 : ℂ
r0 r1 : ℝ
r0p : r0 ≥ 0
r1p : r1 ≥ 0
s : ball z0 r0 ⊆ closedBall z1 r1
m : Metric.diam (ball z0 r0) ≤ Metric.diam (closedBall z1 r1)
⊢ r0 ≤ r1

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0✝ z1✝ w0 w1 : ℂ
r r0✝ r1✝ b e : ℝ
z0 z1 : ℂ
r0 r1 : ℝ
r0p : r0 ≥ 0
r1p : r1 ≥ 0
s : ball z0 r0 ⊆ closedBall z1 r1
m : Metric.diam (ball z0 r0) ≤ Metric.diam (closedBall z1 r1)
⊢ r0 ≤ r1
Tactic:
rw [diam_ball_eq r0p, diam_closedBall_eq r1p] at m
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0✝ z1✝ w0 w1 : ℂ
r r0✝ r1✝ b e : ℝ
z0 z1 : ℂ
r0 r1 : ℝ
r0p : r0 ≥ 0
r1p : r1 ≥ 0
s : ball z0 r0 ⊆ closedBall z1 r1
m : 2 * r0 ≤ 2 * r1
⊢ r0 ≤ r1

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0✝ z1✝ w0 w1 : ℂ
r r0✝ r1✝ b e : ℝ
z0 z1 : ℂ
r0 r1 : ℝ
r0p : r0 ≥ 0
r1p : r1 ≥ 0
s : ball z0 r0 ⊆ closedBall z1 r1
m : 2 * r0 ≤ 2 * r1
⊢ r0 ≤ r1
Tactic:
linarith
State after:
no goals