mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Group.Arithmetic

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

Tactic:
;

Goal state after:
M : Type u_2
ι : Type u_3
α : Type u_4
β : Type u_5
inst✝² : CommMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
mβ : MeasurableSpace β
f : ι → α → β → M
g : α → β
s : Finset ι
hf : ∀ i ∈ s, Measurable ↿(f i)
hg : Measurable g
⊢ Measurable fun a ↦ ∏ c ∈ s, f c a (g a)
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: γ : Type u_3
δ : Type u_5
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
inst✝ : MeasurableSpace δ
f : δ → γ
hf : ∀ (s : Set γ), IsClosed[inst✝³] s → s.Nonempty → s ≠ univ → MeasurableSet (f ⁻¹' s)
⊢ ∀ (s : Set γ), IsClosed[inst✝³] s → MeasurableSet (f ⁻¹' s)

Tactic:
;

Goal state after:
γ : Type u_3
δ : Type u_5
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
inst✝ : MeasurableSpace δ
f : δ → γ
hf : ∀ (s : Set γ), IsClosed[inst✝³] s → s.Nonempty → s ≠ univ → MeasurableSet (f ⁻¹' s)
⊢ ∀ (s : Set γ), IsClosed[inst✝³] s → MeasurableSet (f ⁻¹' s)
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: α : Type u_6
inst✝² : TopologicalSpace α
inst✝¹ : T0Space α
inst✝ : Countable α
⊢ borel α = ⊤

Tactic:
refine top_unique fun s _ ↦ ?_
  borelize α
  exact .of_discrete

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
⊢ max (⨆ x ∈ s, infEDist x t) (⨆ y ∈ t, infEDist y s) = max (⨆ y ∈ t, infEDist y s) (⨆ x ∈ s, infEDist x t)

Tactic:
;

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
⊢ max (⨆ x ∈ s, infEDist x t) (⨆ y ∈ t, infEDist y s) = max (⨆ y ∈ t, infEDist y s) (⨆ x ∈ s, infEDist x t)
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s t u : Set α✝
inst✝¹¹ : TopologicalSpace α✝
mα : MeasurableSpace α✝
inst✝¹⁰ : BorelSpace α✝
mβ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
α : Type u_6
inst✝³ : TopologicalSpace α
inst✝² : DiscreteTopology α
inst✝¹ : MeasurableSpace α
inst✝ : DiscreteMeasurableSpace α
⊢ inst✝¹ = borel α

Tactic:
;

Goal state after:
α✝ : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s t u : Set α✝
inst✝¹¹ : TopologicalSpace α✝
mα : MeasurableSpace α✝
inst✝¹⁰ : BorelSpace α✝
mβ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
α : Type u_6
inst✝³ : TopologicalSpace α
inst✝² : DiscreteTopology α
inst✝¹ : MeasurableSpace α
inst✝ : DiscreteMeasurableSpace α
⊢ inst✝¹ = borel α
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s t u : Set α✝
inst✝¹¹ : TopologicalSpace α✝
mα : MeasurableSpace α✝
inst✝¹⁰ : BorelSpace α✝
mβ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
α : Type u_6
inst✝³ : TopologicalSpace α
inst✝² : DiscreteTopology α
inst✝¹ : MeasurableSpace α
inst✝ : DiscreteMeasurableSpace α
s✝ : Set α
⊢ MeasurableSet s✝ ↔ MeasurableSet s✝

Tactic:
;

Goal state after:
α✝ : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s t u : Set α✝
inst✝¹¹ : TopologicalSpace α✝
mα : MeasurableSpace α✝
inst✝¹⁰ : BorelSpace α✝
mβ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
α : Type u_6
inst✝³ : TopologicalSpace α
inst✝² : DiscreteTopology α
inst✝¹ : MeasurableSpace α
inst✝ : DiscreteMeasurableSpace α
s✝ : Set α
⊢ MeasurableSet s✝ ↔ MeasurableSet s✝
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
ε : ℝ≥0
x : α
hx : x ∈ cthickening (↑ε) s
y : α
hy : y ∈ cthickening (↑ε) s
δ : ℝ≥0
hδ : 0 < δ
x✝ : ediam s + 2 * ↑ε < ∞
⊢ edist x y ≤ ediam s + 2 * ↑ε + ↑δ

Tactic:
mem_cthickening_iff,

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
ε : ℝ≥0
x : α
hx : infEDist x s ≤ ENNReal.ofReal ↑ε
y : α
hy : infEDist y s ≤ ENNReal.ofReal ↑ε
δ : ℝ≥0
hδ : 0 < δ
x✝ : ediam s + 2 * ↑ε < ∞
⊢ edist x y ≤ ediam s + 2 * ↑ε + ↑δ
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
ε : ℝ≥0
x y : α
hy : infEDist y s ≤ ↑ε
δ : ℝ≥0
hδ : 0 < δ
x✝ : ediam s + 2 * ↑ε < ∞
hε : ↑ε < ↑ε + ↑δ
hx : infEDist x s < ↑ε + ↑δ
x' : α
hx' : x' ∈ s
hxx' : edist x x' < ↑ε + ↑δ
⊢ ↑ε + ↑δ + (↑ε + ediam s) = ediam s + (↑ε + ↑ε) + ↑δ

Tactic:
;

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
ε : ℝ≥0
x y : α
hy : infEDist y s ≤ ↑ε
δ : ℝ≥0
hδ : 0 < δ
x✝ : ediam s + 2 * ↑ε < ∞
hε : ↑ε < ↑ε + ↑δ
hx : infEDist x s < ↑ε + ↑δ
x' : α
hx' : x' ∈ s
hxx' : edist x x' < ↑ε + ↑δ
⊢ ↑ε + ↑δ + (↑ε + ediam s) = ediam s + (↑ε + ↑ε) + ↑δ
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
⊢ ∃ δ, 0 < δ ∧ Disjoint (cthickening δ s) (cthickening δ t)

Tactic:
obtain ⟨δ, hδ, h⟩ := hst.exists_thickenings hs ht
  refine ⟨δ / 2, half_pos hδ, h.mono ?_ ?_⟩ <;>
    exact cthickening_subset_thickening' hδ (half_lt_self hδ) _

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

Goal state before:
pp: case h
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set α
x : α
⊢ thickening δ s ⊆ cthickening δ s

Tactic:
;

Goal state after:
case h
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set α
x : α
⊢ thickening δ s ⊆ cthickening δ s
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: case inr
α : Type u
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
hδ : 0 ≤ δ
s : Set α
hε : 0 ≤ ε
x : α
⊢ (∃ z ∈ cthickening δ s, edist x z < ENNReal.ofReal ε) → ∃ z ∈ s, edist x z < ENNReal.ofReal (ε + δ)

Tactic:
mem_cthickening_iff,

Goal state after:
case inr
α : Type u
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
hδ : 0 ≤ δ
s : Set α
hε : 0 ≤ ε
x : α
⊢ (∃ z, infEDist z s ≤ ENNReal.ofReal δ ∧ edist x z < ENNReal.ofReal ε) → ∃ z ∈ s, edist x z < ENNReal.ofReal (ε + δ)
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: case inr
α : Type u
inst✝ : PseudoEMetricSpace α
ε : ℝ
hε : 0 ≤ ε
δ : ℝ
s : Set α
hδ : 0 ≤ δ
x : α
⊢ x ∈ cthickening ε (thickening δ s) → x ∈ cthickening (ε + δ) s

Tactic:
mem_cthickening_iff,

Goal state after:
case inr
α : Type u
inst✝ : PseudoEMetricSpace α
ε : ℝ
hε : 0 ≤ ε
δ : ℝ
s : Set α
hδ : 0 ≤ δ
x : α
⊢ infEDist x (thickening δ s) ≤ ENNReal.ofReal ε → infEDist x s ≤ ENNReal.ofReal (ε + δ)
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case convert_4
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
f : δ → α
hf : ∀ (x : α), MeasurableSet (f ⁻¹' Iio x)
x : α
⊢ MeasurableSet (f ⁻¹' Iio x)

Tactic:
;

Goal state after:
case convert_4
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
f : δ → α
hf : ∀ (x : α), MeasurableSet (f ⁻¹' Iio x)
x : α
⊢ MeasurableSet (f ⁻¹' Iio x)
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a : α
⊢ (fun a ↦ (g (f a)) a) a ∈ ⋃ i ∈ range ⇑f, range ⇑(g i)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a : α
⊢ (fun a ↦ (g (f a)) a) a ∈ ⋃ i ∈ range ⇑f, range ⇑(g i)
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 ≤ δ
s : Set α
x : α
⊢ x ∈ cthickening ε (cthickening δ s) → x ∈ cthickening (ε + δ) s

Tactic:
mem_cthickening_iff,

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 ≤ δ
s : Set α
x : α
⊢ infEDist x (cthickening δ s) ≤ ENNReal.ofReal ε → infEDist x s ≤ ENNReal.ofReal (ε + δ)
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case convert_4
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
f : δ → α
hf : ∀ (x : α), MeasurableSet (f ⁻¹' Ioi x)
x : α
⊢ MeasurableSet (f ⁻¹' Ioi x)

Tactic:
;

Goal state after:
case convert_4
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
f : δ → α
hf : ∀ (x : α), MeasurableSet (f ⁻¹' Ioi x)
x : α
⊢ MeasurableSet (f ⁻¹' Ioi x)
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : α → β
hg : MeasurableEmbedding g
f₂ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : MeasurableSpace γ := ⊤
⊢ ∀ (x : γ), MeasurableSet (Function.extend g ⇑f₁ ⇑f₂ ⁻¹' {x})

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : α → β
hg : MeasurableEmbedding g
f₂ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : MeasurableSpace γ := ⊤
⊢ ∀ (x : γ), MeasurableSet (Function.extend g ⇑f₁ ⇑f₂ ⁻¹' {x})
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
f : α →ₛ β
a✝ : α
⊢ (f.bind (const α)) a✝ = f a✝

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
f : α →ₛ β
a✝ : α
⊢ (f.bind (const α)) a✝ = f a✝
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: α : Type u
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : PseudoEMetricSpace β
f : α → β
K : Set α
U : Set β
hK : IsCompact K
ho : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
hf : ∀ x ∈ K, ContinuousAt f x
hKU : MapsTo f K U
x : α
hx : x ∈ K
⊢ f x ∈ U

Tactic:
;

Goal state after:
α : Type u
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : PseudoEMetricSpace β
f : α → β
K : Set α
U : Set β
hK : IsCompact K
ho : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
hf : ∀ x ∈ K, ContinuousAt f x
hKU : MapsTo f K U
x : α
hx : x ∈ K
⊢ f x ∈ U
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: q : ℚ
⊢ ENNReal.ofReal ↑((some q).getD 0) = ↑(↑q).toNNReal

Tactic:
;

Goal state after:
q : ℚ
⊢ ENNReal.ofReal ↑((some q).getD 0) = ↑(↑q).toNNReal
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: α : Type u
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : PseudoEMetricSpace β
f : α → β
K : Set α
U : Set β
hK : IsCompact K
ho : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
hf : ∀ x ∈ K, ContinuousAt f x
hKU : MapsTo f K U
x : α
hx : x ∈ K
this✝ : {f x} ⊆ U
δ : ℝ
hδ : 0 < δ
hthick : thickening δ {f x} ⊆ U
V : Set α := f ⁻¹' thickening (δ / 2) {f x}
this : V ∈ 𝓝 x
⊢ K ∩ interior V ⊆ interior V

Tactic:
;

Goal state after:
α : Type u
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : PseudoEMetricSpace β
f : α → β
K : Set α
U : Set β
hK : IsCompact K
ho : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
hf : ∀ x ∈ K, ContinuousAt f x
hKU : MapsTo f K U
x : α
hx : x ∈ K
this✝ : {f x} ⊆ U
δ : ℝ
hδ : 0 < δ
hthick : thickening δ {f x} ⊆ U
V : Set α := f ⁻¹' thickening (δ / 2) {f x}
this : V ∈ 𝓝 x
⊢ K ∩ interior V ⊆ interior V
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α →ₛ ℝ≥0∞
⊢ ∑ x ∈ (f.pair g).range, (x.1 + x.2) * μ (⇑(f.pair g) ⁻¹' {x}) =
    ∑ x ∈ (f.pair g).range, (x.1 * μ (⇑(f.pair g) ⁻¹' {x}) + x.2 * μ (⇑(f.pair g) ⁻¹' {x}))

Tactic:
;

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α →ₛ ℝ≥0∞
⊢ ∑ x ∈ (f.pair g).range, (x.1 + x.2) * μ (⇑(f.pair g) ⁻¹' {x}) =
    ∑ x ∈ (f.pair g).range, (x.1 * μ (⇑(f.pair g) ⁻¹' {x}) + x.2 * μ (⇑(f.pair g) ⁻¹' {x}))
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
ι : Type u_5
f : α →ₛ ℝ≥0∞
μ : ι → Measure α
⊢ ∑' (x : ↥f.range) (i : ι), ↑x * (μ i) (⇑f ⁻¹' {↑x}) = ∑' (i : ι) (x : ↥f.range), ↑x * (μ i) (⇑f ⁻¹' {↑x})

Tactic:
apply ENNReal.tsum_comm

Goal state after:
Module: Mathlib.Topology.Instances.Real.Lemmas

Goal state before:
pp: x ε : ℝ
⊢ TotallyBounded (Ioo (x - ε) (x + ε))

Tactic:
;

Goal state after:
x ε : ℝ
⊢ TotallyBounded (Ioo (x - ε) (x + ε))
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 α
ι : Sort u_5
inst✝ : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
⊢ Measurable fun b ↦ ⨆ i, f i b

Tactic:
by
  rcases isEmpty_or_nonempty ι with hι | hι
  · simp [iSup_of_empty']
  have A : MeasurableSet {b | BddAbove (range (fun i ↦ f i b))} :=
    measurableSet_bddAbove_range hf
  have : Measurable (fun (_b : δ) ↦ sSup (∅ : Set α)) := measurable_const
  apply Measurable.isLUB_of_mem hf A _ _ this
  · intro b hb
    apply isLUB_ciSup
    simpa
  · intro b hb
    apply csSup_of_not_bddAbove
    simpa

Goal state after:
Module: Mathlib.Topology.Instances.Real.Lemmas

Goal state before:
pp: case e'_2
q : ℚ
⊢ Rat.cast '' {x | q < x} = Ioi ↑q ∩ range Rat.cast

Tactic:
;

Goal state after:
case e'_2
q : ℚ
⊢ Rat.cast '' {x | q < x} = Ioi ↑q ∩ range Rat.cast
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: case inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
h✝ : Nonempty α
⊢ c * μ ((fun x ↦ c) ⁻¹' {c}) = c * μ univ

Tactic:
;

Goal state after:
case inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
h✝ : Nonempty α
⊢ c * μ ((fun x ↦ c) ⁻¹' {c}) = c * μ univ
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
s : Set α
⊢ (const α c).lintegral (μ.restrict s) = c * μ s

Tactic:
by
  rw [const_lintegral, Measure.restrict_apply MeasurableSet.univ, univ_inter]

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

Goal state before:
pp: a : ℝ
this : IsLUB (range Rat.cast ∩ Iio a) a
⊢ MeasurableSet (⋃ x ∈ Rat.cast '' univ ∩ Iio a, Iio x)

Tactic:
← image_inter_preimage,

Goal state after:
a : ℝ
this : IsLUB (range Rat.cast ∩ Iio a) a
⊢ MeasurableSet (⋃ x ∈ Rat.cast '' (univ ∩ Rat.cast ⁻¹' Iio a), Iio x)
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: a : ℝ
this : IsGLB (range Rat.cast ∩ Ioi a) a
⊢ MeasurableSet (⋃ x ∈ Rat.cast '' univ ∩ Ioi a, Ioi x)

Tactic:
← image_inter_preimage,

Goal state after:
a : ℝ
this : IsGLB (range Rat.cast ∩ Ioi a) a
⊢ MeasurableSet (⋃ x ∈ Rat.cast '' (univ ∩ Rat.cast ⁻¹' Ioi a), Ioi x)
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α
mα : MeasurableSpace α
x✝ : ℝ≥0
⊢ Measurable fun x ↦ ↑x✝ • x

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α
mα : MeasurableSpace α
x✝ : ℝ≥0
⊢ Measurable fun x ↦ ↑x✝ • x
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0
g : α → ℝ≥0
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
lim : ∀ (x : α), Tendsto (fun i ↦ f i x) u (𝓝 (g x))
hf : ∀ (i : ι), Measurable fun x ↦ ↑(f i x)
⊢ ∀ (x : α), Tendsto (fun i ↦ ↑(f i x)) u (𝓝 ↑(g x))

Tactic:
exact fun x => (ENNReal.continuous_coe.tendsto (g x)).comp (lim x)

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

Goal state before:
pp: c : EReal
⊢ Measurable fun x ↦ c * x

Tactic:
by
  rcases eq_or_ne c 0 with rfl | hc
  · simp
  · 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.Constructions.BorelSpace.Real

Goal state before:
pp: case hm
μ : Measure ℝ
inst✝ : IsFiniteMeasureOnCompacts μ
b : ℝ
⊢ ∀ (i j : ℝ), 0 < i → i ≤ j → Icc (b - i) (b + i) ⊆ Icc (b - j) (b + j)

Tactic:
intro r

Goal state after:
case hm
μ : Measure ℝ
inst✝ : IsFiniteMeasureOnCompacts μ
b r : ℝ
⊢ ∀ (j : ℝ), 0 < r → r ≤ j → Icc (b - r) (b + r) ⊆ Icc (b - j) (b + j)
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
motive : (α → ℝ≥0∞) → Prop
indicator : ∀ (c : ℝ≥0∞) ⦃s : Set α⦄, MeasurableSet s → μ s < ∞ → motive (s.indicator fun x ↦ c)
add :
  ∀ ⦃f g : α → ℝ≥0∞⦄,
    Disjoint (support f) (support g) → Measurable f → Measurable g → motive f → motive g → motive (f + g)
iSup :
  ∀ ⦃f : ℕ → α → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f n)) → Monotone f → (∀ (n : ℕ), motive (f n)) → motive fun x ↦ ⨆ n, f n x
f : α → ℝ≥0∞
hf : Measurable f
c : ℝ≥0∞
s : Set α
hs : MeasurableSet s
m n : ℕ
hmn : m ≤ n
a : α
⊢ (s ∩ spanningSets μ m).indicator (fun x ↦ c) a ≤ (s ∩ spanningSets μ n).indicator (fun x ↦ c) a

Tactic:
;

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
motive : (α → ℝ≥0∞) → Prop
indicator : ∀ (c : ℝ≥0∞) ⦃s : Set α⦄, MeasurableSet s → μ s < ∞ → motive (s.indicator fun x ↦ c)
add :
  ∀ ⦃f g : α → ℝ≥0∞⦄,
    Disjoint (support f) (support g) → Measurable f → Measurable g → motive f → motive g → motive (f + g)
iSup :
  ∀ ⦃f : ℕ → α → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f n)) → Monotone f → (∀ (n : ℕ), motive (f n)) → motive fun x ↦ ⨆ n, f n x
f : α → ℝ≥0∞
hf : Measurable f
c : ℝ≥0∞
s : Set α
hs : MeasurableSet s
m n : ℕ
hmn : m ≤ n
a : α
⊢ (s ∩ spanningSets μ m).indicator (fun x ↦ c) a ≤ (s ∩ spanningSets μ n).indicator (fun x ↦ c) a
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
A : ∀ (x : X × Y), Tendsto (fun n ↦ (g n) x) atTop (𝓝 (f x))
⊢ Measurable f

Tactic:
apply measurable_of_tendsto_metrizable (fun n ↦ (g n).measurable) (tendsto_pi_nhds.2 A)

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

Goal state before:
pp: case hfg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
y : α
⊢ ⨅ x, f x ≤ f y

Tactic:
;

Goal state after:
case hfg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
y : α
⊢ ⨅ x, f x ≤ f y
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: case hfg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
x : α
⊢ f x ≤ ⨆ x, f x

Tactic:
;

Goal state after:
case hfg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
x : α
⊢ f x ≤ ⨆ x, f x
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace β
m m₀ : MeasurableSpace α
μ : Measure α
f : α → β
m₀' : MeasurableSpace α
hm₀ : m₀' ≤ m₀
g : α → β
hg_meas : StronglyMeasurable g
hfg : f =ᵐ[μ.trim hm₀] g
⊢ AEStronglyMeasurable f μ

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace β
m m₀ : MeasurableSpace α
μ : Measure α
f : α → β
m₀' : MeasurableSpace α
hm₀ : m₀' ≤ m₀
g : α → β
hg_meas : StronglyMeasurable g
hfg : f =ᵐ[μ.trim hm₀] g
⊢ AEStronglyMeasurable f μ
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: case nil
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
M : Type u_5
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
hl : ∀ f ∈ [], AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable [].prod μ

Tactic:
exact aestronglyMeasurable_one

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

Goal state before:
pp: α : 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
p : ℝ≥0∞
⊢ ⇑(SimpleFunc.map c rs) ⁻¹' {p} = ⇑(SimpleFunc.map c rs) ⁻¹' {p} ∩ ⋃ i, {a | p ≤ f i a}

Tactic:
;

Goal state after:
α : 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
p : ℝ≥0∞
⊢ ⇑(SimpleFunc.map c rs) ⁻¹' {p} = ⇑(SimpleFunc.map c rs) ⁻¹' {p} ∩ ⋃ i, {a | p ≤ f i a}