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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s✝ : Set α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : Injective f ∧ ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)
μ : Measure β
s : Set α
hs : MeasurableSet s
t : Set α
⊢ MeasurableSet (f '' s)

Tactic:
exact hf.2 s hs

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 β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
hs :
  NullMeasurableSet s
    (if hf : Injective f ∧ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ then
      ((OuterMeasure.comap f) μ.toOuterMeasure).toMeasure ⋯
    else 0)
⊢ (if hf : Injective f ∧ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ then
        ((OuterMeasure.comap f) μ.toOuterMeasure).toMeasure ⋯
      else 0)
      s =
    μ (f '' s)

Tactic:
dif_pos (And.intro hfi hf)

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
hs : NullMeasurableSet s (((OuterMeasure.comap f) μ.toOuterMeasure).toMeasure ⋯)
⊢ (((OuterMeasure.comap f) μ.toOuterMeasure).toMeasure ⋯) s = μ (f '' s)
Module: Mathlib.MeasureTheory.Measure.Comap

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s : Set α
⊢ μ (f '' s) ≤
    (if hf : Injective f ∧ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ then
        ((OuterMeasure.comap f) μ.toOuterMeasure).toMeasure ⋯
      else 0)
      s

Tactic:
dif_pos (And.intro hfi hf)

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s : Set α
⊢ μ (f '' s) ≤ (((OuterMeasure.comap f) μ.toOuterMeasure).toMeasure ⋯) s
Module: Mathlib.MeasureTheory.Measure.Comap

Goal state before:
pp: β : Type u_2
mβ : MeasurableSpace β
μ : Measure β
s : Set β
hs : MeasurableSet s
⊢ μ ((fun x ↦ x) '' s) = μ s

pp: case hfi
β : Type u_2
mβ : MeasurableSpace β
μ : Measure β
s : Set β
hs : MeasurableSet s
⊢ Injective fun x ↦ x

pp: case hf
β : Type u_2
mβ : MeasurableSpace β
μ : Measure β
s : Set β
hs : MeasurableSet s
⊢ ∀ (s : Set β), MeasurableSet s → MeasurableSet ((fun x ↦ x) '' s)

pp: case hs
β : Type u_2
mβ : MeasurableSpace β
μ : Measure β
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet s

Tactic:
image_id'

Goal state after:
β : Type u_2
mβ : MeasurableSpace β
μ : Measure β
s : Set β
hs : MeasurableSet s
⊢ μ s = μ s

case hfi
β : Type u_2
mβ : MeasurableSpace β
μ : Measure β
s : Set β
hs : MeasurableSet s
⊢ Injective fun x ↦ x

case hf
β : Type u_2
mβ : MeasurableSpace β
μ : Measure β
s : Set β
hs : MeasurableSet s
⊢ ∀ (s : Set β), MeasurableSet s → MeasurableSet ((fun x ↦ x) '' s)

case hs
β : Type u_2
mβ : MeasurableSpace β
μ : Measure β
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet s
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:
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.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
μ ν : Measure α
s t : Set α
a : α
inst✝¹ : Countable ι
m : ι → Measure α
inst✝ : ∀ (n : ι), SFinite (m n)
⊢ SFinite (sum fun i ↦ sum (sfiniteSeq (m i)))

Tactic:
Measure.sum_sum

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
μ ν : Measure α
s t : Set α
a : α
inst✝¹ : Countable ι
m : ι → Measure α
inst✝ : ∀ (n : ι), SFinite (m n)
⊢ SFinite (sum fun p ↦ sfiniteSeq (m p.1) p.2)
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: R : Type u_1
α : Type u_2
β : Type u_3
δ : Type u_4
γ : Type u_5
ι : Type u_6
m0✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s'✝ t✝ : Set α
m0 : MeasurableSpace α
s : Set α
μ : Measure α
s' : Set α
hs' : MeasurableSet s'
t : Set α
this : μ (s ∩ t) = μ (s ∩ t ∩ s') + μ ((s ∩ t) \ s')
⊢ ((OuterMeasure.restrict s) μ.toOuterMeasure) t =
    ((OuterMeasure.restrict s) μ.toOuterMeasure) (t ∩ s') + ((OuterMeasure.restrict s) μ.toOuterMeasure) (t \ s')

Tactic:
simpa [← Set.inter_assoc, Set.inter_comm _ s, ← inter_sdiff_assoc]

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : s ⊆ t
⊢ μ (toMeasurable (μ.restrict t) s ∩ t) = (μ.restrict t) s

Tactic:
by
        rw [← restrict_apply (measurableSet_toMeasurable _ _), measure_toMeasurable]

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
⊢ (μ.restrict s) univ = μ s

Tactic:
by
  rw [restrict_apply MeasurableSet.univ, Set.univ_inter]

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

Goal state before:
pp: case refine_1
α : Type u_1
m : MeasurableSpace α
inst✝ : Countable α
μ ν : Measure α
h : ∀ (x : α), μ (measurableAtom x) = ν (measurableAtom x)
s : Set α
hs : MeasurableSet s
y : α
hy : y ∈ s
⊢ ∃ i ∈ s, y ∈ measurableAtom i

pp: case refine_2
α : Type u_1
m : MeasurableSpace α
inst✝ : Countable α
μ ν : Measure α
h : ∀ (x : α), μ (measurableAtom x) = ν (measurableAtom x)
s : Set α
hs : MeasurableSet s
y : α
x✝ : ∃ i ∈ s, y ∈ measurableAtom i
x : α
hx : x ∈ s
hy : y ∈ measurableAtom x
⊢ y ∈ s

Tactic:
· exact ⟨y, hy, mem_measurableAtom_self y⟩

Goal state after:
case refine_2
α : Type u_1
m : MeasurableSpace α
inst✝ : Countable α
μ ν : Measure α
h : ∀ (x : α), μ (measurableAtom x) = ν (measurableAtom x)
s : Set α
hs : MeasurableSet s
y : α
x✝ : ∃ i ∈ s, y ∈ measurableAtom i
x : α
hx : x ∈ s
hy : y ∈ measurableAtom x
⊢ y ∈ s
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)
⊢ μ (⋃₀ (measurableAtom '' s)) = ν (⋃₀ (measurableAtom '' s))

Tactic:
have h_count : (measurableAtom '' s).Countable := s.to_countable.image _

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
⊢ μ (⋃₀ (measurableAtom '' s)) = ν (⋃₀ (measurableAtom '' s))
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: case pos
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
m : ℕ → Measure α
hv : ∀ (n : ℕ), (m n) t ≠ ∞
hμ : μ = sum m
A : ∃ t' ⊇ t, MeasurableSet t' ∧ ∀ (u : Set α), MeasurableSet u → μ (t' ∩ u) = μ (t ∩ u)
ht : ∃ t_1 ⊇ t, MeasurableSet t_1 ∧ t_1 =ᵐ[μ] t
⊢ μ (ht.choose ∩ s) = μ (t ∩ s)

Tactic:
apply measure_congr
    exact ae_eq_set_inter ht.choose_spec.2.2 (ae_eq_refl _)

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
m : ℕ → Measure α
hv : ∀ (n : ℕ), (m n) t ≠ ∞
hμ : μ = sum m
⊢ μ (toMeasurable μ t ∩ s) = μ (t ∩ s)

Tactic:
have A : ∃ t', t' ⊇ t ∧ MeasurableSet t' ∧ ∀ u, MeasurableSet u → μ (t' ∩ u) = μ (t ∩ u) := by
    let w n := toMeasurable (m n) t
    have T : t ⊆ ⋂ n, w n := subset_iInter (fun i ↦ subset_toMeasurable (m i) t)
    have M : MeasurableSet (⋂ n, w n) :=
      MeasurableSet.iInter (fun i ↦ measurableSet_toMeasurable (m i) t)
    refine ⟨⋂ n, w n, T, M, fun u hu ↦ ?_⟩
    refine le_antisymm ?_ (by gcongr)
    rw [hμ, sum_apply _ (M.inter hu)]
    apply le_trans _ (le_sum_apply _ _)
    apply ENNReal.tsum_le_tsum (fun i ↦ ?_)
    calc
    m i ((⋂ n, w n) ∩ u) ≤ m i (w i ∩ u) := by gcongr; apply iInter_subset
    _ = m i (t ∩ u) := measure_toMeasurable_inter hu (hv i)
  -- thanks to the definition of `toMeasurable`, the previous property will also be shared
  -- by `toMeasurable μ t`, which is enough to conclude the proof.
  rw [toMeasurable]
  split_ifs with ht
  · apply measure_congr
    exact ae_eq_set_inter ht.choose_spec.2.2 (ae_eq_refl _)
  · exact A.choose_spec.2.2 s hs

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

Goal state before:
pp: case pos
α : 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) ≠ ∞
A : ∃ t' ⊇ t, MeasurableSet t' ∧ ∀ (u : Set α), MeasurableSet u → μ (t' ∩ u) = μ (t ∩ u)
ht : ∃ t_1 ⊇ t, MeasurableSet t_1 ∧ t_1 =ᵐ[μ] t
⊢ μ (ht.choose ∩ s) = μ (t ∩ s)

Tactic:
apply measure_congr
    exact ae_eq_set_inter ht.choose_spec.2.2 (ae_eq_refl _)

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

Goal state before:
pp: case refine_1.refine_2
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
n : ℕ
x✝ : MeasurableSet (natGeneratingSequence α n)
x : α
⊢ (∃ i, i n ∧ x ∈ countablyGeneratedAtom α i) → x ∈ natGeneratingSequence α n

Tactic:
rintro ⟨p, hpn, hpx⟩

Goal state after:
case refine_1.refine_2
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
n : ℕ
x✝ : MeasurableSet (natGeneratingSequence α n)
x : α
p : ℕ → Prop
hpn : p n
hpx : x ∈ countablyGeneratedAtom α p
⊢ x ∈ natGeneratingSequence α n
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
e : α ≃ᵐ β
μ : Measure β
s : Set α
⊢ (Measure.comap (⇑e) μ) s = μ (⇑e.symm ⁻¹' s)

Tactic:
e.measurableEmbedding.comap_apply,

Goal state after:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
e : α ≃ᵐ β
μ : Measure β
s : Set α
⊢ μ (⇑e '' s) = μ (⇑e.symm ⁻¹' s)
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case refine_1
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
⊢ ∀ t ∈ range (natGeneratingSequence α), MeasurableSet t → ∃ q, t = ⋃ p, if q p then countablyGeneratedAtom α p else ∅

pp: case refine_2
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
⊢ ∃ q, ∅ = ⋃ p, if q p then countablyGeneratedAtom α p else ∅

pp: case refine_3
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
⊢ ∀ (t : Set α),
    MeasurableSet t →
      (∃ q, t = ⋃ p, if q p then countablyGeneratedAtom α p else ∅) →
        ∃ q, tᶜ = ⋃ p, if q p then countablyGeneratedAtom α p else ∅

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:
· simp only [mem_range, forall_exists_index, forall_apply_eq_imp_iff]
    refine fun n _ ↦ ⟨fun p ↦ p n, ?_⟩
    ext x
    simp only [mem_iUnion, mem_ite_empty_right]
    refine ⟨fun hx ↦ ?_, ?_⟩
    · exact ⟨(x ∈ natGeneratingSequence α ·), by simp [countablyGeneratedAtom]; grind⟩
    · rintro ⟨p, hpn, hpx⟩
      simp only [countablyGeneratedAtom, mem_iInter] at hpx
      specialize hpx n
      simpa [hpn] using hpx

Goal state after:
case refine_2
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
⊢ ∃ q, ∅ = ⋃ p, if q p then countablyGeneratedAtom α p else ∅

case refine_3
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
⊢ ∀ (t : Set α),
    MeasurableSet t →
      (∃ q, t = ⋃ p, if q p then countablyGeneratedAtom α p else ∅) →
        ∃ q, tᶜ = ⋃ p, if q p then countablyGeneratedAtom α p else ∅

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 ∅
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
mβ : MeasurableSpace β
inst✝¹ : LinearOrder α
inst✝ : atTop.IsCountablyGenerated
x : α
g : α → β
g_meas : ∀ t > x, AEMeasurable g (μ.restrict (Ioc x t))
this : Nonempty α
u : ℕ → α
hu_tendsto : Tendsto u atTop atTop
Ioi_eq_iUnion : Ioi x = ⋃ n, Ioc x (u n)
⊢ AEMeasurable g (μ.restrict (Ioi x))

Tactic:
Ioi_eq_iUnion,

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
mβ : MeasurableSpace β
inst✝¹ : LinearOrder α
inst✝ : atTop.IsCountablyGenerated
x : α
g : α → β
g_meas : ∀ t > x, AEMeasurable g (μ.restrict (Ioc x t))
this : Nonempty α
u : ℕ → α
hu_tendsto : Tendsto u atTop atTop
Ioi_eq_iUnion : Ioi x = ⋃ n, Ioc x (u n)
⊢ AEMeasurable g (μ.restrict (⋃ n, Ioc x (u n)))
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : 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
k : ℕ
hk₁ : μ (t' k) ≤ ν (t' k)
hk₂ : ν (t' k) < μ (t' k)
⊢ k ∈ ∅

Tactic:
exact False.elim <| hk₂.not_ge hk₁

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

Goal state before:
pp: case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t' : ℕ → Set α
ht' : s ⊆ iUnion t'
⊢ sInf {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)} ≤ ∑' (n : ℕ), ⨅ μ_1 ∈ toOuterMeasure '' {μ, ν}, μ_1 (t' n)

Tactic:
simp only [iInf_image, coe_toOuterMeasure, iInf_pair]
    -- Conversely, fixing `t' : ℕ → Set α` such that `s ⊆ ⋃ n, t' n`, we construct `t : Set α`
    -- for which `μ (t ∩ s) + ν (tᶜ ∩ s) ≤ ∑' n, μ (t' n) ⊓ ν (t' n)`.
    -- Denoting `I := {n | μ (t' n) ≤ ν (t' n)}`, we set `t = ⋃ n ∈ I, t' n`.
    -- Clearly `μ (t ∩ s) ≤ ∑' n ∈ I, μ (t' n)` and `ν (tᶜ ∩ s) ≤ ∑' n ∉ I, ν (t' n)`, so
    -- `μ (t ∩ s) + ν (tᶜ ∩ s) ≤ ∑' n ∈ I, μ (t' n) + ∑' n ∉ I, ν (t' n)`
    -- where the RHS equals `∑' n, μ (t' n) ⊓ ν (t' n)` by the choice of `I`.
    set t := ⋃ n ∈ {k : ℕ | μ (t' k) ≤ ν (t' k)}, t' n with ht
    suffices hadd : μ (t ∩ s) + ν (tᶜ ∩ s) ≤ ∑' n, μ (t' n) ⊓ ν (t' n) by
      exact le_trans (sInf_le ⟨t, rfl⟩) hadd
    have hle₁ : μ (t ∩ s) ≤ ∑' (n : {k | μ (t' k) ≤ ν (t' k)}), μ (t' n) :=
      (measure_mono inter_subset_left).trans <| measure_biUnion_le _ (to_countable _) _
    have hcap : tᶜ ∩ s ⊆ ⋃ n ∈ {k | ν (t' k) < μ (t' k)}, t' n := by
      simp_rw [ht, compl_iUnion]
      refine fun x ⟨hx₁, hx₂⟩ ↦ mem_iUnion₂.2 ?_
      obtain ⟨i, hi⟩ := mem_iUnion.1 <| ht' hx₂
      refine ⟨i, ?_, hi⟩
      by_contra h
      simp only [mem_ofPred_eq, not_lt] at h
      exact mem_iInter₂.1 hx₁ i h hi
    have hle₂ : ν (tᶜ ∩ s) ≤ ∑' (n : {k | ν (t' k) < μ (t' k)}), ν (t' n) :=
      (measure_mono hcap).trans (measure_biUnion_le ν (to_countable {k | ν (t' k) < μ (t' k)}) _)
    refine (add_le_add hle₁ hle₂).trans ?_
    have heq : {k | μ (t' k) ≤ ν (t' k)} ∪ {k | ν (t' k) < μ (t' k)} = univ := by
      ext k; simp [le_or_gt]
    conv in ∑' (n : ℕ), μ (t' n) ⊓ ν (t' n) => rw [← tsum_univ, ← heq]
    rw [ENNReal.summable.tsum_union_disjoint (f := fun n ↦ μ (t' n) ⊓ ν (t' n)) ?_ ENNReal.summable]
    · refine add_le_add (tsum_congr ?_).le (tsum_congr ?_).le
      · rw [Subtype.forall]
        intro n hn; simpa
      · rw [Subtype.forall]
        intro n hn
        rw [mem_ofPred_eq] at hn
        simp [le_of_lt hn]
    · rw [Set.disjoint_iff]
      rintro k ⟨hk₁, hk₂⟩
      rw [mem_ofPred_eq] at hk₁ hk₂
      exact False.elim <| hk₂.not_ge hk₁

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
⊢ m0 ≤ ⊤.caratheodory

Tactic:
by rw [OuterMeasure.top_caratheodory]; exact le_top

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : T1Space X
hs : s.Countable
⊢ IsGδ sᶜ

Tactic:
rw [← biUnion_of_singleton s, compl_iUnion₂]

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : T1Space X
hs : s.Countable
⊢ IsGδ (⋂ i ∈ s, {i}ᶜ)
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
d : ℝ≥0∞
⊢ d ≤ infEDist x s ↔ ∀ y ∈ s, d ≤ edist x y

Tactic:
simp only [infEDist, le_iInf_iff]

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

Tactic:
· rintro ⟨y1, y2⟩ hy
        simp only [mem_iUnion, mem_prod, exists_and_left, exists_prop] at hy
        rcases hy with ⟨a, ya, -, b, -, yb, hb⟩
        exact hb (mem_prod.2 ⟨ya, yb⟩)

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

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

Tactic:
hausdorffEDist_comm

Goal state after:
case inl.inr
α : Type u
inst✝ : PseudoEMetricSpace α
t : Set α
fin : hausdorffEDist t ∅ ≠ ∞
ht : t.Nonempty
⊢ ∅ = ∅ ∧ t = ∅ ∨ ∅.Nonempty ∧ t.Nonempty
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
t : Set α
x : α
Φ : α → β
hΦ : Isometry Φ
⊢ infDist (Φ x) (Φ '' t) = infDist x t

Tactic:
simp [infDist, infEDist_image hΦ]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
x : α
xs : x ∈ s
y : α
yt : y ∈ t
⊢ hausdorffDist s t ≤ diam (s ∪ t)

Tactic:
refine hausdorffDist_le_of_mem_dist diam_nonneg ?_ ?_

Goal state after:
case refine_1
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
x : α
xs : x ∈ s
y : α
yt : y ∈ t
⊢ ∀ x ∈ s, ∃ y ∈ t, dist x y ≤ diam (s ∪ t)

case refine_2
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
x : α
xs : x ∈ s
y : α
yt : y ∈ t
⊢ ∀ x ∈ t, ∃ y ∈ s, dist x y ≤ diam (s ∪ t)
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
y : α
r : ℝ
h : y ∈ t
H : hausdorffDist t s < r
fin : hausdorffEDist s t ≠ ∞
⊢ ∃ x ∈ s, dist x y < r

Tactic:
hausdorffEDist_comm

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
y : α
r : ℝ
h : y ∈ t
H : hausdorffDist t s < r
fin : hausdorffEDist t s ≠ ∞
⊢ ∃ x ∈ s, dist x y < r
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

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

Tactic:
hausdorffEDist_comm

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
x : α
fin : hausdorffEDist t s ≠ ∞
h : ¬s.Nonempty
⊢ ¬t.Nonempty
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

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

Tactic:
hausdorffEDist_comm

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s t u : Set α
fin : hausdorffEDist t s ≠ ∞
h : ¬hausdorffEDist s u = ∞
⊢ ¬hausdorffEDist t u = ∞
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s t u : Set α
fin : hausdorffEDist t u ≠ ∞
⊢ hausdorffDist s u ≤ hausdorffDist s t + hausdorffDist t u

Tactic:
hausdorffEDist_comm

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s t u : Set α
fin : hausdorffEDist u t ≠ ∞
⊢ hausdorffDist s u ≤ hausdorffDist s t + hausdorffDist t u
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : MeasurableSpace α
f : α →ₛ β
g : α →ₛ γ
b : β
c : γ
⊢ ⇑(f.pair g) ⁻¹' {b} ×ˢ {c} = ⇑f ⁻¹' {b} ∩ ⇑g ⁻¹' {c}

Tactic:
exact pair_preimage _ _ _ _

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

Goal state before:
pp: α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
f : δ → α
hf : ∀ (x : α), MeasurableSet (f ⁻¹' Iic x)
⊢ Measurable f

Tactic:
by
  apply measurable_of_Ioi
  simp_rw [← compl_Iic, preimage_compl, MeasurableSet.compl_iff]
  assumption

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

Goal state before:
pp: case refine_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
⊢ MeasurableSet (range (Prod.map g f))

Tactic:
rw [range_prodMap]
    exact hg.measurableSet_range.prod hf.measurableSet_range

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
a : α
⊢ ⨆ i, ∑ n ∈ Finset.range (i + 1), ↑((eapproxDiff f n) a) = f a

Tactic:
sum_eapproxDiff,

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
a : α
⊢ ⨆ i, (eapprox f i) a = f a
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
x₀ : α
x₀s : x₀ ∈ s
h₀ : IsTop x₀
⊢ s = {x₀} ∪ s \ {x₀}

Tactic:
rw [union_sdiff_cancel (singleton_subset_iff.2 x₀s)]

Goal state after: