awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
h : ∀ (x : ℝ), ∃ x_1 ∈ s.measureOfNegatives, x_1 < x
f : (n : ℕ) → ℝ
hf : ∀ (n : ℕ), f n ∈ s.measureOfNegatives ∧ f n < -(↑n : ℝ)
B : (n : ℕ) → Set α
hmeas : ∀ (n : ℕ), MeasurableSet (B n)
hr : ∀ (n : ℕ), s ≤[B n] 0
h_lt : ∀ (n : ℕ), (↑s : Set α → ℝ) (B n) < -(↑n : ℝ)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hfalse : ∀ (n : ℕ), (↑s : Set α → ℝ) A ≤ -(↑n : ℝ)
n : ℕ
hn : -(↑s : Set α → ℝ) A < (↑n : ℝ)
⊢ False

Tactic:
lt_irrefl _ ((neg_lt.1 hn).trans_le (hfalse n))

Premises used: lt_irrefl, LT.lt.trans_le, Iff.mp, neg_lt
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
h : ∀ (x : ℝ), ∃ x_1 ∈ s.measureOfNegatives, x_1 < x
f : (n : ℕ) → ℝ
hf : ∀ (n : ℕ), f n ∈ s.measureOfNegatives ∧ f n < -(↑n : ℝ)
B : (n : ℕ) → Set α
hmeas : ∀ (n : ℕ), MeasurableSet (B n)
hr : ∀ (n : ℕ), s ≤[B n] 0
h_lt : ∀ (n : ℕ), (↑s : Set α → ℝ) (B n) < -(↑n : ℝ)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hfalse : ∀ (n : ℕ), (↑s : Set α → ℝ) A ≤ -(↑n : ℝ)
n : ℕ
hn : -(↑s : Set α → ℝ) A < (↑n : ℝ)
⊢ False

Tactic:
exact lt_irrefl _ ((neg_lt.1 hn).trans_le (hfalse n))

Premises used: lt_irrefl, LT.lt.trans_le, Iff.mp, neg_lt
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
obtain :
  ∀ (f : ℕ → ℝ),
    Antitone f →
      ∀ (hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))) (hf₁ : ∀ (n : ℕ), f n ∈ s.measureOfNegatives),
        ∃ (i : Set α), MeasurableSet i ∧ 0 ≤[i] s ∧ s ≤[iᶜ] 0
⊢ ∃ (i : Set α), MeasurableSet i ∧ 0 ≤[i] s ∧ s ≤[iᶜ] 0

Tactic:
obtain ⟨f, _, hf₂, hf₁⟩ :=
    exists_seq_tendsto_sInf ⟨0, @zero_mem_measureOfNegatives _ _ s⟩ bddBelow_measureOfNegatives

Premises used: MeasureTheory.SignedMeasure.bddBelow_measureOfNegatives, Exists.intro, MeasureTheory.SignedMeasure.zero_mem_measureOfNegatives, exists_seq_tendsto_sInf, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
hf₁ : ∀ (n : ℕ), f n ∈ s.measureOfNegatives
choose :
  ∀ (B : (n : ℕ) → Set α)
    (hB :
      ∀ (n : ℕ),
        Membership.mem (γ := Set (Set α)) {B : Set α | MeasurableSet B ∧ s ≤[B] 0} (B n) ∧
          (↑s : Set α → ℝ) (B n) = f n),
    ∃ (i : Set α), MeasurableSet i ∧ 0 ≤[i] s ∧ s ≤[iᶜ] 0
⊢ ∃ (i : Set α), MeasurableSet i ∧ 0 ≤[i] s ∧ s ≤[iᶜ] 0

Tactic:
choose B hB using hf₁
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : (n : ℕ) → Set α
hB :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set α)) {B : Set α | MeasurableSet B ∧ s ≤[B] 0} (B n) ∧ (↑s : Set α → ℝ) (B n) = f n
⊢ ∀ (n : ℕ), MeasurableSet (B n)

Tactic:
have hB₁ : ∀ n, MeasurableSet (B n) := fun n => (hB n).1.1
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : (n : ℕ) → Set α
hB :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set α)) {B : Set α | MeasurableSet B ∧ s ≤[B] 0} (B n) ∧ (↑s : Set α → ℝ) (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
⊢ ∀ (n : ℕ), s ≤[B n] 0

Tactic:
have hB₂ : ∀ n, s ≤[B n] 0 := fun n => (hB n).1.2
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : (n : ℕ) → Set α
hB :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set α)) {B : Set α | MeasurableSet B ∧ s ≤[B] 0} (B n) ∧ (↑s : Set α → ℝ) (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), s ≤[B n] 0
⊢ let A : Set α := ⋃ (n : ℕ), B n;
  A = ⋃ (n : ℕ), B n

Tactic:
set A := ⋃ n, B n with hA
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : (n : ℕ) → Set α
hB :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set α)) {B : Set α | MeasurableSet B ∧ s ≤[B] 0} (B n) ∧ (↑s : Set α → ℝ) (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), s ≤[B n] 0
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
⊢ MeasurableSet A

Tactic:
have hA₁ : MeasurableSet A := MeasurableSet.iUnion hB₁
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : (n : ℕ) → Set α
hB :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set α)) {B : Set α | MeasurableSet B ∧ s ≤[B] 0} (B n) ∧ (↑s : Set α → ℝ) (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), s ≤[B n] 0
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
⊢ s ≤[A] 0

Tactic:
have hA₂ : s ≤[A] 0 := restrict_le_restrict_iUnion _ _ hB₁ hB₂
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : (n : ℕ) → Set α
hB :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set α)) {B : Set α | MeasurableSet B ∧ s ≤[B] 0} (B n) ∧ (↑s : Set α → ℝ) (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), s ≤[B n] 0
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : s ≤[A] 0
a : (↑s : Set α → ℝ) A ≤ sInf s.measureOfNegatives
a₁ : sInf s.measureOfNegatives ≤ (↑s : Set α → ℝ) A
⊢ (↑s : Set α → ℝ) A = sInf s.measureOfNegatives

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : (n : ℕ) → Set α
hB :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set α)) {B : Set α | MeasurableSet B ∧ s ≤[B] 0} (B n) ∧ (↑s : Set α → ℝ) (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), s ≤[B n] 0
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : s ≤[A] 0
⊢ (↑s : Set α → ℝ) A ≤ sInf s.measureOfNegatives

Tactic:
le_of_tendsto_of_tendsto tendsto_const_nhds hf₂ (Eventually.of_forall fun n => ?_)

Premises used: tendsto_const_nhds, Filter.Eventually.of_forall, le_of_tendsto_of_tendsto
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : (n : ℕ) → Set α
hB :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set α)) {B : Set α | MeasurableSet B ∧ s ≤[B] 0} (B n) ∧ (↑s : Set α → ℝ) (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), s ≤[B n] 0
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : s ≤[A] 0
a : ∀ (n : ℕ), (fun (x : ℕ) ↦ (↑s : Set α → ℝ) A) n ≤ f n
⊢ (↑s : Set α → ℝ) A ≤ sInf s.measureOfNegatives

Tactic:
refine le_of_tendsto_of_tendsto tendsto_const_nhds hf₂ (Eventually.of_forall fun n => ?_)

Premises used: tendsto_const_nhds, Filter.Eventually.of_forall, le_of_tendsto_of_tendsto
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : (n : ℕ) → Set α
hB :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set α)) {B : Set α | MeasurableSet B ∧ s ≤[B] 0} (B n) ∧ (↑s : Set α → ℝ) (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), s ≤[B n] 0
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : s ≤[A] 0
n : ℕ
a : (fun (x : ℕ) ↦ (↑s : Set α → ℝ) ((⋃ (i : ℕ), B i) \ B n) + (↑s : Set α → ℝ) (B n)) n ≤ (↑s : Set α → ℝ) (B n)
rw : MeasurableSet ((⋃ (i : ℕ), B i) \ B n)
⊢ (fun (x : ℕ) ↦ (↑s : Set α → ℝ) A) n ≤ f n

Tactic:
rw [← (hB n).2, hA, ← Set.diff_union_of_subset (Set.subset_iUnion _ n),
        of_union Set.disjoint_sdiff_left _ (hB₁ n)]

Premises used: MeasureTheory.VectorMeasure.of_union, Set.subset_iUnion, And.right, Set.disjoint_sdiff_left, Set.diff_union_of_subset
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : (n : ℕ) → Set α
hB :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set α)) {B : Set α | MeasurableSet B ∧ s ≤[B] 0} (B n) ∧ (↑s : Set α → ℝ) (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), s ≤[B n] 0
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : s ≤[A] 0
n : ℕ
⊢ (fun (x : ℕ) ↦ (↑s : Set α → ℝ) ((⋃ (i : ℕ), B i) \ B n) + (↑s : Set α → ℝ) (B n)) n ≤ (↑s : Set α → ℝ) (B n)

Tactic:
add_le_of_nonpos_left ?_

Premises used: add_le_of_nonpos_left
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : (n : ℕ) → Set α
hB :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set α)) {B : Set α | MeasurableSet B ∧ s ≤[B] 0} (B n) ∧ (↑s : Set α → ℝ) (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), s ≤[B n] 0
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : s ≤[A] 0
n : ℕ
a : (↑s : Set α → ℝ) ((⋃ (i : ℕ), B i) \ B n) ≤ 0
⊢ (fun (x : ℕ) ↦ (↑s : Set α → ℝ) ((⋃ (i : ℕ), B i) \ B n) + (↑s : Set α → ℝ) (B n)) n ≤ (↑s : Set α → ℝ) (B n)

Tactic:
refine add_le_of_nonpos_left ?_

Premises used: add_le_of_nonpos_left
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : (n : ℕ) → Set α
hB :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set α)) {B : Set α | MeasurableSet B ∧ s ≤[B] 0} (B n) ∧ (↑s : Set α → ℝ) (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), s ≤[B n] 0
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : s ≤[A] 0
n : ℕ
⊢ s ≤[A] 0

Tactic:
have : s ≤[A] 0 :=
          restrict_le_restrict_iUnion _ _ hB₁ fun m =>
            let ⟨_, h⟩ := (hB m).1
            h
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : (n : ℕ) → Set α
hB :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set α)) {B : Set α | MeasurableSet B ∧ s ≤[B] 0} (B n) ∧ (↑s : Set α → ℝ) (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), s ≤[B n] 0
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : s ≤[A] 0
n : ℕ
this : s ≤[A] 0
⊢ (↑s : Set α → ℝ) ((⋃ (i : ℕ), B i) \ B n) ≤ 0

Tactic:
nonpos_of_restrict_le_zero _ (restrict_le_zero_subset _ ?_ Set.diff_subset this)

Premises used: Set.diff_subset, MeasureTheory.VectorMeasure.nonpos_of_restrict_le_zero, MeasureTheory.VectorMeasure.restrict_le_zero_subset
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : (n : ℕ) → Set α
hB :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set α)) {B : Set α | MeasurableSet B ∧ s ≤[B] 0} (B n) ∧ (↑s : Set α → ℝ) (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), s ≤[B n] 0
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : s ≤[A] 0
n : ℕ
this : s ≤[A] 0
a : MeasurableSet.{u_1} (α := α) (⋃ (i : ℕ), B i)
⊢ (↑s : Set α → ℝ) ((⋃ (i : ℕ), B i) \ B n) ≤ 0

Tactic:
refine
          nonpos_of_restrict_le_zero _ (restrict_le_zero_subset _ ?_ Set.diff_subset this)

Premises used: Set.diff_subset, MeasureTheory.VectorMeasure.nonpos_of_restrict_le_zero, MeasureTheory.VectorMeasure.restrict_le_zero_subset
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : (n : ℕ) → Set α
hB :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set α)) {B : Set α | MeasurableSet B ∧ s ≤[B] 0} (B n) ∧ (↑s : Set α → ℝ) (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), s ≤[B n] 0
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : s ≤[A] 0
n : ℕ
this : s ≤[A] 0
⊢ MeasurableSet.{u_1} (α := α) (⋃ (i : ℕ), B i)

Tactic:
MeasurableSet.iUnion hB₁

Premises used: MeasurableSet.iUnion
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : (n : ℕ) → Set α
hB :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set α)) {B : Set α | MeasurableSet B ∧ s ≤[B] 0} (B n) ∧ (↑s : Set α → ℝ) (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), s ≤[B n] 0
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : s ≤[A] 0
n : ℕ
this : s ≤[A] 0
⊢ MeasurableSet.{u_1} (α := α) (⋃ (i : ℕ), B i)

Tactic:
exact MeasurableSet.iUnion hB₁

Premises used: MeasurableSet.iUnion
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : (n : ℕ) → Set α
hB :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set α)) {B : Set α | MeasurableSet B ∧ s ≤[B] 0} (B n) ∧ (↑s : Set α → ℝ) (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), s ≤[B n] 0
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : s ≤[A] 0
n : ℕ
⊢ MeasurableSet ((⋃ (i : ℕ), B i) \ B n)

Tactic:
(MeasurableSet.iUnion hB₁).diff (hB₁ n)

Premises used: MeasurableSet.diff, MeasurableSet.iUnion
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : (n : ℕ) → Set α
hB :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set α)) {B : Set α | MeasurableSet B ∧ s ≤[B] 0} (B n) ∧ (↑s : Set α → ℝ) (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), s ≤[B n] 0
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : s ≤[A] 0
n : ℕ
⊢ MeasurableSet ((⋃ (i : ℕ), B i) \ B n)

Tactic:
exact (MeasurableSet.iUnion hB₁).diff (hB₁ n)

Premises used: MeasurableSet.diff, MeasurableSet.iUnion
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : (n : ℕ) → Set α
hB :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set α)) {B : Set α | MeasurableSet B ∧ s ≤[B] 0} (B n) ∧ (↑s : Set α → ℝ) (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), s ≤[B n] 0
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : s ≤[A] 0
⊢ sInf s.measureOfNegatives ≤ (↑s : Set α → ℝ) A

Tactic:
csInf_le bddBelow_measureOfNegatives ⟨A, ⟨hA₁, hA₂⟩, rfl⟩

Premises used: MeasureTheory.SignedMeasure.bddBelow_measureOfNegatives, And.intro, Exists.intro, csInf_le, rfl
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : (n : ℕ) → Set α
hB :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set α)) {B : Set α | MeasurableSet B ∧ s ≤[B] 0} (B n) ∧ (↑s : Set α → ℝ) (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), s ≤[B n] 0
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : s ≤[A] 0
⊢ sInf s.measureOfNegatives ≤ (↑s : Set α → ℝ) A

Tactic:
exact csInf_le bddBelow_measureOfNegatives ⟨A, ⟨hA₁, hA₂⟩, rfl⟩

Premises used: MeasureTheory.SignedMeasure.bddBelow_measureOfNegatives, And.intro, Exists.intro, csInf_le, rfl
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : (n : ℕ) → Set α
hB :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set α)) {B : Set α | MeasurableSet B ∧ s ≤[B] 0} (B n) ∧ (↑s : Set α → ℝ) (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), s ≤[B n] 0
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : s ≤[A] 0
⊢ (↑s : Set α → ℝ) A = sInf s.measureOfNegatives

Tactic:
have hA₃ : s A = sInf s.measureOfNegatives := by
    apply le_antisymm
    · refine le_of_tendsto_of_tendsto tendsto_const_nhds hf₂ (Eventually.of_forall fun n => ?_)
      rw [← (hB n).2, hA, ← Set.diff_union_of_subset (Set.subset_iUnion _ n),
        of_union Set.disjoint_sdiff_left _ (hB₁ n)]
      · refine add_le_of_nonpos_left ?_
        have : s ≤[A] 0 :=
          restrict_le_restrict_iUnion _ _ hB₁ fun m =>
            let ⟨_, h⟩ := (hB m).1
            h
        refine
          nonpos_of_restrict_le_zero _ (restrict_le_zero_subset _ ?_ Set.diff_subset this)
        exact MeasurableSet.iUnion hB₁
      · exact (MeasurableSet.iUnion hB₁).diff (hB₁ n)
    · exact csInf_le bddBelow_measureOfNegatives ⟨A, ⟨hA₁, hA₂⟩, rfl⟩
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : (n : ℕ) → Set α
hB :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set α)) {B : Set α | MeasurableSet B ∧ s ≤[B] 0} (B n) ∧ (↑s : Set α → ℝ) (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), s ≤[B n] 0
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : s ≤[A] 0
hA₃ : (↑s : Set α → ℝ) A = sInf s.measureOfNegatives
⊢ ∃ (i : Set α), MeasurableSet i ∧ 0 ≤[i] s ∧ s ≤[iᶜ] 0

Tactic:
⟨Aᶜ, hA₁.compl, ?_, (compl_compl A).symm ▸ hA₂⟩

Premises used: compl_compl, Compl.compl, Eq.rec, MeasurableSet.compl, And.intro, Exists.intro, Eq.symm
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : (n : ℕ) → Set α
hB :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set α)) {B : Set α | MeasurableSet B ∧ s ≤[B] 0} (B n) ∧ (↑s : Set α → ℝ) (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), s ≤[B n] 0
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : s ≤[A] 0
hA₃ : (↑s : Set α → ℝ) A = sInf s.measureOfNegatives
refine : 0 ≤[Aᶜ] s
⊢ ∃ (i : Set α), MeasurableSet i ∧ 0 ≤[i] s ∧ s ≤[iᶜ] 0

Tactic:
refine ⟨Aᶜ, hA₁.compl, ?_, (compl_compl A).symm ▸ hA₂⟩
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : (n : ℕ) → Set α
hB :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set α)) {B : Set α | MeasurableSet B ∧ s ≤[B] 0} (B n) ∧ (↑s : Set α → ℝ) (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), s ≤[B n] 0
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : s ≤[A] 0
hA₃ : (↑s : Set α → ℝ) A = sInf s.measureOfNegatives
rw : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ Aᶜ → (↑0 : Set α → ℝ) j ≤ (↑s : Set α → ℝ) j
⊢ 0 ≤[Aᶜ] s

Tactic:
rw [restrict_le_restrict_iff _ _ hA₁.compl]

Premises used: MeasurableSet.compl, MeasureTheory.VectorMeasure.restrict_le_restrict_iff
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : (n : ℕ) → Set α
hB :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set α)) {B : Set α | MeasurableSet B ∧ s ≤[B] 0} (B n) ∧ (↑s : Set α → ℝ) (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), s ≤[B n] 0
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : s ≤[A] 0
hA₃ : (↑s : Set α → ℝ) A = sInf s.measureOfNegatives
C : Set α
_ : MeasurableSet C → C ⊆ Aᶜ → (↑0 : Set α → ℝ) C ≤ (↑s : Set α → ℝ) C
⊢ MeasurableSet C → C ⊆ Aᶜ → (↑0 : Set α → ℝ) C ≤ (↑s : Set α → ℝ) C

Tactic:
_
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : (n : ℕ) → Set α
hB :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set α)) {B : Set α | MeasurableSet B ∧ s ≤[B] 0} (B n) ∧ (↑s : Set α → ℝ) (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), s ≤[B n] 0
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : s ≤[A] 0
hA₃ : (↑s : Set α → ℝ) A = sInf s.measureOfNegatives
C : Set α
h : MeasurableSet C
hC₁ : C ⊆ Aᶜ
by_contra! : ∀ (hC₂ : (↑s : Set α → ℝ) C < (↑0 : Set α → ℝ) C), False
⊢ (↑0 : Set α → ℝ) C ≤ (↑s : Set α → ℝ) C

Tactic:
by_contra! hC₂
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : (n : ℕ) → Set α
hB :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set α)) {B : Set α | MeasurableSet B ∧ s ≤[B] 0} (B n) ∧ (↑s : Set α → ℝ) (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), s ≤[B n] 0
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : s ≤[A] 0
hA₃ : (↑s : Set α → ℝ) A = sInf s.measureOfNegatives
C : Set α
h : MeasurableSet C
hC₁ : C ⊆ Aᶜ
hC₂ : (↑s : Set α → ℝ) C < (↑0 : Set α → ℝ) C
rcases : ∀ (D : Set α) (hD₁ : MeasurableSet D) (hD : D ⊆ C) (hD₂ : s ≤[D] 0) (hD₃ : (↑s : Set α → ℝ) D < 0), False
⊢ False

Tactic:
rcases exists_subset_restrict_nonpos hC₂ with ⟨D, hD₁, hD, hD₂, hD₃⟩

Premises used: MeasureTheory.SignedMeasure.exists_subset_restrict_nonpos
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : (n : ℕ) → Set α
hB :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set α)) {B : Set α | MeasurableSet B ∧ s ≤[B] 0} (B n) ∧ (↑s : Set α → ℝ) (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), s ≤[B n] 0
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : s ≤[A] 0
hA₃ : (↑s : Set α → ℝ) A = sInf s.measureOfNegatives
C : Set α
h : MeasurableSet C
hC₁ : C ⊆ Aᶜ
hC₂ : (↑s : Set α → ℝ) C < (↑0 : Set α → ℝ) C
D : Set α
hD₁ : MeasurableSet D
hD : D ⊆ C
hD₂ : s ≤[D] 0
hD₃ : (↑s : Set α → ℝ) D < 0
rw : (↑s : Set α → ℝ) A + (↑s : Set α → ℝ) D < (↑s : Set α → ℝ) A
⊢ (↑s : Set α → ℝ) (A ∪ D) < sInf s.measureOfNegatives

Tactic:
rw [← hA₃,
      of_union (Set.disjoint_of_subset_right (Set.Subset.trans hD hC₁) disjoint_compl_right) hA₁
        hD₁]

Premises used: Set.Subset.trans, MeasureTheory.VectorMeasure.of_union, disjoint_compl_right, Set.disjoint_of_subset_right