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

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

Tactic:
use s, this

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : μ.WeaklyRegular
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
g : α → EReal
g_lt_f : ∀ (x : α), ↑(-f x) < g x
gcont : LowerSemicontinuous g
g_integrable : Integrable (fun x ↦ (g x).toReal) μ
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
gint : ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), -f x ∂μ + ε
⊢ UpperSemicontinuous fun x ↦ -g x

Tactic:
exact
      continuous_neg.comp_lowerSemicontinuous_antitone gcont fun x y hxy =>
        EReal.neg_le_neg_iff.2 hxy

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)
e p q e' p' q' : ℕ
hp : n e ≤ p
hq : n e ≤ q
hp' : n e' ≤ p'
hq' : n e' ≤ q'
he' : e ≤ e'
r : ℕ := max (n e) (n e')
I : (1 / 2) ^ e' ≤ (1 / 2) ^ e
J1 : ‖L e p q - L e p r‖ ≤ 4 * (1 / 2) ^ e
J2 : ‖L e p r - L e' p' r‖ ≤ 4 * (1 / 2) ^ e
J3 : ‖L e' p' r - L e' p' q'‖ ≤ 4 * (1 / 2) ^ e
⊢ ‖L e p q - L e' p' q'‖ = ‖L e p q - L e p r + (L e p r - L e' p' r) + (L e' p' r - L e' p' q')‖

Tactic:
congr 1; abel

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
⊢ MeasurableSet (⋂ e, ⋃ n, ⋂ p, ⋂ (_ : p ≥ n), ⋂ q, ⋂ (_ : q ≥ n), B f K ((1 / 2) ^ p) ((1 / 2) ^ q) ((1 / 2) ^ e))

Tactic:
apply_rules [MeasurableSet.iUnion, MeasurableSet.iInter]

Goal state after:
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
hK : IsComplete K
⊢ ∀ (b : ℕ),
    MeasurableSet (⋃ n, ⋂ p, ⋂ (_ : p ≥ n), ⋂ q, ⋂ (_ : q ≥ n), B f K ((1 / 2) ^ p) ((1 / 2) ^ q) ((1 / 2) ^ b))
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
b✝ : ℕ
⊢ MeasurableSet (⋃ n, ⋂ p, ⋂ (_ : p ≥ n), ⋂ q, ⋂ (_ : q ≥ n), B f K ((1 / 2) ^ p) ((1 / 2) ^ q) ((1 / 2) ^ b✝))

Tactic:
apply_rules [MeasurableSet.iUnion, MeasurableSet.iInter]

Goal state after:
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
hK : IsComplete K
b✝ : ℕ
⊢ ∀ (b : ℕ), MeasurableSet (⋂ p, ⋂ (_ : p ≥ b), ⋂ q, ⋂ (_ : q ≥ b), B f K ((1 / 2) ^ p) ((1 / 2) ^ q) ((1 / 2) ^ b✝))
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
b✝¹ b✝ : ℕ
⊢ MeasurableSet (⋂ p, ⋂ (_ : p ≥ b✝), ⋂ q, ⋂ (_ : q ≥ b✝), B f K ((1 / 2) ^ p) ((1 / 2) ^ q) ((1 / 2) ^ b✝¹))

Tactic:
apply_rules [MeasurableSet.iUnion, MeasurableSet.iInter]

Goal state after:
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
hK : IsComplete K
b✝¹ b✝ : ℕ
⊢ ∀ (b : ℕ), MeasurableSet (⋂ (_ : b ≥ b✝), ⋂ q, ⋂ (_ : q ≥ b✝), B f K ((1 / 2) ^ b) ((1 / 2) ^ q) ((1 / 2) ^ b✝¹))
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
b✝² b✝¹ b✝ : ℕ
⊢ MeasurableSet (⋂ (_ : b✝ ≥ b✝¹), ⋂ q, ⋂ (_ : q ≥ b✝¹), B f K ((1 / 2) ^ b✝) ((1 / 2) ^ q) ((1 / 2) ^ b✝²))

Tactic:
apply_rules [MeasurableSet.iUnion, MeasurableSet.iInter]

Goal state after:
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
hK : IsComplete K
b✝² b✝¹ b✝ : ℕ
⊢ b✝ ≥ b✝¹ → MeasurableSet (⋂ q, ⋂ (_ : q ≥ b✝¹), B f K ((1 / 2) ^ b✝) ((1 / 2) ^ q) ((1 / 2) ^ b✝²))
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
b✝³ b✝² b✝¹ : ℕ
b✝ : b✝¹ ≥ b✝²
⊢ MeasurableSet (⋂ q, ⋂ (_ : q ≥ b✝²), B f K ((1 / 2) ^ b✝¹) ((1 / 2) ^ q) ((1 / 2) ^ b✝³))

Tactic:
apply_rules [MeasurableSet.iUnion, MeasurableSet.iInter]

Goal state after:
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
hK : IsComplete K
b✝³ b✝² b✝¹ : ℕ
b✝ : b✝¹ ≥ b✝²
⊢ ∀ (b : ℕ), MeasurableSet (⋂ (_ : b ≥ b✝²), B f K ((1 / 2) ^ b✝¹) ((1 / 2) ^ b) ((1 / 2) ^ b✝³))
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
b✝⁴ b✝³ b✝² : ℕ
b✝¹ : b✝² ≥ b✝³
b✝ : ℕ
⊢ MeasurableSet (⋂ (_ : b✝ ≥ b✝³), B f K ((1 / 2) ^ b✝²) ((1 / 2) ^ b✝) ((1 / 2) ^ b✝⁴))

Tactic:
apply_rules [MeasurableSet.iUnion, MeasurableSet.iInter]

Goal state after:
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
hK : IsComplete K
b✝⁴ b✝³ b✝² : ℕ
b✝¹ : b✝² ≥ b✝³
b✝ : ℕ
⊢ b✝ ≥ b✝³ → MeasurableSet (B f K ((1 / 2) ^ b✝²) ((1 / 2) ^ b✝) ((1 / 2) ^ b✝⁴))
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
b✝⁵ b✝⁴ b✝³ : ℕ
b✝² : b✝³ ≥ b✝⁴
b✝¹ : ℕ
b✝ : b✝¹ ≥ b✝⁴
⊢ MeasurableSet (B f K ((1 / 2) ^ b✝³) ((1 / 2) ^ b✝¹) ((1 / 2) ^ b✝⁵))

Tactic:
apply_rules [MeasurableSet.iUnion, MeasurableSet.iInter]

Goal state after:
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
hK : IsComplete K
b✝⁵ b✝⁴ b✝³ : ℕ
b✝² : b✝³ ≥ b✝⁴
b✝¹ : ℕ
b✝ : b✝¹ ≥ b✝⁴
⊢ ∀ (b : F),
    MeasurableSet (⋃ (_ : b ∈ K), A f b ((1 / 2) ^ b✝³) ((1 / 2) ^ b✝⁵) ∩ A f b ((1 / 2) ^ b✝¹) ((1 / 2) ^ b✝⁵))

F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
hK : IsComplete K
b✝⁵ b✝⁴ b✝³ : ℕ
b✝² : b✝³ ≥ b✝⁴
b✝¹ : ℕ
b✝ : b✝¹ ≥ b✝⁴
⊢ Countable F
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

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

Tactic:
split_ifs with h
  · simp only [integral_of_le h, uIoc_of_le h, one_smul]
  · simp only [integral_of_ge (not_le.1 h).le, uIoc_of_ge (not_le.1 h).le, neg_one_smul]

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

Goal state before:
pp: g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ico a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn φ (Icc a b) volume
hφg : ∀ x ∈ Ico a b, g' x ≤ φ x
ε : ℝ
εpos : 0 < ε
G' : ℝ → EReal
f_lt_G' : ∀ (x : ℝ), ↑(φ x) < G' x
G'cont : LowerSemicontinuous G'
G'int : Integrable (fun x ↦ (G' x).toReal) (volume.restrict (Icc a b))
G'lt_top : ∀ᵐ (x : ℝ) ∂volume.restrict (Icc a b), G' x < ⊤
hG' : ∫ (x : ℝ) in Icc a b, (G' x).toReal < (∫ (x : ℝ) in Icc a b, φ x) + ε
s : Set ℝ := {t | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Icc a b
this : ContinuousOn (fun t ↦ (g t - g a, ∫ (u : ℝ) in a..t, (G' u).toReal)) (Icc a b)
⊢ IsClosed s

Tactic:
simp only [s, inter_comm]

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
this : ContinuousOn (fun t ↦ (g t - g a, ∫ (u : ℝ) in a..t, (G' u).toReal)) (Icc a b)
⊢ IsClosed (Icc a b ∩ {t | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal})
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 ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn φ (Icc a b) volume
hφg : ∀ x ∈ Ioo a b, g' x ≤ φ x
a_lt_b : a < b
s : Set ℝ := {t | g b - g t ≤ ∫ (u : ℝ) in t..b, φ u} ∩ Icc a b
this : ContinuousOn (fun t ↦ (g b - g t, ∫ (u : ℝ) in t..b, φ u)) (Icc a b)
⊢ IsClosed s

Tactic:
simp only [s, inter_comm]

Goal state after:
g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn φ (Icc a b) volume
hφg : ∀ x ∈ Ioo a b, g' x ≤ φ x
a_lt_b : a < b
s : Set ℝ := {t | g b - g t ≤ ∫ (u : ℝ) in t..b, φ u} ∩ Icc a b
this : ContinuousOn (fun t ↦ (g b - g t, ∫ (u : ℝ) in t..b, φ u)) (Icc a b)
⊢ IsClosed (Icc a b ∩ {t | g b - g t ≤ ∫ (u : ℝ) in t..b, φ u})
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 a..b, f x ∂μ

pp: E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a✝ b✝ : ℝ
f : ℝ → E
μ : Measure ℝ
a b : ℝ
hf : IntegrableOn f (Ioi a) μ
hg : IntegrableOn f (Ioi b) μ
hab : a ≤ b
⊢ ∫ (x : ℝ) in Ioi a, f x ∂μ - ∫ (x : ℝ) in Ioi b, f x ∂μ = ∫ (x : ℝ) in a..b, f x ∂μ

Tactic:
· rw [integral_symm, ← this hg hf hab.le, neg_sub]

Goal state after:
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a✝ b✝ : ℝ
f : ℝ → E
μ : Measure ℝ
a b : ℝ
hf : IntegrableOn f (Ioi a) μ
hg : IntegrableOn f (Ioi b) μ
hab : a ≤ b
⊢ ∫ (x : ℝ) in Ioi a, f x ∂μ - ∫ (x : ℝ) in Ioi b, f x ∂μ = ∫ (x : ℝ) in a..b, f x ∂μ
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 : a₀ < b ∧ b₀ < b
this✝ : IsCompact ({q} ×ˢ Icc a b)
M : ℝ
hM : M ∈ upperBounds ((fun x ↦ ‖Function.uncurry f x‖) '' {q} ×ˢ Icc a b)
δ : ℝ
δpos : 0 < δ
hδ : δ < 1
h'δ : Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b
h''δ : (M + 1) * μ.real (Icc (b₀ - δ) (b₀ + δ)) + δ * μ.real (Icc a b) < ε
v : Set X
v_mem : v ∈ 𝓝[univ] q
this : v ×ˢ Ioo (b₀ - δ) (b₀ + δ) ∈ 𝓝 (q, b₀)
p : X
s : ℝ
hp : p ∈ v
hs : s ∈ Ioo (b₀ - δ) (b₀ + δ)
hv : ∀ p ∈ v, ∀ x ∈ Icc a b, ‖f p x - f q x‖ < δ
J : ∀ (r : X) (u v : ℝ), IntervalIntegrable (f r) μ u v
⊢ ‖∫ (t : ℝ) in a₀..s, f p t ∂μ - ∫ (t : ℝ) in a₀..b₀, f q t ∂μ‖ =
    ‖∫ (t : ℝ) in a₀..s, f p t ∂μ - ∫ (t : ℝ) in a₀..b₀, f p t ∂μ +
        (∫ (t : ℝ) in a₀..b₀, f p t ∂μ - ∫ (t : ℝ) in a₀..b₀, f q t ∂μ)‖

Tactic:
congr 1; abel

Goal state after:
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 a..b, f x ∂μ

pp: E : Type u_5
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a✝ b✝ : ℝ
f : ℝ → E
μ : Measure ℝ
inst✝ : NullSingletonClass μ
a b : ℝ
hf : IntegrableOn f (Iio b) μ
hg : IntegrableOn f (Iio a) μ
hab : a ≤ b
⊢ ∫ (x : ℝ) in Iio b, f x ∂μ - ∫ (x : ℝ) in Iio a, f x ∂μ = ∫ (x : ℝ) in a..b, f x ∂μ

Tactic:
· rw [integral_symm, ← this hg hf hab.le, neg_sub]

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

pp: E : Type u_5
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a✝ b✝ : ℝ
f : ℝ → E
μ : Measure ℝ
inst✝ : NullSingletonClass μ
a b : ℝ
hf : IntegrableOn f (Ici a) μ
hg : IntegrableOn f (Ici b) μ
hab : a ≤ b
⊢ ∫ (x : ℝ) in Ici a, f x ∂μ - ∫ (x : ℝ) in Ici b, f x ∂μ = ∫ (x : ℝ) in a..b, f x ∂μ

Tactic:
· rw [integral_symm, ← this hg hf hab.le, neg_sub]

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

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

Tactic:
simp only [Ioc_eq_empty hab.not_gt, empty_union, union_empty] at hf ⊢

Goal state after:
case inl
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hfi : IntervalIntegrable f μ a b
hab : a ≤ b
hf : 0 ≤ᵐ[μ.restrict (Ioc a b)] f
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = 0 ↔ f =ᵐ[μ.restrict (Ioc a b)] 0
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

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

Tactic:
simp only [Ioc_eq_empty hab.not_gt, empty_union, union_empty] at hf ⊢

Goal state after:
case inr
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hfi : IntervalIntegrable f μ a b
hab : b ≤ a
hf : 0 ≤ᵐ[μ.restrict (Ioc b a)] f
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = 0 ↔ f =ᵐ[μ.restrict (Ioc b a)] 0
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

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

Tactic:
rw [uIoc_comm, uIoc_of_le hba] at hf

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.Topology.Algebra.Order.Floor

Goal state before:
pp: α : Type u_1
inst✝⁵ : Ring α
inst✝⁴ : LinearOrder α
inst✝³ : FloorRing α
inst✝² : TopologicalSpace α
inst✝¹ : IsStrictOrderedRing α
inst✝ : OrderClosedTopology α
n : ℤ
⊢ Tendsto floor (𝓝[≥] ↑n) (pure n)

Tactic:
simpa only [floor_intCast] using tendsto_floor_right_pure_floor (n : α)

Goal state after:
Module: Mathlib.Topology.Algebra.Order.Floor

Goal state before:
pp: α : Type u_1
inst✝⁶ : Ring α
inst✝⁵ : LinearOrder α
inst✝⁴ : FloorRing α
inst✝³ : TopologicalSpace α
inst✝² : IsStrictOrderedRing α
inst✝¹ : OrderClosedTopology α
inst✝ : IsTopologicalAddGroup α
n : ℤ
⊢ Tendsto fract (𝓝[<] ↑n) (𝓝 (↑n - (↑n - 1)))

Tactic:
refine (tendsto_id.mono_left nhdsWithin_le_nhds).sub ?_

Goal state after:
α : Type u_1
inst✝⁶ : Ring α
inst✝⁵ : LinearOrder α
inst✝⁴ : FloorRing α
inst✝³ : TopologicalSpace α
inst✝² : IsStrictOrderedRing α
inst✝¹ : OrderClosedTopology α
inst✝ : IsTopologicalAddGroup α
n : ℤ
⊢ Tendsto (fun x ↦ ↑⌊x⌋) (𝓝[<] ↑n) (𝓝 (↑n - 1))
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
inst✝⁹ : PolishSpace G
Γ : Subgroup G
inst✝⁸ : Γ.Normal
inst✝⁷ : T2Space (G ⧸ Γ)
inst✝⁶ : SecondCountableTopology (G ⧸ Γ)
μ : Measure (G ⧸ Γ)
ν : Measure G
inst✝⁵ : ν.IsMulLeftInvariant
inst✝⁴ : Countable ↥Γ
inst✝³ : ν.IsMulRightInvariant
inst✝² : SigmaFinite ν
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : SigmaFinite μ
s : Set G
fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν
V : Set (G ⧸ Γ)
meas_V : MeasurableSet V
neZeroV : μ V ≠ 0
hV : μ V = ν (QuotientGroup.mk ⁻¹' V ∩ s)
neTopV : μ V ≠ ∞
U : Set (G ⧸ Γ)
a✝ : MeasurableSet U
meas_π : Measurable QuotientGroup.mk
μ' : Measure (G ⧸ Γ) := map QuotientGroup.mk (ν.restrict s)
has_fund : HasFundamentalDomain (↥Γ.op) G ν
i : QuotientMeasureEqMeasurePreimage ν μ'
this✝ : μ'.IsMulLeftInvariant
this : SigmaFinite μ'
⊢ μ' V / ν (QuotientGroup.mk ⁻¹' V ∩ s) = 1

Tactic:
Measure.map_apply meas_π meas_V,

Goal state after:
G : Type u_1
inst✝¹⁴ : Group G
inst✝¹³ : MeasurableSpace G
inst✝¹² : TopologicalSpace G
inst✝¹¹ : IsTopologicalGroup G
inst✝¹⁰ : BorelSpace G
inst✝⁹ : PolishSpace G
Γ : Subgroup G
inst✝⁸ : Γ.Normal
inst✝⁷ : T2Space (G ⧸ Γ)
inst✝⁶ : SecondCountableTopology (G ⧸ Γ)
μ : Measure (G ⧸ Γ)
ν : Measure G
inst✝⁵ : ν.IsMulLeftInvariant
inst✝⁴ : Countable ↥Γ
inst✝³ : ν.IsMulRightInvariant
inst✝² : SigmaFinite ν
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : SigmaFinite μ
s : Set G
fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν
V : Set (G ⧸ Γ)
meas_V : MeasurableSet V
neZeroV : μ V ≠ 0
hV : μ V = ν (QuotientGroup.mk ⁻¹' V ∩ s)
neTopV : μ V ≠ ∞
U : Set (G ⧸ Γ)
a✝ : MeasurableSet U
meas_π : Measurable QuotientGroup.mk
μ' : Measure (G ⧸ Γ) := map QuotientGroup.mk (ν.restrict s)
has_fund : HasFundamentalDomain (↥Γ.op) G ν
i : QuotientMeasureEqMeasurePreimage ν μ'
this✝ : μ'.IsMulLeftInvariant
this : SigmaFinite μ'
⊢ (ν.restrict s) (QuotientGroup.mk ⁻¹' V) / ν (QuotientGroup.mk ⁻¹' V ∩ s) = 1
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Goal state before:
pp: case inr
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
T t₁ t₂ : ℝ
hf : Periodic f T
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℝ → E} {T t₁ t₂ : ℝ},
    Periodic f T → T ≠ 0 → (IntervalIntegrable f volume t₁ (t₁ + T) ↔ IntervalIntegrable f volume t₂ (t₂ + T))
hT : ¬T ≠ 0
⊢ IntervalIntegrable f volume t₁ (t₁ + T) ↔ IntervalIntegrable f volume t₂ (t₂ + T)

Tactic:
simp_all

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst✝ : NullSingletonClass μ
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
a : ℝ
ha : a₀ ≤ a
h_int : IntervalIntegrable f μ a₀ a
b : ℝ
hb : b ∈ Icc a₀ a
⊢ ∫ (x : ℝ) in Ioi b, f x ∂μ = ∫ (x : ℝ) in Ioi a₀, f x ∂μ - ∫ (x : ℝ) in a₀..b, f x ∂μ

Tactic:
simp [← integral_Ioi_sub_Ioi hf hb.1]

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst✝ : NullSingletonClass μ
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
a : ℝ
⊢ a ∈ Iic a₀ → ContinuousWithinAt (fun b ↦ ∫ (x : ℝ) in Iio b, f x ∂μ) (Iic a₀) a

Tactic:
(ha : a ≤ a₀)

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst✝ : NullSingletonClass μ
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
a : ℝ
ha : a ≤ a₀
⊢ ContinuousWithinAt (fun b ↦ ∫ (x : ℝ) in Iio b, f x ∂μ) (Iic a₀) a
Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem

Goal state before:
pp: E : Type u
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
n : ℕ
F : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : Preorder F
inst✝¹ : MeasureSpace F
inst✝ : BorelSpace F
eL : F ≃L[ℝ] Fin (n + 1) → ℝ
he_ord : ∀ (x y : F), eL x ≤ eL y ↔ x ≤ y
he_vol : MeasurePreserving (⇑eL) volume volume
f : Fin (n + 1) → F → E
f' : Fin (n + 1) → F → F →L[ℝ] E
s : Set F
hs : s.Countable
a b : F
hle : a ≤ b
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)
Hd : ∀ x ∈ interior (Set.Icc a b) \ s, ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x
DF : F → E
hDF : ∀ (x : F), DF x = ∑ i, (f' i x) (eL.symm (e i))
Hi : IntegrableOn DF (Set.Icc a b) volume
he_emb : MeasurableEmbedding ⇑eL
hIcc : ⇑eL ⁻¹' Set.Icc (eL a) (eL b) = Set.Icc a b
hIcc' : Set.Icc (eL a) (eL b) = ⇑eL.symm ⁻¹' Set.Icc a b
⊢ ∫ (x : F) in Set.Icc a b, ∑ i, (f' i x) (eL.symm (e i)) =
    ∫ (x : F) in ⇑eL ⁻¹' Set.Icc (eL a) (eL b), ∑ i, (f' i (eL.symm (eL x))) (eL.symm (e i))

Tactic:
simp only [hIcc, eL.symm_apply_apply]

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 σ
inst✝ : Nontrivial R
n : ℕ
s t : Finset σ
hst : s ≠ t
h : ∑ i ∈ t, Finsupp.single i 1 = ∑ i ∈ s, Finsupp.single i 1
this : (t.biUnion fun i ↦ (Finsupp.single i 1).support) = s.biUnion fun i ↦ (Finsupp.single i 1).support
⊢ False

Tactic:
simp_all

Goal state after:
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)
s : Multiset R
ht : s ≤ s✝ ∧ s.card = x✝
⊢ (map (fun r ↦ X) (s✝ - s)).prod * C (map (fun i ↦ i) s).prod = C s.prod * X ^ (s✝.card - x✝)

Tactic:
simp [ht, prod_replicate, map_id', card_sub]

Goal state after:
Module: Mathlib.Analysis.Complex.CauchyIntegral

Goal state before:
pp: E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
hw : w ∈ ball c R
hc : ContinuousOn f (closedBall c R)
hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x
⊢ ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z = (2 * ↑π * I) • f w

Tactic:
rw [← two_pi_I_inv_smul_circleIntegral_sub_inv_smul_of_differentiable_on_off_countable
    hs hw hc hd, smul_inv_smul₀]

Goal state after:
case ha
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
hw : w ∈ ball c R
hc : ContinuousOn f (closedBall c R)
hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x
⊢ 2 * ↑π * I ≠ 0