mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

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

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

Goal state after:
Module: Mathlib.MeasureTheory.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
⊢ μ s = μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' {∞}) + ∑' (n : ℤ), μ (s ∩ f ⁻¹' Ico (↑t ^ n) (↑t ^ (n + 1)))

Tactic:
have A : μ s = μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' Ioi 0) := by
    rw [← measure_union]
    · rw [← inter_union_distrib_left, ← preimage_union, singleton_union, Ioi_insert,
        ← _root_.bot_eq_zero, Ici_bot, preimage_univ, inter_univ]
    · exact disjoint_singleton_left.mpr self_notMem_Ioi
        |>.preimage f |>.inter_right' s |>.inter_left' s
    · exact hs.inter (hf measurableSet_Ioi)
  have B : μ (s ∩ f ⁻¹' Ioi 0) = μ (s ∩ f ⁻¹' {∞}) + μ (s ∩ f ⁻¹' Ioo 0 ∞) := by
    rw [← measure_union]
    · 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]
    · refine disjoint_left.2 fun x hx h'x => ?_
      have : f x < ∞ := h'x.2.2
      exact lt_irrefl _ (this.trans_le (le_of_eq hx.2.symm))
    · exact hs.inter (hf measurableSet_Ioo)
  have C : μ (s ∩ f ⁻¹' Ioo 0 ∞) =
      ∑' n : ℤ, μ (s ∩ f ⁻¹' Ico ((t : ℝ≥0∞) ^ n) ((t : ℝ≥0∞) ^ (n + 1))) := by
    rw [← measure_iUnion,
      ENNReal.Ioo_zero_top_eq_iUnion_Ico_zpow (ENNReal.one_lt_coe_iff.2 ht) ENNReal.coe_ne_top,
      preimage_iUnion, inter_iUnion]
    · 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
    · intro n
      exact hs.inter (hf measurableSet_Ico)
  rw [A, B, C, add_assoc]

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

Goal state before:
pp: case pos
α : 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
⊢ 0 ≤ c

Tactic:
exact hc

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hs : MeasurableSet s
hf : AEStronglyMeasurable f (μ.restrict s)
hg : AEStronglyMeasurable g (μ.restrict sᶜ)
h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = AEStronglyMeasurable.mk f hf x
⊢ ∀ᵐ (x : α) ∂μ.restrict s,
    s.piecewise f g x = s.piecewise (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x

Tactic:
rw [ae_restrict_iff' hs]

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hs : MeasurableSet s
hf : AEStronglyMeasurable f (μ.restrict s)
hg : AEStronglyMeasurable g (μ.restrict sᶜ)
h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = AEStronglyMeasurable.mk f hf x
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → s.piecewise f g x = s.piecewise (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x
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 : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, f n a ≤ f n.succ a
s : Set α
hs : {a | ¬∀ (i : ℕ), f i a ≤ f i.succ a} ⊆ s ∧ MeasurableSet s ∧ μ s = 0
g : ℕ → α → ℝ≥0∞ := fun n a ↦ if a ∈ s then 0 else f n a
g_eq_f : ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), g n a = f n a
⊢ ⨆ n, ∫⁻ (a : α), g n a ∂μ = ⨆ n, ∫⁻ (a : α), f n a ∂μ

Tactic:
simp only [lintegral_congr_ae (g_eq_f.mono fun _a ha => ha _)]

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᵐ[μ] g
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
hg : AEMeasurable g μ
hgf : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ
this : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, g x < f x + (↑n)⁻¹
x : α
hlt : ∀ (i : ℕ), g x < f x + (↑i)⁻¹
hle : f x ≤ g x
⊢ Tendsto (fun n ↦ f x + (↑n)⁻¹) atTop (𝓝 (f x))

Tactic:
simpa only [inv_top, add_zero] using
    tendsto_const_nhds.add (tendsto_inv_iff.2 ENNReal.tendsto_nat_nhds_top)

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hμ : ¬μ univ = 0
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
h : ∀ᵐ (x : α) ∂μ, f x < g x
⊢ ∀ᵐ (x : α) ∂μ, x ∈ univ → f x < g x

Tactic:
simpa using h

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

Goal state before:

Tactic:
∫⁻ a, f a + g a ∂μ = ∫⁻ a, φ a ∂μ := hφ_eq
    _ ≤ ∫⁻ a, f a + (φ a - f a) ∂μ := lintegral_mono fun a => le_add_tsub
    _ = ∫⁻ a, f a ∂μ + ∫⁻ a, φ a - f a ∂μ := lintegral_add_aux hf (hφm.sub hf)
    _ ≤ ∫⁻ a, f a ∂μ + ∫⁻ a, g a ∂μ := by gcongr with a; exact tsub_le_iff_left.2 <| hφ_le _

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

Goal state before:
pp: α : Type u_1
E : Type u_5
m : MeasurableSpace α
f g : α → E
inst✝¹ : TopologicalSpace E
inst✝ : MetrizableSpace E
hf : StronglyMeasurable f
hg : StronglyMeasurable g
⊢ MeasurableSet {a | f a = g a}

Tactic:
borelize (E × E)
  exact (hf.prodMk hg).measurable isClosed_diagonal.measurableSet

Goal state after:
Module: Mathlib.Topology.Perfect

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
C : Set α
x : α
U : Set α
h_acc : AccPt x (𝓟 C)
hU : U ∈ 𝓝 x
this : 𝓝[≠] x ≤ 𝓟 U
⊢ AccPt x (𝓟 (U ∩ C))

Tactic:
rw [AccPt, ← inf_principal, ← inf_assoc, inf_of_le_left this]

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
C : Set α
x : α
U : Set α
h_acc : AccPt x (𝓟 C)
hU : U ∈ 𝓝 x
this : 𝓝[≠] x ≤ 𝓟 U
⊢ (𝓝[≠] x ⊓ 𝓟 C).NeBot
Module: Mathlib.Topology.Perfect

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
C : Set α
hC : Preperfect C
x : α
hx : x ∈ closure[inst✝] C
h : x ∉ C
this : {x}ᶜ ∩ C = C
⊢ (𝓝[≠] x ⊓ 𝓟 C).NeBot

Tactic:
nhdsWithin,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
C : Set α
hC : Preperfect C
x : α
hx : x ∈ closure[inst✝] C
h : x ∉ C
this : {x}ᶜ ∩ C = C
⊢ (𝓝 x ⊓ 𝓟 {x}ᶜ ⊓ 𝓟 C).NeBot
Module: Mathlib.Topology.Perfect

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
U : Set α
hu : U.Nontrivial
h : IsPreconnected U
⊢ Preperfect U

Tactic:
intro x hx
  rw [isPreconnected_closed_iff] at h
  specialize h {x} (closure (U \ {x})) isClosed_singleton isClosed_closure ?_ ?_ ?_
  · trans {x} ∪ (U \ {x})
    · simp
    apply Set.union_subset_union_right
    exact subset_closure
  · exact Set.inter_singleton_nonempty.mpr hx
  · 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]
  · apply Set.Nonempty.right at h
    rw [Set.singleton_inter_nonempty, mem_closure_iff_clusterPt,
      ← accPt_principal_iff_clusterPt] at h
    exact h

Goal state after:
Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf : LocallyLipschitzOn s f
⊢ ∃ K, LipschitzOnWith K f s

Tactic:
have hf' := hf.continuousOn

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf : LocallyLipschitzOn s f
hf' : ContinuousOn f s
⊢ ∃ K, LipschitzOnWith K f s
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: E : ℕ → Type u_1
x y : (n : ℕ) → E n
hne : x ≠ y
i : ℕ
⊢ x ∈ cylinder y i ↔ i ≤ firstDiff x y

Tactic:
constructor
  · intro h
    by_contra!
    exact apply_firstDiff_ne hne (h _ this)
  · intro hi j hj
    exact apply_eq_of_lt_firstDiff (hj.trans_le hi)

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

Goal state before:
pp: case mpr.succ
α : Type u_2
x y : ℕ → α
n : ℕ
ih : (∀ ⦃m : ℕ⦄, m < n → x m = y m) → res x n = res y n
h : ∀ ⦃m : ℕ⦄, m < n + 1 → x m = y m
⊢ res x (n + 1) = res y (n + 1)

Tactic:
simp only [res_succ, cons.injEq]

Goal state after:
case mpr.succ
α : Type u_2
x y : ℕ → α
n : ℕ
ih : (∀ ⦃m : ℕ⦄, m < n → x m = y m) → res x n = res y n
h : ∀ ⦃m : ℕ⦄, m < n + 1 → x m = y m
⊢ x n = y n ∧ res x n = res y n
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case mpr
α : Type u_2
x y : ℕ → α
n : ℕ
h : ∀ ⦃m : ℕ⦄, m < n → x m = y m
⊢ res x n = res y n

Tactic:
· induction n with
    | zero => simp
    | succ n ih =>
      simp only [res_succ, cons.injEq]
      refine ⟨h (Nat.lt_succ_self _), ih fun m hm => ?_⟩
      exact h (hm.trans (Nat.lt_succ_self _))

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : MetricSpace α
s : Opens α
inst✝ : CompleteSpace α
u : ℕ → s.CompleteCopy
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (1 / 2) ^ N
⊢ Tendsto (fun n ↦ (1 / 2) ^ n) atTop (𝓝 0)

Tactic:
exact tendsto_pow_atTop_nhds_zero_of_lt_one (by simp) (by norm_num)

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

Goal state before:
pp: case succ
β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
x y : ↑(inducedMap A).fst
hxy : (inducedMap A).snd x = (inducedMap A).snd y
n : ℕ
ih : res (↑x) n = res (↑y) n
⊢ res (↑x) (n + 1) = res (↑y) (n + 1)

Tactic:
simp only [res_succ, cons.injEq]

Goal state after:
case succ
β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
x y : ↑(inducedMap A).fst
hxy : (inducedMap A).snd x = (inducedMap A).snd y
n : ℕ
ih : res (↑x) n = res (↑y) n
⊢ ↑x n = ↑y n ∧ res (↑x) n = res (↑y) n
Module: Mathlib.Topology.MetricSpace.CantorScheme

Goal state before:
pp: β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), (A l).Nonempty
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
⊢ ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)

Tactic:
have : Antitone fun n : ℕ => A (res x n) := by
      refine antitone_nat_of_succ_le ?_
      intro n
      apply hanti.antitone

Goal state after:
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), (A l).Nonempty
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
this : Antitone fun n ↦ A (res x n)
⊢ ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
Module: Mathlib.Dynamics.Ergodic.MeasurePreserving

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
ga : α → α
gb : β → β
hfm : MeasurePreserving f μa μb
hga : MeasurePreserving ga μa μa
hf : Semiconj f ga gb
hgb : Measurable gb
⊢ MeasurePreserving gb μb μb

Tactic:
have := hf.comp_eq ▸ hfm.comp hga |>.map_of_comp hgb hfm.measurable

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
ga : α → α
gb : β → β
hfm : MeasurePreserving f μa μb
hga : MeasurePreserving ga μa μa
hf : Semiconj f ga gb
hgb : Measurable gb
this : MeasurePreserving gb (map f μa) μb
⊢ MeasurePreserving gb μb μb
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case inr
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_3
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
f : β → α
f_cont : Continuous[inst✝¹, inst✝²] f
h✝ : Nonempty β
g : (ℕ → ℕ) → β
g_cont : Continuous[_, inst✝¹] g
hg : Surjective g
⊢ range (f ∘ g) = range f

Tactic:
rw [hg.range_comp]

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
g : α → β
hg : MeasurableEmbedding g
f : β → ℝ≥0∞
f₀ : SimpleFunc α ℝ≥0∞
hf₀ : ⇑f₀ ≤ fun a ↦ f (g a)
⊢ (f₀.extend g hg (const β 0)).lintegral (Measure.map g μ) ≤
    ⨆ g_1, ⨆ (_ : ⇑g_1 ≤ fun a ↦ f a), g_1.lintegral (Measure.map g μ)

Tactic:
←
      SimpleFunc.lintegral_eq_lintegral,

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
g : α → β
hg : MeasurableEmbedding g
f : β → ℝ≥0∞
f₀ : SimpleFunc α ℝ≥0∞
hf₀ : ⇑f₀ ≤ fun a ↦ f (g a)
⊢ ∫⁻ (a : β), (f₀.extend g hg (const β 0)) a ∂Measure.map g μ ≤
    ⨆ g_1, ⨆ (_ : ⇑g_1 ≤ fun a ↦ f a), g_1.lintegral (Measure.map g μ)
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case neg
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n := fun x ↦ if x ∈ s then x else ⋯.some
fs : ∀ x ∈ s, f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∉ s
ys : y ∉ s
Ax : (s ∩ cylinder x (longestPrefix x s)).Nonempty
fx : f x = Ax.some
Ay : (s ∩ cylinder y (longestPrefix y s)).Nonempty
fy : f y = Ay.some
⊢ firstDiff x y ≤ firstDiff (f x) (f y)

Tactic:
by_cases! H : longestPrefix x s < firstDiff x y ∨ longestPrefix y s < firstDiff x y

Goal state after:
case pos
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n := fun x ↦ if x ∈ s then x else ⋯.some
fs : ∀ x ∈ s, f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∉ s
ys : y ∉ s
Ax : (s ∩ cylinder x (longestPrefix x s)).Nonempty
fx : f x = Ax.some
Ay : (s ∩ cylinder y (longestPrefix y s)).Nonempty
fy : f y = Ay.some
H : longestPrefix x s < firstDiff x y ∨ longestPrefix y s < firstDiff x y
⊢ firstDiff x y ≤ firstDiff (f x) (f y)

case neg
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n := fun x ↦ if x ∈ s then x else ⋯.some
fs : ∀ x ∈ s, f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∉ s
ys : y ∉ s
Ax : (s ∩ cylinder x (longestPrefix x s)).Nonempty
fx : f x = Ax.some
Ay : (s ∩ cylinder y (longestPrefix y s)).Nonempty
fy : f y = Ay.some
H : firstDiff x y ≤ longestPrefix x s ∧ firstDiff x y ≤ longestPrefix y s
⊢ firstDiff x y ≤ firstDiff (f x) (f y)
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: α : Type u_4
mα : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
μ : Measure α
s : Finset α
hμ : ∀ᵐ (a : α) ∂μ, a ∈ s
t : Set α
ht : MeasurableSet t
⊢ ∑ p ∈ s, μ (t ∩ {p}) = ∑ x ∈ s, μ {x} • (dirac x) t

Tactic:
congr with a

Goal state after:
case e_f
α : Type u_4
mα : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
μ : Measure α
s : Finset α
hμ : ∀ᵐ (a : α) ∂μ, a ∈ s
t : Set α
ht : MeasurableSet t
a : α
⊢ μ (t ∩ {a}) = μ {a} • (dirac a) t
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
f g : (ℕ → ℕ) → α
hf : Continuous[_, inst✝³] f
hg : Continuous[_, inst✝³] g
h : Disjoint (range f) (range g)
hfg : ¬MeasurablySeparable (range f) (range g)
n : ℕ
x y : ℕ → ℕ
H :
  ∀ (x' y' : ℕ → ℕ),
    x' ∈ cylinder x n → y' ∈ cylinder y n → MeasurablySeparable (f '' cylinder x' (n + 1)) (g '' cylinder y' (n + 1))
⊢ MeasurablySeparable (f '' cylinder x n) (g '' cylinder y n)

Tactic:
rw [← iUnion_cylinder_update x n, ← iUnion_cylinder_update y n, image_iUnion, image_iUnion]

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
f g : (ℕ → ℕ) → α
hf : Continuous[_, inst✝³] f
hg : Continuous[_, inst✝³] g
h : Disjoint (range f) (range g)
hfg : ¬MeasurablySeparable (range f) (range g)
n : ℕ
x y : ℕ → ℕ
H :
  ∀ (x' y' : ℕ → ℕ),
    x' ∈ cylinder x n → y' ∈ cylinder y n → MeasurablySeparable (f '' cylinder x' (n + 1)) (g '' cylinder y' (n + 1))
⊢ MeasurablySeparable (⋃ i, f '' cylinder (update x n i) (n + 1)) (⋃ i, g '' cylinder (update y n i) (n + 1))
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
f g : (ℕ → ℕ) → α
hf : Continuous[_, inst✝³] f
hg : Continuous[_, inst✝³] g
h : Disjoint (range f) (range g)
hfg : ¬MeasurablySeparable (range f) (range g)
I :
  ∀ (n : ℕ) (x y : ℕ → ℕ),
    ¬MeasurablySeparable (f '' cylinder x n) (g '' cylinder y n) →
      ∃ x' y',
        x' ∈ cylinder x n ∧
          y' ∈ cylinder y n ∧ ¬MeasurablySeparable (f '' cylinder x' (n + 1)) (g '' cylinder y' (n + 1))
A : Type := { p // ¬MeasurablySeparable (f '' cylinder p.2.1 p.1) (g '' cylinder p.2.2 p.1) }
F : A → A
hFn : ∀ (p : A), (↑(F p)).1 = (↑p).1 + 1
hFx : ∀ (p : A), (↑(F p)).2.1 ∈ cylinder (↑p).2.1 (↑p).1
hFy : ∀ (p : A), (↑(F p)).2.2 ∈ cylinder (↑p).2.2 (↑p).1
p0 : A := ⟨(0, fun x ↦ 0, fun x ↦ 0), ⋯⟩
p : ℕ → A := fun n ↦ F^[n] p0
prec : ∀ (n : ℕ), p (n + 1) = F (p n)
pn_fst : ∀ (n : ℕ), (↑(p n)).1 = n
Ix : ∀ (m n : ℕ), m + 1 ≤ n → (↑(p n)).2.1 m = (↑(p (m + 1))).2.1 m
m n : ℕ
hmn : m + 1 ≤ n
IH : (↑(p n)).2.2 m = (↑(p (m + 1))).2.2 m
⊢ (↑(F (p n))).2.2 m = (↑(p n)).2.2 m

Tactic:
apply hFy (p n) m

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
f g : (ℕ → ℕ) → α
hf : Continuous[_, inst✝³] f
hg : Continuous[_, inst✝³] g
h : Disjoint (range f) (range g)
hfg : ¬MeasurablySeparable (range f) (range g)
I :
  ∀ (n : ℕ) (x y : ℕ → ℕ),
    ¬MeasurablySeparable (f '' cylinder x n) (g '' cylinder y n) →
      ∃ x' y',
        x' ∈ cylinder x n ∧
          y' ∈ cylinder y n ∧ ¬MeasurablySeparable (f '' cylinder x' (n + 1)) (g '' cylinder y' (n + 1))
A : Type := ⋯
F : A → A
hFn : ∀ (p : A), (↑(F p)).1 = (↑p).1 + 1
hFx : ∀ (p : A), (↑(F p)).2.1 ∈ cylinder (↑p).2.1 (↑p).1
hFy : ∀ (p : A), (↑(F p)).2.2 ∈ cylinder (↑p).2.2 (↑p).1
p0 : A := ⋯
p : ℕ → A := ⋯
prec : ∀ (n : ℕ), p (n + 1) = F (p n)
pn_fst : ∀ (n : ℕ), (↑(p n)).1 = n
Ix : ∀ (m n : ℕ), m + 1 ≤ n → (↑(p n)).2.1 m = (↑(p (m + 1))).2.1 m
m n : ℕ
hmn : m + 1 ≤ n
IH : (↑(p n)).2.2 m = (↑(p (m + 1))).2.2 m
⊢ m < (↑(p n)).1
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0∞
m : Measure (Measure α)
g : α → ℝ≥0∞
hgm : Measurable g
hgf : g ≤ f
hfg_int : ∫⁻ (a : α), f a ∂m.join = ∫⁻ (a : α), g a ∂m.join
⊢ ∫⁻ (x : α), f x ∂m.join ≤ ∫⁻ (μ : Measure α), ∫⁻ (x : α), f x ∂μ ∂m

Tactic:
rw [hfg_int, lintegral_join hgm.aemeasurable]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0∞
m : Measure (Measure α)
g : α → ℝ≥0∞
hgm : Measurable g
hgf : g ≤ f
hfg_int : ∫⁻ (a : α), f a ∂m.join = ∫⁻ (a : α), g a ∂m.join
⊢ ∫⁻ (μ : Measure α), ∫⁻ (x : α), g x ∂μ ∂m ≤ ∫⁻ (μ : Measure α), ∫⁻ (x : α), f x ∂μ ∂m
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U : Set α
ε : ℝ≥0∞
H : μ.InnerRegularWRT p q
h0 : p ∅
hU : q U
hμU : μ U ≠ ∞
hε : ε ≠ 0
⊢ ∃ K ⊆ U, p K ∧ μ U < μ K + ε

Tactic:
rcases eq_or_ne (μ U) 0 with h₀ | h₀

Goal state after:
case inl
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U : Set α
ε : ℝ≥0∞
H : μ.InnerRegularWRT p q
h0 : p ∅
hU : q U
hμU : μ U ≠ ∞
hε : ε ≠ 0
h₀ : μ U = 0
⊢ ∃ K ⊆ U, p K ∧ μ U < μ K + ε

case inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U : Set α
ε : ℝ≥0∞
H : μ.InnerRegularWRT p q
h0 : p ∅
hU : q U
hμU : μ U ≠ ∞
hε : ε ≠ 0
h₀ : μ U ≠ 0
⊢ ∃ K ⊆ U, p K ∧ μ U < μ K + ε
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: γ : Type u_3
β : Type u_4
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : PolishSpace γ
inst✝³ : TopologicalSpace β
inst✝² : T2Space β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
f : γ → β
f_cont : Continuous[inst✝⁵, inst✝³] f
f_inj : Injective f
this✝ : UpgradedIsCompletelyMetrizableSpace γ := upgradeIsCompletelyMetrizable γ
b : Set (Set γ)
b_count : b.Countable
b_nonempty : ∅ ∉ b
hb : IsTopologicalBasis b
this : Encodable ↑b
A : Type (max 0 u_3) := { p // Disjoint ↑p.1 ↑p.2 }
q : A → Set β
hq1 : ∀ (p : A), f '' ↑(↑p).1 ⊆ q p
hq2 : ∀ (p : A), Disjoint (f '' ↑(↑p).2) (q p)
q_meas : ∀ (p : A), MeasurableSet (q p)
E : ↑b → Set β := fun s ↦ closure[inst✝³] (f '' ↑s) ∩ ⋂ t, ⋂ (ht : Disjoint ↑s ↑t), q ⟨(s, t), ht⟩ \ q ⟨(t, s), ⋯⟩
u : ℕ → ℝ
u_anti : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
F : ℕ → Set β := fun n ↦ ⋃ s, ⋃ (_ : Bornology.IsBounded ↑s ∧ diam ↑s ≤ u n), E s
⊢ MeasurableSet (range f)

Tactic:
suffices range f = ⋂ n, F n by
    have E_meas : ∀ s : b, MeasurableSet (E s) := by
      intro b
      refine isClosed_closure.measurableSet.inter ?_
      refine MeasurableSet.iInter fun s => ?_
      exact MeasurableSet.iInter fun hs => (q_meas _).diff (q_meas _)
    have F_meas : ∀ n, MeasurableSet (F n) := by
      intro n
      refine MeasurableSet.iUnion fun s => ?_
      exact MeasurableSet.iUnion fun _ => E_meas _
    rw [this]
    exact MeasurableSet.iInter fun n => F_meas n

Goal state after:
γ : Type u_3
β : Type u_4
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : PolishSpace γ
inst✝³ : TopologicalSpace β
inst✝² : T2Space β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
f : γ → β
f_cont : Continuous[inst✝⁵, inst✝³] f
f_inj : Injective f
this✝ : UpgradedIsCompletelyMetrizableSpace γ := upgradeIsCompletelyMetrizable γ
b : Set (Set γ)
b_count : b.Countable
b_nonempty : ∅ ∉ b
hb : IsTopologicalBasis b
this : Encodable ↑b
A : Type (max 0 u_3) := { p // Disjoint ↑p.1 ↑p.2 }
q : A → Set β
hq1 : ∀ (p : A), f '' ↑(↑p).1 ⊆ q p
hq2 : ∀ (p : A), Disjoint (f '' ↑(↑p).2) (q p)
q_meas : ∀ (p : A), MeasurableSet (q p)
E : ↑b → Set β := fun s ↦ closure[inst✝³] (f '' ↑s) ∩ ⋂ t, ⋂ (ht : Disjoint ↑s ↑t), q ⟨(s, t), ht⟩ \ q ⟨(t, s), ⋯⟩
u : ℕ → ℝ
u_anti : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
F : ℕ → Set β := fun n ↦ ⋃ s, ⋃ (_ : Bornology.IsBounded ↑s ∧ diam ↑s ≤ u n), E s
⊢ range f = ⋂ n, F n
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: case refine_2
α : Type u_4
β : Type u_5
γ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure ((α × β) × γ)
inst✝ : IsFiniteMeasure μ
h_eq :
  ∀ (ν : Measure ((α × β) × γ)) {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s →
      MeasurableSet t → MeasurableSet u → (map (⇑MeasurableEquiv.prodAssoc) ν) (s ×ˢ t ×ˢ u) = ν ((s ×ˢ t) ×ˢ u)
s : Set α
t : Set β
u : Set γ
h : μ ((s ×ˢ t) ×ˢ u) = ν ((s ×ˢ t) ×ˢ u)
hs : MeasurableSet s
ht : MeasurableSet t
hu : MeasurableSet u
⊢ (map (⇑MeasurableEquiv.prodAssoc) μ) (s ×ˢ t ×ˢ u) = (map (⇑MeasurableEquiv.prodAssoc) ν) (s ×ˢ t ×ˢ u)

Tactic:
· rwa [h_eq μ hs ht hu, h_eq ν hs ht hu]

Goal state after: