mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: case a
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s t : Set α
ht : P t
hs : s ⊆ t
⊢ (inducedOuterMeasure m P0 m0) s ≤ m t ht

Tactic:
hs

Goal state after:
case a
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s t : Set α
ht : P t
hs : s ⊆ t
⊢ (inducedOuterMeasure m P0 m0) t ≤ m t ht
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
d : DynkinSystem α
s : Set α
h : d.Has s
f : ℕ → Set α
hd : Pairwise (Disjoint on f)
hf : ∀ (i : ℕ), d.Has (f i ∩ s)
⊢ Pairwise (Disjoint on fun i ↦ f i ∩ s)

Tactic:
exact hd.mono fun i j => Disjoint.mono inter_subset_left inter_subset_left

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_2
m : OuterMeasure α
m0 m1 : MeasurableSpace α
h : m0 ≤ m1
s : Set α
⊢ MeasurableSet s → m.trim s ≤ m s

Tactic:
hs

Goal state after:
α : Type u_2
m : OuterMeasure α
m0 m1 : MeasurableSpace α
h : m0 ≤ m1
s : Set α
hs : MeasurableSet s
⊢ m.trim s ≤ m s
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
hs : ¬ms = ∞
r : ℝ≥0∞
⊢ r > ms → ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t < r

Tactic:
hs

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
hs✝ : ¬ms = ∞
r : ℝ≥0∞
hs : r > ms
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t < r
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet (⇑(Equiv.Set.rangeInr α β) ⁻¹' s)

Tactic:
refine ⟨_, hs.inr_image, Set.ext ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
s : Set β
hs : MeasurableSet s
⊢ ∀ (x : { x // x ∈ range Sum.inr }), x ∈ Subtype.val ⁻¹' Sum.inr '' s ↔ x ∈ ⇑(Equiv.Set.rangeInr α β) ⁻¹' s
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
x : α
⊢ hf.equivRange.symm ⟨f x, ⋯⟩ = hf.equivRange.symm (hf.equivRange x)

Tactic:
rw [hf.equivRange_apply]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
s : Set β
⊢ MeasurableSet s → (map f μ).toOuterMeasure s = ((OuterMeasure.map f) μ.toOuterMeasure) s

Tactic:
hs

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
s : Set β
hs : MeasurableSet s
⊢ (map f μ).toOuterMeasure s = ((OuterMeasure.map f) μ.toOuterMeasure) s
Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : ∀ ⦃s : Set α⦄, MeasurableSet s → ν s = 0 → μ s = 0
s : Set α
⊢ ν s = 0 → μ s = 0

Tactic:
hs

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : ∀ ⦃s : Set α⦄, MeasurableSet s → ν s = 0 → μ s = 0
s : Set α
hs : ν s = 0
⊢ μ s = 0
Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν ν' : Measure α
h1 : μ₁ ≪ ν
h2 : μ₂ ≪ ν'
s : Set α
⊢ (ν + ν') s = 0 → (μ₁ + μ₂) s = 0

Tactic:
hs

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν ν' : Measure α
h1 : μ₁ ≪ ν
h2 : μ₂ ≪ ν'
s : Set α
hs : (ν + ν') s = 0
⊢ (μ₁ + μ₂) s = 0
Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h1 : μ ≪ ν
ν' : Measure α
s : Set α
⊢ (ν + ν') s = 0 → μ s = 0

Tactic:
hs

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h1 : μ ≪ ν
ν' : Measure α
s : Set α
hs : (ν + ν') s = 0
⊢ μ s = 0
Module: Mathlib.MeasureTheory.OuterMeasure.BorelCantelli

Goal state before:
pp: α : Type u_1
ι : Type u_2
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
inst✝ : Countable ι
μ : F
s : ι → Set α
hs : ∑' (i : ι), μ (s i) ≠ ∞
t : Finset ι
⊢ μ (limsup s cofinite) ≤ ∑' (b : { x // x ∉ t }), μ (s ↑b)

Tactic:
calc
    μ (limsup s cofinite) ≤ μ (⋃ i : {i // i ∉ t}, s i) := by
      gcongr
      rw [hasBasis_cofinite.limsup_eq_iInf_iSup, iUnion_subtype]
      exact iInter₂_subset _ t.finite_toSet
    _ ≤ ∑' i : {i // i ∉ t}, μ (s i) := measure_iUnion_le _

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β
g : β → γ
hf' : ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)
hg : Injective g
hg' : ∀ (s : Set β), MeasurableSet s → MeasurableSet (g '' s)
μ : Measure γ
hf : ¬Injective f
⊢ 0 =
    if hf : Injective (g ∘ f) ∧ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (g ∘ f '' s) μ then
      ((OuterMeasure.comap (g ∘ f)) μ.toOuterMeasure).toMeasure ⋯
    else 0

Tactic:
dif_neg fun h ↦ hf h.1.of_comp

Goal state after:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β
g : β → γ
hf' : ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)
hg : Injective g
hg' : ∀ (s : Set β), MeasurableSet s → MeasurableSet (g '' s)
μ : Measure γ
hf : ¬Injective f
⊢ 0 = 0
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
⊢ ⋃ i, accumulate μ.toFiniteSpanningSetsIn.set i = univ

Tactic:
iUnion_accumulate,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
⊢ ⋃ x, μ.toFiniteSpanningSetsIn.set x = univ
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : s ⊆ t
⊢ (μ.restrict t).restrict s = μ.restrict s

Tactic:
ext1 u hu

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : s ⊆ t
u : Set α
hu : MeasurableSet u
⊢ ((μ.restrict t).restrict s) u = (μ.restrict s) u
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t s : Set α
ht : NullMeasurableSet t μ
⊢ μ.restrict (s ∩ t) + μ.restrict (s \ t) = μ.restrict s

Tactic:
ext1 u hu

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t s : Set α
ht : NullMeasurableSet t μ
u : Set α
hu : MeasurableSet u
⊢ (μ.restrict (s ∩ t) + μ.restrict (s \ t)) u = (μ.restrict s) u
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
t : Set α
ht : MeasurableSet t
⊢ (μ.restrict (⋃ i, s i)) t = ⨆ i, (μ.restrict (s i)) t

Tactic:
by
  simp only [restrict_apply ht, inter_iUnion]
  rw [Directed.measure_iUnion]
  exacts [hd.mono_comp _ fun s₁ s₂ => inter_subset_inter_right _]

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : μ.restrict s = ν.restrict s
ht : μ.restrict t = ν.restrict t
⊢ μ.restrict (s ∪ t) = ν.restrict (s ∪ t)

Tactic:
ext1 u hu

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : μ.restrict s = ν.restrict s
ht : μ.restrict t = ν.restrict t
u : Set α
hu : MeasurableSet u
⊢ (μ.restrict (s ∪ t)) u = (ν.restrict (s ∪ t)) u
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
x : α
s : Set α
xs : x ∈ s
⊢ IsOpen[inst✝¹] s → ∃ v ∈ {s | IsOpen[inst✝¹] s ∧ μ s < ∞}, x ∈ v ∧ v ⊆ s

Tactic:
hs

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
x : α
s : Set α
xs : x ∈ s
hs : IsOpen[inst✝¹] s
⊢ ∃ v ∈ {s | IsOpen[inst✝¹] s ∧ μ s < ∞}, x ∈ v ∧ v ⊆ s
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
m : ℝ≥0∞ := ⋯
hm : ⊥ < m
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 m
u_lim : Tendsto u atTop (𝓝 m)
D : ℕ → Set (Set α)
D_mem : ∀ (n : ℕ), D n ∈ {D | D ⊆ C ∧ D.Countable}
huD : ∀ (n : ℕ), u n < μ (⋃₀ D n)
hD : ⋃ n, D n ∈ {D | D ⊆ C ∧ D.Countable}
⊢ ⨆ i ∈ {D | D ⊆ C ∧ D.Countable}, μ (⋃₀ i) ≤ μ (⋃₀ ⋃ n, D n)

Tactic:
apply le_of_tendsto' u_lim (fun n ↦ (huD n).le.trans ?_)

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
m : ℝ≥0∞ := ⨆ D ∈ {D | D ⊆ C ∧ D.Countable}, μ (⋃₀ D)
hm : ⊥ < m
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 m
u_lim : Tendsto u atTop (𝓝 m)
D : ℕ → Set (Set α)
D_mem : ∀ (n : ℕ), D n ∈ {D | D ⊆ C ∧ D.Countable}
huD : ∀ (n : ℕ), u n < μ (⋃₀ D n)
hD : ⋃ n, D n ∈ {D | D ⊆ C ∧ D.Countable}
n : ℕ
⊢ μ (⋃₀ D n) ≤ μ (⋃₀ ⋃ n, D n)
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_8
ι : Type u_9
x✝ : MeasurableSpace α
μ : Measure α
inst✝¹ : SemilatticeSup ι
inst✝ : Countable ι
f : ι → Set α
hm : ∀ (i : ι), NullMeasurableSet (f i) μ
ε : ℝ≥0∞
hε : 0 < ε
hfin : ∃ i, μ (f i) ≠ ∞
hfem : ⋂ n, f n = ∅
F : ι → ℝ≥0∞ := fun m ↦ μ (⋂ n, ⋂ (_ : n ≤ m), f n)
hFAnti : Antitone F
this : Tendsto F atTop (𝓝 0)
⊢ ∃ m, μ (⋂ n, ⋂ (_ : n ≤ m), f n) < ε

Tactic:
let _ := hfin.nonempty

Goal state after:
α : Type u_8
ι : Type u_9
x✝¹ : MeasurableSpace α
μ : Measure α
inst✝¹ : SemilatticeSup ι
inst✝ : Countable ι
f : ι → Set α
hm : ∀ (i : ι), NullMeasurableSet (f i) μ
ε : ℝ≥0∞
hε : 0 < ε
hfin : ∃ i, μ (f i) ≠ ∞
hfem : ⋂ n, f n = ∅
F : ι → ℝ≥0∞ := fun m ↦ μ (⋂ n, ⋂ (_ : n ≤ m), f n)
hFAnti : Antitone F
this : Tendsto F atTop (𝓝 0)
x✝ : Nonempty ι := Exists.nonempty hfin
⊢ ∃ m, μ (⋂ n, ⋂ (_ : n ≤ m), f n) < ε
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
⊢ ∃ D ⊆ C, D.Countable ∧ ∀ s ∈ C, s ≤ᵐ[μ] ⋃₀ D

Tactic:
by
  let m := ⨆ D ∈ {D : Set (Set α) | D ⊆ C ∧ D.Countable}, μ (⋃₀ D)
  obtain ⟨D, D_mem, hD⟩ : ∃ D ∈ {D : Set (Set α) | D ⊆ C ∧ D.Countable}, μ (⋃₀ D) = m := by
    rcases eq_bot_or_bot_lt m with hm | hm
    · exact ⟨∅, by simp, by simp [hm]⟩
    obtain ⟨u, -, u_mem, u_lim⟩ :
        ∃ u : ℕ → ℝ≥0∞, StrictMono u ∧ (∀ n, u n ∈ Ioo 0 m) ∧ Tendsto u atTop (𝓝 m) :=
      exists_seq_strictMono_tendsto' hm
    have A n : ∃ D ∈ {D : Set (Set α) | D ⊆ C ∧ D.Countable}, u n < μ (⋃₀ D) :=
      lt_biSup_iff.1 (u_mem n).2
    choose! D D_mem huD using A
    have hD : ⋃ n, D n ∈ {D | D ⊆ C ∧ D.Countable} := by simp; grind
    refine ⟨⋃ n, D n, hD, ?_⟩
    apply le_antisymm (le_biSup (f := fun D ↦ μ (⋃₀ D)) hD)
    apply le_of_tendsto' u_lim (fun n ↦ (huD n).le.trans ?_)
    exact measure_mono (fun x hx ↦ by simp at hx ⊢; grind)
  refine ⟨D, by grind, by grind, fun s hs ↦ union_ae_eq_right_iff_ae_subset.mp ?_⟩
  symm
  apply ae_eq_of_ae_subset_of_measure_ge subset_union_right.eventuallyLE
  · rw [hD, show s ∪ ⋃₀ D = ⋃₀ (D ∪ {s}) by simp]
    apply le_biSup (f := fun D ↦ μ (⋃₀ D))
    simp [D_mem.2, insert_subset_iff, hs, D_mem.1]
  · exact (MeasurableSet.sUnion D_mem.2 (by grind)).nullMeasurableSet
  · simp

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S T : Set (Set α)
h_gen : m0 = generateFrom S
hc : T.Countable
h_inter : IsPiSystem S
hU : ⋃₀ T = univ
htop : ∀ t ∈ T, μ t ≠ ∞
ST_eq : ∀ t ∈ T, ∀ s ∈ S, μ (s ∩ t) = ν (s ∩ t)
T_eq : ∀ t ∈ T, μ t = ν t
t : Set α
ht : t ∈ T
⊢ μ.restrict t = ν.restrict t

Tactic:
ext1 u hu

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S T : Set (Set α)
h_gen : m0 = generateFrom S
hc : T.Countable
h_inter : IsPiSystem S
hU : ⋃₀ T = univ
htop : ∀ t ∈ T, μ t ≠ ∞
ST_eq : ∀ t ∈ T, ∀ s ∈ S, μ (s ∩ t) = ν (s ∩ t)
T_eq : ∀ t ∈ T, μ t = ν t
t : Set α
ht : t ∈ T
u : Set α
hu : MeasurableSet u
⊢ (μ.restrict t) u = (ν.restrict t) u
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_8
inst✝³ : LinearOrder ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
s : ι → Set α
a : ι
hs : ∀ r > a, NullMeasurableSet (s r) μ
hm : ∀ (i j : ι), a < i → i ≤ j → s i ⊆ s j
hf : ∃ r > a, μ (s r) ≠ ∞
ha : ¬Order.IsPredPrelimit a
⊢ Tendsto (⇑μ ∘ s) (𝓝[>] a) (𝓝 (μ (⋂ r, ⋂ (_ : r > a), s r)))

Tactic:
· rw [Order.not_isPredPrelimit_iff] at ha
    rcases ha with ⟨b, hab⟩
    simp [hab.nhdsGT]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
inst✝ : Countable α
μ ν : Measure α
h : ∀ (x : α), μ (measurableAtom x) = ν (measurableAtom x)
s : Set α
hs : MeasurableSet s
h1 : s = ⋃₀ (measurableAtom '' s)
h_count : (measurableAtom '' s).Countable
t t' : Set α
h_eq : t ≠ t'
y : α
hys : y ∈ s
hy : measurableAtom y = t
y' : α
hy's : y' ∈ s
hy' : measurableAtom y' = t'
⊢ Disjoint t t'

Tactic:
← hy,

Goal state after:
α : Type u_1
m : MeasurableSpace α
inst✝ : Countable α
μ ν : Measure α
h : ∀ (x : α), μ (measurableAtom x) = ν (measurableAtom x)
s : Set α
hs : MeasurableSet s
h1 : s = ⋃₀ (measurableAtom '' s)
h_count : (measurableAtom '' s).Countable
t t' : Set α
y : α
h_eq : measurableAtom y ≠ t'
hys : y ∈ s
hy : measurableAtom y = t
y' : α
hy's : y' ∈ s
hy' : measurableAtom y' = t'
⊢ Disjoint (measurableAtom y) t'
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S T : Set (Set α)
h_gen : m0 = generateFrom S
h_inter : IsPiSystem S
h_sub : T ⊆ S
hc : T.Countable
hU : ⋃₀ T = univ
htop : ∀ s ∈ T, μ s ≠ ∞
h_eq : ∀ s ∈ S, μ s = ν s
t : Set α
ht : t ∈ T
s : Set α
⊢ s ∈ S → μ (s ∩ t) = ν (s ∩ t)

Tactic:
hs

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S T : Set (Set α)
h_gen : m0 = generateFrom S
h_inter : IsPiSystem S
h_sub : T ⊆ S
hc : T.Countable
hU : ⋃₀ T = univ
htop : ∀ s ∈ T, μ s ≠ ∞
h_eq : ∀ s ∈ S, μ s = ν s
t : Set α
ht : t ∈ T
s : Set α
hs : s ∈ S
⊢ μ (s ∩ t) = ν (s ∩ t)
Module: Mathlib.Data.Set.MemPartition

Goal state before:
pp: case zero
α : Type u_1
f : ℕ → Set α
u v : Set α
huv : u ≠ v
hu : u = univ
hv : v = univ
⊢ Disjoint u v

Tactic:
hu,

Goal state after:
case zero
α : Type u_1
f : ℕ → Set α
u v : Set α
huv : univ ≠ v
hu : u = univ
hv : v = univ
⊢ Disjoint u v
Module: Mathlib.Order.Filter.CountableSeparatingOn

Goal state before:
pp: α : Type u_1
l : Filter α
inst✝¹ : CountableInterFilter l
p : Set α → Prop
s : Set α
inst✝ : HasCountableSeparatingOn α p s
hs : s ∈ l
hne : s.Nonempty
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
t : Set α
hts : t ⊆ s
ht : t.Subsingleton
htl : t ∈ l
⊢ ∃ a ∈ s, {a} ∈ l

Tactic:
rcases ht.eq_empty_or_singleton with rfl | ⟨x, rfl⟩

Goal state after:
case inl
α : Type u_1
l : Filter α
inst✝¹ : CountableInterFilter l
p : Set α → Prop
s : Set α
inst✝ : HasCountableSeparatingOn α p s
hs : s ∈ l
hne : s.Nonempty
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
hts : ∅ ⊆ s
ht : ∅.Subsingleton
htl : ∅ ∈ l
⊢ ∃ a ∈ s, {a} ∈ l

case inr
α : Type u_1
l : Filter α
inst✝¹ : CountableInterFilter l
p : Set α → Prop
s : Set α
inst✝ : HasCountableSeparatingOn α p s
hs : s ∈ l
hne : s.Nonempty
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
x : α
hts : {x} ⊆ s
ht : {x}.Subsingleton
htl : {x} ∈ l
⊢ ∃ a ∈ s, {a} ∈ l
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: case refine_2
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set α
h : NullMeasurableSet (t ∩ s) μ
A : NullMeasurableSet (t \ s) (μ.restrict s)
⊢ NullMeasurableSet t (μ.restrict s)

Tactic:
have B : NullMeasurableSet (t ∩ s) (μ.restrict s) :=
      h.mono_ac absolutelyContinuous_restrict

Goal state after:
case refine_2
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set α
h : NullMeasurableSet (t ∩ s) μ
A : NullMeasurableSet (t \ s) (μ.restrict s)
B : NullMeasurableSet (t ∩ s) (μ.restrict s)
⊢ NullMeasurableSet t (μ.restrict s)
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
s : Set α
⊢ MeasurableSet s → MeasurableSet s

Tactic:
hs

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet s
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
⊢ MeasurableSet s → (countablyGeneratedAtom α fun x_1 ↦ x ∈ A x_1) ⊆ s

Tactic:
hs

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 α
hxs : x ∈ s
hs : MeasurableSet s
⊢ (countablyGeneratedAtom α fun x_1 ↦ x ∈ A x_1) ⊆ s
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : 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 ∅
this : q fun x_1 ↦ x ∈ A x_1
⊢ (countablyGeneratedAtom α fun x_1 ↦ x ∈ A x_1) ⊆ s

Tactic:
hq

Goal state after:
α : 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 ∅
this : q fun x_1 ↦ x ∈ A x_1
⊢ (countablyGeneratedAtom α fun x_1 ↦ x ∈ A x_1) ⊆ ⋃ p, if q p then countablyGeneratedAtom α p else ∅
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case refine_2
α : Type u_1
m : MeasurableSpace α
b : Set (Set α)
bct : b.Countable
hbm : ∀ s ∈ b, MeasurableSet s
hb : ∀ x ∈ univ, ∀ y ∈ univ, (∀ s ∈ b, x ∈ s ↔ y ∈ s) → x = y
⊢ SeparatesPoints α

Tactic:
@separatesPoints_iff

Goal state after:
case refine_2
α : Type u_1
m : MeasurableSpace α
b : Set (Set α)
bct : b.Countable
hbm : ∀ s ∈ b, MeasurableSet s
hb : ∀ x ∈ univ, ∀ y ∈ univ, (∀ s ∈ b, x ∈ s ↔ y ∈ s) → x = y
⊢ ∀ (x y : α), (∀ (s : Set α), MeasurableSet s → (x ∈ s ↔ y ∈ s)) → x = y
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
⊢ s ∈ ae μ → s ∈ μ.cofinite

Tactic:
hs

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : s ∈ ae μ
⊢ s ∈ μ.cofinite
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: α : Type u_1
s : Set (Set α)
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
hs : t = TopologicalSpace.generateFrom s
u : Set α
hu : TopologicalSpace.IsOpen u
⊢ MeasurableSet u

Tactic:
hs

Goal state after:
α : Type u_1
s : Set (Set α)
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
hs : t = TopologicalSpace.generateFrom s
u : Set α
hu : TopologicalSpace.IsOpen u
⊢ MeasurableSet u
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: α : Type u_1
s : Set (Set α)
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
hs : t = TopologicalSpace.generateFrom s
u : Set α
f : Set (Set α)
hf : ∀ s_1 ∈ f, GenerateOpen s s_1
ih : ∀ s_1 ∈ f, MeasurableSet s_1
⊢ ∀ s ∈ f, IsOpen[t] s

Tactic:
hs

Goal state after:
α : Type u_1
s : Set (Set α)
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
hs : t = TopologicalSpace.generateFrom s
u : Set α
f : Set (Set α)
hf : ∀ s_1 ∈ f, GenerateOpen s s_1
ih : ∀ s_1 ∈ f, MeasurableSet s_1
⊢ ∀ s_1 ∈ f, IsOpen[TopologicalSpace.generateFrom s] s_1
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: α : Type u_1
s : Set (Set α)
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
hs : t = TopologicalSpace.generateFrom s
u : Set α
hu : u ∈ s
⊢ TopologicalSpace.IsOpen u

Tactic:
hs

Goal state after:
α : Type u_1
s : Set (Set α)
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
hs : t = TopologicalSpace.generateFrom s
u : Set α
hu : u ∈ s
⊢ TopologicalSpace.IsOpen u
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: M : Type u_2
α : Type u_4
inst✝² : CommMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
l : Multiset (α → M)
hl : ∀ f ∈ l, Measurable f
⊢ Measurable l.prod

Tactic:
rcases l with ⟨l⟩

Goal state after:
case mk
M : Type u_2
α : Type u_4
inst✝² : CommMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
l✝ : Multiset (α → M)
l : List (α → M)
hl : ∀ f ∈ Quot.mk (⇑(List.isSetoid (α → M))) l, Measurable f
⊢ Measurable (prod (Quot.mk (⇑(List.isSetoid (α → M))) l))
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: M : Type u_2
α : Type u_4
inst✝² : CommMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
l : Multiset (α → M)
hl : ∀ f ∈ l, AEMeasurable f μ
⊢ AEMeasurable l.prod μ

Tactic:
rcases l with ⟨l⟩

Goal state after:
case mk
M : Type u_2
α : Type u_4
inst✝² : CommMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
l✝ : Multiset (α → M)
l : List (α → M)
hl : ∀ f ∈ Quot.mk (⇑(List.isSetoid (α → M))) l, AEMeasurable f μ
⊢ AEMeasurable (prod (Quot.mk (⇑(List.isSetoid (α → M))) l)) μ
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: γ : Type u_3
δ : Type u_5
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
inst✝ : MeasurableSpace δ
f : δ → γ
hf : ∀ (s : Set γ), IsClosed[inst✝³] s → MeasurableSet (f ⁻¹' s)
s : Set γ
⊢ IsOpen[inst✝³] s → MeasurableSet (f ⁻¹' s)

Tactic:
hs

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

Goal state before:
pp: γ : 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 γ
⊢ IsClosed[inst✝³] s → MeasurableSet (f ⁻¹' s)

Tactic:
hs

Goal state after:
γ : 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
⊢ MeasurableSet (f ⁻¹' s)