mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: case pos
α : Type u_1
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : ⋃ i, s i = univ
hs_meas : ∀ (i : ℕ), s i = ∅ ∨ s i = univ
h_univ_empty : univ = ∅
⊢ μ ∅ < ∞

Tactic:
measure_empty

Goal state after:
case pos
α : Type u_1
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : ⋃ i, s i = univ
hs_meas : ∀ (i : ℕ), s i = ∅ ∨ s i = univ
h_univ_empty : univ = ∅
⊢ 0 < ∞
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
ι : Type u_6
x✝ : MeasurableSpace α
μ : Measure α
s : ι → Set α
M : ℕ
hs_meas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (y : α), {i | y ∈ s i}.encard ≤ ↑M
t : Set α
ht : MeasurableSet t
F : Finset ι
P : Finset ι → Set α := fun C ↦ (⋂ i ∈ C, s i) ∩ ⋂ i ∈ F \ C, (s i)ᶜ
Cs : Finset (Finset ι) := F.powerset \ {∅}
G : ι → Set (Finset ι) := fun i ↦ {C | C ∈ F.powerset ∧ i ∈ C}
⊢ ∑ i ∈ F, (μ.restrict (s i)) t ≤ (M • μ.restrict (⋃ i, s i)) t

Tactic:
have P_meas C : MeasurableSet (P C) :=
    measurableSet_biInter C (fun i _ ↦ hs_meas i) |>.inter <|
      measurableSet_biInter _ (fun i _ ↦ (hs_meas i).compl)

Goal state after:
α : Type u_2
ι : Type u_6
x✝ : MeasurableSpace α
μ : Measure α
s : ι → Set α
M : ℕ
hs_meas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (y : α), {i | y ∈ s i}.encard ≤ ↑M
t : Set α
ht : MeasurableSet t
F : Finset ι
P : Finset ι → Set α := fun C ↦ (⋂ i ∈ C, s i) ∩ ⋂ i ∈ F \ C, (s i)ᶜ
Cs : Finset (Finset ι) := F.powerset \ {∅}
G : ι → Set (Finset ι) := fun i ↦ {C | C ∈ F.powerset ∧ i ∈ C}
P_meas : ∀ (C : Finset ι), MeasurableSet (P C)
⊢ ∑ i ∈ F, (μ.restrict (s i)) t ≤ (M • μ.restrict (⋃ i, s i)) t
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case refine_3
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
x : α
A : ℕ → Set α := natGeneratingSequence α
hA : ∀ (n : ℕ), MeasurableSet (A n)
hA_gen : generateFrom (range A) = mα
s : Set α
hxs : x ∈ s
hs : MeasurableSet s
q : (ℕ → Prop) → Prop
hq : s = ⋃ p, if q p then countablyGeneratedAtom α p else ∅
⊢ q fun x_1 ↦ x ∈ A x_1

Tactic:
simp only [hq, mem_iUnion, mem_ite_empty_right] at hxs

Goal state after:
case refine_3
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
x : α
A : ℕ → Set α := natGeneratingSequence α
hA : ∀ (n : ℕ), MeasurableSet (A n)
hA_gen : generateFrom (range A) = mα
s : Set α
hs : MeasurableSet s
q : (ℕ → Prop) → Prop
hq : s = ⋃ p, if q p then countablyGeneratedAtom α p else ∅
hxs : ∃ i, q i ∧ x ∈ countablyGeneratedAtom α i
⊢ q fun x_1 ↦ x ∈ A x_1
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : CountablySeparated α
f : α → ℕ → Bool
fmeas : Measurable f
finj : Injective f
x : α
⊢ MeasurableSet {x}

Tactic:
rw [← finj.preimage_image {x}, image_singleton]

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : CountablySeparated α
f : α → ℕ → Bool
fmeas : Measurable f
finj : Injective f
x : α
⊢ MeasurableSet (f ⁻¹' {f x})
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t' : ℕ → Set α
ht' : s ⊆ iUnion t'
t : Set α := ⋃ n ∈ {k | μ (t' k) ≤ ν (t' k)}, t' n
ht : t = ⋃ n ∈ {k | μ (t' k) ≤ ν (t' k)}, t' n
hle₁ : μ (t ∩ s) ≤ ∑' (n : ↑{k | μ (t' k) ≤ ν (t' k)}), μ (t' ↑n)
⊢ (⋂ i ∈ {k | μ (t' k) ≤ ν (t' k)}, (t' i)ᶜ) ∩ s ⊆ ⋃ n ∈ {k | ν (t' k) < μ (t' k)}, t' n

Tactic:
refine fun x ⟨hx₁, hx₂⟩ ↦ mem_iUnion₂.2 ?_

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t' : ℕ → Set α
ht' : s ⊆ iUnion t'
t : Set α := ⋃ n ∈ {k | μ (t' k) ≤ ν (t' k)}, t' n
ht : t = ⋃ n ∈ {k | μ (t' k) ≤ ν (t' k)}, t' n
hle₁ : μ (t ∩ s) ≤ ∑' (n : ↑{k | μ (t' k) ≤ ν (t' k)}), μ (t' ↑n)
x : α
x✝ : x ∈ (⋂ i ∈ {k | μ (t' k) ≤ ν (t' k)}, (t' i)ᶜ) ∩ s
hx₁ : x ∈ ⋂ i ∈ {k | μ (t' k) ≤ ν (t' k)}, (t' i)ᶜ
hx₂ : x ∈ s
⊢ ∃ i, ∃ (_ : i ∈ {k | ν (t' k) < μ (t' k)}), x ∈ t' i
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ ν : Measure α
s✝ t✝ : Set α
a : α
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : IsLocallyFiniteMeasure μ
s : α → Set α
hsx : ∀ (x : α), s x ∈ 𝓝 x
hsμ : ∀ (x : α), μ (s x) < ∞
t : Set α
htc : t.Countable
htU : ⋃ x ∈ t, s x = univ
⊢ ⋃₀ (s '' t) = univ

Tactic:
sUnion_image

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ ν : Measure α
s✝ t✝ : Set α
a : α
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : IsLocallyFiniteMeasure μ
s : α → Set α
hsx : ∀ (x : α), s x ∈ 𝓝 x
hsμ : ∀ (x : α), μ (s x) < ∞
t : Set α
htc : t.Countable
htU : ⋃ x ∈ t, s x = univ
⊢ ⋃ a ∈ t, s a = univ
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
t : ℕ → Set α
n : ℕ
⊢ generateFrom (memPartition t n) ≤ generateFrom (⋃ n, memPartition t n)

Tactic:
exact generateFrom_mono (subset_iUnion _ _)

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

Goal state before:
pp: case inl
γ : Type u_3
δ : Type u_5
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
inst✝ : MeasurableSpace δ
f : δ → γ
hf : ∀ (s : Set γ), IsClosed[inst✝³] s → s.Nonempty → s ≠ univ → MeasurableSet (f ⁻¹' s)
s : Set γ
hs : IsClosed[inst✝³] s
h1 : s = ∅
⊢ MeasurableSet (f ⁻¹' s)

pp: case inr
γ : Type u_3
δ : Type u_5
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
inst✝ : MeasurableSpace δ
f : δ → γ
hf : ∀ (s : Set γ), IsClosed[inst✝³] s → s.Nonempty → s ≠ univ → MeasurableSet (f ⁻¹' s)
s : Set γ
hs : IsClosed[inst✝³] s
h1 : s.Nonempty
⊢ MeasurableSet (f ⁻¹' s)

Tactic:
· simp [h1]

Goal state after:
case inr
γ : Type u_3
δ : Type u_5
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
inst✝ : MeasurableSpace δ
f : δ → γ
hf : ∀ (s : Set γ), IsClosed[inst✝³] s → s.Nonempty → s ≠ univ → MeasurableSet (f ⁻¹' s)
s : Set γ
hs : IsClosed[inst✝³] s
h1 : s.Nonempty
⊢ MeasurableSet (f ⁻¹' s)
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: α : Type u_5
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
s t : Set α
this✝¹ : MeasurableSpace α := borel α
this✝ : BorelSpace α
a b : α
⊢ MeasurableSet (Icc a b)

Tactic:
exact measurableSet_Icc

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
⊢ hausdorffEDist (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) t = hausdorffEDist s t

Tactic:
by
  refine le_antisymm ?_ ?_
  · calc
      _ ≤ hausdorffEDist (closure s) s + hausdorffEDist s t := hausdorffEDist_triangle
      _ = hausdorffEDist s t := by simp [hausdorffEDist_comm]
  · calc
      _ ≤ hausdorffEDist s (closure s) + hausdorffEDist (closure s) t := hausdorffEDist_triangle
      _ = hausdorffEDist (closure s) t := by simp

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
ι : Sort u_2
s t : ι → Set α
⊢ hausdorffEDist (⋃ i, s i) (⋃ i, t i) ≤ ⨆ i, hausdorffEDist (s i) (t i)

Tactic:
simp_rw [hausdorffEDist, max_le_iff, iSup_iUnion, iSup_le_iff, infEDist_iUnion]

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
ι : Sort u_2
s t : ι → Set α
⊢ (∀ (i : ι),
      ∀ i_1 ∈ s i, ⨅ i, infEDist i_1 (t i) ≤ ⨆ i, max (⨆ x ∈ s i, infEDist x (t i)) (⨆ y ∈ t i, infEDist y (s i))) ∧
    ∀ (i : ι),
      ∀ i_1 ∈ t i, ⨅ i, infEDist i_1 (s i) ≤ ⨆ i, max (⨆ x ∈ s i, infEDist x (t i)) (⨆ y ∈ t i, infEDist y (s i))
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
ε : ℝ≥0
x : α
hx : infEDist x s ≤ ENNReal.ofReal ↑ε
y : α
hy : infEDist y s ≤ ENNReal.ofReal ↑ε
δ : ℝ≥0
hδ : 0 < δ
x✝ : ediam s + 2 * ↑ε < ∞
⊢ edist x y ≤ ediam s + 2 * ↑ε + ↑δ

Tactic:
ENNReal.ofReal_coe_nnreal

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
ε : ℝ≥0
x : α
hx : infEDist x s ≤ ↑ε
y : α
hy : infEDist y s ≤ ↑ε
δ : ℝ≥0
hδ : 0 < δ
x✝ : ediam s + 2 * ↑ε < ∞
⊢ edist x y ≤ ediam s + 2 * ↑ε + ↑δ
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: case inl
α : Type u
inst✝ : PseudoMetricSpace α
x : α
⊢ infEDist x ∅ = ∞ ↔ ∅ = ∅

Tactic:
simp [*, Nonempty.ne_empty, infEDist_ne_top]

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

Goal state before:
pp: case inr
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
hs : s.Nonempty
⊢ infEDist x s = ∞ ↔ s = ∅

Tactic:
simp [*, Nonempty.ne_empty, infEDist_ne_top]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
ε : ℝ
s : Set α
⊢ (thickening ε s).Nonempty ↔ 0 < ε ∧ s.Nonempty

Tactic:
by
  simp [nonempty_iff_ne_empty]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
r : ℝ≥0
hr : 0 < r
h : ∀ x ∈ s, ∀ y ∈ t, ↑r < edist x y
z : α
hzs : ∃ z_1 ∈ s, edist z z_1 < ENNReal.ofReal ↑(r / 2)
hzt : ∃ z_1 ∈ t, edist z z_1 < ENNReal.ofReal ↑(r / 2)
⊢ z ∈ ⊥

Tactic:
ENNReal.ofReal_coe_nnreal

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
r : ℝ≥0
hr : 0 < r
h : ∀ x ∈ s, ∀ y ∈ t, ↑r < edist x y
z : α
hzs : ∃ z_1 ∈ s, edist z z_1 < ↑(r / 2)
hzt : ∃ z_1 ∈ t, edist z z_1 < ↑(r / 2)
⊢ z ∈ ⊥
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: case h₂
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
⊢ ⋂ ε ∈ s, cthickening ε E ⊆ cthickening δ E

Tactic:
unfold cthickening

Goal state after:
case h₂
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
⊢ ⋂ ε ∈ s, {x | infEDist x E ≤ ENNReal.ofReal ε} ⊆ {x | infEDist x E ≤ ENNReal.ofReal δ}
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : α → β
hg : MeasurableEmbedding g
f₂ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this✝ : MeasurableSpace γ := ⊤
this : MeasurableSingletonClass γ
⊢ ∀ (x : γ), MeasurableSet (Function.extend g ⇑f₁ ⇑f₂ ⁻¹' {x})

Tactic:
exact fun x => hg.measurable_extend f₁.measurable f₂.measurable (measurableSet_singleton _)

Goal state after:
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✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
f : δ → α
hf : ∀ (x : α), MeasurableSet (f ⁻¹' Iic x)
⊢ ∀ (x : α), MeasurableSet (f ⁻¹' Ioi x)

Tactic:
simp_rw [← compl_Iic, preimage_compl, MeasurableSet.compl_iff]

Goal state after:
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
f : δ → α
hf : ∀ (x : α), MeasurableSet (f ⁻¹' Iic x)
⊢ ∀ (x : α), MeasurableSet (f ⁻¹' Iic x)
Module: Mathlib.MeasureTheory.MeasurableSpace.Prod

Goal state before:
pp: α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
⊢ Prod.instMeasurableSpace = generateFrom (image2 (fun x1 x2 ↦ x1 ×ˢ x2) C D)

Tactic:
by
  apply le_antisymm
  · refine sup_le ?_ ?_ <;> rw [comap_generateFrom] <;> apply generateFrom_le <;>
      rintro _ ⟨s, hs, rfl⟩
    · rcases hD with ⟨t, h1t, h2t⟩
      rw [← prod_univ, ← h2t, prod_iUnion]
      apply MeasurableSet.iUnion
      intro n
      apply measurableSet_generateFrom
      exact ⟨s, hs, t n, h1t n, rfl⟩
    · rcases hC with ⟨t, h1t, h2t⟩
      rw [← univ_prod, ← h2t, iUnion_prod_const]
      apply MeasurableSet.iUnion
      rintro n
      apply measurableSet_generateFrom
      exact mem_image2_of_mem (h1t n) hs
  · apply generateFrom_le
    rintro _ ⟨s, hs, t, ht, rfl⟩
    dsimp only
    rw [prod_eq]
    apply (measurable_fst _).inter (measurable_snd _)
    · exact measurableSet_generateFrom hs
    · exact measurableSet_generateFrom ht

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

Goal state before:
pp: case refine_1
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
⊢ MeasurableSpace.comap (Prod.map g f) Prod.instMeasurableSpace = Prod.instMeasurableSpace

Tactic:
rw [Prod.instMeasurableSpace, Prod.instMeasurableSpace, MeasurableSpace.comap_prodMap,
      hg.comap_eq, hf.comap_eq]

Goal state after:
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✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
inst✝ : Countable ι
f : ι → δ → α
g g' : δ → α
hf : ∀ (i : ι), Measurable (f i)
s : Set δ
hs : MeasurableSet s
hg : ∀ b ∈ s, IsLUB {a | ∃ i, f i b = a} (g b)
hg' : EqOn g g' sᶜ
g'_meas : Measurable g'
hι : IsEmpty ι
x : δ
hx : x ∈ s
A : ∀ b ∈ s, IsBot (g b)
b : δ
hb : b ∈ s
⊢ g b = g x

Tactic:
apply le_antisymm (A b hb (g x)) (A x hx (g b))

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

Goal state before:
pp: α : Type u
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : PseudoEMetricSpace β
f : α → β
K : Set α
U : Set β
hK : IsCompact K
ho : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
hf : ∀ x ∈ K, ContinuousAt f x
hKU : MapsTo f K U
x : α
hx : x ∈ K
this : {f x} ⊆ U
δ : ℝ
hδ : 0 < δ
hthick : thickening δ {f x} ⊆ U
V : Set α := f ⁻¹' thickening (δ / 2) {f x}
⊢ V ∈ 𝓝 x

Tactic:
apply hf x hx

Goal state after:
α : Type u
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : PseudoEMetricSpace β
f : α → β
K : Set α
U : Set β
hK : IsCompact K
ho : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
hf : ∀ x ∈ K, ContinuousAt f x
hKU : MapsTo f K U
x : α
hx : x ∈ K
this : {f x} ⊆ U
δ : ℝ
hδ : 0 < δ
hthick : thickening δ {f x} ⊆ U
V : Set α := ⋯
⊢ thickening (δ / 2) {f x} ∈ 𝓝 (f x)
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: case refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs : ∀ (x : α), f x ≠ 0 → μ (⇑f ⁻¹' {f x}) ≠ 0 → f x ∈ s
b : ℝ≥0∞
a✝ : b ∈ s
hb : b * μ (⇑f ⁻¹' {b}) ≠ 0
⊢ ∃ a, ∃ (_ : a ∈ f.range) (_ : a * μ (⇑f ⁻¹' {a}) ≠ 0), a = b

Tactic:
refine ⟨b, ?_, hb, rfl⟩

Goal state after:
case refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs : ∀ (x : α), f x ≠ 0 → μ (⇑f ⁻¹' {f x}) ≠ 0 → f x ∈ s
b : ℝ≥0∞
a✝ : b ∈ s
hb : b * μ (⇑f ⁻¹' {b}) ≠ 0
⊢ b ∈ f.range
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 α
ι : Sort u_5
inst✝ : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hι : Nonempty ι
A : MeasurableSet {b | BddAbove (range fun i ↦ f i b)}
this : Measurable fun _b ↦ sSup ∅
⊢ ∀ b ∈ {b | BddAbove (range fun i ↦ f i b)}, IsLUB {a | ∃ i, f i b = a} (⨆ i, f i b)

Tactic:
intro b hb
    apply isLUB_ciSup
    simpa

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

Goal state before:
pp: case inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
h✝ : Nonempty α
⊢ c * μ ((fun x ↦ c) ⁻¹' {c}) = c * μ univ

Tactic:
preimage_const_of_mem (mem_singleton c)

Goal state after:
case inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
h✝ : Nonempty α
⊢ c * μ univ = c * μ univ
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: μ : Measure ℝ
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : NullSingletonClass μ
b r : ℝ
hr : r < 0
⊢ 0 = μ ∅

Tactic:
measure_empty

Goal state after:
μ : Measure ℝ
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : NullSingletonClass μ
b r : ℝ
hr : r < 0
⊢ 0 = 0
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
ι : Type u_5
inst✝² : PseudoMetrizableSpace β
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) u (𝓝 (g x))
this✝¹ : MeasurableSpace β := ⋯
this✝ : BorelSpace β
v : ℕ → ι
hv : Tendsto v atTop u
t : ℕ → Set β
t_sep : ∀ (n : ℕ), IsSeparable (t n)
ht : ∀ (n : ℕ), f (v n) ⁻¹' t n ∈ ae μ
x : α
hx : ∀ (i : ℕ), f (v i) x ∈ t i
h'x : Tendsto (fun n ↦ f n x) u (𝓝 (g x))
⊢ ∀ᶠ (x_1 : ℕ) in atTop, ((fun n ↦ f n x) ∘ v) x_1 ∈ ⋃ i, t i

Tactic:
filter_upwards with n using mem_iUnion_of_mem n (hx n)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := hf.approx
h_fs_tendsto : ∀ (x : α), Tendsto (fun n ↦ (fs n) x) atTop (𝓝 (f x))
this : ∀ (n : ℕ), ∃ c, ∀ (x : α), (fs n) x = c
cs : ℕ → β := fun n ↦ ⋯.choose
h_cs_eq : ∀ (n : ℕ), ⇑(fs n) = fun x ↦ cs n
x : α
n : ℕ
| (fs n) x

Tactic:
h_cs_eq

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := hf.approx
h_fs_tendsto : ∀ (x : α), Tendsto (fun n ↦ (fs n) x) atTop (𝓝 (f x))
this : ∀ (n : ℕ), ∃ c, ∀ (x : α), (fs n) x = c
cs : ℕ → β := fun n ↦ ⋯.choose
h_cs_eq : ∀ (n : ℕ), ⇑(fs n) = fun x ↦ cs n
x : α
n : ℕ
| (fun x ↦ cs n) x
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n ↦ f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' ↦ Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i ↦ f i x
n : ℕ
⊢ ∀ ⦃b : ℕ⦄, n ≤ b → aeSeq hf p n ≤ aeSeq hf p b

Tactic:
m

Goal state after:
α : Type u_1
m✝ : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n ↦ f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' ↦ Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i ↦ f i x
n m : ℕ
⊢ n ≤ m → aeSeq hf p n ≤ aeSeq hf p m
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (a : α) ∂μ, Antitone fun i ↦ f i a
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' ↦ Antitone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i ↦ f i x
n : ℕ
⊢ ∀ ⦃b : ℕ⦄, n ≤ b → aeSeq h_meas p b ≤ aeSeq h_meas p n

Tactic:
m

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (a : α) ∂μ, Antitone fun i ↦ f i a
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' ↦ Antitone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i ↦ f i x
n m : ℕ
⊢ n ≤ m → aeSeq h_meas p m ≤ aeSeq h_meas p n
Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
g : α → ℝ≥0∞
hf_meas : ∀ (n : ℕ), Measurable (f n)
h_bound : ∀ (n : ℕ), f n ≤ᵐ[μ] g
h_fin : ∫⁻ (a : α), g a ∂μ ≠ ∞
n : ℕ
⊢ ∀ ⦃b : ℕ⦄, n ≤ b → (fun n a ↦ ⨆ i, ⨆ (_ : i ≥ n), f i a) b ≤ (fun n a ↦ ⨆ i, ⨆ (_ : i ≥ n), f i a) n

Tactic:
m

Goal state after:
case refine_2
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
g : α → ℝ≥0∞
hf_meas : ∀ (n : ℕ), Measurable (f n)
h_bound : ∀ (n : ℕ), f n ≤ᵐ[μ] g
h_fin : ∫⁻ (a : α), g a ∂μ ≠ ∞
n m : ℕ
⊢ n ≤ m → (fun n a ↦ ⨆ i, ⨆ (_ : i ≥ n), f i a) m ≤ (fun n a ↦ ⨆ i, ⨆ (_ : i ≥ n), f i a) n
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
s : Finset β
f : β → α → ℝ≥0∞
hf : ∀ b ∈ s, AEMeasurable (f b) μ
⊢ ∫⁻ (a : α), ∑ b ∈ s, f b a ∂μ = ∑ b ∈ s, ∫⁻ (a : α), f b a ∂μ

Tactic:
classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert a s has ih =>
    simp only [Finset.sum_insert has]
    rw [Finset.forall_mem_insert] at hf
    rw [lintegral_add_left' hf.1, ih hf.2]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_5
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : Tendsto f u (𝓝 g)
⊢ StronglyMeasurable g

Tactic:
borelize β
  refine stronglyMeasurable_iff_measurable_separable.2 ⟨?_, ?_⟩
  · exact measurable_of_tendsto_metrizable' u (fun i => (hf i).measurable) lim
  · rcases u.exists_seq_tendsto with ⟨v, hv⟩
    have : IsSeparable (closure (⋃ i, range (f (v i)))) :=
      .closure <| .iUnion fun i => (hf (v i)).isSeparable_range
    apply this.mono
    rintro _ ⟨x, rfl⟩
    rw [tendsto_pi_nhds] at lim
    apply mem_closure_of_tendsto ((lim x).comp hv)
    filter_upwards with n
    apply mem_iUnion_of_mem n
    exact mem_range_self _

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

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

Tactic:
refine ⟨∅, MeasurableSet.empty, by rw [Measure.restrict_empty]; infer_instance, ?_⟩

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
ι : Type u_2
l : Filter ι
inst✝ : l.IsCountablyGenerated
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, AEMeasurable (F n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
⊢ ?m.61

Tactic:
by
    rw [tendsto_atTop'] at xl
    exact xl

Goal state after:
Module: Mathlib.Topology.Perfect

Goal state before:
pp: case left
α : Type u_1
inst✝ : TopologicalSpace α
C U : Set α
hC : Perfect C
x : α
xC : x ∈ C
xU : x ∈ U
Uop : IsOpen[inst✝] U
⊢ Perfect (closure[inst✝] (U ∩ C))

pp: case right
α : Type u_1
inst✝ : TopologicalSpace α
C U : Set α
hC : Perfect C
x : α
xC : x ∈ C
xU : x ∈ U
Uop : IsOpen[inst✝] U
⊢ (closure[inst✝] (U ∩ C)).Nonempty

Tactic:
· apply Preperfect.perfect_closure
    exact hC.acc.open_inter Uop

Goal state after:
case right
α : Type u_1
inst✝ : TopologicalSpace α
C U : Set α
hC : Perfect C
x : α
xC : x ∈ C
xU : x ∈ U
Uop : IsOpen[inst✝] U
⊢ (closure[inst✝] (U ∩ C)).Nonempty