[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x✝¹ : ℝ
x✝ : E
⊢ (fun R x => smoothTransition ((R - ‖x‖) / (R - 1))) x✝¹ (-x✝) =
    (fun R x => smoothTransition ((R - ‖x‖) / (R - 1))) x✝¹ x✝
[PROOFSTEP]
simp only [norm_neg]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
⊢ ContDiffOn ℝ ⊤ (uncurry fun R x => smoothTransition ((R - ‖x‖) / (R - 1))) (Set.Ioi 1 ×ˢ Set.univ)
[PROOFSTEP]
rintro ⟨R, x⟩ ⟨hR : 1 < R, -⟩
[GOAL]
case mk.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
R : ℝ
x : E
hR : 1 < R
⊢ ContDiffWithinAt ℝ ⊤ (uncurry fun R x => smoothTransition ((R - ‖x‖) / (R - 1))) (Set.Ioi 1 ×ˢ Set.univ) (R, x)
[PROOFSTEP]
apply ContDiffAt.contDiffWithinAt
[GOAL]
case mk.intro.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
R : ℝ
x : E
hR : 1 < R
⊢ ContDiffAt ℝ ⊤ (uncurry fun R x => smoothTransition ((R - ‖x‖) / (R - 1))) (R, x)
[PROOFSTEP]
rw [← sub_pos] at hR 
[GOAL]
case mk.intro.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
R : ℝ
x : E
hR✝ : 1 < R
hR : 0 < R - 1
⊢ ContDiffAt ℝ ⊤ (uncurry fun R x => smoothTransition ((R - ‖x‖) / (R - 1))) (R, x)
[PROOFSTEP]
rcases eq_or_ne x 0 with rfl | hx
[GOAL]
case mk.intro.h.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
R : ℝ
hR✝ : 1 < R
hR : 0 < R - 1
⊢ ContDiffAt ℝ ⊤ (uncurry fun R x => smoothTransition ((R - ‖x‖) / (R - 1))) (R, 0)
[PROOFSTEP]
have A : ContinuousAt (fun p : ℝ × E ↦ (p.1 - ‖p.2‖) / (p.1 - 1)) (R, 0) :=
  (continuousAt_fst.sub continuousAt_snd.norm).div (continuousAt_fst.sub continuousAt_const) hR.ne'
[GOAL]
case mk.intro.h.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
R : ℝ
hR✝ : 1 < R
hR : 0 < R - 1
A : ContinuousAt (fun p => (p.fst - ‖p.snd‖) / (p.fst - 1)) (R, 0)
⊢ ContDiffAt ℝ ⊤ (uncurry fun R x => smoothTransition ((R - ‖x‖) / (R - 1))) (R, 0)
[PROOFSTEP]
have B : ∀ᶠ p in 𝓝 (R, (0 : E)), 1 ≤ (p.1 - ‖p.2‖) / (p.1 - 1) :=
  A.eventually <| le_mem_nhds <| (one_lt_div hR).2 <| sub_lt_sub_left (by simp) _
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
R : ℝ
hR✝ : 1 < R
hR : 0 < R - 1
A : ContinuousAt (fun p => (p.fst - ‖p.snd‖) / (p.fst - 1)) (R, 0)
⊢ ‖(R, 0).snd‖ < 1
[PROOFSTEP]
simp
[GOAL]
case mk.intro.h.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
R : ℝ
hR✝ : 1 < R
hR : 0 < R - 1
A : ContinuousAt (fun p => (p.fst - ‖p.snd‖) / (p.fst - 1)) (R, 0)
B : ∀ᶠ (p : ℝ × E) in 𝓝 (R, 0), 1 ≤ (p.fst - ‖p.snd‖) / (p.fst - 1)
⊢ ContDiffAt ℝ ⊤ (uncurry fun R x => smoothTransition ((R - ‖x‖) / (R - 1))) (R, 0)
[PROOFSTEP]
refine (contDiffAt_const (c := 1)).congr_of_eventuallyEq <| B.mono fun _ ↦ smoothTransition.one_of_one_le
[GOAL]
case mk.intro.h.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
R : ℝ
x : E
hR✝ : 1 < R
hR : 0 < R - 1
hx : x ≠ 0
⊢ ContDiffAt ℝ ⊤ (uncurry fun R x => smoothTransition ((R - ‖x‖) / (R - 1))) (R, x)
[PROOFSTEP]
refine smoothTransition.contDiffAt.comp _ (ContDiffAt.div ?_ ?_ hR.ne')
[GOAL]
case mk.intro.h.inr.refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
R : ℝ
x : E
hR✝ : 1 < R
hR : 0 < R - 1
hx : x ≠ 0
⊢ ContDiffAt ℝ ⊤ (fun a => a.fst - ‖a.snd‖) (R, x)
[PROOFSTEP]
exact contDiffAt_fst.sub (contDiffAt_snd.norm ℝ hx)
[GOAL]
case mk.intro.h.inr.refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
R : ℝ
x : E
hR✝ : 1 < R
hR : 0 < R - 1
hx : x ≠ 0
⊢ ContDiffAt ℝ ⊤ (fun a => a.fst - 1) (R, x)
[PROOFSTEP]
exact contDiffAt_fst.sub contDiffAt_const
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
R : ℝ
hR : 1 < R
⊢ Function.support ((fun R x => smoothTransition ((R - ‖x‖) / (R - 1))) R) = Metric.ball 0 R
[PROOFSTEP]
ext x
[GOAL]
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
R : ℝ
hR : 1 < R
x : E
⊢ x ∈ Function.support ((fun R x => smoothTransition ((R - ‖x‖) / (R - 1))) R) ↔ x ∈ Metric.ball 0 R
[PROOFSTEP]
rw [mem_support, Ne.def, smoothTransition.zero_iff_nonpos, not_le, mem_ball_zero_iff]
[GOAL]
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
R : ℝ
hR : 1 < R
x : E
⊢ 0 < (R - ‖x‖) / (R - 1) ↔ ‖x‖ < R
[PROOFSTEP]
simp [div_pos_iff, sq_lt_sq, abs_of_pos (one_pos.trans hR), hR, hR.not_lt]
