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

Goal state before:
pp: case refine_2.a
α : 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 γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n ↦ F^[n] univ
n : ℕ
⊢ F (iInter X) ⊆ F^[n] univ

Tactic:
cases n

Goal state after:
case refine_2.a.zero
α : 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 γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n ↦ F^[n] univ
⊢ F (iInter X) ⊆ F^[0] univ

case refine_2.a.succ
α : 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 γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n ↦ F^[n] univ
n✝ : ℕ
⊢ F (iInter X) ⊆ F^[n✝ + 1] univ
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: case refine_2.a.zero
α : 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 γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n ↦ F^[n] univ
⊢ F (iInter X) ⊆ F^[0] univ

Tactic:
exact subset_univ _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m' : MeasurableSpace β
inst✝ : BooleanAlgebra β
h : Measurable compl
f : α → β
⊢ MeasurableSpace.comap (fun a ↦ (f a)ᶜ) inferInstance = MeasurableSpace.comap f inferInstance

Tactic:
by
  rw [← Function.comp_def, ← MeasurableSpace.comap_comp]
  congr
  exact (MeasurableEquiv.ofInvolutive _ compl_involutive h).measurableEmbedding.comap_eq

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t s : Set α
ht : NullMeasurableSet t μ
s' : Set α
hsub : s ⊆ s'
hs' : μ s' = μ s
hs'm : NullMeasurableSet s' μ
⊢ μ (s ∩ t) + μ (s \ t) ≤ μ s

Tactic:
calc
    μ (s ∩ t) + μ (s \ t) ≤ μ (s' ∩ t) + μ (s' \ t) := by gcongr
    _ = μ (s' ∩ t ∪ s' \ t) :=
      (measure_union₀_aux (hs'm.inter ht) (hs'm.diff ht) <|
          (@disjoint_inf_sdiff _ s' t _).aedisjoint).symm
    _ = μ s' := congr_arg μ (inter_union_sdiff _ _)
    _ = μ s := hs'

Goal state after:
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) ≤ (comap f μ) s

Tactic:
by
  rw [comap, dif_pos (And.intro hfi hf)]
  exact le_toMeasure_apply _ _ _

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 (comap f μ)
⊢ f '' s =ᵐ[μ] toMeasurable μ (f '' toMeasurable (comap f μ) s)

Tactic:
refine EventuallyEq.trans ?_ (NullMeasurableSet.toMeasurable_ae_eq ?_).symm

Goal state after:
case refine_1
α : 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 (comap f μ)
⊢ f '' s =ᵐ[μ] f '' toMeasurable (comap f μ) s

case refine_2
α : 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 (comap f μ)
⊢ NullMeasurableSet (f '' toMeasurable (comap f μ) s) μ
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
t s : Set α
ht : MeasurableSet t
⊢ μ (s ∪ t) + μ (s ∩ t) = μ s + μ t

Tactic:
rw [← measure_inter_add_sdiff (s ∪ t) ht, Set.union_inter_cancel_right, union_sdiff_right, ←
    measure_inter_add_sdiff s ht]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
t s : Set α
ht : MeasurableSet t
⊢ μ t + μ (s \ t) + μ (s ∩ t) = μ (s ∩ t) + μ (s \ t) + μ t
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, NullMeasurableSet (t i) μ
H : (↑s).Pairwise (AEDisjoint μ on t)
⊢ ∑ i ∈ s, μ (t i) ≤ μ univ

Tactic:
by
  rw [← measure_biUnion_finset₀ H h]
  exact measure_mono (subset_univ _)

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

Goal state before:
pp: case inr
X : Type u_1
inst✝⁶ : LinearOrder X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : OrderTopology X
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : NoMaxOrder X
inst✝ : NoMinOrder X
f g : α → X
hl : Tendsto f atTop atTop
hu : Tendsto g atBot atBot
x : X
h✝ : Nonempty α
x_L : X
hx_L : x_L < x
x_R : X
hx_R : x < x_R
a_L : α
ha_L : ∀ a ≤ a_L, g a ≤ x_L
a_R : α
ha_R : ∀ a ≥ a_R, x_R ≤ f a
⊢ ∃ t ∈ 𝓝 x, {i | ((fun n ↦ Icc (f n) (g n)) i ∩ t).Nonempty}.Finite

Tactic:
refine ⟨Ioo x_L x_R, Ioo_mem_nhds hx_L hx_R, (finite_Icc a_L a_R).subset ?_⟩

Goal state after:
case inr
X : Type u_1
inst✝⁶ : LinearOrder X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : OrderTopology X
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : NoMaxOrder X
inst✝ : NoMinOrder X
f g : α → X
hl : Tendsto f atTop atTop
hu : Tendsto g atBot atBot
x : X
h✝ : Nonempty α
x_L : X
hx_L : x_L < x
x_R : X
hx_R : x < x_R
a_L : α
ha_L : ∀ a ≤ a_L, g a ≤ x_L
a_R : α
ha_R : ∀ a ≥ a_R, x_R ≤ f a
⊢ {i | ((fun n ↦ Icc (f n) (g n)) i ∩ Ioo x_L x_R).Nonempty} ⊆ Icc a_L a_R
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 α
⊢ ((OuterMeasure.restrict s) μ.toOuterMeasure) t =
    ((OuterMeasure.restrict s) μ.toOuterMeasure) (t ∩ s') + ((OuterMeasure.restrict s) μ.toOuterMeasure) (t \ s')

Tactic:
suffices μ (s ∩ t) = μ (s ∩ t ∩ s') + μ ((s ∩ t) \ s') by
      simpa [← Set.inter_assoc, Set.inter_comm _ s, ← inter_sdiff_assoc]
    exact le_toOuterMeasure_caratheodory _ _ hs' _

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
x : α
s : Set α
xs : x ∈ s
hs : IsOpen[inst✝¹] s
v : Set α
xv : x ∈ v
hv : IsOpen[inst✝¹] v
μv : μ v < ∞
⊢ ∃ v ∈ {s | IsOpen[inst✝¹] s ∧ μ s < ∞}, x ∈ v ∧ v ⊆ s

Tactic:
refine ⟨v ∩ s, ⟨hv.inter hs, lt_of_le_of_lt ?_ μv⟩, ⟨xv, xs⟩, inter_subset_right⟩

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
x : α
s : Set α
xs : x ∈ s
hs : IsOpen[inst✝¹] s
v : Set α
xv : x ∈ v
hv : IsOpen[inst✝¹] v
μv : μ v < ∞
⊢ μ (v ∩ s) ≤ μ v
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s : Set α
ν : Measure β
f : α → β
hf : QuasiMeasurePreserving f μ ν
t : Set β
hmaps : MapsTo f s t
u : Set β
hum : MeasurableSet u
hu : ν (u ∩ t) = 0
⊢ f ⁻¹' u ∩ s ⊆ f ⁻¹' (u ∩ t)

Tactic:
preimage_inter

Goal state after:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s : Set α
ν : Measure β
f : α → β
hf : QuasiMeasurePreserving f μ ν
t : Set β
hmaps : MapsTo f s t
u : Set β
hum : MeasurableSet u
hu : ν (u ∩ t) = 0
⊢ f ⁻¹' u ∩ s ⊆ f ⁻¹' u ∩ f ⁻¹' t
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: α : 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
T_ne : T.Nonempty
f : ℕ → Set α
hf : T = range f
fS : ∀ (n : ℕ), f n ∈ S
x : α
t : Set α
tT : t ∈ range f
xt : x ∈ t
⊢ ∃ n, f n = t

Tactic:
by simpa only using! tT

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

Goal state before:
pp: α : Type u_2
δ : Type u_4
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
f g : α → δ
⊢ (∀ᶠ (x : α) in ⨆ i, ae (μ.restrict (s i)), f x = g x) ↔ ∀ (i : ι), ∀ᵐ (x : α) ∂μ.restrict (s i), f x = g x

Tactic:
eventually_iSup

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

Goal state before:
pp: α : Type u_2
δ : Type u_4
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
s : ι → Set α
t : Set ι
ht : t.Countable
f g : α → δ
⊢ (∀ᶠ (x : α) in ⨆ i ∈ t, ae (μ.restrict (s i)), f x = g x) ↔ ∀ i ∈ t, ∀ᵐ (x : α) ∂μ.restrict (s i), f x = g x

Tactic:
eventually_iSup

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 α
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 : ℕ), μ (t ∩ disjointed w n ∩ u) = ∑' (n : ℕ), (μ.restrict (t ∩ u)) (disjointed w n)

Tactic:
congr 1
        ext1 n
        rw [restrict_apply, inter_comm t _, inter_assoc]
        refine MeasurableSet.disjointed (fun n => ?_) n
        exact measurableSet_toMeasurable _ _

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

Goal state before:
pp: α : Type u_1
p : Set α → Prop
s₀ : Set α
hp : p s₀
t : Set α
inst✝ : HasCountableSeparatingOn α p t
S : Set (Set α)
hSne : S.Nonempty
hSc : S.Countable
hS : (∀ s ∈ S, p s) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
⊢ ∃ S, (∀ (n : ℕ), p (S n)) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ (n : ℕ), x ∈ S n ↔ y ∈ S n) → x = y

Tactic:
rcases hSc.exists_eq_range hSne with ⟨S, rfl⟩

Goal state after:
α : Type u_1
p : Set α → Prop
s₀ : Set α
hp : p s₀
t : Set α
inst✝ : HasCountableSeparatingOn α p t
S : ℕ → Set α
hSne : (range S).Nonempty
hSc : (range S).Countable
hS : (∀ s ∈ range S, p s) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ s ∈ range S, x ∈ s ↔ y ∈ s) → x = y
⊢ ∃ S, (∀ (n : ℕ), p (S n)) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ (n : ℕ), x ∈ S n ↔ y ∈ S n) → x = y
Module: Mathlib.MeasureTheory.Measure.Restrict

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

Tactic:
exact piecewise_ae_eq_of_ae_eq_set hst

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

Goal state before:
pp: ι : 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
⊢ AEMeasurable f (sum μ)

Tactic:
have hsm : MeasurableSet (⋂ i, s i) :=
    MeasurableSet.iInter fun i => measurableSet_toMeasurable _ _

Goal state after:
ι : 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)
⊢ AEMeasurable f (sum μ)
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case inl
β : Type u_2
α : Type u_3
γ : Type u_4
inst✝¹ : MeasurableSpace γ
inst✝ : Nonempty β
h✝ : CountableOrCountablyGenerated (α × β) γ
h : Countable (α × β)
⊢ CountableOrCountablyGenerated α γ

Tactic:
have := countable_left_of_prod_of_nonempty h

Goal state after:
case inl
β : Type u_2
α : Type u_3
γ : Type u_4
inst✝¹ : MeasurableSpace γ
inst✝ : Nonempty β
h✝ : CountableOrCountablyGenerated (α × β) γ
h : Countable (α × β)
this : Countable α
⊢ CountableOrCountablyGenerated α γ
Module: Mathlib.Topology.Separation.GDelta

Goal state before:
pp: case inr
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)
⊢ HasSeparatingCover s t

Tactic:
have clg'_int : t = ⋂ i, closure (g' i) := by
    apply (subset_iInter fun n ↦ (clt_sub_g' n).trans subset_closure).antisymm
    rw [T_int]
    refine subset_sInter fun t tinT ↦ ?_
    obtain ⟨n, gn⟩ := g_surj ⟨t, tinT⟩
    refine iInter_subset_of_subset n <| (clg'_sub_g n).trans ?_
    rw [gn]

Goal state after:
case inr
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)
clg'_int : t = ⋂ i, closure[inst✝¹] (g' i)
⊢ HasSeparatingCover s t
Module: Mathlib.Topology.Separation.GDelta

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PerfectlyNormalSpace X
x y : X
hxy : x ⤳ y
⊢ ∀ (s : Set X), IsClosed[inst✝²] s → y ∈ s → x ∈ s

Tactic:
intro K hK hyK

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PerfectlyNormalSpace X
x y : X
hxy : x ⤳ y
K : Set X
hK : IsClosed[inst✝²] K
hyK : y ∈ K
⊢ x ∈ K
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case refine_1.inl.inl
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
a b : α
hb : a ⋖ b
⊢ MeasurableSet (Ioi a)

Tactic:
rw [hb.Ioi_eq, ← compl_Iio]
        exact (H _).compl

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 = ∅ → 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
l : α
hlt : l ∈ t
hly : l ≤ y
u : α
hut : u ∈ t
hyu : y < u
hua : u < a
⊢ ∃ i, ∃ (_ : i ∈ t), ∃ i_1, ∃ (_ : i_1 ∈ t) (_ : i < i_1) (_ : i_1 < a), i ≤ y ∧ y ≤ i_1

Tactic:
exact ⟨l, hlt, u, hut, hly.trans_lt hyu, hua, hly, hyu.le⟩

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

Goal state before:
pp: α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
δ : ℝ
⊢ closedBall x δ ⊆ cthickening δ {x}

Tactic:
by
  rcases lt_or_ge δ 0 with (hδ | hδ)
  · simp only [closedBall_eq_empty.mpr hδ, empty_subset]
  · simp only [cthickening_singleton x hδ, Subset.rfl]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
r : ℝ
hs : s.Nonempty
⊢ infDist x s < r ↔ ∃ y ∈ s, dist x y < r

Tactic:
by
  simp [← not_le, le_infDist hs]

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

Goal state before:
pp: case refine_2
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
inst✝ : NoMaxOrder α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) ≠ ∞
h : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) = ν (Ico a b)
s : Set α
hsc : s.Countable
hsd : Dense s
hsb : ∀ (x : α), IsBot x → x ∈ s
right✝ : ∀ (x : α), IsTop x → x ∈ s
this : {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i < i_2), x = Ico i i_2}.Countable
⊢ ⋃₀ {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i < i_2), x = Ico i i_2} = univ

Tactic:
refine sUnion_eq_univ_iff.2 fun x => ?_

Goal state after:
case refine_2
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
inst✝ : NoMaxOrder α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) ≠ ∞
h : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) = ν (Ico a b)
s : Set α
hsc : s.Countable
hsd : Dense s
hsb : ∀ (x : α), IsBot x → x ∈ s
right✝ : ∀ (x : α), IsTop x → x ∈ s
this : {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i < i_2), x = Ico i i_2}.Countable
x : α
⊢ ∃ b ∈ {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i < i_2), x = Ico i i_2}, x ∈ b
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case refine_2
α : Type u_5
inst✝⁴ : TopologicalSpace α
m : MeasurableSpace α
inst✝³ : SecondCountableTopology α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : BorelSpace α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a ≤ b → μ (Icc a b) ≠ ∞
h : ∀ ⦃a b : α⦄, a ≤ b → μ (Icc a b) = ν (Icc a b)
s : Set α
hsc : s.Countable
hsd : Dense s
hsb : ∀ (x : α), IsBot x → x ∈ s
hst : ∀ (x : α), IsTop x → x ∈ s
this : {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i ≤ i_2), x = Icc i i_2}.Countable
⊢ ⋃₀ {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i ≤ i_2), x = Icc i i_2} = univ

Tactic:
refine sUnion_eq_univ_iff.2 fun x => ?_

Goal state after:
case refine_2
α : Type u_5
inst✝⁴ : TopologicalSpace α
m : MeasurableSpace α
inst✝³ : SecondCountableTopology α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : BorelSpace α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a ≤ b → μ (Icc a b) ≠ ∞
h : ∀ ⦃a b : α⦄, a ≤ b → μ (Icc a b) = ν (Icc a b)
s : Set α
hsc : s.Countable
hsd : Dense s
hsb : ∀ (x : α), IsBot x → x ∈ s
hst : ∀ (x : α), IsTop x → x ∈ s
this : {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i ≤ i_2), x = Icc i i_2}.Countable
x : α
⊢ ∃ b ∈ {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i ≤ i_2), x = Icc i i_2}, x ∈ b
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case inl.inl
α : Type u_1
δ : Type u_4
inst✝⁵ : TopologicalSpace α
mα : MeasurableSpace α
inst✝⁴ : BorelSpace α
mδ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
inst✝ : Countable ι
f : ι → δ → α
g g' : δ → α
hf : ∀ (i : ι), Measurable (f i)
g'_meas : Measurable g'
hι : IsEmpty ι
hs : MeasurableSet ∅
hg : ∀ b ∈ ∅, IsLUB {a | ∃ i, f i b = a} (g b)
hg' : EqOn g g' ∅ᶜ
⊢ Measurable g

Tactic:
convert! g'_meas

Goal state after:
α : Type u_1
δ : Type u_4
inst✝⁵ : TopologicalSpace α
mα : MeasurableSpace α
inst✝⁴ : BorelSpace α
mδ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
inst✝ : Countable ι
f : ι → δ → α
g g' : δ → α
hf : ∀ (i : ι), Measurable (f i)
g'_meas : Measurable g'
hι : IsEmpty ι
hs : MeasurableSet ∅
hg : ∀ b ∈ ∅, IsLUB {a | ∃ i, f i b = a} (g b)
hg' : EqOn g g' ∅ᶜ
⊢ g = g'
Module: Mathlib.MeasureTheory.MeasurableSpace.Prod

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_3
γ : Type u_4
inst✝ : MeasurableSingletonClass α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
x : α
f : γ → β
hf : MeasurableEmbedding f
y y' : γ
⊢ (fun y ↦ (x, f y)) y = (fun y ↦ (x, f y)) y' → y = y'

Tactic:
simp only [Prod.mk.injEq, true_and]

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_3
γ : Type u_4
inst✝ : MeasurableSingletonClass α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
x : α
f : γ → β
hf : MeasurableEmbedding f
y y' : γ
⊢ f y = f y' → y = y'
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 α
ι : Sort u_5
inst✝ : Countable ι
f : ι → δ → α
g g' : δ → α
hf : ∀ (i : ι), Measurable (f i)
s : Set δ
hs : MeasurableSet s
hg : ∀ b ∈ s, IsLUB {a | ∃ i, f i b = a} (g b)
hg' : EqOn g g' sᶜ
g'_meas : Measurable g'
i✝ : ι
this : Nonempty ι
f' : ι → δ → α := fun i ↦ s.piecewise (f i) g'
b : δ
hb : b ∈ s
i : ι
⊢ f' i b = f i b

Tactic:
simp [f', hb]

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 α
ι : Sort u_5
inst✝ : Countable ι
f : ι → δ → α
g g' : δ → α
hf : ∀ (i : ι), Measurable (f i)
s : Set δ
hs : MeasurableSet s
hg : ∀ b ∈ s, IsLUB {a | ∃ i, f i b = a} (g b)
hg' : EqOn g g' sᶜ
g'_meas : Measurable g'
i✝ : ι
this : Nonempty ι
f' : ι → δ → α := fun i ↦ s.piecewise (f i) g'
b : δ
hb : b ∉ s
i : ι
⊢ f' i b = g' b

Tactic:
simp [f', hb]

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

Goal state before:
pp: case succ
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
a : α
n : ℕ
IH : ∑ k ∈ Finset.range (n + 1), ↑((eapproxDiff f k) a) = (eapprox f n) a
⊢ ∑ x ∈ Finset.range (n + 1), ↑((eapproxDiff f x) a) + ↑((eapproxDiff f (n + 1)) a) = (eapprox f (n + 1)) a

Tactic:
IH,

Goal state after:
case succ
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
a : α
n : ℕ
IH : ∑ k ∈ Finset.range (n + 1), ↑((eapproxDiff f k) a) = (eapprox f n) a
⊢ (eapprox f n) a + ↑((eapproxDiff f (n + 1)) a) = (eapprox f (n + 1)) a
Module: Mathlib.Topology.IndicatorConstPointwise

Goal state before:
pp: case mpr
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst✝¹ : DecidablePred p
q : Prop
inst✝ : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
h : ∀ᶠ (i : ι) in L, p i ↔ q
⊢ Tendsto (fun i ↦ if p i then a else b) L (if q then F else G)

Tactic:
· have obs : (fun _ ↦ if q then a else b) =ᶠ[L] (fun i ↦ if p i then a else b) := by
      filter_upwards [h] with i hi
      simp only [hi]
    apply Tendsto.congr' obs
    by_cases hq : q
    · simp only [hq, ite_true]
      apply le_trans _ haF
      simp
    · simp only [hq, ite_false]
      apply le_trans _ hbG
      simp only [principal_singleton, le_pure_iff, mem_map, Set.mem_singleton_iff,
        Set.preimage_const_of_mem, univ_mem]

Goal state after: