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

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

Tactic:
rsuffices ⟨n, hn⟩ : ∃ n, ∀ m, n ≤ m → x ∈ S m

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

α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : ℕ → Set α := ⋯
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := ⋯
fs : ℕ → α →ₛ β := ⋯
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, (fs n) x = 0
x : α
hxt : x ∈ t
h : Tendsto (fun n ↦ (f_approx n) x) atTop (𝓝 (f x))
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → x ∈ S m
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

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

Tactic:
by
      congr; ext a; rw [iSup_eapprox_apply hf]

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
ι : Type u_2
l : Filter ι
inst✝ : l.IsCountablyGenerated
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, AEMeasurable (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))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ a, ∀ (b : ℕ), a ≤ b → x b ∈ s
k : ℕ
h : ∀ (b : ℕ), k ≤ b → x b ∈ {x | (fun n ↦ AEMeasurable (F n) μ) x} ∩ {x | (fun n ↦ ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x}
⊢ α → ℝ≥0∞

Tactic:
exact bound

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

Goal state before:
pp: case refine_3
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
hf_mono : Monotone f
hf_prop : ∀ (n : ℕ), ∫⁻ (a : α), f n a ∂μ.trim hm = ∫⁻ (a : α), f n a ∂μ
⊢ ⨆ n, ∫⁻ (a : α), f n a ∂μ.trim hm = ∫⁻ (a : α), (fun x ↦ ⨆ n, f n x) a ∂μ

Tactic:
rw [lintegral_iSup (fun n => Measurable.mono (hf n) hm le_rfl) hf_mono]

Goal state after:
case refine_3
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
hf_mono : Monotone f
hf_prop : ∀ (n : ℕ), ∫⁻ (a : α), f n a ∂μ.trim hm = ∫⁻ (a : α), f n a ∂μ
⊢ ⨆ n, ∫⁻ (a : α), f n a ∂μ.trim hm = ⨆ n, ∫⁻ (a : α), f n a ∂μ
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
E : Type u_5
m : MeasurableSpace α
f g : α → E
inst✝³ : TopologicalSpace E
inst✝² : Preorder E
inst✝¹ : OrderClosedTopology E
inst✝ : PseudoMetrizableSpace E
hf : StronglyMeasurable f
hg : StronglyMeasurable g
⊢ MeasurableSet {a | f a ≤ g a}

Tactic:
borelize (E × E)
  exact (hf.prodMk hg).measurable isClosed_le_prod.measurableSet

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

Goal state before:
pp: α : Type u_5
E : Type u_6
m m₂ : MeasurableSpace α
inst✝¹ : TopologicalSpace E
inst✝ : Zero E
s : Set α
f : α → E
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
⊢ MeasurableSet (s ∩ univ)

Tactic:
by simpa

Goal state after:
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: x : ↑I
⊢ Subtype.val ⁻¹' Iic ↑x = Icc 0 x

Tactic:
rw [preimage_subtype_val_Iic]
  exact Icc_bot.symm

Goal state after:
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: α : Type ?u.3
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a✝ b✝ c d : α
h : a✝ ≤ b✝
δ : α
a b : ℝ
x y : ↑(Icc a b)
t : ↑unitInterval
⊢ (1 - ↑t) * ↑x + ↑t * ↑y ∈ Icc a b

Tactic:
by
    constructor
    · nlinarith [x.2.1, y.2.1, t.2.1, t.2.2]
    · nlinarith [x.2.2, y.2.2, t.2.1, t.2.2]

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 - ↑x) / (↑z - ↑x) ≤ 1

Tactic:
replace hxy : (x : ℝ) ≤ (y : ℝ) := hxy
    replace hyz : (y : ℝ) ≤ (z : ℝ) := hyz
    apply div_le_one_of_le₀ <;> grind

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

Goal state before:
pp: case mp.inl.inr
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
hsX : s ∈ Filter.map (fun p ↦ (Sum.inl p.1, Sum.inl p.2)) (𝓤 X)
hsY : s ∈ Filter.map (fun p ↦ (Sum.inr p.1, Sum.inr p.2)) (𝓤 Y)
εX : ℝ
εX0 : εX > 0
hX : ∀ ⦃a b : X⦄, dist a b < εX → (a, b) ∈ (fun p ↦ (Sum.inl p.1, Sum.inl p.2)) ⁻¹' s
εY : ℝ
εY0 : εY > 0
hY : ∀ ⦃a b : Y⦄, dist a b < εY → (a, b) ∈ (fun p ↦ (Sum.inr p.1, Sum.inr p.2)) ⁻¹' s
a : X
b : Y
h : Sum.dist (Sum.inl a) (Sum.inr b) < min (min εX εY) 1
⊢ (Sum.inl a, Sum.inr b) ∈ s

pp: case mp.inr.inl
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
hsX : s ∈ Filter.map (fun p ↦ (Sum.inl p.1, Sum.inl p.2)) (𝓤 X)
hsY : s ∈ Filter.map (fun p ↦ (Sum.inr p.1, Sum.inr p.2)) (𝓤 Y)
εX : ℝ
εX0 : εX > 0
hX : ∀ ⦃a b : X⦄, dist a b < εX → (a, b) ∈ (fun p ↦ (Sum.inl p.1, Sum.inl p.2)) ⁻¹' s
εY : ℝ
εY0 : εY > 0
hY : ∀ ⦃a b : Y⦄, dist a b < εY → (a, b) ∈ (fun p ↦ (Sum.inr p.1, Sum.inr p.2)) ⁻¹' s
a : Y
b : X
h : Sum.dist (Sum.inr a) (Sum.inl b) < min (min εX εY) 1
⊢ (Sum.inr a, Sum.inl b) ∈ s

pp: case mp.inr.inr
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
hsX : s ∈ Filter.map (fun p ↦ (Sum.inl p.1, Sum.inl p.2)) (𝓤 X)
hsY : s ∈ Filter.map (fun p ↦ (Sum.inr p.1, Sum.inr p.2)) (𝓤 Y)
εX : ℝ
εX0 : εX > 0
hX : ∀ ⦃a b : X⦄, dist a b < εX → (a, b) ∈ (fun p ↦ (Sum.inl p.1, Sum.inl p.2)) ⁻¹' s
εY : ℝ
εY0 : εY > 0
hY : ∀ ⦃a b : Y⦄, dist a b < εY → (a, b) ∈ (fun p ↦ (Sum.inr p.1, Sum.inr p.2)) ⁻¹' s
a b : Y
h : Sum.dist (Sum.inr a) (Sum.inr b) < min (min εX εY) 1
⊢ (Sum.inr a, Sum.inr b) ∈ s

Tactic:
· cases not_le_of_gt (lt_of_lt_of_le h (min_le_right _ _)) Sum.one_le_dist_inl_inr

Goal state after:
case mp.inr.inl
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
hsX : s ∈ Filter.map (fun p ↦ (Sum.inl p.1, Sum.inl p.2)) (𝓤 X)
hsY : s ∈ Filter.map (fun p ↦ (Sum.inr p.1, Sum.inr p.2)) (𝓤 Y)
εX : ℝ
εX0 : εX > 0
hX : ∀ ⦃a b : X⦄, dist a b < εX → (a, b) ∈ (fun p ↦ (Sum.inl p.1, Sum.inl p.2)) ⁻¹' s
εY : ℝ
εY0 : εY > 0
hY : ∀ ⦃a b : Y⦄, dist a b < εY → (a, b) ∈ (fun p ↦ (Sum.inr p.1, Sum.inr p.2)) ⁻¹' s
a : Y
b : X
h : Sum.dist (Sum.inr a) (Sum.inl b) < min (min εX εY) 1
⊢ (Sum.inr a, Sum.inl b) ∈ s

case mp.inr.inr
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
hsX : s ∈ Filter.map (fun p ↦ (Sum.inl p.1, Sum.inl p.2)) (𝓤 X)
hsY : s ∈ Filter.map (fun p ↦ (Sum.inr p.1, Sum.inr p.2)) (𝓤 Y)
εX : ℝ
εX0 : εX > 0
hX : ∀ ⦃a b : X⦄, dist a b < εX → (a, b) ∈ (fun p ↦ (Sum.inl p.1, Sum.inl p.2)) ⁻¹' s
εY : ℝ
εY0 : εY > 0
hY : ∀ ⦃a b : Y⦄, dist a b < εY → (a, b) ∈ (fun p ↦ (Sum.inr p.1, Sum.inr p.2)) ⁻¹' s
a b : Y
h : Sum.dist (Sum.inr a) (Sum.inr b) < min (min εX εY) 1
⊢ (Sum.inr a, Sum.inr b) ∈ s
Module: Mathlib.Topology.MetricSpace.Polish

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : MetricSpace α
s : Opens α
inst✝ : CompleteSpace α
u : ℕ → s.CompleteCopy
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (1 / 2) ^ N
⊢ Tendsto (fun n ↦ (1 / 2) ^ n) atTop (𝓝 0)

Tactic:
· exact tendsto_pow_atTop_nhds_zero_of_lt_one (by simp) (by norm_num)

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
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)
this : ∀ i ∈ F, y i ∈ U i
⊢ y ∈ (↑F).pi U

Tactic:
by simpa

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 y : (n : ℕ) → E n
hx : x ∉ s
hy : y ∈ s
⊢ firstDiff x y ≤ longestPrefix x s

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

Goal state after:
Module: Mathlib.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
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
⊢ x ∈ cylinder y (firstDiff x y)

Tactic:
apply mem_cylinder_firstDiff

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

Goal state before:
pp: case hd
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
h : μ ≪ ν₁ + ν₂
h_ms : μ ⟂ₘ ν₂
s : Set α
hs : MeasurableSet s
hs_zero : ν₁ s = 0
t : Set α := h_ms.nullSet
ht : MeasurableSet t
htμ : μ t = 0
htν₂ : ν₂ tᶜ = 0
⊢ Disjoint (s ∩ t) (s ∩ tᶜ)

Tactic:
exact (disjoint_compl_right.inter_right' _).inter_left' _

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

Goal state before:
pp: α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : Countable α
μ1 μ2 : Measure α
inst✝¹ : SigmaFinite μ1
inst✝ : SigmaFinite μ2
⊢ μ1 = μ2 ↔ ∀ (x : α), μ1.real {x} = μ2.real {x}

Tactic:
Measure.ext_iff_singleton

Goal state after:
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : Countable α
μ1 μ2 : Measure α
inst✝¹ : SigmaFinite μ1
inst✝ : SigmaFinite μ2
⊢ (∀ (a : α), μ1 {a} = μ2 {a}) ↔ ∀ (x : α), μ1.real {x} = μ2.real {x}
Module: Mathlib.MeasureTheory.Measure.Count

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
s : Set α
hs : s.Finite
⊢ count s = ↑(#hs.toFinset)

Tactic:
← count_apply_finset,

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
s : Set α
hs : s.Finite
⊢ count s = count ↑hs.toFinset
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
μ : Measure α
measurableAtoms : Set (Set α) := measurableAtom '' univ
h_nonempty : ∀ (s : ↑measurableAtoms), (↑s).Nonempty
points : ↑measurableAtoms → α := fun s ↦ ⋯.some
x y : α
s : Set α
hyx : ¬y = points ⟨measurableAtom x, ⋯⟩
hyx' : y ∈ measurableAtom x
h1 : measurableAtom y = measurableAtom x
z : α
left✝ : z ∈ univ
hz : measurableAtom z = s
h_points_mem : points ⟨s, ⋯⟩ ∈ s
hsy : points ⟨s, ⋯⟩ = y
⊢ points ⟨s, ⋯⟩ ∈ measurableAtom z

Tactic:
convert! h_points_mem

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

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

Tactic:
rw [← compl_compl s, ← mem_ae_iff, notMem_compl_iff]

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
a : α
hs : MeasurableSet s
⊢ sᶜ ∈ ae (dirac a) ↔ a ∈ sᶜ
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: α : Type u_4
mα : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
μ : Measure α
s : Finset α
hμ : μ = ∑ a ∈ s, μ {a} • dirac a
i : α
hi : i ∈ s
⊢ ∀ᵐ (x : α) ∂dirac i, x ∈ s

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_4
mα : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
μ : Measure α
s : Finset α
hμ : μ = ∑ a ∈ s, μ {a} • dirac a
⊢ ∀ i ∈ s, ∀ᵐ (x : α) ∂μ {i} • dirac i, x ∈ s

Tactic:
exact fun i hi ↦ ae_smul_measure (by simpa) _

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

Goal state before:
pp: α : Type u_4
mα : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
μ : Measure α
a₁ a₂ : α
ha : a₁ ≠ a₂
⊢ a₁ ∉ {a₂}

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSingletonClass α
f : β → α
a₁ a₂ : α
μ : Measure β
hf : AEMeasurable f μ
ha : a₁ ≠ a₂
⊢ a₁ ∉ {a₂}

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * μ s
c_ne_zero : c ≠ 0
⊢ L / ↑c < μ s

Tactic:
ENNReal.div_lt_iff,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * μ s
c_ne_zero : c ≠ 0
⊢ L < μ s * ↑c

case h0
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * μ s
c_ne_zero : c ≠ 0
⊢ ↑c ≠ 0 ∨ L ≠ 0

case ht
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * μ s
c_ne_zero : c ≠ 0
⊢ ↑c ≠ ∞ ∨ L ≠ ∞
Module: Mathlib.MeasureTheory.Group.Convolution

Goal state before:
pp: M : Type u_1
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
μ ν : Measure M
f : M → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (z : M), f z ∂μ ∗ₘ ν = ∫⁻ (z : M × M), f (z.1 * z.2) ∂μ.prod ν

Tactic:
rw [mconv, lintegral_map hf measurable_mul]

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

Goal state before:
pp: case refine_3
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
m : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
⊢ ∀ ⦃f : ℕ → α × β → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f n)) →
      Monotone f →
        (∀ (n : ℕ), Measurable fun x ↦ ∫⁻ (y : β), f n (x, y) ∂ν) →
          Measurable fun x ↦ ∫⁻ (y : β), (fun x ↦ ⨆ n, f n x) (x, y) ∂ν

Tactic:
· intro f hf h2f h3f
    have : ∀ x, Monotone fun n y => f n (x, y) := fun x i j hij y => h2f hij (x, y)
    conv => enter [1, x]; erw [lintegral_iSup (fun n => (hf n).comp m) (this x)]
    exact .iSup h3f

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

Goal state before:
pp: 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
this : map (⇑↑L) (μ ∗ ν) = map (⇑↑L) μ ∗ map (⇑↑L) ν
⊢ map (⇑L) (μ ∗ ν) = map (⇑L) μ ∗ map (⇑L) ν

Tactic:
by simpa

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

Goal state before:
pp: case right
X : Type u_4
Y : Type u_5
m : MeasurableSpace X
μ : Measure X
m' : MeasurableSpace Y
ν : Measure Y
l : Filter X
l' : Filter Y
s : Set X
hs : s ∈ l
hμs : μ s < ∞
t : Set Y
ht : t ∈ l'
hνt : ν t < ∞
⊢ (μ.prod ν) (s ×ˢ t) < ∞

Tactic:
prod_prod_le

Goal state after:
case right
X : Type u_4
Y : Type u_5
m : MeasurableSpace X
μ : Measure X
m' : MeasurableSpace Y
ν : Measure Y
l : Filter X
l' : Filter Y
s : Set X
hs : s ∈ l
hμs : μ s < ∞
t : Set Y
ht : t ∈ l'
hνt : ν t < ∞
⊢ μ s * ν t < ∞
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ μ' : Measure α
ν ν' : Measure β
inst✝ : SFinite ν'
h1 : μ ≪ μ'
h2 : ν ≪ ν'
s : Set (α × β)
hs : MeasurableSet s
h2s : (μ'.prod ν') s = 0
⊢ (μ.prod ν) s = 0

Tactic:
apply measure_prod_null_of_ae_null hs

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ μ' : Measure α
ν ν' : Measure β
inst✝ : SFinite ν'
h1 : μ ≪ μ'
h2 : ν ≪ ν'
s : Set (α × β)
hs : MeasurableSet s
h2s : (μ'.prod ν') s = 0
⊢ (fun x ↦ ν (Prod.mk x ⁻¹' s)) =ᵐ[μ] 0
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case mp
G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g₁ g₂ : G
h : (hSK.equiv g₁).1 = (hSK.equiv g₂).1
⊢ g₁⁻¹ * (↑(hSK.equiv g₂).1 * ↑(hSK.equiv g₂).2) ∈ K

Tactic:
← hSK.equiv_fst_mul_equiv_snd g₁,

Goal state after:
case mp
G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g₁ g₂ : G
h : (hSK.equiv g₁).1 = (hSK.equiv g₂).1
⊢ (↑(hSK.equiv g₁).1 * ↑(hSK.equiv g₁).2)⁻¹ * (↑(hSK.equiv g₂).1 * ↑(hSK.equiv g₂).2) ∈ K
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case mp
G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g₁ g₂ : G
h : (hSK.equiv g₁).1 = (hSK.equiv g₂).1
⊢ (↑(hSK.equiv g₁).1 * ↑(hSK.equiv g₁).2)⁻¹ * (↑(hSK.equiv g₁).1 * ↑(hSK.equiv g₂).2) ∈ K

Tactic:
mul_inv_rev,

Goal state after:
case mp
G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g₁ g₂ : G
h : (hSK.equiv g₁).1 = (hSK.equiv g₂).1
⊢ (↑(hSK.equiv g₁).2)⁻¹ * (↑(hSK.equiv g₁).1)⁻¹ * (↑(hSK.equiv g₁).1 * ↑(hSK.equiv g₂).2) ∈ K
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case mp
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
g₁ g₂ : G
h : (hHT.equiv g₁).2 = (hHT.equiv g₂).2
⊢ ↑(hHT.equiv g₂).1 * ↑(hHT.equiv g₁).2 * (↑(hHT.equiv g₁).1 * ↑(hHT.equiv g₁).2)⁻¹ ∈ H

Tactic:
mul_inv_rev,

Goal state after:
case mp
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
g₁ g₂ : G
h : (hHT.equiv g₁).2 = (hHT.equiv g₂).2
⊢ ↑(hHT.equiv g₂).1 * ↑(hHT.equiv g₁).2 * ((↑(hHT.equiv g₁).2)⁻¹ * (↑(hHT.equiv g₁).1)⁻¹) ∈ H
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
S : Set G
hS : IsComplement S ↑H
g : G
⊢ ((↑(hS.toLeftFun g))⁻¹ * g)⁻¹ = g⁻¹ * ↑(hS.toLeftFun g)

Tactic:
mul_inv_rev,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
S : Set G
hS : IsComplement S ↑H
g : G
⊢ g⁻¹ * (↑(hS.toLeftFun g))⁻¹⁻¹ = g⁻¹ * ↑(hS.toLeftFun g)
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hT : IsComplement (↑H) T
g : G
⊢ (g * (↑(hT.toRightFun g))⁻¹)⁻¹ = ↑(hT.toRightFun g) * g⁻¹

Tactic:
mul_inv_rev,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hT : IsComplement (↑H) T
g : G
⊢ (↑(hT.toRightFun g))⁻¹⁻¹ * g⁻¹ = ↑(hT.toRightFun g) * g⁻¹
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
p : Set α → Prop
inst✝¹ : TopologicalSpace α
inst✝ : μ.OuterRegular
H : μ.InnerRegularWRT p IsOpen[inst✝¹]
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen[inst✝¹] U → p (s \ U)
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
r : ℝ≥0∞
hr : r < μ s
this : 0 < μ univ
⊢ p ∅

Tactic:
obtain ⟨K, -, hK, -⟩ : ∃ K, K ⊆ univ ∧ p K ∧ 0 < μ K := H isOpen_univ _ this

Goal state after:
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
p : Set α → Prop
inst✝¹ : TopologicalSpace α
inst✝ : μ.OuterRegular
H : μ.InnerRegularWRT p IsOpen[inst✝¹]
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen[inst✝¹] U → p (s \ U)
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
r : ℝ≥0∞
hr : r < μ s
this : 0 < μ univ
K : Set α
hK : p K
⊢ p ∅
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝⁵ : MeasurableSpace G
inst✝⁴ : MeasurableSpace H
inst✝³ : DivisionMonoid G
inst✝² : MeasurableMul G
inst✝¹ : MeasurableInv G
μ : Measure G
inst✝ : μ.IsMulLeftInvariant
g : G
⊢ map (fun x ↦ x⁻¹ * g) μ = map (fun x ↦ (g⁻¹ * x)⁻¹) μ

Tactic:
mul_inv_rev,

Goal state after:
G : Type u_1
H : Type u_2
inst✝⁵ : MeasurableSpace G
inst✝⁴ : MeasurableSpace H
inst✝³ : DivisionMonoid G
inst✝² : MeasurableMul G
inst✝¹ : MeasurableInv G
μ : Measure G
inst✝ : μ.IsMulLeftInvariant
g : G
⊢ map (fun x ↦ x⁻¹ * g) μ = map (fun x ↦ x⁻¹ * g⁻¹⁻¹) μ
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝⁵ : MeasurableSpace G
inst✝⁴ : MeasurableSpace H
inst✝³ : DivisionMonoid G
inst✝² : MeasurableMul G
inst✝¹ : MeasurableInv G
μ : Measure G
inst✝ : μ.IsMulRightInvariant
g : G
⊢ map (fun x ↦ g * x⁻¹) μ = map (fun x ↦ (x * g⁻¹)⁻¹) μ

Tactic:
mul_inv_rev,

Goal state after:
G : Type u_1
H : Type u_2
inst✝⁵ : MeasurableSpace G
inst✝⁴ : MeasurableSpace H
inst✝³ : DivisionMonoid G
inst✝² : MeasurableMul G
inst✝¹ : MeasurableInv G
μ : Measure G
inst✝ : μ.IsMulRightInvariant
g : G
⊢ map (fun x ↦ g * x⁻¹) μ = map (fun x ↦ g⁻¹⁻¹ * x⁻¹) μ
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst✝¹¹ : TopologicalSpace α
inst✝¹⁰ : MeasurableSpace α
inst✝⁹ : BorelSpace α
inst✝⁸ : LinearOrder α
inst✝⁷ : OrderTopology α
inst✝⁶ : PolishSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : LinearOrder β
inst✝¹ : OrderTopology β
inst✝ : SecondCountableTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
t' : Set α := ⋯
ht' : t'.Countable
this : g '' t = g '' (t \ t') ∪ g '' t'
⊢ MeasurableSet (g '' (t \ t'))

Tactic:
apply MeasurableSet.image_of_monotoneOn_of_continuousOn (ht.diff ht'.measurableSet)
    (hg.mono sdiff_subset)

Goal state after:
α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst✝¹¹ : TopologicalSpace α
inst✝¹⁰ : MeasurableSpace α
inst✝⁹ : BorelSpace α
inst✝⁸ : LinearOrder α
inst✝⁷ : OrderTopology α
inst✝⁶ : PolishSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : LinearOrder β
inst✝¹ : OrderTopology β
inst✝ : SecondCountableTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
t' : Set α := ⋯
ht' : t'.Countable
this : g '' t = g '' (t \ t') ∪ g '' t'
⊢ ContinuousOn g (t \ t')
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hY : AEMeasurable Y μ
hX : AEMeasurable X μ
s : Set β
hs : MeasurableSet s
⊢ (map (fun a ↦ (X a, Y a)) μ).fst s = (map X μ) s

Tactic:
Measure.fst_apply hs,

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hY : AEMeasurable Y μ
hX : AEMeasurable X μ
s : Set β
hs : MeasurableSet s
⊢ (map (fun a ↦ (X a, Y a)) μ) (Prod.fst ⁻¹' s) = (map X μ) s
Module: Mathlib.MeasureTheory.Group.Prod

Goal state before:
pp: G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SFinite ν
inst✝³ : SFinite μ
inst✝² : MeasurableInv G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : ν.IsMulLeftInvariant
x y : G
⊢ (y * x, x⁻¹) = (y * x, (y * x)⁻¹ * y)

Tactic:
mul_inv_rev,

Goal state after:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SFinite ν
inst✝³ : SFinite μ
inst✝² : MeasurableInv G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : ν.IsMulLeftInvariant
x y : G
⊢ (y * x, x⁻¹) = (y * x, x⁻¹ * y⁻¹ * y)