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

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
M : α → α
hM : ∀ x ∈ s, x < M x
y : α → α
hy : ∀ x ∈ s, y x ∈ Ioi x
h'y : ∀ x ∈ s, Ioo x (y x) ⊆ s
⊢ (s \ interior s).Countable

Tactic:
have B : Set.PairwiseDisjoint (s \ interior s) fun x => Ioo x (y x) := by
    intro x hx x' hx' hxx'
    rcases lt_or_gt_of_ne hxx' with (h' | h')
    · refine disjoint_left.2 fun z hz h'z => ?_
      have : x' ∈ interior s :=
        mem_interior.2 ⟨Ioo x (y x), h'y _ hx.1, isOpen_Ioo, ⟨h', h'z.1.trans hz.2⟩⟩
      exact False.elim (hx'.2 this)
    · refine disjoint_left.2 fun z hz h'z => ?_
      have : x ∈ interior s :=
        mem_interior.2 ⟨Ioo x' (y x'), h'y _ hx'.1, isOpen_Ioo, ⟨h', hz.1.trans h'z.2⟩⟩
      exact False.elim (hx.2 this)

Goal state after:
α : Type u_1
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
M : α → α
hM : ∀ x ∈ s, x < M x
y : α → α
hy : ∀ x ∈ s, y x ∈ Ioi x
h'y : ∀ x ∈ s, Ioo x (y x) ⊆ s
B : (s \ interior s).PairwiseDisjoint fun x ↦ Ioo x (y x)
⊢ (s \ interior s).Countable
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_5
μ : Measure δ
s : Set ι
f : ι → δ → α
hs : s.Countable
hf : ∀ i ∈ s, AEMeasurable (f i) μ
g : ι → δ → α := fun i ↦ if hi : i ∈ s then mk (f i) ⋯ else fun _b ↦ sSup ∅
this : ∀ i ∈ s, Measurable (g i)
i : ι
hi : i ∈ s
⊢ ∀ᵐ (b : δ) ∂μ, f i b = g i b

Tactic:
simpa [g, hi] using! (hf i hi).ae_eq_mk

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

Goal state before:
pp: case pos
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : AddZeroClass γ
motive : (α →ₛ γ) → Prop
const :
  ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), motive (piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ⇑f) (support ⇑g) → motive f → motive g → motive (f + g)
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ), range ⇑f \ {0} = ↑s → motive f
f : α →ₛ γ
h : range ⇑f \ {0} = ↑(insert x s)
mx : MeasurableSet (⇑f ⁻¹' {x})
g : α →ₛ γ := piecewise (⇑f ⁻¹' {x}) mx 0 f
Pg : motive g
y : α
hy : y ∈ ⇑f ⁻¹' {x}
⊢ f y = (g + piecewise (⇑f ⁻¹' {x}) mx (SimpleFunc.const α x) (SimpleFunc.const α 0)) y

pp: case neg
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : AddZeroClass γ
motive : (α →ₛ γ) → Prop
const :
  ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), motive (piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ⇑f) (support ⇑g) → motive f → motive g → motive (f + g)
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ), range ⇑f \ {0} = ↑s → motive f
f : α →ₛ γ
h : range ⇑f \ {0} = ↑(insert x s)
mx : MeasurableSet (⇑f ⁻¹' {x})
g : α →ₛ γ := piecewise (⇑f ⁻¹' {x}) mx 0 f
Pg : motive g
y : α
hy : y ∉ ⇑f ⁻¹' {x}
⊢ f y = (g + piecewise (⇑f ⁻¹' {x}) mx (SimpleFunc.const α x) (SimpleFunc.const α 0)) y

Tactic:
· simpa [g, hy]

Goal state after:
case neg
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : AddZeroClass γ
motive : (α →ₛ γ) → Prop
const :
  ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), motive (piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ⇑f) (support ⇑g) → motive f → motive g → motive (f + g)
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ), range ⇑f \ {0} = ↑s → motive f
f : α →ₛ γ
h : range ⇑f \ {0} = ↑(insert x s)
mx : MeasurableSet (⇑f ⁻¹' {x})
g : α →ₛ γ := piecewise (⇑f ⁻¹' {x}) mx 0 f
Pg : motive g
y : α
hy : y ∉ ⇑f ⁻¹' {x}
⊢ f y = (g + piecewise (⇑f ⁻¹' {x}) mx (SimpleFunc.const α x) (SimpleFunc.const α 0)) y
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : PseudoMetrizableSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
ι : Type u_3
inst✝¹ : Nonempty ι
μ : Measure α
f : ι → α → β
L : Filter ι
inst✝ : L.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n ↦ f n x) L (𝓝 l)
inhabited_h : Inhabited ι
hL : L.NeBot
f_lim : α → β := fun x ↦ if h : ∃ l, Tendsto (fun n ↦ f n x) L (𝓝 l) then h.choose else ⋯.some
⊢ ∃ f_lim, Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) L (𝓝 (f_lim x))

Tactic:
have h_ae_tendsto_f_lim : ∀ᵐ x ∂μ, Tendsto (fun n ↦ f n x) L (𝓝 (f_lim x)) := by
    filter_upwards [h_ae_tendsto] with x hx
    simpa [f_lim, hx] using hx.choose_spec

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : PseudoMetrizableSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
ι : Type u_3
inst✝¹ : Nonempty ι
μ : Measure α
f : ι → α → β
L : Filter ι
inst✝ : L.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n ↦ f n x) L (𝓝 l)
inhabited_h : Inhabited ι
hL : L.NeBot
f_lim : α → β := fun x ↦ if h : ∃ l, Tendsto (fun n ↦ f n x) L (𝓝 l) then h.choose else ⋯.some
h_ae_tendsto_f_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) L (𝓝 (f_lim x))
⊢ ∃ f_lim, Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) L (𝓝 (f_lim x))
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: case pos
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : Nonempty γ
P : (α →ₛ γ) → Prop
const : ∀ (c : γ), P (SimpleFunc.const α c)
pcw : ∀ ⦃f g : α →ₛ γ⦄ {s : Set α} (hs : MeasurableSet s), P f → P g → P (piecewise s hs f g)
c : γ := Classical.ofNonempty
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ), range ⇑f \ {c} = ↑s → P f
f : α →ₛ γ
h : range ⇑f \ {c} = ↑(insert x s)
mx : MeasurableSet (⇑f ⁻¹' {x})
g : α →ₛ γ := piecewise (⇑f ⁻¹' {x}) mx (SimpleFunc.const α c) f
Pg : P g
y : α
hy : y ∈ ⇑f ⁻¹' {x}
⊢ f y = (piecewise (⇑f ⁻¹' {x})ᶜ ⋯ g (SimpleFunc.const α x)) y

pp: case neg
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : Nonempty γ
P : (α →ₛ γ) → Prop
const : ∀ (c : γ), P (SimpleFunc.const α c)
pcw : ∀ ⦃f g : α →ₛ γ⦄ {s : Set α} (hs : MeasurableSet s), P f → P g → P (piecewise s hs f g)
c : γ := Classical.ofNonempty
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ), range ⇑f \ {c} = ↑s → P f
f : α →ₛ γ
h : range ⇑f \ {c} = ↑(insert x s)
mx : MeasurableSet (⇑f ⁻¹' {x})
g : α →ₛ γ := piecewise (⇑f ⁻¹' {x}) mx (SimpleFunc.const α c) f
Pg : P g
y : α
hy : y ∉ ⇑f ⁻¹' {x}
⊢ f y = (piecewise (⇑f ⁻¹' {x})ᶜ ⋯ g (SimpleFunc.const α x)) y

Tactic:
· simpa [g, hy]

Goal state after:
case neg
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : Nonempty γ
P : (α →ₛ γ) → Prop
const : ∀ (c : γ), P (SimpleFunc.const α c)
pcw : ∀ ⦃f g : α →ₛ γ⦄ {s : Set α} (hs : MeasurableSet s), P f → P g → P (piecewise s hs f g)
c : γ := Classical.ofNonempty
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ), range ⇑f \ {c} = ↑s → P f
f : α →ₛ γ
h : range ⇑f \ {c} = ↑(insert x s)
mx : MeasurableSet (⇑f ⁻¹' {x})
g : α →ₛ γ := piecewise (⇑f ⁻¹' {x}) mx (SimpleFunc.const α c) f
Pg : P g
y : α
hy : y ∉ ⇑f ⁻¹' {x}
⊢ f y = (piecewise (⇑f ⁻¹' {x})ᶜ ⋯ g (SimpleFunc.const α x)) y
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✝³ : TopologicalSpace α
inst✝² : PseudoMetrizableSpace α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, inst✝³] f
h'f : HasCompactSupport f
this : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
g : ℕ → SimpleFunc (X × Y) α
hg : ∀ (n : ℕ) (x : X × Y), dist (f x) ((g n) x) < u n
x : X × Y
⊢ Tendsto (fun b ↦ dist ((g b) x) (f x)) atTop (𝓝 0)

Tactic:
apply squeeze_zero (fun n ↦ dist_nonneg) (fun n ↦ ?_) u_lim

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✝³ : TopologicalSpace α
inst✝² : PseudoMetrizableSpace α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, inst✝³] f
h'f : HasCompactSupport f
this : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
g : ℕ → SimpleFunc (X × Y) α
hg : ∀ (n : ℕ) (x : X × Y), dist (f x) ((g n) x) < u n
x : X × Y
n : ℕ
⊢ dist ((g n) x) (f x) ≤ u n
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
h's : EqOn f 0 s
⊢ ∫⁻ (x : α) in s, f x ∂μ = 0

Tactic:
simp [setLIntegral_congr_fun hs h's]

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

Goal state before:
pp: case intro.inr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun x1 x2 ↦ x1 ≤ x2) f
val✝ : Encodable β
h✝ : Nonempty β
inhabited_h : Inhabited β
⊢ ∫⁻ (a : α), ⨆ b, f b a ∂μ = ⨆ b, ∫⁻ (a : α), f b a ∂μ

Tactic:
have : ∀ a, ⨆ b, f b a = ⨆ n, f (h_directed.sequence f n) a := by
    intro a
    refine le_antisymm (iSup_le fun b => ?_) (iSup_le fun n => le_iSup (fun n => f n a) _)
    exact le_iSup_of_le (encode b + 1) (h_directed.le_sequence b a)

Goal state after:
case intro.inr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun x1 x2 ↦ x1 ≤ x2) f
val✝ : Encodable β
h✝ : Nonempty β
inhabited_h : Inhabited β
this : ∀ (a : α), ⨆ b, f b a = ⨆ n, f (Directed.sequence f h_directed n) a
⊢ ∫⁻ (a : α), ⨆ b, f b a ∂μ = ⨆ b, ∫⁻ (a : α), f b a ∂μ
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:
by
  borelize β
  exact measurableSet_mulSupport hf.measurable

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
g : α → γ
hf : StronglyMeasurable f
hg : StronglyMeasurable g
x : α
⊢ Tendsto (fun n ↦ ((fun n ↦ (hf.approx n).pair (hg.approx n)) n) x) atTop (𝓝 ((fun x ↦ (f x, g x)) x))

Tactic:
nhds_prod_eq

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
g : α → γ
hf : StronglyMeasurable f
hg : StronglyMeasurable g
x : α
⊢ Tendsto (fun n ↦ ((fun n ↦ (hf.approx n).pair (hg.approx n)) n) x) atTop (𝓝 (f x) ×ˢ 𝓝 (g x))
Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
F : ℕ → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ (n : ℕ), AEMeasurable (F n) μ
h_bound : ∀ (n : ℕ), F n ≤ᵐ[μ] bound
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
this : ∀ (n : ℕ), ∫⁻ (a : α), F n a ∂μ = ∫⁻ (a : α), AEMeasurable.mk (F n) ⋯ a ∂μ
⊢ Tendsto (fun n ↦ ∫⁻ (a : α), AEMeasurable.mk (F n) ⋯ a ∂μ) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))

Tactic:
apply
    tendsto_lintegral_of_dominated_convergence bound (fun n => (hF_meas n).measurable_mk) _ h_fin

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
F : ℕ → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ (n : ℕ), AEMeasurable (F n) μ
h_bound : ∀ (n : ℕ), F n ≤ᵐ[μ] bound
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
this : ∀ (n : ℕ), ∫⁻ (a : α), F n a ∂μ = ∫⁻ (a : α), AEMeasurable.mk (F n) ⋯ a ∂μ
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ AEMeasurable.mk (F n) ⋯ a) atTop (𝓝 (f a))

α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
F : ℕ → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ (n : ℕ), AEMeasurable (F n) μ
h_bound : ∀ (n : ℕ), F n ≤ᵐ[μ] bound
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
this : ∀ (n : ℕ), ∫⁻ (a : α), F n a ∂μ = ∫⁻ (a : α), AEMeasurable.mk (F n) ⋯ a ∂μ
⊢ ∀ (n : ℕ), AEMeasurable.mk (F n) ⋯ ≤ᵐ[μ] bound
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : IsEmbedding g
this✝⁴ : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this✝³ : MeasurableSpace β := borel β
this✝² : BorelSpace β
this✝¹ : MeasurableSpace γ := borel γ
this✝ : BorelSpace γ
H : StronglyMeasurable fun x ↦ g (f x)
this : IsSeparable (g ⁻¹' range (g ∘ f))
⊢ IsSeparable (range f)

Tactic:
range_comp,

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : IsEmbedding g
this✝⁴ : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this✝³ : MeasurableSpace β := borel β
this✝² : BorelSpace β
this✝¹ : MeasurableSpace γ := borel γ
this✝ : BorelSpace γ
H : StronglyMeasurable fun x ↦ g (f x)
this : IsSeparable (g ⁻¹' g '' range f)
⊢ IsSeparable (range f)
Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

Goal state before:
pp: 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

Tactic:
have h_lt_top : ⨆ (s) (_ : MeasurableSet s) (_ : SigmaFinite (μ.restrict s)), ν s < ∞ := by
      refine (?_ : ⨆ (s) (_ : MeasurableSet s)
        (_ : SigmaFinite (μ.restrict s)), ν s ≤ ν Set.univ).trans_lt (measure_lt_top _ _)
      refine iSup_le (fun s ↦ ?_)
      exact iSup_le (fun _ ↦ iSup_le (fun _ ↦ measure_mono (Set.subset_univ 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
h_lt_top : ⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s < ∞
⊢ ∃ t,
    MeasurableSet t ∧
      SigmaFinite (μ.restrict t) ∧
        (⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s) - 1 / ↑n ≤ ν t
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

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

Tactic:
apply StronglyMeasurable.dite (f := fun x ↦ f x) (g := fun x ↦ f x) ?_ ?_ h's

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

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : SFinite ν
hμν : μ ≪ ν
s : Set α
a✝ : MeasurableSet s
⊢ μ (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) = ∞ * (ν.restrict (μ.sigmaFiniteSetWRT ν)ᶜ) s

Tactic:
Measure.restrict_apply' measurableSet_sigmaFiniteSetWRT.compl

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : SFinite ν
hμν : μ ≪ ν
s : Set α
a✝ : MeasurableSet s
⊢ μ (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) = ∞ * ν (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ)
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 β
ε : ℝ
εpos : ε > 0
t : Finset ι
ht : ∀ (b : Finset ι), t ⊆ b → ∑' (a : { x // x ∉ b }), u ↑a < ε
N : Set ι
hN : N ∈ cofinite
HN : ∀ y ∈ N, ∀ x ∈ s, ‖f y x‖ ≤ u y
n : Finset ι
hn : Finite.toFinset hN ∪ t ⊆ n
x : β
hx : x ∈ s
A : Summable fun n ↦ ‖f n x‖
⊢ ‖∑' (x_1 : { x // x ∉ n }), f (↑x_1) x‖ < ε

Tactic:
apply lt_of_le_of_lt _ (ht n (Finset.union_subset_right hn))

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 β
ε : ℝ
εpos : ε > 0
t : Finset ι
ht : ∀ (b : Finset ι), t ⊆ b → ∑' (a : { x // x ∉ b }), u ↑a < ε
N : Set ι
hN : N ∈ cofinite
HN : ∀ y ∈ N, ∀ x ∈ s, ‖f y x‖ ≤ u y
n : Finset ι
hn : Finite.toFinset hN ∪ t ⊆ n
x : β
hx : x ∈ s
A : Summable fun n ↦ ‖f n x‖
⊢ ‖∑' (x_1 : { x // x ∉ n }), f (↑x_1) x‖ ≤ ∑' (a : { x // x ∉ n }), u ↑a
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:
by
  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.Dynamics.Ergodic.MeasurePreserving

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
hf : MeasurePreserving f μa μb
h₂ : MeasurableEmbedding f
s : Set β
⊢ map f (μa.restrict (f ⁻¹' s)) = (map f μa).restrict s

Tactic:
h₂.restrict_map

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
hf : MeasurePreserving f μa μb
h₂ : MeasurableEmbedding f
s : Set β
⊢ map f (μa.restrict (f ⁻¹' s)) = map f (μa.restrict (f ⁻¹' s))
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
β : Type u_3
inst✝ : TopologicalSpace β
s : Set α
hs : AnalyticSet s
f : α → β
hf : ContinuousOn f s
γ : Type
γtop : TopologicalSpace γ
γpolish : PolishSpace γ
g : γ → α
g_cont : Continuous[γtop, inst✝¹] g
gs : range g = s
⊢ f '' s = range (f ∘ g)

Tactic:
range_comp,

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
β : Type u_3
inst✝ : TopologicalSpace β
s : Set α
hs : AnalyticSet s
f : α → β
hf : ContinuousOn f s
γ : Type
γtop : TopologicalSpace γ
γpolish : PolishSpace γ
g : γ → α
g_cont : Continuous[γtop, inst✝¹] g
gs : range g = s
⊢ f '' s = f '' range g
Module: Mathlib.MeasureTheory.Measure.MutuallySingular

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
h : μ ≪ ν₁ + ν₂
h_ms : μ ⟂ₘ ν₂
s : Set α
hs : MeasurableSet s
hs_zero : ν₁ s = 0
t : Set α := h_ms.nullSet
ht : MeasurableSet t
htμ : μ t = 0
htν₂ : ν₂ tᶜ = 0
this : μ s = μ (s ∩ tᶜ)
⊢ (ν₁ + ν₂) (s ∩ tᶜ) = 0

Tactic:
simp only [Measure.coe_add, Pi.add_apply, add_eq_zero]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
h : μ ≪ ν₁ + ν₂
h_ms : μ ⟂ₘ ν₂
s : Set α
hs : MeasurableSet s
hs_zero : ν₁ s = 0
t : Set α := h_ms.nullSet
ht : MeasurableSet t
htμ : μ t = 0
htν₂ : ν₂ tᶜ = 0
this : μ s = μ (s ∩ tᶜ)
⊢ ν₁ (s ∩ tᶜ) = 0 ∧ ν₂ (s ∩ tᶜ) = 0
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
s : Set α
inst✝ : IsProbabilityMeasure μ
p : α → Prop
f✝ : β → α
f : β ≃ᵐ α
⊢ IsProbabilityMeasure (Measure.comap (⇑f) μ)

Tactic:
rw [← MeasurableEquiv.map_symm]

Goal state after:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
s : Set α
inst✝ : IsProbabilityMeasure μ
p : α → Prop
f✝ : β → α
f : β ≃ᵐ α
⊢ IsProbabilityMeasure (Measure.map (⇑f.symm) μ)
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case refine_2
ι : Type u_2
inst✝¹ : Countable ι
α : Type u_3
inst✝ : MeasurableSpace α
s t : ι → Set α
u : ι → ι → Set α
hsu : ∀ (m n : ι), s m ⊆ u m n
htu : ∀ (m n : ι), Disjoint (t n) (u m n)
hu : ∀ (m n : ι), MeasurableSet (u m n)
⊢ Disjoint (⋃ m, t m) (⋃ m, ⋂ n, u m n)

Tactic:
disjoint_iUnion_left,

Goal state after:
case refine_2
ι : Type u_2
inst✝¹ : Countable ι
α : Type u_3
inst✝ : MeasurableSpace α
s t : ι → Set α
u : ι → ι → Set α
hsu : ∀ (m n : ι), s m ⊆ u m n
htu : ∀ (m n : ι), Disjoint (t n) (u m n)
hu : ∀ (m n : ι), MeasurableSet (u m n)
⊢ ∀ (i : ι), Disjoint (t i) (⋃ m, ⋂ n, u m n)
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
s : Set α
hs : s ∈ ae m.join
⊢ s ∈ (ae m).bind ae

Tactic:
rcases exists_measurable_superset_of_null hs with ⟨t, hst, htm, ht⟩

Goal state after:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
s : Set α
hs : s ∈ ae m.join
t : Set α
hst : sᶜ ⊆ t
htm : MeasurableSet t
ht : m.join t = 0
⊢ s ∈ (ae m).bind ae
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ✝ : Measure α
f : α → ℝ≥0∞
μ : Measure α
inst✝ : SFinite μ
h : IsFiniteMeasure μ
g : ℕ → α → ℝ≥0∞
hgm : ∀ (n : ℕ), Measurable (g n)
hgf : ∀ (n : ℕ), g n ≤ f
hgle : ∀ (n : ℕ), g n ≤ ↑n
hgint : ∀ (n : ℕ), ∫⁻ (a : α), min (f a) ↑n ∂μ = ∫⁻ (a : α), g n a ∂μ
⊢ ∃ g, Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ

Tactic:
set φ : α → ℝ≥0∞ := fun x ↦ ⨆ n, g n x

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ✝ : Measure α
f : α → ℝ≥0∞
μ : Measure α
inst✝ : SFinite μ
h : IsFiniteMeasure μ
g : ℕ → α → ℝ≥0∞
hgm : ∀ (n : ℕ), Measurable (g n)
hgf : ∀ (n : ℕ), g n ≤ f
hgle : ∀ (n : ℕ), g n ≤ ↑n
hgint : ∀ (n : ℕ), ∫⁻ (a : α), min (f a) ↑n ∂μ = ∫⁻ (a : α), g n a ∂μ
φ : α → ℝ≥0∞ := fun x ↦ ⨆ n, g n x
⊢ ∃ g, Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
f : α → Measure β
s : Set β
hs : MeasurableSet s
hf : AEMeasurable f m
⊢ (m.bind f) s = ∫⁻ (a : α), (f a) s ∂m

Tactic:
by
  rw [bind, join_apply hs, lintegral_map' (measurable_coe hs).aemeasurable hf]

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

Goal state before:
pp: ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → PseudoMetricSpace (F i)
x y : (i : ι) → F i
⊢ Summable fun i ↦ min (2⁻¹ ^ encode i) (dist (x i) (y i))

Tactic:
refine .of_nonneg_of_le (fun i => ?_) (fun i => min_le_left _ _) <| by
    simpa [one_div] using summable_geometric_two_encode
  exact le_min (by positivity) dist_nonneg

Goal state after: