mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.LocallyConvex.SeparatingDual

Goal state before:
pp: case mpr
R : Type u_1
V : Type u_2
inst✝⁹ : Field R
inst✝⁸ : AddCommGroup V
inst✝⁷ : TopologicalSpace R
inst✝⁶ : TopologicalSpace V
inst✝⁵ : IsTopologicalRing R
inst✝⁴ : Module R V
inst✝³ : SeparatingDual R V
W : Type u_3
inst✝² : AddCommGroup W
inst✝¹ : Module R W
inst✝ : FiniteDimensional R W
f : W →ₗ[R] V
hf : Injective ⇑f
this : Injective ⇑((ContinuousLinearMap.coeLM R).flip ∘ₗ f)
⊢ Surjective (⇑f.dualMap ∘ ContinuousLinearMap.toLinearMap)

Tactic:
exact LinearMap.flip_surjective_iff₁.mpr this

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

Goal state before:
pp: case inr.inl
R : Type u_1
V : Type u_2
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup V
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalRing R
inst✝¹ : Module R V
inst✝ : SeparatingDual R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
u : StrongDual R V
ux : u x = 1
uy : u y = 0
v : StrongDual R V
vy : v y = 1
vx : v x ≠ 0
⊢ ∃ f, f x = 1 ∧ f y ≠ 0

pp: case inr.inr
R : Type u_1
V : Type u_2
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup V
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalRing R
inst✝¹ : Module R V
inst✝ : SeparatingDual R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
u : StrongDual R V
ux : u x = 1
uy : u y = 0
v : StrongDual R V
vy : v y = 1
vx : v x = 0
⊢ ∃ f, f x = 1 ∧ f y ≠ 0

Tactic:
· exact ⟨(v x)⁻¹ • v, inv_mul_cancel₀ vx, show (v x)⁻¹ * v y ≠ 0 by simp [vx, vy]⟩

Goal state after:
case inr.inr
R : Type u_1
V : Type u_2
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup V
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalRing R
inst✝¹ : Module R V
inst✝ : SeparatingDual R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
u : StrongDual R V
ux : u x = 1
uy : u y = 0
v : StrongDual R V
vy : v y = 1
vx : v x = 0
⊢ ∃ f, f x = 1 ∧ f y ≠ 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
K : Set (E →L[𝕜] F)
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
c : 𝕜
hc : 1 < ‖c‖
x : E
hx : x ∈ D f K
n : ℕ → ℕ
L : ℕ → ℕ → ℕ → E →L[𝕜] F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
M :
  ∀ (e p q e' p' q' : ℕ),
    n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e
L0 : ℕ → E →L[𝕜] F := fun e ↦ L e (n e) (n e)
this : CauchySeq L0
f' : E →L[𝕜] F
f'K : f' ∈ K
hf' : Tendsto L0 atTop (𝓝 f')
Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e
ε : ℝ
εpos : 0 < ε
pos : 0 < 4 + 12 * ‖c‖
e : ℕ
he : (1 / 2) ^ e < ε / (4 + 12 * ‖c‖)
y : E
hy : y ∈ ball 0 ((1 / 2) ^ (n e + 1))
y_pos : ¬y = 0
yzero : 0 < ‖y‖
y_lt : ‖y‖ < (1 / 2) ^ (n e + 1)
yone : ‖y‖ ≤ 1
k : ℕ
k_gt : n e < k
m : ℕ := k - 1
h'k : ‖y‖ ≤ (1 / 2) ^ (m + 1)
hk : (1 / 2) ^ (m + 1 + 1) < ‖y‖
m_ge : n e ≤ m
km : k = m + 1
J1 : ‖f (x + y) - f x - (L e (n e) m) (x + y - x)‖ ≤ (1 / 2) ^ e * (1 / 2) ^ m
J2 : ‖f (x + y) - f x - (L e (n e) m) y‖ ≤ 4 * (1 / 2) ^ e * ‖y‖
⊢ (4 + 12 * ‖c‖) * ‖y‖ * (ε / (4 + 12 * ‖c‖)) = ε * ‖y‖

Tactic:
by field

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

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁸ : Field R
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSpace V
inst✝⁴ : IsTopologicalRing R
inst✝³ : Module R V
inst✝² : SeparatingDual R V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
G : StrongDual R V
Gx : G x = 1
Gy : G y ≠ 0
a b : V
⊢ a + b + (G a • (y - x) + G b • (y - x)) = a + G a • (y - x) + (b + G b • (y - x))

Tactic:
abel

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

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁸ : Field R
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSpace V
inst✝⁴ : IsTopologicalRing R
inst✝³ : Module R V
inst✝² : SeparatingDual R V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
G : StrongDual R V
Gx : G x = 1
Gy : G y ≠ 0
z : V
⊢ z + (G z • y - G z • x) + (G z • x - G z • y) = z

Tactic:
abel

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

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁸ : Field R
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSpace V
inst✝⁴ : IsTopologicalRing R
inst✝³ : Module R V
inst✝² : SeparatingDual R V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
G : StrongDual R V
Gx : G x = 1
Gy : G y ≠ 0
z : V
⊢ z + (((G y)⁻¹ * G z) • x - ((G y)⁻¹ * G z) • y) + (((G y)⁻¹ * G z) • y - ((G y)⁻¹ * G z) • x) = z

Tactic:
abel

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
r ε : ℝ
L : F
x : ℝ
hx : x ∈ A f L r ε
y z : ℝ
hy : y ∈ Icc x (x + r / 2)
hz : z ∈ Icc x (x + r / 2)
⊢ ‖f z - f y - (z - y) • L‖ ≤ ε * r

Tactic:
rcases hx with ⟨r', r'mem, hr'⟩

Goal state after:
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
r ε : ℝ
L : F
x y z : ℝ
hy : y ∈ Icc x (x + r / 2)
hz : z ∈ Icc x (x + r / 2)
r' : ℝ
r'mem : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ Icc x (x + r'), ∀ z ∈ Icc x (x + r'), ‖f z - f y - (z - y) • L‖ ≤ ε * r
⊢ ‖f z - f y - (z - y) • L‖ ≤ ε * r
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
ε : ℝ
hε : 0 < ε
x : ℝ
hx : DifferentiableWithinAt ℝ f (Ici x) x
this✝ : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x_1 : ℝ) in 𝓝[≥] x, ‖f x_1 - f x - (x_1 - x) • derivWithin f (Ici x) x‖ ≤ c * ‖x_1 - x‖
m : ℝ
xm : m ∈ Ioi x
hm : Ico x m ⊆ {x_1 | (fun x_2 ↦ ‖f x_2 - f x - (x_2 - x) • derivWithin f (Ici x) x‖ ≤ ε / 2 * ‖x_2 - x‖) x_1}
r : ℝ
hr : r ∈ Ioo 0 (m - x)
this : r ∈ Ioc (r / 2) r
y : ℝ
hy : y ∈ Icc x (x + r)
z : ℝ
hz : z ∈ Icc x (x + r)
⊢ f z - f y - (z • derivWithin f (Ici x) x - y • derivWithin f (Ici x) x) =
    f z - f x - (z • derivWithin f (Ici x) x - x • derivWithin f (Ici x) x) -
      (f y - f x - (y • derivWithin f (Ici x) x - x • derivWithin f (Ici x) x))

Tactic:
abel

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
x : ℝ
hx : x ∈ D f K
n : ℕ → ℕ
L : ℕ → ℕ → ℕ → F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
e p q e' p' q' : ℕ
hp : n e ≤ p
hq : n e ≤ q
hp' : n e' ≤ p'
hq' : n e' ≤ q'
he' : e ≤ e'
r : ℕ := max (n e) (n e')
I : (1 / 2) ^ e' ≤ (1 / 2) ^ e
J1 : ‖L e p q - L e p r‖ ≤ 4 * (1 / 2) ^ e
J2 : ‖L e p r - L e' p' r‖ ≤ 4 * (1 / 2) ^ e
J3 : ‖L e' p' r - L e' p' q'‖ ≤ 4 * (1 / 2) ^ e
⊢ L e p q - L e' p' q' = L e p q - L e p r + (L e p r - L e' p' r) + (L e' p' r - L e' p' q')

Tactic:
abel

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

Goal state before:
pp: X : Type u_1
E : Type u_3
inst✝⁷ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace ℝ E
ι : Type u_8
inst✝² : Fintype ι
M : ι → Type u_9
inst✝¹ : (i : ι) → NormedAddCommGroup (M i)
inst✝ : (i : ι) → NormedSpace 𝕜 (M i)
φ : X → ContinuousMultilinearMap 𝕜 M E
φ_int : Integrable φ μ
m : (i : ι) → M i
⊢ (∫ (x : X), φ x ∂μ) m = ∫ (x : X), (φ x) m ∂μ

Tactic:
by
  by_cases hE : CompleteSpace E
  · exact ((ContinuousMultilinearMap.apply 𝕜 M E m).integral_comp_comm φ_int).symm
  · by_cases! hm : ∀ i, m i ≠ 0
    · have : ¬ CompleteSpace (ContinuousMultilinearMap 𝕜 M E) := by
        rwa [SeparatingDual.completeSpace_continuousMultilinearMap_iff _ _ hm]
      simp [integral, hE, this]
    · rcases hm with ⟨i, hi⟩
      simp [ContinuousMultilinearMap.map_coord_zero _ i hi]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: α : Type u_1
G : Type u_3
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
l : Filter ι
inst✝¹ : l.IsCountablyGenerated
F : ι → α → G
inst✝ : IsFiniteMeasure μ
f : α → G
h_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (F n) μ
h_bound : ∃ C, ∀ᶠ (n : ι) in l, ∀ᵐ (ω : α) ∂μ, ‖F n ω‖ ≤ C
h_lim : ∀ᵐ (ω : α) ∂μ, Tendsto (fun n ↦ F n ω) l (𝓝 (f ω))
⊢ Tendsto (fun n ↦ setToFun μ (weightedSMul μ) ⋯ (F n)) l (𝓝 (setToFun μ (weightedSMul μ) ⋯ f))

Tactic:
exact tendsto_setToFun_filter_of_norm_le_const _ h_meas h_bound h_lim

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

Goal state before:
pp: case pos.refine_3
ι : Type u_1
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : ℝ → E
c : E
l l' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst✝¹ : l'.IsMeasurablyGenerated
inst✝ : TendstoIxxClass Ioc l l'
hfm : StronglyMeasurableAtFilter f l' μ
hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)
hl : μ.FiniteAtFilter l'
hu : Tendsto u lt l
hv : Tendsto v lt l
hE : CompleteSpace E
A :
  (fun i ↦ ∫ (x : ℝ) in Ioc (u i) (v i), f x ∂μ - μ.real (Ioc (u i) (v i)) • c) =o[lt] fun i ↦ μ.real (Ioc (u i) (v i))
B :
  (fun i ↦ ∫ (x : ℝ) in Ioc (v i) (u i), f x ∂μ - μ.real (Ioc (v i) (u i)) • c) =o[lt] fun i ↦ μ.real (Ioc (v i) (u i))
t : ι
⊢ ∫ (x : ℝ) in Ioc (u t) (v t), f x ∂μ - μ.real (Ioc (u t) (v t)) • c -
      (∫ (x : ℝ) in Ioc (v t) (u t), f x ∂μ - μ.real (Ioc (v t) (u t)) • c) =
    ∫ (x : ℝ) in Ioc (u t) (v t), f x ∂μ - ∫ (x : ℝ) in Ioc (v t) (u t), f x ∂μ -
      (μ.real (Ioc (u t) (v t)) • c - μ.real (Ioc (v t) (u t)) • c)

Tactic:
abel

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

Goal state before:
pp: ι : Type u_1
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
ca cb : E
la la' lb lb' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
ua va ub vb : ι → ℝ
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : FTCFilter a la la'
inst✝ : FTCFilter b lb lb'
hab : IntervalIntegrable f μ a b
hmeas_a : StronglyMeasurableAtFilter f la' μ
hmeas_b : StronglyMeasurableAtFilter f lb' μ
ha_lim : Tendsto f (la' ⊓ ae μ) (𝓝 ca)
hb_lim : Tendsto f (lb' ⊓ ae μ) (𝓝 cb)
hua : Tendsto ua lt la
hva : Tendsto va lt la
hub : Tendsto ub lt lb
hvb : Tendsto vb lt lb
this✝ : la'.IsMeasurablyGenerated
this : lb'.IsMeasurablyGenerated
A : ∀ᶠ (t : ι) in lt, IntervalIntegrable f μ (ua t) (va t)
A' : ∀ᶠ (t : ι) in lt, IntervalIntegrable f μ a (ua t)
B : ∀ᶠ (t : ι) in lt, IntervalIntegrable f μ (ub t) (vb t)
B' : ∀ᶠ (t : ι) in lt, IntervalIntegrable f μ b (ub t)
a✝ : ι
ua_va : IntervalIntegrable f μ (ua a✝) (va a✝)
a_ua : IntervalIntegrable f μ a (ua a✝)
⊢ IntervalIntegrable f μ (ub a✝) (vb a✝) →
    IntervalIntegrable f μ b (ub a✝) →
      -(∫ (x : ℝ) in ua a✝..va a✝, f x ∂μ - ∫ (x : ℝ) in ua a✝..va a✝, ca ∂μ) +
          (∫ (x : ℝ) in ub a✝..vb a✝, f x ∂μ - ∫ (x : ℝ) in ub a✝..vb a✝, cb ∂μ) =
        ∫ (x : ℝ) in va a✝..vb a✝, f x ∂μ - ∫ (x : ℝ) in ua a✝..ub a✝, f x ∂μ -
          (∫ (x : ℝ) in ub a✝..vb a✝, cb ∂μ - ∫ (x : ℝ) in ua a✝..va a✝, ca ∂μ)

Tactic:
ub_vb

Goal state after:
ι : Type u_1
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
ca cb : E
la la' lb lb' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
ua va ub vb : ι → ℝ
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : FTCFilter a la la'
inst✝ : FTCFilter b lb lb'
hab : IntervalIntegrable f μ a b
hmeas_a : StronglyMeasurableAtFilter f la' μ
hmeas_b : StronglyMeasurableAtFilter f lb' μ
ha_lim : Tendsto f (la' ⊓ ae μ) (𝓝 ca)
hb_lim : Tendsto f (lb' ⊓ ae μ) (𝓝 cb)
hua : Tendsto ua lt la
hva : Tendsto va lt la
hub : Tendsto ub lt lb
hvb : Tendsto vb lt lb
this✝ : la'.IsMeasurablyGenerated
this : lb'.IsMeasurablyGenerated
A : ∀ᶠ (t : ι) in lt, IntervalIntegrable f μ (ua t) (va t)
A' : ∀ᶠ (t : ι) in lt, IntervalIntegrable f μ a (ua t)
B : ∀ᶠ (t : ι) in lt, IntervalIntegrable f μ (ub t) (vb t)
B' : ∀ᶠ (t : ι) in lt, IntervalIntegrable f μ b (ub t)
a✝ : ι
ua_va : IntervalIntegrable f μ (ua a✝) (va a✝)
a_ua : IntervalIntegrable f μ a (ua a✝)
ub_vb : IntervalIntegrable f μ (ub a✝) (vb a✝)
⊢ IntervalIntegrable f μ b (ub a✝) →
    -(∫ (x : ℝ) in ua a✝..va a✝, f x ∂μ - ∫ (x : ℝ) in ua a✝..va a✝, ca ∂μ) +
        (∫ (x : ℝ) in ub a✝..vb a✝, f x ∂μ - ∫ (x : ℝ) in ub a✝..vb a✝, cb ∂μ) =
      ∫ (x : ℝ) in va a✝..vb a✝, f x ∂μ - ∫ (x : ℝ) in ua a✝..ub a✝, f x ∂μ -
        (∫ (x : ℝ) in ub a✝..vb a✝, cb ∂μ - ∫ (x : ℝ) in ua a✝..va a✝, ca ∂μ)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

Goal state before:
pp: ι : Type u_1
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
ca cb : E
la la' lb lb' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
ua va ub vb : ι → ℝ
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : FTCFilter a la la'
inst✝ : FTCFilter b lb lb'
hab : IntervalIntegrable f μ a b
hmeas_a : StronglyMeasurableAtFilter f la' μ
hmeas_b : StronglyMeasurableAtFilter f lb' μ
ha_lim : Tendsto f (la' ⊓ ae μ) (𝓝 ca)
hb_lim : Tendsto f (lb' ⊓ ae μ) (𝓝 cb)
hua : Tendsto ua lt la
hva : Tendsto va lt la
hub : Tendsto ub lt lb
hvb : Tendsto vb lt lb
this✝ : la'.IsMeasurablyGenerated
this : lb'.IsMeasurablyGenerated
A : ∀ᶠ (t : ι) in lt, IntervalIntegrable f μ (ua t) (va t)
A' : ∀ᶠ (t : ι) in lt, IntervalIntegrable f μ a (ua t)
B : ∀ᶠ (t : ι) in lt, IntervalIntegrable f μ (ub t) (vb t)
B' : ∀ᶠ (t : ι) in lt, IntervalIntegrable f μ b (ub t)
a✝ : ι
ua_va : IntervalIntegrable f μ (ua a✝) (va a✝)
a_ua : IntervalIntegrable f μ a (ua a✝)
ub_vb : IntervalIntegrable f μ (ub a✝) (vb a✝)
b_ub : IntervalIntegrable f μ b (ub a✝)
⊢ -(∫ (x : ℝ) in ua a✝..va a✝, f x ∂μ - ∫ (x : ℝ) in ua a✝..va a✝, ca ∂μ) +
      (∫ (x : ℝ) in ub a✝..vb a✝, f x ∂μ - ∫ (x : ℝ) in ub a✝..vb a✝, cb ∂μ) =
    ∫ (x : ℝ) in ub a✝..vb a✝, f x ∂μ - ∫ (x : ℝ) in ua a✝..va a✝, f x ∂μ -
      (∫ (x : ℝ) in ub a✝..vb a✝, cb ∂μ - ∫ (x : ℝ) in ua a✝..va a✝, ca ∂μ)

Tactic:
abel

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

Goal state before:
pp: E : Type u_5
inst✝ : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
ht : ‖f (min 0 t)‖ₑ ≠ ∞
⊢ IntervalIntegrable f volume 0 t

Tactic:
by
  rcases lt_trichotomy t 0 with h | h | h
  · rw [IntervalIntegrable.iff_comp_neg ht]
    conv => arg 1; intro t; rw [← h₁f]
    simp [h₂f (-t) (by simp [h])]
  · rw [h]
  · exact h₂f t h

Goal state after:
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:
norm_intervalIntegral_eq,

Goal state after:
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
⊢ ‖∫ (x : ℝ) in Ι a b, f x ∂μ‖ ≤ |∫ (t : ℝ) in a..b, g t ∂μ|
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
inst✝³ : LocallyCompactSpace E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
α : Type u_4
inst✝ : TopologicalSpace α
f : α → E → F
r s : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
L : E →L[𝕜] F
this✝ : ProperSpace E
a : α
x : E
r' : ℝ
hr :
  ∀ (y : E),
    dist y (a, x).2 < r' → ∀ (z : E), dist z (a, x).2 < r' → ‖f (a, x).1 z - f (a, x).1 y - (L z - L y)‖ < s * r
Irr' : r / 2 < r'
Ir'r : r' ≤ r
t : ℝ
hrt : r / 2 < t
htr' : t < r'
t' : ℝ
hrt' : r / 2 < t'
ht't : t' < t
b : ℝ
b_lt : b < s * r
hb : ∀ y ∈ closedBall x t, ∀ z ∈ closedBall x t, ‖f a z - f a y - (L z - L y)‖ ≤ b
ε : ℝ
εpos : 0 < ε
hε : b + 2 * ε < s * r
u : Set α
u_open : IsOpen[inst✝] u
au : a ∈ u
hu : ∀ (p : α × E), p.1 ∈ u → p.2 ∈ closedBall x t → dist (Function.uncurry f p) (Function.uncurry f (a, p.2)) < ε
this : u ×ˢ ball x (t - t') ∈ 𝓝 (a, x)
a' : α
x' : E
ha'x' : a' ∈ u ∧ dist x' x < t - t'
y : E
hy : dist y (a', x').2 < t'
z : E
hz : dist z (a', x').2 < t'
dyx : dist y x ≤ t
dzx : dist z x ≤ t
⊢ f a' z - f a' y - (L z - L y) = f a' z - f a z + (f a y - f a' y) + (f a z - f a y - (L z - L y))

Tactic:
abel

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

Goal state before:
pp: E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b C : ℝ
f : ℝ → E
h : ∀ᵐ (x : ℝ), x ∈ Ι a b → ‖f x‖ ≤ C
⊢ ‖∫ (x : ℝ) in a..b, f x‖ ≤ C * |b - a|

Tactic:
norm_integral_eq_norm_integral_uIoc

Goal state after:
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b C : ℝ
f : ℝ → E
h : ∀ᵐ (x : ℝ), x ∈ Ι a b → ‖f x‖ ≤ C
⊢ ‖∫ (x : ℝ) in Ι a b, f x ∂volume‖ ≤ C * |b - a|
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b C : ℝ
f : ℝ → E
h : ∀ᵐ (x : ℝ), x ∈ Ι a b → ‖f x‖ ≤ C
⊢ C * |b - a| = C * volume.real (Ioc (min a b) (max a b))

Tactic:
Real.volume_real_Ioc_of_le inf_le_sup,

Goal state after:
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b C : ℝ
f : ℝ → E
h : ∀ᵐ (x : ℝ), x ∈ Ι a b → ‖f x‖ ≤ C
⊢ C * |b - a| = C * (max a b - min 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 ℝ
⊢ -∫ (a : ℝ) in Ioc a b, f a ∂μ - -∫ (a : ℝ) in Ioc b a, f a ∂μ =
    -(∫ (a : ℝ) in Ioc a b, f a ∂μ - ∫ (a : ℝ) in Ioc b a, f a ∂μ)

Tactic:
abel

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

Goal state before:
pp: a b : ℝ
μ : Measure ℝ
𝕜 : Type u_8
inst✝ : RCLike 𝕜
r : 𝕜
f : ℝ → 𝕜
⊢ ∫ (x : ℝ) in a..b, f x / r ∂μ = (∫ (x : ℝ) in a..b, f x ∂μ) / r

Tactic:
by
  simpa only [div_eq_mul_inv] using integral_mul_const r⁻¹ f

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

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
L : E →L[𝕜] F
hf : IntervalIntegrable f μ a b
⊢ ∫ (x : ℝ) in a..b, L (f x) ∂μ = L (∫ (x : ℝ) in a..b, f x ∂μ)

Tactic:
simp_rw [intervalIntegral, L.integral_comp_comm hf.1, L.integral_comp_comm hf.2, L.map_sub]

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

Goal state before:
pp: E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
hc : c ≠ 0
d : ℝ
⊢ ∫ (x : ℝ) in a..b, f (d - x / c) = c • ∫ (x : ℝ) in d - b / c..d - a / c, f x

Tactic:
simpa only [div_eq_inv_mul, inv_inv] using integral_comp_sub_mul f (inv_ne_zero hc) d

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

Goal state before:
pp: g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ico a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn φ (Icc a b) volume
hφg : ∀ x ∈ Ico a b, g' x ≤ φ x
ε : ℝ
εpos : 0 < ε
G' : ℝ → EReal
f_lt_G' : ∀ (x : ℝ), ↑(φ x) < G' x
G'cont : LowerSemicontinuous G'
G'int : Integrable (fun x ↦ (G' x).toReal) (volume.restrict (Icc a b))
G'lt_top : ∀ᵐ (x : ℝ) ∂volume.restrict (Icc a b), G' x < ⊤
hG' : ∫ (x : ℝ) in Icc a b, (G' x).toReal < (∫ (x : ℝ) in Icc a b, φ x) + ε
s : Set ℝ := {t | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Icc a b
s_closed : IsClosed s
t : ℝ
ht : t ∈ {t | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Ico a b
v : ℝ
t_lt_v : v ∈ Ioi t
y : ℝ
g'_lt_y' : ↑(g' t) < ↑y
y_lt_G' : ↑y < G' t
I1 : ∀ᶠ (u : ℝ) in 𝓝[>] t, (u - t) * y ≤ ∫ (w : ℝ) in t..u, (G' w).toReal
I2 : ∀ᶠ (u : ℝ) in 𝓝[>] t, g u - g t ≤ (u - t) * y
I3 : ∀ᶠ (u : ℝ) in 𝓝[>] t, g u - g t ≤ ∫ (w : ℝ) in t..u, (G' w).toReal
I4 : ∀ᶠ (u : ℝ) in 𝓝[>] t, u ∈ Ioc t (min v b)
x : ℝ
hx : g x - g t ≤ ∫ (w : ℝ) in t..x, (G' w).toReal
h'x : x ∈ Ioc t (min v b)
⊢ g x - g a = g t - g a + (g x - g t)

Tactic:
abel

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
F : Type u_3
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
α : Type u_4
inst✝⁶ : TopologicalSpace α
inst✝⁵ : MeasurableSpace α
inst✝⁴ : OpensMeasurableSpace α
inst✝³ : CompleteSpace F
inst✝² : LocallyCompactSpace 𝕜
inst✝¹ : MeasurableSpace 𝕜
inst✝ : OpensMeasurableSpace 𝕜
h : SecondCountableTopologyEither α F
f : α → 𝕜 → F
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
this✝¹ : MeasurableSpace F := borel F
this✝ : BorelSpace F
⊢ StronglyMeasurable fun p ↦ deriv (f p.1) p.2

Tactic:
rcases h.out with hα | hF

Goal state after:
case inl
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
F : Type u_3
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
α : Type u_4
inst✝⁶ : TopologicalSpace α
inst✝⁵ : MeasurableSpace α
inst✝⁴ : OpensMeasurableSpace α
inst✝³ : CompleteSpace F
inst✝² : LocallyCompactSpace 𝕜
inst✝¹ : MeasurableSpace 𝕜
inst✝ : OpensMeasurableSpace 𝕜
h : SecondCountableTopologyEither α F
f : α → 𝕜 → F
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
this✝¹ : MeasurableSpace F := borel F
this✝ : BorelSpace F
hα : SecondCountableTopology α
⊢ StronglyMeasurable fun p ↦ deriv (f p.1) p.2

case inr
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
F : Type u_3
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
α : Type u_4
inst✝⁶ : TopologicalSpace α
inst✝⁵ : MeasurableSpace α
inst✝⁴ : OpensMeasurableSpace α
inst✝³ : CompleteSpace F
inst✝² : LocallyCompactSpace 𝕜
inst✝¹ : MeasurableSpace 𝕜
inst✝ : OpensMeasurableSpace 𝕜
h : SecondCountableTopologyEither α F
f : α → 𝕜 → F
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
this✝¹ : MeasurableSpace F := borel F
this✝ : BorelSpace F
hF : SecondCountableTopology F
⊢ StronglyMeasurable fun p ↦ deriv (f p.1) p.2
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

Goal state before:
pp: case e'_3
g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn φ (Icc a b) volume
hφg : ∀ x ∈ Ioo a b, φ x ≤ g' x
⊢ -(g b - g a) = -g b - -g a

Tactic:
abel

Goal state after:
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace X
μ : Measure ℝ
inst✝¹ : NullSingletonClass μ
inst✝ : IsLocallyFiniteMeasure μ
f : X → ℝ → E
a₀ : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
q : X
b₀ ε : ℝ
εpos : ε > 0
a : ℝ
a_lt : a < a₀ ∧ a < b₀
b : ℝ
lt_b : a₀ < b ∧ b₀ < b
this✝ : IsCompact ({q} ×ˢ Icc a b)
M : ℝ
hM : M ∈ upperBounds ((fun x ↦ ‖Function.uncurry f x‖) '' {q} ×ˢ Icc a b)
δ : ℝ
δpos : 0 < δ
hδ : δ < 1
h'δ : Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b
h''δ : (M + 1) * μ.real (Icc (b₀ - δ) (b₀ + δ)) + δ * μ.real (Icc a b) < ε
v : Set X
v_mem : v ∈ 𝓝[univ] q
this : v ×ˢ Ioo (b₀ - δ) (b₀ + δ) ∈ 𝓝 (q, b₀)
p : X
s : ℝ
hp : p ∈ v
hs : s ∈ Ioo (b₀ - δ) (b₀ + δ)
hv : ∀ p ∈ v, ∀ x ∈ Icc a b, ‖f p x - f q x‖ < δ
J : ∀ (r : X) (u v : ℝ), IntervalIntegrable (f r) μ u v
⊢ ∫ (t : ℝ) in a₀..s, f p t ∂μ - ∫ (t : ℝ) in a₀..b₀, f q t ∂μ =
    ∫ (t : ℝ) in a₀..s, f p t ∂μ - ∫ (t : ℝ) in a₀..b₀, f p t ∂μ +
      (∫ (t : ℝ) in a₀..b₀, f p t ∂μ - ∫ (t : ℝ) in a₀..b₀, f q t ∂μ)

Tactic:
abel

Goal state after: