mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝² : (i : α) → NormedAddCommGroup (E i)
inst✝¹ : DecidableEq α
inst✝ : Fact (1 ≤ p)
hp : p ≠ ∞
f : ↥(lp E p)
hp₀ : 0 < p
hp' : 0 < p.toReal
this :
  ∀ ε > 0,
    ∀ᶠ (x : Finset α) in (SummationFilter.unconditional α).filter,
      dist (∑ b ∈ x, ‖↑f b‖ ^ p.toReal) (‖f‖ ^ p.toReal) < ε
ε : ℝ
hε : ε > 0
s : Finset α
hs : dist (‖f‖ ^ p.toReal) (∑ b ∈ s, ‖↑f b‖ ^ p.toReal) < ε ^ p.toReal
⊢ dist (∑ b ∈ s, lp.single p b (↑f b)) f ^ p.toReal < ε ^ p.toReal

Tactic:
simp only [dist_eq_norm, Real.norm_eq_abs] at hs ⊢

Goal state after:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝² : (i : α) → NormedAddCommGroup (E i)
inst✝¹ : DecidableEq α
inst✝ : Fact (1 ≤ p)
hp : p ≠ ∞
f : ↥(lp E p)
hp₀ : 0 < p
hp' : 0 < p.toReal
this :
  ∀ ε > 0,
    ∀ᶠ (x : Finset α) in (SummationFilter.unconditional α).filter,
      dist (∑ b ∈ x, ‖↑f b‖ ^ p.toReal) (‖f‖ ^ p.toReal) < ε
ε : ℝ
hε : ε > 0
s : Finset α
hs : |‖f‖ ^ p.toReal - ∑ b ∈ s, ‖↑f b‖ ^ p.toReal| < ε ^ p.toReal
⊢ ‖∑ b ∈ s, lp.single p b (↑f b) - f‖ ^ p.toReal < ε ^ p.toReal
Module: Mathlib.Analysis.Calculus.ParametricIntegral

Goal state before:
pp: case pos
α : Type u_1
inst✝⁶ : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst✝⁵ : RCLike 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace 𝕜 E
H : Type u_4
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
F : H → α → E
x₀ : H
bound : α → ℝ
s : Set H
F' : α → H →L[𝕜] E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ x ∈ s, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt (fun x ↦ F x a) (F' a) x₀
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
nneg : ∀ (x : H), 0 ≤ ‖x - x₀‖⁻¹
b : α → ℝ := fun a ↦ |bound a|
b_int : Integrable b μ
b_nonneg : ∀ (a : α), 0 ≤ b a
h_lipsch : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
hF_int' : ∀ x ∈ ball x₀ ε, Integrable (F x) μ
hF'_int : Integrable F' μ
hE : CompleteSpace E
h_ball : ball x₀ ε ∈ 𝓝 x₀
⊢ HasFDerivAt (fun x ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀

Tactic:
have : ∀ᶠ x in 𝓝 x₀, ‖x - x₀‖⁻¹ * ‖((∫ a, F x a ∂μ) - ∫ a, F x₀ a ∂μ) - (∫ a, F' a ∂μ) (x - x₀)‖ =
      ‖∫ a, ‖x - x₀‖⁻¹ • (F x a - F x₀ a - F' a (x - x₀)) ∂μ‖ := by
    apply mem_of_superset (ball_mem_nhds _ ε_pos)
    intro x x_in; simp only
    rw [Set.mem_ofPred_eq, ← norm_smul_of_nonneg (nneg _), integral_smul, integral_sub,
      integral_sub, ← ContinuousLinearMap.integral_apply hF'_int]
    exacts [hF_int' x x_in, hF_int, (hF_int' x x_in).sub hF_int,
      hF'_int.apply_continuousLinearMap _]

Goal state after:
case pos
α : Type u_1
inst✝⁶ : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst✝⁵ : RCLike 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace 𝕜 E
H : Type u_4
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
F : H → α → E
x₀ : H
bound : α → ℝ
s : Set H
F' : α → H →L[𝕜] E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ x ∈ s, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt (fun x ↦ F x a) (F' a) x₀
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
nneg : ∀ (x : H), 0 ≤ ‖x - x₀‖⁻¹
b : α → ℝ := fun a ↦ |bound a|
b_int : Integrable b μ
b_nonneg : ∀ (a : α), 0 ≤ b a
h_lipsch : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
hF_int' : ∀ x ∈ ball x₀ ε, Integrable (F x) μ
hF'_int : Integrable F' μ
hE : CompleteSpace E
h_ball : ball x₀ ε ∈ 𝓝 x₀
this :
  ∀ᶠ (x : H) in 𝓝 x₀,
    ‖x - x₀‖⁻¹ * ‖∫ (a : α), F x a ∂μ - ∫ (a : α), F x₀ a ∂μ - (∫ (a : α), F' a ∂μ) (x - x₀)‖ =
      ‖∫ (a : α), ‖x - x₀‖⁻¹ • (F x a - F x₀ a - (F' a) (x - x₀)) ∂μ‖
⊢ HasFDerivAt (fun x ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: G : Type uG
x : G
inst✝¹ : MeasurableSpace G
μ : Measure G
inst✝ : AddGroup G
f g g' : G → ℝ
hfg : ConvolutionExistsAt f g x (lsmul ℝ ℝ) μ
hfg' : ConvolutionExistsAt f g' x (lsmul ℝ ℝ) μ
hf : ∀ (x : G), 0 ≤ f x
hg : ∀ (x : G), g x ≤ g' x
⊢ (f ⋆[lsmul ℝ ℝ, μ] g) x ≤ (f ⋆[lsmul ℝ ℝ, μ] g') x

Tactic:
by
  apply integral_mono hfg hfg'
  simp only [lsmul_apply, smul_eq_mul]
  intro t
  dsimp
  gcongr
  exacts [hf _, hg _]

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

Goal state before:
pp: α : Type u_1
inst✝⁶ : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst✝⁵ : RCLike 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace 𝕜 E
H : Type u_4
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
F : H → α → E
x₀ : H
bound : α → ℝ
s : Set H
F' : α → H →L[𝕜] E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ x ∈ s, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt (fun x ↦ F x a) (F' a) x₀
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
nneg : ∀ (x : H), 0 ≤ ‖x - x₀‖⁻¹
b : α → ℝ := fun a ↦ |bound a|
b_int : Integrable b μ
b_nonneg : ∀ (a : α), 0 ≤ b a
h_lipsch : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
hF_int' : ∀ x ∈ ball x₀ ε, Integrable (F x) μ
hF'_int : Integrable F' μ
hE : CompleteSpace E
h_ball : ball x₀ ε ∈ 𝓝 x₀
this✝ :
  ∀ᶠ (x : H) in 𝓝 x₀,
    ‖x - x₀‖⁻¹ * ‖∫ (a : α), F x a ∂μ - ∫ (a : α), F x₀ a ∂μ - (∫ (a : α), F' a ∂μ) (x - x₀)‖ =
      ‖∫ (a : α), ‖x - x₀‖⁻¹ • (F x a - F x₀ a - (F' a) (x - x₀)) ∂μ‖
a : α
ha : HasFDerivAt (fun x ↦ F x a) (F' a) x₀
this : Tendsto (fun x ↦ ‖x - x₀‖⁻¹ • (F x a - F x₀ a - (F' a) (x - x₀))) (𝓝 x₀) (𝓝 0)
⊢ Tendsto (fun n ↦ ‖n - x₀‖⁻¹ • (F n a - F x₀ a - (F' a) (n - x₀))) (𝓝 x₀)
    (𝓝 (‖x₀ - x₀‖⁻¹ • (F x₀ a - F x₀ a - (F' a) (x₀ - x₀))))

Tactic:
by simpa

Goal state after:
Module: Mathlib.Topology.MetricSpace.ProperSpace.Lemmas

Goal state before:
pp: α : Type u_1
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
r : ℝ
s : Set α
hs : IsClosed s
h : s ⊆ ball x r
⊢ ∃ r' < r, s ⊆ ball x r'

Tactic:
by
  rcases le_or_gt r 0 with hr | hr
  · rw [ball_eq_empty.2 hr, subset_empty_iff] at h
    subst s
    exact (exists_lt r).imp fun r' hr' => ⟨hr', empty_subset _⟩
  · exact (exists_pos_lt_subset_ball hr hs h).imp fun r' hr' => ⟨hr'.1.2, hr'.2⟩

Goal state after:
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: case neg
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁶ : MeasurableSpace G
μ : Measure G
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
inst✝¹ : μ.IsAddLeftInvariant
inst✝ : SFinite μ
x₀ : G
R ε : ℝ
z₀ : E'
hε : 0 ≤ ε
hif : Integrable f μ
hf : support f ⊆ ball 0 R
hmg : AEStronglyMeasurable g μ
hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε
hfg : ConvolutionExistsAt f g x₀ L μ
t : G
ht : t ∉ support f
⊢ dist ((L (f t)) (g (x₀ - t))) ((L (f t)) z₀) ≤ ‖L (f t)‖ * ε

Tactic:
rw [notMem_support] at ht
      simp_rw [ht, L.map_zero₂, L.map_zero, norm_zero, zero_mul, dist_self]
      rfl

Goal state after:
Module: Mathlib.MeasureTheory.Measure.EverywherePos

Goal state before:
pp: G : Type u_2
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : LocallyCompactSpace G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : μ.IsMulLeftInvariant
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : μ.InnerRegularCompactLTTop
k : Set G
h : μ.IsEverywherePos k
hk : IsCompact k
h'k : IsClosed[inst✝⁷] k
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 1
u_lim : Tendsto u atTop (𝓝 0)
W : ℕ → Set G
W_open : ∀ (n : ℕ), IsOpen[inst✝⁷] (W n)
mem_W : ∀ (n : ℕ), 1 ∈ W n
hW : ∀ (n : ℕ), ∀ g ∈ W n * W n, μ (g • k \ k) < u n
V : ℕ → Set G := fun n ↦ ⋂ i ∈ Finset.range n, W i
x : G
hx : x ∈ ⋂ n, V n * k
v : ℕ → G
hv : ∀ (i : ℕ), v i ∈ V i
y : ℕ → G
hy : ∀ (i : ℕ), y i ∈ k
hvy : ∀ (i : ℕ), (fun x1 x2 ↦ x1 * x2) (v i) (y i) = x
z : G
zk : z ∈ k
hz : MapClusterPt z atTop y
n : ℕ
this : W n * {z} ∈ 𝓝 z
i : ℕ
hi : y i ∈ W n * {z}
ni : n < i
I : V i ⊆ W n
J : x * (y i)⁻¹ ∈ V i
⊢ x * (y i)⁻¹ ∈ W n

Tactic:
exact I J

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

Goal state before:
pp: case refine_3
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), f x ∈ Icc 0 1
⊢ (support fun x ↦ (f x + f (-x)) / 2) = ball 0 1

Tactic:
refine support_eq_iff.2 ⟨fun x hx => ?_, fun x hx => ?_⟩

Goal state after:
case refine_3.refine_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), f x ∈ Icc 0 1
x : E
hx : x ∈ ball 0 1
⊢ (f x + f (-x)) / 2 ≠ 0

case refine_3.refine_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), f x ∈ Icc 0 1
x : E
hx : x ∉ ball 0 1
⊢ (f x + f (-x)) / 2 = 0
Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
hx : x ∈ closedBall 0 (1 - D)
C : ball x D ⊆ ball 0 1
y : E
hy : y ∈ ball x D
h'y : 1 < dist y 0
⊢ False

Tactic:
linarith only [mem_ball.1 (C hy), h'y]

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

Goal state before:
pp: case left
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
D_lt_one : D < 1
hx : ‖x‖ < 1 + D
z : E := ⋯
hz : z = (D / (1 + D)) • x
B : 0 < 1 + D
y : E
hy : y ∈ ball z (D * (1 + D - ‖x‖) / (1 + D))
⊢ y ∈ ball 0 D

pp: case right
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
D_lt_one : D < 1
hx : ‖x‖ < 1 + D
z : E := ⋯
hz : z = (D / (1 + D)) • x
B : 0 < 1 + D
y : E
hy : y ∈ ball z (D * (1 + D - ‖x‖) / (1 + D))
⊢ ‖x - y‖ ≤ 1

Tactic:
· apply ball_subset_ball' _ hy
        simp only [hz, norm_smul, abs_of_nonneg Dpos.le, abs_of_nonneg B.le, dist_zero_right,
          Real.norm_eq_abs, abs_div]
        field_simp
        linarith only

Goal state after:
case right
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
D_lt_one : D < 1
hx : ‖x‖ < 1 + D
z : E := ⋯
hz : z = (D / (1 + D)) • x
B : 0 < 1 + D
y : E
hy : y ∈ ball z (D * (1 + D - ‖x‖) / (1 + D))
⊢ ‖x - y‖ ≤ 1
Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ c ∈ s, ‖c‖ ≤ 2
h : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
μ : Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ c ∈ s, ball c δ
hA : A = ⋃ c ∈ s, ball c δ
D : (↑s).Pairwise (Disjoint on fun c ↦ ball c δ)
A_subset : A ⊆ ball 0 ρ
⊢ ↑s.card * ENNReal.ofReal (δ ^ finrank ℝ E) * μ (ball 0 1) = μ A

Tactic:
rw [hA, measure_biUnion_finset D fun c _ => measurableSet_ball]

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ c ∈ s, ‖c‖ ≤ 2
h : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
μ : Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ c ∈ s, ball c δ
hA : A = ⋃ c ∈ s, ball c δ
D : (↑s).Pairwise (Disjoint on fun c ↦ ball c δ)
A_subset : A ⊆ ball 0 ρ
⊢ ↑s.card * ENNReal.ofReal (δ ^ finrank ℝ E) * μ (ball 0 1) = ∑ p ∈ s, μ (ball p δ)
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:
by simpa

Goal state after:
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 - δ ≤ ‖(if ‖a.c i‖ ≤ 2 then a.c i else (2 / ‖a.c i‖) • a.c i) - if True then a.c j else (2 / ‖a.c j‖) • a.c j‖

Tactic:
hij.trans Hj,

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 - δ ≤ ‖(if True then a.c i else (2 / ‖a.c i‖) • a.c i) - if True then a.c j else (2 / ‖a.c j‖) • a.c j‖
Module: Mathlib.Topology.MetricSpace.Holder

Goal state before:
pp: case inl
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
C D : ℝ≥0
A : Set X
hA : ∀ x ∈ A, ∀ y ∈ A, edist x y ≤ ↑D
hf : HolderOnWith C r f A
hsr : 0 ≤ r
⊢ HolderOnWith (C * D ^ (↑r - ↑0)) 0 f A

Tactic:
simpa using hf.holderOnWith_zero_of_bounded hA

Goal state after:
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:
by simpa

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

Goal state before:
pp: f : ℝ → ℝ
x₀ : ℝ
hf : deriv f x₀ > 0
hx : f x₀ = 0
h_tendsto : Tendsto (slope f x₀) (𝓝[≠] x₀) (𝓝 (deriv f x₀))
x : ℝ
hx₀ : 0 < slope f x₀ x
hx₁ : ¬x = x₀
⊢ sign (f x) = sign (x - x₀)

Tactic:
← Ne.eq_def

Goal state after:
f : ℝ → ℝ
x₀ : ℝ
hf : deriv f x₀ > 0
hx : f x₀ = 0
h_tendsto : Tendsto (slope f x₀) (𝓝[≠] x₀) (𝓝 (deriv f x₀))
x : ℝ
hx₀ : 0 < slope f x₀ x
hx₁ : x ≠ x₀
⊢ sign (f x) = sign (x - x₀)
Module: Mathlib.Analysis.Calculus.DerivativeTest

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

Tactic:
by 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:
by 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:
by simpa

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

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : E → F [⋀^ι]→L[𝕜] G
g : ι → E → F
x : E
inst✝ : Finite ι
hf : DifferentiableAt 𝕜 f x
hg : ∀ (i : ι), DifferentiableAt 𝕜 (g i) x
⊢ DifferentiableAt 𝕜 (fun x ↦ (f x) fun x_1 ↦ g x_1 x) x

Tactic:
by
  cases nonempty_fintype ι
  classical
  exact hf.hasFDerivAt.continuousAlternatingMap_apply (fun i ↦ (hg i).hasFDerivAt)
    |>.differentiableAt

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
v : E
f : E → F
x₀ : E
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
⊢ ‖lineDeriv 𝕜 f x₀ v‖ ≤ C * ‖v‖

Tactic:
apply norm_deriv_le_of_lip' (by positivity)
  have A : Continuous (fun (t : 𝕜) ↦ x₀ + t • v) := by fun_prop
  have : ∀ᶠ x in 𝓝 (x₀ + (0 : 𝕜) • v), ‖f x - f x₀‖ ≤ C * ‖x - x₀‖ := by simpa using hlip
  filter_upwards [(A.continuousAt (x := 0)).preimage_mem_nhds this] with t ht
  simp only [preimage_ofPred_eq, add_sub_cancel_left, norm_smul, mem_ofPred_eq,
    mul_comm (‖t‖)] at ht
  simpa [mul_assoc] using ht

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
⊢ DifferentiableAt ℝ Norm.norm (0 • x)

Tactic:
by simpa

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁹ : RCLike 𝕜
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
n : ℕ∞ω
cdf : ContDiffAt 𝕜 n f u
pn : n ≠ 0
if₂ : (fderiv 𝕜 f u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible
φ : ImplicitFunctionData 𝕜 (E₁ × E₂) F E₁ := ⋯.implicitFunctionDataOfProdDomain if₂
⊢ ContDiffAt 𝕜 n φ.rightFun φ.pt

Tactic:
simpa [φ] using contDiffAt_fst

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
s : Set 𝕜
t : Set E
x : 𝕜
n : ℕ∞ω
i : ℕ
hg : ContDiffWithinAt 𝕜 n g t (f x)
hf : ContDiffWithinAt 𝕜 n f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
hi : ↑i ≤ n
⊢ iteratedDerivWithin i (g ∘ f) s x =
    ∑ c, (iteratedFDerivWithin 𝕜 c.length g t (f x)) fun j ↦ iteratedDerivWithin (c.partSize j) f s x

Tactic:
simp only [iteratedDerivWithin, iteratedFDerivWithin_comp hg hf ht hs hx hst hi]

Goal state after:
𝕜 : 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
s : Set 𝕜
t : Set E
x : 𝕜
n : ℕ∞ω
i : ℕ
hg : ContDiffWithinAt 𝕜 n g t (f x)
hf : ContDiffWithinAt 𝕜 n f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
hi : ↑i ≤ n
⊢ (((ftaylorSeriesWithin 𝕜 g t (f x)).taylorComp (ftaylorSeriesWithin 𝕜 f s x) i) fun x ↦ 1) =
    ∑ c, (iteratedFDerivWithin 𝕜 c.length g t (f x)) fun j ↦ (iteratedFDerivWithin 𝕜 (c.partSize j) f s x) fun x ↦ 1
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
⊢ ∃ 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:
let K : ℕ → T → ℕ → Set E := fun n z p => closure (M n z) ∩ closedBall (d p) (u n / 3)

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)
⊢ ∃ 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)
Module: Mathlib.Analysis.Calculus.LHopital

Goal state before:
pp: a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in 𝓝[<] a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝[<] a, deriv g x ≠ 0
hfa : Tendsto f (𝓝[<] a) (𝓝 0)
hga : Tendsto g (𝓝[<] a) (𝓝 0)
hdiv : Tendsto (fun x ↦ deriv f x / deriv g x) (𝓝[<] a) l
⊢ Tendsto (fun x ↦ f x / g x) (𝓝[<] a) l

Tactic:
← Iic_sdiff_right

Goal state after:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in 𝓝[Iic a \ {a}] a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝[Iic a \ {a}] a, deriv g x ≠ 0
hfa : Tendsto f (𝓝[Iic a \ {a}] a) (𝓝 0)
hga : Tendsto g (𝓝[Iic a \ {a}] a) (𝓝 0)
hdiv : Tendsto (fun x ↦ deriv f x / deriv g x) (𝓝[Iic a \ {a}] a) l
⊢ Tendsto (fun x ↦ f x / g x) (𝓝[Iic a \ {a}] a) l