mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Haar.Unique

Goal state before:
pp: G : Type u_1
inst✝¹² : TopologicalSpace G
inst✝¹¹ : Group G
inst✝¹⁰ : IsTopologicalGroup G
inst✝⁹ : MeasurableSpace G
inst✝⁸ : BorelSpace G
H : Type u_2
inst✝⁷ : Group H
inst✝⁶ : TopologicalSpace H
inst✝⁵ : IsTopologicalGroup H
inst✝⁴ : CompactSpace H
inst✝³ : MeasurableSpace H
inst✝² : BorelSpace H
μ : Measure G
inst✝¹ : μ.IsHaarMeasure
ν : Measure H
inst✝ : ν.IsHaarMeasure
f : G →* H
hcont : Continuous[inst✝¹², inst✝⁶] ⇑f
hsurj : Surjective ⇑f
huniv : μ univ = ν univ
this✝¹ : IsFiniteMeasure μ
this✝ : (map (⇑f) μ).IsHaarMeasure
C : ℝ≥0 := (map (⇑f) μ).haarScalarFactor ν
hC : map (⇑f) μ = C • ν
this : ↑C * ν univ = 1 * ν univ
⊢ C = 1

Tactic:
ENNReal.mul_left_inj (NeZero.ne _) (measure_ne_top _ _),

Goal state after:
G : Type u_1
inst✝¹² : TopologicalSpace G
inst✝¹¹ : Group G
inst✝¹⁰ : IsTopologicalGroup G
inst✝⁹ : MeasurableSpace G
inst✝⁸ : BorelSpace G
H : Type u_2
inst✝⁷ : Group H
inst✝⁶ : TopologicalSpace H
inst✝⁵ : IsTopologicalGroup H
inst✝⁴ : CompactSpace H
inst✝³ : MeasurableSpace H
inst✝² : BorelSpace H
μ : Measure G
inst✝¹ : μ.IsHaarMeasure
ν : Measure H
inst✝ : ν.IsHaarMeasure
f : G →* H
hcont : Continuous[inst✝¹², inst✝⁶] ⇑f
hsurj : Surjective ⇑f
huniv : μ univ = ν univ
this✝¹ : IsFiniteMeasure μ
this✝ : (map (⇑f) μ).IsHaarMeasure
C : ℝ≥0 := (map (⇑f) μ).haarScalarFactor ν
hC : map (⇑f) μ = C • ν
this : ↑C = 1
⊢ C = 1
Module: Mathlib.MeasureTheory.Measure.Haar.Unique

Goal state before:
pp: G : Type u_1
inst✝⁷ : CommGroup G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : μ.IsHaarMeasure
inst✝¹ : LocallyCompactSpace G
inst✝ : μ.Regular
⊢ μ.IsInvInvariant

Tactic:
by
  -- the image measure is a Haar measure. By uniqueness up to multiplication, it is of the form
  -- `c μ`. Applying again inversion, one gets the measure `c^2 μ`. But since inversion is an
  -- involution, this is also `μ`. Hence, `c^2 = 1`, which implies `c = 1`.
  constructor
  let c : ℝ≥0∞ := haarScalarFactor μ.inv μ
  have hc : μ.inv = c • μ := isMulLeftInvariant_eq_smul_of_regular μ.inv μ
  have : map Inv.inv (map Inv.inv μ) = c ^ 2 • μ := by
    rw [← inv_def μ, hc, Measure.map_smul, ← inv_def μ, hc, smul_smul, pow_two]
  have μeq : μ = c ^ 2 • μ := by
    rw [map_map continuous_inv.measurable continuous_inv.measurable] at this
    simpa only [inv_involutive, Involutive.comp_self, Measure.map_id]
  have K : PositiveCompacts G := Classical.arbitrary _
  have : c ^ 2 * μ K = 1 ^ 2 * μ K := by
    conv_rhs => rw [μeq]
    simp
  have : c ^ 2 = 1 ^ 2 :=
    (ENNReal.mul_left_inj (measure_pos_of_nonempty_interior _ K.interior_nonempty).ne'
          K.isCompact.measure_lt_top.ne).1 this
  have : c = 1 := (ENNReal.pow_right_strictMono two_ne_zero).injective this
  rw [hc, this, one_smul]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : a.c (last N) = 0
lastr : a.r (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
i j : Fin N.succ
inej : i ≠ j
ah : Pairwise fun i j ↦ a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i ∨ a.r j ≤ ‖a.c j - a.c i‖ ∧ a.r i ≤ τ * a.r j
δnonneg : 0 ≤ δ
hcrj : ‖a.c j‖ ≤ a.r j + 1
hj : 2 < ‖a.c j‖
s : ℝ := ‖a.c i‖
hi : 2 < s
hij : s ≤ ‖a.c j‖
A : a.r i ≤ s
spos : 0 < s
d : E := (s / ‖a.c j‖) • a.c j
hd : d = (s / ‖a.c j‖) • a.c j
I : ‖a.c j - a.c i‖ ≤ ‖a.c j‖ - s + ‖d - a.c i‖
J : a.r j - ‖a.c j - a.c i‖ ≤ s / 2 * δ
⊢ 1 - δ ≤ ‖(2 / s) • a.c i - (2 / ‖a.c j‖) • a.c j‖

Tactic:
have invs_nonneg : 0 ≤ 2 / s := div_nonneg zero_le_two (zero_le_two.trans hi.le)

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : a.c (last N) = 0
lastr : a.r (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
i j : Fin N.succ
inej : i ≠ j
ah : Pairwise fun i j ↦ a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i ∨ a.r j ≤ ‖a.c j - a.c i‖ ∧ a.r i ≤ τ * a.r j
δnonneg : 0 ≤ δ
hcrj : ‖a.c j‖ ≤ a.r j + 1
hj : 2 < ‖a.c j‖
s : ℝ := ‖a.c i‖
hi : 2 < s
hij : s ≤ ‖a.c j‖
A : a.r i ≤ s
spos : 0 < s
d : E := (s / ‖a.c j‖) • a.c j
hd : d = (s / ‖a.c j‖) • a.c j
I : ‖a.c j - a.c i‖ ≤ ‖a.c j‖ - s + ‖d - a.c i‖
J : a.r j - ‖a.c j - a.c i‖ ≤ s / 2 * δ
invs_nonneg : 0 ≤ 2 / s
⊢ 1 - δ ≤ ‖(2 / s) • a.c i - (2 / ‖a.c j‖) • a.c j‖
Module: Mathlib.Analysis.Calculus.ContDiff.RestrictScalars

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NontriviallyNormedField 𝕜'
inst✝⁸ : NormedAlgebra 𝕜 𝕜'
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜' E
inst✝⁴ : IsScalarTower 𝕜 𝕜' E
F : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
x : E
f : E → F
n : ℕ
s : Set E
h : ContDiffWithinAt 𝕜' (↑n) f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
⊢ restrictScalars 𝕜 ∘ iteratedFDerivWithin 𝕜' n f s =ᶠ[𝓝[s] x] iteratedFDerivWithin 𝕜 n f s

Tactic:
by
  induction n with
  | zero =>
    filter_upwards with a
    ext m
    simp
  | succ n hn =>
    have t₀ := h.of_le (Nat.cast_le.mpr (n.le_add_right 1))
    have t₁ : ∀ᶠ (y : E) in 𝓝[s] x, ContDiffWithinAt 𝕜' (↑(n + 1)) f s y := by
      nth_rw 2 [← s.insert_eq_of_mem hx]
      apply h.eventually (by simp)
    filter_upwards [eventually_eventually_nhdsWithin.2 (hn t₀), t₁,
      eventually_mem_nhdsWithin (a := x) (s := s)] with a h₁a h₃a h₄a
    rw [← Filter.EventuallyEq] at h₁a
    ext m
    simp only [Function.comp_apply, coe_restrictScalars, iteratedFDerivWithin_succ_apply_left]
    rw [← (h₁a.fderivWithin' (by tauto)).eq_of_nhdsWithin h₄a,
      fderivWithin_restrictScalars_comp]
    · simp
    · apply h₃a.differentiableWithinAt_iteratedFDerivWithin
      · rw [Nat.cast_lt]
        simp
      · have : UniqueDiffOn 𝕜' s := hs.mono_field
        simpa [s.insert_eq_of_mem h₄a]
    apply hs a h₄a

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

Goal state before:
pp: case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : a.c (last N) = 0
lastr : a.r (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin N.succ → E := fun i ↦ if ‖a.c i‖ ≤ 2 then a.c i else (2 / ‖a.c i‖) • a.c i
norm_c'_le : ∀ (i : Fin N.succ), ‖c' i‖ ≤ 2
i j : Fin N.succ
inej : i ≠ j
hij : ‖a.c i‖ ≤ ‖a.c j‖
Hj : 2 < ‖a.c j‖
⊢ 1 - δ ≤ ‖c' i - c' j‖

Tactic:
have H'j : ‖a.c j‖ ≤ 2 ↔ False := by simpa only [not_le, iff_false] using Hj
    rcases le_or_gt ‖a.c i‖ 2 with (Hi | Hi)
    · -- case `‖c i‖ ≤ 2`
      simp_rw [c', Hi, if_true, H'j, if_false]
      exact exists_normalized_aux2 a lastc lastr hτ δ hδ1 hδ2 i j inej Hi Hj
    · -- case `2 < ‖c i‖`
      have H'i : ‖a.c i‖ ≤ 2 ↔ False := by simpa only [not_le, iff_false] using Hi
      simp_rw [c', H'i, if_false, H'j, if_false]
      exact exists_normalized_aux3 a lastc lastr hτ δ hδ1 i j inej Hi hij

Goal state after:
Module: Mathlib.Topology.MetricSpace.Holder

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
C D s : ℝ≥0
A : Set X
hA : ∀ x ∈ A, ∀ y ∈ A, edist x y ≤ ↑D
hf : HolderOnWith C r f A
hsr : ↑s ≤ ↑r
ht : 0 < s
hr : 0 < ↑r
θ₁ : ℝ≥0 := ⋯
θ₂ : ℝ≥0 := ⋯
hθ : θ₁ + θ₂ = 1
⊢ ↑(r * θ₁ + 0 * θ₂) = ↑s

Tactic:
simp [θ₁, mul_div_cancel₀ _ hr.ne']

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

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

Tactic:
h'j

Goal state after:
case hD
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
Fu : Type u
inst✝³ : NormedAddCommGroup Fu
inst✝² : NormedSpace 𝕜 Fu
f : E → Fu
s : Set E
t : Set Fu
x : E
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
n : ℕ
IH :
  ∀ m ≤ n,
    ∀ {Gu : Type u} [inst : NormedAddCommGroup Gu] [inst_1 : NormedSpace 𝕜 Gu] {g : Fu → Gu},
      ContDiffOn 𝕜 (↑m) g t →
        ContDiffOn 𝕜 (↑m) f s →
          (∀ i ≤ m, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C) →
            (∀ (i : ℕ), 1 ≤ i → i ≤ m → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i) →
              ‖iteratedFDerivWithin 𝕜 m (g ∘ f) s x‖ ≤ ↑m ! * C * D ^ m
Gu : Type u
inst✝¹ : NormedAddCommGroup Gu
inst✝ : NormedSpace 𝕜 Gu
g : Fu → Gu
hg : ContDiffOn 𝕜 (↑(n + 1)) g t
hf : ContDiffOn 𝕜 (↑(n + 1)) f s
hC : ∀ i ≤ n + 1, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C
hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n + 1 → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i
M : ↑n < ↑n.succ
Cnonneg : 0 ≤ C
Dnonneg : 0 ≤ D
i : ℕ
hi : i ≤ n
j : ℕ
hj : 1 ≤ j
h'j : j ≤ i
⊢ ‖iteratedFDerivWithin 𝕜 j f s x‖ ≤ D ^ j
Module: Mathlib.Analysis.Calculus.DifferentialForm.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ
r : WithTop ℕ∞
s : Set E
x : E
ω : F → F [⋀^Fin n]→L[𝕜] G
f : E → F
t : Set F
hω : DifferentiableWithinAt 𝕜 ω t (f x)
hf : ContDiffWithinAt 𝕜 r f s x
hr : minSmoothness 𝕜 2 ≤ r
hs : UniqueDiffOn 𝕜 s
hxc : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
hxs : x ∈ s
hst : MapsTo f s t
hdf : DifferentiableWithinAt 𝕜 f s x
hd2f : DifferentiableWithinAt 𝕜 (fderivWithin 𝕜 f s) s x
⊢ DifferentiableWithinAt 𝕜 (fun x ↦ ω (f x)) s x

Tactic:
exact hω.comp x hdf hst

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₀ f₁ : E → F
f' : F
x v : E
h : f₀ =ᶠ[𝓝 x] f₁
⊢ HasLineDerivAt 𝕜 f₀ f' x v ↔ HasLineDerivAt 𝕜 f₁ f' x v

Tactic:
apply hasDerivAt_iff
  let F := fun (t : 𝕜) ↦ x + t • v
  have B : ContinuousAt F 0 := by apply Continuous.continuousAt; fun_prop
  have : f₀ =ᶠ[𝓝 (F 0)] f₁ := by convert! h; simp [F]
  exact B.preimage_mem_nhds this

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✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : E → F
s : Set E
x v : E
f' : F
h : HasDerivWithinAt (fun t ↦ f (x + t • v)) f' ((fun t ↦ x + t • v) ⁻¹' s) 0
c : 𝕜
g : 𝕜 → 𝕜 := fun t ↦ c • t
⊢ HasDerivWithinAt (fun t ↦ f (x + t • c • v)) (c • f') ((fun t ↦ x + t • c • v) ⁻¹' s) 0

Tactic:
let s' := (fun (t : 𝕜) ↦ x + t • v) ⁻¹' s

Goal state after:
𝕜 : 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
s : Set E
x v : E
f' : F
h : HasDerivWithinAt (fun t ↦ f (x + t • v)) f' ((fun t ↦ x + t • v) ⁻¹' s) 0
c : 𝕜
g : 𝕜 → 𝕜 := fun t ↦ c • t
s' : Set 𝕜 := (fun t ↦ x + t • v) ⁻¹' s
⊢ HasDerivWithinAt (fun t ↦ f (x + t • c • v)) (c • f') ((fun t ↦ x + t • c • v) ⁻¹' s) 0
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)
⊢ IsSymmSndFDerivWithinAt 𝕜 f s x

Tactic:
have h'u : UniqueDiffOn 𝕜 (s ∩ u) := hs.inter u_open

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)
⊢ IsSymmSndFDerivWithinAt 𝕜 f s x
Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno

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
g : E → F
f : 𝕜 → E
x : 𝕜
hg : ContDiffAt 𝕜 2 g (f x)
hf : ContDiffAt 𝕜 2 f x
⊢ iteratedDerivWithin 2 (g ∘ f) univ x =
    ((iteratedFDerivWithin 𝕜 2 g univ (f x)) fun x_1 ↦ derivWithin f univ x) +
      (fderivWithin 𝕜 g univ (f x)) (iteratedDerivWithin 2 f univ x)

Tactic:
exact iteratedDerivWithin_vcomp_two hg hf uniqueDiffOn_univ
    uniqueDiffOn_univ (mem_univ x) (mapsTo_univ f _)

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

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
g : E → F
f : 𝕜 → E
x : 𝕜
hg : ContDiffAt 𝕜 3 g (f x)
hf : ContDiffAt 𝕜 3 f x
⊢ iteratedDerivWithin 3 (g ∘ f) univ x =
    ((iteratedFDerivWithin 𝕜 3 g univ (f x)) fun x_1 ↦ derivWithin f univ x) +
          (iteratedFDerivWithin 𝕜 2 g univ (f x)) ![iteratedDerivWithin 2 f univ x, derivWithin f univ x] +
        2 • (iteratedFDerivWithin 𝕜 2 g univ (f x)) ![derivWithin f univ x, iteratedDerivWithin 2 f univ x] +
      (fderivWithin 𝕜 g univ (f x)) (iteratedDerivWithin 3 f univ x)

Tactic:
exact iteratedDerivWithin_vcomp_three hg hf uniqueDiffOn_univ
    uniqueDiffOn_univ (mem_univ x) (mapsTo_univ f _)

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

Goal state before:
pp: l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ᶠ (x : ℝ) in atTop, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in atTop, HasDerivAt g (g' x) x
hg' : ∀ᶠ (x : ℝ) in atTop, g' x ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun x ↦ f' x / g' x) atTop l
⊢ Tendsto (fun x ↦ f x / g x) atTop l

Tactic:
rw [eventually_iff_exists_mem] at *
  rcases hff' with ⟨s₁, hs₁, hff'⟩
  rcases hgg' with ⟨s₂, hs₂, hgg'⟩
  rcases hg' with ⟨s₃, hs₃, hg'⟩
  let s := s₁ ∩ s₂ ∩ s₃
  have hs : s ∈ atTop := inter_mem (inter_mem hs₁ hs₂) hs₃
  rw [mem_atTop_sets] at hs
  rcases hs with ⟨l, hl⟩
  have hl' : Ioi l ⊆ s := fun x hx => hl x (le_of_lt hx)
  refine lhopital_zero_atTop_on_Ioi ?_ ?_ (fun x hx ↦ hg' x (hl' hx).2) hftop hgtop hdiv <;> grind

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

Goal state before:
pp: s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : MonotoneOn f s
u : ℝ → ℝ≥0∞
a b c : Set ℝ
h_union : a ∪ (b ∪ c) = s
ha : MeasurableSet a
hb : MeasurableSet b
hc : MeasurableSet c
h_disj : Disjoint a (b ∪ c)
h_disj' : Disjoint b c
a_count : a.Countable
fb_count : (f '' b).Countable
deriv_b : ∀ x ∈ b, f' x = 0
deriv_c : ∀ x ∈ c, 0 ≤ f' x
inj_c : InjOn f c
I : ∫⁻ (x : ℝ) in s, ENNReal.ofReal (f' x) * u (f x) = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)
J : ∫⁻ (x : ℝ) in f '' s, u x = ∫⁻ (x : ℝ) in f '' c, u x
c_s : c ⊆ s
F' : ℝ → ℝ →L[ℝ] ℝ := fun x ↦ smulRight 1 (f' x)
⊢ ∫⁻ (x : ℝ) in f '' c, u x = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)

Tactic:
have hf' (x : ℝ) (hx : x ∈ c) : HasFDerivWithinAt f (F' x) c x :=
    (hf' x (c_s hx)).hasFDerivWithinAt.mono c_s

Goal state after:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf'✝ : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : MonotoneOn f s
u : ℝ → ℝ≥0∞
a b c : Set ℝ
h_union : a ∪ (b ∪ c) = s
ha : MeasurableSet a
hb : MeasurableSet b
hc : MeasurableSet c
h_disj : Disjoint a (b ∪ c)
h_disj' : Disjoint b c
a_count : a.Countable
fb_count : (f '' b).Countable
deriv_b : ∀ x ∈ b, f' x = 0
deriv_c : ∀ x ∈ c, 0 ≤ f' x
inj_c : InjOn f c
I : ∫⁻ (x : ℝ) in s, ENNReal.ofReal (f' x) * u (f x) = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)
J : ∫⁻ (x : ℝ) in f '' s, u x = ∫⁻ (x : ℝ) in f '' c, u x
c_s : c ⊆ s
F' : ℝ → ℝ →L[ℝ] ℝ := fun x ↦ smulRight 1 (f' x)
hf' : ∀ x ∈ c, HasFDerivWithinAt f (F' x) c x
⊢ ∫⁻ (x : ℝ) in f '' c, u x = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: α : Type u_1
ι : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : NormedAddCommGroup E
inst✝¹ : l.NeBot
inst✝ : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (φ i) μ
hbounded : ∀ᶠ (i : ι) in l, ∫ (x : α) in φ i, ‖f x‖ ∂μ ≤ I
⊢ Integrable f μ

Tactic:
by
  have hfm : AEStronglyMeasurable f μ :=
    hφ.aestronglyMeasurable fun i => (hfi i).aestronglyMeasurable
  refine hφ.integrable_of_lintegral_enorm_bounded I hfm ?_
  conv at hbounded in integral _ _ =>
    rw [integral_eq_lintegral_of_nonneg_ae (ae_of_all _ fun x => @norm_nonneg E _ (f x))
        hfm.norm.restrict]
  conv at hbounded in ENNReal.ofReal _ =>
    rw [← coe_nnnorm, ENNReal.ofReal_coe_nnreal]
  refine hbounded.mono fun i hi => ?_
  rw [← ENNReal.ofReal_toReal <| ne_top_of_lt <| hasFiniteIntegral_iff_enorm.mp (hfi i).2]
  apply ENNReal.ofReal_le_ofReal hi

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

Goal state before:
pp: ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : l.IsCountablyGenerated
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : ι → ℝ
f : ℝ → E
ha : Tendsto a l atBot
⊢ Tendsto (fun i ↦ ∫ (x : ℝ) in Iic (a i), f x ∂μ) l (𝓝 0)

Tactic:
by
  by_cases! h : ∀ b, ¬ IntegrableOn f (Iic b) μ
  · exact tendsto_const_nhds.congr (fun i => (integral_undef (h (a i))).symm)
  obtain ⟨b, hb⟩ := h
  have : ∀ᶠ i in l, ∫ x in Iic b, f x ∂μ - ∫ x in a i..b, f x ∂μ = ∫ x in Iic (a i), f x ∂μ := by
    filter_upwards [ha.eventually_mem (Iic_mem_atBot b)] with i hi
    rw [sub_eq_iff_comm,
      intervalIntegral.integral_Iic_sub_Iic (hb.mono_set (Iic_subset_Iic.2 hi)) hb]
  rw [← sub_self (∫ x in Iic b, f x ∂μ)]
  exact Tendsto.congr' this (Tendsto.const_sub _ <| intervalIntegral_tendsto_integral_Iic b hb ha)

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

Goal state before:
pp: ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : l.IsCountablyGenerated
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : ι → ℝ
f : ℝ → E
ha : Tendsto a l atTop
⊢ Tendsto (fun i ↦ ∫ (x : ℝ) in Ici (a i), f x ∂μ) l (𝓝 0)

Tactic:
by
  by_cases! h : ∀ b, ¬ IntegrableOn f (Ici b) μ
  · exact tendsto_const_nhds.congr (fun i => (integral_undef (h (a i))).symm)
  obtain ⟨b, hb⟩ := h
  have : ∀ᶠ i in l, ∫ x in Ici b, f x ∂μ - ∫ x in Ico b (a i), f x ∂μ =
      ∫ x in Ici (a i), f x ∂μ := by
    filter_upwards [ha.eventually_mem (Ici_mem_atTop b)] with i hi
    rw [sub_eq_iff_comm, intervalIntegral.integral_Ici_sub_Ici hb hi]
  rw [← sub_self (∫ x in Ici b, f x ∂μ)]
  exact Tendsto.congr' this (Tendsto.const_sub _ <| tendsto_integral_Ico_integral_Ici b hb ha)

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

Goal state before:
pp: case e'_2
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : AntitoneOn f s
u : ℝ → ℝ≥0∞
n : ℝ → ℝ := fun x ↦ -x
e : ℝ → ℝ := n ∘ f
hg' : ∀ x ∈ s, HasDerivWithinAt e (-f' x) s x
A : ∫⁻ (x : ℝ) in e '' s, u (n x) = ∫⁻ (x : ℝ) in s, ENNReal.ofReal (-f' x) * (u ∘ n) (e x)
B : ∫⁻ (x : ℝ) in n ∘ e '' s, u x = ∫⁻ (x : ℝ) in s, ENNReal.ofReal (-f' x) * (u ∘ n) (e x)
x : ℝ
hx : x ∈ s
⊢ f x = (n ∘ e) x

Tactic:
simp [n, e]

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

Goal state before:
pp: case e'_3
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : AntitoneOn f s
u : ℝ → ℝ≥0∞
n : ℝ → ℝ := fun x ↦ -x
e : ℝ → ℝ := n ∘ f
hg' : ∀ x ∈ s, HasDerivWithinAt e (-f' x) s x
A : ∫⁻ (x : ℝ) in e '' s, u (n x) = ∫⁻ (x : ℝ) in s, ENNReal.ofReal (-f' x) * (u ∘ n) (e x)
B : ∫⁻ (x : ℝ) in n ∘ e '' s, u x = ∫⁻ (x : ℝ) in s, ENNReal.ofReal (-f' x) * (u ∘ n) (e x)
x : ℝ
⊢ u (f x) = (u ∘ n) (e x)

Tactic:
simp [n, e]

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

Goal state before:
pp: 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

Tactic:
simp [n, e]

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

Goal state before:
pp: 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)

Tactic:
simp [n, e]

Goal state after: