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 : Set α
I : Finset (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : (↑I : Set (Set α)) ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I : Set (Set α)).PairwiseDisjoint id
⊢ (m : (a : Set α) → G) (⋃₀ (↑(I ∪ hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))) =
    HAdd.hAdd (α := G) (∑ i ∈ I, (m : (a : Set α) → G) i)
      (∑ i ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI, (m : (a : Set α) → G) i)
have rw : ∑ u ∈ I ∪ hC.disjointOfDiffUnion (C := C) (s := s) hs hI, (m : (a : Set α) → G) u =
  HAdd.hAdd (α := G) (∑ i ∈ I, (m : (a : Set α) → G) i)
    (∑ i ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI, (m : (a : Set α) → G) i)
Tactic: rw [addContent_sUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : (↑I : Set (Set α)) ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I : Set (Set α)).PairwiseDisjoint id
rw :
  ∑ u ∈ I ∪ hC.disjointOfDiffUnion (C := C) (s := s) hs hI, (m : (a : Set α) → G) u =
    HAdd.hAdd (α := G) (∑ i ∈ I, (m : (a : Set α) → G) i)
      (∑ i ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI, (m : (a : Set α) → G) i)
⊢ (m : (a : Set α) → G) (⋃₀ (↑(I ∪ hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))) =
    HAdd.hAdd (α := G) (∑ i ∈ I, (m : (a : Set α) → G) i)
      (∑ i ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI, (m : (a : Set α) → G) i)
have h_ss : (↑(I ∪ hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)) ⊆ C
Tactic: rw [addContent_sUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : (↑I : Set (Set α)) ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I : Set (Set α)).PairwiseDisjoint id
rw :
  ∑ u ∈ I ∪ hC.disjointOfDiffUnion (C := C) (s := s) hs hI, (m : (a : Set α) → G) u =
    HAdd.hAdd (α := G) (∑ i ∈ I, (m : (a : Set α) → G) i)
      (∑ i ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI, (m : (a : Set α) → G) i)
h_ss : (↑(I ∪ hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)) ⊆ C
⊢ (m : (a : Set α) → G) (⋃₀ (↑(I ∪ hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))) =
    HAdd.hAdd (α := G) (∑ i ∈ I, (m : (a : Set α) → G) i)
      (∑ i ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI, (m : (a : Set α) → G) i)
have h_dis₁ : (↑(I ∪ hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)).PairwiseDisjoint id
Tactic: rw [addContent_sUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : (↑I : Set (Set α)) ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I : Set (Set α)).PairwiseDisjoint id
rw :
  ∑ u ∈ I ∪ hC.disjointOfDiffUnion (C := C) (s := s) hs hI, (m : (a : Set α) → G) u =
    HAdd.hAdd (α := G) (∑ i ∈ I, (m : (a : Set α) → G) i)
      (∑ i ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI, (m : (a : Set α) → G) i)
h_ss : (↑(I ∪ hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)) ⊆ C
h_dis₁ : (↑(I ∪ hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)).PairwiseDisjoint id
⊢ (m : (a : Set α) → G) (⋃₀ (↑(I ∪ hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))) =
    HAdd.hAdd (α := G) (∑ i ∈ I, (m : (a : Set α) → G) i)
      (∑ i ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI, (m : (a : Set α) → G) i)
have h_mem : ⋃₀ (↑(I ∪ hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)) ∈ C
Tactic: rw [addContent_sUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : (↑I : Set (Set α)) ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I : Set (Set α)).PairwiseDisjoint id
⊢ ∑ u ∈ I ∪ hC.disjointOfDiffUnion (C := C) (s := s) hs hI, (m : (a : Set α) → G) u =
    HAdd.hAdd (α := G) (∑ i ∈ I, (m : (a : Set α) → G) i)
      (∑ i ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI, (m : (a : Set α) → G) i)
have rw : Disjoint I (hC.disjointOfDiffUnion (C := C) (s := s) hs hI)
Tactic: rw [sum_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : (↑I : Set (Set α)) ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I : Set (Set α)).PairwiseDisjoint id
⊢ (↑(I ∪ hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)) ⊆ C
have h_ss : (↑I : Set (Set α)) ∪ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)) ⊆ C
Tactic: rw [coe_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : (↑I : Set (Set α)) ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I : Set (Set α)).PairwiseDisjoint id
⊢ (↑(I ∪ hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)).PairwiseDisjoint id
have h_dis₁ : ((↑I : Set (Set α)) ∪ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))).PairwiseDisjoint id
Tactic: rw [coe_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : (↑I : Set (Set α)) ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I : Set (Set α)).PairwiseDisjoint id
⊢ (m : (a : Set α) → G) s =
    HAdd.hAdd (α := G) (∑ i ∈ I, (m : (a : Set α) → G) i)
      (∑ i ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI, (m : (a : Set α) → G) i)
have conv_lhs : (m : (a : Set α) → G) s =
  HAdd.hAdd (α := G) (∑ i ∈ I, (m : (a : Set α) → G) i)
    (∑ i ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI, (m : (a : Set α) → G) i)
Tactic: classical
  conv_lhs => rw [← hC.sUnion_union_disjointOfDiffUnion_of_subset hs hI hI_ss]
  rw [addContent_sUnion]
  · rw [sum_union]
    exact hC.disjoint_disjointOfDiffUnion hs hI
  · rw [coe_union]
    exact Set.union_subset hI (hC.disjointOfDiffUnion_subset hs hI)
  · rw [coe_union]
    exact hC.pairwiseDisjoint_union_disjointOfDiffUnion hs hI h_dis
  · rwa [hC.sUnion_union_disjointOfDiffUnion_of_subset hs hI hI_ss]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : (↑I : Set (Set α)) ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I : Set (Set α)).PairwiseDisjoint id
conv_lhs :
  (m : (a : Set α) → G) s =
    HAdd.hAdd (α := G) (∑ i ∈ I, (m : (a : Set α) → G) i)
      (∑ i ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI, (m : (a : Set α) → G) i)
⊢ (m : (a : Set α) → G) s =
    HAdd.hAdd (α := G) (∑ i ∈ I, (m : (a : Set α) → G) i)
      (∑ i ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI, (m : (a : Set α) → G) i)
have conv_lhs₁ : (m : (a : Set α) → G) (⋃₀ (↑(I ∪ hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))) =
  HAdd.hAdd (α := G) (∑ i ∈ I, (m : (a : Set α) → G) i)
    (∑ i ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI, (m : (a : Set α) → G) i)
Tactic: classical
  conv_lhs => rw [← hC.sUnion_union_disjointOfDiffUnion_of_subset hs hI hI_ss]
  rw [addContent_sUnion]
  · rw [sum_union]
    exact hC.disjoint_disjointOfDiffUnion hs hI
  · rw [coe_union]
    exact Set.union_subset hI (hC.disjointOfDiffUnion_subset hs hI)
  · rw [coe_union]
    exact hC.pairwiseDisjoint_union_disjointOfDiffUnion hs hI h_dis
  · rwa [hC.sUnion_union_disjointOfDiffUnion_of_subset hs hI hI_ss]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : (↑I : Set (Set α)) ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I : Set (Set α)).PairwiseDisjoint id
conv_lhs :
  (m : (a : Set α) → G) s =
    HAdd.hAdd (α := G) (∑ i ∈ I, (m : (a : Set α) → G) i)
      (∑ i ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI, (m : (a : Set α) → G) i)
conv_lhs₁ conv_lhs₂ :
  (m : (a : Set α) → G) (⋃₀ (↑(I ∪ hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))) =
    HAdd.hAdd (α := G) (∑ i ∈ I, (m : (a : Set α) → G) i)
      (∑ i ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI, (m : (a : Set α) → G) i)
⊢ (m : (a : Set α) → G) s =
    HAdd.hAdd (α := G) (∑ i ∈ I, (m : (a : Set α) → G) i)
      (∑ i ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI, (m : (a : Set α) → G) i)
have conv_lhs₃ : ∑ u ∈ I ∪ hC.disjointOfDiffUnion (C := C) (s := s) hs hI, (m : (a : Set α) → G) u =
  HAdd.hAdd (α := G) (∑ i ∈ I, (m : (a : Set α) → G) i)
    (∑ i ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI, (m : (a : Set α) → G) i)
Tactic: classical
  conv_lhs => rw [← hC.sUnion_union_disjointOfDiffUnion_of_subset hs hI hI_ss]
  rw [addContent_sUnion]
  · rw [sum_union]
    exact hC.disjoint_disjointOfDiffUnion hs hI
  · rw [coe_union]
    exact Set.union_subset hI (hC.disjointOfDiffUnion_subset hs hI)
  · rw [coe_union]
    exact hC.pairwiseDisjoint_union_disjointOfDiffUnion hs hI h_dis
  · rwa [hC.sUnion_union_disjointOfDiffUnion_of_subset hs hI hI_ss]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : (↑I : Set (Set α)) ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I : Set (Set α)).PairwiseDisjoint id
conv_lhs :
  (m : (a : Set α) → G) s =
    HAdd.hAdd (α := G) (∑ i ∈ I, (m : (a : Set α) → G) i)
      (∑ i ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI, (m : (a : Set α) → G) i)
conv_lhs₁ conv_lhs₂ :
  (m : (a : Set α) → G) (⋃₀ (↑(I ∪ hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))) =
    HAdd.hAdd (α := G) (∑ i ∈ I, (m : (a : Set α) → G) i)
      (∑ i ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI, (m : (a : Set α) → G) i)
conv_lhs₃ :
  ∑ u ∈ I ∪ hC.disjointOfDiffUnion (C := C) (s := s) hs hI, (m : (a : Set α) → G) u =
    HAdd.hAdd (α := G) (∑ i ∈ I, (m : (a : Set α) → G) i)
      (∑ i ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI, (m : (a : Set α) → G) i)
⊢ (m : (a : Set α) → G) s =
    HAdd.hAdd (α := G) (∑ i ∈ I, (m : (a : Set α) → G) i)
      (∑ i ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI, (m : (a : Set α) → G) i)
have h_ss : (↑(I ∪ hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)) ⊆ C
Tactic: classical
  conv_lhs => rw [← hC.sUnion_union_disjointOfDiffUnion_of_subset hs hI hI_ss]
  rw [addContent_sUnion]
  · rw [sum_union]
    exact hC.disjoint_disjointOfDiffUnion hs hI
  · rw [coe_union]
    exact Set.union_subset hI (hC.disjointOfDiffUnion_subset hs hI)
  · rw [coe_union]
    exact hC.pairwiseDisjoint_union_disjointOfDiffUnion hs hI h_dis
  · rwa [hC.sUnion_union_disjointOfDiffUnion_of_subset hs hI hI_ss]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : (↑I : Set (Set α)) ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I : Set (Set α)).PairwiseDisjoint id
conv_lhs :
  (m : (a : Set α) → G) s =
    HAdd.hAdd (α := G) (∑ i ∈ I, (m : (a : Set α) → G) i)
      (∑ i ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI, (m : (a : Set α) → G) i)
conv_lhs₁ conv_lhs₂ :
  (m : (a : Set α) → G) (⋃₀ (↑(I ∪ hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))) =
    HAdd.hAdd (α := G) (∑ i ∈ I, (m : (a : Set α) → G) i)
      (∑ i ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI, (m : (a : Set α) → G) i)
conv_lhs₃ :
  ∑ u ∈ I ∪ hC.disjointOfDiffUnion (C := C) (s := s) hs hI, (m : (a : Set α) → G) u =
    HAdd.hAdd (α := G) (∑ i ∈ I, (m : (a : Set α) → G) i)
      (∑ i ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI, (m : (a : Set α) → G) i)
h_ss : (↑(I ∪ hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)) ⊆ C
⊢ (m : (a : Set α) → G) s =
    HAdd.hAdd (α := G) (∑ i ∈ I, (m : (a : Set α) → G) i)
      (∑ i ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI, (m : (a : Set α) → G) i)
have h_dis₁ : (↑(I ∪ hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)).PairwiseDisjoint id
Tactic: classical
  conv_lhs => rw [← hC.sUnion_union_disjointOfDiffUnion_of_subset hs hI hI_ss]
  rw [addContent_sUnion]
  · rw [sum_union]
    exact hC.disjoint_disjointOfDiffUnion hs hI
  · rw [coe_union]
    exact Set.union_subset hI (hC.disjointOfDiffUnion_subset hs hI)
  · rw [coe_union]
    exact hC.pairwiseDisjoint_union_disjointOfDiffUnion hs hI h_dis
  · rwa [hC.sUnion_union_disjointOfDiffUnion_of_subset hs hI hI_ss]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : (↑I : Set (Set α)) ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I : Set (Set α)).PairwiseDisjoint id
conv_lhs :
  (m : (a : Set α) → G) s =
    HAdd.hAdd (α := G) (∑ i ∈ I, (m : (a : Set α) → G) i)
      (∑ i ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI, (m : (a : Set α) → G) i)
conv_lhs₁ conv_lhs₂ :
  (m : (a : Set α) → G) (⋃₀ (↑(I ∪ hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))) =
    HAdd.hAdd (α := G) (∑ i ∈ I, (m : (a : Set α) → G) i)
      (∑ i ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI, (m : (a : Set α) → G) i)
conv_lhs₃ :
  ∑ u ∈ I ∪ hC.disjointOfDiffUnion (C := C) (s := s) hs hI, (m : (a : Set α) → G) u =
    HAdd.hAdd (α := G) (∑ i ∈ I, (m : (a : Set α) → G) i)
      (∑ i ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI, (m : (a : Set α) → G) i)
h_ss : (↑(I ∪ hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)) ⊆ C
h_dis₁ : (↑(I ∪ hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)).PairwiseDisjoint id
⊢ (m : (a : Set α) → G) s =
    HAdd.hAdd (α := G) (∑ i ∈ I, (m : (a : Set α) → G) i)
      (∑ i ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI, (m : (a : Set α) → G) i)
have h_mem : ⋃₀ (↑(I ∪ hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)) ∈ C
Tactic: classical
  conv_lhs => rw [← hC.sUnion_union_disjointOfDiffUnion_of_subset hs hI hI_ss]
  rw [addContent_sUnion]
  · rw [sum_union]
    exact hC.disjoint_disjointOfDiffUnion hs hI
  · rw [coe_union]
    exact Set.union_subset hI (hC.disjointOfDiffUnion_subset hs hI)
  · rw [coe_union]
    exact hC.pairwiseDisjoint_union_disjointOfDiffUnion hs hI h_dis
  · rwa [hC.sUnion_union_disjointOfDiffUnion_of_subset hs hI hI_ss]
-- 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
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
| ((m : (a : Set α) → G) t : G)
have rw : ((m : (a : Set α) → G) (⋃₀ insert s (↑(hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs) : Set (Set α))) : G)
Tactic: rw [← hC.sUnion_insert_disjointOfDiff ht hs hst]
-- 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
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
⊢ (m : (a : Set α) → G) t =
    HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) s : G)
      (∑ i ∈ hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs, (m : (a : Set α) → G) i : G)
have conv_lhs : (m : (a : Set α) → G) (⋃₀ insert s (↑(hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs) : Set (Set α))) =
  HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) s : G)
    (∑ i ∈ hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs, (m : (a : Set α) → G) i : G)
Tactic: conv_lhs => rw [← hC.sUnion_insert_disjointOfDiff ht hs hst]
-- 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
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
⊢ (m : (a : Set α) → G) (⋃₀ insert s (↑(hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs) : Set (Set α))) =
    HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) s : G)
      (∑ i ∈ hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs, (m : (a : Set α) → G) i : G)
have rw : ∑ u ∈ insert s (hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs), (m : (a : Set α) → G) u =
  HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) s : G)
    (∑ i ∈ hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs, (m : (a : Set α) → G) i : G)
Tactic: rw [← coe_insert, addContent_sUnion]
-- 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
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
rw :
  ∑ u ∈ insert s (hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs), (m : (a : Set α) → G) u =
    HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) s : G)
      (∑ i ∈ hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs, (m : (a : Set α) → G) i : G)
⊢ (m : (a : Set α) → G) (⋃₀ insert s (↑(hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs) : Set (Set α))) =
    HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) s : G)
      (∑ i ∈ hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs, (m : (a : Set α) → G) i : G)
have h_ss : (↑(insert s (hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs)) : Set (Set α)) ⊆ C
Tactic: rw [← coe_insert, addContent_sUnion]
-- 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
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
rw :
  ∑ u ∈ insert s (hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs), (m : (a : Set α) → G) u =
    HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) s : G)
      (∑ i ∈ hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs, (m : (a : Set α) → G) i : G)
h_ss : (↑(insert s (hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs)) : Set (Set α)) ⊆ C
⊢ (m : (a : Set α) → G) (⋃₀ insert s (↑(hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs) : Set (Set α))) =
    HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) s : G)
      (∑ i ∈ hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs, (m : (a : Set α) → G) i : G)
have h_dis : (↑(insert s (hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs)) : Set (Set α)).PairwiseDisjoint id
Tactic: rw [← coe_insert, addContent_sUnion]
-- 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
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
rw :
  ∑ u ∈ insert s (hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs), (m : (a : Set α) → G) u =
    HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) s : G)
      (∑ i ∈ hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs, (m : (a : Set α) → G) i : G)
h_ss : (↑(insert s (hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs)) : Set (Set α)) ⊆ C
h_dis : (↑(insert s (hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs)) : Set (Set α)).PairwiseDisjoint id
⊢ (m : (a : Set α) → G) (⋃₀ insert s (↑(hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs) : Set (Set α))) =
    HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) s : G)
      (∑ i ∈ hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs, (m : (a : Set α) → G) i : G)
have h_mem : ⋃₀ (↑(insert s (hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs)) : Set (Set α)) ∈ C
Tactic: rw [← coe_insert, addContent_sUnion]
-- 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
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
⊢ ∑ u ∈ insert s (hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs), (m : (a : Set α) → G) u =
    HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) s : G)
      (∑ i ∈ hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs, (m : (a : Set α) → G) i : G)
have rw : s ∉ hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs
Tactic: rw [sum_insert]
-- 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
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
⊢ (↑(insert s (hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs)) : Set (Set α)) ⊆ C
have h_ss : insert s (↑(hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs) : Set (Set α)) ⊆ C
Tactic: rw [coe_insert]
-- 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
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
⊢ (↑(insert s (hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs)) : Set (Set α)).PairwiseDisjoint id
have h_dis : (insert s (↑(hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs) : Set (Set α))).PairwiseDisjoint id
Tactic: rw [coe_insert]
-- 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
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
⊢ ⋃₀ (↑(insert s (hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs)) : Set (Set α)) ∈ C
have h_mem : ⋃₀ insert s (↑(hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs) : Set (Set α)) ∈ C
Tactic: rw [coe_insert]
-- 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
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
⊢ (m : (a : Set α) → G) t =
    HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) s : G)
      (∑ i ∈ hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs, (m : (a : Set α) → G) i : G)
have conv_lhs : (m : (a : Set α) → G) t =
  HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) s : G)
    (∑ i ∈ hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs, (m : (a : Set α) → G) i : G)
Tactic: classical
  conv_lhs => rw [← hC.sUnion_insert_disjointOfDiff ht hs hst]
  rw [← coe_insert, addContent_sUnion]
  · rw [sum_insert]
    exact hC.notMem_disjointOfDiff ht hs
  · rw [coe_insert]
    exact Set.insert_subset hs (hC.subset_disjointOfDiff ht hs)
  · rw [coe_insert]
    exact hC.pairwiseDisjoint_insert_disjointOfDiff ht hs
  · rw [coe_insert]
    rwa [hC.sUnion_insert_disjointOfDiff ht hs hst]
-- 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
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
conv_lhs :
  (m : (a : Set α) → G) t =
    HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) s : G)
      (∑ i ∈ hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs, (m : (a : Set α) → G) i : G)
⊢ (m : (a : Set α) → G) t =
    HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) s : G)
      (∑ i ∈ hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs, (m : (a : Set α) → G) i : G)
have conv_lhs₁ : (m : (a : Set α) → G) (⋃₀ insert s (↑(hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs) : Set (Set α))) =
  HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) s : G)
    (∑ i ∈ hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs, (m : (a : Set α) → G) i : G)
Tactic: classical
  conv_lhs => rw [← hC.sUnion_insert_disjointOfDiff ht hs hst]
  rw [← coe_insert, addContent_sUnion]
  · rw [sum_insert]
    exact hC.notMem_disjointOfDiff ht hs
  · rw [coe_insert]
    exact Set.insert_subset hs (hC.subset_disjointOfDiff ht hs)
  · rw [coe_insert]
    exact hC.pairwiseDisjoint_insert_disjointOfDiff ht hs
  · rw [coe_insert]
    rwa [hC.sUnion_insert_disjointOfDiff ht hs hst]