mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: case inr
α : 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
X : ι → Type u_7
inst✝³ : Subsingleton ι
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : (i : ι) → MeasurableSpace (X i)
inst✝ : ∀ (i : ι), OpensMeasurableSpace (X i)
h : Nonempty ι
this : Unique ι
⊢ borel ((i : ι) → X i) ≤ MeasurableSpace.pi

Tactic:
rw [borel, MeasurableSpace.pi, ciSup_unique]

Goal state after:
case inr
α : 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
X : ι → Type u_7
inst✝³ : Subsingleton ι
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : (i : ι) → MeasurableSpace (X i)
inst✝ : ∀ (i : ι), OpensMeasurableSpace (X i)
h : Nonempty ι
this : Unique ι
⊢ MeasurableSpace.generateFrom {s | IsOpen[topologicalSpace] s} ≤
    MeasurableSpace.comap (fun b ↦ b default) (inst✝¹ default)
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:

Tactic:
edist x y ≤ edist x i + edist i y := edist_triangle _ _ _
    _ ≤ edist x i + Metric.ediam s := add_le_add le_rfl (Metric.edist_le_ediam_of_mem hi hy)

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

Goal state before:
pp: α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
⊢ borel α = MeasurableSpace.generateFrom {S | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}

Tactic:
by
  set S : Set (Set α) := { S | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S }
  refine le_antisymm ?_ (generateFrom_Icc_mem_le_borel _ _)
  let : MeasurableSpace α := generateFrom S
  rw [borel_eq_generateFrom_Iio]
  refine generateFrom_le (forall_mem_range.2 fun a => ?_)
  rcases hd.exists_countable_dense_subset_bot_top with ⟨t, hts, hc, htd, htb, -⟩
  by_cases! ha : ∀ b < a, (Ioo b a).Nonempty
  · convert_to MeasurableSet (⋃ (l ∈ t) (u ∈ t) (_ : l < u) (_ : u < a), Icc l u)
    · 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, hly, hyu.le⟩
      · rintro ⟨l, -, u, -, -, hua, -, hyu⟩
        exact hyu.trans_lt hua
    · refine MeasurableSet.biUnion hc fun a ha => MeasurableSet.biUnion hc fun b hb => ?_
      refine MeasurableSet.iUnion fun hab => MeasurableSet.iUnion fun _ => ?_
      exact .basic _ ⟨a, hts ha, b, hts hb, hab.le, mem_singleton _⟩
  · rcases ha with ⟨b, ba, hb⟩
    have hbs : b ∈ s := hIoo b a ba hb
    convert_to MeasurableSet (⋃ (l ∈ t) (_ : l ≤ b), Icc l b)
    · ext x
      simp only [mem_Iio, mem_iUnion, mem_Icc, exists_and_left, exists_prop]
      refine ⟨fun h ↦ ?_, fun ⟨y, yx, hy1, hy2, hy⟩ ↦ by order⟩
      have : x ≤ b := by
        contrapose! hb
        exact ⟨x, hb, h⟩
      rcases htd.exists_le' (fun b hb => htb _ hb (hbot b hb)) x with ⟨z, hzt, hzx⟩
      exact ⟨z, hzx, by order, hzt, by order⟩
    · refine .biUnion hc fun x hx => MeasurableSet.iUnion fun hlt => ?_
      exact .basic _ ⟨x, hts hx, b, hbs, hlt, mem_singleton _⟩

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 γ
f g : α → γ
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
hf : ContinuousOn f s
hg : ContinuousOn g sᶜ
hs : MeasurableSet s
⊢ Measurable (s.piecewise f g)

Tactic:
refine measurable_of_isOpen fun t ht => ?_

Goal state after:
α : Type u_1
γ : Type u_3
inst✝⁶ : TopologicalSpace α
inst✝⁵ : MeasurableSpace α
inst✝⁴ : OpensMeasurableSpace α
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
f g : α → γ
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
hf : ContinuousOn f s
hg : ContinuousOn g sᶜ
hs : MeasurableSet s
t : Set γ
ht : IsOpen[inst✝³] t
⊢ MeasurableSet (s.piecewise f g ⁻¹' t)
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ cthickening (max 0 δ) E = cthickening δ E

Tactic:
cases le_total δ 0 <;> simp [cthickening_of_nonpos, *]

Goal state after:
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 : γ
s : Finset γ
a✝ : a ∉ s
ih : (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✝¹

Tactic:
Finset.sup_insert,

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✝ : a ∉ s
ih : (s.sup f) a✝¹ = s.sup fun c ↦ (f c) a✝¹
⊢ (f a ⊔ s.sup f) a✝¹ = (insert a s).sup fun c ↦ (f c) a✝¹
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 : γ
s : Finset γ
a✝ : a ∉ s
ih : (s.sup f) a✝¹ = s.sup fun c ↦ (f c) a✝¹
⊢ (f a ⊔ s.sup f) a✝¹ = (insert a s).sup fun c ↦ (f c) a✝¹

Tactic:
Finset.sup_insert,

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✝ : a ∉ s
ih : (s.sup f) a✝¹ = s.sup fun c ↦ (f c) a✝¹
⊢ (f a ⊔ s.sup f) a✝¹ = (f a) a✝¹ ⊔ s.sup fun c ↦ (f c) a✝¹
Module: Mathlib.MeasureTheory.MeasurableSpace.Prod

Goal state before:
pp: case a.refine_1
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
⊢ MeasurableSpace.comap Prod.fst (generateFrom C) ≤ generateFrom (image2 (fun x1 x2 ↦ x1 ×ˢ x2) C D)

Tactic:
comap_generateFrom

Goal state after:
case a.refine_1
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
⊢ generateFrom (preimage Prod.fst '' C) ≤ generateFrom (image2 (fun x1 x2 ↦ x1 ×ˢ x2) C D)
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
⊢ MeasurableSpace.comap Prod.snd (generateFrom D) ≤ generateFrom (image2 (fun x1 x2 ↦ x1 ×ˢ x2) C D)

Tactic:
comap_generateFrom

Goal state after:
case a.refine_2
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
⊢ generateFrom (preimage Prod.snd '' D) ≤ generateFrom (image2 (fun x1 x2 ↦ x1 ×ˢ x2) C D)
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case neg
α : Type u_1
δ : Type u_4
inst✝⁵ : TopologicalSpace α
mα : MeasurableSpace α
inst✝⁴ : BorelSpace α
mδ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
inst✝ : Countable ι
f : ι → δ → α
g g' : δ → α
hf : ∀ (i : ι), Measurable (f i)
s : Set δ
hs : MeasurableSet s
hg : ∀ b ∈ s, IsLUB {a | ∃ i, f i b = a} (g b)
hg' : EqOn g g' sᶜ
g'_meas : Measurable g'
hι : IsEmpty ι
x : δ
hx : x ∈ s
A : ∀ b ∈ s, IsBot (g b)
B : ∀ b ∈ s, g b = g x
b : δ
hb : b ∉ s
⊢ g b = s.piecewise (fun _y ↦ g x) g' b

Tactic:
· simp [hb, hg' hb]

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

Goal state before:

Tactic:
thickening (ε₁ ⊓ ε₂) (f '' V₁) ∪ thickening (ε₁ ⊓ ε₂) (f '' V₂)
      _ ⊆ thickening ε₁ (f '' V₁) ∪ thickening ε₂ (f '' V₂) := by gcongr <;> norm_num
      _ ⊆ U ∪ U := by gcongr
      _ = U := union_self _

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
hf_meas : Measurable f
a : α
⊢ Tendsto (fun n ↦ (eapprox f n) a) atTop (𝓝 (f a))

Tactic:
nth_rw 2 [← iSup_coe_eapprox hf_meas]
  rw [iSup_apply]
  exact tendsto_atTop_iSup fun _ _ hnm ↦ monotone_eapprox f hnm a

Goal state after:
Module: Mathlib.Topology.Instances.Real.Lemmas

Goal state before:
pp: K : Subfield ℝ
hc : IsClosed ↑K
⊢ range Rat.cast ⊆ ↑K

Tactic:
rintro - ⟨_, rfl⟩

Goal state after:
K : Subfield ℝ
hc : IsClosed ↑K
w✝ : ℚ
⊢ ↑w✝ ∈ ↑K
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case pos
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_5
s : Set ι
f : ι → δ → α
hs : s.Countable
hf : ∀ i ∈ s, Measurable (f i)
this : Encodable ↑s
H : ∀ (i : ι), i ∈ s
⊢ Measurable fun b ↦ ⨆ i ∈ s, f i b

Tactic:
have : ∀ b, ⨆ i ∈ s, f i b = ⨆ (i : s), f i b :=
      fun b ↦ cbiSup_eq_of_forall (f := fun i ↦ f i b) H

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

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

Tactic:
rw [tendsto_nhds_unique h_tto (tendsto_atTop_ciSup h_mon h_bdd)]

Goal state after:
ι : Type u_1
inst✝² : Preorder ι
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x1 x2 ↦ x1 ≤ x2
f : ι → ℝ
x : ℝ
h_tto : Tendsto f atTop (𝓝 x)
h_mon : Monotone f
h_bdd : BddAbove (range f)
⊢ IsLUB (range f) (⨆ i, f i)
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Zero β
inst✝ : MeasurableSpace α
f : α →ₛ β
⊢ MeasurableSet (support ⇑f)

Tactic:
rw [f.support_eq]
  exact Finset.measurableSet_biUnion _ fun y _ => measurableSet_fiber _ _

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

Goal state before:
pp: case insert
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : AddZeroClass γ
motive : (α →ₛ γ) → Prop
const :
  ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), motive (piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ⇑f) (support ⇑g) → motive f → motive g → motive (f + g)
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ), range ⇑f \ {0} = ↑s → motive f
f : α →ₛ γ
h : range ⇑f \ {0} = ↑(insert x s)
mx : MeasurableSet (⇑f ⁻¹' {x})
⊢ motive f

Tactic:
let g := SimpleFunc.piecewise (f ⁻¹' {x}) mx 0 f

Goal state after:
case insert
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : AddZeroClass γ
motive : (α →ₛ γ) → Prop
const :
  ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), motive (piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ⇑f) (support ⇑g) → motive f → motive g → motive (f + g)
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ), range ⇑f \ {0} = ↑s → motive f
f : α →ₛ γ
h : range ⇑f \ {0} = ↑(insert x s)
mx : MeasurableSet (⇑f ⁻¹' {x})
g : α →ₛ γ := piecewise (⇑f ⁻¹' {x}) mx 0 f
⊢ motive f
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : AddZeroClass γ
motive : (α →ₛ γ) → Prop
const :
  ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), motive (piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ⇑f) (support ⇑g) → motive f → motive g → motive (f + g)
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ), range ⇑f \ {0} = ↑s → motive f
f : α →ₛ γ
h : range ⇑f \ {0} = ↑(insert x s)
mx : MeasurableSet (⇑f ⁻¹' {x})
g : α →ₛ γ := piecewise (⇑f ⁻¹' {x}) mx 0 f
⊢ ⇑0 '' ⇑f ⁻¹' {x} \ {0} ∪ (range ⇑f \ {x}) \ {0} = ↑s

Tactic:
sdiff_sdiff_comm,

Goal state after:
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : AddZeroClass γ
motive : (α →ₛ γ) → Prop
const :
  ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), motive (piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ⇑f) (support ⇑g) → motive f → motive g → motive (f + g)
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ), range ⇑f \ {0} = ↑s → motive f
f : α →ₛ γ
h : range ⇑f \ {0} = ↑(insert x s)
mx : MeasurableSet (⇑f ⁻¹' {x})
g : α →ₛ γ := piecewise (⇑f ⁻¹' {x}) mx 0 f
⊢ ⇑0 '' ⇑f ⁻¹' {x} \ {0} ∪ (range ⇑f \ {0}) \ {x} = ↑s
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: case refine_1
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0
hf : Measurable f
μ : Measure α
inst✝ : SigmaFinite μ
sigma_finite_sets : ℕ → Set α := spanningSets μ
norm_sets : ℕ → Set α := fun n ↦ {x | f x ≤ ↑n}
norm_sets_spanning : ⋃ n, norm_sets n = univ
sets : ℕ → Set α := fun n ↦ sigma_finite_sets n ∩ norm_sets n
n : ℕ
⊢ MeasurableSet (sigma_finite_sets n)

pp: case refine_2
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0
hf : Measurable f
μ : Measure α
inst✝ : SigmaFinite μ
sigma_finite_sets : ℕ → Set α := spanningSets μ
norm_sets : ℕ → Set α := fun n ↦ {x | f x ≤ ↑n}
norm_sets_spanning : ⋃ n, norm_sets n = univ
sets : ℕ → Set α := fun n ↦ sigma_finite_sets n ∩ norm_sets n
n : ℕ
⊢ MeasurableSet (norm_sets n)

Tactic:
· exact measurableSet_spanningSets μ n

Goal state after:
case refine_2
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0
hf : Measurable f
μ : Measure α
inst✝ : SigmaFinite μ
sigma_finite_sets : ℕ → Set α := spanningSets μ
norm_sets : ℕ → Set α := fun n ↦ {x | f x ≤ ↑n}
norm_sets_spanning : ⋃ n, norm_sets n = univ
sets : ℕ → Set α := fun n ↦ sigma_finite_sets n ∩ norm_sets n
n : ℕ
⊢ MeasurableSet (norm_sets n)
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : Nonempty γ
P : (α →ₛ γ) → Prop
const : ∀ (c : γ), P (SimpleFunc.const α c)
pcw : ∀ ⦃f g : α →ₛ γ⦄ {s : Set α} (hs : MeasurableSet s), P f → P g → P (piecewise s hs f g)
c : γ := Classical.ofNonempty
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ), range ⇑f \ {c} = ↑s → P f
f : α →ₛ γ
h : range ⇑f \ {c} = ↑(insert x s)
mx : MeasurableSet (⇑f ⁻¹' {x})
g : α →ₛ γ := piecewise (⇑f ⁻¹' {x}) mx (SimpleFunc.const α c) f
⊢ ⇑(SimpleFunc.const α c) '' ⇑f ⁻¹' {x} \ {c} ∪ (range ⇑f \ {x}) \ {c} = ↑s

Tactic:
sdiff_sdiff_comm,

Goal state after:
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : Nonempty γ
P : (α →ₛ γ) → Prop
const : ∀ (c : γ), P (SimpleFunc.const α c)
pcw : ∀ ⦃f g : α →ₛ γ⦄ {s : Set α} (hs : MeasurableSet s), P f → P g → P (piecewise s hs f g)
c : γ := Classical.ofNonempty
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ), range ⇑f \ {c} = ↑s → P f
f : α →ₛ γ
h : range ⇑f \ {c} = ↑(insert x s)
mx : MeasurableSet (⇑f ⁻¹' {x})
g : α →ₛ γ := piecewise (⇑f ⁻¹' {x}) mx (SimpleFunc.const α c) f
⊢ ⇑(SimpleFunc.const α c) '' ⇑f ⁻¹' {x} \ {c} ∪ (range ⇑f \ {c}) \ {x} = ↑s
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

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

Tactic:
exact hs.inter (hf measurableSet_Ioi)

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
⊢ ∫⁻ (x : α), c ∂μ = ∫⁻ (a : α), (const α c) a ∂μ

Tactic:
SimpleFunc.coe_const

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

Goal state before:
pp: case cons
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
M : Type u_5
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
f : α → M
l : List (α → M)
ihl : (∀ f ∈ l, AEStronglyMeasurable f μ) → AEStronglyMeasurable l.prod μ
hl : AEStronglyMeasurable f μ ∧ ∀ x ∈ l, AEStronglyMeasurable x μ
⊢ AEStronglyMeasurable (f :: l).prod μ

Tactic:
List.prod_cons

Goal state after:
case cons
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
M : Type u_5
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
f : α → M
l : List (α → M)
ihl : (∀ f ∈ l, AEStronglyMeasurable f μ) → AEStronglyMeasurable l.prod μ
hl : AEStronglyMeasurable f μ ∧ ∀ x ∈ l, AEStronglyMeasurable x μ
⊢ AEStronglyMeasurable (f * l.prod) μ
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : ℕ → Set α := spanningSets (μ.restrict t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := hf_meas.approx
fs : ℕ → α →ₛ β := fun n ↦ (f_approx n).restrict (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, (fs n) x = 0
⊢ ∀ (n : ℕ), μ (support ⇑(fs n)) < ∞

Tactic:
simp_rw [SimpleFunc.support_eq, ← Finset.mem_coe]

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : ℕ → Set α := spanningSets (μ.restrict t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := hf_meas.approx
fs : ℕ → α →ₛ β := fun n ↦ (f_approx n).restrict (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, (fs n) x = 0
⊢ ∀ (n : ℕ), μ (⋃ y ∈ ↑({y ∈ (fs n).range | y ≠ 0}), ⇑(fs n) ⁻¹' {y}) < ∞
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: α : Type u_1
m✝ : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n ↦ f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' ↦ Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i ↦ f i x
n m : ℕ
hnm : n ≤ m
x : α
⊢ aeSeq hf p n x ≤ aeSeq hf p m x

Tactic:
by_cases hx : x ∈ aeSeqSet hf p

Goal state after:
case pos
α : Type u_1
m✝ : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n ↦ f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' ↦ Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i ↦ f i x
n m : ℕ
hnm : n ≤ m
x : α
hx : x ∈ aeSeqSet hf p
⊢ aeSeq hf p n x ≤ aeSeq hf p m x

case neg
α : Type u_1
m✝ : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n ↦ f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' ↦ Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i ↦ f i x
n m : ℕ
hnm : n ≤ m
x : α
hx : x ∉ aeSeqSet hf p
⊢ aeSeq hf p n x ≤ aeSeq hf p m x
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ∫⁻ (x : α), f x ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
ε₂ : ℝ≥0∞
hε₂0 : 0 < ε₂
hε₂ε : ε₂ < ε
ε₁ : ℝ≥0∞
hε₁0 : 0 < ε₁
hε₁₂ : ε₁ < ε₂
φ : α →ₛ ℝ≥0
left✝ : ∀ (x : α), ↑(φ x) ≤ f x
hφ : ∀ (ψ : α →ₛ ℝ≥0), (∀ (x : α), ↑(ψ x) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε₁
⊢ ∃ δ > 0, ∀ (s : Set α), μ s < δ → ∫⁻ (x : α) in s, f x ∂μ < ε

Tactic:
rcases φ.exists_forall_le with ⟨C, hC⟩

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ∫⁻ (x : α), f x ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
ε₂ : ℝ≥0∞
hε₂0 : 0 < ε₂
hε₂ε : ε₂ < ε
ε₁ : ℝ≥0∞
hε₁0 : 0 < ε₁
hε₁₂ : ε₁ < ε₂
φ : α →ₛ ℝ≥0
left✝ : ∀ (x : α), ↑(φ x) ≤ f x
hφ : ∀ (ψ : α →ₛ ℝ≥0), (∀ (x : α), ↑(ψ x) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε₁
C : ℝ≥0
hC : ∀ (x : α), φ x ≤ C
⊢ ∃ δ > 0, ∀ (s : Set α), μ s < δ → ∫⁻ (x : α) in s, f x ∂μ < ε
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:

Tactic:
∫⁻ a, ⨆ b, f b a ∂μ = ∫⁻ a, ⨆ n, f (h_directed.sequence f n) a ∂μ := by simp only [this]
    _ = ⨆ n, ∫⁻ a, f (h_directed.sequence f n) a ∂μ :=
      (lintegral_iSup (fun n => hf _) h_directed.sequence_mono)
    _ = ⨆ b, ∫⁻ a, f b a ∂μ := by
      refine le_antisymm (iSup_le fun n => ?_) (iSup_le fun b => ?_)
      · exact le_iSup (fun b => ∫⁻ a, f b a ∂μ) _
      · exact le_iSup_of_le (encode b + 1) (lintegral_mono <| h_directed.le_sequence b)

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun x1 x2 ↦ x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' ↦ Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i ↦ f i x
b₁ b₂ z : β
hz₁ : f b₁ ≤ f z
hz₂ : f b₂ ≤ f z
x : α
⊢ aeSeq hf p b₁ x ≤ aeSeq hf p z x

Tactic:
by_cases hx : x ∈ aeSeqSet hf p

Goal state after:
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun x1 x2 ↦ x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' ↦ Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i ↦ f i x
b₁ b₂ z : β
hz₁ : f b₁ ≤ f z
hz₂ : f b₂ ≤ f z
x : α
hx : x ∈ aeSeqSet hf p
⊢ aeSeq hf p b₁ x ≤ aeSeq hf p z x

case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun x1 x2 ↦ x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' ↦ Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i ↦ f i x
b₁ b₂ z : β
hz₁ : f b₁ ≤ f z
hz₂ : f b₂ ≤ f z
x : α
hx : x ∉ aeSeqSet hf p
⊢ aeSeq hf p b₁ x ≤ aeSeq hf p z x
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun x1 x2 ↦ x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' ↦ Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i ↦ f i x
b₁ b₂ z : β
hz₁ : f b₁ ≤ f z
hz₂ : f b₂ ≤ f z
x : α
⊢ aeSeq hf p b₂ x ≤ aeSeq hf p z x

Tactic:
by_cases hx : x ∈ aeSeqSet hf p

Goal state after:
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun x1 x2 ↦ x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' ↦ Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i ↦ f i x
b₁ b₂ z : β
hz₁ : f b₁ ≤ f z
hz₂ : f b₂ ≤ f z
x : α
hx : x ∈ aeSeqSet hf p
⊢ aeSeq hf p b₂ x ≤ aeSeq hf p z x

case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun x1 x2 ↦ x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' ↦ Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i ↦ f i x
b₁ b₂ z : β
hz₁ : f b₁ ≤ f z
hz₂ : f b₂ ≤ f z
x : α
hx : x ∉ aeSeqSet hf p
⊢ aeSeq hf p b₂ x ≤ aeSeq hf p z x