awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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 α))

Tactic:
Disjoint.sup_sdiff_cancel_left ?_

Premises used: Disjoint.sup_sdiff_cancel_left
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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'
refine : Disjoint (Set.Ioc u' v) (⋃₀ (↑I' : Set (Set α)))
⊢ (Set.Ioc u' v ∪ ⋃₀ (↑I' : Set (Set α))) \ Set.Ioc u' v = ⋃₀ (↑I' : Set (Set α))

Tactic:
refine Disjoint.sup_sdiff_cancel_left ?_

Premises used: Disjoint.sup_sdiff_cancel_left
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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'
simp : ∀ t ∈ (↑I : Set (Set α)), ¬t = Set.Ioc u' v → Disjoint (Set.Ioc u' v) t
⊢ Disjoint (Set.Ioc u' v) (⋃₀ (↑I' : Set (Set α)))

Tactic:
simp only [coe_erase, disjoint_sUnion_right, mem_diff, mem_singleton_iff, and_imp, I']

Premises used: and_imp, Finset.coe_erase, Set.mem_singleton_iff, Set.disjoint_sUnion_right, Set.mem_diff
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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_1 v : α
huv_1 : u_1 ≤ v
h'uv : ⋃₀ (↑I : Set (Set α)) = Set.Ioc u_1 v
huv : u_1 < v
this : v ∈ ⋃₀ (↑I : Set (Set α))
u' : α
uu' : u_1 ≤ 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'
u : Set α
hu : u ∈ (↑I : Set (Set α))
hu' : ¬u = Set.Ioc u' v
⊢ Disjoint (Set.Ioc u' v) u

Tactic:
(h'I hu tI hu').symm

Premises used: Set.Ioc, setOf, Disjoint.symm
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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_1 v : α
huv_1 : u_1 ≤ v
h'uv : ⋃₀ (↑I : Set (Set α)) = Set.Ioc u_1 v
huv : u_1 < v
this : v ∈ ⋃₀ (↑I : Set (Set α))
u' : α
uu' : u_1 ≤ 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'
u : Set α
hu : u ∈ (↑I : Set (Set α))
hu' : ¬u = Set.Ioc u' v
⊢ Disjoint (Set.Ioc u' v) u

Tactic:
exact (h'I hu tI hu').symm

Premises used: Disjoint.symm
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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 α))

Tactic:
have : (Ioc u' v ∪ ⋃₀ ↑I') \ Ioc u' v = ⋃₀ ↑I' := by
          refine Disjoint.sup_sdiff_cancel_left ?_
          simp only [coe_erase, disjoint_sUnion_right, mem_diff, mem_singleton_iff, and_imp, I']
          intro u hu hu'
          exact (h'I hu tI hu').symm
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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_1 : 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'
this : (Set.Ioc u' v ∪ ⋃₀ (↑I' : Set (Set α))) \ Set.Ioc u' v = ⋃₀ (↑I' : Set (Set α))
⊢ Set.Ioc u' v ∪ ⋃₀ (↑I' : Set (Set α)) = Set.Ioc u v

Tactic:
simp only [I_eq_insert, coe_insert, sUnion_insert] at h'uv

Premises used: Set.sUnion_insert, Finset.coe_insert
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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
huv : u < v
this_1 : 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'
this : (Set.Ioc u' v ∪ ⋃₀ (↑I' : Set (Set α))) \ Set.Ioc u' v = ⋃₀ (↑I' : Set (Set α))
h'uv : Set.Ioc u' v ∪ ⋃₀ (↑I' : Set (Set α)) = Set.Ioc u v
⊢ ⋃₀ (↑I' : Set (Set α)) = Set.Ioc u u'

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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'
⊢ ⋃₀ (↑I' : Set (Set α)) = Set.Ioc u u'

Tactic:
have UI' : ⋃₀ ↑I' = Ioc u u' := by
        have : (Ioc u' v ∪ ⋃₀ ↑I') \ Ioc u' v = ⋃₀ ↑I' := by
          refine Disjoint.sup_sdiff_cancel_left ?_
          simp only [coe_erase, disjoint_sUnion_right, mem_diff, mem_singleton_iff, and_imp, I']
          intro u hu hu'
          exact (h'I hu tI hu').symm
        simp only [I_eq_insert, coe_insert, sUnion_insert] at h'uv
        grind
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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'
UI' : ⋃₀ (↑I' : Set (Set α)) = Set.Ioc u u'
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v} (⋃₀ (↑I' : Set (Set α)))

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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'
UI' : ⋃₀ (↑I' : Set (Set α)) = Set.Ioc u u'
⊢ #I' = n

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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'
UI' : ⋃₀ (↑I' : Set (Set α)) = Set.Ioc u u'
⊢ onIocAux f (⋃₀ (↑I' : Set (Set α))) = ∑ u ∈ I', onIocAux f u

Tactic:
have IH : onIocAux f (⋃₀ ↑I') = ∑ u ∈ I', onIocAux f u :=
        ih _ (Subset.trans I'I hI) (h'I.subset I'I) (by grind) (by grind)
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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'
UI' : ⋃₀ (↑I' : Set (Set α)) = Set.Ioc u u'
IH : onIocAux f (⋃₀ (↑I' : Set (Set α))) = ∑ u ∈ I', onIocAux f u
succ : f v - f u = f v - f u' + (f u' - f u)
succ₁ : Set.Ioc u' v ∉ I'
⊢ f v - f u = ∑ u ∈ I, onIocAux f u

Tactic:
rw [I_eq_insert, sum_insert, ← IH, UI', onIocAux_apply hu'v', onIocAux_apply uu']

Premises used: MeasureTheory.AddContent.onIocAux_apply, Finset.sum_insert
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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'
UI' : ⋃₀ (↑I' : Set (Set α)) = Set.Ioc u u'
IH : onIocAux f (⋃₀ (↑I' : Set (Set α))) = ∑ u ∈ I', onIocAux f u
⊢ f v - f u = f v - f u' + (f u' - f u)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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'
UI' : ⋃₀ (↑I' : Set (Set α)) = Set.Ioc u u'
IH : onIocAux f (⋃₀ (↑I' : Set (Set α))) = ∑ u ∈ I', onIocAux f u
⊢ Set.Ioc u' v ∉ I'

Tactic:
simp [I']
-- Module: Mathlib.MeasureTheory.Measure.AddContent
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
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 α)))
induction : ∀ (x : ℕ) (hn : #I = x), onIocAux f (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, onIocAux f u
⊢ onIocAux f (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, onIocAux f u

Tactic:
induction hn : Finset.card I generalizing I with
    | zero =>
      have : I = ∅ := by grind
      simp [this, onIocAux_empty f]
    | succ n ih =>
      rcases h''I with ⟨u, v, huv, h'uv⟩
      -- If the interval `(u, v]` is empty, i.e., `u = v`, then the result is easy.
      rcases huv.eq_or_lt with rfl | huv
      · have : onIocAux f (Set.Ioc u u) = ∑ u ∈ I, 0 := by simp [onIocAux_empty f]
        rw [h'uv, this]
        apply Finset.sum_congr rfl fun i hi ↦ ?_
        have : i = ∅ := by grind [sUnion_eq_empty]
        grind [onIocAux_empty]
      -- otherwise, `v` is in `(u, v]`, therefore it belongs to some interval `(u', v']`
      -- featuring in the union.
      have : v ∈ ⋃₀ ↑I := by simp [h'uv, huv]
      obtain ⟨t, tI, ht⟩ : ∃ t ∈ I, v ∈ t := by simpa using this
      rcases hI tI with ⟨u', v', hu'v', rfl⟩
      -- we have `u ≤ u'` and `v' = v` since `(u', v']` is part of the union, and therefore
      -- contained in `(u, v]`.
      have ⟨_, uu'⟩ : v' ≤ v ∧ u ≤ u' := (Ioc_subset_Ioc_iff (by grind)).1 (by grind)
      obtain rfl : v = v' := by grind
      rw [h'uv, onIocAux_apply huv.le]
      -- let us remove the right-most interval `(u', v]` from the union, and let `I'` be the
      -- remaining set of intervals.
      let I' := I.erase (Set.Ioc u' v)
      have I'I : I' ⊆ I := erase_subset (Set.Ioc u' v) I
      have I_eq_insert : I = insert (Set.Ioc u' v) I' := by simp [I', tI]
      -- the intervals in `I'` cover exactly `(u, u']`.
      have UI' : ⋃₀ ↑I' = Ioc u u' := by
        have : (Ioc u' v ∪ ⋃₀ ↑I') \ Ioc u' v = ⋃₀ ↑I' := by
          refine Disjoint.sup_sdiff_cancel_left ?_
          simp only [coe_erase, disjoint_sUnion_right, mem_diff, mem_singleton_iff, and_imp, I']
          intro u hu hu'
          exact (h'I hu tI hu').symm
        simp only [I_eq_insert, coe_insert, sUnion_insert] at h'uv
        grind
      -- by the inductive assumption, the sum over `I'` is exactly `f u' - f u`.
      have IH : onIocAux f (⋃₀ ↑I') = ∑ u ∈ I', onIocAux f u :=
        ih _ (Subset.trans I'I hI) (h'I.subset I'I) (by grind) (by grind)
      -- the conclusion follows.
      rw [I_eq_insert, sum_insert, ← IH, UI', onIocAux_apply hu'v', onIocAux_apply uu']
      · simp
      · simp [I']

Premises used: Finset.card, MeasureTheory.AddContent.onIocAux_empty, Finset.sum_insert, Finset.sum_congr, rfl
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
inst : LinearOrder α
G : Type u_3
inst_1 : AddCommGroup G
f : α → G
u v : α
h : u ≤ v
⊢ (onIoc f : (a : Set α) → G) (Set.Ioc u v) = f v - f u

Tactic:
AddContent.onIocAux_apply h

Premises used: MeasureTheory.AddContent.onIocAux, dite, MeasureTheory.AddContent.onIocAux_apply
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
I : Finset (Set α)
G : Type u_2
inst : AddCommMonoid G
m_1 m' : AddContent G C
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
h : ∅ ∈ C
⊢ extend (P := Membership.mem C) (fun (x : Set α) (x_1 : x ∈ C) ↦ (m : (a : Set α) → ℝ≥0∞) x) ∅ = 0

Tactic:
rw [extend_eq, addContent_empty]

Premises used: MeasureTheory.extend_eq, MeasureTheory.addContent_empty
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
I : Finset (Set α)
G : Type u_2
inst : AddCommMonoid G
m_1 m' : AddContent G C
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
⊢ ∅ ∈ C

Tactic:
hC.empty_mem

Premises used: MeasureTheory.IsSetSemiring.empty_mem