awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_1 : Type u_2
inst : AddCommMonoid G_1
m m' : AddContent G_1 C
inst_1 : LinearOrder α
G : Type u_3
inst_2 : AddCommGroup G
f : α → G
n : ℕ
ih :
  ∀ (I : Finset (Set α)) (hI : (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v})
    (h'I : (↑I : Set (Set α)).PairwiseDisjoint id)
    (h''I :
      Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
        (⋃₀ (↑I : Set (Set α))))
    (hn : #I = n), onIocAux f (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, onIocAux f u
I : Finset (Set α)
hI : (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
h'I : (↑I : Set (Set α)).PairwiseDisjoint id
hn : #I = n + 1
u v : α
huv_1 : u ≤ v
h'uv : ⋃₀ (↑I : Set (Set α)) = Set.Ioc u v
huv : u < v
this : v ∈ ⋃₀ (↑I : Set (Set α))
u' : α
uu' : u ≤ u'
hu'v' : u' ≤ v
tI : Set.Ioc u' v ∈ I
ht : v ∈ Set.Ioc u' v
left : v ≤ v
I' : Finset (Set α) := I.erase (Set.Ioc u' v)
I'I : I' ⊆ I
I_eq_insert : I = insert (Set.Ioc u' v) I'
⊢ Disjoint (Set.Ioc u' v) (⋃₀ (↑I' : Set (Set α)))
have simp : ∀ t ∈ (↑I : Set (Set α)), ¬t = Set.Ioc u' v → Disjoint (Set.Ioc u' v) t
Tactic: simp only [coe_erase, disjoint_sUnion_right, mem_diff, mem_singleton_iff, and_imp, I']
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (hypothesis)
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
I_1 : Finset (Set α)
G_1 : Type u_2
inst : AddCommMonoid G_1
m m' : AddContent G_1 C
inst_1 : LinearOrder α
G : Type u_3
inst_2 : AddCommGroup G
f : α → G
n : ℕ
ih :
  ∀ (I : Finset (Set α)) (hI : (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v})
    (h'I : (↑I : Set (Set α)).PairwiseDisjoint id)
    (h''I :
      Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
        (⋃₀ (↑I : Set (Set α))))
    (hn : #I = n), onIocAux f (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, onIocAux f u
I : Finset (Set α)
hI : (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
h'I : (↑I : Set (Set α)).PairwiseDisjoint id
hn : #I = n + 1
u v : α
huv_1 : u ≤ v
h'uv : ⋃₀ (↑I : Set (Set α)) = Set.Ioc u v
huv : u < v
this : v ∈ ⋃₀ (↑I : Set (Set α))
u' : α
uu' : u ≤ u'
hu'v' : u' ≤ v
tI : Set.Ioc u' v ∈ I
ht : v ∈ Set.Ioc u' v
left : v ≤ v
I' : Finset (Set α) := I.erase (Set.Ioc u' v)
I'I : I' ⊆ I
I_eq_insert : I = insert (Set.Ioc u' v) I'
⊢ ⋃₀ (↑I' : Set (Set α)) = Set.Ioc u u'
have this₁ : (Set.Ioc u' v ∪ ⋃₀ (↑I' : Set (Set α))) \ Set.Ioc u' v = ⋃₀ (↑I' : Set (Set α))
Tactic: have : (Ioc u' v ∪ ⋃₀ ↑I') \ Ioc u' v = ⋃₀ ↑I' := by
          refine Disjoint.sup_sdiff_cancel_left ?_
          simp only [coe_erase, disjoint_sUnion_right, mem_diff, mem_singleton_iff, and_imp, I']
          intro u hu hu'
          exact (h'I hu tI hu').symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (hypothesis)
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
I_1 : Finset (Set α)
G_1 : Type u_2
inst : AddCommMonoid G_1
m m' : AddContent G_1 C
inst_1 : LinearOrder α
G : Type u_3
inst_2 : AddCommGroup G
f : α → G
n : ℕ
ih :
  ∀ (I : Finset (Set α)) (hI : (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v})
    (h'I : (↑I : Set (Set α)).PairwiseDisjoint id)
    (h''I :
      Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
        (⋃₀ (↑I : Set (Set α))))
    (hn : #I = n), onIocAux f (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, onIocAux f u
I : Finset (Set α)
hI : (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
h'I : (↑I : Set (Set α)).PairwiseDisjoint id
hn : #I = n + 1
u v : α
huv_1 : u ≤ v
h'uv : ⋃₀ (↑I : Set (Set α)) = Set.Ioc u v
huv : u < v
this_1 : v ∈ ⋃₀ (↑I : Set (Set α))
u' : α
uu' : u ≤ u'
hu'v' : u' ≤ v
tI : Set.Ioc u' v ∈ I
ht : v ∈ Set.Ioc u' v
left : v ≤ v
I' : Finset (Set α) := I.erase (Set.Ioc u' v)
I'I : I' ⊆ I
I_eq_insert : I = insert (Set.Ioc u' v) I'
this : (Set.Ioc u' v ∪ ⋃₀ (↑I' : Set (Set α))) \ Set.Ioc u' v = ⋃₀ (↑I' : Set (Set α))
⊢ ⋃₀ (↑I' : Set (Set α)) = Set.Ioc u u'
have h'uv₁ : Set.Ioc u' v ∪ ⋃₀ (↑I' : Set (Set α)) = Set.Ioc u v
Tactic: simp only [I_eq_insert, coe_insert, sUnion_insert] at h'uv
Cleared hypotheses: h'uv
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (hypothesis)
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
I_1 : Finset (Set α)
G_1 : Type u_2
inst : AddCommMonoid G_1
m m' : AddContent G_1 C
inst_1 : LinearOrder α
G : Type u_3
inst_2 : AddCommGroup G
f : α → G
n : ℕ
ih :
  ∀ (I : Finset (Set α)) (hI : (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v})
    (h'I : (↑I : Set (Set α)).PairwiseDisjoint id)
    (h''I :
      Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
        (⋃₀ (↑I : Set (Set α))))
    (hn : #I = n), onIocAux f (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, onIocAux f u
I : Finset (Set α)
hI : (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
h'I : (↑I : Set (Set α)).PairwiseDisjoint id
hn : #I = n + 1
u v : α
huv_1 : u ≤ v
h'uv : ⋃₀ (↑I : Set (Set α)) = Set.Ioc u v
huv : u < v
this : v ∈ ⋃₀ (↑I : Set (Set α))
u' : α
uu' : u ≤ u'
hu'v' : u' ≤ v
tI : Set.Ioc u' v ∈ I
ht : v ∈ Set.Ioc u' v
left : v ≤ v
I' : Finset (Set α) := I.erase (Set.Ioc u' v)
I'I : I' ⊆ I
I_eq_insert : I = insert (Set.Ioc u' v) I'
⊢ f v - f u = ∑ u ∈ I, onIocAux f u
have UI' : ⋃₀ (↑I' : Set (Set α)) = Set.Ioc u u'
Tactic: have UI' : ⋃₀ ↑I' = Ioc u u' := by
        have : (Ioc u' v ∪ ⋃₀ ↑I') \ Ioc u' v = ⋃₀ ↑I' := by
          refine Disjoint.sup_sdiff_cancel_left ?_
          simp only [coe_erase, disjoint_sUnion_right, mem_diff, mem_singleton_iff, and_imp, I']
          intro u hu hu'
          exact (h'I hu tI hu').symm
        simp only [I_eq_insert, coe_insert, sUnion_insert] at h'uv
        grind
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (hypothesis)
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
I_1 : Finset (Set α)
G_1 : Type u_2
inst : AddCommMonoid G_1
m m' : AddContent G_1 C
inst_1 : LinearOrder α
G : Type u_3
inst_2 : AddCommGroup G
f : α → G
n : ℕ
ih :
  ∀ (I : Finset (Set α)) (hI : (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v})
    (h'I : (↑I : Set (Set α)).PairwiseDisjoint id)
    (h''I :
      Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
        (⋃₀ (↑I : Set (Set α))))
    (hn : #I = n), onIocAux f (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, onIocAux f u
I : Finset (Set α)
hI : (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
h'I : (↑I : Set (Set α)).PairwiseDisjoint id
hn : #I = n + 1
u v : α
huv_1 : u ≤ v
h'uv : ⋃₀ (↑I : Set (Set α)) = Set.Ioc u v
huv : u < v
this : v ∈ ⋃₀ (↑I : Set (Set α))
u' : α
uu' : u ≤ u'
hu'v' : u' ≤ v
tI : Set.Ioc u' v ∈ I
ht : v ∈ Set.Ioc u' v
left : v ≤ v
I' : Finset (Set α) := I.erase (Set.Ioc u' v)
I'I : I' ⊆ I
I_eq_insert : I = insert (Set.Ioc u' v) I'
UI' : ⋃₀ (↑I' : Set (Set α)) = Set.Ioc u u'
⊢ f v - f u = ∑ u ∈ I, onIocAux f u
have IH : onIocAux f (⋃₀ (↑I' : Set (Set α))) = ∑ u ∈ I', onIocAux f u
Tactic: have IH : onIocAux f (⋃₀ ↑I') = ∑ u ∈ I', onIocAux f u :=
        ih _ (Subset.trans I'I hI) (h'I.subset I'I) (by grind) (by grind)
-- 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_1 : Type u_2
inst : AddCommMonoid G_1
m m' : AddContent G_1 C
inst_1 : LinearOrder α
G : Type u_3
inst_2 : AddCommGroup G
f : α → G
n : ℕ
ih :
  ∀ (I : Finset (Set α)) (hI : (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v})
    (h'I : (↑I : Set (Set α)).PairwiseDisjoint id)
    (h''I :
      Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
        (⋃₀ (↑I : Set (Set α))))
    (hn : #I = n), onIocAux f (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, onIocAux f u
I : Finset (Set α)
hI : (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
h'I : (↑I : Set (Set α)).PairwiseDisjoint id
hn : #I = n + 1
u v : α
huv_1 : u ≤ v
h'uv : ⋃₀ (↑I : Set (Set α)) = Set.Ioc u v
huv : u < v
this : v ∈ ⋃₀ (↑I : Set (Set α))
u' : α
uu' : u ≤ u'
hu'v' : u' ≤ v
tI : Set.Ioc u' v ∈ I
ht : v ∈ Set.Ioc u' v
left : v ≤ v
I' : Finset (Set α) := I.erase (Set.Ioc u' v)
I'I : I' ⊆ I
I_eq_insert : I = insert (Set.Ioc u' v) I'
UI' : ⋃₀ (↑I' : Set (Set α)) = Set.Ioc u u'
IH : onIocAux f (⋃₀ (↑I' : Set (Set α))) = ∑ u ∈ I', onIocAux f u
⊢ f v - f u = ∑ u ∈ I, onIocAux f u
have succ : f v - f u = f v - f u' + (f u' - f u)
Tactic: rw [I_eq_insert, sum_insert, ← IH, UI', onIocAux_apply hu'v', onIocAux_apply uu']
-- 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_1 : Type u_2
inst : AddCommMonoid G_1
m m' : AddContent G_1 C
inst_1 : LinearOrder α
G : Type u_3
inst_2 : AddCommGroup G
f : α → G
n : ℕ
ih :
  ∀ (I : Finset (Set α)) (hI : (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v})
    (h'I : (↑I : Set (Set α)).PairwiseDisjoint id)
    (h''I :
      Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
        (⋃₀ (↑I : Set (Set α))))
    (hn : #I = n), onIocAux f (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, onIocAux f u
I : Finset (Set α)
hI : (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
h'I : (↑I : Set (Set α)).PairwiseDisjoint id
hn : #I = n + 1
u v : α
huv_1 : u ≤ v
h'uv : ⋃₀ (↑I : Set (Set α)) = Set.Ioc u v
huv : u < v
this : v ∈ ⋃₀ (↑I : Set (Set α))
u' : α
uu' : u ≤ u'
hu'v' : u' ≤ v
tI : Set.Ioc u' v ∈ I
ht : v ∈ Set.Ioc u' v
left : v ≤ v
I' : Finset (Set α) := I.erase (Set.Ioc u' v)
I'I : I' ⊆ I
I_eq_insert : I = insert (Set.Ioc u' v) I'
UI' : ⋃₀ (↑I' : Set (Set α)) = Set.Ioc u u'
IH : onIocAux f (⋃₀ (↑I' : Set (Set α))) = ∑ u ∈ I', onIocAux f u
succ : f v - f u = f v - f u' + (f u' - f u)
⊢ f v - f u = ∑ u ∈ I, onIocAux f u
have succ₁ : Set.Ioc u' v ∉ I'
Tactic: rw [I_eq_insert, sum_insert, ← IH, UI', onIocAux_apply hu'v', onIocAux_apply uu']
-- 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_1 : Type u_2
inst : AddCommMonoid G_1
m m' : AddContent G_1 C
inst_1 : LinearOrder α
G : Type u_3
inst_2 : AddCommGroup G
f : α → G
I : Finset (Set α)
hI : (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
h'I : (↑I : Set (Set α)).PairwiseDisjoint id
h''I :
  Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v} (⋃₀ (↑I : Set (Set α)))
⊢ onIocAux f (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, onIocAux f u
have induction : ∀ (x : ℕ) (hn : #I = x), onIocAux f (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, onIocAux f u
Tactic: induction hn : Finset.card I generalizing I with
    | zero =>
      have : I = ∅ := by grind
      simp [this, onIocAux_empty f]
    | succ n ih =>
      rcases h''I with ⟨u, v, huv, h'uv⟩
      -- If the interval `(u, v]` is empty, i.e., `u = v`, then the result is easy.
      rcases huv.eq_or_lt with rfl | huv
      · have : onIocAux f (Set.Ioc u u) = ∑ u ∈ I, 0 := by simp [onIocAux_empty f]
        rw [h'uv, this]
        apply Finset.sum_congr rfl fun i hi ↦ ?_
        have : i = ∅ := by grind [sUnion_eq_empty]
        grind [onIocAux_empty]
      -- otherwise, `v` is in `(u, v]`, therefore it belongs to some interval `(u', v']`
      -- featuring in the union.
      have : v ∈ ⋃₀ ↑I := by simp [h'uv, huv]
      obtain ⟨t, tI, ht⟩ : ∃ t ∈ I, v ∈ t := by simpa using this
      rcases hI tI with ⟨u', v', hu'v', rfl⟩
      -- we have `u ≤ u'` and `v' = v` since `(u', v']` is part of the union, and therefore
      -- contained in `(u, v]`.
      have ⟨_, uu'⟩ : v' ≤ v ∧ u ≤ u' := (Ioc_subset_Ioc_iff (by grind)).1 (by grind)
      obtain rfl : v = v' := by grind
      rw [h'uv, onIocAux_apply huv.le]
      -- let us remove the right-most interval `(u', v]` from the union, and let `I'` be the
      -- remaining set of intervals.
      let I' := I.erase (Set.Ioc u' v)
      have I'I : I' ⊆ I := erase_subset (Set.Ioc u' v) I
      have I_eq_insert : I = insert (Set.Ioc u' v) I' := by simp [I', tI]
      -- the intervals in `I'` cover exactly `(u, u']`.
      have UI' : ⋃₀ ↑I' = Ioc u u' := by
        have : (Ioc u' v ∪ ⋃₀ ↑I') \ Ioc u' v = ⋃₀ ↑I' := by
          refine Disjoint.sup_sdiff_cancel_left ?_
          simp only [coe_erase, disjoint_sUnion_right, mem_diff, mem_singleton_iff, and_imp, I']
          intro u hu hu'
          exact (h'I hu tI hu').symm
        simp only [I_eq_insert, coe_insert, sUnion_insert] at h'uv
        grind
      -- by the inductive assumption, the sum over `I'` is exactly `f u' - f u`.
      have IH : onIocAux f (⋃₀ ↑I') = ∑ u ∈ I', onIocAux f u :=
        ih _ (Subset.trans I'I hI) (h'I.subset I'I) (by grind) (by grind)
      -- the conclusion follows.
      rw [I_eq_insert, sum_insert, ← IH, UI', onIocAux_apply hu'v', onIocAux_apply uu']
      · simp
      · simp [I']
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
I : Finset (Set α)
G : Type u_2
inst : AddCommMonoid G
m_1 m' : AddContent G C
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
⊢ extend (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) ∅ = 0
have h : ∅ ∈ C
Tactic: rw [extend_eq, addContent_empty]
-- 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
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
I : Finset (Set α)
h_ss : (↑I : Set (Set α)) ⊆ C
h_dis : (↑I : Set (Set α)).PairwiseDisjoint id
h_mem : ⋃₀ (↑I : Set (Set α)) ∈ C
⊢ extend (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) (⋃₀ (↑I : Set (Set α))) =
    ∑ u ∈ I, extend (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) u
have rw : Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃₀ (↑I : Set (Set α))) : ℝ≥0∞)
  (∑ u ∈ I, extend (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) u : ℝ≥0∞)
Tactic: rw [extend_eq]
-- 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
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
I : Finset (Set α)
h_ss : (↑I : Set (Set α)) ⊆ C
h_dis : (↑I : Set (Set α)).PairwiseDisjoint id
h_mem : ⋃₀ (↑I : Set (Set α)) ∈ C
⊢ Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃₀ (↑I : Set (Set α))) : ℝ≥0∞)
    (∑ u ∈ I, extend (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) u : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) (∑ u ∈ I, (m : (a : Set α) → ℝ≥0∞) u)
  (∑ u ∈ I, extend (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) u)
Tactic: rw [addContent_sUnion 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
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
I : Finset (Set α)
h_ss : (↑I : Set (Set α)) ⊆ C
h_dis : (↑I : Set (Set α)).PairwiseDisjoint id
h_mem : ⋃₀ (↑I : Set (Set α)) ∈ C
⊢ Eq (α := ℝ≥0∞) (∑ u ∈ I, (m : (a : Set α) → ℝ≥0∞) u)
    (∑ u ∈ I, extend (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) u)
have refine : ∀ (s : Set α) (hs : s ∈ I),
  (m : (a : Set α) → ℝ≥0∞) s =
    extend (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) s
Tactic: refine Finset.sum_congr rfl (fun s hs ↦ ?_)
-- 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
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
I : Finset (Set α)
h_ss : (↑I : Set (Set α)) ⊆ C
h_dis : (↑I : Set (Set α)).PairwiseDisjoint id
h_mem : ⋃₀ (↑I : Set (Set α)) ∈ C
s : Set α
hs : s ∈ I
⊢ (m : (a : Set α) → ℝ≥0∞) s =
    extend (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) s
have h : s ∈ C
Tactic: rw [extend_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
hs : s ∈ C
⊢ Eq (α := ℝ≥0∞) ((AddContent.extend (C := C) hC m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rwa : extend (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) s =
  (m : (a : Set α) → ℝ≥0∞) s
Tactic: rwa [m.extend_eq_extend, extend_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
hs : s ∈ C
rwa :
  extend (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) s =
    (m : (a : Set α) → ℝ≥0∞) s
⊢ Eq (α := ℝ≥0∞) ((AddContent.extend (C := C) hC m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rwa₁ : Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rwa [m.extend_eq_extend, extend_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
hs : s ∉ C
⊢ Eq (α := ℝ≥0∞) ((AddContent.extend (C := C) hC m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
have rwa : extend (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) s = ∞
Tactic: rwa [m.extend_eq_extend, extend_eq_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
hs : s ∉ C
rwa : extend (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) s = ∞
⊢ Eq (α := ℝ≥0∞) ((AddContent.extend (C := C) hC m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
have rwa₁ : Eq (α := ℝ≥0∞) ∞ ∞
Tactic: rwa [m.extend_eq_extend, extend_eq_top]
-- 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 α
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)
have insert : (m : (a : Set α) → G) (⋃ i_1 ∈ insert i S, s i_1) =
  HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) (s i) : G) (∑ x ∈ S, (m : (a : Set α) → G) (s x) : G)
Tactic: rw [Finset.sum_insert hiS]
-- 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 α
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
⊢ (m : (a : Set α) → G) (⋃ i_1 ∈ insert i S, s i_1) =
    HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) (s i) : G) (∑ x ∈ S, (m : (a : Set α) → G) (s x) : G)
have insert : (m : (a : Set α) → G) (s i ∪ ⋃ x ∈ (↑S : Set ι), s x) =
  HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) (s i) : G) (∑ x ∈ S, (m : (a : Set α) → G) (s x) : G)
Tactic: simp_rw [← Finset.mem_coe, Finset.coe_insert, Set.biUnion_insert]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (hypothesis)
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 α
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
⊢ (m : (a : Set α) → G) (s i ∪ ⋃ x ∈ (↑S : Set ι), s x) =
    HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) (s i) : G) (∑ x ∈ S, (m : (a : Set α) → G) (s x) : G)
have hs₁ : s i ∈ C ∧ ∀ a ∈ S, s a ∈ C
Tactic: simp only [Finset.mem_insert, forall_eq_or_imp] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (hypothesis)
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 α
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 : (↑(insert i S) : Set ι).PairwiseDisjoint s
hs : s i ∈ C ∧ ∀ a ∈ S, s a ∈ C
⊢ (m : (a : Set α) → G) (s i ∪ ⋃ x ∈ (↑S : Set ι), s x) =
    HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) (s i) : G) (∑ x ∈ S, (m : (a : Set α) → G) (s x) : G)
have hS₁ : (↑S : Set ι).PairwiseDisjoint s ∧ ∀ j ∈ (↑S : Set ι), i ≠ j → Disjoint (s i) (s j)
Tactic: simp only [Finset.coe_insert, Set.pairwiseDisjoint_insert] at hS
Cleared hypotheses: 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 α
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 : s i ∈ C ∧ ∀ a ∈ S, s a ∈ C
hS : (↑S : Set ι).PairwiseDisjoint s ∧ ∀ j ∈ (↑S : Set ι), i ≠ j → Disjoint (s i) (s j)
⊢ (m : (a : Set α) → G) (s i ∪ ⋃ x ∈ (↑S : Set ι), s x) =
    HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) (s i) : G) (∑ x ∈ S, (m : (a : Set α) → G) (s x) : G)
have insert : (m : (a : Set α) → G) (s i ∪ ⋃ x ∈ (↑S : Set ι), s x) =
  HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) (s i) : G) ((m : (a : Set α) → G) (⋃ i ∈ S, s i) : G)
Tactic: rw [← h hs.2 hS.1]
-- 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 α
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 : s i ∈ C ∧ ∀ a ∈ S, s a ∈ C
hS : (↑S : Set ι).PairwiseDisjoint s ∧ ∀ j ∈ (↑S : Set ι), i ≠ j → Disjoint (s i) (s j)
⊢ (m : (a : Set α) → G) (s i ∪ ⋃ x ∈ (↑S : Set ι), s x) =
    HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) (s i) : G) ((m : (a : Set α) → G) (⋃ i ∈ S, s i) : G)
have insert : Disjoint (s i) (⋃ x ∈ (↑S : Set ι), s x)
Tactic: refine addContent_union hC hs.1 (hC.biUnion_mem S hs.2) ?_
-- 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 α
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 : s i ∈ C ∧ ∀ a ∈ S, s a ∈ C
hS : (↑S : Set ι).PairwiseDisjoint s ∧ ∀ j ∈ (↑S : Set ι), i ≠ j → Disjoint (s i) (s j)
⊢ Disjoint (s i) (⋃ x ∈ (↑S : Set ι), s x)
have insert : ∀ (i_1 : ι) (j : i_1 ∈ (↑S : Set ι)), Disjoint (s i) (s i_1)
Tactic: rw [disjoint_iUnion₂_right]