mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Order.AtTopBotIxx

Goal state before:
pp: case inr.right
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
x : X
h✝ : Nonempty α
x_L : X
hx_L : x_L < x
x_R : X
hx_R : x < x_R
a_L : α
ha_L : ∀ a ≤ a_L, g a ≤ x_L
a_R : α
ha_R : ∀ a ≥ a_R, x_R ≤ f a
n : α
y : X
hf : f n ≤ y
hg : y ≤ g n
hxL : x_L < y
hxR : y < x_R
⊢ n ≤ a_R

Tactic:
· contrapose! hxR
    exact (ha_R n hxR.le).trans hf

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t ((liftLinear (OuterMeasure.restrict s) ⋯) μ)
⊢ (μ.restrict s) t = μ (t ∩ s)

Tactic:
rw [← restrictₗ_apply, restrictₗ, liftLinear_apply₀ _ ht, OuterMeasure.restrict_apply,
    coe_toOuterMeasure]

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) ≠ ∞
⊢ μ (⋂ i, s i) = ⨅ i, μ (s i)

Tactic:
refine le_antisymm (le_iInf fun i ↦ measure_mono <| iInter_subset _ _) ?_

Goal state after:
α : 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) ≠ ∞
⊢ ⨅ i, μ (s i) ≤ μ (⋂ i, s i)
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ✝ ν ν₁ ν₂ : Measure α
s t : Set α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
c : ℝ≥0
x : α
o : Set α
xo : x ∈ o
o_open : IsOpen[inst✝¹] o
μo : μ o < ∞
⊢ (c • μ).FiniteAtFilter (𝓝 x)

Tactic:
refine ⟨o, o_open.mem_nhds xo, ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ✝ ν ν₁ ν₂ : Measure α
s t : Set α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
c : ℝ≥0
x : α
o : Set α
xo : x ∈ o
o_open : IsOpen[inst✝¹] o
μo : μ o < ∞
⊢ (c • μ) o < ∞
Module: Mathlib.MeasureTheory.Measure.Trim

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
⊢ μ.trim hm = Measure.map id μ

Tactic:
by
  refine @Measure.ext α m _ _ (fun s hs ↦ ?_)
  rw [Measure.map_apply (measurable_id'' hm) hs, trim_measurableSet_eq hm hs, Set.preimage_id]

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

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

Tactic:
by
  ext s hs
  simp [hs]

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

Goal state before:
pp: case pos
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ⋃₀ memPartition f n = univ
x : α
t : Set α
ht : t ∈ memPartition f n
hxt : x ∈ t
hxf : x ∈ f n
⊢ ∃ t ∈ {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}, x ∈ t

Tactic:
exact ⟨t ∩ f n, ⟨t, ht, Or.inl rfl⟩, hxt, hxf⟩

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
h : (μ + ν) t ≠ ∞
h' : s ⊆ t
h'' : (μ + ν) s = (μ + ν) t
⊢ μ s = μ t

Tactic:
by
  refine le_antisymm (measure_mono h') ?_
  have : μ t + ν t ≤ μ s + ν t :=
    calc
      μ t + ν t = μ s + ν s := h''.symm
      _ ≤ μ s + ν t := by gcongr
  apply ENNReal.le_of_add_le_add_right _ this
  exact ne_top_of_le_ne_top h (le_add_left le_rfl)

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

Goal state before:
pp: case refine_2
ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
a✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i ↦ toMeasurable (μ i) {x | f x ≠ mk f ⋯ x}
hsμ : ∀ (i : ι), (μ i) (s i) = 0
hsm : MeasurableSet (⋂ i, s i)
hs : ∀ (i : ι), ∀ x ∉ s i, f x = mk f ⋯ x
g : α → β := (⋂ i, s i).piecewise (const α default) f
⊢ Measurable ((⋂ i, s i)ᶜ.domRestrict g)

Tactic:
rw [domRestrict_piecewise_compl, compl_iInter]
    intro t ht
    refine ⟨⋃ i, (h i).mk f ⁻¹' t ∩ (s i)ᶜ, MeasurableSet.iUnion fun i ↦
      (measurable_mk _ ht).inter (measurableSet_toMeasurable _ _).compl, ?_⟩
    ext ⟨x, hx⟩
    simp only [mem_preimage, mem_iUnion, Set.domRestrict, mem_inter_iff,
      mem_compl_iff] at hx ⊢
    constructor
    · rintro ⟨i, hxt, hxs⟩
      rwa [hs _ _ hxs]
    · rcases hx with ⟨i, hi⟩
      rw [hs _ _ hi]
      exact fun h => ⟨i, h, hi⟩

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

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ ν : Measure α
⊢ AEMeasurable f (μ + ν) ↔ AEMeasurable f μ ∧ AEMeasurable f ν

Tactic:
rw [← sum_cond, aemeasurable_sum_measure_iff, Bool.forall_bool, and_comm]
  rfl

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

Goal state before:
pp: α : 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
⊢ AEMeasurable f μ

Tactic:
by
  rcases eq_empty_or_nonempty t with rfl | hne
  · obtain rfl : μ = 0 := by simpa using hft
    apply aemeasurable_zero_measure
  · rw [← μ.ae_completion] at hft
    obtain ⟨f', hf'm, hf't, hff'⟩ :
        ∃ f' : α → β, NullMeasurable f' μ ∧ range f' ⊆ t ∧ f =ᵐ[μ] f' :=
      h.measurable'.aemeasurable.exists_ae_eq_range_subset hft hne
    rw [range_subset_iff] at hf't
    lift f' to α → t using hf't
    replace hf'm : NullMeasurable f' μ := hf'm.measurable'.subtype_mk
    exact (measurable_subtype_coe.comp_aemeasurable hf'm.aemeasurable).congr hff'.symm

Goal state after:
Module: Mathlib.Topology.Separation.GDelta

Goal state before:
pp: case inl
X : Type u_1
inst✝¹ : TopologicalSpace X
s t : Set X
inst✝ : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed[inst✝¹] t
T_open : ∀ t ∈ ∅, IsOpen[inst✝¹] t
T_count : ∅.Countable
T_int : t = ⋂₀ ∅
⊢ HasSeparatingCover s t

Tactic:
T_int,

Goal state after:
case inl
X : Type u_1
inst✝¹ : TopologicalSpace X
s t : Set X
inst✝ : NormalSpace X
st_dis : Disjoint s (⋂₀ ∅)
t_cl : IsClosed[inst✝¹] t
T_open : ∀ t ∈ ∅, IsOpen[inst✝¹] t
T_count : ∅.Countable
T_int : t = ⋂₀ ∅
⊢ HasSeparatingCover s t
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case refine_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ MeasurableSpace.generateFrom (range Iic) ≤ MeasurableSpace.generateFrom (range Ioi)

Tactic:
refine MeasurableSpace.generateFrom_le fun t ht => ?_
    obtain ⟨u, rfl⟩ := ht
    rw [← compl_Ioi]
    exact (MeasurableSpace.measurableSet_generateFrom (mem_range.mpr ⟨u, rfl⟩)).compl

Goal state after:
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
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 : α
x✝ : ∃ i ≤ x, i ≤ b ∧ i ∈ t ∧ x ≤ b
y : α
yx : y ≤ x
hy1 : y ≤ b
hy2 : y ∈ t
hy : x ≤ b
⊢ x < a

Tactic:
order

Goal state after:
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
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 : α
h : x < a
this : x ≤ b
z : α
hzt : z ∈ t
hzx : z ≤ x
⊢ z ≤ b

Tactic:
order

Goal state after:
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
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 : α
h : x < a
this : x ≤ b
z : α
hzt : z ∈ t
hzx : z ≤ x
⊢ x ≤ b

Tactic:
order

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

Goal state before:
pp: case inr
α : Type u
inst✝ : PseudoEMetricSpace α
A : Set α
r₁ r₂ : ℝ
hr : r₁ < r₂
h₁ : 0 ≤ r₁
h : r₁ = (ENNReal.ofReal r₂).toReal
⊢ r₁ = r₂

Tactic:
ENNReal.toReal_ofReal (h₁.trans hr.le)

Goal state after:
case inr
α : Type u
inst✝ : PseudoEMetricSpace α
A : Set α
r₁ r₂ : ℝ
hr : r₁ < r₂
h₁ : 0 ≤ r₁
h : r₁ = r₂
⊢ r₁ = r₂
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
r : ℝ
hs : s.Nonempty
⊢ r ≤ (infEDist x s).toReal ↔ ∀ ⦃y : α⦄, y ∈ s → r ≤ dist x y

Tactic:
← ENNReal.ofReal_le_iff_le_toReal (infEDist_ne_top hs),

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
r : ℝ
hs : s.Nonempty
⊢ ENNReal.ofReal r ≤ infEDist x s ↔ ∀ ⦃y : α⦄, y ∈ s → r ≤ dist x y
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

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

Tactic:
rcases hne with ⟨z, hz⟩

Goal state after:
α : Type u
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : ProperSpace α
h : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
x z : α
hz : z ∈ s
⊢ ∃ y ∈ s, infDist x s = dist x y
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: case refine_2
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_nn : 0 ≤ δ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
⊢ ⋂ i ∈ s, thickening i E ⊆ cthickening δ E

Tactic:
rw [cthickening_eq_iInter_cthickening' s hsδ hs E]

Goal state after:
case refine_2
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_nn : 0 ≤ δ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
⊢ ⋂ i ∈ s, thickening i E ⊆ ⋂ ε ∈ s, cthickening ε E
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 : ∀ (a : α), μ (Iic a) = ν (Iic a)
⊢ μ = ν

Tactic:
refine ext_of_Ioc_finite μ ν ?_ fun a b hlt => ?_

Goal state after:
case refine_1
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
h : ∀ (a : α), μ (Iic a) = ν (Iic a)
⊢ μ univ = ν univ

case refine_2
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
h : ∀ (a : α), μ (Iic a) = ν (Iic a)
a b : α
hlt : a < b
⊢ μ (Ioc a b) = ν (Ioc 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✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
f : δ → α
hf : ∀ (x : α), MeasurableSet (f ⁻¹' Iio x)
⊢ Measurable f

Tactic:
by
  convert! measurable_generateFrom (α := δ) _
  · exact BorelSpace.measurable_eq.trans (borel_eq_generateFrom_Iio _)
  · rintro _ ⟨x, rfl⟩; exact hf x

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

Goal state before:
pp: case inl
α : 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 ι
⊢ Measurable g

Tactic:
rcases eq_empty_or_nonempty s with rfl | ⟨x, hx⟩

Goal state after:
case inl.inl
α : 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)
g'_meas : Measurable g'
hι : IsEmpty ι
hs : MeasurableSet ∅
hg : ∀ b ∈ ∅, IsLUB {a | ∃ i, f i b = a} (g b)
hg' : EqOn g g' ∅ᶜ
⊢ Measurable g

case inl.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'
hι : IsEmpty ι
x : δ
hx : x ∈ s
⊢ Measurable g
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
h' : ∀ x ∈ s, ∃ y, x < y
⊢ MeasurableSet s

Tactic:
by
  choose! M hM using h'
  suffices H : (s \ interior s).Countable by
    have : s = interior s ∪ s \ interior s := by rw [union_sdiff_cancel interior_subset]
    rw [this]
    exact isOpen_interior.measurableSet.union H.measurableSet
  have A : ∀ x ∈ s, ∃ y ∈ Ioi x, Ioo x y ⊆ s := fun x hx =>
    (mem_nhdsGT_iff_exists_Ioo_subset' (hM x hx)).1 (h x hx)
  choose! y hy h'y using A
  have B : Set.PairwiseDisjoint (s \ interior s) fun x => Ioo x (y x) := by
    intro x hx x' hx' hxx'
    rcases lt_or_gt_of_ne hxx' with (h' | h')
    · refine disjoint_left.2 fun z hz h'z => ?_
      have : x' ∈ interior s :=
        mem_interior.2 ⟨Ioo x (y x), h'y _ hx.1, isOpen_Ioo, ⟨h', h'z.1.trans hz.2⟩⟩
      exact False.elim (hx'.2 this)
    · refine disjoint_left.2 fun z hz h'z => ?_
      have : x ∈ interior s :=
        mem_interior.2 ⟨Ioo x' (y x'), h'y _ hx'.1, isOpen_Ioo, ⟨h', hz.1.trans h'z.2⟩⟩
      exact False.elim (hx.2 this)
  exact B.countable_of_Ioo fun x hx => hy x hx.1

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
f : ι → δ → α
s : Set ι
hs : s.Countable
hf : ∀ i ∈ s, Measurable (f i)
⊢ Measurable fun x ↦ sSup ((fun i ↦ f i x) '' s)

Tactic:
image_eq_range

Goal state after:
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_5
f : ι → δ → α
s : Set ι
hs : s.Countable
hf : ∀ i ∈ s, Measurable (f i)
⊢ Measurable fun x ↦ sSup (range fun x_1 ↦ f (↑x_1) x)
Module: Mathlib.Topology.Instances.Real.Lemmas

Goal state before:
pp: ι : Type u_1
inst✝² : Preorder ι
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x1 x2 ↦ x1 ≤ x2
f : ι → ℝ
x : ℝ
h_tto : Tendsto f atTop (𝓝 x)
h_ant : Antitone f
h_bdd : BddBelow (range f)
⊢ IsGLB (range f) x

Tactic:
rw [tendsto_nhds_unique h_tto (tendsto_atTop_ciInf h_ant h_bdd)]
  exact isGLB_ciInf h_bdd

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

Goal state before:
pp: case empty
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : AddZeroClass γ
motive : (α →ₛ γ) → Prop
const :
  ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), motive (piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ⇑f) (support ⇑g) → motive f → motive g → motive (f + g)
f : α →ₛ γ
h : ⇑f = Function.const α 0
⊢ motive f

Tactic:
convert! const 0 MeasurableSet.univ

Goal state after:
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : AddZeroClass γ
motive : (α →ₛ γ) → Prop
const :
  ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), motive (piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ⇑f) (support ⇑g) → motive f → motive g → motive (f + g)
f : α →ₛ γ
h : ⇑f = Function.const α 0
⊢ f = piecewise univ ⋯ (SimpleFunc.const α 0) (SimpleFunc.const α 0)
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α
mα : MeasurableSpace α
x✝ : ℝ≥0
⊢ Measurable fun x ↦ x✝ • x

Tactic:
simp_rw [ENNReal.smul_def]; exact measurable_const_smul _

Goal state after:
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 fun x ↦ ∑' (i : ι), f i x

Tactic:
by
  simp_rw [ENNReal.tsum_eq_iSup_sum]
  exact .iSup fun s ↦ s.measurable_fun_sum fun i _ => h i

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

Goal state before:
pp: case refine_4
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α✝
mα✝ : MeasurableSpace α✝
α : Type u_5
β : Type u_6
γ : Type u_7
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
⊢ Measurable fun r ↦ (↑r, ⊥).1 * (↑r, ⊥).2

pp: case refine_5
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α✝
mα✝ : MeasurableSpace α✝
α : Type u_5
β : Type u_6
γ : Type u_7
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
⊢ Measurable fun r ↦ (↑r, ⊤).1 * (↑r, ⊤).2

Tactic:
· simp_rw [mul_comm _ ⊥]
    exact (measurable_const_mul _).comp measurable_coe_real_ereal

Goal state after:
case refine_5
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α✝
mα✝ : MeasurableSpace α✝
α : Type u_5
β : Type u_6
γ : Type u_7
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
⊢ Measurable fun r ↦ (↑r, ⊤).1 * (↑r, ⊤).2
Module: Mathlib.MeasureTheory.Function.SimpleFuncDense

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
hx : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (range e)
⊢ Tendsto (fun N ↦ (nearestPt e N) x) atTop (𝓝 x)

Tactic:
refine (atTop_basis.tendsto_iff nhds_basis_eball).2 fun ε hε => ?_

Goal state after:
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
hx : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (range e)
ε : ℝ≥0∞
hε : 0 < ε
⊢ ∃ ia, True ∧ ∀ x_1 ∈ Ici ia, (nearestPt e x_1) x ∈ eball x ε
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case hd
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A : μ s = μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' Ioi 0)
⊢ Disjoint (s ∩ f ⁻¹' {∞}) (s ∩ f ⁻¹' Ioo 0 ∞)

Tactic:
refine disjoint_left.2 fun x hx h'x => ?_

Goal state after:
case hd
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A : μ s = μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' Ioi 0)
x : α
hx : x ∈ s ∩ f ⁻¹' {∞}
h'x : x ∈ s ∩ f ⁻¹' Ioo 0 ∞
⊢ False
Module: Mathlib.MeasureTheory.Function.SimpleFuncDense

Goal state before:
pp: case hmono
X : Type u_3
Y : Type u_4
α : Type u_5
inst✝⁷ : Zero α
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : MeasurableSpace X
inst✝³ : MeasurableSpace Y
inst✝² : OpensMeasurableSpace X
inst✝¹ : OpensMeasurableSpace Y
inst✝ : PseudoMetricSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
ε : ℝ
hε : 0 < ε
K : Set (X × Y)
hK : IsCompact K
⊢ ∀ ⦃s t : Set (X × Y)⦄,
    s ⊆ t →
      (∃ g s, MeasurableSet s ∧ t ⊆ s ∧ ∀ x ∈ s, dist (f x) (g x) < ε) →
        ∃ g s_1, MeasurableSet s_1 ∧ s ⊆ s_1 ∧ ∀ x ∈ s_1, dist (f x) (g x) < ε

Tactic:
intro t t' htt' ⟨g, s, s_meas, ts, hg⟩
      exact ⟨g, s, s_meas, htt'.trans ts, hg⟩

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun x1 x2 ↦ x1 ≤ x2) f
val✝ : Encodable β
h✝ : Nonempty β
inhabited_h : Inhabited β
this : ∀ (a : α), ⨆ b, f b a = ⨆ n, f (Directed.sequence f h_directed n) a
⊢ ⨆ n, ∫⁻ (a : α), f (Directed.sequence f h_directed n) a ∂μ = ⨆ b, ∫⁻ (a : α), f b a ∂μ

Tactic:
refine le_antisymm (iSup_le fun n => ?_) (iSup_le fun b => ?_)
      · exact le_iSup (fun b => ∫⁻ a, f b a ∂μ) _
      · exact le_iSup_of_le (encode b + 1) (lintegral_mono <| h_directed.le_sequence b)

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
μ : Measure α
f₁ f₁' : α → β
f₂ f₂' : α → γ
h₁✝ : f₁ =ᵐ[μ] f₁'
h₂✝ : f₂ =ᵐ[μ] f₂'
g : β → γ → ℝ≥0∞
x✝ : α
h₂ : f₂ x✝ = f₂' x✝
h₁ : f₁ x✝ = f₁' x✝
⊢ (fun a ↦ g (f₁ a) (f₂ a)) x✝ = (fun a ↦ g (f₁' a) (f₂' a)) x✝

Tactic:
by dsimp only; rw [h₁, h₂]

Goal state after:
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
m : MeasurableSpace α
l : List (α → M)
hl : ∀ f ∈ l, StronglyMeasurable f
⊢ StronglyMeasurable fun x ↦ (List.map (fun f ↦ f x) l).prod

Tactic:
by
  simpa only [← Pi.list_prod_apply] using l.stronglyMeasurable_prod hl

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub

Goal state before:
pp: case hfg
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ∞
g : α → ℝ≥0∞
hmg : Measurable g
hgf : g ≤ f
hifg : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ
s : Set α
hms : MeasurableSet s
x : α
⊢ g x ≤ f x

Tactic:
apply hgf

Goal state after:
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : (x : α) → Decidable (x ∈ s)
f : ↑s → β
hf : StronglyMeasurable f
g : ↑sᶜ → β
hg : StronglyMeasurable g
hs : MeasurableSet s
x : α
hx : x ∉ s
⊢ Tendsto (fun n ↦ ((fun n ↦ SimpleFunc.dite s hs (hf.approx n) (hg.approx n)) n) x) atTop
    (𝓝 ((fun x ↦ if hx : x ∈ s then f ⟨x, hx⟩ else g ⟨x, hx⟩) x))

Tactic:
· simpa [hx] using hg.tendsto_approx ⟨x, hx⟩

Goal state after: