mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Filter.CountableSeparatingOn

Goal state before:
pp: case inr
α : Type u_1
l : Filter α
inst✝¹ : CountableInterFilter l
p : Set α → Prop
s : Set α
inst✝ : HasCountableSeparatingOn α p s
hs : s ∈ l
hne : s.Nonempty
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
x : α
hts : {x} ⊆ s
ht : {x}.Subsingleton
htl : {x} ∈ l
⊢ ∃ a ∈ s, {a} ∈ l

Tactic:
exact ⟨x, hts rfl, htl⟩

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : SigmaFinite μ
hs : MeasurableSet s
⊢ (μ.restrict (⋃ i, spanningSets μ i)) s = μ s

Tactic:
by rw [iUnion_spanningSets, restrict_univ]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
P : α → Prop
h : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ν s < ∞ → ∀ᵐ (x : α) ∂μ.restrict s, P x
⊢ ∀ᵐ (x : α) ∂μ, P x

Tactic:
have : ∀ n, ∀ᵐ x ∂μ, x ∈ spanningSets (μ + ν) n → P x := by
    intro n
    have := h
      (spanningSets (μ + ν) n) (measurableSet_spanningSets _ _)
      ((self_le_add_right _ _).trans_lt (measure_spanningSets_lt_top (μ + ν) _))
      ((self_le_add_left _ _).trans_lt (measure_spanningSets_lt_top (μ + ν) _))
    exact (ae_restrict_iff' (measurableSet_spanningSets _ _)).mp this
  filter_upwards [ae_all_iff.2 this] with _ hx using hx _ (mem_spanningSetsIndex _ _)

Goal state after:
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)
P_cover : ∀ {i : ι}, i ∈ F → s i ⊆ ⋃ C ∈ G i, P C
iUnion_P : ⋃ C ∈ Cs, P C ⊆ ⋃ i, s i
P_subset_s : ∀ {i : ι} {C : Finset ι}, i ∈ C → P C ⊆ s i
mem_C : ∀ {i : ι}, i ∈ F → ∀ {C : Finset ι} {x : α}, x ∈ P C → x ∈ s i → i ∈ C
C_subset_C : ∀ {C₁ C₂ : Finset ι}, C₁ ∈ Cs → ∀ {x : α}, x ∈ P C₁ ∩ P C₂ → C₁ ⊆ C₂
⊢ ∑ i ∈ F, ∑' (C : ↑(G i)), (μ.restrict (P ↑C)) t =
    ∑' (C : Finset ι), ∑ i ∈ F, (G i).indicator (fun C ↦ (μ.restrict (P C)) t) C

Tactic:
by
      rw [Summable.tsum_finsetSum (fun _ _ ↦ ENNReal.summable)]
      congr with i
      rw [tsum_subtype (G i) (fun C ↦ (μ.restrict (P C)) t)]

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

Goal state before:
pp: case refine_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
s : Set α := toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := s.piecewise (fun x ↦ h₀.some) (mk f H)
⊢ Measurable g

Tactic:
exact Measurable.piecewise (measurableSet_toMeasurable _ _) measurable_const H.measurable_mk

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → γ
hg : MeasurableEmbedding g
μ : Measure α
H : AEMeasurable (g ∘ f) μ
⊢ AEMeasurable ((rangeSplitting g ∘ rangeFactorization g) ∘ f) μ

Tactic:
exact hg.measurable_rangeSplitting.comp_aemeasurable H.subtype_mk

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

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
a✝ : Nontrivial β
inhabited_h : Inhabited β
S : Set (Set β)
hSc : S.Countable
hc : MeasurableSpace.CountablyGenerated β
h : NullMeasurable f μ
T : Set β → Set α
hTf : ∀ s ∈ S, T s ⊆ f ⁻¹' s
hTm : ∀ s ∈ S, MeasurableSet (T s)
hTeq : ∀ s ∈ S, T s =ᵐ[μ] f ⁻¹' s
U : Set β → Set α
hUf : ∀ s ∈ S, U s ⊇ f ⁻¹' s
hUm : ∀ s ∈ S, MeasurableSet (U s)
hUeq : ∀ s ∈ S, U s =ᵐ[μ] f ⁻¹' s
v : Set α := ⋃ s ∈ S, U s \ T s
hvm : MeasurableSet v
hvμ : μ v = 0
s : Set β
hs : s ∈ S
x : α
hxv : x ∈ vᶜ
hx : x ∈ f ⁻¹' s
⊢ x ∈ T s

Tactic:
exact by_contra fun hx' ↦ hxv <| mem_biUnion hs ⟨hUf s hs hx, hx'⟩

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

Goal state before:
pp: case inr
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
f : α → β
t : Set β
inst✝ : MeasurableSpace.CountablyGenerated ↑t
h : NullMeasurable f μ
hft : ∀ᵐ (x : α) ∂μ.completion, f x ∈ t
hne : t.Nonempty
f' : α → β
hf'm : NullMeasurable f' μ
hf't : range f' ⊆ t
hff' : f =ᵐ[μ] f'
⊢ AEMeasurable f μ

Tactic:
range_subset_iff

Goal state after:
case inr
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
f : α → β
t : Set β
inst✝ : MeasurableSpace.CountablyGenerated ↑t
h : NullMeasurable f μ
hft : ∀ᵐ (x : α) ∂μ.completion, f x ∈ t
hne : t.Nonempty
f' : α → β
hf'm : NullMeasurable f' μ
hf't : ∀ (y : α), f' y ∈ t
hff' : f =ᵐ[μ] f'
⊢ AEMeasurable f μ
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:

Tactic:
infEDist x s ≤ edist x z := infEDist_le_edist_of_mem zs
    _ ≤ edist x y + edist y z := edist_triangle _ _ _
    _ ≤ infEDist x (closure s) + ε / 2 + ε / 2 := add_le_add (le_of_lt hy) (le_of_lt dyz)
    _ = infEDist x (closure s) + ↑ε := by rw [add_assoc, ENNReal.add_halves]

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

Goal state before:
pp: α' : Type u_6
inst✝¹ : TopologicalSpace α'
inst✝ : MeasurableSpace α'
μ : Measure α'
s s' : Set α'
h : μ (frontier s) = 0
h' : μ (frontier s') = 0
⊢ μ (frontier s) + μ (frontier s') = 0

Tactic:
by simp [h, h']

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

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

Tactic:
have : infEDist x ∅ ≤ hausdorffEDist s ∅ := infEDist_le_hausdorffEDist_of_mem xs

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
x : α
xs : x ∈ s
this : infEDist x ∅ ≤ hausdorffEDist s ∅
⊢ hausdorffEDist s ∅ = ∞
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case refine_2
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
h : ∀ (a : α), μ (Iic a) = ν (Iic a)
a b : α
hlt : a < b
⊢ μ (Iic b \ Iic a) = ν (Iic b \ Iic a)

Tactic:
measure_sdiff (Iic_subset_Iic.2 hlt.le) nullMeasurableSet_Iic,

Goal state after:
case refine_2
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
h : ∀ (a : α), μ (Iic a) = ν (Iic a)
a b : α
hlt : a < b
⊢ μ (Iic b) - μ (Iic a) = ν (Iic b \ Iic a)

case refine_2
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
h : ∀ (a : α), μ (Iic a) = ν (Iic a)
a b : α
hlt : a < b
⊢ μ (Iic a) ≠ ∞
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case refine_2
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
h : ∀ (a : α), μ (Iic a) = ν (Iic a)
a b : α
hlt : a < b
⊢ μ (Iic b) - μ (Iic a) = ν (Iic b \ Iic a)

pp: case refine_2
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
h : ∀ (a : α), μ (Iic a) = ν (Iic a)
a b : α
hlt : a < b
⊢ μ (Iic a) ≠ ∞

Tactic:
measure_sdiff (Iic_subset_Iic.2 hlt.le) nullMeasurableSet_Iic,

Goal state after:
case refine_2
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
h : ∀ (a : α), μ (Iic a) = ν (Iic a)
a b : α
hlt : a < b
⊢ μ (Iic b) - μ (Iic a) = ν (Iic b) - ν (Iic a)

case refine_2
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
h : ∀ (a : α), μ (Iic a) = ν (Iic a)
a b : α
hlt : a < b
⊢ ν (Iic a) ≠ ∞

case refine_2
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
h : ∀ (a : α), μ (Iic a) = ν (Iic a)
a b : α
hlt : a < b
⊢ μ (Iic a) ≠ ∞
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: β : Type u_2
α : Type u_5
inst✝¹ : MeasurableSpace α
inst✝ : Nonempty α
b : β
⊢ ↑(const α b).range = ↑{b}

Tactic:
by simp +unfoldPartialApp [Function.const]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
f : α →ₛ β
μ : Measure α
⊢ ∑ y ∈ f.range, μ (⇑f ⁻¹' {y}) = μ univ

Tactic:
by
  rw [f.sum_measure_preimage_singleton, coe_range, preimage_range]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Zero γ
g : β → γ
hg : g 0 = 0
f : α →ₛ β
s : Set α
⊢ map g (f.restrict s) = (map g f).restrict s

Tactic:
classical
  exact ext fun x =>
    if hs : MeasurableSet s then by simp [hs, Set.indicator_comp_of_zero hg]
    else by simp [restrict_of_not_measurable hs, hg]

Goal state after:
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 k ↦ (const α (i k)).restrict {a | i k ≤ f a}) a =
    (Finset.range n).sup fun k ↦ if i k ≤ f a then i k else 0

Tactic:
finset_sup_apply

Goal state after:
α : 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
Module: Mathlib.Topology.Instances.Real.Lemmas

Goal state before:
pp: q : ℚ
⊢ closure (Rat.cast '' {x | q < x}) = {r | ↑q ≤ r}

Tactic:
by
  convert! closure_ordConnected_inter_rat (ordConnected_Ioi (a := (q : ℝ))) _ using 1
  · congr!; aesop
  · exact (closure_Ioi _).symm
  · exact ⟨q + 1, show (q : ℝ) < _ by linarith, q + 2, show (q : ℝ) < _ by linarith, by simp⟩

Goal state after:
Module: Mathlib.Topology.IndicatorConstPointwise

Goal state before:
pp: case neg
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst✝¹ : DecidablePred p
q : Prop
inst✝ : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
h : Tendsto (fun i ↦ if p i then a else b) L (if q then F else G)
hq : ¬q
⊢ ∀ᶠ (i : ι) in L, p i ↔ q

Tactic:
simp only [hq, ite_false] at h
      filter_upwards [mem_map.mp (h haG)] with i hi
      simp only [Set.preimage_compl, Set.mem_compl_iff, Set.mem_preimage, Set.mem_singleton_iff,
        ite_eq_left_iff, not_forall, exists_prop] at hi
      tauto

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

Goal state before:
pp: case hunion
X : Type u_3
Y : Type u_4
α : Type u_5
inst✝⁷ : Zero α
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : MeasurableSpace X
inst✝³ : MeasurableSpace Y
inst✝² : OpensMeasurableSpace X
inst✝¹ : OpensMeasurableSpace Y
inst✝ : PseudoMetricSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
ε : ℝ
hε : 0 < ε
K : Set (X × Y)
hK : IsCompact K
t t' : Set (X × Y)
g : SimpleFunc (X × Y) α
s : Set (X × Y)
s_meas : MeasurableSet s
ts : t ⊆ s
hg : ∀ x ∈ s, dist (f x) (g x) < ε
g' : SimpleFunc (X × Y) α
s' : Set (X × Y)
s'_meas : MeasurableSet s'
t's' : t' ⊆ s'
hg' : ∀ x ∈ s', dist (f x) (g' x) < ε
p : X × Y
hp : p ∈ s ∪ s'
⊢ dist (f p) ((SimpleFunc.piecewise s s_meas g g') p) < ε

Tactic:
by_cases H : p ∈ s

Goal state after:
case pos
X : Type u_3
Y : Type u_4
α : Type u_5
inst✝⁷ : Zero α
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : MeasurableSpace X
inst✝³ : MeasurableSpace Y
inst✝² : OpensMeasurableSpace X
inst✝¹ : OpensMeasurableSpace Y
inst✝ : PseudoMetricSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
ε : ℝ
hε : 0 < ε
K : Set (X × Y)
hK : IsCompact K
t t' : Set (X × Y)
g : SimpleFunc (X × Y) α
s : Set (X × Y)
s_meas : MeasurableSet s
ts : t ⊆ s
hg : ∀ x ∈ s, dist (f x) (g x) < ε
g' : SimpleFunc (X × Y) α
s' : Set (X × Y)
s'_meas : MeasurableSet s'
t's' : t' ⊆ s'
hg' : ∀ x ∈ s', dist (f x) (g' x) < ε
p : X × Y
hp : p ∈ s ∪ s'
H : p ∈ s
⊢ dist (f p) ((SimpleFunc.piecewise s s_meas g g') p) < ε

case neg
X : Type u_3
Y : Type u_4
α : Type u_5
inst✝⁷ : Zero α
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : MeasurableSpace X
inst✝³ : MeasurableSpace Y
inst✝² : OpensMeasurableSpace X
inst✝¹ : OpensMeasurableSpace Y
inst✝ : PseudoMetricSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
ε : ℝ
hε : 0 < ε
K : Set (X × Y)
hK : IsCompact K
t t' : Set (X × Y)
g : SimpleFunc (X × Y) α
s : Set (X × Y)
s_meas : MeasurableSet s
ts : t ⊆ s
hg : ∀ x ∈ s, dist (f x) (g x) < ε
g' : SimpleFunc (X × Y) α
s' : Set (X × Y)
s'_meas : MeasurableSet s'
t's' : t' ⊆ s'
hg' : ∀ x ∈ s', dist (f x) (g' x) < ε
p : X × Y
hp : p ∈ s ∪ s'
H : p ∉ s
⊢ dist (f p) ((SimpleFunc.piecewise s s_meas g g') p) < ε
Module: Mathlib.MeasureTheory.Function.SimpleFuncDense

Goal state before:
pp: case pos
X : Type u_3
Y : Type u_4
α : Type u_5
inst✝⁷ : Zero α
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : MeasurableSpace X
inst✝³ : MeasurableSpace Y
inst✝² : OpensMeasurableSpace X
inst✝¹ : OpensMeasurableSpace Y
inst✝ : PseudoMetricSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
ε : ℝ
hε : 0 < ε
K : Set (X × Y)
hK : IsCompact K
t t' : Set (X × Y)
g : SimpleFunc (X × Y) α
s : Set (X × Y)
s_meas : MeasurableSet s
ts : t ⊆ s
hg : ∀ x ∈ s, dist (f x) (g x) < ε
g' : SimpleFunc (X × Y) α
s' : Set (X × Y)
s'_meas : MeasurableSet s'
t's' : t' ⊆ s'
hg' : ∀ x ∈ s', dist (f x) (g' x) < ε
p : X × Y
hp : p ∈ s ∪ s'
H : p ∈ s
⊢ dist (f p) ((SimpleFunc.piecewise s s_meas g g') p) < ε

pp: case neg
X : Type u_3
Y : Type u_4
α : Type u_5
inst✝⁷ : Zero α
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : MeasurableSpace X
inst✝³ : MeasurableSpace Y
inst✝² : OpensMeasurableSpace X
inst✝¹ : OpensMeasurableSpace Y
inst✝ : PseudoMetricSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
ε : ℝ
hε : 0 < ε
K : Set (X × Y)
hK : IsCompact K
t t' : Set (X × Y)
g : SimpleFunc (X × Y) α
s : Set (X × Y)
s_meas : MeasurableSet s
ts : t ⊆ s
hg : ∀ x ∈ s, dist (f x) (g x) < ε
g' : SimpleFunc (X × Y) α
s' : Set (X × Y)
s'_meas : MeasurableSet s'
t's' : t' ⊆ s'
hg' : ∀ x ∈ s', dist (f x) (g' x) < ε
p : X × Y
hp : p ∈ s ∪ s'
H : p ∉ s
⊢ dist (f p) ((SimpleFunc.piecewise s s_meas g g') p) < ε

Tactic:
· simpa [H, SimpleFunc.piecewise_apply] using hg p H

Goal state after:
case neg
X : Type u_3
Y : Type u_4
α : Type u_5
inst✝⁷ : Zero α
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : MeasurableSpace X
inst✝³ : MeasurableSpace Y
inst✝² : OpensMeasurableSpace X
inst✝¹ : OpensMeasurableSpace Y
inst✝ : PseudoMetricSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
ε : ℝ
hε : 0 < ε
K : Set (X × Y)
hK : IsCompact K
t t' : Set (X × Y)
g : SimpleFunc (X × Y) α
s : Set (X × Y)
s_meas : MeasurableSet s
ts : t ⊆ s
hg : ∀ x ∈ s, dist (f x) (g x) < ε
g' : SimpleFunc (X × Y) α
s' : Set (X × Y)
s'_meas : MeasurableSet s'
t's' : t' ⊆ s'
hg' : ∀ x ∈ s', dist (f x) (g' x) < ε
p : X × Y
hp : p ∈ s ∪ s'
H : p ∉ s
⊢ dist (f p) ((SimpleFunc.piecewise s s_meas g g') p) < ε
Module: Mathlib.MeasureTheory.Function.SimpleFuncDense

Goal state before:
pp: X : Type u_3
Y : Type u_4
α : Type u_5
inst✝⁷ : Zero α
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : MeasurableSpace X
inst✝³ : MeasurableSpace Y
inst✝² : OpensMeasurableSpace X
inst✝¹ : OpensMeasurableSpace Y
inst✝ : PseudoMetricSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
ε : ℝ
hε : 0 < ε
M : ∀ (K : Set (X × Y)), IsCompact K → ∃ g s, MeasurableSet s ∧ K ⊆ s ∧ ∀ x ∈ s, dist (f x) (g x) < ε
g : SimpleFunc (X × Y) α
s : Set (X × Y)
s_meas : MeasurableSet s
fs : tsupport f ⊆ s
hg : ∀ x ∈ s, dist (f x) (g x) < ε
p : X × Y
⊢ dist (f p) ((SimpleFunc.piecewise s s_meas g 0) p) < ε

Tactic:
by_cases H : p ∈ s

Goal state after:
case pos
X : Type u_3
Y : Type u_4
α : Type u_5
inst✝⁷ : Zero α
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : MeasurableSpace X
inst✝³ : MeasurableSpace Y
inst✝² : OpensMeasurableSpace X
inst✝¹ : OpensMeasurableSpace Y
inst✝ : PseudoMetricSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
ε : ℝ
hε : 0 < ε
M : ∀ (K : Set (X × Y)), IsCompact K → ∃ g s, MeasurableSet s ∧ K ⊆ s ∧ ∀ x ∈ s, dist (f x) (g x) < ε
g : SimpleFunc (X × Y) α
s : Set (X × Y)
s_meas : MeasurableSet s
fs : tsupport f ⊆ s
hg : ∀ x ∈ s, dist (f x) (g x) < ε
p : X × Y
H : p ∈ s
⊢ dist (f p) ((SimpleFunc.piecewise s s_meas g 0) p) < ε

case neg
X : Type u_3
Y : Type u_4
α : Type u_5
inst✝⁷ : Zero α
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : MeasurableSpace X
inst✝³ : MeasurableSpace Y
inst✝² : OpensMeasurableSpace X
inst✝¹ : OpensMeasurableSpace Y
inst✝ : PseudoMetricSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
ε : ℝ
hε : 0 < ε
M : ∀ (K : Set (X × Y)), IsCompact K → ∃ g s, MeasurableSet s ∧ K ⊆ s ∧ ∀ x ∈ s, dist (f x) (g x) < ε
g : SimpleFunc (X × Y) α
s : Set (X × Y)
s_meas : MeasurableSet s
fs : tsupport f ⊆ s
hg : ∀ x ∈ s, dist (f x) (g x) < ε
p : X × Y
H : p ∉ s
⊢ dist (f p) ((SimpleFunc.piecewise s s_meas g 0) p) < ε
Module: Mathlib.MeasureTheory.Function.SimpleFuncDense

Goal state before:
pp: case pos
X : Type u_3
Y : Type u_4
α : Type u_5
inst✝⁷ : Zero α
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : MeasurableSpace X
inst✝³ : MeasurableSpace Y
inst✝² : OpensMeasurableSpace X
inst✝¹ : OpensMeasurableSpace Y
inst✝ : PseudoMetricSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
ε : ℝ
hε : 0 < ε
M : ∀ (K : Set (X × Y)), IsCompact K → ∃ g s, MeasurableSet s ∧ K ⊆ s ∧ ∀ x ∈ s, dist (f x) (g x) < ε
g : SimpleFunc (X × Y) α
s : Set (X × Y)
s_meas : MeasurableSet s
fs : tsupport f ⊆ s
hg : ∀ x ∈ s, dist (f x) (g x) < ε
p : X × Y
H : p ∈ s
⊢ dist (f p) ((SimpleFunc.piecewise s s_meas g 0) p) < ε

pp: case neg
X : Type u_3
Y : Type u_4
α : Type u_5
inst✝⁷ : Zero α
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : MeasurableSpace X
inst✝³ : MeasurableSpace Y
inst✝² : OpensMeasurableSpace X
inst✝¹ : OpensMeasurableSpace Y
inst✝ : PseudoMetricSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
ε : ℝ
hε : 0 < ε
M : ∀ (K : Set (X × Y)), IsCompact K → ∃ g s, MeasurableSet s ∧ K ⊆ s ∧ ∀ x ∈ s, dist (f x) (g x) < ε
g : SimpleFunc (X × Y) α
s : Set (X × Y)
s_meas : MeasurableSet s
fs : tsupport f ⊆ s
hg : ∀ x ∈ s, dist (f x) (g x) < ε
p : X × Y
H : p ∉ s
⊢ dist (f p) ((SimpleFunc.piecewise s s_meas g 0) p) < ε

Tactic:
· simpa [H, SimpleFunc.piecewise_apply] using hg p H

Goal state after:
case neg
X : Type u_3
Y : Type u_4
α : Type u_5
inst✝⁷ : Zero α
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : MeasurableSpace X
inst✝³ : MeasurableSpace Y
inst✝² : OpensMeasurableSpace X
inst✝¹ : OpensMeasurableSpace Y
inst✝ : PseudoMetricSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
ε : ℝ
hε : 0 < ε
M : ∀ (K : Set (X × Y)), IsCompact K → ∃ g s, MeasurableSet s ∧ K ⊆ s ∧ ∀ x ∈ s, dist (f x) (g x) < ε
g : SimpleFunc (X × Y) α
s : Set (X × Y)
s_meas : MeasurableSet s
fs : tsupport f ⊆ s
hg : ∀ x ∈ s, dist (f x) (g x) < ε
p : X × Y
H : p ∉ s
⊢ dist (f p) ((SimpleFunc.piecewise s s_meas g 0) p) < ε
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := hf.approx
h_fs_tendsto : ∀ (x : α), Tendsto (fun n ↦ (fs n) x) atTop (𝓝 (f x))
this : ∀ (n : ℕ), ∃ c, ∀ (x : α), (fs n) x = c
cs : ℕ → β := fun n ↦ ⋯.choose
h_cs_eq : ∀ (n : ℕ), ⇑(fs n) = fun x ↦ cs n
| ∀ (x : α), Tendsto (fun n ↦ (fs n) x) atTop (𝓝 (f x))

Tactic:
enter [x, 1, n]; rw [h_cs_eq]

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := hf.approx
h_fs_tendsto : ∀ (x : α), Tendsto (fun n ↦ (fs n) x) atTop (𝓝 (f x))
this : ∀ (n : ℕ), ∃ c, ∀ (x : α), (fs n) x = c
cs : ℕ → β := fun n ↦ ⋯.choose
h_cs_eq : ∀ (n : ℕ), ⇑(fs n) = fun x ↦ cs n
x : α
n : ℕ
| (fun x ↦ cs n) x
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: case mpr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∫⁻ (a : α), f a ∂μ = 0
meas_levels_0 : ∀ ε > 0, μ {x | ε ≤ f x} = 0
u : ℕ → ℝ≥0∞
bu : ∀ (n : ℕ), u n ∈ Ioo 0 1
tu : ∀ ε > 0, ∃ N, ∀ n ≥ N, u n ≤ ε
x : α
n : ℕ
hn : x ∈ {x | u n ≤ f x}
⊢ 0 < f x

Tactic:
exact (bu n).1.trans_le hn

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s t : Set α
⊢ ∫⁻ (a : α) in s ∪ t, f a ∂μ ≤ ∫⁻ (a : α), f a ∂(μ.restrict s + μ.restrict t)

Tactic:
exact lintegral_mono' (restrict_union_le _ _) le_rfl

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

Goal state before:
pp: α : Type u_5
E : Type u_6
x✝ : MeasurableSpace α
inst✝⁵ : AddCancelMonoid E
inst✝⁴ : TopologicalSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : ContinuousAdd E
inst✝ : PseudoMetrizableSpace E
g f : α → E
hg : Measurable g
hf : StronglyMeasurable f
⊢ Measurable (g + f)

Tactic:
by
  rcases hf with ⟨φ, hφ⟩
  have : Tendsto (fun n x ↦ g x + φ n x) atTop (𝓝 (g + f)) :=
    tendsto_pi_nhds.2 (fun x ↦ tendsto_const_nhds.add (hφ x))
  apply measurable_of_tendsto_metrizable (fun n ↦ ?_) this
  exact hg.add_simpleFunc _

Goal state after: