-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t s : Set α
ht : NullMeasurableSet t μ
rw :
  HAdd.hAdd (β := ℝ≥0∞)
      (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((s ∪ t) ∩ t) : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) ((s ∪ t) \ t) : ℝ≥0∞))
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
rw₁ :
  HAdd.hAdd (β := ℝ≥0∞)
      (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) ((s ∪ t) \ t) : ℝ≥0∞))
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
rw₂ :
  HAdd.hAdd (β := ℝ≥0∞)
      (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞))
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
rw₃ :
  HAdd.hAdd (β := ℝ≥0∞)
      (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞))
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) =
    HAdd.hAdd (β := ℝ≥0∞)
      (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞))
      ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
rw₄ :
  HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
      (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞)) =
    HAdd.hAdd (β := ℝ≥0∞)
      (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞))
      ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
rw₅ :
  HAdd.hAdd (β := ℝ≥0∞)
      (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞))
      ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) =
    HAdd.hAdd (β := ℝ≥0∞)
      (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞))
      ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
rw₆ rw₇ :
  HAdd.hAdd (β := ℝ≥0∞)
      (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞))
      ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) =
    HAdd.hAdd (β := ℝ≥0∞)
      (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞))
      ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
rw [← measure_inter_add_diff₀ (s ∪ t) ht, union_inter_cancel_right, union_diff_right, ←
    measure_inter_add_diff₀ s ht, add_comm, ← add_assoc, add_right_comm]

Premises used: MeasureTheory.measure_inter_add_diff₀, add_assoc, add_right_comm, add_comm, Set.union_diff_right, Union.union, Set.union_inter_cancel_right