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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : Preorder β
inst✝¹ : OrderClosedTopology β
inst✝ : PseudoMetrizableSpace β
f g : α → β
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
x : α
⊢ f x = AEStronglyMeasurable.mk f hf x →
    g x = AEStronglyMeasurable.mk g hg x →
      {a | AEStronglyMeasurable.mk f hf a < AEStronglyMeasurable.mk g hg a} x = {a | f a < g a} x

Tactic:
hfx

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : Preorder β
inst✝¹ : OrderClosedTopology β
inst✝ : PseudoMetrizableSpace β
f g : α → β
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
x : α
hfx : f x = AEStronglyMeasurable.mk f hf x
⊢ g x = AEStronglyMeasurable.mk g hg x →
    {a | AEStronglyMeasurable.mk f hf a < AEStronglyMeasurable.mk g hg a} x = {a | f a < g a} x
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : Preorder β
inst✝¹ : OrderClosedTopology β
inst✝ : PseudoMetrizableSpace β
f g : α → β
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
x : α
⊢ f x = AEStronglyMeasurable.mk f hf x →
    g x = AEStronglyMeasurable.mk g hg x →
      {a | AEStronglyMeasurable.mk f hf a ≤ AEStronglyMeasurable.mk g hg a} x = {a | f a ≤ g a} x

Tactic:
hfx

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : Preorder β
inst✝¹ : OrderClosedTopology β
inst✝ : PseudoMetrizableSpace β
f g : α → β
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
x : α
hfx : f x = AEStronglyMeasurable.mk f hf x
⊢ g x = AEStronglyMeasurable.mk g hg x →
    {a | AEStronglyMeasurable.mk f hf a ≤ AEStronglyMeasurable.mk g hg a} x = {a | f a ≤ g a} x
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_5
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m m0 : MeasurableSpace α
μ : Measure α
hf : StronglyMeasurable f
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
x : α
⊢ ‖f x‖ ≤ c → Tendsto (fun n ↦ (hf.approxBounded c n) x) atTop (𝓝 (f x))

Tactic:
hfx

Goal state after:
α : Type u_1
β : Type u_5
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m m0 : MeasurableSpace α
μ : Measure α
hf : StronglyMeasurable f
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
x : α
hfx : ‖f x‖ ≤ c
⊢ Tendsto (fun n ↦ (hf.approxBounded c n) x) atTop (𝓝 (f x))
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
m₀ : MeasurableSpace α
μ : Measure α
inst✝¹ : PseudoMetrizableSpace β
inst✝ : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : IsEmbedding g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this✝³ : MeasurableSpace β := borel β
this✝² : BorelSpace β
this✝¹ : MeasurableSpace γ := borel γ
this✝ : BorelSpace γ
H : AEStronglyMeasurable (fun x ↦ g (f x)) μ
t : Set γ
ht : IsSeparable t
h't : ∀ᵐ (x : α) ∂μ, g (f x) ∈ t
⊢ ∃ t, IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, f x ∈ t

Tactic:
exact ⟨g ⁻¹' t, hg.isSeparable_preimage ht, h't⟩

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (x : α) in s, f x ∂μ ≤ (⨆ x ∈ s, f x) * μ s

Tactic:
calc ∫⁻ x in s, f x ∂μ
  _ ≤ ∫⁻ y in s, ⨆ x ∈ s, f x ∂μ :=
    setLIntegral_mono' hs fun x hx ↦ le_iSup₂ (f := fun x _ ↦ f x) x hx
  _ = (⨆ x ∈ s, f x) * μ s := by simp

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

Goal state before:
pp: case right
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ∞
g : α → ℝ≥0∞
hmg : Measurable g
hgf : g ≤ f
hifg : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ
s : Set α
hms : MeasurableSet s
⊢ ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ

Tactic:
rw [← compl_compl s, setLIntegral_compl hms.compl, setLIntegral_compl hms.compl, hifg]

Goal state after:
case right
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ∞
g : α → ℝ≥0∞
hmg : Measurable g
hgf : g ≤ f
hifg : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ
s : Set α
hms : MeasurableSet s
⊢ ∫⁻ (a : α), g a ∂μ - ∫⁻ (x : α) in sᶜ, f x ∂μ ≤ ∫⁻ (x : α), g x ∂μ - ∫⁻ (x : α) in sᶜ, g x ∂μ

case right
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ∞
g : α → ℝ≥0∞
hmg : Measurable g
hgf : g ≤ f
hifg : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ
s : Set α
hms : MeasurableSet s
⊢ ∫⁻ (x : α) in sᶜ, g x ∂μ ≠ ∞

case right
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ∞
g : α → ℝ≥0∞
hmg : Measurable g
hgf : g ≤ f
hifg : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ
s : Set α
hms : MeasurableSet s
⊢ ∫⁻ (x : α) in sᶜ, f x ∂μ ≠ ∞
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : SubtractionMonoid β
inst✝ : ContinuousNeg β
hf : FinStronglyMeasurable f μ
⊢ FinStronglyMeasurable (-f) μ

Tactic:
by
  refine ⟨fun n ↦ -hf.approx n, fun n ↦ ?_, fun x ↦ (hf.tendsto_approx x).neg⟩
  suffices μ (Function.support fun x ↦ -(hf.approx n) x) < ∞ by convert! this
  rw [Function.support_fun_neg (hf.approx n)]
  exact hf.fin_support_approx n

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

Goal state before:

Tactic:
edist (f x) (f y)
      _ ≤ edist (f z) (f x) + edist (f z) (f y) := edist_triangle_left _ _ _
      _ ≤ (K _ z.2) * edist z.1 x + edist (f z) (f y) := add_le_add_left
        (hf _ z.2 ⟨mem_ball_self <| hε _ z.2, z.2⟩ ⟨hx'.2.trans <| half_lt_self <| hε _ z.2, hx⟩) _
      _ ≤ (K _ z.2) * edist z.1 x + (K' _ z.2) * edist z.1 y :=
        add_le_add_right (hK' _ z.2 _ ⟨hy, hy'⟩) _
      _ ≤ (K _ z.2) * edist z.1 x + (K' _ z.2) * (edist x z.1 + edist x y) := by
        gcongr; exact edist_triangle_left z.1 y x
      _ ≤ (K _ z.2) * edist x y + (K' _ z.2) * (edist x y + edist x y) := by
        simp_rw [edist_dist, dist_comm _ x]
        gcongr <;> linarith [mem_ball.1 hx'.2, (not_lt (α := ℝ)).1 hy', dist_triangle_left y z x]
      _ = ↑(K _ z.2 + 2 * K' _ z.2) * edist x y := by push_cast; ring
      _ ≤ _ := by gcongr; exact .trans (by rfl) (t.le_sup hz)

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
ε : ℝ
p : Z
⊢ glueDist Φ Ψ ε (Sum.inl (Φ p)) (Sum.inr (Ψ p)) = ε

Tactic:
have : ⨅ q, dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q) = 0 := by
    have A : ∀ q, 0 ≤ dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q) := fun _ => by positivity
    refine le_antisymm ?_ (le_ciInf A)
    have : 0 = dist (Φ p) (Φ p) + dist (Ψ p) (Ψ p) := by simp
    rw [this]
    exact ciInf_le ⟨0, forall_mem_range.2 A⟩ p

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
ε : ℝ
p : Z
this : ⨅ q, dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q) = 0
⊢ glueDist Φ Ψ ε (Sum.inl (Φ p)) (Sum.inr (Ψ p)) = ε
Module: Mathlib.Topology.MetricSpace.Polish

Goal state before:
pp: case refine_4.refine_1
α : Type u_1
β : Type u_2
inst✝ : MetricSpace α
s : Opens α
t : Set s.CompleteCopy
h : IsOpen t
x : s.CompleteCopy
hx : x ∈ t
⊢ ∃ ε > 0, ∀ (y : s.CompleteCopy), dist x y < ε → y ∈ t

pp: case refine_4.refine_2
α : Type u_1
β : Type u_2
inst✝ : MetricSpace α
s : Opens α
t : Set s.CompleteCopy
h : ∀ x ∈ t, ∃ ε > 0, ∀ (y : s.CompleteCopy), dist x y < ε → y ∈ t
x : s.CompleteCopy
hx : x ∈ t
⊢ t ∈ 𝓝 x

Tactic:
· rcases (Metric.isOpen_iff (α := s)).1 h x hx with ⟨ε, ε0, hε⟩
      exact ⟨ε, ε0, fun y hy ↦ hε <| (dist_comm _ _).trans_lt <| (dist_val_le_dist _ _).trans_lt hy⟩

Goal state after:
case refine_4.refine_2
α : Type u_1
β : Type u_2
inst✝ : MetricSpace α
s : Opens α
t : Set s.CompleteCopy
h : ∀ x ∈ t, ∃ ε > 0, ∀ (y : s.CompleteCopy), dist x y < ε → y ∈ t
x : s.CompleteCopy
hx : x ∈ t
⊢ t ∈ 𝓝 x
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: case mp.inl
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
hs : IsOpen[instTopologicalSpaceSigma] s
i : ι
x : E i
hx : ⟨i, x⟩ ∈ s
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ Sigma.mk i ⁻¹' s
y : E i
hy : dist ⟨i, x⟩ ⟨i, y⟩ < min ε 1
⊢ ⟨i, y⟩ ∈ s

Tactic:
simp only [Sigma.dist_same, lt_min_iff] at hy

Goal state after:
case mp.inl
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
hs : IsOpen[instTopologicalSpaceSigma] s
i : ι
x : E i
hx : ⟨i, x⟩ ∈ s
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ Sigma.mk i ⁻¹' s
y : E i
hy : dist x y < ε ∧ dist x y < 1
⊢ ⟨i, y⟩ ∈ s
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: case mp.inl
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
hs : IsOpen[instTopologicalSpaceSigma] s
i : ι
x : E i
hx : ⟨i, x⟩ ∈ s
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ Sigma.mk i ⁻¹' s
y : E i
hy : dist ⟨i, x⟩ ⟨i, y⟩ < min ε 1
⊢ ⟨i, y⟩ ∈ s

Tactic:
simp only [Sigma.dist_same, lt_min_iff] at hy
      exact hε (mem_ball'.2 hy.1)

Goal state after:
Module: Mathlib.SetTheory.Cardinal.ENNReal

Goal state before:
pp: case inl
α : Type u_1
h✝ : Finite α
⊢ (↑(ENat.card α)).toReal = ↑(Nat.card α)

Tactic:
simp [ENat.card_eq_coe_natCard]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.ENNReal

Goal state before:
pp: case inr
α : Type u_1
h✝ : Infinite α
⊢ (↑(ENat.card α)).toReal = ↑(Nat.card α)

Tactic:
simp [ENat.card_eq_coe_natCard]

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

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
f g : (ℕ → ℕ) → α
hf : Continuous[_, inst✝³] f
hg : Continuous[_, inst✝³] g
h : Disjoint (range f) (range g)
hfg : ¬MeasurablySeparable (range f) (range g)
n : ℕ
x y : ℕ → ℕ
H :
  ∀ (x' y' : ℕ → ℕ),
    x' ∈ cylinder x n → y' ∈ cylinder y n → MeasurablySeparable (f '' cylinder x' (n + 1)) (g '' cylinder y' (n + 1))
⊢ MeasurablySeparable (⋃ i, f '' cylinder (update x n i) (n + 1)) (⋃ i, g '' cylinder (update y n i) (n + 1))

Tactic:
refine MeasurablySeparable.iUnion fun i j => ?_

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
f g : (ℕ → ℕ) → α
hf : Continuous[_, inst✝³] f
hg : Continuous[_, inst✝³] g
h : Disjoint (range f) (range g)
hfg : ¬MeasurablySeparable (range f) (range g)
n : ℕ
x y : ℕ → ℕ
H :
  ∀ (x' y' : ℕ → ℕ),
    x' ∈ cylinder x n → y' ∈ cylinder y n → MeasurablySeparable (f '' cylinder x' (n + 1)) (g '' cylinder y' (n + 1))
i j : ℕ
⊢ MeasurablySeparable (f '' cylinder (update x n i) (n + 1)) (g '' cylinder (update y n j) (n + 1))
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α → ℝ≥0∞
a_mble : Measurable a
c : ℝ≥0∞
tsum_le_c : ∑' (i : α), a i ≤ c
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
ε_ne_top : ε ≠ ∞
⊢ count {i | ε ≤ a i} ≤ c / ε

Tactic:
by
  rw [← lintegral_count] at tsum_le_c
  apply (MeasureTheory.meas_ge_le_lintegral_div a_mble.aemeasurable ε_ne_zero ε_ne_top).trans
  exact ENNReal.div_le_div tsum_le_c rfl.le

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ≥0∞
⊢ ∃ g, Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ

Tactic:
by
  -- We only need to prove the `≤` inequality for the integrals, the other one follows from `g ≤ f`.
  rsuffices ⟨g, hgm, hgle, hleg⟩ :
      ∃ g : α → ℝ≥0∞, Measurable g ∧ g ≤ f ∧ ∀ s, ∫⁻ a in s, f a ∂μ ≤ ∫⁻ a in s, g a ∂μ
  · exact ⟨g, hgm, hgle, fun s ↦ (hleg s).antisymm (lintegral_mono hgle)⟩
  -- Without loss of generality, `μ` is a finite measure.
  wlog h : IsFiniteMeasure μ generalizing μ
  · choose g hgm hgle hgint using fun n ↦ @this (sfiniteSeq μ n) _ inferInstance
    refine ⟨fun x ↦ ⨆ n, g n x, .iSup hgm, fun x ↦ iSup_le (hgle · x), fun s ↦ ?_⟩
    rw [← sum_sfiniteSeq μ, Measure.restrict_sum_of_countable,
      lintegral_sum_measure, lintegral_sum_measure]
    exact ENNReal.tsum_le_tsum fun n ↦ (hgint n s).trans (lintegral_mono fun x ↦ le_iSup (g · x) _)
  -- According to `exists_measurable_le_lintegral_eq`, for any natural `n`
  -- we can choose a measurable function $g_{n}$
  -- such that $g_{n}(x) ≤ \min (f(x), n)$ for all $x$
  -- and both sides have the same integral over the whole space w.r.t. $μ$.
  have (n : ℕ) : ∃ g : α → ℝ≥0∞, Measurable g ∧ g ≤ f ∧ g ≤ n ∧
      ∫⁻ a, min (f a) n ∂μ = ∫⁻ a, g a ∂μ := by
    simpa [and_assoc] using exists_measurable_le_lintegral_eq μ (f ⊓ n)
  choose g hgm hgf hgle hgint using this
  -- Let `φ` be the pointwise supremum of the functions $g_{n}$.
  -- Clearly, `φ` is a measurable function and `φ ≤ f`.
  set φ : α → ℝ≥0∞ := fun x ↦ ⨆ n, g n x
  have hφm : Measurable φ := by fun_prop
  have hφle : φ ≤ f := fun x ↦ iSup_le (hgf · x)
  refine ⟨φ, hφm, hφle, fun s ↦ ?_⟩
  -- Now we show the inequality between set integrals.
  -- Choose a simple function `ψ ≤ f` with values in `ℝ≥0` and prove for `ψ`.
  rw [lintegral_eq_nnreal]
  refine iSup₂_le fun ψ hψ ↦ ?_
  -- Choose `n` such that `ψ x ≤ n` for all `x`.
  obtain ⟨n, hn⟩ : ∃ n : ℕ, ∀ x, ψ x ≤ n := by
    rcases ψ.range.bddAbove with ⟨C, hC⟩
    exact ⟨⌈C⌉₊, fun x ↦ (hC <| ψ.mem_range_self x).trans (Nat.le_ceil _)⟩
  calc
    (ψ.map (↑)).lintegral (μ.restrict s) = ∫⁻ a in s, ψ a ∂μ :=
      SimpleFunc.lintegral_eq_lintegral .. |>.symm
    _ ≤ ∫⁻ a in s, min (f a) n ∂μ :=
      lintegral_mono fun a ↦ le_min (hψ _) (ENNReal.coe_le_coe.2 (hn a))
    _ ≤ ∫⁻ a in s, g n a ∂μ := by
      have : ∫⁻ a in (toMeasurable μ s)ᶜ, min (f a) n ∂μ ≠ ∞ :=
        IsFiniteMeasure.lintegral_lt_top_of_bounded_to_ennreal _ ⟨n, fun _ ↦ min_le_right ..⟩ |>.ne
      have hsm : MeasurableSet (toMeasurable μ s) := measurableSet_toMeasurable ..
      apply ENNReal.le_of_add_le_add_right this
      rw [← μ.restrict_toMeasurable_of_sFinite, lintegral_add_compl _ hsm, hgint,
        ← lintegral_add_compl _ hsm]
      gcongr with x
      exact le_min (hgf n x) (hgle n x)
    _ ≤ _ := lintegral_mono fun x ↦ le_iSup (g · x) n

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
m : MeasurableSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
μ : Measure X
inst✝ : μ.IsOpenPosMeasure
U : Set X
f g : X → Y
h : f =ᵐ[μ.restrict U] g
hU : IsOpen[inst✝³] U
hf : ContinuousOn f U
hg : ContinuousOn g U
⊢ EqOn f g U

Tactic:
by
  replace h := ae_imp_of_ae_restrict h
  simp only [ae_iff, Classical.not_imp] at h
  have : IsOpen (U ∩ { a | f a ≠ g a }) := by
    refine isOpen_iff_mem_nhds.mpr fun a ha => inter_mem (hU.mem_nhds ha.1) ?_
    rcases ha with ⟨ha : a ∈ U, ha' : (f a, g a) ∈ (diagonal Y)ᶜ⟩
    exact
      (hf.continuousAt (hU.mem_nhds ha)).prodMk_nhds (hg.continuousAt (hU.mem_nhds ha))
        (isClosed_diagonal.isOpen_compl.mem_nhds ha')
  replace := (this.eq_empty_of_measure_zero h).le
  exact fun x hx => Classical.not_not.1 fun h => this ⟨hx, h⟩

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

Goal state before:
pp: α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
n : ℕ
ihn : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), μ (closedBall x (2 ^ n * (2 * ε))) ≤ ↑C ^ n * μ (closedBall x (2 * ε))
ε : ℝ
⊢ (∀ (x : α), μ (closedBall x (2 ^ n * (2 * ε))) ≤ ↑C ^ n * μ (closedBall x (2 * ε))) →
    (∀ (x : α), μ (closedBall x (2 * ε)) ≤ ↑(doublingConstant μ) * μ (closedBall x ε)) →
      ∀ (x : α), μ (closedBall x (2 ^ (n + 1) * ε)) ≤ ↑C ^ (n + 1) * μ (closedBall x ε)

Tactic:
hεn

Goal state after:
α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
n : ℕ
ihn : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), μ (closedBall x (2 ^ n * (2 * ε))) ≤ ↑C ^ n * μ (closedBall x (2 * ε))
ε : ℝ
hεn : ∀ (x : α), μ (closedBall x (2 ^ n * (2 * ε))) ≤ ↑C ^ n * μ (closedBall x (2 * ε))
⊢ (∀ (x : α), μ (closedBall x (2 * ε)) ≤ ↑(doublingConstant μ) * μ (closedBall x ε)) →
    ∀ (x : α), μ (closedBall x (2 ^ (n + 1) * ε)) ≤ ↑C ^ (n + 1) * μ (closedBall x ε)
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
⊢ Measurable fun x ↦ ν (Prod.mk x ⁻¹' s)

Tactic:
by
  rw [← sum_sfiniteSeq ν]
  simp_rw [Measure.sum_apply_of_countable]
  exact Measurable.tsum (fun i ↦ measurable_measure_prodMk_left_finite hs)

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U : Set α
H : μ.InnerRegularWRT p q
hU : q U
⊢ μ U = ⨆ K, ⨆ (_ : K ⊆ U), ⨆ (_ : p K), μ K

Tactic:
refine
    le_antisymm (le_of_forall_lt fun r hr => ?_) (iSup₂_le fun K hK => iSup_le fun _ => μ.mono hK)
  simpa only [lt_iSup_iff, exists_prop] using H hU r hr

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case fst
G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g : G
k : ↥K
this : (hSK.equiv (g * ↑k)).1 = (hSK.equiv g).1
⊢ ↑(hSK.equiv (g * ↑k)).1 = ↑((hSK.equiv g).1, (hSK.equiv g).2 * k).1

pp: case snd
G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g : G
k : ↥K
this : (hSK.equiv (g * ↑k)).1 = (hSK.equiv g).1
⊢ ↑(hSK.equiv (g * ↑k)).2 = ↑((hSK.equiv g).1, (hSK.equiv g).2 * k).2

Tactic:
· rw [this]

Goal state after:
case snd
G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g : G
k : ↥K
this : (hSK.equiv (g * ↑k)).1 = (hSK.equiv g).1
⊢ ↑(hSK.equiv (g * ↑k)).2 = ↑((hSK.equiv g).1, (hSK.equiv g).2 * k).2
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case refine_2.snd
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
h : ↥H
g : G
this : (hHT.equiv (↑h * g)).2 = (hHT.equiv g).2
⊢ ↑(hHT.equiv (↑h * g)).2 = ↑(h * (hHT.equiv g).1, (hHT.equiv g).2).2

Tactic:
· rw [this]

Goal state after:
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 + ε
⊢ μ.WeaklyRegular

Tactic:
refine
      { outerRegular := fun s hs r hr => ?_
        innerRegular := H }

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
⊢ ∃ U ⊇ s, IsOpen[inst✝²] U ∧ μ U < r
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : InvolutiveInv G
inst✝¹ : MeasurableInv G
μ : Measure G
inst✝ : μ.IsInvInvariant
A : Set G
⊢ μ A⁻¹ = μ A

Tactic:
← inv_apply,

Goal state after:
G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : InvolutiveInv G
inst✝¹ : MeasurableInv G
μ : Measure G
inst✝ : μ.IsInvInvariant
A : Set G
⊢ μ.inv A = μ A
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hX : AEMeasurable X μ
⊢ (map (fun a ↦ (X a, Y a)) μ).snd = map Y μ

Tactic:
by
  by_cases hY : AEMeasurable Y μ
  · ext1 s hs
    rw [Measure.snd_apply hs, Measure.map_apply_of_aemeasurable (hX.prodMk hY) (measurable_snd hs),
      Measure.map_apply_of_aemeasurable hY hs, ← univ_prod, mk_preimage_prod, preimage_univ,
      univ_inter]
  · have : ¬AEMeasurable (fun x ↦ (X x, Y x)) μ := by
      contrapose hY
      exact measurable_snd.comp_aemeasurable hY
    simp [map_of_not_aemeasurable, hY, this]

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

Goal state before:
pp: case inr
G : Type u_1
H : Type u_2
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
μ✝ : Measure G
inst✝⁶ : μ✝.IsHaarMeasure
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : BorelSpace G
inst✝³ : T1Space G
inst✝² : WeaklyLocallyCompactSpace G
inst✝¹ : (𝓝[≠] 1).NeBot
μ : Measure G
inst✝ : μ.IsHaarMeasure
h : μ 1 ≠ 0
⊢ NullSingletonClass μ

Tactic:
obtain ⟨K, K_compact, K_nhds⟩ : ∃ K : Set G, IsCompact K ∧ K ∈ 𝓝 1 := exists_compact_mem_nhds 1
    have K_inf : Set.Infinite K := infinite_of_mem_nhds (1 : G) K_nhds
    exact absurd (K_inf.meas_eq_top ⟨_, h, fun x _ ↦ (haar_singleton _ _).ge⟩)
      K_compact.measure_lt_top.ne

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

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : μ.Regular
x : ℝ≥0∞
hx : x ≠ ∞
⊢ (x • μ).Regular

Tactic:
by
  have := OuterRegular.smul μ hx
  have := IsFiniteMeasureOnCompacts.smul μ hx
  exact ⟨Regular.innerRegular.smul x⟩

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

Goal state before:
pp: case mp.ht
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᵐ[μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : g =ᵐ[μ.withDensity fun x ↦ ↑(f x)] g'
A : MeasurableSet {x | f' x ≠ 0}
⊢ ∀ᵐ (x : α) ∂μ.restrict {x | f' x ≠ 0}, (fun x ↦ ↑(f x) * g x) x = (fun x ↦ ↑(f' x) * g' x) x

pp: case mp.htc
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᵐ[μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : g =ᵐ[μ.withDensity fun x ↦ ↑(f x)] g'
A : MeasurableSet {x | f' x ≠ 0}
⊢ ∀ᵐ (x : α) ∂μ.restrict {x | f' x ≠ 0}ᶜ, (fun x ↦ ↑(f x) * g x) x = (fun x ↦ ↑(f' x) * g' x) x

Tactic:
· rw [EventuallyEq, ae_withDensity_iff' hf.coe_nnreal_ennreal] at hg'
      rw [ae_restrict_iff' A]
      filter_upwards [hg', hf'_ae] with a ha h'a h_a_nonneg
      have : (f' a : ℝ≥0∞) ≠ 0 := by simpa only [Ne, ENNReal.coe_eq_zero] using h_a_nonneg
      rw [← h'a] at this ⊢
      rw [ha this]

Goal state after:
case mp.htc
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᵐ[μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : g =ᵐ[μ.withDensity fun x ↦ ↑(f x)] g'
A : MeasurableSet {x | f' x ≠ 0}
⊢ ∀ᵐ (x : α) ∂μ.restrict {x | f' x ≠ 0}ᶜ, (fun x ↦ ↑(f x) * g x) x = (fun x ↦ ↑(f' x) * g' x) x