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

Goal state before:
pp: α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
t : Finset (Set α)
t_ne : t.Nonempty
ht : ∀ s ∈ t, s ∈ S
h' : (⋂ s ∈ t, s).Nonempty
⊢ ⋂ s ∈ t, s ∈ S

Tactic:
by
  induction t_ne using Finset.Nonempty.cons_induction with
  | singleton a => simpa using ht
  | cons a t hat t_ne ih =>
    simp only [Finset.cons_eq_insert, Finset.mem_insert, iInter_iInter_eq_or_left] at h' ht ⊢
    refine h_pi _ (ht a (Or.inl rfl)) _ ?_ h'
    refine ih (fun s hs ↦ ?_) h'.right
    exact ht s (Or.inr hs)

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Set α
⊢ IsPiSystem (Iio '' s)

Tactic:
rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩ -
  exact ⟨a ⊓ b, inf_ind a b ha hb, Iio_inter_Iio.symm⟩

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

Goal state before:
pp: case refine_2
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
h₀ : m ∅ = 0
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
f : ℕ → Set α
hf : t ⊆ ⋃ i, f i
⊢ t \ s ⊆ (⋃ i, f i) \ s

Tactic:
exact sdiff_subset_sdiff_left hf

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
s : Set (Set α)
hs : IsPiSystem s
⊢ generate s ≤ ofMeasurableSpace (generateFrom s)

Tactic:
exact generate_le _ fun t ht => measurableSet_generateFrom ht

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
ι : Sort u_2
inst✝ : Countable ι
μ : ι → OuterMeasure α
s : Set α
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ∀ (i : ι), (μ i) t = (μ i).trim s

Tactic:
choose t hst ht hμt using fun i => (μ i).exists_measurable_superset_eq_trim s

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
ι : Sort u_2
inst✝ : Countable ι
μ : ι → OuterMeasure α
s : Set α
t : ι → Set α
hst : ∀ (i : ι), s ⊆ t i
ht : ∀ (i : ι), MeasurableSet (t i)
hμt : ∀ (i : ι), (μ i) (t i) = (μ i).trim s
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ∀ (i : ι), (μ i) t = (μ i).trim s
Module: Mathlib.MeasureTheory.Measure.NullMeasurable

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : μ sᶜ = 0
⊢ μ s = μ univ

Tactic:
simpa [hs] using measure_add_measure_compl₀ <| .of_compl <| .of_null hs

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

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSingletonClass α
mβ : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass β
inst✝ : Countable α
μ : Measure (α × β)
y : β
this : Prod.snd ⁻¹' {y} = ⋃ x, {(x, y)}
⊢ μ (Prod.snd ⁻¹' {y}) = ∑' (x : α), μ {(x, y)}

Tactic:
rw [this, measure_iUnion] <;> simp [Pairwise]

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

Goal state before:
pp: α : Type u_1
ι : Type u_8
x✝ : MeasurableSpace α
μ : Measure α
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ
As_disj : Pairwise (AEDisjoint μ on As)
⊢ ∑' (i : ι), μ (As i) ≤ μ (⋃ i, As i)

Tactic:
rw [ENNReal.tsum_eq_iSup_sum, iSup_le_iff]
  intro s
  simp only [← measure_biUnion_finset₀ (fun _i _hi _j _hj hij => As_disj hij) fun i _ => As_mble i]
  gcongr
  exact iUnion_subset fun _ ↦ Subset.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
⊢ comap Subtype.val (𝓝[>] b) = atBot ↔ s ⊆ Ioi b ∧ (s.Nonempty → ∀ a > b, (s ∩ Ioo b a).Nonempty)

Tactic:
refine comap_coe_nhdsLT_eq_atTop_iff (s := OrderDual.ofDual ⁻¹' s) (b := OrderDual.toDual b)
    |>.trans ?_

Goal state after:
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
b : X
⊢ ⇑ofDual ⁻¹' s ⊆ Iio (toDual b) ∧
      ((⇑ofDual ⁻¹' s).Nonempty → ∀ a < toDual b, (⇑ofDual ⁻¹' s ∩ Ioo a (toDual b)).Nonempty) ↔
    s ⊆ Ioi b ∧ (s.Nonempty → ∀ a > b, (s ∩ Ioo b a).Nonempty)
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
⊢ t ∪ s =ᵐ[μ] t ↔ s ≤ᵐ[μ] t

Tactic:
union_ae_eq_left_iff_ae_subset

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
⊢ s ≤ᵐ[μ] t ↔ s ≤ᵐ[μ] t
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 + ε
⊢ μ univ - μ s + (μ t + ε) = μ univ - μ s + ε + μ t

Tactic:
by rw [add_right_comm, add_assoc]

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → β
hf : AEMeasurable f μ
⊢ IsFiniteMeasure (map f μ)

Tactic:
constructor
    rw [map_apply_of_aemeasurable hf MeasurableSet.univ]
    exact measure_lt_top μ _

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t s : Set α
ht : NullMeasurableSet t μ
⊢ μ.restrict (s ∩ t) + μ.restrict (s \ t) = μ.restrict s

Tactic:
by
  ext1 u hu
  simp only [add_apply, restrict_apply hu, ← inter_assoc, sdiff_eq]
  exact measure_inter_add_sdiff₀ (u ∩ s) ht

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}
i : ι
ω : α
⊢ (Monotone fun x ↦ ω ∈ s x) → s i ω = t i ω

Tactic:
hω

Goal state after:
α : 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}
i : ι
ω : α
hω : Monotone fun x ↦ ω ∈ s x
⊢ s i ω = t i ω
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
hd : Pairwise (AEDisjoint μ on s)
hm : ∀ (i : ι), NullMeasurableSet (s i) μ
t : Set α
ht : MeasurableSet t
⊢ μ (⋃ i, t ∩ s i) = ∑' (i : ι), μ (t ∩ s i)

Tactic:
exact
    measure_iUnion₀ (hd.mono fun i j h => h.mono inter_subset_right inter_subset_right)
      fun i => ht.nullMeasurableSet.inter (hm i)

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

Goal state before:
pp: α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsDirectedOrder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hs : ∀ᵐ (ω : α) ∂μ, Antitone fun x ↦ ω ∈ s x
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
hfin : ∃ i, μ (s i) ≠ ∞
ω : α
⊢ (Antitone fun x ↦ ω ∈ s x) → Monotone fun x ↦ ω ∈ s x

Tactic:
hω

Goal state after:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsDirectedOrder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hs : ∀ᵐ (ω : α) ∂μ, Antitone fun x ↦ ω ∈ s x
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
hfin : ∃ i, μ (s i) ≠ ∞
ω : α
hω : Antitone fun x ↦ ω ∈ s x
⊢ Monotone fun x ↦ ω ∈ s x
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_8
inst✝³ : LinearOrder ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
s : ι → Set α
a : ι
hs : ∀ r > a, NullMeasurableSet (s r) μ
hm : ∀ (i j : ι), a < i → i ≤ j → s i ⊆ s j
hf : ∃ r > a, μ (s r) ≠ ∞
ha : Order.IsPredPrelimit a
this : atBot.IsCountablyGenerated
⊢ Tendsto (⇑μ ∘ s) (𝓝[>] a) (𝓝 (μ (⋂ r, ⋂ (_ : r > a), s r)))

Tactic:
simp_rw [← map_coe_Ioi_atBot a ha, tendsto_map'_iff, ← mem_Ioi, biInter_eq_iInter]

Goal state after:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_8
inst✝³ : LinearOrder ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
s : ι → Set α
a : ι
hs : ∀ r > a, NullMeasurableSet (s r) μ
hm : ∀ (i j : ι), a < i → i ≤ j → s i ⊆ s j
hf : ∃ r > a, μ (s r) ≠ ∞
ha : Order.IsPredPrelimit a
this : atBot.IsCountablyGenerated
⊢ Tendsto ((⇑μ ∘ s) ∘ Subtype.val) atBot (𝓝 (μ (⋂ x, s ↑x)))
Module: Mathlib.MeasureTheory.Measure.Trim

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
hm : m ≤ m0
⊢ μ.trim hm ≪ ν.trim hm

Tactic:
by
  refine Measure.AbsolutelyContinuous.mk (fun s hs hsν ↦ ?_)
  rw [trim_measurableSet_eq hm hs] at hsν ⊢
  exact hμν hsν

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

Goal state before:
pp: α : Type u_1
p : Set α → Prop
t : Set α
q : Set ↑t → Prop
h✝ : HasCountableSeparatingOn (↑t) q univ
hpq : ∀ (U : Set ↑t), q U → ∃ V, p V ∧ Subtype.val ⁻¹' V = U
S : Set (Set ↑t)
hSc : S.Countable
hSq : ∀ s ∈ S, q s
hS : ∀ x ∈ univ, ∀ y ∈ univ, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
V : Set ↑t → Set α
hpV : ∀ s ∈ S, p (V s)
hV : ∀ s ∈ S, Subtype.val ⁻¹' V s = s
x : α
hx : x ∈ t
y : α
hy : y ∈ t
h : ∀ s ∈ V '' S, x ∈ s ↔ y ∈ s
U : Set ↑t
hU : U ∈ S
⊢ ⟨x, hx⟩ ∈ U ↔ ⟨y, hy⟩ ∈ U

Tactic:
← hV U hU

Goal state after:
α : Type u_1
p : Set α → Prop
t : Set α
q : Set ↑t → Prop
h✝ : HasCountableSeparatingOn (↑t) q univ
hpq : ∀ (U : Set ↑t), q U → ∃ V, p V ∧ Subtype.val ⁻¹' V = U
S : Set (Set ↑t)
hSc : S.Countable
hSq : ∀ s ∈ S, q s
hS : ∀ x ∈ univ, ∀ y ∈ univ, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
V : Set ↑t → Set α
hpV : ∀ s ∈ S, p (V s)
hV : ∀ s ∈ S, Subtype.val ⁻¹' V s = s
x : α
hx : x ∈ t
y : α
hy : y ∈ t
h : ∀ s ∈ V '' S, x ∈ s ↔ y ∈ s
U : Set ↑t
hU : U ∈ S
⊢ ⟨x, hx⟩ ∈ Subtype.val ⁻¹' V U ↔ ⟨y, hy⟩ ∈ Subtype.val ⁻¹' V U
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: case hn
α : 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
⊢ Pairwise (Disjoint on disjointed w)

Tactic:
exact disjoint_disjointed _

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

Goal state before:
pp: case refine_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : Group β
f g : α → β
h : f / g =ᵐ[μ] 1
x : α
hx : f x / g x = 1 x
⊢ f x = g x

Tactic:
Pi.one_apply,

Goal state after:
case refine_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : Group β
f g : α → β
h : f / g =ᵐ[μ] 1
x : α
hx : f x / g x = 1
⊢ f x = g x
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: case refine_2
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : Group β
f g : α → β
h : f =ᵐ[μ] g
x : α
hx : f x = g x
⊢ f x / g x = 1 x

Tactic:
Pi.one_apply,

Goal state after:
case refine_2
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : Group β
f g : α → β
h : f =ᵐ[μ] g
x : α
hx : f x = g x
⊢ f x / g x = 1
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: case refine_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝² : Group β
inst✝¹ : LE β
inst✝ : MulRightMono β
f g : α → β
h : 1 ≤ᵐ[μ] g / f
a : α
ha : 1 a ≤ (g / f) a
⊢ f a ≤ g a

Tactic:
Pi.one_apply,

Goal state after:
case refine_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝² : Group β
inst✝¹ : LE β
inst✝ : MulRightMono β
f g : α → β
h : 1 ≤ᵐ[μ] g / f
a : α
ha : 1 ≤ (g / f) a
⊢ f a ≤ g a
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: case refine_2
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝² : Group β
inst✝¹ : LE β
inst✝ : MulRightMono β
f g : α → β
h : f ≤ᵐ[μ] g
a : α
ha : f a ≤ g a
⊢ 1 a ≤ (g / f) a

Tactic:
Pi.one_apply,

Goal state after:
case refine_2
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝² : Group β
inst✝¹ : LE β
inst✝ : MulRightMono β
f g : α → β
h : f ≤ᵐ[μ] g
a : α
ha : f a ≤ g a
⊢ 1 ≤ (g / f) a
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : (μ.restrict sᶜ) {a | ¬f a = b} = 0
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
⊢ μ (f ⁻¹' t) = μ (f ⁻¹' t ∩ s)

Tactic:
Measure.restrict_apply₀

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : μ ({a | ¬f a = b} ∩ sᶜ) = 0
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
⊢ μ (f ⁻¹' t) = μ (f ⁻¹' t ∩ s)

α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : (μ.restrict sᶜ) {a | ¬f a = b} = 0
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
⊢ NullMeasurableSet {a | ¬f a = b} (μ.restrict sᶜ)
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 α
m : Set (Measure α)
x✝ : MeasurableSpace α
f : ℕ → Set α
⊢ (∀ (i : ℕ), MeasurableSet (f i)) → Pairwise (Disjoint on f) → ⊤ (⋃ i, f i) = ∑' (i : ℕ), ⊤ (f i)

Tactic:
_

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 α
m : Set (Measure α)
x✝ : MeasurableSpace α
f : ℕ → Set α
a✝ : ∀ (i : ℕ), MeasurableSet (f i)
⊢ Pairwise (Disjoint on f) → ⊤ (⋃ i, f i) = ∑' (i : ℕ), ⊤ (f i)
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 α
m : Set (Measure α)
x✝ : MeasurableSpace α
f : ℕ → Set α
a✝ : ∀ (i : ℕ), MeasurableSet (f i)
⊢ Pairwise (Disjoint on f) → ⊤ (⋃ i, f i) = ∑' (i : ℕ), ⊤ (f i)

Tactic:
_

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 α
m : Set (Measure α)
x✝ : MeasurableSpace α
f : ℕ → Set α
a✝¹ : ∀ (i : ℕ), MeasurableSet (f i)
a✝ : Pairwise (Disjoint on f)
⊢ ⊤ (⋃ i, f i) = ∑' (i : ℕ), ⊤ (f i)
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)
u : Set α
huS : u ∈ ↑S
v : Set α
huV : v ∈ memPartition t n \ ↑S
⊢ Disjoint v u

Tactic:
refine disjoint_memPartition t n (mem_of_mem_sdiff huV) (hS_subset huS) ?_

Goal state after:
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)
u : Set α
huS : u ∈ ↑S
v : Set α
huV : v ∈ memPartition t n \ ↑S
⊢ v ≠ u
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case refine_1
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
h : MeasurableSet s
⊢ ∃ S, ↑S ⊆ memPartition t n ∧ s = ⋃₀ ↑S

Tactic:
induction s, h using generateFrom_induction with
    | hC u hu _ => exact ⟨{u}, by simp [hu], by simp⟩
    | empty => exact ⟨∅, by simp, by simp⟩
    | compl u _ hu =>
      obtain ⟨S, hS_subset, rfl⟩ := hu
      refine ⟨(memPartition t n).toFinset \ S, ?_, ?_⟩
      · simp only [Finset.coe_sdiff, coe_toFinset]
        exact sdiff_subset
      · simp only [Finset.coe_sdiff, coe_toFinset]
        refine (IsCompl.eq_compl ⟨?_, ?_⟩).symm
        · 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
        · rw [codisjoint_iff]
          simp only [sup_eq_union, top_eq_univ]
          rw [← sUnion_memPartition t n, union_comm, ← sUnion_union, union_sdiff_cancel hS_subset]
    | iUnion f _ h =>
      choose S hS_subset hS_eq using h
      have : Fintype (⋃ n, (S n : Set (Set α))) := by
        refine (Finite.subset (finite_memPartition t n) ?_).fintype
        simp only [iUnion_subset_iff]
        exact hS_subset
      refine ⟨(⋃ n, (S n : Set (Set α))).toFinset, ?_, ?_⟩
      · simp only [coe_toFinset, iUnion_subset_iff]
        exact hS_subset
      · simp only [coe_toFinset, sUnion_iUnion, hS_eq]

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'
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
⊢ ∑' (n : ↑{k | μ (t' k) ≤ ν (t' k)}), μ (t' ↑n) + ∑' (n : ↑{k | ν (t' k) < μ (t' k)}), ν (t' ↑n) ≤
    ∑' (x : ↑({k | μ (t' k) ≤ ν (t' k)} ∪ {k | ν (t' k) < μ (t' k)})), min (μ (t' ↑x)) (ν (t' ↑x))

Tactic:
ENNReal.summable.tsum_union_disjoint (f := fun n ↦ μ (t' n) ⊓ ν (t' n)) ?_ ENNReal.summable

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
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
⊢ ∑' (n : ↑{k | μ (t' k) ≤ ν (t' k)}), μ (t' ↑n) + ∑' (n : ↑{k | ν (t' k) < μ (t' k)}), ν (t' ↑n) ≤
    ∑' (x : ↑{k | μ (t' k) ≤ ν (t' k)}), min (μ (t' ↑x)) (ν (t' ↑x)) +
      ∑' (x : ↑{k | ν (t' k) < μ (t' k)}), min (μ (t' ↑x)) (ν (t' ↑x))

α : 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)}
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: case negSucc
α : Type u_1
G : Type u
inst✝³ : DivInvMonoid G
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableMul₂ G
inst✝ : MeasurableInv G
n : ℕ
⊢ Measurable fun x ↦ (x, Int.negSucc n).1 ^ (x, Int.negSucc n).2

Tactic:
simp_rw [zpow_negSucc]
        exact (measurable_id.pow_const (n + 1)).inv

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

Goal state before:
pp: M : Type u_2
α : Type u_3
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
l : List (α → M)
hl : ∀ f ∈ l, Measurable f
⊢ Measurable fun x ↦ (map (fun f ↦ f x) l).prod

Tactic:
by
  simpa only [← Pi.list_prod_apply] using l.measurable_prod hl

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
⊢ infEDist x s ≤ infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)

Tactic:
refine ENNReal.le_of_forall_pos_le_add fun ε εpos h => ?_

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) < ∞
⊢ infEDist x s ≤ infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + ↑ε
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: α : Type u_6
β : Type u_7
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace β
inst✝ : TopologicalSpace β
hβ : BorelSpace β
e : α → β
h'e : MeasurableEmbedding e
h''e : IsInducing e
⊢ inst✝³ = borel α

Tactic:
have : MeasurableSpace.comap e (borel β) = ‹_› := by simpa [hβ.measurable_eq] using h'e.comap_eq

Goal state after:
α : Type u_6
β : Type u_7
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace β
inst✝ : TopologicalSpace β
hβ : BorelSpace β
e : α → β
h'e : MeasurableEmbedding e
h''e : IsInducing e
this : MeasurableSpace.comap e (borel β) = inst✝³
⊢ inst✝³ = borel α
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: case h₂
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
x : α
hx : ∀ i ∈ s, infEDist x E ≤ ENNReal.ofReal i
η : ℝ≥0
η_pos : 0 < η
⊢ ENNReal.ofReal δ < ∞ → infEDist x E ≤ ENNReal.ofReal δ + ↑η

Tactic:
_

Goal state after:
case h₂
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
x : α
hx : ∀ i ∈ s, infEDist x E ≤ ENNReal.ofReal i
η : ℝ≥0
η_pos : 0 < η
a✝ : ENNReal.ofReal δ < ∞
⊢ infEDist x E ≤ ENNReal.ofReal δ + ↑η
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: β : Type u_2
δ : Type u_4
inst✝⁶ : TopologicalSpace β
mβ : MeasurableSpace β
inst✝⁵ : BorelSpace β
mδ : MeasurableSpace δ
inst✝⁴ : CompleteLinearOrder β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
ι : Type u_5
inst✝¹ : TopologicalSpace ι
inst✝ : SeparableSpace ι
f : ι → δ → β
mf : ∀ (t : ι), Measurable (f t)
cf : ∀ (x : δ), LowerSemicontinuous fun x_1 ↦ f x_1 x
c : β
⊢ MeasurableSet ((⨆ i, f i) ⁻¹' Ioi c)

Tactic:
obtain ⟨J, cJ, dJ⟩ := TopologicalSpace.exists_countable_dense ι

Goal state after:
β : Type u_2
δ : Type u_4
inst✝⁶ : TopologicalSpace β
mβ : MeasurableSpace β
inst✝⁵ : BorelSpace β
mδ : MeasurableSpace δ
inst✝⁴ : CompleteLinearOrder β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
ι : Type u_5
inst✝¹ : TopologicalSpace ι
inst✝ : SeparableSpace ι
f : ι → δ → β
mf : ∀ (t : ι), Measurable (f t)
cf : ∀ (x : δ), LowerSemicontinuous fun x_1 ↦ f x_1 x
c : β
J : Set ι
cJ : J.Countable
dJ : Dense J
⊢ MeasurableSet ((⨆ i, f i) ⁻¹' Ioi c)
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
f : γ → α →ₛ β
s✝ : Finset γ
a✝ : α
a : γ
s : Finset γ
⊢ a ∉ s → ((s.sup f) a✝ = s.sup fun c ↦ (f c) a✝) → ((insert a s).sup f) a✝ = (insert a s).sup fun c ↦ (f c) a✝

Tactic:
_

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
f : γ → α →ₛ β
s✝ : Finset γ
a✝¹ : α
a : γ
s : Finset γ
a✝ : a ∉ s
⊢ ((s.sup f) a✝¹ = s.sup fun c ↦ (f c) a✝¹) → ((insert a s).sup f) a✝¹ = (insert a s).sup fun c ↦ (f c) a✝¹