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
μ' μ : Measure G
inst✝² : μ.IsHaarMeasure
inst✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
f : G → ℝ
hf : Continuous[inst✝⁷, _] f
h'f : HasCompactSupport f
u : ℕ → ℝ
u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 1
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → ℝ → ℝ := fun n x ↦ ↑((thickenedIndicator ⋯ {1}) x)
vf_cont : ∀ (n : ℕ), Continuous[inst✝⁷, _] (v n ∘ f)
I :
  ∀ (ν : Measure G),
    IsFiniteMeasureOnCompacts ν →
      Tendsto (fun n ↦ ∫ (x : G), v n (f x) ∂ν) atTop (𝓝 (∫ (x : G), {1}.indicator (fun x ↦ 1) (f x) ∂ν))
M : ∀ (n : ℕ), ∫ (x : G), v n (f x) ∂μ' = ∫ (x : G), v n (f x) ∂μ'.haarScalarFactor μ • μ
I1 :
  Tendsto (fun n ↦ ∫ (x : G), v n (f x) ∂μ'.haarScalarFactor μ • μ) atTop
    (𝓝 (∫ (x : G), {1}.indicator (fun x ↦ 1) (f x) ∂μ'))
J1 :
  ∫ (x : G), {1}.indicator (fun x ↦ 1) (f x) ∂μ' = ∫ (x : G), {1}.indicator (fun x ↦ 1) (f x) ∂μ'.haarScalarFactor μ • μ
⊢ μ'.real (f ⁻¹' {1}) = (μ'.haarScalarFactor μ • μ).real (f ⁻¹' {1})

Tactic:
have : (fun x ↦ indicator {1} (fun _ ↦ (1 : ℝ)) (f x)) =
        (fun x ↦ indicator (f ⁻¹' {1}) (fun _ ↦ (1 : ℝ)) x) := by
      ext x
      exact (indicator_comp_right f (s := ({1} : Set ℝ)) (g := (fun _ ↦ (1 : ℝ))) (x := x)).symm

Goal state after:
G : Type u_1
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ' μ : Measure G
inst✝² : μ.IsHaarMeasure
inst✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
f : G → ℝ
hf : Continuous[inst✝⁷, _] f
h'f : HasCompactSupport f
u : ℕ → ℝ
u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 1
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → ℝ → ℝ := fun n x ↦ ↑((thickenedIndicator ⋯ {1}) x)
vf_cont : ∀ (n : ℕ), Continuous[inst✝⁷, _] (v n ∘ f)
I :
  ∀ (ν : Measure G),
    IsFiniteMeasureOnCompacts ν →
      Tendsto (fun n ↦ ∫ (x : G), v n (f x) ∂ν) atTop (𝓝 (∫ (x : G), {1}.indicator (fun x ↦ 1) (f x) ∂ν))
M : ∀ (n : ℕ), ∫ (x : G), v n (f x) ∂μ' = ∫ (x : G), v n (f x) ∂μ'.haarScalarFactor μ • μ
I1 :
  Tendsto (fun n ↦ ∫ (x : G), v n (f x) ∂μ'.haarScalarFactor μ • μ) atTop
    (𝓝 (∫ (x : G), {1}.indicator (fun x ↦ 1) (f x) ∂μ'))
J1 :
  ∫ (x : G), {1}.indicator (fun x ↦ 1) (f x) ∂μ' = ∫ (x : G), {1}.indicator (fun x ↦ 1) (f x) ∂μ'.haarScalarFactor μ • μ
this : (fun x ↦ {1}.indicator (fun x ↦ 1) (f x)) = fun x ↦ (f ⁻¹' {1}).indicator (fun x ↦ 1) x
⊢ μ'.real (f ⁻¹' {1}) = (μ'.haarScalarFactor μ • μ).real (f ⁻¹' {1})
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: α : Type u_1
inst✝⁴ : MetricSpace α
inst✝³ : SecondCountableTopology α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
s : Set α
r : α → ℝ
rpos : ∀ x ∈ s, 0 < r x
rle : ∀ x ∈ s, r x ≤ 1
hμs : 0 < μ s
h✝ : Nonempty α
Npos : N ≠ 0
o : Set α
so : s ⊆ o
omeas : MeasurableSet o
μo : μ o = μ s
a : BallPackage (↑s) α := { c := fun x ↦ ↑x, r := fun x ↦ r ↑x, rpos := ⋯, r_bound := 1, r_le := ⋯ }
u : Fin N → Set ↑s
hu : ∀ (i : Fin N), (u i).PairwiseDisjoint fun j ↦ closedBall (a.c j) (a.r j)
hu' : range a.c ⊆ ⋃ i, ⋃ j ∈ u i, ball (a.c j) (a.r j)
u_count : ∀ (i : Fin N), (u i).Countable
v : Fin N → Set α := fun i ↦ ⋃ x ∈ u i, closedBall (↑x) (r ↑x)
A : s = ⋃ i, s ∩ v i
S : ∑ _i, μ s / ↑N ≤ ∑ i, μ (s ∩ v i)
i : Fin N
hi : μ s / ↑N ≤ μ (s ∩ v i)
⊢ μ s / (↑N + 1) < μ (s ∩ v i)

Tactic:
grw [← hi, ← _root_.zero_lt_one, add_zero] <;> finiteness

Goal state after:
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
inst✝² : LocallyCompactSpace G
μ' μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := ⋯
k : Set G
k_comp : IsCompact k
k_closed : IsClosed[inst✝⁷] k
k_mem : k ∈ 𝓝 1
one_k : 1 ∈ k
A : Set (Set G) := ⋯
m : Set G
m_max : Maximal (fun x ↦ x ∈ A) m
hms : m ⊆ s
hdj : m.PairwiseDisjoint fun x ↦ x • k
sm : s ⊆ ⋃ x ∈ m, x • (k * k⁻¹)
hm : m.Nonempty
ρ : Measure G
hρ : ρ.IsEverywherePos s
M : ∀ (i : ↑m), MeasurableSet (s ∩ ↑i • k)
h'm : ρ s ≠ ∞
⊢ ρ (⋃ i, s ∩ ↑i • k) < ∞

Tactic:
exact lt_of_le_of_lt (measure_mono (by simp [inter_subset_left])) h'm.lt_top

Goal state after:
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
inst✝² : LocallyCompactSpace G
μ' μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed[inst✝⁷] k
k_mem : k ∈ 𝓝 1
one_k : 1 ∈ k
A : Set (Set G) := {t | t ⊆ s ∧ t.PairwiseDisjoint fun x ↦ x • k}
m : Set G
m_max : Maximal (fun x ↦ x ∈ A) m
hms : m ⊆ s
hdj : m.PairwiseDisjoint fun x ↦ x • k
sm : s ⊆ ⋃ x ∈ m, x • (k * k⁻¹)
hm : m.Nonempty
ρ : Measure G
hρ : ρ.IsEverywherePos s
M : ∀ (i : ↑m), MeasurableSet (s ∩ ↑i • k)
h'm : ρ s ≠ ∞
this : ∑' (x : ↑m), ρ (s ∩ ↑x • k) < ∞
C : (support fun i ↦ ρ (s ∩ ↑i • k)).Countable
i : ↑m
⊢ ↑i • k ∈ 𝓝 ↑i

Tactic:
simpa

Goal state after:
Module: Mathlib.Analysis.Convex.NNReal

Goal state before:
pp: M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module ℝ M
s : Set M
H : Convex ℝ≥0 s
x✝ : M
hx : x✝ ∈ s
y✝ : M
hy : y✝ ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ↑(⟨a, ha⟩ + ⟨b, hb⟩) = ↑1

Tactic:
simpa

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
f : X → Y
C : ℝ≥0
⊢ Convex ℝ≥0 {r | HolderWith C r f}

Tactic:
simp_rw [← holderOnWith_univ]
  exact convex_setOfPred_holderOnWith f C _

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PseudoMetricSpace X
inst✝ : PseudoMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
x y : X
hf : HolderOnWith C r f s
hx : x ∈ s
hy : y ∈ s
d : ℝ≥0
hd : nndist x y ≤ d
⊢ nndist (f x) (f y) ≤ C * d ^ ↑r

Tactic:
exact hf.nndist_le_of_le hx hy hd

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise

Goal state before:
pp: case hp_bdd
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
k : ℕ
α : ↑I
f : E → F
a : E
g : F → G
hg : ContDiffPointwiseHolderAt k α g (f a)
hf : ContDiffPointwiseHolderAt k α f a
hd : DifferentiableAt ℝ g (f a) ∨ DifferentiableAt ℝ f a
⊢ ∀ k_1 ≤ k, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 a) fun x ↦ ‖ftaylorSeries ℝ g (f x) k_1‖

Tactic:
intro i hi

Goal state after:
case hp_bdd
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
k : ℕ
α : ↑I
f : E → F
a : E
g : F → G
hg : ContDiffPointwiseHolderAt k α g (f a)
hf : ContDiffPointwiseHolderAt k α f a
hd : DifferentiableAt ℝ g (f a) ∨ DifferentiableAt ℝ f a
i : ℕ
hi : i ≤ k
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 a) fun x ↦ ‖ftaylorSeries ℝ g (f x) i‖
Module: Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise

Goal state before:
pp: case hpf
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
k : ℕ
α : ↑I
f : E → F
a : E
g : F → G
hg : ContDiffPointwiseHolderAt k α g (f a)
hf : ContDiffPointwiseHolderAt k α f a
hd : DifferentiableAt ℝ g (f a) ∨ DifferentiableAt ℝ f a
⊢ ∀ k_1 ≤ k, (fun a_2 ↦ ftaylorSeries ℝ g (f a_2) k_1 - ftaylorSeries ℝ g (f a) k_1) =O[𝓝 a] fun x ↦ ‖x - a‖ ^ ↑α

Tactic:
intro i hi

Goal state after:
case hpf
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
k : ℕ
α : ↑I
f : E → F
a : E
g : F → G
hg : ContDiffPointwiseHolderAt k α g (f a)
hf : ContDiffPointwiseHolderAt k α f a
hd : DifferentiableAt ℝ g (f a) ∨ DifferentiableAt ℝ f a
i : ℕ
hi : i ≤ k
⊢ (fun a_1 ↦ ftaylorSeries ℝ g (f a_1) i - ftaylorSeries ℝ g (f a) i) =O[𝓝 a] fun x ↦ ‖x - a‖ ^ ↑α
Module: Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise

Goal state before:
pp: case hq₁_bdd
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
k : ℕ
α : ↑I
f : E → F
a : E
g : F → G
hg : ContDiffPointwiseHolderAt k α g (f a)
hf : ContDiffPointwiseHolderAt k α f a
hd : DifferentiableAt ℝ g (f a) ∨ DifferentiableAt ℝ f a
⊢ ∀ k_1 ≤ k, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 a) fun x ↦ ‖ftaylorSeries ℝ f x k_1‖

Tactic:
intro i hi

Goal state after:
case hq₁_bdd
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
k : ℕ
α : ↑I
f : E → F
a : E
g : F → G
hg : ContDiffPointwiseHolderAt k α g (f a)
hf : ContDiffPointwiseHolderAt k α f a
hd : DifferentiableAt ℝ g (f a) ∨ DifferentiableAt ℝ f a
i : ℕ
hi : i ≤ k
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 a) fun x ↦ ‖ftaylorSeries ℝ f x i‖
Module: Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise

Goal state before:
pp: case hq₂_bdd
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
k : ℕ
α : ↑I
f : E → F
a : E
g : F → G
hg : ContDiffPointwiseHolderAt k α g (f a)
hf : ContDiffPointwiseHolderAt k α f a
hd : DifferentiableAt ℝ g (f a) ∨ DifferentiableAt ℝ f a
⊢ ∀ k_1 ≤ k, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 a) fun x ↦ ‖ftaylorSeries ℝ f a k_1‖

Tactic:
intro i hi

Goal state after:
case hq₂_bdd
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
k : ℕ
α : ↑I
f : E → F
a : E
g : F → G
hg : ContDiffPointwiseHolderAt k α g (f a)
hf : ContDiffPointwiseHolderAt k α f a
hd : DifferentiableAt ℝ g (f a) ∨ DifferentiableAt ℝ f a
i : ℕ
hi : i ≤ k
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 a) fun x ↦ ‖ftaylorSeries ℝ f a i‖
Module: Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise

Goal state before:
pp: case hqf
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
k : ℕ
α : ↑I
f : E → F
a : E
g : F → G
hg : ContDiffPointwiseHolderAt k α g (f a)
hf : ContDiffPointwiseHolderAt k α f a
hd : DifferentiableAt ℝ g (f a) ∨ DifferentiableAt ℝ f a
⊢ ∀ k_1 ≤ k, (fun a_2 ↦ ftaylorSeries ℝ f a_2 k_1 - ftaylorSeries ℝ f a k_1) =O[𝓝 a] fun x ↦ ‖x - a‖ ^ ↑α

Tactic:
intro i hi

Goal state after:
case hqf
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
k : ℕ
α : ↑I
f : E → F
a : E
g : F → G
hg : ContDiffPointwiseHolderAt k α g (f a)
hf : ContDiffPointwiseHolderAt k α f a
hd : DifferentiableAt ℝ g (f a) ∨ DifferentiableAt ℝ f a
i : ℕ
hi : i ≤ k
⊢ (fun a_1 ↦ ftaylorSeries ℝ f a_1 i - ftaylorSeries ℝ f a i) =O[𝓝 a] fun x ↦ ‖x - a‖ ^ ↑α
Module: Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise

Goal state before:
pp: E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
k : ℕ
α : ↑I
f : E → F
a : E
g : F → G
hg : ContDiffPointwiseHolderAt k α g (f a)
hf : ContDiffPointwiseHolderAt k α f a
hd : DifferentiableAt ℝ g (f a) ∨ DifferentiableAt ℝ f a
i : ℕ
hi : i ≤ k
hfd : ¬DifferentiableAt ℝ f a
⊢ k = 0

Tactic:
contrapose! hfd
            exact hf.differentiableAt hfd

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

Goal state before:
pp: case inr.inl
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ x ∈ Icc a b, HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun x ↦ f x - m * x
hg : ∀ x ∈ Icc a b, HasDerivWithinAt g (f' x - m) (Icc a b) x
cmem : b ∈ Icc a b
hc : IsMinOn g (Icc a b) b
hac : a < b
this : a - b ∈ posTangentConeAt (Icc a b) b
⊢ 0 ≤ (a - b) * (f' b - m)

Tactic:
simpa only [ContinuousLinearMap.smulRight_apply, one_apply_eq_self]
        using! hc.localize.hasFDerivWithinAt_nonneg (hg b (right_mem_Icc.2 hab)) this

Goal state after:
Module: Mathlib.Analysis.Calculus.Deriv.Abs

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
x : E
hf : HasStrictFDerivAt f f' x
h₀ : f x ≠ 0
⊢ HasStrictFDerivAt (fun x ↦ |f x|) (↑(SignType.sign (f x)) • f') x

Tactic:
convert! (hasStrictDerivAt_abs h₀).hasStrictFDerivAt.comp x hf using 1

Goal state after:
case e'_12
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
x : E
hf : HasStrictFDerivAt f f' x
h₀ : f x ≠ 0
e_8✝ : instAddCommGroup = normedAddCommGroup.toAddCommGroup
e_9✝ : Semiring.toModule ≍ RCLike.toInnerProductSpaceReal.toModule
⊢ ↑(SignType.sign (f x)) • f' = ContinuousLinearMap.toSpanSingleton ℝ ↑(SignType.sign (f x)) ∘SL f'
Module: Mathlib.Analysis.Calculus.ContDiff.Bounds

Goal state before:
pp: 𝕜 : 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 ∈ Finset.range (n + 1), ‖iteratedFDerivWithin 𝕜 i (fderivWithin 𝕜 g t ∘ f) s x‖ ≤ ↑i ! * C * D ^ i

Tactic:
intro i hi

Goal state after:
𝕜 : 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 ∈ Finset.range (n + 1)
⊢ ‖iteratedFDerivWithin 𝕜 i (fderivWithin 𝕜 g t ∘ f) s x‖ ≤ ↑i ! * C * D ^ i
Module: Mathlib.Analysis.Calculus.DerivativeTest

Goal state before:
pp: f : ℝ → ℝ
x₀ : ℝ
hf : deriv f x₀ > 0
hx : f x₀ = 0
⊢ ∀ᶠ (x : ℝ) in pure x₀, sign (f x) = sign (x - x₀)

Tactic:
simpa

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

Goal state before:
pp: f : ℝ → ℝ
x₀ : ℝ
hf : deriv f x₀ < 0
hx : f x₀ = 0
⊢ -f x₀ = 0

Tactic:
simpa

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

Goal state before:
pp: f : ℝ → ℝ
x₀ : ℝ
hf : deriv (deriv f) x₀ < 0
hd : deriv f x₀ = 0
hc : ContinuousAt f x₀
⊢ deriv (deriv (-f)) x₀ > 0

Tactic:
simpa

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

Goal state before:
pp: f : ℝ → ℝ
x₀ : ℝ
hf : deriv (deriv f) x₀ < 0
hd : deriv f x₀ = 0
hc : ContinuousAt f x₀
⊢ deriv (-f) x₀ = 0

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
inst✝⁶ : MetricSpace α
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : MeasurableSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : HasBesicovitchCovering α
μ : Measure α
inst✝¹ : SFinite μ
inst✝ : μ.OuterRegular
ε : ℝ≥0∞
hε : ε ≠ 0
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
u : Set α
su : u ⊇ s
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
μu : μ u ≤ μ s + ε / 2
R : α → ℝ
hR : ∀ x ∈ s, R x > 0 ∧ ball x (R x) ⊆ u
t0 : Set α
r0 : α → ℝ
t0_count : t0.Countable
t0s : t0 ⊆ s
hr0 : ∀ x ∈ t0, r0 x ∈ f x ∩ Ioo 0 (R x)
μt0 : μ (s \ ⋃ x ∈ t0, closedBall x (r0 x)) = 0
t0_disj : t0.PairwiseDisjoint fun x ↦ closedBall x (r0 x)
s' : Set α := s \ ⋃ x ∈ t0, closedBall x (r0 x)
s's : s' ⊆ s
N : ℕ
τ : ℝ
hτ : 1 < τ
H : IsEmpty (SatelliteConfig α N τ)
v : Set α
s'v : v ⊇ s'
v_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] v
μv : μ v ≤ μ s' + ε / 2 / ↑N
x : α
hx : x ∈ s'
r : ℝ
rpos : r > 0
hr : ball x r ⊆ v
R' : ℝ
hR' : R' ∈ f x ∩ Ioo 0 (min r 1)
⊢ ∃ r1 ∈ f x ∩ Ioo 0 1, closedBall x r1 ⊆ v

Tactic:
exact
      ⟨R', ⟨hR'.1, hR'.2.1, hR'.2.2.trans_le (min_le_right _ _)⟩,
        Subset.trans (closedBall_subset_ball (hR'.2.2.trans_le (min_le_left _ _))) hr⟩

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝⁶ : MetricSpace α
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : MeasurableSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : HasBesicovitchCovering α
μ : Measure α
inst✝¹ : SFinite μ
inst✝ : μ.OuterRegular
ε : ℝ≥0∞
hε : ε ≠ 0
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
u : Set α
su : u ⊇ s
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
μu : μ u ≤ μ s + ε / 2
R : α → ℝ
hR : ∀ x ∈ s, R x > 0 ∧ ball x (R x) ⊆ u
t0 : Set α
r0 : α → ℝ
t0_count : t0.Countable
t0s : t0 ⊆ s
hr0 : ∀ x ∈ t0, r0 x ∈ f x ∩ Ioo 0 (R x)
μt0 : μ (s \ ⋃ x ∈ t0, closedBall x (r0 x)) = 0
t0_disj : t0.PairwiseDisjoint fun x ↦ closedBall x (r0 x)
s' : Set α := s \ ⋃ x ∈ t0, closedBall x (r0 x)
s's : s' ⊆ s
N : ℕ
τ : ℝ
hτ : 1 < τ
H : IsEmpty (SatelliteConfig α N τ)
v : Set α
s'v : v ⊇ s'
v_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] v
μv : μ v ≤ μ s' + ε / 2 / ↑N
r1 : α → ℝ
hr1 : ∀ x ∈ s', r1 x ∈ f x ∩ Ioo 0 1 ∧ closedBall x (r1 x) ⊆ v
q : BallPackage (↑s') α := { c := fun x ↦ ↑x, r := fun x ↦ r1 ↑x, rpos := ⋯, r_bound := 1, r_le := ⋯ }
S : Fin N → Set ↑s'
S_disj : ∀ (i : Fin N), (S i).PairwiseDisjoint fun j ↦ closedBall (q.c j) (q.r j)
hS : range q.c ⊆ ⋃ i, ⋃ j ∈ S i, ball (q.c j) (q.r j)
S_count : ∀ (i : Fin N), (S i).Countable
r : α → ℝ := fun x ↦ if x ∈ s' then r1 x else r0 x
r_t0 : ∀ x ∈ t0, r x = r0 x
⊢ t0 ∪ ⋃ i, Subtype.val '' S i ⊆ s

Tactic:
simp only [t0s, true_and, union_subset_iff, image_subset_iff, iUnion_subset_iff]

Goal state after:
case refine_2
α : Type u_1
inst✝⁶ : MetricSpace α
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : MeasurableSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : HasBesicovitchCovering α
μ : Measure α
inst✝¹ : SFinite μ
inst✝ : μ.OuterRegular
ε : ℝ≥0∞
hε : ε ≠ 0
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
u : Set α
su : u ⊇ s
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
μu : μ u ≤ μ s + ε / 2
R : α → ℝ
hR : ∀ x ∈ s, R x > 0 ∧ ball x (R x) ⊆ u
t0 : Set α
r0 : α → ℝ
t0_count : t0.Countable
t0s : t0 ⊆ s
hr0 : ∀ x ∈ t0, r0 x ∈ f x ∩ Ioo 0 (R x)
μt0 : μ (s \ ⋃ x ∈ t0, closedBall x (r0 x)) = 0
t0_disj : t0.PairwiseDisjoint fun x ↦ closedBall x (r0 x)
s' : Set α := s \ ⋃ x ∈ t0, closedBall x (r0 x)
s's : s' ⊆ s
N : ℕ
τ : ℝ
hτ : 1 < τ
H : IsEmpty (SatelliteConfig α N τ)
v : Set α
s'v : v ⊇ s'
v_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] v
μv : μ v ≤ μ s' + ε / 2 / ↑N
r1 : α → ℝ
hr1 : ∀ x ∈ s', r1 x ∈ f x ∩ Ioo 0 1 ∧ closedBall x (r1 x) ⊆ v
q : BallPackage (↑s') α := { c := fun x ↦ ↑x, r := fun x ↦ r1 ↑x, rpos := ⋯, r_bound := 1, r_le := ⋯ }
S : Fin N → Set ↑s'
S_disj : ∀ (i : Fin N), (S i).PairwiseDisjoint fun j ↦ closedBall (q.c j) (q.r j)
hS : range q.c ⊆ ⋃ i, ⋃ j ∈ S i, ball (q.c j) (q.r j)
S_count : ∀ (i : Fin N), (S i).Countable
r : α → ℝ := fun x ↦ if x ∈ s' then r1 x else r0 x
r_t0 : ∀ x ∈ t0, r x = r0 x
⊢ ∀ (i : Fin N), S i ⊆ Subtype.val ⁻¹' s
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
s : Set E
x : E
f : E → 𝕜
hf : DifferentiableWithinAt 𝕜 f s x
hV : DifferentiableWithinAt 𝕜 V s x
hs : UniqueDiffWithinAt 𝕜 s x
⊢ -((fderivWithin 𝕜 f s x) (W x) • V x + f x • (-lieBracketWithin 𝕜 V W s) x) =
    -(fderivWithin 𝕜 f s x) (W x) • V x + f x • lieBracketWithin 𝕜 V W s x

Tactic:
add_comm

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

Tactic:
add_comm

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : E → E
x : E
f : E → 𝕜
hf : DifferentiableAt 𝕜 f x
hV : DifferentiableAt 𝕜 V x
⊢ -(f x • -lieBracket 𝕜 V W x + (fderiv 𝕜 f x) (W x) • V x) = -(fderiv 𝕜 f x) (W x) • V x + f x • lieBracket 𝕜 V W x