-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
ι : Type u_3
a : Finset ι
f : ι → Set α
hf : ∀ i ∈ a, f i ∈ C
h_dis : (↑a : Set ι).PairwiseDisjoint f
h_mem : ⋃ i ∈ a, f i ∈ C
have : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))
have₁ :
  ∀ (A : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))),
    Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (⋃ i ∈ a, f i) : G) (∑ i ∈ a, (m : (a : Set α) → G) (f i) : G)
have₂ : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))
have₃ have₄ :
  ∀ (A : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))),
    Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (⋃ i ∈ a, f i) : G) (∑ i ∈ a, (m : (a : Set α) → G) (f i) : G)
have₅ :
  ∀ (A : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))),
    Eq.{u_2 + 1} (α := G) (∑ u ∈ Finset.image f a, (m : (a : Set α) → G) u) (∑ i ∈ a, (m : (a : Set α) → G) (f i))
h_ss : ∀ (A : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))), (↑(Finset.image f a) : Set (Set α)) ⊆ C
h_dis₁ :
  ∀ (A : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))), (↑(Finset.image f a) : Set (Set α)).PairwiseDisjoint id
h_mem₁ : ∀ (A : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))), ⋃₀ (↑(Finset.image f a) : Set (Set α)) ∈ C
have₆ :
  ∀ (A : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))),
    Eq.{u_2 + 1} (α := G) (∑ u ∈ Finset.image f a, (m : (a : Set α) → G) u) (∑ i ∈ a, (m : (a : Set α) → G) (f i))
h_ss₁ : ∀ (A : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))), (↑(Finset.image f a) : Set (Set α)) ⊆ C
h_dis₂ :
  ∀ (A : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))), (↑(Finset.image f a) : Set (Set α)).PairwiseDisjoint id
h_mem₂ : ∀ (A : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))), ⋃₀ (↑(Finset.image f a) : Set (Set α)) ∈ C
h_ss₂ : ∀ (A : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))), (↑(Finset.image f a) : Set (Set α)) ⊆ C
h_dis₃ :
  ∀ (A : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))), (↑(Finset.image f a) : Set (Set α)).PairwiseDisjoint id
h_mem₃ : ∀ (A : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))), ⋃₀ (↑(Finset.image f a) : Set (Set α)) ∈ C
have₇ :
  ∀ (A : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))),
    Eq.{u_2 + 1} (α := G) (∑ u ∈ Finset.image f a, (m : (a : Set α) → G) u) (∑ i ∈ a, (m : (a : Set α) → G) (f i))
h_dis₄ :
  ∀ (A : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))), (↑(Finset.image f a) : Set (Set α)).PairwiseDisjoint id
h_mem₄ : ∀ (A : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))), ⋃₀ (↑(Finset.image f a) : Set (Set α)) ∈ C
have₈ :
  ∀ (A : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))),
    Eq.{u_2 + 1} (α := G) (∑ u ∈ Finset.image f a, (m : (a : Set α) → G) u) (∑ i ∈ a, (m : (a : Set α) → G) (f i))
h_mem₅ : ∀ (A : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))), ⋃₀ (↑(Finset.image f a) : Set (Set α)) ∈ C
have₉ have₁₀ :
  ∀ (A : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))),
    Eq.{u_2 + 1} (α := G) (∑ u ∈ Finset.image f a, (m : (a : Set α) → G) u) (∑ i ∈ a, (m : (a : Set α) → G) (f i))
have₁₁ :
  ∀ (A : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))),
    (↑a : Set ι).Pairwise fun (i j : ι) ↦ f i = f j → Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (f i) : G) (0 : G)
⊢ Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (⋃ i ∈ a, f i) : G) (∑ i ∈ a, (m : (a : Set α) → G) (f i) : G)
have have₁₂ : ∀ (A : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))) ⦃a b : ι⦄,
  (Disjoint on f) a b → f a = f b → Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (f a) : G) (0 : G)
Tactic: classical
  have A : ⋃ i ∈ a, f i = ⋃₀ (a.image f) := by simp
  rw [A, addContent_sUnion]; rotate_left
  · grind
  · simpa using h_dis.image
  · rwa [← A]
  rw [sum_image_of_pairwise_eq_zero]
  refine h_dis.imp ?_
  grind [Set.bot_eq_empty (α := α), addContent_empty]