mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
⊢ sign a = sign b ∨ sign a = -sign b

Tactic:
by
  rcases trichotomy (sign a) with hsa | hsa | hsa <;>
    rcases trichotomy (sign b) with hsb | hsb | hsb <;>
    simp_all

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: f : ℕ → ℝ≥0∞
hf : f 0 + ∑' (b : ℕ), f (b + 1) = ∞
hf0 : f 0 ≠ ∞
⊢ ∑' (n : ℕ), f (n + 1) = ∞

Tactic:
add_eq_top

Goal state after:
f : ℕ → ℝ≥0∞
hf : f 0 = ∞ ∨ ∑' (b : ℕ), f (b + 1) = ∞
hf0 : f 0 ≠ ∞
⊢ ∑' (n : ℕ), f (n + 1) = ∞
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: β : Type u_2
f : β → ℝ≥0
hf : Summable f
g : β → ℝ≥0
hgf : ∀ (b : β), (fun i ↦ ↑(g i)) b ≤ (fun i ↦ ↑(f i)) b
⊢ Summable g

Tactic:
exact NNReal.summable_of_le (fun b => NNReal.coe_le_coe.1 (hgf b)) hf

Goal state after:
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a b c d : EReal
⊢ a / b * (c / d) = a * (c / (b * d))

Tactic:
mul_comm b d,

Goal state after:
a b c d : EReal
⊢ a / b * (c / d) = a * (c / (d * b))
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case inr.inr.inl.inl
a c : EReal
a_top : a < ⊤
h₁ : a ≠ 0 ∨ ⊤ ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < ⊤
hc : a * ⊤ < c
b0 : 0 < ⊤
a0 : a < 0
⊢ ∃ a' ∈ Ioo a ⊤, a' * ⊤ < c

pp: case inr.inr.inl.inr.inl
c : EReal
b0 : 0 < ⊤
a_top : 0 < ⊤
h₁ : 0 ≠ 0 ∨ ⊤ ≠ ⊤
h₂ : 0 ≠ ⊤ ∨ 0 < ⊤
hc : 0 * ⊤ < c
⊢ ∃ a' ∈ Ioo 0 ⊤, a' * ⊤ < c

pp: case inr.inr.inl.inr.inr
a c : EReal
a_top : a < ⊤
h₁ : a ≠ 0 ∨ ⊤ ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < ⊤
hc : a * ⊤ < c
b0 : 0 < ⊤
a0 : 0 < a
⊢ ∃ a' ∈ Ioo a ⊤, a' * ⊤ < c

Tactic:
· obtain ⟨a', aa', a0'⟩ := exists_between a0
      rw [mul_top_of_neg a0] at hc
      refine ⟨a', mem_Ioo.2 ⟨aa', lt_top_of_lt a0'⟩, mul_top_of_neg a0' ▸ hc⟩

Goal state after:
case inr.inr.inl.inr.inl
c : EReal
b0 : 0 < ⊤
a_top : 0 < ⊤
h₁ : 0 ≠ 0 ∨ ⊤ ≠ ⊤
h₂ : 0 ≠ ⊤ ∨ 0 < ⊤
hc : 0 * ⊤ < c
⊢ ∃ a' ∈ Ioo 0 ⊤, a' * ⊤ < c

case inr.inr.inl.inr.inr
a c : EReal
a_top : a < ⊤
h₁ : a ≠ 0 ∨ ⊤ ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < ⊤
hc : a * ⊤ < c
b0 : 0 < ⊤
a0 : 0 < a
⊢ ∃ a' ∈ Ioo a ⊤, a' * ⊤ < c
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: α : Type u_3
f : Filter α
u v : α → EReal
h : limsup u f ≠ ⊥ ∨ limsup v f ≠ ⊤
h' : limsup u f ≠ ⊤ ∨ limsup v f ≠ ⊥
a : EReal
a_u : a > limsup u f
b : EReal
b_v : b > limsup v f
c : EReal
c_ab : c > a + b
x : α
a_x : u x < a
b_x : v x < b
⊢ (u + v) x < c

Tactic:
exact (add_lt_add a_x b_x).trans c_ab

Goal state after:
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case inr
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h₁ : limsup u f ≠ 0 ∨ limsup v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ limsup v f ≠ 0
h✝ : f.NeBot
⊢ limsup (u * v) f ≤ limsup u f * limsup v f

Tactic:
have u_0 : 0 ≤ limsup u f := le_limsup_of_frequently_le hu

Goal state after:
case inr
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h₁ : limsup u f ≠ 0 ∨ limsup v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ limsup v f ≠ 0
h✝ : f.NeBot
u_0 : 0 ≤ limsup u f
⊢ limsup (u * v) f ≤ limsup u f * limsup v f
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case coe.top
a✝ : ℝ
h : (↑a✝, ⊤).1 ≠ ⊤ ∨ (↑a✝, ⊤).2 ≠ ⊥
h' : (↑a✝, ⊤).1 ≠ ⊥ ∨ (↑a✝, ⊤).2 ≠ ⊤
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (↑a✝, ⊤)

Tactic:
exact continuousAt_add_coe_top _

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

Goal state before:
pp: α : Type u_4
inst✝³ : TopologicalSpace α
β : Type u_5
f : α → β
a : α
inst✝² : PartialOrder β
inst✝¹ : CommGroup β
inst✝ : IsOrderedMonoid β
⊢ LowerSemicontinuousAt f⁻¹ a ↔ UpperSemicontinuousAt f a

Tactic:
simp [← lowerSemicontinuousWithinAt_univ_iff, ← upperSemicontinuousWithinAt_univ_iff]

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

Goal state before:
pp: α : Type u_4
inst✝³ : TopologicalSpace α
β : Type u_5
f : α → β
a : α
inst✝² : PartialOrder β
inst✝¹ : CommGroup β
inst✝ : IsOrderedMonoid β
⊢ UpperSemicontinuousAt f⁻¹ a ↔ LowerSemicontinuousAt f a

Tactic:
simp [← lowerSemicontinuousWithinAt_univ_iff, ← upperSemicontinuousWithinAt_univ_iff]

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_1
ι : Sort u_3
ι' : Sort u_4
inst✝ : LinearOrder α
Ixx : α → α → Set α
p : α → α → Prop
Hne : ∀ {a b : α}, (Ixx a b).Nonempty → p a b
Hi : ∀ {a₁ b₁ a₂ b₂ : α}, Ixx a₁ b₁ ∩ Ixx a₂ b₂ = Ixx (max a₁ a₂) (min b₁ b₂)
f : ι → α
g : ι' → α
⊢ IsPiSystem {S | ∃ i j, p (f i) (g j) ∧ Ixx (f i) (g j) = S}

Tactic:
simpa only [exists_range_iff] using isPiSystem_Ixx_mem (@Hne) (@Hi) (range f) (range g)

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ₁ μ₂ : Measure α
h : ∀ (s : Set α), MeasurableSet s → μ₁ s = μ₂ s
⊢ μ₁.toOuterMeasure = μ₂.toOuterMeasure

Tactic:
by
  rw [← trimmed, OuterMeasure.trim_congr (h _), trimmed]

Goal state after:
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 α
⊢ (∀ᵐ (x : α) ∂μ, x ∈ s → x ∈ t) ↔ μ (s \ t) = 0

Tactic:
simp [ae_iff]

Goal state after:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
⊢ μ {a | a ∈ s ∧ a ∉ t} = 0 ↔ μ (s \ t) = 0
Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
⊢ s ⊆ toMeasurable μ s

Tactic:
rw [toMeasurable_def]

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
⊢ s ⊆
    if h : ∃ t ⊇ s, MeasurableSet t ∧ t =ᵐ[μ] s then h.choose
    else
      if h' : ∃ t ⊇ s, MeasurableSet t ∧ ∀ (u : Set α), MeasurableSet u → μ (t ∩ u) = μ (s ∩ u) then h'.choose
      else ⋯.choose
Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
⊢ MeasurableSet (toMeasurable μ s)

Tactic:
rw [toMeasurable_def]

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
⊢ MeasurableSet
    (if h : ∃ t ⊇ s, MeasurableSet t ∧ t =ᵐ[μ] s then h.choose
    else
      if h' : ∃ t ⊇ s, MeasurableSet t ∧ ∀ (u : Set α), MeasurableSet u → μ (t ∩ u) = μ (s ∩ u) then h'.choose
      else ⋯.choose)
Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
⊢ μ (toMeasurable μ s) = μ s

Tactic:
rw [toMeasurable_def]

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
⊢ μ
      (if h : ∃ t ⊇ s, MeasurableSet t ∧ t =ᵐ[μ] s then h.choose
      else
        if h' : ∃ t ⊇ s, MeasurableSet t ∧ ∀ (u : Set α), MeasurableSet u → μ (t ∩ u) = μ (s ∩ u) then h'.choose
        else ⋯.choose) =
    μ s
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst✝¹ : MeasurableSpace α
f : ι → Filter α
inst✝ : ∀ (i : ι), (f i).IsMeasurablyGenerated
⊢ (⨅ i, f i).IsMeasurablyGenerated

Tactic:
by
  refine ⟨fun s hs => ?_⟩
  rw [← Equiv.plift.surjective.iInf_comp, mem_iInf] at hs
  rcases hs with ⟨t, ht, ⟨V, hVf, rfl⟩⟩
  choose U hUf hU using fun i => IsMeasurablyGenerated.exists_measurable_subset (hVf i)
  refine ⟨⋂ i : t, U i, ?_, ?_, ?_⟩
  · rw [← Equiv.plift.surjective.iInf_comp, mem_iInf]
    exact ⟨t, ht, U, hUf, rfl⟩
  · have := ht.countable.toEncodable.countable
    exact MeasurableSet.iInter fun i => (hU i).1
  · exact iInter_mono fun i => (hU i).2

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β
g : β → γ
hf' : ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)
hg : Injective g
hg' : ∀ (s : Set β), MeasurableSet s → MeasurableSet (g '' s)
μ : Measure γ
hf : Injective f
⊢ comap f (comap g μ) = comap (g ∘ f) μ

Tactic:
ext s hs
    rw [comap_apply _ hf hf' _ hs, comap_apply _ hg hg' _ (hf' _ hs),
      comap_apply _ (hg.comp hf) (fun t ht ↦ image_comp g f _ ▸ hg' _ <| hf' _ ht) _ hs, image_comp]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
s : Set β
f : β → Set α
hs : s.Countable
hd : s.Pairwise (AEDisjoint μ on f)
h : ∀ b ∈ s, NullMeasurableSet (f b) μ
this : Encodable ↑s
⊢ μ (⋃ b ∈ s, f b) = ∑' (p : ↑s), μ (f ↑p)

Tactic:
rw [biUnion_eq_iUnion]

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
s : Set β
f : β → Set α
hs : s.Countable
hd : s.Pairwise (AEDisjoint μ on f)
h : ∀ b ∈ s, NullMeasurableSet (f b) μ
this : Encodable ↑s
⊢ μ (⋃ x, f ↑x) = ∑' (p : ↑s), μ (f ↑p)
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s₁ s₂ s₃ : Set α
h12 : s₁ ⊆ s₂
h23 : s₂ ⊆ s₃
h_nullsdiff : μ (s₃ \ s₁) = 0
le12 : μ s₁ ≤ μ s₂
le23 : μ s₂ ≤ μ s₃
⊢ μ s₃ = μ (s₃ \ s₁ ∪ s₁)

Tactic:
rw [sdiff_union_of_subset (h12.trans h23)]

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

Goal state before:
pp: α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : ι → Set α
t : Set ι
ht : t.Countable
hd : DirectedOn ((fun x1 x2 ↦ x1 ⊆ x2) on s) t
this : Countable ↑t
⊢ ⨆ i, μ (s ↑i) = ⨆ i ∈ t, μ (s i)

Tactic:
← iSup_subtype''

Goal state after:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : ι → Set α
t : Set ι
ht : t.Countable
hd : DirectedOn ((fun x1 x2 ↦ x1 ⊆ x2) on s) t
this : Countable ↑t
⊢ ⨆ i, μ (s ↑i) = ⨆ i, μ (s ↑i)
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 fun x ↦ ω ∈ s x
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
i : ι
hi : μ (s i) ≠ ∞
this : Nonempty ι
t : ι → Set α := fun i ↦ s i ∩ {ω | Monotone fun x ↦ ω ∈ s x}
⊢ μ (⋂ i, s i) = ⨅ i, μ (s i)

Tactic:
have hst (i : ι) : s i =ᵐ[μ] t i := by
    filter_upwards [hs] with ω hω
    suffices ω ∈ s i ↔ ω ∈ t i from propext this
    simpa [t] using fun _ ↦ hω

Goal state after:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsCodirectedOrder ι
inst✝ : atBot.IsCountablyGenerated
s : ι → Set α
hs : ∀ᵐ (ω : α) ∂μ, Monotone fun x ↦ ω ∈ s x
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
i : ι
hi : μ (s i) ≠ ∞
this : Nonempty ι
t : ι → Set α := fun i ↦ s i ∩ {ω | Monotone fun x ↦ ω ∈ s x}
hst : ∀ (i : ι), s i =ᵐ[μ] t i
⊢ μ (⋂ i, s i) = ⨅ i, μ (s i)
Module: Mathlib.MeasureTheory.Measure.Restrict

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

Tactic:
rw [Directed.measure_iUnion]

Goal state after:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
t : Set α
ht : MeasurableSet t
⊢ Directed (fun x1 x2 ↦ x1 ⊆ x2) fun i ↦ t ∩ s i
Module: Mathlib.MeasureTheory.Measure.Trim

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
⊢ μ s ≤ (μ.trim hm) s

Tactic:
simp_rw [Measure.trim]
  exact @le_toMeasure_apply _ m _ _ _

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

Goal state before:
pp: α : Type u_1
ms : MeasurableSpace α
μ : OuterMeasure α
h : ms ≤ μ.caratheodory
⊢ μ = 0 → μ.toMeasure h = 0

Tactic:
by rintro rfl; simp

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

Goal state before:
pp: α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
inst✝ : Countable ι
μ : ι → Measure α
s t : Set α
ht : MeasurableSet t
⊢ ((sum μ).restrict s) t = (sum fun i ↦ (μ i).restrict s) t

Tactic:
simp_rw [sum_apply _ ht, restrict_apply ht, sum_apply_of_countable]

Goal state after:
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
⊢ ⨆ i, ae (μ.restrict (s ↑i)) = ⨆ i ∈ t, ae (μ.restrict (s i))

Tactic:
← iSup_subtype''

Goal state after:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
s : ι → Set α
t : Set ι
ht : t.Countable
this : Countable ↑t
⊢ ⨆ i, ae (μ.restrict (s ↑i)) = ⨆ i, ae (μ.restrict (s ↑i))
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ₁ μ₂ : Measure α
h : ∀ (s : Set α), MeasurableSet s → s.Nonempty → μ₁ s ≤ μ₂ s
s : Set α
hs : MeasurableSet s
⊢ s = ∅ → μ₁ s ≤ μ₂ s

Tactic:
by rintro rfl; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
m : Set (Measure α)
x✝ : MeasurableSpace α
f : ℕ → Set α
a✝¹ : ∀ (i : ℕ), MeasurableSet (f i)
a✝ : Pairwise (Disjoint on f)
hne : (⋃ i, f i).Nonempty
⊢ ∑' (i : ℕ), ⊤ (f i) ≤ ⊤ (⋃ i, f i)

Tactic:
OuterMeasure.top_apply hne

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
m : Set (Measure α)
x✝ : MeasurableSpace α
f : ℕ → Set α
a✝¹ : ∀ (i : ℕ), MeasurableSet (f i)
a✝ : Pairwise (Disjoint on f)
hne : (⋃ i, f i).Nonempty
⊢ ∑' (i : ℕ), ⊤ (f i) ≤ ∞
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
⊢ ∃ q, s = ⋃ p, if q p then countablyGeneratedAtom α p else ∅

Tactic:
refine generateFrom_induction (range (natGeneratingSequence α)) _ ?_ ?_ ?_ ?_ s hs

Goal state after:
case refine_1
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
⊢ ∀ t ∈ range (natGeneratingSequence α), MeasurableSet t → ∃ q, t = ⋃ p, if q p then countablyGeneratedAtom α p else ∅

case refine_2
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
⊢ ∃ q, ∅ = ⋃ p, if q p then countablyGeneratedAtom α p else ∅

case refine_3
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
⊢ ∀ (t : Set α),
    MeasurableSet t →
      (∃ q, t = ⋃ p, if q p then countablyGeneratedAtom α p else ∅) →
        ∃ q, tᶜ = ⋃ p, if q p then countablyGeneratedAtom α p else ∅

case refine_4
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
⊢ ∀ (s : ℕ → Set α),
    (∀ (n : ℕ), MeasurableSet (s n)) →
      (∀ (n : ℕ), ∃ q, s n = ⋃ p, if q p then countablyGeneratedAtom α p else ∅) →
        ∃ q, ⋃ i, s i = ⋃ p, if q p then countablyGeneratedAtom α p else ∅
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: case refine_2
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
a✝ : Nontrivial β
inhabited_h : Inhabited β
S : Set (Set β)
hSc : S.Countable
hc : MeasurableSpace.CountablyGenerated β
h : NullMeasurable f μ
T : Set β → Set α
hTf : ∀ s ∈ S, T s ⊆ f ⁻¹' s
hTm : ∀ s ∈ S, MeasurableSet (T s)
hTeq : ∀ s ∈ S, T s =ᵐ[μ] f ⁻¹' s
U : Set β → Set α
hUf : ∀ s ∈ S, U s ⊇ f ⁻¹' s
hUm : ∀ s ∈ S, MeasurableSet (U s)
hUeq : ∀ s ∈ S, U s =ᵐ[μ] f ⁻¹' s
v : Set α := ⋃ s ∈ S, U s \ T s
hvm : MeasurableSet v
hvμ : μ v = 0
⊢ Measurable (vᶜ.domRestrict (v.piecewise (fun x ↦ default) f))

Tactic:
rw [domRestrict_piecewise_compl, domRestrict_eq]
    refine measurable_generateFrom fun s hs ↦ .of_subtype_image ?_
    rw [preimage_comp, Subtype.image_preimage_coe]
    convert! (hTm s hs).diff hvm using 1
    rw [inter_comm]
    refine Set.ext fun x ↦ and_congr_left fun hxv ↦ ⟨fun hx ↦ ?_, fun hx ↦ hTf s hs hx⟩
    exact by_contra fun hx' ↦ hxv <| mem_biUnion hs ⟨hUf s hs hx, hx'⟩

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

Goal state before:
pp: case inr
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
f : α → β
t : Set β
inst✝ : MeasurableSpace.CountablyGenerated ↑t
h : NullMeasurable f μ
hft : ∀ᵐ (x : α) ∂μ, f x ∈ t
hne : t.Nonempty
⊢ AEMeasurable f μ

Tactic:
← μ.ae_completion

Goal state after:
case inr
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
f : α → β
t : Set β
inst✝ : MeasurableSpace.CountablyGenerated ↑t
h : NullMeasurable f μ
hft : ∀ᵐ (x : α) ∂μ.completion, f x ∈ t
hne : t.Nonempty
⊢ AEMeasurable f μ
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case mp
α : 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 : α
⊢ y < a → ∃ i, ∃ (_ : i ∈ t), ∃ i_1, ∃ (_ : i_1 ∈ t) (_ : i < i_1) (_ : i_1 < a), i ≤ y ∧ y ≤ i_1

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:
· 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⟩

Goal state after:
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
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
⊢ hausdorffEDist s (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) = 0

Tactic:
by
  rw [hausdorffEDist_zero_iff_closure_eq_closure, closure_closure]

Goal state after:
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 : α ≃ₜ β
⊢ IsFiniteMeasureOnCompacts (map (⇑f) μ)

Tactic:
by
  refine ⟨fun K hK ↦ ?_⟩
  rw [← f.toMeasurableEquiv_coe, MeasurableEquiv.map_apply]
  exact IsCompact.measure_lt_top (f.isCompact_preimage.2 hK)

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
E : Set α
x : α
h : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEDist x E
⊢ ∀ᶠ (δ : ℝ) in 𝓝 0, x ∉ thickening δ E

Tactic:
filter_upwards [eventually_lt_nhds ε_pos] with δ hδ

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
E : Set α
x : α
h : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEDist x E
δ : ℝ
hδ : δ < ε
⊢ x ∉ thickening δ E
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
hs : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
⊢ hausdorffEDist s t = 0 ↔ s = t

Tactic:
by
  rw [hausdorffEDist_zero_iff_closure_eq_closure, hs.closure_eq, ht.closure_eq]

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

Goal state before:
pp: X : Type u
inst✝ : PseudoMetricSpace X
δ : ℝ
x : X
⊢ thickening δ {x} = ball x δ

Tactic:
by
  ext
  simp [mem_thickening_iff]

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

Goal state before:
pp: case inr
X : Type u
inst✝ : PseudoMetricSpace X
δ : ℝ
E : Set X
h : Bornology.IsBounded E
x : X
hx : x ∈ E
⊢ Bornology.IsBounded (thickening δ E)

Tactic:
refine (isBounded_iff_subset_closedBall x).2 ⟨δ + diam E, fun y hy ↦ ?_⟩

Goal state after:
case inr
X : Type u
inst✝ : PseudoMetricSpace X
δ : ℝ
E : Set X
h : Bornology.IsBounded E
x : X
hx : x ∈ E
y : X
hy : y ∈ thickening δ E
⊢ y ∈ closedBall x (δ + diam E)
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
E : Set α
x : α
h : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEDist x E
⊢ ∀ᶠ (δ : ℝ) in 𝓝 0, x ∉ cthickening δ E

Tactic:
filter_upwards [eventually_lt_nhds ε_pos] with δ hδ

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
E : Set α
x : α
h : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEDist x E
δ : ℝ
hδ : δ < ε
⊢ x ∉ cthickening δ E
Module: Mathlib.Topology.Instances.Real.Lemmas

Goal state before:
pp: f : ℕ → ℝ
k : ℕ
x : ℝ
h_tto : Tendsto f atTop (𝓝 x)
h_ant : AntitoneOn f (Ici k)
h_bdd : BddBelow (f '' Ici k)
⊢ IsGLB (f '' Ici k) x

Tactic:
rw [tendsto_nhds_unique h_tto
    (Real.tendsto_atTop_csInf_of_antitoneOn_bddBelow_nat_Ici h_ant h_bdd)]
  exact isGLB_csInf (image_nonempty.mpr nonempty_Ici) h_bdd

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

Goal state before:
pp: a : ℝ
this : IsLUB (range Rat.cast ∩ Iio a) a
⊢ MeasurableSet (Iio a)

Tactic:
← this.biUnion_Iio_eq,

Goal state after:
a : ℝ
this : IsLUB (range Rat.cast ∩ Iio a) a
⊢ MeasurableSet (⋃ x ∈ range Rat.cast ∩ Iio a, Iio x)
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: case hf
μ : Measure ℝ
inst✝ : IsFiniteMeasureOnCompacts μ
b : ℝ
⊢ ∃ r > 0, μ (Icc (b - r) (b + r)) ≠ ∞

Tactic:
· exact ⟨1, zero_lt_one, isCompact_Icc.measure_ne_top⟩

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✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_5
ι' : Type u_6
f : ι → δ → α
v : Filter ι
hf : ∀ (i : ι), Measurable (f i)
p : ι' → Prop
s : ι' → Set ι
hv : v.HasCountableBasis p s
hs : ∀ (j : ι'), (s j).Countable
this✝¹ : Countable (Subtype p)
hp : Nonempty (Subtype p)
H : ¬∃ j, s ↑j = ∅
this✝ : ∀ (i : ι'), Countable ↑(s i)
m : Subtype p → Set δ := fun j ↦ {x | BddBelow (range fun i ↦ f (↑i) x)}
m_meas : ∀ (j : Subtype p), MeasurableSet (m j)
mc_meas : MeasurableSet {x | ∀ (j : Subtype p), x ∉ m j}
j : Subtype p
reparam : δ → Subtype p → Subtype p := fun x ↦ liminfReparam (fun i ↦ f i x) s p
F0 : Subtype p → δ → α := fun j x ↦ ⨅ i, f (↑i) x
F0_meas : ∀ (j : Subtype p), Measurable (F0 j)
F1 : δ → α := fun x ↦ F0 (reparam x j) x
hF1 : F1 = fun x ↦ F0 (reparam x j) x
g : ℕ → Subtype p := Classical.choose ⋯
Z : ∀ (x : δ), ∃ n, x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k
this : F1 = fun x ↦ if x ∈ m j then F0 j x else F0 (g (Nat.find ⋯)) x
n : ℕ
⊢ MeasurableSet {x | x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k}

Tactic:
exact (m_meas (g n)).union mc_meas

Goal state after: