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

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
inst✝ : CompleteSpace E
f : E → F
s : Set E
x : E
h'f : ContDiffWithinAt 𝕜 2 f s x
hf : (fderivWithin 𝕜 f s x).IsInvertible
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
⊢ ∃ N,
    ContDiffWithinAt 𝕜 1 (fun y ↦ ↑(N y)) s x ∧
      ContDiffWithinAt 𝕜 1 (fun y ↦ ↑(N y).symm) s x ∧
        (∀ᶠ (y : E) in 𝓝[s] x, ↑(N y) = fderivWithin 𝕜 f s y) ∧
          ∀ (v : E),
            (fderivWithin 𝕜 (fun y ↦ ↑(N y).symm) s x) v =
              -↑(N x).symm ∘SL (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) v ∘SL ↑(N x).symm

Tactic:
classical
  rcases hf with ⟨M, hM⟩
  let U := {y | ∃ (N : E ≃L[𝕜] F), N = fderivWithin 𝕜 f s y}
  have hU : U ∈ 𝓝[s] x := by
    have I : range ((↑) : (E ≃L[𝕜] F) → E →L[𝕜] F) ∈ 𝓝 (fderivWithin 𝕜 f s x) := by
      rw [← hM]
      exact M.nhds
    have : ContinuousWithinAt (fderivWithin 𝕜 f s) s x :=
      (h'f.fderivWithin_right (m := 1) hs le_rfl hx).continuousWithinAt
    exact this I
  let N : E → (E ≃L[𝕜] F) := fun x ↦ if h : x ∈ U then h.choose else M
  have eN : (fun y ↦ (N y : E →L[𝕜] F)) =ᶠ[𝓝[s] x] fun y ↦ fderivWithin 𝕜 f s y := by
    filter_upwards [hU] with y hy
    simpa only [hy, ↓reduceDIte, N] using Exists.choose_spec hy
  have e'N : N x = fderivWithin 𝕜 f s x := by apply mem_of_mem_nhdsWithin hx eN
  have hN : ContDiffWithinAt 𝕜 1 (fun y ↦ (N y : E →L[𝕜] F)) s x := by
    have : ContDiffWithinAt 𝕜 1 (fun y ↦ fderivWithin 𝕜 f s y) s x :=
      h'f.fderivWithin_right (m := 1) hs le_rfl hx
    apply this.congr_of_eventuallyEq eN e'N
  have hN' : ContDiffWithinAt 𝕜 1 (fun y ↦ ((N y).symm : F →L[𝕜] E)) s x := by
    have : ContDiffWithinAt 𝕜 1 (ContinuousLinearMap.inverse ∘ (fun y ↦ (N y : E →L[𝕜] F))) s x :=
      (contDiffAt_map_inverse (N x)).comp_contDiffWithinAt x hN
    convert! this with y
    simp only [Function.comp_apply, ContinuousLinearMap.inverse_equiv]
  refine ⟨N, hN, hN', eN, fun v ↦ ?_⟩
  have A' y : ContinuousLinearMap.compL 𝕜 F E F (N y : E →L[𝕜] F) ((N y).symm : F →L[𝕜] E)
      = ContinuousLinearMap.id 𝕜 F := by ext; simp
  have : fderivWithin 𝕜 (fun y ↦ ContinuousLinearMap.compL 𝕜 F E F (N y : E →L[𝕜] F)
      ((N y).symm : F →L[𝕜] E)) s x v = 0 := by
    simp [A', fderivWithin_const_apply]
  have I : (N x : E →L[𝕜] F) ∘L (fderivWithin 𝕜 (fun y ↦ ((N y).symm : F →L[𝕜] E)) s x v) =
      - (fderivWithin 𝕜 (fun y ↦ (N y : E →L[𝕜] F)) s x v) ∘L ((N x).symm : F →L[𝕜] E) := by
    rw [ContinuousLinearMap.fderivWithin_of_bilinear _ (hN.differentiableWithinAt one_ne_zero)
      (hN'.differentiableWithinAt one_ne_zero) (hs x hx)] at this
    simpa [eq_neg_iff_add_eq_zero] using this
  have B (M : F →L[𝕜] E) : M = ((N x).symm : F →L[𝕜] E) ∘L ((N x) ∘L M) := by
    ext; simp
  rw [B (fderivWithin 𝕜 (fun y ↦ ((N y).symm : F →L[𝕜] E)) s x v), I]
  simp only [ContinuousLinearMap.comp_neg, eN.fderivWithin_eq e'N]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : E → F
s : Set E
x v : E
h : s ∈ 𝓝 x
⊢ s ∈ 𝓝 (x + 0 • v)

Tactic:
by simpa using h

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

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
inst✝ : CompleteSpace E
f : E → F
V : F → F
s : Set E
t : Set F
x : E
hV : DifferentiableWithinAt 𝕜 V t (f x)
hf : ContDiffWithinAt 𝕜 2 f s x
hf' : (fderivWithin 𝕜 f s x).IsInvertible
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
M : E → E ≃L[𝕜] F
M_symm_smooth : ContDiffWithinAt 𝕜 1 (fun y ↦ ↑(M y).symm) s x
hM : ∀ᶠ (y : E) in 𝓝[s] x, ↑(M y) = fderivWithin 𝕜 f s y
⊢ DifferentiableWithinAt 𝕜 (VectorField.pullbackWithin 𝕜 f V s) s x

Tactic:
simp only [pullbackWithin_eq]

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
inst✝ : CompleteSpace E
f : E → F
V : F → F
s : Set E
t : Set F
x : E
hV : DifferentiableWithinAt 𝕜 V t (f x)
hf : ContDiffWithinAt 𝕜 2 f s x
hf' : (fderivWithin 𝕜 f s x).IsInvertible
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
M : E → E ≃L[𝕜] F
M_symm_smooth : ContDiffWithinAt 𝕜 1 (fun y ↦ ↑(M y).symm) s x
hM : ∀ᶠ (y : E) in 𝓝[s] x, ↑(M y) = fderivWithin 𝕜 f s y
⊢ DifferentiableWithinAt 𝕜 (fun x ↦ (fderivWithin 𝕜 f s x).inverse (V (f x))) s x
Module: Mathlib.Analysis.Calculus.LineDeriv.Basic

Goal state before:
pp: case h₁
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₀ f₁ : E → F
f' : F
s : Set E
x v : E
h : f₀ =ᶠ[𝓝[s] x] f₁
hx : f₀ x = f₁ x
⊢ (fun t ↦ f₀ (x + t • v)) =ᶠ[𝓝[(fun t ↦ x + t • v) ⁻¹' s] 0] fun t ↦ f₁ (x + t • v)

pp: case hx
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₀ f₁ : E → F
f' : F
s : Set E
x v : E
h : f₀ =ᶠ[𝓝[s] x] f₁
hx : f₀ x = f₁ x
⊢ f₀ (x + 0 • v) = f₁ (x + 0 • v)

Tactic:
· have A : Continuous (fun (t : 𝕜) ↦ x + t • v) := by fun_prop
    exact A.continuousWithinAt.preimage_mem_nhdsWithin'' h (by simp)

Goal state after:
case hx
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₀ f₁ : E → F
f' : F
s : Set E
x v : E
h : f₀ =ᶠ[𝓝[s] x] f₁
hx : f₀ x = f₁ x
⊢ f₀ (x + 0 • v) = f₁ (x + 0 • v)
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
f : E → F
inst✝ : IsRCLikeNormedField 𝕜
f' : E → E →L[𝕜] F
x : E
f'' : E →L[𝕜] E →L[𝕜] F
hf : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (f' y) y
hx : HasFDerivAt f' f'' x
v w : E
x✝² : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x✝¹ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
x✝ : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
f'R : E → E →L[ℝ] F := fun x ↦ ContinuousLinearMap.restrictScalars ℝ (f' x)
f''R : E →L[ℝ] E →L[ℝ] F := ContinuousLinearMap.bilinearRestrictScalars ℝ f''
hfR : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (f'R y) y
this : HasFDerivAt f'R f''R x
⊢ (f'' v) w = (f'' w) v

Tactic:
change f''R v w = f''R w v

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
f : E → F
inst✝ : IsRCLikeNormedField 𝕜
f' : E → E →L[𝕜] F
x : E
f'' : E →L[𝕜] E →L[𝕜] F
hf : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (f' y) y
hx : HasFDerivAt f' f'' x
v w : E
x✝² : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x✝¹ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
x✝ : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
f'R : E → E →L[ℝ] F := fun x ↦ ContinuousLinearMap.restrictScalars ℝ (f' x)
f''R : E →L[ℝ] E →L[ℝ] F := ContinuousLinearMap.bilinearRestrictScalars ℝ f''
hfR : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (f'R y) y
this : HasFDerivAt f'R f''R x
⊢ (f''R v) w = (f''R w) v
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: case refine_4
α : Type u_1
inst✝⁵ : MetricSpace α
β : Type u
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : Measure α
inst✝ : SFinite μ
s : Set α
f : α → Set (Set α)
fsubset : ∀ x ∈ s, f x ⊆ (fun r ↦ closedBall x r) '' Ioi 0
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
g : α → Set ℝ := fun x ↦ {r | 0 < r ∧ closedBall x r ∈ f x}
A : ∀ x ∈ s, ∀ δ > 0, (g x ∩ Ioo 0 δ).Nonempty
t : Set α
r : α → ℝ
left✝ : t.Countable
ts : t ⊆ s
tg : ∀ x ∈ t, r x ∈ g x ∩ Ioo 0 1
μt : μ (s \ ⋃ x ∈ t, closedBall x (r x)) = 0
tdisj : t.PairwiseDisjoint fun x ↦ closedBall x (r x)
F : α → α × Set α := fun x ↦ (x, closedBall x (r x))
⊢ μ (s \ ⋃ p ∈ F '' t, p.2) = 0

Tactic:
· rwa [biUnion_image]

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

Goal state before:
pp: case h₁
𝕜 : Type u_1
E₁ : Type u_2
E₂ : Type u_3
F : Type u_4
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E₁
inst✝⁵ : NormedSpace 𝕜 E₁
inst✝⁴ : NormedAddCommGroup E₂
inst✝³ : NormedSpace 𝕜 E₂
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : IsRCLikeNormedField 𝕜
u : E₁ × E₂
f : E₁ → E₂ → F
f₁ : E₁ → E₂ → E₁ →L[𝕜] F
f₂ : E₁ → E₂ → E₂ →L[𝕜] F
df₁ : ∀ᶠ (v : E₁ × E₂) in 𝓝 u.1 ×ˢ 𝓝 u.2, HasFDerivAt (fun x ↦ f x v.2) (↿f₁ v) v.1
df₂ : ∀ᶠ (v : E₁ × E₂) in 𝓝 u.1 ×ˢ 𝓝 u.2, HasFDerivAt (fun x ↦ f v.1 x) (↿f₂ v) v.2
cf₁ : Tendsto (↿f₁) (𝓝 u.1 ×ˢ 𝓝 u.2) (𝓝 (↿f₁ u))
cf₂ : Tendsto (↿f₂) (𝓝 u.1 ×ˢ 𝓝 u.2) (𝓝 (↿f₂ u))
this : RCLike 𝕜 := ⋯
⊢ (fun x ↦ f x.1.1 x.2.2 - f x.2.1 x.2.2 - (↿f₁ u) (x.1.1 - x.2.1)) =o[(𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ 𝓝 u.1 ×ˢ 𝓝 u.2] fun x ↦
    match x with
    | (v, w) => v - w

Tactic:
calc
          fun (v, w) => f v.1 w.2 - f w.1 w.2 - ↿f₁ u (v.1 - w.1)
          _ =o[(𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ (𝓝 u.1 ×ˢ 𝓝 u.2)] (fun (v, w) => v.1 - w.1 : _ → E₁) := by
            have h := tendsto_snd.prodMk <| tendsto_snd.comp <| tendsto_snd.comp <|
              tendsto_fst (f := (𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ (𝓝 u.1 ×ˢ 𝓝 u.2)) (g := 𝓝 u.1)
            let : NormedSpace ℝ E₁ := RestrictScalars.normedSpace ℝ 𝕜 E₁
            apply isLittleO_sub_sub_fderiv (α := (E₁ × E₂) × (E₁ × E₂))
              (f := fun (v, w) x => f x w.2) (f' := fun (v, w) x => f₁ x w.2)
              (tendsto_fst.comp tendsto_fst) (tendsto_fst.comp tendsto_snd)
            · simpa using! h.eventually df₁
            · simpa using! cf₁.comp h
          _ =O[(𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ (𝓝 u.1 ×ˢ 𝓝 u.2)] (fun (v, w) => v - w : _ → E₁ × E₂) := by
            simp [isBigO_of_le]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x ↦ ‖x‖) x
this : ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖
⊢ deriv _root_.abs (1 + 0) * deriv (fun t ↦ 1 + t) 0 * ‖x‖ = ‖x‖

pp: case hh₂
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x ↦ ‖x‖) x
this : ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖
⊢ DifferentiableAt ℝ _root_.abs (1 + 0)

pp: case hh
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x ↦ ‖x‖) x
this : ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖
⊢ DifferentiableAt ℝ (fun t ↦ 1 + t) 0

Tactic:
deriv_abs,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x ↦ ‖x‖) x
this : ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖
⊢ ↑(SignType.sign (1 + 0)) * deriv (fun t ↦ 1 + t) 0 * ‖x‖ = ‖x‖

case hh₂
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x ↦ ‖x‖) x
this : ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖
⊢ DifferentiableAt ℝ _root_.abs (1 + 0)

case hh
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x ↦ ‖x‖) x
this : ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖
⊢ DifferentiableAt ℝ (fun t ↦ 1 + t) 0
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts

Goal state before:
pp: case hg
a b : ℝ
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAlgebra ℝ 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : IsScalarTower ℝ 𝕜 E
u u' : ℝ → 𝕜
v v' : ℝ → E
hu : ContinuousOn u [[a, b]]
hv : ContinuousOn v [[a, b]]
huu' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt u (u' x) (Ioi x) x
hvv' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt v (v' x) (Ioi x) x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
⊢ IntervalIntegrable (fun x ↦ u' x • v x) volume a b

Tactic:
exact hu'.smul_continuousOn hv

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

Goal state before:
pp: case inr
E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : SecondCountableTopology F
f : E → F
s : Set E
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
r : (E →L[ℝ] F) → ℝ≥0
rpos : ∀ (A : E →L[ℝ] F), r A ≠ 0
hs : s.Nonempty
T : Set ↑s
T_count : T.Countable
hT : ⋃ x ∈ T, ball (f' ↑x) ↑(r (f' ↑x)) = ⋃ x, ball (f' ↑x) ↑(r (f' ↑x))
u : ℕ → ℝ
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
M : ℕ → ↑T → Set E :=
  fun n z ↦ {x | x ∈ s ∧ ∀ y ∈ s ∩ ball x (u n), ‖f y - f x - (f' ↑↑z) (y - x)‖ ≤ ↑(r (f' ↑↑z)) * ‖y - x‖}
s_subset : ∀ x ∈ s, ∃ n z, x ∈ M n z
closure_M_subset : ∀ (n : ℕ) (z : ↑T), s ∩ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (M n z) ⊆ M n z
d : ℕ → E
hd : DenseRange d
K : ℕ → ↑T → ℕ → Set E :=
  fun n z p ↦ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (M n z) ∩ closedBall (d p) (u n / 3)
K_approx : ∀ (n : ℕ) (z : ↑T) (p : ℕ), ApproximatesLinearOn f (f' ↑↑z) (s ∩ K n z p) (r (f' ↑↑z))
⊢ ∃ t A,
    (∀ (n : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (t n)) ∧
      s ⊆ ⋃ n, t n ∧
        (∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (r (A n))) ∧ (s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y)

Tactic:
have K_closed : ∀ (n) (z : T) (p), IsClosed (K n z p) := fun n z p =>
    isClosed_closure.inter isClosed_closedBall

Goal state after:
case inr
E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : SecondCountableTopology F
f : E → F
s : Set E
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
r : (E →L[ℝ] F) → ℝ≥0
rpos : ∀ (A : E →L[ℝ] F), r A ≠ 0
hs : s.Nonempty
T : Set ↑s
T_count : T.Countable
hT : ⋃ x ∈ T, ball (f' ↑x) ↑(r (f' ↑x)) = ⋃ x, ball (f' ↑x) ↑(r (f' ↑x))
u : ℕ → ℝ
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
M : ℕ → ↑T → Set E :=
  fun n z ↦ {x | x ∈ s ∧ ∀ y ∈ s ∩ ball x (u n), ‖f y - f x - (f' ↑↑z) (y - x)‖ ≤ ↑(r (f' ↑↑z)) * ‖y - x‖}
s_subset : ∀ x ∈ s, ∃ n z, x ∈ M n z
closure_M_subset : ∀ (n : ℕ) (z : ↑T), s ∩ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (M n z) ⊆ M n z
d : ℕ → E
hd : DenseRange d
K : ℕ → ↑T → ℕ → Set E :=
  fun n z p ↦ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (M n z) ∩ closedBall (d p) (u n / 3)
K_approx : ∀ (n : ℕ) (z : ↑T) (p : ℕ), ApproximatesLinearOn f (f' ↑↑z) (s ∩ K n z p) (r (f' ↑↑z))
K_closed : ∀ (n : ℕ) (z : ↑T) (p : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (K n z p)
⊢ ∃ t A,
    (∀ (n : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (t n)) ∧
      s ⊆ ⋃ n, t n ∧
        (∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (r (A n))) ∧ (s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y)
Module: Mathlib.MeasureTheory.Function.Jacobian

Goal state before:
pp: E : Type u_1
F✝ : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : NormedAddCommGroup F✝
inst✝¹ : NormedSpace ℝ F✝
inst✝ : SecondCountableTopology F✝
f : E → F✝
s : Set E
f' : E → E →L[ℝ] F✝
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
r : (E →L[ℝ] F✝) → ℝ≥0
rpos : ∀ (A : E →L[ℝ] F✝), r A ≠ 0
hs : s.Nonempty
T : Set ↑s
T_count : T.Countable
hT : ⋃ x ∈ T, ball (f' ↑x) ↑(r (f' ↑x)) = ⋃ x, ball (f' ↑x) ↑(r (f' ↑x))
u : ℕ → ℝ
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
M : ℕ → ↑T → Set E :=
  fun n z ↦ {x | x ∈ s ∧ ∀ y ∈ s ∩ ball x (u n), ‖f y - f x - (f' ↑↑z) (y - x)‖ ≤ ↑(r (f' ↑↑z)) * ‖y - x‖}
s_subset : ∀ x ∈ s, ∃ n z, x ∈ M n z
closure_M_subset : ∀ (n : ℕ) (z : ↑T), s ∩ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (M n z) ⊆ M n z
d : ℕ → E
hd : DenseRange d
K : ℕ → ↑T → ℕ → Set E :=
  fun n z p ↦ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (M n z) ∩ closedBall (d p) (u n / 3)
K_approx : ∀ (n : ℕ) (z : ↑T) (p : ℕ), ApproximatesLinearOn f (f' ↑↑z) (s ∩ K n z p) (r (f' ↑↑z))
K_closed : ∀ (n : ℕ) (z : ↑T) (p : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (K n z p)
F : ℕ → ℕ × ↑T × ℕ
hF : Function.Surjective F
x : E
xs : x ∈ s
n : ℕ
z : ↑T
hnz : x ∈ M n z
p : ℕ
hp : x ∈ closedBall (d p) (u n / 3)
q : ℕ
hq : F q = (n, z, p)
⊢ x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (M n z)

Tactic:
exact subset_closure hnz

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 : ENNReal.ofReal |A.det| < ↑m
d : ℝ≥0∞ := ENNReal.ofReal |A.det|
HC : IsCompact (⇑A '' closedBall 0 1)
L0 : Tendsto (fun ε ↦ μ (cthickening ε (⇑A '' closedBall 0 1))) (𝓝[>] 0) (𝓝 (μ (⇑A '' closedBall 0 1)))
L1 : Tendsto (fun ε ↦ μ (closedBall 0 ε + ⇑A '' closedBall 0 1)) (𝓝[>] 0) (𝓝 (μ (⇑A '' closedBall 0 1)))
L2 : Tendsto (fun ε ↦ μ (closedBall 0 ε + ⇑A '' closedBall 0 1)) (𝓝[>] 0) (𝓝 (d * μ (closedBall 0 1)))
I : d * μ (closedBall 0 1) < ↑m * μ (closedBall 0 1)
H : ∀ᶠ (b : ℝ) in 𝓝[>] 0, μ (closedBall 0 b + ⇑A '' closedBall 0 1) < ↑m * μ (closedBall 0 1)
⊢ ∃ ε, μ (closedBall 0 ε + ⇑A '' closedBall 0 1) < ↑m * μ (closedBall 0 1) ∧ 0 < ε

Tactic:
exact (H.and self_mem_nhdsWithin).exists

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

Goal state before:
pp: E : Type u_1
f f' : ℝ → E
a : ℝ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a) volume
ε : ℝ
εpos : ε > 0
A : ∀ᶠ (n : ℕ) in atTop, ∫ (x : ℝ) in Ici ↑n, ‖f' x‖ < ε
B : ∀ᶠ (n : ℕ) in atTop, a < ↑n
N : ℕ
hN : ∫ (x : ℝ) in Ici ↑N, ‖f' x‖ < ε
h'N : a < ↑N
x : ℝ
hx : x ≥ ↑N
⊢ dist (f x) (f ↑N) < ε

Tactic:
calc
  dist (f x) (f ↑N)
    = ‖f x - f N‖ := dist_eq_norm _ _
  _ = ‖∫ t in Ioc ↑N x, f' t‖ := by
      rw [← intervalIntegral.integral_of_le hx, intervalIntegral.integral_eq_sub_of_hasDerivAt]
      · intro y hy
        simp only [hx, uIcc_of_le, mem_Icc] at hy
        exact hderiv _ (h'N.trans_le hy.1)
      · rw [intervalIntegrable_iff_integrableOn_Ioc_of_le hx]
        exact f'int.mono_set (Ioc_subset_Ioi_self.trans (Ioi_subset_Ioi h'N.le))
  _ ≤ ∫ t in Ioc ↑N x, ‖f' t‖ := norm_integral_le_integral_norm fun a ↦ f' a
  _ ≤ ∫ t in Ici ↑N, ‖f' t‖ := by
      apply setIntegral_mono_set
      · apply IntegrableOn.mono_set f'int.norm (Ici_subset_Ioi.2 h'N)
      · filter_upwards with x using norm_nonneg _
      · have : Ioc (↑N) x ⊆ Ici ↑N := Ioc_subset_Ioi_self.trans Ioi_subset_Ici_self
        exact this.eventuallyLE
  _ < ε := hN

Goal state after:
Module: Mathlib.Analysis.Calculus.LocalExtr.LineDeriv

Goal state before:
pp: E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
f : E → ℝ
a b : E
f' : ℝ
l : Filter E
h : IsExtrFilter f l a
hd : HasLineDerivAt ℝ f f' a b
h' : Tendsto (fun t ↦ a + t • b) (𝓝 0) l
⊢ IsExtrFilter f l (a + 0 • b)

Tactic:
by simpa using h

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
s : Set E
f : E → E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
A : E →L[ℝ] E
δ : ℝ≥0
hf : ApproximatesLinearOn f A s δ
hs : MeasurableSet s
f' : E → E →L[ℝ] E
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
x : E
hx : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)
xs : x ∈ s
z : E
ε : ℝ
εpos : 0 < ε
B₁ : ∀ᶠ (r : ℝ) in 𝓝[>] 0, (s ∩ ({x} + r • closedBall z ε)).Nonempty
ρ : ℝ
ρpos : ρ > 0
hρ : ball x ρ ∩ s ⊆ {y | ‖f y - f x - (f' x) (y - x)‖ ≤ ε * ‖y - x‖}
B₂ : ∀ᶠ (r : ℝ) in 𝓝[>] 0, {x} + r • closedBall z ε ⊆ ball x ρ
r : ℝ
y : E
ys : y ∈ s
hy : y ∈ {x} + r • closedBall z ε
rρ : {x} + r • closedBall z ε ⊆ ball x ρ
rpos : 0 < r
a : E
az : a ∈ closedBall z ε
ya : y = x + r • a
norm_a : ‖a‖ ≤ ‖z‖ + ε
I : r * ‖(f' x - A) a‖ ≤ r * (↑δ + ε) * (‖z‖ + ε)
⊢ ‖(f' x - A) z‖ ≤ (↑δ + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε

Tactic:
calc
    ‖(f' x - A) z‖ = ‖(f' x - A) a + (f' x - A) (z - a)‖ := by
      congr 1
      simp only [FunLike.coe_sub, map_sub, Pi.sub_apply]
      abel
    _ ≤ ‖(f' x - A) a‖ + ‖(f' x - A) (z - a)‖ := norm_add_le _ _
    _ ≤ (δ + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ‖z - a‖ := by
      apply add_le_add
      · rw [mul_assoc] at I; exact (mul_le_mul_iff_right₀ rpos).1 I
      · apply ContinuousLinearMap.le_opNorm
    _ ≤ (δ + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε := by
      rw [mem_closedBall_iff_norm'] at az
      gcongr

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : ℝ → E
a : ℝ
⊢ ∫ (y : ℝ) in Ioi (rexp a), g y = ∫ (x : ℝ) in Ioi a, rexp x • g (rexp x)

Tactic:
rw [← image_exp_Ioi]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : ℝ → E
a : ℝ
⊢ ∫ (y : ℝ) in rexp '' Ioi a, g y = ∫ (x : ℝ) in Ioi a, rexp x • g (rexp x)
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : ℝ → E
a : ℝ
⊢ IntegrableOn g (Ioi (rexp a)) volume ↔ IntegrableOn (fun x ↦ rexp x • g (rexp x)) (Ioi a) volume

Tactic:
rw [← image_exp_Ioi]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : ℝ → E
a : ℝ
⊢ IntegrableOn g (rexp '' Ioi a) volume ↔ IntegrableOn (fun x ↦ rexp x • g (rexp x)) (Ioi a) volume
Module: Mathlib.Analysis.Complex.LocallyUniformLimit

Goal state before:
pp: E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
U : Set ℂ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
inst✝ : CompleteSpace E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
⊢ TendstoLocallyUniformlyOn (_root_.deriv ∘ F) (_root_.deriv f) φ U

Tactic:
rw [tendstoLocallyUniformlyOn_iff_forall_isCompact hU]
  rcases φ.eq_or_neBot with rfl | hne
  · simp only [TendstoUniformlyOn, eventually_bot, imp_true_iff]
  rintro K hKU hK
  obtain ⟨δ, hδ, hK4, h⟩ := exists_cthickening_tendstoUniformlyOn hf hF hK hU hKU
  refine h.congr_right fun z hz => cderiv_eq_deriv hU (hf.differentiableOn hF hU) hδ ?_
  exact (closedBall_subset_cthickening hz δ).trans hK4

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

Goal state before:
pp: H : Type u
M : Type u_2
M' : Type u_3
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
x' : M'
⊢ chartAt H (Sum.inr x') = (chartAt H x').lift_openEmbedding ⋯

Tactic:
simp +instances only [chartAt, sum, nonempty_of_chartedSpace x', ↓reduceDIte]

Goal state after:
H : Type u
M : Type u_2
M' : Type u_3
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
x' : M'
⊢ ChartedSpace.chartAt (Sum.inr x') = (ChartedSpace.chartAt x').lift_openEmbedding ⋯
Module: Mathlib.Geometry.Manifold.ChartedSpace

Goal state before:
pp: H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : TopologicalSpace M'
inst✝¹ : TopologicalSpace H
inst✝ : ChartedSpace H M
f : M → M'
hf : IsLocalHomeomorph f
g : M' → M
hg : Function.RightInverse g f
q : M'
⊢ q ∈ (hf.localInverseAt (g q) ≫ₕ chartAt H (g q)).source

Tactic:
nth_rw 3 [← hg.eq q]
    simp

Goal state after: