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_1 : Type u_2
inst : AddCommMonoid G_1
m m' : AddContent G_1 C
inst_1 : LinearOrder α
G : Type u_3
inst_2 : AddCommGroup G
f : α → G
n : ℕ
ih :
  ∀ (I : Finset (Set α)) (hI : (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v})
    (h'I : (↑I : Set (Set α)).PairwiseDisjoint id)
    (h''I :
      Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
        (⋃₀ (↑I : Set (Set α))))
    (hn : #I = n), onIocAux f (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, onIocAux f u
I : Finset (Set α)
hI : (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
h'I : (↑I : Set (Set α)).PairwiseDisjoint id
h''I :
  Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v} (⋃₀ (↑I : Set (Set α)))
hn : #I = n + 1
⊢ onIocAux f (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, onIocAux f u
have succ : ∀ (u v : α) (huv : u ≤ v) (h'uv : ⋃₀ (↑I : Set (Set α)) = Set.Ioc u v),
  onIocAux f (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, onIocAux f u
Tactic: rcases h''I with ⟨u, v, huv, h'uv⟩
Cleared hypotheses: h''I
-- 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_1 : Type u_2
inst : AddCommMonoid G_1
m m' : AddContent G_1 C
inst_1 : LinearOrder α
G : Type u_3
inst_2 : AddCommGroup G
f : α → G
n : ℕ
ih :
  ∀ (I : Finset (Set α)) (hI : (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v})
    (h'I : (↑I : Set (Set α)).PairwiseDisjoint id)
    (h''I :
      Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
        (⋃₀ (↑I : Set (Set α))))
    (hn : #I = n), onIocAux f (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, onIocAux f u
I : Finset (Set α)
hI : (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
h'I : (↑I : Set (Set α)).PairwiseDisjoint id
hn : #I = n + 1
u v : α
huv : u ≤ v
h'uv : ⋃₀ (↑I : Set (Set α)) = Set.Ioc u v
⊢ onIocAux f (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, onIocAux f u
have succ : ∀ (huv : u ≤ u) (h'uv : ⋃₀ (↑I : Set (Set α)) = Set.Ioc u u), onIocAux f (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, onIocAux f u
Tactic: rcases huv.eq_or_lt with rfl | huv
Cleared hypotheses: v, huv, h'uv
-- 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_1 : Type u_2
inst : AddCommMonoid G_1
m m' : AddContent G_1 C
inst_1 : LinearOrder α
G : Type u_3
inst_2 : AddCommGroup G
f : α → G
n : ℕ
ih :
  ∀ (I : Finset (Set α)) (hI : (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v})
    (h'I : (↑I : Set (Set α)).PairwiseDisjoint id)
    (h''I :
      Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
        (⋃₀ (↑I : Set (Set α))))
    (hn : #I = n), onIocAux f (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, onIocAux f u
I : Finset (Set α)
hI : (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
h'I : (↑I : Set (Set α)).PairwiseDisjoint id
hn : #I = n + 1
u v : α
huv : u ≤ v
h'uv : ⋃₀ (↑I : Set (Set α)) = Set.Ioc u v
succ :
  ∀ (huv : u ≤ u) (h'uv : ⋃₀ (↑I : Set (Set α)) = Set.Ioc u u),
    onIocAux f (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, onIocAux f u
⊢ onIocAux f (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, onIocAux f u
have succ₁ : ∀ (huv : u < v), onIocAux f (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, onIocAux f u
Tactic: rcases huv.eq_or_lt with rfl | huv
-- 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_1 : Type u_2
inst : AddCommMonoid G_1
m m' : AddContent G_1 C
inst_1 : LinearOrder α
G : Type u_3
inst_2 : AddCommGroup G
f : α → G
n : ℕ
ih :
  ∀ (I : Finset (Set α)) (hI : (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v})
    (h'I : (↑I : Set (Set α)).PairwiseDisjoint id)
    (h''I :
      Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
        (⋃₀ (↑I : Set (Set α))))
    (hn : #I = n), onIocAux f (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, onIocAux f u
I : Finset (Set α)
hI : (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
h'I : (↑I : Set (Set α)).PairwiseDisjoint id
hn : #I = n + 1
u : α
huv : u ≤ u
h'uv : ⋃₀ (↑I : Set (Set α)) = Set.Ioc u u
⊢ onIocAux f (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, onIocAux f u
have this : onIocAux f (Set.Ioc u u) = ∑ u ∈ I, 0
Tactic: have : onIocAux f (Set.Ioc u u) = ∑ u ∈ I, 0 := by simp [onIocAux_empty f]
-- 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_1 : Type u_2
inst : AddCommMonoid G_1
m m' : AddContent G_1 C
inst_1 : LinearOrder α
G : Type u_3
inst_2 : AddCommGroup G
f : α → G
n : ℕ
ih :
  ∀ (I : Finset (Set α)) (hI : (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v})
    (h'I : (↑I : Set (Set α)).PairwiseDisjoint id)
    (h''I :
      Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
        (⋃₀ (↑I : Set (Set α))))
    (hn : #I = n), onIocAux f (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, onIocAux f u
I : Finset (Set α)
hI : (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
h'I : (↑I : Set (Set α)).PairwiseDisjoint id
hn : #I = n + 1
u : α
huv : u ≤ u
h'uv : ⋃₀ (↑I : Set (Set α)) = Set.Ioc u u
this : onIocAux f (Set.Ioc u u) = ∑ u ∈ I, 0
⊢ onIocAux f (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, onIocAux f u
have succ : Eq.{u_3 + 1} (α := G) (∑ u ∈ I, 0) (∑ u ∈ I, onIocAux f u)
Tactic: rw [h'uv, this]
-- 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_1 : Type u_2
inst : AddCommMonoid G_1
m m' : AddContent G_1 C
inst_1 : LinearOrder α
G : Type u_3
inst_2 : AddCommGroup G
f : α → G
n : ℕ
ih :
  ∀ (I : Finset (Set α)) (hI : (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v})
    (h'I : (↑I : Set (Set α)).PairwiseDisjoint id)
    (h''I :
      Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
        (⋃₀ (↑I : Set (Set α))))
    (hn : #I = n), onIocAux f (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, onIocAux f u
I : Finset (Set α)
hI : (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
h'I : (↑I : Set (Set α)).PairwiseDisjoint id
hn : #I = n + 1
u : α
huv : u ≤ u
h'uv : ⋃₀ (↑I : Set (Set α)) = Set.Ioc u u
this : onIocAux f (Set.Ioc u u) = ∑ u ∈ I, 0
⊢ Eq.{u_3 + 1} (α := G) (∑ u ∈ I, 0) (∑ u ∈ I, onIocAux f u)
have apply : ∀ (i : Set α) (hi : i ∈ I), 0 = onIocAux f i
Tactic: apply Finset.sum_congr rfl fun 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_1 : Type u_2
inst : AddCommMonoid G_1
m m' : AddContent G_1 C
inst_1 : LinearOrder α
G : Type u_3
inst_2 : AddCommGroup G
f : α → G
n : ℕ
ih :
  ∀ (I : Finset (Set α)) (hI : (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v})
    (h'I : (↑I : Set (Set α)).PairwiseDisjoint id)
    (h''I :
      Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
        (⋃₀ (↑I : Set (Set α))))
    (hn : #I = n), onIocAux f (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, onIocAux f u
I : Finset (Set α)
hI : (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
h'I : (↑I : Set (Set α)).PairwiseDisjoint id
hn : #I = n + 1
u : α
huv : u ≤ u
h'uv : ⋃₀ (↑I : Set (Set α)) = Set.Ioc u u
this : onIocAux f (Set.Ioc u u) = ∑ u ∈ I, 0
i : Set α
hi : i ∈ I
⊢ 0 = onIocAux f i
have this₁ : i = ∅
Tactic: have : i = ∅ := by grind [sUnion_eq_empty]
-- 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_1 : Type u_2
inst : AddCommMonoid G_1
m m' : AddContent G_1 C
inst_1 : LinearOrder α
G : Type u_3
inst_2 : AddCommGroup G
f : α → G
n : ℕ
ih :
  ∀ (I : Finset (Set α)) (hI : (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v})
    (h'I : (↑I : Set (Set α)).PairwiseDisjoint id)
    (h''I :
      Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
        (⋃₀ (↑I : Set (Set α))))
    (hn : #I = n), onIocAux f (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, onIocAux f u
I : Finset (Set α)
hI : (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
h'I : (↑I : Set (Set α)).PairwiseDisjoint id
hn : #I = n + 1
u v : α
huv_1 : u ≤ v
h'uv : ⋃₀ (↑I : Set (Set α)) = Set.Ioc u v
huv : u < v
⊢ onIocAux f (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, onIocAux f u
have this : v ∈ ⋃₀ (↑I : Set (Set α))
Tactic: have : v ∈ ⋃₀ ↑I := by simp [h'uv, huv]
-- 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_1 : Type u_2
inst : AddCommMonoid G_1
m m' : AddContent G_1 C
inst_1 : LinearOrder α
G : Type u_3
inst_2 : AddCommGroup G
f : α → G
n : ℕ
ih :
  ∀ (I : Finset (Set α)) (hI : (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v})
    (h'I : (↑I : Set (Set α)).PairwiseDisjoint id)
    (h''I :
      Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
        (⋃₀ (↑I : Set (Set α))))
    (hn : #I = n), onIocAux f (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, onIocAux f u
I : Finset (Set α)
hI : (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
h'I : (↑I : Set (Set α)).PairwiseDisjoint id
hn : #I = n + 1
u v : α
huv_1 : u ≤ v
h'uv : ⋃₀ (↑I : Set (Set α)) = Set.Ioc u v
huv : u < v
this : v ∈ ⋃₀ (↑I : Set (Set α))
⊢ onIocAux f (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, onIocAux f u
have succ : ∀ (t : Set α) (tI : t ∈ I) (ht : v ∈ t), onIocAux f (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, onIocAux f u
Tactic: obtain ⟨t, tI, ht⟩ : ∃ t ∈ I, v ∈ t := by simpa using this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
s t_1 : Set α
I_1 : Finset (Set α)
G_1 : Type u_2
inst : AddCommMonoid G_1
m m' : AddContent G_1 C
inst_1 : LinearOrder α
G : Type u_3
inst_2 : AddCommGroup G
f : α → G
n : ℕ
ih :
  ∀ (I : Finset (Set α)) (hI : (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v})
    (h'I : (↑I : Set (Set α)).PairwiseDisjoint id)
    (h''I :
      Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
        (⋃₀ (↑I : Set (Set α))))
    (hn : #I = n), onIocAux f (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, onIocAux f u
I : Finset (Set α)
hI : (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
h'I : (↑I : Set (Set α)).PairwiseDisjoint id
hn : #I = n + 1
u v : α
huv_1 : u ≤ v
h'uv : ⋃₀ (↑I : Set (Set α)) = Set.Ioc u v
huv : u < v
this : v ∈ ⋃₀ (↑I : Set (Set α))
t : Set α
tI : t ∈ I
ht : v ∈ t
⊢ onIocAux f (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, onIocAux f u
have succ : ∀ (u' v' : α) (hu'v' : u' ≤ v') (tI : Set.Ioc u' v' ∈ I) (ht : v ∈ Set.Ioc u' v'),
  onIocAux f (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, onIocAux f u
Tactic: rcases hI tI with ⟨u', v', hu'v', rfl⟩
Cleared hypotheses: t, tI, ht
-- 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_1 : Type u_2
inst : AddCommMonoid G_1
m m' : AddContent G_1 C
inst_1 : LinearOrder α
G : Type u_3
inst_2 : AddCommGroup G
f : α → G
n : ℕ
ih :
  ∀ (I : Finset (Set α)) (hI : (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v})
    (h'I : (↑I : Set (Set α)).PairwiseDisjoint id)
    (h''I :
      Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
        (⋃₀ (↑I : Set (Set α))))
    (hn : #I = n), onIocAux f (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, onIocAux f u
I : Finset (Set α)
hI : (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
h'I : (↑I : Set (Set α)).PairwiseDisjoint id
hn : #I = n + 1
u v : α
huv_1 : u ≤ v
h'uv : ⋃₀ (↑I : Set (Set α)) = Set.Ioc u v
huv : u < v
this : v ∈ ⋃₀ (↑I : Set (Set α))
u' v' : α
hu'v' : u' ≤ v'
tI : Set.Ioc u' v' ∈ I
ht : v ∈ Set.Ioc u' v'
⊢ onIocAux f (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, onIocAux f u
have left : v' ≤ v
Tactic: have ⟨_, uu'⟩ : v' ≤ v ∧ u ≤ u' := (Ioc_subset_Ioc_iff (by grind)).1 (by grind)
-- 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_1 : Type u_2
inst : AddCommMonoid G_1
m m' : AddContent G_1 C
inst_1 : LinearOrder α
G : Type u_3
inst_2 : AddCommGroup G
f : α → G
n : ℕ
ih :
  ∀ (I : Finset (Set α)) (hI : (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v})
    (h'I : (↑I : Set (Set α)).PairwiseDisjoint id)
    (h''I :
      Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
        (⋃₀ (↑I : Set (Set α))))
    (hn : #I = n), onIocAux f (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, onIocAux f u
I : Finset (Set α)
hI : (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
h'I : (↑I : Set (Set α)).PairwiseDisjoint id
hn : #I = n + 1
u v : α
huv_1 : u ≤ v
h'uv : ⋃₀ (↑I : Set (Set α)) = Set.Ioc u v
huv : u < v
this : v ∈ ⋃₀ (↑I : Set (Set α))
u' v' : α
hu'v' : u' ≤ v'
tI : Set.Ioc u' v' ∈ I
ht : v ∈ Set.Ioc u' v'
left : v' ≤ v
⊢ onIocAux f (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, onIocAux f u
have uu' : u ≤ u'
Tactic: have ⟨_, uu'⟩ : v' ≤ v ∧ u ≤ u' := (Ioc_subset_Ioc_iff (by grind)).1 (by grind)
-- 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_1 : Type u_2
inst : AddCommMonoid G_1
m m' : AddContent G_1 C
inst_1 : LinearOrder α
G : Type u_3
inst_2 : AddCommGroup G
f : α → G
n : ℕ
ih :
  ∀ (I : Finset (Set α)) (hI : (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v})
    (h'I : (↑I : Set (Set α)).PairwiseDisjoint id)
    (h''I :
      Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
        (⋃₀ (↑I : Set (Set α))))
    (hn : #I = n), onIocAux f (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, onIocAux f u
I : Finset (Set α)
hI : (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
h'I : (↑I : Set (Set α)).PairwiseDisjoint id
hn : #I = n + 1
u v : α
huv_1 : u ≤ v
h'uv : ⋃₀ (↑I : Set (Set α)) = Set.Ioc u v
huv : u < v
this : v ∈ ⋃₀ (↑I : Set (Set α))
u' v' : α
hu'v' : u' ≤ v'
tI : Set.Ioc u' v' ∈ I
ht : v ∈ Set.Ioc u' v'
left : v' ≤ v
uu' : u ≤ u'
⊢ onIocAux f (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, onIocAux f u
have hu'v'₁ : u' ≤ v
Tactic: obtain rfl : v = v' := by grind
Cleared hypotheses: v', hu'v', tI, ht, left
-- 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_1 : Type u_2
inst : AddCommMonoid G_1
m m' : AddContent G_1 C
inst_1 : LinearOrder α
G : Type u_3
inst_2 : AddCommGroup G
f : α → G
n : ℕ
ih :
  ∀ (I : Finset (Set α)) (hI : (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v})
    (h'I : (↑I : Set (Set α)).PairwiseDisjoint id)
    (h''I :
      Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
        (⋃₀ (↑I : Set (Set α))))
    (hn : #I = n), onIocAux f (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, onIocAux f u
I : Finset (Set α)
hI : (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
h'I : (↑I : Set (Set α)).PairwiseDisjoint id
hn : #I = n + 1
u v : α
huv_1 : u ≤ v
h'uv : ⋃₀ (↑I : Set (Set α)) = Set.Ioc u v
huv : u < v
this : v ∈ ⋃₀ (↑I : Set (Set α))
u' v' : α
hu'v' : u' ≤ v'
tI : Set.Ioc u' v' ∈ I
ht : v ∈ Set.Ioc u' v'
left : v' ≤ v
uu' : u ≤ u'
hu'v'₁ : u' ≤ v
⊢ onIocAux f (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, onIocAux f u
have tI₁ : Set.Ioc u' v ∈ I
Tactic: obtain rfl : v = v' := by grind
Cleared hypotheses: v', hu'v', tI, ht, left
-- 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_1 : Type u_2
inst : AddCommMonoid G_1
m m' : AddContent G_1 C
inst_1 : LinearOrder α
G : Type u_3
inst_2 : AddCommGroup G
f : α → G
n : ℕ
ih :
  ∀ (I : Finset (Set α)) (hI : (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v})
    (h'I : (↑I : Set (Set α)).PairwiseDisjoint id)
    (h''I :
      Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
        (⋃₀ (↑I : Set (Set α))))
    (hn : #I = n), onIocAux f (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, onIocAux f u
I : Finset (Set α)
hI : (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
h'I : (↑I : Set (Set α)).PairwiseDisjoint id
hn : #I = n + 1
u v : α
huv_1 : u ≤ v
h'uv : ⋃₀ (↑I : Set (Set α)) = Set.Ioc u v
huv : u < v
this : v ∈ ⋃₀ (↑I : Set (Set α))
u' v' : α
hu'v' : u' ≤ v'
tI : Set.Ioc u' v' ∈ I
ht : v ∈ Set.Ioc u' v'
left : v' ≤ v
uu' : u ≤ u'
hu'v'₁ : u' ≤ v
tI₁ : Set.Ioc u' v ∈ I
⊢ onIocAux f (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, onIocAux f u
have ht₁ : v ∈ Set.Ioc u' v
Tactic: obtain rfl : v = v' := by grind
Cleared hypotheses: v', hu'v', tI, ht, left
-- 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_1 : Type u_2
inst : AddCommMonoid G_1
m m' : AddContent G_1 C
inst_1 : LinearOrder α
G : Type u_3
inst_2 : AddCommGroup G
f : α → G
n : ℕ
ih :
  ∀ (I : Finset (Set α)) (hI : (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v})
    (h'I : (↑I : Set (Set α)).PairwiseDisjoint id)
    (h''I :
      Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
        (⋃₀ (↑I : Set (Set α))))
    (hn : #I = n), onIocAux f (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, onIocAux f u
I : Finset (Set α)
hI : (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
h'I : (↑I : Set (Set α)).PairwiseDisjoint id
hn : #I = n + 1
u v : α
huv_1 : u ≤ v
h'uv : ⋃₀ (↑I : Set (Set α)) = Set.Ioc u v
huv : u < v
this : v ∈ ⋃₀ (↑I : Set (Set α))
u' v' : α
hu'v' : u' ≤ v'
tI : Set.Ioc u' v' ∈ I
ht : v ∈ Set.Ioc u' v'
left : v' ≤ v
uu' : u ≤ u'
hu'v'₁ : u' ≤ v
tI₁ : Set.Ioc u' v ∈ I
ht₁ : v ∈ Set.Ioc u' v
⊢ onIocAux f (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, onIocAux f u
have left : v ≤ v
Tactic: obtain rfl : v = v' := by grind
Cleared hypotheses: v', hu'v', tI, ht, left
-- 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_1 : Type u_2
inst : AddCommMonoid G_1
m m' : AddContent G_1 C
inst_1 : LinearOrder α
G : Type u_3
inst_2 : AddCommGroup G
f : α → G
n : ℕ
ih :
  ∀ (I : Finset (Set α)) (hI : (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v})
    (h'I : (↑I : Set (Set α)).PairwiseDisjoint id)
    (h''I :
      Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
        (⋃₀ (↑I : Set (Set α))))
    (hn : #I = n), onIocAux f (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, onIocAux f u
I : Finset (Set α)
hI : (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
h'I : (↑I : Set (Set α)).PairwiseDisjoint id
hn : #I = n + 1
u v : α
huv_1 : u ≤ v
h'uv : ⋃₀ (↑I : Set (Set α)) = Set.Ioc u v
huv : u < v
this : v ∈ ⋃₀ (↑I : Set (Set α))
u' : α
uu' : u ≤ u'
hu'v' : u' ≤ v
tI : Set.Ioc u' v ∈ I
ht : v ∈ Set.Ioc u' v
left : v ≤ v
⊢ onIocAux f (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, onIocAux f u
have succ : f v - f u = ∑ u ∈ I, onIocAux f u
Tactic: rw [h'uv, onIocAux_apply huv.le]
-- 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_1 : Type u_2
inst : AddCommMonoid G_1
m m' : AddContent G_1 C
inst_1 : LinearOrder α
G : Type u_3
inst_2 : AddCommGroup G
f : α → G
n : ℕ
ih :
  ∀ (I : Finset (Set α)) (hI : (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v})
    (h'I : (↑I : Set (Set α)).PairwiseDisjoint id)
    (h''I :
      Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
        (⋃₀ (↑I : Set (Set α))))
    (hn : #I = n), onIocAux f (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, onIocAux f u
I : Finset (Set α)
hI : (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
h'I : (↑I : Set (Set α)).PairwiseDisjoint id
hn : #I = n + 1
u v : α
huv_1 : u ≤ v
h'uv : ⋃₀ (↑I : Set (Set α)) = Set.Ioc u v
huv : u < v
this : v ∈ ⋃₀ (↑I : Set (Set α))
u' : α
uu' : u ≤ u'
hu'v' : u' ≤ v
tI : Set.Ioc u' v ∈ I
ht : v ∈ Set.Ioc u' v
left : v ≤ v
I' : Finset (Set α) := I.erase (Set.Ioc u' v)
⊢ f v - f u = ∑ u ∈ I, onIocAux f u
have I'I : I' ⊆ I
Tactic: have I'I : I' ⊆ I := erase_subset (Set.Ioc u' v) I
-- 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_1 : Type u_2
inst : AddCommMonoid G_1
m m' : AddContent G_1 C
inst_1 : LinearOrder α
G : Type u_3
inst_2 : AddCommGroup G
f : α → G
n : ℕ
ih :
  ∀ (I : Finset (Set α)) (hI : (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v})
    (h'I : (↑I : Set (Set α)).PairwiseDisjoint id)
    (h''I :
      Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
        (⋃₀ (↑I : Set (Set α))))
    (hn : #I = n), onIocAux f (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, onIocAux f u
I : Finset (Set α)
hI : (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
h'I : (↑I : Set (Set α)).PairwiseDisjoint id
hn : #I = n + 1
u v : α
huv_1 : u ≤ v
h'uv : ⋃₀ (↑I : Set (Set α)) = Set.Ioc u v
huv : u < v
this : v ∈ ⋃₀ (↑I : Set (Set α))
u' : α
uu' : u ≤ u'
hu'v' : u' ≤ v
tI : Set.Ioc u' v ∈ I
ht : v ∈ Set.Ioc u' v
left : v ≤ v
I' : Finset (Set α) := I.erase (Set.Ioc u' v)
I'I : I' ⊆ I
⊢ f v - f u = ∑ u ∈ I, onIocAux f u
have I_eq_insert : I = insert (Set.Ioc u' v) I'
Tactic: have I_eq_insert : I = insert (Set.Ioc u' v) I' := by simp [I', tI]
-- 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_1 : Type u_2
inst : AddCommMonoid G_1
m m' : AddContent G_1 C
inst_1 : LinearOrder α
G : Type u_3
inst_2 : AddCommGroup G
f : α → G
n : ℕ
ih :
  ∀ (I : Finset (Set α)) (hI : (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v})
    (h'I : (↑I : Set (Set α)).PairwiseDisjoint id)
    (h''I :
      Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
        (⋃₀ (↑I : Set (Set α))))
    (hn : #I = n), onIocAux f (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, onIocAux f u
I : Finset (Set α)
hI : (↑I : Set (Set α)) ⊆ {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}
h'I : (↑I : Set (Set α)).PairwiseDisjoint id
hn : #I = n + 1
u v : α
huv_1 : u ≤ v
h'uv : ⋃₀ (↑I : Set (Set α)) = Set.Ioc u v
huv : u < v
this : v ∈ ⋃₀ (↑I : Set (Set α))
u' : α
uu' : u ≤ u'
hu'v' : u' ≤ v
tI : Set.Ioc u' v ∈ I
ht : v ∈ Set.Ioc u' v
left : v ≤ v
I' : Finset (Set α) := I.erase (Set.Ioc u' v)
I'I : I' ⊆ I
I_eq_insert : I = insert (Set.Ioc u' v) I'
⊢ (Set.Ioc u' v ∪ ⋃₀ (↑I' : Set (Set α))) \ Set.Ioc u' v = ⋃₀ (↑I' : Set (Set α))
have refine : Disjoint (Set.Ioc u' v) (⋃₀ (↑I' : Set (Set α)))
Tactic: refine Disjoint.sup_sdiff_cancel_left ?_