mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s t : Set α
hs_finite : μ s ≠ ∞
⊢ μ (s ∩ t) < ∞

Tactic:
by
  finiteness

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s t : Set α
ht_finite : μ t ≠ ∞
⊢ μ (s ∩ t) < ∞

Tactic:
by
  finiteness

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
d : DynkinSystem α
s₁ s₂ : Set α
h₁ : d.Has s₁
h₂ : d.Has s₂
h : s₂ ⊆ s₁
⊢ d.Has (s₁ \ s₂)

Tactic:
by
  apply d.has_compl_iff.1
  simp only [sdiff_eq, compl_inter, compl_compl]
  exact d.has_union (d.has_compl h₁) h₂ (disjoint_compl_left.mono_right h)

Goal state after:
Module: Mathlib.MeasureTheory.Function.AEMeasurableSequence

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i) μ
x : α
hx : x ∈ aeSeqSet hf p
h_ss : aeSeqSet hf p ⊆ {x | p x fun n ↦ f n x}
⊢ p x fun n ↦ f n x

Tactic:
have hx' := Set.mem_of_subset_of_mem h_ss hx

Goal state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i) μ
x : α
hx : x ∈ aeSeqSet hf p
h_ss : aeSeqSet hf p ⊆ {x | p x fun n ↦ f n x}
hx' : x ∈ {x | p x fun n ↦ f n x}
⊢ p x fun n ↦ f n x
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: case pos
α : Type u_1
s : Set α
x : Set Prop
hT : True ∈ x
⊢ (fun x ↦ x ∈ s) ⁻¹' x = ∅ ∨ (fun x ↦ x ∈ s) ⁻¹' x = s ∨ (fun x ↦ x ∈ s) ⁻¹' x = sᶜ ∨ (fun x ↦ x ∈ s) ⁻¹' x = univ

pp: case neg
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
⊢ (fun x ↦ x ∈ s) ⁻¹' x = ∅ ∨ (fun x ↦ x ∈ s) ⁻¹' x = s ∨ (fun x ↦ x ∈ s) ⁻¹' x = sᶜ ∨ (fun x ↦ x ∈ s) ⁻¹' x = univ

Tactic:
· by_cases hF : False ∈ x
      · suffices x = univ by grind
        grind [univ_eq_true_false]
      · grind

Goal state after:
case neg
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
⊢ (fun x ↦ x ∈ s) ⁻¹' x = ∅ ∨ (fun x ↦ x ∈ s) ⁻¹' x = s ∨ (fun x ↦ x ∈ s) ⁻¹' x = sᶜ ∨ (fun x ↦ x ∈ s) ⁻¹' x = univ
Module: Mathlib.MeasureTheory.Measure.NullMeasurable

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hd : AEDisjoint μ s t
⊢ ∑' (i : Bool), μ (bif i then s else t) = μ s + μ t

pp: case hd
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hd : AEDisjoint μ s t
⊢ Pairwise (AEDisjoint μ on fun b ↦ bif b then s else t)

pp: case h
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hd : AEDisjoint μ s t
⊢ ∀ (i : Bool), NullMeasurableSet (bif i then s else t) μ

Tactic:
tsum_fintype,

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hd : AEDisjoint μ s t
⊢ ∑ b, μ (bif b then s else t) = μ s + μ t

case hd
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hd : AEDisjoint μ s t
⊢ Pairwise (AEDisjoint μ on fun b ↦ bif b then s else t)

case h
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hd : AEDisjoint μ s t
⊢ ∀ (i : Bool), NullMeasurableSet (bif i then s else t) μ
Module: Mathlib.MeasureTheory.Measure.Comap

Goal state before:
pp: α : Type u_1
β : Type u_2
ma : MeasurableSpace α
mb : MeasurableSpace β
μ : Measure α
e : α ≃ᵐ β
s : Set β
hs : MeasurableSet s
⊢ ∀ (s : Set β), MeasurableSet s → MeasurableSet (⇑e.symm '' s)

Tactic:
exact fun t ht ↦ e.symm.measurableSet_image.mpr ht

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
S : Set (Set α)
hs : S.Countable
hd : S.Pairwise (AEDisjoint μ)
h : ∀ s ∈ S, NullMeasurableSet s μ
⊢ μ (⋃₀ S) = ∑' (s : ↑S), μ ↑s

Tactic:
by
  rw [sUnion_eq_biUnion, measure_biUnion₀ hs hd h]

Goal state after:
Module: Mathlib.Topology.Order.AtTopBotIxx

Goal state before:
pp: case neg
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
b : X
hsne : s.Nonempty
this : Nonempty ↑s
hsub : ¬s ⊆ Iio b
⊢ comap Subtype.val (𝓝[<] b) = atTop ↔ s ⊆ Iio b ∧ ∀ a < b, (s ∩ Ioo a b).Nonempty

Tactic:
suffices ¬Tendsto (↑) (atTop : Filter s) (𝓝[<] b) by
      contrapose this
      simp_all [tendsto_iff_comap]

Goal state after:
case neg
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
b : X
hsne : s.Nonempty
this : Nonempty ↑s
hsub : ¬s ⊆ Iio b
⊢ ¬Tendsto Subtype.val atTop (𝓝[<] b)
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsCodirectedOrder ι
inst✝ : atBot.IsCountablyGenerated
s : ι → Set α
hs : ∀ᵐ (ω : α) ∂μ, Monotone fun x ↦ ω ∈ s x
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
i : ι
hi : μ (s i) ≠ ∞
this : Nonempty ι
t : ι → Set α := fun i ↦ s i ∩ {ω | Monotone fun x ↦ ω ∈ s x}
hst : ∀ (i : ι), s i =ᵐ[μ] t i
hMono : Monotone t
⊢ μ (⋂ i, s i) = ⨅ i, μ (t i)

Tactic:
← hMono.measure_iInter (fun i ↦ (hsm i).congr (hst i)) ⟨i, by rwa [← measure_congr (hst i)]⟩

Goal state after:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsCodirectedOrder ι
inst✝ : atBot.IsCountablyGenerated
s : ι → Set α
hs : ∀ᵐ (ω : α) ∂μ, Monotone fun x ↦ ω ∈ s x
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
i : ι
hi : μ (s i) ≠ ∞
this : Nonempty ι
t : ι → Set α := fun i ↦ s i ∩ {ω | Monotone fun x ↦ ω ∈ s x}
hst : ∀ (i : ι), s i =ᵐ[μ] t i
hMono : Monotone t
⊢ μ (⋂ i, s i) = μ (⋂ i, t i)
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : s ⊆ t
h : μ.restrict t = ν.restrict t
⊢ μ.restrict s = ν.restrict s

Tactic:
rw [← restrict_restrict_of_subset hs, h, restrict_restrict_of_subset hs]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
m : ℝ≥0∞ := ⨆ D ∈ {D | D ⊆ C ∧ D.Countable}, μ (⋃₀ D)
hm : ⊥ < m
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 m
u_lim : Tendsto u atTop (𝓝 m)
D : ℕ → Set (Set α)
D_mem : ∀ (n : ℕ), D n ∈ {D | D ⊆ C ∧ D.Countable}
huD : ∀ (n : ℕ), u n < μ (⋃₀ D n)
⊢ ∃ D ∈ {D | D ⊆ C ∧ D.Countable}, μ (⋃₀ D) = m

Tactic:
have hD : ⋃ n, D n ∈ {D | D ⊆ C ∧ D.Countable} := by simp; grind

Goal state after:
case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
m : ℝ≥0∞ := ⨆ D ∈ {D | D ⊆ C ∧ D.Countable}, μ (⋃₀ D)
hm : ⊥ < m
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 m
u_lim : Tendsto u atTop (𝓝 m)
D : ℕ → Set (Set α)
D_mem : ∀ (n : ℕ), D n ∈ {D | D ⊆ C ∧ D.Countable}
huD : ∀ (n : ℕ), u n < μ (⋃₀ D n)
hD : ⋃ n, D n ∈ {D | D ⊆ C ∧ D.Countable}
⊢ ∃ D ∈ {D | D ⊆ C ∧ D.Countable}, μ (⋃₀ D) = m
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
c : ℝ≥0∞
μ : Measure α
⊢ c • μ = 0 ↔ c = 0 ∨ μ = 0

Tactic:
simp [Measure.ext_iff', forall_or_left]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure β
s : Set β
⊢ Measure.comap f (μ.restrict s) = (Measure.comap f μ).restrict (f ⁻¹' s)

Tactic:
by
  ext t ht
  rw [Measure.restrict_apply ht, comap_apply hf, comap_apply hf,
    Measure.restrict_apply (hf.measurableSet_image.2 ht), image_inter_preimage]

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

Goal state before:
pp: case refine_4
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
⊢ ∀ (s : ℕ → Set α),
    (∀ (n : ℕ), MeasurableSet (s n)) →
      (∀ (n : ℕ), ∃ q, s n = ⋃ p, if q p then countablyGeneratedAtom α p else ∅) →
        ∃ q, ⋃ i, s i = ⋃ p, if q p then countablyGeneratedAtom α p else ∅

Tactic:
· intro t ht h
    choose q hq using h
    refine ⟨fun p ↦ ⨆ n, q n p, ?_⟩
    ext
    simp [hq]
    grind

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: case intro.refine_1
α : Type u_1
β : Type u_2
ι✝ : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
μ✝ ν : Measure α
s t : Set α
a : α
ι : Type u_4
inst✝¹ : Finite ι
μ : ι → Measure α
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
val✝ : Fintype ι
this : ∀ (n : ℕ), MeasurableSet (⋂ i, spanningSets (μ i) n)
n : ℕ
⊢ ∑' (i : ι), (μ i) (⋂ i, spanningSets (μ i) n) < ∞

Tactic:
tsum_fintype,

Goal state after:
case intro.refine_1
α : Type u_1
β : Type u_2
ι✝ : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
μ✝ ν : Measure α
s t : Set α
a : α
ι : Type u_4
inst✝¹ : Finite ι
μ : ι → Measure α
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
val✝ : Fintype ι
this : ∀ (n : ℕ), MeasurableSet (⋂ i, spanningSets (μ i) n)
n : ℕ
⊢ ∑ b, (μ b) (⋂ i, spanningSets (μ i) n) < ∞
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: case refine_2.mpr
ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
a✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := ⋯
hsμ : ∀ (i : ι), (μ i) (s i) = 0
hsm : MeasurableSet (⋂ i, s i)
hs : ∀ (i : ι), ∀ x ∉ s i, f x = mk f ⋯ x
g : α → β := ⋯
t : Set β
ht : MeasurableSet t
x : α
hx : ∃ i, x ∉ s i
⊢ f x ∈ t → ∃ i, mk f ⋯ x ∈ t ∧ x ∉ s i

Tactic:
rcases hx with ⟨i, hi⟩
      rw [hs _ _ hi]
      exact fun h => ⟨i, h, hi⟩

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

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
s : Set α := toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := s.piecewise (fun x ↦ h₀.some) (mk f H)
⊢ μ (toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ) = 0

Tactic:
measure_toMeasurable,

Goal state after:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
s : Set α := toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := s.piecewise (fun x ↦ h₀.some) (mk f H)
⊢ μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ = 0
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
ι : Type u_6
x✝ : MeasurableSpace α
μ : Measure α
s : ι → Set α
M : ℕ
hs_meas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (y : α), {i | y ∈ s i}.encard ≤ ↑M
t : Set α
ht : MeasurableSet t
F : Finset ι
P : Finset ι → Set α := fun C ↦ (⋂ i ∈ C, s i) ∩ ⋂ i ∈ F \ C, (s i)ᶜ
Cs : Finset (Finset ι) := F.powerset \ {∅}
G : ι → Set (Finset ι) := fun i ↦ {C | C ∈ F.powerset ∧ i ∈ C}
P_meas : ∀ (C : Finset ι), MeasurableSet (P C)
P_cover : ∀ {i : ι}, i ∈ F → s i ⊆ ⋃ C ∈ G i, P C
iUnion_P : ⋃ C ∈ Cs, P C ⊆ ⋃ i, s i
P_subset_s : ∀ {i : ι} {C : Finset ι}, i ∈ C → P C ⊆ s i
mem_C : ∀ {i : ι}, i ∈ F → ∀ {C : Finset ι} {x : α}, x ∈ P C → x ∈ s i → i ∈ C
C_subset_C : ∀ {C₁ C₂ : Finset ι}, C₁ ∈ Cs → ∀ {x : α}, x ∈ P C₁ ∩ P C₂ → C₁ ⊆ C₂
⊢ ∑' (C : Finset ι), ∑ i ∈ F, (G i).indicator (fun C ↦ (μ.restrict (P C)) t) C =
    ∑ C ∈ Cs, ∑ i ∈ F, (↑C).indicator (fun x ↦ (μ.restrict (P C)) t) i

Tactic:
rw [sum_eq_tsum_indicator]
      congr with C
      by_cases hC : C ∈ F.powerset <;> by_cases hC' : C = ∅ <;>
        simp [hC, hC', Cs, G, indicator, -Finset.mem_powerset, -coe_powerset]

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
s t : Set X
inst✝ : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed[inst✝¹] t
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen[inst✝¹] t
T_count : T.Countable
T_int : t = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → ↑T
g_surj : Surjective g
n : ℕ
⊢ t ⊆ ↑(g n)

Tactic:
T_int

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
s t : Set X
inst✝ : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed[inst✝¹] t
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen[inst✝¹] t
T_count : T.Countable
T_int : t = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → ↑T
g_surj : Surjective g
n : ℕ
⊢ ⋂₀ T ⊆ ↑(g n)
Module: Mathlib.Topology.Separation.GDelta

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
s t : Set X
inst✝ : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed[inst✝¹] t
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen[inst✝¹] t
T_count : T.Countable
T_int : t = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → ↑T
g_surj : Surjective g
g' : ℕ → Set X
g'_open : ∀ (n : ℕ), IsOpen[inst✝¹] (g' n)
clt_sub_g' : ∀ (n : ℕ), t ⊆ g' n
clg'_sub_g : ∀ (n : ℕ), closure[inst✝¹] (g' n) ⊆ ↑(g n)
⊢ ⋂ i, closure[inst✝¹] (g' i) ⊆ t

Tactic:
T_int

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
s t : Set X
inst✝ : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed[inst✝¹] t
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen[inst✝¹] t
T_count : T.Countable
T_int : t = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → ↑T
g_surj : Surjective g
g' : ℕ → Set X
g'_open : ∀ (n : ℕ), IsOpen[inst✝¹] (g' n)
clt_sub_g' : ∀ (n : ℕ), t ⊆ g' n
clg'_sub_g : ∀ (n : ℕ), closure[inst✝¹] (g' n) ⊆ ↑(g n)
⊢ ⋂ i, closure[inst✝¹] (g' i) ⊆ ⋂₀ T
Module: Mathlib.Topology.Separation.GDelta

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
s t : Set X
inst✝ : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed[inst✝¹] t
t_gd : IsGδ t
⊢ HasSeparatingCover s t

Tactic:
obtain ⟨T, T_open, T_count, T_int⟩ := t_gd
  rcases T.eq_empty_or_nonempty with rfl | T_nonempty
  · rw [T_int, sInter_empty] at st_dis
    rw [(s.disjoint_univ).mp st_dis]
    exact t.hasSeparatingCover_empty_left
  obtain ⟨g, g_surj⟩ := T_count.exists_surjective T_nonempty
  choose g' g'_open clt_sub_g' clg'_sub_g using fun n ↦ by
    apply normal_exists_closure_subset t_cl (T_open (g n).1 (g n).2)
    rw [T_int]
    exact sInter_subset_of_mem (g n).2
  have clg'_int : t = ⋂ i, closure (g' i) := by
    apply (subset_iInter fun n ↦ (clt_sub_g' n).trans subset_closure).antisymm
    rw [T_int]
    refine subset_sInter fun t tinT ↦ ?_
    obtain ⟨n, gn⟩ := g_surj ⟨t, tinT⟩
    refine iInter_subset_of_subset n <| (clg'_sub_g n).trans ?_
    rw [gn]
  use fun n ↦ (closure (g' n))ᶜ
  constructor
  · rw [← compl_iInter, subset_compl_comm, ← clg'_int]
    exact st_dis.subset_compl_left
  · refine fun n ↦ ⟨isOpen_compl_iff.mpr isClosed_closure, ?_⟩
    simp only [closure_compl, disjoint_compl_left_iff_subset]
    rw [← closure_eq_iff_isClosed.mpr t_cl] at clt_sub_g'
    exact subset_closure.trans <| (clt_sub_g' n).trans <| (g'_open n).subset_interior_closure

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

Goal state before:
pp: α : Type u_1
s : Set (Set α)
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
hs : t = TopologicalSpace.generateFrom s
u : Set α
hu : u ∈ s
⊢ TopologicalSpace.IsOpen u

Tactic:
rw [hs]; exact GenerateOpen.basic _ hu

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

Goal state before:
pp: case h₁
α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s✝ t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : OpensMeasurableSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : OpensMeasurableSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : TopologicalSpace γ₂
inst✝² : MeasurableSpace γ₂
inst✝¹ : BorelSpace γ₂
inst✝ : MeasurableSpace δ
h : SecondCountableTopologyEither α β
s : Set (α × β)
hs : IsOpen[instTopologicalSpaceProd] s
hβ : SecondCountableTopology β
F : Set β → Set α := ⋯
A : ∀ (a : Set β), IsOpen[inst✝¹²] (F a)
⊢ s ⊆ ⋃ a ∈ countableBasis β, F a ×ˢ a

Tactic:
rintro ⟨y1, y2⟩ hy
        rcases isOpen_prod_iff.1 hs y1 y2 hy with ⟨u, v, u_open, v_open, yu, yv, huv⟩
        obtain ⟨a, ha, ya, au⟩ : ∃ a ∈ countableBasis β, y2 ∈ a ∧ a ⊆ v :=
          IsTopologicalBasis.exists_subset_of_mem_open (isBasis_countableBasis β) yv v_open
        simp only [mem_iUnion, mem_prod, exists_and_left, exists_prop]
        exact ⟨a, ⟨u, u_open, yu, (Set.prod_mono_right au).trans huv⟩, ha, ya⟩

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
h : x ∉ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ ContinuousAt (fun x ↦ (infDist x s)⁻¹) x

Tactic:
by
  rcases s.eq_empty_or_nonempty with (rfl | hs)
  · simp only [infDist_empty, continuousAt_const]
  · refine (continuous_infDist_pt s).continuousAt.inv₀ ?_
    rwa [Ne, ← mem_closure_iff_infDist_zero hs]

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case refine_1
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
h : ∀ (a : α), μ (Iic a) = ν (Iic a)
⊢ μ univ = ν univ

Tactic:
rcases exists_countable_dense_bot_top α with ⟨s, hsc, hsd, -, hst⟩
    have : DirectedOn (· ≤ ·) s := directedOn_iff_directed.2 (Subtype.mono_coe _).directed_le
    simp only [← biSup_measure_Iic hsc (hsd.exists_ge' hst) this, h]

Goal state after:
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
f : α →ₛ β
p : β → Prop
⊢ (∃ y ∈ f.range, p y) ↔ ∃ x, p (f x)

Tactic:
simpa only [mem_range, exists_prop] using Set.exists_range_iff

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
x : α
fin : hausdorffEDist s t ≠ ∞
h : infEDist x s = ∞
⊢ infEDist x t = ∞

Tactic:
rw [infEDist_eq_top_iff, ← not_nonempty_iff_eq_empty] at h ⊢

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
x : α
fin : hausdorffEDist s t ≠ ∞
h : ¬s.Nonempty
⊢ ¬t.Nonempty
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric

Goal state before:
pp: α : Type u_5
m : MeasurableSpace α
inst✝¹ : CountablyGenerated α
inst✝ : MeasurableSpace.SeparatesPoints α
⊢ ∃ x, SecondCountableTopology α ∧ T4Space α ∧ BorelSpace α

Tactic:
rcases measurableEquiv_nat_bool_of_countablyGenerated α with ⟨s, ⟨f⟩⟩

Goal state after:
α : Type u_5
m : MeasurableSpace α
inst✝¹ : CountablyGenerated α
inst✝ : MeasurableSpace.SeparatesPoints α
s : Set (ℕ → Bool)
f : α ≃ᵐ ↑s
⊢ ∃ x, SecondCountableTopology α ∧ T4Space α ∧ BorelSpace α
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
⊢ (map g f).lintegral μ = ∑ x ∈ f.range, g x * μ (⇑f ⁻¹' {x})

Tactic:
simp only [lintegral, range_map]
  refine Finset.sum_image' _ fun b hb => ?_
  rcases mem_range.1 hb with ⟨a, rfl⟩
  rw [map_preimage_singleton, ← f.sum_measure_preimage_singleton, Finset.mul_sum]
  refine Finset.sum_congr ?_ ?_
  · congr
  · grind

Goal state after:
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
⊢ (map g f).lintegral μ = ∑ x ∈ f.range, g x * μ (⇑f ⁻¹' {x})

Tactic:
by
  simp only [lintegral, range_map]
  refine Finset.sum_image' _ fun b hb => ?_
  rcases mem_range.1 hb with ⟨a, rfl⟩
  rw [map_preimage_singleton, ← f.sum_measure_preimage_singleton, Finset.mul_sum]
  refine Finset.sum_congr ?_ ?_
  · congr
  · grind

Goal state after:
Module: Mathlib.Topology.IndicatorConstPointwise

Goal state before:
pp: α : Type u_1
A : Set α
β : Type u_2
inst✝³ : Zero β
inst✝² : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
inst✝¹ : T1Space β
b : β
inst✝ : NeZero b
x : α
⊢ Tendsto (fun i ↦ (As i).indicator (fun x ↦ b) x) L (𝓝 (A.indicator (fun x ↦ b) x)) ↔ ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A

Tactic:
apply tendsto_indicator_const_apply_iff_eventually' _ b

Goal state after:
case nhds_b
α : Type u_1
A : Set α
β : Type u_2
inst✝³ : Zero β
inst✝² : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
inst✝¹ : T1Space β
b : β
inst✝ : NeZero b
x : α
⊢ {0}ᶜ ∈ 𝓝 b

case nhds_o
α : Type u_1
A : Set α
β : Type u_2
inst✝³ : Zero β
inst✝² : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
inst✝¹ : T1Space β
b : β
inst✝ : NeZero b
x : α
⊢ {b}ᶜ ∈ 𝓝 0
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α
mα : MeasurableSpace α
x✝ : ℝ≥0∞
⊢ Measurable fun x ↦ ↑x • x✝

Tactic:
exact measurable_coe_nnreal_ennreal.mul_const _

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: case refine_1
β : Type u_6
mβ : MeasurableSpace β
f : EReal × EReal → β
h_real : Measurable fun p ↦ f (↑p.1, ↑p.2)
h_bot_left : Measurable fun r ↦ f (⊥, ↑r)
h_top_left : Measurable fun r ↦ f (⊤, ↑r)
h_bot_right : Measurable fun r ↦ f (↑r, ⊥)
h_top_right : Measurable fun r ↦ f (↑r, ⊤)
⊢ Measurable fun p ↦ f (↑p.1, p.2)

Tactic:
refine measurable_swap_iff.mp <| measurable_of_real_prod ?_ h_bot_right h_top_right
    exact h_real.comp measurable_swap

Goal state after:
Module: Mathlib.MeasureTheory.Function.SimpleFuncDense

Goal state before:
pp: case pos
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : ∀ {k : ℕ}, k ≤ N → edist ((nearestPt e N) x) x ≤ edist (e k) x
k : ℕ
hk : k ≤ N + 1
h : ∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x
⊢ edist (e (N + 1)) x ≤ edist (e k) x

Tactic:
rcases hk.eq_or_lt with (rfl | hk)
      exacts [le_rfl, (h k (Nat.lt_succ_iff.1 hk)).le]

Goal state after: