mathlib-initiative/mathlib-tactics huggingface dataset:
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
f' : G →L[𝕜] E
⊢ HasFDerivWithinAt (⇑iso ∘ f) (↑iso ∘SL f') s x ↔ HasFDerivWithinAt f f' s x

Tactic:
by
  refine ⟨fun H => ?_, fun H => iso.hasFDerivAt.comp_hasFDerivWithinAt x H⟩
  simpa [Function.comp_def, ← ContinuousLinearMap.comp_assoc]
    using iso.symm.hasFDerivAt.comp_hasFDerivWithinAt x H

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
x : G
f' : G →L[𝕜] F
⊢ HasFDerivAt (⇑iso ∘ f) f' x ↔ HasFDerivAt f (↑iso.symm ∘SL f') x

Tactic:
simp_rw [← hasFDerivWithinAt_univ, iso.comp_hasFDerivWithinAt_iff']

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 : F → G
s : Set F
⊢ DifferentiableOn 𝕜 (f ∘ ⇑iso) (⇑iso ⁻¹' s) ↔ DifferentiableOn 𝕜 f s

Tactic:
by
  refine ⟨fun H y hy => ?_, fun H y hy => iso.comp_right_differentiableWithinAt_iff.2 (H _ hy)⟩
  rw [← iso.apply_symm_apply y, ← comp_right_differentiableWithinAt_iff]
  apply H
  simpa only [mem_preimage, apply_symm_apply] using hy

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_3
ι : Type u_4
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : TopologicalSpace M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : TopologicalSpace N
inst✝² : IsTopologicalAddGroup N
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f✝ f : ContinuousMultilinearMap R (fun x ↦ M) N
v : ι → M
i j : ι
hv : v i = v j
hne : i ≠ j
⊢ (∑ σ, Equiv.Perm.sign σ • domDomCongr σ f).toFun v = 0

Tactic:
simpa [MultilinearMap.alternatization_apply]
          using f.1.alternatization.map_eq_zero_of_eq' v i j hv hne

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

Goal state before:
pp: case pos
𝕜 : 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 : F → G
s : Set F
x : E
hxs : UniqueDiffWithinAt 𝕜 (⇑iso ⁻¹' s) x
h : DifferentiableWithinAt 𝕜 f s (iso x)
⊢ fderivWithin 𝕜 (f ∘ ⇑iso) (⇑iso ⁻¹' s) x = fderivWithin 𝕜 f s (iso x) ∘SL ↑iso

Tactic:
exact (iso.comp_right_hasFDerivWithinAt_iff.2 h.hasFDerivWithinAt).fderivWithin hxs

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
f : E → F
s : Set E
f' : E →L[𝕜] F
x : E
c : 𝕜
hc : c ≠ 0
⊢ HasFDerivWithinAt (fun x ↦ f (c • x)) f' s x ↔ HasFDerivWithinAt (c • f) f' (c • s) (c • x)

Tactic:
simp only [← hasFDerivWithinAt_comp_smul_smul_iff, Pi.smul_apply]
  lift c to 𝕜ˣ using IsUnit.mk0 c hc
  exact (ContinuousLinearEquiv.smulLeft c).comp_hasFDerivWithinAt_iff.symm

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Alternating.Basic

Goal state before:
pp: 𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
f✝ : E [⋀^ι]→L[𝕜] F
m : ι → E
inst✝ : IsEmpty ι
f : E [⋀^ι]→L[𝕜] F
⊢ constOfIsEmpty 𝕜 E ι ((fun f ↦ f 0) f) = f

Tactic:
ext x; simp [Subsingleton.allEq x 0]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
ι : Type u_6
F' : ι → Type u_7
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
i : ι
⊢ Differentiable 𝕜 fun f ↦ f i

Tactic:
by intro x; apply differentiableAt_apply

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
N : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
hN : ∞ ≤ N
k : ℕ
H : ∀ (n : ℕ), HasFTaylorSeriesUpToOn (↑(n + k)) f p s
m : ℕ
a✝ : ↑m < N
⊢ ∀ x ∈ s, HasFDerivWithinAt (fun x ↦ p x m) (p x m.succ).curryLeft s x

Tactic:
apply (H m.succ).fderivWithin m (by norm_cast; lia)

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
f : E → F
N : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
hN : ∞ ≤ N
⊢ HasFTaylorSeriesUpTo N f p ↔
    (∀ (x : E), (p x 0).curry0 = f x) ∧ ∀ (m : ℕ) (x : E), HasFDerivAt (fun y ↦ p y m) (p x m.succ).curryLeft x

Tactic:
simp only [← hasFTaylorSeriesUpToOn_univ_iff, hasFTaylorSeriesUpToOn_top_iff' hN, mem_univ,
    forall_true_left, hasFDerivWithinAt_univ]

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
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p univ
m : ℕ
hmn : ↑m ≤ n
x : E
⊢ p x m = iteratedFDerivWithin 𝕜 m f univ x

Tactic:
exact h.eq_iteratedFDerivWithin_of_uniqueDiffOn hmn uniqueDiffOn_univ (mem_univ _)

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
f : E → F
x : E
m : Fin 1 → E
⊢ (iteratedFDeriv 𝕜 1 f x) m = (fderiv 𝕜 f x) (m 0)

Tactic:
rw [iteratedFDeriv_succ_apply_right, iteratedFDeriv_zero_apply, last_zero]

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

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝔸 : Type u_3
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
c : 𝕜 → 𝔸
c' : 𝔸
hc : HasDerivWithinAt c c' s x
d : 𝔸
⊢ HasDerivWithinAt (fun y ↦ c y * d) (c' * d) s x

Tactic:
convert! hc.mul (hasDerivWithinAt_const x s d) using 1
  rw [mul_zero, add_zero]

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)
f : ContinuousMultilinearMap 𝕜 (fun x ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) F :=
  (ContinuousLinearMap.id 𝕜 (ContinuousMultilinearMap 𝕜 E F)).continuousMultilinearMapOption
Hf :
  HasStrictFDerivAt (fun x ↦ f fun x_1 ↦ x)
    ((f.linearDeriv fun x ↦ fa) ∘SL
      ContinuousLinearMap.pi fun x ↦ ContinuousLinearMap.id 𝕜 (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)))
    fa
⊢ 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:
convert! Hf using 1

Goal state after:
case e'_12
𝕜 : 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 := ⋯
Hf :
  HasStrictFDerivAt (fun x ↦ f fun x_1 ↦ x)
    ((f.linearDeriv fun x ↦ fa) ∘SL
      ContinuousLinearMap.pi fun x ↦ ContinuousLinearMap.id 𝕜 (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)))
    fa
e_4✝ : Prod.instAddCommGroup = Prod.normedAddCommGroup.toAddCommGroup
e_5✝ : Prod.instModule ≍ Prod.normedSpace.toModule
e_6✝ : instTopologicalSpaceProd = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
⊢ 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) =
    (f.linearDeriv fun x ↦ fa) ∘SL
      ContinuousLinearMap.pi fun x ↦ ContinuousLinearMap.id 𝕜 (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i))
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:
← slope_fun_def_field

Goal state after:
𝕜 : Type u
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : DecidableEq 𝕜
f : 𝕜 → 𝕜
c a : 𝕜
hf : HasDerivAt f a c
⊢ ContinuousAt (Function.update (slope f c) c a) c
Module: Mathlib.Analysis.Calculus.DSlope

Goal state before:
pp: case inl
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
s : Set 𝕜
hc : ContinuousOn f s
x : 𝕜
hx : x ∈ s
h : s ∈ 𝓝 x
hd : DifferentiableAt 𝕜 f x
⊢ ContinuousWithinAt (dslope f x) s x

pp: case inr
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a : 𝕜
s : Set 𝕜
h : s ∈ 𝓝 a
hc : ContinuousOn f s
hd : DifferentiableAt 𝕜 f a
x : 𝕜
hx : x ∈ s
hne : x ≠ a
⊢ ContinuousWithinAt (dslope f a) s x

Tactic:
exacts [(continuousAt_dslope_same.2 hd).continuousWithinAt,
    (continuousWithinAt_dslope_of_ne hne).2 (hc x hx)]

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
ι : Type u_5
𝔸' : Type u_7
inst✝² : NormedCommRing 𝔸'
inst✝¹ : NormedAlgebra 𝕜 𝔸'
g : ι → E → 𝔸'
g' : ι → E →L[𝕜] 𝔸'
inst✝ : DecidableEq ι
u : Multiset ι
x : E
h : ∀ i ∈ u, HasStrictFDerivAt (fun x ↦ g i x) (g' i) x
⊢ ((Multiset.map (fun i ↦ (Multiset.map (fun i ↦ g (↑i) x) (u.attach.erase i)).prod •> proj i) u.attach).sum ∘SL
      pi fun i ↦ g' ↑i) =
    (Multiset.map
        ((fun x_1 ↦ (Multiset.map (fun x_2 ↦ g x_2 x) ((Multiset.map Subtype.val u.attach).erase x_1)).prod •> g' x_1) ∘
          Subtype.val)
        u.attach).sum

Tactic:
by ext; simp [Finset.sum_multiset_map_count, u.erase_attach_map (g · x)]

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
ι : Type u_5
𝔸' : Type u_7
inst✝² : NormedCommRing 𝔸'
inst✝¹ : NormedAlgebra 𝕜 𝔸'
g : ι → E → 𝔸'
g' : ι → E →L[𝕜] 𝔸'
inst✝ : DecidableEq ι
u : Multiset ι
x : E
h : ∀ i ∈ u, HasFDerivAt (fun x ↦ g i x) (g' i) x
⊢ ((Multiset.map (fun i ↦ (Multiset.map (fun i ↦ g (↑i) x) (u.attach.erase i)).prod •> proj i) u.attach).sum ∘SL
      pi fun i ↦ g' ↑i) =
    (Multiset.map
        ((fun x_1 ↦ (Multiset.map (fun x_2 ↦ g x_2 x) ((Multiset.map Subtype.val u.attach).erase x_1)).prod •> g' x_1) ∘
          Subtype.val)
        u.attach).sum

Tactic:
by ext; simp [Finset.sum_multiset_map_count, u.erase_attach_map (g · x)]

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
⊢ ((Multiset.map (fun i ↦ (Multiset.map (fun i ↦ g (↑i) x) (u.attach.erase i)).prod •> proj i) u.attach).sum ∘SL
      pi fun i ↦ g' ↑i) =
    (Multiset.map
        ((fun x_1 ↦ (Multiset.map (fun x_2 ↦ g x_2 x) ((Multiset.map Subtype.val u.attach).erase x_1)).prod •> g' x_1) ∘
          Subtype.val)
        u.attach).sum

Tactic:
by ext; simp [Finset.sum_multiset_map_count, u.erase_attach_map (g · x)]

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

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h₂ : 𝕜' → 𝕜'
h₂' : 𝕜'
L' : Filter (𝕜' × 𝕜')
f : E → 𝕜'
f' : E →L[𝕜] 𝕜'
L'' : Filter (E × E)
hh₂ : HasDerivAtFilter h₂ h₂' L'
hf : HasFDerivAtFilter f f' L''
hL : Tendsto (Prod.map f f) L'' L'
⊢ HasFDerivAtFilter (h₂ ∘ f) (h₂' • f') L''

Tactic:
by
  convert! (hh₂.restrictScalars 𝕜).comp hf hL
  ext x
  simp [mul_comm]

Goal state after:
Module: Mathlib.Analysis.Analytic.IsolatedZeros

Goal state before:
pp: case mp
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g z₀
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
hg_ne : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
⊢ g =ᶠ[𝓝 z₀] fun {z₀} ↦ 0

Tactic:
EventuallyEq,

Goal state after:
case mp
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g z₀
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
hg_ne : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
⊢ ∀ᶠ (x : 𝕜) in 𝓝 z₀, g x = 0
Module: Mathlib.Analysis.Analytic.IsolatedZeros

Goal state before:
pp: case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
s : Set E
hfx : AnalyticAt 𝕜 f x
hs : s ∈ 𝓝[≠] f x
this : ∀ᶠ (z : 𝕜) in 𝓝 x, f z ∈ insert (f x) s
h : ¬f ⁻¹' s ∈ 𝓝[≠] x
⊢ f =ᶠ[𝓝 x] fun x_1 ↦ f x

Tactic:
EventuallyEq,

Goal state after:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
s : Set E
hfx : AnalyticAt 𝕜 f x
hs : s ∈ 𝓝[≠] f x
this : ∀ᶠ (z : 𝕜) in 𝓝 x, f z ∈ insert (f x) s
h : ¬f ⁻¹' s ∈ 𝓝[≠] x
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝 x, f x_1 = f x
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
⊢ ∃ a, ∀ x ∈ s, f x = a

Tactic:
obtain (rfl | ⟨y, hy⟩) := s.eq_empty_or_nonempty

Goal state after:
case inl
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
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ∅
hs' : IsPreconnected ∅
hf : DifferentiableOn 𝕜 f ∅
hf' : EqOn (fderiv 𝕜 f) 0 ∅
⊢ ∃ a, ∀ x ∈ ∅, f x = a

case inr
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
y : E
hy : y ∈ s
⊢ ∃ a, ∀ x ∈ s, f x = a
Module: Mathlib.Analysis.Calculus.ContDiff.Basic

Goal state before:
pp: 𝕜 : 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
f : E → F
x : E
n : ℕ∞ω
inst✝ : Subsingleton F
⊢ ContDiffAt 𝕜 n (fun x ↦ 0) x

Tactic:
exact contDiffAt_const

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

Goal state before:
pp: 𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
f : G → H
f' : G → G →L[𝕜] H
x : G
hder : ∀ᶠ (y : G) in 𝓝 x, HasFDerivAt f (f' y) y
hcont : ContinuousAt f' x
c : ℝ
hc : 0 < c
ε : ℝ
ε0 : ε > 0
hε : ball x ε ⊆ {x | (fun y ↦ HasFDerivAt f (f' y) y) x} ∩ f' ⁻¹' ball (f' x) c
a b : G
h : (a, b) ∈ ball x ε ×ˢ ball x ε
⊢ ‖f (a, b).1 - f (a, b).2 - (f' x) ((a, b).1 - (a, b).2)‖ ≤ c * ‖(a, b).1 - (a, b).2‖

Tactic:
prodMk_mem_set_prod_eq

Goal state after:
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
f : G → H
f' : G → G →L[𝕜] H
x : G
hder : ∀ᶠ (y : G) in 𝓝 x, HasFDerivAt f (f' y) y
hcont : ContinuousAt f' x
c : ℝ
hc : 0 < c
ε : ℝ
ε0 : ε > 0
hε : ball x ε ⊆ {x | (fun y ↦ HasFDerivAt f (f' y) y) x} ∩ f' ⁻¹' ball (f' x) c
a b : G
h : a ∈ ball x ε ∧ b ∈ ball x ε
⊢ ‖f (a, b).1 - f (a, b).2 - (f' x) ((a, b).1 - (a, b).2)‖ ≤ c * ‖(a, b).1 - (a, b).2‖
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:
by
  subst hy; exact hg.comp_of_mem_nhdsWithin_image x hf hs

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

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ∞ω
f : 𝕜 → F
s : Set 𝕜
hs : IsOpen s
⊢ ContDiffOn 𝕜 (n + 1) f s ↔ DifferentiableOn 𝕜 f s ∧ (n = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 n (deriv f) s

Tactic:
contDiffOn_succ_iff_derivWithin hs.uniqueDiffOn

Goal state after:
𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ∞ω
f : 𝕜 → F
s : Set 𝕜
hs : IsOpen s
⊢ DifferentiableOn 𝕜 f s ∧ (n = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 n (derivWithin f s) s ↔
    DifferentiableOn 𝕜 f s ∧ (n = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 n (deriv f) s
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
this : c.partSize (c.index 0) = Nat.card ↑(range (c.emb (c.index 0)))
⊢ 1 < Nat.card ↑(range (c.emb (c.index 0)))

Tactic:
rcases eq_or_ne (c.index 0) 0 with h | h

Goal state after:
case inl
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
this : c.partSize (c.index 0) = Nat.card ↑(range (c.emb (c.index 0)))
h : c.index 0 = 0
⊢ 1 < Nat.card ↑(range (c.emb (c.index 0)))

case inr
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
this : c.partSize (c.index 0) = Nat.card ↑(range (c.emb (c.index 0)))
h : c.index 0 ≠ 0
⊢ 1 < Nat.card ↑(range (c.emb (c.index 0)))
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: n : ℕ
c : OrderedFinpartition n
⊢ (range fun x ↦ 0) = {0}

Tactic:
apply @range_const _ _ (by simp; infer_instance)

Goal state after:
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) (deriv^[n] f) s

Tactic:
by
  apply Set.EqOn.trans (iteratedDerivWithin_of_isOpen hs)
  rw [iteratedDeriv_eq_iterate]
  exact Set.eqOn_refl _ _

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

Goal state before:
pp: case pos.refine_1
𝕜 : 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
j : Fin (update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i)
h : i = c.index 0
⊢ update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i + 1 = c.partSize i

Tactic:
rw [h]
        simpa using Nat.sub_add_cancel (c.partSize_pos (c.index 0))

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

Goal state before:
pp: case e'_4
𝕜 : 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 j : Fin c.length
hij : i < j
⊢ ↑(if h : j = c.index 0 then
          (c.emb j (Fin.cast ⋯ ⟨update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) j - 1, ⋯⟩.succ)).pred ⋯
        else (c.emb j (Fin.cast ⋯ ⟨update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) j - 1, ⋯⟩)).pred ⋯) +
      1 =
    ↑((fun m ↦ c.emb m ⟨c.partSize m - 1, ⋯⟩) j)

Tactic:
rcases eq_or_ne j (c.index 0) with rfl | hj
      · simp only [↓reduceDIte, update_self, succ_mk, cast_mk, val_pred]
        have A := c.one_lt_partSize_index_zero hc
        rw [Nat.sub_add_cancel]
        · congr; lia
        · rw [Order.one_le_iff_pos]
          conv_lhs => rw [show (0 : ℕ) = c.emb (c.index 0) 0 by simp [emb_zero]]
          rw [← lt_def]
          apply c.emb_strictMono
          simp [lt_def]
      · simp only [hj, ↓reduceDIte, ne_eq, not_false_eq_true, update_of_ne, cast_mk, val_pred]
        apply Nat.sub_add_cancel
        have : c.emb j ⟨c.partSize j - 1, Nat.sub_one_lt_of_lt (c.partSize_pos j)⟩
            ≠ c.emb (c.index 0) 0 := c.emb_ne_emb_of_ne hj
        simp only [c.emb_zero, ne_eq, ← val_eq_val, val_zero] at this
        lia

Goal state after: