mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
s : Set α
y : β
inst✝¹ : Zero β
inst✝ : Preorder β
hs : IsOpen[inst✝²] s
hy : 0 ≤ y
⊢ LowerSemicontinuous (s.indicator fun _x ↦ y)

Tactic:
intro x z hz

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
s : Set α
y : β
inst✝¹ : Zero β
inst✝ : Preorder β
hs : IsOpen[inst✝²] s
hy : 0 ≤ y
x : α
z : β
hz : s.indicator (fun _x ↦ y) x > z
⊢ ∀ᶠ (x' : α) in 𝓝 x, (fun x1 x2 ↦ s.indicator (fun _x ↦ y) x1 > x2) x' z
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: case inr
α : Type u_4
s : Set α
hinf : s.Infinite
this : Infinite ↑s
⊢ ∑' (x : ↑s), 1 = ↑s.encard

Tactic:
rw [tsum_const_eq_top_of_ne_zero one_ne_zero, encard_eq_top hinf, ENat.toENNReal_top]

Goal state after:
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
s : Set α
y : β
inst✝¹ : Zero β
inst✝ : Preorder β
hs : IsClosed[inst✝²] s
hy : y ≤ 0
⊢ LowerSemicontinuous (s.indicator fun _x ↦ y)

Tactic:
intro x z hz

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
s : Set α
y : β
inst✝¹ : Zero β
inst✝ : Preorder β
hs : IsClosed[inst✝²] s
hy : y ≤ 0
x : α
z : β
hz : s.indicator (fun _x ↦ y) x > z
⊢ ∀ᶠ (x' : α) in 𝓝 x, (fun x1 x2 ↦ s.indicator (fun _x ↦ y) x1 > x2) x' z
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: ⊢ 𝓝[≠] ⊤ = map Real.toEReal atTop

Tactic:
apply (nhdsWithin_hasBasis nhds_top_basis_Ici _).ext (atTop_basis.map Real.toEReal)
  · simp only [EReal.image_coe_Ici, true_and]
    intro x hx
    by_cases hx_bot : x = ⊥
    · simp [hx_bot]
    lift x to ℝ using ⟨hx.ne_top, hx_bot⟩
    refine ⟨x, fun x ⟨h1, h2⟩ ↦ ?_⟩
    simp [h1, h2.ne_top]
  · simp only [EReal.image_coe_Ici, true_implies]
    refine fun x ↦ ⟨x, ⟨EReal.coe_lt_top x, fun x ⟨(h1 : _ ≤ x), h2⟩ ↦ ?_⟩⟩
    simp [h1, Ne.lt_top' fun a ↦ h2 a.symm]

Goal state after:
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : TopologicalSpace α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst✝³] s
hf : ∀ x ∈ s, ∀ y < f x, ∀ᶠ (x : α) in 𝓝 x, x ∈ s → y < f x
x : α
y : γ
h : (x, y).1 ∈ s → (x, y).2 < f (x, y).1
hx : x ∈ s
⊢ ∀ᶠ (a : α × γ) in 𝓝 (x, y), a.1 ∈ s → a.2 < f a.1

pp: case neg
α : Type u_1
inst✝³ : TopologicalSpace α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst✝³] s
hf : ∀ x ∈ s, ∀ y < f x, ∀ᶠ (x : α) in 𝓝 x, x ∈ s → y < f x
x : α
y : γ
h : (x, y).1 ∈ s → (x, y).2 < f (x, y).1
hx : x ∉ s
⊢ ∀ᶠ (a : α × γ) in 𝓝 (x, y), a.1 ∈ s → a.2 < f a.1

Tactic:
· have ⟨y', hy', z, hz, h₁⟩ := (h hx).exists_disjoint_Iio_Ioi
      filter_upwards [(hf x hx z hz).prodMk_nhds (eventually_lt_nhds hy')]
        with _ ⟨h₂, h₃⟩ h₄ using h₁ _ h₃ _ <| h₂ h₄

Goal state after:
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst✝³] s
hf : ∀ x ∈ s, ∀ y < f x, ∀ᶠ (x : α) in 𝓝 x, x ∈ s → y < f x
x : α
y : γ
h : (x, y).1 ∈ s → (x, y).2 < f (x, y).1
hx : x ∉ s
⊢ ∀ᶠ (a : α × γ) in 𝓝 (x, y), a.1 ∈ s → a.2 < f a.1
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
P : Set α → Prop
m_top : ∀ (s : Set α), ¬P s → m s = ∞
s : Set α
t : ℕ → Set α
x✝ : ∀ (i : ℕ), P (t i)
h : s ⊆ ⋃ i, t i
⊢ s ⊆ iUnion t

Tactic:
by exact h

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

Goal state before:
pp: case refine_2
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : β → α
h : Monotone m ∨ Surjective f
s : Set β
t : ℕ → Set α
ht : f '' s ⊆ iUnion t
⊢ ∃ (_ : s ⊆ ⋃ k, f ⁻¹' t k), ∑' (n : ℕ), m (f '' (fun k ↦ f ⁻¹' t k) n) ≤ ∑' (n : ℕ), m (t n)

Tactic:
rw [Set.image_subset_iff, preimage_iUnion] at ht

Goal state after:
case refine_2
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : β → α
h : Monotone m ∨ Surjective f
s : Set β
t : ℕ → Set α
ht : s ⊆ ⋃ i, f ⁻¹' t i
⊢ ∃ (_ : s ⊆ ⋃ k, f ⁻¹' t k), ∑' (n : ℕ), m (f '' (fun k ↦ f ⁻¹' t k) n) ≤ ∑' (n : ℕ), m (t n)
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
w : ι → ℝ≥0
⊢ ∃ δ, (∀ (i : ι), 0 < δ i) ∧ ∑' (i : ι), (fun i ↦ ↑(w i)) i * ↑(δ i) < ε

Tactic:
rcases exists_pos_sum_of_countable hε ι with ⟨δ', Hpos, Hsum⟩

Goal state after:
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
w δ' : ι → ℝ≥0
Hpos : ∀ (i : ι), 0 < δ' i
Hsum : ∑' (i : ι), ↑(δ' i) < ε
⊢ ∃ δ, (∀ (i : ι), 0 < δ i) ∧ ∑' (i : ι), (fun i ↦ ↑(w i)) i * ↑(δ i) < ε
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
β : Type u_4
S : Set (Set β)
h_pi : IsPiSystem S
f : α → β
⊢ IsPiSystem {s | ∃ t ∈ S, f ⁻¹' t = s}

Tactic:
rintro _ ⟨s, hs_mem, rfl⟩ _ ⟨t, ht_mem, rfl⟩ hst
  rw [← Set.preimage_inter] at hst ⊢
  exact ⟨s ∩ t, h_pi s hs_mem t ht_mem (nonempty_of_nonempty_preimage hst), rfl⟩

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

Goal state before:
pp: α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
t : Set α
⊢ m (t ∩ ⋃ i, s i) ≤ ⨆ n, m (t ∩ ⋃ i, ⋃ (_ : i < n), s i)

Tactic:
convert! measure_iUnion_le (μ := m) fun i => t ∩ s i using 1

Goal state after:
case e'_3
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
t : Set α
⊢ m (t ∩ ⋃ i, s i) = m (⋃ i, t ∩ s i)

case e'_4
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
t : Set α
⊢ ⨆ n, m (t ∩ ⋃ i, ⋃ (_ : i < n), s i) = ∑' (i : ℕ), m (t ∩ s i)
Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory

Goal state before:
pp: case refine_3
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
h₀ : m ∅ = 0
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
f : ℕ → Set α
hf : t ⊆ ⋃ i, f i
⊢ ∑' (i : ℕ), m ((fun i ↦ f i ∩ s) i) + ∑' (i : ℕ), m ((fun i ↦ f i \ s) i) ≤ ∑' (i : ℕ), m (f i)

Tactic:
· rw [← ENNReal.tsum_add]
    exact ENNReal.tsum_le_tsum fun i => hs _

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s t : Set α
h : μ (s ∪ t) < ∞
⊢ μ s < ∞

Tactic:
exact (measure_mono Set.subset_union_left).trans_lt h

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
d : DynkinSystem α
s₁ s₂ : Set α
h₁ : d.Has s₁
h₂ : d.Has s₂
h : Disjoint s₁ s₂
⊢ d.Has (s₁ ∪ s₂)

Tactic:
union_eq_iUnion

Goal state after:
α : Type u_3
d : DynkinSystem α
s₁ s₂ : Set α
h₁ : d.Has s₁
h₂ : d.Has s₂
h : Disjoint s₁ s₂
⊢ d.Has (⋃ b, bif b then s₁ else s₂)
Module: Mathlib.MeasureTheory.MeasurableSpace.EventuallyMeasurable

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s t : Set α
l : Filter α
inst✝ : CountableInterFilter l
ht : EventuallyMeasurableSet m l t
hst : s =ᶠ[l] t
⊢ EventuallyMeasurableSet m l s

Tactic:
rcases ht with ⟨t', ht', htt'⟩
  exact ⟨t', ht', hst.trans htt'⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
hs : ∀ ⦃s_1 : Set α⦄, s_1 ∈ 𝓟 s → ∃ t ∈ 𝓟 s, MeasurableSet t ∧ t ⊆ s_1
t : Set α
ht : t ∈ 𝓟 s
htm : MeasurableSet t
hts : t ⊆ s
this : t = s
⊢ MeasurableSet s

Tactic:
rwa [← this]

Goal state after:
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 γ✝
π : δ' → Type u_6
π' : δ' → Type u_7
inst✝³ : (x : δ') → MeasurableSpace (π x)
inst✝² : (x : δ') → MeasurableSpace (π' x)
α : Type u_8
β : Type u_9
γ : Type u_10
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
⊢ Measurable ⇑(Equiv.arrowProdEquivProdArrow γ (fun i ↦ α) fun i ↦ β)

Tactic:
by
    dsimp [Equiv.arrowProdEquivProdArrow]
    fun_prop

Goal state after:
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 γ✝
π : δ' → Type u_6
π' : δ' → Type u_7
inst✝³ : (x : δ') → MeasurableSpace (π x)
inst✝² : (x : δ') → MeasurableSpace (π' x)
α : Type u_8
β : Type u_9
γ : Type u_10
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
⊢ Measurable ⇑(Equiv.arrowProdEquivProdArrow γ (fun i ↦ α) fun i ↦ β).symm

Tactic:
by
    dsimp [Equiv.arrowProdEquivProdArrow]
    fun_prop

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : MeasurableSpace α
μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
⊢ ((restrict s) μ.trim) t ≤ ((restrict s) μ) t

Tactic:
· rw [restrict_apply, trim_eq _ (ht.inter hs), restrict_apply]

Goal state after:
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 γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A ↦ (g '' (f '' A)ᶜ)ᶜ
this : (A : Set α) ×' MeasurableSet A ∧ F A = A
⊢ α ≃ᵐ β

Tactic:
classical
    rcases this with ⟨A, Ameas, Afp⟩
    let B := f '' A
    have Bmeas : MeasurableSet B := hf.measurableSet_image' Ameas
    refine (MeasurableEquiv.sumCompl Ameas).symm.trans
      (MeasurableEquiv.trans ?_ (MeasurableEquiv.sumCompl Bmeas))
    apply MeasurableEquiv.sumCongr (hf.equivImage _)
    have : Aᶜ = g '' Bᶜ := by
      apply compl_injective
      rw [← Afp]
      simp [F, B]
    rw [this]
    exact (hg.equivImage _).symm

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

Goal state before:
pp: case refine_2.a
α : 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 γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := ⋯
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := ⋯
⊢ F (iInter X) ⊆ iInter X

Tactic:
apply subset_iInter
    intro n
    cases n
    · exact subset_univ _
    rw [Function.iterate_succ', Function.comp_apply]
    exact Fmono (iInter_subset _ _)

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
h : μ s = μ t
hfin : μ (s ∩ t) ≠ ∞
⊢ μ (s \ t) = μ (t \ s)

Tactic:
rw [← ENNReal.add_right_inj hfin, measure_inter_add_sdiff₀ _ ht, inter_comm,
    measure_inter_add_sdiff₀ _ hs, h]

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν : Measure α
h : μ₁ + μ₂ ≪ ν
s : Set α
⊢ ν s = 0 → μ₁ s = 0 ∧ μ₂ s = 0

Tactic:
hs0

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν : Measure α
h : μ₁ + μ₂ ≪ ν
s : Set α
hs0 : ν s = 0
⊢ μ₁ s = 0 ∧ μ₂ s = 0
Module: Mathlib.MeasureTheory.Measure.Comap

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s : Set α
hs : (comap f μ) s = 0
⊢ μ (f '' s) = 0

Tactic:
by
  rw [← nonpos_iff_eq_zero]
  exact (le_comap_apply f μ hfi hf s).trans hs.le

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
h₁ : s ≤ᵐ[μ] t
hsm : NullMeasurableSet s μ
h₂ : μ t = μ s
ht : μ s ≠ ∞
⊢ μ (t ∪ s) - μ s = 0

Tactic:
measure_congr (union_ae_eq_left_iff_ae_subset.mpr h₁),

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
h₁ : s ≤ᵐ[μ] t
hsm : NullMeasurableSet s μ
h₂ : μ t = μ s
ht : μ s ≠ ∞
⊢ μ t - μ s = 0
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s₁ s₂ t₁ t₂ : Set α
hs : s₁ ⊆ s₂
hsμ : μ s₂ ≤ μ s₁
ht : t₁ ⊆ t₂
htμ : μ t₂ ≤ μ t₁
⊢ μ (⋃ b, bif b then s₁ else t₁) = μ (s₂ ∪ t₂)

Tactic:
union_eq_iUnion

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s₁ s₂ t₁ t₂ : Set α
hs : s₁ ⊆ s₂
hsμ : μ s₂ ≤ μ s₁
ht : t₁ ⊆ t₂
htμ : μ t₂ ≤ μ t₁
⊢ μ (⋃ b, bif b then s₁ else t₁) = μ (⋃ b, bif b then s₂ else t₂)
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
p : α → Prop
⊢ (∀ᵐ (x : α) ∂μ.restrict (⋃ i ∈ t, s i), p x) ↔ ∀ i ∈ t, ∀ᵐ (x : α) ∂μ.restrict (s i), p x

Tactic:
simp_rw [Filter.Eventually, ae_restrict_biUnion_eq s ht, mem_iSup]

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
s : Set α
t : Set β
f : α → β
hs : MeasurableSet s
⊢ t ∈ Filter.map f (ae (μ.restrict s)) ↔ μ ((f ⁻¹' t)ᶜ ∩ s) = 0

Tactic:
rw [mem_map, mem_ae_iff, Measure.restrict_apply' hs]

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : Group β
f g : α → β
⊢ f / g =ᵐ[μ] 1 ↔ f =ᵐ[μ] g

Tactic:
refine ⟨fun h ↦ h.mono fun x hx ↦ ?_, fun h ↦ h.mono fun x hx ↦ ?_⟩
  · rwa [Pi.div_apply, Pi.one_apply, div_eq_one] at hx
  · rwa [Pi.div_apply, Pi.one_apply, div_eq_one]

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

Goal state before:
pp: case pos
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
g : α → β
hs : MeasurableSet s
h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x
x : α
hx : x ∈ s → f x = g x
hxs : x ∈ s
⊢ s.indicator f x = s.indicator g x

Tactic:
simp [hxs, hx hxs]

Goal state after:
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 α
hs : MeasurableSet s
q : (ℕ → Prop) → Prop
hq : s = ⋃ p, if q p then countablyGeneratedAtom α p else ∅
p : ℕ → Prop
hpq : q p
hpx : x ∈ countablyGeneratedAtom α p
this : p = fun x_1 ↦ x ∈ A x_1
⊢ q fun x_1 ↦ x ∈ A x_1

Tactic:
rwa [← this]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
inst✝ : LinearOrder α
f : α → β
a b : α
⊢ AEMeasurable f (μ.restrict (Ioc a b ∪ Ioc b a)) ↔
    AEMeasurable f (μ.restrict (Ioc a b)) ∧ AEMeasurable f (μ.restrict (Ioc b a))

Tactic:
aemeasurable_union_iff

Goal state after:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
inst✝ : LinearOrder α
f : α → β
a b : α
⊢ AEMeasurable f (μ.restrict (Ioc a b)) ∧ AEMeasurable f (μ.restrict (Ioc b a)) ↔
    AEMeasurable f (μ.restrict (Ioc a b)) ∧ AEMeasurable f (μ.restrict (Ioc b a))
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
μ : Measure α
g : β → γ
hf : MeasurableEmbedding f
g₁ : α → γ
hgm₁ : Measurable g₁
heq : g ∘ f =ᵐ[μ] g₁
⊢ AEMeasurable g (Measure.map f μ)

Tactic:
rcases hf.exists_measurable_extend hgm₁ fun x => ⟨g x⟩ with ⟨g₂, hgm₂, rfl⟩

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
μ : Measure α
g : β → γ
hf : MeasurableEmbedding f
g₂ : β → γ
hgm₂ : Measurable g₂
hgm₁ : Measurable (g₂ ∘ f)
heq : g ∘ f =ᵐ[μ] g₂ ∘ f
⊢ AEMeasurable g (Measure.map f μ)
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) < ∞
⊢ 0 < ↑ε / 2

Tactic:
simpa [pos_iff_ne_zero] using εpos

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

Goal state before:
pp: case mpr
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
S : Set (Set α) := ⋯
this : MeasurableSpace α := ⋯
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
ha : ∀ b < a, (Ioo b a).Nonempty
y : α
⊢ (∃ i, ∃ (_ : i ∈ t), ∃ i_1, ∃ (_ : i_1 ∈ t) (_ : i < i_1) (_ : i_1 < a), i ≤ y ∧ y ≤ i_1) → y < a

Tactic:
· rintro ⟨l, -, u, -, -, hua, -, hyu⟩
        exact hyu.trans_lt hua

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

Goal state before:
pp: case pos
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
S : Set (Set α) := {S | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
this : MeasurableSpace α := MeasurableSpace.generateFrom S
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
ha : ∀ b < a, (Ioo b a).Nonempty
⊢ MeasurableSet (⋃ l ∈ t, ⋃ u ∈ t, ⋃ (_ : l < u), ⋃ (_ : u < a), Icc l u)

Tactic:
refine MeasurableSet.biUnion hc fun a ha => MeasurableSet.biUnion hc fun b hb => ?_

Goal state after:
case pos
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
S : Set (Set α) := {S | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
this : MeasurableSpace α := MeasurableSpace.generateFrom S
a✝ : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
ha✝ : ∀ b < a✝, (Ioo b a✝).Nonempty
a : α
ha : a ∈ t
b : α
hb : b ∈ t
⊢ MeasurableSet (⋃ (_ : a < b), ⋃ (_ : b < a✝), Icc a b)
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
⊢ borel α = MeasurableSpace.generateFrom {S | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}

Tactic:
set S : Set (Set α) := { S | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S }
  refine le_antisymm ?_ (generateFrom_Icc_mem_le_borel _ _)
  let : MeasurableSpace α := generateFrom S
  rw [borel_eq_generateFrom_Iio]
  refine generateFrom_le (forall_mem_range.2 fun a => ?_)
  rcases hd.exists_countable_dense_subset_bot_top with ⟨t, hts, hc, htd, htb, -⟩
  by_cases! ha : ∀ b < a, (Ioo b a).Nonempty
  · convert_to MeasurableSet (⋃ (l ∈ t) (u ∈ t) (_ : l < u) (_ : u < a), Icc l u)
    · ext y
      push _ ∈ _
      constructor
      · intro hy
        rcases htd.exists_le' (fun b hb => htb _ hb (hbot b hb)) y with ⟨l, hlt, hly⟩
        rcases htd.exists_mem_open isOpen_Ioo (ha y hy) with ⟨u, hut, hyu, hua⟩
        exact ⟨l, hlt, u, hut, hly.trans_lt hyu, hua, hly, hyu.le⟩
      · rintro ⟨l, -, u, -, -, hua, -, hyu⟩
        exact hyu.trans_lt hua
    · refine MeasurableSet.biUnion hc fun a ha => MeasurableSet.biUnion hc fun b hb => ?_
      refine MeasurableSet.iUnion fun hab => MeasurableSet.iUnion fun _ => ?_
      exact .basic _ ⟨a, hts ha, b, hts hb, hab.le, mem_singleton _⟩
  · rcases ha with ⟨b, ba, hb⟩
    have hbs : b ∈ s := hIoo b a ba hb
    convert_to MeasurableSet (⋃ (l ∈ t) (_ : l ≤ b), Icc l b)
    · ext x
      simp only [mem_Iio, mem_iUnion, mem_Icc, exists_and_left, exists_prop]
      refine ⟨fun h ↦ ?_, fun ⟨y, yx, hy1, hy2, hy⟩ ↦ by order⟩
      have : x ≤ b := by
        contrapose! hb
        exact ⟨x, hb, h⟩
      rcases htd.exists_le' (fun b hb => htb _ hb (hbot b hb)) x with ⟨z, hzt, hzx⟩
      exact ⟨z, hzx, by order, hzt, by order⟩
    · refine .biUnion hc fun x hx => MeasurableSet.iUnion fun hlt => ?_
      exact .basic _ ⟨x, hts hx, b, hbs, hlt, mem_singleton _⟩

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s t : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEDist x s + hausdorffEDist s t < ∞
⊢ ↑ε / 2 ≠ 0

Tactic:
simpa [pos_iff_ne_zero] using εpos

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

Goal state before:
pp: case pos
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → y ∈ s
S : Set (Set α) := {S | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ico l u = S}
this : MeasurableSpace α := MeasurableSpace.generateFrom S
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
ha : ∀ b < a, (Ioo b a).Nonempty
⊢ MeasurableSet (⋃ l ∈ t, ⋃ u ∈ t, ⋃ (_ : l < u), ⋃ (_ : u ≤ a), Ico l u)

Tactic:
refine MeasurableSet.biUnion hc fun a ha => MeasurableSet.biUnion hc fun b hb => ?_

Goal state after:
case pos
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → y ∈ s
S : Set (Set α) := {S | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ico l u = S}
this : MeasurableSpace α := MeasurableSpace.generateFrom S
a✝ : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
ha✝ : ∀ b < a✝, (Ioo b a✝).Nonempty
a : α
ha : a ∈ t
b : α
hb : b ∈ t
⊢ MeasurableSet (⋃ (_ : a < b), ⋃ (_ : b ≤ a✝), Ico a b)
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mβ : TopologicalSpace β
inst✝² : MeasurableSpace β
inst✝¹ : BorelSpace β
μ : Measure α
inst✝ : IsFiniteMeasureOnCompacts μ
f : α ≃ₜ β
K : Set β
hK : IsCompact K
⊢ (map (⇑f) μ) K < ∞

Tactic:
rw [← f.toMeasurableEquiv_coe, MeasurableEquiv.map_apply]

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mβ : TopologicalSpace β
inst✝² : MeasurableSpace β
inst✝¹ : BorelSpace β
μ : Measure α
inst✝ : IsFiniteMeasureOnCompacts μ
f : α ≃ₜ β
K : Set β
hK : IsCompact K
⊢ μ (⇑f.toMeasurableEquiv ⁻¹' K) < ∞
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
hμν : μ univ = ν univ
h : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) = ν (Ico a b)
⊢ μ = ν

Tactic:
refine
    ext_of_generate_finite _ (BorelSpace.measurable_eq.trans (borel_eq_generateFrom_Ico α))
      (isPiSystem_Ico (id : α → α) id) ?_ hμν

Goal state after:
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
hμν : μ univ = ν univ
h : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) = ν (Ico a b)
⊢ ∀ s ∈ {S | ∃ l u, l < u ∧ Ico l u = S}, μ s = ν s