mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α →ₛ ℝ≥0∞
h : ⇑f =ᵐ[μ] ⇑g
y : ℝ≥0∞
x : α
hx : f x = g x
⊢ x ∈ ⇑f ⁻¹' {y} ↔ x ∈ ⇑g ⁻¹' {y}

Tactic:
by simp [hx]

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

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

Tactic:
| empty =>

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
inst✝ : Countable ι
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), Measurable (f i)
⊢ Measurable fun x ↦ ∑' (i : ι), f i x

Tactic:
ENNReal.tsum_eq_iSup_sum

Goal state after:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
inst✝ : Countable ι
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), Measurable (f i)
⊢ Measurable fun x ↦ ⨆ s, ∑ i ∈ s, f i x
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
inst✝ : Countable ι
f : ι → α → ℝ≥0∞
μ : Measure α
h : ∀ (i : ι), AEMeasurable (f i) μ
⊢ AEMeasurable (fun x ↦ ∑' (i : ι), f i x) μ

Tactic:
ENNReal.tsum_eq_iSup_sum

Goal state after:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
inst✝ : Countable ι
f : ι → α → ℝ≥0∞
μ : Measure α
h : ∀ (i : ι), AEMeasurable (f i) μ
⊢ AEMeasurable (fun x ↦ ⨆ s, ∑ i ∈ s, f i x) μ
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
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) < ∞
this : ⋃ i, sigma_finite_sets i ∩ norm_sets i = (⋃ i, sigma_finite_sets i) ∩ ⋃ i, norm_sets i
⊢ (⋃ i, sigma_finite_sets i) ∩ ⋃ i, norm_sets i = univ

Tactic:
norm_sets_spanning,

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) < ∞
this : ⋃ i, sigma_finite_sets i ∩ norm_sets i = (⋃ i, sigma_finite_sets i) ∩ ⋃ i, norm_sets i
⊢ (⋃ i, sigma_finite_sets i) ∩ univ = univ
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: case empty
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : Nonempty γ
P : (α →ₛ γ) → Prop
const : ∀ (c : γ), P (SimpleFunc.const α c)
pcw : ∀ ⦃f g : α →ₛ γ⦄ {s : Set α} (hs : MeasurableSet s), P f → P g → P (piecewise s hs f g)
c : γ := Classical.ofNonempty
f : α →ₛ γ
h : range ⇑f \ {c} = ↑∅
⊢ P f

Tactic:
| empty =>

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

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

Tactic:
List.forall_mem_cons

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

Goal state before:
pp: α : Type u_1
β : Type u_5
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n ↦ (hf.approx n) x) atTop (𝓝 0)
hfx0 : f x = 0
⊢ 0 = ‖0‖

Tactic:
rw [norm_zero]

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

Goal state before:
pp: case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : α → ℝ≥0∞ := fun a ↦ ⨆ n, f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), ↑(s x) ≤ ⨆ n, f n x
r : ℝ≥0
right✝ ha✝ : ↑r < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun a ↦ r * a) s
eq_rs : SimpleFunc.map c rs = const α ↑r * SimpleFunc.map c s
p : ℝ≥0∞
x : α
hx : x ∈ ⇑(SimpleFunc.map c rs) ⁻¹' {p}
p_eq : p = 0
⊢ x ∈ ⋃ i, {a | p ≤ f i a}

Tactic:
simp [p_eq]

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 : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : α → ℝ≥0∞ := fun a ↦ ⨆ n, f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), ↑(s x) ≤ ⨆ n, f n x
r : ℝ≥0
right✝ ha✝ : ↑r < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun a ↦ r * a) s
eq_rs : SimpleFunc.map c rs = const α ↑r * SimpleFunc.map c s
x : α
p_eq : ¬c (rs x) = 0
this : r * s x ≠ 0
⊢ x ∈ ⋃ i, {a | c (rs x) ≤ f i a}

Tactic:
have : s x ≠ 0 := right_ne_zero_of_mul this

Goal state after:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : α → ℝ≥0∞ := fun a ↦ ⨆ n, f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), ↑(s x) ≤ ⨆ n, f n x
r : ℝ≥0
right✝ ha✝ : ↑r < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun a ↦ r * a) s
eq_rs : SimpleFunc.map c rs = const α ↑r * SimpleFunc.map c s
x : α
p_eq : ¬c (rs x) = 0
this✝ : r * s x ≠ 0
this : s x ≠ 0
⊢ x ∈ ⋃ i, {a | c (rs x) ≤ f i a}
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
ι : Type u_5
inst✝² : PseudoMetrizableSpace β
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) u (𝓝 (g x))
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ ∃ t, IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, g x ∈ t

Tactic:
rcases u.exists_seq_tendsto with ⟨v, hv⟩
    have : ∀ n : ℕ, ∃ t : Set β, IsSeparable t ∧ f (v n) ⁻¹' t ∈ ae μ := fun n =>
      (aestronglyMeasurable_iff_aemeasurable_separable.1 (hf (v n))).2
    choose t t_sep ht using this
    refine ⟨closure (⋃ i, t i), .closure <| .iUnion t_sep, ?_⟩
    filter_upwards [ae_all_iff.2 ht, lim] with x hx h'x
    apply mem_closure_of_tendsto (h'x.comp hv)
    filter_upwards with n using mem_iUnion_of_mem n (hx n)

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x
⊢ ∀ᵐ (x : α) ∂μ.restrict s, f x = g x

Tactic:
ae_restrict_iff' hs

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hs : MeasurableSet s
hf : AEStronglyMeasurable f (μ.restrict s)
hg : AEStronglyMeasurable g (μ.restrict sᶜ)
h : ∀ᵐ (x : α) ∂μ.restrict s, f x = AEStronglyMeasurable.mk f hf x
⊢ ∀ᵐ (x : α) ∂μ.restrict s,
    s.piecewise f g x = s.piecewise (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x

Tactic:
ae_restrict_iff' hs

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hs : MeasurableSet s
hf : AEStronglyMeasurable f (μ.restrict s)
hg : AEStronglyMeasurable g (μ.restrict sᶜ)
h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = AEStronglyMeasurable.mk f hf x
⊢ ∀ᵐ (x : α) ∂μ.restrict s,
    s.piecewise f g x = s.piecewise (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hs : MeasurableSet s
hf : AEStronglyMeasurable f (μ.restrict s)
hg : AEStronglyMeasurable g (μ.restrict sᶜ)
h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = AEStronglyMeasurable.mk f hf x
⊢ ∀ᵐ (x : α) ∂μ.restrict s,
    s.piecewise f g x = s.piecewise (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x

Tactic:
ae_restrict_iff' hs

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hs : MeasurableSet s
hf : AEStronglyMeasurable f (μ.restrict s)
hg : AEStronglyMeasurable g (μ.restrict sᶜ)
h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = AEStronglyMeasurable.mk f hf x
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → s.piecewise f g x = s.piecewise (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : Zero β
inst✝ : T2Space β
g : α → β
hg : FinStronglyMeasurable g μ
hfg : f =ᵐ[μ] g
⊢ ∃ t, MeasurableSet t ∧ f =ᵐ[μ.restrict tᶜ] 0 ∧ SigmaFinite (μ.restrict t)

Tactic:
obtain ⟨t, ht, hgt_zero, htμ⟩ := hg.exists_set_sigmaFinite

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : Zero β
inst✝ : T2Space β
g : α → β
hg : FinStronglyMeasurable g μ
hfg : f =ᵐ[μ] g
t : Set α
ht : MeasurableSet t
hgt_zero : ∀ x ∈ tᶜ, g x = 0
htμ : SigmaFinite (μ.restrict t)
⊢ ∃ t, MeasurableSet t ∧ f =ᵐ[μ.restrict tᶜ] 0 ∧ SigmaFinite (μ.restrict t)
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

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

Tactic:
apply mul_div_le

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
g : α →ₛ ℝ≥0∞
hg : ⇑g ≤ fun a ↦ s.indicator f a
this : ⇑g ≤ f
⊢ ∑ x ∈ g.range, x * μ (⇑g ⁻¹' {x}) = ∑ y ∈ g.range, y * μ (⇑g ⁻¹' {y} ∩ s)

Tactic:
congr with t

Goal state after:
case e_f
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
g : α →ₛ ℝ≥0∞
hg : ⇑g ≤ fun a ↦ s.indicator f a
this : ⇑g ≤ f
t : ℝ≥0∞
⊢ t * μ (⇑g ⁻¹' {t}) = t * μ (⇑g ⁻¹' {t} ∩ s)
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m✝ : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : ℕ → Set α := spanningSets (μ.restrict t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := hf_meas.approx
fs : ℕ → α →ₛ β := fun n ↦ (f_approx n).restrict (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, (fs n) x = 0
x : α
hxt : x ∈ t
h : ∀ s ∈ 𝓝 (f x), ∃ a, ∀ (b : ℕ), a ≤ b → (f_approx b) x ∈ s
n₁ : ℕ
hn₁ : ∀ (m : ℕ), n₁ ≤ m → (fs m) x = (f_approx m) x
s : Set β
hs : s ∈ 𝓝 (f x)
n₂ : ℕ
hn₂ : ∀ (b : ℕ), n₂ ≤ b → (f_approx b) x ∈ s
m : ℕ
hm : max n₁ n₂ ≤ m
⊢ (f_approx m) x ∈ s

Tactic:
exact hn₂ m ((le_max_right _ _).trans hm)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
g : α → γ
hf : StronglyMeasurable f
hg : StronglyMeasurable g
⊢ StronglyMeasurable fun x ↦ (f x, g x)

Tactic:
refine ⟨fun n => SimpleFunc.pair (hf.approx n) (hg.approx n), fun x => ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
g : α → γ
hf : StronglyMeasurable f
hg : StronglyMeasurable g
x : α
⊢ Tendsto (fun n ↦ ((fun n ↦ (hf.approx n).pair (hg.approx n)) n) x) atTop (𝓝 ((fun x ↦ (f x, g x)) x))
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

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

Tactic:
by
  rw [lintegral_congr_ae hf.ae_eq_mk, lintegral_eq_iSup_eapprox_lintegral hf.measurable_mk]

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

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

Tactic:
List.forall_mem_cons

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

Goal state before:
pp: case empty
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
f : β → α → ℝ≥0∞
hf : ∀ b ∈ ∅, AEMeasurable (f b) μ
⊢ ∫⁻ (a : α), ∑ b ∈ ∅, f b a ∂μ = ∑ b ∈ ∅, ∫⁻ (a : α), f b a ∂μ

Tactic:
| empty =>

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : IsEmbedding g
⊢ (StronglyMeasurable fun x ↦ g (f x)) ↔ StronglyMeasurable f

Tactic:
let := pseudoMetrizableSpacePseudoMetric γ
  borelize β γ
  refine
    ⟨fun H => stronglyMeasurable_iff_measurable_separable.2 ⟨?_, ?_⟩, fun H =>
      hg.continuous.comp_stronglyMeasurable H⟩
  · let G : β → range g := rangeFactorization g
    have hG : IsClosedEmbedding G :=
      { hg.codRestrict _ _ with
        isClosed_range := by
          rw [rangeFactorization_surjective.range_eq]
          exact isClosed_univ }
    have : Measurable (G ∘ f) := Measurable.subtype_mk H.measurable
    exact hG.measurableEmbedding.measurable_comp_iff.1 this
  · have : IsSeparable (g ⁻¹' range (g ∘ f)) := hg.isSeparable_preimage H.isSeparable_range
    rwa [range_comp, hg.injective.preimage_image] at this

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst✝² : Zero β
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
fs : ℕ → α →ₛ β
hT_lt_top : ∀ (n : ℕ), μ (support ⇑(fs n)) < ∞
h_approx : ∀ (x : α), Tendsto (fun n ↦ (fs n) x) atTop (𝓝 (f x))
T : ℕ → Set α := fun n ↦ support ⇑(fs n)
hT_meas : ∀ (n : ℕ), MeasurableSet (T n)
⊢ ∃ t, MeasurableSet t ∧ (∀ x ∈ tᶜ, f x = 0) ∧ SigmaFinite (μ.restrict t)

Tactic:
let t := ⋃ n, T n

Goal state after:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst✝² : Zero β
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
fs : ℕ → α →ₛ β
hT_lt_top : ∀ (n : ℕ), μ (support ⇑(fs n)) < ∞
h_approx : ∀ (x : α), Tendsto (fun n ↦ (fs n) x) atTop (𝓝 (f x))
T : ℕ → Set α := fun n ↦ support ⇑(fs n)
hT_meas : ∀ (n : ℕ), MeasurableSet (T n)
t : Set α := ⋃ n, T n
⊢ ∃ t, MeasurableSet t ∧ (∀ x ∈ tᶜ, f x = 0) ∧ SigmaFinite (μ.restrict t)
Module: Mathlib.Topology.Perfect

Goal state before:
pp: case refine_2
α : 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
⊢ Preperfect D

Tactic:
rw [preperfect_iff_nhds]

Goal state after:
case refine_2
α : 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 ∈ D, ∀ U ∈ 𝓝 x, ∃ y ∈ U ∩ D, y ≠ x
Module: Mathlib.Analysis.Normed.Group.InfiniteSum

Goal state before:
pp: ι : Type u_1
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ≥0
a : ℝ≥0
hg : HasSum g a
h : ∀ (i : ι), ‖f i‖₊ ≤ g i
⊢ ‖∑' (i : ι), f i‖₊ ≤ a

Tactic:
simp only [← NNReal.coe_le_coe, ← NNReal.hasSum_coe, coe_nnnorm] at *
  exact tsum_of_norm_bounded hg h

Goal state after:
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: case pos
a b : ℝ
x y z : ↑(Icc a b)
s t : ↑unitInterval
hs : ↑s = 1
⊢ (1 - ↑s) * ↑x + ↑s * ((1 - ↑t) * ↑y + ↑t * ↑z) =
    (1 - ↑s * ↑t) * ((1 - ↑s * (1 - ↑t) / (1 - ↑s * ↑t)) * ↑x + ↑s * (1 - ↑t) / (1 - ↑s * ↑t) * ↑y) + ↑s * ↑t * ↑z

pp: case neg
a b : ℝ
x y z : ↑(Icc a b)
s t : ↑unitInterval
hs : ¬↑s = 1
⊢ (1 - ↑s) * ↑x + ↑s * ((1 - ↑t) * ↑y + ↑t * ↑z) =
    (1 - ↑s * ↑t) * ((1 - ↑s * (1 - ↑t) / (1 - ↑s * ↑t)) * ↑x + ↑s * (1 - ↑t) / (1 - ↑s * ↑t) * ↑y) + ↑s * ↑t * ↑z

Tactic:
· simp only [hs]
    by_cases ht : (t : ℝ) = 1
    · simp [ht]
    · have : (1 - t : ℝ) ≠ 0 := by grind
      field_simp
      simp

Goal state after:
case neg
a b : ℝ
x y z : ↑(Icc a b)
s t : ↑unitInterval
hs : ¬↑s = 1
⊢ (1 - ↑s) * ↑x + ↑s * ((1 - ↑t) * ↑y + ↑t * ↑z) =
    (1 - ↑s * ↑t) * ((1 - ↑s * (1 - ↑t) / (1 - ↑s * ↑t)) * ↑x + ↑s * (1 - ↑t) / (1 - ↑s * ↑t) * ↑y) + ↑s * ↑t * ↑z
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y z : (n : ℕ) × X n
m : ℕ := max (max x.fst y.fst) z.fst
hx : x.fst ≤ m
hy : y.fst ≤ m
hz : z.fst ≤ m
⊢ dist (leRecOn hx (fun {k} ↦ f k) x.snd) (leRecOn hy (fun {k} ↦ f k) y.snd) +
      dist (leRecOn hy (fun {k} ↦ f k) y.snd) (leRecOn hz (fun {k} ↦ f k) z.snd) =
    dist (leRecOn hx (fun {k} ↦ f k) x.snd) (leRecOn hy (fun {k} ↦ f k) y.snd) + inductiveLimitDist f y z

Tactic:
inductiveLimitDist_eq_dist I y z m hy hz

Goal state after:
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y z : (n : ℕ) × X n
m : ℕ := max (max x.fst y.fst) z.fst
hx : x.fst ≤ m
hy : y.fst ≤ m
hz : z.fst ≤ m
⊢ dist (leRecOn hx (fun {k} ↦ f k) x.snd) (leRecOn hy (fun {k} ↦ f k) y.snd) +
      dist (leRecOn hy (fun {k} ↦ f k) y.snd) (leRecOn hz (fun {k} ↦ f k) z.snd) =
    dist (leRecOn hx (fun {k} ↦ f k) x.snd) (leRecOn hy (fun {k} ↦ f k) y.snd) +
      dist (leRecOn hy (fun {k} ↦ f k) y.snd) (leRecOn hz (fun {k} ↦ f k) z.snd)
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
x y : (n : ℕ) → E n
hx : x ∉ s
hy : y ∈ s
⊢ firstDiff x y ≤ longestPrefix x s

Tactic:
rw [longestPrefix, le_tsub_iff_right]
  · exact firstDiff_lt_shortestPrefixDiff hs hx hy
  · exact shortestPrefixDiff_pos hs ⟨y, hy⟩ hx

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
f : β → ℝ≥0∞
g : α → β
hg : AEMeasurable g μ
⊢ ∫⁻ (a : β), f a ∂Measure.map g μ ≤ ∫⁻ (a : α), f (g a) ∂μ

pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
f : β → ℝ≥0∞
g : α → β
hg : ¬AEMeasurable g μ
⊢ ∫⁻ (a : β), f a ∂Measure.map g μ ≤ ∫⁻ (a : α), f (g a) ∂μ

Tactic:
· rw [← iSup_lintegral_measurable_le_eq_lintegral]
    refine iSup₂_le fun i hi => iSup_le fun h'i => ?_
    rw [lintegral_map' hi.aemeasurable hg]
    exact lintegral_mono fun _ ↦ h'i _

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
f : β → ℝ≥0∞
g : α → β
hg : ¬AEMeasurable g μ
⊢ ∫⁻ (a : β), f a ∂Measure.map g μ ≤ ∫⁻ (a : α), f (g a) ∂μ
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
a : α
⊢ μ.restrict {a} = μ {a} • dirac a

Tactic:
by
  ext1 s hs
  by_cases ha : a ∈ s
  · have : s ∩ {a} = {a} := by simpa
    simp [*]
  · have : s ∩ {a} = ∅ := inter_singleton_eq_empty.2 ha
    simp [*]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
μ : Measure α
measurableAtoms : Set (Set α) := measurableAtom '' univ
h_nonempty : ∀ (s : ↑measurableAtoms), (↑s).Nonempty
points : ↑measurableAtoms → α := fun s ↦ ⋯.some
h_points_mem : ∀ (s : ↑measurableAtoms), points s ∈ ↑s
x : α
⊢ μ (measurableAtom x) = ∑' (i : ↑(range points)), μ (measurableAtom ↑i) * (dirac ↑i) (measurableAtom x)

Tactic:
simp_rw [dirac_apply' _ (MeasurableSet.measurableAtom_of_countable x)]

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
μ : Measure α
measurableAtoms : Set (Set α) := measurableAtom '' univ
h_nonempty : ∀ (s : ↑measurableAtoms), (↑s).Nonempty
points : ↑measurableAtoms → α := fun s ↦ ⋯.some
h_points_mem : ∀ (s : ↑measurableAtoms), points s ∈ ↑s
x : α
⊢ μ (measurableAtom x) = ∑' (i : ↑(range points)), μ (measurableAtom ↑i) * (measurableAtom x).indicator 1 ↑i
Module: Mathlib.MeasureTheory.Measure.Count

Goal state before:
pp: case pos
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
s_mble : MeasurableSet s
hs : s.Finite
⊢ count s = ∞ ↔ s.Infinite

Tactic:
simp [Set.Infinite, hs, count_apply_finite' hs s_mble]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : β → α
hf : Function.Injective f
s : Set β
s_mble : MeasurableSet s
fs_mble : MeasurableSet (f '' s)
⊢ count (f '' s) = count s

Tactic:
classical
  by_cases hs : s.Finite
  · lift s to Finset β using hs
    rw [← Finset.coe_image, count_apply_finset' _, count_apply_finset' s_mble,
      s.card_image_of_injective hf]
    simpa only [Finset.coe_image] using fs_mble
  · rw [count_apply_infinite hs]
    rw [← finite_image_iff hf.injOn] at hs
    rw [count_apply_infinite hs]

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

Goal state before:
pp: X : Type u_3
Y : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : PolishSpace X
inst✝ : T2Space Y
s : Set Y
hs : AnalyticSet s
f : X → Y
hf : Continuous[inst✝³, inst✝²] f
⊢ AnalyticSet (f ⁻¹' s)

Tactic:
rcases analyticSet_iff_exists_polishSpace_range.1 hs with ⟨Z, _, _, g, hg, rfl⟩
  have : IsClosed {x : X × Z | f x.1 = g x.2} := isClosed_eq hf.fst' hg.snd'
  convert! this.analyticSet.image_of_continuous continuous_fst
  ext x
  simp [eq_comm]

Goal state after: