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 α
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 α) ∩ (↑(↑s : MeasuredSets μ) : Set α) ∪
              (↑(↑t : MeasuredSets μ) : Set α) \ (↑(↑s : 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 α) ∩ (↑(↑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∞)

Tactic:
nth_rewrite 3 [← It]
-- 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 α)
simp :
  ‖HSub.hSub (α := E) (β := E)
        ((m : (a : Set α) → E) ((↑(↑s : MeasuredSets μ) : Set α) \ (↑(↑t : MeasuredSets μ) : Set α)) : E)
        ((m : (a : Set α) → E) ((↑(↑t : MeasuredSets μ) : Set α) \ (↑(↑s : 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∞)
⊢ ‖HAdd.hAdd (α := E) (β := E)
          ((m : (a : Set α) → E) ((↑(↑t : MeasuredSets μ) : Set α) ∩ (↑(↑s : MeasuredSets μ) : Set α)) : E)
          ((m : (a : Set α) → E) ((↑(↑s : MeasuredSets μ) : Set α) \ (↑(↑t : MeasuredSets μ) : Set α)) : E) -
        HAdd.hAdd (α := E) (β := E)
          ((m : (a : Set α) → E) ((↑(↑t : MeasuredSets μ) : Set α) ∩ (↑(↑s : MeasuredSets μ) : Set α)) : E)
          ((m : (a : Set α) → E) ((↑(↑t : MeasuredSets μ) : Set α) \ (↑(↑s : 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:
simp only [add_sub_add_left_eq_sub, ge_iff_le]

Premises used: ge_iff_le, add_sub_add_left_eq_sub
-- 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 α)
apply :
  enorm.{u_2} (E := E)
        ((m : (a : Set α) → E) ((↑(↑s : MeasuredSets μ) : Set α) \ (↑(↑t : MeasuredSets μ) : Set α)) : E) +
      enorm.{u_2} (E := E)
        ((m : (a : Set α) → E) ((↑(↑t : MeasuredSets μ) : Set α) \ (↑(↑s : 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 α) \ (↑(↑t : MeasuredSets μ) : Set α)) : E)
        ((m : (a : Set α) → E) ((↑(↑t : MeasuredSets μ) : Set α) \ (↑(↑s : 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:
apply enorm_sub_le.trans

Premises used: enorm_sub_le, LE.le.trans
-- 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 α)
h₁ :
  enorm.{u_2} (E := E)
      ((m : (a : Set α) → E) ((↑(↑s : MeasuredSets μ) : Set α) \ (↑(↑t : MeasuredSets μ) : Set α)) : E) ≤
    (μ : (a : Set α) → ℝ≥0∞) ((↑(↑s : MeasuredSets μ) : Set α) \ (↑(↑t : MeasuredSets μ) : Set α))
h₂ :
  enorm.{u_2} (E := E)
      ((m : (a : Set α) → E) ((↑(↑t : MeasuredSets μ) : Set α) \ (↑(↑s : MeasuredSets μ) : Set α)) : E) ≤
    (μ : (a : Set α) → ℝ≥0∞) ((↑(↑t : MeasuredSets μ) : Set α) \ (↑(↑s : MeasuredSets μ) : Set α))
⊢ enorm.{u_2} (E := E)
        ((m : (a : Set α) → E) ((↑(↑s : MeasuredSets μ) : Set α) \ (↑(↑t : MeasuredSets μ) : Set α)) : E) +
      enorm.{u_2} (E := E)
        ((m : (a : Set α) → E) ((↑(↑t : MeasuredSets μ) : Set α) \ (↑(↑s : 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:
gcongr
-- 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 α)
⊢ enorm.{u_2} (E := E)
      ((m : (a : Set α) → E) ((↑(↑s : MeasuredSets μ) : Set α) \ (↑(↑t : MeasuredSets μ) : Set α)) : E) ≤
    (μ : (a : Set α) → ℝ≥0∞) ((↑(↑s : MeasuredSets μ) : Set α) \ (↑(↑t : MeasuredSets μ) : Set α))

Tactic:
hm _ (hC.diff_mem (C'C _ s.2) (C'C _ t.2))

Premises used: MeasureTheory.IsSetRing.diff_mem, 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 μ)
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 α)
⊢ enorm.{u_2} (E := E)
      ((m : (a : Set α) → E) ((↑(↑s : MeasuredSets μ) : Set α) \ (↑(↑t : MeasuredSets μ) : Set α)) : E) ≤
    (μ : (a : Set α) → ℝ≥0∞) ((↑(↑s : MeasuredSets μ) : Set α) \ (↑(↑t : MeasuredSets μ) : Set α))

Tactic:
exact hm _ (hC.diff_mem (C'C _ s.2) (C'C _ t.2))

Premises used: MeasureTheory.IsSetRing.diff_mem, 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 μ)
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 α)
⊢ enorm.{u_2} (E := E)
      ((m : (a : Set α) → E) ((↑(↑t : MeasuredSets μ) : Set α) \ (↑(↑s : MeasuredSets μ) : Set α)) : E) ≤
    (μ : (a : Set α) → ℝ≥0∞) ((↑(↑t : MeasuredSets μ) : Set α) \ (↑(↑s : MeasuredSets μ) : Set α))

Tactic:
hm _ (hC.diff_mem (C'C _ t.2) (C'C _ s.2))

Premises used: MeasureTheory.IsSetRing.diff_mem, 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 μ)
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 α)
⊢ enorm.{u_2} (E := E)
      ((m : (a : Set α) → E) ((↑(↑t : MeasuredSets μ) : Set α) \ (↑(↑s : MeasuredSets μ) : Set α)) : E) ≤
    (μ : (a : Set α) → ℝ≥0∞) ((↑(↑t : MeasuredSets μ) : Set α) \ (↑(↑s : MeasuredSets μ) : Set α))

Tactic:
exact hm _ (hC.diff_mem (C'C _ t.2) (C'C _ s.2))

Premises used: MeasureTheory.IsSetRing.diff_mem, 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 α)
⊢ LipschitzWith 1 m₀

Tactic:
have lip : LipschitzWith 1 m₀ := by
    intro s t
    have : edist s t = edist (s : MeasuredSets μ) t := rfl
    simp only [ENNReal.coe_one, one_mul, this, MeasuredSets.edist_def, m₀, edist_eq_enorm_sub]
    rw [measure_symmDiff_eq (by exact s.1.2.nullMeasurableSet) (by exact t.1.2.nullMeasurableSet)]
    have Is : ((s : Set α) ∩ t) ∪ (s \ t) = (s : Set α) := Set.inter_union_diff _ _
    have It : ((t : Set α) ∩ s) ∪ (t \ s) = (t : Set α) := Set.inter_union_diff _ _
    nth_rewrite 1 [← Is]
    nth_rewrite 3 [← It]
    rw [addContent_union hC (hC.inter_mem (C'C _ t.2) (C'C _ s.2))
        (hC.diff_mem (C'C _ t.2) (C'C _ s.2)) Set.disjoint_sdiff_inter.symm,
      addContent_union hC (hC.inter_mem (C'C _ s.2) (C'C _ t.2))
        (hC.diff_mem (C'C _ s.2) (C'C _ t.2)) Set.disjoint_sdiff_inter.symm, Set.inter_comm]
    simp only [add_sub_add_left_eq_sub, ge_iff_le]
    apply enorm_sub_le.trans
    gcongr
    · exact hm _ (hC.diff_mem (C'C _ s.2) (C'C _ t.2))
    · exact hm _ (hC.diff_mem (C'C _ t.2) (C'C _ s.2))
-- 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 α)
lip : LipschitzWith 1 m₀
m₁ : MeasuredSets μ → E := C'_dense.extend (s := C') m₀
⊢ LipschitzWith 1 m₁

Tactic:
have m₁_lip : LipschitzWith 1 m₁ := C'_dense.lipschitzWith_extend lip
-- 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 α)
lip : LipschitzWith 1 m₀
m₁ : MeasuredSets μ → E := C'_dense.extend (s := C') m₀
m₁_lip : LipschitzWith 1 m₁
⊢ IsClosed.{u_1} (X := MeasuredSets μ) {s : MeasuredSets μ | ‖m₁ s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) (↑s : Set α)}

Tactic:
have : IsClosed {s | ‖m₁ s‖ₑ ≤ μ s} :=
      isClosed_le m₁_lip.continuous.enorm MeasuredSets.continuous_measure
-- 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 α)
lip : LipschitzWith 1 m₀
m₁ : MeasuredSets μ → E := C'_dense.extend (s := C') m₀
m₁_lip : LipschitzWith 1 m₁
this : IsClosed.{u_1} (X := MeasuredSets μ) {s : MeasuredSets μ | ‖m₁ s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) (↑s : Set α)}
apply : C' ⊆ {s : MeasuredSets μ | ‖m₁ s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) (↑s : Set α)}
⊢ Dense.{u_1} (X := MeasuredSets μ) {s : MeasuredSets μ | ‖m₁ s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) (↑s : Set α)}

Tactic:
apply C'_dense.mono

Premises used: Dense.mono
-- 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 α)
lip : LipschitzWith 1 m₀
m₁ : MeasuredSets μ → E := C'_dense.extend (s := C') m₀
m₁_lip : LipschitzWith 1 m₁
this : IsClosed.{u_1} (X := MeasuredSets μ) {s : MeasuredSets μ | ‖m₁ s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) (↑s : Set α)}
s : MeasuredSets μ
hs : s ∈ C'
⊢ enorm.{u_2} (E := E) ((m : (a : Set α) → E) (↑s : Set α) : E) ≤ (μ : (a : Set α) → ℝ≥0∞) (↑s : Set α)

Tactic:
hm s (C'C s hs)

Premises used: SetLike.coe
-- 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 α)
lip : LipschitzWith 1 m₀
m₁ : MeasuredSets μ → E := C'_dense.extend (s := C') m₀
m₁_lip : LipschitzWith 1 m₁
this : IsClosed.{u_1} (X := MeasuredSets μ) {s : MeasuredSets μ | ‖m₁ s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) (↑s : Set α)}
s : MeasuredSets μ
hs : s ∈ C'
h : m₁ s = (m : (a : Set α) → E) (↑s : Set α)
⊢ ‖m₁ s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) (↑s : Set α)

Tactic:
convert! hm s (C'C s hs)

Premises used: SetLike.coe