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

Goal state before:
pp: α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
N : ℕ
hN : IsEmpty (SatelliteConfig α N p.τ)
i : Ordinal.{u}
IH : ∀ y < i, y < p.lastStep → p.color y < N
hi : i < p.lastStep
A : Set ℕ :=
  ⋃ j,
    ⋃ (_ :
      (closedBall (p.c (p.index ↑j)) (p.r (p.index ↑j)) ∩ closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty),
      {p.color ↑j}
color_i : p.color i = sInf (univ \ A)
N_mem : N ∈ univ \ A
Inf_eq_N : sInf (univ \ A) = N
g : ℕ → Ordinal.{u}
hg :
  ∀ k < N,
    g k < i ∧
      (closedBall (p.c (p.index (g k))) (p.r (p.index (g k))) ∩
            closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty ∧
        k = p.color (g k)
G : ℕ → Ordinal.{u} := fun n ↦ if n = N then i else g n
n : ℕ
⊢ n ≤ N → p.color (G n) = n

Tactic:
hn

Goal state after:
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
N : ℕ
hN : IsEmpty (SatelliteConfig α N p.τ)
i : Ordinal.{u}
IH : ∀ y < i, y < p.lastStep → p.color y < N
hi : i < p.lastStep
A : Set ℕ :=
  ⋃ j,
    ⋃ (_ :
      (closedBall (p.c (p.index ↑j)) (p.r (p.index ↑j)) ∩ closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty),
      {p.color ↑j}
color_i : p.color i = sInf (univ \ A)
N_mem : N ∈ univ \ A
Inf_eq_N : sInf (univ \ A) = N
g : ℕ → Ordinal.{u}
hg :
  ∀ k < N,
    g k < i ∧
      (closedBall (p.c (p.index (g k))) (p.r (p.index (g k))) ∩
            closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty ∧
        k = p.color (g k)
G : ℕ → Ordinal.{u} := fun n ↦ if n = N then i else g n
n : ℕ
hn : n ≤ N
⊢ p.color (G n) = n
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
N : ℕ
hN : IsEmpty (SatelliteConfig α N p.τ)
i : Ordinal.{u}
IH : ∀ y < i, y < p.lastStep → p.color y < N
hi : i < p.lastStep
A : Set ℕ :=
  ⋃ j,
    ⋃ (_ :
      (closedBall (p.c (p.index ↑j)) (p.r (p.index ↑j)) ∩ closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty),
      {p.color ↑j}
color_i : p.color i = sInf (univ \ A)
N_mem : N ∈ univ \ A
Inf_eq_N : sInf (univ \ A) = N
g : ℕ → Ordinal.{u}
hg :
  ∀ k < N,
    g k < i ∧
      (closedBall (p.c (p.index (g k))) (p.r (p.index (g k))) ∩
            closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty ∧
        k = p.color (g k)
G : ℕ → Ordinal.{u} := fun n ↦ if n = N then i else g n
color_G : ∀ n ≤ N, p.color (G n) = n
n : ℕ
⊢ n ≤ N → G n < p.lastStep

Tactic:
hn

Goal state after:
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
N : ℕ
hN : IsEmpty (SatelliteConfig α N p.τ)
i : Ordinal.{u}
IH : ∀ y < i, y < p.lastStep → p.color y < N
hi : i < p.lastStep
A : Set ℕ :=
  ⋃ j,
    ⋃ (_ :
      (closedBall (p.c (p.index ↑j)) (p.r (p.index ↑j)) ∩ closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty),
      {p.color ↑j}
color_i : p.color i = sInf (univ \ A)
N_mem : N ∈ univ \ A
Inf_eq_N : sInf (univ \ A) = N
g : ℕ → Ordinal.{u}
hg :
  ∀ k < N,
    g k < i ∧
      (closedBall (p.c (p.index (g k))) (p.r (p.index (g k))) ∩
            closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty ∧
        k = p.color (g k)
G : ℕ → Ordinal.{u} := fun n ↦ if n = N then i else g n
color_G : ∀ n ≤ N, p.color (G n) = n
n : ℕ
hn : n ≤ N
⊢ G n < p.lastStep
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
N : ℕ
hN : IsEmpty (SatelliteConfig α N p.τ)
i : Ordinal.{u}
IH : ∀ y < i, y < p.lastStep → p.color y < N
hi : i < p.lastStep
A : Set ℕ :=
  ⋃ j,
    ⋃ (_ :
      (closedBall (p.c (p.index ↑j)) (p.r (p.index ↑j)) ∩ closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty),
      {p.color ↑j}
color_i : p.color i = sInf (univ \ A)
N_mem : N ∈ univ \ A
Inf_eq_N : sInf (univ \ A) = N
g : ℕ → Ordinal.{u}
hg :
  ∀ k < N,
    g k < i ∧
      (closedBall (p.c (p.index (g k))) (p.r (p.index (g k))) ∩
            closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty ∧
        k = p.color (g k)
G : ℕ → Ordinal.{u} := fun n ↦ if n = N then i else g n
color_G : ∀ n ≤ N, p.color (G n) = n
G_lt_last : ∀ n ≤ N, G n < p.lastStep
n : ℕ
⊢ n ≤ N → p.c (p.index (G n)) ∉ p.iUnionUpTo (G n) ∧ p.R (G n) ≤ p.τ * p.r (p.index (G n))

Tactic:
hn

Goal state after:
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
N : ℕ
hN : IsEmpty (SatelliteConfig α N p.τ)
i : Ordinal.{u}
IH : ∀ y < i, y < p.lastStep → p.color y < N
hi : i < p.lastStep
A : Set ℕ :=
  ⋃ j,
    ⋃ (_ :
      (closedBall (p.c (p.index ↑j)) (p.r (p.index ↑j)) ∩ closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty),
      {p.color ↑j}
color_i : p.color i = sInf (univ \ A)
N_mem : N ∈ univ \ A
Inf_eq_N : sInf (univ \ A) = N
g : ℕ → Ordinal.{u}
hg :
  ∀ k < N,
    g k < i ∧
      (closedBall (p.c (p.index (g k))) (p.r (p.index (g k))) ∩
            closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty ∧
        k = p.color (g k)
G : ℕ → Ordinal.{u} := fun n ↦ if n = N then i else g n
color_G : ∀ n ≤ N, p.color (G n) = n
G_lt_last : ∀ n ≤ N, G n < p.lastStep
n : ℕ
hn : n ≤ N
⊢ p.c (p.index (G n)) ∉ p.iUnionUpTo (G n) ∧ p.R (G n) ≤ p.τ * p.r (p.index (G n))
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 ∉ ball 0 (1 + D)
⊢ y D x = 0

Tactic:
change (w D ⋆[lsmul ℝ ℝ, μ] φ) x = 0

Goal state after:
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 ∉ ball 0 (1 + D)
⊢ (w D ⋆[lsmul ℝ ℝ, μ] φ) x = 0
Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

Goal state before:
pp: case refine_3.hf
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
hs : IsOpen (Ioo 0 1)
hk : IsCompact (closedBall 0 1)
⊢ ContDiffOn ℝ ∞ (fun x ↦ |x.1| ^ finrank ℝ E) (Ioo 0 1 ×ˢ univ)

Tactic:
apply ContDiffOn.pow

Goal state after:
case refine_3.hf
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
hs : IsOpen (Ioo 0 1)
hk : IsCompact (closedBall 0 1)
⊢ ContDiffOn ℝ ∞ (fun y ↦ |y.1|) (Ioo 0 1 ×ˢ univ)
Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

Goal state before:
pp: case hg
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
hs : IsOpen (Ioo 0 1)
hk : IsCompact (closedBall 0 1)
⊢ ContDiffOn ℝ ∞ (fun x ↦ u (x.1⁻¹ • x.2)) (Ioo 0 1 ×ˢ univ)

Tactic:
· apply (u_smooth E).comp_contDiffOn
      exact ContDiffOn.smul (contDiffOn_fst.inv fun x hx => ne_of_gt hx.1.1) contDiffOn_snd

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

Goal state before:
pp: G : Type uG
E' : Type uE'
inst✝⁸ : NormedAddCommGroup E'
g : G → E'
inst✝⁷ : MeasurableSpace G
μ : Measure G
inst✝⁶ : NormedSpace ℝ E'
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace ℝ G
inst✝³ : CompleteSpace E'
φ : ContDiffBump 0
inst✝² : BorelSpace G
inst✝¹ : FiniteDimensional ℝ G
inst✝ : μ.IsAddHaarMeasure
x₀ : G
ε : ℝ
hmg : AEStronglyMeasurable g μ
hg : ∀ x ∈ ball x₀ φ.rOut, dist (g x) (g x₀) ≤ ε
⊢ 0 ≤ ε

Tactic:
← dist_self (g x₀),

Goal state after:
G : Type uG
E' : Type uE'
inst✝⁸ : NormedAddCommGroup E'
g : G → E'
inst✝⁷ : MeasurableSpace G
μ : Measure G
inst✝⁶ : NormedSpace ℝ E'
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace ℝ G
inst✝³ : CompleteSpace E'
φ : ContDiffBump 0
inst✝² : BorelSpace G
inst✝¹ : FiniteDimensional ℝ G
inst✝ : μ.IsAddHaarMeasure
x₀ : G
ε : ℝ
hmg : AEStronglyMeasurable g μ
hg : ∀ x ∈ ball x₀ φ.rOut, dist (g x) (g x₀) ≤ ε
⊢ dist (g x₀) (g x₀) ≤ ε
Module: Mathlib.Analysis.Normed.Operator.Conformal

Goal state before:
pp: R : Type u_1
N : Type u_3
M' : Type u_5
inst✝⁵ : NormedField R
inst✝⁴ : SeminormedAddCommGroup N
inst✝³ : NormedSpace R N
inst✝² : NormedAddCommGroup M'
inst✝¹ : NormedSpace R M'
inst✝ : Nontrivial M'
hf' : IsConformalMap 0
⊢ False

Tactic:
rcases exists_ne (0 : M') with ⟨a, ha⟩

Goal state after:
R : Type u_1
N : Type u_3
M' : Type u_5
inst✝⁵ : NormedField R
inst✝⁴ : SeminormedAddCommGroup N
inst✝³ : NormedSpace R N
inst✝² : NormedAddCommGroup M'
inst✝¹ : NormedSpace R M'
inst✝ : Nontrivial M'
hf' : IsConformalMap 0
a : M'
ha : a ≠ 0
⊢ False
Module: Mathlib.MeasureTheory.Covering.Besicovitch

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

Tactic:
simpa only [a, Subtype.range_coe_subtype, ofPred_mem_eq]

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

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastr : a.r (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin N.succ
inej : i ≠ j
ah : Pairwise fun i j ↦ a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i ∨ a.r j ≤ ‖a.c j - a.c i‖ ∧ a.r i ≤ τ * a.r j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
⊢ 1 - δ ≤ ‖a.c i - a.c j‖

Tactic:
have τpos : 0 < τ := _root_.zero_lt_one.trans_le hτ

Goal state after:
E : Type u_1
inst✝ : NormedAddCommGroup E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastr : a.r (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin N.succ
inej : i ≠ j
ah : Pairwise fun i j ↦ a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i ∨ a.r j ≤ ‖a.c j - a.c i‖ ∧ a.r i ≤ τ * a.r j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
τpos : 0 < τ
⊢ 1 - δ ≤ ‖a.c i - a.c j‖
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 : ℕ∞ω
s : Set D
x : D
hf : ContDiffOn 𝕜 N f s
hg : ContDiffOn 𝕜 N g s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
hn : ↑n ≤ N
Du : Type (max uD uE uF uG) := ULift.{max uE uF uG, uD} D
Eu : Type (max uD uE uF uG) := ULift.{max uD uF uG, uE} E
⊢ ‖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‖

Tactic:
let Fu : Type max uD uE uF uG := ULift.{max uD uE uG, uF} F

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 : ℕ∞ω
s : Set D
x : D
hf : ContDiffOn 𝕜 N f s
hg : ContDiffOn 𝕜 N g s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
hn : ↑n ≤ N
Du : Type (max uD uE uF uG) := ULift.{max uE uF uG, uD} D
Eu : Type (max uD uE uF uG) := ULift.{max uD uF uG, uE} E
Fu : Type (max uD uE uF uG) := ULift.{max uD uE uG, uF} F
⊢ ‖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‖
Module: Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise

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

Tactic:
refine ((hg.of_order_le hi).isBigO.comp_tendsto hf.continuousAt).trans ?_

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

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

Tactic:
apply hd₀.continuousOn.union_continuousAt isOpen_Iio (by simp [h])

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

Goal state before:
pp: case refine_1
f : ℝ → ℝ
b c : ℝ
hb : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Iio b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Iio b, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
⊢ MonotoneOn f (Iic b)

Tactic:
apply monotoneOn_of_deriv_nonneg (convex_Iic b) (continuousOn_Iic hb hd₀)

Goal state after:
case refine_1.hf'
f : ℝ → ℝ
b c : ℝ
hb : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Iio b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Iio b, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
⊢ DifferentiableOn ℝ f (interior (Iic b))

case refine_1.hf'_nonneg
f : ℝ → ℝ
b c : ℝ
hb : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Iio b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Iio b, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
⊢ ∀ x ∈ interior (Iic b), 0 ≤ deriv f x
Module: Mathlib.Analysis.Calculus.DerivativeTest

Goal state before:
pp: case refine_1
f : ℝ → ℝ
b c : ℝ
hb : ContinuousAt f b
hc : ContinuousAt f c
hd₀ : DifferentiableOn ℝ f (Iio b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Iio b, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
⊢ MonotoneOn f (Iic b)

Tactic:
apply monotoneOn_of_deriv_nonneg (convex_Iic b) (continuousOn_Iic hb hd₀)

Goal state after:
case refine_1.hf'
f : ℝ → ℝ
b c : ℝ
hb : ContinuousAt f b
hc : ContinuousAt f c
hd₀ : DifferentiableOn ℝ f (Iio b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Iio b, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
⊢ DifferentiableOn ℝ f (interior (Iic b))

case refine_1.hf'_nonneg
f : ℝ → ℝ
b c : ℝ
hb : ContinuousAt f b
hc : ContinuousAt f c
hd₀ : DifferentiableOn ℝ f (Iio b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Iio b, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
⊢ ∀ x ∈ interior (Iic b), 0 ≤ deriv f x
Module: Mathlib.Analysis.Calculus.DerivativeTest

Goal state before:
pp: case refine_1
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
⊢ MonotoneOn f (Iic b)

Tactic:
apply monotoneOn_of_deriv_nonneg (convex_Iic b) (continuousOn_Iic hb hd₀)

Goal state after:
case refine_1.hf'
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
⊢ DifferentiableOn ℝ f (interior (Iic b))

case refine_1.hf'_nonneg
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
⊢ ∀ x ∈ interior (Iic b), 0 ≤ deriv f x
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: case refine_3.inl
α : 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 ∈ t0
⊢ r x ∈ f x

Tactic:
rw [r_t0 x hx]
      exact (hr0 _ hx).1

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

Goal state before:
pp: 𝕜 : 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 ℕ∞
x : E
ω : F → F [⋀^Fin n]→L[𝕜] G
f : E → F
hr : minSmoothness 𝕜 2 ≤ r
hω : DifferentiableWithinAt 𝕜 ω univ (f x)
hf : ContDiffWithinAt 𝕜 r f univ x
⊢ extDerivWithin (fun x ↦ (ω (f x)).compContinuousLinearMap (fderivWithin 𝕜 f univ x)) univ x =
    (extDerivWithin ω univ (f x)).compContinuousLinearMap (fderivWithin 𝕜 f univ x)

Tactic:
apply extDerivWithin_pullback (r := r) <;> simp [*]

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
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
V W : E → E
x : E
f : E → F
hf : ContDiffAt 𝕜 2 f x
hsymm : IsSymmSndFDerivAt 𝕜 f x
hW : DifferentiableAt 𝕜 W x
hV : DifferentiableAt 𝕜 V x
⊢ (fderiv 𝕜 f x) (lieBracket 𝕜 V W x) =
    (fderiv 𝕜 (fun x ↦ (fderiv 𝕜 f x) (W x)) x) (V x) - (fderiv 𝕜 (fun x ↦ (fderiv 𝕜 f x) (V x)) x) (W x)

Tactic:
simp only [← fderivWithin_univ, ← lieBracketWithin_univ, ← contDiffWithinAt_univ,
    ← isSymmSndFDerivWithinAt_univ, ← differentiableWithinAt_univ] at *

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
V W : E → E
x : E
f : E → F
hf : ContDiffWithinAt 𝕜 2 f univ x
hsymm : IsSymmSndFDerivWithinAt 𝕜 f univ x
hW : DifferentiableWithinAt 𝕜 W univ x
hV : DifferentiableWithinAt 𝕜 V univ x
⊢ (fderivWithin 𝕜 f univ x) (lieBracketWithin 𝕜 V W univ x) =
    (fderivWithin 𝕜 (fun x ↦ (fderivWithin 𝕜 f univ x) (W x)) univ x) (V x) -
      (fderivWithin 𝕜 (fun x ↦ (fderivWithin 𝕜 f univ x) (V x)) univ x) (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
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
V : F → F
x : E
h'f : (fderiv 𝕜 f x).IsInvertible
⊢ (fderiv 𝕜 f x) (pullback 𝕜 f V x) = V (f x)

Tactic:
rcases h'f with ⟨M, hM⟩
  simp [pullback_eq_of_fderiv_eq hM, ← hM]

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✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : E → F
f' : F
x v : E
h : HasLineDerivAt 𝕜 f f' x v
⊢ lineDeriv 𝕜 f x v = f'

Tactic:
by
  rw [h.unique h.lineDifferentiableAt.hasLineDerivAt]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
t : ℝ
ht : t ≠ 0
h : ContDiffAt ℝ n (fun x ↦ ‖x‖) x
h1 : ContDiffAt ℝ n (fun y ↦ t⁻¹ • y) (t • x)
h2 : ContDiffAt ℝ n (fun y ↦ |t| * ‖y‖) (t⁻¹ • t • x)
y : E
⊢ ‖y‖ = |1| * ‖y‖

Tactic:
abs_one,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
t : ℝ
ht : t ≠ 0
h : ContDiffAt ℝ n (fun x ↦ ‖x‖) x
h1 : ContDiffAt ℝ n (fun y ↦ t⁻¹ • y) (t • x)
h2 : ContDiffAt ℝ n (fun y ↦ |t| * ‖y‖) (t⁻¹ • t • x)
y : E
⊢ ‖y‖ = 1 * ‖y‖
Module: Mathlib.Analysis.Calculus.FDeriv.Norm

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
t : ℝ
ht : t ≠ 0
hd : ContDiffAt ℝ n (fun x ↦ ‖x‖) (t • x)
⊢ x = (t⁻¹ * t) • x

Tactic:
inv_mul_cancel₀ ht,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
t : ℝ
ht : t ≠ 0
hd : ContDiffAt ℝ n (fun x ↦ ‖x‖) (t • x)
⊢ x = 1 • x
Module: Mathlib.Analysis.Calculus.FDeriv.Norm

Goal state before:
pp: case e'_11
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) (t⁻¹ • t • x)
x✝ : E
⊢ ‖x✝‖ = |1| * ‖x✝‖

Tactic:
abs_one,

Goal state after:
case e'_11
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) (t⁻¹ • t • x)
x✝ : E
⊢ ‖x✝‖ = 1 * ‖x✝‖