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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s t : Set α
hs : μ s ≠ ∞
ht : μ t ≠ ∞
⊢ μ (s ∪ t) ≠ ∞

Tactic:
by finiteness

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
C : Set (Set α)
s : Set α
⊢ GenerateHas C sᶜ ↔ GenerateHas C s

Tactic:
by
  refine ⟨?_, GenerateHas.compl⟩
  intro h
  convert! GenerateHas.compl h
  simp

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
m : MeasurableSpace α
C : (s : Set α) → MeasurableSet s → Prop
s : Set (Set α)
h_eq : m = generateFrom s
h_inter : IsPiSystem s
empty : C ∅ ⋯
basic : ∀ (t : Set α) (ht : t ∈ s), C t ⋯
compl : ∀ (t : Set α) (htm : MeasurableSet t), C t htm → C tᶜ ⋯
iUnion :
  ∀ (f : ℕ → Set α),
    Pairwise (Disjoint on f) → ∀ (hfm : ∀ (i : ℕ), MeasurableSet (f i)), (∀ (i : ℕ), C (f i) ⋯) → C (⋃ i, f i) ⋯
⊢ MeasurableSet = DynkinSystem.GenerateHas s

Tactic:
DynkinSystem.generateFrom_eq h_inter

Goal state after:
α : Type u_3
m : MeasurableSpace α
C : (s : Set α) → MeasurableSet s → Prop
s : Set (Set α)
h_eq : m = generateFrom s
h_inter : IsPiSystem s
empty : C ∅ ⋯
basic : ∀ (t : Set α) (ht : t ∈ s), C t ⋯
compl : ∀ (t : Set α) (htm : MeasurableSet t), C t htm → C tᶜ ⋯
iUnion :
  ∀ (f : ℕ → Set α),
    Pairwise (Disjoint on f) → ∀ (hfm : ∀ (i : ℕ), MeasurableSet (f i)), (∀ (i : ℕ), C (f i) ⋯) → C (⋃ i, f i) ⋯
⊢ MeasurableSet = DynkinSystem.GenerateHas s
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

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

Tactic:
have : ∀ r > ms, ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t < r := by
      intro r hs
      have : ∃ t, MeasurableSet t ∧ s ⊆ t ∧ m t < r := by simpa [ms, iInf_lt_iff] using hs
      rcases this with ⟨t, hmt, hin, hlt⟩
      exists t

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

Goal state before:
pp: case refine_1
α✝ : 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 γ✝
α : Type ?u.23
β : Type ?u.25
γ : Type ?u.102
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
⊢ Measurable fun a ↦ (Equiv.sumProdDistrib α β γ) ↑a

Tactic:
refine (Set.prod (range Sum.inl) univ).symm.measurable_comp_iff.1 ?_
      refine (prodCongr Set.rangeInl (Set.univ _)).symm.measurable_comp_iff.1 ?_
      exact measurable_inl

Goal state after:
Module: Mathlib.Order.Interval.Set.Monotone

Goal state before:
pp: case neg.inl
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : OrderBot α
n : α
φ : α → α
k : α
ih : StrictMonoOn φ (Iic k) → ∀ m ≤ k, m ≤ φ m
hφ : StrictMonoOn φ (Iic (succ k))
hk : ¬IsMax k
hm : succ k ≤ succ k
⊢ succ k ≤ φ (succ k)

Tactic:
specialize ih (StrictMonoOn.mono hφ fun x hx => le_trans hx (le_succ _)) k le_rfl

Goal state after:
case neg.inl
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : OrderBot α
n : α
φ : α → α
k : α
ih : k ≤ φ k
hφ : StrictMonoOn φ (Iic (succ k))
hk : ¬IsMax k
hm : succ k ≤ succ k
⊢ succ k ≤ φ (succ k)
Module: Mathlib.MeasureTheory.Measure.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
e : α ≃ᵐ β
⊢ Injective (map ⇑e)

Tactic:
intro μ₁ μ₂ hμ
  apply_fun Measure.map e.symm at hμ
  simpa [map_symm_map e] using hμ

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s✝ : Set α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : Injective f ∧ ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)
μ : Measure β
s : Set α
hs : MeasurableSet s
t : Set α
⊢ μ.toOuterMeasure (f '' t) = μ.toOuterMeasure (f '' t ∩ f '' s) + μ.toOuterMeasure (f '' t \ f '' s)

Tactic:
apply le_toOuterMeasure_caratheodory

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ : Set α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : Injective f ∧ ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)
μ : Measure β
s : Set α
hs : MeasurableSet s
t : Set α
⊢ MeasurableSet (f '' s)
Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving

Goal state before:
pp: case succ
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → α
hf : QuasiMeasurePreserving f μ μ
hs : f ⁻¹' s =ᵐ[μ] s
k : ℕ
ih : f^[k] ⁻¹' s =ᵐ[μ] s
⊢ f ⁻¹' f^[k] ⁻¹' s =ᵐ[μ] s

Tactic:
exact EventuallyEq.trans (hf.preimage_ae_eq ih) hs

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝ : IsFiniteMeasure μ
hs : MeasurableSet s
ht : MeasurableSet t
ε : ℝ≥0∞
h : μ s ≤ μ t + ε
⊢ μ t ≠ ∞

Tactic:
by finiteness

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝ : IsFiniteMeasure μ
hs : MeasurableSet s
ht : MeasurableSet t
ε : ℝ≥0∞
h : μ s ≤ μ t + ε
⊢ μ s ≠ ∞

Tactic:
by finiteness

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
⊢ μ univ ≠ ∞

Tactic:
by finiteness

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
hμν : μ ≤ ν
s : Set α
h_univ : μ s + μ sᶜ = ν s + ν sᶜ
hs : MeasurableSet s
x✝ : s.Nonempty
h_lt : μ s < ν s
h_disj : Disjoint s sᶜ
⊢ μ sᶜ ≠ ∞

Tactic:
by finiteness

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : IsFiniteMeasure μ
hs : NullMeasurableSet s μ
h : μ s = μ univ
⊢ μ univ ≠ ∞

Tactic:
by finiteness

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

Goal state before:
pp: α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsCodirectedOrder ι
inst✝ : atBot.IsCountablyGenerated
s : ι → Set α
hs : Monotone s
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
hfin : ∃ i, μ (s i) ≠ ∞
this : Nonempty ι
x : ℕ → ι
hxm : Antitone x
hx : Tendsto x atTop atBot
i : ι
n : ℕ
hn : x n ≤ i
⊢ ∃ i_1, s (x i_1) ⊆ s i

Tactic:
exact ⟨n, hs hn⟩

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hs' : μ s ≠ ∞
ht' : μ t ≠ ∞
hst : μ (s \ t) ≠ ∞
hts : μ (t \ s) ≠ ∞
⊢ μ (s ∪ t) ≠ ∞

Tactic:
by finiteness

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hs' : μ s ≠ ∞
ht' : μ t ≠ ∞
hst : μ (s \ t) ≠ ∞
hts : μ (t \ s) ≠ ∞
⊢ μ (t ∪ s) ≠ ∞

Tactic:
by finiteness

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝ : IsFiniteMeasure μ
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
⊢ μ s ≠ ∞

Tactic:
by finiteness

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝ : IsFiniteMeasure μ
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
⊢ μ t ≠ ∞

Tactic:
by finiteness

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

Goal state before:
pp: α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ✝ ν ν₁ ν₂ : Measure α
s t✝ : Set α
inst✝ : TopologicalSpace α
μ : Measure α
hμ : IsLocallyFiniteMeasure μ
x : α
t : Set α
ht : t ∈ 𝓝 x
hmus : μ t < ∞
⊢ (μ.restrict s).FiniteAtFilter (𝓝 x)

Tactic:
exact ⟨t, ht, lt_of_le_of_lt (restrict_apply_le s t) hmus⟩

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
inst✝² : PseudoMetricSpace α
inst✝¹ : ProperSpace α
μ : Measure α
inst✝ : IsFiniteMeasureOnCompacts μ
x : α
r : ℝ
⊢ μ (Metric.ball x r) < ∞

Tactic:
by finiteness

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

Goal state before:
pp: α : Type u_8
ι : Type u_9
x✝ : MeasurableSpace α
μ : Measure α
inst✝¹ : Countable ι
inst✝ : Preorder ι
f : ι → Set α
hm : ∀ (i : ι), NullMeasurableSet (f i) μ
hf : ∃ i, μ (f i) ≠ ∞
hne : atTop.NeBot
⊢ Tendsto (fun i ↦ μ (⋂ j, ⋂ (_ : j ≤ i), f j)) atTop (𝓝 (μ (⋂ i, f i)))

Tactic:
cases atTop_neBot_iff.mp hne

Goal state after:
case intro
α : Type u_8
ι : Type u_9
x✝ : MeasurableSpace α
μ : Measure α
inst✝¹ : Countable ι
inst✝ : Preorder ι
f : ι → Set α
hm : ∀ (i : ι), NullMeasurableSet (f i) μ
hf : ∃ i, μ (f i) ≠ ∞
hne : atTop.NeBot
left✝ : Nonempty ι
right✝ : IsDirectedOrder ι
⊢ Tendsto (fun i ↦ μ (⋂ j, ⋂ (_ : j ≤ i), f j)) atTop (𝓝 (μ (⋂ i, f i)))
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: α : Type u_5
m₀ : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hμν : ∀ s ∈ C, μ s = ν s
m : MeasurableSpace α
h : m ≤ m₀
hA : m = generateFrom C
hC : IsPiSystem C
h_univ : μ univ = ν univ
s : Set α
this : IsFiniteMeasure ν
t : Set α
htm : MeasurableSet t
iht : μ t = ν t
⊢ μ t ≠ ∞

Tactic:
by finiteness

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

Goal state before:
pp: α : Type u_5
m₀ : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hμν : ∀ s ∈ C, μ s = ν s
m : MeasurableSpace α
h : m ≤ m₀
hA : m = generateFrom C
hC : IsPiSystem C
h_univ : μ univ = ν univ
s : Set α
this : IsFiniteMeasure ν
t : Set α
htm : MeasurableSet t
iht : μ t = ν t
⊢ ν t ≠ ∞

Tactic:
by finiteness

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

Goal state before:
pp: case refine_1
α : Type u_1
m : MeasurableSpace α
inst✝ : Countable α
μ ν : Measure α
h : ∀ (x : α), μ (measurableAtom x) = ν (measurableAtom x)
s : Set α
hs : MeasurableSet s
y : α
hy : y ∈ s
⊢ ∃ i ∈ s, y ∈ measurableAtom i

Tactic:
exact ⟨y, hy, mem_measurableAtom_self y⟩

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
m : ℕ → Measure α
hv : ∀ (n : ℕ), (m n) t ≠ ∞
hμ : μ = sum m
A : ∃ t' ⊇ t, MeasurableSet t' ∧ ∀ (u : Set α), MeasurableSet u → μ (t' ∩ u) = μ (t ∩ u)
⊢ μ (toMeasurable μ t ∩ s) = μ (t ∩ s)

Tactic:
rw [toMeasurable]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
m : ℕ → Measure α
hv : ∀ (n : ℕ), (m n) t ≠ ∞
hμ : μ = sum m
A : ∃ t' ⊇ t, MeasurableSet t' ∧ ∀ (u : Set α), MeasurableSet u → μ (t' ∩ u) = μ (t ∩ u)
⊢ μ
      ((if h : ∃ t_1 ⊇ t, MeasurableSet t_1 ∧ t_1 =ᵐ[μ] t then h.choose
        else
          if h' : ∃ t_1 ⊇ t, MeasurableSet t_1 ∧ ∀ (u : Set α), MeasurableSet u → μ (t_1 ∩ u) = μ (t ∩ u) then h'.choose
          else ⋯.choose) ∩
        s) =
    μ (t ∩ s)
Module: Mathlib.Data.Set.MemPartition

Goal state before:
pp: case pos
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ⋃₀ memPartition f n = univ
x : α
t : Set α
ht : t ∈ memPartition f n
hxt : x ∈ t
hxf : x ∈ f n
⊢ ∃ t ∈ {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}, x ∈ t

pp: case neg
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ⋃₀ memPartition f n = univ
x : α
t : Set α
ht : t ∈ memPartition f n
hxt : x ∈ t
hxf : x ∉ f n
⊢ ∃ t ∈ {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}, x ∈ t

Tactic:
· exact ⟨t ∩ f n, ⟨t, ht, Or.inl rfl⟩, hxt, hxf⟩

Goal state after:
case neg
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ⋃₀ memPartition f n = univ
x : α
t : Set α
ht : t ∈ memPartition f n
hxt : x ∈ t
hxf : x ∉ f n
⊢ ∃ t ∈ {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}, x ∈ t
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ n, v n
h'v : ∀ (n : ℕ), μ (t ∩ v n) ≠ ∞
A : ∃ t' ⊇ t, MeasurableSet t' ∧ ∀ (u : Set α), MeasurableSet u → μ (t' ∩ u) = μ (t ∩ u)
⊢ μ (toMeasurable μ t ∩ s) = μ (t ∩ s)

Tactic:
rw [toMeasurable]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ n, v n
h'v : ∀ (n : ℕ), μ (t ∩ v n) ≠ ∞
A : ∃ t' ⊇ t, MeasurableSet t' ∧ ∀ (u : Set α), MeasurableSet u → μ (t' ∩ u) = μ (t ∩ u)
⊢ μ
      ((if h : ∃ t_1 ⊇ t, MeasurableSet t_1 ∧ t_1 =ᵐ[μ] t then h.choose
        else
          if h' : ∃ t_1 ⊇ t, MeasurableSet t_1 ∧ ∀ (u : Set α), MeasurableSet u → μ (t_1 ∩ u) = μ (t ∩ u) then h'.choose
          else ⋯.choose) ∩
        s) =
    μ (t ∩ s)
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: case refine_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set α
h : NullMeasurableSet t (μ.restrict s)
t' : Set α
ht' : MeasurableSet t'
t't : t' =ᵐ[μ.restrict s] t
⊢ NullMeasurableSet (t ∩ s) μ

Tactic:
have A : (t' ∩ s : Set α) =ᵐ[μ] (t ∩ s : Set α) := by
      have : ∀ᵐ x ∂μ, x ∈ s → (x ∈ t') = (x ∈ t) :=
        (ae_restrict_iff'₀ hs).1 t't
      filter_upwards [this] with y hy
      change (y ∈ t' ∩ s) = (y ∈ t ∩ s)
      simpa only [eq_iff_iff, mem_inter_iff, and_congr_left_iff] using hy

Goal state after:
case refine_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set α
h : NullMeasurableSet t (μ.restrict s)
t' : Set α
ht' : MeasurableSet t'
t't : t' =ᵐ[μ.restrict s] t
A : t' ∩ s =ᵐ[μ] t ∩ s
⊢ NullMeasurableSet (t ∩ s) μ
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : s ∈ countableGeneratingSet α
⊢ MeasurableSet s

Tactic:
by
  rw [← generateFrom_countableGeneratingSet (α := α)]
  exact measurableSet_generateFrom hs

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

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure β
t : Set β
ht : MeasurableSet t
⊢ μ (f '' f ⁻¹' t) = (μ.restrict (range f)) t

Tactic:
image_preimage_eq_inter_range,

Goal state after:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure β
t : Set β
ht : MeasurableSet t
⊢ μ (t ∩ range f) = (μ.restrict (range f)) t
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
inst✝ : MeasureSpace α
s t : Set α
hs : NullMeasurableSet s volume
ht : MeasurableSet t
⊢ volume ((fun a ↦ ↑a) '' Subtype.val ⁻¹' t) = volume (t ∩ s)

Tactic:
image_preimage_eq_inter_range,

Goal state after:
α : Type u_2
inst✝ : MeasureSpace α
s t : Set α
hs : NullMeasurableSet s volume
ht : MeasurableSet t
⊢ volume (t ∩ range fun a ↦ ↑a) = volume (t ∩ s)
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:
by
  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_1.compl.refine_2.refine_2
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
S : Finset (Set α)
hS_subset : ↑S ⊆ memPartition t n
ht✝ : MeasurableSet (⋃₀ ↑S)
⊢ Codisjoint (⋃₀ (memPartition t n \ ↑S)) (⋃₀ ↑S)

Tactic:
codisjoint_iff

Goal state after:
case refine_1.compl.refine_2.refine_2
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
S : Finset (Set α)
hS_subset : ↑S ⊆ memPartition t n
ht✝ : MeasurableSet (⋃₀ ↑S)
⊢ ⋃₀ (memPartition t n \ ↑S) ⊔ ⋃₀ ↑S = ⊤
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case refine_2
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
x✝ : ∃ S, ↑S ⊆ memPartition t n ∧ s = ⋃₀ ↑S
S : Finset (Set α)
hS_subset : ↑S ⊆ memPartition t n
hS_eq : s = ⋃₀ ↑S
⊢ MeasurableSet s

Tactic:
rw [hS_eq, sUnion_eq_biUnion]

Goal state after:
case refine_2
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
x✝ : ∃ S, ↑S ⊆ memPartition t n ∧ s = ⋃₀ ↑S
S : Finset (Set α)
hS_subset : ↑S ⊆ memPartition t n
hS_eq : s = ⋃₀ ↑S
⊢ MeasurableSet (⋃ i ∈ ↑S, i)
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s✝ t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : OpensMeasurableSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : OpensMeasurableSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : TopologicalSpace γ₂
inst✝² : MeasurableSpace γ₂
inst✝¹ : BorelSpace γ₂
inst✝ : MeasurableSpace δ
h : SecondCountableTopologyEither α β
s : Set (α × β)
hs : IsOpen[instTopologicalSpaceProd] s
hα : SecondCountableTopology α
F : Set α → Set β := fun a ↦ {y | ∃ b, IsOpen[inst✝⁹] b ∧ y ∈ b ∧ a ×ˢ b ⊆ s}
a : Set α
⊢ IsOpen[inst✝⁹] (F a)

Tactic:
apply isOpen_iff_forall_mem_open.2

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s✝ t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : OpensMeasurableSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : OpensMeasurableSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : TopologicalSpace γ₂
inst✝² : MeasurableSpace γ₂
inst✝¹ : BorelSpace γ₂
inst✝ : MeasurableSpace δ
h : SecondCountableTopologyEither α β
s : Set (α × β)
hs : IsOpen[instTopologicalSpaceProd] s
hα : SecondCountableTopology α
F : Set α → Set β := ⋯
a : Set α
⊢ ∀ x ∈ F a, ∃ t ⊆ F a, IsOpen[inst✝⁹] t ∧ x ∈ t
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s✝ t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : OpensMeasurableSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : OpensMeasurableSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : TopologicalSpace γ₂
inst✝² : MeasurableSpace γ₂
inst✝¹ : BorelSpace γ₂
inst✝ : MeasurableSpace δ
h : SecondCountableTopologyEither α β
s : Set (α × β)
hs : IsOpen[instTopologicalSpaceProd] s
hβ : SecondCountableTopology β
F : Set β → Set α := fun a ↦ {y | ∃ b, IsOpen[inst✝¹²] b ∧ y ∈ b ∧ b ×ˢ a ⊆ s}
a : Set β
⊢ IsOpen[inst✝¹²] (F a)

Tactic:
apply isOpen_iff_forall_mem_open.2

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s✝ t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : OpensMeasurableSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : OpensMeasurableSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : TopologicalSpace γ₂
inst✝² : MeasurableSpace γ₂
inst✝¹ : BorelSpace γ₂
inst✝ : MeasurableSpace δ
h : SecondCountableTopologyEither α β
s : Set (α × β)
hs : IsOpen[instTopologicalSpaceProd] s
hβ : SecondCountableTopology β
F : Set β → Set α := ⋯
a : Set β
⊢ ∀ x ∈ F a, ∃ t ⊆ F a, IsOpen[inst✝¹²] t ∧ x ∈ t
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: α : Type u_1
γ : Type u_3
inst✝⁶ : TopologicalSpace α
inst✝⁵ : MeasurableSpace α
inst✝⁴ : OpensMeasurableSpace α
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
f g : α → γ
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
hf : ContinuousOn f s
hg : ContinuousOn g sᶜ
hs : MeasurableSet s
t : Set γ
ht : IsOpen[inst✝³] t
⊢ MeasurableSet (s.piecewise f g ⁻¹' t)

Tactic:
piecewise_preimage,

Goal state after:
α : Type u_1
γ : Type u_3
inst✝⁶ : TopologicalSpace α
inst✝⁵ : MeasurableSpace α
inst✝⁴ : OpensMeasurableSpace α
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
f g : α → γ
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
hf : ContinuousOn f s
hg : ContinuousOn g sᶜ
hs : MeasurableSet s
t : Set γ
ht : IsOpen[inst✝³] t
⊢ MeasurableSet (s.ite (f ⁻¹' t) (g ⁻¹' t))
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

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

Tactic:
grw [infEDist_le_hausdorffEDist_of_mem xs]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
A : Set α
r₁ r₂ : ℝ
hr : r₁ < r₂
⊢ Disjoint (frontier (thickening r₁ A)) (frontier (thickening r₂ A))

Tactic:
rcases le_total r₁ 0 with h₁ | h₁

Goal state after:
case inl
α : Type u
inst✝ : PseudoEMetricSpace α
A : Set α
r₁ r₂ : ℝ
hr : r₁ < r₂
h₁ : r₁ ≤ 0
⊢ Disjoint (frontier (thickening r₁ A)) (frontier (thickening r₂ A))

case inr
α : Type u
inst✝ : PseudoEMetricSpace α
A : Set α
r₁ r₂ : ℝ
hr : r₁ < r₂
h₁ : 0 ≤ r₁
⊢ Disjoint (frontier (thickening r₁ A)) (frontier (thickening r₂ A))
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Zero β
r : β
s : Set α
f : α →ₛ β
hs : MeasurableSet s
⊢ r ∈ (f.restrict s).range ↔ r = 0 ∧ s ≠ univ ∨ r ∈ ⇑f '' s

Tactic:
rw [← Finset.mem_coe, coe_range, coe_restrict _ hs, mem_range_indicator]

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

Goal state before:
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:
· rintro s t ⟨ε₁, hε₁, V₁, hV₁, hV₁thickening⟩ ⟨ε₂, hε₂, V₂, hV₂, hV₂thickening⟩
    refine ⟨min ε₁ ε₂, by positivity, V₁ ∪ V₂, union_mem_nhdsSet hV₁ hV₂, ?_⟩
    rw [image_union, thickening_union]
    calc thickening (ε₁ ⊓ ε₂) (f '' V₁) ∪ thickening (ε₁ ⊓ ε₂) (f '' V₂)
      _ ⊆ thickening ε₁ (f '' V₁) ∪ thickening ε₂ (f '' V₂) := by gcongr <;> norm_num
      _ ⊆ U ∪ U := by gcongr
      _ = U := union_self _

Goal state after:
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: K : Subfield ℝ
hc : IsClosed ↑K
⊢ K = ⊤

Tactic:
SetLike.ext'_iff,

Goal state after:
K : Subfield ℝ
hc : IsClosed ↑K
⊢ ↑K = ↑⊤