mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
r C : ℝ
f : ℕ → α
hr : r < 1
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
⊢ dist (f n) a ≤ C * r ^ n / (1 - r)

Tactic:
have := aux_hasSum_of_le_geometric hr hu

Goal state after:
α : Type u_1
inst✝ : PseudoMetricSpace α
r C : ℝ
f : ℕ → α
hr : r < 1
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
this : HasSum (fun n ↦ C * r ^ n) (C / (1 - r))
⊢ dist (f n) a ≤ C * r ^ n / (1 - r)
Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory

Goal state before:
pp: α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
n : ℕ
⊢ ∑ a ∈ Finset.range n, m (s a) ≤ m (⋃ i, s i)

Tactic:
have := @isCaratheodory_sum _ m _ h hd univ n

Goal state after:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
n : ℕ
this : ∑ i ∈ Finset.range n, m (univ ∩ s i) = m (univ ∩ ⋃ i, ⋃ (_ : i < n), s i)
⊢ ∑ a ∈ Finset.range n, m (s a) ≤ m (⋃ i, s i)
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: case a
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
⊢ (inducedOuterMeasure m P0 m0) s ≤ ⨅ t, ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht

Tactic:
simp only [le_iInf_iff]
    intro t ht hs
    grw [hs]
    exact le_of_eq (inducedOuterMeasure_eq' _ msU m_mono _)

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
⊢ IsPiSystem (piiUnionInter π S)

Tactic:
by
  classical
  rintro t1 ⟨p1, hp1S, f1, hf1m, ht1_eq⟩ t2 ⟨p2, hp2S, f2, hf2m, ht2_eq⟩ h_nonempty
  simp_rw [piiUnionInter, Set.mem_ofPred_eq]
  let g n := ite (n ∈ p1) (f1 n) Set.univ ∩ ite (n ∈ p2) (f2 n) Set.univ
  have hp_union_ss : ↑(p1 ∪ p2) ⊆ S := by
    simp only [hp1S, hp2S, Finset.coe_union, union_subset_iff, and_self_iff]
  use p1 ∪ p2, hp_union_ss, g
  have h_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i := by
    rw [ht1_eq, ht2_eq]
    simp_rw [← Set.inf_eq_inter]
    ext1 x
    simp only [inf_eq_inter, mem_inter_iff, mem_iInter]
    grind
  refine ⟨fun n hn => ?_, h_inter_eq⟩
  simp only [g]
  split_ifs with hn1 hn2 h
  · refine hpi n (f1 n) (hf1m n hn1) (f2 n) (hf2m n hn2) (Set.nonempty_iff_ne_empty.2 fun h => ?_)
    rw [h_inter_eq] at h_nonempty
    suffices h_empty : ⋂ i ∈ p1 ∪ p2, g i = ∅ from
      (Set.not_nonempty_iff_eq_empty.mpr h_empty) h_nonempty
    refine le_antisymm (Set.iInter_subset_of_subset n ?_) (Set.empty_subset _)
    refine Set.iInter_subset_of_subset hn ?_
    grind
  · simp [hf1m n hn1]
  · simp [hf2m n h]
  · exact absurd hn (by simp [hn1, h])

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

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α✝
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace β✝
inst✝³ : MeasurableSpace γ✝
α : Type ?u.23
β : Type ?u.25
γ : Type ?u.27
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
⊢ Measurable ⇑(Equiv.sumProdDistrib α β γ)

Tactic:
refine
      measurable_of_measurable_union_cover (range Sum.inl ×ˢ (univ : Set γ))
        (range Sum.inr ×ˢ (univ : Set γ)) (measurableSet_range_inl.prod MeasurableSet.univ)
        (measurableSet_range_inr.prod MeasurableSet.univ)
        (by rintro ⟨a | b, c⟩ <;> simp [Set.prod_eq]) ?_ ?_
    · refine (Set.prod (range Sum.inl) univ).symm.measurable_comp_iff.1 ?_
      refine (prodCongr Set.rangeInl (Set.univ _)).symm.measurable_comp_iff.1 ?_
      exact measurable_inl
    · refine (Set.prod (range Sum.inr) univ).symm.measurable_comp_iff.1 ?_
      refine (prodCongr Set.rangeInr (Set.univ _)).symm.measurable_comp_iff.1 ?_
      exact measurable_inr

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
hs : s.Countable
h : ∀ t ∈ s, NullMeasurableSet t μ
⊢ NullMeasurableSet (⋃₀ s) μ

Tactic:
rw [sUnion_eq_biUnion]
  exact MeasurableSet.biUnion hs h

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Finset α
inst✝ : MeasurableSingletonClass α
⊢ ∑ x ∈ s, μ {x} = μ ↑s

Tactic:
trans ∑ x ∈ s, μ (id ⁻¹' {x})

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Finset α
inst✝ : MeasurableSingletonClass α
⊢ ∑ x ∈ s, μ {x} = ∑ x ∈ s, μ (id ⁻¹' {x})

α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Finset α
inst✝ : MeasurableSingletonClass α
⊢ ∑ x ∈ s, μ (id ⁻¹' {x}) = μ ↑s
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
e : ι → ℕ
he : Injective e
t : ℕ → Set α
ht : Function.extend e s ⊥ = t
⊢ μ (⋃ i, s i) = ⨆ i, μ (s i)

Tactic:
replace hd : Directed (· ⊆ ·) t := ht ▸ hd.extend_bot he

Goal state after:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
e : ι → ℕ
he : Injective e
t : ℕ → Set α
ht : Function.extend e s ⊥ = t
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) t
⊢ μ (⋃ i, s i) = ⨆ i, μ (s i)
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
h : MeasurableSet s
⊢ ({ toFun := fun μ ↦ ((OuterMeasure.restrict s) μ.toOuterMeasure).toMeasure ⋯, map_add' := ⋯ } μ).toOuterMeasure =
    (OuterMeasure.restrict s) μ.toOuterMeasure

Tactic:
AddHom.coe_mk,

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
h : MeasurableSet s
⊢ (((OuterMeasure.restrict s) μ.toOuterMeasure).toMeasure ⋯).toOuterMeasure = (OuterMeasure.restrict s) μ.toOuterMeasure
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
x : α
n : ℕ
⊢ spanningSetsIndex μ x = n ↔ x ∈ disjointed (spanningSets μ) n

Tactic:
convert! Set.ext_iff.1 (preimage_spanningSetsIndex_singleton μ n) x

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

Goal state before:
pp: case compl
α : Type u_5
m₀ : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hμν : ∀ s ∈ C, μ s = ν s
m : MeasurableSpace α
h : m ≤ m₀
hA : m = generateFrom C
hC : IsPiSystem C
h_univ : μ univ = ν univ
s : Set α
this : IsFiniteMeasure ν
t : Set α
htm : MeasurableSet t
iht : μ t = ν t
⊢ μ univ - ν t = ν univ - ν t

Tactic:
h_univ

Goal state after:
case compl
α : Type u_5
m₀ : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hμν : ∀ s ∈ C, μ s = ν s
m : MeasurableSpace α
h : m ≤ m₀
hA : m = generateFrom C
hC : IsPiSystem C
h_univ : μ univ = ν univ
s : Set α
this : IsFiniteMeasure ν
t : Set α
htm : MeasurableSet t
iht : μ t = ν t
⊢ ν univ - ν t = ν univ - ν t
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: case h₂
α : 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)
D : Set (Set α)
D_mem : D ∈ {D | D ⊆ C ∧ D.Countable}
hD : μ (⋃₀ D) = m
s : Set α
hs : s ∈ C
⊢ μ (s ∪ ⋃₀ D) ≤ m

Tactic:
show s ∪ ⋃₀ D = ⋃₀ (D ∪ {s}) by simp

Goal state after:
case h₂
α : 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)
D : Set (Set α)
D_mem : D ∈ {D | D ⊆ C ∧ D.Countable}
hD : μ (⋃₀ D) = m
s : Set α
hs : s ∈ C
⊢ μ (⋃₀ (D ∪ {s})) ≤ m
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_8
ι : Type u_9
x✝ : MeasurableSpace α
μ : Measure α
inst✝¹ : SemilatticeSup ι
inst✝ : Countable ι
f : ι → Set α
hm : ∀ (i : ι), NullMeasurableSet (f i) μ
ε : ℝ≥0∞
hε : 0 < ε
hfin : ∃ i, μ (f i) ≠ ∞
hfem : ⋂ n, f n = ∅
⊢ ∃ m, μ (⋂ n, ⋂ (_ : n ≤ m), f n) < ε

Tactic:
let F m := μ (⋂ n ≤ m, f n)
  have hFAnti : Antitone F :=
      fun i j hij => measure_mono (biInter_subset_biInter_left fun k hki => le_trans hki hij)
  suffices Filter.Tendsto F Filter.atTop (𝓝 0) by
    let _ := hfin.nonempty
    rw [ENNReal.tendsto_atTop_zero_iff_lt_of_antitone hFAnti] at this
    exact this ε hε
  have hzero : μ (⋂ n, f n) = 0 := by
    simp only [hfem, measure_empty]
  rw [← hzero]
  exact tendsto_measure_iInter_le hm hfin

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

Goal state before:
pp: case hsm
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
m : ℝ≥0∞ := ⋯
D : Set (Set α)
D_mem : D ∈ {D | D ⊆ C ∧ D.Countable}
hD : μ (⋃₀ D) = m
s : Set α
hs : s ∈ C
⊢ NullMeasurableSet (⋃₀ D) μ

Tactic:
exact (MeasurableSet.sUnion D_mem.2 (by grind)).nullMeasurableSet

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
⊢ ∃ D ⊆ C, D.Countable ∧ ∀ s ∈ C, s ≤ᵐ[μ] ⋃₀ D

Tactic:
let m := ⨆ D ∈ {D : Set (Set α) | D ⊆ C ∧ D.Countable}, μ (⋃₀ D)
  obtain ⟨D, D_mem, hD⟩ : ∃ D ∈ {D : Set (Set α) | D ⊆ C ∧ D.Countable}, μ (⋃₀ D) = m := by
    rcases eq_bot_or_bot_lt m with hm | hm
    · exact ⟨∅, by simp, by simp [hm]⟩
    obtain ⟨u, -, u_mem, u_lim⟩ :
        ∃ u : ℕ → ℝ≥0∞, StrictMono u ∧ (∀ n, u n ∈ Ioo 0 m) ∧ Tendsto u atTop (𝓝 m) :=
      exists_seq_strictMono_tendsto' hm
    have A n : ∃ D ∈ {D : Set (Set α) | D ⊆ C ∧ D.Countable}, u n < μ (⋃₀ D) :=
      lt_biSup_iff.1 (u_mem n).2
    choose! D D_mem huD using A
    have hD : ⋃ n, D n ∈ {D | D ⊆ C ∧ D.Countable} := by simp; grind
    refine ⟨⋃ n, D n, hD, ?_⟩
    apply le_antisymm (le_biSup (f := fun D ↦ μ (⋃₀ D)) hD)
    apply le_of_tendsto' u_lim (fun n ↦ (huD n).le.trans ?_)
    exact measure_mono (fun x hx ↦ by simp at hx ⊢; grind)
  refine ⟨D, by grind, by grind, fun s hs ↦ union_ae_eq_right_iff_ae_subset.mp ?_⟩
  symm
  apply ae_eq_of_ae_subset_of_measure_ge subset_union_right.eventuallyLE
  · rw [hD, show s ∪ ⋃₀ D = ⋃₀ (D ∪ {s}) by simp]
    apply le_biSup (f := fun D ↦ μ (⋃₀ D))
    simp [D_mem.2, insert_subset_iff, hs, D_mem.1]
  · exact (MeasurableSet.sUnion D_mem.2 (by grind)).nullMeasurableSet
  · simp

Goal state after:
Module: Mathlib.Order.Filter.CountableSeparatingOn

Goal state before:
pp: case refine_1
α : Type u_1
l : Filter α
inst✝ : CountableInterFilter l
p : Set α → Prop
s : Set α
h : HasCountableSeparatingOn α p s
hs : s ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
S : Set (Set α)
hSc : S.Countable
hSp : ∀ s ∈ S, p s
hS : ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
⊢ s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ U ∈ S, ⋂ (_ : Uᶜ ∈ l), Uᶜ ⊆ s

Tactic:
exact fun _ h ↦ h.1.1

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
inst✝ : SigmaFinite μ
⊢ μ + ν₁ = μ + ν₂ ↔ ν₁ = ν₂

Tactic:
μ.add_right_inj

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
inst✝ : SigmaFinite μ
⊢ ν₁ = ν₂ ↔ ν₁ = ν₂
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : MeasurableSpace α
μ : Measure α
s t : Set α
f g : α → β
inst✝¹ : DecidablePred fun x ↦ x ∈ s
inst✝ : DecidablePred fun x ↦ x ∈ t
hst : s =ᵐ[μ] t
x : α
hx : x ∈ s ↔ x ∈ t
⊢ s.piecewise f g x = t.piecewise f g x

Tactic:
simp [piecewise, hx]

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

Goal state before:
pp: case pos
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
t : Set β
ht : 0 ∈ t
⊢ t ∈ Filter.map (s.indicator f) (ae μ) → t ∈ Filter.map f (ae (μ.restrict s))

pp: case neg
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
t : Set β
ht : 0 ∉ t
⊢ t ∈ Filter.map (s.indicator f) (ae μ) → t ∈ Filter.map f (ae (μ.restrict s))

Tactic:
· rw [mem_map_indicator_ae_iff_mem_map_restrict_ae_of_zero_mem ht hs]
    exact id

Goal state after:
case neg
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
t : Set β
ht : 0 ∉ t
⊢ t ∈ Filter.map (s.indicator f) (ae μ) → t ∈ Filter.map f (ae (μ.restrict s))
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: case refine_2
ι : 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 α := fun i ↦ toMeasurable (μ i) {x | f x ≠ mk f ⋯ x}
hsμ : ∀ (i : ι), (μ i) (s i) = 0
hsm : MeasurableSet (⋂ i, s i)
hs : ∀ (i : ι), ∀ x ∉ s i, f x = mk f ⋯ x
g : α → β := (⋂ i, s i).piecewise (const α default) f
t : Set β
ht : MeasurableSet t
⊢ MeasurableSet ((⋃ i, (s i)ᶜ).domRestrict f ⁻¹' t)

Tactic:
refine ⟨⋃ i, (h i).mk f ⁻¹' t ∩ (s i)ᶜ, MeasurableSet.iUnion fun i ↦
      (measurable_mk _ ht).inter (measurableSet_toMeasurable _ _).compl, ?_⟩

Goal state after:
case refine_2
ι : 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 α := fun i ↦ toMeasurable (μ i) {x | f x ≠ mk f ⋯ x}
hsμ : ∀ (i : ι), (μ i) (s i) = 0
hsm : MeasurableSet (⋂ i, s i)
hs : ∀ (i : ι), ∀ x ∉ s i, f x = mk f ⋯ x
g : α → β := (⋂ i, s i).piecewise (const α default) f
t : Set β
ht : MeasurableSet t
⊢ Subtype.val ⁻¹' ⋃ i, mk f ⋯ ⁻¹' t ∩ (s i)ᶜ = (⋃ i, (s i)ᶜ).domRestrict f ⁻¹' t
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
s t : Set α
⊢ AEMeasurable f (μ.restrict (s ∪ t)) ↔ AEMeasurable f (μ.restrict s) ∧ AEMeasurable f (μ.restrict t)

Tactic:
simp only [union_eq_iUnion, aemeasurable_iUnion_iff, Bool.forall_bool, cond, and_comm]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NeZero μ
h : IsEmpty α
⊢ False

Tactic:
by
    simpa [eq_empty_of_isEmpty] using NeZero.ne (μ univ)

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

Goal state before:
pp: α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
inst✝ : Countable ι
f : ι → Measure α
s : Set α
⊢ (sum f) s = ∑' (i : ι), (f i) s

Tactic:
apply le_antisymm ?_ (le_sum_apply _ _)
  rcases exists_measurable_superset_forall_eq f s with ⟨t, hst, htm, ht⟩
  calc
  sum f s ≤ sum f t := measure_mono hst
  _ = ∑' i, f i t := sum_apply _ htm
  _ = ∑' i, f i s := by simp [ht]

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PseudoMetrizableSpace X
s : Set X
hs : IsClosed s
this✝ : UniformSpace X := pseudoMetrizableSpaceUniformity X
this : (uniformity X).IsCountablyGenerated
U : ℕ → SetRel X X
hUo : ∀ (i : ℕ), U i ∈ uniformity X ∧ IsOpen (U i)
hU : (uniformity X).HasBasis (fun x ↦ True) fun i ↦ id (U i)
⊢ IsGδ (⋂ i, ⋂ (_ : True), ⋃ x ∈ s, UniformSpace.ball x (id (U i)))

Tactic:
refine .biInter (to_countable _) fun n _ => IsOpen.isGδ ?_

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PseudoMetrizableSpace X
s : Set X
hs : IsClosed s
this✝ : UniformSpace X := pseudoMetrizableSpaceUniformity X
this : (uniformity X).IsCountablyGenerated
U : ℕ → SetRel X X
hUo : ∀ (i : ℕ), U i ∈ uniformity X ∧ IsOpen (U i)
hU : (uniformity X).HasBasis (fun x ↦ True) fun i ↦ id (U i)
n : ℕ
x✝ : n ∈ fun i ↦ True
⊢ IsOpen (⋃ x ∈ s, UniformSpace.ball x (id (U 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)
t : Set X
tinT : t ∈ T
⊢ ⋂ i, closure[inst✝¹] (g' i) ⊆ t

Tactic:
obtain ⟨n, gn⟩ := g_surj ⟨t, tinT⟩

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)
t : Set X
tinT : t ∈ T
n : ℕ
gn : g n = ⟨t, tinT⟩
⊢ ⋂ i, closure[inst✝¹] (g' i) ⊆ t
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: case inl
α : 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 β := fun a ↦ {y | ∃ b, IsOpen[inst✝⁹] b ∧ y ∈ b ∧ a ×ˢ b ⊆ s}
⊢ MeasurableSet s

Tactic:
have A : ∀ a, IsOpen (F a) := by
      intro a
      apply isOpen_iff_forall_mem_open.2
      rintro y ⟨b, b_open, yb, hb⟩
      exact ⟨b, fun z zb ↦ ⟨b, b_open, zb, hb⟩, b_open, yb⟩

Goal state after:
case inl
α : 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 β := fun a ↦ {y | ∃ b, IsOpen[inst✝⁹] b ∧ y ∈ b ∧ a ×ˢ b ⊆ s}
A : ∀ (a : Set α), IsOpen[inst✝⁹] (F a)
⊢ MeasurableSet s
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:

Tactic:
infEDist x s ≤ edist x y := infEDist_le_edist_of_mem h'y
    _ ≤ r := by rwa [Metric.mem_closedEBall, edist_comm] at hy
    _ < infEDist x s := h

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

Goal state before:
pp: case inr
α : 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 α := fun a ↦ {y | ∃ b, IsOpen[inst✝¹²] b ∧ y ∈ b ∧ b ×ˢ a ⊆ s}
⊢ MeasurableSet s

Tactic:
have A : ∀ a, IsOpen (F a) := by
      intro a
      apply isOpen_iff_forall_mem_open.2
      rintro y ⟨b, b_open, yb, hb⟩
      exact ⟨b, fun z zb ↦ ⟨b, b_open, zb, hb⟩, b_open, yb⟩

Goal state after:
case inr
α : 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 α := fun a ↦ {y | ∃ b, IsOpen[inst✝¹²] b ∧ y ∈ b ∧ b ×ˢ a ⊆ s}
A : ∀ (a : Set β), IsOpen[inst✝¹²] (F a)
⊢ MeasurableSet s
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: case refine_2
α : Type u
inst✝ : PseudoEMetricSpace α
U : Set α
hU : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n ↦ (fun x ↦ infEDist x Uᶜ) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
⊢ Monotone F

Tactic:
intro m n hmn x hx

Goal state after:
case refine_2
α : Type u
inst✝ : PseudoEMetricSpace α
U : Set α
hU : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n ↦ (fun x ↦ infEDist x Uᶜ) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
m n : ℕ
hmn : m ≤ n
x : α
hx : x ∈ F m
⊢ x ∈ F n
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: α : Type u_1
γ : Type u_3
inst✝⁶ : TopologicalSpace α
inst✝⁵ : MeasurableSpace α
inst✝⁴ : OpensMeasurableSpace α
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
inst✝ : MeasurableSingletonClass α
f : α → γ
s : Set α
hf : ContinuousOn f s
hs : sᶜ.Countable
⊢ Measurable f

Tactic:
apply measurable_of_measurable_on_compl_countable _ hs
  rw [compl_compl]
  exact (continuousOn_iff_continuous_domRestrict.1 hf).measurable

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
x : α
hx : infEDist x E < ENNReal.ofReal δ
⊢ x ∈ cthickening δ E

Tactic:
exact hx.le

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_nn : 0 ≤ δ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
⊢ cthickening δ E = ⋂ ε ∈ s, thickening ε E

Tactic:
refine (subset_iInter₂ fun ε hε => ?_).antisymm ?_

Goal state after:
case refine_1
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_nn : 0 ≤ δ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
ε : ℝ
hε : ε ∈ s
⊢ cthickening δ E ⊆ thickening ε E

case refine_2
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_nn : 0 ≤ δ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
⊢ ⋂ i ∈ s, thickening i E ⊆ cthickening δ E
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: δ : ℝ
α : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
E : Set α
hδ : 0 ≤ δ
⊢ cthickening δ E = ⋃ x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] E, closedBall x δ

Tactic:
by
  rcases eq_empty_or_nonempty E with (rfl | hne)
  · simp only [cthickening_empty, biUnion_empty, closure_empty]
  rw [← cthickening_closure]
  refine Subset.antisymm (fun x hx ↦ ?_)
    (iUnion₂_subset fun x hx ↦ closedBall_subset_cthickening hx _)
  obtain ⟨y, yE, hy⟩ : ∃ y ∈ closure E, infDist x (closure E) = dist x y :=
    isClosed_closure.exists_infDist_eq_dist (closure_nonempty_iff.mpr hne) x
  replace hy : dist x y ≤ δ :=
    (ENNReal.ofReal_le_ofReal_iff hδ).mp
      (((congr_arg ENNReal.ofReal hy.symm).le.trans ENNReal.ofReal_toReal_le).trans hx)
  exact mem_biUnion yE hy

Goal state after: