mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: case hf
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∀ (n : ℕ), Measurable ⇑(eapprox f n)

Tactic:
fun_prop

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

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

Tactic:
simp_all only [ne_eq, SimpleFunc.coe_div, SimpleFunc.coe_restrict,
      Pi.div_apply, mem_ofPred_eq, not_false_eq_true, indicator_of_mem]

Goal state after:
case neg
α : Type u_1
β : Type u_2
f g : α → β
mα : MeasurableSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : GroupWithZero β
inst✝² : ContinuousMul β
inst✝¹ : ContinuousInv₀ β
inst✝ : MetrizableSpace β
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
x : α
this : MeasurableSet {x | ¬g x = 0}
h : ¬g x = 0
⊢ Tendsto (fun n ↦ (hf.approx n) x / (hg.approx n) x) atTop (𝓝 (f x / g x))
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

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

Tactic:
fun_prop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
m : MeasurableSpace α
n : MeasurableSpace β
ι : Type u_6
f : ι → α → β → M
g : α → β
s : Finset ι
hf : ∀ i ∈ s, StronglyMeasurable ↿(f i)
hg : Measurable g
⊢ StronglyMeasurable fun a ↦ ∏ c ∈ s, f c a (g a)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
⊢ SigmaFinite (μ.restrict (μ.sigmaFiniteSetWRT' ν))

Tactic:
have := sigmaFinite_restrict_sigmaFiniteSetGE μ ν

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
this : ∀ (n : ℕ), SigmaFinite (μ.restrict (μ.sigmaFiniteSetGE ν n))
⊢ SigmaFinite (μ.restrict (μ.sigmaFiniteSetWRT' ν))
Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
ι : Type u_2
l : Filter ι
inst✝ : l.IsCountablyGenerated
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) l (𝓝 (f a))
⊢ ∀ (a : ι), Measurable (F a) → AEMeasurable (F a) μ

Tactic:
fun_prop

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
a b : α
h : a ≤ b
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
⊢ Continuous[inst✝¹, inst✝¹] fun x ↦ max a (min b x)

Tactic:
fun_prop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
x : α
r : ℝ
hr : 0 < r
K : ℝ
h : ∀ (y : α), dist y x < r → dist (f y) (f x) ≤ K * dist y x
⊢ Continuous fun a ↦ K * dist a x

Tactic:
fun_prop

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)
x : α
hx : x ∈ s
⊢ ContinuousOn (fun y ↦ dist (f x) (f y)) s

Tactic:
fun_prop

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)
x : α
hx : x ∈ s
⊢ ContinuousOn (dist x) (s \ ball x (ε x hx))

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: ⊢ Continuous fun x ↦ 1 - ↑x

Tactic:
fun_prop

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

Goal state before:
pp: X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
x : X
y z : Y
⊢ (⨅ p, dist x (Φ p) + dist z (Ψ p)) + ε ≤ (⨅ p, dist x (Φ p) + dist y (Ψ p)) + ε + dist y z

Tactic:
add_right_comm,

Goal state after:
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
x : X
y z : Y
⊢ (⨅ p, dist x (Φ p) + dist z (Ψ p)) + ε ≤ (⨅ p, dist x (Φ p) + dist y (Ψ p)) + dist y z + ε
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: a b : ℝ
x y : ↑(Icc a b)
⊢ Continuous fun t ↦ ⟨(1 - ↑t) * ↑x + ↑t * ↑y, ⋯⟩

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: a b : ℝ
⊢ Continuous fun x ↦ ⟨(1 - ↑x.2.2) * ↑x.1 + ↑x.2.2 * ↑x.2.1, ⋯⟩

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: case neg
a b : ℝ
x y z : ↑(Icc a b)
hxy : x ≤ y
hyz : y ≤ z
h : ¬↑z - ↑x = 0
⊢ ↑y = (1 - (↑y - ↑x) / (↑z - ↑x)) * ↑x + (↑y - ↑x) / (↑z - ↑x) * ↑z

Tactic:
field_simp
    ring_nf

Goal state after:
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⟩

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:
· simpa using dist_triangle x y z

Goal state after:
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⟩
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: ⊢ Continuous fun i ↦ ⟨↑i, ⋯⟩

Tactic:
fun_prop

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)
x : (n : ℕ) → E n
n : ℕ
⊢ IsOpen[Pi.topologicalSpace] (cylinder x n)

Tactic:
rw [PiNat.cylinder_eq_pi]
  exact isOpen_set_pi (Finset.range n).finite_toSet fun a _ => isOpen_discrete _

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

Goal state before:
pp: case h_nhds
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x : (n : ℕ) → E n
u : Set ((n : ℕ) → E n)
hx : x ∈ u
u_open : IsOpen[Pi.topologicalSpace] u
U : (i : ℕ) → Set (E i)
F : Finset ℕ
xU : x ∈ (↑F).pi U
Uu : (↑F).pi U ⊆ u
n : ℕ
hn : n ∈ upperBounds ↑F
y : (n : ℕ) → E n
hy : y ∈ cylinder x (n + 1)
i : ℕ
hi : i ∈ F
this : y i = x i
⊢ x i ∈ U i

Tactic:
simp only [Set.mem_pi, Finset.mem_coe] at xU

Goal state after:
case h_nhds
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x : (n : ℕ) → E n
u : Set ((n : ℕ) → E n)
hx : x ∈ u
u_open : IsOpen[Pi.topologicalSpace] u
U : (i : ℕ) → Set (E i)
F : Finset ℕ
Uu : (↑F).pi U ⊆ u
n : ℕ
hn : n ∈ upperBounds ↑F
y : (n : ℕ) → E n
hy : y ∈ cylinder x (n + 1)
i : ℕ
hi : i ∈ F
this : y i = x i
xU : ∀ i ∈ F, x i ∈ U i
⊢ x i ∈ U i
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case refine_2.inr.inr
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 := fun x ↦ if x ∈ s then x else ⋯.some
fs : ∀ x ∈ s, f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
⊢ dist (f x) (f y) ≤ dist x y

Tactic:
suffices firstDiff x y ≤ firstDiff (f x) (f y) by
      simpa [dist_eq_of_ne hxy, dist_eq_of_ne hfxfy]

Goal state after:
case refine_2.inr.inr
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 := fun x ↦ if x ∈ s then x else ⋯.some
fs : ∀ x ∈ s, f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
⊢ firstDiff x y ≤ firstDiff (f x) (f y)
Module: Mathlib.Topology.MetricSpace.Perfect

Goal state before:
pp: case refine_2
α : 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ε)
DP : List Bool → P := ⋯
D : List Bool → Set α := ⋯
hanti : ClosureAntitone D
hdiam : VanishingDiam D
hdisj' : CantorScheme.Disjoint D
hdom : ∀ {x : ℕ → Bool}, x ∈ (inducedMap D).fst
⊢ Continuous fun x ↦ ⟨x, ⋯⟩

Tactic:
fun_prop

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
ε : ℝ≥0
hε : 0 < ε
h₁ : sInf {m | ∃ t, m = μ t + ν tᶜ} = 0
h₂ : ∀ (n : ℕ), ∃ t, μ t + ν tᶜ < ↑ε * (1 / 2) ^ n
⊢ ∃ s, μ s = 0 ∧ ν sᶜ ≤ 2 * ↑ε

Tactic:
choose t ht₂ using h₂

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
ε : ℝ≥0
hε : 0 < ε
h₁ : sInf {m | ∃ t, m = μ t + ν tᶜ} = 0
t : ℕ → Set α
ht₂ : ∀ (n : ℕ), μ (t n) + ν (t n)ᶜ < ↑ε * (1 / 2) ^ n
⊢ ∃ s, μ s = 0 ∧ ν sᶜ ≤ 2 * ↑ε
Module: Mathlib.MeasureTheory.Measure.MutuallySingular

Goal state before:
pp: case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
ε : ℝ≥0
hε : 0 < ε
h₁ : sInf {m | ∃ t, m = μ t + ν tᶜ} = 0
t : ℕ → Set α
ht₂ : ∀ (n : ℕ), μ (t n) + ν (t n)ᶜ < ↑ε * (1 / 2) ^ n
⊢ ν (⋂ n, t n)ᶜ ≤ 2 * ↑ε

Tactic:
rw [compl_iInter, (by simp [ENNReal.tsum_mul_left, mul_comm] :
      2 * (ε : ℝ≥0∞) = ∑' (n : ℕ), ε * (1 / 2 : ℝ≥0∞) ^ n)]

Goal state after:
case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
ε : ℝ≥0
hε : 0 < ε
h₁ : sInf {m | ∃ t, m = μ t + ν tᶜ} = 0
t : ℕ → Set α
ht₂ : ∀ (n : ℕ), μ (t n) + ν (t n)ᶜ < ↑ε * (1 / 2) ^ n
⊢ ν (⋃ i, (t i)ᶜ) ≤ ∑' (n : ℕ), ↑ε * (1 / 2) ^ n
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
μ : Measure α
⊢ ∃ s, μ = sum fun x ↦ μ (measurableAtom ↑x) • dirac ↑x

Tactic:
let measurableAtoms := measurableAtom '' (Set.univ : Set α)
  have h_nonempty (s : measurableAtoms) : Set.Nonempty s.1 := by
    obtain ⟨y, _, hy⟩ := s.2
    rw [← hy]
    exact ⟨y, mem_measurableAtom_self y⟩
  let points : measurableAtoms → α := fun s ↦ (h_nonempty s).some
  have h_points_mem (s : measurableAtoms) : points s ∈ s.1 := (h_nonempty s).some_mem
  refine ⟨Set.range points, ext_of_measurableAtoms fun x ↦ ?_⟩
  rw [sum_apply _ (MeasurableSet.measurableAtom_of_countable x)]
  simp only [Measure.smul_apply, smul_eq_mul]
  simp_rw [dirac_apply' _ (MeasurableSet.measurableAtom_of_countable x)]
  rw [tsum_eq_single ⟨points ⟨measurableAtom x, by simp [measurableAtoms]⟩, by simp⟩]
  · rw [indicator_of_mem]
    · simp only [Pi.one_apply, mul_one]
      congr 1
      refine (measurableAtom_eq_of_mem ?_).symm
      convert! h_points_mem _
      simp
    · convert! h_points_mem _
      simp
  · simp only [ne_eq, mul_eq_zero, indicator_apply_eq_zero, Pi.one_apply, one_ne_zero, imp_false,
      Subtype.forall, Set.mem_range, Subtype.exists, Subtype.mk.injEq, forall_exists_index]
    refine fun y s hs hsy hyx ↦ .inr fun hyx' ↦ hyx ?_
    rw [← hsy]
    congr
    have h1 : measurableAtom y = measurableAtom x := measurableAtom_eq_of_mem hyx'
    have h2 : measurableAtom y = s := by
      specialize h_points_mem ⟨s, hs⟩
      obtain ⟨z, _, hz⟩ := hs
      simp only at h_points_mem
      rw [← hz, ← hsy]
      refine measurableAtom_eq_of_mem ?_
      convert! h_points_mem
    rw [← h2, h1]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass α
inst✝ : MeasurableSingletonClass β
f : α → β
a : α
s : Set β
hs : MeasurableSet s
⊢ AEMeasurable f (dirac a)

Tactic:
fun_prop

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

Goal state before:
pp: X : Type u_3
Y : Type u_4
inst✝⁵ : MeasurableSpace X
inst✝⁴ : StandardBorelSpace X
inst✝³ : TopologicalSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : OpensMeasurableSpace Y
f : X → Y
inst✝ : SecondCountableTopology ↑(range f)
s : Set X
hs : MeasurableSet s
hf : Measurable f
this : UpgradedStandardBorel X := upgradeStandardBorel X
τ' : TopologicalSpace X
hle : τ' ≤ this.toTopologicalSpace
hfc : Continuous[τ', inst✝³] f
hτ' : PolishSpace X
m' : MeasurableSpace X := borel X
⊢ AnalyticSet (f '' s)

Tactic:
have b' : BorelSpace X := ⟨rfl⟩

Goal state after:
X : Type u_3
Y : Type u_4
inst✝⁵ : MeasurableSpace X
inst✝⁴ : StandardBorelSpace X
inst✝³ : TopologicalSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : OpensMeasurableSpace Y
f : X → Y
inst✝ : SecondCountableTopology ↑(range f)
s : Set X
hs : MeasurableSet s
hf : Measurable f
this : UpgradedStandardBorel X := upgradeStandardBorel X
τ' : TopologicalSpace X
hle : τ' ≤ this.toTopologicalSpace
hfc : Continuous[τ', inst✝³] f
hτ' : PolishSpace X
m' : MeasurableSpace X := borel X
b' : BorelSpace X
⊢ AnalyticSet (f '' s)
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → ℝ≥0∞
hf : Measurable f
μ : Measure β
s : Set β
hs : MeasurableSet s
⊢ Measurable fun b ↦ f b * μ s

Tactic:
fun_prop

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
⊢ join 0 = 0

Tactic:
by
  ext1 s hs
  simp [hs]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ✝ : Measure α
f : α → ℝ≥0∞
μ : Measure α
inst✝ : SFinite μ
h : IsFiniteMeasure μ
g : ℕ → α → ℝ≥0∞
hgm : ∀ (n : ℕ), Measurable (g n)
hgf : ∀ (n : ℕ), g n ≤ f
hgle : ∀ (n : ℕ), g n ≤ ↑n
hgint : ∀ (n : ℕ), ∫⁻ (a : α), min (f a) ↑n ∂μ = ∫⁻ (a : α), g n a ∂μ
φ : α → ℝ≥0∞ := fun x ↦ ⨆ n, g n x
⊢ Measurable φ

Tactic:
fun_prop

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f✝ : α → ℝ≥0∞
hfm : Measurable f✝
s : ℕ → Finset ℝ≥0∞
f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞
hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)
hm : Monotone fun n μ ↦ ∑ r ∈ s n, r * f n r μ
⊢ ∀ (n : ℕ), Measurable fun μ ↦ ∑ r ∈ s n, r * f n r μ

Tactic:
fun_prop

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

Goal state before:
pp: case right
E : ℕ → Type u_1
ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → PseudoEMetricSpace (F i)
⊢ ∀ (i : ι) (i_1 : ℝ≥0∞), 0 < i_1 → {a | edist (a.1 i) (a.2 i) < i_1} ∈ ⨅ ε, ⨅ (_ : 0 < ε), 𝓟 {p | edist p.1 p.2 < ε}

Tactic:
intro i ε hε₀

Goal state after:
case right
E : ℕ → Type u_1
ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → PseudoEMetricSpace (F i)
i : ι
ε : ℝ≥0∞
hε₀ : 0 < ε
⊢ {a | edist (a.1 i) (a.2 i) < ε} ∈ ⨅ ε, ⨅ (_ : 0 < ε), 𝓟 {p | edist p.1 p.2 < ε}
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: ι : Type u_2
X : Type u_3
Y : ι → Type u_4
f : (i : ι) → X → Y i
inst✝² : Encodable ι
inst✝¹ : (i : ι) → PseudoMetricSpace (Y i)
inst✝ : TopologicalSpace X
continuous_f : ∀ (i : ι), Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f i)
⊢ ∀ (i : ι), Continuous[instTopologicalSpaceProd, _] fun x ↦ min (2⁻¹ ^ encode i) (dist (f i x.1) (f i x.2))

Tactic:
fun_prop

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

Goal state before:
pp: M : Type u_1
inst✝³ : Monoid M
inst✝² : MeasurableSpace M
inst✝¹ : MeasurableMul₂ M
μ ν : Measure M
inst✝ : SFinite ν
f : M → ℝ≥0∞
hf : Measurable f
⊢ AEMeasurable (fun z ↦ f (z.1 * z.2)) (μ.prod ν)

Tactic:
fun_prop

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

Goal state before:
pp: M : Type u_1
inst✝³ : Monoid M
inst✝² : MeasurableSpace M
inst✝¹ : MeasurableMul₂ M
x : M
μ : Measure M
inst✝ : SFinite μ
⊢ Measurable fun x ↦ x.1 * x.2

Tactic:
fun_prop

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

Goal state before:
pp: M : Type u_1
inst✝³ : Monoid M
inst✝² : MeasurableSpace M
inst✝¹ : MeasurableMul₂ M
x : M
μ : Measure M
inst✝ : SFinite μ
⊢ Measurable (Prod.mk x)

Tactic:
fun_prop

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

Goal state before:
pp: M : Type u_1
inst✝³ : Monoid M
inst✝² : MeasurableSpace M
inst✝¹ : MeasurableMul₂ M
μ : Measure M
inst✝ : SFinite μ
x : M
⊢ Measurable fun x ↦ x.1 * x.2

Tactic:
fun_prop

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

Goal state before:
pp: M : Type u_1
inst✝³ : Monoid M
inst✝² : MeasurableSpace M
inst✝¹ : MeasurableMul₂ M
μ : Measure M
inst✝ : SFinite μ
x : M
⊢ Measurable fun x_1 ↦ (x_1, x)

Tactic:
fun_prop

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

Goal state before:
pp: M : Type u_1
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
x y : M
⊢ Measurable fun y_1 ↦ y_1 * y

Tactic:
fun_prop

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

Goal state before:
pp: case hf
M : Type u_1
inst✝⁵ : Monoid M
inst✝⁴ : MeasurableSpace M
inst✝³ : MeasurableMul₂ M
μ ν ρ : Measure M
inst✝² : SFinite μ
inst✝¹ : SFinite ν
inst✝ : SFinite ρ
⊢ Measurable fun x ↦ x.1 * x.2

Tactic:
fun_prop

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

Goal state before:
pp: M : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν : Measure M
inst✝¹ : SFinite μ
inst✝ : SFinite ν
⊢ Measurable fun x ↦ x.1 * x.2

Tactic:
fun_prop

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

Goal state before:
pp: M : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν : Measure M
inst✝¹ : SFinite μ
inst✝ : SFinite ν
⊢ Measurable Prod.swap

Tactic:
fun_prop

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

Goal state before:
pp: M : Type u_1
inst✝⁴ : Monoid M
inst✝³ : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν ρ : Measure M
inst✝¹ : SFinite ν
inst✝ : SFinite ρ
f : M → ℝ≥0∞
hf : Measurable f
⊢ Measurable f

Tactic:
fun_prop

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

Goal state before:
pp: M : Type u_1
inst✝⁴ : Monoid M
inst✝³ : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν ρ : Measure M
inst✝¹ : SFinite ν
inst✝ : SFinite ρ
f : M → ℝ≥0∞
hf : Measurable f
⊢ Measurable fun x ↦ ∫⁻ (y : M), f (x * y) ∂ρ

Tactic:
fun_prop

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

Goal state before:
pp: M : Type u_1
inst✝⁴ : Monoid M
inst✝³ : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν ρ : Measure M
inst✝¹ : SFinite ν
inst✝ : SFinite ρ
f : M → ℝ≥0∞
hf : Measurable f
x : M
⊢ Measurable fun y ↦ f (x * y)

Tactic:
fun_prop

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

Goal state before:
pp: M : Type u_1
inst✝⁴ : Monoid M
inst✝³ : MeasurableSpace M
μ ν : Measure M
inst✝² : MeasurableMul₂ M
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
⊢ AEMeasurable (fun x ↦ x.1 * x.2) (μ.prod ν)

Tactic:
fun_prop

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

Goal state before:
pp: M : Type u_1
inst✝⁴ : Monoid M
inst✝³ : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν ρ : Measure M
inst✝¹ : ρ.IsMulLeftInvariant
inst✝ : SFinite ν
hν : ν ≪ ρ
s : Set M
hs : MeasurableSet s
h : ρ s = 0
x : M
⊢ Measurable (HMul.hMul x)

Tactic:
fun_prop

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

Goal state before:
pp: M : Type u_2
M' : Type u_3
mM : MeasurableSpace M
inst✝⁵ : Monoid M
inst✝⁴ : MeasurableMul₂ M
mM' : MeasurableSpace M'
inst✝³ : Monoid M'
inst✝² : MeasurableMul₂ M'
μ ν : Measure M
inst✝¹ : SFinite μ
inst✝ : SFinite ν
L : M →* M'
hL : Measurable ⇑L
⊢ Measurable ⇑L

Tactic:
fun_prop

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

Goal state before:
pp: M : Type u_2
M' : Type u_3
mM : MeasurableSpace M
inst✝⁵ : Monoid M
inst✝⁴ : MeasurableMul₂ M
mM' : MeasurableSpace M'
inst✝³ : Monoid M'
inst✝² : MeasurableMul₂ M'
μ ν : Measure M
inst✝¹ : SFinite μ
inst✝ : SFinite ν
L : M →* M'
hL : Measurable ⇑L
⊢ Measurable fun x ↦ x.1 * x.2

Tactic:
fun_prop

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

Goal state before:
pp: M : Type u_2
M' : Type u_3
mM : MeasurableSpace M
inst✝⁵ : Monoid M
inst✝⁴ : MeasurableMul₂ M
mM' : MeasurableSpace M'
inst✝³ : Monoid M'
inst✝² : MeasurableMul₂ M'
μ ν : Measure M
inst✝¹ : SFinite μ
inst✝ : SFinite ν
L : M →* M'
hL : Measurable ⇑L
this : (⇑L ∘ fun p ↦ p.1 * p.2) = (fun p ↦ p.1 * p.2) ∘ Prod.map ⇑L ⇑L
⊢ Measurable fun p ↦ p.1 * p.2

Tactic:
fun_prop

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

Goal state before:
pp: M : Type u_2
M' : Type u_3
mM : MeasurableSpace M
inst✝⁵ : Monoid M
inst✝⁴ : MeasurableMul₂ M
mM' : MeasurableSpace M'
inst✝³ : Monoid M'
inst✝² : MeasurableMul₂ M'
μ ν : Measure M
inst✝¹ : SFinite μ
inst✝ : SFinite ν
L : M →* M'
hL : Measurable ⇑L
this : (⇑L ∘ fun p ↦ p.1 * p.2) = (fun p ↦ p.1 * p.2) ∘ Prod.map ⇑L ⇑L
⊢ Measurable (Prod.map ⇑L ⇑L)

Tactic:
fun_prop

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

Goal state before:
pp: M : Type u_2
M' : Type u_3
mM : MeasurableSpace M
inst✝⁵ : Monoid M
inst✝⁴ : MeasurableMul₂ M
mM' : MeasurableSpace M'
inst✝³ : Monoid M'
inst✝² : MeasurableMul₂ M'
μ ν : Measure M
inst✝¹ : SFinite μ
inst✝ : SFinite ν
L : M →* M'
hL : Measurable ⇑L
this : (⇑L ∘ fun p ↦ p.1 * p.2) = (fun p ↦ p.1 * p.2) ∘ Prod.map ⇑L ⇑L
⊢ Measurable ⇑L

Tactic:
fun_prop

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

Goal state before:
pp: case hL
E : Type u_2
F : Type u_3
inst✝¹¹ : AddCommMonoid E
inst✝¹⁰ : AddCommMonoid F
inst✝⁹ : Module ℝ E
inst✝⁸ : Module ℝ F
inst✝⁷ : TopologicalSpace E
inst✝⁶ : TopologicalSpace F
mE : MeasurableSpace E
inst✝⁵ : MeasurableAdd₂ E
mF : MeasurableSpace F
inst✝⁴ : MeasurableAdd₂ F
inst✝³ : OpensMeasurableSpace E
inst✝² : BorelSpace F
μ ν : Measure E
inst✝¹ : SFinite μ
inst✝ : SFinite ν
L : E →L[ℝ] F
⊢ Measurable ⇑L

Tactic:
fun_prop

Goal state after: