mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: case inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
hm : f.FinMeasSupp μ
hf : ∀ᵐ (a : α) ∂μ, f a ≠ ∞
a : ℝ≥0∞
ha✝ : a ∈ f.range
ha : a ≠ ∞
⊢ a * μ (⇑f ⁻¹' {a}) < ∞

Tactic:
· by_cases ha0 : a = 0
    · subst a
      simp
    · exact mul_lt_top ha.lt_top (finMeasSupp_iff.1 hm _ ha0)

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

Goal state before:
pp: ⊢ borel ℝ = generateFrom (⋃ a, {Iio ↑a})

Tactic:
rw [borel_eq_generateFrom_Iio]
  refine le_antisymm
    (generateFrom_le ?_)
    (generateFrom_mono <| iUnion_subset fun q ↦ singleton_subset_iff.mpr <| mem_range_self _)
  rintro _ ⟨a, rfl⟩
  have : IsLUB (range ((↑) : ℚ → ℝ) ∩ Iio a) a := by
    simp [isLUB_iff_le_iff, mem_upperBounds, ← le_iff_forall_rat_lt_imp_le]
  rw [← this.biUnion_Iio_eq, ← image_univ, ← image_inter_preimage, univ_inter, biUnion_image]
  exact MeasurableSet.biUnion (to_countable _)
    fun b _ => GenerateMeasurable.basic (Iio (b : ℝ)) (by simp)

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

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

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

Tactic:
· exact iSup_le fun i => iSup_le fun _ => iSup_le fun h'i => lintegral_mono h'i

Goal state after:
case a
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
⊢ ∫⁻ (a : α), f a ∂μ ≤ ⨆ g, ⨆ (_ : Measurable g), ⨆ (_ : g ≤ f), ∫⁻ (a : α), g a ∂μ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
⊢ Tendsto (fun n ↦ ∫⁻ (x : α), f n x ∂μ) atTop (𝓝 (∫⁻ (x : α), F x ∂μ))

Tactic:
by
  have : Monotone fun n => ∫⁻ x, f n x ∂μ := fun i j hij =>
    lintegral_mono_ae (h_mono.mono fun x hx => hx hij)
  suffices key : ∫⁻ x, F x ∂μ = ⨆ n, ∫⁻ x, f n x ∂μ by
    rw [key]
    exact tendsto_atTop_iSup this
  rw [← lintegral_iSup' hf h_mono]
  refine lintegral_congr_ae ?_
  filter_upwards [h_mono, h_tendsto] with _ hx_mono hx_tendsto using
    tendsto_nhds_unique hx_tendsto (tendsto_atTop_iSup hx_mono)

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (a : α), r * f a ∂μ = ∫⁻ (a : α), ⨆ n, (const α r * eapprox f n) a ∂μ

Tactic:
by
      congr
      funext a
      rw [← iSup_eapprox_apply hf, ENNReal.mul_iSup]
      simp

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

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

Tactic:
intro f hf hf_mono hf_prop

Goal state after:
case refine_3
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
hf_mono : Monotone f
hf_prop : ∀ (n : ℕ), ∫⁻ (a : α), f n a ∂μ.trim hm = ∫⁻ (a : α), f n a ∂μ
⊢ ∫⁻ (a : α), (fun x ↦ ⨆ n, f n x) a ∂μ.trim hm = ∫⁻ (a : α), (fun x ↦ ⨆ n, f n x) a ∂μ
Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : SFinite ν
hμν : μ ≪ ν
⊢ μ.restrict (μ.sigmaFiniteSetWRT ν)ᶜ = ∞ • ν.restrict (μ.sigmaFiniteSetWRT ν)ᶜ

Tactic:
ext s

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : SFinite ν
hμν : μ ≪ ν
s : Set α
a✝ : MeasurableSet s
⊢ (μ.restrict (μ.sigmaFiniteSetWRT ν)ᶜ) s = (∞ • ν.restrict (μ.sigmaFiniteSetWRT ν)ᶜ) s
Module: Mathlib.Topology.Perfect

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T1Space α
h : Perfect (closure[inst✝¹] C)
x : α
xC : x ∈ C
H : ∃ᶠ (y : α) in 𝓝 x, y ≠ x ∧ y ∈ closure[inst✝¹] C
y : α
hyx : y ≠ x
yC : y ∈ closure[inst✝¹] C
⊢ ∃ᶠ (z : α) in 𝓝 y, z ≠ x ∧ z ∈ C

Tactic:
simp only [← mem_compl_singleton_iff, and_comm, ← frequently_nhdsWithin_iff,
      hyx.nhdsWithin_compl_singleton, ← mem_closure_iff_frequently]

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T1Space α
h : Perfect (closure[inst✝¹] C)
x : α
xC : x ∈ C
H : ∃ᶠ (y : α) in 𝓝 x, y ≠ x ∧ y ∈ closure[inst✝¹] C
y : α
hyx : y ≠ x
yC : y ∈ closure[inst✝¹] C
⊢ y ∈ closure[inst✝¹] C
Module: Mathlib.Analysis.Normed.Group.FunctionSeries

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
u : α → ℝ
f : α → β → F
hu : Summable u
s : Set β
hfu : ∀ (n : α), ∀ x ∈ s, ‖f n x‖ ≤ u n
ε : ℝ
εpos : ε > 0
t : Finset α
ht : ∑' (a : { x // x ∉ t }), u ↑a < ε
x : β
hx : x ∈ s
A : Summable fun n ↦ ‖f n x‖
⊢ dist (∑' (n : α), f n x) (∑ n ∈ t, f n x) < ε

Tactic:
rw [dist_eq_norm, ← A.of_norm.sum_add_tsum_subtype_compl t, add_sub_cancel_left]

Goal state after:
α : Type u_1
β : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
u : α → ℝ
f : α → β → F
hu : Summable u
s : Set β
hfu : ∀ (n : α), ∀ x ∈ s, ‖f n x‖ ≤ u n
ε : ℝ
εpos : ε > 0
t : Finset α
ht : ∑' (a : { x // x ∉ t }), u ↑a < ε
x : β
hx : x ∈ s
A : Summable fun n ↦ ‖f n x‖
⊢ ‖∑' (x_1 : { x // x ∉ t }), f (↑x_1) x‖ < ε
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: case refine_2
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c✝ d✝ : α
h : a ≤ b
c d : α
hdc : 0 ≤ c - d
⊢ |c - d| ≤ c - d

Tactic:
exact (abs_eq_self.mpr hdc).le

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

Goal state before:
pp: case inl
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
q : X ⊕ Y
x : X
y : Y
val✝ : X
⊢ Sum.dist (Sum.inl val✝) q = glueDist (fun x_1 ↦ ⋯.some) (fun x ↦ ⋯.some) 1 (Sum.inl val✝) q

Tactic:
cases q

Goal state after:
case inl.inl
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
x : X
y : Y
val✝¹ val✝ : X
⊢ Sum.dist (Sum.inl val✝¹) (Sum.inl val✝) =
    glueDist (fun x_1 ↦ ⋯.some) (fun x ↦ ⋯.some) 1 (Sum.inl val✝¹) (Sum.inl val✝)

case inl.inr
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
x : X
y : Y
val✝¹ : X
val✝ : Y
⊢ Sum.dist (Sum.inl val✝¹) (Sum.inr val✝) =
    glueDist (fun x_1 ↦ ⋯.some) (fun x ↦ ⋯.some) 1 (Sum.inl val✝¹) (Sum.inr val✝)
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: case inr
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
q : X ⊕ Y
x : X
y val✝ : Y
⊢ Sum.dist (Sum.inr val✝) q = glueDist (fun x_1 ↦ ⋯.some) (fun x ↦ ⋯.some) 1 (Sum.inr val✝) q

Tactic:
cases q

Goal state after:
case inr.inl
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
x : X
y val✝¹ : Y
val✝ : X
⊢ Sum.dist (Sum.inr val✝¹) (Sum.inl val✝) =
    glueDist (fun x_1 ↦ ⋯.some) (fun x ↦ ⋯.some) 1 (Sum.inr val✝¹) (Sum.inl val✝)

case inr.inr
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
x : X
y val✝¹ val✝ : Y
⊢ Sum.dist (Sum.inr val✝¹) (Sum.inr val✝) =
    glueDist (fun x_1 ↦ ⋯.some) (fun x ↦ ⋯.some) 1 (Sum.inr val✝¹) (Sum.inr val✝)
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case mp.h₂
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hy : y ∈ cylinder x n
z : (n : ℕ) → E n
hz : z ∈ cylinder x n
i : ℕ
hi : i < n
⊢ z i = y i

Tactic:
hy i hi

Goal state after:
case mp.h₂
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hy : y ∈ cylinder x n
z : (n : ℕ) → E n
hz : z ∈ cylinder x n
i : ℕ
hi : i < n
⊢ z i = x i
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: a b : ℝ
x y z : ↑(Icc a b)
s t : ↑unitInterval
⊢ convexComb x (convexComb z y (convexComb_assoc_coeff₁ (unitInterval.symm t) (unitInterval.symm s)))
      (unitInterval.symm (convexComb_assoc_coeff₂ (unitInterval.symm t) (unitInterval.symm s))) =
    convexComb x
      (convexComb z y
        (unitInterval.symm (unitInterval.symm (convexComb_assoc_coeff₁ (unitInterval.symm t) (unitInterval.symm s)))))
      (unitInterval.symm (convexComb_assoc_coeff₂ (unitInterval.symm t) (unitInterval.symm s)))

Tactic:
unitInterval.symm_symm

Goal state after:
a b : ℝ
x y z : ↑(Icc a b)
s t : ↑unitInterval
⊢ convexComb x (convexComb z y (convexComb_assoc_coeff₁ (unitInterval.symm t) (unitInterval.symm s)))
      (unitInterval.symm (convexComb_assoc_coeff₂ (unitInterval.symm t) (unitInterval.symm s))) =
    convexComb x (convexComb z y (convexComb_assoc_coeff₁ (unitInterval.symm t) (unitInterval.symm s)))
      (unitInterval.symm (convexComb_assoc_coeff₂ (unitInterval.symm t) (unitInterval.symm s)))
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: E : ℕ → Type u_1
x y : (n : ℕ) → E n
⊢ dist x y = dist y x

Tactic:
by
  classical
  simp [dist, @eq_comm _ x y, firstDiff_comm]

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

Goal state before:
pp: ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
z : E i
hij : i ≠ j
⊢ dist x ⋯.some + 0 + 0 + (0 + 0 + dist ⋯.some z) ≤
    dist x ⋯.some + 1 + dist ⋯.some y + (dist y ⋯.some + 1 + dist ⋯.some z)

Tactic:
by apply_rules [add_le_add, le_rfl, dist_nonneg, zero_le_one]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MetricSpace α
C : Set α
hC : Perfect C
hnonempty : C.Nonempty
inst✝ : CompleteSpace α
u : ℕ → ℝ≥0∞
upos' : ∀ (n : ℕ), u n ∈ Ioo 0 1
hu : Tendsto u atTop (nhds 0)
upos : ∀ (n : ℕ), 0 < u n
P : Type (max 0 u_1) := { E // Perfect E ∧ E.Nonempty }
⊢ ∃ f, range f ⊆ C ∧ Continuous f ∧ Injective f

Tactic:
choose C0 C1 h0 h1 hdisj using
    fun {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε) =>
    hC.small_diam_splitting hnonempty hε

Goal state after:
α : Type u_1
inst✝¹ : MetricSpace α
C : Set α
hC : Perfect C
hnonempty : C.Nonempty
inst✝ : CompleteSpace α
u : ℕ → ℝ≥0∞
upos' : ∀ (n : ℕ), u n ∈ Ioo 0 1
hu : Tendsto u atTop (nhds 0)
upos : ∀ (n : ℕ), 0 < u n
P : Type (max 0 u_1) := { E // Perfect E ∧ E.Nonempty }
C0 C1 : {C : Set α} → Perfect C → C.Nonempty → {ε : ℝ≥0∞} → 0 < ε → Set α
h0 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C0 hC hnonempty hε) ∧
      (C0 hC hnonempty hε).Nonempty ∧ C0 hC hnonempty hε ⊆ C ∧ ediam (C0 hC hnonempty hε) ≤ ε
h1 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C1 hC hnonempty hε) ∧
      (C1 hC hnonempty hε).Nonempty ∧ C1 hC hnonempty hε ⊆ C ∧ ediam (C1 hC hnonempty hε) ≤ ε
hdisj :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Disjoint (C0 hC hnonempty hε) (C1 hC hnonempty hε)
⊢ ∃ f, range f ⊆ C ∧ Continuous f ∧ Injective f
Module: Mathlib.Topology.MetricSpace.Perfect

Goal state before:
pp: α : Type u_1
inst✝¹ : MetricSpace α
C : Set α
hC : Perfect C
hnonempty : C.Nonempty
inst✝ : CompleteSpace α
u : ℕ → ℝ≥0∞
upos' : ∀ (n : ℕ), u n ∈ Ioo 0 1
hu : Tendsto u atTop (nhds 0)
upos : ∀ (n : ℕ), 0 < u n
P : Type (max 0 u_1) := { E // Perfect E ∧ E.Nonempty }
C0 C1 : {C : Set α} → Perfect C → C.Nonempty → {ε : ℝ≥0∞} → 0 < ε → Set α
h0 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C0 hC hnonempty hε) ∧
      (C0 hC hnonempty hε).Nonempty ∧ C0 hC hnonempty hε ⊆ C ∧ ediam (C0 hC hnonempty hε) ≤ ε
h1 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C1 hC hnonempty hε) ∧
      (C1 hC hnonempty hε).Nonempty ∧ C1 hC hnonempty hε ⊆ C ∧ ediam (C1 hC hnonempty hε) ≤ ε
hdisj :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Disjoint (C0 hC hnonempty hε) (C1 hC hnonempty hε)
l : List Bool
⊢ P

Tactic:
induction l with
    | nil => exact ⟨C, ⟨hC, hnonempty⟩⟩
    | cons a l ih =>
      cases a
      · use C0 ih.property.1 ih.property.2 (upos (l.length + 1))
        exact ⟨(h0 _ _ _).1, (h0 _ _ _).2.1⟩
      use C1 ih.property.1 ih.property.2 (upos (l.length + 1))
      exact ⟨(h1 _ _ _).1, (h1 _ _ _).2.1⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
e : α ≃ᵐ β
μa : Measure α
μb : Measure β
h : MeasurePreserving (⇑e) μa μb
⊢ map (⇑e.symm) μb = μa

Tactic:
← h.map_eq,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
e : α ≃ᵐ β
μa : Measure α
μb : Measure β
h : MeasurePreserving (⇑e) μa μb
⊢ map (⇑e.symm) (map (⇑e) μa) = μa
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
f : β → ℝ≥0∞
g : α → β
s : Set β
hs : MeasurableSet s
hf : Measurable f
hg : Measurable g
⊢ ∫⁻ (y : β), f y ∂Measure.map g (μ.restrict (g ⁻¹' s)) = ∫⁻ (x : α) in g ⁻¹' s, f (g x) ∂μ

Tactic:
lintegral_map hf hg

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
f : β → ℝ≥0∞
g : α → β
s : Set β
hs : MeasurableSet s
hf : Measurable f
hg : Measurable g
⊢ ∫⁻ (a : α) in g ⁻¹' s, f (g a) ∂μ = ∫⁻ (x : α) in g ⁻¹' s, f (g x) ∂μ
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : Measurable f
a : α
s : Set β
hs : MeasurableSet s
⊢ (map f (dirac a)) s = (dirac (f a)) s

Tactic:
by simp [hs, map_apply hf hs, hf hs, indicator_apply]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : Countable β
inst✝ : MeasurableSingletonClass β
μ : Measure α
f : α → β
hf : Measurable f
⊢ map f μ = sum fun b ↦ μ (f ⁻¹' {b}) • dirac b

Tactic:
ext s

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : Countable β
inst✝ : MeasurableSingletonClass β
μ : Measure α
f : α → β
hf : Measurable f
s : Set β
a✝ : MeasurableSet s
⊢ (map f μ) s = (sum fun b ↦ μ (f ⁻¹' {b}) • dirac b) s
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : Countable ι
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
β : ι → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous[hβ n, inst✝¹] (f n)
f_range : ∀ (n : ι), range (f n) = s n
γ : Type (max u_2 0) := (n : ι) × β n
F : γ → α :=
  fun x ↦
    match x with
    | ⟨n, x⟩ => f n x
F_cont : Continuous[instTopologicalSpaceSigma, inst✝¹] F
⊢ range F = ⋃ n, s n

Tactic:
simp only [γ, F, range_sigma_eq_iUnion_range, f_range]

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
⊢ s = ∅ → count s = 0

Tactic:
rintro rfl; exact measure_empty

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α
⊢ ae (dirac a) = pure a

Tactic:
ext s

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
⊢ s ∈ ae (dirac a) ↔ s ∈ pure a
Module: Mathlib.MeasureTheory.Measure.Count

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : Function.Injective f
h2f : Measurable f
⊢ map f count ≤ count

Tactic:
refine le_intro fun s hs _ ↦ ?_

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : Function.Injective f
h2f : Measurable f
s : Set β
hs : MeasurableSet s
x✝ : s.Nonempty
⊢ (map f count) s ≤ count s
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
⊢ ∀ b ∈ s, MeasurableSet (t ∩ {b})

Tactic:
by measurability

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

Goal state before:
pp: case inr
α : 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
y x : ↑s
hxy : dist x y < 1
hne : x ≠ y
hne' : ↑x ≠ ↑y
⊢ dist (g x) (g y) ≤ 4 * dist x y

Tactic:
have dist' : dist x y = dist x.1 y.1 := rfl

Goal state after:
case inr
α : 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
y x : ↑s
hxy : dist x y < 1
hne : x ≠ y
hne' : ↑x ≠ ↑y
dist' : dist x y = dist ↑x ↑y
⊢ dist (g x) (g y) ≤ 4 * dist x y
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 μ
⊢ MeasurableSet {x | x ∈ s}

Tactic:
by measurability

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f✝ : α → ℝ≥0∞
hfm : Measurable f✝
s : ℕ → Finset ℝ≥0∞
f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞
hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)
hm : Monotone fun n μ ↦ ∑ r ∈ s n, r * f n r μ
n : ℕ
⊢ ∑ r ∈ s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m = ∑ b ∈ s n, ∫⁻ (a : Measure α), b * f n b a ∂m

Tactic:
simp_rw [lintegral_const_mul _ (hf _ _)]

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

Goal state before:
pp: case const.refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * μ s
c_ne_zero : c ≠ 0
this : L / ↑c < μ s
t : Set α
ht : MeasurableSet t
ts : t ⊆ s
mlt : L / ↑c < μ t
t_top : μ t < ∞
⊢ ∫⁻ (x : α), ↑((piecewise t ht (const α c) (const α 0)) x) ∂μ < ∞

Tactic:
simp only [ht, const_zero, coe_piecewise, coe_const, SimpleFunc.coe_zero, univ_inter,
        piecewise_eq_indicator, ENNReal.coe_indicator, Function.const_apply, lintegral_indicator,
        lintegral_const, Measure.restrict_apply', ENNReal.mul_lt_top ENNReal.coe_lt_top t_top]

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

Goal state before:
pp: E : ℕ → Type u_1
ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → PseudoMetricSpace (F i)
x✝ y✝ : (i : ι) → F i
i : ι
x y : (i : ι) → F i
⊢ ∑' (i : ι), min (2⁻¹ ^ encode i) (edist (x i) (y i)) =
    ∑' (n : ι), ENNReal.ofReal (min (2⁻¹ ^ encode n) (dist (x n) (y n)))

Tactic:
congr! with a

Goal state after:
E : ℕ → Type u_1
ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → PseudoMetricSpace (F i)
x✝ y✝ : (i : ι) → F i
i : ι
x y : (i : ι) → F i
a : ι
⊢ min (2⁻¹ ^ encode a) (edist (x a) (y a)) = ENNReal.ofReal (min (2⁻¹ ^ encode a) (dist (x a) (y a)))
Module: Mathlib.MeasureTheory.Measure.OpenPos

Goal state before:
pp: X : Type u_1
inst✝⁵ : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst✝⁴ : μ.IsOpenPosMeasure
inst✝³ : OpensMeasurableSpace X
Z : Type u_3
inst✝² : TopologicalSpace Z
inst✝¹ : MeasurableSpace Z
inst✝ : BorelSpace Z
f : X → Z
hf : Continuous[inst✝⁵, inst✝²] f
hf_surj : Surjective f
⊢ (map f μ).IsOpenPosMeasure

Tactic:
refine ⟨fun U hUo hUne => ?_⟩
  rw [Measure.map_apply hf.measurable hUo.measurableSet]
  exact (hUo.preimage hf).measure_ne_zero μ (hf_surj.nonempty_preimage.mpr hUne)

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

Goal state before:
pp: case e'_4
α : 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
Iy : ∀ (m n : ℕ), m + 1 ≤ n → (↑(p n)).2.2 m = (↑(p (m + 1))).2.2 m
x : ℕ → ℕ := fun n ↦ (↑(p (n + 1))).2.1 n
hx : x = fun n ↦ (↑(p (n + 1))).2.1 n
y : ℕ → ℕ := fun n ↦ (↑(p (n + 1))).2.2 n
hy : y = fun n ↦ (↑(p (n + 1))).2.2 n
n i : ℕ
hi : i < n
⊢ (fun n ↦ (↑(p (n + 1))).2.2 n) i = (↑(p n)).2.2 i

Tactic:
exact (Iy i n hi).symm

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

Goal state before:
pp: case neg.refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (Function.support ⇑f₁) (Function.support ⇑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    L < ∫⁻ (x : α), ↑(f₁ x) ∂μ → ∃ g, (∀ (x : α), g x ≤ f₁ x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ∞ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    L < ∫⁻ (x : α), ↑(f₂ x) ∂μ → ∃ g, (∀ (x : α), g x ≤ f₂ x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ∞ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ
L : ℝ≥0∞
hL✝ : L < ∫⁻ (x : α), ↑(f₁ x) ∂μ + ∫⁻ (x : α), ↑(f₂ x) ∂μ
hf₁ : ¬∫⁻ (x : α), ↑(f₁ x) ∂μ = 0
hf₂ : ¬∫⁻ (x : α), ↑(f₂ x) ∂μ = 0
L₁ : ℝ≥0∞
hL₁ : L₁ < ∫⁻ (x : α), ↑(f₁ x) ∂μ
L₂ : ℝ≥0∞
hL₂ : L₂ < ∫⁻ (x : α), ↑(f₂ x) ∂μ
hL : L < L₁ + L₂
g₁ : α →ₛ ℝ≥0
g₁_le : ∀ (x : α), g₁ x ≤ f₁ x
g₁_top : ∫⁻ (x : α), ↑(g₁ x) ∂μ < ∞
hg₁ : L₁ < ∫⁻ (x : α), ↑(g₁ x) ∂μ
g₂ : α →ₛ ℝ≥0
g₂_le : ∀ (x : α), g₂ x ≤ f₂ x
g₂_top : ∫⁻ (x : α), ↑(g₂ x) ∂μ < ∞
hg₂ : L₂ < ∫⁻ (x : α), ↑(g₂ x) ∂μ
⊢ ∫⁻ (x : α), ↑((g₁ + g₂) x) ∂μ < ∞

Tactic:
apply lt_of_le_of_lt _ (add_lt_top.2 ⟨g₁_top, g₂_top⟩)

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (Function.support ⇑f₁) (Function.support ⇑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    L < ∫⁻ (x : α), ↑(f₁ x) ∂μ → ∃ g, (∀ (x : α), g x ≤ f₁ x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ∞ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    L < ∫⁻ (x : α), ↑(f₂ x) ∂μ → ∃ g, (∀ (x : α), g x ≤ f₂ x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ∞ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ
L : ℝ≥0∞
hL✝ : L < ∫⁻ (x : α), ↑(f₁ x) ∂μ + ∫⁻ (x : α), ↑(f₂ x) ∂μ
hf₁ : ¬∫⁻ (x : α), ↑(f₁ x) ∂μ = 0
hf₂ : ¬∫⁻ (x : α), ↑(f₂ x) ∂μ = 0
L₁ : ℝ≥0∞
hL₁ : L₁ < ∫⁻ (x : α), ↑(f₁ x) ∂μ
L₂ : ℝ≥0∞
hL₂ : L₂ < ∫⁻ (x : α), ↑(f₂ x) ∂μ
hL : L < L₁ + L₂
g₁ : α →ₛ ℝ≥0
g₁_le : ∀ (x : α), g₁ x ≤ f₁ x
g₁_top : ∫⁻ (x : α), ↑(g₁ x) ∂μ < ∞
hg₁ : L₁ < ∫⁻ (x : α), ↑(g₁ x) ∂μ
g₂ : α →ₛ ℝ≥0
g₂_le : ∀ (x : α), g₂ x ≤ f₂ x
g₂_top : ∫⁻ (x : α), ↑(g₂ x) ∂μ < ∞
hg₂ : L₂ < ∫⁻ (x : α), ↑(g₂ x) ∂μ
⊢ ∫⁻ (x : α), ↑((g₁ + g₂) x) ∂μ ≤ ∫⁻ (x : α), ↑(g₁ x) ∂μ + ∫⁻ (x : α), ↑(g₂ x) ∂μ