awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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
⊢ 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'
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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)
h₁ : ∀ (i : ι) (hi : r < (μ i : (a : Set Ω) → ℝ≥0) (⋃ t ∈ T, t)), r < (μ i : (a : Set Ω) → ℝ≥0) G
⊢ ∀ᶠ (a : ι) in l, r < (μ a : (a : Set Ω) → ℝ≥0) G

Tactic:
filter_upwards [(tendsto_order.1 this).1 r T_meas] with i hi

Premises used: tendsto_order, And.left, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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)
i : ι
hi : r < (μ i : (a : Set Ω) → ℝ≥0) (⋃ t ∈ T, t)
⊢ r < (μ i : (a : Set Ω) → ℝ≥0) G

Tactic:
hi.trans_le <| ProbabilityMeasure.apply_mono _ TG

Premises used: MeasureTheory.ProbabilityMeasure.apply_mono, LT.lt.trans_le
-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
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)
i : ι
hi : r < (μ i : (a : Set Ω) → ℝ≥0) (⋃ t ∈ T, t)
⊢ r < (μ i : (a : Set Ω) → ℝ≥0) G

Tactic:
exact hi.trans_le <| ProbabilityMeasure.apply_mono _ TG

Premises used: MeasureTheory.ProbabilityMeasure.apply_mono, LT.lt.trans_le
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
⊢ preVariationFun f ∅ = 0

Tactic:
simp [preVariationFun]

Premises used: MeasureTheory.preVariationFun
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
h : ∀ (x : Set X), preVariationFun 0 x = 0 x
⊢ Eq.{u_1 + 1} (α := (s : Set X) → ℝ≥0∞) (preVariationFun 0) 0

Tactic:
ext
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
x : Set X
⊢ preVariationFun 0 x = 0 x

Tactic:
simp [preVariationFun]

Premises used: MeasureTheory.preVariationFun
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s : Set X
hs : MeasurableSet s
P : Finpartition (Subtype.mk (p := MeasurableSet) s hs)
⊢ ∑ p ∈ P.parts, f (↑p : Set X) ≤ preVariationFun f s

Tactic:
simpa [preVariationFun, hs, le_iSup_iff] using fun _ a ↦ a P

Premises used: MeasureTheory.preVariationFun, le_iSup_iff
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s : Set X
P : Finpartition s
hs : MeasurableSet s
hP : ∀ p ∈ P.parts (a := s), MeasurableSet p
⊢ ∀ ⦃s t : Set X⦄, MeasurableSet s → MeasurableSet t → MeasurableSet (s ⊔ t)

Tactic:
measurability
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s : Set X
P : Finpartition s
hs : MeasurableSet s
hP : ∀ p ∈ P.parts (a := s), MeasurableSet p
⊢ ∀ ⦃s t : Set X⦄, MeasurableSet s → MeasurableSet t → MeasurableSet (s ⊓ t)

Tactic:
measurability
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s : Set X
P : Finpartition s
hs : MeasurableSet s
hP : ∀ p ∈ P.parts (a := s), MeasurableSet p
⊢ MeasurableSet.{u_1} (α := X) ⊥

Tactic:
measurability
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
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
simp :
  LE.le (α := ℝ≥0∞) (∑ p ∈ P.parts (a := s), f p)
    (⨆ (P : Finpartition (Subtype.mk (p := MeasurableSet) s ⋯)), ∑ p ∈ P.parts, f (↑p : Set X))
⊢ ∑ p ∈ P.parts (a := s), f p ≤ preVariationFun f s

Tactic:
simp only [preVariationFun, hs, ↓reduceDIte]

Premises used: reduceDIte, MeasureTheory.preVariationFun
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
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
⊢ ∀ ⦃s t : Set X⦄, MeasurableSet s → MeasurableSet t → MeasurableSet (s ⊔ t)

Tactic:
measurability
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
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
⊢ ∀ ⦃s t : Set X⦄, MeasurableSet s → MeasurableSet t → MeasurableSet (s ⊓ t)

Tactic:
measurability
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
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
⊢ MeasurableSet.{u_1} (α := X) ⊥

Tactic:
measurability
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
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
⊢ LE.le (α := ℝ≥0∞) (∑ p ∈ (P.toMeasurableSet (s := s) hs hP).parts, f (↑p : Set X))
    (⨆ (Q : Finpartition (Subtype.mk (p := MeasurableSet) s hs)), ∑ p ∈ Q.parts, f (↑p : Set X))

Tactic:
le_iSup (fun Q => ∑ p ∈ Q.parts, f p.1) (P.toMeasurableSet hs hP)

Premises used: le_iSup, Finpartition.toMeasurableSet, Finset.sum
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
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
⊢ LE.le (α := ℝ≥0∞) (∑ p ∈ P.parts (a := s), f p)
    (⨆ (P : Finpartition (Subtype.mk (p := MeasurableSet) s ⋯)), ∑ p ∈ P.parts, f (↑p : Set X))

Tactic:
calc
    ∑ p ∈ P.parts, f p = ∑ p ∈ (P.toMeasurableSet hs hP).parts, f p :=
      P.sum_eq_sum_finpartition_subtype (by measurability) (by measurability)
        (by measurability) hs hP f
    _ ≤ ⨆ (Q : Finpartition (⟨s, hs⟩ : Subtype MeasurableSet)), ∑ p ∈ Q.parts, f p :=
      le_iSup (fun Q => ∑ p ∈ Q.parts, f p.1) (P.toMeasurableSet hs hP)

Premises used: le_iSup, Finpartition.parts, Subtype.mk, Finpartition.sum_eq_sum_finpartition_subtype, Finpartition.toMeasurableSet, Finpartition, Finset.sum
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
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₂
neg : ∀ (heq : ¬s₁ = s₂), ∑ p ∈ P.parts, f (↑p : Set X) ≤ preVariationFun f s₂
⊢ ∑ p ∈ P.parts, f (↑p : Set X) ≤ preVariationFun f s₂

Tactic:
by_cases heq : s₁ = s₂
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
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₂
pos : ∑ p ∈ P.parts, f (↑p : Set X) ≤ preVariationFun f s₁
⊢ ∑ p ∈ P.parts, f (↑p : Set X) ≤ preVariationFun f s₂

Tactic:
rw [← heq]
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
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₁

Tactic:
sum_le f hs₁ P

Premises used: MeasureTheory.preVariation.sum_le
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
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₁

Tactic:
exact sum_le f hs₁ P

Premises used: MeasureTheory.preVariation.sum_le
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
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₁) ⋯
⊢ b ≠ ⊥

Tactic:
have hb : b ≠ ⊥ := fun hc => heq (h.antisymm (Set.diff_eq_empty.mp (congrArg (·.1) hc)))
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
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 ≠ ⊥
simp : (↑(Subtype.mk (p := MeasurableSet) s₁ hs₁ ⊓ Subtype.mk (p := MeasurableSet) (s₂ \ s₁) ⋯) : Set X) = (↑⊥ : Set X)
⊢ Disjoint (Subtype.mk (p := MeasurableSet) s₁ hs₁) b

Tactic:
simp only [b, disjoint_iff, Subtype.ext_iff]

Premises used: disjoint_iff, Subtype.ext_iff
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
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 ≠ ⊥
⊢ (↑(Subtype.mk (p := MeasurableSet) s₁ hs₁ ⊓ Subtype.mk (p := MeasurableSet) (s₂ \ s₁) ⋯) : Set X) = (↑⊥ : Set X)

Tactic:
Set.inter_diff_self s₁ s₂

Premises used: Set.inter_diff_self
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
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 ≠ ⊥
⊢ (↑(Subtype.mk (p := MeasurableSet) s₁ hs₁ ⊓ Subtype.mk (p := MeasurableSet) (s₂ \ s₁) ⋯) : Set X) = (↑⊥ : Set X)

Tactic:
exact Set.inter_diff_self s₁ s₂

Premises used: Set.inter_diff_self
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
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

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₂
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
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
⊢ 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)
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
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
hc : Subtype.mk (p := MeasurableSet) s₁ hs₁ ⊔ b = Subtype.mk (p := MeasurableSet) s₂ hs₂
⊢ LE.le (α := ℝ≥0∞) (∑ p ∈ P.parts, f (↑p : Set X)) (∑ p ∈ (P.extend hb hab hc).parts, f (↑p : Set X))

Tactic:
Finset.sum_le_sum_of_subset fun _ hx => Finset.mem_insert_of_mem hx

Premises used: Finset.sum_le_sum_of_subset, Finset.mem_insert_of_mem
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
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
hc : Subtype.mk (p := MeasurableSet) s₁ hs₁ ⊔ b = Subtype.mk (p := MeasurableSet) s₂ hs₂
⊢ ∑ p ∈ (P.extend hb hab hc).parts, f (↑p : Set X) ≤ preVariationFun f s₂

Tactic:
sum_le f hs₂ _

Premises used: MeasureTheory.preVariation.sum_le
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
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
hc : Subtype.mk (p := MeasurableSet) s₁ hs₁ ⊔ b = Subtype.mk (p := MeasurableSet) s₂ hs₂
⊢ ∑ p ∈ P.parts, f (↑p : Set X) ≤ preVariationFun f s₂

Tactic:
calc ∑ p ∈ P.parts, f p
      _ ≤ ∑ p ∈ (P.extend hb hab hc).parts, f p :=
          Finset.sum_le_sum_of_subset fun _ hx => Finset.mem_insert_of_mem hx
      _ ≤ preVariationFun f s₂ := sum_le f hs₂ _

Premises used: Finpartition.parts, Finset.sum_le_sum_of_subset, Finset.mem_insert_of_mem, MeasureTheory.preVariation.sum_le, Finpartition.extend, MeasureTheory.preVariationFun
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
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₂
neg : ∀ (hs₁ : ¬MeasurableSet s₁), preVariationFun f s₁ ≤ preVariationFun f s₂
⊢ preVariationFun f s₁ ≤ preVariationFun f s₂

Tactic:
by_cases hs₁ : MeasurableSet s₁

Premises used: MeasurableSet
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
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₁
⊢ ∀ (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
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
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₁
this :
  ∀ (P : Finpartition (Subtype.mk (p := MeasurableSet) s₁ hs₁)), ∑ p ∈ P.parts, f (↑p : Set X) ≤ preVariationFun f s₂
⊢ preVariationFun f s₁ ≤ preVariationFun f s₂

Tactic:
simp_all [preVariationFun]

Premises used: MeasureTheory.preVariationFun
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
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₂

Tactic:
simp [preVariationFun, hs₁]

Premises used: MeasureTheory.preVariationFun
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s : Set X
hs : MeasurableSet s
a : ℝ≥0∞
ha : a < preVariationFun f s
⊢ ∃ (P : Finpartition (Subtype.mk (p := MeasurableSet) s hs)), a < ∑ p ∈ P.parts, f (↑p : Set X)

Tactic:
simp_all [preVariationFun, lt_iSup_iff]

Premises used: MeasureTheory.preVariationFun, lt_iSup_iff
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
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
⊢ (↑ε' : ℝ≥0∞) ≤ preVariationFun f s

Tactic:
simp_all [ε']
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
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
⊢ (↑ε' : ℝ≥0∞) ≤ preVariationFun f s

Tactic:
have hε' : ε' ≤ preVariationFun f s := by simp_all [ε']
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
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
⊢ ε' ≤ ε

Tactic:
simp_all [ε']
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
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
⊢ ε' ≤ ε

Tactic:
have : ε' ≤ ε := by simp_all [ε']
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
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 : ε' ≤ ε
⊢ preVariationFun f s ≠ 0 ∨ preVariationFun f s = 0

Tactic:
ne_or_eq _ _

Premises used: ne_or_eq
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
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∞)
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∞)
⊢ ∃ (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 _ _

Premises used: ne_or_eq, MeasureTheory.preVariationFun
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
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
simp : 0 < ε ∧ 0 < (preVariationFun f s).toNNReal
⊢ 0 < ε'

Tactic:
simp only [lt_inf_iff, ε']

Premises used: lt_inf_iff
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
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 < ε ∧ 0 < (preVariationFun f s).toNNReal

Tactic:
⟨hε, toNNReal_pos hw h⟩

Premises used: ENNReal.toNNReal_pos, And.intro
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
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 < ε ∧ 0 < (preVariationFun f s).toNNReal

Tactic:
exact ⟨hε, toNNReal_pos hw h⟩
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
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 < ε'

Tactic:
have : 0 < ε' := by
      simp only [lt_inf_iff, ε']
      exact ⟨hε, toNNReal_pos hw h⟩
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
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∞)
⊢ (↑ε' : ℝ≥0∞) ≠ 0

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
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∞)
⊢ a < preVariationFun f s

Tactic:
have ha : a < preVariationFun f s := ENNReal.sub_lt_self h hw (by positivity)