mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.ContDiff.Bounds

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
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
g : F → G
f : E → F
n : ℕ
s : Set E
t : Set F
x : E
N : ℕ∞ω
hg : ContDiffOn 𝕜 N g t
hf : ContDiffOn 𝕜 N f s
hn : ↑n ≤ N
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
hC : ∀ i ≤ n, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C
hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i
Fu : Type (max uF uG) := ULift.{uG, uF} F
Gu : Type (max uF uG) := ULift.{uF, uG} G
isoF : Fu ≃ₗᵢ[𝕜] F
isoG : Gu ≃ₗᵢ[𝕜] G
fu : E → Fu := ⇑isoF.symm ∘ f
gu : Fu → Gu := ⇑isoG.symm ∘ g ∘ ⇑isoF
tu : Set Fu := ⇑isoF ⁻¹' t
htu : UniqueDiffOn 𝕜 tu
hstu : MapsTo fu s tu
Ffu : isoF (fu x) = f x
hfu : ContDiffOn 𝕜 (↑n) fu s
hgu : ContDiffOn 𝕜 (↑n) gu tu
Nfu : ∀ (i : ℕ), ‖iteratedFDerivWithin 𝕜 i fu s x‖ = ‖iteratedFDerivWithin 𝕜 i f s x‖
⊢ ‖iteratedFDerivWithin 𝕜 n (g ∘ f) s x‖ ≤ ↑n ! * C * D ^ n

Tactic:
[

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
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
g : F → G
f : E → F
n : ℕ
s : Set E
t : Set F
x : E
N : ℕ∞ω
hg : ContDiffOn 𝕜 N g t
hf : ContDiffOn 𝕜 N f s
hn : ↑n ≤ N
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
hC : ∀ i ≤ n, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C
hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i
Fu : Type (max uF uG) := ULift.{uG, uF} F
Gu : Type (max uF uG) := ULift.{uF, uG} G
isoF : Fu ≃ₗᵢ[𝕜] F
isoG : Gu ≃ₗᵢ[𝕜] G
fu : E → Fu := ⇑isoF.symm ∘ f
gu : Fu → Gu := ⇑isoG.symm ∘ g ∘ ⇑isoF
tu : Set Fu := ⇑isoF ⁻¹' t
htu : UniqueDiffOn 𝕜 tu
hstu : MapsTo fu s tu
Ffu : isoF (fu x) = f x
hfu : ContDiffOn 𝕜 (↑n) fu s
hgu : ContDiffOn 𝕜 (↑n) gu tu
Nfu : ∀ (i : ℕ), ‖iteratedFDerivWithin 𝕜 i fu s x‖ = ‖iteratedFDerivWithin 𝕜 i f s x‖
⊢ ‖iteratedFDerivWithin 𝕜 n (g ∘ f) s x‖ ≤ ↑n ! * C * D ^ n
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
f : E → F
x : E
hf : ContDiffAt 𝕜 ω f x
⊢ IsSymmSndFDerivAt 𝕜 f x

Tactic:
simp only [← isSymmSndFDerivWithinAt_univ, ← contDiffWithinAt_univ] at hf ⊢

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
f : E → F
x : E
hf : ContDiffWithinAt 𝕜 ω f univ x
⊢ IsSymmSndFDerivWithinAt 𝕜 f univ 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
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : F → G
f : E → F
n : ℕ
s : Set E
t : Set F
x : E
N : ℕ∞ω
hg : ContDiffOn 𝕜 N g t
hf : ContDiffOn 𝕜 N f s
hn : ↑n ≤ N
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
hC : ∀ i ≤ n, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C
Fu : Type (max uF uG) := ULift.{uG, uF} F
Gu : Type (max uF uG) := ULift.{uF, uG} G
isoF : Fu ≃ₗᵢ[𝕜] F
isoG : Gu ≃ₗᵢ[𝕜] G
fu : E → Fu := ⇑isoF.symm ∘ f
gu : Fu → Gu := ⇑isoG.symm ∘ g ∘ ⇑isoF
tu : Set Fu := ⇑isoF ⁻¹' t
htu : UniqueDiffOn 𝕜 tu
hstu : MapsTo fu s tu
Ffu : isoF (fu x) = f x
hfu : ContDiffOn 𝕜 (↑n) fu s
hgu : ContDiffOn 𝕜 (↑n) gu tu
Nfu : ∀ (i : ℕ), ‖iteratedFDerivWithin 𝕜 i fu s x‖ = ‖iteratedFDerivWithin 𝕜 i f s x‖
hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDerivWithin 𝕜 i fu s x‖ ≤ D ^ i
Ngu : ∀ (i : ℕ), ‖iteratedFDerivWithin 𝕜 i gu tu (fu x)‖ = ‖iteratedFDerivWithin 𝕜 i g t (f x)‖
⊢ ‖iteratedFDerivWithin 𝕜 n (g ∘ f) s x‖ ≤ ↑n ! * C * D ^ n

Tactic:
[

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
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
g : F → G
f : E → F
n : ℕ
s : Set E
t : Set F
x : E
N : ℕ∞ω
hg : ContDiffOn 𝕜 N g t
hf : ContDiffOn 𝕜 N f s
hn : ↑n ≤ N
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
hC : ∀ i ≤ n, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C
Fu : Type (max uF uG) := ULift.{uG, uF} F
Gu : Type (max uF uG) := ULift.{uF, uG} G
isoF : Fu ≃ₗᵢ[𝕜] F
isoG : Gu ≃ₗᵢ[𝕜] G
fu : E → Fu := ⇑isoF.symm ∘ f
gu : Fu → Gu := ⇑isoG.symm ∘ g ∘ ⇑isoF
tu : Set Fu := ⇑isoF ⁻¹' t
htu : UniqueDiffOn 𝕜 tu
hstu : MapsTo fu s tu
Ffu : isoF (fu x) = f x
hfu : ContDiffOn 𝕜 (↑n) fu s
hgu : ContDiffOn 𝕜 (↑n) gu tu
Nfu : ∀ (i : ℕ), ‖iteratedFDerivWithin 𝕜 i fu s x‖ = ‖iteratedFDerivWithin 𝕜 i f s x‖
hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDerivWithin 𝕜 i fu s x‖ ≤ D ^ i
Ngu : ∀ (i : ℕ), ‖iteratedFDerivWithin 𝕜 i gu tu (fu x)‖ = ‖iteratedFDerivWithin 𝕜 i g t (f x)‖
⊢ ‖iteratedFDerivWithin 𝕜 n (g ∘ f) s x‖ ≤ ↑n ! * C * D ^ n
Module: Mathlib.Analysis.Calculus.ContDiff.Bounds

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
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
g : F → G
f : E → F
n : ℕ
N : ℕ∞ω
t : Set F
ht : range f ⊆ t
ht' : UniqueDiffOn 𝕜 t
hg : ContDiffOn 𝕜 N g t
hf : ContDiff 𝕜 N f
hn : ↑n ≤ N
x : E
C D : ℝ
hC : ∀ i ≤ n, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C
hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDeriv 𝕜 i f x‖ ≤ D ^ i
⊢ ‖iteratedFDeriv 𝕜 n (g ∘ f) x‖ ≤ ↑n ! * C * D ^ n

Tactic:
[

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
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
g : F → G
f : E → F
n : ℕ
N : ℕ∞ω
t : Set F
ht : range f ⊆ t
ht' : UniqueDiffOn 𝕜 t
hg : ContDiffOn 𝕜 N g t
hf : ContDiff 𝕜 N f
hn : ↑n ≤ N
x : E
C D : ℝ
hC : ∀ i ≤ n, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C
hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDeriv 𝕜 i f x‖ ≤ D ^ i
⊢ ‖iteratedFDeriv 𝕜 n (g ∘ f) x‖ ≤ ↑n ! * C * D ^ n
Module: Mathlib.Analysis.Calculus.ContDiff.Bounds

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
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
g : F → G
f : E → F
n : ℕ
N : ℕ∞ω
hg : ContDiff 𝕜 N g
hf : ContDiff 𝕜 N f
hn : ↑n ≤ N
x : E
C D : ℝ
hC : ∀ i ≤ n, ‖iteratedFDeriv 𝕜 i g (f x)‖ ≤ C
hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDeriv 𝕜 i f x‖ ≤ D ^ i
⊢ ‖iteratedFDeriv 𝕜 n (g ∘ f) x‖ ≤ ↑n ! * C * D ^ n

Tactic:
[

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
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
g : F → G
f : E → F
n : ℕ
N : ℕ∞ω
hg : ContDiff 𝕜 N g
hf : ContDiff 𝕜 N f
hn : ↑n ≤ N
x : E
C D : ℝ
hC : ∀ i ≤ n, ‖iteratedFDeriv 𝕜 i g (f x)‖ ≤ C
hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDeriv 𝕜 i f x‖ ≤ D ^ i
⊢ ‖iteratedFDeriv 𝕜 n (g ∘ f) x‖ ≤ ↑n ! * C * D ^ n
Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric

Goal state before:
pp: case hf.hf.hf.refine_2
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
t : ℝ
ht : t ∈ Icc 0 1
⊢ HasDerivWithinAt (fun t ↦ x + h • v + (t * h) • w) (h • w) (Icc 0 1) t

Tactic:
apply_rules [HasDerivAt.hasDerivWithinAt, HasDerivAt.const_add, HasDerivAt.smul_const,
        hasDerivAt_mul_const]

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

Goal state before:
pp: case pos.refine_1
α : 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
x : α
hx : x ∈ s
h'x : x ∈ s'
i : Fin N
y : ↑s'
ySi : y ∈ S i
xy : x ∈ ball (↑y) (r1 ↑y)
⊢ ↑y ∈ ⋃ i, Subtype.val '' S i

Tactic:
simp only [mem_iUnion, mem_image]
        exact ⟨i, y, ySi, rfl⟩

Goal state after:
Module: Mathlib.Analysis.Calculus.DifferentialForm.Basic

Goal state before:
pp: case hsymm
𝕜 : 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
⊢ ∀ (x_1 y : E), ((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) x_1) y = ((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) y) x_1

Tactic:
· apply hf.isSymmSndFDerivWithinAt <;> assumption

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : E → E
x : E
f : E → 𝕜
hf : DifferentiableAt 𝕜 f x
hW : DifferentiableAt 𝕜 W x
⊢ lieBracket 𝕜 V (fun y ↦ f y • W y) x = (fderiv 𝕜 f x) (V x) • W x + f x • lieBracket 𝕜 V W x

Tactic:
[

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
hW : DifferentiableAt 𝕜 W x
⊢ lieBracket 𝕜 V (fun y ↦ f y • W y) x = (fderiv 𝕜 f x) (V x) • W x + f x • lieBracket 𝕜 V W x
Module: Mathlib.Analysis.Calculus.VectorField

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : E → E
x : E
m n : ℕ∞ω
hV : ContDiffWithinAt 𝕜 n V univ x
hW : ContDiffWithinAt 𝕜 n W univ x
hmn : m + 1 ≤ n
⊢ ContDiffWithinAt 𝕜 m (lieBracket 𝕜 V W) univ x

Tactic:
[

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : E → E
x : E
m n : ℕ∞ω
hV : ContDiffWithinAt 𝕜 n V univ x
hW : ContDiffWithinAt 𝕜 n W univ x
hmn : m + 1 ≤ n
⊢ ContDiffWithinAt 𝕜 m (lieBracket 𝕜 V W) univ x
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
r_t0 : ∀ x ∈ t0, r x = r0 x
A : ∑' (x : ↑t0), μ (closedBall (↑x) (r ↑x)) ≤ μ s + ε / 2
i : Fin N
⊢ ∑' (x : ↑(S i)), μ (closedBall (↑↑x) (r1 ↑↑x)) = μ (⋃ x, closedBall (↑↑x) (r1 ↑↑x))

Tactic:
by
          have : Encodable (S i) := (S_count i).toEncodable
          rw [measure_iUnion]
          · exact (pairwise_subtype_iff_pairwise_set _ _).2 (S_disj i)
          · exact fun i => measurableSet_closedBall

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
hx : 0 < ‖x‖
h : DifferentiableAt ℝ (fun x ↦ ‖x‖) 0
this : DifferentiableAt ℝ (fun t ↦ ‖t • x‖) 0
⊢ DifferentiableAt ℝ (fun x ↦ |x|) 0

Tactic:
[

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
hx : 0 < ‖x‖
h : DifferentiableAt ℝ (fun x ↦ ‖x‖) 0
this : DifferentiableAt ℝ (fun t ↦ ‖t • x‖) 0
⊢ DifferentiableAt ℝ (fun x ↦ |x|) 0
Module: Mathlib.Analysis.Calculus.FDeriv.Partial

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
u : E
v w : α → E
l : Filter α
hv : Tendsto v l (𝓝 u)
hw : Tendsto w l (𝓝 u)
s : Set E
seg : ∀ᶠ (χ : α) in l, [w χ -[ℝ] v χ] ⊆ s
f : α → E → F
f' : α → E → E →L[𝕜] F
φ : E →L[𝕜] F
cf' : Tendsto (↿f') (l ×ˢ 𝓝[s] u) (𝓝 φ)
ε : ℝ
hε : 0 < ε
df' : ∀ᶠ (χ : α) in l, ∀ z ∈ [w χ -[ℝ] v χ], HasFDerivWithinAt (f χ) (f' χ z) s z
⊢ ∀ᶠ (χ : α) in l, ∀ z ∈ [w χ -[ℝ] v χ], ‖f' χ z - φ‖ < ε

Tactic:
[

Goal state after:
α : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
u : E
v w : α → E
l : Filter α
hv : Tendsto v l (𝓝 u)
hw : Tendsto w l (𝓝 u)
s : Set E
seg : ∀ᶠ (χ : α) in l, [w χ -[ℝ] v χ] ⊆ s
f : α → E → F
f' : α → E → E →L[𝕜] F
φ : E →L[𝕜] F
cf' : Tendsto (↿f') (l ×ˢ 𝓝[s] u) (𝓝 φ)
ε : ℝ
hε : 0 < ε
df' : ∀ᶠ (χ : α) in l, ∀ z ∈ [w χ -[ℝ] v χ], HasFDerivWithinAt (f χ) (f' χ z) s z
⊢ ∀ᶠ (χ : α) in l, ∀ z ∈ [w χ -[ℝ] v χ], ‖f' χ z - φ‖ < ε
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: case inr
α : 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
r : ℝ
rpos : 0 < r
tf : closedBall x r ∈ f x
ht : closedBall x r ⊆ closedBall x (δ / 2)
H : δ / 2 ≤ r
this : closedBall x r = closedBall x (δ / 2)
⊢ (g x ∩ Ioo 0 δ).Nonempty

Tactic:
this

Goal state after:
case inr
α : 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
r : ℝ
rpos : 0 < r
tf : closedBall x (δ / 2) ∈ f x
ht : closedBall x r ⊆ closedBall x (δ / 2)
H : δ / 2 ≤ r
this : closedBall x r = closedBall x (δ / 2)
⊢ (g x ∩ Ioo 0 δ).Nonempty
Module: Mathlib.Analysis.Calculus.FDeriv.Norm

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x ↦ ‖x‖) x
this : ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖
⊢ deriv (fun t ↦ ‖x + t • x‖) 0 = ‖x‖

Tactic:
[

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x ↦ ‖x‖) x
this : ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖
⊢ deriv (fun t ↦ ‖x + t • x‖) 0 = ‖x‖
Module: Mathlib.Analysis.Calculus.FDeriv.Norm

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x ↦ ‖x‖) x
this : ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖
⊢ deriv (fun t ↦ ‖x + t • x‖) 0 = ‖x‖

Tactic:
this

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x ↦ ‖x‖) x
this : ∀ (t : ℝ), ‖x + t • x‖ = |1 + t| * ‖x‖
⊢ deriv (fun t ↦ |1 + t| * ‖x‖) 0 = ‖x‖
Module: Mathlib.Analysis.Calculus.FDeriv.Norm

Goal state before:
pp: case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
t : ℝ
h✝ : Subsingleton E
⊢ fderiv ℝ (fun x ↦ ‖x‖) (t • x) = ↑(SignType.sign t) • fderiv ℝ (fun x ↦ ‖x‖) x

Tactic:
[

Goal state after:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
t : ℝ
h✝ : Subsingleton E
⊢ fderiv ℝ (fun x ↦ ‖x‖) (t • x) = ↑(SignType.sign t) • fderiv ℝ (fun x ↦ ‖x‖) x
Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff

Goal state before:
pp: case hf₀'
𝕂 : Type u_1
inst✝⁵ : RCLike 𝕂
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕂 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕂 F
inst✝ : CompleteSpace E
f : E → F
f' : E ≃L[𝕂] F
a : E
n : WithTop ℕ∞
hf : ContDiffAt 𝕂 n f a
hf' : HasFDerivAt f (↑f') a
hn : n ≠ 0
this : hf.localInverse hf' hn (f a) = a
⊢ HasFDerivAt (↑(toOpenPartialHomeomorph f hf hf' hn)) (↑?m.110) (↑(toOpenPartialHomeomorph f hf hf' hn).symm (f a))

pp: case hf
𝕂 : Type u_1
inst✝⁵ : RCLike 𝕂
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕂 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕂 F
inst✝ : CompleteSpace E
f : E → F
f' : E ≃L[𝕂] F
a : E
n : WithTop ℕ∞
hf : ContDiffAt 𝕂 n f a
hf' : HasFDerivAt f (↑f') a
hn : n ≠ 0
this : hf.localInverse hf' hn (f a) = a
⊢ ContDiffAt 𝕂 n (↑(toOpenPartialHomeomorph f hf hf' hn)) (↑(toOpenPartialHomeomorph f hf hf' hn).symm (f a))

pp: 𝕂 : Type u_1
inst✝⁵ : RCLike 𝕂
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕂 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕂 F
inst✝ : CompleteSpace E
f : E → F
f' : E ≃L[𝕂] F
a : E
n : WithTop ℕ∞
hf : ContDiffAt 𝕂 n f a
hf' : HasFDerivAt f (↑f') a
hn : n ≠ 0
this : hf.localInverse hf' hn (f a) = a
⊢ E ≃L[𝕂] F

Tactic:
· convert! hf'

Goal state after:
case hf
𝕂 : Type u_1
inst✝⁵ : RCLike 𝕂
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕂 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕂 F
inst✝ : CompleteSpace E
f : E → F
f' : E ≃L[𝕂] F
a : E
n : WithTop ℕ∞
hf : ContDiffAt 𝕂 n f a
hf' : HasFDerivAt f (↑f') a
hn : n ≠ 0
this : hf.localInverse hf' hn (f a) = a
⊢ ContDiffAt 𝕂 n (↑(toOpenPartialHomeomorph f hf hf' hn)) (↑(toOpenPartialHomeomorph f hf hf' hn).symm (f a))
Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : FiniteDimensional ℝ F
s : Set E
f : E → F
f' : E ≃L[ℝ] F
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ lipschitzExtensionConstant F * c < ‖↑f'.symm‖₊⁻¹
u : E → F
hu : LipschitzWith (lipschitzExtensionConstant F * c) u
uf : EqOn (f - ⇑f') u s
g : E → F := fun x ↦ f' x + u x
x : E
hx : x ∈ s
⊢ f x = g x

Tactic:
[

Goal state after:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : FiniteDimensional ℝ F
s : Set E
f : E → F
f' : E ≃L[ℝ] F
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ lipschitzExtensionConstant F * c < ‖↑f'.symm‖₊⁻¹
u : E → F
hu : LipschitzWith (lipschitzExtensionConstant F * c) u
uf : EqOn (f - ⇑f') u s
g : E → F := fun x ↦ f' x + u x
x : E
hx : x ∈ s
⊢ f x = g x