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

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
ι : Sort u_2
inst✝ : Countable ι
μ : ι → OuterMeasure α
s t : Set α
left✝¹ : s ⊆ t
left✝ : MeasurableSet t
hμt : (⨆ i, μ i.down) t = (⨆ i, μ i.down).trim s ∧ ∀ (x : PLift ι), ((μ ∘ PLift.down) x) t = ((μ ∘ PLift.down) x).trim s
⊢ (⨆ i, μ i.down).trim s = (⨆ i, (μ i.down).trim) s

Tactic:
simp only [iSup_apply, ← hμt.1]

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
ι : Sort u_2
inst✝ : Countable ι
μ : ι → OuterMeasure α
s t : Set α
left✝¹ : s ⊆ t
left✝ : MeasurableSet t
hμt : (⨆ i, μ i.down) t = (⨆ i, μ i.down).trim s ∧ ∀ (x : PLift ι), ((μ ∘ PLift.down) x) t = ((μ ∘ PLift.down) x).trim s
⊢ ⨆ i, (μ i.down) t = ⨆ i, (μ i.down).trim s
Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν ν' : Measure α
h1 : μ₁ ≪ ν
h2 : μ₂ ≪ ν'
s : Set α
hs : (ν + ν') s = 0
⊢ (μ₁ + μ₂) s = 0

Tactic:
simp only [coe_add, Pi.add_apply, add_eq_zero] at hs ⊢

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν ν' : Measure α
h1 : μ₁ ≪ ν
h2 : μ₂ ≪ ν'
s : Set α
hs : ν s = 0 ∧ ν' s = 0
⊢ μ₁ s = 0 ∧ μ₂ s = 0
Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous

Goal state before:
pp: case refine_1
α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν : Measure α
h : μ₁ + μ₂ ≪ ν
this : ∀ (s : Set α), ν s = 0 → μ₁ s = 0 ∧ μ₂ s = 0
⊢ μ₁ ≪ ν ∧ μ₂ ≪ ν

Tactic:
exact ⟨fun s hs0 ↦ (this s hs0).1, fun s hs0 ↦ (this s hs0).2⟩

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h1 : μ ≪ ν
ν' : Measure α
s : Set α
hs : (ν + ν') s = 0
⊢ μ s = 0

Tactic:
simp only [coe_add, Pi.add_apply, add_eq_zero] at hs ⊢

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h1 : μ ≪ ν
ν' : Measure α
s : Set α
hs : ν s = 0 ∧ ν' s = 0
⊢ μ s = 0
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).symm ⁻¹' s =ᵐ[μ] s

Tactic:
obtain ⟨k, rfl | rfl⟩ := k.eq_nat_or_neg

Goal state after:
case inl
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving (⇑e) μ μ
he' : QuasiMeasurePreserving (⇑e.symm) μ μ
hs : ⇑e '' s =ᵐ[μ] s
k : ℕ
⊢ ⇑(e ^ ↑k).symm ⁻¹' s =ᵐ[μ] s

case inr
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving (⇑e) μ μ
he' : QuasiMeasurePreserving (⇑e.symm) μ μ
hs : ⇑e '' s =ᵐ[μ] s
k : ℕ
⊢ ⇑(e ^ (-↑k)).symm ⁻¹' s =ᵐ[μ] s
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hs : μ s = ∞
ht : μ t ≠ ∞
⊢ μ (s \ t) = ∞

Tactic:
by
  contrapose! hs
  exact ((measure_mono (subset_sdiff_union s t)).trans_lt
    ((measure_union_le _ _).trans_lt (ENNReal.add_lt_top.2 ⟨hs.lt_top, ht.lt_top⟩))).ne

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
⊢ μ (s₁ ∩ s₂) + μ (s₁ \ s₂) ≤ μ s₂ + μ (s₁ \ s₂)

Tactic:
gcongr; apply inter_subset_right

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
h : Tendsto Subtype.val atTop (𝓝[<] b)
a : X
has : a ∈ s
ha : a ∉ Iio b
c : X
hcs : c ∈ s
hcb : ↑⟨c, hcs⟩ ∈ Iio b
hac : ⟨a, has⟩ ≤ ⟨c, hcs⟩
⊢ False

Tactic:
apply lt_irrefl a

Goal state after:
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
h : Tendsto Subtype.val atTop (𝓝[<] b)
a : X
has : a ∈ s
ha : a ∉ Iio b
c : X
hcs : c ∈ s
hcb : ↑⟨c, hcs⟩ ∈ Iio b
hac : ⟨a, has⟩ ≤ ⟨c, hcs⟩
⊢ a < a
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
⊢ s ∪ t =ᵐ[μ] t ↔ s ≤ᵐ[μ] t

Tactic:
rw [union_comm, union_ae_eq_left_iff_ae_subset]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
μ ν : Measure α
s t : Set α
a : α
⊢ 0 = sum fun x ↦ 0

Tactic:
rw [Measure.sum_zero]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
μ ν : Measure α
s t : Set α
a : α
⊢ 0 = sum fun x ↦ 0

Tactic:
by rw [Measure.sum_zero]

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)
h_count : (measurableAtom '' s).Countable
⊢ μ (⋃₀ (measurableAtom '' s)) = ν (⋃₀ (measurableAtom '' s))

Tactic:
have h_disj : (measurableAtom '' s).Pairwise Disjoint := by
    intro t ht t' ht' h_eq
    obtain ⟨y, hys, hy⟩ := ht
    obtain ⟨y', hy's, hy'⟩ := ht'
    rw [← hy, ← hy'] at h_eq ⊢
    refine disjoint_measurableAtom_of_notMem fun hyy' ↦ h_eq ?_
    exact measurableAtom_eq_of_mem hyy'

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)
h_count : (measurableAtom '' s).Countable
h_disj : (measurableAtom '' s).Pairwise Disjoint
⊢ μ (⋃₀ (measurableAtom '' s)) = ν (⋃₀ (measurableAtom '' s))
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:

Tactic:
μ (t ∩ disjointed w n) ≤ μ (t ∩ w n) := by
            gcongr
            exact disjointed_le w n
          _ ≤ μ (w n) := measure_mono inter_subset_right
          _ < ∞ := hw n

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
⊢ ⨆ i, μ (spanningSets μ i ∩ s) = ⨆ i, μ (toMeasurable μ s ∩ spanningSets μ i)

Tactic:
← restrict_apply (measurableSet_spanningSets μ _),

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
⊢ ⨆ i, (μ.restrict s) (spanningSets μ i) = ⨆ i, μ (toMeasurable μ s ∩ spanningSets μ i)
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: δ : Type u_4
u : Set δ
inst✝ : MeasureSpace δ
hu : NullMeasurableSet u volume
⊢ (comap Subtype.val volume) univ = volume u

Tactic:
comap_apply₀ _ _ _ _ MeasurableSet.univ.nullMeasurableSet

Goal state after:
δ : Type u_4
u : Set δ
inst✝ : MeasureSpace δ
hu : NullMeasurableSet u volume
⊢ volume (Subtype.val '' univ) = volume u

δ : Type u_4
u : Set δ
inst✝ : MeasureSpace δ
hu : NullMeasurableSet u volume
⊢ Injective Subtype.val

δ : Type u_4
u : Set δ
inst✝ : MeasureSpace δ
hu : NullMeasurableSet u volume
⊢ ∀ (s : Set { x // x ∈ u }), MeasurableSet s → NullMeasurableSet (Subtype.val '' s) volume
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: case refine_1.refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
x✝ : μ (t ∩ s) + ν (tᶜ ∩ s) ∈ {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)}
t' : ℕ → Set α := fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
ht' : t' = fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
⊢ (min (μ (t' 0)) (ν (t' 0)) + ∑' (x : ℕ), if x = 0 then 0 else min (μ (t' x)) (ν (t' x))) ≤ μ (t ∩ s) + ν (tᶜ ∩ s)

Tactic:
tsum_eq_add_tsum_ite 1,

Goal state after:
case refine_1.refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
x✝ : μ (t ∩ s) + ν (tᶜ ∩ s) ∈ {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)}
t' : ℕ → Set α := fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
ht' : t' = fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
⊢ min (μ (t' 0)) (ν (t' 0)) +
      ((if 1 = 0 then 0 else min (μ (t' 1)) (ν (t' 1))) +
        ∑' (x : ℕ), if x = 1 then 0 else if x = 0 then 0 else min (μ (t' x)) (ν (t' x))) ≤
    μ (t ∩ s) + ν (tᶜ ∩ s)
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: case neg
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
t : Set β
ht : 0 ∉ t
⊢ t ∈ Filter.map (s.indicator f) (ae μ) → t ∈ Filter.map f (ae (μ.restrict s))

Tactic:
mem_map_indicator_ae_iff_of_zero_notMem ht,

Goal state after:
case neg
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
t : Set β
ht : 0 ∉ t
⊢ μ ((f ⁻¹' t)ᶜ ∪ sᶜ) = 0 → t ∈ Filter.map f (ae (μ.restrict s))
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
f : α → β
h : NeZero (Measure.map f μ)
⊢ AEMeasurable f μ

Tactic:
by_contra h'

Goal state after:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
f : α → β
h : NeZero (Measure.map f μ)
h' : ¬AEMeasurable f μ
⊢ False
Module: Mathlib.MeasureTheory.Order.Lattice

Goal state before:
pp: α : Type u_2
m : MeasurableSpace α
δ : Type u_3
inst✝² : MeasurableSpace δ
inst✝¹ : SemilatticeSup α
inst✝ : MeasurableSup₂ α
f : ℕ → δ → α
n : ℕ
hf : ∀ k ≤ n, Measurable (f k)
⊢ Measurable ((range (n + 1)).sup' ⋯ f)

Tactic:
refine Finset.measurable_sup' _ ?_
  simpa [Finset.mem_range]

Goal state after:
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
a✝ : Nontrivial α
inhabited_h : Inhabited α
g : α → β
g_meas : Measurable g
hg : range g ⊆ s
fg : f =ᵐ[μ] g
x : α
hx : f x = g x
⊢ codRestrict f s hfs x = codRestrict g s ⋯ x

Tactic:
simpa [Subtype.ext_iff]

Goal state after:
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

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:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

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

Tactic:
rcases hy with ⟨a, ⟨b, -, yb, hb⟩, -, ya⟩

Goal state after:
case h₂
α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s✝ t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : OpensMeasurableSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : OpensMeasurableSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : TopologicalSpace γ₂
inst✝² : MeasurableSpace γ₂
inst✝¹ : BorelSpace γ₂
inst✝ : MeasurableSpace δ
h : SecondCountableTopologyEither α β
s : Set (α × β)
hs : IsOpen[instTopologicalSpaceProd] s
hβ : SecondCountableTopology β
F : Set β → Set α := fun a ↦ {y | ∃ b, IsOpen[inst✝¹²] b ∧ y ∈ b ∧ b ×ˢ a ⊆ s}
A : ∀ (a : Set β), IsOpen[inst✝¹²] (F a)
y1 : α
y2 : β
a : Set β
b : Set α
yb : y1 ∈ b
hb : b ×ˢ a ⊆ s
ya : y2 ∈ a
⊢ (y1, y2) ∈ s
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case neg
α : 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
b : α
ba : b < a
hb : Ioo b a = ∅
hbs : b ∈ s
⊢ MeasurableSet (⋃ l ∈ t, ⋃ (_ : l ≤ b), Icc l b)

Tactic:
refine .biUnion hc fun x hx => MeasurableSet.iUnion fun hlt => ?_

Goal state after:
case neg
α : 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
b : α
ba : b < a
hb : Ioo b a = ∅
hbs : b ∈ s
x : α
hx : x ∈ t
hlt : x ≤ b
⊢ MeasurableSet (Icc x b)
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case neg
α : 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 : a ∈ s
⊢ MeasurableSet (⋃ l ∈ t, ⋃ (_ : l < a), Ico l a)

Tactic:
refine .biUnion hc fun x hx => MeasurableSet.iUnion fun hlt => ?_

Goal state after:
case neg
α : 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 : a ∈ s
x : α
hx : x ∈ t
hlt : x < a
⊢ MeasurableSet (Ico x a)
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: α : Type u
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : ProperSpace α
hne : s.Nonempty
x : α
⊢ ∃ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s, infDist x s = dist x y

Tactic:
simpa only [infDist_closure] using isClosed_closure.exists_infDist_eq_dist hne.closure x

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

Goal state before:
pp: case pos
α : Type u
inst✝ : PseudoEMetricSpace α
E : Set α
s : Set ℝ
hs : ∀ (ε : ℝ), 0 < ε → (s ∩ Ioc 0 ε).Nonempty
hs₀ : s ⊆ Ioi 0
⊢ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E = ⋂ δ ∈ s, cthickening δ E

Tactic:
rw [← cthickening_zero]
    apply cthickening_eq_iInter_cthickening' _ hs₀ hs

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, infDist x t ≤ r
H2 : ∀ x ∈ t, infDist x s ≤ r
hs : s.Nonempty
ht : t.Nonempty
⊢ ∀ x ∈ s, infEDist x t ≤ ENNReal.ofReal r

pp: α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, infDist x t ≤ r
H2 : ∀ x ∈ t, infDist x s ≤ r
hs : s.Nonempty
ht : t.Nonempty
⊢ ∀ x ∈ t, infEDist x s ≤ ENNReal.ofReal r

Tactic:
· simpa only [infDist, ← ENNReal.le_ofReal_iff_toReal_le (infEDist_ne_top ht) hr] using H1

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, infDist x t ≤ r
H2 : ∀ x ∈ t, infDist x s ≤ r
hs : s.Nonempty
ht : t.Nonempty
⊢ ∀ x ∈ t, infEDist x s ≤ ENNReal.ofReal r
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: β : Type u_2
α : Type u_5
f : α →ₛ β
inst✝ : Nonempty β
⊢ ∃ c, ∀ (x : α), f x = c

Tactic:
by
  have hf_meas := @SimpleFunc.measurableSet_fiber α _ ⊥ f
  simp_rw [MeasurableSpace.measurableSet_bot_iff] at hf_meas
  exact (exists_eq_const_of_preimage_singleton hf_meas).imp fun c hc ↦ congr_fun hc

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

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

Tactic:
simpa [add_comm, hausdorffDist_comm] using I

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'
hι : IsEmpty ι
x : δ
hx : x ∈ s
A : ∀ b ∈ s, IsBot (g b)
⊢ ∀ b ∈ s, g b = g x

Tactic:
intro b

Goal state after:
α : 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'
hι : IsEmpty ι
x : δ
hx : x ∈ s
A : ∀ b ∈ s, IsBot (g b)
b : δ
⊢ b ∈ s → g b = g x
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case inr
α : 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 : δ), IsLUB {a | ∃ i, f' i b = a} (g b)

Tactic:
intro b

Goal state after:
case inr
α : 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 : δ
⊢ IsLUB {a | ∃ i, f' i b = a} (g b)
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
n : ℕ
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:
intro b

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
n : ℕ
a : α
b : ℕ
⊢ 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 <
      ∞
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
μ : 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 : δ), IsLUB {a | ∃ i, aeSeq hf p i b = a} (g_seq b)

Tactic:
intro b

Goal state after:
α : 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 : δ
⊢ IsLUB {a | ∃ i, aeSeq hf p i b = a} (g_seq b)
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: case refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs : ∀ (x : α), f x ≠ 0 → μ (⇑f ⁻¹' {f x}) ≠ 0 → f x ∈ s
⊢ ∀ b ∈ s, b * μ (⇑f ⁻¹' {b}) ≠ 0 → ∃ a, ∃ (_ : a ∈ f.range) (_ : a * μ (⇑f ⁻¹' {a}) ≠ 0), a = b

Tactic:
intro b

Goal state after:
case refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs : ∀ (x : α), f x ≠ 0 → μ (⇑f ⁻¹' {f x}) ≠ 0 → f x ∈ s
b : ℝ≥0∞
⊢ b ∈ s → b * μ (⇑f ⁻¹' {b}) ≠ 0 → ∃ a, ∃ (_ : a ∈ f.range) (_ : a * μ (⇑f ⁻¹' {a}) ≠ 0), a = b
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 α
ι : Sort u_5
inst✝ : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hι : Nonempty ι
A : MeasurableSet {b | BddAbove (range fun i ↦ f i b)}
this : Measurable fun _b ↦ sSup ∅
⊢ ∀ b ∈ {b | BddAbove (range fun i ↦ f i b)}, IsLUB {a | ∃ i, f i b = a} (⨆ i, f i b)

Tactic:
intro b

Goal state after:
α : Type u_1
δ : Type u_4
inst✝⁵ : TopologicalSpace α
mα : MeasurableSpace α
inst✝⁴ : BorelSpace α
mδ : MeasurableSpace δ
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
inst✝ : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hι : Nonempty ι
A : MeasurableSet {b | BddAbove (range fun i ↦ f i b)}
this : Measurable fun _b ↦ sSup ∅
b : δ
⊢ b ∈ {b | BddAbove (range fun i ↦ f i b)} → IsLUB {a | ∃ i, f i b = a} (⨆ i, f i b)