mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule

Goal state before:
pp: f : ℝ → ℝ
a b : ℝ
h_df : DifferentiableOn ℝ f [[a, b]]
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f [[a, b]]) [[a, b]]
ζ : ℝ
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f [[a, b]] x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
⊢ |trapezoidal_error f N a b| ≤ |b - a| ^ 3 * ζ / (12 * ↑N ^ 2)

Tactic:
rcases lt_trichotomy a b with h_lt | h_eq | h_gt

Goal state after:
case inl
f : ℝ → ℝ
a b : ℝ
h_df : DifferentiableOn ℝ f [[a, b]]
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f [[a, b]]) [[a, b]]
ζ : ℝ
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f [[a, b]] x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h_lt : a < b
⊢ |trapezoidal_error f N a b| ≤ |b - a| ^ 3 * ζ / (12 * ↑N ^ 2)

case inr.inl
f : ℝ → ℝ
a b : ℝ
h_df : DifferentiableOn ℝ f [[a, b]]
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f [[a, b]]) [[a, b]]
ζ : ℝ
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f [[a, b]] x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h_eq : a = b
⊢ |trapezoidal_error f N a b| ≤ |b - a| ^ 3 * ζ / (12 * ↑N ^ 2)

case inr.inr
f : ℝ → ℝ
a b : ℝ
h_df : DifferentiableOn ℝ f [[a, b]]
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f [[a, b]]) [[a, b]]
ζ : ℝ
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f [[a, b]] x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h_gt : b < a
⊢ |trapezoidal_error f N a b| ≤ |b - a| ^ 3 * ζ / (12 * ↑N ^ 2)
Module: Mathlib.MeasureTheory.MeasurableSpace.Invariants

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_2
inst✝ : MeasurableSpace β
fa : α → α
fb : β → β
g : α → β
hg : Measurable g
hfg : Semiconj g fa fb
s : Set β
hs : MeasurableSet s
⊢ g ∘ fa ⁻¹' s = g ⁻¹' s

Tactic:
hfg.comp_eq,

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_2
inst✝ : MeasurableSpace β
fa : α → α
fb : β → β
g : α → β
hg : Measurable g
hfg : Semiconj g fa fb
s : Set β
hs : MeasurableSet s
⊢ fb ∘ g ⁻¹' s = g ⁻¹' s
Module: Mathlib.MeasureTheory.MeasurableSpace.Card

Goal state before:
pp: α : Type u
s : Set (Set α)
i✝¹ i✝ i : Ordinal.{v}
IH : ∀ y < i, y ≤ ω_ 1 → #↑(generateMeasurableRec s y) ≤ max (#↑s) 2 ^ ℵ₀
hi : i ≤ ω_ 1
A : 𝔠 ≤ max (#↑s) 2 ^ ℵ₀
B : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
⊢ Cardinal.lift.{u, v} i.card ≤ Cardinal.lift.{v, u} (max (#↑s) 2) ^ Cardinal.lift.{v, u} ℵ₀

Tactic:
lift_aleph0

Goal state after:
α : Type u
s : Set (Set α)
i✝¹ i✝ i : Ordinal.{v}
IH : ∀ y < i, y ≤ ω_ 1 → #↑(generateMeasurableRec s y) ≤ max (#↑s) 2 ^ ℵ₀
hi : i ≤ ω_ 1
A : 𝔠 ≤ max (#↑s) 2 ^ ℵ₀
B : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
⊢ Cardinal.lift.{u, v} i.card ≤ Cardinal.lift.{v, u} (max (#↑s) 2) ^ ℵ₀
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real

Goal state before:
pp: X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst✝ : LocallyCompactSpace X
f : X →C_c ℝ
μ : Measure X := rieszMeasure Λ
K : Set X := tsupport ⇑f
ε : ℝ
hε : 0 < ε
a b : ℝ
hab : a < b ∧ range ⇑f ⊆ Ioo a b
N : ℕ
hN : 0 < N
ε' : ℝ := (b - a) / ↑N
hε' : 0 < ε' ∧ ε' * (2 * μ.real K + |a| + b + ε') ≤ ε
E : Fin N → Set X
hE :
  tsupport ⇑f = ⋃ j, E j ∧
    univ.PairwiseDisjoint E ∧
      (∀ (n : Fin N), ∀ x ∈ E n, a + ε' * ↑↑n < f x ∧ f x ≤ a + ε' * (↑↑n + 1)) ∧ ∀ (n : Fin N), MeasurableSet (E n)
y : Fin N → ℝ := fun n ↦ a + ε' * (↑↑n + 1)
hE' : ∀ (n : Fin N), μ (E n) ≠ ∞
h_ε' : 0 < ε' / ↑N
h : ∀ (n : Fin N), ∀ x ∈ E n, f x < a + ε' * (↑↑n + 1) + ε'
h' : ∀ (n : Fin N), (rieszContent (toNNRealLinear Λ)).outerMeasure (E n) ≠ ∞
V : Fin N → Opens X
hV :
  ∀ (n : Fin N),
    E n ⊆ ↑(V n) ∧
      (∀ x ∈ V n, f x < a + ε' * (↑↑n + 1) + ε') ∧
        (rieszContent (toNNRealLinear Λ)).measure ↑(V n) ≤
          (rieszContent (toNNRealLinear Λ)).measure (E n) + ENNReal.ofReal (ε' / ↑N)
⊢ ∃ V, ∀ (n : Fin N), E n ⊆ ↑(V n) ∧ (∀ x ∈ V n, f x < y n + ε') ∧ μ ↑(V n) ≤ μ (E n) + ENNReal.ofReal (ε' / ↑N)

Tactic:
exact ⟨V, hV⟩

Goal state after:
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: ι : Type u_6
inst✝⁷ : Fintype ι
E : ι → Type u_7
inst✝⁶ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁵ : (i : ι) → InnerProductSpace ℝ (E i)
mE : (i : ι) → MeasurableSpace (E i)
inst✝⁴ : ∀ (i : ι), CompleteSpace (E i)
inst✝³ : ∀ (i : ι), SecondCountableTopology (E i)
inst✝² : ∀ (i : ι), BorelSpace (E i)
μ : (i : ι) → Measure (E i)
ν : Measure ((i : ι) → E i)
inst✝¹ : ∀ (i : ι), IsFiniteMeasure (μ i)
inst✝ : IsFiniteMeasure ν
h : ∀ (t : WithLp 2 ((i : ι) → E i)), charFun (Measure.map (toLp 2) ν) t = ∏ i, charFun (μ i) (t.ofLp i)
t : WithLp 2 ((i : ι) → E i)
⊢ ∏ i, charFun (μ i) (t.ofLp i) = charFun (Measure.map (toLp 2) (Measure.pi μ)) t

Tactic:
charFun_pi

Goal state after:
ι : Type u_6
inst✝⁷ : Fintype ι
E : ι → Type u_7
inst✝⁶ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁵ : (i : ι) → InnerProductSpace ℝ (E i)
mE : (i : ι) → MeasurableSpace (E i)
inst✝⁴ : ∀ (i : ι), CompleteSpace (E i)
inst✝³ : ∀ (i : ι), SecondCountableTopology (E i)
inst✝² : ∀ (i : ι), BorelSpace (E i)
μ : (i : ι) → Measure (E i)
ν : Measure ((i : ι) → E i)
inst✝¹ : ∀ (i : ι), IsFiniteMeasure (μ i)
inst✝ : IsFiniteMeasure ν
h : ∀ (t : WithLp 2 ((i : ι) → E i)), charFun (Measure.map (toLp 2) ν) t = ∏ i, charFun (μ i) (t.ofLp i)
t : WithLp 2 ((i : ι) → E i)
⊢ ∏ i, charFun (μ i) (t.ofLp i) = ∏ i, charFun (μ i) (t.ofLp i)
Module: Mathlib.Topology.Separation.CompletelyRegular

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : T35Space X
x y : X
x_ne_y : x ≠ y
f : X → ↑I
f_cont : Continuous[inst✝¹, _] f
f_zero : f x = 0
f_one : EqOn f 1 {y}
⊢ ∃ f ∈ {f | Continuous[inst✝¹, _] f}, f x ≠ f y

Tactic:
exact ⟨fun x ↦ f x, continuous_subtype_val.comp f_cont, by simp_all⟩

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

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace Ω
μ ν : Measure Ω
c : ℝ≥0∞
h : levyProkhorovEDist μ ν < c
B : Set Ω
B_mble : MeasurableSet B
⊢ ν B ≤ μ (thickening c.toReal B) + c

Tactic:
obtain ⟨c', ⟨hc', lt_c⟩⟩ := sInf_lt_iff.mp h
  exact meas_le_of_le_of_forall_le_meas_thickening_add ν μ lt_c.le (hc' B B_mble).2

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

Goal state before:
pp: Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᵐ[μ] ⇑f
key : (fun t ↦ μ.real {a | t ≤ f a}) ≤ fun t ↦ ν.real (thickening ε {a | t ≤ f a}) + ε
intble₁ : IntegrableOn (fun t ↦ μ.real {a | t ≤ f a}) (Ioc 0 ‖f‖) volume
intble₂ : IntegrableOn (fun t ↦ ν.real (thickening ε {a | t ≤ f a})) (Ioc 0 ‖f‖) volume
⊢ IntegrableOn (fun t ↦ ν.real (thickening ε {a | t ≤ f a}) + ε) (Ioc 0 ‖f‖) volume

Tactic:
· exact intble₂.add <| integrable_const ε

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

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst✝¹⁸ : Group A
inst✝¹⁷ : Group B
inst✝¹⁶ : Group C
inst✝¹⁵ : TopologicalSpace A
inst✝¹⁴ : TopologicalSpace B
inst✝¹³ : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst✝¹² : IsTopologicalGroup A
inst✝¹¹ : IsTopologicalGroup B
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : MeasurableSpace A
inst✝⁸ : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : IsTopologicalGroup C
inst✝⁵ : LocallyCompactSpace B
inst✝⁴ : MeasurableSpace C
inst✝³ : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
inst✝² : T2Space B
inst✝¹ : MeasurableSpace B
inst✝ : BorelSpace B
U : Set B
hU : IsOpen U
b : B
hb✝ : b ∈ U
K : Set B
hK : IsCompact K
hb : b ∈ interior K
hKU : K ⊆ U
f : C(B, ℝ)
hf1 : Set.EqOn (⇑f) 1 K
hf2 : IsCompact (tsupport ⇑f)
hf3 : tsupport ⇑f ⊆ U
hf4 : ∀ (x : B), f x ∈ Set.Icc 0 1
⊢ 0 ≤ (H.pushforward μA) { toContinuousMap := f, hasCompactSupport' := hf2 }

Tactic:
← map_zero (H.pushforward μA)

Goal state after:
A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst✝¹⁸ : Group A
inst✝¹⁷ : Group B
inst✝¹⁶ : Group C
inst✝¹⁵ : TopologicalSpace A
inst✝¹⁴ : TopologicalSpace B
inst✝¹³ : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst✝¹² : IsTopologicalGroup A
inst✝¹¹ : IsTopologicalGroup B
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : MeasurableSpace A
inst✝⁸ : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : IsTopologicalGroup C
inst✝⁵ : LocallyCompactSpace B
inst✝⁴ : MeasurableSpace C
inst✝³ : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
inst✝² : T2Space B
inst✝¹ : MeasurableSpace B
inst✝ : BorelSpace B
U : Set B
hU : IsOpen U
b : B
hb✝ : b ∈ U
K : Set B
hK : IsCompact K
hb : b ∈ interior K
hKU : K ⊆ U
f : C(B, ℝ)
hf1 : Set.EqOn (⇑f) 1 K
hf2 : IsCompact (tsupport ⇑f)
hf3 : tsupport ⇑f ⊆ U
hf4 : ∀ (x : B), f x ∈ Set.Icc 0 1
⊢ (H.pushforward μA) 0 ≤ (H.pushforward μA) { toContinuousMap := f, hasCompactSupport' := hf2 }
Module: Mathlib.MeasureTheory.Measure.IntegralCharFun

Goal state before:
pp: case e_s
μ : Measure ℝ
r : ℝ
inst✝ : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (fun x ↦ sinc (r * x)) μ
x : ℝ
⊢ x ∈ {x | r < |x|} ↔ x ∈ {x | 2 < |2 * r⁻¹ * x|}

Tactic:
simp only [Set.mem_ofPred_eq, abs_mul, Nat.abs_ofNat]

Goal state after:
case e_s
μ : Measure ℝ
r : ℝ
inst✝ : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (fun x ↦ sinc (r * x)) μ
x : ℝ
⊢ r < |x| ↔ 2 < 2 * |r⁻¹| * |x|
Module: Mathlib.MeasureTheory.Measure.Prokhorov

Goal state before:
pp: E : Type u_1
inst✝⁴ : MeasurableSpace E
inst✝³ : TopologicalSpace E
inst✝² : T2Space E
inst✝¹ : BorelSpace E
inst✝ : CompactSpace E
C : ℝ≥0
this : {μ | μ.mass = C} = {μ | μ.mass ≤ C} ∩ {μ | μ.mass = C}
⊢ IsCompact ({μ | μ.mass ≤ C} ∩ {μ | μ.mass = C})

Tactic:
apply IsCompact.inter_right (isCompact_setOfPred_finiteMeasure_le_of_compactSpace E C)

Goal state after:
E : Type u_1
inst✝⁴ : MeasurableSpace E
inst✝³ : TopologicalSpace E
inst✝² : T2Space E
inst✝¹ : BorelSpace E
inst✝ : CompactSpace E
C : ℝ≥0
this : {μ | μ.mass = C} = {μ | μ.mass ≤ C} ∩ {μ | μ.mass = C}
⊢ IsClosed[FiniteMeasure.instTopologicalSpace] {μ | μ.mass = C}
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
a b c : E
s : Set E
ω : E → E →L[𝕜] F
dω : E → E →L[ℝ] E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ x ∈ s, HasFDerivWithinAt ω (dω x) s x
hdω : ∀ a ∈ s, ∀ x ∈ tangentConeAt ℝ s a, ∀ y ∈ tangentConeAt ℝ s a, ((dω a) x) y = ((dω a) y) x
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
φ : (↑(Path.segment a b)).Homotopy ↑(Path.segment a c) :=
  ContinuousMap.Homotopy.affine ↑(Path.segment a b) ↑(Path.segment a c)
⊢ range ⇑φ ⊆ s

Tactic:
rw [range_subset_iff]

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
a b c : E
s : Set E
ω : E → E →L[𝕜] F
dω : E → E →L[ℝ] E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ x ∈ s, HasFDerivWithinAt ω (dω x) s x
hdω : ∀ a ∈ s, ∀ x ∈ tangentConeAt ℝ s a, ∀ y ∈ tangentConeAt ℝ s a, ((dω a) x) y = ((dω a) y) x
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
φ : (↑(Path.segment a b)).Homotopy ↑(Path.segment a c) :=
  ContinuousMap.Homotopy.affine ↑(Path.segment a b) ↑(Path.segment a c)
⊢ ∀ (y : ↑I × ↑I), φ y ∈ s
Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

Goal state before:
pp: ι : Type u_1
inst✝¹ : Nonempty ι
inst✝ : Fintype ι
x : EuclideanSpace ℝ ι
r : ℝ
hr : 0 ≤ r
this : volume (Metric.ball 0 1) = ENNReal.ofReal (√π ^ card ι / Gamma (↑(card ι) / 2 + 1))
⊢ ENNReal.ofReal r ^ Module.finrank ℝ (EuclideanSpace ℝ ι) * ENNReal.ofReal (√π ^ card ι / Gamma (↑(card ι) / 2 + 1)) =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (↑(card ι) / 2 + 1))

Tactic:
finrank_euclideanSpace

Goal state after:
ι : Type u_1
inst✝¹ : Nonempty ι
inst✝ : Fintype ι
x : EuclideanSpace ℝ ι
r : ℝ
hr : 0 ≤ r
this : volume (Metric.ball 0 1) = ENNReal.ofReal (√π ^ card ι / Gamma (↑(card ι) / 2 + 1))
⊢ ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (↑(card ι) / 2 + 1)) =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (↑(card ι) / 2 + 1))
Module: Mathlib.MeasureTheory.Measure.LevyConvergence

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : ℕ → Measure E
inst✝ : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun n ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
n : ℕ
r : ℝ
hr : 0 < r
hr' : -(2 * r⁻¹) ≤ 2 * r⁻¹
⊢ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖ ≤ 4

Tactic:
calc 2⁻¹ * r * ‖∫ t in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖
    _ ≤ 2⁻¹ * r * ∫ t in -(2 * r⁻¹)..2 * r⁻¹, ‖1 - charFun (μ n) (t • z)‖ := by
      grw [neg_mul, intervalIntegral.norm_integral_le_integral_norm hr']
    _ ≤ 2⁻¹ * r * ∫ t in -(2 * r⁻¹)..2 * r⁻¹, 2 := by
      gcongr
      rw [intervalIntegral.integral_of_le hr', intervalIntegral.integral_of_le hr']
      refine integral_mono_of_nonneg ?_ (by fun_prop) ?_
      · exact ae_of_all _ fun _ ↦ by positivity
      · exact ae_of_all _ fun _ ↦ norm_one_sub_charFun_le_two
    _ ≤ 4 := by
      simp only [intervalIntegral.integral_const, sub_neg_eq_add, smul_eq_mul]
      field_simp
      norm_num

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : MeasurableSpace X
μ : Measure X
⊢ μ.support = ⋂₀ {t | IsClosed[inst✝¹] t ∧ μ tᶜ = 0}

Tactic:
by
  convert! congr($(compl_support_eq_sUnion (μ := μ))ᶜ)
  all_goals simp [Set.compl_sUnion, compl_involutive.image_eq_preimage_symm]

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : HereditarilyLindelofSpace 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : MeasurableSpace 𝕜
inst✝³ : BorelSpace 𝕜
inst✝² : RCLike A
inst✝¹ : NormedAlgebra 𝕜 A
μ : Measure 𝕜
inst✝ : IsFiniteMeasure μ
a : A
ha : a ∉ ⇑(algebraMap 𝕜 A) '' μ.support
h : μ.support.Nonempty
this : 0 < infDist a (⇑(algebraMap 𝕜 A) '' μ.support)
s : Set A := ball a (infDist a (⇑(algebraMap 𝕜 A) '' μ.support) / 2)
hs_z : s ∈ 𝓝 a
hs_μ : s ⊆ (⇑(algebraMap 𝕜 A) '' μ.support)ᶜ
⊢ ∀ᶠ (w : A) in 𝓝 a, AEStronglyMeasurable (resolvent w) μ

Tactic:
filter_upwards with _ using by fun_prop

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.OfAddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s✝ : Set α
m : AddContent ℝ≥0∞ C
hC : IsSetSemiring C
m_sigma_subadd : m.IsSigmaSubadditive
this : MeasurableSpace α := (inducedOuterMeasure (fun x x_1 ↦ m x) ⋯ ⋯).caratheodory
s : Set α
hs : s ∈ C
⊢ MeasurableSet s

Tactic:
change (inducedOuterMeasure (fun x _ ↦ m x) hC.empty_mem addContent_empty).IsCaratheodory s

Goal state after:
α : Type u_1
C : Set (Set α)
s✝ : Set α
m : AddContent ℝ≥0∞ C
hC : IsSetSemiring C
m_sigma_subadd : m.IsSigmaSubadditive
this : MeasurableSpace α := (inducedOuterMeasure (fun x x_1 ↦ m x) ⋯ ⋯).caratheodory
s : Set α
hs : s ∈ C
⊢ (inducedOuterMeasure (fun x x_1 ↦ m x) ⋯ ⋯).IsCaratheodory s
Module: Mathlib.MeasureTheory.SpecificCodomains.WithLp

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : Measure X
q : ℝ≥0∞
inst✝⁴ : Fact (1 ≤ q)
ι : Type u_2
inst✝³ : Fintype ι
E : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (E i)
f : X → PiLp q E
inst✝¹ : (i : ι) → NormedSpace ℝ (E i)
inst✝ : ∀ (i : ι), CompleteSpace (E i)
hf : ∀ (i : ι), Integrable (fun x ↦ (f x).ofLp i) μ
i : ι
⊢ (∫ (x : X), f x ∂μ).ofLp i = ∫ (x : X), (f x).ofLp i ∂μ

Tactic:
by
  rw [← PiLp.proj_apply (𝕜 := ℝ) q E i (∫ x, f x ∂μ), ← ContinuousLinearMap.integral_comp_comm]
  · simp
  exact Integrable.of_eval_piLp hf

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic

Goal state before:
pp: case inr
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst✝² : TopologicalSpace V
inst✝¹ : ENormedAddCommMonoid V
inst✝ : T2Space V
μ : VectorMeasure X V
s : Set X
hs : MeasurableSet s
P : Finset (Set X)
hP₁ : ∀ t ∈ P, t ⊆ s
hP₂ : (↑P).PairwiseDisjoint id
Q : Finpartition (P.sup id) := Finpartition.ofPairwiseDisjoint P hP₂
defQ : Q = Finpartition.ofPairwiseDisjoint P hP₂
Q' : Finpartition ((filter MeasurableSet Q.parts).sup id) := Q.ofSubset ⋯ ⋯
defQ' : Q' = Q.ofSubset ⋯ ⋯
hQ' : ∀ t ∈ Q'.parts, t ⊆ s
hp : s \ (filter MeasurableSet Q.parts).sup id ∈ (Q'.extendOfLE ⋯).parts
⊢ MeasurableSet (s \ ⋃ x ∈ filter MeasurableSet Q.parts, x)

Tactic:
exact hs.diff <| .biUnion (Finset.countable_toSet _) (by simp)

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic

Goal state before:
pp: X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst✝³ : TopologicalSpace V
inst✝² : ENormedAddCommMonoid V
inst✝¹ : T2Space V
μ : VectorMeasure X V
Y : Type u_3
inst✝ : MeasurableSpace Y
φ : X → Y
hφ : MeasurableEmbedding φ
s : Set Y
hs : MeasurableSet s
⊢ (μ.map φ).variation s = (μ.map φ).variation (s ∩ Set.range φ)

Tactic:
← inter_union_sdiff s (range φ)

Goal state after:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst✝³ : TopologicalSpace V
inst✝² : ENormedAddCommMonoid V
inst✝¹ : T2Space V
μ : VectorMeasure X V
Y : Type u_3
inst✝ : MeasurableSpace Y
φ : X → Y
hφ : MeasurableEmbedding φ
s : Set Y
hs : MeasurableSet s
⊢ (μ.map φ).variation (s ∩ Set.range φ ∪ s \ Set.range φ) = (μ.map φ).variation (s ∩ Set.range φ)
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 : IsSetRing C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ C, μ (s ∆ t) < ε
C' : Set (MeasuredSets μ) := {s | ∃ c ∈ C, ↑s = c}
C'C : ∀ s ∈ C', ↑s ∈ C
C'_dense : Dense C'
m₀ : ↑C' → E := fun x ↦ m ↑↑x
lip : LipschitzWith 1 m₀
m₁ : MeasuredSets μ → E := C'_dense.extend m₀
m₁_lip : LipschitzWith 1 m₁
hBound : ∀ (s : MeasuredSets μ), ‖m₁ s‖ₑ ≤ μ ↑s
s t : MeasuredSets μ
h : Disjoint ↑s ↑t
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ : 8 * δ = ε
s' : Set α
s'C : s' ∈ C
hs' : μ (s' ∆ ↑s) < δ
t' : Set α
t'C : t' ∈ C
ht' : μ (t' ∆ ↑t) < δ
It : ‖m t' - m₁ t‖ₑ < δ
hμ' : μ (s' ∩ t') < 2 * δ
s'' : Set α := s' \ t'
⊢ ‖m₁ ⟨↑s ∪ ↑t, ⋯⟩ - m₁ s - m₁ t‖ₑ < ε

Tactic:
have s''C : s'' ∈ C := hC.sdiff_mem s'C t'C

Goal state after:
α : 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 : IsSetRing C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ C, μ (s ∆ t) < ε
C' : Set (MeasuredSets μ) := {s | ∃ c ∈ C, ↑s = c}
C'C : ∀ s ∈ C', ↑s ∈ C
C'_dense : Dense C'
m₀ : ↑C' → E := fun x ↦ m ↑↑x
lip : LipschitzWith 1 m₀
m₁ : MeasuredSets μ → E := C'_dense.extend m₀
m₁_lip : LipschitzWith 1 m₁
hBound : ∀ (s : MeasuredSets μ), ‖m₁ s‖ₑ ≤ μ ↑s
s t : MeasuredSets μ
h : Disjoint ↑s ↑t
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ : 8 * δ = ε
s' : Set α
s'C : s' ∈ C
hs' : μ (s' ∆ ↑s) < δ
t' : Set α
t'C : t' ∈ C
ht' : μ (t' ∆ ↑t) < δ
It : ‖m t' - m₁ t‖ₑ < δ
hμ' : μ (s' ∩ t') < 2 * δ
s'' : Set α := s' \ t'
s''C : s'' ∈ C
⊢ ‖m₁ ⟨↑s ∪ ↑t, ⋯⟩ - m₁ s - m₁ t‖ₑ < ε
Module: Mathlib.MeasureTheory.VectorMeasure.SetIntegral

Goal state before:
pp: case pos.h_closed.hf
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
I : ∀ (f : ↥(Lp H 1 μ.variation)), ∫ᵛ (x : X), C (↑↑f x) ∂[B; μ] = ∫ᵛ (x : X), ↑↑(C.compLp f) x ∂[B; μ]
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun y ↦ ∫ᵛ (y_1 : X), C (↑↑y y_1) ∂[B; μ]

Tactic:
I

Goal state after:
case pos.h_closed.hf
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
I : ∀ (f : ↥(Lp H 1 μ.variation)), ∫ᵛ (x : X), C (↑↑f x) ∂[B; μ] = ∫ᵛ (x : X), ↑↑(C.compLp f) x ∂[B; μ]
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun y ↦ ∫ᵛ (x : X), ↑↑(C.compLp y) x ∂[B; μ]
Module: Mathlib.MeasureTheory.VectorMeasure.Prod

Goal state before:
pp: ι : Type u_1
X : Type u_2
Y : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
H : Type u_7
I : Type u_8
J : Type u_9
mX : MeasurableSpace X
mY : MeasurableSpace Y
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
inst✝⁶ : NormedAddCommGroup H
inst✝⁵ : NormedSpace ℝ H
inst✝⁴ : NormedAddCommGroup I
inst✝³ : NormedSpace ℝ I
inst✝² : NormedAddCommGroup J
inst✝¹ : NormedSpace ℝ J
μ✝ : VectorMeasure X E
ν✝ : VectorMeasure Y F
B✝ : E →L[ℝ] F →L[ℝ] G
μ : VectorMeasure X E
ν : VectorMeasure Y F
B : E →L[ℝ] F →L[ℝ] G
inst✝ : IsFiniteMeasure μ.variation
f : ℕ → Set (X × Y)
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Disjoint on f)
⊢ HasSum (fun i ↦ if MeasurableSet (f i) then ∫ᵛ (x : X), ν (Prod.mk x ⁻¹' f i) ∂[B.flip; μ] else 0)
    (if MeasurableSet (⋃ i, f i) then ∫ᵛ (x : X), ν (Prod.mk x ⁻¹' ⋃ i, f i) ∂[B.flip; μ] else 0)

Tactic:
simp only [f_meas, ↓reduceIte, implies_true, MeasurableSet.iUnion, preimage_iUnion,
      HasSum, SummationFilter.unconditional_filter]
    have A (a : Finset ℕ) : ∑ y ∈ a, ∫ᵛ x, ν (Prod.mk x ⁻¹' f y) ∂[B.flip; μ]
        = ∫ᵛ x, ∑ y ∈ a, ν (Prod.mk x ⁻¹' f y) ∂[B.flip; μ] := by
      rw [integral_finsetSum _ (fun i hi ↦ integrable_vectorMeasure_prodMk_left (f_meas i))]
    simp_rw [A]
    apply tendsto_integral_filter_of_dominated_convergence (bound := fun x ↦ ν.bound)
    · apply Eventually.of_forall (fun a ↦ ?_)
      apply StronglyMeasurable.aestronglyMeasurable
      apply Finset.stronglyMeasurable_fun_sum _ (fun i hi ↦ ?_)
      apply stronglyMeasurable_vectorMeasure_prodMk_left (f_meas i)
    · filter_upwards with a
      filter_upwards with x
      rw [← VectorMeasure.of_biUnion_finset]
      · apply norm_apply_le_bound
      · exact fun i hi j hj hij ↦ (f_disj hij).preimage _
      · exact fun i hi ↦ measurable_prodMk_left (f_meas i)
    · apply integrable_const
    · filter_upwards with x
      apply hasSum_of_disjoint_iUnion
      · exact fun i ↦ measurable_prodMk_left (f_meas i)
      · exact fun i j hij ↦ (f_disj hij).preimage _

Goal state after:
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
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
c : ℝ
⊢ (c • μ).transpose B = c • μ.transpose B

Tactic:
simp [transpose, mapRange_smul]

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

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
S₁ : Set (Set M)
hS₁ : S₁.Finite
hS₁' : ∀ t ∈ S₁, IsLinearSet t
S₂ : Set (Set M)
hS₂ : S₂.Finite
hS₂' : ∀ t ∈ S₂, IsLinearSet t
⊢ IsSemilinearSet (⋃₀ S₁ ∪ ⋃₀ S₂)

Tactic:
← sUnion_union

Goal state after:
M : Type u_1
inst✝ : AddCommMonoid M
S₁ : Set (Set M)
hS₁ : S₁.Finite
hS₁' : ∀ t ∈ S₁, IsLinearSet t
S₂ : Set (Set M)
hS₂ : S₂.Finite
hS₂' : ∀ t ∈ S₂, IsLinearSet t
⊢ IsSemilinearSet (⋃₀ (S₁ ∪ S₂))