mathlib-initiative/mathlib-tactics huggingface dataset:
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:
by
  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.MeasureTheory.MeasurableSpace.Prod

Goal state before:
pp: case a.refine_1
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
s : Set α
hs : s ∈ C
t : ℕ → Set β
h1t : ∀ (n : ℕ), t n ∈ D
h2t : ⋃ n, t n = univ
⊢ MeasurableSet (s ×ˢ ⋃ n, t n)

Tactic:
prod_iUnion

Goal state after:
case a.refine_1
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
s : Set α
hs : s ∈ C
t : ℕ → Set β
h1t : ∀ (n : ℕ), t n ∈ D
h2t : ⋃ n, t n = univ
⊢ MeasurableSet (⋃ i, s ×ˢ t i)
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: μ : Measure ℝ
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : NullSingletonClass μ
b r : ℝ
⊢ r ∈ Iio 0 → 0 = μ (Icc (b - r) (b + r))

Tactic:
(hr : r < 0)

Goal state after:
μ : Measure ℝ
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : NullSingletonClass μ
b r : ℝ
hr : r < 0
⊢ 0 = μ (Icc (b - r) (b + r))
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case hd
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
⊢ Disjoint (s ∩ f ⁻¹' {0}) (s ∩ f ⁻¹' Ioi 0)

pp: case h
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
⊢ MeasurableSet (s ∩ f ⁻¹' Ioi 0)

Tactic:
· exact disjoint_singleton_left.mpr self_notMem_Ioi
        |>.preimage f |>.inter_right' s |>.inter_left' s

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
⊢ MeasurableSet (s ∩ f ⁻¹' Ioi 0)
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 < ε
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 : f p ≠ 0
⊢ p ∈ s

Tactic:
← Function.mem_support

Goal state after:
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 ∈ support f
⊢ p ∈ s
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m : MeasurableSpace α
f : α → β
m' m₀ : MeasurableSpace α
μ : Measure α
inst✝ : Zero β
hm : m ≤ m₀
s : Set α
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : AEStronglyMeasurable f μ
hf_zero : f =ᵐ[μ.restrict sᶜ] 0
x : α
hx : f x = AEStronglyMeasurable.mk f hf x
hxs : x ∉ s
⊢ s.indicator (AEStronglyMeasurable.mk f hf) x = s.indicator f x

Tactic:
· simp [hxs]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
ι : Type u_5
inst✝² : PseudoMetrizableSpace β
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) u (𝓝 (g x))
⊢ AEStronglyMeasurable g μ

Tactic:
borelize β

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
ι : Type u_5
inst✝² : PseudoMetrizableSpace β
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) u (𝓝 (g x))
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ AEStronglyMeasurable g μ
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
inst✝ : PseudoMetrizableSpace β
f : ℕ → α → β
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n ↦ f n x) atTop (𝓝 l)
⊢ ∃ f_lim, StronglyMeasurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (f_lim x))

Tactic:
borelize β

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
inst✝ : PseudoMetrizableSpace β
f : ℕ → α → β
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n ↦ f n x) atTop (𝓝 l)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ ∃ f_lim, StronglyMeasurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (f_lim x))
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: α : Type u_5
β : Type u_6
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
mb : MeasurableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
μ : Measure α
f : α → β
s : Set β
hs : MeasurableSet s
h_nonempty : s.Nonempty
h_mem : ∀ᵐ (x : α) ∂μ, f x ∈ s
f' : α → β
hf' : StronglyMeasurable f'
hff' : f =ᵐ[μ] f'
⊢ ∃ g, StronglyMeasurable g ∧ (∀ (x : α), g x ∈ s) ∧ f =ᵐ[μ] g

Tactic:
classical
  refine ⟨(f' ⁻¹' s).piecewise f' (fun _ ↦ h_nonempty.some), ?meas, ?subset, ?ae_eq⟩
  case meas => exact hf'.piecewise (hf'.measurable hs) stronglyMeasurable_const
  case subset =>
    rw [← Set.range_subset_iff]
    simpa [Set.range_piecewise] using! fun _ _ ↦ h_nonempty.some_mem
  case ae_eq =>
    apply hff'.trans
    filter_upwards [h_mem, hff'] with x hx hx'
    exact Eq.symm <| (f' ⁻¹' s).piecewise_eq_of_mem f' _ (by simpa [hx'] using! hx)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝² : Countable ι
inst✝¹ : TopologicalSpace β
f : α → β
inst✝ : PseudoMetrizableSpace β
m : MeasurableSpace α
μ : ι → Measure α
h : ∀ (i : ι), AEStronglyMeasurable f (μ i)
⊢ AEStronglyMeasurable f (sum μ)

Tactic:
borelize β

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝² : Countable ι
inst✝¹ : TopologicalSpace β
f : α → β
inst✝ : PseudoMetrizableSpace β
m : MeasurableSpace α
μ : ι → Measure α
h : ∀ (i : ι), AEStronglyMeasurable f (μ i)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ AEStronglyMeasurable f (sum μ)
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

Tactic:
let : (y : β) → Decidable (y = 0) := fun y => Classical.propDecidable _

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})
this : (y : β) → Decidable (y = 0) := fun y ↦ Classical.propDecidable (y = 0)
⊢ y ≠ 0
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
m : MeasurableSpace α
inst✝² : One β
inst✝¹ : TopologicalSpace β
inst✝ : MetrizableSpace β
hf : StronglyMeasurable f
⊢ MeasurableSet (mulSupport f)

Tactic:
borelize β

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
m : MeasurableSpace α
inst✝² : One β
inst✝¹ : TopologicalSpace β
inst✝ : MetrizableSpace β
hf : StronglyMeasurable f
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ MeasurableSet (mulSupport f)
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
mα : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : GroupWithZero β
inst✝¹ : ContinuousInv₀ β
inst✝ : MetrizableSpace β
hf : StronglyMeasurable f
⊢ StronglyMeasurable f⁻¹

Tactic:
borelize β

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
mα : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : GroupWithZero β
inst✝¹ : ContinuousInv₀ β
inst✝ : MetrizableSpace β
hf : StronglyMeasurable f
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ StronglyMeasurable f⁻¹
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
f g : α → β
mα : MeasurableSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : GroupWithZero β
inst✝² : ContinuousMul β
inst✝¹ : ContinuousInv₀ β
inst✝ : MetrizableSpace β
hf : StronglyMeasurable f
hg : StronglyMeasurable g
⊢ StronglyMeasurable (f / g)

Tactic:
borelize β

Goal state after:
α : Type u_1
β : Type u_2
f g : α → β
mα : MeasurableSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : GroupWithZero β
inst✝² : ContinuousMul β
inst✝¹ : ContinuousInv₀ β
inst✝ : MetrizableSpace β
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ StronglyMeasurable (f / g)
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
n : ℕ
⊢ (eapprox f n).lintegral μ ≤ ∫⁻ (x : α), f x ∂μ

Tactic:
rw [lintegral_eq_iSup_eapprox_lintegral hf]
  exact le_iSup (fun n ↦ (eapprox f n).lintegral μ) n

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : TopologicalSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
h : SecondCountableTopologyEither α β
f : α → β
hf : Continuous[inst✝³, inst✝¹] f
⊢ StronglyMeasurable f

Tactic:
borelize β

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : TopologicalSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
h : SecondCountableTopologyEither α β
f : α → β
hf : Continuous[inst✝³, inst✝¹] f
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ StronglyMeasurable f
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : One β
f : α → β
hf : Continuous[inst✝⁴, inst✝²] f
k : Set α
hk : IsCompact k
h'f : mulSupport f ⊆ k
⊢ StronglyMeasurable f

Tactic:
borelize β

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : One β
f : α → β
hf : Continuous[inst✝⁴, inst✝²] f
k : Set α
hk : IsCompact k
h'f : mulSupport f ⊆ k
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ StronglyMeasurable f
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_5
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : Tendsto f u (𝓝 g)
⊢ StronglyMeasurable g

Tactic:
borelize β

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_5
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : Tendsto f u (𝓝 g)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ StronglyMeasurable g
Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

Goal state before:
pp: case refine_2
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
this : ∀ (n : ℕ), SigmaFinite (μ.restrict (μ.sigmaFiniteSetGE ν n))
f : ℕ × ℕ → Set α :=
  fun p ↦
    (μ.sigmaFiniteSetWRT' ν)ᶜ ∪ spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν p.1)) p.2 ∩ μ.sigmaFiniteSetGE ν p.1
e : ℕ ≃ ℕ × ℕ := Nat.pairEquiv.symm
⊢ ⋃ n,
      spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν (Nat.unpair n).1)) (Nat.unpair n).2 ∩
        μ.sigmaFiniteSetGE ν (Nat.unpair n).1 =
    μ.sigmaFiniteSetWRT' ν

Tactic:
calc ⋃ n, (spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν (Nat.unpair n).1)) n.unpair.2
        ∩ μ.sigmaFiniteSetGE ν n.unpair.1)
      = ⋃ n, ⋃ m, (spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν n)) m
            ∩ μ.sigmaFiniteSetGE ν n) :=
          Set.iUnion_unpair (fun n m ↦ spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν n)) m
            ∩ μ.sigmaFiniteSetGE ν n)
    _ = ⋃ n, μ.sigmaFiniteSetGE ν n := by
        refine Set.iUnion_congr (fun n ↦ ?_)
        rw [← Set.iUnion_inter, iUnion_spanningSets, Set.univ_inter]
    _ = μ.sigmaFiniteSetWRT' ν := rfl

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
⊢ SigmaFinite (μ.restrict (μ.sigmaFiniteSetWRT' ν))

Tactic:
by
  have := sigmaFinite_restrict_sigmaFiniteSetGE μ ν
  let f : ℕ × ℕ → Set α := fun p : ℕ × ℕ ↦ (μ.sigmaFiniteSetWRT' ν)ᶜ
    ∪ (spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν p.1)) p.2 ∩ (μ.sigmaFiniteSetGE ν p.1))
  suffices (μ.restrict (μ.sigmaFiniteSetWRT' ν)).FiniteSpanningSetsIn (Set.range f) from
    this.sigmaFinite
  let e : ℕ ≃ ℕ × ℕ := Nat.pairEquiv.symm
  refine ⟨fun n ↦ f (e n), fun _ ↦ by simp, fun n ↦ ?_, ?_⟩
  · simp only [Nat.pairEquiv_symm_apply, measure_union_lt_top_iff, f, e]
    rw [Measure.restrict_apply' measurableSet_sigmaFiniteSetWRT', Set.compl_inter_self,
      Measure.restrict_apply' measurableSet_sigmaFiniteSetWRT']
    simp only [measure_empty, ENNReal.zero_lt_top, true_and]
    refine (measure_mono Set.inter_subset_left).trans_lt ?_
    rw [← Measure.restrict_apply' (measurableSet_sigmaFiniteSetGE _)]
    exact measure_spanningSets_lt_top _ _
  · simp only [Nat.pairEquiv_symm_apply, f, e]
    rw [← Set.union_iUnion]
    suffices ⋃ n, (spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν (Nat.unpair n).1)) n.unpair.2
        ∩ μ.sigmaFiniteSetGE ν n.unpair.1) = μ.sigmaFiniteSetWRT' ν by
      rw [this, Set.compl_union_self]
    calc ⋃ n, (spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν (Nat.unpair n).1)) n.unpair.2
        ∩ μ.sigmaFiniteSetGE ν n.unpair.1)
      = ⋃ n, ⋃ m, (spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν n)) m
            ∩ μ.sigmaFiniteSetGE ν n) :=
          Set.iUnion_unpair (fun n m ↦ spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν n)) m
            ∩ μ.sigmaFiniteSetGE ν n)
    _ = ⋃ n, μ.sigmaFiniteSetGE ν n := by
        refine Set.iUnion_congr (fun n ↦ ?_)
        rw [← Set.iUnion_inter, iUnion_spanningSets, Set.univ_inter]
    _ = μ.sigmaFiniteSetWRT' ν := rfl

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

Goal state before:
pp: case refine_3
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∀ ⦃f : ℕ → α → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f n)) →
      Monotone f →
        (∀ (n : ℕ), ∫⁻ (a : α), f n a ∂μ.trim hm = ∫⁻ (a : α), f n a ∂μ) →
          ∫⁻ (a : α), (fun x ↦ ⨆ n, f n x) a ∂μ.trim hm = ∫⁻ (a : α), (fun x ↦ ⨆ n, f n x) a ∂μ

Tactic:
· intro f hf hf_mono hf_prop
    rw [lintegral_iSup hf hf_mono]
    rw [lintegral_iSup (fun n => Measurable.mono (hf n) hm le_rfl) hf_mono]
    congr with n
    exact hf_prop n

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s t : Set α
⊢ SigmaFinite (μ.restrict μ.sigmaFiniteSet)

Tactic:
Measure.sigmaFiniteSet

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s t : Set α
⊢ SigmaFinite (μ.restrict (μ.sigmaFiniteSetWRT μ))
Module: Mathlib.Topology.Perfect

Goal state before:
pp: case h.left
α : 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

Tactic:
refine ⟨hC.closure_nhds_inter x xC xU Uop, ?_⟩
    rw [hC.closed.closure_subset_iff]
    exact inter_subset_right

Goal state after:
Module: Mathlib.Analysis.Normed.Group.InfiniteSum

Goal state before:
pp: ι : Type u_1
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ᶠ (i : ι) in cofinite, ‖f i‖ ≤ g i
⊢ CauchySeq fun s ↦ ∑ i ∈ s, f i

Tactic:
refine cauchySeq_finset_iff_vanishing_norm.2 fun ε hε => ?_
  rcases summable_iff_vanishing_norm.1 hg ε hε with ⟨s, hs⟩
  classical
  refine ⟨s ∪ h.toFinset, fun t ht => ?_⟩
  have : ∀ i ∈ t, ‖f i‖ ≤ g i := by
    intro i hi
    simp only [disjoint_left, mem_union, not_or, h.mem_toFinset, Set.mem_compl_iff,
      Classical.not_not] at ht
    exact (ht hi).2
  calc
    ‖∑ i ∈ t, f i‖ ≤ ∑ i ∈ t, g i := norm_sum_le_of_le _ this
    _ ≤ ‖∑ i ∈ t, g i‖ := le_abs_self _
    _ < ε := hs _ (ht.mono_right le_sup_left)

Goal state after:
Module: Mathlib.Analysis.Normed.Group.FunctionSeries

Goal state before:
pp: β : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
ι : Type u_4
f : ι → β → F
u : ι → ℝ
hu : Summable u
s : Set β
hfu : ∀ᶠ (n : ι) in cofinite, ∀ x ∈ s, ‖f n x‖ ≤ u n
ε : ℝ
εpos : ε > 0
t : Finset ι
ht : ∀ (b : Finset ι), t ⊆ b → ∑' (a : { x // x ∉ b }), u ↑a < ε
⊢ ∃ a, ∀ (b : Finset ι), a ⊆ b → ∀ x ∈ s, dist (∑' (n : ι), f n x) (∑ n ∈ b, f n x) < ε

Tactic:
rw [eventually_iff_exists_mem] at hfu

Goal state after:
β : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
ι : Type u_4
f : ι → β → F
u : ι → ℝ
hu : Summable u
s : Set β
hfu : ∃ v ∈ cofinite, ∀ y ∈ v, ∀ x ∈ s, ‖f y x‖ ≤ u y
ε : ℝ
εpos : ε > 0
t : Finset ι
ht : ∀ (b : Finset ι), t ⊆ b → ∑' (a : { x // x ∉ b }), u ↑a < ε
⊢ ∃ a, ∀ (b : Finset ι), a ⊆ b → ∀ x ∈ s, dist (∑' (n : ι), f n x) (∑ n ∈ b, f n x) < ε
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_5
β : Type u_6
ι : Type u_7
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst✝⁷, inst✝²] fun i ↦ u i x
h : ∀ (i : ι), StronglyMeasurable (u i)
⊢ StronglyMeasurable (uncurry u)

Tactic:
borelize β

Goal state after:
α : Type u_5
β : Type u_6
ι : Type u_7
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst✝⁷, inst✝²] fun i ↦ u i x
h : ∀ (i : ι), StronglyMeasurable (u i)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ StronglyMeasurable (uncurry u)
Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence

Goal state before:
pp: case a
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hF_meas : AEMeasurable F μ
hf_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
g : ℕ → α → ℝ≥0∞
gmeas : ∀ (n : ℕ), Measurable (g n)
gf : ∀ (n : ℕ), g n ≤ f n
hg : ∀ (n : ℕ), ∫⁻ (a : α), f n a ∂μ = ∫⁻ (a : α), g n a ∂μ
g' : ℕ → α → ℝ≥0∞ := ⋯
M : ∀ (n : ℕ), Measurable (g' n)
I : ∀ (n : ℕ) (x : α), g n x ≤ g' n x
I' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), g' n x ≤ f n x
n : ℕ
⊢ ∫⁻ (x : α), g' n x ∂μ ≤ ∫⁻ (x : α), f n x ∂μ

pp: case a
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hF_meas : AEMeasurable F μ
hf_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
g : ℕ → α → ℝ≥0∞
gmeas : ∀ (n : ℕ), Measurable (g n)
gf : ∀ (n : ℕ), g n ≤ f n
hg : ∀ (n : ℕ), ∫⁻ (a : α), f n a ∂μ = ∫⁻ (a : α), g n a ∂μ
g' : ℕ → α → ℝ≥0∞ := ⋯
M : ∀ (n : ℕ), Measurable (g' n)
I : ∀ (n : ℕ) (x : α), g n x ≤ g' n x
I' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), g' n x ≤ f n x
n : ℕ
⊢ ∫⁻ (x : α), f n x ∂μ ≤ ∫⁻ (x : α), g' n x ∂μ

Tactic:
· apply lintegral_mono_ae
      filter_upwards [I'] with x hx using hx n

Goal state after:
case a
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hF_meas : AEMeasurable F μ
hf_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
g : ℕ → α → ℝ≥0∞
gmeas : ∀ (n : ℕ), Measurable (g n)
gf : ∀ (n : ℕ), g n ≤ f n
hg : ∀ (n : ℕ), ∫⁻ (a : α), f n a ∂μ = ∫⁻ (a : α), g n a ∂μ
g' : ℕ → α → ℝ≥0∞ := ⋯
M : ∀ (n : ℕ), Measurable (g' n)
I : ∀ (n : ℕ) (x : α), g n x ≤ g' n x
I' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), g' n x ≤ f n x
n : ℕ
⊢ ∫⁻ (x : α), f n x ∂μ ≤ ∫⁻ (x : α), g' n x ∂μ
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε
x : X
y : Y
z : X
⊢ glueDist Φ Ψ ε (Sum.inl x) (Sum.inl z) ≤
    glueDist Φ Ψ ε (Sum.inl x) (Sum.inr y) + glueDist Φ Ψ ε (Sum.inr y) (Sum.inl z)

Tactic:
simp_rw [glueDist, add_add_add_comm _ ε, add_assoc]
  refine le_ciInf_add fun p => ?_
  rw [add_left_comm, add_assoc, ← two_mul]
  refine le_ciInf_add fun q => ?_
  rw [dist_comm z]
  linarith [dist_triangle4 x (Φ p) (Φ q) z, dist_triangle_left (Ψ p) (Ψ q) y, (abs_le.1 (H p q)).2]

Goal state after: