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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s✝ : Set α
h : IsCompact s✝
hμ : ∀ x ∈ s✝, μ.FiniteAtFilter (𝓝 x)
s t : Set α
hst : s ⊆ t
U : Set α
htU : U ⊇ t
hUo : IsOpen[inst✝¹] U
hU : μ U < ∞
⊢ ∃ U ⊇ s, IsOpen[inst✝¹] U ∧ μ U < ∞

Tactic:
exact ⟨U, hst.trans htU, hUo, hU⟩

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
D : ℕ → Set (Set α)
DC : ∀ (n : ℕ), D n ⊆ C
D_count : ∀ (n : ℕ), (D n).Countable
hD : ∀ (n : ℕ), ∀ s ∈ C, s ≤ᵐ[sfiniteSeq μ n] ⋃₀ D n
s : Set α
hs : s ∈ C
⊢ s ≤ᵐ[sum (sfiniteSeq μ)] ⋃₀ ⋃ n, D n

Tactic:
apply ae_sum_iff.2 (fun n ↦ (hD n s hs).trans ?_)

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
D : ℕ → Set (Set α)
DC : ∀ (n : ℕ), D n ⊆ C
D_count : ∀ (n : ℕ), (D n).Countable
hD : ∀ (n : ℕ), ∀ s ∈ C, s ≤ᵐ[sfiniteSeq μ n] ⋃₀ D n
s : Set α
hs : s ∈ C
n : ℕ
⊢ ⋃₀ D n ≤ᵐ[sfiniteSeq μ n] ⋃₀ ⋃ n, D n
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : ι → Measure α
s : Set α
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
⊢ ((sum μ).restrict s) t = (sum fun i ↦ (μ i).restrict s) t

Tactic:
simp only [sum_apply, restrict_apply, ht, ht.inter hs]

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

Goal state before:
pp: α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
s : ι → Set α
T : Set ι
hT : Countable ↑T
t : Set α
ht : MeasurableSet t
⊢ (μ.restrict (⋃ i ∈ T, s i)) t ≤ (sum fun i ↦ μ.restrict (s ↑i)) t

Tactic:
simpa [ht, inter_iUnion] using measure_biUnion_le μ hT (t ∩ s ·)

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

Goal state before:
pp: case h₂
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
s : Set α
hs : MeasurableSet s
⊢ ⋃ y ∈ s, measurableAtom y ⊆ s

Tactic:
simp only [iUnion_subset_iff]
        intro x hx
        exact measurableAtom_subset hs hx

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : SigmaFinite μ
r : ℝ≥0∞
hs : MeasurableSet s
h's : ∃ i, r < (μ.restrict (spanningSets μ i)) s
⊢ ∃ t, MeasurableSet t ∧ t ⊆ s ∧ r < μ t ∧ μ t < ∞

Tactic:
rcases h's with ⟨n, hn⟩

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : SigmaFinite μ
r : ℝ≥0∞
hs : MeasurableSet s
n : ℕ
hn : r < (μ.restrict (spanningSets μ n)) s
⊢ ∃ t, MeasurableSet t ∧ t ⊆ s ∧ r < μ t ∧ μ t < ∞
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
⊢ Filter.map f (ae (μ.restrict s)) ≤ Filter.map (s.indicator f) (ae μ)

Tactic:
intro t
  by_cases ht : (0 : β) ∈ t
  · rw [mem_map_indicator_ae_iff_mem_map_restrict_ae_of_zero_mem ht hs]
    exact id
  rw [mem_map_indicator_ae_iff_of_zero_notMem ht, mem_map_restrict_ae_iff hs]
  exact fun h => measure_mono_null (Set.inter_subset_left.trans Set.subset_union_left) h

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

Goal state before:
pp: case refine_3.refine_2
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
q : (ℕ → Prop) → Prop
htq : t = ⋃ p, if q p then countablyGeneratedAtom α p else ∅
x : α
⊢ (∃ i, ¬q i ∧ x ∈ countablyGeneratedAtom α i) → ∀ (i : ℕ → Prop), q i → x ∉ countablyGeneratedAtom α i

Tactic:
rintro ⟨p, hpq, hpx⟩ p' hqp' hx_mem
      have hpp' : p ≠ p' := by grind
      have h_disj : Disjoint (countablyGeneratedAtom α p) (countablyGeneratedAtom α p') :=
        disjoint_countablyGeneratedAtom hpp'
      grind

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

Goal state before:
pp: case refine_4
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
q : ℕ → (ℕ → Prop) → Prop
hq : ∀ (n : ℕ), t n = ⋃ p, if q n p then countablyGeneratedAtom α p else ∅
x✝ : α
⊢ x✝ ∈ ⋃ i, t i ↔ x✝ ∈ ⋃ p, if (fun p ↦ ⨆ n, q n p) p then countablyGeneratedAtom α p else ∅

Tactic:
simp [hq]

Goal state after:
case refine_4
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
q : ℕ → (ℕ → Prop) → Prop
hq : ∀ (n : ℕ), t n = ⋃ p, if q n p then countablyGeneratedAtom α p else ∅
x✝ : α
⊢ (∃ i i_1, q i i_1 ∧ x✝ ∈ countablyGeneratedAtom α i_1) ↔ ∃ i, (∃ n, q n i) ∧ x✝ ∈ countablyGeneratedAtom α i
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: case refine_2
α : 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 : ι
hi : i ∈ F
x : α
hx : x ∈ s i
⊢ (∀ i ∈ {x_1 ∈ F | x ∈ s x_1}, x ∈ s i) ∧ ∀ (i : ι), i ∈ F ∧ i ∉ {x_1 ∈ F | x ∈ s x_1} → x ∈ (s i)ᶜ

Tactic:
mem_filter

Goal state after:
case refine_2
α : 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 : ι
hi : i ∈ F
x : α
hx : x ∈ s i
⊢ (∀ (i : ι), i ∈ F ∧ x ∈ s i → x ∈ s i) ∧ ∀ (i : ι), i ∈ F ∧ ¬(i ∈ F ∧ x ∈ s i) → x ∈ (s i)ᶜ
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: case refine_2
α : 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)
hcap : tᶜ ∩ s ⊆ ⋃ n ∈ {k | ν (t' k) < μ (t' k)}, t' n
hle₂ : ν (tᶜ ∩ s) ≤ ∑' (n : ↑{k | ν (t' k) < μ (t' k)}), ν (t' ↑n)
⊢ ∑' (n : ↑{k | μ (t' k) ≤ ν (t' k)}), μ (t' ↑n) + ∑' (n : ↑{k | ν (t' k) < μ (t' k)}), ν (t' ↑n) ≤
    ∑' (n : ℕ), min (μ (t' n)) (ν (t' n))

Tactic:
have heq : {k | μ (t' k) ≤ ν (t' k)} ∪ {k | ν (t' k) < μ (t' k)} = univ := by
      ext k; simp [le_or_gt]

Goal state after:
case refine_2
α : 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)
hcap : tᶜ ∩ s ⊆ ⋃ n ∈ {k | ν (t' k) < μ (t' k)}, t' n
hle₂ : ν (tᶜ ∩ s) ≤ ∑' (n : ↑{k | ν (t' k) < μ (t' k)}), ν (t' ↑n)
heq : {k | μ (t' k) ≤ ν (t' k)} ∪ {k | ν (t' k) < μ (t' k)} = univ
⊢ ∑' (n : ↑{k | μ (t' k) ≤ ν (t' k)}), μ (t' ↑n) + ∑' (n : ↑{k | ν (t' k) < μ (t' k)}), ν (t' ↑n) ≤
    ∑' (n : ℕ), min (μ (t' n)) (ν (t' n))
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: α : Type u_5
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
s t : Set α
⊢ MeasurableSpace.generateFrom {S | ∃ l ∈ s, ∃ u ∈ t, l < u ∧ Ico l u = S} ≤ borel α

Tactic:
apply generateFrom_le
  borelize α
  rintro _ ⟨a, -, b, -, -, rfl⟩
  exact measurableSet_Ico

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s t u : Set α
⊢ hausdorffEDist s u ≤ hausdorffEDist s t + hausdorffEDist t u

Tactic:
rw [hausdorffEDist_def]
  simp only [sup_le_iff, iSup_le_iff]
  constructor
  · change ∀ x ∈ s, infEDist x u ≤ hausdorffEDist s t + hausdorffEDist t u
    exact fun x xs =>
      calc
        infEDist x u ≤ infEDist x t + hausdorffEDist t u :=
          infEDist_le_infEDist_add_hausdorffEDist
        _ ≤ hausdorffEDist s t + hausdorffEDist t u := by grw [infEDist_le_hausdorffEDist_of_mem xs]
  · change ∀ x ∈ u, infEDist x s ≤ hausdorffEDist s t + hausdorffEDist t u
    exact fun x xu =>
      calc
        infEDist x s ≤ infEDist x t + hausdorffEDist t s :=
          infEDist_le_infEDist_add_hausdorffEDist
        _ ≤ hausdorffEDist u t + hausdorffEDist t s := by grw [infEDist_le_hausdorffEDist_of_mem xu]
        _ = hausdorffEDist s t + hausdorffEDist t u := by simp [hausdorffEDist_comm, add_comm]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
hs : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
⊢ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s =
      closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t ↔
    s = t

Tactic:
hs.closure_eq,

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
hs : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
⊢ s = closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t ↔ s = t
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: α : Type u_2
inst✝ : PseudoMetricSpace α
s t : Set α
hs : IsCompact s
⊢ t ∈ 𝓝ˢ s ↔ ∃ ε > 0, thickening ε s ⊆ t

Tactic:
(hasBasis_nhdsSet_thickening hs).mem_iff

Goal state after:
α : Type u_2
inst✝ : PseudoMetricSpace α
s t : Set α
hs : IsCompact s
⊢ (∃ i, 0 < i ∧ thickening i s ⊆ t) ↔ ∃ ε > 0, thickening ε s ⊆ t
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: case he
α : 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
⊢ ∃ ε > 0, ∃ V ∈ 𝓝ˢ ∅, thickening ε (f '' V) ⊆ U

pp: case hmono
α : 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
⊢ ∀ ⦃s t : Set α⦄,
    s ⊆ t → (∃ ε > 0, ∃ V ∈ 𝓝ˢ t, thickening ε (f '' V) ⊆ U) → ∃ ε > 0, ∃ V ∈ 𝓝ˢ s, thickening ε (f '' V) ⊆ U

pp: case hunion
α : 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
⊢ ∀ ⦃s t : Set α⦄,
    (∃ ε > 0, ∃ V ∈ 𝓝ˢ s, thickening ε (f '' V) ⊆ U) →
      (∃ ε > 0, ∃ V ∈ 𝓝ˢ t, thickening ε (f '' V) ⊆ U) → ∃ ε > 0, ∃ V ∈ 𝓝ˢ (s ∪ t), thickening ε (f '' V) ⊆ U

pp: case hnhds
α : 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 ∈ K, ∃ t ∈ 𝓝[K] x, ∃ ε > 0, ∃ V ∈ 𝓝ˢ t, thickening ε (f '' V) ⊆ U

Tactic:
· use 1, by positivity, ∅, by simp, by simp

Goal state after:
case hmono
α : 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
⊢ ∀ ⦃s t : Set α⦄,
    s ⊆ t → (∃ ε > 0, ∃ V ∈ 𝓝ˢ t, thickening ε (f '' V) ⊆ U) → ∃ ε > 0, ∃ V ∈ 𝓝ˢ s, thickening ε (f '' V) ⊆ U

case hunion
α : 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
⊢ ∀ ⦃s t : Set α⦄,
    (∃ ε > 0, ∃ V ∈ 𝓝ˢ s, thickening ε (f '' V) ⊆ U) →
      (∃ ε > 0, ∃ V ∈ 𝓝ˢ t, thickening ε (f '' V) ⊆ U) → ∃ ε > 0, ∃ V ∈ 𝓝ˢ (s ∪ t), thickening ε (f '' V) ⊆ U

case hnhds
α : 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 ∈ K, ∃ t ∈ 𝓝[K] x, ∃ ε > 0, ∃ V ∈ 𝓝ˢ t, thickening ε (f '' V) ⊆ U
Module: Mathlib.Topology.Instances.Real.Lemmas

Goal state before:
pp: f : ℕ → ℝ
k : ℕ
h_ant : Antitone fun n ↦ f (n + k)
h_bdd : BddBelow (range fun x ↦ f (x + k))
⊢ Tendsto f atTop (𝓝 (sInf (f '' Ici k)))

Tactic:
rw [← tendsto_add_atTop_iff_nat k, ← range_add_eq_image_Ici, sInf_range]

Goal state after:
f : ℕ → ℝ
k : ℕ
h_ant : Antitone fun n ↦ f (n + k)
h_bdd : BddBelow (range fun x ↦ f (x + k))
⊢ Tendsto (fun n ↦ f (n + k)) atTop (𝓝 (⨅ x, f (x + k)))
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : PseudoMetrizableSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
ι : Type u_3
f : ι → α → β
g : α → β
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : Tendsto f u (𝓝 g)
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
s : Set β
h1s : IsClosed[inst✝⁵] s
h2s : s.Nonempty
⊢ s ≠ Set.univ → MeasurableSet (g ⁻¹' s)

Tactic:
h3s

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : PseudoMetrizableSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
ι : Type u_3
f : ι → α → β
g : α → β
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : Tendsto f u (𝓝 g)
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
s : Set β
h1s : IsClosed[inst✝⁵] s
h2s : s.Nonempty
h3s : s ≠ Set.univ
⊢ MeasurableSet (g ⁻¹' s)
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: ⊢ generateFrom (range fun a ↦ Iio ↑a) = generateFrom (range fun a ↦ Ici ↑a)

Tactic:
refine le_antisymm (generateFrom_le ?_) (generateFrom_le ?_) <;>
  rintro _ ⟨q, rfl⟩ <;>
  dsimp only <;>
  [rw [← compl_Ici]; rw [← compl_Iio]]

Goal state after:
case refine_1
q : ℚ
⊢ MeasurableSet (Ici ↑q)ᶜ

case refine_2
q : ℚ
⊢ MeasurableSet (Iio ↑q)ᶜ
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0
hf : Measurable f
μ : Measure α
inst✝ : SigmaFinite μ
sigma_finite_sets : ℕ → Set α := spanningSets μ
norm_sets : ℕ → Set α := fun n ↦ {x | f x ≤ ↑n}
norm_sets_spanning : ⋃ n, norm_sets n = univ
sets : ℕ → Set α := fun n ↦ sigma_finite_sets n ∩ norm_sets n
h_meas : ∀ (n : ℕ), MeasurableSet (sets n)
⊢ ∀ (n : ℕ), μ (sets n) < ∞

Tactic:
refine fun n => (measure_mono Set.inter_subset_left).trans_lt ?_

Goal state after:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0
hf : Measurable f
μ : Measure α
inst✝ : SigmaFinite μ
sigma_finite_sets : ℕ → Set α := spanningSets μ
norm_sets : ℕ → Set α := fun n ↦ {x | f x ≤ ↑n}
norm_sets_spanning : ⋃ n, norm_sets n = univ
sets : ℕ → Set α := fun n ↦ sigma_finite_sets n ∩ norm_sets n
h_meas : ∀ (n : ℕ), MeasurableSet (sets n)
n : ℕ
⊢ μ (sigma_finite_sets n) < ∞
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case neg
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_5
ι' : Type u_6
f : ι → δ → α
v : Filter ι
hf : ∀ (i : ι), Measurable (f i)
p : ι' → Prop
s : ι' → Set ι
hv : v.HasCountableBasis p s
hs : ∀ (j : ι'), (s j).Countable
this✝¹ : Countable (Subtype p)
hp : Nonempty (Subtype p)
H : ¬∃ j, s ↑j = ∅
this✝ : ∀ (i : ι'), Countable ↑(s i)
m : Subtype p → Set δ := ⋯
m_meas : ∀ (j : Subtype p), MeasurableSet (m j)
mc_meas : MeasurableSet {x | ∀ (j : Subtype p), x ∉ m j}
j : Subtype p
reparam : δ → Subtype p → Subtype p := ⋯
F0 : Subtype p → δ → α := ⋯
F0_meas : ∀ (j : Subtype p), Measurable (F0 j)
F1 : δ → α := ⋯
hF1 : F1 = fun x ↦ F0 (reparam x j) x
g : ℕ → Subtype p := ⋯
Z : ∀ (x : δ), ∃ n, x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k
this : F1 = fun x ↦ if x ∈ m j then F0 j x else F0 (g (Nat.find ⋯)) x
⊢ Measurable fun x ↦ F0 (g (Nat.find ⋯)) x

Tactic:
apply Measurable.find (fun n ↦ F0_meas (g n)) (fun n ↦ ?_)

Goal state after:
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_5
ι' : Type u_6
f : ι → δ → α
v : Filter ι
hf : ∀ (i : ι), Measurable (f i)
p : ι' → Prop
s : ι' → Set ι
hv : v.HasCountableBasis p s
hs : ∀ (j : ι'), (s j).Countable
this✝¹ : Countable (Subtype p)
hp : Nonempty (Subtype p)
H : ¬∃ j, s ↑j = ∅
this✝ : ∀ (i : ι'), Countable ↑(s i)
m : Subtype p → Set δ := fun j ↦ {x | BddBelow (range fun i ↦ f (↑i) x)}
m_meas : ∀ (j : Subtype p), MeasurableSet (m j)
mc_meas : MeasurableSet {x | ∀ (j : Subtype p), x ∉ m j}
j : Subtype p
reparam : δ → Subtype p → Subtype p := fun x ↦ liminfReparam (fun i ↦ f i x) s p
F0 : Subtype p → δ → α := fun j x ↦ ⨅ i, f (↑i) x
F0_meas : ∀ (j : Subtype p), Measurable (F0 j)
F1 : δ → α := fun x ↦ F0 (reparam x j) x
hF1 : F1 = fun x ↦ F0 (reparam x j) x
g : ℕ → Subtype p := Classical.choose ⋯
Z : ∀ (x : δ), ∃ n, x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k
this : F1 = fun x ↦ if x ∈ m j then F0 j x else F0 (g (Nat.find ⋯)) x
n : ℕ
⊢ MeasurableSet {x | x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k}
Module: Mathlib.MeasureTheory.Function.SimpleFuncDense

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : PseudoEMetricSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace β
f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
x : β
n : ℕ
⊢ edist y₀ (f x) + edist ((approxOn f hf s y₀ h₀ n) x) (f x) ≤ edist y₀ (f x) + edist y₀ (f x)

Tactic:
by grw [edist_approxOn_le hf h₀ x n]

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

Goal state before:
pp: α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
M : Type u_5
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
l : List (α → M)
hl : ∀ f ∈ l, AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable l.prod μ

Tactic:
by
  induction l with
  | nil => exact aestronglyMeasurable_one
  | cons f l ihl =>
    rw [List.forall_mem_cons] at hl
    rw [List.prod_cons]
    exact hl.1.mul (ihl hl.2)

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : α → ℝ≥0∞ := fun a ↦ ⨆ n, f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), ↑(s x) ≤ ⨆ n, f n x
r : ℝ≥0
right✝ ha✝ : ↑r < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun a ↦ r * a) s
eq_rs : SimpleFunc.map c rs = const α ↑r * SimpleFunc.map c s
p : ℝ≥0∞
⊢ ⇑(SimpleFunc.map c rs) ⁻¹' {p} = ⇑(SimpleFunc.map c rs) ⁻¹' {p} ∩ ⋃ i, {a | p ≤ f i a}

Tactic:
← inter_univ (map c rs ⁻¹' {p})

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : α → ℝ≥0∞ := fun a ↦ ⨆ n, f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), ↑(s x) ≤ ⨆ n, f n x
r : ℝ≥0
right✝ ha✝ : ↑r < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun a ↦ r * a) s
eq_rs : SimpleFunc.map c rs = const α ↑r * SimpleFunc.map c s
p : ℝ≥0∞
⊢ ⇑(SimpleFunc.map c rs) ⁻¹' {p} ∩ univ = ⇑(SimpleFunc.map c rs) ⁻¹' {p} ∩ ⋃ i, {a | p ≤ f i a}
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∫⁻ (a : α), f a ∂μ = 0
ε : ℝ≥0∞
εpos : ε > 0
h' : μ {x | ε ≤ f x} ≠ 0
⊢ False

Tactic:
refine ((ENNReal.mul_pos εpos.ne' h').trans_le ?_).ne' h

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∫⁻ (a : α), f a ∂μ = 0
ε : ℝ≥0∞
εpos : ε > 0
h' : μ {x | ε ≤ f x} ≠ 0
⊢ ε * μ {x | ε ≤ f x} ≤ ∫⁻ (a : α), f a ∂μ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : Function.support f ⊆ s
x : α
h : x ∉ s
⊢ f x = 0

Tactic:
exact Function.support_subset_iff'.1 hsf x h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
s : β → Set α
f : α → ℝ≥0∞
⊢ ∫⁻ (a : α) in ⋃ i, s i, f a ∂μ ≤ ∑' (i : β), ∫⁻ (a : α) in s i, f a ∂μ

Tactic:
rw [← lintegral_sum_measure]

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
s : β → Set α
f : α → ℝ≥0∞
⊢ ∫⁻ (a : α) in ⋃ i, s i, f a ∂μ ≤ ∫⁻ (a : α), f a ∂sum fun i ↦ μ.restrict (s i)
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

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

Tactic:
by
  refine le_antisymm ?_ (le_lintegral_add _ _)
  rcases exists_measurable_le_lintegral_eq μ fun a => f a + g a with ⟨φ, hφm, hφ_le, hφ_eq⟩
  calc
    ∫⁻ a, f a + g a ∂μ = ∫⁻ a, φ a ∂μ := hφ_eq
    _ ≤ ∫⁻ a, f a + (φ a - f a) ∂μ := lintegral_mono fun a => le_add_tsub
    _ = ∫⁻ a, f a ∂μ + ∫⁻ a, φ a - f a ∂μ := lintegral_add_aux hf (hφm.sub hf)
    _ ≤ ∫⁻ a, f a ∂μ + ∫⁻ a, g a ∂μ := by gcongr with a; exact tsub_le_iff_left.2 <| hφ_le _

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

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

Tactic:
simp_rw [this]

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

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

Tactic:
rw [lintegral_add_left' hf.1, ih hf.2]

Goal state after: