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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
Fu : Type u
inst✝³ : NormedAddCommGroup Fu
inst✝² : NormedSpace 𝕜 Fu
f : E → Fu
s : Set E
t : Set Fu
x : E
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
n : ℕ
IH :
  ∀ m ≤ n,
    ∀ {Gu : Type u} [inst : NormedAddCommGroup Gu] [inst_1 : NormedSpace 𝕜 Gu] {g : Fu → Gu},
      ContDiffOn 𝕜 (↑m) g t →
        ContDiffOn 𝕜 (↑m) f s →
          (∀ i ≤ m, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C) →
            (∀ (i : ℕ), 1 ≤ i → i ≤ m → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i) →
              ‖iteratedFDerivWithin 𝕜 m (g ∘ f) s x‖ ≤ ↑m ! * C * D ^ m
Gu : Type u
inst✝¹ : NormedAddCommGroup Gu
inst✝ : NormedSpace 𝕜 Gu
g : Fu → Gu
hg : ContDiffOn 𝕜 (↑(n + 1)) g t
hf : ContDiffOn 𝕜 (↑(n + 1)) f s
hC : ∀ i ≤ n + 1, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C
hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n + 1 → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i
M : ↑n < ↑n.succ
Cnonneg : 0 ≤ C
Dnonneg : 0 ≤ D
I : ∀ i ∈ Finset.range (n + 1), ‖iteratedFDerivWithin 𝕜 i (fderivWithin 𝕜 g t ∘ f) s x‖ ≤ ↑i ! * C * D ^ i
J : ∀ (i : ℕ), ‖iteratedFDerivWithin 𝕜 (n - i) (fderivWithin 𝕜 f s) s x‖ ≤ D ^ (n - i + 1)
⊢ ‖(⇑(continuousMultilinearCurryRightEquiv' 𝕜 n E Gu).symm ∘
          iteratedFDerivWithin 𝕜 n (fun y ↦ fderivWithin 𝕜 (g ∘ f) s y) s)
        x‖ =
    ‖iteratedFDerivWithin 𝕜 n (fun y ↦ fderivWithin 𝕜 (g ∘ f) s y) s x‖

Tactic:
comp_apply,

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
Fu : Type u
inst✝³ : NormedAddCommGroup Fu
inst✝² : NormedSpace 𝕜 Fu
f : E → Fu
s : Set E
t : Set Fu
x : E
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
n : ℕ
IH :
  ∀ m ≤ n,
    ∀ {Gu : Type u} [inst : NormedAddCommGroup Gu] [inst_1 : NormedSpace 𝕜 Gu] {g : Fu → Gu},
      ContDiffOn 𝕜 (↑m) g t →
        ContDiffOn 𝕜 (↑m) f s →
          (∀ i ≤ m, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C) →
            (∀ (i : ℕ), 1 ≤ i → i ≤ m → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i) →
              ‖iteratedFDerivWithin 𝕜 m (g ∘ f) s x‖ ≤ ↑m ! * C * D ^ m
Gu : Type u
inst✝¹ : NormedAddCommGroup Gu
inst✝ : NormedSpace 𝕜 Gu
g : Fu → Gu
hg : ContDiffOn 𝕜 (↑(n + 1)) g t
hf : ContDiffOn 𝕜 (↑(n + 1)) f s
hC : ∀ i ≤ n + 1, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C
hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n + 1 → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i
M : ↑n < ↑n.succ
Cnonneg : 0 ≤ C
Dnonneg : 0 ≤ D
I : ∀ i ∈ Finset.range (n + 1), ‖iteratedFDerivWithin 𝕜 i (fderivWithin 𝕜 g t ∘ f) s x‖ ≤ ↑i ! * C * D ^ i
J : ∀ (i : ℕ), ‖iteratedFDerivWithin 𝕜 (n - i) (fderivWithin 𝕜 f s) s x‖ ≤ D ^ (n - i + 1)
⊢ ‖(continuousMultilinearCurryRightEquiv' 𝕜 n E Gu).symm
        (iteratedFDerivWithin 𝕜 n (fun y ↦ fderivWithin 𝕜 (g ∘ f) s y) s x)‖ =
    ‖iteratedFDerivWithin 𝕜 n (fun y ↦ fderivWithin 𝕜 (g ∘ f) s y) s x‖
Module: Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin

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
n : ℕ
S : Type u_5
inst✝³ : Monoid S
inst✝² : DistribMulAction S F
inst✝¹ : ContinuousConstSMul S F
inst✝ : SMulCommClass 𝕜 S F
c : S
f : E →L[𝕜] E [⋀^Fin n]→L[𝕜] F
⊢ alternatizeUncurryFin (c • f) = c • alternatizeUncurryFin f

Tactic:
ext v
  simp [alternatizeUncurryFin_apply, smul_comm _ c, Finset.smul_sum]

Goal state after:
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: case refine_4
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
P : Finset (α × ℝ) → Prop :=
  fun t ↦ ((↑t).PairwiseDisjoint fun p ↦ closedBall p.1 p.2) ∧ (∀ p ∈ t, p.1 ∈ s) ∧ ∀ p ∈ t, p.2 ∈ f p.1
F : Finset (α × ℝ) → Finset (α × ℝ)
hF :
  ∀ (t : Finset (α × ℝ)),
    P t →
      t ⊆ F t ∧ P (F t) ∧ μ (s \ ⋃ p ∈ F t, closedBall p.1 p.2) ≤ ↑N / (↑N + 1) * μ (s \ ⋃ p ∈ t, closedBall p.1 p.2)
u : ℕ → Finset (α × ℝ) := fun n ↦ F^[n] ∅
u_succ : ∀ (n : ℕ), u n.succ = F (u n)
Pu : ∀ (n : ℕ), P (u n)
⊢ (⋃ n, ↑(u n)).PairwiseDisjoint fun p ↦ closedBall p.1 p.2

Tactic:
refine (pairwiseDisjoint_iUnion ?_).2 fun n => (Pu n).1
    apply (monotone_nat_of_le_succ fun n => ?_).directed_le
    rw [← Nat.succ_eq_add_one, u_succ]
    exact (hF (u n) (Pu n)).1

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

Goal state before:
pp: f : ℝ → ℝ
x₀ : ℝ
h₀ : ∀ᶠ (x : ℝ) in 𝓝[≠] x₀, sign (deriv f x) = sign (x₀ - x)
⊢ ∀ᶠ (b : ℝ) in 𝓝[<] x₀, deriv f b > 0

Tactic:
by
  filter_upwards [nhdsLT_le_nhdsNE _ h₀, self_mem_nhdsWithin] with x hx' (hx : x < x₀)
  rwa [← sub_pos, ← sign_eq_one_iff, ← hx', sign_eq_one_iff] at hx

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : F → G
f : E → F
n : ℕ
s : Set E
t : Set F
x : E
N : ℕ∞ω
hg : ContDiffOn 𝕜 N g t
hf : ContDiffOn 𝕜 N f s
hn : ↑n ≤ N
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
hC : ∀ i ≤ n, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C
hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i
Fu : Type (max uF uG) := ULift.{uG, uF} F
Gu : Type (max uF uG) := ULift.{uF, uG} G
isoF : Fu ≃ₗᵢ[𝕜] F
isoG : Gu ≃ₗᵢ[𝕜] G
fu : E → Fu := ⇑isoF.symm ∘ f
gu : Fu → Gu := ⇑isoG.symm ∘ g ∘ ⇑isoF
tu : Set Fu := ⇑isoF ⁻¹' t
⊢ ‖iteratedFDerivWithin 𝕜 n (g ∘ f) s x‖ ≤ ↑n ! * C * D ^ n

Tactic:
have htu : UniqueDiffOn 𝕜 tu := isoF.toContinuousLinearEquiv.uniqueDiffOn_preimage_iff.2 ht

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : F → G
f : E → F
n : ℕ
s : Set E
t : Set F
x : E
N : ℕ∞ω
hg : ContDiffOn 𝕜 N g t
hf : ContDiffOn 𝕜 N f s
hn : ↑n ≤ N
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
hC : ∀ i ≤ n, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C
hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i
Fu : Type (max uF uG) := ULift.{uG, uF} F
Gu : Type (max uF uG) := ULift.{uF, uG} G
isoF : Fu ≃ₗᵢ[𝕜] F
isoG : Gu ≃ₗᵢ[𝕜] G
fu : E → Fu := ⇑isoF.symm ∘ f
gu : Fu → Gu := ⇑isoG.symm ∘ g ∘ ⇑isoF
tu : Set Fu := ⇑isoF ⁻¹' t
htu : UniqueDiffOn 𝕜 tu
⊢ ‖iteratedFDerivWithin 𝕜 n (g ∘ f) s x‖ ≤ ↑n ! * C * D ^ n
Module: Mathlib.Analysis.Calculus.VectorField

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W V₁ W₁ : E → E
x : E
hV : V₁ =ᶠ[𝓝 x] V
hW : W₁ =ᶠ[𝓝 x] W
y : E
⊢ V₁ =ᶠ[𝓝 y] V → W₁ =ᶠ[𝓝 y] W → lieBracket 𝕜 V₁ W₁ y = lieBracket 𝕜 V W y

Tactic:
hVy

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W V₁ W₁ : E → E
x : E
hV : V₁ =ᶠ[𝓝 x] V
hW : W₁ =ᶠ[𝓝 x] W
y : E
hVy : V₁ =ᶠ[𝓝 y] V
⊢ W₁ =ᶠ[𝓝 y] W → lieBracket 𝕜 V₁ W₁ y = lieBracket 𝕜 V W y
Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
H : Type u_6
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
f : E → G [⋀^ι]→L[𝕜] H
g : E → F →L[𝕜] G
s : Set E
x : E
inst✝ : Finite ι
hf : DifferentiableWithinAt 𝕜 f s x
hg : DifferentiableWithinAt 𝕜 g s x
⊢ DifferentiableWithinAt 𝕜 (fun x ↦ (f x).compContinuousLinearMap (g x)) s x

Tactic:
cases nonempty_fintype ι
  classical
  exact hf.hasFDerivWithinAt.continuousAlternatingMapCompContinuousLinearMap hg.hasFDerivWithinAt
    |>.differentiableWithinAt

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

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w : E
h4v : x + 4 • v ∈ interior s
h4w : x + 4 • w ∈ interior s
A : (fun h ↦ h ^ 2 • ((f'' w) v - (f'' v) w)) =o[𝓝[>] 0] fun h ↦ h ^ 2
this : (fun h ↦ 1 / h ^ 2) =O[𝓝[>] 0] fun h ↦ 1 / h ^ 2
C : (fun x ↦ (1 / x ^ 2) • x ^ 2 • ((f'' w) v - (f'' v) w)) =o[𝓝[>] 0] fun x ↦ (1 / x ^ 2) • x ^ 2
h : ℝ
hpos : 0 < h
⊢ (1 / h ^ 2) • h ^ 2 = 1

Tactic:
simp [field]

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

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n : ℕ∞ω
m : ℕ
hm : (if IsRCLikeNormedField 𝕜 then ↑m else ω) ≤ n
h : IsRCLikeNormedField 𝕜
⊢ ∃ n', ↑m ≤ n' ∧ n' ≤ n ∧ n' ≠ ∞

Tactic:
simp only [h, ↓reduceIte] at hm

Goal state after:
case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n : ℕ∞ω
m : ℕ
h : IsRCLikeNormedField 𝕜
hm : ↑m ≤ n
⊢ ∃ n', ↑m ≤ n' ∧ n' ≤ n ∧ n' ≠ ∞
Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n : ℕ∞ω
m : ℕ
hm : (if IsRCLikeNormedField 𝕜 then ↑m else ω) ≤ n
h : ¬IsRCLikeNormedField 𝕜
⊢ ∃ n', ω ≤ n' ∧ n' ≤ n ∧ n' ≠ ∞

Tactic:
simp only [h, ↓reduceIte] at hm

Goal state after:
case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n : ℕ∞ω
m : ℕ
h : ¬IsRCLikeNormedField 𝕜
hm : ω ≤ n
⊢ ∃ n', ω ≤ n' ∧ n' ≤ n ∧ n' ≠ ∞
Module: Mathlib.Analysis.Calculus.Gradient.Basic

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : CompleteSpace F
f : F → 𝕜
f' x : F
⊢ HasGradientWithinAt f f' univ x ↔ HasGradientAt f f' x

Tactic:
rw [hasGradientWithinAt_iff_hasFDerivWithinAt, hasGradientAt_iff_hasFDerivAt]
  exact hasFDerivWithinAt_univ

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
hf : ContDiffWithinAt 𝕜 n f s x
hn : minSmoothness 𝕜 2 ≤ n
hs : UniqueDiffOn 𝕜 s
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
h'x : x ∈ s
m : ℕ∞ω
hm : minSmoothness 𝕜 ↑2 ≤ m
hmn : m ≤ n
m_ne : m ≠ ∞
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : ContDiffOn 𝕜 m f (s ∩ u)
h'u : UniqueDiffOn 𝕜 (s ∩ u)
y : ℕ → E
hy : ∀ (n : ℕ), y n ∈ interior s
y_lim : Tendsto y atTop (𝓝 x)
L : ∀ᶠ (k : ℕ) in atTop, y k ∈ u
I : ∀ᶠ (k : ℕ) in atTop, IsSymmSndFDerivWithinAt 𝕜 f s (y k)
A : ContinuousOn (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s) (s ∩ u)
⊢ IsSymmSndFDerivWithinAt 𝕜 f s x

Tactic:
have B : Tendsto (fun k ↦ fderivWithin 𝕜 (fderivWithin 𝕜 f s) s (y k)) atTop
      (𝓝 (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x)) := by
    have : Tendsto y atTop (𝓝[s ∩ u] x) := by
      apply tendsto_nhdsWithin_iff.2 ⟨y_lim, ?_⟩
      filter_upwards [L] with k hk using ⟨interior_subset (hy k), hk⟩
    exact (A x ⟨h'x, xu⟩ ).tendsto.comp this

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
hf : ContDiffWithinAt 𝕜 n f s x
hn : minSmoothness 𝕜 2 ≤ n
hs : UniqueDiffOn 𝕜 s
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
h'x : x ∈ s
m : ℕ∞ω
hm : minSmoothness 𝕜 ↑2 ≤ m
hmn : m ≤ n
m_ne : m ≠ ∞
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : ContDiffOn 𝕜 m f (s ∩ u)
h'u : UniqueDiffOn 𝕜 (s ∩ u)
y : ℕ → E
hy : ∀ (n : ℕ), y n ∈ interior s
y_lim : Tendsto y atTop (𝓝 x)
L : ∀ᶠ (k : ℕ) in atTop, y k ∈ u
I : ∀ᶠ (k : ℕ) in atTop, IsSymmSndFDerivWithinAt 𝕜 f s (y k)
A : ContinuousOn (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s) (s ∩ u)
B : Tendsto (fun k ↦ fderivWithin 𝕜 (fderivWithin 𝕜 f s) s (y k)) atTop (𝓝 (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x))
⊢ IsSymmSndFDerivWithinAt 𝕜 f s x
Module: Mathlib.Analysis.Calculus.Gradient.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
g : 𝕜 → 𝕜
g' u : 𝕜
h : HasGradientAt g g' u
⊢ HasDerivAt g ((starRingEnd 𝕜) g') u

Tactic:
rw [hasGradientAt_iff_hasFDerivAt, hasFDerivAt_iff_hasDerivAt] at h

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
g : 𝕜 → 𝕜
g' u : 𝕜
h : HasDerivAt g (((toDual 𝕜 𝕜) g') 1) u
⊢ HasDerivAt g ((starRingEnd 𝕜) g') u
Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
hf : ContDiffWithinAt 𝕜 n f s x
hn : minSmoothness 𝕜 2 ≤ n
hs : UniqueDiffOn 𝕜 s
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
h'x : x ∈ s
m : ℕ∞ω
hm : minSmoothness 𝕜 ↑2 ≤ m
hmn : m ≤ n
m_ne : m ≠ ∞
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : ContDiffOn 𝕜 m f (s ∩ u)
h'u : UniqueDiffOn 𝕜 (s ∩ u)
y : ℕ → E
hy : ∀ (n : ℕ), y n ∈ interior s
y_lim : Tendsto y atTop (𝓝 x)
L : ∀ᶠ (k : ℕ) in atTop, y k ∈ u
I : ∀ᶠ (k : ℕ) in atTop, IsSymmSndFDerivWithinAt 𝕜 f s (y k)
A : ContinuousOn (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s) (s ∩ u)
B : Tendsto (fun k ↦ fderivWithin 𝕜 (fderivWithin 𝕜 f s) s (y k)) atTop (𝓝 (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x))
v w : E
⊢ Tendsto (fun k ↦ ((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s (y k)) v) w) atTop
    (𝓝 (((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) v) w))

Tactic:
have : Continuous (fun (A : E →L[𝕜] E →L[𝕜] F) ↦ A v w) := by fun_prop

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
hf : ContDiffWithinAt 𝕜 n f s x
hn : minSmoothness 𝕜 2 ≤ n
hs : UniqueDiffOn 𝕜 s
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
h'x : x ∈ s
m : ℕ∞ω
hm : minSmoothness 𝕜 ↑2 ≤ m
hmn : m ≤ n
m_ne : m ≠ ∞
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : ContDiffOn 𝕜 m f (s ∩ u)
h'u : UniqueDiffOn 𝕜 (s ∩ u)
y : ℕ → E
hy : ∀ (n : ℕ), y n ∈ interior s
y_lim : Tendsto y atTop (𝓝 x)
L : ∀ᶠ (k : ℕ) in atTop, y k ∈ u
I : ∀ᶠ (k : ℕ) in atTop, IsSymmSndFDerivWithinAt 𝕜 f s (y k)
A : ContinuousOn (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s) (s ∩ u)
B : Tendsto (fun k ↦ fderivWithin 𝕜 (fderivWithin 𝕜 f s) s (y k)) atTop (𝓝 (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x))
v w : E
this : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun A ↦ (A v) w
⊢ Tendsto (fun k ↦ ((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s (y k)) v) w) atTop
    (𝓝 (((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) v) w))
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts

Goal state before:
pp: a b : ℝ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo (min a b) (max a b), f' x ≤ 0
⊢ ∫ (x : ℝ) in a..b, f' x • (g ∘ f) x = ∫ (u : ℝ) in f a..f b, g u

Tactic:
have M : AntitoneOn f (uIcc a b) := by
    apply antitoneOn_of_deriv_nonpos (convex_uIcc a b) hf
    · rw [uIcc, interior_Icc]
      exact fun z hz ↦ (hff' z hz).differentiableAt.differentiableWithinAt
    · rw [uIcc, interior_Icc]
      intro z hz
      simpa [(hff' z hz).deriv] using hf' z hz
  simp only [Function.comp_apply]
  rcases le_or_gt a b with hab | hab
  · rw [integral_of_le hab, ← integral_Icc_eq_integral_Ioc,
      integral_Icc_deriv_smul_of_deriv_nonpos, integral_of_ge, ← integral_Icc_eq_integral_Ioc]
    · apply M left_mem_uIcc right_mem_uIcc hab
    · rwa [uIcc_of_le hab] at hf
    · grind
    · grind
    · exact hab
  · rw [integral_of_ge hab.le, ← integral_Icc_eq_integral_Ioc,
      integral_Icc_deriv_smul_of_deriv_nonpos, integral_of_le, ← integral_Icc_eq_integral_Ioc,
      neg_neg]
    · apply M right_mem_uIcc left_mem_uIcc hab.le
    · rwa [uIcc_of_ge hab.le] at hf
    · grind
    · grind
    · exact hab.le

Goal state after:
Module: Mathlib.MeasureTheory.Function.JacobianOneDim

Goal state before:
pp: case hf
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, 0 ≤ f' x
hab : a ≤ b
M : MonotoneOn f (Icc a b)
A : ∫ (u : ℝ) in Icc (f a) (f b), g u = ∫ (u : ℝ) in f '' Ioo a b, g u
⊢ MonotoneOn f (Ioo a b)

Tactic:
· exact M.mono Ioo_subset_Icc_self

Goal state after:
Module: Mathlib.MeasureTheory.Function.Jacobian

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal |A.det|
mpos : 0 < m
hA : A.det ≠ 0
B : E ≃L[ℝ] E := A.toContinuousLinearEquivOfDetNeZero hA
I : ENNReal.ofReal |(↑B.symm).det| < ↑m⁻¹
this : ∀ᶠ (δ : ℝ≥0) in 𝓝[>] 0, ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑B.symm) t δ → μ (g '' t) ≤ ↑m⁻¹ * μ t
⊢ ∃ δ, 0 < δ ∧ ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑B.symm) t δ → μ (g '' t) ≤ ↑m⁻¹ * μ t

Tactic:
rcases (this.and self_mem_nhdsWithin).exists with ⟨δ₀, h, h'⟩

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal |A.det|
mpos : 0 < m
hA : A.det ≠ 0
B : E ≃L[ℝ] E := A.toContinuousLinearEquivOfDetNeZero hA
I : ENNReal.ofReal |(↑B.symm).det| < ↑m⁻¹
this : ∀ᶠ (δ : ℝ≥0) in 𝓝[>] 0, ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑B.symm) t δ → μ (g '' t) ≤ ↑m⁻¹ * μ t
δ₀ : ℝ≥0
h : ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑B.symm) t δ₀ → μ (g '' t) ≤ ↑m⁻¹ * μ t
h' : 0 < δ₀
⊢ ∃ δ, 0 < δ ∧ ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑B.symm) t δ → μ (g '' t) ≤ ↑m⁻¹ * μ t
Module: Mathlib.MeasureTheory.Function.JacobianOneDim

Goal state before:
pp: case hf
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, 0 ≤ f' x
hab : a ≤ b
M : MonotoneOn f (Icc a b)
A : IntegrableOn g (Icc (f a) (f b)) volume ↔ IntegrableOn g (f '' Ioo a b) volume
⊢ MonotoneOn f (Ioo a b)

Tactic:
· exact M.mono Ioo_subset_Icc_self

Goal state after:
Module: Mathlib.MeasureTheory.Function.JacobianOneDim

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : AntitoneOn f s
g : ℝ → F
n : ℝ → ℝ := fun x ↦ -x
e : ℝ → ℝ := n ∘ f
hg' : ∀ x ∈ s, HasDerivWithinAt e (-f' x) s x
A : IntegrableOn (fun x ↦ g (n x)) (e '' s) volume ↔ IntegrableOn (fun x ↦ -f' x • (g ∘ n) (e x)) s volume
⊢ IntegrableOn g (f '' s) volume ↔ IntegrableOn (fun x ↦ -f' x • g (f x)) s volume

Tactic:
have B : IntegrableOn g (n '' e '' s) ↔ IntegrableOn (fun x ↦ (|-1| : ℝ) • g (n x)) (e '' s) :=
    integrableOn_image_iff_integrableOn_abs_deriv_smul (hs.image_of_monotoneOn hf.neg)
      (fun x hx ↦ hasDerivWithinAt_neg _ _) neg_injective.injOn _

Goal state after:
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : AntitoneOn f s
g : ℝ → F
n : ℝ → ℝ := fun x ↦ -x
e : ℝ → ℝ := n ∘ f
hg' : ∀ x ∈ s, HasDerivWithinAt e (-f' x) s x
A : IntegrableOn (fun x ↦ g (n x)) (e '' s) volume ↔ IntegrableOn (fun x ↦ -f' x • (g ∘ n) (e x)) s volume
B : IntegrableOn g (n '' e '' s) volume ↔ IntegrableOn (fun x ↦ |(-1)| • g (n x)) (e '' s) volume
⊢ IntegrableOn g (f '' s) volume ↔ IntegrableOn (fun x ↦ -f' x • g (f x)) s volume
Module: Mathlib.MeasureTheory.Function.JacobianOneDim

Goal state before:
pp: case hf
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, f' x ≤ 0
hab : a ≤ b
M : AntitoneOn f (Icc a b)
A : ∫ (u : ℝ) in Icc (f b) (f a), g u = ∫ (u : ℝ) in f '' Ioo a b, g u
⊢ AntitoneOn f (Ioo a b)

Tactic:
· exact M.mono Ioo_subset_Icc_self

Goal state after:
Module: Mathlib.MeasureTheory.Function.JacobianOneDim

Goal state before:
pp: case hf
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, f' x ≤ 0
hab : a ≤ b
M : AntitoneOn f (Icc a b)
A : IntegrableOn g (Icc (f b) (f a)) volume ↔ IntegrableOn g (f '' Ioo a b) volume
⊢ AntitoneOn f (Ioo a b)

Tactic:
· exact M.mono Ioo_subset_Icc_self

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : ℝ → E
p : ℝ
hp : 0 < p
c : ℝ
hc : 0 ≤ c
this✝ : 0 ≤ c ^ p⁻¹
this : Ioi c = (fun x ↦ x ^ p) '' Ioi (c ^ p⁻¹)
⊢ ∫ (x : ℝ) in Ioi (c ^ p⁻¹), (p * x ^ (p - 1)) • g (x ^ p) = ∫ (y : ℝ) in (fun x ↦ x ^ p) '' Ioi (c ^ p⁻¹), g y

Tactic:
integral_image_eq_integral_abs_deriv_smul (measurableSet_Ioi (a := c ^ p⁻¹))
      (fun _ _ ↦ (hasDerivAt_rpow_const (by grind)).hasDerivWithinAt)
      ((rpow_left_injOn hp.ne.symm).mono (Set.Ioi_subset_Ici (by positivity)))

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : ℝ → E
p : ℝ
hp : 0 < p
c : ℝ
hc : 0 ≤ c
this✝ : 0 ≤ c ^ p⁻¹
this : Ioi c = (fun x ↦ x ^ p) '' Ioi (c ^ p⁻¹)
⊢ ∫ (x : ℝ) in Ioi (c ^ p⁻¹), (p * x ^ (p - 1)) • g (x ^ p) = ∫ (x : ℝ) in Ioi (c ^ p⁻¹), |p * x ^ (p - 1)| • g (x ^ p)
Module: Mathlib.Analysis.Complex.LocallyUniformLimit

Goal state before:
pp: E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
U K : Set ℂ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
inst✝ : CompleteSpace E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
⊢ ∃ δ > 0, cthickening δ K ⊆ U ∧ TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K

Tactic:
by
  obtain ⟨δ, hδ, hKδ⟩ := hK.exists_cthickening_subset_open hU hKU
  exact ⟨δ, hδ, hKδ, tendstoUniformlyOn_deriv_of_cthickening_subset hf hF hδ hK hU hKδ⟩

Goal state after:
Module: Mathlib.Geometry.Manifold.StructureGroupoid

Goal state before:
pp: case inr
H✝ : Type u_1
inst✝¹ : TopologicalSpace H✝
H : Type u_2
inst✝ : TopologicalSpace H
e e' : OpenPartialHomeomorph H H
he' : e' ∈ {OpenPartialHomeomorph.refl H} ∪ {e | e.source = ∅}
he : e ∈ {e | e.source = ∅}
⊢ e ≫ₕ e' ∈ {OpenPartialHomeomorph.refl H} ∪ {e | e.source = ∅}

Tactic:
· have : (e ≫ₕ e').source ⊆ e.source := sep_subset _ _
      rw [he] at this
      have : e ≫ₕ e' ∈ { e : OpenPartialHomeomorph H H | e.source = ∅ } := eq_bot_iff.2 this
      exact (mem_union _ _ _).2 (Or.inr this)

Goal state after: