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

Goal state before:
pp: ι : Type u_2
α : ι → Type u_1
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
hC_univ : ∀ (i : ι), univ ∈ C i
s₁ : Finset ι
t₁ : (i : ι) → Set (α i)
h₁ : t₁ ∈ univ.pi C
s₂ : Finset ι
t₂ : (i : ι) → Set (α i)
h₂ : t₂ ∈ univ.pi C
t₁' : (i : ι) → Set (α i) := s₁.piecewise t₁ fun i ↦ univ
t₂' : (i : ι) → Set (α i) := s₂.piecewise t₂ fun i ↦ univ
h1 : ∀ i ∈ ↑s₁, t₁ i = t₁' i
h1' : ∀ i ∉ ↑s₁, t₁' i = univ
h2 : ∀ i ∈ ↑s₂, t₂ i = t₂' i
h2' : ∀ i ∉ ↑s₂, t₂' i = univ
i : ι
f : (i : ι) → α i
hf : (∀ i ∈ ↑s₁, f i ∈ t₁' i) ∧ ∀ i ∈ ↑s₂, f i ∈ t₂' i
⊢ (t₁' i ∩ t₂' i).Nonempty

Tactic:
refine ⟨f i, ⟨?_, ?_⟩⟩

Goal state after:
case refine_1
ι : Type u_2
α : ι → Type u_1
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
hC_univ : ∀ (i : ι), univ ∈ C i
s₁ : Finset ι
t₁ : (i : ι) → Set (α i)
h₁ : t₁ ∈ univ.pi C
s₂ : Finset ι
t₂ : (i : ι) → Set (α i)
h₂ : t₂ ∈ univ.pi C
t₁' : (i : ι) → Set (α i) := s₁.piecewise t₁ fun i ↦ univ
t₂' : (i : ι) → Set (α i) := s₂.piecewise t₂ fun i ↦ univ
h1 : ∀ i ∈ ↑s₁, t₁ i = t₁' i
h1' : ∀ i ∉ ↑s₁, t₁' i = univ
h2 : ∀ i ∈ ↑s₂, t₂ i = t₂' i
h2' : ∀ i ∉ ↑s₂, t₂' i = univ
i : ι
f : (i : ι) → α i
hf : (∀ i ∈ ↑s₁, f i ∈ t₁' i) ∧ ∀ i ∈ ↑s₂, f i ∈ t₂' i
⊢ f i ∈ t₁' i

case refine_2
ι : Type u_2
α : ι → Type u_1
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
hC_univ : ∀ (i : ι), univ ∈ C i
s₁ : Finset ι
t₁ : (i : ι) → Set (α i)
h₁ : t₁ ∈ univ.pi C
s₂ : Finset ι
t₂ : (i : ι) → Set (α i)
h₂ : t₂ ∈ univ.pi C
t₁' : (i : ι) → Set (α i) := s₁.piecewise t₁ fun i ↦ univ
t₂' : (i : ι) → Set (α i) := s₂.piecewise t₂ fun i ↦ univ
h1 : ∀ i ∈ ↑s₁, t₁ i = t₁' i
h1' : ∀ i ∉ ↑s₁, t₁' i = univ
h2 : ∀ i ∈ ↑s₂, t₂ i = t₂' i
h2' : ∀ i ∉ ↑s₂, t₂' i = univ
i : ι
f : (i : ι) → α i
hf : (∀ i ∈ ↑s₁, f i ∈ t₁' i) ∧ ∀ i ∈ ↑s₂, f i ∈ t₂' i
⊢ f i ∈ t₂' i
Module: Mathlib.MeasureTheory.Constructions.Projective

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)
h : IsEmpty ((i : ι) → α i)
hP : IsProjectiveMeasureFamily P
I : Finset ι
i : ι
hi : IsEmpty (α i)
⊢ Measure.map (Finset.restrict₂ ⋯) (P (insert i I)) = 0

Tactic:
have : IsEmpty (Π j : ↑(insert i I), α j) := by simp [hi]

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)
h : IsEmpty ((i : ι) → α i)
hP : IsProjectiveMeasureFamily P
I : Finset ι
i : ι
hi : IsEmpty (α i)
this : IsEmpty ((j : ↥(insert i I)) → α ↑j)
⊢ Measure.map (Finset.restrict₂ ⋯) (P (insert i I)) = 0
Module: Mathlib.LinearAlgebra.Transvection.Generation

Goal state before:
pp: K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
n✝ : ℕ
e : V ≃ₗ[K] V
he : e.fixedReduce = 1
n : ℕ
h : finrank K (V ⧸ (↑e).fixedSubmodule) = n + 2
hind :
  ∀ {e : V ≃ₗ[K] V},
    e.fixedReduce = 1 → finrank K (V ⧸ (↑e).fixedSubmodule) = n + 1 → e ∈ transvections K V ^ n * dilatransvections K V
⊢ ∃ x ∈ transvections K V, ∃ y, (∃ x ∈ transvections K V ^ n, ∃ y_1 ∈ dilatransvections K V, x * y_1 = y) ∧ x * y = e

Tactic:
have : ∃ f : Dual K V, ∃ v : V, e.fixedSubmodule ≤ ker f ∧ f v = 1 := by
        have : ∃ u : V, u ∉ e.fixedSubmodule := by
          by_contra! he
          rw [← Submodule.eq_top_iff'] at he
          rw [he, ← Nat.add_left_inj, Submodule.finrank_quotient_add_finrank, finrank_top] at h
          simp at h
        obtain ⟨u, hu⟩ := this
        obtain ⟨f, hfu, hf⟩ := Submodule.exists_dual_map_eq_bot_of_notMem hu inferInstance
        let v := (f u)⁻¹ • u
        have hv : f v = 1 := by simp [v, inv_mul_cancel₀ hfu]
        exact ⟨f, v, by rwa [LinearMap.le_ker_iff_map], hv⟩

Goal state after:
K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
n✝ : ℕ
e : V ≃ₗ[K] V
he : e.fixedReduce = 1
n : ℕ
h : finrank K (V ⧸ (↑e).fixedSubmodule) = n + 2
hind :
  ∀ {e : V ≃ₗ[K] V},
    e.fixedReduce = 1 → finrank K (V ⧸ (↑e).fixedSubmodule) = n + 1 → e ∈ transvections K V ^ n * dilatransvections K V
this : ∃ f v, (↑e).fixedSubmodule ≤ ker f ∧ f v = 1
⊢ ∃ x ∈ transvections K V, ∃ y, (∃ x ∈ transvections K V ^ n, ∃ y_1 ∈ dilatransvections K V, x * y_1 = y) ∧ x * y = e
Module: Mathlib.MeasureTheory.Constructions.Projective

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)
I J : Finset ι
hP : IsProjectiveMeasureFamily P
S : Set ((i : ↥I) → α ↑i)
T : Set ((i : ↥J) → α ↑i)
hT : MeasurableSet T
h_eq : cylinder I S = cylinder J T
hJI : J ⊆ I
h : IsEmpty ((i : ι) → α i)
this : ∀ (I : Finset ι), P I = 0
⊢ (P I) S = (P J) T

Tactic:
simp [this]

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: case a
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
S : Set ((i : ι) → α i)
hS : S ∈ measurableCylinders α
⊢ MeasurableSet S

Tactic:
obtain ⟨s, S, hSm, rfl⟩ := (mem_measurableCylinders _).mp hS

Goal state after:
case a
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
s : Finset ι
S : Set ((i : ↥s) → α ↑i)
hSm : MeasurableSet S
hS : cylinder s S ∈ measurableCylinders α
⊢ MeasurableSet (cylinder s S)
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
ι : Type u_3
a : Finset ι
f : ι → Set α
hf : ∀ i ∈ a, f i ∈ C
h_dis : (↑a).PairwiseDisjoint f
h_mem : ⋃ i ∈ a, f i ∈ C
A : ⋃ i ∈ a, f i = ⋃₀ ↑(Finset.image f a)
⊢ ∑ u ∈ Finset.image f a, m u = ∑ i ∈ a, m (f i)

Tactic:
rw [sum_image_of_pairwise_eq_zero]

Goal state after:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
ι : Type u_3
a : Finset ι
f : ι → Set α
hf : ∀ i ∈ a, f i ∈ C
h_dis : (↑a).PairwiseDisjoint f
h_mem : ⋃ i ∈ a, f i ∈ C
A : ⋃ i ∈ a, f i = ⋃₀ ↑(Finset.image f a)
⊢ (↑a).Pairwise fun i j ↦ f i = f j → m (f i) = 0
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: case e'_3
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ i, ![s, t] i
⊢ m s + m t = ∑ i, m (![s, t] i)

pp: case convert_1
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ i, ![s, t] i
i : Fin (Nat.succ 0).succ
⊢ ![s, t] i ∈ C

pp: case convert_2
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ i, ![s, t] i
i j : Fin (Nat.succ 0).succ
hij : i ≠ j
⊢ (Disjoint on ![s, t]) i j

pp: case convert_3
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ i, ![s, t] i
⊢ ⋃ i, ![s, t] i ∈ C

Tactic:
· simp [Fin.univ_castSuccEmb, add_comm]

Goal state after:
case convert_1
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ i, ![s, t] i
i : Fin (Nat.succ 0).succ
⊢ ![s, t] i ∈ C

case convert_2
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ i, ![s, t] i
i j : Fin (Nat.succ 0).succ
hij : i ≠ j
⊢ (Disjoint on ![s, t]) i j

case convert_3
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ i, ![s, t] i
⊢ ⋃ i, ![s, t] i ∈ C
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
hC : IsSetSemiring C
m : AddContent G C
s : Set α
hs : s ∈ C
this : m.supClosureFun s = ∑ t ∈ {s}, m t
⊢ m.supClosureFun s = m s

Tactic:
simp [this]

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

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : OrderTop ι
this : interior {⊤} = {⊤}
⊢ {⊤} \ interior {⊤} = ∅

Tactic:
simp [this]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
E : Set α
ε : ℝ
hε : 0 < ε
⊢ ∃ δ,
    ∃ (_ : 0 < δ),
      ∀ (i : ι) (s : Set α),
        MeasurableSet s →
          μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator ((fun i ↦ E.indicator (f i)) i)) p μ ≤ ENNReal.ofReal ε

Tactic:
obtain ⟨δ, hδ_pos, hε⟩ := hf hε
  refine ⟨δ, hδ_pos, fun i s hs hμs ↦ ?_⟩
  calc
    eLpNorm (s.indicator (E.indicator (f i))) p μ
      = eLpNorm (E.indicator (s.indicator (f i))) p μ := by
      simp only [indicator_indicator, inter_comm]
    _ ≤ eLpNorm (s.indicator (f i)) p μ := eLpNorm_indicator_le _
    _ ≤ ENNReal.ofReal ε := hε _ _ hs hμs

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case mpr
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v w : VectorMeasure α M
⊢ (∀ (i : Set α), MeasurableSet i → v i = w i) → ∀ (x : Set α), v x = w x

Tactic:
intro h i

Goal state after:
case mpr
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v w : VectorMeasure α M
h : ∀ (i : Set α), MeasurableSet i → v i = w i
i : Set α
⊢ v i = w i
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
A B : Set α
h : Disjoint A B
hA₁ : MeasurableSet A
hB₁ : MeasurableSet B
hA₂ : 0 ≤ s A
hB₂ : 0 ≤ s B
hAB : s A + s B = 0
⊢ s A = 0

Tactic:
linarith

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
A B : Set α
h : Disjoint A B
hA₁ : MeasurableSet A
hB₁ : MeasurableSet B
hA₂ : s A ≤ 0
hB₂ : s B ≤ 0
hAB : s A + s B = 0
⊢ s A = 0

Tactic:
linarith

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_4
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
r : R
v : VectorMeasure α M
⊢ (r • ⇑v) ∅ = 0

Tactic:
by rw [Pi.smul_apply, empty, smul_zero]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : M ≤ 0
s : Set α
x✝¹ : MeasurableSet s
x✝ : μ s ≤ ENNReal.ofReal 1
⊢ f = 0

Tactic:
ext x
      rw [Pi.zero_apply, ← norm_le_zero_iff]
      exact (lt_of_lt_of_le (hf x) hM).le

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
s : Set α
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
⊢ μ.real (t ∩ s) = (μ.restrict s).real t

Tactic:
measureReal_restrict_apply ht

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
s : Set α
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
⊢ μ.real (t ∩ s) = μ.real (t ∩ s)
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : 0 ≤[u] s
hw₁ : s w = 0
hw₂ : w ⊆ u
hwt : v ⊆ w
this : s v + s (w \ v) = 0
h₁ : 0 ≤ s v
h₂ : 0 ≤ s (w \ v)
⊢ s v = 0

Tactic:
linarith

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: case left
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ u → 0 j ≤ s j
hsv : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ v → 0 j ≤ s j
hs : s (u \ v) + s (v \ u) = 0
a : 0 ≤ s (u \ v)
b : 0 ≤ s (v \ u)
⊢ s (u \ v) = 0

Tactic:
linarith

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: case right
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ u → 0 j ≤ s j
hsv : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ v → 0 j ≤ s j
hs : s (u \ v) + s (v \ u) = 0
a : 0 ≤ s (u \ v)
b : 0 ≤ s (v \ u)
⊢ s (v \ u) = 0

Tactic:
linarith

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case refine_1
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
s : Set α
hs : MeasurableSet s
h₁ : ∀ t ⊆ s, MeasurableSet t → v t = 0
h₂ : ∀ t ⊆ sᶜ, MeasurableSet t → w t = 0
t : Set α
hst : t ⊆ s
⊢ v t = 0

Tactic:
by_cases ht : MeasurableSet t

Goal state after:
case pos
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
s : Set α
hs : MeasurableSet s
h₁ : ∀ t ⊆ s, MeasurableSet t → v t = 0
h₂ : ∀ t ⊆ sᶜ, MeasurableSet t → w t = 0
t : Set α
hst : t ⊆ s
ht : MeasurableSet t
⊢ v t = 0

case neg
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
s : Set α
hs : MeasurableSet s
h₁ : ∀ t ⊆ s, MeasurableSet t → v t = 0
h₂ : ∀ t ⊆ sᶜ, MeasurableSet t → w t = 0
t : Set α
hst : t ⊆ s
ht : ¬MeasurableSet t
⊢ v t = 0
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case refine_2
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
s : Set α
hs : MeasurableSet s
h₁ : ∀ t ⊆ s, MeasurableSet t → v t = 0
h₂ : ∀ t ⊆ sᶜ, MeasurableSet t → w t = 0
t : Set α
hst : t ⊆ sᶜ
⊢ w t = 0

Tactic:
by_cases ht : MeasurableSet t

Goal state after:
case pos
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
s : Set α
hs : MeasurableSet s
h₁ : ∀ t ⊆ s, MeasurableSet t → v t = 0
h₂ : ∀ t ⊆ sᶜ, MeasurableSet t → w t = 0
t : Set α
hst : t ⊆ sᶜ
ht : MeasurableSet t
⊢ w t = 0

case neg
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
s : Set α
hs : MeasurableSet s
h₁ : ∀ t ⊆ s, MeasurableSet t → v t = 0
h₂ : ∀ t ⊆ sᶜ, MeasurableSet t → w t = 0
t : Set α
hst : t ⊆ sᶜ
ht : ¬MeasurableSet t
⊢ w t = 0
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ≥0
⊢ (r • s).toJordanDecomposition.toSignedMeasure = (r • s.toJordanDecomposition).toSignedMeasure

Tactic:
simp [toSignedMeasure_smul]

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ s ≤[B] 0} ∧ s (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), s ≤[B n] 0
A : Set α := ⋃ n, B n
hA : A = ⋃ n, B n
hA₁ : MeasurableSet A
hA₂ : s ≤[A] 0
hA₃ : s A = sInf s.measureOfNegatives
C : Set α
a✝ : MeasurableSet C
hC₁ : C ⊆ Aᶜ
hC₂ : s C < 0 C
D : Set α
hD₁ : MeasurableSet D
hD : D ⊆ C
hD₂ : s ≤[D] 0
hD₃ : s D < 0
⊢ s A + s D < s A

Tactic:
linarith

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
⊢ Measure α

Tactic:
refine Measure.ofMeasurable (s.toMeasureOfZeroLE' i hi₂) ?_ ?_
  · simp_rw [toMeasureOfZeroLE', s.restrict_apply hi₁ MeasurableSet.empty, Set.empty_inter i,
      s.empty]
    rfl
  · intro f hf₁ hf₂
    have h₁ : ∀ n, MeasurableSet (i ∩ f n) := fun n => hi₁.inter (hf₁ n)
    have h₂ : Pairwise (Disjoint on fun n : ℕ => i ∩ f n) := by
      intro n m hnm
      exact ((hf₂ hnm).inf_left' i).inf_right' i
    simp only [toMeasureOfZeroLE', s.restrict_apply hi₁ (MeasurableSet.iUnion hf₁), Set.inter_comm,
      Set.inter_iUnion, s.of_disjoint_iUnion h₁ h₂]
    have h : ∀ n, 0 ≤ s (i ∩ f n) := fun n =>
      s.nonneg_of_zero_le_restrict (s.zero_le_restrict_subset hi₁ Set.inter_subset_left hi₂)
    rw [NNReal.coe_tsum_of_nonneg h, ENNReal.coe_tsum]
    · refine tsum_congr fun n => ?_
      simp_rw [s.restrict_apply hi₁ (hf₁ n), Set.inter_comm]
    · exact (NNReal.summable_mk h).2 (s.m_iUnion h₁ h₂).summable

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
htμ' : t ⟂ᵥ μ.toENNRealVectorMeasure
⊢ s.HaveLebesgueDecomposition μ

Tactic:
mutuallySingular_ennreal_iff

Goal state after:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
htμ : t.totalVariation ⟂ₘ μ.toENNRealVectorMeasure.ennrealToMeasure
hadd : s = t + μ.withDensityᵥ f
htμ' : t ⟂ᵥ μ.toENNRealVectorMeasure
⊢ s.HaveLebesgueDecomposition μ
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
⊢ t = s.singularPart μ

Tactic:
have htμ' := htμ
  rw [mutuallySingular_ennreal_iff, totalVariation_mutuallySingular_iff,
    VectorMeasure.ennrealToMeasure_toENNRealVectorMeasure] at htμ
  rw [singularPart, ← t.toSignedMeasure_toJordanDecomposition,
    JordanDecomposition.toSignedMeasure]
  congr
  · have hfpos : Measurable fun x => ENNReal.ofReal (f x) := by fun_prop
    refine eq_singularPart hfpos htμ.1 ?_
    rw [toJordanDecomposition_eq_of_eq_add_withDensity hf hfi htμ' hadd]
  · have hfneg : Measurable fun x => ENNReal.ofReal (-f x) := by fun_prop
    refine eq_singularPart hfneg htμ.2 ?_
    rw [toJordanDecomposition_eq_of_eq_add_withDensity hf hfi htμ' hadd]

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

Goal state before:
pp: Ω : Type u_1
inst✝ : MeasurableSpace Ω
ν : ProbabilityMeasure Ω
⊢ ν univ ≠ 0

Tactic:
simp only [coeFn_univ, Ne, one_ne_zero, not_false_iff]

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

Goal state before:
pp: Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
s₁ s₂ : Set Ω
⊢ μ.toFiniteMeasure (s₁ ∪ s₂) ≤ μ.toFiniteMeasure s₁ + μ.toFiniteMeasure s₂

Tactic:
exact FiniteMeasure.apply_union_le _

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ
hp : 1 ≤ p
f : α → E
s : Set α
hs : MeasurableSet s
hf : Integrable (fun x ↦ ‖f x‖ ^ p) μ
⊢ p ≠ 0

Tactic:
linarith

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

Goal state before:
pp: Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : HasOuterApproxClosed Ω
inst✝ : BorelSpace Ω
μ ν : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ), ∫ (x : Ω), f x ∂↑μ = ∫ (x : Ω), f x ∂↑ν
⊢ μ = ν

Tactic:
apply ext_of_forall_lintegral_eq

Goal state after:
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : HasOuterApproxClosed Ω
inst✝ : BorelSpace Ω
μ ν : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ), ∫ (x : Ω), f x ∂↑μ = ∫ (x : Ω), f x ∂↑ν
⊢ ∀ (f : Ω →ᵇ ℝ≥0), ∫⁻ (x : Ω), ↑(f x) ∂↑μ = ∫⁻ (x : Ω), ↑(f x) ∂↑ν
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
key : μ.testAgainstNN f₂ ≤ μ.testAgainstNN f₁ + μ.mass * nndist f₂ f₁
this : ↑(μ.testAgainstNN f₂) ≤ ↑(μ.testAgainstNN f₁) + ↑μ.mass * dist f₁ f₂
⊢ -(↑μ.mass * dist f₁ f₂) ≤ ↑(μ.testAgainstNN f₁) - ↑(μ.testAgainstNN f₂)

Tactic:
linarith

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

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
key : μ.testAgainstNN f₁ ≤ μ.testAgainstNN f₂ + μ.mass * nndist f₁ f₂
this : ↑(μ.testAgainstNN f₁) ≤ ↑(μ.testAgainstNN f₂) + ↑μ.mass * dist f₁ f₂
⊢ ↑(μ.testAgainstNN f₁) - ↑(μ.testAgainstNN f₂) ≤ ↑μ.mass * dist f₁ f₂

Tactic:
linarith

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

Goal state before:
pp: Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : HasOuterApproxClosed Ω
inst✝ : BorelSpace Ω
μ ν : FiniteMeasure Ω
hμν : μ.toWeakDualBCNN = ν.toWeakDualBCNN
⊢ μ = ν

Tactic:
apply ext_of_forall_lintegral_eq

Goal state after:
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : HasOuterApproxClosed Ω
inst✝ : BorelSpace Ω
μ ν : FiniteMeasure Ω
hμν : μ.toWeakDualBCNN = ν.toWeakDualBCNN
⊢ ∀ (f : Ω →ᵇ ℝ≥0), ∫⁻ (x : Ω), ↑(f x) ∂↑μ = ∫⁻ (x : Ω), ↑(f x) ∂↑ν
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:

Tactic:
eLpNorm (f i) p μ ≤
        eLpNorm ({ x : α | ‖f i x‖₊ < C }.indicator (f i)) p μ +
          eLpNorm ({ x : α | C ≤ ‖f i x‖₊ }.indicator (f i)) p μ := by
      refine le_trans (eLpNorm_mono_enorm fun x => ?_) (eLpNorm_add_le
        (StronglyMeasurable.aestronglyMeasurable
          ((hf i).indicator ((hf i).nnnorm.measurableSet_lt stronglyMeasurable_const)))
        (StronglyMeasurable.aestronglyMeasurable
          ((hf i).indicator (stronglyMeasurable_const.measurableSet_le (hf i).nnnorm))) hp)
      rw [Pi.add_apply, Set.indicator_apply]
      split_ifs with hx
      · rw [Set.indicator_of_notMem, add_zero]
        simpa using hx
      · rw [Set.indicator_of_mem, zero_add]
        simpa using hx
    _ ≤ (C : ℝ≥0∞) * μ Set.univ ^ p.toReal⁻¹ + 1 := by
      have : ∀ᵐ x ∂μ, ‖{ x : α | ‖f i x‖₊ < C }.indicator (f i) x‖₊ ≤ C := by
        filter_upwards
        simp_rw [nnnorm_indicator_eq_indicator_nnnorm]
        exact Set.indicator_le fun x (hx : _ < _) => hx.le
      refine add_le_add (le_trans (eLpNorm_le_of_ae_bound this) ?_) (ENNReal.ofReal_one ▸ hC i)
      simp_rw [NNReal.val_eq_coe, ENNReal.ofReal_coe_nnreal, mul_comm]
      exact le_rfl
    _ = ((C : ℝ≥0∞) * μ Set.univ ^ p.toReal⁻¹ + 1 : ℝ≥0∞).toNNReal := by
      rw [ENNReal.coe_toNNReal (by finiteness)]

Goal state after: