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‖
i j : Fin N
hij : f i = f j
h : ¬i = j
this : 1 ≤ ‖f i - f j‖
⊢ False

Tactic:
simp only [hij, norm_zero, sub_self] at this

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‖
i j : Fin N
hij : f i = f j
h : ¬i = j
this : 1 ≤ 0
⊢ False
Module: Mathlib.Analysis.Calculus.Conformal.NormedSpace

Goal state before:
pp: case neg
X : Type u_1
Y : Type u_2
inst✝³ : NormedAddCommGroup X
inst✝² : NormedAddCommGroup Y
inst✝¹ : NormedSpace ℝ X
inst✝ : NormedSpace ℝ Y
f : X → Y
x : X
H : IsConformalMap (fderiv ℝ f x)
h : ¬DifferentiableAt ℝ f x
⊢ ConformalAt f x

Tactic:
nontriviality X
      exact absurd (fderiv_zero_of_not_differentiableAt h) H.ne_zero

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
n : ℕ
f : Fin n → E
h✝ : ∀ (i : Fin n), ‖f i‖ ≤ 2
h' : Pairwise fun i j ↦ 1 - goodδ E ≤ ‖f i - f j‖
i j : Fin n
hij : f i = f j
h : ¬i = j
this : 1 - goodδ E ≤ ‖f i - f j‖
⊢ False

Tactic:
simp only [hij, norm_zero, sub_self] at this

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
n : ℕ
f : Fin n → E
h✝ : ∀ (i : Fin n), ‖f i‖ ≤ 2
h' : Pairwise fun i j ↦ 1 - goodδ E ≤ ‖f i - f j‖
i j : Fin n
hij : f i = f j
h : ¬i = j
this : 1 - goodδ E ≤ 0
⊢ False
Module: Mathlib.Topology.MetricSpace.Holder

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
C r : ℝ≥0
f : X → Y
x : X
⊢ HolderOnWith C r f {x}

Tactic:
by
  simp [HolderOnWith]

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
A : Set X
r : ℝ≥0
hr : r ∈ {r | HolderOnWith C r f A}
⊢ StarConvex ℝ≥0 r {r | HolderOnWith C r f A}

Tactic:
s

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
f : X → Y
C : ℝ≥0
A : Set X
r : ℝ≥0
hr : r ∈ {r | HolderOnWith C r f A}
s : ℝ≥0
⊢ s ∈ {r | HolderOnWith C r f A} → ∀ ⦃a b : ℝ≥0⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • r + b • s ∈ {r | HolderOnWith C r f A}
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 : ℝ
hd : dist x y ≤ d
⊢ dist (f x) (f y) ≤ ↑C * d ^ ↑r

Tactic:
by
  lift d to ℝ≥0 using dist_nonneg.trans hd
  rw [dist_nndist] at hd ⊢
  norm_cast at hd ⊢
  exact hf.nndist_le_of_le hx hy hd

Goal state after:
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✝² : SeminormedAddCommGroup α
inst✝¹ : SMulZeroClass α Y
inst✝ : IsBoundedSMul α Y
a : α
hf : HolderWith C r f
x₁ x₂ : X
⊢ edist ((a • f) x₁) ((a • f) x₂) ≤ ↑(C * ‖a‖₊) * edist x₁ x₂ ^ ↑r

Tactic:
by
  refine edist_smul_le _ _ _ |>.trans ?_
  rw [ENNReal.coe_mul, ENNReal.smul_def, smul_eq_mul, mul_comm (C : ℝ≥0∞), mul_assoc]
  gcongr
  exact hf x₁ x₂

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✝ : IsFiniteMeasure μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
P : Finset (α × ℝ) → Prop :=
  fun t ↦ ((↑t).PairwiseDisjoint fun p ↦ closedBall p.1 p.2) ∧ (∀ p ∈ t, p.1 ∈ s) ∧ ∀ p ∈ t, p.2 ∈ f p.1
F : Finset (α × ℝ) → Finset (α × ℝ)
hF :
  ∀ (t : Finset (α × ℝ)),
    P t →
      t ⊆ F t ∧ P (F t) ∧ μ (s \ ⋃ p ∈ F t, closedBall p.1 p.2) ≤ ↑N / (↑N + 1) * μ (s \ ⋃ p ∈ t, closedBall p.1 p.2)
u : ℕ → Finset (α × ℝ) := fun n ↦ F^[n] ∅
u_succ : ∀ (n : ℕ), u n.succ = F (u n)
Pu : ∀ (n : ℕ), P (u n)
A : ∀ (n : ℕ), μ (s \ ⋃ p ∈ ⋃ n, ↑(u n), closedBall p.1 p.2) ≤ μ (s \ ⋃ p ∈ u n, closedBall p.1 p.2)
n : ℕ
IH : μ (s \ ⋃ p ∈ u n, closedBall p.1 p.2) ≤ (↑N / (↑N + 1)) ^ n * μ s
⊢ ↑N / (↑N + 1) * μ (s \ ⋃ p ∈ u n, closedBall p.1 p.2) ≤ (↑N / (↑N + 1)) ^ (n + 1) * μ s

Tactic:
grw [pow_succ', mul_assoc, IH]

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

Goal state before:
pp: case refine_2
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
⊢ AntitoneOn f (Ici b)

Tactic:
apply antitoneOn_of_deriv_nonpos (convex_Ici b) (continuousOn_Ici hb hd₁) <;> simp_all

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

Goal state before:
pp: case refine_2
f : ℝ → ℝ
a b : ℝ
ha : ContinuousAt f a
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
⊢ AntitoneOn f (Ici b)

Tactic:
apply antitoneOn_of_deriv_nonpos (convex_Ici b) (continuousOn_Ici hb hd₁) <;> simp_all

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

Goal state before:
pp: case refine_2
f : ℝ → ℝ
b : ℝ
hb : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Iio b)
hd₁ : DifferentiableOn ℝ f (Ioi b)
h₀ : ∀ x ∈ Iio b, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioi b, deriv f x ≤ 0
⊢ AntitoneOn f (Ici b)

Tactic:
apply antitoneOn_of_deriv_nonpos (convex_Ici b) (continuousOn_Ici hb hd₁) <;> simp_all

Goal state after:
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, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioi b, 0 ≤ deriv f x
⊢ IsMinOn f (Ioi a) b

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

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin

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
f : E →L[𝕜] F
⊢ alternatizeUncurryFin (↑↑(constOfIsEmptyLIE 𝕜 E F (Fin 0)) ∘SL f) = (ofSubsingleton 𝕜 E F 0) f

Tactic:
ext
  simp [alternatizeUncurryFin_apply]

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 : IsSymmSndFDerivWithinAt 𝕜 f t x
hst : t ∈ 𝓝[s] x
hf : ContDiffWithinAt 𝕜 2 f t x
hs : UniqueDiffOn 𝕜 s
ht : UniqueDiffOn 𝕜 t
hx : x ∈ s
v w : E
⊢ ((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) v) w = ((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) w) v

Tactic:
rw [fderivWithin_fderivWithin_eq_of_mem_nhdsWithin hst hf hs ht hx]

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 : IsSymmSndFDerivWithinAt 𝕜 f t x
hst : t ∈ 𝓝[s] x
hf : ContDiffWithinAt 𝕜 2 f t x
hs : UniqueDiffOn 𝕜 s
ht : UniqueDiffOn 𝕜 t
hx : x ∈ s
v w : E
⊢ ((fderivWithin 𝕜 (fderivWithin 𝕜 f t) t x) v) w = ((fderivWithin 𝕜 (fderivWithin 𝕜 f t) t x) w) v
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:
simp_rw [← Nfu] at hD

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
⊢ ‖iteratedFDerivWithin 𝕜 n (g ∘ f) s x‖ ≤ ↑n ! * C * D ^ n
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 V₁ W₁ : E → E
s t : Set E
x✝ : E
hV : V₁ =ᶠ[𝓝[s] x✝] V
hW : W₁ =ᶠ[𝓝[s] x✝] W
ht : t ⊆ s
x : E
hV' : fderivWithin 𝕜 V₁ t x = fderivWithin 𝕜 V t x
⊢ fderivWithin 𝕜 W₁ t x = fderivWithin 𝕜 W t x →
    V₁ x = V x → W₁ x = W x → lieBracketWithin 𝕜 V₁ W₁ t x = lieBracketWithin 𝕜 V W t x

Tactic:
hW'

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W V₁ W₁ : E → E
s t : Set E
x✝ : E
hV : V₁ =ᶠ[𝓝[s] x✝] V
hW : W₁ =ᶠ[𝓝[s] x✝] W
ht : t ⊆ s
x : E
hV' : fderivWithin 𝕜 V₁ t x = fderivWithin 𝕜 V t x
hW' : fderivWithin 𝕜 W₁ t x = fderivWithin 𝕜 W t x
⊢ V₁ x = V x → W₁ x = W x → lieBracketWithin 𝕜 V₁ W₁ t x = lieBracketWithin 𝕜 V W t x
Module: Mathlib.Analysis.Calculus.FDeriv.Norm

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : StrongDual ℝ E
x : E
t : ℝ
ht : t ≠ 0
h : HasStrictFDerivAt (fun x ↦ ‖x‖) f x
h1 : HasStrictFDerivAt (fun y ↦ t⁻¹ • y) (t⁻¹ • ContinuousLinearMap.id ℝ E) (t • x)
⊢ HasStrictFDerivAt (fun x ↦ ‖x‖) (↑(SignType.sign t) • f) (t • x)

Tactic:
have h2 : HasStrictFDerivAt (fun y ↦ |t| * ‖y‖) (|t| • f) x := h.const_smul |t|

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : StrongDual ℝ E
x : E
t : ℝ
ht : t ≠ 0
h : HasStrictFDerivAt (fun x ↦ ‖x‖) f x
h1 : HasStrictFDerivAt (fun y ↦ t⁻¹ • y) (t⁻¹ • ContinuousLinearMap.id ℝ E) (t • x)
h2 : HasStrictFDerivAt (fun y ↦ |t| * ‖y‖) (|t| • f) x
⊢ HasStrictFDerivAt (fun x ↦ ‖x‖) (↑(SignType.sign t) • f) (t • x)
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: α : Type u_1
inst✝⁵ : MetricSpace α
β : Type u
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : Measure α
inst✝ : SFinite μ
s : Set α
f : α → Set (Set α)
fsubset : ∀ x ∈ s, f x ⊆ (fun r ↦ closedBall x r) '' Ioi 0
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
g : α → Set ℝ := fun x ↦ {r | 0 < r ∧ closedBall x r ∈ f x}
x : α
xs : x ∈ s
δ : ℝ
δpos : δ > 0
t : Set α
tf : t ∈ f x
ht : t ⊆ closedBall x (δ / 2)
⊢ (g x ∩ Ioo 0 δ).Nonempty

Tactic:
obtain ⟨r, rpos, rfl⟩ : ∃ r : ℝ, 0 < r ∧ closedBall x r = t := by simpa using fsubset x xs tf

Goal state after:
α : Type u_1
inst✝⁵ : MetricSpace α
β : Type u
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : Measure α
inst✝ : SFinite μ
s : Set α
f : α → Set (Set α)
fsubset : ∀ x ∈ s, f x ⊆ (fun r ↦ closedBall x r) '' Ioi 0
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
g : α → Set ℝ := fun x ↦ {r | 0 < r ∧ closedBall x r ∈ f x}
x : α
xs : x ∈ s
δ : ℝ
δpos : δ > 0
r : ℝ
rpos : 0 < r
tf : closedBall x r ∈ f x
ht : closedBall x r ⊆ closedBall x (δ / 2)
⊢ (g x ∩ Ioo 0 δ).Nonempty
Module: Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E₁ : Type u_2
inst✝⁸ : NormedAddCommGroup E₁
inst✝⁷ : NormedSpace 𝕜 E₁
inst✝⁶ : CompleteSpace E₁
E₂ : Type u_3
inst✝⁵ : NormedAddCommGroup E₂
inst✝⁴ : NormedSpace 𝕜 E₂
inst✝³ : CompleteSpace E₂
F : Type u_4
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
u : E₁ × E₂
f : E₁ × E₂ → F
f'u : E₁ × E₂ →L[𝕜] F
dfu : HasStrictFDerivAt f f'u u
if₂u : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible
⊢ HasStrictFDerivAt (dfu.implicitFunctionOfProdDomain if₂u)
    (-(f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).inverse ∘SL f'u ∘SL ContinuousLinearMap.inl 𝕜 E₁ E₂) u.1

Tactic:
suffices f'u ∘L (.prod (.id ..) (-(f'u ∘L .inr ..).inverse ∘L (f'u ∘L .inl ..))) = 0 from
    ((dfu.implicitFunctionDataOfProdDomain if₂u).hasStrictFDerivAt_implicitFunction _
      (ContinuousLinearMap.fst_comp_prod _ _) this).snd
  ext
  rw [f'u.comp_apply, ← f'u.comp_inl_add_comp_inr]
  simp [-ContinuousLinearMap.comp_apply, ContinuousLinearMap.coe_comp, map_neg, if₂u]

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 𝕜 2 g (f x)
hf : ContDiffAt 𝕜 2 f x
⊢ iteratedDeriv 2 (g ∘ f) x =
    ((iteratedFDeriv 𝕜 2 g (f x)) fun x_1 ↦ deriv f x) + (fderiv 𝕜 g (f x)) (iteratedDeriv 2 f x)

Tactic:
by
  simp only [← iteratedDerivWithin_univ, ← iteratedFDerivWithin_univ,
    ← derivWithin_univ, ← fderivWithin_univ]
  exact iteratedDerivWithin_vcomp_two hg hf uniqueDiffOn_univ
    uniqueDiffOn_univ (mem_univ x) (mapsTo_univ f _)

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

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : SecondCountableTopology F
f : E → F
s : Set E
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
r : (E →L[ℝ] F) → ℝ≥0
rpos : ∀ (A : E →L[ℝ] F), r A ≠ 0
hs : s.Nonempty
T : Set ↑s
T_count : T.Countable
hT : ⋃ x ∈ T, ball (f' ↑x) ↑(r (f' ↑x)) = ⋃ x, ball (f' ↑x) ↑(r (f' ↑x))
u : ℕ → ℝ
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
M : ℕ → ↑T → Set E :=
  fun n z ↦ {x | x ∈ s ∧ ∀ y ∈ s ∩ ball x (u n), ‖f y - f x - (f' ↑↑z) (y - x)‖ ≤ ↑(r (f' ↑↑z)) * ‖y - x‖}
x : E
xs : x ∈ s
z : ↑s
zT : z ∈ T
hz : f' x ∈ ball (f' ↑z) ↑(r (f' ↑z))
⊢ ∃ ε, 0 < ε ∧ ‖f' x - f' ↑z‖ + ε ≤ ↑(r (f' ↑z))

Tactic:
refine ⟨r (f' z) - ‖f' x - f' z‖, ?_, le_of_eq (by abel)⟩
      simpa only [sub_pos] using! mem_ball_iff_norm.mp hz

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts

Goal state before:
pp: a b : ℝ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x ↦ f' x • (g ∘ f) x) [[a, b]] volume
hE : CompleteSpace E
h_cont : ContinuousOn (fun u ↦ ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (min a b) (max a b)
c : ℝ
hc : c ∈ Ioo (min a b) x
d : ℝ
hd : d ∈ Ioo x (max a b)
cdsub : [[c, d]] ⊆ Ioo (min a b) (max a b)
hg_cont : ContinuousOn g (f '' [[c, d]])
J : Set ℝ := [[sInf (f '' [[c, d]]), sSup (f '' [[c, d]])]]
hJ : f '' [[c, d]] = J
⊢ HasDerivWithinAt (fun u ↦ ∫ (t : ℝ) in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x

Tactic:
rw [hJ] at hg_cont

Goal state after:
a b : ℝ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x ↦ f' x • (g ∘ f) x) [[a, b]] volume
hE : CompleteSpace E
h_cont : ContinuousOn (fun u ↦ ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (min a b) (max a b)
c : ℝ
hc : c ∈ Ioo (min a b) x
d : ℝ
hd : d ∈ Ioo x (max a b)
cdsub : [[c, d]] ⊆ Ioo (min a b) (max a b)
J : Set ℝ := [[sInf (f '' [[c, d]]), sSup (f '' [[c, d]])]]
hg_cont : ContinuousOn g J
hJ : f '' [[c, d]] = J
⊢ HasDerivWithinAt (fun u ↦ ∫ (t : ℝ) in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts

Goal state before:
pp: case inl
a b : ℝ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo (min a b) (max a b), 0 ≤ f' x
M : MonotoneOn f [[a, b]]
hab : a ≤ b
⊢ ∫ (x : ℝ) in a..b, f' x • g (f x) = ∫ (u : ℝ) in f a..f b, g u

Tactic:
rw [integral_of_le hab, ← integral_Icc_eq_integral_Ioc,
      integral_Icc_deriv_smul_of_deriv_nonneg, integral_of_le, ← integral_Icc_eq_integral_Ioc]
    · apply M left_mem_uIcc right_mem_uIcc hab
    · rwa [uIcc_of_le hab] at hf
    · grind
    · grind
    · exact hab

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

Goal state before:
pp: case inr
E : Type u_1
F✝ : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : NormedAddCommGroup F✝
inst✝¹ : NormedSpace ℝ F✝
inst✝ : SecondCountableTopology F✝
f : E → F✝
s : Set E
f' : E → E →L[ℝ] F✝
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
r : (E →L[ℝ] F✝) → ℝ≥0
rpos : ∀ (A : E →L[ℝ] F✝), r A ≠ 0
hs : s.Nonempty
T : Set ↑s
T_count : T.Countable
hT : ⋃ x ∈ T, ball (f' ↑x) ↑(r (f' ↑x)) = ⋃ x, ball (f' ↑x) ↑(r (f' ↑x))
u : ℕ → ℝ
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
M : ℕ → ↑T → Set E :=
  fun n z ↦ {x | x ∈ s ∧ ∀ y ∈ s ∩ ball x (u n), ‖f y - f x - (f' ↑↑z) (y - x)‖ ≤ ↑(r (f' ↑↑z)) * ‖y - x‖}
s_subset : ∀ x ∈ s, ∃ n z, x ∈ M n z
closure_M_subset : ∀ (n : ℕ) (z : ↑T), s ∩ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (M n z) ⊆ M n z
d : ℕ → E
hd : DenseRange d
K : ℕ → ↑T → ℕ → Set E :=
  fun n z p ↦ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (M n z) ∩ closedBall (d p) (u n / 3)
K_approx : ∀ (n : ℕ) (z : ↑T) (p : ℕ), ApproximatesLinearOn f (f' ↑↑z) (s ∩ K n z p) (r (f' ↑↑z))
K_closed : ∀ (n : ℕ) (z : ↑T) (p : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (K n z p)
F : ℕ → ℕ × ↑T × ℕ
hF : Function.Surjective F
⊢ ∃ t A,
    (∀ (n : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (t n)) ∧
      s ⊆ ⋃ n, t n ∧
        (∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (r (A n))) ∧ (s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y)

Tactic:
refine
    ⟨fun q => K (F q).1 (F q).2.1 (F q).2.2, fun q => f' (F q).2.1, fun n => K_closed _ _ _,
      fun x xs => ?_, fun q => K_approx _ _ _, fun _ q => ⟨(F q).2.1, (F q).2.1.1.2, rfl⟩⟩

Goal state after:
case inr
E : Type u_1
F✝ : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : NormedAddCommGroup F✝
inst✝¹ : NormedSpace ℝ F✝
inst✝ : SecondCountableTopology F✝
f : E → F✝
s : Set E
f' : E → E →L[ℝ] F✝
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
r : (E →L[ℝ] F✝) → ℝ≥0
rpos : ∀ (A : E →L[ℝ] F✝), r A ≠ 0
hs : s.Nonempty
T : Set ↑s
T_count : T.Countable
hT : ⋃ x ∈ T, ball (f' ↑x) ↑(r (f' ↑x)) = ⋃ x, ball (f' ↑x) ↑(r (f' ↑x))
u : ℕ → ℝ
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
M : ℕ → ↑T → Set E :=
  fun n z ↦ {x | x ∈ s ∧ ∀ y ∈ s ∩ ball x (u n), ‖f y - f x - (f' ↑↑z) (y - x)‖ ≤ ↑(r (f' ↑↑z)) * ‖y - x‖}
s_subset : ∀ x ∈ s, ∃ n z, x ∈ M n z
closure_M_subset : ∀ (n : ℕ) (z : ↑T), s ∩ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (M n z) ⊆ M n z
d : ℕ → E
hd : DenseRange d
K : ℕ → ↑T → ℕ → Set E :=
  fun n z p ↦ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (M n z) ∩ closedBall (d p) (u n / 3)
K_approx : ∀ (n : ℕ) (z : ↑T) (p : ℕ), ApproximatesLinearOn f (f' ↑↑z) (s ∩ K n z p) (r (f' ↑↑z))
K_closed : ∀ (n : ℕ) (z : ↑T) (p : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (K n z p)
F : ℕ → ℕ × ↑T × ℕ
hF : Function.Surjective F
x : E
xs : x ∈ s
⊢ x ∈ ⋃ n, (fun q ↦ K (F q).1 (F q).2.1 (F q).2.2) n
Module: Mathlib.MeasureTheory.Function.Jacobian

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : ENNReal.ofReal |A.det| < ↑m
d : ℝ≥0∞ := ENNReal.ofReal |A.det|
ε : ℝ
hε : μ (closedBall 0 ε + ⇑A '' closedBall 0 1) < ↑m * μ (closedBall 0 1)
εpos : 0 < ε
this : Iio (NNReal.mk ε ⋯) ∈ 𝓝 0
δ : ℝ≥0
hδ : δ ∈ Iio (NNReal.mk ε ⋯)
⊢ ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → μ (f '' s) ≤ ↑m * μ s

Tactic:
s

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : ENNReal.ofReal |A.det| < ↑m
d : ℝ≥0∞ := ENNReal.ofReal |A.det|
ε : ℝ
hε : μ (closedBall 0 ε + ⇑A '' closedBall 0 1) < ↑m * μ (closedBall 0 1)
εpos : 0 < ε
this : Iio (NNReal.mk ε ⋯) ∈ 𝓝 0
δ : ℝ≥0
hδ : δ ∈ Iio (NNReal.mk ε ⋯)
s : Set E
⊢ ∀ (f : E → E), ApproximatesLinearOn f A s δ → μ (f '' s) ≤ ↑m * μ s
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝¹ : PseudoMetricSpace α
inst✝ : OpensMeasurableSpace α
x : α
r : ι → ℝ
hr : Tendsto r l atTop
y : α
⊢ ∀ᶠ (i : ι) in l, y ∈ Metric.closedBall x (r i)

Tactic:
filter_upwards [hr (Ici_mem_atTop (dist x y))] with a ha using by simpa [dist_comm] using ha

Goal state after: