awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Subadditive (goal)
Goal:
u : ℕ → ℝ
h : Subadditive u
L : ℝ
n : ℕ
hn : n ≠ 0
hL : u n / (↑n : ℝ) < L
r : ℕ
h_1 : r < n
A :
  Tendsto (fun (x : ℝ) ↦ (u n + u r / x) / ((↑n : ℝ) + (↑r : ℝ) / x)) atTop
    (𝓝 ((u n + 0) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 0))
B : Tendsto (fun (x : ℝ) ↦ (x * u n + u r) / (x * (↑n : ℝ) + (↑r : ℝ))) atTop (𝓝 (u n / (↑n : ℝ)))
k : ℕ
hk : ((fun (x : ℝ) ↦ (x * u n + u r) / (x * (↑n : ℝ) + (↑r : ℝ))) ∘ Nat.cast) k < L
⊢ u (k * n + r) / (↑(k * n + r) : ℝ) ≤ ((fun (x : ℝ) ↦ (x * u n + u r) / (x * (↑n : ℝ) + (↑r : ℝ))) ∘ Nat.cast) k
have simp : u (k * n + r) / (↑(k * n + r) : ℝ) ≤ ((↑k : ℝ) * u n + u r) / (↑(k * n + r) : ℝ)
Tactic: simp only [(· ∘ ·), ← Nat.cast_add, ← Nat.cast_mul]
-- Lean 4 proof step from Mathlib.Analysis.Subadditive (goal)
Goal:
u : ℕ → ℝ
h : Subadditive u
L : ℝ
n : ℕ
hn : n ≠ 0
hL : u n / (↑n : ℝ) < L
r : ℕ
h_1 : r < n
A :
  Tendsto (fun (x : ℝ) ↦ (u n + u r / x) / ((↑n : ℝ) + (↑r : ℝ) / x)) atTop
    (𝓝 ((u n + 0) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 0))
B : Tendsto (fun (x : ℝ) ↦ (x * u n + u r) / (x * (↑n : ℝ) + (↑r : ℝ))) atTop (𝓝 (u n / (↑n : ℝ)))
k : ℕ
hk : ((fun (x : ℝ) ↦ (x * u n + u r) / (x * (↑n : ℝ) + (↑r : ℝ))) ∘ Nat.cast) k < L
⊢ u (k * n + r) / (↑(k * n + r) : ℝ) ≤ ((↑k : ℝ) * u n + u r) / (↑(k * n + r) : ℝ)
have hab : u (k * n + r) ≤ (↑k : ℝ) * u n + u r
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Subadditive (goal)
Goal:
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (α := ℝ) (range fun (n : ℕ) ↦ u n / (↑n : ℝ))
⊢ Tendsto (fun (n : ℕ) ↦ u n / (↑n : ℝ)) atTop (𝓝 h.lim)
have refine_1 : ∀ (l : ℝ) (hl : l < h.lim), ∀ᶠ (b : ℕ) in atTop, l < u b / (↑b : ℝ)
Tactic: refine tendsto_order.2 ⟨fun l hl => ?_, fun L hL => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Subadditive (goal)
Goal:
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (α := ℝ) (range fun (n : ℕ) ↦ u n / (↑n : ℝ))
refine_1 : ∀ (l : ℝ) (hl : l < h.lim), ∀ᶠ (b : ℕ) in atTop, l < u b / (↑b : ℝ)
⊢ Tendsto (fun (n : ℕ) ↦ u n / (↑n : ℝ)) atTop (𝓝 h.lim)
have refine_2 : ∀ (L : ℝ) (hL : L > h.lim), ∀ᶠ (b : ℕ) in atTop, u b / (↑b : ℝ) < L
Tactic: refine tendsto_order.2 ⟨fun l hl => ?_, fun L hL => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Subadditive (hypothesis)
Goal:
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (α := ℝ) (range fun (n : ℕ) ↦ u n / (↑n : ℝ))
L : ℝ
hL : L > h.lim
⊢ ∃ (n : ℕ), 0 < n ∧ u n / (↑n : ℝ) < L
have hL₁ : L > sInf ((fun (n : ℕ) ↦ u n / (↑n : ℝ)) '' Ici 1)
Tactic: rw [Subadditive.lim] at hL
Cleared hypotheses: hL
-- Lean 4 proof step from Mathlib.Analysis.Subadditive (goal)
Goal:
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (α := ℝ) (range fun (n : ℕ) ↦ u n / (↑n : ℝ))
L : ℝ
hL : L > sInf ((fun (n : ℕ) ↦ u n / (↑n : ℝ)) '' Ici 1)
⊢ ∃ (n : ℕ), 0 < n ∧ u n / (↑n : ℝ) < L
have rcases : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) ((fun (n : ℕ) ↦ u n / (↑n : ℝ)) '' Ici 1) x) (xL : x < L),
  ∃ (n : ℕ), 0 < n ∧ u n / (↑n : ℝ) < L
Tactic: rcases exists_lt_of_csInf_lt (by simp) hL with ⟨x, hx, xL⟩
-- Lean 4 proof step from Mathlib.Analysis.Subadditive (goal)
Goal:
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (α := ℝ) (range fun (n : ℕ) ↦ u n / (↑n : ℝ))
L : ℝ
hL : L > sInf ((fun (n : ℕ) ↦ u n / (↑n : ℝ)) '' Ici 1)
x : ℝ
hx : Membership.mem (γ := Set ℝ) ((fun (n : ℕ) ↦ u n / (↑n : ℝ)) '' Ici 1) x
xL : x < L
⊢ ∃ (n : ℕ), 0 < n ∧ u n / (↑n : ℝ) < L
have rcases : ∀ (n : ℕ) (hn : Membership.mem (γ := Set ℕ) (Ici 1) n)
  (hx : Membership.mem (γ := Set ℝ) ((fun (n : ℕ) ↦ u n / (↑n : ℝ)) '' Ici 1) (u n / (↑n : ℝ)))
  (xL : u n / (↑n : ℝ) < L), ∃ (n : ℕ), 0 < n ∧ u n / (↑n : ℝ) < L
Tactic: rcases (mem_image _ _ _).1 hx with ⟨n, hn, rfl⟩
Cleared hypotheses: x, hx, xL
-- Lean 4 proof step from Mathlib.Analysis.Subadditive (goal)
Goal:
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (α := ℝ) (range fun (n : ℕ) ↦ u n / (↑n : ℝ))
L : ℝ
hL : L > h.lim
⊢ ∀ᶠ (b : ℕ) in atTop, u b / (↑b : ℝ) < L
have refine_2 : ∀ (n : ℕ) (npos : 0 < n) (hn : u n / (↑n : ℝ) < L), ∀ᶠ (b : ℕ) in atTop, u b / (↑b : ℝ) < L
Tactic: obtain ⟨n, npos, hn⟩ : ∃ n : ℕ, 0 < n ∧ u n / n < L := by
      rw [Subadditive.lim] at hL
      rcases exists_lt_of_csInf_lt (by simp) hL with ⟨x, hx, xL⟩
      rcases (mem_image _ _ _).1 hx with ⟨n, hn, rfl⟩
      exact ⟨n, zero_lt_one.trans_le hn, xL⟩
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
h : ∀ i ∈ Ico a b, ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Ico (↑i : ℝ) (↑(i + 1) : ℝ)) x → f (↑i : ℝ) ≤ g x
hg : IntegrableOn (mα := toMeasurableSpace) g (Ico (↑a : ℝ) (↑b : ℝ)) volume
i : ℕ
hi : i ∈ Finset.Ico a b
⊢ IntervalIntegrable g volume (↑i : ℝ) (↑(i + 1) : ℝ)
have rw : IntegrableOn (mα := Real.measurableSpace) g (Ico (↑i : ℝ) (↑(i + 1) : ℝ)) volume
Tactic: rw [intervalIntegrable_iff_integrableOn_Ico_of_le (by simp)]
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
h : ∀ i ∈ Ico a b, ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Ico (↑i : ℝ) (↑(i + 1) : ℝ)) x → f (↑i : ℝ) ≤ g x
hg : IntegrableOn (mα := toMeasurableSpace) g (Ico (↑a : ℝ) (↑b : ℝ)) volume
i : ℕ
hi : i ∈ Finset.Ico a b
⊢ IntegrableOn (mα := Real.measurableSpace) g (Ico (↑i : ℝ) (↑(i + 1) : ℝ)) volume
have apply : Subset (α := Set ℝ) (Ico (↑i : ℝ) (↑(i + 1) : ℝ)) (Ico (↑a : ℝ) (↑b : ℝ))
Tactic: apply hg.mono _ le_rfl
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (hypothesis)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
h : ∀ i ∈ Ico a b, ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Ico (↑i : ℝ) (↑(i + 1) : ℝ)) x → f (↑i : ℝ) ≤ g x
hg : IntegrableOn (mα := toMeasurableSpace) g (Ico (↑a : ℝ) (↑b : ℝ)) volume
i : ℕ
hi : i ∈ Finset.Ico a b
x : ℝ
hx : (↑i : ℝ) ≤ x
h'x : x < (↑(i + 1) : ℝ)
⊢ Membership.mem (γ := Set ℝ) (Ico (↑a : ℝ) (↑b : ℝ)) x
have hi₁ : a ≤ i ∧ i < b
Tactic: simp only [Finset.mem_Ico, mem_Ico] at hi ⊢
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (hypothesis)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
h : ∀ i ∈ Ico a b, ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Ico (↑i : ℝ) (↑(i + 1) : ℝ)) x → f (↑i : ℝ) ≤ g x
hg : IntegrableOn (mα := toMeasurableSpace) g (Ico (↑a : ℝ) (↑b : ℝ)) volume
⊢ LE.le (α := ℝ) (∑ i ∈ Finset.Ico a b, f (↑i : ℝ)) (∫ (x : ℝ) in (↑a : ℝ)..(↑b : ℝ), g x)
have A : ∀ (i : ℕ) (hi : i ∈ Finset.Ico a b), IntervalIntegrable g volume (↑i : ℝ) (↑(i + 1) : ℝ)
Tactic: have A i (hi : i ∈ Finset.Ico a b) : IntervalIntegrable g volume i (i + 1 : ℕ) := by
    rw [intervalIntegrable_iff_integrableOn_Ico_of_le (by simp)]
    apply hg.mono _ le_rfl
    rintro x ⟨hx, h'x⟩
    simp only [Finset.mem_Ico, mem_Ico] at hi ⊢
    exact ⟨le_trans (mod_cast hi.1) hx, h'x.trans_le (mod_cast hi.2)⟩
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
h : ∀ i ∈ Ico a b, ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Ico (↑i : ℝ) (↑(i + 1) : ℝ)) x → f (↑i : ℝ) ≤ g x
hg : IntegrableOn (mα := toMeasurableSpace) g (Ico (↑a : ℝ) (↑b : ℝ)) volume
A : ∀ (i : ℕ) (hi : i ∈ Finset.Ico a b), IntervalIntegrable g volume (↑i : ℝ) (↑(i + 1) : ℝ)
⊢ LE.le (α := ℝ) (∑ i ∈ Finset.Ico a b, ∫ (x : ℝ) in (↑i : ℝ)..(↑(i + 1) : ℝ), f (↑i : ℝ))
    (∑ i ∈ Finset.Ico a b, ∫ (x : ℝ) in (↑i : ℝ)..(↑(i + 1) : ℝ), g x)
have h₁ : ∀ (i : ℕ) (hi : i ∈ Finset.Ico a b),
  LE.le (α := ℝ) (∫ (x : ℝ) in (↑i : ℝ)..(↑(i + 1) : ℝ), f (↑i : ℝ)) (∫ (x : ℝ) in (↑i : ℝ)..(↑(i + 1) : ℝ), g x)
Tactic: gcongr with i hi
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
h : ∀ i ∈ Ico a b, ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Ico (↑i : ℝ) (↑(i + 1) : ℝ)) x → f (↑i : ℝ) ≤ g x
hg : IntegrableOn (mα := toMeasurableSpace) g (Ico (↑a : ℝ) (↑b : ℝ)) volume
A : ∀ (i : ℕ) (hi : i ∈ Finset.Ico a b), IntervalIntegrable g volume (↑i : ℝ) (↑(i + 1) : ℝ)
i : ℕ
hi : i ∈ Finset.Ico a b
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in (↑i : ℝ)..(↑(i + 1) : ℝ), f (↑i : ℝ)) (∫ (x : ℝ) in (↑i : ℝ)..(↑(i + 1) : ℝ), g x)
have apply : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioo (↑i : ℝ) (↑(i + 1) : ℝ)) x), f (↑i : ℝ) ≤ g x
Tactic: apply intervalIntegral.integral_mono_on_of_le_Ioo (by simp) (by simp) (A _ hi) (fun x hx ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
h : ∀ i ∈ Ico a b, ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Ico (↑i : ℝ) (↑(i + 1) : ℝ)) x → f (↑i : ℝ) ≤ g x
hg : IntegrableOn (mα := toMeasurableSpace) g (Ico (↑a : ℝ) (↑b : ℝ)) volume
A : ∀ (i : ℕ) (hi : i ∈ Finset.Ico a b), IntervalIntegrable g volume (↑i : ℝ) (↑(i + 1) : ℝ)
⊢ Eq (α := ℝ) (∑ i ∈ Finset.Ico a b, ∫ (x : ℝ) in (↑i : ℝ)..(↑(i + 1) : ℝ), g x) (∫ (x : ℝ) in (↑a : ℝ)..(↑b : ℝ), g x)
have rw : ∀ k ∈ Ico a b, IntervalIntegrable g volume (↑k : ℝ) (↑(k + 1) : ℝ)
Tactic: rw [intervalIntegral.sum_integral_adjacent_intervals_Ico (a := fun i ↦ i) hab]
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
h : ∀ i ∈ Ico a b, ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Ico (↑i : ℝ) (↑(i + 1) : ℝ)) x → f (↑i : ℝ) ≤ g x
hg : IntegrableOn (mα := toMeasurableSpace) g (Ico (↑a : ℝ) (↑b : ℝ)) volume
A : ∀ (i : ℕ) (hi : i ∈ Finset.Ico a b), IntervalIntegrable g volume (↑i : ℝ) (↑(i + 1) : ℝ)
⊢ LE.le (α := ℝ) (∑ i ∈ Finset.Ico a b, f (↑i : ℝ)) (∫ (x : ℝ) in (↑a : ℝ)..(↑b : ℝ), g x)
have i : Eq (α := ℝ) (∑ i ∈ Finset.Ico a b, f (↑i : ℝ)) (∑ i ∈ Finset.Ico a b, ∫ (x : ℝ) in (↑i : ℝ)..(↑(i + 1) : ℝ), f (↑i : ℝ))
Tactic: calc
  ∑ i ∈ Finset.Ico a b, f i
  _ = ∑ i ∈ Finset.Ico a b, (∫ x in (i : ℝ)..(i + 1 : ℕ), f i) := by simp
  _ ≤ ∑ i ∈ Finset.Ico a b, (∫ x in (i : ℝ)..(i + 1 : ℕ), g x) := by
    gcongr with i hi
    apply intervalIntegral.integral_mono_on_of_le_Ioo (by simp) (by simp) (A _ hi) (fun x hx ↦ ?_)
    exact h _ (by simpa using hi) _ (Ioo_subset_Ico_self hx)
  _ = ∫ x in a..b, g x := by
    rw [intervalIntegral.sum_integral_adjacent_intervals_Ico (a := fun i ↦ i) hab]
    intro i hi
    exact A _ (by simpa using hi)
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
h : ∀ i ∈ Ico a b, ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Ico (↑i : ℝ) (↑(i + 1) : ℝ)) x → f (↑i : ℝ) ≤ g x
hg : IntegrableOn (mα := toMeasurableSpace) g (Ico (↑a : ℝ) (↑b : ℝ)) volume
A : ∀ (i : ℕ) (hi : i ∈ Finset.Ico a b), IntervalIntegrable g volume (↑i : ℝ) (↑(i + 1) : ℝ)
i :
  Eq (α := ℝ) (∑ i ∈ Finset.Ico a b, f (↑i : ℝ))
    (∑ i ∈ Finset.Ico a b, ∫ (x : ℝ) in (↑i : ℝ)..(↑(i + 1) : ℝ), f (↑i : ℝ))
⊢ LE.le (α := ℝ) (∑ i ∈ Finset.Ico a b, f (↑i : ℝ)) (∫ (x : ℝ) in (↑a : ℝ)..(↑b : ℝ), g x)
have i₁ : LE.le (α := ℝ) (∑ i ∈ Finset.Ico a b, ∫ (x : ℝ) in (↑i : ℝ)..(↑(i + 1) : ℝ), f (↑i : ℝ))
  (∑ i ∈ Finset.Ico a b, ∫ (x : ℝ) in (↑i : ℝ)..(↑(i + 1) : ℝ), g x)
Tactic: calc
  ∑ i ∈ Finset.Ico a b, f i
  _ = ∑ i ∈ Finset.Ico a b, (∫ x in (i : ℝ)..(i + 1 : ℕ), f i) := by simp
  _ ≤ ∑ i ∈ Finset.Ico a b, (∫ x in (i : ℝ)..(i + 1 : ℕ), g x) := by
    gcongr with i hi
    apply intervalIntegral.integral_mono_on_of_le_Ioo (by simp) (by simp) (A _ hi) (fun x hx ↦ ?_)
    exact h _ (by simpa using hi) _ (Ioo_subset_Ico_self hx)
  _ = ∫ x in a..b, g x := by
    rw [intervalIntegral.sum_integral_adjacent_intervals_Ico (a := fun i ↦ i) hab]
    intro i hi
    exact A _ (by simpa using hi)
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
h : ∀ i ∈ Ico a b, ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Ico (↑i : ℝ) (↑(i + 1) : ℝ)) x → f (↑i : ℝ) ≤ g x
hg : IntegrableOn (mα := toMeasurableSpace) g (Ico (↑a : ℝ) (↑b : ℝ)) volume
A : ∀ (i : ℕ) (hi : i ∈ Finset.Ico a b), IntervalIntegrable g volume (↑i : ℝ) (↑(i + 1) : ℝ)
i :
  Eq (α := ℝ) (∑ i ∈ Finset.Ico a b, f (↑i : ℝ))
    (∑ i ∈ Finset.Ico a b, ∫ (x : ℝ) in (↑i : ℝ)..(↑(i + 1) : ℝ), f (↑i : ℝ))
i₁ :
  LE.le (α := ℝ) (∑ i ∈ Finset.Ico a b, ∫ (x : ℝ) in (↑i : ℝ)..(↑(i + 1) : ℝ), f (↑i : ℝ))
    (∑ i ∈ Finset.Ico a b, ∫ (x : ℝ) in (↑i : ℝ)..(↑(i + 1) : ℝ), g x)
⊢ LE.le (α := ℝ) (∑ i ∈ Finset.Ico a b, f (↑i : ℝ)) (∫ (x : ℝ) in (↑a : ℝ)..(↑b : ℝ), g x)
have i₂ : Eq (α := ℝ) (∑ i ∈ Finset.Ico a b, ∫ (x : ℝ) in (↑i : ℝ)..(↑(i + 1) : ℝ), g x) (∫ (x : ℝ) in (↑a : ℝ)..(↑b : ℝ), g x)
Tactic: calc
  ∑ i ∈ Finset.Ico a b, f i
  _ = ∑ i ∈ Finset.Ico a b, (∫ x in (i : ℝ)..(i + 1 : ℕ), f i) := by simp
  _ ≤ ∑ i ∈ Finset.Ico a b, (∫ x in (i : ℝ)..(i + 1 : ℕ), g x) := by
    gcongr with i hi
    apply intervalIntegral.integral_mono_on_of_le_Ioo (by simp) (by simp) (A _ hi) (fun x hx ↦ ?_)
    exact h _ (by simpa using hi) _ (Ioo_subset_Ico_self hx)
  _ = ∫ x in a..b, g x := by
    rw [intervalIntegral.sum_integral_adjacent_intervals_Ico (a := fun i ↦ i) hab]
    intro i hi
    exact A _ (by simpa using hi)
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
h : ∀ i ∈ Ico a b, ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Ico (↑i : ℝ) (↑(i + 1) : ℝ)) x → g x ≤ f (↑i : ℝ)
hg : IntegrableOn (mα := toMeasurableSpace) g (Ico (↑a : ℝ) (↑b : ℝ)) volume
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in (↑a : ℝ)..(↑b : ℝ), g x) (∑ i ∈ Finset.Ico a b, f (↑i : ℝ))
have h₁ : Eq (α := ℝ) (∫ (x : ℝ) in (↑a : ℝ)..(↑b : ℝ), g x) (-∫ (x : ℝ) in (↑a : ℝ)..(↑b : ℝ), (-g) x)
Tactic: convert!
    neg_le_neg
      (sum_Ico_le_integral_of_le (f := -f) (g := -g) hab (fun i hi x hx ↦ neg_le_neg (h i hi x hx))
        hg.neg)
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
h : ∀ i ∈ Ico a b, ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Ico (↑i : ℝ) (↑(i + 1) : ℝ)) x → g x ≤ f (↑i : ℝ)
hg : IntegrableOn (mα := toMeasurableSpace) g (Ico (↑a : ℝ) (↑b : ℝ)) volume
h₁ : Eq (α := ℝ) (∫ (x : ℝ) in (↑a : ℝ)..(↑b : ℝ), g x) (-∫ (x : ℝ) in (↑a : ℝ)..(↑b : ℝ), (-g) x)
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in (↑a : ℝ)..(↑b : ℝ), g x) (∑ i ∈ Finset.Ico a b, f (↑i : ℝ))
have h₂ : Eq (α := ℝ) (∑ i ∈ Finset.Ico a b, f (↑i : ℝ)) (-∑ i ∈ Finset.Ico a b, (-f) (↑i : ℝ))
Tactic: convert!
    neg_le_neg
      (sum_Ico_le_integral_of_le (f := -f) (g := -g) hab (fun i hi x hx ↦ neg_le_neg (h i hi x hx))
        hg.neg)
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
k : ℕ
hk : k < a
⊢ IntervalIntegrable f volume (x₀ + (↑k : ℝ)) (x₀ + (↑(k + 1) : ℝ))
have refine : uIcc (x₀ + (↑k : ℝ)) (x₀ + (↑(k + 1) : ℝ)) ⊆ Icc x₀ (x₀ + (↑a : ℝ))
Tactic: refine (hf.mono ?_).intervalIntegrable
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
k : ℕ
hk : k < a
⊢ uIcc (x₀ + (↑k : ℝ)) (x₀ + (↑(k + 1) : ℝ)) ⊆ Icc x₀ (x₀ + (↑a : ℝ))
have rw : Icc (x₀ + (↑k : ℝ)) (x₀ + (↑(k + 1) : ℝ)) ⊆ Icc x₀ (x₀ + (↑a : ℝ))
Tactic: rw [uIcc_of_le]
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
k : ℕ
hk : k < a
rw : Icc (x₀ + (↑k : ℝ)) (x₀ + (↑(k + 1) : ℝ)) ⊆ Icc x₀ (x₀ + (↑a : ℝ))
⊢ uIcc (x₀ + (↑k : ℝ)) (x₀ + (↑(k + 1) : ℝ)) ⊆ Icc x₀ (x₀ + (↑a : ℝ))
have rw₁ : x₀ + (↑k : ℝ) ≤ x₀ + (↑(k + 1) : ℝ)
Tactic: rw [uIcc_of_le]
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
k : ℕ
hk : k < a
⊢ Icc (x₀ + (↑k : ℝ)) (x₀ + (↑(k + 1) : ℝ)) ⊆ Icc x₀ (x₀ + (↑a : ℝ))
have ha : x₀ ≤ x₀ + (↑k : ℝ)
Tactic: apply Icc_subset_Icc
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
k : ℕ
hk : k < a
ha : x₀ ≤ x₀ + (↑k : ℝ)
⊢ Icc (x₀ + (↑k : ℝ)) (x₀ + (↑(k + 1) : ℝ)) ⊆ Icc x₀ (x₀ + (↑a : ℝ))
have hb : x₀ + (↑(k + 1) : ℝ) ≤ x₀ + (↑a : ℝ)
Tactic: apply Icc_subset_Icc
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (hypothesis)
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in x₀..x₀ + (↑a : ℝ), f x) (∑ i ∈ Finset.range a, f (x₀ + (↑i : ℝ)))
have hint : ∀ k < a, IntervalIntegrable f volume (x₀ + (↑k : ℝ)) (x₀ + (↑(k + 1) : ℝ))
Tactic: have hint : ∀ k : ℕ, k < a → IntervalIntegrable f volume (x₀ + k) (x₀ + (k + 1 : ℕ)) := by
    intro k hk
    refine (hf.mono ?_).intervalIntegrable
    rw [uIcc_of_le]
    · apply Icc_subset_Icc
      · simp only [le_add_iff_nonneg_right, Nat.cast_nonneg]
      · simp only [add_le_add_iff_left, Nat.cast_le, Nat.succ_le_of_lt hk]
    · simp only [add_le_add_iff_left, Nat.cast_le, Nat.le_succ]
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
hint : ∀ k < a, IntervalIntegrable f volume (x₀ + (↑k : ℝ)) (x₀ + (↑(k + 1) : ℝ))
⊢ Eq (α := ℝ) (∫ (x : ℝ) in x₀..x₀ + (↑a : ℝ), f x)
    (∑ i ∈ Finset.range a, ∫ (x : ℝ) in x₀ + (↑i : ℝ)..x₀ + (↑(i + 1) : ℝ), f x)
have h : x₀ = x₀ + (↑0 : ℝ)
Tactic: convert! (intervalIntegral.sum_integral_adjacent_intervals hint).symm
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
hint : ∀ k < a, IntervalIntegrable f volume (x₀ + (↑k : ℝ)) (x₀ + (↑(k + 1) : ℝ))
⊢ LE.le (α := ℝ) (∑ i ∈ Finset.range a, ∫ (x : ℝ) in x₀ + (↑i : ℝ)..x₀ + (↑(i + 1) : ℝ), f x)
    (∑ i ∈ Finset.range a, ∫ (x : ℝ) in x₀ + (↑i : ℝ)..x₀ + (↑(i + 1) : ℝ), f (x₀ + (↑i : ℝ)))
have h : ∀ (i : ℕ) (hi : i ∈ Finset.range a),
  LE.le (α := ℝ) (∫ (x : ℝ) in x₀ + (↑i : ℝ)..x₀ + (↑(i + 1) : ℝ), f x)
    (∫ (x : ℝ) in x₀ + (↑i : ℝ)..x₀ + (↑(i + 1) : ℝ), f (x₀ + (↑i : ℝ)))
Tactic: gcongr with i hi
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (hypothesis)
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
hint : ∀ k < a, IntervalIntegrable f volume (x₀ + (↑k : ℝ)) (x₀ + (↑(k + 1) : ℝ))
i : ℕ
hi : i ∈ Finset.range a
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in x₀ + (↑i : ℝ)..x₀ + (↑(i + 1) : ℝ), f x)
    (∫ (x : ℝ) in x₀ + (↑i : ℝ)..x₀ + (↑(i + 1) : ℝ), f (x₀ + (↑i : ℝ)))
have ia : i < a
Tactic: have ia : i < a := Finset.mem_range.1 hi
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
hint : ∀ k < a, IntervalIntegrable f volume (x₀ + (↑k : ℝ)) (x₀ + (↑(k + 1) : ℝ))
i : ℕ
hi : i ∈ Finset.range a
ia : i < a
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in x₀ + (↑i : ℝ)..x₀ + (↑(i + 1) : ℝ), f x)
    (∫ (x : ℝ) in x₀ + (↑i : ℝ)..x₀ + (↑(i + 1) : ℝ), f (x₀ + (↑i : ℝ)))
have h : ∀ (x : ℝ) (hx : x ∈ Icc (x₀ + (↑i : ℝ)) (x₀ + (↑(i + 1) : ℝ))), f x ≤ f (x₀ + (↑i : ℝ))
Tactic: refine intervalIntegral.integral_mono_on (by simp) (hint _ ia) (by simp) fun x hx => ?_
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
hint : ∀ k < a, IntervalIntegrable f volume (x₀ + (↑k : ℝ)) (x₀ + (↑(k + 1) : ℝ))
i : ℕ
hi : i ∈ Finset.range a
ia : i < a
x : ℝ
hx : x ∈ Icc (x₀ + (↑i : ℝ)) (x₀ + (↑(i + 1) : ℝ))
⊢ f x ≤ f (x₀ + (↑i : ℝ))
have apply : x₀ + (↑i : ℝ) ∈ Icc x₀ (x₀ + (↑a : ℝ))
Tactic: apply hf _ _ hx.1
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
hint : ∀ k < a, IntervalIntegrable f volume (x₀ + (↑k : ℝ)) (x₀ + (↑(k + 1) : ℝ))
i : ℕ
hi : i ∈ Finset.range a
ia : i < a
x : ℝ
hx : x ∈ Icc (x₀ + (↑i : ℝ)) (x₀ + (↑(i + 1) : ℝ))
apply : x₀ + (↑i : ℝ) ∈ Icc x₀ (x₀ + (↑a : ℝ))
⊢ f x ≤ f (x₀ + (↑i : ℝ))
have apply₁ : x ∈ Icc x₀ (x₀ + (↑a : ℝ))
Tactic: apply hf _ _ hx.1
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
hint : ∀ k < a, IntervalIntegrable f volume (x₀ + (↑k : ℝ)) (x₀ + (↑(k + 1) : ℝ))
i : ℕ
hi : i ∈ Finset.range a
ia : i < a
x : ℝ
hx : x ∈ Icc (x₀ + (↑i : ℝ)) (x₀ + (↑(i + 1) : ℝ))
⊢ x ∈ Icc x₀ (x₀ + (↑a : ℝ))
have refine : x₀ + (↑(i + 1) : ℝ) ≤ x₀ + (↑a : ℝ)
Tactic: refine mem_Icc.2 ⟨le_trans (by simp) hx.1, le_trans hx.2 ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
hint : ∀ k < a, IntervalIntegrable f volume (x₀ + (↑k : ℝ)) (x₀ + (↑(k + 1) : ℝ))
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in x₀..x₀ + (↑a : ℝ), f x) (∑ i ∈ Finset.range a, f (x₀ + (↑i : ℝ)))
have x : Eq (α := ℝ) (∫ (x : ℝ) in x₀..x₀ + (↑a : ℝ), f x)
  (∑ i ∈ Finset.range a, ∫ (x : ℝ) in x₀ + (↑i : ℝ)..x₀ + (↑(i + 1) : ℝ), f x)
Tactic: calc
    ∫ x in x₀..x₀ + a, f x = ∑ i ∈ Finset.range a, ∫ x in x₀ + i..x₀ + (i + 1 : ℕ), f x := by
      convert! (intervalIntegral.sum_integral_adjacent_intervals hint).symm
      simp only [Nat.cast_zero, add_zero]
    _ ≤ ∑ i ∈ Finset.range a, ∫ _ in x₀ + i..x₀ + (i + 1 : ℕ), f (x₀ + i) := by
      gcongr with i hi
      have ia : i < a := Finset.mem_range.1 hi
      refine intervalIntegral.integral_mono_on (by simp) (hint _ ia) (by simp) fun x hx => ?_
      apply hf _ _ hx.1
      · simp only [ia.le, mem_Icc, le_add_iff_nonneg_right, Nat.cast_nonneg, add_le_add_iff_left,
          Nat.cast_le, and_self_iff]
      · refine mem_Icc.2 ⟨le_trans (by simp) hx.1, le_trans hx.2 ?_⟩
        simp only [add_le_add_iff_left, Nat.cast_le, Nat.succ_le_of_lt ia]
    _ = ∑ i ∈ Finset.range a, f (x₀ + i) := by simp
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
hint : ∀ k < a, IntervalIntegrable f volume (x₀ + (↑k : ℝ)) (x₀ + (↑(k + 1) : ℝ))
x :
  Eq (α := ℝ) (∫ (x : ℝ) in x₀..x₀ + (↑a : ℝ), f x)
    (∑ i ∈ Finset.range a, ∫ (x : ℝ) in x₀ + (↑i : ℝ)..x₀ + (↑(i + 1) : ℝ), f x)
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in x₀..x₀ + (↑a : ℝ), f x) (∑ i ∈ Finset.range a, f (x₀ + (↑i : ℝ)))
have x₁ : LE.le (α := ℝ) (∑ i ∈ Finset.range a, ∫ (x : ℝ) in x₀ + (↑i : ℝ)..x₀ + (↑(i + 1) : ℝ), f x)
  (∑ i ∈ Finset.range a, ∫ (x : ℝ) in x₀ + (↑i : ℝ)..x₀ + (↑(i + 1) : ℝ), f (x₀ + (↑i : ℝ)))
Tactic: calc
    ∫ x in x₀..x₀ + a, f x = ∑ i ∈ Finset.range a, ∫ x in x₀ + i..x₀ + (i + 1 : ℕ), f x := by
      convert! (intervalIntegral.sum_integral_adjacent_intervals hint).symm
      simp only [Nat.cast_zero, add_zero]
    _ ≤ ∑ i ∈ Finset.range a, ∫ _ in x₀ + i..x₀ + (i + 1 : ℕ), f (x₀ + i) := by
      gcongr with i hi
      have ia : i < a := Finset.mem_range.1 hi
      refine intervalIntegral.integral_mono_on (by simp) (hint _ ia) (by simp) fun x hx => ?_
      apply hf _ _ hx.1
      · simp only [ia.le, mem_Icc, le_add_iff_nonneg_right, Nat.cast_nonneg, add_le_add_iff_left,
          Nat.cast_le, and_self_iff]
      · refine mem_Icc.2 ⟨le_trans (by simp) hx.1, le_trans hx.2 ?_⟩
        simp only [add_le_add_iff_left, Nat.cast_le, Nat.succ_le_of_lt ia]
    _ = ∑ i ∈ Finset.range a, f (x₀ + i) := by simp