awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
t : Set α
G : Type u_2
inst : AddCommMonoid G
inst_1 : PartialOrder G
inst_2 : CanonicallyOrderedAdd G
m : AddContent G C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
ht : t ∈ C
htJ : t ⊆ ⋃₀ (↑J : Set (Set α))
Jt : Finset (Set α) := Finset.image (fun (u : Set α) ↦ t ∩ u) J
rw : t ⊆ ⋃ i ∈ (↑J : Set (Set α)), i
⊢ t = ⋃₀ (↑Jt : Set (Set α))

Tactic:
rw [coe_image, sUnion_image, ← inter_iUnion₂, inter_eq_self_of_subset_left]

Premises used: Finset.coe_image, Set.inter_iUnion₂, Set.sUnion_image, Set.inter_eq_self_of_subset_left
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
t : Set α
G : Type u_2
inst : AddCommMonoid G
inst_1 : PartialOrder G
inst_2 : CanonicallyOrderedAdd G
m : AddContent G C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
ht : t ∈ C
htJ : t ⊆ ⋃₀ (↑J : Set (Set α))
Jt : Finset (Set α) := Finset.image (fun (u : Set α) ↦ t ∩ u) J
rwa rwa₁ rwa₂ rwa₃ : t ⊆ ⋃₀ (↑J : Set (Set α))
⊢ t ⊆ ⋃ i ∈ (↑J : Set (Set α)), i

Tactic:
rwa [← sUnion_eq_biUnion]

Premises used: Set.sUnion_eq_biUnion
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
t : Set α
G : Type u_2
inst : AddCommMonoid G
inst_1 : PartialOrder G
inst_2 : CanonicallyOrderedAdd G
m : AddContent G C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
ht : t ∈ C
htJ : t ⊆ ⋃₀ (↑J : Set (Set α))
Jt : Finset (Set α) := Finset.image (fun (u : Set α) ↦ t ∩ u) J
⊢ t = ⋃₀ (↑Jt : Set (Set α))

Tactic:
have ht_eq : t = ⋃₀ Jt := by
    rw [coe_image, sUnion_image, ← inter_iUnion₂, inter_eq_self_of_subset_left]
    rwa [← sUnion_eq_biUnion]
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
t : Set α
G : Type u_2
inst : AddCommMonoid G
inst_1 : PartialOrder G
inst_2 : CanonicallyOrderedAdd G
m : AddContent G C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
ht : t ∈ C
htJ : t ⊆ ⋃₀ (↑J : Set (Set α))
Jt : Finset (Set α) := Finset.image (fun (u : Set α) ↦ t ∩ u) J
ht_eq : t = ⋃₀ (↑Jt : Set (Set α))
rw : LE.le.{u_2} (α := G) ((m : (a : Set α) → G) (⋃₀ (↑Jt : Set (Set α))) : G) (∑ u ∈ J, (m : (a : Set α) → G) u : G)
⊢ LE.le.{u_2} (α := G) ((m : (a : Set α) → G) t : G) (∑ u ∈ J, (m : (a : Set α) → G) u : G)

Tactic:
rw [ht_eq]
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
t : Set α
G : Type u_2
inst : AddCommMonoid G
inst_1 : PartialOrder G
inst_2 : CanonicallyOrderedAdd G
m : AddContent G C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
ht : t ∈ C
htJ : t ⊆ ⋃₀ (↑J : Set (Set α))
Jt : Finset (Set α) := Finset.image (fun (u : Set α) ↦ t ∩ u) J
ht_eq : t = ⋃₀ (↑Jt : Set (Set α))
⊢ LE.le.{u_2} (α := G) ((m : (a : Set α) → G) (⋃₀ (↑Jt : Set (Set α))) : G) (∑ u ∈ J, (m : (a : Set α) → G) u : G)

Tactic:
(addContent_sUnion_le_sum hC Jt ?_ ?_).trans ?_

Premises used: MeasureTheory.addContent_sUnion_le_sum, LE.le.trans
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
t : Set α
G : Type u_2
inst : AddCommMonoid G
inst_1 : PartialOrder G
inst_2 : CanonicallyOrderedAdd G
m : AddContent G C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
ht : t ∈ C
htJ : t ⊆ ⋃₀ (↑J : Set (Set α))
Jt : Finset (Set α) := Finset.image (fun (u : Set α) ↦ t ∩ u) J
ht_eq : t = ⋃₀ (↑Jt : Set (Set α))
refine_1 : (↑Jt : Set (Set α)) ⊆ C
refine_2 : ⋃₀ (↑Jt : Set (Set α)) ∈ C
refine_3 : LE.le.{u_2} (α := G) (∑ u ∈ Jt, (m : (a : Set α) → G) u) (∑ u ∈ J, (m : (a : Set α) → G) u)
⊢ LE.le.{u_2} (α := G) ((m : (a : Set α) → G) (⋃₀ (↑Jt : Set (Set α))) : G) (∑ u ∈ J, (m : (a : Set α) → G) u : G)

Tactic:
refine (addContent_sUnion_le_sum hC Jt ?_ ?_).trans ?_

Premises used: MeasureTheory.addContent_sUnion_le_sum, LE.le.trans
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
t : Set α
G : Type u_2
inst : AddCommMonoid G
inst_1 : PartialOrder G
inst_2 : CanonicallyOrderedAdd G
m : AddContent G C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
ht : t ∈ C
htJ : t ⊆ ⋃₀ (↑J : Set (Set α))
Jt : Finset (Set α) := Finset.image (fun (u : Set α) ↦ t ∩ u) J
ht_eq : t = ⋃₀ (↑Jt : Set (Set α))
s : Set α
refine_1 : ∀ x ∈ J, t ∩ x = s → s ∈ C
⊢ s ∈ (↑Jt : Set (Set α)) → s ∈ C

Tactic:
simp only [Jt, coe_image, Set.mem_image, mem_coe, forall_exists_index, and_imp]

Premises used: and_imp, Set.mem_image, forall_exists_index, Finset.coe_image, Finset.mem_coe
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
t : Set α
G : Type u_2
inst : AddCommMonoid G
inst_1 : PartialOrder G
inst_2 : CanonicallyOrderedAdd G
m : AddContent G C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
ht : t ∈ C
htJ : t ⊆ ⋃₀ (↑J : Set (Set α))
Jt : Finset (Set α) := Finset.image (fun (u : Set α) ↦ t ∩ u) J
ht_eq : t = ⋃₀ (↑Jt : Set (Set α))
u : Set α
hu : u ∈ J
⊢ t ∩ u ∈ C

Tactic:
hC.inter_mem _ ht _ (h_ss hu)

Premises used: MeasureTheory.IsSetSemiring.inter_mem
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
t : Set α
G : Type u_2
inst : AddCommMonoid G
inst_1 : PartialOrder G
inst_2 : CanonicallyOrderedAdd G
m : AddContent G C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
ht : t ∈ C
htJ : t ⊆ ⋃₀ (↑J : Set (Set α))
Jt : Finset (Set α) := Finset.image (fun (u : Set α) ↦ t ∩ u) J
ht_eq : t = ⋃₀ (↑Jt : Set (Set α))
u : Set α
hu : u ∈ J
⊢ t ∩ u ∈ C

Tactic:
exact hC.inter_mem _ ht _ (h_ss hu)

Premises used: MeasureTheory.IsSetSemiring.inter_mem
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
t : Set α
G : Type u_2
inst : AddCommMonoid G
inst_1 : PartialOrder G
inst_2 : CanonicallyOrderedAdd G
m : AddContent G C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
ht : t ∈ C
htJ : t ⊆ ⋃₀ (↑J : Set (Set α))
Jt : Finset (Set α) := Finset.image (fun (u : Set α) ↦ t ∩ u) J
ht_eq : t = ⋃₀ (↑Jt : Set (Set α))
refine_2 refine_2₁ refine_2₂ refine_2₃ : t ∈ C
⊢ ⋃₀ (↑Jt : Set (Set α)) ∈ C

Tactic:
rwa [← ht_eq]
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
t : Set α
G : Type u_2
inst : AddCommMonoid G
inst_1 : PartialOrder G
inst_2 : CanonicallyOrderedAdd G
m : AddContent G C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
ht : t ∈ C
htJ : t ⊆ ⋃₀ (↑J : Set (Set α))
Jt : Finset (Set α) := Finset.image (fun (u : Set α) ↦ t ∩ u) J
ht_eq : t = ⋃₀ (↑Jt : Set (Set α))
⊢ LE.le.{u_2} (α := G) (∑ u ∈ Jt, (m : (a : Set α) → G) u) (∑ u ∈ J, (m : (a : Set α) → G) u)

Tactic:
(Finset.sum_image_le_of_nonneg fun _ _ ↦ zero_le).trans (sum_le_sum fun u hu ↦ ?_)

Premises used: zero_le, Finset.sum_image_le_of_nonneg, Finset.sum_le_sum, LE.le.trans
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
t : Set α
G : Type u_2
inst : AddCommMonoid G
inst_1 : PartialOrder G
inst_2 : CanonicallyOrderedAdd G
m : AddContent G C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
ht : t ∈ C
htJ : t ⊆ ⋃₀ (↑J : Set (Set α))
Jt : Finset (Set α) := Finset.image (fun (u : Set α) ↦ t ∩ u) J
ht_eq : t = ⋃₀ (↑Jt : Set (Set α))
refine_3 :
  ∀ (u : Set α) (hu : u ∈ J), LE.le.{u_2} (α := G) ((m : (a : Set α) → G) (t ∩ u) : G) ((m : (a : Set α) → G) u : G)
⊢ LE.le.{u_2} (α := G) (∑ u ∈ Jt, (m : (a : Set α) → G) u) (∑ u ∈ J, (m : (a : Set α) → G) u)

Tactic:
refine (Finset.sum_image_le_of_nonneg fun _ _ ↦ zero_le).trans (sum_le_sum fun u hu ↦ ?_)

Premises used: zero_le, Finset.sum_image_le_of_nonneg, Finset.sum_le_sum, LE.le.trans
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
t : Set α
G : Type u_2
inst : AddCommMonoid G
inst_1 : PartialOrder G
inst_2 : CanonicallyOrderedAdd G
m : AddContent G C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
ht : t ∈ C
htJ : t ⊆ ⋃₀ (↑J : Set (Set α))
Jt : Finset (Set α) := Finset.image (fun (u : Set α) ↦ t ∩ u) J
ht_eq : t = ⋃₀ (↑Jt : Set (Set α))
u : Set α
hu : u ∈ J
⊢ LE.le.{u_2} (α := G) ((m : (a : Set α) → G) (t ∩ u) : G) ((m : (a : Set α) → G) u : G)

Tactic:
addContent_mono hC (hC.inter_mem _ ht _ (h_ss hu)) (h_ss hu) inter_subset_right

Premises used: MeasureTheory.addContent_mono, MeasureTheory.IsSetSemiring.inter_mem, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
t : Set α
G : Type u_2
inst : AddCommMonoid G
inst_1 : PartialOrder G
inst_2 : CanonicallyOrderedAdd G
m : AddContent G C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
ht : t ∈ C
htJ : t ⊆ ⋃₀ (↑J : Set (Set α))
Jt : Finset (Set α) := Finset.image (fun (u : Set α) ↦ t ∩ u) J
ht_eq : t = ⋃₀ (↑Jt : Set (Set α))
u : Set α
hu : u ∈ J
⊢ LE.le.{u_2} (α := G) ((m : (a : Set α) → G) (t ∩ u) : G) ((m : (a : Set α) → G) u : G)

Tactic:
exact addContent_mono hC (hC.inter_mem _ ht _ (h_ss hu)) (h_ss hu) inter_subset_right

Premises used: MeasureTheory.addContent_mono, MeasureTheory.IsSetSemiring.inter_mem, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
t : Set α
G : Type u_2
inst : AddCommMonoid G
inst_1 : PartialOrder G
inst_2 : CanonicallyOrderedAdd G
m : AddContent G C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
ht : t ∈ C
htJ : t ⊆ ⋃₀ (↑J : Set (Set α))
let let₁ let₂ : LE.le.{u_2} (α := G) ((m : (a : Set α) → G) t : G) (∑ u ∈ J, (m : (a : Set α) → G) u : G)
let₃ :
  let Jt : Finset (Set α) := Finset.image (fun (u : Set α) ↦ t ∩ u) J;
  ∀ (ht_eq : t = ⋃₀ (↑Jt : Set (Set α))),
    LE.le.{u_2} (α := G) ((m : (a : Set α) → G) t : G) (∑ u ∈ J, (m : (a : Set α) → G) u : G)
let₄ :
  let Jt : Finset (Set α) := Finset.image (fun (u : Set α) ↦ t ∩ u) J;
  ∀ (ht_eq : t = ⋃₀ (↑Jt : Set (Set α))),
    LE.le.{u_2} (α := G) ((m : (a : Set α) → G) (⋃₀ (↑Jt : Set (Set α))) : G) (∑ u ∈ J, (m : (a : Set α) → G) u : G)
refine_1 :
  let Jt : Finset (Set α) := Finset.image (fun (u : Set α) ↦ t ∩ u) J;
  ∀ (ht_eq : t = ⋃₀ (↑Jt : Set (Set α))), (↑Jt : Set (Set α)) ⊆ C
refine_2 :
  let Jt : Finset (Set α) := Finset.image (fun (u : Set α) ↦ t ∩ u) J;
  ∀ (ht_eq : t = ⋃₀ (↑Jt : Set (Set α))), ⋃₀ (↑Jt : Set (Set α)) ∈ C
refine_3 :
  let Jt : Finset (Set α) := Finset.image (fun (u : Set α) ↦ t ∩ u) J;
  ∀ (ht_eq : t = ⋃₀ (↑Jt : Set (Set α))),
    LE.le.{u_2} (α := G) (∑ u ∈ Jt, (m : (a : Set α) → G) u) (∑ u ∈ J, (m : (a : Set α) → G) u)
refine_2₁ :
  let Jt : Finset (Set α) := Finset.image (fun (u : Set α) ↦ t ∩ u) J;
  ∀ (ht_eq : t = ⋃₀ (↑Jt : Set (Set α))), ⋃₀ (↑Jt : Set (Set α)) ∈ C
refine_3₁ refine_3₂ :
  let Jt : Finset (Set α) := Finset.image (fun (u : Set α) ↦ t ∩ u) J;
  ∀ (ht_eq : t = ⋃₀ (↑Jt : Set (Set α))),
    LE.le.{u_2} (α := G) (∑ u ∈ Jt, (m : (a : Set α) → G) u) (∑ u ∈ J, (m : (a : Set α) → G) u)
⊢ LE.le.{u_2} (α := G) ((m : (a : Set α) → G) t : G) (∑ u ∈ J, (m : (a : Set α) → G) u : G)

Tactic:
classical
  let Jt := J.image (fun u ↦ t ∩ u)
  have ht_eq : t = ⋃₀ Jt := by
    rw [coe_image, sUnion_image, ← inter_iUnion₂, inter_eq_self_of_subset_left]
    rwa [← sUnion_eq_biUnion]
  rw [ht_eq]
  refine (addContent_sUnion_le_sum hC Jt ?_ ?_).trans ?_
  · intro s
    simp only [Jt, coe_image, Set.mem_image, mem_coe, forall_exists_index, and_imp]
    rintro u hu rfl
    exact hC.inter_mem _ ht _ (h_ss hu)
  · rwa [← ht_eq]
  · refine (Finset.sum_image_le_of_nonneg fun _ _ ↦ zero_le).trans (sum_le_sum fun u hu ↦ ?_)
    exact addContent_mono hC (hC.inter_mem _ ht _ (h_ss hu)) (h_ss hu) inter_subset_right

Premises used: zero_le, Finset.sum_image_le_of_nonneg, and_imp, Set.mem_image, forall_exists_index, Finset.coe_image, Finset.sum_le_sum, LE.le.trans, Finset.mem_coe, rfl
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetSemiring C
m_subadd :
  ∀ (f : ℕ → Set α),
    (∀ (i : ℕ), f i ∈ C) →
      ⋃ (i : ℕ), f i ∈ C →
        ∀ (_hf_disj : Pairwise (Disjoint on f)),
          LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
            (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ (i : ℕ), f i ∈ C
hf_disj : Pairwise (Disjoint on f)
⊢ Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞) (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)

Tactic:
le_antisymm (m_subadd f hf hf_Union hf_disj) ?_

Premises used: le_antisymm
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetSemiring C
m_subadd :
  ∀ (f : ℕ → Set α),
    (∀ (i : ℕ), f i ∈ C) →
      ⋃ (i : ℕ), f i ∈ C →
        ∀ (_hf_disj : Pairwise (Disjoint on f)),
          LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
            (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ (i : ℕ), f i ∈ C
hf_disj : Pairwise (Disjoint on f)
refine :
  LE.le (α := ℝ≥0∞) (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞) (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)

Tactic:
refine le_antisymm (m_subadd f hf hf_Union hf_disj) ?_

Premises used: le_antisymm
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetSemiring C
m_subadd :
  ∀ (f : ℕ → Set α),
    (∀ (i : ℕ), f i ∈ C) →
      ⋃ (i : ℕ), f i ∈ C →
        ∀ (_hf_disj : Pairwise (Disjoint on f)),
          LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
            (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ (i : ℕ), f i ∈ C
hf_disj : Pairwise (Disjoint on f)
⊢ LE.le (α := ℝ≥0∞) (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)

Tactic:
ENNReal.summable.tsum_le_of_sum_le fun I ↦ ?_

Premises used: ENNReal.summable, Summable.tsum_le_of_sum_le
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetSemiring C
m_subadd :
  ∀ (f : ℕ → Set α),
    (∀ (i : ℕ), f i ∈ C) →
      ⋃ (i : ℕ), f i ∈ C →
        ∀ (_hf_disj : Pairwise (Disjoint on f)),
          LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
            (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ (i : ℕ), f i ∈ C
hf_disj : Pairwise (Disjoint on f)
refine :
  ∀ (I : Finset ℕ),
    LE.le (α := ℝ≥0∞) (∑ i ∈ I, (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
      ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)

Tactic:
refine ENNReal.summable.tsum_le_of_sum_le fun I ↦ ?_

Premises used: ENNReal.summable, Summable.tsum_le_of_sum_le
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetSemiring C
m_subadd :
  ∀ (f : ℕ → Set α),
    (∀ (i : ℕ), f i ∈ C) →
      ⋃ (i : ℕ), f i ∈ C →
        ∀ (_hf_disj : Pairwise (Disjoint on f)),
          LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
            (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ (i : ℕ), f i ∈ C
hf_disj : Pairwise (Disjoint on f)
I : Finset ℕ
rw :
  LE.le (α := ℝ≥0∞) (∑ s ∈ Finset.image f I, (m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (∑ i ∈ I, (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)

Tactic:
rw [← Finset.sum_image_of_disjoint addContent_empty (hf_disj.pairwiseDisjoint _)]

Premises used: Finset.sum_image_of_disjoint, Pairwise.pairwiseDisjoint
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetSemiring C
m_subadd :
  ∀ (f : ℕ → Set α),
    (∀ (i : ℕ), f i ∈ C) →
      ⋃ (i : ℕ), f i ∈ C →
        ∀ (_hf_disj : Pairwise (Disjoint on f)),
          LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
            (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ (i : ℕ), f i ∈ C
hf_disj : Pairwise (Disjoint on f)
I : Finset ℕ
⊢ LE.le (α := ℝ≥0∞) (∑ s ∈ Finset.image f I, (m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)

Tactic:
sum_addContent_le_of_subset hC (I := I.image f) ?_ ?_ hf_Union ?_

Premises used: MeasureTheory.sum_addContent_le_of_subset
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetSemiring C
m_subadd :
  ∀ (f : ℕ → Set α),
    (∀ (i : ℕ), f i ∈ C) →
      ⋃ (i : ℕ), f i ∈ C →
        ∀ (_hf_disj : Pairwise (Disjoint on f)),
          LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
            (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ (i : ℕ), f i ∈ C
hf_disj : Pairwise (Disjoint on f)
I : Finset ℕ
refine_1 : (↑(Finset.image f I) : Set (Set α)) ⊆ C
refine_2 : (↑(Finset.image f I) : Set (Set α)).PairwiseDisjoint id
refine_3 : ∀ s ∈ Finset.image f I, s ⊆ ⋃ (i : ℕ), f i
⊢ LE.le (α := ℝ≥0∞) (∑ s ∈ Finset.image f I, (m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)

Tactic:
refine sum_addContent_le_of_subset hC (I := I.image f) ?_ ?_ hf_Union ?_

Premises used: MeasureTheory.sum_addContent_le_of_subset
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetSemiring C
m_subadd :
  ∀ (f : ℕ → Set α),
    (∀ (i : ℕ), f i ∈ C) →
      ⋃ (i : ℕ), f i ∈ C →
        ∀ (_hf_disj : Pairwise (Disjoint on f)),
          LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
            (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ (i : ℕ), f i ∈ C
hf_disj : Pairwise (Disjoint on f)
I : Finset ℕ
refine_1 : (↑I : Set ℕ) ⊆ f ⁻¹' C
⊢ (↑(Finset.image f I) : Set (Set α)) ⊆ C

Tactic:
simp only [coe_image, Set.image_subset_iff]

Premises used: Finset.coe_image, Set.image_subset_iff
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetSemiring C
m_subadd :
  ∀ (f : ℕ → Set α),
    (∀ (i : ℕ), f i ∈ C) →
      ⋃ (i : ℕ), f i ∈ C →
        ∀ (_hf_disj : Pairwise (Disjoint on f)),
          LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
            (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ (i : ℕ), f i ∈ C
hf_disj : Pairwise (Disjoint on f)
I : Finset ℕ
⊢ (↑I : Set ℕ) ⊆ f ⁻¹' C

Tactic:
(subset_preimage_image f I).trans (preimage_mono ?_)

Premises used: HasSubset.Subset.trans, Set.preimage_mono, SetLike.coe, Set.subset_preimage_image
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetSemiring C
m_subadd :
  ∀ (f : ℕ → Set α),
    (∀ (i : ℕ), f i ∈ C) →
      ⋃ (i : ℕ), f i ∈ C →
        ∀ (_hf_disj : Pairwise (Disjoint on f)),
          LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
            (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ (i : ℕ), f i ∈ C
hf_disj : Pairwise (Disjoint on f)
I : Finset ℕ
refine_1 : f '' (↑I : Set ℕ) ⊆ C
⊢ (↑I : Set ℕ) ⊆ f ⁻¹' C

Tactic:
refine (subset_preimage_image f I).trans (preimage_mono ?_)

Premises used: HasSubset.Subset.trans, Set.preimage_mono, SetLike.coe, Set.subset_preimage_image
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetSemiring C
m_subadd :
  ∀ (f : ℕ → Set α),
    (∀ (i : ℕ), f i ∈ C) →
      ⋃ (i : ℕ), f i ∈ C →
        ∀ (_hf_disj : Pairwise (Disjoint on f)),
          LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
            (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ (i : ℕ), f i ∈ C
hf_disj : Pairwise (Disjoint on f)
I : Finset ℕ
j : ℕ
left : j ∈ (↑I : Set ℕ)
⊢ f j ∈ C

Tactic:
hf j
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetSemiring C
m_subadd :
  ∀ (f : ℕ → Set α),
    (∀ (i : ℕ), f i ∈ C) →
      ⋃ (i : ℕ), f i ∈ C →
        ∀ (_hf_disj : Pairwise (Disjoint on f)),
          LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
            (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ (i : ℕ), f i ∈ C
hf_disj : Pairwise (Disjoint on f)
I : Finset ℕ
j : ℕ
left : j ∈ (↑I : Set ℕ)
⊢ f j ∈ C

Tactic:
exact hf j
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetSemiring C
m_subadd :
  ∀ (f : ℕ → Set α),
    (∀ (i : ℕ), f i ∈ C) →
      ⋃ (i : ℕ), f i ∈ C →
        ∀ (_hf_disj : Pairwise (Disjoint on f)),
          LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
            (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ (i : ℕ), f i ∈ C
hf_disj : Pairwise (Disjoint on f)
I : Finset ℕ
refine_2 : (f '' (↑I : Set ℕ)).PairwiseDisjoint id
⊢ (↑(Finset.image f I) : Set (Set α)).PairwiseDisjoint id

Tactic:
simp only [coe_image]

Premises used: Finset.coe_image
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetSemiring C
m_subadd :
  ∀ (f : ℕ → Set α),
    (∀ (i : ℕ), f i ∈ C) →
      ⋃ (i : ℕ), f i ∈ C →
        ∀ (_hf_disj : Pairwise (Disjoint on f)),
          LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
            (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ (i : ℕ), f i ∈ C
hf_disj : Pairwise (Disjoint on f)
I : Finset ℕ
s : Set α
hs : s ∈ f '' (↑I : Set ℕ)
t : Set α
ht : t ∈ f '' (↑I : Set ℕ)
hst : s ≠ t
refine_2 :
  ∀ (hs : ∃ x ∈ (↑I : Set ℕ), f x = s) ⦃t : Set α⦄ (ht : ∃ x ∈ (↑I : Set ℕ), f x = t) (hst : s ≠ t),
    (Disjoint on id) s t
⊢ (Disjoint on id) s t

Tactic:
rw [Set.mem_image] at hs ht

Premises used: Set.mem_image
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetSemiring C
m_subadd :
  ∀ (f : ℕ → Set α),
    (∀ (i : ℕ), f i ∈ C) →
      ⋃ (i : ℕ), f i ∈ C →
        ∀ (_hf_disj : Pairwise (Disjoint on f)),
          LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
            (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ (i : ℕ), f i ∈ C
hf_disj : Pairwise (Disjoint on f)
I : Finset ℕ
s : Set α
hs : ∃ x ∈ (↑I : Set ℕ), f x = s
t : Set α
ht : ∃ x ∈ (↑I : Set ℕ), f x = t
hst : s ≠ t
refine_2 : ∀ i ∈ (↑I : Set ℕ), ∀ (hst : f i ≠ t), (Disjoint on id) (f i) t
⊢ (Disjoint on id) s t

Tactic:
obtain ⟨i, _, rfl⟩ := hs

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetSemiring C
m_subadd :
  ∀ (f : ℕ → Set α),
    (∀ (i : ℕ), f i ∈ C) →
      ⋃ (i : ℕ), f i ∈ C →
        ∀ (_hf_disj : Pairwise (Disjoint on f)),
          LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
            (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ (i : ℕ), f i ∈ C
hf_disj : Pairwise (Disjoint on f)
I : Finset ℕ
t : Set α
ht : ∃ x ∈ (↑I : Set ℕ), f x = t
i : ℕ
left : i ∈ (↑I : Set ℕ)
hst : f i ≠ t
refine_2 : ∀ j ∈ (↑I : Set ℕ), ∀ (hst : f i ≠ f j), (Disjoint on id) (f i) (f j)
⊢ (Disjoint on id) (f i) t

Tactic:
obtain ⟨j, _, rfl⟩ := ht

Premises used: rfl