awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
linarith :
  (↑s : Set α → ℝ) A ≤ (↑s : Set α → ℝ) A + (↑s : Set α → ℝ) D →
    (↑s : Set α → ℝ) D - 0 + ((↑s : Set α → ℝ) A - ((↑s : Set α → ℝ) A + (↑s : Set α → ℝ) D)) = 0
⊢ (↑s : Set α → ℝ) A + (↑s : Set α → ℝ) D < (↑s : Set α → ℝ) A

Tactic:
linarith
-- 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
⊢ (↑s : Set α → ℝ) (A ∪ D) < sInf s.measureOfNegatives

Tactic:
have : s (A ∪ D) < sInf s.measureOfNegatives := by
    rw [← hA₃,
      of_union (Set.disjoint_of_subset_right (Set.Subset.trans hD hC₁) disjoint_compl_right) hA₁
        hD₁]
    linarith
-- 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
this : (↑s : Set α → ℝ) (A ∪ D) < sInf s.measureOfNegatives
⊢ False

Tactic:
not_le.2 this ?_

Premises used: not_le, Iff.mpr
-- 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
this : (↑s : Set α → ℝ) (A ∪ D) < sInf s.measureOfNegatives
refine : sInf s.measureOfNegatives ≤ (↑s : Set α → ℝ) (A ∪ D)
⊢ False

Tactic:
refine not_le.2 this ?_

Premises used: not_le, Iff.mpr
-- 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
this : (↑s : Set α → ℝ) (A ∪ D) < sInf s.measureOfNegatives
⊢ sInf s.measureOfNegatives ≤ (↑s : Set α → ℝ) (A ∪ D)

Tactic:
csInf_le bddBelow_measureOfNegatives ⟨A ∪ D, ⟨?_, ?_⟩, rfl⟩

Premises used: MeasureTheory.SignedMeasure.bddBelow_measureOfNegatives, And.intro, Exists.intro, Union.union, 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
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
this : (↑s : Set α → ℝ) (A ∪ D) < sInf s.measureOfNegatives
refine_1 : MeasurableSet (A ∪ D)
refine_2 : s ≤[A ∪ D] 0
⊢ sInf s.measureOfNegatives ≤ (↑s : Set α → ℝ) (A ∪ D)

Tactic:
refine csInf_le bddBelow_measureOfNegatives ⟨A ∪ D, ⟨?_, ?_⟩, rfl⟩

Premises used: MeasureTheory.SignedMeasure.bddBelow_measureOfNegatives, And.intro, Exists.intro, Union.union, 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
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
this : (↑s : Set α → ℝ) (A ∪ D) < sInf s.measureOfNegatives
⊢ MeasurableSet (A ∪ D)

Tactic:
hA₁.union hD₁

Premises used: MeasurableSet.union
-- 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
this : (↑s : Set α → ℝ) (A ∪ D) < sInf s.measureOfNegatives
⊢ MeasurableSet (A ∪ D)

Tactic:
exact hA₁.union hD₁

Premises used: MeasurableSet.union
-- 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
this : (↑s : Set α → ℝ) (A ∪ D) < sInf s.measureOfNegatives
⊢ s ≤[A ∪ D] 0

Tactic:
restrict_le_restrict_union _ _ hA₁ hA₂ hD₁ hD₂

Premises used: MeasureTheory.VectorMeasure.restrict_le_restrict_union
-- 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
this : (↑s : Set α → ℝ) (A ∪ D) < sInf s.measureOfNegatives
⊢ s ≤[A ∪ D] 0

Tactic:
exact restrict_le_restrict_union _ _ hA₁ hA₂ hD₁ hD₂

Premises used: MeasureTheory.VectorMeasure.restrict_le_restrict_union
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
⊢ ∃ (i : Set α) (j : Set α), MeasurableSet i ∧ 0 ≤[i] s ∧ MeasurableSet j ∧ s ≤[j] 0 ∧ IsCompl i j

Tactic:
let ⟨i, hi₁, hi₂, hi₃⟩ := exists_compl_positive_negative s
  ⟨i, iᶜ, hi₁, hi₂, hi₁.compl, hi₃, isCompl_compl⟩

Premises used: MeasureTheory.SignedMeasure.exists_compl_positive_negative, MeasurableSet, Compl.compl, Exists, LE.le, MeasurableSet.compl, And, IsCompl, And.intro, Exists.intro, isCompl_compl, OfNat.ofNat, MeasureTheory.VectorMeasure.restrict, _private.0.MeasureTheory.SignedMeasure.exists_isCompl_positive_negative.match_1
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' : 0 ≤[i] s ∧ s ≤[iᶜ] 0
hj' : 0 ≤[j] s ∧ s ≤[jᶜ] 0
rw :
  ∀
    (hi' :
      (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → (↑0 : Set α → ℝ) j ≤ (↑s : Set α → ℝ) j) ∧
        ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → (↑s : Set α → ℝ) j ≤ (↑0 : Set α → ℝ) j)
    (hj' :
      (∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ j → (↑0 : Set α → ℝ) j_1 ≤ (↑s : Set α → ℝ) j_1) ∧
        ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → (↑s : Set α → ℝ) j_1 ≤ (↑0 : Set α → ℝ) j_1),
    (↑s : Set α → ℝ) (i ∆ j) = 0 ∧ (↑s : Set α → ℝ) (iᶜ ∆ jᶜ) = 0
rw₁ :
  ∀
    (hi' :
      (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → (↑0 : Set α → ℝ) j ≤ (↑s : Set α → ℝ) j) ∧
        ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → (↑s : Set α → ℝ) j ≤ (↑0 : Set α → ℝ) j)
    (hj' : 0 ≤[j] s ∧ ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → (↑s : Set α → ℝ) j_1 ≤ (↑0 : Set α → ℝ) j_1),
    MeasurableSet j
rw₂ :
  ∀ (hi' : 0 ≤[i] s ∧ ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → (↑s : Set α → ℝ) j ≤ (↑0 : Set α → ℝ) j)
    (hj' : 0 ≤[j] s ∧ ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → (↑s : Set α → ℝ) j_1 ≤ (↑0 : Set α → ℝ) j_1),
    MeasurableSet i
rw₃ :
  ∀ (hi' : 0 ≤[i] s ∧ ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → (↑s : Set α → ℝ) j ≤ (↑0 : Set α → ℝ) j)
    (hj' : 0 ≤[j] s ∧ s ≤[jᶜ] 0), MeasurableSet jᶜ
rw₄ : MeasurableSet iᶜ
⊢ (↑s : Set α → ℝ) (i ∆ j) = 0 ∧ (↑s : Set α → ℝ) (iᶜ ∆ jᶜ) = 0

Tactic:
rw [restrict_le_restrict_iff s 0, restrict_le_restrict_iff 0 s] at hi' hj'

Premises used: OfNat.ofNat, MeasureTheory.VectorMeasure.restrict_le_restrict_iff
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' :
  (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → (↑0 : Set α → ℝ) j ≤ (↑s : Set α → ℝ) j) ∧
    ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → (↑s : Set α → ℝ) j ≤ (↑0 : Set α → ℝ) j
hj' :
  (∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ j → (↑0 : Set α → ℝ) j_1 ≤ (↑s : Set α → ℝ) j_1) ∧
    ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → (↑s : Set α → ℝ) j_1 ≤ (↑0 : Set α → ℝ) j_1
left : (↑s : Set α → ℝ) (i ∆ j) = 0
right : (↑s : Set α → ℝ) (iᶜ ∆ jᶜ) = 0
⊢ (↑s : Set α → ℝ) (i ∆ j) = 0 ∧ (↑s : Set α → ℝ) (iᶜ ∆ jᶜ) = 0

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' :
  (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → (↑0 : Set α → ℝ) j ≤ (↑s : Set α → ℝ) j) ∧
    ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → (↑s : Set α → ℝ) j ≤ (↑0 : Set α → ℝ) j
hj' :
  (∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ j → (↑0 : Set α → ℝ) j_1 ≤ (↑s : Set α → ℝ) j_1) ∧
    ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → (↑s : Set α → ℝ) j_1 ≤ (↑0 : Set α → ℝ) j_1
left : Disjoint (jᶜ ∩ i) (iᶜ ∩ j)
left₁ : MeasurableSet (jᶜ ∩ i)
left₂ : MeasurableSet (iᶜ ∩ j)
⊢ (↑s : Set α → ℝ) (i ∆ j) = 0

Tactic:
rw [Set.symmDiff_def, Set.diff_eq_compl_inter, Set.diff_eq_compl_inter, of_union,
      le_antisymm (hi'.2 (hi.compl.inter hj) Set.inter_subset_left)
        (hj'.1 (hi.compl.inter hj) Set.inter_subset_right),
      le_antisymm (hj'.2 (hj.compl.inter hi) Set.inter_subset_left)
        (hi'.1 (hj.compl.inter hi) Set.inter_subset_right),
      zero_apply, zero_apply, zero_add]

Premises used: Set.symmDiff_def, MeasureTheory.VectorMeasure.zero_apply, Set.diff_eq_compl_inter, Set.inter_subset_left, MeasureTheory.VectorMeasure.of_union, zero_add, MeasurableSet.compl, le_antisymm, And.right, And.left, Set.inter_subset_right, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' :
  (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → (↑0 : Set α → ℝ) j ≤ (↑s : Set α → ℝ) j) ∧
    ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → (↑s : Set α → ℝ) j ≤ (↑0 : Set α → ℝ) j
hj' :
  (∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ j → (↑0 : Set α → ℝ) j_1 ≤ (↑s : Set α → ℝ) j_1) ∧
    ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → (↑s : Set α → ℝ) j_1 ≤ (↑0 : Set α → ℝ) j_1
⊢ Disjoint (jᶜ ∩ i) (iᶜ ∩ j)

Tactic:
Set.disjoint_of_subset_left Set.inter_subset_left
          (Set.disjoint_of_subset_right Set.inter_subset_right
            (disjoint_comm.1 (IsCompl.disjoint isCompl_compl)))

Premises used: Set.disjoint_of_subset_left, disjoint_comm, Set.inter_subset_left, Iff.mp, isCompl_compl, IsCompl.disjoint, Set.disjoint_of_subset_right, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' :
  (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → (↑0 : Set α → ℝ) j ≤ (↑s : Set α → ℝ) j) ∧
    ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → (↑s : Set α → ℝ) j ≤ (↑0 : Set α → ℝ) j
hj' :
  (∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ j → (↑0 : Set α → ℝ) j_1 ≤ (↑s : Set α → ℝ) j_1) ∧
    ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → (↑s : Set α → ℝ) j_1 ≤ (↑0 : Set α → ℝ) j_1
⊢ Disjoint (jᶜ ∩ i) (iᶜ ∩ j)

Tactic:
exact
        Set.disjoint_of_subset_left Set.inter_subset_left
          (Set.disjoint_of_subset_right Set.inter_subset_right
            (disjoint_comm.1 (IsCompl.disjoint isCompl_compl)))

Premises used: Set.disjoint_of_subset_left, disjoint_comm, Set.inter_subset_left, Iff.mp, isCompl_compl, IsCompl.disjoint, Set.disjoint_of_subset_right, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' :
  (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → (↑0 : Set α → ℝ) j ≤ (↑s : Set α → ℝ) j) ∧
    ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → (↑s : Set α → ℝ) j ≤ (↑0 : Set α → ℝ) j
hj' :
  (∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ j → (↑0 : Set α → ℝ) j_1 ≤ (↑s : Set α → ℝ) j_1) ∧
    ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → (↑s : Set α → ℝ) j_1 ≤ (↑0 : Set α → ℝ) j_1
⊢ MeasurableSet (jᶜ ∩ i)

Tactic:
hj.compl.inter hi

Premises used: MeasurableSet.compl, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' :
  (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → (↑0 : Set α → ℝ) j ≤ (↑s : Set α → ℝ) j) ∧
    ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → (↑s : Set α → ℝ) j ≤ (↑0 : Set α → ℝ) j
hj' :
  (∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ j → (↑0 : Set α → ℝ) j_1 ≤ (↑s : Set α → ℝ) j_1) ∧
    ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → (↑s : Set α → ℝ) j_1 ≤ (↑0 : Set α → ℝ) j_1
⊢ MeasurableSet (jᶜ ∩ i)

Tactic:
exact hj.compl.inter hi

Premises used: MeasurableSet.compl, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' :
  (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → (↑0 : Set α → ℝ) j ≤ (↑s : Set α → ℝ) j) ∧
    ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → (↑s : Set α → ℝ) j ≤ (↑0 : Set α → ℝ) j
hj' :
  (∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ j → (↑0 : Set α → ℝ) j_1 ≤ (↑s : Set α → ℝ) j_1) ∧
    ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → (↑s : Set α → ℝ) j_1 ≤ (↑0 : Set α → ℝ) j_1
⊢ MeasurableSet (iᶜ ∩ j)

Tactic:
hi.compl.inter hj

Premises used: MeasurableSet.compl, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' :
  (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → (↑0 : Set α → ℝ) j ≤ (↑s : Set α → ℝ) j) ∧
    ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → (↑s : Set α → ℝ) j ≤ (↑0 : Set α → ℝ) j
hj' :
  (∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ j → (↑0 : Set α → ℝ) j_1 ≤ (↑s : Set α → ℝ) j_1) ∧
    ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → (↑s : Set α → ℝ) j_1 ≤ (↑0 : Set α → ℝ) j_1
⊢ MeasurableSet (iᶜ ∩ j)

Tactic:
exact hi.compl.inter hj

Premises used: MeasurableSet.compl, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' :
  (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → (↑0 : Set α → ℝ) j ≤ (↑s : Set α → ℝ) j) ∧
    ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → (↑s : Set α → ℝ) j ≤ (↑0 : Set α → ℝ) j
hj' :
  (∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ j → (↑0 : Set α → ℝ) j_1 ≤ (↑s : Set α → ℝ) j_1) ∧
    ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → (↑s : Set α → ℝ) j_1 ≤ (↑0 : Set α → ℝ) j_1
right : Disjoint (j ∩ iᶜ) (i ∩ jᶜ)
right₁ : MeasurableSet (j ∩ iᶜ)
right₂ : MeasurableSet (i ∩ jᶜ)
⊢ (↑s : Set α → ℝ) (iᶜ ∆ jᶜ) = 0

Tactic:
rw [Set.symmDiff_def, Set.diff_eq_compl_inter, Set.diff_eq_compl_inter, compl_compl,
      compl_compl, of_union,
      le_antisymm (hi'.2 (hj.inter hi.compl) Set.inter_subset_right)
        (hj'.1 (hj.inter hi.compl) Set.inter_subset_left),
      le_antisymm (hj'.2 (hi.inter hj.compl) Set.inter_subset_right)
        (hi'.1 (hi.inter hj.compl) Set.inter_subset_left),
      zero_apply, zero_apply, zero_add]

Premises used: compl_compl, Set.symmDiff_def, MeasureTheory.VectorMeasure.zero_apply, Set.diff_eq_compl_inter, Set.inter_subset_left, MeasureTheory.VectorMeasure.of_union, zero_add, MeasurableSet.compl, le_antisymm, And.right, And.left, Set.inter_subset_right, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' :
  (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → (↑0 : Set α → ℝ) j ≤ (↑s : Set α → ℝ) j) ∧
    ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → (↑s : Set α → ℝ) j ≤ (↑0 : Set α → ℝ) j
hj' :
  (∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ j → (↑0 : Set α → ℝ) j_1 ≤ (↑s : Set α → ℝ) j_1) ∧
    ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → (↑s : Set α → ℝ) j_1 ≤ (↑0 : Set α → ℝ) j_1
⊢ Disjoint (j ∩ iᶜ) (i ∩ jᶜ)

Tactic:
Set.disjoint_of_subset_left Set.inter_subset_left
          (Set.disjoint_of_subset_right Set.inter_subset_right
            (IsCompl.disjoint isCompl_compl))

Premises used: Set.disjoint_of_subset_left, Set.inter_subset_left, isCompl_compl, IsCompl.disjoint, Set.disjoint_of_subset_right, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' :
  (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → (↑0 : Set α → ℝ) j ≤ (↑s : Set α → ℝ) j) ∧
    ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → (↑s : Set α → ℝ) j ≤ (↑0 : Set α → ℝ) j
hj' :
  (∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ j → (↑0 : Set α → ℝ) j_1 ≤ (↑s : Set α → ℝ) j_1) ∧
    ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → (↑s : Set α → ℝ) j_1 ≤ (↑0 : Set α → ℝ) j_1
⊢ Disjoint (j ∩ iᶜ) (i ∩ jᶜ)

Tactic:
exact
        Set.disjoint_of_subset_left Set.inter_subset_left
          (Set.disjoint_of_subset_right Set.inter_subset_right
            (IsCompl.disjoint isCompl_compl))

Premises used: Set.disjoint_of_subset_left, Set.inter_subset_left, isCompl_compl, IsCompl.disjoint, Set.disjoint_of_subset_right, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' :
  (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → (↑0 : Set α → ℝ) j ≤ (↑s : Set α → ℝ) j) ∧
    ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → (↑s : Set α → ℝ) j ≤ (↑0 : Set α → ℝ) j
hj' :
  (∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ j → (↑0 : Set α → ℝ) j_1 ≤ (↑s : Set α → ℝ) j_1) ∧
    ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → (↑s : Set α → ℝ) j_1 ≤ (↑0 : Set α → ℝ) j_1
⊢ MeasurableSet (j ∩ iᶜ)

Tactic:
hj.inter hi.compl

Premises used: MeasurableSet.compl, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' :
  (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → (↑0 : Set α → ℝ) j ≤ (↑s : Set α → ℝ) j) ∧
    ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → (↑s : Set α → ℝ) j ≤ (↑0 : Set α → ℝ) j
hj' :
  (∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ j → (↑0 : Set α → ℝ) j_1 ≤ (↑s : Set α → ℝ) j_1) ∧
    ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → (↑s : Set α → ℝ) j_1 ≤ (↑0 : Set α → ℝ) j_1
⊢ MeasurableSet (j ∩ iᶜ)

Tactic:
exact hj.inter hi.compl

Premises used: MeasurableSet.compl, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' :
  (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → (↑0 : Set α → ℝ) j ≤ (↑s : Set α → ℝ) j) ∧
    ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → (↑s : Set α → ℝ) j ≤ (↑0 : Set α → ℝ) j
hj' :
  (∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ j → (↑0 : Set α → ℝ) j_1 ≤ (↑s : Set α → ℝ) j_1) ∧
    ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → (↑s : Set α → ℝ) j_1 ≤ (↑0 : Set α → ℝ) j_1
⊢ MeasurableSet (i ∩ jᶜ)

Tactic:
hi.inter hj.compl

Premises used: MeasurableSet.compl, MeasurableSet.inter