awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
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 α))
⊢ Eq.{u_2 + 1} (α := G) (∑ x ∈ I, ∑ i ∈ J x, (m : (a : Set α) → G) i) (∑ u ∈ I, m.supClosureFun (C := C) u)
have apply : ∀ (i : Set α) (hi : i ∈ I), m.supClosureFun (C := C) i = ∑ i ∈ J i, (m : (a : Set α) → G) i
Tactic: apply Finset.sum_congr rfl (fun i hi ↦ Eq.symm ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
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 α)))
⊢ m.supClosureFun (C := C) (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, m.supClosureFun (C := C) u
have have : ∀ (s : Set α) (hs : s ∈ I),
  ∃ (J : Finset (Set α)), (↑J : Set (Set α)) ⊆ C ∧ (↑J : Set (Set α)).PairwiseDisjoint id ∧ s = ⋃₀ (↑J : Set (Set α))
Tactic: classical
    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]
    choose! J hJC hJdisj hJs using A
    have H {a i} (hi : i ∈ I) (ha : a ∈ J i) : a ⊆ i := by
      rw [hJs i hi]
      exact subset_sUnion_of_mem ha
    let K : Finset (Set α) := Finset.biUnion I J
    have : ⋃₀ ↑I = ⋃₀ (↑K : Set (Set α)) := by grind
    rw [this, m.supClosureFun_apply hC (J := K) (by simpa [K] using hJC) _ rfl]; swap
    · simp only [K, coe_biUnion]
      refine (h'I.mono_on ?_).biUnion hJdisj
      simp
      grind
    simp only [K]
    rw [sum_biUnion_of_pairwise_eq_zero]; swap
    · intro i hi j hj hij k hk
      simp only [Finset.mem_inter] at hk
      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)
      simp only [disjoint_self, Set.bot_eq_empty] at this
      simp [this]
    apply Finset.sum_congr rfl (fun i hi ↦ Eq.symm ?_)
    exact m.supClosureFun_apply hC (hJC i hi) (hJdisj i hi) (hJs i hi)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
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 α)))
have :
  ∀ (s : Set α) (hs : s ∈ I),
    ∃ (J : Finset (Set α)), (↑J : Set (Set α)) ⊆ C ∧ (↑J : Set (Set α)).PairwiseDisjoint id ∧ s = ⋃₀ (↑J : Set (Set α))
⊢ m.supClosureFun (C := C) (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, m.supClosureFun (C := C) u
have have₁ : ∀
  (A :
    ∀ (s : Set α) (hs : s ∈ I),
      ∃ (J : Finset (Set α)),
        (↑J : Set (Set α)) ⊆ C ∧ (↑J : Set (Set α)).PairwiseDisjoint id ∧ s = ⋃₀ (↑J : Set (Set α))),
  m.supClosureFun (C := C) (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, m.supClosureFun (C := C) u
Tactic: classical
    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]
    choose! J hJC hJdisj hJs using A
    have H {a i} (hi : i ∈ I) (ha : a ∈ J i) : a ⊆ i := by
      rw [hJs i hi]
      exact subset_sUnion_of_mem ha
    let K : Finset (Set α) := Finset.biUnion I J
    have : ⋃₀ ↑I = ⋃₀ (↑K : Set (Set α)) := by grind
    rw [this, m.supClosureFun_apply hC (J := K) (by simpa [K] using hJC) _ rfl]; swap
    · simp only [K, coe_biUnion]
      refine (h'I.mono_on ?_).biUnion hJdisj
      simp
      grind
    simp only [K]
    rw [sum_biUnion_of_pairwise_eq_zero]; swap
    · intro i hi j hj hij k hk
      simp only [Finset.mem_inter] at hk
      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)
      simp only [disjoint_self, Set.bot_eq_empty] at this
      simp [this]
    apply Finset.sum_congr rfl (fun i hi ↦ Eq.symm ?_)
    exact m.supClosureFun_apply hC (hJC i hi) (hJdisj i hi) (hJs i hi)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
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 α)))
have :
  ∀ (s : Set α) (hs : s ∈ I),
    ∃ (J : Finset (Set α)), (↑J : Set (Set α)) ⊆ C ∧ (↑J : Set (Set α)).PairwiseDisjoint id ∧ s = ⋃₀ (↑J : Set (Set α))
have₁ :
  ∀
    (A :
      ∀ (s : Set α) (hs : s ∈ I),
        ∃ (J : Finset (Set α)),
          (↑J : Set (Set α)) ⊆ C ∧ (↑J : Set (Set α)).PairwiseDisjoint id ∧ s = ⋃₀ (↑J : Set (Set α))),
    m.supClosureFun (C := C) (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, m.supClosureFun (C := C) u
have₂ :
  ∀ (s : Set α) (hs : s ∈ I),
    ∃ (J : Finset (Set α)), (↑J : Set (Set α)) ⊆ C ∧ (↑J : Set (Set α)).PairwiseDisjoint id ∧ s = ⋃₀ (↑J : Set (Set α))
have₃ have₄ :
  ∀
    (A :
      ∀ (s : Set α) (hs : s ∈ I),
        ∃ (J : Finset (Set α)),
          (↑J : Set (Set α)) ⊆ C ∧ (↑J : Set (Set α)).PairwiseDisjoint id ∧ s = ⋃₀ (↑J : 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
have have₅ : ∀ (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
Tactic: classical
    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]
    choose! J hJC hJdisj hJs using A
    have H {a i} (hi : i ∈ I) (ha : a ∈ J i) : a ⊆ i := by
      rw [hJs i hi]
      exact subset_sUnion_of_mem ha
    let K : Finset (Set α) := Finset.biUnion I J
    have : ⋃₀ ↑I = ⋃₀ (↑K : Set (Set α)) := by grind
    rw [this, m.supClosureFun_apply hC (J := K) (by simpa [K] using hJC) _ rfl]; swap
    · simp only [K, coe_biUnion]
      refine (h'I.mono_on ?_).biUnion hJdisj
      simp
      grind
    simp only [K]
    rw [sum_biUnion_of_pairwise_eq_zero]; swap
    · intro i hi j hj hij k hk
      simp only [Finset.mem_inter] at hk
      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)
      simp only [disjoint_self, Set.bot_eq_empty] at this
      simp [this]
    apply Finset.sum_congr rfl (fun i hi ↦ Eq.symm ?_)
    exact m.supClosureFun_apply hC (hJC i hi) (hJdisj i hi) (hJs i hi)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
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_2 + 1} (α := G) ((m.supClosure (C := C) hC : (a : Set α) → G) s : G)
    (∑ s ∈ J.parts (a := s), (m : (a : Set α) → G) s : G)
have rw : s = ⋃₀ (↑(J.parts (a := s)) : Set (Set α))
Tactic: rw [m.supClosure_apply _ hJ J.disjoint]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
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
⊢ s = ⋃₀ (↑(J.parts (a := s)) : Set (Set α))
have nth_rewrite : Eq.{u_1 + 1} (α := Set α) (⋃ x ∈ J.parts (a := s), id x) (⋃ i ∈ (↑(J.parts (a := s)) : Set (Set α)), i)
Tactic: nth_rewrite 1 [← J.sup_parts, Finset.sup_set_eq_biUnion, sUnion_eq_biUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
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
⊢ LE.le.{u_2} (α := G) (∑ u ∈ I, (m : (a : Set α) → G) u : G) ((m : (a : Set α) → G) t : G)
have 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)
Tactic: rw [addContent_eq_add_disjointOfDiffUnion_of_subset hC ht h_ss hJt h_dis]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
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
⊢ LE.le.{u_2} (α := G) (∑ u ∈ I, (m : (a : Set α) → G) u : G) ((m : (a : Set α) → G) t : G)
have 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)
Tactic: classical
  rw [addContent_eq_add_disjointOfDiffUnion_of_subset hC ht h_ss hJt h_dis]
  exact le_add_right le_rfl
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
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
⊢ LE.le.{u_2} (α := G) ((m : (a : Set α) → G) s : G) ((m : (a : Set α) → G) t : G)
have 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)
Tactic: have h := sum_addContent_le_of_subset (m := m) hC (I := {s}) ?_ ?_ ht ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
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)
⊢ LE.le.{u_2} (α := G) ((m : (a : Set α) → G) s : G) ((m : (a : Set α) → G) t : G)
have refine_1 : (↑{s} : Set (Set α)) ⊆ C
Tactic: have h := sum_addContent_le_of_subset (m := m) hC (I := {s}) ?_ ?_ ht ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
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
⊢ LE.le.{u_2} (α := G) ((m : (a : Set α) → G) s : G) ((m : (a : Set α) → G) t : G)
have refine_2 : (↑{s} : Set (Set α)).PairwiseDisjoint id
Tactic: have h := sum_addContent_le_of_subset (m := m) hC (I := {s}) ?_ ?_ ht ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
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
⊢ LE.le.{u_2} (α := G) ((m : (a : Set α) → G) s : G) ((m : (a : Set α) → G) t : G)
have refine_3 : ∀ (s_1 : Set α), Membership.mem (γ := Finset (Set α)) {s} s_1 → s_1 ⊆ t
Tactic: have h := sum_addContent_le_of_subset (m := m) hC (I := {s}) ?_ ?_ ht ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
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
have simp : ∀ (i : Set α) (i_1 : i ∈ J), (↑(hC.disjointOfUnion (C := C) h_ss i) : Set (Set α)) ⊆ C
Tactic: simp only [disjiUnion_eq_biUnion, coe_biUnion, mem_coe, iUnion_subset_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (hypothesis)
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
⊢ LE.le.{u_2} (α := G) ((m : (a : Set α) → G) (⋃₀ (↑J : Set (Set α))) : G) (∑ u ∈ J, (m : (a : Set α) → G) u : G)
have h1 : (↑(J.disjiUnion (hC.disjointOfUnion (C := C) h_ss) sorry) : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
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
have simp : PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(hC.disjointOfUnion (C := C) h_ss x) : Set (Set α))) id
Tactic: simp only [disjiUnion_eq_biUnion, coe_biUnion, mem_coe]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (hypothesis)
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
⊢ LE.le.{u_2} (α := G) ((m : (a : Set α) → G) (⋃₀ (↑J : Set (Set α))) : G) (∑ u ∈ J, (m : (a : Set α) → G) u : G)
have h2 : (↑(J.disjiUnion (hC.disjointOfUnion (C := C) h_ss) sorry) : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
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 α))
have simp : ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(hC.disjointOfUnion (C := C) h_ss x) : Set (Set α))
Tactic: simp only [disjiUnion_eq_biUnion, coe_biUnion, mem_coe]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (hypothesis)
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
⊢ LE.le.{u_2} (α := G) ((m : (a : Set α) → G) (⋃₀ (↑J : Set (Set α))) : G) (∑ u ∈ J, (m : (a : Set α) → G) u : G)
have h3 : ⋃₀ (↑J : Set (Set α)) = ⋃₀ (↑(J.disjiUnion (hC.disjointOfUnion (C := C) h_ss) sorry) : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
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 α))
⊢ LE.le.{u_2} (α := G) ((m : (a : Set α) → G) (⋃₀ (↑J : Set (Set α))) : G) (∑ u ∈ J, (m : (a : Set α) → G) u : G)
have 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)
Tactic: rw [h3, addContent_sUnion h1 h2, sum_disjiUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
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)
⊢ LE.le.{u_2} (α := G) ((m : (a : Set α) → G) (⋃₀ (↑J : Set (Set α))) : G) (∑ u ∈ J, (m : (a : Set α) → G) u : G)
have rw₁ : ⋃₀ (↑(J.disjiUnion (hC.disjointOfUnion (C := C) h_ss) sorry) : Set (Set α)) ∈ C
Tactic: rw [h3, addContent_sUnion h1 h2, sum_disjiUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
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 α))
⊢ 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)
have 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)
Tactic: gcongr with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
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 α))
⊢ ⋃₀ (↑(J.disjiUnion (hC.disjointOfUnion (C := C) h_ss) ⋯) : Set (Set α)) ∈ C
have 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
Tactic: simp only [disjiUnion_eq_biUnion, coe_biUnion, mem_coe] at *
Cleared hypotheses: h1, h2, h3