awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hC : IsSetRing C
s : ι → Set α
S : Finset ι
hs : ∀ n ∈ S, s n ∈ C
hS : (↑S : Set ι).PairwiseDisjoint s
⊢ Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (⋃ i ∈ S, s i) : G) (∑ i ∈ S, (m : (a : Set α) → G) (s i) : G)
have empty : ∀ (hs : ∀ (n : ι), Membership.mem (γ := Finset ι) ∅ n → s n ∈ C) (hS : (↑∅ : Set ι).PairwiseDisjoint s),
  Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), s i) : G)
    (∑ i ∈ ∅, (m : (a : Set α) → G) (s i) : G)
Tactic: induction S using Finset.induction with
  | empty => simp
  | insert i S hiS h =>
    rw [Finset.sum_insert hiS]
    simp_rw [← Finset.mem_coe, Finset.coe_insert, Set.biUnion_insert]
    simp only [Finset.mem_insert, forall_eq_or_imp] at hs
    simp only [Finset.coe_insert, Set.pairwiseDisjoint_insert] at hS
    rw [← h hs.2 hS.1]
    refine addContent_union hC hs.1 (hC.biUnion_mem S hs.2) ?_
    rw [disjoint_iUnion₂_right]
    exact fun j hjS ↦ hS.2 j hjS (ne_of_mem_of_not_mem hjS hiS).symm
Cleared hypotheses: S, hs, hS
-- 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
hC : IsSetRing C
s : ι → Set α
S : Finset ι
hs : ∀ n ∈ S, s n ∈ C
hS : (↑S : Set ι).PairwiseDisjoint s
empty :
  ∀ (hs : ∀ (n : ι), Membership.mem (γ := Finset ι) ∅ n → s n ∈ C) (hS : (↑∅ : Set ι).PairwiseDisjoint s),
    Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), s i) : G)
      (∑ i ∈ ∅, (m : (a : Set α) → G) (s i) : G)
⊢ Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (⋃ i ∈ S, s i) : G) (∑ i ∈ S, (m : (a : Set α) → G) (s i) : G)
have insert : ∀ (i : ι) (S : Finset ι) (hiS : i ∉ S)
  (h :
    ∀ (hs : ∀ n ∈ S, s n ∈ C) (hS : (↑S : Set ι).PairwiseDisjoint s),
      Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (⋃ i ∈ S, s i) : G) (∑ i ∈ S, (m : (a : Set α) → G) (s i) : G))
  (hs : ∀ n ∈ insert i S, s n ∈ C) (hS : (↑(insert i S) : Set ι).PairwiseDisjoint s),
  Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (⋃ i_1 ∈ insert i S, s i_1) : G)
    (∑ i ∈ insert i S, (m : (a : Set α) → G) (s i) : G)
Tactic: induction S using Finset.induction with
  | empty => simp
  | insert i S hiS h =>
    rw [Finset.sum_insert hiS]
    simp_rw [← Finset.mem_coe, Finset.coe_insert, Set.biUnion_insert]
    simp only [Finset.mem_insert, forall_eq_or_imp] at hs
    simp only [Finset.coe_insert, Set.pairwiseDisjoint_insert] at hS
    rw [← h hs.2 hS.1]
    refine addContent_union hC hs.1 (hC.biUnion_mem S hs.2) ?_
    rw [disjoint_iUnion₂_right]
    exact fun j hjS ↦ hS.2 j hjS (ne_of_mem_of_not_mem hjS hiS).symm
Cleared hypotheses: S, hs, hS
-- 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
hC : IsSetRing C
s : ι → Set α
S : Finset ι
hs : ∀ n ∈ S, s n ∈ C
hS : (↑S : Set ι).PairwiseDisjoint s
⊢ Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (⋃ i ∈ S, s i) : G) (∑ i ∈ S, (m : (a : Set α) → G) (s i) : G)
have empty : ∀ (hs : ∀ (n : ι), Membership.mem (γ := Finset ι) ∅ n → s n ∈ C) (hS : (↑∅ : Set ι).PairwiseDisjoint s),
  Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), s i) : G)
    (∑ i ∈ ∅, (m : (a : Set α) → G) (s i) : G)
Tactic: classical
  induction S using Finset.induction with
  | empty => simp
  | insert i S hiS h =>
    rw [Finset.sum_insert hiS]
    simp_rw [← Finset.mem_coe, Finset.coe_insert, Set.biUnion_insert]
    simp only [Finset.mem_insert, forall_eq_or_imp] at hs
    simp only [Finset.coe_insert, Set.pairwiseDisjoint_insert] at hS
    rw [← h hs.2 hS.1]
    refine addContent_union hC hs.1 (hC.biUnion_mem S hs.2) ?_
    rw [disjoint_iUnion₂_right]
    exact fun j hjS ↦ hS.2 j hjS (ne_of_mem_of_not_mem hjS hiS).symm
Cleared hypotheses: S, hs, hS
-- 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
hC : IsSetRing C
s : ι → Set α
S : Finset ι
hs : ∀ n ∈ S, s n ∈ C
hS : (↑S : Set ι).PairwiseDisjoint s
empty :
  ∀ (hs : ∀ (n : ι), Membership.mem (γ := Finset ι) ∅ n → s n ∈ C) (hS : (↑∅ : Set ι).PairwiseDisjoint s),
    Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), s i) : G)
      (∑ i ∈ ∅, (m : (a : Set α) → G) (s i) : G)
⊢ Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (⋃ i ∈ S, s i) : G) (∑ i ∈ S, (m : (a : Set α) → G) (s i) : G)
have insert : ∀ (i : ι) (S : Finset ι) (hiS : i ∉ S)
  (h :
    ∀ (hs : ∀ n ∈ S, s n ∈ C) (hS : (↑S : Set ι).PairwiseDisjoint s),
      Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (⋃ i ∈ S, s i) : G) (∑ i ∈ S, (m : (a : Set α) → G) (s i) : G))
  (hs : ∀ n ∈ insert i S, s n ∈ C) (hS : (↑(insert i S) : Set ι).PairwiseDisjoint s),
  Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (⋃ i_1 ∈ insert i S, s i_1) : G)
    (∑ i ∈ insert i S, (m : (a : Set α) → G) (s i) : G)
Tactic: classical
  induction S using Finset.induction with
  | empty => simp
  | insert i S hiS h =>
    rw [Finset.sum_insert hiS]
    simp_rw [← Finset.mem_coe, Finset.coe_insert, Set.biUnion_insert]
    simp only [Finset.mem_insert, forall_eq_or_imp] at hs
    simp only [Finset.coe_insert, Set.pairwiseDisjoint_insert] at hS
    rw [← h hs.2 hS.1]
    refine addContent_union hC hs.1 (hC.biUnion_mem S hs.2) ?_
    rw [disjoint_iUnion₂_right]
    exact fun j hjS ↦ hS.2 j hjS (ne_of_mem_of_not_mem hjS hiS).symm
Cleared hypotheses: S, hs, hS
-- 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
hC : IsSetRing C
s : ℕ → Set α
hs_disj : Pairwise (Disjoint on s)
hsC : ∀ (i : ℕ), s i ∈ C
n : ℕ
hn :
  Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (accumulate s n) : G)
    (∑ i ∈ Finset.range (n + 1), (m : (a : Set α) → G) (s i) : G)
⊢ Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (accumulate s (n + 1)) : G)
    (∑ i ∈ Finset.range (n + 1 + 1), (m : (a : Set α) → G) (s i) : G)
have succ : Disjoint (accumulate s n) (s (n + 1))
Tactic: rw [Finset.sum_range_succ, ← hn, Set.accumulate_succ, addContent_union hC _ (hsC _)]
-- 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
hC : IsSetRing C
s : ℕ → Set α
hs_disj : Pairwise (Disjoint on s)
hsC : ∀ (i : ℕ), s i ∈ C
n : ℕ
hn :
  Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (accumulate s n) : G)
    (∑ i ∈ Finset.range (n + 1), (m : (a : Set α) → G) (s i) : G)
succ : Disjoint (accumulate s n) (s (n + 1))
⊢ Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (accumulate s (n + 1)) : G)
    (∑ i ∈ Finset.range (n + 1 + 1), (m : (a : Set α) → G) (s i) : G)
have rw : accumulate s n ∈ C
Tactic: rw [Finset.sum_range_succ, ← hn, Set.accumulate_succ, addContent_union hC _ (hsC _)]
-- 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
hC : IsSetRing C
s : ℕ → Set α
hs_disj : Pairwise (Disjoint on s)
hsC : ∀ (i : ℕ), s i ∈ C
n : ℕ
⊢ Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (accumulate s n) : G)
    (∑ i ∈ Finset.range (n + 1), (m : (a : Set α) → G) (s i) : G)
have zero : Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (accumulate s 0) : G)
  (∑ i ∈ Finset.range (HAdd.hAdd (α := ℕ) 0 1), (m : (a : Set α) → G) (s i) : G)
Tactic: induction n with
  | zero => simp
  | succ n hn =>
    rw [Finset.sum_range_succ, ← hn, Set.accumulate_succ, addContent_union hC _ (hsC _)]
    · exact Set.disjoint_accumulate hs_disj (Nat.lt_succ_self n)
    · exact hC.accumulate_mem hsC n
Cleared hypotheses: n
-- 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
hC : IsSetRing C
s : ℕ → Set α
hs_disj : Pairwise (Disjoint on s)
hsC : ∀ (i : ℕ), s i ∈ C
n : ℕ
zero :
  Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (accumulate s 0) : G)
    (∑ i ∈ Finset.range (HAdd.hAdd (α := ℕ) 0 1), (m : (a : Set α) → G) (s i) : G)
⊢ Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (accumulate s n) : G)
    (∑ i ∈ Finset.range (n + 1), (m : (a : Set α) → G) (s i) : G)
have succ : ∀ (n : ℕ)
  (hn :
    Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (accumulate s n) : G)
      (∑ i ∈ Finset.range (n + 1), (m : (a : Set α) → G) (s i) : G)),
  Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (accumulate s (n + 1)) : G)
    (∑ i ∈ Finset.range (n + 1 + 1), (m : (a : Set α) → G) (s i) : G)
Tactic: induction n with
  | zero => simp
  | succ n hn =>
    rw [Finset.sum_range_succ, ← hn, Set.accumulate_succ, addContent_union hC _ (hsC _)]
    · exact Set.disjoint_accumulate hs_disj (Nat.lt_succ_self n)
    · exact hC.accumulate_mem hsC n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
s_1 t : Set α
I_1 : Finset (Set α)
G : Type u_2
inst : AddCommMonoid G
m_1 m' : AddContent G C
m : Set α → G
hC : IsSetRing C
m_empty : m ∅ = 0
m_add : ∀ {s t : Set α} (_hs : s ∈ C) (_ht : t ∈ C), Disjoint s t → m (s ∪ t) = m s + m t
s : Set α
I : Finset (Set α)
hsI : s ∉ I
h :
  ∀ (h_ss : (↑I : Set (Set α)) ⊆ C) (h_dis : (↑I : Set (Set α)).PairwiseDisjoint id)
    (h_mem : ⋃₀ (↑I : Set (Set α)) ∈ C), m (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, m u
h_ss : (↑(insert s I) : Set (Set α)) ⊆ C
h_dis : (↑(insert s I) : Set (Set α)).PairwiseDisjoint id
h_mem : ⋃₀ (↑(insert s I) : Set (Set α)) ∈ C
⊢ m (⋃₀ (↑(insert s I) : Set (Set α))) = ∑ u ∈ insert s I, m u
have insert : ∀ (h_ss : insert s (↑I : Set (Set α)) ⊆ C) (h_dis : (insert s (↑I : Set (Set α))).PairwiseDisjoint id)
  (h_mem : ⋃₀ insert s (↑I : Set (Set α)) ∈ C), m (⋃₀ insert s (↑I : Set (Set α))) = ∑ u ∈ insert s I, m u
Tactic: rw [Finset.coe_insert] at *
Cleared hypotheses: h_ss, h_dis, h_mem
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (hypothesis)
Goal:
α : Type u_1
C : Set (Set α)
s_1 t : Set α
I_1 : Finset (Set α)
G : Type u_2
inst : AddCommMonoid G
m_1 m' : AddContent G C
m : Set α → G
hC : IsSetRing C
m_empty : m ∅ = 0
m_add : ∀ {s t : Set α} (_hs : s ∈ C) (_ht : t ∈ C), Disjoint s t → m (s ∪ t) = m s + m t
s : Set α
I : Finset (Set α)
hsI : s ∉ I
h :
  ∀ (h_ss : (↑I : Set (Set α)) ⊆ C) (h_dis : (↑I : Set (Set α)).PairwiseDisjoint id)
    (h_mem : ⋃₀ (↑I : Set (Set α)) ∈ C), m (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, m u
h_ss : insert s (↑I : Set (Set α)) ⊆ C
h_dis : (insert s (↑I : Set (Set α))).PairwiseDisjoint id
h_mem : ⋃₀ insert s (↑I : Set (Set α)) ∈ C
⊢ m (⋃₀ insert s (↑I : Set (Set α))) = ∑ u ∈ insert s I, m u
have h_ss₁ : s ∈ C ∧ (↑I : Set (Set α)) ⊆ C
Tactic: rw [Set.insert_subset_iff] at h_ss
Cleared hypotheses: h_ss, h_dis, h_mem
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
s_1 t : Set α
I_1 : Finset (Set α)
G : Type u_2
inst : AddCommMonoid G
m_1 m' : AddContent G C
m : Set α → G
hC : IsSetRing C
m_empty : m ∅ = 0
m_add : ∀ {s t : Set α} (_hs : s ∈ C) (_ht : t ∈ C), Disjoint s t → m (s ∪ t) = m s + m t
s : Set α
I : Finset (Set α)
hsI : s ∉ I
h :
  ∀ (h_ss : (↑I : Set (Set α)) ⊆ C) (h_dis : (↑I : Set (Set α)).PairwiseDisjoint id)
    (h_mem : ⋃₀ (↑I : Set (Set α)) ∈ C), m (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, m u
h_ss : s ∈ C ∧ (↑I : Set (Set α)) ⊆ C
h_dis : (insert s (↑I : Set (Set α))).PairwiseDisjoint id
h_mem : ⋃₀ insert s (↑I : Set (Set α)) ∈ C
⊢ m (⋃₀ insert s (↑I : Set (Set α))) = ∑ u ∈ insert s I, m u
have insert : ∀ (h_dis : (↑I : Set (Set α)).PairwiseDisjoint id ∧ ∀ j ∈ (↑I : Set (Set α)), Disjoint (id s) (id j))
  (h_mem : ⋃₀ insert s (↑I : Set (Set α)) ∈ C), m (⋃₀ insert s (↑I : Set (Set α))) = ∑ u ∈ insert s I, m u
Tactic: rw [Set.pairwiseDisjoint_insert_of_notMem] at h_dis
Cleared hypotheses: h_dis, h_mem
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
s_1 t : Set α
I_1 : Finset (Set α)
G : Type u_2
inst : AddCommMonoid G
m_1 m' : AddContent G C
m : Set α → G
hC : IsSetRing C
m_empty : m ∅ = 0
m_add : ∀ {s t : Set α} (_hs : s ∈ C) (_ht : t ∈ C), Disjoint s t → m (s ∪ t) = m s + m t
s : Set α
I : Finset (Set α)
hsI : s ∉ I
h :
  ∀ (h_ss : (↑I : Set (Set α)) ⊆ C) (h_dis : (↑I : Set (Set α)).PairwiseDisjoint id)
    (h_mem : ⋃₀ (↑I : Set (Set α)) ∈ C), m (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, m u
h_ss : s ∈ C ∧ (↑I : Set (Set α)) ⊆ C
h_dis : (Insert.insert s (↑I : Set (Set α))).PairwiseDisjoint id
h_mem : ⋃₀ Insert.insert s (↑I : Set (Set α)) ∈ C
insert :
  ∀ (h_dis : (↑I : Set (Set α)).PairwiseDisjoint id ∧ ∀ j ∈ (↑I : Set (Set α)), Disjoint (id s) (id j))
    (h_mem : ⋃₀ Insert.insert s (↑I : Set (Set α)) ∈ C),
    m (⋃₀ Insert.insert s (↑I : Set (Set α))) = ∑ u ∈ Insert.insert s I, m u
⊢ m (⋃₀ Insert.insert s (↑I : Set (Set α))) = ∑ u ∈ Insert.insert s I, m u
have insert₁ : s ∉ (↑I : Set (Set α))
Tactic: rw [Set.pairwiseDisjoint_insert_of_notMem] at h_dis
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
s_1 t : Set α
I_1 : Finset (Set α)
G : Type u_2
inst : AddCommMonoid G
m_1 m' : AddContent G C
m : Set α → G
hC : IsSetRing C
m_empty : m ∅ = 0
m_add : ∀ {s t : Set α} (_hs : s ∈ C) (_ht : t ∈ C), Disjoint s t → m (s ∪ t) = m s + m t
s : Set α
I : Finset (Set α)
hsI : s ∉ I
h :
  ∀ (h_ss : (↑I : Set (Set α)) ⊆ C) (h_dis : (↑I : Set (Set α)).PairwiseDisjoint id)
    (h_mem : ⋃₀ (↑I : Set (Set α)) ∈ C), m (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, m u
h_ss : s ∈ C ∧ (↑I : Set (Set α)) ⊆ C
h_dis : (↑I : Set (Set α)).PairwiseDisjoint id ∧ ∀ j ∈ (↑I : Set (Set α)), Disjoint (id s) (id j)
h_mem : ⋃₀ insert s (↑I : Set (Set α)) ∈ C
⊢ ⋃₀ (↑I : Set (Set α)) ∈ C
have rw : ⋃ i ∈ (↑I : Set (Set α)), i ∈ C
Tactic: rw [Set.sUnion_eq_biUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
s_1 t : Set α
I_1 : Finset (Set α)
G : Type u_2
inst : AddCommMonoid G
m_1 m' : AddContent G C
m : Set α → G
hC : IsSetRing C
m_empty : m ∅ = 0
m_add : ∀ {s t : Set α} (_hs : s ∈ C) (_ht : t ∈ C), Disjoint s t → m (s ∪ t) = m s + m t
s : Set α
I : Finset (Set α)
hsI : s ∉ I
h :
  ∀ (h_ss : (↑I : Set (Set α)) ⊆ C) (h_dis : (↑I : Set (Set α)).PairwiseDisjoint id)
    (h_mem : ⋃₀ (↑I : Set (Set α)) ∈ C), m (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, m u
h_ss : s ∈ C ∧ (↑I : Set (Set α)) ⊆ C
h_dis : (↑I : Set (Set α)).PairwiseDisjoint id ∧ ∀ j ∈ (↑I : Set (Set α)), Disjoint (id s) (id j)
h_mem : ⋃₀ insert s (↑I : Set (Set α)) ∈ C
⊢ ⋃ i ∈ (↑I : Set (Set α)), i ∈ C
have hs : ∀ n ∈ I, n ∈ C
Tactic: apply hC.biUnion_mem
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (hypothesis)
Goal:
α : Type u_1
C : Set (Set α)
s_1 t : Set α
I_1 : Finset (Set α)
G : Type u_2
inst : AddCommMonoid G
m_1 m' : AddContent G C
m : Set α → G
hC : IsSetRing C
m_empty : m ∅ = 0
m_add : ∀ {s t : Set α} (_hs : s ∈ C) (_ht : t ∈ C), Disjoint s t → m (s ∪ t) = m s + m t
s : Set α
I : Finset (Set α)
hsI : s ∉ I
h :
  ∀ (h_ss : (↑I : Set (Set α)) ⊆ C) (h_dis : (↑I : Set (Set α)).PairwiseDisjoint id)
    (h_mem : ⋃₀ (↑I : Set (Set α)) ∈ C), m (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, m u
h_ss : s ∈ C ∧ (↑I : Set (Set α)) ⊆ C
h_dis : (↑I : Set (Set α)).PairwiseDisjoint id ∧ ∀ j ∈ (↑I : Set (Set α)), Disjoint (id s) (id j)
h_mem : ⋃₀ insert s (↑I : Set (Set α)) ∈ C
⊢ m (⋃₀ insert s (↑I : Set (Set α))) = ∑ u ∈ insert s I, m u
have h_sUnion_mem : ⋃₀ (↑I : Set (Set α)) ∈ C
Tactic: have h_sUnion_mem : ⋃₀ ↑I ∈ C := by
        rw [Set.sUnion_eq_biUnion]
        apply hC.biUnion_mem
        intro n hn
        exact h_ss.2 hn
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
s_1 t : Set α
I_1 : Finset (Set α)
G : Type u_2
inst : AddCommMonoid G
m_1 m' : AddContent G C
m : Set α → G
hC : IsSetRing C
m_empty : m ∅ = 0
m_add : ∀ {s t : Set α} (_hs : s ∈ C) (_ht : t ∈ C), Disjoint s t → m (s ∪ t) = m s + m t
s : Set α
I : Finset (Set α)
hsI : s ∉ I
h :
  ∀ (h_ss : (↑I : Set (Set α)) ⊆ C) (h_dis : (↑I : Set (Set α)).PairwiseDisjoint id)
    (h_mem : ⋃₀ (↑I : Set (Set α)) ∈ C), m (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, m u
h_ss : s ∈ C ∧ (↑I : Set (Set α)) ⊆ C
h_dis : (↑I : Set (Set α)).PairwiseDisjoint id ∧ ∀ j ∈ (↑I : Set (Set α)), Disjoint (id s) (id j)
h_mem : ⋃₀ insert s (↑I : Set (Set α)) ∈ C
h_sUnion_mem : ⋃₀ (↑I : Set (Set α)) ∈ C
⊢ ⋃₀ (↑I : Set (Set α)) ∈ C
have insert : ∀ (h_mem : s ∪ ⋃₀ (↑I : Set (Set α)) ∈ C) (h_sUnion_mem : ⋃₀ (↑I : Set (Set α)) ∈ C), ⋃₀ (↑I : Set (Set α)) ∈ C
Tactic: rwa [Set.sUnion_insert] at h_mem
Cleared hypotheses: h_mem, h_sUnion_mem
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
I_1 : Finset (Set α)
G : Type u_2
inst : AddCommMonoid G
m_1 m' : AddContent G C
m : Set α → G
hC : IsSetRing C
m_empty : m ∅ = 0
m_add : ∀ {s t : Set α} (_hs : s ∈ C) (_ht : t ∈ C), Disjoint s t → m (s ∪ t) = m s + m t
I : Finset (Set α)
h_ss : (↑I : Set (Set α)) ⊆ C
h_dis : (↑I : Set (Set α)).PairwiseDisjoint id
h_mem : ⋃₀ (↑I : Set (Set α)) ∈ C
⊢ m (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, m u
have empty : ∀ (h_ss : (↑∅ : Set (Set α)) ⊆ C) (h_dis : (↑∅ : Set (Set α)).PairwiseDisjoint id) (h_mem : ⋃₀ (↑∅ : Set (Set α)) ∈ C),
  m (⋃₀ (↑∅ : Set (Set α))) = ∑ u ∈ ∅, m u
Tactic: induction I using Finset.induction with
    | empty => simp only [Finset.coe_empty, Set.sUnion_empty, Finset.sum_empty, m_empty]
    | insert s I hsI h =>
      rw [Finset.coe_insert] at *
      rw [Set.insert_subset_iff] at h_ss
      rw [Set.pairwiseDisjoint_insert_of_notMem] at h_dis
      swap; · exact hsI
      have h_sUnion_mem : ⋃₀ ↑I ∈ C := by
        rw [Set.sUnion_eq_biUnion]
        apply hC.biUnion_mem
        intro n hn
        exact h_ss.2 hn
      rw [Set.sUnion_insert, m_add h_ss.1 h_sUnion_mem (Set.disjoint_sUnion_right.mpr h_dis.2),
        Finset.sum_insert hsI, h h_ss.2 h_dis.1]
      rwa [Set.sUnion_insert] at h_mem
Cleared hypotheses: I, h_ss, h_dis, h_mem
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
I_1 : Finset (Set α)
G : Type u_2
inst : AddCommMonoid G
m_1 m' : AddContent G C
m : Set α → G
hC : IsSetRing C
m_empty : m ∅ = 0
m_add : ∀ {s t : Set α} (_hs : s ∈ C) (_ht : t ∈ C), Disjoint s t → m (s ∪ t) = m s + m t
I : Finset (Set α)
h_ss : (↑I : Set (Set α)) ⊆ C
h_dis : (↑I : Set (Set α)).PairwiseDisjoint id
h_mem : ⋃₀ (↑I : Set (Set α)) ∈ C
empty :
  ∀ (h_ss : (↑∅ : Set (Set α)) ⊆ C) (h_dis : (↑∅ : Set (Set α)).PairwiseDisjoint id)
    (h_mem : ⋃₀ (↑∅ : Set (Set α)) ∈ C), m (⋃₀ (↑∅ : Set (Set α))) = ∑ u ∈ ∅, m u
⊢ m (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, m u
have insert : ∀ (s : Set α) (I : Finset (Set α)) (hsI : s ∉ I)
  (h :
    ∀ (h_ss : (↑I : Set (Set α)) ⊆ C) (h_dis : (↑I : Set (Set α)).PairwiseDisjoint id)
      (h_mem : ⋃₀ (↑I : Set (Set α)) ∈ C), m (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, m u)
  (h_ss : (↑(insert s I) : Set (Set α)) ⊆ C) (h_dis : (↑(insert s I) : Set (Set α)).PairwiseDisjoint id)
  (h_mem : ⋃₀ (↑(insert s I) : Set (Set α)) ∈ C), m (⋃₀ (↑(insert s I) : Set (Set α))) = ∑ u ∈ insert s I, m u
Tactic: induction I using Finset.induction with
    | empty => simp only [Finset.coe_empty, Set.sUnion_empty, Finset.sum_empty, m_empty]
    | insert s I hsI h =>
      rw [Finset.coe_insert] at *
      rw [Set.insert_subset_iff] at h_ss
      rw [Set.pairwiseDisjoint_insert_of_notMem] at h_dis
      swap; · exact hsI
      have h_sUnion_mem : ⋃₀ ↑I ∈ C := by
        rw [Set.sUnion_eq_biUnion]
        apply hC.biUnion_mem
        intro n hn
        exact h_ss.2 hn
      rw [Set.sUnion_insert, m_add h_ss.1 h_sUnion_mem (Set.disjoint_sUnion_right.mpr h_dis.2),
        Finset.sum_insert hsI, h h_ss.2 h_dis.1]
      rwa [Set.sUnion_insert] at h_mem
Cleared hypotheses: I, h_ss, h_dis, h_mem
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
I_1 : Finset (Set α)
G : Type u_2
inst : AddCommMonoid G
m_1 m' : AddContent G C
m : Set α → G
hC : IsSetRing C
m_empty : m ∅ = 0
m_add : ∀ {s t : Set α} (_hs : s ∈ C) (_ht : t ∈ C), Disjoint s t → m (s ∪ t) = m s + m t
I : Finset (Set α)
h_ss : (↑I : Set (Set α)) ⊆ C
h_dis : (↑I : Set (Set α)).PairwiseDisjoint id
h_mem : ⋃₀ (↑I : Set (Set α)) ∈ C
⊢ m (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, m u
have empty : ∀ (h_ss : (↑∅ : Set (Set α)) ⊆ C) (h_dis : (↑∅ : Set (Set α)).PairwiseDisjoint id) (h_mem : ⋃₀ (↑∅ : Set (Set α)) ∈ C),
  m (⋃₀ (↑∅ : Set (Set α))) = ∑ u ∈ ∅, m u
Tactic: classical
    induction I using Finset.induction with
    | empty => simp only [Finset.coe_empty, Set.sUnion_empty, Finset.sum_empty, m_empty]
    | insert s I hsI h =>
      rw [Finset.coe_insert] at *
      rw [Set.insert_subset_iff] at h_ss
      rw [Set.pairwiseDisjoint_insert_of_notMem] at h_dis
      swap; · exact hsI
      have h_sUnion_mem : ⋃₀ ↑I ∈ C := by
        rw [Set.sUnion_eq_biUnion]
        apply hC.biUnion_mem
        intro n hn
        exact h_ss.2 hn
      rw [Set.sUnion_insert, m_add h_ss.1 h_sUnion_mem (Set.disjoint_sUnion_right.mpr h_dis.2),
        Finset.sum_insert hsI, h h_ss.2 h_dis.1]
      rwa [Set.sUnion_insert] at h_mem
Cleared hypotheses: I, h_ss, h_dis, h_mem
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
I_1 : Finset (Set α)
G : Type u_2
inst : AddCommMonoid G
m_1 m' : AddContent G C
m : Set α → G
hC : IsSetRing C
m_empty : m ∅ = 0
m_add : ∀ {s t : Set α} (_hs : s ∈ C) (_ht : t ∈ C), Disjoint s t → m (s ∪ t) = m s + m t
I : Finset (Set α)
h_ss : (↑I : Set (Set α)) ⊆ C
h_dis : (↑I : Set (Set α)).PairwiseDisjoint id
h_mem : ⋃₀ (↑I : Set (Set α)) ∈ C
empty :
  ∀ (h_ss : (↑∅ : Set (Set α)) ⊆ C) (h_dis : (↑∅ : Set (Set α)).PairwiseDisjoint id)
    (h_mem : ⋃₀ (↑∅ : Set (Set α)) ∈ C), m (⋃₀ (↑∅ : Set (Set α))) = ∑ u ∈ ∅, m u
⊢ m (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, m u
have insert : ∀ (s : Set α) (I : Finset (Set α)) (hsI : s ∉ I)
  (h :
    ∀ (h_ss : (↑I : Set (Set α)) ⊆ C) (h_dis : (↑I : Set (Set α)).PairwiseDisjoint id)
      (h_mem : ⋃₀ (↑I : Set (Set α)) ∈ C), m (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, m u)
  (h_ss : (↑(insert s I) : Set (Set α)) ⊆ C) (h_dis : (↑(insert s I) : Set (Set α)).PairwiseDisjoint id)
  (h_mem : ⋃₀ (↑(insert s I) : Set (Set α)) ∈ C), m (⋃₀ (↑(insert s I) : Set (Set α))) = ∑ u ∈ insert s I, m u
Tactic: classical
    induction I using Finset.induction with
    | empty => simp only [Finset.coe_empty, Set.sUnion_empty, Finset.sum_empty, m_empty]
    | insert s I hsI h =>
      rw [Finset.coe_insert] at *
      rw [Set.insert_subset_iff] at h_ss
      rw [Set.pairwiseDisjoint_insert_of_notMem] at h_dis
      swap; · exact hsI
      have h_sUnion_mem : ⋃₀ ↑I ∈ C := by
        rw [Set.sUnion_eq_biUnion]
        apply hC.biUnion_mem
        intro n hn
        exact h_ss.2 hn
      rw [Set.sUnion_insert, m_add h_ss.1 h_sUnion_mem (Set.disjoint_sUnion_right.mpr h_dis.2),
        Finset.sum_insert hsI, h h_ss.2 h_dis.1]
      rwa [Set.sUnion_insert] at h_mem
Cleared hypotheses: I, h_ss, h_dis, h_mem
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
inst_1 : PartialOrder G
inst_2 : CanonicallyOrderedAdd G
hC : IsSetRing C
hs : s ∈ C
ht : t ∈ C
⊢ (m : (a : Set α) → G) (s ∪ t) ≤
    HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) s : G) ((m : (a : Set α) → G) t : G)
have rw : HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) s : G) ((m : (a : Set α) → G) (t \ s) : G) ≤
  HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) s : G) ((m : (a : Set α) → G) t : G)
Tactic: rw [← union_diff_self, addContent_union hC hs (hC.diff_mem ht hs)]