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

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
G' : Type u_5
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
B : E →L[𝕜] F →L[𝕜] G
f : G' → E
g : G' → F
f' : G' →L[𝕜] E
g' : G' →L[𝕜] F
x : G'
hf : HasFDerivAt f f' x
hg : HasFDerivAt g g' x
⊢ HasFDerivAt (fun y ↦ (B (f y)) (g y)) (((precompR G' B) (f x)) g' + ((precompL G' B) f') (g x)) x

Tactic:
by
  -- need `by exact` to deal with tricky unification
  exact (B.isBoundedBilinearMap.hasFDerivAt (f x, g x)).comp x (hf.prodMk hg)

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

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
iso : E ≃L[𝕜] F
f : G → E
s : Set G
x : G
H : DifferentiableWithinAt 𝕜 (⇑iso ∘ f) s x
this : DifferentiableWithinAt 𝕜 (⇑iso.symm ∘ ⇑iso ∘ f) s x
⊢ DifferentiableWithinAt 𝕜 f s x

Tactic:
← Function.comp_assoc iso.symm iso f,

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
iso : E ≃L[𝕜] F
f : G → E
s : Set G
x : G
H : DifferentiableWithinAt 𝕜 (⇑iso ∘ f) s x
this : DifferentiableWithinAt 𝕜 ((⇑iso.symm ∘ ⇑iso) ∘ f) s x
⊢ DifferentiableWithinAt 𝕜 f s x
Module: Mathlib.Analysis.Calculus.FDeriv.Add

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
x : E
s : Set E
c : F
⊢ fderivWithin 𝕜 (fun y ↦ c + f y) s x = fderivWithin 𝕜 f s x

Tactic:
by
  simpa only [add_comm] using fderivWithin_add_const c

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Alternating.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_4
ι : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : TopologicalSpace M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : TopologicalSpace N
f g : M [⋀^ι]→L[R] N
h : f.toAlternatingMap = g.toAlternatingMap
⊢ ⇑f = ⇑g

Tactic:
convert! DFunLike.ext'_iff.1 h

Goal state after:
Module: Mathlib.Topology.MetricSpace.Completion

Goal state before:
pp: case ih
α : Type u
β : Type v
inst✝⁵ : PseudoMetricSpace α
M : Type u_1
inst✝⁴ : Zero M
inst✝³ : Zero α
inst✝² : SMul M α
inst✝¹ : PseudoMetricSpace M
inst✝ : IsBoundedSMul M α
c₁ c₂ : M
x : α
⊢ dist (c₁ • ↑x) (c₂ • ↑x) ≤ dist c₁ c₂ * dist (↑x) 0

Tactic:
| ih x =>

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

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 : ℕ∞ω
p q : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn n f p s
hpq : ∀ (m : ℕ), ↑m ≤ n → EqOn (fun x ↦ p x m) (fun x ↦ q x m) s
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
⊢ HasFDerivWithinAt (fun x ↦ q x m) (q x m.succ).curryLeft s x

Tactic:
by
    refine ((hp.fderivWithin m hm x hx).congr' (hpq m hm.le).symm hx).congr_fderiv ?_
    refine congrArg _ (hpq (m + 1) ?_ hx)
    exact ENat.add_one_natCast_le_withTop_of_lt hm

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

Goal state before:
pp: case mpr
𝕜 : 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 : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
hN : ∞ ≤ N
k : ℕ
⊢ (∀ (n : ℕ), HasFTaylorSeriesUpToOn (↑(n + k)) f p s) → HasFTaylorSeriesUpToOn N f p s

Tactic:
· intro H
    constructor
    · exact (H 0).zero_eq
    · intro m _
      apply (H m.succ).fderivWithin m (by norm_cast; lia)
    · intro m _
      apply (H m).cont m (by simp)

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

Goal state before:
pp: case fderivWithin
𝕜 : 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
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ x ∈ s, (p x 0).curry0 = f x
Hfderiv_zero : ∀ x ∈ s, HasFDerivWithinAt (fun y ↦ p y 0) (p x 1).curryLeft s x
Htaylor : HasFTaylorSeriesUpToOn (↑n) (fun x ↦ (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) (fun x ↦ (p x).shift) s
m : ℕ
hm : ↑m < ↑n.succ
x : E
hx : x ∈ s
⊢ HasFDerivWithinAt (fun x ↦ p x m) (p x m.succ).curryLeft s x

Tactic:
rcases m with - | m

Goal state after:
case fderivWithin.zero
𝕜 : 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
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ x ∈ s, (p x 0).curry0 = f x
Hfderiv_zero : ∀ x ∈ s, HasFDerivWithinAt (fun y ↦ p y 0) (p x 1).curryLeft s x
Htaylor : HasFTaylorSeriesUpToOn (↑n) (fun x ↦ (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) (fun x ↦ (p x).shift) s
x : E
hx : x ∈ s
hm : ↑0 < ↑n.succ
⊢ HasFDerivWithinAt (fun x ↦ p x 0) (p x (Nat.succ 0)).curryLeft s x

case fderivWithin.succ
𝕜 : 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
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ x ∈ s, (p x 0).curry0 = f x
Hfderiv_zero : ∀ x ∈ s, HasFDerivWithinAt (fun y ↦ p y 0) (p x 1).curryLeft s x
Htaylor : HasFTaylorSeriesUpToOn (↑n) (fun x ↦ (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) (fun x ↦ (p x).shift) s
x : E
hx : x ∈ s
m : ℕ
hm : ↑(m + 1) < ↑n.succ
⊢ HasFDerivWithinAt (fun x ↦ p x (m + 1)) (p x (m + 1).succ).curryLeft s x
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: case mpr.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
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ x ∈ s, (p x 0).curry0 = f x
Hfderiv_zero : ∀ x ∈ s, HasFDerivWithinAt (fun y ↦ p y 0) (p x 1).curryLeft s x
Htaylor : HasFTaylorSeriesUpToOn (↑n) (fun x ↦ (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) (fun x ↦ (p x).shift) s
m : ℕ
hm : ↑m ≤ ↑n.succ
⊢ ContinuousOn (fun x ↦ p x m) s

Tactic:
rcases m with - | m

Goal state after:
case mpr.cont.zero
𝕜 : 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
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ x ∈ s, (p x 0).curry0 = f x
Hfderiv_zero : ∀ x ∈ s, HasFDerivWithinAt (fun y ↦ p y 0) (p x 1).curryLeft s x
Htaylor : HasFTaylorSeriesUpToOn (↑n) (fun x ↦ (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) (fun x ↦ (p x).shift) s
hm : ↑0 ≤ ↑n.succ
⊢ ContinuousOn (fun x ↦ p x 0) s

case mpr.cont.succ
𝕜 : 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
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ x ∈ s, (p x 0).curry0 = f x
Hfderiv_zero : ∀ x ∈ s, HasFDerivWithinAt (fun y ↦ p y 0) (p x 1).curryLeft s x
Htaylor : HasFTaylorSeriesUpToOn (↑n) (fun x ↦ (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) (fun x ↦ (p x).shift) s
m : ℕ
hm : ↑(m + 1) ≤ ↑n.succ
⊢ ContinuousOn (fun x ↦ p x (m + 1)) s
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

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
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpTo n f p
x : E
⊢ p x 0 = (continuousMultilinearCurryFin0 𝕜 E F).symm (f x)

Tactic:
rw [← h.zero_eq x]
  exact (p x 0).uncurry0_curry0.symm

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

Goal state before:
pp: 𝕜 : Type u_1
𝔸 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
x : 𝔸
n : ℕ
⊢ fderiv 𝕜 (fun x ↦ x ^ n) x = ∑ i ∈ Finset.range n, x ^ (n.pred - i) •> ContinuousLinearMap.id 𝕜 𝔸 <• x ^ i

Tactic:
rw [fderiv_fun_pow' n differentiableAt_fun_id, fderiv_fun_id]

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

Goal state before:
pp: 𝕜 : Type u_1
𝔸 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
f : 𝕜 → 𝔸
x : 𝕜
s : Set 𝕜
h : DifferentiableWithinAt 𝕜 f s x
n : ℕ
⊢ derivWithin (fun x ↦ f x ^ n) s x = ∑ i ∈ Finset.range n, f x ^ (n.pred - i) * derivWithin f s x * f x ^ i

Tactic:
by_cases hsx : UniqueDiffWithinAt 𝕜 s x
  · exact (h.hasDerivWithinAt.pow' n).derivWithin hsx
  · simp [derivWithin_zero_of_not_uniqueDiffWithinAt hsx]

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

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_2
𝔸' : Type u_3
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
hd : ∀ i ∈ u, DifferentiableAt 𝕜 (f i) x
⊢ DifferentiableAt 𝕜 (fun x ↦ ∏ i ∈ u, f i x) x

Tactic:
exact
    (HasDerivAt.fun_finsetProd (fun i hi ↦ DifferentiableAt.hasDerivAt (hd i hi))).differentiableAt

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

Goal state before:
pp: 𝕜 : 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 ι
inst✝ : DecidableEq ι
fa : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)
⊢ HasStrictFDerivAt (fun fx ↦ fx.1 fx.2)
    (apply 𝕜 E F fa.2 ∘SL ContinuousLinearMap.fst 𝕜 (ContinuousMultilinearMap 𝕜 E F) ((i : ι) → E i) +
      fa.1.linearDeriv fa.2 ∘SL ContinuousLinearMap.snd 𝕜 (ContinuousMultilinearMap 𝕜 E F) ((i : ι) → E i))
    fa

Tactic:
let f := ContinuousLinearMap.id 𝕜 (ContinuousMultilinearMap 𝕜 E F)
    |>.continuousMultilinearMapOption

Goal state after:
𝕜 : 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 ι
inst✝ : DecidableEq ι
fa : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)
f : ContinuousMultilinearMap 𝕜 (fun x ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) F :=
  (ContinuousLinearMap.id 𝕜 (ContinuousMultilinearMap 𝕜 E F)).continuousMultilinearMapOption
⊢ HasStrictFDerivAt (fun fx ↦ fx.1 fx.2)
    (apply 𝕜 E F fa.2 ∘SL ContinuousLinearMap.fst 𝕜 (ContinuousMultilinearMap 𝕜 E F) ((i : ι) → E i) +
      fa.1.linearDeriv fa.2 ∘SL ContinuousLinearMap.snd 𝕜 (ContinuousMultilinearMap 𝕜 E F) ((i : ι) → E i))
    fa
Module: Mathlib.Analysis.Analytic.Uniqueness

Goal state before:
pp: case e'_5
𝕜 : 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
inst✝ : CompleteSpace F
f : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfz₀ : f =ᶠ[𝓝 z₀] 0
u : Set E := {x | f =ᶠ[𝓝 x] 0}
x : E
xu : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xU : x ∈ U
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p x r
y : E
yu : y ∈ u
hxy : edist x y < r / 2
q : FormalMultilinearSeries 𝕜 E F := p.changeOrigin (y - x)
has_series : HasFPowerSeriesOnBall f q y (r / 2)
M : Metric.eball y (r / 2) ∈ 𝓝 x
z : E
hz : z ∈ Metric.eball y (r / 2)
A : HasSum (fun n ↦ (q n) fun x ↦ z - y) (f z)
this : HasFPowerSeriesAt 0 q y
n : ℕ
⊢ ((q n) fun x ↦ z - y) = 0

Tactic:
exact this.apply_eq_zero n _

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

Goal state before:
pp: case succ
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
x : E
r : ℝ≥0∞
y : E
n : ℕ
ih :
  ∀ {F : Type (max u v)} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace 𝕜 F] [CompleteSpace F]
    {p : FormalMultilinearSeries 𝕜 E F} {f : E → F},
    HasFPowerSeriesOnBall f p x r → (n ! • (p n) fun x ↦ y) = (iteratedFDeriv 𝕜 n f x) fun x ↦ y
F : Type (max u v)
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
h : HasFPowerSeriesOnBall f p x r
⊢ ((n + 1)! • (p (n + 1)) fun x ↦ y) = (iteratedFDeriv 𝕜 (n + 1) f x) fun x ↦ y

Tactic:
rw [factorial_succ, mul_comm, mul_smul, ← derivSeries_apply_diag,
      ← _root_.smul_apply, ih h.fderiv, iteratedFDeriv_succ_apply_right]

Goal state after:
case succ
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
x : E
r : ℝ≥0∞
y : E
n : ℕ
ih :
  ∀ {F : Type (max u v)} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace 𝕜 F] [CompleteSpace F]
    {p : FormalMultilinearSeries 𝕜 E F} {f : E → F},
    HasFPowerSeriesOnBall f p x r → (n ! • (p n) fun x ↦ y) = (iteratedFDeriv 𝕜 n f x) fun x ↦ y
F : Type (max u v)
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
h : HasFPowerSeriesOnBall f p x r
⊢ ((iteratedFDeriv 𝕜 n (fderiv 𝕜 f) x) fun x ↦ y) y =
    ((iteratedFDeriv 𝕜 n (fun y ↦ fderiv 𝕜 f y) x) (Fin.init fun x ↦ y)) y
Module: Mathlib.Analysis.Calculus.Deriv.Slope

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
f' : E
s : Set ℝ
x r : ℝ
hf : HasDerivWithinAt f f' s x
hr : ‖f'‖ < r
hr₀ : 0 < r
A : ∀ᶠ (z : ℝ) in 𝓝[s \ {x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r
⊢ x ∈ {x_1 | (fun z ↦ ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r) x_1}

Tactic:
simp [hr₀]

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

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
f' : E
x r : ℝ
hf : HasDerivWithinAt f f' (Ici x) x
hr : ‖f'‖ < r
this : ∃ᶠ (x_1 : ℝ) in 𝓝[>] x, ‖x_1 - x‖⁻¹ * (‖f x_1‖ - ‖f x‖) < r
z : ℝ
hxz : x < z
hz : |z - x|⁻¹ * (‖f z‖ - ‖f x‖) < r
⊢ (z - x)⁻¹ * (‖f z‖ - ‖f x‖) < r

Tactic:
abs_of_pos (sub_pos_of_lt hxz)

Goal state after:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
f' : E
x r : ℝ
hf : HasDerivWithinAt f f' (Ici x) x
hr : ‖f'‖ < r
this : ∃ᶠ (x_1 : ℝ) in 𝓝[>] x, ‖x_1 - x‖⁻¹ * (‖f x_1‖ - ‖f x‖) < r
z : ℝ
hxz : x < z
hz : (z - x)⁻¹ * (‖f z‖ - ‖f x‖) < r
⊢ (z - x)⁻¹ * (‖f z‖ - ‖f x‖) < r
Module: Mathlib.Analysis.Calculus.FDeriv.Mul

Goal state before:
pp: case cons
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸 : Type u_6
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕜 𝔸
inst✝ : Finite ι
x : ι → 𝔸
this : Fintype ι
a : ι
l : List ι
IH :
  HasStrictFDerivAt (fun x ↦ (List.map x l).prod)
    (∑ i, (List.map x (List.take (↑i) l)).prod •> (proj l[i] <• (List.map x (List.drop (↑i).succ l)).prod)) x
⊢ HasStrictFDerivAt (fun x ↦ (proj a) x * (List.map x l).prod)
    (∑ i,
      (List.map x (List.take (↑i) (a :: l))).prod •>
        (proj (a :: l)[i] <• (List.map x (List.drop (↑i).succ (a :: l))).prod))
    x

Tactic:
exact .congr_fderiv (.mul' (ContinuousLinearMap.hasStrictFDerivAt _) IH)
      (by ext; simp [Fin.sum_univ_succ, Finset.mul_sum, mul_assoc, add_comm])

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
s : Set E
ι : Type u_5
𝔸' : Type u_7
inst✝² : NormedCommRing 𝔸'
inst✝¹ : NormedAlgebra 𝕜 𝔸'
g : ι → E → 𝔸'
g' : ι → E →L[𝕜] 𝔸'
inst✝ : DecidableEq ι
u : Multiset ι
x : E
h : ∀ i ∈ u, HasFDerivWithinAt (fun x ↦ g i x) (g' i) s x
⊢ HasFDerivWithinAt (fun x ↦ (Multiset.map (fun x_1 ↦ g x_1 x) u).prod)
    (Multiset.map (fun i ↦ (Multiset.map (fun x_1 ↦ g x_1 x) (u.erase i)).prod •> g' i) u).sum s x

Tactic:
simp only [← Multiset.attach_map_val u, Multiset.map_map]
  exact .congr_fderiv
    (hasFDerivAt_multiset_prod.comp_hasFDerivWithinAt x <|
      hasFDerivWithinAt_pi.mpr fun i ↦ h (Subtype.val i) i.prop :)
    (by ext; simp [Finset.sum_multiset_map_count, u.erase_attach_map (g · x)])

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

Goal state before:
pp: 𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
k : ℕ
x : 𝕜
⊢ (∏ i ∈ Finset.range k, (-1 - ↑i)) * x ^ (-1 - ↑k) = (-1) ^ k * ↑k ! * x ^ (-1 - ↑k)

Tactic:
simp only [← neg_add', Finset.prod_neg, ← Finset.prod_Ico_id_eq_factorial,
      Finset.prod_Ico_eq_prod_range]
    simp

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

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → G
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (fderiv 𝕜 f) 0 s
x y : E
hx : x ∈ s
hy : y ∈ s
⊢ f x = f y

Tactic:
obtain ⟨a, ha⟩ := hs.exists_is_const_of_fderiv_eq_zero hs' hf hf'

Goal state after:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → G
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (fderiv 𝕜 f) 0 s
x y : E
hx : x ∈ s
hy : y ∈ s
a : G
ha : ∀ x ∈ s, f x = a
⊢ f x = f y
Module: Mathlib.Analysis.Calculus.ContDiff.Basic

Goal state before:
pp: case cont
𝕜 : 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 := ⋯
⊢ ∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x ↦ (p x m).prod (q x m)) s

Tactic:
· intro m hm
    exact (L m).continuous.comp_continuousOn ((hf.cont m hm).prodMk (hg.cont m hm))

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

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
s : Set E
n : ℕ∞ω
f : E → F → G
g : E → F
t : Set F
hn : n ≠ ∞
x₀ : E
hf : ContDiffWithinAt 𝕜 (n + 1) (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
hg : ContDiffWithinAt 𝕜 n g s x₀
hgt : t ∈ 𝓝[g '' s] g x₀
hst : insert x₀ s ×ˢ t ∈ 𝓝[(fun x ↦ (x, g x)) '' s] (x₀, g x₀)
v : Set (E × F)
hv : v ∈ 𝓝[insert (x₀, g x₀) (insert x₀ s ×ˢ t)] (x₀, g x₀)
hvs : v ⊆ insert (x₀, g x₀) (insert x₀ s ×ˢ t)
f_an : n = ω → AnalyticOn 𝕜 (uncurry f) v
f' : E × F → E × F →L[𝕜] G
hvf' : ∀ x ∈ v, HasFDerivWithinAt (uncurry f) (f' x) (insert x₀ s ×ˢ t) x
hf' : ContDiffWithinAt 𝕜 n f' (insert x₀ s ×ˢ t) (x₀, g x₀)
this : (x₀, g x₀) ∈ v
⊢ v ∈ 𝓝[(fun x ↦ (id x, g x)) '' s] (id x₀, g x₀)

Tactic:
rw [← nhdsWithin_le_iff] at hst hv ⊢

Goal state after:
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
s : Set E
n : ℕ∞ω
f : E → F → G
g : E → F
t : Set F
hn : n ≠ ∞
x₀ : E
hf : ContDiffWithinAt 𝕜 (n + 1) (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
hg : ContDiffWithinAt 𝕜 n g s x₀
hgt : t ∈ 𝓝[g '' s] g x₀
hst : 𝓝[(fun x ↦ (x, g x)) '' s] (x₀, g x₀) ≤ 𝓝[insert x₀ s ×ˢ t] (x₀, g x₀)
v : Set (E × F)
hv : 𝓝[insert (x₀, g x₀) (insert x₀ s ×ˢ t)] (x₀, g x₀) ≤ 𝓝[v] (x₀, g x₀)
hvs : v ⊆ insert (x₀, g x₀) (insert x₀ s ×ˢ t)
f_an : n = ω → AnalyticOn 𝕜 (uncurry f) v
f' : E × F → E × F →L[𝕜] G
hvf' : ∀ x ∈ v, HasFDerivWithinAt (uncurry f) (f' x) (insert x₀ s ×ˢ t) x
hf' : ContDiffWithinAt 𝕜 n f' (insert x₀ s ×ˢ t) (x₀, g x₀)
this : (x₀, g x₀) ∈ v
⊢ 𝓝[(fun x ↦ (id x, g x)) '' s] (id x₀, g x₀) ≤ 𝓝[v] (id x₀, g x₀)
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: case mp
𝕜 : 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 ≠ ∞
h'n : n + 1 ≠ ∞
h : ContDiffWithinAt 𝕜 (n + 1) f s x
⊢ ∃ u ∈ 𝓝[insert x s] x,
    (n = ω → AnalyticOn 𝕜 f u) ∧ ∃ f', (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffWithinAt 𝕜 n f' u x

Tactic:
rcases (contDiffWithinAt_iff_of_ne_infty h'n).1 h with ⟨u, hu, p, Hp, H'p⟩

Goal state after:
case mp
𝕜 : 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 ≠ ∞
h'n : n + 1 ≠ ∞
h : ContDiffWithinAt 𝕜 (n + 1) f s x
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (n + 1) f p u
H'p : n + 1 = ω → ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ p x i) u
⊢ ∃ u ∈ 𝓝[insert x s] x,
    (n = ω → AnalyticOn 𝕜 f u) ∧ ∃ f', (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffWithinAt 𝕜 n f' u 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
m n : ℕ∞ω
hm : m ≤ n
h' : m = ∞ → n = ω
h : ContDiffWithinAt 𝕜 n f s x
⊢ ∃ u ∈ 𝓝[insert x s] x, u ⊆ insert x s ∧ ContDiffOn 𝕜 m f u

Tactic:
by
  obtain ⟨_u, uo, xu, h⟩ := h.contDiffOn' hm h'
  exact ⟨_, inter_mem_nhdsWithin _ (uo.mem_nhds xu), inter_subset_left, h⟩

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
⊢ ∀ (x : Fin (n + 1)),
    ∃ m,
      x ∈
        range (cases (motive := fun x ↦ Fin (cons 1 c.partSize x) → Fin (n + 1)) (fun x ↦ 0) (fun m ↦ succ ∘ c.emb m) m)

Tactic:
refine Fin.cases ?_ (fun i ↦ ?_)
    · simp only [mem_range]
      exact ⟨0, ⟨0, by simp⟩, by simp⟩
    · simp only [mem_range]
      exact ⟨Fin.succ (c.index i), Fin.cast (by simp) (c.invEmbedding i), by simp⟩

Goal state after: