awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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
h_mem : ⋃₀ (↑(I ∪ hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)) ∈ C
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
h_mem₁ : ⋃₀ (↑(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
h_mem₂ h_mem₃ : ⋃₀ (↑(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)

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]

Premises used: MeasureTheory.IsSetSemiring.pairwiseDisjoint_union_disjointOfDiffUnion, MeasureTheory.addContent_sUnion, Finset.sum_union, MeasureTheory.IsSetSemiring.sUnion_union_disjointOfDiffUnion_of_subset, Set.union_subset, MeasureTheory.IsSetSemiring.disjointOfDiffUnion_subset, MeasureTheory.IsSetSemiring.disjoint_disjointOfDiffUnion, Finset.coe_union
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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 : ((m : (a : Set α) → G) (⋃₀ insert s (↑(hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs) : Set (Set α))) : G)
| ((m : (a : Set α) → G) t : G)

Tactic:
rw [← hC.sUnion_insert_disjointOfDiff ht hs hst]

Premises used: MeasureTheory.IsSetSemiring.sUnion_insert_disjointOfDiff
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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) (⋃₀ 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)
⊢ (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:
conv_lhs => rw [← hC.sUnion_insert_disjointOfDiff ht hs hst]

Premises used: MeasureTheory.IsSetSemiring.sUnion_insert_disjointOfDiff
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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
h_mem : ⋃₀ (↑(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)

Tactic:
rw [← coe_insert, addContent_sUnion]

Premises used: MeasureTheory.addContent_sUnion, Finset.coe_insert
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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 : s ∉ hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs
⊢ ∑ 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 [sum_insert]

Premises used: Finset.sum_insert
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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
⊢ s ∉ hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs

Tactic:
hC.notMem_disjointOfDiff ht hs

Premises used: MeasureTheory.IsSetSemiring.notMem_disjointOfDiff
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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
⊢ s ∉ hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs

Tactic:
exact hC.notMem_disjointOfDiff ht hs

Premises used: MeasureTheory.IsSetSemiring.notMem_disjointOfDiff
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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
h_ss : insert s (↑(hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs) : Set (Set α)) ⊆ C
⊢ (↑(insert s (hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs)) : Set (Set α)) ⊆ C

Tactic:
rw [coe_insert]

Premises used: Finset.coe_insert
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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

Tactic:
Set.insert_subset hs (hC.subset_disjointOfDiff ht hs)

Premises used: MeasureTheory.IsSetSemiring.subset_disjointOfDiff, Set.insert_subset
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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

Tactic:
exact Set.insert_subset hs (hC.subset_disjointOfDiff ht hs)

Premises used: MeasureTheory.IsSetSemiring.subset_disjointOfDiff, Set.insert_subset
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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
h_dis : (insert s (↑(hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs) : Set (Set α))).PairwiseDisjoint id
⊢ (↑(insert s (hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs)) : Set (Set α)).PairwiseDisjoint id

Tactic:
rw [coe_insert]

Premises used: Finset.coe_insert
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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

Tactic:
hC.pairwiseDisjoint_insert_disjointOfDiff ht hs

Premises used: MeasureTheory.IsSetSemiring.pairwiseDisjoint_insert_disjointOfDiff
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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

Tactic:
exact hC.pairwiseDisjoint_insert_disjointOfDiff ht hs

Premises used: MeasureTheory.IsSetSemiring.pairwiseDisjoint_insert_disjointOfDiff
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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
h_mem : ⋃₀ insert s (↑(hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs) : Set (Set α)) ∈ C
⊢ ⋃₀ (↑(insert s (hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs)) : Set (Set α)) ∈ C

Tactic:
rw [coe_insert]

Premises used: Finset.coe_insert
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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
h_mem h_mem₁ h_mem₂ h_mem₃ : t ∈ C
⊢ ⋃₀ insert s (↑(hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs) : Set (Set α)) ∈ C

Tactic:
rwa [hC.sUnion_insert_disjointOfDiff ht hs hst]

Premises used: MeasureTheory.IsSetSemiring.sUnion_insert_disjointOfDiff
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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)
conv_lhs₁ 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)
conv_lhs₃ :
  ∑ 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
h_mem : ⋃₀ (↑(insert s (hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs)) : Set (Set α)) ∈ C
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
h_mem₁ : ⋃₀ (↑(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
h_mem₂ h_mem₃ : ⋃₀ (↑(insert s (hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs)) : Set (Set α)) ∈ C
⊢ (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]

Premises used: MeasureTheory.IsSetSemiring.pairwiseDisjoint_insert_disjointOfDiff, MeasureTheory.addContent_sUnion, MeasureTheory.IsSetSemiring.notMem_disjointOfDiff, MeasureTheory.IsSetSemiring.sUnion_insert_disjointOfDiff, Finset.sum_insert, Finset.coe_insert, MeasureTheory.IsSetSemiring.subset_disjointOfDiff, Set.insert_subset
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
J J' : Finset (Set α)
hJ : (↑J : Set (Set α)) ⊆ C
hJdisj : (↑J : Set (Set α)).PairwiseDisjoint id
hJ' : (↑J' : Set (Set α)) ⊆ C
hJ'disj : (↑J' : Set (Set α)).PairwiseDisjoint id
h : ⋃₀ (↑J : Set (Set α)) = ⋃₀ (↑J' : Set (Set α))
apply :
  ∀ (s : Set α) (hs : s ∈ J),
    Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) s : G) (∑ t ∈ J', (m : (a : Set α) → G) (s ∩ t) : G)
⊢ Eq.{u_2 + 1} (α := G) (∑ s ∈ J, (m : (a : Set α) → G) s) (∑ s ∈ J, ∑ t ∈ J', (m : (a : Set α) → G) (s ∩ t))

Tactic:
apply Finset.sum_congr rfl (fun s hs ↦ ?_)

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
J J' : Finset (Set α)
hJ : (↑J : Set (Set α)) ⊆ C
hJdisj : (↑J : Set (Set α)).PairwiseDisjoint id
hJ' : (↑J' : Set (Set α)) ⊆ C
hJ'disj : (↑J' : Set (Set α)).PairwiseDisjoint id
h : ⋃₀ (↑J : Set (Set α)) = ⋃₀ (↑J' : Set (Set α))
s : Set α
hs : s ∈ J
simp_rw : s ⊆ ⋃₀ (↑J : Set (Set α))
⊢ s = ⋃ t ∈ J', s ∩ t

Tactic:
simp_rw [← Finset.set_biUnion_coe, ← inter_iUnion, left_eq_inter, ← sUnion_eq_biUnion, ← h]

Premises used: Finset.set_biUnion_coe, Set.left_eq_inter, Set.sUnion_eq_biUnion, Set.inter_iUnion
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
J J' : Finset (Set α)
hJ : (↑J : Set (Set α)) ⊆ C
hJdisj : (↑J : Set (Set α)).PairwiseDisjoint id
hJ' : (↑J' : Set (Set α)) ⊆ C
hJ'disj : (↑J' : Set (Set α)).PairwiseDisjoint id
h : ⋃₀ (↑J : Set (Set α)) = ⋃₀ (↑J' : Set (Set α))
s : Set α
hs : s ∈ J
⊢ s ⊆ ⋃₀ (↑J : Set (Set α))

Tactic:
subset_sUnion_of_mem hs

Premises used: Set.subset_sUnion_of_mem
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
J J' : Finset (Set α)
hJ : (↑J : Set (Set α)) ⊆ C
hJdisj : (↑J : Set (Set α)).PairwiseDisjoint id
hJ' : (↑J' : Set (Set α)) ⊆ C
hJ'disj : (↑J' : Set (Set α)).PairwiseDisjoint id
h : ⋃₀ (↑J : Set (Set α)) = ⋃₀ (↑J' : Set (Set α))
s : Set α
hs : s ∈ J
⊢ s ⊆ ⋃₀ (↑J : Set (Set α))

Tactic:
exact subset_sUnion_of_mem hs

Premises used: Set.subset_sUnion_of_mem
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
J J' : Finset (Set α)
hJ : (↑J : Set (Set α)) ⊆ C
hJdisj : (↑J : Set (Set α)).PairwiseDisjoint id
hJ' : (↑J' : Set (Set α)) ⊆ C
hJ'disj : (↑J' : Set (Set α)).PairwiseDisjoint id
h : ⋃₀ (↑J : Set (Set α)) = ⋃₀ (↑J' : Set (Set α))
s : Set α
hs : s ∈ J
⊢ s = ⋃ t ∈ J', s ∩ t

Tactic:
have : s = ⋃ t ∈ J', s ∩ t := by
      simp_rw [← Finset.set_biUnion_coe, ← inter_iUnion, left_eq_inter, ← sUnion_eq_biUnion, ← h]
      exact subset_sUnion_of_mem hs
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
J J' : Finset (Set α)
hJ : (↑J : Set (Set α)) ⊆ C
hJdisj : (↑J : Set (Set α)).PairwiseDisjoint id
hJ' : (↑J' : Set (Set α)) ⊆ C
hJ'disj : (↑J' : Set (Set α)).PairwiseDisjoint id
h : ⋃₀ (↑J : Set (Set α)) = ⋃₀ (↑J' : Set (Set α))
s : Set α
hs : s ∈ J
this : s = ⋃ t ∈ J', s ∩ t
nth_rewrite :
  Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (⋃ t ∈ J', s ∩ t) : G) (∑ t ∈ J', (m : (a : Set α) → G) (s ∩ t) : G)
⊢ Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) s : G) (∑ t ∈ J', (m : (a : Set α) → G) (s ∩ t) : G)

Tactic:
nth_rewrite 1 [this]
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
J J' : Finset (Set α)
hJ : (↑J : Set (Set α)) ⊆ C
hJdisj : (↑J : Set (Set α)).PairwiseDisjoint id
hJ' : (↑J' : Set (Set α)) ⊆ C
hJ'disj : (↑J' : Set (Set α)).PairwiseDisjoint id
h : ⋃₀ (↑J : Set (Set α)) = ⋃₀ (↑J' : Set (Set α))
s : Set α
hs : s ∈ J
this : s = ⋃ t ∈ J', s ∩ t
hf : ∀ i ∈ J', s ∩ i ∈ C
h_dis : (↑J' : Set (Set α)).PairwiseDisjoint (Inter.inter s)
h_mem : ⋃ i ∈ J', s ∩ i ∈ C
⊢ Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (⋃ t ∈ J', s ∩ t) : G) (∑ t ∈ J', (m : (a : Set α) → G) (s ∩ t) : G)

Tactic:
apply addContent_biUnion

Premises used: MeasureTheory.addContent_biUnion
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
J J' : Finset (Set α)
hJ : (↑J : Set (Set α)) ⊆ C
hJdisj : (↑J : Set (Set α)).PairwiseDisjoint id
hJ' : (↑J' : Set (Set α)) ⊆ C
hJ'disj : (↑J' : Set (Set α)).PairwiseDisjoint id
h : ⋃₀ (↑J : Set (Set α)) = ⋃₀ (↑J' : Set (Set α))
s : Set α
hs : s ∈ J
this : s = ⋃ t ∈ J', s ∩ t
⊢ ∀ i ∈ J', s ∩ i ∈ C

Tactic:
fun t ht ↦ hC.inter_mem _ (hJ hs) _ (hJ' ht)

Premises used: MeasureTheory.IsSetSemiring.inter_mem
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
J J' : Finset (Set α)
hJ : (↑J : Set (Set α)) ⊆ C
hJdisj : (↑J : Set (Set α)).PairwiseDisjoint id
hJ' : (↑J' : Set (Set α)) ⊆ C
hJ'disj : (↑J' : Set (Set α)).PairwiseDisjoint id
h : ⋃₀ (↑J : Set (Set α)) = ⋃₀ (↑J' : Set (Set α))
s : Set α
hs : s ∈ J
this : s = ⋃ t ∈ J', s ∩ t
x : Set α
⊢ s ∩ x ≤ id x

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
J J' : Finset (Set α)
hJ : (↑J : Set (Set α)) ⊆ C
hJdisj : (↑J : Set (Set α)).PairwiseDisjoint id
hJ' : (↑J' : Set (Set α)) ⊆ C
hJ'disj : (↑J' : Set (Set α)).PairwiseDisjoint id
h : ⋃₀ (↑J : Set (Set α)) = ⋃₀ (↑J' : Set (Set α))
s : Set α
hs : s ∈ J
this : s = ⋃ t ∈ J', s ∩ t
⊢ (↑J' : Set (Set α)).PairwiseDisjoint (Inter.inter s)

Tactic:
exact hJ'disj.mono fun _ ↦ by simp

Premises used: Set.PairwiseDisjoint.mono
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
J J' : Finset (Set α)
hJ : (↑J : Set (Set α)) ⊆ C
hJdisj : (↑J : Set (Set α)).PairwiseDisjoint id
hJ' : (↑J' : Set (Set α)) ⊆ C
hJ'disj : (↑J' : Set (Set α)).PairwiseDisjoint id
h : ⋃₀ (↑J : Set (Set α)) = ⋃₀ (↑J' : Set (Set α))
s : Set α
hs : s ∈ J
this : s = ⋃ t ∈ J', s ∩ t
h_mem : s ∈ C
⊢ ⋃ i ∈ J', s ∩ i ∈ C

Tactic:
rw [← this]
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
J J' : Finset (Set α)
hJ : (↑J : Set (Set α)) ⊆ C
hJdisj : (↑J : Set (Set α)).PairwiseDisjoint id
hJ' : (↑J' : Set (Set α)) ⊆ C
hJ'disj : (↑J' : Set (Set α)).PairwiseDisjoint id
h : ⋃₀ (↑J : Set (Set α)) = ⋃₀ (↑J' : Set (Set α))
s : Set α
hs : s ∈ J
this : s = ⋃ t ∈ J', s ∩ t
⊢ s ∈ C

Tactic:
hJ hs
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
J J' : Finset (Set α)
hJ : (↑J : Set (Set α)) ⊆ C
hJdisj : (↑J : Set (Set α)).PairwiseDisjoint id
hJ' : (↑J' : Set (Set α)) ⊆ C
hJ'disj : (↑J' : Set (Set α)).PairwiseDisjoint id
h : ⋃₀ (↑J : Set (Set α)) = ⋃₀ (↑J' : Set (Set α))
s : Set α
hs : s ∈ J
this : s = ⋃ t ∈ J', s ∩ t
⊢ s ∈ C

Tactic:
exact hJ hs
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
J J' : Finset (Set α)
hJ : (↑J : Set (Set α)) ⊆ C
hJdisj : (↑J : Set (Set α)).PairwiseDisjoint id
hJ' : (↑J' : Set (Set α)) ⊆ C
hJ'disj : (↑J' : Set (Set α)).PairwiseDisjoint id
h : ⋃₀ (↑J : Set (Set α)) = ⋃₀ (↑J' : Set (Set α))
⊢ Eq.{u_2 + 1} (α := G) (∑ s ∈ J, ∑ t ∈ J', (m : (a : Set α) → G) (s ∩ t))
    (∑ t ∈ J', ∑ s ∈ J, (m : (a : Set α) → G) (s ∩ t))

Tactic:
sum_comm

Premises used: Finset.sum_comm
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
J J' : Finset (Set α)
hJ : (↑J : Set (Set α)) ⊆ C
hJdisj : (↑J : Set (Set α)).PairwiseDisjoint id
hJ' : (↑J' : Set (Set α)) ⊆ C
hJ'disj : (↑J' : Set (Set α)).PairwiseDisjoint id
h : ⋃₀ (↑J : Set (Set α)) = ⋃₀ (↑J' : Set (Set α))
apply :
  ∀ (t : Set α) (ht : t ∈ J'),
    Eq.{u_2 + 1} (α := G) (∑ s ∈ J, (m : (a : Set α) → G) (s ∩ t) : G) ((m : (a : Set α) → G) t : G)
⊢ Eq.{u_2 + 1} (α := G) (∑ t ∈ J', ∑ s ∈ J, (m : (a : Set α) → G) (s ∩ t)) (∑ t ∈ J', (m : (a : Set α) → G) t)

Tactic:
apply Finset.sum_congr rfl (fun t ht ↦ ?_)

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
J J' : Finset (Set α)
hJ : (↑J : Set (Set α)) ⊆ C
hJdisj : (↑J : Set (Set α)).PairwiseDisjoint id
hJ' : (↑J' : Set (Set α)) ⊆ C
hJ'disj : (↑J' : Set (Set α)).PairwiseDisjoint id
h : ⋃₀ (↑J : Set (Set α)) = ⋃₀ (↑J' : Set (Set α))
t : Set α
ht : t ∈ J'
simp_rw : t ⊆ ⋃₀ (↑J' : Set (Set α))
⊢ t = ⋃ s ∈ J, s ∩ t

Tactic:
simp_rw [← Finset.set_biUnion_coe, ← iUnion_inter, right_eq_inter, ← sUnion_eq_biUnion, h]

Premises used: Finset.set_biUnion_coe, Set.sUnion_eq_biUnion, Set.iUnion_inter, Set.right_eq_inter
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
J J' : Finset (Set α)
hJ : (↑J : Set (Set α)) ⊆ C
hJdisj : (↑J : Set (Set α)).PairwiseDisjoint id
hJ' : (↑J' : Set (Set α)) ⊆ C
hJ'disj : (↑J' : Set (Set α)).PairwiseDisjoint id
h : ⋃₀ (↑J : Set (Set α)) = ⋃₀ (↑J' : Set (Set α))
t : Set α
ht : t ∈ J'
⊢ t ⊆ ⋃₀ (↑J' : Set (Set α))

Tactic:
subset_sUnion_of_mem ht

Premises used: Set.subset_sUnion_of_mem
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
J J' : Finset (Set α)
hJ : (↑J : Set (Set α)) ⊆ C
hJdisj : (↑J : Set (Set α)).PairwiseDisjoint id
hJ' : (↑J' : Set (Set α)) ⊆ C
hJ'disj : (↑J' : Set (Set α)).PairwiseDisjoint id
h : ⋃₀ (↑J : Set (Set α)) = ⋃₀ (↑J' : Set (Set α))
t : Set α
ht : t ∈ J'
⊢ t ⊆ ⋃₀ (↑J' : Set (Set α))

Tactic:
exact subset_sUnion_of_mem ht

Premises used: Set.subset_sUnion_of_mem
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
J J' : Finset (Set α)
hJ : (↑J : Set (Set α)) ⊆ C
hJdisj : (↑J : Set (Set α)).PairwiseDisjoint id
hJ' : (↑J' : Set (Set α)) ⊆ C
hJ'disj : (↑J' : Set (Set α)).PairwiseDisjoint id
h : ⋃₀ (↑J : Set (Set α)) = ⋃₀ (↑J' : Set (Set α))
t : Set α
ht : t ∈ J'
⊢ t = ⋃ s ∈ J, s ∩ t

Tactic:
have : t = ⋃ s ∈ J, s ∩ t := by
      simp_rw [← Finset.set_biUnion_coe, ← iUnion_inter, right_eq_inter, ← sUnion_eq_biUnion, h]
      exact subset_sUnion_of_mem ht