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

Goal state before:
pp: case h₂
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
m : ℝ≥0∞ := ⋯
D : Set (Set α)
D_mem : D ∈ {D | D ⊆ C ∧ D.Countable}
hD : μ (⋃₀ D) = m
s : Set α
hs : s ∈ C
⊢ μ (s ∪ ⋃₀ D) ≤ μ (⋃₀ D)

Tactic:
hD,

Goal state after:
case h₂
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
m : ℝ≥0∞ := ⨆ D ∈ {D | D ⊆ C ∧ D.Countable}, μ (⋃₀ D)
D : Set (Set α)
D_mem : D ∈ {D | D ⊆ C ∧ D.Countable}
hD : μ (⋃₀ D) = m
s : Set α
hs : s ∈ C
⊢ μ (s ∪ ⋃₀ D) ≤ m
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : ∀ᵐ (a : α) ∂μ, a ∈ t
⊢ μ (t ∩ s) = μ s

Tactic:
by
  refine le_antisymm (measure_mono inter_subset_right) ?_
  apply EventuallyLE.measure_le
  filter_upwards [h] with x hx h'x using ⟨hx, h'x⟩

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ≪ ν
s : Set α
⊢ μ.restrict s ≪ ν.restrict s

Tactic:
refine Measure.AbsolutelyContinuous.mk (fun t ht htν ↦ ?_)
  rw [restrict_apply ht] at htν ⊢
  exact h htν

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
s : Set α
t : Set β
f : α → β
hs : MeasurableSet s
⊢ t ∈ Filter.map f (ae (μ.restrict s)) ↔ μ ((f ⁻¹' t)ᶜ ∩ s) = 0

Tactic:
mem_map,

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
s : Set α
t : Set β
f : α → β
hs : MeasurableSet s
⊢ f ⁻¹' t ∈ ae (μ.restrict s) ↔ μ ((f ⁻¹' t)ᶜ ∩ s) = 0
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
m : Set (Measure α)
s : Set α
hs : MeasurableSet s
t : Set α
μ : Measure α
hμ : μ ∈ m
u : Set α
htu : t ⊆ u
_hu : MeasurableSet u
hm : ∀ {s t : Set α}, s ⊆ t → OuterMeasure.sInfGen (toOuterMeasure '' m) s ≤ μ t
⊢ (⨅ μ ∈ toOuterMeasure '' m, μ (t ∩ s)) + ⨅ μ ∈ toOuterMeasure '' m, μ (t \ s) ≤ μ u

Tactic:
rw [← measure_inter_add_sdiff u hs]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
m : Set (Measure α)
s : Set α
hs : MeasurableSet s
t : Set α
μ : Measure α
hμ : μ ∈ m
u : Set α
htu : t ⊆ u
_hu : MeasurableSet u
hm : ∀ {s t : Set α}, s ⊆ t → OuterMeasure.sInfGen (toOuterMeasure '' m) s ≤ μ t
⊢ (⨅ μ ∈ toOuterMeasure '' m, μ (t ∩ s)) + ⨅ μ ∈ toOuterMeasure '' m, μ (t \ s) ≤ μ (u ∩ s) + μ (u \ s)
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: case refine_2
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝² : Group β
inst✝¹ : LE β
inst✝ : MulRightMono β
f g : α → β
h : f ≤ᵐ[μ] g
a : α
ha : f a ≤ g a
⊢ 1 a ≤ (g / f) a

Tactic:
rwa [Pi.one_apply, Pi.div_apply, one_le_div']

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

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

Tactic:
by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · obtain ⟨t', -, ht', t't⟩ : ∃ t' ⊇ t, MeasurableSet t' ∧ t' =ᵐ[μ.restrict s] t :=
      h.exists_measurable_superset_ae_eq
    have A : (t' ∩ s : Set α) =ᵐ[μ] (t ∩ s : Set α) := by
      have : ∀ᵐ x ∂μ, x ∈ s → (x ∈ t') = (x ∈ t) :=
        (ae_restrict_iff'₀ hs).1 t't
      filter_upwards [this] with y hy
      change (y ∈ t' ∩ s) = (y ∈ t ∩ s)
      simpa only [eq_iff_iff, mem_inter_iff, and_congr_left_iff] using hy
    obtain ⟨s', -, hs', s's⟩ : ∃ s' ⊇ s, MeasurableSet s' ∧ s' =ᵐ[μ] s :=
      hs.exists_measurable_superset_ae_eq
    have B : (t' ∩ s' : Set α) =ᵐ[μ] (t' ∩ s : Set α) :=
      ae_eq_set_inter (EventuallyEq.refl _ _) s's
    exact (ht'.inter hs').nullMeasurableSet.congr (B.trans A)
  · have A : NullMeasurableSet (t \ s) (μ.restrict s) := by
      apply NullMeasurableSet.of_null
      rw [Measure.restrict_apply₀' hs]
      simp
    have B : NullMeasurableSet (t ∩ s) (μ.restrict s) :=
      h.mono_ac absolutelyContinuous_restrict
    simpa using A.union B

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

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

Tactic:
mem_map,

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
t : Set β
ht : 0 ∈ t
hs : MeasurableSet s
⊢ s.indicator f ⁻¹' t ∈ ae μ ↔ f ⁻¹' t ∈ ae (μ.restrict s)
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
t : Set β
ht : 0 ∉ t
⊢ t ∈ Filter.map (s.indicator f) (ae μ) ↔ μ ((f ⁻¹' t)ᶜ ∪ sᶜ) = 0

Tactic:
mem_map,

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
t : Set β
ht : 0 ∉ t
⊢ s.indicator f ⁻¹' t ∈ ae μ ↔ μ ((f ⁻¹' t)ᶜ ∪ sᶜ) = 0
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
⊢ SeparatesPoints α

Tactic:
refine ⟨fun x y h ↦ ?_⟩
  specialize h _ (MeasurableSet.singleton x)
  simp_rw [mem_singleton_iff, forall_true_left] at h
  exact h.symm

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

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
Y : Type u_2
inst✝¹ : TopologicalSpace Y
inst✝ : PseudoMetrizableSpace Y
f : X → Y
⊢ IsGδ {x | ContinuousAt f x}

Tactic:
let := pseudoMetrizableSpaceUniformity Y

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
Y : Type u_2
inst✝¹ : TopologicalSpace Y
inst✝ : PseudoMetrizableSpace Y
f : X → Y
this : UniformSpace Y := pseudoMetrizableSpaceUniformity Y
⊢ IsGδ {x | ContinuousAt f x}
Module: Mathlib.Topology.GDelta.MetrizableSpace

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
Y : Type u_2
inst✝¹ : TopologicalSpace Y
inst✝ : PseudoMetrizableSpace Y
f : X → Y
⊢ IsGδ {x | ContinuousAt f x}

Tactic:
let := pseudoMetrizableSpaceUniformity Y
  have := pseudoMetrizableSpaceUniformity_countably_generated Y
  obtain ⟨U, _, hU⟩ := (@uniformity_hasBasis_open_symmetric Y _).exists_antitone_subbasis
  simp only [Uniform.continuousAt_iff_prod, nhds_prod_eq]
  simp only [(nhds_basis_opens _).prod_self.tendsto_iff hU.toHasBasis,
    forall_prop_of_true, ofPred_forall]
  refine .iInter fun k ↦ IsOpen.isGδ <| isOpen_iff_mem_nhds.2 fun x ↦ ?_
  rintro ⟨s, ⟨hsx, hso⟩, hsU⟩
  filter_upwards [IsOpen.mem_nhds hso hsx] with _ hy using ⟨s, ⟨hy, hso⟩, hsU⟩

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 α
⊢ ∀ t ∈ range Iio, MeasurableSet t

Tactic:
forall_mem_range

Goal state after:
case refine_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ ∀ (i : α), MeasurableSet (Iio i)
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 δ
α' : Type u_6
inst✝² : TopologicalSpace α'
inst✝¹ : MeasurableSpace α'
inst✝ : T0Space α
x y : α
⊢ (∀ (s : Set α), MeasurableSet s → x ∈ s → y ∈ s) → x = y

Tactic:
contrapose!
    exact fun a => exists_measurableSet_of_ne a

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

Goal state before:
pp: case refine_1
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
x : α
xs : x ∈ s
y : α
yt : y ∈ t
⊢ ∀ x ∈ s, ∃ y ∈ t, edist x y ≤ ediam (s ∪ t)

Tactic:
intro z

Goal state after:
case refine_1
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
x : α
xs : x ∈ s
y : α
yt : y ∈ t
z : α
⊢ z ∈ s → ∃ y ∈ t, edist z y ≤ ediam (s ∪ t)
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: case refine_2
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
x : α
xs : x ∈ s
y : α
yt : y ∈ t
⊢ ∀ x ∈ t, ∃ y ∈ s, edist x y ≤ ediam (s ∪ t)

Tactic:
intro z

Goal state after:
case refine_2
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
x : α
xs : x ∈ s
y : α
yt : y ∈ t
z : α
⊢ z ∈ t → ∃ y ∈ s, edist z y ≤ ediam (s ∪ t)
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 = ∅ → 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 : ∀ b < a, (Ioo b a).Nonempty
⊢ Iio a = ⋃ l ∈ t, ⋃ u ∈ t, ⋃ (_ : l < u), ⋃ (_ : u ≤ a), Ico l u

pp: case pos
α : 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 : ∀ b < a, (Ioo b a).Nonempty
⊢ MeasurableSet (⋃ l ∈ t, ⋃ u ∈ t, ⋃ (_ : l < u), ⋃ (_ : u ≤ a), Ico l u)

Tactic:
· ext y
      push _ ∈ _
      constructor
      · 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.le, hly, hyu⟩
      · rintro ⟨l, -, u, -, -, hua, -, hyu⟩
        exact hyu.trans_le hua

Goal state after:
case pos
α : 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 : ∀ b < a, (Ioo b a).Nonempty
⊢ MeasurableSet (⋃ l ∈ t, ⋃ u ∈ t, ⋃ (_ : l < u), ⋃ (_ : u ≤ a), Ico l u)
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ E ⊆ (thickening δ (thickening δ E)ᶜ)ᶜ

Tactic:
intro x x_in_E
  simp only [thickening, mem_compl_iff, mem_ofPred_eq, not_lt]
  apply le_infEDist.mpr fun y hy ↦ ?_
  simp only [mem_compl_iff, mem_ofPred_eq, not_lt] at hy
  simpa only [edist_comm] using le_trans hy <| Metric.infEDist_le_edist_of_mem x_in_E

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

Goal state before:
pp: X : Type u
inst✝ : PseudoMetricSpace X
δ : ℝ
E : Set X
⊢ thickening δ E = ⋃ x ∈ E, ball x δ

Tactic:
by
  ext x
  simp only [mem_iUnion₂, exists_prop]
  exact mem_thickening_iff

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

Goal state before:
pp: case a
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ borel α ≤ MeasurableSpace.generateFrom {S | ∃ l u, l ≤ u ∧ Ioc l u = S}

Tactic:
borel_eq_generateFrom_Ioc

Goal state after:
case a
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ MeasurableSpace.generateFrom {S | ∃ l u, l < u ∧ Ioc l u = S} ≤
    MeasurableSpace.generateFrom {S | ∃ l u, l ≤ u ∧ Ioc l u = S}
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: case inl
α : Type u_2
inst✝ : PseudoMetricSpace α
δ : ℝ
hδ : 0 ≤ δ
hE : IsCompact ∅
⊢ cthickening δ ∅ = ⋃ x ∈ ∅, closedBall x δ

pp: case inr
α : Type u_2
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
hne : E.Nonempty
⊢ cthickening δ E = ⋃ x ∈ E, closedBall x δ

Tactic:
· simp only [cthickening_empty, biUnion_empty]

Goal state after:
case inr
α : Type u_2
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
hne : E.Nonempty
⊢ cthickening δ E = ⋃ x ∈ E, closedBall x δ
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 ∈ t, infEDist x s ≤ ENNReal.ofReal r

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

Goal state after:
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
M : α → α
hM : ∀ x ∈ s, x < M x
y : α → α
hy : ∀ x ∈ s, y x ∈ Ioi x
h'y : ∀ x ∈ s, Ioo x (y x) ⊆ s
x : α
hx : x ∈ s \ interior s
x' : α
hx' : x' ∈ s \ interior s
hxx' : x ≠ x'
⊢ Function.onFun Disjoint (fun x ↦ Ioo x (y x)) x x'

Tactic:
rcases lt_or_gt_of_ne hxx' with (h' | h')

Goal state after:
case inl
α : Type u_1
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
M : α → α
hM : ∀ x ∈ s, x < M x
y : α → α
hy : ∀ x ∈ s, y x ∈ Ioi x
h'y : ∀ x ∈ s, Ioo x (y x) ⊆ s
x : α
hx : x ∈ s \ interior s
x' : α
hx' : x' ∈ s \ interior s
hxx' : x ≠ x'
h' : x < x'
⊢ Function.onFun Disjoint (fun x ↦ Ioo x (y x)) x x'

case inr
α : Type u_1
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
M : α → α
hM : ∀ x ∈ s, x < M x
y : α → α
hy : ∀ x ∈ s, y x ∈ Ioi x
h'y : ∀ x ∈ s, Ioo x (y x) ⊆ s
x : α
hx : x ∈ s \ interior s
x' : α
hx' : x' ∈ s \ interior s
hxx' : x ≠ x'
h' : x' < x
⊢ Function.onFun Disjoint (fun x ↦ Ioo x (y x)) x x'
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝² : Countable ι
inst✝¹ : TopologicalSpace β
f : α → β
inst✝ : PseudoMetrizableSpace β
m : MeasurableSpace α
μ : ι → Measure α
h : ∀ (i : ι), AEStronglyMeasurable f (μ i)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
t : ι → Set β
t_sep : ∀ (i : ι), IsSeparable (t i)
ht : ∀ (i : ι), f ⁻¹' t i ∈ ae (μ i)
i : ι
x : α
hx : x ∈ f ⁻¹' t i
⊢ ∃ i, f x ∈ t i

Tactic:
exact ⟨i, hx⟩

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, f n a ≤ f n.succ a
s : Set α
hs : {a | ¬∀ (i : ℕ), f i a ≤ f i.succ a} ⊆ s ∧ MeasurableSet s ∧ μ s = 0
g : ℕ → α → ℝ≥0∞ := fun n a ↦ if a ∈ s then 0 else f n a
g_eq_f : ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), g n a = f n a
a : α
ha : ∀ (n : ℕ), g n a = f n a
⊢ (fun a ↦ ⨆ n, f n a) a = (fun a ↦ ⨆ n, g n a) a

Tactic:
simp only [ha]

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
hf : ∀ a ∈ s, a ∈ t → f a ≤ 1
hf' : ∀ a ∈ s, a ∉ t → f a = 0
⊢ ∫⁻ (a : α), s.indicator f a ∂μ ≤ μ t

Tactic:
refine lintegral_le_meas (fun a ↦ ?_) (by simp_all)

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
hf : ∀ a ∈ s, a ∈ t → f a ≤ 1
hf' : ∀ a ∈ s, a ∉ t → f a = 0
a : α
⊢ s.indicator f a ≤ 1
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
⊢ ∫⁻ (x : α) in ∅, f x ∂μ = 0

Tactic:
Measure.restrict_empty,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
⊢ ∫⁻ (x : α), f x ∂0 = 0
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : TopologicalSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
h : SecondCountableTopologyEither α β
f : α → β
hf : Continuous[inst✝³, inst✝¹] f
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
h✝ : SecondCountableTopology α
⊢ StronglyMeasurable f

Tactic:
rw [stronglyMeasurable_iff_measurable_separable]

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : TopologicalSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
h : SecondCountableTopologyEither α β
f : α → β
hf : Continuous[inst✝³, inst✝¹] f
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
h✝ : SecondCountableTopology α
⊢ Measurable f ∧ IsSeparable (range f)
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : One β
f : α → β
hf : Continuous[inst✝⁴, inst✝²] f
k : Set α
hk : IsCompact k
h'f : mulSupport f ⊆ k
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
⊢ StronglyMeasurable f

Tactic:
rw [stronglyMeasurable_iff_measurable_separable]

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : One β
f : α → β
hf : Continuous[inst✝⁴, inst✝²] f
k : Set α
hk : IsCompact k
h'f : mulSupport f ⊆ k
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
⊢ Measurable f ∧ IsSeparable (range f)
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: case h.left
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
s t : Finset β
⊢ (fun x1 x2 ↦ x1 ≤ x2) ((fun s a ↦ ∑ i ∈ s, f i a) s) ((fun s a ↦ ∑ i ∈ s, f i a) (s ∪ t))

pp: case h.right
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
s t : Finset β
⊢ (fun x1 x2 ↦ x1 ≤ x2) ((fun s a ↦ ∑ i ∈ s, f i a) t) ((fun s a ↦ ∑ i ∈ s, f i a) (s ∪ t))

Tactic:
· exact fun a => Finset.sum_le_sum_of_subset Finset.subset_union_left

Goal state after:
case h.right
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
s t : Finset β
⊢ (fun x1 x2 ↦ x1 ≤ x2) ((fun s a ↦ ∑ i ∈ s, f i a) t) ((fun s a ↦ ∑ i ∈ s, f i a) (s ∪ t))
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSingletonClass α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
h : SecondCountableTopologyEither α β
f : α → β
s : Set α
hf : ContinuousOn f s
hs : sᶜ.Countable
⊢ MeasurableSet s

Tactic:
simpa using hs.measurableSet.compl

Goal state after:
Module: Mathlib.Topology.Perfect

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
C U : Set α
hC : Perfect C
x : α
xC : x ∈ C
xU : x ∈ U
Uop : IsOpen[inst✝] U
⊢ Perfect (closure[inst✝] (U ∩ C)) ∧ (closure[inst✝] (U ∩ C)).Nonempty

Tactic:
by
  constructor
  · apply Preperfect.perfect_closure
    exact hC.acc.open_inter Uop
  apply Nonempty.closure
  exact ⟨x, ⟨xU, xC⟩⟩

Goal state after:
Module: Mathlib.Topology.Perfect

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed[inst✝¹] C
b : Set (Set α)
bct : b.Countable
left✝ : ∅ ∉ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ (U ∩ C).Countable}
V : Set α := ⋃ U ∈ v, U
D : Set α := C \ V
Vct : (V ∩ C).Countable
x : α
xD : x ∈ D
E : Set α
⊢ E ∈ 𝓝 x → ∃ y ∈ E ∩ D, y ≠ x

Tactic:
xE

Goal state after:
case refine_2
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed[inst✝¹] C
b : Set (Set α)
bct : b.Countable
left✝ : ∅ ∉ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ (U ∩ C).Countable}
V : Set α := ⋃ U ∈ v, U
D : Set α := C \ V
Vct : (V ∩ C).Countable
x : α
xD : x ∈ D
E : Set α
xE : E ∈ 𝓝 x
⊢ ∃ y ∈ E ∩ D, y ≠ x
Module: Mathlib.Analysis.Normed.Group.FunctionSeries

Goal state before:
pp: β : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
ι : Type u_4
f : ι → β → F
u : ι → ℝ
hu : Summable u
s : Set β
ε : ℝ
εpos : ε > 0
t : Finset ι
ht : ∀ (b : Finset ι), t ⊆ b → ∑' (a : { x // x ∉ b }), u ↑a < ε
N : Set ι
hN : N ∈ cofinite
HN : ∀ y ∈ N, ∀ x ∈ s, ‖f y x‖ ≤ u y
n : Finset ι
hn : Finite.toFinset hN ∪ t ⊆ n
x : β
hx : x ∈ s
A : Summable fun n ↦ ‖f n x‖
⊢ dist (∑' (n : ι), f n x) (∑ n ∈ n, f n x) < ε

Tactic:
rw [dist_eq_norm, ← A.of_norm.sum_add_tsum_subtype_compl n, add_sub_cancel_left]

Goal state after:
β : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
ι : Type u_4
f : ι → β → F
u : ι → ℝ
hu : Summable u
s : Set β
ε : ℝ
εpos : ε > 0
t : Finset ι
ht : ∀ (b : Finset ι), t ⊆ b → ∑' (a : { x // x ∉ b }), u ↑a < ε
N : Set ι
hN : N ∈ cofinite
HN : ∀ y ∈ N, ∀ x ∈ s, ‖f y x‖ ≤ u y
n : Finset ι
hn : Finite.toFinset hN ∪ t ⊆ n
x : β
hx : x ∈ s
A : Summable fun n ↦ ‖f n x‖
⊢ ‖∑' (x_1 : { x // x ∉ n }), f (↑x_1) x‖ < ε
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: case left
α : Type ?u.3
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a✝ b✝ c d : α
h : a✝ ≤ b✝
δ : α
a b : ℝ
x y : ↑(Icc a b)
t : ↑unitInterval
⊢ a ≤ (1 - ↑t) * ↑x + ↑t * ↑y

Tactic:
nlinarith [x.2.1, y.2.1, t.2.1, t.2.2]

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

Goal state before:
pp: case mp.h₁
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hy : y ∈ cylinder x n
⊢ cylinder y n ⊆ cylinder x n

Tactic:
intro z

Goal state after:
case mp.h₁
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hy : y ∈ cylinder x n
z : (n : ℕ) → E n
⊢ z ∈ cylinder y n → z ∈ cylinder x n
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case mp.h₂
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hy : y ∈ cylinder x n
⊢ cylinder x n ⊆ cylinder y n

Tactic:
intro z

Goal state after:
case mp.h₂
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hy : y ∈ cylinder x n
z : (n : ℕ) → E n
⊢ z ∈ cylinder x n → z ∈ cylinder y n
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case mpr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
h : cylinder y n = cylinder x n
⊢ y ∈ cylinder x n

Tactic:
← h

Goal state after:
case mpr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
h : cylinder y n = cylinder x n
⊢ y ∈ cylinder y n