awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
m : Set α → E
hm : ∀ (s : Set α), ‖m s‖ₑ ≤ (μ : (a : Set α) → ENNReal) s
inst_2 : IsFiniteMeasure μ
h'm : ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t
h''m : ∀ (s : Set α), ¬MeasurableSet s → m s = 0
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Function.onFun Disjoint f)
A : ∀ (n : ℕ), m (⋃ i ∈ Finset.range n, f i) = ∑ i ∈ Finset.range n, m (f i)
B : ∀ (n : ℕ), m (⋃ (i : ℕ), f i) = m (⋃ i ∈ Finset.range n, f i) + m (⋃ i ∈ Set.Ici n, f i)
C : ∀ (n : ℕ), m (⋃ (i : ℕ), f i) - ∑ i ∈ Finset.range n, m (f i) = m (⋃ i ∈ Set.Ici n, f i)
⊢ Filter.Tendsto (β := ENNReal) (fun (n : ℕ) ↦ (μ : (a : Set α) → ENNReal) (⋃ i ∈ Set.Ici n, f i)) Filter.atTop (nhds ⊥)

Tactic:
exact tendsto_measure_biUnion_Ici_zero_of_pairwise_disjoint
      (fun i ↦ (f_meas i).nullMeasurableSet) f_disj

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.tendsto_measure_biUnion_Ici_zero_of_pairwise_disjoint
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
inst_2 : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetRing C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ C, (μ : (a : Set α) → ℝ≥0∞) (s ∆ t) < ε
C' : Set (MeasuredSets μ) := {s : MeasuredSets μ | ∃ c ∈ C, (↑s : Set α) = c}
s : MeasuredSets μ
hs : s ∈ C'
⊢ (↑s : Set α) ∈ C

Tactic:
rcases hs with ⟨t, ht, rfl⟩

Premises used: rfl
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
inst_2 : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetRing C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ C, (μ : (a : Set α) → ℝ≥0∞) (s ∆ t) < ε
C' : Set (MeasuredSets μ) := {s : MeasuredSets μ | ∃ c ∈ C, (↑s : Set α) = c}
s : MeasuredSets μ
ht : (↑s : Set α) ∈ C
⊢ (↑s : Set α) ∈ C

Tactic:
ht
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
inst_2 : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetRing C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ C, (μ : (a : Set α) → ℝ≥0∞) (s ∆ t) < ε
C' : Set (MeasuredSets μ) := {s : MeasuredSets μ | ∃ c ∈ C, (↑s : Set α) = c}
s : MeasuredSets μ
ht : (↑s : Set α) ∈ C
⊢ (↑s : Set α) ∈ C

Tactic:
exact ht
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
inst_2 : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetRing C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ C, (μ : (a : Set α) → ℝ≥0∞) (s ∆ t) < ε
C' : Set (MeasuredSets μ) := {s : MeasuredSets μ | ∃ c ∈ C, (↑s : Set α) = c}
⊢ ∀ (s : MeasuredSets μ) (hs : s ∈ C'), (↑s : Set α) ∈ C

Tactic:
have C'C (s : MeasuredSets μ) (hs : s ∈ C') : (s : Set α) ∈ C := by
    rcases hs with ⟨t, ht, rfl⟩; exact ht
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
inst_2 : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetRing C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ C, (μ : (a : Set α) → ℝ≥0∞) (s ∆ t) < ε
C' : Set (MeasuredSets μ) := {s : MeasuredSets μ | ∃ c ∈ C, (↑s : Set α) = c}
C'C : ∀ (s : MeasuredSets μ) (hs : s ∈ C'), (↑s : Set α) ∈ C
simp : ∀ (x : MeasuredSets μ) (ε : ℝ≥0∞), 0 < ε → ∃ y ∈ C', edist x y < ε
⊢ Dense C'

Tactic:
simp only [Dense, EMetric.mem_closure_iff, gt_iff_lt]

Premises used: Dense, gt_iff_lt, EMetric.mem_closure_iff
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
inst_2 : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetRing C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ C, (μ : (a : Set α) → ℝ≥0∞) (s ∆ t) < ε
C' : Set (MeasuredSets μ) := {s : MeasuredSets μ | ∃ c ∈ C, (↑s : Set α) = c}
C'C : ∀ (s : MeasuredSets μ) (hs : s ∈ C'), (↑s : Set α) ∈ C
x : MeasuredSets μ
ε : ℝ≥0∞
εpos : 0 < ε
rcases : ∀ (s : Set α) (sC : s ∈ C) (hs : (μ : (a : Set α) → ℝ≥0∞) (s ∆ (↑x : Set α)) < ε), ∃ y ∈ C', edist x y < ε
⊢ ∃ y ∈ C', edist x y < ε

Tactic:
rcases h'C x ε x.2 εpos with ⟨s, sC, hs⟩

Premises used: SetLike.coe, Subtype.property
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
inst_2 : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetRing C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ C, (μ : (a : Set α) → ℝ≥0∞) (s ∆ t) < ε
C' : Set (MeasuredSets μ) := {s : MeasuredSets μ | ∃ c ∈ C, (↑s : Set α) = c}
C'C : ∀ (s : MeasuredSets μ) (hs : s ∈ C'), (↑s : Set α) ∈ C
x : MeasuredSets μ
ε : ℝ≥0∞
εpos : 0 < ε
s : Set α
sC : s ∈ C
hs : (μ : (a : Set α) → ℝ≥0∞) (s ∆ (↑x : Set α)) < ε
⊢ ∃ y ∈ C', edist x y < ε

Tactic:
⟨⟨s, hCmeas s sC⟩, ⟨s, sC, rfl⟩, ?_⟩

Premises used: Subtype.mk, And.intro, Exists.intro, rfl
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
inst_2 : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetRing C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ C, (μ : (a : Set α) → ℝ≥0∞) (s ∆ t) < ε
C' : Set (MeasuredSets μ) := {s : MeasuredSets μ | ∃ c ∈ C, (↑s : Set α) = c}
C'C : ∀ (s : MeasuredSets μ) (hs : s ∈ C'), (↑s : Set α) ∈ C
x : MeasuredSets μ
ε : ℝ≥0∞
εpos : 0 < ε
s : Set α
sC : s ∈ C
hs : (μ : (a : Set α) → ℝ≥0∞) (s ∆ (↑x : Set α)) < ε
refine : edist x (Subtype.mk (p := fun (s : Set α) ↦ MeasurableSet s) s ⋯) < ε
⊢ ∃ y ∈ C', edist x y < ε

Tactic:
refine ⟨⟨s, hCmeas s sC⟩, ⟨s, sC, rfl⟩, ?_⟩
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
inst_2 : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetRing C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ C, (μ : (a : Set α) → ℝ≥0∞) (s ∆ t) < ε
C' : Set (MeasuredSets μ) := {s : MeasuredSets μ | ∃ c ∈ C, (↑s : Set α) = c}
C'C : ∀ (s : MeasuredSets μ) (hs : s ∈ C'), (↑s : Set α) ∈ C
x : MeasuredSets μ
ε : ℝ≥0∞
εpos : 0 < ε
s : Set α
sC : s ∈ C
hs : (μ : (a : Set α) → ℝ≥0∞) (s ∆ (↑x : Set α)) < ε
rw : edist (Subtype.mk (p := fun (s : Set α) ↦ MeasurableSet s) s ⋯) x < ε
⊢ edist x (Subtype.mk (p := fun (s : Set α) ↦ MeasurableSet s) s ⋯) < ε

Tactic:
rw [edist_comm]

Premises used: PseudoEMetricSpace.edist_comm
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
inst_2 : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetRing C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ C, (μ : (a : Set α) → ℝ≥0∞) (s ∆ t) < ε
C' : Set (MeasuredSets μ) := {s : MeasuredSets μ | ∃ c ∈ C, (↑s : Set α) = c}
C'C : ∀ (s : MeasuredSets μ) (hs : s ∈ C'), (↑s : Set α) ∈ C
x : MeasuredSets μ
ε : ℝ≥0∞
εpos : 0 < ε
s : Set α
sC : s ∈ C
hs : (μ : (a : Set α) → ℝ≥0∞) (s ∆ (↑x : Set α)) < ε
⊢ edist (Subtype.mk (p := fun (s : Set α) ↦ MeasurableSet s) s ⋯) x < ε

Tactic:
hs
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
inst_2 : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetRing C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ C, (μ : (a : Set α) → ℝ≥0∞) (s ∆ t) < ε
C' : Set (MeasuredSets μ) := {s : MeasuredSets μ | ∃ c ∈ C, (↑s : Set α) = c}
C'C : ∀ (s : MeasuredSets μ) (hs : s ∈ C'), (↑s : Set α) ∈ C
x : MeasuredSets μ
ε : ℝ≥0∞
εpos : 0 < ε
s : Set α
sC : s ∈ C
hs : (μ : (a : Set α) → ℝ≥0∞) (s ∆ (↑x : Set α)) < ε
⊢ edist (Subtype.mk (p := fun (s : Set α) ↦ MeasurableSet s) s ⋯) x < ε

Tactic:
exact hs
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
inst_2 : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetRing C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ C, (μ : (a : Set α) → ℝ≥0∞) (s ∆ t) < ε
C' : Set (MeasuredSets μ) := {s : MeasuredSets μ | ∃ c ∈ C, (↑s : Set α) = c}
C'C : ∀ (s : MeasuredSets μ) (hs : s ∈ C'), (↑s : Set α) ∈ C
⊢ Dense C'

Tactic:
have C'_dense : Dense C' := by
    simp only [Dense, EMetric.mem_closure_iff, gt_iff_lt]
    intro x ε εpos
    rcases h'C x ε x.2 εpos with ⟨s, sC, hs⟩
    refine ⟨⟨s, hCmeas s sC⟩, ⟨s, sC, rfl⟩, ?_⟩
    rw [edist_comm]
    exact hs
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
inst_2 : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetRing C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ C, (μ : (a : Set α) → ℝ≥0∞) (s ∆ t) < ε
C' : Set (MeasuredSets μ) := {s : MeasuredSets μ | ∃ c ∈ C, (↑s : Set α) = c}
C'C : ∀ (s : MeasuredSets μ) (hs : s ∈ C'), (↑s : Set α) ∈ C
C'_dense : Dense C'
m₀ : (↑C' : Type u_1) → E := fun (x : (↑C' : Type u_1)) ↦ (m : (a : Set α) → E) (↑(↑x : MeasuredSets μ) : Set α)
s t : (↑C' : Type u_1)
⊢ edist s t = edist (↑s : MeasuredSets μ) (↑t : MeasuredSets μ)

Tactic:
have : edist s t = edist (s : MeasuredSets μ) t := rfl
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
inst_2 : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetRing C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ C, (μ : (a : Set α) → ℝ≥0∞) (s ∆ t) < ε
C' : Set (MeasuredSets μ) := {s : MeasuredSets μ | ∃ c ∈ C, (↑s : Set α) = c}
C'C : ∀ (s : MeasuredSets μ) (hs : s ∈ C'), (↑s : Set α) ∈ C
C'_dense : Dense C'
m₀ : (↑C' : Type u_1) → E := fun (x : (↑C' : Type u_1)) ↦ (m : (a : Set α) → E) (↑(↑x : MeasuredSets μ) : Set α)
s t : (↑C' : Type u_1)
this : edist s t = edist (↑s : MeasuredSets μ) (↑t : MeasuredSets μ)
simp :
  ‖HSub.hSub (α := E) (β := E) ((m : (a : Set α) → E) (↑(↑s : MeasuredSets μ) : Set α) : E)
        ((m : (a : Set α) → E) (↑(↑t : MeasuredSets μ) : Set α) : E)‖ₑ ≤
    (μ : (a : Set α) → ℝ≥0∞) ((↑(↑s : MeasuredSets μ) : Set α) ∆ (↑(↑t : MeasuredSets μ) : Set α))
⊢ edist (m₀ s) (m₀ t) ≤ (↑1 : ℝ≥0∞) * edist s t

Tactic:
simp only [ENNReal.coe_one, one_mul, this, MeasuredSets.edist_def, m₀, edist_eq_enorm_sub]

Premises used: edist_eq_enorm_sub, ENNReal.coe_one, MeasureTheory.MeasuredSets.edist_def, one_mul
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
inst_2 : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetRing C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ C, (μ : (a : Set α) → ℝ≥0∞) (s ∆ t) < ε
C' : Set (MeasuredSets μ) := {s : MeasuredSets μ | ∃ c ∈ C, (↑s : Set α) = c}
C'C : ∀ (s : MeasuredSets μ) (hs : s ∈ C'), (↑s : Set α) ∈ C
C'_dense : Dense C'
m₀ : (↑C' : Type u_1) → E := fun (x : (↑C' : Type u_1)) ↦ (m : (a : Set α) → E) (↑(↑x : MeasuredSets μ) : Set α)
s t : (↑C' : Type u_1)
this : edist s t = edist (↑s : MeasuredSets μ) (↑t : MeasuredSets μ)
⊢ NullMeasurableSet (↑(↑s : MeasuredSets μ) : Set α) μ

Tactic:
s.1.2.nullMeasurableSet

Premises used: MeasurableSet.nullMeasurableSet, Subtype.val, Subtype.property
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
inst_2 : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetRing C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ C, (μ : (a : Set α) → ℝ≥0∞) (s ∆ t) < ε
C' : Set (MeasuredSets μ) := {s : MeasuredSets μ | ∃ c ∈ C, (↑s : Set α) = c}
C'C : ∀ (s : MeasuredSets μ) (hs : s ∈ C'), (↑s : Set α) ∈ C
C'_dense : Dense C'
m₀ : (↑C' : Type u_1) → E := fun (x : (↑C' : Type u_1)) ↦ (m : (a : Set α) → E) (↑(↑x : MeasuredSets μ) : Set α)
s t : (↑C' : Type u_1)
this : edist s t = edist (↑s : MeasuredSets μ) (↑t : MeasuredSets μ)
⊢ NullMeasurableSet (↑(↑s : MeasuredSets μ) : Set α) μ

Tactic:
exact s.1.2.nullMeasurableSet

Premises used: MeasurableSet.nullMeasurableSet, Subtype.val, Subtype.property
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
inst_2 : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetRing C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ C, (μ : (a : Set α) → ℝ≥0∞) (s ∆ t) < ε
C' : Set (MeasuredSets μ) := {s : MeasuredSets μ | ∃ c ∈ C, (↑s : Set α) = c}
C'C : ∀ (s : MeasuredSets μ) (hs : s ∈ C'), (↑s : Set α) ∈ C
C'_dense : Dense C'
m₀ : (↑C' : Type u_1) → E := fun (x : (↑C' : Type u_1)) ↦ (m : (a : Set α) → E) (↑(↑x : MeasuredSets μ) : Set α)
s t : (↑C' : Type u_1)
this : edist s t = edist (↑s : MeasuredSets μ) (↑t : MeasuredSets μ)
⊢ NullMeasurableSet (↑(↑t : MeasuredSets μ) : Set α) μ

Tactic:
t.1.2.nullMeasurableSet

Premises used: MeasurableSet.nullMeasurableSet, Subtype.val, Subtype.property
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
inst_2 : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetRing C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ C, (μ : (a : Set α) → ℝ≥0∞) (s ∆ t) < ε
C' : Set (MeasuredSets μ) := {s : MeasuredSets μ | ∃ c ∈ C, (↑s : Set α) = c}
C'C : ∀ (s : MeasuredSets μ) (hs : s ∈ C'), (↑s : Set α) ∈ C
C'_dense : Dense C'
m₀ : (↑C' : Type u_1) → E := fun (x : (↑C' : Type u_1)) ↦ (m : (a : Set α) → E) (↑(↑x : MeasuredSets μ) : Set α)
s t : (↑C' : Type u_1)
this : edist s t = edist (↑s : MeasuredSets μ) (↑t : MeasuredSets μ)
⊢ NullMeasurableSet (↑(↑t : MeasuredSets μ) : Set α) μ

Tactic:
exact t.1.2.nullMeasurableSet

Premises used: MeasurableSet.nullMeasurableSet, Subtype.val, Subtype.property
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
inst_2 : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetRing C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ C, (μ : (a : Set α) → ℝ≥0∞) (s ∆ t) < ε
C' : Set (MeasuredSets μ) := {s : MeasuredSets μ | ∃ c ∈ C, (↑s : Set α) = c}
C'C : ∀ (s : MeasuredSets μ) (hs : s ∈ C'), (↑s : Set α) ∈ C
C'_dense : Dense C'
m₀ : (↑C' : Type u_1) → E := fun (x : (↑C' : Type u_1)) ↦ (m : (a : Set α) → E) (↑(↑x : MeasuredSets μ) : Set α)
s t : (↑C' : Type u_1)
this : edist s t = edist (↑s : MeasuredSets μ) (↑t : MeasuredSets μ)
rw :
  ‖HSub.hSub (α := E) (β := E) ((m : (a : Set α) → E) (↑(↑s : MeasuredSets μ) : Set α) : E)
        ((m : (a : Set α) → E) (↑(↑t : MeasuredSets μ) : Set α) : E)‖ₑ ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) ((↑(↑s : MeasuredSets μ) : Set α) \ (↑(↑t : MeasuredSets μ) : Set α)) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) ((↑(↑t : MeasuredSets μ) : Set α) \ (↑(↑s : MeasuredSets μ) : Set α)) : ℝ≥0∞)
⊢ ‖HSub.hSub (α := E) (β := E) ((m : (a : Set α) → E) (↑(↑s : MeasuredSets μ) : Set α) : E)
        ((m : (a : Set α) → E) (↑(↑t : MeasuredSets μ) : Set α) : E)‖ₑ ≤
    (μ : (a : Set α) → ℝ≥0∞) ((↑(↑s : MeasuredSets μ) : Set α) ∆ (↑(↑t : MeasuredSets μ) : Set α))

Tactic:
rw [measure_symmDiff_eq (by exact s.1.2.nullMeasurableSet) (by exact t.1.2.nullMeasurableSet)]

Premises used: MeasureTheory.measure_symmDiff_eq
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
inst_2 : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetRing C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ C, (μ : (a : Set α) → ℝ≥0∞) (s ∆ t) < ε
C' : Set (MeasuredSets μ) := {s : MeasuredSets μ | ∃ c ∈ C, (↑s : Set α) = c}
C'C : ∀ (s : MeasuredSets μ) (hs : s ∈ C'), (↑s : Set α) ∈ C
C'_dense : Dense C'
m₀ : (↑C' : Type u_1) → E := fun (x : (↑C' : Type u_1)) ↦ (m : (a : Set α) → E) (↑(↑x : MeasuredSets μ) : Set α)
s t : (↑C' : Type u_1)
this : edist s t = edist (↑s : MeasuredSets μ) (↑t : MeasuredSets μ)
⊢ (↑(↑s : MeasuredSets μ) : Set α) ∩ (↑(↑t : MeasuredSets μ) : Set α) ∪
      (↑(↑s : MeasuredSets μ) : Set α) \ (↑(↑t : MeasuredSets μ) : Set α) =
    (↑(↑s : MeasuredSets μ) : Set α)

Tactic:
have Is : ((s : Set α) ∩ t) ∪ (s \ t) = (s : Set α) := Set.inter_union_diff _ _
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
inst_2 : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetRing C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ C, (μ : (a : Set α) → ℝ≥0∞) (s ∆ t) < ε
C' : Set (MeasuredSets μ) := {s : MeasuredSets μ | ∃ c ∈ C, (↑s : Set α) = c}
C'C : ∀ (s : MeasuredSets μ) (hs : s ∈ C'), (↑s : Set α) ∈ C
C'_dense : Dense C'
m₀ : (↑C' : Type u_1) → E := fun (x : (↑C' : Type u_1)) ↦ (m : (a : Set α) → E) (↑(↑x : MeasuredSets μ) : Set α)
s t : (↑C' : Type u_1)
this : edist s t = edist (↑s : MeasuredSets μ) (↑t : MeasuredSets μ)
Is :
  (↑(↑s : MeasuredSets μ) : Set α) ∩ (↑(↑t : MeasuredSets μ) : Set α) ∪
      (↑(↑s : MeasuredSets μ) : Set α) \ (↑(↑t : MeasuredSets μ) : Set α) =
    (↑(↑s : MeasuredSets μ) : Set α)
⊢ (↑(↑t : MeasuredSets μ) : Set α) ∩ (↑(↑s : MeasuredSets μ) : Set α) ∪
      (↑(↑t : MeasuredSets μ) : Set α) \ (↑(↑s : MeasuredSets μ) : Set α) =
    (↑(↑t : MeasuredSets μ) : Set α)

Tactic:
have It : ((t : Set α) ∩ s) ∪ (t \ s) = (t : Set α) := Set.inter_union_diff _ _
-- Module: Mathlib.MeasureTheory.VectorMeasure.AddContent
Goal:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
μ : Measure α
inst_2 : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetRing C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, enorm.{u_2} (E := E) ((m : (a : Set α) → E) s : E) ≤ (μ : (a : Set α) → ℝ≥0∞) s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ C, (μ : (a : Set α) → ℝ≥0∞) (s ∆ t) < ε
C' : Set (MeasuredSets μ) := {s : MeasuredSets μ | ∃ c ∈ C, (↑s : Set α) = c}
C'C : ∀ (s : MeasuredSets μ) (hs : s ∈ C'), (↑s : Set α) ∈ C
C'_dense : Dense C'
m₀ : (↑C' : Type u_1) → E := fun (x : (↑C' : Type u_1)) ↦ (m : (a : Set α) → E) (↑(↑x : MeasuredSets μ) : Set α)
s t : (↑C' : Type u_1)
this : edist s t = edist (↑s : MeasuredSets μ) (↑t : MeasuredSets μ)
Is :
  (↑(↑s : MeasuredSets μ) : Set α) ∩ (↑(↑t : MeasuredSets μ) : Set α) ∪
      (↑(↑s : MeasuredSets μ) : Set α) \ (↑(↑t : MeasuredSets μ) : Set α) =
    (↑(↑s : MeasuredSets μ) : Set α)
It :
  (↑(↑t : MeasuredSets μ) : Set α) ∩ (↑(↑s : MeasuredSets μ) : Set α) ∪
      (↑(↑t : MeasuredSets μ) : Set α) \ (↑(↑s : MeasuredSets μ) : Set α) =
    (↑(↑t : MeasuredSets μ) : Set α)
nth_rewrite :
  ‖HSub.hSub (α := E) (β := E)
        ((m : (a : Set α) → E)
            ((↑(↑s : MeasuredSets μ) : Set α) ∩ (↑(↑t : MeasuredSets μ) : Set α) ∪
              (↑(↑s : MeasuredSets μ) : Set α) \ (↑(↑t : MeasuredSets μ) : Set α)) :
          E)
        ((m : (a : Set α) → E) (↑(↑t : MeasuredSets μ) : Set α) : E)‖ₑ ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) ((↑(↑s : MeasuredSets μ) : Set α) \ (↑(↑t : MeasuredSets μ) : Set α)) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) ((↑(↑t : MeasuredSets μ) : Set α) \ (↑(↑s : MeasuredSets μ) : Set α)) : ℝ≥0∞)
⊢ ‖HSub.hSub (α := E) (β := E) ((m : (a : Set α) → E) (↑(↑s : MeasuredSets μ) : Set α) : E)
        ((m : (a : Set α) → E) (↑(↑t : MeasuredSets μ) : Set α) : E)‖ₑ ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) ((↑(↑s : MeasuredSets μ) : Set α) \ (↑(↑t : MeasuredSets μ) : Set α)) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) ((↑(↑t : MeasuredSets μ) : Set α) \ (↑(↑s : MeasuredSets μ) : Set α)) : ℝ≥0∞)

Tactic:
nth_rewrite 1 [← Is]