awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
inst_5 : CompactIccSpace α
hα : MeasurableSpace α
inst_6 : BorelSpace α
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : CompleteSpace E
f : α → E
hf : BoundedVariationOn f univ
a : α
⊢ (↑hf.vectorMeasure : Set α → E) (Iic a) = Function.rightLim f a - limUnder atBot f

Tactic:
have := hf.vectorMeasure_Iic a
-- Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
inst_5 : CompactIccSpace α
hα : MeasurableSpace α
inst_6 : BorelSpace α
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : CompleteSpace E
f : α → E
hf : BoundedVariationOn f univ
a : α
this : (↑hf.vectorMeasure : Set α → E) (Iio a ∪ Icc a a) = Function.rightLim f a - limUnder atBot f
⊢ Disjoint (Iio a) (Icc a a)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
inst_5 : CompactIccSpace α
hα : MeasurableSpace α
inst_6 : BorelSpace α
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : CompleteSpace E
f : α → E
hf : BoundedVariationOn f univ
a : α
this : (↑hf.vectorMeasure : Set α → E) (Iic a) = Function.rightLim f a - limUnder atBot f
⊢ (↑hf.vectorMeasure : Set α → E) (Iio a) + (Function.rightLim f a - Function.leftLim f a) =
    Function.rightLim f a - limUnder atBot f

Tactic:
rw [← Iio_union_Icc_eq_Iic le_rfl, VectorMeasure.of_union (by simp) measurableSet_Iio
    measurableSet_Icc, hf.vectorMeasure_Icc le_rfl] at this

Premises used: le_rfl, measurableSet_Iio, MeasureTheory.VectorMeasure.of_union, BoundedVariationOn.vectorMeasure_Icc, measurableSet_Icc, Set.Iio_union_Icc_eq_Iic
-- Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
inst_5 : CompactIccSpace α
hα : MeasurableSpace α
inst_6 : BorelSpace α
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : CompleteSpace E
f : α → E
hf : BoundedVariationOn f univ
a : α
this :
  (↑hf.vectorMeasure : Set α → E) (Iio a) + (Function.rightLim f a - Function.leftLim f a) =
    Function.rightLim f a - limUnder atBot f
⊢ (↑hf.vectorMeasure : Set α → E) (Iio a) = Function.leftLim f a - limUnder atBot f

Tactic:
grind
-- Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
inst_5 : CompactIccSpace α
hα : MeasurableSpace α
inst_6 : BorelSpace α
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : CompleteSpace E
f : α → E
hf : BoundedVariationOn f univ
inl : ∀ (hα_1 : IsEmpty α), (↑hf.vectorMeasure : Set α → E) univ = limUnder atTop f - limUnder atBot f
inr : ∀ (hα_1 : Nonempty α), (↑hf.vectorMeasure : Set α → E) univ = limUnder atTop f - limUnder atBot f
⊢ (↑hf.vectorMeasure : Set α → E) univ = limUnder atTop f - limUnder atBot f

Tactic:
rcases isEmpty_or_nonempty α with hα | hα

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
inst_5 : CompactIccSpace α
hα_1 : MeasurableSpace α
inst_6 : BorelSpace α
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : CompleteSpace E
f : α → E
hf : BoundedVariationOn f univ
hα : IsEmpty α
⊢ (↑hf.vectorMeasure : Set α → E) univ = limUnder atTop f - limUnder atBot f

Tactic:
simp [eq_empty_of_isEmpty, filter_eq_bot_of_isEmpty]

Premises used: Set.eq_empty_of_isEmpty, Filter.filter_eq_bot_of_isEmpty
-- Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
inst_5 : CompactIccSpace α
hα_1 : MeasurableSpace α
inst_6 : BorelSpace α
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : CompleteSpace E
f : α → E
hf : BoundedVariationOn f univ
hα : Nonempty α
⊢ Disjoint (Iio hα.some) (Ici hα.some)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
inst_5 : CompactIccSpace α
hα_1 : MeasurableSpace α
inst_6 : BorelSpace α
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : CompleteSpace E
f : α → E
hf : BoundedVariationOn f univ
hα : Nonempty α
inr :
  Function.leftLim f hα.some - limUnder atBot f + (limUnder atTop f - Function.leftLim f hα.some) =
    limUnder atTop f - limUnder atBot f
⊢ (↑hf.vectorMeasure : Set α → E) univ = limUnder atTop f - limUnder atBot f

Tactic:
rw [← Iio_union_Ici (a := hα.some), VectorMeasure.of_union (by simp) measurableSet_Iio
    measurableSet_Ici, hf.vectorMeasure_Iio, hf.vectorMeasure_Ici]

Premises used: Set.Iio_union_Ici, measurableSet_Iio, MeasureTheory.VectorMeasure.of_union, BoundedVariationOn.vectorMeasure_Iio, BoundedVariationOn.vectorMeasure_Ici, measurableSet_Ici
-- Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
inst_5 : CompactIccSpace α
hα_1 : MeasurableSpace α
inst_6 : BorelSpace α
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : CompleteSpace E
f : α → E
hf : BoundedVariationOn f univ
hα : Nonempty α
⊢ Function.leftLim f hα.some - limUnder atBot f + (limUnder atTop f - Function.leftLim f hα.some) =
    limUnder atTop f - limUnder atBot f

Tactic:
abel
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬s ≤[i] 0
⊢ ∃ (n : ℕ), s.ExistsOneDivLT i n

Tactic:
let ⟨k, hj₁, hj₂, hj⟩ := exists_pos_measure_of_not_restrict_le_zero s hi
  let ⟨n, hn⟩ := exists_nat_one_div_lt hj
  ⟨n, k, hj₂, hj₁, hn⟩

Premises used: exists_nat_one_div_lt, _private.0.MeasureTheory.SignedMeasure.existsNatOneDivLTMeasure_of_not_negative.match_1, Exists, And.intro, Exists.intro, _private.0.MeasureTheory.SignedMeasure.ExistsOneDivLT, _private.0.MeasureTheory.SignedMeasure.existsNatOneDivLTMeasure_of_not_negative.match_2, MeasureTheory.VectorMeasure.exists_pos_measure_of_not_restrict_le_zero
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬s ≤[i] 0
rw : s.ExistsOneDivLT i (Nat.find (p := s.ExistsOneDivLT i) ⋯)
⊢ s.ExistsOneDivLT i (s.findExistsOneDivLT i)

Tactic:
rw [findExistsOneDivLT, dif_pos hi]

Premises used: _private.0.MeasureTheory.SignedMeasure.findExistsOneDivLT, dif_pos
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬s ≤[i] 0
⊢ s.ExistsOneDivLT i (Nat.find (p := s.ExistsOneDivLT i) ⋯)

Tactic:
Nat.find_spec (existsNatOneDivLTMeasure_of_not_negative hi)

Premises used: _private.0.MeasureTheory.SignedMeasure.existsNatOneDivLTMeasure_of_not_negative, Nat.find_spec
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬s ≤[i] 0
⊢ s.ExistsOneDivLT i (Nat.find (p := s.ExistsOneDivLT i) ⋯)

Tactic:
convert! Nat.find_spec (existsNatOneDivLTMeasure_of_not_negative hi)
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬s ≤[i] 0
m : ℕ
hm : m < s.findExistsOneDivLT i
⊢ m < Nat.find (p := s.ExistsOneDivLT i) ⋯

Tactic:
rw [findExistsOneDivLT, dif_pos hi] at hm

Premises used: _private.0.MeasureTheory.SignedMeasure.findExistsOneDivLT, dif_pos
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬s ≤[i] 0
m : ℕ
hm : m < Nat.find (p := s.ExistsOneDivLT i) ⋯
⊢ ¬s.ExistsOneDivLT i m

Tactic:
Nat.find_min _ hm

Premises used: Nat.find_min
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬s ≤[i] 0
m : ℕ
hm : m < Nat.find (p := s.ExistsOneDivLT i) ⋯
⊢ ¬s.ExistsOneDivLT i m

Tactic:
exact Nat.find_min _ hm

Premises used: Nat.find_min
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬s ≤[i] 0
m : ℕ
hm : m < s.findExistsOneDivLT i
rw : ∀ (hm : m < if hi : ¬s ≤[i] 0 then Nat.find (p := s.ExistsOneDivLT i) ⋯ else 0), ¬s.ExistsOneDivLT i m
rw₁ rw₂ rw₃ : ∀ (hm : m < Nat.find (p := s.ExistsOneDivLT i) ⋯), ¬s.ExistsOneDivLT i m
⊢ ¬s.ExistsOneDivLT i m

Tactic:
classical
  rw [findExistsOneDivLT, dif_pos hi] at hm
  exact Nat.find_min _ hm

Premises used: _private.0.MeasureTheory.SignedMeasure.findExistsOneDivLT, dif_pos, Nat.find_min
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬s ≤[i] 0
rw :
  Classical.choose (p := fun (x : Set α) ↦
        x ⊆ i ∧ MeasurableSet x ∧ 1 / HAdd.hAdd (α := ℝ) (↑(s.findExistsOneDivLT i) : ℝ) 1 < (↑s : Set α → ℝ) x) ⋯ ⊆
      i ∧
    MeasurableSet
        (Classical.choose (p := fun (x : Set α) ↦
          x ⊆ i ∧ MeasurableSet x ∧ 1 / HAdd.hAdd (α := ℝ) (↑(s.findExistsOneDivLT i) : ℝ) 1 < (↑s : Set α → ℝ) x) ⋯) ∧
      1 / HAdd.hAdd (α := ℝ) (↑(s.findExistsOneDivLT i) : ℝ) 1 <
        (↑s : Set α → ℝ)
          (Classical.choose (p := fun (x : Set α) ↦
            x ⊆ i ∧ MeasurableSet x ∧ 1 / HAdd.hAdd (α := ℝ) (↑(s.findExistsOneDivLT i) : ℝ) 1 < (↑s : Set α → ℝ) x) ⋯)
⊢ s.someExistsOneDivLT i ⊆ i ∧
    MeasurableSet (s.someExistsOneDivLT i) ∧
      1 / HAdd.hAdd (α := ℝ) (↑(s.findExistsOneDivLT i) : ℝ) 1 < (↑s : Set α → ℝ) (s.someExistsOneDivLT i)

Tactic:
rw [someExistsOneDivLT, dif_pos hi]

Premises used: dif_pos, _private.0.MeasureTheory.SignedMeasure.someExistsOneDivLT
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬s ≤[i] 0
⊢ Classical.choose (p := fun (x : Set α) ↦
        x ⊆ i ∧ MeasurableSet x ∧ 1 / HAdd.hAdd (α := ℝ) (↑(s.findExistsOneDivLT i) : ℝ) 1 < (↑s : Set α → ℝ) x) ⋯ ⊆
      i ∧
    MeasurableSet
        (Classical.choose (p := fun (x : Set α) ↦
          x ⊆ i ∧ MeasurableSet x ∧ 1 / HAdd.hAdd (α := ℝ) (↑(s.findExistsOneDivLT i) : ℝ) 1 < (↑s : Set α → ℝ) x) ⋯) ∧
      1 / HAdd.hAdd (α := ℝ) (↑(s.findExistsOneDivLT i) : ℝ) 1 <
        (↑s : Set α → ℝ)
          (Classical.choose (p := fun (x : Set α) ↦
            x ⊆ i ∧ MeasurableSet x ∧ 1 / HAdd.hAdd (α := ℝ) (↑(s.findExistsOneDivLT i) : ℝ) 1 < (↑s : Set α → ℝ) x) ⋯)

Tactic:
Classical.choose_spec (findExistsOneDivLT_spec hi)

Premises used: Classical.choose_spec, _private.0.MeasureTheory.SignedMeasure.findExistsOneDivLT_spec
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬s ≤[i] 0
⊢ Classical.choose (p := fun (x : Set α) ↦
        x ⊆ i ∧ MeasurableSet x ∧ 1 / HAdd.hAdd (α := ℝ) (↑(s.findExistsOneDivLT i) : ℝ) 1 < (↑s : Set α → ℝ) x) ⋯ ⊆
      i ∧
    MeasurableSet
        (Classical.choose (p := fun (x : Set α) ↦
          x ⊆ i ∧ MeasurableSet x ∧ 1 / HAdd.hAdd (α := ℝ) (↑(s.findExistsOneDivLT i) : ℝ) 1 < (↑s : Set α → ℝ) x) ⋯) ∧
      1 / HAdd.hAdd (α := ℝ) (↑(s.findExistsOneDivLT i) : ℝ) 1 <
        (↑s : Set α → ℝ)
          (Classical.choose (p := fun (x : Set α) ↦
            x ⊆ i ∧ MeasurableSet x ∧ 1 / HAdd.hAdd (α := ℝ) (↑(s.findExistsOneDivLT i) : ℝ) 1 < (↑s : Set α → ℝ) x) ⋯)

Tactic:
exact Classical.choose_spec (findExistsOneDivLT_spec hi)

Premises used: Classical.choose_spec, _private.0.MeasureTheory.SignedMeasure.findExistsOneDivLT_spec
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
pos : ∀ (hi : ¬s ≤[i] 0), s.someExistsOneDivLT i ⊆ i
neg : ∀ (hi : ¬¬s ≤[i] 0), s.someExistsOneDivLT i ⊆ i
⊢ s.someExistsOneDivLT i ⊆ i

Tactic:
by_cases hi : ¬s ≤[i] 0
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬s ≤[i] 0
⊢ s.someExistsOneDivLT i ⊆ i

Tactic:
let ⟨h, _⟩ := someExistsOneDivLT_spec hi
      h

Premises used: _private.0.MeasureTheory.SignedMeasure.someExistsOneDivLT_spec, HasSubset.Subset, _private.0.MeasureTheory.SignedMeasure.someExistsOneDivLT_subset.match_1, _private.0.MeasureTheory.SignedMeasure.someExistsOneDivLT
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬s ≤[i] 0
⊢ s.someExistsOneDivLT i ⊆ i

Tactic:
exact
      let ⟨h, _⟩ := someExistsOneDivLT_spec hi
      h
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬¬s ≤[i] 0
neg : ∅ ⊆ i
⊢ s.someExistsOneDivLT i ⊆ i

Tactic:
rw [someExistsOneDivLT, dif_neg hi]

Premises used: dif_neg, _private.0.MeasureTheory.SignedMeasure.someExistsOneDivLT
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬¬s ≤[i] 0
⊢ ∅ ⊆ i

Tactic:
Set.empty_subset _

Premises used: Set.empty_subset
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬¬s ≤[i] 0
⊢ ∅ ⊆ i

Tactic:
exact Set.empty_subset _

Premises used: Set.empty_subset
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i j : Set α
⊢ s.someExistsOneDivLT (i \ j) ⊆ i

Tactic:
someExistsOneDivLT_subset.trans Set.diff_subset

Premises used: _private.0.MeasureTheory.SignedMeasure.someExistsOneDivLT_subset, Set.diff_subset, HasSubset.Subset.trans
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
pos : ∀ (hi : ¬s ≤[i] 0), MeasurableSet (s.someExistsOneDivLT i)
neg : ∀ (hi : ¬¬s ≤[i] 0), MeasurableSet (s.someExistsOneDivLT i)
⊢ MeasurableSet (s.someExistsOneDivLT i)

Tactic:
by_cases hi : ¬s ≤[i] 0
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬s ≤[i] 0
⊢ MeasurableSet (s.someExistsOneDivLT i)

Tactic:
let ⟨_, h, _⟩ := someExistsOneDivLT_spec hi
      h

Premises used: MeasurableSet, _private.0.MeasureTheory.SignedMeasure.someExistsOneDivLT_spec, _private.0.MeasureTheory.SignedMeasure.someExistsOneDivLT_measurableSet.match_1, _private.0.MeasureTheory.SignedMeasure.someExistsOneDivLT
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬s ≤[i] 0
⊢ MeasurableSet (s.someExistsOneDivLT i)

Tactic:
exact
      let ⟨_, h, _⟩ := someExistsOneDivLT_spec hi
      h
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬¬s ≤[i] 0
neg : MeasurableSet.{u_1} (α := α) ∅
⊢ MeasurableSet (s.someExistsOneDivLT i)

Tactic:
rw [someExistsOneDivLT, dif_neg hi]

Premises used: dif_neg, _private.0.MeasureTheory.SignedMeasure.someExistsOneDivLT
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬¬s ≤[i] 0
⊢ MeasurableSet.{u_1} (α := α) ∅

Tactic:
MeasurableSet.empty

Premises used: MeasurableSet.empty
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬¬s ≤[i] 0
⊢ MeasurableSet.{u_1} (α := α) ∅

Tactic:
exact MeasurableSet.empty

Premises used: MeasurableSet.empty
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬s ≤[i] 0
⊢ 1 / HAdd.hAdd (α := ℝ) (↑(s.findExistsOneDivLT i) : ℝ) 1 < (↑s : Set α → ℝ) (s.someExistsOneDivLT i)

Tactic:
let ⟨_, _, h⟩ := someExistsOneDivLT_spec hi
  h

Premises used: MeasureTheory.VectorMeasure.measureOf', _private.0.MeasureTheory.SignedMeasure.findExistsOneDivLT, _private.0.MeasureTheory.SignedMeasure.someExistsOneDivLT_spec, HDiv.hDiv, Nat.cast, HAdd.hAdd, LT.lt, _private.0.MeasureTheory.SignedMeasure.someExistsOneDivLT_measurableSet.match_1, OfNat.ofNat, _private.0.MeasureTheory.SignedMeasure.someExistsOneDivLT
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
n : ℕ
rw rw₁ :
  s.someExistsOneDivLT
      (i \
        ⋃ (k : ℕ),
          ⋃ (H : k ≤ n),
            have this := ⋯;
            s.restrictNonposSeq i k) =
    s.someExistsOneDivLT (i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k)
⊢ s.restrictNonposSeq i n.succ = s.someExistsOneDivLT (i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k)

Tactic:
rw [restrictNonposSeq]

Premises used: _private.0.MeasureTheory.SignedMeasure.restrictNonposSeq
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
n : ℕ
zero : s.restrictNonposSeq i 0 ⊆ i
succ : ∀ (n : ℕ), s.restrictNonposSeq i (n + 1) ⊆ i
⊢ s.restrictNonposSeq i n ⊆ i

Tactic:
cases n
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
zero : s.someExistsOneDivLT (i \ ∅) ⊆ i
⊢ s.restrictNonposSeq i 0 ⊆ i

Tactic:
rw [restrictNonposSeq]

Premises used: _private.0.MeasureTheory.SignedMeasure.restrictNonposSeq
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
⊢ s.someExistsOneDivLT (i \ ∅) ⊆ i

Tactic:
someExistsOneDivLT_subset'

Premises used: _private.0.MeasureTheory.SignedMeasure.someExistsOneDivLT_subset'
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
⊢ s.someExistsOneDivLT (i \ ∅) ⊆ i

Tactic:
exact someExistsOneDivLT_subset'

Premises used: _private.0.MeasureTheory.SignedMeasure.someExistsOneDivLT_subset'
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
n : ℕ
succ :
  s.someExistsOneDivLT
      (i \
        ⋃ (k : ℕ),
          ⋃ (H : k ≤ n),
            have this := ⋯;
            s.restrictNonposSeq i k) ⊆
    i
⊢ s.restrictNonposSeq i (n + 1) ⊆ i

Tactic:
rw [restrictNonposSeq]

Premises used: _private.0.MeasureTheory.SignedMeasure.restrictNonposSeq
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
n : ℕ
⊢ s.someExistsOneDivLT
      (i \
        ⋃ (k : ℕ),
          ⋃ (H : k ≤ n),
            have this := ⋯;
            s.restrictNonposSeq i k) ⊆
    i

Tactic:
someExistsOneDivLT_subset'

Premises used: _private.0.MeasureTheory.SignedMeasure.someExistsOneDivLT_subset'
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
n : ℕ
⊢ s.someExistsOneDivLT
      (i \
        ⋃ (k : ℕ),
          ⋃ (H : k ≤ n),
            have this := ⋯;
            s.restrictNonposSeq i k) ⊆
    i

Tactic:
exact someExistsOneDivLT_subset'

Premises used: _private.0.MeasureTheory.SignedMeasure.someExistsOneDivLT_subset'
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
n : ℕ
hn : ¬s ≤[i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k] 0
rw :
  1 / HAdd.hAdd (α := ℝ) (↑(s.findExistsOneDivLT (i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k)) : ℝ) 1 <
    (↑s : Set α → ℝ) (s.someExistsOneDivLT (i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k))
⊢ 1 / HAdd.hAdd (α := ℝ) (↑(s.findExistsOneDivLT (i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k)) : ℝ) 1 <
    (↑s : Set α → ℝ) (s.restrictNonposSeq i n.succ)

Tactic:
rw [restrictNonposSeq_succ]

Premises used: _private.0.MeasureTheory.SignedMeasure.restrictNonposSeq_succ
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
n : ℕ
hn : ¬s ≤[i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k] 0
⊢ 1 / HAdd.hAdd (α := ℝ) (↑(s.findExistsOneDivLT (i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k)) : ℝ) 1 <
    (↑s : Set α → ℝ) (s.someExistsOneDivLT (i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k))

Tactic:
apply someExistsOneDivLT_lt hn

Premises used: _private.0.MeasureTheory.SignedMeasure.someExistsOneDivLT_lt
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₂ : ¬s ≤[i] 0
hn : ¬s ≤[i \ ⋃ (k : ℕ), ⋃ (_ : k < 0), s.restrictNonposSeq i k] 0
zero : 0 < (↑s : Set α → ℝ) (s.someExistsOneDivLT (i \ ∅))
⊢ 0 < (↑s : Set α → ℝ) (s.restrictNonposSeq i 0)

Tactic:
rw [restrictNonposSeq]

Premises used: _private.0.MeasureTheory.SignedMeasure.restrictNonposSeq
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₂ : ¬s ≤[i] 0
hn : ¬s ≤[i \ ⋃ (k : ℕ), ⋃ (_ : k < 0), s.restrictNonposSeq i k] 0
⊢ ¬s ≤[i \ ∅] 0

Tactic:
rw [← @Set.diff_empty _ i] at hi₂

Premises used: Set.diff_empty
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₂ : ¬s ≤[i] 0
hn : ¬s ≤[i \ ⋃ (k : ℕ), ⋃ (_ : k < 0), s.restrictNonposSeq i k] 0
hi₃ : ¬s ≤[i \ ∅] 0
⊢ ¬s ≤[i \ ⋃ (k : ℕ), ⋃ (_ : k < 0), s.restrictNonposSeq i k] 0

Tactic:
rw [← @Set.diff_empty _ i] at hi₂

Premises used: Set.diff_empty
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₂ : ¬s ≤[i \ ∅] 0
hn : ¬s ≤[i \ ⋃ (k : ℕ), ⋃ (_ : k < 0), s.restrictNonposSeq i k] 0
⊢ s.someExistsOneDivLT (i \ ∅) ⊆ i \ ∅

Tactic:
rcases someExistsOneDivLT_spec hi₂ with ⟨_, _, h⟩

Premises used: _private.0.MeasureTheory.SignedMeasure.someExistsOneDivLT_spec
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₂ : ¬s ≤[i \ ∅] 0
hn : ¬s ≤[i \ ⋃ (k : ℕ), ⋃ (_ : k < 0), s.restrictNonposSeq i k] 0
left : s.someExistsOneDivLT (i \ ∅) ⊆ i \ ∅
⊢ MeasurableSet (s.someExistsOneDivLT (i \ ∅))

Tactic:
rcases someExistsOneDivLT_spec hi₂ with ⟨_, _, h⟩

Premises used: _private.0.MeasureTheory.SignedMeasure.someExistsOneDivLT_spec
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₂ : ¬s ≤[i \ ∅] 0
hn : ¬s ≤[i \ ⋃ (k : ℕ), ⋃ (_ : k < 0), s.restrictNonposSeq i k] 0
left : s.someExistsOneDivLT (i \ ∅) ⊆ i \ ∅
left₁ : MeasurableSet (s.someExistsOneDivLT (i \ ∅))
⊢ 1 / HAdd.hAdd (α := ℝ) (↑(s.findExistsOneDivLT (i \ ∅)) : ℝ) 1 < (↑s : Set α → ℝ) (s.someExistsOneDivLT (i \ ∅))

Tactic:
rcases someExistsOneDivLT_spec hi₂ with ⟨_, _, h⟩

Premises used: _private.0.MeasureTheory.SignedMeasure.someExistsOneDivLT_spec