mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: case cont
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (E i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
⊢ ∀ (m : ℕ), ↑m ≤ ⊤ → Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun x ↦ f.iteratedFDeriv m x

Tactic:
rintro n -

Goal state after:
case cont
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (E i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
n : ℕ
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun x ↦ f.iteratedFDeriv n x
Module: Mathlib.Analysis.Analytic.Uniqueness

Goal state before:
pp: 𝕜 : 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
f : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfz₀ : f =ᶠ[𝓝 z₀] 0
F' : Type u_3 := UniformSpace.Completion F
e : F →L[𝕜] F' := UniformSpace.Completion.toComplL
⊢ EqOn f 0 U

Tactic:
have : AnalyticOnNhd 𝕜 (e ∘ f) U := fun x hx => (e.analyticAt _).comp (hf x hx)

Goal state after:
𝕜 : 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
f : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfz₀ : f =ᶠ[𝓝 z₀] 0
F' : Type u_3 := UniformSpace.Completion F
e : F →L[𝕜] F' := UniformSpace.Completion.toComplL
this : AnalyticOnNhd 𝕜 (⇑e ∘ f) U
⊢ EqOn f 0 U
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
r : ℝ≥0∞
h : HasFPowerSeriesOnBall f p x r
y : E
inst✝ : CompleteSpace F
n : ℕ
⊢ (n ! • (p n) fun x ↦ y) = (iteratedFDeriv 𝕜 n f x) fun x ↦ y

Tactic:
cases n
  · rw [factorial_zero, one_smul, h.iteratedFDeriv_zero_apply_diag]
  · rw [factorial_succ, mul_comm, mul_smul, ← derivSeries_apply_diag,
      ← _root_.smul_apply, factorial_smul' _ h.fderiv, iteratedFDeriv_succ_apply_right]
    rfl

Goal state after:
Module: Mathlib.Analysis.Calculus.Deriv.Slope

Goal state before:
pp: 𝕜 : Type u
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : DecidableEq 𝕜
f : 𝕜 → 𝕜
c a : 𝕜
hf : HasDerivAt f a c
⊢ ContinuousAt (Function.update (fun x ↦ (f x - f c) / (x - c)) c a) c

Tactic:
by
  rw [← slope_fun_def_field]
  exact continuousAt_update_same.mpr <| hasDerivAt_iff_tendsto_slope.mp hf

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸' : Type u_7
inst✝³ : NormedCommRing 𝔸'
inst✝² : NormedAlgebra 𝕜 𝔸'
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
l : List ι
x : ι → 𝔸'
this : Fintype ι
⊢ HasStrictFDerivAt (fun x ↦ (List.map x l).prod) (List.map (fun i ↦ (List.map x (l.erase i)).prod •> proj i) l).sum x

Tactic:
refine hasStrictFDerivAt_list_prod'.congr_fderiv ?_

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸' : Type u_7
inst✝³ : NormedCommRing 𝔸'
inst✝² : NormedAlgebra 𝕜 𝔸'
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
l : List ι
x : ι → 𝔸'
this : Fintype ι
⊢ ∑ i, (List.map x (List.take (↑i) l)).prod •> (proj l[i] <• (List.map x (List.drop (↑i).succ l)).prod) =
    (List.map (fun i ↦ (List.map x (l.erase i)).prod •> proj i) l).sum
Module: Mathlib.Analysis.Calculus.Deriv.Comp

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
s' : Set 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
y : 𝕜'
hh₂ : DifferentiableWithinAt 𝕜' h₂ s' y
hh : DifferentiableWithinAt 𝕜 h s x
hs : MapsTo h s s'
hy : h x = y
⊢ derivWithin (h₂ ∘ h) s x = derivWithin h₂ s' (h x) * derivWithin h s x

Tactic:
subst hy

Goal state after:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
s' : Set 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
hh : DifferentiableWithinAt 𝕜 h s x
hs : MapsTo h s s'
hh₂ : DifferentiableWithinAt 𝕜' h₂ s' (h x)
⊢ derivWithin (h₂ ∘ h) s x = derivWithin h₂ s' (h x) * derivWithin h s x
Module: Mathlib.Analysis.Calculus.Deriv.Comp

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
y : 𝕜'
hh₂ : DifferentiableAt 𝕜' h₂ y
hh : DifferentiableAt 𝕜 h x
hy : h x = y
⊢ deriv (h₂ ∘ h) x = deriv h₂ (h x) * deriv h x

Tactic:
subst hy

Goal state after:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
hh : DifferentiableAt 𝕜 h x
hh₂ : DifferentiableAt 𝕜' h₂ (h x)
⊢ deriv (h₂ ∘ h) x = deriv h₂ (h x) * deriv h x
Module: Mathlib.Analysis.Calculus.LogDeriv

Goal state before:
pp: case inr.inr
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hdf : DifferentiableAt 𝕜 f x
n : ℤ
hn : n ≠ 0
hf : f x ≠ 0
⊢ deriv (fun x ↦ f x ^ n) x / f x ^ n = ↑n * logDeriv f x

Tactic:
← comp_def (· ^ n),

Goal state after:
case inr.inr
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hdf : DifferentiableAt 𝕜 f x
n : ℤ
hn : n ≠ 0
hf : f x ≠ 0
⊢ deriv ((fun x ↦ x ^ n) ∘ f) x / f x ^ n = ↑n * logDeriv f x
Module: Mathlib.Analysis.Calculus.LogDeriv

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NontriviallyNormedField 𝕜'
inst✝¹ : NormedAlgebra 𝕜 𝕜'
inst✝ : IsRCLikeNormedField 𝕜
f g : 𝕜 → 𝕜'
s : Set 𝕜
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hs2 : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hsc : IsPreconnected s
hgn : ∀ x ∈ s, g x ≠ 0
hfn : ∀ x ∈ s, f x ≠ 0
⊢ EqOn (logDeriv f) (logDeriv g) s ↔ ∃ z, z ≠ 0 ∧ EqOn f (z • g) s

Tactic:
by
  rcases s.eq_empty_or_nonempty with rfl | ⟨t, ht⟩
  · simpa using ⟨1, one_ne_zero⟩
  · constructor
    · refine fun h ↦ ⟨f t * (g t)⁻¹, by grind, fun y hy ↦ ?_⟩
      have hderiv : s.EqOn (deriv (f * g⁻¹)) (deriv f * g⁻¹ - f * deriv g / g ^ 2) := by
        intro z hz
        rw [deriv_mul (hf.differentiableAt (hs2.mem_nhds hz)) ((hg.differentiableAt
          (hs2.mem_nhds hz)).inv (hgn z hz))]
        simp only [Pi.inv_apply, show g⁻¹ = (fun x => x⁻¹) ∘ g by rfl, deriv_inv, neg_mul,
          deriv_comp z (differentiableAt_inv (hgn z hz)) (hg.differentiableAt (hs2.mem_nhds hz)),
          mul_neg, Pi.sub_apply, Pi.mul_apply, comp_apply, Pi.div_apply, Pi.pow_apply]
        ring
      have hfg : EqOn (deriv (f * g⁻¹)) 0 s := hderiv.trans fun z hz ↦ by
        simp only [Pi.sub_apply, Pi.mul_apply, Pi.inv_apply, Pi.div_apply, Pi.pow_apply,
          Pi.zero_apply]
        grind [logDeriv_apply, Pi.div_apply]
      let := IsRCLikeNormedField.rclike 𝕜
      obtain ⟨a, ha⟩ := hs2.exists_is_const_of_deriv_eq_zero hsc (hf.mul (hg.inv hgn)) hfg
      grind [Pi.mul_apply, Pi.inv_apply, Pi.smul_apply, smul_eq_mul]
    · rintro ⟨z, hz0, hz⟩ x hx
      simp [logDeriv_apply, hz.deriv hs2 hx, hz hx, deriv_const_smul _
        (hg.differentiableAt (hs2.mem_nhds hx)), mul_div_mul_left (deriv g x) (g x) hz0]

Goal state after:
Module: Mathlib.Analysis.Calculus.MeanValue

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b C : ℝ
hf : DifferentiableOn ℝ f (Icc a b)
bound : ∀ x ∈ Ico a b, ‖derivWithin f (Icc a b) x‖ ≤ C
⊢ ∀ x ∈ Icc a b, HasDerivWithinAt f (derivWithin f (Icc a b) x) (Icc a b) x

Tactic:
exact fun x hx => (hf x hx).hasDerivWithinAt

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

Goal state before:
pp: case succ
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
i : ℕ
⊢ iteratedFDerivWithin 𝕜 (i + 1) 0 s = 0

Tactic:
apply iteratedFDerivWithin_succ_const

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
n : ℕ∞ω
s : Set E
t : Set F
g : F → G
f : E → F
y : F
x : E
hg : ContDiffWithinAt 𝕜 n g t y
hf : ContDiffWithinAt 𝕜 n f s x
st : MapsTo f s t
hy : f x = y
⊢ ContDiffWithinAt 𝕜 n (g ∘ f) s x

Tactic:
subst hy

Goal state after:
𝕜 : 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
n : ℕ∞ω
s : Set E
t : Set F
g : F → G
f : E → F
x : E
hf : ContDiffWithinAt 𝕜 n f s x
st : MapsTo f s t
hg : ContDiffWithinAt 𝕜 n g t (f x)
⊢ ContDiffWithinAt 𝕜 n (g ∘ f) s x
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
n : ℕ∞ω
s : Set E
t : Set F
g : F → G
f : E → F
y : F
x : E
hg : ContDiffWithinAt 𝕜 n g t y
hf : ContDiffWithinAt 𝕜 n f s x
hs : t ∈ 𝓝[f '' s] f x
hy : f x = y
⊢ ContDiffWithinAt 𝕜 n (g ∘ f) s x

Tactic:
subst hy

Goal state after:
𝕜 : 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
n : ℕ∞ω
s : Set E
t : Set F
g : F → G
f : E → F
x : E
hf : ContDiffWithinAt 𝕜 n f s x
hs : t ∈ 𝓝[f '' s] f x
hg : ContDiffWithinAt 𝕜 n g t (f x)
⊢ ContDiffWithinAt 𝕜 n (g ∘ f) s x
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
n : ℕ∞ω
s : Set E
t : Set F
g : F → G
f : E → F
y : F
x : E
hg : ContDiffWithinAt 𝕜 n g t y
hf : ContDiffWithinAt 𝕜 n f s x
hy : f x = y
⊢ ContDiffWithinAt 𝕜 n (g ∘ f) (s ∩ f ⁻¹' t) x

Tactic:
subst hy

Goal state after:
𝕜 : 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
n : ℕ∞ω
s : Set E
t : Set F
g : F → G
f : E → F
x : E
hf : ContDiffWithinAt 𝕜 n f s x
hg : ContDiffWithinAt 𝕜 n g t (f x)
⊢ ContDiffWithinAt 𝕜 n (g ∘ f) (s ∩ f ⁻¹' t) x
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
n : ℕ∞ω
s : Set E
t : Set F
g : F → G
f : E → F
y : F
x : E
hg : ContDiffWithinAt 𝕜 n g t y
hf : ContDiffWithinAt 𝕜 n f s x
hs : f ⁻¹' t ∈ 𝓝[s] x
hy : f x = y
⊢ ContDiffWithinAt 𝕜 n (g ∘ f) s x

Tactic:
subst hy

Goal state after:
𝕜 : 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
n : ℕ∞ω
s : Set E
t : Set F
g : F → G
f : E → F
x : E
hf : ContDiffWithinAt 𝕜 n f s x
hs : f ⁻¹' t ∈ 𝓝[s] x
hg : ContDiffWithinAt 𝕜 n g t (f x)
⊢ ContDiffWithinAt 𝕜 n (g ∘ f) s x
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
f : E → F
g : F → G
n : ℕ∞ω
y : F
x : E
hg : ContDiffAt 𝕜 n g y
hf : ContDiffWithinAt 𝕜 n f s x
hy : f x = y
⊢ ContDiffWithinAt 𝕜 n (g ∘ f) s x

Tactic:
subst hy

Goal state after:
𝕜 : 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
g : F → G
n : ℕ∞ω
x : E
hf : ContDiffWithinAt 𝕜 n f s x
hg : ContDiffAt 𝕜 n g (f x)
⊢ ContDiffWithinAt 𝕜 n (g ∘ 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
x : E
inst✝ : CompleteSpace F
⊢ ContDiffWithinAt 𝕜 ω f s x ↔ AnalyticWithinAt 𝕜 f s x

Tactic:
refine ⟨fun h ↦ h.analyticWithinAt, fun h ↦ ?_⟩
  obtain ⟨u, hu, p, hp, h'p⟩ := h.exists_hasFTaylorSeriesUpToOn ω
  exact ⟨u, hu, p, hp.of_le le_top, fun i ↦ h'p i⟩

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 : 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

Tactic:
obtain ⟨w, hw, hxw, hwu⟩ := mem_nhdsWithin.mp hu

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
w : Set E
hw : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] w
hxw : x ∈ w
hwu : w ∩ insert x s ⊆ u
⊢ ∃ 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.Topology.OpenPartialHomeomorph.IsImage

Goal state before:
pp: case right
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e e' : OpenPartialHomeomorph X Y
h : EqOn (↑e) (↑e') (e.source ∩ e'.source)
⊢ EqOn (↑(e.restr e'.source)) (↑(e'.restr e.source)) (e.restr e'.source).source

Tactic:
rw [e.restr_source' _ e'.open_source]
    refine (EqOn.trans ?_ h).trans ?_ <;> simp only [mfld_simps, eqOn_refl]

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

Goal state before:
pp: 𝕜 : 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✝ c : OrderedFinpartition n
m : Fin c.length
this : ∀ (a' b' : Fin (c.partSize m + 1)), a' < b' → cases 0 (succ ∘ c.emb m) a' < cases 0 (succ ∘ c.emb m) b'
a : Fin (update c.partSize m (c.partSize m + 1) m)
⊢ ∀ ⦃b : Fin (update c.partSize m (c.partSize m + 1) m)⦄,
    a < b →
      ((fun i ↦ cases 0 (succ ∘ c.emb m) i) ∘ Fin.cast ⋯) a < ((fun i ↦ cases 0 (succ ∘ c.emb m) i) ∘ Fin.cast ⋯) b

Tactic:
b

Goal state after:
𝕜 : 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✝ c : OrderedFinpartition n
m : Fin c.length
this : ∀ (a' b' : Fin (c.partSize m + 1)), a' < b' → cases 0 (succ ∘ c.emb m) a' < cases 0 (succ ∘ c.emb m) b'
a b : Fin (update c.partSize m (c.partSize m + 1) m)
⊢ a < b → ((fun i ↦ cases 0 (succ ∘ c.emb m) i) ∘ Fin.cast ⋯) a < ((fun i ↦ cases 0 (succ ∘ c.emb m) i) ∘ Fin.cast ⋯) b
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: 𝕜 : 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✝ c : OrderedFinpartition n
m : Fin c.length
this : ∀ (a' b' : Fin (c.partSize m + 1)), a' < b' → cases 0 (succ ∘ c.emb m) a' < cases 0 (succ ∘ c.emb m) b'
a b : Fin (update c.partSize m (c.partSize m + 1) m)
hab : a < b
⊢ ((fun i ↦ cases 0 (succ ∘ c.emb m) i) ∘ Fin.cast ⋯) a < ((fun i ↦ cases 0 (succ ∘ c.emb m) i) ∘ Fin.cast ⋯) b

Tactic:
exact this _ _ hab

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

Goal state before:
pp: 𝕜 : 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✝ c : OrderedFinpartition n
i : Fin c.length
hi : i ∈ univ
j : Fin c.length
hj : j ∈ univ
hij h : i ≠ j
this : ∀ (a' : Fin (c.partSize i)) (b' : Fin (c.partSize j + 1)), (c.emb i a').succ ≠ cases 0 (succ ∘ c.emb j) b'
a : Fin (update c.partSize j (c.partSize j + 1) i)
⊢ ∀ (a_1 : Fin (update c.partSize j (c.partSize j + 1) j)),
    ¬(c.emb i (Fin.cast ⋯ a)).succ = cases 0 (succ ∘ c.emb j) (Fin.cast ⋯ a_1)

Tactic:
b

Goal state after:
𝕜 : 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✝ c : OrderedFinpartition n
i : Fin c.length
hi : i ∈ univ
j : Fin c.length
hj : j ∈ univ
hij h : i ≠ j
this : ∀ (a' : Fin (c.partSize i)) (b' : Fin (c.partSize j + 1)), (c.emb i a').succ ≠ cases 0 (succ ∘ c.emb j) b'
a : Fin (update c.partSize j (c.partSize j + 1) i)
b : Fin (update c.partSize j (c.partSize j + 1) j)
⊢ ¬(c.emb i (Fin.cast ⋯ a)).succ = cases 0 (succ ∘ c.emb j) (Fin.cast ⋯ b)
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 : E
hx : x ∈ s
⊢ ∃ t,
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧
      x ∈ t ∧ ContinuousOn (fun x ↦ ftaylorSeriesWithin 𝕜 f s x m) (s ∩ t)

Tactic:
rcases (h x hx).of_le hm _ le_rfl with ⟨u, hu, p, Hp⟩

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
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑m) f p u
⊢ ∃ t,
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧
      x ∈ t ∧ ContinuousOn (fun x ↦ ftaylorSeriesWithin 𝕜 f s x m) (s ∩ t)
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case inr
𝕜 : 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✝ c : OrderedFinpartition n
k i : Fin c.length
hi : i ∈ univ
j : Fin c.length
hj✝ : j ∈ univ
hij : i ≠ j
h : i ≠ k
hj : j ≠ k
a : Fin (update c.partSize k (c.partSize k + 1) i)
⊢ ∀ (a_1 : Fin (update c.partSize k (c.partSize k + 1) j)), ¬c.emb i (Fin.cast ⋯ a) = c.emb j (Fin.cast ⋯ a_1)

Tactic:
b

Goal state after:
case inr
𝕜 : 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✝ c : OrderedFinpartition n
k i : Fin c.length
hi : i ∈ univ
j : Fin c.length
hj✝ : j ∈ univ
hij : i ≠ j
h : i ≠ k
hj : j ≠ k
a : Fin (update c.partSize k (c.partSize k + 1) i)
b : Fin (update c.partSize k (c.partSize k + 1) j)
⊢ ¬c.emb i (Fin.cast ⋯ a) = c.emb j (Fin.cast ⋯ b)
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case inl
n : ℕ
c : OrderedFinpartition n
j : Fin c.length
h : range ((c.extendMiddle j).emb j) = {0}
this : (c.emb j 0).succ ∈ {0}
⊢ False

Tactic:
simp only [mem_singleton_iff] at this

Goal state after:
case inl
n : ℕ
c : OrderedFinpartition n
j : Fin c.length
h : range ((c.extendMiddle j).emb j) = {0}
this : (c.emb j 0).succ = 0
⊢ False
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: 𝕜 : 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
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) = {0}
i : Fin (c.length - 1)
x✝¹ : i ∈ univ
j : Fin (c.length - 1)
x✝ : j ∈ univ
hij : i ≠ j
a : Fin (c.partSize (Fin.cast ⋯ i.succ))
⊢ ∀ (a_1 : Fin (c.partSize (Fin.cast ⋯ j.succ))), ¬c.emb (Fin.cast ⋯ i.succ) a = c.emb (Fin.cast ⋯ j.succ) a_1

Tactic:
b

Goal state after:
𝕜 : 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
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) = {0}
i : Fin (c.length - 1)
x✝¹ : i ∈ univ
j : Fin (c.length - 1)
x✝ : j ∈ univ
hij : i ≠ j
a : Fin (c.partSize (Fin.cast ⋯ i.succ))
b : Fin (c.partSize (Fin.cast ⋯ j.succ))
⊢ ¬c.emb (Fin.cast ⋯ i.succ) a = c.emb (Fin.cast ⋯ j.succ) b