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

Goal state before:
pp: α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hm : Monotone s
h : atTop.NeBot
this : IsDirectedOrder ι
⊢ Tendsto (⇑μ ∘ s) atTop (𝓝 (μ (⋃ n, s n)))

Tactic:
rw [hm.measure_iUnion]

Goal state after:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hm : Monotone s
h : atTop.NeBot
this : IsDirectedOrder ι
⊢ Tendsto (⇑μ ∘ s) atTop (𝓝 (⨆ i, μ (s i)))
Module: Mathlib.Order.Filter.CountableSeparatingOn

Goal state before:
pp: α : Type u_1
p : Set α → Prop
t : Set α
⊢ HasCountableSeparatingOn (↑t) (fun u ↦ ∃ v, p v ∧ Subtype.val ⁻¹' v = u) univ ↔ HasCountableSeparatingOn α p t

Tactic:
constructor <;> intro h
  · exact h.of_subtype <| fun s ↦ id
  rcases h with ⟨S, Sct, Sp, hS⟩
  use {Subtype.val ⁻¹' s | s ∈ S}, Sct.image _, ?_, ?_
  · rintro u ⟨t, tS, rfl⟩
    exact ⟨t, Sp _ tS, rfl⟩
  rintro x - y - hxy
  exact Subtype.val_injective <| hS _ (Subtype.coe_prop _) _ (Subtype.coe_prop _)
    fun s hs ↦ hxy (Subtype.val ⁻¹' s) ⟨s, hs, rfl⟩

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : t ⊆ s
h : NullMeasurableSet t (μ.restrict s)
t' : Set α
t'_subs : t' ⊆ t
ht' : MeasurableSet t'
t't : t' =ᵐ[μ.restrict s] t
this✝ : ∀ᵐ (x : α) ∂μ, x ∈ s → (x ∈ t' ↔ x ∈ t)
this : t' =ᵐ[μ] t
⊢ NullMeasurableSet t μ

Tactic:
exact ht'.nullMeasurableSet.congr this

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

Goal state before:
pp: case neg
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
t : Set β
ht : 0 ∉ t
⊢ μ ((f ⁻¹' t)ᶜ ∪ sᶜ) = 0 → t ∈ Filter.map f (ae (μ.restrict s))

Tactic:
mem_map_restrict_ae_iff hs

Goal state after:
case neg
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
t : Set β
ht : 0 ∉ t
⊢ μ ((f ⁻¹' t)ᶜ ∪ sᶜ) = 0 → μ ((f ⁻¹' t)ᶜ ∩ s) = 0
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case refine_1.compl.refine_2.refine_2
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
S : Finset (Set α)
hS_subset : ↑S ⊆ memPartition t n
ht✝ : MeasurableSet (⋃₀ ↑S)
⊢ Codisjoint (⋃₀ (memPartition t n \ ↑S)) (⋃₀ ↑S)

Tactic:
rw [codisjoint_iff]
          simp only [sup_eq_union, top_eq_univ]
          rw [← sUnion_memPartition t n, union_comm, ← sUnion_union, union_sdiff_cancel hS_subset]

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case refine_1.compl.refine_2
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
S : Finset (Set α)
hS_subset : ↑S ⊆ memPartition t n
ht✝ : MeasurableSet (⋃₀ ↑S)
⊢ (⋃₀ ↑S)ᶜ = ⋃₀ ↑((memPartition t n).toFinset \ S)

Tactic:
· simp only [Finset.coe_sdiff, coe_toFinset]
        refine (IsCompl.eq_compl ⟨?_, ?_⟩).symm
        · refine Set.disjoint_sUnion_right.mpr fun u huS => ?_
          refine Set.disjoint_sUnion_left.mpr fun v huV => ?_
          refine disjoint_memPartition t n (mem_of_mem_sdiff huV) (hS_subset huS) ?_
          exact ne_of_mem_of_not_mem huS (notMem_of_mem_sdiff huV) |>.symm
        · rw [codisjoint_iff]
          simp only [sup_eq_union, top_eq_univ]
          rw [← sUnion_memPartition t n, union_comm, ← sUnion_union, union_sdiff_cancel hS_subset]

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
m : MeasurableSpace α✝
h : CountablyGenerated α✝
α : Type u_3
γ : Type u_4
inst✝ : MeasurableSpace γ
hα : CountableOrCountablyGenerated α γ
hβ : CountableOrCountablyGenerated β γ
⊢ CountableOrCountablyGenerated (α × β) γ

Tactic:
rcases hα with (hα | hα) <;> rcases hβ with (hβ | hβ) <;> infer_instance

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

Goal state before:
pp: α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
inst✝ : Fintype ι
μ : ι → Measure α
⊢ sum μ = ∑ i, μ i

Tactic:
by
  ext1 s hs
  simp only [sum_apply, finsetSum_apply, hs, tsum_fintype]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
f : α → β
hc : MeasurableSpace.CountablyGenerated β
h : NullMeasurable f μ
⊢ AEMeasurable f μ

Tactic:
nontriviality β; inhabit β
  rcases hc.1 with ⟨S, hSc, rfl⟩
  choose! T hTf hTm hTeq using fun s hs ↦ (h <| .basic s hs).exists_measurable_subset_ae_eq
  choose! U hUf hUm hUeq using fun s hs ↦ (h <| .basic s hs).exists_measurable_superset_ae_eq
  set v := ⋃ s ∈ S, U s \ T s
  have hvm : MeasurableSet v := .biUnion hSc fun s hs ↦ (hUm s hs).diff (hTm s hs)
  have hvμ : μ v = 0 := (measure_biUnion_null_iff hSc).2 fun s hs ↦ ae_le_set.1 <|
    ((hUeq s hs).trans (hTeq s hs).symm).le
  refine ⟨v.piecewise (fun _ ↦ default) f, ?_, measure_mono_null (fun x ↦
    not_imp_comm.2 fun hxv ↦ (piecewise_eq_of_notMem _ _ _ hxv).symm) hvμ⟩
  refine measurable_of_restrict_of_restrict_compl hvm ?_ ?_
  · rw [domRestrict_piecewise]
    apply measurable_const
  · rw [domRestrict_piecewise_compl, domRestrict_eq]
    refine measurable_generateFrom fun s hs ↦ .of_subtype_image ?_
    rw [preimage_comp, Subtype.image_preimage_coe]
    convert! (hTm s hs).diff hvm using 1
    rw [inter_comm]
    refine Set.ext fun x ↦ and_congr_left fun hxv ↦ ⟨fun hx ↦ ?_, fun hx ↦ hTf s hs hx⟩
    exact by_contra fun hx' ↦ hxv <| mem_biUnion hs ⟨hUf s hs hx, hx'⟩

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

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
Y : Type u_2
inst✝¹ : TopologicalSpace Y
inst✝ : PseudoMetrizableSpace Y
f : X → Y
this : UniformSpace Y := pseudoMetrizableSpaceUniformity Y
⊢ IsGδ {x | ContinuousAt f x}

Tactic:
have := pseudoMetrizableSpaceUniformity_countably_generated Y

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
Y : Type u_2
inst✝¹ : TopologicalSpace Y
inst✝ : PseudoMetrizableSpace Y
f : X → Y
this✝ : UniformSpace Y := pseudoMetrizableSpaceUniformity Y
this : (uniformity Y).IsCountablyGenerated
⊢ IsGδ {x | ContinuousAt f x}
Module: Mathlib.Topology.Separation.GDelta

Goal state before:
pp: case h.left
X : Type u_1
inst✝¹ : TopologicalSpace X
s t : Set X
inst✝ : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed[inst✝¹] t
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen[inst✝¹] t
T_count : T.Countable
T_int : t = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → ↑T
g_surj : Surjective g
g' : ℕ → Set X
g'_open : ∀ (n : ℕ), IsOpen[inst✝¹] (g' n)
clt_sub_g' : ∀ (n : ℕ), t ⊆ g' n
clg'_sub_g : ∀ (n : ℕ), closure[inst✝¹] (g' n) ⊆ ↑(g n)
clg'_int : t = ⋂ i, closure[inst✝¹] (g' i)
⊢ s ⊆ (⋂ i, closure[inst✝¹] (g' i))ᶜ

Tactic:
subset_compl_comm,

Goal state after:
case h.left
X : Type u_1
inst✝¹ : TopologicalSpace X
s t : Set X
inst✝ : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed[inst✝¹] t
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen[inst✝¹] t
T_count : T.Countable
T_int : t = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → ↑T
g_surj : Surjective g
g' : ℕ → Set X
g'_open : ∀ (n : ℕ), IsOpen[inst✝¹] (g' n)
clt_sub_g' : ∀ (n : ℕ), t ⊆ g' n
clg'_sub_g : ∀ (n : ℕ), closure[inst✝¹] (g' n) ⊆ ↑(g n)
clg'_int : t = ⋂ i, closure[inst✝¹] (g' i)
⊢ ⋂ i, closure[inst✝¹] (g' i) ⊆ sᶜ
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: M : Type u_2
α : Type u_3
β : Type u_4
inst✝² : MeasurableSpace M
inst✝¹ : Mul M
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableMul₂ M
f g : α → β → M
h : α → β
hf : Measurable ↿f
hg : Measurable ↿g
hh : Measurable h
⊢ Measurable fun a ↦ (f a * g a) (h a)

Tactic:
by
  dsimp; fun_prop

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

Goal state before:
pp: G : Type u_2
α : Type u_3
β : Type u_4
inst✝² : MeasurableSpace G
inst✝¹ : Div G
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableDiv₂ G
f g : α → β → G
h : α → β
hf : Measurable ↿f
hg : Measurable ↿g
hh : Measurable h
⊢ Measurable fun a ↦ (f a / g a) (h a)

Tactic:
by
  dsimp; fun_prop

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

Goal state before:
pp: M : Type u_2
α : Type u_4
inst✝² : CommMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
l✝ : Multiset (α → M)
l : List (α → M)
hl : ∀ f ∈ Quot.mk (⇑(List.isSetoid (α → M))) l, Measurable f
⊢ ∀ f ∈ l, Measurable f

Tactic:
by simpa using hl

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

Goal state before:
pp: M : Type u_2
α : Type u_4
inst✝² : CommMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
l✝ : Multiset (α → M)
l : List (α → M)
hl : ∀ f ∈ Quot.mk (⇑(List.isSetoid (α → M))) l, AEMeasurable f μ
⊢ ∀ f ∈ l, AEMeasurable f μ

Tactic:
by simpa using hl

Goal state after:
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 α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : OpensMeasurableSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : OpensMeasurableSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : TopologicalSpace γ₂
inst✝² : MeasurableSpace γ₂
inst✝¹ : BorelSpace γ₂
inst✝ : MeasurableSpace δ
h : SecondCountableTopologyEither α β
s : Set (α × β)
hs : IsOpen[instTopologicalSpaceProd] s
hβ : SecondCountableTopology β
F : Set β → Set α := fun a ↦ {y | ∃ b, IsOpen[inst✝¹²] b ∧ y ∈ b ∧ b ×ˢ a ⊆ s}
A : ∀ (a : Set β), IsOpen[inst✝¹²] (F a)
this : s = ⋃ a ∈ countableBasis β, F a ×ˢ a
a : Set β
ha : a ∈ countableBasis β
⊢ MeasurableSet (F a ×ˢ a)

Tactic:
exact (A a).measurableSet.prod (isOpen_of_mem_countableBasis ha).measurableSet

Goal state after:
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:
rw [mem_cthickening_iff, ENNReal.ofReal_coe_nnreal] at hx hy

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

Goal state before:
pp: case e'_3.e'_2.mp
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s✝ : Set α
hd : Dense s✝
hbot : ∀ (x : α), IsTop x → x ∈ s✝
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s✝
e_1✝¹ : MeasurableSpace α = MeasurableSpace αᵒᵈ
e_1✝ : α = αᵒᵈ
s : Set α
⊢ s ∈ {S | ∃ l ∈ s✝, ∃ u ∈ s✝, l < u ∧ Ioc l u = S} →
    s ∈ {S | ∃ l ∈ ⇑OrderDual.ofDual ⁻¹' s✝, ∃ u ∈ ⇑OrderDual.ofDual ⁻¹' s✝, l < u ∧ Ico l u = S}

Tactic:
rintro ⟨l, hl, u, hu, hlt, rfl⟩

Goal state after:
case e'_3.e'_2.mp
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsTop x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
e_1✝¹ : MeasurableSpace α = MeasurableSpace αᵒᵈ
e_1✝ : α = αᵒᵈ
l : α
hl : l ∈ s
u : α
hu : u ∈ s
hlt : l < u
⊢ Ioc l u ∈ {S | ∃ l ∈ ⇑OrderDual.ofDual ⁻¹' s, ∃ u ∈ ⇑OrderDual.ofDual ⁻¹' s, l < u ∧ Ico l u = S}
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case e'_3.e'_2.mpr
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s✝ : Set α
hd : Dense s✝
hbot : ∀ (x : α), IsTop x → x ∈ s✝
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s✝
e_1✝¹ : MeasurableSpace α = MeasurableSpace αᵒᵈ
e_1✝ : α = αᵒᵈ
s : Set α
⊢ s ∈ {S | ∃ l ∈ ⇑OrderDual.ofDual ⁻¹' s✝, ∃ u ∈ ⇑OrderDual.ofDual ⁻¹' s✝, l < u ∧ Ico l u = S} →
    s ∈ {S | ∃ l ∈ s✝, ∃ u ∈ s✝, l < u ∧ Ioc l u = S}

Tactic:
rintro ⟨l, hl, u, hu, hlt, rfl⟩

Goal state after:
case e'_3.e'_2.mpr
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsTop x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
e_1✝¹ : MeasurableSpace α = MeasurableSpace αᵒᵈ
e_1✝ : α = αᵒᵈ
l : αᵒᵈ
hl : l ∈ ⇑OrderDual.ofDual ⁻¹' s
u : αᵒᵈ
hu : u ∈ ⇑OrderDual.ofDual ⁻¹' s
hlt : l < u
⊢ Ico l u ∈ {S | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ioc l u = S}
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
⊢ infDist x (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s) = infDist x s

Tactic:
by
  simp [infDist, infEDist_closure]

Goal state after:
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
δ : ℝ
hδ : 0 < δ
h : Disjoint (thickening δ s) (thickening δ t)
⊢ ∃ δ, 0 < δ ∧ Disjoint (cthickening δ s) (cthickening δ t)

Tactic:
refine ⟨δ / 2, half_pos hδ, h.mono ?_ ?_⟩

Goal state after:
case refine_1
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
δ : ℝ
hδ : 0 < δ
h : Disjoint (thickening δ s) (thickening δ t)
⊢ cthickening (δ / 2) s ⊆ thickening δ s

case refine_2
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
δ : ℝ
hδ : 0 < δ
h : Disjoint (thickening δ s) (thickening δ t)
⊢ cthickening (δ / 2) t ⊆ thickening δ t
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: case refine_1
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_nn : 0 ≤ δ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
ε : ℝ
hε : ε ∈ s
⊢ cthickening δ E ⊆ thickening ε E

Tactic:
obtain ⟨ε', -, hε'⟩ := hs ε (hsδ hε)
    have ss := cthickening_subset_thickening' (lt_of_le_of_lt δ_nn hε'.1) hε'.1 E
    exact ss.trans (thickening_mono hε'.2 E)

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

Goal state before:
pp: case inr
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
h : s.Nonempty
⊢ hausdorffDist s ∅ = 0

Tactic:
· simp [hausdorffDist, hausdorffEDist_empty h]

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

Goal state before:
pp: α : Type u_5
m : MeasurableSpace α
inst✝ : CountablySeparated α
m' : MeasurableSpace α
left✝³ : CountablyGenerated α
left✝² : MeasurableSpace.SeparatesPoints α
m'le : m' ≤ m
τ : TopologicalSpace α
left✝¹ : SecondCountableTopology α
left✝ : T4Space α
τm' : BorelSpace α
⊢ ∃ x, SecondCountableTopology α ∧ T4Space α ∧ OpensMeasurableSpace α

Tactic:
exact ⟨τ, ‹_›, ‹_›, @OpensMeasurableSpace.mk _ _ m (τm'.measurable_eq.symm.le.trans m'le)⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
hf_meas : Measurable f
a : α
⊢ Tendsto (fun n ↦ (eapprox f n) a) atTop (𝓝 (⨆ i, (eapprox f i) a))

Tactic:
exact tendsto_atTop_iSup fun _ _ hnm ↦ monotone_eapprox f hnm a

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
a : α
hb : f a ∈ f.range
⊢ ∀ x ∈ {j ∈ f.range | g j = g (f a)}, g (f a) * μ (⇑f ⁻¹' {x}) = g x * μ (⇑f ⁻¹' {x})

Tactic:
· grind

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

Goal state before:
pp: ι : Type u_1
inst✝² : Preorder ι
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x1 x2 ↦ x1 ≤ x2
f : ι → ℝ
x : ℝ
h_tto : Tendsto f atTop (𝓝 x)
h_mon : Monotone f
h_bdd : BddAbove (range f)
⊢ IsLUB (range f) x

Tactic:
tendsto_nhds_unique h_tto (tendsto_atTop_ciSup h_mon h_bdd)

Goal state after:
ι : Type u_1
inst✝² : Preorder ι
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x1 x2 ↦ x1 ≤ x2
f : ι → ℝ
x : ℝ
h_tto : Tendsto f atTop (𝓝 x)
h_mon : Monotone f
h_bdd : BddAbove (range f)
⊢ IsLUB (range f) (⨆ i, f i)
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)
mc_meas : MeasurableSet {x | ∀ (j : Subtype p), x ∉ m j}
j : Subtype p
reparam : δ → Subtype p → Subtype p := fun x ↦ liminfReparam (fun i ↦ f i x) s p
F0 : Subtype p → δ → α := fun j x ↦ ⨅ i, f (↑i) x
F0_meas : ∀ (j : Subtype p), Measurable (F0 j)
F1 : δ → α := fun x ↦ F0 (reparam x j) x
hF1 : F1 = fun x ↦ F0 (reparam x j) x
g : ℕ → Subtype p := Classical.choose ⋯
Z : ∀ (x : δ), ∃ n, x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k
x : δ
A : reparam x j = if x ∈ m j then j else g (Nat.find ⋯)
hjx : x ∉ m j
⊢ F1 x = F0 (g (Nat.find ⋯)) x

Tactic:
· have : reparam x j = g (Nat.find (Z x)) := by rw [A, if_neg hjx]
      simp only [hF1, this]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : PseudoEMetricSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace β
f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
x : β
m n : ℕ
h : m ≤ n
⊢ edist ((nearestPt (fun k ↦ Nat.rec y₀ (fun n n_ih ↦ ↑(denseSeq (↑s) n)) k) n) (f x)) (f x) ≤
    edist ((nearestPt (fun k ↦ Nat.rec y₀ (fun n n_ih ↦ ↑(denseSeq (↑s) n)) k) m) (f x)) (f x)

Tactic:
exact edist_nearestPt_le _ _ ((nearestPtInd_le _ _ _).trans 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)
⊢ μ (s ∩ f ⁻¹' Ioi 0) = μ (s ∩ f ⁻¹' {∞} ∪ s ∩ f ⁻¹' Ioo 0 ∞)

Tactic:
rw [← inter_union_distrib_left]
      congr
      ext x
      simp only [mem_singleton_iff, mem_union, mem_Ioo, mem_Ioi, mem_preimage]
      obtain (H | H) : f x = ∞ ∨ f x < ∞ := eq_or_lt_of_le le_top
      · simp only [H, or_false, ENNReal.zero_lt_top, not_top_lt, and_false]
      · simp only [H, H.ne, and_true, false_or]

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

Goal state before:
pp: case hn
α : 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 ∞)
⊢ Pairwise (Function.onFun Disjoint fun n ↦ s ∩ f ⁻¹' Ico (↑t ^ n) (↑t ^ (n + 1)))

pp: case h
α : 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 : ℤ), MeasurableSet (s ∩ f ⁻¹' Ico (↑t ^ i) (↑t ^ (i + 1)))

Tactic:
· intro i j hij
      wlog h : i < j generalizing i j
      · exact (this hij.symm (hij.lt_or_gt.resolve_left h)).symm
      refine disjoint_left.2 fun x hx h'x => lt_irrefl (f x) ?_
      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:
case h
α : 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 : ℤ), MeasurableSet (s ∩ f ⁻¹' Ico (↑t ^ i) (↑t ^ (i + 1)))
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
l✝ : Multiset (α → M)
l : List (α → M)
hl : ∀ f ∈ Quot.mk (⇑(List.isSetoid (α → M))) l, AEStronglyMeasurable f μ
⊢ ∀ f ∈ l, AEStronglyMeasurable f μ

Tactic:
by simpa using hl

Goal state after:
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
this :
  ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ <
    (⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ) + ε
⊢ ∃ φ,
    (∀ (x : α), ↑(φ x) ≤ f x) ∧
      ∀ (ψ : α →ₛ ℝ≥0), (∀ (x : α), ↑(ψ x) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε

Tactic:
ENNReal.biSup_add

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
this :
  ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ <
    ⨆ i ∈ fun φ ↦ ∀ (x : α), ↑(φ x) ≤ f x, (SimpleFunc.map ofNNReal i).lintegral μ + ε
⊢ ∃ φ,
    (∀ (x : α), ↑(φ x) ≤ f x) ∧
      ∀ (ψ : α →ₛ ℝ≥0), (∀ (x : α), ↑(ψ x) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε

case hs
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
this :
  ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ <
    (⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ) + ε
⊢ Set.Nonempty fun φ ↦ ∀ (x : α), ↑(φ x) ≤ f x
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∫⁻ (a : α), f a ∂μ = 0
ε : ℝ≥0∞
εpos : ε > 0
h' : μ {x | ε ≤ f x} ≠ 0
⊢ ε * μ {x | ε ≤ f x} ≤ ∫⁻ (a : α), f a ∂μ

Tactic:
calc
      _ ≥ ∫⁻ a in {x | ε ≤ f x}, f a ∂μ := setLIntegral_le_lintegral _ _
      _ ≥ ∫⁻ _ in {x | ε ≤ f x}, ε ∂μ :=
        setLIntegral_mono_ae hf.restrict (ae_of_all μ fun _ ↦ id)
      _ = _ := setLIntegral_const _ _

Goal state after:
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : Zero β
inst✝ : T2Space β
g : α → β
hg : FinStronglyMeasurable g μ
hfg : f =ᵐ[μ] g
t : Set α
ht : MeasurableSet t
hgt_zero : ∀ x ∈ tᶜ, g x = 0
htμ : SigmaFinite (μ.restrict t)
⊢ g =ᵐ[μ.restrict tᶜ] 0

Tactic:
rw [EventuallyEq, ae_restrict_iff' ht.compl]

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : Zero β
inst✝ : T2Space β
g : α → β
hg : FinStronglyMeasurable g μ
hfg : f =ᵐ[μ] g
t : Set α
ht : MeasurableSet t
hgt_zero : ∀ x ∈ tᶜ, g x = 0
htμ : SigmaFinite (μ.restrict t)
⊢ ∀ᵐ (x : α) ∂μ, x ∈ tᶜ → g x = 0 x
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hsm : MeasurableSet s
hfs : ∫⁻ (x : α) in s, f x ∂μ ≠ ∞
⊢ ∫⁻ (x : α) in sᶜ, f x ∂μ = ∫⁻ (x : α) in s, f x ∂μ + ∫⁻ (x : α) in sᶜ, f x ∂μ - ∫⁻ (x : α) in s, f x ∂μ

Tactic:
ENNReal.add_sub_cancel_left hfs

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hsm : MeasurableSet s
hfs : ∫⁻ (x : α) in s, f x ∂μ ≠ ∞
⊢ ∫⁻ (x : α) in sᶜ, f x ∂μ = ∫⁻ (x : α) in sᶜ, f x ∂μ