mathlib-initiative/mathlib-tactics huggingface dataset:
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
  · 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)))
    obtain ⟨t, ht⟩ := exists_lt_of_lt_ciSup
      (ENNReal.sub_lt_self h_lt_top.ne hC_lt.ne_bot (by simp) :
          (⨆ (s) (_ : MeasurableSet s) (_ : SigmaFinite (μ.restrict s)), ν s) - 1 / n
        < ⨆ (s) (_ : MeasurableSet s) (_ : SigmaFinite (μ.restrict s)), ν s)
    have ht_meas : MeasurableSet t := by
      by_contra h_notMem
      simp only [h_notMem] at ht
      simp at ht
    have ht_mem : SigmaFinite (μ.restrict t) := by
      by_contra h_notMem
      simp only [h_notMem] at ht
      simp at ht
    refine ⟨t, ht_meas, ht_mem, ?_⟩
    simp only [ht_meas, ht_mem, iSup_true] at ht
    exact ht.le
  · refine ⟨∅, MeasurableSet.empty, by rw [Measure.restrict_empty]; infer_instance, ?_⟩
    rw [tsub_eq_zero_of_le hC_lt]
    exact zero_le

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

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ

Tactic:
refine
    @Measurable.ennreal_induction α m (fun f => ∫⁻ a, f a ∂μ.trim hm = ∫⁻ a, f a ∂μ) ?_ ?_ ?_ f hf
  · intro c s hs
    rw [lintegral_indicator hs, lintegral_indicator (hm s hs), setLIntegral_const,
      setLIntegral_const]
    suffices h_trim_s : μ.trim hm s = μ s by rw [h_trim_s]
    exact trim_measurableSet_eq hm hs
  · intro f g _ hf _ hf_prop hg_prop
    have h_m := lintegral_add_left (μ := Measure.trim μ hm) hf g
    have h_m0 := lintegral_add_left (μ := μ) (Measurable.mono hf hm le_rfl) g
    rwa [hf_prop, hg_prop, ← h_m0] at h_m
  · intro f hf hf_mono hf_prop
    rw [lintegral_iSup hf hf_mono]
    rw [lintegral_iSup (fun n => Measurable.mono (hf n) hm le_rfl) hf_mono]
    congr with n
    exact hf_prop n

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

Goal state before:
pp: α : Type u_5
E : Type u_6
m m₂ : MeasurableSpace α
inst✝¹ : TopologicalSpace E
inst✝ : Zero E
s : Set α
f : α → E
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
hs_m₂ : MeasurableSet s
⊢ StronglyMeasurable f

Tactic:
have h_sub : m.comap ((↑) : s → α) ≤ m₂.comap ((↑) : s → α) := by
    intro _ ht
    rcases ht with ⟨u, hu, rfl⟩
    exact ⟨s ∩ u, hs u (hs_m.inter hu), by simp⟩

Goal state after:
α : Type u_5
E : Type u_6
m m₂ : MeasurableSpace α
inst✝¹ : TopologicalSpace E
inst✝ : Zero E
s : Set α
f : α → E
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
hs_m₂ : MeasurableSet s
h_sub : MeasurableSpace.comap Subtype.val m ≤ MeasurableSpace.comap Subtype.val m₂
⊢ StronglyMeasurable f
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: x : ↑I
⊢ Iic x = Icc 0 x

Tactic:
exact Icc_bot.symm

Goal state after:
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: x : ↑I
⊢ Iio x = Ico 0 x

Tactic:
exact Ico_bot.symm

Goal state after:
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : LinearOrder α
a b : α
h : a ≤ b
δ : α
⊢ ↑(projIcc a b h (a + 0)) = a

Tactic:
add_zero,

Goal state after:
α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : LinearOrder α
a b : α
h : a ≤ b
δ : α
⊢ ↑(projIcc a b h a) = a
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: case mp
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
hε : 0 < ε
s : Set ((X ⊕ Y) × (X ⊕ Y))
⊢ ((∃ ε > 0, ∀ ⦃a b : X⦄, dist a b < ε → Prod.map Sum.inl Sum.inl (a, b) ∈ s) ∧
      ∃ ε > 0, ∀ ⦃a b : Y⦄, dist a b < ε → Prod.map Sum.inr Sum.inr (a, b) ∈ s) →
    ∃ δ > 0, ∀ (a b : X ⊕ Y), glueDist Φ Ψ ε a b < δ → (a, b) ∈ s

Tactic:
rintro ⟨⟨δX, δX0, hX⟩, δY, δY0, hY⟩
    refine ⟨min (min δX δY) ε, lt_min (lt_min δX0 δY0) hε, ?_⟩
    rintro (a | a) (b | b) h <;> simp only [lt_min_iff] at h
    · exact hX h.1.1
    · exact absurd h.2 (le_glueDist_inl_inr _ _ _ _ _).not_gt
    · exact absurd h.2 (le_glueDist_inr_inl _ _ _ _ _).not_gt
    · exact hY h.1.2

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

Goal state before:
pp: case mpr.left
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε✝ : ℝ
hε : 0 < ε✝
s : Set ((X ⊕ Y) × (X ⊕ Y))
ε : ℝ
ε0 : ε > 0
H : ∀ (a b : X ⊕ Y), glueDist Φ Ψ ε✝ a b < ε → (a, b) ∈ s
⊢ ∃ ε > 0, ∀ ⦃a b : X⦄, dist a b < ε → Prod.map Sum.inl Sum.inl (a, b) ∈ s

Tactic:
exact ⟨ε, ε0, fun _ _ h => H _ _ h⟩

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

Goal state before:
pp: case mpr.right
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε✝ : ℝ
hε : 0 < ε✝
s : Set ((X ⊕ Y) × (X ⊕ Y))
ε : ℝ
ε0 : ε > 0
H : ∀ (a b : X ⊕ Y), glueDist Φ Ψ ε✝ a b < ε → (a, b) ∈ s
⊢ ∃ ε > 0, ∀ ⦃a b : Y⦄, dist a b < ε → Prod.map Sum.inr Sum.inr (a, b) ∈ s

Tactic:
exact ⟨ε, ε0, fun _ _ h => H _ _ h⟩

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

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

Tactic:
intro m

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

Goal state before:
pp: case mpr.left
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
ε : ℝ
ε0 : ε > 0
H : ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s
⊢ ∃ ε > 0, ∀ ⦃a b : X⦄, dist a b < ε → (a, b) ∈ (fun p ↦ (Sum.inl p.1, Sum.inl p.2)) ⁻¹' s

Tactic:
exact ⟨ε, ε0, fun _ _ h => H _ _ h⟩

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

Goal state before:
pp: case mpr.right
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
ε : ℝ
ε0 : ε > 0
H : ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s
⊢ ∃ ε > 0, ∀ ⦃a b : Y⦄, dist a b < ε → (a, b) ∈ (fun p ↦ (Sum.inr p.1, Sum.inr p.2)) ⁻¹' s

Tactic:
exact ⟨ε, ε0, fun _ _ h => H _ _ h⟩

Goal state after:
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : IsTopologicalRing 𝕜
a b : 𝕜
h : a < b
e : ↑(Icc 0 1) ≃ₜ ↑(⇑(affineHomeomorph (b - a) a ⋯) '' Icc 0 1) := ⋯
⊢ ⇑(affineHomeomorph (b - a) a ⋯) '' Icc 0 1 = Icc a b

Tactic:
affineHomeomorph_image_I _ _ (sub_pos.2 h)

Goal state after:
𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : IsTopologicalRing 𝕜
a b : 𝕜
h : a < b
e : ↑(Icc 0 1) ≃ₜ ↑(⇑(affineHomeomorph (b - a) a ⋯) '' Icc 0 1) := (affineHomeomorph (b - a) a ⋯).image (Icc 0 1)
⊢ Icc a (b - a + a) = Icc a b
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: case refine_2.inl
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x y : E i
⊢ Sigma.dist ⟨i, x⟩ ⟨i, y⟩ = Sigma.dist ⟨i, y⟩ ⟨i, x⟩

Tactic:
simp [Sigma.dist, dist_comm]

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

Goal state before:
pp: case refine_3.inl
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x y : E i
⊢ Sigma.dist ⟨i, x⟩ ⟨i, y⟩ = 0 → ⟨i, x⟩ = ⟨i, y⟩

pp: case refine_3.inr
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
hij : i ≠ j
⊢ Sigma.dist ⟨i, x⟩ ⟨j, y⟩ = 0 → ⟨i, x⟩ = ⟨j, y⟩

Tactic:
· simp [Sigma.dist]

Goal state after:
case refine_3.inr
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
hij : i ≠ j
⊢ Sigma.dist ⟨i, x⟩ ⟨j, y⟩ = 0 → ⟨i, x⟩ = ⟨j, y⟩
Module: Mathlib.Topology.MetricSpace.CantorScheme

Goal state before:
pp: case refine_1.x
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
x : ↑(inducedMap A).fst
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ y ∈ A (res (↑x) n), ∀ z ∈ A (res (↑x) n), dist y z < ε
y : ↑(inducedMap A).fst
hyx : res (↑y) n = res (↑x) n
⊢ (inducedMap A).snd y ∈ A (res (↑x) n)

pp: case refine_1.x
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
x : ↑(inducedMap A).fst
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ y ∈ A (res (↑x) n), ∀ z ∈ A (res (↑x) n), dist y z < ε
y : ↑(inducedMap A).fst
hyx : res (↑y) n = res (↑x) n
⊢ (inducedMap A).snd x ∈ A (res (↑x) n)

Tactic:
· rw [← hyx]
      apply map_mem

Goal state after:
case refine_1.x
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
x : ↑(inducedMap A).fst
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ y ∈ A (res (↑x) n), ∀ z ∈ A (res (↑x) n), dist y z < ε
y : ↑(inducedMap A).fst
hyx : res (↑y) n = res (↑x) n
⊢ (inducedMap A).snd x ∈ A (res (↑x) n)
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
hs : ∀ (n : ℕ), TopologicalSpace.SeparableSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
⊢ TopologicalSpace.SeparableSpace (InductiveLimit I)

Tactic:
choose hsX hcX hdX using (fun n ↦ TopologicalSpace.exists_countable_dense (X n))
  let s := ⋃ (i : ℕ), (toInductiveLimit I i '' (hsX i))
  refine ⟨s, countable_iUnion (fun n => (hcX n).image _), ?_⟩
  refine .of_closure <| (dense_iUnion_range_toInductiveLimit I).mono <| iUnion_subset fun i ↦ ?_
  calc
    range (toInductiveLimit I i) ⊆ closure (toInductiveLimit I i '' (hsX i)) :=
      (toInductiveLimit_isometry I i |>.continuous).range_subset_closure_image_dense (hdX i)
    _ ⊆ closure s := closure_mono <| subset_iUnion (fun j ↦ toInductiveLimit I j '' hsX j) i

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
ε : ℝ≥0
hε : 0 < ε
⊢ ∃ s, μ s = 0 ∧ ν sᶜ ≤ 2 * ↑ε

Tactic:
have h₁ : (μ ⊓ ν) univ = 0 := le_bot_iff.1 (h (inf_le_left (b := ν)) inf_le_right) ▸ rfl
  simp_rw [Measure.inf_apply MeasurableSet.univ, inter_univ] at h₁
  have h₂ : ∀ n : ℕ, ∃ t, μ t + ν tᶜ < ε * (1 / 2) ^ n := by
    intro n
    obtain ⟨m, ⟨t, ht₁, rfl⟩, hm₂⟩ :
        ∃ x ∈ {m | ∃ t, m = μ t + ν tᶜ}, x < ε * (1 / 2 : ℝ≥0∞) ^ n := by
      refine exists_lt_of_csInf_lt ⟨ν univ, ∅, by simp⟩ <| h₁ ▸ ENNReal.mul_pos ?_ (by simp)
      norm_cast
      exact hε.ne.symm
    exact ⟨t, hm₂⟩
  choose t ht₂ using h₂
  refine ⟨⋂ n, t n, ?_, ?_⟩
  · refine eq_zero_of_le_mul_pow (by simp)
      fun n ↦ ((measure_mono <| iInter_subset_of_subset n fun _ ht ↦ ht).trans
      (le_add_right le_rfl)).trans (ht₂ n).le
  · rw [compl_iInter, (by simp [ENNReal.tsum_mul_left, mul_comm] :
      2 * (ε : ℝ≥0∞) = ∑' (n : ℕ), ε * (1 / 2 : ℝ≥0∞) ^ n)]
    refine (measure_iUnion_le _).trans ?_
    exact ENNReal.summable.tsum_le_tsum (fun n ↦ (le_add_left le_rfl).trans (ht₂ n).le)
      ENNReal.summable

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
s : Set α
inst✝ : Nonempty α
⊢ count ≠ 0

Tactic:
rintro h

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
s : Set α
inst✝ : Nonempty α
h : count = 0
⊢ False
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

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

Tactic:
intro m

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
f g : (ℕ → ℕ) → α
hf : Continuous[_, inst✝³] f
hg : Continuous[_, inst✝³] g
h : Disjoint (range f) (range g)
hfg : ¬MeasurablySeparable (range f) (range g)
I :
  ∀ (n : ℕ) (x y : ℕ → ℕ),
    ¬MeasurablySeparable (f '' cylinder x n) (g '' cylinder y n) →
      ∃ x' y',
        x' ∈ cylinder x n ∧
          y' ∈ cylinder y n ∧ ¬MeasurablySeparable (f '' cylinder x' (n + 1)) (g '' cylinder y' (n + 1))
A : Type := { 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
m : ℕ
⊢ ∀ (n : ℕ), m + 1 ≤ n → (↑(p n)).2.1 m = (↑(p (m + 1))).2.1 m
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
⊢ Measurable fun μ ↦ map f μ

Tactic:
by
  refine measurable_of_measurable_coe _ fun s hs => ?_
  simp_rw [map_apply hf hs]
  exact measurable_coe (hf hs)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α → ℝ≥0∞
a_mble : Measurable a
c : ℝ≥0∞
tsum_le_c : ∑' (i : α), a i ≤ c
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
ε_ne_top : ε ≠ ∞
⊢ count {i | ε ≤ a i} ≤ c / ε

Tactic:
rw [← lintegral_count] at tsum_le_c
  apply (MeasureTheory.meas_ge_le_lintegral_div a_mble.aemeasurable ε_ne_zero ε_ne_top).trans
  exact ENNReal.div_le_div tsum_le_c rfl.le

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
⊢ Measurable fun μ ↦ ⨆ n, ∑ x ∈ (SimpleFunc.eapprox f n).range, x * μ (⇑(SimpleFunc.eapprox f n) ⁻¹' {x})

Tactic:
refine .iSup fun n => Finset.measurable_fun_sum _ fun i _ => ?_

Goal state after:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
n : ℕ
i : ℝ≥0∞
x✝ : i ∈ (SimpleFunc.eapprox f n).range
⊢ Measurable fun μ ↦ i * μ (⇑(SimpleFunc.eapprox f n) ⁻¹' {i})
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

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

Tactic:
intro m

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

Goal state before:
pp: case neg
α : 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
⊢ ∃ g, (∀ (x : α), g x ≤ (f₁ + f₂) x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ∞ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ

Tactic:
by_cases hf₂ : ∫⁻ x, f₂ x ∂μ = 0

Goal state after:
case pos
α : 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
⊢ ∃ g, (∀ (x : α), g x ≤ (f₁ + f₂) x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ∞ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ

case neg
α : 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
⊢ ∃ g, (∀ (x : α), g x ≤ (f₁ + f₂) x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ∞ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case inr.refine_1
X : Type u_3
inst✝¹ : MetricSpace X
inst✝ : SeparableSpace X
x : X
C : Set X
hxC : C ∈ 𝓝 x
ε : ℝ := min (infDist x (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ)) 1
hC : (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ).Nonempty
this : Nonempty X
n : ℕ
hn : dist x (denseSeq X n) < ε / 2
⊢ distDenseSeq X n x ∈ ball 0 (ε / 2)

pp: case inr.refine_2
X : Type u_3
inst✝¹ : MetricSpace X
inst✝ : SeparableSpace X
x : X
C : Set X
hxC : C ∈ 𝓝 x
ε : ℝ := min (infDist x (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ)) 1
hC : (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ).Nonempty
this : Nonempty X
n : ℕ
hn : dist x (denseSeq X n) < ε / 2
⊢ distDenseSeq X n ⁻¹' ball 0 (ε / 2) ⊆ C

Tactic:
· simp [Subtype.dist_eq, abs_eq_self.mpr, coe_projIcc, hn]

Goal state after:
case inr.refine_2
X : Type u_3
inst✝¹ : MetricSpace X
inst✝ : SeparableSpace X
x : X
C : Set X
hxC : C ∈ 𝓝 x
ε : ℝ := min (infDist x (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ)) 1
hC : (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ).Nonempty
this : Nonempty X
n : ℕ
hn : dist x (denseSeq X n) < ε / 2
⊢ distDenseSeq X n ⁻¹' ball 0 (ε / 2) ⊆ C
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 α
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
⊢ ∃ K ⊆ U, pa K ∧ r < (comap f μ) K

Tactic:
refine ⟨f ⁻¹' K, ?_, hAB' K hKrange hK, ?_⟩

Goal state after:
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 ⊆ U

case refine_2
α : 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
⊢ r < (comap f μ) (f ⁻¹' K)
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
mβ : MeasurableSpace β
inst✝¹ : TopologicalSpace β
μ : Measure β
inst✝ : μ.OuterRegular
f : α → β
f_cont : Continuous[inst✝², inst✝¹] f
f_me : MeasurableEmbedding f
A : Set α
hA : MeasurableSet A
r : ℝ≥0∞
hr : r > μ (f '' A)
U : Set β
hUA : U ⊇ f '' A
Uopen : IsOpen[inst✝¹] U
hμU : μ U < r
⊢ f ⁻¹' U ⊇ A

Tactic:
rwa [ge_iff_le, ← image_subset_iff]

Goal state after: