-- Mathlib/Analysis/Calculus/BumpFunction/Basic.lean
theorem _root_.ContDiffWithinAt.contDiffBump {c g : X → E} {s : Set X}
    {f : ∀ x, ContDiffBump (c x)} {x : X} (hc : ContDiffWithinAt ℝ n c s x)
    (hr : ContDiffWithinAt ℝ n (fun x => (f x).rIn) s x)
    (hR : ContDiffWithinAt ℝ n (fun x => (f x).rOut) s x)
    (hg : ContDiffWithinAt ℝ n g s x) :
    ContDiffWithinAt ℝ n (fun x => f x (g x)) s x

Proof state:
case refine_2
E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace ℝ X
inst✝ : HasContDiffBump E
n : ℕ∞
c g : X → E
s : Set X
f : (x : X) → ContDiffBump (c x)
x : X
hc : ContDiffWithinAt ℝ (↑n) c s x
hr : ContDiffWithinAt ℝ (↑n) (fun x => (f x).rIn) s x
hR : ContDiffWithinAt ℝ (↑n) (fun x => (f x).rOut) s x
hg : ContDiffWithinAt ℝ (↑n) g s x
⊢ ContDiffWithinAt ℝ (↑n) (fun x => ((f x).rOut / (f x).rIn, (f x).rIn⁻¹ • (g x - c x))) s x

Tactic:
exact (hR.div hr (f x).rIn_pos.ne').prod ((hr.inv (f x).rIn_pos.ne').smul (hg.sub hc))

Result:
no goals

Proof state:
E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace ℝ X
inst✝ : HasContDiffBump E
n : ℕ∞
c g : X → E
s : Set X
f : (x : X) → ContDiffBump (c x)
x : X
hc : ContDiffWithinAt ℝ (↑n) c s x
hr : ContDiffWithinAt ℝ (↑n) (fun x => (f x).rIn) s x
hR : ContDiffWithinAt ℝ (↑n) (fun x => (f x).rOut) s x
hg : ContDiffWithinAt ℝ (↑n) g s x
⊢ ContDiffWithinAt ℝ (↑n)
    (uncurry (someContDiffBumpBase E).toFun ∘ fun x => ((f x).rOut / (f x).rIn, (f x).rIn⁻¹ • (g x - c x))) s x

Tactic:
refine (((someContDiffBumpBase E).smooth.contDiffAt ?_).of_le
  (mod_cast le_top)).comp_contDiffWithinAt x ?_

Result:
case refine_1
E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace ℝ X
inst✝ : HasContDiffBump E
n : ℕ∞
c g : X → E
s : Set X
f : (x : X) → ContDiffBump (c x)
x : X
hc : ContDiffWithinAt ℝ (↑n) c s x
hr : ContDiffWithinAt ℝ (↑n) (fun x => (f x).rIn) s x
hR : ContDiffWithinAt ℝ (↑n) (fun x => (f x).rOut) s x
hg : ContDiffWithinAt ℝ (↑n) g s x
⊢ Ioi 1 ×ˢ univ ∈ 𝓝 ((f x).rOut / (f x).rIn, (f x).rIn⁻¹ • (g x - c x))

case refine_2
E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace ℝ X
inst✝ : HasContDiffBump E
n : ℕ∞
c g : X → E
s : Set X
f : (x : X) → ContDiffBump (c x)
x : X
hc : ContDiffWithinAt ℝ (↑n) c s x
hr : ContDiffWithinAt ℝ (↑n) (fun x => (f x).rIn) s x
hR : ContDiffWithinAt ℝ (↑n) (fun x => (f x).rOut) s x
hg : ContDiffWithinAt ℝ (↑n) g s x
⊢ ContDiffWithinAt ℝ (↑n) (fun x => ((f x).rOut / (f x).rIn, (f x).rIn⁻¹ • (g x - c x))) s x

Proof state:
case refine_1
E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace ℝ X
inst✝ : HasContDiffBump E
n : ℕ∞
c g : X → E
s : Set X
f : (x : X) → ContDiffBump (c x)
x : X
hc : ContDiffWithinAt ℝ (↑n) c s x
hr : ContDiffWithinAt ℝ (↑n) (fun x => (f x).rIn) s x
hR : ContDiffWithinAt ℝ (↑n) (fun x => (f x).rOut) s x
hg : ContDiffWithinAt ℝ (↑n) g s x
⊢ Ioi 1 ×ˢ univ ∈ 𝓝 ((f x).rOut / (f x).rIn, (f x).rIn⁻¹ • (g x - c x))

Tactic:
exact prod_mem_nhds (Ioi_mem_nhds (f x).one_lt_rOut_div_rIn) univ_mem

Result:
no goals

Proof state:
E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace ℝ X
inst✝ : HasContDiffBump E
n : ℕ∞
c g : X → E
s : Set X
f : (x : X) → ContDiffBump (c x)
x : X
hc : ContDiffWithinAt ℝ (↑n) c s x
hr : ContDiffWithinAt ℝ (↑n) (fun x => (f x).rIn) s x
hR : ContDiffWithinAt ℝ (↑n) (fun x => (f x).rOut) s x
hg : ContDiffWithinAt ℝ (↑n) g s x
⊢ ContDiffWithinAt ℝ (↑n) (fun x => ↑(f x) (g x)) s x

Tactic:
change ContDiffWithinAt ℝ n (uncurry (someContDiffBumpBase E).toFun ∘ fun x : X =>
  ((f x).rOut / (f x).rIn, (f x).rIn⁻¹ • (g x - c x))) s x

Result:
E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace ℝ X
inst✝ : HasContDiffBump E
n : ℕ∞
c g : X → E
s : Set X
f : (x : X) → ContDiffBump (c x)
x : X
hc : ContDiffWithinAt ℝ (↑n) c s x
hr : ContDiffWithinAt ℝ (↑n) (fun x => (f x).rIn) s x
hR : ContDiffWithinAt ℝ (↑n) (fun x => (f x).rOut) s x
hg : ContDiffWithinAt ℝ (↑n) g s x
⊢ ContDiffWithinAt ℝ (↑n)
    (uncurry (someContDiffBumpBase E).toFun ∘ fun x => ((f x).rOut / (f x).rIn, (f x).rIn⁻¹ • (g x - c x))) s x