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 α
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
conv_lhs :
  (m : (a : Set α) → G) t =
    HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) s : G)
      (∑ i ∈ hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs, (m : (a : Set α) → G) i : G)
conv_lhs₁ conv_lhs₂ :
  (m : (a : Set α) → G) (⋃₀ insert s (↑(hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs) : Set (Set α))) =
    HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) s : G)
      (∑ i ∈ hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs, (m : (a : Set α) → G) i : G)
⊢ (m : (a : Set α) → G) t =
    HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) s : G)
      (∑ i ∈ hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs, (m : (a : Set α) → G) i : G)
have conv_lhs₃ : ∑ u ∈ insert s (hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs), (m : (a : Set α) → G) u =
  HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) s : G)
    (∑ i ∈ hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs, (m : (a : Set α) → G) i : G)
Tactic: classical
  conv_lhs => rw [← hC.sUnion_insert_disjointOfDiff ht hs hst]
  rw [← coe_insert, addContent_sUnion]
  · rw [sum_insert]
    exact hC.notMem_disjointOfDiff ht hs
  · rw [coe_insert]
    exact Set.insert_subset hs (hC.subset_disjointOfDiff ht hs)
  · rw [coe_insert]
    exact hC.pairwiseDisjoint_insert_disjointOfDiff ht hs
  · rw [coe_insert]
    rwa [hC.sUnion_insert_disjointOfDiff ht hs hst]
-- 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
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
conv_lhs :
  (m : (a : Set α) → G) t =
    HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) s : G)
      (∑ i ∈ hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs, (m : (a : Set α) → G) i : G)
conv_lhs₁ conv_lhs₂ :
  (m : (a : Set α) → G) (⋃₀ insert s (↑(hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs) : Set (Set α))) =
    HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) s : G)
      (∑ i ∈ hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs, (m : (a : Set α) → G) i : G)
conv_lhs₃ :
  ∑ u ∈ insert s (hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs), (m : (a : Set α) → G) u =
    HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) s : G)
      (∑ i ∈ hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs, (m : (a : Set α) → G) i : G)
⊢ (m : (a : Set α) → G) t =
    HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) s : G)
      (∑ i ∈ hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs, (m : (a : Set α) → G) i : G)
have h_ss : (↑(insert s (hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs)) : Set (Set α)) ⊆ C
Tactic: classical
  conv_lhs => rw [← hC.sUnion_insert_disjointOfDiff ht hs hst]
  rw [← coe_insert, addContent_sUnion]
  · rw [sum_insert]
    exact hC.notMem_disjointOfDiff ht hs
  · rw [coe_insert]
    exact Set.insert_subset hs (hC.subset_disjointOfDiff ht hs)
  · rw [coe_insert]
    exact hC.pairwiseDisjoint_insert_disjointOfDiff ht hs
  · rw [coe_insert]
    rwa [hC.sUnion_insert_disjointOfDiff ht hs hst]
-- 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
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
conv_lhs :
  (m : (a : Set α) → G) t =
    HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) s : G)
      (∑ i ∈ hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs, (m : (a : Set α) → G) i : G)
conv_lhs₁ conv_lhs₂ :
  (m : (a : Set α) → G) (⋃₀ insert s (↑(hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs) : Set (Set α))) =
    HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) s : G)
      (∑ i ∈ hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs, (m : (a : Set α) → G) i : G)
conv_lhs₃ :
  ∑ u ∈ insert s (hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs), (m : (a : Set α) → G) u =
    HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) s : G)
      (∑ i ∈ hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs, (m : (a : Set α) → G) i : G)
h_ss : (↑(insert s (hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs)) : Set (Set α)) ⊆ C
⊢ (m : (a : Set α) → G) t =
    HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) s : G)
      (∑ i ∈ hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs, (m : (a : Set α) → G) i : G)
have h_dis : (↑(insert s (hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs)) : Set (Set α)).PairwiseDisjoint id
Tactic: classical
  conv_lhs => rw [← hC.sUnion_insert_disjointOfDiff ht hs hst]
  rw [← coe_insert, addContent_sUnion]
  · rw [sum_insert]
    exact hC.notMem_disjointOfDiff ht hs
  · rw [coe_insert]
    exact Set.insert_subset hs (hC.subset_disjointOfDiff ht hs)
  · rw [coe_insert]
    exact hC.pairwiseDisjoint_insert_disjointOfDiff ht hs
  · rw [coe_insert]
    rwa [hC.sUnion_insert_disjointOfDiff ht hs hst]
-- 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
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
conv_lhs :
  (m : (a : Set α) → G) t =
    HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) s : G)
      (∑ i ∈ hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs, (m : (a : Set α) → G) i : G)
conv_lhs₁ conv_lhs₂ :
  (m : (a : Set α) → G) (⋃₀ insert s (↑(hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs) : Set (Set α))) =
    HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) s : G)
      (∑ i ∈ hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs, (m : (a : Set α) → G) i : G)
conv_lhs₃ :
  ∑ u ∈ insert s (hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs), (m : (a : Set α) → G) u =
    HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) s : G)
      (∑ i ∈ hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs, (m : (a : Set α) → G) i : G)
h_ss : (↑(insert s (hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs)) : Set (Set α)) ⊆ C
h_dis : (↑(insert s (hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs)) : Set (Set α)).PairwiseDisjoint id
⊢ (m : (a : Set α) → G) t =
    HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) s : G)
      (∑ i ∈ hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs, (m : (a : Set α) → G) i : G)
have h_mem : ⋃₀ (↑(insert s (hC.disjointOfDiff (C := C) (s := t) (t := s) ht hs)) : Set (Set α)) ∈ C
Tactic: classical
  conv_lhs => rw [← hC.sUnion_insert_disjointOfDiff ht hs hst]
  rw [← coe_insert, addContent_sUnion]
  · rw [sum_insert]
    exact hC.notMem_disjointOfDiff ht hs
  · rw [coe_insert]
    exact Set.insert_subset hs (hC.subset_disjointOfDiff ht hs)
  · rw [coe_insert]
    exact hC.pairwiseDisjoint_insert_disjointOfDiff ht hs
  · rw [coe_insert]
    rwa [hC.sUnion_insert_disjointOfDiff ht hs hst]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
J J' : Finset (Set α)
hJ : (↑J : Set (Set α)) ⊆ C
hJdisj : (↑J : Set (Set α)).PairwiseDisjoint id
hJ' : (↑J' : Set (Set α)) ⊆ C
hJ'disj : (↑J' : Set (Set α)).PairwiseDisjoint id
h : ⋃₀ (↑J : Set (Set α)) = ⋃₀ (↑J' : Set (Set α))
⊢ Eq.{u_2 + 1} (α := G) (∑ s ∈ J, (m : (a : Set α) → G) s) (∑ s ∈ J, ∑ t ∈ J', (m : (a : Set α) → G) (s ∩ t))
have apply : ∀ (s : Set α) (hs : s ∈ J),
  Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) s : G) (∑ t ∈ J', (m : (a : Set α) → G) (s ∩ t) : G)
Tactic: apply Finset.sum_congr rfl (fun s hs ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
J J' : Finset (Set α)
hJ : (↑J : Set (Set α)) ⊆ C
hJdisj : (↑J : Set (Set α)).PairwiseDisjoint id
hJ' : (↑J' : Set (Set α)) ⊆ C
hJ'disj : (↑J' : Set (Set α)).PairwiseDisjoint id
h : ⋃₀ (↑J : Set (Set α)) = ⋃₀ (↑J' : Set (Set α))
s : Set α
hs : s ∈ J
⊢ s = ⋃ t ∈ J', s ∩ t
have simp_rw : s ⊆ ⋃₀ (↑J : Set (Set α))
Tactic: simp_rw [← Finset.set_biUnion_coe, ← inter_iUnion, left_eq_inter, ← sUnion_eq_biUnion, ← h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (hypothesis)
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
J J' : Finset (Set α)
hJ : (↑J : Set (Set α)) ⊆ C
hJdisj : (↑J : Set (Set α)).PairwiseDisjoint id
hJ' : (↑J' : Set (Set α)) ⊆ C
hJ'disj : (↑J' : Set (Set α)).PairwiseDisjoint id
h : ⋃₀ (↑J : Set (Set α)) = ⋃₀ (↑J' : Set (Set α))
s : Set α
hs : s ∈ J
⊢ Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) s : G) (∑ t ∈ J', (m : (a : Set α) → G) (s ∩ t) : G)
have this : s = ⋃ t ∈ J', s ∩ t
Tactic: have : s = ⋃ t ∈ J', s ∩ t := by
      simp_rw [← Finset.set_biUnion_coe, ← inter_iUnion, left_eq_inter, ← sUnion_eq_biUnion, ← h]
      exact subset_sUnion_of_mem hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
J J' : Finset (Set α)
hJ : (↑J : Set (Set α)) ⊆ C
hJdisj : (↑J : Set (Set α)).PairwiseDisjoint id
hJ' : (↑J' : Set (Set α)) ⊆ C
hJ'disj : (↑J' : Set (Set α)).PairwiseDisjoint id
h : ⋃₀ (↑J : Set (Set α)) = ⋃₀ (↑J' : Set (Set α))
s : Set α
hs : s ∈ J
this : s = ⋃ t ∈ J', s ∩ t
⊢ Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) s : G) (∑ t ∈ J', (m : (a : Set α) → G) (s ∩ t) : G)
have nth_rewrite : Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (⋃ t ∈ J', s ∩ t) : G) (∑ t ∈ J', (m : (a : Set α) → G) (s ∩ t) : G)
Tactic: nth_rewrite 1 [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
J J' : Finset (Set α)
hJ : (↑J : Set (Set α)) ⊆ C
hJdisj : (↑J : Set (Set α)).PairwiseDisjoint id
hJ' : (↑J' : Set (Set α)) ⊆ C
hJ'disj : (↑J' : Set (Set α)).PairwiseDisjoint id
h : ⋃₀ (↑J : Set (Set α)) = ⋃₀ (↑J' : Set (Set α))
s : Set α
hs : s ∈ J
this : s = ⋃ t ∈ J', s ∩ t
⊢ Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (⋃ t ∈ J', s ∩ t) : G) (∑ t ∈ J', (m : (a : Set α) → G) (s ∩ t) : G)
have hf : ∀ i ∈ J', s ∩ i ∈ C
Tactic: apply addContent_biUnion
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
J J' : Finset (Set α)
hJ : (↑J : Set (Set α)) ⊆ C
hJdisj : (↑J : Set (Set α)).PairwiseDisjoint id
hJ' : (↑J' : Set (Set α)) ⊆ C
hJ'disj : (↑J' : Set (Set α)).PairwiseDisjoint id
h : ⋃₀ (↑J : Set (Set α)) = ⋃₀ (↑J' : Set (Set α))
s : Set α
hs : s ∈ J
this : s = ⋃ t ∈ J', s ∩ t
hf : ∀ i ∈ J', s ∩ i ∈ C
⊢ Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (⋃ t ∈ J', s ∩ t) : G) (∑ t ∈ J', (m : (a : Set α) → G) (s ∩ t) : G)
have h_dis : (↑J' : Set (Set α)).PairwiseDisjoint (Inter.inter s)
Tactic: apply addContent_biUnion
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
J J' : Finset (Set α)
hJ : (↑J : Set (Set α)) ⊆ C
hJdisj : (↑J : Set (Set α)).PairwiseDisjoint id
hJ' : (↑J' : Set (Set α)) ⊆ C
hJ'disj : (↑J' : Set (Set α)).PairwiseDisjoint id
h : ⋃₀ (↑J : Set (Set α)) = ⋃₀ (↑J' : Set (Set α))
s : Set α
hs : s ∈ J
this : s = ⋃ t ∈ J', s ∩ t
hf : ∀ i ∈ J', s ∩ i ∈ C
h_dis : (↑J' : Set (Set α)).PairwiseDisjoint (Inter.inter s)
⊢ Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (⋃ t ∈ J', s ∩ t) : G) (∑ t ∈ J', (m : (a : Set α) → G) (s ∩ t) : G)
have h_mem : ⋃ i ∈ J', s ∩ i ∈ C
Tactic: apply addContent_biUnion
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
J J' : Finset (Set α)
hJ : (↑J : Set (Set α)) ⊆ C
hJdisj : (↑J : Set (Set α)).PairwiseDisjoint id
hJ' : (↑J' : Set (Set α)) ⊆ C
hJ'disj : (↑J' : Set (Set α)).PairwiseDisjoint id
h : ⋃₀ (↑J : Set (Set α)) = ⋃₀ (↑J' : Set (Set α))
s : Set α
hs : s ∈ J
this : s = ⋃ t ∈ J', s ∩ t
⊢ ⋃ i ∈ J', s ∩ i ∈ C
have h_mem : s ∈ C
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
J J' : Finset (Set α)
hJ : (↑J : Set (Set α)) ⊆ C
hJdisj : (↑J : Set (Set α)).PairwiseDisjoint id
hJ' : (↑J' : Set (Set α)) ⊆ C
hJ'disj : (↑J' : Set (Set α)).PairwiseDisjoint id
h : ⋃₀ (↑J : Set (Set α)) = ⋃₀ (↑J' : Set (Set α))
⊢ Eq.{u_2 + 1} (α := G) (∑ t ∈ J', ∑ s ∈ J, (m : (a : Set α) → G) (s ∩ t)) (∑ t ∈ J', (m : (a : Set α) → G) t)
have apply : ∀ (t : Set α) (ht : t ∈ J'),
  Eq.{u_2 + 1} (α := G) (∑ s ∈ J, (m : (a : Set α) → G) (s ∩ t) : G) ((m : (a : Set α) → G) t : G)
Tactic: apply Finset.sum_congr rfl (fun t 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
m : AddContent G C
hC : IsSetSemiring C
J J' : Finset (Set α)
hJ : (↑J : Set (Set α)) ⊆ C
hJdisj : (↑J : Set (Set α)).PairwiseDisjoint id
hJ' : (↑J' : Set (Set α)) ⊆ C
hJ'disj : (↑J' : Set (Set α)).PairwiseDisjoint id
h : ⋃₀ (↑J : Set (Set α)) = ⋃₀ (↑J' : Set (Set α))
t : Set α
ht : t ∈ J'
⊢ t = ⋃ s ∈ J, s ∩ t
have simp_rw : t ⊆ ⋃₀ (↑J' : Set (Set α))
Tactic: simp_rw [← Finset.set_biUnion_coe, ← iUnion_inter, right_eq_inter, ← sUnion_eq_biUnion, h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (hypothesis)
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
J J' : Finset (Set α)
hJ : (↑J : Set (Set α)) ⊆ C
hJdisj : (↑J : Set (Set α)).PairwiseDisjoint id
hJ' : (↑J' : Set (Set α)) ⊆ C
hJ'disj : (↑J' : Set (Set α)).PairwiseDisjoint id
h : ⋃₀ (↑J : Set (Set α)) = ⋃₀ (↑J' : Set (Set α))
t : Set α
ht : t ∈ J'
⊢ Eq.{u_2 + 1} (α := G) (∑ s ∈ J, (m : (a : Set α) → G) (s ∩ t) : G) ((m : (a : Set α) → G) t : G)
have this : t = ⋃ s ∈ J, s ∩ t
Tactic: have : t = ⋃ s ∈ J, s ∩ t := by
      simp_rw [← Finset.set_biUnion_coe, ← iUnion_inter, right_eq_inter, ← sUnion_eq_biUnion, h]
      exact subset_sUnion_of_mem ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
J J' : Finset (Set α)
hJ : (↑J : Set (Set α)) ⊆ C
hJdisj : (↑J : Set (Set α)).PairwiseDisjoint id
hJ' : (↑J' : Set (Set α)) ⊆ C
hJ'disj : (↑J' : Set (Set α)).PairwiseDisjoint id
h : ⋃₀ (↑J : Set (Set α)) = ⋃₀ (↑J' : Set (Set α))
t : Set α
ht : t ∈ J'
this : t = ⋃ s ∈ J, s ∩ t
⊢ Eq.{u_2 + 1} (α := G) (∑ s ∈ J, (m : (a : Set α) → G) (s ∩ t) : G) ((m : (a : Set α) → G) t : G)
have nth_rewrite : Eq.{u_2 + 1} (α := G) (∑ s ∈ J, (m : (a : Set α) → G) (s ∩ t) : G) ((m : (a : Set α) → G) (⋃ s ∈ J, s ∩ t) : G)
Tactic: nth_rewrite 2 [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
J J' : Finset (Set α)
hJ : (↑J : Set (Set α)) ⊆ C
hJdisj : (↑J : Set (Set α)).PairwiseDisjoint id
hJ' : (↑J' : Set (Set α)) ⊆ C
hJ'disj : (↑J' : Set (Set α)).PairwiseDisjoint id
h : ⋃₀ (↑J : Set (Set α)) = ⋃₀ (↑J' : Set (Set α))
t : Set α
ht : t ∈ J'
this : t = ⋃ s ∈ J, s ∩ t
⊢ Eq.{u_2 + 1} (α := G) (∑ s ∈ J, (m : (a : Set α) → G) (s ∩ t) : G) ((m : (a : Set α) → G) (⋃ s ∈ J, s ∩ t) : G)
have apply : ∀ i ∈ J, i ∩ t ∈ C
Tactic: apply (addContent_biUnion _ _ _).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
J J' : Finset (Set α)
hJ : (↑J : Set (Set α)) ⊆ C
hJdisj : (↑J : Set (Set α)).PairwiseDisjoint id
hJ' : (↑J' : Set (Set α)) ⊆ C
hJ'disj : (↑J' : Set (Set α)).PairwiseDisjoint id
h : ⋃₀ (↑J : Set (Set α)) = ⋃₀ (↑J' : Set (Set α))
t : Set α
ht : t ∈ J'
this : t = ⋃ s ∈ J, s ∩ t
apply : ∀ i ∈ J, i ∩ t ∈ C
⊢ Eq.{u_2 + 1} (α := G) (∑ s ∈ J, (m : (a : Set α) → G) (s ∩ t) : G) ((m : (a : Set α) → G) (⋃ s ∈ J, s ∩ t) : G)
have apply₁ : (↑J : Set (Set α)).PairwiseDisjoint (α := Set α) fun (i : Set α) ↦ i ∩ t
Tactic: apply (addContent_biUnion _ _ _).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
J J' : Finset (Set α)
hJ : (↑J : Set (Set α)) ⊆ C
hJdisj : (↑J : Set (Set α)).PairwiseDisjoint id
hJ' : (↑J' : Set (Set α)) ⊆ C
hJ'disj : (↑J' : Set (Set α)).PairwiseDisjoint id
h : ⋃₀ (↑J : Set (Set α)) = ⋃₀ (↑J' : Set (Set α))
t : Set α
ht : t ∈ J'
this : t = ⋃ s ∈ J, s ∩ t
apply : ∀ i ∈ J, i ∩ t ∈ C
apply₁ : (↑J : Set (Set α)).PairwiseDisjoint (α := Set α) fun (i : Set α) ↦ i ∩ t
⊢ Eq.{u_2 + 1} (α := G) (∑ s ∈ J, (m : (a : Set α) → G) (s ∩ t) : G) ((m : (a : Set α) → G) (⋃ s ∈ J, s ∩ t) : G)
have apply₂ : ⋃ i ∈ J, i ∩ t ∈ C
Tactic: apply (addContent_biUnion _ _ _).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
J J' : Finset (Set α)
hJ : (↑J : Set (Set α)) ⊆ C
hJdisj : (↑J : Set (Set α)).PairwiseDisjoint id
hJ' : (↑J' : Set (Set α)) ⊆ C
hJ'disj : (↑J' : Set (Set α)).PairwiseDisjoint id
h : ⋃₀ (↑J : Set (Set α)) = ⋃₀ (↑J' : Set (Set α))
t : Set α
ht : t ∈ J'
this : t = ⋃ s ∈ J, s ∩ t
⊢ ⋃ i ∈ J, i ∩ t ∈ C
have rw : t ∈ C
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
J J' : Finset (Set α)
hJ : (↑J : Set (Set α)) ⊆ C
hJdisj : (↑J : Set (Set α)).PairwiseDisjoint id
hJ' : (↑J' : Set (Set α)) ⊆ C
hJ'disj : (↑J' : Set (Set α)).PairwiseDisjoint id
h : ⋃₀ (↑J : Set (Set α)) = ⋃₀ (↑J' : Set (Set α))
⊢ Eq.{u_2 + 1} (α := G) (∑ s ∈ J, (m : (a : Set α) → G) s) (∑ t ∈ J', (m : (a : Set α) → G) t)
have calc : Eq.{u_2 + 1} (α := G) (∑ s ∈ J, (m : (a : Set α) → G) s) (∑ s ∈ J, ∑ t ∈ J', (m : (a : Set α) → G) (s ∩ t))
Tactic: calc ∑ s ∈ J, m s
  _ = ∑ s ∈ J, (∑ t ∈ J', m (s ∩ t)) := by
    apply Finset.sum_congr rfl (fun s hs ↦ ?_)
    have : s = ⋃ t ∈ J', s ∩ t := by
      simp_rw [← Finset.set_biUnion_coe, ← inter_iUnion, left_eq_inter, ← sUnion_eq_biUnion, ← h]
      exact subset_sUnion_of_mem hs
    nth_rewrite 1 [this]
    apply addContent_biUnion
    · exact fun t ht ↦ hC.inter_mem _ (hJ hs) _ (hJ' ht)
    · exact hJ'disj.mono fun _ ↦ by simp
    · rw [← this]
      exact hJ hs
  _ = ∑ t ∈ J', (∑ s ∈ J, m (s ∩ t)) := sum_comm
  _ = ∑ t ∈ J', m t := by
    apply Finset.sum_congr rfl (fun t ht ↦ ?_)
    have : t = ⋃ s ∈ J, s ∩ t := by
      simp_rw [← Finset.set_biUnion_coe, ← iUnion_inter, right_eq_inter, ← sUnion_eq_biUnion, h]
      exact subset_sUnion_of_mem ht
    nth_rewrite 2 [this]
    apply (addContent_biUnion _ _ _).symm
    · exact fun s hs ↦ hC.inter_mem _ (hJ hs) _ (hJ' ht)
    · exact hJdisj.mono fun _ ↦ by simp
    · rw [← this]
      exact hJ' ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
J J' : Finset (Set α)
hJ : (↑J : Set (Set α)) ⊆ C
hJdisj : (↑J : Set (Set α)).PairwiseDisjoint id
hJ' : (↑J' : Set (Set α)) ⊆ C
hJ'disj : (↑J' : Set (Set α)).PairwiseDisjoint id
h : ⋃₀ (↑J : Set (Set α)) = ⋃₀ (↑J' : Set (Set α))
calc : Eq.{u_2 + 1} (α := G) (∑ s ∈ J, (m : (a : Set α) → G) s) (∑ s ∈ J, ∑ t ∈ J', (m : (a : Set α) → G) (s ∩ t))
⊢ Eq.{u_2 + 1} (α := G) (∑ s ∈ J, (m : (a : Set α) → G) s) (∑ t ∈ J', (m : (a : Set α) → G) t)
have calc₁ : Eq.{u_2 + 1} (α := G) (∑ t ∈ J', ∑ s ∈ J, (m : (a : Set α) → G) (s ∩ t)) (∑ t ∈ J', (m : (a : Set α) → G) t)
Tactic: calc ∑ s ∈ J, m s
  _ = ∑ s ∈ J, (∑ t ∈ J', m (s ∩ t)) := by
    apply Finset.sum_congr rfl (fun s hs ↦ ?_)
    have : s = ⋃ t ∈ J', s ∩ t := by
      simp_rw [← Finset.set_biUnion_coe, ← inter_iUnion, left_eq_inter, ← sUnion_eq_biUnion, ← h]
      exact subset_sUnion_of_mem hs
    nth_rewrite 1 [this]
    apply addContent_biUnion
    · exact fun t ht ↦ hC.inter_mem _ (hJ hs) _ (hJ' ht)
    · exact hJ'disj.mono fun _ ↦ by simp
    · rw [← this]
      exact hJ hs
  _ = ∑ t ∈ J', (∑ s ∈ J, m (s ∩ t)) := sum_comm
  _ = ∑ t ∈ J', m t := by
    apply Finset.sum_congr rfl (fun t ht ↦ ?_)
    have : t = ⋃ s ∈ J, s ∩ t := by
      simp_rw [← Finset.set_biUnion_coe, ← iUnion_inter, right_eq_inter, ← sUnion_eq_biUnion, h]
      exact subset_sUnion_of_mem ht
    nth_rewrite 2 [this]
    apply (addContent_biUnion _ _ _).symm
    · exact fun s hs ↦ hC.inter_mem _ (hJ hs) _ (hJ' ht)
    · exact hJdisj.mono fun _ ↦ by simp
    · rw [← this]
      exact hJ' ht
-- 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 α
J : Finset (Set α)
hJ : (↑J : Set (Set α)) ⊆ C
h'J : (↑J : Set (Set α)).PairwiseDisjoint id
hs : s = ⋃₀ (↑J : Set (Set α))
⊢ m.supClosureFun (C := C) s = ∑ s ∈ J, (m : (a : Set α) → G) s
have h : ∃ (J : Finset (Set α)), (↑J : Set (Set α)) ⊆ C ∧ (↑J : Set (Set α)).PairwiseDisjoint id ∧ s = ⋃₀ (↑J : Set (Set α))
Tactic: have h : ∃ (J : Finset (Set α)), ↑J ⊆ C ∧ (PairwiseDisjoint (J : Set (Set α)) id) ∧ s = ⋃₀ ↑J :=
    ⟨J, hJ, h'J, hs⟩
-- 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 : Finset (Set α)
hJ : (↑J : Set (Set α)) ⊆ C
h'J : (↑J : Set (Set α)).PairwiseDisjoint id
hs : s = ⋃₀ (↑J : Set (Set α))
h : ∃ (J : Finset (Set α)), (↑J : Set (Set α)) ⊆ C ∧ (↑J : Set (Set α)).PairwiseDisjoint id ∧ s = ⋃₀ (↑J : Set (Set α))
⊢ m.supClosureFun (C := C) s = ∑ s ∈ J, (m : (a : Set α) → G) s
have simp : Eq.{u_2 + 1} (α := G)
  (∑
    s ∈
      sorry.choose (p := fun (J : Finset (Set α)) ↦
        (↑J : Set (Set α)) ⊆ C ∧ (↑J : Set (Set α)).PairwiseDisjoint id ∧ s = ⋃₀ (↑J : Set (Set α))),
    (m : (a : Set α) → G) s)
  (∑ s ∈ J, (m : (a : Set α) → G) s)
Tactic: simp only [supClosureFun, h, ↓reduceDIte]
-- 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 : Finset (Set α)
hJ : (↑J : Set (Set α)) ⊆ C
h'J : (↑J : Set (Set α)).PairwiseDisjoint id
hs : s = ⋃₀ (↑J : Set (Set α))
h : ∃ (J : Finset (Set α)), (↑J : Set (Set α)) ⊆ C ∧ (↑J : Set (Set α)).PairwiseDisjoint id ∧ s = ⋃₀ (↑J : Set (Set α))
⊢ Eq.{u_2 + 1} (α := G)
    (∑
      s ∈
        ⋯.choose (p := fun (J : Finset (Set α)) ↦
          (↑J : Set (Set α)) ⊆ C ∧ (↑J : Set (Set α)).PairwiseDisjoint id ∧ s = ⋃₀ (↑J : Set (Set α))),
      (m : (a : Set α) → G) s)
    (∑ s ∈ J, (m : (a : Set α) → G) s)
have apply : ⋃₀
    (↑(h.choose (p := fun (J : Finset (Set α)) ↦
          (↑J : Set (Set α)) ⊆ C ∧ (↑J : Set (Set α)).PairwiseDisjoint id ∧ s = ⋃₀ (↑J : Set (Set α)))) :
      Set (Set α)) =
  ⋃₀ (↑J : Set (Set α))
Tactic: apply sum_addContent_eq_of_sUnion_eq hC _ _ h.choose_spec.1 h.choose_spec.2.1 hJ h'J
-- 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 : Finset (Set α)
hJ : (↑J : Set (Set α)) ⊆ C
h'J : (↑J : Set (Set α)).PairwiseDisjoint id
hs : s = ⋃₀ (↑J : Set (Set α))
h : ∃ (J : Finset (Set α)), (↑J : Set (Set α)) ⊆ C ∧ (↑J : Set (Set α)).PairwiseDisjoint id ∧ s = ⋃₀ (↑J : Set (Set α))
⊢ ⋃₀
      (↑(h.choose (p := fun (J : Finset (Set α)) ↦
            (↑J : Set (Set α)) ⊆ C ∧ (↑J : Set (Set α)).PairwiseDisjoint id ∧ s = ⋃₀ (↑J : Set (Set α)))) :
        Set (Set α)) =
    ⋃₀ (↑J : Set (Set α))
have rw : ⋃₀
    (↑(h.choose (p := fun (J : Finset (Set α)) ↦
          (↑J : Set (Set α)) ⊆ C ∧ (↑J : Set (Set α)).PairwiseDisjoint id ∧ s = ⋃₀ (↑J : Set (Set α)))) :
      Set (Set α)) =
  s
Tactic: rw [← hs]