mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Order.UpperLower

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
h : ∀ (δ : ℝ), 0 < δ → ∃ y, closedBall y (δ / 4) ⊆ closedBall x δ ∧ closedBall y (δ / 4) ⊆ interior s
⊢ ¬Tendsto (fun r ↦ volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0) (𝓝 0)

Tactic:
by
  choose f hf₀ hf₁ using h
  intro H
  obtain ⟨ε, -, hε', hε₀⟩ := exists_seq_strictAnti_tendsto_nhdsWithin (0 : ℝ)
  refine not_eventually.2
    (Frequently.of_forall fun _ ↦ lt_irrefl <| ENNReal.ofReal <| 4⁻¹ ^ Fintype.card ι)
    ((Filter.Tendsto.eventually_lt (H.comp hε₀) tendsto_const_nhds ?_).mono fun n ↦
      lt_of_le_of_lt ?_)
  on_goal 2 =>
    calc
      ENNReal.ofReal (4⁻¹ ^ Fintype.card ι)
        = volume (closedBall (f (ε n) (hε' n)) (ε n / 4)) / volume (closedBall x (ε n)) := ?_
      _ ≤ volume (closure s ∩ closedBall x (ε n)) / volume (closedBall x (ε n)) := by
        gcongr
        exact subset_inter ((hf₁ _ <| hε' n).trans interior_subset_closure) <| hf₀ _ <| hε' n
    have := hε' n
    rw [Real.volume_pi_closedBall, Real.volume_pi_closedBall, ← ENNReal.ofReal_div_of_pos,
      ← div_pow, mul_div_mul_left _ _ (two_ne_zero' ℝ), div_right_comm, div_self, one_div]
  all_goals positivity

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Prokhorov

Goal state before:
pp: case refine_1
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst✝³ : PseudoMetricSpace 𝓧
inst✝² : OpensMeasurableSpace 𝓧
inst✝¹ : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
inst✝ : CompleteSpace 𝓧
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
hnonempty : Nonempty 𝓧
D : ℕ → 𝓧
hD : DenseRange D
u : ℕ → ℝ
hu_anti : StrictAnti u
hu_pos : ∀ (n : ℕ), 0 < u n
hu : Tendsto u atTop (𝓝 0)
hcov : ∀ (m : ℕ), ⋃ i, ball (D i) (u m) = univ
ε : ℝ≥0∞
εpos : 0 < ε
hεbound : ε ≤ 1
m : ℕ
⊢ 0 < ε * 2 ^ (-↑m)

Tactic:
simpa using ⟨εpos, (ENNReal.zpow_pos (by simp) (by simp) (-↑m))⟩

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.AddContent

Goal state before:
pp: case h
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
μ : Measure α
m : Set α → E
hm : ∀ (s : Set α), ‖m s‖ₑ ≤ μ s
inst✝ : IsFiniteMeasure μ
h'm : ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t
h''m : ∀ (s : Set α), ¬MeasurableSet s → m s = 0
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Function.onFun Disjoint f)
i : ℕ
⊢ ‖m (f i)‖ₑ ≤ μ (f i)

Tactic:
apply hm

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation

Goal state before:
pp: case pos
α : Type u_1
inst✝⁸ : LinearOrder α
inst✝⁷ : DenselyOrdered α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : SecondCountableTopology α
inst✝³ : CompactIccSpace α
hα : MeasurableSpace α
inst✝² : BorelSpace α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : α → E
a : α
hf : BoundedVariationOn f univ
ha : IsBot a
h : ∃ x, IsBot x
heqa : h.choose = a
A : ⋯.choose {a} = 0
⊢ hf.vectorMeasure {a} = Function.rightLim f a - Function.leftLim f a

Tactic:
simp only [vectorMeasure, h, ↓reduceDIte, add_apply, A, zero_add]

Goal state after:
case pos
α : Type u_1
inst✝⁸ : LinearOrder α
inst✝⁷ : DenselyOrdered α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : SecondCountableTopology α
inst✝³ : CompactIccSpace α
hα : MeasurableSpace α
inst✝² : BorelSpace α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : α → E
a : α
hf : BoundedVariationOn f univ
ha : IsBot a
h : ∃ x, IsBot x
heqa : h.choose = a
A : ⋯.choose {a} = 0
⊢ (VectorMeasure.dirac ⋯.choose (Function.rightLim f ⋯.choose - f ⋯.choose)) {a} =
    Function.rightLim f a - Function.leftLim f a
Module: Mathlib.MeasureTheory.VectorMeasure.SetIntegral

Goal state before:
pp: case h_ind
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
H : Type u_6
mX : MeasurableSpace X
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedAddCommGroup H
μ : VectorMeasure X F
f : X → E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedSpace ℝ G
inst✝² : NormedSpace ℝ H
B : E →L[ℝ] F →L[ℝ] G
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace H
C : G →L[ℝ] H
hf : Integrable f μ.variation
⊢ ∀ (c : E) ⦃s : Set X⦄,
    MeasurableSet s →
      μ.variation s < ∞ →
        C ∫ᵛ (y : X), s.indicator (fun x ↦ c) y ∂[B; μ] =
          ∫ᵛ (y : X), s.indicator (fun x ↦ c) y ∂[(compL ℝ F G H) C ∘SL B; μ]

Tactic:
intro c

Goal state after:
case h_ind
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
H : Type u_6
mX : MeasurableSpace X
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedAddCommGroup H
μ : VectorMeasure X F
f : X → E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedSpace ℝ G
inst✝² : NormedSpace ℝ H
B : E →L[ℝ] F →L[ℝ] G
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace H
C : G →L[ℝ] H
hf : Integrable f μ.variation
c : E
⊢ ∀ ⦃s : Set X⦄,
    MeasurableSet s →
      μ.variation s < ∞ →
        C ∫ᵛ (y : X), s.indicator (fun x ↦ c) y ∂[B; μ] =
          ∫ᵛ (y : X), s.indicator (fun x ↦ c) y ∂[(compL ℝ F G H) C ∘SL B; μ]
Module: Mathlib.MeasureTheory.VectorMeasure.AddContent

Goal state before:
pp: α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetSemiring C
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : hα = generateFrom C
h''C : ∃ D, D.Countable ∧ D ⊆ C ∧ μ (⋃₀ D)ᶜ = 0
t : Set α
ε : ℝ≥0∞
ht : MeasurableSet t
εpos : 0 < ε
⊢ ∃ s ∈ supClosure C, μ (s ∆ t) < ε

Tactic:
exact exists_measure_symmDiff_lt_of_generateFrom_isSetSemiring hC h''C h'C ht εpos

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.SetIntegral

Goal state before:
pp: case pos.h_ind
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
H : Type u_6
mX : MeasurableSpace X
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedAddCommGroup H
μ : VectorMeasure X F
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace ℝ G
inst✝ : NormedSpace ℝ H
B : E →L[ℝ] F →L[ℝ] G
f : X → H
C : H →L[ℝ] E
hf : Integrable f μ.variation
hG : CompleteSpace G
⊢ ∀ (c : H) ⦃s : Set X⦄,
    MeasurableSet s →
      μ.variation s < ∞ →
        ∫ᵛ (y : X), C (s.indicator (fun x ↦ c) y) ∂[B; μ] = ∫ᵛ (y : X), s.indicator (fun x ↦ c) y ∂[B ∘SL C; μ]

Tactic:
intro c

Goal state after:
case pos.h_ind
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
H : Type u_6
mX : MeasurableSpace X
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedAddCommGroup H
μ : VectorMeasure X F
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace ℝ G
inst✝ : NormedSpace ℝ H
B : E →L[ℝ] F →L[ℝ] G
f : X → H
C : H →L[ℝ] E
hf : Integrable f μ.variation
hG : CompleteSpace G
c : H
⊢ ∀ ⦃s : Set X⦄,
    MeasurableSet s →
      μ.variation s < ∞ →
        ∫ᵛ (y : X), C (s.indicator (fun x ↦ c) y) ∂[B; μ] = ∫ᵛ (y : X), s.indicator (fun x ↦ c) y ∂[B ∘SL C; μ]
Module: Mathlib.MeasureTheory.VectorMeasure.SetIntegral

Goal state before:
pp: case pos
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
μ : VectorMeasure X F
f : X → E
s : Set X
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
C : ℝ≥0∞
hC : ∀ᵐ (x : X) ∂μ.variation.restrict s, ‖f x‖ₑ ≤ C
hs : MeasurableSet s
⊢ ‖∫ᵛ (x : X) in s, f x ∂[B; μ]‖ₑ ≤ C * ‖B‖ₑ * μ.variation s

Tactic:
← variation_restrict hs

Goal state after:
case pos
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
μ : VectorMeasure X F
f : X → E
s : Set X
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
C : ℝ≥0∞
hC : ∀ᵐ (x : X) ∂(μ.restrict s).variation, ‖f x‖ₑ ≤ C
hs : MeasurableSet s
⊢ ‖∫ᵛ (x : X) in s, f x ∂[B; μ]‖ₑ ≤ C * ‖B‖ₑ * μ.variation s
Module: Mathlib.MeasureTheory.VectorMeasure.SetIntegral

Goal state before:
pp: X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
μ : VectorMeasure X F
f : X → E
s : Set X
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
C : ℝ≥0∞
hC : ∀ x ∈ s, ‖f x‖ₑ ≤ C
⊢ ‖∫ᵛ (x : X) in s, f x ∂[B; μ]‖ₑ ≤ C * ‖B‖ₑ * μ.variation s

Tactic:
by_cases hs : MeasurableSet s; swap
  · simp [setIntegral_eq_zero_of_not_measurableSet hs]
  apply enorm_setIntegral_le_of_enorm_le_const_ae
  apply (ae_restrict_iff' hs).2
  filter_upwards with x using hC x

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.SetIntegral

Goal state before:
pp: case pos
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
μ : VectorMeasure X F
f : X → E
s : Set X
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
C : ℝ
h : IsFiniteMeasure (μ.variation.restrict s)
hC : ∀ᵐ (x : X) ∂μ.variation.restrict s, ‖f x‖ ≤ C
hs : MeasurableSet s
⊢ ‖∫ᵛ (x : X) in s, f x ∂[B; μ]‖ ≤ C * ‖B‖ * μ.variation.real s

Tactic:
← variation_restrict hs

Goal state after:
case pos
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
μ : VectorMeasure X F
f : X → E
s : Set X
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
C : ℝ
h : IsFiniteMeasure (μ.restrict s).variation
hC : ∀ᵐ (x : X) ∂(μ.restrict s).variation, ‖f x‖ ≤ C
hs : MeasurableSet s
⊢ ‖∫ᵛ (x : X) in s, f x ∂[B; μ]‖ ≤ C * ‖B‖ * μ.variation.real s
Module: Mathlib.MeasureTheory.VectorMeasure.SetIntegral

Goal state before:
pp: X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
μ : VectorMeasure X F
f : X → E
s : Set X
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
⊢ ‖∫ᵛ (x : X) in s, f x ∂[B; μ]‖ₑ ≤ ∫⁻ (x : X) in s, ‖f x‖ₑ ∂(μ.transpose B).variation

Tactic:
by
  grw [enorm_integral_le_lintegral_enorm_transpose, transpose_restrict,variation_restrict_le]

Goal state after:
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
s : Set M
F : Type u_6
inst✝¹ : EquivLike F M N
inst✝ : AddEquivClass F M N
f : F
h : IsSemilinearSet (⇑f '' s)
⊢ s = ⇑(↑f).symm '' ⇑f '' s

Tactic:
simp [image_image]

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.SetIntegral

Goal state before:
pp: X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
μ : VectorMeasure X F
f : X → E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
ι : Type u_7
hf : μ.Integrable f
l : Filter ι
s : ι → Set X
hs : Tendsto (⇑μ.variation ∘ s) l (𝓝 0)
this : Tendsto (fun i ↦ ‖B‖ₑ * ∫⁻ (x : X) in s i, ‖f x‖ₑ ∂μ.variation) l (𝓝 (‖B‖ₑ * 0))
⊢ Tendsto (fun a ↦ ↑‖∫ᵛ (x : X) in s a, f x ∂[B; μ]‖₊) l (𝓝 0)

Tactic:
mul_zero

Goal state after:
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
μ : VectorMeasure X F
f : X → E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
ι : Type u_7
hf : μ.Integrable f
l : Filter ι
s : ι → Set X
hs : Tendsto (⇑μ.variation ∘ s) l (𝓝 0)
this : Tendsto (fun i ↦ ‖B‖ₑ * ∫⁻ (x : X) in s i, ‖f x‖ₑ ∂μ.variation) l (𝓝 0)
⊢ Tendsto (fun a ↦ ↑‖∫ᵛ (x : X) in s a, f x ∂[B; μ]‖₊) l (𝓝 0)
Module: Mathlib.MeasureTheory.VectorMeasure.SetIntegral

Goal state before:
pp: X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
μ : VectorMeasure X F
f : X → E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
ι : Type u_7
hf : μ.Integrable f
l : Filter ι
s : ι → Set X
hs : Tendsto (⇑μ.variation ∘ s) l (𝓝 0)
this : Tendsto (fun i ↦ ‖B‖ₑ * ∫⁻ (x : X) in s i, ‖f x‖ₑ ∂μ.variation) l (𝓝 0)
⊢ Tendsto (fun a ↦ ↑‖∫ᵛ (x : X) in s a, f x ∂[B; μ]‖₊) l (𝓝 0)

Tactic:
apply tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds this (fun i ↦ zero_le)

Goal state after:
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
μ : VectorMeasure X F
f : X → E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
ι : Type u_7
hf : μ.Integrable f
l : Filter ι
s : ι → Set X
hs : Tendsto (⇑μ.variation ∘ s) l (𝓝 0)
this : Tendsto (fun i ↦ ‖B‖ₑ * ∫⁻ (x : X) in s i, ‖f x‖ₑ ∂μ.variation) l (𝓝 0)
⊢ (fun a ↦ ↑‖∫ᵛ (x : X) in s a, f x ∂[B; μ]‖₊) ≤ fun i ↦ ‖B‖ₑ * ∫⁻ (x : X) in s i, ‖f x‖ₑ ∂μ.variation
Module: Mathlib.MeasureTheory.VectorMeasure.Integral

Goal state before:
pp: X : Type u_2
E : Type u_4
F : Type u_5
G : Type u_6
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
f : X → E
B : E →L[ℝ] F →L[ℝ] G
inst✝¹ : MeasurableSpace X
inst✝ : CompleteSpace G
a : X
v : F
hfm : StronglyMeasurable f
⊢ ∫ᵛ (x : X), f x ∂[B; dirac a v] = (B (f a)) v

Tactic:
borelize E
  have : IsFiniteMeasure ((dirac a v).transpose B).variation := by
    have : ‖B.flip v‖ₑ • Measure.dirac a = ‖B.flip v‖₊ • Measure.dirac a := rfl
    simp only [transpose_dirac, variation_dirac, this]
    infer_instance
  calc
    ∫ᵛ x, f x ∂[B; VectorMeasure.dirac a v] = ∫ᵛ _, f a ∂[B; VectorMeasure.dirac a v] := by
      apply integral_congr_ae
      simp only [variation_dirac]
      exact Measure.ae_smul_measure (ae_eq_dirac' hfm.measurable) _
    _ = B (f a) v := by simp

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

Goal state before:
pp: case neg
X : Type u_2
E : Type u_4
F : Type u_5
G : Type u_6
mX : MeasurableSpace X
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
β : Type u_9
inst✝ : MeasurableSpace β
φ : X → β
hφ : MeasurableEmbedding φ
f : β → E
hfm : AEStronglyMeasurable f (Measure.map φ μ.variation)
h'fm : ¬μ.Integrable (f ∘ φ)
⊢ ¬(μ.map φ).Integrable f

Tactic:
rwa [hφ.integrable_map_vectorMeasure]

Goal state after:
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: L : Language
G' : ℕ → Type w
inst✝ : (i : ℕ) → L.Structure (G' i)
f' : (n : ℕ) → G' n ↪[L] G' (n + 1)
m n : ℕ
h : m ≤ n
⊢ ⇑(natLERec f' m n h) = fun a ↦ Nat.leRecOn h (fun k ↦ ⇑(f' k)) a

Tactic:
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le h

Goal state after:
L : Language
G' : ℕ → Type w
inst✝ : (i : ℕ) → L.Structure (G' i)
f' : (n : ℕ) → G' n ↪[L] G' (n + 1)
m k : ℕ
h : m ≤ m + k
⊢ ⇑(natLERec f' m (m + k) h) = fun a ↦ Nat.leRecOn h (fun k ↦ ⇑(f' k)) a
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: L : Language
ι : Type v
inst✝⁴ : Preorder ι
G : ι → Type w
inst✝³ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝² : IsDirectedOrder ι
inst✝¹ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝ : Nonempty ι
i j : ι
hij : i ≤ j
x : G i
⊢ (setoid G f) (Structure.Sigma.mk f j ((f i j hij) x)) (Structure.Sigma.mk f i x)

Tactic:
refine Setoid.symm ⟨j, hij, refl j, ?_⟩

Goal state after:
L : Language
ι : Type v
inst✝⁴ : Preorder ι
G : ι → Type w
inst✝³ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝² : IsDirectedOrder ι
inst✝¹ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝ : Nonempty ι
i j : ι
hij : i ≤ j
x : G i
⊢ (f i j hij) x = (f j j ⋯) ((f i j hij) x)
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
f : (ι → ℕ) → ℕ
x : ι → ℕ
i : ↑hs.basisSet
⊢ ⌊(hs.basis.repr (toRatVec x - toRatVec hs.base + toRatVec (∑ j, f ↑j • ↑j))) i⌋ =
    ⌊(hs.basis.repr (toRatVec x - toRatVec hs.base)) i⌋ + ↑(f ↑i)

Tactic:
← Finset.sum_coe_sort

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
f : (ι → ℕ) → ℕ
x : ι → ℕ
i : ↑hs.basisSet
⊢ ⌊(hs.basis.repr (toRatVec x - toRatVec hs.base + toRatVec (∑ i, f ↑↑i • ↑↑i))) i⌋ =
    ⌊(hs.basis.repr (toRatVec x - toRatVec hs.base)) i⌋ + ↑(f ↑i)
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: case mp
L : Language
ι : Type w
inst✝⁴ : Preorder ι
inst✝³ : IsDirectedOrder ι
inst✝² : Nonempty ι
G : ι → Type (max w w')
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
M : Bundled L.Structure
⊢ M ∈ L.age (DirectLimit G f) → ∃ i, M ∈ L.age (G i)

Tactic:
rintro ⟨Mfg, ⟨e⟩⟩
    obtain ⟨s, hs⟩ := Mfg.range e.toHom
    let out := @Quotient.out _ (DirectLimit.setoid G f)
    obtain ⟨i, hi⟩ := Finset.exists_le (s.image (Sigma.fst ∘ out))
    have e' := (DirectLimit.of L ι G f i).equivRange.symm.toEmbedding
    refine ⟨i, Mfg, ⟨e'.comp ((Substructure.inclusion ?_).comp e.equivRange.toEmbedding)⟩⟩
    rw [← hs, closure_le]
    intro x hx
    refine ⟨f (out x).1 i (hi (out x).1 (Finset.mem_image_of_mem _ hx)) (out x).2, ?_⟩
    rw [Embedding.coe_toHom, DirectLimit.of_apply, @Quotient.mk_eq_iff_out _ (_),
      DirectLimit.equiv_iff G f (le_refl _) (hi (out x).1 (Finset.mem_image_of_mem _ hx)),
      DirectedSystem.map_self]

Goal state after:
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: L : Language
K : Set (Bundled L.Structure)
hn : K.Nonempty
hc : (Quotient.mk' '' K).Countable
fg : ∀ M ∈ K, Structure.FG L ↑M
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient equivSetoid
hF : Quotient.mk' '' K = range F
⊢ ∃ M, Structure.CG L ↑M ∧ L.age ↑M = K

Tactic:
simp only [Set.ext_iff, Quotient.forall, mem_image, mem_range] at hF

Goal state after:
L : Language
K : Set (Bundled L.Structure)
hn : K.Nonempty
hc : (Quotient.mk' '' K).Countable
fg : ∀ M ∈ K, Structure.FG L ↑M
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient equivSetoid
hF : ∀ (a : Bundled L.Structure), (∃ x ∈ K, Quotient.mk' x = ⟦a⟧) ↔ ∃ y, F y = ⟦a⟧
⊢ ∃ M, Structure.CG L ↑M ∧ L.age ↑M = K
Module: Mathlib.Order.CountableDenseLinearOrder

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ b, (a, b) ∈ ↑f
this : ∀ x ∈ Finset.image Prod.snd ({p ∈ ↑f | p.1 < a}), ∀ y ∈ Finset.image Prod.snd ({p ∈ ↑f | a < p.1}), x < y
b : β
hb : (∀ x ∈ Finset.image Prod.snd ({p ∈ ↑f | p.1 < a}), x < b) ∧ ∀ y ∈ Finset.image Prod.snd ({p ∈ ↑f | a < p.1}), b < y
⊢ ∀ p ∈ ↑f, cmp p.1 a = cmp p.2 b

Tactic:
rintro ⟨p1, p2⟩ hp

Goal state after:
case h
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ b, (a, b) ∈ ↑f
this : ∀ x ∈ Finset.image Prod.snd ({p ∈ ↑f | p.1 < a}), ∀ y ∈ Finset.image Prod.snd ({p ∈ ↑f | a < p.1}), x < y
b : β
hb : (∀ x ∈ Finset.image Prod.snd ({p ∈ ↑f | p.1 < a}), x < b) ∧ ∀ y ∈ Finset.image Prod.snd ({p ∈ ↑f | a < p.1}), b < y
p1 : α
p2 : β
hp : (p1, p2) ∈ ↑f
⊢ cmp (p1, p2).1 a = cmp (p1, p2).2 b
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc a b) volume
t₁ t₂ : ℝ
n : ℕ
h : t₁ ≤ t₂
h₁ : ↑n ≤ t₁
h₂ : t₂ ≤ ↑n + 1
h₃ : a ≤ t₁
h₄ : t₂ ≤ b
h_inc₁ : Ι t₁ t₂ ⊆ Set.Icc (↑n) (↑n + 1)
h_inc₂ : [[t₁, t₂]] ⊆ Set.Icc a b
⊢ Set.Icc t₁ t₂ ⊆ Set.Icc a b

Tactic:
rwa [← Set.uIcc_of_le h]

Goal state after:
Module: Mathlib.NumberTheory.Basic

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommRing R
p : ℕ
a b : R
k : ℕ
ih : ↑p ^ (k + 1) ∣ a ^ p ^ k - b ^ p ^ k
f : R →+* R ⧸ span {↑p} := mk (span {↑p})
h : f (a - b) = 0
hf : ∀ (r : R), ↑p ∣ r ↔ f r = 0
⊢ ↑p ∣ ∑ i ∈ Finset.range p, (a ^ p ^ k) ^ i * (b ^ p ^ k) ^ (p - 1 - i)

Tactic:
map_sub,

Goal state after:
case succ
R : Type u_1
inst✝ : CommRing R
p : ℕ
a b : R
k : ℕ
ih : ↑p ^ (k + 1) ∣ a ^ p ^ k - b ^ p ^ k
f : R →+* R ⧸ span {↑p} := mk (span {↑p})
h : f a - f b = 0
hf : ∀ (r : R), ↑p ∣ r ↔ f r = 0
⊢ ↑p ∣ ∑ i ∈ Finset.range p, (a ^ p ^ k) ^ i * (b ^ p ^ k) ^ (p - 1 - i)
Module: Mathlib.RingTheory.PowerSeries.Exp

Goal state before:
pp: case e_a
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
⊢ (algebraMap ℚ A) (1 / ↑x ! * (1 / ↑(n - x)!)) = (algebraMap ℚ A) (↑(n.choose x) * (1 / ↑n !))

Tactic:
refine RingHom.congr_arg _ ?_

Goal state after:
case e_a
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
⊢ 1 / ↑x ! * (1 / ↑(n - x)!) = ↑(n.choose x) * (1 / ↑n !)
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n p : ℕ
⊢ (↑p + 1) * ∑ i ∈ range (p + 1), _root_.bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / (↑p + 1) =
    ∑ i ∈ range (p.succ + 1), eval (↑n) ((monomial i) (_root_.bernoulli (p.succ - i) * ↑(p.succ.choose i))) -
      _root_.bernoulli p.succ

Tactic:
← sum_div,

Goal state after:
n p : ℕ
⊢ (↑p + 1) * ((∑ i ∈ range (p + 1), _root_.bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i)) / (↑p + 1)) =
    ∑ i ∈ range (p.succ + 1), eval (↑n) ((monomial i) (_root_.bernoulli (p.succ - i) * ↑(p.succ.choose i))) -
      _root_.bernoulli p.succ
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n : ℕ
h_odd : Odd n
hlt : 1 < n
⊢ (-1) ^ n * 0 = 0

Tactic:
mul_zero

Goal state after:
n : ℕ
h_odd : Odd n
hlt : 1 < n
⊢ 0 = 0
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: case e'_11
x✝ : ℝ
x_large : 512 ≤ x✝
f : ℝ → ℝ := fun x ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3))
h5 : 0 < x✝
x : ℝ
⊢ x ∈ Set.Ioi 0.5 ↔ x ∈ ⇑(2 • LinearMap.id) ⁻¹' Set.Ioi 1

Tactic:
simp only [Set.mem_Ioi, Set.mem_preimage, LinearMap.smul_apply,
        LinearMap.id_coe, id_eq, smul_eq_mul]

Goal state after:
case e'_11
x✝ : ℝ
x_large : 512 ≤ x✝
f : ℝ → ℝ := fun x ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3))
h5 : 0 < x✝
x : ℝ
⊢ 0.5 < x ↔ 1 < 2 * x
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: case refine_2.hx
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := ⋯
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : √(2 * 512) = 32
⊢ 1 ≤ 2

pp: case refine_2.hyz
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := ⋯
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : √(2 * 512) = 32
⊢ ↑(9 + 10 * 32) ≤ 2 * (512 / 3)

pp: case refine_2.hx
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun x ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : √(2 * 512) = 32
⊢ 0 ≤ 2

Tactic:
all_goals norm_num1

Goal state after: