mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: case inr
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
mβ : MeasurableSpace β
inst✝¹ : LinearOrder α
inst✝ : atTop.IsCountablyGenerated
x : α
g : α → β
g_meas : ∀ t > x, AEMeasurable g (μ.restrict (Ioc x t))
this : Nonempty α
u : ℕ → α
hu_tendsto : Tendsto u atTop atTop
Ioi_eq_iUnion : Ioi x = ⋃ n, Ioc x (u n)
n : ℕ
h : u n ≤ x
⊢ AEMeasurable g (μ.restrict ∅)

Tactic:
Measure.restrict_empty

Goal state after:
case inr
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
mβ : MeasurableSpace β
inst✝¹ : LinearOrder α
inst✝ : atTop.IsCountablyGenerated
x : α
g : α → β
g_meas : ∀ t > x, AEMeasurable g (μ.restrict (Ioc x t))
this : Nonempty α
u : ℕ → α
hu_tendsto : Tendsto u atTop atTop
Ioi_eq_iUnion : Ioi x = ⋃ n, Ioc x (u n)
n : ℕ
h : u n ≤ x
⊢ AEMeasurable g 0
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Preorder α
s : Set α
hsc : s.Countable
hst : ∀ (x : α), ∃ y ∈ s, x ≤ y
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
⊢ DirectedOn ((fun x1 x2 ↦ x1 ⊆ x2) on Iic) s

Tactic:
exact directedOn_iff_directed.2 (hdir.directed_val.mono_comp _ fun x y => Iic_subset_Iic.2)

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

Goal state before:
pp: M : Type u_2
ι : Type u_3
α : Type u_4
inst✝² : CommMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
f : ι → α → M
s : Finset ι
hf : ∀ i ∈ s, Measurable (f i)
⊢ Measurable fun a ↦ ∏ i ∈ s, f i a

Tactic:
simp_rw [← Finset.prod_apply]

Goal state after:
M : Type u_2
ι : Type u_3
α : Type u_4
inst✝² : CommMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
f : ι → α → M
s : Finset ι
hf : ∀ i ∈ s, Measurable (f i)
⊢ Measurable fun a ↦ (∏ c ∈ s, f c) a
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
r : ℝ≥0∞
h : r < infEDist x s
⊢ ∀ ⦃a : α⦄, a ∈ closedEBall x r → a ∉ s

Tactic:
intro y

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
r : ℝ≥0∞
h : r < infEDist x s
y : α
⊢ y ∈ closedEBall x r → y ∉ s
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → y ∈ s
S : Set (Set α) := {S | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ico l u = S}
this : MeasurableSpace α := MeasurableSpace.generateFrom S
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
ha : ∀ b < a, (Ioo b a).Nonempty
⊢ Iio a = ⋃ l ∈ t, ⋃ u ∈ t, ⋃ (_ : l < u), ⋃ (_ : u ≤ a), Ico l u

Tactic:
ext y
      push _ ∈ _
      constructor
      · intro hy
        rcases htd.exists_le' (fun b hb => htb _ hb (hbot b hb)) y with ⟨l, hlt, hly⟩
        rcases htd.exists_mem_open isOpen_Ioo (ha y hy) with ⟨u, hut, hyu, hua⟩
        exact ⟨l, hlt, u, hut, hly.trans_lt hyu, hua.le, hly, hyu⟩
      · rintro ⟨l, -, u, -, -, hua, -, hyu⟩
        exact hyu.trans_le hua

Goal state after:
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
⊢ thickening δ ∅ = ∅

Tactic:
by
  simp only [thickening, ofPred_false, infEDist_empty, not_top_lt]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: case inr
α : Type u
inst✝ : PseudoEMetricSpace α
A : Set α
r₁ r₂ : ℝ
hr : r₁ < r₂
h₁ : 0 ≤ r₁
h : (ENNReal.ofReal r₁).toReal = (ENNReal.ofReal r₂).toReal
⊢ r₁ = r₂

Tactic:
rwa [ENNReal.toReal_ofReal h₁, ENNReal.toReal_ofReal (h₁.trans hr.le)] at h

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case neg
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → y ∈ s
S : Set (Set α) := {S | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ico l u = S}
this : MeasurableSpace α := MeasurableSpace.generateFrom S
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
ha : ∃ b < a, Ioo b a = ∅
⊢ MeasurableSet (Iio a)

Tactic:
replace ha : a ∈ s := hIoo ha.choose a ha.choose_spec.1 ha.choose_spec.2

Goal state after:
case neg
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → y ∈ s
S : Set (Set α) := {S | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ico l u = S}
this : MeasurableSpace α := MeasurableSpace.generateFrom S
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
ha : a ∈ s
⊢ MeasurableSet (Iio a)
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: case inl.inl
α : Type u
inst✝ : PseudoEMetricSpace α
fin : hausdorffEDist ∅ ∅ ≠ ∞
⊢ ∅ = ∅ ∧ ∅ = ∅ ∨ ∅.Nonempty ∧ ∅.Nonempty

pp: case inl.inr
α : Type u
inst✝ : PseudoEMetricSpace α
t : Set α
fin : hausdorffEDist ∅ t ≠ ∞
ht : t.Nonempty
⊢ ∅ = ∅ ∧ t = ∅ ∨ ∅.Nonempty ∧ t.Nonempty

Tactic:
· exact Or.inl ⟨rfl, rfl⟩

Goal state after:
case inl.inr
α : Type u
inst✝ : PseudoEMetricSpace α
t : Set α
fin : hausdorffEDist ∅ t ≠ ∞
ht : t.Nonempty
⊢ ∅ = ∅ ∧ t = ∅ ∨ ∅.Nonempty ∧ t.Nonempty
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: case refine_3
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
ε : ℝ≥0
⊢ (ediam s).toReal + (2 * ↑ε).toReal = diam s + 2 * ↑ε

Tactic:
simp [diam]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : PseudoMetricSpace α
l : Filter β
s : Set α
f : β → α
hs₁ : IsCompact s
hs₂ : s.Nonempty
⊢ Tendsto f l (𝓝ˢ s) ↔ ∀ ε > 0, ∀ᶠ (x : β) in l, infDist (f x) s < ε

Tactic:
by
  rw [(hasBasis_nhdsSet_thickening hs₁).tendsto_right_iff]
  congrm (∀ ε hε, ?_)
  simp [mem_thickening_iff_infDist_lt hs₂]

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric

Goal state before:
pp: α : Type u_1
inst✝² : PseudoEMetricSpace α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, μ (cthickening R s) ≠ ∞
⊢ Tendsto (fun r ↦ μ (cthickening r s)) (𝓝[>] 0)
    (𝓝 (μ (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)))

Tactic:
closure_eq_iInter_cthickening

Goal state after:
α : Type u_1
inst✝² : PseudoEMetricSpace α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, μ (cthickening R s) ≠ ∞
⊢ Tendsto (fun r ↦ μ (cthickening r s)) (𝓝[>] 0) (𝓝 (μ (⋂ δ, ⋂ (_ : 0 < δ), cthickening δ s)))
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
δ : ℝ
hδ : 0 < δ
hs : thickening δ s ⊆ s
⊢ IsClopen s

Tactic:
replace hs : thickening δ s = s := le_antisymm hs (self_subset_thickening hδ s)

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
δ : ℝ
hδ : 0 < δ
hs : thickening δ s = s
⊢ IsClopen s
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Zero β
r : β
s : Set α
f : α →ₛ β
hs : MeasurableSet s
⊢ r ∈ range ⇑(f.restrict s) ↔ r = 0 ∧ s ≠ univ ∨ r ∈ ⇑f '' s

Tactic:
coe_restrict _ hs,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Zero β
r : β
s : Set α
f : α →ₛ β
hs : MeasurableSet s
⊢ r ∈ range (s.indicator ⇑f) ↔ r = 0 ∧ s ≠ univ ∨ r ∈ ⇑f '' s
Module: Mathlib.MeasureTheory.MeasurableSpace.Prod

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_3
γ : Type u_4
inst✝ : MeasurableSingletonClass α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
x : α
f : γ → β
hf : MeasurableEmbedding f
⊢ Function.Injective fun y ↦ (x, f y)

Tactic:
intro y

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_3
γ : Type u_4
inst✝ : MeasurableSingletonClass α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
x : α
f : γ → β
hf : MeasurableEmbedding f
y : γ
⊢ ∀ ⦃a₂ : γ⦄, (fun y ↦ (x, f y)) y = (fun y ↦ (x, f y)) a₂ → y = a₂
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: case e_f.hs
α : Type u_1
β : Type u_2
inst✝⁷ : MeasurableSpace α
inst✝⁶ : SemilatticeSup β
inst✝⁵ : OrderBot β
inst✝⁴ : Zero β
inst✝³ : TopologicalSpace β
inst✝² : OrderClosedTopology β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
i : ℕ → β
f : α → β
n : ℕ
a : α
hf : Measurable f
k : ℕ
⊢ MeasurableSet {a | i k ≤ f a}

Tactic:
· exact hf measurableSet_Ici

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case pos
α : Type u_1
δ : Type u_4
inst✝⁵ : TopologicalSpace α
mα : MeasurableSpace α
inst✝⁴ : BorelSpace α
mδ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
inst✝ : Countable ι
f : ι → δ → α
g g' : δ → α
hf : ∀ (i : ι), Measurable (f i)
s : Set δ
hs : MeasurableSet s
hg : ∀ b ∈ s, IsLUB {a | ∃ i, f i b = a} (g b)
hg' : EqOn g g' sᶜ
g'_meas : Measurable g'
i : ι
this : Nonempty ι
f' : ι → δ → α := fun i ↦ s.piecewise (f i) g'
b : δ
hb : b ∈ s
A : ∀ (i : ι), f' i b = f i b
⊢ IsLUB {a | ∃ i, f' i b = a} (g b)

Tactic:
simpa [A] using hg b hb

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_5
f : ι → δ → α
s : Set ι
hs : s.Countable
hf : ∀ i ∈ s, Measurable (f i)
⊢ Measurable fun x ↦ sSup ((fun i ↦ f i x) '' s)

Tactic:
simp_rw [image_eq_range]

Goal state after:
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_5
f : ι → δ → α
s : Set ι
hs : s.Countable
hf : ∀ i ∈ s, Measurable (f i)
⊢ Measurable fun x ↦ sSup (range fun x_1 ↦ f (↑x_1) x)
Module: Mathlib.Topology.Instances.Real.Lemmas

Goal state before:
pp: f : ℕ → ℝ
k : ℕ
h_ant : Antitone fun n ↦ f (n + k)
h_bdd : BddBelow (range fun x ↦ f (x + k))
⊢ Tendsto (fun n ↦ f (n + k)) atTop (𝓝 (⨅ x, f (x + k)))

Tactic:
exact tendsto_atTop_ciInf h_ant h_bdd

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
h : f.lintegral μ ≠ ∞
b : ℝ≥0∞
hb : b ≠ 0
⊢ μ (⇑f ⁻¹' {b}) < ∞

Tactic:
rw [f.lintegral_eq_of_subset' (Finset.subset_insert b _)] at h

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
b : ℝ≥0∞
h : ∑ x ∈ insert b (f.range \ {0}), x * μ (⇑f ⁻¹' {x}) ≠ ∞
hb : b ≠ 0
⊢ μ (⇑f ⁻¹' {b}) < ∞
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: case inr
c : EReal
hc : c ≠ 0
⊢ Measurable fun x ↦ c * x

Tactic:
refine measurable_of_continuousOn_compl_singleton 0 fun x (hx : x ≠ 0) ↦ ?_
    exact (continuousAt_mul (Or.inl hc) (Or.inl hc) (Or.inr hx) (Or.inr hx)).comp_of_eq
      (continuousAt_const.prodMk continuousAt_id) rfl |>.continuousWithinAt

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

Goal state before:
pp: case insert
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : AddZeroClass γ
motive : (α →ₛ γ) → Prop
const :
  ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), motive (piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ⇑f) (support ⇑g) → motive f → motive g → motive (f + g)
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ), range ⇑f \ {0} = ↑s → motive f
f : α →ₛ γ
h : range ⇑f \ {0} = ↑(insert x s)
mx : MeasurableSet (⇑f ⁻¹' {x})
g : α →ₛ γ := piecewise (⇑f ⁻¹' {x}) mx 0 f
Pg : motive g
⊢ support ⇑g ⊓ support ⇑(piecewise (⇑f ⁻¹' {x}) mx (SimpleFunc.const α x) (SimpleFunc.const α 0)) ⊆ ⊥

Tactic:
rintro y

Goal state after:
case insert
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : AddZeroClass γ
motive : (α →ₛ γ) → Prop
const :
  ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), motive (piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ⇑f) (support ⇑g) → motive f → motive g → motive (f + g)
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ), range ⇑f \ {0} = ↑s → motive f
f : α →ₛ γ
h : range ⇑f \ {0} = ↑(insert x s)
mx : MeasurableSet (⇑f ⁻¹' {x})
g : α →ₛ γ := piecewise (⇑f ⁻¹' {x}) mx 0 f
Pg : motive g
y : α
⊢ y ∈ support ⇑g ⊓ support ⇑(piecewise (⇑f ⁻¹' {x}) mx (SimpleFunc.const α x) (SimpleFunc.const α 0)) → y ∈ ⊥
Module: Mathlib.MeasureTheory.Function.SimpleFuncDense

Goal state before:
pp: X : Type u_3
Y : Type u_4
α : Type u_5
inst✝¹⁰ : Zero α
inst✝⁹ : TopologicalSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : MeasurableSpace X
inst✝⁶ : MeasurableSpace Y
inst✝⁵ : OpensMeasurableSpace X
inst✝⁴ : OpensMeasurableSpace Y
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetrizableSpace α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, inst✝³] f
h'f : HasCompactSupport f
this : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
g : ℕ → SimpleFunc (X × Y) α
hg : ∀ (n : ℕ) (x : X × Y), dist (f x) ((g n) x) < u n
x : X × Y
n : ℕ
⊢ dist ((g n) x) (f x) ≤ u n

Tactic:
rw [dist_comm]

Goal state after:
X : Type u_3
Y : Type u_4
α : Type u_5
inst✝¹⁰ : Zero α
inst✝⁹ : TopologicalSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : MeasurableSpace X
inst✝⁶ : MeasurableSpace Y
inst✝⁵ : OpensMeasurableSpace X
inst✝⁴ : OpensMeasurableSpace Y
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetrizableSpace α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, inst✝³] f
h'f : HasCompactSupport f
this : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
g : ℕ → SimpleFunc (X × Y) α
hg : ∀ (n : ℕ) (x : X × Y), dist (f x) ((g n) x) < u n
x : X × Y
n : ℕ
⊢ dist (f x) ((g n) x) ≤ u n
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
φ : α →ₛ ℝ≥0
hle : ∀ (x : α), ↑(φ x) ≤ f x
b : ℝ≥0∞
hbφ : b < (SimpleFunc.map ofNNReal φ).lintegral μ + ε
hb : ∀ (i : α →ₛ ℝ≥0), (∀ (x : α), ↑(i x) ≤ f x) → (SimpleFunc.map ofNNReal i).lintegral μ ≤ b
ψ : α →ₛ ℝ≥0
hψ : ∀ (x : α), ↑(ψ x) ≤ f x
this : (SimpleFunc.map ofNNReal φ).lintegral μ ≠ ∞
⊢ (SimpleFunc.map ofNNReal (φ + (ψ - φ))).lintegral μ < (SimpleFunc.map ofNNReal φ).lintegral μ + ε

Tactic:
refine (hb _ fun x => le_trans ?_ (max_le (hle x) (hψ x))).trans_lt hbφ

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
φ : α →ₛ ℝ≥0
hle : ∀ (x : α), ↑(φ x) ≤ f x
b : ℝ≥0∞
hbφ : b < (SimpleFunc.map ofNNReal φ).lintegral μ + ε
hb : ∀ (i : α →ₛ ℝ≥0), (∀ (x : α), ↑(i x) ≤ f x) → (SimpleFunc.map ofNNReal i).lintegral μ ≤ b
ψ : α →ₛ ℝ≥0
hψ : ∀ (x : α), ↑(ψ x) ≤ f x
this : (SimpleFunc.map ofNNReal φ).lintegral μ ≠ ∞
x : α
⊢ ↑((φ + (ψ - φ)) x) ≤ max ↑(φ x) ↑(ψ x)
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
⊢ StronglyMeasurable f ↔ ∃ c, f = fun x ↦ c

Tactic:
refine ⟨fun hf => ?_, fun hf_eq => ?_⟩

Goal state after:
case inr.refine_1
α : Type u_1
β : Type u_2
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
⊢ ∃ c, f = fun x ↦ c

case inr.refine_2
α : Type u_1
β : Type u_2
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
hf_eq : ∃ c, f = fun x ↦ c
⊢ StronglyMeasurable f
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : α → ℝ≥0∞ := fun a ↦ ⨆ n, f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), ↑(s x) ≤ ⨆ n, f n x
r✝ : ℝ≥0
right✝ ha✝ : ↑r✝ < 1
ha : r✝ < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun a ↦ r✝ * a) s
eq_rs : SimpleFunc.map c rs = const α ↑r✝ * SimpleFunc.map c s
eq : ∀ (p : ℝ≥0∞), ⇑(SimpleFunc.map c rs) ⁻¹' {p} = ⋃ n, ⇑(SimpleFunc.map c rs) ⁻¹' {p} ∩ {a | p ≤ f n a}
mono : ∀ (r : ℝ≥0∞), Monotone fun n ↦ ⇑(SimpleFunc.map c rs) ⁻¹' {r} ∩ {a | r ≤ f n a}
h_meas : ∀ (n : ℕ), MeasurableSet {a | (SimpleFunc.map c rs) a ≤ f n a}
n : ℕ
r : ℝ≥0∞
x✝ : r ∈ (SimpleFunc.map c rs).range
⊢ r * μ (⇑(SimpleFunc.map c rs) ⁻¹' {r} ∩ {a | r ≤ f n a}) =
    r * μ (⇑(SimpleFunc.map c rs) ⁻¹' {r} ∩ {a | (SimpleFunc.map c rs) a ≤ f n a})

Tactic:
congr 2 with a

Goal state after:
case h.e_a.e_6
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : α → ℝ≥0∞ := fun a ↦ ⨆ n, f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), ↑(s x) ≤ ⨆ n, f n x
r✝ : ℝ≥0
right✝ ha✝ : ↑r✝ < 1
ha : r✝ < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun a ↦ r✝ * a) s
eq_rs : SimpleFunc.map c rs = const α ↑r✝ * SimpleFunc.map c s
eq : ∀ (p : ℝ≥0∞), ⇑(SimpleFunc.map c rs) ⁻¹' {p} = ⋃ n, ⇑(SimpleFunc.map c rs) ⁻¹' {p} ∩ {a | p ≤ f n a}
mono : ∀ (r : ℝ≥0∞), Monotone fun n ↦ ⇑(SimpleFunc.map c rs) ⁻¹' {r} ∩ {a | r ≤ f n a}
h_meas : ∀ (n : ℕ), MeasurableSet {a | (SimpleFunc.map c rs) a ≤ f n a}
n : ℕ
r : ℝ≥0∞
x✝ : r ∈ (SimpleFunc.map c rs).range
a : α
⊢ a ∈ ⇑(SimpleFunc.map c rs) ⁻¹' {r} ∩ {a | r ≤ f n a} ↔
    a ∈ ⇑(SimpleFunc.map c rs) ⁻¹' {r} ∩ {a | (SimpleFunc.map c rs) a ≤ f n a}
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
h's : EqOn f 0 s
⊢ ∫⁻ (x : α) in s, f x ∂μ = 0

Tactic:
by
  simp [setLIntegral_congr_fun hs h's]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
⊢ ∀ (i j : { i // ⇑i ≤ fun a ↦ f a }), ∃ k, (↑i).lintegral μ + (↑j).lintegral ν ≤ (↑k).lintegral μ + (↑k).lintegral ν

Tactic:
rintro ⟨φ, hφ⟩ ⟨ψ, hψ⟩

Goal state after:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
φ : α →ₛ ℝ≥0∞
hφ : ⇑φ ≤ fun a ↦ f a
ψ : α →ₛ ℝ≥0∞
hψ : ⇑ψ ≤ fun a ↦ f a
⊢ ∃ k, (↑⟨φ, hφ⟩).lintegral μ + (↑⟨ψ, hψ⟩).lintegral ν ≤ (↑k).lintegral μ + (↑k).lintegral ν
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᵐ[μ] g
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
hg : AEMeasurable g μ
hgf : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ
this : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, g x < f x + (↑n)⁻¹
⊢ f =ᵐ[μ] g

Tactic:
refine hfg.mp ((ae_all_iff.2 this).mono fun x hlt hle => hle.antisymm ?_)

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᵐ[μ] g
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
hg : AEMeasurable g μ
hgf : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ
this : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, g x < f x + (↑n)⁻¹
x : α
hlt : ∀ (i : ℕ), g x < f x + (↑i)⁻¹
hle : f x ≤ g x
⊢ g x ≤ f x
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Countable β
f : β → α → ℝ≥0∞
μ : Measure α
hμ : μ ≠ 0
hf : ∀ (b : β), Measurable (f b)
hf_int : ∀ (b : β), ∫⁻ (a : α), f b a ∂μ ≠ ∞
h_directed : Directed (fun x1 x2 ↦ x1 ≥ x2) f
val✝ : Encodable β
h✝ : Nonempty β
inhabited_h : Inhabited β
this : ∀ (a : α), ⨅ b, f b a = ⨅ n, f (Directed.sequence f h_directed n) a
b : β
⊢ ⨅ n, ∫⁻ (a : α), (f ∘ Directed.sequence f h_directed) n a ∂μ ≤ ∫⁻ (a : α), f b a ∂μ

Tactic:
exact iInf_le_of_le (Encodable.encode b + 1) (lintegral_mono <| h_directed.sequence_le b)

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

Goal state before:
pp: case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s t : Set α
h : ¬∃ s, MeasurableSet s ∧ SigmaFinite (μ.restrict s) ∧ ∀ t ⊆ sᶜ, ν t ≠ 0 → μ t = ∞
⊢ SigmaFinite (μ.restrict ∅)

Tactic:
Measure.restrict_empty

Goal state after:
case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s t : Set α
h : ¬∃ s, MeasurableSet s ∧ SigmaFinite (μ.restrict s) ∧ ∀ t ⊆ sᶜ, ν t ≠ 0 → μ t = ∞
⊢ SigmaFinite 0
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
s : Finset β
f : β → α → ℝ≥0∞
hf : ∀ b ∈ s, AEMeasurable (f b) μ
⊢ ∫⁻ (a : α), ∑ b ∈ s, f b a ∂μ = ∑ b ∈ s, ∫⁻ (a : α), f b a ∂μ

Tactic:
by
  classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert a s has ih =>
    simp only [Finset.sum_insert has]
    rw [Finset.forall_mem_insert] at hf
    rw [lintegral_add_left' hf.1, ih hf.2]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
n : ℕ
hC_lt : ⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s ≤ 1 / ↑n
⊢ SigmaFinite (μ.restrict ∅)

Tactic:
Measure.restrict_empty

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
n : ℕ
hC_lt : ⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s ≤ 1 / ↑n
⊢ SigmaFinite 0
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
E : Type u_5
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝³ : TopologicalSpace E
inst✝² : Preorder E
inst✝¹ : OrderClosedTopology E
inst✝ : PseudoMetrizableSpace E
hm : m ≤ m₀
hf : StronglyMeasurable f
hg : StronglyMeasurable g
hfg : f ≤ᵐ[μ] g
⊢ f ≤ᵐ[μ.trim hm] g

Tactic:
by
  rwa [EventuallyLE, ae_iff, trim_measurableSet_eq hm]
  exact (hf.measurableSet_le hg).compl

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence

Goal state before:
pp: case refine_5
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
ι : Type u_2
l : Filter ι
inst✝ : l.IsCountablyGenerated
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, AEMeasurable (F n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ a, ∀ (b : ℕ), a ≤ b → x b ∈ s
k : ℕ
h : ∀ (b : ℕ), k ≤ b → x b ∈ {x | (fun n ↦ AEMeasurable (F n) μ) x} ∩ {x | (fun n ↦ ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x}
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F (x (n + k)) a) atTop (𝓝 (f a))

Tactic:
· refine h_lim.mono fun a h_lim => ?_
    apply @Tendsto.comp _ _ _ (fun n => x (n + k)) fun n => F n a
    · assumption
    rw [tendsto_add_atTop_iff_nat]
    assumption

Goal state after:
Module: Mathlib.Analysis.Normed.Group.FunctionSeries

Goal state before:
pp: β : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
ι : Type u_4
f : ι → β → F
u : ι → ℝ
hu : Summable u
hfu : ∀ᶠ (n : ι) in cofinite, ∀ (x : β), ‖f n x‖ ≤ u n
⊢ TendstoUniformlyOn (fun t x ↦ ∑ n ∈ t, f n x) (fun x ↦ ∑' (n : ι), f n x) atTop univ

Tactic:
apply tendstoUniformlyOn_tsum_of_cofinite_eventually hu

Goal state after:
β : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
ι : Type u_4
f : ι → β → F
u : ι → ℝ
hu : Summable u
hfu : ∀ᶠ (n : ι) in cofinite, ∀ (x : β), ‖f n x‖ ≤ u n
⊢ ∀ᶠ (n : ι) in cofinite, ∀ x ∈ univ, ‖f n x‖ ≤ u n