mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

Goal state before:
pp: E✝ : Type u_1
inst✝⁵ : NormedAddCommGroup E✝
inst✝⁴ : NormedSpace ℝ E✝
inst✝³ : FiniteDimensional ℝ E✝
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
hR : 1 < R
x : E
hx : ‖x‖ ≤ 1
A : 0 < R + 1
⊢ y ((R - 1) / (R + 1)) (((R + 1) / 2)⁻¹ • x) = 1

Tactic:
apply y_eq_one_of_mem_closedBall (IR R hR)

Goal state after:
E✝ : Type u_1
inst✝⁵ : NormedAddCommGroup E✝
inst✝⁴ : NormedSpace ℝ E✝
inst✝³ : FiniteDimensional ℝ E✝
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
this✝¹ : MeasurableSpace E := ⋯
this✝ : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
hR : 1 < R
x : E
hx : ‖x‖ ≤ 1
A : 0 < R + 1
⊢ ((R + 1) / 2)⁻¹ • x ∈ closedBall 0 (1 - (R - 1) / (R + 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 δ
⊢ (↑s).Pairwise (Disjoint on fun c ↦ ball c δ)

Tactic:
rintro c hc d hd hcd

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 δ
c : E
hc : c ∈ ↑s
d : E
hd : d ∈ ↑s
hcd : c ≠ d
⊢ (Disjoint on fun c ↦ ball c δ) c d
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: case inl
α : 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 : μ s ≤ 0
⊢ ∃ t,
    ↑t ⊆ s ∧
      μ (s \ ⋃ x ∈ t, closedBall x (r x)) ≤ ↑N / (↑N + 1) * μ s ∧ (↑t).PairwiseDisjoint fun x ↦ closedBall x (r x)

Tactic:
have : μ s = 0 := le_bot_iff.1 hμs

Goal state after:
case inl
α : 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 : μ s ≤ 0
this : μ s = 0
⊢ ∃ t,
    ↑t ⊆ s ∧
      μ (s \ ⋃ x ∈ t, closedBall x (r x)) ≤ ↑N / (↑N + 1) * μ s ∧ (↑t).PairwiseDisjoint fun x ↦ closedBall x (r x)
Module: Mathlib.MeasureTheory.Measure.Haar.Unique

Goal state before:
pp: case a
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✝³ : IsFiniteMeasureOnCompacts μ'
inst✝² : μ'.IsMulLeftInvariant
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : μ'.InnerRegularCompactLTTop
s : Set G
hs : μ s ≠ ∞
h's : μ' s ≠ ∞
c : ℝ≥0 := ⋯
B : ∀ (s : Set G), MeasurableSet s → μ s < ∞ → μ' s < ∞ → μ' s = (c • μ) s
t : Set G := ⋯
st : s ⊆ t
mu'_t : μ' t = μ' s
mu_t : μ t = μ s
⊢ μ t < ∞

Tactic:
exact mu_t.le.trans_lt hs.lt_top

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

Goal state before:

Tactic:
‖iteratedFDerivWithin 𝕜 n (fun y : Du => B.precompR Du (f y) (fderivWithin 𝕜 g s y)) s x‖ ≤
            ‖B.precompR Du‖ * ∑ i ∈ Finset.range (n + 1),
              n.choose i * ‖iteratedFDerivWithin 𝕜 i f s x‖ *
                ‖iteratedFDerivWithin 𝕜 (n - i) (fderivWithin 𝕜 g s) s x‖ :=
          IH _ (hf.of_le (Nat.cast_le.2 (Nat.le_succ n))) (hg.fderivWithin hs In)
        _ ≤ ‖B‖ * ∑ i ∈ Finset.range (n + 1), n.choose i * ‖iteratedFDerivWithin 𝕜 i f s x‖ *
              ‖iteratedFDerivWithin 𝕜 (n - i) (fderivWithin 𝕜 g s) s x‖ := by
            gcongr; exact B.norm_precompR_le Du
        _ = _ := by
          congr 1
          apply Finset.sum_congr rfl fun i hi => ?_
          rw [Nat.succ_sub (Nat.lt_succ_iff.1 (Finset.mem_range.1 hi)),
            ← norm_iteratedFDerivWithin_fderivWithin hs hx]

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

Goal state before:
pp: case inr.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : a.c (last N) = 0
lastr : a.r (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin N.succ → E := fun i ↦ if ‖a.c i‖ ≤ 2 then a.c i else (2 / ‖a.c i‖) • a.c i
norm_c'_le : ∀ (i : Fin N.succ), ‖c' i‖ ≤ 2
i j : Fin N.succ
inej : i ≠ j
hij : ‖a.c i‖ ≤ ‖a.c j‖
Hj : 2 < ‖a.c j‖
H'j : ‖a.c j‖ ≤ 2 ↔ False
Hi : ‖a.c i‖ ≤ 2
⊢ 1 - δ ≤
    ‖(if ‖a.c i‖ ≤ 2 then a.c i else (2 / ‖a.c i‖) • a.c i) - if ‖a.c j‖ ≤ 2 then a.c j else (2 / ‖a.c j‖) • a.c j‖

Tactic:
Hi,

Goal state after:
case inr.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : a.c (last N) = 0
lastr : a.r (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin N.succ → E := fun i ↦ if ‖a.c i‖ ≤ 2 then a.c i else (2 / ‖a.c i‖) • a.c i
norm_c'_le : ∀ (i : Fin N.succ), ‖c' i‖ ≤ 2
i j : Fin N.succ
inej : i ≠ j
hij : ‖a.c i‖ ≤ ‖a.c j‖
Hj : 2 < ‖a.c j‖
H'j : ‖a.c j‖ ≤ 2 ↔ False
Hi : ‖a.c i‖ ≤ 2
⊢ 1 - δ ≤ ‖(if True then a.c i else (2 / ‖a.c i‖) • a.c i) - if ‖a.c j‖ ≤ 2 then a.c j else (2 / ‖a.c j‖) • a.c j‖
Module: Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise

Goal state before:
pp: 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
x : E
hfx : ContDiffAt ℝ (↑k) f x
hgx : ContDiffAt ℝ (↑k) g (f x)
⊢ (ftaylorSeries ℝ g (f x)).taylorComp (ftaylorSeries ℝ f x) k - iteratedFDeriv ℝ k (g ∘ f) a =
    (ftaylorSeries ℝ g (f x)).taylorComp (ftaylorSeries ℝ f x) k -
      (ftaylorSeries ℝ g (f a)).taylorComp (ftaylorSeries ℝ f a) k

Tactic:
iteratedFDeriv_comp hg.contDiffAt hf.contDiffAt le_rfl

Goal state after:
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
x : E
hfx : ContDiffAt ℝ (↑k) f x
hgx : ContDiffAt ℝ (↑k) g (f x)
⊢ (ftaylorSeries ℝ g (f x)).taylorComp (ftaylorSeries ℝ f x) k -
      (ftaylorSeries ℝ g (f a)).taylorComp (ftaylorSeries ℝ f a) k =
    (ftaylorSeries ℝ g (f x)).taylorComp (ftaylorSeries ℝ f x) k -
      (ftaylorSeries ℝ g (f a)).taylorComp (ftaylorSeries ℝ f a) k
Module: Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise

Goal state before:
pp: case refine_1
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
k : ℕ
α : ↑I
f : E → F
a : E
g : E → F
hf : ContDiffPointwiseHolderAt k α f a
hfg : f =ᶠ[𝓝 a] g
⊢ iteratedFDeriv ℝ k g =ᶠ[𝓝 a] iteratedFDeriv ℝ k f

Tactic:
exact hfg.symm.iteratedFDeriv ℝ _

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

Goal state before:
pp: case refine_2.inr
α : 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
t : Finset (α × ℝ)
ht : P t
B : Set α := ⋃ p ∈ t, closedBall p.1 p.2
hB : B = ⋃ p ∈ t, closedBall p.1 p.2
B_closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] B
s' : Set α := s \ B
r : α → ℝ
hr : ∀ x ∈ s', r x ∈ f x ∩ Ioo 0 1 ∧ Disjoint B (closedBall x (r x))
v : Finset α
vs' : ↑v ⊆ s'
hμv : μ (s' \ ⋃ x ∈ v, closedBall x (r x)) ≤ ↑N / (↑N + 1) * μ s'
hv : (↑v).PairwiseDisjoint fun x ↦ closedBall x (r x)
p : α × ℝ
hp : p ∈ t ∪ Finset.image (fun x ↦ (x, r x)) v
h'p : p ∈ Finset.image (fun x ↦ (x, r x)) v
⊢ p.1 ∈ s

Tactic:
rcases Finset.mem_image.1 h'p with ⟨p', p'v, rfl⟩
        exact ((mem_sdiff _).1 (vs' (Finset.mem_coe.2 p'v))).1

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✝ : SFinite μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
R : α → ℝ
hR : ∀ x ∈ s, 0 < R x
g : α → Set ℝ := fun x ↦ f x ∩ Ioo 0 (R x)
hg : ∀ x ∈ s, ∀ δ > 0, (g x ∩ Ioo 0 δ).Nonempty
r : α → ℝ
t : Set α
v_count : (graphOn r t).Countable
vs : ∀ p ∈ graphOn r t, p.1 ∈ s
vg : ∀ p ∈ graphOn r t, p.2 ∈ g p.1
μv : μ (s \ ⋃ p ∈ graphOn r t, closedBall p.1 p.2) = 0
v_disj : (graphOn r t).PairwiseDisjoint fun p ↦ closedBall p.1 p.2
hinj : InjOn (fun x ↦ (x, r x)) t
⊢ ∃ t r,
    t.Countable ∧
      t ⊆ s ∧
        (∀ x ∈ t, r x ∈ f x ∩ Ioo 0 (R x)) ∧
          μ (s \ ⋃ x ∈ t, closedBall x (r x)) = 0 ∧ t.PairwiseDisjoint fun x ↦ closedBall x (r x)

Tactic:
simp only [graphOn, forall_mem_image, biUnion_image, hinj.pairwiseDisjoint_image] at *

Goal state after:
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : Measure α
inst✝ : SFinite μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
R : α → ℝ
hR : ∀ x ∈ s, 0 < R x
g : α → Set ℝ := fun x ↦ f x ∩ Ioo 0 (R x)
hg : ∀ x ∈ s, ∀ δ > 0, (g x ∩ Ioo 0 δ).Nonempty
r : α → ℝ
t : Set α
v_count : ((fun x ↦ (x, r x)) '' t).Countable
hinj : InjOn (fun x ↦ (x, r x)) t
vs : ∀ ⦃x : α⦄, x ∈ t → x ∈ s
vg : ∀ ⦃x : α⦄, x ∈ t → r x ∈ g x
μv : μ (s \ ⋃ y ∈ t, closedBall y (r y)) = 0
v_disj : t.PairwiseDisjoint ((fun p ↦ closedBall p.1 p.2) ∘ fun x ↦ (x, r x))
⊢ ∃ t r,
    t.Countable ∧
      t ⊆ s ∧
        (∀ x ∈ t, r x ∈ f x ∩ Ioo 0 (R x)) ∧
          μ (s \ ⋃ x ∈ t, closedBall x (r x)) = 0 ∧ t.PairwiseDisjoint fun x ↦ closedBall x (r x)
Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x v w : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hf :
  ∀ (x_1 : Fin 2 → E),
    (ContinuousMultilinearMap.domDomCongr Fin.revPerm (iteratedFDerivWithin 𝕜 2 f s x)) x_1 =
      (iteratedFDerivWithin 𝕜 2 f s x) x_1
⊢ (iteratedFDerivWithin 𝕜 2 f s x) ![v, w] = (iteratedFDerivWithin 𝕜 2 f s x) ![w, v]

Tactic:
ContinuousMultilinearMap.domDomCongr_apply

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x v w : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hf :
  ∀ (x_1 : Fin 2 → E),
    ((iteratedFDerivWithin 𝕜 2 f s x) fun i ↦ x_1 (Fin.revPerm i)) = (iteratedFDerivWithin 𝕜 2 f s x) x_1
⊢ (iteratedFDerivWithin 𝕜 2 f s x) ![v, w] = (iteratedFDerivWithin 𝕜 2 f s x) ![w, v]
Module: Mathlib.Analysis.Calculus.DifferentialForm.VectorField

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
n : ℕ
s : Set E
x : E
ω : E → E [⋀^Fin (n + 1)]→L[𝕜] F
V : Fin (n + 2) → E → E
hω : DifferentiableWithinAt 𝕜 ω s x
hV : ∀ (i : Fin (n + 2)), DifferentiableWithinAt 𝕜 (V i) s x
hsx : UniqueDiffWithinAt 𝕜 s x
H₀ : ∀ (i : Fin (n + 2)) (j : Fin (n + 1)), DifferentiableWithinAt 𝕜 (fun y ↦ i.removeNth (fun x ↦ V x y) j) s x
i j : Fin (n + 1)
hj : i ≤ j
⊢ (-1) ^ ↑i.castSucc •
        (ω x)
          (Function.update (fun x_1 ↦ i.castSucc.removeNth (fun x_2 ↦ V x_2 x) x_1) j
            ((fderivWithin 𝕜 (fun y ↦ i.castSucc.removeNth (fun x ↦ V x y) j) s x) (V i.castSucc x))) +
      (-1) ^ ↑j.succ •
        (ω x)
          (Function.update (fun x_1 ↦ j.succ.removeNth (fun x_2 ↦ V x_2 x) x_1) i
            ((fderivWithin 𝕜 (fun y ↦ j.succ.removeNth (fun x ↦ V x y) i) s x) (V j.succ x))) =
    (-1) ^ (↑i + ↑j) •
      (ω x)
        (Matrix.vecCons (lieBracketWithin 𝕜 (V i.castSucc) (V j.succ) s x)
          (j.removeNth (i.castSucc.removeNth fun x_1 ↦ V x_1 x)))

Tactic:
simp only [← Fin.insertNth_removeNth, map_insertNth]

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
n : ℕ
s : Set E
x : E
ω : E → E [⋀^Fin (n + 1)]→L[𝕜] F
V : Fin (n + 2) → E → E
hω : DifferentiableWithinAt 𝕜 ω s x
hV : ∀ (i : Fin (n + 2)), DifferentiableWithinAt 𝕜 (V i) s x
hsx : UniqueDiffWithinAt 𝕜 s x
H₀ : ∀ (i : Fin (n + 2)) (j : Fin (n + 1)), DifferentiableWithinAt 𝕜 (fun y ↦ i.removeNth (fun x ↦ V x y) j) s x
i j : Fin (n + 1)
hj : i ≤ j
⊢ (-1) ^ ↑i.castSucc •
        (-1) ^ ↑j •
          (ω x)
            (Matrix.vecCons ((fderivWithin 𝕜 (fun y ↦ i.castSucc.removeNth (fun x ↦ V x y) j) s x) (V i.castSucc x))
              (j.removeNth fun x_1 ↦ i.castSucc.removeNth (fun x_2 ↦ V x_2 x) x_1)) +
      (-1) ^ ↑j.succ •
        (-1) ^ ↑i •
          (ω x)
            (Matrix.vecCons ((fderivWithin 𝕜 (fun y ↦ j.succ.removeNth (fun x ↦ V x y) i) s x) (V j.succ x))
              (i.removeNth fun x_1 ↦ j.succ.removeNth (fun x_2 ↦ V x_2 x) x_1)) =
    (-1) ^ (↑i + ↑j) •
      (ω x)
        (Matrix.vecCons (lieBracketWithin 𝕜 (V i.castSucc) (V j.succ) s x)
          (j.removeNth (i.castSucc.removeNth fun x_1 ↦ V x_1 x)))
Module: Mathlib.Analysis.Calculus.Implicit

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : CompleteSpace E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : CompleteSpace F
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace G
φ : ImplicitFunctionData 𝕜 E F G
x : G
y : E
⊢ (fderiv 𝕜
          (fun b ↦
            HasStrictFDerivAt.localInverse φ.prodFun (φ.leftDeriv.equivProdOfSurjectiveOfIsCompl φ.rightDeriv ⋯ ⋯ ⋯)
              φ.pt ⋯ (φ.leftFun φ.pt, b))
          (φ.rightFun φ.pt))
        x =
      y ↔
    φ.leftDeriv y = 0 ∧ φ.rightDeriv y = x

Tactic:
φ.hasStrictFDerivAt.to_localInverse.comp (φ.rightFun φ.pt)
    ((hasStrictFDerivAt_const _ _).prodMk (hasStrictFDerivAt_id _)) |>.hasFDerivAt |>.fderiv

Goal state after:
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : CompleteSpace E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : CompleteSpace F
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace G
φ : ImplicitFunctionData 𝕜 E F G
x : G
y : E
⊢ (↑(φ.leftDeriv.equivProdOfSurjectiveOfIsCompl φ.rightDeriv ⋯ ⋯ ⋯).symm ∘SL
          ContinuousLinearMap.prod 0 (ContinuousLinearMap.id 𝕜 G))
        x =
      y ↔
    φ.leftDeriv y = 0 ∧ φ.rightDeriv y = x
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 𝕜 3 g (f x)
hf : ContDiffAt 𝕜 3 f x
⊢ iteratedDeriv 3 (g ∘ f) x =
    ((iteratedFDeriv 𝕜 3 g (f x)) fun x_1 ↦ deriv f x) +
          (iteratedFDeriv 𝕜 2 g (f x)) ![iteratedDeriv 2 f x, deriv f x] +
        2 • (iteratedFDeriv 𝕜 2 g (f x)) ![deriv f x, iteratedDeriv 2 f x] +
      (fderiv 𝕜 g (f x)) (iteratedDeriv 3 f x)

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

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

Goal state before:
pp: case hg
a b : ℝ
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAlgebra ℝ 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : IsScalarTower ℝ 𝕜 E
u u' : ℝ → 𝕜
v v' : ℝ → E
hu : ContinuousOn u [[a, b]]
hv : ContinuousOn v [[a, b]]
huu' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt u (u' x) (Ioi x) x
hvv' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt v (v' x) (Ioi x) x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
⊢ IntervalIntegrable (fun x ↦ u' x • v x) volume a b

Tactic:
· exact hu'.smul_continuousOn hv

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

Goal state before:
pp: s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf : MonotoneOn f s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : Set ℝ := {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}
a_count : a.Countable
s₁ : Set ℝ := s \ a
hs₁ : MeasurableSet s₁
u : Set ℝ := {c | ∃ x y, x ∈ s₁ ∧ y ∈ s₁ ∧ x < y ∧ f x = c ∧ f y = c}
hu : u.Countable
b : Set ℝ := s₁ ∩ f ⁻¹' u
hb : MeasurableSet b
c : Set ℝ := s₁ \ b
hc : MeasurableSet c
x : ℝ
hx : x ∈ b
⊢ ∃ p ∈ s₁, p ≠ x ∧ f p = f x

Tactic:
rcases hx.2 with ⟨p, q, ps₁, qs₁, pq, hp, hq⟩
      rcases eq_or_ne p x with h'p | h'p
      · exact ⟨q, qs₁, (h'p.symm.le.trans_lt pq).ne', hq⟩
      · exact ⟨p, ps₁, h'p, hp⟩

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‖}
s_subset : ∀ x ∈ s, ∃ n z, x ∈ M n z
n : ℕ
z : ↑T
x : E
xs : x ∈ s
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (M n z)
y : E
hy : y ∈ s ∩ ball x (u n)
a : ℕ → E
aM : ∀ (k : ℕ), a k ∈ M n z
a_lim : Tendsto a atTop (𝓝 x)
⊢ ‖f y - f x - (f' ↑↑z) (y - x)‖ ≤ ↑(r (f' ↑↑z)) * ‖y - x‖

Tactic:
have L1 :
      Tendsto (fun k : ℕ => ‖f y - f (a k) - (f' z) (y - a k)‖) atTop
        (𝓝 ‖f y - f x - (f' z) (y - x)‖) := by
      apply Tendsto.norm
      have L : Tendsto (fun k => f (a k)) atTop (𝓝 (f x)) := by
        apply (hf' x xs).continuousWithinAt.tendsto.comp
        apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ a_lim
        exact Eventually.of_forall fun k => (aM k).1
      apply Tendsto.sub (tendsto_const_nhds.sub L)
      exact ((f' z).continuous.tendsto _).comp (tendsto_const_nhds.sub a_lim)

Goal state after:
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
n : ℕ
z : ↑T
x : E
xs : x ∈ s
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (M n z)
y : E
hy : y ∈ s ∩ ball x (u n)
a : ℕ → E
aM : ∀ (k : ℕ), a k ∈ M n z
a_lim : Tendsto a atTop (𝓝 x)
L1 : Tendsto (fun k ↦ ‖f y - f (a k) - (f' ↑↑z) (y - a k)‖) atTop (𝓝 ‖f y - f x - (f' ↑↑z) (y - x)‖)
⊢ ‖f y - f x - (f' ↑↑z) (y - x)‖ ≤ ↑(r (f' ↑↑z)) * ‖y - x‖
Module: Mathlib.Analysis.Calculus.LHopital

Goal state before:
pp: case inr.inl
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hg' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, g' x ≠ 0
hfa : Tendsto f (𝓝[s \ {a}] a) (𝓝 0)
hga : Tendsto g (𝓝[s \ {a}] a) (𝓝 0)
hdiv : Tendsto (fun x ↦ f' x / g' x) (𝓝[s \ {a}] a) l
has : a ∈ closure s
h : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, s \ {a} ∈ 𝓝 x
hff' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, HasDerivAt g (g' x) x
hs_Iio : (s ∩ Iio a).Nonempty
hs_Ioi : s ∩ Ioi a = ∅
⊢ Tendsto (fun x ↦ f x / g x) (𝓝[s \ {a}] a) l

Tactic:
simp_rw [hs.nhdsWithin_sdiff_eq_nhdsLT has hs_Iio hs_Ioi] at *
    exact lhopital_zero_nhdsLT hff' hgg' hg' hfa hga hdiv

Goal state after:
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
⊢ IntervalIntegrable (fun x ↦ f' x • g (f x)) volume a b ↔ IntervalIntegrable g volume (f a) (f b)

Tactic:
intervalIntegrable_iff_integrableOn_Icc_of_le hab,

Goal state after:
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
⊢ IntegrableOn (fun x ↦ f' x • g (f x)) (Icc a b) volume ↔ IntervalIntegrable g volume (f a) (f b)
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: case neg
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : l.IsCountablyGenerated
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : ι → ℝ
f : ℝ → E
ha : Tendsto a l atBot
b : ℝ
hb : IntegrableOn f (Iio b) μ
this : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in Iio b, f x ∂μ - ∫ (x : ℝ) in Ico (a i) b, f x ∂μ = ∫ (x : ℝ) in Iio (a i), f x ∂μ
⊢ Tendsto (fun i ↦ ∫ (x : ℝ) in Iio (a i), f x ∂μ) l (𝓝 (∫ (x : ℝ) in Iio b, f x ∂μ - ∫ (x : ℝ) in Iio b, f x ∂μ))

Tactic:
exact Tendsto.congr' this (Tendsto.const_sub _ <| tendsto_integral_Ico_integral_Iio b hb ha)

Goal state after: