mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
h : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs : s.Nonempty
⊢ x ∈ s ↔ infDist x s = 0

Tactic:
← mem_closure_iff_infDist_zero hs,

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
h : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs : s.Nonempty
⊢ x ∈ s ↔ x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Preorder β
s : Set α
f g : α →ₛ β
H : f ≤ g
⊢ f.restrict s ≤ g.restrict s

Tactic:
exact if hs : MeasurableSet s then fun x => by
    simp only [coe_restrict _ hs, indicator_le_indicator (H x)]
  else by simp only [restrict_of_not_measurable hs, le_refl]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
s : Set α
h : s.Countable
μ : Measure α
inst✝ : NullSingletonClass μ
⊢ μ s = 0

Tactic:
rw [← biUnion_of_singleton s, measure_biUnion_null_iff h]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
s : Set α
h : s.Countable
μ : Measure α
inst✝ : NullSingletonClass μ
⊢ ∀ i ∈ s, μ {i} = 0
Module: Mathlib.Topology.Instances.Real.Lemmas

Goal state before:
pp: K : Subfield ℝ
hc : IsClosed ↑K
⊢ ↑K = ↑⊤

Tactic:
Subfield.coe_top,

Goal state after:
K : Subfield ℝ
hc : IsClosed ↑K
⊢ ↑K = univ
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0∞
g : α → ℝ≥0∞
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : ∀ (x : α), Tendsto (fun i ↦ f i x) u (𝓝 (g x))
x : ℕ → ι
hx : Tendsto x atTop u
this : (fun y ↦ liminf (fun n ↦ f (x n) y) atTop) = g
⊢ Measurable fun y ↦ liminf (fun n ↦ f (x n) y) atTop

Tactic:
change Measurable fun y => liminf (fun n => (f (x n) y : ℝ≥0∞)) atTop

Goal state after:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0∞
g : α → ℝ≥0∞
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : ∀ (x : α), Tendsto (fun i ↦ f i x) u (𝓝 (g x))
x : ℕ → ι
hx : Tendsto x atTop u
this : (fun y ↦ liminf (fun n ↦ f (x n) y) atTop) = g
⊢ Measurable fun y ↦ liminf (fun n ↦ f (x n) y) atTop
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: case refine_1
β : Type u_6
mβ : MeasurableSpace β
f : EReal × EReal → β
h_real : Measurable fun p ↦ f (↑p.1, ↑p.2)
h_bot_left : Measurable fun r ↦ f (⊥, ↑r)
h_top_left : Measurable fun r ↦ f (⊤, ↑r)
h_bot_right : Measurable fun r ↦ f (↑r, ⊥)
h_top_right : Measurable fun r ↦ f (↑r, ⊤)
⊢ Measurable fun p ↦ f (↑p.1, p.2)

Tactic:
refine measurable_swap_iff.mp <| measurable_of_real_prod ?_ h_bot_right h_top_right

Goal state after:
case refine_1
β : Type u_6
mβ : MeasurableSpace β
f : EReal × EReal → β
h_real : Measurable fun p ↦ f (↑p.1, ↑p.2)
h_bot_left : Measurable fun r ↦ f (⊥, ↑r)
h_top_left : Measurable fun r ↦ f (⊤, ↑r)
h_bot_right : Measurable fun r ↦ f (↑r, ⊥)
h_top_right : Measurable fun r ↦ f (↑r, ⊤)
⊢ Measurable fun p ↦ ((fun p ↦ f (↑p.1, p.2)) ∘ Prod.swap) (↑p.1, p.2)
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case neg
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_5
ι' : Type u_6
f : ι → δ → α
v : Filter ι
hf : ∀ (i : ι), Measurable (f i)
p : ι' → Prop
s : ι' → Set ι
hv : v.HasCountableBasis p s
hs : ∀ (j : ι'), (s j).Countable
this✝ : Countable (Subtype p)
hp : Nonempty (Subtype p)
H : ¬∃ j, s ↑j = ∅
this : ∀ (i : ι'), Countable ↑(s i)
m : Subtype p → Set δ := fun j ↦ {x | BddBelow (range fun i ↦ f (↑i) x)}
m_meas : ∀ (j : Subtype p), MeasurableSet (m j)
mc_meas : MeasurableSet {x | ∀ (j : Subtype p), x ∉ m j}
j : Subtype p
reparam : δ → Subtype p → Subtype p := fun x ↦ liminfReparam (fun i ↦ f i x) s p
F0 : Subtype p → δ → α := fun j x ↦ ⨅ i, f (↑i) x
F0_meas : ∀ (j : Subtype p), Measurable (F0 j)
F1 : δ → α := fun x ↦ F0 (reparam x j) x
hF1 : F1 = fun x ↦ F0 (reparam x j) x
g : ℕ → Subtype p := Classical.choose ⋯
Z : ∀ (x : δ), ∃ n, x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k
⊢ Measurable F1

Tactic:
have : F1 = fun x ↦ if x ∈ m j then F0 j x else F0 (g (Nat.find (Z x))) x := by
    ext x
    have A : reparam x j = if x ∈ m j then j else g (Nat.find (Z x)) := rfl
    split_ifs with hjx
    · have : reparam x j = j := by rw [A, if_pos hjx]
      simp only [hF1, this]
    · have : reparam x j = g (Nat.find (Z x)) := by rw [A, if_neg hjx]
      simp only [hF1, this]

Goal state after:
case neg
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_5
ι' : Type u_6
f : ι → δ → α
v : Filter ι
hf : ∀ (i : ι), Measurable (f i)
p : ι' → Prop
s : ι' → Set ι
hv : v.HasCountableBasis p s
hs : ∀ (j : ι'), (s j).Countable
this✝¹ : Countable (Subtype p)
hp : Nonempty (Subtype p)
H : ¬∃ j, s ↑j = ∅
this✝ : ∀ (i : ι'), Countable ↑(s i)
m : Subtype p → Set δ := fun j ↦ {x | BddBelow (range fun i ↦ f (↑i) x)}
m_meas : ∀ (j : Subtype p), MeasurableSet (m j)
mc_meas : MeasurableSet {x | ∀ (j : Subtype p), x ∉ m j}
j : Subtype p
reparam : δ → Subtype p → Subtype p := fun x ↦ liminfReparam (fun i ↦ f i x) s p
F0 : Subtype p → δ → α := fun j x ↦ ⨅ i, f (↑i) x
F0_meas : ∀ (j : Subtype p), Measurable (F0 j)
F1 : δ → α := fun x ↦ F0 (reparam x j) x
hF1 : F1 = fun x ↦ F0 (reparam x j) x
g : ℕ → Subtype p := Classical.choose ⋯
Z : ∀ (x : δ), ∃ n, x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k
this : F1 = fun x ↦ if x ∈ m j then F0 j x else F0 (g (Nat.find ⋯)) x
⊢ Measurable F1
Module: Mathlib.MeasureTheory.Function.SimpleFuncDense

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : PseudoEMetricSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace β
f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
x : β
hx : f x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
this : Nonempty ↑s
⊢ Tendsto (fun n ↦ (approxOn f hf s y₀ h₀ n) x) atTop (𝓝 (f x))

Tactic:
← @Subtype.range_coe _ s,

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : PseudoEMetricSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace β
f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
x : β
hx : f x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (range Subtype.val)
this : Nonempty ↑s
⊢ Tendsto (fun n ↦ (approxOn f hf s y₀ h₀ n) x) atTop (𝓝 (f x))
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f (μ.restrict s)
hμf : μ {x | x ∈ s ∧ f x = ∞} ≠ 0
⊢ μ ({a | f a = ∞} ∩ s) ≤ (μ.restrict s) {x | f x = ∞}

Tactic:
exact Measure.le_restrict_apply _ _

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

Goal state before:

Tactic:
∫⁻ a, ⨅ b, f b a ∂μ
    _ = ∫⁻ a, ⨅ n, (f ∘ h_directed.sequence f) n a ∂μ := by simp only [this, Function.comp_apply]
    _ = ⨅ n, ∫⁻ a, (f ∘ h_directed.sequence f) n a ∂μ := by
      rw [lintegral_iInf ?_ h_directed.sequence_anti]
      · exact hf_int _
      · exact fun n => hf _
    _ = ⨅ b, ∫⁻ a, f b a ∂μ := by
      refine le_antisymm (le_iInf fun b => ?_) (le_iInf fun n => ?_)
      · exact iInf_le_of_le (Encodable.encode b + 1) (lintegral_mono <| h_directed.sequence_le b)
      · exact iInf_le (fun b => ∫⁻ a, f b a ∂μ) _

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
⊢ (⨆ g, ⨆ (_ : ⇑g ≤ fun a ↦ f a), g.lintegral μ) + ⨆ g_1, ⨆ (_ : ⇑g_1 ≤ fun a ↦ g a), g_1.lintegral μ ≤
    ⨆ g_1, ⨆ (_ : ⇑g_1 ≤ fun a ↦ f a + g a), g_1.lintegral μ

Tactic:
refine ENNReal.biSup_add_biSup_le' (p := fun h : α →ₛ ℝ≥0∞ => h ≤ f)
    (q := fun h : α →ₛ ℝ≥0∞ => h ≤ g) ⟨0, zero_le⟩ ⟨0, zero_le⟩ fun f' hf' g' hg' => ?_

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
f' : α →ₛ ℝ≥0∞
hf' : ⇑f' ≤ f
g' : α →ₛ ℝ≥0∞
hg' : ⇑g' ≤ g
⊢ f'.lintegral μ + g'.lintegral μ ≤ ⨆ g_1, ⨆ (_ : ⇑g_1 ≤ fun a ↦ f a + g a), g_1.lintegral μ
Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
⊢ MeasurableSet (μ.sigmaFiniteSetWRT ν)

Tactic:
by
  rw [Measure.sigmaFiniteSetWRT]
  split_ifs with h
  · exact h.choose_spec.1
  · exact MeasurableSet.empty

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

Goal state before:
pp: case e_f
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
a : α
⊢ r * f a = ⨆ n, (const α r * eapprox f n) a

Tactic:
← iSup_eapprox_apply hf,

Goal state after:
case e_f
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
a : α
⊢ r * ⨆ n, (eapprox f n) a = ⨆ n, (const α r * eapprox f n) a
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
        dsimp
        gcongr
        exact monotone_eapprox _ h _

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ ∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (a : α), f a ∂μ

Tactic:
have A : ∫⁻ a, f a ∂μ = ∫⁻ a, hf.mk f a ∂μ := lintegral_congr_ae hf.ae_eq_mk

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : AEMeasurable f μ
A : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), AEMeasurable.mk f hf a ∂μ
⊢ ∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (a : α), f a ∂μ
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: case neg
α : 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 : α
hx : x ∉ s
⊢ Tendsto (fun n ↦ ((fun n ↦ (hf.approx n).restrict s) n) x) atTop (𝓝 (f x))

Tactic:
· simpa [SimpleFunc.coe_restrict, hs, hx, hf_zero x hx] using tendsto_const_nhds

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

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

Tactic:
SimpleFunc.coe_smul

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

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

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

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
x : X
y : Y
⊢ 1 ≤ dist x ⋯.some + 1 + dist ⋯.some y

Tactic:
← le_add_of_nonneg_right dist_nonneg,

Goal state after:
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
x : X
y : Y
⊢ 1 ≤ dist x ⋯.some + 1
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: α : Type u_2
⊢ Injective res

Tactic:
intro x y h

Goal state after:
α : Type u_2
x y : ℕ → α
h : res x = res y
⊢ x = y
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
⊢ s ∈ 𝓤 (X ⊕ Y) ↔ ∃ ε > 0, ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s

Tactic:
constructor
  · rintro ⟨hsX, hsY⟩
    rcases mem_uniformity_dist.1 hsX with ⟨εX, εX0, hX⟩
    rcases mem_uniformity_dist.1 hsY with ⟨εY, εY0, hY⟩
    refine ⟨min (min εX εY) 1, lt_min (lt_min εX0 εY0) zero_lt_one, ?_⟩
    rintro (a | a) (b | b) h
    · exact hX (lt_of_lt_of_le h (le_trans (min_le_left _ _) (min_le_left _ _)))
    · cases not_le_of_gt (lt_of_lt_of_le h (min_le_right _ _)) Sum.one_le_dist_inl_inr
    · cases not_le_of_gt (lt_of_lt_of_le h (min_le_right _ _)) Sum.one_le_dist_inr_inl
    · exact hY (lt_of_lt_of_le h (le_trans (min_le_left _ _) (min_le_right _ _)))
  · rintro ⟨ε, ε0, H⟩
    constructor <;> rw [Filter.mem_map, mem_uniformity_dist] <;> exact ⟨ε, ε0, fun _ _ h => H _ _ h⟩

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

Goal state before:
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:
· exact eq_of_glueDist_eq_zero _ _ _ one_pos _ _ ((Sum.dist_eq_glueDist p q).symm.trans h)

Goal state after:
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 inl.inl
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x z y : E i
⊢ dist ⟨i, x⟩ ⟨i, z⟩ ≤ dist ⟨i, x⟩ ⟨i, y⟩ + dist ⟨i, y⟩ ⟨i, z⟩

Tactic:
simpa using dist_triangle x y z

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
t : TopologicalSpace α
t_le : t ≤ inst✝
t_polish : PolishSpace α
h : IsClosed[t] s
h' : IsOpen[t] s
⊢ IsClopenable sᶜ

Tactic:
exact ⟨t, t_le, t_polish, @IsOpen.isClosed_compl α t s h', @IsClosed.isOpen_compl α t s h⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
g : α → β
hg : MeasurePreserving g μ ν
hge : MeasurableEmbedding g
f : β → ℝ≥0∞
s : Set β
⊢ ∫⁻ (a : α) in g ⁻¹' s, f (g a) ∂μ = ∫⁻ (b : β) in s, f b ∂Measure.map g μ

Tactic:
hge.restrict_map,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
g : α → β
hg : MeasurePreserving g μ ν
hge : MeasurableEmbedding g
f : β → ℝ≥0∞
s : Set β
⊢ ∫⁻ (a : α) in g ⁻¹' s, f (g a) ∂μ = ∫⁻ (b : β), f b ∂Measure.map g (μ.restrict (g ⁻¹' s))
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability

Goal state before:
pp: case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : IsZeroOrProbabilityMeasure μ
p : ℝ≥0∞
hμs : p < μ s
s_mble : MeasurableSet s
h : IsProbabilityMeasure μ
⊢ 1 - μ s < 1 - p

Tactic:
apply ENNReal.sub_lt_of_sub_lt prob_le_one (Or.inl one_ne_top)

Goal state after:
case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : IsZeroOrProbabilityMeasure μ
p : ℝ≥0∞
hμs : p < μ s
s_mble : MeasurableSet s
h : IsProbabilityMeasure μ
⊢ 1 - (1 - p) < μ s
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : Countable ι
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
β : ι → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous[hβ n, inst✝¹] (f n)
f_range : ∀ (n : ι), range (f n) = s n
⊢ AnalyticSet (⋃ n, s n)

Tactic:
let γ := Σ n, β n

Goal state after:
α : Type u_1
ι : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : Countable ι
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
β : ι → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous[hβ n, inst✝¹] (f n)
f_range : ∀ (n : ι), range (f n) = s n
γ : Type (max u_2 0) := (n : ι) × β n
⊢ AnalyticSet (⋃ n, s n)
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: α : Type u_2
inst✝³ : MetricSpace α
inst✝² : CompleteSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := ⋯
g : ↑s → α := ⋯
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
y x : ↑s
hxy : dist x y < 1
hne : x ≠ y
hne' : ↑x ≠ ↑y
dist' : dist x y = dist ↑x ↑y
n : ℕ := ⋯
h : firstDiff ↑x ↑y ≤ 0
⊢ ↑x (firstDiff ↑x ↑y) = ↑y (firstDiff ↑x ↑y)

Tactic:
Nat.le_zero.1 h

Goal state after:
α : Type u_2
inst✝³ : MetricSpace α
inst✝² : CompleteSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x | (⋂ n, closedBall (u (x n)) ((1 / 2) ^ n)).Nonempty}
g : ↑s → α := fun x ↦ Set.Nonempty.some ⋯
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
y x : ↑s
hxy : dist x y < 1
hne : x ≠ y
hne' : ↑x ≠ ↑y
dist' : dist x y = dist ↑x ↑y
n : ℕ := firstDiff ↑x ↑y - 1
h : firstDiff ↑x ↑y ≤ 0
⊢ ↑x 0 = ↑y 0
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
mα : MeasurableSpace α✝
mβ : MeasurableSpace β
α : Type u_3
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ Measurable fun b ↦ (⇑b.1 + ⇑b.2) s

Tactic:
Pi.add_apply

Goal state after:
α✝ : Type u_1
β : Type u_2
mα : MeasurableSpace α✝
mβ : MeasurableSpace β
α : Type u_3
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ Measurable fun b ↦ b.1 s + b.2 s
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α → ℝ≥0
a_mble : Measurable a
a_summable : Summable a
c : ℝ≥0
tsum_le_c : ∑' (i : α), a i ≤ c
ε : ℝ≥0
ε_ne_zero : ε ≠ 0
⊢ ∑' (i : α), ↑(a i) = ↑(∑' (i : α), a i)

Tactic:
rw [ENNReal.tsum_coe_eq a_summable.hasSum]

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

Goal state before:
pp: E : ℕ → Type u_1
ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → PseudoEMetricSpace (F i)
⊢ uniformity ((i : ι) → F i) = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | edist p.1 p.2 < ε}

Tactic:
simp only [Pi.uniformity, comap_iInf, gt_iff_lt, preimage_ofPred_eq, comap_principal,
      PseudoEMetricSpace.uniformity_edist, le_antisymm_iff, le_iInf_iff, le_principal_iff]
    constructor
    · intro ε hε
      obtain ⟨K, hK⟩ : ∃ K : Finset ι, ∑' i : {j // j ∉ K}, 2⁻¹ ^ encode (i : ι) < ε / 2 :=
        ((tendsto_order.1 <| ENNReal.tendsto_tsum_compl_atTop_zero
          (tsum_geometric_encode_lt_top ENNReal.one_half_lt_one).ne).2 _
            <| by simpa using hε.ne').exists
      obtain ⟨δ, δpos, hδ⟩ : ∃ δ, 0 < δ ∧ δ * K.card < ε / 2 :=
        ENNReal.exists_pos_mul_lt (by simp) (by simpa using hε.ne')
      apply @mem_iInf_of_iInter _ _ _ _ _ K.finite_toSet fun i =>
          {p : (∀ i : ι, F i) × ∀ i : ι, F i | edist (p.fst i) (p.snd i) < δ}
      · rintro ⟨i, hi⟩
        refine mem_iInf_of_mem δ (mem_iInf_of_mem δpos ?_)
        simp only [mem_principal, Subset.rfl]
      · rintro ⟨x, y⟩ hxy
        simp only [mem_iInter, mem_ofPred_eq, SetCoe.forall, Finset.mem_coe] at hxy
        calc
          edist x y = ∑' i : ι, min (2⁻¹ ^ encode i) (edist (x i) (y i)) := rfl
          _ = ∑ i ∈ K, min (2⁻¹ ^ encode i) (edist (x i) (y i)) +
                ∑' i : ↑(K : Set ι)ᶜ, min (2⁻¹ ^ encode (i : ι)) (edist (x i) (y i)) :=
            (ENNReal.sum_add_tsum_compl ..).symm
          _ ≤ ∑ i ∈ K, edist (x i) (y i) + ∑' i : ↑(K : Set ι)ᶜ, 2⁻¹ ^ encode (i : ι) := by
            gcongr
            · apply min_le_right
            · apply min_le_left
          _ < ∑ _i ∈ K, δ + ε / 2 := by
            refine ENNReal.add_lt_add_of_le_of_lt (by simpa using fun i hi ↦ (hxy i hi).ne_top) ?_
              hK
            gcongr with i hi
            exact (hxy i hi).le
          _ ≤ ε / 2 + ε / 2 := by gcongr; simpa [mul_comm] using hδ.le
          _ = ε := ENNReal.add_halves _
    · intro i ε hε₀
      have : (0 : ℝ≥0∞) < 2⁻¹ ^ encode i := ENNReal.pow_pos (by norm_num) _
      refine mem_iInf_of_mem (min (2⁻¹ ^ encode i) ε) <| mem_iInf_of_mem (by positivity) ?_
      simp only [and_imp, Prod.forall, ofPred_subset_ofPred, lt_min_iff, mem_principal]
      intro x y hn
      exact (edist_le_edist_pi_of_edist_lt hn).trans_lt

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
⊢ map Prod.fst (μ.prod ν) = ν univ • μ

Tactic:
ext s hs
  simp [Measure.map_apply measurable_fst hs, ← prod_univ, mul_comm]

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

Goal state before:
pp: α : Type u_1
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : R1Space α
inst✝ : μ.OuterRegular
k : Set α
hk : IsCompact k
u : Set α
⊢ k ⊆ u → IsOpen[inst✝²] u → μ (closure[inst✝²] k) ≤ μ u

Tactic:
ku

Goal state after:
α : Type u_1
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : R1Space α
inst✝ : μ.OuterRegular
k : Set α
hk : IsCompact k
u : Set α
ku : k ⊆ u
⊢ IsOpen[inst✝²] u → μ (closure[inst✝²] k) ≤ μ u
Module: Mathlib.MeasureTheory.Group.Action

Goal state before:
pp: G : Type u
α : Type w
m : MeasurableSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
c : G
⊢ c • ae μ = ae μ

Tactic:
ext s
  simp only [mem_smul_filter, preimage_smul, smul_mem_ae]

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

Goal state before:
pp: G : Type u
α : Type w
m : MeasurableSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
c : G
s t : Set α
⊢ c • s =ᵐ[μ] c • t ↔ s =ᵐ[μ] t

Tactic:
simp only [Filter.eventuallyLE_antisymm_iff, smul_set_ae_le]

Goal state after: