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

Goal state before:
pp: case As_disj
α : Type u_1
ι : Type u_4
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sfiniteSeq μ))
As_disj : Pairwise (AEDisjoint (sum (sfiniteSeq μ)) on As)
obs : {i | 0 < (sum (sfiniteSeq μ)) (As i)} ⊆ ⋃ n, {i | 0 < (sfiniteSeq μ n) (As i)}
n : ℕ
⊢ Pairwise (AEDisjoint (sfiniteSeq μ n) on As)

pp: case Union_As_finite
α : Type u_1
ι : Type u_4
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sfiniteSeq μ))
As_disj : Pairwise (AEDisjoint (sum (sfiniteSeq μ)) on As)
obs : {i | 0 < (sum (sfiniteSeq μ)) (As i)} ⊆ ⋃ n, {i | 0 < (sfiniteSeq μ n) (As i)}
n : ℕ
⊢ (sfiniteSeq μ n) (⋃ i, As i) ≠ ∞

Tactic:
· exact fun i j hij ↦ AEDisjoint.of_le (As_disj hij) (le_sum _ _)

Goal state after:
case Union_As_finite
α : Type u_1
ι : Type u_4
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sfiniteSeq μ))
As_disj : Pairwise (AEDisjoint (sum (sfiniteSeq μ)) on As)
obs : {i | 0 < (sum (sfiniteSeq μ)) (As i)} ⊆ ⋃ n, {i | 0 < (sfiniteSeq μ n) (As i)}
n : ℕ
⊢ (sfiniteSeq μ n) (⋃ i, As i) ≠ ∞
Module: Mathlib.MeasureTheory.Measure.Restrict

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

Tactic:
restrict_apply ht,

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

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

Tactic:
restrict_apply ht,

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
H : ∀ t ⊆ s, MeasurableSet t → μ t = ν t
t : Set α
ht : MeasurableSet t
⊢ μ (t ∩ s) = ν (t ∩ s)
Module: Mathlib.MeasureTheory.Measure.Trim

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
m₁ m₂ : MeasurableSpace α
hm₁₂ : m₁ ≤ m₂
hm₂ : m₂ ≤ m0
⊢ (μ.trim hm₂).trim hm₁₂ = μ.trim ⋯

Tactic:
by
  refine @Measure.ext _ m₁ _ _ (fun t ht => ?_)
  rw [trim_measurableSet_eq hm₁₂ ht, trim_measurableSet_eq (hm₁₂.trans hm₂) ht,
    trim_measurableSet_eq hm₂ (hm₁₂ t ht)]

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

Goal state before:
pp: α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
inst✝ : Countable ι
μ : ι → Measure α
s t : Set α
ht : MeasurableSet t
⊢ ((sum μ).restrict s) t = ∑' (i : ι), ((μ i).restrict s) t

Tactic:
restrict_apply ht,

Goal state after:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
inst✝ : Countable ι
μ : ι → Measure α
s t : Set α
ht : MeasurableSet t
⊢ (sum μ) (t ∩ s) = ∑' (i : ι), (μ i) (t ∩ s)
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
⊢ ¬ν ≤ μ ↔ ∃ s, μ s < ν s

Tactic:
simp only [le_iff', not_forall, not_le]

Goal state after:
Module: Mathlib.Order.Filter.CountableSeparatingOn

Goal state before:
pp: α : Type u_1
p : Set α → Prop
t : Set α
q : Set ↑t → Prop
h✝ : HasCountableSeparatingOn (↑t) q univ
hpq : ∀ (U : Set ↑t), q U → ∃ V, p V ∧ Subtype.val ⁻¹' V = U
S : Set (Set ↑t)
hSc : S.Countable
hSq : ∀ s ∈ S, q s
hS : ∀ x ∈ univ, ∀ y ∈ univ, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
V : Set ↑t → Set α
hpV : ∀ s ∈ S, p (V s)
hV : ∀ s ∈ S, Subtype.val ⁻¹' V s = s
x : α
hx : x ∈ t
y : α
hy : y ∈ t
h : ∀ s ∈ V '' S, x ∈ s ↔ y ∈ s
U : Set ↑t
hU : U ∈ S
⊢ ⟨x, hx⟩ ∈ U ↔ ⟨y, hy⟩ ∈ U

Tactic:
rw [← hV U hU]

Goal state after:
α : Type u_1
p : Set α → Prop
t : Set α
q : Set ↑t → Prop
h✝ : HasCountableSeparatingOn (↑t) q univ
hpq : ∀ (U : Set ↑t), q U → ∃ V, p V ∧ Subtype.val ⁻¹' V = U
S : Set (Set ↑t)
hSc : S.Countable
hSq : ∀ s ∈ S, q s
hS : ∀ x ∈ univ, ∀ y ∈ univ, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
V : Set ↑t → Set α
hpV : ∀ s ∈ S, p (V s)
hV : ∀ s ∈ S, Subtype.val ⁻¹' V s = s
x : α
hx : x ∈ t
y : α
hy : y ∈ t
h : ∀ s ∈ V '' S, x ∈ s ↔ y ∈ s
U : Set ↑t
hU : U ∈ S
⊢ ⟨x, hx⟩ ∈ Subtype.val ⁻¹' V U ↔ ⟨y, hy⟩ ∈ Subtype.val ⁻¹' V U
Module: Mathlib.Order.Filter.CountableSeparatingOn

Goal state before:
pp: α : Type u_1
p : Set α → Prop
t : Set α
⊢ HasCountableSeparatingOn (↑t) (fun u ↦ ∃ v, p v ∧ Subtype.val ⁻¹' v = u) univ ↔ HasCountableSeparatingOn α p t

Tactic:
by
  constructor <;> intro h
  · exact h.of_subtype <| fun s ↦ id
  rcases h with ⟨S, Sct, Sp, hS⟩
  use {Subtype.val ⁻¹' s | s ∈ S}, Sct.image _, ?_, ?_
  · rintro u ⟨t, tS, rfl⟩
    exact ⟨t, Sp _ tS, rfl⟩
  rintro x - y - hxy
  exact Subtype.val_injective <| hS _ (Subtype.coe_prop _) _ (Subtype.coe_prop _)
    fun s hs ↦ hxy (Subtype.val ⁻¹' s) ⟨s, hs, rfl⟩

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ n, v n
h'v : ∀ (n : ℕ), μ (t ∩ v n) ≠ ∞
w : ℕ → Set α := fun n ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), μ (w n) < ∞
t' : Set α := ⋃ n, toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ n, toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
⊢ ∑' (n : ℕ), (μ.restrict (t ∩ u)) (disjointed w n) = (μ.restrict (t ∩ u)) (⋃ n, disjointed w n)

Tactic:
by
        rw [measure_iUnion]
        · exact disjoint_disjointed _
        · intro i
          refine MeasurableSet.disjointed (fun n => ?_) i
          exact measurableSet_toMeasurable _ _

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
s t : Set α
ht : MeasurableSet t
⊢ (μ.restrict (toMeasurable μ s)) t = (μ.restrict s) t

Tactic:
restrict_apply ht,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
s t : Set α
ht : MeasurableSet t
⊢ μ (t ∩ toMeasurable μ s) = (μ.restrict s) t
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
s t : Set α
ht : MeasurableSet t
⊢ μ (s ∩ t) = (μ.restrict s) t

Tactic:
restrict_apply ht,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
s t : Set α
ht : MeasurableSet t
⊢ μ (s ∩ t) = μ (t ∩ s)
Module: Mathlib.MeasureTheory.Measure.Restrict

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

Tactic:
by
  rw [Subtype.instMeasurableSpace, comap_eq_generateFrom] at ht
  induction t, ht using generateFrom_induction with
  | hC t' ht' =>
    obtain ⟨s', hs', rfl⟩ := ht'
    rw [Subtype.image_preimage_coe]
    exact hs.inter (hs'.nullMeasurableSet)
  | empty => simp only [image_empty, nullMeasurableSet_empty]
  | compl t' _ ht' =>
    simp only [← range_sdiff_image Subtype.coe_injective, Subtype.range_coe_subtype, ofPred_mem_eq]
    exact hs.diff ht'
  | iUnion f _ hf =>
    rw [image_iUnion]
    exact .iUnion hf

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

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure β
s : Set α
⊢ (Measure.comap f μ).restrict s = Measure.comap f (μ.restrict (f '' s))

Tactic:
by
  rw [comap_restrict hf, preimage_image_eq _ hf.injective]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
x✝¹ : MeasurableSpace α
x✝ : MeasurableSpace β
f : α → β
g : β → α
μ : Measure α
hf : Measurable f
hg : MeasurableEmbedding g
hμg : ∀ᵐ (a : α) ∂μ, a ∈ range g
hfg : ∀ (a : β), f (g a) = a
s : Set β
hs : MeasurableSet s
⊢ μ (f ⁻¹' s) = μ (g '' s)

Tactic:
← measure_sdiff_null hμg

Goal state after:
α : Type u_2
β : Type u_3
x✝¹ : MeasurableSpace α
x✝ : MeasurableSpace β
f : α → β
g : β → α
μ : Measure α
hf : Measurable f
hg : MeasurableEmbedding g
hμg : ∀ᵐ (a : α) ∂μ, a ∈ range g
hfg : ∀ (a : β), f (g a) = a
s : Set β
hs : MeasurableSet s
⊢ μ (f ⁻¹' s \ {x | (fun a ↦ a ∈ range g) x}ᶜ) = μ (g '' s)
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
inst✝ : MeasureSpace α
s t : Set α
hs : NullMeasurableSet s volume
ht : MeasurableSet t
⊢ volume (Subtype.val ⁻¹' t) = volume (t ∩ s)

Tactic:
rw [volume_set_coe_def,
    comap_apply₀ _ _ Subtype.coe_injective
      (fun h => MeasurableSet.nullMeasurableSet_subtype_coe hs)
      (measurable_subtype_coe ht).nullMeasurableSet,
    image_preimage_eq_inter_range, Subtype.range_coe]

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

Goal state before:
pp: α : Type u_1
S : Set (Set α)
h : SeparatesPoints α
⊢ ∀ (x y : α), (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y

Tactic:
by
  let := generateFrom S
  intro x y hxy
  rw [← forall_generateFrom_mem_iff_mem_iff] at hxy
  exact separatesPoints_def <| fun _ hs ↦ (hxy _ hs).mp

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

Goal state before:
pp: case refine_1
α : Type u_1
t : ℕ → Set α
u : Set α
hu : u ∈ ⋃ n, memPartition t n
⊢ MeasurableSet u

Tactic:
simp only [mem_iUnion] at hu

Goal state after:
case refine_1
α : Type u_1
t : ℕ → Set α
u : Set α
hu : ∃ i, u ∈ memPartition t i
⊢ MeasurableSet u
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]

Goal state after:
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 f)
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
⊢ sᶜ ∈ μ.cofinite ↔ μ s < ∞

Tactic:
by rw [mem_cofinite, compl_compl]

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

Goal state before:
pp: M : Type u_2
ι : Type u_3
α : Type u_4
inst✝² : CommMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
f : ι → α → M
s : Finset ι
hf : ∀ i ∈ s, Measurable (f i)
⊢ Measurable fun a ↦ ∏ i ∈ s, f i a

Tactic:
simp_rw [← Finset.prod_apply]
  exact Finset.prod_induction _ _ (fun _ _ => Measurable.mul) (@measurable_one M _ _ _ _) hf

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

Goal state before:
pp: α : Type u_1
s : Set α
inst✝³ : TopologicalSpace α
mα : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
h : s.OrdConnected
⊢ MeasurableSet s

Tactic:
let u := ⋃ (x ∈ s) (y ∈ s), Ioo x y

Goal state after:
α : Type u_1
s : Set α
inst✝³ : TopologicalSpace α
mα : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
h : s.OrdConnected
u : Set α := ⋃ x ∈ s, ⋃ y ∈ s, Ioo x y
⊢ MeasurableSet s
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

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

Tactic:
by
  simpa only [exists_prop, mem_univ, true_and] using
    (@dense_univ α _).borel_eq_generateFrom_Icc_mem_aux (fun _ _ => mem_univ _) fun _ _ _ _ =>
      mem_univ _

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

Goal state before:
pp: α : Type u_1
γ : Type u_3
inst✝⁶ : TopologicalSpace α
inst✝⁵ : MeasurableSpace α
inst✝⁴ : OpensMeasurableSpace α
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
inst✝ : MeasurableSingletonClass α
f : α → γ
hf : {x | ¬ContinuousAt f x}.Countable
this : ContinuousOn f {x | ContinuousAt f x}
⊢ Measurable f

Tactic:
apply this.measurable_of_countable_compl

Goal state after:
α : Type u_1
γ : Type u_3
inst✝⁶ : TopologicalSpace α
inst✝⁵ : MeasurableSpace α
inst✝⁴ : OpensMeasurableSpace α
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
inst✝ : MeasurableSingletonClass α
f : α → γ
hf : {x | ¬ContinuousAt f x}.Countable
this : ContinuousOn f {x | ContinuousAt f x}
⊢ {x | ContinuousAt f x}ᶜ.Countable
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case mpr
α : 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
y l u : α
hua : u ≤ a
hyu : y < u
⊢ y < a

Tactic:
exact hyu.trans_le hua

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
x : α
xs : x ∈ s
this : infEDist x ∅ ≤ hausdorffEDist s ∅
⊢ hausdorffEDist s ∅ = ∞

Tactic:
simpa using this

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
E : Set α
x : α
h : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEDist x E
δ : ℝ
hδ : δ < ε
⊢ ENNReal.ofReal δ < infEDist x E

Tactic:
exact ((ofReal_lt_ofReal_iff ε_pos).mpr hδ).trans ε_lt

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

Goal state before:
pp: case e'_3.e'_2
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s✝ : Set α
hd : Dense s✝
hbot : ∀ (x : α), IsTop x → x ∈ s✝
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s✝
e_1✝¹ : MeasurableSpace α = MeasurableSpace αᵒᵈ
e_1✝ : α = αᵒᵈ
s : Set α
⊢ s ∈ {S | ∃ l ∈ s✝, ∃ u ∈ s✝, l < u ∧ Ioc l u = S} ↔
    s ∈ {S | ∃ l ∈ ⇑OrderDual.ofDual ⁻¹' s✝, ∃ u ∈ ⇑OrderDual.ofDual ⁻¹' s✝, l < u ∧ Ico l u = S}

Tactic:
constructor <;> rintro ⟨l, hl, u, hu, hlt, rfl⟩

Goal state after:
case e'_3.e'_2.mp
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsTop x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
e_1✝¹ : MeasurableSpace α = MeasurableSpace αᵒᵈ
e_1✝ : α = αᵒᵈ
l : α
hl : l ∈ s
u : α
hu : u ∈ s
hlt : l < u
⊢ Ioc l u ∈ {S | ∃ l ∈ ⇑OrderDual.ofDual ⁻¹' s, ∃ u ∈ ⇑OrderDual.ofDual ⁻¹' s, l < u ∧ Ico l u = S}

case e'_3.e'_2.mpr
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsTop x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
e_1✝¹ : MeasurableSpace α = MeasurableSpace αᵒᵈ
e_1✝ : α = αᵒᵈ
l : αᵒᵈ
hl : l ∈ ⇑OrderDual.ofDual ⁻¹' s
u : αᵒᵈ
hu : u ∈ ⇑OrderDual.ofDual ⁻¹' s
hlt : l < u
⊢ Ico l u ∈ {S | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ioc l u = S}
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x y : α
⊢ infDist x s ≤ infDist y s + dist x y

Tactic:
by
  rw [infDist, infDist, dist_edist]
  refine ENNReal.toReal_le_add' infEDist_le_infEDist_add_edist ?_ (flip absurd (edist_ne_top _ _))
  simp only [infEDist_eq_top_iff, imp_self]

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Canonical.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
a b c : α
inst✝³ : Add α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : AddLeftMono α
inst✝ : IsLeftCancelAdd α
⊢ a ≤ b + c ↔ a < b ∨ ∃ d ≤ c, a = b + d

Tactic:
by
  obtain h | h := lt_or_ge a b
  · have : a ≤ b + c := h.le.trans (le_self_add ..)
    tauto
  · obtain ⟨a, rfl⟩ := exists_add_of_le h
    simp

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
a : α
h : ⨆ k, ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k < f a
q : ℚ
left✝ : 0 ≤ q
lt_q : ⨆ k, ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k < ↑(↑q).toNNReal
q_lt : ↑(↑q).toNNReal < f a
⊢ ↑(↑q).toNNReal ≤ ⨆ (_ : ennrealRatEmbed (Encodable.encode q) ≤ f a), ennrealRatEmbed (Encodable.encode q)

Tactic:
ennrealRatEmbed_encode q

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
a : α
h : ⨆ k, ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k < f a
q : ℚ
left✝ : 0 ≤ q
lt_q : ⨆ k, ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k < ↑(↑q).toNNReal
q_lt : ↑(↑q).toNNReal < f a
⊢ ↑(↑q).toNNReal ≤ ⨆ (_ : ↑(↑q).toNNReal ≤ f a), ↑(↑q).toNNReal
Module: Mathlib.MeasureTheory.Function.SimpleFuncDense

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : PseudoEMetricSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace β
f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
n : ℕ
x : β
⊢ (approxOn f hf s y₀ h₀ n) x ∈ s

Tactic:
have : Nonempty s := ⟨⟨y₀, h₀⟩⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : PseudoEMetricSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace β
f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
n : ℕ
x : β
this : Nonempty ↑s
⊢ (approxOn f hf s y₀ h₀ n) x ∈ s
Module: Mathlib.MeasureTheory.Function.SimpleFuncDense

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : PseudoEMetricSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace β
f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
x : β
hx : f x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ Tendsto (fun n ↦ (approxOn f hf s y₀ h₀ n) x) atTop (𝓝 (f x))

Tactic:
have : Nonempty s := ⟨⟨y₀, h₀⟩⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : PseudoEMetricSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace β
f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
x : β
hx : f x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
this : Nonempty ↑s
⊢ Tendsto (fun n ↦ (approxOn f hf s y₀ h₀ n) x) atTop (𝓝 (f x))
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f g : α → ℝ≥0∞
hg : AEMeasurable g (μ.restrict s)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ g x
f' : α → ℝ≥0∞
hf'm : Measurable f'
hle : f' ≤ f
hf' : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, f' a ∂μ
⊢ ∫⁻ (a : α) in s, f' a ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ

Tactic:
apply lintegral_mono_ae

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f g : α → ℝ≥0∞
hg : AEMeasurable g (μ.restrict s)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ g x
f' : α → ℝ≥0∞
hf'm : Measurable f'
hle : f' ≤ f
hf' : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, f' a ∂μ
⊢ ∀ᵐ (a : α) ∂μ.restrict s, f' a ≤ g a
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 : 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
eq : ∀ (p : ℝ≥0∞), ⇑(SimpleFunc.map c rs) ⁻¹' {p} = ⋃ n, ⇑(SimpleFunc.map c rs) ⁻¹' {p} ∩ {a | p ≤ f n a}
mono : ∀ (r : ℝ≥0∞), Monotone fun n ↦ ⇑(SimpleFunc.map c rs) ⁻¹' {r} ∩ {a | r ≤ f n a}
h_meas : ∀ (n : ℕ), MeasurableSet {a | (SimpleFunc.map c rs) a ≤ f n a}
⊢ ⨆ n, ∑ r ∈ (SimpleFunc.map c rs).range, r * μ (⇑(SimpleFunc.map c rs) ⁻¹' {r} ∩ {a | r ≤ f n a}) ≤
    ⨆ n, ((SimpleFunc.map c rs).restrict {a | (SimpleFunc.map c rs) a ≤ f n a}).lintegral μ

Tactic:
gcongr with n
      rw [restrict_lintegral _ (h_meas n)]
      refine le_of_eq (Finset.sum_congr rfl fun r _ => ?_)
      congr 2 with a
      refine and_congr_right ?_
      simp +contextual

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

Goal state before:
pp: case pos
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hf : ∀ (a : α), f a ≤ 1
h'f : ∀ a ∈ sᶜ, f a = 0
x : α
hx : x ∈ s
⊢ f x ≤ s.indicator 1 x

pp: case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hf : ∀ (a : α), f a ≤ 1
h'f : ∀ a ∈ sᶜ, f a = 0
x : α
hx : x ∉ s
⊢ f x ≤ s.indicator 1 x

Tactic:
· simpa [hx] using hf x

Goal state after:
case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hf : ∀ (a : α), f a ≤ 1
h'f : ∀ a ∈ sᶜ, f a = 0
x : α
hx : x ∉ s
⊢ f x ≤ s.indicator 1 x
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
hf₀ : ¬∫⁻ (a : α), f a ∂μ = 0
⊢ ∃ g ≤ f, Measurable g ∧ μ (support g) < ∞ ∧ ∫⁻ (a : α), f a ∂μ - ε < ∫⁻ (a : α), g a ∂μ

Tactic:
by
    obtain ⟨g, hgf, hgε⟩ : ∃ (g : α →ₛ ℝ≥0∞) (_ : g ≤ f), ∫⁻ a, f a ∂μ - ε < g.lintegral μ := by
      simpa only [← lt_iSup_iff, ← lintegral_def] using ENNReal.sub_lt_self hf hf₀ hε
    refine ⟨g, hgf, g.measurable, ?_, by rwa [g.lintegral_eq_lintegral]⟩
    exact SimpleFunc.FinMeasSupp.of_lintegral_ne_top <| ne_top_of_le_ne_top hf <|
      g.lintegral_eq_lintegral μ ▸ lintegral_mono hgf

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
s : Set α
⊢ ∫⁻ (x : α) in {x | f x ≤ g x} ∩ s, g x ∂μ + ∫⁻ (x : α) in {x | g x < f x} ∩ s, f x ∂μ =
    ∫⁻ (x : α) in s ∩ {x | f x ≤ g x}, g x ∂μ + ∫⁻ (x : α) in s ∩ {x | g x < f x}, f x ∂μ

pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
s : Set α
⊢ MeasurableSet {x | g x < f x}

pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
s : Set α
⊢ MeasurableSet {x | f x ≤ g x}

Tactic:
inter_comm s,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
s : Set α
⊢ ∫⁻ (x : α) in {x | f x ≤ g x} ∩ s, g x ∂μ + ∫⁻ (x : α) in {x | g x < f x} ∩ s, f x ∂μ =
    ∫⁻ (x : α) in {x | f x ≤ g x} ∩ s, g x ∂μ + ∫⁻ (x : α) in s ∩ {x | g x < f x}, f x ∂μ

α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
s : Set α
⊢ MeasurableSet {x | g x < f x}

α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
s : Set α
⊢ MeasurableSet {x | f x ≤ g x}
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hg : AEMeasurable g μ
⊢ ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ

Tactic:
by
  simpa only [add_comm] using lintegral_add_left' hg f

Goal state after: