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 α))
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:
exact m.supClosureFun_apply hC (hJC i hi) (hJdisj i hi) (hJs i hi)

Premises used: _private.0.MeasureTheory.AddContent.supClosureFun_apply
-- 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 α))
⊢ Eq.{u_2 + 1} (α := G) ((m.supClosure (C := C) hC : (a : Set α) → G) s : G) (∑ s ∈ J, (m : (a : Set α) → G) s : G)

Tactic:
m.supClosureFun_apply hC hJ h'J hs

Premises used: dite, _private.0.MeasureTheory.AddContent.supClosureFun, _private.0.MeasureTheory.AddContent.supClosureFun_apply
-- 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 : Finpartition s
hJ : (↑(J.parts (a := s)) : Set (Set α)) ⊆ C
rw : s = ⋃₀ (↑(J.parts (a := s)) : Set (Set α))
⊢ Eq.{u_2 + 1} (α := G) ((m.supClosure (C := C) hC : (a : Set α) → G) s : G)
    (∑ s ∈ J.parts (a := s), (m : (a : Set α) → G) s : G)

Tactic:
rw [m.supClosure_apply _ hJ J.disjoint]

Premises used: Finpartition.disjoint, MeasureTheory.AddContent.supClosure_apply
-- 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 : Finpartition s
hJ : (↑(J.parts (a := s)) : Set (Set α)) ⊆ C
nth_rewrite : Eq.{u_1 + 1} (α := Set α) (⋃ x ∈ J.parts (a := s), id x) (⋃ i ∈ (↑(J.parts (a := s)) : Set (Set α)), i)
⊢ s = ⋃₀ (↑(J.parts (a := s)) : Set (Set α))

Tactic:
nth_rewrite 1 [← J.sup_parts, Finset.sup_set_eq_biUnion, sUnion_eq_biUnion]

Premises used: Finset.sup_set_eq_biUnion, Set.sUnion_eq_biUnion, Finpartition.sup_parts
-- 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 : Finpartition s
hJ : (↑(J.parts (a := s)) : Set (Set α)) ⊆ C
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ x ∈ J.parts (a := s), id x) (⋃ i ∈ (↑(J.parts (a := s)) : Set (Set α)), i)

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
⊢ Eq.{u_2 + 1} (α := G) ((m.supClosure (C := C) hC : (a : Set α) → G) s : G) ((m : (a : Set α) → G) s : G)

Tactic:
m.supClosureFun_apply_of_mem hC hs

Premises used: _private.0.MeasureTheory.AddContent.supClosureFun_apply_of_mem, dite, _private.0.MeasureTheory.AddContent.supClosureFun
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
t : Set α
I : Finset (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
inst_1 : PartialOrder G
inst_2 : CanonicallyOrderedAdd G
hC : IsSetSemiring C
h_ss : (↑I : Set (Set α)) ⊆ C
h_dis : (↑I : Set (Set α)).PairwiseDisjoint id
ht : t ∈ C
hJt : ∀ s ∈ I, s ⊆ t
rw :
  ∑ u ∈ I, (m : (a : Set α) → G) u ≤
    HAdd.hAdd (α := G) (∑ i ∈ I, (m : (a : Set α) → G) i)
      (∑ i ∈ hC.disjointOfDiffUnion (C := C) (s := t) ht h_ss, (m : (a : Set α) → G) i)
⊢ LE.le.{u_2} (α := G) (∑ u ∈ I, (m : (a : Set α) → G) u : G) ((m : (a : Set α) → G) t : G)

Tactic:
rw [addContent_eq_add_disjointOfDiffUnion_of_subset hC ht h_ss hJt h_dis]

Premises used: MeasureTheory.addContent_eq_add_disjointOfDiffUnion_of_subset
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
t : Set α
I : Finset (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
inst_1 : PartialOrder G
inst_2 : CanonicallyOrderedAdd G
hC : IsSetSemiring C
h_ss : (↑I : Set (Set α)) ⊆ C
h_dis : (↑I : Set (Set α)).PairwiseDisjoint id
ht : t ∈ C
hJt : ∀ s ∈ I, s ⊆ t
⊢ ∑ u ∈ I, (m : (a : Set α) → G) u ≤
    HAdd.hAdd (α := G) (∑ i ∈ I, (m : (a : Set α) → G) i)
      (∑ i ∈ hC.disjointOfDiffUnion (C := C) (s := t) ht h_ss, (m : (a : Set α) → G) i)

Tactic:
le_add_right le_rfl

Premises used: le_rfl, le_add_right
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
t : Set α
I : Finset (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
inst_1 : PartialOrder G
inst_2 : CanonicallyOrderedAdd G
hC : IsSetSemiring C
h_ss : (↑I : Set (Set α)) ⊆ C
h_dis : (↑I : Set (Set α)).PairwiseDisjoint id
ht : t ∈ C
hJt : ∀ s ∈ I, s ⊆ t
⊢ ∑ u ∈ I, (m : (a : Set α) → G) u ≤
    HAdd.hAdd (α := G) (∑ i ∈ I, (m : (a : Set α) → G) i)
      (∑ i ∈ hC.disjointOfDiffUnion (C := C) (s := t) ht h_ss, (m : (a : Set α) → G) i)

Tactic:
exact le_add_right le_rfl

Premises used: le_rfl, le_add_right
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
t : Set α
I : Finset (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
inst_1 : PartialOrder G
inst_2 : CanonicallyOrderedAdd G
hC : IsSetSemiring C
h_ss : (↑I : Set (Set α)) ⊆ C
h_dis : (↑I : Set (Set α)).PairwiseDisjoint id
ht : t ∈ C
hJt : ∀ s ∈ I, s ⊆ t
rw rw₁ rw₂ :
  ∑ u ∈ I, (m : (a : Set α) → G) u ≤
    HAdd.hAdd (α := G) (∑ i ∈ I, (m : (a : Set α) → G) i)
      (∑ i ∈ hC.disjointOfDiffUnion (C := C) (s := t) ht h_ss, (m : (a : Set α) → G) i)
⊢ LE.le.{u_2} (α := G) (∑ u ∈ I, (m : (a : Set α) → G) u : G) ((m : (a : Set α) → G) t : G)

Tactic:
classical
  rw [addContent_eq_add_disjointOfDiffUnion_of_subset hC ht h_ss hJt h_dis]
  exact le_add_right le_rfl

Premises used: le_rfl, MeasureTheory.addContent_eq_add_disjointOfDiffUnion_of_subset, le_add_right
-- 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
inst_1 : PartialOrder G
inst_2 : CanonicallyOrderedAdd G
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
refine_4 :
  ∀ (h : LE.le.{u_2} (α := G) (∑ u ∈ {s}, (m : (a : Set α) → G) u : G) ((m : (a : Set α) → G) t : G)),
    LE.le.{u_2} (α := G) ((m : (a : Set α) → G) s : G) ((m : (a : Set α) → G) t : G)
refine_1 : (↑{s} : Set (Set α)) ⊆ C
refine_2 : (↑{s} : Set (Set α)).PairwiseDisjoint id
refine_3 : ∀ (s_1 : Set α), Membership.mem (γ := Finset (Set α)) {s} s_1 → s_1 ⊆ t
⊢ LE.le.{u_2} (α := G) ((m : (a : Set α) → G) s : G) ((m : (a : Set α) → G) t : G)

Tactic:
have h := sum_addContent_le_of_subset (m := m) hC (I := {s}) ?_ ?_ ht ?_
-- 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
inst_1 : PartialOrder G
inst_2 : CanonicallyOrderedAdd G
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
h : LE.le.{u_2} (α := G) (∑ u ∈ {s}, (m : (a : Set α) → G) u : G) ((m : (a : Set α) → G) t : G)
⊢ LE.le.{u_2} (α := G) ((m : (a : Set α) → G) s : G) ((m : (a : Set α) → G) t : G)

Tactic:
simpa only [sum_singleton] using h

Premises used: Finset.sum_singleton
-- 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
inst_1 : PartialOrder G
inst_2 : CanonicallyOrderedAdd G
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
refine_1 refine_1₁ refine_1₂ refine_1₃ : s ∈ C
⊢ (↑{s} : Set (Set α)) ⊆ C

Tactic:
rwa [singleton_subset_set_iff]

Premises used: Finset.singleton_subset_set_iff
-- 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
inst_1 : PartialOrder G
inst_2 : CanonicallyOrderedAdd G
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
⊢ (↑{s} : Set (Set α)).PairwiseDisjoint id

Tactic:
simp only [coe_singleton, pairwiseDisjoint_singleton]

Premises used: Finset.coe_singleton, Set.pairwiseDisjoint_singleton
-- 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
inst_1 : PartialOrder G
inst_2 : CanonicallyOrderedAdd G
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
⊢ ∀ (s_1 : Set α), Membership.mem (γ := Finset (Set α)) {s} s_1 → s_1 ⊆ t

Tactic:
simp [hst]
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
inst_1 : PartialOrder G
inst_2 : CanonicallyOrderedAdd G
m : AddContent G C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
h_mem : ⋃₀ (↑J : Set (Set α)) ∈ C
simp : ∀ (i : Set α) (i_1 : i ∈ J), (↑(hC.disjointOfUnion (C := C) h_ss i) : Set (Set α)) ⊆ C
⊢ (↑(J.disjiUnion (hC.disjointOfUnion (C := C) h_ss) ⋯) : Set (Set α)) ⊆ C

Tactic:
simp only [disjiUnion_eq_biUnion, coe_biUnion, mem_coe, iUnion_subset_iff]

Premises used: Finset.coe_biUnion, Finset.disjiUnion_eq_biUnion, Set.iUnion_subset_iff, Finset.mem_coe
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
inst_1 : PartialOrder G
inst_2 : CanonicallyOrderedAdd G
m : AddContent G C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
h_mem : ⋃₀ (↑J : Set (Set α)) ∈ C
⊢ ∀ (i : Set α) (i_1 : i ∈ J), (↑(hC.disjointOfUnion (C := C) h_ss i) : Set (Set α)) ⊆ C

Tactic:
fun _ x ↦ hC.disjointOfUnion_subset h_ss x

Premises used: MeasureTheory.IsSetSemiring.disjointOfUnion_subset
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
inst_1 : PartialOrder G
inst_2 : CanonicallyOrderedAdd G
m : AddContent G C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
h_mem : ⋃₀ (↑J : Set (Set α)) ∈ C
⊢ ∀ (i : Set α) (i_1 : i ∈ J), (↑(hC.disjointOfUnion (C := C) h_ss i) : Set (Set α)) ⊆ C

Tactic:
exact fun _ x ↦ hC.disjointOfUnion_subset h_ss x

Premises used: MeasureTheory.IsSetSemiring.disjointOfUnion_subset
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
inst_1 : PartialOrder G
inst_2 : CanonicallyOrderedAdd G
m : AddContent G C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
h_mem : ⋃₀ (↑J : Set (Set α)) ∈ C
⊢ (↑(J.disjiUnion (hC.disjointOfUnion (C := C) h_ss) ⋯) : Set (Set α)) ⊆ C

Tactic:
have h1 : (disjiUnion J (hC.disjointOfUnion h_ss)
      (hC.pairwiseDisjoint_disjointOfUnion h_ss) : Set (Set α)) ⊆ C := by
    simp only [disjiUnion_eq_biUnion, coe_biUnion, mem_coe, iUnion_subset_iff]
    exact fun _ x ↦ hC.disjointOfUnion_subset h_ss x
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
inst_1 : PartialOrder G
inst_2 : CanonicallyOrderedAdd G
m : AddContent G C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
h_mem : ⋃₀ (↑J : Set (Set α)) ∈ C
h1 : (↑(J.disjiUnion (hC.disjointOfUnion (C := C) h_ss) ⋯) : Set (Set α)) ⊆ C
simp : PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(hC.disjointOfUnion (C := C) h_ss x) : Set (Set α))) id
⊢ (↑(J.disjiUnion (hC.disjointOfUnion (C := C) h_ss) ⋯) : Set (Set α)).PairwiseDisjoint id

Tactic:
simp only [disjiUnion_eq_biUnion, coe_biUnion, mem_coe]

Premises used: Finset.coe_biUnion, Finset.disjiUnion_eq_biUnion, Finset.mem_coe
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
inst_1 : PartialOrder G
inst_2 : CanonicallyOrderedAdd G
m : AddContent G C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
h_mem : ⋃₀ (↑J : Set (Set α)) ∈ C
h1 : (↑(J.disjiUnion (hC.disjointOfUnion (C := C) h_ss) ⋯) : Set (Set α)) ⊆ C
⊢ PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(hC.disjointOfUnion (C := C) h_ss x) : Set (Set α))) id

Tactic:
hC.pairwiseDisjoint_biUnion_disjointOfUnion h_ss

Premises used: MeasureTheory.IsSetSemiring.pairwiseDisjoint_biUnion_disjointOfUnion
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
inst_1 : PartialOrder G
inst_2 : CanonicallyOrderedAdd G
m : AddContent G C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
h_mem : ⋃₀ (↑J : Set (Set α)) ∈ C
h1 : (↑(J.disjiUnion (hC.disjointOfUnion (C := C) h_ss) ⋯) : Set (Set α)) ⊆ C
⊢ PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(hC.disjointOfUnion (C := C) h_ss x) : Set (Set α))) id

Tactic:
exact hC.pairwiseDisjoint_biUnion_disjointOfUnion h_ss

Premises used: MeasureTheory.IsSetSemiring.pairwiseDisjoint_biUnion_disjointOfUnion
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
inst_1 : PartialOrder G
inst_2 : CanonicallyOrderedAdd G
m : AddContent G C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
h_mem : ⋃₀ (↑J : Set (Set α)) ∈ C
h1 : (↑(J.disjiUnion (hC.disjointOfUnion (C := C) h_ss) ⋯) : Set (Set α)) ⊆ C
⊢ (↑(J.disjiUnion (hC.disjointOfUnion (C := C) h_ss) ⋯) : Set (Set α)).PairwiseDisjoint id

Tactic:
have h2 : PairwiseDisjoint (disjiUnion J (hC.disjointOfUnion h_ss)
      ((hC.pairwiseDisjoint_disjointOfUnion h_ss)) : Set (Set α)) id := by
    simp only [disjiUnion_eq_biUnion, coe_biUnion, mem_coe]
    exact hC.pairwiseDisjoint_biUnion_disjointOfUnion h_ss
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
inst_1 : PartialOrder G
inst_2 : CanonicallyOrderedAdd G
m : AddContent G C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
h_mem : ⋃₀ (↑J : Set (Set α)) ∈ C
h1 : (↑(J.disjiUnion (hC.disjointOfUnion (C := C) h_ss) ⋯) : Set (Set α)) ⊆ C
h2 : (↑(J.disjiUnion (hC.disjointOfUnion (C := C) h_ss) ⋯) : Set (Set α)).PairwiseDisjoint id
simp : ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(hC.disjointOfUnion (C := C) h_ss x) : Set (Set α))
⊢ ⋃₀ (↑J : Set (Set α)) = ⋃₀ (↑(J.disjiUnion (hC.disjointOfUnion (C := C) h_ss) ⋯) : Set (Set α))

Tactic:
simp only [disjiUnion_eq_biUnion, coe_biUnion, mem_coe]

Premises used: Finset.coe_biUnion, Finset.disjiUnion_eq_biUnion, Finset.mem_coe
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
inst_1 : PartialOrder G
inst_2 : CanonicallyOrderedAdd G
m : AddContent G C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
h_mem : ⋃₀ (↑J : Set (Set α)) ∈ C
h1 : (↑(J.disjiUnion (hC.disjointOfUnion (C := C) h_ss) ⋯) : Set (Set α)) ⊆ C
h2 : (↑(J.disjiUnion (hC.disjointOfUnion (C := C) h_ss) ⋯) : Set (Set α)).PairwiseDisjoint id
⊢ ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(hC.disjointOfUnion (C := C) h_ss x) : Set (Set α))

Tactic:
(Exists.choose_spec (hC.disjointOfUnion_props h_ss)).2.2.2.2.2

Premises used: Exists.choose_spec, MeasureTheory.IsSetSemiring.disjointOfUnion_props, setOf, And.right
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
inst_1 : PartialOrder G
inst_2 : CanonicallyOrderedAdd G
m : AddContent G C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
h_mem : ⋃₀ (↑J : Set (Set α)) ∈ C
h1 : (↑(J.disjiUnion (hC.disjointOfUnion (C := C) h_ss) ⋯) : Set (Set α)) ⊆ C
h2 : (↑(J.disjiUnion (hC.disjointOfUnion (C := C) h_ss) ⋯) : Set (Set α)).PairwiseDisjoint id
⊢ ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(hC.disjointOfUnion (C := C) h_ss x) : Set (Set α))

Tactic:
exact (Exists.choose_spec (hC.disjointOfUnion_props h_ss)).2.2.2.2.2

Premises used: Exists.choose_spec, MeasureTheory.IsSetSemiring.disjointOfUnion_props, And.right
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
inst_1 : PartialOrder G
inst_2 : CanonicallyOrderedAdd G
m : AddContent G C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
h_mem : ⋃₀ (↑J : Set (Set α)) ∈ C
h1 : (↑(J.disjiUnion (hC.disjointOfUnion (C := C) h_ss) ⋯) : Set (Set α)) ⊆ C
h2 : (↑(J.disjiUnion (hC.disjointOfUnion (C := C) h_ss) ⋯) : Set (Set α)).PairwiseDisjoint id
⊢ ⋃₀ (↑J : Set (Set α)) = ⋃₀ (↑(J.disjiUnion (hC.disjointOfUnion (C := C) h_ss) ⋯) : Set (Set α))

Tactic:
have h3 : ⋃₀ J = ⋃₀ ((disjiUnion J (hC.disjointOfUnion h_ss)
      (hC.pairwiseDisjoint_disjointOfUnion h_ss)) : Set (Set α)) := by
    simp only [disjiUnion_eq_biUnion, coe_biUnion, mem_coe]
    exact (Exists.choose_spec (hC.disjointOfUnion_props h_ss)).2.2.2.2.2
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
inst_1 : PartialOrder G
inst_2 : CanonicallyOrderedAdd G
m : AddContent G C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
h_mem : ⋃₀ (↑J : Set (Set α)) ∈ C
h1 : (↑(J.disjiUnion (hC.disjointOfUnion (C := C) h_ss) ⋯) : Set (Set α)) ⊆ C
h2 : (↑(J.disjiUnion (hC.disjointOfUnion (C := C) h_ss) ⋯) : Set (Set α)).PairwiseDisjoint id
h3 : ⋃₀ (↑J : Set (Set α)) = ⋃₀ (↑(J.disjiUnion (hC.disjointOfUnion (C := C) h_ss) ⋯) : Set (Set α))
rw :
  LE.le.{u_2} (α := G) (∑ i ∈ J, ∑ x ∈ hC.disjointOfUnion (C := C) h_ss i, (m : (a : Set α) → G) x)
    (∑ u ∈ J, (m : (a : Set α) → G) u)
rw₁ : ⋃₀ (↑(J.disjiUnion (hC.disjointOfUnion (C := C) h_ss) ⋯) : Set (Set α)) ∈ C
⊢ LE.le.{u_2} (α := G) ((m : (a : Set α) → G) (⋃₀ (↑J : Set (Set α))) : G) (∑ u ∈ J, (m : (a : Set α) → G) u : G)

Tactic:
rw [h3, addContent_sUnion h1 h2, sum_disjiUnion]

Premises used: MeasureTheory.addContent_sUnion, Finset.sum_disjiUnion
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
inst_1 : PartialOrder G
inst_2 : CanonicallyOrderedAdd G
m : AddContent G C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
h_mem : ⋃₀ (↑J : Set (Set α)) ∈ C
h1 : (↑(J.disjiUnion (hC.disjointOfUnion (C := C) h_ss) ⋯) : Set (Set α)) ⊆ C
h2 : (↑(J.disjiUnion (hC.disjointOfUnion (C := C) h_ss) ⋯) : Set (Set α)).PairwiseDisjoint id
h3 : ⋃₀ (↑J : Set (Set α)) = ⋃₀ (↑(J.disjiUnion (hC.disjointOfUnion (C := C) h_ss) ⋯) : Set (Set α))
h :
  ∀ (x : Set α) (hx : x ∈ J),
    LE.le.{u_2} (α := G) (∑ x ∈ hC.disjointOfUnion (C := C) h_ss x, (m : (a : Set α) → G) x : G)
      ((m : (a : Set α) → G) x : G)
⊢ LE.le.{u_2} (α := G) (∑ i ∈ J, ∑ x ∈ hC.disjointOfUnion (C := C) h_ss i, (m : (a : Set α) → G) x)
    (∑ u ∈ J, (m : (a : Set α) → G) u)

Tactic:
gcongr with x hx
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
inst_1 : PartialOrder G
inst_2 : CanonicallyOrderedAdd G
m : AddContent G C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
h_mem : ⋃₀ (↑J : Set (Set α)) ∈ C
h1 : (↑(J.disjiUnion (hC.disjointOfUnion (C := C) h_ss) ⋯) : Set (Set α)) ⊆ C
h2 : (↑(J.disjiUnion (hC.disjointOfUnion (C := C) h_ss) ⋯) : Set (Set α)).PairwiseDisjoint id
h3 : ⋃₀ (↑J : Set (Set α)) = ⋃₀ (↑(J.disjiUnion (hC.disjointOfUnion (C := C) h_ss) ⋯) : Set (Set α))
x : Set α
hx : x ∈ J
⊢ LE.le.{u_2} (α := G) (∑ x ∈ hC.disjointOfUnion (C := C) h_ss x, (m : (a : Set α) → G) x : G)
    ((m : (a : Set α) → G) x : G)

Tactic:
sum_addContent_le_of_subset hC (hC.disjointOfUnion_subset h_ss hx)
      (hC.pairwiseDisjoint_disjointOfUnion_of_mem h_ss hx) (h_ss hx)
      (fun _ s ↦ hC.subset_of_mem_disjointOfUnion h_ss hx s)

Premises used: MeasureTheory.sum_addContent_le_of_subset, MeasureTheory.IsSetSemiring.pairwiseDisjoint_disjointOfUnion_of_mem, MeasureTheory.IsSetSemiring.disjointOfUnion_subset, MeasureTheory.IsSetSemiring.subset_of_mem_disjointOfUnion
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
inst_1 : PartialOrder G
inst_2 : CanonicallyOrderedAdd G
m : AddContent G C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
h_mem : ⋃₀ (↑J : Set (Set α)) ∈ C
h1 : (↑(J.disjiUnion (hC.disjointOfUnion (C := C) h_ss) ⋯) : Set (Set α)) ⊆ C
h2 : (↑(J.disjiUnion (hC.disjointOfUnion (C := C) h_ss) ⋯) : Set (Set α)).PairwiseDisjoint id
h3 : ⋃₀ (↑J : Set (Set α)) = ⋃₀ (↑(J.disjiUnion (hC.disjointOfUnion (C := C) h_ss) ⋯) : Set (Set α))
x : Set α
hx : x ∈ J
⊢ LE.le.{u_2} (α := G) (∑ x ∈ hC.disjointOfUnion (C := C) h_ss x, (m : (a : Set α) → G) x : G)
    ((m : (a : Set α) → G) x : G)

Tactic:
refine sum_addContent_le_of_subset hC (hC.disjointOfUnion_subset h_ss hx)
      (hC.pairwiseDisjoint_disjointOfUnion_of_mem h_ss hx) (h_ss hx)
      (fun _ s ↦ hC.subset_of_mem_disjointOfUnion h_ss hx s)

Premises used: MeasureTheory.sum_addContent_le_of_subset, MeasureTheory.IsSetSemiring.pairwiseDisjoint_disjointOfUnion_of_mem, MeasureTheory.IsSetSemiring.disjointOfUnion_subset, MeasureTheory.IsSetSemiring.subset_of_mem_disjointOfUnion
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
inst_1 : PartialOrder G
inst_2 : CanonicallyOrderedAdd G
m : AddContent G C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
h_mem : ⋃₀ (↑J : Set (Set α)) ∈ C
h1 : (↑(J.disjiUnion (hC.disjointOfUnion (C := C) h_ss) ⋯) : Set (Set α)) ⊆ C
h2 : (↑(J.disjiUnion (hC.disjointOfUnion (C := C) h_ss) ⋯) : Set (Set α)).PairwiseDisjoint id
h3 : ⋃₀ (↑J : Set (Set α)) = ⋃₀ (↑(J.disjiUnion (hC.disjointOfUnion (C := C) h_ss) ⋯) : Set (Set α))
simp :
  ∀ (h1 : ⋃ x ∈ J, (↑(hC.disjointOfUnion (C := C) h_ss x) : Set (Set α)) ⊆ C)
    (h2 : PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(hC.disjointOfUnion (C := C) h_ss x) : Set (Set α))) id)
    (h3 : ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(hC.disjointOfUnion (C := C) h_ss x) : Set (Set α))),
    ⋃₀ ⋃ x ∈ J, (↑(hC.disjointOfUnion (C := C) h_ss x) : Set (Set α)) ∈ C
⊢ ⋃₀ (↑(J.disjiUnion (hC.disjointOfUnion (C := C) h_ss) ⋯) : Set (Set α)) ∈ C

Tactic:
simp only [disjiUnion_eq_biUnion, coe_biUnion, mem_coe] at *

Premises used: Finset.coe_biUnion, Finset.disjiUnion_eq_biUnion, Finset.mem_coe
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
inst_1 : PartialOrder G
inst_2 : CanonicallyOrderedAdd G
m : AddContent G C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
h_mem : ⋃₀ (↑J : Set (Set α)) ∈ C
h1 : ⋃ x ∈ J, (↑(hC.disjointOfUnion (C := C) h_ss x) : Set (Set α)) ⊆ C
h2 : PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(hC.disjointOfUnion (C := C) h_ss x) : Set (Set α))) id
h3 : ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(hC.disjointOfUnion (C := C) h_ss x) : Set (Set α))
⊢ ⋃₀ ⋃ x ∈ J, (↑(hC.disjointOfUnion (C := C) h_ss x) : Set (Set α)) ∈ C

Tactic:
h3.symm ▸ h_mem

Premises used: Eq.rec, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
inst_1 : PartialOrder G
inst_2 : CanonicallyOrderedAdd G
m : AddContent G C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
h_mem : ⋃₀ (↑J : Set (Set α)) ∈ C
h1 : ⋃ x ∈ J, (↑(hC.disjointOfUnion (C := C) h_ss x) : Set (Set α)) ⊆ C
h2 : PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(hC.disjointOfUnion (C := C) h_ss x) : Set (Set α))) id
h3 : ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(hC.disjointOfUnion (C := C) h_ss x) : Set (Set α))
⊢ ⋃₀ ⋃ x ∈ J, (↑(hC.disjointOfUnion (C := C) h_ss x) : Set (Set α)) ∈ C

Tactic:
exact h3.symm ▸ h_mem