mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: case refine_2
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : Fintype γ
μ : γ → Measure α
ν : γ → Measure β
inst✝¹ : ∀ (i : γ), SigmaFinite (μ i)
inst✝ : ∀ (i : γ), SigmaFinite (ν i)
s : γ → Set α
left✝¹ : s ∈ univ.pi fun i ↦ {s | MeasurableSet s}
t : γ → Set β
left✝ : t ∈ univ.pi fun i ↦ {s | MeasurableSet s}
⊢ (Measure.pi μ) (univ.pi s) * (Measure.pi ν) (univ.pi t) = ∏ x, (μ x) (s x) * (ν x) (t x)

Tactic:
pi_pi,

Goal state after:
case refine_2
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : Fintype γ
μ : γ → Measure α
ν : γ → Measure β
inst✝¹ : ∀ (i : γ), SigmaFinite (μ i)
inst✝ : ∀ (i : γ), SigmaFinite (ν i)
s : γ → Set α
left✝¹ : s ∈ univ.pi fun i ↦ {s | MeasurableSet s}
t : γ → Set β
left✝ : t ∈ univ.pi fun i ↦ {s | MeasurableSet s}
⊢ (∏ i, (μ i) (s i)) * ∏ i, (ν i) (t i) = ∏ x, (μ x) (s x) * (ν x) (t x)
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: case refine_2
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : Fintype γ
μ : γ → Measure α
ν : γ → Measure β
inst✝¹ : ∀ (i : γ), SigmaFinite (μ i)
inst✝ : ∀ (i : γ), SigmaFinite (ν i)
s : γ → Set α
left✝¹ : s ∈ univ.pi fun i ↦ {s | MeasurableSet s}
t : γ → Set β
left✝ : t ∈ univ.pi fun i ↦ {s | MeasurableSet s}
⊢ (∏ i, (μ i) (s i)) * ∏ i, (ν i) (t i) = ∏ x, (μ x) (s x) * (ν x) (t x)

Tactic:
Finset.prod_mul_distrib

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
⊢ (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)

Tactic:
by
  have hxz := hxy.trans hyz
  rw [← sub_pos] at hxy hxz hyz
  have ha : 0 ≤ (z - y) / (z - x) := by positivity
  have hb : 0 ≤ (y - x) / (z - x) := by positivity
  have key := hf.2 hx hz ha hb (by field)
  simp only [smul_eq_mul] at key
  ring_nf at key
  field_simp at key ⊢
  linarith

Goal state after:
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: p q : ℝ≥0∞
hp : 1 < p.toNNReal
⊢ p.toNNReal.HolderConjugate q.toNNReal ↔ p.HolderConjugate q

Tactic:
by
  simp_rw [← NNReal.holderTriple_coe_iff, coe_toNNReal_eq_toReal]
  apply toReal_iff ?_
  all_goals simpa [← coe_toNNReal_eq_toReal]

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: case pos
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
hp : p ≠ 0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
hp' : p = ∞
⊢ ∀ᵐ (x : α) ∂μ, liminf (fun n ↦ ‖f n x‖ₑ) atTop < ∞

Tactic:
subst hp'
    simp_rw [eLpNorm_exponent_top] at hbdd
    have : ∀ n, ∀ᵐ x ∂μ, (‖f n x‖ₑ) < R + 1 := fun n =>
      ae_lt_of_essSup_lt
        (lt_of_le_of_lt (hbdd n) <| ENNReal.lt_add_right ENNReal.coe_ne_top one_ne_zero)
    rw [← ae_all_iff] at this
    filter_upwards [this] with x hx using lt_of_le_of_lt
        (liminf_le_of_frequently_le' <| Frequently.of_forall fun n => (hx n).le)
        (ENNReal.add_lt_top.2 ⟨ENNReal.coe_lt_top, ENNReal.one_lt_top⟩)

Goal state after:
Module: Mathlib.Algebra.Order.Monovary

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : Semifield α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
inst✝² : Semifield β
inst✝¹ : LinearOrder β
inst✝ : IsStrictOrderedRing β
f : ι → α
g : ι → β
hf : StrongLT 0 f
hg : StrongLT 0 g
⊢ Antivary f⁻¹ g⁻¹ ↔ Antivary f g

Tactic:
by
  rw [antivary_inv_left₀ hf, monovary_inv_right₀ hg]

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_norm : ∫⁻ (a : α), f a ^ p ∂μ = 1
hg_norm : ∫⁻ (a : α), g a ^ q ∂μ = 1
⊢ ∫⁻ (a : α), f a ^ p * (ENNReal.ofReal p)⁻¹ ∂μ + ∫⁻ (a : α), g a ^ q * (ENNReal.ofReal q)⁻¹ ∂μ = 1

Tactic:
rw [lintegral_mul_const'' _ (hf.pow_const p), lintegral_mul_const', hf_norm, hg_norm,
          one_mul, one_mul, hpq.inv_add_inv_ennreal]

Goal state after:
case hr
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_norm : ∫⁻ (a : α), f a ^ p ∂μ = 1
hg_norm : ∫⁻ (a : α), g a ^ q ∂μ = 1
⊢ (ENNReal.ofReal q)⁻¹ ≠ ∞
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
hp0_lt : 0 < p
f : α → ℝ≥0∞
hf_nonzero : ∫⁻ (a : α), f a ^ p ∂μ ≠ 0
hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ∞
⊢ ∫⁻ (c : α), funMulInvSnorm f p μ c ^ p ∂μ = 1

Tactic:
simp_rw [funMulInvSnorm_rpow hp0_lt]
  rw [lintegral_mul_const', ENNReal.mul_inv_cancel hf_nonzero hf_top]
  rwa [inv_ne_top]

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_nontop : ∫⁻ (a : α), f a ^ p ∂μ ≠ ∞
hg_nontop : ∫⁻ (a : α), g a ^ q ∂μ ≠ ∞
hf_nonzero : ∫⁻ (a : α), f a ^ p ∂μ ≠ 0
hg_nonzero : ∫⁻ (a : α), g a ^ q ∂μ ≠ 0
npf : ℝ≥0∞ := (∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p)
nqg : ℝ≥0∞ := (∫⁻ (c : α), g c ^ q ∂μ) ^ (1 / q)
⊢ ∫⁻ (a : α), (f * g) a ∂μ = ∫⁻ (a : α), (funMulInvSnorm f p μ * funMulInvSnorm g q μ) a * (npf * nqg) ∂μ

Tactic:
refine lintegral_congr fun a => ?_
      rw [Pi.mul_apply, fun_eq_funMulInvSnorm_mul_eLpNorm f hf_nonzero hf_nontop,
        fun_eq_funMulInvSnorm_mul_eLpNorm g hg_nonzero hg_nontop, Pi.mul_apply]
      ring

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u_1
s : Finset ι
hs : s.Nonempty
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : 0 < ∑ i ∈ s, w i
hz : ∀ i ∈ s, 0 < z i
⊢ (∑ i ∈ s, w i) / ∑ i ∈ s, w i / z i ≤ (∏ i ∈ s, z i ^ w i) ^ (∑ i ∈ s, w i)⁻¹

Tactic:
have := harm_mean_le_geom_mean_weighted s (fun i => (w i) / ∑ i ∈ s, w i) z hs ?_ ?_ hz

Goal state after:
case refine_3
ι : Type u_1
s : Finset ι
hs : s.Nonempty
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : 0 < ∑ i ∈ s, w i
hz : ∀ i ∈ s, 0 < z i
this : (∑ i ∈ s, (w i / ∑ i ∈ s, w i) / z i)⁻¹ ≤ ∏ i ∈ s, z i ^ (w i / ∑ i ∈ s, w i)
⊢ (∑ i ∈ s, w i) / ∑ i ∈ s, w i / z i ≤ (∏ i ∈ s, z i ^ w i) ^ (∑ i ∈ s, w i)⁻¹

case refine_1
ι : Type u_1
s : Finset ι
hs : s.Nonempty
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : 0 < ∑ i ∈ s, w i
hz : ∀ i ∈ s, 0 < z i
⊢ ∀ i ∈ s, 0 < w i / ∑ i ∈ s, w i

case refine_2
ι : Type u_1
s : Finset ι
hs : s.Nonempty
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : 0 < ∑ i ∈ s, w i
hz : ∀ i ∈ s, 0 < z i
⊢ ∑ i ∈ s, w i / ∑ i ∈ s, w i = 1
Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp

Goal state before:
pp: case inl
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
p q : ℝ
inst✝ : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm' f q μ < ∞
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_nonpos : p ≤ 0
⊢ eLpNorm' f p μ < ∞

Tactic:
rw [le_antisymm hp_nonpos hp_nonneg]
    simp

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case inr.inr.refine_1
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : 0 < ∑ i ∈ s, f i ^ p
hg : 0 < ∑ i ∈ s, g i ^ q
f' : ι → ℝ≥0 := fun i ↦ f i / (∑ i ∈ s, f i ^ p) ^ (1 / p)
g' : ι → ℝ≥0 := fun i ↦ g i / (∑ i ∈ s, g i ^ q) ^ (1 / q)
⊢ (∑ i ∈ s, f i ^ p) / ∑ i ∈ s, f i ^ p = 1

Tactic:
div_self hf.ne'

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
p q r : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr✝ : p.HolderTriple q r
hpqr : 1 / r = 1 / p + 1 / q
hp : 0 < p.toReal
hq : 0 < q.toReal
hp₁ : 0 < p
hp₂ : p < ∞
hq₁ : 0 < q
hq₂ : q < ∞
hpqr' : 1 / r.toReal = 1 / p.toReal + 1 / q.toReal
⊢ 0 < 1 / r.toReal

Tactic:
rw [hpqr']; positivity

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.Complete

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝² : SeminormedAddGroup E
ι : Type u_3
inst✝¹ : Nonempty ι
inst✝ : LinearOrder ι
f : ι → α → E
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (f_lim x))
⊢ eLpNormEssSup f_lim μ = essSup (fun x ↦ liminf (fun m ↦ ‖f m x‖ₑ) atTop) μ

Tactic:
eLpNormEssSup_eq_essSup_enorm

Goal state after:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝² : SeminormedAddGroup E
ι : Type u_3
inst✝¹ : Nonempty ι
inst✝ : LinearOrder ι
f : ι → α → E
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (f_lim x))
⊢ essSup (fun x ↦ ‖f_lim x‖ₑ) μ = essSup (fun x ↦ liminf (fun m ↦ ‖f m x‖ₑ) atTop) μ
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case e'_3.a
ι : Type u
s : Finset ι
p : ℝ
hp✝ : 1 ≤ p
w f : ι → ℝ≥0∞
hp : 1 < p
hp₀ : 0 < p
hp₁ : p⁻¹ < 1
H : (∑ i ∈ s, w i) ^ (1 - p⁻¹) ≠ 0 ∧ (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹ ≠ 0
H' : (∀ i ∈ s, w i ≠ ∞) ∧ ∀ i ∈ s, w i * f i ^ p ≠ ∞
this :
  ∑ x ∈ s, ↑(w x).toNNReal * ↑(f x).toNNReal ≤ (∑ i ∈ s, ↑(w i).toNNReal) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹
i : ι
hi : i ∈ s
⊢ w i * f i = ↑(w i).toNNReal * ↑(f i).toNNReal

pp: case e'_4
ι : Type u
s : Finset ι
p : ℝ
hp✝ : 1 ≤ p
w f : ι → ℝ≥0∞
hp : 1 < p
hp₀ : 0 < p
hp₁ : p⁻¹ < 1
H : (∑ i ∈ s, w i) ^ (1 - p⁻¹) ≠ 0 ∧ (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹ ≠ 0
H' : (∀ i ∈ s, w i ≠ ∞) ∧ ∀ i ∈ s, w i * f i ^ p ≠ ∞
this :
  ∑ x ∈ s, ↑(w x).toNNReal * ↑(f x).toNNReal ≤ (∑ i ∈ s, ↑(w i).toNNReal) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹
⊢ (∑ i ∈ s, w i) ^ (1 - p⁻¹) = (∑ i ∈ s, ↑(w i).toNNReal) ^ (1 - p⁻¹)

Tactic:
· obtain hw | hw := eq_or_ne (w i) 0
    · simp [hw]
    rw [coe_toNNReal (H'.1 _ hi), coe_toNNReal]
    simpa [mul_eq_top, hw, hp₀, hp₀.not_gt, H'.1 _ hi] using H'.2 _ hi

Goal state after:
case e'_4
ι : Type u
s : Finset ι
p : ℝ
hp✝ : 1 ≤ p
w f : ι → ℝ≥0∞
hp : 1 < p
hp₀ : 0 < p
hp₁ : p⁻¹ < 1
H : (∑ i ∈ s, w i) ^ (1 - p⁻¹) ≠ 0 ∧ (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹ ≠ 0
H' : (∀ i ∈ s, w i ≠ ∞) ∧ ∀ i ∈ s, w i * f i ^ p ≠ ∞
this :
  ∑ x ∈ s, ↑(w x).toNNReal * ↑(f x).toNNReal ≤ (∑ i ∈ s, ↑(w i).toNNReal) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹
⊢ (∑ i ∈ s, w i) ^ (1 - p⁻¹) = (∑ i ∈ s, ↑(w i).toNNReal) ^ (1 - p⁻¹)
Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure

Goal state before:
pp: α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝ : SeminormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
δ : ℝ≥0∞
hδ : 0 < δ
hδ_top : δ ≠ ∞
hfg : ∀ᶠ (x : ι) in l, essSup (fun x_1 ↦ ‖(f x - g) x_1‖ₑ) μ ≤ δ / 2
ε : ℝ≥0∞
hε : ε > 0
n : ι
hn : essSup (fun x ↦ ‖(f n - g) x‖ₑ) μ ≤ δ / 2
⊢ μ {x | δ ≤ edist (f n x) (g x)} ≤ ε

Tactic:
simp only [Pi.sub_apply] at *

Goal state after:
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝ : SeminormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
δ : ℝ≥0∞
hδ : 0 < δ
hδ_top : δ ≠ ∞
hfg : ∀ᶠ (x : ι) in l, essSup (fun x_1 ↦ ‖f x x_1 - g x_1‖ₑ) μ ≤ δ / 2
ε : ℝ≥0∞
hε : ε > 0
n : ι
hn : essSup (fun x ↦ ‖f n x - g x‖ₑ) μ ≤ δ / 2
⊢ μ {x | δ ≤ edist (f n x) (g x)} ≤ ε
Module: Mathlib.Analysis.Normed.Ring.Units

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
a✝ : Nontrivial R
⊢ ∃ ε > 0, ∀ ⦃y : R⦄, dist y 0 < ε → (↑x + y)⁻¹ʳ = (1 + ↑x⁻¹ * y)⁻¹ʳ * ↑x⁻¹

Tactic:
refine ⟨‖(↑x⁻¹ : R)‖⁻¹, by cancel_denoms, fun t ht ↦ ?_⟩

Goal state after:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
a✝ : Nontrivial R
t : R
ht : dist t 0 < ‖↑x⁻¹‖⁻¹
⊢ (↑x + t)⁻¹ʳ = (1 + ↑x⁻¹ * t)⁻¹ʳ * ↑x⁻¹
Module: Mathlib.Analysis.Normed.Ring.Units

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
n : ℕ
⊢ ∀ᶠ (t : R) in 𝓝 0, (↑x + t)⁻¹ʳ = (∑ i ∈ range n, (-↑x⁻¹ * t) ^ i) * ↑x⁻¹ + (-↑x⁻¹ * t) ^ n * (↑x + t)⁻¹ʳ

Tactic:
have hzero : Tendsto (-(↑x⁻¹ : R) * ·) (𝓝 0) (𝓝 0) :=
    (mulLeft_continuous _).tendsto' _ _ <| mul_zero _

Goal state after:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
n : ℕ
hzero : Tendsto (fun x_1 ↦ -↑x⁻¹ * x_1) (𝓝 0) (𝓝 0)
⊢ ∀ᶠ (t : R) in 𝓝 0, (↑x + t)⁻¹ʳ = (∑ i ∈ range n, (-↑x⁻¹ * t) ^ i) * ↑x⁻¹ + (-↑x⁻¹ * t) ^ n * (↑x + t)⁻¹ʳ
Module: Mathlib.Analysis.Normed.Ring.Units

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
⊢ (fun x_1 ↦ (1 - -↑x⁻¹ * x_1)⁻¹ʳ * ↑x⁻¹) =O[𝓝 0] fun _t ↦ 1 * 1

Tactic:
have hzero : Tendsto (-(↑x⁻¹ : R) * ·) (𝓝 0) (𝓝 0) :=
    (mulLeft_continuous _).tendsto' _ _ <| mul_zero _

Goal state after:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
hzero : Tendsto (fun x_1 ↦ -↑x⁻¹ * x_1) (𝓝 0) (𝓝 0)
⊢ (fun x_1 ↦ (1 - -↑x⁻¹ * x_1)⁻¹ʳ * ↑x⁻¹) =O[𝓝 0] fun _t ↦ 1 * 1
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
⊢ μ.real ∅ = 0

Tactic:
simp [Measure.real]

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

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s : Set α
c : ℝ≥0∞
⊢ (c • μ).real s = c.toReal * μ.real s

Tactic:
simp [Measure.real]

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

Goal state before:
pp: case inl
α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
h : μ t ≠ ∞
hs : μ s = ∞
⊢ μ.real s ≤ μ.real (s ∪ t)

Tactic:
simp [Measure.real, hs]

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

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t μ
h : μ s ≠ ∞
⊢ (μ (s ∩ t)).toReal + (μ (s \ t)).toReal = (μ s).toReal

Tactic:
← ENNReal.toReal_add,

Goal state after:
α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t μ
h : μ s ≠ ∞
⊢ (μ (s ∩ t) + μ (s \ t)).toReal = (μ s).toReal

case ha
α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t μ
h : μ s ≠ ∞
⊢ μ (s ∩ t) ≠ ∞

case hb
α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t μ
h : μ s ≠ ∞
⊢ μ (s \ t) ≠ ∞
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
ht : MeasurableSet t
h : μ s ≠ ∞
⊢ (μ (s ∩ t)).toReal + (μ (s \ t)).toReal = (μ s).toReal

Tactic:
← ENNReal.toReal_add,

Goal state after:
α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
ht : MeasurableSet t
h : μ s ≠ ∞
⊢ (μ (s ∩ t) + μ (s \ t)).toReal = (μ s).toReal

case ha
α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
ht : MeasurableSet t
h : μ s ≠ ∞
⊢ μ (s ∩ t) ≠ ∞

case hb
α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
ht : MeasurableSet t
h : μ s ≠ ∞
⊢ μ (s \ t) ≠ ∞
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h₁ : μ s ≠ ∞
h₂ : μ t ≠ ∞
⊢ (μ (s ∆ t)).toReal = (μ (s \ t)).toReal + (μ (t \ s)).toReal

Tactic:
← ENNReal.toReal_add,

Goal state after:
α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h₁ : μ s ≠ ∞
h₂ : μ t ≠ ∞
⊢ (μ (s ∆ t)).toReal = (μ (s \ t) + μ (t \ s)).toReal

case ha
α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h₁ : μ s ≠ ∞
h₂ : μ t ≠ ∞
⊢ μ (s \ t) ≠ ∞

case hb
α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h₁ : μ s ≠ ∞
h₂ : μ t ≠ ∞
⊢ μ (t \ s) ≠ ∞
Module: Mathlib.Topology.Algebra.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
l : E →ₗ[𝕜] 𝕜
hl : IsClosed[inst✝²] ↑l.ker
H : ¬finrank 𝕜 ↥l.range = 0
this : finrank 𝕜 ↥l.range = 1
hi : Function.Injective ⇑(l.ker.liftQ l ⋯)
⊢ Function.Surjective ⇑(l.ker.liftQ l ⋯)

Tactic:
← LinearMap.range_eq_top,

Goal state after:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
l : E →ₗ[𝕜] 𝕜
hl : IsClosed[inst✝²] ↑l.ker
H : ¬finrank 𝕜 ↥l.range = 0
this : finrank 𝕜 ↥l.range = 1
hi : Function.Injective ⇑(l.ker.liftQ l ⋯)
⊢ (l.ker.liftQ l ⋯).range = ⊤
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
l : Filter α
inst✝ : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → ε
s : Set α
hs : s ∈ l ∧ IntegrableOn (f ∘ e) s μ
⊢ e '' s ∈ map e l ∧ IntegrableOn (f ∘ e) (e ⁻¹' e '' s) μ

Tactic:
by rwa [mem_map, he.injective.preimage_image]

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

Goal state before:
pp: case pos
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst✝⁴ : PartialOrder α
inst✝³ : MeasurableSingletonClass α
inst✝² : TopologicalSpace ε'
inst✝¹ : ESeminormedAddMonoid ε'
inst✝ : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
ha : μ {a} ≠ ∞
ha' : ‖f a‖ₑ ≠ ∞
hab : a ≤ b
⊢ IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ioc a b) μ

Tactic:
rw [← Ioc_union_left hab, integrableOn_union, eq_true (integrableOn_singleton ha'), and_true]

Goal state after:
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: X : Type u_1
ε : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst✝ : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
u : ↑s → Set X
u_open : ∀ (x : ↑s), IsOpen[inst✝³] (u x)
xu : ∀ (x : ↑s), ↑x ∈ u x
hu : ∀ (x : ↑s), IntegrableOn f (u x ∩ s) μ
⊢ ∃ T, T.Countable ∧ s ⊆ ⋃ i ∈ T, u i

Tactic:
by
    have : s ⊆ ⋃ x : s, u x := fun y hy => mem_iUnion_of_mem ⟨y, hy⟩ (xu ⟨y, hy⟩)
    obtain ⟨T, hT_count, hT_un⟩ := isOpen_iUnion_countable u u_open
    exact ⟨T, hT_count, by rwa [hT_un]⟩

Goal state after:
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: case refine_1.inl
X : Type u_1
ε : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst✝ : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
T : Set (Set X)
T_count : T.Countable
T_open : ∀ u ∈ T, IsOpen[inst✝³] u
sT : s ⊆ ⋃ u ∈ T, u
hT : ∀ u ∈ T, IntegrableOn f (u ∩ s) μ
T' : Set (Set X) := insert ∅ T
T'_count : T'.Countable
T'_ne : T'.Nonempty
u : ℕ → Set X
hu : T' = range u
n : ℕ
this : u n ∈ T'
h : u n = ∅
⊢ IsOpen[inst✝³] ∅

Tactic:
exact isOpen_empty

Goal state after:
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: X : Type u_1
E : Type u_6
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup E
μ : Measure X
s : Set X
f : X → E
⊢ LocallyIntegrableOn (-f) s μ ↔ LocallyIntegrableOn f s μ

Tactic:
by
  unfold LocallyIntegrableOn
  simp_rw [MeasureTheory.integrableAtFilter_neg_iff]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : SeminormedAddCommGroup β
T : Set α → β
C : ℝ
μ' : Measure α
h : μ ≤ μ'
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
h' : ∀ (s : Set α), μ s = ∞ → μ' s = ∞
s : Set α
hs : MeasurableSet s
hμ's : μ' s < ∞
hμs : μ s < ∞
⊢ ‖T s‖ ≤ C * μ'.real s

Tactic:
calc
    ‖T s‖ ≤ C * μ.real s := hT.2 s hs hμs
    _ ≤ C * μ'.real s := by
      simp only [measureReal_def]
      gcongr
      exact hμ's.ne

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α →ₛ ℝ
⊢ map norm f.negPart = f.negPart

Tactic:
by
  rw [negPart]; exact posPart_map_norm _

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

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 T' T'' : Set α → E →L[ℝ] F
h_add : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T'' s = T s + T' s
f : α →ₛ E
hf : Integrable (⇑f) μ
⊢ ∑ x ∈ f.range with x ≠ 0, (T'' (⇑f ⁻¹' {x})) x =
    ∑ x ∈ f.range with x ≠ 0, (T (⇑f ⁻¹' {x})) x + ∑ x ∈ f.range with x ≠ 0, (T' (⇑f ⁻¹' {x})) x

Tactic:
suffices ∀ x ∈ {x ∈ f.range | x ≠ 0}, T'' (f ⁻¹' {x}) = T (f ⁻¹' {x}) + T' (f ⁻¹' {x}) by
    rw [← sum_add_distrib]
    refine Finset.sum_congr rfl fun x hx => ?_
    rw [this x hx]
    push_cast
    rw [Pi.add_apply]

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 T' T'' : Set α → E →L[ℝ] F
h_add : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T'' s = T s + T' s
f : α →ₛ E
hf : Integrable (⇑f) μ
⊢ ∀ x ∈ {x ∈ f.range | x ≠ 0}, T'' (⇑f ⁻¹' {x}) = T (⇑f ⁻¹' {x}) + T' (⇑f ⁻¹' {x})
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
G' : Type u_7
G'' : Type u_8
inst✝⁷ : NormedAddCommGroup G''
inst✝⁶ : PartialOrder G''
inst✝⁵ : IsOrderedAddMonoid G''
inst✝⁴ : NormedSpace ℝ G''
inst✝³ : NormedAddCommGroup G'
inst✝² : PartialOrder G'
inst✝¹ : NormedSpace ℝ G'
inst✝ : IsOrderedAddMonoid G'
T : Set α → G' →L[ℝ] G''
h_add : FinMeasAdditive μ T
hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x
f g : α →ₛ G'
hfi : Integrable (⇑f) μ
hgi : Integrable (⇑g) μ
hfg : f ≤ g
⊢ setToSimpleFunc T f ≤ setToSimpleFunc T g

Tactic:
rw [← sub_nonneg, ← setToSimpleFunc_sub T h_add hgi hfi]
  refine setToSimpleFunc_nonneg' T hT_nonneg _ ?_ (hgi.sub hfi)
  intro x
  simp only [coe_sub, sub_nonneg, coe_zero, Pi.zero_apply, Pi.sub_apply]
  exact hfg x

Goal state after:
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
⊢ x ∉ {0}

Tactic:
Finset.mem_singleton

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
⊢ ¬x = 0
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
a✝ : α
h₁ : ↑↑(Lp.posPart f₁) a✝ = max (↑↑f₁ a✝) 0
h₂ : ↑↑(Integrable.toL1 f hf) a✝ = f a✝
⊢ ↑(f a✝).toNNReal = ↑(NNReal.mk (max (f a✝) 0) ⋯)

Tactic:
Real.coe_toNNReal',

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
a✝ : α
h₁ : ↑↑(Lp.posPart f₁) a✝ = max (↑↑f₁ a✝) 0
h₂ : ↑↑(Integrable.toL1 f hf) a✝ = f a✝
⊢ max (f a✝) 0 = ↑(NNReal.mk (max (f a✝) 0) ⋯)