mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Order.AtTopBotIxx

Goal state before:
pp: case inr
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
b : X
hsne : s.Nonempty
this : Nonempty ↑s
⊢ comap Subtype.val (𝓝[<] b) = atTop ↔ s ⊆ Iio b ∧ ∀ a < b, (s ∩ Ioo a b).Nonempty

Tactic:
by_cases hsub : s ⊆ Iio b

Goal state after:
case pos
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
⊢ comap Subtype.val (𝓝[<] b) = atTop ↔ s ⊆ Iio b ∧ ∀ a < b, (s ∩ Ioo a b).Nonempty

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
⊢ comap Subtype.val (𝓝[<] b) = atTop ↔ s ⊆ Iio b ∧ ∀ a < b, (s ∩ Ioo a b).Nonempty
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
s : Set β
f : β → Set α
hs : s.Countable
hd : s.Pairwise (AEDisjoint μ on f)
h : ∀ b ∈ s, NullMeasurableSet (f b) μ
this : Encodable ↑s
⊢ μ (⋃ x, f ↑x) = ∑' (p : ↑s), μ (f ↑p)

Tactic:
exact measure_iUnion₀ (hd.on_injective Subtype.coe_injective fun x => x.2) fun x => h x x.2

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

Goal state before:
pp: case inl
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
b : X
hsb : s ⊆ Iio b
hs : ∀ a' < b, ∃ a < b, Ioo a b ⊆ s
hb : IsSuccPrelimit b
hb' : Iio b = ∅
⊢ map Subtype.val atTop = 𝓝[<] b

Tactic:
have : IsEmpty s := ⟨fun x => hb'.subset (hsb x.2)⟩
    rw [filter_eq_bot_of_isEmpty atTop, Filter.map_bot, hb', nhdsWithin_empty]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSingletonClass α
s : Set α
hs : s.Infinite
h' : ∃ ε, ε ≠ 0 ∧ ∀ x ∈ s, ε ≤ μ {x}
ε : ℝ≥0∞
hne✝ : ε ≠ 0
hε : ∀ x ∈ s, ε ≤ μ {x}
this : Infinite ↑s
x y : ↑s
hne : x ≠ y
⊢ (Disjoint on fun x ↦ {↑x}) x y

Tactic:
simpa [Subtype.val_inj]

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : μ s ≠ ∞
ht : MeasurableSet t
hst : s ⊆ t
u : Set α
hu : MeasurableSet u
⊢ μ (toMeasurable μ s ∩ (t ∩ u)) = μ (u ∩ s)

Tactic:
measure_toMeasurable_inter (ht.inter hu) h

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : μ s ≠ ∞
ht : MeasurableSet t
hst : s ⊆ t
u : Set α
hu : MeasurableSet u
⊢ μ (s ∩ (t ∩ u)) = μ (u ∩ s)
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ✝ ν ν₁ ν₂ : Measure α
s t : Set α
inst✝¹ : Finite ι
μ : ι → Measure α
inst✝ : ∀ (i : ι), IsFiniteMeasure (μ i)
⊢ (sum μ) univ < ∞

Tactic:
cases nonempty_fintype ι

Goal state after:
case intro
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ✝ ν ν₁ ν₂ : Measure α
s t : Set α
inst✝¹ : Finite ι
μ : ι → Measure α
inst✝ : ∀ (i : ι), IsFiniteMeasure (μ i)
val✝ : Fintype ι
⊢ (sum μ) univ < ∞
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_8
ι : Type u_9
x✝¹ : MeasurableSpace α
μ : Measure α
inst✝¹ : SemilatticeSup ι
inst✝ : Countable ι
f : ι → Set α
hm : ∀ (i : ι), NullMeasurableSet (f i) μ
ε : ℝ≥0∞
hε : 0 < ε
hfin : ∃ i, μ (f i) ≠ ∞
hfem : ⋂ n, f n = ∅
F : ι → ℝ≥0∞ := fun m ↦ μ (⋂ n, ⋂ (_ : n ≤ m), f n)
hFAnti : Antitone F
this : Tendsto F atTop (𝓝 0)
x✝ : Nonempty ι := Exists.nonempty hfin
⊢ ∃ m, μ (⋂ n, ⋂ (_ : n ≤ m), f n) < ε

Tactic:
ENNReal.tendsto_atTop_zero_iff_lt_of_antitone hFAnti

Goal state after:
α : Type u_8
ι : Type u_9
x✝¹ : MeasurableSpace α
μ : Measure α
inst✝¹ : SemilatticeSup ι
inst✝ : Countable ι
f : ι → Set α
hm : ∀ (i : ι), NullMeasurableSet (f i) μ
ε : ℝ≥0∞
hε : 0 < ε
hfin : ∃ i, μ (f i) ≠ ∞
hfem : ⋂ n, f n = ∅
F : ι → ℝ≥0∞ := fun m ↦ μ (⋂ n, ⋂ (_ : n ≤ m), f n)
hFAnti : Antitone F
this : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, F n < ε
x✝ : Nonempty ι := Exists.nonempty hfin
⊢ ∃ m, μ (⋂ n, ⋂ (_ : n ≤ m), f n) < ε
Module: Mathlib.MeasureTheory.Measure.Restrict

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

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

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι✝ : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
μ✝ ν : Measure α
s t : Set α
a : α
ι : Type u_4
inst✝¹ : Finite ι
μ : ι → Measure α
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
⊢ SigmaFinite (sum μ)

Tactic:
cases nonempty_fintype ι

Goal state after:
case intro
α : Type u_1
β : Type u_2
ι✝ : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
μ✝ ν : Measure α
s t : Set α
a : α
ι : Type u_4
inst✝¹ : Finite ι
μ : ι → Measure α
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
val✝ : Fintype ι
⊢ SigmaFinite (sum μ)
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
ι : Type u_6
x✝ : MeasurableSpace α
μ : Measure α
s : ι → Set α
M : ℕ
hs_meas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (y : α), {i | y ∈ s i}.encard ≤ ↑M
t : Set α
ht : MeasurableSet t
F : Finset ι
P : Finset ι → Set α := fun C ↦ (⋂ i ∈ C, s i) ∩ ⋂ i ∈ F \ C, (s i)ᶜ
Cs : Finset (Finset ι) := F.powerset \ {∅}
G : ι → Set (Finset ι) := fun i ↦ {C | C ∈ F.powerset ∧ i ∈ C}
P_meas : ∀ (C : Finset ι), MeasurableSet (P C)
i : ι
hi : i ∈ F
⊢ s i ⊆ ⋃ C ∈ G i, P C

Tactic:
refine fun x hx ↦ Set.mem_biUnion (x := F.filter (x ∈ s ·)) ?_ ?_

Goal state after:
case refine_1
α : Type u_2
ι : Type u_6
x✝ : MeasurableSpace α
μ : Measure α
s : ι → Set α
M : ℕ
hs_meas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (y : α), {i | y ∈ s i}.encard ≤ ↑M
t : Set α
ht : MeasurableSet t
F : Finset ι
P : Finset ι → Set α := fun C ↦ (⋂ i ∈ C, s i) ∩ ⋂ i ∈ F \ C, (s i)ᶜ
Cs : Finset (Finset ι) := F.powerset \ {∅}
G : ι → Set (Finset ι) := fun i ↦ {C | C ∈ F.powerset ∧ i ∈ C}
P_meas : ∀ (C : Finset ι), MeasurableSet (P C)
i : ι
hi : i ∈ F
x : α
hx : x ∈ s i
⊢ {x_1 ∈ F | x ∈ s x_1} ∈ G i

case refine_2
α : Type u_2
ι : Type u_6
x✝ : MeasurableSpace α
μ : Measure α
s : ι → Set α
M : ℕ
hs_meas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (y : α), {i | y ∈ s i}.encard ≤ ↑M
t : Set α
ht : MeasurableSet t
F : Finset ι
P : Finset ι → Set α := fun C ↦ (⋂ i ∈ C, s i) ∩ ⋂ i ∈ F \ C, (s i)ᶜ
Cs : Finset (Finset ι) := F.powerset \ {∅}
G : ι → Set (Finset ι) := fun i ↦ {C | C ∈ F.powerset ∧ i ∈ C}
P_meas : ∀ (C : Finset ι), MeasurableSet (P C)
i : ι
hi : i ∈ F
x : α
hx : x ∈ s i
⊢ x ∈ P ({x_1 ∈ F | x ∈ s x_1})
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : CountablyGenerated α
inst✝ : SeparatesPoints α
⊢ Injective (mapNatBool α)

Tactic:
by
  intro x y hxy
  rw [← generateFrom_natGeneratingSequence α] at *
  apply separating_of_generateFrom (range (natGeneratingSequence _))
  rintro - ⟨n, rfl⟩
  rw [← decide_eq_decide]
  exact congr_fun hxy n

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

Goal state before:
pp: case refine_2
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
x✝ : ∃ S, ↑S ⊆ memPartition t n ∧ s = ⋃₀ ↑S
S : Finset (Set α)
hS_subset : ↑S ⊆ memPartition t n
hS_eq : s = ⋃₀ ↑S
⊢ MeasurableSet (⋃₀ ↑S)

Tactic:
sUnion_eq_biUnion

Goal state after:
case refine_2
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
x✝ : ∃ S, ↑S ⊆ memPartition t n ∧ s = ⋃₀ ↑S
S : Finset (Set α)
hS_subset : ↑S ⊆ memPartition t n
hS_eq : s = ⋃₀ ↑S
⊢ MeasurableSet (⋃ i ∈ ↑S, i)
Module: Mathlib.Topology.Separation.GDelta

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
inst✝ : T1Space X
x : X
U : ℕ → Set X
hU : ∀ (i : ℕ), x ∈ U i ∧ IsOpen[inst✝²] (U i)
h_basis : (𝓝 x).HasAntitoneBasis fun i ↦ U i
⊢ IsGδ {x}

Tactic:
rw [← biInter_basis_nhds h_basis.toHasBasis]

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
inst✝ : T1Space X
x : X
U : ℕ → Set X
hU : ∀ (i : ℕ), x ∈ U i ∧ IsOpen[inst✝²] (U i)
h_basis : (𝓝 x).HasAntitoneBasis fun i ↦ U i
⊢ IsGδ (⋂ i, ⋂ (_ : True), U i)
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: case refine_2
α : 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
m n : ℕ
hmn : m ≤ n
x : α
hx : a ^ m ≤ infEDist x Uᶜ
⊢ a ^ n ≤ infEDist x Uᶜ

Tactic:
apply le_trans (pow_le_pow_right_of_le_one' a_lt_one.le hmn) hx

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

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

Tactic:
simp only [mem_iUnion₂, exists_prop]

Goal state after:
X : Type u
inst✝ : PseudoMetricSpace X
δ : ℝ
E : Set X
x : X
⊢ x ∈ thickening δ E ↔ ∃ i ∈ E, x ∈ ball i δ
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
δ : ℝ
hδ : 0 ≤ δ
⊢ cthickening δ {x} = closedBall x δ

Tactic:
by
  ext y
  simp [cthickening, edist_dist, ENNReal.ofReal_le_ofReal_iff hδ]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
r : ℝ
hs : s.Nonempty
⊢ r ≤ infDist x s ↔ ∀ ⦃y : α⦄, y ∈ s → r ≤ dist x y

Tactic:
simp_rw [infDist, ← ENNReal.ofReal_le_iff_le_toReal (infEDist_ne_top hs), le_infEDist,
    ENNReal.ofReal_le_iff_le_toReal (edist_ne_top _ _), ← dist_edist]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ cthickening (max 0 δ) E = ⋂ ε, ⋂ (_ : max 0 δ < ε), thickening ε E

Tactic:
cthickening_eq_iInter_thickening

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ ⋂ ε, ⋂ (_ : max 0 δ < ε), thickening ε E = ⋂ ε, ⋂ (_ : max 0 δ < ε), thickening ε E

case δ_nn
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ 0 ≤ max 0 δ
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: case inr.inl
α : Type u
inst✝ : PseudoEMetricSpace α
ε δ : ℝ
s : Set α
hε : 0 ≤ ε
hδ : δ ≤ 0
⊢ thickening ε (thickening δ s) ⊆ thickening (ε + δ) s

pp: case inr.inr
α : Type u
inst✝ : PseudoEMetricSpace α
ε δ : ℝ
s : Set α
hε : 0 ≤ ε
hδ : 0 ≤ δ
⊢ thickening ε (thickening δ s) ⊆ thickening (ε + δ) s

Tactic:
· simp only [thickening_of_nonpos hδ, thickening_empty, empty_subset]

Goal state after:
case inr.inr
α : Type u
inst✝ : PseudoEMetricSpace α
ε δ : ℝ
s : Set α
hε : 0 ≤ ε
hδ : 0 ≤ δ
⊢ thickening ε (thickening δ s) ⊆ thickening (ε + δ) s
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Zero β
f : α →ₛ β
s : Set α
hs : MeasurableSet s
⊢ ⇑(f.restrict s) = s.indicator ⇑f

Tactic:
by
  classical
  rw [restrict, dif_pos hs, coe_piecewise, coe_zero, piecewise_eq_indicator]

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

Goal state before:
pp: X : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : NullSingletonClass μ
E : Set X
inst✝ : SeparableSpace ↑E
hE : 0 < μ E
h : ∀ (x : X), ¬AccPt x (𝓟 E)
⊢ False

Tactic:
have : DiscreteTopology E := discreteTopology_of_noAccPts fun x _ => h x

Goal state after:
X : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : NullSingletonClass μ
E : Set X
inst✝ : SeparableSpace ↑E
hE : 0 < μ E
h : ∀ (x : X), ¬AccPt x (𝓟 E)
this : DiscreteTopology ↑E
⊢ False
Module: Mathlib.MeasureTheory.Function.SimpleFunc

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

Tactic:
simp [eapproxDiff, (eapprox_lt_top f 0 a).ne]

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
M : α → α
hM : ∀ x ∈ s, x < M x
H : (s \ interior s).Countable
⊢ s = interior s ∪ s \ interior s

Tactic:
union_sdiff_cancel interior_subset

Goal state after:
α : 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
H : (s \ interior s).Countable
⊢ s = s
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α →ₛ ℝ≥0∞
⊢ ∑ x ∈ (f.pair g).range, (x.1 * μ (⇑(f.pair g) ⁻¹' {x}) + x.2 * μ (⇑(f.pair g) ⁻¹' {x})) =
    ∑ x ∈ (f.pair g).range, x.1 * μ (⇑(f.pair g) ⁻¹' {x}) + ∑ x ∈ (f.pair g).range, x.2 * μ (⇑(f.pair g) ⁻¹' {x})

Tactic:
Finset.sum_add_distrib

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α →ₛ ℝ≥0∞
⊢ ∑ x ∈ (f.pair g).range, x.1 * μ (⇑(f.pair g) ⁻¹' {x}) + ∑ x ∈ (f.pair g).range, x.2 * μ (⇑(f.pair g) ⁻¹' {x}) =
    ∑ x ∈ (f.pair g).range, x.1 * μ (⇑(f.pair g) ⁻¹' {x}) + ∑ x ∈ (f.pair g).range, x.2 * μ (⇑(f.pair g) ⁻¹' {x})
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: case refine_4
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α✝
mα✝ : MeasurableSpace α✝
α : Type u_5
β : Type u_6
γ : Type u_7
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
⊢ Measurable fun r ↦ (↑r, ⊥).1 * (↑r, ⊥).2

Tactic:
simp_rw [mul_comm _ ⊥]
    exact (measurable_const_mul _).comp measurable_coe_real_ereal

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

Goal state before:
pp: α : Type u_3
inst✝² : MeasurableSpace α
A : Set α
ι : Type u_4
L : Filter ι
inst✝¹ : L.IsCountablyGenerated
As : ι → Set α
inst✝ : L.NeBot
h_lim : ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
As_mble : ∀ (i : ι), Measurable ((As i).indicator fun x ↦ 1)
⊢ Measurable (A.indicator fun x ↦ 1)

Tactic:
exact ENNReal.measurable_of_tendsto' L As_mble
    ((tendsto_indicator_const_iff_forall_eventually L (1 : ℝ≥0∞)).mpr h_lim)

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

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

Tactic:
by
  simp only [nearestPtInd, coe_piecewise, Set.piecewise]
  congr
  simp

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
motive : (α → ℝ≥0∞) → Prop
indicator : ∀ (c : ℝ≥0∞) ⦃s : Set α⦄, MeasurableSet s → μ s < ∞ → motive (s.indicator fun x ↦ c)
add :
  ∀ ⦃f g : α → ℝ≥0∞⦄,
    Disjoint (support f) (support g) → Measurable f → Measurable g → motive f → motive g → motive (f + g)
iSup :
  ∀ ⦃f : ℕ → α → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f n)) → Monotone f → (∀ (n : ℕ), motive (f n)) → motive fun x ↦ ⨆ n, f n x
f : α → ℝ≥0∞
hf : Measurable f
c : ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ motive (s.indicator fun x ↦ c)

Tactic:
convert!
    iSup (f := fun n ↦ (s ∩ spanningSets μ n).indicator fun _ ↦ c)
      (fun n ↦ measurable_const.indicator (hs.inter (measurableSet_spanningSets ..)))
      (fun m n hmn a ↦ by dsimp; grw [hmn])
      (fun n ↦
        indicator _ (hs.inter (measurableSet_spanningSets ..))
          (measure_inter_lt_top_of_right_ne_top (measure_spanningSets_lt_top ..).ne)) with
    a

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
motive : (α → ℝ≥0∞) → Prop
indicator : ∀ (c : ℝ≥0∞) ⦃s : Set α⦄, MeasurableSet s → μ s < ∞ → motive (s.indicator fun x ↦ c)
add :
  ∀ ⦃f g : α → ℝ≥0∞⦄,
    Disjoint (support f) (support g) → Measurable f → Measurable g → motive f → motive g → motive (f + g)
iSup :
  ∀ ⦃f : ℕ → α → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f n)) → Monotone f → (∀ (n : ℕ), motive (f n)) → motive fun x ↦ ⨆ n, f n x
f : α → ℝ≥0∞
hf : Measurable f
c : ℝ≥0∞
s : Set α
hs : MeasurableSet s
a : α
⊢ s.indicator (fun x ↦ c) a = ⨆ n, (s ∩ spanningSets μ n).indicator (fun x ↦ c) a
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
⊢ AEStronglyMeasurable f μ ↔ AEMeasurable f μ ∧ ∃ t, IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, f x ∈ t

Tactic:
refine ⟨fun H => ⟨H.aemeasurable, H.isSeparable_ae_range⟩, ?_⟩
  rintro ⟨H, ⟨t, t_sep, ht⟩⟩
  rcases eq_empty_or_nonempty t with (rfl | h₀)
  · simp only [mem_empty_iff_false, eventually_false_iff_eq_bot, ae_eq_bot] at ht
    rw [ht]
    exact aestronglyMeasurable_zero_measure f
  · obtain ⟨g, g_meas, gt, fg⟩ : ∃ g : α → β, Measurable g ∧ range g ⊆ t ∧ f =ᵐ[μ] g :=
      H.exists_ae_eq_range_subset ht h₀
    refine ⟨g, ?_, fg⟩
    exact stronglyMeasurable_iff_measurable_separable.2 ⟨g_meas, t_sep.mono gt⟩

Goal state after:
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝² : Countable ι
inst✝¹ : TopologicalSpace β
f : α → β
inst✝ : PseudoMetrizableSpace β
m : MeasurableSpace α
μ : ι → Measure α
h : ∀ (i : ι), AEStronglyMeasurable f (μ i)
⊢ AEStronglyMeasurable f (sum μ)

Tactic:
borelize β
  refine
    aestronglyMeasurable_iff_aemeasurable_separable.2
      ⟨AEMeasurable.sum_measure fun i => (h i).aemeasurable, ?_⟩
  have A : ∀ i : ι, ∃ t : Set β, IsSeparable t ∧ f ⁻¹' t ∈ ae (μ i) := fun i =>
    (aestronglyMeasurable_iff_aemeasurable_separable.1 (h i)).2
  choose t t_sep ht using A
  refine ⟨⋃ i, t i, .iUnion t_sep, ?_⟩
  simp only [Measure.ae_sum_eq, mem_iUnion, eventually_iSup]
  intro i
  filter_upwards [ht i] with x hx
  exact ⟨i, hx⟩

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
⊢ 0 < (μ.restrict s) (Function.support f) ↔ 0 < μ (Function.support f ∩ s)

Tactic:
Measure.restrict_apply (measurableSet_support hf)

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
⊢ 0 < μ (Function.support f ∩ s) ↔ 0 < μ (Function.support f ∩ s)
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hle : f ≤ᵐ[μ] g
hg : AEMeasurable g μ
ε : ℝ≥0∞
φ : α → ℝ≥0∞
hφm : Measurable φ
hφ_le : φ ≤ f
hφ_eq : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), φ a ∂μ
⊢ ∫⁻ (x : α), f x ∂μ + ε * μ {x | f x + ε ≤ g x} = ∫⁻ (x : α), φ x ∂μ + ε * μ {x | f x + ε ≤ g x}

Tactic:
by
      rw [hφ_eq]

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

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : Function.support f ⊆ s
x : α
h : x ∉ s
⊢ f x = 0

Tactic:
· exact Function.support_subset_iff'.1 hsf x h

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
r : ℝ≥0∞
this : ∀ x ∈ {x | f x = r}, f x = r
⊢ ∫⁻ (x : α) in {x | f x = r}, r ∂μ = r * μ {x | f x = r}

Tactic:
rw [lintegral_const, Measure.restrict_apply MeasurableSet.univ, Set.univ_inter]

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

Goal state before:
pp: case e_f
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
a : α
⊢ ⨆ a_1, (eapprox f a_1) a + (eapprox g a_1) a = ⨆ n, (⇑(eapprox f n) + ⇑(eapprox g n)) a

pp: case e_f.hf
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
a : α
⊢ Monotone fun n ↦ (eapprox f n) a

pp: case e_f.hg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
a : α
⊢ Monotone fun n ↦ (eapprox g n) a

Tactic:
· simp only [Pi.add_apply]

Goal state after:
case e_f.hf
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
a : α
⊢ Monotone fun n ↦ (eapprox f n) a

case e_f.hg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
a : α
⊢ Monotone fun n ↦ (eapprox g n) a
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

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

Tactic:
← SimpleFunc.lintegral_eq_lintegral

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
n : ℕ
⊢ ∫⁻ (a : α), (⇑(eapprox f n) + ⇑(eapprox g n)) a ∂μ = ∫⁻ (a : α), (eapprox f n + eapprox g n) a ∂μ
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : SecondCountableTopology β
inst✝ : OpensMeasurableSpace β
hf : Measurable f
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
a✝ : Nontrivial β
inhabited_h : Inhabited β
⊢ StronglyMeasurable f

Tactic:
exact ⟨SimpleFunc.approxOn f hf Set.univ default (Set.mem_univ _), fun x ↦
    SimpleFunc.tendsto_approxOn hf (Set.mem_univ _) (by simp)⟩

Goal state after:
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
⊢ ∃ s, MeasurableSet s ∧ μ s < ∞ ∧ ∫⁻ (a : α) in sᶜ, f a ∂μ < ε

Tactic:
by_cases hf₀ : ∫⁻ a, f a ∂μ = 0
  · exact ⟨∅, .empty, by simp, by simpa [hf₀, pos_iff_ne_zero]⟩
  obtain ⟨g, hgf, hg_meas, hgsupp, hgε⟩ :
      ∃ g ≤ f, Measurable g ∧ μ (support g) < ∞ ∧ ∫⁻ a, f a ∂μ - ε < ∫⁻ a, g a ∂μ := 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
  refine ⟨_, measurableSet_support hg_meas, hgsupp, ?_⟩
  calc
    ∫⁻ a in (support g)ᶜ, f a ∂μ
      = ∫⁻ a in (support g)ᶜ, f a - g a ∂μ := setLIntegral_congr_fun
      (measurableSet_support hg_meas).compl <| by intro; simp_all
    _ ≤ ∫⁻ a, f a - g a ∂μ := setLIntegral_le_lintegral _ _
    _ = ∫⁻ a, f a ∂μ - ∫⁻ a, g a ∂μ :=
      lintegral_sub hg_meas (ne_top_of_le_ne_top hf <| lintegral_mono hgf) (ae_of_all _ hgf)
    _ < ε := ENNReal.sub_lt_of_lt_add (lintegral_mono hgf) <|
      ENNReal.lt_add_of_sub_lt_left (.inl hf) hgε

Goal state after: