mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
inst✝⁶ : TopologicalSpace α
x : α
ι : Type u_4
γ : Type u_5
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : LinearOrder γ
inst✝³ : IsOrderedAddMonoid γ
inst✝² : TopologicalSpace γ
inst✝¹ : OrderTopology γ
inst✝ : ContinuousAdd γ
f : ι → α → γ
a : Finset ι
ha : ∀ i ∈ a, UpperSemicontinuousAt (f i) x
⊢ UpperSemicontinuousAt (fun z ↦ ∑ i ∈ a, f i z) x

Tactic:
simp_rw [← upperSemicontinuousWithinAt_univ_iff] at *

Goal state after:
α : Type u_1
inst✝⁶ : TopologicalSpace α
x : α
ι : Type u_4
γ : Type u_5
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : LinearOrder γ
inst✝³ : IsOrderedAddMonoid γ
inst✝² : TopologicalSpace γ
inst✝¹ : OrderTopology γ
inst✝ : ContinuousAdd γ
f : ι → α → γ
a : Finset ι
ha : ∀ i ∈ a, UpperSemicontinuousWithinAt (f i) univ x
⊢ UpperSemicontinuousWithinAt (fun z ↦ ∑ i ∈ a, f i z) univ x
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 α
f : ℕ → Set α
hf : s ⊆ ⋃ i, f i
⊢ ∀ (i : P (⋃ i, f i)), ⨅ t, ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht ≤ m (⋃ i, f i) i

Tactic:
intro h2f

Goal state after:
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 α
f : ℕ → Set α
hf : s ⊆ ⋃ i, f i
h2f : P (⋃ i, f i)
⊢ ⨅ t, ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht ≤ m (⋃ i, f i) h2f
Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s t : Set α
⊢ ¬μ (s ∪ t) = ∞ ↔ ¬(μ s = ∞ ∨ μ t = ∞)

Tactic:
by simp only [← lt_top_iff_ne_top, ← Ne.eq_def, not_or, measure_union_lt_top_iff]

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

Goal state before:
pp: case mp
α : Type u_1
m : MeasurableSpace α
μ : Measure α
δ : Type u_6
X : δ → Type u_7
mX : (a : δ) → MeasurableSpace (X a)
inst✝ : Countable δ
g : α → (a : δ) → X a
⊢ AEMeasurable g μ → ∀ (a : δ), AEMeasurable (fun x ↦ g x a) μ

Tactic:
exact AEMeasurable.eval

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

Goal state before:
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
      · grind
      · suffices x ⊆ ∅ by grind
        intro p hp
        fin_cases p <;> contradiction

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
hs✝ : ¬ms = ∞
r : ℝ≥0∞
hs : r > ms
⊢ ∃ t, MeasurableSet t ∧ s ⊆ t ∧ m t < r

Tactic:
simpa [ms, iInf_lt_iff] using hs

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → α
hf : 0 = μ
s : Set α
hs : NullMeasurableSet s μ
hfm : ¬AEMeasurable f μ
⊢ μ (f ⁻¹' s) = μ s

Tactic:
simp [← hf]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hs : NullMeasurableSet s (comap f μ)
⊢ (comap f μ) s ≤ μ (f '' s)

Tactic:
by_cases hf : Injective f ∧ ∀ t, MeasurableSet t → NullMeasurableSet (f '' t) μ
  · rw [comap_apply₀ _ _ hf.1 hf.2 hs]
  · simp [comap_undef hf]

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

Goal state before:
pp: G : Type u_5
α : Type u_6
inst✝¹ : Group G
inst✝ : MulAction G α
x✝ : MeasurableSpace α
μ : Measure α
s : Set α
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun x ↦ g • x) μ μ
⊢ Pairwise (AEDisjoint μ on fun g ↦ g • s)

Tactic:
by
  intro g₁ g₂ hg
  let g := g₂⁻¹ * g₁
  replace hg : g ≠ 1 := by
    rw [Ne, inv_mul_eq_one]
    exact hg.symm
  have : (g₂⁻¹ • ·) ⁻¹' (g • s ∩ s) = g₁ • s ∩ g₂ • s := by
    rw [preimage_eq_iff_eq_image (MulAction.bijective g₂⁻¹), image_smul, smul_set_inter, smul_smul,
      smul_smul, inv_mul_cancel, one_smul]
  change μ (g₁ • s ∩ g₂ • s) = 0
  exact this ▸ (h_qmp g₂⁻¹).preimage_null (h_ae_disjoint g hg)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
s : Set β
hs : s.Countable
f : α → β
hf : ∀ y ∈ s, MeasurableSet (f ⁻¹' {y})
⊢ ∑' (b : ↑s), μ (f ⁻¹' {↑b}) = μ (f ⁻¹' s)

Tactic:
by
  rw [← Set.biUnion_preimage_singleton, measure_biUnion hs (pairwiseDisjoint_fiber f s) hf]

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

Goal state before:
pp: X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
α : Type u_2
l : Filter α
f : X → α
ha : IsSuccPrelimit a
⊢ Tendsto (fun x ↦ f ↑x) atTop l ↔ Tendsto f (𝓝[<] a) l

Tactic:
by
  rw [← map_coe_Iio_atTop a ha, tendsto_map'_iff, Function.comp_def]

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → β
hf : ¬AEMeasurable f μ
⊢ IsFiniteMeasure (map f μ)

Tactic:
· rw [map_of_not_aemeasurable hf]
    exact MeasureTheory.isFiniteMeasureZero

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

Goal state before:
pp: α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Directed (fun x1 x2 ↦ x1 ⊇ x2) s
k : ι
hk : μ (s k) ≠ ∞
this : ∀ t ⊆ s k, μ t ≠ ∞
⊢ μ (s k) - ⨆ i, μ (s k \ s i) = μ (s k) - ⨆ i, μ (s k) - μ (s i)

pp: α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Directed (fun x1 x2 ↦ x1 ⊇ x2) s
k : ι
hk : μ (s k) ≠ ∞
this : ∀ t ⊆ s k, μ t ≠ ∞
⊢ Directed (fun x1 x2 ↦ x1 ⊆ x2) fun i ↦ s k \ s i

Tactic:
· congr 1
    refine le_antisymm (iSup_mono' fun i => ?_) (iSup_mono fun i => le_measure_sdiff)
    rcases hd i k with ⟨j, hji, hjk⟩
    use j
    rw [← measure_sdiff hjk (h _) (this _ hjk)]
    gcongr

Goal state after:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Directed (fun x1 x2 ↦ x1 ⊇ x2) s
k : ι
hk : μ (s k) ≠ ∞
this : ∀ t ⊆ s k, μ t ≠ ∞
⊢ Directed (fun x1 x2 ↦ x1 ⊆ x2) fun i ↦ s k \ s i
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
m : MeasurableSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
h✝ : Nonempty α
inhabited_h : Inhabited α
S : Set (Set α) := {s | IsOpen[inst✝²] s ∧ μ s < ∞}
T : Set (Set α)
T_count : T.Countable
TS : T ⊆ S
hT : ⋃₀ T = ⋃₀ S
⊢ Nonempty (μ.FiniteSpanningSetsIn {K | IsOpen[inst✝²] K})

Tactic:
μ.isTopologicalBasis_isOpen_lt_top.sUnion_eq

Goal state after:
case inr
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
m : MeasurableSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
h✝ : Nonempty α
inhabited_h : Inhabited α
S : Set (Set α) := {s | IsOpen[inst✝²] s ∧ μ s < ∞}
T : Set (Set α)
T_count : T.Countable
TS : T ⊆ S
hT : ⋃₀ T = univ
⊢ Nonempty (μ.FiniteSpanningSetsIn {K | IsOpen[inst✝²] K})
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: case compl
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S T : Set (Set α)
h_gen : m0 = generateFrom S
hc : T.Countable
h_inter : IsPiSystem S
hU : ⋃₀ T = univ
htop : ∀ t ∈ T, μ t ≠ ∞
ST_eq : ∀ t ∈ T, ∀ s ∈ S, μ (s ∩ t) = ν (s ∩ t)
T_eq : ∀ t ∈ T, μ t = ν t
t : Set α
ht : t ∈ T
u✝ u : Set α
hu : MeasurableSet u
ihu : μ (u ∩ t) = ν (u ∩ t)
this : μ t = ν t
⊢ μ (uᶜ ∩ t) = ν (uᶜ ∩ t)

Tactic:
Set.inter_comm

Goal state after:
case compl
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S T : Set (Set α)
h_gen : m0 = generateFrom S
hc : T.Countable
h_inter : IsPiSystem S
hU : ⋃₀ T = univ
htop : ∀ t ∈ T, μ t ≠ ∞
ST_eq : ∀ t ∈ T, ∀ s ∈ S, μ (s ∩ t) = ν (s ∩ t)
T_eq : ∀ t ∈ T, μ t = ν t
t : Set α
ht : t ∈ T
u✝ u : Set α
hu : MeasurableSet u
ihu : μ (t ∩ u) = ν (t ∩ u)
this : μ t = ν t
⊢ μ (t ∩ uᶜ) = ν (t ∩ uᶜ)
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
ms : MeasurableSpace α
μ : OuterMeasure α
h : ms ≤ μ.caratheodory
hμ : μ.toMeasure h = 0
⊢ μ = 0

Tactic:
ext s; exact le_bot_iff.1 <| (le_toMeasure_apply _ _ _).trans_eq congr($hμ s)

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ≪ ν
s : Set α
⊢ μ.restrict s ≪ ν.restrict s

Tactic:
refine Measure.AbsolutelyContinuous.mk (fun t ht htν ↦ ?_)

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ≪ ν
s t : Set α
ht : MeasurableSet t
htν : (ν.restrict s) t = 0
⊢ (μ.restrict s) t = 0
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ n, v n
h'v : ∀ (n : ℕ), μ (t ∩ v n) ≠ ∞
w : ℕ → Set α := fun n ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), μ (w n) < ∞
t' : Set α := ⋃ n, toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ n, toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
⊢ ∑' (n : ℕ), (μ.restrict (t ∩ u)) (disjointed w n) = (μ.restrict (t ∩ u)) (⋃ n, disjointed w n)

Tactic:
rw [measure_iUnion]

Goal state after:
case hn
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ n, v n
h'v : ∀ (n : ℕ), μ (t ∩ v n) ≠ ∞
w : ℕ → Set α := fun n ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), μ (w n) < ∞
t' : Set α := ⋃ n, toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ n, toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
⊢ Pairwise (Disjoint on disjointed w)

case h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ n, v n
h'v : ∀ (n : ℕ), μ (t ∩ v n) ≠ ∞
w : ℕ → Set α := fun n ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), μ (w n) < ∞
t' : Set α := ⋃ n, toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ n, toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
⊢ ∀ (i : ℕ), MeasurableSet (disjointed w i)
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
p : α → Prop
s : Finset ι
μ : ι → Measure α
⊢ (∀ᵐ (x : α) ∂∑ i ∈ s, μ i, p x) ↔ ∀ i ∈ s, ∀ᵐ (x : α) ∂μ i, p x

Tactic:
induction s using Finset.cons_induction <;> simp [*]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
h : CountablySeparated α
s : Set α
⊢ HasCountableSeparatingOn α MeasurableSet s

Tactic:
exact h.countably_separated.mono (fun s ↦ id) <| subset_univ _

Goal state after:
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
x : α
hx : x ∈ ⋃ C, ⋃ (_ : C ∈ F.powerset ∧ C ∉ {∅}), P C
⊢ x ∈ ⋃ i, s i

Tactic:
mem_iUnion

Goal state after:
α : 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
x : α
hx : ∃ i, ∃ (_ : i ∈ F.powerset ∧ i ∉ {∅}), x ∈ P i
⊢ x ∈ ⋃ i, s i
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 α := 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
x : α
i : ι
hi : x ∉ s i
⊢ f x ∈ t → ∃ i, mk f ⋯ x ∈ t ∧ x ∉ s i

Tactic:
hs _ _ hi

Goal state after:
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 α := 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
x : α
i : ι
hi : x ∉ s i
⊢ mk f ⋯ x ∈ t → ∃ i, mk f ⋯ x ∈ t ∧ x ∉ s i
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: γ : Type u_3
δ : Type u_5
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
inst✝ : MeasurableSpace δ
f : δ → γ
hf : ∀ (s : Set γ), IsOpen[inst✝³] s → MeasurableSet (f ⁻¹' s)
⊢ Measurable f

Tactic:
‹BorelSpace γ›.measurable_eq

Goal state after:
γ : Type u_3
δ : Type u_5
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
inst✝ : MeasurableSpace δ
f : δ → γ
hf : ∀ (s : Set γ), IsOpen[inst✝³] s → MeasurableSet (f ⁻¹' s)
⊢ Measurable f
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case mp
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
S : Set (Set α) := ⋯
this : MeasurableSpace α := ⋯
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
ha : ∀ b < a, (Ioo b a).Nonempty
y : α
⊢ y < a → ∃ i, ∃ (_ : i ∈ t), ∃ i_1, ∃ (_ : i_1 ∈ t) (_ : i < i_1) (_ : i_1 < a), i ≤ y ∧ y ≤ i_1

Tactic:
intro hy

Goal state after:
case mp
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
S : Set (Set α) := {S | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
this : MeasurableSpace α := MeasurableSpace.generateFrom S
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
ha : ∀ b < a, (Ioo b a).Nonempty
y : α
hy : y < a
⊢ ∃ i, ∃ (_ : i ∈ t), ∃ i_1, ∃ (_ : i_1 ∈ t) (_ : i < i_1) (_ : i_1 < a), i ≤ y ∧ y ≤ i_1
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 β := fun a ↦ {y | ∃ b, IsOpen[inst✝⁹] b ∧ y ∈ b ∧ a ×ˢ b ⊆ s}
A : ∀ (a : Set α), IsOpen[inst✝⁹] (F a)
y1 : α
y2 : β
hy : ∃ i, y1 ∈ i ∧ i ∈ countableBasis α ∧ y2 ∈ F i
⊢ (y1, y2) ∈ s

Tactic:
rcases hy with ⟨a, ya, -, b, -, yb, hb⟩

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

Goal state before:
pp: α : 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
⊢ ∃ F,
    (∀ (n : ℕ), IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (F n)) ∧
      (∀ (n : ℕ), F n ⊆ U) ∧ ⋃ n, F n = U ∧ Monotone F

Tactic:
refine ⟨F, fun n => IsClosed.preimage continuous_infEDist isClosed_Ici, F_subset, ?_, ?_⟩

Goal state after:
case refine_1
α : 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
⊢ ⋃ n, F n = U

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
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
S : Set (Set α) := {S | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
this : MeasurableSpace α := MeasurableSpace.generateFrom S
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
b : α
ba : b < a
hbs : b ∈ s
x : α
h : x < a
hb : b < x
⊢ (Ioo b a).Nonempty

Tactic:
exact ⟨x, hb, h⟩

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x : α × β
s : Set α
t : Set β
⊢ infEDist x (s ×ˢ t) = max (infEDist x.1 s) (infEDist x.2 t)

Tactic:
by
  simp_rw +singlePass [infEDist, Prod.edist_eq, iInf_prod, Set.mem_prod, iInf_and, iInf_sup_eq,
    sup_iInf_eq, iInf_sup_eq, sup_iInf_eq]

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

Goal state before:
pp: case mp
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → y ∈ s
S : Set (Set α) := ⋯
this : MeasurableSpace α := ⋯
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
ha : ∀ b < a, (Ioo b a).Nonempty
y : α
⊢ y < a → ∃ i, ∃ (_ : i ∈ t), ∃ i_1, ∃ (_ : i_1 ∈ t) (_ : i < i_1) (_ : i_1 ≤ a), i ≤ y ∧ y < i_1

Tactic:
intro hy

Goal state after:
case mp
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → y ∈ s
S : Set (Set α) := {S | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ico l u = S}
this : MeasurableSpace α := MeasurableSpace.generateFrom S
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
ha : ∀ b < a, (Ioo b a).Nonempty
y : α
hy : y < a
⊢ ∃ i, ∃ (_ : i ∈ t), ∃ i_1, ∃ (_ : i_1 ∈ t) (_ : i < i_1) (_ : i_1 ≤ a), i ≤ y ∧ y < i_1
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s t : Set α
⊢ thickening δ (s ∪ t) = thickening δ s ∪ thickening δ t

Tactic:
simp_rw [thickening, infEDist_union, min_lt_iff, ofPred_or]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s₁ s₂ t₁ t₂ : Set α
⊢ hausdorffEDist (⋃ b, bif b then s₁ else s₂) (⋃ b, bif b then t₁ else t₂) ≤
    ⨆ b, bif b then hausdorffEDist s₁ t₁ else hausdorffEDist s₂ t₂

Tactic:
convert! hausdorffEDist_iUnion_le with (_ | _)

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x y : α
h : y ∈ s
⊢ infDist x (s ∩ closedBall x (dist y x)) = infDist x s

Tactic:
by
  replace h : y ∈ s ∩ closedBall x (dist y x) := ⟨h, mem_closedBall.2 le_rfl⟩
  refine le_antisymm ?_ (infDist_le_infDist_of_subset inter_subset_left ⟨y, h⟩)
  refine not_lt.1 fun hlt => ?_
  rcases (infDist_lt_iff ⟨y, h.1⟩).mp hlt with ⟨z, hzs, hz⟩
  rcases le_or_gt (dist z x) (dist y x) with hle | hlt
  · exact hz.not_ge (infDist_le_dist_of_mem ⟨hzs, hle⟩)
  · rw [dist_comm z, dist_comm y] at hlt
    exact (hlt.trans hz).not_ge (infDist_le_dist_of_mem h)

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

Goal state before:
pp: case h₂
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
x : α
hx : ∀ i ∈ s, infEDist x E ≤ ENNReal.ofReal i
⊢ ∀ (ε : ℝ≥0), 0 < ε → ENNReal.ofReal δ < ∞ → infEDist x E ≤ ENNReal.ofReal δ + ↑ε

Tactic:
intro η

Goal state after:
case h₂
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
x : α
hx : ∀ i ∈ s, infEDist x E ≤ ENNReal.ofReal i
η : ℝ≥0
⊢ 0 < η → ENNReal.ofReal δ < ∞ → infEDist x E ≤ ENNReal.ofReal δ + ↑η
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ cthickening δ E = ⋂ ε, ⋂ (_ : δ < ε), cthickening ε E

Tactic:
apply cthickening_eq_iInter_cthickening' (Ioi δ) rfl.subset

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ ∀ (ε : ℝ), δ < ε → (Ioi δ ∩ Ioc δ ε).Nonempty
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: 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

pp: 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

Tactic:
· obtain ⟨ε', -, hε'⟩ := hs ε (hsδ hε)
    have ss := cthickening_subset_thickening' (lt_of_le_of_lt δ_nn hε'.1) hε'.1 E
    exact ss.trans (thickening_mono hε'.2 E)

Goal state after:
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