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
e : V ≃ₗ[K] V
he : ∀ (a : K), ∃ x, e.fixedReduce x ≠ a • x
h : 1 < finrank K (V ⧸ (↑e).fixedSubmodule)
v : V ⧸ (↑e).fixedSubmodule
hu : LinearIndependent K ![v, e.fixedReduce v]
⊢ ∃ f v,
    LinearIndependent K ![(↑e).fixedSubmodule.mkQ v, e.fixedReduce ((↑e).fixedSubmodule.mkQ v)] ∧
      (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker f ∧ f v = 1

Tactic:
obtain ⟨u, rfl⟩ := e.fixedSubmodule.mkQ_surjective v

Goal state after:
K : Type u_1
inst✝² : DivisionRing K
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module K V
e : V ≃ₗ[K] V
he : ∀ (a : K), ∃ x, e.fixedReduce x ≠ a • x
h : 1 < finrank K (V ⧸ (↑e).fixedSubmodule)
u : V
hu : LinearIndependent K ![(↑e).fixedSubmodule.mkQ u, e.fixedReduce ((↑e).fixedSubmodule.mkQ u)]
⊢ ∃ f v,
    LinearIndependent K ![(↑e).fixedSubmodule.mkQ v, e.fixedReduce ((↑e).fixedSubmodule.mkQ v)] ∧
      (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker f ∧ f v = 1
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
S : Finset (Set α)
hS : S.Nonempty
hSC : ↑S ⊆ C
⊢ ∃ P, ↑P.parts ⊆ C

Tactic:
sup'_eq_sup

Goal state after:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
S : Finset (Set α)
hS : S.Nonempty
hSC : ↑S ⊆ C
⊢ ∃ P, ↑P.parts ⊆ C
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: case refine_1
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
s₁ : Finset ι
S₁ : Set ((i : ↥s₁) → α ↑i)
hS₁ : MeasurableSet S₁
s₂ : Finset ι
S₂ : Set ((i : ↥s₂) → α ↑i)
hS₂ : MeasurableSet S₂
⊢ MeasurableSet (Finset.restrict₂ ⋯ ⁻¹' S₁ ∩ {f | Finset.restrict₂ ⋯ f ∈ S₂})

Tactic:
refine MeasurableSet.inter ?_ ?_

Goal state after:
case refine_1.refine_1
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
s₁ : Finset ι
S₁ : Set ((i : ↥s₁) → α ↑i)
hS₁ : MeasurableSet S₁
s₂ : Finset ι
S₂ : Set ((i : ↥s₂) → α ↑i)
hS₂ : MeasurableSet S₂
⊢ MeasurableSet (Finset.restrict₂ ⋯ ⁻¹' S₁)

case refine_1.refine_2
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
s₁ : Finset ι
S₁ : Set ((i : ↥s₁) → α ↑i)
hS₁ : MeasurableSet S₁
s₂ : Finset ι
S₂ : Set ((i : ↥s₂) → α ↑i)
hS₂ : MeasurableSet S₂
⊢ MeasurableSet {f | Finset.restrict₂ ⋯ f ∈ S₂}
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
s : Set α
hs : s ∈ supClosure C
T : Finset (Set α)
hT : T.Nonempty
hTC : ↑T ⊆ C
⊢ s \ T.sup' hT id ∈ supClosure C

Tactic:
sup'_eq_sup

Goal state after:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
s : Set α
hs : s ∈ supClosure C
T : Finset (Set α)
hT : T.Nonempty
hTC : ↑T ⊆ C
⊢ s \ T.sup id ∈ supClosure C
Module: Mathlib.Topology.Order.WithTop

Goal state before:
pp: case a
ι : Type u_1
inst✝¹ : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst✝ : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := if h : ∃ x, Ioi x = ∅ then h.choose else x₀
d : Set (WithTop ι) := WithTop.some '' c ∪ WithTop.some '' c' ∪ {⊤} ∪ {↑x₁}
basis : Set (Set ι) := {s | ∃ f g, f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite ∧ s = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a}
h_basis : IsTopologicalBasis basis
⊢ generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a} ≤ instWithTopOfOrderTopology

Tactic:
OrderTopology.topology_eq_generate_intervals (α := WithTop ι)

Goal state after:
case a
ι : Type u_1
inst✝¹ : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst✝ : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := if h : ∃ x, Ioi x = ∅ then h.choose else x₀
d : Set (WithTop ι) := WithTop.some '' c ∪ WithTop.some '' c' ∪ {⊤} ∪ {↑x₁}
basis : Set (Set ι) := {s | ∃ f g, f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite ∧ s = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a}
h_basis : IsTopologicalBasis basis
⊢ generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a} ≤ Preorder.topology (WithTop ι)
Module: Mathlib.MeasureTheory.SetAlgebra

Goal state before:
pp: case compl.refine_1
α : Type u_1
𝒜 : Set (Set α)
s u : Set α
hs✝ : generateSetAlgebra 𝒜 u
A : Set (Set (Set α))
A_fin : A.Finite
mem_A : ∀ a ∈ A, a.Finite
hA : ∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ A, ⋂ t ∈ a, t
this✝ : Finite ↑A
this : ∀ (a : ↑A), Finite ↑↑a
f : (a : ↑A) → ↑↑a
a : ↑A
⊢ (↑(f a))ᶜ ∈ 𝒜 ∨ (↑(f a))ᶜᶜ ∈ 𝒜

Tactic:
compl_compl,

Goal state after:
case compl.refine_1
α : Type u_1
𝒜 : Set (Set α)
s u : Set α
hs✝ : generateSetAlgebra 𝒜 u
A : Set (Set (Set α))
A_fin : A.Finite
mem_A : ∀ a ∈ A, a.Finite
hA : ∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ A, ⋂ t ∈ a, t
this✝ : Finite ↑A
this : ∀ (a : ↑A), Finite ↑↑a
f : (a : ↑A) → ↑↑a
a : ↑A
⊢ (↑(f a))ᶜ ∈ 𝒜 ∨ ↑(f a) ∈ 𝒜
Module: Mathlib.LinearAlgebra.Transvection.Generation

Goal state before:
pp: case inl
K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
e : V ≃ₗ[K] V
f g : Dual K V
v : V
a b : K
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
hg : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker (f + g)
hfgv : (f + g) v = 1
hg0 : g ≠ 0
hne_top : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ⊔ K ∙ v < ⊤
ha : ∀ (v_1 : V), (auxTransvection hf * e) v_1 - a • v_1 ∈ (↑e).fixedSubmodule ⊔ K ∙ v
hb : ∀ (v_1 : V), (auxTransvection hg * e) v_1 - b • v_1 ∈ (↑e).fixedSubmodule ⊔ K ∙ v
c : K := b - a
hc : c = b - a
key : ∀ (x : V), g (e x) • (v - e v) - c • x ∈ (↑e).fixedSubmodule ⊔ K ∙ v
hc0 : c = 0
⊢ False

Tactic:
apply one_ne_zero (α := K)
    rw [LinearIndependent.pair_iff] at hv
    have hmem : v - e v ∈ e.fixedSubmodule ⊔ K ∙ v := by
      simp only [hc0, zero_smul, sub_zero] at key
      obtain ⟨w, hw⟩ : ∃ w, g w ≠ 0 := by
        contrapose! hg0
        exact LinearMap.ext hg0
      simpa [hw] using key ((g w)⁻¹ • e⁻¹ w)
    simp only [mem_sup, mem_span_singleton, exists_exists_eq_and] at hmem
    obtain ⟨y, hy, k, hk⟩ := hmem
    refine (hv (k - 1) 1 ?_).right
    simp only [Submodule.mkQ_apply, fixedReduce_mk]
    simp only [← e.fixedSubmodule.mkQ_apply, ← LinearMap.map_smul, ← map_add,
      ← LinearMap.mem_ker, Submodule.ker_mkQ]
    rw [← Submodule.neg_mem_iff] at hy
    convert hy using 1
    rw [eq_comm, ← sub_eq_iff_eq_add] at hk
    rw [← hk]
    simp only [sub_smul, one_smul]
    abel

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)
s t : Set ((i : ι) → α i)
hP : IsProjectiveMeasureFamily P
hs : s ∈ measurableCylinders α
ht : t ∈ measurableCylinders α
hst : Disjoint s t
I : Finset ι
S : Set ((i : ↥I) → α ↑i)
hS : MeasurableSet S
hs_eq : s = cylinder I S
J : Finset ι
T : Set ((i : ↥J) → α ↑i)
hT : MeasurableSet T
ht_eq : t = cylinder J T
⊢ projectiveFamilyFun P (s ∪ t) = projectiveFamilyFun P s + projectiveFamilyFun P t

Tactic:
let S' := restrict₂ (subset_union_left (s₂ := J)) ⁻¹' S
  let T' := restrict₂ (subset_union_right (s₁ := I)) ⁻¹' T
  have hS' : MeasurableSet S' := measurable_restrict₂ _ hS
  have hT' : MeasurableSet T' := measurable_restrict₂ _ hT
  have h_eq1 : s = cylinder (I ∪ J) S' := by rw [hs_eq]; exact cylinder_eq_cylinder_union I S J
  have h_eq2 : t = cylinder (I ∪ J) T' := by rw [ht_eq]; exact cylinder_eq_cylinder_union J T I
  have h_eq3 : s ∪ t = cylinder (I ∪ J) (S' ∪ T') := by
    rw [hs_eq, ht_eq]; exact union_cylinder _ _ _ _
  rw [projectiveFamilyFun_congr hP hs h_eq1 hS', projectiveFamilyFun_congr hP ht h_eq2 hT',
    projectiveFamilyFun_congr hP (union_mem_measurableCylinders hs ht) h_eq3 (hS'.union hT')]
  cases isEmpty_or_nonempty (Π i, α i) with
  | inl h => simp [hP.eq_zero_of_isEmpty]
  | inr h =>
    rw [measure_union _ hT']
    rwa [hs_eq, ht_eq, disjoint_cylinder_iff] at hst

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

Goal state before:
pp: α : Type u_1
C : Set (Set α)
t : Set α
G : Type u_2
inst✝² : AddCommMonoid G
inst✝¹ : PartialOrder G
inst✝ : CanonicallyOrderedAdd G
m : AddContent G C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
ht : t ∈ C
htJ : t ⊆ ⋃ x, ↑(J.equivFin.symm x)
⊢ m t ≤ ∑ u ∈ J, m u

Tactic:
← iUnion_disjointed

Goal state after:
α : Type u_1
C : Set (Set α)
t : Set α
G : Type u_2
inst✝² : AddCommMonoid G
inst✝¹ : PartialOrder G
inst✝ : CanonicallyOrderedAdd G
m : AddContent G C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
ht : t ∈ C
htJ : t ⊆ ⋃ i, disjointed (fun i ↦ ↑(J.equivFin.symm i)) i
⊢ m t ≤ ∑ u ∈ J, m u
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 α
hf_mono : Monotone f
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ i, f i ∈ C
⊢ ⋃ i, disjointed f i ∈ C

Tactic:
rwa [iUnion_disjointed]

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
⊢ ∃ 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
⊢ ∃ M, eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε

Tactic:
· exact ⟨1, by simp [hp_ne_zero]⟩

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
⊢ ∃ 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_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v : VectorMeasure α M
inst✝ : T2Space M
s : ℕ → Set α
hm : Monotone s
hs : ∀ (i : ℕ), MeasurableSet (s i)
t : ℕ → Set α := disjointed s
ht : ∀ (n : ℕ), MeasurableSet (t n)
⊢ HasSum (fun n ↦ v (t n)) (v (⋃ n, s n))

Tactic:
← iUnion_disjointed

Goal state after:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v : VectorMeasure α M
inst✝ : T2Space M
s : ℕ → Set α
hm : Monotone s
hs : ∀ (i : ℕ), MeasurableSet (s i)
t : ℕ → Set α := disjointed s
ht : ∀ (n : ℕ), MeasurableSet (t n)
⊢ HasSum (fun n ↦ v (t n)) (v (⋃ i, disjointed s i))
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 : ℝ
hM' : 0 ≤ M
hM :
  ∫⁻ (x : α), ‖{x | M ≤ ↑‖‖f x‖ ^ p.toReal‖₊}.indicator (fun x ↦ ‖f x‖ ^ p.toReal) x‖ₑ ∂μ ≤
    ENNReal.ofReal (ε ^ p.toReal)
x : α
hiff : M ^ (1 / p.toReal) ≤ ↑‖f x‖₊ ↔ M ≤ ↑‖‖f x‖ ^ p.toReal‖₊
hx : x ∈ {x | M ^ (1 / p.toReal) ≤ ↑‖f x‖₊}
⊢ ‖f x‖ₑ ^ p.toReal = ENNReal.ofReal (‖f x‖ ^ p.toReal)

pp: case pos.h
α : 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 : ℝ
hM' : 0 ≤ M
hM :
  ∫⁻ (x : α), ‖{x | M ≤ ↑‖‖f x‖ ^ p.toReal‖₊}.indicator (fun x ↦ ‖f x‖ ^ p.toReal) x‖ₑ ∂μ ≤
    ENNReal.ofReal (ε ^ p.toReal)
x : α
hiff : M ^ (1 / p.toReal) ≤ ↑‖f x‖₊ ↔ M ≤ ↑‖‖f x‖ ^ p.toReal‖₊
hx : x ∈ {x | M ^ (1 / p.toReal) ≤ ↑‖f x‖₊}
⊢ x ∈ {x | M ≤ ↑‖‖f x‖ ^ p.toReal‖₊}

Tactic:
← ENNReal.ofReal_rpow_of_nonneg (norm_nonneg _) ENNReal.toReal_nonneg,

Goal state after:
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 : ℝ
hM' : 0 ≤ M
hM :
  ∫⁻ (x : α), ‖{x | M ≤ ↑‖‖f x‖ ^ p.toReal‖₊}.indicator (fun x ↦ ‖f x‖ ^ p.toReal) x‖ₑ ∂μ ≤
    ENNReal.ofReal (ε ^ p.toReal)
x : α
hiff : M ^ (1 / p.toReal) ≤ ↑‖f x‖₊ ↔ M ≤ ↑‖‖f x‖ ^ p.toReal‖₊
hx : x ∈ {x | M ^ (1 / p.toReal) ≤ ↑‖f x‖₊}
⊢ ‖f x‖ₑ ^ p.toReal = ENNReal.ofReal ‖f x‖ ^ p.toReal

case pos.h
α : 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 : ℝ
hM' : 0 ≤ M
hM :
  ∫⁻ (x : α), ‖{x | M ≤ ↑‖‖f x‖ ^ p.toReal‖₊}.indicator (fun x ↦ ‖f x‖ ^ p.toReal) x‖ₑ ∂μ ≤
    ENNReal.ofReal (ε ^ p.toReal)
x : α
hiff : M ^ (1 / p.toReal) ≤ ↑‖f x‖₊ ↔ M ≤ ↑‖‖f x‖ ^ p.toReal‖₊
hx : x ∈ {x | M ^ (1 / p.toReal) ≤ ↑‖f x‖₊}
⊢ x ∈ {x | M ≤ ↑‖‖f x‖ ^ p.toReal‖₊}
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: case inl
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n m : ℕ
h✝ : n ≠ m
h : n < m
⊢ s.restrictNonposSeq i n ∩ s.restrictNonposSeq i m = ∅

Tactic:
rw [restrictNonposSeq_disjoint' h]

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

Goal state before:
pp: case refine_3
α : 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 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      ?m.82 s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator ({x | ‖f x‖ < M}.indicator f)) p ?m.82 ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
⊢ eLpNorm ({x | ‖f x‖ < M}.indicator f) p (μ.restrict s) ≤ ENNReal.ofReal ε

Tactic:
rw [← eLpNorm_indicator_eq_eLpNorm_restrict hs]

Goal state after:
case refine_3
α : 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 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      ?m.82 s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator ({x | ‖f x‖ < M}.indicator f)) p ?m.82 ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
⊢ eLpNorm (s.indicator ({x | ‖f x‖ < M}.indicator f)) p μ ≤ ENNReal.ofReal ε
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
i : Set α
hi : MeasurableSet i
hi₂ : v ≤[i] w
j : Set α
hj : j ⊆ i
⊢ v j ≤ w j

Tactic:
by
  by_cases hj₁ : MeasurableSet j
  · exact (restrict_le_restrict_iff _ _ hi).1 hi₂ hj₁ hj
  · rw [v.not_measurable hj₁, w.not_measurable hj₁]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : s i < 0
h : ¬s ≤[i] 0
hn : ∃ n, s ≤[i \ ⋃ l, ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
k : ℕ := Nat.find hn
hk₂ : s ≤[i \ ⋃ l, ⋃ (_ : l < k), s.restrictNonposSeq i l] 0
hmeas : MeasurableSet (⋃ l, ⋃ (_ : l < k), s.restrictNonposSeq i l)
⊢ ⋃ l, ⋃ (_ : l < k), s.restrictNonposSeq i l ⊆ i

Tactic:
apply Set.iUnion_subset
    intro a x
    simp only [and_imp, exists_prop, Set.mem_iUnion]
    intro _ hx
    exact restrictNonposSeq_subset _ hx

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

Goal state before:
pp: case e'_5
α : Type u_1
m✝ : MeasurableSpace α
μ✝ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
f : α → E
hf : Integrable f μ
s : ℕ → Set α
hs₁ : ∀ (i : ℕ), MeasurableSet (s i)
hs₂ : Pairwise (Function.onFun Disjoint s)
n : ℕ
⊢ (if MeasurableSet (s n) then ∫ (x : α) in s n, f x ∂μ else 0) = ∫ (x : α) in s n, f x ∂μ

Tactic:
if_pos (hs₁ n)

Goal state after:
case e'_5
α : Type u_1
m✝ : MeasurableSpace α
μ✝ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
f : α → E
hf : Integrable f μ
s : ℕ → Set α
hs₁ : ∀ (i : ℕ), MeasurableSet (s i)
hs₂ : Pairwise (Function.onFun Disjoint s)
n : ℕ
⊢ ∫ (x : α) in s n, f x ∂μ = ∫ (x : α) in s n, f x ∂μ
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → E
hf : ¬Integrable f μ
⊢ (if hf : Integrable (-f) μ then
      { measureOf' := fun s ↦ if MeasurableSet s then ∫ (x : α) in s, (-f) x ∂μ else 0, empty' := ⋯,
        not_measurable' := ⋯, m_iUnion' := ⋯ }
    else 0) =
    -if hf : Integrable f μ then
        { measureOf' := fun s ↦ if MeasurableSet s then ∫ (x : α) in s, f x ∂μ else 0, empty' := ⋯,
          not_measurable' := ⋯, m_iUnion' := ⋯ }
      else 0

Tactic:
dif_neg hf,

Goal state after:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → E
hf : ¬Integrable f μ
⊢ (if hf : Integrable (-f) μ then
      { measureOf' := fun s ↦ if MeasurableSet s then ∫ (x : α) in s, (-f) x ∂μ else 0, empty' := ⋯,
        not_measurable' := ⋯, m_iUnion' := ⋯ }
    else 0) =
    -0
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
𝕜 : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : SMulCommClass ℝ 𝕜 E
f : α → E
r : 𝕜
hf : ¬Integrable f μ
hr : ¬r = 0
⊢ (if hf : Integrable (r • f) μ then
      { measureOf' := fun s ↦ if MeasurableSet s then ∫ (x : α) in s, (r • f) x ∂μ else 0, empty' := ⋯,
        not_measurable' := ⋯, m_iUnion' := ⋯ }
    else 0) =
    r •
      if hf : Integrable f μ then
        { measureOf' := fun s ↦ if MeasurableSet s then ∫ (x : α) in s, f x ∂μ else 0, empty' := ⋯,
          not_measurable' := ⋯, m_iUnion' := ⋯ }
      else 0

Tactic:
dif_neg hf,

Goal state after:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
𝕜 : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : SMulCommClass ℝ 𝕜 E
f : α → E
r : 𝕜
hf : ¬Integrable f μ
hr : ¬r = 0
⊢ (if hf : Integrable (r • f) μ then
      { measureOf' := fun s ↦ if MeasurableSet s then ∫ (x : α) in s, (r • f) x ∂μ else 0, empty' := ⋯,
        not_measurable' := ⋯, m_iUnion' := ⋯ }
    else 0) =
    r • 0
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : α → E
h : f =ᵐ[μ] g
hf : ¬Integrable f μ
hg : ¬Integrable g μ
⊢ (if hf : Integrable f μ then
      { measureOf' := fun s ↦ if MeasurableSet s then ∫ (x : α) in s, f x ∂μ else 0, empty' := ⋯, not_measurable' := ⋯,
        m_iUnion' := ⋯ }
    else 0) =
    if hf : Integrable g μ then
      { measureOf' := fun s ↦ if MeasurableSet s then ∫ (x : α) in s, g x ∂μ else 0, empty' := ⋯, not_measurable' := ⋯,
        m_iUnion' := ⋯ }
    else 0

Tactic:
dif_neg hf,

Goal state after:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : α → E
h : f =ᵐ[μ] g
hf : ¬Integrable f μ
hg : ¬Integrable g μ
⊢ 0 =
    if hf : Integrable g μ then
      { measureOf' := fun s ↦ if MeasurableSet s then ∫ (x : α) in s, g x ∂μ else 0, empty' := ⋯, not_measurable' := ⋯,
        m_iUnion' := ⋯ }
    else 0
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
this :
  (s.singularPart μ).toJordanDecomposition =
    { posPart := s.toJordanDecomposition.posPart.singularPart μ,
      negPart := s.toJordanDecomposition.negPart.singularPart μ, posPart_finite := ⋯, negPart_finite := ⋯,
      mutuallySingular := ⋯ }
⊢ (s.singularPart μ).totalVariation =
    s.toJordanDecomposition.posPart.singularPart μ + s.toJordanDecomposition.negPart.singularPart μ

Tactic:
rw [totalVariation, this]

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

Goal state before:
pp: case right
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' : (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → 0 j ≤ s j) ∧ ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → s j ≤ 0 j
hj' :
  (∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ j → 0 j_1 ≤ s j_1) ∧
    ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → s j_1 ≤ 0 j_1
⊢ s (jᶜᶜ ∩ iᶜ ∪ iᶜᶜ ∩ jᶜ) = 0

Tactic:
compl_compl,

Goal state after:
case right
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' : (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → 0 j ≤ s j) ∧ ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → s j ≤ 0 j
hj' :
  (∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ j → 0 j_1 ≤ s j_1) ∧
    ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → s j_1 ≤ 0 j_1
⊢ s (j ∩ iᶜ ∪ iᶜᶜ ∩ jᶜ) = 0
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: case right
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' : (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → 0 j ≤ s j) ∧ ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → s j ≤ 0 j
hj' :
  (∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ j → 0 j_1 ≤ s j_1) ∧
    ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → s j_1 ≤ 0 j_1
⊢ s (j ∩ iᶜ ∪ iᶜᶜ ∩ jᶜ) = 0

Tactic:
compl_compl,

Goal state after:
case right
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' : (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → 0 j ≤ s j) ∧ ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → s j ≤ 0 j
hj' :
  (∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ j → 0 j_1 ≤ s j_1) ∧
    ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → s j_1 ≤ 0 j_1
⊢ s (j ∩ iᶜ ∪ i ∩ jᶜ) = 0
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:
by
  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.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst✝ : c.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
⊢ Integrable (fun x ↦ (c.rnDeriv μ x).re) μ

Tactic:
exact SignedMeasure.integrable_rnDeriv _ _

Goal state after: