-- 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 α)
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∞)
⊢ ‖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:
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]

Premises used: Set.disjoint_sdiff_inter, MeasureTheory.IsSetRing.inter_mem, Set.inter_comm, MeasureTheory.addContent_union, Disjoint.symm, MeasureTheory.IsSetRing.diff_mem, Subtype.property