mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Separation.GDelta

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
s t : Set X
inst✝ : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed[inst✝¹] t
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen[inst✝¹] t
T_count : T.Countable
T_int : t = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → ↑T
g_surj : Surjective g
n : ℕ
⊢ t ⊆ ↑(g n)

Tactic:
rw [T_int]

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
s t : Set X
inst✝ : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed[inst✝¹] t
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen[inst✝¹] t
T_count : T.Countable
T_int : t = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → ↑T
g_surj : Surjective g
n : ℕ
⊢ ⋂₀ T ⊆ ↑(g n)
Module: Mathlib.Topology.Separation.GDelta

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
s t : Set X
inst✝ : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed[inst✝¹] t
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen[inst✝¹] t
T_count : T.Countable
T_int : t = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → ↑T
g_surj : Surjective g
g' : ℕ → Set X
g'_open : ∀ (n : ℕ), IsOpen[inst✝¹] (g' n)
clt_sub_g' : ∀ (n : ℕ), t ⊆ g' n
clg'_sub_g : ∀ (n : ℕ), closure[inst✝¹] (g' n) ⊆ ↑(g n)
⊢ ⋂ i, closure[inst✝¹] (g' i) ⊆ t

Tactic:
rw [T_int]

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
s t : Set X
inst✝ : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed[inst✝¹] t
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen[inst✝¹] t
T_count : T.Countable
T_int : t = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → ↑T
g_surj : Surjective g
g' : ℕ → Set X
g'_open : ∀ (n : ℕ), IsOpen[inst✝¹] (g' n)
clt_sub_g' : ∀ (n : ℕ), t ⊆ g' n
clg'_sub_g : ∀ (n : ℕ), closure[inst✝¹] (g' n) ⊆ ↑(g n)
⊢ ⋂ i, closure[inst✝¹] (g' i) ⊆ ⋂₀ T
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ E ⊆ (thickening δ (thickening δ E)ᶜ)ᶜ

Tactic:
intro x x_in_E

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
x : α
x_in_E : x ∈ E
⊢ x ∈ (thickening δ (thickening δ E)ᶜ)ᶜ
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: case inl
α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
δ : ℝ
hδ : δ < 0
⊢ closedBall x δ ⊆ cthickening δ {x}

pp: case inr
α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
δ : ℝ
hδ : 0 ≤ δ
⊢ closedBall x δ ⊆ cthickening δ {x}

Tactic:
· simp only [closedBall_eq_empty.mpr hδ, empty_subset]

Goal state after:
case inr
α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
δ : ℝ
hδ : 0 ≤ δ
⊢ closedBall x δ ⊆ cthickening δ {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:
simp [infEDist_zero_of_mem h, infDist]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
t : Set α
x : α
Φ : α → β
hΦ : Isometry Φ
⊢ infDist (Φ x) (Φ '' t) = infDist x t

Tactic:
by
  simp [infDist, infEDist_image hΦ]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
cs : α
hcs : cs ∈ s
ct : α
hct : ct ∈ t
rs : ℝ
hrs : s ⊆ closedBall ct rs
rt : ℝ
hrt : t ⊆ closedBall cs rt
this : hausdorffEDist s t ≤ ENNReal.ofReal (max rs rt)
⊢ hausdorffEDist s t ≠ ∞

Tactic:
exact ne_top_of_le_ne_top ENNReal.ofReal_ne_top this

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s t u : Set α
fin : hausdorffEDist s t ≠ ∞
⊢ hausdorffDist s u ≤ hausdorffDist s t + hausdorffDist t u

Tactic:
refine toReal_le_add' hausdorffEDist_triangle (flip absurd fin) (not_imp_not.1 fun h ↦ ?_)

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s t u : Set α
fin : hausdorffEDist s t ≠ ∞
h : ¬hausdorffEDist s u = ∞
⊢ ¬hausdorffEDist t u = ∞
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case convert_4
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
f : δ → α
hf : ∀ (x : α), MeasurableSet (f ⁻¹' Iio x)
x : α
⊢ MeasurableSet (f ⁻¹' Iio x)

Tactic:
exact hf x

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

Goal state before:
pp: case convert_4
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
f : δ → α
hf : ∀ (x : α), MeasurableSet (f ⁻¹' Ioi x)
x : α
⊢ MeasurableSet (f ⁻¹' Ioi x)

Tactic:
exact hf x

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : MeasurableSpace α
f : α →ₛ β
g : β → γ
s : Set γ
⊢ g ∘ ⇑f ⁻¹' s = ⇑f ⁻¹' g ⁻¹' s

Tactic:
exact preimage_comp

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

Goal state before:
pp: case inl
α : Type u_1
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
M : α → α
hM : ∀ x ∈ s, x < M x
y : α → α
hy : ∀ x ∈ s, y x ∈ Ioi x
h'y : ∀ x ∈ s, Ioo x (y x) ⊆ s
x : α
hx : x ∈ s \ interior s
x' : α
hx' : x' ∈ s \ interior s
hxx' : x ≠ x'
h' : x < x'
⊢ Function.onFun Disjoint (fun x ↦ Ioo x (y x)) x x'

Tactic:
refine disjoint_left.2 fun z hz h'z => ?_

Goal state after:
case inl
α : Type u_1
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
M : α → α
hM : ∀ x ∈ s, x < M x
y : α → α
hy : ∀ x ∈ s, y x ∈ Ioi x
h'y : ∀ x ∈ s, Ioo x (y x) ⊆ s
x : α
hx : x ∈ s \ interior s
x' : α
hx' : x' ∈ s \ interior s
hxx' : x ≠ x'
h' : x < x'
z : α
hz : z ∈ (fun x ↦ Ioo x (y x)) x
h'z : z ∈ (fun x ↦ Ioo x (y x)) x'
⊢ False
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case inr
α : Type u_1
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
M : α → α
hM : ∀ x ∈ s, x < M x
y : α → α
hy : ∀ x ∈ s, y x ∈ Ioi x
h'y : ∀ x ∈ s, Ioo x (y x) ⊆ s
x : α
hx : x ∈ s \ interior s
x' : α
hx' : x' ∈ s \ interior s
hxx' : x ≠ x'
h' : x' < x
⊢ Function.onFun Disjoint (fun x ↦ Ioo x (y x)) x x'

Tactic:
refine disjoint_left.2 fun z hz h'z => ?_

Goal state after:
case inr
α : Type u_1
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
M : α → α
hM : ∀ x ∈ s, x < M x
y : α → α
hy : ∀ x ∈ s, y x ∈ Ioi x
h'y : ∀ x ∈ s, Ioo x (y x) ⊆ s
x : α
hx : x ∈ s \ interior s
x' : α
hx' : x' ∈ s \ interior s
hxx' : x ≠ x'
h' : x' < x
z : α
hz : z ∈ (fun x ↦ Ioo x (y x)) x
h'z : z ∈ (fun x ↦ Ioo x (y x)) x'
⊢ False
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: δ : Type u_4
mδ : MeasurableSpace δ
α : Type u_5
mα : MeasurableSpace α
inst✝ : ConditionallyCompleteLattice α
p : Prop
f : δ → α
hf : Measurable f
⊢ Measurable fun b ↦ ⨆ (_ : p), f b

Tactic:
by
  classical
  simp_rw [ciSup_eq_ite]
  split_ifs with h
  · exact hf
  · exact measurable_const

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Set α
hs : MeasurableSet s
x : α
hx : (f.restrict s) x ≠ 0
hxs : x ∉ s
⊢ (f.restrict s) x = 0

Tactic:
by simp [*]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
s : Set α
⊢ c * (μ.restrict s) univ = c * μ s

Tactic:
Measure.restrict_apply MeasurableSet.univ,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
s : Set α
⊢ c * μ (univ ∩ s) = c * μ s
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: x : Set ℝ
⊢ x ∈ ⋃ a, ⋃ b, ⋃ (_ : a < b), {Ioo ↑a ↑b} ↔ x ∈ {S | ∃ l u, ↑l < ↑u ∧ Ioo ↑l ↑u = S}

Tactic:
simp [eq_comm]

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∞
μ : Measure α
h : ∀ (i : ι), AEMeasurable (f i) μ
⊢ AEMeasurable (fun x ↦ ∑' (i : ι), f i x) μ

Tactic:
simp_rw [ENNReal.tsum_eq_iSup_sum]
  exact .iSup fun s ↦ Finset.aemeasurable_fun_sum s fun i _ => h i

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

Goal state before:
pp: case neg
α : 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)
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ), range ⇑f \ {0} = ↑s → motive f
f : α →ₛ γ
h : range ⇑f \ {0} = ↑(insert x s)
mx : MeasurableSet (⇑f ⁻¹' {x})
g : α →ₛ γ := piecewise (⇑f ⁻¹' {x}) mx 0 f
Pg : motive g
y : α
hy : y ∉ ⇑f ⁻¹' {x}
⊢ f y = (g + piecewise (⇑f ⁻¹' {x}) mx (SimpleFunc.const α x) (SimpleFunc.const α 0)) y

Tactic:
· simp [g, hy]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : PseudoEMetricSpace α
inst✝⁴ : OpensMeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : Zero α
inst✝¹ : Preorder α
f : β → α
hf : 0 ≤ f
hfm : Measurable f
inst✝ : SeparableSpace ↑(range f ∪ {0})
n : ℕ
x : β
⊢ f x ∈ Ici 0

Tactic:
exact hf x

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

Goal state before:
pp: case neg
α : 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
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ), range ⇑f \ {c} = ↑s → P f
f : α →ₛ γ
h : range ⇑f \ {c} = ↑(insert x s)
mx : MeasurableSet (⇑f ⁻¹' {x})
g : α →ₛ γ := piecewise (⇑f ⁻¹' {x}) mx (SimpleFunc.const α c) f
Pg : P g
y : α
hy : y ∉ ⇑f ⁻¹' {x}
⊢ f y = (piecewise (⇑f ⁻¹' {x})ᶜ ⋯ g (SimpleFunc.const α x)) y

Tactic:
· simp [g, hy]

Goal state after:
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✝³ : TopologicalSpace α
inst✝² : PseudoMetrizableSpace α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, inst✝³] f
h'f : HasCompactSupport f
this : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α
⊢ Measurable f

Tactic:
obtain ⟨u, -, u_pos, u_lim⟩ : ∃ u, StrictAnti u ∧ (∀ (n : ℕ), 0 < u n) ∧ Tendsto u atTop (𝓝 0) :=
    exists_seq_strictAnti_tendsto (0 : ℝ)

Goal state after:
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✝³ : TopologicalSpace α
inst✝² : PseudoMetrizableSpace α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, inst✝³] f
h'f : HasCompactSupport f
this : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
⊢ Measurable f
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace β
γ : Type u_5
mγ : MeasurableSpace γ
mα : MeasurableSpace α
f : γ → α
μ : Measure γ
hf : MeasurableEmbedding f
g : α → β
⊢ AEStronglyMeasurable (g ∘ f) μ → AEStronglyMeasurable g (Measure.map f μ)

Tactic:
rintro ⟨g₁, hgm₁, heq⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace β
γ : Type u_5
mγ : MeasurableSpace γ
mα : MeasurableSpace α
f : γ → α
μ : Measure γ
hf : MeasurableEmbedding f
g : α → β
g₁ : γ → β
hgm₁ : StronglyMeasurable g₁
heq : g ∘ f =ᵐ[μ] g₁
⊢ AEStronglyMeasurable g (Measure.map f μ)
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: α : Type u_5
β : Type u_6
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
mb : MeasurableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
μ : Measure α
f : α → β
s : Set β
hs : MeasurableSet s
h_nonempty : s.Nonempty
h_mem : ∀ᵐ (x : α) ∂μ, f x ∈ s
f' : α → β
hf' : StronglyMeasurable f'
hff' : f =ᵐ[μ] f'
⊢ StronglyMeasurable ((f' ⁻¹' s).piecewise f' fun x ↦ h_nonempty.some)

Tactic:
case =>

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

Goal state before:
pp: α : Type u_5
β : Type u_6
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
mb : MeasurableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
μ : Measure α
f : α → β
s : Set β
hs : MeasurableSet s
h_nonempty : s.Nonempty
h_mem : ∀ᵐ (x : α) ∂μ, f x ∈ s
f' : α → β
hf' : StronglyMeasurable f'
hff' : f =ᵐ[μ] f'
⊢ ∀ (x : α), (f' ⁻¹' s).piecewise f' (fun x ↦ h_nonempty.some) x ∈ s

Tactic:
case =>

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

Goal state before:
pp: α : Type u_5
β : Type u_6
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
mb : MeasurableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
μ : Measure α
f : α → β
s : Set β
hs : MeasurableSet s
h_nonempty : s.Nonempty
h_mem : ∀ᵐ (x : α) ∂μ, f x ∈ s
f' : α → β
hf' : StronglyMeasurable f'
hff' : f =ᵐ[μ] f'
⊢ f =ᵐ[μ] (f' ⁻¹' s).piecewise f' fun x ↦ h_nonempty.some

Tactic:
case =>

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

Goal state before:
pp: case refine_2
α : 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 : g =ᵐ[μ.restrict sᶜ] AEStronglyMeasurable.mk g hg
⊢ ∀ᵐ (x : α) ∂μ.restrict sᶜ,
    s.piecewise f g x = s.piecewise (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x

Tactic:
rw [Filter.EventuallyEq, ae_restrict_iff' hs.compl] at h

Goal state after:
case refine_2
α : 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ᶜ → g x = AEStronglyMeasurable.mk g hg x
⊢ ∀ᵐ (x : α) ∂μ.restrict sᶜ,
    s.piecewise f g x = s.piecewise (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : IsEmpty α
μ : Measure α
f : α → ℝ≥0∞
⊢ ∫⁻ (x : α), f x ∂μ = 0

Tactic:
have : Subsingleton (Measure α) := inferInstance

Goal state after:
α : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : IsEmpty α
μ : Measure α
f : α → ℝ≥0∞
this : Subsingleton (Measure α)
⊢ ∫⁻ (x : α), f x ∂μ = 0
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

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

Tactic:
Measure.restrict_apply MeasurableSet.univ,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
r : ℝ≥0∞
this : ∀ x ∈ {x | f x = r}, f x = r
⊢ r * μ (univ ∩ {x | f x = r}) = r * μ {x | f x = r}
Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : ν s ≠ 0
this : ∀ t ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ, s ⊆ t → MeasurableSet t → μ t = ∞
t : Set α
hts : s ⊆ t
ht : MeasurableSet t
hs_subset_t : s ⊆ t ∩ (μ.sigmaFiniteSetWRT' ν)ᶜ
⊢ μ (t ∩ (μ.sigmaFiniteSetWRT' ν)ᶜ) = ∞

Tactic:
exact this (t ∩ (μ.sigmaFiniteSetWRT' ν)ᶜ) Set.inter_subset_right hs_subset_t
      (ht.inter measurableSet_sigmaFiniteSetWRT'.compl)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
⊢ ∃ fs, (∀ (x : α), Tendsto (fun n ↦ (fs n) x) atTop (𝓝 (f x))) ∧ ∀ x ∉ s, ∀ (n : ℕ), (fs n) x = 0

Tactic:
refine ⟨fun n => (hf.approx n).restrict s, ?_, ?_⟩

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
⊢ ∀ (x : α), Tendsto (fun n ↦ ((fun n ↦ (hf.approx n).restrict s) n) x) atTop (𝓝 (f x))

case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
⊢ ∀ x ∉ s, ∀ (n : ℕ), ((fun n ↦ (hf.approx n).restrict s) n) x = 0
Module: Mathlib.Analysis.Normed.Group.FunctionSeries

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : TopologicalSpace β
f : α → β → F
hf : ∀ (i : α), Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f i)
hu : Summable u
hfu : ∀ (n : α) (x : β), ‖f n x‖ ≤ u n
⊢ Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ ∑' (n : α), f n x

Tactic:
simp_rw [← continuousOn_univ] at hf ⊢

Goal state after:
α : Type u_1
β : Type u_2
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : TopologicalSpace β
f : α → β → F
hu : Summable u
hfu : ∀ (n : α) (x : β), ‖f n x‖ ≤ u n
hf : ∀ (i : α), ContinuousOn (f i) univ
⊢ ContinuousOn (fun x ↦ ∑' (n : α), f n x) univ
Module: Mathlib.Analysis.Normed.Group.FunctionSeries

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : TopologicalSpace β
f : α → β → F
hu : Summable u
hfu : ∀ (n : α) (x : β), ‖f n x‖ ≤ u n
hf : ∀ (i : α), ContinuousOn (f i) univ
⊢ ContinuousOn (fun x ↦ ∑' (n : α), f n x) univ

Tactic:
exact continuousOn_tsum hf hu fun n x _ => hfu n x

Goal state after:
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c✝ d✝ : α
h : a ≤ b
c d : α
hdc : 0 ≤ c - d
⊢ a - a ≤ c - d

Tactic:
rwa [sub_self]

Goal state after:
Module: Mathlib.Topology.Metrizable.CompletelyMetrizable

Goal state before:
pp: X : Type u_3
ht : TopologicalSpace X
h : IsCompletelyPseudoMetrizableSpace X
⊢ CompleteSpace X

Tactic:
by
  convert! h.complete.choose_spec.2
  exact PseudoMetricSpace.replaceTopology_eq _ _

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

Goal state before:
pp: E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
⊢ y ∈ cylinder x n ↔ x ∈ cylinder y n

Tactic:
simp [eq_comm]

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

Goal state before:
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

Tactic:
exact eq_of_glueDist_eq_zero _ _ _ one_pos _ _ ((Sum.dist_eq_glueDist q p).symm.trans h)

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

Goal state before:
pp: case inl.inr
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
z : E i
hij : i ≠ j
⊢ dist ⟨i, x⟩ ⟨i, z⟩ ≤ dist ⟨i, x⟩ ⟨j, y⟩ + dist ⟨j, y⟩ ⟨i, z⟩

Tactic:
simp only [Sigma.dist_same, Sigma.dist_ne hij, Sigma.dist_ne hij.symm]
      calc
        dist x z ≤ dist x (Nonempty.some ⟨x⟩) + 0 + 0 + (0 + 0 + dist (Nonempty.some ⟨z⟩) z) := by
          simpa only [zero_add, add_zero] using dist_triangle _ _ _
        _ ≤ _ := by apply_rules [add_le_add, le_rfl, dist_nonneg, zero_le_one]

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

Goal state before:
pp: case refine_1.h₁
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n := ⋯
fs : ∀ x ∈ s, f x = x
⊢ range f ⊆ s

pp: case refine_1.h₂
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n := ⋯
fs : ∀ x ∈ s, f x = x
⊢ s ⊆ range f

Tactic:
· rintro x ⟨y, rfl⟩
      by_cases hy : y ∈ s
      · rwa [fs y hy]
      simpa [f, if_neg hy] using! (inter_cylinder_longestPrefix_nonempty hs hne y).choose_spec.1

Goal state after:
case refine_1.h₂
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n := ⋯
fs : ∀ x ∈ s, f x = x
⊢ s ⊆ range f
Module: Mathlib.MeasureTheory.Measure.MutuallySingular

Goal state before:
pp: case refine_1
α : Type u_1
m0 : MeasurableSpace α
ν : Measure α
ι : Type u_2
inst✝ : Countable ι
μ : ι → Measure α
s : ι → Set α
hsm : ∀ (i : ι), MeasurableSet (s i)
hsμ : ∀ (i : ι), (μ i) (s i) = 0
hsν : ∀ (i : ι), ν (s i)ᶜ = 0
⊢ (sum μ) (⋂ i, s i) = 0

Tactic:
rw [sum_apply _ (MeasurableSet.iInter hsm), ENNReal.tsum_eq_zero]
    exact fun i => measure_mono_null (iInter_subset _ _) (hsμ i)

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

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s : Set α
h✝ : NeZero μ
h : μ univ = ∞
⊢ IsZeroOrProbabilityMeasure ((μ univ)⁻¹ • μ)

Tactic:
simp [h]; infer_instance

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : Measurable f
a : α
⊢ map f (dirac a) = dirac (f a)

Tactic:
classical
  exact ext fun s hs => by simp [hs, map_apply hf hs, hf hs, indicator_apply]

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
f : X → Y
hf : Continuous[inst✝³, inst✝²] f
Z : Type
w✝¹ : TopologicalSpace Z
w✝ : PolishSpace Z
g : Z → Y
hg : Continuous[w✝¹, inst✝²] g
hs : AnalyticSet (range g)
this : IsClosed[instTopologicalSpaceProd] {x | f x.1 = g x.2}
x : X
⊢ x ∈ f ⁻¹' range g ↔ x ∈ Prod.fst '' {x | f x.1 = g x.2}

Tactic:
simp [eq_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
⊢ Measurable fun μ ↦ map f μ

Tactic:
refine measurable_of_measurable_coe _ fun s hs => ?_

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ Measurable fun b ↦ (map f b) s