mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Order.AtTopBotIxx

Goal state before:
pp: case pos.mp
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
b : X
hsne : s.Nonempty
this✝ : Nonempty ↑s
hsub : s ⊆ Iio b
h : comap Subtype.val (𝓝[<] b) = atTop
a : X
ha : a < b
this : Subtype.val ⁻¹' Ioo a b ∈ atTop
⊢ (s ∩ Ioo a b).Nonempty

Tactic:
rcases Filter.nonempty_of_mem this with ⟨⟨c, hcs⟩, hc⟩

Goal state after:
case pos.mp
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
b : X
hsne : s.Nonempty
this✝ : Nonempty ↑s
hsub : s ⊆ Iio b
h : comap Subtype.val (𝓝[<] b) = atTop
a : X
ha : a < b
this : Subtype.val ⁻¹' Ioo a b ∈ atTop
c : X
hcs : c ∈ s
hc : ⟨c, hcs⟩ ∈ Subtype.val ⁻¹' Ioo a b
⊢ (s ∩ Ioo a b).Nonempty
Module: Mathlib.Topology.Order.AtTopBotIxx

Goal state before:
pp: X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a b : X
α : Type u_2
l : Filter α
f : α → ↑(Ioo a b)
ha : IsPredPrelimit a
⊢ Tendsto f l atBot ↔ Tendsto (fun x ↦ ↑(f x)) l (𝓝[>] a)

Tactic:
← comap_coe_Ioo_nhdsGT a b ha,

Goal state after:
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a b : X
α : Type u_2
l : Filter α
f : α → ↑(Ioo a b)
ha : IsPredPrelimit a
⊢ Tendsto f l (comap Subtype.val (𝓝[>] a)) ↔ Tendsto (fun x ↦ ↑(f x)) l (𝓝[>] a)
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: case h
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : s ⊆ t
u : Set α
hu : MeasurableSet u
⊢ u ∩ s ⊆ t

Tactic:
exact inter_subset_right.trans h

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
h : IsCompact s
hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝 x)
⊢ ∃ U ⊇ ∅, IsOpen[inst✝¹] U ∧ μ U < ∞

Tactic:
use ∅

Goal state after:
case h
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
h : IsCompact s
hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝 x)
⊢ ∅ ⊇ ∅ ∧ IsOpen[inst✝¹] ∅ ∧ μ ∅ < ∞
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
inst✝ : Countable α
μ ν : Measure α
h : ∀ (x : α), μ (measurableAtom x) = ν (measurableAtom x)
s : Set α
hs : MeasurableSet s
h1 : s = ⋃₀ (measurableAtom '' s)
h_count : (measurableAtom '' s).Countable
t t' : Set α
ht' : t' ∈ measurableAtom '' s
h_eq : t ≠ t'
y : α
hys : y ∈ s
hy : measurableAtom y = t
⊢ Disjoint t t'

Tactic:
obtain ⟨y', hy's, hy'⟩ := ht'

Goal state after:
α : Type u_1
m : MeasurableSpace α
inst✝ : Countable α
μ ν : Measure α
h : ∀ (x : α), μ (measurableAtom x) = ν (measurableAtom x)
s : Set α
hs : MeasurableSet s
h1 : s = ⋃₀ (measurableAtom '' s)
h_count : (measurableAtom '' s).Countable
t t' : Set α
h_eq : t ≠ t'
y : α
hys : y ∈ s
hy : measurableAtom y = t
y' : α
hy's : y' ∈ s
hy' : measurableAtom y' = t'
⊢ Disjoint t t'
Module: Mathlib.MeasureTheory.Measure.Trim

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
h : (μ.trim hm) s = 0
⊢ μ s = 0

Tactic:
grw [← nonpos_iff_eq_zero, ← h, le_trim hm]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
⊢ IsFiniteMeasure (μ.trim ⋯) ↔ IsFiniteMeasure μ

Tactic:
refine ⟨fun h => ⟨?_⟩, fun h => ⟨?_⟩⟩

Goal state after:
case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
h : IsFiniteMeasure (μ.trim ⋯)
⊢ μ Set.univ < ∞

case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
h : IsFiniteMeasure μ
⊢ (μ.trim ⋯) Set.univ < ∞
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: case refine_2
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
C : Set (Set α)
B : ℕ → Set α
hA : m0 = generateFrom C
hC : IsPiSystem C
h1B : ⋃ i, B i = univ
h2B : ∀ (i : ℕ), B i ∈ C
hμB : ∀ (i : ℕ), μ (B i) ≠ ∞
h_eq : ∀ s ∈ C, μ s = ν s
⊢ ∀ s ∈ range B, μ s ≠ ∞

Tactic:
rintro _ ⟨i, rfl⟩
    apply hμB

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : ⋃ i, s i = univ
hs_meas : ∀ (i : ℕ), MeasurableSet (s i)
⊢ μ univ < ∞

Tactic:
simp_rw [MeasurableSpace.measurableSet_bot_iff] at hs_meas

Goal state after:
α : Type u_1
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : ⋃ i, s i = univ
hs_meas : ∀ (i : ℕ), s i = ∅ ∨ s i = univ
⊢ μ univ < ∞
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: case intro
α : Type u_1
β : Type u_2
ι✝ : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
μ✝ ν : Measure α
s t : Set α
a : α
ι : Type u_4
inst✝¹ : Finite ι
μ : ι → Measure α
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
val✝ : Fintype ι
this : ∀ (n : ℕ), MeasurableSet (⋂ i, spanningSets (μ i) n)
⊢ SigmaFinite (sum μ)

Tactic:
refine ⟨⟨⟨fun n => ⋂ i, spanningSets (μ i) n, fun _ => trivial, fun n => ?_, ?_⟩⟩⟩

Goal state after:
case intro.refine_1
α : Type u_1
β : Type u_2
ι✝ : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
μ✝ ν : Measure α
s t : Set α
a : α
ι : Type u_4
inst✝¹ : Finite ι
μ : ι → Measure α
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
val✝ : Fintype ι
this : ∀ (n : ℕ), MeasurableSet (⋂ i, spanningSets (μ i) n)
n : ℕ
⊢ (sum μ) (⋂ i, spanningSets (μ i) n) < ∞

case intro.refine_2
α : Type u_1
β : Type u_2
ι✝ : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
μ✝ ν : Measure α
s t : Set α
a : α
ι : Type u_4
inst✝¹ : Finite ι
μ : ι → Measure α
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
val✝ : Fintype ι
this : ∀ (n : ℕ), MeasurableSet (⋂ i, spanningSets (μ i) n)
⊢ ⋃ i, ⋂ i_1, spanningSets (μ i_1) i = univ
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace β
inst✝¹ : Nonempty β
inst✝ : SeparatesPoints β
f : α → β
hf : Measurable f
a₁ a₂ : α
h : f a₁ ≠ f a₂
s : Set β
hs : MeasurableSet s
hx : f a₁ ∈ s
hy : f a₂ ∉ s
h' : f ⁻¹' s = univ
⊢ False

Tactic:
absurd hy
      simp [← mem_preimage, h']

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : CountablyGenerated α
⊢ Measurable (mapNatBool α)

Tactic:
by
  rw [measurable_pi_iff]
  refine fun n ↦ measurable_to_bool ?_
  simp only [preimage, mem_singleton_iff, mapNatBool,
    Bool.decide_iff, ofPred_mem_eq]
  apply measurableSet_natGeneratingSequence

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

Goal state before:
pp: case measurable_invFun
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : CountablyGenerated α
inst✝ : SeparatesPoints α
⊢ autoParam (Measurable ⇑(Equiv.ofInjective (mapNatBool α) ⋯).symm) MeasurableEquiv.measurable_invFun._autoParam

Tactic:
simp_rw +instances [← generateFrom_natGeneratingSequence α]

Goal state after:
case measurable_invFun
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : CountablyGenerated α
inst✝ : SeparatesPoints α
⊢ autoParam (Measurable ⇑(Equiv.ofInjective (mapNatBool α) ⋯).symm) MeasurableEquiv.measurable_invFun._autoParam
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case measurable_invFun
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : CountablyGenerated α
inst✝ : SeparatesPoints α
n : ℕ
⊢ MeasurableSet (⇑(Equiv.ofInjective (mapNatBool α) ⋯).symm ⁻¹' natGeneratingSequence α n)

Tactic:
← Equiv.image_eq_preimage_symm _ _

Goal state after:
case measurable_invFun
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : CountablyGenerated α
inst✝ : SeparatesPoints α
n : ℕ
⊢ MeasurableSet (⇑(Equiv.ofInjective (mapNatBool α) ⋯) '' natGeneratingSequence α n)
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case refine_1
α : Type u_1
t : ℕ → Set α
u : Set α
n : ℕ
hun : u ∈ memPartition t n
⊢ MeasurableSet u

Tactic:
induction n generalizing u with

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
⊢ sᶜ ∈ μ.cofinite ↔ μ s < ∞

Tactic:
mem_cofinite,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
⊢ μ sᶜᶜ < ∞ ↔ μ s < ∞
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
mα : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
mδ : MeasurableSpace δ
inst✝¹ : Preorder α
a b x : α
μ : Measure α
inst✝ : R1Space α
⊢ ∀ ⦃s : Set α⦄, s ∈ cocompact α → ∃ t ∈ cocompact α, MeasurableSet t ∧ t ⊆ s

Tactic:
by
    intro _ hs
    obtain ⟨t, ht, hts⟩ := mem_cocompact.mp hs
    exact ⟨(closure t)ᶜ, ht.closure.compl_mem_cocompact, isClosed_closure.measurableSet.compl,
      (compl_subset_compl.2 subset_closure).trans hts⟩

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:
apply sup_comm

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

Goal state before:
pp: α : Type u_1
γ : Type u_3
inst✝⁶ : TopologicalSpace α
inst✝⁵ : MeasurableSpace α
inst✝⁴ : OpensMeasurableSpace α
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
f g : α → γ
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
hf : ContinuousOn f s
hg : ContinuousOn g sᶜ
hs : MeasurableSet s
⊢ Measurable (s.piecewise f g)

Tactic:
by
  refine measurable_of_isOpen fun t ht => ?_
  rw [piecewise_preimage, Set.ite]
  apply MeasurableSet.union
  · rcases _root_.continuousOn_iff'.1 hf t ht with ⟨u, u_open, hu⟩
    rw [hu]
    exact u_open.measurableSet.inter hs
  · rcases _root_.continuousOn_iff'.1 hg t ht with ⟨u, u_open, hu⟩
    rw [sdiff_eq_compl_inter, inter_comm, hu]
    exact u_open.measurableSet.inter hs.compl

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
s₁ t₁ : Set α
s₂ t₂ : Set β
⊢ hausdorffEDist (s₁ ×ˢ s₂) (t₁ ×ˢ t₂) ≤ max (hausdorffEDist s₁ t₁) (hausdorffEDist s₂ t₂)

Tactic:
refine le_of_forall_ge fun _ _ => ?_

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
s₁ t₁ : Set α
s₂ t₂ : Set β
x✝¹ : ℝ≥0∞
x✝ : max (hausdorffEDist s₁ t₁) (hausdorffEDist s₂ t₂) ≤ x✝¹
⊢ hausdorffEDist (s₁ ×ˢ s₂) (t₁ ×ˢ t₂) ≤ x✝¹
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, infDist x t ≤ r
H2 : ∀ x ∈ t, infDist x s ≤ r
hs : s.Nonempty
ht : t.Nonempty
⊢ ∀ x ∈ t, infEDist x s ≤ ENNReal.ofReal r

Tactic:
simpa only [infDist, ← ENNReal.le_ofReal_iff_toReal_le (infEDist_ne_top hs) hr] using H2

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Zero β
r : β
s : Set α
f : α →ₛ β
hr : r ∈ SimpleFunc.range 0
h0 : r ≠ 0
hs : ¬MeasurableSet s
⊢ r ∈ ⇑f '' s

Tactic:
exact (h0 <| eq_zero_of_mem_range_zero hr).elim

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

Goal state before:
pp: f : ℕ → ℝ
k : ℕ
x : ℝ
h_tto : Tendsto f atTop (𝓝 x)
h_mon : MonotoneOn f (Ici k)
h_bdd : BddAbove (f '' Ici k)
⊢ IsLUB (f '' Ici k) x

Tactic:
tendsto_nhds_unique h_tto
    (Real.tendsto_atTop_csSup_of_monotoneOn_bddAbove_nat_Ici h_mon h_bdd)

Goal state after:
f : ℕ → ℝ
k : ℕ
x : ℝ
h_tto : Tendsto f atTop (𝓝 x)
h_mon : MonotoneOn f (Ici k)
h_bdd : BddAbove (f '' Ici k)
⊢ IsLUB (f '' Ici k) (sSup (f '' Ici k))
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
⊢ Tendsto (fun i ↦ (As i).indicator fun x ↦ b) L (𝓝 (A.indicator fun x ↦ b)) ↔
    ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A

Tactic:
simp_rw [tendsto_pi_nhds]

Goal state after:
α : 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
⊢ (∀ (x : α), Tendsto (fun i ↦ (As i).indicator (fun x ↦ b) x) L (𝓝 (A.indicator (fun x ↦ b) x))) ↔
    ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
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
eq : ∀ (p : ℝ≥0∞), ⇑(SimpleFunc.map c rs) ⁻¹' {p} = ⋃ n, ⇑(SimpleFunc.map c rs) ⁻¹' {p} ∩ {a | p ≤ f n a}
r : ℝ≥0∞
i j : ℕ
h : i ≤ j
⊢ (fun n ↦ ⇑(SimpleFunc.map c rs) ⁻¹' {r} ∩ {a | r ≤ f n a}) i ⊆
    (fun n ↦ ⇑(SimpleFunc.map c rs) ⁻¹' {r} ∩ {a | r ≤ f n a}) j

Tactic:
refine inter_subset_inter_right _ ?_

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
eq : ∀ (p : ℝ≥0∞), ⇑(SimpleFunc.map c rs) ⁻¹' {p} = ⋃ n, ⇑(SimpleFunc.map c rs) ⁻¹' {p} ∩ {a | p ≤ f n a}
r : ℝ≥0∞
i j : ℕ
h : i ≤ j
⊢ {a | r ≤ f i a} ⊆ {a | r ≤ f j a}
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
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, ∫⁻ (a : α), ((SimpleFunc.map c rs).restrict {a | (SimpleFunc.map c rs) a ≤ f n a}) a ∂μ ≤
    ⨆ n, ∫⁻ (a : α), f n a ∂μ

Tactic:
gcongr with n a

Goal state after:
case hfg
α : 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 : ℕ
a : α
⊢ ((SimpleFunc.map c rs).restrict {a | (SimpleFunc.map c rs) a ≤ f n a}) a ≤ f n a
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
G₀ : Type u_7
inst✝⁵ : GroupWithZero G₀
inst✝⁴ : MulAction G₀ β
inst✝³ : TopologicalSpace G₀
inst✝² : ContinuousInv₀ G₀
inst✝¹ : MetrizableSpace G₀
inst✝ : ContinuousSMul G₀ β
c : α → G₀
hc : AEStronglyMeasurable c μ
hc0 : ∀ᵐ (x : α) ∂μ, c x ≠ 0
h : AEStronglyMeasurable (fun x ↦ c x • f x) μ
⊢ (fun i ↦ (c i)⁻¹ • c i • f i) =ᵐ[μ] f

Tactic:
filter_upwards [hc0] with x hx

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁶ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
G₀ : Type u_7
inst✝⁵ : GroupWithZero G₀
inst✝⁴ : MulAction G₀ β
inst✝³ : TopologicalSpace G₀
inst✝² : ContinuousInv₀ G₀
inst✝¹ : MetrizableSpace G₀
inst✝ : ContinuousSMul G₀ β
c : α → G₀
hc : AEStronglyMeasurable c μ
hc0 : ∀ᵐ (x : α) ∂μ, c x ≠ 0
h : AEStronglyMeasurable (fun x ↦ c x • f x) μ
x : α
hx : c x ≠ 0
⊢ (c x)⁻¹ • c x • f x = f x
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hg : AEMeasurable g μ
hg_fin : ∫⁻ (a : α), g a ∂μ ≠ ∞
h_le : g ≤ᵐ[μ] f
⊢ ∫⁻ (a : α), f a - g a ∂μ = ∫⁻ (a : α), f a ∂μ - ∫⁻ (a : α), g a ∂μ

Tactic:
refine ENNReal.eq_sub_of_add_eq hg_fin ?_

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hg : AEMeasurable g μ
hg_fin : ∫⁻ (a : α), g a ∂μ ≠ ∞
h_le : g ≤ᵐ[μ] f
⊢ ∫⁻ (a : α), f a - g a ∂μ + ∫⁻ (a : α), g a ∂μ = ∫⁻ (a : α), f a ∂μ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub

Goal state before:
pp: α : 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
⊢ ∫⁻ (a : α), ⨅ b, f b a ∂μ = ⨅ b, ∫⁻ (a : α), f b a ∂μ

Tactic:
by
  cases nonempty_encodable β
  cases isEmpty_or_nonempty β
  · simp only [iInf_of_empty, lintegral_const,
      ENNReal.top_mul (Measure.measure_univ_ne_zero.mpr hμ)]
  inhabit β
  have : ∀ a, ⨅ b, f b a = ⨅ n, f (h_directed.sequence f n) a := by
    refine fun a =>
      le_antisymm (le_iInf fun n => iInf_le _ _)
        (le_iInf fun b => iInf_le_of_le (Encodable.encode b + 1) ?_)
    exact h_directed.sequence_le b a
  calc
    ∫⁻ a, ⨅ b, f b a ∂μ
    _ = ∫⁻ a, ⨅ n, (f ∘ h_directed.sequence f) n a ∂μ := by simp only [this, Function.comp_apply]
    _ = ⨅ n, ∫⁻ a, (f ∘ h_directed.sequence f) n a ∂μ := by
      rw [lintegral_iInf ?_ h_directed.sequence_anti]
      · exact hf_int _
      · exact fun n => hf _
    _ = ⨅ b, ∫⁻ a, f b a ∂μ := by
      refine le_antisymm (le_iInf fun b => ?_) (le_iInf fun n => ?_)
      · exact iInf_le_of_le (Encodable.encode b + 1) (lintegral_mono <| h_directed.sequence_le b)
      · exact iInf_le (fun b => ∫⁻ a, f b a ∂μ) _

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

Goal state before:
pp: α : Type u_5
E : Type u_6
x✝ : MeasurableSpace α
inst✝⁶ : AddGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : ContinuousAdd E
inst✝¹ : ContinuousNeg E
inst✝ : PseudoMetrizableSpace E
g f : α → E
hg : Measurable g
hf : StronglyMeasurable f
⊢ Measurable (g - f)

Tactic:
rw [sub_eq_add_neg]
  exact hg.add_stronglyMeasurable hf.neg

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : (x : α) → Decidable (x ∈ s)
f : ↑s → β
hf : StronglyMeasurable f
g : ↑sᶜ → β
hg : StronglyMeasurable g
hs : MeasurableSet s
x : α
hx : x ∈ s
⊢ Tendsto (fun n ↦ ((fun n ↦ SimpleFunc.dite s hs (hf.approx n) (hg.approx n)) n) x) atTop
    (𝓝 ((fun x ↦ if hx : x ∈ s then f ⟨x, hx⟩ else g ⟨x, hx⟩) x))

pp: case neg
α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : (x : α) → Decidable (x ∈ s)
f : ↑s → β
hf : StronglyMeasurable f
g : ↑sᶜ → β
hg : StronglyMeasurable g
hs : MeasurableSet s
x : α
hx : x ∉ s
⊢ Tendsto (fun n ↦ ((fun n ↦ SimpleFunc.dite s hs (hf.approx n) (hg.approx n)) n) x) atTop
    (𝓝 ((fun x ↦ if hx : x ∈ s then f ⟨x, hx⟩ else g ⟨x, hx⟩) x))

Tactic:
· simpa [hx] using hf.tendsto_approx ⟨x, hx⟩

Goal state after:
case neg
α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : (x : α) → Decidable (x ∈ s)
f : ↑s → β
hf : StronglyMeasurable f
g : ↑sᶜ → β
hg : StronglyMeasurable g
hs : MeasurableSet s
x : α
hx : x ∉ s
⊢ Tendsto (fun n ↦ ((fun n ↦ SimpleFunc.dite s hs (hf.approx n) (hg.approx n)) n) x) atTop
    (𝓝 ((fun x ↦ if hx : x ∈ s then f ⟨x, hx⟩ else g ⟨x, hx⟩) x))
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSingletonClass α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
h : SecondCountableTopologyEither α β
f : α → β
s : Set α
hf : ContinuousOn f s
hs : sᶜ.Countable
h's : MeasurableSet s
this : f = fun x ↦ if hx : x ∈ s then f ↑⟨x, hx⟩ else f ↑⟨x, hx⟩
⊢ StronglyMeasurable fun x ↦ f ↑x

Tactic:
have : SecondCountableTopologyEither s β := by cases h.out <;> infer_instance
    exact (continuousOn_iff_continuous_domRestrict.1 hf).stronglyMeasurable

Goal state after:
Module: Mathlib.Topology.Perfect

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T1Space α
h : Perfect (closure[inst✝¹] C)
x : α
xC : x ∈ C
⊢ AccPt x (𝓟 C)

Tactic:
have H : AccPt x (𝓟 (closure C)) := h.acc _ (subset_closure xC)

Goal state after:
case mpr
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T1Space α
h : Perfect (closure[inst✝¹] C)
x : α
xC : x ∈ C
H : AccPt x (𝓟 (closure[inst✝¹] C))
⊢ AccPt x (𝓟 C)
Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
h : μ μ.sigmaFiniteSetᶜ = 0
⊢ SigmaFinite (μ.restrict μ.sigmaFiniteSet + μ.restrict μ.sigmaFiniteSetᶜ)

Tactic:
Measure.restrict_eq_zero.mpr h,

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
h : μ μ.sigmaFiniteSetᶜ = 0
⊢ SigmaFinite (μ.restrict μ.sigmaFiniteSet + 0)
Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
h : μ μ.sigmaFiniteSetᶜ = 0
⊢ SigmaFinite μ

Tactic:
by
  rw [← Measure.restrict_add_restrict_compl (μ := μ) (measurableSet_sigmaFiniteSet (μ := μ)),
    Measure.restrict_eq_zero.mpr h, add_zero]
  infer_instance

Goal state after:
Module: Mathlib.Topology.Perfect

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen[inst✝¹] U
V : Set α
yV : y ∈ V
Vop : IsOpen[inst✝¹] V
hUV : Disjoint (closure[inst✝¹] U) (closure[inst✝¹] V)
⊢ ∃ C₀ C₁, (Perfect C₀ ∧ C₀.Nonempty ∧ C₀ ⊆ C) ∧ (Perfect C₁ ∧ C₁.Nonempty ∧ C₁ ⊆ C) ∧ Disjoint C₀ C₁

Tactic:
use closure (U ∩ C), closure (V ∩ C)

Goal state after:
case h
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen[inst✝¹] U
V : Set α
yV : y ∈ V
Vop : IsOpen[inst✝¹] V
hUV : Disjoint (closure[inst✝¹] U) (closure[inst✝¹] V)
⊢ (Perfect (closure[inst✝¹] (U ∩ C)) ∧ (closure[inst✝¹] (U ∩ C)).Nonempty ∧ closure[inst✝¹] (U ∩ C) ⊆ C) ∧
    (Perfect (closure[inst✝¹] (V ∩ C)) ∧ (closure[inst✝¹] (V ∩ C)).Nonempty ∧ closure[inst✝¹] (V ∩ C) ⊆ C) ∧
      Disjoint (closure[inst✝¹] (U ∩ C)) (closure[inst✝¹] (V ∩ C))
Module: Mathlib.Topology.Perfect

Goal state before:
pp: case specialize_3
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
U : Set α
hu : U.Nontrivial
h :
  ∀ (t t' : Set α),
    IsClosed[inst✝¹] t →
      IsClosed[inst✝¹] t' → U ⊆ t ∪ t' → (U ∩ t).Nonempty → (U ∩ t').Nonempty → (U ∩ (t ∩ t')).Nonempty
x : α
hx : x ∈ U
⊢ (U ∩ closure[inst✝¹] (U \ {x})).Nonempty

pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
U : Set α
hu : U.Nontrivial
x : α
h : (U ∩ ({x} ∩ closure[inst✝¹] (U \ {x}))).Nonempty
hx : x ∈ U
⊢ AccPt x (𝓟 U)

Tactic:
· obtain ⟨y, hy⟩ := Set.Nontrivial.exists_ne hu x
    use y
    simp only [Set.mem_inter_iff, hy, true_and]
    apply subset_closure
    simp [hy]

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
U : Set α
hu : U.Nontrivial
x : α
h : (U ∩ ({x} ∩ closure[inst✝¹] (U \ {x}))).Nonempty
hx : x ∈ U
⊢ AccPt x (𝓟 U)