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

Goal state before:
pp: X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
a : X
hsa : s ⊆ Ioi a
hs : ∀ b' > a, ∃ b > a, Ioo a b ⊆ s
ha : IsPredPrelimit a
b' : Xᵒᵈ
⊢ b' < toDual a → ∃ a_2 < toDual a, Ioo a_2 (toDual a) ⊆ ⇑ofDual ⁻¹' s

Tactic:
hb'

Goal state after:
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
a : X
hsa : s ⊆ Ioi a
hs : ∀ b' > a, ∃ b > a, Ioo a b ⊆ s
ha : IsPredPrelimit a
b' : Xᵒᵈ
hb' : b' < toDual a
⊢ ∃ a_1 < toDual a, Ioo a_1 (toDual a) ⊆ ⇑ofDual ⁻¹' s
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 : α
μ : Measure α
h : SigmaFinite μ
n : ℕ
⊢ μ (⋯.some.set n) < ∞

Tactic:
exact h.out.some.finite n

Goal state after:
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✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
⊢ (μ + ν) univ < ∞

Tactic:
by
    rw [Measure.coe_add, Pi.add_apply, ENNReal.add_lt_top]
    exact ⟨measure_lt_top _ _, measure_lt_top _ _⟩

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

Goal state before:
pp: case inr
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsDirectedOrder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hs : Monotone s
h✝ : Nonempty ι
x : ℕ → ι
hxm : Monotone x
hx : Tendsto x atTop atTop
⊢ μ (⋃ i, s i) = ⨆ i, μ (s i)

Tactic:
rw [← hs.iUnion_comp_tendsto_atTop hx, ← Monotone.iSup_comp_tendsto_atTop _ hx]

Goal state after:
case inr
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsDirectedOrder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hs : Monotone s
h✝ : Nonempty ι
x : ℕ → ι
hxm : Monotone x
hx : Tendsto x atTop atTop
⊢ μ (⋃ a, s (x a)) = ⨆ a, μ (s (x a))

α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsDirectedOrder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hs : Monotone s
h✝ : Nonempty ι
x : ℕ → ι
hxm : Monotone x
hx : Tendsto x atTop atTop
⊢ Monotone fun 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 : Pairwise (AEDisjoint μ on s)
hm : ∀ (i : ι), NullMeasurableSet (s i) μ
t : Set α
ht : MeasurableSet t
⊢ (μ.restrict (⋃ i, s i)) t = ∑' (i : ι), (μ.restrict (s i)) t

Tactic:
simp only [restrict_apply, ht, inter_iUnion]
  exact
    measure_iUnion₀ (hd.mono fun i j h => h.mono inter_subset_right inter_subset_right)
      fun i => ht.nullMeasurableSet.inter (hm i)

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

Goal state before:
pp: α : Type u_1
ι : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
U : ι → Set α
hU : ⋃ i, U i = univ
hμ : μ ≠ 0
⊢ ∃ i, 0 < μ (U i)

Tactic:
contrapose! hμ with H
  rw [← measure_univ_eq_zero, ← hU]
  exact measure_iUnion_null fun i => nonpos_iff_eq_zero.1 (H i)

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

Goal state before:
pp: case zero
α : Type u_1
f : ℕ → Set α
⊢ ∀ {u v : Set α}, u ∈ memPartition f 0 → v ∈ memPartition f 0 → u ≠ v → Disjoint u v

Tactic:
| zero =>

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

Goal state before:
pp: case zero
α : Type u_1
f : ℕ → Set α
⊢ ⋃₀ memPartition f 0 = univ

Tactic:
| zero =>

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

Goal state before:
pp: case zero
α : Type u_1
f : ℕ → Set α
⊢ (memPartition f 0).Finite

Tactic:
| zero =>

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

Goal state before:
pp: case zero
α : Type u_1
f : ℕ → Set α
a : α
⊢ memPartitionSet f 0 a ∈ memPartition f 0

Tactic:
| zero =>

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : MeasurableSet s
ht : (μ + ν) t ≠ ∞
⊢ μ (toMeasurable (μ + ν) t ∩ s) = μ (t ∩ s)

Tactic:
by
  refine (measure_inter_eq_of_measure_eq hs ?_ (subset_toMeasurable _ _) ?_).symm
  · refine
      measure_eq_left_of_subset_of_measure_add_eq ?_ (subset_toMeasurable _ _)
        (measure_toMeasurable t).symm
    rwa [measure_toMeasurable t]
  · simp only [not_or, ENNReal.add_eq_top, Pi.add_apply, Ne, coe_add] at ht
    exact ht.1

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

Goal state before:
pp: case zero
α : Type u_1
f : ℕ → Set α
a : α
⊢ a ∈ memPartitionSet f 0 a

Tactic:
| zero =>

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

Goal state before:
pp: case compl
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
t : Set ↑s
hs : NullMeasurableSet s μ
t' : Set ↑s
ht✝ : MeasurableSet t'
ht' : NullMeasurableSet (Subtype.val '' t') μ
⊢ NullMeasurableSet (Subtype.val '' t'ᶜ) μ

Tactic:
| compl t' _ ht' =>

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : SeparatesPoints α
x y : α
h : x ≠ y
⊢ ∃ s, MeasurableSet s ∧ x ∈ s ∧ y ∉ s

Tactic:
by
  contrapose! h
  exact separatesPoints_def h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : Countable α
inst✝ : SeparatesPoints α
x : α
⊢ MeasurableSet {x}

Tactic:
by
    choose s hsm hxs hys using fun y (h : x ≠ y) ↦ exists_measurableSet_of_ne h
    convert! MeasurableSet.iInter fun y ↦ .iInter fun h ↦ hsm y h
    ext y
    rcases eq_or_ne x y with rfl | h
    · simpa
    · simp only [mem_singleton_iff, h.symm, false_iff, mem_iInter, not_forall]
      exact ⟨y, h, hys y h⟩

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

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : CountablyGenerated α
inst✝ : SeparatesPoints α
⊢ ∃ s, Nonempty (α ≃ᵐ ↑s)

Tactic:
use range (mapNatBool α), Equiv.ofInjective _ <|
    injective_mapNatBool _,
    Measurable.subtype_mk <| measurable_mapNatBool _

Goal state after:
case measurable_invFun
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : CountablyGenerated α
inst✝ : SeparatesPoints α
⊢ autoParam (Measurable ⇑(Equiv.ofInjective (mapNatBool α) ⋯).symm) MeasurableEquiv.measurable_invFun._autoParam
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
t : ℕ → Set α
n : ℕ
⊢ t n = ⋃₀ memPartition t n ∩ t n

Tactic:
sUnion_memPartition,

Goal state after:
α : Type u_1
t : ℕ → Set α
n : ℕ
⊢ t n = univ ∩ t n
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case refine_1.zero
α : Type u_1
t : ℕ → Set α
u : Set α
hun : u ∈ memPartition t 0
⊢ MeasurableSet u

Tactic:
| zero =>

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

Goal state before:
pp: α : Type u_2
ι : Type u_6
x✝ : MeasurableSpace α
μ : Measure α
s : ι → Set α
M : ℕ
hs_meas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (y : α), {i | y ∈ s i}.encard ≤ ↑M
t : Set α
ht : MeasurableSet t
F : Finset ι
P : Finset ι → Set α := fun C ↦ (⋂ i ∈ C, s i) ∩ ⋂ i ∈ F \ C, (s i)ᶜ
Cs : Finset (Finset ι) := F.powerset \ {∅}
G : ι → Set (Finset ι) := fun i ↦ {C | C ∈ F.powerset ∧ i ∈ C}
P_meas : ∀ (C : Finset ι), MeasurableSet (P C)
P_cover : ∀ {i : ι}, i ∈ F → s i ⊆ ⋃ C ∈ G i, P C
iUnion_P : ⋃ C ∈ Cs, P C ⊆ ⋃ i, s i
P_subset_s : ∀ {i : ι} {C : Finset ι}, i ∈ C → P C ⊆ s i
i : ι
hi : i ∈ F
C : Finset ι
x : α
hx : x ∈ P C
hxs : x ∈ s i
⊢ i ∈ C

Tactic:
rw [mem_inter_iff, mem_iInter₂, mem_iInter₂] at hx

Goal state after:
α : Type u_2
ι : Type u_6
x✝ : MeasurableSpace α
μ : Measure α
s : ι → Set α
M : ℕ
hs_meas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (y : α), {i | y ∈ s i}.encard ≤ ↑M
t : Set α
ht : MeasurableSet t
F : Finset ι
P : Finset ι → Set α := fun C ↦ (⋂ i ∈ C, s i) ∩ ⋂ i ∈ F \ C, (s i)ᶜ
Cs : Finset (Finset ι) := F.powerset \ {∅}
G : ι → Set (Finset ι) := fun i ↦ {C | C ∈ F.powerset ∧ i ∈ C}
P_meas : ∀ (C : Finset ι), MeasurableSet (P C)
P_cover : ∀ {i : ι}, i ∈ F → s i ⊆ ⋃ C ∈ G i, P C
iUnion_P : ⋃ C ∈ Cs, P C ⊆ ⋃ i, s i
P_subset_s : ∀ {i : ι} {C : Finset ι}, i ∈ C → P C ⊆ s i
i : ι
hi : i ∈ F
C : Finset ι
x : α
hx : (∀ i ∈ C, x ∈ s i) ∧ ∀ i ∈ F \ C, x ∈ (s i)ᶜ
hxs : x ∈ s i
⊢ i ∈ C
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: case mpr
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
μ : Measure α
inst✝ : Zero β
s : Set α
hs : MeasurableSet s
⊢ AEMeasurable f (μ.restrict s) → AEMeasurable (s.indicator f) μ

Tactic:
· intro h
    refine ⟨indicator s (h.mk f), h.measurable_mk.indicator hs, ?_⟩
    have A : s.indicator f =ᵐ[μ.restrict s] s.indicator (AEMeasurable.mk f h) :=
      (indicator_ae_eq_restrict hs).trans (h.ae_eq_mk.trans <| (indicator_ae_eq_restrict hs).symm)
    have B : s.indicator f =ᵐ[μ.restrict sᶜ] s.indicator (AEMeasurable.mk f h) :=
      (indicator_ae_eq_restrict_compl hs).trans (indicator_ae_eq_restrict_compl hs).symm
    exact ae_of_ae_restrict_of_ae_restrict_compl _ A B

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 t : Set α
ht : MeasurableSet t
hst : s =ᵐ[μ] t
⊢ AEMeasurable f (μ.restrict t) ↔ AEMeasurable f (μ.restrict s)

Tactic:
restrict_congr_set hst

Goal state after:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
μ : Measure α
inst✝ : Zero β
s t : Set α
ht : MeasurableSet t
hst : s =ᵐ[μ] t
⊢ AEMeasurable f (μ.restrict t) ↔ AEMeasurable f (μ.restrict t)
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
s : Finset ι
μ : ι → Measure α
⊢ (sum fun i ↦ μ ↑i) = ∑ i ∈ s, μ i

Tactic:
by rw [sum_fintype, Finset.sum_coe_sort s μ]

Goal state after:
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: case zero
α : Type u_1
M : Type u_2
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
⊢ Measurable fun x ↦ (x, 0).1 ^ (x, 0).2

Tactic:
| zero =>

Goal state after:
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: case succ
α : Type u_1
M : Type u_2
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
n : ℕ
ih : Measurable fun x ↦ (x, n).1 ^ (x, n).2
⊢ Measurable fun x ↦ x ^ n * x

Tactic:
exact ih.mul measurable_id

Goal state after:
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: case zero
α✝ : Type u_1
M✝ : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
inst✝⁶ : MeasurableSpace X
inst✝⁵ : SMul M✝ X
m : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → M✝
g : α → X
inst✝⁴ : MeasurableSpace M✝
inst✝³ : MeasurableSMul M✝ X
M : Type u_6
inst✝² : AddMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableAdd₂ M
⊢ Measurable fun x ↦ (x, 0).2 • (x, 0).1

Tactic:
| zero =>

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ ∀ (i : α), MeasurableSet (Iio i)

Tactic:
intro a

Goal state after:
case refine_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
⊢ MeasurableSet (Iio a)
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: α : 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 ∧ a ×ˢ b ⊆ s}
⊢ ∀ (a : Set α), IsOpen[inst✝⁹] (F a)

Tactic:
intro a

Goal state after:
α : 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 ∧ a ×ˢ b ⊆ s}
a : Set α
⊢ IsOpen[inst✝⁹] (F a)
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: α : 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 : Set β), IsOpen[inst✝¹²] (F a)

Tactic:
intro a

Goal state after:
α : 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 : Set β
⊢ IsOpen[inst✝¹²] (F a)
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: α' : Type u_6
inst✝¹ : TopologicalSpace α'
inst✝ : MeasurableSpace α'
μ : Measure α'
s s' : Set α'
h : μ (frontier s) = 0
h' : μ (frontier s') = 0
⊢ μ (frontier (s ∩ s')) = 0

Tactic:
by
  apply bot_unique
  calc μ (frontier (s ∩ s'))
  _ ≤ μ (frontier s ∪ frontier s') := measure_mono <| (frontier_inter_subset _ _).trans (by grind)
  _ ≤ μ (frontier s) + μ (frontier s') := measure_union_le _ _
  _ = 0 := by simp [h, h']

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

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

Tactic:
by
  simp [hausdorffEDist_def, ← subset_def, ← mem_closure_iff_infEDist_zero,
    subset_antisymm_iff, isClosed_closure.closure_subset_iff]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x y : α
h : y ∈ s
⊢ infDist x s ≤ (edist x y).toReal

Tactic:
infDist

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x y : α
h : y ∈ s
⊢ (infEDist x s).toReal ≤ (edist x y).toReal
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case refine_1
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
inst✝ : NoMinOrder α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a < b → μ (Ioc a b) ≠ ∞
h : ∀ ⦃a b : α⦄, a < b → μ (Ioc a b) = ν (Ioc a b)
⊢ ∀ ⦃a b : αᵒᵈ⦄, a < b → μ (Ico a b) ≠ ∞

Tactic:
intro a

Goal state after:
case refine_1
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
inst✝ : NoMinOrder α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a < b → μ (Ioc a b) ≠ ∞
h : ∀ ⦃a b : α⦄, a < b → μ (Ioc a b) = ν (Ioc a b)
a : αᵒᵈ
⊢ ∀ ⦃b : αᵒᵈ⦄, a < b → μ (Ico a b) ≠ ∞
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case refine_2
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
inst✝ : NoMinOrder α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a < b → μ (Ioc a b) ≠ ∞
h : ∀ ⦃a b : α⦄, a < b → μ (Ioc a b) = ν (Ioc a b)
⊢ ∀ ⦃a b : αᵒᵈ⦄, a < b → μ (Ico a b) = ν (Ico a b)

Tactic:
intro a

Goal state after:
case refine_2
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
inst✝ : NoMinOrder α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a < b → μ (Ioc a b) ≠ ∞
h : ∀ ⦃a b : α⦄, a < b → μ (Ioc a b) = ν (Ioc a b)
a : αᵒᵈ
⊢ ∀ ⦃b : αᵒᵈ⦄, a < b → μ (Ico a b) = ν (Ico a b)
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 : edist x y < ENNReal.ofReal r
⊢ ∃ y ∈ t, dist x y < r

Tactic:
rw [edist_dist, ENNReal.ofReal_lt_ofReal_iff r0] at yr

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.Topology.MetricSpace.Thickening

Goal state before:
pp: case inr
α : Type u
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
hδ : 0 ≤ δ
s : Set α
hε : 0 ≤ ε
x : α
⊢ (∃ z, infEDist z s ≤ ENNReal.ofReal δ ∧ edist x z < ENNReal.ofReal ε) →
    infEDist x s < ENNReal.ofReal ε + ENNReal.ofReal δ

Tactic:
rintro ⟨y, hy, hxy⟩

Goal state after:
case inr
α : Type u
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
hδ : 0 ≤ δ
s : Set α
hε : 0 ≤ ε
x y : α
hy : infEDist y s ≤ ENNReal.ofReal δ
hxy : edist x y < ENNReal.ofReal ε
⊢ infEDist x s < ENNReal.ofReal ε + ENNReal.ofReal δ
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
f : γ → α →ₛ β
s : Finset γ
a : α
⊢ ∀ (a_1 : γ) (s : Finset γ),
    a_1 ∉ s → ((s.sup f) a = s.sup fun c ↦ (f c) a) → ((insert a_1 s).sup f) a = (insert a_1 s).sup fun c ↦ (f c) a

Tactic:
intro a

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
f : γ → α →ₛ β
s : Finset γ
a✝ : α
a : γ
⊢ ∀ (s : Finset γ),
    a ∉ s → ((s.sup f) a✝ = s.sup fun c ↦ (f c) a✝) → ((insert a s).sup f) a✝ = (insert a s).sup fun c ↦ (f c) a✝
Module: Mathlib.MeasureTheory.MeasurableSpace.Prod

Goal state before:
pp: case a.refine_2
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
s : Set β
hs : s ∈ D
⊢ MeasurableSet (Prod.snd ⁻¹' s)

Tactic:
rcases hC with ⟨t, h1t, h2t⟩

Goal state after:
case a.refine_2
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hD : IsCountablySpanning D
s : Set β
hs : s ∈ D
t : ℕ → Set α
h1t : ∀ (n : ℕ), t n ∈ C
h2t : ⋃ n, t n = univ
⊢ MeasurableSet (Prod.snd ⁻¹' s)
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: case zero
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
a : α
⊢ ∑ k ∈ Finset.range (0 + 1), ↑((eapproxDiff f k) a) = (eapprox f 0) a

Tactic:
| zero =>

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

Goal state before:
pp: α : Type u_3
inst✝² : MeasurableSpace α
A : Set α
ι : Type u_4
L : Filter ι
inst✝¹ : L.IsCountablyGenerated
As : ι → Set α
inst✝ : L.NeBot
As_mble : ∀ (i : ι), MeasurableSet (As i)
h_lim : ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
⊢ MeasurableSet A

Tactic:
by
  simp_rw [← measurable_indicator_const_iff (1 : ℝ≥0∞)] at As_mble ⊢
  exact ENNReal.measurable_of_tendsto' L As_mble
    ((tendsto_indicator_const_iff_forall_eventually L (1 : ℝ≥0∞)).mpr h_lim)

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

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

Tactic:
| zero =>

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

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

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : α → ℝ≥0∞ := fun a ↦ ⨆ n, f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), ↑(s x) ≤ ⨆ n, f n x
r : ℝ≥0
right✝ ha✝ : ↑r < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun a ↦ r * a) s
eq_rs : SimpleFunc.map c rs = const α ↑r * SimpleFunc.map c s
x : α
p_eq : ¬c (rs x) = 0
this✝¹ : r * s x ≠ 0
this✝ : s x ≠ 0
this : (SimpleFunc.map c rs) x < ⨆ n, f n x
i : ℕ
hi : (SimpleFunc.map c rs) x < f i x
⊢ x ∈ ⋃ i, {a | c (rs x) ≤ f i a}

Tactic:
exact mem_iUnion.2 ⟨i, le_of_lt hi⟩

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

Goal state before:
pp: case refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
h : ∀ᵐ (a : α) ∂μ, f a ≤ g a
t : Set α
hts : {x | (fun a ↦ f a ≤ g a) x}ᶜ ⊆ t
ht : MeasurableSet t
ht0 : μ t = 0
this : ∀ᵐ (x : α) ∂μ, x ∉ t
s : α →ₛ ℝ≥0∞
hfs : ⇑s ≤ fun a ↦ f a
⊢ ⇑(s.restrict tᶜ) ≤ fun a ↦ g a

Tactic:
intro a

Goal state after:
case refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
h : ∀ᵐ (a : α) ∂μ, f a ≤ g a
t : Set α
hts : {x | (fun a ↦ f a ≤ g a) x}ᶜ ⊆ t
ht : MeasurableSet t
ht0 : μ t = 0
this : ∀ᵐ (x : α) ∂μ, x ∉ t
s : α →ₛ ℝ≥0∞
hfs : ⇑s ≤ fun a ↦ f a
a : α
⊢ (s.restrict tᶜ) a ≤ (fun a ↦ g a) a