-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
inst_1 : PartialOrder G
inst_2 : CanonicallyOrderedAdd G
m : AddContent G C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
h_mem : ⋃₀ (↑J : Set (Set α)) ∈ C
have : (↑(J.disjiUnion (hC.disjointOfUnion (C := C) h_ss) ⋯) : Set (Set α)) ⊆ C
have₁ :
  ∀ (h1 : (↑(J.disjiUnion (hC.disjointOfUnion (C := C) h_ss) ⋯) : Set (Set α)) ⊆ C),
    LE.le.{u_2} (α := G) ((m : (a : Set α) → G) (⋃₀ (↑J : Set (Set α))) : G) (∑ u ∈ J, (m : (a : Set α) → G) u : G)
have₂ : (↑(J.disjiUnion (hC.disjointOfUnion (C := C) h_ss) ⋯) : Set (Set α)) ⊆ C
have₃ have₄ :
  ∀ (h1 : (↑(J.disjiUnion (hC.disjointOfUnion (C := C) h_ss) ⋯) : Set (Set α)) ⊆ C),
    LE.le.{u_2} (α := G) ((m : (a : Set α) → G) (⋃₀ (↑J : Set (Set α))) : G) (∑ u ∈ J, (m : (a : Set α) → G) u : G)
have₅ :
  ∀ (h1 : (↑(J.disjiUnion (hC.disjointOfUnion (C := C) h_ss) ⋯) : Set (Set α)) ⊆ C)
    (h2 : (↑(J.disjiUnion (hC.disjointOfUnion (C := C) h_ss) ⋯) : Set (Set α)).PairwiseDisjoint id),
    LE.le.{u_2} (α := G) ((m : (a : Set α) → G) (⋃₀ (↑J : Set (Set α))) : G) (∑ u ∈ J, (m : (a : Set α) → G) u : G)
have₆ :
  ∀ (h1 : (↑(J.disjiUnion (hC.disjointOfUnion (C := C) h_ss) ⋯) : Set (Set α)) ⊆ C)
    (h2 : (↑(J.disjiUnion (hC.disjointOfUnion (C := C) h_ss) ⋯) : Set (Set α)).PairwiseDisjoint id)
    (h3 : ⋃₀ (↑J : Set (Set α)) = ⋃₀ (↑(J.disjiUnion (hC.disjointOfUnion (C := C) h_ss) ⋯) : Set (Set α))),
    LE.le.{u_2} (α := G) ((m : (a : Set α) → G) (⋃₀ (↑J : Set (Set α))) : G) (∑ u ∈ J, (m : (a : Set α) → G) u : G)
have₇ :
  ∀ (h1 : (↑(J.disjiUnion (hC.disjointOfUnion (C := C) h_ss) ⋯) : Set (Set α)) ⊆ C)
    (h2 : (↑(J.disjiUnion (hC.disjointOfUnion (C := C) h_ss) ⋯) : Set (Set α)).PairwiseDisjoint id)
    (h3 : ⋃₀ (↑J : Set (Set α)) = ⋃₀ (↑(J.disjiUnion (hC.disjointOfUnion (C := C) h_ss) ⋯) : Set (Set α))),
    LE.le.{u_2} (α := G) (∑ i ∈ J, ∑ x ∈ hC.disjointOfUnion (C := C) h_ss i, (m : (a : Set α) → G) x)
      (∑ u ∈ J, (m : (a : Set α) → G) u)
have₈ have₉ :
  ∀ (h1 : (↑(J.disjiUnion (hC.disjointOfUnion (C := C) h_ss) ⋯) : Set (Set α)) ⊆ C)
    (h2 : (↑(J.disjiUnion (hC.disjointOfUnion (C := C) h_ss) ⋯) : Set (Set α)).PairwiseDisjoint id)
    (h3 : ⋃₀ (↑J : Set (Set α)) = ⋃₀ (↑(J.disjiUnion (hC.disjointOfUnion (C := C) h_ss) ⋯) : Set (Set α))),
    ⋃₀ (↑(J.disjiUnion (hC.disjointOfUnion (C := C) h_ss) ⋯) : Set (Set α)) ∈ C
⊢ LE.le.{u_2} (α := G) ((m : (a : Set α) → G) (⋃₀ (↑J : Set (Set α))) : G) (∑ u ∈ J, (m : (a : Set α) → G) u : G)

Tactic:
classical
  have h1 : (disjiUnion J (hC.disjointOfUnion h_ss)
      (hC.pairwiseDisjoint_disjointOfUnion h_ss) : Set (Set α)) ⊆ C := by
    simp only [disjiUnion_eq_biUnion, coe_biUnion, mem_coe, iUnion_subset_iff]
    exact fun _ x ↦ hC.disjointOfUnion_subset h_ss x
  have h2 : PairwiseDisjoint (disjiUnion J (hC.disjointOfUnion h_ss)
      ((hC.pairwiseDisjoint_disjointOfUnion h_ss)) : Set (Set α)) id := by
    simp only [disjiUnion_eq_biUnion, coe_biUnion, mem_coe]
    exact hC.pairwiseDisjoint_biUnion_disjointOfUnion h_ss
  have h3 : ⋃₀ J = ⋃₀ ((disjiUnion J (hC.disjointOfUnion h_ss)
      (hC.pairwiseDisjoint_disjointOfUnion h_ss)) : Set (Set α)) := by
    simp only [disjiUnion_eq_biUnion, coe_biUnion, mem_coe]
    exact (Exists.choose_spec (hC.disjointOfUnion_props h_ss)).2.2.2.2.2
  rw [h3, addContent_sUnion h1 h2, sum_disjiUnion]
  · gcongr with x hx
    refine sum_addContent_le_of_subset hC (hC.disjointOfUnion_subset h_ss hx)
      (hC.pairwiseDisjoint_disjointOfUnion_of_mem h_ss hx) (h_ss hx)
      (fun _ s ↦ hC.subset_of_mem_disjointOfUnion h_ss hx s)
  · simp only [disjiUnion_eq_biUnion, coe_biUnion, mem_coe] at *
    exact h3.symm ▸ h_mem

Premises used: Finset.coe_biUnion, Finset.disjiUnion_eq_biUnion, Finset.sum_disjiUnion, Finset.mem_coe