mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
ι : Sort u_2
inst✝ : Nonempty ι
m : ι → OuterMeasure α
s : Set α
⊢ (⨅ i, m i) s = ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ i, (m i) (t n)

Tactic:
rw [iInf, sInf_apply (range_nonempty m)]

Goal state after:
α : Type u_1
ι : Sort u_2
inst✝ : Nonempty ι
m : ι → OuterMeasure α
s : Set α
⊢ ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ μ ∈ range m, μ (t n) =
    ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ i, (m i) (t n)
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: k : ℕ
hn : 0 < k.succ
⊢ ↑(∏ i ∈ Finset.range k.succ, (i + 1)) / ↑k.succ ^ k.succ ≤ 1 / ↑k.succ

Tactic:
pow_eq_prod_const,

Goal state after:
k : ℕ
hn : 0 < k.succ
⊢ ↑(∏ i ∈ Finset.range k.succ, (i + 1)) / ∏ _k ∈ Finset.range k.succ, ↑k.succ ≤ 1 / ↑k.succ
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case hfh
R : Type u_4
inst✝⁵ : TopologicalSpace R
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x ↦ a + x⁻¹) atTop (𝓝 a)
⊢ ∀ᶠ (b : R) in atTop, ↑⌈a * b⌉₊ / b ≤ a + b⁻¹

Tactic:
refine eventually_atTop.2 ⟨1, fun x hx ↦ ?_⟩
    simp [div_le_iff₀ (zero_lt_one.trans_le hx), inv_mul_cancel₀ (zero_lt_one.trans_le hx).ne',
      (Nat.ceil_lt_add_one (mul_nonneg ha (zero_le_one.trans hx))).le, add_mul]

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

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hsm : Antitone s
hs : ∃ᶠ (i : ι) in atTop, MeasurableSet (s i)
⊢ MeasurableSet (⋂ i, s i)

Tactic:
rw [← compl_iff, compl_iInter]
  exact .iUnion_of_monotone_of_frequently (compl_anti.comp hsm) <| hs.mono fun _ ↦ .compl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
hf : MeasurableEmbedding f
g : α → γ
g' : β → γ
hg : Measurable g
hg' : Measurable g'
⊢ Measurable (extend f g g')

Tactic:
refine measurable_of_restrict_of_restrict_compl hf.measurableSet_range ?_ ?_

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
hf : MeasurableEmbedding f
g : α → γ
g' : β → γ
hg : Measurable g
hg' : Measurable g'
⊢ Measurable ((range f).domRestrict (extend f g g'))

case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
hf : MeasurableEmbedding f
g : α → γ
g' : β → γ
hg : Measurable g
hg' : Measurable g'
⊢ Measurable ((range f)ᶜ.domRestrict (extend f g g'))
Module: Mathlib.MeasureTheory.Measure.NullMeasurable

Goal state before:

Tactic:
μ (s ∩ t) + μ (s \ t) ≤ μ (s' ∩ t) + μ (s' \ t) := by gcongr
    _ = μ (s' ∩ t ∪ s' \ t) :=
      (measure_union₀_aux (hs'm.inter ht) (hs'm.diff ht) <|
          (@disjoint_inf_sdiff _ s' t _).aedisjoint).symm
    _ = μ s' := congr_arg μ (inter_union_sdiff _ _)
    _ = μ s := hs'

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
s : Set β
hs : NullMeasurableSet s (map f μ)
⊢ (map f μ) s = μ (f ⁻¹' s)

Tactic:
rw [map, dif_pos hf, mapₗ, dif_pos hf.measurable_mk] at hs ⊢

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
s : Set β
hs : NullMeasurableSet s ((liftLinear (OuterMeasure.map (AEMeasurable.mk f hf)) ⋯) μ)
⊢ ((liftLinear (OuterMeasure.map (AEMeasurable.mk f hf)) ⋯) μ) s = μ (f ⁻¹' s)
Module: Mathlib.MeasureTheory.Measure.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
s : Set β
⊢ μ (f ⁻¹' s) ≤ μ (f ⁻¹' toMeasurable (map f μ) s)

Tactic:
gcongr; apply subset_toMeasurable

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

Goal state before:
pp: case refine_2
α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν : Measure α
h : μ₁ ≪ ν ∧ μ₂ ≪ ν
⊢ ν + ν ≪ ν

Tactic:
← two_smul ℝ≥0

Goal state after:
case refine_2
α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν : Measure α
h : μ₁ ≪ ν ∧ μ₂ ≪ ν
⊢ 2 • ν ≪ ν
Module: Mathlib.MeasureTheory.Measure.Comap

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s : Set α
hs : (comap f μ) s = 0
⊢ μ (f '' s) = 0

Tactic:
← nonpos_iff_eq_zero

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s : Set α
hs : (comap f μ) s = 0
⊢ μ (f '' s) ≤ 0
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
ht : μ tᶜ = 0
⊢ μ (s ∩ t) = μ s

Tactic:
by
  rw [← sdiff_compl, measure_sdiff_null ht]

Goal state after:
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 : X → α
h : a < b
ha : IsPredPrelimit a
⊢ Tendsto (fun x ↦ f ↑x) atBot l ↔ Tendsto f (𝓝[>] a) l

Tactic:
← map_coe_Ioo_atBot h 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 : X → α
h : a < b
ha : IsPredPrelimit a
⊢ Tendsto (fun x ↦ f ↑x) atBot l ↔ Tendsto f (map Subtype.val atBot) l
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t s : Set α
ht : NullMeasurableSet t μ
⊢ μ.restrict t + μ.restrict (s \ t) + μ.restrict (s ∩ t) = μ.restrict s + μ.restrict t

Tactic:
←
    restrict_inter_add_sdiff₀ s ht,

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t s : Set α
ht : NullMeasurableSet t μ
⊢ μ.restrict t + μ.restrict (s \ t) + μ.restrict (s ∩ t) = μ.restrict (s ∩ t) + μ.restrict (s \ t) + μ.restrict t
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
R : Type u_8
inst✝⁴ : Semiring R
inst✝³ : IsDomain R
inst✝² : Module R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : Module.IsTorsionFree R ℝ≥0∞
c : R
hc : c ≠ 0
μ : Measure α
s✝ : Set α
⊢ s✝ ∈ ae (c • μ) ↔ s✝ ∈ ae μ

Tactic:
exact ae_smul_measure_iff hc

Goal state after:
Module: Mathlib.Data.Set.MemPartition

Goal state before:
pp: case succ
α : Type u_1
f : ℕ → Set α
a : α
n : ℕ
ih : a ∈ memPartitionSet f n a
⊢ a ∈ memPartitionSet f (n + 1) a

Tactic:
rw [memPartitionSet_succ]
    split_ifs with h <;> exact ⟨ih, h⟩

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
⊢ ⨆ i, (μ.restrict (spanningSets μ i)) s = ⨆ i, (μ.restrict (spanningSets μ i)) (toMeasurable μ s)

Tactic:
restrict_apply' (measurableSet_spanningSets μ _),

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
⊢ ⨆ i, μ (s ∩ spanningSets μ i) = ⨆ i, μ (toMeasurable μ s ∩ spanningSets μ i)
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
x : α
⊢ MeasurableSet (measurableAtom x)

Tactic:
rw [measurableAtom_eq_countablyGeneratedAtom_natGeneratingSequence]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
x : α
⊢ MeasurableSet (countablyGeneratedAtom α fun x_1 ↦ x ∈ natGeneratingSequence α x_1)
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace β
inst✝¹ : Nonempty β
inst✝ : SeparatesPoints β
f : α → β
hf : Measurable f
h : ∀ (a₁ a₂ : α), f a₁ = f a₂
h' : IsEmpty α
⊢ ∃ c, f = fun x ↦ c

Tactic:
use (Classical.ofNonempty : β), funext (by simp)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
x y : α
h : x ∈ {x} → y ∈ {x}
⊢ x = y

Tactic:
simp_rw [mem_singleton_iff, forall_true_left] at h

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
x y : α
h : y = x
⊢ x = y
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
f : ℕ → Set α
hs✝ : ∀ (n_1 : ℕ), MeasurableSet (f n_1)
S : ℕ → Finset (Set α)
hS_subset : ∀ (n_1 : ℕ), ↑(S n_1) ⊆ memPartition t n
hS_eq : ∀ (n : ℕ), f n = ⋃₀ ↑(S n)
⊢ ∀ (i : ℕ), ↑(S i) ⊆ memPartition t n

Tactic:
exact hS_subset

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

Goal state before:
pp: case refine_1.iUnion.refine_1
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
f : ℕ → Set α
hs✝ : ∀ (n_1 : ℕ), MeasurableSet (f n_1)
S : ℕ → Finset (Set α)
hS_subset : ∀ (n_1 : ℕ), ↑(S n_1) ⊆ memPartition t n
hS_eq : ∀ (n : ℕ), f n = ⋃₀ ↑(S n)
this : Fintype ↑(⋃ n, ↑(S n))
⊢ ∀ (i : ℕ), ↑(S i) ⊆ memPartition t n

Tactic:
exact hS_subset

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

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

Tactic:
by
  rcases h with (h | h)
  · refine ⟨Or.inl countable_prod_swap⟩
  · exact ⟨Or.inr h⟩

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

Goal state before:
pp: case negSucc
α✝ : Type u_1
M✝ : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
inst✝⁷ : MeasurableSpace X
inst✝⁶ : SMul M✝ X
m : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → M✝
g : α → X
inst✝⁵ : MeasurableSpace M✝
inst✝⁴ : MeasurableSMul M✝ X
M : Type u_6
inst✝³ : SubNegMonoid M
inst✝² : MeasurableSpace M
inst✝¹ : MeasurableAdd₂ M
inst✝ : MeasurableNeg M
n : ℕ
⊢ Measurable fun x ↦ -((n + 1) • x)

Tactic:
exact (measurable_const_smul _).neg

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

Goal state before:
pp: case refine_1
α : Type u
inst✝ : PseudoEMetricSpace α
U : Set α
hU : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n ↦ (fun x ↦ infEDist x Uᶜ) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
x : α
hx : x ∈ U
this✝ : ¬infEDist x Uᶜ = 0
B : 0 < infEDist x Uᶜ
this : Tendsto (fun n ↦ a ^ n) atTop (𝓝 0)
n : ℕ
hn : a ^ n < infEDist x Uᶜ
⊢ x ∈ ⋃ n, F n

Tactic:
simp only [mem_iUnion]

Goal state after:
case refine_1
α : Type u
inst✝ : PseudoEMetricSpace α
U : Set α
hU : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n ↦ (fun x ↦ infEDist x Uᶜ) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
x : α
hx : x ∈ U
this✝ : ¬infEDist x Uᶜ = 0
B : 0 < infEDist x Uᶜ
this : Tendsto (fun n ↦ a ^ n) atTop (𝓝 0)
n : ℕ
hn : a ^ n < infEDist x Uᶜ
⊢ ∃ i, x ∈ F i
Module: Mathlib.MeasureTheory.MeasurableSpace.Prod

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_3
γ : Type u_4
inst✝ : MeasurableSingletonClass α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
x✝ : α
f : γ → β
hf : MeasurableEmbedding f
s : Set γ
hs : MeasurableSet s
x : α × β
⊢ x ∈ (fun y ↦ (x✝, f y)) '' s ↔ x ∈ {x✝} ×ˢ (f '' s)

Tactic:
simp [Prod.ext_iff, eq_comm, ← exists_and_left, and_left_comm]

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

Goal state before:
pp: a : ℝ
x✝ : Set ℝ
hav : a ∈ x✝
hv : IsOpen x✝
w✝¹ w✝ : ℝ
hl : w✝¹ < a
hu : a < w✝
h : Ioo w✝¹ w✝ ⊆ x✝
q : ℚ
hlq : w✝¹ < ↑q
hqa : ↑q < a
p : ℚ
hap : a < ↑p
hpu : ↑p < w✝
⊢ Ioo ↑q ↑p ∈ ⋃ a, ⋃ b, ⋃ (_ : a < b), {Ioo ↑a ↑b}

Tactic:
simp only [mem_iUnion]

Goal state after:
a : ℝ
x✝ : Set ℝ
hav : a ∈ x✝
hv : IsOpen x✝
w✝¹ w✝ : ℝ
hl : w✝¹ < a
hu : a < w✝
h : Ioo w✝¹ w✝ ⊆ x✝
q : ℚ
hlq : w✝¹ < ↑q
hqa : ↑q < a
p : ℚ
hap : a < ↑p
hpu : ↑p < w✝
⊢ ∃ i i_1, ∃ (_ : i < i_1), Ioo ↑q ↑p ∈ {Ioo ↑i ↑i_1}
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : Zero β
μ : Measure α
f : α →ₛ β
hf : ∀ (y : β), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ∞
⊢ μ (support ⇑f) < ∞

Tactic:
rw [support_eq]
  refine (measure_biUnion_finset_le _ _).trans_lt (ENNReal.sum_lt_top.mpr fun y hy => ?_)
  rw [Finset.mem_filter] at hy
  exact hf y hy.2

Goal state after:
Module: Mathlib.Topology.IndicatorConstPointwise

Goal state before:
pp: case nhds_b
α : Type u_1
A : Set α
β : Type u_2
inst✝³ : Zero β
inst✝² : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
inst✝¹ : T1Space β
b : β
inst✝ : NeZero b
x : α
⊢ {0}ᶜ ∈ 𝓝 b

pp: case nhds_o
α : Type u_1
A : Set α
β : Type u_2
inst✝³ : Zero β
inst✝² : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
inst✝¹ : T1Space β
b : β
inst✝ : NeZero b
x : α
⊢ {b}ᶜ ∈ 𝓝 0

Tactic:
· simp only [compl_singleton_mem_nhds_iff, ne_eq, NeZero.ne, not_false_eq_true]

Goal state after:
case nhds_o
α : Type u_1
A : Set α
β : Type u_2
inst✝³ : Zero β
inst✝² : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
inst✝¹ : T1Space β
b : β
inst✝ : NeZero b
x : α
⊢ {b}ᶜ ∈ 𝓝 0
Module: Mathlib.Topology.IndicatorConstPointwise

Goal state before:
pp: case nhds_b
α : Type u_1
A : Set α
β : Type u_2
inst✝³ : Zero β
inst✝² : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
inst✝¹ : T1Space β
b : β
inst✝ : NeZero b
⊢ {0}ᶜ ∈ 𝓝 b

pp: case nhds_o
α : Type u_1
A : Set α
β : Type u_2
inst✝³ : Zero β
inst✝² : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
inst✝¹ : T1Space β
b : β
inst✝ : NeZero b
⊢ {b}ᶜ ∈ 𝓝 0

Tactic:
· simp only [compl_singleton_mem_nhds_iff, ne_eq, NeZero.ne, not_false_eq_true]

Goal state after:
case nhds_o
α : Type u_1
A : Set α
β : Type u_2
inst✝³ : Zero β
inst✝² : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
inst✝¹ : T1Space β
b : β
inst✝ : NeZero b
⊢ {b}ᶜ ∈ 𝓝 0
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: case refine_2
β : Type u_6
mβ : MeasurableSpace β
f : EReal × EReal → β
h_real : Measurable fun p ↦ f (↑p.1, ↑p.2)
h_bot_left : Measurable fun r ↦ f (⊥, ↑r)
h_top_left : Measurable fun r ↦ f (⊤, ↑r)
h_bot_right : Measurable fun r ↦ f (↑r, ⊥)
h_top_right : Measurable fun r ↦ f (↑r, ⊤)
⊢ Measurable fun x ↦ f (⊥, x)

Tactic:
exact measurable_of_measurable_real h_bot_left

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 ((approxOn f hf s y₀ h₀ n) x) (f x) ≤ edist ((approxOn f hf s y₀ h₀ m) x) (f x)

Tactic:
dsimp only [approxOn, coe_comp, Function.comp_def]
  exact edist_nearestPt_le _ _ ((nearestPtInd_le _ _ _).trans h)

Goal state after:
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✝ : PseudoMetricSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
ε : ℝ
hε : 0 < ε
⊢ ∃ g, ∀ (x : X × Y), dist (f x) (g x) < ε

Tactic:
by
  have M : ∀ (K : Set (X × Y)), IsCompact K →
      ∃ (g : SimpleFunc (X × Y) α), ∃ (s : Set (X × Y)), MeasurableSet s ∧ K ⊆ s ∧
      ∀ x ∈ s, dist (f x) (g x) < ε := by
    intro K hK
    apply IsCompact.induction_on
      (p := fun t ↦ ∃ (g : SimpleFunc (X × Y) α), ∃ (s : Set (X × Y)), MeasurableSet s ∧ t ⊆ s ∧
        ∀ x ∈ s, dist (f x) (g x) < ε) hK
    · exact ⟨0, ∅, by simp⟩
    · intro t t' htt' ⟨g, s, s_meas, ts, hg⟩
      exact ⟨g, s, s_meas, htt'.trans ts, hg⟩
    · intro t t' ⟨g, s, s_meas, ts, hg⟩ ⟨g', s', s'_meas, t's', hg'⟩
      refine ⟨g.piecewise s s_meas g', s ∪ s', s_meas.union s'_meas,
        union_subset_union ts t's', fun p hp ↦ ?_⟩
      by_cases H : p ∈ s
      · simpa [H, SimpleFunc.piecewise_apply] using hg p H
      · simp only [SimpleFunc.piecewise_apply, H, ite_false]
        apply hg'
        simpa [H] using (mem_union _ _ _).1 hp
    · rintro ⟨x, y⟩ -
      obtain ⟨u, v, hu, xu, hv, yv, huv⟩ : ∃ u v, IsOpen u ∧ x ∈ u ∧ IsOpen v ∧ y ∈ v ∧
        u ×ˢ v ⊆ {z | dist (f z) (f (x, y)) < ε} :=
          mem_nhds_prod_iff'.1 <| Metric.continuousAt_iff'.1 hf.continuousAt ε hε
      refine ⟨u ×ˢ v, nhdsWithin_le_nhds <| (hu.prod hv).mem_nhds (mk_mem_prod xu yv), ?_⟩
      exact ⟨SimpleFunc.const _ (f (x, y)), u ×ˢ v, hu.measurableSet.prod hv.measurableSet,
        Subset.rfl, fun z hz ↦ huv hz⟩
  obtain ⟨g, s, s_meas, fs, hg⟩ : ∃ (g : SimpleFunc (X × Y) α) (s : Set (X × Y)),
    MeasurableSet s ∧ tsupport f ⊆ s ∧ ∀ (x : X × Y), x ∈ s → dist (f x) (g x) < ε := M _ h'f
  refine ⟨g.piecewise s s_meas 0, fun p ↦ ?_⟩
  by_cases H : p ∈ s
  · simpa [H, SimpleFunc.piecewise_apply] using hg p H
  · have : f p = 0 := by
      contrapose! H
      rw [← Function.mem_support] at H
      exact fs (subset_tsupport _ H)
    simp [SimpleFunc.piecewise_apply, H, this, hε]

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

Goal state before:
pp: case neg.inr
α : Type u_1
β : Type u_5
f : α → β
inst✝¹ : SeminormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
h0 : ¬‖(hf.approx n) x‖ = 0
h : c ≤ ‖(hf.approx n) x‖
⊢ ‖(hf.approx n) x‖ * (‖c‖ / ‖(hf.approx n) x‖) ≤ c

Tactic:
mul_div,

Goal state after:
case neg.inr
α : Type u_1
β : Type u_5
f : α → β
inst✝¹ : SeminormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
h0 : ¬‖(hf.approx n) x‖ = 0
h : c ≤ ‖(hf.approx n) x‖
⊢ ‖(hf.approx n) x‖ * ‖c‖ / ‖(hf.approx n) x‖ ≤ c
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : ℕ → Set α := spanningSets (μ.restrict t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := hf_meas.approx
fs : ℕ → α →ₛ β := fun n ↦ (f_approx n).restrict (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, (fs n) x = 0
n : ℕ
y : β
hy : y ∈ ↑({y ∈ (fs n).range | y ≠ 0})
⊢ y ≠ 0

pp: case refine_1
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : ℕ → Set α := spanningSets (μ.restrict t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := hf_meas.approx
fs : ℕ → α →ₛ β := fun n ↦ (f_approx n).restrict (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, (fs n) x = 0
n : ℕ
y : β
hy : y ∈ ↑({y ∈ (fs n).range | y ≠ 0})
⊢ μ (S n ∩ t ∩ ⇑(f_approx n) ⁻¹' {y}) < ∞

Tactic:
· let : (y : β) → Decidable (y = 0) := fun y => Classical.propDecidable _
      rw [Finset.mem_coe, Finset.mem_filter] at hy
      exact hy.2

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : ℕ → Set α := spanningSets (μ.restrict t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := hf_meas.approx
fs : ℕ → α →ₛ β := fun n ↦ (f_approx n).restrict (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, (fs n) x = 0
n : ℕ
y : β
hy : y ∈ ↑({y ∈ (fs n).range | y ≠ 0})
⊢ μ (S n ∩ t ∩ ⇑(f_approx n) ⁻¹' {y}) < ∞
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : ℕ → Set α := spanningSets (μ.restrict t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := hf_meas.approx
fs : ℕ → α →ₛ β := fun n ↦ (f_approx n).restrict (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, (fs n) x = 0
⊢ ∀ (n : ℕ), μ (support ⇑(fs n)) < ∞

Tactic:
simp_rw [SimpleFunc.support_eq, ← Finset.mem_coe]
    classical
    refine fun n => measure_biUnion_lt_top {y ∈ (fs n).range | y ≠ 0}.finite_toSet fun y hy => ?_
    rw [SimpleFunc.restrict_preimage_singleton _ ((hS_meas n).inter ht)]
    swap
    · let : (y : β) → Decidable (y = 0) := fun y => Classical.propDecidable _
      rw [Finset.mem_coe, Finset.mem_filter] at hy
      exact hy.2
    refine (measure_mono Set.inter_subset_left).trans_lt ?_
    have h_lt_top := measure_spanningSets_lt_top (μ.restrict t) n
    rwa [Measure.restrict_apply' ht] at h_lt_top

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
g : α →ₛ ℝ≥0∞
hg : ⇑g ≤ fun a ↦ s.indicator f a
this : ⇑g ≤ f
⊢ g.lintegral μ = g.lintegral (μ.restrict s)

Tactic:
lintegral_restrict,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
g : α →ₛ ℝ≥0∞
hg : ⇑g ≤ fun a ↦ s.indicator f a
this : ⇑g ≤ f
⊢ g.lintegral μ = ∑ y ∈ g.range, y * μ (⇑g ⁻¹' {y} ∩ s)
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: case e'_3
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun x1 x2 ↦ x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' ↦ Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i ↦ f i x
h_ae_seq_directed : Directed LE.le (aeSeq hf p)
⊢ (fun b ↦ ∫⁻ (a : α), f b a ∂μ) = fun b ↦ ∫⁻ (a : α), aeSeq hf p b a ∂μ

Tactic:
ext1 b

Goal state after:
case e'_3
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun x1 x2 ↦ x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' ↦ Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i ↦ f i x
h_ae_seq_directed : Directed LE.le (aeSeq hf p)
b : β
⊢ ∫⁻ (a : α), f b a ∂μ = ∫⁻ (a : α), aeSeq hf p b a ∂μ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (x : α) ∂μ, Antitone fun n ↦ f n x
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
this : Antitone fun n ↦ ∫⁻ (x : α), f n x ∂μ
key : ∫⁻ (x : α), F x ∂μ = ⨅ n, ∫⁻ (x : α), f n x ∂μ
⊢ Tendsto (fun n ↦ ∫⁻ (x : α), f n x ∂μ) atTop (𝓝 (∫⁻ (x : α), F x ∂μ))

Tactic:
rw [key]
    exact tendsto_atTop_iInf this

Goal state after: