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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
r : ℝ≥0∞
h : HasFPowerSeriesOnBall f p x r
inst✝¹ : CompleteSpace F
inst✝ : CharZero 𝕜
y : E
hy : y ∈ Metric.eball 0 r
n : ℕ
⊢ (n ! • (↑n !)⁻¹ • (p n) fun x ↦ y) = (p n) fun x ↦ y

Tactic:
← smul_assoc,

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
r : ℝ≥0∞
h : HasFPowerSeriesOnBall f p x r
inst✝¹ : CompleteSpace F
inst✝ : CharZero 𝕜
y : E
hy : y ∈ Metric.eball 0 r
n : ℕ
⊢ ((n ! • (↑n !)⁻¹) • (p n) fun x ↦ y) = (p n) fun x ↦ y
Module: Mathlib.Analysis.Calculus.Deriv.ZPow

Goal state before:
pp: 𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
k : ℕ
x : 𝕜
⊢ (∏ i ∈ Finset.range k, (-1 - ↑i)) * x ^ (-1 - ↑k) = (-1) ^ k * ↑k ! * x ^ (-1 - ↑k)

Tactic:
by
    simp only [← neg_add', Finset.prod_neg, ← Finset.prod_Ico_id_eq_factorial,
      Finset.prod_Ico_eq_prod_range]
    simp

Goal state after:
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
x : E
n : ℕ∞ω
f : E → F
g : F →L[𝕜] G
hf : ContDiffWithinAt 𝕜 n f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
i : ℕ
hi : ↑i ≤ n
U : Set E
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hxU : x ∈ U
hfU : ContDiffOn 𝕜 (↑i) f (insert x s ∩ U)
⊢ iteratedFDerivWithin 𝕜 i (⇑g ∘ f) (s ∩ U) x = g.compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 i f s x)

Tactic:
← iteratedFDerivWithin_inter_open (f := f) hU hxU

Goal state after:
𝕜 : 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
x : E
n : ℕ∞ω
f : E → F
g : F →L[𝕜] G
hf : ContDiffWithinAt 𝕜 n f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
i : ℕ
hi : ↑i ≤ n
U : Set E
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hxU : x ∈ U
hfU : ContDiffOn 𝕜 (↑i) f (insert x s ∩ U)
⊢ iteratedFDerivWithin 𝕜 i (⇑g ∘ f) (s ∩ U) x = g.compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 i f (s ∩ U) x)
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
x : E
n : ℕ∞ω
h : ContDiffWithinAt 𝕜 n f s x
⊢ ContinuousWithinAt f s x

Tactic:
have := h.of_le zero_le
  simp only [ContDiffWithinAt, nonpos_iff_eq_zero, Nat.cast_eq_zero, forall_eq, CharP.cast_eq_zero]
    at this
  rcases this with ⟨u, hu, p, H⟩
  rw [mem_nhdsWithin_insert] at hu
  exact (H.continuousOn.continuousWithinAt hu.1).mono_of_mem_nhdsWithin hu.2

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

Goal state before:
pp: case mp
𝕜 : 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 : ℕ∞ω
hn : n ≠ ∞
h : ContDiffOn 𝕜 (n + 1) f s
x : E
hx : x ∈ s
u : Set E
hu : u ∈ 𝓝[insert x s] x
f_an : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
hf' : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x
⊢ ∃ u ∈ 𝓝[insert x s] x,
    (n = ω → AnalyticOn 𝕜 f u) ∧ ∃ f', (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffOn 𝕜 n f' u

Tactic:
rcases Hf'.contDiffOn le_rfl (by simp [hn]) with ⟨v, vu, v'u, hv⟩

Goal state after:
case mp
𝕜 : 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 : ℕ∞ω
hn : n ≠ ∞
h : ContDiffOn 𝕜 (n + 1) f s
x : E
hx : x ∈ s
u : Set E
hu : u ∈ 𝓝[insert x s] x
f_an : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
hf' : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x
v : Set E
vu : v ∈ 𝓝[insert x u] x
v'u : v ⊆ insert x u
hv : ContDiffOn 𝕜 n f' v
⊢ ∃ u ∈ 𝓝[insert x s] x,
    (n = ω → AnalyticOn 𝕜 f u) ∧ ∃ f', (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffOn 𝕜 n f' u
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 + 1)
hi : i ∈ univ
j : Fin (c.length + 1)
hj : j ∈ univ
hij : i ≠ j
⊢ (Disjoint on fun m ↦
      range (cases (motive := fun x ↦ Fin (cons 1 c.partSize x) → Fin (n + 1)) (fun x ↦ 0) (fun m ↦ succ ∘ c.emb m) m))
    i j

Tactic:
by
    wlog! h : j < i generalizing i j
    · exact .symm
        (this j (mem_univ j) i (mem_univ i) hij.symm (lt_of_le_of_ne h hij))
    induction i using Fin.induction with
    | zero => simp at h
    | succ i =>
      induction j using Fin.induction with
      | zero =>
        simp only [onFun, cases_succ, cases_zero]
        apply Set.disjoint_iff_forall_ne.2
        simp only [mem_range, comp_apply, exists_prop', cons_zero, ne_eq, and_imp,
          Nonempty.forall, forall_const, forall_eq', forall_exists_index, forall_apply_eq_imp_iff]
        exact fun _ ↦ succ_ne_zero _
      | succ j =>
        simp only [onFun, cases_succ]
        apply Set.disjoint_iff_forall_ne.2
        simp only [mem_range, comp_apply, ne_eq, forall_exists_index, forall_apply_eq_imp_iff,
          succ_inj]
        intro a b
        apply c.emb_ne_emb_of_ne (by simpa using hij)

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

Goal state before:
pp: case fderivWithin
𝕜 : 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 : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
⊢ HasFDerivWithinAt (fun x ↦ ftaylorSeriesWithin 𝕜 f s x m) (ftaylorSeriesWithin 𝕜 f s x m.succ).curryLeft s x

Tactic:
have : (m + 1 : ℕ) ≤ n := ENat.add_one_natCast_le_withTop_of_lt hm

Goal state after:
case fderivWithin
𝕜 : 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 : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
this : ↑(m + 1) ≤ n
⊢ HasFDerivWithinAt (fun x ↦ ftaylorSeriesWithin 𝕜 f s x m) (ftaylorSeriesWithin 𝕜 f s x m.succ).curryLeft s x
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
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ ContDiffOn 𝕜 ∞ f s ↔ DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 ∞ (fderiv 𝕜 f) s

Tactic:
rw [← ENat.coe_top_add_one, contDiffOn_succ_iff_fderiv_of_isOpen hs]

Goal state after:
𝕜 : 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
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ DifferentiableOn 𝕜 f s ∧ (∞ = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 ∞ (fderiv 𝕜 f) s ↔
    DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 (∞ + 1) (fderiv 𝕜 f) s
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: case succ
𝔸 : Type u_1
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra ℚ 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
n : ℕ
ih : exp (n • x) = exp x ^ n
⊢ exp ((n + 1) • x) = exp x ^ (n + 1)

Tactic:
succ_nsmul,

Goal state after:
case succ
𝔸 : Type u_1
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra ℚ 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
n : ℕ
ih : exp (n • x) = exp x ^ n
⊢ exp (n • x + x) = exp x ^ (n + 1)
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: case succ
𝔸 : Type u_1
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra ℚ 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
n : ℕ
ih : exp (n • x) = exp x ^ n
⊢ exp (n • x) * exp x = exp x ^ n * exp x

Tactic:
ih

Goal state after:
case succ
𝔸 : Type u_1
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra ℚ 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
n : ℕ
ih : exp (n • x) = exp x ^ n
⊢ exp x ^ n * exp x = exp x ^ n * exp x
Module: Mathlib.Analysis.SpecialFunctions.Exponential

Goal state before:
pp: x : ℂ
⊢ (exp' x).lim = (fun x ↦ ∑' (n : ℕ), x ^ n / ↑n !) x

Tactic:
exact tendsto_nhds_unique x.exp'.tendsto_limit (expSeries_div_summable x).hasSum.tendsto_sum_nat

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv

Goal state before:
pp: n : ℕ
⊢ deriv^[n] cexp = cexp

Tactic:
iter_deriv_exp n

Goal state after:
n : ℕ
⊢ cexp = cexp
Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv

Goal state before:
pp: n : ℕ
⊢ deriv^[n] rexp = rexp

Tactic:
iter_deriv_exp n

Goal state after:
n : ℕ
⊢ rexp = rexp
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 : WithTop ℕ∞
g : F → G
f : E → F
hg : HasFTaylorSeriesUpToOn n g q t
hf : HasFTaylorSeriesUpToOn n f p s
h : MapsTo f s t
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
c : OrderedFinpartition m
B : (F [×c.length]→L[𝕜] G) →L[𝕜] (E [×c.partSize i]→L[𝕜] F) [×c.length]→L[𝕜] E [×m]→L[𝕜] G :=
  compAlongOrderedFinpartitionL 𝕜 E F G c
cm : ↑c.length ≤ ↑m
cp : ∀ (i : Fin c.length), ↑(c.partSize i) ≤ ↑m
⊢ HasFDerivWithinAt (fun y ↦ (B (q (f y) c.length)) fun i ↦ p y (c.partSize i))
    (∑ i, ((q (f x)).compAlongOrderedFinpartition (p x) (c.extend i)).curryLeft) s x

Tactic:
have I i : HasFDerivWithinAt (fun x ↦ p x (c.partSize i))
          (p x (c.partSize i).succ).curryLeft s x :=
        hf.fderivWithin (c.partSize i) ((cp i).trans_lt hm) x hx

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
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 : WithTop ℕ∞
g : F → G
f : E → F
hg : HasFTaylorSeriesUpToOn n g q t
hf : HasFTaylorSeriesUpToOn n f p s
h : MapsTo f s t
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
c : OrderedFinpartition m
B : (F [×c.length]→L[𝕜] G) →L[𝕜] (E [×c.partSize i]→L[𝕜] F) [×c.length]→L[𝕜] E [×m]→L[𝕜] G :=
  compAlongOrderedFinpartitionL 𝕜 E F G c
cm : ↑c.length ≤ ↑m
cp : ∀ (i : Fin c.length), ↑(c.partSize i) ≤ ↑m
I : ∀ (i : Fin c.length), HasFDerivWithinAt (fun x ↦ p x (c.partSize i)) (p x (c.partSize i).succ).curryLeft s x
⊢ HasFDerivWithinAt (fun y ↦ (B (q (f y) c.length)) fun i ↦ p y (c.partSize i))
    (∑ i, ((q (f x)).compAlongOrderedFinpartition (p x) (c.extend i)).curryLeft) s x
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
s : Set E
x : E
i : ℕ
f g : E → F
hf : ContDiffWithinAt 𝕜 (↑i) f s x
hg : ContDiffWithinAt 𝕜 (↑i) g s x
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
⊢ iteratedFDerivWithin 𝕜 i (f + g) s x = iteratedFDerivWithin 𝕜 i f s x + iteratedFDerivWithin 𝕜 i g s x

Tactic:
have := (hf.eventually (by simp)).and (hg.eventually (by simp))
  obtain ⟨t, ht, hxt, h⟩ := mem_nhdsWithin.mp this
  have hft : ContDiffOn 𝕜 i f (s ∩ t) := fun a ha ↦ (h (by simp_all)).1.mono inter_subset_left
  have hgt : ContDiffOn 𝕜 i g (s ∩ t) := fun a ha ↦ (h (by simp_all)).2.mono inter_subset_left
  have hut : UniqueDiffOn 𝕜 (s ∩ t) := hu.inter ht
  have H : ↑(s ∩ t) =ᶠ[𝓝 x] s :=
    inter_eventuallyEq_left.mpr (eventually_of_mem (ht.mem_nhds hxt) (fun _ h _ ↦ h))
  rw [← iteratedFDerivWithin_congr_set H, ← iteratedFDerivWithin_congr_set H,
    ← iteratedFDerivWithin_congr_set H]
  exact .symm (((hft.ftaylorSeriesWithin hut).add
      (hgt.ftaylorSeriesWithin hut)).eq_iteratedFDerivWithin_of_uniqueDiffOn le_rfl hut ⟨hx, hxt⟩)

Goal state after:
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 : ℕ∞ω
inst✝ : CompleteSpace E
e : E ≃L[𝕜] F
a✝ : Nontrivial E
O₁ : (E →L[𝕜] E) → F →L[𝕜] E := fun f ↦ f ∘SL ↑e.symm
O₂ : (E →L[𝕜] F) → E →L[𝕜] E := fun f ↦ ↑e.symm ∘SL f
this : inverse = O₁ ∘ Ring.inverse ∘ O₂
h₁ : ContDiff 𝕜 n O₁
⊢ ContDiffAt 𝕜 n (O₁ ∘ Ring.inverse ∘ O₂) ↑e

Tactic:
have h₂ : ContDiff 𝕜 n O₂ := contDiff_const.clm_comp contDiff_id

Goal state after:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type uF
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
n : ℕ∞ω
inst✝ : CompleteSpace E
e : E ≃L[𝕜] F
a✝ : Nontrivial E
O₁ : (E →L[𝕜] E) → F →L[𝕜] E := fun f ↦ f ∘SL ↑e.symm
O₂ : (E →L[𝕜] F) → E →L[𝕜] E := fun f ↦ ↑e.symm ∘SL f
this : inverse = O₁ ∘ Ring.inverse ∘ O₂
h₁ : ContDiff 𝕜 n O₁
h₂ : ContDiff 𝕜 n O₂
⊢ ContDiffAt 𝕜 n (O₁ ∘ Ring.inverse ∘ O₂) ↑e
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
this : (fun s ↦ ∫ (x : X) in s, f x ∂μ - μ.real s • b) =o[l.smallSets] fun s ↦ μ.real s
a : ι
ha : (fun i ↦ μ.real (s i)) a = m a
⊢ ((fun s ↦ ∫ (x : X) in s, f x ∂μ - μ.real s • b) ∘ s) a = (fun i ↦ ∫ (x : X) in s i, f x ∂μ - m i • b) a

Tactic:
dsimp only [Function.comp_apply] at ha ⊢

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
this : (fun s ↦ ∫ (x : X) in s, f x ∂μ - μ.real s • b) =o[l.smallSets] fun s ↦ μ.real s
a : ι
ha : μ.real (s a) = m a
⊢ ∫ (x : X) in s a, f x ∂μ - μ.real (s a) • b = ∫ (x : X) in s a, f x ∂μ - m a • b
Module: Mathlib.Analysis.Calculus.Deriv.MeanValue

Goal state before:
pp: D : Set ℝ
hD : Convex ℝ D
f f' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'₀ : ∀ x ∈ interior D, 0 < f' x
x : ℝ
hx : x ∈ interior D
⊢ 0 < deriv f x

Tactic:
deriv_eqOn isOpen_interior hf' hx

Goal state after:
D : Set ℝ
hD : Convex ℝ D
f f' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'₀ : ∀ x ∈ interior D, 0 < f' x
x : ℝ
hx : x ∈ interior D
⊢ 0 < f' x
Module: Mathlib.Analysis.Calculus.Deriv.MeanValue

Goal state before:
pp: D : Set ℝ
hD : Convex ℝ D
f f' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'₀ : ∀ x ∈ interior D, 0 ≤ f' x
x : ℝ
hx : x ∈ interior D
⊢ 0 ≤ deriv f x

Tactic:
deriv_eqOn isOpen_interior hf' hx

Goal state after:
D : Set ℝ
hD : Convex ℝ D
f f' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'₀ : ∀ x ∈ interior D, 0 ≤ f' x
x : ℝ
hx : x ∈ interior D
⊢ 0 ≤ f' x
Module: Mathlib.Analysis.Calculus.Deriv.MeanValue

Goal state before:
pp: D : Set ℝ
hD : Convex ℝ D
f f' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'₀ : ∀ x ∈ interior D, f' x < 0
x : ℝ
hx : x ∈ interior D
⊢ deriv f x < 0

Tactic:
deriv_eqOn isOpen_interior hf' hx

Goal state after:
D : Set ℝ
hD : Convex ℝ D
f f' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'₀ : ∀ x ∈ interior D, f' x < 0
x : ℝ
hx : x ∈ interior D
⊢ f' x < 0
Module: Mathlib.Analysis.Calculus.Deriv.MeanValue

Goal state before:
pp: D : Set ℝ
hD : Convex ℝ D
f f' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'₀ : ∀ x ∈ interior D, f' x ≤ 0
x : ℝ
hx : x ∈ interior D
⊢ deriv f x ≤ 0

Tactic:
deriv_eqOn isOpen_interior hf' hx

Goal state after:
D : Set ℝ
hD : Convex ℝ D
f f' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'₀ : ∀ x ∈ interior D, f' x ≤ 0
x : ℝ
hx : x ∈ interior D
⊢ f' x ≤ 0
Module: Mathlib.Geometry.Convex.Cone.Basic

Goal state before:
pp: 𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : AddCommGroup G
inst✝ : SMul R G
C✝ C₁ C₂ C : ConvexCone R G
h₁ : C.Pointed
h₂ : C.Salient
⊢ ∀ (a b : G), a ≤ b → b ≤ a → a = b

Tactic:
intro a b ab ba
      by_contra h
      have h' : b - a ≠ 0 := fun h'' => h (eq_of_sub_eq_zero h'').symm
      have H := h₂ (b - a) ab h'
      rw [neg_sub b a] at H
      exact H ba

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: x : ℝ
hx : x = 0
⊢ deriv log x = x⁻¹

Tactic:
deriv_zero_of_not_differentiableAt (differentiableAt_log_iff.not_left.2 hx),

Goal state after:
x : ℝ
hx : x = 0
⊢ 0 = x⁻¹
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

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
K : Set (E →L[𝕜] F)
x : E
hx : x ∈ {x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ K}
⊢ x ∈ ⋂ e, ⋃ n, ⋂ p, ⋂ (_ : p ≥ n), ⋂ q, ⋂ (_ : q ≥ n), B f K ((1 / 2) ^ p) ((1 / 2) ^ q) ((1 / 2) ^ e)

Tactic:
mem_iInter

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
f : E → F
K : Set (E →L[𝕜] F)
x : E
hx : x ∈ {x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ K}
⊢ ∀ (i : ℕ), x ∈ ⋃ n, ⋂ p, ⋂ (_ : p ≥ n), ⋂ q, ⋂ (_ : q ≥ n), B f K ((1 / 2) ^ p) ((1 / 2) ^ q) ((1 / 2) ^ i)
Module: Mathlib.Geometry.Convex.Cone.Basic

Goal state before:
pp: R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : LinearOrder R
inst✝³ : AddLeftStrictMono R
inst✝² : AddCommGroup M
inst✝¹ : Nontrivial M
inst✝ : Module R M
C : ConvexCone R M
h : Submodule.span R ↑C = ⊤
x : M
hne : (↑C).Nonempty
⊢ ∀ (c : R) {x : M}, x ∈ ↑C - ↑C → c • x ∈ ↑C - ↑C

Tactic:
by
      rintro r _ ⟨y, hy, z, hz, rfl⟩
      simp only [Set.mem_sub, SetLike.mem_coe]
      rcases lt_trichotomy r 0 with hr | rfl | hr
      · -- r < 0: use (-r) • z - (-r) • y = r • (y - z)
        refine ⟨(-r) • z, C.smul_mem (neg_pos.mpr hr) hz,
               (-r) • y, C.smul_mem (neg_pos.mpr hr) hy, ?_⟩
        rw [neg_smul, neg_smul, neg_sub_neg, smul_sub]
      · -- r = 0
        simp only [zero_smul]
        obtain ⟨c, hc⟩ := hne
        exact ⟨c, hc, c, hc, sub_self c⟩
      · -- r > 0: use r • y - r • z
        exact ⟨r • y, C.smul_mem hr hy, r • z, C.smul_mem hr hz, (smul_sub r y z).symm⟩

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.Pointed

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
C : PointedCone R E
r : R
x✝ : E
hx : x✝ ∈ C.support.carrier
⊢ r • x✝ ∈ C.support.carrier

Tactic:
by_cases hr : 0 ≤ r
    · simpa using And.intro (C.smul_mem hr hx.1) (C.smul_mem hr hx.2)
    · have hr := le_of_lt <| neg_pos_of_neg <| lt_of_not_ge hr
      simpa using And.intro (C.smul_mem hr hx.2) (C.smul_mem hr hx.1)

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: a : ℝ
h : 0 ≤ a
⊢ HasSum (fun k ↦ 2 * (1 / (2 * ↑k + 1)) * (a / (a + 2)) ^ (2 * k + 1)) (log (1 + a))

Tactic:
by
  obtain (rfl | ha0) := eq_or_ne a 0
  · simp [hasSum_zero]
  · convert! hasSum_log_one_add_inv (inv_pos.mpr (lt_of_le_of_ne h ha0.symm)) using 4
    all_goals simp [field, add_comm]

Goal state after:
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
x : E
a : ℝ
absorbs : Absorbent ℝ s
h : gauge s x < a
⊢ ∃ b, 0 < b ∧ b < a ∧ x ∈ b • s

Tactic:
obtain ⟨b, ⟨hb, hx⟩, hba⟩ := exists_lt_of_csInf_lt absorbs.gauge_set_nonempty h
  exact ⟨b, hb, hba, hx⟩

Goal state after:
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
x : E
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
hs : Absorbent ℝ s
hb : Bornology.IsVonNBounded ℝ s
⊢ 0 < gauge s x ↔ x ≠ 0

Tactic:
by
  simp only [(gauge_nonneg _).lt_iff_ne', Ne, gauge_eq_zero hs hb]

Goal state after:
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr✝ : 0 ≤ r
x : E
hr : 0 < r
⊢ gauge (ball 0 r) x = ‖x‖ / r

Tactic:
rw [← smul_unitBall_of_pos hr, gauge_smul_left, Pi.smul_apply, gauge_unit_ball, smul_eq_mul,
    abs_of_nonneg hr.le, div_eq_inv_mul]

Goal state after:
case inr.symmetric
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr✝ : 0 ≤ r
x : E
hr : 0 < r
⊢ ∀ x ∈ ball 0 1, -x ∈ ball 0 1
Module: Mathlib.Analysis.LocallyConvex.SeparatingDual

Goal state before:
pp: R : Type u_4
V : Type u_5
W : Type u_6
inst✝¹³ : NormedField R
inst✝¹² : AddCommGroup V
inst✝¹¹ : AddCommGroup W
inst✝¹⁰ : TopologicalSpace R
inst✝⁹ : TopologicalSpace V
inst✝⁸ : TopologicalSpace W
inst✝⁷ : IsTopologicalRing R
inst✝⁶ : Module R V
inst✝⁵ : Module R W
inst✝⁴ : SeparatingDual R V
inst✝³ : IsTopologicalAddGroup V
inst✝² : IsTopologicalAddGroup W
inst✝¹ : ContinuousSMul R V
inst✝ : ContinuousSMul R W
f g : V ≃L[R] W
⊢ (∀ (x : V →L[R] V), x ∘SL ↑g.symm = ((↑g.symm ∘SL ↑f) ∘SL x) ∘SL ↑f.symm) ↔ ∃ α, f = α • g

Tactic:
eq_comp_toContinuousLinearMap_symm,

Goal state after:
R : Type u_4
V : Type u_5
W : Type u_6
inst✝¹³ : NormedField R
inst✝¹² : AddCommGroup V
inst✝¹¹ : AddCommGroup W
inst✝¹⁰ : TopologicalSpace R
inst✝⁹ : TopologicalSpace V
inst✝⁸ : TopologicalSpace W
inst✝⁷ : IsTopologicalRing R
inst✝⁶ : Module R V
inst✝⁵ : Module R W
inst✝⁴ : SeparatingDual R V
inst✝³ : IsTopologicalAddGroup V
inst✝² : IsTopologicalAddGroup W
inst✝¹ : ContinuousSMul R V
inst✝ : ContinuousSMul R W
f g : V ≃L[R] W
⊢ (∀ (x : V →L[R] V), (x ∘SL ↑g.symm) ∘SL ↑f = (↑g.symm ∘SL ↑f) ∘SL x) ↔ ∃ α, f = α • g