mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ∀ (a : K), ∃ x, e.fixedReduce x ≠ a • x
n : ℕ
hind :
  ∀ {e : V ≃ₗ[K] V},
    (∀ (a : K), ∃ x, ¬e.fixedReduce x = a • x) →
      finrank K (V ⧸ (↑e).fixedSubmodule) = n + 1 → e ∈ transvections K V ^ n * dilatransvections K V
h : finrank K (V ⧸ (↑e).fixedSubmodule) = n + 2
f : Dual K V
v : V
hv : LinearIndependent K ![(↑e).fixedSubmodule.mkQ v, e.fixedReduce ((↑e).fixedSubmodule.mkQ v)]
hf : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker f
hfv : f v = 1
hv_notMem : v ∉ (↑e).fixedSubmodule
hrank : finrank K (V ⧸ (↑e).fixedSubmodule ⊔ K ∙ v) = n + 1
hn_pos : n > 0
he' : auxTransvection hf * e ∈ transvections K V ^ n * dilatransvections K V
⊢ (auxTransvection hf)⁻¹ * (auxTransvection hf * e) = e

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s✝ t : Set α
I✝ : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m✝ m' : AddContent G C
m : Set α → G
hC : IsSetRing C
m_empty : m ∅ = 0
m_add : ∀ {s t : Set α}, s ∈ C → t ∈ C → Disjoint s t → m (s ∪ t) = m s + m t
s : Set α
I : Finset (Set α)
hsI : s ∉ I
h : ↑I ⊆ C → (↑I).PairwiseDisjoint id → ⋃₀ ↑I ∈ C → m (⋃₀ ↑I) = ∑ u ∈ I, m u
h_ss : s ∈ C ∧ ↑I ⊆ C
h_dis : (↑I).PairwiseDisjoint id ∧ ∀ j ∈ ↑I, Disjoint (id s) (id j)
h_mem : ⋃₀ insert s ↑I ∈ C
⊢ ⋃₀ ↑I ∈ C

Tactic:
Set.sUnion_eq_biUnion

Goal state after:
α : Type u_1
C : Set (Set α)
s✝ t : Set α
I✝ : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m✝ m' : AddContent G C
m : Set α → G
hC : IsSetRing C
m_empty : m ∅ = 0
m_add : ∀ {s t : Set α}, s ∈ C → t ∈ C → Disjoint s t → m (s ∪ t) = m s + m t
s : Set α
I : Finset (Set α)
hsI : s ∉ I
h : ↑I ⊆ C → (↑I).PairwiseDisjoint id → ⋃₀ ↑I ∈ C → m (⋃₀ ↑I) = ∑ u ∈ I, m u
h_ss : s ∈ C ∧ ↑I ⊆ C
h_dis : (↑I).PairwiseDisjoint id ∧ ∀ j ∈ ↑I, Disjoint (id s) (id j)
h_mem : ⋃₀ insert s ↑I ∈ C
⊢ ⋃ i ∈ ↑I, i ∈ C
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: case empty
α : Type u_1
C : Set (Set α)
G : Type u_2
inst✝² : AddCommMonoid G
m : AddContent G C
inst✝¹ : PartialOrder G
inst✝ : CanonicallyOrderedAdd G
ι : Type u_3
hC : IsSetRing C
s : ι → Set α
hs : ∀ n ∈ ∅, s n ∈ C
⊢ m (⋃ i ∈ ∅, s i) ≤ ∑ i ∈ ∅, m (s i)

Tactic:
simp

Goal state after:
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 : ∀ (a : K), ∃ x, e.fixedReduce x ≠ a • x
n : ℕ
hind :
  ∀ {e : V ≃ₗ[K] V},
    (∀ (a : K), ∃ x, ¬e.fixedReduce x = a • x) →
      finrank K (V ⧸ (↑e).fixedSubmodule) = n + 1 → e ∈ transvections K V ^ n * dilatransvections K V
h : finrank K (V ⧸ (↑e).fixedSubmodule) = n + 2
f : Dual K V
v : V
hv : LinearIndependent K ![(↑e).fixedSubmodule.mkQ v, e.fixedReduce ((↑e).fixedSubmodule.mkQ v)]
hf : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker f
hfv : f v = 1
hv_notMem : v ∉ (↑e).fixedSubmodule
hrank : finrank K (V ⧸ (↑e).fixedSubmodule ⊔ K ∙ v) = n + 1
hn_pos : n > 0
he' : auxTransvection hf * e ∉ transvections K V ^ n * dilatransvections K V
hne_top : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ⊔ K ∙ v < ⊤
g : Dual K V
hg0 : g ≠ 0
hg2 : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ⊔ K ∙ v ≤ ker g
hg : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker (f + g)
hfgv : (f + g) v = 1
⊢ (auxTransvection hg)⁻¹ * (auxTransvection hg * e) = e

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetRing C
m_iUnion :
  ∀ (f : ℕ → Set α), (∀ (i : ℕ), f i ∈ C) → ⋃ i, f i ∈ C → Pairwise (Disjoint on f) → m (⋃ i, f i) = ∑' (i : ℕ), m (f i)
f : ℕ → Set α
⊢ (∀ (i : ℕ), f i ∈ C) → ⋃ i, f i ∈ C → m (⋃ i, f i) ≤ ∑' (i : ℕ), m (f i)

Tactic:
hf

Goal state after:
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetRing C
m_iUnion :
  ∀ (f : ℕ → Set α), (∀ (i : ℕ), f i ∈ C) → ⋃ i, f i ∈ C → Pairwise (Disjoint on f) → m (⋃ i, f i) = ∑' (i : ℕ), m (f i)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
⊢ ⋃ i, f i ∈ C → m (⋃ i, f i) ≤ ∑' (i : ℕ), m (f i)
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
hC : IsSetRing C
m : AddContent ℝ≥0∞ C
s : ℕ → Set α
hd : Pairwise (Disjoint on s)
hs : ∀ (i : ℕ), s i ∈ C
hm_iSup : ∀ ⦃s : ℕ → Set α⦄, (∀ (n : ℕ), s n ∈ C) → Monotone s → m (⋃ n, s n) = ⨆ n, m (s n)
⊢ m (⋃ i, s i) = m (⋃ i, accumulate s i)

Tactic:
simp

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

Goal state before:
pp: Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst✝ : CompleteSpace E
hm : m ≤ mΩ
f : SimpleFunc Ω F
g : Ω → E
hg : Integrable g μ
this :
  ∀ (s : Set Ω) (c : F) (f : Ω → E),
    (fun ω ↦ (B (s.indicator (Function.const Ω c) ω)) (f ω)) = s.indicator fun ω ↦ (B c) (f ω)
g₁ g₂ : SimpleFunc Ω F
x✝ : Disjoint (Function.support ⇑g₁) (Function.support ⇑g₂)
h_eq₁ : μ[fun ω ↦ (B (g₁ ω)) (g ω) | m] =ᵐ[μ] fun ω ↦ (B (g₁ ω)) (μ[g | m] ω)
h_eq₂ : μ[fun ω ↦ (B (g₂ ω)) (g ω) | m] =ᵐ[μ] fun ω ↦ (B (g₂ ω)) (μ[g | m] ω)
h_add : ⇑(g₁ + g₂) = ⇑g₁ + ⇑g₂
⊢ (fun ω ↦ (B (g₁ ω)) (μ[g | m] ω) + (B (g₂ ω)) (μ[g | m] ω)) =ᵐ[μ] fun ω ↦ (B ((g₁ + g₂) ω)) (μ[g | m] ω)

Tactic:
simp

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

Goal state before:
pp: Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
inst✝² : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst✝¹ : CompleteSpace E
hm : m ≤ mΩ
inst✝ : IsFiniteMeasure μ
f : Ω → F
g : Ω → E
hf : StronglyMeasurable f
hg : Integrable g μ
c : ℝ
hf_bound : ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖ ≤ c
fs : ℕ → SimpleFunc Ω F := hf.approxBounded c
hfs_tendsto : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun x ↦ (fs x) ω) atTop (𝓝 (f ω))
hμ : ¬μ = 0
this : (ae μ).NeBot
w✝ : Ω
h : ‖f w✝‖ ≤ c
⊢ 0 ≤ c

Tactic:
exact (norm_nonneg _).trans h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : NormedAddCommGroup β
inst✝ : MeasurableSpace α
p : ℝ≥0∞
f : ι → α → β
ε : ℝ
x✝² : 0 < ε
i : ι
s : Set α
x✝¹ : MeasurableSet s
x✝ : 0 s ≤ ENNReal.ofReal 1
⊢ eLpNorm (s.indicator (f i)) p 0 ≤ ENNReal.ofReal ε

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f ∞ μ
hmeas : StronglyMeasurable f
⊢ ∃ M, eLpNormEssSup ({x | M ≤ ↑‖f x‖₊}.indicator f) μ = 0

Tactic:
by
  have hbdd : eLpNormEssSup f μ < ∞ := hf.eLpNorm_lt_top
  refine ⟨(eLpNorm f ∞ μ + 1).toReal, ?_⟩
  rw [eLpNormEssSup_indicator_eq_eLpNormEssSup_restrict]
  · have : μ.restrict { x : α | (eLpNorm f ⊤ μ + 1).toReal ≤ ‖f x‖₊ } = 0 := by
      simp only [coe_nnnorm, eLpNorm_exponent_top, Measure.restrict_eq_zero]
      have : { x : α | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖ } ⊆
          { x : α | eLpNormEssSup f μ < ‖f x‖₊ } := by
        intro x hx
        rw [Set.mem_ofPred_eq, ← ENNReal.toReal_lt_toReal hbdd.ne ENNReal.coe_lt_top.ne,
          ENNReal.coe_toReal, coe_nnnorm]
        refine lt_of_lt_of_le ?_ hx
        rw [ENNReal.toReal_lt_toReal hbdd.ne]
        · exact ENNReal.lt_add_right hbdd.ne one_ne_zero
        · finiteness
      rw [← nonpos_iff_eq_zero]
      refine (measure_mono this).trans ?_
      have hle := enorm_ae_le_eLpNormEssSup f μ
      simp_rw [ae_iff, not_le] at hle
      exact nonpos_iff_eq_zero.2 hle
    rw [this, eLpNormEssSup_measure_zero]
  exact measurableSet_le measurable_const hmeas.nnnorm.measurable.subtype_coe

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : p = ∞
⊢ ∃ M, eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε

pp: case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ∞
⊢ ∃ M, eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε

Tactic:
· subst hp_ne_top
    obtain ⟨M, hM⟩ := hf.eLpNormEssSup_indicator_norm_ge_eq_zero hmeas
    refine ⟨M, ?_⟩
    simp only [eLpNorm_exponent_top, hM, zero_le]

Goal state after:
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ∞
⊢ ∃ M, eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
inst✝ : ContinuousSub M
v : VectorMeasure α M
s : ℕ → Set α
hm : Antitone s
hs : ∀ (i : ℕ), MeasurableSet (s i)
I : ∀ (n : ℕ), v (s n) = v univ - v (s n)ᶜ
⊢ v (⋂ n, s n) = v (⋃ b, (s b)ᶜ)ᶜ

Tactic:
simp

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

Goal state before:
pp: case empty
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
X : Type u_5
mX : MeasurableSpace X
μ ν : VectorMeasure X M
C : Set (Set X)
hμν : ∀ s ∈ C, μ s = ν s
hA : mX = MeasurableSpace.generateFrom C
hC : IsPiSystem C
h_univ : μ univ = ν univ
s : Set X
⊢ μ ∅ = ν ∅

Tactic:
simp

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
inst✝ : ContinuousAdd M
v w : VectorMeasure α M
⊢ (⇑v + ⇑w) ∅ = 0

Tactic:
simp

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✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
v : VectorMeasure α M
⊢ (-⇑v) ∅ = 0

Tactic:
simp

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✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
v w : VectorMeasure α M
⊢ (⇑v - ⇑w) ∅ = 0

Tactic:
simp

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
inst✝ : MeasurableSpace β
x✝ : β
v✝ : M
s : Set β
x : β
v : M
⊢ (if MeasurableSet ∅ ∧ x ∈ ∅ then v else 0) = 0

Tactic:
simp

Goal state after:
Module: Mathlib.MeasureTheory.Covering.LiminfLimsup

Goal state before:
pp: α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
hr' : ∀ᶠ (i : ℕ) in atTop, p i → 0 < r i
h₁ : blimsup (fun i ↦ cthickening (r i) (s i)) atTop p =ᵐ[μ] blimsup (fun i ↦ thickening (r i) (s i)) atTop p
h₂ : blimsup (fun i ↦ cthickening (M * r i) (s i)) atTop p =ᵐ[μ] blimsup (fun i ↦ cthickening (r i) (s i)) atTop p
⊢ 0 = M * 0

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
hμ : IsFiniteMeasure μ
⊢ (if MeasurableSet ∅ then μ.real ∅ else 0) = 0

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
⊢ (if MeasurableSet ∅ then μ ∅ else 0) = 0

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
i : Set α
a✝ : MeasurableSet i
⊢ (toENNRealVectorMeasure 0) i = 0 i

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
⊢ toENNRealVectorMeasure 0 = 0

Tactic:
ext i
  simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m mα : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v✝ v : VectorMeasure α M
f : α → β
hf : Measurable f
⊢ (if MeasurableSet ∅ then v (f ⁻¹' ∅) else 0) = 0

Tactic:
simp

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

Goal state before:
pp: case mp.left
α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : c ≪ᵥ μ
⊢ re c ≪ᵥ μ

Tactic:
· intro i hi; simp [h hi]

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

Goal state before:
pp: case mp.right
α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : c ≪ᵥ μ
⊢ im c ≪ᵥ μ

Tactic:
· intro i hi; simp [h hi]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : re c ≪ᵥ μ ∧ im c ≪ᵥ μ
i : Set α
hi : μ i = 0
⊢ ↑0 + ↑0 * Complex.I = 0

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
N : Type u_4
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
f : M →+ N
hf : Continuous[inst✝², inst✝] ⇑f
i✝ : Set α
a✝ : MeasurableSet i✝
⊢ (mapRange 0 f hf) i✝ = 0 i✝

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
M : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
N : Type u_4
inst✝³ : AddCommMonoid N
inst✝² : TopologicalSpace N
inst✝¹ : ContinuousAdd M
inst✝ : ContinuousAdd N
v w : VectorMeasure α M
f : M →+ N
hf : Continuous[inst✝⁴, inst✝²] ⇑f
i✝ : Set α
a✝ : MeasurableSet i✝
⊢ ((v + w).mapRange f hf) i✝ = (v.mapRange f hf + w.mapRange f hf) i✝

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
M : Type u_3
inst✝⁸ : AddCommMonoid M
inst✝⁷ : TopologicalSpace M
N : Type u_4
inst✝⁶ : AddCommMonoid N
inst✝⁵ : TopologicalSpace N
R : Type u_5
inst✝⁴ : Semiring R
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : ContinuousConstSMul R M
inst✝ : ContinuousConstSMul R N
v : VectorMeasure α M
f : M →ₗ[R] N
hf : Continuous[inst✝⁷, inst✝⁵] ⇑f
c : R
i✝ : Set α
a✝ : MeasurableSet i✝
⊢ ((c • v).mapRange f.toAddMonoidHom hf) i✝ = (c • v.mapRange f.toAddMonoidHom hf) i✝

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m mα : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v✝ v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
⊢ (if MeasurableSet ∅ then v (∅ ∩ i) else 0) = 0

Tactic:
simp

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

Goal state before:
pp: case pos
α : 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
⊢ eLpNorm (s.indicator 0) p μ ≤ ENNReal.ofReal ε

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₂ : ¬s ≤[i] 0
n : ℕ
hn : ¬s ≤[i \ ⋃ k, ⋃ (_ : k < n + 1), s.restrictNonposSeq i k] 0
⊢ i \ ⋃ k, ⋃ (_ : k < n + 1), s.restrictNonposSeq i k ⊆ i \ ⋃ k, ⋃ (_ : k ≤ n), s.restrictNonposSeq i k

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : AddCommMonoid M
inst✝¹ : T2Space M
inst✝ : ContinuousAdd M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
A : Set α
hA : MeasurableSet A
⊢ v (A ∩ i ∪ A ∩ iᶜ) = v A

Tactic:
simp

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝⁵ : 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
v : VectorMeasure α M
f : α → β
c : R
hf : ¬Measurable f
i : Set β
a✝ : MeasurableSet i
⊢ 0 i = (c • 0) i

Tactic:
simp

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

Goal state before:
pp: case neg
α : Type u_1
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
v : VectorMeasure α M
i : Set α
c : R
hi : ¬MeasurableSet i
j : Set α
a✝ : MeasurableSet j
⊢ 0 j = (c • 0) j

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
⊢ v ≤[∅] w

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
⊢ v ≤[univ] w ↔ v ≤ w

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommGroup M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedAddMonoid M
inst✝ : IsTopologicalAddGroup M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
h : v ≤[i] w
⊢ -w ≤[i] -v

Tactic:
intro j

Goal state after:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommGroup M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedAddMonoid M
inst✝ : IsTopologicalAddGroup M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
h : v ≤[i] w
j : Set α
⊢ MeasurableSet j → ((-w).restrict i) j ≤ ((-v).restrict i) j
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : MeasurableSpace α
s✝ s : SignedMeasure α
i : Set α := ⋯.choose
hi : MeasurableSet ⋯.choose ∧ 0 ≤[⋯.choose] s ∧ s ≤[⋯.chooseᶜ] 0
⊢ ↑(NNReal.mk (s (⋯.choose ∩ ⋯.chooseᶜ)) ⋯) = 0

Tactic:
simp

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : MeasurableSpace α
s✝ s : SignedMeasure α
i : Set α := ⋯.choose
hi : MeasurableSet ⋯.choose ∧ 0 ≤[⋯.choose] s ∧ s ≤[⋯.chooseᶜ] 0
⊢ ↑(NNReal.mk (-s (⋯.chooseᶜ ∩ ⋯.chooseᶜᶜ)) ⋯) = 0

Tactic:
simp

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

Goal state before:
pp: case negPart
α : Type u_1
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.posPart = j₂.posPart
hj' : j₁.toSignedMeasure = j₂.toSignedMeasure
⊢ j₁.negPart = j₂.negPart

Tactic:
← toSignedMeasure_eq_toSignedMeasure_iff

Goal state after:
case negPart
α : Type u_1
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.posPart = j₂.posPart
hj' : j₁.toSignedMeasure = j₂.toSignedMeasure
⊢ j₁.negPart.toSignedMeasure = j₂.negPart.toSignedMeasure
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case intro.refine_2.none
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid M
inst✝³ : PartialOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : OrderClosedTopology M
v w : VectorMeasure α M
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (b : β), MeasurableSet (f b)
hf₂ : ∀ (b : β), v ≤[f b] w
val✝ : Encodable β
n : ℕ
⊢ v ≤[⋃ b ∈ none, f b] w

Tactic:
simp

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_one : 1 ≤ p
hp_top : p ≠ ∞
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
δ : ℝ
hδpos : 0 < δ
hδ : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f) p μ ≤ 2 * ENNReal.ofReal (ε / 2)
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
⊢ ENNReal.ofReal 2 = 2

Tactic:
simp

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

Goal state before:
pp: α : 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
R : Type u_6
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
r : R
v : VectorMeasure α M
w : VectorMeasure α N
h : v ≪ᵥ w
⊢ r • v ≪ᵥ w

Tactic:
by
  intro s hs
  rw [_root_.smul_apply, h hs, smul_zero]

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : s i < 0
hi₁ : MeasurableSet i
h : ¬s ≤[i] 0
hn : ∀ (n : ℕ), ¬s ≤[i \ ⋃ l, ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
A : Set α := i \ ⋃ l, s.restrictNonposSeq i l
hA : A = i \ ⋃ l, s.restrictNonposSeq i l
bdd : ℕ → ℕ := fun n ↦ s.findExistsOneDivLT (i \ ⋃ k, ⋃ (_ : k ≤ n), s.restrictNonposSeq i k)
hn' : ∀ (n : ℕ), ¬s ≤[i \ ⋃ l, ⋃ (_ : l ≤ n), s.restrictNonposSeq i l] 0
h₁ : s i = s A + ∑' (l : ℕ), s (s.restrictNonposSeq i l)
h₂ : s A ≤ s i
h₃' : Summable fun n ↦ 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n ↦ ↑(bdd n) + 1) atTop atTop
x✝ : ℕ
⊢ ↑(bdd x✝) = ↑(bdd x✝) + 1 + -1

Tactic:
simp

Goal state after: