mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.IsUniformGroup.Order

Goal state before:
pp: α : Type u_1
ι : Type u_2
β : Type u_3
inst✝⁶ : UniformSpace β
inst✝⁵ : AddGroup β
inst✝⁴ : IsUniformAddGroup β
inst✝³ : PartialOrder β
inst✝² : OrderTopology β
inst✝¹ : AddLeftMono β
inst✝ : AddRightMono β
f : ι → α → β
g : α → β
K : Set α
p : Filter ι
u v : β
huv : u < v
hg : ∀ x ∈ K, g x ≤ u
hf :
  ∀ ⦃p_1 : β × β → Prop⦄,
    (∀ᶠ (b : β) in 𝓝 0, ∀ (a b_1 : β), -a + b_1 = b → p_1 (a, b_1)) → ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 K, p_1 (g x.2, f x.1 x.2)
| ∀ ⦃p_1 : β × β → Prop⦄,
    (∀ᶠ (b : β) in 𝓝 0, ∀ (a b_1 : β), -a + b_1 = b → p_1 (a, b_1)) → ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 K, p_1 (g x.2, f x.1 x.2)

Tactic:
conv =>

Goal state after:
α : Type u_1
ι : Type u_2
β : Type u_3
inst✝⁶ : UniformSpace β
inst✝⁵ : AddGroup β
inst✝⁴ : IsUniformAddGroup β
inst✝³ : PartialOrder β
inst✝² : OrderTopology β
inst✝¹ : AddLeftMono β
inst✝ : AddRightMono β
f : ι → α → β
g : α → β
K : Set α
p : Filter ι
u v : β
huv : u < v
hg : ∀ x ∈ K, g x ≤ u
hf :
  ∀ ⦃p_1 : β × β → Prop⦄,
    (∀ᶠ (b : β) in 𝓝 0, ∀ (a b_1 : β), -a + b_1 = b → p_1 (a, b_1)) → ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 K, p_1 (g x.2, f x.1 x.2)
p✝ : β × β → Prop
| (∃ v ∈ 𝓝 0, ∀ y ∈ v, ∀ (a b : β), -a + b = y → p✝ (a, b)) → ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 K, p✝ (g x.2, f x.1 x.2)
Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁶ : MeasurableSpace X
μ : Measure X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : CompactSpace Y
R : Type u_8
inst✝³ : NormedCommRing R
inst✝² : Zero Y
inst✝¹ : NormedAlgebra ℝ R
inst✝ : CompleteSpace R
f : X → C(Y, R)₀
hf : Integrable f μ
y : Y
⊢ (∫ (x : X), f x ∂μ) y = ∫ (x : X), (f x) y ∂μ

Tactic:
by
  calc (∫ x, f x ∂μ) y = ContinuousMapZero.evalCLM ℝ y (∫ x, f x ∂μ) := rfl
    _ = ∫ x, ContinuousMapZero.evalCLM ℝ y (f x) ∂μ :=
          (ContinuousLinearMap.integral_comp_comm _ hf).symm
    _ = _ := rfl

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

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

Tactic:
cases le_total (u t) (v t)

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

case pos.refine_1.inr
ι : Type u_1
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : ℝ → E
c : E
l l' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst✝¹ : l'.IsMeasurablyGenerated
inst✝ : TendstoIxxClass Ioc l l'
hfm : StronglyMeasurableAtFilter f l' μ
hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)
hl : μ.FiniteAtFilter l'
hu : Tendsto u lt l
hv : Tendsto v lt l
hE : CompleteSpace E
A :
  (fun i ↦ ∫ (x : ℝ) in Ioc (u i) (v i), f x ∂μ - μ.real (Ioc (u i) (v i)) • c) =o[lt] fun i ↦ μ.real (Ioc (u i) (v i))
B :
  (fun i ↦ ∫ (x : ℝ) in Ioc (v i) (u i), f x ∂μ - μ.real (Ioc (v i) (u i)) • c) =o[lt] fun i ↦ μ.real (Ioc (v i) (u i))
t : ι
h✝ : v t ≤ u t
⊢ ‖μ.real (Ioc (u t) (v t))‖ ≤ ‖μ.real (Ioc (u t) (v t)) • 1 - μ.real (Ioc (v t) (u t)) • 1‖
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

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

Tactic:
cases le_total (u t) (v t)

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

case pos.refine_2.inr
ι : Type u_1
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : ℝ → E
c : E
l l' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst✝¹ : l'.IsMeasurablyGenerated
inst✝ : TendstoIxxClass Ioc l l'
hfm : StronglyMeasurableAtFilter f l' μ
hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)
hl : μ.FiniteAtFilter l'
hu : Tendsto u lt l
hv : Tendsto v lt l
hE : CompleteSpace E
A :
  (fun i ↦ ∫ (x : ℝ) in Ioc (u i) (v i), f x ∂μ - μ.real (Ioc (u i) (v i)) • c) =o[lt] fun i ↦ μ.real (Ioc (u i) (v i))
B :
  (fun i ↦ ∫ (x : ℝ) in Ioc (v i) (u i), f x ∂μ - μ.real (Ioc (v i) (u i)) • c) =o[lt] fun i ↦ μ.real (Ioc (v i) (u i))
t : ι
h✝ : v t ≤ u t
⊢ ‖μ.real (Ioc (v t) (u t))‖ ≤ ‖μ.real (Ioc (u t) (v t)) • 1 - μ.real (Ioc (v t) (u t)) • 1‖
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: ε : Type u_3
inst✝² : TopologicalSpace ε
inst✝¹ : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst✝ : PseudoMetrizableSpace ε
c : ℝ
h : ‖f (min a b + c)‖ₑ ≠ ∞
hf : IntervalIntegrable f volume (a + c) (b + c)
⊢ ‖f (min (a + c) (b + c))‖ₑ ≠ ∞

Tactic:
min_add_add_right

Goal state after:
ε : Type u_3
inst✝² : TopologicalSpace ε
inst✝¹ : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst✝ : PseudoMetrizableSpace ε
c : ℝ
h : ‖f (min a b + c)‖ₑ ≠ ∞
hf : IntervalIntegrable f volume (a + c) (b + c)
⊢ ‖f (min a b + c)‖ₑ ≠ ∞
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

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

Tactic:
conv =>

Goal state after:
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
t : ℝ
| f t
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

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

Tactic:
conv =>

Goal state after:
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
t : ℝ
| -f t
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a b : ℝ
⊢ ∫ (x : ℝ) in b..a, f x ∂μ = -∫ (x : ℝ) in a..b, f x ∂μ

Tactic:
by
  simp only [intervalIntegral, neg_sub]

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) + ε
⊢ g b - g a ≤ (∫ (y : ℝ) in a..b, φ y) + ε

Tactic:
set s := {t | g t - g a ≤ ∫ u in a..t, (G' u).toReal} ∩ Icc a b

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
⊢ g b - g a ≤ (∫ (y : ℝ) in a..b, φ y) + ε
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

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

Tactic:
convert! norm_setIntegral_le_of_norm_le_const_ae' _ h using 1

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

E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b C : ℝ
f : ℝ → E
h : ∀ᵐ (x : ℝ), x ∈ Ι a b → ‖f x‖ ≤ C
⊢ volume (Ι a b) < ∞
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace X
μ : Measure ℝ
inst✝¹ : NullSingletonClass μ
inst✝ : IsLocallyFiniteMeasure μ
f : X → ℝ → E
a₀ : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
q : X
b₀ ε : ℝ
εpos : ε > 0
a : ℝ
a_lt : a < a₀ ∧ a < b₀
b : ℝ
lt_b : max a₀ b₀ < b
⊢ ∀ᶠ (x : X × ℝ) in 𝓝 (q, b₀),
    dist (∫ (t : ℝ) in a₀..x.2, f x.1 t ∂μ) (∫ (t : ℝ) in a₀..(q, b₀).2, f (q, b₀).1 t ∂μ) < ε

Tactic:
max_lt_iff

Goal state after:
E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace X
μ : Measure ℝ
inst✝¹ : NullSingletonClass μ
inst✝ : IsLocallyFiniteMeasure μ
f : X → ℝ → E
a₀ : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
q : X
b₀ ε : ℝ
εpos : ε > 0
a : ℝ
a_lt : a < a₀ ∧ a < b₀
b : ℝ
lt_b : a₀ < b ∧ b₀ < b
⊢ ∀ᶠ (x : X × ℝ) in 𝓝 (q, b₀),
    dist (∫ (t : ℝ) in a₀..x.2, f x.1 t ∂μ) (∫ (t : ℝ) in a₀..(q, b₀).2, f (q, b₀).1 t ∂μ) < ε
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 (Iic a) μ
hb : IntegrableOn f (Iic b) μ
this :
  ∀ {a b : ℝ},
    IntegrableOn f (Iic a) μ →
      IntegrableOn f (Iic b) μ →
        a ≤ b → ∫ (x : ℝ) in Iic b, f x ∂μ - ∫ (x : ℝ) in Iic a, f x ∂μ = ∫ (x : ℝ) in a..b, f x ∂μ
hab : ¬a ≤ b
⊢ ∫ (x : ℝ) in Iic b, f x ∂μ - ∫ (x : ℝ) in Iic a, f x ∂μ = -(∫ (x : ℝ) in Iic a, f x ∂μ - ∫ (x : ℝ) in Iic b, f x ∂μ)

Tactic:
neg_sub

Goal state after:
case inr
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
ha : IntegrableOn f (Iic a) μ
hb : IntegrableOn f (Iic b) μ
this :
  ∀ {a b : ℝ},
    IntegrableOn f (Iic a) μ →
      IntegrableOn f (Iic b) μ →
        a ≤ b → ∫ (x : ℝ) in Iic b, f x ∂μ - ∫ (x : ℝ) in Iic a, f x ∂μ = ∫ (x : ℝ) in a..b, f x ∂μ
hab : ¬a ≤ b
⊢ ∫ (x : ℝ) in Iic b, f x ∂μ - ∫ (x : ℝ) in Iic a, f x ∂μ = ∫ (x : ℝ) in Iic b, f x ∂μ - ∫ (x : ℝ) in Iic 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 ℝ
hf : IntegrableOn f (Ioi a) μ
hg : IntegrableOn f (Ioi b) μ
this :
  ∀ {a b : ℝ},
    IntegrableOn f (Ioi a) μ →
      IntegrableOn f (Ioi b) μ →
        a ≤ b → ∫ (x : ℝ) in Ioi a, f x ∂μ - ∫ (x : ℝ) in Ioi b, f x ∂μ = ∫ (x : ℝ) in a..b, f x ∂μ
hab : b < a
⊢ ∫ (x : ℝ) in Ioi a, f x ∂μ - ∫ (x : ℝ) in Ioi b, f x ∂μ = -(∫ (x : ℝ) in Ioi b, f x ∂μ - ∫ (x : ℝ) in Ioi a, f x ∂μ)

Tactic:
neg_sub

Goal state after:
case inr
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
hf : IntegrableOn f (Ioi a) μ
hg : IntegrableOn f (Ioi b) μ
this :
  ∀ {a b : ℝ},
    IntegrableOn f (Ioi a) μ →
      IntegrableOn f (Ioi b) μ →
        a ≤ b → ∫ (x : ℝ) in Ioi a, f x ∂μ - ∫ (x : ℝ) in Ioi b, f x ∂μ = ∫ (x : ℝ) in a..b, f x ∂μ
hab : b < a
⊢ ∫ (x : ℝ) in Ioi a, f x ∂μ - ∫ (x : ℝ) in Ioi b, f x ∂μ = ∫ (x : ℝ) in Ioi a, f x ∂μ - ∫ (x : ℝ) in Ioi b, f x ∂μ
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

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

Tactic:
neg_sub

Goal state after:
case inr
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : CompleteSpace E
f f' : ℝ → E
hint : IntervalIntegrable f' volume a b
hab : b ≤ a
hcont : ContinuousOn f (Icc b a)
hderiv : ∀ x ∈ Ioo b a, HasDerivWithinAt f (f' x) (Ioi x) x
⊢ f b - f a = f b - f a
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 ℝ
inst✝ : NullSingletonClass μ
hf : IntegrableOn f (Iio b) μ
hg : IntegrableOn f (Iio a) μ
this :
  ∀ {a b : ℝ},
    IntegrableOn f (Iio b) μ →
      IntegrableOn f (Iio a) μ →
        a ≤ b → ∫ (x : ℝ) in Iio b, f x ∂μ - ∫ (x : ℝ) in Iio a, f x ∂μ = ∫ (x : ℝ) in a..b, f x ∂μ
hab : b < a
⊢ ∫ (x : ℝ) in Iio b, f x ∂μ - ∫ (x : ℝ) in Iio a, f x ∂μ = -(∫ (x : ℝ) in Iio a, f x ∂μ - ∫ (x : ℝ) in Iio b, f x ∂μ)

Tactic:
neg_sub

Goal state after:
case inr
E : Type u_5
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
inst✝ : NullSingletonClass μ
hf : IntegrableOn f (Iio b) μ
hg : IntegrableOn f (Iio a) μ
this :
  ∀ {a b : ℝ},
    IntegrableOn f (Iio b) μ →
      IntegrableOn f (Iio a) μ →
        a ≤ b → ∫ (x : ℝ) in Iio b, f x ∂μ - ∫ (x : ℝ) in Iio a, f x ∂μ = ∫ (x : ℝ) in a..b, f x ∂μ
hab : b < a
⊢ ∫ (x : ℝ) in Iio b, f x ∂μ - ∫ (x : ℝ) in Iio a, f x ∂μ = ∫ (x : ℝ) in Iio b, f x ∂μ - ∫ (x : ℝ) in Iio 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 ℝ
inst✝ : NullSingletonClass μ
hf : IntegrableOn f (Ici a) μ
hg : IntegrableOn f (Ici b) μ
this :
  ∀ {a b : ℝ},
    IntegrableOn f (Ici a) μ →
      IntegrableOn f (Ici b) μ →
        a ≤ b → ∫ (x : ℝ) in Ici a, f x ∂μ - ∫ (x : ℝ) in Ici b, f x ∂μ = ∫ (x : ℝ) in a..b, f x ∂μ
hab : b < a
⊢ ∫ (x : ℝ) in Ici a, f x ∂μ - ∫ (x : ℝ) in Ici b, f x ∂μ = -(∫ (x : ℝ) in Ici b, f x ∂μ - ∫ (x : ℝ) in Ici a, f x ∂μ)

Tactic:
neg_sub

Goal state after:
case inr
E : Type u_5
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
inst✝ : NullSingletonClass μ
hf : IntegrableOn f (Ici a) μ
hg : IntegrableOn f (Ici b) μ
this :
  ∀ {a b : ℝ},
    IntegrableOn f (Ici a) μ →
      IntegrableOn f (Ici b) μ →
        a ≤ b → ∫ (x : ℝ) in Ici a, f x ∂μ - ∫ (x : ℝ) in Ici b, f x ∂μ = ∫ (x : ℝ) in a..b, f x ∂μ
hab : b < a
⊢ ∫ (x : ℝ) in Ici a, f x ∂μ - ∫ (x : ℝ) in Ici b, f x ∂μ = ∫ (x : ℝ) in Ici a, f x ∂μ - ∫ (x : ℝ) in Ici b, f x ∂μ
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

Goal state before:
pp: case inr
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : CompleteSpace E
f : ℝ → E
hint : IntervalIntegrable (deriv f) volume a b
hab : b ≤ a
hcont : ContinuousOn f (Icc b a)
hderiv : ∀ x ∈ Ioo b a, DifferentiableAt ℝ f x
⊢ -(f a - f b) = f b - f a

Tactic:
neg_sub

Goal state after:
case inr
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : CompleteSpace E
f : ℝ → E
hint : IntervalIntegrable (deriv f) volume a b
hab : b ≤ a
hcont : ContinuousOn f (Icc b a)
hderiv : ∀ x ∈ Ioo b a, DifferentiableAt ℝ f x
⊢ f b - f a = f b - f a
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: case inr
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hf : 0 ≤ᵐ[μ.restrict (Ι b a)] f
hfi : IntervalIntegrable f μ a b
hba : b ≤ a
⊢ 0 ≤ ∫ (x : ℝ) in Ioc b a, f x ∂μ

Tactic:
uIoc_of_le hba

Goal state after:
case inr
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hf : 0 ≤ᵐ[μ.restrict (Ioc b a)] f
hfi : IntervalIntegrable f μ a b
hba : b ≤ a
⊢ 0 ≤ ∫ (x : ℝ) in Ioc b a, f x ∂μ
Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable

Goal state before:
pp: a b c : ℝ
⊢ IntervalIntegrable (fun x ↦ (x - c)⁻¹) volume a b ↔ a = b ∨ c ∉ [[a, b]]

Tactic:
constructor
  · refine fun h => or_iff_not_imp_left.2 fun hne hc => ?_
    exact not_intervalIntegrable_of_sub_inv_isBigO_punctured (isBigO_refl _ _) hne hc h
  · rintro (rfl | h₀)
    · exact IntervalIntegrable.refl
    refine ((continuous_sub_right c).continuousOn.inv₀ ?_).intervalIntegrable
    exact fun x hx => sub_ne_zero.2 <| ne_of_mem_of_not_mem hx h₀

Goal state after:
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
⊢ (Measure.map (⇑(equivIoc T a)) volume) s = volume (Subtype.val '' s)

Tactic:
map_apply (by measurability) hs,

Goal state after:
T : ℝ
hT : Fact (0 < T)
a : ℝ
h : Measurable ⇑(measurableEquivIoc T a)
s : Set ↑(Ioc a (a + T))
hs : MeasurableSet s
⊢ volume (⇑(equivIoc T a) ⁻¹' s) = volume (Subtype.val '' s)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Goal state before:
pp: T : ℝ
g : ℝ → ℝ
hg : Periodic g T
h_int : IntervalIntegrable g volume 0 T
hT : 0 < T
t : ℝ
h'_int : ∀ (a₁ a₂ : ℝ), IntervalIntegrable g volume a₁ a₂ := intervalIntegrable₀ hg (LT.lt.ne' hT) h_int
ε : ℝ := Int.fract (t / T) * T
⊢ ∫ (x : ℝ) in 0..ε, g x ≤ sSup ((fun t ↦ ∫ (x : ℝ) in 0..t, g x) '' Icc 0 T)

Tactic:
exact (continuous_primitive h'_int 0).continuousOn.le_sSup_image_Icc
    (mem_Icc_of_Ico (Int.fract_div_mul_self_mem_Ico T t hT))

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 α
ν : Measure β
inst✝¹ : NormedAddCommGroup E
inst✝ : SFinite ν
f : α × β → E
h1f : StronglyMeasurable f
this✝ : ∀ (x : α), ∀ᵐ (y : β) ∂ν, 0 ≤ ‖f (x, y)‖
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
h2f : ∀ᵐ (x : α) ∂μ, ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞
x : α
hx : ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞
⊢ ∫⁻ (y : β), ‖f (x, y)‖ₑ ∂ν = ENNReal.ofReal (∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν).toReal

Tactic:
rw [ofReal_toReal]

Goal state after:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : NormedAddCommGroup E
inst✝ : SFinite ν
f : α × β → E
h1f : StronglyMeasurable f
this✝ : ∀ (x : α), ∀ᵐ (y : β) ∂ν, 0 ≤ ‖f (x, y)‖
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
h2f : ∀ᵐ (x : α) ∂μ, ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞
x : α
hx : ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞
⊢ ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν ≠ ∞
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ≥0
hf : CircleIntegrable f c ↑R
hR : 0 < R
y✝ : ℂ
hy : y✝ ∈ eball 0 ↑R
⊢ ‖y✝‖ < ↑R

Tactic:
simpa using hy

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

Goal state before:
pp: c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
H : HasSum (fun n ↦ ∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹) (2 * ↑π * I)
⊢ ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ = 2 * ↑π * I

Tactic:
have A : CircleIntegrable (fun _ => (1 : ℂ)) c R := continuousOn_const.circleIntegrable'
    refine (H.unique ?_).symm
    simpa only [smul_eq_mul, mul_one, add_sub_cancel] using
      hasSum_two_pi_I_cauchyPowerSeries_integral A (mem_ball_iff_norm.1 hw)

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

Goal state before:
pp: σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
⊢ msymm σ R (Nat.Partition.indiscrete 0) = 1

Tactic:
rw [msymm, Fintype.sum_subsingleton _ ⟨(Sym.nil : Sym σ 0), rfl⟩]

Goal state after:
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
⊢ (Multiset.map X ↑↑⟨Sym.nil, ⋯⟩).prod = 1
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
⊢ (map
        (fun a ↦
          (map ((fun p ↦ (map (fun r ↦ X) p.1).prod * (map (⇑C) p.2).prod) ∘ fun t ↦ (s - t, t))
              (powersetCard a s)).sum)
        (range (s.card + 1))).sum =
    (map (fun j ↦ C (s.esymm j) * X ^ (s.card - j)) (range (s.card + 1))).sum

Tactic:
map_congr (Eq.refl _)

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
⊢ (map ?m.110 (range (s.card + 1))).sum = (map (fun j ↦ C (s.esymm j) * X ^ (s.card - j)) (range (s.card + 1))).sum

R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
⊢ ∀ x ∈ range (s.card + 1),
    (map ((fun p ↦ (map (fun r ↦ X) p.1).prod * (map (⇑C) p.2).prod) ∘ fun t ↦ (s - t, t)) (powersetCard x s)).sum =
      ?m.110 x

R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
⊢ ℕ → R[X]
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
x✝ : ℕ
a✝ : x✝ ∈ range (s.card + 1)
⊢ (map ((fun p ↦ (map (fun r ↦ X) p.1).prod * (map (⇑C) p.2).prod) ∘ fun t ↦ (s - t, t)) (powersetCard x✝ s)).sum =
    (map (fun i ↦ C i.prod * X ^ (s.card - x✝)) (powersetCard x✝ s)).sum

Tactic:
map_congr (Eq.refl _)

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
x✝ : ℕ
a✝ : x✝ ∈ range (s.card + 1)
⊢ (map ?m.148 (powersetCard x✝ s)).sum = (map (fun i ↦ C i.prod * X ^ (s.card - x✝)) (powersetCard x✝ s)).sum

R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
x✝ : ℕ
a✝ : x✝ ∈ range (s.card + 1)
⊢ ∀ x ∈ powersetCard x✝ s,
    ((fun p ↦ (map (fun r ↦ X) p.1).prod * (map (⇑C) p.2).prod) ∘ fun t ↦ (s - t, t)) x = ?m.148 x

R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
x✝ : ℕ
a✝ : x✝ ∈ range (s.card + 1)
⊢ Multiset R → R[X]