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

Goal state before:
pp: case zero
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → α
hf : QuasiMeasurePreserving f μ μ
hs : f ⁻¹' s =ᵐ[μ] s
⊢ f^[0] ⁻¹' s =ᵐ[μ] s

Tactic:
rfl

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

Goal state before:
pp: X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
b : X
hsne : s.Nonempty
this : Nonempty ↑s
hsub : ¬s ⊆ Iio b
h : Tendsto Subtype.val atTop (𝓝[<] b)
a : X
has : a ∈ s
ha : a ∉ Iio b
c : X
hcs : c ∈ s
hcb : ↑⟨c, hcs⟩ ∈ Iio b
hac : ⟨a, has⟩ ≤ ⟨c, hcs⟩
⊢ a ≤ c

Tactic:
by simpa using hac

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

Goal state before:
pp: X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a b : X
α : Type u_2
l : Filter α
f : X → α
h : a < b
hb : IsSuccPrelimit b
⊢ Tendsto (fun x ↦ f ↑x) atTop l ↔ Tendsto (f ∘ Subtype.val) atTop l

Tactic:
Function.comp_def

Goal state after:
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a b : X
α : Type u_2
l : Filter α
f : X → α
h : a < b
hb : IsSuccPrelimit b
⊢ Tendsto (fun x ↦ f ↑x) atTop l ↔ Tendsto (fun x ↦ f ↑x) atTop l
Module: Mathlib.Topology.Order.AtTopBotIxx

Goal state before:
pp: X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a b : X
α : Type u_2
l : Filter α
f : X → α
h : a < b
ha : IsPredPrelimit a
⊢ Tendsto (fun x ↦ f ↑x) atBot l ↔ Tendsto (f ∘ Subtype.val) atBot l

Tactic:
Function.comp_def

Goal state after:
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a b : X
α : Type u_2
l : Filter α
f : X → α
h : a < b
ha : IsPredPrelimit a
⊢ Tendsto (fun x ↦ f ↑x) atBot l ↔ Tendsto (fun x ↦ f ↑x) atBot l
Module: Mathlib.Topology.Order.AtTopBotIxx

Goal state before:
pp: X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
α : Type u_2
l : Filter α
f : X → α
ha : IsPredPrelimit a
⊢ Tendsto (fun x ↦ f ↑x) atBot l ↔ Tendsto (f ∘ Subtype.val) atBot l

Tactic:
Function.comp_def

Goal state after:
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
α : Type u_2
l : Filter α
f : X → α
ha : IsPredPrelimit a
⊢ Tendsto (fun x ↦ f ↑x) atBot l ↔ Tendsto (fun x ↦ f ↑x) atBot l
Module: Mathlib.Topology.Order.AtTopBotIxx

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

Tactic:
Function.comp_def

Goal state after:
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
α : Type u_2
l : Filter α
f : X → α
ha : IsSuccPrelimit a
⊢ Tendsto (fun x ↦ f ↑x) atTop l ↔ Tendsto (fun x ↦ f ↑x) atTop l
Module: Mathlib.Topology.Order.AtTopBotIxx

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

Tactic:
Function.comp_def

Goal state after:
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a b : X
α : Type u_2
l : Filter α
f : α → ↑(Ioo a b)
hb : IsSuccPrelimit b
⊢ Tendsto (fun x ↦ ↑(f x)) l (𝓝[<] b) ↔ Tendsto (fun x ↦ ↑(f x)) l (𝓝[<] b)
Module: Mathlib.Topology.Order.AtTopBotIxx

Goal state before:
pp: X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a b : X
α : Type u_2
l : Filter α
f : α → ↑(Ioo a b)
ha : IsPredPrelimit a
⊢ Tendsto (Subtype.val ∘ f) l (𝓝[>] a) ↔ Tendsto (fun x ↦ ↑(f x)) l (𝓝[>] a)

Tactic:
Function.comp_def

Goal state after:
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a b : X
α : Type u_2
l : Filter α
f : α → ↑(Ioo a b)
ha : IsPredPrelimit a
⊢ Tendsto (fun x ↦ ↑(f x)) l (𝓝[>] a) ↔ Tendsto (fun x ↦ ↑(f x)) l (𝓝[>] a)
Module: Mathlib.Topology.Order.AtTopBotIxx

Goal state before:
pp: X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
α : Type u_2
l : Filter α
f : α → ↑(Ioi a)
ha : IsPredPrelimit a
⊢ Tendsto (Subtype.val ∘ f) l (𝓝[>] a) ↔ Tendsto (fun x ↦ ↑(f x)) l (𝓝[>] a)

Tactic:
Function.comp_def

Goal state after:
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
α : Type u_2
l : Filter α
f : α → ↑(Ioi a)
ha : IsPredPrelimit a
⊢ Tendsto (fun x ↦ ↑(f x)) l (𝓝[>] a) ↔ Tendsto (fun x ↦ ↑(f x)) l (𝓝[>] a)
Module: Mathlib.Topology.Order.AtTopBotIxx

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

Tactic:
Function.comp_def

Goal state after:
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
α : Type u_2
l : Filter α
f : α → ↑(Iio a)
ha : IsSuccPrelimit a
⊢ Tendsto (fun x ↦ ↑(f x)) l (𝓝[<] a) ↔ Tendsto (fun x ↦ ↑(f x)) l (𝓝[<] a)
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 : ℕ
⊢ {i | as n ≤ μ (As i)} = (fun i ↦ μ (As i)) ⁻¹' Ici (as n)

Tactic:
rfl

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

Goal state before:
pp: case e_6
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : μ s ≠ ∞
ht : MeasurableSet t
hst : s ⊆ t
u : Set α
hu : MeasurableSet u
⊢ s ∩ (t ∩ u) = u ∩ s

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsCodirectedOrder ι
inst✝ : atBot.IsCountablyGenerated
s : ι → Set α
hs : ∀ᵐ (ω : α) ∂μ, Monotone fun x ↦ ω ∈ s x
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
i : ι
hi : μ (s i) ≠ ∞
this : Nonempty ι
t : ι → Set α := fun i ↦ s i ∩ {ω | Monotone fun x ↦ ω ∈ s x}
hst : ∀ (i : ι), s i =ᵐ[μ] t i
hMono : Monotone t
⊢ ⋂ i, s i =ᵐ[μ] ⋂ i, s i

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
γ : Type u_5
f g : α → γ
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hs_zero : μ s = 0
⊢ (fun x ↦ if x ∈ s then f x else g x) =ᵐ[μ] g

Tactic:
by
  have h_ss : sᶜ ⊆ { a : α | ite (a ∈ s) (f a) (g a) = g a } := fun x hx => by
    simp [(Set.mem_compl_iff _ _).mp hx]
  refine measure_mono_null ?_ hs_zero
  conv_rhs => rw [← compl_compl s]
  rwa [Set.compl_subset_compl]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
γ : Type u_5
f g : α → γ
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hs_zero : s ∈ ae μ
a✝¹ : α
a✝ : a✝¹ ∈ s
⊢ f a✝¹ = f a✝¹

Tactic:
rfl

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

Goal state before:
pp: case hfin
α : Type u_8
ι : Type u_9
x✝ : MeasurableSpace α
μ : Measure α
inst✝² : Countable ι
inst✝¹ : Preorder ι
inst✝ : IsDirectedOrder ι
f : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (f i) μ
hfin : ∃ i, μ (f i) ≠ ∞
k : ι
hk : μ (f k) ≠ ∞
⊢ k ≤ k

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
m : ℝ≥0∞ := ⨆ D ∈ {D | D ⊆ C ∧ D.Countable}, μ (⋃₀ D)
hm : ⊥ < m
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 m
u_lim : Tendsto u atTop (𝓝 m)
D : ℕ → Set (Set α)
D_mem : ∀ (n : ℕ), D n ∈ {D | D ⊆ C ∧ D.Countable}
huD : ∀ (n : ℕ), u n < μ (⋃₀ D n)
⊢ (∀ (i : ℕ), D i ⊆ C) ∧ ∀ (i : ℕ), (D i).Countable

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
m : ℝ≥0∞ := ⨆ D ∈ {D | D ⊆ C ∧ D.Countable}, μ (⋃₀ D)
hm : ⊥ < m
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 m
u_lim : Tendsto u atTop (𝓝 m)
D : ℕ → Set (Set α)
D_mem : ∀ (n : ℕ), D n ∈ {D | D ⊆ C ∧ D.Countable}
huD : ∀ (n : ℕ), u n < μ (⋃₀ D n)
hD : ⋃ n, D n ∈ {D | D ⊆ C ∧ D.Countable}
n : ℕ
x : α
hx : ∃ t ∈ D n, x ∈ t
⊢ ∃ t, (∃ i, t ∈ D i) ∧ x ∈ t

Tactic:
grind

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

Goal state before:
pp: α : Type u_5
m₀ : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hμν : ∀ s ∈ C, μ s = ν s
m : MeasurableSpace α
h : m ≤ m₀
hA : m = generateFrom C
hC : IsPiSystem C
h_univ : μ univ = ν univ
s : Set α
hs : MeasurableSet s
⊢ μ univ < ∞

Tactic:
apply IsFiniteMeasure.measure_univ_lt_top

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
m : ℝ≥0∞ := ⨆ D ∈ {D | D ⊆ C ∧ D.Countable}, μ (⋃₀ D)
D : Set (Set α)
D_mem : D ∈ {D | D ⊆ C ∧ D.Countable}
hD : μ (⋃₀ D) = m
⊢ D ⊆ C

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
m : ℝ≥0∞ := ⨆ D ∈ {D | D ⊆ C ∧ D.Countable}, μ (⋃₀ D)
D : Set (Set α)
D_mem : D ∈ {D | D ⊆ C ∧ D.Countable}
hD : μ (⋃₀ D) = m
⊢ D.Countable

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
m : ℝ≥0∞ := ⨆ D ∈ {D | D ⊆ C ∧ D.Countable}, μ (⋃₀ D)
D : Set (Set α)
D_mem : D ∈ {D | D ⊆ C ∧ D.Countable}
hD : μ (⋃₀ D) = m
s : Set α
hs : s ∈ C
⊢ ∀ t ∈ D, MeasurableSet t

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
D : ℕ → Set (Set α)
DC : ∀ (n : ℕ), D n ⊆ C
D_count : ∀ (n : ℕ), (D n).Countable
hD : ∀ (n : ℕ), ∀ s ∈ C, s ≤ᵐ[sfiniteSeq μ n] ⋃₀ D n
s : Set α
hs : s ∈ C
n : ℕ
x : α
hx : ∃ t ∈ D n, x ∈ t
⊢ ∃ t, (∃ i, t ∈ D i) ∧ x ∈ t

Tactic:
grind

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
A : ∃ t' ⊇ t, MeasurableSet t' ∧ ∀ (u : Set α), MeasurableSet u → μ (t' ∩ u) = μ (t ∩ u)
⊢ μ (toMeasurable μ t ∩ s) = μ (t ∩ s)

Tactic:
toMeasurable

Goal state after:
α : 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)
⊢ μ
      ((if h : ∃ t_1 ⊇ t, MeasurableSet t_1 ∧ t_1 =ᵐ[μ] t then h.choose
        else
          if h' : ∃ t_1 ⊇ t, MeasurableSet t_1 ∧ ∀ (u : Set α), MeasurableSet u → μ (t_1 ∩ u) = μ (t ∩ u) then h'.choose
          else ⋯.choose) ∩
        s) =
    μ (t ∩ s)
Module: Mathlib.MeasureTheory.Measure.Trim

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : Measurable f
p : β → Prop
hp : MeasurableSet {x | p x}
⊢ (∀ᵐ (y : β) ∂Measure.map f μ, p y) ↔ ∀ᵐ (x : α) ∂μ.trim ⋯, p (f x)

Tactic:
rw [← map_trim_comap hf, ae_map_iff (Measurable.of_comap_le le_rfl).aemeasurable hp]

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

Goal state before:
pp: α : Type u_1
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m
inst✝ : SigmaFinite (μ.trim ⋯)
⊢ SigmaFinite (μ.trim hm)

Tactic:
have : SigmaFinite ((μ.trim hm).trim hm₂) := by simpa [trim_trim]

Goal state after:
α : Type u_1
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m
inst✝ : SigmaFinite (μ.trim ⋯)
this : SigmaFinite ((μ.trim hm).trim hm₂)
⊢ SigmaFinite (μ.trim hm)
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
⊢ μ (tᶜ ∩ s) = 0 ↔ μ {a | a ∉ t ∧ a ∈ s} = 0

Tactic:
rfl

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) ≠ ∞
A : ∃ t' ⊇ t, MeasurableSet t' ∧ ∀ (u : Set α), MeasurableSet u → μ (t' ∩ u) = μ (t ∩ u)
⊢ μ (toMeasurable μ t ∩ s) = μ (t ∩ s)

Tactic:
toMeasurable

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) ≠ ∞
A : ∃ t' ⊇ t, MeasurableSet t' ∧ ∀ (u : Set α), MeasurableSet u → μ (t' ∩ u) = μ (t ∩ u)
⊢ μ
      ((if h : ∃ t_1 ⊇ t, MeasurableSet t_1 ∧ t_1 =ᵐ[μ] t then h.choose
        else
          if h' : ∃ t_1 ⊇ t, MeasurableSet t_1 ∧ ∀ (u : Set α), MeasurableSet u → μ (t_1 ∩ u) = μ (t ∩ u) then h'.choose
          else ⋯.choose) ∩
        s) =
    μ (t ∩ s)
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
b : Set (Set β)
hbc : b.Countable
this : MeasurableSpace α := generateFrom (preimage f '' b)
⊢ CountablyGenerated α

Tactic:
exact ⟨_, hbc.image _, rfl⟩

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
p q : ℕ → Prop
hpq : p ≠ q
s : Set α
hsp : s ⊆ countablyGeneratedAtom α p
hsq : s ⊆ countablyGeneratedAtom α q
x : α
hxs : x ∈ s
⊢ ∃ n, p n ≠ q n

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
p q : ℕ → Prop
hpq : p ≠ q
s : Set α
x : α
hxs : x ∈ s
n : ℕ
hn : p n ≠ q n
hsp : ∀ (i : ℕ), x ∈ if p i then natGeneratingSequence α i else (natGeneratingSequence α i)ᶜ
hsq : ∀ (i : ℕ), x ∈ if q i then natGeneratingSequence α i else (natGeneratingSequence α i)ᶜ
⊢ False

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
x : α
⊢ ∀ (i : ℕ),
    x ∈ if (fun n ↦ x ∈ natGeneratingSequence α n) i then natGeneratingSequence α i else (natGeneratingSequence α i)ᶜ

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
x : α
⊢ ∀ (i : ℕ), x ∈ if x ∈ natGeneratingSequence α i then natGeneratingSequence α i else (natGeneratingSequence α i)ᶜ

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
n : ℕ
x✝ : MeasurableSet (natGeneratingSequence α n)
x : α
hx : x ∈ natGeneratingSequence α n
⊢ x ∈ natGeneratingSequence α n ∧
    ∀ (i : ℕ), x ∈ if x ∈ natGeneratingSequence α i then natGeneratingSequence α i else (natGeneratingSequence α i)ᶜ

Tactic:
grind

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

Goal state before:
pp: case e_6
α : Type u_2
β : Type u_3
x✝¹ : MeasurableSpace α
x✝ : MeasurableSpace β
f : α → β
g : β → α
μ : Measure α
hf : Measurable f
hg : MeasurableEmbedding g
hμg : ∀ᵐ (a : α) ∂μ, a ∈ range g
hfg : ∀ (a : β), f (g a) = a
s : Set β
hs : MeasurableSet s
⊢ f ⁻¹' s ∩ {x | ∃ y, g y = x} = g '' s

Tactic:
grind

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

Goal state before:
pp: α : 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 : α
p : ℕ → Prop
hpq : ¬q p
hpx : x ∈ countablyGeneratedAtom α p
p' : ℕ → Prop
hqp' : q p'
hx_mem : x ∈ countablyGeneratedAtom α p'
⊢ p ≠ p'

Tactic:
grind

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

Goal state before:
pp: 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 : α
p : ℕ → Prop
hpq : ¬q p
hpx : x ∈ countablyGeneratedAtom α p
p' : ℕ → Prop
hqp' : q p'
hx_mem : x ∈ countablyGeneratedAtom α p'
hpp' : p ≠ p'
h_disj : Disjoint (countablyGeneratedAtom α p) (countablyGeneratedAtom α p')
⊢ False

Tactic:
grind

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

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

Tactic:
grind

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

Goal state before:
pp: case refine_3
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
x : α
A : ℕ → Set α := natGeneratingSequence α
hA : ∀ (n : ℕ), MeasurableSet (A n)
hA_gen : generateFrom (range A) = mα
s : Set α
hs : MeasurableSet s
q : (ℕ → Prop) → Prop
hq : s = ⋃ p, if q p then countablyGeneratedAtom α p else ∅
p : ℕ → Prop
hpq : q p
hpx : x ∈ countablyGeneratedAtom α p
hp : p ≠ fun x_1 ↦ x ∈ A x_1
h_disj : Disjoint (countablyGeneratedAtom α p) (countablyGeneratedAtom α fun x_1 ↦ x ∈ A x_1)
hx_mem : x ∈ countablyGeneratedAtom α fun x_1 ↦ x ∈ A x_1
⊢ False

Tactic:
grind

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

Goal state before:
pp: case refine_1.compl.refine_2.refine_1
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
S : Finset (Set α)
hS_subset : ↑S ⊆ memPartition t n
ht✝ : MeasurableSet (⋃₀ ↑S)
⊢ Disjoint (⋃₀ (memPartition t n \ ↑S)) (⋃₀ ↑S)

pp: case refine_1.compl.refine_2.refine_2
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
S : Finset (Set α)
hS_subset : ↑S ⊆ memPartition t n
ht✝ : MeasurableSet (⋃₀ ↑S)
⊢ Codisjoint (⋃₀ (memPartition t n \ ↑S)) (⋃₀ ↑S)

Tactic:
· refine Set.disjoint_sUnion_right.mpr fun u huS => ?_
          refine Set.disjoint_sUnion_left.mpr fun v huV => ?_
          refine disjoint_memPartition t n (mem_of_mem_sdiff huV) (hS_subset huS) ?_
          exact ne_of_mem_of_not_mem huS (notMem_of_mem_sdiff huV) |>.symm

Goal state after:
case refine_1.compl.refine_2.refine_2
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
S : Finset (Set α)
hS_subset : ↑S ⊆ memPartition t n
ht✝ : MeasurableSet (⋃₀ ↑S)
⊢ Codisjoint (⋃₀ (memPartition t n \ ↑S)) (⋃₀ ↑S)
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ ν : Measure α
⊢ AEMeasurable f (bif true then μ else ν) ∧ AEMeasurable f (bif false then μ else ν) ↔
    AEMeasurable f μ ∧ AEMeasurable f ν

Tactic:
rfl

Goal state after:
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
⊢ Disjoint {k | μ (t' k) ≤ ν (t' k)} {k | ν (t' k) < μ (t' k)}

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

Goal state before:
pp: α : Type u_2
ι : Type u_6
x✝ : MeasurableSpace α
μ : Measure α
s : ι → Set α
M : ℕ
hs_meas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (y : α), {i | y ∈ s i}.encard ≤ ↑M
t : Set α
ht : MeasurableSet t
F : Finset ι
P : Finset ι → Set α := fun C ↦ (⋂ i ∈ C, s i) ∩ ⋂ i ∈ F \ C, (s i)ᶜ
Cs : Finset (Finset ι) := F.powerset \ {∅}
G : ι → Set (Finset ι) := fun i ↦ {C | C ∈ F.powerset ∧ i ∈ C}
P_meas : ∀ (C : Finset ι), MeasurableSet (P C)
P_cover : ∀ {i : ι}, i ∈ F → s i ⊆ ⋃ C ∈ G i, P C
iUnion_P : ⋃ C ∈ Cs, P C ⊆ ⋃ i, s i
P_subset_s : ∀ {i : ι} {C : Finset ι}, i ∈ C → P C ⊆ s i
mem_C : ∀ {i : ι}, i ∈ F → ∀ {C : Finset ι} {x : α}, x ∈ P C → x ∈ s i → i ∈ C
C_subset_C : ∀ {C₁ C₂ : Finset ι}, C₁ ∈ Cs → ∀ {x : α}, x ∈ P C₁ ∩ P C₂ → C₁ ⊆ C₂
⊢ ∑ x ∈ Cs, ↑(#(F ∩ x)) * (μ.restrict (P x)) t = ∑ x ∈ Cs, ↑(#({a ∈ F | a ∈ x})) * (μ.restrict (P x)) t

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
E : Type u_8
inst✝ : Zero E
μ : Measure α
f : α → E
⊢ μ (support f) = 0 ↔ f =ᵐ[μ] 0

Tactic:
rfl

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

Goal state before:
pp: α' : Type u_6
inst✝¹ : TopologicalSpace α'
inst✝ : MeasurableSpace α'
μ : Measure α'
s s' : Set α'
h : μ (frontier s) = 0
h' : μ (frontier s') = 0
⊢ frontier s ∩ closure[inst✝¹] s' ∪ closure[inst✝¹] s ∩ frontier s' ⊆ frontier s ∪ frontier s'

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
γ : Type u_3
inst✝⁶ : TopologicalSpace α
inst✝⁵ : MeasurableSpace α
inst✝⁴ : OpensMeasurableSpace α
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
inst✝ : MeasurableSingletonClass α
f : α → γ
hf : {x | ¬ContinuousAt f x}.Countable
this : ContinuousOn f {x | ContinuousAt f x}
⊢ {x | ContinuousAt f x}ᶜ = {x | ¬ContinuousAt f x}

Tactic:
grind

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ thickening δ E ⊆ cthickening δ E

Tactic:
by
  intro x hx
  rw [thickening, mem_ofPred_eq] at hx
  exact hx.le

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

Goal state before:
pp: α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ {S | ∃ l u, l < u ∧ Ioc l u = S} ⊆ {S | ∃ l u, l ≤ u ∧ Ioc l u = S}

Tactic:
grind

Goal state after: