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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
m : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
μ : Measure α
g : β → γ
hg : Measurable g
hf : NullMeasurable f μ
⊢ NullMeasurable (g ∘ f) μ

Tactic:
rw [nullMeasurable_iff_eventuallyMeasurable]
  exact hg.comp_eventuallyMeasurable hf

Goal state after:
Module: Mathlib.Topology.Order.AtTopBotIxx

Goal state before:
pp: case neg
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
b : X
hsne : s.Nonempty
this : Nonempty ↑s
hsub : ¬s ⊆ Iio b
⊢ comap Subtype.val (𝓝[<] b) = atTop ↔ s ⊆ Iio b ∧ ∀ a < b, (s ∩ Ioo a b).Nonempty

Tactic:
suffices ¬Tendsto (↑) (atTop : Filter s) (𝓝[<] b) by
      contrapose this
      simp_all [tendsto_iff_comap]
    intro h
    rcases not_subset_iff_exists_mem_notMem.mp hsub with ⟨a, has, ha⟩
    rcases h.eventually eventually_mem_nhdsWithin |>.and (eventually_ge_atTop ⟨a, has⟩) |>.exists
      with ⟨⟨c, hcs⟩, hcb, hac⟩
    apply lt_irrefl a
    calc
      a ≤ c := by simpa using hac
      _ < b := by simpa using hcb
      _ ≤ a := by simpa using ha

Goal state after:
Module: Mathlib.Topology.Order.AtTopBotIxx

Goal state before:
pp: X : Type u_1
inst✝⁶ : LinearOrder X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : OrderTopology X
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : NoMaxOrder X
inst✝ : NoMinOrder X
f g : α → X
hl : Tendsto f atTop atTop
hu : Tendsto g atBot atBot
⊢ LocallyFinite fun n ↦ Icc (f n) (g n)

Tactic:
by
  intro x
  cases isEmpty_or_nonempty α
  · use univ
    simp [Subsingleton.elim _ (∅ : Set α)]
  obtain ⟨x_L, hx_L⟩ := exists_lt x
  obtain ⟨x_R, hx_R⟩ := exists_gt x
  obtain ⟨a_L, ha_L : ∀ a ≤ a_L, g a ≤ x_L⟩ :=
    hu.eventually_le_atBot x_L |>.exists_forall_of_atBot
  obtain ⟨a_R, ha_R : ∀ a ≥ a_R, x_R ≤ f a⟩ :=
    hl.eventually_ge_atTop x_R |>.exists_forall_of_atTop
  refine ⟨Ioo x_L x_R, Ioo_mem_nhds hx_L hx_R, (finite_Icc a_L a_R).subset ?_⟩
  rintro n ⟨y, ⟨hf, hg⟩, ⟨hxL, hxR⟩⟩
  constructor
  · contrapose! hxL
    exact hg.trans (ha_L n hxL.le)
  · contrapose! hxR
    exact (ha_R n hxR.le).trans hf

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

Goal state before:
pp: α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
e : ι → ℕ
he : Injective e
t : ℕ → Set α
ht : Function.extend e s ⊥ = t
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) t
this : μ (⋃ n, t n) = ⨆ n, μ (t n)
⊢ μ (⋃ i, s i) = ⨆ i, μ (s i)

Tactic:
by
    simp only [← ht, Function.apply_extend μ, ← iSup_eq_iUnion, iSup_extend_bot he,
      Function.comp_def, Pi.bot_apply, bot_eq_empty, measure_empty] at this
    exact this.trans (iSup_extend_bot he _)

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
⊢ ⨅ n, μ (s (x n)) = μ (⋂ n, s (x n))

Tactic:
by
      refine .symm <| (hs.comp_antitone hxm).directed_ge.measure_iInter (fun n ↦ hsm _) ?_
      rcases hfin with ⟨k, hk⟩
      rcases (hx.eventually_le_atBot k).exists with ⟨n, hn⟩
      exact ⟨n, ne_top_of_le_ne_top hk <| measure_mono <| hs hn⟩

Goal state after:
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 ∈ ae μ
a✝¹ : α
a✝ : a✝¹ ∈ s
⊢ (if a✝¹ ∈ s then f a✝¹ else g a✝¹) = f a✝¹

Tactic:
split_ifs

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 ∈ ae μ
a✝¹ : α
a✝ : a✝¹ ∈ s
⊢ f a✝¹ = f a✝¹
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_5
inst✝³ : TopologicalSpace β
inst✝² : T1Space β
inst✝¹ : SecondCountableTopology β
inst✝ : Nonempty β
f : α → β
m : OuterMeasure β := (OuterMeasure.map f) μ.toOuterMeasure
h : ∀ (b : β), m {b}ᶜ ≠ 0
inhabited_h : Inhabited β
this : m univ ≠ 0
b : β
hb : ∀ t ∈ 𝓝 b, 0 < m t
a : β
hab : a ≠ b
ha : ∀ t ∈ 𝓝 a, 0 < m t
⊢ ∃ a b, a ≠ b ∧ (∀ s ∈ 𝓝 a, 0 < μ (f ⁻¹' s)) ∧ ∀ t ∈ 𝓝 b, 0 < μ (f ⁻¹' t)

Tactic:
exact ⟨a, b, hab, ha, hb⟩

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 α
hs : MeasurableSet s
⊢ μ s = ν s

Tactic:
have : IsFiniteMeasure ν := by
    constructor
    rw [← h_univ]
    apply IsFiniteMeasure.measure_univ_lt_top
  induction s, hs using induction_on_inter hA hC with
  | empty => simp
  | basic t ht => exact hμν t ht
  | compl t htm iht =>
    rw [measure_compl (h t htm) (by finiteness), measure_compl (h t htm) (by finiteness), iht,
      h_univ]
  | iUnion f hfd hfm ihf =>
    simp [measure_iUnion, hfd, h _ (hfm _), ihf]

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

Goal state before:
pp: case pos
α : 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
this : atBot.IsCountablyGenerated
⊢ Tendsto ((⇑μ ∘ s) ∘ Subtype.val) atBot (𝓝 (μ (⋂ x, s ↑x)))

Tactic:
apply tendsto_measure_iInter_atBot

Goal state after:
case pos.hs
α : 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
this : atBot.IsCountablyGenerated
⊢ ∀ (i : { x // x ∈ Ioi a }), NullMeasurableSet (s ↑i) μ

case pos.hm
α : 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
this : atBot.IsCountablyGenerated
⊢ Monotone fun x ↦ s ↑x

case pos.hf
α : 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
this : atBot.IsCountablyGenerated
⊢ ∃ i, μ (s ↑i) ≠ ∞
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

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

Tactic:
exact LE.le.eventuallyLE (fun x hx ↦ by simp at hx ⊢; grind)

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)
⊢ μ s = ν s

Tactic:
h1

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)
⊢ μ (⋃₀ (measurableAtom '' s)) = ν (⋃₀ (measurableAtom '' s))
Module: Mathlib.MeasureTheory.Measure.Trim

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
s : Set α
hm : m ≤ m0
μ : Measure α
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
⊢ (μ.trim hm) (t ∩ s) = μ (t ∩ s)

Tactic:
trim_measurableSet_eq hm (@MeasurableSet.inter α m t s ht hs)

Goal state after:
α : Type u_1
m m0 : MeasurableSpace α
s : Set α
hm : m ≤ m0
μ : Measure α
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
⊢ μ (t ∩ s) = μ (t ∩ s)
Module: Mathlib.Data.Set.MemPartition

Goal state before:
pp: case succ
α : Type u_1
f : ℕ → Set α
a : α
n : ℕ
ih : memPartitionSet f n a ∈ memPartition f n
⊢ memPartitionSet f n a ∈ memPartition f n ∧
    ((if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n) = memPartitionSet f n a ∩ f n ∨
      (if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n) = memPartitionSet f n a \ f n)

Tactic:
split_ifs

Goal state after:
case pos
α : Type u_1
f : ℕ → Set α
a : α
n : ℕ
ih : memPartitionSet f n a ∈ memPartition f n
h✝ : a ∈ f n
⊢ memPartitionSet f n a ∈ memPartition f n ∧
    (memPartitionSet f n a ∩ f n = memPartitionSet f n a ∩ f n ∨
      memPartitionSet f n a ∩ f n = memPartitionSet f n a \ f n)

case neg
α : Type u_1
f : ℕ → Set α
a : α
n : ℕ
ih : memPartitionSet f n a ∈ memPartition f n
h✝ : a ∉ f n
⊢ memPartitionSet f n a ∈ memPartition f n ∧
    (memPartitionSet f n a \ f n = memPartitionSet f n a ∩ f n ∨
      memPartitionSet f n a \ f n = memPartitionSet f n a \ f n)
Module: Mathlib.Order.Filter.CountableSeparatingOn

Goal state before:
pp: case refine_1
α : Type u_1
l : Filter α
inst✝ : CountableInterFilter l
p : Set α → Prop
s : Set α
h : HasCountableSeparatingOn α p s
hs : s ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
S : Set (Set α)
hSc : S.Countable
hSp : ∀ s ∈ S, p s
hS : ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
⊢ s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ U ∈ S, ⋂ (_ : Uᶜ ∈ l), Uᶜ ⊆ s

pp: case refine_2
α : Type u_1
l : Filter α
inst✝ : CountableInterFilter l
p : Set α → Prop
s : Set α
h : HasCountableSeparatingOn α p s
hs : s ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
S : Set (Set α)
hSc : S.Countable
hSp : ∀ s ∈ S, p s
hS : ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
⊢ (s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ U ∈ S, ⋂ (_ : Uᶜ ∈ l), Uᶜ).Subsingleton

pp: case refine_3
α : Type u_1
l : Filter α
inst✝ : CountableInterFilter l
p : Set α → Prop
s : Set α
h : HasCountableSeparatingOn α p s
hs : s ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
S : Set (Set α)
hSc : S.Countable
hSp : ∀ s ∈ S, p s
hS : ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
⊢ s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ U ∈ S, ⋂ (_ : Uᶜ ∈ l), Uᶜ ∈ l

Tactic:
· exact fun _ h ↦ h.1.1

Goal state after:
case refine_2
α : Type u_1
l : Filter α
inst✝ : CountableInterFilter l
p : Set α → Prop
s : Set α
h : HasCountableSeparatingOn α p s
hs : s ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
S : Set (Set α)
hSc : S.Countable
hSp : ∀ s ∈ S, p s
hS : ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
⊢ (s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ U ∈ S, ⋂ (_ : Uᶜ ∈ l), Uᶜ).Subsingleton

case refine_3
α : Type u_1
l : Filter α
inst✝ : CountableInterFilter l
p : Set α → Prop
s : Set α
h : HasCountableSeparatingOn α p s
hs : s ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
S : Set (Set α)
hSc : S.Countable
hSp : ∀ s ∈ S, p s
hS : ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
⊢ s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ U ∈ S, ⋂ (_ : Uᶜ ∈ l), Uᶜ ∈ l
Module: Mathlib.Order.Filter.CountableSeparatingOn

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

Tactic:
by
  rcases s.eq_empty_or_nonempty with rfl | hne
  · exact ‹Nonempty α›.elim fun a ↦ ⟨a, mem_of_superset hs (empty_subset _)⟩
  · exact (exists_mem_singleton_mem_of_mem_of_nonempty_of_forall_separating p hs hne hl).imp fun _ ↦
      And.right

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set α
⊢ NullMeasurableSet t (μ.restrict s) ↔ NullMeasurableSet (t ∩ s) μ

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · obtain ⟨t', -, ht', t't⟩ : ∃ t' ⊇ t, MeasurableSet t' ∧ t' =ᵐ[μ.restrict s] t :=
      h.exists_measurable_superset_ae_eq
    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
    obtain ⟨s', -, hs', s's⟩ : ∃ s' ⊇ s, MeasurableSet s' ∧ s' =ᵐ[μ] s :=
      hs.exists_measurable_superset_ae_eq
    have B : (t' ∩ s' : Set α) =ᵐ[μ] (t' ∩ s : Set α) :=
      ae_eq_set_inter (EventuallyEq.refl _ _) s's
    exact (ht'.inter hs').nullMeasurableSet.congr (B.trans A)
  · have A : NullMeasurableSet (t \ s) (μ.restrict s) := by
      apply NullMeasurableSet.of_null
      rw [Measure.restrict_apply₀' hs]
      simp
    have B : NullMeasurableSet (t ∩ s) (μ.restrict s) :=
      h.mono_ac absolutelyContinuous_restrict
    simpa using A.union B

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

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

Tactic:
simp only [htq, compl_iUnion, mem_iInter, mem_compl_iff, mem_ite_empty_right, not_and,
      mem_iUnion]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
h : AEMeasurable f μ
s : Set β
hfs : ∀ (x : α), f x ∈ s
⊢ AEMeasurable (codRestrict f s hfs) μ

Tactic:
nontriviality α; inhabit α
  obtain ⟨g, g_meas, hg, fg⟩ : ∃ g : α → β, Measurable g ∧ range g ⊆ s ∧ f =ᵐ[μ] g :=
    h.exists_ae_eq_range_subset (Eventually.of_forall hfs) ⟨_, hfs default⟩
  refine ⟨codRestrict g s fun x => hg (mem_range_self _), Measurable.subtype_mk g_meas, ?_⟩
  filter_upwards [fg] with x hx
  simpa [Subtype.ext_iff]

Goal state after:
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:
by
  rcases hs with ⟨t, ht, hst⟩
  rw [← aemeasurable_congr (indicator_ae_eq_of_ae_eq_set hst.symm), aemeasurable_indicator_iff ht,
      restrict_congr_set hst]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
inst✝² : Preorder α
inst✝¹ : NoMaxOrder α
inst✝ : atTop.IsCountablyGenerated
μ : Measure α
a : α
⊢ Tendsto (fun x ↦ μ (Ico a x)) atTop (𝓝 (μ (Ici a)))

Tactic:
by
  rw [← iUnion_Ico_right]
  exact tendsto_measure_iUnion_atTop (antitone_const.Ico monotone_id)

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
r : ℝ≥0∞
⊢ infEDist x s < r ↔ ∃ y ∈ s, edist x y < r

Tactic:
simp_rw [infEDist, iInf_lt_iff, exists_prop]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
⊢ ∀ (x y : α), infEDist x s ≤ infEDist y s + 1 * edist x y

Tactic:
by
    simp only [one_mul, infEDist_le_infEDist_add_edist, forall₂_true_iff]

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

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

Tactic:
by
  simp only [hausdorffEDist_def, sup_idem, ENNReal.iSup_eq_zero]
  exact fun x hx => infEDist_zero_of_mem hx

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 < ∞
⊢ infEDist x t ≤ infEDist x s + hausdorffEDist s t + ↑ε

Tactic:
have ε0 : (ε / 2 : ℝ≥0∞) ≠ 0 := by simpa [pos_iff_ne_zero] using εpos
    have : infEDist x s < infEDist x s + ε / 2 :=
      ENNReal.lt_add_right (ENNReal.add_lt_top.1 h).1.ne ε0
    obtain ⟨y : α, ys : y ∈ s, dxy : edist x y < infEDist x s + ↑ε / 2⟩ := infEDist_lt_iff.mp this
    have : hausdorffEDist s t < hausdorffEDist s t + ε / 2 :=
      ENNReal.lt_add_right (ENNReal.add_lt_top.1 h).2.ne ε0
    obtain ⟨z : α, zt : z ∈ t, dyz : edist y z < hausdorffEDist s t + ↑ε / 2⟩ :=
      exists_edist_lt_of_hausdorffEDist_lt ys this
    calc
      infEDist x t ≤ edist x z := infEDist_le_edist_of_mem zt
      _ ≤ edist x y + edist y z := edist_triangle _ _ _
      _ ≤ infEDist x s + ε / 2 + (hausdorffEDist s t + ε / 2) := add_le_add dxy.le dyz.le
      _ = infEDist x s + hausdorffEDist s t + ε := by
        rw [add_add_add_comm, ENNReal.add_halves]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
⊢ ∃ δ, 0 < δ ∧ Disjoint (cthickening δ s) (cthickening δ t)

Tactic:
by
  obtain ⟨δ, hδ, h⟩ := hst.exists_thickenings hs ht
  refine ⟨δ / 2, half_pos hδ, h.mono ?_ ?_⟩ <;>
    exact cthickening_subset_thickening' hδ (half_lt_self hδ) _

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

Goal state before:
pp: case inl
α : Type u
inst✝ : PseudoMetricSpace α
t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ ∅, infDist x t ≤ r
H2 : ∀ x ∈ t, infDist x ∅ ≤ r
⊢ hausdorffDist ∅ t ≤ r

Tactic:
rwa [hausdorffDist_empty']

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
x : α
r : ℝ
h : x ∈ s
H : hausdorffDist s t < r
fin : hausdorffEDist s t ≠ ∞
r0 : 0 < r
this : hausdorffEDist s t < ENNReal.ofReal r
y : α
hy : y ∈ t
yr : ENNReal.ofReal (dist x y) < ENNReal.ofReal r
⊢ ∃ y ∈ t, dist x y < r

Tactic:
ENNReal.ofReal_lt_ofReal_iff r0

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
x : α
r : ℝ
h : x ∈ s
H : hausdorffDist s t < r
fin : hausdorffEDist s t ≠ ∞
r0 : 0 < r
this : hausdorffEDist s t < ENNReal.ofReal r
y : α
hy : y ∈ t
yr : dist x y < r
⊢ ∃ y ∈ t, dist x y < r
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
n : ℕ
a : α
b : ℕ
a✝ : b ∈ Finset.range n
⊢ (if hs : MeasurableSet {a | ennrealRatEmbed b ≤ f a} then
        piecewise {a | ennrealRatEmbed b ≤ f a} hs (const α (ennrealRatEmbed b)) 0
      else 0)
      a <
    ∞

Tactic:
split_ifs

Goal state after:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
n : ℕ
a : α
b : ℕ
a✝ : b ∈ Finset.range n
h✝ : MeasurableSet {a | ennrealRatEmbed b ≤ f a}
⊢ (piecewise {a | ennrealRatEmbed b ≤ f a} h✝ (const α (ennrealRatEmbed b)) 0) a < ∞

case neg
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
n : ℕ
a : α
b : ℕ
a✝ : b ∈ Finset.range n
h✝ : ¬MeasurableSet {a | ennrealRatEmbed b ≤ f a}
⊢ 0 a < ∞
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: α : 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 : α
hx : x ∈ K
this✝ : {f x} ⊆ U
δ : ℝ
hδ : 0 < δ
hthick : thickening δ {f x} ⊆ U
V : Set α := f ⁻¹' thickening (δ / 2) {f x}
this : V ∈ 𝓝 x
⊢ V ∈ 𝓝ˢ (K ∩ interior V)

Tactic:
rw [← subset_interior_iff_mem_nhdsSet]

Goal state after:
α : 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 : α
hx : x ∈ K
this✝ : {f x} ⊆ U
δ : ℝ
hδ : 0 < δ
hthick : thickening δ {f x} ⊆ U
V : Set α := f ⁻¹' thickening (δ / 2) {f x}
this : V ∈ 𝓝 x
⊢ K ∩ interior V ⊆ interior V
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
inst✝ : Countable ι
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), Measurable (f i)
⊢ Measurable (∑' (i : ι), f i)

Tactic:
convert! Measurable.ennreal_tsum h with x

Goal state after:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
inst✝ : Countable ι
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), Measurable (f i)
x : α
⊢ (∑' (i : ι), f i) x = ∑' (i : ι), f i x
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable

Goal state before:
pp: α : Type u_1
inst✝³ : MeasurableSpace α
β : Type u_3
inst✝² : MeasurableSpace β
inst✝¹ : PseudoMetricSpace β
inst✝ : BorelSpace β
μ : Measure α
g : α → β
hf : ∀ ε > 0, ∃ f, AEMeasurable f μ ∧ ∀ᵐ (x : α) ∂μ, dist (f x) (g x) ≤ ε
⊢ AEMeasurable g μ

Tactic:
by
  obtain ⟨u, -, u_pos, u_lim⟩ :
    ∃ u : ℕ → ℝ, StrictAnti u ∧ (∀ n : ℕ, 0 < u n) ∧ Tendsto u atTop (𝓝 0) :=
    exists_seq_strictAnti_tendsto (0 : ℝ)
  choose f Hf using fun n : ℕ => hf (u n) (u_pos n)
  have : ∀ᵐ x ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x)) := by
    have : ∀ᵐ x ∂μ, ∀ n, dist (f n x) (g x) ≤ u n := ae_all_iff.2 fun n => (Hf n).2
    filter_upwards [this]
    intro x hx
    rw [tendsto_iff_dist_tendsto_zero]
    exact squeeze_zero (fun n => dist_nonneg) hx u_lim
  exact aemeasurable_of_tendsto_metrizable_ae' (fun n => (Hf n).1) this

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

Goal state before:
pp: case succ
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : (nearestPtInd e N) x ≤ N
⊢ (if ∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x then N + 1 else (nearestPtInd e N) x) ≤ N + 1

Tactic:
split_ifs

Goal state after:
case pos
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : (nearestPtInd e N) x ≤ N
h✝ : ∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x
⊢ N + 1 ≤ N + 1

case neg
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : (nearestPtInd e N) x ≤ N
h✝ : ¬∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x
⊢ (nearestPtInd e N) x ≤ N + 1
Module: Mathlib.MeasureTheory.Function.SimpleFuncDense

Goal state before:
pp: case zero
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
k : ℕ
hk : k ≤ 0
⊢ edist ((nearestPt e 0) x) x ≤ edist (e k) x

Tactic:
simp [nonpos_iff_eq_zero.1 hk]

Goal state after: