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

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
g : F → G
x : E
n : ℕ∞ω
t : Set F
hg : ContDiffWithinAt 𝕜 n g t (f x)
hf : ContDiffWithinAt 𝕜 n f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hxs : x ∈ s
hst : ∀ᶠ (y : E) in 𝓝[s] x, f y ∈ t
i : ℕ
hi : ↑i ≤ n
hxt : f x ∈ t
hf_tendsto : Tendsto f (𝓝[s] x) (𝓝[t] f x)
⊢ ∃ u,
    x ∈ u ∧
      IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧
        HasFTaylorSeriesUpToOn (↑i) f (ftaylorSeriesWithin 𝕜 f s) (s ∩ u) ∧
          HasFTaylorSeriesUpToOn (↑i) g (ftaylorSeriesWithin 𝕜 g t) (f '' (s ∩ u))

Tactic:
have H₁ : ∀ᶠ u in (𝓝[s] x).smallSets,
        HasFTaylorSeriesUpToOn i f (ftaylorSeriesWithin 𝕜 f s) u :=
      hf.eventually_hasFTaylorSeriesUpToOn hs hxs hi

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
f : E → F
g : F → G
x : E
n : ℕ∞ω
t : Set F
hg : ContDiffWithinAt 𝕜 n g t (f x)
hf : ContDiffWithinAt 𝕜 n f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hxs : x ∈ s
hst : ∀ᶠ (y : E) in 𝓝[s] x, f y ∈ t
i : ℕ
hi : ↑i ≤ n
hxt : f x ∈ t
hf_tendsto : Tendsto f (𝓝[s] x) (𝓝[t] f x)
H₁ : ∀ᶠ (u : Set E) in (𝓝[s] x).smallSets, HasFTaylorSeriesUpToOn (↑i) f (ftaylorSeriesWithin 𝕜 f s) u
⊢ ∃ u,
    x ∈ u ∧
      IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧
        HasFTaylorSeriesUpToOn (↑i) f (ftaylorSeriesWithin 𝕜 f s) (s ∩ u) ∧
          HasFTaylorSeriesUpToOn (↑i) g (ftaylorSeriesWithin 𝕜 g t) (f '' (s ∩ u))
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
x : E
n : ℕ∞ω
f : E → F
g : E → G
hf : ContDiffAt 𝕜 n f x
hg : ContDiffAt 𝕜 n g x
i : ℕ
hi : ↑i ≤ n
⊢ iteratedFDeriv 𝕜 i (fun x ↦ (f x, g x)) x = (iteratedFDeriv 𝕜 i f x).prod (iteratedFDeriv 𝕜 i g x)

Tactic:
simp only [← iteratedFDerivWithin_univ]
  exact iteratedFDerivWithin_prodMk hf.contDiffWithinAt hg.contDiffWithinAt uniqueDiffOn_univ
    (Set.mem_univ _) hi

Goal state after:
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 : ℕ∞ω
t : Set E
hst : s ∈ 𝓝[t] x
h : ContDiffWithinAt 𝕜 ω f s x
⊢ ContDiffWithinAt 𝕜 ω f t x

Tactic:
obtain ⟨u, hu, p, H, H'⟩ := h
    exact ⟨u, nhdsWithin_le_of_mem (insert_mem_nhdsWithin_insert hst) hu, p, H, H'⟩

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: case empty
𝔸 : Type u_1
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra ℚ 𝔸
inst✝ : CompleteSpace 𝔸
ι : Type u_3
f : ι → 𝔸
h : (↑∅).Pairwise (Commute on f)
⊢ exp (∑ i ∈ ∅, f i) = ∅.noncommProd (fun i ↦ exp (f i)) ⋯

Tactic:
| empty =>

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
α : Type u_5
H : Type u_6
inst✝ : NormedAddCommGroup H
l : Filter α
p₁ p₂ : α → FormalMultilinearSeries 𝕜 F G
q₁ q₂ : α → FormalMultilinearSeries 𝕜 E F
f : α → H
n : ℕ
hp_bdd : ∀ k ≤ n, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖p₁ x k‖
hpf : ∀ k ≤ n, (fun a ↦ p₁ a k - p₂ a k) =O[l] f
hq₁_bdd : ∀ k ≤ n, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖q₁ x k‖
hq₂_bdd : ∀ k ≤ n, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖q₂ x k‖
hqf : ∀ k ≤ n, (fun a ↦ q₁ a k - q₂ a k) =O[l] f
⊢ (fun a ↦ ∑ x, ((p₁ a).compAlongOrderedFinpartition (q₁ a) x - (p₂ a).compAlongOrderedFinpartition (q₂ a) x)) =O[l] f

Tactic:
refine .fun_sum fun c _ ↦ ?_

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
α : Type u_5
H : Type u_6
inst✝ : NormedAddCommGroup H
l : Filter α
p₁ p₂ : α → FormalMultilinearSeries 𝕜 F G
q₁ q₂ : α → FormalMultilinearSeries 𝕜 E F
f : α → H
n : ℕ
hp_bdd : ∀ k ≤ n, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖p₁ x k‖
hpf : ∀ k ≤ n, (fun a ↦ p₁ a k - p₂ a k) =O[l] f
hq₁_bdd : ∀ k ≤ n, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖q₁ x k‖
hq₂_bdd : ∀ k ≤ n, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖q₂ x k‖
hqf : ∀ k ≤ n, (fun a ↦ q₁ a k - q₂ a k) =O[l] f
c : OrderedFinpartition n
x✝ : c ∈ Finset.univ
⊢ (fun a ↦ (p₁ a).compAlongOrderedFinpartition (q₁ a) c - (p₂ a).compAlongOrderedFinpartition (q₂ a) c) =O[l] f
Module: Mathlib.Analysis.SpecialFunctions.Exponential

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
this :
  (fun h ↦ exp x * (exp (0 + h) - exp 0 - (ContinuousLinearMap.id 𝕂 𝔸) h)) =ᶠ[𝓝 0] fun h ↦
    exp (x + h) - exp x - exp x • (ContinuousLinearMap.id 𝕂 𝔸) h
⊢ (fun h ↦ exp (x + h) - exp x - (exp x • 1) h) =o[𝓝 0] fun h ↦ h

Tactic:
refine (IsLittleO.const_mul_left ?_ _).congr' this (EventuallyEq.refl _ _)
    rw [← hasFDerivAt_iff_isLittleO_nhds_zero]
    exact hasFDerivAt_exp_zero_of_radius_pos hx.pos

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

Goal state before:
pp: case empty
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ∞ω
ι : Type u_3
f : ι → E → F
t : Set E
x : E
h : ∀ i ∈ ∅, ContDiffWithinAt 𝕜 n (fun x ↦ f i x) t x
⊢ ContDiffWithinAt 𝕜 n (fun x ↦ ∑ i ∈ ∅, f i x) t x

Tactic:
| empty =>

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

Goal state before:
pp: case empty
𝕜 : 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
ι : Type u_3
f : ι → E → F
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
h : ∀ j ∈ ∅, ContDiffWithinAt 𝕜 (↑i) (f j) s x
⊢ iteratedFDerivWithin 𝕜 i (fun x ↦ ∑ j ∈ ∅, f j x) s x = ∑ j ∈ ∅, iteratedFDerivWithin 𝕜 i (f j) s x

Tactic:
| empty =>

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
ι : Type u_3
f : ι → E → F
u : Finset ι
n : ℕ
x : E
h : ∀ j ∈ u, ContDiffAt 𝕜 (↑n) (f j) x
⊢ iteratedFDeriv 𝕜 n (∑ j ∈ u, f j) x = ∑ j ∈ u, iteratedFDeriv 𝕜 n (f j) x

Tactic:
simp only [← iteratedFDerivWithin_univ]
  apply iteratedFDerivWithin_sum_apply uniqueDiffOn_univ (Set.mem_univ x)
    (h · · |>.contDiffWithinAt)

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

Goal state before:
pp: case empty
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
ι : Type u_7
n : ℕ
x : 𝕜
f : ι → 𝕜 → F
I : Finset ι
s : Set 𝕜
hx : x ∈ s
hs : UniqueDiffOn 𝕜 s
hf : ∀ i ∈ ∅, ContDiffWithinAt 𝕜 (↑n) (f i) s x
⊢ iteratedDerivWithin n (∑ i ∈ ∅, f i) s x = ∑ i ∈ ∅, iteratedDerivWithin n (f i) s x

Tactic:
| empty =>

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
n : ℕ∞ω
𝕜' : Type u_4
inst✝¹ : NormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : E → 𝕜'
hf : ContDiff 𝕜 n f
h : ∀ (x : E), f x ≠ 0
⊢ ContDiff 𝕜 n f⁻¹

Tactic:
rw [contDiff_iff_contDiffAt]; exact fun x => hf.contDiffAt.inv (h x)

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

Goal state before:
pp: f f' : ℝ → ℝ
hf : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : ∀ (x : ℝ), 0 < f' x
x : ℝ
⊢ 0 < deriv f x

Tactic:
rw [(hf _).deriv]

Goal state after:
f f' : ℝ → ℝ
hf : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : ∀ (x : ℝ), 0 < f' x
x : ℝ
⊢ 0 < f' x
Module: Mathlib.Analysis.Calculus.Deriv.MeanValue

Goal state before:
pp: f f' : ℝ → ℝ
hf : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : 0 ≤ f'
x : ℝ
⊢ 0 ≤ deriv f x

Tactic:
rw [(hf _).deriv]

Goal state after:
f f' : ℝ → ℝ
hf : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : 0 ≤ f'
x : ℝ
⊢ 0 ≤ f' x
Module: Mathlib.Analysis.Calculus.Deriv.MeanValue

Goal state before:
pp: f f' : ℝ → ℝ
hf : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : ∀ (x : ℝ), f' x < 0
x : ℝ
⊢ deriv f x < 0

Tactic:
rw [(hf _).deriv]

Goal state after:
f f' : ℝ → ℝ
hf : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : ∀ (x : ℝ), f' x < 0
x : ℝ
⊢ f' x < 0
Module: Mathlib.Analysis.Calculus.Deriv.MeanValue

Goal state before:
pp: f f' : ℝ → ℝ
hf : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : f' ≤ 0
x : ℝ
⊢ deriv f x ≤ 0

Tactic:
rw [(hf _).deriv]

Goal state after:
f f' : ℝ → ℝ
hf : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : f' ≤ 0
x : ℝ
⊢ f' x ≤ 0
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
r ε : ℝ
L : E →L[𝕜] F
x y z : E
hy : y ∈ closedBall x (r / 2)
hz : z ∈ closedBall x (r / 2)
r' : ℝ
r'mem : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ ball x r', ∀ z ∈ ball x r', ‖f z - f y - L (z - y)‖ < ε * r
⊢ ‖f z - f y - L (z - y)‖ ≤ ε * r

Tactic:
apply le_of_lt

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
r ε : ℝ
L : E →L[𝕜] F
x y z : E
hy : y ∈ closedBall x (r / 2)
hz : z ∈ closedBall x (r / 2)
r' : ℝ
r'mem : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ ball x r', ∀ z ∈ ball x r', ‖f z - f y - L (z - y)‖ < ε * r
⊢ ‖f z - f y - L (z - y)‖ < ε * r
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✝¹ : AddCommMonoid M
inst✝ : Module R M
C₁✝ C₂✝ : ConvexCone R M
x✝ : M
C₁ C₂ : ConvexCone R M
c : R
hc : 0 < c
x : M
hx : x ∈ ↑C₁
y : M
hy : y ∈ ↑C₂
⊢ c • (fun x1 x2 ↦ x1 + x2) x y ∈ ↑C₁ + ↑C₂

Tactic:
rw [smul_add]

Goal state after:
𝕜 : 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✝¹ : AddCommMonoid M
inst✝ : Module R M
C₁✝ C₂✝ : ConvexCone R M
x✝ : M
C₁ C₂ : ConvexCone R M
c : R
hc : 0 < c
x : M
hx : x ∈ ↑C₁
y : M
hy : y ∈ ↑C₂
⊢ c • x + c • y ∈ ↑C₁ + ↑C₂
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
c : 𝕜
hc : 1 < ‖c‖
r ε : ℝ
hε : 0 < ε
hr : 0 < r
x : E
L₁ L₂ : E →L[𝕜] F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
y : E
ley : r ≤ 2 * ‖c‖ * ‖y‖
ylt : ‖y‖ < r / 2
⊢ ‖(L₁ - L₂) y‖ = ‖f (x + y) - f x - L₂ (x + y - x) - (f (x + y) - f x - L₁ (x + y - x))‖

Tactic:
by
      simp

Goal state after:
Module: Mathlib.Analysis.Convex.Cone.Extension

Goal state before:
pp: E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : PointedCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), ↑x ∈ s → 0 ≤ ↑f x
dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
hdom : f.domain ≠ ⊤
⊢ ∃ g, f < g ∧ ∀ (x : ↥g.domain), ↑x ∈ s → 0 ≤ ↑g x

Tactic:
obtain ⟨y, -, hy⟩ : ∃ y ∈ ⊤, y ∉ f.domain := SetLike.exists_of_lt (lt_top_iff_ne_top.2 hdom)

Goal state after:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : PointedCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), ↑x ∈ s → 0 ≤ ↑f x
dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
⊢ ∃ g, f < g ∧ ∀ (x : ↥g.domain), ↑x ∈ s → 0 ≤ ↑g x
Module: Mathlib.Analysis.Convex.Cone.Extension

Goal state before:
pp: E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : PointedCone ℝ E
p : E →ₗ.[ℝ] ℝ
hp_nonneg : ∀ (x : ↥p.domain), ↑x ∈ s → 0 ≤ ↑p x
hp_dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : ↥p.domain), ↑x ∈ s → 0 ≤ ↑p x}
⊢ ∀ c ⊆ S, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub

Tactic:
intro c hcs c_chain y hy

Goal state after:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : PointedCone ℝ E
p : E →ₗ.[ℝ] ℝ
hp_nonneg : ∀ (x : ↥p.domain), ↑x ∈ s → 0 ≤ ↑p x
hp_dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : ↥p.domain), ↑x ∈ s → 0 ≤ ↑p x}
c : Set (E →ₗ.[ℝ] ℝ)
hcs : c ⊆ S
c_chain : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
y : E →ₗ.[ℝ] ℝ
hy : y ∈ c
⊢ ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: case refine_2
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
a : ℝ
hs₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : Absorbent ℝ s
ha : 0 ≤ a
x : E
h : ∀ (i : ℝ), a < i → x ∈ i • s
ε : ℝ
hε : 0 < ε
⊢ gauge s x < a + ε

Tactic:
linarith [gauge_le_of_mem (by linarith) <| h (a + ε / 2) (by linarith)]

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Separation

Goal state before:
pp: case refine_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
x₀ : E
hx₀ : x₀ ∉ s
f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 ⋯
x : E
hx : x ∈ f.domain
⊢ ↑f ⟨x, hx⟩ ≤ gauge s ↑⟨x, hx⟩

Tactic:
obtain ⟨y, rfl⟩ := Submodule.mem_span_singleton.1 hx

Goal state after:
case refine_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
x₀ : E
hx₀ : x₀ ∉ s
f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 ⋯
y : ℝ
hx : y • x₀ ∈ f.domain
⊢ ↑f ⟨y • x₀, hx⟩ ≤ gauge s ↑⟨y • x₀, hx⟩
Module: Mathlib.Analysis.Convex.Gauge

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

Tactic:
rw [← gauge_ball hr]
      exact gauge_mono (absorbent_ball_zero hr') ball_subset_closedBall x

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

Goal state before:
pp: case neg
X : Type u_1
E : Type u_3
inst✝⁵ : MeasurableSpace X
μ : Measure X
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
𝕜 : Type u_8
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : X → 𝕜
c : E
hf : ¬Integrable f μ
hc : ¬c = 0
⊢ ∫ (x : X), f x • c ∂μ = 0 • c

Tactic:
integral_undef,

Goal state after:
case neg
X : Type u_1
E : Type u_3
inst✝⁵ : MeasurableSpace X
μ : Measure X
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
𝕜 : Type u_8
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : X → 𝕜
c : E
hf : ¬Integrable f μ
hc : ¬c = 0
⊢ 0 = 0 • c

case neg
X : Type u_1
E : Type u_3
inst✝⁵ : MeasurableSpace X
μ : Measure X
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
𝕜 : Type u_8
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : X → 𝕜
c : E
hf : ¬Integrable f μ
hc : ¬c = 0
⊢ ¬Integrable (fun x ↦ f x • c) μ
Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap

Goal state before:
pp: X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : Integrable g (μ.withDensity fun x ↦ ↑(f x))
u v : X → E
huv : u =ᵐ[μ.withDensity fun x ↦ ↑(f x)] v
a✝ : Integrable u (μ.withDensity fun x ↦ ↑(f x))
hu : (∫ (x : X), u x ∂μ.withDensity fun x ↦ ↑(f x)) = ∫ (x : X), f x • u x ∂μ
x : X
hx : ↑(f x) ≠ 0 → u x = v x
h'x : f x ≠ 0
⊢ ↑(f x) ≠ 0

Tactic:
simpa only [Ne, ENNReal.coe_eq_zero] using h'x

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

Goal state before:
pp: ε : Type u_3
inst✝¹ : TopologicalSpace ε
inst✝ : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
h : IntervalIntegrable f μ a b
⊢ AEStronglyMeasurable f (μ.restrict (Ι a b))

Tactic:
by_cases hab : a ≤ b

Goal state after:
case pos
ε : Type u_3
inst✝¹ : TopologicalSpace ε
inst✝ : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
h : IntervalIntegrable f μ a b
hab : a ≤ b
⊢ AEStronglyMeasurable f (μ.restrict (Ι a b))

case neg
ε : Type u_3
inst✝¹ : TopologicalSpace ε
inst✝ : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
h : IntervalIntegrable f μ a b
hab : ¬a ≤ b
⊢ AEStronglyMeasurable f (μ.restrict (Ι a b))
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

Goal state before:
pp: case refine_1
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
ca cb : E
a b : ℝ
hf : IntervalIntegrable f volume a b
hmeas_a : StronglyMeasurableAtFilter f (𝓝 a) volume
hmeas_b : StronglyMeasurableAtFilter f (𝓝 b) volume
ha : Tendsto f (𝓝 a ⊓ ae volume) (𝓝 ca)
hb : Tendsto f (𝓝 b ⊓ ae volume) (𝓝 cb)
this :
  (fun t ↦
      ((∫ (x : ℝ) in t.1.1..t.1.2, f x) - ∫ (x : ℝ) in t.2.1..t.2.2, f x) -
        ((t.1.2 - t.2.2) • cb - (t.1.1 - t.2.1) • ca)) =o[𝓝 ((a, b), a, b)]
    fun t ↦ ‖t.1.1 - t.2.1‖ + ‖t.1.2 - t.2.2‖
⊢ ∀ (x : (ℝ × ℝ) × ℝ × ℝ),
    ((∫ (x : ℝ) in x.1.1..x.1.2, f x) - ∫ (x : ℝ) in x.2.1..x.2.2, f x) -
        ((x.1.2 - x.2.2) • cb - (x.1.1 - x.2.1) • ca) =
      ((∫ (x : ℝ) in x.1.1..x.1.2, f x) - ∫ (x : ℝ) in x.2.1..x.2.2, f x) -
        ((snd ℝ ℝ ℝ).smulRight cb - (fst ℝ ℝ ℝ).smulRight ca) (x.1 - x.2)

pp: case refine_2
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
ca cb : E
a b : ℝ
hf : IntervalIntegrable f volume a b
hmeas_a : StronglyMeasurableAtFilter f (𝓝 a) volume
hmeas_b : StronglyMeasurableAtFilter f (𝓝 b) volume
ha : Tendsto f (𝓝 a ⊓ ae volume) (𝓝 ca)
hb : Tendsto f (𝓝 b ⊓ ae volume) (𝓝 cb)
this :
  (fun t ↦
      ((∫ (x : ℝ) in t.1.1..t.1.2, f x) - ∫ (x : ℝ) in t.2.1..t.2.2, f x) -
        ((t.1.2 - t.2.2) • cb - (t.1.1 - t.2.1) • ca)) =o[𝓝 ((a, b), a, b)]
    fun t ↦ ‖t.1.1 - t.2.1‖ + ‖t.1.2 - t.2.2‖
⊢ (fun t ↦ ‖t.1.1 - t.2.1‖ + ‖t.1.2 - t.2.2‖) =O[𝓝 ((a, b), a, b)] fun p ↦ p.1 - p.2

Tactic:
· simp [sub_smul]

Goal state after:
case refine_2
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
ca cb : E
a b : ℝ
hf : IntervalIntegrable f volume a b
hmeas_a : StronglyMeasurableAtFilter f (𝓝 a) volume
hmeas_b : StronglyMeasurableAtFilter f (𝓝 b) volume
ha : Tendsto f (𝓝 a ⊓ ae volume) (𝓝 ca)
hb : Tendsto f (𝓝 b ⊓ ae volume) (𝓝 cb)
this :
  (fun t ↦
      ((∫ (x : ℝ) in t.1.1..t.1.2, f x) - ∫ (x : ℝ) in t.2.1..t.2.2, f x) -
        ((t.1.2 - t.2.2) • cb - (t.1.1 - t.2.1) • ca)) =o[𝓝 ((a, b), a, b)]
    fun t ↦ ‖t.1.1 - t.2.1‖ + ‖t.1.2 - t.2.2‖
⊢ (fun t ↦ ‖t.1.1 - t.2.1‖ + ‖t.1.2 - t.2.2‖) =O[𝓝 ((a, b), a, b)] fun p ↦ p.1 - p.2
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

Goal state before:
pp: E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
f : ℝ → E
ca cb : E
la lb : Filter ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
s t : Set ℝ
inst✝¹ : FTCFilter a (𝓝[s] a) la
inst✝ : FTCFilter b (𝓝[t] b) lb
hmeas_a : StronglyMeasurableAtFilter f la volume
hmeas_b : StronglyMeasurableAtFilter f lb volume
ha : Tendsto f (la ⊓ ae volume) (𝓝 ca)
hb : Tendsto f (lb ⊓ ae volume) (𝓝 cb)
this :
  (fun t ↦
      ((∫ (x : ℝ) in t.1..t.2, f x) - ∫ (x : ℝ) in a..b, f x) - ((t.2 - b) • cb - (t.1 - a) • ca)) =o[𝓝[s] a ×ˢ 𝓝[t] b]
    fun t ↦ ‖t.1 - a‖ + ‖t.2 - b‖
⊢ HasFDerivWithinAt (fun p ↦ ∫ (x : ℝ) in p.1..p.2, f x) ((snd ℝ ℝ ℝ).smulRight cb - (fst ℝ ℝ ℝ).smulRight ca) (s ×ˢ t)
    (a, b)

Tactic:
← nhdsWithin_prod_eq

Goal state after:
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
f : ℝ → E
ca cb : E
la lb : Filter ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
s t : Set ℝ
inst✝¹ : FTCFilter a (𝓝[s] a) la
inst✝ : FTCFilter b (𝓝[t] b) lb
hmeas_a : StronglyMeasurableAtFilter f la volume
hmeas_b : StronglyMeasurableAtFilter f lb volume
ha : Tendsto f (la ⊓ ae volume) (𝓝 ca)
hb : Tendsto f (lb ⊓ ae volume) (𝓝 cb)
this :
  (fun t ↦
      ((∫ (x : ℝ) in t.1..t.2, f x) - ∫ (x : ℝ) in a..b, f x) - ((t.2 - b) • cb - (t.1 - a) • ca)) =o[𝓝[s ×ˢ t] (a, b)]
    fun t ↦ ‖t.1 - a‖ + ‖t.2 - b‖
⊢ HasFDerivWithinAt (fun p ↦ ∫ (x : ℝ) in p.1..p.2, f x) ((snd ℝ ℝ ℝ).smulRight cb - (fst ℝ ℝ ℝ).smulRight ca) (s ×ˢ t)
    (a, b)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

Goal state before:
pp: case refine_1
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
f : ℝ → E
ca cb : E
la lb : Filter ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
s t : Set ℝ
inst✝¹ : FTCFilter a (𝓝[s] a) la
inst✝ : FTCFilter b (𝓝[t] b) lb
hmeas_a : StronglyMeasurableAtFilter f la volume
hmeas_b : StronglyMeasurableAtFilter f lb volume
ha : Tendsto f (la ⊓ ae volume) (𝓝 ca)
hb : Tendsto f (lb ⊓ ae volume) (𝓝 cb)
this :
  (fun t ↦
      ((∫ (x : ℝ) in t.1..t.2, f x) - ∫ (x : ℝ) in a..b, f x) - ((t.2 - b) • cb - (t.1 - a) • ca)) =o[𝓝[s ×ˢ t] (a, b)]
    fun t ↦ ‖t.1 - a‖ + ‖t.2 - b‖
⊢ ∀ (x : ℝ × ℝ),
    ((∫ (x : ℝ) in x.1..x.2, f x) - ∫ (x : ℝ) in a..b, f x) - ((x.2 - b) • cb - (x.1 - a) • ca) =
      ((∫ (x : ℝ) in x.1..x.2, f x) - ∫ (x : ℝ) in (a, b).1..(a, b).2, f x) -
        ((snd ℝ ℝ ℝ).smulRight cb - (fst ℝ ℝ ℝ).smulRight ca) (x - (a, b))

pp: case refine_2
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
f : ℝ → E
ca cb : E
la lb : Filter ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
s t : Set ℝ
inst✝¹ : FTCFilter a (𝓝[s] a) la
inst✝ : FTCFilter b (𝓝[t] b) lb
hmeas_a : StronglyMeasurableAtFilter f la volume
hmeas_b : StronglyMeasurableAtFilter f lb volume
ha : Tendsto f (la ⊓ ae volume) (𝓝 ca)
hb : Tendsto f (lb ⊓ ae volume) (𝓝 cb)
this :
  (fun t ↦
      ((∫ (x : ℝ) in t.1..t.2, f x) - ∫ (x : ℝ) in a..b, f x) - ((t.2 - b) • cb - (t.1 - a) • ca)) =o[𝓝[s ×ˢ t] (a, b)]
    fun t ↦ ‖t.1 - a‖ + ‖t.2 - b‖
⊢ (fun t ↦ ‖t.1 - a‖ + ‖t.2 - b‖) =O[𝓝[s ×ˢ t] (a, b)] fun x' ↦ x' - (a, b)

Tactic:
· simp [sub_smul]

Goal state after:
case refine_2
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
f : ℝ → E
ca cb : E
la lb : Filter ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
s t : Set ℝ
inst✝¹ : FTCFilter a (𝓝[s] a) la
inst✝ : FTCFilter b (𝓝[t] b) lb
hmeas_a : StronglyMeasurableAtFilter f la volume
hmeas_b : StronglyMeasurableAtFilter f lb volume
ha : Tendsto f (la ⊓ ae volume) (𝓝 ca)
hb : Tendsto f (lb ⊓ ae volume) (𝓝 cb)
this :
  (fun t ↦
      ((∫ (x : ℝ) in t.1..t.2, f x) - ∫ (x : ℝ) in a..b, f x) - ((t.2 - b) • cb - (t.1 - a) • ca)) =o[𝓝[s ×ˢ t] (a, b)]
    fun t ↦ ‖t.1 - a‖ + ‖t.2 - b‖
⊢ (fun t ↦ ‖t.1 - a‖ + ‖t.2 - b‖) =O[𝓝[s ×ˢ t] (a, b)] fun x' ↦ x' - (a, b)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
g : ℝ → ℝ
h : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖f t‖ ≤ g t
hbound : IntervalIntegrable g μ a b
⊢ ‖∫ (t : ℝ) in a..b, f t ∂μ‖ ≤ |∫ (t : ℝ) in a..b, g t ∂μ|

Tactic:
rw [norm_intervalIntegral_eq, abs_intervalIntegral_eq]
  exact (norm_integral_le_of_norm_le hbound.def' h).trans (le_abs_self _)

Goal state after: