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

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c✝ : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
i : Fin c.length
j : Fin (update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i)
h : ¬i = c.index 0
⊢ Fin n

Tactic:
refine Fin.pred (c.emb i (Fin.cast ?_ j)) ?_

Goal state after:
case neg.refine_1
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c✝ : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
i : Fin c.length
j : Fin (update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i)
h : ¬i = c.index 0
⊢ update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i = c.partSize i

case neg.refine_2
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c✝ : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
i : Fin c.length
j : Fin (update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i)
h : ¬i = c.index 0
⊢ c.emb i (Fin.cast ?neg.refine_1✝ j) ≠ 0
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c✝ : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
i : Fin c.length
x✝¹ : i ∈ univ
j : Fin c.length
x✝ : j ∈ univ
hij : i ≠ j
h : i ≠ c.index 0
hj : j ≠ c.index 0
⊢ (Disjoint on fun m ↦
      range fun j ↦ if h : m = c.index 0 then (c.emb m (Fin.cast ⋯ j.succ)).pred ⋯ else (c.emb m (Fin.cast ⋯ j)).pred ⋯)
    i j

Tactic:
simp only [onFun, h, ↓reduceDIte, hj]

Goal state after:
case inr
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c✝ : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
i : Fin c.length
x✝¹ : i ∈ univ
j : Fin c.length
x✝ : j ∈ univ
hij : i ≠ j
h : i ≠ c.index 0
hj : j ≠ c.index 0
⊢ Disjoint (range fun j ↦ (c.emb i (Fin.cast ⋯ j)).pred ⋯) (range fun j_1 ↦ (c.emb j (Fin.cast ⋯ j_1)).pred ⋯)
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case pos.emb.refine_2
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n✝ : ℕ
c✝ : OrderedFinpartition n✝
n : ℕ
c : OrderedFinpartition (n + 1)
h : range (c.emb 0) = {0}
A : c.length - 1 + 1 = c.length
i : Fin (c.length - 1 + 1)
h' : i ≍ Fin.cast A i
⊢ ∀ (i_1 : Fin (cons 1 (fun i ↦ c.partSize (Fin.cast ⋯ i.succ)) i)),
    cases (motive := fun x ↦ Fin (cons 1 (fun i ↦ c.partSize (Fin.cast ⋯ i.succ)) x) → Fin (n + 1)) (fun x ↦ 0)
        (fun m ↦ succ ∘ fun j ↦ (c.emb (Fin.cast ⋯ m.succ) j).pred ⋯) i i_1 =
      c.emb (Fin.cast A i) ⟨↑i_1, ⋯⟩

Tactic:
intro j
          induction i using Fin.induction with
          | zero =>
            simp only [cases_zero, cast_zero, val_eq_zero]
            exact (apply_eq_of_range_eq_singleton h _).symm
          | succ i => simp

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 : ℕ∞ω
ι : Type u_3
f : ι → E → F
s : Finset ι
h : ∀ i ∈ s, ContDiff 𝕜 n fun x ↦ f i x
⊢ ContDiff 𝕜 n fun x ↦ ∑ i ∈ s, f i x

Tactic:
by
  simp only [← contDiffOn_univ] at *; exact ContDiffOn.sum h

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set 𝕜
f g : 𝕜 → F
hfg : EqOn f g s
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
n : ℕ
⊢ EqOn (iteratedDeriv n f) (iteratedDeriv n g) s

Tactic:
refine fun x hx ↦ Filter.EventuallyEq.iteratedDeriv_eq n ?_
  filter_upwards [IsOpen.mem_nhds hs hx] with a ha
  exact hfg ha

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

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
ε0 : ε ≠ 0
f : α →ₛ ℝ≥0 := piecewise s hs (const α c) (const α 0)
h : ¬∫⁻ (x : α), ↑(f x) ∂μ = ∞
hc : c = 0
⊢ ∃ g,
    (∀ (x : α), (piecewise s hs (const α c) (const α 0)) x ≤ g x) ∧
      LowerSemicontinuous g ∧ ∫⁻ (x : α), ↑(g x) ∂μ ≤ ∫⁻ (x : α), ↑((piecewise s hs (const α c) (const α 0)) x) ∂μ + ε

Tactic:
refine ⟨fun _ => 0, ?_, lowerSemicontinuous_const, ?_⟩

Goal state after:
case pos.refine_1
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
ε0 : ε ≠ 0
f : α →ₛ ℝ≥0 := piecewise s hs (const α c) (const α 0)
h : ¬∫⁻ (x : α), ↑(f x) ∂μ = ∞
hc : c = 0
⊢ ∀ (x : α), (piecewise s hs (const α c) (const α 0)) x ≤ (fun x ↦ 0) x

case pos.refine_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
ε0 : ε ≠ 0
f : α →ₛ ℝ≥0 := piecewise s hs (const α c) (const α 0)
h : ¬∫⁻ (x : α), ↑(f x) ∂μ = ∞
hc : c = 0
⊢ ∫⁻ (x : α), ↑((fun x ↦ 0) x) ∂μ ≤ ∫⁻ (x : α), ↑((piecewise s hs (const α c) (const α 0)) x) ∂μ + ε
Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
ε0 : ε ≠ 0
f : α →ₛ ℝ≥0 := piecewise s hs (const α c) (const α 0)
h : ¬∫⁻ (x : α), ↑(f x) ∂μ = ∞
hc : ¬c = 0
ne_top : μ s ≠ ∞
this : μ s < μ s + ε / ↑c
u : Set α
su : u ⊇ s
u_open : IsOpen u
μu : μ u < μ s + ε / ↑c
⊢ ↑c * (μ s + ε / ↑c) = ↑c * μ s + ε

Tactic:
simp_rw [mul_add]
          rw [ENNReal.mul_div_cancel _ ENNReal.coe_ne_top]
          simpa using hc

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

Goal state before:
pp: case pos
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
h₀ : ∀ᶠ (b : ℝ) in 𝓝[>] a, ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
h₁ : ∀ᶠ (b : ℝ) in 𝓝[>] a, slope f a b < derivWithin f (Ioi a) a + 1
b : ℝ
hb : ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
hslope : slope f a b < derivWithin f (Ioi a) a + 1
hab : a < b
hdiff' : DifferentiableOn ℝ f (Ioc a b)
hcont_Ioc : ∀ z ∈ Ioc a b, ContinuousWithinAt f (Icc a b) z
z : ℝ
hz : z ∈ Icc a b
hz' : z = a
⊢ ContinuousWithinAt f (Icc a b) z

Tactic:
rw [hz']
          exact hcont_at_a.mono Icc_subset_Ici_self

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

Goal state before:
pp: D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
hf'_gt : ∀ x ∈ interior D, C < deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
⊢ x < y → C * (y - x) < f y - f x

Tactic:
hxy

Goal state after:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
hf'_gt : ∀ x ∈ interior D, C < deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x < y
⊢ C * (y - x) < f y - f x
Module: Mathlib.Analysis.Calculus.Deriv.MeanValue

Goal state before:
pp: D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
hf'_ge : ∀ x ∈ interior D, C ≤ deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
⊢ x ≤ y → C * (y - x) ≤ f y - f x

Tactic:
hxy

Goal state after:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
hf'_ge : ∀ x ∈ interior D, C ≤ deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x ≤ y
⊢ C * (y - x) ≤ f y - f 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
ε : ℝ
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
⊢ ‖f z - f y - (fderiv 𝕜 f x) (z - y)‖ < ε * r

Tactic:
calc
    ‖f z - f y - (fderiv 𝕜 f x) (z - y)‖ =
        ‖f z - f x - (fderiv 𝕜 f x) (z - x) - (f y - f x - (fderiv 𝕜 f x) (y - x))‖ := by
      simp only [map_sub]; abel_nf
    _ ≤ ‖f z - f x - (fderiv 𝕜 f x) (z - x)‖ + ‖f y - f x - (fderiv 𝕜 f x) (y - x)‖ :=
      norm_sub_le _ _
    _ ≤ δ * ‖z - x‖ + δ * ‖y - x‖ :=
      add_le_add (hR _ (ball_subset_ball hr.2.le hz)) (hR _ (ball_subset_ball hr.2.le hy))
    _ ≤ δ * r + δ * r := by rw [mem_ball_iff_norm] at hz hy; gcongr
    _ = (ε / 2) * r := by ring
    _ < ε * r := by gcongr; exacts [hr.1, half_lt_self hε]

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

Goal state before:
pp: 𝕜 : Type u_1
M : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
C : ConvexCone 𝕜 M
s : Set M
hs : Convex 𝕜 s
⊢ Disjoint (hull 𝕜 s) C → Disjoint s ↑C

Tactic:
rw [← disjoint_coe]; exact .mono_left subset_hull

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

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
int_f : ∫⁻ (x : α), ↑((piecewise s hs (const α c) (const α 0)) x) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
hc : ¬c = 0
μs_lt_top : μ s < ∞
this : 0 < ε / ↑c
F : Set α
Fs : F ⊆ s
F_closed : IsClosed F
μF : μ s < μ F + ε / ↑c
⊢ ↑c * (μ F + ε / ↑c) = ↑c * μ F + ε

Tactic:
simp_rw [mul_add]
          rw [ENNReal.mul_div_cancel _ ENNReal.coe_ne_top]
          simpa using hc

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
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')
e p : ℕ
hp : n e ≤ p
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → ‖L e (n e) p - L0 b‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e

Tactic:
exact ⟨e, fun e' he' => M _ _ _ _ _ _ le_rfl hp le_rfl le_rfl he'⟩

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

Goal state before:
pp: case inr
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
p : Seminorm ℝ E
x : E
hp : {r | 0 < r ∧ x ∈ r • p.ball 0 1}.Nonempty
⊢ gauge (p.ball 0 1) x = p x

Tactic:
refine IsGLB.csInf_eq ⟨fun r => ?_, fun r hr => le_of_forall_pos_le_add fun ε hε => ?_⟩ hp

Goal state after:
case inr.refine_1
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
p : Seminorm ℝ E
x : E
hp : {r | 0 < r ∧ x ∈ r • p.ball 0 1}.Nonempty
r : ℝ
⊢ r ∈ {r | 0 < r ∧ x ∈ r • p.ball 0 1} → p x ≤ r

case inr.refine_2
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
p : Seminorm ℝ E
x : E
hp : {r | 0 < r ∧ x ∈ r • p.ball 0 1}.Nonempty
r : ℝ
hr : r ∈ lowerBounds {r | 0 < r ∧ x ∈ r • p.ball 0 1}
ε : ℝ
hε : 0 < ε
⊢ r ≤ p x + ε
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 μ
⊢ ∫ (x : X), f x • c ∂μ = (∫ (x : X), f x ∂μ) • c

Tactic:
· by_cases hc : c = 0
    · simp [hc, integral_zero, smul_zero]
    rw [integral_undef hf, integral_undef, zero_smul]
    rw [integrable_smul_const hc]
    simp_rw [hf, not_false_eq_true]

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)
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 * (1 / 2) ^ e
L0 : ℕ → F := fun e ↦ L e (n e) (n e)
this : CauchySeq L0
f' : F
f'K : f' ∈ K
hf' : Tendsto L0 atTop (𝓝 f')
e p : ℕ
hp : n e ≤ p
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → ‖L e (n e) p - L0 b‖ ≤ 12 * (1 / 2) ^ e

Tactic:
exact ⟨e, fun e' he' => M _ _ _ _ _ _ le_rfl hp le_rfl le_rfl he'⟩

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

Goal state before:
pp: case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
⊢ ContinuousWithinAt (fun b ↦ ∫ (x : ℝ) in a..b, f x ∂μ) (Icc b₁ b₂) b₀

Tactic:
have : ∀ b ∈ Icc b₁ b₂,
        ∫ x in a..b, f x ∂μ = (∫ x in a..b₁, f x ∂μ) + ∫ x in b₁..b, f x ∂μ := by
      rintro b ⟨h₁, h₂⟩
      rw [← integral_add_adjacent_intervals _ (h_int' ⟨h₁, h₂⟩)]
      apply h_int.mono_set
      apply uIcc_subset_uIcc
      · exact ⟨min_le_of_left_le (min_le_left a b₁), le_max_of_le_right (le_max_left _ _)⟩
      · exact ⟨min_le_of_left_le (min_le_right _ _),
          le_max_of_le_right (h₁.trans <| h₂.trans (le_max_right a b₂))⟩

Goal state after:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this : ∀ b ∈ Icc b₁ b₂, ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ) in a..b₁, f x ∂μ + ∫ (x : ℝ) in b₁..b, f x ∂μ
⊢ ContinuousWithinAt (fun b ↦ ∫ (x : ℝ) in a..b, f x ∂μ) (Icc b₁ b₂) b₀
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: case refine_3.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this✝¹ :
  (fun b ↦ ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b ↦ ∫ (x : ℝ) in b₁..b₂, {x | x ≤ b}.indicator f x ∂μ
this✝ : ∀ᵐ (t : ℝ) ∂μ, t < b₀ ∨ b₀ < t
x₀ : ℝ
hx₀ : b₀ < x₀
this : ∀ᶠ (x : ℝ) in 𝓝[Icc b₁ b₂] b₀, {t | t ≤ x}.indicator f x₀ = 0
⊢ {t | t ≤ b₀}.indicator f x₀ = 0

Tactic:
simp [hx₀]

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 + -c * x) = c⁻¹ • ∫ (x : ℝ) in d + -c * b..d + -c * a, f x

Tactic:
integral_comp_add_mul f (neg_ne_zero.mpr hc) d,

Goal state after:
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
hc : c ≠ 0
d : ℝ
⊢ (-c)⁻¹ • ∫ (x : ℝ) in d + -c * a..d + -c * b, f x = c⁻¹ • ∫ (x : ℝ) in d + -c * b..d + -c * a, f x
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: case inr
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
ha : IntegrableOn f (Ioi a) μ
hb : IntegrableOn f (Ioi b) μ
this :
  ∀ {a b : ℝ},
    IntegrableOn f (Ioi a) μ →
      IntegrableOn f (Ioi b) μ →
        a ≤ b → ∫ (x : ℝ) in a..b, f x ∂μ + ∫ (x : ℝ) in Ioi b, f x ∂μ = ∫ (x : ℝ) in Ioi a, f x ∂μ
hab : ¬a ≤ b
⊢ ∫ (x : ℝ) in a..b, f x ∂μ + ∫ (x : ℝ) in Ioi b, f x ∂μ = ∫ (x : ℝ) in Ioi a, f x ∂μ

Tactic:
rw [integral_symm, ← this hb ha (le_of_not_ge hab)]; grind

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 ℝ
a b : ℝ
ha : IntegrableOn f (Ioi a) μ
hb : IntegrableOn f (Ioi b) μ
hab : a ≤ b
⊢ ∫ (x : ℝ) in Ioc a b ∪ Ioi b, f x ∂μ = ∫ (x : ℝ) in Ioi a, f x ∂μ

Tactic:
Ioc_union_Ioi_eq_Ioi hab

Goal state after:
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a✝ b✝ : ℝ
f : ℝ → E
μ : Measure ℝ
a b : ℝ
ha : IntegrableOn f (Ioi a) μ
hb : IntegrableOn f (Ioi b) μ
hab : a ≤ b
⊢ ∫ (x : ℝ) in Ioi a, f x ∂μ = ∫ (x : ℝ) in Ioi a, f x ∂μ
Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b c : ℝ
hne : a ≠ b
hc : c ∈ [[a, b]]
h_deriv : ∀ᶠ (x : ℝ) in 𝓝[[[a, b]] \ {c}] c, DifferentiableAt ℝ f x
h_infty : Tendsto (fun x ↦ ‖f x‖) (𝓝[[[a, b]] \ {c}] c) atTop
hg : deriv f =O[𝓝[[[a, b]] \ {c}] c] g
⊢ ∃ l, TendstoIxxClass Icc l l ∧ l.NeBot ∧ l ≤ 𝓝 c ∧ [[a, b]] \ {c} ∈ l

Tactic:
rcases (min_lt_max.2 hne).gt_or_lt c with hlt | hlt

Goal state after:
case inl
E : Type u_1
F : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b c : ℝ
hne : a ≠ b
hc : c ∈ [[a, b]]
h_deriv : ∀ᶠ (x : ℝ) in 𝓝[[[a, b]] \ {c}] c, DifferentiableAt ℝ f x
h_infty : Tendsto (fun x ↦ ‖f x‖) (𝓝[[[a, b]] \ {c}] c) atTop
hg : deriv f =O[𝓝[[[a, b]] \ {c}] c] g
hlt : min a b < c
⊢ ∃ l, TendstoIxxClass Icc l l ∧ l.NeBot ∧ l ≤ 𝓝 c ∧ [[a, b]] \ {c} ∈ l

case inr
E : Type u_1
F : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b c : ℝ
hne : a ≠ b
hc : c ∈ [[a, b]]
h_deriv : ∀ᶠ (x : ℝ) in 𝓝[[[a, b]] \ {c}] c, DifferentiableAt ℝ f x
h_infty : Tendsto (fun x ↦ ‖f x‖) (𝓝[[[a, b]] \ {c}] c) atTop
hg : deriv f =O[𝓝[[[a, b]] \ {c}] c] g
hlt : c < max a b
⊢ ∃ l, TendstoIxxClass Icc l l ∧ l.NeBot ∧ l ≤ 𝓝 c ∧ [[a, b]] \ {c} ∈ l
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: f : ℝ → ℝ
a b : ℝ
hfi : IntervalIntegrable f volume a b
hpos : ∀ x ∈ Ioo a b, 0 < f x
hab : a < b
hsupp : Ioo a b ⊆ support f ∩ Ioc a b
⊢ 0 ≤ᵐ[volume.restrict (Ι a b)] f

Tactic:
rw [EventuallyLE, uIoc_of_le hab.le]

Goal state after:
f : ℝ → ℝ
a b : ℝ
hfi : IntervalIntegrable f volume a b
hpos : ∀ x ∈ Ioo a b, 0 < f x
hab : a < b
hsupp : Ioo a b ⊆ support f ∩ Ioc a b
⊢ ∀ᵐ (x : ℝ) ∂volume.restrict (Ioc a b), 0 x ≤ f x
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
h : f ≤ᵐ[μ.restrict (Icc a b)] g
H : ∀ᵐ (x : ℝ) ∂μ.restrict (Ioc a b), f x ≤ g x :=
  Eventually.filter_mono (ae_mono (Measure.restrict_mono Ioc_subset_Icc_self (le_refl μ))) h
⊢ ∫ (u : ℝ) in a..b, f u ∂μ ≤ ∫ (u : ℝ) in a..b, g u ∂μ

Tactic:
simpa only [integral_of_le hab] using setIntegral_mono_ae_restrict hf.1 hg.1 H

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

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
⊢ volume (Metric.closedBall x ε) = ENNReal.ofReal (min T (2 * ε))

Tactic:
have hT' : |T| = T := abs_eq_self.mpr hT.out.le

Goal state after:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
⊢ volume (Metric.closedBall x ε) = ENNReal.ofReal (min T (2 * ε))
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
⊢ IsUnifLocDoublingMeasure volume

Tactic:
refine ⟨⟨Real.toNNReal 2, Filter.Eventually.of_forall fun ε x => ?_⟩⟩

Goal state after:
T : ℝ
hT : Fact (0 < T)
ε : ℝ
x : AddCircle T
⊢ volume (Metric.closedBall x (2 * ε)) ≤ ↑(Real.toNNReal 2) * volume (Metric.closedBall x ε)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
a : ℝ
h : Measurable ⇑(measurableEquivIoc T a)
s : Set ↑(Ioc a (a + T))
hs : MeasurableSet s
x : ℝ
⊢ (equivIoc T a) ↑x ∈ s ∧ x ∈ Ioc a (a + T) ↔ ∃ (x_1 : x ∈ Ioc a (a + T)), ⟨x, ⋯⟩ ∈ s

Tactic:
rw [and_comm, ← exists_prop]

Goal state after:
T : ℝ
hT : Fact (0 < T)
a : ℝ
h : Measurable ⇑(measurableEquivIoc T a)
s : Set ↑(Ioc a (a + T))
hs : MeasurableSet s
x : ℝ
⊢ (∃ (_ : x ∈ Ioc a (a + T)), (equivIoc T a) ↑x ∈ s) ↔ ∃ (x_1 : x ∈ Ioc a (a + T)), ⟨x, ⋯⟩ ∈ s
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: c : ℂ
R z : ℝ
hz : z ∈ univ
⊢ AnalyticAt ℝ (circleMap c R) z

Tactic:
apply analyticAt_const.add

Goal state after:
c : ℂ
R z : ℝ
hz : z ∈ univ
⊢ AnalyticAt ℝ (fun θ ↦ ↑R * cexp (↑θ * I)) z
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
a : ℝ
ha : a ∈ Ici a₀
⊢ ∀ᵐ (a_1 : ℝ) ∂μ, ‖(Ioi a).indicator f a_1‖ ≤ (Ioi a₀).indicator (norm ∘ f) a_1

Tactic:
refine ae_of_all _ fun x ↦ ?_

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
a : ℝ
ha : a ∈ Ici a₀
x : ℝ
⊢ ‖(Ioi a).indicator f x‖ ≤ (Ioi a₀).indicator (norm ∘ f) x
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: case h_lim
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
⊢ ∀ᵐ (a : ℝ) ∂μ, Tendsto (fun n ↦ (Ioi n).indicator f a) (𝓝[≥] a₀) (𝓝 ((Ioi a₀).indicator f a))

Tactic:
refine ae_of_all _ fun x ↦ ?_

Goal state after:
case h_lim
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
x : ℝ
⊢ Tendsto (fun n ↦ (Ioi n).indicator f x) (𝓝[≥] a₀) (𝓝 ((Ioi a₀).indicator f x))