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

Goal state before:
pp: case ha
𝕜 : 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
δ : ℝ := ⋯
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
⊢ 0 < r

pp: case hbc
𝕜 : 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
δ : ℝ := ⋯
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 < ε

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

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

Goal state before:
pp: x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x ↦ ∑ i ∈ Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)
F' : ℝ → ℝ := fun x ↦ -x ^ n / (1 - x)
A : ∀ y ∈ Set.Ioo (-1) 1, HasDerivAt F (F' y) y
y : ℝ
hy : y ∈ Set.Icc (-|x|) |x|
⊢ |F' y| = |y| ^ n / |1 - y|

Tactic:
simp [F', abs_div]

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

Goal state before:
pp: case refine_2
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
Sp : Set ℝ := ↑f '' {x | ↑x + y ∈ s}
Sn : Set ℝ := ↑f '' {x | -↑x - y ∈ s}
xn : ↥f.domain
hxn : xn ∈ {x | -↑x - y ∈ s}
xp : ↥f.domain
hxp : xp ∈ {x | ↑x + y ∈ s}
this : ↑xp + (y + (-↑xn - y)) ∈ s
⊢ ↑f xn ≤ ↑f xp

Tactic:
add_sub_cancel,

Goal state after:
case refine_2
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
Sp : Set ℝ := ↑f '' {x | ↑x + y ∈ s}
Sn : Set ℝ := ↑f '' {x | -↑x - y ∈ s}
xn : ↥f.domain
hxn : xn ∈ {x | -↑x - y ∈ s}
xp : ↥f.domain
hxp : xp ∈ {x | ↑x + y ∈ s}
this : ↑xp + -↑xn ∈ s
⊢ ↑f xn ≤ ↑f xp
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: a : ℝ
h : 0 < a
⊢ |1 / (2 * a + 1)| < 1

Tactic:
rw [abs_of_pos, div_lt_one]

Goal state after:
a : ℝ
h : 0 < a
⊢ 1 < 2 * a + 1

a : ℝ
h : 0 < a
⊢ 0 < 2 * a + 1

a : ℝ
h : 0 < a
⊢ 0 < 1 / (2 * a + 1)
Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory

Goal state before:
pp: case add
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (Function.support ⇑f₁) (Function.support ⇑f₂)
h₁ :
  ∫⁻ (x : α), ↑(f₁ x) ∂μ ≠ ∞ →
    ∀ {ε : ℝ≥0∞},
      ε ≠ 0 → ∃ g, (∀ (x : α), g x ≤ f₁ x) ∧ UpperSemicontinuous g ∧ ∫⁻ (x : α), ↑(f₁ x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε
h₂ :
  ∫⁻ (x : α), ↑(f₂ x) ∂μ ≠ ∞ →
    ∀ {ε : ℝ≥0∞},
      ε ≠ 0 → ∃ g, (∀ (x : α), g x ≤ f₂ x) ∧ UpperSemicontinuous g ∧ ∫⁻ (x : α), ↑(f₂ x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε
int_f : ∫⁻ (x : α), ↑((f₁ + f₂) x) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
A : ∫⁻ (x : α), ↑(f₁ x) ∂μ + ∫⁻ (x : α), ↑(f₂ x) ∂μ ≠ ∞
g₁ : α → ℝ≥0
f₁_le_g₁ : ∀ (x : α), g₁ x ≤ f₁ x
g₁cont : UpperSemicontinuous g₁
g₁int : ∫⁻ (x : α), ↑(f₁ x) ∂μ ≤ ∫⁻ (x : α), ↑(g₁ x) ∂μ + ε / 2
g₂ : α → ℝ≥0
f₂_le_g₂ : ∀ (x : α), g₂ x ≤ f₂ x
g₂cont : UpperSemicontinuous g₂
g₂int : ∫⁻ (x : α), ↑(f₂ x) ∂μ ≤ ∫⁻ (x : α), ↑(g₂ x) ∂μ + ε / 2
⊢ ∫⁻ (x : α), ↑(f₁ x) + ↑(f₂ x) ∂μ ≤ ∫⁻ (x : α), ↑(g₁ x) + ↑(g₂ x) ∂μ + ε

Tactic:
rw [lintegral_add_left f₁.measurable.coe_nnreal_ennreal,
      lintegral_add_left g₁cont.measurable.coe_nnreal_ennreal]

Goal state after:
case add
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (Function.support ⇑f₁) (Function.support ⇑f₂)
h₁ :
  ∫⁻ (x : α), ↑(f₁ x) ∂μ ≠ ∞ →
    ∀ {ε : ℝ≥0∞},
      ε ≠ 0 → ∃ g, (∀ (x : α), g x ≤ f₁ x) ∧ UpperSemicontinuous g ∧ ∫⁻ (x : α), ↑(f₁ x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε
h₂ :
  ∫⁻ (x : α), ↑(f₂ x) ∂μ ≠ ∞ →
    ∀ {ε : ℝ≥0∞},
      ε ≠ 0 → ∃ g, (∀ (x : α), g x ≤ f₂ x) ∧ UpperSemicontinuous g ∧ ∫⁻ (x : α), ↑(f₂ x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε
int_f : ∫⁻ (x : α), ↑((f₁ + f₂) x) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
A : ∫⁻ (x : α), ↑(f₁ x) ∂μ + ∫⁻ (x : α), ↑(f₂ x) ∂μ ≠ ∞
g₁ : α → ℝ≥0
f₁_le_g₁ : ∀ (x : α), g₁ x ≤ f₁ x
g₁cont : UpperSemicontinuous g₁
g₁int : ∫⁻ (x : α), ↑(f₁ x) ∂μ ≤ ∫⁻ (x : α), ↑(g₁ x) ∂μ + ε / 2
g₂ : α → ℝ≥0
f₂_le_g₂ : ∀ (x : α), g₂ x ≤ f₂ x
g₂cont : UpperSemicontinuous g₂
g₂int : ∫⁻ (x : α), ↑(f₂ x) ∂μ ≤ ∫⁻ (x : α), ↑(g₂ x) ∂μ + ε / 2
⊢ ∫⁻ (a : α), ↑(f₁ a) ∂μ + ∫⁻ (a : α), ↑(f₂ a) ∂μ ≤ ∫⁻ (a : α), ↑(g₁ a) ∂μ + ∫⁻ (a : α), ↑(g₂ a) ∂μ + ε
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
H₁ : Tendsto (fun r ↦ r⁻¹ • x) (𝓝[<] 1) (𝓝 x)
H₂ : ∀ᶠ (r : ℝ) in 𝓝[<] 1, x ∈ r • s ∧ 0 < r ∧ r < 1
⊢ x ∈ {x | gauge s x < 1}

Tactic:
rcases H₂.exists with ⟨r, hxr, hr₀, hr₁⟩

Goal state after:
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
H₁ : Tendsto (fun r ↦ r⁻¹ • x) (𝓝[<] 1) (𝓝 x)
H₂ : ∀ᶠ (r : ℝ) in 𝓝[<] 1, x ∈ r • s ∧ 0 < r ∧ r < 1
r : ℝ
hxr : x ∈ r • s
hr₀ : 0 < r
hr₁ : r < 1
⊢ x ∈ {x | gauge s x < 1}
Module: Mathlib.Analysis.LocallyConvex.Separation

Goal state before:
pp: case inl
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
t : Set E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
ht : Convex ℝ t
hs₁ : Convex ℝ ∅
hs₂ : IsOpen ∅
disj : Disjoint ∅ t
⊢ ∃ f u, (∀ a ∈ ∅, f a < u) ∧ ∀ b ∈ t, u ≤ f b

pp: case inr
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s t : Set E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
ht : Convex ℝ t
disj : Disjoint s t
a₀ : E
ha₀ : a₀ ∈ s
⊢ ∃ f u, (∀ a ∈ s, f a < u) ∧ ∀ b ∈ t, u ≤ f b

Tactic:
· exact ⟨0, 0, by simp, fun b _hb => le_rfl⟩

Goal state after:
case inr
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s t : Set E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
ht : Convex ℝ t
disj : Disjoint s t
a₀ : E
ha₀ : a₀ ∈ s
⊢ ∃ f u, (∀ a ∈ s, f a < u) ∧ ∀ b ∈ t, u ≤ f b
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
S : Type u_3
inst✝⁶ : CommSemiring S
inst✝⁵ : Module S V
inst✝⁴ : SMulCommClass R S V
inst✝³ : Algebra S R
inst✝² : IsScalarTower S R V
inst✝¹ : ContinuousConstSMul S V
inst✝ : Algebra.IsCentral S R
f : V →L[R] V
hf : f ∈ Subalgebra.center S (V →L[R] V)
a✝ : Nontrivial V
x : V
hx : x ≠ 0
g : StrongDual R V
hg : g x = 1
y : V
⊢ ?m.159 y

Tactic:
by simpa [hg] using congr($(Subalgebra.mem_center_iff.mp hf (g.smulRight y)) x)

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 x : ℝ
hr : 0 < r
ε : ℝ
L₁ L₂ : F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
H : ‖(r / 2) • (L₁ - L₂)‖ ≤ r / 2 * (4 * ε)
⊢ ‖L₁ - L₂‖ ≤ 4 * ε

Tactic:
rwa [norm_smul, Real.norm_of_nonneg (half_pos hr).le, mul_le_mul_iff_right₀ (half_pos hr)] at H

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
𝕜 : Type u_6
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace ℝ E
H : Type u_8
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
φ : X → H →L[𝕜] E
φ_int : Integrable φ μ
v : H
hE : ¬CompleteSpace E
⊢ (∫ (x : X), φ x ∂μ) v = ∫ (x : X), (φ x) v ∂μ

Tactic:
· rcases subsingleton_or_nontrivial H with hH | hH
    · simp [Subsingleton.eq_zero v]
    · have : ¬(CompleteSpace (H →L[𝕜] E)) := by
        rwa [SeparatingDual.completeSpace_continuousLinearMap_iff]
      simp [integral, hE, this]

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

Goal state before:
pp: 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
⊢ ∫ (x : X), c * f x ∂μ = c * ∫ (x : X), f x ∂μ

Tactic:
by_cases hA : CompleteSpace A
  · change ∫ x, ContinuousLinearMap.mul ℝ _ c (f x) ∂μ = ContinuousLinearMap.mul ℝ _ c (∫ x, f x ∂μ)
    rw [ContinuousLinearMap.integral_comp_comm _ hf]
  · simp [integral, hA]

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

Goal state before:
pp: ε : Type u_3
inst✝² : TopologicalSpace ε
inst✝¹ : ENormedAddMonoid ε
inst✝ : PseudoMetrizableSpace ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
⊢ IntervalIntegrable f μ a b ↔ IntegrableOn f (Ι a b) μ

Tactic:
uIoc_eq_union,

Goal state after:
ε : Type u_3
inst✝² : TopologicalSpace ε
inst✝¹ : ENormedAddMonoid ε
inst✝ : PseudoMetrizableSpace ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
⊢ IntervalIntegrable f μ a b ↔ IntegrableOn f (Ioc a b ∪ Ioc b a) μ
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'
⊢ ∃ r',
    (r / 2 < r' ∧ r' ≤ r) ∧
      ∀ (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

Tactic:
refine ⟨t', ⟨hrt', ht't.le.trans (htr'.le.trans Ir'r)⟩, fun y hy z hz ↦ ?_⟩

Goal state after:
𝕜 : 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'
⊢ ‖f (a', x').1 z - f (a', x').1 y - (L z - L y)‖ < s * r
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 : ℝ
⊢ (-c)⁻¹ • ∫ (x : ℝ) in d + -c * a..d + -c * b, f x = c⁻¹ • ∫ (x : ℝ) in d + -c * b..d + -c * a, f x

Tactic:
integral_symm

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

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

Tactic:
by
  by_cases hc : c = 0 <;> simp [hc, integral_comp_sub_div]

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
inst✝ : NullSingletonClass μ
h_int : IntervalIntegrable f μ b₁ b₂
ha : a ∈ [[b₁, b₂]]
x✝¹ : ℝ
x✝ : x✝¹ ∈ [[b₁, b₂]]
⊢ IntervalIntegrable f μ (min b₁ b₂) (max a (max b₁ b₂))

Tactic:
max_eq_right ha.2

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
inst✝ : NullSingletonClass μ
h_int : IntervalIntegrable f μ b₁ b₂
ha : a ∈ [[b₁, b₂]]
x✝¹ : ℝ
x✝ : x✝¹ ∈ [[b₁, b₂]]
⊢ IntervalIntegrable f μ (min b₁ b₂) (max b₁ b₂)
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
main : Icc a b ⊆ {t | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal}
⊢ ∫ (y : ℝ) in a..b, (G' y).toReal ≤ (∫ (y : ℝ) in a..b, φ y) + ε

Tactic:
by
      convert! hG'.le <;>
        · rw [intervalIntegral.integral_of_le hab]
          simp only [integral_Icc_eq_integral_Ioc', Real.volume_singleton]

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

Goal state before:
pp: E✝ : Type u_1
inst✝¹ : NormedAddCommGroup E✝
f✝ : ℝ → E✝
T✝ : ℝ
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT✝ : T ≠ 0
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
hT : 0 < T
n₁ : ℕ
hn₁ : (t - min a₁ a₂) / T ≤ ↑n₁
n₂ : ℕ
hn₂ : (max a₁ a₂ - t) / T ≤ ↑n₂
this : uIcc a₁ a₂ ⊆ uIcc (t - ↑n₁ * T) (t + ↑n₂ * T)
⊢ IntervalIntegrable f volume a₁ a₂

Tactic:
apply IntervalIntegrable.mono_set _ this

Goal state after:
E✝ : Type u_1
inst✝¹ : NormedAddCommGroup E✝
f✝ : ℝ → E✝
T✝ : ℝ
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT✝ : T ≠ 0
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
hT : 0 < T
n₁ : ℕ
hn₁ : (t - min a₁ a₂) / T ≤ ↑n₁
n₂ : ℕ
hn₂ : (max a₁ a₂ - t) / T ≤ ↑n₂
this : uIcc a₁ a₂ ⊆ uIcc (t - ↑n₁ * T) (t + ↑n₂ * T)
⊢ IntervalIntegrable f volume (t - ↑n₁ * T) (t + ↑n₂ * T)
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: case hF
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
ι : Type u_2
f : ι → ℂ → E
g : ℂ → E
c : ℂ
R : ℝ
l : Filter ι
inst✝ : l.IsCountablyGenerated
hR : 0 ≤ R
hf : ∀ᶠ (i : ι) in l, ContinuousOn (f i) (sphere c R)
h : TendstoUniformlyOn f g l (sphere c R)
⊢ ∀ᶠ (i : ι) in l, ContinuousOn (fun x ↦ deriv (circleMap c R) x • (fun z ↦ f i z) (circleMap c R x)) [[0, 2 * π]]

Tactic:
refine hf.mono fun i hi ↦ .smul ?_ (hi.comp ?_ ?_)

Goal state after:
case hF.refine_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
ι : Type u_2
f : ι → ℂ → E
g : ℂ → E
c : ℂ
R : ℝ
l : Filter ι
inst✝ : l.IsCountablyGenerated
hR : 0 ≤ R
hf : ∀ᶠ (i : ι) in l, ContinuousOn (f i) (sphere c R)
h : TendstoUniformlyOn f g l (sphere c R)
i : ι
hi : ContinuousOn (f i) (sphere c R)
⊢ ContinuousOn (deriv (circleMap c R)) [[0, 2 * π]]

case hF.refine_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
ι : Type u_2
f : ι → ℂ → E
g : ℂ → E
c : ℂ
R : ℝ
l : Filter ι
inst✝ : l.IsCountablyGenerated
hR : 0 ≤ R
hf : ∀ᶠ (i : ι) in l, ContinuousOn (f i) (sphere c R)
h : TendstoUniformlyOn f g l (sphere c R)
i : ι
hi : ContinuousOn (f i) (sphere c R)
⊢ ContinuousOn (circleMap c R) [[0, 2 * π]]

case hF.refine_3
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
ι : Type u_2
f : ι → ℂ → E
g : ℂ → E
c : ℂ
R : ℝ
l : Filter ι
inst✝ : l.IsCountablyGenerated
hR : 0 ≤ R
hf : ∀ᶠ (i : ι) in l, ContinuousOn (f i) (sphere c R)
h : TendstoUniformlyOn f g l (sphere c R)
i : ι
hi : ContinuousOn (f i) (sphere c R)
⊢ MapsTo (circleMap c R) [[0, 2 * π]] (sphere c R)
Module: Mathlib.Analysis.BoxIntegral.DivergenceTheorem

Goal state before:
pp: E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
hfc : ContinuousOn f (Box.Icc I)
x : Fin (n + 1) → ℝ
hxI : x ∈ Box.Icc I
a : E
ε : ℝ
h0 : 0 < ε
hε : ∀ y ∈ Box.Icc I, ‖f y - a - f' (y - x)‖ ≤ ε * ‖y - x‖
c : ℝ≥0
hc : I.distortion ≤ c
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := i.insertNth
Hl : I.lower i ∈ Set.Icc (I.lower i) (I.upper i)
Hu : I.upper i ∈ Set.Icc (I.lower i) (I.upper i)
Hi : ∀ x ∈ Set.Icc (I.lower i) (I.upper i), Integrable (I.face i) ⊥ (f ∘ e x) BoxAdditiveMap.volume
this :
  ∀ y ∈ Box.Icc (I.face i),
    ‖f' (Pi.single i (I.upper i - I.lower i)) - (f (e (I.upper i) y) - f (e (I.lower i) y))‖ ≤ 2 * ε * diam (Box.Icc I)
⊢ ‖(∏ j, (I.upper j - I.lower j)) • f' (Pi.single i 1) -
        (integral (I.face i) ⊥ (f ∘ e (I.upper i)) BoxAdditiveMap.volume -
          integral (I.face i) ⊥ (f ∘ e (I.lower i)) BoxAdditiveMap.volume)‖ =
    ‖integral (I.face i) ⊥
        (fun x ↦ f' (Pi.single i (I.upper i - I.lower i)) - (f (e (I.upper i) x) - f (e (I.lower i) x)))
        BoxAdditiveMap.volume‖

Tactic:
by
      rw [← integral_sub (Hi _ Hu) (Hi _ Hl), ← Box.volume_face_mul i, mul_smul, ← Box.volume_apply,
        ← BoxAdditiveMap.toSMul_apply, ← integral_const, ← BoxAdditiveMap.volume,
        ← integral_sub (integrable_const _) ((Hi _ Hu).sub (Hi _ Hl))]
      simp only [(· ∘ ·), Pi.sub_def, ← f'.map_smul, ← Pi.single_smul', smul_eq_mul, mul_one]

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.DivergenceTheorem

Goal state before:
pp: case refine_3.refine_1
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hs : ∀ x ∈ s, ContinuousWithinAt f (Box.Icc I) x
Hd : ∀ x ∈ Box.Icc I \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J ↦ integral J GP (fun x ↦ f (i.insertNth y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (I.lower i) (I.upper i)) → Fin n →ᵇᵃ[↑(I.face i)] E := fun x ↦ ⋯.toBoxAdditive
F : Fin (n + 1) →ᵇᵃ[↑I] E := BoxAdditiveMap.upperSubLower I i fI fb ⋯
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ Box.Icc I ∩ s
ε : ℝ
ε0 : ε > 0
this :
  ∀ᶠ (δ : ℝ) in 𝓝[>] 0,
    δ ∈ Set.Ioc 0 (1 / 2) ∧
      (∀ y₁ ∈ closedBall x δ ∩ Box.Icc I, ∀ y₂ ∈ closedBall x δ ∩ Box.Icc I, ‖f y₁ - f y₂‖ ≤ ε / 2) ∧
        (2 * δ) ^ (n + 1) * ‖(f' x) (Pi.single i 1)‖ ≤ ε / 2
δ : ℝ
hδ0 : 0 < δ
hδ12 : δ ≤ 1 / 2
hdfδ : ∀ y₁ ∈ closedBall x δ ∩ Box.Icc I, ∀ y₂ ∈ closedBall x δ ∩ Box.Icc I, ‖f y₁ - f y₂‖ ≤ ε / 2
hδ : (2 * δ) ^ (n + 1) * ‖(f' x) (Pi.single i 1)‖ ≤ ε / 2
J : Box (Fin (n + 1))
hJI : J ≤ I
hJδ : Box.Icc J ⊆ closedBall x δ
x✝¹ : x ∈ Box.Icc J
x✝ : GP.bDistortion = true → J.distortion ≤ c
Hl : J.lower i ∈ Set.Icc (J.lower i) (J.upper i)
Hu : J.upper i ∈ Set.Icc (J.lower i) (J.upper i)
Hi : ∀ x ∈ Set.Icc (J.lower i) (J.upper i), Integrable (J.face i) GP (fun y ↦ f (i.insertNth x y)) BoxAdditiveMap.volume
hJδ' : Box.Icc J ⊆ closedBall x δ ∩ Box.Icc I
Hmaps : ∀ z ∈ Set.Icc (J.lower i) (J.upper i), MapsTo (i.insertNth z) (Box.Icc (J.face i)) (closedBall x δ ∩ Box.Icc I)
⊢ ‖(BoxAdditiveMap.volume J) ((f' x) (Pi.single i 1))‖ ≤ ε / 2

Tactic:
simp_rw [BoxAdditiveMap.volume_apply, norm_smul, Real.norm_eq_abs, abs_prod]
      refine (mul_le_mul_of_nonneg_right ?_ <| norm_nonneg _).trans hδ
      have : ∀ j, |J.upper j - J.lower j| ≤ 2 * δ := fun j ↦
        calc
          dist (J.upper j) (J.lower j) ≤ dist J.upper J.lower := dist_le_pi_dist _ _ _
          _ ≤ dist J.upper x + dist J.lower x := dist_triangle_right _ _ _
          _ ≤ δ + δ := add_le_add (hJδ J.upper_mem_Icc) (hJδ J.lower_mem_Icc)
          _ = 2 * δ := (two_mul δ).symm
      calc
        ∏ j, |J.upper j - J.lower j| ≤ ∏ j : Fin (n + 1), 2 * δ := by
          gcongr with j _; exact this j
        _ = (2 * δ) ^ (n + 1) := by simp

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

Goal state before:
pp: E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
X : Type u_5
Y : Type u_6
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : MeasurableSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : OpensMeasurableSpace X
inst✝² : OpensMeasurableSpace Y
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
h'f : HasCompactSupport (uncurry f)
μ : Measure X
ν : Measure Y
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : IsFiniteMeasureOnCompacts ν
⊢ ∫ (x : X), ∫ (y : Y), f x y ∂ν ∂μ = ∫ (y : Y), ∫ (x : X), f x y ∂μ ∂ν

Tactic:
let U := Prod.fst '' (tsupport f.uncurry)

Goal state after:
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
X : Type u_5
Y : Type u_6
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : MeasurableSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : OpensMeasurableSpace X
inst✝² : OpensMeasurableSpace Y
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
h'f : HasCompactSupport (uncurry f)
μ : Measure X
ν : Measure Y
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : IsFiniteMeasureOnCompacts ν
U : Set X := Prod.fst '' tsupport (uncurry f)
⊢ ∫ (x : X), ∫ (y : Y), f x y ∂ν ∂μ = ∫ (y : Y), ∫ (x : X), f x y ∂μ ∂ν
Module: Mathlib.Analysis.Complex.CauchyIntegral

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
a : ℝ
h0 : 0 < rexp a
b : ℝ
hle : a ≤ b
hd : ∀ z ∈ (ball c (rexp b) \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z
A : Set ℂ := closedBall c (rexp b) \ ball c (rexp a)
hc : ContinuousOn f A
R : Set ℂ := [[a, b]] ×ℂ [[0, 2 * π]]
g : ℂ → ℂ := fun x ↦ c + cexp x
⊢ ∫ (θ : ℝ) in 0..2 * π, I • f (circleMap c (rexp b) θ) = ∫ (θ : ℝ) in 0..2 * π, I • f (circleMap c (rexp a) θ)

Tactic:
have hdg : Differentiable ℂ g := differentiable_exp.const_add _

Goal state after:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
a : ℝ
h0 : 0 < rexp a
b : ℝ
hle : a ≤ b
hd : ∀ z ∈ (ball c (rexp b) \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z
A : Set ℂ := closedBall c (rexp b) \ ball c (rexp a)
hc : ContinuousOn f A
R : Set ℂ := [[a, b]] ×ℂ [[0, 2 * π]]
g : ℂ → ℂ := fun x ↦ c + cexp x
hdg : Differentiable ℂ g
⊢ ∫ (θ : ℝ) in 0..2 * π, I • f (circleMap c (rexp b) θ) = ∫ (θ : ℝ) in 0..2 * π, I • f (circleMap c (rexp a) θ)