mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.ContDiff.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
n : ℕ∞ω
e : G ≃L[𝕜] E
⊢ ContDiffOn 𝕜 n (f ∘ ⇑e) (?m.75 ⁻¹' univ) ↔ ContDiffOn 𝕜 n f univ

pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
n : ℕ∞ω
e : G ≃L[𝕜] E
⊢ Type ?u.68

pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
n : ℕ∞ω
e : G ≃L[𝕜] E
⊢ G → ?m.74

Tactic:
exact e.contDiffOn_comp_iff

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.Basic

Goal state before:
pp: case zero_eq
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ∞ω
hf : HasFTaylorSeriesUpToOn n f p s
g : E → G
q : E → FormalMultilinearSeries 𝕜 E G
hg : HasFTaylorSeriesUpToOn n g q s
L : (m : ℕ) → (E [×m]→L[𝕜] F) × (E [×m]→L[𝕜] G) ≃ₗᵢ[𝕜] E [×m]→L[𝕜] F × G := ⋯
⊢ ∀ x ∈ s, ((p x 0).prod (q x 0)).curry0 = (f x, g x)

Tactic:
intro x hx

Goal state after:
case zero_eq
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ∞ω
hf : HasFTaylorSeriesUpToOn n f p s
g : E → G
q : E → FormalMultilinearSeries 𝕜 E G
hg : HasFTaylorSeriesUpToOn n g q s
L : (m : ℕ) → (E [×m]→L[𝕜] F) × (E [×m]→L[𝕜] G) ≃ₗᵢ[𝕜] E [×m]→L[𝕜] F × G :=
  fun m ↦ ContinuousMultilinearMap.prodL 𝕜 (fun x ↦ E) F G
x : E
hx : x ∈ s
⊢ ((p x 0).prod (q x 0)).curry0 = (f x, g x)
Module: Mathlib.Analysis.Calculus.FDeriv.OfCompLeft

Goal state before:
pp: case refine_1
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : E → F
f : F → G
h : E → G
g' : E →L[𝕜] F
f' : F →L[𝕜] G
h' : E →L[𝕜] G
lE : Filter (E × E)
lF : Filter (F × F)
hf_emb : Topology.IsEmbedding ⇑f'
htendsto : Tendsto (Prod.map g g) lE lF
hh : HasFDerivAtFilter h h' lE
hf : HasFDerivAtFilter f f' lF
hcomp : Prod.map (f ∘ g) (f ∘ g) =ᶠ[lE] Prod.map h h
ho :
  (fun x ↦
      match x with
      | (x, y) => g x - g y - g' (x - y)) =O[𝕜;
    lE] fun x ↦
    match x with
    | (x, y) => f' (g x - g y) - h' (x - y)
⊢ ∀ (x : E × E),
    Prod.map (f ∘ g) (f ∘ g) x = Prod.map h h x →
      ((fun p ↦ f p.1 - f p.2 - f' (p.1 - p.2)) ∘ Prod.map g g) x =
        ((fun p ↦ h p.1 - h p.2) - fun x ↦ f' (g x.1 - g x.2)) x

Tactic:
simp +contextual

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.OfCompLeft

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : E → F
f : F → G
h : E → G
g' : E →L[𝕜] F
f' : F →L[𝕜] G
h' : E →L[𝕜] G
lE : Filter (E × E)
lF : Filter (F × F)
hf_emb : Topology.IsEmbedding ⇑f'
htendsto : Tendsto (Prod.map g g) lE lF
hh : HasFDerivAtFilter h h' lE
hf : HasFDerivAtFilter f f' lF
hcomp : Prod.map (f ∘ g) (f ∘ g) =ᶠ[lE] Prod.map h h
ho :
  (fun x ↦
      match x with
      | (x, y) => g x - g y - g' (x - y)) =O[𝕜;
    lE] fun x ↦
    match x with
    | (x, y) => f' (g x - g y) - h' (x - y)
⊢ ∀ (x : E × E),
    Prod.map (f ∘ g) (f ∘ g) x = Prod.map h h x → (fun p ↦ h p.1 - h p.2) x = ((fun p ↦ f p.1 - f p.2) ∘ Prod.map g g) x

Tactic:
simp +contextual

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.Comp

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
x₀ : E
m n : ℕ∞ω
f : E → F → G
g : E → F
t : Set F
hf : ContDiffWithinAt 𝕜 n (uncurry f) (s ×ˢ t) (x₀, g x₀)
hg : ContDiffWithinAt 𝕜 m g s x₀
ht : UniqueDiffOn 𝕜 t
hmn : m + 1 ≤ n
hx₀ : x₀ ∈ s
hst : s ⊆ g ⁻¹' t
⊢ ContDiffWithinAt 𝕜 m (fun x ↦ fderivWithin 𝕜 (f x) t (g x)) s x₀

Tactic:
by
  rw [← insert_eq_self.mpr hx₀] at hf
  refine hf.fderivWithin' hg ?_ hmn hst
  rw [insert_eq_self.mpr hx₀]
  exact eventually_of_mem self_mem_nhdsWithin fun x hx => ht _ (hst hx)

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: case refine_1
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
hn : n ≠ ∞
hf : ContDiffWithinAt 𝕜 (n + 1) f s x
⊢ ∃ u ∈ 𝓝[insert x s] x,
    u ⊆ insert x s ∧
      (n = ω → AnalyticOn 𝕜 f u) ∧ ∃ f', (∀ x ∈ u, HasFDerivWithinAt f (f' x) s x) ∧ ContDiffWithinAt 𝕜 n f' s x

Tactic:
obtain ⟨u, hu, f_an, f', huf', hf'⟩ := (contDiffWithinAt_succ_iff_hasFDerivWithinAt hn).mp hf

Goal state after:
case refine_1
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
hn : n ≠ ∞
hf : ContDiffWithinAt 𝕜 (n + 1) f s x
u : Set E
hu : u ∈ 𝓝[insert x s] x
f_an : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
huf' : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
hf' : ContDiffWithinAt 𝕜 n f' u x
⊢ ∃ u ∈ 𝓝[insert x s] x,
    u ⊆ insert x s ∧
      (n = ω → AnalyticOn 𝕜 f u) ∧ ∃ f', (∀ x ∈ u, HasFDerivWithinAt f (f' x) s x) ∧ ContDiffWithinAt 𝕜 n f' s x
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ EqOn (iteratedDerivWithin n f s) (iteratedDeriv n f) s

Tactic:
intro x hx

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
x : 𝕜
hx : x ∈ s
⊢ iteratedDerivWithin n f s x = iteratedDeriv n f x
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: case cont
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞ω
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : ↑m ≤ n
⊢ ∀ x ∈ s,
    ∃ t,
      IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧
        x ∈ t ∧ ContinuousOn (fun x ↦ ftaylorSeriesWithin 𝕜 f s x m) (s ∩ t)

Tactic:
intro x hx

Goal state after:
case cont
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞ω
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : ↑m ≤ n
x : E
hx : x ∈ s
⊢ ∃ t,
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧
      x ∈ t ∧ ContinuousOn (fun x ↦ ftaylorSeriesWithin 𝕜 f s x m) (s ∩ t)
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞ω
h : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p s ∧ ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ p x i) s
⊢ ContDiffOn 𝕜 ω f s

Tactic:
intro x hx

Goal state after:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞ω
h : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p s ∧ ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ p x i) s
x : E
hx : x ∈ s
⊢ ContDiffWithinAt 𝕜 ω f s x
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞ω
h : ∀ (m : ℕ), AnalyticOn 𝕜 (iteratedFDerivWithin 𝕜 m f s) s
⊢ ContDiffOn 𝕜 ω f s

Tactic:
intro x hx

Goal state after:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞ω
h : ∀ (m : ℕ), AnalyticOn 𝕜 (iteratedFDerivWithin 𝕜 m f s) s
x : E
hx : x ∈ s
⊢ ContDiffWithinAt 𝕜 ω f s x
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞ω
m : ℕ
h : ContDiffOn 𝕜 n f s
hmn : ↑m < n
hs : UniqueDiffOn 𝕜 s
⊢ DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 m f s) s

Tactic:
intro x hx

Goal state after:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞ω
m : ℕ
h : ContDiffOn 𝕜 n f s
hmn : ↑m < n
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
⊢ DifferentiableWithinAt 𝕜 (iteratedFDerivWithin 𝕜 m f s) s x
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: case inr
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞ω
hf : DifferentiableOn 𝕜 f s
h' : n = ω → AnalyticOn 𝕜 f s
h : ContDiffOn 𝕜 n (fun y ↦ fderivWithin 𝕜 f s y) s
hn : n ≠ ∞
⊢ ContDiffOn 𝕜 (n + 1) f s

Tactic:
intro x hx

Goal state after:
case inr
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞ω
hf : DifferentiableOn 𝕜 f s
h' : n = ω → AnalyticOn 𝕜 f s
h : ContDiffOn 𝕜 n (fun y ↦ fderivWithin 𝕜 f s y) s
hn : n ≠ ∞
x : E
hx : x ∈ s
⊢ ContDiffWithinAt 𝕜 (n + 1) f s x
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: case inr
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞ω
hf : DifferentiableOn 𝕜 f s
h' : n = ω → AnalyticOn 𝕜 f s
h : ContDiffOn 𝕜 n (fun y ↦ fderivWithin 𝕜 f s y) s
hn : n ≠ ∞
⊢ ContDiffOn 𝕜 (n + 1) f s

Tactic:
· intro x hx
    rw [contDiffWithinAt_succ_iff_hasFDerivWithinAt hn,
      insert_eq_of_mem hx]
    exact ⟨s, self_mem_nhdsWithin, h', fderivWithin 𝕜 f s,
      fun y hy => (hf y hy).hasFDerivWithinAt, h x hx⟩

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞ω
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ ContDiffOn 𝕜 (n + 1) f s ↔ DifferentiableOn 𝕜 f s ∧ (n = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 n (fderiv 𝕜 f) s

Tactic:
rw [contDiffOn_succ_iff_fderivWithin hs.uniqueDiffOn,
    contDiffOn_congr fun x hx ↦ fderivWithin_of_isOpen hs hx]

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ
hs : UniqueDiffOn 𝕜 s
h : ContDiffAt 𝕜 (↑n) f x
hx : x ∈ s
⊢ iteratedFDerivWithin 𝕜 n f s x = iteratedFDeriv 𝕜 n f x

Tactic:
by
  rw [← iteratedFDerivWithin_univ]
  rcases h.contDiffOn' le_rfl (by simp) with ⟨u, u_open, xu, hu⟩
  rw [← iteratedFDerivWithin_inter_open u_open xu,
    ← iteratedFDerivWithin_inter_open u_open xu (s := univ)]
  apply iteratedFDerivWithin_subset
  · exact inter_subset_inter_left _ (subset_univ _)
  · exact hs.inter u_open
  · apply uniqueDiffOn_univ.inter u_open
  · simpa using hu
  · exact ⟨hx, xu⟩

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case emb
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n✝ : ℕ
c✝ : OrderedFinpartition n✝
n : ℕ
c : OrderedFinpartition n
o : Option (Fin c.length)
i : Fin c.length
⊢ { length := (c.extendMiddle i).length,
        partSize :=
          update (c.extendMiddle i).partSize ((c.extendMiddle i).index 0)
            ((c.extendMiddle i).partSize ((c.extendMiddle i).index 0) - 1),
        partSize_pos := ⋯,
        emb := fun i_1 j ↦
          if h : i_1 = i then ((c.extendMiddle i).emb i_1 (Fin.cast ⋯ j.succ)).pred ⋯
          else ((c.extendMiddle i).emb i_1 (Fin.cast ⋯ j)).pred ⋯,
        emb_strictMono := ⋯, parts_strictMono := ⋯, disjoint := ⋯, cover := ⋯ }.emb ≍
    c.emb

Tactic:
refine HEq.symm (hfunext rfl ?_)
        simp only [heq_eq_eq, forall_eq']
        intro a
        rcases eq_or_ne a i with rfl | hij
        · refine (Fin.heq_fun_iff ?_).mpr ?_
          · rw [index_extendMiddle_zero]
            simp [extendMiddle]
          · simp [extendMiddle]
        · refine (Fin.heq_fun_iff ?_).mpr ?_
          · rw [index_extendMiddle_zero]
            simp [extendMiddle]
          · simp [extendMiddle, hij]

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : DivisionRing 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
x : 𝔸
n : ℕ
⊢ (↑n !)⁻¹ • x ^ n = (↑n !)⁻¹ • x ^ n

Tactic:
inv_natCast_smul_eq 𝕂 𝔸

Goal state after:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : DivisionRing 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
x : 𝔸
n : ℕ
⊢ (↑n !)⁻¹ • x ^ n = (↑n !)⁻¹ • x ^ n
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
h : 0 < (expSeries 𝕂 𝔸).radius
⊢ HasFPowerSeriesAt exp (expSeries 𝕂 𝔸) 0

Tactic:
by
  simpa only [exp, expSeries_sum_eq_rat] using
    (hasFPowerSeriesOnBall_exp_of_radius_pos h).hasFPowerSeriesAt

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.Operations

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
s : Set E
ι : Type u_3
inst✝² : Fintype ι
F' : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
Φ : E → (i : ι) → F' i
P' : E → FormalMultilinearSeries 𝕜 E ((i : ι) → F' i)
n : ℕ∞ω
⊢ HasFTaylorSeriesUpToOn n Φ P' s ↔
    ∀ (i : ι),
      HasFTaylorSeriesUpToOn n (fun x ↦ Φ x i)
        (fun x m ↦ (ContinuousLinearMap.proj i).compContinuousMultilinearMap (P' x m)) s

Tactic:
convert! hasFTaylorSeriesUpToOn_pi (𝕜 := 𝕜) (φ := fun i x ↦ Φ x i)

Goal state after:
case e'_1.e
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
s : Set E
ι : Type u_3
inst✝² : Fintype ι
F' : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
Φ : E → (i : ι) → F' i
P' : E → FormalMultilinearSeries 𝕜 E ((i : ι) → F' i)
n : ℕ∞ω
⊢ HasFTaylorSeriesUpToOn n Φ P' =
    HasFTaylorSeriesUpToOn n (fun x i ↦ Φ x i) fun x m ↦
      ContinuousMultilinearMap.pi fun i ↦ (ContinuousLinearMap.proj i).compContinuousMultilinearMap (P' x m)
Module: Mathlib.Analysis.SpecialFunctions.Exponential

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : CharZero 𝕂
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
t : 𝕂
htx : t • x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
⊢ HasStrictDerivAt (fun u ↦ exp (u • x)) (exp (t • x) * x) t

Tactic:
simpa using (hasStrictFDerivAt_exp_smul_const_of_mem_ball 𝕂 x t htx).hasStrictDerivAt

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case zero_eq
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : WithTop ℕ∞
g : F → G
f : E → F
hg : HasFTaylorSeriesUpToOn n g q t
hf : HasFTaylorSeriesUpToOn n f p s
h : MapsTo f s t
⊢ ∀ x ∈ s, ((q (f x)).taylorComp (p x) 0).curry0 = (g ∘ f) x

Tactic:
intro x hx

Goal state after:
case zero_eq
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : WithTop ℕ∞
g : F → G
f : E → F
hg : HasFTaylorSeriesUpToOn n g q t
hf : HasFTaylorSeriesUpToOn n f p s
h : MapsTo f s t
x : E
hx : x ∈ s
⊢ ((q (f x)).taylorComp (p x) 0).curry0 = (g ∘ f) x
Module: Mathlib.Topology.ExtendFrom

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : RegularSpace Y
f : X → Y
A B : Set X
hB : B ⊆ closure[inst✝²] A
hf : ∀ x ∈ B, ∃ y, Tendsto f (𝓝[A] x) (𝓝 y)
⊢ ContinuousOn (extendFrom A f) B

Tactic:
set φ := extendFrom A f
  intro x x_in
  suffices ∀ V' ∈ 𝓝 (φ x), IsClosed V' → φ ⁻¹' V' ∈ 𝓝[B] x by
    simpa [ContinuousWithinAt, (closed_nhds_basis (φ x)).tendsto_right_iff]
  intro V' V'_in V'_closed
  obtain ⟨V, V_in, V_op, hV⟩ : ∃ V ∈ 𝓝 x, IsOpen V ∧ V ∩ A ⊆ f ⁻¹' V' := by
    have := tendsto_extendFrom (hf x x_in)
    rcases (nhdsWithin_basis_open x A).tendsto_left_iff.mp this V' V'_in with ⟨V, ⟨hxV, V_op⟩, hV⟩
    exact ⟨V, IsOpen.mem_nhds V_op hxV, V_op, hV⟩
  suffices ∀ y ∈ V ∩ B, φ y ∈ V' from
    mem_of_superset (inter_mem_inf V_in <| mem_principal_self B) this
  rintro y ⟨hyV, hyB⟩
  have := mem_closure_iff_nhdsWithin_neBot.mp (hB hyB)
  have limy : Tendsto f (𝓝[A] y) (𝓝 <| φ y) := tendsto_extendFrom (hf y hyB)
  have hVy : V ∈ 𝓝 y := IsOpen.mem_nhds V_op hyV
  have : V ∩ A ∈ 𝓝[A] y := by simpa only [inter_comm] using inter_mem_nhdsWithin A hVy
  exact V'_closed.mem_of_tendsto limy (mem_of_superset this hV)

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.Operations

Goal state before:
pp: case h.refine_3
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type uF
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
n✝ : ℕ∞ω
inst✝ : CompleteSpace E
f : OpenPartialHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑f.symm a)
n : ℕ
IH : ContDiffAt 𝕜 (↑↑n) (↑f) (↑f.symm a) → ContDiffAt 𝕜 (↑↑n) (↑f.symm) a
hf : ContDiffAt 𝕜 (↑↑n.succ) (↑f) (↑f.symm a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑f.symm a)
u : Set E
hu : u ∈ 𝓝 (↑f.symm a)
hff' : ∀ x ∈ u, HasFDerivAt (↑f) (f' x) x
eq_f₀' : f' (↑f.symm a) = ↑f₀'
h_nhds : {y | ∃ e, ↑e = f' y} ∈ 𝓝 (↑f.symm a)
t : Set E
htu : t ⊆ u ∩ {y | ∃ e, ↑e = f' y}
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
htf : ↑f.symm a ∈ t
⊢ ∀ x ∈ f.target ∩ ↑f.symm ⁻¹' t, HasFDerivAt (↑f.symm) ((inverse ∘ f' ∘ ↑f.symm) x) x

Tactic:
intro x hx

Goal state after:
case h.refine_3
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type uF
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
n✝ : ℕ∞ω
inst✝ : CompleteSpace E
f : OpenPartialHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑f.symm a)
n : ℕ
IH : ContDiffAt 𝕜 (↑↑n) (↑f) (↑f.symm a) → ContDiffAt 𝕜 (↑↑n) (↑f.symm) a
hf : ContDiffAt 𝕜 (↑↑n.succ) (↑f) (↑f.symm a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑f.symm a)
u : Set E
hu : u ∈ 𝓝 (↑f.symm a)
hff' : ∀ x ∈ u, HasFDerivAt (↑f) (f' x) x
eq_f₀' : f' (↑f.symm a) = ↑f₀'
h_nhds : {y | ∃ e, ↑e = f' y} ∈ 𝓝 (↑f.symm a)
t : Set E
htu : t ⊆ u ∩ {y | ∃ e, ↑e = f' y}
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
htf : ↑f.symm a ∈ t
x : F
hx : x ∈ f.target ∩ ↑f.symm ⁻¹' t
⊢ HasFDerivAt (↑f.symm) ((inverse ∘ f' ∘ ↑f.symm) x) x
Module: Mathlib.Analysis.Calculus.Deriv.MeanValue

Goal state before:
pp: f f' : ℝ → ℝ
a b : ℝ
hab : a < b
g g' : ℝ → ℝ
lfa lga lfb lgb : ℝ
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[>] a) (𝓝 lfa)
hga : Tendsto g (𝓝[>] a) (𝓝 lga)
hfb : Tendsto f (𝓝[<] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[<] b) (𝓝 lgb)
h : ℝ → ℝ := fun x ↦ (lgb - lga) * f x - (lfb - lfa) * g x
hha : Tendsto h (𝓝[>] a) (𝓝 (lgb * lfa - lfb * lga))
hhb : Tendsto h (𝓝[<] b) (𝓝 (lgb * lfa - lfb * lga))
h' : ℝ → ℝ := fun x ↦ (lgb - lga) * f' x - (lfb - lfa) * g' x
⊢ ∀ x ∈ Ioo a b, HasDerivAt h (h' x) x

Tactic:
intro x hx

Goal state after:
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
g g' : ℝ → ℝ
lfa lga lfb lgb : ℝ
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[>] a) (𝓝 lfa)
hga : Tendsto g (𝓝[>] a) (𝓝 lga)
hfb : Tendsto f (𝓝[<] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[<] b) (𝓝 lgb)
h : ℝ → ℝ := fun x ↦ (lgb - lga) * f x - (lfb - lfa) * g x
hha : Tendsto h (𝓝[>] a) (𝓝 (lgb * lfa - lfb * lga))
hhb : Tendsto h (𝓝[<] b) (𝓝 (lgb * lfa - lfb * lga))
h' : ℝ → ℝ := fun x ↦ (lgb - lga) * f' x - (lfb - lfa) * g' x
x : ℝ
hx : x ∈ Ioo a b
⊢ HasDerivAt h (h' x) x