awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
ι : Type u_3
a : Finset ι
f : ι → Set α
hf : ∀ i ∈ a, f i ∈ C
h_dis : (↑a : Set ι).PairwiseDisjoint f
h_mem : ⋃ i ∈ a, f i ∈ C
A : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))
rw : Eq.{u_2 + 1} (α := G) (∑ u ∈ Finset.image f a, (m : (a : Set α) → G) u) (∑ i ∈ a, (m : (a : Set α) → G) (f i))
h_ss : (↑(Finset.image f a) : Set (Set α)) ⊆ C
h_dis₁ : (↑(Finset.image f a) : Set (Set α)).PairwiseDisjoint id
⊢ Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (⋃ i ∈ a, f i) : G) (∑ i ∈ a, (m : (a : Set α) → G) (f i) : G)
have h_mem₁ : ⋃₀ (↑(Finset.image f a) : Set (Set α)) ∈ C
Tactic: rw [A, addContent_sUnion]
-- 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
ι : Type u_3
a : Finset ι
f : ι → Set α
hf : ∀ i ∈ a, f i ∈ C
h_dis : (↑a : Set ι).PairwiseDisjoint f
h_mem : ⋃ i ∈ a, f i ∈ C
A : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))
⊢ Eq.{u_2 + 1} (α := G) (∑ u ∈ Finset.image f a, (m : (a : Set α) → G) u) (∑ i ∈ a, (m : (a : Set α) → G) (f i))
have rw : (↑a : Set ι).Pairwise fun (i j : ι) ↦ f i = f j → Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (f i) : G) (0 : G)
Tactic: rw [sum_image_of_pairwise_eq_zero]
-- 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
ι : Type u_3
a : Finset ι
f : ι → Set α
hf : ∀ i ∈ a, f i ∈ C
h_dis : (↑a : Set ι).PairwiseDisjoint f
h_mem : ⋃ i ∈ a, f i ∈ C
A : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))
⊢ (↑a : Set ι).Pairwise fun (i j : ι) ↦ f i = f j → Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (f i) : G) (0 : G)
have refine : ∀ ⦃a b : ι⦄, (Disjoint on f) a b → f a = f b → Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (f a) : G) (0 : G)
Tactic: refine h_dis.imp ?_
-- 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
ι : Type u_3
a : Finset ι
f : ι → Set α
hf : ∀ i ∈ a, f i ∈ C
h_dis : (↑a : Set ι).PairwiseDisjoint f
h_mem : ⋃ i ∈ a, f i ∈ C
⊢ Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (⋃ i ∈ a, f i) : G) (∑ i ∈ a, (m : (a : Set α) → G) (f i) : G)
have have : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))
Tactic: classical
  have A : ⋃ i ∈ a, f i = ⋃₀ (a.image f) := by simp
  rw [A, addContent_sUnion]; rotate_left
  · grind
  · simpa using h_dis.image
  · rwa [← A]
  rw [sum_image_of_pairwise_eq_zero]
  refine h_dis.imp ?_
  grind [Set.bot_eq_empty (α := α), addContent_empty]
-- 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
ι : Type u_3
a : Finset ι
f : ι → Set α
hf : ∀ i ∈ a, f i ∈ C
h_dis : (↑a : Set ι).PairwiseDisjoint f
h_mem : ⋃ i ∈ a, f i ∈ C
have : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))
⊢ Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (⋃ i ∈ a, f i) : G) (∑ i ∈ a, (m : (a : Set α) → G) (f i) : G)
have have₁ : ∀ (A : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))),
  Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (⋃ i ∈ a, f i) : G) (∑ i ∈ a, (m : (a : Set α) → G) (f i) : G)
Tactic: classical
  have A : ⋃ i ∈ a, f i = ⋃₀ (a.image f) := by simp
  rw [A, addContent_sUnion]; rotate_left
  · grind
  · simpa using h_dis.image
  · rwa [← A]
  rw [sum_image_of_pairwise_eq_zero]
  refine h_dis.imp ?_
  grind [Set.bot_eq_empty (α := α), addContent_empty]
-- 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
ι : Type u_3
a : Finset ι
f : ι → Set α
hf : ∀ i ∈ a, f i ∈ C
h_dis : (↑a : Set ι).PairwiseDisjoint f
h_mem : ⋃ i ∈ a, f i ∈ C
have : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))
have₁ :
  ∀ (A : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))),
    Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (⋃ i ∈ a, f i) : G) (∑ i ∈ a, (m : (a : Set α) → G) (f i) : G)
have₂ : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))
have₃ have₄ :
  ∀ (A : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))),
    Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (⋃ i ∈ a, f i) : G) (∑ i ∈ a, (m : (a : Set α) → G) (f i) : G)
⊢ Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (⋃ i ∈ a, f i) : G) (∑ i ∈ a, (m : (a : Set α) → G) (f i) : G)
have have₅ : ∀ (A : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))),
  Eq.{u_2 + 1} (α := G) (∑ u ∈ Finset.image f a, (m : (a : Set α) → G) u) (∑ i ∈ a, (m : (a : Set α) → G) (f i))
Tactic: classical
  have A : ⋃ i ∈ a, f i = ⋃₀ (a.image f) := by simp
  rw [A, addContent_sUnion]; rotate_left
  · grind
  · simpa using h_dis.image
  · rwa [← A]
  rw [sum_image_of_pairwise_eq_zero]
  refine h_dis.imp ?_
  grind [Set.bot_eq_empty (α := α), addContent_empty]
-- 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
ι : Type u_3
a : Finset ι
f : ι → Set α
hf : ∀ i ∈ a, f i ∈ C
h_dis : (↑a : Set ι).PairwiseDisjoint f
h_mem : ⋃ i ∈ a, f i ∈ C
have : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))
have₁ :
  ∀ (A : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))),
    Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (⋃ i ∈ a, f i) : G) (∑ i ∈ a, (m : (a : Set α) → G) (f i) : G)
have₂ : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))
have₃ have₄ :
  ∀ (A : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))),
    Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (⋃ i ∈ a, f i) : G) (∑ i ∈ a, (m : (a : Set α) → G) (f i) : G)
have₅ :
  ∀ (A : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))),
    Eq.{u_2 + 1} (α := G) (∑ u ∈ Finset.image f a, (m : (a : Set α) → G) u) (∑ i ∈ a, (m : (a : Set α) → G) (f i))
⊢ Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (⋃ i ∈ a, f i) : G) (∑ i ∈ a, (m : (a : Set α) → G) (f i) : G)
have h_ss : ∀ (A : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))), (↑(Finset.image f a) : Set (Set α)) ⊆ C
Tactic: classical
  have A : ⋃ i ∈ a, f i = ⋃₀ (a.image f) := by simp
  rw [A, addContent_sUnion]; rotate_left
  · grind
  · simpa using h_dis.image
  · rwa [← A]
  rw [sum_image_of_pairwise_eq_zero]
  refine h_dis.imp ?_
  grind [Set.bot_eq_empty (α := α), addContent_empty]
-- 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
ι : Type u_3
a : Finset ι
f : ι → Set α
hf : ∀ i ∈ a, f i ∈ C
h_dis : (↑a : Set ι).PairwiseDisjoint f
h_mem : ⋃ i ∈ a, f i ∈ C
have : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))
have₁ :
  ∀ (A : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))),
    Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (⋃ i ∈ a, f i) : G) (∑ i ∈ a, (m : (a : Set α) → G) (f i) : G)
have₂ : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))
have₃ have₄ :
  ∀ (A : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))),
    Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (⋃ i ∈ a, f i) : G) (∑ i ∈ a, (m : (a : Set α) → G) (f i) : G)
have₅ :
  ∀ (A : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))),
    Eq.{u_2 + 1} (α := G) (∑ u ∈ Finset.image f a, (m : (a : Set α) → G) u) (∑ i ∈ a, (m : (a : Set α) → G) (f i))
h_ss : ∀ (A : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))), (↑(Finset.image f a) : Set (Set α)) ⊆ C
⊢ Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (⋃ i ∈ a, f i) : G) (∑ i ∈ a, (m : (a : Set α) → G) (f i) : G)
have h_dis₁ : ∀ (A : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))), (↑(Finset.image f a) : Set (Set α)).PairwiseDisjoint id
Tactic: classical
  have A : ⋃ i ∈ a, f i = ⋃₀ (a.image f) := by simp
  rw [A, addContent_sUnion]; rotate_left
  · grind
  · simpa using h_dis.image
  · rwa [← A]
  rw [sum_image_of_pairwise_eq_zero]
  refine h_dis.imp ?_
  grind [Set.bot_eq_empty (α := α), addContent_empty]
-- 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
ι : Type u_3
a : Finset ι
f : ι → Set α
hf : ∀ i ∈ a, f i ∈ C
h_dis : (↑a : Set ι).PairwiseDisjoint f
h_mem : ⋃ i ∈ a, f i ∈ C
have : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))
have₁ :
  ∀ (A : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))),
    Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (⋃ i ∈ a, f i) : G) (∑ i ∈ a, (m : (a : Set α) → G) (f i) : G)
have₂ : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))
have₃ have₄ :
  ∀ (A : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))),
    Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (⋃ i ∈ a, f i) : G) (∑ i ∈ a, (m : (a : Set α) → G) (f i) : G)
have₅ :
  ∀ (A : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))),
    Eq.{u_2 + 1} (α := G) (∑ u ∈ Finset.image f a, (m : (a : Set α) → G) u) (∑ i ∈ a, (m : (a : Set α) → G) (f i))
h_ss : ∀ (A : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))), (↑(Finset.image f a) : Set (Set α)) ⊆ C
h_dis₁ :
  ∀ (A : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))), (↑(Finset.image f a) : Set (Set α)).PairwiseDisjoint id
⊢ Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (⋃ i ∈ a, f i) : G) (∑ i ∈ a, (m : (a : Set α) → G) (f i) : G)
have h_mem₁ : ∀ (A : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))), ⋃₀ (↑(Finset.image f a) : Set (Set α)) ∈ C
Tactic: classical
  have A : ⋃ i ∈ a, f i = ⋃₀ (a.image f) := by simp
  rw [A, addContent_sUnion]; rotate_left
  · grind
  · simpa using h_dis.image
  · rwa [← A]
  rw [sum_image_of_pairwise_eq_zero]
  refine h_dis.imp ?_
  grind [Set.bot_eq_empty (α := α), addContent_empty]
-- 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
ι : Type u_3
inst_1 : Fintype ι
f : ι → Set α
hf : ∀ (i : ι), f i ∈ C
h_dis : Pairwise (Disjoint on f)
h_mem : ⋃ (i : ι), f i ∈ C
⊢ Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (⋃ (i : ι), f i) : G) (∑ i : ι, (m : (a : Set α) → G) (f i) : G)
have h : Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (⋃ (i : ι), f i) : G)
  ((m : (a : Set α) → G) (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) Finset.univ i), f i) : G)
Tactic: convert! addContent_biUnion (a := Finset.univ) (f := f) (m := m) ?_ ?_ ?_ using 1
-- 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
ι : Type u_3
inst_1 : Fintype ι
f : ι → Set α
hf : ∀ (i : ι), f i ∈ C
h_dis : Pairwise (Disjoint on f)
h_mem : ⋃ (i : ι), f i ∈ C
h :
  Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (⋃ (i : ι), f i) : G)
    ((m : (a : Set α) → G) (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) Finset.univ i), f i) : G)
⊢ Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (⋃ (i : ι), f i) : G) (∑ i : ι, (m : (a : Set α) → G) (f i) : G)
have convert_1 : ∀ (i : ι), Membership.mem (γ := Finset ι) Finset.univ i → f i ∈ C
Tactic: convert! addContent_biUnion (a := Finset.univ) (f := f) (m := m) ?_ ?_ ?_ using 1
-- 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
ι : Type u_3
inst_1 : Fintype ι
f : ι → Set α
hf : ∀ (i : ι), f i ∈ C
h_dis : Pairwise (Disjoint on f)
h_mem : ⋃ (i : ι), f i ∈ C
h :
  Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (⋃ (i : ι), f i) : G)
    ((m : (a : Set α) → G) (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) Finset.univ i), f i) : G)
convert_1 : ∀ (i : ι), Membership.mem (γ := Finset ι) Finset.univ i → f i ∈ C
⊢ Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (⋃ (i : ι), f i) : G) (∑ i : ι, (m : (a : Set α) → G) (f i) : G)
have convert_2 : (↑Finset.univ : Set ι).PairwiseDisjoint f
Tactic: convert! addContent_biUnion (a := Finset.univ) (f := f) (m := m) ?_ ?_ ?_ using 1
-- 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
ι : Type u_3
inst_1 : Fintype ι
f : ι → Set α
hf : ∀ (i : ι), f i ∈ C
h_dis : Pairwise (Disjoint on f)
h_mem : ⋃ (i : ι), f i ∈ C
h :
  Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (⋃ (i : ι), f i) : G)
    ((m : (a : Set α) → G) (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) Finset.univ i), f i) : G)
convert_1 : ∀ (i : ι), Membership.mem (γ := Finset ι) Finset.univ i → f i ∈ C
convert_2 : (↑Finset.univ : Set ι).PairwiseDisjoint f
⊢ Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (⋃ (i : ι), f i) : G) (∑ i : ι, (m : (a : Set α) → G) (f i) : G)
have convert_3 : ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) Finset.univ i), f i ∈ C
Tactic: convert! addContent_biUnion (a := Finset.univ) (f := f) (m := m) ?_ ?_ ?_ using 1
-- 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
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
⊢ s ∪ t = ⋃ (i : Fin (Nat.succ 0).succ), ![s, t] i
have h : ∀ (x : α), x ∈ s ∪ t ↔ Membership.mem (γ := Set α) (⋃ (i : Fin (Nat.succ 0).succ), ![s, t] i) x
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (hypothesis)
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
⊢ (m : (a : Set α) → G) (s ∪ t) =
    HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) s : G) ((m : (a : Set α) → G) t : G)
have A : s ∪ t = ⋃ (i : Fin (Nat.succ 0).succ), ![s, t] i
Tactic: have A : s ∪ t = ⋃ i, ![s, t] i := by ext; simp
-- 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
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ (i : Fin (Nat.succ 0).succ), ![s, t] i
⊢ (m : (a : Set α) → G) (s ∪ t) =
    HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) s : G) ((m : (a : Set α) → G) t : G)
have h : HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) s : G) ((m : (a : Set α) → G) t : G) =
  ∑ i : Fin (Nat.succ 0).succ, (m : (a : Set α) → G) (![s, t] i)
Tactic: convert! addContent_iUnion (f := ![s, t]) (m := m) (fun i ↦ ?_) (fun i j hij ↦ ?_) ?_ using 2
-- 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
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ (i : Fin (Nat.succ 0).succ), ![s, t] i
h :
  HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) s : G) ((m : (a : Set α) → G) t : G) =
    ∑ i : Fin (Nat.succ 0).succ, (m : (a : Set α) → G) (![s, t] i)
⊢ (m : (a : Set α) → G) (s ∪ t) =
    HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) s : G) ((m : (a : Set α) → G) t : G)
have convert_1 : ∀ (i : Fin (Nat.succ 0).succ), ![s, t] i ∈ C
Tactic: convert! addContent_iUnion (f := ![s, t]) (m := m) (fun i ↦ ?_) (fun i j hij ↦ ?_) ?_ using 2
-- 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
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ (i : Fin (Nat.succ 0).succ), ![s, t] i
h :
  HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) s : G) ((m : (a : Set α) → G) t : G) =
    ∑ i : Fin (Nat.succ 0).succ, (m : (a : Set α) → G) (![s, t] i)
convert_1 : ∀ (i : Fin (Nat.succ 0).succ), ![s, t] i ∈ C
⊢ (m : (a : Set α) → G) (s ∪ t) =
    HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) s : G) ((m : (a : Set α) → G) t : G)
have convert_2 : ∀ (i j : Fin (Nat.succ 0).succ) (hij : i ≠ j), (Disjoint on ![s, t]) i j
Tactic: convert! addContent_iUnion (f := ![s, t]) (m := m) (fun i ↦ ?_) (fun i j hij ↦ ?_) ?_ using 2
-- 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
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ (i : Fin (Nat.succ 0).succ), ![s, t] i
h :
  HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) s : G) ((m : (a : Set α) → G) t : G) =
    ∑ i : Fin (Nat.succ 0).succ, (m : (a : Set α) → G) (![s, t] i)
convert_1 : ∀ (i : Fin (Nat.succ 0).succ), ![s, t] i ∈ C
convert_2 : ∀ (i j : Fin (Nat.succ 0).succ) (hij : i ≠ j), (Disjoint on ![s, t]) i j
⊢ (m : (a : Set α) → G) (s ∪ t) =
    HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) s : G) ((m : (a : Set α) → G) t : G)
have convert_3 : ⋃ (i : Fin (Nat.succ 0).succ), ![s, t] i ∈ C
Tactic: convert! addContent_iUnion (f := ![s, t]) (m := m) (fun i ↦ ?_) (fun i j hij ↦ ?_) ?_ using 2
-- 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
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ (i : Fin (Nat.succ 0).succ), ![s, t] i
i : Fin (Nat.succ 0).succ
⊢ ![s, t] i ∈ C
have convert_1 : ![s, t] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, sorry⟩ : Fin (Nat.succ 0).succ)) ∈ C
Tactic: fin_cases i
Cleared hypotheses: i
-- 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
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ (i : Fin (Nat.succ 0).succ), ![s, t] i
i : Fin (Nat.succ 0).succ
convert_1 : ![s, t] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ)) ∈ C
⊢ ![s, t] i ∈ C
have convert_1₁ : ![s, t] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, sorry⟩ : Fin (Nat.succ 0).succ)) ∈ C
Tactic: fin_cases i
Cleared hypotheses: i
-- 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
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ (i : Fin (Nat.succ 0).succ), ![s, t] i
i j : Fin (Nat.succ 0).succ
hij : i ≠ j
⊢ (Disjoint on ![s, t]) i j
have convert_2 : ∀ (hij : (fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, sorry⟩ ≠ j),
  (Disjoint on ![s, t]) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, sorry⟩) j
Tactic: fin_cases i
Cleared hypotheses: i, hij
-- 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
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ (i : Fin (Nat.succ 0).succ), ![s, t] i
i j : Fin (Nat.succ 0).succ
hij : i ≠ j
convert_2 :
  ∀ (hij : (fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩ ≠ j),
    (Disjoint on ![s, t]) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩) j
⊢ (Disjoint on ![s, t]) i j
have convert_2₁ : ∀ (hij : (fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, sorry⟩ ≠ j),
  (Disjoint on ![s, t]) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, sorry⟩) j
Tactic: fin_cases i
Cleared hypotheses: i, hij
-- 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
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ (i : Fin (Nat.succ 0).succ), ![s, t] i
j : Fin (Nat.succ 0).succ
hij : (fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩ ≠ j
⊢ (Disjoint on ![s, t]) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩) j
have convert_2 : ∀
  (hij :
    Ne (α := Fin (Nat.succ 0).succ) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, sorry⟩)
      ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, sorry⟩)),
  (Disjoint on ![s, t]) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j, hij
-- 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
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ (i : Fin (Nat.succ 0).succ), ![s, t] i
j : Fin (Nat.succ 0).succ
hij : (fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩ ≠ j
convert_2 :
  ∀
    (hij :
      Ne (α := Fin (Nat.succ 0).succ) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)
        ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)),
    (Disjoint on ![s, t]) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)
⊢ (Disjoint on ![s, t]) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩) j
have convert_2₁ : ∀
  (hij :
    Ne (α := Fin (Nat.succ 0).succ) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, sorry⟩)
      ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, sorry⟩)),
  (Disjoint on ![s, t]) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j, hij
-- 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
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ (i : Fin (Nat.succ 0).succ), ![s, t] i
j : Fin (Nat.succ 0).succ
hij : (fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩ ≠ j
⊢ (Disjoint on ![s, t]) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩) j
have convert_2 : ∀
  (hij :
    Ne (α := Fin (Nat.succ 0).succ) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, sorry⟩)
      ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, sorry⟩)),
  (Disjoint on ![s, t]) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, sorry⟩) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j, hij
-- 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
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ (i : Fin (Nat.succ 0).succ), ![s, t] i
j : Fin (Nat.succ 0).succ
hij : (fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩ ≠ j
convert_2 :
  ∀
    (hij :
      Ne (α := Fin (Nat.succ 0).succ) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩)
        ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)),
    (Disjoint on ![s, t]) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)
⊢ (Disjoint on ![s, t]) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩) j
have convert_2₁ : ∀
  (hij :
    Ne (α := Fin (Nat.succ 0).succ) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, sorry⟩)
      ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, sorry⟩)),
  (Disjoint on ![s, t]) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, sorry⟩) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j, hij
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : (↑I : Set (Set α)) ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I : Set (Set α)).PairwiseDisjoint id
| ((m : (a : Set α) → G) s : G)
have rw : ((m : (a : Set α) → G) (⋃₀ (↑(I ∪ hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))) : G)
Tactic: rw [← hC.sUnion_union_disjointOfDiffUnion_of_subset hs hI hI_ss]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : (↑I : Set (Set α)) ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I : Set (Set α)).PairwiseDisjoint id
⊢ (m : (a : Set α) → G) s =
    HAdd.hAdd (α := G) (∑ i ∈ I, (m : (a : Set α) → G) i)
      (∑ i ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI, (m : (a : Set α) → G) i)
have conv_lhs : (m : (a : Set α) → G) (⋃₀ (↑(I ∪ hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))) =
  HAdd.hAdd (α := G) (∑ i ∈ I, (m : (a : Set α) → G) i)
    (∑ i ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI, (m : (a : Set α) → G) i)
Tactic: conv_lhs => rw [← hC.sUnion_union_disjointOfDiffUnion_of_subset hs hI hI_ss]