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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : OuterMeasure α
⊢ LawfulFunctor OuterMeasure

Tactic:
constructor <;> intros <;> rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : OuterMeasure α
a : α
x✝¹ x✝ : Set α
h : x✝¹ ⊆ x✝
⊢ x✝¹.indicator (fun x ↦ 1) a ≤ x✝.indicator (fun x ↦ 1) a

Tactic:
h

Goal state after:
α : Type u_1
β : Type u_2
m : OuterMeasure α
a : α
x✝¹ x✝ : Set α
h : x✝¹ ⊆ x✝
⊢ x✝.indicator (fun x ↦ 1) a ≤ x✝.indicator (fun x ↦ 1) a
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
inst✝ : MeasurableSpace α
⊢ MeasurableSet (range Sum.inr)

Tactic:
by
  rw [← image_univ]
  exact MeasurableSet.univ.inr_image

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: α : Type u_1
inst✝⁵ : Zero α
inst✝⁴ : One α
inst✝³ : Neg α
β : Type u_2
inst✝² : One β
inst✝¹ : Neg β
inst✝ : Zero β
f : α → β
h₁ : f 1 = 1
h₂ : f 0 = 0
h₃ : f (-1) = -1
s : SignType
⊢ f ↑s = ↑s

Tactic:
by
  cases s <;> simp only [SignType.cast, h₁, h₂, h₃]

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h : 0 = a
⊢ 0 ≤ sign a ↔ 0 ≤ a

pp: case inr.inr
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h : a < 0
⊢ 0 ≤ sign a ↔ 0 ≤ a

Tactic:
· simp [← h]

Goal state after:
case inr.inr
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h : a < 0
⊢ 0 ≤ sign a ↔ 0 ≤ a
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h : 0 = a
⊢ sign a ≤ 0 ↔ a ≤ 0

pp: case inr.inr
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h : a < 0
⊢ sign a ≤ 0 ↔ a ≤ 0

Tactic:
· simp [← h]

Goal state after:
case inr.inr
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h : a < 0
⊢ sign a ≤ 0 ↔ a ≤ 0
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_1
ι : Type u_4
S : Set ι
f : α → ℝ≥0∞
t : ι → Set α
h : S.PairwiseDisjoint t
⊢ ∑' (x : ↑(⋃ i ∈ S, t i)), f ↑x = ∑' (i : ↑S) (x : ↑(t ↑i)), f ↑x

Tactic:
simp [← ENNReal.tsum_sigma, ← (Set.biUnionEqSigmaOfDisjoint h).tsum_eq]

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

Goal state before:
pp: case symm
x✝ y✝ : EReal
h : (x✝ * y✝).abs = x✝.abs * y✝.abs
⊢ (y✝ * x✝).abs = y✝.abs * x✝.abs

Tactic:
rwa [mul_comm, EReal.mul_comm]

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

Goal state before:
pp: case symm
x✝ y✝ : EReal
h : sign (x✝ * y✝) = sign x✝ * sign y✝
⊢ sign (y✝ * x✝) = sign y✝ * sign x✝

Tactic:
rwa [mul_comm, EReal.mul_comm]

Goal state after:
Module: Mathlib.Topology.Semicontinuity.Defs

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r : α → β → Prop
x : α
s : Set α
r' : α → β → Prop
h : SemicontinuousWithinAt r s x
h' : SemicontinuousWithinAt r' s x
b : β
hb : r x b
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (r ⊔ r') x' b

Tactic:
exact (h b hb).mono fun _ hx ↦ Or.inl hx

Goal state after:
Module: Mathlib.Topology.Semicontinuity.Defs

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r : α → β → Prop
x : α
r' : α → β → Prop
h : SemicontinuousAt r x
h' : SemicontinuousAt r' x
b : β
hb : r x b
⊢ ∀ᶠ (x' : α) in 𝓝 x, (r ⊔ r') x' b

Tactic:
exact (h b hb).mono fun _ hx ↦ Or.inl hx

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

Goal state before:
pp: case coe_coe
x y : ℝ
⊢ (↑x * ↑y)⁻¹ = (↑x)⁻¹ * (↑y)⁻¹

Tactic:
rw [← coe_mul, ← coe_inv, _root_.mul_inv, coe_mul, coe_inv, coe_inv]

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

Goal state before:
pp: α : Type u_1
f : α → ℝ
hf_nonneg : ∀ (n : α), 0 ≤ f n
hf : Summable f
⊢ ↑(∑' (n : α), f n).toNNReal = ∑' (n : α), ↑(f n).toNNReal

Tactic:
ENNReal.tsum_coe_eq (NNReal.hasSum_real_toNNReal_of_nonneg hf_nonneg hf)

Goal state after:
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
s : Set α
y : β
inst✝¹ : Zero β
inst✝ : Preorder β
hs : IsOpen[inst✝²] s
hy : 0 ≤ y
x : α
⊢ SemicontinuousAt (fun x1 x2 ↦ s.indicator (fun _x ↦ y) x1 > x2) x

Tactic:
z

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
s : Set α
y : β
inst✝¹ : Zero β
inst✝ : Preorder β
hs : IsOpen[inst✝²] s
hy : 0 ≤ y
x : α
z : β
⊢ (fun x1 x2 ↦ s.indicator (fun _x ↦ y) x1 > x2) x z →
    ∀ᶠ (x' : α) in 𝓝 x, (fun x1 x2 ↦ s.indicator (fun _x ↦ y) x1 > x2) x' z
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
s : Set α
y : β
inst✝¹ : Zero β
inst✝ : Preorder β
hs : IsClosed[inst✝²] s
hy : y ≤ 0
x : α
⊢ SemicontinuousAt (fun x1 x2 ↦ s.indicator (fun _x ↦ y) x1 > x2) x

Tactic:
z

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
s : Set α
y : β
inst✝¹ : Zero β
inst✝ : Preorder β
hs : IsClosed[inst✝²] s
hy : y ≤ 0
x : α
z : β
⊢ (fun x1 x2 ↦ s.indicator (fun _x ↦ y) x1 > x2) x z →
    ∀ᶠ (x' : α) in 𝓝 x, (fun x1 x2 ↦ s.indicator (fun _x ↦ y) x1 > x2) x' z
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
s : Set α
ι : Type u_4
f : ι → α → β
inst✝ : Preorder β
I : Set ι
hfy : ∀ i ∈ I, LowerSemicontinuousOn (f i) s
M : α → ι
M_mem : ∀ x ∈ s, M x ∈ I
M_max : ∀ x ∈ s, IsMaxOn (fun y ↦ f y x) I (M x)
x : α
hx : x ∈ s
b : β
hb : (fun x ↦ f (M x) x) x > b
z : α
hz : z ∈ s
⊢ (fun x1 x2 ↦ f (M x) x1 > x2) z b → (fun x1 x2 ↦ (fun x ↦ f (M x) x) x1 > x2) z b

Tactic:
h

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
s : Set α
ι : Type u_4
f : ι → α → β
inst✝ : Preorder β
I : Set ι
hfy : ∀ i ∈ I, LowerSemicontinuousOn (f i) s
M : α → ι
M_mem : ∀ x ∈ s, M x ∈ I
M_max : ∀ x ∈ s, IsMaxOn (fun y ↦ f y x) I (M x)
x : α
hx : x ∈ s
b : β
hb : (fun x ↦ f (M x) x) x > b
z : α
hz : z ∈ s
h : f (M x) z > b
⊢ (fun x ↦ f (M x) x) z > b
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : Set α → ℝ≥0∞ := fun s ↦ ⨅ f, ⨅ (_ : s ⊆ ⋃ i, f i), ∑' (i : ℕ), m (f i)
s : ℕ → Set α
x✝ : Pairwise (Disjoint on s)
ε : ℝ≥0
hε : 0 < ε
hb : ∑' (i : ℕ), μ (s i) < ∞
ε' : ℕ → ℝ≥0
hε' : ∀ (i : ℕ), 0 < ε' i
hl : ∑' (i : ℕ), ↑(ε' i) < ↑ε
⊢ μ (⋃ i, s i) ≤ ∑' (i : ℕ), μ (s i) + ↑ε

Tactic:
← hl

Goal state after:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : Set α → ℝ≥0∞ := fun s ↦ ⨅ f, ⨅ (_ : s ⊆ ⋃ i, f i), ∑' (i : ℕ), m (f i)
s : ℕ → Set α
x✝ : Pairwise (Disjoint on s)
ε : ℝ≥0
hε : 0 < ε
hb : ∑' (i : ℕ), μ (s i) < ∞
ε' : ℕ → ℝ≥0
hε' : ∀ (i : ℕ), 0 < ε' i
hl : ∑' (i : ℕ), ↑(ε' i) < ↑ε
⊢ μ (⋃ i, s i) ≤ ∑' (i : ℕ), μ (s i) + ∑' (i : ℕ), ↑(ε' i)
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case mp
α : Type u_1
inst✝³ : TopologicalSpace α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst✝³] s
hf : ∀ x ∈ s, ∀ y < f x, ∀ᶠ (x : α) in 𝓝 x, x ∈ s → y < f x
x : α
y : γ
⊢ ((x, y).1 ∈ s → (x, y).2 < f (x, y).1) → ∀ᶠ (a : α × γ) in 𝓝 (x, y), a.1 ∈ s → a.2 < f a.1

Tactic:
h

Goal state after:
case mp
α : Type u_1
inst✝³ : TopologicalSpace α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst✝³] s
hf : ∀ x ∈ s, ∀ y < f x, ∀ᶠ (x : α) in 𝓝 x, x ∈ s → y < f x
x : α
y : γ
h : (x, y).1 ∈ s → (x, y).2 < f (x, y).1
⊢ ∀ᶠ (a : α × γ) in 𝓝 (x, y), a.1 ∈ s → a.2 < f a.1
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: α : Type u_3
f : Filter α
u v : α → EReal
h : limsup u f = ⊥
h' : limsup v f ≠ ⊤
⊢ limsup u f ≠ ⊤ ∨ limsup v f ≠ ⊥

Tactic:
h

Goal state after:
α : Type u_3
f : Filter α
u v : α → EReal
h : limsup u f = ⊥
h' : limsup v f ≠ ⊤
⊢ ⊥ ≠ ⊤ ∨ limsup v f ≠ ⊥
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s t : Set α
h : ∀ (u : Set α), (s ∩ u).Nonempty → (t ∩ u).Nonempty → m u = ∞
f : ℕ → Set α
hf : s ∪ t ⊆ ⋃ i, f i
μ : OuterMeasure α := OuterMeasure.ofFunction m m_empty
⊢ μ s + μ t ≤ ∑' (i : ℕ), m (f i)

Tactic:
rcases Classical.em (∃ i, (s ∩ f i).Nonempty ∧ (t ∩ f i).Nonempty) with (⟨i, hs, ht⟩ | he)

Goal state after:
case inl
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s t : Set α
h : ∀ (u : Set α), (s ∩ u).Nonempty → (t ∩ u).Nonempty → m u = ∞
f : ℕ → Set α
hf : s ∪ t ⊆ ⋃ i, f i
μ : OuterMeasure α := OuterMeasure.ofFunction m m_empty
i : ℕ
hs : (s ∩ f i).Nonempty
ht : (t ∩ f i).Nonempty
⊢ μ s + μ t ≤ ∑' (i : ℕ), m (f i)

case inr
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s t : Set α
h : ∀ (u : Set α), (s ∩ u).Nonempty → (t ∩ u).Nonempty → m u = ∞
f : ℕ → Set α
hf : s ∪ t ⊆ ⋃ i, f i
μ : OuterMeasure α := OuterMeasure.ofFunction m m_empty
he : ¬∃ i, (s ∩ f i).Nonempty ∧ (t ∩ f i).Nonempty
⊢ μ s + μ t ≤ ∑' (i : ℕ), m (f i)
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case intro
ε : ℝ≥0
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
val✝ : Encodable ι
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∃ c, HasSum ε' c ∧ c < ε

Tactic:
obtain ⟨a, a0, aε⟩ := exists_between (pos_iff_ne_zero.2 hε)

Goal state after:
case intro
ε : ℝ≥0
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
val✝ : Encodable ι
a : ℝ≥0
a0 : 0 < a
aε : a < ε
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∃ c, HasSum ε' c ∧ c < ε
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
ι : Sort u_4
p : ι → Set (Set α)
hp_pi : ∀ (n : ι), IsPiSystem (p n)
hp_directed : Directed (fun x1 x2 ↦ x1 ⊆ x2) p
t1 : Set α
ht1 : t1 ∈ ⋃ n, p n
t2 : Set α
ht2 : t2 ∈ ⋃ n, p n
⊢ (t1 ∩ t2).Nonempty → t1 ∩ t2 ∈ ⋃ n, p n

Tactic:
h

Goal state after:
α : Type u_3
ι : Sort u_4
p : ι → Set (Set α)
hp_pi : ∀ (n : ι), IsPiSystem (p n)
hp_directed : Directed (fun x1 x2 ↦ x1 ⊆ x2) p
t1 : Set α
ht1 : t1 ∈ ⋃ n, p n
t2 : Set α
ht2 : t2 ∈ ⋃ n, p n
h : (t1 ∩ t2).Nonempty
⊢ t1 ∩ t2 ∈ ⋃ n, p n
Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory

Goal state before:
pp: α : Type u
m : OuterMeasure α
ι : Type u_1
s : ι → Set α
t : Set ι
ht : t.Finite
h : ∀ i ∈ t, m.IsCaratheodory (s i)
⊢ m.IsCaratheodory (⋃ i ∈ t, s i)

Tactic:
lift t to Finset ι using ht

Goal state after:
α : Type u
m : OuterMeasure α
ι : Type u_1
s : ι → Set α
t : Finset ι
h : ∀ i ∈ ↑t, m.IsCaratheodory (s i)
⊢ m.IsCaratheodory (⋃ i ∈ ↑t, s i)
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_1
S : Set (Set α)
h_S : IsPiSystem S
x : Set α
h : x ∈ generatePiSystem S
⊢ x ∈ S

Tactic:
induction h with

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

Goal state before:
pp: α : Type u_1
s : Set α
x✝ : MeasurableSet s
t : Set α
ht : t.Nonempty
⊢ ⊤ (t ∩ s) + ⊤ (t \ s) ≤ ⊤ t

Tactic:
simp only [ht, top_apply, le_top]

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
d : DynkinSystem α
s₁ s₂ : Set α
h₁ : d.Has s₁
h₂ : d.Has s₂
h : Disjoint s₁ s₂
⊢ d.Has (s₁ ∪ s₂)

Tactic:
rw [union_eq_iUnion]
  exact d.has_iUnion (pairwise_disjoint_on_bool.2 h) (Bool.forall_bool.2 ⟨h₂, h₁⟩)

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
f : ℕ → Set α
⊢ ∀ (hm : ∀ (i : ℕ), MeasurableSet (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯

Tactic:
h

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
f : ℕ → Set α
h : ∀ (i : ℕ), MeasurableSet (f i)
⊢ m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet (_root_.id '' s)

Tactic:
by rwa [image_id]

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

Goal state before:
pp: case refine_1
α✝ : 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 γ
⊢ Measurable
    (((fun a ↦ (Equiv.sumProdDistrib α β γ) ↑a) ∘ ⇑(Set.prod (range Sum.inl) univ).symm) ∘
      ⇑(Set.rangeInl.prodCongr (Set.univ γ)).symm)

Tactic:
exact measurable_inl

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
m₁ m₂ m₃ : OuterMeasure α
op : ℝ≥0∞ → ℝ≥0∞ → ℝ≥0∞
h : ∀ (s : Set α), m₁ s = op (m₂ s) (m₃ s)
s t : Set α
_hst : s ⊆ t
_ht : MeasurableSet t
htm : m₁ t = m₁.trim s ∧ m₂ t = m₂.trim s ∧ m₃ t = m₃.trim s ∧ ∀ (i : Fin 0), (![] i) t = (![] i).trim s
⊢ m₁ t = op (m₂ t) (m₃ t)

Tactic:
h

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
m₁ m₂ m₃ : OuterMeasure α
op : ℝ≥0∞ → ℝ≥0∞ → ℝ≥0∞
h : ∀ (s : Set α), m₁ s = op (m₂ s) (m₃ s)
s t : Set α
_hst : s ⊆ t
_ht : MeasurableSet t
htm : m₁ t = m₁.trim s ∧ m₂ t = m₂.trim s ∧ m₃ t = m₃.trim s ∧ ∀ (i : Fin 0), (![] i) t = (![] i).trim s
⊢ op (m₂ t) (m₃ t) = op (m₂ t) (m₃ t)
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
⊢ α ≃ᵐ β

Tactic:
let F : Set α → Set α := fun A => (g '' (f '' A)ᶜ)ᶜ

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)ᶜ)ᶜ
⊢ α ≃ᵐ β
Module: Mathlib.MeasureTheory.Measure.NullMeasurable

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
h : μ s = μ t
hfin : μ (s ∩ t) ≠ ∞
⊢ μ s = μ t

Tactic:
h

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
h : μ s = μ t
hfin : μ (s ∩ t) ≠ ∞
⊢ μ t = μ t
Module: Mathlib.MeasureTheory.Measure.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
⊢ map f μ = map f ν → μ = ν

Tactic:
h

Goal state after:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
h : map f μ = map f ν
⊢ μ = ν
Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving

Goal state before:
pp: case succ
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → α
hf : QuasiMeasurePreserving f μ μ
hs : f ⁻¹' s =ᵐ[μ] s
k : ℕ
ih : f^[k] ⁻¹' s =ᵐ[μ] s
⊢ f^[k + 1] ⁻¹' s =ᵐ[μ] s

Tactic:
rw [iterate_succ, preimage_comp]
    exact EventuallyEq.trans (hf.preimage_ae_eq ih) hs

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

Goal state before:
pp: case pos.mp
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 : comap Subtype.val (𝓝[<] b) = atTop
a : X
ha : a < b
this : Subtype.val ⁻¹' Ioo a b ∈ comap Subtype.val (𝓝[<] b)
⊢ (s ∩ Ioo a b).Nonempty

Tactic:
h

Goal state after:
case pos.mp
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 : comap Subtype.val (𝓝[<] b) = atTop
a : X
ha : a < b
this : Subtype.val ⁻¹' Ioo a b ∈ atTop
⊢ (s ∩ Ioo a b).Nonempty
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst✝ : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), μ (t i) ≤ μ (s i)
⊢ μ (⋃ i, s i) = μ (⋃ i, t i)

Tactic:
by
  refine le_antisymm (by gcongr; apply hsub) ?_
  by_cases! htop : ∃ i, μ (t i) = ∞
  · rcases htop with ⟨i, hi⟩
    calc
      μ (⋃ i, t i) ≤ ∞ := le_top
      _ ≤ μ (s i) := hi ▸ h_le i
      _ ≤ μ (⋃ i, s i) := measure_mono <| subset_iUnion _ _
  set M := toMeasurable μ
  have H : ∀ b, (M (t b) ∩ M (⋃ b, s b) : Set α) =ᵐ[μ] M (t b) := by
    refine fun b => ae_eq_of_subset_of_measure_ge inter_subset_left ?_ ?_ ?_
    · calc
        μ (M (t b)) = μ (t b) := measure_toMeasurable _
        _ ≤ μ (s b) := h_le b
        _ ≤ μ (M (t b) ∩ M (⋃ b, s b)) :=
          measure_mono <|
            subset_inter ((hsub b).trans <| subset_toMeasurable _ _)
              ((subset_iUnion _ _).trans <| subset_toMeasurable _ _)
    · measurability
    · rw [measure_toMeasurable]
      exact htop b
  calc
    μ (⋃ b, t b) ≤ μ (⋃ b, M (t b)) := measure_mono (iUnion_mono fun b => subset_toMeasurable _ _)
    _ = μ (⋃ b, M (t b) ∩ M (⋃ b, s b)) :=
      measure_congr (Filter.EventuallyEq.countable_iUnion H).symm
    _ ≤ μ (M (⋃ b, s b)) := measure_mono (iUnion_subset fun b => inter_subset_right)
    _ = μ (⋃ b, s b) := measure_toMeasurable _

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
⊢ (∀ (n : ℕ), μ (s ∩ spanningSets μ n) ≤ 0) ↔ μ s ≤ 0

Tactic:
nonpos_iff_eq_zero,

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
⊢ (∀ (n : ℕ), μ (s ∩ spanningSets μ n) ≤ 0) ↔ μ s = 0
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

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

Tactic:
rw [map_of_not_aemeasurable hf]
    exact MeasureTheory.isFiniteMeasureZero

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hs' : μ s ≠ ∞
ht' : μ t ≠ ∞
⊢ |μ.real s - μ.real t| ≤ μ.real (s ∆ t)

Tactic:
by
  simp only [Measure.real]
  have hst : μ (s \ t) ≠ ∞ := (measure_lt_top_of_subset sdiff_subset hs').ne
  have hts : μ (t \ s) ≠ ∞ := (measure_lt_top_of_subset sdiff_subset ht').ne
  suffices (μ s).toReal - (μ t).toReal = (μ (s \ t)).toReal - (μ (t \ s)).toReal by
    rw [this, measure_symmDiff_eq hs ht, ENNReal.toReal_add hst hts]
    convert! abs_sub (μ (s \ t)).toReal (μ (t \ s)).toReal <;> simp
  rw [measure_sdiff' s ht ht', measure_sdiff' t hs hs',
    ENNReal.toReal_sub_of_le measure_le_measure_union_right (by finiteness),
    ENNReal.toReal_sub_of_le measure_le_measure_union_right (by finiteness),
    union_comm t s]
  abel

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
h_ss : sᶜ ⊆ {a | (if a ∈ s then f a else g a) = g a}
⊢ {x | (fun x ↦ (fun x ↦ if x ∈ s then f x else g x) x = g x) x}ᶜ ⊆ sᶜᶜ

Tactic:
rwa [Set.compl_subset_compl]

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

Goal state before:
pp: α : Type u_8
ι : Type u_9
x✝ : MeasurableSpace α
μ : Measure α
inst✝¹ : Countable ι
inst✝ : Preorder ι
f : ι → Set α
hm : ∀ (i : ι), NullMeasurableSet (f i) μ
hf : ∃ i, μ (f i) ≠ ∞
⊢ Tendsto (fun i ↦ μ (⋂ j, ⋂ (_ : j ≤ i), f j)) atTop (𝓝 (μ (⋂ i, f i)))

Tactic:
by
  refine .of_neBot_imp fun hne ↦ ?_
  cases atTop_neBot_iff.mp hne
  rw [measure_iInter_eq_iInf_measure_iInter_le hm hf]
  exact tendsto_atTop_iInf
    fun i j hij ↦ measure_mono <| biInter_subset_biInter_left fun k hki ↦ le_trans hki hij

Goal state after:
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) ∘ Subtype.val) atBot (𝓝 (μ (⋂ r, ⋂ (_ : r > a), s r)))

Tactic:
← mem_Ioi,

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 (𝓝 (μ (⋂ r ∈ Ioi a, s r)))
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h : μ t = μ u
htu : t ⊆ u
ht_ne_top : μ t ≠ ∞
⊢ μ (t ∩ s) = μ (u ∩ s)

Tactic:
h

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h : μ t = μ u
htu : t ⊆ u
ht_ne_top : μ u ≠ ∞
⊢ μ (t ∩ s) = μ (u ∩ s)
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
ms : MeasurableSpace α
μ : OuterMeasure α
h : ms ≤ μ.caratheodory
⊢ μ = 0 → μ.toMeasure h = 0

Tactic:
rintro rfl; simp

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
R : Type u_8
inst✝⁴ : Semiring R
inst✝³ : IsDomain R
inst✝² : Module R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : Module.IsTorsionFree R ℝ≥0∞
c : R
p : α → Prop
hc : c ≠ 0
μ : Measure α
⊢ (∀ᵐ (x : α) ∂c • μ, p x) ↔ ∀ᵐ (x : α) ∂μ, p x

Tactic:
simp [ae_iff, hc]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
c : ℝ≥0∞
p : α → Prop
hc : c ≠ 0
μ : Measure α
⊢ (∀ᵐ (x : α) ∂c • μ, p x) ↔ ∀ᵐ (x : α) ∂μ, p x

Tactic:
simp [ae_iff, hc]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ₁ μ₂ : Measure α
h : ∀ (s : Set α), MeasurableSet s → s.Nonempty → μ₁ s ≤ μ₂ s
s : Set α
hs : MeasurableSet s
⊢ s = ∅ → μ₁ s ≤ μ₂ s

Tactic:
rintro rfl; simp

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
m : Set (Measure α)
s : Set α
hs : MeasurableSet s
t : Set α
μ : Measure α
hμ : μ ∈ m
u : Set α
htu : t ⊆ u
_hu : MeasurableSet u
⊢ (⨅ μ ∈ toOuterMeasure '' m, μ (t ∩ s)) + ⨅ μ ∈ toOuterMeasure '' m, μ (t \ s) ≤ μ u

Tactic:
have hm : ∀ {s t}, s ⊆ t → OuterMeasure.sInfGen (toOuterMeasure '' m) s ≤ μ t := by
    intro s t hst
    rw [OuterMeasure.sInfGen_def, iInf_image]
    exact iInf₂_le_of_le μ hμ <| measure_mono hst

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
m : Set (Measure α)
s : Set α
hs : MeasurableSet s
t : Set α
μ : Measure α
hμ : μ ∈ m
u : Set α
htu : t ⊆ u
_hu : MeasurableSet u
hm : ∀ {s t : Set α}, s ⊆ t → OuterMeasure.sInfGen (toOuterMeasure '' m) s ≤ μ t
⊢ (⨅ μ ∈ toOuterMeasure '' m, μ (t ∩ s)) + ⨅ μ ∈ toOuterMeasure '' m, μ (t \ s) ≤ μ u
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
inst✝ : SigmaFinite μ
h : ν₁ = ν₂
⊢ μ + ν₁ = μ + ν₂

Tactic:
h

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
inst✝ : SigmaFinite μ
h : ν₁ = ν₂
⊢ μ + ν₂ = μ + ν₂