awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
inst_1 : PartialOrder G
inst_2 : CanonicallyOrderedAdd G
hC : IsSetRing C
hs : s ∈ C
ht : t ∈ C
rw :
  HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) s : G) ((m : (a : Set α) → G) (t \ s) : G) ≤
    HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) s : G) ((m : (a : Set α) → G) t : G)
⊢ (m : (a : Set α) → G) (s ∪ t) ≤
    HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) s : G) ((m : (a : Set α) → G) t : G)
have rw₁ : Disjoint s (t \ s)
Tactic: rw [← union_diff_self, addContent_union hC hs (hC.diff_mem ht hs)]
-- 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
inst_1 : PartialOrder G
inst_2 : CanonicallyOrderedAdd G
hC : IsSetRing C
hs : s ∈ C
ht : t ∈ C
⊢ Disjoint s (t \ s)
have rw : s ∩ (t \ s) = ∅
Tactic: rw [Set.disjoint_iff_inter_eq_empty, inter_diff_self]
-- 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
inst_1 : PartialOrder G
inst_2 : CanonicallyOrderedAdd G
hC : IsSetRing C
hs : s ∈ C
ht : t ∈ C
rw : s ∩ (t \ s) = ∅
⊢ Disjoint s (t \ s)
have rw₁ : Eq.{u_1 + 1} (α := Set α) ∅ ∅
Tactic: rw [Set.disjoint_iff_inter_eq_empty, inter_diff_self]
-- 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
inst_1 : PartialOrder G
inst_2 : CanonicallyOrderedAdd G
ι : Type u_3
hC : IsSetRing C
s : ι → Set α
i : ι
S : Finset ι
hiS : i ∉ S
h :
  ∀ (hs : ∀ n ∈ S, s n ∈ C),
    LE.le.{u_2} (α := G) ((m : (a : Set α) → G) (⋃ i ∈ S, s i) : G) (∑ i ∈ S, (m : (a : Set α) → G) (s i) : G)
hs : ∀ n ∈ insert i S, s n ∈ C
⊢ LE.le.{u_2} (α := G) ((m : (a : Set α) → G) (⋃ i_1 ∈ insert i S, s i_1) : G)
    (∑ i ∈ insert i S, (m : (a : Set α) → G) (s i) : G)
have insert : (m : (a : Set α) → G) (⋃ i_1 ∈ insert i S, s i_1) ≤
  HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) (s i) : G) (∑ x ∈ S, (m : (a : Set α) → G) (s x) : G)
Tactic: rw [Finset.sum_insert hiS]
-- 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
inst_1 : PartialOrder G
inst_2 : CanonicallyOrderedAdd G
ι : Type u_3
hC : IsSetRing C
s : ι → Set α
i : ι
S : Finset ι
hiS : i ∉ S
h :
  ∀ (hs : ∀ n ∈ S, s n ∈ C),
    LE.le.{u_2} (α := G) ((m : (a : Set α) → G) (⋃ i ∈ S, s i) : G) (∑ i ∈ S, (m : (a : Set α) → G) (s i) : G)
hs : ∀ n ∈ insert i S, s n ∈ C
⊢ (m : (a : Set α) → G) (⋃ i_1 ∈ insert i S, s i_1) ≤
    HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) (s i) : G) (∑ x ∈ S, (m : (a : Set α) → G) (s x) : G)
have insert : (m : (a : Set α) → G) (s i ∪ ⋃ x ∈ (↑S : Set ι), s x) ≤
  HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) (s i) : G) (∑ x ∈ S, (m : (a : Set α) → G) (s x) : G)
Tactic: simp_rw [← Finset.mem_coe, Finset.coe_insert, Set.biUnion_insert]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (hypothesis)
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
inst_1 : PartialOrder G
inst_2 : CanonicallyOrderedAdd G
ι : Type u_3
hC : IsSetRing C
s : ι → Set α
i : ι
S : Finset ι
hiS : i ∉ S
h :
  ∀ (hs : ∀ n ∈ S, s n ∈ C),
    LE.le.{u_2} (α := G) ((m : (a : Set α) → G) (⋃ i ∈ S, s i) : G) (∑ i ∈ S, (m : (a : Set α) → G) (s i) : G)
hs : ∀ n ∈ insert i S, s n ∈ C
⊢ (m : (a : Set α) → G) (s i ∪ ⋃ x ∈ (↑S : Set ι), s x) ≤
    HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) (s i) : G) (∑ x ∈ S, (m : (a : Set α) → G) (s x) : G)
have hs₁ : s i ∈ C ∧ ∀ a ∈ S, s a ∈ C
Tactic: simp only [Finset.mem_insert, forall_eq_or_imp] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
inst_1 : PartialOrder G
inst_2 : CanonicallyOrderedAdd G
ι : Type u_3
hC : IsSetRing C
s : ι → Set α
i : ι
S : Finset ι
hiS : i ∉ S
h :
  ∀ (hs : ∀ n ∈ S, s n ∈ C),
    LE.le.{u_2} (α := G) ((m : (a : Set α) → G) (⋃ i ∈ S, s i) : G) (∑ i ∈ S, (m : (a : Set α) → G) (s i) : G)
hs : s i ∈ C ∧ ∀ a ∈ S, s a ∈ C
⊢ (m : (a : Set α) → G) (s i ∪ ⋃ x ∈ (↑S : Set ι), s x) ≤
    HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) (s i) : G) (∑ x ∈ S, (m : (a : Set α) → G) (s x) : G)
have insert : HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) (s i) : G) ((m : (a : Set α) → G) (⋃ i ∈ S, s i) : G) ≤
  HAdd.hAdd (α := G) (β := G) ((m : (a : Set α) → G) (s i) : G) (∑ x ∈ S, (m : (a : Set α) → G) (s x) : G)
Tactic: refine (addContent_union_le hC hs.1 (hC.biUnion_mem S hs.2)).trans ?_
-- 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
inst_1 : PartialOrder G
inst_2 : CanonicallyOrderedAdd G
ι : Type u_3
hC : IsSetRing C
s : ι → Set α
S : Finset ι
hs : ∀ n ∈ S, s n ∈ C
⊢ LE.le.{u_2} (α := G) ((m : (a : Set α) → G) (⋃ i ∈ S, s i) : G) (∑ i ∈ S, (m : (a : Set α) → G) (s i) : G)
have empty : ∀ (hs : ∀ (n : ι), Membership.mem (γ := Finset ι) ∅ n → s n ∈ C),
  LE.le.{u_2} (α := G) ((m : (a : Set α) → G) (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), s i) : G)
    (∑ i ∈ ∅, (m : (a : Set α) → G) (s i) : G)
Tactic: induction S using Finset.induction with
  | empty => simp
  | insert i S hiS h =>
    rw [Finset.sum_insert hiS]
    simp_rw [← Finset.mem_coe, Finset.coe_insert, Set.biUnion_insert]
    simp only [Finset.mem_insert, forall_eq_or_imp] at hs
    refine (addContent_union_le hC hs.1 (hC.biUnion_mem S hs.2)).trans ?_
    exact add_le_add le_rfl (h hs.2)
Cleared hypotheses: S, hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
inst_1 : PartialOrder G
inst_2 : CanonicallyOrderedAdd G
ι : Type u_3
hC : IsSetRing C
s : ι → Set α
S : Finset ι
hs : ∀ n ∈ S, s n ∈ C
empty :
  ∀ (hs : ∀ (n : ι), Membership.mem (γ := Finset ι) ∅ n → s n ∈ C),
    LE.le.{u_2} (α := G) ((m : (a : Set α) → G) (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), s i) : G)
      (∑ i ∈ ∅, (m : (a : Set α) → G) (s i) : G)
⊢ LE.le.{u_2} (α := G) ((m : (a : Set α) → G) (⋃ i ∈ S, s i) : G) (∑ i ∈ S, (m : (a : Set α) → G) (s i) : G)
have insert : ∀ (i : ι) (S : Finset ι) (hiS : i ∉ S)
  (h :
    ∀ (hs : ∀ n ∈ S, s n ∈ C),
      LE.le.{u_2} (α := G) ((m : (a : Set α) → G) (⋃ i ∈ S, s i) : G) (∑ i ∈ S, (m : (a : Set α) → G) (s i) : G))
  (hs : ∀ n ∈ insert i S, s n ∈ C),
  LE.le.{u_2} (α := G) ((m : (a : Set α) → G) (⋃ i_1 ∈ insert i S, s i_1) : G)
    (∑ i ∈ insert i S, (m : (a : Set α) → G) (s i) : G)
Tactic: induction S using Finset.induction with
  | empty => simp
  | insert i S hiS h =>
    rw [Finset.sum_insert hiS]
    simp_rw [← Finset.mem_coe, Finset.coe_insert, Set.biUnion_insert]
    simp only [Finset.mem_insert, forall_eq_or_imp] at hs
    refine (addContent_union_le hC hs.1 (hC.biUnion_mem S hs.2)).trans ?_
    exact add_le_add le_rfl (h hs.2)
Cleared hypotheses: S, hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
inst_1 : PartialOrder G
inst_2 : CanonicallyOrderedAdd G
ι : Type u_3
hC : IsSetRing C
s : ι → Set α
S : Finset ι
hs : ∀ n ∈ S, s n ∈ C
⊢ LE.le.{u_2} (α := G) ((m : (a : Set α) → G) (⋃ i ∈ S, s i) : G) (∑ i ∈ S, (m : (a : Set α) → G) (s i) : G)
have empty : ∀ (hs : ∀ (n : ι), Membership.mem (γ := Finset ι) ∅ n → s n ∈ C),
  LE.le.{u_2} (α := G) ((m : (a : Set α) → G) (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), s i) : G)
    (∑ i ∈ ∅, (m : (a : Set α) → G) (s i) : G)
Tactic: classical
  induction S using Finset.induction with
  | empty => simp
  | insert i S hiS h =>
    rw [Finset.sum_insert hiS]
    simp_rw [← Finset.mem_coe, Finset.coe_insert, Set.biUnion_insert]
    simp only [Finset.mem_insert, forall_eq_or_imp] at hs
    refine (addContent_union_le hC hs.1 (hC.biUnion_mem S hs.2)).trans ?_
    exact add_le_add le_rfl (h hs.2)
Cleared hypotheses: S, hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
inst_1 : PartialOrder G
inst_2 : CanonicallyOrderedAdd G
ι : Type u_3
hC : IsSetRing C
s : ι → Set α
S : Finset ι
hs : ∀ n ∈ S, s n ∈ C
empty :
  ∀ (hs : ∀ (n : ι), Membership.mem (γ := Finset ι) ∅ n → s n ∈ C),
    LE.le.{u_2} (α := G) ((m : (a : Set α) → G) (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), s i) : G)
      (∑ i ∈ ∅, (m : (a : Set α) → G) (s i) : G)
⊢ LE.le.{u_2} (α := G) ((m : (a : Set α) → G) (⋃ i ∈ S, s i) : G) (∑ i ∈ S, (m : (a : Set α) → G) (s i) : G)
have insert : ∀ (i : ι) (S : Finset ι) (hiS : i ∉ S)
  (h :
    ∀ (hs : ∀ n ∈ S, s n ∈ C),
      LE.le.{u_2} (α := G) ((m : (a : Set α) → G) (⋃ i ∈ S, s i) : G) (∑ i ∈ S, (m : (a : Set α) → G) (s i) : G))
  (hs : ∀ n ∈ insert i S, s n ∈ C),
  LE.le.{u_2} (α := G) ((m : (a : Set α) → G) (⋃ i_1 ∈ insert i S, s i_1) : G)
    (∑ i ∈ insert i S, (m : (a : Set α) → G) (s i) : G)
Tactic: classical
  induction S using Finset.induction with
  | empty => simp
  | insert i S hiS h =>
    rw [Finset.sum_insert hiS]
    simp_rw [← Finset.mem_coe, Finset.coe_insert, Set.biUnion_insert]
    simp only [Finset.mem_insert, forall_eq_or_imp] at hs
    refine (addContent_union_le hC hs.1 (hC.biUnion_mem S hs.2)).trans ?_
    exact add_le_add le_rfl (h hs.2)
Cleared hypotheses: S, hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent ℝ≥0∞ C
hC : IsSetRing C
hs : s ∈ C
ht : t ∈ C
| HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have rw : HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (s ∩ t ∪ s \ t) : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [← inter_union_diff s t]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent ℝ≥0∞ C
hC : IsSetRing C
hs : s ∈ C
ht : t ∈ C
⊢ HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ≤
    (m : (a : Set α) → ℝ≥0∞) (s \ t)
have conv_lhs : HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (s ∩ t ∪ s \ t) : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ≤
  (m : (a : Set α) → ℝ≥0∞) (s \ t)
Tactic: conv_lhs => rw [← inter_union_diff s t]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent ℝ≥0∞ C
hC : IsSetRing C
hs : s ∈ C
ht : t ∈ C
⊢ HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (s ∩ t ∪ s \ t) : ℝ≥0∞)
      ((m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ≤
    (m : (a : Set α) → ℝ≥0∞) (s \ t)
have rw : HSub.hSub (β := ℝ≥0∞)
    (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞)
      ((m : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞))
    ((m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ≤
  (m : (a : Set α) → ℝ≥0∞) (s \ t)
Tactic: rw [addContent_union hC (hC.inter_mem hs ht) (hC.diff_mem hs ht) disjoint_inf_sdiff, add_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent ℝ≥0∞ C
hC : IsSetRing C
hs : s ∈ C
ht : t ∈ C
⊢ HSub.hSub (β := ℝ≥0∞)
      (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞)
        ((m : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞))
      ((m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ≤
    (m : (a : Set α) → ℝ≥0∞) (s \ t)
have refine : HAdd.hAdd (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞)
    (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)) =
  (m : (a : Set α) → ℝ≥0∞) (s \ t)
Tactic: refine add_tsub_le_assoc.trans_eq ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent ℝ≥0∞ C
hC : IsSetRing C
hs : s ∈ C
ht : t ∈ C
⊢ HAdd.hAdd (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞)
      (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
        ((m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)) =
    (m : (a : Set α) → ℝ≥0∞) (s \ t)
have rw : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) (0 : ℝ≥0∞) =
  (m : (a : Set α) → ℝ≥0∞) (s \ t)
Tactic: rw [tsub_eq_zero_of_le
    (addContent_mono hC.isSetSemiring (hC.inter_mem hs ht) ht inter_subset_right), add_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent ℝ≥0∞ C
hC : IsSetRing C
hs : s ∈ C
ht : t ∈ C
rw :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) (0 : ℝ≥0∞) =
    (m : (a : Set α) → ℝ≥0∞) (s \ t)
⊢ HAdd.hAdd (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞)
      (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
        ((m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)) =
    (m : (a : Set α) → ℝ≥0∞) (s \ t)
have rw₁ : Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞)
Tactic: rw [tsub_eq_zero_of_le
    (addContent_mono hC.isSetSemiring (hC.inter_mem hs ht) ht inter_subset_right), add_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (hypothesis)
Goal:
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetRing C
hm_ne_top : ∀ s ∈ C, Ne (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
s t : Set α
hs : s ∈ C
ht : t ∈ C
hts : t ⊆ s
⊢ (m : (a : Set α) → ℝ≥0∞) (s \ t) =
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have h_union : (m : (a : Set α) → ℝ≥0∞) (t ∪ s \ t) =
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞)
Tactic: have h_union : m (t ∪ s \ t) = m t + m (s \ t) :=
    addContent_union hC ht (hC.diff_mem hs ht) disjoint_sdiff_self_right
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (hypothesis)
Goal:
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetRing C
hm_ne_top : ∀ s ∈ C, Ne (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
s t : Set α
hs : s ∈ C
ht : t ∈ C
hts : t ⊆ s
h_union :
  (m : (a : Set α) → ℝ≥0∞) (t ∪ s \ t) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞)
⊢ (m : (a : Set α) → ℝ≥0∞) (s \ t) =
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have h_union₁ : (m : (a : Set α) → ℝ≥0∞) s =
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞)
Tactic: simp_rw [Set.union_diff_self, Set.union_eq_right.mpr hts] at h_union
Cleared hypotheses: h_union
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetRing C
hm_ne_top : ∀ s ∈ C, Ne (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
s t : Set α
hs : s ∈ C
ht : t ∈ C
hts : t ⊆ s
h_union :
  (m : (a : Set α) → ℝ≥0∞) s =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞)
⊢ (m : (a : Set α) → ℝ≥0∞) (s \ t) =
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have rw : (m : (a : Set α) → ℝ≥0∞) (s \ t) =
  HSub.hSub (β := ℝ≥0∞)
    (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞))
    ((m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [h_union, ENNReal.add_sub_cancel_left (hm_ne_top _ ht)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetRing C
hm_ne_top : ∀ s ∈ C, Ne (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
s t : Set α
hs : s ∈ C
ht : t ∈ C
hts : t ⊆ s
h_union :
  (m : (a : Set α) → ℝ≥0∞) s =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞)
rw :
  (m : (a : Set α) → ℝ≥0∞) (s \ t) =
    HSub.hSub (β := ℝ≥0∞)
      (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞))
      ((m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ (m : (a : Set α) → ℝ≥0∞) (s \ t) =
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞)
Tactic: rw [h_union, ENNReal.add_sub_cancel_left (hm_ne_top _ ht)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (hypothesis)
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
m : AddContent ℝ≥0∞ C
hm_ne_top : ∀ s ∈ C, Ne (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hm_tendsto :
  ∀ ⦃s : ℕ → Set α⦄,
    (∀ (n : ℕ), s n ∈ C) →
      Antitone s →
        Eq.{u_1 + 1} (α := Set α) (⋂ (n : ℕ), s n) ∅ →
          Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (m : (a : Set α) → ℝ≥0∞) (s n)) atTop (𝓝 0)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hUf : ⋃ (i : ℕ), f i ∈ C
h_disj : Pairwise (Disjoint on f)
s : ℕ → Set α := fun (n : ℕ) ↦ (⋃ (i : ℕ), f i) \ accumulate f n
⊢ Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞) (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
have hCs : ∀ (n : ℕ), s n ∈ C
Tactic: have hCs n : s n ∈ C := hC.diff_mem hUf (hC.accumulate_mem hf n)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
m : AddContent ℝ≥0∞ C
hm_ne_top : ∀ s ∈ C, Ne (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hm_tendsto :
  ∀ ⦃s : ℕ → Set α⦄,
    (∀ (n : ℕ), s n ∈ C) →
      Antitone s →
        Eq.{u_1 + 1} (α := Set α) (⋂ (n : ℕ), s n) ∅ →
          Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (m : (a : Set α) → ℝ≥0∞) (s n)) atTop (𝓝 0)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hUf : ⋃ (i : ℕ), f i ∈ C
h_disj : Pairwise (Disjoint on f)
s : ℕ → Set α := fun (n : ℕ) ↦ (⋃ (i : ℕ), f i) \ accumulate f n
hCs : ∀ (n : ℕ), s n ∈ C
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (m : (a : Set α) → ℝ≥0∞) (s n)) atTop (𝓝 0)
have refine_1 : Antitone s
Tactic: refine hm_tendsto hCs ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
m : AddContent ℝ≥0∞ C
hm_ne_top : ∀ s ∈ C, Ne (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hm_tendsto :
  ∀ ⦃s : ℕ → Set α⦄,
    (∀ (n : ℕ), s n ∈ C) →
      Antitone s →
        Eq.{u_1 + 1} (α := Set α) (⋂ (n : ℕ), s n) ∅ →
          Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (m : (a : Set α) → ℝ≥0∞) (s n)) atTop (𝓝 0)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hUf : ⋃ (i : ℕ), f i ∈ C
h_disj : Pairwise (Disjoint on f)
s : ℕ → Set α := fun (n : ℕ) ↦ (⋃ (i : ℕ), f i) \ accumulate f n
hCs : ∀ (n : ℕ), s n ∈ C
refine_1 : Antitone s
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (m : (a : Set α) → ℝ≥0∞) (s n)) atTop (𝓝 0)
have refine_2 : Eq.{u_1 + 1} (α := Set α) (⋂ (n : ℕ), s n) ∅
Tactic: refine hm_tendsto hCs ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
m : AddContent ℝ≥0∞ C
hm_ne_top : ∀ s ∈ C, Ne (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hm_tendsto :
  ∀ ⦃s : ℕ → Set α⦄,
    (∀ (n : ℕ), s n ∈ C) →
      Antitone s →
        Eq.{u_1 + 1} (α := Set α) (⋂ (n : ℕ), s n) ∅ →
          Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (m : (a : Set α) → ℝ≥0∞) (s n)) atTop (𝓝 0)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hUf : ⋃ (i : ℕ), f i ∈ C
h_disj : Pairwise (Disjoint on f)
s : ℕ → Set α := fun (n : ℕ) ↦ (⋃ (i : ℕ), f i) \ accumulate f n
hCs : ∀ (n : ℕ), s n ∈ C
i j : ℕ
hij : i ≤ j
x : α
hxj : x ∈ s j
⊢ x ∈ s i
have refine_1 : ∀ (hxj : Membership.mem (γ := Set α) (⋃ (i : ℕ), f i) x ∧ x ∉ accumulate f j),
  Membership.mem (γ := Set α) (⋃ (i : ℕ), f i) x ∧ x ∉ accumulate f i
Tactic: rw [Set.mem_diff] at hxj ⊢
Cleared hypotheses: hxj
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
m : AddContent ℝ≥0∞ C
hm_ne_top : ∀ s ∈ C, Ne (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hm_tendsto :
  ∀ ⦃s : ℕ → Set α⦄,
    (∀ (n : ℕ), s n ∈ C) →
      Antitone s →
        Eq.{u_1 + 1} (α := Set α) (⋂ (n : ℕ), s n) ∅ →
          Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (m : (a : Set α) → ℝ≥0∞) (s n)) atTop (𝓝 0)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hUf : ⋃ (i : ℕ), f i ∈ C
h_disj : Pairwise (Disjoint on f)
s : ℕ → Set α := fun (n : ℕ) ↦ (⋃ (i : ℕ), f i) \ accumulate f n
hCs : ∀ (n : ℕ), s n ∈ C
⊢ Eq.{u_1 + 1} (α := Set α) (⋂ (n : ℕ), s n) ∅
have refine_2 : Eq.{u_1 + 1} (α := Set α) (⋂ (n : ℕ), (⋃ (i : ℕ), f i) ∩ (accumulate f n)ᶜ) ∅
Tactic: simp_rw [s, Set.diff_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
m : AddContent ℝ≥0∞ C
hm_ne_top : ∀ s ∈ C, Ne (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hm_tendsto :
  ∀ ⦃s : ℕ → Set α⦄,
    (∀ (n : ℕ), s n ∈ C) →
      Antitone s →
        Eq.{u_1 + 1} (α := Set α) (⋂ (n : ℕ), s n) ∅ →
          Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (m : (a : Set α) → ℝ≥0∞) (s n)) atTop (𝓝 0)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hUf : ⋃ (i : ℕ), f i ∈ C
h_disj : Pairwise (Disjoint on f)
s : ℕ → Set α := fun (n : ℕ) ↦ (⋃ (i : ℕ), f i) \ accumulate f n
hCs : ∀ (n : ℕ), s n ∈ C
⊢ Eq.{u_1 + 1} (α := Set α) (⋂ (n : ℕ), (⋃ (i : ℕ), f i) ∩ (accumulate f n)ᶜ) ∅
have refine_2 : Eq.{u_1 + 1} (α := Set α) ((⋃ (i : ℕ), f i) ∩ (⋃ (x : ℕ), f x)ᶜ) ∅
Tactic: rw [Set.iInter_inter_distrib, Set.iInter_const, ← Set.compl_iUnion, Set.iUnion_accumulate]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (hypothesis)
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
m : AddContent ℝ≥0∞ C
hm_ne_top : ∀ s ∈ C, Ne (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hm_tendsto :
  ∀ ⦃s : ℕ → Set α⦄,
    (∀ (n : ℕ), s n ∈ C) →
      Antitone s →
        Eq.{u_1 + 1} (α := Set α) (⋂ (n : ℕ), s n) ∅ →
          Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (m : (a : Set α) → ℝ≥0∞) (s n)) atTop (𝓝 0)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hUf : ⋃ (i : ℕ), f i ∈ C
h_disj : Pairwise (Disjoint on f)
s : ℕ → Set α := fun (n : ℕ) ↦ (⋃ (i : ℕ), f i) \ accumulate f n
hCs : ∀ (n : ℕ), s n ∈ C
⊢ Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞) (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
have h_tendsto : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (m : (a : Set α) → ℝ≥0∞) (s n)) atTop (𝓝 0)
Tactic: have h_tendsto : Tendsto (fun n ↦ m (s n)) atTop (𝓝 0) := by
    refine hm_tendsto hCs ?_ ?_
    · intro i j hij x hxj
      rw [Set.mem_diff] at hxj ⊢
      exact ⟨hxj.1, fun hxi ↦ hxj.2 (Set.monotone_accumulate hij hxi)⟩
    · simp_rw [s, Set.diff_eq]
      rw [Set.iInter_inter_distrib, Set.iInter_const, ← Set.compl_iUnion, Set.iUnion_accumulate]
      exact Set.inter_compl_self _