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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν✝ ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝³ : SMul R ℝ≥0∞
inst✝² : LE R
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : IsOrderedSMul R ℝ≥0∞
μ ν : Measure α
hμν : μ ≤ ν
a : R
s : Set α
⊢ (a • μ) s ≤ (a • ν) s

Tactic:
gcongr

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝³ : SMul R ℝ≥0∞
inst✝² : LE R
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : IsOrderedSMul R ℝ≥0∞
a b : R
hab : a ≤ b
μ : Measure α
s : Set α
⊢ a • μ s ≤ b • μ s

Tactic:
gcongr

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

Goal state before:
pp: α : Type u_2
δ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
f g : α → δ
s : Set α
hfg : f =ᵐ[μ] g
⊢ ae (μ.restrict s) ≤ ae μ

Tactic:
Measure.ae_le_iff_absolutelyContinuous

Goal state after:
α : Type u_2
δ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
f g : α → δ
s : Set α
hfg : f =ᵐ[μ] g
⊢ μ.restrict s ≪ μ
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
m : Set (Measure α)
x✝ : MeasurableSpace α
f : ℕ → Set α
a✝¹ : ∀ (i : ℕ), MeasurableSet (f i)
a✝ : Pairwise (Disjoint on f)
hne : (⋃ i, f i).Nonempty
⊢ ∑' (i : ℕ), ⊤ (f i) ≤ ∞

Tactic:
exact le_top

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : μ ({a | ¬f a = b} ∩ sᶜ) = 0
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
⊢ μ (f ⁻¹' t ∩ sᶜ) ≤ μ ({a | ¬f a = b} ∩ sᶜ)

Tactic:
gcongr

Goal state after:
case h₁
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : μ ({a | ¬f a = b} ∩ sᶜ) = 0
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
⊢ f ⁻¹' t ⊆ {a | ¬f a = b}
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: case pos
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ n, v n
h'v : ∀ (n : ℕ), μ (t ∩ v n) ≠ ∞
A : ∃ t' ⊇ t, MeasurableSet t' ∧ ∀ (u : Set α), MeasurableSet u → μ (t' ∩ u) = μ (t ∩ u)
ht : ∃ t_1 ⊇ t, MeasurableSet t_1 ∧ t_1 =ᵐ[μ] t
⊢ μ (ht.choose ∩ s) = μ (t ∩ s)

pp: case neg
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ n, v n
h'v : ∀ (n : ℕ), μ (t ∩ v n) ≠ ∞
A : ∃ t' ⊇ t, MeasurableSet t' ∧ ∀ (u : Set α), MeasurableSet u → μ (t' ∩ u) = μ (t ∩ u)
ht : ¬∃ t_1 ⊇ t, MeasurableSet t_1 ∧ t_1 =ᵐ[μ] t
⊢ μ (A.choose ∩ s) = μ (t ∩ s)

Tactic:
· apply measure_congr
    exact ae_eq_set_inter ht.choose_spec.2.2 (ae_eq_refl _)

Goal state after:
case neg
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ n, v n
h'v : ∀ (n : ℕ), μ (t ∩ v n) ≠ ∞
A : ∃ t' ⊇ t, MeasurableSet t' ∧ ∀ (u : Set α), MeasurableSet u → μ (t' ∩ u) = μ (t ∩ u)
ht : ¬∃ t_1 ⊇ t, MeasurableSet t_1 ∧ t_1 =ᵐ[μ] t
⊢ μ (A.choose ∩ s) = μ (t ∩ s)
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
h : ∀ᵐ (x : α) (y : α) ∂μ, f x = f y
⊢ AEMeasurable f μ

Tactic:
rcases eq_or_ne μ 0 with (rfl | hμ)

Goal state after:
case inl
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
h : ∀ᵐ (x : α) (y : α) ∂0, f x = f y
⊢ AEMeasurable f 0

case inr
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
h : ∀ᵐ (x : α) (y : α) ∂μ, f x = f y
hμ : μ ≠ 0
⊢ AEMeasurable f μ
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
a✝ : Nontrivial β
inhabited_h : Inhabited β
S : Set (Set β)
hSc : S.Countable
hc : MeasurableSpace.CountablyGenerated β
h : NullMeasurable f μ
T : Set β → Set α
hTf : ∀ s ∈ S, T s ⊆ f ⁻¹' s
hTm : ∀ s ∈ S, MeasurableSet (T s)
hTeq : ∀ s ∈ S, T s =ᵐ[μ] f ⁻¹' s
U : Set β → Set α
hUf : ∀ s ∈ S, U s ⊇ f ⁻¹' s
hUm : ∀ s ∈ S, MeasurableSet (U s)
hUeq : ∀ s ∈ S, U s =ᵐ[μ] f ⁻¹' s
⊢ AEMeasurable f μ

Tactic:
set v := ⋃ s ∈ S, U s \ T s

Goal state after:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
a✝ : Nontrivial β
inhabited_h : Inhabited β
S : Set (Set β)
hSc : S.Countable
hc : MeasurableSpace.CountablyGenerated β
h : NullMeasurable f μ
T : Set β → Set α
hTf : ∀ s ∈ S, T s ⊆ f ⁻¹' s
hTm : ∀ s ∈ S, MeasurableSet (T s)
hTeq : ∀ s ∈ S, T s =ᵐ[μ] f ⁻¹' s
U : Set β → Set α
hUf : ∀ s ∈ S, U s ⊇ f ⁻¹' s
hUm : ∀ s ∈ S, MeasurableSet (U s)
hUeq : ∀ s ∈ S, U s =ᵐ[μ] f ⁻¹' s
v : Set α := ⋃ s ∈ S, U s \ T s
⊢ AEMeasurable f μ
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
⊢ m0 ≤ ⊤

Tactic:
exact le_top

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
inst✝¹ : Preorder α
inst✝ : atTop.IsCountablyGenerated
μ : Measure α
⊢ Tendsto (fun x ↦ μ (Iic x)) atTop (𝓝 (μ univ))

Tactic:
by
  rw [← iUnion_Iic]
  exact tendsto_measure_iUnion_atTop monotone_Iic

Goal state after:
Module: Mathlib.Topology.Separation.GDelta

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PerfectlyNormalSpace X
x y : X
hxy : x ⤳ y
K : Set X
hyK : y ∈ K
hK : IsGδ K
⊢ x ∈ K

Tactic:
obtain ⟨Ts, hoTs, -, rfl⟩ := hK

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PerfectlyNormalSpace X
x y : X
hxy : x ⤳ y
Ts : Set (Set X)
hoTs : ∀ t ∈ Ts, IsOpen[inst✝²] t
hyK : y ∈ ⋂₀ Ts
⊢ x ∈ ⋂₀ Ts
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s t u : Set α
⊢ hausdorffEDist s u ≤ hausdorffEDist s t + hausdorffEDist t u

Tactic:
by
  rw [hausdorffEDist_def]
  simp only [sup_le_iff, iSup_le_iff]
  constructor
  · change ∀ x ∈ s, infEDist x u ≤ hausdorffEDist s t + hausdorffEDist t u
    exact fun x xs =>
      calc
        infEDist x u ≤ infEDist x t + hausdorffEDist t u :=
          infEDist_le_infEDist_add_hausdorffEDist
        _ ≤ hausdorffEDist s t + hausdorffEDist t u := by grw [infEDist_le_hausdorffEDist_of_mem xs]
  · change ∀ x ∈ u, infEDist x s ≤ hausdorffEDist s t + hausdorffEDist t u
    exact fun x xu =>
      calc
        infEDist x s ≤ infEDist x t + hausdorffEDist t s :=
          infEDist_le_infEDist_add_hausdorffEDist
        _ ≤ hausdorffEDist u t + hausdorffEDist t s := by grw [infEDist_le_hausdorffEDist_of_mem xu]
        _ = hausdorffEDist s t + hausdorffEDist t u := by simp [hausdorffEDist_comm, add_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mβ : TopologicalSpace β
inst✝² : MeasurableSpace β
inst✝¹ : BorelSpace β
μ : Measure α
inst✝ : IsFiniteMeasureOnCompacts μ
f : α ≃ₜ β
⊢ IsFiniteMeasureOnCompacts (map (⇑f) μ)

Tactic:
refine ⟨fun K hK ↦ ?_⟩
  rw [← f.toMeasurableEquiv_coe, MeasurableEquiv.map_apply]
  exact IsCompact.measure_lt_top (f.isCompact_preimage.2 hK)

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

Goal state before:
pp: α : Type u_2
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
h : Bornology.IsBounded E
⊢ Bornology.IsBounded (Metric.cthickening δ E)

Tactic:
have : IsBounded (thickening (max (δ + 1) 1) E) := h.thickening

Goal state after:
α : Type u_2
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
h : Bornology.IsBounded E
this : Bornology.IsBounded (thickening (max (δ + 1) 1) E)
⊢ Bornology.IsBounded (Metric.cthickening δ E)
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: case neg.inr
ε : ℝ
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
hε✝ : 0 ≤ ε
hs : ¬Bornology.IsBounded s
hε : 0 < ε
⊢ diam (thickening ε s) ≤ diam s + 2 * ε

Tactic:
rw [diam_eq_zero_of_unbounded (mt (IsBounded.subset · <| self_subset_thickening hε _) hs)]

Goal state after:
case neg.inr
ε : ℝ
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
hε✝ : 0 ≤ ε
hs : ¬Bornology.IsBounded s
hε : 0 < ε
⊢ 0 ≤ diam s + 2 * ε
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: case inr
α : Type u_2
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
hne : E.Nonempty
x : α
hx : x ∈ cthickening δ E
⊢ x ∈ ⋃ x ∈ E, closedBall x δ

Tactic:
obtain ⟨y, yE, hy⟩ : ∃ y ∈ E, infEDist x E = edist x y := hE.exists_infEDist_eq_edist hne _

Goal state after:
case inr
α : Type u_2
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
hne : E.Nonempty
x : α
hx : x ∈ cthickening δ E
y : α
yE : y ∈ E
hy : infEDist x E = edist x y
⊢ x ∈ ⋃ x ∈ E, closedBall x δ
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, ∃ y ∈ t, dist x y ≤ r
H2 : ∀ x ∈ t, ∃ y ∈ s, dist x y ≤ r
⊢ hausdorffDist s t ≤ r

Tactic:
apply hausdorffDist_le_of_infDist hr
  · intro x xs
    rcases H1 x xs with ⟨y, yt, hy⟩
    exact le_trans (infDist_le_dist_of_mem yt) hy
  · intro x xt
    rcases H2 x xt with ⟨y, ys, hy⟩
    exact le_trans (infDist_le_dist_of_mem ys) hy

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set α
x : α
⊢ infEDist x (cthickening ?m.15 s) + ENNReal.ofReal ?m.15 ≤ infEDist x (thickening δ s) + ENNReal.ofReal δ

Tactic:
gcongr

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
f : α →ₛ β
p : β → Prop
⊢ (∃ y ∈ f.range, p y) ↔ ∃ x, p (f x)

Tactic:
by
  simpa only [mem_range, exists_prop] using Set.exists_range_iff

Goal state after:
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
s t : Set α
ε₁ : ℝ
hε₁ : ε₁ > 0
V₁ : Set α
hV₁ : V₁ ∈ 𝓝ˢ s
hV₁thickening : thickening ε₁ (f '' V₁) ⊆ U
ε₂ : ℝ
hε₂ : ε₂ > 0
V₂ : Set α
hV₂ : V₂ ∈ 𝓝ˢ t
hV₂thickening : thickening ε₂ (f '' V₂) ⊆ U
⊢ thickening (min ε₁ ε₂) (f '' V₁) ∪ thickening (min ε₁ ε₂) (f '' V₂) ⊆
    thickening ε₁ (f '' V₁) ∪ thickening ε₂ (f '' V₂)

Tactic:
gcongr

Goal state after:
case hle
α : 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
s t : Set α
ε₁ : ℝ
hε₁ : ε₁ > 0
V₁ : Set α
hV₁ : V₁ ∈ 𝓝ˢ s
hV₁thickening : thickening ε₁ (f '' V₁) ⊆ U
ε₂ : ℝ
hε₂ : ε₂ > 0
V₂ : Set α
hV₂ : V₂ ∈ 𝓝ˢ t
hV₂thickening : thickening ε₂ (f '' V₂) ⊆ U
⊢ min ε₁ ε₂ ≤ ε₁

case hle
α : 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
s t : Set α
ε₁ : ℝ
hε₁ : ε₁ > 0
V₁ : Set α
hV₁ : V₁ ∈ 𝓝ˢ s
hV₁thickening : thickening ε₁ (f '' V₁) ⊆ U
ε₂ : ℝ
hε₂ : ε₂ > 0
V₂ : Set α
hV₂ : V₂ ∈ 𝓝ˢ t
hV₂thickening : thickening ε₂ (f '' V₂) ⊆ U
⊢ min ε₁ ε₂ ≤ ε₂
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
s t : Set α
ε₁ : ℝ
hε₁ : ε₁ > 0
V₁ : Set α
hV₁ : V₁ ∈ 𝓝ˢ s
hV₁thickening : thickening ε₁ (f '' V₁) ⊆ U
ε₂ : ℝ
hε₂ : ε₂ > 0
V₂ : Set α
hV₂ : V₂ ∈ 𝓝ˢ t
hV₂thickening : thickening ε₂ (f '' V₂) ⊆ U
⊢ thickening ε₁ (f '' V₁) ∪ thickening ε₂ (f '' V₂) ⊆ U ∪ U

Tactic:
gcongr

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

Goal state before:
pp: case left
α : Type u_1
m : MeasurableSpace α
ι : Type u_5
inst✝ : Countable ι
f : α →ₛ ℝ≥0∞
s : ι → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
μ : Measure α
i j k : ι
x✝ : (fun x1 x2 ↦ x1 ⊆ x2) (s i) (s k) ∧ (fun x1 x2 ↦ x1 ⊆ x2) (s j) (s k)
hik : (fun x1 x2 ↦ x1 ⊆ x2) (s i) (s k)
hjk : (fun x1 x2 ↦ x1 ⊆ x2) (s j) (s k)
a : ℝ≥0∞
⊢ a * (μ.restrict (s i)) (⇑f ⁻¹' {a}) ≤ a * (μ.restrict (s k)) (⇑f ⁻¹' {a})

Tactic:
gcongr

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

Goal state before:
pp: case right
α : Type u_1
m : MeasurableSpace α
ι : Type u_5
inst✝ : Countable ι
f : α →ₛ ℝ≥0∞
s : ι → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
μ : Measure α
i j k : ι
x✝ : (fun x1 x2 ↦ x1 ⊆ x2) (s i) (s k) ∧ (fun x1 x2 ↦ x1 ⊆ x2) (s j) (s k)
hik : (fun x1 x2 ↦ x1 ⊆ x2) (s i) (s k)
hjk : (fun x1 x2 ↦ x1 ⊆ x2) (s j) (s k)
a : ℝ≥0∞
⊢ a * (μ.restrict (s j)) (⇑f ⁻¹' {a}) ≤ a * (μ.restrict (s k)) (⇑f ⁻¹' {a})

Tactic:
gcongr

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

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

Tactic:
gcongr

Goal state after:
case h₁
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f✝ g✝ : α →ₛ ℝ≥0∞
h : f✝ ≤ g✝
f g : α →ₛ ℝ≥0∞
x : ℝ≥0∞ × ℝ≥0∞
a✝ : x ∈ (f.pair g).range
⊢ x.1 ≤ max x.1 x.2
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f : α →ₛ ℝ≥0∞
h : μ ≤ ν
⊢ ∑ x ∈ f.range, x * μ (⇑f ⁻¹' {x}) ≤ ∑ x ∈ f.range, x * ν (⇑f ⁻¹' {x})

Tactic:
gcongr

Goal state after:
Module: Mathlib.Topology.IndicatorConstPointwise

Goal state before:
pp: case pos
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst✝¹ : DecidablePred p
q : Prop
inst✝ : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
h : ∀ᶠ (i : ι) in L, p i ↔ q
obs : (fun x ↦ if q then a else b) =ᶠ[L] fun i ↦ if p i then a else b
hq : q
⊢ Tendsto (fun x ↦ if q then a else b) L (if q then F else G)

Tactic:
simp only [hq, ite_true]

Goal state after:
case pos
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst✝¹ : DecidablePred p
q : Prop
inst✝ : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
h : ∀ᶠ (i : ι) in L, p i ↔ q
obs : (fun x ↦ if q then a else b) =ᶠ[L] fun i ↦ if p i then a else b
hq : q
⊢ Tendsto (fun x ↦ a) L F
Module: Mathlib.Topology.IndicatorConstPointwise

Goal state before:
pp: α : Type u_1
A : Set α
β : Type u_2
inst✝¹ : Zero β
inst✝ : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhds_b : {0}ᶜ ∈ 𝓝 b
nhds_o : {b}ᶜ ∈ 𝓝 0
⊢ ∀ (a : α),
    Tendsto (fun i ↦ (As i).indicator (fun x ↦ b) a) L (𝓝 (A.indicator (fun x ↦ b) a)) ↔
      ∀ᶠ (i : ι) in L, a ∈ As i ↔ a ∈ A

Tactic:
exact tendsto_indicator_const_apply_iff_eventually' L b nhds_b nhds_o

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

Goal state before:
pp: case neg
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_5
ι' : Type u_6
f : ι → δ → α
v : Filter ι
hf : ∀ (i : ι), Measurable (f i)
p : ι' → Prop
s : ι' → Set ι
hv : v.HasCountableBasis p s
hs : ∀ (j : ι'), (s j).Countable
this✝ : Countable (Subtype p)
hp : Nonempty (Subtype p)
H : ¬∃ j, s ↑j = ∅
this : ∀ (i : ι'), Countable ↑(s i)
m : Subtype p → Set δ := fun j ↦ {x | BddBelow (range fun i ↦ f (↑i) x)}
m_meas : ∀ (j : Subtype p), MeasurableSet (m j)
⊢ Measurable fun x ↦ if ∀ (j : Subtype p), ¬BddBelow (range fun i ↦ f (↑i) x) then sSup ∅ else ⨆ j, ⨅ i, f (↑i) x

Tactic:
have mc_meas : MeasurableSet {x | ∀ (j : Subtype p), x ∉ m j} := by
    rw [ofPred_forall]
    exact MeasurableSet.iInter (fun j ↦ (m_meas j).compl)

Goal state after:
case neg
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_5
ι' : Type u_6
f : ι → δ → α
v : Filter ι
hf : ∀ (i : ι), Measurable (f i)
p : ι' → Prop
s : ι' → Set ι
hv : v.HasCountableBasis p s
hs : ∀ (j : ι'), (s j).Countable
this✝ : Countable (Subtype p)
hp : Nonempty (Subtype p)
H : ¬∃ j, s ↑j = ∅
this : ∀ (i : ι'), Countable ↑(s i)
m : Subtype p → Set δ := fun j ↦ {x | BddBelow (range fun i ↦ f (↑i) x)}
m_meas : ∀ (j : Subtype p), MeasurableSet (m j)
mc_meas : MeasurableSet {x | ∀ (j : Subtype p), x ∉ m j}
⊢ Measurable fun x ↦ if ∀ (j : Subtype p), ¬BddBelow (range fun i ↦ f (↑i) x) then sSup ∅ else ⨆ j, ⨅ i, f (↑i) x
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : 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)
f : α →ₛ γ
s : Finset γ
h : f.range \ {0} = s
⊢ motive f

Tactic:
rw [← Finset.coe_inj, Finset.coe_sdiff, Finset.coe_singleton, SimpleFunc.coe_range] at h

Goal state after:
α : 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)
f : α →ₛ γ
s : Finset γ
h : range ⇑f \ {0} = ↑s
⊢ motive f
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
hf : ∀ (i : ι), Measurable (f i)
lim : ∀ (x : α), Tendsto (fun i ↦ f i x) u (𝓝 (g x))
x : ℕ → ι
hx : Tendsto x atTop u
⊢ Measurable g

Tactic:
have : (fun y => liminf (fun n => (f (x n) y : ℝ≥0∞)) atTop) = g := by
    ext1 y
    exact ((lim y).comp hx).liminf_eq

Goal state after:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0∞
g : α → ℝ≥0∞
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : ∀ (x : α), Tendsto (fun i ↦ f i x) u (𝓝 (g x))
x : ℕ → ι
hx : Tendsto x atTop u
this : (fun y ↦ liminf (fun n ↦ f (x n) y) atTop) = g
⊢ Measurable g
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
inst✝ : Countable ι
f : ι → α → ℝ≥0
h : ∀ (i : ι), Measurable (f i)
⊢ Measurable fun x ↦ ∑' (i : ι), f i x

Tactic:
simp_rw [NNReal.tsum_eq_toNNReal_tsum]
  exact (Measurable.ennreal_tsum fun i => (h i).coe_nnreal_ennreal).ennreal_toNNReal

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

Goal state before:
pp: α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : Nonempty γ
P : (α →ₛ γ) → Prop
const : ∀ (c : γ), P (SimpleFunc.const α c)
pcw : ∀ ⦃f g : α →ₛ γ⦄ {s : Set α} (hs : MeasurableSet s), P f → P g → P (piecewise s hs f g)
f : α →ₛ γ
c : γ := Classical.ofNonempty
s : Finset γ
h : f.range \ {c} = s
⊢ P f

Tactic:
rw [← Finset.coe_inj, Finset.coe_sdiff, Finset.coe_singleton, SimpleFunc.coe_range] at h

Goal state after:
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : Nonempty γ
P : (α →ₛ γ) → Prop
const : ∀ (c : γ), P (SimpleFunc.const α c)
pcw : ∀ ⦃f g : α →ₛ γ⦄ {s : Set α} (hs : MeasurableSet s), P f → P g → P (piecewise s hs f g)
f : α →ₛ γ
c : γ := Classical.ofNonempty
s : Finset γ
h : range ⇑f \ {c} = ↑s
⊢ P f
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: μ : Measure ℝ
inst✝ : IsFiniteMeasureOnCompacts μ
b : ℝ
⊢ Tendsto (fun δ ↦ μ (Icc (b - δ) (b + δ))) (𝓝[>] 0) (𝓝 (μ {b}))

Tactic:
rw [Real.singleton_eq_inter_Icc]
  apply tendsto_measure_biInter_gt (fun r hr ↦ nullMeasurableSet_Icc)
  · intro r s _rpos hrs
    exact Icc_subset_Icc (by linarith) (by linarith)
  · exact ⟨1, zero_lt_one, isCompact_Icc.measure_ne_top⟩

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

Goal state before:
pp: case pos
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✝ : PseudoMetricSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
ε : ℝ
hε : 0 < ε
K : Set (X × Y)
hK : IsCompact K
t t' : Set (X × Y)
g : SimpleFunc (X × Y) α
s : Set (X × Y)
s_meas : MeasurableSet s
ts : t ⊆ s
hg : ∀ x ∈ s, dist (f x) (g x) < ε
g' : SimpleFunc (X × Y) α
s' : Set (X × Y)
s'_meas : MeasurableSet s'
t's' : t' ⊆ s'
hg' : ∀ x ∈ s', dist (f x) (g' x) < ε
p : X × Y
hp : p ∈ s ∪ s'
H : p ∈ s
⊢ dist (f p) ((SimpleFunc.piecewise s s_meas g g') p) < ε

Tactic:
simpa [H, SimpleFunc.piecewise_apply] using hg p H

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

Goal state before:
pp: case pos
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✝ : PseudoMetricSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
ε : ℝ
hε : 0 < ε
M : ∀ (K : Set (X × Y)), IsCompact K → ∃ g s, MeasurableSet s ∧ K ⊆ s ∧ ∀ x ∈ s, dist (f x) (g x) < ε
g : SimpleFunc (X × Y) α
s : Set (X × Y)
s_meas : MeasurableSet s
fs : tsupport f ⊆ s
hg : ∀ x ∈ s, dist (f x) (g x) < ε
p : X × Y
H : p ∈ s
⊢ dist (f p) ((SimpleFunc.piecewise s s_meas g 0) p) < ε

Tactic:
simpa [H, SimpleFunc.piecewise_apply] using hg p H

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

Goal state before:
pp: α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A : μ s = μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' Ioi 0)
B : μ (s ∩ f ⁻¹' Ioi 0) = μ (s ∩ f ⁻¹' {∞}) + μ (s ∩ f ⁻¹' Ioo 0 ∞)
i j : ℤ
hij : i ≠ j
h : i < j
x : α
hx : x ∈ (fun n ↦ s ∩ f ⁻¹' Ico (↑t ^ n) (↑t ^ (n + 1))) i
h'x : x ∈ (fun n ↦ s ∩ f ⁻¹' Ico (↑t ^ n) (↑t ^ (n + 1))) j
⊢ f x < f x

Tactic:
calc
        f x < (t : ℝ≥0∞) ^ (i + 1) := hx.2.2
        _ ≤ (t : ℝ≥0∞) ^ j := ENNReal.zpow_le_of_le (ENNReal.one_le_coe_iff.2 ht.le) h
        _ ≤ f x := h'x.2.1

Goal state after: