awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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'
this : t = ⋃ s ∈ J, s ∩ t
nth_rewrite :
  Eq.{u_2 + 1} (α := G) (∑ s ∈ J, (m : (a : Set α) → G) (s ∩ t) : G) ((m : (a : Set α) → G) (⋃ s ∈ J, s ∩ t) : G)
⊢ Eq.{u_2 + 1} (α := G) (∑ s ∈ J, (m : (a : Set α) → G) (s ∩ t) : G) ((m : (a : Set α) → G) t : G)

Tactic:
nth_rewrite 2 [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 α))
t : Set α
ht : t ∈ J'
this : t = ⋃ s ∈ J, s ∩ t
apply : ∀ i ∈ J, i ∩ t ∈ C
apply₁ : (↑J : Set (Set α)).PairwiseDisjoint (α := Set α) fun (i : Set α) ↦ i ∩ t
apply₂ : ⋃ i ∈ J, i ∩ t ∈ C
⊢ Eq.{u_2 + 1} (α := G) (∑ s ∈ J, (m : (a : Set α) → G) (s ∩ t) : G) ((m : (a : Set α) → G) (⋃ s ∈ J, s ∩ t) : G)

Tactic:
apply (addContent_biUnion _ _ _).symm

Premises used: MeasureTheory.addContent_biUnion, Eq.symm
-- 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'
this : t = ⋃ s ∈ J, s ∩ t
⊢ ∀ i ∈ J, i ∩ t ∈ C

Tactic:
fun s hs ↦ 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 α))
t : Set α
ht : t ∈ J'
this : t = ⋃ s ∈ J, s ∩ t
⊢ ∀ i ∈ J, i ∩ t ∈ C

Tactic:
exact fun s hs ↦ 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 α))
t : Set α
ht : t ∈ J'
this : t = ⋃ s ∈ J, s ∩ t
x : Set α
⊢ x ∩ t ≤ 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 α))
t : Set α
ht : t ∈ J'
this : t = ⋃ s ∈ J, s ∩ t
⊢ (↑J : Set (Set α)).PairwiseDisjoint (α := Set α) fun (i : Set α) ↦ i ∩ t

Tactic:
exact hJdisj.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 α))
t : Set α
ht : t ∈ J'
this : t = ⋃ s ∈ J, s ∩ t
rw : t ∈ C
⊢ ⋃ i ∈ J, i ∩ t ∈ 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 α))
t : Set α
ht : t ∈ J'
this : t = ⋃ s ∈ J, s ∩ t
⊢ t ∈ C

Tactic:
hJ' ht
-- 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'
this : t = ⋃ s ∈ J, s ∩ t
⊢ t ∈ C

Tactic:
exact hJ' ht
-- 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 α))
calc : Eq.{u_2 + 1} (α := G) (∑ s ∈ J, (m : (a : Set α) → G) s) (∑ s ∈ J, ∑ t ∈ J', (m : (a : Set α) → G) (s ∩ t))
calc₁ : Eq.{u_2 + 1} (α := G) (∑ t ∈ J', ∑ s ∈ J, (m : (a : Set α) → G) (s ∩ t)) (∑ t ∈ J', (m : (a : Set α) → G) t)
⊢ Eq.{u_2 + 1} (α := G) (∑ s ∈ J, (m : (a : Set α) → G) s) (∑ t ∈ J', (m : (a : Set α) → G) t)

Tactic:
calc ∑ s ∈ J, m s
  _ = ∑ s ∈ J, (∑ t ∈ J', m (s ∩ t)) := by
    apply Finset.sum_congr rfl (fun s hs ↦ ?_)
    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
    nth_rewrite 1 [this]
    apply addContent_biUnion
    · exact fun t ht ↦ hC.inter_mem _ (hJ hs) _ (hJ' ht)
    · exact hJ'disj.mono fun _ ↦ by simp
    · rw [← this]
      exact hJ hs
  _ = ∑ t ∈ J', (∑ s ∈ J, m (s ∩ t)) := sum_comm
  _ = ∑ t ∈ J', m t := by
    apply Finset.sum_congr rfl (fun t ht ↦ ?_)
    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
    nth_rewrite 2 [this]
    apply (addContent_biUnion _ _ _).symm
    · exact fun s hs ↦ hC.inter_mem _ (hJ hs) _ (hJ' ht)
    · exact hJdisj.mono fun _ ↦ by simp
    · rw [← this]
      exact hJ' ht

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

Tactic:
have h : ∃ (J : Finset (Set α)), ↑J ⊆ C ∧ (PairwiseDisjoint (J : Set (Set α)) id) ∧ s = ⋃₀ ↑J :=
    ⟨J, hJ, h'J, hs⟩
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
hC : IsSetSemiring C
m : AddContent G C
s : Set α
J : Finset (Set α)
hJ : (↑J : Set (Set α)) ⊆ C
h'J : (↑J : Set (Set α)).PairwiseDisjoint id
hs : s = ⋃₀ (↑J : Set (Set α))
h : ∃ (J : Finset (Set α)), (↑J : Set (Set α)) ⊆ C ∧ (↑J : Set (Set α)).PairwiseDisjoint id ∧ s = ⋃₀ (↑J : Set (Set α))
simp :
  Eq.{u_2 + 1} (α := G)
    (∑
      s ∈
        ⋯.choose (p := fun (J : Finset (Set α)) ↦
          (↑J : Set (Set α)) ⊆ C ∧ (↑J : Set (Set α)).PairwiseDisjoint id ∧ s = ⋃₀ (↑J : Set (Set α))),
      (m : (a : Set α) → G) s)
    (∑ s ∈ J, (m : (a : Set α) → G) s)
⊢ m.supClosureFun (C := C) s = ∑ s ∈ J, (m : (a : Set α) → G) s

Tactic:
simp only [supClosureFun, h, ↓reduceDIte]

Premises used: reduceDIte, _private.0.MeasureTheory.AddContent.supClosureFun
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
hC : IsSetSemiring C
m : AddContent G C
s : Set α
J : Finset (Set α)
hJ : (↑J : Set (Set α)) ⊆ C
h'J : (↑J : Set (Set α)).PairwiseDisjoint id
hs : s = ⋃₀ (↑J : Set (Set α))
h : ∃ (J : Finset (Set α)), (↑J : Set (Set α)) ⊆ C ∧ (↑J : Set (Set α)).PairwiseDisjoint id ∧ s = ⋃₀ (↑J : Set (Set α))
apply :
  ⋃₀
      (↑(h.choose (p := fun (J : Finset (Set α)) ↦
            (↑J : Set (Set α)) ⊆ C ∧ (↑J : Set (Set α)).PairwiseDisjoint id ∧ s = ⋃₀ (↑J : Set (Set α)))) :
        Set (Set α)) =
    ⋃₀ (↑J : Set (Set α))
⊢ Eq.{u_2 + 1} (α := G)
    (∑
      s ∈
        ⋯.choose (p := fun (J : Finset (Set α)) ↦
          (↑J : Set (Set α)) ⊆ C ∧ (↑J : Set (Set α)).PairwiseDisjoint id ∧ s = ⋃₀ (↑J : Set (Set α))),
      (m : (a : Set α) → G) s)
    (∑ s ∈ J, (m : (a : Set α) → G) s)

Tactic:
apply sum_addContent_eq_of_sUnion_eq hC _ _ h.choose_spec.1 h.choose_spec.2.1 hJ h'J

Premises used: Exists.choose_spec, MeasureTheory.sum_addContent_eq_of_sUnion_eq, And.right, And.left
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
hC : IsSetSemiring C
m : AddContent G C
s : Set α
J : Finset (Set α)
hJ : (↑J : Set (Set α)) ⊆ C
h'J : (↑J : Set (Set α)).PairwiseDisjoint id
hs : s = ⋃₀ (↑J : Set (Set α))
h : ∃ (J : Finset (Set α)), (↑J : Set (Set α)) ⊆ C ∧ (↑J : Set (Set α)).PairwiseDisjoint id ∧ s = ⋃₀ (↑J : Set (Set α))
rw :
  ⋃₀
      (↑(h.choose (p := fun (J : Finset (Set α)) ↦
            (↑J : Set (Set α)) ⊆ C ∧ (↑J : Set (Set α)).PairwiseDisjoint id ∧ s = ⋃₀ (↑J : Set (Set α)))) :
        Set (Set α)) =
    s
⊢ ⋃₀
      (↑(h.choose (p := fun (J : Finset (Set α)) ↦
            (↑J : Set (Set α)) ⊆ C ∧ (↑J : Set (Set α)).PairwiseDisjoint id ∧ s = ⋃₀ (↑J : Set (Set α)))) :
        Set (Set α)) =
    ⋃₀ (↑J : Set (Set α))

Tactic:
rw [← hs]
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
hC : IsSetSemiring C
m : AddContent G C
s : Set α
J : Finset (Set α)
hJ : (↑J : Set (Set α)) ⊆ C
h'J : (↑J : Set (Set α)).PairwiseDisjoint id
hs : s = ⋃₀ (↑J : Set (Set α))
h : ∃ (J : Finset (Set α)), (↑J : Set (Set α)) ⊆ C ∧ (↑J : Set (Set α)).PairwiseDisjoint id ∧ s = ⋃₀ (↑J : Set (Set α))
⊢ ⋃₀
      (↑(h.choose (p := fun (J : Finset (Set α)) ↦
            (↑J : Set (Set α)) ⊆ C ∧ (↑J : Set (Set α)).PairwiseDisjoint id ∧ s = ⋃₀ (↑J : Set (Set α)))) :
        Set (Set α)) =
    s

Tactic:
h.choose_spec.2.2.symm

Premises used: Exists.choose_spec, And.right, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
hC : IsSetSemiring C
m : AddContent G C
s : Set α
J : Finset (Set α)
hJ : (↑J : Set (Set α)) ⊆ C
h'J : (↑J : Set (Set α)).PairwiseDisjoint id
hs : s = ⋃₀ (↑J : Set (Set α))
h : ∃ (J : Finset (Set α)), (↑J : Set (Set α)) ⊆ C ∧ (↑J : Set (Set α)).PairwiseDisjoint id ∧ s = ⋃₀ (↑J : Set (Set α))
⊢ ⋃₀
      (↑(h.choose (p := fun (J : Finset (Set α)) ↦
            (↑J : Set (Set α)) ⊆ C ∧ (↑J : Set (Set α)).PairwiseDisjoint id ∧ s = ⋃₀ (↑J : Set (Set α)))) :
        Set (Set α)) =
    s

Tactic:
exact h.choose_spec.2.2.symm

Premises used: Exists.choose_spec, And.right, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
hC : IsSetSemiring C
m : AddContent G C
s : Set α
hs : s ∈ C
⊢ (↑{s} : Set (Set α)) ⊆ C

Tactic:
simp [hs]
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
hC : IsSetSemiring C
m : AddContent G C
s : Set α
hs : s ∈ C
⊢ (↑{s} : Set (Set α)).PairwiseDisjoint id

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
hC : IsSetSemiring C
m : AddContent G C
s : Set α
hs : s ∈ C
⊢ s = ⋃₀ (↑{s} : Set (Set α))

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
hC : IsSetSemiring C
m : AddContent G C
s : Set α
hs : s ∈ C
⊢ m.supClosureFun (C := C) s = ∑ t ∈ {s}, (m : (a : Set α) → G) t

Tactic:
have : m.supClosureFun s = ∑ t ∈ {s}, m t :=
    m.supClosureFun_apply hC (by simp [hs]) (by simp) (by simp)
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
hC : IsSetSemiring C
m : AddContent G C
s : Set α
hs : s ∈ C
this : m.supClosureFun (C := C) s = ∑ t ∈ {s}, (m : (a : Set α) → G) t
⊢ m.supClosureFun (C := C) s = (m : (a : Set α) → G) s

Tactic:
simp [this]
-- 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' m : AddContent G C
hC : IsSetSemiring C
rw : Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) ∅ : G) (0 : G)
rw₁ rw₂ : Eq.{u_2 + 1} (α := G) 0 0
⊢ m.supClosureFun (C := C) ∅ = 0

Tactic:
rw [m.supClosureFun_apply_of_mem hC hC.empty_mem, addContent_empty]

Premises used: _private.0.MeasureTheory.AddContent.supClosureFun_apply_of_mem, MeasureTheory.IsSetSemiring.empty_mem, MeasureTheory.addContent_empty
-- 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' m : AddContent G C
hC : IsSetSemiring C
I : Finset (Set α)
hI : (↑I : Set (Set α)) ⊆ (_root_.supClosure : (a : Set (Set α)) → Set (Set α)) C
h'I : (↑I : Set (Set α)).PairwiseDisjoint id
hh'I :
  Membership.mem (γ := Set (Set α)) ((_root_.supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α))
    (⋃₀ (↑I : Set (Set α)))
s : Set α
hs : s ∈ I
⊢ Membership.mem (γ := Set (Set α)) ((_root_.supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s

Tactic:
have := hI 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' m : AddContent G C
hC : IsSetSemiring C
I : Finset (Set α)
hI : (↑I : Set (Set α)) ⊆ (_root_.supClosure : (a : Set (Set α)) → Set (Set α)) C
h'I : (↑I : Set (Set α)).PairwiseDisjoint id
hh'I :
  Membership.mem (γ := Set (Set α)) ((_root_.supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α))
    (⋃₀ (↑I : Set (Set α)))
s : Set α
hs : s ∈ I
this : Membership.mem (γ := Set (Set α)) ((_root_.supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (this : ∃ (P : Finpartition s), (↑(P.parts (a := s)) : Set (Set α)) ⊆ C),
    ∃ (P : Finpartition s), (↑(P.parts (a := s)) : Set (Set α)) ⊆ C
⊢ ∃ (P : Finpartition s), (↑(P.parts (a := s)) : Set (Set α)) ⊆ C

Tactic:
rwa [hC.mem_supClosure_iff] at this

Premises used: MeasureTheory.IsSetSemiring.mem_supClosure_iff
-- 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' m : AddContent G C
hC : IsSetSemiring C
I : Finset (Set α)
hI : (↑I : Set (Set α)) ⊆ (_root_.supClosure : (a : Set (Set α)) → Set (Set α)) C
h'I : (↑I : Set (Set α)).PairwiseDisjoint id
hh'I :
  Membership.mem (γ := Set (Set α)) ((_root_.supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α))
    (⋃₀ (↑I : Set (Set α)))
s : Set α
hs : s ∈ I
obtain :
  ∀ (P : Finpartition s) (PC : (↑(P.parts (a := s)) : Set (Set α)) ⊆ C),
    ∃ (J : Finset (Set α)), (↑J : Set (Set α)) ⊆ C ∧ (↑J : Set (Set α)).PairwiseDisjoint id ∧ s = ⋃₀ (↑J : Set (Set α))
⊢ ∃ (J : Finset (Set α)), (↑J : Set (Set α)) ⊆ C ∧ (↑J : Set (Set α)).PairwiseDisjoint id ∧ s = ⋃₀ (↑J : Set (Set α))

Tactic:
obtain ⟨P, PC⟩ : ∃ (P : Finpartition s), ↑P.parts ⊆ C := by
        have := hI hs
        rwa [hC.mem_supClosure_iff] at this

Premises used: Finpartition
-- 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' m : AddContent G C
hC : IsSetSemiring C
I : Finset (Set α)
hI : (↑I : Set (Set α)) ⊆ (supClosure : (a : Set (Set α)) → Set (Set α)) C
h'I : (↑I : Set (Set α)).PairwiseDisjoint id
hh'I :
  Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α))
    (⋃₀ (↑I : Set (Set α)))
s : Set α
hs : s ∈ I
P : Finpartition s
PC : (↑(P.parts (a := s)) : Set (Set α)) ⊆ C
⊢ ∃ (J : Finset (Set α)), (↑J : Set (Set α)) ⊆ C ∧ (↑J : Set (Set α)).PairwiseDisjoint id ∧ s = ⋃₀ (↑J : Set (Set α))

Tactic:
⟨P.parts, PC, P.disjoint, ?_⟩

Premises used: Finpartition.disjoint, Finpartition.parts, And.intro, Exists.intro
-- 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' m : AddContent G C
hC : IsSetSemiring C
I : Finset (Set α)
hI : (↑I : Set (Set α)) ⊆ (_root_.supClosure : (a : Set (Set α)) → Set (Set α)) C
h'I : (↑I : Set (Set α)).PairwiseDisjoint id
hh'I :
  Membership.mem (γ := Set (Set α)) ((_root_.supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α))
    (⋃₀ (↑I : Set (Set α)))
s : Set α
hs : s ∈ I
P : Finpartition s
PC : (↑(P.parts (a := s)) : Set (Set α)) ⊆ C
refine : s = ⋃₀ (↑(P.parts (a := s)) : Set (Set α))
⊢ ∃ (J : Finset (Set α)), (↑J : Set (Set α)) ⊆ C ∧ (↑J : Set (Set α)).PairwiseDisjoint id ∧ s = ⋃₀ (↑J : Set (Set α))

Tactic:
refine ⟨P.parts, PC, P.disjoint, ?_⟩
-- 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' m : AddContent G C
hC : IsSetSemiring C
I : Finset (Set α)
hI : (↑I : Set (Set α)) ⊆ (supClosure : (a : Set (Set α)) → Set (Set α)) C
h'I : (↑I : Set (Set α)).PairwiseDisjoint id
hh'I :
  Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α))
    (⋃₀ (↑I : Set (Set α)))
s : Set α
hs : s ∈ I
P : Finpartition s
PC : (↑(P.parts (a := s)) : Set (Set α)) ⊆ C
⊢ s = P.parts (a := s).sup id

Tactic:
P.sup_parts.symm

Premises used: Eq.symm, Finpartition.sup_parts
-- 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' m : AddContent G C
hC : IsSetSemiring C
I : Finset (Set α)
hI : (↑I : Set (Set α)) ⊆ (_root_.supClosure : (a : Set (Set α)) → Set (Set α)) C
h'I : (↑I : Set (Set α)).PairwiseDisjoint id
hh'I :
  Membership.mem (γ := Set (Set α)) ((_root_.supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α))
    (⋃₀ (↑I : Set (Set α)))
s : Set α
hs : s ∈ I
P : Finpartition s
PC : (↑(P.parts (a := s)) : Set (Set α)) ⊆ C
h : ⋃₀ (↑(P.parts (a := s)) : Set (Set α)) = P.parts (a := s).sup id
⊢ s = ⋃₀ (↑(P.parts (a := s)) : Set (Set α))

Tactic:
convert! P.sup_parts.symm

Premises used: Eq.symm, Finpartition.sup_parts
-- 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' m : AddContent G C
hC : IsSetSemiring C
I : Finset (Set α)
hI : (↑I : Set (Set α)) ⊆ (_root_.supClosure : (a : Set (Set α)) → Set (Set α)) C
h'I : (↑I : Set (Set α)).PairwiseDisjoint id
hh'I :
  Membership.mem (γ := Set (Set α)) ((_root_.supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α))
    (⋃₀ (↑I : Set (Set α)))
s : Set α
hs : s ∈ I
P : Finpartition s
PC : (↑(P.parts (a := s)) : Set (Set α)) ⊆ C
⊢ ⋃₀ (↑(P.parts (a := s)) : Set (Set α)) = P.parts (a := s).sup id

Tactic:
simp [sUnion_eq_biUnion]

Premises used: Set.sUnion_eq_biUnion
-- 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' m : AddContent G C
hC : IsSetSemiring C
I : Finset (Set α)
hI : (↑I : Set (Set α)) ⊆ (_root_.supClosure : (a : Set (Set α)) → Set (Set α)) C
h'I : (↑I : Set (Set α)).PairwiseDisjoint id
hh'I :
  Membership.mem (γ := Set (Set α)) ((_root_.supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α))
    (⋃₀ (↑I : Set (Set α)))
⊢ ∀ (s : Set α) (hs : s ∈ I),
    ∃ (J : Finset (Set α)), (↑J : Set (Set α)) ⊆ C ∧ (↑J : Set (Set α)).PairwiseDisjoint id ∧ s = ⋃₀ (↑J : Set (Set α))

Tactic:
have A (s) (hs : s ∈ I) : ∃ (J : Finset (Set α)),
        ↑J ⊆ C ∧ (PairwiseDisjoint (J : Set (Set α)) id) ∧ s = ⋃₀ ↑J := by
      obtain ⟨P, PC⟩ : ∃ (P : Finpartition s), ↑P.parts ⊆ C := by
        have := hI hs
        rwa [hC.mem_supClosure_iff] at this
      refine ⟨P.parts, PC, P.disjoint, ?_⟩
      convert! P.sup_parts.symm
      simp [sUnion_eq_biUnion]
-- 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' m : AddContent G C
hC : IsSetSemiring C
I : Finset (Set α)
hI : (↑I : Set (Set α)) ⊆ (_root_.supClosure : (a : Set (Set α)) → Set (Set α)) C
h'I : (↑I : Set (Set α)).PairwiseDisjoint id
hh'I :
  Membership.mem (γ := Set (Set α)) ((_root_.supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α))
    (⋃₀ (↑I : Set (Set α)))
A :
  ∀ (s : Set α) (hs : s ∈ I),
    ∃ (J : Finset (Set α)), (↑J : Set (Set α)) ⊆ C ∧ (↑J : Set (Set α)).PairwiseDisjoint id ∧ s = ⋃₀ (↑J : Set (Set α))
choose! :
  ∀ (J : (s : Set α) → Finset (Set α)) (hJC : ∀ (s : Set α) (hs : s ∈ I), (↑(J s) : Set (Set α)) ⊆ C)
    (hJdisj : ∀ (s : Set α) (hs : s ∈ I), (↑(J s) : Set (Set α)).PairwiseDisjoint id)
    (hJs : ∀ (s : Set α) (hs : s ∈ I), s = ⋃₀ (↑(J s) : Set (Set α))),
    m.supClosureFun (C := C) (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, m.supClosureFun (C := C) u
⊢ m.supClosureFun (C := C) (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, m.supClosureFun (C := C) u

Tactic:
choose! J hJC hJdisj hJs using A
-- 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' m : AddContent G C
hC : IsSetSemiring C
I : Finset (Set α)
hI : (↑I : Set (Set α)) ⊆ (_root_.supClosure : (a : Set (Set α)) → Set (Set α)) C
h'I : (↑I : Set (Set α)).PairwiseDisjoint id
hh'I :
  Membership.mem (γ := Set (Set α)) ((_root_.supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α))
    (⋃₀ (↑I : Set (Set α)))
J : (s : Set α) → Finset (Set α)
hJC : ∀ (s : Set α) (hs : s ∈ I), (↑(J s) : Set (Set α)) ⊆ C
hJdisj : ∀ (s : Set α) (hs : s ∈ I), (↑(J s) : Set (Set α)).PairwiseDisjoint id
hJs : ∀ (s : Set α) (hs : s ∈ I), s = ⋃₀ (↑(J s) : Set (Set α))
a i : Set α
hi : i ∈ I
ha : a ∈ J i
rw : a ⊆ ⋃₀ (↑(J i) : Set (Set α))
⊢ a ⊆ i

Tactic:
rw [hJs i hi]
-- 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' m : AddContent G C
hC : IsSetSemiring C
I : Finset (Set α)
hI : (↑I : Set (Set α)) ⊆ (supClosure : (a : Set (Set α)) → Set (Set α)) C
h'I : (↑I : Set (Set α)).PairwiseDisjoint id
hh'I :
  Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α))
    (⋃₀ (↑I : Set (Set α)))
J : (s : Set α) → Finset (Set α)
hJC : ∀ (s : Set α) (hs : s ∈ I), (↑(J s) : Set (Set α)) ⊆ C
hJdisj : ∀ (s : Set α) (hs : s ∈ I), (↑(J s) : Set (Set α)).PairwiseDisjoint id
hJs : ∀ (s : Set α) (hs : s ∈ I), s = ⋃₀ (↑(J s) : Set (Set α))
a i : Set α
hi : i ∈ I
ha : a ∈ J i
⊢ a ⊆ ⋃₀ (↑(J i) : Set (Set α))

Tactic:
subset_sUnion_of_mem ha

Premises used: Set.subset_sUnion_of_mem