case a
E : Type u_1
X : Type ?u.80093
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace ℝ X
inst✝ : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
hx : x ∈ closedBall c f.rIn
⊢ ‖(fun x => f.rIn⁻¹ • (x - c)) x‖ ≤ 1
E : Type u_1
X : Type ?u.80093
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace ℝ X
inst✝ : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
hx : x ∈ closedBall c f.rIn
⊢ ↑f x = 1
apply ContDiffBumpBase.eq_one _ _ f.one_lt_rOut_div_rIn
no goals
case a
E : Type u_1
X : Type ?u.80093
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace ℝ X
inst✝ : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
hx : x ∈ closedBall c f.rIn
⊢ ‖(fun x => f.rIn⁻¹ • (x - c)) x‖ ≤ 1
simpa only [norm_smul, norm_eq_abs, abs_inv, abs_of_nonneg f.rIn_pos.le, ← div_eq_inv_mul,
  div_le_one f.rIn_pos] using mem_closedBall_iff_norm.1 hx