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

Goal state before:
pp: case refine_1.left
α : 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 ∈ (fun x ↦ (x, r x)) '' ↑v
q : α × ℝ
hq : q ∈ (fun x ↦ (x, r x)) '' ↑v
hpq : p ≠ q
⊢ Function.onFun Disjoint (fun p ↦ closedBall p.1 p.2) p q

Tactic:
rcases (mem_image _ _ _).1 hp with ⟨p', p'v, rfl⟩

Goal state after:
case refine_1.left
α : 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)
q : α × ℝ
hq : q ∈ (fun x ↦ (x, r x)) '' ↑v
p' : α
p'v : p' ∈ ↑v
hp : (p', r p') ∈ (fun x ↦ (x, r x)) '' ↑v
hpq : (p', r p') ≠ q
⊢ Function.onFun Disjoint (fun p ↦ closedBall p.1 p.2) (p', r p') q
Module: Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise

Goal state before:
pp: case hq₁_bdd
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
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 a) fun x ↦ ‖ftaylorSeries ℝ f x i‖

Tactic:
exact (hf.contDiffAt.continuousAt_iteratedFDeriv (mod_cast hi)).norm.isBoundedUnder_le

Goal state after:
Module: Mathlib.Analysis.Calculus.Deriv.Star

Goal state before:
pp: 𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : StarRing 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : StarAddMonoid F
inst✝² : StarModule 𝕜 F
inst✝¹ : ContinuousStar F
f : 𝕜 → F
x : 𝕜
inst✝ : TrivialStar 𝕜
s : Set 𝕜
⊢ derivWithin (fun y ↦ star (f y)) s x = star (derivWithin f s x)

Tactic:
by
  by_cases hxs : UniqueDiffWithinAt 𝕜 s x
  · exact DFunLike.congr_fun (fderivWithin_star hxs) _
  · simp [derivWithin_zero_of_not_uniqueDiffWithinAt hxs]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
s : Set E
ι : Type u_2
A' : Type u_4
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
f : ι → E → A'
N : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
i : ι
u : Finset ι
hi : i ∉ u
IH :
  (∀ i ∈ u, ContDiffOn 𝕜 N (f i) s) →
    ∀ {n : ℕ},
      ↑n ≤ N →
        ‖iteratedFDerivWithin 𝕜 n (fun x ↦ ∏ j ∈ u, f j x) s x‖ ≤
          ∑ p ∈ u.sym n, ↑(↑p).countPerms * ∏ j ∈ u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
n : ℕ
hn : ↑n ≤ N
hf : ContDiffOn 𝕜 N (f i) s ∧ ∀ a ∈ u, ContDiffOn 𝕜 N (f a) s
⊢ ∀ i_1 ∈ Finset.univ,
    ↑(↑↑i_1).countPerms * ∏ j ∈ insert i u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑↑i_1) (f j) s x‖ =
      ((fun v ↦ ↑v.countPerms * ∏ j ∈ insert i u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j v) (f j) s x‖) ∘
          Sym.toMultiset ∘ Subtype.val ∘ ⇑(Finset.symInsertEquiv hi).symm)
        ((Finset.symInsertEquiv hi) i_1)

Tactic:
by simp only [← comp_apply (g := Finset.symInsertEquiv hi), comp_assoc]; simp

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

Goal state before:
pp: case hi
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
Fu : Type u
inst✝³ : NormedAddCommGroup Fu
inst✝² : NormedSpace 𝕜 Fu
f : E → Fu
s : Set E
t : Set Fu
x : E
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
n : ℕ
IH :
  ∀ m ≤ n,
    ∀ {Gu : Type u} [inst : NormedAddCommGroup Gu] [inst_1 : NormedSpace 𝕜 Gu] {g : Fu → Gu},
      ContDiffOn 𝕜 (↑m) g t →
        ContDiffOn 𝕜 (↑m) f s →
          (∀ i ≤ m, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C) →
            (∀ (i : ℕ), 1 ≤ i → i ≤ m → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i) →
              ‖iteratedFDerivWithin 𝕜 m (g ∘ f) s x‖ ≤ ↑m ! * C * D ^ m
Gu : Type u
inst✝¹ : NormedAddCommGroup Gu
inst✝ : NormedSpace 𝕜 Gu
g : Fu → Gu
hg : ContDiffOn 𝕜 (↑(n + 1)) g t
hf : ContDiffOn 𝕜 (↑(n + 1)) f s
hC : ∀ i ≤ n + 1, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C
hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n + 1 → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i
M : ↑n < ↑n.succ
Cnonneg : 0 ≤ C
Dnonneg : 0 ≤ D
I : ∀ i ∈ Finset.range (n + 1), ‖iteratedFDerivWithin 𝕜 i (fderivWithin 𝕜 g t ∘ f) s x‖ ≤ ↑i ! * C * D ^ i
⊢ ‖iteratedFDerivWithin 𝕜 (n + 1) (g ∘ f) s x‖ ≤ ↑(n + 1)! * C * D ^ (n + 1)

Tactic:
have J : ∀ i, ‖iteratedFDerivWithin 𝕜 (n - i) (fderivWithin 𝕜 f s) s x‖ ≤ D ^ (n - i + 1) := by
    intro i
    have : ‖iteratedFDerivWithin 𝕜 (n - i + 1) f s x‖ ≤ D ^ (n - i + 1) :=
      hD (n - i + 1) (by simp) (Nat.succ_le_succ tsub_le_self)
    simpa [iteratedFDerivWithin_succ_eq_comp_right hs hx]

Goal state after:
case hi
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
Fu : Type u
inst✝³ : NormedAddCommGroup Fu
inst✝² : NormedSpace 𝕜 Fu
f : E → Fu
s : Set E
t : Set Fu
x : E
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
n : ℕ
IH :
  ∀ m ≤ n,
    ∀ {Gu : Type u} [inst : NormedAddCommGroup Gu] [inst_1 : NormedSpace 𝕜 Gu] {g : Fu → Gu},
      ContDiffOn 𝕜 (↑m) g t →
        ContDiffOn 𝕜 (↑m) f s →
          (∀ i ≤ m, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C) →
            (∀ (i : ℕ), 1 ≤ i → i ≤ m → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i) →
              ‖iteratedFDerivWithin 𝕜 m (g ∘ f) s x‖ ≤ ↑m ! * C * D ^ m
Gu : Type u
inst✝¹ : NormedAddCommGroup Gu
inst✝ : NormedSpace 𝕜 Gu
g : Fu → Gu
hg : ContDiffOn 𝕜 (↑(n + 1)) g t
hf : ContDiffOn 𝕜 (↑(n + 1)) f s
hC : ∀ i ≤ n + 1, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C
hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n + 1 → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i
M : ↑n < ↑n.succ
Cnonneg : 0 ≤ C
Dnonneg : 0 ≤ D
I : ∀ i ∈ Finset.range (n + 1), ‖iteratedFDerivWithin 𝕜 i (fderivWithin 𝕜 g t ∘ f) s x‖ ≤ ↑i ! * C * D ^ i
J : ∀ (i : ℕ), ‖iteratedFDerivWithin 𝕜 (n - i) (fderivWithin 𝕜 f s) s x‖ ≤ D ^ (n - i + 1)
⊢ ‖iteratedFDerivWithin 𝕜 (n + 1) (g ∘ f) s x‖ ≤ ↑(n + 1)! * C * D ^ (n + 1)
Module: Mathlib.Analysis.Calculus.DerivativeTest

Goal state before:
pp: f : ℝ → ℝ
x₀ : ℝ
hf : deriv f x₀ > 0
hx : f x₀ = 0
⊢ ∀ᶠ (x : ℝ) in 𝓝[≠] x₀, sign (f x) = sign (x - x₀)

Tactic:
have h_tendsto := hasDerivAt_iff_tendsto_slope.mp
    (differentiableAt_of_deriv_ne_zero <| ne_of_gt hf).hasDerivAt

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 : ℝ) in 𝓝[≠] x₀, sign (f x) = sign (x - x₀)
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: case refine_3.inr
α : 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 ∈ ⋃ i, Subtype.val '' S i
⊢ r x ∈ f x

Tactic:
have h'x : x ∈ s' := by
        simp only [mem_iUnion, mem_image] at hx
        rcases hx with ⟨i, y, _, rfl⟩
        exact y.2
      simp only [r, if_pos h'x, (hr1 x h'x).1.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 ℕ∞
s : Set E
x : E
ω : F → F [⋀^Fin n]→L[𝕜] G
f : E → F
t : Set F
hω : DifferentiableWithinAt 𝕜 ω t (f x)
hf : ContDiffWithinAt 𝕜 r f s x
hr : minSmoothness 𝕜 2 ≤ r
hs : UniqueDiffOn 𝕜 s
hxc : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
hxs : x ∈ s
hst : MapsTo f s t
hdf : DifferentiableWithinAt 𝕜 f s x
hd2f : DifferentiableWithinAt 𝕜 (fderivWithin 𝕜 f s) s x
⊢ alternatizeUncurryFin
      (compContinuousLinearMapCLM (fderivWithin 𝕜 f s x) ∘SL fderivWithin 𝕜 ω t (f x) ∘SL fderivWithin 𝕜 f s x) =
    (alternatizeUncurryFin (fderivWithin 𝕜 ω t (f x))).compContinuousLinearMap (fderivWithin 𝕜 f s x)

Tactic:
ext v
    simp +unfoldPartialApp [alternatizeUncurryFin_apply, Fin.removeNth, Function.comp_def]

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
s : Set E
x : E
f : E → F
hf : ContDiffWithinAt 𝕜 2 f s x
hsymm : IsSymmSndFDerivWithinAt 𝕜 f s x
hs : UniqueDiffOn 𝕜 s
hxs : x ∈ s
hW : DifferentiableWithinAt 𝕜 W s x
hV : DifferentiableWithinAt 𝕜 V s x
⊢ 1 + 1 ≤ 2

Tactic:
decide

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
n : ℕ∞ω
hf : ContDiffAt 𝕜 n f x
hn : minSmoothness 𝕜 2 ≤ n
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:
apply fderiv_apply_lieBracket_of_isSymmSndFDerivAt <;> try assumption

Goal state after:
case hf
𝕜 : 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
n : ℕ∞ω
hf : ContDiffAt 𝕜 n f x
hn : minSmoothness 𝕜 2 ≤ n
hW : DifferentiableAt 𝕜 W x
hV : DifferentiableAt 𝕜 V x
⊢ ContDiffAt 𝕜 2 f x

case hsymm
𝕜 : 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
n : ℕ∞ω
hf : ContDiffAt 𝕜 n f x
hn : minSmoothness 𝕜 2 ≤ n
hW : DifferentiableAt 𝕜 W x
hV : DifferentiableAt 𝕜 V x
⊢ IsSymmSndFDerivAt 𝕜 f x
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
⊢ ((extDerivWithin ω s x) fun x_1 ↦ V x_1 x) =
    ∑ i, (-1) ^ ↑i • (fderivWithin 𝕜 (fun x ↦ (ω x) (i.removeNth fun x_1 ↦ V x_1 x)) s x) (V i x) -
      ∑ i,
        ∑ j ≥ i,
          (-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:
symm

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, (-1) ^ ↑i • (fderivWithin 𝕜 (fun x ↦ (ω x) (i.removeNth fun x_1 ↦ V x_1 x)) s x) (V i x) -
      ∑ i,
        ∑ j ≥ i,
          (-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))) =
    (extDerivWithin ω s x) fun x_1 ↦ V x_1 x
Module: Mathlib.Analysis.Calculus.VectorField

Goal state before:
pp: case hx
𝕜 : 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
inst✝ : CompleteSpace E
f : E → F
V : F → F
s : Set E
t : Set F
x : E
hV : DifferentiableWithinAt 𝕜 V t (f x)
hf : ContDiffWithinAt 𝕜 2 f s x
hf' : (fderivWithin 𝕜 f s x).IsInvertible
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
M : E → E ≃L[𝕜] F
M_symm_smooth : ContDiffWithinAt 𝕜 1 (fun y ↦ ↑(M y).symm) s x
hM : ∀ᶠ (y : E) in 𝓝[s] x, ↑(M y) = fderivWithin 𝕜 f s y
this : DifferentiableWithinAt 𝕜 (fun y ↦ ↑(M y).symm (V (f y))) s x
⊢ (fderivWithin 𝕜 f s x).inverse (V (f x)) = ↑(M x).symm (V (f x))

Tactic:
have hMx : M x = fderivWithin 𝕜 f s x := by apply mem_of_mem_nhdsWithin hx hM
    simp [← hMx]

Goal state after:
Module: Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain

Goal state before:
pp: case codisjoint
𝕜 : 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
⊢ Codisjoint (↑f'u).ker (↑(ContinuousLinearMap.fst 𝕜 E₁ E₂)).ker

Tactic:
rw [Submodule.codisjoint_iff_exists_add_eq]
      intro v
      have ⟨y, hy⟩ := if₂u.surjective (f'u v)
      use v - (0, y), (0, y)
      aesop

Goal state after:
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Analytic

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CharZero 𝕜
inst✝ : CompleteSpace 𝕜
z₀ : 𝕜
R R₁ : 𝕜 → 𝕜
hf1 : ∀ (z : 𝕜), AnalyticAt 𝕜 R₁ z
k : ℕ
IH :
  ∀ {t : ℕ},
    (∀ (z : 𝕜), R z = (z - z₀) ^ (k + t) * R₁ z) →
      ∃ R₂,
        (∀ (z : 𝕜), AnalyticAt 𝕜 R₂ z) ∧
          ∀ (z : 𝕜), iteratedDeriv k R z = (z - z₀) ^ t * (↑(k + t)! / ↑t ! * R₁ z + (z - z₀) * R₂ z)
t : ℕ
hR₁ : ∀ (z : 𝕜), R z = (z - z₀) ^ (k + 1 + t) * R₁ z
R₂ : 𝕜 → 𝕜
hR₂ : ∀ (z : 𝕜), AnalyticAt 𝕜 R₂ z
hR₂_eq : ∀ (z : 𝕜), iteratedDeriv k R z = (z - z₀) ^ (t + 1) * (↑(k + (t + 1))! / ↑(t + 1)! * R₁ z + (z - z₀) * R₂ z)
R₂' : 𝕜 → 𝕜 := fun z ↦ (↑t + 1) * R₂ z + (↑(k + (t + 1))! / ↑(t + 1)! * deriv R₁ z + (R₂ z + (z - z₀) * deriv R₂ z))
z : 𝕜
⊢ iteratedDeriv (k + 1) R z =
    deriv (fun w ↦ (w - z₀) ^ (t + 1) * (↑(k + (t + 1))! / ↑(t + 1)! * R₁ w + (w - z₀) * R₂ w)) z

Tactic:
by
        rw [iteratedDeriv_succ, funext hR₂_eq]

Goal state after:
Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
g : 𝕜 → E
f : 𝕜 → 𝕜
x : 𝕜
hg : ContDiffAt 𝕜 2 g (f x)
hf : ContDiffAt 𝕜 2 f x
⊢ iteratedDeriv 2 (g ∘ f) x = deriv f x ^ 2 • iteratedDeriv 2 g (f x) + iteratedDeriv 2 f x • deriv g (f x)

Tactic:
simp only [← iteratedDerivWithin_univ, ← derivWithin_univ]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
g : 𝕜 → E
f : 𝕜 → 𝕜
x : 𝕜
hg : ContDiffAt 𝕜 2 g (f x)
hf : ContDiffAt 𝕜 2 f x
⊢ iteratedDerivWithin 2 (g ∘ f) univ x =
    derivWithin f univ x ^ 2 • iteratedDerivWithin 2 g univ (f x) +
      iteratedDerivWithin 2 f univ x • derivWithin g univ (f x)
Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
g : 𝕜 → E
f : 𝕜 → 𝕜
x : 𝕜
hg : ContDiffAt 𝕜 3 g (f x)
hf : ContDiffAt 𝕜 3 f x
⊢ iteratedDeriv 3 (g ∘ f) x =
    deriv f x ^ 3 • iteratedDeriv 3 g (f x) + 3 • iteratedDeriv 2 f x • deriv f x • iteratedDeriv 2 g (f x) +
      iteratedDeriv 3 f x • deriv g (f x)

Tactic:
simp only [← iteratedDerivWithin_univ, ← derivWithin_univ]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
g : 𝕜 → E
f : 𝕜 → 𝕜
x : 𝕜
hg : ContDiffAt 𝕜 3 g (f x)
hf : ContDiffAt 𝕜 3 f x
⊢ iteratedDerivWithin 3 (g ∘ f) univ x =
    derivWithin f univ x ^ 3 • iteratedDerivWithin 3 g univ (f x) +
        3 • iteratedDerivWithin 2 f univ x • derivWithin f univ x • iteratedDerivWithin 2 g univ (f x) +
      iteratedDerivWithin 3 f univ x • derivWithin g univ (f x)
Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
g f : 𝕜 → 𝕜
x : 𝕜
hg : ContDiffAt 𝕜 2 g (f x)
hf : ContDiffAt 𝕜 2 f x
⊢ iteratedDeriv 2 (g ∘ f) x = iteratedDeriv 2 g (f x) * deriv f x ^ 2 + deriv g (f x) * iteratedDeriv 2 f x

Tactic:
simp only [← iteratedDerivWithin_univ, ← derivWithin_univ]

Goal state after:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
g f : 𝕜 → 𝕜
x : 𝕜
hg : ContDiffAt 𝕜 2 g (f x)
hf : ContDiffAt 𝕜 2 f x
⊢ iteratedDerivWithin 2 (g ∘ f) univ x =
    iteratedDerivWithin 2 g univ (f x) * derivWithin f univ x ^ 2 +
      derivWithin g univ (f x) * iteratedDerivWithin 2 f univ x
Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
g f : 𝕜 → 𝕜
x : 𝕜
hg : ContDiffAt 𝕜 3 g (f x)
hf : ContDiffAt 𝕜 3 f x
⊢ iteratedDeriv 3 (g ∘ f) x =
    iteratedDeriv 3 g (f x) * deriv f x ^ 3 + 3 * iteratedDeriv 2 g (f x) * iteratedDeriv 2 f x * deriv f x +
      deriv g (f x) * iteratedDeriv 3 f x

Tactic:
simp only [← iteratedDerivWithin_univ, ← derivWithin_univ]

Goal state after:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
g f : 𝕜 → 𝕜
x : 𝕜
hg : ContDiffAt 𝕜 3 g (f x)
hf : ContDiffAt 𝕜 3 f x
⊢ iteratedDerivWithin 3 (g ∘ f) univ x =
    iteratedDerivWithin 3 g univ (f x) * derivWithin f univ x ^ 3 +
        3 * iteratedDerivWithin 2 g univ (f x) * iteratedDerivWithin 2 f univ x * derivWithin f univ x +
      derivWithin g univ (f x) * iteratedDerivWithin 3 f univ x
Module: Mathlib.Analysis.Calculus.LHopital

Goal state before:
pp: a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Ioi a, g' x ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun x ↦ f' x / g' x) atTop l
a' : ℝ
haa' : a < a'
ha' : 0 < a'
⊢ Tendsto (fun x ↦ f x / g x) atTop l

Tactic:
have fact1 : ∀ x : ℝ, x ∈ Ioo 0 a'⁻¹ → x ≠ 0 := fun _ hx => (ne_of_lt hx.1).symm

Goal state after:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Ioi a, g' x ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun x ↦ f' x / g' x) atTop l
a' : ℝ
haa' : a < a'
ha' : 0 < a'
fact1 : ∀ x ∈ Ioo 0 a'⁻¹, x ≠ 0
⊢ Tendsto (fun x ↦ f x / g x) atTop l
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 :
  (¬𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬𝓝[s ∩ Iio x] x = ⊥) ∧
    x ∉ s \ ({x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}) ∩ f ⁻¹' u
⊢ AccPt x (𝓟 s)

Tactic:
accPt_principal_iff_nhdsWithin

Goal state after:
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 :
  (¬𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬𝓝[s ∩ Iio x] x = ⊥) ∧
    x ∉ s \ ({x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}) ∩ f ⁻¹' u
⊢ (𝓝[s \ {x}] x).NeBot
Module: Mathlib.Analysis.Calculus.LHopital

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

Tactic:
(first | apply eventually_nhdsWithin_of_eventually_nhds |
      apply tendsto_nhdsWithin_of_tendsto_nhds)

Goal state after:
case hff'
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt g (g' x) x
hg' : ∀ᶠ (x : ℝ) in 𝓝 a, g' x ≠ 0
hfa : Tendsto f (𝓝 a) (𝓝 0)
hga : Tendsto g (𝓝 a) (𝓝 0)
hdiv : Tendsto (fun x ↦ f' x / g' x) (𝓝 a) l
⊢ ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt f (f' x) x