awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
calc : proximity (f₁ * f₂) ⊤ = circleAverage (fun (x : ℂ) ↦ log⁺ (‖f₁ x‖ * ‖f₂ x‖)) 0
calc₁ :
  LE.le (α := (R : ℝ) → ℝ) (circleAverage (fun (x : ℂ) ↦ log⁺ (‖f₁ x‖ * ‖f₂ x‖)) 0)
    (circleAverage (fun (x : ℂ) ↦ log⁺ ‖f₁ x‖ + log⁺ ‖f₂ x‖) 0)
calc₂ :
  circleAverage (fun (x : ℂ) ↦ log⁺ ‖f₁ x‖ + log⁺ ‖f₂ x‖) 0 =
    HAdd.hAdd (α := (R : ℝ) → ℝ) (circleAverage (fun (x : ℂ) ↦ log⁺ ‖f₁ x‖) 0)
      (circleAverage (fun (x : ℂ) ↦ log⁺ ‖f₂ x‖) 0)
⊢ proximity (f₁ * f₂) ⊤ ≤ proximity f₁ ⊤ + proximity f₂ ⊤
have calc₃ : HAdd.hAdd (α := (R : ℝ) → ℝ) (circleAverage (fun (x : ℂ) ↦ log⁺ ‖f₁ x‖) 0)
    (circleAverage (fun (x : ℂ) ↦ log⁺ ‖f₂ x‖) 0) =
  proximity f₁ ⊤ + proximity f₂ ⊤
Tactic: calc proximity (f₁ * f₂) ⊤
    _ = circleAverage (fun x ↦ log⁺ (‖f₁ x‖ * ‖f₂ x‖)) 0 := by
      simp [proximity]
    _ ≤ circleAverage (fun x ↦ log⁺ ‖f₁ x‖ + log⁺ ‖f₂ x‖) 0 := by
      intro r
      apply circleAverage_mono
      · simp_rw [← norm_mul]
        apply MeromorphicOn.circleIntegrable_posLog_norm
        apply Meromorphic.meromorphicOn
        fun_prop
      · apply (MeromorphicOn.circleIntegrable_posLog_norm (fun x a ↦ h₁f₁ x)).add
          (MeromorphicOn.circleIntegrable_posLog_norm (fun x a ↦ h₁f₂ x))
      · exact fun _ _ ↦ posLog_mul
    _ = circleAverage (log⁺ ‖f₁ ·‖) 0 + circleAverage (log⁺ ‖f₂ ·‖) 0 := by
      ext r
      apply circleAverage_add
      · exact MeromorphicOn.circleIntegrable_posLog_norm (fun x a ↦ h₁f₁ x)
      · exact MeromorphicOn.circleIntegrable_posLog_norm (fun x a ↦ h₁f₂ x)
    _ = proximity f₁ ⊤ + proximity f₂ ⊤ := by simp [proximity]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
⊢ proximity (f₁ * f₂) 0 ≤ proximity f₁⁻¹ ⊤ + proximity f₂⁻¹ ⊤
have rw : proximity (f₁⁻¹ * f₂⁻¹) ⊤ ≤ proximity f₁⁻¹ ⊤ + proximity f₂⁻¹ ⊤
Tactic: rw [← proximity_inv, mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
⊢ proximity f₁⁻¹ ⊤ + proximity f₂⁻¹ ⊤ = proximity f₁ 0 + proximity f₂ 0
have rw : proximity f₁ 0 + proximity f₂⁻¹ ⊤ = proximity f₁ 0 + proximity f₂ 0
Tactic: rw [proximity_inv, proximity_inv]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
rw : proximity f₁ 0 + proximity f₂⁻¹ ⊤ = proximity f₁ 0 + proximity f₂ 0
⊢ proximity f₁⁻¹ ⊤ + proximity f₂⁻¹ ⊤ = proximity f₁ 0 + proximity f₂ 0
have rw₁ : proximity f₁ 0 + proximity f₂ 0 = proximity f₁ 0 + proximity f₂ 0
Tactic: rw [proximity_inv, proximity_inv]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
⊢ proximity (f₁ * f₂) 0 ≤ proximity f₁ 0 + proximity f₂ 0
have calc : proximity (f₁ * f₂) 0 ≤ proximity f₁⁻¹ ⊤ + proximity f₂⁻¹ ⊤
Tactic: calc proximity (f₁ * f₂) 0
    _ ≤ (proximity f₁⁻¹ ⊤) + (proximity f₂⁻¹ ⊤) := by
      rw [← proximity_inv, mul_inv]
      apply proximity_mul_top_le h₁f₁.inv h₁f₂.inv
    _ = (proximity f₁ 0) + (proximity f₂ 0) := by
      rw [proximity_inv, proximity_inv]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
calc : proximity (f₁ * f₂) 0 ≤ proximity f₁⁻¹ ⊤ + proximity f₂⁻¹ ⊤
⊢ proximity (f₁ * f₂) 0 ≤ proximity f₁ 0 + proximity f₂ 0
have calc₁ : proximity f₁⁻¹ ⊤ + proximity f₂⁻¹ ⊤ = proximity f₁ 0 + proximity f₂ 0
Tactic: calc proximity (f₁ * f₂) 0
    _ ≤ (proximity f₁⁻¹ ⊤) + (proximity f₂⁻¹ ⊤) := by
      rw [← proximity_inv, mul_inv]
      apply proximity_mul_top_le h₁f₁.inv h₁f₂.inv
    _ = (proximity f₁ 0) + (proximity f₂ 0) := by
      rw [proximity_inv, proximity_inv]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
f : ℂ → ℂ
n : ℕ
⊢ proximity (f ^ n) ⊤ = n • proximity f ⊤
have h : ∀ (x : ℝ), proximity (f ^ n) ⊤ x = (n • proximity f ⊤) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
f : ℂ → ℂ
n : ℕ
⊢ proximity (f ^ n) 0 = n • proximity f 0
have rw : proximity (f ^ n)⁻¹ ⊤ = n • proximity f 0
Tactic: rw [← proximity_inv, ← proximity_inv, ← inv_pow, proximity_pow_top]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
f : ℂ → ℂ
n : ℕ
rw : proximity (f ^ n)⁻¹ ⊤ = n • proximity f 0
⊢ proximity (f ^ n) 0 = n • proximity f 0
have rw₁ : proximity (f ^ n)⁻¹ ⊤ = n • proximity f⁻¹ ⊤
Tactic: rw [← proximity_inv, ← proximity_inv, ← inv_pow, proximity_pow_top]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
f : ℂ → ℂ
n : ℕ
rw : proximity (f ^ n)⁻¹ ⊤ = n • proximity f 0
rw₁ : proximity (f ^ n)⁻¹ ⊤ = n • proximity f⁻¹ ⊤
⊢ proximity (f ^ n) 0 = n • proximity f 0
have rw₂ : proximity (f⁻¹ ^ n) ⊤ = n • proximity f⁻¹ ⊤
Tactic: rw [← proximity_inv, ← proximity_inv, ← inv_pow, proximity_pow_top]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
f : ℂ → ℂ
n : ℕ
rw : proximity (f ^ n)⁻¹ ⊤ = n • proximity f 0
rw₁ : proximity (f ^ n)⁻¹ ⊤ = n • proximity f⁻¹ ⊤
rw₂ : proximity (f⁻¹ ^ n) ⊤ = n • proximity f⁻¹ ⊤
⊢ proximity (f ^ n) 0 = n • proximity f 0
have rw₃ : n • proximity f⁻¹ ⊤ = n • proximity f⁻¹ ⊤
Tactic: rw [← proximity_inv, ← proximity_inv, ← inv_pow, proximity_pow_top]
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
hs : s.Subsingleton
l : ℝ≥0
x : ℝ
hx : x ∈ s
y : ℝ
hy : y ∈ s
⊢ eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
have refl : ∀ (hy : x ∈ s), eVariationOn f (s ∩ Icc x x) = ENNReal.ofReal ((↑l : ℝ) * (x - x))
Tactic: cases hs hx hy
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
hs : s.Subsingleton
l : ℝ≥0
x : ℝ
hx hy : x ∈ s
⊢ eVariationOn f (s ∩ Icc x x) = ENNReal.ofReal ((↑l : ℝ) * (x - x))
have refl : 0 = ENNReal.ofReal ((↑l : ℝ) * (x - x))
Tactic: rw [eVariationOn.subsingleton f (fun y hy z hz => hs hy.1 hz.1 : (s ∩ Icc x x).Subsingleton)]
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
⊢ HasConstantSpeedOnWith f s l ↔
    ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
have refine : ∀ (h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x)))
  (x : ℝ) (xs : x ∈ s) (y : ℝ) (ys : y ∈ s), eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
Tactic: refine ⟨fun h x xs y ys _ => h xs ys, fun h x xs y ys => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
⊢ eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
have inl : ∀ (xy : x ≤ y), eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
Tactic: rcases le_total x y with (xy | yx)
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
inl : ∀ (xy : x ≤ y), eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
⊢ eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
have inr : ∀ (yx : y ≤ x), eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
Tactic: rcases le_total x y with (xy | yx)
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
yx : y ≤ x
⊢ eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
have inr : (↑l : ℝ) * (y - x) ≤ 0
Tactic: rw [eVariationOn.subsingleton, ENNReal.ofReal_of_nonpos]
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
yx : y ≤ x
inr : (↑l : ℝ) * (y - x) ≤ 0
⊢ eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
have inr₁ : (s ∩ Icc x y).Subsingleton
Tactic: rw [eVariationOn.subsingleton, ENNReal.ofReal_of_nonpos]
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
yx : y ≤ x
z : ℝ
zs : z ∈ s
xz : x ≤ z
zy : z ≤ y
w : ℝ
ws : w ∈ s
xw : x ≤ w
wy : w ≤ y
⊢ z = w
have inr : ∀ (zs : x ∈ s) (xz : x ≤ x) (zy : x ≤ y), x = w
Tactic: cases le_antisymm (zy.trans yx) xz
Cleared hypotheses: z, zs, xz, zy
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
yx : y ≤ x
w : ℝ
ws : w ∈ s
xw : x ≤ w
wy : w ≤ y
zs : x ∈ s
xz : x ≤ x
zy : x ≤ y
⊢ x = w
have inr : ∀ (ws : x ∈ s) (xw : x ≤ x) (wy : x ≤ y), x = x
Tactic: cases le_antisymm (wy.trans yx) xw
Cleared hypotheses: w, ws, xw, wy
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
⊢ HasConstantSpeedOnWith f s l ↔
    LocallyBoundedVariationOn f s ∧ ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → variationOnFromTo f s x y = (↑l : ℝ) * (y - x)
have mp : HasConstantSpeedOnWith f s l →
  LocallyBoundedVariationOn f s ∧ ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → variationOnFromTo f s x y = (↑l : ℝ) * (y - x)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
mp :
  HasConstantSpeedOnWith f s l →
    LocallyBoundedVariationOn f s ∧ ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → variationOnFromTo f s x y = (↑l : ℝ) * (y - x)
⊢ HasConstantSpeedOnWith f s l ↔
    LocallyBoundedVariationOn f s ∧ ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → variationOnFromTo f s x y = (↑l : ℝ) * (y - x)
have mpr : (LocallyBoundedVariationOn f s ∧ ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → variationOnFromTo f s x y = (↑l : ℝ) * (y - x)) →
  HasConstantSpeedOnWith f s l
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : HasConstantSpeedOnWith f s l
⊢ LocallyBoundedVariationOn f s ∧ ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → variationOnFromTo f s x y = (↑l : ℝ) * (y - x)
have mp : ∀ (x : ℝ) (xs : x ∈ s) (y : ℝ) (ys : y ∈ s), variationOnFromTo f s x y = (↑l : ℝ) * (y - x)
Tactic: refine ⟨h.hasLocallyBoundedVariationOn, fun x xs y ys => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : HasConstantSpeedOnWith f s l
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
⊢ variationOnFromTo f s x y = (↑l : ℝ) * (y - x)
have mp : ∀ (h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x)))
  (x : ℝ) (xs : x ∈ s) (y : ℝ) (ys : y ∈ s), variationOnFromTo f s x y = (↑l : ℝ) * (y - x)
Tactic: rw [hasConstantSpeedOnWith_iff_ordered] at h
Cleared hypotheses: h, x, xs, y, ys
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
⊢ variationOnFromTo f s x y = (↑l : ℝ) * (y - x)
have mp : ∀ (xy : x ≤ y), variationOnFromTo f s x y = (↑l : ℝ) * (y - x)
Tactic: rcases le_total x y with (xy | yx)
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
mp : ∀ (xy : x ≤ y), variationOnFromTo f s x y = (↑l : ℝ) * (y - x)
⊢ variationOnFromTo f s x y = (↑l : ℝ) * (y - x)
have mp₁ : ∀ (yx : y ≤ x), variationOnFromTo f s x y = (↑l : ℝ) * (y - x)
Tactic: rcases le_total x y with (xy | yx)
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
xy : x ≤ y
⊢ variationOnFromTo f s x y = (↑l : ℝ) * (y - x)
have mp : (ENNReal.ofReal ((↑l : ℝ) * (y - x))).toReal = (↑l : ℝ) * (y - x)
Tactic: rw [variationOnFromTo.eq_of_le f s xy, h xs ys xy]
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
yx : y ≤ x
⊢ variationOnFromTo f s x y = (↑l : ℝ) * (y - x)
have mp : -(ENNReal.ofReal ((↑l : ℝ) * (x - y))).toReal = (↑l : ℝ) * (y - x)
Tactic: rw [variationOnFromTo.eq_of_ge f s yx, h ys xs yx]
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (hypothesis)
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
yx : y ≤ x
⊢ -(ENNReal.ofReal ((↑l : ℝ) * (x - y))).toReal = (↑l : ℝ) * (y - x)
have this : (ENNReal.ofReal ((↑l : ℝ) * (x - y))).toReal = (↑l : ℝ) * (x - y)
Tactic: have := ENNReal.toReal_ofReal (mul_nonneg l.prop (sub_nonneg.mpr yx))
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
yx : y ≤ x
this : (ENNReal.ofReal ((↑l : ℝ) * (x - y))).toReal = (↑l : ℝ) * (x - y)
⊢ -(ENNReal.ofReal ((↑l : ℝ) * (x - y))).toReal = (↑l : ℝ) * (y - x)
have mp : ∀ (this : (ENNReal.ofReal ((↑l : ℝ) * (x - y))).toReal = (↑l : ℝ) * (x - y)), -((↑l : ℝ) * (x - y)) = (↑l : ℝ) * (y - x)
Tactic: simp_all only [NNReal.val_eq_coe]
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
⊢ (LocallyBoundedVariationOn f s ∧
      ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → variationOnFromTo f s x y = (↑l : ℝ) * (y - x)) →
    HasConstantSpeedOnWith f s l
have mpr : (LocallyBoundedVariationOn f s ∧ ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → variationOnFromTo f s x y = (↑l : ℝ) * (y - x)) →
  ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
Tactic: rw [hasConstantSpeedOnWith_iff_ordered]
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : LocallyBoundedVariationOn f s ∧ ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → variationOnFromTo f s x y = (↑l : ℝ) * (y - x)
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
xy : x ≤ y
⊢ eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
have mpr : eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (variationOnFromTo f s x y)
Tactic: rw [← h.2 xs ys, variationOnFromTo.eq_of_le f s xy, ENNReal.ofReal_toReal (h.1 x y xs ys)]
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : LocallyBoundedVariationOn f s ∧ ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → variationOnFromTo f s x y = (↑l : ℝ) * (y - x)
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
xy : x ≤ y
mpr : eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (variationOnFromTo f s x y)
⊢ eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
have mpr₁ : eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (eVariationOn f (s ∩ Icc x y)).toReal
Tactic: rw [← h.2 xs ys, variationOnFromTo.eq_of_le f s xy, ENNReal.ofReal_toReal (h.1 x y xs ys)]
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : LocallyBoundedVariationOn f s ∧ ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → variationOnFromTo f s x y = (↑l : ℝ) * (y - x)
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
xy : x ≤ y
mpr : eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (variationOnFromTo f s x y)
mpr₁ : eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (eVariationOn f (s ∩ Icc x y)).toReal
⊢ eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
have mpr₂ : eVariationOn f (s ∩ Icc x y) = eVariationOn f (s ∩ Icc x y)
Tactic: rw [← h.2 xs ys, variationOnFromTo.eq_of_le f s xy, ENNReal.ofReal_toReal (h.1 x y xs ys)]
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : HasConstantSpeedOnWith f s l
hft : HasConstantSpeedOnWith f t l
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
⊢ HasConstantSpeedOnWith f (s ∪ t) l
have rw : ∀
  (hfs :
    ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x)))
  (hft :
    ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x)))
  {x : ℝ} (hs : IsGreatest s x) (ht : IsLeast t x) ⦃x : ℝ⦄,
  x ∈ s ∪ t → ∀ ⦃y : ℝ⦄, y ∈ s ∪ t → x ≤ y → eVariationOn f ((s ∪ t) ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
Tactic: rw [hasConstantSpeedOnWith_iff_ordered] at hfs hft ⊢
Cleared hypotheses: hfs, hft, x, hs, ht
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zs : z ∈ s
y : ℝ
ys : y ∈ s
zy : z ≤ y
⊢ (s ∪ t) ∩ Icc z y = s ∩ Icc z y
have h : ∀ (w : ℝ), w ∈ (s ∪ t) ∩ Icc z y ↔ w ∈ s ∩ Icc z y
Tactic: ext w
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zs : z ∈ s
y : ℝ
ys : y ∈ s
zy : z ≤ y
w : ℝ
⊢ w ∈ (s ∪ t) ∩ Icc z y ↔ w ∈ s ∩ Icc z y
have h : w ∈ (s ∪ t) ∩ Icc z y → w ∈ s ∩ Icc z y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zs : z ∈ s
y : ℝ
ys : y ∈ s
zy : z ≤ y
w : ℝ
h : w ∈ (s ∪ t) ∩ Icc z y → w ∈ s ∩ Icc z y
⊢ w ∈ (s ∪ t) ∩ Icc z y ↔ w ∈ s ∩ Icc z y
have h₁ : w ∈ s ∩ Icc z y → w ∈ (s ∪ t) ∩ Icc z y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (hypothesis)
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zs : z ∈ s
y : ℝ
ys : y ∈ s
zy : z ≤ y
⊢ eVariationOn f ((s ∪ t) ∩ Icc z y) = ENNReal.ofReal ((↑l : ℝ) * (y - z))
have this : (s ∪ t) ∩ Icc z y = s ∩ Icc z y
Tactic: have : (s ∪ t) ∩ Icc z y = s ∩ Icc z y := by
      ext w; constructor
      · rintro ⟨ws | wt, zw, wy⟩
        · exact ⟨ws, zw, wy⟩
        · exact ⟨(le_antisymm (wy.trans (hs.2 ys)) (ht.2 wt)).symm ▸ hs.1, zw, wy⟩
      · rintro ⟨ws, zwy⟩; exact ⟨Or.inl ws, zwy⟩
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zs : z ∈ s
y : ℝ
ys : y ∈ s
zy : z ≤ y
this : (s ∪ t) ∩ Icc z y = s ∩ Icc z y
⊢ eVariationOn f ((s ∪ t) ∩ Icc z y) = ENNReal.ofReal ((↑l : ℝ) * (y - z))
have inl : eVariationOn f (s ∩ Icc z y) = ENNReal.ofReal ((↑l : ℝ) * (y - z))
Tactic: rw [this, hfs zs ys zy]
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zs : z ∈ s
y : ℝ
ys : y ∈ s
zy : z ≤ y
this : (s ∪ t) ∩ Icc z y = s ∩ Icc z y
inl : eVariationOn f (s ∩ Icc z y) = ENNReal.ofReal ((↑l : ℝ) * (y - z))
⊢ eVariationOn f ((s ∪ t) ∩ Icc z y) = ENNReal.ofReal ((↑l : ℝ) * (y - z))
have inl₁ : ENNReal.ofReal ((↑l : ℝ) * (y - z)) = ENNReal.ofReal ((↑l : ℝ) * (y - z))
Tactic: rw [this, hfs zs ys zy]
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zs : z ∈ s
y : ℝ
yt : y ∈ t
zy : z ≤ y
⊢ (s ∪ t) ∩ Icc z y = s ∩ Icc z x ∪ t ∩ Icc x y
have h : ∀ (w : ℝ), w ∈ (s ∪ t) ∩ Icc z y ↔ w ∈ s ∩ Icc z x ∪ t ∩ Icc x y
Tactic: ext w
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zs : z ∈ s
y : ℝ
yt : y ∈ t
zy : z ≤ y
w : ℝ
⊢ w ∈ (s ∪ t) ∩ Icc z y ↔ w ∈ s ∩ Icc z x ∪ t ∩ Icc x y
have h : w ∈ (s ∪ t) ∩ Icc z y → w ∈ s ∩ Icc z x ∪ t ∩ Icc x y
Tactic: constructor