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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : TendstoInMeasure μ f atTop g
⊢ Tendsto (fun n ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)

Tactic:
refine tendsto_of_subseq_tendsto fun ns hns => ?_

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : TendstoInMeasure μ f atTop g
ns : ℕ → ℕ
hns : Tendsto ns atTop atTop
⊢ ∃ ms, Tendsto (fun n ↦ eLpNorm (f (ns (ms n)) - g) p μ) atTop (𝓝 0)
Module: Mathlib.MeasureTheory.Integral.Gamma

Goal state before:
pp: p q : ℝ
hp : 0 < p
hq : -1 < q
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ 1 * (x✝ ^ (1 / p - 1) * (x✝ ^ (1 / p * q) * rexp (-x✝))) / p = 1 / p * (rexp (-x✝) * x✝ ^ (1 / p - 1 + q / p))

Tactic:
one_mul,

Goal state after:
p q : ℝ
hp : 0 < p
hq : -1 < q
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ x✝ ^ (1 / p - 1) * (x✝ ^ (1 / p * q) * rexp (-x✝)) / p = 1 / p * (rexp (-x✝) * x✝ ^ (1 / p - 1 + q / p))
Module: Mathlib.MeasureTheory.Integral.Gamma

Goal state before:
pp: p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ x✝ ^ q * rexp (-b * x✝ ^ p) = 1 * (x✝ ^ q * rexp (-(b * x✝ ^ p)))

pp: case hx
p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ 0 < b

pp: p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ p ≠ 0

pp: case hx
p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ 0 ≤ b

pp: case hx
p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ 0 ≤ b

pp: p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ 0 ≤ b ^ p⁻¹

pp: p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ 0 ≤ b ^ p⁻¹

Tactic:
one_mul,

Goal state after:
p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ x✝ ^ q * rexp (-b * x✝ ^ p) = x✝ ^ q * rexp (-(b * x✝ ^ p))

case hx
p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ 0 < b

p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ p ≠ 0

case hx
p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ 0 ≤ b

case hx
p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ 0 ≤ b

p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ 0 ≤ b ^ p⁻¹

p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ 0 ≤ b ^ p⁻¹
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
a b c : E
ω : E → E →L[𝕜] F
γab : Path a b
γbc : Path b c
h₁ : CurveIntegrable ω γab
h₂ : CurveIntegrable ω γbc
instF : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
⊢ ∫ᶜ (x : E) in γab.trans γbc, ω x = ∫ᶜ (x : E) in γab, ω x + ∫ᶜ (x : E) in γbc, ω x

Tactic:
rw [curveIntegral_def, ← intervalIntegral.integral_add_adjacent_intervals
    (h₁.intervalIntegrable_curveIntegralFun_trans_left γbc)
    (h₂.intervalIntegrable_curveIntegralFun_trans_right γab),
    intervalIntegral.integral_congr_ae_restrict (curveIntegralFun_trans_aeeq_left _ _ _),
    intervalIntegral.integral_congr_ae_restrict (curveIntegralFun_trans_aeeq_right _ _ _)]

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
a b c : E
ω : E → E →L[𝕜] F
γab : Path a b
γbc : Path b c
h₁ : CurveIntegrable ω γab
h₂ : CurveIntegrable ω γbc
instF : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
⊢ (∫ (x : ℝ) in 0..1 / 2, 2 • curveIntegralFun ω γab (2 * x)) +
      ∫ (x : ℝ) in 1 / 2..1, 2 • curveIntegralFun ω γbc (2 * x - 1) =
    ∫ᶜ (x : E) in γab, ω x + ∫ᶜ (x : E) in γbc, ω x
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b C : ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hnorm : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ C
s : Set ℝ := toMeasurable volume {x | deriv f x ≠ 0}
hsm : MeasurableSet s
⊢ ∫ (t : ℝ) in a..b, s.indicator (fun x ↦ C) t = C * volume.real {x | x ∈ Ioo a b ∧ deriv f x ≠ 0}

Tactic:
rw [intervalIntegral.integral_of_le hab, Measure.restrict_congr_set Ioo_ae_eq_Ioc.symm,
        integral_indicator hsm, Measure.restrict_restrict hsm,
        setIntegral_const, smul_eq_mul, mul_comm]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b C : ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hnorm : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ C
s : Set ℝ := toMeasurable volume {x | deriv f x ≠ 0}
hsm : MeasurableSet s
⊢ C * volume.real (s ∩ Ioo a b) = C * volume.real {x | x ∈ Ioo a b ∧ deriv f x ≠ 0}
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral

Goal state before:
pp: case e'_3
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
hfc : ContinuousOn f (segment ℝ a b)
hfd : ∀ t ∈ Ioo 0 1, LineDifferentiableAt ℝ f ((lineMap a b) t) (b - a)
hf' : ∀ᵐ (t : ℝ), t ∈ Ioo 0 1 → ‖lineDeriv ℝ f ((lineMap a b) t) (b - a)‖ ≤ C
g : ℝ → F := fun t ↦ f ((lineMap a b) t)
hgc : ContinuousOn g (Icc 0 1)
hdg : ∀ t ∈ Ioo 0 1, HasDerivAt g (lineDeriv ℝ f ((lineMap a b) t) (b - a)) t
this : ‖g 1 - g 0‖ ≤ C * volume.real {t | t ∈ Ioo 0 1 ∧ deriv g t ≠ 0}
⊢ ‖f b - f a‖ = ‖g 1 - g 0‖

Tactic:
simp [g]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule

Goal state before:
pp: f : ℝ → ℝ
a b : ℝ
⊢ trapezoidal_integral f 1 a b = (b - a) / 2 * (f a + f b)

Tactic:
simp [trapezoidal_integral, mul_comm_div]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule

Goal state before:
pp: f : ℝ → ℝ
N : ℕ
a h : ℝ
N_nonzero : 0 < N
⊢ ∑ x ∈ Finset.range N, 1 * h / 2 * (f (a + ↑x * h) + f (a + (↑x + 1) * h)) =
    ↑N * h / ↑N * ((f a + f (a + ↑N * h)) / 2 + ∑ x ∈ Finset.range (N - 1), f (a + (↑x + 1) * (↑N * h) / ↑N))

Tactic:
one_mul,

Goal state after:
f : ℝ → ℝ
N : ℕ
a h : ℝ
N_nonzero : 0 < N
⊢ ∑ x ∈ Finset.range N, h / 2 * (f (a + ↑x * h) + f (a + (↑x + 1) * h)) =
    ↑N * h / ↑N * ((f a + f (a + ↑N * h)) / 2 + ∑ x ∈ Finset.range (N - 1), f (a + (↑x + 1) * (↑N * h) / ↑N))
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
s₀ s₁ t : Set X
s₀_compact : IsCompact s₀
s₁_compact : IsCompact s₁
t_compact : IsCompact t
disj : s₀ᶜ ∪ s₁ᶜ = univ
hst : s₀ ∪ s₁ ⊆ t
so : Fin 2 → Set X := fun j ↦ if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun j ↦ if j = 0 then s₀ᶜ else s₁ᶜ
soopen : ∀ (j : Fin 2), IsOpen (so j)
x : X
hx : x ∈ t
⊢ x ∈ univ

Tactic:
exact mem_univ _

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule

Goal state before:
pp: f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h : ℝ := (b - a) / ↑N
ak : ℕ → ℝ := fun k ↦ a + ↑k * h
h0 : ∀ (k : ℕ), ak (k + 1) - ak k = h
hab : 0 < b - a
hpos : 0 < h
hb : b = a + ↑N * h
k : ℕ
hk : k < N
h1 : a ≤ ak k
h2 : ak (k + 1) ≤ b
h3 : Set.Icc (ak k) (ak (k + 1)) ⊆ Set.Icc a b
h4 : ak k < ak (k + 1)
h5 :
  EqOn (_root_.derivWithin f (Set.Icc a b)) (_root_.derivWithin f (Set.Icc (ak k) (ak (k + 1))))
    (Set.Icc (ak k) (ak (k + 1)))
x : ℝ
hx : x ∈ Set.Icc (ak k) (ak (k + 1))
⊢ iteratedDerivWithin 2 f (Set.Icc a b) x = iteratedDerivWithin 2 f (Set.Icc (ak k) (ak (k + 1))) x

Tactic:
simp only [iteratedDerivWithin_succ', iteratedDerivWithin_zero]

Goal state after:
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h : ℝ := (b - a) / ↑N
ak : ℕ → ℝ := fun k ↦ a + ↑k * h
h0 : ∀ (k : ℕ), ak (k + 1) - ak k = h
hab : 0 < b - a
hpos : 0 < h
hb : b = a + ↑N * h
k : ℕ
hk : k < N
h1 : a ≤ ak k
h2 : ak (k + 1) ≤ b
h3 : Set.Icc (ak k) (ak (k + 1)) ⊆ Set.Icc a b
h4 : ak k < ak (k + 1)
h5 :
  EqOn (_root_.derivWithin f (Set.Icc a b)) (_root_.derivWithin f (Set.Icc (ak k) (ak (k + 1))))
    (Set.Icc (ak k) (ak (k + 1)))
x : ℝ
hx : x ∈ Set.Icc (ak k) (ak (k + 1))
⊢ _root_.derivWithin (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b) x =
    _root_.derivWithin (_root_.derivWithin f (Set.Icc (ak k) (ak (k + 1)))) (Set.Icc (ak k) (ak (k + 1))) x
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K : Compacts X
b : ℝ≥0∞
hb : ∀ (i : Compacts X), b ≤ ⨅ (_ : ↑K ⊆ interior ↑i), ↑(rieszContentAux Λ i)
this : b < ∞
ε : ℝ≥0
hε : 0 < ↑ε
f : X →C_c ℝ≥0
hfleoneonK : ∀ x ∈ K, 1 ≤ f x
hfle : ↑(Λ f) < ↑(sInf (⇑Λ '' {f | ∀ x ∈ K, 1 ≤ f x}) + NNReal.mk ↑ε ⋯)
α : ℝ≥0
hα : 1 < α
⊢ b.toNNReal ≤ Λ f * α

Tactic:
mul_comm,

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K : Compacts X
b : ℝ≥0∞
hb : ∀ (i : Compacts X), b ≤ ⨅ (_ : ↑K ⊆ interior ↑i), ↑(rieszContentAux Λ i)
this : b < ∞
ε : ℝ≥0
hε : 0 < ↑ε
f : X →C_c ℝ≥0
hfleoneonK : ∀ x ∈ K, 1 ≤ f x
hfle : ↑(Λ f) < ↑(sInf (⇑Λ '' {f | ∀ x ∈ K, 1 ≤ f x}) + NNReal.mk ↑ε ⋯)
α : ℝ≥0
hα : 1 < α
⊢ b.toNNReal ≤ α * Λ f
Module: Mathlib.MeasureTheory.Integral.TorusIntegral

Goal state before:
pp: n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : (Fin n → ℂ) → E
c : Fin n → ℂ
R : Fin n → ℝ
inst✝ : NormedSpace ℂ E
hf : TorusIntegrable f c R
⊢ IntegrableOn (fun θ ↦ (∏ i, ↑(R i) * cexp (↑(θ i) * I) * I) • f (torusMap c R θ)) (Icc 0 fun x ↦ 2 * π) volume

Tactic:
refine (hf.norm.const_mul (∏ i, |R i|)).mono' ?_ ?_
  · refine (Continuous.aestronglyMeasurable ?_).smul hf.1; fun_prop
  simp [norm_smul]

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Card

Goal state before:
pp: α : Type u
s : Set (Set α)
⊢ generateMeasurableRec s (ω_ 1) = ⋃ i, ⋃ (_ : i < ω_ 1), generateMeasurableRec s i

Tactic:
by
  apply (iUnion₂_subset fun i h => generateMeasurableRec_mono s h.le).antisymm'
  intro t ht
  rw [mem_iUnion₂]
  refine generateMeasurableRec_induction ?_ ?_ ?_ ?_ ht
  · intro t ht
    exact ⟨0, omega_pos 1, self_subset_generateMeasurableRec s 0 ht⟩
  · exact ⟨0, omega_pos 1, empty_mem_generateMeasurableRec s 0⟩
  · rintro u - ⟨j, hj, hj'⟩
    exact ⟨_, (isSuccLimit_omega 1).succ_lt hj,
      compl_mem_generateMeasurableRec (Order.lt_succ j) hj'⟩
  · intro f H
    choose I hI using fun n => (H n).1
    simp_rw [exists_prop] at hI
    refine ⟨_, Ordinal.lift_iSup_add_one_lt_of_lt_cof ?_ fun n => (hI n).1,
      iUnion_mem_generateMeasurableRec fun n => ⟨_, Ordinal.lt_iSup_add_one I n, (hI n).2⟩⟩
    simp

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Card

Goal state before:
pp: α : Type u
s : Set (Set α)
i✝¹ i✝ i : Ordinal.{v}
IH : ∀ y < i, y ≤ ω_ 1 → #↑(generateMeasurableRec s y) ≤ max (#↑s) 2 ^ ℵ₀
hi : Ordinal.lift.{u, v} i ≤ (ℵ_ 1).ord
A : 𝔠 ≤ max (#↑s) 2 ^ ℵ₀
B : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
⊢ Cardinal.lift.{u, v} i.card ≤ Cardinal.lift.{v, u} (max (#↑s) 2) ^ ℵ₀

Tactic:
have H := card_le_of_le_ord hi

Goal state after:
α : Type u
s : Set (Set α)
i✝¹ i✝ i : Ordinal.{v}
IH : ∀ y < i, y ≤ ω_ 1 → #↑(generateMeasurableRec s y) ≤ max (#↑s) 2 ^ ℵ₀
hi : Ordinal.lift.{u, v} i ≤ (ℵ_ 1).ord
A : 𝔠 ≤ max (#↑s) 2 ^ ℵ₀
B : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
H : (Ordinal.lift.{u, v} i).card ≤ ℵ_ 1
⊢ Cardinal.lift.{u, v} i.card ≤ Cardinal.lift.{v, u} (max (#↑s) 2) ^ ℵ₀
Module: Mathlib.Topology.Separation.CompletelyRegular

Goal state before:
pp: case h.right.right
ι : Type u_1
X : Type u_2
t : ι → TopologicalSpace X
ht : ∀ (i : ι), CompletelyRegularSpace X
this : TopologicalSpace X := ⨅ i, t i
x : X
I' : Finset ι
V U : ↥I' → Set X
hUV : ∀ (i : ↥I'), U i ⊆ V i
fs : ↥I' → X → ↑I
hfs : ∀ (i : ↥I'), Continuous[t ↑i, _] (fs i)
hxfs : ∀ (i : ↥I'), fs i x = 0
hfsU : ∀ (i : ↥I') ⦃x : X⦄, x ∈ (U i)ᶜ → fs i x = ⊤
⊢ ∀ (x : X) (i : ↥I'), x ∈ (V i)ᶜ → ∃ b, fs b x = ⊤

Tactic:
intro x i hxi

Goal state after:
case h.right.right
ι : Type u_1
X : Type u_2
t : ι → TopologicalSpace X
ht : ∀ (i : ι), CompletelyRegularSpace X
this : TopologicalSpace X := ⨅ i, t i
x✝ : X
I' : Finset ι
V U : ↥I' → Set X
hUV : ∀ (i : ↥I'), U i ⊆ V i
fs : ↥I' → X → ↑I
hfs : ∀ (i : ↥I'), Continuous[t ↑i, _] (fs i)
hxfs : ∀ (i : ↥I'), fs i x✝ = 0
hfsU : ∀ (i : ↥I') ⦃x : X⦄, x ∈ (U i)ᶜ → fs i x = ⊤
x : X
i : ↥I'
hxi : x ∈ (V i)ᶜ
⊢ ∃ b, fs b x = ⊤
Module: Mathlib.Topology.Separation.CompletelyRegular

Goal state before:
pp: ι : Type u_1
X : Type u_2
t : ι → TopologicalSpace X
ht : ∀ (i : ι), CompletelyRegularSpace X
⊢ CompletelyRegularSpace X

Tactic:
let := (⨅ i, t i) -- register this as default topological space to reduce `@`s
  rw [completelyRegularSpace_iff_isOpen]
  intro x K hK hxK
  simp_rw [← hK.mem_nhds_iff, nhds_iInf, mem_iInf, exists_finite_iff_finset,
    Finset.coe_sort_coe] at hxK; clear hK
  obtain ⟨I', V, hV, rfl⟩ := hxK
  simp only [mem_nhds_iff] at hV
  choose U hUV hU hxU using hV
  replace hU := fun (i : ↥I') =>
    @CompletelyRegularSpace.completely_regular_isOpen _ (t i) (ht i) x (U i) (hU i) (hxU i)
  clear hxU
  choose fs hfs hxfs hfsU using hU
  use I'.attach.sup fs
  constructorm* _ ∧ _
  · solve_by_elim [Continuous.finset_sup, continuous_iInf_dom]
  · simpa [show (0 : ↥I) = ⊥ from rfl] using hxfs
  · simp only [EqOn, Pi.one_apply, show (1 : ↥I) = ⊤ from rfl] at hfsU ⊢
    conv => equals ∀ x i, x ∈ (V i)ᶜ → ∃ b, fs b x = ⊤ => simp [Finset.sup_eq_top_iff]
    intro x i hxi
    specialize hfsU i (by tauto_set)
    exists i

Goal state after:
Module: Mathlib.Topology.Separation.CompletelyRegular

Goal state before:
pp: case refine_2
X : Type u
inst✝ : TopologicalSpace X
h : TopologicalSpace.IsTopologicalBasis {s | IsClopen s}
x✝ : X
K : Set X
hK : IsClosed[inst✝] K
hx✝¹ : x✝ ∉ K
s : Set X
hs : s ∈ {s | IsClopen s}
hx✝ : x✝ ∈ s
hsK : s ⊆ Kᶜ
x : X
hx : x ∈ K
⊢ x ∈ sᶜ

Tactic:
· exact (mem_compl_iff s x).mpr fun hs ↦ hsK hs hx

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

Goal state before:
pp: X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : T0Space X
x : X
⊢ diracProba x ∈ range diracProba

Tactic:
exact mem_range_self x

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

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace Ω
μ ν : Measure Ω
c : ℝ≥0∞
h : levyProkhorovEDist μ ν < c
B : Set Ω
B_mble : MeasurableSet B
⊢ μ B ≤ ν (thickening c.toReal B) + c

Tactic:
by
  obtain ⟨c', ⟨hc', lt_c⟩⟩ := sInf_lt_iff.mp h
  exact meas_le_of_le_of_forall_le_meas_thickening_add μ ν lt_c.le (hc' B B_mble).1

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

Goal state before:
pp: α : Type u_1
inst✝⁹ : MeasurableSpace α
β : Type u_2
inst✝⁸ : MeasurableSpace β
inst✝⁷ : TopologicalSpace α
inst✝⁶ : TopologicalSpace β
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : SecondCountableTopology β
inst✝³ : PseudoMetrizableSpace α
inst✝² : PseudoMetrizableSpace β
inst✝¹ : OpensMeasurableSpace α
inst✝ : OpensMeasurableSpace β
μ : ProbabilityMeasure α × ProbabilityMeasure β
S : Set (Set (α × β)) :=
  {t | ∃ a b, MeasurableSet a ∧ μ.1 (frontier a) = 0 ∧ MeasurableSet b ∧ μ.2 (frontier b) = 0 ∧ t = a ×ˢ b}
this✝¹ : IsPiSystem S
this✝ : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
u : Set (α × β)
u_open : IsOpen[instTopologicalSpaceProd] u
x : α × β
xu : x ∈ u
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ u
r : ℝ
hr : r ∈ Ioo 0 ε
r' : ℝ
hr' : r' ∈ Ioo 0 ε
μr : ↑μ.1 (frontier (ball x.1 r)) = 0
μr' : ↑μ.2 (frontier (ball x.2 r')) = 0
⊢ ball x.1 r ×ˢ ball x.2 r' ⊆ ball x.1 ε ×ˢ ball x.2 ε

Tactic:
by gcongr; exacts [hr.2.le, hr'.2.le]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.DistribChar

Goal state before:
pp: G : Type u_1
A : Type u_2
inst✝¹⁰ : Group G
inst✝⁹ : AddCommGroup A
inst✝⁸ : DistribMulAction G A
inst✝⁷ : TopologicalSpace A
inst✝⁶ : IsTopologicalAddGroup A
inst✝⁵ : LocallyCompactSpace A
inst✝⁴ : ContinuousConstSMul G A
inst✝³ : MeasurableSpace A
inst✝² : BorelSpace A
μ : Measure A
inst✝¹ : μ.IsAddHaarMeasure
inst✝ : μ.Regular
g : G
s : Set A
⊢ ↑((distribHaarChar A) g) * μ s = μ (g • s)

Tactic:
have : (DomMulAct.mk g • μ) s = μ (g • s) := by simp [domSMul_apply]

Goal state after:
G : Type u_1
A : Type u_2
inst✝¹⁰ : Group G
inst✝⁹ : AddCommGroup A
inst✝⁸ : DistribMulAction G A
inst✝⁷ : TopologicalSpace A
inst✝⁶ : IsTopologicalAddGroup A
inst✝⁵ : LocallyCompactSpace A
inst✝⁴ : ContinuousConstSMul G A
inst✝³ : MeasurableSpace A
inst✝² : BorelSpace A
μ : Measure A
inst✝¹ : μ.IsAddHaarMeasure
inst✝ : μ.Regular
g : G
s : Set A
this : (DomMulAct.mk g • μ) s = μ (g • s)
⊢ ↑((distribHaarChar A) g) * μ s = μ (g • s)
Module: Mathlib.MeasureTheory.Measure.Haar.Extension

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst✝¹³ : Group A
inst✝¹² : Group B
inst✝¹¹ : Group C
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : TopologicalSpace B
inst✝⁸ : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst✝⁷ : IsTopologicalGroup A
inst✝⁶ : IsTopologicalGroup B
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace A
inst✝³ : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst✝² : NormedSpace ℝ E
inst✝¹ : IsTopologicalGroup C
inst✝ : LocallyCompactSpace B
f : CompactlySupportedContinuousMap B E
this : UniformSpace B := IsTopologicalGroup.rightUniformSpace B
b : B
ε : ℝ
hε : ε > 0
⊢ ∀ᶠ (x : B) in nhds b, dist (∫ (a : A), (H.pullback f x) a ∂μA) (∫ (a : A), (H.pullback f b) a ∂μA) < ε

Tactic:
obtain ⟨U₀, hU₀, hb⟩ := exists_compact_mem_nhds b

Goal state after:
A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst✝¹³ : Group A
inst✝¹² : Group B
inst✝¹¹ : Group C
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : TopologicalSpace B
inst✝⁸ : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst✝⁷ : IsTopologicalGroup A
inst✝⁶ : IsTopologicalGroup B
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace A
inst✝³ : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst✝² : NormedSpace ℝ E
inst✝¹ : IsTopologicalGroup C
inst✝ : LocallyCompactSpace B
f : CompactlySupportedContinuousMap B E
this : UniformSpace B := IsTopologicalGroup.rightUniformSpace B
b : B
ε : ℝ
hε : ε > 0
U₀ : Set B
hU₀ : IsCompact U₀
hb : U₀ ∈ nhds b
⊢ ∀ᶠ (x : B) in nhds b, dist (∫ (a : A), (H.pullback f x) a ∂μA) (∫ (a : A), (H.pullback f b) a ∂μA) < ε
Module: Mathlib.MeasureTheory.Measure.Haar.Extension

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst✝¹⁸ : Group A
inst✝¹⁷ : Group B
inst✝¹⁶ : Group C
inst✝¹⁵ : TopologicalSpace A
inst✝¹⁴ : TopologicalSpace B
inst✝¹³ : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst✝¹² : IsTopologicalGroup A
inst✝¹¹ : IsTopologicalGroup B
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : MeasurableSpace A
inst✝⁸ : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : IsTopologicalGroup C
inst✝⁵ : LocallyCompactSpace B
inst✝⁴ : MeasurableSpace C
inst✝³ : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
inst✝² : T2Space B
inst✝¹ : MeasurableSpace B
inst✝ : BorelSpace B
K : Set B
hK : IsCompact K
⊢ (H.inducedMeasure μA μC) K < ⊤

Tactic:
obtain ⟨f, hf1, hf2, hf3, hf4⟩ :=
      exists_continuousMap_one_of_isCompact_subset_isOpen hK isOpen_univ K.subset_univ
    exact lt_of_le_of_lt (RealRMK.rieszMeasure_le_of_eq_one (f := ⟨f, hf2⟩) _
      (fun x ↦ (hf4 x).1) hK (fun x hx ↦ hf1 hx)) ENNReal.ofReal_lt_top

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

Goal state before:
pp: case inr.refine_5
Ω : Type u_1
inst✝³ : PseudoMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
inst✝ : SeparableSpace Ω
ε : ℝ
ε_pos : 0 < ε
h✝ : Nonempty Ω
xs : ℕ → Ω
xs_dense : DenseRange xs
half_ε_pos : 0 < ε / 2
Bs : ℕ → Set Ω := fun n ↦ ball (xs n) (ε / 2)
As : ℕ → Set Ω := disjointed Bs
⊢ Pairwise fun n m ↦ Disjoint (As n) (As m)

Tactic:
· exact disjoint_disjointed Bs

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

Goal state before:
pp: case inr
E : Type u_1
p : ℝ
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hp : 0 < p
hE : Nontrivial E
this✝ : 0 < ↑(finrank ℝ E)
this :
  (∫ (y : ℝ) in Set.Ioi 0, y ^ (finrank ℝ E - 1) • Real.exp (-y ^ p)) / Real.Gamma (↑(finrank ℝ E) / p + 1) *
      ↑(finrank ℝ E) =
    1
⊢ μ (Metric.ball 0 1) =
    ENNReal.ofReal
      (↑(finrank ℝ E) *
        (μ.real (Metric.ball 0 1) *
          ((∫ (y : ℝ) in Set.Ioi 0, y ^ (finrank ℝ E - 1) • Real.exp (-y ^ p)) / Real.Gamma (↑(finrank ℝ E) / p + 1))))

Tactic:
mul_comm,

Goal state after:
case inr
E : Type u_1
p : ℝ
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hp : 0 < p
hE : Nontrivial E
this✝ : 0 < ↑(finrank ℝ E)
this :
  (∫ (y : ℝ) in Set.Ioi 0, y ^ (finrank ℝ E - 1) • Real.exp (-y ^ p)) / Real.Gamma (↑(finrank ℝ E) / p + 1) *
      ↑(finrank ℝ E) =
    1
⊢ μ (Metric.ball 0 1) =
    ENNReal.ofReal
      (μ.real (Metric.ball 0 1) *
          ((∫ (y : ℝ) in Set.Ioi 0, y ^ (finrank ℝ E - 1) • Real.exp (-y ^ p)) / Real.Gamma (↑(finrank ℝ E) / p + 1)) *
        ↑(finrank ℝ E))
Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

Goal state before:
pp: case e'_3
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℂ), 0 ≤ ∑ i, ‖x i‖ ^ p
h₂ : ∀ (x : ι → ℂ), 0 ≤ (∑ i, ‖x i‖ ^ p) ^ (1 / p)
hr : 0 < r
⊢ ENNReal.ofReal (r ^ (2 * card ι)) = ENNReal.ofReal (r ^ (Finset.univ.card * 2))

Tactic:
mul_comm,

Goal state after:
case e'_3
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℂ), 0 ≤ ∑ i, ‖x i‖ ^ p
h₂ : ∀ (x : ι → ℂ), 0 ≤ (∑ i, ‖x i‖ ^ p) ^ (1 / p)
hr : 0 < r
⊢ ENNReal.ofReal (r ^ (card ι * 2)) = ENNReal.ofReal (r ^ (Finset.univ.card * 2))
Module: Mathlib.MeasureTheory.Measure.TightNormed

Goal state before:
pp: case neg
E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst✝³ : NormedAddCommGroup E
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
h : Tendsto (fun r ↦ ⨆ μ ∈ S, μ {x | r < ‖x‖}) atTop (𝓝 0)
y : E
this : ProperSpace E
hy : ¬y = 0
h' : Tendsto (fun r ↦ ⨆ μ ∈ S, μ {x | r * ‖y‖⁻¹ < ‖x‖}) atTop (𝓝 0)
r : ℝ
⊢ (fun r ↦ ⨆ μ ∈ S, μ {x | r < ‖⟪y, x⟫_𝕜‖}) r ≤ (fun r ↦ ⨆ μ ∈ S, μ {x | r * ‖y‖⁻¹ < ‖x‖}) r

Tactic:
have h_le (μ : Measure E) : μ {x | r < ‖⟪y, x⟫_𝕜‖} ≤ μ {x | r * ‖y‖⁻¹ < ‖x‖} := by
    refine measure_mono fun x hx ↦ ?_
    simp only [Set.mem_ofPred_eq] at hx ⊢
    rw [mul_inv_lt_iff₀]
    · rw [mul_comm]
      exact hx.trans_le (norm_inner_le_norm y x)
    · positivity

Goal state after:
case neg
E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst✝³ : NormedAddCommGroup E
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
h : Tendsto (fun r ↦ ⨆ μ ∈ S, μ {x | r < ‖x‖}) atTop (𝓝 0)
y : E
this : ProperSpace E
hy : ¬y = 0
h' : Tendsto (fun r ↦ ⨆ μ ∈ S, μ {x | r * ‖y‖⁻¹ < ‖x‖}) atTop (𝓝 0)
r : ℝ
h_le : ∀ (μ : Measure E), μ {x | r < ‖⟪y, x⟫_𝕜‖} ≤ μ {x | r * ‖y‖⁻¹ < ‖x‖}
⊢ (fun r ↦ ⨆ μ ∈ S, μ {x | r < ‖⟪y, x⟫_𝕜‖}) r ≤ (fun r ↦ ⨆ μ ∈ S, μ {x | r * ‖y‖⁻¹ < ‖x‖}) r