awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t' : ℕ → Set α
ht' : s ⊆ iUnion t'
t : Set α :=
  ⋃ (n : ℕ),
    ⋃ (_ :
      Membership.mem (γ := Set ℕ)
        {k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
        n),
      t' n
ht :
  t =
    ⋃ (n : ℕ),
      ⋃ (_ :
        Membership.mem (γ := Set ℕ)
          {k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
          n),
        t' n
hle₁ :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
    (∑' (n :
        (↑{k : ℕ |
              LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} :
          Type)),
        (μ : (a : Set α) → ℝ≥0∞) (t' (↑n : ℕ)) :
      ℝ≥0∞)
hcap :
  tᶜ ∩ s ⊆
    ⋃ (n : ℕ),
      ⋃ (_ :
        Membership.mem (γ := Set ℕ)
          {k : ℕ | LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
          n),
        t' n
hle₂ :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (tᶜ ∩ s) : ℝ≥0∞)
    (∑' (n :
        (↑{k : ℕ |
              LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} :
          Type)),
        (ν : (a : Set α) → ℝ≥0∞) (t' (↑n : ℕ)) :
      ℝ≥0∞)
⊢ Eq (α := Set ℕ)
    ({k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} ∪
      {k : ℕ | LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)})
    univ
have h : ∀ (k : ℕ),
  Membership.mem (γ := Set ℕ)
      ({k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} ∪
        {k : ℕ | LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)})
      k ↔
    Membership.mem (γ := Set ℕ) univ k
Tactic: ext k
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t' : ℕ → Set α
ht' : s ⊆ iUnion t'
t : Set α :=
  ⋃ (n : ℕ),
    ⋃ (_ :
      Membership.mem (γ := Set ℕ)
        {k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
        n),
      t' n
ht :
  t =
    ⋃ (n : ℕ),
      ⋃ (_ :
        Membership.mem (γ := Set ℕ)
          {k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
          n),
        t' n
hle₁ :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
    (∑' (n :
        (↑{k : ℕ |
              LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} :
          Type)),
        (μ : (a : Set α) → ℝ≥0∞) (t' (↑n : ℕ)) :
      ℝ≥0∞)
hcap :
  tᶜ ∩ s ⊆
    ⋃ (n : ℕ),
      ⋃ (_ :
        Membership.mem (γ := Set ℕ)
          {k : ℕ | LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
          n),
        t' n
hle₂ :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (tᶜ ∩ s) : ℝ≥0∞)
    (∑' (n :
        (↑{k : ℕ |
              LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} :
          Type)),
        (ν : (a : Set α) → ℝ≥0∞) (t' (↑n : ℕ)) :
      ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞)
      (∑' (n :
        (↑{k : ℕ |
              LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} :
          Type)),
        (μ : (a : Set α) → ℝ≥0∞) (t' (↑n : ℕ)))
      (∑' (n :
        (↑{k : ℕ |
              LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} :
          Type)),
        (ν : (a : Set α) → ℝ≥0∞) (t' (↑n : ℕ))) ≤
    ∑' (n : ℕ), min ((μ : (a : Set α) → ℝ≥0∞) (t' n)) ((ν : (a : Set α) → ℝ≥0∞) (t' n))
have heq : Eq (α := Set ℕ)
  ({k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} ∪
    {k : ℕ | LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)})
  univ
Tactic: have heq : {k | μ (t' k) ≤ ν (t' k)} ∪ {k | ν (t' k) < μ (t' k)} = univ := by
      ext k; simp [le_or_gt]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t' : ℕ → Set α
ht' : s ⊆ iUnion t'
t : Set α :=
  ⋃ (n : ℕ),
    ⋃ (_ :
      Membership.mem (γ := Set ℕ)
        {k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
        n),
      t' n
ht :
  t =
    ⋃ (n : ℕ),
      ⋃ (_ :
        Membership.mem (γ := Set ℕ)
          {k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
          n),
        t' n
hle₁ :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
    (∑' (n :
        (↑{k : ℕ |
              LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} :
          Type)),
        (μ : (a : Set α) → ℝ≥0∞) (t' (↑n : ℕ)) :
      ℝ≥0∞)
hcap :
  tᶜ ∩ s ⊆
    ⋃ (n : ℕ),
      ⋃ (_ :
        Membership.mem (γ := Set ℕ)
          {k : ℕ | LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
          n),
        t' n
hle₂ :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (tᶜ ∩ s) : ℝ≥0∞)
    (∑' (n :
        (↑{k : ℕ |
              LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} :
          Type)),
        (ν : (a : Set α) → ℝ≥0∞) (t' (↑n : ℕ)) :
      ℝ≥0∞)
heq :
  Eq (α := Set ℕ)
    ({k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} ∪
      {k : ℕ | LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)})
    univ
| ∑' (n : ℕ), min ((μ : (a : Set α) → ℝ≥0∞) (t' n)) ((ν : (a : Set α) → ℝ≥0∞) (t' n))
have rw : ∑' (x :
  (↑({k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} ∪
        {k : ℕ | LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}) :
    Type)),
  min ((μ : (a : Set α) → ℝ≥0∞) (t' (↑x : ℕ))) ((ν : (a : Set α) → ℝ≥0∞) (t' (↑x : ℕ)))
Tactic: rw [← tsum_univ, ← heq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t' : ℕ → Set α
ht' : s ⊆ iUnion t'
t : Set α :=
  ⋃ (n : ℕ),
    ⋃ (_ :
      Membership.mem (γ := Set ℕ)
        {k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
        n),
      t' n
ht :
  t =
    ⋃ (n : ℕ),
      ⋃ (_ :
        Membership.mem (γ := Set ℕ)
          {k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
          n),
        t' n
hle₁ :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
    (∑' (n :
        (↑{k : ℕ |
              LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} :
          Type)),
        (μ : (a : Set α) → ℝ≥0∞) (t' (↑n : ℕ)) :
      ℝ≥0∞)
hcap :
  tᶜ ∩ s ⊆
    ⋃ (n : ℕ),
      ⋃ (_ :
        Membership.mem (γ := Set ℕ)
          {k : ℕ | LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
          n),
        t' n
hle₂ :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (tᶜ ∩ s) : ℝ≥0∞)
    (∑' (n :
        (↑{k : ℕ |
              LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} :
          Type)),
        (ν : (a : Set α) → ℝ≥0∞) (t' (↑n : ℕ)) :
      ℝ≥0∞)
heq :
  Eq (α := Set ℕ)
    ({k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} ∪
      {k : ℕ | LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)})
    univ
⊢ HAdd.hAdd (α := ℝ≥0∞)
      (∑' (n :
        (↑{k : ℕ |
              LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} :
          Type)),
        (μ : (a : Set α) → ℝ≥0∞) (t' (↑n : ℕ)))
      (∑' (n :
        (↑{k : ℕ |
              LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} :
          Type)),
        (ν : (a : Set α) → ℝ≥0∞) (t' (↑n : ℕ))) ≤
    ∑' (n : ℕ), min ((μ : (a : Set α) → ℝ≥0∞) (t' n)) ((ν : (a : Set α) → ℝ≥0∞) (t' n))
have refine_2 : HAdd.hAdd (α := ℝ≥0∞)
    (∑' (n :
      (↑{k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} :
        Type)),
      (μ : (a : Set α) → ℝ≥0∞) (t' (↑n : ℕ)))
    (∑' (n :
      (↑{k : ℕ | LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} :
        Type)),
      (ν : (a : Set α) → ℝ≥0∞) (t' (↑n : ℕ))) ≤
  ∑' (x :
    (↑({k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} ∪
          {k : ℕ |
            LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}) :
      Type)),
    min ((μ : (a : Set α) → ℝ≥0∞) (t' (↑x : ℕ))) ((ν : (a : Set α) → ℝ≥0∞) (t' (↑x : ℕ)))
Tactic: conv in ∑' (n : ℕ), μ (t' n) ⊓ ν (t' n) => rw [← tsum_univ, ← heq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t' : ℕ → Set α
ht' : s ⊆ iUnion t'
t : Set α :=
  ⋃ (n : ℕ),
    ⋃ (_ :
      Membership.mem (γ := Set ℕ)
        {k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
        n),
      t' n
ht :
  t =
    ⋃ (n : ℕ),
      ⋃ (_ :
        Membership.mem (γ := Set ℕ)
          {k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
          n),
        t' n
hle₁ :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
    (∑' (n :
        (↑{k : ℕ |
              LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} :
          Type)),
        (μ : (a : Set α) → ℝ≥0∞) (t' (↑n : ℕ)) :
      ℝ≥0∞)
hcap :
  tᶜ ∩ s ⊆
    ⋃ (n : ℕ),
      ⋃ (_ :
        Membership.mem (γ := Set ℕ)
          {k : ℕ | LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
          n),
        t' n
hle₂ :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (tᶜ ∩ s) : ℝ≥0∞)
    (∑' (n :
        (↑{k : ℕ |
              LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} :
          Type)),
        (ν : (a : Set α) → ℝ≥0∞) (t' (↑n : ℕ)) :
      ℝ≥0∞)
heq :
  Eq (α := Set ℕ)
    ({k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} ∪
      {k : ℕ | LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)})
    univ
⊢ HAdd.hAdd (α := ℝ≥0∞)
      (∑' (n :
        (↑{k : ℕ |
              LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} :
          Type)),
        (μ : (a : Set α) → ℝ≥0∞) (t' (↑n : ℕ)))
      (∑' (n :
        (↑{k : ℕ |
              LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} :
          Type)),
        (ν : (a : Set α) → ℝ≥0∞) (t' (↑n : ℕ))) ≤
    HAdd.hAdd (α := ℝ≥0∞)
      (∑' (x :
        (↑{k : ℕ |
              LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} :
          Type)),
        min ((μ : (a : Set α) → ℝ≥0∞) (t' (↑x : ℕ))) ((ν : (a : Set α) → ℝ≥0∞) (t' (↑x : ℕ))))
      (∑' (x :
        (↑{k : ℕ |
              LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} :
          Type)),
        min ((μ : (a : Set α) → ℝ≥0∞) (t' (↑x : ℕ))) ((ν : (a : Set α) → ℝ≥0∞) (t' (↑x : ℕ))))
have refine_2 : ∀
  (b :
    (↑{k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} :
      Type)),
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' (↑b : ℕ)) : ℝ≥0∞)
    (min ((μ : (a : Set α) → ℝ≥0∞) (t' (↑b : ℕ))) ((ν : (a : Set α) → ℝ≥0∞) (t' (↑b : ℕ))) : ℝ≥0∞)
Tactic: refine add_le_add (tsum_congr ?_).le (tsum_congr ?_).le
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t' : ℕ → Set α
ht' : s ⊆ iUnion t'
t : Set α :=
  ⋃ (n : ℕ),
    ⋃ (_ :
      Membership.mem (γ := Set ℕ)
        {k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
        n),
      t' n
ht :
  t =
    ⋃ (n : ℕ),
      ⋃ (_ :
        Membership.mem (γ := Set ℕ)
          {k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
          n),
        t' n
hle₁ :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
    (∑' (n :
        (↑{k : ℕ |
              LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} :
          Type)),
        (μ : (a : Set α) → ℝ≥0∞) (t' (↑n : ℕ)) :
      ℝ≥0∞)
hcap :
  tᶜ ∩ s ⊆
    ⋃ (n : ℕ),
      ⋃ (_ :
        Membership.mem (γ := Set ℕ)
          {k : ℕ | LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
          n),
        t' n
hle₂ :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (tᶜ ∩ s) : ℝ≥0∞)
    (∑' (n :
        (↑{k : ℕ |
              LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} :
          Type)),
        (ν : (a : Set α) → ℝ≥0∞) (t' (↑n : ℕ)) :
      ℝ≥0∞)
heq :
  Eq (α := Set ℕ)
    ({k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} ∪
      {k : ℕ | LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)})
    univ
n : ℕ
hn :
  Membership.mem (γ := Set ℕ)
    {k : ℕ | LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} n
⊢ Eq (α := ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞)
        (t'
          (↑(Subtype.mk (p := fun (a : ℕ) ↦
                Membership.mem (γ := Set ℕ)
                  {k : ℕ |
                    LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
                  a)
                n hn) :
            ℕ)) :
      ℝ≥0∞)
    (min
        ((μ : (a : Set α) → ℝ≥0∞)
          (t'
            (↑(Subtype.mk (p := fun (a : ℕ) ↦
                  Membership.mem (γ := Set ℕ)
                    {k : ℕ |
                      LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)
                        ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
                    a)
                  n hn) :
              ℕ)))
        ((ν : (a : Set α) → ℝ≥0∞)
          (t'
            (↑(Subtype.mk (p := fun (a : ℕ) ↦
                  Membership.mem (γ := Set ℕ)
                    {k : ℕ |
                      LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)
                        ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
                    a)
                  n hn) :
              ℕ))) :
      ℝ≥0∞)
have hn₁ : LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' n) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' n) : ℝ≥0∞)
Tactic: rw [mem_setOf_eq] at hn
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t' : ℕ → Set α
ht' : s ⊆ iUnion t'
t : Set α :=
  ⋃ (n : ℕ),
    ⋃ (_ :
      Membership.mem (γ := Set ℕ)
        {k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
        n),
      t' n
ht :
  t =
    ⋃ (n : ℕ),
      ⋃ (_ :
        Membership.mem (γ := Set ℕ)
          {k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
          n),
        t' n
hle₁ :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
    (∑' (n :
        (↑{k : ℕ |
              LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} :
          Type)),
        (μ : (a : Set α) → ℝ≥0∞) (t' (↑n : ℕ)) :
      ℝ≥0∞)
hcap :
  tᶜ ∩ s ⊆
    ⋃ (n : ℕ),
      ⋃ (_ :
        Membership.mem (γ := Set ℕ)
          {k : ℕ | LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
          n),
        t' n
hle₂ :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (tᶜ ∩ s) : ℝ≥0∞)
    (∑' (n :
        (↑{k : ℕ |
              LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} :
          Type)),
        (ν : (a : Set α) → ℝ≥0∞) (t' (↑n : ℕ)) :
      ℝ≥0∞)
heq :
  Eq (α := Set ℕ)
    ({k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} ∪
      {k : ℕ | LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)})
    univ
⊢ Disjoint (α := Set ℕ)
    {k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
    {k : ℕ | LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
have rw : Subset (α := Set ℕ)
  ({k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} ∩
    {k : ℕ | LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)})
  ∅
Tactic: rw [Set.disjoint_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t' : ℕ → Set α
ht' : s ⊆ iUnion t'
t : Set α :=
  ⋃ (n : ℕ),
    ⋃ (_ :
      Membership.mem (γ := Set ℕ)
        {k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
        n),
      t' n
ht :
  t =
    ⋃ (n : ℕ),
      ⋃ (_ :
        Membership.mem (γ := Set ℕ)
          {k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
          n),
        t' n
hle₁ :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
    (∑' (n :
        (↑{k : ℕ |
              LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} :
          Type)),
        (μ : (a : Set α) → ℝ≥0∞) (t' (↑n : ℕ)) :
      ℝ≥0∞)
hcap :
  tᶜ ∩ s ⊆
    ⋃ (n : ℕ),
      ⋃ (_ :
        Membership.mem (γ := Set ℕ)
          {k : ℕ | LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
          n),
        t' n
hle₂ :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (tᶜ ∩ s) : ℝ≥0∞)
    (∑' (n :
        (↑{k : ℕ |
              LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} :
          Type)),
        (ν : (a : Set α) → ℝ≥0∞) (t' (↑n : ℕ)) :
      ℝ≥0∞)
heq :
  Eq (α := Set ℕ)
    ({k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} ∪
      {k : ℕ | LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)})
    univ
k : ℕ
hk₁ :
  Membership.mem (γ := Set ℕ)
    {k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} k
hk₂ :
  Membership.mem (γ := Set ℕ)
    {k : ℕ | LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} k
⊢ Membership.mem (γ := Set ℕ) ∅ k
have hk₃ : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)
Tactic: rw [mem_setOf_eq] at hk₁ hk₂
Cleared hypotheses: hk₁, hk₂
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t' : ℕ → Set α
ht' : s ⊆ iUnion t'
t : Set α :=
  ⋃ (n : ℕ),
    ⋃ (_ :
      Membership.mem (γ := Set ℕ)
        {k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
        n),
      t' n
ht :
  t =
    ⋃ (n : ℕ),
      ⋃ (_ :
        Membership.mem (γ := Set ℕ)
          {k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
          n),
        t' n
hle₁ :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
    (∑' (n :
        (↑{k : ℕ |
              LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} :
          Type)),
        (μ : (a : Set α) → ℝ≥0∞) (t' (↑n : ℕ)) :
      ℝ≥0∞)
hcap :
  tᶜ ∩ s ⊆
    ⋃ (n : ℕ),
      ⋃ (_ :
        Membership.mem (γ := Set ℕ)
          {k : ℕ | LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
          n),
        t' n
hle₂ :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (tᶜ ∩ s) : ℝ≥0∞)
    (∑' (n :
        (↑{k : ℕ |
              LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} :
          Type)),
        (ν : (a : Set α) → ℝ≥0∞) (t' (↑n : ℕ)) :
      ℝ≥0∞)
heq :
  Eq (α := Set ℕ)
    ({k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} ∪
      {k : ℕ | LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)})
    univ
k : ℕ
hk₁ :
  Membership.mem (γ := Set ℕ)
    {k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} k
hk₂ :
  Membership.mem (γ := Set ℕ)
    {k : ℕ | LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} k
hk₃ : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)
⊢ Membership.mem (γ := Set ℕ) ∅ k
have hk₄ : LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)
Tactic: rw [mem_setOf_eq] at hk₁ hk₂
Cleared hypotheses: hk₁, hk₂
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
⊢ m0 ≤ OuterMeasure.caratheodory ⊤
have rw : m0 ≤ ⊤
Tactic: rw [OuterMeasure.top_caratheodory]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
f : ι → Measure α
s : Set α
hs : NullMeasurableSet s (sum f)
⊢ Eq (α := ℝ≥0∞) ((sum f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∑' (i : ι), (f i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have apply : LE.le (α := ℝ≥0∞) ((sum f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∑' (i : ι), (f i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: apply le_antisymm ?_ (le_sum_apply _ _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
f : ι → Measure α
s : Set α
hs : NullMeasurableSet s (sum f)
⊢ LE.le (α := ℝ≥0∞) ((sum f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∑' (i : ι), (f i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rcases : ∀ (t : Set α) (ts : t ⊆ s) (t_meas : MeasurableSet t) (ht : t =ᶠ[ae (sum f)] s),
  LE.le (α := ℝ≥0∞) ((sum f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∑' (i : ι), (f i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rcases hs.exists_measurable_subset_ae_eq with ⟨t, ts, t_meas, ht⟩