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

Goal state before:
pp: case e'_4
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
g_deriv : ∀ t ∈ Icc 0 1, HasDerivWithinAt g (g' t) (Icc 0 1) t
g'_bound : ∀ t ∈ Ico 0 1, ‖g' t‖ ≤ ε * ((‖v‖ + ‖w‖) * ‖w‖) * h ^ 2
I : ‖g 1 - g 0‖ ≤ ε * ((‖v‖ + ‖w‖) * ‖w‖) * h ^ 2
⊢ ε * ‖(‖v‖ + ‖w‖) * ‖w‖ * h ^ 2‖ = ε * ((‖v‖ + ‖w‖) * ‖w‖) * h ^ 2

Tactic:
simp (discharger := positivity) only [Real.norm_eq_abs, abs_of_nonneg]

Goal state after:
case e'_4
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
g_deriv : ∀ t ∈ Icc 0 1, HasDerivWithinAt g (g' t) (Icc 0 1) t
g'_bound : ∀ t ∈ Ico 0 1, ‖g' t‖ ≤ ε * ((‖v‖ + ‖w‖) * ‖w‖) * h ^ 2
I : ‖g 1 - g 0‖ ≤ ε * ((‖v‖ + ‖w‖) * ‖w‖) * h ^ 2
⊢ ε * ((‖v‖ + ‖w‖) * ‖w‖ * h ^ 2) = ε * ((‖v‖ + ‖w‖) * ‖w‖) * h ^ 2
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: α : 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}
x : α
xs : x ∈ s
δ : ℝ
⊢ δ > 0 → (g x ∩ Ioo 0 δ).Nonempty

Tactic:
δpos

Goal state after:
α : 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}
x : α
xs : x ∈ s
δ : ℝ
δpos : δ > 0
⊢ (g x ∩ Ioo 0 δ).Nonempty
Module: Mathlib.Analysis.Calculus.FDeriv.Partial

Goal state before:
pp: 𝕜 : 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 𝕜 := IsRCLikeNormedField.rclike 𝕜
⊢ (fun x ↦
      match x with
      | (v, w) => v.1 - w.1) =O[(𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ 𝓝 u.1 ×ˢ 𝓝 u.2]
    fun x ↦
    match x with
    | (v, w) => v - w

Tactic:
simp [isBigO_of_le]

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

Goal state before:
pp: 𝕜 : 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 𝕜 := IsRCLikeNormedField.rclike 𝕜
⊢ (fun x ↦
      match x with
      | (v, w) => v.2 - w.2) =O[(𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ 𝓝 u.1 ×ˢ 𝓝 u.2]
    fun x ↦
    match x with
    | (v, w) => v - w

Tactic:
simp [isBigO_of_le]

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

Goal state before:
pp: case disjoint
𝕜 : 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
⊢ ∀ x ∈ (↑f'u).ker, ↑(ContinuousLinearMap.fst 𝕜 E₁ E₂) x = 0 → x = 0

Tactic:
intro (_, y) h rfl

Goal state after:
case disjoint
𝕜 : 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
y : E₂
h : (0, y) ∈ (↑f'u).ker
⊢ (0, y) = 0
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))
⊢ ∃ 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:
obtain ⟨u, _, u_pos, u_lim⟩ :
    ∃ u : ℕ → ℝ, StrictAnti u ∧ (∀ n : ℕ, 0 < u n) ∧ Tendsto u atTop (𝓝 0) :=
    exists_seq_strictAnti_tendsto (0 : ℝ)

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)
⊢ ∃ 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.Analysis.Calculus.LHopital

Goal state before:
pp: a b : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hab : a < b
hdf : DifferentiableOn ℝ f (Ioo a b)
hcf : ContinuousOn f (Ico a b)
hcg : ContinuousOn g (Ico a b)
hg' : ∀ x ∈ Ioo a b, deriv g x ≠ 0
hfa : f a = 0
hga : g a = 0
hdiv : Tendsto (fun x ↦ deriv f x / deriv g x) (𝓝[>] a) l
⊢ Tendsto (fun x ↦ f x / g x) (𝓝[>] a) l

Tactic:
by
  refine lhopital_zero_right_on_Ioo hab hdf hg' ?_ ?_ hdiv
  · rw [← hfa, ← nhdsWithin_Ioo_eq_nhdsGT hab]
    exact ((hcf a <| left_mem_Ico.mpr hab).mono Ioo_subset_Ico_self).tendsto
  · rw [← hga, ← nhdsWithin_Ioo_eq_nhdsGT hab]
    exact ((hcg a <| left_mem_Ico.mpr hab).mono Ioo_subset_Ico_self).tendsto

Goal state after:
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), 0 ≤ f' x
⊢ IntervalIntegrable (fun x ↦ f' x • (g ∘ f) x) volume a b ↔ IntervalIntegrable g volume (f a) (f b)

Tactic:
have M : MonotoneOn f (uIcc a b) := by
    apply monotoneOn_of_deriv_nonneg (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 [intervalIntegrable_iff_integrableOn_Icc_of_le hab,
      integrableOn_Icc_deriv_smul_iff_of_deriv_nonneg,
      intervalIntegrable_iff_integrableOn_Icc_of_le]
    · apply M left_mem_uIcc right_mem_uIcc hab
    · rwa [uIcc_of_le hab] at hf
    · grind
    · grind
    · exact hab
  · rw [IntervalIntegrable.symm_iff, intervalIntegrable_iff_integrableOn_Icc_of_le hab.le,
      integrableOn_Icc_deriv_smul_iff_of_deriv_nonneg,
      IntervalIntegrable.symm_iff, intervalIntegrable_iff_integrableOn_Icc_of_le]
    · 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: 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 ↦ -f' x • (g ∘ n) (e x)) s volume
⊢ IntegrableOn g (f '' s) volume ↔ IntegrableOn (fun x ↦ -f' x • g (f x)) s volume

Tactic:
convert! B using 3 with x hx x

Goal state after:
case e'_1
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 ↦ -f' x • (g ∘ n) (e x)) s volume
x : ℝ
hx : x ∈ s
⊢ f x = (n ∘ e) x

case e'_2
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 ↦ -f' x • (g ∘ n) (e x)) s volume
x : ℝ
⊢ -f' x • g (f x) = -f' x • (g ∘ n) (e x)
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 : ∫ (x : ℝ) in e '' s, g (n x) = ∫ (x : ℝ) in s, -f' x • (g ∘ n) (e x)
B : ∫ (x : ℝ) in n ∘ e '' s, g x = ∫ (x : ℝ) in s, -f' x • (g ∘ n) (e x)
⊢ ∫ (x : ℝ) in f '' s, g x = ∫ (x : ℝ) in s, -f' x • g (f x)

Tactic:
convert! B using 3 with x hx x

Goal state after:
case e'_2
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 : ∫ (x : ℝ) in e '' s, g (n x) = ∫ (x : ℝ) in s, -f' x • (g ∘ n) (e x)
B : ∫ (x : ℝ) in n ∘ e '' s, g x = ∫ (x : ℝ) in s, -f' x • (g ∘ n) (e x)
⊢ f '' s = n ∘ e '' s

case e'_3
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 : ∫ (x : ℝ) in e '' s, g (n x) = ∫ (x : ℝ) in s, -f' x • (g ∘ n) (e x)
B : ∫ (x : ℝ) in n ∘ e '' s, g x = ∫ (x : ℝ) in s, -f' x • (g ∘ n) (e x)
x : ℝ
⊢ -f' x • g (f x) = -f' x • (g ∘ n) (e x)
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), HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo (min a b) (max a b), 0 ≤ f' x
⊢ ∫ (x : ℝ) in a..b, (g ∘ f) x * f' x = ∫ (u : ℝ) in f a..f b, g u

Tactic:
by
  simpa [mul_comm] using! integral_deriv_smul_comp_of_deriv_nonneg hf hff' hf'

Goal state after:
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'pos : ∀ x ∈ Ioi a, 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
hcont : ContinuousOn g (Ici a)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
⊢ ∫ (y : ℝ) in a..id x, g' y = ∫ (y : ℝ) in a..id x, ‖g' y‖

Tactic:
simp_rw [intervalIntegral.integral_of_le h'x]

Goal state after:
g g' : ℝ → ℝ
a l : ℝ
hcont✝ : ContinuousWithinAt g (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
hcont : ContinuousOn g (Ici a)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
⊢ ∫ (y : ℝ) in Ioc a (id x), g' y ∂volume = ∫ (y : ℝ) in Ioc a (id x), ‖g' y‖ ∂volume
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 ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Iic a) volume
g : ℝ → E := f ∘ fun x ↦ -x
hdg : ∀ x ∈ Ioi (-a), HasDerivAt g (-f' (-x)) x
L : Tendsto g atTop (𝓝 (atTop.limUnder g))
⊢ Tendsto f atBot (𝓝 (atTop.limUnder g))

Tactic:
have : Tendsto (fun x ↦ g (-x)) atBot (𝓝 (limUnder atTop g)) := L.comp tendsto_neg_atBot_atTop

Goal state after:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Iic a) volume
g : ℝ → E := f ∘ fun x ↦ -x
hdg : ∀ x ∈ Ioi (-a), HasDerivAt g (-f' (-x)) x
L : Tendsto g atTop (𝓝 (atTop.limUnder g))
this : Tendsto (fun x ↦ g (-x)) atBot (𝓝 (atTop.limUnder g))
⊢ Tendsto f atBot (𝓝 (atTop.limUnder g))
Module: Mathlib.MeasureTheory.Function.JacobianOneDim

Goal state before:
pp: f : ℝ ≃ᵐ ℝ
s : Set ℝ
hs : MeasurableSet s
g : ℝ → ℝ
hg : ∀ᵐ (x : ℝ), x ∈ ⇑f '' s → 0 ≤ g x
hf_int : IntegrableOn g (⇑f '' s) volume
f' : ℝ → ℝ
hf' : ∀ x ∈ s, HasDerivWithinAt (⇑f) (f' x) s x
⊢ (Measure.map (⇑f.symm) (volume.withDensity fun x ↦ ENNReal.ofReal (g x))) s =
    ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * g (f x))

Tactic:
by
  rw [MeasurableEquiv.withDensity_ofReal_map_symm_apply_eq_integral_abs_det_fderiv_mul volume hs
      f hg hf_int hf']
  simp only [det_toSpanSingleton]

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
hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Iic a) volume
fint : IntegrableOn f (Iic a) volume
F : E →L[ℝ] Completion E := Completion.toComplL
Fderiv : ∀ x ∈ Iic a, HasDerivAt (⇑F ∘ f) (F (f' x)) x
Fint : IntegrableOn (⇑F ∘ f) (Iic a) volume
F'int : IntegrableOn (⇑F ∘ f') (Iic a) volume
A : Tendsto (⇑F ∘ f) atBot (𝓝 (atBot.limUnder (⇑F ∘ f)))
this : IntegrableAtFilter (⇑F ∘ f) atBot volume
s : Set ℝ
hs : s ∈ atBot
⊢ volume s = ∞

Tactic:
rcases mem_atBot_sets.1 hs with ⟨b, hb⟩

Goal state after:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Iic a) volume
fint : IntegrableOn f (Iic a) volume
F : E →L[ℝ] Completion E := Completion.toComplL
Fderiv : ∀ x ∈ Iic a, HasDerivAt (⇑F ∘ f) (F (f' x)) x
Fint : IntegrableOn (⇑F ∘ f) (Iic a) volume
F'int : IntegrableOn (⇑F ∘ f') (Iic a) volume
A : Tendsto (⇑F ∘ f) atBot (𝓝 (atBot.limUnder (⇑F ∘ f)))
this : IntegrableAtFilter (⇑F ∘ f) atBot volume
s : Set ℝ
hs : s ∈ atBot
b : ℝ
hb : ∀ b_1 ≤ b, b_1 ∈ s
⊢ volume s = ∞
Module: Mathlib.Geometry.Manifold.StructureGroupoid

Goal state before:
pp: case inr.inl
H✝ : Type u_1
inst✝¹ : TopologicalSpace H✝
H : Type u_2
inst✝ : TopologicalSpace H
e : OpenPartialHomeomorph H H
he : ∀ x ∈ e.source, ∃ s, IsOpen[inst✝] s ∧ x ∈ s ∧ e.restr s ∈ {OpenPartialHomeomorph.refl H} ∪ {e | e.source = ∅}
x : H
hx : x ∈ e.source
s : Set H
open_s : IsOpen[inst✝] s
xs : x ∈ s
x's : x ∈ (e.restr s).source
hs : e.restr s = OpenPartialHomeomorph.refl H
⊢ e ∈ {OpenPartialHomeomorph.refl H}

Tactic:
have : (e.restr s).source = univ := by
          rw [hs]
          simp

Goal state after:
case inr.inl
H✝ : Type u_1
inst✝¹ : TopologicalSpace H✝
H : Type u_2
inst✝ : TopologicalSpace H
e : OpenPartialHomeomorph H H
he : ∀ x ∈ e.source, ∃ s, IsOpen[inst✝] s ∧ x ∈ s ∧ e.restr s ∈ {OpenPartialHomeomorph.refl H} ∪ {e | e.source = ∅}
x : H
hx : x ∈ e.source
s : Set H
open_s : IsOpen[inst✝] s
xs : x ∈ s
x's : x ∈ (e.restr s).source
hs : e.restr s = OpenPartialHomeomorph.refl H
this : (e.restr s).source = univ
⊢ e ∈ {OpenPartialHomeomorph.refl H}
Module: Mathlib.Geometry.Manifold.HasGroupoid

Goal state before:
pp: case left
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
inst✝³ : TopologicalSpace M'
inst✝² : TopologicalSpace M''
G : StructureGroupoid H
inst✝¹ : ChartedSpace H M'
inst✝ : ChartedSpace H M''
e : Structomorph G M M'
e' : Structomorph G M' M''
c : OpenPartialHomeomorph M H
c' : OpenPartialHomeomorph M'' H
hc : c ∈ atlas H M
hc' : c' ∈ atlas H M''
x : H
hx : x ∈ (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').source
f₁ : OpenPartialHomeomorph M M' := ⋯
f₂ : OpenPartialHomeomorph M' M'' := ⋯
f : OpenPartialHomeomorph M M'' := ⋯
feq : f = f₁ ≫ₕ f₂
y : M' := ⋯
g : OpenPartialHomeomorph M' H := ⋯
hg₁ : chartAt H y ∈ atlas H M'
hg₂ : y ∈ (chartAt H y).source
s : Set H := ⋯
open_s : IsOpen[inst✝⁶] s
⊢ x ∈ (c.symm ≫ₕ f₁).source

pp: case right
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
inst✝³ : TopologicalSpace M'
inst✝² : TopologicalSpace M''
G : StructureGroupoid H
inst✝¹ : ChartedSpace H M'
inst✝ : ChartedSpace H M''
e : Structomorph G M M'
e' : Structomorph G M' M''
c : OpenPartialHomeomorph M H
c' : OpenPartialHomeomorph M'' H
hc : c ∈ atlas H M
hc' : c' ∈ atlas H M''
x : H
hx : x ∈ (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').source
f₁ : OpenPartialHomeomorph M M' := ⋯
f₂ : OpenPartialHomeomorph M' M'' := ⋯
f : OpenPartialHomeomorph M M'' := ⋯
feq : f = f₁ ≫ₕ f₂
y : M' := ⋯
g : OpenPartialHomeomorph M' H := ⋯
hg₁ : chartAt H y ∈ atlas H M'
hg₂ : y ∈ (chartAt H y).source
s : Set H := ⋯
open_s : IsOpen[inst✝⁶] s
⊢ x ∈ ↑(c.symm ≫ₕ f₁) ⁻¹' g.source

Tactic:
· simp only [f₁, trans_source, preimage_univ, inter_univ,
            Homeomorph.toOpenPartialHomeomorph_source]
          rw [trans_source] at hx
          exact hx.1

Goal state after:
case right
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
inst✝³ : TopologicalSpace M'
inst✝² : TopologicalSpace M''
G : StructureGroupoid H
inst✝¹ : ChartedSpace H M'
inst✝ : ChartedSpace H M''
e : Structomorph G M M'
e' : Structomorph G M' M''
c : OpenPartialHomeomorph M H
c' : OpenPartialHomeomorph M'' H
hc : c ∈ atlas H M
hc' : c' ∈ atlas H M''
x : H
hx : x ∈ (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').source
f₁ : OpenPartialHomeomorph M M' := ⋯
f₂ : OpenPartialHomeomorph M' M'' := ⋯
f : OpenPartialHomeomorph M M'' := ⋯
feq : f = f₁ ≫ₕ f₂
y : M' := ⋯
g : OpenPartialHomeomorph M' H := ⋯
hg₁ : chartAt H y ∈ atlas H M'
hg₂ : y ∈ (chartAt H y).source
s : Set H := ⋯
open_s : IsOpen[inst✝⁶] s
⊢ x ∈ ↑(c.symm ≫ₕ f₁) ⁻¹' g.source
Module: Mathlib.Geometry.Manifold.StructureGroupoid

Goal state before:
pp: case h
H : Type u_1
inst✝ : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
e : OpenPartialHomeomorph H H
s : Set H
hs : IsOpen[inst✝] s
hes : e ≈ ofSet s hs
x✝ : H
⊢ ↑(ofSet s hs) x✝ = ↑((OpenPartialHomeomorph.refl H).restr s) x✝

Tactic:
simp [hs.interior_eq]

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

Goal state before:
pp: case hinv
H : Type u_1
inst✝ : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
e : OpenPartialHomeomorph H H
s : Set H
hs : IsOpen[inst✝] s
hes : e ≈ ofSet s hs
x✝ : H
⊢ ↑(ofSet s hs).symm x✝ = ↑((OpenPartialHomeomorph.refl H).restr s).symm x✝

Tactic:
simp [hs.interior_eq]

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

Goal state before:
pp: case hs
H : Type u_1
inst✝ : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
e : OpenPartialHomeomorph H H
s : Set H
hs : IsOpen[inst✝] s
hes : e ≈ ofSet s hs
x✝ : H
⊢ x✝ ∈ (ofSet s hs).source ↔ x✝ ∈ ((OpenPartialHomeomorph.refl H).restr s).source

Tactic:
simp [hs.interior_eq]

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 E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ IsOpen[inst✝] ((f.extend I).source ∩ ↑(f.extend I) ⁻¹' s)

Tactic:
exact isOpen_extend_preimage' f hs

Goal state after: