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

Goal state before:
pp: α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A : μ s = μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' Ioi 0)
B : μ (s ∩ f ⁻¹' Ioi 0) = μ (s ∩ f ⁻¹' {∞}) + μ (s ∩ f ⁻¹' Ioo 0 ∞)
C : μ (s ∩ f ⁻¹' Ioo 0 ∞) = ∑' (n : ℤ), μ (s ∩ f ⁻¹' Ico (↑t ^ n) (↑t ^ (n + 1)))
⊢ μ s = μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' {∞}) + ∑' (n : ℤ), μ (s ∩ f ⁻¹' Ico (↑t ^ n) (↑t ^ (n + 1)))

Tactic:
A,

Goal state after:
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A : μ s = μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' Ioi 0)
B : μ (s ∩ f ⁻¹' Ioi 0) = μ (s ∩ f ⁻¹' {∞}) + μ (s ∩ f ⁻¹' Ioo 0 ∞)
C : μ (s ∩ f ⁻¹' Ioo 0 ∞) = ∑' (n : ℤ), μ (s ∩ f ⁻¹' Ico (↑t ^ n) (↑t ^ (n + 1)))
⊢ μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' Ioi 0) =
    μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' {∞}) + ∑' (n : ℤ), μ (s ∩ f ⁻¹' Ico (↑t ^ n) (↑t ^ (n + 1)))
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
⊢ ⨆ g, ⨆ (_ : Measurable g), ⨆ (_ : g ≤ f), ∫⁻ (a : α), g a ∂μ = ∫⁻ (a : α), f a ∂μ

Tactic:
by
  apply le_antisymm
  · exact iSup_le fun i => iSup_le fun _ => iSup_le fun h'i => lintegral_mono h'i
  · rw [lintegral]
    refine iSup₂_le fun i hi => le_iSup₂_of_le i i.measurable <| le_iSup_of_le hi ?_
    exact le_of_eq (i.lintegral_eq_lintegral _).symm

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
mβ : MeasurableSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : BorelSpace β
f : α → β
hf : AEStronglyMeasurable f μ
t : Set β
ht1 : IsSeparable t
ht2 : ∀ᵐ (x : α) ∂μ, f x ∈ t
⊢ ∀ᵐ (x : α) ∂μ, (⋂₀ {t_1 | IsClosed[inst✝²] t_1 ∧ t ⊆ t_1}) (f x)

Tactic:
filter_upwards [ht2] with ω hω using subset_closure hω

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

Goal state before:
pp: case neg.inl
α : 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 : ‖(hf.approx n) x‖ ≤ c
⊢ ‖1‖ * ‖(hf.approx n) x‖ ≤ c

Tactic:
simpa only [norm_one, one_mul] using h

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

Goal state before:
pp: case h
α : 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}
p : ℝ≥0∞
i j : ℕ
h : i ≤ j
⊢ ⇑(SimpleFunc.map c rs) ⁻¹' {p} ∩ {a | p ≤ f i a} ⊆ ⇑(SimpleFunc.map c rs) ⁻¹' {p} ∩ {a | p ≤ f j a}

Tactic:
exact mono p h

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f g : α → ℝ≥0∞
hg : AEMeasurable g (μ.restrict s)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ g x
f' : α → ℝ≥0∞
hf'm : Measurable f'
hle : f' ≤ f
hf' : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, f' a ∂μ
⊢ ∀ᵐ (a : α) ∂μ.restrict s, f' a ≤ g a

Tactic:
rw [ae_restrict_iff₀]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f g : α → ℝ≥0∞
hg : AEMeasurable g (μ.restrict s)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ g x
f' : α → ℝ≥0∞
hf'm : Measurable f'
hle : f' ≤ f
hf' : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, f' a ∂μ
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → f' x ≤ g x

α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f g : α → ℝ≥0∞
hg : AEMeasurable g (μ.restrict s)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ g x
f' : α → ℝ≥0∞
hf'm : Measurable f'
hle : f' ≤ f
hf' : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, f' a ∂μ
⊢ NullMeasurableSet {x | f' x ≤ g x} (μ.restrict s)
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: case inr.refine_1
α : Type u_1
β : Type u_2
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
⊢ ∃ c, f = fun x ↦ c

Tactic:
refine ⟨f hα.some, ?_⟩
    let fs := hf.approx
    have h_fs_tendsto : ∀ x, Tendsto (fun n => fs n x) atTop (𝓝 (f x)) := hf.tendsto_approx
    have : ∀ n, ∃ c, ∀ x, fs n x = c := fun n => SimpleFunc.simpleFunc_bot (fs n)
    let cs n := (this n).choose
    have h_cs_eq : ∀ n, ⇑(fs n) = fun _ => cs n := fun n => funext (this n).choose_spec
    conv at h_fs_tendsto => enter [x, 1, n]; rw [h_cs_eq]
    have h_tendsto : Tendsto cs atTop (𝓝 (f hα.some)) := h_fs_tendsto hα.some
    ext1 x
    exact tendsto_nhds_unique (h_fs_tendsto x) h_tendsto

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∫⁻ (a : α), f a ∂μ = 0
meas_levels_0 : ∀ ε > 0, μ {x | ε ≤ f x} = 0
u : ℕ → ℝ≥0∞
bu : ∀ (n : ℕ), u n ∈ Ioo 0 1
tu : Tendsto u atTop (𝓝 0)
x : α
⊢ f x ≠ 0 ↔ ∃ i, x ∈ {x | u i ≤ f x}

Tactic:
← pos_iff_ne_zero

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∫⁻ (a : α), f a ∂μ = 0
meas_levels_0 : ∀ ε > 0, μ {x | ε ≤ f x} = 0
u : ℕ → ℝ≥0∞
bu : ∀ (n : ℕ), u n ∈ Ioo 0 1
tu : Tendsto u atTop (𝓝 0)
x : α
⊢ 0 < f x ↔ ∃ i, x ∈ {x | u i ≤ f x}
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
μ : Measure α
f₁ f₁' : α → β
f₂ f₂' : α → γ
h₁✝ : f₁ =ᵐ[μ] f₁'
h₂✝ : f₂ =ᵐ[μ] f₂'
g : β → γ → ℝ≥0∞
x✝ : α
h₂ : f₂ x✝ = f₂' x✝
h₁ : f₁ x✝ = f₁' x✝
⊢ (fun a ↦ g (f₁ a) (f₂ a)) x✝ = (fun a ↦ g (f₁' a) (f₂' a)) x✝

Tactic:
dsimp only; rw [h₁, h₂]

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
n : ℕ
⊢ ∃ t,
    MeasurableSet t ∧
      SigmaFinite (μ.restrict t) ∧
        (⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s) - 1 / ↑n ≤ ν t

Tactic:
by_cases! hC_lt : 1 / n < ⨆ (s) (_ : MeasurableSet s) (_ : SigmaFinite (μ.restrict s)), ν s

Goal state after:
case pos
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
n : ℕ
hC_lt : 1 / ↑n < ⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s
⊢ ∃ t,
    MeasurableSet t ∧
      SigmaFinite (μ.restrict t) ∧
        (⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s) - 1 / ↑n ≤ ν t

case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
n : ℕ
hC_lt : ⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s ≤ 1 / ↑n
⊢ ∃ t,
    MeasurableSet t ∧
      SigmaFinite (μ.restrict t) ∧
        (⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s) - 1 / ↑n ≤ ν t
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: case hf
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∀ (n : ℕ), Measurable ⇑(const α r * eapprox f n)

Tactic:
intro n
        exact SimpleFunc.measurable _

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : AEMeasurable f μ
A : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), AEMeasurable.mk f hf a ∂μ
B : ∫⁻ (a : α), r * f a ∂μ = ∫⁻ (a : α), r * AEMeasurable.mk f hf a ∂μ
⊢ ∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (a : α), f a ∂μ

Tactic:
A,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : AEMeasurable f μ
A : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), AEMeasurable.mk f hf a ∂μ
B : ∫⁻ (a : α), r * f a ∂μ = ∫⁻ (a : α), r * AEMeasurable.mk f hf a ∂μ
⊢ ∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (a : α), AEMeasurable.mk f hf a ∂μ
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' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
x : α
hx : x ∈ s
K' : ℝ
hK' : K' ∈ upperBounds ((fun y ↦ dist (f x) (f y) / dist x y) '' (s \ ball x (ε x hx)))
y : α
hy : y ∈ s.diff (ball x (ε x hx))
⊢ ↑(nndist (f x) (f y)) ≤ ↑(NNReal.mk (max K' 0) ⋯ * nndist x y)

Tactic:
ENNReal.coe_le_coe

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
x : α
hx : x ∈ s
K' : ℝ
hK' : K' ∈ upperBounds ((fun y ↦ dist (f x) (f y) / dist x y) '' (s \ ball x (ε x hx)))
y : α
hy : y ∈ s.diff (ball x (ε x hx))
⊢ nndist (f x) (f y) ≤ NNReal.mk (max K' 0) ⋯ * nndist x y
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: ⊢ CompactSpace ↑I

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b : α
h : a ≤ b
δ : α
hδ : 0 ≤ δ
t : ↑(Icc a b)
n : ℕ
ht : t ∈ Icc (addNSMul h δ n) (addNSMul h δ (n + 1))
⊢ |0 + ((n + 1) • δ - n • δ)| ≤ δ

Tactic:
zero_add,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b : α
h : a ≤ b
δ : α
hδ : 0 ≤ δ
t : ↑(Icc a b)
n : ℕ
ht : t ∈ Icc (addNSMul h δ n) (addNSMul h δ (n + 1))
⊢ |(n + 1) • δ - n • δ| ≤ δ
Module: Mathlib.Topology.Metrizable.CompletelyMetrizable

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : IsCompletelyPseudoMetrizableSpace X
inst✝ : T0Space X
this : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
⊢ CompleteSpace X

Tactic:
by infer_instance

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

Goal state before:
pp: α : Type u_2
x : ℕ → α
n : ℕ
⊢ (res x n).length = n

Tactic:
induction n <;> simp [*]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
f : α → β
hf : IsClosedEmbedding f
this✝¹ : UpgradedIsCompletelyMetrizableSpace β := upgradeIsCompletelyMetrizable β
this✝ : MetricSpace α := IsEmbedding.comapMetricSpace f ⋯
this : SecondCountableTopology α
⊢ PolishSpace α

Tactic:
have : CompleteSpace α := by
    rw [completeSpace_iff_isComplete_range hf.isEmbedding.to_isometry.isUniformInducing]
    exact hf.isClosed_range.isComplete

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
f : α → β
hf : IsClosedEmbedding f
this✝² : UpgradedIsCompletelyMetrizableSpace β := upgradeIsCompletelyMetrizable β
this✝¹ : MetricSpace α := IsEmbedding.comapMetricSpace f ⋯
this✝ : SecondCountableTopology α
this : CompleteSpace α
⊢ PolishSpace α
Module: Mathlib.Topology.MetricSpace.CantorScheme

Goal state before:
pp: case h
β : 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)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ y ∈ A (res x n), ∀ z ∈ A (res x n), dist y z < ε
m₀ : ℕ
hm₀ : m₀ ≥ n
m₁ : ℕ
hm₁ : m₁ ≥ n
⊢ dist (u m₀) (u m₁) < ε

Tactic:
apply hn <;> apply umem

Goal state after:
case h.x
β : 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)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ y ∈ A (res x n), ∀ z ∈ A (res x n), dist y z < ε
m₀ : ℕ
hm₀ : m₀ ≥ n
m₁ : ℕ
hm₁ : m₁ ≥ n
⊢ n ≤ m₀

case h.x
β : 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)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ y ∈ A (res x n), ∀ z ∈ A (res x n), dist y z < ε
m₀ : ℕ
hm₀ : m₀ ≥ n
m₁ : ℕ
hm₁ : m₁ ≥ n
⊢ n ≤ m₁
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOrProbabilityMeasure μ
s : Set α
⊢ μ univ ≤ 1

Tactic:
rcases IsZeroOrProbabilityMeasure.measure_univ (μ := μ) with h | h <;> simp [h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass α
inst✝ : MeasurableSingletonClass β
f : α → β
a : α
⊢ map f (dirac a) = dirac (f a)

Tactic:
by
  classical
  ext s hs
  rw [map_apply_of_aemeasurable (by fun_prop) hs]
  simp [indicator_apply]

Goal state after:
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
⊢ firstDiff x y ≤ firstDiff (f x) (f y)

Tactic:
· by_cases ys : y ∈ s
      -- case where `y ∈ s` (similar to the above)
      · have A : (s ∩ cylinder x (longestPrefix x s)).Nonempty :=
          inter_cylinder_longestPrefix_nonempty hs hne x
        have fx : f x = A.some := by simp_rw [f, if_neg xs]
        have I : cylinder A.some (firstDiff x y) = cylinder x (firstDiff x y) := by
          rw [← mem_cylinder_iff_eq]
          apply cylinder_anti x _ A.some_mem.2
          apply firstDiff_le_longestPrefix hs xs ys
        rw [fs y ys] at hfxfy ⊢
        rwa [← fx, I2, ← mem_cylinder_iff_eq, mem_cylinder_iff_le_firstDiff hfxfy] at I
      -- case where `y ∉ s`
      · have Ax : (s ∩ cylinder x (longestPrefix x s)).Nonempty :=
          inter_cylinder_longestPrefix_nonempty hs hne x
        have fx : f x = Ax.some := by simp_rw [f, if_neg xs]
        have Ay : (s ∩ cylinder y (longestPrefix y s)).Nonempty :=
          inter_cylinder_longestPrefix_nonempty hs hne y
        have fy : f y = Ay.some := by simp_rw [f, if_neg ys]
        -- case where the common prefix to `x` and `s`, or `y` and `s`, is shorter than the
        -- common part to `x` and `y` -- then `f x = f y`.
        by_cases! H : longestPrefix x s < firstDiff x y ∨ longestPrefix y s < firstDiff x y
        · have : cylinder x (longestPrefix x s) = cylinder y (longestPrefix y s) := by
            rcases H with H | H
            · exact cylinder_longestPrefix_eq_of_longestPrefix_lt_firstDiff hs hne H xs ys
            · symm
              rw [firstDiff_comm] at H
              exact cylinder_longestPrefix_eq_of_longestPrefix_lt_firstDiff hs hne H ys xs
          rw [fx, fy] at hfxfy
          apply (hfxfy _).elim
          congr
        -- case where the common prefix to `x` and `s` is long, as well as the common prefix to
        -- `y` and `s`. Then all points remain in the same cylinders.
        · have I1 : cylinder Ax.some (firstDiff x y) = cylinder x (firstDiff x y) := by
            rw [← mem_cylinder_iff_eq]
            exact cylinder_anti x H.1 Ax.some_mem.2
          have I3 : cylinder y (firstDiff x y) = cylinder Ay.some (firstDiff x y) := by
            rw [eq_comm, ← mem_cylinder_iff_eq]
            exact cylinder_anti y H.2 Ay.some_mem.2
          have : cylinder Ax.some (firstDiff x y) = cylinder Ay.some (firstDiff x y) := by
            rw [I1, I2, I3]
          rw [← fx, ← fy, ← mem_cylinder_iff_eq, mem_cylinder_iff_le_firstDiff hfxfy] at this
          exact this

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

Goal state before:
pp: X : Type u_3
Y : Type u_4
inst✝⁵ : MeasurableSpace X
inst✝⁴ : StandardBorelSpace X
inst✝³ : TopologicalSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : OpensMeasurableSpace Y
f : X → Y
inst✝ : SecondCountableTopology ↑(range f)
s : Set X
hs : MeasurableSet s
hf : Measurable f
this : UpgradedStandardBorel X := upgradeStandardBorel X
τ' : TopologicalSpace X
hle✝ : τ' ≤ this.toTopologicalSpace
hfc : Continuous[τ', inst✝³] f
hτ' : PolishSpace X
m' : MeasurableSpace X := borel X
b' : BorelSpace X
hle : borel X ≤ borel X
⊢ AnalyticSet (f '' s)

Tactic:
exact (hle _ hs).analyticSet.image_of_continuous hfc

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (a : α), f a ∂count = ∑' (a : α), f a

Tactic:
count,

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (a : α), f a ∂sum dirac = ∑' (a : α), f a
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
f : α → ℝ≥0∞
⊢ ∫⁻ (a : α), f a ∂count = ∑' (a : α), f a

Tactic:
count,

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
f : α → ℝ≥0∞
⊢ ∫⁻ (a : α), f a ∂sum dirac = ∑' (a : α), f a
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: α : Type u_2
inst✝³ : MetricSpace α
inst✝² : CompleteSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x | (⋂ n, closedBall (u (x n)) ((1 / 2) ^ n)).Nonempty}
g : ↑s → α := fun x ↦ Set.Nonempty.some ⋯
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
g_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
g_surj : Surjective g
s_closed : IsClosed s
⊢ ∃ f, Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f ∧ Surjective f

Tactic:
obtain ⟨f, -, f_surj, f_cont⟩ :
    ∃ f : (ℕ → ℕ) → s, (∀ x : s, f x = x) ∧ Surjective f ∧ Continuous f := by
    apply exists_retraction_subtype_of_isClosed s_closed
    simpa only [nonempty_coe_sort] using g_surj.nonempty

Goal state after:
α : Type u_2
inst✝³ : MetricSpace α
inst✝² : CompleteSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x | (⋂ n, closedBall (u (x n)) ((1 / 2) ^ n)).Nonempty}
g : ↑s → α := fun x ↦ Set.Nonempty.some ⋯
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
g_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
g_surj : Surjective g
s_closed : IsClosed s
f : (ℕ → ℕ) → ↑s
f_surj : Surjective f
f_cont : Continuous f
⊢ ∃ f, Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f ∧ Surjective f
Module: Mathlib.MeasureTheory.Measure.OpenPos

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst✝² : μ.IsOpenPosMeasure
F : Set X
inst✝¹ : OpensMeasurableSpace X
inst✝ : IsFiniteMeasure μ
hF : IsClosed[inst✝³] F
⊢ F =ᵐ[μ] univ ↔ F = univ

Tactic:
hF.ae_eq_univ_iff_eq

Goal state after:
X : Type u_1
inst✝³ : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst✝² : μ.IsOpenPosMeasure
F : Set X
inst✝¹ : OpensMeasurableSpace X
inst✝ : IsFiniteMeasure μ
hF : IsClosed[inst✝³] F
⊢ F = univ ↔ F = univ
Module: Mathlib.MeasureTheory.Measure.OpenPos

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst✝² : μ.IsOpenPosMeasure
F : Set X
inst✝¹ : OpensMeasurableSpace X
inst✝ : IsFiniteMeasure μ
hF : IsClosed[inst✝³] F
⊢ μ F = μ univ ↔ F = univ

Tactic:
rw [← ae_eq_univ_iff_measure_eq hF.measurableSet.nullMeasurableSet, hF.ae_eq_univ_iff_eq]

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

Goal state before:
pp: 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
⊢ 0 < 0 + ε

Tactic:
zero_add,

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
⊢ 0 < ε
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: case refine_1
α : Type u_2
β : Type u_3
inst✝ : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure β
pa qa : Set α → Prop
pb qb : Set β → Prop
H : μ.InnerRegularWRT pb qb
f : α → β
hf : MeasurableEmbedding f
hAB : ∀ (U : Set α), qa U → qb (f '' U)
hAB' : ∀ K ⊆ range f, pb K → pa (f ⁻¹' K)
U : Set α
hU : qa U
r : ℝ≥0∞
hr : r < μ (f '' U)
K : Set β
hKU : K ⊆ f '' U
hK : pb K
hμU : r < μ K
hKrange : K ⊆ range f
⊢ f ⁻¹' K ⊆ f ⁻¹' f '' U

Tactic:
exact preimage_mono hKU

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
H : μ.InnerRegularWRT p q
c : ℝ≥0∞
⊢ (c • μ).InnerRegularWRT p q

Tactic:
intro U hU r hr
  rw [smul_apply, H.measure_eq_iSup hU, smul_eq_mul] at hr
  simpa only [ENNReal.mul_iSup, lt_iSup_iff, exists_prop] using! hr

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

Goal state before:
pp: α : Type u_1
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : R1Space α
inst✝ : μ.OuterRegular
k : Set α
hk : IsCompact k
⊢ μ (closure[inst✝²] k) ≤ μ k

Tactic:
simp only [measure_eq_iInf_isOpen k, le_iInf_iff]

Goal state after:
α : Type u_1
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : R1Space α
inst✝ : μ.OuterRegular
k : Set α
hk : IsCompact k
⊢ ∀ (i : Set α), k ⊆ i → IsOpen[inst✝²] i → μ (closure[inst✝²] k) ≤ μ i
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g ν
⊢ ∫⁻ (x : α), ∫⁻ (y : β), f (x, y).1 * g (x, y).2 ∂ν ∂μ = (∫⁻ (x : α), f x ∂μ) * ∫⁻ (y : β), g y ∂ν

Tactic:
simp [lintegral_lintegral_mul hf hg]

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

Goal state before:
pp: case pos
X : Type u_6
E : Type u_7
ι : Type u_8
inst✝⁸ : MeasurableSpace X
inst✝⁷ : CommMonoid E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : PseudoMetrizableSpace E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : MeasurableMul₂ E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEMeasurable (f i) μ
hm : Multipliable (fun i ↦ f i) L
h✝¹ : L.HasSupport ∧ ((mulSupport fun i ↦ f i) ∩ L.support).Finite
h✝ : HasFiniteMulSupport ((L.support.mulIndicator fun i ↦ f i) ∘ PLift.down)
⊢ AEMeasurable (∏ i ∈ Finite.toFinset h✝, L.support.mulIndicator (fun i ↦ f i) i.down) μ

Tactic:
refine Finset.aemeasurable_prod _ (fun _ _ ↦ ?_)
    rw [Set.mulIndicator]
    split_ifs <;> fun_prop

Goal state after: