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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
h₁ : s ≤ᵐ[μ] t
h₂ : μ t ≤ μ s
hsm : NullMeasurableSet s μ
ht : μ t ≠ ∞
⊢ s =ᵐ[μ] t

Tactic:
refine eventuallyLE_antisymm_iff.mpr ⟨h₁, ae_le_set.mpr ?_⟩
  replace h₂ : μ t = μ s := h₂.antisymm (measure_mono_ae h₁)
  replace ht : μ s ≠ ∞ := h₂ ▸ ht
  rw [measure_sdiff' t hsm ht, measure_congr (union_ae_eq_left_iff_ae_subset.mpr h₁), h₂, tsub_self]

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

Goal state before:
pp: X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
α : Type u_2
l : Filter α
f : X → α
ha : IsPredPrelimit a
⊢ Tendsto (fun x ↦ f ↑x) atBot l ↔ Tendsto f (𝓝[>] a) l

Tactic:
rw [← map_coe_Ioi_atBot a ha, tendsto_map'_iff, Function.comp_def]

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

Goal state before:
pp: α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : ι → Set α
hs : ∀ (i : ι), NullMeasurableSet (s i) μ
H : μ univ < ∑' (i : ι), μ (s i)
⊢ ∃ i j, i ≠ j ∧ (s i ∩ s j).Nonempty

Tactic:
contrapose! H
  apply tsum_measure_le_measure_univ hs
  intro i j hij
  exact (disjoint_iff_inter_eq_empty.mpr (H i j hij)).aedisjoint

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
inst✝ : IsFiniteMeasure (map f μ)
⊢ μ univ < ∞

Tactic:
rw [← Set.preimage_univ (f := f), ← map_apply_of_aemeasurable hf .univ]

Goal state after:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
inst✝ : IsFiniteMeasure (map f μ)
⊢ (map f μ) univ < ∞
Module: Mathlib.MeasureTheory.Measure.Trim

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
⊢ IsFiniteMeasure (μ.trim ⋯) ↔ IsFiniteMeasure μ

Tactic:
refine ⟨fun h => ⟨?_⟩, fun h => ⟨?_⟩⟩ <;> have h_univ := h.measure_univ_lt_top

Goal state after:
case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
h : IsFiniteMeasure (μ.trim ⋯)
h_univ : (μ.trim ⋯) Set.univ < ∞
⊢ μ Set.univ < ∞

case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
h : IsFiniteMeasure μ
h_univ : μ Set.univ < ∞
⊢ (μ.trim ⋯) Set.univ < ∞
Module: Mathlib.MeasureTheory.Measure.Trim

Goal state before:
pp: case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
h : IsFiniteMeasure μ
h_univ : μ Set.univ < ∞
⊢ (μ.trim ⋯) Set.univ < ∞

Tactic:
rwa [trim_measurableSet_eq bot_le MeasurableSet.univ]

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : α → Prop
hst : s =ᵐ[μ] t
p : α → Prop
⊢ (∀ᵐ (x : α) ∂μ.restrict s, p x) → ∀ᵐ (x : α) ∂μ.restrict t, p x

Tactic:
by simp [Measure.restrict_congr_set hst]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s t : Set α
f : α → β
inst✝ : Zero β
hst : s =ᵐ[μ] t
⊢ s.indicator f =ᵐ[μ] t.indicator f

Tactic:
classical exact piecewise_ae_eq_of_ae_eq_set hst

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

Goal state before:
pp: case refine_1.iUnion
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
f : ℕ → Set α
hs✝ : ∀ (n_1 : ℕ), MeasurableSet (f n_1)
h : ∀ (n_1 : ℕ), ∃ S, ↑S ⊆ memPartition t n ∧ f n_1 = ⋃₀ ↑S
⊢ ∃ S, ↑S ⊆ memPartition t n ∧ ⋃ i, f i = ⋃₀ ↑S

Tactic:
choose S hS_subset hS_eq using h

Goal state after:
case refine_1.iUnion
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
f : ℕ → Set α
hs✝ : ∀ (n_1 : ℕ), MeasurableSet (f n_1)
S : ℕ → Finset (Set α)
hS_subset : ∀ (n_1 : ℕ), ↑(S n_1) ⊆ memPartition t n
hS_eq : ∀ (n : ℕ), f n = ⋃₀ ↑(S n)
⊢ ∃ S, ↑S ⊆ memPartition t n ∧ ⋃ i, f i = ⋃₀ ↑S
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
s : Set ι
μ : ι → Measure α
⊢ ((sum fun i ↦ μ ↑i) + sum fun i ↦ μ ↑i) = sum μ

Tactic:
ext1 t ht
  simp only [add_apply, sum_apply _ ht]
  exact ENNReal.summable.tsum_add_tsum_compl (f := fun i => μ i t) ENNReal.summable

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 : ∀ (y : α), f' y ∈ t
hff' : f =ᵐ[μ] f'
⊢ AEMeasurable f μ

Tactic:
lift f' to α → t using hf't

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' : α → ↑t
hf'm : NullMeasurable (fun i ↦ ↑(f' i)) μ
hff' : f =ᵐ[μ] fun i ↦ ↑(f' i)
⊢ AEMeasurable f μ
Module: Mathlib.Topology.Separation.GDelta

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : T1Space X
hs : s.Countable
⊢ IsGδ sᶜ

Tactic:
rw [← biUnion_of_singleton s, compl_iUnion₂]
  exact .biInter hs fun x _ => .compl_singleton x

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

Goal state before:
pp: α✝ : Type u_1
M : Type u_2
α : Type u_3
inst✝⁵ : MeasurableSpace M
inst✝⁴ : MeasurableSpace α
inst✝³ : SMul M α
inst✝² : SMul Mᵐᵒᵖ α
inst✝¹ : IsCentralScalar M α
inst✝ : MeasurableSMul₂ M α
⊢ Measurable fun x ↦ unop x.1 • x.2

Tactic:
exact (measurable_mul_unop.comp measurable_fst).smul measurable_snd

Goal state after:
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 a) ≠ ∞

Tactic:
rw [← h a]
    finiteness

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
x : α
r : ℝ
h : x ∈ s
H : hausdorffDist s t < r
fin : hausdorffEDist s t ≠ ∞
r0 : 0 < r
⊢ hausdorffEDist s t < ENNReal.ofReal r

Tactic:
hausdorffDist,

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
x : α
r : ℝ
h : x ∈ s
H : (hausdorffEDist s t).toReal < r
fin : hausdorffEDist s t ≠ ∞
r0 : 0 < r
⊢ hausdorffEDist s t < ENNReal.ofReal r
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x y : α
⊢ hausdorffDist {x} {y} = dist x y

Tactic:
hausdorffDist,

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
⊢ (hausdorffEDist {x} {y}).toReal = dist x y
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric

Goal state before:
pp: α : Type u_1
inst✝² : PseudoEMetricSpace α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, μ (cthickening R s) ≠ ∞
A :
  Tendsto (fun r ↦ μ (cthickening r s)) (𝓝[>] 0)
    (𝓝 (μ (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)))
B :
  Tendsto (fun r ↦ μ (cthickening r s)) (𝓝[≤] 0)
    (𝓝 (μ (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)))
⊢ 𝓝 0 = 𝓝[≤] 0 ⊔ 𝓝[>] 0

Tactic:
exact (nhdsLE_sup_nhdsGT 0).symm

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

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

Tactic:
by
  simp_rw [NNReal.tsum_eq_toNNReal_tsum]
  exact (AEMeasurable.ennreal_tsum fun i => (h i).coe_nnreal_ennreal).ennreal_toNNReal

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : PseudoMetrizableSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
ι : Type u_3
inst✝¹ : Nonempty ι
μ : Measure α
f : ι → α → β
L : Filter ι
inst✝ : L.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n ↦ f n x) L (𝓝 l)
inhabited_h : Inhabited ι
hL : L.NeBot
f_lim : α → β := fun x ↦ if h : ∃ l, Tendsto (fun n ↦ f n x) L (𝓝 l) then h.choose else ⋯.some
h_ae_tendsto_f_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) L (𝓝 (f_lim x))
hf_lim : AEMeasurable f_lim μ
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) L (𝓝 (AEMeasurable.mk f_lim hf_lim x))

Tactic:
filter_upwards [h_ae_tendsto_f_lim, hf_lim.ae_eq_mk] with x hx h_eq

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : PseudoMetrizableSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
ι : Type u_3
inst✝¹ : Nonempty ι
μ : Measure α
f : ι → α → β
L : Filter ι
inst✝ : L.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n ↦ f n x) L (𝓝 l)
inhabited_h : Inhabited ι
hL : L.NeBot
f_lim : α → β := fun x ↦ if h : ∃ l, Tendsto (fun n ↦ f n x) L (𝓝 l) then h.choose else ⋯.some
h_ae_tendsto_f_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) L (𝓝 (f_lim x))
hf_lim : AEMeasurable f_lim μ
x : α
hx : Tendsto (fun n ↦ f n x) L (𝓝 (f_lim x))
h_eq : f_lim x = AEMeasurable.mk f_lim hf_lim x
⊢ Tendsto (fun n ↦ f n x) L (𝓝 (AEMeasurable.mk f_lim hf_lim x))
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: case hm
μ : Measure ℝ
inst✝ : IsFiniteMeasureOnCompacts μ
b r s : ℝ
_rpos : 0 < r
⊢ r ≤ s → Icc (b - r) (b + r) ⊆ Icc (b - s) (b + s)

Tactic:
hrs

Goal state after:
case hm
μ : Measure ℝ
inst✝ : IsFiniteMeasureOnCompacts μ
b r s : ℝ
_rpos : 0 < r
hrs : r ≤ s
⊢ Icc (b - r) (b + r) ⊆ Icc (b - s) (b + s)
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: case inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h₀ : ∫⁻ (a : α), f a ∂μ ≠ 0
⊢ ∃ g, Measurable g ∧ g ≤ f ∧ ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ

Tactic:
rcases exists_seq_strictMono_tendsto' h₀.bot_lt with ⟨L, _, hLf, hL_tendsto⟩

Goal state after:
case inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h₀ : ∫⁻ (a : α), f a ∂μ ≠ 0
L : ℕ → ℝ≥0∞
left✝ : StrictMono L
hLf : ∀ (n : ℕ), L n ∈ Ioo ⊥ (∫⁻ (a : α), f a ∂μ)
hL_tendsto : Tendsto L atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
⊢ ∃ g, Measurable g ∧ g ≤ f ∧ ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: α : 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
⊢ lintegral μ F ≤ ⨆ n, ∫⁻ (a : α), f n a ∂μ

Tactic:
lintegral_eq_nnreal

Goal state after:
α : 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
⊢ ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ ⨆ n, f n x), (SimpleFunc.map ofNNReal φ).lintegral μ ≤ ⨆ n, ∫⁻ (a : α), f n a ∂μ
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
H : AEMeasurable f μ
t_sep : IsSeparable ∅
ht : μ = 0
⊢ AEStronglyMeasurable f 0

Tactic:
exact aestronglyMeasurable_zero_measure f

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ∫⁻ (x : α), f x ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ φ,
    (∀ (x : α), ↑(φ x) ≤ f x) ∧
      ∀ (ψ : α →ₛ ℝ≥0), (∀ (x : α), ↑(ψ x) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε

Tactic:
lintegral_eq_nnreal

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ φ,
    (∀ (x : α), ↑(φ x) ≤ f x) ∧
      ∀ (ψ : α →ₛ ℝ≥0), (∀ (x : α), ↑(ψ x) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: case neg.e_a.e_6
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
g : α →ₛ ℝ≥0∞
hg : ⇑g ≤ fun a ↦ s.indicator f a
this : ⇑g ≤ f
x : α
H : x ∉ s
⊢ g x = 0

Tactic:
simpa [H] using hg x

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
f : α → β
mα : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : GroupWithZero β
inst✝¹ : ContinuousInv₀ β
inst✝ : MetrizableSpace β
hf : StronglyMeasurable f
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
x : α
this : MeasurableSet {x | f x ≠ 0}
h : ¬f x = 0
⊢ Tendsto (fun n ↦ ((fun n ↦ ((hf.approx n).restrict {x | f x ≠ 0})⁻¹) n) x) atTop (𝓝 (f⁻¹ x))

Tactic:
· simp_all only [ne_eq, measurableSet_setOfPred, SimpleFunc.coe_inv, SimpleFunc.coe_restrict,
      Pi.inv_apply, mem_ofPred_eq, not_false_eq_true, indicator_of_mem]
    apply (hf.tendsto_approx x).inv₀ h

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

Goal state before:
pp: case h_mono
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
⊢ Monotone fun n ↦ ⇑(eapprox f n) + ⇑(eapprox g n)

Tactic:
intro i j h a

Goal state after:
case h_mono
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
i j : ℕ
h : i ≤ j
a : α
⊢ (fun n ↦ ⇑(eapprox f n) + ⇑(eapprox g n)) i a ≤ (fun n ↦ ⇑(eapprox f n) + ⇑(eapprox g n)) j a
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
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this✝³ : MeasurableSpace β := borel β
this✝² : BorelSpace β
this✝¹ : MeasurableSpace γ := borel γ
this✝ : BorelSpace γ
⊢ (StronglyMeasurable fun x ↦ g (f x)) ↔ StronglyMeasurable f

Tactic:
refine
    ⟨fun H => stronglyMeasurable_iff_measurable_separable.2 ⟨?_, ?_⟩, fun H =>
      hg.continuous.comp_stronglyMeasurable H⟩

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : IsEmbedding g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this✝³ : MeasurableSpace β := borel β
this✝² : BorelSpace β
this✝¹ : MeasurableSpace γ := borel γ
this✝ : BorelSpace γ
H : StronglyMeasurable fun x ↦ g (f x)
⊢ Measurable f

case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : IsEmbedding g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this✝³ : MeasurableSpace β := borel β
this✝² : BorelSpace β
this✝¹ : MeasurableSpace γ := borel γ
this✝ : BorelSpace γ
H : StronglyMeasurable fun x ↦ g (f x)
⊢ IsSeparable (range f)
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: case h_mono
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
⊢ Monotone fun n ↦ ⇑(const α r * eapprox f n)

Tactic:
intro i j h a

Goal state after:
case h_mono
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
i j : ℕ
h : i ≤ j
a : α
⊢ (fun n ↦ ⇑(const α r * eapprox f n)) i a ≤ (fun n ↦ ⇑(const α r * eapprox f n)) j a
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSingletonClass α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
h : SecondCountableTopologyEither α β
f : α → β
s : Set α
hf : ContinuousOn f s
hs : sᶜ.Countable
h's : MeasurableSet s
this : f = fun x ↦ if hx : x ∈ s then f ↑⟨x, hx⟩ else f ↑⟨x, hx⟩
⊢ StronglyMeasurable fun x ↦ f ↑x

Tactic:
have := hs.to_subtype
    exact MeasureTheory.StronglyMeasurable.of_discrete

Goal state after:
Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
K' : (x : α) → x ∈ s → ℝ≥0
hK' : ∀ (x : α) (hx : x ∈ s), ∀ y ∈ s.diff (ball x (ε x hx)), edist (f x) (f y) ≤ ↑(K' x hx) * edist x y
t : Finset ↑s
ht : s ⊆ ⋃ x ∈ t, s ∩ ball (↑x) (ε ↑x ⋯ / 2)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
z : ↑s
hz : z ∈ t
hx' : x ∈ s ∩ ball (↑z) (ε ↑z ⋯ / 2)
hy' : y ∉ ball (↑z) (ε ↑z ⋯)
⊢ ↑(K ↑z ⋯) * ENNReal.ofReal (dist (↑z) x) + ↑(K' ↑z ⋯) * (ENNReal.ofReal (dist x ↑z) + ENNReal.ofReal (dist x y)) ≤
    ↑(K ↑z ⋯) * ENNReal.ofReal (dist x y) + ↑(K' ↑z ⋯) * (ENNReal.ofReal (dist x y) + ENNReal.ofReal (dist x y))

Tactic:
dist_comm _ x

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
K' : (x : α) → x ∈ s → ℝ≥0
hK' : ∀ (x : α) (hx : x ∈ s), ∀ y ∈ s.diff (ball x (ε x hx)), edist (f x) (f y) ≤ ↑(K' x hx) * edist x y
t : Finset ↑s
ht : s ⊆ ⋃ x ∈ t, s ∩ ball (↑x) (ε ↑x ⋯ / 2)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
z : ↑s
hz : z ∈ t
hx' : x ∈ s ∩ ball (↑z) (ε ↑z ⋯ / 2)
hy' : y ∉ ball (↑z) (ε ↑z ⋯)
⊢ ↑(K ↑z ⋯) * ENNReal.ofReal (dist x ↑z) + ↑(K' ↑z ⋯) * (ENNReal.ofReal (dist x ↑z) + ENNReal.ofReal (dist x y)) ≤
    ↑(K ↑z ⋯) * ENNReal.ofReal (dist x y) + ↑(K' ↑z ⋯) * (ENNReal.ofReal (dist x y) + ENNReal.ofReal (dist x y))
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: i j : ↑I
h : 0 < ↑i ∧ ↑j < 1
⊢ ↑j * ↑i < ↑i

Tactic:
simpa using mul_lt_mul_of_pos_right h.right h.left

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

Goal state before:
pp: case inl.inl
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
p q : X
h : Sum.dist (Sum.inl p) (Sum.inl q) = 0
⊢ Sum.inl p = Sum.inl q

pp: case inl.inr
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
p : X
q : Y
h : Sum.dist (Sum.inl p) (Sum.inr q) = 0
⊢ Sum.inl p = Sum.inr q

pp: case inr.inl
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
p : Y
q : X
h : Sum.dist (Sum.inr p) (Sum.inl q) = 0
⊢ Sum.inr p = Sum.inl q

pp: case inr.inr
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
p q : Y
h : Sum.dist (Sum.inr p) (Sum.inr q) = 0
⊢ Sum.inr p = Sum.inr q

Tactic:
· rw [eq_of_dist_eq_zero h]

Goal state after:
case inl.inr
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
p : X
q : Y
h : Sum.dist (Sum.inl p) (Sum.inr q) = 0
⊢ Sum.inl p = Sum.inr q

case inr.inl
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
p : Y
q : X
h : Sum.dist (Sum.inr p) (Sum.inl q) = 0
⊢ Sum.inr p = Sum.inl q

case inr.inr
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
p q : Y
h : Sum.dist (Sum.inr p) (Sum.inr q) = 0
⊢ Sum.inr p = Sum.inr q
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: case inr.inr
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
p q : Y
h : Sum.dist (Sum.inr p) (Sum.inr q) = 0
⊢ Sum.inr p = Sum.inr q

Tactic:
· rw [eq_of_dist_eq_zero h]

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

Goal state before:
pp: β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), (A l).Nonempty
x : ℕ → β
⊢ x ∈ (inducedMap A).fst

Tactic:
choose u hu using fun n => hnonempty (res x n)

Goal state after:
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), (A l).Nonempty
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
⊢ x ∈ (inducedMap A).fst
Module: Mathlib.Topology.MetricSpace.Perfect

Goal state before:
pp: case property
α : Type u_1
inst✝¹ : MetricSpace α
C : Set α
hC : Perfect C
hnonempty : C.Nonempty
inst✝ : CompleteSpace α
u : ℕ → ℝ≥0∞
upos' : ∀ (n : ℕ), u n ∈ Ioo 0 1
hu : Tendsto u atTop (nhds 0)
upos : ∀ (n : ℕ), 0 < u n
P : Type (max 0 u_1) := ⋯
C0 C1 : {C : Set α} → Perfect C → C.Nonempty → {ε : ℝ≥0∞} → 0 < ε → Set α
h0 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C0 hC hnonempty hε) ∧
      (C0 hC hnonempty hε).Nonempty ∧ C0 hC hnonempty hε ⊆ C ∧ ediam (C0 hC hnonempty hε) ≤ ε
h1 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C1 hC hnonempty hε) ∧
      (C1 hC hnonempty hε).Nonempty ∧ C1 hC hnonempty hε ⊆ C ∧ ediam (C1 hC hnonempty hε) ≤ ε
hdisj :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Disjoint (C0 hC hnonempty hε) (C1 hC hnonempty hε)
l : List Bool
ih : P
⊢ Perfect (C1 ⋯ ⋯ ⋯) ∧ (C1 ⋯ ⋯ ⋯).Nonempty

Tactic:
exact ⟨(h1 _ _ _).1, (h1 _ _ _).2.1⟩

Goal state after:
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 : (n : ℕ) → E n
hx : x ∉ s
n : ℕ
hn : longestPrefix x s < n
⊢ Disjoint s (cylinder x n)

Tactic:
by
  contrapose! hn
  rcases not_disjoint_iff_nonempty_inter.1 hn with ⟨y, ys, hy⟩
  apply le_trans _ (firstDiff_le_longestPrefix hs hx ys)
  apply (mem_cylinder_iff_le_firstDiff (ne_of_mem_of_not_mem ys hx).symm _).1
  rwa [mem_cylinder_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
f : α → β
inst✝ : IsProbabilityMeasure (map f μ)
hf : AEMeasurable f μ
⊢ μ univ = 1

Tactic:
rw [← Set.preimage_univ (f := f), ← map_apply_of_aemeasurable hf .univ]

Goal state after:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
f : α → β
inst✝ : IsProbabilityMeasure (map f μ)
hf : AEMeasurable f μ
⊢ (map f μ) univ = 1
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
a : α
s : Set α
hs : MeasurableSet s
ha : a ∉ s
⊢ (μ.restrict {a}) s = (μ {a} • dirac a) s

Tactic:
have : s ∩ {a} = ∅ := inter_singleton_eq_empty.2 ha

Goal state after:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
a : α
s : Set α
hs : MeasurableSet s
ha : a ∉ s
this : s ∩ {a} = ∅
⊢ (μ.restrict {a}) s = (μ {a} • dirac a) s
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
a : α
hs : MeasurableSet s
⊢ s ∈ ae (dirac a) ↔ a ∈ s

Tactic:
by
  by_cases a ∈ s <;> simp [mem_ae_iff, dirac_apply', hs.compl, *]

Goal state after: