mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x_1 : E) in 𝓝[interior s] x, ‖f' x_1 - f' x - f'' (x_1 - x)‖ ≤ c * ‖x_1 - x‖
v w : E
hv : x + v ∈ interior s
hw : x + v + w ∈ interior s
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : δ > 0
sδ : Metric.ball x δ ∩ interior s ⊆ {x_1 | (fun x_2 ↦ ‖f' x_2 - f' x - f'' (x_2 - x)‖ ≤ ε * ‖x_2 - x‖) x_1}
E1 : ∀ᶠ (h : ℝ) in 𝓝[>] 0, h * (‖v‖ + ‖w‖) < δ
E2 : ∀ᶠ (h : ℝ) in 𝓝[>] 0, h < 1
h : ℝ
hδ : h * (‖v‖ + ‖w‖) < δ
h_lt_1 : h < 1
hpos : 0 < h
xt_mem : ∀ t ∈ Icc 0 1, x + h • v + (t * h) • w ∈ interior s
g : ℝ → F :=
  fun t ↦ f (x + h • v + (t * h) • w) - (t * h) • (f' x) w - (t * h ^ 2) • (f'' v) w - ((t * h) ^ 2 / 2) • (f'' w) w
g' : ℝ → F :=
  fun t ↦ (f' (x + h • v + (t * h) • w)) (h • w) - h • (f' x) w - h ^ 2 • (f'' v) w - (t * h ^ 2) • (f'' w) w
hg' : g' = fun t ↦ (f' (x + h • v + (t * h) • w)) (h • w) - h • (f' x) w - h ^ 2 • (f'' v) w - (t * h ^ 2) • (f'' w) w
t : ℝ
ht : t ∈ Icc 0 1
H :
  HasDerivWithinAt (fun u ↦ ((u * h) ^ 2 / 2) • (f'' w) w) ((↑2 * (t * h) ^ (2 - 1) * (1 * h) / 2) • (f'' w) w)
    (Icc 0 1) t
⊢ HasDerivWithinAt (fun t ↦ ((t * h) ^ 2 / 2) • (f'' w) w) ((t * h ^ 2) • (f'' w) w) (Icc 0 1) t

Tactic:
convert H
        ring

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
V W : E → E
x : E
hV : V x = 0
hW : W x = 0
⊢ lieBracket 𝕜 V W x = 0

Tactic:
by
  simp [lieBracket, hV, hW]

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
s : Set E
x : E
h'f : ContDiffWithinAt 𝕜 2 f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
M : E ≃L[𝕜] F
hM : ↑M = fderivWithin 𝕜 f s x
U : Set E := {y | ∃ N, ↑N = fderivWithin 𝕜 f s y}
hU : U ∈ 𝓝[s] x
N : E → E ≃L[𝕜] F := fun x ↦ if h : x ∈ U then Exists.choose h else M
eN : (fun y ↦ ↑(N y)) =ᶠ[𝓝[s] x] fun y ↦ fderivWithin 𝕜 f s y
⊢ ∃ 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:
have e'N : N x = fderivWithin 𝕜 f s x := by apply mem_of_mem_nhdsWithin hx eN

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
s : Set E
x : E
h'f : ContDiffWithinAt 𝕜 2 f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
M : E ≃L[𝕜] F
hM : ↑M = fderivWithin 𝕜 f s x
U : Set E := {y | ∃ N, ↑N = fderivWithin 𝕜 f s y}
hU : U ∈ 𝓝[s] x
N : E → E ≃L[𝕜] F := fun x ↦ if h : x ∈ U then Exists.choose h else M
eN : (fun y ↦ ↑(N y)) =ᶠ[𝓝[s] x] fun y ↦ fderivWithin 𝕜 f s y
e'N : ↑(N x) = fderivWithin 𝕜 f s x
⊢ ∃ 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
Module: Mathlib.Analysis.Calculus.DifferentialForm.VectorField

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 : ℕ
x : E
ω : E → E [⋀^Fin n]→L[𝕜] F
V : Fin (n + 1) → E → E
hω : DifferentiableAt 𝕜 ω x
hV : ∀ (i : Fin (n + 1)), DifferentiableAt 𝕜 (V i) x
hcomm : Pairwise fun i j ↦ lieBracket 𝕜 (V i) (V j) x = 0
⊢ ((extDeriv ω x) fun x_1 ↦ V x_1 x) =
    ∑ i, (-1) ^ ↑i • (fderiv 𝕜 (fun x ↦ (ω x) (i.removeNth fun x_1 ↦ V x_1 x)) x) (V i x)

Tactic:
simp only [← differentiableWithinAt_univ, ← lieBracketWithin_univ, ← extDerivWithin_univ,
    ← fderivWithin_univ] at *

Goal state after:
𝕜 : 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 : ℕ
x : E
ω : E → E [⋀^Fin n]→L[𝕜] F
V : Fin (n + 1) → E → E
hω : DifferentiableWithinAt 𝕜 ω Set.univ x
hV : ∀ (i : Fin (n + 1)), DifferentiableWithinAt 𝕜 (V i) Set.univ x
hcomm : Pairwise fun i j ↦ lieBracketWithin 𝕜 (V i) (V j) Set.univ x = 0
⊢ ((extDerivWithin ω Set.univ x) fun x_1 ↦ V x_1 x) =
    ∑ x_1, (-1) ^ ↑x_1 • (fderivWithin 𝕜 (fun x ↦ (ω x) (x_1.removeNth fun x_2 ↦ V x_2 x)) Set.univ x) (V x_1 x)
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
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
M : E ≃L[𝕜] F
hM : ↑M = fderivWithin 𝕜 f s x
U : Set E := {y | ∃ N, ↑N = fderivWithin 𝕜 f s y}
hU : U ∈ 𝓝[s] x
N : E → E ≃L[𝕜] F := fun x ↦ if h : x ∈ U then Exists.choose h else M
eN : (fun y ↦ ↑(N y)) =ᶠ[𝓝[s] x] fun y ↦ fderivWithin 𝕜 f s y
e'N : ↑(N x) = fderivWithin 𝕜 f s x
hN : ContDiffWithinAt 𝕜 1 (fun y ↦ ↑(N y)) s x
hN' : ContDiffWithinAt 𝕜 1 (fun y ↦ ↑(N y).symm) s x
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:
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

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
s : Set E
x : E
h'f : ContDiffWithinAt 𝕜 2 f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
M : E ≃L[𝕜] F
hM : ↑M = fderivWithin 𝕜 f s x
U : Set E := {y | ∃ N, ↑N = fderivWithin 𝕜 f s y}
hU : U ∈ 𝓝[s] x
N : E → E ≃L[𝕜] F := fun x ↦ if h : x ∈ U then Exists.choose h else M
eN : (fun y ↦ ↑(N y)) =ᶠ[𝓝[s] x] fun y ↦ fderivWithin 𝕜 f s y
e'N : ↑(N x) = fderivWithin 𝕜 f s x
hN : ContDiffWithinAt 𝕜 1 (fun y ↦ ↑(N y)) s x
hN' : ContDiffWithinAt 𝕜 1 (fun y ↦ ↑(N y).symm) s x
v : E
A' : ∀ (y : E), ((ContinuousLinearMap.compL 𝕜 F E F) ↑(N y)) ↑(N y).symm = ContinuousLinearMap.id 𝕜 F
⊢ (fderivWithin 𝕜 (fun y ↦ ↑(N y).symm) s x) v =
    -↑(N x).symm ∘SL (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) v ∘SL ↑(N x).symm
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✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : E → F
x v : E
c : 𝕜
⊢ lineDeriv 𝕜 f x (c • v) = c • lineDeriv 𝕜 f x v

Tactic:
rcases eq_or_ne c 0 with rfl | hc

Goal state after:
case inl
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : E → F
x v : E
⊢ lineDeriv 𝕜 f x (0 • v) = 0 • lineDeriv 𝕜 f x v

case inr
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : E → F
x v : E
c : 𝕜
hc : c ≠ 0
⊢ lineDeriv 𝕜 f x (c • v) = c • lineDeriv 𝕜 f x v
Module: Mathlib.Analysis.Calculus.FDeriv.Norm

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
hn : n ≠ 0
h : ContDiffAt ℝ n (fun x ↦ ‖x‖) (0 • x)
this : Subsingleton E
⊢ ContDiffAt ℝ n (fun x ↦ ‖x‖) x

Tactic:
eq_const_of_subsingleton (‖·‖) 0

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
hn : n ≠ 0
h : ContDiffAt ℝ n (fun x ↦ ‖x‖) (0 • x)
this : Subsingleton E
⊢ ContDiffAt ℝ n (Function.const E ‖0‖) x
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 → 𝕜
x : F
h : ¬DifferentiableAt 𝕜 f x
⊢ ∇ f x = 0

Tactic:
gradient,

Goal state after:
𝕜 : Type u_1
F : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : CompleteSpace F
f : F → 𝕜
x : F
h : ¬DifferentiableAt 𝕜 f x
⊢ (toDual 𝕜 F).symm (fderiv 𝕜 f x) = 0
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 → 𝕜
x : F
⊢ (toDual 𝕜 F) (∇ f x) = fderiv 𝕜 f x

Tactic:
gradient,

Goal state after:
𝕜 : Type u_1
F : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : CompleteSpace F
f : F → 𝕜
x : F
⊢ (toDual 𝕜 F) ((toDual 𝕜 F).symm (fderiv 𝕜 f x)) = fderiv 𝕜 f x
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 → 𝕜
x y : F
⊢ ⟪∇ f x, y⟫ = (fderiv 𝕜 f x) y

Tactic:
simp [← gradientWithin_univ]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
g : 𝕜 → E
f : 𝕜 → 𝕜
s t : Set 𝕜
x : 𝕜
hg : ContDiffWithinAt 𝕜 3 g t (f x)
hf : ContDiffWithinAt 𝕜 3 f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
⊢ ((iteratedFDerivWithin 𝕜 3 g t (f x)) fun x_1 ↦ derivWithin f s x) +
          (iteratedFDerivWithin 𝕜 2 g t (f x)) ![iteratedDerivWithin 2 f s x, derivWithin f s x] +
        2 • (iteratedFDerivWithin 𝕜 2 g t (f x)) ![derivWithin f s x, iteratedDerivWithin 2 f s x] +
      (fderivWithin 𝕜 g t (f x)) (iteratedDerivWithin 3 f s x) =
    derivWithin f s x ^ 3 • iteratedDerivWithin 3 g t (f x) +
        3 • iteratedDerivWithin 2 f s x • derivWithin f s x • iteratedDerivWithin 2 g t (f x) +
      iteratedDerivWithin 3 f s x • derivWithin g t (f x)

Tactic:
simp [← toSpanSingleton_derivWithin, mul_smul, smul_comm (iteratedDerivWithin 2 f s x),
        iteratedFDerivWithin_apply_eq_iteratedDerivWithin_mul_prod]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
g : 𝕜 → E
f : 𝕜 → 𝕜
s t : Set 𝕜
x : 𝕜
hg : ContDiffWithinAt 𝕜 3 g t (f x)
hf : ContDiffWithinAt 𝕜 3 f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
⊢ derivWithin f s x ^ 3 • iteratedDerivWithin 3 g t (f x) +
        derivWithin f s x • iteratedDerivWithin 2 f s x • iteratedDerivWithin 2 g t (f x) +
      2 • derivWithin f s x • iteratedDerivWithin 2 f s x • iteratedDerivWithin 2 g t (f x) =
    derivWithin f s x ^ 3 • iteratedDerivWithin 3 g t (f x) +
      3 • derivWithin f s x • iteratedDerivWithin 2 f s x • iteratedDerivWithin 2 g t (f x)
Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
g : 𝕜 → E
f : 𝕜 → 𝕜
x : 𝕜
hg : ContDiffAt 𝕜 3 g (f x)
hf : ContDiffAt 𝕜 3 f x
⊢ iteratedDerivWithin 3 (g ∘ f) univ x =
    derivWithin f univ x ^ 3 • iteratedDerivWithin 3 g univ (f x) +
        3 • iteratedDerivWithin 2 f univ x • derivWithin f univ x • iteratedDerivWithin 2 g univ (f x) +
      iteratedDerivWithin 3 f univ x • derivWithin g univ (f x)

Tactic:
exact iteratedDerivWithin_scomp_three hg hf uniqueDiffOn_univ uniqueDiffOn_univ (mem_univ _)
    (mapsTo_univ _ _)

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : CompleteSpace 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : FiniteDimensional 𝕜 F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : (↑f').range = ⊤
α : Type u_4
l : Filter α
g₁ : α → F
g₂ : α → ↥(↑f').ker
h₁ : Tendsto g₁ l (𝓝 (f a))
h₂ : Tendsto g₂ l (𝓝 0)
⊢ Tendsto (fun t ↦ (g₁ t, g₂ t)) l (𝓝 (f a, 0))

Tactic:
exact h₁.prodMk_nhds h₂

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

Goal state before:
pp: case intro.refine_2
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
φ : E → ℝ
x₀ : E
φ' : StrongDual ℝ E
ι : Type u_3
inst✝ : Finite ι
f : ι → E → ℝ
f' : ι → StrongDual ℝ E
hextr : IsLocalExtrOn φ {x | ∀ (i : ι), f i x = f i x₀} x₀
hf' : ∀ (i : ι), HasStrictFDerivAt (f i) (f' i) x₀
hφ' : HasStrictFDerivAt φ φ' x₀
val✝ : Fintype ι
Λ : ι → ℝ
Λ₀ : ℝ
hΛ : (Λ, Λ₀) ≠ 0
hΛf : ∑ i, Λ i • f' i + Λ₀ • φ' = 0
⊢ ∃ i, Option.elim' Λ₀ Λ i ≠ 0

Tactic:
· simpa only [funext_iff, not_and_or, or_comm, Option.exists, Prod.mk_eq_zero, Ne,
      not_forall] using! hΛ

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

Goal state before:
pp: a b : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hab : a < b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfa : Tendsto f (𝓝[>] a) (𝓝 0)
hga : Tendsto g (𝓝[>] a) (𝓝 0)
hdiv : Tendsto (fun x ↦ f' x / g' x) (𝓝[>] a) l
sub : ∀ x ∈ Ioo a b, Ioo a x ⊆ Ioo a b
hg : ∀ x ∈ Ioo a b, g x ≠ 0
c : ℝ → ℝ
hc : ∀ x ∈ Ioo a b, c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)
this : ∀ x ∈ Ioo a b, ((fun x' ↦ f' x' / g' x') ∘ c) x = f x / g x
⊢ Tendsto (fun x ↦ f x / g x) (𝓝[>] a) l

Tactic:
have cmp : ∀ x ∈ Ioo a b, a < c x ∧ c x < x := fun x hx ↦ (hc x hx).1

Goal state after:
a b : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hab : a < b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfa : Tendsto f (𝓝[>] a) (𝓝 0)
hga : Tendsto g (𝓝[>] a) (𝓝 0)
hdiv : Tendsto (fun x ↦ f' x / g' x) (𝓝[>] a) l
sub : ∀ x ∈ Ioo a b, Ioo a x ⊆ Ioo a b
hg : ∀ x ∈ Ioo a b, g x ≠ 0
c : ℝ → ℝ
hc : ∀ x ∈ Ioo a b, c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)
this : ∀ x ∈ Ioo a b, ((fun x' ↦ f' x' / g' x') ∘ c) x = f x / g x
cmp : ∀ x ∈ Ioo a b, a < c x ∧ c x < x
⊢ Tendsto (fun x ↦ f x / g x) (𝓝[>] a) l
Module: Mathlib.MeasureTheory.Function.JacobianOneDim

Goal state before:
pp: s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf : MonotoneOn f s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : Set ℝ := {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}
a_count : a.Countable
s₁ : Set ℝ := s \ a
hs₁ : MeasurableSet s₁
u : Set ℝ := {c | ∃ x y, x ∈ s₁ ∧ y ∈ s₁ ∧ x < y ∧ f x = c ∧ f y = c}
hu : u.Countable
b : Set ℝ := s₁ ∩ f ⁻¹' u
hb : MeasurableSet b
⊢ ∃ a b c,
    a ∪ (b ∪ c) = s ∧
      MeasurableSet a ∧
        MeasurableSet b ∧
          MeasurableSet c ∧
            Disjoint a (b ∪ c) ∧
              Disjoint b c ∧ a.Countable ∧ (f '' b).Countable ∧ (∀ x ∈ b, f' x = 0) ∧ (∀ x ∈ c, 0 ≤ f' x) ∧ InjOn f c

Tactic:
let c := s₁ \ b

Goal state after:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf : MonotoneOn f s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : Set ℝ := {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}
a_count : a.Countable
s₁ : Set ℝ := s \ a
hs₁ : MeasurableSet s₁
u : Set ℝ := {c | ∃ x y, x ∈ s₁ ∧ y ∈ s₁ ∧ x < y ∧ f x = c ∧ f y = c}
hu : u.Countable
b : Set ℝ := s₁ ∩ f ⁻¹' u
hb : MeasurableSet b
c : Set ℝ := s₁ \ b
⊢ ∃ a b c,
    a ∪ (b ∪ c) = s ∧
      MeasurableSet a ∧
        MeasurableSet b ∧
          MeasurableSet c ∧
            Disjoint a (b ∪ c) ∧
              Disjoint b c ∧ a.Countable ∧ (f '' b).Countable ∧ (∀ x ∈ b, f' x = 0) ∧ (∀ x ∈ c, 0 ≤ f' x) ∧ InjOn f c
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
H : ∀ (ε : ℝ), 0 < ε → ‖(f' x - A) z‖ ≤ (↑δ + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε
this : Tendsto (fun ε ↦ (↑δ + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε) (𝓝[>] 0) (𝓝 ((↑δ + 0) * (‖z‖ + 0) + ‖f' x - A‖ * 0))
⊢ ‖(f' x - A) z‖ ≤ ↑δ * ‖z‖

Tactic:
simp only [add_zero, mul_zero] at this

Goal state after:
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
H : ∀ (ε : ℝ), 0 < ε → ‖(f' x - A) z‖ ≤ (↑δ + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε
this : Tendsto (fun ε ↦ (↑δ + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε) (𝓝[>] 0) (𝓝 (↑δ * ‖z‖))
⊢ ‖(f' x - A) z‖ ≤ ↑δ * ‖z‖
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: g g' : ℝ → ℝ
a l : ℝ
hcont : ContinuousWithinAt g (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
g'neg : ∀ x ∈ Ioi a, g' x ≤ 0
hg : Tendsto g atTop (𝓝 l)
⊢ IntegrableOn g' (Ioi a) volume

Tactic:
apply integrable_neg_iff.1
  exact integrableOn_Ioi_deriv_of_nonneg hcont.neg (fun x hx => (hderiv x hx).neg)
    (fun x hx => neg_nonneg_of_nonpos (g'neg x hx)) hg.neg

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : LocallyCompactSpace 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : OpensMeasurableSpace E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace F
f : E → F
inst✝ : SecondCountableTopology E
hf : Continuous f
this✝¹ : MeasurableSpace 𝕜 := borel 𝕜
this✝ : BorelSpace 𝕜
g : E × E → 𝕜 → F := fun p t ↦ f (p.1 + t • p.2)
this : Continuous (Function.uncurry g)
M_meas : MeasurableSet {q | DifferentiableAt 𝕜 (g q.1) q.2}
⊢ MeasurableSet {p | LineDifferentiableAt 𝕜 f p.1 p.2}

Tactic:
exact measurable_prodMk_right M_meas

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

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 H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
⊢ HasGroupoid M (continuousGroupoid H)

Tactic:
refine ⟨fun _ _ ↦ ?_⟩

Goal state after:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
e✝ e'✝ : OpenPartialHomeomorph M H
x✝¹ : e✝ ∈ atlas H M
x✝ : e'✝ ∈ atlas H M
⊢ e✝.symm ≫ₕ e'✝ ∈ continuousGroupoid H
Module: Mathlib.Geometry.Manifold.StructureGroupoid

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

Tactic:
simp [mem_singleton_iff.mp E]

Goal state after:
Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s : Set M
hs : s ⊆ f.source
⊢ ↑I ∘ ↑f '' s ⊆ ↑f.symm ∘ ↑I.symm ⁻¹' s ∩ range ↑I

Tactic:
preimage_comp,

Goal state after:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s : Set M
hs : s ⊆ f.source
⊢ ↑I ∘ ↑f '' s ⊆ ↑I.symm ⁻¹' ↑f.symm ⁻¹' s ∩ range ↑I
Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s : Set M
y : M
hy : y ∈ f.source
⊢ map (↑(f.extend I).symm) (𝓝[↑(f.extend I).symm ⁻¹' s ∩ range ↑I] ↑(f.extend I) y) = 𝓝[s] y

Tactic:
by
  rw [← map_extend_nhdsWithin f hy, map_map, Filter.map_congr, map_id]
  exact (f.extend I).leftInvOn.eqOn.eventuallyEq_of_mem (extend_source_mem_nhdsWithin _ hy)

Goal state after:
Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst✝ : ChartedSpace H M
he : e ∈ maximalAtlas I n M
he' : e' ∈ maximalAtlas I n M
⊢ ContDiffOn 𝕜 n (↑(extendCoordChange e e')) (extendCoordChange e e').source

Tactic:
rw [I.extendCoordChange_source, I.image_eq]

Goal state after:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst✝ : ChartedSpace H M
he : e ∈ maximalAtlas I n M
he' : e' ∈ maximalAtlas I n M
⊢ ContDiffOn 𝕜 n (↑(extendCoordChange e e')) (↑I.symm ⁻¹' (e.symm ≫ₕ e').source ∩ range ↑I)
Module: Mathlib.Geometry.Manifold.LocalInvariantProperties

Goal state before:
pp: H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
P : (H → H') → Set H → H → Prop
g : M → M'
s t : Set M
x : M
mono_of_mem_nhdsWithin : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, s ∈ 𝓝[t] x → P f s x → P f t x
hst : s ∈ 𝓝[t] x
h :
  ContinuousWithinAt g s x ∧
    P (↑(chartAt H' (g x)) ∘ g ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) x)
⊢ ↑(chartAt H x).symm ⁻¹' s ∈ 𝓝[↑(chartAt H x).symm ⁻¹' t] ↑(chartAt H x) x

Tactic:
simp_rw [← mem_map, (chartAt H x).symm.map_nhdsWithin_preimage_eq (mem_chart_target H x),
    (chartAt H x).left_inv (mem_chart_source H x), hst]

Goal state after:
Module: Mathlib.Geometry.Manifold.IsManifold.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
n : ℕ∞ω
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
⊢ IsManifold I 0 M

Tactic:
suffices HasGroupoid M (contDiffGroupoid 0 I) from mk' I 0 M

Goal state after:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
n : ℕ∞ω
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
⊢ HasGroupoid M (contDiffGroupoid 0 I)