awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (hypothesis)
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 = (m : (a : Set α) → G) s
have this : 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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
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
⊢ m.supClosureFun (C := C) ∅ = 0
have rw : Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) ∅ : G) (0 : G)
Tactic: rw [m.supClosureFun_apply_of_mem hC hC.empty_mem, addContent_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
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)
⊢ m.supClosureFun (C := C) ∅ = 0
have rw₁ : Eq.{u_2 + 1} (α := G) 0 0
Tactic: rw [m.supClosureFun_apply_of_mem hC hC.empty_mem, addContent_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (hypothesis)
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), (↑(P.parts (a := s)) : Set (Set α)) ⊆ C
have this : Membership.mem (γ := Set (Set α)) ((_root_.supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s
Tactic: have := hI hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
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
⊢ ∃ (P : Finpartition s), (↑(P.parts (a := s)) : Set (Set α)) ⊆ C
have rwa : ∀ (this : ∃ (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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
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
⊢ ∃ (J : Finset (Set α)), (↑J : Set (Set α)) ⊆ C ∧ (↑J : Set (Set α)).PairwiseDisjoint id ∧ s = ⋃₀ (↑J : Set (Set α))
have 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 α))
Tactic: obtain ⟨P, PC⟩ : ∃ (P : Finpartition s), ↑P.parts ⊆ C := by
        have := hI hs
        rwa [hC.mem_supClosure_iff] at this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
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
⊢ ∃ (J : Finset (Set α)), (↑J : Set (Set α)) ⊆ C ∧ (↑J : Set (Set α)).PairwiseDisjoint id ∧ s = ⋃₀ (↑J : Set (Set α))
have refine : s = ⋃₀ (↑(P.parts (a := s)) : Set (Set α))
Tactic: refine ⟨P.parts, PC, P.disjoint, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
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
⊢ s = ⋃₀ (↑(P.parts (a := s)) : Set (Set α))
have h : ⋃₀ (↑(P.parts (a := s)) : Set (Set α)) = P.parts (a := s).sup id
Tactic: convert! P.sup_parts.symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (hypothesis)
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 A : ∀ (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]
-- 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 α)))
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 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
Tactic: choose! J hJC hJdisj hJs using A
Cleared hypotheses: A
-- 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 α))
a i : Set α
hi : i ∈ I
ha : a ∈ J i
⊢ a ⊆ i
have rw : a ⊆ ⋃₀ (↑(J i) : Set (Set α))
Tactic: rw [hJs i hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (hypothesis)
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 α))
⊢ m.supClosureFun (C := C) (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, m.supClosureFun (C := C) u
have H : ∀ {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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (hypothesis)
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
⊢ m.supClosureFun (C := C) (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, m.supClosureFun (C := C) u
have this : ⋃₀ (↑I : Set (Set α)) = ⋃₀ (↑K : Set (Set α))
Tactic: have : ⋃₀ ↑I = ⋃₀ (↑K : Set (Set α)) := by grind
-- 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 α))
⊢ m.supClosureFun (C := C) (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, m.supClosureFun (C := C) u
have rw : Eq.{u_2 + 1} (α := G) (∑ s ∈ K, (m : (a : Set α) → G) s) (∑ u ∈ I, m.supClosureFun (C := C) u)
Tactic: rw [this, m.supClosureFun_apply hC (J := K) (by simpa [K] using hJC) _ rfl]
-- 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 α))
rw : Eq.{u_2 + 1} (α := G) (∑ s ∈ K, (m : (a : Set α) → G) s) (∑ u ∈ I, m.supClosureFun (C := C) u)
⊢ m.supClosureFun (C := C) (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, m.supClosureFun (C := C) u
have rw₁ : (↑K : Set (Set α)).PairwiseDisjoint id
Tactic: rw [this, m.supClosureFun_apply hC (J := K) (by simpa [K] using hJC) _ rfl]
-- 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 α))
⊢ (↑K : Set (Set α)).PairwiseDisjoint id
have simp : PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ (↑I : Set (Set α)), (↑(J x) : Set (Set α))) id
Tactic: simp only [K, coe_biUnion]
-- 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 α))
⊢ PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ (↑I : Set (Set α)), (↑(J x) : Set (Set α))) id
have refine : ∀ ⦃i : Set α⦄, i ∈ (↑I : Set (Set α)) → ⨆ i_1 ∈ (↑(J i) : Set (Set α)), id i_1 ≤ id i
Tactic: refine (h'I.mono_on ?_).biUnion hJdisj
-- 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 α))
⊢ ∀ ⦃i : Set α⦄, i ∈ (↑I : Set (Set α)) → ⨆ i_1 ∈ (↑(J i) : Set (Set α)), id i_1 ≤ id i
have simp : ∀ ⦃i : Set α⦄, i ∈ I → ∀ (i_1 : Set α) (i_2 : i_1 ∈ J i), i_1 ⊆ i
Tactic: simp
-- 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) (∑ s ∈ I.biUnion J, (m : (a : Set α) → G) s) (∑ u ∈ I, m.supClosureFun (C := C) u)
have rw : Eq.{u_2 + 1} (α := G) (∑ x ∈ I, ∑ i ∈ J x, (m : (a : Set α) → G) i) (∑ u ∈ I, m.supClosureFun (C := C) u)
Tactic: rw [sum_biUnion_of_pairwise_eq_zero]
-- 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 α))
rw : Eq.{u_2 + 1} (α := G) (∑ x ∈ I, ∑ i ∈ J x, (m : (a : Set α) → G) i) (∑ u ∈ I, m.supClosureFun (C := C) u)
⊢ Eq.{u_2 + 1} (α := G) (∑ s ∈ I.biUnion J, (m : (a : Set α) → G) s) (∑ u ∈ I, m.supClosureFun (C := C) u)
have 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)
Tactic: rw [sum_biUnion_of_pairwise_eq_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (hypothesis)
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
⊢ Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) k : G) (0 : G)
have hk₁ : k ∈ J i ∧ k ∈ J j
Tactic: simp only [Finset.mem_inter] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (hypothesis)
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
have this₁ : Disjoint i j
Tactic: have : Disjoint i j := h'I hi hj hij
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (hypothesis)
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
⊢ Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) k : G) (0 : G)
have this₁ : 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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (hypothesis)
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
⊢ Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) k : G) (0 : G)
have this₁ : k = ∅
Tactic: simp only [disjoint_self, Set.bot_eq_empty] at this
Cleared hypotheses: this