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

Goal state before:
pp: x : Set ℝ
⊢ x ∈ ⋃ a, {Iio ↑a} ↔ x ∈ Iio '' Rat.cast '' univ

Tactic:
simp only [iUnion_singleton_eq_range, mem_range, image_univ, mem_image, exists_exists_eq_and]

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: x : Set ℝ
⊢ x ∈ ⋃ a, {Ioi ↑a} ↔ x ∈ Ioi '' Rat.cast '' univ

Tactic:
simp only [iUnion_singleton_eq_range, mem_range, image_univ, mem_image, exists_exists_eq_and]

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: x : Set ℝ
⊢ x ∈ ⋃ a, {Iic ↑a} ↔ x ∈ Iic '' Rat.cast '' univ

Tactic:
simp only [iUnion_singleton_eq_range, mem_range, image_univ, mem_image, exists_exists_eq_and]

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: x : Set ℝ
⊢ x ∈ ⋃ a, {Ici ↑a} ↔ x ∈ Ici '' Rat.cast '' univ

Tactic:
simp only [iUnion_singleton_eq_range, mem_range, image_univ, mem_image, exists_exists_eq_and]

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: μ : Measure ℝ
inst✝ : IsFiniteMeasureOnCompacts μ
b : ℝ
⊢ ∀ s ∈ 𝓝 (μ {b}), μ (Icc (b - 0) (b + 0)) ∈ s

Tactic:
intro s hs

Goal state after:
μ : Measure ℝ
inst✝ : IsFiniteMeasureOnCompacts μ
b : ℝ
s : Set ℝ≥0∞
hs : s ∈ 𝓝 (μ {b})
⊢ μ (Icc (b - 0) (b + 0)) ∈ s
Module: Mathlib.MeasureTheory.Function.SimpleFuncDense

Goal state before:
pp: case hmono
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 < ε
K : Set (X × Y)
hK : IsCompact K
t t' : Set (X × Y)
htt' : t ⊆ t'
⊢ (∃ g s, MeasurableSet s ∧ t' ⊆ s ∧ ∀ x ∈ s, dist (f x) (g x) < ε) →
    ∃ g s, MeasurableSet s ∧ t ⊆ s ∧ ∀ x ∈ s, dist (f x) (g x) < ε

Tactic:
⟨g, s, s_meas, ts, hg⟩

Goal state after:
case hmono
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 < ε
K : Set (X × Y)
hK : IsCompact K
t t' : Set (X × Y)
htt' : t ⊆ t'
g : SimpleFunc (X × Y) α
s : Set (X × Y)
s_meas : MeasurableSet s
ts : t' ⊆ s
hg : ∀ x ∈ s, dist (f x) (g x) < ε
⊢ ∃ g s, MeasurableSet s ∧ t ⊆ s ∧ ∀ x ∈ s, dist (f x) (g x) < ε
Module: Mathlib.MeasureTheory.Function.SimpleFuncDense

Goal state before:
pp: case hunion
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 < ε
K : Set (X × Y)
hK : IsCompact K
t t' : Set (X × Y)
⊢ (∃ g s, MeasurableSet s ∧ t ⊆ s ∧ ∀ x ∈ s, dist (f x) (g x) < ε) →
    (∃ g s, MeasurableSet s ∧ t' ⊆ s ∧ ∀ x ∈ s, dist (f x) (g x) < ε) →
      ∃ g s, MeasurableSet s ∧ t ∪ t' ⊆ s ∧ ∀ x ∈ s, dist (f x) (g x) < ε

Tactic:
⟨g, s, s_meas, ts, hg⟩

Goal state after:
case hunion
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 < ε
K : Set (X × Y)
hK : IsCompact K
t t' : Set (X × Y)
g : SimpleFunc (X × Y) α
s : Set (X × Y)
s_meas : MeasurableSet s
ts : t ⊆ s
hg : ∀ x ∈ s, dist (f x) (g x) < ε
⊢ (∃ g s, MeasurableSet s ∧ t' ⊆ s ∧ ∀ x ∈ s, dist (f x) (g x) < ε) →
    ∃ g s, MeasurableSet s ∧ t ∪ t' ⊆ s ∧ ∀ x ∈ s, dist (f x) (g x) < ε
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
⊢ (AEMeasurable f μ ∧ ∃ t, IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, f x ∈ t) → AEStronglyMeasurable f μ

Tactic:
rintro ⟨H, ⟨t, t_sep, ht⟩⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
H : AEMeasurable f μ
t : Set β
t_sep : IsSeparable t
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
⊢ AEStronglyMeasurable f μ
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_5
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n ↦ (hf.approx n) x) atTop (𝓝 (f x))
hfx0 : ‖f x‖ = 0
⊢ Tendsto (fun n ↦ min 1 (c / ‖(hf.approx n) x‖) • (hf.approx n) x) atTop (𝓝 (f x))

pp: case neg
α : Type u_1
β : Type u_5
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n ↦ (hf.approx n) x) atTop (𝓝 (f x))
hfx0 : ¬‖f x‖ = 0
⊢ Tendsto (fun n ↦ min 1 (c / ‖(hf.approx n) x‖) • (hf.approx n) x) atTop (𝓝 (f x))

Tactic:
· rw [norm_eq_zero] at hfx0
    rw [hfx0] at h_tendsto ⊢
    have h_tendsto_norm : Tendsto (fun n => ‖hf.approx n x‖) atTop (𝓝 0) := by
      convert! h_tendsto.norm
      rw [norm_zero]
    refine squeeze_zero_norm (fun n => ?_) h_tendsto_norm
    calc
      ‖min 1 (c / ‖hf.approx n x‖) • hf.approx n x‖ =
          ‖min 1 (c / ‖hf.approx n x‖)‖ * ‖hf.approx n x‖ :=
        norm_smul _ _
      _ ≤ ‖(1 : ℝ)‖ * ‖hf.approx n x‖ := by
        gcongr
        rw [norm_one, Real.norm_of_nonneg]
        · exact min_le_left _ _
        · exact le_min zero_le_one (div_nonneg ((norm_nonneg _).trans hfx) (norm_nonneg _))
      _ = ‖hf.approx n x‖ := by rw [norm_one, one_mul]

Goal state after:
case neg
α : Type u_1
β : Type u_5
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n ↦ (hf.approx n) x) atTop (𝓝 (f x))
hfx0 : ¬‖f x‖ = 0
⊢ Tendsto (fun n ↦ min 1 (c / ‖(hf.approx n) x‖) • (hf.approx n) x) atTop (𝓝 (f x))
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
s : Set α
hs : ∀ x ∈ s, 1 ≤ f x
⊢ μ s ≤ ∫⁻ (a : α), f a ∂μ

Tactic:
by
  apply le_trans _ (mul_meas_ge_le_lintegral₀ hf 1)
  rw [one_mul]
  exact measure_mono hs

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

Goal state before:
pp: α : 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 = ⨆ n, f (Directed.sequence f h_directed n) a

Tactic:
refine le_antisymm (iSup_le fun b => ?_) (iSup_le fun n => le_iSup (fun n => f n a) _)

Goal state after:
α : 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 ≤ ⨆ n, f (Directed.sequence f h_directed n) a
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: case pos
α : 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
x : α
hxt : x ∈ t
h : ∀ s ∈ 𝓝 (f x), ∃ a, ∀ (b : ℕ), a ≤ b → (f_approx b) x ∈ s
n₁ : ℕ
hn₁ : ∀ (m_1 : ℕ), n₁ ≤ m_1 → (fs m_1) x = (f_approx m_1) x
⊢ ∀ s ∈ 𝓝 (f x), ∃ a, ∀ (b : ℕ), a ≤ b → (fs b) x ∈ s

Tactic:
intro s hs

Goal state after:
case pos
α : 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
x : α
hxt : x ∈ t
h : ∀ s ∈ 𝓝 (f x), ∃ a, ∀ (b : ℕ), a ≤ b → (f_approx b) x ∈ s
n₁ : ℕ
hn₁ : ∀ (m_1 : ℕ), n₁ ≤ m_1 → (fs m_1) x = (f_approx m_1) x
s : Set β
hs : s ∈ 𝓝 (f x)
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → (fs b) x ∈ s
Module: Mathlib.Topology.Perfect

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T1Space α
h : Perfect (closure[inst✝¹] C)
⊢ Preperfect C

Tactic:
intro x xC

Goal state after:
case mpr
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T1Space α
h : Perfect (closure[inst✝¹] C)
x : α
xC : x ∈ C
⊢ AccPt x (𝓟 C)
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)
⊢ U ∩ C ⊆ C

Tactic:
exact inter_subset_right

Goal state after:
Module: Mathlib.Topology.Perfect

Goal state before:
pp: case h.right.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)
⊢ V ∩ C ⊆ C

Tactic:
exact inter_subset_right

Goal state after:
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: x : ↑I
⊢ Subtype.val ⁻¹' Iic ↑x = Icc 0 x

Tactic:
by
  rw [preimage_subtype_val_Iic]
  exact Icc_bot.symm

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝ : MetricSpace α
s : Opens α
x✝ : s.CompleteCopy
⊢ dist x✝ x✝ = 0

Tactic:
simp only [dist_eq, dist_self, one_div, sub_self, abs_zero, add_zero]

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
this✝ : x ∈ eball x (ε / 2)
this : Perfect (closure (eball x (ε / 2) ∩ C)) ∧ (closure (eball x (ε / 2) ∩ C)).Nonempty
⊢ eball x (ε / 2) ∩ C ⊆ C

Tactic:
apply inter_subset_right

Goal state after:
Module: Mathlib.Dynamics.Ergodic.MeasurePreserving

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μa : Measure α
μb : Measure β
μc : Measure γ
g : β → γ
f : α → β
hg : MeasurePreserving g μb μc
hf : MeasurePreserving f μa μb
⊢ map (g ∘ f) μa = μc

Tactic:
rw [← map_map hg.1 hf.1, hf.2, hg.2]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
hμs : μ s = 0
hμs_compl : μ sᶜ = 0
this : μ univ = 0
⊢ μ = 0

Tactic:
measure_univ_eq_zero

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
hμs : μ s = 0
hμs_compl : μ sᶜ = 0
this : μ = 0
⊢ μ = 0
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
inst✝ : IsProbabilityMeasure μ
f : α → β
hf : AEMeasurable f μ
⊢ (map f μ) univ = 1

Tactic:
simp [map_apply_of_aemeasurable, hf]

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s : Set α
h : NeZero μ
⊢ IsZeroOrProbabilityMeasure ((μ univ)⁻¹ • μ)

Tactic:
rcases eq_top_or_lt_top (μ univ) with h | h

Goal state after:
case inr.inl
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s : Set α
h✝ : NeZero μ
h : μ univ = ∞
⊢ IsZeroOrProbabilityMeasure ((μ univ)⁻¹ • μ)

case inr.inr
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s : Set α
h✝ : NeZero μ
h : μ univ < ∞
⊢ IsZeroOrProbabilityMeasure ((μ univ)⁻¹ • μ)
Module: Mathlib.MeasureTheory.Measure.MutuallySingular

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
n : ℕ
x✝ : Set α
⊢ (1 / 2) ^ n = 2 * ↑((1 / 2) ^ (n + 1))

Tactic:
conv =>
      -- this tweak is needed due to the known issue of `norm_cast` with numeric fractions
      enter [1, 1]
      equals ((1 : ℝ≥0) / (2 : ℝ≥0)) => rfl

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
n : ℕ
x✝ : Set α
⊢ (↑1 / ↑2) ^ n = 2 * ↑((1 / 2) ^ (n + 1))
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
μ : Measure α
measurableAtoms : Set (Set α) := measurableAtom '' univ
h_nonempty : ∀ (s : ↑measurableAtoms), (↑s).Nonempty
points : ↑measurableAtoms → α := fun s ↦ ⋯.some
x y : α
s : Set α
hyx : ¬y = points ⟨measurableAtom x, ⋯⟩
hyx' : y ∈ measurableAtom x
h1 : measurableAtom y = measurableAtom x
z : α
left✝ : z ∈ univ
hz : measurableAtom z = s
h_points_mem : points ⟨s, ⋯⟩ ∈ s
hsy : points ⟨s, ⋯⟩ = y
⊢ measurableAtom y = s

Tactic:
← hz,

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
μ : Measure α
measurableAtoms : Set (Set α) := measurableAtom '' univ
h_nonempty : ∀ (s : ↑measurableAtoms), (↑s).Nonempty
points : ↑measurableAtoms → α := fun s ↦ ⋯.some
x y : α
s : Set α
hyx : ¬y = points ⟨measurableAtom x, ⋯⟩
hyx' : y ∈ measurableAtom x
h1 : measurableAtom y = measurableAtom x
z : α
left✝ : z ∈ univ
hz : measurableAtom z = s
h_points_mem : points ⟨s, ⋯⟩ ∈ s
hsy : points ⟨s, ⋯⟩ = y
⊢ measurableAtom y = measurableAtom z
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: α : Type u_3
β : Type u_4
t : TopologicalSpace α
inst✝⁵ : PolishSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
tβ : TopologicalSpace β
inst✝² : MeasurableSpace β
inst✝¹ : OpensMeasurableSpace β
f : α → β
inst✝ : SecondCountableTopology ↑(range f)
hf : Measurable f
b : Set (Set ↑(range f))
b_count : b.Countable
hb : IsTopologicalBasis b
this✝ : Countable ↑b
this : ∀ (s : ↑b), IsClopenable (rangeFactorization f ⁻¹' ↑s)
⊢ ∃ t' ≤ t, Continuous[_, tβ] f ∧ PolishSpace α

Tactic:
choose T Tt Tpolish _ Topen using this

Goal state after:
α : Type u_3
β : Type u_4
t : TopologicalSpace α
inst✝⁵ : PolishSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
tβ : TopologicalSpace β
inst✝² : MeasurableSpace β
inst✝¹ : OpensMeasurableSpace β
f : α → β
inst✝ : SecondCountableTopology ↑(range f)
hf : Measurable f
b : Set (Set ↑(range f))
b_count : b.Countable
hb : IsTopologicalBasis b
this : Countable ↑b
T : ↑b → TopologicalSpace α
Tt : ∀ (s : ↑b), T s ≤ t
Tpolish : ∀ (s : ↑b), PolishSpace α
h✝ : ∀ (s : ↑b), IsClosed[T s] (rangeFactorization f ⁻¹' ↑s)
Topen : ∀ (s : ↑b), IsOpen[T s] (rangeFactorization f ⁻¹' ↑s)
⊢ ∃ t' ≤ t, Continuous[_, tβ] f ∧ PolishSpace α
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSingletonClass α
f : β → α
s : Finset α
μ : Measure β
hf : AEMeasurable f μ
⊢ map f μ = ∑ a ∈ s, (map f μ) {a} • dirac a ↔ map f μ = ∑ a ∈ s, μ (f ⁻¹' {a}) • dirac a

Tactic:
simp [map_apply₀ hf]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : α → Measure β
inst✝ : ∀ (a : α), IsFiniteMeasure (μ a)
S : Set (Set β)
hgen : mβ = MeasurableSpace.generateFrom S
hpi : IsPiSystem S
h_basic : ∀ s ∈ S, Measurable fun a ↦ (μ a) s
h_univ : Measurable fun a ↦ (μ a) univ
⊢ ∀ (s : Set β), MeasurableSet s → Measurable fun b ↦ (μ b) s

Tactic:
intro s hs

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : α → Measure β
inst✝ : ∀ (a : α), IsFiniteMeasure (μ a)
S : Set (Set β)
hgen : mβ = MeasurableSpace.generateFrom S
hpi : IsPiSystem S
h_basic : ∀ s ∈ S, Measurable fun a ↦ (μ a) s
h_univ : Measurable fun a ↦ (μ a) univ
s : Set β
hs : MeasurableSet s
⊢ Measurable fun b ↦ (μ b) s
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
h : a ∉ s
f : α → ℝ≥0∞
⊢ ∫⁻ (x : α) in s ∪ {a}, f x ∂μ = f a * μ {a} + ∫⁻ (x : α) in s, f x ∂μ

Tactic:
lintegral_union (measurableSet_singleton a),

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
h : a ∉ s
f : α → ℝ≥0∞
⊢ ∫⁻ (a : α) in s, f a ∂μ + ∫⁻ (a : α) in {a}, f a ∂μ = f a * μ {a} + ∫⁻ (x : α) in s, f x ∂μ

α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
h : a ∉ s
f : α → ℝ≥0∞
⊢ Disjoint s {a}
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
⊢ (ae m).bind ae ≤ ae m.join

Tactic:
intro s hs

Goal state after:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
s : Set α
hs : s ∈ ae m.join
⊢ 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 ∂μ
φ : α → ℝ≥0∞ := fun x ↦ ⨆ n, g n x
hφm : Measurable φ
hφle : φ ≤ f
s : Set α
ψ : SimpleFunc α ℝ≥0
hψ : ∀ (x : α), ↑(ψ x) ≤ f x
⊢ ∃ n, ∀ (x : α), ψ x ≤ ↑n

Tactic:
by
    rcases ψ.range.bddAbove with ⟨C, hC⟩
    exact ⟨⌈C⌉₊, fun x ↦ (hC <| ψ.mem_range_self x).trans (Nat.le_ceil _)⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
⊢ ∀ (s : Set (α × β)), MeasurableSet s → Measurable fun b ↦ (map (Prod.mk b) ν) s

Tactic:
intro s hs

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
⊢ Measurable fun b ↦ (map (Prod.mk b) ν) s
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
inst✝ : SFinite μ
⊢ ∀ (s : Set (α × β)), MeasurableSet s → Measurable fun b ↦ (map (fun x ↦ (x, b)) μ) s

Tactic:
intro s hs

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
inst✝ : SFinite μ
s : Set (α × β)
hs : MeasurableSet s
⊢ Measurable fun b ↦ (map (fun x ↦ (x, b)) μ) s
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
pa qa : Set α → Prop
H : μ.InnerRegularWRT pa qa
f : α → β
hf : AEMeasurable f μ
pb qb : Set β → Prop
hAB : ∀ (U : Set β), qb U → qa (f ⁻¹' U)
hAB' : ∀ (K : Set α), pa K → pb (f '' K)
hB₂ : ∀ (U : Set β), qb U → MeasurableSet U
U : Set β
⊢ qb U → ∀ r < (map f μ) U, ∃ K ⊆ U, pb K ∧ r < (map f μ) K

Tactic:
hU

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
pa qa : Set α → Prop
H : μ.InnerRegularWRT pa qa
f : α → β
hf : AEMeasurable f μ
pb qb : Set β → Prop
hAB : ∀ (U : Set β), qb U → qa (f ⁻¹' U)
hAB' : ∀ (K : Set α), pa K → pb (f '' K)
hB₂ : ∀ (U : Set β), qb U → MeasurableSet U
U : Set β
hU : qb U
⊢ ∀ r < (map f μ) U, ∃ K ⊆ U, pb K ∧ r < (map f μ) K
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
pa qa : Set α → Prop
H : μ.InnerRegularWRT pa qa
f : α ≃ᵐ β
pb qb : Set β → Prop
hAB : ∀ (U : Set β), qb U → qa (⇑f ⁻¹' U)
hAB' : ∀ (K : Set α), pa K → pb (⇑f '' K)
U : Set β
⊢ qb U → ∀ r < (map (⇑f) μ) U, ∃ K ⊆ U, pb K ∧ r < (map (⇑f) μ) K

Tactic:
hU

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
pa qa : Set α → Prop
H : μ.InnerRegularWRT pa qa
f : α ≃ᵐ β
pb qb : Set β → Prop
hAB : ∀ (U : Set β), qb U → qa (⇑f ⁻¹' U)
hAB' : ∀ (K : Set α), pa K → pb (⇑f '' K)
U : Set β
hU : qb U
⊢ ∀ r < (map (⇑f) μ) U, ∃ K ⊆ U, pb K ∧ r < (map (⇑f) μ) K
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : 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 α
⊢ qa U → ∀ r < (comap f μ) U, ∃ K ⊆ U, pa K ∧ r < (comap f μ) K

Tactic:
hU

Goal state after:
α : 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 < (comap f μ) U, ∃ K ⊆ U, pa K ∧ r < (comap f μ) K
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_4
β : Type u_5
γ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure (α × β × γ)
inst✝ : IsFiniteMeasure μ
h :
  ∀ {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s → MeasurableSet t → MeasurableSet u → μ (s ×ˢ t ×ˢ u) = ν (s ×ˢ t ×ˢ u)
s : Set (α × β × γ)
hs : MeasurableSet s
⊢ μ (univ ×ˢ univ ×ˢ univ) = ν (univ ×ˢ univ ×ˢ univ)

Tactic:
exact h .univ .univ .univ

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∞
U : Set α
⊢ q U → ∀ r < (c • μ) U, ∃ K ⊆ U, p K ∧ r < (c • μ) K

Tactic:
hU

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
H : μ.InnerRegularWRT p q
c : ℝ≥0∞
U : Set α
hU : q U
⊢ ∀ r < (c • μ) U, ∃ K ⊆ U, p K ∧ r < (c • μ) K
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q q' : Set α → Prop
H : μ.InnerRegularWRT p q
H' : μ.InnerRegularWRT q q'
U : Set α
⊢ q' U → ∀ r < μ U, ∃ K ⊆ U, p K ∧ r < μ K

Tactic:
hU

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q q' : Set α → Prop
H : μ.InnerRegularWRT p q
H' : μ.InnerRegularWRT q q'
U : Set α
hU : q' U
⊢ ∀ r < μ U, ∃ K ⊆ U, p K ∧ r < μ K