-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem ContDiffWithinAt.comp_continuousLinearMap {x : G} (g : G →L[𝕜] E)
    (hf : ContDiffWithinAt 𝕜 n f s (g x)) : ContDiffWithinAt 𝕜 n (f ∘ g) (g ⁻¹' s) x

Proof state:
case intro.intro.intro.intro
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
f : E → F
n : WithTop ℕ∞
x : G
g : G →L[𝕜] E
u : Set E
hu : u ∈ 𝓝[insert (g x) s] g x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p u
h'p : ∀ (i : ℕ), AnalyticOn 𝕜 (fun x => p x i) u
⊢ ContDiffWithinAt 𝕜 ω (f ∘ ⇑g) (⇑g ⁻¹' s) x

Tactic:
refine ⟨g ⁻¹' u, ?_, _, hp.compContinuousLinearMap g, ?_⟩

Result:
case intro.intro.intro.intro.refine_1
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
f : E → F
n : WithTop ℕ∞
x : G
g : G →L[𝕜] E
u : Set E
hu : u ∈ 𝓝[insert (g x) s] g x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p u
h'p : ∀ (i : ℕ), AnalyticOn 𝕜 (fun x => p x i) u
⊢ ⇑g ⁻¹' u ∈ 𝓝[insert x (⇑g ⁻¹' s)] x

case intro.intro.intro.intro.refine_2
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
f : E → F
n : WithTop ℕ∞
x : G
g : G →L[𝕜] E
u : Set E
hu : u ∈ 𝓝[insert (g x) s] g x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p u
h'p : ∀ (i : ℕ), AnalyticOn 𝕜 (fun x => p x i) u
⊢ ∀ (i : ℕ), AnalyticOn 𝕜 (fun x => (p (g x) i).compContinuousLinearMap fun x => g) (⇑g ⁻¹' u)

Proof state:
case intro.intro.intro.intro.refine_2
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
f : E → F
n : WithTop ℕ∞
x : G
g : G →L[𝕜] E
u : Set E
hu : u ∈ 𝓝[insert (g x) s] g x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p u
h'p : ∀ (i : ℕ), AnalyticOn 𝕜 (fun x => p x i) u
i : ℕ
⊢ AnalyticOn 𝕜 (fun x => (p (g x) i).compContinuousLinearMap fun x => g) (⇑g ⁻¹' u)

Tactic:
change AnalyticOn 𝕜 (fun x ↦
  ContinuousMultilinearMap.compContinuousLinearMapL (fun _ ↦ g) (p (g x) i)) (⇑g ⁻¹' u)

Result:
case intro.intro.intro.intro.refine_2
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
f : E → F
n : WithTop ℕ∞
x : G
g : G →L[𝕜] E
u : Set E
hu : u ∈ 𝓝[insert (g x) s] g x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p u
h'p : ∀ (i : ℕ), AnalyticOn 𝕜 (fun x => p x i) u
i : ℕ
⊢ AnalyticOn 𝕜 (fun x => (ContinuousMultilinearMap.compContinuousLinearMapL fun x => g) (p (g x) i)) (⇑g ⁻¹' u)

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
f : E → F
n : WithTop ℕ∞
x : G
g : G →L[𝕜] E
hf : ContDiffWithinAt 𝕜 ω f s (g x)
⊢ ContDiffWithinAt 𝕜 ω (f ∘ ⇑g) (⇑g ⁻¹' s) x

Tactic:
obtain ⟨u, hu, p, hp, h'p⟩ := hf

Result:
case intro.intro.intro.intro
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
f : E → F
n : WithTop ℕ∞
x : G
g : G →L[𝕜] E
u : Set E
hu : u ∈ 𝓝[insert (g x) s] g x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p u
h'p : ∀ (i : ℕ), AnalyticOn 𝕜 (fun x => p x i) u
⊢ ContDiffWithinAt 𝕜 ω (f ∘ ⇑g) (⇑g ⁻¹' s) x

Proof state:
case intro.intro.intro.intro.refine_2
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
f : E → F
n : WithTop ℕ∞
x : G
g : G →L[𝕜] E
u : Set E
hu : u ∈ 𝓝[insert (g x) s] g x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p u
h'p : ∀ (i : ℕ), AnalyticOn 𝕜 (fun x => p x i) u
⊢ ∀ (i : ℕ), AnalyticOn 𝕜 (fun x => (p (g x) i).compContinuousLinearMap fun x => g) (⇑g ⁻¹' u)

Tactic:
intro i

Result:
case intro.intro.intro.intro.refine_2
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
f : E → F
n : WithTop ℕ∞
x : G
g : G →L[𝕜] E
u : Set E
hu : u ∈ 𝓝[insert (g x) s] g x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p u
h'p : ∀ (i : ℕ), AnalyticOn 𝕜 (fun x => p x i) u
i : ℕ
⊢ AnalyticOn 𝕜 (fun x => (p (g x) i).compContinuousLinearMap fun x => g) (⇑g ⁻¹' u)

Proof state:
case intro.intro.intro.intro.refine_1
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
f : E → F
n : WithTop ℕ∞
x : G
g : G →L[𝕜] E
u : Set E
hu : u ∈ 𝓝[insert (g x) s] g x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p u
h'p : ∀ (i : ℕ), AnalyticOn 𝕜 (fun x => p x i) u
⊢ MapsTo (⇑g) (insert x (⇑g ⁻¹' s)) (insert (g x) s)

Tactic:
exact (mapsTo_singleton.2 <| mem_singleton _).union_union (mapsTo_preimage _ _)

Result:
no goals