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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : μ.restrict s = ν.restrict s
ht : μ.restrict t = ν.restrict t
u : Set α
hu : MeasurableSet u
US : Set α
hsub : u ∩ s ⊆ US
hm : MeasurableSet US
hμ : μ US = μ (u ∩ s)
hν : ν US = ν (u ∩ s)
⊢ μ (u ∩ s ∪ u ∩ t) = ν (u ∩ s ∪ u ∩ t)

Tactic:
calc
    μ (u ∩ s ∪ u ∩ t) = μ (US ∪ u ∩ t) :=
      measure_union_congr_of_subset hsub hμ.le Subset.rfl le_rfl
    _ = μ US + μ ((u ∩ t) \ US) := (measure_add_sdiff hm.nullMeasurableSet _).symm
    _ = restrict μ s u + restrict μ t (u \ US) := by
      simp only [restrict_apply, hu, hu.diff hm, hμ, ← inter_comm t, inter_sdiff_assoc]
    _ = restrict ν s u + restrict ν t (u \ US) := by rw [hs, ht]
    _ = ν US + ν ((u ∩ t) \ US) := by
      simp only [restrict_apply, hu, hu.diff hm, hν, ← inter_comm t, inter_sdiff_assoc]
    _ = ν (US ∪ u ∩ t) := measure_add_sdiff hm.nullMeasurableSet _
    _ = ν (u ∩ s ∪ u ∩ t) := .symm <| measure_union_congr_of_subset hsub hν.le Subset.rfl le_rfl

Goal state after:
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✝ : TopologicalSpace α
μ : Measure α
hμ : IsLocallyFiniteMeasure μ
x : α
⊢ (μ.restrict s).FiniteAtFilter (𝓝 x)

Tactic:
obtain ⟨t, ht, hmus⟩ := hμ.finiteAtNhds x
    exact ⟨t, ht, lt_of_le_of_lt (restrict_apply_le s t) hmus⟩

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

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
h : IsCompact s
hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝 x)
⊢ ∃ U ⊇ s, IsOpen[inst✝¹] U ∧ μ U < ∞

Tactic:
by
  refine IsCompact.induction_on h ?_ ?_ ?_ ?_
  · use ∅
    simp
  · rintro s t hst ⟨U, htU, hUo, hU⟩
    exact ⟨U, hst.trans htU, hUo, hU⟩
  · rintro s t ⟨U, hsU, hUo, hU⟩ ⟨V, htV, hVo, hV⟩
    refine
      ⟨U ∪ V, union_subset_union hsU htV, hUo.union hVo,
        (measure_union_le _ _).trans_lt <| ENNReal.add_lt_top.2 ⟨hU, hV⟩⟩
  · intro x hx
    rcases (hμ x hx).exists_mem_basis (nhds_basis_opens _) with ⟨U, ⟨hx, hUo⟩, hU⟩
    exact ⟨U, nhdsWithin_le_nhds (hUo.mem_nhds hx), U, Subset.rfl, hUo, hU⟩

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

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_8
inst✝³ : LinearOrder ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
s : ι → Set α
a : ι
hs : ∀ r > a, NullMeasurableSet (s r) μ
hm : ∀ (i j : ι), a < i → i ≤ j → s i ⊆ s j
hf : ∃ r > a, μ (s r) ≠ ∞
ha : ¬Order.IsPredPrelimit a
⊢ Tendsto (⇑μ ∘ s) (𝓝[>] a) (𝓝 (μ (⋂ r, ⋂ (_ : r > a), s r)))

Tactic:
rw [Order.not_isPredPrelimit_iff] at ha

Goal state after:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_8
inst✝³ : LinearOrder ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
s : ι → Set α
a : ι
hs : ∀ r > a, NullMeasurableSet (s r) μ
hm : ∀ (i j : ι), a < i → i ≤ j → s i ⊆ s j
hf : ∃ r > a, μ (s r) ≠ ∞
ha : ∃ b, a ⋖ b
⊢ Tendsto (⇑μ ∘ s) (𝓝[>] a) (𝓝 (μ (⋂ r, ⋂ (_ : r > a), s r)))
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁✝ μ₂✝ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
x✝ : MeasurableSpace α
μ₁ μ₂ : Measure α
s : ℕ → Set α
hs : ∀ (i : ℕ), MeasurableSet (s i)
hd : Pairwise (Disjoint on s)
⊢ ∑' (i : ℕ), μ₁ (s i) + μ₂ (⋃ i, s i) = ∑' (a : ℕ), μ₁ (s a) + ∑' (a : ℕ), μ₂ (s a)

Tactic:
measure_iUnion hd hs

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁✝ μ₂✝ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
x✝ : MeasurableSpace α
μ₁ μ₂ : Measure α
s : ℕ → Set α
hs : ∀ (i : ℕ), MeasurableSet (s i)
hd : Pairwise (Disjoint on s)
⊢ ∑' (i : ℕ), μ₁ (s i) + ∑' (i : ℕ), μ₂ (s i) = ∑' (a : ℕ), μ₁ (s a) + ∑' (a : ℕ), μ₂ (s a)
Module: Mathlib.Data.Set.MemPartition

Goal state before:
pp: α : Type u_1
f : ℕ → Set α
n : ℕ
⊢ (memPartition f n).Finite

Tactic:
induction n with
  | zero => simp
  | succ n ih =>
    rw [memPartition_succ]
    have : Finite (memPartition f n) := Set.finite_coe_iff.mp ih
    rw [← Set.finite_coe_iff]
    simp_rw [ofPred_exists, ← exists_prop, ofPred_exists, ofPred_or]
    refine Finite.Set.finite_biUnion (memPartition f n) _ (fun u _ ↦ ?_)
    rw [Set.finite_coe_iff]
    simp

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

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
e : α ≃ᵐ β
μ : Measure β
s : Set α
⊢ (Measure.comap (⇑e) μ) s = μ (⇑e.symm ⁻¹' s)

Tactic:
by
  rw [e.measurableEmbedding.comap_apply, e.image_eq_preimage_symm]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : CountablyGenerated α
n : ℕ
⊢ MeasurableSet ((fun x ↦ mapNatBool α x n) ⁻¹' {true})

Tactic:
simp only [preimage, mem_singleton_iff, mapNatBool,
    Bool.decide_iff, ofPred_mem_eq]

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : CountablyGenerated α
n : ℕ
⊢ MeasurableSet (natGeneratingSequence α n)
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : CountablySeparated α
⊢ MeasurableSingletonClass α

Tactic:
rcases measurable_injection_nat_bool_of_countablySeparated α with ⟨f, fmeas, finj⟩
  refine ⟨fun x ↦ ?_⟩
  rw [← finj.preimage_image {x}, image_singleton]
  exact fmeas <| MeasurableSet.singleton _

Goal state after:
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
t : Set β
ht : MeasurableSet t
⊢ Subtype.val ⁻¹' ⋃ i, mk f ⋯ ⁻¹' t ∩ (s i)ᶜ = (⋃ i, (s i)ᶜ).domRestrict f ⁻¹' t

Tactic:
ext ⟨x, hx⟩

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
t : Set β
ht : MeasurableSet t
x : α
hx : x ∈ ⋃ i, (s i)ᶜ
⊢ ⟨x, hx⟩ ∈ Subtype.val ⁻¹' ⋃ i, mk f ⋯ ⁻¹' t ∩ (s i)ᶜ ↔ ⟨x, hx⟩ ∈ (⋃ i, (s i)ᶜ).domRestrict f ⁻¹' t
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
m : MeasurableSpace α✝
h : CountablyGenerated α✝
α : Type u_3
γ : Type u_4
inst✝ : MeasurableSpace γ
hα : CountableOrCountablyGenerated α γ
hβ : CountableOrCountablyGenerated β γ
⊢ CountableOrCountablyGenerated (α × β) γ

Tactic:
by
  rcases hα with (hα | hα) <;> rcases hβ with (hβ | hβ) <;> infer_instance

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

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
μ ν : Measure α
f : α → β
hμ : AEMeasurable f μ
hν : AEMeasurable f ν
⊢ Measure.map f (μ + ν) = Measure.map f μ + Measure.map f ν

Tactic:
by
  ext
  simp [*]

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

Goal state before:
pp: M : Type u_2
α : Type u_4
inst✝² : CommMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
s : Multiset (α → M)
hs : ∀ f ∈ s, Measurable f
⊢ Measurable fun x ↦ (map (fun f ↦ f x) s).prod

Tactic:
by
  simpa only [← Pi.multiset_prod_apply] using s.measurable_prod hs

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

Goal state before:
pp: α : Type u_2
inst✝ : PseudoMetricSpace α
x y : α
δ : ℝ
E : Set α
h : y ∈ E
h' : dist x y ≤ δ
⊢ x ∈ cthickening δ E

Tactic:
by
  apply mem_cthickening_of_edist_le x y δ E h
  rw [edist_dist]
  exact ENNReal.ofReal_le_ofReal h'

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E ⊆ cthickening δ E

Tactic:
← cthickening_of_nonpos (min_le_right δ 0)

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ cthickening (min δ 0) E ⊆ cthickening δ E
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 | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ioc l u = S} =
    {S | ∃ l ∈ ⇑OrderDual.ofDual ⁻¹' s, ∃ u ∈ ⇑OrderDual.ofDual ⁻¹' s, l < u ∧ Ico l u = S}

pp: α : 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
x y : αᵒᵈ
hlt : x < y
he : Ioo x y = ∅
⊢ Ioo y x = ∅

Tactic:
· ext s
    constructor <;> rintro ⟨l, hl, u, hu, hlt, rfl⟩
    exacts [⟨u, hu, l, hl, hlt, Ico_toDual⟩, ⟨u, hu, l, hl, hlt, Ioc_toDual⟩]

Goal state after:
α : 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
x y : αᵒᵈ
hlt : x < y
he : Ioo x y = ∅
⊢ Ioo y x = ∅
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
h : x ∈ s
⊢ infDist x s = 0

Tactic:
by
  simp [infEDist_zero_of_mem h, infDist]

Goal state after:
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)]
  exact isLUB_ciSup h_bdd

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f✝ g✝ : α →ₛ ℝ≥0∞
h : f✝ ≤ g✝
f g : α →ₛ ℝ≥0∞
⊢ (map Prod.fst (f.pair g)).lintegral μ ≤ (map (fun p ↦ max p.1 p.2) (f.pair g)).lintegral μ

Tactic:
simp only [map_lintegral]

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

Goal state before:
pp: α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_5
μ : Measure δ
s : Set ι
f : ι → δ → α
hs : s.Countable
hf : ∀ i ∈ s, AEMeasurable (f i) μ
g : ι → δ → α := fun i ↦ if hi : i ∈ s then mk (f i) ⋯ else fun _b ↦ sSup ∅
⊢ AEMeasurable (fun b ↦ ⨆ i ∈ s, f i b) μ

Tactic:
have : ∀ i ∈ s, Measurable (g i) := by
    intro i hi
    simpa [g, hi] using! (hf i hi).measurable_mk

Goal state after:
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_5
μ : Measure δ
s : Set ι
f : ι → δ → α
hs : s.Countable
hf : ∀ i ∈ s, AEMeasurable (f i) μ
g : ι → δ → α := fun i ↦ if hi : i ∈ s then mk (f i) ⋯ else fun _b ↦ sSup ∅
this : ∀ i ∈ s, Measurable (g i)
⊢ AEMeasurable (fun b ↦ ⨆ i ∈ s, f i b) μ
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0∞
g : α → ℝ≥0∞
μ : Measure α
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (i : ι), AEMeasurable (f i) μ
hlim : ∀ᵐ (a : α) ∂μ, Tendsto (fun i ↦ f i a) u (𝓝 (g a))
v : ℕ → ι
hv : Tendsto v atTop u
h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ
⊢ AEMeasurable g μ

Tactic:
set p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' ↦ Tendsto f' atTop (𝓝 (g x))

Goal state after:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0∞
g : α → ℝ≥0∞
μ : Measure α
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (i : ι), AEMeasurable (f i) μ
hlim : ∀ᵐ (a : α) ∂μ, Tendsto (fun i ↦ f i a) u (𝓝 (g a))
v : ℕ → ι
hv : Tendsto v atTop u
h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' ↦ Tendsto f' atTop (𝓝 (g x))
⊢ AEMeasurable g μ
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : PseudoMetrizableSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
ι : Type u_3
inst✝¹ : Nonempty ι
μ : Measure α
f : ι → α → β
hf : ∀ (n : ι), AEMeasurable (f n) μ
inhabited_h : Inhabited ι
inst✝ : ⊥.IsCountablyGenerated
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n ↦ f n x) ⊥ (𝓝 l)
⊢ ∃ f_lim, Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) ⊥ (𝓝 (f_lim x))

Tactic:
exact ⟨(hf default).mk _, (hf default).measurable_mk, Eventually.of_forall fun x => tendsto_bot⟩

Goal state after:
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
h_meas : ∀ (n : ℕ), MeasurableSet (sets n)
h_finite : ∀ (n : ℕ), μ (sets n) < ∞
n : ℕ
⊢ ∀ x ∈ sets n, f x ≤ ↑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
h_meas : ∀ (n : ℕ), MeasurableSet (sets n)
h_finite : ∀ (n : ℕ), μ (sets n) < ∞
⊢ ⋃ i, sets i = univ

Tactic:
· exact fun x hx => hx.2

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
h_meas : ∀ (n : ℕ), MeasurableSet (sets n)
h_finite : ∀ (n : ℕ), μ (sets n) < ∞
⊢ ⋃ i, sets i = univ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
φ : α →ₛ ℝ≥0
hle : ∀ (x : α), ↑(φ x) ≤ f x
b : ℝ≥0∞
hbφ : b < (SimpleFunc.map ofNNReal φ).lintegral μ + ε
hb : ∀ (i : α →ₛ ℝ≥0), (∀ (x : α), ↑(i x) ≤ f x) → (SimpleFunc.map ofNNReal i).lintegral μ ≤ b
ψ : α →ₛ ℝ≥0
hψ : ∀ (x : α), ↑(ψ x) ≤ f x
this : (SimpleFunc.map ofNNReal φ).lintegral μ ≠ ∞
⊢ (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε

Tactic:
rw [← ENNReal.add_lt_add_iff_left this, ← add_lintegral, ← SimpleFunc.map_add @ENNReal.coe_add]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
φ : α →ₛ ℝ≥0
hle : ∀ (x : α), ↑(φ x) ≤ f x
b : ℝ≥0∞
hbφ : b < (SimpleFunc.map ofNNReal φ).lintegral μ + ε
hb : ∀ (i : α →ₛ ℝ≥0), (∀ (x : α), ↑(i x) ≤ f x) → (SimpleFunc.map ofNNReal i).lintegral μ ≤ b
ψ : α →ₛ ℝ≥0
hψ : ∀ (x : α), ↑(ψ x) ≤ f x
this : (SimpleFunc.map ofNNReal φ).lintegral μ ≠ ∞
⊢ (SimpleFunc.map ofNNReal (φ + (ψ - φ))).lintegral μ < (SimpleFunc.map ofNNReal φ).lintegral μ + ε
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
⊢ StronglyMeasurable f ↔ ∃ c, f = fun x ↦ c

Tactic:
rcases isEmpty_or_nonempty α with hα | hα
  · simp [eq_iff_true_of_subsingleton]
  refine ⟨fun hf => ?_, fun hf_eq => ?_⟩
  · refine ⟨f hα.some, ?_⟩
    let fs := hf.approx
    have h_fs_tendsto : ∀ x, Tendsto (fun n => fs n x) atTop (𝓝 (f x)) := hf.tendsto_approx
    have : ∀ n, ∃ c, ∀ x, fs n x = c := fun n => SimpleFunc.simpleFunc_bot (fs n)
    let cs n := (this n).choose
    have h_cs_eq : ∀ n, ⇑(fs n) = fun _ => cs n := fun n => funext (this n).choose_spec
    conv at h_fs_tendsto => enter [x, 1, n]; rw [h_cs_eq]
    have h_tendsto : Tendsto cs atTop (𝓝 (f hα.some)) := h_fs_tendsto hα.some
    ext1 x
    exact tendsto_nhds_unique (h_fs_tendsto x) h_tendsto
  · obtain ⟨c, rfl⟩ := hf_eq
    exact stronglyMeasurable_const

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)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ ∃ t, IsSeparable t ∧ ∀ᵐ (x : α) ∂sum μ, f x ∈ t

Tactic:
have A : ∀ i : ι, ∃ t : Set β, IsSeparable t ∧ f ⁻¹' t ∈ ae (μ i) := fun i =>
    (aestronglyMeasurable_iff_aemeasurable_separable.1 (h i)).2

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝² : Countable ι
inst✝¹ : TopologicalSpace β
f : α → β
inst✝ : PseudoMetrizableSpace β
m : MeasurableSpace α
μ : ι → Measure α
h : ∀ (i : ι), AEStronglyMeasurable f (μ i)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
A : ∀ (i : ι), ∃ t, IsSeparable t ∧ f ⁻¹' t ∈ ae (μ i)
⊢ ∃ t, IsSeparable t ∧ ∀ᵐ (x : α) ∂sum μ, f x ∈ t
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
⊢ 0 < ∫⁻ (a : α), f a ∂μ ↔ 0 < μ (Function.support f)

Tactic:
simp [pos_iff_ne_zero, hf, Filter.EventuallyEq, ae_iff, Function.support]

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)
⊢ ∫⁻ (a : α), aeSeq h_meas p 0 a ∂μ ≠ ∞

Tactic:
lintegral_congr_ae (aeSeq.aeSeq_n_eq_fun_n_ae h_meas hp 0)

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)
⊢ ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_3
f : ι → α → ℝ≥0∞
u : Filter ι
inst✝ : u.IsCountablyGenerated
h_meas : ∀ (i : ι), AEMeasurable (f i) μ
hu : u.NeBot
g : ℕ → ι
hg : Tendsto (fun n ↦ ∫⁻ (a : α), f (g n) a ∂μ) atTop (𝓝 (liminf (fun i ↦ ∫⁻ (a : α), f i a ∂μ) u)) ∧ Tendsto g atTop u
⊢ ∫⁻ (a : α), liminf (fun i ↦ f i a) u ∂μ ≤ liminf (fun i ↦ ∫⁻ (a : α), f i a ∂μ) u

Tactic:
calc
    _ ≤ ∫⁻ a, liminf (fun n => f (g n) a) atTop ∂μ :=
      lintegral_mono fun a => hg.2.liminf_le_liminf_comp
    _ ≤ liminf (fun n => ∫⁻ a, f (g n) a ∂μ) atTop :=
      lintegral_liminf_nat_le' (fun n => h_meas (g n))
    _ = _ := hg.1.liminf_eq

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
hf₀ : ¬∫⁻ (a : α), f a ∂μ = 0
g : α →ₛ ℝ≥0∞
hgf : ⇑g ≤ f
hgε : ∫⁻ (a : α), f a ∂μ - ε < g.lintegral μ
⊢ ∃ g ≤ f, Measurable g ∧ μ (support g) < ∞ ∧ ∫⁻ (a : α), f a ∂μ - ε < ∫⁻ (a : α), g a ∂μ

Tactic:
refine ⟨g, hgf, g.measurable, ?_, by rwa [g.lintegral_eq_lintegral]⟩

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
hf₀ : ¬∫⁻ (a : α), f a ∂μ = 0
g : α →ₛ ℝ≥0∞
hgf : ⇑g ≤ f
hgε : ∫⁻ (a : α), f a ∂μ - ε < g.lintegral μ
⊢ μ (support ⇑g) < ∞
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Norm

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
⊢ ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ ≤ ∫⁻ (x : α), ‖f x‖ₑ ∂μ

Tactic:
simp_rw [← ofReal_norm]

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
⊢ ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ ≤ ∫⁻ (x : α), ENNReal.ofReal ‖f x‖ ∂μ
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst✝⁴ : TopologicalSpace β
𝕜 : Type u_5
inst✝³ : TopologicalSpace 𝕜
inst✝² : Zero β
inst✝¹ : SMulZeroClass 𝕜 β
inst✝ : ContinuousSMul 𝕜 β
hf : FinStronglyMeasurable f μ
c : 𝕜
⊢ FinStronglyMeasurable (c • f) μ

Tactic:
refine ⟨fun n => c • hf.approx n, fun n => ?_, fun x => (hf.tendsto_approx x).const_smul c⟩

Goal state after:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst✝⁴ : TopologicalSpace β
𝕜 : Type u_5
inst✝³ : TopologicalSpace 𝕜
inst✝² : Zero β
inst✝¹ : SMulZeroClass 𝕜 β
inst✝ : ContinuousSMul 𝕜 β
hf : FinStronglyMeasurable f μ
c : 𝕜
n : ℕ
⊢ μ (support ⇑((fun n ↦ c • hf.approx n) n)) < ∞
Module: Mathlib.Topology.Perfect

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed[inst✝¹] C
b : Set (Set α)
bct : b.Countable
left✝ : ∅ ∉ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ (U ∩ C).Countable}
V : Set α := ⋃ U ∈ v, U
D : Set α := C \ V
Vct : (V ∩ C).Countable
x✝ : Set α
⊢ x✝ ∈ v → IsOpen[inst✝¹] x✝

Tactic:
exact fun ⟨Ub, _⟩ ↦ IsTopologicalBasis.isOpen bbasis Ub

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

Goal state before:
pp: X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε
x : X
y : Y
z : X
p q : Z
⊢ dist x z ≤ dist (Φ q) z + dist y (Ψ q) + (dist x (Φ p) + (dist y (Ψ p) + 2 * ε))

Tactic:
linarith [dist_triangle4 x (Φ p) (Φ q) z, dist_triangle_left (Ψ p) (Ψ q) y, (abs_le.1 (H p q)).2]

Goal state after:
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: α : Type ?u.3
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c d : α
h : a ≤ b
δ : α
s t : ↑unitInterval
⊢ ↑s * (1 - ↑t) / (1 - ↑s * ↑t) ≤ 1

Tactic:
apply div_le_one_of_le₀
      · nlinarith [s.2.2]
      · nlinarith [s.2.2, t.2.2, t.2.1]

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

Goal state before:
pp: E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
⊢ cylinder x n = (↑(Finset.range n)).pi fun i ↦ {x i}

Tactic:
ext y
  simp [cylinder]

Goal state after: