awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
ι : Type u_2
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : SecondCountableTopology Ω
inst_3 : OpensMeasurableSpace Ω
S : Set (Set Ω)
hS : IsPiSystem S
μ : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
l : Filter ι
inst_4 : l.IsCountablyGenerated
hmeas : ∀ s ∈ S, MeasurableSet s
h : ∀ (u : Set Ω), IsOpen[inst_1] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
h' :
  ∀ s ∈ S,
    Tendsto (β := ℝ≥0) (fun (i : ι) ↦ ((μ i : (a : Set Ω) → ℝ≥0) s : ℝ≥0)) l
      (𝓝 ((ν : (a : Set Ω) → ℝ≥0) s) : Filter ℝ≥0)
hl : l.NeBot
⊢ Tendsto μ l (𝓝 ν)
have inr : ∀ (G : Set Ω),
  IsOpen[inst_1] G →
    LE.le (α := ℝ≥0) ((ν : (a : Set Ω) → ℝ≥0) G : ℝ≥0) (liminf (fun (i : ι) ↦ (μ i : (a : Set Ω) → ℝ≥0) G) l : ℝ≥0)
Tactic: apply tendsto_of_forall_isOpen_le_liminf
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
ι : Type u_2
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : SecondCountableTopology Ω
inst_3 : OpensMeasurableSpace Ω
S : Set (Set Ω)
hS : IsPiSystem S
μ : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
l : Filter ι
inst_4 : l.IsCountablyGenerated
hmeas : ∀ s ∈ S, MeasurableSet s
h : ∀ (u : Set Ω), IsOpen[inst_1] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
h' :
  ∀ s ∈ S,
    Tendsto (β := ℝ≥0) (fun (i : ι) ↦ ((μ i : (a : Set Ω) → ℝ≥0) s : ℝ≥0)) l
      (𝓝 ((ν : (a : Set Ω) → ℝ≥0) s) : Filter ℝ≥0)
hl : l.NeBot
G : Set Ω
hG : IsOpen[inst_1] G
⊢ LE.le (α := ℝ≥0) ((ν : (a : Set Ω) → ℝ≥0) G : ℝ≥0) (liminf (fun (i : ι) ↦ (μ i : (a : Set Ω) → ℝ≥0) G) l : ℝ≥0)
have inr : ∀ (r : ℝ≥0) (hr : r < (ν : (a : Set Ω) → ℝ≥0) G), ∀ᶠ (a : ι) in l, r < (μ a : (a : Set Ω) → ℝ≥0) G
Tactic: refine (le_liminf_iff (isCoboundedUnder_ge_of_le (x := 1) l (by simp)) (by isBoundedDefault)).2
    (fun r hr ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
ι : Type u_2
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : SecondCountableTopology Ω
inst_3 : OpensMeasurableSpace Ω
S : Set (Set Ω)
hS : IsPiSystem S
μ : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
l : Filter ι
inst_4 : l.IsCountablyGenerated
hmeas : ∀ s ∈ S, MeasurableSet s
h : ∀ (u : Set Ω), IsOpen[inst_1] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
h' :
  ∀ s ∈ S,
    Tendsto (β := ℝ≥0) (fun (i : ι) ↦ ((μ i : (a : Set Ω) → ℝ≥0) s : ℝ≥0)) l
      (𝓝 ((ν : (a : Set Ω) → ℝ≥0) s) : Filter ℝ≥0)
hl : l.NeBot
G : Set Ω
hG : IsOpen[inst_1] G
r : ℝ≥0
hr : r < (ν : (a : Set Ω) → ℝ≥0) G
⊢ ∀ᶠ (a : ι) in l, r < (μ a : (a : Set Ω) → ℝ≥0) G
have inr : ∀ (T : Finset (Set Ω)) (TS : ∀ t ∈ T, t ∈ S) (T_meas : r < (ν : (a : Set Ω) → ℝ≥0) (⋃ t ∈ T, t)) (TG : ⋃ t ∈ T, t ⊆ G),
  ∀ᶠ (a : ι) in l, r < (μ a : (a : Set Ω) → ℝ≥0) G
Tactic: obtain ⟨T, TS, T_meas, TG⟩ :
      ∃ T : Finset (Set Ω), (∀ t ∈ T, t ∈ S) ∧ (r < ν (⋃ t ∈ T, t)) ∧ (⋃ t ∈ T, t) ⊆ G :=
    ν.exists_lt_measure_biUnion_of_isOpen h hG hr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_2
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : SecondCountableTopology Ω
inst_3 : OpensMeasurableSpace Ω
S : Set (Set Ω)
hS : IsPiSystem S
μ : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
l : Filter ι
inst_4 : l.IsCountablyGenerated
hmeas : ∀ s ∈ S, MeasurableSet s
h : ∀ (u : Set Ω), IsOpen[inst_1] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
h' :
  ∀ s ∈ S,
    Tendsto (β := ℝ≥0) (fun (i : ι) ↦ ((μ i : (a : Set Ω) → ℝ≥0) s : ℝ≥0)) l
      (𝓝 ((ν : (a : Set Ω) → ℝ≥0) s) : Filter ℝ≥0)
hl : l.NeBot
G : Set Ω
hG : IsOpen[inst_1] G
r : ℝ≥0
hr : r < (ν : (a : Set Ω) → ℝ≥0) G
T : Finset (Set Ω)
TS : ∀ t ∈ T, t ∈ S
T_meas : r < (ν : (a : Set Ω) → ℝ≥0) (⋃ t ∈ T, t)
TG : ⋃ t ∈ T, t ⊆ G
⊢ ∀ᶠ (a : ι) in l, r < (μ a : (a : Set Ω) → ℝ≥0) G
have this : Tendsto (β := ℝ≥0) (fun (i : ι) ↦ ((μ i : (a : Set Ω) → ℝ≥0) (⋃ t ∈ T, t) : ℝ≥0)) l
  (𝓝 ((ν : (a : Set Ω) → ℝ≥0) (⋃ t ∈ T, t)) : Filter ℝ≥0)
Tactic: have : Tendsto (fun i ↦ μ i (⋃ t ∈ T, t)) l (𝓝 (ν (⋃ t ∈ T, t))) :=
    hS.tendsto_probabilityMeasure_biUnion TS hmeas h'
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
ι : Type u_2
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : SecondCountableTopology Ω
inst_3 : OpensMeasurableSpace Ω
S : Set (Set Ω)
hS : IsPiSystem S
μ : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
l : Filter ι
inst_4 : l.IsCountablyGenerated
hmeas : ∀ s ∈ S, MeasurableSet s
h : ∀ (u : Set Ω), IsOpen[inst_1] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
h' :
  ∀ s ∈ S,
    Tendsto (β := ℝ≥0) (fun (i : ι) ↦ ((μ i : (a : Set Ω) → ℝ≥0) s : ℝ≥0)) l
      (𝓝 ((ν : (a : Set Ω) → ℝ≥0) s) : Filter ℝ≥0)
hl : l.NeBot
G : Set Ω
hG : IsOpen[inst_1] G
r : ℝ≥0
hr : r < (ν : (a : Set Ω) → ℝ≥0) G
T : Finset (Set Ω)
TS : ∀ t ∈ T, t ∈ S
T_meas : r < (ν : (a : Set Ω) → ℝ≥0) (⋃ t ∈ T, t)
TG : ⋃ t ∈ T, t ⊆ G
this :
  Tendsto (β := ℝ≥0) (fun (i : ι) ↦ ((μ i : (a : Set Ω) → ℝ≥0) (⋃ t ∈ T, t) : ℝ≥0)) l
    (𝓝 ((ν : (a : Set Ω) → ℝ≥0) (⋃ t ∈ T, t)) : Filter ℝ≥0)
⊢ ∀ᶠ (a : ι) in l, r < (μ a : (a : Set Ω) → ℝ≥0) G
have h₁ : ∀ (i : ι) (hi : r < (μ i : (a : Set Ω) → ℝ≥0) (⋃ t ∈ T, t)), r < (μ i : (a : Set Ω) → ℝ≥0) G
Tactic: filter_upwards [(tendsto_order.1 this).1 r T_meas] with i hi
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.PreVariation (goal)
Goal:
X : Type u_1
inst : MeasurableSpace X
⊢ Eq.{u_1 + 1} (α := (s : Set X) → ℝ≥0∞) (preVariationFun 0) 0
have h : ∀ (x : Set X), preVariationFun 0 x = 0 x
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.PreVariation (goal)
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s : Set X
hs : MeasurableSet s
P : Finpartition s
hP : ∀ p ∈ P.parts (a := s), MeasurableSet p
⊢ ∑ p ∈ P.parts (a := s), f p ≤ preVariationFun f s
have simp : LE.le (α := ℝ≥0∞) (∑ p ∈ P.parts (a := s), f p)
  (⨆ (P : Finpartition (Subtype.mk (p := MeasurableSet) s sorry)), ∑ p ∈ P.parts, f (↑p : Set X))
Tactic: simp only [preVariationFun, hs, ↓reduceDIte]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.PreVariation (goal)
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s₁ s₂ : Set X
hs₁ : MeasurableSet s₁
hs₂ : MeasurableSet s₂
h : s₁ ⊆ s₂
P : Finpartition (Subtype.mk (p := MeasurableSet) s₁ hs₁)
⊢ ∑ p ∈ P.parts, f (↑p : Set X) ≤ preVariationFun f s₂
have pos : ∀ (heq : s₁ = s₂), ∑ p ∈ P.parts, f (↑p : Set X) ≤ preVariationFun f s₂
Tactic: by_cases heq : s₁ = s₂
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.PreVariation (goal)
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s₁ s₂ : Set X
hs₁ : MeasurableSet s₁
hs₂ : MeasurableSet s₂
h : s₁ ⊆ s₂
P : Finpartition (Subtype.mk (p := MeasurableSet) s₁ hs₁)
pos : ∀ (heq : s₁ = s₂), ∑ p ∈ P.parts, f (↑p : Set X) ≤ preVariationFun f s₂
⊢ ∑ p ∈ P.parts, f (↑p : Set X) ≤ preVariationFun f s₂
have neg : ∀ (heq : ¬s₁ = s₂), ∑ p ∈ P.parts, f (↑p : Set X) ≤ preVariationFun f s₂
Tactic: by_cases heq : s₁ = s₂
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.PreVariation (goal)
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s₁ s₂ : Set X
hs₁ : MeasurableSet s₁
hs₂ : MeasurableSet s₂
h : s₁ ⊆ s₂
P : Finpartition (Subtype.mk (p := MeasurableSet) s₁ hs₁)
heq : s₁ = s₂
⊢ ∑ p ∈ P.parts, f (↑p : Set X) ≤ preVariationFun f s₂
have pos : ∑ p ∈ P.parts, f (↑p : Set X) ≤ preVariationFun f s₁
Tactic: rw [← heq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.PreVariation (hypothesis)
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s₁ s₂ : Set X
hs₁ : MeasurableSet s₁
hs₂ : MeasurableSet s₂
h : s₁ ⊆ s₂
P : Finpartition (Subtype.mk (p := MeasurableSet) s₁ hs₁)
heq : ¬s₁ = s₂
b : Subtype (α := Set X) MeasurableSet := Subtype.mk (p := MeasurableSet) (s₂ \ s₁) ⋯
⊢ ∑ p ∈ P.parts, f (↑p : Set X) ≤ preVariationFun f s₂
have hb : b ≠ ⊥
Tactic: have hb : b ≠ ⊥ := fun hc => heq (h.antisymm (Set.diff_eq_empty.mp (congrArg (·.1) hc)))
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.PreVariation (goal)
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s₁ s₂ : Set X
hs₁ : MeasurableSet s₁
hs₂ : MeasurableSet s₂
h : s₁ ⊆ s₂
P : Finpartition (Subtype.mk (p := MeasurableSet) s₁ hs₁)
heq : ¬s₁ = s₂
b : Subtype (α := Set X) MeasurableSet := Subtype.mk (p := MeasurableSet) (s₂ \ s₁) ⋯
hb : b ≠ ⊥
⊢ Disjoint (Subtype.mk (p := MeasurableSet) s₁ hs₁) b
have simp : (↑(Subtype.mk (p := MeasurableSet) s₁ hs₁ ⊓ Subtype.mk (p := MeasurableSet) (s₂ \ s₁) sorry) : Set X) = (↑⊥ : Set X)
Tactic: simp only [b, disjoint_iff, Subtype.ext_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.PreVariation (hypothesis)
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s₁ s₂ : Set X
hs₁ : MeasurableSet s₁
hs₂ : MeasurableSet s₂
h : s₁ ⊆ s₂
P : Finpartition (Subtype.mk (p := MeasurableSet) s₁ hs₁)
heq : ¬s₁ = s₂
b : Subtype (α := Set X) MeasurableSet := Subtype.mk (p := MeasurableSet) (s₂ \ s₁) ⋯
hb : b ≠ ⊥
⊢ ∑ p ∈ P.parts, f (↑p : Set X) ≤ preVariationFun f s₂
have hab : Disjoint (Subtype.mk (p := MeasurableSet) s₁ hs₁) b
Tactic: have hab : Disjoint (⟨s₁, hs₁⟩ : Subtype MeasurableSet) b := by
      simp only [b, disjoint_iff, Subtype.ext_iff]
      exact Set.inter_diff_self s₁ s₂
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.PreVariation (hypothesis)
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s₁ s₂ : Set X
hs₁ : MeasurableSet s₁
hs₂ : MeasurableSet s₂
h : s₁ ⊆ s₂
P : Finpartition (Subtype.mk (p := MeasurableSet) s₁ hs₁)
heq : ¬s₁ = s₂
b : Subtype (α := Set X) MeasurableSet := Subtype.mk (p := MeasurableSet) (s₂ \ s₁) ⋯
hb : b ≠ ⊥
hab : Disjoint (Subtype.mk (p := MeasurableSet) s₁ hs₁) b
⊢ ∑ p ∈ P.parts, f (↑p : Set X) ≤ preVariationFun f s₂
have hc : Subtype.mk (p := MeasurableSet) s₁ hs₁ ⊔ b = Subtype.mk (p := MeasurableSet) s₂ hs₂
Tactic: have hc : (⟨s₁, hs₁⟩ : Subtype MeasurableSet) ⊔ b = ⟨s₂, hs₂⟩ :=
      Subtype.ext (Set.union_diff_cancel h)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.PreVariation (goal)
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s₁ s₂ : Set X
hs₂ : MeasurableSet s₂
h : s₁ ⊆ s₂
⊢ preVariationFun f s₁ ≤ preVariationFun f s₂
have pos : ∀ (hs₁ : MeasurableSet s₁), preVariationFun f s₁ ≤ preVariationFun f s₂
Tactic: by_cases hs₁ : MeasurableSet s₁
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.PreVariation (goal)
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s₁ s₂ : Set X
hs₂ : MeasurableSet s₂
h : s₁ ⊆ s₂
pos : ∀ (hs₁ : MeasurableSet s₁), preVariationFun f s₁ ≤ preVariationFun f s₂
⊢ preVariationFun f s₁ ≤ preVariationFun f s₂
have neg : ∀ (hs₁ : ¬MeasurableSet s₁), preVariationFun f s₁ ≤ preVariationFun f s₂
Tactic: by_cases hs₁ : MeasurableSet s₁
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.PreVariation (hypothesis)
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s₁ s₂ : Set X
hs₂ : MeasurableSet s₂
h : s₁ ⊆ s₂
hs₁ : MeasurableSet s₁
⊢ preVariationFun f s₁ ≤ preVariationFun f s₂
have this : ∀ (P : Finpartition (Subtype.mk (p := MeasurableSet) s₁ hs₁)), ∑ p ∈ P.parts, f (↑p : Set X) ≤ preVariationFun f s₂
Tactic: have := sum_le_preVariationFun_of_subset f hs₁ hs₂ h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.PreVariation (hypothesis)
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s : Set X
hs : MeasurableSet s
ε : ℝ≥0
hε : 0 < ε
h : preVariationFun f s ≠ ∞
ε' : ℝ≥0 := min ε (preVariationFun f s).toNNReal
⊢ ∃ (P : Finpartition (Subtype.mk (p := MeasurableSet) s hs)),
    preVariationFun f s ≤ ∑ p ∈ P.parts, f (↑p : Set X) + (↑ε : ℝ≥0∞)
have hε' : (↑ε' : ℝ≥0∞) ≤ preVariationFun f s
Tactic: have hε' : ε' ≤ preVariationFun f s := by simp_all [ε']
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.PreVariation (hypothesis)
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s : Set X
hs : MeasurableSet s
ε : ℝ≥0
hε : 0 < ε
h : preVariationFun f s ≠ ∞
ε' : ℝ≥0 := min ε (preVariationFun f s).toNNReal
hε' : (↑ε' : ℝ≥0∞) ≤ preVariationFun f s
⊢ ∃ (P : Finpartition (Subtype.mk (p := MeasurableSet) s hs)),
    preVariationFun f s ≤ ∑ p ∈ P.parts, f (↑p : Set X) + (↑ε : ℝ≥0∞)
have this : ε' ≤ ε
Tactic: have : ε' ≤ ε := by simp_all [ε']
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.PreVariation (goal)
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s : Set X
hs : MeasurableSet s
ε : ℝ≥0
hε : 0 < ε
h : preVariationFun f s ≠ ∞
ε' : ℝ≥0 := min ε (preVariationFun f s).toNNReal
hε' : (↑ε' : ℝ≥0∞) ≤ preVariationFun f s
this : ε' ≤ ε
⊢ ∃ (P : Finpartition (Subtype.mk (p := MeasurableSet) s hs)),
    preVariationFun f s ≤ ∑ p ∈ P.parts, f (↑p : Set X) + (↑ε : ℝ≥0∞)
have inl : ∀ (hw : preVariationFun f s ≠ 0),
  ∃ (P : Finpartition (Subtype.mk (p := MeasurableSet) s hs)),
    preVariationFun f s ≤ ∑ p ∈ P.parts, f (↑p : Set X) + (↑ε : ℝ≥0∞)
Tactic: obtain hw | hw : preVariationFun f s ≠ 0 ∨ preVariationFun f s = 0 := ne_or_eq _ _
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.PreVariation (goal)
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s : Set X
hs : MeasurableSet s
ε : ℝ≥0
hε : 0 < ε
h : preVariationFun f s ≠ ∞
ε' : ℝ≥0 := min ε (preVariationFun f s).toNNReal
hε' : (↑ε' : ℝ≥0∞) ≤ preVariationFun f s
this : ε' ≤ ε
inl :
  ∀ (hw : preVariationFun f s ≠ 0),
    ∃ (P : Finpartition (Subtype.mk (p := MeasurableSet) s hs)),
      preVariationFun f s ≤ ∑ p ∈ P.parts, f (↑p : Set X) + (↑ε : ℝ≥0∞)
⊢ ∃ (P : Finpartition (Subtype.mk (p := MeasurableSet) s hs)),
    preVariationFun f s ≤ ∑ p ∈ P.parts, f (↑p : Set X) + (↑ε : ℝ≥0∞)
have inr : ∀ (hw : preVariationFun f s = 0),
  ∃ (P : Finpartition (Subtype.mk (p := MeasurableSet) s hs)),
    preVariationFun f s ≤ ∑ p ∈ P.parts, f (↑p : Set X) + (↑ε : ℝ≥0∞)
Tactic: obtain hw | hw : preVariationFun f s ≠ 0 ∨ preVariationFun f s = 0 := ne_or_eq _ _
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.PreVariation (goal)
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s : Set X
hs : MeasurableSet s
ε : ℝ≥0
hε : 0 < ε
h : preVariationFun f s ≠ ∞
ε' : ℝ≥0 := min ε (preVariationFun f s).toNNReal
hε' : (↑ε' : ℝ≥0∞) ≤ preVariationFun f s
this : ε' ≤ ε
hw : preVariationFun f s ≠ 0
⊢ 0 < ε'
have simp : 0 < ε ∧ 0 < (preVariationFun f s).toNNReal
Tactic: simp only [lt_inf_iff, ε']
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.PreVariation (hypothesis)
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s : Set X
hs : MeasurableSet s
ε : ℝ≥0
hε : 0 < ε
h : preVariationFun f s ≠ ∞
ε' : ℝ≥0 := min ε (preVariationFun f s).toNNReal
hε' : (↑ε' : ℝ≥0∞) ≤ preVariationFun f s
this : ε' ≤ ε
hw : preVariationFun f s ≠ 0
⊢ ∃ (P : Finpartition (Subtype.mk (p := MeasurableSet) s hs)),
    preVariationFun f s ≤ ∑ p ∈ P.parts, f (↑p : Set X) + (↑ε : ℝ≥0∞)
have this₁ : 0 < ε'
Tactic: have : 0 < ε' := by
      simp only [lt_inf_iff, ε']
      exact ⟨hε, toNNReal_pos hw h⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.PreVariation (hypothesis)
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s : Set X
hs : MeasurableSet s
ε : ℝ≥0
hε : 0 < ε
h : preVariationFun f s ≠ ∞
ε' : ℝ≥0 := min ε (preVariationFun f s).toNNReal
hε' : (↑ε' : ℝ≥0∞) ≤ preVariationFun f s
this_1 : ε' ≤ ε
hw : preVariationFun f s ≠ 0
this : 0 < ε'
a : ℝ≥0∞ := preVariationFun f s - (↑ε' : ℝ≥0∞)
⊢ ∃ (P : Finpartition (Subtype.mk (p := MeasurableSet) s hs)),
    preVariationFun f s ≤ ∑ p ∈ P.parts, f (↑p : Set X) + (↑ε : ℝ≥0∞)
have ha : a < preVariationFun f s
Tactic: have ha : a < preVariationFun f s := ENNReal.sub_lt_self h hw (by positivity)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.PreVariation (goal)
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s : Set X
hs : MeasurableSet s
ε : ℝ≥0
hε : 0 < ε
h : preVariationFun f s ≠ ∞
ε' : ℝ≥0 := min ε (preVariationFun f s).toNNReal
hε' : (↑ε' : ℝ≥0∞) ≤ preVariationFun f s
this_1 : ε' ≤ ε
hw : preVariationFun f s ≠ 0
this : 0 < ε'
a : ℝ≥0∞ := preVariationFun f s - (↑ε' : ℝ≥0∞)
ha : a < preVariationFun f s
⊢ ∃ (P : Finpartition (Subtype.mk (p := MeasurableSet) s hs)),
    preVariationFun f s ≤ ∑ p ∈ P.parts, f (↑p : Set X) + (↑ε : ℝ≥0∞)
have inl : ∀ (P : Finpartition (Subtype.mk (p := MeasurableSet) s hs)) (hP : a < ∑ p ∈ P.parts, f (↑p : Set X)),
  ∃ (P : Finpartition (Subtype.mk (p := MeasurableSet) s hs)),
    preVariationFun f s ≤ ∑ p ∈ P.parts, f (↑p : Set X) + (↑ε : ℝ≥0∞)
Tactic: obtain ⟨P, hP⟩ := exists_Finpartition_sum_gt f hs ha
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.PreVariation (goal)
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s : Set X
hs : MeasurableSet s
ε : ℝ≥0
hε : 0 < ε
h : preVariationFun f s ≠ ∞
ε' : ℝ≥0 := min ε (preVariationFun f s).toNNReal
hε' : (↑ε' : ℝ≥0∞) ≤ preVariationFun f s
this_1 : ε' ≤ ε
hw : preVariationFun f s ≠ 0
this : 0 < ε'
a : ℝ≥0∞ := preVariationFun f s - (↑ε' : ℝ≥0∞)
ha : a < preVariationFun f s
P : Finpartition (Subtype.mk (p := MeasurableSet) s hs)
hP : a < ∑ p ∈ P.parts, f (↑p : Set X)
⊢ ∃ (P : Finpartition (Subtype.mk (p := MeasurableSet) s hs)),
    preVariationFun f s ≤ ∑ p ∈ P.parts, f (↑p : Set X) + (↑ε : ℝ≥0∞)
have h₁ : preVariationFun f s ≤ ∑ p ∈ P.parts, f (↑p : Set X) + (↑ε : ℝ≥0∞)
Tactic: use P
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.PreVariation (goal)
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s : Set X
hs : MeasurableSet s
ε : ℝ≥0
hε : 0 < ε
h : preVariationFun f s ≠ ∞
ε' : ℝ≥0 := min ε (preVariationFun f s).toNNReal
hε' : (↑ε' : ℝ≥0∞) ≤ preVariationFun f s
this_1 : ε' ≤ ε
hw : preVariationFun f s ≠ 0
this : 0 < ε'
a : ℝ≥0∞ := preVariationFun f s - (↑ε' : ℝ≥0∞)
ha : a < preVariationFun f s
P : Finpartition (Subtype.mk (p := MeasurableSet) s hs)
hP : a < ∑ p ∈ P.parts, f (↑p : Set X)
⊢ preVariationFun f s ≤ ∑ p ∈ P.parts, f (↑p : Set X) + (↑ε : ℝ≥0∞)
have calc : a + (↑ε' : ℝ≥0∞) ≤ ∑ p ∈ P.parts, f (↑p : Set X) + (↑ε' : ℝ≥0∞)
Tactic: calc preVariationFun f s
      _ = a + ε' := (tsub_add_cancel_of_le hε').symm
      _ ≤ ∑ p ∈ P.parts, f p + ε' := by
        exact (ENNReal.add_le_add_iff_right coe_ne_top).mpr (le_of_lt hP)
      _ ≤ ∑ p ∈ P.parts, f p + ε := by gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.PreVariation (goal)
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s : Set X
hs : MeasurableSet s
ε : ℝ≥0
hε : 0 < ε
h : preVariationFun f s ≠ ∞
ε' : ℝ≥0 := min ε (preVariationFun f s).toNNReal
hε' : (↑ε' : ℝ≥0∞) ≤ preVariationFun f s
this_1 : ε' ≤ ε
hw : preVariationFun f s ≠ 0
this : 0 < ε'
a : ℝ≥0∞ := preVariationFun f s - (↑ε' : ℝ≥0∞)
ha : a < preVariationFun f s
P : Finpartition (Subtype.mk (p := MeasurableSet) s hs)
hP : a < ∑ p ∈ P.parts, f (↑p : Set X)
calc : a + (↑ε' : ℝ≥0∞) ≤ ∑ p ∈ P.parts, f (↑p : Set X) + (↑ε' : ℝ≥0∞)
⊢ preVariationFun f s ≤ ∑ p ∈ P.parts, f (↑p : Set X) + (↑ε : ℝ≥0∞)
have calc₁ : ∑ p ∈ P.parts, f (↑p : Set X) + (↑ε' : ℝ≥0∞) ≤ ∑ p ∈ P.parts, f (↑p : Set X) + (↑ε : ℝ≥0∞)
Tactic: calc preVariationFun f s
      _ = a + ε' := (tsub_add_cancel_of_le hε').symm
      _ ≤ ∑ p ∈ P.parts, f p + ε' := by
        exact (ENNReal.add_le_add_iff_right coe_ne_top).mpr (le_of_lt hP)
      _ ≤ ∑ p ∈ P.parts, f p + ε := by gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.PreVariation (goal)
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
P : (i : ℕ) → Finpartition (Subtype.mk (p := MeasurableSet) (s i) ⋯)
n : ℕ
s' : (i : ℕ) → Subtype (α := Set X) MeasurableSet := fun (i : ℕ) ↦ Subtype.mk (p := MeasurableSet) (s i) ⋯
i : ℕ
h : i ∈ (↑(Finset.range n) : Set ℕ)
j : ℕ
h_1 : j ∈ (↑(Finset.range n) : Set ℕ)
hij : i ≠ j
⊢ (Disjoint on s') i j
have simp : (↑(s' i ⊓ s' j) : Set X) = (↑⊥ : Set X)
Tactic: simp only [Function.onFun, disjoint_iff, Subtype.ext_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.PreVariation (hypothesis)
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
P : (i : ℕ) → Finpartition (Subtype.mk (p := MeasurableSet) (s i) ⋯)
n : ℕ
s' : (i : ℕ) → Subtype (α := Set X) MeasurableSet := fun (i : ℕ) ↦ Subtype.mk (p := MeasurableSet) (s i) ⋯
⊢ ∑ i ∈ Finset.range n, ∑ p ∈ (P i).parts, f (↑p : Set X) ≤ preVariationFun f (⋃ (i : ℕ), s i)
have hs_disj : (↑(Finset.range n) : Set ℕ).PairwiseDisjoint s'
Tactic: have hs_disj : Set.PairwiseDisjoint (Finset.range n : Set ℕ) s' := fun i _ j _ hij => by
    simp only [Function.onFun, disjoint_iff, Subtype.ext_iff]
    exact Set.disjoint_iff_inter_eq_empty.mp (hs' hij)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.PreVariation (goal)
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
P : (i : ℕ) → Finpartition (Subtype.mk (p := MeasurableSet) (s i) ⋯)
n : ℕ
s' : (i : ℕ) → Subtype (α := Set X) MeasurableSet := fun (i : ℕ) ↦ Subtype.mk (p := MeasurableSet) (s i) ⋯
hs_disj : (↑(Finset.range n) : Set ℕ).PairwiseDisjoint s'
Q : Finpartition (α := Subtype (α := Set X) MeasurableSet)
  ((Finset.range n).sup fun (i : ℕ) ↦ Subtype.mk (p := MeasurableSet) (s i) ⋯) :=
  Finpartition.combine P ⋯
⊢ (Finset.range n).sup s' ≤ Subtype.mk (p := MeasurableSet) (⋃ (i : ℕ), s i) ⋯
have rw : ⋃ x ∈ Finset.range n, (↑(s' x) : Set X) ≤ (↑(Subtype.mk (p := MeasurableSet) (⋃ (i : ℕ), s i) sorry) : Set X)
Tactic: rw [← Subtype.coe_le_coe, Finset.sup_coe (Psup := by measurability), Finset.sup_set_eq_biUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.PreVariation (hypothesis)
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
P : (i : ℕ) → Finpartition (Subtype.mk (p := MeasurableSet) (s i) ⋯)
n : ℕ
s' : (i : ℕ) → Subtype (α := Set X) MeasurableSet := fun (i : ℕ) ↦ Subtype.mk (p := MeasurableSet) (s i) ⋯
hs_disj : (↑(Finset.range n) : Set ℕ).PairwiseDisjoint s'
Q : Finpartition (α := Subtype (α := Set X) MeasurableSet)
  ((Finset.range n).sup fun (i : ℕ) ↦ Subtype.mk (p := MeasurableSet) (s i) ⋯) :=
  Finpartition.combine P ⋯
⊢ ∑ i ∈ Finset.range n, ∑ p ∈ (P i).parts, f (↑p : Set X) ≤ preVariationFun f (⋃ (i : ℕ), s i)
have hQ_le : (Finset.range n).sup s' ≤ Subtype.mk (p := MeasurableSet) (⋃ (i : ℕ), s i) sorry
Tactic: have hQ_le : (Finset.range n).sup s' ≤ ⟨⋃ i, s i, MeasurableSet.iUnion hs⟩ := by
    rw [← Subtype.coe_le_coe, Finset.sup_coe (Psup := by measurability), Finset.sup_set_eq_biUnion]
    exact Set.iUnion₂_subset fun i _ => Set.subset_iUnion s i
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.PreVariation (goal)
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
⊢ ∑' (i : ℕ), preVariationFun f (s i) ≤ preVariationFun f (⋃ (i : ℕ), s i)
have refine : ∀ (n : ℕ), ∑ i ∈ Finset.range n, preVariationFun f (s i) ≤ preVariationFun f (⋃ (i : ℕ), s i)
Tactic: refine ENNReal.tsum_le_of_sum_range_le fun n ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.PreVariation (goal)
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
n : ℕ
⊢ ∑ i ∈ Finset.range n, preVariationFun f (s i) ≤ preVariationFun f (⋃ (i : ℕ), s i)
have pos : ∀ (hn : n = 0), ∑ i ∈ Finset.range n, preVariationFun f (s i) ≤ preVariationFun f (⋃ (i : ℕ), s i)
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.PreVariation (goal)
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
n : ℕ
pos : ∀ (hn : n = 0), ∑ i ∈ Finset.range n, preVariationFun f (s i) ≤ preVariationFun f (⋃ (i : ℕ), s i)
⊢ ∑ i ∈ Finset.range n, preVariationFun f (s i) ≤ preVariationFun f (⋃ (i : ℕ), s i)
have neg : ∀ (hn : ¬n = 0), ∑ i ∈ Finset.range n, preVariationFun f (s i) ≤ preVariationFun f (⋃ (i : ℕ), s i)
Tactic: by_cases hn : n = 0