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

Goal state before:
pp: case hgf
R : Type u_4
inst✝⁵ : TopologicalSpace R
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x ↦ a + x⁻¹) atTop (𝓝 a)
x : R
hx : 1 ≤ x
⊢ a ≤ ↑⌈a * x⌉₊ / x

Tactic:
le_div_iff₀ (zero_lt_one.trans_le hx)

Goal state after:
case hgf
R : Type u_4
inst✝⁵ : TopologicalSpace R
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x ↦ a + x⁻¹) atTop (𝓝 a)
x : R
hx : 1 ≤ x
⊢ a * x ≤ ↑⌈a * x⌉₊
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case h.right
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ b ∈ T_t', f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ b, g b) (⋂ b ∈ T_t', f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ b ∈ T_s, f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ b, g b) (⋂ b ∈ T_s, f_s b)
h_nonempty : ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b).Nonempty
⊢ ∀ b ∈ T_s ∪ T_t',
    (if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅) ∈ g b

Tactic:
intro b h_b

Goal state after:
case h.right
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ b ∈ T_t', f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ b, g b) (⋂ b ∈ T_t', f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ b ∈ T_s, f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ b, g b) (⋂ b ∈ T_s, f_s b)
h_nonempty : ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b).Nonempty
b : β
h_b : b ∈ T_s ∪ T_t'
⊢ (if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅) ∈ g b
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 ∈ Finset.image (fun x ↦ ↑x) T, Function.extend (fun x ↦ ↑x) f (fun x ↦ ∅) b ∈ g b

Tactic:
intro b h_b

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 : b ∈ Finset.image (fun x ↦ ↑x) T
⊢ Function.extend (fun x ↦ ↑x) f (fun x ↦ ∅) b ∈ g b
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
⊢ piiUnionInter (fun i ↦ {s i}) S = {s' | ∃ t, ∃ (_ : ↑t ⊆ S), s' = ⋂ i ∈ t, s i}

Tactic:
ext1 s'

Goal state after:
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
s' : Set α
⊢ s' ∈ piiUnionInter (fun i ↦ {s i}) S ↔ s' ∈ {s' | ∃ t, ∃ (_ : ↑t ⊆ S), s' = ⋂ i ∈ t, s i}
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
h_nonempty : (t1 ∩ t2).Nonempty
g : ι → Set α := fun n ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
h_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i
n : ι
hn : n ∈ p1 ∪ p2
hn1 : n ∉ p1
h : n ∉ p2
⊢ n ∉ p1 ∪ p2

Tactic:
by simp [hn1, h]

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
d : DynkinSystem α
⊢ d.Has univ

Tactic:
by simpa using d.has_compl d.has_empty

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

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
h : t =ᵐ[μ] univ
⊢ s ∪ t =ᵐ[μ] univ

Tactic:
by
  convert! ae_eq_set_union (ae_eq_refl s) h
  rw [union_univ]

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
⊢ (𝓟 s).IsMeasurablyGenerated ↔ MeasurableSet s

Tactic:
refine ⟨?_, fun hs => ⟨fun t ht => ⟨s, mem_principal_self s, hs, ht⟩⟩⟩

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
⊢ (𝓟 s).IsMeasurablyGenerated → MeasurableSet s
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet (rangeFactorization f '' s)

Tactic:
← (subtype_coe hf.measurableSet_range).measurableSet_image,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet (Subtype.val '' rangeFactorization f '' s)
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α✝
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace β✝
inst✝³ : MeasurableSpace γ✝
α : Type ?u.23
β : Type ?u.25
γ : Type ?u.102
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
⊢ univ ⊆ range Sum.inl ×ˢ univ ∪ range Sum.inr ×ˢ univ

Tactic:
by rintro ⟨a | b, c⟩ <;> simp [Set.prod_eq]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
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
⊢ (A : Set α) ×' MeasurableSet A ∧ F A = A

Tactic:
let X : ℕ → Set α := fun n => F^[n] univ

Goal state after:
α : 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
⊢ (A : Set α) ×' MeasurableSet A ∧ F A = A
Module: Mathlib.MeasureTheory.Measure.NullMeasurable

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hd : AEDisjoint μ s t
⊢ μ (s ∪ t) = μ s + μ t

Tactic:
rw [union_eq_iUnion, measure_iUnion₀, tsum_fintype, Fintype.sum_bool, cond, cond]
  exacts [pairwise_on_bool.mpr hd, fun b ↦ Bool.casesOn b ht hs]

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν : Measure α
h : μ₁ + μ₂ ≪ ν
s : Set α
hs0 : ν s = 0
⊢ μ₁ s = 0 ∧ μ₂ s = 0

Tactic:
simpa using h hs0

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

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

Tactic:
measure_union_add_inter t hs,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
⊢ μ t + μ s = μ s + μ t
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 m)

Tactic:
change SFinite (Measure.sum (fun i ↦ m i))
  simp_rw [← sum_sfiniteSeq (m _), Measure.sum_sum]
  apply sfinite_sum_of_countable

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝ : IsFiniteMeasure μ
hs : MeasurableSet s
ht : MeasurableSet t
ε : ℝ≥0∞
h : μ s ≤ μ t + ε
⊢ μ tᶜ ≤ μ sᶜ + ε

Tactic:
rw [measure_compl ht (by finiteness), measure_compl hs (by finiteness), tsub_le_iff_right]
  calc
    μ univ = μ univ - μ s + μ s := (tsub_add_cancel_of_le <| measure_mono s.subset_univ).symm
    _ ≤ μ univ - μ s + (μ t + ε) := by gcongr
    _ = _ := by rw [add_right_comm, add_assoc]

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
C : Set (Set α)
hC : IsCountablySpanning C
hm : ∀ t ∈ C, MeasurableSet t
ht : ∀ t ∈ C, (μ.restrict t) s = 0
⊢ μ s = 0

Tactic:
rw [← forall_measure_inter_isCountablySpanning_eq_zero hC]
  intro t htc
  simpa [← μ.restrict_apply' (hm _ htc)] using ht t htc

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

Goal state before:
pp: α : Type u_2
t : Set α
m0 : MeasurableSpace α
m : Set (Measure α)
hm : m.Nonempty
ht : MeasurableSet t
s : Set α
hs : MeasurableSet s
⊢ (sInf (toOuterMeasure '' m)) (s ∩ t) = ((OuterMeasure.restrict t) (sInf (toOuterMeasure '' m))) s

Tactic:
OuterMeasure.restrict_apply

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

Goal state before:
pp: α : Type u_2
t : Set α
m0 : MeasurableSpace α
m : Set (Measure α)
hm : m.Nonempty
ht : MeasurableSet t
⊢ (sInf m).restrict t = sInf ((fun μ ↦ μ.restrict t) '' m)

Tactic:
by
  ext1 s hs
  simp_rw [sInf_apply hs, restrict_apply hs, sInf_apply (MeasurableSet.inter hs ht),
    Set.image_image, restrict_toOuterMeasure_eq_toOuterMeasure_restrict ht, ←
    Set.image_image _ toOuterMeasure, ← OuterMeasure.restrict_sInf_eq_sInf_restrict _ (hm.image _),
    OuterMeasure.restrict_apply]

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

Goal state before:
pp: α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable ι
s : ι → Set α
hs : ⋃ i, s i = univ
⊢ μ = ν ↔ μ.restrict univ = ν.restrict univ

Tactic:
restrict_univ,

Goal state after:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable ι
s : ι → Set α
hs : ⋃ i, s i = univ
⊢ μ = ν ↔ μ = ν.restrict univ
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
S : Set ι
s : ι → Set α
hc : S.Countable
hs : ⋃ i ∈ S, s i = univ
⊢ μ = ν ↔ μ.restrict univ = ν.restrict univ

Tactic:
restrict_univ,

Goal state after:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
S : Set ι
s : ι → Set α
hc : S.Countable
hs : ⋃ i ∈ S, s i = univ
⊢ μ = ν ↔ μ = ν.restrict univ
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
t : Set α
ht : t ∈ measurableAtom '' s
⊢ ∀ ⦃y : Set α⦄, y ∈ measurableAtom '' s → t ≠ y → Disjoint t y

Tactic:
t'

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
t : Set α
ht : t ∈ measurableAtom '' s
t' : Set α
⊢ t' ∈ measurableAtom '' s → t ≠ t' → Disjoint t t'
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: case e_f
α : 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 : ℕ
⊢ MeasurableSet (disjointed w n)

Tactic:
refine MeasurableSet.disjointed (fun n => ?_) n

Goal state after:
case e_f
α : 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✝ n : ℕ
⊢ MeasurableSet (w n)
Module: Mathlib.Order.Filter.CountableSeparatingOn

Goal state before:
pp: α : Type u_1
l : Filter α
inst✝ : CountableInterFilter l
p : Set α → Prop
s : Set α
h : HasCountableSeparatingOn α p s
hs : s ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
S : Set (Set α)
hSc : S.Countable
hSp : ∀ s ∈ S, p s
hS : ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
⊢ ∃ t ⊆ s, t.Subsingleton ∧ t ∈ l

Tactic:
refine ⟨s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ (U ∈ S) (_ : Uᶜ ∈ l), Uᶜ, ?_, ?_, ?_⟩

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

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

case refine_3
α : Type u_1
l : Filter α
inst✝ : CountableInterFilter l
p : Set α → Prop
s : Set α
h : HasCountableSeparatingOn α p s
hs : s ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
S : Set (Set α)
hSc : S.Countable
hSp : ∀ s ∈ S, p s
hS : ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
⊢ s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ U ∈ S, ⋂ (_ : Uᶜ ∈ l), Uᶜ ∈ l
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: case refine_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set α
h : NullMeasurableSet t (μ.restrict s)
⊢ NullMeasurableSet (t ∩ s) μ

Tactic:
obtain ⟨t', -, ht', t't⟩ : ∃ t' ⊇ t, MeasurableSet t' ∧ t' =ᵐ[μ.restrict s] t :=
      h.exists_measurable_superset_ae_eq

Goal state after:
case refine_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set α
h : NullMeasurableSet t (μ.restrict s)
t' : Set α
ht' : MeasurableSet t'
t't : t' =ᵐ[μ.restrict s] t
⊢ NullMeasurableSet (t ∩ s) μ
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'
t : Set α := ⋃ n ∈ {k | μ (t' k) ≤ ν (t' k)}, t' n
ht : t = ⋃ n ∈ {k | μ (t' k) ≤ ν (t' k)}, t' n
⊢ sInf {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)} ≤ ∑' (n : ℕ), min (μ (t' n)) (ν (t' n))

Tactic:
suffices hadd : μ (t ∩ s) + ν (tᶜ ∩ s) ≤ ∑' n, μ (t' n) ⊓ ν (t' n) by
      exact le_trans (sInf_le ⟨t, rfl⟩) hadd

Goal state after:
case 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
⊢ μ (t ∩ s) + ν (tᶜ ∩ s) ≤ ∑' (n : ℕ), min (μ (t' n)) (ν (t' n))
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
hs : s ∈ memPartition t n
⊢ MeasurableSet s

Tactic:
rw [← sdiff_union_inter s (t n)]
  refine MeasurableSet.union ?_ ?_ <;>
    · refine measurableSet_generateFrom ?_
      rw [memPartition_succ]
      exact ⟨s, hs, by simp⟩

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:
OuterMeasure.top_caratheodory

Goal state after:
α : 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 ≤ ⊤
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: case refine_2
α : 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 s : Set α
hs : s ∈ μ.cofinite
⊢ (toMeasurable μ sᶜ)ᶜ ⊆ s

Tactic:
compl_subset_comm

Goal state after:
case refine_2
α : 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 s : Set α
hs : s ∈ μ.cofinite
⊢ sᶜ ⊆ toMeasurable μ sᶜ
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

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

pp: case refine_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ ∀ t ∈ range Iio, MeasurableSet t

Tactic:
· 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

Goal state after:
case refine_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ ∀ t ∈ range Iio, MeasurableSet t
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
hs : s.Nonempty
ht : t.Nonempty
⊢ hausdorffEDist s t ≤ ediam (s ∪ t)

Tactic:
rcases hs with ⟨x, xs⟩

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
ht : t.Nonempty
x : α
xs : x ∈ s
⊢ hausdorffEDist s t ≤ ediam (s ∪ t)
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
ε : ℝ≥0
x y : α
hy : infEDist y s ≤ ↑ε
δ : ℝ≥0
hδ : 0 < δ
x✝ : ediam s + 2 * ↑ε < ∞
hε : ↑ε < ↑ε + ↑δ
hx : infEDist x s < ↑ε + ↑δ
x' : α
hx' : x' ∈ s
hxx' : edist x x' < ↑ε + ↑δ
⊢ ↑ε + ↑δ + (↑ε + ediam s) = ediam s + 2 * ↑ε + ↑δ

Tactic:
rw [two_mul]; ac_rfl

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
⊢ infDist x (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s) = infDist x s

Tactic:
simp [infDist, infEDist_closure]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
hs : s.Nonempty
bs : Bornology.IsBounded s
ht : t.Nonempty
bt : Bornology.IsBounded t
⊢ hausdorffDist s t ≤ diam (s ∪ t)

Tactic:
rcases hs with ⟨x, xs⟩

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
ht : t.Nonempty
bt : Bornology.IsBounded t
x : α
xs : x ∈ s
⊢ hausdorffDist s t ≤ diam (s ∪ t)
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : OpensMeasurableSpace α
mδ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : SecondCountableTopology α
inst✝ : OrderClosedTopology α
f g : δ → α
hf : Measurable f
hg : Measurable g
⊢ Measurable fun a ↦ Max.max (f a) (g a)

Tactic:
simpa only [max_def'] using! hf.piecewise (measurableSet_le hg hf) hg

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Zero β
r : β
s : Set α
f : α →ₛ β
hr : r ∈ (f.restrict s).range
h0 : r ≠ 0
hs : ¬MeasurableSet s
⊢ r ∈ ⇑f '' s

Tactic:
by
    rw [restrict_of_not_measurable hs] at hr
    exact (h0 <| eq_zero_of_mem_range_zero hr).elim

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

Goal state before:
pp: case h₂
α : 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 : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hα : Nonempty α
A : ∀ (i : ι) (c : α), MeasurableSet {x | f i x ≤ c}
B : ∀ (c : α), MeasurableSet {x | ∀ (i : ι), f i x ≤ c}
u : ℕ → α
hu : Tendsto u atTop atTop
x : δ
n : ℕ
hn : ∀ (i : ι), f i x ≤ u n
⊢ x ∈ {b | BddAbove (range fun i ↦ f i b)}

Tactic:
refine ⟨u n, ?_⟩

Goal state after:
case h₂
α : 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 : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hα : Nonempty α
A : ∀ (i : ι) (c : α), MeasurableSet {x | f i x ≤ c}
B : ∀ (c : α), MeasurableSet {x | ∀ (i : ι), f i x ≤ c}
u : ℕ → α
hu : Tendsto u atTop atTop
x : δ
n : ℕ
hn : ∀ (i : ι), f i x ≤ u n
⊢ u n ∈ upperBounds (range fun i ↦ f i x)
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ (f.restrict s).lintegral μ = f.lintegral (μ.restrict s)

Tactic:
f.restrict_lintegral hs,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ ∑ r ∈ f.range, r * μ (⇑f ⁻¹' {r} ∩ s) = f.lintegral (μ.restrict s)
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : Zero β
μ : Measure α
f : α →ₛ β
H : ∀ (y : β), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ∞
⊢ f.FinMeasSupp μ

Tactic:
rw [finMeasSupp_iff_support, support_eq]

Goal state after:
case mpr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : Zero β
μ : Measure α
f : α →ₛ β
H : ∀ (y : β), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ∞
⊢ μ (⋃ y ∈ {y ∈ f.range | y ≠ 0}, ⇑f ⁻¹' {y}) < ∞
Module: Mathlib.MeasureTheory.Function.SimpleFuncDense

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : PseudoEMetricSpace α
inst✝⁴ : OpensMeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : Zero α
inst✝¹ : Preorder α
f : β → α
hf : 0 ≤ f
hfm : Measurable f
inst✝ : SeparableSpace ↑(range f ∪ {0})
n : ℕ
⊢ 0 ≤ approxOn f hfm (range f ∪ {0}) 0 ⋯ n

Tactic:
have : range f ∪ {0} ⊆ Set.Ici 0 := by
    simp only [Set.union_singleton, Set.insert_subset_iff, Set.mem_Ici, le_refl, true_and]
    rintro - ⟨x, rfl⟩
    exact hf x
  exact fun _ ↦ this <| approxOn_mem ..

Goal state after: