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

Goal state before:
pp: 𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
e : E
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
f : (i : ι) → E → Fm i
s : Set E
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
⊢ HasFPowerSeriesWithinAt (fun x x_1 ↦ f x_1 x) (FormalMultilinearSeries.pi p) s e ↔
    ∀ (i : ι), HasFPowerSeriesWithinAt (f i) (p i) s e

Tactic:
refine ⟨fun h i ↦ ?_, fun h ↦ .pi h⟩

Goal state after:
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
e : E
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
f : (i : ι) → E → Fm i
s : Set E
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
h : HasFPowerSeriesWithinAt (fun x x_1 ↦ f x_1 x) (FormalMultilinearSeries.pi p) s e
i : ι
⊢ HasFPowerSeriesWithinAt (f i) (p i) s e
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: 𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
e : E
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
f : (i : ι) → E → Fm i
s : Set E
⊢ AnalyticWithinAt 𝕜 (fun x x_1 ↦ f x_1 x) s e ↔ ∀ (i : ι), AnalyticWithinAt 𝕜 (f i) s e

Tactic:
refine ⟨fun h i ↦ ?_, fun h ↦ .pi h⟩

Goal state after:
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
e : E
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
f : (i : ι) → E → Fm i
s : Set E
h : AnalyticWithinAt 𝕜 (fun x x_1 ↦ f x_1 x) s e
i : ι
⊢ AnalyticWithinAt 𝕜 (f i) s e
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
n✝ n : ℕ
c : Composition n
d : (i : Fin c.length) → Composition (c.blocksFun i)
this : List.map sum (ofFn fun i ↦ (d i).blocks) = c.blocks
e_2✝ :
  ({ blocks := (ofFn fun j ↦ (d j).blocks).flatten, blocks_pos := ⋯, blocks_sum := ⋯ }.gather
        { blocks := ofFn fun j ↦ (d j).length, blocks_pos := ⋯, blocks_sum := ⋯ }).length =
    c.length
i :
  Fin
    ({ blocks := (ofFn fun j ↦ (d j).blocks).flatten, blocks_pos := ⋯, blocks_sum := ⋯ }.gather
        { blocks := ofFn fun j ↦ (d j).length, blocks_pos := ⋯, blocks_sum := ⋯ }).length
⊢ List.map List.length (ofFn fun j ↦ (d j).blocks) =
    { blocks := ofFn fun j ↦ (d j).length, blocks_pos := ⋯, blocks_sum := ⋯ }.blocks

Tactic:
simp only [map_ofFn, Function.comp_def]

Goal state after:
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
b : E × F → G
h : IsBoundedBilinearMap 𝕜 b
p : E × F
⊢ HasStrictFDerivAt b (h.deriv p) p

Tactic:
simp only [hasStrictFDerivAt_iff_isLittleO]

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
b : E × F → G
h : IsBoundedBilinearMap 𝕜 b
p : E × F
⊢ (fun p_1 ↦ b p_1.1 - b p_1.2 - (h.deriv p) (p_1.1 - p_1.2)) =o[𝓝 (p, p)] fun p ↦ p.1 - p.2
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
b : E × F → G
h : IsBoundedBilinearMap 𝕜 b
T : Type (max u_3 u_2) := (E × F) × E × F
x₁ : E
y₁ : F
x₂ : E
y₂ : F
x : E
y : F
⊢ b (x, y) + b (x₁, y) + (b (x, y₁) + b (x₁, y₁)) - (b (x, y) + b (x₂, y) + (b (x, y₂) + b (x₂, y₂))) -
      (b (x, y) + b (x, y₁) + (b (x, y) + b (x₁, y)) - (b (x, y) + b (x, y₂) + (b (x, y) + b (x₂, y)))) =
    b (x₁, y₁) - b (x₂, y₂)

Tactic:
abel

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[𝕜] E
⊢ HasStrictFDerivAt (⇑iso ∘ f) (↑iso ∘SL f') x ↔ HasStrictFDerivAt f f' x

Tactic:
by
  refine ⟨fun H => ?_, fun H => iso.hasStrictFDerivAt.comp x H⟩
  convert! iso.symm.hasStrictFDerivAt.comp x H using 1 <;>
    ext z <;> apply (iso.symm_apply_apply _).symm

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
G' : Type u_5
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
L : G ≃L[𝕜] G'
f : E → F →L[𝕜] G
x : E
⊢ fderiv 𝕜 (fun x ↦ ↑L ∘SL f x) x = ↑((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L) ∘SL fderiv 𝕜 f x

Tactic:
change fderiv 𝕜 (((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L) ∘ f) x = _

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
G' : Type u_5
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
L : G ≃L[𝕜] G'
f : E → F →L[𝕜] G
x : E
⊢ fderiv 𝕜 (⇑((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L) ∘ f) x =
    ↑((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L) ∘SL fderiv 𝕜 f x
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
x : E
⊢ DifferentiableWithinAt 𝕜 (f ∘ ⇑iso) (⇑iso ⁻¹' s) x ↔ DifferentiableWithinAt 𝕜 f s (iso x)

Tactic:
refine ⟨fun H => ?_, fun H => H.comp x iso.differentiableWithinAt (mapsTo_preimage _ s)⟩
  have : DifferentiableWithinAt 𝕜 ((f ∘ iso) ∘ iso.symm) s (iso x) := by
    rw [← iso.symm_apply_apply x] at H
    apply H.comp (iso x) iso.symm.differentiableWithinAt
    intro y hy
    simpa only [mem_preimage, apply_symm_apply] using hy
  rwa [Function.comp_assoc, iso.self_comp_symm] at this

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

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
f' : E →L[ℝ] F
x : E
L : Filter E
⊢ Tendsto (fun x' ↦ ‖x' - x‖⁻¹ * ‖f x' - f x - f' (x' - x)‖) L (𝓝 0) ↔
    Tendsto (fun x' ↦ ‖x' - x‖⁻¹ • (f x' - f x - f' (x' - x))) L (𝓝 0)

Tactic:
symm
  rw [tendsto_iff_norm_sub_tendsto_zero]
  refine tendsto_congr fun x' => ?_
  simp [norm_smul]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Completion

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
A : Type u_3
inst✝ : SeminormedRing A
x y : Completion A
⊢ ‖x * y‖ ≤ ‖x‖ * ‖y‖

Tactic:
induction x, y using induction_on₂ with

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

Goal state before:
pp: α : Type u
β : Type v
inst✝⁷ : PseudoMetricSpace α
inst✝⁶ : Ring α
inst✝⁵ : IsTopologicalRing α
inst✝⁴ : IsUniformAddGroup α
inst✝³ : Ring β
inst✝² : PseudoMetricSpace β
inst✝¹ : IsUniformAddGroup β
inst✝ : IsTopologicalRing β
f : α →+* β
h : Isometry ⇑f
x y : Completion α
⊢ dist (h.mapRingHom x) (h.mapRingHom y) = dist x y

Tactic:
induction x, y using induction_on₂ with

Goal state after:
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
s : Set E
h : HasFPowerSeriesWithinAt f p s x
⊢ (fun y ↦
      f y.1 - f y.2 - ((continuousMultilinearCurryFin1 𝕜 E F) (p 1)) (y.1 - y.2)) =o[𝓝[insert x s ×ˢ insert x s] (x, x)]
    fun y ↦ y.1 - y.2

Tactic:
refine h.isBigO_image_sub_norm_mul_norm_sub.trans_isLittleO (IsLittleO.of_norm_right ?_)

Goal state after:
𝕜 : 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
s : Set E
h : HasFPowerSeriesWithinAt f p s x
⊢ (fun y ↦ ‖y - (x, x)‖ * ‖y.1 - y.2‖) =o[𝓝[insert x s ×ˢ insert x s] (x, x)] fun x ↦ ‖x.1 - x.2‖
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 : ℕ
a : E
⊢ (iteratedFDeriv 𝕜 n fun z ↦ f (z + a)) = fun x ↦ iteratedFDeriv 𝕜 n f (x + a)

Tactic:
by
  simpa [add_comm a] using iteratedFDeriv_comp_add_left' n a

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

Goal state before:
pp: case pos
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
R : Type u_2
inst✝³ : Monoid R
inst✝² : DistribMulAction R F
inst✝¹ : SMulCommClass 𝕜 R F
inst✝ : ContinuousConstSMul R F
c : R
hf : DifferentiableWithinAt 𝕜 f s x
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y ↦ c • f y) s x = c • derivWithin f s x

Tactic:
exact (hf.hasDerivWithinAt.const_smul c).derivWithin hsx

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

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝¹ : NormedDivisionRing 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
v : 𝕜 → 𝕜'
u : 𝕜'
⊢ derivWithin (fun y ↦ u * v y) s x = u * derivWithin v s x

Tactic:
apply derivWithin_const_smul_field (c := u)

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

Goal state before:
pp: case inr.refine_3
𝕜 : 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
x : (i : ι) → E i
inst✝ : DecidableEq ι
y : (i : ι) → E i
h✝ : Nonempty ι
i : ι
⊢ f (Function.update x i (y i)) =
    f fun i_1 ↦
      (ContinuousLinearMap.proj i_1)
        (Function.update (fun x_1 ↦ x) ((Fintype.equivFinOfCardEq ⋯) i) y ((Fintype.equivFinOfCardEq ⋯) i_1))

Tactic:
ContinuousLinearMap.proj_apply,

Goal state after:
case inr.refine_3
𝕜 : 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
x : (i : ι) → E i
inst✝ : DecidableEq ι
y : (i : ι) → E i
h✝ : Nonempty ι
i : ι
⊢ f (Function.update x i (y i)) =
    f fun i_1 ↦ Function.update (fun x_1 ↦ x) ((Fintype.equivFinOfCardEq ⋯) i) y ((Fintype.equivFinOfCardEq ⋯) i_1) i_1
Module: Mathlib.LinearAlgebra.AffineSpace.Slope

Goal state before:
pp: k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b : k
h : slope f a b = 0
⊢ f a = 0 +ᵥ f a

Tactic:
zero_vadd

Goal state after:
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b : k
h : slope f a b = 0
⊢ f a = f a
Module: Mathlib.Analysis.Calculus.Deriv.CompMul

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
f : 𝕜 → E
s : Set 𝕜
x : 𝕜
⊢ derivWithin (fun x ↦ f (c • x)) s x = c • derivWithin f (c • s) (c • x)

Tactic:
rw [← derivWithin_const_smul_field, derivWithin, derivWithin,
    fderivWithin_comp_smul_eq_fderivWithin_smul, Pi.smul_def]

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

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
a x : 𝕜
⊢ deriv (fun x ↦ f (a + -x)) x = -deriv f (a + -x)

Tactic:
deriv_comp_neg (f <| a + ·),

Goal state after:
𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
a x : 𝕜
⊢ -deriv (fun x ↦ f (a + x)) (-x) = -deriv f (a + -x)
Module: Mathlib.Analysis.Calculus.Deriv.ZPow

Goal state before:
pp: case e'_9.e_a.e_a
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this✝ : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun x ↦ x ^ m) (↑m * x ^ (m - 1)) x
hm : m < 0
hx : x ≠ 0
this : HasStrictDerivAt (fun x ↦ x ^ m) (↑(-m) * x ^ (-m - 1) * -((x ^ m)⁻¹ ^ 2)⁻¹) x
⊢ m - 1 = -m - 1 + (m + m)

Tactic:
abel

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

Goal state before:
pp: case inl
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, f x = B x → f' x < B' x
s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (fun x ↦ (f x, B x)) (Icc a b)
this✝¹ : IsClosed s
x : ℝ
hxB✝ : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
hxB : f x < B x
this✝ : ∀ᶠ (x : ℝ) in 𝓝[Icc a b] x, f x < B x
this : ∀ᶠ (x : ℝ) in 𝓝[>] x, f x < B x
⊢ {x | f x ≤ B x} ∈ 𝓝[>] x

Tactic:
exact this.mono fun y => le_of_lt

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
C : ℝ
s : Set E
x y : E
f' : E → E →L[𝕜] G
φ : E →L[𝕜] G
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
bound : ∀ x ∈ s, ‖f' x - φ‖ ≤ C
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : E → G := fun y ↦ f y - φ y
hg : ∀ x ∈ s, HasFDerivWithinAt g (f' x - φ) s x
⊢ f y - f x - (φ y - φ x) = f y - φ y - (f x - φ x)

Tactic:
abel

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 g : E → G
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hf' : EqOn (fderiv 𝕜 f) (fderiv 𝕜 g) s
x : E
hx : x ∈ s
⊢ fderiv 𝕜 (fun x ↦ f x - g x) x = 0 x

Tactic:
rw [fderiv_fun_sub (hf.differentiableAt (hs.mem_nhds hx)) (hg.differentiableAt (hs.mem_nhds hx)),
    hf' hx, sub_self, Pi.zero_apply]

Goal state after:
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
s : Set E
f : E → F
n : ℕ∞ω
x : G
g : G →L[𝕜] E
hf : ContDiffWithinAt 𝕜 n f s (g x)
⊢ ContDiffWithinAt 𝕜 n (f ∘ ⇑g) (⇑g ⁻¹' s) x

Tactic:
by
  match n with
  | ω =>
    obtain ⟨u, hu, p, hp, h'p⟩ := hf
    refine ⟨g ⁻¹' u, ?_, _, hp.compContinuousLinearMap g, ?_⟩
    · refine g.continuous.continuousWithinAt.tendsto_nhdsWithin ?_ hu
      exact (mapsTo_singleton.2 <| mem_singleton _).union_union (mapsTo_preimage _ _)
    · intro i
      change AnalyticOn 𝕜 (fun x ↦
        ContinuousMultilinearMap.compContinuousLinearMapL (fun _ ↦ g) (p (g x) i)) (⇑g ⁻¹' u)
      apply AnalyticOn.comp _ _ (Set.mapsTo_univ _ _)
      · exact ContinuousLinearMap.analyticOn _ _
      · exact (h'p i).comp (g.analyticOn _) (mapsTo_preimage _ _)
  | (n : ℕ∞) =>
    intro m hm
    rcases hf m hm with ⟨u, hu, p, hp⟩
    refine ⟨g ⁻¹' u, ?_, _, hp.compContinuousLinearMap g⟩
    refine g.continuous.continuousWithinAt.tendsto_nhdsWithin ?_ hu
    exact (mapsTo_singleton.2 <| mem_singleton _).union_union (mapsTo_preimage _ _)

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

pp: case refine_2
𝕜 : 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 ≠ ∞
⊢ (∃ 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) →
    ContDiffWithinAt 𝕜 (n + 1) f s x

Tactic:
· obtain ⟨u, hu, f_an, f', huf', hf'⟩ := (contDiffWithinAt_succ_iff_hasFDerivWithinAt hn).mp hf
    obtain ⟨w, hw, hxw, hwu⟩ := mem_nhdsWithin.mp hu
    rw [inter_comm] at hwu
    refine ⟨insert x s ∩ w, inter_mem_nhdsWithin _ (hw.mem_nhds hxw), inter_subset_left, ?_, f',
      fun y hy => ?_, ?_⟩
    · intro h
      apply (f_an h).mono hwu
    · refine ((huf' y <| hwu hy).mono hwu).mono_of_mem_nhdsWithin ?_
      grw [← subset_insert]
      exact inter_mem_nhdsWithin _ (hw.mem_nhds hy.2)
    · exact hf'.mono_of_mem_nhdsWithin (nhdsWithin_mono _ (subset_insert _ _) hu)

Goal state after:
case refine_2
𝕜 : 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 ≠ ∞
⊢ (∃ 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) →
    ContDiffWithinAt 𝕜 (n + 1) f s x
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
k m : Fin c.length
hm : m ≠ k
⊢ StrictMono (Fin.cast ⋯)

Tactic:
exact fun ⦃a b⦄ h ↦ 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✝ : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) = {0}
i : Fin (c.length - 1)
a b : Fin (c.partSize (Fin.cast ⋯ i.succ))
hab : a < b
⊢ c.emb (Fin.cast ⋯ i.succ) a < c.emb (Fin.cast ⋯ i.succ) b

Tactic:
apply c.emb_strictMono _ 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✝ : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) = {0}
x : Fin n
i : Fin c.length
j : Fin (c.partSize i)
hij : c.emb i j = x.succ
A : c.length = c.length - 1 + 1
i_ne : i ≠ 0
⊢ Fin.cast A i ≠ 0

Tactic:
by simpa using i_ne

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
f : E → F
⊢ ContDiff 𝕜 1 f ↔
    ∃ f', Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] f' ∧ ∀ (x : E), HasFDerivAt f (f' x) x

Tactic:
by
  convert! contDiff_succ_iff_hasFDerivAt using 4; simp

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

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕂
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedRing 𝔹
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
⊢ exp x * exp (-x) = 1

Tactic:
have hnx : -x ∈ Metric.eball (0 : 𝔸) (expSeries 𝕂 𝔸).radius := by
      rw [Metric.mem_eball, ← neg_zero, edist_neg_neg]
      exact hx
    rw [← exp_add_of_commute_of_mem_ball (Commute.neg_right <| Commute.refl x) hx hnx,
      add_neg_cancel, exp_zero]

Goal state after:
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas

Goal state before:
pp: case succ
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
n✝ : ℕ
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
𝔸 : Type u_5
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedAlgebra 𝕜 𝔸
inst✝² : Module 𝔸 F
inst✝¹ : IsBoundedSMul 𝔸 F
inst✝ : IsScalarTower 𝕜 𝔸 F
n : ℕ
IH :
  ∀ {f : 𝕜 → 𝔸} {g : 𝕜 → F},
    ContDiffWithinAt 𝕜 (↑n) f s x →
      ContDiffWithinAt 𝕜 (↑n) g s x →
        iteratedDerivWithin n (f • g) s x =
          ∑ i ∈ Finset.range (n + 1), n.choose i • iteratedDerivWithin i f s x • iteratedDerivWithin (n - i) g s x
f : 𝕜 → 𝔸
g : 𝕜 → F
hf : ContDiffWithinAt 𝕜 (↑(n + 1)) f s x
hg : ContDiffWithinAt 𝕜 (↑(n + 1)) g s x
U : Set 𝕜
hU : U ∈ 𝓝[insert x s] x
H : ∀ y ∈ U, ContDiffWithinAt 𝕜 (↑(n + 1)) f s y ∧ ContDiffWithinAt 𝕜 (↑(n + 1)) g s y
this : ∀ i ∈ Finset.range n, 1 ≤ n - i
⊢ ∑ x_1 ∈ Finset.range n,
          n.choose (x_1 + 1) • iteratedDerivWithin (x_1 + 1) f s x • iteratedDerivWithin (n - x_1) g s x +
        f x • iteratedDerivWithin (n + 1) g s x +
      ∑ x_1 ∈ Finset.range (n + 1),
        n.choose x_1 • iteratedDerivWithin (x_1 + 1) f s x • iteratedDerivWithin (n - x_1) g s x =
    ∑ x_1 ∈ Finset.range (n + 1),
          n.choose x_1 • iteratedDerivWithin (x_1 + 1) f s x • iteratedDerivWithin (n - x_1) g s x +
        ∑ x_1 ∈ Finset.range n,
          n.choose (x_1 + 1) • iteratedDerivWithin (x_1 + 1) f s x • iteratedDerivWithin (n - x_1) g s x +
      f x • iteratedDerivWithin (n + 1) g s x

Tactic:
abel

Goal state after: