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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : OuterMeasure α
ι : Type ?u.14
f : ι → OuterMeasure α
s : ℕ → Set α
x✝ : Pairwise (Disjoint on s)
⊢ ∑' (i : ι), (f i) (⋃ i, s i) ≤ ∑' (i : ℕ) (i_1 : ι), (f i_1) (s i)

Tactic:
by
    rw [ENNReal.tsum_comm]; exact ENNReal.tsum_le_tsum fun i => measure_iUnion_le _

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

Goal state before:
pp: case cons
δ : Type u_4
X : δ → Type u_6
inst✝ : (i : δ) → MeasurableSpace (X i)
s : (i : δ) → Set (X i)
hs : ∀ (i : δ), MeasurableSet (s i)
i : δ
l : List δ
ih : MeasurableSet (Set.tprod l s)
⊢ MeasurableSet (Set.tprod (i :: l) s)

Tactic:
exact (hs i).prod ih

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: a : SignType
ha : a ≠ 0
⊢ a * id a = 1

Tactic:
cases a <;> trivial

Goal state after:
Module: Mathlib.Data.Nat.Cast.Order.Field

Goal state before:
pp: case zero
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
m : ℕ
⊢ ↑(m / 0) ≤ ↑m / ↑0

Tactic:
cast_zero,

Goal state after:
case zero
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
m : ℕ
⊢ ↑(m / 0) ≤ ↑m / 0
Module: Mathlib.Topology.Algebra.Algebra

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
A : Type u
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : IsSemitopologicalSemiring A
s : Subalgebra R A
B : Type u_2
inst✝³ : TopologicalSpace B
inst✝² : Ring B
inst✝¹ : IsSemitopologicalRing B
inst✝ : Algebra R B
f : B →ₐ[R] A
f' : B ≃ₜ A
w : ⇑f = ⇑f'
⊢ ↑(comap f s.topologicalClosure) = ↑(comap f s).topologicalClosure

Tactic:
simp only [Subalgebra.topologicalClosure_coe]

Goal state after:
R : Type u_1
inst✝⁸ : CommSemiring R
A : Type u
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : IsSemitopologicalSemiring A
s : Subalgebra R A
B : Type u_2
inst✝³ : TopologicalSpace B
inst✝² : Ring B
inst✝¹ : IsSemitopologicalRing B
inst✝ : Algebra R B
f : B →ₐ[R] A
f' : B ≃ₜ A
w : ⇑f = ⇑f'
⊢ ↑(comap f s.topologicalClosure) = closure[inst✝³] ↑(comap f s)
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case mp.zero
x y : EReal
h : ↑(sign x) * ↑x.abs ≤ ↑(sign y) * ↑y.abs
hs : sign x = sign y
hy : sign y = zero
⊢ sign x = neg ∧ zero = neg ∧ y.abs ≤ x.abs ∨ sign x = zero ∧ zero = zero ∨ sign x = pos ∧ zero = pos ∧ x.abs ≤ y.abs

Tactic:
rw [hs, hy] at h ⊢

Goal state after:
case mp.zero
x y : EReal
h : ↑zero * ↑x.abs ≤ ↑zero * ↑y.abs
hs : sign x = sign y
hy : sign y = zero
⊢ zero = neg ∧ zero = neg ∧ y.abs ≤ x.abs ∨ zero = zero ∧ zero = zero ∨ zero = pos ∧ zero = pos ∧ x.abs ≤ y.abs
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case mp.neg
x y : EReal
h : ↑(sign x) * ↑x.abs ≤ ↑(sign y) * ↑y.abs
hs : sign x = sign y
hy : sign y = neg
⊢ sign x = neg ∧ neg = neg ∧ y.abs ≤ x.abs ∨ sign x = zero ∧ neg = zero ∨ sign x = pos ∧ neg = pos ∧ x.abs ≤ y.abs

Tactic:
rw [hs, hy] at h ⊢

Goal state after:
case mp.neg
x y : EReal
h : ↑neg * ↑x.abs ≤ ↑neg * ↑y.abs
hs : sign x = sign y
hy : sign y = neg
⊢ neg = neg ∧ neg = neg ∧ y.abs ≤ x.abs ∨ neg = zero ∧ neg = zero ∨ neg = pos ∧ neg = pos ∧ x.abs ≤ y.abs
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case mp.pos
x y : EReal
h : ↑(sign x) * ↑x.abs ≤ ↑(sign y) * ↑y.abs
hs : sign x = sign y
hy : sign y = pos
⊢ sign x = neg ∧ pos = neg ∧ y.abs ≤ x.abs ∨ sign x = zero ∧ pos = zero ∨ sign x = pos ∧ pos = pos ∧ x.abs ≤ y.abs

Tactic:
rw [hs, hy] at h ⊢

Goal state after:
case mp.pos
x y : EReal
h : ↑pos * ↑x.abs ≤ ↑pos * ↑y.abs
hs : sign x = sign y
hy : sign y = pos
⊢ pos = neg ∧ pos = neg ∧ y.abs ≤ x.abs ∨ pos = zero ∧ pos = zero ∨ pos = pos ∧ pos = pos ∧ x.abs ≤ y.abs
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: α : Type u_3
f : Filter α
u v : α → EReal
h : liminf u f = ⊤
h' : liminf v f ≠ ⊥
⊢ liminf (u + v) f = ⊤

Tactic:
by
  apply top_le_iff.1 (le_trans _ le_liminf_add)
  rw [h, top_add_of_ne_bot h']

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: x r : ℝ≥0∞
ε : ℝ≥0
hr : r < 1
h : ∀ (n : ℕ), x ≤ ↑ε * r ^ n
⊢ Tendsto (fun n ↦ ↑ε * r ^ n) atTop (𝓝 0)

Tactic:
← mul_zero (M₀ := ℝ≥0∞) (a := ε)

Goal state after:
x r : ℝ≥0∞
ε : ℝ≥0
hr : r < 1
h : ∀ (n : ℕ), x ≤ ↑ε * r ^ n
⊢ Tendsto (fun n ↦ ↑ε * r ^ n) atTop (𝓝 (↑ε * 0))
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set (OuterMeasure α)
h : m.Nonempty
t : Set α
⊢ ⨆ (_ : t.Nonempty), sInfGen m t = ⨅ μ ∈ m, μ t

Tactic:
rcases t.eq_empty_or_nonempty with (rfl | ht)

Goal state after:
case inl
α : Type u_1
m : Set (OuterMeasure α)
h : m.Nonempty
⊢ ⨆ (_ : ∅.Nonempty), sInfGen m ∅ = ⨅ μ ∈ m, μ ∅

case inr
α : Type u_1
m : Set (OuterMeasure α)
h : m.Nonempty
t : Set α
ht : t.Nonempty
⊢ ⨆ (_ : t.Nonempty), sInfGen m t = ⨅ μ ∈ m, μ t
Module: Mathlib.Order.SetDissipate

Goal state before:
pp: case h₁
α : Type u_1
β : Type u_2
inst✝ : Preorder α
s : α → Set β
x : α
⊢ ⋂ y, ⋂ (_ : y ≤ x), dissipate s y ⊆ dissipate s x

pp: case h₂
α : Type u_1
β : Type u_2
inst✝ : Preorder α
s : α → Set β
x : α
⊢ dissipate s x ⊆ ⋂ y, ⋂ (_ : y ≤ x), dissipate s y

Tactic:
· apply iInter_mono fun z y hy ↦ ?_
    simp only [mem_iInter, mem_dissipate] at *
    exact fun h ↦ hy h z le_rfl

Goal state after:
case h₂
α : Type u_1
β : Type u_2
inst✝ : Preorder α
s : α → Set β
x : α
⊢ dissipate s x ⊆ ⋂ y, ⋂ (_ : y ≤ x), dissipate s y
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case cons
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
t✝ : Finset (Set α)
a : Set α
t : Finset (Set α)
hat : a ∉ t
t_ne : t.Nonempty
ih : (∀ s ∈ t, s ∈ S) → (⋂ s ∈ t, s).Nonempty → ⋂ s ∈ t, s ∈ S
h' : (a ∩ ⋂ x ∈ t, x).Nonempty
ht : ∀ (s : Set α), s = a ∨ s ∈ t → s ∈ S
⊢ ⋂ x ∈ t, x ∈ S

Tactic:
refine ih (fun s hs ↦ ?_) h'.right

Goal state after:
case cons
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
t✝ : Finset (Set α)
a : Set α
t : Finset (Set α)
hat : a ∉ t
t_ne : t.Nonempty
ih : (∀ s ∈ t, s ∈ S) → (⋂ s ∈ t, s).Nonempty → ⋂ s ∈ t, s ∈ S
h' : (a ∩ ⋂ x ∈ t, x).Nonempty
ht : ∀ (s : Set α), s = a ∨ s ∈ t → s ∈ S
s : Set α
hs : s ∈ t
⊢ s ∈ S
Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory

Goal state before:
pp: case insert
α : Type u
m : OuterMeasure α
ι : Type u_1
s : ι → Set α
i : ι
t : Finset ι
hi : i ∉ t
IH : (∀ i ∈ ↑t, m.IsCaratheodory (s i)) → m.IsCaratheodory (⋃ i ∈ ↑t, s i)
h : ∀ i_1 ∈ ↑(insert i t), m.IsCaratheodory (s i_1)
⊢ m.IsCaratheodory (⋃ i_1 ∈ ↑(insert i t), s i_1)

Tactic:
simp only [Finset.mem_coe, Finset.mem_insert, iUnion_iUnion_eq_or_left] at h ⊢
    exact m.isCaratheodory_union (h _ <| Or.inl rfl) (IH fun _ hj ↦ h _ <| Or.inr hj)

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case refine_2.inr
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ {univ}
⊢ s ∈ {s | ∃ t, ↑t ⊆ {i} ∧ ∃ f, (∀ x ∈ t, f x ∈ π x) ∧ s = ⋂ x ∈ t, f x}

Tactic:
refine ⟨∅, ?_⟩
      simpa only [Finset.coe_empty, subset_singleton_iff, mem_empty_iff_false, IsEmpty.forall_iff,
        imp_true_iff, Finset.notMem_empty, iInter_false, iInter_univ, true_and,
        exists_const] using! hs

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
s' : Set α
⊢ s' ∈ piiUnionInter (fun i ↦ {s i}) S ↔ s' ∈ {s' | ∃ t, ∃ (_ : ↑t ⊆ S), s' = ⋂ i ∈ t, s i}

Tactic:
simp_rw [piiUnionInter, Set.mem_singleton_iff, exists_prop, Set.mem_ofPred_eq]

Goal state after:
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
s' : Set α
⊢ (∃ t, ↑t ⊆ S ∧ ∃ f, (∀ x ∈ t, f x = s x) ∧ s' = ⋂ x ∈ t, f x) ↔ ∃ t, ↑t ⊆ S ∧ s' = ⋂ i ∈ t, s i
Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
⊢ μ s = ⨅ i, ⨅ (_ : s ⊆ i), ⨅ (_ : MeasurableSet i), μ i

Tactic:
← measure_eq_iInf

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

Goal state before:
pp: case h
α : Type u_1
s : Set α
⊢ (fun x ↦ x ∈ s) ⁻¹' ∅ = ∅

pp: case h
α : Type u_1
t : Set α
⊢ (fun x ↦ x ∈ t) ⁻¹' {True} = t

pp: case mpr.inr.inr.inl
α : Type u_1
s : Set α
⊢ ∃ s', (fun x ↦ x ∈ s) ⁻¹' s' = sᶜ

pp: case mpr.inr.inr.inr
α : Type u_1
s : Set α
⊢ ∃ s', (fun x ↦ x ∈ s) ⁻¹' s' = univ

Tactic:
(Batteries.Tactic.«tacticOn_goal-_=>_»
 "on_goal"
 []
 (num "3")
 "=>"
 (Tactic.tacticSeq
  (Tactic.tacticSeq1Indented
   [(Mathlib.Tactic.useSyntax
     "use"
     []
     (group)
     [(choice
       («term{_}» "{" [`False] "}")
       (Term.structInst
        "{"
        []
        (Term.structInstFields [(Term.structInstField (Term.structInstLVal `False []) [])])
        (Term.optEllipsis [])
        []
        "}"))])])))

Goal state after:
case h
α : Type u_1
s : Set α
⊢ (fun x ↦ x ∈ s) ⁻¹' ∅ = ∅

case h
α : Type u_1
t : Set α
⊢ (fun x ↦ x ∈ t) ⁻¹' {True} = t

case h
α : Type u_1
s : Set α
⊢ (fun x ↦ x ∈ s) ⁻¹' {False} = sᶜ

case mpr.inr.inr.inr
α : Type u_1
s : Set α
⊢ ∃ s', (fun x ↦ x ∈ s) ⁻¹' s' = univ
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
inst✝ : Nonempty α
hf : MeasurableEmbedding f
⊢ LeftInverse hf.invFun f

Tactic:
by
  intro x
  simp [MeasurableEmbedding.invFun]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure α
s✝ : Set α
inst✝ : MeasurableSpace β
f : OuterMeasure α →ₗ[ℝ≥0∞] OuterMeasure β
hf : ∀ (μ : Measure α), inst✝ ≤ (f μ.toOuterMeasure).caratheodory
μ₁ μ₂ : Measure α
s : Set β
hs : MeasurableSet s
⊢ ((f (μ₁ + μ₂).toOuterMeasure).toMeasure ⋯) s =
    ((f μ₁.toOuterMeasure).toMeasure ⋯ + (f μ₂.toOuterMeasure).toMeasure ⋯) s

Tactic:
simp only [map_add, coe_add, Pi.add_apply, toMeasure_apply, add_toOuterMeasure,
      FunLike.coe_add, hs]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
μ : Measure α
⊢ (mapₗ f) μ = (mapₗ (AEMeasurable.mk f ⋯)) μ

Tactic:
exact mapₗ_congr hf hf.aemeasurable.measurable_mk hf.aemeasurable.ae_eq_mk

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

Goal state before:
pp: case refine_1
α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν : Measure α
h : μ₁ + μ₂ ≪ ν
⊢ μ₁ ≪ ν ∧ μ₂ ≪ ν

Tactic:
have : ∀ s, ν s = 0 → μ₁ s = 0 ∧ μ₂ s = 0 := by intro s hs0; simpa using h hs0

Goal state after:
case refine_1
α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν : Measure α
h : μ₁ + μ₂ ≪ ν
this : ∀ (s : Set α), ν s = 0 → μ₁ s = 0 ∧ μ₂ s = 0
⊢ μ₁ ≪ ν ∧ μ₂ ≪ ν
Module: Mathlib.MeasureTheory.OuterMeasure.BorelCantelli

Goal state before:
pp: case h
α : Type u_1
ι : Type u_2
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
inst✝ : Countable ι
μ : F
s : ι → Set α
hs : ∑' (i : ι), μ (s i) ≠ ∞
t : Finset ι
⊢ ⨅ i, ⨅ (_ : i.Finite), ⨆ a ∈ iᶜ, s a ⊆ ⋃ x, ⋃ (hx : x ∉ t), s ↑⟨x, hx⟩

Tactic:
exact iInter₂_subset _ t.finite_toSet

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⟩
⊢ a < a

Tactic:
calc
      a ≤ c := by simpa using hac
      _ < b := by simpa using hcb
      _ ≤ a := by simpa using ha

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst✝ : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), μ (t i) ≤ μ (s i)
⊢ μ (⋃ i, s i) ≤ μ (⋃ i, t i)

Tactic:
by gcongr; apply hsub

Goal state after:
Module: Mathlib.Topology.Order.AtTopBotIxx

Goal state before:
pp: X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
α : Type u_2
l : Filter α
f : X → α
ha : IsPredPrelimit a
⊢ Tendsto (fun x ↦ f ↑x) atBot l ↔ Tendsto f (𝓝[>] a) l

Tactic:
by
  rw [← map_coe_Ioi_atBot a ha, tendsto_map'_iff, Function.comp_def]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s₁ s₂ t₁ t₂ : Set α
hs : s₁ ⊆ s₂
hsμ : μ s₂ ≤ μ s₁
ht : t₁ ⊆ t₂
htμ : μ t₂ ≤ μ t₁
⊢ μ (⋃ b, bif b then s₁ else t₁) = μ (⋃ b, bif b then s₂ else t₂)

Tactic:
exact measure_iUnion_congr_of_subset (Bool.forall_bool.2 ⟨ht, hs⟩) (Bool.forall_bool.2 ⟨htμ, hsμ⟩)

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : MeasurableSet t
⊢ (μ.restrict s) t = 0 ↔ μ (t ∩ s) = 0

Tactic:
restrict_apply ht

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : MeasurableSet t
⊢ μ (t ∩ s) = 0 ↔ μ (t ∩ s) = 0
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
H : μ.restrict s = ν.restrict s
t : Set α
hts : t ⊆ s
ht : MeasurableSet t
⊢ (ν.restrict s) t = ν (t ∩ s)

Tactic:
restrict_apply ht

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
H : μ.restrict s = ν.restrict s
t : Set α
hts : t ⊆ s
ht : MeasurableSet t
⊢ ν (t ∩ s) = ν (t ∩ s)
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : 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
⊢ ⋃₀ D =ᵐ[μ] s ∪ ⋃₀ D

Tactic:
apply ae_eq_of_ae_subset_of_measure_ge subset_union_right.eventuallyLE

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

case hsm
α : 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
⊢ NullMeasurableSet (⋃₀ D) μ

case ht
α : 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) ≠ ∞
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

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

Tactic:
apply EventuallyLE.measure_le

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : ∀ᵐ (a : α) ∂μ, a ∈ t
⊢ s ≤ᵐ[μ] t ∩ s
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ≪ ν
s t : Set α
ht : MeasurableSet t
htν : (ν.restrict s) t = 0
⊢ (μ.restrict s) t = 0

Tactic:
restrict_apply ht

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ≪ ν
s t : Set α
ht : MeasurableSet t
htν : ν (t ∩ s) = 0
⊢ μ (t ∩ s) = 0
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : LinearOrder α
a b : α
⊢ ae (μ.restrict (Ι a b)) = ae (μ.restrict (Ioc a b)) ⊔ ae (μ.restrict (Ioc b a))

Tactic:
by
  simp only [uIoc_eq_union, ae_restrict_union_eq]

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : f =ᵐ[μ.restrict sᶜ] fun x ↦ b
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
⊢ μ (f ⁻¹' t) = (μ.restrict s) (f ⁻¹' t)

Tactic:
rw [Measure.restrict_apply₀ (f_mble t_mble)]

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : f =ᵐ[μ.restrict sᶜ] fun x ↦ b
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
⊢ μ (f ⁻¹' t) = μ (f ⁻¹' t ∩ s)
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: case refine_1
α : 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 ∅
⊢ ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ μ_1 ∈ toOuterMeasure '' {μ, ν}, μ_1 (t n) ≤ μ (t ∩ s) + ν (tᶜ ∩ s)

Tactic:
refine (iInf₂_le t' fun x hx ↦ ?_).trans ?_

Goal state after:
case refine_1.refine_1
α : 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 ∅
x : α
hx : x ∈ s
⊢ x ∈ iUnion t'

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 ∅
⊢ ∑' (n : ℕ), ⨅ μ_1 ∈ toOuterMeasure '' {μ, ν}, μ_1 (t' n) ≤ μ (t ∩ s) + ν (tᶜ ∩ s)
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: case pos
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = 0 x
x : α
hx : x ∈ s → f x = 0 x
hxs : x ∈ s
⊢ s.indicator f x = 0 x

pp: case neg
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = 0 x
x : α
hx : x ∈ s → f x = 0 x
hxs : x ∉ s
⊢ s.indicator f x = 0 x

Tactic:
· simp only [hxs, hx hxs, Set.indicator_of_mem]

Goal state after:
case neg
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = 0 x
x : α
hx : x ∈ s → f x = 0 x
hxs : x ∉ s
⊢ s.indicator f x = 0 x
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t' : ℕ → Set α
ht' : s ⊆ iUnion t'
t : Set α := ⋃ n ∈ {k | μ (t' k) ≤ ν (t' k)}, t' n
ht : t = ⋃ n ∈ {k | μ (t' k) ≤ ν (t' k)}, t' n
hle₁ : μ (t ∩ s) ≤ ∑' (n : ↑{k | μ (t' k) ≤ ν (t' k)}), μ (t' ↑n)
x : α
x✝ : x ∈ (⋂ i ∈ {k | μ (t' k) ≤ ν (t' k)}, (t' i)ᶜ) ∩ s
hx₁ : x ∈ ⋂ i ∈ {k | μ (t' k) ≤ ν (t' k)}, (t' i)ᶜ
hx₂ : x ∈ s
i : ℕ
hi : x ∈ t' i
⊢ ∃ i, ∃ (_ : i ∈ {k | ν (t' k) < μ (t' k)}), x ∈ t' i

Tactic:
refine ⟨i, ?_, hi⟩

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t' : ℕ → Set α
ht' : s ⊆ iUnion t'
t : Set α := ⋃ n ∈ {k | μ (t' k) ≤ ν (t' k)}, t' n
ht : t = ⋃ n ∈ {k | μ (t' k) ≤ ν (t' k)}, t' n
hle₁ : μ (t ∩ s) ≤ ∑' (n : ↑{k | μ (t' k) ≤ ν (t' k)}), μ (t' ↑n)
x : α
x✝ : x ∈ (⋂ i ∈ {k | μ (t' k) ≤ ν (t' k)}, (t' i)ᶜ) ∩ s
hx₁ : x ∈ ⋂ i ∈ {k | μ (t' k) ≤ ν (t' k)}, (t' i)ᶜ
hx₂ : x ∈ s
i : ℕ
hi : x ∈ t' i
⊢ i ∈ {k | ν (t' k) < μ (t' k)}
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: case inr
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
mβ : MeasurableSpace β
inst✝¹ : LinearOrder α
inst✝ : atTop.IsCountablyGenerated
x : α
g : α → β
g_meas : ∀ t > x, AEMeasurable g (μ.restrict (Ioc x t))
this : Nonempty α
u : ℕ → α
hu_tendsto : Tendsto u atTop atTop
Ioi_eq_iUnion : Ioi x = ⋃ n, Ioc x (u n)
n : ℕ
h : u n ≤ x
⊢ AEMeasurable g (μ.restrict (Ioc x (u n)))

Tactic:
· rw [Ioc_eq_empty (not_lt.mpr h), Measure.restrict_empty]
    exact aemeasurable_zero_measure

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
t : Set α
ht : t ∈ range Ioi
⊢ MeasurableSet t

Tactic:
obtain ⟨u, rfl⟩ := ht

Goal state after:
case refine_1
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
u : α
⊢ MeasurableSet (Ioi u)
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 : Set α
ht : t ∈ range Iic
⊢ MeasurableSet t

Tactic:
obtain ⟨u, rfl⟩ := ht

Goal state after:
case refine_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
u : α
⊢ MeasurableSet (Iic u)
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
μ : 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ι : IsEmpty ι
⊢ AEMeasurable g μ

Tactic:
simp only [IsEmpty.exists_iff, ofPred_false, isLUB_empty_iff] at hg
    exact aemeasurable_const' (hg.mono fun a ha => hg.mono fun b hb => (ha _).antisymm (hb _))

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

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

Tactic:
by
  induction n with
  | zero =>
    simp [eapproxDiff, (eapprox_lt_top f 0 a).ne]
  | succ n IH =>
    rw [Finset.sum_range_succ, IH, eapproxDiff, coe_map, Function.comp_apply,
      coe_sub, Pi.sub_apply, ENNReal.coe_toNNReal,
      add_tsub_cancel_of_le (monotone_eapprox f (Nat.le_succ _) _)]
    apply (lt_of_le_of_lt _ (eapprox_lt_top f (n + 1) a)).ne
    rw [tsub_le_iff_right]
    exact le_self_add

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 : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hα : Nonempty α
i : ι
c : α
⊢ MeasurableSet {x | f i x ≤ c}

Tactic:
exact measurableSet_le (hf i) measurable_const

Goal state after: