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

Goal state before:
pp: case refine_4
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
s : Set E
ι : Type u_3
inst✝² : Fintype ι
F' : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
φ : (i : ι) → E → F' i
p' : (i : ι) → E → FormalMultilinearSeries 𝕜 E (F' i)
n : ℕ∞ω
pr : (i : ι) → ((i : ι) → F' i) →L[𝕜] F' i := ContinuousLinearMap.proj
L : (m : ℕ) → ((i : ι) → E [×m]→L[𝕜] F' i) ≃ₗᵢ[𝕜] E [×m]→L[𝕜] (i : ι) → F' i :=
  fun m ↦ ContinuousMultilinearMap.piₗᵢ 𝕜 fun _i ↦ E
h : ∀ (i : ι), HasFTaylorSeriesUpToOn n (φ i) (p' i) s
⊢ ∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x ↦ ContinuousMultilinearMap.pi fun i ↦ p' i x m) s

Tactic:
intro m hm
    exact (L m).continuous.comp_continuousOn <| continuousOn_pi.2 fun i => (h i).cont m hm

Goal state after:
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
L : E →L[𝕜] F
r ε : ℝ
x : E
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
s : ℝ
s_gt : r / 2 < s
s_lt : s < r'
this : s ∈ Ioc (r / 2) r
x' : E
hx' : x' ∈ ball x (r' - s)
B : ball x' s ⊆ ball x r'
⊢ ∀ y ∈ ball x' s, ∀ z ∈ ball x' s, ‖f z - f y - L (z - y)‖ < ε * r

Tactic:
intro y hy z hz

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
L : E →L[𝕜] F
r ε : ℝ
x : E
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
s : ℝ
s_gt : r / 2 < s
s_lt : s < r'
this : s ∈ Ioc (r / 2) r
x' : E
hx' : x' ∈ ball x (r' - s)
B : ball x' s ⊆ ball x r'
y : E
hy : y ∈ ball x' s
z : E
hz : z ∈ ball x' s
⊢ ‖f z - f y - L (z - y)‖ < ε * r
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
ε : ℝ
hε : 0 < ε
x : E
hx : DifferentiableAt 𝕜 f x
δ : ℝ := ε / 2 / 2
R : ℝ
R_pos : R > 0
hR : ∀ y ∈ ball x R, ‖f y - f x - (fderiv 𝕜 f x) (y - x)‖ ≤ δ * ‖y - x‖
r : ℝ
hr : r ∈ Ioo 0 R
this : r ∈ Ioc (r / 2) r
y : E
hy : y ∈ ball x r
z : E
hz : z ∈ ball x r
⊢ ε / 2 * r < ε * r

Tactic:
by gcongr; exacts [hr.1, half_lt_self hε]

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

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

Tactic:
hx,

Goal state after:
x : ℝ
hx : x = 0
⊢ 0 = 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✝¹ : AddCommMonoid M
inst✝ : Module R M
C₁✝ C₂✝ : ConvexCone R M
x : M
C₁ C₂ : ConvexCone R M
⊢ ∀ ⦃x : M⦄, x ∈ ↑C₁ + ↑C₂ → ∀ ⦃y : M⦄, y ∈ ↑C₁ + ↑C₂ → x + y ∈ ↑C₁ + ↑C₂

Tactic:
rintro _ ⟨x₁, hx₁, x₂, hx₂, rfl⟩ y ⟨y₁, hy₁, y₂, hy₂, rfl⟩
      exact ⟨x₁ + y₁, add_mem hx₁ hy₁, x₂ + y₂, add_mem hx₂ hy₂, add_add_add_comm ..⟩

Goal state after:
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
⊢ 0 ∈ ↑C - ↑C

Tactic:
obtain ⟨c, hc⟩ := hne

Goal state after:
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 c : M
hc : c ∈ ↑C
⊢ 0 ∈ ↑C - ↑C
Module: Mathlib.Geometry.Convex.Cone.Basic

Goal state before:
pp: case inr.inl
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
y : M
hy : y ∈ ↑C
z : M
hz : z ∈ ↑C
⊢ ∃ x ∈ C, ∃ y ∈ C, x - y = 0

Tactic:
obtain ⟨c, hc⟩ := hne

Goal state after:
case inr.inl
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 y : M
hy : y ∈ ↑C
z : M
hz : z ∈ ↑C
c : M
hc : c ∈ ↑C
⊢ ∃ x ∈ C, ∃ y ∈ C, x - y = 0
Module: Mathlib.Geometry.Convex.Cone.Pointed

Goal state before:
pp: case inl
R : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
C✝ C₁ C₂ : PointedCone R E
x✝¹ : E
r : R
C : ConvexCone R E
hC : C.Pointed
x✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x : E
hx : x ∈ ↑C
c : R
hc : 0 ≤ c
hzero : 0 = c
⊢ ⟨c, hc⟩ • x ∈ C

pp: case inr
R : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
C✝ C₁ C₂ : PointedCone R E
x✝¹ : E
r : R
C : ConvexCone R E
hC : C.Pointed
x✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x : E
hx : x ∈ ↑C
c : R
hc : 0 ≤ c
hpos : 0 < c
⊢ ⟨c, hc⟩ • x ∈ C

Tactic:
· unfold ConvexCone.Pointed at hC
      convert! hC
      simp [← hzero]

Goal state after:
case inr
R : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
C✝ C₁ C₂ : PointedCone R E
x✝¹ : E
r : R
C : ConvexCone R E
hC : C.Pointed
x✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x : E
hx : x ∈ ↑C
c : R
hc : 0 ≤ c
hpos : 0 < c
⊢ ⟨c, hc⟩ • x ∈ C
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✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
C✝ C₁ C₂ : PointedCone R E
x✝¹ : E
r : R
C : ConvexCone R E
hC : C.Pointed
x✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x : E
hx : x ∈ ↑C
c : R
hc : 0 ≤ c
⊢ ⟨c, hc⟩ • x ∈ ↑C

Tactic:
simp_rw [SetLike.mem_coe]
    rcases eq_or_lt_of_le hc with hzero | hpos
    · unfold ConvexCone.Pointed at hC
      convert! hC
      simp [← hzero]
    · apply ConvexCone.smul_mem
      · convert! hpos
      · exact 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
absorbs : Absorbent ℝ s
a : ℝ
x✝ : E
⊢ gauge s x✝ < a ↔ ∃ i, (0 < i ∧ i < a) ∧ x✝ ∈ i • s

Tactic:
and_assoc

Goal state after:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
absorbs : Absorbent ℝ s
a : ℝ
x✝ : E
⊢ gauge s x✝ < a ↔ ∃ i, 0 < i ∧ i < a ∧ x✝ ∈ i • s
Module: Mathlib.Analysis.RCLike.Extend

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
F : Type u_2
inst✝³ : AddCommGroup F
inst✝² : Module ℝ F
inst✝¹ : Module 𝕜 F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : Dual ℝ F
fc : F → 𝕜 := fun x ↦ ↑(fr x) - I * ↑(fr (I • x))
add : ∀ (x y : F), fc (x + y) = fc x + fc y
A : ∀ (c : ℝ) (x : F), ↑(fr (↑c • x)) = ↑c * ↑(fr x)
smul_ℝ : ∀ (c : ℝ) (x : F), fc (↑c • x) = ↑c * fc x
smul_I : ∀ (x : F), fc (I • x) = I * fc x
c : 𝕜
x : F
⊢ fc (c • x) = c • fc x

Tactic:
← re_add_im c

Goal state after:
𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
F : Type u_2
inst✝³ : AddCommGroup F
inst✝² : Module ℝ F
inst✝¹ : Module 𝕜 F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : Dual ℝ F
fc : F → 𝕜 := fun x ↦ ↑(fr x) - I * ↑(fr (I • x))
add : ∀ (x y : F), fc (x + y) = fc x + fc y
A : ∀ (c : ℝ) (x : F), ↑(fr (↑c • x)) = ↑c * ↑(fr x)
smul_ℝ : ∀ (c : ℝ) (x : F), fc (↑c • x) = ↑c * fc x
smul_I : ∀ (x : F), fc (I • x) = I * fc x
c : 𝕜
x : F
⊢ fc ((↑(re c) + ↑(im c) * I) • x) = (↑(re c) + ↑(im c) * I) • fc x
Module: Mathlib.Analysis.RCLike.Extend

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
F : Type u_2
inst✝³ : AddCommGroup F
inst✝² : Module ℝ F
inst✝¹ : Module 𝕜 F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : Dual ℝ F
x : F
⊢ re ((starRingEnd 𝕜) (fr.extendRCLike x) * fr.extendRCLike x) = fr ((starRingEnd 𝕜) (fr.extendRCLike x) • x)

Tactic:
← smul_eq_mul,

Goal state after:
𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
F : Type u_2
inst✝³ : AddCommGroup F
inst✝² : Module ℝ F
inst✝¹ : Module 𝕜 F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : Dual ℝ F
x : F
⊢ re ((starRingEnd 𝕜) (fr.extendRCLike x) • fr.extendRCLike x) = fr ((starRingEnd 𝕜) (fr.extendRCLike x) • x)
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s : Set E
inst✝² : RCLike 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsScalarTower ℝ 𝕜 E
hs : Balanced 𝕜 s
r : 𝕜
x : E
⊢ gauge s (r • x) = ‖r‖ * gauge s x

Tactic:
← smul_eq_mul,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s : Set E
inst✝² : RCLike 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsScalarTower ℝ 𝕜 E
hs : Balanced 𝕜 s
r : 𝕜
x : E
⊢ gauge s (r • x) = ‖r‖ • gauge s x
Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : μ.WeaklyRegular
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := NNReal.mk (ε / 2) ⋯
δpos : 0 < δ
⊢ ∃ g,
    (∀ (x : α), ↑(f x) < g x) ∧
      LowerSemicontinuous g ∧
        Integrable (fun x ↦ (g x).toReal) μ ∧
          (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), f x ∂μ + ε

Tactic:
let fp : α → ℝ≥0 := fun x => Real.toNNReal (f x)

Goal state after:
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : μ.WeaklyRegular
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := NNReal.mk (ε / 2) ⋯
δpos : 0 < δ
fp : α → ℝ≥0 := fun x ↦ (f x).toNNReal
⊢ ∃ g,
    (∀ (x : α), ↑(f x) < g x) ∧
      LowerSemicontinuous g ∧
        Integrable (fun x ↦ (g x).toReal) μ ∧
          (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), f x ∂μ + ε
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: case right
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
L : F
r ε x r' : ℝ
rr' : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ Icc x (x + r'), ∀ z ∈ Icc x (x + r'), ‖f z - f y - (z - y) • L‖ ≤ ε * r
s : ℝ
s_gt : r / 2 < s
s_lt : s < r'
this : s ∈ Ioc (r / 2) r
x' : ℝ
hx' : x' ∈ Ioo x (x + r' - s)
A : Icc x' (x' + s) ⊆ Icc x (x + r')
⊢ ∀ y ∈ Icc x' (x' + s), ∀ z ∈ Icc x' (x' + s), ‖f z - f y - (z - y) • L‖ ≤ ε * r

Tactic:
intro y hy z hz

Goal state after:
case right
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
L : F
r ε x r' : ℝ
rr' : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ Icc x (x + r'), ∀ z ∈ Icc x (x + r'), ‖f z - f y - (z - y) • L‖ ≤ ε * r
s : ℝ
s_gt : r / 2 < s
s_lt : s < r'
this : s ∈ Ioc (r / 2) r
x' : ℝ
hx' : x' ∈ Ioo x (x + r' - s)
A : Icc x' (x' + s) ⊆ Icc x (x + r')
y : ℝ
hy : y ∈ Icc x' (x' + s)
z : ℝ
hz : z ∈ Icc x' (x' + s)
⊢ ‖f z - f y - (z - y) • L‖ ≤ ε * r
Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap

Goal state before:
pp: case pos
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
hE : ¬CompleteSpace E
hm : ∀ (i : ι), m i ≠ 0
⊢ (∫ (x : X), φ x ∂μ) m = ∫ (x : X), (φ x) m ∂μ

pp: case neg
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
hE : ¬CompleteSpace E
hm : ∃ i, m i = 0
⊢ (∫ (x : X), φ x ∂μ) m = ∫ (x : X), (φ x) m ∂μ

Tactic:
· have : ¬ CompleteSpace (ContinuousMultilinearMap 𝕜 M E) := by
        rwa [SeparatingDual.completeSpace_continuousMultilinearMap_iff _ _ hm]
      simp [integral, hE, this]

Goal state after:
case neg
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
hE : ¬CompleteSpace E
hm : ∃ i, m i = 0
⊢ (∫ (x : X), φ x ∂μ) m = ∫ (x : X), (φ x) m ∂μ
Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap

Goal state before:
pp: X : Type u_1
inst✝¹ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
inst✝ : RCLike 𝕜
f : X → 𝕜
hf : Integrable f μ
⊢ ∫ (x : X), ↑(re (f x)) ∂μ + I * ∫ (x : X), ↑(im (f x)) ∂μ = ∫ (x : X), f x ∂μ

Tactic:
← smul_eq_mul,

Goal state after:
X : Type u_1
inst✝¹ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
inst✝ : RCLike 𝕜
f : X → 𝕜
hf : Integrable f μ
⊢ ∫ (x : X), ↑(re (f x)) ∂μ + I • ∫ (x : X), ↑(im (f x)) ∂μ = ∫ (x : X), f x ∂μ
Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap

Goal state before:
pp: case pos
X : Type u_1
inst✝⁴ : MeasurableSpace X
μ : Measure X
A : Type u_8
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace ℝ A
inst✝¹ : IsScalarTower ℝ A A
inst✝ : SMulCommClass ℝ A A
f : X → A
hf : Integrable f μ
c : A
hA : CompleteSpace A
⊢ ∫ (x : X), c * f x ∂μ = c * ∫ (x : X), f x ∂μ

Tactic:
change ∫ x, ContinuousLinearMap.mul ℝ _ c (f x) ∂μ = ContinuousLinearMap.mul ℝ _ c (∫ x, f x ∂μ)
    rw [ContinuousLinearMap.integral_comp_comm _ hf]

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

Goal state before:
pp: case pos.h_bound
ι : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : Countable ι
f : ι → C(ℝ, E)
hf_sum : Summable fun i ↦ ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ }) (f i)‖
hE : CompleteSpace E
i : ι
x : ℝ
hx : x ∈ Ι a b
⊢ ‖(f i) x‖ ≤ ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ }) (f i)‖

Tactic:
apply ContinuousMap.norm_coe_le_norm ((f i).restrict _) ⟨x, _⟩

Goal state after:
ι : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : Countable ι
f : ι → C(ℝ, E)
hf_sum : Summable fun i ↦ ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ }) (f i)‖
hE : CompleteSpace E
i : ι
x : ℝ
hx : x ∈ Ι a b
⊢ x ∈ ↑{ carrier := [[a, b]], isCompact' := ⋯ }
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: case pos.h_lim
ι : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : Countable ι
f : ι → C(ℝ, E)
hf_sum : Summable fun i ↦ ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ }) (f i)‖
hE : CompleteSpace E
⊢ ∀ᵐ (t : ℝ), t ∈ Ι a b → HasSum (fun n ↦ (f n) t) (∑' (i : ι), (f i) t)

Tactic:
· refine ae_of_all _ fun x hx => Summable.hasSum ?_
    let x : (⟨uIcc a b, isCompact_uIcc⟩ : Compacts ℝ) := ⟨x, ⟨hx.1.le, hx.2⟩⟩
    have := hf_sum.of_norm
    simpa only [Compacts.coe_mk, ContinuousMap.restrict_apply]
      using ContinuousMap.summable_apply this x

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

Goal state before:
pp: case inl
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)‖ₑ ≠ ∞
h : t < 0
⊢ IntervalIntegrable f volume 0 t

pp: case inr.inl
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)‖ₑ ≠ ∞
h : t = 0
⊢ IntervalIntegrable f volume 0 t

pp: case inr.inr
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)‖ₑ ≠ ∞
h : 0 < t
⊢ IntervalIntegrable f volume 0 t

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

Goal state after:
case inr.inl
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)‖ₑ ≠ ∞
h : t = 0
⊢ IntervalIntegrable f volume 0 t

case inr.inr
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)‖ₑ ≠ ∞
h : 0 < t
⊢ IntervalIntegrable f volume 0 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
⊢ dist z x ≤ t

Tactic:
linarith [dist_triangle z x' x]

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 : ℝ
μ : Measure ℝ
inst✝ : CompleteSpace E
c : E
⊢ ∫ (x : ℝ) in a..b, c ∂μ = (μ.real (Ioc a b) - μ.real (Ioc b a)) • c

Tactic:
by
  simp only [measureReal_def, intervalIntegral, setIntegral_const, sub_smul]

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
g'_lt_y : g' t < y
u : ℝ
hu : slope g t u < y
t_lt_u : u ∈ Ioi t
this : (u - t) * slope g t u ≤ (u - t) * y
⊢ g u - g t ≤ (u - t) * y

Tactic:
← smul_eq_mul,

Goal state after:
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
g'_lt_y : g' t < y
u : ℝ
hu : slope g t u < y
t_lt_u : u ∈ Ioi t
this : (u - t) • slope g t u ≤ (u - t) * y
⊢ g u - g t ≤ (u - t) * y
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: case refine_2.hbc
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
p : ℕ
hmp : m ≤ p
IH :
  (∀ k ∈ Ico m p, IntervalIntegrable f μ (a k) (a (k + 1))) →
    ∑ k ∈ Finset.Ico m p, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ = ∫ (x : ℝ) in a m..a p, f x ∂μ
h : ∀ k ∈ Ico m (p + 1), IntervalIntegrable f μ (a k) (a (k + 1))
⊢ IntervalIntegrable f μ (a p) (a (p + 1))

pp: case refine_2
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
p : ℕ
hmp : m ≤ p
IH :
  (∀ k ∈ Ico m p, IntervalIntegrable f μ (a k) (a (k + 1))) →
    ∑ k ∈ Finset.Ico m p, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ = ∫ (x : ℝ) in a m..a p, f x ∂μ
h : ∀ k ∈ Ico m (p + 1), IntervalIntegrable f μ (a k) (a (k + 1))
⊢ ∀ k ∈ Ico m p, IntervalIntegrable f μ (a k) (a (k + 1))

Tactic:
· apply h
      simp [hmp]

Goal state after:
case refine_2
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
p : ℕ
hmp : m ≤ p
IH :
  (∀ k ∈ Ico m p, IntervalIntegrable f μ (a k) (a (k + 1))) →
    ∑ k ∈ Finset.Ico m p, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ = ∫ (x : ℝ) in a m..a p, f x ∂μ
h : ∀ k ∈ Ico m (p + 1), IntervalIntegrable f μ (a k) (a (k + 1))
⊢ ∀ k ∈ Ico m p, IntervalIntegrable f μ (a k) (a (k + 1))
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: case pos
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
ha : IntervalIntegrable f μ a b
hb : IntegrableOn f (Ioi b) μ
h : a ≤ b
⊢ IntegrableOn f (Ioi a) μ

pp: case neg
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
ha : IntervalIntegrable f μ a b
hb : IntegrableOn f (Ioi b) μ
h : b < a
⊢ IntegrableOn f (Ioi a) μ

Tactic:
· exact (Ioc_union_Ioi_eq_Ioi h) ▸ IntegrableOn.union
      ((intervalIntegrable_iff_integrableOn_Ioc_of_le h).1 ha) hb

Goal state after:
case neg
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
ha : IntervalIntegrable f μ a b
hb : IntegrableOn f (Ioi b) μ
h : b < a
⊢ IntegrableOn f (Ioi a) μ
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 ℝ
hf : IntegrableOn f (Iio b) μ
hab : a ≤ b
⊢ ∫ (x : ℝ) in Iio b, f x ∂μ - ∫ (x : ℝ) in Iio a, f x ∂μ = ∫ (x : ℝ) in Ico a b, f x ∂μ

Tactic:
by
  have ha : IntegrableOn f (Iio a) μ := hf.mono_set (Iio_subset_Iio hab)
  have h : IntegrableOn f (Ico a b) μ := hf.mono_set Ico_subset_Iio_self
  rw [sub_eq_iff_eq_add', ← setIntegral_union (by grind) measurableSet_Ico ha h,
      Iio_union_Ico_eq_Iio hab]

Goal state after: