awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ a ⊆ ⋃₀ (↑(J i) : Set (Set α))

Tactic:
exact subset_sUnion_of_mem ha

Premises used: Set.subset_sUnion_of_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' 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), a ⊆ i

Tactic:
have H {a i} (hi : i ∈ I) (ha : a ∈ J i) : a ⊆ i := by
      rw [hJs i hi]
      exact subset_sUnion_of_mem ha
-- 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 α))
H : ∀ {a i : Set α} (hi : i ∈ I) (ha : a ∈ J i), a ⊆ i
K : Finset (Set α) := I.biUnion J
⊢ ⋃₀ (↑I : Set (Set α)) = ⋃₀ (↑K : Set (Set α))

Tactic:
grind
-- 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 α))
H : ∀ {a i : Set α} (hi : i ∈ I) (ha : a ∈ J i), a ⊆ i
K : Finset (Set α) := I.biUnion J
⊢ ⋃₀ (↑I : Set (Set α)) = ⋃₀ (↑K : Set (Set α))

Tactic:
have : ⋃₀ ↑I = ⋃₀ (↑K : Set (Set α)) := by grind
-- 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 α))
H : ∀ {a i : Set α} (hi : i ∈ I) (ha : a ∈ J i), a ⊆ i
K : Finset (Set α) := I.biUnion J
this : ⋃₀ (↑I : Set (Set α)) = ⋃₀ (↑K : Set (Set α))
⊢ (↑K : Set (Set α)) ⊆ C

Tactic:
simpa [K] using hJC
-- 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 α))
H : ∀ {a i : Set α} (hi : i ∈ I) (ha : a ∈ J i), a ⊆ i
K : Finset (Set α) := I.biUnion J
this : ⋃₀ (↑I : Set (Set α)) = ⋃₀ (↑K : Set (Set α))
rw : Eq.{u_2 + 1} (α := G) (∑ s ∈ K, (m : (a : Set α) → G) s) (∑ u ∈ I, m.supClosureFun (C := C) u)
rw₁ : (↑K : Set (Set α)).PairwiseDisjoint id
⊢ m.supClosureFun (C := C) (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, m.supClosureFun (C := C) u

Tactic:
rw [this, m.supClosureFun_apply hC (J := K) (by simpa [K] using hJC) _ rfl]

Premises used: _private.0.MeasureTheory.AddContent.supClosureFun_apply, 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' 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 α))
H : ∀ {a i : Set α} (hi : i ∈ I) (ha : a ∈ J i), a ⊆ i
K : Finset (Set α) := I.biUnion J
this : ⋃₀ (↑I : Set (Set α)) = ⋃₀ (↑K : Set (Set α))
simp : PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ (↑I : Set (Set α)), (↑(J x) : Set (Set α))) id
⊢ (↑K : Set (Set α)).PairwiseDisjoint id

Tactic:
simp only [K, coe_biUnion]

Premises used: Finset.coe_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 α)) ⊆ (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 α))
H : ∀ {a i : Set α} (hi : i ∈ I) (ha : a ∈ J i), a ⊆ i
K : Finset (Set α) := I.biUnion J
this : ⋃₀ (↑I : Set (Set α)) = ⋃₀ (↑K : Set (Set α))
⊢ PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ (↑I : Set (Set α)), (↑(J x) : Set (Set α))) id

Tactic:
(h'I.mono_on ?_).biUnion hJdisj

Premises used: Set.PairwiseDisjoint.biUnion, Set.PairwiseDisjoint.mono_on
-- 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 α))
H : ∀ {a i : Set α} (hi : i ∈ I) (ha : a ∈ J i), a ⊆ i
K : Finset (Set α) := I.biUnion J
this : ⋃₀ (↑I : Set (Set α)) = ⋃₀ (↑K : Set (Set α))
refine : ∀ ⦃i : Set α⦄, i ∈ (↑I : Set (Set α)) → ⨆ i_1 ∈ (↑(J i) : Set (Set α)), id i_1 ≤ id i
⊢ PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ (↑I : Set (Set α)), (↑(J x) : Set (Set α))) id

Tactic:
refine (h'I.mono_on ?_).biUnion hJdisj

Premises used: Set.PairwiseDisjoint.biUnion, Set.PairwiseDisjoint.mono_on
-- 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 α))
H : ∀ {a i : Set α} (hi : i ∈ I) (ha : a ∈ J i), a ⊆ i
K : Finset (Set α) := I.biUnion J
this : ⋃₀ (↑I : Set (Set α)) = ⋃₀ (↑K : Set (Set α))
simp : ∀ ⦃i : Set α⦄, i ∈ I → ∀ (i_1 : Set α) (i_2 : i_1 ∈ J i), i_1 ⊆ i
⊢ ∀ ⦃i : Set α⦄, i ∈ (↑I : Set (Set α)) → ⨆ i_1 ∈ (↑(J i) : Set (Set α)), id i_1 ≤ id i

Tactic:
simp
-- 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 α))
H : ∀ {a i : Set α} (hi : i ∈ I) (ha : a ∈ J i), a ⊆ i
K : Finset (Set α) := I.biUnion J
this : ⋃₀ (↑I : Set (Set α)) = ⋃₀ (↑K : Set (Set α))
⊢ ∀ ⦃i : Set α⦄, i ∈ I → ∀ (i_1 : Set α) (i_2 : i_1 ∈ J i), i_1 ⊆ i

Tactic:
grind
-- 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 α))
H : ∀ {a i : Set α} (hi : i ∈ I) (ha : a ∈ J i), a ⊆ i
K : Finset (Set α) := I.biUnion J
this : ⋃₀ (↑I : Set (Set α)) = ⋃₀ (↑K : Set (Set α))
simp : Eq.{u_2 + 1} (α := G) (∑ s ∈ I.biUnion J, (m : (a : Set α) → G) s) (∑ u ∈ I, m.supClosureFun (C := C) u)
⊢ Eq.{u_2 + 1} (α := G) (∑ s ∈ K, (m : (a : Set α) → G) s) (∑ u ∈ I, m.supClosureFun (C := C) u)

Tactic:
simp only [K]
-- 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 α))
H : ∀ {a i : Set α} (hi : i ∈ I) (ha : a ∈ J i), a ⊆ i
K : Finset (Set α) := I.biUnion J
this : ⋃₀ (↑I : Set (Set α)) = ⋃₀ (↑K : Set (Set α))
rw : Eq.{u_2 + 1} (α := G) (∑ x ∈ I, ∑ i ∈ J x, (m : (a : Set α) → G) i) (∑ u ∈ I, m.supClosureFun (C := C) u)
rw₁ :
  (↑I : Set (Set α)).Pairwise fun (i j : Set α) ↦
    ∀ k ∈ J i ∩ J j, Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) k : G) (0 : G)
⊢ Eq.{u_2 + 1} (α := G) (∑ s ∈ I.biUnion J, (m : (a : Set α) → G) s) (∑ u ∈ I, m.supClosureFun (C := C) u)

Tactic:
rw [sum_biUnion_of_pairwise_eq_zero]

Premises used: Finset.sum_biUnion_of_pairwise_eq_zero
-- 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 α))
H : ∀ {a i : Set α} (hi : i ∈ I) (ha : a ∈ J i), a ⊆ i
K : Finset (Set α) := I.biUnion J
this : ⋃₀ (↑I : Set (Set α)) = ⋃₀ (↑K : Set (Set α))
i : Set α
hi : i ∈ (↑I : Set (Set α))
j : Set α
hj : j ∈ (↑I : Set (Set α))
hij : i ≠ j
k : Set α
hk : k ∈ J i ∩ J j
⊢ k ∈ J i ∧ k ∈ J j

Tactic:
simp only [Finset.mem_inter] at hk

Premises used: Finset.mem_inter
-- 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 α))
H : ∀ {a i : Set α} (hi : i ∈ I) (ha : a ∈ J i), a ⊆ i
K : Finset (Set α) := I.biUnion J
this : ⋃₀ (↑I : Set (Set α)) = ⋃₀ (↑K : Set (Set α))
i : Set α
hi : i ∈ (↑I : Set (Set α))
j : Set α
hj : j ∈ (↑I : Set (Set α))
hij : i ≠ j
k : Set α
hk : k ∈ J i ∧ k ∈ J j
⊢ Disjoint i j

Tactic:
have : Disjoint i j := h'I hi hj hij
-- 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 α))
H : ∀ {a i : Set α} (hi : i ∈ I) (ha : a ∈ J i), a ⊆ i
K : Finset (Set α) := I.biUnion J
this_1 : ⋃₀ (↑I : Set (Set α)) = ⋃₀ (↑K : Set (Set α))
i : Set α
hi : i ∈ (↑I : Set (Set α))
j : Set α
hj : j ∈ (↑I : Set (Set α))
hij : i ≠ j
k : Set α
hk : k ∈ J i ∧ k ∈ J j
this : Disjoint i j
⊢ Disjoint k k

Tactic:
this.mono (H hi hk.1) (H hj hk.2)

Premises used: And.right, And.left, Disjoint.mono
-- 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 α))
H : ∀ {a i : Set α} (hi : i ∈ I) (ha : a ∈ J i), a ⊆ i
K : Finset (Set α) := I.biUnion J
this_1 : ⋃₀ (↑I : Set (Set α)) = ⋃₀ (↑K : Set (Set α))
i : Set α
hi : i ∈ (↑I : Set (Set α))
j : Set α
hj : j ∈ (↑I : Set (Set α))
hij : i ≠ j
k : Set α
hk : k ∈ J i ∧ k ∈ J j
this : Disjoint i j
⊢ Disjoint k k

Tactic:
exact this.mono (H hi hk.1) (H hj hk.2)

Premises used: And.right, And.left, Disjoint.mono
-- 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 α))
H : ∀ {a i : Set α} (hi : i ∈ I) (ha : a ∈ J i), a ⊆ i
K : Finset (Set α) := I.biUnion J
this : ⋃₀ (↑I : Set (Set α)) = ⋃₀ (↑K : Set (Set α))
i : Set α
hi : i ∈ (↑I : Set (Set α))
j : Set α
hj : j ∈ (↑I : Set (Set α))
hij : i ≠ j
k : Set α
hk : k ∈ J i ∧ k ∈ J j
⊢ Disjoint k k

Tactic:
have : Disjoint k k := by
        have : Disjoint i j := h'I hi hj hij
        exact this.mono (H hi hk.1) (H hj hk.2)
-- 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 α))
H : ∀ {a i : Set α} (hi : i ∈ I) (ha : a ∈ J i), a ⊆ i
K : Finset (Set α) := I.biUnion J
this_1 : ⋃₀ (↑I : Set (Set α)) = ⋃₀ (↑K : Set (Set α))
i : Set α
hi : i ∈ (↑I : Set (Set α))
j : Set α
hj : j ∈ (↑I : Set (Set α))
hij : i ≠ j
k : Set α
hk : k ∈ J i ∧ k ∈ J j
this : Disjoint k k
⊢ k = ∅

Tactic:
simp only [disjoint_self, Set.bot_eq_empty] at this

Premises used: Set.bot_eq_empty, disjoint_self
-- 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 α))
H : ∀ {a i : Set α} (hi : i ∈ I) (ha : a ∈ J i), a ⊆ i
K : Finset (Set α) := I.biUnion J
this_1 : ⋃₀ (↑I : Set (Set α)) = ⋃₀ (↑K : Set (Set α))
i : Set α
hi : i ∈ (↑I : Set (Set α))
j : Set α
hj : j ∈ (↑I : Set (Set α))
hij : i ≠ j
k : Set α
hk : k ∈ J i ∧ k ∈ J j
this : k = ∅
⊢ Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) k : G) (0 : G)

Tactic:
simp [this]
-- 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 α))
H : ∀ {a i : Set α} (hi : i ∈ I) (ha : a ∈ J i), a ⊆ i
K : Finset (Set α) := I.biUnion J
this : ⋃₀ (↑I : Set (Set α)) = ⋃₀ (↑K : Set (Set α))
apply : ∀ (i : Set α) (hi : i ∈ I), m.supClosureFun (C := C) i = ∑ i ∈ J i, (m : (a : Set α) → G) i
⊢ Eq.{u_2 + 1} (α := G) (∑ x ∈ I, ∑ i ∈ J x, (m : (a : Set α) → G) i) (∑ u ∈ I, m.supClosureFun (C := C) u)

Tactic:
apply Finset.sum_congr rfl (fun i hi ↦ Eq.symm ?_)

Premises used: Eq.symm, 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' 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 α))
H : ∀ {a i : Set α} (hi : i ∈ I) (ha : a ∈ J i), a ⊆ i
K : Finset (Set α) := I.biUnion J
this : ⋃₀ (↑I : Set (Set α)) = ⋃₀ (↑K : Set (Set α))
i : Set α
hi : i ∈ I
⊢ m.supClosureFun (C := C) i = ∑ i ∈ J i, (m : (a : Set α) → G) i

Tactic:
m.supClosureFun_apply hC (hJC i hi) (hJdisj i hi) (hJs i hi)

Premises used: _private.0.MeasureTheory.AddContent.supClosureFun_apply