mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ∞
c : E
hc : c ≠ 0
s : Set α
hs : MeasurableSet s
hcs : MemLp (⇑(piecewise s hs (const α c) (const α 0))) p μ
⊢ μ s < ∞

Tactic:
have : Function.support (const α c) = Set.univ := Function.support_const hc
  simpa only [memLp_iff_finMeasSupp hp_pos hp_ne_top, finMeasSupp_iff_support,
    support_indicator, Set.inter_univ, this] using hcs

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

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
⊢ weightedSMul μ ∅ = 0

Tactic:
ext1 x

Goal state after:
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
x : F
⊢ (weightedSMul μ ∅) x = 0 x
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hμs : μ s ≠ ∞
hνs : ν s ≠ ∞
⊢ weightedSMul (μ + ν) s = weightedSMul μ s + weightedSMul ν s

Tactic:
ext1 x

Goal state after:
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hμs : μ s ≠ ∞
hνs : ν s ≠ ∞
x : F
⊢ (weightedSMul (μ + ν) s) x = (weightedSMul μ s + weightedSMul ν s) x
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
s : Set α
⊢ weightedSMul (c • μ) s = c.toReal • weightedSMul μ s

Tactic:
ext1 x

Goal state after:
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
s : Set α
x : F
⊢ (weightedSMul (c • μ) s) x = (c.toReal • weightedSMul μ s) x
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
s t : Set α
hst : μ s = μ t
⊢ weightedSMul μ s = weightedSMul μ t

Tactic:
ext1 x

Goal state after:
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
s t : Set α
hst : μ s = μ t
x : F
⊢ (weightedSMul μ s) x = (weightedSMul μ t) x
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
s : Set α
h_zero : μ s = 0
⊢ weightedSMul μ s = 0

Tactic:
ext1 x

Goal state after:
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
s : Set α
h_zero : μ s = 0
x : F
⊢ (weightedSMul μ s) x = 0 x
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst✝¹ : NormedAddCommGroup G
inst✝ : PartialOrder G
f : ↥(simpleFunc G p μ)
hf : 0 ≤ f
⊢ ∃ f', 0 ≤ f' ∧ ↑↑↑f =ᵐ[μ] ⇑f'

Tactic:
rcases f with ⟨⟨f, hp⟩, g, (rfl : _ = f)⟩
  change 0 ≤ᵐ[μ] g at hf
  classical
  refine ⟨g.map ({x : G | 0 ≤ x}.piecewise id 0), fun x ↦ ?_, (AEEqFun.coeFn_mk _ _).trans ?_⟩
  · simpa using! Set.indicator_apply_nonneg id
  · filter_upwards [hf] with x (hx : 0 ≤ g x)
    simpa using! Set.indicator_of_mem hx id |>.symm

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

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
s t : Set α
ht : MeasurableSet t
hs_finite : μ s ≠ ∞
ht_finite : μ t ≠ ∞
hdisj : Disjoint s t
⊢ weightedSMul μ (s ∪ t) = weightedSMul μ s + weightedSMul μ t

Tactic:
ext1 x

Goal state after:
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
s t : Set α
ht : MeasurableSet t
hs_finite : μ s ≠ ∞
ht_finite : μ t ≠ ∞
hdisj : Disjoint s t
x : F
⊢ (weightedSMul μ (s ∪ t)) x = (weightedSMul μ s + weightedSMul μ t) x
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: case neg
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : s.Nonempty
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ ⇑(piecewise s hs (const α x) (const α 0)) ⁻¹' {x} = s

Tactic:
simp only [coe_piecewise, piecewise_eq_indicator, coe_const, Function.const_zero,
    piecewise_eq_indicator]

Goal state after:
case neg
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : s.Nonempty
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ s.indicator (Function.const α x) ⁻¹' {x} = s
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
⊢ setToSimpleFunc T (piecewise s hs (const α x) (const α 0)) = (T s) x

Tactic:
obtain rfl | hs_empty := s.eq_empty_or_nonempty
  · simp only [hT_empty, zero_apply, piecewise_empty, const_zero,
      setToSimpleFunc_zero_apply]
  simp_rw [setToSimpleFunc]
  obtain rfl | hs_univ := eq_or_ne s univ
  · have hα := hs_empty.to_type
    simp [← Function.const_def]
  rw [range_indicator hs hs_empty hs_univ]
  by_cases hx0 : x = 0
  · simp_rw [hx0]; simp
  rw [sum_insert]
  swap; · rw [Finset.mem_singleton]; exact hx0
  rw [sum_singleton, (T _).map_zero, add_zero]
  congr
  simp only [coe_piecewise, piecewise_eq_indicator, coe_const, Function.const_zero,
    piecewise_eq_indicator]
  rw [indicator_preimage, ← Function.const_def, preimage_const_of_mem]
  swap; · exact Set.mem_singleton x
  rw [← Function.const_zero, ← Function.const_def, preimage_const_of_notMem]
  swap; · rw [Set.mem_singleton_iff]; exact Ne.symm hx0
  simp

Goal state after:
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
c : β
h✝ : c ≠ 0
h : Tendsto (u - fun x ↦ c) l (𝓝 0)
⊢ Tendsto u l (𝓝 c)

Tactic:
have := h.sub (tendsto_const_nhds (x := -c))

Goal state after:
case mp
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
c : β
h✝ : c ≠ 0
h : Tendsto (u - fun x ↦ c) l (𝓝 0)
this : Tendsto (fun x ↦ (u - fun x ↦ c) x - -c) l (𝓝 (0 - -c))
⊢ Tendsto u l (𝓝 c)
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : Integrable f μ
h_min : ∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ = 0
⊢ (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal - (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ).toReal =
    (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal

Tactic:
h_min,

Goal state after:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : Integrable f μ
h_min : ∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ = 0
⊢ (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal - ENNReal.toReal 0 = (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal
Module: Mathlib.Analysis.Normed.Group.AddTorsor

Goal state before:
pp: V : Type u_2
P : Type u_3
inst✝² : SeminormedAddCommGroup V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ p₄ : P
⊢ dist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) ≤ dist p₁ p₃ + dist p₂ p₄

Tactic:
rw [dist_eq_norm, vsub_sub_vsub_comm, dist_eq_norm_vsub V, dist_eq_norm_vsub V]

Goal state after:
V : Type u_2
P : Type u_3
inst✝² : SeminormedAddCommGroup V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ p₄ : P
⊢ ‖p₁ -ᵥ p₃ - (p₂ -ᵥ p₄)‖ ≤ ‖p₁ -ᵥ p₃‖ + ‖p₂ -ᵥ p₄‖
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: case inr.const
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_ne_top : p ≠ ∞
P : (α → E) → Prop
h0P :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s → μ s < ∞ → ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ g, eLpNorm (g - s.indicator fun x ↦ c) p μ ≤ ε ∧ P g
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f : α → E
hf : MemLp f p μ
ε✝ : ℝ≥0∞
hε : ε✝ ≠ 0
hp_pos : p ≠ 0
c : E
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
εpos : ε ≠ 0
⊢ MemLp (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))) p μ →
    ∃ g, eLpNorm (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) - g) p μ ≤ ε ∧ P g

Tactic:
Hs

Goal state after:
case inr.const
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_ne_top : p ≠ ∞
P : (α → E) → Prop
h0P :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s → μ s < ∞ → ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ g, eLpNorm (g - s.indicator fun x ↦ c) p μ ≤ ε ∧ P g
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f : α → E
hf : MemLp f p μ
ε✝ : ℝ≥0∞
hε : ε✝ ≠ 0
hp_pos : p ≠ 0
c : E
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
εpos : ε ≠ 0
Hs : MemLp (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))) p μ
⊢ ∃ g, eLpNorm (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) - g) p μ ≤ ε ∧ P g
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hμ : NeZero μ
hf : Integrable (fun x ↦ Real.exp (f x)) μ
⊢ (Function.support fun x ↦ Real.exp (f x)) = univ

Tactic:
ext1 x

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hμ : NeZero μ
hf : Integrable (fun x ↦ Real.exp (f x)) μ
x : α
⊢ (x ∈ Function.support fun x ↦ Real.exp (f x)) ↔ x ∈ univ
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case e_f
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] G)
h_eq : ∀ (a : α), (SimpleFunc.map (fun x ↦ ‖x‖ₑ) (toSimpleFunc f)) a = ‖(toSimpleFunc f) a‖ₑ
⊢ (fun a ↦ (‖a‖ₑ * μ (⇑(toSimpleFunc f) ⁻¹' {a})).toReal) = fun x ↦ (μ (⇑(toSimpleFunc f) ⁻¹' {x})).toReal * ‖x‖

Tactic:
ext1 x

Goal state after:
case e_f
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] G)
h_eq : ∀ (a : α), (SimpleFunc.map (fun x ↦ ‖x‖ₑ) (toSimpleFunc f)) a = ‖(toSimpleFunc f) a‖ₑ
x : G
⊢ (‖x‖ₑ * μ (⇑(toSimpleFunc f) ⁻¹' {x})).toReal = (μ (⇑(toSimpleFunc f) ⁻¹' {x})).toReal * ‖x‖
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ μ' : Measure α
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
hμ : μ ≪ μ'
f : ↥(α →₁ₛ[μ] E)
f' : ↥(α →₁ₛ[μ'] E)
h : ↑↑↑f =ᵐ[μ] ↑↑↑f'
⊢ ↑↑↑f' =ᵐ[μ] ⇑(toSimpleFunc f')

Tactic:
have goal' : (f' : α → E) =ᵐ[μ'] simpleFunc.toSimpleFunc f' := (toSimpleFunc_eq_toFun f').symm

Goal state after:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ μ' : Measure α
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
hμ : μ ≪ μ'
f : ↥(α →₁ₛ[μ] E)
f' : ↥(α →₁ₛ[μ'] E)
h : ↑↑↑f =ᵐ[μ] ↑↑↑f'
goal' : ↑↑↑f' =ᵐ[μ'] ⇑(toSimpleFunc f')
⊢ ↑↑↑f' =ᵐ[μ] ⇑(toSimpleFunc f')
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case pos
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
c : ℝ
f : α → E
hF : CompleteSpace F
hf : Integrable f μ
⊢ (L1.setToL1 ⋯) (Integrable.toL1 f hf) = c • (L1.setToL1 hT) (Integrable.toL1 f hf)

Tactic:
L1.setToL1_smul_left hT c

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

Goal state before:
pp: ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
inst✝ : NormedSpace ℝ E
hfi : ∀ (i : ι), Integrable f (μ i)
ε : ℝ≥0
ε0 : 0 < ↑ε
hf_lt : ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < ∞
hmem : ∀ᶠ (y : ℝ≥0∞) in 𝓝 (∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ), ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < y + ↑ε
s : Finset ι
ν : Measure X
hs : ∫⁻ (a : X), ‖f a‖ₑ ∂∑ i ∈ s, μ i + ∫⁻ (a : X), ‖f a‖ₑ ∂ν < ∑ b ∈ s, (fun i ↦ ∫⁻ (a : X), ‖f a‖ₑ ∂μ i) b + ↑ε
hf : Integrable f (∑ i ∈ s, μ i) ∧ Integrable f ν
hν : ∑ i ∈ s, μ i + ν = Measure.sum μ
⊢ ∫⁻ (x : X), ‖f x‖ₑ ∂ν < ↑ε

Tactic:
lintegral_finsetSum_measure

Goal state after:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
inst✝ : NormedSpace ℝ E
hfi : ∀ (i : ι), Integrable f (μ i)
ε : ℝ≥0
ε0 : 0 < ↑ε
hf_lt : ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < ∞
hmem : ∀ᶠ (y : ℝ≥0∞) in 𝓝 (∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ), ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < y + ↑ε
s : Finset ι
ν : Measure X
hs : ∑ i ∈ s, ∫⁻ (a : X), ‖f a‖ₑ ∂μ i + ∫⁻ (a : X), ‖f a‖ₑ ∂ν < ∑ b ∈ s, (fun i ↦ ∫⁻ (a : X), ‖f a‖ₑ ∂μ i) b + ↑ε
hf : Integrable f (∑ i ∈ s, μ i) ∧ Integrable f ν
hν : ∑ i ∈ s, μ i + ν = Measure.sum μ
⊢ ∫⁻ (x : X), ‖f x‖ₑ ∂ν < ↑ε
Module: Mathlib.Topology.Bornology.BoundedOperation

Goal state before:
pp: R : Type u_1
inst✝ : SeminormedAddCommGroup R
x : R
⊢ Tendsto (fun x_1 ↦ x_1 + x) (cobounded R) (cobounded R)

Tactic:
by
  intro s hs
  rw [mem_map]
  rw [← isCobounded_def, ← isBounded_compl_iff] at hs ⊢
  rw [← Set.preimage_compl]
  convert! isBounded_sub hs (t := { x }) isBounded_singleton using 1
  ext y
  simp [sub_eq_iff_eq_add]

Goal state after:
Module: Mathlib.Topology.Bornology.BoundedOperation

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalSeminormedRing R
s t : Set R
hs : ∃ C, ∀ ⦃x : R⦄, x ∈ s → ∀ ⦃y : R⦄, y ∈ s → dist x y ≤ C
ht : ∃ C, ∀ ⦃x : R⦄, x ∈ t → ∀ ⦃y : R⦄, y ∈ t → dist x y ≤ C
Af : ℝ
hAf : s ⊆ Metric.closedBall 0 Af
Ag : ℝ
hAg : t ⊆ Metric.closedBall 0 Ag
z : R
hz : z ∈ s * t
w : R
hw : w ∈ s * t
x₁ : R
hx₁ : x₁ ∈ s
y₁ : R
hy₁ : y₁ ∈ t
z_eq : x₁ * y₁ = z
x₂ : R
hx₂ : x₂ ∈ s
y₂ : R
hy₂ : y₂ ∈ t
w_eq : x₂ * y₂ = w
hAf' : 0 ≤ Af
x y : R
x_in_s : x ∈ s
y_in_t : y ∈ t
⊢ ‖x‖ ≤ Af

Tactic:
exact mem_closedBall_zero_iff.mp (hAf x_in_s)

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

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
hE : CompleteSpace E
inst✝ : MeasurableSpace α
f : α → E
a : α
hfm : StronglyMeasurable f
⊢ ∫ (x : α), f x ∂Measure.dirac a = f a

Tactic:
borelize E
  calc
    ∫ x, f x ∂Measure.dirac a = ∫ _, f a ∂Measure.dirac a :=
      integral_congr_ae <| ae_eq_dirac' hfm.measurable
    _ = f a := by simp

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

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
hE : CompleteSpace E
inst✝ : MeasurableSpace α
f : α → E
a : α
hfm : StronglyMeasurable f
⊢ ∫ (x : α), f x ∂Measure.dirac a = f a

Tactic:
by
  borelize E
  calc
    ∫ x, f x ∂Measure.dirac a = ∫ _, f a ∂Measure.dirac a :=
      integral_congr_ae <| ae_eq_dirac' hfm.measurable
    _ = f a := by simp

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: case refine_2
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
δ : Type u_2
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : α
⊢ dist ((extend f g₁ h₁) (f x)) (g₂ x) ≤ dist (extend f g₁ h₁) (extend f g₂ h₂)

Tactic:
← extend_apply f g₂ h₂

Goal state after:
case refine_2
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
δ : Type u_2
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : α
⊢ dist ((extend f g₁ h₁) (f x)) ((extend f g₂ h₂) (f x)) ≤ dist (extend f g₁ h₁) (extend f g₂ h₂)
Module: Mathlib.Topology.ContinuousMap.Compact

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : LocallyCompactSpace X
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
ι : Type u_3
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable fun i ↦ ‖restrict (↑K) (F i)‖
K : Compacts X
s : Finset ι
⊢ restrict (↑K) (∑ i ∈ s, F i) = ∑ i ∈ s, restrict (↑K) (F i)

Tactic:
ext1 x

Goal state after:
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : LocallyCompactSpace X
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
ι : Type u_3
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable fun i ↦ ‖restrict (↑K) (F i)‖
K : Compacts X
s : Finset ι
x : ↑↑K
⊢ (restrict (↑K) (∑ i ∈ s, F i)) x = (∑ i ∈ s, restrict (↑K) (F i)) x
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case pos.refine_1
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hr : r = 0
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ 0
hnegf : ∫ (x : α), -f x ∂μ = 0
⊢ 0 ≤ᵐ[μ] -f

Tactic:
· filter_upwards [hf] with ω hω
      rwa [Pi.zero_apply, Pi.neg_apply, Right.nonneg_neg_iff]

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

Goal state before:
pp: δ : Type u_1
X : δ → Type u_3
inst✝¹ : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝ : DecidableEq δ
f : ((i : δ) → X i) → ℝ≥0∞
⊢ ∫⋯∫⁻_∅, f ∂μ = f

Tactic:
ext1 x

Goal state after:
δ : Type u_1
X : δ → Type u_3
inst✝¹ : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝ : DecidableEq δ
f : ((i : δ) → X i) → ℝ≥0∞
x : (i : δ) → X i
⊢ (∫⋯∫⁻_∅, f ∂μ) x = f x
Module: Mathlib.MeasureTheory.Integral.Marginal

Goal state before:
pp: δ : Type u_1
X : δ → Type u_3
inst✝¹ : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝ : DecidableEq δ
f : ((i : δ) → X i) → ℝ≥0∞
i : δ
α : Type u_1 := ↥{i}
e : X ↑default ≃ᵐ ((i_1 : α) → X ↑i_1) := (MeasurableEquiv.piUnique fun j ↦ X ↑j).symm
⊢ ∫⋯∫⁻_{i}, f ∂μ = fun x ↦ ∫⁻ (xᵢ : X i), f (update x i xᵢ) ∂μ i

Tactic:
ext1 x

Goal state after:
δ : Type u_1
X : δ → Type u_3
inst✝¹ : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝ : DecidableEq δ
f : ((i : δ) → X i) → ℝ≥0∞
i : δ
α : Type u_1 := ↥{i}
e : X ↑default ≃ᵐ ((i_1 : α) → X ↑i_1) := (MeasurableEquiv.piUnique fun j ↦ X ↑j).symm
x : (i : δ) → X i
⊢ (∫⋯∫⁻_{i}, f ∂μ) x = ∫⁻ (xᵢ : X i), f (update x i xᵢ) ∂μ i
Module: Mathlib.MeasureTheory.Integral.Marginal

Goal state before:
pp: δ : Type u_1
X : δ → Type u_3
inst✝² : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝¹ : DecidableEq δ
s t : Finset δ
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
f : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
hst : Disjoint s t
⊢ ∫⋯∫⁻_s ∪ t, f ∂μ = ∫⋯∫⁻_s, ∫⋯∫⁻_t, f ∂μ ∂μ

Tactic:
ext1 x

Goal state after:
δ : Type u_1
X : δ → Type u_3
inst✝² : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝¹ : DecidableEq δ
s t : Finset δ
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
f : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
hst : Disjoint s t
x : (i : δ) → X i
⊢ (∫⋯∫⁻_s ∪ t, f ∂μ) x = (∫⋯∫⁻_s, ∫⋯∫⁻_t, f ∂μ ∂μ) x
Module: Mathlib.MeasureTheory.Integral.Marginal

Goal state before:
pp: δ : Type u_1
X : δ → Type u_3
inst✝² : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝¹ : DecidableEq δ
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
f : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
s t : Finset δ
hst : Disjoint s t
⊢ ∫⋯∫⁻_s ∪ t, f ∂μ = ∫⋯∫⁻_t, ∫⋯∫⁻_s, f ∂μ ∂μ

Tactic:
rw [Finset.union_comm, lmarginal_union μ f hf hst.symm]

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

Goal state before:
pp: δ : Type u_1
X : δ → Type u_3
inst✝³ : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝² : DecidableEq δ
inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)
inst✝ : Fintype δ
f : ((i : δ) → X i) → ℝ≥0∞
e : ↥Finset.univ ≃ δ := subtypeUnivEquiv ⋯
⊢ ∫⋯∫⁻_Finset.univ, f ∂μ = fun x ↦ ∫⁻ (x : (i : δ) → X i), f x ∂Measure.pi μ

Tactic:
ext1 x

Goal state after:
δ : Type u_1
X : δ → Type u_3
inst✝³ : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝² : DecidableEq δ
inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)
inst✝ : Fintype δ
f : ((i : δ) → X i) → ℝ≥0∞
e : ↥Finset.univ ≃ δ := subtypeUnivEquiv ⋯
x : (i : δ) → X i
⊢ (∫⋯∫⁻_Finset.univ, f ∂μ) x = ∫⁻ (x : (i : δ) → X i), f x ∂Measure.pi μ
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : (𝓝[<] y).NeBot
a : α
xa : x < a
ay : a < y
⊢ rightLim f x ≤ leftLim f y

Tactic:
calc
    rightLim f x ≤ f a := hf.rightLim_le xa
    _ ≤ leftLim f y := hf.le_leftLim ay

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

Goal state before:
pp: R : Type u_1
inst✝³ : LinearOrder R
inst✝² : TopologicalSpace R
f : StieltjesFunction R
inst✝¹ : OrderTopology R
inst✝ : CompactIccSpace R
a b : R
c d : ℕ → R
ss : Icc a b ⊆ ⋃ i, Iotop (c i) (d i)
this :
  ∀ (s : Finset ℕ) (b : R),
    Icc a b ⊆ ⋃ i ∈ ↑s, Iotop (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i ∈ s, ofReal (↑f (d i) - ↑f (c i))
s : Set ℕ
left✝ : s ⊆ univ
hf : s.Finite
hs : Icc a b ⊆ ⋃ i ∈ s, Iotop (c i) (d i)
e : ⋃ i ∈ ↑hf.toFinset, Iotop (c i) (d i) = ⋃ i ∈ s, Iotop (c i) (d i)
⊢ ofReal (↑f b - ↑f a) ≤ ⨆ s, ∑ a ∈ s, ofReal (↑f (d a) - ↑f (c a))

Tactic:
refine le_trans ?_ (le_iSup _ hf.toFinset)

Goal state after:
R : Type u_1
inst✝³ : LinearOrder R
inst✝² : TopologicalSpace R
f : StieltjesFunction R
inst✝¹ : OrderTopology R
inst✝ : CompactIccSpace R
a b : R
c d : ℕ → R
ss : Icc a b ⊆ ⋃ i, Iotop (c i) (d i)
this :
  ∀ (s : Finset ℕ) (b : R),
    Icc a b ⊆ ⋃ i ∈ ↑s, Iotop (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i ∈ s, ofReal (↑f (d i) - ↑f (c i))
s : Set ℕ
left✝ : s ⊆ univ
hf : s.Finite
hs : Icc a b ⊆ ⋃ i ∈ s, Iotop (c i) (d i)
e : ⋃ i ∈ ↑hf.toFinset, Iotop (c i) (d i) = ⋃ i ∈ s, Iotop (c i) (d i)
⊢ ofReal (↑f b - ↑f a) ≤ ∑ a ∈ hf.toFinset, ofReal (↑f (d a) - ↑f (c a))
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: R : Type u_1
inst✝⁴ : LinearOrder R
inst✝³ : TopologicalSpace R
f : StieltjesFunction R
inst✝² : OrderTopology R
inst✝¹ : CompactIccSpace R
inst✝ : DenselyOrdered R
a b : R
hab : a < b
s : ℕ → Set R
hs : Ioc a b ⊆ ⋃ i, s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), f.length (s i) < ∞
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
⊢ ∃ a', ↑f a' - ↑f a < ↑δ ∧ a < a'

Tactic:
by
    have A : ContinuousWithinAt (fun r => f r - f a) (Ioi a) a := by
      refine ContinuousWithinAt.sub ?_ continuousWithinAt_const
      exact (f.right_continuous a).mono Ioi_subset_Ici_self
    have B : f a - f a < δ := by rwa [sub_self, NNReal.coe_pos, ← ENNReal.coe_pos]
    have : (𝓝[>] a).NeBot := nhdsGT_neBot_of_exists_gt ⟨b, hab⟩
    exact (((tendsto_order.1 A).2 _ B).and self_mem_nhdsWithin).exists

Goal state after:
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace α
s : Set α
μ : Measure α
inst✝¹ : Countable G
inst✝ : SMulInvariantMeasure G α μ
hμ : μ ≠ 0
h : IsFundamentalDomain G s μ
hc : μ s = 0
⊢ ∑' (i : G), μ (i • s) ≤ 0

Tactic:
simp_rw [measure_smul, hc, tsum_zero, le_refl]

Goal state after: