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

Goal state before:
pp: case refine_2
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
T : Finset ↑s
f : ↑s → Set α
h_t' : ∀ b ∈ T, f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b ∈ s, g b)
this : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b, (g ∘ Subtype.val) b)
b : β
h_b_w : b ∈ s
h_b_h : ⟨b, ⋯⟩ ∈ T
h_b_alt : b = ↑⟨b, h_b_w⟩
⊢ Function.extend (fun x ↦ ↑x) f (fun x ↦ ∅) b ∈ g b

Tactic:
h_b_alt,

Goal state after:
case refine_2
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
T : Finset ↑s
f : ↑s → Set α
h_t' : ∀ b ∈ T, f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b ∈ s, g b)
this : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b, (g ∘ Subtype.val) b)
b : β
h_b_w : b ∈ s
h_b_h : ⟨b, ⋯⟩ ∈ T
h_b_alt : b = ↑⟨b, h_b_w⟩
⊢ Function.extend (fun x ↦ ↑x) f (fun x ↦ ∅) ↑⟨b, h_b_w⟩ ∈ g ↑⟨b, h_b_w⟩
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
⊢ generateFrom (piiUnionInter (fun n ↦ {s | MeasurableSet s}) S) = ⨆ i ∈ S, m i

Tactic:
refine le_antisymm ?_ ?_

Goal state after:
case refine_1
α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
⊢ generateFrom (piiUnionInter (fun n ↦ {s | MeasurableSet s}) S) ≤ ⨆ i ∈ S, m i

case refine_2
α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
⊢ ⨆ i ∈ S, m i ≤ generateFrom (piiUnionInter (fun n ↦ {s | MeasurableSet s}) S)
Module: Mathlib.MeasureTheory.Measure.Map

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

Tactic:
map,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
s : Set β
hs : NullMeasurableSet s (if hf : AEMeasurable f μ then (mapₗ (AEMeasurable.mk f hf)) μ else 0)
⊢ (if hf : AEMeasurable f μ then (mapₗ (AEMeasurable.mk f hf)) μ else 0) s = μ (f ⁻¹' s)
Module: Mathlib.MeasureTheory.Measure.NullMeasurable

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ✝ : Measure α
s t : Set α
x✝ : MeasurableSpace α
μ : Measure α
⊢ μ.trim ≤ μ.toOuterMeasure

Tactic:
nth_rewrite 2 [← μ.trimmed]
    exact OuterMeasure.trim_anti_measurableSpace _ fun _ ↦ MeasurableSet.nullMeasurableSet

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure α
s : Set β
t : Set β := f '' toMeasurable μ (f ⁻¹' s) ∪ (range f)ᶜ
⊢ (map f μ) s ≤ μ (f ⁻¹' s)

Tactic:
have htm : MeasurableSet t :=
    (hf.measurableSet_image.2 <| measurableSet_toMeasurable _ _).union
      hf.measurableSet_range.compl

Goal state after:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure α
s : Set β
t : Set β := f '' toMeasurable μ (f ⁻¹' s) ∪ (range f)ᶜ
htm : MeasurableSet t
⊢ (map f μ) s ≤ μ (f ⁻¹' s)
Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving (⇑e) μ μ
he' : QuasiMeasurePreserving (⇑e.symm) μ μ
k : ℤ
hs : ⇑e '' s =ᵐ[μ] s
⊢ ⇑(e ^ k) '' s =ᵐ[μ] s

Tactic:
by
  rw [Equiv.image_eq_preimage_symm]
  obtain ⟨k, rfl | rfl⟩ := k.eq_nat_or_neg
  · replace hs : (⇑e⁻¹) ⁻¹' s =ᵐ[μ] s := by rwa [Equiv.image_eq_preimage_symm] at hs
    replace he' : (⇑e⁻¹)^[k] ⁻¹' s =ᵐ[μ] s := he'.preimage_iterate_ae_eq k hs
    rwa [Equiv.Perm.iterate_eq_pow e⁻¹ k, inv_pow e k] at he'
  · rw [zpow_neg, zpow_natCast]
    replace hs : e ⁻¹' s =ᵐ[μ] s := by
      convert! he.preimage_ae_eq hs.symm
      rw [Equiv.preimage_image]
    replace he : (⇑e)^[k] ⁻¹' s =ᵐ[μ] s := he.preimage_iterate_ae_eq k hs
    rwa [Equiv.Perm.iterate_eq_pow e k] at he

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

Goal state before:
pp: α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : ι → Set α
hs : ∀ (i : ι), NullMeasurableSet (s i) μ
H : Pairwise (AEDisjoint μ on s)
⊢ ∑' (i : ι), μ (s i) ≤ μ univ

Tactic:
rw [ENNReal.tsum_eq_iSup_sum]
  exact iSup_le fun s =>
    sum_measure_le_measure_univ (fun i _hi => hs i) fun i _hi j _hj hij => H hij

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
t : ℕ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) t
T : ℕ → Set α := fun n ↦ toMeasurable μ (t n)
Td : ℕ → Set α := disjointed T
hm : ∀ (n : ℕ), MeasurableSet (Td n)
⊢ μ (⋃ n, t n) = μ (⋃ n, Td n)

Tactic:
iUnion_disjointed,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
t : ℕ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) t
T : ℕ → Set α := fun n ↦ toMeasurable μ (t n)
Td : ℕ → Set α := disjointed T
hm : ∀ (n : ℕ), MeasurableSet (Td n)
⊢ μ (⋃ n, t n) = μ (⋃ i, T i)
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite ν
⊢ μ.restrict (⋃ i, disjointed (spanningSets ν) i) = μ

Tactic:
iUnion_disjointed,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite ν
⊢ μ.restrict (⋃ i, spanningSets ν i) = μ
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
ι : Type u_4
x✝ : MeasurableSpace α
μ : Measure α
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ
As_disj : Pairwise (AEDisjoint μ on As)
Union_As_finite : μ (⋃ i, As i) ≠ ∞
posmeas : Set ι := {i | 0 < μ (As i)}
posmeas_def : posmeas = {i | 0 < μ (As i)}
as : ℕ → ℝ≥0∞
left✝ : StrictAnti as
as_mem : ∀ (n : ℕ), as n ∈ Ioo 0 1
as_lim : Tendsto as atTop (𝓝 0)
fairmeas : ℕ → Set ι := fun n ↦ {i | as n ≤ μ (As i)}
n : ℕ
⊢ fairmeas n = (fun i ↦ μ (As i)) ⁻¹' Ici (as n)

Tactic:
simp only [fairmeas]
      rfl

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
inst✝ : Countable α
μ ν : Measure α
h : ∀ (x : α), μ (measurableAtom x) = ν (measurableAtom x)
s : Set α
hs : MeasurableSet s
h1 : s = ⋃₀ (measurableAtom '' s)
h_count : (measurableAtom '' s).Countable
h_disj : (measurableAtom '' s).Pairwise Disjoint
t : Set α
x : α
hxs : x ∈ s
hx : measurableAtom x = t
⊢ MeasurableSet t

Tactic:
rw [← hx]

Goal state after:
α : Type u_1
m : MeasurableSpace α
inst✝ : Countable α
μ ν : Measure α
h : ∀ (x : α), μ (measurableAtom x) = ν (measurableAtom x)
s : Set α
hs : MeasurableSet s
h1 : s = ⋃₀ (measurableAtom '' s)
h_count : (measurableAtom '' s).Countable
h_disj : (measurableAtom '' s).Pairwise Disjoint
t : Set α
x : α
hxs : x ∈ s
hx : measurableAtom x = t
⊢ MeasurableSet (measurableAtom x)
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)
⊢ t ⊆ t ∩ ⋃ i, disjointed w i

Tactic:
iUnion_disjointed,

Goal state after:
α : 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)
⊢ t ⊆ t ∩ ⋃ i, w i
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: case e_f
α : Type u_1
m : MeasurableSpace α
inst✝ : Countable α
μ ν : Measure α
h : ∀ (x : α), μ (measurableAtom x) = ν (measurableAtom x)
s : Set α
hs : MeasurableSet s
h1 : s = ⋃₀ (measurableAtom '' s)
h_count : (measurableAtom '' s).Countable
h_disj : (measurableAtom '' s).Pairwise Disjoint
h_meas : ∀ t ∈ measurableAtom '' s, MeasurableSet t
s' : ↑(measurableAtom '' s)
x : α
hxs : x ∈ s
hx : measurableAtom x = ↑s'
⊢ μ ↑s' = ν ↑s'

Tactic:
rw [← hx]

Goal state after:
case e_f
α : Type u_1
m : MeasurableSpace α
inst✝ : Countable α
μ ν : Measure α
h : ∀ (x : α), μ (measurableAtom x) = ν (measurableAtom x)
s : Set α
hs : MeasurableSet s
h1 : s = ⋃₀ (measurableAtom '' s)
h_count : (measurableAtom '' s).Countable
h_disj : (measurableAtom '' s).Pairwise Disjoint
h_meas : ∀ t ∈ measurableAtom '' s, MeasurableSet t
s' : ↑(measurableAtom '' s)
x : α
hxs : x ∈ s
hx : measurableAtom x = ↑s'
⊢ μ (measurableAtom x) = ν (measurableAtom x)
Module: Mathlib.MeasureTheory.Measure.Trim

Goal state before:
pp: case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
h : IsFiniteMeasure (μ.trim ⋯)
h_univ : (μ.trim ⋯) Set.univ < ∞
⊢ μ Set.univ < ∞

Tactic:
trim_measurableSet_eq bot_le MeasurableSet.univ

Goal state after:
case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
h : IsFiniteMeasure (μ.trim ⋯)
h_univ : μ Set.univ < ∞
⊢ μ Set.univ < ∞
Module: Mathlib.MeasureTheory.Measure.Trim

Goal state before:
pp: case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
h : IsFiniteMeasure μ
h_univ : μ Set.univ < ∞
⊢ (μ.trim ⋯) Set.univ < ∞

Tactic:
trim_measurableSet_eq bot_le MeasurableSet.univ

Goal state after:
case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
h : IsFiniteMeasure μ
h_univ : μ Set.univ < ∞
⊢ μ Set.univ < ∞
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : MeasurableSet s
ht : (μ + ν) t ≠ ∞
⊢ (μ + ν) (toMeasurable (μ + ν) t) ≠ ∞

Tactic:
rwa [measure_toMeasurable t]

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

Goal state before:
pp: case refine_3
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
q : (ℕ → Prop) → Prop
htq : t = ⋃ p, if q p then countablyGeneratedAtom α p else ∅
x : α
⊢ (∀ (i : ℕ → Prop), q i → x ∉ countablyGeneratedAtom α i) ↔ ∃ i, ¬q i ∧ x ∈ countablyGeneratedAtom α i

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩

Goal state after:
case refine_3.refine_1
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
q : (ℕ → Prop) → Prop
htq : t = ⋃ p, if q p then countablyGeneratedAtom α p else ∅
x : α
h : ∀ (i : ℕ → Prop), q i → x ∉ countablyGeneratedAtom α i
⊢ ∃ i, ¬q i ∧ x ∈ countablyGeneratedAtom α i

case refine_3.refine_2
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
q : (ℕ → Prop) → Prop
htq : t = ⋃ p, if q p then countablyGeneratedAtom α p else ∅
x : α
⊢ (∃ i, ¬q i ∧ x ∈ countablyGeneratedAtom α i) → ∀ (i : ℕ → Prop), q i → x ∉ countablyGeneratedAtom α i
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
⊢ s.indicator f =ᵐ[μ.restrict sᶜ] 0

Tactic:
by
  classical exact piecewise_ae_eq_restrict_compl hs

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ : Measure α
g : β → γ
f : α → β
hg : AEMeasurable g (Measure.map f μ)
hf : AEMeasurable f μ
s : Set γ
hs : MeasurableSet s
⊢ (Measure.map g (Measure.map f μ)) s = (Measure.map (g ∘ f) μ) s

Tactic:
map_apply_of_aemeasurable hg hs,

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ : Measure α
g : β → γ
f : α → β
hg : AEMeasurable g (Measure.map f μ)
hf : AEMeasurable f μ
s : Set γ
hs : MeasurableSet s
⊢ (Measure.map f μ) (g ⁻¹' s) = (Measure.map (g ∘ f) μ) s
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: case refine_2.refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t' : ℕ → Set α
ht' : s ⊆ iUnion t'
t : Set α := ⋃ n ∈ {k | μ (t' k) ≤ ν (t' k)}, t' n
ht : t = ⋃ n ∈ {k | μ (t' k) ≤ ν (t' k)}, t' n
hle₁ : μ (t ∩ s) ≤ ∑' (n : ↑{k | μ (t' k) ≤ ν (t' k)}), μ (t' ↑n)
hcap : tᶜ ∩ s ⊆ ⋃ n ∈ {k | ν (t' k) < μ (t' k)}, t' n
hle₂ : ν (tᶜ ∩ s) ≤ ∑' (n : ↑{k | ν (t' k) < μ (t' k)}), ν (t' ↑n)
heq : {k | μ (t' k) ≤ ν (t' k)} ∪ {k | ν (t' k) < μ (t' k)} = univ
⊢ ∀ (b : ↑{k | ν (t' k) < μ (t' k)}), ν (t' ↑b) = min (μ (t' ↑b)) (ν (t' ↑b))

Tactic:
rw [Subtype.forall]
        intro n hn
        rw [mem_ofPred_eq] at hn
        simp [le_of_lt hn]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
ι : Type u_8
ι' : Type u_9
e : ι' ≃ ι
m : ι → Measure α
⊢ sum (m ∘ ⇑e) = sum m

Tactic:
by
  ext s hs
  simpa [hs, sum_apply] using e.tsum_eq (fun n ↦ m n s)

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

Goal state before:
pp: M : Type u_2
ι : Type u_3
α : Type u_4
inst✝² : CommMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
f : ι → α → M
s : Finset ι
hf : ∀ i ∈ s, Measurable (f i)
⊢ Measurable fun a ↦ ∏ i ∈ s, f i a

Tactic:
by
  simp_rw [← Finset.prod_apply]
  exact Finset.prod_induction _ _ (fun _ _ => Measurable.mul) (@measurable_one M _ _ _ _) hf

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

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ borel α = MeasurableSpace.generateFrom (range Iio)

Tactic:
by
  refine le_antisymm ?_ (generateFrom_le ?_)
  · rw [borel_eq_generateFrom_of_subbasis (@OrderTopology.topology_eq_generate_intervals α _ _ _)]
    let : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
    have H : ∀ a : α, MeasurableSet (Iio a) := fun a => GenerateMeasurable.basic _ ⟨_, rfl⟩
    refine generateFrom_le ?_
    rintro _ ⟨a, rfl | rfl⟩
    · rcases em (∃ b, a ⋖ b) with ⟨b, hb⟩ | hcovBy
      · rw [hb.Ioi_eq, ← compl_Iio]
        exact (H _).compl
      · rcases isOpen_biUnion_countable (Ioi a) Ioi fun _ _ ↦ isOpen_Ioi with ⟨t, hat, htc, htU⟩
        have : Ioi a = ⋃ b ∈ t, Ici b := by
          refine Subset.antisymm ?_ <| iUnion₂_subset fun b hb ↦ Ici_subset_Ioi.2 (hat hb)
          refine Subset.trans ?_ <| iUnion₂_mono fun _ _ ↦ Ioi_subset_Ici_self
          simpa [CovBy, htU, subset_def] using hcovBy
        simp only [this, ← compl_Iio]
        exact .biUnion htc <| fun _ _ ↦ (H _).compl
    · apply H
  · rw [forall_mem_range]
    intro a
    exact GenerateMeasurable.basic _ isOpen_Iio

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

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ MeasurableSpace.generateFrom (range Ioi) = MeasurableSpace.generateFrom (range Iic)

Tactic:
refine le_antisymm ?_ ?_

Goal state after:
case refine_1
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ MeasurableSpace.generateFrom (range Ioi) ≤ MeasurableSpace.generateFrom (range Iic)

case refine_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ MeasurableSpace.generateFrom (range Iic) ≤ MeasurableSpace.generateFrom (range Ioi)
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 α
⊢ MeasurableSet s

Tactic:
let F : Set α → Set β := fun a ↦ {y | ∃ b, IsOpen b ∧ y ∈ b ∧ a ×ˢ b ⊆ s}

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}
⊢ MeasurableSet s
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x : α
E : Set α
⊢ 0 < infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E) ↔
    x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E

Tactic:
rw [infEDist_closure, infEDist_pos_iff_notMem_closure]

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

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)
⊢ ⋃ a ∈ countableBasis β, F a ×ˢ a ⊆ s

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:
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)
⊢ ⋃ a ∈ countableBasis β, F a ×ˢ a ⊆ s
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
hs : IsCompact s
hne : s.Nonempty
x : α
A : Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, _] fun y ↦ edist x y
y : α
ys : y ∈ s
hy : IsMinOn (fun y ↦ edist x y) s y
⊢ edist x y ≤ infEDist x s

Tactic:
le_infEDist

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
hs : IsCompact s
hne : s.Nonempty
x : α
A : Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, _] fun y ↦ edist x y
y : α
ys : y ∈ s
hy : IsMinOn (fun y ↦ edist x y) s y
⊢ ∀ y_1 ∈ s, edist x y ≤ edist x y_1
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
hst : Disjoint s t
⊢ ∃ r, 0 < r ∧ ∀ x ∈ s, ∀ y ∈ t, ↑r < edist x y

Tactic:
rcases s.eq_empty_or_nonempty with (rfl | hne)
  · use 1
    simp
  obtain ⟨x, hx, h⟩ := hs.exists_isMinOn hne continuous_infEDist.continuousOn
  have : 0 < infEDist x t :=
    pos_iff_ne_zero.2 fun H => hst.le_bot ⟨hx, (mem_iff_infEDist_zero_of_closed ht).mpr H⟩
  rcases ENNReal.lt_iff_exists_nnreal_btwn.1 this with ⟨r, h₀, hr⟩
  exact ⟨r, ENNReal.coe_pos.mp h₀, fun y hy z hz => hr.trans_le <| le_infEDist.1 (h hy) z hz⟩

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
⊢ hausdorffEDist (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) t = hausdorffEDist s t

Tactic:
refine le_antisymm ?_ ?_

Goal state after:
case refine_1
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
⊢ hausdorffEDist (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) t ≤ hausdorffEDist s t

case refine_2
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
⊢ hausdorffEDist s t ≤ hausdorffEDist (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) t
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: case inl.inl
α : Type u
inst✝ : PseudoEMetricSpace α
fin : hausdorffEDist ∅ ∅ ≠ ∞
⊢ ∅ = ∅ ∧ ∅ = ∅ ∨ ∅.Nonempty ∧ ∅.Nonempty

Tactic:
exact Or.inl ⟨rfl, rfl⟩

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

Goal state before:
pp: case neg
α : 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 = ∅
⊢ MeasurableSet (Iio a)

Tactic:
replace ha : a ∈ s := hIoo ha.choose a ha.choose_spec.1 ha.choose_spec.2
    convert_to MeasurableSet (⋃ (l ∈ t) (_ : l < a), Ico l a)
    · symm
      simp only [← Ici_inter_Iio, ← iUnion_inter, inter_eq_right, subset_def, mem_iUnion,
        mem_Ici, mem_Iio]
      intro x hx
      rcases htd.exists_le' (fun b hb => htb _ hb (hbot b hb)) x with ⟨z, hzt, hzx⟩
      exact ⟨z, hzt, hzx.trans_lt hx, hzx⟩
    · refine .biUnion hc fun x hx => MeasurableSet.iUnion fun hlt => ?_
      exact .basic _ ⟨x, hts hx, a, ha, hlt, mem_singleton _⟩

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
⊢ infEDist x s = ∞ ↔ s = ∅

Tactic:
rcases s.eq_empty_or_nonempty with rfl | hs <;> simp [*, Nonempty.ne_empty, infEDist_ne_top]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x y : α
⊢ infDist x {y} = dist x y

Tactic:
by simp [infDist, dist_edist]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
r : ℝ
hs : s.Nonempty
⊢ (∀ y ∈ s, r ≤ (edist x y).toReal) ↔ ∀ ⦃y : α⦄, y ∈ s → r ≤ dist x y

Tactic:
← dist_edist

Goal state after: