mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory

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

Tactic:
have μs_lt_top : μ s < ∞ := by simpa [hs, hc, ENNReal.mul_eq_top, lt_top_iff_ne_top] using int_f

Goal state after:
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
int_f : ∫⁻ (x : α), ↑((piecewise s hs (const α c) (const α 0)) x) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
hc : ¬c = 0
μs_lt_top : μ s < ∞
⊢ ∃ g,
    (∀ (x : α), g x ≤ (piecewise s hs (const α c) (const α 0)) x) ∧
      UpperSemicontinuous g ∧ ∫⁻ (x : α), ↑((piecewise s hs (const α c) (const α 0)) x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: x : ℝ
h : |x| < 1
i : ℕ
⊢ |x| ^ (i + 1) / (0 + 1) ≤ |x| ^ i

Tactic:
by
      simpa [pow_succ] using mul_le_of_le_one_right (by positivity) h.le

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

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

Tactic:
by
  obtain rfl | rfl := subset_singleton_iff_eq.1 h
  exacts [gauge_empty, gauge_zero']

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
f : α → ℝ≥0
fint : Integrable (fun x ↦ ↑(f x)) μ
ε : ℝ≥0
εpos : 0 < ↑ε
If : ∫⁻ (x : α), ↑(f x) ∂μ < ∞
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : ∫⁻ (x : α), ↑(f x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ↑ε
Ig : ∫⁻ (x : α), ↑(g x) ∂μ < ∞
⊢ ∀ᵐ (a : α) ∂μ, ‖↑(g a)‖ ≤ ‖↑(f a)‖

Tactic:
exact Filter.Eventually.of_forall fun x => by simp [gf x]

Goal state after:
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 s (x - y) ≤ gauge s y + ‖x - y‖ / ↑r

Tactic:
by grw [gauge_mono this hs (x - y), gauge_ball]; positivity

Goal state after:
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
⊢ SeparatingDual R V ↔ Function.Injective ⇑(ContinuousLinearMap.coeLM R).flip

Tactic:
simp_rw [separatingDual_def, Ne, injective_iff_map_eq_zero]
  congrm ∀ v, ?_
  rw [not_imp_comm, LinearMap.ext_iff]
  push Not; rfl

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

Goal state before:
pp: case pos
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

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:
· obtain ⟨f, u, -, hs', ht'⟩ :=
      geometric_hahn_banach_of_nonempty_interior hs ht hst hsint htne
    exact ⟨f, u, hs', ht'⟩

Goal state after:
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
Module: Mathlib.Analysis.LocallyConvex.SeparatingDual

Goal state before:
pp: R : Type u_4
V : Type u_5
W : Type u_6
inst✝¹³ : NormedField R
inst✝¹² : AddCommGroup V
inst✝¹¹ : AddCommGroup W
inst✝¹⁰ : TopologicalSpace R
inst✝⁹ : TopologicalSpace V
inst✝⁸ : TopologicalSpace W
inst✝⁷ : IsTopologicalRing R
inst✝⁶ : Module R V
inst✝⁵ : Module R W
inst✝⁴ : SeparatingDual R V
inst✝³ : IsTopologicalAddGroup V
inst✝² : IsTopologicalAddGroup W
inst✝¹ : ContinuousSMul R V
inst✝ : ContinuousSMul R W
f g : V ≃L[R] W
x✝ : ∃ y, y • 1 = ↑g.symm ∘SL ↑f
y : R
h : y • 1 = ↑g.symm ∘SL ↑f
hy : y = 0
x : V
⊢ f x = (1 • g) x

Tactic:
simp [by simpa [hy] using congr($h x).symm]

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

Goal state before:
pp: case refine_5
α : 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 ∂μ + ε
⊢ ∫ (x : α), f x ∂μ < ∫ (x : α), ((fun x ↦ -g x) x).toReal ∂μ + ε

Tactic:
· simp_rw [integral_neg, lt_neg_add_iff_add_lt] at gint
    rw [add_comm] at gint
    simpa [integral_neg] using gint

Goal state after:
Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero

Goal state before:
pp: X : Type u_1
R : Type u_3
inst✝⁴ : Zero X
inst✝³ : Zero R
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace R
inst✝ : T1Space R
⊢ IsClosed {f | f 0 = 0}

Tactic:
exact isClosed_singleton.preimage <| continuous_eval_const 0

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: case refine_1
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
x : ℝ
hx : x ∈ {x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K}
e : ℕ
this : 0 < (1 / 2) ^ e
R : ℝ
R_pos : R > 0
hR : ∀ r ∈ Ioo 0 R, x ∈ A f (derivWithin f (Ici x) x) r ((1 / 2) ^ e)
n : ℕ
hn : (1 / 2) ^ n < R
p : ℕ
hp : p ≥ n
q : ℕ
hq : q ≥ n
⊢ x ∈ A f (derivWithin f (Ici x) x) ((1 / 2) ^ p) ((1 / 2) ^ e)

Tactic:
· refine hR _ ⟨pow_pos (by norm_num) _, lt_of_le_of_lt ?_ hn⟩
      exact pow_le_pow_of_le_one (by norm_num) (by norm_num) (by assumption)

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: case refine_2
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
x : ℝ
hx : x ∈ {x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K}
e : ℕ
this : 0 < (1 / 2) ^ e
R : ℝ
R_pos : R > 0
hR : ∀ r ∈ Ioo 0 R, x ∈ A f (derivWithin f (Ici x) x) r ((1 / 2) ^ e)
n : ℕ
hn : (1 / 2) ^ n < R
p : ℕ
hp : p ≥ n
q : ℕ
hq : q ≥ n
⊢ x ∈ A f (derivWithin f (Ici x) x) ((1 / 2) ^ q) ((1 / 2) ^ e)

Tactic:
· refine hR _ ⟨pow_pos (by norm_num) _, lt_of_le_of_lt ?_ hn⟩
      exact pow_le_pow_of_le_one (by norm_num) (by norm_num) (by assumption)

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
⊢ ‖L e p q - L e' p' q'‖ ≤ 12 * (1 / 2) ^ e

Tactic:
have J3 : ‖L e' p' r - L e' p' q'‖ ≤ 4 * (1 / 2) ^ e := by
      have I1 : x ∈ A f (L e' p' r) ((1 / 2) ^ p') ((1 / 2) ^ e') :=
        (hn e' p' r hp' (le_max_right _ _)).2.1
      have I2 : x ∈ A f (L e' p' q') ((1 / 2) ^ p') ((1 / 2) ^ e') := (hn e' p' q' hp' hq').2.1
      exact norm_sub_le_of_mem_A P _ (A_mono _ _ I I1) (A_mono _ _ I I2)

Goal state after:
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'‖ ≤ 12 * (1 / 2) ^ e
Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap

Goal state before:
pp: X : Type u_1
E : Type u_3
F : Type u_4
inst✝⁵ : MeasurableSpace X
μ : Measure X
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace E
f : X → E × F
hf : Integrable f μ
⊢ (∫ (x : X), f x ∂μ).2 = ∫ (x : X), (f x).2 ∂μ

Tactic:
rw [← Prod.fst_swap, swap_integral]

Goal state after:
X : Type u_1
E : Type u_3
F : Type u_4
inst✝⁵ : MeasurableSpace X
μ : Measure X
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace E
f : X → E × F
hf : Integrable f μ
⊢ (∫ (x : X), (f x).swap ∂μ).1 = ∫ (x : X), (f x).2 ∂μ
Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap

Goal state before:
pp: case pos.refine_1
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : Integrable g (μ.withDensity fun x ↦ ↑(f x))
c : E
s : Set X
s_meas : MeasurableSet s
hs : (μ.withDensity fun x ↦ ↑(f x)) s < ∞
⊢ 0 ≤ ∫ (a : X) in s, ↑(f a) ∂μ

pp: case pos.refine_1.hfi
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : Integrable g (μ.withDensity fun x ↦ ↑(f x))
c : E
s : Set X
s_meas : MeasurableSet s
hs : (μ.withDensity fun x ↦ ↑(f x)) s < ∞
⊢ Integrable (fun x ↦ ↑(f x)) (μ.restrict s)

Tactic:
· exact integral_nonneg fun x => NNReal.coe_nonneg _

Goal state after:
case pos.refine_1.hfi
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : Integrable g (μ.withDensity fun x ↦ ↑(f x))
c : E
s : Set X
s_meas : MeasurableSet s
hs : (μ.withDensity fun x ↦ ↑(f x)) s < ∞
⊢ Integrable (fun x ↦ ↑(f x)) (μ.restrict s)
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
F : ι → α → E
hF_int : ∀ (i : ι), Integrable (F i) μ
hF_sum : Summable fun i ↦ ∫ (a : α), ‖F i a‖ ∂μ
hE : CompleteSpace E
i : ι
⊢ ENNReal.ofReal (∫ (a : α), ↑‖F i a‖₊ ∂μ) = ↑‖∫ (a : α), ‖F i a‖ ∂μ‖₊

Tactic:
coe_nnreal_eq,

Goal state after:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
F : ι → α → E
hF_int : ∀ (i : ι), Integrable (F i) μ
hF_sum : Summable fun i ↦ ∫ (a : α), ‖F i a‖ ∂μ
hE : CompleteSpace E
i : ι
⊢ ENNReal.ofReal (∫ (a : α), ↑‖F i a‖₊ ∂μ) = ENNReal.ofReal ↑‖∫ (a : α), ‖F i a‖ ∂μ‖₊
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: ε : Type u_3
inst✝² : TopologicalSpace ε
inst✝¹ : ENormedAddMonoid ε
f : ℝ → ε
μ : Measure ℝ
inst✝ : PseudoMetrizableSpace ε
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
p : ℕ
hp : m ≤ p
IH : (∀ k ∈ Ico m p, IntervalIntegrable f μ (a k) (a (k + 1))) → IntervalIntegrable f μ (a m) (a p)
h : ∀ k ∈ Ico m (p + 1), IntervalIntegrable f μ (a k) (a (k + 1))
⊢ p ∈ Ico m (p + 1)

Tactic:
by simp [hp]

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
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 : Continuous[instTopologicalSpaceProd, _] fun p ↦ ‖f a p.2 - f a p.1 - (L p.2 - L p.1)‖
C : (closedBall x t ×ˢ closedBall x t).Nonempty
⊢ ∃ b < s * r, ∀ y ∈ closedBall x t, ∀ z ∈ closedBall x t, ‖f a z - f a y - (L z - L y)‖ ≤ b

Tactic:
rcases ((isCompact_closedBall x t).prod (isCompact_closedBall x t)).exists_isMaxOn
      C B.continuousOn with ⟨p, pt, hp⟩

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 : Continuous[instTopologicalSpaceProd, _] fun p ↦ ‖f a p.2 - f a p.1 - (L p.2 - L p.1)‖
C : (closedBall x t ×ˢ closedBall x t).Nonempty
p : E × E
pt : p ∈ closedBall x t ×ˢ closedBall x t
hp : IsMaxOn (fun p ↦ ‖f a p.2 - f a p.1 - (L p.2 - L p.1)‖) (closedBall x t ×ˢ closedBall x t) p
⊢ ∃ b < s * r, ∀ y ∈ closedBall x t, ∀ z ∈ closedBall x t, ‖f a z - f a y - (L z - L y)‖ ≤ b
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'
y : E
hy : dist y (a', x').2 < t'
z : E
hz : dist z (a', x').2 < t'
dyx : dist y x ≤ t
dzx : dist z x ≤ t
⊢ (a', z).2 ∈ closedBall x t

Tactic:
simp [dzx]

Goal state after:
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)
A : ∀ᶠ (δ : ℝ) in 𝓝[>] 0, δ ∈ Ioo 0 1
I : Tendsto (fun δ ↦ b₀ - δ) (𝓝 0) (𝓝 (b₀ - 0))
⊢ ∀ᶠ (δ : ℝ) in 𝓝 0, Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b

Tactic:
have J : Tendsto (fun δ ↦ b₀ + δ) (𝓝 0) (𝓝 (b₀ + 0)) := tendsto_const_nhds.add tendsto_id

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
this : IsCompact ({q} ×ˢ Icc a b)
M : ℝ
hM : M ∈ upperBounds ((fun x ↦ ‖Function.uncurry f x‖) '' {q} ×ˢ Icc a b)
A : ∀ᶠ (δ : ℝ) in 𝓝[>] 0, δ ∈ Ioo 0 1
I : Tendsto (fun δ ↦ b₀ - δ) (𝓝 0) (𝓝 (b₀ - 0))
J : Tendsto (fun δ ↦ b₀ + δ) (𝓝 0) (𝓝 (b₀ + 0))
⊢ ∀ᶠ (δ : ℝ) in 𝓝 0, Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

Goal state before:
pp: case inr
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g [[a, b]]
hderiv : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt g (g' x) x
hpos : ∀ x ∈ Ioo (min a b) (max a b), 0 ≤ g' x
hab : b ≤ a
⊢ IntervalIntegrable g' volume a b

Tactic:
simp only [uIcc_of_ge, min_eq_right, max_eq_left, hab, IntervalIntegrable, Ioc_eq_empty_of_le,
      integrableOn_empty, true_and] at hcont hderiv hpos ⊢

Goal state after:
case inr
g' g : ℝ → ℝ
a b : ℝ
hab : b ≤ a
hcont : ContinuousOn g (Icc b a)
hderiv : ∀ x ∈ Ioo b a, HasDerivAt g (g' x) x
hpos : ∀ x ∈ Ioo b a, 0 ≤ g' x
⊢ IntegrableOn g' (Ioc b a) volume
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: case hg
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
inst✝ : NullSingletonClass μ
h : ∀ x ∈ Ioo a b, f x ≤ g x
⊢ IntegrableOn g (Ioo a b) μ

pp: case hs
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
inst✝ : NullSingletonClass μ
h : ∀ x ∈ Ioo a b, f x ≤ g x
⊢ MeasurableSet (Ioo a b)

pp: case h
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
inst✝ : NullSingletonClass μ
h : ∀ x ∈ Ioo a b, f x ≤ g x
⊢ ∀ x ∈ Ioo a b, f x ≤ g x

Tactic:
· apply hg.1.mono Ioo_subset_Ioc_self le_rfl

Goal state after:
case hs
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
inst✝ : NullSingletonClass μ
h : ∀ x ∈ Ioo a b, f x ≤ g x
⊢ MeasurableSet (Ioo a b)

case h
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
inst✝ : NullSingletonClass μ
h : ∀ x ∈ Ioo a b, f x ≤ g x
⊢ ∀ x ∈ Ioo a b, f x ≤ g x
Module: Mathlib.Topology.Algebra.Order.Floor

Goal state before:
pp: α : Type u_1
inst✝⁴ : Ring α
inst✝³ : LinearOrder α
inst✝² : FloorRing α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
x : α
⊢ ↑(⌊x⌋ + 1) - 1 ≤ x

Tactic:
rw [cast_add, cast_one, add_sub_cancel_right]; exact floor_le _

Goal state after:
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 ≠ ∞
⊢ QuotientMeasureEqMeasurePreimage ν μ

Tactic:
apply fund_dom_s.quotientMeasureEqMeasurePreimage

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 ≠ ∞
⊢ μ = map (Quotient.mk (MulAction.orbitRel (↥Γ.op) G)) (ν.restrict s)
Module: Mathlib.Topology.Algebra.Order.Floor

Goal state before:
pp: case inl.left
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : FloorRing α
inst✝⁴ : TopologicalSpace α
inst✝³ : IsStrictOrderedRing α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : β → α → γ
h : ContinuousOn (uncurry f) (univ ×ˢ Icc 0 1)
hf : ∀ (s : β), f s 0 = f s 1
s : β
n : ℤ
⊢ Tendsto (uncurry f ∘ Prod.map id fract) (𝓝 s ×ˢ 𝓝[<] ↑n) (𝓝 ((uncurry f ∘ Prod.map id fract) (s, ↑n)))

Tactic:
refine (((h (s, 1) ⟨trivial, zero_le_one, le_rfl⟩).tendsto.mono_left ?_).comp
        (tendsto_id.prodMap (tendsto_fract_left _))).mono_right (le_of_eq ?_)
      · rw [nhdsWithin_prod_eq, nhdsWithin_univ, ← nhdsWithin_Ico_eq_nhdsLT one_pos]
        exact Filter.prod_mono le_rfl (nhdsWithin_mono _ Ico_subset_Icc_self)
      · simp [hf]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.Quotient

Goal state before:
pp: G' : Type u_1
inst✝¹⁰ : AddGroup G'
inst✝⁹ : MeasurableSpace G'
inst✝⁸ : TopologicalSpace G'
inst✝⁷ : IsTopologicalAddGroup G'
inst✝⁶ : BorelSpace G'
μ' : Measure G'
Γ' : AddSubgroup G'
𝓕' : Set G'
h𝓕 : IsAddFundamentalDomain (↥Γ'.op) 𝓕' μ'
inst✝⁵ : Countable ↥Γ'
inst✝⁴ : MeasurableSpace (G' ⧸ Γ')
inst✝³ : BorelSpace (G' ⧸ Γ')
K : Type u_2
inst✝² : NormedField K
inst✝¹ : NormedSpace ℝ K
inst✝ : μ'.IsAddRightInvariant
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 𝓕'))
π : G' → G' ⧸ Γ' := mk
meas_π : Measurable π
H₀ : automorphize (g ∘ π * f) = g * automorphize f
⊢ ∫ (x : G'), g ↑x * f x ∂μ' = ∫ (x : G' ⧸ Γ'), g x * automorphize f x ∂Measure.map mk (μ'.restrict 𝓕')

Tactic:
calc ∫ (x : G'), g (π x) * f x ∂μ' =
    ∫ (x : G' ⧸ Γ'), QuotientAddGroup.automorphize ((g ∘ π) * f) x ∂μ_𝓕 := ?_
    _ = ∫ (x : G' ⧸ Γ'), g x * (QuotientAddGroup.automorphize f x) ∂μ_𝓕 := by simp [H₀]

Goal state after:
G' : Type u_1
inst✝¹⁰ : AddGroup G'
inst✝⁹ : MeasurableSpace G'
inst✝⁸ : TopologicalSpace G'
inst✝⁷ : IsTopologicalAddGroup G'
inst✝⁶ : BorelSpace G'
μ' : Measure G'
Γ' : AddSubgroup G'
𝓕' : Set G'
h𝓕 : IsAddFundamentalDomain (↥Γ'.op) 𝓕' μ'
inst✝⁵ : Countable ↥Γ'
inst✝⁴ : MeasurableSpace (G' ⧸ Γ')
inst✝³ : BorelSpace (G' ⧸ Γ')
K : Type u_2
inst✝² : NormedField K
inst✝¹ : NormedSpace ℝ K
inst✝ : μ'.IsAddRightInvariant
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 𝓕'))
π : G' → G' ⧸ Γ' := mk
meas_π : Measurable π
H₀ : automorphize (g ∘ π * f) = g * automorphize f
⊢ ∫ (x : G'), g (π x) * f x ∂μ' = ∫ (x : G' ⧸ Γ'), automorphize (g ∘ π * f) x ∂Measure.map mk (μ'.restrict 𝓕')