awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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 : ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioc y x) = ofReal ((↑f : R → ℝ) x - (↑f : R → ℝ) y)
⊢ (↑f : R → ℝ) x = (↑g : R → ℝ) x
have h : ∀ (hf : (↑f : R → ℝ) x - (↑g : R → ℝ) y = (↑g : R → ℝ) x - (↑g : R → ℝ) y), (↑f : R → ℝ) x = (↑g : R → ℝ) x
Tactic: rw [hfg, measure_Ioc g y x, ENNReal.ofReal_eq_ofReal_iff, eq_comm, hy] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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 : ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioc y x) = ofReal ((↑f : R → ℝ) x - (↑f : R → ℝ) y)
h : ∀ (hf : (↑f : R → ℝ) x - (↑g : R → ℝ) y = (↑g : R → ℝ) x - (↑g : R → ℝ) y), (↑f : R → ℝ) x = (↑g : R → ℝ) x
⊢ (↑f : R → ℝ) x = (↑g : R → ℝ) x
have h₁ : ∀ (hf : ofReal ((↑g : R → ℝ) x - (↑g : R → ℝ) y) = ofReal ((↑f : R → ℝ) x - (↑f : R → ℝ) y)),
  0 ≤ (↑g : R → ℝ) x - (↑g : R → ℝ) y
Tactic: rw [hfg, measure_Ioc g y x, ENNReal.ofReal_eq_ofReal_iff, eq_comm, hy] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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 : ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioc y x) = ofReal ((↑f : R → ℝ) x - (↑f : R → ℝ) y)
h : ∀ (hf : (↑f : R → ℝ) x - (↑g : R → ℝ) y = (↑g : R → ℝ) x - (↑g : R → ℝ) y), (↑f : R → ℝ) x = (↑g : R → ℝ) x
h₁ :
  ∀ (hf : ofReal ((↑g : R → ℝ) x - (↑g : R → ℝ) y) = ofReal ((↑f : R → ℝ) x - (↑f : R → ℝ) y)),
    0 ≤ (↑g : R → ℝ) x - (↑g : R → ℝ) y
⊢ (↑f : R → ℝ) x = (↑g : R → ℝ) x
have h₂ : ∀ (hf : ofReal ((↑g : R → ℝ) x - (↑g : R → ℝ) y) = ofReal ((↑f : R → ℝ) x - (↑f : R → ℝ) y)),
  0 ≤ (↑f : R → ℝ) x - (↑f : R → ℝ) y
Tactic: rw [hfg, measure_Ioc g y x, ENNReal.ofReal_eq_ofReal_iff, eq_comm, hy] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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)
⊢ 0 ≤ (↑g : R → ℝ) x - (↑g : R → ℝ) y
have h : (↑g : R → ℝ) y ≤ (↑g : R → ℝ) x
Tactic: rw [sub_nonneg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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)
⊢ 0 ≤ (↑f : R → ℝ) x - (↑f : R → ℝ) y
have h : (↑f : R → ℝ) y ≤ (↑f : R → ℝ) x
Tactic: rw [sub_nonneg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (hypothesis)
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
⊢ (↑f : R → ℝ) x = (↑g : R → ℝ) x
have x₁ : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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 : ℝ
⊢ Eq (α := Measure R) (StieltjesFunction.measure (StieltjesFunction.const R c)) 0
have 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∞)
Tactic: apply Measure.ext_of_Icc _ _ (fun a b hab ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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
⊢ 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∞)
have simp : c ≤ leftLim (↑(StieltjesFunction.const R c) : R → ℝ) a
Tactic: simp only [measure_Icc, const_apply, Measure.coe_zero, Pi.ofNat_apply, ofReal_eq_zero,
    tsub_le_iff_right, zero_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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 ≤ leftLim (↑(StieltjesFunction.const R c) : R → ℝ) a
have rw : c ≤ (↑(StieltjesFunction.const R c) : R → ℝ) a
Tactic: rw [ContinuousWithinAt.leftLim_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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
⊢ c ≤ leftLim (↑(StieltjesFunction.const R c) : R → ℝ) a
have rw₁ : ContinuousWithinAt (↑(StieltjesFunction.const R c) : R → ℝ) (Iic a) a
Tactic: rw [ContinuousWithinAt.leftLim_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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
have 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∞)
Tactic: refine Measure.ext_of_Icc _ _ (fun a b h ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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
have inl : ∀ (ha : 𝓝[<] a = ⊥), leftLim (↑(f + g) : R → ℝ) a = leftLim (↑f : R → ℝ) a + leftLim (↑g : R → ℝ) a
Tactic: rcases Filter.eq_or_neBot (𝓝[<] a) with ha | ha
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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
⊢ leftLim (↑(f + g) : R → ℝ) a = leftLim (↑f : R → ℝ) a + leftLim (↑g : R → ℝ) a
have inr : ∀ (ha : (𝓝[<] a).NeBot), leftLim (↑(f + g) : R → ℝ) a = leftLim (↑f : R → ℝ) a + leftLim (↑g : R → ℝ) a
Tactic: rcases Filter.eq_or_neBot (𝓝[<] a) with ha | ha
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (hypothesis)
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
⊢ 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∞)
have this : 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))
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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
⊢ 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∞)
have 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)
Tactic: simp only [measure_Icc, add_apply, Measure.coe_add, Pi.add_apply, this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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) + ofReal ((↑g : R → ℝ) b - leftLim (↑g : R → ℝ) a)
have 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))
Tactic: rw [← ENNReal.ofReal_add (sub_nonneg_of_le (f.mono.leftLim_le h))
    (sub_nonneg_of_le (g.mono.leftLim_le h))]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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
have 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∞)
Tactic: refine Measure.ext_of_Icc _ _ (fun a b h ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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
⊢ 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∞)
have simp : ofReal ((↑(c • f) : R → ℝ) b - leftLim (↑(c • f) : R → ℝ) a) = c • ofReal ((↑f : R → ℝ) b - leftLim (↑f : R → ℝ) a)
Tactic: simp only [measure_Icc, Measure.smul_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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
have inl : ∀ (ha : 𝓝[<] a = ⊥), leftLim (↑(c • f) : R → ℝ) a = (↑c : ℝ) * leftLim (↑f : R → ℝ) a
Tactic: rcases Filter.eq_or_neBot (𝓝[<] a) with ha | ha
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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
⊢ leftLim (↑(c • f) : R → ℝ) a = (↑c : ℝ) * leftLim (↑f : R → ℝ) a
have inr : ∀ (ha : (𝓝[<] a).NeBot), leftLim (↑(c • f) : R → ℝ) a = (↑c : ℝ) * leftLim (↑f : R → ℝ) a
Tactic: rcases Filter.eq_or_neBot (𝓝[<] a) with ha | ha
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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 = ⊥
⊢ leftLim (↑(c • f) : R → ℝ) a = (↑c : ℝ) * leftLim (↑f : R → ℝ) a
have inl : (↑(c • f) : R → ℝ) a = (↑c : ℝ) * (↑f : R → ℝ) a
Tactic: simp [leftLim_eq_of_eq_bot _ ha]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (hypothesis)
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
⊢ ofReal ((↑c : ℝ) * (↑f : R → ℝ) b - leftLim (↑(c • f) : R → ℝ) a) =
    c • ofReal ((↑f : R → ℝ) b - leftLim (↑f : R → ℝ) a)
have this : 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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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
⊢ ofReal ((↑c : ℝ) * (↑f : R → ℝ) b - leftLim (↑(c • f) : R → ℝ) a) =
    c • ofReal ((↑f : R → ℝ) b - leftLim (↑f : R → ℝ) a)
have rw : (↑c : ℝ≥0∞) • ofReal ((↑f : R → ℝ) b - leftLim (↑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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Sub (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
⊢ sInf {d : Measure α | μ ≤ d + 0} = μ
have a : sInf {d : Measure α | μ ≤ d + 0} ≤ μ
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Sub (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
a : sInf {d : Measure α | μ ≤ d + 0} ≤ μ
⊢ sInf {d : Measure α | μ ≤ d + 0} = μ
have a₁ : μ ≤ sInf {d : Measure α | μ ≤ d + 0}
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Sub (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
g : ℕ → Set α
h_meas : ∀ (i : ℕ), MeasurableSet (g i)
h_disj : Pairwise (Function.onFun Disjoint g)
⊢ Eq (α := ENNReal)
    ((fun (t : Set α) (x : MeasurableSet t) ↦
        HSub.hSub (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)
          ((ν : (a : Set α) → ENNReal) t : ENNReal))
      (⋃ (i : ℕ), g i) ⋯)
    (∑' (i : ℕ),
      (fun (t : Set α) (x : MeasurableSet t) ↦
          HSub.hSub (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)
            ((ν : (a : Set α) → ENNReal) t : ENNReal))
        (g i) ⋯)
have simp : HSub.hSub (α := ENNReal) (∑' (i : ℕ), (μ : (a : Set α) → ENNReal) (g i))
    (∑' (i : ℕ), (ν : (a : Set α) → ENNReal) (g i)) =
  ∑' (i : ℕ),
    HSub.hSub (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) (g i) : ENNReal)
      ((ν : (a : Set α) → ENNReal) (g i) : ENNReal)
Tactic: simp only [measure_iUnion h_disj h_meas]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Sub (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
g : ℕ → Set α
h_meas : ∀ (i : ℕ), MeasurableSet (g i)
h_disj : Pairwise (Function.onFun Disjoint g)
⊢ HSub.hSub (α := ENNReal) (∑' (i : ℕ), (μ : (a : Set α) → ENNReal) (g i))
      (∑' (i : ℕ), (ν : (a : Set α) → ENNReal) (g i)) =
    ∑' (i : ℕ),
      HSub.hSub (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) (g i) : ENNReal)
        ((ν : (a : Set α) → ENNReal) (g i) : ENNReal)
have rw : Ne (α := ENNReal) (∑' (i : ℕ), (ν : (a : Set α) → ENNReal) (g i)) ⊤
Tactic: rw [ENNReal.tsum_sub _ (h₂ <| g ·)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Sub (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
g : ℕ → Set α
h_meas : ∀ (i : ℕ), MeasurableSet (g i)
h_disj : Pairwise (Function.onFun Disjoint g)
⊢ Ne (α := ENNReal) (∑' (i : ℕ), (ν : (a : Set α) → ENNReal) (g i)) ⊤
have rw : Ne (α := ENNReal) ((ν : (a : Set α) → ENNReal) (⋃ (i : ℕ), g i) : ENNReal) (⊤ : ENNReal)
Tactic: rw [← measure_iUnion h_disj h_meas]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Sub (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α :=
  ofMeasurable
    (fun (t : Set α) (x : MeasurableSet t) ↦
      HSub.hSub (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)
        ((ν : (a : Set α) → ENNReal) t : ENNReal))
    ⋯ ⋯
⊢ ν + measure_sub = μ
have h : ∀ (t : Set α) (h_t_measurable_set : MeasurableSet t),
  Eq (α := ENNReal) ((ν + measure_sub : (a : Set α) → ENNReal) t : ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)
Tactic: ext1 t h_t_measurable_set
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Sub (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α :=
  ofMeasurable
    (fun (t : Set α) (x : MeasurableSet t) ↦
      HSub.hSub (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)
        ((ν : (a : Set α) → ENNReal) t : ENNReal))
    ⋯ ⋯
t : Set α
h_t_measurable_set : MeasurableSet t
⊢ Eq (α := ENNReal) ((ν + measure_sub : (a : Set α) → ENNReal) t : ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)
have h : HAdd.hAdd (α := ENNReal) (β := ENNReal) ((ν : (a : Set α) → ENNReal) t : ENNReal)
    ((measure_sub : (a : Set α) → ENNReal) t : ENNReal) =
  (μ : (a : Set α) → ENNReal) t
Tactic: simp only [Pi.add_apply, coe_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Sub (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α :=
  ofMeasurable
    (fun (t : Set α) (x : MeasurableSet t) ↦
      HSub.hSub (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)
        ((ν : (a : Set α) → ENNReal) t : ENNReal))
    ⋯ ⋯
t : Set α
h_t_measurable_set : MeasurableSet t
⊢ HAdd.hAdd (α := ENNReal) (β := ENNReal) ((ν : (a : Set α) → ENNReal) t : ENNReal)
      ((measure_sub : (a : Set α) → ENNReal) t : ENNReal) =
    (μ : (a : Set α) → ENNReal) t
have h : HAdd.hAdd (α := ENNReal) ((ν : (a : Set α) → ENNReal) t : ENNReal)
    (HSub.hSub (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)
      ((ν : (a : Set α) → ENNReal) t : ENNReal)) =
  (μ : (a : Set α) → ENNReal) t
Tactic: rw [MeasureTheory.Measure.ofMeasurable_apply _ h_t_measurable_set, add_comm,
      tsub_add_cancel_of_le (h₂ t)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Sub (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α :=
  ofMeasurable
    (fun (t : Set α) (x : MeasurableSet t) ↦
      HSub.hSub (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)
        ((ν : (a : Set α) → ENNReal) t : ENNReal))
    ⋯ ⋯
t : Set α
h_t_measurable_set : MeasurableSet t
h :
  HAdd.hAdd (α := ENNReal) ((ν : (a : Set α) → ENNReal) t : ENNReal)
      (HSub.hSub (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)
        ((ν : (a : Set α) → ENNReal) t : ENNReal)) =
    (μ : (a : Set α) → ENNReal) t
⊢ HAdd.hAdd (α := ENNReal) (β := ENNReal) ((ν : (a : Set α) → ENNReal) t : ENNReal)
      ((measure_sub : (a : Set α) → ENNReal) t : ENNReal) =
    (μ : (a : Set α) → ENNReal) t
have h₃ : HAdd.hAdd (β := ENNReal)
    (HSub.hSub (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)
      ((ν : (a : Set α) → ENNReal) t : ENNReal))
    ((ν : (a : Set α) → ENNReal) t : ENNReal) =
  (μ : (a : Set α) → ENNReal) t
Tactic: rw [MeasureTheory.Measure.ofMeasurable_apply _ h_t_measurable_set, add_comm,
      tsub_add_cancel_of_le (h₂ t)]