awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.AddContent (hypothesis)
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 μ)
⊢ ‖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∞)
have Is : (↑(↑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 _ _
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.AddContent (hypothesis)
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 α)
⊢ ‖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∞)
have It : (↑(↑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 _ _
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.AddContent (goal)
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 α)
⊢ ‖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∞)
have 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∞)
Tactic: nth_rewrite 1 [← Is]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.AddContent (goal)
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 α)
⊢ ‖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∞)
have 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∞)
Tactic: nth_rewrite 3 [← It]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.AddContent (goal)
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 α)
⊢ ‖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∞)
have rw : ‖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: 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.AddContent (goal)
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 α)
⊢ ‖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∞)
have 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∞)
Tactic: simp only [add_sub_add_left_eq_sub, ge_iff_le]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.AddContent (goal)
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 α)
⊢ ‖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∞)
have 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∞)
Tactic: apply enorm_sub_le.trans
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.AddContent (goal)
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) +
      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∞)
have 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 α))
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.AddContent (goal)
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 α))
⊢ 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∞)
have 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 α))
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.AddContent (hypothesis)
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 α)
⊢ ∃ (m' : VectorMeasure α E),
    (∀ s ∈ C, (↑m' : Set α → E) s = (m : (a : Set α) → E) s) ∧
      ∀ (s : Set α), ‖(↑m' : Set α → E) s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) s
have lip : 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))
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.AddContent (hypothesis)
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' : VectorMeasure α E),
    (∀ s ∈ C, (↑m' : Set α → E) s = (m : (a : Set α) → E) s) ∧
      ∀ (s : Set α), ‖(↑m' : Set α → E) s‖ₑ ≤ (μ : (a : Set α) → ℝ≥0∞) s
have m₁_lip : LipschitzWith 1 m₁
Tactic: have m₁_lip : LipschitzWith 1 m₁ := C'_dense.lipschitzWith_extend lip