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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
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}
x : Fin n
i : Fin c.length
j : Fin (c.partSize i)
hij : c.emb i j = x.succ
hi : i ≠ c.index 0
A : update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i = c.partSize i
⊢ (if h : i = c.index 0 then (c.emb i (Fin.cast ⋯ (Fin.cast ⋯ j).succ)).pred ⋯
    else (c.emb i (Fin.cast ⋯ (Fin.cast ⋯ j))).pred ⋯) =
    x

Tactic:
by simp [hi, hij]

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) ∂μ = ∞
⊢ ∃ 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 _ => c, fun x => ?_, lowerSemicontinuous_const, by
          simp only [f, _root_.top_add, le_top, h]⟩
      simp only [SimpleFunc.coe_const, SimpleFunc.const_zero, SimpleFunc.coe_zero,
        Set.piecewise_eq_indicator, SimpleFunc.coe_piecewise]
      exact Set.indicator_le_self _ _ _

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 s ↑C → Disjoint (hull 𝕜 s) C

Tactic:
← disjoint_coe,

Goal state after:
𝕜 : 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 s ↑C → Disjoint ↑(hull 𝕜 s) ↑C
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: x : ℝ
h : |x| < 1
i : ℕ
⊢ ‖x ^ (i + 1) / (↑i + 1)‖ = |x| ^ (i + 1) / (↑i + 1)

Tactic:
by
      have : (0 : ℝ) ≤ i + 1 := le_of_lt (Nat.cast_add_one_pos i)
      rw [norm_eq_abs, abs_div, ← pow_abs, abs_of_nonneg this]

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

Goal state before:
pp: E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
hs : Absorbent ℝ s
h : s ⊆ t
x✝ : E
⊢ gauge t x✝ ≤ gauge s x✝

Tactic:
unfold gauge

Goal state after:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
hs : Absorbent ℝ s
h : s ⊆ t
x✝ : E
⊢ sInf {r | 0 < r ∧ x✝ ∈ r • t} ≤ sInf {r | 0 < r ∧ x✝ ∈ r • s}
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
⊢ gauge s 0 = 0

Tactic:
rw [gauge_def']

Goal state after:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
⊢ sInf {r | r ∈ Ioi 0 ∧ r⁻¹ • 0 ∈ s} = 0
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
x : E
⊢ gauge 0 x = 0 x

Tactic:
rw [gauge_def']

Goal state after:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
x : E
⊢ sInf {r | r ∈ Ioi 0 ∧ r⁻¹ • x ∈ 0} = 0 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) = gauge s (r • x)

Tactic:
unfold gauge

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
⊢ sInf {r_1 | 0 < r_1 ∧ ‖r‖ • x ∈ r_1 • s} = sInf {r_1 | 0 < r_1 ∧ r • x ∈ r_1 • s}
Module: Mathlib.Analysis.LocallyConvex.Separation

Goal state before:
pp: case inr.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
b₀ : E
hb₀ : b₀ ∈ t
x₀ : E := b₀ - a₀
C : Set E := x₀ +ᵥ s - t
⊢ ∃ f u, (∀ a ∈ s, f a < u) ∧ ∀ b ∈ t, u ≤ f b

Tactic:
have : (0 : E) ∈ C :=
    ⟨a₀ - b₀, sub_mem_sub ha₀ hb₀, by simp_rw [x₀, vadd_eq_add, sub_add_sub_cancel', sub_self]⟩

Goal state after:
case inr.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
b₀ : E
hb₀ : b₀ ∈ t
x₀ : E := b₀ - a₀
C : Set E := x₀ +ᵥ s - t
this : 0 ∈ C
⊢ ∃ f u, (∀ a ∈ s, f a < u) ∧ ∀ b ∈ t, u ≤ f b
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
r : ℝ≥0
hc : Convex ℝ s
hr : 0 < r
hs : ball 0 ↑r ⊆ s
this : Absorbent ℝ (ball 0 ↑r)
x y : E
⊢ gauge s y + gauge (ball 0 ↑r) (x - y) ≤ gauge s y + ‖x - y‖ / ↑r

Tactic:
gauge_ball

Goal state after:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
r : ℝ≥0
hc : Convex ℝ s
hr : 0 < r
hs : ball 0 ↑r ⊆ s
this : Absorbent ℝ (ball 0 ↑r)
x y : E
⊢ gauge s y + ‖x - y‖ / ↑r ≤ gauge s y + ‖x - y‖ / ↑r

case hr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
r : ℝ≥0
hc : Convex ℝ s
hr : 0 < r
hs : ball 0 ↑r ⊆ s
this : Absorbent ℝ (ball 0 ↑r)
x y : E
⊢ 0 ≤ ↑r
Module: Mathlib.Analysis.LocallyConvex.SeparatingDual

Goal state before:
pp: E : Type u_1
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : Module ℝ E
inst✝² : ContinuousSMul ℝ E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : T1Space E
x : E
hx : x ≠ 0
⊢ ∃ f, f x ≠ 0

Tactic:
rcases geometric_hahn_banach_point_point hx.symm with ⟨f, hf⟩
    simp only [map_zero] at hf
    exact ⟨f, hf.ne'⟩

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

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup V
inst✝³ : TopologicalSpace V
inst✝² : TopologicalSpace R
inst✝¹ : Module R V
inst✝ : SeparatingDual R V
x y : V
⊢ (∀ (g : StrongDual R V), g (x - y) = 0) ↔ ∀ (g : StrongDual R V), g x = g y

Tactic:
simp [sub_eq_zero]

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

Goal state before:
pp: case neg
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
ht : Convex ℝ t
hst : Disjoint (interior s) t
hsint : (interior s).Nonempty
htne : ¬t.Nonempty
⊢ ∃ f u, (∀ a ∈ s, f a ≤ u) ∧ ∀ b ∈ t, u ≤ f b

Tactic:
exact ⟨0, 0, by simp⟩

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

Goal state before:
pp: case refine_1
α : 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
int_fp : Integrable (fun x ↦ ↑(fp x)) μ
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ∞
gp_integrable : Integrable (fun x ↦ (gp x).toReal) μ
gpint : ∫ (x : α), (gp x).toReal ∂μ < ∫ (x : α), ↑(fp x) ∂μ + ↑δ
fm : α → ℝ≥0 := fun x ↦ (-f x).toNNReal
int_fm : Integrable (fun x ↦ ↑(fm x)) μ
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable (fun x ↦ ↑(gm x)) μ
gmint : ∫ (x : α), ↑(fm x) ∂μ - ↑δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x ↦ ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, (g x).toReal = (↑(gp x)).toReal - (↑↑(gm x)).toReal
x : α
⊢ ↑(f x).toNNReal < gp x

Tactic:
exact fp_lt_gp x

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

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s t : Set E
inst✝⁴ : RCLike 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsScalarTower ℝ 𝕜 E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
hs : Convex ℝ s
ht : Convex ℝ t
hst : Disjoint (interior s) t
hsint : (interior s).Nonempty
htne : ¬t.Nonempty
⊢ ∃ f u, (∀ a ∈ s, re (f a) ≤ u) ∧ ∀ b ∈ t, u ≤ re (f b)

Tactic:
exact ⟨0, 0, by simp⟩

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

Goal state before:
pp: case h_ind.e_f
X : Type u_1
E : Type u_3
F : Type u_4
inst✝¹¹ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
𝕜' : Type u_7
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : RCLike 𝕜'
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
inst✝⁴ : NormedSpace ℝ F
σ : 𝕜 →+* 𝕜'
inst✝³ : RingHomIsometric σ
inst✝² : CompleteSpace F
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hσ : ∀ (r : ℝ) (x : 𝕜), σ (r • x) = r • σ x
L : E →SL[σ] F
φ : X → E
φ_int : Integrable φ μ
e : E
s : Set X
s_meas : MeasurableSet s
a✝ : μ s < ∞
a : X
⊢ L (s.indicator (fun x ↦ e) a) = (⇑L ∘ s.indicator fun x ↦ e) a

Tactic:
Function.comp_apply

Goal state after:
case h_ind.e_f
X : Type u_1
E : Type u_3
F : Type u_4
inst✝¹¹ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
𝕜' : Type u_7
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : RCLike 𝕜'
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
inst✝⁴ : NormedSpace ℝ F
σ : 𝕜 →+* 𝕜'
inst✝³ : RingHomIsometric σ
inst✝² : CompleteSpace F
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hσ : ∀ (r : ℝ) (x : 𝕜), σ (r • x) = r • σ x
L : E →SL[σ] F
φ : X → E
φ_int : Integrable φ μ
e : E
s : Set X
s_meas : MeasurableSet s
a✝ : μ s < ∞
a : X
⊢ L (s.indicator (fun x ↦ e) a) = L (s.indicator (fun x ↦ e) a)
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: F : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
f : ℝ → F
inst✝² : CompleteSpace F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
⊢ Measurable fun x ↦ derivWithin f (Ici x) x

Tactic:
refine measurable_of_isClosed fun s hs => ?_
  have :
    (fun x => derivWithin f (Ici x) x) ⁻¹' s =
      { x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ s } ∪
        { x | ¬DifferentiableWithinAt ℝ f (Ici x) x } ∩ { _x | (0 : F) ∈ s } :=
    Set.ext fun x => mem_preimage.trans derivWithin_mem_iff
  rw [this]
  exact
    (measurableSet_of_differentiableWithinAt_Ici_of_isComplete _ hs.isComplete).union
      ((measurableSet_of_differentiableWithinAt_Ici _).compl.inter (MeasurableSet.const _))

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
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
⊢ IsOpen[instTopologicalSpaceProd] {p | p.2 ∈ A (f p.1) L r s}

Tactic:
have : ProperSpace E := .of_locallyCompactSpace 𝕜

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
⊢ IsOpen[instTopologicalSpaceProd] {p | p.2 ∈ A (f p.1) L r s}
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: E : Type u_5
inst✝ : NormedAddCommGroup E
a b : ℝ
f : ℝ → E
h : ‖f (min a b)‖ₑ ≠ ∞
⊢ IntervalIntegrable (fun x ↦ f (-1 * x)) volume (a / -1) (b / -1) ↔
    IntervalIntegrable (fun x ↦ f (-x)) volume (-a) (-b)

Tactic:
simp [div_neg]

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

Tactic:
IntervalIntegrable.iff_comp_neg

Goal state after:
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 (fun x ↦ f (-x)) volume (-0) (-t)
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 : ¬AEStronglyMeasurable f (μ.restrict (Ι a b))
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = 0

Tactic:
rw [intervalIntegral_eq_integral_uIoc, integral_non_aestronglyMeasurable hf, smul_zero]

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
B : ∀ᶠ (u : ℝ) in 𝓝 t, ↑y < G' u
m M : ℝ
H : Ioo m M ⊆ {x | (fun u ↦ ↑y < G' u) x}
hm : m < t
hM : t < M
this : Ioo t (min M b) ∈ 𝓝[>] t
⊢ ∀ᶠ (u : ℝ) in 𝓝[>] t, (u - t) * y ≤ ∫ (w : ℝ) in t..u, (G' w).toReal

Tactic:
filter_upwards [this] with u hu

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
B : ∀ᶠ (u : ℝ) in 𝓝 t, ↑y < G' u
m M : ℝ
H : Ioo m M ⊆ {x | (fun u ↦ ↑y < G' u) x}
hm : m < t
hM : t < M
this : Ioo t (min M b) ∈ 𝓝[>] t
u : ℝ
hu : u ∈ Ioo t (min M b)
⊢ (u - t) * y ≤ ∫ (w : ℝ) in t..u, (G' w).toReal
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

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

Tactic:
simp only [intervalIntegral, integral_ofReal, RCLike.ofReal_sub]

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
inst✝⁷ : LocallyCompactSpace E
F : Type u_3
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
α : Type u_4
inst✝⁴ : TopologicalSpace α
f : α → E → F
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
K : Set (E →L[𝕜] F)
hK : IsComplete K
this : {p | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ K} = {p | p.2 ∈ D (f p.1) K}
x✝⁵ x✝⁴ x✝³ : ℕ
x✝² : x✝³ ≥ x✝⁴
x✝¹ : ℕ
x✝ : x✝¹ ≥ x✝⁴
⊢ MeasurableSet {x | x.2 ∈ B (f x.1) K ((1 / 2) ^ x✝³) ((1 / 2) ^ x✝¹) ((1 / 2) ^ x✝⁵)}

Tactic:
have : ProperSpace E := .of_locallyCompactSpace 𝕜

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
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
K : Set (E →L[𝕜] F)
hK : IsComplete K
this✝ : {p | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ K} = {p | p.2 ∈ D (f p.1) K}
x✝⁵ x✝⁴ x✝³ : ℕ
x✝² : x✝³ ≥ x✝⁴
x✝¹ : ℕ
x✝ : x✝¹ ≥ x✝⁴
this : ProperSpace E
⊢ MeasurableSet {x | x.2 ∈ B (f x.1) K ((1 / 2) ^ x✝³) ((1 / 2) ^ x✝¹) ((1 / 2) ^ x✝⁵)}
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

Goal state before:
pp: E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : CompleteSpace E
f f' : ℝ → E
hab : a ≤ b
hcont : ContinuousOn f (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt f (f' x) (Ioi x) x
f'int : IntervalIntegrable f' volume a b
g : StrongDual ℝ E
⊢ ∫ (x : ℝ) in a..b, g (f' x) = g (f b - f a)

Tactic:
g.map_sub

Goal state after:
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : CompleteSpace E
f f' : ℝ → E
hab : a ≤ b
hcont : ContinuousOn f (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt f (f' x) (Ioi x) x
f'int : IntervalIntegrable f' volume a b
g : StrongDual ℝ E
⊢ ∫ (x : ℝ) in a..b, g (f' x) = g (f b) - g (f a)
Module: Mathlib.MeasureTheory.Measure.Haar.Quotient

Goal state before:
pp: G : Type u_1
inst✝¹⁰ : Group G
inst✝⁹ : MeasurableSpace G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : IsTopologicalGroup G
inst✝⁶ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst✝⁵ : Countable ↥Γ
inst✝⁴ : MeasurableSpace (G ⧸ Γ)
inst✝³ : BorelSpace (G ⧸ Γ)
K : Type u_2
inst✝² : NormedField K
inst✝¹ : NormedSpace ℝ K
inst✝ : μ.IsMulRightInvariant
f : G → K
f_ℒ_1 : Integrable f μ
g : G ⧸ Γ → K
hg : AEStronglyMeasurable g (Measure.map mk (μ.restrict 𝓕))
g_ℒ_infinity : essSup (fun x ↦ ‖g x‖ₑ) (Measure.map mk (μ.restrict 𝓕)) ≠ ∞
F_ae_measurable : AEStronglyMeasurable (automorphize f) (Measure.map mk (μ.restrict 𝓕))
⊢ ∫ (x : G), g ↑x * f x ∂μ = ∫ (x : G ⧸ Γ), g x * automorphize f x ∂Measure.map mk (μ.restrict 𝓕)

Tactic:
by
  let π : G → G ⧸ Γ := QuotientGroup.mk
  have meas_π : Measurable π := continuous_quotient_mk'.measurable
  have H₀ : QuotientGroup.automorphize ((g ∘ π) * f) = g * (QuotientGroup.automorphize f) := by
    exact QuotientGroup.automorphize_smul_left f g
  calc ∫ (x : G), g (π x) * (f x) ∂μ =
        ∫ (x : G ⧸ Γ), QuotientGroup.automorphize ((g ∘ π) * f) x ∂μ_𝓕 := ?_
    _ = ∫ (x : G ⧸ Γ), g x * (QuotientGroup.automorphize f x) ∂μ_𝓕 := by simp [H₀]
  have H₁ : Integrable ((g ∘ π) * f) μ := by
    have : AEStronglyMeasurable (fun (x : G) ↦ g (x : (G ⧸ Γ))) μ :=
      (hg.mono_ac h𝓕.absolutelyContinuous_map).comp_measurable meas_π
    refine Integrable.essSup_smul f_ℒ_1 this ?_
    have hg' : AEStronglyMeasurable (‖g ·‖ₑ) μ_𝓕 := continuous_enorm.comp_aestronglyMeasurable hg
    rw [← essSup_comp_quotientGroup_mk h𝓕 hg'.aemeasurable]
    exact g_ℒ_infinity
  have H₂ : AEStronglyMeasurable (QuotientGroup.automorphize ((g ∘ π) * f)) μ_𝓕 := by
    simp_rw [H₀]
    exact hg.mul F_ae_measurable
  apply QuotientGroup.integral_eq_integral_automorphize h𝓕 H₁ H₂

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

Goal state before:
pp: case convert_2
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) → ℝ) →L[ℝ] E
x : Fin (n + 1) → ℝ
hxI : x ∈ Box.Icc I
a : E
ε : ℝ
h0 : 0 < ε
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)
y : Fin n → ℝ
hy : y ∈ Box.Icc (I.face i)
g : (Fin (n + 1) → ℝ) → E
hfc : ContinuousOn (fun y ↦ a + f' (y - x) + g y) (Box.Icc I)
Hi :
  ∀ x_1 ∈ Set.Icc (I.lower i) (I.upper i),
    Integrable (I.face i) ⊥ ((fun y ↦ a + f' (y - x) + g y) ∘ e x_1) BoxAdditiveMap.volume
hg : g = fun y ↦ (fun y ↦ a + f' (y - x) + g y) y - a - f' (y - x)
this : ∀ z ∈ Set.Icc (I.lower i) (I.upper i), e z y ∈ Box.Icc I
hε : ∀ y ∈ Box.Icc I, ‖g y‖ ≤ ε * diam (Box.Icc I)
⊢ ‖g (e (I.lower i) y) - g (e (I.upper i) y)‖ ≤ 2 * ε * diam (Box.Icc I)

Tactic:
two_mul,

Goal state after:
case convert_2
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) → ℝ) →L[ℝ] E
x : Fin (n + 1) → ℝ
hxI : x ∈ Box.Icc I
a : E
ε : ℝ
h0 : 0 < ε
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)
y : Fin n → ℝ
hy : y ∈ Box.Icc (I.face i)
g : (Fin (n + 1) → ℝ) → E
hfc : ContinuousOn (fun y ↦ a + f' (y - x) + g y) (Box.Icc I)
Hi :
  ∀ x_1 ∈ Set.Icc (I.lower i) (I.upper i),
    Integrable (I.face i) ⊥ ((fun y ↦ a + f' (y - x) + g y) ∘ e x_1) BoxAdditiveMap.volume
hg : g = fun y ↦ (fun y ↦ a + f' (y - x) + g y) y - a - f' (y - x)
this : ∀ z ∈ Set.Icc (I.lower i) (I.upper i), e z y ∈ Box.Icc I
hε : ∀ y ∈ Box.Icc I, ‖g y‖ ≤ ε * diam (Box.Icc I)
⊢ ‖g (e (I.lower i) y) - g (e (I.upper i) y)‖ ≤ (ε + ε) * diam (Box.Icc I)
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: case bound_integrable
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
⊢ Integrable ((Iio a₀).indicator (norm ∘ f)) μ

Tactic:
simpa [integrable_indicator_iff measurableSet_Iio] using! hf.norm

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

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
inst✝¹ : NormedAddCommGroup E
f : α → E
hf : Integrable f μ
ν : Measure β
inst✝ : IsFiniteMeasure ν
⊢ Integrable (fun x ↦ f x.1) (μ.prod ν)

Tactic:
by
  rw [← memLp_one_iff_integrable] at hf ⊢
  exact hf.comp_fst ν

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

Goal state before:
pp: c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
H : ∀ (n : ℕ), n ≠ 0 → ∮ (z : ℂ) in C(c, R), (z - c) ^ (-↑n - 1) = 0
this : ∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ 0 * (z - c)⁻¹ = 2 * ↑π * I
n : ℕ
hn : n ≠ 0
z : ℂ
hz✝ : z ∈ sphere c R
⊢ (z - c) ^ (-↑(n + 1)) = (z - c) ^ (-↑n - 1)

Tactic:
Int.natCast_succ,

Goal state after:
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
H : ∀ (n : ℕ), n ≠ 0 → ∮ (z : ℂ) in C(c, R), (z - c) ^ (-↑n - 1) = 0
this : ∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ 0 * (z - c)⁻¹ = 2 * ↑π * I
n : ℕ
hn : n ≠ 0
z : ℂ
hz✝ : z ∈ sphere c R
⊢ (z - c) ^ (-(↑n + 1)) = (z - c) ^ (-↑n - 1)