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

Goal state before:
pp: case cons
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
ι : Type u_3
f : ι → 𝕜 → 𝕜'
x : 𝕜
a : ι
s : Finset ι
ha : a ∉ s
ih :
  (∀ i ∈ s, f i x ≠ 0) →
    (∀ i ∈ s, DifferentiableAt 𝕜 (f i) x) → logDeriv (fun x ↦ ∏ i ∈ s, f i x) x = ∑ i ∈ s, logDeriv (f i) x
hf : f a x ≠ 0 ∧ ∀ x_1 ∈ s, f x_1 x ≠ 0
hd : DifferentiableAt 𝕜 (f a) x ∧ ∀ x_1 ∈ s, DifferentiableAt 𝕜 (f x_1) x
⊢ logDeriv (fun x ↦ f a x * ∏ i ∈ s, f i x) x = logDeriv (f a) x + ∑ i ∈ s, logDeriv (f i) x

Tactic:
rw [logDeriv_mul, ih hf.2 hd.2]

Goal state after:
case cons.hf
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
ι : Type u_3
f : ι → 𝕜 → 𝕜'
x : 𝕜
a : ι
s : Finset ι
ha : a ∉ s
ih :
  (∀ i ∈ s, f i x ≠ 0) →
    (∀ i ∈ s, DifferentiableAt 𝕜 (f i) x) → logDeriv (fun x ↦ ∏ i ∈ s, f i x) x = ∑ i ∈ s, logDeriv (f i) x
hf : f a x ≠ 0 ∧ ∀ x_1 ∈ s, f x_1 x ≠ 0
hd : DifferentiableAt 𝕜 (f a) x ∧ ∀ x_1 ∈ s, DifferentiableAt 𝕜 (f x_1) x
⊢ f a x ≠ 0

case cons.hg
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
ι : Type u_3
f : ι → 𝕜 → 𝕜'
x : 𝕜
a : ι
s : Finset ι
ha : a ∉ s
ih :
  (∀ i ∈ s, f i x ≠ 0) →
    (∀ i ∈ s, DifferentiableAt 𝕜 (f i) x) → logDeriv (fun x ↦ ∏ i ∈ s, f i x) x = ∑ i ∈ s, logDeriv (f i) x
hf : f a x ≠ 0 ∧ ∀ x_1 ∈ s, f x_1 x ≠ 0
hd : DifferentiableAt 𝕜 (f a) x ∧ ∀ x_1 ∈ s, DifferentiableAt 𝕜 (f x_1) x
⊢ ∏ i ∈ s, f i x ≠ 0

case cons.hdf
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
ι : Type u_3
f : ι → 𝕜 → 𝕜'
x : 𝕜
a : ι
s : Finset ι
ha : a ∉ s
ih :
  (∀ i ∈ s, f i x ≠ 0) →
    (∀ i ∈ s, DifferentiableAt 𝕜 (f i) x) → logDeriv (fun x ↦ ∏ i ∈ s, f i x) x = ∑ i ∈ s, logDeriv (f i) x
hf : f a x ≠ 0 ∧ ∀ x_1 ∈ s, f x_1 x ≠ 0
hd : DifferentiableAt 𝕜 (f a) x ∧ ∀ x_1 ∈ s, DifferentiableAt 𝕜 (f x_1) x
⊢ DifferentiableAt 𝕜 (f a) x

case cons.hdg
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
ι : Type u_3
f : ι → 𝕜 → 𝕜'
x : 𝕜
a : ι
s : Finset ι
ha : a ∉ s
ih :
  (∀ i ∈ s, f i x ≠ 0) →
    (∀ i ∈ s, DifferentiableAt 𝕜 (f i) x) → logDeriv (fun x ↦ ∏ i ∈ s, f i x) x = ∑ i ∈ s, logDeriv (f i) x
hf : f a x ≠ 0 ∧ ∀ x_1 ∈ s, f x_1 x ≠ 0
hd : DifferentiableAt 𝕜 (f a) x ∧ ∀ x_1 ∈ s, DifferentiableAt 𝕜 (f x_1) x
⊢ DifferentiableAt 𝕜 (fun x ↦ ∏ i ∈ s, f i x) x
Module: Mathlib.Analysis.Calculus.ContDiff.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
s : Set E
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
hf : HasFTaylorSeriesUpToOn n f p s
g : G →ᴬ[𝕜] E
⊢ HasFTaylorSeriesUpToOn n (f ∘ ⇑g) (fun x k ↦ (p (g x) k).compContinuousLinearMap fun x ↦ g.contLinear) (⇑g ⁻¹' s)

Tactic:
by
  let A : ∀ m : ℕ, (E [×m]→L[𝕜] F) → G [×m]→L[𝕜] F :=
    fun m h ↦ h.compContinuousLinearMap fun _ ↦ g.contLinear
  have hA : ∀ m, IsBoundedLinearMap 𝕜 (A m) := fun m =>
    isBoundedLinearMap_continuousMultilinearMap_comp_linear g.contLinear
  constructor
  · intro x hx
    simp only [(hf.zero_eq (g x) hx).symm, Function.comp_apply]
    change (p (g x) 0 fun _ : Fin 0 => g.contLinear 0) = p (g x) 0 0
    rw [map_zero]
    rfl
  · intro m hm x hx
    convert!
      (hA m).hasFDerivAt.comp_hasFDerivWithinAt x
        ((hf.fderivWithin m hm (g x) hx).comp x g.hasFDerivWithinAt (Subset.refl _))
    ext y v
    change p (g x) (Nat.succ m) (g.contLinear ∘ cons y v)
      = p (g x) m.succ (cons (g.contLinear y) (g.contLinear ∘ v))
    rw [comp_cons]
  · intro m hm
    exact (hA m).continuous.comp_continuousOn <| (hf.cont m hm).comp g.continuous.continuousOn <|
      Subset.refl _

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

Goal state before:
pp: case succ
𝕜 : 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 : ℕ∞ω
s : Set E
hs : UniqueDiffOn 𝕜 s
c : E → F →L[𝕜] G
hc : ContDiffOn 𝕜 n c s
u : F
i : ℕ
ih :
  ↑i ≤ n →
    ∀ {x : E},
      x ∈ s →
        ∀ {m : Fin i → E}, (iteratedFDerivWithin 𝕜 i (fun y ↦ (c y) u) s x) m = ((iteratedFDerivWithin 𝕜 i c s x) m) u
x : E
hx : x ∈ s
m : Fin (i + 1) → E
hi : ↑i < n
h_deriv_apply : DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 i (fun y ↦ (c y) u) s) s
h_deriv : DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 i c s) s
⊢ ((iteratedFDerivWithin 𝕜 i c s x) (Fin.tail m) ∘SL fderivWithin 𝕜 (fun x ↦ u) s x +
        (fderivWithin 𝕜 (fun y ↦ (iteratedFDerivWithin 𝕜 i c s y) (Fin.tail m)) s x).flip u)
      (m 0) =
    (((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i c s) s x) (m 0)) (Fin.tail m)) u

Tactic:
rw [fderivWithin_const_apply]

Goal state after:
case succ
𝕜 : 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 : ℕ∞ω
s : Set E
hs : UniqueDiffOn 𝕜 s
c : E → F →L[𝕜] G
hc : ContDiffOn 𝕜 n c s
u : F
i : ℕ
ih :
  ↑i ≤ n →
    ∀ {x : E},
      x ∈ s →
        ∀ {m : Fin i → E}, (iteratedFDerivWithin 𝕜 i (fun y ↦ (c y) u) s x) m = ((iteratedFDerivWithin 𝕜 i c s x) m) u
x : E
hx : x ∈ s
m : Fin (i + 1) → E
hi : ↑i < n
h_deriv_apply : DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 i (fun y ↦ (c y) u) s) s
h_deriv : DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 i c s) s
⊢ ((iteratedFDerivWithin 𝕜 i c s x) (Fin.tail m) ∘SL 0 +
        (fderivWithin 𝕜 (fun y ↦ (iteratedFDerivWithin 𝕜 i c s y) (Fin.tail m)) s x).flip u)
      (m 0) =
    (((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i c s) s x) (m 0)) (Fin.tail m)) u
Module: Mathlib.Analysis.Calculus.ContDiff.Deriv

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ∞ω
f : 𝕜 → F
s : Set 𝕜
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
hn : 1 ≤ n
⊢ ContinuousOn (derivWithin f s) s

Tactic:
rw [show (1 : ℕ∞ω) = 0 + 1 from rfl] at hn

Goal state after:
𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ∞ω
f : 𝕜 → F
s : Set 𝕜
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
hn : 0 + 1 ≤ n
⊢ ContinuousOn (derivWithin f s) s
Module: Mathlib.Analysis.Calculus.ContDiff.Deriv

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ∞ω
f : 𝕜 → F
s : Set 𝕜
h : ContDiffOn 𝕜 n f s
hs : IsOpen s
hn : 1 ≤ n
⊢ ContinuousOn (deriv f) s

Tactic:
rw [show (1 : ℕ∞ω) = 0 + 1 from rfl] at hn

Goal state after:
𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ∞ω
f : 𝕜 → F
s : Set 𝕜
h : ContDiffOn 𝕜 n f s
hs : IsOpen s
hn : 0 + 1 ≤ n
⊢ ContinuousOn (deriv f) s
Module: Mathlib.Analysis.Calculus.ContDiff.Deriv

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ∞ω
f : 𝕜 → F
h : ContDiff 𝕜 n f
hn : 1 ≤ n
⊢ Continuous (deriv f)

Tactic:
rw [show (1 : ℕ∞ω) = 0 + 1 from rfl] at hn

Goal state after:
𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ∞ω
f : 𝕜 → F
h : ContDiff 𝕜 n f
hn : 0 + 1 ≤ n
⊢ Continuous (deriv f)
Module: Mathlib.Analysis.Calculus.ContDiff.Comp

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
s : Set E
f : E → F
x₀ : E
m n : ℕ∞ω
hf : ContDiffWithinAt 𝕜 n f s x₀
hs : UniqueDiffOn 𝕜 s
hmn : m + 1 ≤ n
hx₀s : x₀ ∈ s
⊢ s ⊆ (fun x ↦ x) ⁻¹' s

Tactic:
rw [preimage_id']

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

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
m n : ℕ∞ω
f : F → G
k : F → F
s : Set F
x₀ : F
hf : ContDiffWithinAt 𝕜 n f s x₀
hk : ContDiffWithinAt 𝕜 m k s x₀
hs : UniqueDiffOn 𝕜 s
hmn : m + 1 ≤ n
hx₀s : x₀ ∈ s
⊢ s ⊆ (fun x ↦ x) ⁻¹' s

Tactic:
rw [preimage_id']

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

Goal state before:
pp: case zero
𝕜 : 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
s : Set E
f : E → F
x₀ : E
n : ℕ∞ω
hf : ContDiffWithinAt 𝕜 n f s x₀
hs : UniqueDiffOn 𝕜 s
hx₀s : x₀ ∈ s
m : ℕ∞ω
hmn : m + ↑0 ≤ n
⊢ ContDiffWithinAt 𝕜 m (iteratedFDerivWithin 𝕜 0 f s) s x₀

Tactic:
simp only [CharP.cast_eq_zero, add_zero] at hmn

Goal state after:
case zero
𝕜 : 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
s : Set E
f : E → F
x₀ : E
n : ℕ∞ω
hf : ContDiffWithinAt 𝕜 n f s x₀
hs : UniqueDiffOn 𝕜 s
hx₀s : x₀ ∈ s
m : ℕ∞ω
hmn : m ≤ n
⊢ ContDiffWithinAt 𝕜 m (iteratedFDerivWithin 𝕜 0 f s) s x₀
Module: Mathlib.Analysis.Calculus.FDeriv.OfCompLeft

Goal state before:
pp: case refine_1
𝕜 : 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
g : E → F
f : F → G
h : E → G
f' : F →L[𝕜] G
h' : E →L[𝕜] G
f'symm : G →L[𝕜] F
a : E
s : Set E
t : Set F
hst : Tendsto g (𝓝[s] a) (𝓝[t] g a)
hf : HasFDerivWithinAt f f' t (g a)
hh : HasFDerivWithinAt h h' s a
hcomp : f ∘ g =ᶠ[𝓝[s] a] h
hf'symm : Function.LeftInverse ⇑f'symm ⇑f'
ha : a ∈ s
⊢ Tendsto (Prod.map g g) (𝓝[s] a ×ˢ pure a) (𝓝[t] g a ×ˢ pure (g a))

Tactic:
exact hst.prodMap (by simp)

Goal state after:
Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ ofSet univ ⋯ = OpenPartialHomeomorph.refl X

Tactic:
ext <;> simp

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
⊢ iteratedFDerivWithin 𝕜 n f s = ⇑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F) ∘ iteratedDerivWithin n f s

Tactic:
iteratedDerivWithin_eq_equiv_comp,

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
⊢ iteratedFDerivWithin 𝕜 n f s =
    ⇑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F) ∘
      ⇑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F).symm ∘ iteratedFDerivWithin 𝕜 n f s
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞ω
h : ∀ x ∈ s, ∃ u, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ ContDiffOn 𝕜 n f (s ∩ u)
⊢ ContDiffOn 𝕜 n f s

Tactic:
by
  intro x xs
  rcases h x xs with ⟨u, u_open, xu, hu⟩
  apply (contDiffWithinAt_inter _).1 (hu x ⟨xs, xu⟩)
  exact IsOpen.mem_nhds u_open xu

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
⊢ ‖iteratedFDerivWithin 𝕜 n f s x‖ = ‖iteratedDerivWithin n f s x‖

Tactic:
iteratedDerivWithin_eq_equiv_comp,

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
⊢ ‖iteratedFDerivWithin 𝕜 n f s x‖ =
    ‖(⇑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F).symm ∘ iteratedFDerivWithin 𝕜 n f s) x‖
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
n : ℕ∞ω
m : ℕ
h : ContDiffWithinAt 𝕜 n f s x
hmn : ↑m < n
hs : UniqueDiffOn 𝕜 (insert x s)
⊢ DifferentiableWithinAt 𝕜 (iteratedDerivWithin m f s) s x

Tactic:
simpa only [iteratedDerivWithin_eq_equiv_comp,
    LinearIsometryEquiv.comp_differentiableWithinAt_iff] using
    h.differentiableWithinAt_iteratedFDerivWithin hmn hs

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

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
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c✝ c : OrderedFinpartition n
i : Fin c.length
hi : i ∈ univ
j : Fin c.length
hj : j ∈ univ
hij h : i ≠ j
this : ∀ (a' : Fin (c.partSize i)) (b' : Fin (c.partSize j + 1)), (c.emb i a').succ ≠ cases 0 (succ ∘ c.emb j) b'
⊢ Disjoint
    (range (if h : i = j then (fun i ↦ cases 0 (succ ∘ c.emb j) i) ∘ Fin.cast ⋯ else succ ∘ c.emb i ∘ Fin.cast ⋯))
    (range ((fun i ↦ cases 0 (succ ∘ c.emb j) i) ∘ Fin.cast ⋯))

Tactic:
apply Set.disjoint_iff_forall_ne.2
        simp only [hij, ↓reduceDIte, mem_range, comp_apply, ne_eq, forall_exists_index,
          forall_apply_eq_imp_iff]
        intro a b
        apply this

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

Goal state before:
pp: case e'_4.inl
𝕜 : 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
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c✝ : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
i : Fin c.length
hij : i < c.index 0
A : 1 < c.partSize (c.index 0)
⊢ c.partSize (c.index 0) - 1 - 1 + 1 = c.partSize (c.index 0) - 1

Tactic:
lia

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

Goal state before:
pp: case e'_4.inr
𝕜 : 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
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c✝ : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
i j : Fin c.length
hij : i < j
hj : j ≠ c.index 0
this : ¬↑(c.emb j ⟨c.partSize j - 1, ⋯⟩) = 0
⊢ 1 ≤ ↑(c.emb j ⟨c.partSize j - 1, ⋯⟩)

Tactic:
lia

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

Goal state before:
pp: case mpr
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n✝ : ℕ∞ω
n : ℕ∞
⊢ ContDiff 𝕜 (↑n) f → ContDiffOn 𝕜 (↑n) f univ

Tactic:
rintro ⟨p, hp⟩ x _ m hm

Goal state after:
case mpr
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n✝ : ℕ∞ω
n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpTo (↑n) f p
x : E
a✝ : x ∈ univ
m : ℕ
hm : ↑m ≤ n
⊢ ∃ u ∈ 𝓝[insert x univ] x, ∃ p, HasFTaylorSeriesUpToOn (↑m) f p u
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
n✝ : ℕ
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
𝔸 : Type u_5
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedAlgebra 𝕜 𝔸
inst✝² : Module 𝔸 F
inst✝¹ : IsBoundedSMul 𝔸 F
inst✝ : IsScalarTower 𝕜 𝔸 F
n : ℕ
IH :
  ∀ {f : 𝕜 → 𝔸} {g : 𝕜 → F},
    ContDiffWithinAt 𝕜 (↑n) f s x →
      ContDiffWithinAt 𝕜 (↑n) g s x →
        iteratedDerivWithin n (f • g) s x =
          ∑ i ∈ Finset.range (n + 1), n.choose i • iteratedDerivWithin i f s x • iteratedDerivWithin (n - i) g s x
f : 𝕜 → 𝔸
g : 𝕜 → F
hf : ContDiffWithinAt 𝕜 (↑(n + 1)) f s x
hg : ContDiffWithinAt 𝕜 (↑(n + 1)) g s x
U : Set 𝕜
hU : U ∈ 𝓝[insert x s] x
H : ∀ y ∈ U, ContDiffWithinAt 𝕜 (↑(n + 1)) f s y ∧ ContDiffWithinAt 𝕜 (↑(n + 1)) g s y
⊢ ∀ i < n, 1 ≤ n - i

Tactic:
lia

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

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
i : ℕ
IH : ∀ (k : ℕ), iteratedDerivWithin k (fun x ↦ x ^ i) s x = ↑(i.descFactorial k) * x ^ (i - k)
k : ℕ
h✝ : k ≤ i
⊢ i + 1 = k + 1 + (i - k) ∨ i < k

Tactic:
lia

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
i : ℕ
IH : ∀ (k : ℕ), iteratedDerivWithin k (fun x ↦ x ^ i) s x = ↑(i.descFactorial k) * x ^ (i - k)
k : ℕ
this : (i + 1).descFactorial (k + 1) = (k + 1) * i.descFactorial k + i.descFactorial (k + 1)
hik : i ≤ k
⊢ ∀ x < k, ¬k + 1 - x = 0

Tactic:
lia

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
i : ℕ
IH : ∀ (k : ℕ), iteratedDerivWithin k (fun x ↦ x ^ i) s x = ↑(i.descFactorial k) * x ^ (i - k)
k : ℕ
this : (i + 1).descFactorial (k + 1) = (k + 1) * i.descFactorial k + i.descFactorial (k + 1)
hik : i ≤ k
⊢ ∀ x < k, ¬k + 1 - x = 1

Tactic:
lia

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
i : ℕ
IH : ∀ (k : ℕ), iteratedDerivWithin k (fun x ↦ x ^ i) s x = ↑(i.descFactorial k) * x ^ (i - k)
k : ℕ
this : (i + 1).descFactorial (k + 1) = (k + 1) * i.descFactorial k + i.descFactorial (k + 1)
hik : i ≤ k
⊢ k < i → i - k = i - (k + 1) + 1

Tactic:
lia

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
i : ℕ
IH : ∀ (k : ℕ), iteratedDerivWithin k (fun x ↦ x ^ i) s x = ↑(i.descFactorial k) * x ^ (i - k)
k : ℕ
this : (i + 1).descFactorial (k + 1) = (k + 1) * i.descFactorial k + i.descFactorial (k + 1)
hik : k < i
⊢ ∀ x < k, ¬k + 1 - x = 0

Tactic:
lia

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
i : ℕ
IH : ∀ (k : ℕ), iteratedDerivWithin k (fun x ↦ x ^ i) s x = ↑(i.descFactorial k) * x ^ (i - k)
k : ℕ
this : (i + 1).descFactorial (k + 1) = (k + 1) * i.descFactorial k + i.descFactorial (k + 1)
hik : k < i
⊢ ∀ x < k, ¬k + 1 - x = 1

Tactic:
lia

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
i : ℕ
IH : ∀ (k : ℕ), iteratedDerivWithin k (fun x ↦ x ^ i) s x = ↑(i.descFactorial k) * x ^ (i - k)
k : ℕ
this : (i + 1).descFactorial (k + 1) = (k + 1) * i.descFactorial k + i.descFactorial (k + 1)
hik : k < i
⊢ k < i → i - k = i - (k + 1) + 1

Tactic:
lia

Goal state after:
Module: Mathlib.Topology.Order.ExtendFrom

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst✝ : RegularSpace β
hf : ContinuousOn f (uIoo a b)
ha : Tendsto f (𝓝[uIoo a b] a) (𝓝 la)
hb : Tendsto f (𝓝[uIoo a b] b) (𝓝 lb)
hab : a ≠ b
⊢ ContinuousOn (extendFrom (uIoo a b) f) (uIcc a b)

Tactic:
obtain hab' | hba' := hab.lt_or_gt

Goal state after:
case neg.inl
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst✝ : RegularSpace β
hf : ContinuousOn f (uIoo a b)
ha : Tendsto f (𝓝[uIoo a b] a) (𝓝 la)
hb : Tendsto f (𝓝[uIoo a b] b) (𝓝 lb)
hab : a ≠ b
hab' : a < b
⊢ ContinuousOn (extendFrom (uIoo a b) f) (uIcc a b)

case neg.inr
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst✝ : RegularSpace β
hf : ContinuousOn f (uIoo a b)
ha : Tendsto f (𝓝[uIoo a b] a) (𝓝 la)
hb : Tendsto f (𝓝[uIoo a b] b) (𝓝 lb)
hab : a ≠ b
hba' : b < a
⊢ ContinuousOn (extendFrom (uIoo a b) f) (uIcc a b)
Module: Mathlib.Analysis.Calculus.ContDiff.Operations

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
n : ℕ∞ω
E' : Type u_3
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
F' : Type u_4
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕜 F'
f : E → F
g : E' → F'
x : E
y : E'
hf : ContDiffAt 𝕜 n f x
hg : ContDiffAt 𝕜 n g y
⊢ ContDiffAt 𝕜 n (Prod.map f g) (x, y)

Tactic:
by
  rw [ContDiffAt] at *
  simpa only [univ_prod_univ] using hf.prodMap hg

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.FundThmCalculus

Goal state before:
pp: X : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure X
l : Filter X
inst✝ : l.IsMeasurablyGenerated
f : X → E
b : E
h : Tendsto f (l ⊓ ae μ) (𝓝 b)
hfm : StronglyMeasurableAtFilter f l μ
hμ : μ.FiniteAtFilter l
s : ι → Set X
li : Filter ι
hs : Tendsto s li l.smallSets
m : ι → ℝ
hsμ : (fun i ↦ μ.real (s i)) =ᶠ[li] m
ε : ℝ
ε₀ : 0 < ε
⊢ ∀ᶠ (x : Set X) in l.smallSets, ‖∫ (x : X) in x, f x ∂μ - μ.real x • b‖ ≤ ε * ‖μ.real x‖

Tactic:
have : ∀ᶠ s in l.smallSets, ∀ᵐ x ∂μ, x ∈ s → f x ∈ closedBall b ε :=
    eventually_smallSets_eventually.2 (h.eventually <| closedBall_mem_nhds _ ε₀)

Goal state after:
X : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure X
l : Filter X
inst✝ : l.IsMeasurablyGenerated
f : X → E
b : E
h : Tendsto f (l ⊓ ae μ) (𝓝 b)
hfm : StronglyMeasurableAtFilter f l μ
hμ : μ.FiniteAtFilter l
s : ι → Set X
li : Filter ι
hs : Tendsto s li l.smallSets
m : ι → ℝ
hsμ : (fun i ↦ μ.real (s i)) =ᶠ[li] m
ε : ℝ
ε₀ : 0 < ε
this : ∀ᶠ (s : Set X) in l.smallSets, ∀ᵐ (x : X) ∂μ, x ∈ s → f x ∈ closedBall b ε
⊢ ∀ᶠ (x : Set X) in l.smallSets, ‖∫ (x : X) in x, f x ∂μ - μ.real x • b‖ ≤ ε * ‖μ.real x‖