awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : ¬μ ⟂ₘ ν
n : ℕ
s : Set α
hs : MeasurableSet s
hs_le :
  ∀ (t : Set α),
    MeasurableSet t →
      t ⊆ s →
        LE.le (α := ℝ≥0∞) (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
hs_ge :
  ∀ (t : Set α),
    MeasurableSet t →
      t ⊆ sᶜ →
        LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
          (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
t : Set α
ht : MeasurableSet t
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ sᶜ) : ℝ≥0∞)
    (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) (t ∩ sᶜ) : ℝ≥0∞)

Tactic:
hs_ge (t ∩ sᶜ) (ht.inter hs.compl) inter_subset_right

Premises used: Compl.compl, MeasurableSet.compl, Inter.inter, Set.inter_subset_right, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : ¬μ ⟂ₘ ν
n : ℕ
s : Set α
hs : MeasurableSet s
hs_le :
  ∀ (t : Set α),
    MeasurableSet t →
      t ⊆ s →
        LE.le (α := ℝ≥0∞) (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
hs_ge :
  ∀ (t : Set α),
    MeasurableSet t →
      t ⊆ sᶜ →
        LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
          (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
t : Set α
ht : MeasurableSet t
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ sᶜ) : ℝ≥0∞)
    (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) (t ∩ sᶜ) : ℝ≥0∞)

Tactic:
exact hs_ge (t ∩ sᶜ) (ht.inter hs.compl) inter_subset_right

Premises used: Compl.compl, MeasurableSet.compl, Inter.inter, Set.inter_subset_right, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : ¬μ ⟂ₘ ν
⊢ ∀ (n : ℕ),
    ∃ (s : Set α),
      MeasurableSet s ∧
        (∀ (t : Set α),
            MeasurableSet t →
              LE.le (α := ℝ≥0∞) (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
                ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)) ∧
          ∀ (t : Set α),
            MeasurableSet t →
              LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ sᶜ) : ℝ≥0∞)
                (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) (t ∩ sᶜ) : ℝ≥0∞)

Tactic:
have h_decomp (n : ℕ) : ∃ s : Set α, MeasurableSet s
        ∧ (∀ t, MeasurableSet t → ((1 / (n + 1) : ℝ≥0) • ν) (t ∩ s) ≤ μ (t ∩ s))
        ∧ (∀ t, MeasurableSet t → μ (t ∩ sᶜ) ≤ ((1 / (n + 1) : ℝ≥0) • ν) (t ∩ sᶜ)) := by
    obtain ⟨s, hs, hs_le, hs_ge⟩ := hahn_decomposition μ ((1 / (n + 1) : ℝ≥0) • ν)
    refine ⟨s, hs, fun t ht ↦ ?_, fun t ht ↦ ?_⟩
    · exact hs_le (t ∩ s) (ht.inter hs) inter_subset_right
    · exact hs_ge (t ∩ sᶜ) (ht.inter hs.compl) inter_subset_right
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : ¬μ ⟂ₘ ν
h_decomp :
  ∀ (n : ℕ),
    ∃ (s : Set α),
      MeasurableSet s ∧
        (∀ (t : Set α),
            MeasurableSet t →
              LE.le (α := ℝ≥0∞) (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
                ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)) ∧
          ∀ (t : Set α),
            MeasurableSet t →
              LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ sᶜ) : ℝ≥0∞)
                (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) (t ∩ sᶜ) : ℝ≥0∞)
choose :
  ∀ (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∞)),
    ∃ (ε : ℝ≥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)
⊢ ∃ (ε : ℝ≥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:
choose f hf₁ hf₂ hf₃ using h_decomp
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
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)ᶜ
⊢ MeasurableSet A

Tactic:
have hAmeas : MeasurableSet A := MeasurableSet.iInter fun n ↦ (hf₁ n).compl
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
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
n : ℕ
t : Set α
ht : MeasurableSet t
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ A ∩ (f n)ᶜ) : ℝ≥0∞)
    (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) (t ∩ A ∩ (f n)ᶜ) : ℝ≥0∞)

Tactic:
specialize hf₃ n (t ∩ A) (ht.inter hAmeas)

Premises used: Inter.inter, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
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∞)
A : Set α := ⋂ (n : ℕ), (f n)ᶜ
hAmeas : MeasurableSet A
n : ℕ
t : Set α
ht : MeasurableSet t
hf₃ :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ A ∩ (f n)ᶜ) : ℝ≥0∞)
    (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) (t ∩ A ∩ (f n)ᶜ) : ℝ≥0∞)
⊢ A ∩ (f n)ᶜ = A

Tactic:
have : A ∩ (f n)ᶜ = A := inter_eq_left.mpr (iInter_subset _ n)
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
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∞)
A : Set α := ⋂ (n : ℕ), (f n)ᶜ
hAmeas : MeasurableSet A
n : ℕ
t : Set α
ht : MeasurableSet t
hf₃ :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ A ∩ (f n)ᶜ) : ℝ≥0∞)
    (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) (t ∩ A ∩ (f n)ᶜ) : ℝ≥0∞)
this : A ∩ (f n)ᶜ = A
rwa :
  ∀
    (hf₃ :
      LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ (A ∩ (f n)ᶜ)) : ℝ≥0∞)
        (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) (t ∩ (A ∩ (f n)ᶜ)) : ℝ≥0∞))
    (this : A ∩ (f n)ᶜ = A),
    LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ A) : ℝ≥0∞)
      (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) (t ∩ A) : ℝ≥0∞)
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀
    (hf₃ :
      LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ A) : ℝ≥0∞)
        (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) (t ∩ A) : ℝ≥0∞))
    (this : A ∩ (f n)ᶜ = A),
    LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ A) : ℝ≥0∞)
      (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) (t ∩ A) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ A) : ℝ≥0∞)
    (((1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) • ν : (a : Set α) → ℝ≥0∞) (t ∩ A) : ℝ≥0∞)

Tactic:
rwa [inter_assoc, this] at hf₃

Premises used: Set.inter_assoc
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
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
⊢ ∀ (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∞)

Tactic:
have hA₂ (n : ℕ) (t : Set α) (ht : MeasurableSet t) :
      μ (t ∩ A) ≤ ((1 / (n + 1) : ℝ≥0) • ν) (t ∩ A) := by
    specialize hf₃ n (t ∩ A) (ht.inter hAmeas)
    have : A ∩ (f n)ᶜ = A := inter_eq_left.mpr (iInter_subset _ n)
    rwa [inter_assoc, this] at hf₃
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
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∞)
n : ℕ
⊢ (μ : (a : Set α) → ℝ≥0∞) A ≤
    HMul.hMul (β := ℝ≥0∞) (↑(1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)

Tactic:
simpa using hA₂ n univ .univ

Premises used: Set.univ, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
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∞)
⊢ ∀ (n : ℕ),
    (μ : (a : Set α) → ℝ≥0∞) A ≤
      HMul.hMul (β := ℝ≥0∞) (↑(1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)

Tactic:
have hA₃ (n : ℕ) : μ A ≤ (1 / (n + 1) : ℝ≥0) * ν A := by simpa using hA₂ n univ .univ
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
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∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
measure_ne_top _ _

Premises used: MeasureTheory.measure_ne_top
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
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∞)
lift :
  ∀ (μA : ℝ≥0)
    (hA₃ :
      ∀ (n : ℕ),
        (↑μA : ℝ≥0∞) ≤
          HMul.hMul (β := ℝ≥0∞) (↑(1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)),
    (↑μA : ℝ≥0∞) = 0
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
lift μ A to ℝ≥0 using measure_ne_top _ _ with μA

Premises used: MeasureTheory.measure_ne_top, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
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 : ℝ≥0
hA₃ :
  ∀ (n : ℕ),
    (↑μA : ℝ≥0∞) ≤
      HMul.hMul (β := ℝ≥0∞) (↑(1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
measure_ne_top _ _

Premises used: MeasureTheory.measure_ne_top
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
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 : ℝ≥0
hA₃ :
  ∀ (n : ℕ),
    (↑μA : ℝ≥0∞) ≤
      HMul.hMul (β := ℝ≥0∞) (↑(1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
lift :
  ∀ (νA : ℝ≥0) (hA₃ : ∀ (n : ℕ), (↑μA : ℝ≥0∞) ≤ (↑(1 / HAdd.hAdd (α := ℝ≥0) (↑n : ℝ≥0) 1) : ℝ≥0∞) * (↑νA : ℝ≥0∞)),
    (↑μA : ℝ≥0∞) = 0
⊢ (↑μA : ℝ≥0∞) = 0

Tactic:
lift ν A to ℝ≥0 using measure_ne_top _ _ with νA

Premises used: MeasureTheory.measure_ne_top, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
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∞)
rw : μA = 0
⊢ (↑μA : ℝ≥0∞) = 0

Tactic:
rw [ENNReal.coe_eq_zero]

Premises used: ENNReal.coe_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
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∞)
pos : ∀ (hb : 0 < νA), μA = 0
neg : ∀ (hb : νA ≤ 0), μA = 0
⊢ μA = 0

Tactic:
by_cases! hb : 0 < νA
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
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
this : ∀ (b : ℝ≥0), 0 < b → μA ≤ b
by_contra : ∀ (h : ¬μA = 0), False
⊢ μA = 0

Tactic:
by_contra h
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h_1 : ¬μ ⟂ₘ ν
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
this : ∀ (b : ℝ≥0), 0 < b → μA ≤ b
h : ¬μA = 0
⊢ μA ≤ μA / 2

Tactic:
have h' := this (μA / 2) (half_pos (zero_lt_iff.2 h))