mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: ⊢ pos ≤ neg

Tactic:
by constructor

Goal state after:
⊢ pos ≤ neg
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: ⊢ pos ≤ pos

Tactic:
by constructor

Goal state after:
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ ∞ = ∞ * (↑x✝).abs

Tactic:
ENNReal.top_mul

Goal state after:
case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ ∞ = ∞

case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ (↑x✝).abs ≠ 0
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: case pos
β : Type u_2
f : β → ℝ≥0
h : Summable f
⊢ ∑' (b : β), f b = (↑(tsum f)).toNNReal

Tactic:
ENNReal.toNNReal_coe

Goal state after:
case pos
β : Type u_2
f : β → ℝ≥0
h : Summable f
⊢ ∑' (b : β), f b = tsum f
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: case mp
f : ℕ → ℝ≥0
⊢ ¬Summable f → Tendsto (fun n ↦ ∑ i ∈ Finset.range n, f i) atTop atTop

pp: case mpr
f : ℕ → ℝ≥0
⊢ Tendsto (fun n ↦ ∑ i ∈ Finset.range n, f i) atTop atTop → ¬Summable f

Tactic:
· intro h
    refine ((tendsto_atTop_of_monotone ?_).resolve_right h).comp ?_
    exacts [Finset.sum_mono_set _, tendsto_finset_range]

Goal state after:
case mpr
f : ℕ → ℝ≥0
⊢ Tendsto (fun n ↦ ∑ i ∈ Finset.range n, f i) atTop atTop → ¬Summable f
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: f : ℕ → ℝ≥0∞
hf : ∑' (i : ℕ), f i ≠ ∞
⊢ Tendsto (fun i ↦ ∑' (k : ℕ), f (k + i)) atTop (𝓝 0)

Tactic:
lift f to ℕ → ℝ≥0 using ENNReal.ne_top_of_tsum_ne_top hf
  replace hf : Summable f := tsum_coe_ne_top_iff_summable.1 hf
  simp only [← ENNReal.coe_tsum, NNReal.summable_nat_add _ hf, ← ENNReal.coe_zero]
  exact mod_cast NNReal.tendsto_sum_nat_add f

Goal state after:
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: m n : ℕ
⊢ ↑(m / n) ≤ ↑m / ↑n

Tactic:
rw [← coe_coe_eq_natCast, ← coe_coe_eq_natCast, ← coe_coe_eq_natCast, ← coe_div,
    EReal.coe_le_coe_iff]

Goal state after:
m n : ℕ
⊢ ↑(m / n) ≤ ↑m / ↑n
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → β
inst✝ : LinearOrder β
s : Set α
ne_s : s.Nonempty
hs : IsCompact s
hf : LowerSemicontinuousOn f s
x✝¹ : Nonempty α
x✝ : Nonempty ↑s
φ : β → Filter α := fun b ↦ 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ a, φ (f ↑a)
this : ℱ.NeBot
hℱs : ℱ ≤ 𝓟 s
x : α
hx : x ∈ s
⊢ {x_1 | (fun y ↦ f y ≤ f x) x_1} ∈ φ (f ↑⟨x, hx⟩)

Tactic:
apply inter_subset_right

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ ↑(d n)
ε : ℝ≥0
εpos : 0 < ε
hd : CauchySeq fun n ↦ ∑ x ∈ Finset.range n, d x
⊢ ∃ N, ∀ (n : ℕ), N ≤ n → edist (f n) (f N) < ↑ε

Tactic:
refine (Metric.cauchySeq_iff'.1 hd ε (NNReal.coe_pos.2 εpos)).imp fun N hN n hn ↦ ?_

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ ↑(d n)
ε : ℝ≥0
εpos : 0 < ε
hd : CauchySeq fun n ↦ ∑ x ∈ Finset.range n, d x
N : ℕ
hN : ∀ n ≥ N, dist (∑ x ∈ Finset.range n, d x) (∑ x ∈ Finset.range N, d x) < ↑ε
n : ℕ
hn : N ≤ n
⊢ edist (f n) (f N) < ↑ε
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a b c : EReal
h₁ : a ≠ 0 ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < b
hc : a * b < c
⊢ ∃ a' ∈ Ioo a ⊤, a' * b < c

Tactic:
rcases eq_top_or_lt_top a with rfl | a_top

Goal state after:
case inl
b c : EReal
h₁ : ⊤ ≠ 0 ∨ b ≠ ⊤
h₂ : ⊤ ≠ ⊤ ∨ 0 < b
hc : ⊤ * b < c
⊢ ∃ a' ∈ Ioo ⊤ ⊤, a' * b < c

case inr
a b c : EReal
h₁ : a ≠ 0 ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < b
hc : a * b < c
a_top : a < ⊤
⊢ ∃ a' ∈ Ioo a ⊤, a' * b < c
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case inr.inr.inl.inr.inl
c : EReal
b0 : 0 < ⊤
a_top : 0 < ⊤
h₁ : 0 ≠ 0 ∨ ⊤ ≠ ⊤
h₂ : 0 ≠ ⊤ ∨ 0 < ⊤
hc : 0 * ⊤ < c
⊢ ∃ a' ∈ Ioo 0 ⊤, a' * ⊤ < c

Tactic:
rw [ne_self_iff_false, ne_self_iff_false, false_or] at h₁; exact h₁.rec

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

Goal state before:
pp: α : Type u_1
⊢ ∀ (s : Set α), s.Nonempty → ⊤ s ≤ ⊤ s

Tactic:
intro s hs

Goal state after:
α : Type u_1
s : Set α
hs : s.Nonempty
⊢ ⊤ s ≤ ⊤ s
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case inr
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
ht : t ∈ insert ∅ S
hst : (s ∩ t).Nonempty
hs : s ∈ S
⊢ s ∩ t ∈ insert ∅ S

Tactic:
· rcases ht with ht | ht
    · simp [ht]
    · exact Set.mem_insert_of_mem _ (h_pi s hs t ht hst)

Goal state after:
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)
⊢ ∀ᶠ (b : R) in atTop, a - b⁻¹ ≤ ↑⌊a * b⌋₊ / b

pp: case hfh
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)
⊢ ∀ᶠ (b : R) in atTop, ↑⌊a * b⌋₊ / b ≤ a

Tactic:
· refine eventually_atTop.2 ⟨1, fun x hx ↦ ?_⟩
    simp only [le_div_iff₀ (zero_lt_one.trans_le hx), _root_.sub_mul,
      inv_mul_cancel₀ (zero_lt_one.trans_le hx).ne']
    have := Nat.lt_floor_add_one (a * x)
    linarith

Goal state after:
case hfh
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)
⊢ ∀ᶠ (b : R) in atTop, ↑⌊a * b⌋₊ / b ≤ a
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_2
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
s : α
h : P s
⊢ extend m s = m s h

Tactic:
simp [extend, h]

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

Goal state before:
pp: α : Type u_2
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
s : α
h : ¬P s
⊢ extend m s = ∞

Tactic:
simp [extend, h]

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

Goal state before:
pp: α : Type u
m : OuterMeasure α
s₁ s₂ : Set α
h₁ : m.IsCaratheodory s₁
h₂ : m.IsCaratheodory s₂
⊢ m.IsCaratheodory (s₁ ∩ s₂)

Tactic:
by
  rw [← isCaratheodory_compl_iff, Set.compl_inter]
  exact isCaratheodory_union _ (isCaratheodory_compl _ h₁) (isCaratheodory_compl _ h₂)

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
s : Set (Set α)
hs : IsPiSystem s
t₁ t₂ : Set α
ht₁ : (generate s).Has t₁
ht₂ : (generate s).Has t₂
s₁ : Set α
hs₁ : s₁ ∈ s
this✝¹ : (generate s).Has s₁
this✝ : generate s ≤ (generate s).restrictOn this✝¹
this : (generate s).Has (t₂ ∩ s₁)
⊢ (generate s).Has (s₁ ∩ t₂)

Tactic:
rwa [inter_comm]

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

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst✝ : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i) μ
hp : ∀ᵐ (x : α) ∂μ, p x fun n ↦ f n x
⊢ μ {x | (∀ (i : ι), f i x = AEMeasurable.mk (f i) ⋯ x) ∧ p x fun n ↦ f n x}ᶜ = 0

Tactic:
have hf_eq := fun i => (hf i).ae_eq_mk

Goal state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst✝ : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i) μ
hp : ∀ᵐ (x : α) ∂μ, p x fun n ↦ f n x
hf_eq : ∀ (i : ι), f i =ᵐ[μ] AEMeasurable.mk (f i) ⋯
⊢ μ {x | (∀ (i : ι), f i x = AEMeasurable.mk (f i) ⋯ x) ∧ p x fun n ↦ f n x}ᶜ = 0
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_2
m : OuterMeasure α
m0 m1 : MeasurableSpace α
h : m0 ≤ m1
⊢ ∀ (s : Set α), MeasurableSet s → m.trim s ≤ m s

Tactic:
intro s hs

Goal state after:
α : Type u_2
m : OuterMeasure α
m0 m1 : MeasurableSpace α
h : m0 ≤ m1
s : Set α
hs : MeasurableSet s
⊢ m.trim s ≤ m s
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → γ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet (g ∘ f '' s)

Tactic:
by
    rwa [image_comp, hg.measurableSet_image, hf.measurableSet_image]

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

Goal state before:
pp: case refine_2
ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
hd : Pairwise (AEDisjoint μ on s)
i j : ι
hne : i ≠ j
x : α
hi : x ∈ s i
⊢ x ∉ toMeasurable μ (s i ∩ ⋃ j ∈ {i}ᶜ, s j) → x ∈ s j → x ∈ toMeasurable μ (s j ∩ ⋃ j_1 ∈ {j}ᶜ, s j_1)

Tactic:
hU

Goal state after:
case refine_2
ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
hd : Pairwise (AEDisjoint μ on s)
i j : ι
hne : i ≠ j
x : α
hi : x ∈ s i
hU : x ∉ toMeasurable μ (s i ∩ ⋃ j ∈ {i}ᶜ, s j)
⊢ x ∈ s j → x ∈ toMeasurable μ (s j ∩ ⋃ j_1 ∈ {j}ᶜ, s j_1)
Module: Mathlib.MeasureTheory.Measure.AEDisjoint

Goal state before:
pp: α : Type u_2
m : MeasurableSpace α
μ : Measure α
s t : Set α
h : AEDisjoint μ s t
⊢ AEDisjoint μ t s

Tactic:
AEDisjoint,

Goal state after:
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s t : Set α
h : AEDisjoint μ s t
⊢ μ (t ∩ s) = 0
Module: Mathlib.MeasureTheory.Measure.AEDisjoint

Goal state before:
pp: α : Type u_2
m : MeasurableSpace α
μ : Measure α
s t : Set α
h : Disjoint s t
⊢ AEDisjoint μ s t

Tactic:
AEDisjoint,

Goal state after:
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s t : Set α
h : Disjoint s t
⊢ μ (s ∩ t) = 0
Module: Mathlib.MeasureTheory.Measure.Map

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f g : α → β
h : f =ᵐ[μ] g
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ map f μ = map g μ

Tactic:
simp only [← mapₗ_mk_apply_of_aemeasurable hf, ← mapₗ_mk_apply_of_aemeasurable hg]

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f g : α → β
h : f =ᵐ[μ] g
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ (mapₗ (AEMeasurable.mk f hf)) μ = (mapₗ (AEMeasurable.mk g hg)) μ
Module: Mathlib.MeasureTheory.Measure.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
⊢ ∀ (s : Set β), MeasurableSet s → (map f μ).toOuterMeasure s = ((OuterMeasure.map f) μ.toOuterMeasure) s

Tactic:
intro s hs

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
s : Set β
hs : MeasurableSet s
⊢ (map f μ).toOuterMeasure s = ((OuterMeasure.map f) μ.toOuterMeasure) s
Module: Mathlib.MeasureTheory.Measure.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure α
s : Set β
⊢ (map f μ) s ≤ μ (f ⁻¹' s)

Tactic:
set t := f '' toMeasurable μ (f ⁻¹' s) ∪ (range f)ᶜ

Goal state after:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure α
s : Set β
t : Set β := f '' toMeasurable μ (f ⁻¹' s) ∪ (range f)ᶜ
⊢ (map f μ) s ≤ μ (f ⁻¹' s)
Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : ∀ ⦃s : Set α⦄, MeasurableSet s → ν s = 0 → μ s = 0
⊢ μ ≪ ν

Tactic:
intro s hs

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : ∀ ⦃s : Set α⦄, MeasurableSet s → ν s = 0 → μ s = 0
s : Set α
hs : ν s = 0
⊢ μ s = 0
Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν ν' : Measure α
h1 : μ₁ ≪ ν
h2 : μ₂ ≪ ν'
⊢ μ₁ + μ₂ ≪ ν + ν'

Tactic:
intro s hs

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν ν' : Measure α
h1 : μ₁ ≪ ν
h2 : μ₂ ≪ ν'
s : Set α
hs : (ν + ν') s = 0
⊢ (μ₁ + μ₂) s = 0
Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h1 : μ ≪ ν
ν' : Measure α
⊢ μ ≪ ν + ν'

Tactic:
intro s hs

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h1 : μ ≪ ν
ν' : Measure α
s : Set α
hs : (ν + ν') s = 0
⊢ μ s = 0
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
⊢ s₁ ∩ s₂ ⊆ s₂

Tactic:
apply inter_subset_right

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
hst : s ⊆ t
hs' : μ s ≠ ∞
ε : ℝ≥0∞
⊢ μ (t \ s) ≤ ε ↔ μ t ≤ μ s + ε

Tactic:
measure_sdiff hst hs hs',

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
hst : s ⊆ t
hs' : μ s ≠ ∞
ε : ℝ≥0∞
⊢ μ t - μ s ≤ ε ↔ μ t ≤ μ s + ε
Module: Mathlib.Topology.Order.AtTopBotIxx

Goal state before:
pp: case inr
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
b : X
hsb : s ⊆ Iio b
hs : ∀ a' < b, ∃ a < b, Ioo a b ⊆ s
hb : IsSuccPrelimit b
a : X
ha : a ∈ Iio b
⊢ map Subtype.val atTop = 𝓝[<] b

Tactic:
rw [← comap_coe_nhdsLT_of_Ioo_subset hsb (fun _ => hs a ha) hb, map_comap_of_mem]
    rw [Subtype.range_val]
    exact (mem_nhdsLT_iff_exists_Ioo_subset' ha).2 (hs a ha)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ ν : Measure α
s✝ t : Set α
a : α
inst✝ : SFinite μ
s : Set α
⊢ μ.restrict s = sum fun n ↦ (sfiniteSeq μ n).restrict s

Tactic:
← restrict_sum_of_countable,

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ ν : Measure α
s✝ t : Set α
a : α
inst✝ : SFinite μ
s : Set α
⊢ μ.restrict s = (sum (sfiniteSeq μ)).restrict s
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)}
fairmeas_eq : ∀ (n : ℕ), fairmeas n = (fun i ↦ μ (As i)) ⁻¹' Ici (as n)
⊢ posmeas = ⋃ n, fairmeas n

Tactic:
simpa only [fairmeas_eq, posmeas_def, ← preimage_iUnion,
      iUnion_Ici_eq_Ioi_of_lt_of_tendsto (fun n => (as_mem n).1) as_lim]

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 α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
t : Set α
ht : MeasurableSet t
⊢ (μ.restrict (⋃ i, s i)) t = ⨆ i, (μ.restrict (s i)) t

Tactic:
simp only [restrict_apply ht, inter_iUnion]
  rw [Directed.measure_iUnion]
  exacts [hd.mono_comp _ fun s₁ s₂ => inter_subset_inter_right _]

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

Goal state before:
pp: α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
s : Finset ι
t : ι → Set α
⊢ μ.restrict (⋃ i ∈ s, t i) = ν.restrict (⋃ i ∈ s, t i) ↔ ∀ i ∈ s, μ.restrict (t i) = ν.restrict (t i)

Tactic:
induction s using Finset.induction_on with
  | empty => simp
  | insert i s _ hs =>
    simp only [forall_eq_or_imp, iUnion_iUnion_eq_or_left, Finset.mem_insert]
    rw [restrict_union_congr, ← hs]

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S : Set (Set α)
hc : S.Countable
⊢ μ.restrict (⋃₀ S) = ν.restrict (⋃₀ S) ↔ ∀ s ∈ S, μ.restrict s = ν.restrict s

Tactic:
rw [sUnion_eq_biUnion, restrict_biUnion_congr hc]

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

Goal state before:
pp: α : 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) ≠ ∞
⊢ Tendsto (⇑μ ∘ s) (𝓝[>] a) (𝓝 (μ (⋂ r, ⋂ (_ : r > a), s r)))

Tactic:
by
  by_cases ha : Order.IsPredPrelimit a
  · have : (atBot : Filter (Ioi a)).IsCountablyGenerated := by
      rw [← comap_coe_Ioi_nhdsGT a ha]
      infer_instance
    simp_rw [← map_coe_Ioi_atBot a ha, tendsto_map'_iff, ← mem_Ioi, biInter_eq_iInter]
    apply tendsto_measure_iInter_atBot
    · rwa [Subtype.forall]
    · exact fun i j h ↦ hm i j i.2 h
    · simpa only [Subtype.exists, exists_prop]
  · rw [Order.not_isPredPrelimit_iff] at ha
    rcases ha with ⟨b, hab⟩
    simp [hab.nhdsGT]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
⊢ inst✝¹ ≤ generateFrom (⋃ y, {measurableAtom y})

Tactic:
intro s hs

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet s
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
a✝ : Nontrivial β
inhabited_h : Inhabited β
S : Set (Set β)
hSc : S.Countable
hc : MeasurableSpace.CountablyGenerated β
h : NullMeasurable f μ
T : Set β → Set α
hTf : ∀ s ∈ S, T s ⊆ f ⁻¹' s
hTm : ∀ s ∈ S, MeasurableSet (T s)
hTeq : ∀ s ∈ S, T s =ᵐ[μ] f ⁻¹' s
U : Set β → Set α
hUf : ∀ s ∈ S, U s ⊇ f ⁻¹' s
hUm : ∀ s ∈ S, MeasurableSet (U s)
hUeq : ∀ s ∈ S, U s =ᵐ[μ] f ⁻¹' s
v : Set α := ⋃ s ∈ S, U s \ T s
⊢ AEMeasurable f μ

Tactic:
have hvm : MeasurableSet v := .biUnion hSc fun s hs ↦ (hUm s hs).diff (hTm s hs)

Goal state after:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
a✝ : Nontrivial β
inhabited_h : Inhabited β
S : Set (Set β)
hSc : S.Countable
hc : MeasurableSpace.CountablyGenerated β
h : NullMeasurable f μ
T : Set β → Set α
hTf : ∀ s ∈ S, T s ⊆ f ⁻¹' s
hTm : ∀ s ∈ S, MeasurableSet (T s)
hTeq : ∀ s ∈ S, T s =ᵐ[μ] f ⁻¹' s
U : Set β → Set α
hUf : ∀ s ∈ S, U s ⊇ f ⁻¹' s
hUm : ∀ s ∈ S, MeasurableSet (U s)
hUeq : ∀ s ∈ S, U s =ᵐ[μ] f ⁻¹' s
v : Set α := ⋃ s ∈ S, U s \ T s
hvm : MeasurableSet v
⊢ AEMeasurable f μ
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
⊢ μ.cofinite ≤ ae μ

Tactic:
intro s hs

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : s ∈ ae μ
⊢ s ∈ μ.cofinite
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
⊢ μ univ = 0 ↔ μ = 0

Tactic:
measure_univ_eq_zero

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
⊢ μ = 0 ↔ μ = 0
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
ι : Type u_7
β : Type u_8
mβ : MeasurableSpace β
m : ι → Measure α
f : α → β
s : Finset ι
hf : AEMeasurable f (∑ i ∈ s, m i)
⊢ map f (∑ i ∈ s, m i) = ∑ i ∈ s, map f (m i)

Tactic:
rw [← sum_coe_finset, ← sum_coe_finset, Measure.map_sum]
  rwa [sum_coe_finset]

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

Goal state before:
pp: γ : Type u_3
δ : Type u_5
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
inst✝ : MeasurableSpace δ
f : δ → γ
hf : ∀ (s : Set γ), IsClosed[inst✝³] s → MeasurableSet (f ⁻¹' s)
⊢ ∀ (s : Set γ), IsOpen[inst✝³] s → MeasurableSet (f ⁻¹' s)

Tactic:
intro s hs

Goal state after:
γ : Type u_3
δ : Type u_5
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
inst✝ : MeasurableSpace δ
f : δ → γ
hf : ∀ (s : Set γ), IsClosed[inst✝³] s → MeasurableSet (f ⁻¹' s)
s : Set γ
hs : IsOpen[inst✝³] s
⊢ MeasurableSet (f ⁻¹' s)
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: γ : Type u_3
δ : Type u_5
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
inst✝ : MeasurableSpace δ
f : δ → γ
hf : ∀ (s : Set γ), IsClosed[inst✝³] s → s.Nonempty → s ≠ univ → MeasurableSet (f ⁻¹' s)
⊢ ∀ (s : Set γ), IsClosed[inst✝³] s → MeasurableSet (f ⁻¹' s)

Tactic:
intro s hs

Goal state after:
γ : Type u_3
δ : Type u_5
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
inst✝ : MeasurableSpace δ
f : δ → γ
hf : ∀ (s : Set γ), IsClosed[inst✝³] s → s.Nonempty → s ≠ univ → MeasurableSet (f ⁻¹' s)
s : Set γ
hs : IsClosed[inst✝³] s
⊢ MeasurableSet (f ⁻¹' s)
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

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

Tactic:
simp only [hausdorffEDist_def, iSup_image, infEDist_image h]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
h : s.Nonempty
⊢ x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s ↔ infDist x s = 0

Tactic:
simp [mem_closure_iff_infEDist_zero, infDist, ENNReal.toReal_eq_zero_iff, infEDist_ne_top h]

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

Goal state before:
pp: α : Type u
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : ProperSpace α
hne : s.Nonempty
x : α
⊢ ∃ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s, infDist x s = dist x y

Tactic:
by
  simpa only [infDist_closure] using isClosed_closure.exists_infDist_eq_dist hne.closure x

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ ∀ (ε : ℝ), δ < ε → (Ioi δ ∩ Ioc δ ε).Nonempty

Tactic:
simp_rw [inter_eq_right.mpr Ioc_subset_Ioi_self]

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ ∀ (ε : ℝ), δ < ε → (Ioc δ ε).Nonempty
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_nn : 0 ≤ δ
E : Set α
⊢ ∀ (ε : ℝ), δ < ε → (Ioi δ ∩ Ioc δ ε).Nonempty

Tactic:
simp_rw [inter_eq_right.mpr Ioc_subset_Ioi_self]

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_nn : 0 ≤ δ
E : Set α
⊢ ∀ (ε : ℝ), δ < ε → (Ioc δ ε).Nonempty
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
⊢ ∀ ⦃s : Set γ⦄, MeasurableSet s → MeasurableSet ((fun y ↦ (x, f y)) '' s)

Tactic:
intro s hs

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
s : Set γ
hs : MeasurableSet s
⊢ MeasurableSet ((fun y ↦ (x, f y)) '' s)
Module: Mathlib.Topology.Instances.Real.Lemmas

Goal state before:
pp: s : Set ℝ
x : ℝ
⊢ x ∈ closure s ↔ ∀ ε > 0, ∃ y ∈ s, |y - x| < ε

Tactic:
simp [mem_closure_iff_nhds_basis nhds_basis_ball, Real.dist_eq]

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

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

Tactic:
classical
  rw [support_eq]
  refine (measure_biUnion_finset_le _ _).trans_lt (ENNReal.sum_lt_top.mpr fun y hy => ?_)
  rw [Finset.mem_filter] at hy
  exact hf y hy.2

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

Goal state before:
pp: a : ℝ
this : IsGLB (range Rat.cast ∩ Ioi a) a
⊢ MeasurableSet (Ioi a)

Tactic:
← this.biUnion_Ioi_eq,

Goal state after:
a : ℝ
this : IsGLB (range Rat.cast ∩ Ioi a) a
⊢ MeasurableSet (⋃ x ∈ range Rat.cast ∩ Ioi a, Ioi x)