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

Goal state before:
pp: α : Type u
m : OuterMeasure α
s s₁✝ s₂✝ s₁ s₂ : Set α
⊢ m.caratheodoryDynkin.Has s₁ → m.caratheodoryDynkin.Has s₂ → m.caratheodoryDynkin.Has (s₁ ∩ s₂)

Tactic:
apply isCaratheodory_inter

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
h_nonempty : (t1 ∩ t2).Nonempty
g : ι → Set α := fun n ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
x : α
⊢ x ∈ (⋂ x ∈ p1, f1 x) ⊓ ⋂ x ∈ p2, f2 x ↔ x ∈ ⋂ i ∈ p1 ∪ p2, g i

Tactic:
simp only [inf_eq_inter, mem_inter_iff, mem_iInter]

Goal state after:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
h_nonempty : (t1 ∩ t2).Nonempty
g : ι → Set α := fun n ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
x : α
⊢ ((∀ i ∈ p1, x ∈ f1 i) ∧ ∀ i ∈ p2, x ∈ f2 i) ↔ ∀ i ∈ p1 ∪ p2, x ∈ g i
Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
s : Set β
f : β → Set α
hs : s.Finite
hfin : ∀ i ∈ s, μ (f i) < ∞
⊢ μ (⋃ i ∈ s, f i) < ∞

Tactic:
convert! (measure_biUnion_finset_le (μ := μ) hs.toFinset f).trans_lt _ using 3

Goal state after:
case e'_3
α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
s : Set β
f : β → Set α
hs : s.Finite
hfin : ∀ i ∈ s, μ (f i) < ∞
⊢ (fun i ↦ ⋃ (_ : i ∈ s), f i) = fun i ↦ ⋃ (_ : i ∈ hs.toFinset), f i

case convert_2
α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
s : Set β
f : β → Set α
hs : s.Finite
hfin : ∀ i ∈ s, μ (f i) < ∞
⊢ ∑ i ∈ hs.toFinset, μ (f i) < ∞
Module: Mathlib.MeasureTheory.OuterMeasure.AE

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
h : s =ᵐ[μ] univ
⊢ s ∩ t =ᵐ[μ] t

Tactic:
by
  convert! ae_eq_set_inter h (ae_eq_refl t)
  rw [univ_inter]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
s : Set β
⊢ MeasurableSet (f ⁻¹' s) ↔ MeasurableSet (s ∩ range f)

Tactic:
by
  rw [← image_preimage_eq_inter_range, hf.measurableSet_image]

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

Goal state before:
pp: case neg.refine_2
α : 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 : ℕ → Set α
hsub : ∀ (n : ℕ), s ⊆ t n
hm : ∀ (n : ℕ), MeasurableSet (t n)
hm' : ∀ (n : ℕ), m (t n) < ms + (↑n)⁻¹
this : Tendsto (fun n ↦ ms + (↑n)⁻¹) atTop (𝓝 ms)
⊢ ⨅ (_ : s ⊆ ⋂ n, t n), ⨅ (_ : MeasurableSet (⋂ n, t n)), m (⋂ n, t n) ≤ m (⋂ n, t n)

Tactic:
refine iInf_le_of_le (subset_iInter hsub) ?_

Goal state after:
case neg.refine_2
α : 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 : ℕ → Set α
hsub : ∀ (n : ℕ), s ⊆ t n
hm : ∀ (n : ℕ), MeasurableSet (t n)
hm' : ∀ (n : ℕ), m (t n) < ms + (↑n)⁻¹
this : Tendsto (fun n ↦ ms + (↑n)⁻¹) atTop (𝓝 ms)
⊢ ⨅ (_ : MeasurableSet (⋂ n, t n)), m (⋂ n, t n) ≤ m (⋂ n, t n)
Module: Mathlib.MeasureTheory.Measure.AEDisjoint

Goal state before:
pp: α : Type u_2
m : MeasurableSpace α
μ : Measure α
s : Set α
ι : Sort u_3
inst✝ : Countable ι
t : ι → Set α
⊢ AEDisjoint μ s (⋃ i, t i) ↔ ∀ (i : ι), AEDisjoint μ s (t i)

Tactic:
simp only [AEDisjoint, inter_iUnion, measure_iUnion_null_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m' : MeasurableSpace β
inst✝ : BooleanAlgebra β
h : Measurable compl
f : α → β
⊢ MeasurableSpace.comap (fun a ↦ (f a)ᶜ) inferInstance = MeasurableSpace.comap f inferInstance

Tactic:
← Function.comp_def,

Goal state after:
α : Type u_1
β : Type u_2
m' : MeasurableSpace β
inst✝ : BooleanAlgebra β
h : Measurable compl
f : α → β
⊢ MeasurableSpace.comap (compl ∘ f) inferInstance = MeasurableSpace.comap f inferInstance
Module: Mathlib.MeasureTheory.Measure.NullMeasurable

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
htm : MeasurableSet t
hst : s =ᵐ[μ] t
⊢ toMeasurable μ (s \ t) =ᵐ[μ] ∅

Tactic:
simp [ae_le_set.1 hst.le]

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

Goal state before:
pp: α : Type u_1
ι : Type u_4
mα : MeasurableSpace α
ν : Measure α
μs : ι → Measure α
hμs : ∀ (i : ι), μs i ≪ ν
s : Set α
hs : MeasurableSet s
hs0 : ν s = 0
⊢ (sum μs) s = 0

Tactic:
simp [sum_apply _ hs, fun i ↦ hμs i hs0]

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving (⇑e) μ μ
he' : QuasiMeasurePreserving (⇑e.symm) μ μ
k : ℤ
hs : ⇑e '' s =ᵐ[μ] s
⊢ ⇑(e ^ k) '' s =ᵐ[μ] s

Tactic:
rw [Equiv.image_eq_preimage_symm]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving (⇑e) μ μ
he' : QuasiMeasurePreserving (⇑e.symm) μ μ
k : ℤ
hs : ⇑e '' s =ᵐ[μ] s
⊢ ⇑(e ^ k).symm ⁻¹' s =ᵐ[μ] s
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h's : s ⊆ u
h't : t ⊆ u
h : μ u < μ t + μ s
⊢ (t ∩ s).Nonempty

Tactic:
exact nonempty_inter_of_measure_lt_add μ hs h't h's h

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → β
hf : AEMeasurable f μ
⊢ IsFiniteMeasure (map f μ)

pp: case neg
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → β
hf : ¬AEMeasurable f μ
⊢ IsFiniteMeasure (map f μ)

Tactic:
· constructor
    rw [map_apply_of_aemeasurable hf MeasurableSet.univ]
    exact measure_lt_top μ _

Goal state after:
case neg
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → β
hf : ¬AEMeasurable f μ
⊢ IsFiniteMeasure (map f μ)
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
γ : Type u_5
f g : α → γ
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hs_zero : μ s = 0
h_ss : sᶜ ⊆ {a | (if a ∈ s then f a else g a) = g a}
| s

Tactic:
← compl_compl s

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
γ : Type u_5
f g : α → γ
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hs_zero : μ s = 0
h_ss : sᶜ ⊆ {a | (if a ∈ s then f a else g a) = g a}
| sᶜᶜ
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
s : ι → Set α
t : Set ι
ht : t.Countable
this : Countable ↑t
⊢ ae (μ.restrict (⋃ i ∈ t, s i)) = ⨆ i ∈ t, ae (μ.restrict (s i))

Tactic:
rw [biUnion_eq_iUnion, ae_restrict_iUnion_eq, ← iSup_subtype'']

Goal state after:
Module: Mathlib.Data.Set.MemPartition

Goal state before:
pp: case succ
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : (memPartition f n).Finite
this : Finite ↑(memPartition f n)
⊢ Finite ↑(⋃ i, {x | i ∈ memPartition f n ∧ (x = i ∩ f n ∨ x = i \ f n)})

Tactic:
← exists_prop,

Goal state after:
case succ
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : (memPartition f n).Finite
this : Finite ↑(memPartition f n)
⊢ Finite ↑(⋃ i, {x | ∃ (_ : i ∈ memPartition f n), x = i ∩ f n ∨ x = i \ f n})
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : MeasurableSet s
ht : (μ + ν) t ≠ ∞
⊢ μ t ≠ ∞

Tactic:
simp only [not_or, ENNReal.add_eq_top, Pi.add_apply, Ne, coe_add] at ht

Goal state after:
case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : MeasurableSet s
ht : ¬μ t = ∞ ∧ ¬ν t = ∞
⊢ μ t ≠ ∞
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
δ : Type u_4
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
f g : α → δ
⊢ f =ᵐ[μ.restrict (⋃ i, s i)] g ↔ ∀ (i : ι), f =ᵐ[μ.restrict (s i)] g

Tactic:
simp_rw [EventuallyEq, ae_restrict_iUnion_eq, eventually_iSup]

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

Goal state before:
pp: β : Type u_2
m₁ m₂ : MeasurableSpace β
h₁ : CountablyGenerated β
h₂ : CountablyGenerated β
⊢ CountablyGenerated β

Tactic:
rcases h₁ with ⟨⟨b₁, hb₁c, rfl⟩⟩
  rcases h₂ with ⟨⟨b₂, hb₂c, rfl⟩⟩
  exact @mk _ (_ ⊔ _) ⟨_, hb₁c.union hb₂c, generateFrom_sup_generateFrom⟩

Goal state after:
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
hf : f =ᵐ[μ.restrict s] 0
⊢ s.indicator f =ᵐ[μ] 0

Tactic:
rw [Filter.EventuallyEq, ae_restrict_iff' hs] at hf

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = 0 x
⊢ s.indicator f =ᵐ[μ] 0
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : Countable α
inst✝ : SeparatesPoints α
x : α
s : (y : α) → x ≠ y → Set α
hsm : ∀ (y : α) (h : x ≠ y), MeasurableSet (s y h)
hxs : ∀ (y : α) (h : x ≠ y), x ∈ s y h
hys : ∀ (y : α) (h : x ≠ y), y ∉ s y h
y : α
h : x ≠ y
⊢ y ∈ {x} ↔ y ∈ ⋂ b, ⋂ (b_1 : x ≠ b), s b b_1

Tactic:
simp only [mem_singleton_iff, h.symm, false_iff, mem_iInter, not_forall]

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : Countable α
inst✝ : SeparatesPoints α
x : α
s : (y : α) → x ≠ y → Set α
hsm : ∀ (y : α) (h : x ≠ y), MeasurableSet (s y h)
hxs : ∀ (y : α) (h : x ≠ y), x ∈ s y h
hys : ∀ (y : α) (h : x ≠ y), y ∉ s y h
y : α
h : x ≠ y
⊢ ∃ x_1, ∃ (x : x ≠ x_1), y ∉ s x_1 x
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
⊢ x ∈ P ({x_1 ∈ F | x ∈ s x_1})

Tactic:
· simp_rw [P, mem_inter_iff, mem_iInter, Finset.mem_sdiff, mem_filter]; tauto

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
⊢ ∀ t_1 ∈ range t, MeasurableSet t_1

Tactic:
rintro s ⟨i, rfl⟩

Goal state after:
α : Type u_1
m : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
i : ℕ
⊢ MeasurableSet (t i)
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
μ : Measure α
inst✝ : Zero β
s : Set α
hs : NullMeasurableSet s μ
⊢ AEMeasurable (s.indicator f) μ ↔ AEMeasurable f (μ.restrict s)

Tactic:
rcases hs with ⟨t, ht, hst⟩

Goal state after:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
μ : Measure α
inst✝ : Zero β
s t : Set α
ht : MeasurableSet t
hst : s =ᵐ[μ] t
⊢ AEMeasurable (s.indicator f) μ ↔ AEMeasurable f (μ.restrict s)
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
inst✝¹ : Preorder α
inst✝ : atTop.IsCountablyGenerated
μ : Measure α
⊢ Tendsto (fun x ↦ μ (Iic x)) atTop (𝓝 (μ univ))

Tactic:
rw [← iUnion_Iic]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
inst✝¹ : Preorder α
inst✝ : atTop.IsCountablyGenerated
μ : Measure α
⊢ Tendsto (fun x ↦ μ (Iic x)) atTop (𝓝 (μ (⋃ a, Iic a)))
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 α✝
α : Type u_6
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
hα : BorelSpace α
p : α → Prop
⊢ instMeasurableSpace = borel (Subtype p)

Tactic:
borelize α

Goal state after:
α✝ : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s t u : Set α✝
α : Type u_6
inst✝ : TopologicalSpace α
p : α → Prop
hα : BorelSpace α
this✝ : MeasurableSpace α := borel α
⊢ instMeasurableSpace = borel (Subtype p)
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 α✝
α : Type u_6
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
inst✝ : SecondCountableTopology α
b : Set (Set α)
bct : b.Countable
hb : IsTopologicalBasis b
⊢ inst✝² = MeasurableSpace.generateFrom b

Tactic:
borelize α

Goal state after:
α✝ : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s t u : Set α✝
α : Type u_6
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
b : Set (Set α)
bct : b.Countable
hb : IsTopologicalBasis b
inst✝ : BorelSpace α
this✝ : MeasurableSpace α := borel α
⊢ borel α = MeasurableSpace.generateFrom b
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: α : Type u_6
inst✝² : TopologicalSpace α
inst✝¹ : T0Space α
inst✝ : Countable α
s : Set α
x✝ : MeasurableSet s
⊢ MeasurableSet s

Tactic:
borelize α

Goal state after:
α : Type u_6
inst✝² : TopologicalSpace α
inst✝¹ : T0Space α
inst✝ : Countable α
s : Set α
x✝ : MeasurableSet s
this✝¹ : MeasurableSpace α := borel α
this✝ : BorelSpace α
⊢ MeasurableSet s
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: α : Type u_5
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
s t : Set α
⊢ ∀ t_1 ∈ {S | ∃ l ∈ s, ∃ u ∈ t, l ≤ u ∧ Icc l u = S}, MeasurableSet t_1

Tactic:
borelize α

Goal state after:
α : Type u_5
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
s t : Set α
this✝¹ : MeasurableSpace α := borel α
this✝ : BorelSpace α
⊢ ∀ t_1 ∈ {S | ∃ l ∈ s, ∃ u ∈ t, l ≤ u ∧ Icc l u = S}, MeasurableSet t_1
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

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

Tactic:
borelize α

Goal state after:
α : Type u_5
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
s t : Set α
this✝¹ : MeasurableSpace α := borel α
this✝ : BorelSpace α
⊢ ∀ t_1 ∈ {S | ∃ l ∈ s, ∃ u ∈ t, l < u ∧ Ico l u = S}, MeasurableSet t_1
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
⊢ hausdorffEDist s s = 0

Tactic:
simp only [hausdorffEDist_def, sup_idem, ENNReal.iSup_eq_zero]

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
⊢ ∀ i ∈ s, infEDist i s = 0
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

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

Tactic:
calc
      _ ≤ hausdorffEDist s (closure s) + hausdorffEDist (closure s) t := hausdorffEDist_triangle
      _ = hausdorffEDist (closure s) t := by simp

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

Goal state before:
pp: case a
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
u v : α
⊢ MeasurableSet (Ioc u v)

Tactic:
borelize α

Goal state after:
case a
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
u v : α
this✝¹ : MeasurableSpace α := borel α
this✝ : BorelSpace α
⊢ MeasurableSet (Ioc u v)
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s t u : Set α
fin : hausdorffEDist s t ≠ ∞
⊢ hausdorffDist s u ≤ hausdorffDist s t + hausdorffDist t u

Tactic:
by
  refine toReal_le_add' hausdorffEDist_triangle (flip absurd fin) (not_imp_not.1 fun h ↦ ?_)
  rw [hausdorffEDist_comm] at fin
  exact ne_top_of_le_ne_top (add_ne_top.2 ⟨fin, h⟩) hausdorffEDist_triangle

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

Goal state before:
pp: α : Type u_5
m : MeasurableSpace α
inst✝¹ : CountablyGenerated α
inst✝ : MeasurableSpace.SeparatesPoints α
s : Set (ℕ → Bool)
f : α ≃ᵐ ↑s
this : TopologicalSpace α := induced (⇑f) inferInstance
⊢ ∃ x, SecondCountableTopology α ∧ T4Space α ∧ BorelSpace α

Tactic:
let F := f.toEquiv.toHomeomorphOfIsInducing <| .induced _

Goal state after:
α : Type u_5
m : MeasurableSpace α
inst✝¹ : CountablyGenerated α
inst✝ : MeasurableSpace.SeparatesPoints α
s : Set (ℕ → Bool)
f : α ≃ᵐ ↑s
this : TopologicalSpace α := induced (⇑f) inferInstance
F : α ≃ₜ ↑s := f.toHomeomorphOfIsInducing ⋯
⊢ ∃ x, SecondCountableTopology α ∧ T4Space α ∧ BorelSpace α
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: case e_f
α : Type u_1
β : Type u_2
inst✝⁷ : MeasurableSpace α
inst✝⁶ : SemilatticeSup β
inst✝⁵ : OrderBot β
inst✝⁴ : Zero β
inst✝³ : TopologicalSpace β
inst✝² : OrderClosedTopology β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
i : ℕ → β
f : α → β
n : ℕ
a : α
hf : Measurable f
k : ℕ
⊢ {a | i k ≤ f a}.indicator (⇑(const α (i k))) a = if i k ≤ f a then i k else 0

Tactic:
simp only [coe_const, mem_ofPred_eq, indicator_apply, Function.const_apply]

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'
i✝ : ι
this : Nonempty ι
f' : ι → δ → α := fun i ↦ s.piecewise (f i) g'
b : δ
hb : b ∈ s
i : ι
⊢ f' i b = f i b

Tactic:
by simp [f', hb]

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'
i✝ : ι
this : Nonempty ι
f' : ι → δ → α := fun i ↦ s.piecewise (f i) g'
b : δ
hb : b ∉ s
i : ι
⊢ f' i b = g' b

Tactic:
by simp [f', hb]

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

Goal state before:
pp: case pos
α : Type u_1
δ : Type u_4
inst✝⁵ : TopologicalSpace α
mα : MeasurableSpace α
inst✝⁴ : BorelSpace α
mδ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
μ : Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i) μ
hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a | ∃ i, f i b = a} (g b)
a✝ : Nontrivial α
hα : Nonempty α
hι : Nonempty ι
p : δ → (ι → α) → Prop := fun x f' ↦ IsLUB {a | ∃ i, f' i = a} (g x)
g_seq : δ → α := (aeSeqSet hf p).piecewise g fun x ↦ hα.some
b : δ
h : b ∈ aeSeqSet hf p
h_set_eq : {a | ∃ i, mk (f i) ⋯ b = a} = {a | ∃ i, f i b = a}
⊢ IsLUB {a | ∃ i, mk (f i) ⋯ b = a} (g b)

Tactic:
rw [h_set_eq]

Goal state after:
case pos
α : Type u_1
δ : Type u_4
inst✝⁵ : TopologicalSpace α
mα : MeasurableSpace α
inst✝⁴ : BorelSpace α
mδ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
μ : Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i) μ
hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a | ∃ i, f i b = a} (g b)
a✝ : Nontrivial α
hα : Nonempty α
hι : Nonempty ι
p : δ → (ι → α) → Prop := fun x f' ↦ IsLUB {a | ∃ i, f' i = a} (g x)
g_seq : δ → α := (aeSeqSet hf p).piecewise g fun x ↦ hα.some
b : δ
h : b ∈ aeSeqSet hf p
h_set_eq : {a | ∃ i, mk (f i) ⋯ b = a} = {a | ∃ i, f i b = a}
⊢ IsLUB {a | ∃ i, f i b = a} (g b)
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: δ : Type u_4
mδ : MeasurableSpace δ
α : Type u_5
mα : MeasurableSpace α
inst✝ : ConditionallyCompleteLattice α
p : Prop
f : δ → α
hf : Measurable f
⊢ Measurable fun b ↦ ⨅ (_ : p), f b

Tactic:
simp_rw [ciInf_eq_ite]
  split_ifs with h
  · exact hf
  · exact measurable_const

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
⊢ (const α c).lintegral μ = c * μ univ

Tactic:
rw [lintegral]
  cases isEmpty_or_nonempty α
  · simp [μ.eq_zero_of_isEmpty]
  · simp only [range_const, coe_const, Finset.sum_singleton]
    unfold Function.const; rw [preimage_const_of_mem (mem_singleton c)]

Goal state after:
Module: Mathlib.Topology.IndicatorConstPointwise

Goal state before:
pp: case mp
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst✝¹ : DecidablePred p
q : Prop
inst✝ : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
h : Tendsto (fun i ↦ if p i then a else b) L (if q then F else G)
⊢ ∀ᶠ (i : ι) in L, p i ↔ q

Tactic:
by_cases hq : q

Goal state after:
case pos
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst✝¹ : DecidablePred p
q : Prop
inst✝ : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
h : Tendsto (fun i ↦ if p i then a else b) L (if q then F else G)
hq : q
⊢ ∀ᶠ (i : ι) in L, p i ↔ q

case neg
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst✝¹ : DecidablePred p
q : Prop
inst✝ : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
h : Tendsto (fun i ↦ if p i then a else b) L (if q then F else G)
hq : ¬q
⊢ ∀ᶠ (i : ι) in L, p i ↔ q