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

Goal state before:
pp: α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hF_meas : AEMeasurable F μ
hf_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
g : ℕ → α → ℝ≥0∞
gmeas : ∀ (n : ℕ), Measurable (g n)
gf : ∀ (n : ℕ), g n ≤ f n
hg : ∀ (n : ℕ), ∫⁻ (a : α), f n a ∂μ = ∫⁻ (a : α), g n a ∂μ
g' : ℕ → α → ℝ≥0∞ := ⋯
M : ∀ (n : ℕ), Measurable (g' n)
I : ∀ (n : ℕ) (x : α), g n x ≤ g' n x
I' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), g' n x ≤ f n x
Int_eq : ∀ (n : ℕ), ∫⁻ (x : α), g' n x ∂μ = ∫⁻ (x : α), f n x ∂μ
⊢ Tendsto (fun i ↦ ∫⁻ (a : α), g' i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))

Tactic:
simp_rw [Int_eq]

Goal state after:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hF_meas : AEMeasurable F μ
hf_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
g : ℕ → α → ℝ≥0∞
gmeas : ∀ (n : ℕ), Measurable (g n)
gf : ∀ (n : ℕ), g n ≤ f n
hg : ∀ (n : ℕ), ∫⁻ (a : α), f n a ∂μ = ∫⁻ (a : α), g n a ∂μ
g' : ℕ → α → ℝ≥0∞ := fun t ↦ Nat.rec (motive := fun x ↦ α → ℝ≥0∞) (g 0) (fun n I x ↦ max (g (n + 1) x) (I x)) t
M : ∀ (n : ℕ), Measurable (g' n)
I : ∀ (n : ℕ) (x : α), g n x ≤ g' n x
I' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), g' n x ≤ f n x
Int_eq : ∀ (n : ℕ), ∫⁻ (x : α), g' n x ∂μ = ∫⁻ (x : α), f n x ∂μ
⊢ Tendsto (fun i ↦ ∫⁻ (x : α), f i x ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case mp
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
⊢ y ∈ cylinder x n → cylinder y n = cylinder x n

pp: case mpr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
⊢ cylinder y n = cylinder x n → y ∈ cylinder x n

Tactic:
· intro hy
    apply Subset.antisymm
    · intro z hz i hi
      rw [← hy i hi]
      exact hz i hi
    · intro z hz i hi
      rw [hy i hi]
      exact hz i hi

Goal state after:
case mpr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
⊢ cylinder y n = cylinder x n → y ∈ cylinder x n
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case mp.succ.inl
α : Type u_2
x y : ℕ → α
n : ℕ
ih : res x n = res y n → ∀ ⦃m : ℕ⦄, m < n → x m = y m
m : ℕ
h : x n = y n ∧ res x n = res y n
hm : m < n
⊢ x m = y m

pp: case mp.succ.inr
α : Type u_2
x y : ℕ → α
n : ℕ
ih : res x n = res y n → ∀ ⦃m : ℕ⦄, m < n → x m = y m
m : ℕ
h : x n = y n ∧ res x n = res y n
hm : m = n
⊢ x m = y m

Tactic:
· exact ih h.2 hm

Goal state after:
case mp.succ.inr
α : Type u_2
x y : ℕ → α
n : ℕ
ih : res x n = res y n → ∀ ⦃m : ℕ⦄, m < n → x m = y m
m : ℕ
h : x n = y n ∧ res x n = res y n
hm : m = n
⊢ x m = y m
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: α : Type u_2
x : ℕ → α
n : ℕ
y : ℕ → α
⊢ (∀ i < n, y i = x i) ↔ res y n = res x n

Tactic:
res_eq_res

Goal state after:
α : Type u_2
x : ℕ → α
n : ℕ
y : ℕ → α
⊢ (∀ i < n, y i = x i) ↔ ∀ ⦃m : ℕ⦄, m < n → y m = x m
Module: Mathlib.Topology.MetricSpace.CantorScheme

Goal state before:
pp: case succ
β : Type u_1
α : Type u_2
A : List β → Set α
x y : ↑(inducedMap A).fst
hxy : (inducedMap A).snd x = (inducedMap A).snd y
n : ℕ
ih : res (↑x) n = res (↑y) n
hA : ¬↑x n = ↑y n
⊢ ∃ x_1 ∈ A (↑x n :: res (↑x) n), x_1 ∈ A (↑y n :: res (↑x) n)

Tactic:
refine ⟨(inducedMap A).2 x, ?_, ?_⟩

Goal state after:
case succ.refine_1
β : Type u_1
α : Type u_2
A : List β → Set α
x y : ↑(inducedMap A).fst
hxy : (inducedMap A).snd x = (inducedMap A).snd y
n : ℕ
ih : res (↑x) n = res (↑y) n
hA : ¬↑x n = ↑y n
⊢ (inducedMap A).snd x ∈ A (↑x n :: res (↑x) n)

case succ.refine_2
β : Type u_1
α : Type u_2
A : List β → Set α
x y : ↑(inducedMap A).fst
hxy : (inducedMap A).snd x = (inducedMap A).snd y
n : ℕ
ih : res (↑x) n = res (↑y) n
hA : ¬↑x n = ↑y n
⊢ (inducedMap A).snd x ∈ A (↑y n :: res (↑x) n)
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: case mpr
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
H : ∀ x ∈ s, ∃ ε > 0, ∀ (y : (i : ι) × E i), dist x y < ε → y ∈ s
i : ι
x : E i
hx : x ∈ Sigma.mk i ⁻¹' s
⊢ ∃ ε > 0, ball x ε ⊆ Sigma.mk i ⁻¹' s

Tactic:
obtain ⟨ε, εpos, hε⟩ : ∃ ε > 0, ∀ y, dist (⟨i, x⟩ : Σ j, E j) y < ε → y ∈ s :=
      H ⟨i, x⟩ hx

Goal state after:
case mpr
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
H : ∀ x ∈ s, ∃ ε > 0, ∀ (y : (i : ι) × E i), dist x y < ε → y ∈ s
i : ι
x : E i
hx : x ∈ Sigma.mk i ⁻¹' s
ε : ℝ
εpos : ε > 0
hε : ∀ (y : (j : ι) × E j), dist ⟨i, x⟩ y < ε → y ∈ s
⊢ ∃ ε > 0, ball x ε ⊆ Sigma.mk i ⁻¹' s
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
⊢ IsTopologicalBasis {s | ∃ x n, s = cylinder x n}

Tactic:
by
  apply isTopologicalBasis_of_isOpen_of_nhds
  · rintro u ⟨x, n, rfl⟩
    apply isOpen_cylinder
  · intro x u hx u_open
    obtain ⟨v, ⟨U, F, -, rfl⟩, xU, Uu⟩ :
        ∃ v ∈ { S : Set (∀ i : ℕ, E i) | ∃ (U : ∀ i : ℕ, Set (E i)) (F : Finset ℕ),
          (∀ i : ℕ, i ∈ F → U i ∈ { s : Set (E i) | IsOpen s }) ∧ S = (F : Set ℕ).pi U },
        x ∈ v ∧ v ⊆ u :=
      (isTopologicalBasis_pi fun n : ℕ => isTopologicalBasis_opens).exists_subset_of_mem_open hx
        u_open
    rcases Finset.bddAbove F with ⟨n, hn⟩
    refine ⟨cylinder x (n + 1), ⟨x, n + 1, rfl⟩, self_mem_cylinder _ _, Subset.trans ?_ Uu⟩
    intro y hy
    suffices ∀ i : ℕ, i ∈ F → y i ∈ U i by simpa
    intro i hi
    have : y i = x i := mem_cylinder_iff.1 hy i ((hn hi).trans_lt (lt_add_one n))
    rw [this]
    simp only [Set.mem_pi, Finset.mem_coe] at xU
    exact xU i hi

Goal state after:
Module: Mathlib.Dynamics.Ergodic.MeasurePreserving

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
hf : MeasurePreserving f μa μb
hfe : MeasurableEmbedding f
s : Set β
⊢ μa (f ⁻¹' s) = μb s

Tactic:
rw [← hf.map_eq, hfe.map_apply]

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

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

Tactic:
rw [disjoint_iff_inf_le]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
⊢ ae μ ⊓ ae ν ≤ ⊥
Module: Mathlib.MeasureTheory.Measure.MutuallySingular

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : μ sᶜ = 0
t : Set α
ht : ν tᶜ = 0
hst : Disjoint s t
⊢ Disjoint μ ν

Tactic:
rw [disjoint_iff_inf_le]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : μ sᶜ = 0
t : Set α
ht : ν tᶜ = 0
hst : Disjoint s t
⊢ μ ⊓ ν ≤ ⊥
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: case inr
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f : α → ℝ≥0∞
this :
  ∀ {f : α → ℝ≥0∞},
    AEMeasurable f m.join → Measurable f → ∫⁻ (x : α), f x ∂m.join = ∫⁻ (μ : Measure α), ∫⁻ (x : α), f x ∂μ ∂m
hfm : ¬Measurable f
g : α → ℝ≥0∞
hgm : Measurable g
hfg : f =ᵐ[m.join] g
⊢ ∫⁻ (x : α), f x ∂m.join = ∫⁻ (μ : Measure α), ∫⁻ (x : α), f x ∂μ ∂m

Tactic:
rw [lintegral_congr_ae hfg, this hgm.aemeasurable hgm]

Goal state after:
case inr
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f : α → ℝ≥0∞
this :
  ∀ {f : α → ℝ≥0∞},
    AEMeasurable f m.join → Measurable f → ∫⁻ (x : α), f x ∂m.join = ∫⁻ (μ : Measure α), ∫⁻ (x : α), f x ∂μ ∂m
hfm : ¬Measurable f
g : α → ℝ≥0∞
hgm : Measurable g
hfg : f =ᵐ[m.join] g
⊢ ∫⁻ (μ : Measure α), ∫⁻ (x : α), g x ∂μ ∂m = ∫⁻ (μ : Measure α), ∫⁻ (x : α), f x ∂μ ∂m
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

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

Tactic:
have hφm : Measurable φ := by fun_prop

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ✝ : Measure α
f : α → ℝ≥0∞
μ : Measure α
inst✝ : SFinite μ
h : IsFiniteMeasure μ
g : ℕ → α → ℝ≥0∞
hgm : ∀ (n : ℕ), Measurable (g n)
hgf : ∀ (n : ℕ), g n ≤ f
hgle : ∀ (n : ℕ), g n ≤ ↑n
hgint : ∀ (n : ℕ), ∫⁻ (a : α), min (f a) ↑n ∂μ = ∫⁻ (a : α), g n a ∂μ
φ : α → ℝ≥0∞ := fun x ↦ ⨆ n, g n x
hφm : Measurable φ
⊢ ∃ g, Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set α
t : Set β
S : Set α := toMeasurable μ s
T : Set β := toMeasurable ν t
⊢ μ s * ν T = μ s * ν t

Tactic:
measure_toMeasurable

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set α
t : Set β
S : Set α := toMeasurable μ s
T : Set β := toMeasurable ν t
⊢ μ s * ν t = μ s * ν t
Module: Mathlib.MeasureTheory.Group.MeasurableEquiv

Goal state before:
pp: G : Type u_1
A : Type u_2
inst✝³ : Group G
inst✝² : MulAction G A
inst✝¹ : MeasurableSpace A
inst✝ : MeasurableConstSMul G A
μ✝ ν : Measure A
g✝ : G
g g' : Gᵈᵐᵃ
μ : Measure A
⊢ map (fun x ↦ DomMulAct.mk.symm (g * g')⁻¹ • x) μ =
    map ((fun x ↦ DomMulAct.mk.symm g⁻¹ • x) ∘ fun x ↦ DomMulAct.mk.symm g'⁻¹ • x) μ

pp: case hg
G : Type u_1
A : Type u_2
inst✝³ : Group G
inst✝² : MulAction G A
inst✝¹ : MeasurableSpace A
inst✝ : MeasurableConstSMul G A
μ✝ ν : Measure A
g✝ : G
g g' : Gᵈᵐᵃ
μ : Measure A
⊢ Measurable fun x ↦ DomMulAct.mk.symm g⁻¹ • x

pp: case hf
G : Type u_1
A : Type u_2
inst✝³ : Group G
inst✝² : MulAction G A
inst✝¹ : MeasurableSpace A
inst✝ : MeasurableConstSMul G A
μ✝ ν : Measure A
g✝ : G
g g' : Gᵈᵐᵃ
μ : Measure A
⊢ Measurable fun x ↦ DomMulAct.mk.symm g'⁻¹ • x

Tactic:
· simp [Function.comp_def, mul_smul]

Goal state after:
case hg
G : Type u_1
A : Type u_2
inst✝³ : Group G
inst✝² : MulAction G A
inst✝¹ : MeasurableSpace A
inst✝ : MeasurableConstSMul G A
μ✝ ν : Measure A
g✝ : G
g g' : Gᵈᵐᵃ
μ : Measure A
⊢ Measurable fun x ↦ DomMulAct.mk.symm g⁻¹ • x

case hf
G : Type u_1
A : Type u_2
inst✝³ : Group G
inst✝² : MulAction G A
inst✝¹ : MeasurableSpace A
inst✝ : MeasurableConstSMul G A
μ✝ ν : Measure A
g✝ : G
g g' : Gᵈᵐᵃ
μ : Measure A
⊢ Measurable fun x ↦ DomMulAct.mk.symm g'⁻¹ • x
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case hs
X : Type u_3
Z : Type u_5
inst✝³ : MeasurableSpace X
inst✝² : StandardBorelSpace X
inst✝¹ : MeasurableSpace Z
inst✝ : CountablySeparated Z
f : X → Z
hf : Measurable f
hsurj : Surjective f
s : Set Z
h : MeasurableSet (f ⁻¹' s)
τ : TopologicalSpace Z
left✝¹ : SecondCountableTopology Z
left✝ : T4Space Z
right✝ : OpensMeasurableSpace Z
⊢ AnalyticSet s

Tactic:
rw [← image_preimage_eq s hsurj]

Goal state after:
case hs
X : Type u_3
Z : Type u_5
inst✝³ : MeasurableSpace X
inst✝² : StandardBorelSpace X
inst✝¹ : MeasurableSpace Z
inst✝ : CountablySeparated Z
f : X → Z
hf : Measurable f
hsurj : Surjective f
s : Set Z
h : MeasurableSet (f ⁻¹' s)
τ : TopologicalSpace Z
left✝¹ : SecondCountableTopology Z
left✝ : T4Space Z
right✝ : OpensMeasurableSpace Z
⊢ AnalyticSet (f '' f ⁻¹' s)
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S T : Set G
g : G
x : ↑S × ↑T
hx : ↑x.1 * ↑x.2 = g
hx' : ∀ (y : ↑S × ↑T), (fun x ↦ ↑x.1 * ↑x.2 = g) y → y = x
⊢ (fun s ↦ (↑s)⁻¹ * g ∈ T) x.1

Tactic:
by simp [← hx]

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S T : Set G
g : G
x : ↑S × ↑T
hx : ↑x.1 * ↑x.2 = g
hx' : ∀ (y : ↑S × ↑T), (fun x ↦ ↑x.1 * ↑x.2 = g) y → y = x
⊢ (fun t ↦ g * (↑t)⁻¹ ∈ S) x.2

Tactic:
by simp [← hx]

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

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : μ.OuterRegular
A : Set α
r : ℝ≥0∞
hr : μ A < r
⊢ r > ?m.21 (toMeasurable μ A)

Tactic:
measure_toMeasurable

Goal state after:
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : μ.OuterRegular
A : Set α
r : ℝ≥0∞
hr : μ A < r
⊢ r > μ A
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
⊢ ∃ K ⊆ s, p K ∧ r < μ K

Tactic:
have h0 : p ∅ := by
    have : 0 < μ univ := (bot_le.trans_lt hr).trans_le (measure_mono (subset_univ _))
    obtain ⟨K, -, hK, -⟩ : ∃ K, K ⊆ univ ∧ p K ∧ 0 < μ K := H isOpen_univ _ this
    simpa using hd hK isOpen_univ

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
h0 : p ∅
⊢ ∃ K ⊆ s, p K ∧ r < μ K
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case h₂
γ : Type u_3
β : Type u_4
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : PolishSpace γ
inst✝³ : TopologicalSpace β
inst✝² : T2Space β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
f : γ → β
f_cont : Continuous[inst✝⁵, inst✝³] f
f_inj : Injective f
this✝² : UpgradedIsCompletelyMetrizableSpace γ := upgradeIsCompletelyMetrizable γ
b : Set (Set γ)
b_count : b.Countable
b_nonempty : ∅ ∉ b
hb : IsTopologicalBasis b
this✝¹ : Encodable ↑b
A : Type (max 0 u_3) := { p // Disjoint ↑p.1 ↑p.2 }
q : A → Set β
hq1 : ∀ (p : A), f '' ↑(↑p).1 ⊆ q p
hq2 : ∀ (p : A), Disjoint (f '' ↑(↑p).2) (q p)
q_meas : ∀ (p : A), MeasurableSet (q p)
E : ↑b → Set β := fun s ↦ closure[inst✝³] (f '' ↑s) ∩ ⋂ t, ⋂ (ht : Disjoint ↑s ↑t), q ⟨(s, t), ht⟩ \ q ⟨(t, s), ⋯⟩
u : ℕ → ℝ
u_anti : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
F : ℕ → Set β := fun n ↦ ⋃ s, ⋃ (_ : Bornology.IsBounded ↑s ∧ diam ↑s ≤ u n), E s
x : β
hx : x ∈ ⋂ n, F n
s : ℕ → ↑b
hs : ∀ (n : ℕ), Bornology.IsBounded ↑(s n) ∧ diam ↑(s n) ≤ u n
hxs : ∀ (n : ℕ), x ∈ E (s n)
y : ℕ → γ
hy : ∀ (n : ℕ), y n ∈ ↑(s n)
I : ∀ (m n : ℕ), (↑(s m) ∩ ↑(s n)).Nonempty
cauchy_y : CauchySeq y
this✝ : Nonempty γ
z : γ := atTop.limUnder y
y_lim : Tendsto y atTop (𝓝 z)
hne : f z ≠ x
v w : Set β
v_open : IsOpen[inst✝³] v
w_open : IsOpen[inst✝³] w
fzv : f z ∈ v
xw : x ∈ w
hvw : Disjoint v w
δ : ℝ
δpos : δ > 0
hδ : ball z δ ⊆ f ⁻¹' v
n : ℕ
hn : u n + dist (y n) z < δ
fsnv : f '' ↑(s n) ⊆ v
this : x ∈ closure[inst✝³] v
⊢ False

Tactic:
exact disjoint_left.1 (hvw.closure_left w_open) this xw

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
δ : Type u_4
inst✝² : MeasurableSpace δ
f : α → β
g : γ → δ
μa : Measure α
μc : Measure γ
inst✝¹ : SFinite μa
inst✝ : SFinite μc
hf : Measurable f
hg : Measurable g
i : ℕ × ℕ
s : Set β
t : Set δ
hs : MeasurableSet s
ht : MeasurableSet t
⊢ (map (Prod.map f g) ((sfiniteSeq μa i.1).prod (sfiniteSeq μc i.2))) (s ×ˢ t) =
    (map f (sfiniteSeq μa i.1)) s * (map g (sfiniteSeq μc i.2)) t

Tactic:
map_apply (hf.prodMap hg) (hs.prod ht),

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
δ : Type u_4
inst✝² : MeasurableSpace δ
f : α → β
g : γ → δ
μa : Measure α
μc : Measure γ
inst✝¹ : SFinite μa
inst✝ : SFinite μc
hf : Measurable f
hg : Measurable g
i : ℕ × ℕ
s : Set β
t : Set δ
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ((sfiniteSeq μa i.1).prod (sfiniteSeq μc i.2)) (Prod.map f g ⁻¹' s ×ˢ t) =
    (map f (sfiniteSeq μa i.1)) s * (map g (sfiniteSeq μc i.2)) t
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 α := {x | x ∈ t ∧ ¬ContinuousWithinAt g t x}
ht' : t'.Countable
this : g '' t = g '' (t \ t') ∪ g '' t'
x : α
hx : x ∈ t \ t'
⊢ ContinuousWithinAt g (t \ t') x

Tactic:
simp only [sdiff_sep_self, not_not, mem_ofPred_eq, t'] at hx

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 α := {x | x ∈ t ∧ ¬ContinuousWithinAt g t x}
ht' : t'.Countable
this : g '' t = g '' (t \ t') ∪ g '' t'
x : α
hx : x ∈ t ∧ ContinuousWithinAt g t x
⊢ ContinuousWithinAt g (t \ t') x
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
H : Type u_3
inst✝² : Group H
mH : MeasurableSpace H
inst✝¹ : MeasurableMul H
μ : Measure H
inst✝ : μ.IsMulRightInvariant
f : G →* H
hf : MeasurableEmbedding ⇑f
g : G
⊢ map (fun x ↦ x * g) (comap (⇑f) μ) = comap (⇑f) μ

Tactic:
ext s hs
    rw [map_apply (by fun_prop) hs]
    repeat rw [hf.comap_apply]
    have : f '' (· * g) ⁻¹' s = (· * f g) ⁻¹' f '' s := by
      ext
      constructor
      · rintro ⟨y, hy, rfl⟩
        exact ⟨y * g, hy, by simp⟩
      · intro ⟨y, yins, hy⟩
        exact ⟨y * g⁻¹, by simp [yins], by simp [hy]⟩
    rw [this, ← map_apply (by fun_prop), IsMulRightInvariant.map_mul_right_eq_self]
    exact hf.measurableSet_image.mpr hs

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

Goal state before:
pp: X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : PseudoMetrizableSpace X
inst✝ : MeasurableSpace X
μ : Measure X
A : PseudoMetricSpace X := pseudoMetrizableSpacePseudoMetric X
U : Set X
hU : IsOpen[inst✝²] U
r : ℝ≥0∞
hr : r < μ U
⊢ ∃ K ⊆ U, IsClosed[inst✝²] K ∧ r < μ K

Tactic:
rcases hU.exists_iUnion_isClosed with ⟨F, F_closed, -, rfl, F_mono⟩

Goal state after:
X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : PseudoMetrizableSpace X
inst✝ : MeasurableSpace X
μ : Measure X
A : PseudoMetricSpace X := pseudoMetrizableSpacePseudoMetric X
r : ℝ≥0∞
F : ℕ → Set X
F_closed : ∀ (n : ℕ), IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (F n)
F_mono : Monotone F
hU : IsOpen[inst✝²] (⋃ n, F n)
hr : r < μ (⋃ n, F n)
⊢ ∃ K ⊆ ⋃ n, F n, IsClosed[inst✝²] K ∧ r < μ K
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : R1Space α
inst✝ : OpensMeasurableSpace α
h : μ.InnerRegular
U : Set α
hU : IsOpen[inst✝²] U
r : ℝ≥0∞
hr : r < μ U
K : Set α
KU : K ⊆ U
K_comp : IsCompact K
hK : r < μ K
⊢ ∃ K ⊆ U, IsClosed[inst✝²] K ∧ r < μ K

Tactic:
exact ⟨closure K, K_comp.closure_subset_of_isOpen hU KU, isClosed_closure,
    hK.trans_le (measure_mono subset_closure)⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α ≃ₜ β
h : (map (⇑f) μ).InnerRegular
⊢ μ = map (⇑f.symm) (map (⇑f) μ)

Tactic:
rw [map_map f.symm.continuous.measurable f.continuous.measurable]

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α ≃ₜ β
h : (map (⇑f) μ).InnerRegular
⊢ μ = map (⇑f.symm ∘ ⇑f) μ
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✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
⊢ (ae μ)⁻¹ = ae μ

Tactic:
by
  refine le_antisymm (quasiMeasurePreserving_inv μ).tendsto_ae ?_
  nth_rewrite 1 [← inv_inv (ae μ)]
  exact Filter.map_mono (quasiMeasurePreserving_inv μ).tendsto_ae

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Measurable f
S : Set α := {x | f x < 0}
⊢ (μ.withDensity fun x ↦ ENNReal.ofReal (f x)) ⟂ₘ μ.withDensity fun x ↦ ENNReal.ofReal (-f x)

Tactic:
have hS : MeasurableSet S := measurableSet_lt hf measurable_const

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Measurable f
S : Set α := {x | f x < 0}
hS : MeasurableSet S
⊢ (μ.withDensity fun x ↦ ENNReal.ofReal (f x)) ⟂ₘ μ.withDensity fun x ↦ ENNReal.ofReal (-f x)
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : μ ({x | f x ≠ 0} ∩ s) = 0
t : Set α := ⋯
A : s ⊆ t ∪ {x | f x = 0}
⊢ μ t = 0

Tactic:
measure_toMeasurable

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : μ ({x | f x ≠ 0} ∩ s) = 0
t : Set α := toMeasurable μ ({x | f x ≠ 0} ∩ s)
A : s ⊆ t ∪ {x | f x = 0}
⊢ μ ({x | f x ≠ 0} ∩ s) = 0
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace α
h : μ.InnerRegularCompactLTTop
c : ℝ≥0∞
hc : ¬c = 0
h'c : ¬c = ∞
⊢ (c • μ).InnerRegularWRT IsCompact fun s ↦ MeasurableSet s ∧ (c • μ) s ≠ ∞

Tactic:
convert! InnerRegularWRT.smul h.innerRegular c using 2 with s

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace α
h : μ.InnerRegularCompactLTTop
c : ℝ≥0∞
hc : ¬c = 0
h'c : ¬c = ∞
s : Set α
⊢ MeasurableSet s ∧ (c • μ) s ≠ ∞ ↔ MeasurableSet s ∧ μ s ≠ ∞
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α ≃ₜ β
h : (map (⇑f) μ).Regular
⊢ μ = map (⇑f.symm) (map (⇑f) μ)

Tactic:
rw [map_map f.symm.continuous.measurable f.continuous.measurable]

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α ≃ₜ β
h : (map (⇑f) μ).Regular
⊢ μ = map (⇑f.symm ∘ ⇑f) μ
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case mpr
α : 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' : (fun x ↦ ↑(f x) * g x) =ᵐ[μ] g'
⊢ g =ᵐ[μ.withDensity fun x ↦ ↑(f x)] fun x ↦ (↑(f' x))⁻¹ * g' x

Tactic:
rw [EventuallyEq, ae_withDensity_iff' hf.coe_nnreal_ennreal]

Goal state after:
case mpr
α : 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' : (fun x ↦ ↑(f x) * g x) =ᵐ[μ] g'
⊢ ∀ᵐ (x : α) ∂μ, ↑(f x) ≠ 0 → g x = (↑(f' x))⁻¹ * g' x
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x : ℝ≥0
⊢ ↑(NNReal.sqrt x) = √↑x

Tactic:
by
  rw [Real.sqrt, Real.toNNReal_coe]

Goal state after: