awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : ¬μ ⟂ₘ ν
f : (n : ℕ) → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ :
  ∀ (n : ℕ) (t : Set α),
    MeasurableSet t →
      LE.le (α := ℝ≥0∞) (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) (t ∩ f n) : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) (t ∩ f n) : ℝ≥0∞)
hf₃ :
  ∀ (n : ℕ) (t : Set α),
    MeasurableSet t →
      LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ (f n)ᶜ) : ℝ≥0∞)
        (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) (t ∩ (f n)ᶜ) : ℝ≥0∞)
A : Set α := ⋂ (n : ℕ), (f n)ᶜ
hAmeas : MeasurableSet A
hA₂ :
  ∀ (n : ℕ) (t : Set α) (ht : MeasurableSet t),
    LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ A) : ℝ≥0∞)
      (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) (t ∩ A) : ℝ≥0∞)
μA νA : ℝ≥0
hA₃ : ∀ (n : ℕ), (↑μA : ℝ≥0∞) ≤ (↑(1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) : ℝ≥0∞) * (↑νA : ℝ≥0∞)
hb : 0 < νA
c : ℝ≥0
hc : 0 < c
n : ℕ
hn : 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < (↑c : ℝ) * (↑νA : ℝ)⁻¹
hb₁ : 0 < (↑νA : ℝ)⁻¹
rw : (↑(1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) : ℝ) < (↑c : ℝ) * (↑νA : ℝ)⁻¹
⊢ 1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1 * νA < c
have rw₁ : νA ≠ 0
Tactic: rw [← NNReal.coe_lt_coe, ← mul_lt_mul_iff_left₀ hb₁, NNReal.coe_mul, mul_assoc, ←
          NNReal.coe_inv, ← NNReal.coe_mul, mul_inv_cancel₀, ← NNReal.coe_mul, mul_one,
          NNReal.coe_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : ¬μ ⟂ₘ ν
f : (n : ℕ) → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ :
  ∀ (n : ℕ) (t : Set α),
    MeasurableSet t →
      LE.le (α := ℝ≥0∞) (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) (t ∩ f n) : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) (t ∩ f n) : ℝ≥0∞)
hf₃ :
  ∀ (n : ℕ) (t : Set α),
    MeasurableSet t →
      LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ (f n)ᶜ) : ℝ≥0∞)
        (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) (t ∩ (f n)ᶜ) : ℝ≥0∞)
A : Set α := ⋂ (n : ℕ), (f n)ᶜ
hAmeas : MeasurableSet A
hA₂ :
  ∀ (n : ℕ) (t : Set α) (ht : MeasurableSet t),
    LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ A) : ℝ≥0∞)
      (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) (t ∩ A) : ℝ≥0∞)
μA νA : ℝ≥0
hA₃ : ∀ (n : ℕ), (↑μA : ℝ≥0∞) ≤ (↑(1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) : ℝ≥0∞) * (↑νA : ℝ≥0∞)
hb : 0 < νA
c : ℝ≥0
hc : 0 < c
n : ℕ
hn : 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < (↑c : ℝ) * (↑νA : ℝ)⁻¹
hb₁ : 0 < (↑νA : ℝ)⁻¹
⊢ μA ≤ c
have h' : 1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1 * νA < c
Tactic: have h' : 1 / (↑n + 1) * νA < c := by
        rw [← NNReal.coe_lt_coe, ← mul_lt_mul_iff_left₀ hb₁, NNReal.coe_mul, mul_assoc, ←
          NNReal.coe_inv, ← NNReal.coe_mul, mul_inv_cancel₀, ← NNReal.coe_mul, mul_one,
          NNReal.coe_inv]
        · exact hn
        · exact hb.ne'
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : ¬μ ⟂ₘ ν
f : (n : ℕ) → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ :
  ∀ (n : ℕ) (t : Set α),
    MeasurableSet t →
      LE.le (α := ℝ≥0∞) (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) (t ∩ f n) : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) (t ∩ f n) : ℝ≥0∞)
hf₃ :
  ∀ (n : ℕ) (t : Set α),
    MeasurableSet t →
      LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ (f n)ᶜ) : ℝ≥0∞)
        (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) (t ∩ (f n)ᶜ) : ℝ≥0∞)
A : Set α := ⋂ (n : ℕ), (f n)ᶜ
hAmeas : MeasurableSet A
hA₂ :
  ∀ (n : ℕ) (t : Set α) (ht : MeasurableSet t),
    LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ A) : ℝ≥0∞)
      (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) (t ∩ A) : ℝ≥0∞)
μA νA : ℝ≥0
hA₃ : ∀ (n : ℕ), (↑μA : ℝ≥0∞) ≤ (↑(1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) : ℝ≥0∞) * (↑νA : ℝ≥0∞)
hb : 0 < νA
c : ℝ≥0
hc : 0 < c
n : ℕ
hn : 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < (↑c : ℝ) * (↑νA : ℝ)⁻¹
hb₁ : 0 < (↑νA : ℝ)⁻¹
h' : 1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1 * νA < c
⊢ μA ≤ c
have pos : μA ≤ 1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1 * νA
Tactic: refine le_trans ?_ h'.le
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : ¬μ ⟂ₘ ν
f : (n : ℕ) → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ :
  ∀ (n : ℕ) (t : Set α),
    MeasurableSet t →
      LE.le (α := ℝ≥0∞) (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) (t ∩ f n) : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) (t ∩ f n) : ℝ≥0∞)
hf₃ :
  ∀ (n : ℕ) (t : Set α),
    MeasurableSet t →
      LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ (f n)ᶜ) : ℝ≥0∞)
        (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) (t ∩ (f n)ᶜ) : ℝ≥0∞)
A : Set α := ⋂ (n : ℕ), (f n)ᶜ
hAmeas : MeasurableSet A
hA₂ :
  ∀ (n : ℕ) (t : Set α) (ht : MeasurableSet t),
    LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ A) : ℝ≥0∞)
      (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) (t ∩ A) : ℝ≥0∞)
μA νA : ℝ≥0
hA₃ : ∀ (n : ℕ), (↑μA : ℝ≥0∞) ≤ (↑(1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) : ℝ≥0∞) * (↑νA : ℝ≥0∞)
hb : 0 < νA
c : ℝ≥0
hc : 0 < c
n : ℕ
hn : 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < (↑c : ℝ) * (↑νA : ℝ)⁻¹
hb₁ : 0 < (↑νA : ℝ)⁻¹
h' : 1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1 * νA < c
⊢ μA ≤ 1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1 * νA
have pos : (↑μA : ℝ≥0∞) ≤ (↑(1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) : ℝ≥0∞) * (↑νA : ℝ≥0∞)
Tactic: rw [← ENNReal.coe_le_coe, ENNReal.coe_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : ¬μ ⟂ₘ ν
f : (n : ℕ) → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ :
  ∀ (n : ℕ) (t : Set α),
    MeasurableSet t →
      LE.le (α := ℝ≥0∞) (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) (t ∩ f n) : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) (t ∩ f n) : ℝ≥0∞)
hf₃ :
  ∀ (n : ℕ) (t : Set α),
    MeasurableSet t →
      LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ (f n)ᶜ) : ℝ≥0∞)
        (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) (t ∩ (f n)ᶜ) : ℝ≥0∞)
A : Set α := ⋂ (n : ℕ), (f n)ᶜ
hAmeas : MeasurableSet A
hA₂ :
  ∀ (n : ℕ) (t : Set α) (ht : MeasurableSet t),
    LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ A) : ℝ≥0∞)
      (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) (t ∩ A) : ℝ≥0∞)
μA νA : ℝ≥0
hA₃ : ∀ (n : ℕ), (↑μA : ℝ≥0∞) ≤ (↑(1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) : ℝ≥0∞) * (↑νA : ℝ≥0∞)
hb : νA ≤ 0
⊢ μA = 0
have hb₁ : νA = 0
Tactic: rw [le_zero_iff] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : ¬μ ⟂ₘ ν
f : (n : ℕ) → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ :
  ∀ (n : ℕ) (t : Set α),
    MeasurableSet t →
      LE.le (α := ℝ≥0∞) (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) (t ∩ f n) : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) (t ∩ f n) : ℝ≥0∞)
hf₃ :
  ∀ (n : ℕ) (t : Set α),
    MeasurableSet t →
      LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ (f n)ᶜ) : ℝ≥0∞)
        (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) (t ∩ (f n)ᶜ) : ℝ≥0∞)
A : Set α := ⋂ (n : ℕ), (f n)ᶜ
hAmeas : MeasurableSet A
hA₂ :
  ∀ (n : ℕ) (t : Set α) (ht : MeasurableSet t),
    LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ A) : ℝ≥0∞)
      (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) (t ∩ A) : ℝ≥0∞)
hA₃ :
  ∀ (n : ℕ),
    (μ : (a : Set α) → ℝ≥0∞) A ≤
      HMul.hMul (β := ℝ≥0∞) (↑(1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
⊢ ∃ (ε : ℝ≥0),
    0 < ε ∧
      ∃ (E : Set α),
        MeasurableSet E ∧
          LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞) ∧
            ∀ (A : Set α),
              MeasurableSet A →
                HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A ∩ E) : ℝ≥0∞) ≤
                  (μ : (a : Set α) → ℝ≥0∞) (A ∩ E)
have hμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: have hμ : μ A = 0 := by
    lift μ A to ℝ≥0 using measure_ne_top _ _ with μA
    lift ν A to ℝ≥0 using measure_ne_top _ _ with νA
    rw [ENNReal.coe_eq_zero]
    by_cases! hb : 0 < νA
    · suffices ∀ b, 0 < b → μA ≤ b by
        by_contra h
        have h' := this (μA / 2) (half_pos (zero_lt_iff.2 h))
        rw [← @Classical.not_not (μA ≤ μA / 2)] at h'
        exact h' (not_le.2 (NNReal.half_lt_self h))
      intro c hc
      have : ∃ n : ℕ, 1 / (n + 1 : ℝ) < c * (νA : ℝ)⁻¹ := by
        refine exists_nat_one_div_lt ?_
        positivity
      rcases this with ⟨n, hn⟩
      have hb₁ : (0 : ℝ) < (νA : ℝ)⁻¹ := by rw [_root_.inv_pos]; exact hb
      have h' : 1 / (↑n + 1) * νA < c := by
        rw [← NNReal.coe_lt_coe, ← mul_lt_mul_iff_left₀ hb₁, NNReal.coe_mul, mul_assoc, ←
          NNReal.coe_inv, ← NNReal.coe_mul, mul_inv_cancel₀, ← NNReal.coe_mul, mul_one,
          NNReal.coe_inv]
        · exact hn
        · exact hb.ne'
      refine le_trans ?_ h'.le
      rw [← ENNReal.coe_le_coe, ENNReal.coe_mul]
      exact hA₃ n
    · rw [le_zero_iff] at hb
      simpa [hb] using hA₃ 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h :
  ¬∃ (s : Set α),
      MeasurableSet s ∧
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
          Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
f : (n : ℕ) → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ :
  ∀ (n : ℕ) (t : Set α),
    MeasurableSet t →
      LE.le (α := ℝ≥0∞) (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) (t ∩ f n) : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) (t ∩ f n) : ℝ≥0∞)
hf₃ :
  ∀ (n : ℕ) (t : Set α),
    MeasurableSet t →
      LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ (f n)ᶜ) : ℝ≥0∞)
        (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) (t ∩ (f n)ᶜ) : ℝ≥0∞)
A : Set α := ⋂ (n : ℕ), (f n)ᶜ
hAmeas : MeasurableSet A
hA₂ :
  ∀ (n : ℕ) (t : Set α) (ht : MeasurableSet t),
    LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ A) : ℝ≥0∞)
      (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) (t ∩ A) : ℝ≥0∞)
hA₃ :
  ∀ (n : ℕ),
    (μ : (a : Set α) → ℝ≥0∞) A ≤
      HMul.hMul (β := ℝ≥0∞) (↑(1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
hμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ (ε : ℝ≥0),
    0 < ε ∧
      ∃ (E : Set α),
        MeasurableSet E ∧
          LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞) ∧
            ∀ (A : Set α),
              MeasurableSet A →
                HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A ∩ E) : ℝ≥0∞) ≤
                  (μ : (a : Set α) → ℝ≥0∞) (A ∩ E)
have h₁ : ∀ (s : Set α) (_ : MeasurableSet s) (_ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
  Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: push Not at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
f : (n : ℕ) → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ :
  ∀ (n : ℕ) (t : Set α),
    MeasurableSet t →
      LE.le (α := ℝ≥0∞) (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) (t ∩ f n) : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) (t ∩ f n) : ℝ≥0∞)
hf₃ :
  ∀ (n : ℕ) (t : Set α),
    MeasurableSet t →
      LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ (f n)ᶜ) : ℝ≥0∞)
        (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) (t ∩ (f n)ᶜ) : ℝ≥0∞)
A : Set α := ⋂ (n : ℕ), (f n)ᶜ
hAmeas : MeasurableSet A
hA₂ :
  ∀ (n : ℕ) (t : Set α) (ht : MeasurableSet t),
    LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ A) : ℝ≥0∞)
      (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) (t ∩ A) : ℝ≥0∞)
hA₃ :
  ∀ (n : ℕ),
    (μ : (a : Set α) → ℝ≥0∞) A ≤
      HMul.hMul (β := ℝ≥0∞) (↑(1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
hμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (0 : ℝ≥0∞)
h :
  ∀ (s : Set α) (_ : MeasurableSet s) (_ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ (ε : ℝ≥0),
    0 < ε ∧
      ∃ (E : Set α),
        MeasurableSet E ∧
          LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞) ∧
            ∀ (A : Set α),
              MeasurableSet A →
                HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A ∩ E) : ℝ≥0∞) ≤
                  (μ : (a : Set α) → ℝ≥0∞) (A ∩ E)
have this : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) Aᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: have := h _ hAmeas hμ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
f : (n : ℕ) → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ :
  ∀ (n : ℕ) (t : Set α),
    MeasurableSet t →
      LE.le (α := ℝ≥0∞) (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) (t ∩ f n) : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) (t ∩ f n) : ℝ≥0∞)
hf₃ :
  ∀ (n : ℕ) (t : Set α),
    MeasurableSet t →
      LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ (f n)ᶜ) : ℝ≥0∞)
        (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) (t ∩ (f n)ᶜ) : ℝ≥0∞)
A : Set α := ⋂ (n : ℕ), (f n)ᶜ
hAmeas : MeasurableSet A
hA₂ :
  ∀ (n : ℕ) (t : Set α) (ht : MeasurableSet t),
    LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ A) : ℝ≥0∞)
      (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) (t ∩ A) : ℝ≥0∞)
hA₃ :
  ∀ (n : ℕ),
    (μ : (a : Set α) → ℝ≥0∞) A ≤
      HMul.hMul (β := ℝ≥0∞) (↑(1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
hμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (0 : ℝ≥0∞)
h :
  ∀ (s : Set α) (_ : MeasurableSet s) (_ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
this : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) Aᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ (ε : ℝ≥0),
    0 < ε ∧
      ∃ (E : Set α),
        MeasurableSet E ∧
          LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞) ∧
            ∀ (A : Set α),
              MeasurableSet A →
                HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A ∩ E) : ℝ≥0∞) ≤
                  (μ : (a : Set α) → ℝ≥0∞) (A ∩ E)
have this₁ : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp_rw [A, compl_iInter, compl_compl] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
f : (n : ℕ) → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ :
  ∀ (n : ℕ) (t : Set α),
    MeasurableSet t →
      LE.le (α := ℝ≥0∞) (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) (t ∩ f n) : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) (t ∩ f n) : ℝ≥0∞)
hf₃ :
  ∀ (n : ℕ) (t : Set α),
    MeasurableSet t →
      LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ (f n)ᶜ) : ℝ≥0∞)
        (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) (t ∩ (f n)ᶜ) : ℝ≥0∞)
A : Set α := ⋂ (n : ℕ), (f n)ᶜ
hAmeas : MeasurableSet A
hA₂ :
  ∀ (n : ℕ) (t : Set α) (ht : MeasurableSet t),
    LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ A) : ℝ≥0∞)
      (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) (t ∩ A) : ℝ≥0∞)
hA₃ :
  ∀ (n : ℕ),
    (μ : (a : Set α) → ℝ≥0∞) A ≤
      HMul.hMul (β := ℝ≥0∞) (↑(1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
hμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (0 : ℝ≥0∞)
h :
  ∀ (s : Set α) (_ : MeasurableSet s) (_ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
this : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ (ε : ℝ≥0),
    0 < ε ∧
      ∃ (E : Set α),
        MeasurableSet E ∧
          LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞) ∧
            ∀ (A : Set α),
              MeasurableSet A →
                HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A ∩ E) : ℝ≥0∞) ≤
                  (μ : (a : Set α) → ℝ≥0∞) (A ∩ E)
have obtain : ∀ (n : ℕ) (hn : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (f n) : ℝ≥0∞)),
  ∃ (ε : ℝ≥0),
    0 < ε ∧
      ∃ (E : Set α),
        MeasurableSet E ∧
          LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞) ∧
            ∀ (A : Set α),
              MeasurableSet A →
                HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A ∩ E) : ℝ≥0∞) ≤
                  (μ : (a : Set α) → ℝ≥0∞) (A ∩ E)
Tactic: obtain ⟨n, hn⟩ := exists_measure_pos_of_not_measure_iUnion_null this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : f ∈ measurableLE μ ν
hg : g ∈ measurableLE μ ν
⊢ (fun (a : α) ↦ max (f a) (g a)) ∈ measurableLE μ ν
have refine : ∀ (A : Set α) (hA : MeasurableSet A), ∫⁻ (x : α) in A, (fun (a : α) ↦ max (f a) (g a)) x ∂μ ≤ (ν : (a : Set α) → ℝ≥0∞) A
Tactic: refine ⟨Measurable.max hf.1 hg.1, fun A hA ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : f ∈ measurableLE μ ν
hg : g ∈ measurableLE μ ν
A : Set α
hA : MeasurableSet A
⊢ ∫⁻ (x : α) in A, (fun (a : α) ↦ max (f a) (g a)) x ∂μ ≤ (ν : (a : Set α) → ℝ≥0∞) A
have h₁ : MeasurableSet (A ∩ {a : α | f a ≤ g a})
Tactic: have h₁ := hA.inter (measurableSet_le hf.1 hg.1)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : f ∈ measurableLE μ ν
hg : g ∈ measurableLE μ ν
A : Set α
hA : MeasurableSet A
h₁ : MeasurableSet (A ∩ {a : α | f a ≤ g a})
⊢ ∫⁻ (x : α) in A, (fun (a : α) ↦ max (f a) (g a)) x ∂μ ≤ (ν : (a : Set α) → ℝ≥0∞) A
have h₂ : MeasurableSet (A ∩ {a : α | g a < f a})
Tactic: have h₂ := hA.inter (measurableSet_lt hg.1 hf.1)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : f ∈ measurableLE μ ν
hg : g ∈ measurableLE μ ν
A : Set α
hA : MeasurableSet A
h₁ : MeasurableSet (A ∩ {a : α | f a ≤ g a})
h₂ : MeasurableSet (A ∩ {a : α | g a < f a})
⊢ ∫⁻ (x : α) in A, (fun (a : α) ↦ max (f a) (g a)) x ∂μ ≤ (ν : (a : Set α) → ℝ≥0∞) A
have rw : ∫⁻ (x : α) in A ∩ {x : α | f x ≤ g x}, g x ∂μ + ∫⁻ (x : α) in A ∩ {x : α | g x < f x}, f x ∂μ ≤
  (ν : (a : Set α) → ℝ≥0∞) A
Tactic: rw [setLIntegral_max hf.1 hg.1]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : f ∈ measurableLE μ ν
hg : g ∈ measurableLE μ ν
A : Set α
hA : MeasurableSet A
h₁ : MeasurableSet (A ∩ {a : α | f a ≤ g a})
h₂ : MeasurableSet (A ∩ {a : α | g a < f a})
⊢ ∫⁻ (x : α) in A ∩ {x : α | f x ≤ g x}, g x ∂μ + ∫⁻ (x : α) in A ∩ {x : α | g x < f x}, f x ∂μ ≤
    (ν : (a : Set α) → ℝ≥0∞) A
have refine : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A ∩ {a : α | f a ≤ g a}) : ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) (A ∩ {a : α | g a < f a}) : ℝ≥0∞) =
  (ν : (a : Set α) → ℝ≥0∞) A
Tactic: refine (add_le_add (hg.2 _ h₁) (hf.2 _ h₂)).trans_eq ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : f ∈ measurableLE μ ν
hg : g ∈ measurableLE μ ν
A : Set α
hA : MeasurableSet A
h₁ : MeasurableSet (A ∩ {a : α | f a ≤ g a})
h₂ : MeasurableSet (A ∩ {a : α | g a < f a})
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A ∩ {a : α | f a ≤ g a}) : ℝ≥0∞)
      ((ν : (a : Set α) → ℝ≥0∞) (A ∩ {a : α | g a < f a}) : ℝ≥0∞) =
    (ν : (a : Set α) → ℝ≥0∞) A
have simp : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A ∩ {a : α | f a ≤ g a}) : ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) (A \ {a : α | f a ≤ g a}) : ℝ≥0∞) =
  (ν : (a : Set α) → ℝ≥0∞) A
Tactic: simp only [← not_le, ← compl_setOf, ← diff_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Sort u_2
f : ℕ → α → ℝ≥0∞
m : ℕ
a : α
⊢ ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a = max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
have set : let c : ℝ≥0∞ := ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a;
∀ (hc : c = ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a), c = max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
Tactic: set c := ⨆ (k : ℕ) (_ : k ≤ m + 1), f k a with hc
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Sort u_2
f : ℕ → α → ℝ≥0∞
m : ℕ
a : α
c : ℝ≥0∞ := ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a
hc : c = ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a
⊢ c = max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
have set : let d := max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a);
∀ (hd : d = max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)), c = d
Tactic: set d := f m.succ a ⊔ ⨆ (k : ℕ) (_ : k ≤ m), f k a with hd
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Sort u_2
f : ℕ → α → ℝ≥0∞
m : ℕ
a : α
c : ℝ≥0∞ := ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a
hc : c = ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a
d : ℝ≥0∞ := max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
hd : d = max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
⊢ c = d
have rw : ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a ≤ max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a) ∧
  max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a) ≤ ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a
Tactic: rw [le_antisymm_iff, hc, hd]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Sort u_2
f : ℕ → α → ℝ≥0∞
m : ℕ
a : α
c : ℝ≥0∞ := ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a
hc : c = ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a
d : ℝ≥0∞ := max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
hd : d = max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
⊢ ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a ≤ max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a) ∧
    max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a) ≤ ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a
have left : ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a ≤ max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Sort u_2
f : ℕ → α → ℝ≥0∞
m : ℕ
a : α
c : ℝ≥0∞ := ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a
hc : c = ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a
d : ℝ≥0∞ := max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
hd : d = max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
left : ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a ≤ max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
⊢ ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a ≤ max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a) ∧
    max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a) ≤ ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a
have right : max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a) ≤ ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a
Tactic: constructor