awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.BoundedVariation (hypothesis)
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 : Nonempty α
hlim : Tendsto f atBot (𝓝 (limUnder atBot f))
u : ℕ → α
u_anti : Antitone u
hu : Tendsto u atTop atBot
⊢ (↑hf.vectorMeasure : Set α → E) (Iic a) = Function.rightLim f a - limUnder atBot f
have A : Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc (u n) a)) atTop
  (𝓝 ((↑hf.vectorMeasure : Set α → E) (Iic a)))
Tactic: have A : Tendsto (fun n ↦ hf.vectorMeasure (Icc (u n) a)) atTop
      (𝓝 (hf.vectorMeasure (Iic a))) := by
    have : Iic a = ⋃ n, Icc (u n) a := by
      apply le_antisymm ?_ (by simp [Icc_subset_Iic_self])
      intro x (hx : x ≤ a)
      simpa [hx] using (hu.eventually (Iic_mem_atBot x)).exists
    rw [this]
    exact hf.vectorMeasure.tendsto_vectorMeasure_iUnion_atTop_nat (s := fun n ↦ Icc (u n) a)
      (fun i j hij x hx ↦ by grind [Antitone]) (fun i ↦ measurableSet_Icc)
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.BoundedVariation (hypothesis)
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 : Nonempty α
hlim : Tendsto f atBot (𝓝 (limUnder atBot f))
u : ℕ → α
u_anti : Antitone u
hu : Tendsto u atTop atBot
A :
  Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc (u n) a)) atTop
    (𝓝 ((↑hf.vectorMeasure : Set α → E) (Iic a)))
⊢ ∀ᶠ (n : ℕ) in atTop, u n ≤ a
have hu₁ : ∀ (b : α), ∃ (a : ℕ), ∀ b_1 ≥ a, u b_1 ≤ b
Tactic: simp only [tendsto_atBot, eventually_atTop] at hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.BoundedVariation (hypothesis)
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 : Nonempty α
hlim : Tendsto f atBot (𝓝 (limUnder atBot f))
u : ℕ → α
u_anti : Antitone u
hu : Tendsto u atTop atBot
A :
  Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc (u n) a)) atTop
    (𝓝 ((↑hf.vectorMeasure : Set α → E) (Iic a)))
⊢ EventuallyEq.{0, u_2} (β := E) atTop (fun (n : ℕ) ↦ Function.rightLim f a - Function.leftLim f (u n)) fun (n : ℕ) ↦
    (↑hf.vectorMeasure : Set α → E) (Icc (u n) a)
have this₁ : ∀ᶠ (n : ℕ) in atTop, u n ≤ a
Tactic: have : ∀ᶠ n in atTop, u n ≤ a := by
        simp only [tendsto_atBot, eventually_atTop] at hu
        simp [hu]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.BoundedVariation (goal)
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_1 : Nonempty α
hlim : Tendsto f atBot (𝓝 (limUnder atBot f))
u : ℕ → α
u_anti : Antitone u
hu : Tendsto u atTop atBot
A :
  Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc (u n) a)) atTop
    (𝓝 ((↑hf.vectorMeasure : Set α → E) (Iic a)))
this : ∀ᶠ (n : ℕ) in atTop, u n ≤ a
n : ℕ
hn : u n ≤ a
⊢ Function.rightLim f a - Function.leftLim f (u n) = (↑hf.vectorMeasure : Set α → E) (Icc (u n) a)
have rw : Function.rightLim f a - Function.leftLim f (u n) = Function.rightLim f a - Function.leftLim f (u n)
Tactic: rw [hf.vectorMeasure_Icc hn]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.BoundedVariation (goal)
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_1 : Nonempty α
hlim : Tendsto f atBot (𝓝 (limUnder atBot f))
u : ℕ → α
u_anti : Antitone u
hu : Tendsto u atTop atBot
A :
  Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc (u n) a)) atTop
    (𝓝 ((↑hf.vectorMeasure : Set α → E) (Iic a)))
this : ∀ᶠ (n : ℕ) in atTop, u n ≤ a
⊢ EventuallyEq.{0, u_2} (β := E) atTop (fun (n : ℕ) ↦ Function.rightLim f a - Function.leftLim f (u n)) fun (n : ℕ) ↦
    (↑hf.vectorMeasure : Set α → E) (Icc (u n) a)
have h : ∀ (a_1 : ℕ),
  Membership.mem (γ := Set ℕ)
    {x : ℕ |
      Membership.mem (γ := Set ℕ) {x : ℕ | (fun (n : ℕ) ↦ u n ≤ a) x} x →
        Membership.mem (γ := Set ℕ)
          {x : ℕ |
            (fun (x : ℕ) ↦
                Eq.{u_2 + 1} (α := E) ((fun (n : ℕ) ↦ Function.rightLim f a - Function.leftLim f (u n)) x)
                  ((fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc (u n) a)) x))
              x}
          x}
    a_1
Tactic: filter_upwards [this] with n hn using by rw [hf.vectorMeasure_Icc hn]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.BoundedVariation (goal)
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_1 : Nonempty α
hlim : Tendsto f atBot (𝓝 (limUnder atBot f))
u : ℕ → α
u_anti : Antitone u
hu : Tendsto u atTop atBot
A :
  Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc (u n) a)) atTop
    (𝓝 ((↑hf.vectorMeasure : Set α → E) (Iic a)))
this : ∀ᶠ (n : ℕ) in atTop, u n ≤ a
h :
  ∀ (a_1 : ℕ),
    Membership.mem (γ := Set ℕ)
      {x : ℕ |
        Membership.mem (γ := Set ℕ) {x : ℕ | (fun (n : ℕ) ↦ u n ≤ a) x} x →
          Membership.mem (γ := Set ℕ)
            {x : ℕ |
              (fun (x : ℕ) ↦
                  Eq.{u_2 + 1} (α := E) ((fun (n : ℕ) ↦ Function.rightLim f a - Function.leftLim f (u n)) x)
                    ((fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc (u n) a)) x))
                x}
            x}
      a_1
⊢ EventuallyEq.{0, u_2} (β := E) atTop (fun (n : ℕ) ↦ Function.rightLim f a - Function.leftLim f (u n)) fun (n : ℕ) ↦
    (↑hf.vectorMeasure : Set α → E) (Icc (u n) a)
have h₁ : ∀ (a_1 : ℕ),
  u a_1 ≤ a → Function.rightLim f a - Function.leftLim f (u a_1) = (↑hf.vectorMeasure : Set α → E) (Icc (u a_1) a)
Tactic: filter_upwards [this] with n hn using by rw [hf.vectorMeasure_Icc hn]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.BoundedVariation (hypothesis)
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 : Nonempty α
hlim : Tendsto f atBot (𝓝 (limUnder atBot f))
u : ℕ → α
u_anti : Antitone u
hu : Tendsto u atTop atBot
A :
  Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc (u n) a)) atTop
    (𝓝 ((↑hf.vectorMeasure : Set α → E) (Iic a)))
⊢ Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc (u n) a)) atTop
    (𝓝 (Function.rightLim f a - limUnder atBot f))
have this₁ : EventuallyEq.{0, u_2} (β := E) atTop (fun (n : ℕ) ↦ Function.rightLim f a - Function.leftLim f (u n)) fun (n : ℕ) ↦
  (↑hf.vectorMeasure : Set α → E) (Icc (u n) a)
Tactic: have : (fun n ↦ f.rightLim a - f.leftLim (u n)) =ᶠ[atTop]
        (fun n ↦ hf.vectorMeasure (Icc (u n) a)) := by
      have : ∀ᶠ n in atTop, u n ≤ a := by
        simp only [tendsto_atBot, eventually_atTop] at hu
        simp [hu]
      filter_upwards [this] with n hn using by rw [hf.vectorMeasure_Icc hn]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.BoundedVariation (goal)
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_1 : Nonempty α
hlim : Tendsto f atBot (𝓝 (limUnder atBot f))
u : ℕ → α
u_anti : Antitone u
hu : Tendsto u atTop atBot
A :
  Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc (u n) a)) atTop
    (𝓝 ((↑hf.vectorMeasure : Set α → E) (Iic a)))
this :
  EventuallyEq.{0, u_2} (β := E) atTop (fun (n : ℕ) ↦ Function.rightLim f a - Function.leftLim f (u n)) fun (n : ℕ) ↦
    (↑hf.vectorMeasure : Set α → E) (Icc (u n) a)
⊢ Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc (u n) a)) atTop
    (𝓝 (Function.rightLim f a - limUnder atBot f))
have apply : Tendsto (fun (n : ℕ) ↦ Function.rightLim f a - Function.leftLim f (u n)) atTop
  (𝓝 (Function.rightLim f a - limUnder atBot f))
Tactic: apply Tendsto.congr' this
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.BoundedVariation (goal)
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_1 : Nonempty α
hlim : Tendsto f atBot (𝓝 (limUnder atBot f))
u : ℕ → α
u_anti : Antitone u
hu : Tendsto u atTop atBot
A :
  Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc (u n) a)) atTop
    (𝓝 ((↑hf.vectorMeasure : Set α → E) (Iic a)))
this :
  EventuallyEq.{0, u_2} (β := E) atTop (fun (n : ℕ) ↦ Function.rightLim f a - Function.leftLim f (u n)) fun (n : ℕ) ↦
    (↑hf.vectorMeasure : Set α → E) (Icc (u n) a)
⊢ Tendsto (fun (n : ℕ) ↦ Function.rightLim f a - Function.leftLim f (u n)) atTop
    (𝓝 (Function.rightLim f a - limUnder atBot f))
have apply : Tendsto (fun (x : ℕ) ↦ Function.leftLim f (u x)) atTop (𝓝 (limUnder atBot f))
Tactic: apply Tendsto.sub tendsto_const_nhds
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.BoundedVariation (hypothesis)
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 : Nonempty α
hlim : Tendsto f atBot (𝓝 (limUnder atBot f))
u : ℕ → α
u_anti : Antitone u
hu : Tendsto u atTop atBot
A :
  Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc (u n) a)) atTop
    (𝓝 ((↑hf.vectorMeasure : Set α → E) (Iic a)))
⊢ (↑hf.vectorMeasure : Set α → E) (Iic a) = Function.rightLim f a - limUnder atBot f
have B : Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc (u n) a)) atTop
  (𝓝 (Function.rightLim f a - limUnder atBot f))
Tactic: have B : Tendsto (fun n ↦ hf.vectorMeasure (Icc (u n) a)) atTop
      (𝓝 (f.rightLim a - limUnder atBot f)) := by
    have : (fun n ↦ f.rightLim a - f.leftLim (u n)) =ᶠ[atTop]
        (fun n ↦ hf.vectorMeasure (Icc (u n) a)) := by
      have : ∀ᶠ n in atTop, u n ≤ a := by
        simp only [tendsto_atBot, eventually_atTop] at hu
        simp [hu]
      filter_upwards [this] with n hn using by rw [hf.vectorMeasure_Icc hn]
    apply Tendsto.congr' this
    apply Tendsto.sub tendsto_const_nhds
    exact (tendsto_leftLim_atBot_of_tendsto hf.tendsto_atBot_limUnder).comp hu
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.BoundedVariation (hypothesis)
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) (Iio a) = Function.leftLim f a - limUnder atBot f
have this : (↑hf.vectorMeasure : Set α → E) (Iic a) = Function.rightLim f a - limUnder atBot f
Tactic: have := hf.vectorMeasure_Iic a
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.BoundedVariation (hypothesis)
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.leftLim f a - limUnder atBot f
have this₁ : (↑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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.BoundedVariation (goal)
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
⊢ (↑hf.vectorMeasure : Set α → E) univ = limUnder atTop f - limUnder atBot f
have inl : ∀ (hα_1 : IsEmpty α), (↑hf.vectorMeasure : Set α → E) univ = limUnder atTop f - limUnder atBot f
Tactic: rcases isEmpty_or_nonempty α with hα | hα
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.BoundedVariation (goal)
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
⊢ (↑hf.vectorMeasure : Set α → E) univ = limUnder atTop f - limUnder atBot f
have inr : ∀ (hα_1 : Nonempty α), (↑hf.vectorMeasure : Set α → E) univ = limUnder atTop f - limUnder atBot f
Tactic: rcases isEmpty_or_nonempty α with hα | hα
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.BoundedVariation (goal)
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 α
⊢ (↑hf.vectorMeasure : Set α → E) univ = limUnder atTop f - limUnder atBot f
have inr : Function.leftLim f hα.some - limUnder atBot f + (limUnder atTop f - Function.leftLim f hα.some) =
  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]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬s ≤[i] 0
⊢ s.ExistsOneDivLT i (s.findExistsOneDivLT i)
have rw : s.ExistsOneDivLT i (Nat.find (p := s.ExistsOneDivLT i) sorry)
Tactic: rw [findExistsOneDivLT, dif_pos hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬s ≤[i] 0
m : ℕ
hm : m < s.findExistsOneDivLT i
⊢ ¬s.ExistsOneDivLT i m
have hm₁ : m < Nat.find (p := s.ExistsOneDivLT i) sorry
Tactic: rw [findExistsOneDivLT, dif_pos hi] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬s ≤[i] 0
m : ℕ
hm : m < s.findExistsOneDivLT i
⊢ ¬s.ExistsOneDivLT i m
have rw : ∀ (hm : m < if hi : ¬s ≤[i] 0 then Nat.find (p := s.ExistsOneDivLT i) sorry else 0), ¬s.ExistsOneDivLT i m
Tactic: classical
  rw [findExistsOneDivLT, dif_pos hi] at hm
  exact Nat.find_min _ hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
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
⊢ ¬s.ExistsOneDivLT i m
have rw₁ : ∀ (hm : m < Nat.find (p := s.ExistsOneDivLT i) sorry), ¬s.ExistsOneDivLT i m
Tactic: classical
  rw [findExistsOneDivLT, dif_pos hi] at hm
  exact Nat.find_min _ hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬s ≤[i] 0
⊢ s.someExistsOneDivLT i ⊆ i ∧
    MeasurableSet (s.someExistsOneDivLT i) ∧
      1 / HAdd.hAdd (α := ℝ) (↑(s.findExistsOneDivLT i) : ℝ) 1 < (↑s : Set α → ℝ) (s.someExistsOneDivLT i)
have rw : Classical.choose (p := fun (x : Set α) ↦
      x ⊆ i ∧ MeasurableSet x ∧ 1 / HAdd.hAdd (α := ℝ) (↑(s.findExistsOneDivLT i) : ℝ) 1 < (↑s : Set α → ℝ) x) sorry ⊆
    i ∧
  MeasurableSet
      (Classical.choose (p := fun (x : Set α) ↦
        x ⊆ i ∧ MeasurableSet x ∧ 1 / HAdd.hAdd (α := ℝ) (↑(s.findExistsOneDivLT i) : ℝ) 1 < (↑s : Set α → ℝ) x) sorry) ∧
    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) sorry)
Tactic: rw [someExistsOneDivLT, dif_pos hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
⊢ s.someExistsOneDivLT i ⊆ i
have pos : ∀ (hi : ¬s ≤[i] 0), s.someExistsOneDivLT i ⊆ i
Tactic: by_cases hi : ¬s ≤[i] 0
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
pos : ∀ (hi : ¬s ≤[i] 0), s.someExistsOneDivLT i ⊆ i
⊢ s.someExistsOneDivLT i ⊆ i
have neg : ∀ (hi : ¬¬s ≤[i] 0), s.someExistsOneDivLT i ⊆ i
Tactic: by_cases hi : ¬s ≤[i] 0
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬¬s ≤[i] 0
⊢ s.someExistsOneDivLT i ⊆ i
have neg : ∅ ⊆ i
Tactic: rw [someExistsOneDivLT, dif_neg hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
⊢ MeasurableSet (s.someExistsOneDivLT i)
have pos : ∀ (hi : ¬s ≤[i] 0), MeasurableSet (s.someExistsOneDivLT i)
Tactic: by_cases hi : ¬s ≤[i] 0
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
pos : ∀ (hi : ¬s ≤[i] 0), MeasurableSet (s.someExistsOneDivLT i)
⊢ MeasurableSet (s.someExistsOneDivLT i)
have neg : ∀ (hi : ¬¬s ≤[i] 0), MeasurableSet (s.someExistsOneDivLT i)
Tactic: by_cases hi : ¬s ≤[i] 0
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬¬s ≤[i] 0
⊢ MeasurableSet (s.someExistsOneDivLT i)
have neg : MeasurableSet.{u_1} (α := α) ∅
Tactic: rw [someExistsOneDivLT, dif_neg hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
n : ℕ
⊢ s.restrictNonposSeq i n.succ = s.someExistsOneDivLT (i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k)
have rw : s.someExistsOneDivLT
    (i \
      ⋃ (k : ℕ),
        ⋃ (H : k ≤ n),
          have this := sorry;
          s.restrictNonposSeq i k) =
  s.someExistsOneDivLT (i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k)
Tactic: rw [restrictNonposSeq]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
n : ℕ
⊢ s.restrictNonposSeq i n ⊆ i
have zero : s.restrictNonposSeq i 0 ⊆ i
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
n : ℕ
zero : s.restrictNonposSeq i 0 ⊆ i
⊢ s.restrictNonposSeq i n ⊆ i
have succ : ∀ (n : ℕ), s.restrictNonposSeq i (n + 1) ⊆ i
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
⊢ s.restrictNonposSeq i 0 ⊆ i
have zero : s.someExistsOneDivLT (i \ ∅) ⊆ i
Tactic: rw [restrictNonposSeq]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
n : ℕ
⊢ s.restrictNonposSeq i (n + 1) ⊆ i
have succ : s.someExistsOneDivLT
    (i \
      ⋃ (k : ℕ),
        ⋃ (H : k ≤ n),
          have this := sorry;
          s.restrictNonposSeq i k) ⊆
  i
Tactic: rw [restrictNonposSeq]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
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.restrictNonposSeq i n.succ)
have 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))
Tactic: rw [restrictNonposSeq_succ]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
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
⊢ 0 < (↑s : Set α → ℝ) (s.restrictNonposSeq i 0)
have zero : 0 < (↑s : Set α → ℝ) (s.someExistsOneDivLT (i \ ∅))
Tactic: rw [restrictNonposSeq]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (hypothesis)
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
⊢ 0 < (↑s : Set α → ℝ) (s.someExistsOneDivLT (i \ ∅))
have hi₃ : ¬s ≤[i \ ∅] 0
Tactic: rw [← @Set.diff_empty _ i] at hi₂
Cleared hypotheses: hi₂, hn
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (hypothesis)
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
⊢ 0 < (↑s : Set α → ℝ) (s.someExistsOneDivLT (i \ ∅))
have left : s.someExistsOneDivLT (i \ ∅) ⊆ i \ ∅
Tactic: rcases someExistsOneDivLT_spec hi₂ with ⟨_, _, h⟩