awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
g : StieltjesFunction R
y : R
hfg : Eq (α := Measure R) f.measure g.measure
hy : (↑f : R → ℝ) y = (↑g : R → ℝ) y
x : R
hxy : y ≤ x
hf : ofReal ((↑g : R → ℝ) x - (↑g : R → ℝ) y) = ofReal ((↑f : R → ℝ) x - (↑f : R → ℝ) y)
h : (↑f : R → ℝ) y ≤ (↑f : R → ℝ) x
⊢ 0 ≤ (↑f : R → ℝ) x - (↑f : R → ℝ) y

Tactic:
rw [sub_nonneg]

Premises used: sub_nonneg
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
g : StieltjesFunction R
y : R
hfg : Eq (α := Measure R) f.measure g.measure
hy : (↑f : R → ℝ) y = (↑g : R → ℝ) y
x : R
hxy : y ≤ x
hf : ofReal ((↑g : R → ℝ) x - (↑g : R → ℝ) y) = ofReal ((↑f : R → ℝ) x - (↑f : R → ℝ) y)
⊢ (↑f : R → ℝ) y ≤ (↑f : R → ℝ) x

Tactic:
f.mono hxy

Premises used: StieltjesFunction.mono
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
g : StieltjesFunction R
y : R
hfg : Eq (α := Measure R) f.measure g.measure
hy : (↑f : R → ℝ) y = (↑g : R → ℝ) y
x : R
hxy : y ≤ x
hf : ofReal ((↑g : R → ℝ) x - (↑g : R → ℝ) y) = ofReal ((↑f : R → ℝ) x - (↑f : R → ℝ) y)
⊢ (↑f : R → ℝ) y ≤ (↑f : R → ℝ) x

Tactic:
exact f.mono hxy

Premises used: StieltjesFunction.mono
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
g : StieltjesFunction R
y : R
hfg : Eq (α := Measure R) f.measure g.measure
hy : (↑f : R → ℝ) y = (↑g : R → ℝ) y
x : R
⊢ x ≤ y ∨ y ≤ x

Tactic:
cases le_total x y with
  | inl hxy =>
    have hf := measure_Ioc f x y
    rw [hfg, measure_Ioc g x y, ENNReal.ofReal_eq_ofReal_iff, eq_comm, hy] at hf
    · simpa using hf
    · rw [sub_nonneg]
      exact g.mono hxy
    · rw [sub_nonneg]
      exact f.mono hxy
  | inr hxy =>
    have hf := measure_Ioc f y x
    rw [hfg, measure_Ioc g y x, ENNReal.ofReal_eq_ofReal_iff, eq_comm, hy] at hf
    · simpa using hf
    · rw [sub_nonneg]
      exact g.mono hxy
    · rw [sub_nonneg]
      exact f.mono hxy

Premises used: ENNReal.ofReal_eq_ofReal_iff, le_total, eq_comm, StieltjesFunction.measure_Ioc, sub_nonneg
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
c : ℝ
apply :
  ∀ (a b : R) (hab : a ≤ b),
    Eq (α := ℝ≥0∞)
      (((StieltjesFunction.measure (StieltjesFunction.const R c) : Measure R) : (a : Set R) → ℝ≥0∞) (Icc a b) : ℝ≥0∞)
      (((0 : Measure R) : (a : Set R) → ℝ≥0∞) (Icc a b) : ℝ≥0∞)
⊢ Eq (α := Measure R) (StieltjesFunction.measure (StieltjesFunction.const R c)) 0

Tactic:
apply Measure.ext_of_Icc _ _ (fun a b hab ↦ ?_)

Premises used: MeasureTheory.Measure.ext_of_Icc
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
c : ℝ
a b : R
hab : a ≤ b
simp : c ≤ leftLim (↑(StieltjesFunction.const R c) : R → ℝ) a
⊢ Eq (α := ℝ≥0∞)
    (((StieltjesFunction.measure (StieltjesFunction.const R c) : Measure R) : (a : Set R) → ℝ≥0∞) (Icc a b) : ℝ≥0∞)
    (((0 : Measure R) : (a : Set R) → ℝ≥0∞) (Icc a b) : ℝ≥0∞)

Tactic:
simp only [measure_Icc, const_apply, Measure.coe_zero, Pi.ofNat_apply, ofReal_eq_zero,
    tsub_le_iff_right, zero_add]

Premises used: ENNReal.ofReal_eq_zero, StieltjesFunction.const_apply, Pi.ofNat_apply, zero_add, tsub_le_iff_right, StieltjesFunction.measure_Icc, MeasureTheory.Measure.coe_zero
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
c : ℝ
a b : R
hab : a ≤ b
rw : c ≤ (↑(StieltjesFunction.const R c) : R → ℝ) a
rw₁ : ContinuousWithinAt (↑(StieltjesFunction.const R c) : R → ℝ) (Iic a) a
⊢ c ≤ leftLim (↑(StieltjesFunction.const R c) : R → ℝ) a

Tactic:
rw [ContinuousWithinAt.leftLim_eq]

Premises used: ContinuousWithinAt.leftLim_eq
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
c : ℝ
a b : R
hab : a ≤ b
⊢ c ≤ (↑(StieltjesFunction.const R c) : R → ℝ) a

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
c : ℝ
a b : R
hab : a ≤ b
⊢ ContinuousWithinAt (↑(StieltjesFunction.const R c) : R → ℝ) (Iic a) a

Tactic:
continuousWithinAt_const

Premises used: continuousWithinAt_const
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
c : ℝ
a b : R
hab : a ≤ b
⊢ ContinuousWithinAt (↑(StieltjesFunction.const R c) : R → ℝ) (Iic a) a

Tactic:
exact continuousWithinAt_const

Premises used: continuousWithinAt_const
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
⊢ Eq.{u_1 + 1} (α := Measure R) (StieltjesFunction.measure 0) 0

Tactic:
measure_const 0

Premises used: OfNat.ofNat, StieltjesFunction.measure_const
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
f g : StieltjesFunction R
⊢ (f + g).measure = HAdd.hAdd (α := Measure R) f.measure g.measure

Tactic:
Measure.ext_of_Icc _ _ (fun a b h ↦ ?_)

Premises used: MeasureTheory.Measure.ext_of_Icc
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
f g : StieltjesFunction R
refine :
  ∀ (a b : R) (h : a ≤ b),
    Eq (α := ℝ≥0∞) ((((f + g).measure : Measure R) : (a : Set R) → ℝ≥0∞) (Icc a b) : ℝ≥0∞)
      ((HAdd.hAdd (α := Measure R) f.measure g.measure : (a : Set R) → ℝ≥0∞) (Icc a b) : ℝ≥0∞)
⊢ (f + g).measure = HAdd.hAdd (α := Measure R) f.measure g.measure

Tactic:
refine Measure.ext_of_Icc _ _ (fun a b h ↦ ?_)

Premises used: MeasureTheory.Measure.ext_of_Icc
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
f g : StieltjesFunction R
a b : R
h : a ≤ b
inl : ∀ (ha : 𝓝[<] a = ⊥), leftLim (↑(f + g) : R → ℝ) a = leftLim (↑f : R → ℝ) a + leftLim (↑g : R → ℝ) a
inr : ∀ (ha : (𝓝[<] a).NeBot), leftLim (↑(f + g) : R → ℝ) a = leftLim (↑f : R → ℝ) a + leftLim (↑g : R → ℝ) a
⊢ leftLim (↑(f + g) : R → ℝ) a = leftLim (↑f : R → ℝ) a + leftLim (↑g : R → ℝ) a

Tactic:
rcases Filter.eq_or_neBot (𝓝[<] a) with ha | ha

Premises used: nhdsWithin, Filter.eq_or_neBot, Set.Iio
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
f g : StieltjesFunction R
a b : R
h : a ≤ b
ha : 𝓝[<] a = ⊥
⊢ leftLim (↑(f + g) : R → ℝ) a = leftLim (↑f : R → ℝ) a + leftLim (↑g : R → ℝ) a

Tactic:
simp [leftLim_eq_of_eq_bot _ ha]

Premises used: leftLim_eq_of_eq_bot
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
f g : StieltjesFunction R
a b : R
h : a ≤ b
ha : (𝓝[<] a).NeBot
⊢ leftLim (↑(f + g) : R → ℝ) a = leftLim (↑f : R → ℝ) a + leftLim (↑g : R → ℝ) a

Tactic:
tendsto_nhds_unique ((f + g).mono.tendsto_leftLim a)
        ((f.mono.tendsto_leftLim a).add (g.mono.tendsto_leftLim a))

Premises used: StieltjesFunction.mono, HAdd.hAdd, Filter.Tendsto.add, tendsto_nhds_unique, Monotone.tendsto_leftLim
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
f g : StieltjesFunction R
a b : R
h : a ≤ b
ha : (𝓝[<] a).NeBot
⊢ leftLim (↑(f + g) : R → ℝ) a = leftLim (↑f : R → ℝ) a + leftLim (↑g : R → ℝ) a

Tactic:
exact tendsto_nhds_unique ((f + g).mono.tendsto_leftLim a)
        ((f.mono.tendsto_leftLim a).add (g.mono.tendsto_leftLim a))

Premises used: StieltjesFunction.mono, HAdd.hAdd, Filter.Tendsto.add, tendsto_nhds_unique, Monotone.tendsto_leftLim
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
f g : StieltjesFunction R
a b : R
h : a ≤ b
⊢ leftLim (↑(f + g) : R → ℝ) a = leftLim (↑f : R → ℝ) a + leftLim (↑g : R → ℝ) a

Tactic:
have : leftLim (f + g) a = leftLim f a + leftLim g a := by
    rcases Filter.eq_or_neBot (𝓝[<] a) with ha | ha
    · simp [leftLim_eq_of_eq_bot _ ha]
    · exact tendsto_nhds_unique ((f + g).mono.tendsto_leftLim a)
        ((f.mono.tendsto_leftLim a).add (g.mono.tendsto_leftLim a))
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
f g : StieltjesFunction R
a b : R
h : a ≤ b
this : leftLim (↑(f + g) : R → ℝ) a = leftLim (↑f : R → ℝ) a + leftLim (↑g : R → ℝ) a
simp :
  ofReal ((↑f : R → ℝ) b + (↑g : R → ℝ) b - (leftLim (↑f : R → ℝ) a + leftLim (↑g : R → ℝ) a)) =
    ofReal ((↑f : R → ℝ) b - leftLim (↑f : R → ℝ) a) + ofReal ((↑g : R → ℝ) b - leftLim (↑g : R → ℝ) a)
⊢ Eq (α := ℝ≥0∞) ((((f + g).measure : Measure R) : (a : Set R) → ℝ≥0∞) (Icc a b) : ℝ≥0∞)
    ((HAdd.hAdd (α := Measure R) f.measure g.measure : (a : Set R) → ℝ≥0∞) (Icc a b) : ℝ≥0∞)

Tactic:
simp only [measure_Icc, add_apply, Measure.coe_add, Pi.add_apply, this]

Premises used: MeasureTheory.Measure.coe_add, StieltjesFunction.add_apply, Pi.add_apply, StieltjesFunction.measure_Icc
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
f g : StieltjesFunction R
a b : R
h : a ≤ b
this : leftLim (↑(f + g) : R → ℝ) a = leftLim (↑f : R → ℝ) a + leftLim (↑g : R → ℝ) a
rw :
  ofReal ((↑f : R → ℝ) b + (↑g : R → ℝ) b - (leftLim (↑f : R → ℝ) a + leftLim (↑g : R → ℝ) a)) =
    ofReal ((↑f : R → ℝ) b - leftLim (↑f : R → ℝ) a + ((↑g : R → ℝ) b - leftLim (↑g : R → ℝ) a))
⊢ ofReal ((↑f : R → ℝ) b + (↑g : R → ℝ) b - (leftLim (↑f : R → ℝ) a + leftLim (↑g : R → ℝ) a)) =
    ofReal ((↑f : R → ℝ) b - leftLim (↑f : R → ℝ) a) + ofReal ((↑g : R → ℝ) b - leftLim (↑g : R → ℝ) a)

Tactic:
rw [← ENNReal.ofReal_add (sub_nonneg_of_le (f.mono.leftLim_le h))
    (sub_nonneg_of_le (g.mono.leftLim_le h))]

Premises used: sub_nonneg_of_le, StieltjesFunction.mono, ENNReal.ofReal_add, Monotone.leftLim_le
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
f g : StieltjesFunction R
a b : R
h : a ≤ b
this : leftLim (↑(f + g) : R → ℝ) a = leftLim (↑f : R → ℝ) a + leftLim (↑g : R → ℝ) a
⊢ ofReal ((↑f : R → ℝ) b + (↑g : R → ℝ) b - (leftLim (↑f : R → ℝ) a + leftLim (↑g : R → ℝ) a)) =
    ofReal ((↑f : R → ℝ) b - leftLim (↑f : R → ℝ) a + ((↑g : R → ℝ) b - leftLim (↑g : R → ℝ) a))

Tactic:
ring_nf
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
c : ℝ≥0
f : StieltjesFunction R
⊢ (c • f).measure = HSMul.hSMul (β := Measure R) c f.measure

Tactic:
Measure.ext_of_Icc _ _ (fun a b h ↦ ?_)

Premises used: MeasureTheory.Measure.ext_of_Icc
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
c : ℝ≥0
f : StieltjesFunction R
refine :
  ∀ (a b : R) (h : a ≤ b),
    Eq (α := ℝ≥0∞) ((((c • f).measure : Measure R) : (a : Set R) → ℝ≥0∞) (Icc a b) : ℝ≥0∞)
      ((HSMul.hSMul (β := Measure R) c f.measure : (a : Set R) → ℝ≥0∞) (Icc a b) : ℝ≥0∞)
⊢ (c • f).measure = HSMul.hSMul (β := Measure R) c f.measure

Tactic:
refine Measure.ext_of_Icc _ _ (fun a b h ↦ ?_)

Premises used: MeasureTheory.Measure.ext_of_Icc
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
c : ℝ≥0
f : StieltjesFunction R
a b : R
h : a ≤ b
simp :
  ofReal ((↑(c • f) : R → ℝ) b - leftLim (↑(c • f) : R → ℝ) a) = c • ofReal ((↑f : R → ℝ) b - leftLim (↑f : R → ℝ) a)
⊢ Eq (α := ℝ≥0∞) ((((c • f).measure : Measure R) : (a : Set R) → ℝ≥0∞) (Icc a b) : ℝ≥0∞)
    ((HSMul.hSMul (β := Measure R) c f.measure : (a : Set R) → ℝ≥0∞) (Icc a b) : ℝ≥0∞)

Tactic:
simp only [measure_Icc, Measure.smul_apply]

Premises used: StieltjesFunction.measure_Icc, MeasureTheory.Measure.smul_apply
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
c : ℝ≥0
f : StieltjesFunction R
a b : R
h : a ≤ b
inl : ∀ (ha : 𝓝[<] a = ⊥), leftLim (↑(c • f) : R → ℝ) a = (↑c : ℝ) * leftLim (↑f : R → ℝ) a
inr : ∀ (ha : (𝓝[<] a).NeBot), leftLim (↑(c • f) : R → ℝ) a = (↑c : ℝ) * leftLim (↑f : R → ℝ) a
⊢ leftLim (↑(c • f) : R → ℝ) a = (↑c : ℝ) * leftLim (↑f : R → ℝ) a

Tactic:
rcases Filter.eq_or_neBot (𝓝[<] a) with ha | ha

Premises used: nhdsWithin, Filter.eq_or_neBot, Set.Iio
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
c : ℝ≥0
f : StieltjesFunction R
a b : R
h : a ≤ b
ha : 𝓝[<] a = ⊥
inl : (↑(c • f) : R → ℝ) a = (↑c : ℝ) * (↑f : R → ℝ) a
⊢ leftLim (↑(c • f) : R → ℝ) a = (↑c : ℝ) * leftLim (↑f : R → ℝ) a

Tactic:
simp [leftLim_eq_of_eq_bot _ ha]

Premises used: leftLim_eq_of_eq_bot
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
c : ℝ≥0
f : StieltjesFunction R
a b : R
h : a ≤ b
ha : 𝓝[<] a = ⊥
⊢ (↑(c • f) : R → ℝ) a = (↑c : ℝ) * (↑f : R → ℝ) a

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
c : ℝ≥0
f : StieltjesFunction R
a b : R
h : a ≤ b
ha : (𝓝[<] a).NeBot
⊢ leftLim (↑(c • f) : R → ℝ) a = (↑c : ℝ) * leftLim (↑f : R → ℝ) a

Tactic:
tendsto_nhds_unique ((c • f).mono.tendsto_leftLim a)
        ((f.mono.tendsto_leftLim a).const_smul c)

Premises used: StieltjesFunction.mono, Filter.Tendsto.const_smul, HSMul.hSMul, tendsto_nhds_unique, Monotone.tendsto_leftLim
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
c : ℝ≥0
f : StieltjesFunction R
a b : R
h : a ≤ b
ha : (𝓝[<] a).NeBot
⊢ leftLim (↑(c • f) : R → ℝ) a = (↑c : ℝ) * leftLim (↑f : R → ℝ) a

Tactic:
exact tendsto_nhds_unique ((c • f).mono.tendsto_leftLim a)
        ((f.mono.tendsto_leftLim a).const_smul c)

Premises used: StieltjesFunction.mono, Filter.Tendsto.const_smul, HSMul.hSMul, tendsto_nhds_unique, Monotone.tendsto_leftLim
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
c : ℝ≥0
f : StieltjesFunction R
a b : R
h : a ≤ b
⊢ leftLim (↑(c • f) : R → ℝ) a = (↑c : ℝ) * leftLim (↑f : R → ℝ) a

Tactic:
have : leftLim (c • f) a = c * leftLim f a := by
    rcases Filter.eq_or_neBot (𝓝[<] a) with ha | ha
    · simp [leftLim_eq_of_eq_bot _ ha]
      rfl
    · exact tendsto_nhds_unique ((c • f).mono.tendsto_leftLim a)
        ((f.mono.tendsto_leftLim a).const_smul c)
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
c : ℝ≥0
f : StieltjesFunction R
a b : R
h : a ≤ b
this : leftLim (↑(c • f) : R → ℝ) a = (↑c : ℝ) * leftLim (↑f : R → ℝ) a
rw :
  (↑c : ℝ≥0∞) • ofReal ((↑f : R → ℝ) b - leftLim (↑f : R → ℝ) a) = c • ofReal ((↑f : R → ℝ) b - leftLim (↑f : R → ℝ) a)
⊢ ofReal ((↑c : ℝ) * (↑f : R → ℝ) b - leftLim (↑(c • f) : R → ℝ) a) =
    c • ofReal ((↑f : R → ℝ) b - leftLim (↑f : R → ℝ) a)

Tactic:
rw [this, ← _root_.mul_sub, ENNReal.ofReal_mul zero_le_coe, ofReal_coe_nnreal, ← smul_eq_mul]

Premises used: mul_sub, ENNReal.ofReal_mul, ENNReal.ofReal_coe_nnreal, smul_eq_mul, NNReal.zero_le_coe
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
c : ℝ≥0
f : StieltjesFunction R
a b : R
h : a ≤ b
this : leftLim (↑(c • f) : R → ℝ) a = (↑c : ℝ) * leftLim (↑f : R → ℝ) a
⊢ (↑c : ℝ≥0∞) • ofReal ((↑f : R → ℝ) b - leftLim (↑f : R → ℝ) a) = c • ofReal ((↑f : R → ℝ) b - leftLim (↑f : R → ℝ) a)

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Measure.Sub
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
⊢ μ - ν = sInf {d : Measure α | μ ≤ d + ν}

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Measure.Sub
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν d : Measure α
h : μ ≤ d + ν
⊢ μ - ν ≤ d

Tactic:
sInf_le h

Premises used: sInf_le
-- Module: Mathlib.MeasureTheory.Measure.Sub
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h rwa rwa₁ rwa₂ rwa₃ : μ ≤ ν
⊢ μ ≤ 0 + ν

Tactic:
rwa [zero_add]

Premises used: zero_add
-- Module: Mathlib.MeasureTheory.Measure.Sub
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
⊢ μ - ν ≤ μ

Tactic:
sub_le_of_le_add <| Measure.le_add_right le_rfl

Premises used: le_rfl, MeasureTheory.Measure.sub_le_of_le_add, MeasureTheory.Measure.le_add_right
-- Module: Mathlib.MeasureTheory.Measure.Sub
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
⊢ μ - ⊤ = 0

Tactic:
sub_eq_zero_of_le le_top

Premises used: MeasureTheory.Measure.sub_eq_zero_of_le, le_top
-- Module: Mathlib.MeasureTheory.Measure.Sub
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
⊢ 0 - μ = 0

Tactic:
sub_eq_zero_of_le μ.zero_le

Premises used: MeasureTheory.Measure.zero_le, MeasureTheory.Measure.sub_eq_zero_of_le
-- Module: Mathlib.MeasureTheory.Measure.Sub
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
⊢ μ - μ = 0

Tactic:
sub_eq_zero_of_le le_rfl

Premises used: le_rfl, MeasureTheory.Measure.sub_eq_zero_of_le
-- Module: Mathlib.MeasureTheory.Measure.Sub
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
a : sInf {d : Measure α | μ ≤ d + 0} ≤ μ
a₁ : μ ≤ sInf {d : Measure α | μ ≤ d + 0}
⊢ sInf {d : Measure α | μ ≤ d + 0} = μ

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.MeasureTheory.Measure.Sub
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
⊢ sInf {d : Measure α | μ ≤ d + 0} ≤ μ

Tactic:
simp [sInf_le]

Premises used: sInf_le
-- Module: Mathlib.MeasureTheory.Measure.Sub
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
⊢ μ ≤ sInf {d : Measure α | μ ≤ d + 0}

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Sub
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
⊢ Eq (α := ENNReal)
    ((fun (t : Set α) (x : MeasurableSet t) ↦
        HSub.hSub (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)
          ((ν : (a : Set α) → ENNReal) t : ENNReal))
      ∅ ⋯)
    0

Tactic:
simp