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
V W V₁ : E → E
s : Set E
x : E
hV : DifferentiableWithinAt 𝕜 V s x
hV₁ : DifferentiableWithinAt 𝕜 V₁ s x
hs : UniqueDiffWithinAt 𝕜 s x
⊢ lieBracketWithin 𝕜 (V + V₁) W s x = lieBracketWithin 𝕜 V W s x + lieBracketWithin 𝕜 V₁ W s x

Tactic:
simp only [lieBracketWithin, Pi.add_apply, map_add]

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W V₁ : E → E
s : Set E
x : E
hV : DifferentiableWithinAt 𝕜 V s x
hV₁ : DifferentiableWithinAt 𝕜 V₁ s x
hs : UniqueDiffWithinAt 𝕜 s x
⊢ (fderivWithin 𝕜 W s x) (V x) + (fderivWithin 𝕜 W s x) (V₁ x) - (fderivWithin 𝕜 (V + V₁) s x) (W x) =
    (fderivWithin 𝕜 W s x) (V x) - (fderivWithin 𝕜 V s x) (W x) +
      ((fderivWithin 𝕜 W s x) (V₁ x) - (fderivWithin 𝕜 V₁ s x) (W 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
V W V₁ : E → E
x : E
hV : DifferentiableAt 𝕜 V x
hV₁ : DifferentiableAt 𝕜 V₁ x
⊢ lieBracket 𝕜 (V + V₁) W x = lieBracket 𝕜 V W x + lieBracket 𝕜 V₁ W x

Tactic:
by
  simp only [lieBracket, Pi.add_apply, map_add]
  rw [fderiv_add hV hV₁, add_apply]
  abel

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 W₁ : E → E
s : Set E
x : E
hW : DifferentiableWithinAt 𝕜 W s x
hW₁ : DifferentiableWithinAt 𝕜 W₁ s x
hs : UniqueDiffWithinAt 𝕜 s x
⊢ lieBracketWithin 𝕜 V (W + W₁) s x = lieBracketWithin 𝕜 V W s x + lieBracketWithin 𝕜 V W₁ s x

Tactic:
simp only [lieBracketWithin, Pi.add_apply, map_add]

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W W₁ : E → E
s : Set E
x : E
hW : DifferentiableWithinAt 𝕜 W s x
hW₁ : DifferentiableWithinAt 𝕜 W₁ s x
hs : UniqueDiffWithinAt 𝕜 s x
⊢ (fderivWithin 𝕜 (W + W₁) s x) (V x) - ((fderivWithin 𝕜 V s x) (W x) + (fderivWithin 𝕜 V s x) (W₁ x)) =
    (fderivWithin 𝕜 W s x) (V x) - (fderivWithin 𝕜 V s x) (W x) +
      ((fderivWithin 𝕜 W₁ s x) (V x) - (fderivWithin 𝕜 V s x) (W₁ x))
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
v : E
f : E → F
f' : F
x₀ : E
hf : HasLineDerivAt 𝕜 f f' x₀ v
s : Set E
hs : s ∈ 𝓝 x₀
C : ℝ≥0
hlip : LipschitzOnWith C f s
⊢ ‖f'‖ ≤ ↑C * ‖v‖

Tactic:
refine hf.le_of_lip' C.coe_nonneg ?_
  filter_upwards [hs] with x hx using hlip.norm_sub_le hx (mem_of_mem_nhds hs)

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 y : E
hy : y ∈ interior s
z : E
hz : z = (1 / 4) • (y - x)
A : ∀ (m : E), Tendsto (fun t ↦ x + 4 • (z + t • m)) (𝓝 0) (𝓝 y)
m : E
⊢ interior s ∈ 𝓝 y

Tactic:
mem_interior_iff_mem_nhds

Goal state after:
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 y : E
hy : s ∈ 𝓝 y
z : E
hz : z = (1 / 4) • (y - x)
A : ∀ (m : E), Tendsto (fun t ↦ x + 4 • (z + t • m)) (𝓝 0) (𝓝 y)
m : E
⊢ interior s ∈ 𝓝 y
Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n : ℕ∞ω
m : ℕ
hm : minSmoothness 𝕜 ↑m ≤ n
⊢ ∃ n', minSmoothness 𝕜 ↑m ≤ n' ∧ n' ≤ n ∧ n' ≠ ∞

Tactic:
by
  simp only [minSmoothness] at hm ⊢
  split_ifs with h
  · simp only [h, ↓reduceIte] at hm
    exact ⟨m, le_rfl, hm, by simp⟩
  · simp only [h, ↓reduceIte] at hm
    refine ⟨ω, le_rfl, by simp [hm], by simp⟩

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)
this : ContinuousOn (fderivWithin 𝕜 (fderivWithin 𝕜 f (s ∩ u)) (s ∩ u)) (s ∩ u)
y : E
hy : y ∈ s ∩ u
z : E
hz : z ∈ u
⊢ s z = (s ∩ u) z

Tactic:
change (z ∈ s) = (z ∈ s ∩ u)

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)
this : ContinuousOn (fderivWithin 𝕜 (fderivWithin 𝕜 f (s ∩ u)) (s ∩ u)) (s ∩ u)
y : E
hy : y ∈ s ∩ u
z : E
hz : z ∈ u
⊢ (z ∈ s) = (z ∈ s ∩ u)
Module: Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain

Goal state before:
pp: case h
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E₁ : Type u_2
inst✝⁸ : NormedAddCommGroup E₁
inst✝⁷ : NormedSpace 𝕜 E₁
inst✝⁶ : CompleteSpace E₁
E₂ : Type u_3
inst✝⁵ : NormedAddCommGroup E₂
inst✝⁴ : NormedSpace 𝕜 E₂
inst✝³ : CompleteSpace E₂
F : Type u_4
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
u : E₁ × E₂
f : E₁ × E₂ → F
f'u : E₁ × E₂ →L[𝕜] F
dfu : HasStrictFDerivAt f f'u u
if₂u : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible
v : E₁ × E₂
y : E₂
hy : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂) y = f'u v
⊢ v - (0, y) ∈ (↑f'u).ker ∧ (0, y) ∈ (↑(ContinuousLinearMap.fst 𝕜 E₁ E₂)).ker ∧ v - (0, y) + (0, y) = v

Tactic:
aesop

Goal state after:
Module: Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E₁ : Type u_2
inst✝⁸ : NormedAddCommGroup E₁
inst✝⁷ : NormedSpace 𝕜 E₁
inst✝⁶ : CompleteSpace E₁
E₂ : Type u_3
inst✝⁵ : NormedAddCommGroup E₂
inst✝⁴ : NormedSpace 𝕜 E₂
inst✝³ : CompleteSpace E₂
F : Type u_4
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
u : E₁ × E₂
f : E₁ × E₂ → F
f'u : E₁ × E₂ →L[𝕜] F
dfu : HasStrictFDerivAt f f'u u
if₂u : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible
φ : ImplicitFunctionData 𝕜 (E₁ × E₂) F E₁ := dfu.implicitFunctionDataOfProdDomain if₂u
v : E₁ × E₂
h : φ.leftFun v = φ.leftFun φ.pt ↔ φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun v) = v
x✝ : φ.rightFun (φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun v)) = φ.rightFun v
⊢ dfu.implicitFunctionOfProdDomain if₂u v.1 = v.2 → φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun v) = v

Tactic:
aesop

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

Goal state before:
pp: a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ x ∈ Iio a, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Iio a, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Iio a, g' x ≠ 0
hfbot : Tendsto f atBot (𝓝 0)
hgbot : Tendsto g atBot (𝓝 0)
hdiv : Tendsto (fun x ↦ f' x / g' x) atBot l
hdnf : ∀ x ∈ -Iio a, HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ x ∈ -Iio a, HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
⊢ Tendsto (fun x ↦ f x / g x) atBot l

Tactic:
neg_Iio

Goal state after:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ x ∈ Iio a, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Iio a, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Iio a, g' x ≠ 0
hfbot : Tendsto f atBot (𝓝 0)
hgbot : Tendsto g atBot (𝓝 0)
hdiv : Tendsto (fun x ↦ f' x / g' x) atBot l
hdnf : ∀ x ∈ Ioi (-a), HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ x ∈ Ioi (-a), HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
⊢ Tendsto (fun x ↦ f x / g x) atBot 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
c : Set ℝ := s₁ \ b
hc : MeasurableSet c
x : ℝ
hx : x ∈ b
p : ℝ
ps₁ : p ∈ s₁
px✝ : p ≠ x
fpx : f p = f x
px : p < x
K : HasDerivWithinAt f 0 (s ∩ Ioo p x) x
K' : HasDerivWithinAt f (f' x) (s ∩ Ioo p x) x
J1 : (s ∩ Ioo p x) \ {x} = s ∩ Ioo p x
J2 : 𝓝[s ∩ Ioo p x] x = 𝓝[s ∩ Iio x] x
⊢ (𝓝[s ∩ Ioo p x] x).NeBot

Tactic:
J2

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
hc : MeasurableSet c
x : ℝ
hx : x ∈ b
p : ℝ
ps₁ : p ∈ s₁
px✝ : p ≠ x
fpx : f p = f x
px : p < x
K : HasDerivWithinAt f 0 (s ∩ Ioo p x) x
K' : HasDerivWithinAt f (f' x) (s ∩ Ioo p x) x
J1 : (s ∩ Ioo p x) \ {x} = s ∩ Ioo p x
J2 : 𝓝[s ∩ Ioo p x] x = 𝓝[s ∩ Iio x] x
⊢ (𝓝[s ∩ Iio x] x).NeBot
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
c : Set ℝ := s₁ \ b
hc : MeasurableSet c
x : ℝ
hx : x ∈ b
p : ℝ
ps₁ : p ∈ s₁
px✝ : p ≠ x
fpx : f p = f x
px : x < p
K : HasDerivWithinAt f 0 (s ∩ Ioo x p) x
K' : HasDerivWithinAt f (f' x) (s ∩ Ioo x p) x
J1 : (s ∩ Ioo x p) \ {x} = s ∩ Ioo x p
J2 : 𝓝[s ∩ Ioo x p] x = 𝓝[s ∩ Ioi x] x
⊢ (𝓝[s ∩ Ioo x p] x).NeBot

Tactic:
J2

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
hc : MeasurableSet c
x : ℝ
hx : x ∈ b
p : ℝ
ps₁ : p ∈ s₁
px✝ : p ≠ x
fpx : f p = f x
px : x < p
K : HasDerivWithinAt f 0 (s ∩ Ioo x p) x
K' : HasDerivWithinAt f (f' x) (s ∩ Ioo x p) x
J1 : (s ∩ Ioo x p) \ {x} = s ∩ Ioo x p
J2 : 𝓝[s ∩ Ioo x p] x = 𝓝[s ∩ Ioi x] x
⊢ (𝓝[s ∩ Ioi x] x).NeBot
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts

Goal state before:
pp: a b : ℝ
f f' g : ℝ → ℝ
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioo (min a b) (max a b))
hg1 : IntegrableOn g (f '' [[a, b]]) volume
hg2 : IntegrableOn (fun x ↦ (g ∘ f) x * f' x) [[a, b]] volume
hg2' : IntegrableOn (fun x ↦ f' x • (g ∘ f) x) [[a, b]] volume
⊢ ∫ (x : ℝ) in a..b, (g ∘ f) x * f' x = ∫ (u : ℝ) in f a..f b, g u

Tactic:
simpa [mul_comm] using integral_deriv_smul_comp''' hf hff' hg_cont hg1 hg2'

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
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
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)
⊢ Measurable fun p ↦ lineDeriv 𝕜 f p.1 p.2

Tactic:
exact (measurable_deriv_with_param this).comp measurable_prodMk_right

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

Goal state before:
pp: E : Type u_1
f f' : ℝ → E
a : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont✝ : ContinuousWithinAt f (Iic a) a
hderiv : ∀ x ∈ Iio a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Iic a) volume
hf : Tendsto f atBot (𝓝 m)
hcont : ContinuousOn f (Iic a)
x : ℝ
hx : x ∈ Iic a
⊢ IntegrableOn f' (Ioc x a) volume

Tactic:
exact f'int.mono (fun y hy => hy.2) le_rfl

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

Goal state before:
pp: case h₂
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 - a)‖ ≤ ‖f' x - A‖ * ‖z - a‖

Tactic:
· apply ContinuousLinearMap.le_opNorm

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝³ : CommMonoid α
f : ι → β → α
g : β → α
inst✝² : UniformSpace α
inst✝¹ : TopologicalSpace β
inst✝ : LocallyCompactSpace β
h : ∀ (K : Set β), IsCompact K → HasProdUniformlyOn f g K
⊢ HasProdLocallyUniformly f g

Tactic:
rw [HasProdLocallyUniformly, tendstoLocallyUniformly_iff_forall_isCompact]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝³ : CommMonoid α
f : ι → β → α
g : β → α
inst✝² : UniformSpace α
inst✝¹ : TopologicalSpace β
inst✝ : LocallyCompactSpace β
h : ∀ (K : Set β), IsCompact K → HasProdUniformlyOn f g K
⊢ ∀ (K : Set β), IsCompact K → TendstoUniformlyOn (fun x1 x2 ↦ ∏ i ∈ x1, f i x2) g atTop K
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:
by
  refine ⟨fun _ _ ↦ ?_⟩
  rw [continuousGroupoid, mem_groupoid_of_pregroupoid]
  simp only [and_self_iff]

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

Goal state before:
pp: case inr
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✝¹ : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
inst✝ : Nonempty H
x : M'
⊢ Sum.inr x ∈
    (Sum.elim (fun x ↦ (ChartedSpace.chartAt x).lift_openEmbedding ⋯)
        (fun x ↦ (ChartedSpace.chartAt x).lift_openEmbedding ⋯) (Sum.inr x)).source

Tactic:
| inr x =>

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

Goal state before:
pp: case inr
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✝¹ : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
inst✝ : Nonempty H
x : M'
⊢ Sum.elim (fun x ↦ (ChartedSpace.chartAt x).lift_openEmbedding ⋯)
      (fun x ↦ (ChartedSpace.chartAt x).lift_openEmbedding ⋯) (Sum.inr x) ∈
    (fun e ↦ e.lift_openEmbedding ⋯) '' ChartedSpace.atlas ∪ (fun e ↦ e.lift_openEmbedding ⋯) '' ChartedSpace.atlas

Tactic:
| inr x =>

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

Goal state before:
pp: H : Type u
M : Type u_2
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
e : OpenPartialHomeomorph M H
he : e ∈ atlas H M
s : Opens M
hs : Nonempty ↥s
G : StructureGroupoid H
inst✝¹ : HasGroupoid M G
inst✝ : ClosedUnderRestriction G
⊢ e.subtypeRestr hs ∈ maximalAtlas (↥s) G

Tactic:
by
  intro e' he'
  -- `e'` is the restriction of some chart of `M` at `x`,
  obtain ⟨x, this⟩ := Opens.chart_eq hs he'
  rw [this]
  -- The transition functions between the unrestricted charts lie in the groupoid,
  -- the transition functions of the restriction are the restriction of the transition function.
  exact ⟨G.trans_restricted he (chart_mem_atlas H (x : M)) hs,
         G.trans_restricted (chart_mem_atlas H (x : M)) he hs⟩

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

Goal state before:
pp: case right.refine_2
H : Type u_1
inst✝ : TopologicalSpace H
PG : Pregroupoid H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ s, IsOpen[inst✝] s ∧ x ∈ s ∧ e.restr s ∈ {e | PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target}
x : H
xu : x ∈ e.target
s : Set H
s_open : IsOpen[inst✝] s
xs : ↑e.symm x ∈ s
hs : e.restr s ∈ {e | PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target}
⊢ PG.property (↑e.symm) (e.target ∩ (e.target ∩ ↑e.symm ⁻¹' s))

Tactic:
· rw [← inter_assoc, inter_self]
        convert! hs.2 using 1
        dsimp [OpenPartialHomeomorph.restr]
        rw [s_open.interior_eq]

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

Goal state before:
pp: H : Type u
M : Type u_2
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
G : StructureGroupoid H
e : OpenPartialHomeomorph M H
he : e ∈ atlas H M
hs : Nonempty ↑e.source
inst✝¹ : HasGroupoid M G
inst✝ : ClosedUnderRestriction G
s : Opens M := { carrier := e.source, is_open' := ⋯ }
t : Opens H := { carrier := e.target, is_open' := ⋯ }
c' : OpenPartialHomeomorph (↥t) H
hc'✝ : c' ∈ atlas H ↥t
this : Nonempty ↥t
x : ↥t
hc' : c' = (chartAt H ↑x).subtypeRestr this
goal : OpenPartialHomeomorph (↑e.source) H :=
  e.toHomeomorphSourceTarget.toOpenPartialHomeomorph ≫ₕ t.openPartialHomeomorphSubtypeCoe this
⊢ goal.source = (e.subtypeRestr hs).source

Tactic:
simp only [trans_toPartialEquiv, PartialEquiv.trans_source,
          Homeomorph.toOpenPartialHomeomorph_source, toFun_eq_coe,
          Homeomorph.toOpenPartialHomeomorph_apply, Opens.openPartialHomeomorphSubtypeCoe_source,
          preimage_univ, inter_self, subtypeRestr_source, goal, s]

Goal state after:
H : Type u
M : Type u_2
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
G : StructureGroupoid H
e : OpenPartialHomeomorph M H
he : e ∈ atlas H M
hs : Nonempty ↑e.source
inst✝¹ : HasGroupoid M G
inst✝ : ClosedUnderRestriction G
s : Opens M := { carrier := e.source, is_open' := ⋯ }
t : Opens H := { carrier := e.target, is_open' := ⋯ }
c' : OpenPartialHomeomorph (↥t) H
hc'✝ : c' ∈ atlas H ↥t
this : Nonempty ↥t
x : ↥t
hc' : c' = (chartAt H ↑x).subtypeRestr this
goal : OpenPartialHomeomorph (↑e.source) H :=
  e.toHomeomorphSourceTarget.toOpenPartialHomeomorph ≫ₕ t.openPartialHomeomorphSubtypeCoe this
⊢ univ = Subtype.val ⁻¹' e.source
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
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
x : E
hx : x ∈ ↑I '' (e.symm ≫ₕ e').source
⊢ ↑I '' (e.symm ≫ₕ e').source ∈ 𝓝[range ↑I] x

Tactic:
obtain ⟨x, hx, rfl⟩ := hx

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
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
x : H
hx : x ∈ (e.symm ≫ₕ e').source
⊢ ↑I '' (e.symm ≫ₕ e').source ∈ 𝓝[range ↑I] ↑I x
Module: Mathlib.Geometry.Manifold.LocalInvariantProperties

Goal state before:
pp: case e_s
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'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
g : M → M'
s t : Set M
x : M
hG : G.LocalInvariantProp G' P
hu : s =ᶠ[𝓝 x] t
⊢ s ∩ {x | (fun x ↦ s x = t x) x} = t ∩ {x | (fun x ↦ s x = t x) x}

Tactic:
aesop

Goal state after:
Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions

Goal state before:
pp: case inr
𝕜 : 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
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
M' : Type u_16
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H M'
n : WithTop ℕ∞
E' : Type u_17
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_18
inst✝² : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H' N
f : M → N
g : M' → N
hf : ContMDiff I J n f
hg : ContMDiff I J n g
x : M'
⊢ ContDiffWithinAt 𝕜 n (↑(extChartAt J (Sum.elim f g (Sum.inr x))) ∘ Sum.elim f g ∘ ↑(extChartAt I (Sum.inr x)).symm)
    (range ↑I) (↑(extChartAt I (Sum.inr x)) (Sum.inr x))

Tactic:
| inr x =>

Goal state after: