mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
h :
  ∀ (δ : ℝ),
    0 < δ → δ < 1 → ∃ s, (∀ c ∈ s, ‖c‖ ≤ 2) ∧ (∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 - δ ≤ ‖c - d‖) ∧ multiplicity E < s.card
N : ℕ := multiplicity E + 1
hN : N = multiplicity E + 1
F : ℝ → Fin N → E
hF : ∀ (δ : ℝ), 0 < δ → (∀ (i : Fin N), ‖F δ i‖ ≤ 2) ∧ Pairwise fun i j ↦ 1 - δ ≤ ‖F δ i - F δ j‖
f : Fin N → E
hf : ∀ (i : Fin N), ‖f i‖ ≤ 2
h'f : Pairwise fun i j ↦ 1 ≤ ‖f i - f j‖
finj : Function.Injective f
s : Finset E := Finset.image f Finset.univ
s_card : s.card = N
hs : ∀ c ∈ s, ‖c‖ ≤ 2
h's : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖
this : N ≤ multiplicity E
⊢ False

Tactic:
hN

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
h :
  ∀ (δ : ℝ),
    0 < δ → δ < 1 → ∃ s, (∀ c ∈ s, ‖c‖ ≤ 2) ∧ (∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 - δ ≤ ‖c - d‖) ∧ multiplicity E < s.card
N : ℕ := multiplicity E + 1
hN : N = multiplicity E + 1
F : ℝ → Fin N → E
hF : ∀ (δ : ℝ), 0 < δ → (∀ (i : Fin N), ‖F δ i‖ ≤ 2) ∧ Pairwise fun i j ↦ 1 - δ ≤ ‖F δ i - F δ j‖
f : Fin N → E
hf : ∀ (i : Fin N), ‖f i‖ ≤ 2
h'f : Pairwise fun i j ↦ 1 ≤ ‖f i - f j‖
finj : Function.Injective f
s : Finset E := Finset.image f Finset.univ
s_card : s.card = N
hs : ∀ c ∈ s, ‖c‖ ≤ 2
h's : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖
this : multiplicity E + 1 ≤ multiplicity E
⊢ False
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
this : (support fun i ↦ ρ (s ∩ ↑i • k)) = univ
⊢ m.Countable

Tactic:
this

Goal state after:
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 : univ.Countable
this : (support fun i ↦ ρ (s ∩ ↑i • k)) = univ
⊢ m.Countable
Module: Mathlib.Analysis.Calculus.ContDiff.Bounds

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
Du : Type u
inst✝⁷ : NormedAddCommGroup Du
inst✝⁶ : NormedSpace 𝕜 Du
s : Set Du
x : Du
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
IH :
  ∀ {Eu Fu Gu : Type u} [inst : NormedAddCommGroup Eu] [inst_1 : NormedSpace 𝕜 Eu] [inst_2 : NormedAddCommGroup Fu]
    [inst_3 : NormedSpace 𝕜 Fu] [inst_4 : NormedAddCommGroup Gu] [inst_5 : NormedSpace 𝕜 Gu] (B : Eu →L[𝕜] Fu →L[𝕜] Gu)
    {f : Du → Eu} {g : Du → Fu},
    ContDiffOn 𝕜 (↑n) f s →
      ContDiffOn 𝕜 (↑n) g s →
        ‖iteratedFDerivWithin 𝕜 n (fun y ↦ (B (f y)) (g y)) s x‖ ≤
          ‖B‖ *
            ∑ i ∈ Finset.range (n + 1),
              ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖
Eu Fu Gu : Type u
inst✝⁵ : NormedAddCommGroup Eu
inst✝⁴ : NormedSpace 𝕜 Eu
inst✝³ : NormedAddCommGroup Fu
inst✝² : NormedSpace 𝕜 Fu
inst✝¹ : NormedAddCommGroup Gu
inst✝ : NormedSpace 𝕜 Gu
B : Eu →L[𝕜] Fu →L[𝕜] Gu
f : Du → Eu
g : Du → Fu
hf : ContDiffOn 𝕜 (↑(n + 1)) f s
hg : ContDiffOn 𝕜 (↑(n + 1)) g s
In : ↑n + 1 ≤ ↑n.succ
⊢ ‖precompR Du B‖ *
      ∑ i ∈ Finset.range (n + 1),
        ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) (fderivWithin 𝕜 g s) s x‖ ≤
    ‖B‖ *
      ∑ i ∈ Finset.range (n + 1),
        ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) (fderivWithin 𝕜 g s) s x‖

Tactic:
by
            gcongr; exact B.norm_precompR_le Du

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁷ : NormedAddCommGroup D
inst✝⁶ : NormedSpace 𝕜 D
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
n : ℕ∞ω
inst✝¹ : CompleteSpace 𝕜
f : D → E →L[𝕜] F
inst✝ : FiniteDimensional 𝕜 E
⊢ ContDiff 𝕜 n f ↔ ∀ (y : E), ContDiff 𝕜 n fun x ↦ (f x) y

Tactic:
[

Goal state after:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁷ : NormedAddCommGroup D
inst✝⁶ : NormedSpace 𝕜 D
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
n : ℕ∞ω
inst✝¹ : CompleteSpace 𝕜
f : D → E →L[𝕜] F
inst✝ : FiniteDimensional 𝕜 E
⊢ ContDiff 𝕜 n f ↔ ∀ (y : E), ContDiff 𝕜 n fun x ↦ (f x) y
Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace

Goal state before:
pp: case inl
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 : ‖a.c j‖ ≤ 2
⊢ 1 - δ ≤ ‖c' i - c' j‖

Tactic:
[

Goal state after:
case inl
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 : ‖a.c j‖ ≤ 2
⊢ 1 - δ ≤ ‖c' i - c' j‖
Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace

Goal state before:
pp: case inr.inl
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‖
H'j : ‖a.c j‖ ≤ 2 ↔ False
Hi : ‖a.c i‖ ≤ 2
⊢ 1 - δ ≤ ‖c' i - c' j‖

Tactic:
[

Goal state after:
case inr.inl
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‖
H'j : ‖a.c j‖ ≤ 2 ↔ False
Hi : ‖a.c i‖ ≤ 2
⊢ 1 - δ ≤ ‖c' i - c' j‖
Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace

Goal state before:
pp: case inr.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‖
H'j : ‖a.c j‖ ≤ 2 ↔ False
Hi : 2 < ‖a.c i‖
H'i : ‖a.c i‖ ≤ 2 ↔ False
⊢ 1 - δ ≤ ‖c' i - c' j‖

Tactic:
[

Goal state after:
case inr.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‖
H'j : ‖a.c j‖ ≤ 2 ↔ False
Hi : 2 < ‖a.c i‖
H'i : ‖a.c i‖ ≤ 2 ↔ False
⊢ 1 - δ ≤ ‖c' i - c' j‖
Module: Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
α : ↑I
f : E → F
a : E
hfc : ContDiffAt ℝ 0 f a
⊢ ((fun x ↦ ‖(continuousMultilinearCurryFin0 ℝ E F).symm (f x - f a)‖) =O[𝓝 a] fun x ↦ ‖x - a‖ ^ ↑α) ↔
    (fun x ↦ f x - f a) =O[𝓝 a] fun x ↦ ‖x - a‖ ^ ↑α

Tactic:
[

Goal state after:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
α : ↑I
f : E → F
a : E
hfc : ContDiffAt ℝ 0 f a
⊢ ((fun x ↦ ‖(continuousMultilinearCurryFin0 ℝ E F).symm (f x - f a)‖) =O[𝓝 a] fun x ↦ ‖x - a‖ ^ ↑α) ↔
    (fun x ↦ f x - f a) =O[𝓝 a] fun x ↦ ‖x - a‖ ^ ↑α
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:
[

Goal state after:
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}
Module: Mathlib.Topology.MetricSpace.Holder

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁴ : PseudoMetricSpace X
inst✝³ : SeminormedAddCommGroup Y
C r : ℝ≥0
f : X → Y
α : Type u_4
inst✝² : SeminormedRing α
inst✝¹ : Module α Y
inst✝ : NormSMulClass α Y
a : α
ha : ‖a‖₊ ≠ 0
⊢ HolderWith (C * ‖a‖₊) r (a • f) ↔ HolderWith C r f

Tactic:
[

Goal state after:
X : Type u_1
Y : Type u_2
inst✝⁴ : PseudoMetricSpace X
inst✝³ : SeminormedAddCommGroup Y
C r : ℝ≥0
f : X → Y
α : Type u_4
inst✝² : SeminormedRing α
inst✝¹ : Module α Y
inst✝ : NormSMulClass α Y
a : α
ha : ‖a‖₊ ≠ 0
⊢ HolderWith (C * ‖a‖₊) r (a • f) ↔ HolderWith C r f
Module: Mathlib.Analysis.Calculus.ContDiff.Bounds

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁷ : NormedAddCommGroup D
inst✝⁶ : NormedSpace 𝕜 D
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
f : D → E
g : D → F
N : ℕ∞ω
hf : ContDiff 𝕜 N f
hg : ContDiff 𝕜 N g
x : D
n : ℕ
hn : ↑n ≤ N
⊢ ‖iteratedFDeriv 𝕜 n (fun y ↦ (B (f y)) (g y)) x‖ ≤
    ‖B‖ * ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDeriv 𝕜 i f x‖ * ‖iteratedFDeriv 𝕜 (n - i) g x‖

Tactic:
[

Goal state after:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁷ : NormedAddCommGroup D
inst✝⁶ : NormedSpace 𝕜 D
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
f : D → E
g : D → F
N : ℕ∞ω
hf : ContDiff 𝕜 N f
hg : ContDiff 𝕜 N g
x : D
n : ℕ
hn : ↑n ≤ N
⊢ ‖iteratedFDeriv 𝕜 n (fun y ↦ (B (f y)) (g y)) x‖ ≤
    ‖B‖ * ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDeriv 𝕜 i f x‖ * ‖iteratedFDeriv 𝕜 (n - i) g x‖
Module: Mathlib.Analysis.Calculus.ContDiff.Bounds

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁷ : NormedAddCommGroup D
inst✝⁶ : NormedSpace 𝕜 D
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
f : D → E
g : D → F
N : ℕ∞ω
hf : ContDiff 𝕜 N f
hg : ContDiff 𝕜 N g
x : D
n : ℕ
hn : ↑n ≤ N
hB : ‖B‖ ≤ 1
⊢ ‖iteratedFDeriv 𝕜 n (fun y ↦ (B (f y)) (g y)) x‖ ≤
    ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDeriv 𝕜 i f x‖ * ‖iteratedFDeriv 𝕜 (n - i) g x‖

Tactic:
[

Goal state after:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁷ : NormedAddCommGroup D
inst✝⁶ : NormedSpace 𝕜 D
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
f : D → E
g : D → F
N : ℕ∞ω
hf : ContDiff 𝕜 N f
hg : ContDiff 𝕜 N g
x : D
n : ℕ
hn : ↑n ≤ N
hB : ‖B‖ ≤ 1
⊢ ‖iteratedFDeriv 𝕜 n (fun y ↦ (B (f y)) (g y)) x‖ ≤
    ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDeriv 𝕜 i f x‖ * ‖iteratedFDeriv 𝕜 (n - i) g x‖
Module: Mathlib.Analysis.Calculus.ContDiff.Bounds

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
A : Type u_3
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
f g : E → A
N : ℕ∞ω
hf : ContDiff 𝕜 N f
hg : ContDiff 𝕜 N g
x : E
n : ℕ
hn : ↑n ≤ N
⊢ ‖iteratedFDeriv 𝕜 n (fun y ↦ f y * g y) x‖ ≤
    ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDeriv 𝕜 i f x‖ * ‖iteratedFDeriv 𝕜 (n - i) g x‖

Tactic:
[

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
A : Type u_3
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
f g : E → A
N : ℕ∞ω
hf : ContDiff 𝕜 N f
hg : ContDiff 𝕜 N g
x : E
n : ℕ
hn : ↑n ≤ N
⊢ ‖iteratedFDeriv 𝕜 n (fun y ↦ f y * g y) x‖ ≤
    ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDeriv 𝕜 i f x‖ * ‖iteratedFDeriv 𝕜 (n - i) g x‖
Module: Mathlib.Analysis.Calculus.DerivativeTest

Goal state before:
pp: f : ℝ → ℝ
b : ℝ
h : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Iio b)
⊢ ContinuousOn f (Iic b)

Tactic:
[

Goal state after:
f : ℝ → ℝ
b : ℝ
h : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Iio b)
⊢ ContinuousOn f (Iic b)
Module: Mathlib.Analysis.Calculus.DerivativeTest

Goal state before:
pp: f : ℝ → ℝ
a b : ℝ
hb : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioi b)
h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioi b, deriv f x ≤ 0
⊢ IsMaxOn f (Ioi a) b

Tactic:
by
  refine isMaxOn_Ioi_of_mono_anti ?_ ?_
  · apply monotoneOn_of_deriv_nonneg (convex_Ioc a b) (continuousOn_Ioc hb hd₀) <;> simp_all
  · apply antitoneOn_of_deriv_nonpos (convex_Ici b) (continuousOn_Ici hb hd₁) <;> simp_all

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

Goal state before:
pp: case hC
𝕜 : 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 : j ≤ i
this : ‖iteratedFDerivWithin 𝕜 j (fderivWithin 𝕜 g t) t (f x)‖ = ‖iteratedFDerivWithin 𝕜 (j + 1) g t (f x)‖
⊢ ‖iteratedFDerivWithin 𝕜 j (fderivWithin 𝕜 g t) t (f x)‖ ≤ C

Tactic:
this

Goal state after:
case hC
𝕜 : 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 : j ≤ i
this : ‖iteratedFDerivWithin 𝕜 j (fderivWithin 𝕜 g t) t (f x)‖ = ‖iteratedFDerivWithin 𝕜 (j + 1) g t (f x)‖
⊢ ‖iteratedFDerivWithin 𝕜 (j + 1) g t (f x)‖ ≤ C
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 : ∀ i ∈ Finset.range (n + 1), ‖iteratedFDerivWithin 𝕜 i (fderivWithin 𝕜 g t ∘ f) s x‖ ≤ ↑i ! * C * D ^ i
i : ℕ
this : ‖iteratedFDerivWithin 𝕜 (n - i + 1) f s x‖ ≤ D ^ (n - i + 1)
⊢ ‖iteratedFDerivWithin 𝕜 (n - i) (fderivWithin 𝕜 f s) s x‖ ≤ D ^ (n - i + 1)

Tactic:
simpa [iteratedFDerivWithin_succ_eq_comp_right hs hx]

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 t : Set E
f : E → F
x : E
h : t ∈ 𝓝[s] x
hf : ContDiffWithinAt 𝕜 2 f t x
hs : UniqueDiffOn 𝕜 s
ht : UniqueDiffOn 𝕜 t
hx : x ∈ s
A : ∀ᶠ (y : E) in 𝓝[s] x, fderivWithin 𝕜 f s y = fderivWithin 𝕜 f t y
this : fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x = fderivWithin 𝕜 (fderivWithin 𝕜 f t) s x
⊢ fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x = fderivWithin 𝕜 (fderivWithin 𝕜 f t) t x

Tactic:
this

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 t : Set E
f : E → F
x : E
h : t ∈ 𝓝[s] x
hf : ContDiffWithinAt 𝕜 2 f t x
hs : UniqueDiffOn 𝕜 s
ht : UniqueDiffOn 𝕜 t
hx : x ∈ s
A : ∀ᶠ (y : E) in 𝓝[s] x, fderivWithin 𝕜 f s y = fderivWithin 𝕜 f t y
this : fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x = fderivWithin 𝕜 (fderivWithin 𝕜 f t) s x
⊢ fderivWithin 𝕜 (fderivWithin 𝕜 f t) s x = fderivWithin 𝕜 (fderivWithin 𝕜 f t) t x
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
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
⊢ IsSymmSndFDerivWithinAt 𝕜 f s x ↔
    ContinuousMultilinearMap.domDomCongr Fin.revPerm (iteratedFDerivWithin 𝕜 2 f s x) = iteratedFDerivWithin 𝕜 2 f s x

Tactic:
[

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
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
⊢ IsSymmSndFDerivWithinAt 𝕜 f s x ↔
    ContinuousMultilinearMap.domDomCongr Fin.revPerm (iteratedFDerivWithin 𝕜 2 f s x) = iteratedFDerivWithin 𝕜 2 f s x
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 v w : E
hf : IsSymmSndFDerivWithinAt 𝕜 f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
⊢ (iteratedFDerivWithin 𝕜 2 f s x) ![v, w] = (iteratedFDerivWithin 𝕜 2 f s x) ![w, v]

Tactic:
[

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 v w : E
hf : IsSymmSndFDerivWithinAt 𝕜 f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
⊢ (iteratedFDerivWithin 𝕜 2 f s x) ![v, w] = (iteratedFDerivWithin 𝕜 2 f s x) ![w, v]
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
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
x : α
hx : x ∈ t0
this : x ∉ s'
⊢ r x = r0 x

Tactic:
simp [r, this]

Goal state after: