mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case refine_1
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
x : α
A : ℕ → Set α := natGeneratingSequence α
hA : ∀ (n : ℕ), MeasurableSet (A n)
hA_gen : generateFrom (range A) = mα
⊢ MeasurableSet (countablyGeneratedAtom α fun x_1 ↦ x ∈ A x_1)

pp: case refine_2
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
x : α
A : ℕ → Set α := natGeneratingSequence α
hA : ∀ (n : ℕ), MeasurableSet (A n)
hA_gen : generateFrom (range A) = mα
⊢ x ∈ countablyGeneratedAtom α fun x_1 ↦ x ∈ A x_1

pp: case refine_3
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
x : α
A : ℕ → Set α := natGeneratingSequence α
hA : ∀ (n : ℕ), MeasurableSet (A n)
hA_gen : generateFrom (range A) = mα
⊢ (countablyGeneratedAtom α fun x_1 ↦ x ∈ A x_1) ⊆ measurableAtom x

Tactic:
· exact measurableSet_countablyGeneratedAtom _

Goal state after:
case refine_2
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
x : α
A : ℕ → Set α := natGeneratingSequence α
hA : ∀ (n : ℕ), MeasurableSet (A n)
hA_gen : generateFrom (range A) = mα
⊢ x ∈ countablyGeneratedAtom α fun x_1 ↦ x ∈ A x_1

case refine_3
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
x : α
A : ℕ → Set α := natGeneratingSequence α
hA : ∀ (n : ℕ), MeasurableSet (A n)
hA_gen : generateFrom (range A) = mα
⊢ (countablyGeneratedAtom α fun x_1 ↦ x ∈ A x_1) ⊆ measurableAtom x
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

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

Tactic:
y

Goal state after:
α : Type u_1
S : Set (Set α)
h : SeparatesPoints α
this : MeasurableSpace α := generateFrom S
x y : α
⊢ (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : CountablyGenerated α
inst✝ : SeparatesPoints α
x : α
⊢ ∀ ⦃a₂ : α⦄, mapNatBool α x = mapNatBool α a₂ → x = a₂

Tactic:
y

Goal state after:
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : CountablyGenerated α
inst✝ : SeparatesPoints α
x y : α
⊢ mapNatBool α x = mapNatBool α y → x = y
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: case refine_3
ι : 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
i : ι
⊢ ∀ᵐ (x : α) ∂μ i, f x = g x

Tactic:
refine measure_mono_null (fun x (hx : f x ≠ g x) => ?_) (hsμ i)

Goal state after:
case refine_3
ι : 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
i : ι
x : α
hx : f x ≠ g x
⊢ x ∈ s i
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Preorder α
s : Set α
hsc : s.Countable
hst : ∀ (x : α), ∃ y ∈ s, x ≤ y
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
⊢ μ (⋃ i ∈ s, Iic i) = μ univ

Tactic:
congr

Goal state after:
case e_6
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Preorder α
s : Set α
hsc : s.Countable
hst : ∀ (x : α), ∃ y ∈ s, x ≤ y
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
⊢ ⋃ i ∈ s, Iic i = univ
Module: Mathlib.Topology.Separation.GDelta

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
inst✝ : T1Space X
x : X
⊢ IsGδ {x}

Tactic:
rcases (nhds_basis_opens x).exists_antitone_subbasis with ⟨U, hU, h_basis⟩
  rw [← biInter_basis_nhds h_basis.toHasBasis]
  exact .biInter (to_countable _) fun n _ => (hU n).2.isGδ

Goal state after:
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 α✝
α : Type u_6
inst✝ : TopologicalSpace α
p : α → Prop
hα : BorelSpace α
this✝ : MeasurableSpace α := ⋯
⊢ borel (Subtype p) = instMeasurableSpace

Tactic:
apply borel_comap

Goal state after:
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 δ
inst✝ : T0Space α
x : α
⊢ ∀ (y : α), (∀ (s : Set α), MeasurableSet s → (x ∈ s ↔ y ∈ s)) → x = y

Tactic:
y

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : OpensMeasurableSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : OpensMeasurableSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : TopologicalSpace γ₂
inst✝³ : MeasurableSpace γ₂
inst✝² : BorelSpace γ₂
inst✝¹ : MeasurableSpace δ
inst✝ : T0Space α
x y : α
⊢ (∀ (s : Set α), MeasurableSet s → (x ∈ s ↔ y ∈ s)) → x = y
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case refine_1
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ borel α ≤ MeasurableSpace.generateFrom (range Iio)

Tactic:
borel_eq_generateFrom_of_subbasis (@OrderTopology.topology_eq_generate_intervals α _ _ _)

Goal state after:
case refine_1
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ MeasurableSpace.generateFrom {s | ∃ a, s = Ioi a ∨ s = Iio a} ≤ MeasurableSpace.generateFrom (range Iio)
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x y : α
s : Set α
hy : y ∈ s
⊢ edist x y ≤ infEDist x s + ediam s

Tactic:
by
  simp_rw [infEDist, ENNReal.iInf_add]
  refine le_iInf₂ fun i hi => ?_
  calc
    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.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: case refine_1
α : Type u
inst✝ : PseudoEMetricSpace α
U : Set α
hU : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n ↦ (fun x ↦ infEDist x Uᶜ) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
x : α
hx : x ∈ U
this : ¬infEDist x Uᶜ = 0
⊢ x ∈ ⋃ n, F n

Tactic:
have B : 0 < infEDist x Uᶜ := by simpa [pos_iff_ne_zero] using this

Goal state after:
case refine_1
α : Type u
inst✝ : PseudoEMetricSpace α
U : Set α
hU : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n ↦ (fun x ↦ infEDist x Uᶜ) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
x : α
hx : x ∈ U
this : ¬infEDist x Uᶜ = 0
B : 0 < infEDist x Uᶜ
⊢ x ∈ ⋃ n, F n
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 : α → γ
s : Set α
hf : ContinuousOn f s
hs : sᶜ.Countable
⊢ Measurable (sᶜᶜ.domRestrict f)

Tactic:
rw [compl_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 : α → γ
s : Set α
hf : ContinuousOn f s
hs : sᶜ.Countable
⊢ Measurable (s.domRestrict f)
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
r : ℝ
hs : s.Nonempty
⊢ infDist x s < r ↔ ∃ y ∈ s, dist x y < r

Tactic:
simp [← not_le, le_infDist hs]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x y : α
hs : Bornology.IsBounded s
hy : y ∈ s
⊢ dist x y ≤ (infEDist x s).toReal + diam s

Tactic:
diam,

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x y : α
hs : Bornology.IsBounded s
hy : y ∈ s
⊢ dist x y ≤ (infEDist x s).toReal + (ediam s).toReal
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

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

Tactic:
rcases exists_countable_dense_bot_top α with ⟨s, hsc, hsd, hsb, _⟩

Goal state after:
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
inst✝ : NoMaxOrder α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) ≠ ∞
h : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) = ν (Ico a b)
s : Set α
hsc : s.Countable
hsd : Dense s
hsb : ∀ (x : α), IsBot x → x ∈ s
right✝ : ∀ (x : α), IsTop x → x ∈ s
⊢ μ = ν
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : MeasurableSpace α
inst✝⁶ : SemilatticeSup β
inst✝⁵ : OrderBot β
inst✝⁴ : Zero β
inst✝³ : TopologicalSpace β
inst✝² : OrderClosedTopology β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
i : ℕ → β
f : α → β
n : ℕ
a : α
hf : Measurable f
⊢ ((Finset.range n).sup fun c ↦ ((const α (i c)).restrict {a | i c ≤ f a}) a) =
    (Finset.range n).sup fun k ↦ if i k ≤ f a then i k else 0

Tactic:
congr

Goal state after:
case e_f
α : Type u_1
β : Type u_2
inst✝⁷ : MeasurableSpace α
inst✝⁶ : SemilatticeSup β
inst✝⁵ : OrderBot β
inst✝⁴ : Zero β
inst✝³ : TopologicalSpace β
inst✝² : OrderClosedTopology β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
i : ℕ → β
f : α → β
n : ℕ
a : α
hf : Measurable f
⊢ (fun c ↦ ((const α (i c)).restrict {a | i c ≤ f a}) a) = fun k ↦ if i k ≤ f a then i k else 0
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: case hnhds
α : Type u
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : PseudoEMetricSpace β
f : α → β
K : Set α
U : Set β
hK : IsCompact K
ho : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
hf : ∀ x ∈ K, ContinuousAt f x
hKU : MapsTo f K U
x : α
hx : x ∈ K
this✝ : {f x} ⊆ U
δ : ℝ
hδ : 0 < δ
hthick : thickening δ {f x} ⊆ U
V : Set α := f ⁻¹' thickening (δ / 2) {f x}
this : V ∈ 𝓝 x
⊢ thickening (δ / 2) (f '' V) ⊆ U

Tactic:
calc thickening (δ / 2) (f '' V)
      _ ⊆ thickening (δ / 2) (thickening (δ / 2) {f x}) :=
        thickening_subset_of_subset _ (image_preimage_subset f _)
      _ ⊆ thickening ((δ / 2) + (δ / 2)) ({f x}) :=
        thickening_thickening_subset (δ / 2) (δ / 2) {f x}
      _ ⊆ U := by simp [hthick]

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

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

Tactic:
Function.comp_apply,

Goal state after:
case succ
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
a : α
n : ℕ
IH : ∑ k ∈ Finset.range (n + 1), ↑((eapproxDiff f k) a) = (eapprox f n) a
⊢ (eapprox f n) a + ↑((eapprox f (n + 1) - eapprox f n) a).toNNReal = (eapprox f (n + 1)) a
Module: Mathlib.MeasureTheory.Function.SimpleFunc

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

Tactic:
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: 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
z : α
hz : z ∈ (fun x ↦ Ioo x (y x)) x
h'z : z ∈ (fun x ↦ Ioo x (y x)) x'
⊢ False

Tactic:
have : x ∈ interior s :=
        mem_interior.2 ⟨Ioo x' (y x'), h'y _ hx'.1, isOpen_Ioo, ⟨h', hz.1.trans h'z.2⟩⟩

Goal state after:
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
z : α
hz : z ∈ (fun x ↦ Ioo x (y x)) x
h'z : z ∈ (fun x ↦ Ioo x (y x)) x'
this : x ∈ interior s
⊢ False
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
a : α
hb : f a ∈ f.range
⊢ {b ∈ f.range | g b = g (f a)} = {j ∈ f.range | g j = g (f a)}

Tactic:
congr

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

Goal state before:
pp: f : ℕ → ℝ
k : ℕ
x : ℝ
h_tto : Tendsto f atTop (𝓝 x)
h_ant : AntitoneOn f (Ici k)
h_bdd : BddBelow (f '' Ici k)
⊢ IsGLB (f '' Ici k) x

Tactic:
rw [tendsto_nhds_unique h_tto
    (Real.tendsto_atTop_csInf_of_antitoneOn_bddBelow_nat_Ici h_ant h_bdd)]

Goal state after:
f : ℕ → ℝ
k : ℕ
x : ℝ
h_tto : Tendsto f atTop (𝓝 x)
h_ant : AntitoneOn f (Ici k)
h_bdd : BddBelow (f '' Ici k)
⊢ IsGLB (f '' Ici k) (sInf (f '' Ici k))
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0∞
g : α → ℝ≥0∞
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : ∀ (x : α), Tendsto (fun i ↦ f i x) u (𝓝 (g x))
x : ℕ → ι
hx : Tendsto x atTop u
y : α
⊢ liminf (fun n ↦ f (x n) y) atTop = g y

Tactic:
exact ((lim y).comp hx).liminf_eq

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

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
N : ℕ
x : α
⊢ (if x ∈ ⋂ k, ⋂ (_ : k ≤ N), {x | edist (e (N + 1)) x < edist (e k) x} then (const α (N + 1)) x
    else (nearestPtInd e N) x) =
    if ∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x then N + 1 else (nearestPtInd e N) x

Tactic:
congr

Goal state after:
case e_c
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
N : ℕ
x : α
⊢ (x ∈ ⋂ k, ⋂ (_ : k ≤ N), {x | edist (e (N + 1)) x < edist (e k) x}) = ∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x
Module: Mathlib.MeasureTheory.Function.SimpleFuncDense

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : PseudoEMetricSpace α
inst✝⁴ : OpensMeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : Zero α
inst✝¹ : Preorder α
f : β → α
hf : 0 ≤ f
hfm : Measurable f
inst✝ : SeparableSpace ↑(range f ∪ {0})
n : ℕ
⊢ 0 ≤ approxOn f hfm (range f ∪ {0}) 0 ⋯ n

Tactic:
by
  have : range f ∪ {0} ⊆ Set.Ici 0 := by
    simp only [Set.union_singleton, Set.insert_subset_iff, Set.mem_Ici, le_refl, true_and]
    rintro - ⟨x, rfl⟩
    exact hf x
  exact fun _ ↦ this <| approxOn_mem ..

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

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

Tactic:
congr

Goal state after:
case e_a
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A : μ s = μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' Ioi 0)
⊢ f ⁻¹' Ioi 0 = f ⁻¹' {∞} ∪ f ⁻¹' Ioo 0 ∞
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case e_a
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A : μ s = μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' Ioi 0)
x : α
⊢ x ∈ f ⁻¹' Ioi 0 ↔ x ∈ f ⁻¹' {∞} ∪ f ⁻¹' Ioo 0 ∞

Tactic:
simp only [mem_singleton_iff, mem_union, mem_Ioo, mem_Ioi, mem_preimage]

Goal state after:
case e_a
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A : μ s = μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' Ioi 0)
x : α
⊢ 0 < f x ↔ f x = ∞ ∨ 0 < f x ∧ f x < ∞
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : Preorder β
inst✝¹ : OrderClosedTopology β
inst✝ : PseudoMetrizableSpace β
f g : α → β
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
⊢ NullMeasurableSet {a | f a ≤ g a} μ

Tactic:
apply
    (hf.stronglyMeasurable_mk.measurableSet_le hg.stronglyMeasurable_mk).nullMeasurableSet.congr

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : Preorder β
inst✝¹ : OrderClosedTopology β
inst✝ : PseudoMetrizableSpace β
f g : α → β
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
⊢ {a | AEStronglyMeasurable.mk f hf a ≤ AEStronglyMeasurable.mk g hg a} =ᵐ[μ] {a | f a ≤ g a}
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
m₀ : MeasurableSpace α
μ : Measure α
inst✝¹ : PseudoMetrizableSpace β
inst✝ : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : IsEmbedding g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this✝³ : MeasurableSpace β := borel β
this✝² : BorelSpace β
this✝¹ : MeasurableSpace γ := borel γ
this✝ : BorelSpace γ
H : AEStronglyMeasurable (fun x ↦ g (f x)) μ
G : β → ↑(range g) := rangeFactorization g
⊢ IsClosed[instTopologicalSpaceSubtype] (range G)

Tactic:
by rw [rangeFactorization_surjective.range_eq]; exact isClosed_univ

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

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : ∀ (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
n : ℕ
a : α
h : a ∉ s
this : a ∉ {a | ¬∀ (i : ℕ), f i a ≤ f i.succ a}
⊢ f n a ≤ f (n + 1) a

Tactic:
simp only [not_forall, not_le, mem_ofPred_eq, not_exists, not_lt] at this

Goal state after:
case neg
α : 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
n : ℕ
a : α
h : a ∉ s
this : ∀ (x : ℕ), f x a ≤ f x.succ a
⊢ f n a ≤ f (n + 1) a
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun x1 x2 ↦ x1 ≤ x2) f
⊢ ∫⁻ (a : α), ⨆ b, f b a ∂μ = ⨆ b, ∫⁻ (a : α), f b a ∂μ

Tactic:
cases nonempty_encodable β
  cases isEmpty_or_nonempty β
  · simp
  inhabit β
  have : ∀ a, ⨆ b, f b a = ⨆ n, f (h_directed.sequence f n) a := by
    intro a
    refine le_antisymm (iSup_le fun b => ?_) (iSup_le fun n => le_iSup (fun n => f n a) _)
    exact le_iSup_of_le (encode b + 1) (h_directed.le_sequence b a)
  calc
    ∫⁻ 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.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : Function.support f ⊆ s
⊢ ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α), f x ∂μ

Tactic:
apply le_antisymm (setLIntegral_le_lintegral s fun x ↦ f x)
  apply le_trans (le_of_eq _) (lintegral_indicator_le _ _)
  congr with x
  simp only [indicator]
  split_ifs with h
  · rfl
  · exact Function.support_subset_iff'.1 hsf x h

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (a : α) ∂μ, Antitone fun i ↦ f i a
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' ↦ Antitone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i ↦ f i x
h_ae_seq_mono : Antitone (aeSeq h_meas p)
⊢ ⨅ n, ∫⁻ (a : α), aeSeq h_meas p n a ∂μ = ⨅ n, ∫⁻ (a : α), f n a ∂μ

Tactic:
congr

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (a : α) ∂μ, Antitone fun i ↦ f i a
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' ↦ Antitone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i ↦ f i x
h_ae_seq_mono : Antitone (aeSeq h_meas p)
⊢ (fun n ↦ ∫⁻ (a : α), aeSeq h_meas p n a ∂μ) = fun n ↦ ∫⁻ (a : α), f n a ∂μ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), ⨆ n, (eapprox f n) a ∂μ

Tactic:
congr

Goal state after:
case e_f
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
⊢ (fun a ↦ f a) = fun a ↦ ⨆ n, (eapprox f n) a
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
⊢ ⨆ n, ∫⁻ (a : α), (eapprox f n) a ∂μ = ⨆ n, (eapprox f n).lintegral μ

Tactic:
congr

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
⊢ (fun n ↦ ∫⁻ (a : α), (eapprox f n) a ∂μ) = fun n ↦ (eapprox f n).lintegral μ