awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
s : Finset.range (b - a)
| ∑ x ∈ Finset.range (b - a), f (↑(a + x + 1) : ℝ)
have f₁ : fun (x : ℕ) ↦ f (↑(a + x + 1) : ℝ)
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
| Finset.range (b - a)
have s : b - a
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
| fun (x : ℕ) ↦ f (↑(a + x + 1) : ℝ)
have f₁ : ∀ (x : ℕ), f (↑(a + x + 1) : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
x : ℕ
| f (↑(a + x + 1) : ℝ)
have f₁ : f (HAdd.hAdd (α := ℝ) (↑a : ℝ) (↑(x + 1) : ℝ))
Tactic: rw [add_assoc, Nat.cast_add]
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
| LE.le (α := ℝ) (∑ x ∈ Finset.range (b - a), f (↑(a + x + 1) : ℝ))
    (∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑a : ℝ) (↑(b - a) : ℝ), f x)
have f₁ : ∀ (x : ℕ), f (HAdd.hAdd (α := ℝ) (↑a : ℝ) (↑(x + 1) : ℝ))
Tactic: lhs
    congr
    congr
    · skip
    ext
    rw [add_assoc, Nat.cast_add]
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
⊢ LE.le (α := ℝ) (∑ x ∈ Finset.range (b - a), f (↑(a + x + 1) : ℝ))
    (∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑a : ℝ) (↑(b - a) : ℝ), f x)
have conv : LE.le (α := ℝ) (∑ x ∈ Finset.range (b - a), f (HAdd.hAdd (α := ℝ) (↑a : ℝ) (↑(x + 1) : ℝ)))
  (∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑a : ℝ) (↑(b - a) : ℝ), f x)
Tactic: conv =>
    lhs
    congr
    congr
    · skip
    ext
    rw [add_assoc, Nat.cast_add]
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
⊢ LE.le (α := ℝ) (∑ x ∈ Finset.range (b - a), f (HAdd.hAdd (α := ℝ) (↑a : ℝ) (↑(x + 1) : ℝ)))
    (∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑a : ℝ) (↑(b - a) : ℝ), f x)
have hf₁ : AntitoneOn f (Icc (↑a : ℝ) (HAdd.hAdd (α := ℝ) (↑a : ℝ) (↑(b - a) : ℝ)))
Tactic: apply AntitoneOn.sum_le_integral
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : MonotoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
⊢ LE.le (α := ℝ) (∑ i ∈ Finset.range a, f (x₀ + (↑i : ℝ))) (∫ (x : ℝ) in x₀..x₀ + (↑a : ℝ), f x)
have rw : LE.le (α := ℝ) (∫ (x : ℝ) in x₀..x₀ + (↑a : ℝ), -f x) (∑ x ∈ Finset.range a, -f (x₀ + (↑x : ℝ)))
Tactic: rw [← neg_le_neg_iff, ← Finset.sum_neg_distrib, ← intervalIntegral.integral_neg]
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
⊢ LE.le (α := ℝ) (∑ x ∈ Finset.Ico a b, f (↑x : ℝ)) (∫ (x : ℝ) in (↑a : ℝ)..(↑b : ℝ), f x)
have rw : LE.le (α := ℝ) (∫ (x : ℝ) in (↑a : ℝ)..(↑b : ℝ), -f x) (∑ x ∈ Finset.Ico a b, -f (↑x : ℝ))
Tactic: rw [← neg_le_neg_iff, ← Finset.sum_neg_distrib, ← intervalIntegral.integral_neg]
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : MonotoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in x₀..x₀ + (↑a : ℝ), f x) (∑ i ∈ Finset.range a, f (x₀ + (↑(i + 1) : ℝ)))
have rw : LE.le (α := ℝ) (∑ x ∈ Finset.range a, -f (x₀ + (↑(x + 1) : ℝ))) (∫ (x : ℝ) in x₀..x₀ + (↑a : ℝ), -f x)
Tactic: rw [← neg_le_neg_iff, ← Finset.sum_neg_distrib, ← intervalIntegral.integral_neg]
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in (↑a : ℝ)..(↑b : ℝ), f x) (∑ i ∈ Finset.Ico a b, f (↑(i + 1) : ℝ))
have rw : LE.le (α := ℝ) (∑ x ∈ Finset.Ico a b, -f (↑(x + 1) : ℝ)) (∫ (x : ℝ) in (↑a : ℝ)..(↑b : ℝ), -f x)
Tactic: rw [← neg_le_neg_iff, ← Finset.sum_neg_distrib, ← intervalIntegral.integral_neg]
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
⊢ LE.le (α := ℝ) (∑ i ∈ Finset.Ico a b, f (↑i : ℝ) * g (↑i : ℝ)) (∫ (x : ℝ) in (↑a : ℝ)..(↑b : ℝ), f x * g (x - 1))
have h : ∀ i ∈ Ico a b,
  ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Ico (↑i : ℝ) (↑(i + 1) : ℝ)) x → f (↑i : ℝ) * g (↑i : ℝ) ≤ f x * g (x - 1)
Tactic: apply sum_Ico_le_integral_of_le (f := fun x ↦ f x * g x) hab
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
h :
  ∀ i ∈ Ico a b,
    ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Ico (↑i : ℝ) (↑(i + 1) : ℝ)) x → f (↑i : ℝ) * g (↑i : ℝ) ≤ f x * g (x - 1)
⊢ LE.le (α := ℝ) (∑ i ∈ Finset.Ico a b, f (↑i : ℝ) * g (↑i : ℝ)) (∫ (x : ℝ) in (↑a : ℝ)..(↑b : ℝ), f x * g (x - 1))
have hg₁ : IntegrableOn (ε := ℝ) (mα := toMeasurableSpace) (fun (x : ℝ) ↦ f x * g (x - 1)) (Ico (↑a : ℝ) (↑b : ℝ)) volume
Tactic: apply sum_Ico_le_integral_of_le (f := fun x ↦ f x * g x) hab
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (hypothesis)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
hi : i ∈ Ico a b
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ico (↑i : ℝ) (↑(i + 1) : ℝ)) x
⊢ f (↑i : ℝ) * g (↑i : ℝ) ≤ f x * g (x - 1)
have hx₁ : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
Tactic: simp only [Nat.cast_add, Nat.cast_one, mem_Ico] at hx hi
Cleared hypotheses: hi, hx
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (hypothesis)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
hi : i ∈ Ico a b
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ico (↑i : ℝ) (↑(i + 1) : ℝ)) x
hx₁ : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
⊢ f (↑i : ℝ) * g (↑i : ℝ) ≤ f x * g (x - 1)
have hi₁ : a ≤ i ∧ i < b
Tactic: simp only [Nat.cast_add, Nat.cast_one, mem_Ico] at hx hi
Cleared hypotheses: hi, hx
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
⊢ (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
have simp : HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 ≤ (↑b : ℝ)
Tactic: simp only [le_sub_iff_add_le]
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
⊢ HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 ≤ (↑b : ℝ)
have norm_cast : i + 1 ≤ b
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (hypothesis)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
⊢ f (↑i : ℝ) * g (↑i : ℝ) ≤ f x * g (x - 1)
have I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
Tactic: have I0 : (i : ℝ) ≤ b - 1 := by
      simp only [le_sub_iff_add_le]
      norm_cast
      lia
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
⊢ (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
have simp : (↑a : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 ∧ (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
Tactic: simp only [mem_Icc, tsub_le_iff_right]
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
⊢ (↑a : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
have norm_cast : a ≤ i + 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (hypothesis)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
⊢ f (↑i : ℝ) * g (↑i : ℝ) ≤ f x * g (x - 1)
have I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
Tactic: have I1 : (i : ℝ) ∈ Icc (a - 1 : ℝ) (b - 1) := by
      simp only [mem_Icc, tsub_le_iff_right]
      exact ⟨by norm_cast; lia, I0⟩
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
⊢ Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
have refine : HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 ≤ (↑b : ℝ)
Tactic: refine ⟨le_trans (mod_cast hi.1) hx.1, hx.2.le.trans ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
⊢ HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 ≤ (↑b : ℝ)
have norm_cast : i + 1 ≤ b
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (hypothesis)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
⊢ f (↑i : ℝ) * g (↑i : ℝ) ≤ f x * g (x - 1)
have I2 : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
Tactic: have I2 : x ∈ Icc (a : ℝ) b := by
      refine ⟨le_trans (mod_cast hi.1) hx.1, hx.2.le.trans ?_⟩
      norm_cast
      lia
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
I2 : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
⊢ f (↑i : ℝ) * g (↑i : ℝ) ≤ f x * g (x - 1)
have h : f (↑i : ℝ) ≤ f x
Tactic: apply mul_le_mul
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
I2 : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
h : f (↑i : ℝ) ≤ f x
⊢ f (↑i : ℝ) * g (↑i : ℝ) ≤ f x * g (x - 1)
have h₁ : g (↑i : ℝ) ≤ g (x - 1)
Tactic: apply mul_le_mul
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
I2 : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
h : f (↑i : ℝ) ≤ f x
h₁ : g (↑i : ℝ) ≤ g (x - 1)
⊢ f (↑i : ℝ) * g (↑i : ℝ) ≤ f x * g (x - 1)
have h₂ : 0 ≤ g (↑i : ℝ)
Tactic: apply mul_le_mul
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
I2 : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
h : f (↑i : ℝ) ≤ f x
h₁ : g (↑i : ℝ) ≤ g (x - 1)
h₂ : 0 ≤ g (↑i : ℝ)
⊢ f (↑i : ℝ) * g (↑i : ℝ) ≤ f x * g (x - 1)
have h₃ : 0 ≤ f x
Tactic: apply mul_le_mul
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
I2 : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
⊢ f (↑i : ℝ) ≤ f x
have h : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) (↑i : ℝ)
Tactic: apply hf
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
I2 : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
h : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) (↑i : ℝ)
h₁ : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
⊢ f (↑i : ℝ) ≤ f x
have h₂ : (↑i : ℝ) ≤ x
Tactic: apply hf
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
I2 : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
⊢ Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) (↑i : ℝ)
have h : a ≤ i ∧ i ≤ b
Tactic: simp only [mem_Icc, Nat.cast_le]
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
I2 : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
⊢ g (↑i : ℝ) ≤ g (x - 1)
have h : x - 1 ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
Tactic: apply hg
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
I2 : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
h : x - 1 ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
h₁ : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
⊢ g (↑i : ℝ) ≤ g (x - 1)
have h₂ : x - 1 ≤ (↑i : ℝ)
Tactic: apply hg
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
I2 : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
⊢ x - 1 ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
have h : (↑a : ℝ) ≤ x ∧ x ≤ (↑b : ℝ)
Tactic: simp only [mem_Icc, tsub_le_iff_right, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
I2 : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
⊢ (↑a : ℝ) ≤ x ∧ x ≤ (↑b : ℝ)
have h : HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 ≤ (↑b : ℝ)
Tactic: refine ⟨le_trans (mod_cast hi.1) hx.1, hx.2.le.trans ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
I2 : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
⊢ HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 ≤ (↑b : ℝ)
have h : i + 1 ≤ b
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
I2 : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
⊢ 0 ≤ g (↑i : ℝ)
have h : g (HSub.hSub (α := ℝ) (↑b : ℝ) 1) ≤ g (↑i : ℝ)
Tactic: apply gpos.trans
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
I2 : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
⊢ 0 ≤ f x
have h : f (↑a : ℝ) ≤ f x
Tactic: apply fpos.trans
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
I2 : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
⊢ f (↑a : ℝ) ≤ f x
have h : (↑a : ℝ) ≤ x
Tactic: apply hf (by simp [hab]) I2
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
⊢ IntegrableOn (ε := ℝ) (mα := toMeasurableSpace) (fun (x : ℝ) ↦ f x * g (x - 1)) (Ico (↑a : ℝ) (↑b : ℝ)) volume
have apply : @Integrable ℝ _ _ _ toMeasurableSpace (fun (x : ℝ) ↦ f x * g (x - 1)) (Measure.restrict volume (Icc (↑a : ℝ) (↑b : ℝ)))
Tactic: apply Integrable.mono_measure _ (Measure.restrict_mono_set _ Ico_subset_Icc_self)
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
⊢ @Integrable ℝ _ _ _ toMeasurableSpace (fun (x : ℝ) ↦ f x * g (x - 1))
    (Measure.restrict volume (Icc (↑a : ℝ) (↑b : ℝ)))
have hφ : @Integrable _ _ _ _ toMeasurableSpace f (Measure.restrict volume (Icc (↑a : ℝ) (↑b : ℝ)))
Tactic: apply Integrable.mul_of_top_left