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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hm : MeasurableSet {x | f x ≤ g x}
⊢ ∫⁻ (x : α), max (f x) (g x) ∂μ = ∫⁻ (x : α) in {x | f x ≤ g x}, g x ∂μ + ∫⁻ (x : α) in {x | g x < f x}, f x ∂μ

Tactic:
← lintegral_add_compl (fun x => max (f x) (g x)) hm

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hm : MeasurableSet {x | f x ≤ g x}
⊢ ∫⁻ (x : α) in {x | f x ≤ g x}, max (f x) (g x) ∂μ + ∫⁻ (x : α) in {x | f x ≤ g x}ᶜ, max (f x) (g x) ∂μ =
    ∫⁻ (x : α) in {x | f x ≤ g x}, g x ∂μ + ∫⁻ (x : α) in {x | g x < f x}, f x ∂μ
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : One β
f : α → β
hf : Continuous[inst✝⁴, inst✝²] f
k : Set α
hk : IsCompact k
h'f : mulSupport f ⊆ k
⊢ StronglyMeasurable f

Tactic:
borelize β
  let : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
  rw [stronglyMeasurable_iff_measurable_separable]
  exact ⟨hf.measurable, (isCompact_range_of_mulSupport_subset_isCompact hf hk h'f).isSeparable⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
⊢ ∫⁻ (a : α), ⨆ s, ∑ i ∈ s, f i a ∂μ = ⨆ s, ∑ i ∈ s, ∫⁻ (a : α), f i a ∂μ

Tactic:
lintegral_iSup_directed

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
⊢ ⨆ b, ∫⁻ (a : α), ∑ i ∈ b, f i a ∂μ = ⨆ s, ∑ i ∈ s, ∫⁻ (a : α), f i a ∂μ

case hf
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
⊢ ∀ (b : Finset β), AEMeasurable (fun a ↦ ∑ i ∈ b, f i a) μ

case h_directed
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
⊢ Directed (fun x1 x2 ↦ x1 ≤ x2) fun s a ↦ ∑ i ∈ s, f i a
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, 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))
⊢ Tendsto (fun n ↦ ∫⁻ (a : α), F n a ∂μ) l (𝓝 (∫⁻ (a : α), f a ∂μ))

Tactic:
tendsto_iff_seq_tendsto

Goal state after:
α : 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 : ℕ → ι), Tendsto x atTop l → Tendsto ((fun n ↦ ∫⁻ (a : α), F n a ∂μ) ∘ x) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
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, 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 : ℕ → ι), Tendsto x atTop l → Tendsto ((fun n ↦ ∫⁻ (a : α), F n a ∂μ) ∘ x) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))

Tactic:
intro x xl

Goal state after:
α : 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
⊢ Tendsto ((fun n ↦ ∫⁻ (a : α), F n a ∂μ) ∘ x) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSingletonClass α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
h : SecondCountableTopologyEither α β
f : α → β
s : Set α
hf : ContinuousOn f s
hs : sᶜ.Countable
⊢ StronglyMeasurable f

Tactic:
classical
  have h's : MeasurableSet s := by simpa using hs.measurableSet.compl
  have : f = fun x ↦ if hx : x ∈ s then f (⟨x, hx⟩ : s) else f (⟨x, hx⟩ : (sᶜ : Set α)) := by simp
  rw [this]
  apply StronglyMeasurable.dite (f := fun x ↦ f x) (g := fun x ↦ f x) ?_ ?_ h's
  · have : SecondCountableTopologyEither s β := by cases h.out <;> infer_instance
    exact (continuousOn_iff_continuous_domRestrict.1 hf).stronglyMeasurable
  · have := hs.to_subtype
    exact MeasureTheory.StronglyMeasurable.of_discrete

Goal state after:
Module: Mathlib.Topology.Perfect

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
C : Set α
x : α
U : Set α
h_acc : AccPt x (𝓟 C)
hU : U ∈ 𝓝 x
⊢ 𝓝[≠] x ≤ 𝓟 U

Tactic:
rw [le_principal_iff]

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
C : Set α
x : α
U : Set α
h_acc : AccPt x (𝓟 C)
hU : U ∈ 𝓝 x
⊢ U ∈ 𝓝[≠] x
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 : α → ℝ
f : α → β → F
hu : Summable u
s : Set β
hfu : ∀ (n : α), ∀ x ∈ s, ‖f n x‖ ≤ u n
ε : ℝ
εpos : ε > 0
t : Finset α
ht : ∑' (a : { x // x ∉ t }), u ↑a < ε
x : β
hx : x ∈ s
A : Summable fun n ↦ ‖f n x‖
⊢ ‖∑' (x_1 : { x // x ∉ t }), f (↑x_1) x‖ ≤ ∑' (a : { x // x ∉ t }), u ↑a

Tactic:
apply (norm_tsum_le_tsum_norm (A.subtype _)).trans

Goal state after:
α : Type u_1
β : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
u : α → ℝ
f : α → β → F
hu : Summable u
s : Set β
hfu : ∀ (n : α), ∀ x ∈ s, ‖f n x‖ ≤ u n
ε : ℝ
εpos : ε > 0
t : Finset α
ht : ∑' (a : { x // x ∉ t }), u ↑a < ε
x : β
hx : x ∈ s
A : Summable fun n ↦ ‖f n x‖
⊢ ∑' (i : { x // x ∉ t }), ‖f (↑i) x‖ ≤ ∑' (a : { x // x ∉ t }), u ↑a
Module: Mathlib.Analysis.Normed.Group.FunctionSeries

Goal state before:
pp: β : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
ι : Type u_4
f : ι → β → F
u : ι → ℝ
hu : Summable u
s : Set β
ε : ℝ
εpos : ε > 0
t : Finset ι
ht : ∀ (b : Finset ι), t ⊆ b → ∑' (a : { x // x ∉ b }), u ↑a < ε
N : Set ι
hN : N ∈ cofinite
HN : ∀ y ∈ N, ∀ x ∈ s, ‖f y x‖ ≤ u y
n : Finset ι
hn : Finite.toFinset hN ∪ t ⊆ n
x : β
hx : x ∈ s
A : Summable fun n ↦ ‖f n x‖
⊢ ‖∑' (x_1 : { x // x ∉ n }), f (↑x_1) x‖ ≤ ∑' (a : { x // x ∉ n }), u ↑a

Tactic:
apply (norm_tsum_le_tsum_norm (A.subtype _)).trans

Goal state after:
β : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
ι : Type u_4
f : ι → β → F
u : ι → ℝ
hu : Summable u
s : Set β
ε : ℝ
εpos : ε > 0
t : Finset ι
ht : ∀ (b : Finset ι), t ⊆ b → ∑' (a : { x // x ∉ b }), u ↑a < ε
N : Set ι
hN : N ∈ cofinite
HN : ∀ y ∈ N, ∀ x ∈ s, ‖f y x‖ ≤ u y
n : Finset ι
hn : Finite.toFinset hN ∪ t ⊆ n
x : β
hx : x ∈ s
A : Summable fun n ↦ ‖f n x‖
⊢ ∑' (i : { x // x ∉ n }), ‖f (↑i) x‖ ≤ ∑' (a : { x // x ∉ n }), u ↑a
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: t : ℝ
⊢ 2 * t - 1 ∈ I ↔ t ∈ Icc (1 / 2) 1

Tactic:
constructor <;> rintro ⟨h₁, h₂⟩ <;> constructor <;> linarith

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
ε : ℝ
H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε
x : X
y : Y
z : X
⊢ dist x z ≤ (⨅ p, dist x (Φ p) + dist y (Ψ p)) + ε + ((⨅ p, dist z (Φ p) + dist y (Ψ p)) + ε)

Tactic:
add_add_add_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
ε : ℝ
H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε
x : X
y : Y
z : X
⊢ dist x z ≤ ((⨅ p, dist x (Φ p) + dist y (Ψ p)) + ⨅ p, dist z (Φ p) + dist y (Ψ p)) + (ε + ε)
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: E : ℕ → Type u_1
x y : (n : ℕ) → E n
h : x ≠ y
⊢ x (firstDiff x y) ≠ y (firstDiff x y)

Tactic:
rw [firstDiff_def, dif_pos h]
  classical
  exact Nat.find_spec (ne_iff.1 h)

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

Goal state before:
pp: E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : E n
i : ℕ
hi : i < n
⊢ update x n y i = x i

Tactic:
simp [hi.ne]

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

Goal state before:
pp: case inr.inr.inr
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
k : ι
z : E k
hik : i ≠ k
hij : i ≠ j
hjk : j ≠ k
⊢ dist x ⋯.some + 1 + dist ⋯.some z ≤ dist x ⋯.some + 1 + dist ⋯.some y + (dist y ⋯.some + 1 + dist ⋯.some z)

Tactic:
calc
          dist x (Nonempty.some ⟨x⟩) + 1 + dist (Nonempty.some ⟨z⟩) z =
              dist x (Nonempty.some ⟨x⟩) + 1 + 0 + (0 + 0 + dist (Nonempty.some ⟨z⟩) z) := by
            simp only [add_zero, zero_add]
          _ ≤ _ := by apply_rules [add_le_add, zero_le_one, dist_nonneg, le_rfl]

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

Goal state before:
pp: case refine_1
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
⊢ ∀ (x : (i : ι) × E i), Sigma.dist x x = 0

Tactic:
rintro ⟨i, x⟩

Goal state after:
case refine_1
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
⊢ Sigma.dist ⟨i, x⟩ ⟨i, x⟩ = 0
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)
⊢ IsOpen[Pi.topologicalSpace] s ↔ ∀ x ∈ s, ∃ ε > 0, ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s

Tactic:
by
  constructor
  · intro hs x hx
    obtain ⟨v, ⟨y, n, rfl⟩, h'x, h's⟩ :
        ∃ v ∈ { s | ∃ (x : ∀ n : ℕ, E n) (n : ℕ), s = cylinder x n }, x ∈ v ∧ v ⊆ s :=
      (isTopologicalBasis_cylinders E).exists_subset_of_mem_open hx hs
    rw [← mem_cylinder_iff_eq.1 h'x] at h's
    exact
      ⟨(1 / 2 : ℝ) ^ n, by simp, fun y hy => h's fun i hi => (apply_eq_of_dist_lt hy hi.le).symm⟩
  · intro h
    refine (isTopologicalBasis_cylinders E).isOpen_iff.2 fun x hx => ?_
    rcases h x hx with ⟨ε, εpos, hε⟩
    obtain ⟨n, hn⟩ : ∃ n : ℕ, (1 / 2 : ℝ) ^ n < ε := exists_pow_lt_of_lt_one εpos one_half_lt_one
    refine ⟨cylinder x n, ⟨x, n, rfl⟩, self_mem_cylinder x n, fun y hy => hε y ?_⟩
    rw [PiNat.dist_comm]
    exact (mem_cylinder_iff_dist_le.1 hy).trans_lt hn

Goal state after:
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
⊢ ν (⋃ i, (t i)ᶜ) ≤ ∑' (n : ℕ), ↑ε * (1 / 2) ^ n

Tactic:
refine (measure_iUnion_le _).trans ?_

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: case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
h : a ∉ s
⊢ (dirac a) s = 0

Tactic:
← nonpos_iff_eq_zero

Goal state after:
case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
h : a ∉ s
⊢ (dirac a) s ≤ 0
Module: Mathlib.MeasureTheory.Measure.MutuallySingular

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
⊢ μ ⟂ₘ ν

Tactic:
have h' (n : ℕ) : ∃ s, μ s = 0 ∧ ν sᶜ ≤ (1 / 2) ^ n := by
    convert!
      exists_null_set_measure_lt_of_disjoint h (ε := (1 / 2) ^ (n + 1)) <| pow_pos (by simp) (n + 1)
    conv =>
      -- this tweak is needed due to the known issue of `norm_cast` with numeric fractions
      enter [1, 1]
      equals ((1 : ℝ≥0) / (2 : ℝ≥0)) => rfl
    norm_cast
    ring
  choose s hs₂ hs₃ using h'
  refine Measure.MutuallySingular.mk (t := (⋃ n, s n)ᶜ) (measure_iUnion_null hs₂) ?_ ?_
  · rw [compl_iUnion]
    refine eq_zero_of_le_mul_pow (ε := 1) (by simp : (1 / 2 : ℝ≥0∞) < 1) <| fun n ↦ ?_
    rw [ENNReal.coe_one, one_mul]
    exact (measure_mono <| iInter_subset_of_subset n fun _ ht ↦ ht).trans (hs₃ n)
  · rw [union_compl_self]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : β → Measure α
h : ∀ (s : Set α), MeasurableSet s → Measurable fun b ↦ (f b) s
s : Set α
hs : MeasurableSet s
⊢ borel ℝ≥0∞ ≤ MeasurableSpace.map (fun μ ↦ μ s) (MeasurableSpace.map f mβ)

Tactic:
by rw [MeasurableSpace.map_comp]; exact h s hs

Goal state after:
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 : ι) → MetricSpace (Y i)
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
continuous_f : ∀ (i : ι), Continuous[inst✝¹, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f i)
separating_f : Pairwise fun x y ↦ ∃ i, f i x ≠ f i y
this : EMetricSpace (PiNatEmbed X Y f) := emetricSpace separating_f
⊢ Continuous[inst✝¹, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] toPiNat ∧ Bijective toPiNat

Tactic:
exact ⟨continuous_toPiNat continuous_f, (toPiNatEquiv X Y f).bijective⟩

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

Goal state before:
pp: α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K r : ℝ
hr : ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * r)) ≤ ↑(Classical.choose ⋯) * μ (closedBall x r)
x : α
⊢ ↑(Classical.choose ⋯) * μ (closedBall x r) ≤ ↑(scalingConstantOf μ K) * μ (closedBall x r)

Tactic:
scalingConstantOf,

Goal state after:
α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K r : ℝ
hr : ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * r)) ≤ ↑(Classical.choose ⋯) * μ (closedBall x r)
x : α
⊢ ↑(Classical.choose ⋯) * μ (closedBall x r) ≤ ↑(max (Classical.choose ⋯) 1) * μ (closedBall x r)
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ν : ν ≪ ρ
⊢ μ ∗ₘ ν ≪ ρ

Tactic:
refine AbsolutelyContinuous.mk (fun s hs h ↦ ?_)
  rw [← lintegral_indicator_one hs, lintegral_mconv (by measurability)]
  conv in s.indicator 1 (_ * _) => change s.indicator 1 ((fun y ↦ x * y) y)
  simp only [← Set.indicator_comp_right, Pi.one_comp]
  conv in ∫⁻ _, _ ∂ν =>
    rw [lintegral_indicator_one (by apply MeasurableSet.preimage hs (by fun_prop))]
  have h0 (x : M) : ν (HMul.hMul x ⁻¹' s) = 0 := by
    apply hν
    rw [← map_apply (by fun_prop) hs, IsMulLeftInvariant.map_mul_left_eq_self, h]
  simp [h0]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set (α × β)
hsm : MeasurableSet s
hs : (fun x ↦ ν (Prod.mk x ⁻¹' s)) =ᵐ[μ] 0
⊢ (μ.prod ν) s = 0

Tactic:
← nonpos_iff_eq_zero

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set (α × β)
hsm : MeasurableSet s
hs : (fun x ↦ ν (Prod.mk x ⁻¹' s)) =ᵐ[μ] 0
⊢ (μ.prod ν) s ≤ 0
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set α
hs : MeasurableSet s
h2s : μ s = 0
⊢ (μ.prod ν) (s ×ˢ univ) = 0

Tactic:
← nonpos_iff_eq_zero

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set α
hs : MeasurableSet s
h2s : μ s = 0
⊢ (μ.prod ν) (s ×ˢ univ) ≤ 0
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set β
hs : MeasurableSet s
h2s : ν s = 0
⊢ (μ.prod ν) (univ ×ˢ s) = 0

Tactic:
← nonpos_iff_eq_zero

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set β
hs : MeasurableSet s
h2s : ν s = 0
⊢ (μ.prod ν) (univ ×ˢ s) ≤ 0
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set α
t : Set β
s_ae_univ : μ sᶜ = 0
t_ae_univ : ν tᶜ = 0
⊢ (μ.prod ν) (sᶜ ×ˢ univ) = 0 ∧ (μ.prod ν) (univ ×ˢ tᶜ) = 0

Tactic:
simp [s_ae_univ, t_ae_univ]

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✝³ : PolishSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T0Space Y
inst✝ : SecondCountableTopology Y
f : X → Y
hf : Continuous[inst✝⁴, inst✝²] f
hsurj : Surjective f
⊢ MeasurableSpace.map f (borel X) = borel Y

Tactic:
by
  borelize X
  exact hf.map_eq_borel hsurj

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

Goal state before:
pp: case refine_2
α : Type u_4
β : Type u_5
γ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure (α × β × γ)
inst✝ : IsFiniteMeasure μ
h :
  ∀ {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s → MeasurableSet t → MeasurableSet u → μ (s ×ˢ t ×ˢ u) = ν (s ×ˢ t ×ˢ u)
s : Set (α × β × γ)
hs : MeasurableSet s
h_univ : μ univ = ν univ
this : IsFiniteMeasure ν
C₂ : Set (Set (β × γ)) := image2 (fun x1 x2 ↦ x1 ×ˢ x2) {t | MeasurableSet t} {u | MeasurableSet u}
C : Set (Set (α × β × γ)) := image2 (fun x1 x2 ↦ x1 ×ˢ x2) {s | MeasurableSet s} C₂
⊢ IsPiSystem C

Tactic:
exact MeasurableSpace.isPiSystem_measurableSet.prod isPiSystem_prod

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
g : G
⊢ RightCosetEquivalence (↑H) g ↑(hHT.equiv g).2

Tactic:
rw [RightCosetEquivalence, rightCoset_eq_iff, equiv_snd_eq_inv_mul]; simp

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
p : Set α → Prop
μ : Measure α
s : ℕ → Set α
h : ∀ (n : ℕ), (μ.restrict (s n)).InnerRegularWRT p MeasurableSet
hs : univ ⊆ ⋃ n, s n
hmono : Monotone s
F : Set α
hF : MeasurableSet F
r : ℝ≥0∞
hr : r < ⨆ n, μ (F ∩ s n)
hBU : ⋃ n, F ∩ s n = F
this : μ F = ⨆ n, μ (F ∩ s n)
⊢ ∃ K ⊆ F, p K ∧ r < μ K

Tactic:
rcases lt_iSup_iff.1 hr with ⟨n, hn⟩

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
p : Set α → Prop
μ : Measure α
s : ℕ → Set α
h : ∀ (n : ℕ), (μ.restrict (s n)).InnerRegularWRT p MeasurableSet
hs : univ ⊆ ⋃ n, s n
hmono : Monotone s
F : Set α
hF : MeasurableSet F
r : ℝ≥0∞
hr : r < ⨆ n, μ (F ∩ s n)
hBU : ⋃ n, F ∩ s n = F
this : μ F = ⨆ n, μ (F ∩ s n)
n : ℕ
hn : r < μ (F ∩ s n)
⊢ ∃ K ⊆ F, p K ∧ r < μ K
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
B : ℕ → Set α := spanningSets μ
hr : r < ⨆ n, μ (s ∩ B n)
hBU : ⋃ n, s ∩ B n = s
this : μ s = ⨆ n, μ (s ∩ B n)
⊢ ∃ K ⊆ s, (fun s ↦ MeasurableSet s ∧ μ s ≠ ∞) K ∧ r < μ K

Tactic:
rcases lt_iSup_iff.1 hr with ⟨n, hn⟩

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
B : ℕ → Set α := spanningSets μ
hr : r < ⨆ n, μ (s ∩ B n)
hBU : ⋃ n, s ∩ B n = s
this : μ s = ⨆ n, μ (s ∩ B n)
n : ℕ
hn : r < μ (s ∩ B n)
⊢ ∃ K ⊆ s, (fun s ↦ MeasurableSet s ∧ μ s ≠ ∞) K ∧ r < μ K
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
H : μ.InnerRegularWRT IsClosed[inst✝²] IsOpen[inst✝²]
hfin : ∀ {s : Set α}, μ s ≠ ∞
this :
  ∀ (s : Set α),
    MeasurableSet s →
      ∀ (ε : ℝ≥0∞), ε ≠ 0 → ∃ F ⊆ s, ∃ U ⊇ s, IsClosed[inst✝²] F ∧ IsOpen[inst✝²] U ∧ μ s ≤ μ F + ε ∧ μ U ≤ μ s + ε
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r > μ s
⊢ ∃ U ⊇ s, IsOpen[inst✝²] U ∧ μ U < r

Tactic:
rcases exists_between hr with ⟨r', hsr', hr'r⟩

Goal state after:
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
H : μ.InnerRegularWRT IsClosed[inst✝²] IsOpen[inst✝²]
hfin : ∀ {s : Set α}, μ s ≠ ∞
this :
  ∀ (s : Set α),
    MeasurableSet s →
      ∀ (ε : ℝ≥0∞), ε ≠ 0 → ∃ F ⊆ s, ∃ U ⊇ s, IsClosed[inst✝²] F ∧ IsOpen[inst✝²] U ∧ μ s ≤ μ F + ε ∧ μ U ≤ μ s + ε
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r > μ s
r' : ℝ≥0∞
hsr' : μ s < r'
hr'r : r' < r
⊢ ∃ U ⊇ s, IsOpen[inst✝²] U ∧ μ U < r
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
H : μ.InnerRegularWRT IsClosed[inst✝²] IsOpen[inst✝²]
hfin : ∀ {s : Set α}, μ s ≠ ∞
⊢ μ.WeaklyRegular

Tactic:
suffices ∀ s, MeasurableSet s → ∀ ε, ε ≠ 0 → ∃ F, F ⊆ s ∧ ∃ U, U ⊇ s ∧
      IsClosed F ∧ IsOpen U ∧ μ s ≤ μ F + ε ∧ μ U ≤ μ s + ε by
    refine
      { outerRegular := fun s hs r hr => ?_
        innerRegular := H }
    rcases exists_between hr with ⟨r', hsr', hr'r⟩
    rcases this s hs _ (tsub_pos_iff_lt.2 hsr').ne' with ⟨-, -, U, hsU, -, hUo, -, H⟩
    refine ⟨U, hsU, hUo, ?_⟩
    rw [add_tsub_cancel_of_le hsr'.le] at H
    exact H.trans_lt hr'r

Goal state after:
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
H : μ.InnerRegularWRT IsClosed[inst✝²] IsOpen[inst✝²]
hfin : ∀ {s : Set α}, μ s ≠ ∞
⊢ ∀ (s : Set α),
    MeasurableSet s →
      ∀ (ε : ℝ≥0∞), ε ≠ 0 → ∃ F ⊆ s, ∃ U ⊇ s, IsClosed[inst✝²] F ∧ IsOpen[inst✝²] U ∧ μ s ≤ μ F + ε ∧ μ U ≤ μ s + ε
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case f_cont
γ : Type u_3
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : PolishSpace γ
β : Type u_4
inst✝³ : TopologicalSpace β
inst✝² : T2Space β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
s : Set γ
hs : IsClosed[inst✝⁵] s
f : γ → β
f_cont : ContinuousOn f s
f_inj : InjOn f s
this : PolishSpace ↑s
⊢ Continuous[instTopologicalSpaceSubtype, inst✝³] fun x ↦ f ↑x

Tactic:
continuousOn_iff_continuous_domRestrict

Goal state after:
case f_cont
γ : Type u_3
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : PolishSpace γ
β : Type u_4
inst✝³ : TopologicalSpace β
inst✝² : T2Space β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
s : Set γ
hs : IsClosed[inst✝⁵] s
f : γ → β
f_cont : Continuous[instTopologicalSpaceSubtype, inst✝³] (s.domRestrict f)
f_inj : InjOn f s
this : PolishSpace ↑s
⊢ Continuous[instTopologicalSpaceSubtype, inst✝³] fun x ↦ f ↑x
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
inst✝⁴ : MeasurableSpace G
inst✝³ : Group G
inst✝² : MeasurableMul G
H : Subgroup G
inst✝¹ : H.FiniteIndex
hH : MeasurableSet ↑H
μ : Measure G
inst✝ : μ.IsMulLeftInvariant
s : Set G
hs : Subgroup.IsComplement s ↑H
hs' : Finite ↑s
⊢ μ (⋃ i, ↑i • ↑H) = μ univ

Tactic:
simp [hs.mul_eq]

Goal state after: