awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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
⊢ ∅ ∈ C

Tactic:
exact hC.empty_mem

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

Tactic:
rw [extend_eq]

Premises used: MeasureTheory.extend_eq
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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
⊢ ⋃₀ (↑I : Set (Set α)) ∈ C

Tactic:
h_mem
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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
⊢ ⋃₀ (↑I : Set (Set α)) ∈ C

Tactic:
exact h_mem
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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
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)
⊢ 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 [addContent_sUnion h_ss h_dis h_mem]

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

Tactic:
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 α)
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
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
⊢ 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:
refine 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 α)
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
h : s ∈ C
⊢ (m : (a : Set α) → ℝ≥0∞) s =
    extend (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) s

Tactic:
rw [extend_eq]

Premises used: MeasureTheory.extend_eq
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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
⊢ s ∈ C

Tactic:
h_ss hs
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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
⊢ s ∈ C

Tactic:
exact h_ss hs
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
⊢ Eq (α := (a : Set α) → ℝ≥0∞) (⇑(AddContent.extend (C := C) hC m) : (a : Set α) → ℝ≥0∞)
    (extend (P := Membership.mem C) fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x)

Tactic:
rfl

Premises used: iInf, MeasureTheory.extend, rfl, ite
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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
rwa₁ : Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h : s ∈ C
rwa₂ : Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h₁ h₂ h₃ : s ∈ C
⊢ Eq (α := ℝ≥0∞) ((AddContent.extend (C := C) hC m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rwa [m.extend_eq_extend, extend_eq]

Premises used: MeasureTheory.extend_eq, MeasureTheory.AddContent.extend_eq_extend
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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 = ∞
rwa₁ : Eq (α := ℝ≥0∞) ∞ ∞
h : s ∉ C
rwa₂ : Eq (α := ℝ≥0∞) ∞ ∞
h₁ h₂ h₃ : s ∉ C
⊢ Eq (α := ℝ≥0∞) ((AddContent.extend (C := C) hC m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rwa [m.extend_eq_extend, extend_eq_top]

Premises used: MeasureTheory.extend_eq_top, MeasureTheory.AddContent.extend_eq_extend
-- 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 : IsSetRing C
hs : s ∈ C
ht : t ∈ C
h_dis : Disjoint s t
⊢ (m : (a : Set α) → G) (s ∪ t) =
    HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) s : G) ((m : (a : Set α) → G) t : G)

Tactic:
addContent_union' hs ht (hC.union_mem hs ht) h_dis

Premises used: MeasureTheory.IsSetRing.union_mem, MeasureTheory.addContent_union'
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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 α
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:
simp
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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.insert i S, s n ∈ C
hS : (↑(Insert.insert i S) : Set ι).PairwiseDisjoint s
insert :
  (m : (a : Set α) → G) (⋃ i_1 ∈ Insert.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)
⊢ Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (⋃ i_1 ∈ Insert.insert i S, s i_1) : G)
    (∑ i ∈ Insert.insert i S, (m : (a : Set α) → G) (s i) : G)

Tactic:
rw [Finset.sum_insert hiS]

Premises used: Finset.sum_insert
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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.insert i S, s n ∈ C
hS : (↑(Insert.insert i S) : Set ι).PairwiseDisjoint s
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)
⊢ (m : (a : Set α) → G) (⋃ i_1 ∈ Insert.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:
simp_rw [← Finset.mem_coe, Finset.coe_insert, Set.biUnion_insert]

Premises used: Set.biUnion_insert, Finset.coe_insert, Finset.mem_coe
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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
⊢ s i ∈ C ∧ ∀ a ∈ S, s a ∈ C

Tactic:
simp only [Finset.mem_insert, forall_eq_or_imp] at hs

Premises used: Finset.mem_insert, forall_eq_or_imp
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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
⊢ (↑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

Premises used: Set.pairwiseDisjoint_insert, Finset.coe_insert
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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)
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)
⊢ (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:
rw [← h hs.2 hS.1]

Premises used: And.right, And.left
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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)

Tactic:
addContent_union hC hs.1 (hC.biUnion_mem S hs.2) ?_

Premises used: MeasureTheory.addContent_union, And.right, And.left, MeasureTheory.IsSetRing.biUnion_mem
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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)
insert : Disjoint (s i) (⋃ x ∈ (↑S : Set ι), s x)
⊢ (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:
refine addContent_union hC hs.1 (hC.biUnion_mem S hs.2) ?_

Premises used: MeasureTheory.addContent_union, And.right, And.left, MeasureTheory.IsSetRing.biUnion_mem
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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)
insert : ∀ (i_1 : ι) (j : i_1 ∈ (↑S : Set ι)), Disjoint (s i) (s i_1)
⊢ Disjoint (s i) (⋃ x ∈ (↑S : Set ι), s x)

Tactic:
rw [disjoint_iUnion₂_right]

Premises used: Set.disjoint_iUnion₂_right
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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)
⊢ ∀ (i_1 : ι) (j : i_1 ∈ (↑S : Set ι)), Disjoint (s i) (s i_1)

Tactic:
fun j hjS ↦ hS.2 j hjS (ne_of_mem_of_not_mem hjS hiS).symm

Premises used: Ne.symm, ne_of_mem_of_not_mem, And.right
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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)
⊢ ∀ (i_1 : ι) (j : i_1 ∈ (↑S : Set ι)), Disjoint (s i) (s i_1)

Tactic:
exact fun j hjS ↦ hS.2 j hjS (ne_of_mem_of_not_mem hjS hiS).symm

Premises used: Ne.symm, ne_of_mem_of_not_mem, And.right
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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)
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.insert i S, s n ∈ C) (hS : (↑(Insert.insert i S) : Set ι).PairwiseDisjoint s),
    Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (⋃ i_1 ∈ Insert.insert i S, s i_1) : G)
      (∑ i ∈ Insert.insert i S, (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)

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

Premises used: Set.biUnion_insert, Insert.insert, Finset.mem_insert, forall_eq_or_imp, Set.disjoint_iUnion₂_right, Set.pairwiseDisjoint_insert, Finset.coe_insert, Finset.mem_coe
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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)
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.insert i S, s n ∈ C) (hS : (↑(Insert.insert i S) : Set ι).PairwiseDisjoint s),
    Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (⋃ i_1 ∈ Insert.insert i S, s i_1) : G)
      (∑ i ∈ Insert.insert i S, (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)

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

Premises used: Set.biUnion_insert, Insert.insert, Finset.mem_insert, forall_eq_or_imp, Set.disjoint_iUnion₂_right, Set.pairwiseDisjoint_insert, Finset.coe_insert, Finset.mem_coe
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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
⊢ 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:
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 : 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))
rw : accumulate s n ∈ C
⊢ 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:
rw [Finset.sum_range_succ, ← hn, Set.accumulate_succ, addContent_union hC _ (hsC _)]

Premises used: Set.accumulate_succ, MeasureTheory.addContent_union, Finset.sum_range_succ
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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)
⊢ Disjoint (accumulate s n) (s (n + 1))

Tactic:
Set.disjoint_accumulate hs_disj (Nat.lt_succ_self n)

Premises used: Set.disjoint_accumulate, Nat.lt_succ_self
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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)
⊢ Disjoint (accumulate s n) (s (n + 1))

Tactic:
exact Set.disjoint_accumulate hs_disj (Nat.lt_succ_self n)

Premises used: Set.disjoint_accumulate, Nat.lt_succ_self
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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)
⊢ accumulate s n ∈ C

Tactic:
hC.accumulate_mem hsC n

Premises used: MeasureTheory.IsSetRing.accumulate_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 : 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)
⊢ accumulate s n ∈ C

Tactic:
exact hC.accumulate_mem hsC n

Premises used: MeasureTheory.IsSetRing.accumulate_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 : 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)
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)
⊢ 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)

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

Premises used: Set.accumulate_succ, Set.disjoint_accumulate, Nat.lt_succ_self, MeasureTheory.addContent_union, MeasureTheory.IsSetRing.accumulate_mem, Finset.sum_range_succ