awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Subadditive
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 : ℝ)))
⊢ ∀ᶠ (a : ℕ) in atTop, u (n * a + r) / (↑(n * a + r) : ℝ) < L

Tactic:
((B.comp tendsto_natCast_atTop_atTop).eventually (gt_mem_nhds hL)).mono fun k hk => ?_

Premises used: gt_mem_nhds, Filter.Eventually.mono, tendsto_natCast_atTop_atTop, Filter.Tendsto.eventually, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.Subadditive
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 : ℝ)))
refine :
  ∀ (k : ℕ) (hk : ((fun (x : ℝ) ↦ (x * u n + u r) / (x * (↑n : ℝ) + (↑r : ℝ))) ∘ Nat.cast) k < L),
    u (n * k + r) / (↑(n * k + r) : ℝ) < L
⊢ ∀ᶠ (a : ℕ) in atTop, u (n * a + r) / (↑(n * a + r) : ℝ) < L

Tactic:
refine ((B.comp tendsto_natCast_atTop_atTop).eventually (gt_mem_nhds hL)).mono fun k hk => ?_

Premises used: gt_mem_nhds, Filter.Eventually.mono, tendsto_natCast_atTop_atTop, Filter.Tendsto.eventually, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.Subadditive
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
rw : u (k * n + r) / (↑(k * n + r) : ℝ) < L
⊢ u (n * k + r) / (↑(n * k + r) : ℝ) < L

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Analysis.Subadditive
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) : ℝ) < L

Tactic:
lt_of_le_of_lt ?_ hk

Premises used: lt_of_le_of_lt
-- Module: Mathlib.Analysis.Subadditive
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
refine : u (k * n + r) / (↑(k * n + r) : ℝ) ≤ ((fun (x : ℝ) ↦ (x * u n + u r) / (x * (↑n : ℝ) + (↑r : ℝ))) ∘ Nat.cast) k
⊢ u (k * n + r) / (↑(k * n + r) : ℝ) < L

Tactic:
refine lt_of_le_of_lt ?_ hk

Premises used: lt_of_le_of_lt
-- Module: Mathlib.Analysis.Subadditive
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
simp : u (k * n + r) / (↑(k * n + r) : ℝ) ≤ ((↑k : ℝ) * u n + u r) / (↑(k * n + r) : ℝ)
⊢ u (k * n + r) / (↑(k * n + r) : ℝ) ≤ ((fun (x : ℝ) ↦ (x * u n + u r) / (x * (↑n : ℝ) + (↑r : ℝ))) ∘ Nat.cast) k

Tactic:
simp only [(· ∘ ·), ← Nat.cast_add, ← Nat.cast_mul]

Premises used: Function.comp, Nat.cast_add, Nat.cast_mul
-- Module: Mathlib.Analysis.Subadditive
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
hab : u (k * n + r) ≤ (↑k : ℝ) * u n + u r
⊢ u (k * n + r) / (↑(k * n + r) : ℝ) ≤ ((↑k : ℝ) * u n + u r) / (↑(k * n + r) : ℝ)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Subadditive
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 : ℝ) * u n + u r

Tactic:
apply h.apply_mul_add_le

Premises used: Subadditive.apply_mul_add_le
-- Module: Mathlib.Analysis.Subadditive
Goal:
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (α := ℝ) (range fun (n : ℕ) ↦ u n / (↑n : ℝ))
⊢ Tendsto (fun (n : ℕ) ↦ u n / (↑n : ℝ)) atTop (𝓝 h.lim)

Tactic:
tendsto_order.2 ⟨fun l hl => ?_, fun L hL => ?_⟩

Premises used: Iff.mpr, tendsto_order, And.intro
-- Module: Mathlib.Analysis.Subadditive
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 : ℝ)
refine_2 : ∀ (L : ℝ) (hL : L > h.lim), ∀ᶠ (b : ℕ) in atTop, u b / (↑b : ℝ) < L
⊢ Tendsto (fun (n : ℕ) ↦ u n / (↑n : ℝ)) atTop (𝓝 h.lim)

Tactic:
refine tendsto_order.2 ⟨fun l hl => ?_, fun L hL => ?_⟩

Premises used: Iff.mpr, tendsto_order, And.intro
-- Module: Mathlib.Analysis.Subadditive
Goal:
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (α := ℝ) (range fun (n : ℕ) ↦ u n / (↑n : ℝ))
l : ℝ
hl : l < h.lim
⊢ ∀ᶠ (b : ℕ) in atTop, l < u b / (↑b : ℝ)

Tactic:
eventually_atTop.2
      ⟨1, fun n hn => hl.trans_le (h.lim_le_div hbdd (zero_lt_one.trans_le hn).ne')⟩

Premises used: Iff.mpr, LT.lt.ne', zero_lt_one, LT.lt.trans_le, Exists.intro, Filter.eventually_atTop, OfNat.ofNat, Subadditive.lim_le_div
-- Module: Mathlib.Analysis.Subadditive
Goal:
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (α := ℝ) (range fun (n : ℕ) ↦ u n / (↑n : ℝ))
l : ℝ
hl : l < h.lim
⊢ ∀ᶠ (b : ℕ) in atTop, l < u b / (↑b : ℝ)

Tactic:
refine eventually_atTop.2
      ⟨1, fun n hn => hl.trans_le (h.lim_le_div hbdd (zero_lt_one.trans_le hn).ne')⟩

Premises used: Iff.mpr, LT.lt.ne', zero_lt_one, LT.lt.trans_le, Exists.intro, Filter.eventually_atTop, OfNat.ofNat, Subadditive.lim_le_div
-- Module: Mathlib.Analysis.Subadditive
Goal:
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (α := ℝ) (range fun (n : ℕ) ↦ u n / (↑n : ℝ))
L : ℝ
hL : L > h.lim
⊢ L > sInf ((fun (n : ℕ) ↦ u n / (↑n : ℝ)) '' Ici 1)

Tactic:
rw [Subadditive.lim] at hL

Premises used: Subadditive.lim
-- Module: Mathlib.Analysis.Subadditive
Goal:
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (α := ℝ) (range fun (n : ℕ) ↦ u n / (↑n : ℝ))
L : ℝ
hL : L > sInf ((fun (n : ℕ) ↦ u n / (↑n : ℝ)) '' Ici 1)
⊢ Set.Nonempty (α := ℝ) ((fun (n : ℕ) ↦ u n / (↑n : ℝ)) '' Ici 1)

Tactic:
simp
-- Module: Mathlib.Analysis.Subadditive
Goal:
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (α := ℝ) (range fun (n : ℕ) ↦ u n / (↑n : ℝ))
L : ℝ
hL : L > sInf ((fun (n : ℕ) ↦ u n / (↑n : ℝ)) '' Ici 1)
rcases :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) ((fun (n : ℕ) ↦ u n / (↑n : ℝ)) '' Ici 1) x) (xL : x < L),
    ∃ (n : ℕ), 0 < n ∧ u n / (↑n : ℝ) < L
⊢ ∃ (n : ℕ), 0 < n ∧ u n / (↑n : ℝ) < L

Tactic:
rcases exists_lt_of_csInf_lt (by simp) hL with ⟨x, hx, xL⟩

Premises used: exists_lt_of_csInf_lt
-- Module: Mathlib.Analysis.Subadditive
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
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
⊢ ∃ (n : ℕ), 0 < n ∧ u n / (↑n : ℝ) < L

Tactic:
rcases (mem_image _ _ _).1 hx with ⟨n, hn, rfl⟩

Premises used: Set.mem_image, Iff.mp, rfl
-- Module: Mathlib.Analysis.Subadditive
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 : ℕ
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:
⟨n, zero_lt_one.trans_le hn, xL⟩

Premises used: zero_lt_one, LT.lt.trans_le, And.intro, Exists.intro
-- Module: Mathlib.Analysis.Subadditive
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 : ℕ
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:
exact ⟨n, zero_lt_one.trans_le hn, xL⟩
-- Module: Mathlib.Analysis.Subadditive
Goal:
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (α := ℝ) (range fun (n : ℕ) ↦ u n / (↑n : ℝ))
L : ℝ
hL : L > h.lim
refine_2 : ∀ (n : ℕ) (npos : 0 < n) (hn : u n / (↑n : ℝ) < L), ∀ᶠ (b : ℕ) in atTop, u b / (↑b : ℝ) < 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⟩
-- Module: Mathlib.Analysis.Subadditive
Goal:
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (α := ℝ) (range fun (n : ℕ) ↦ u n / (↑n : ℝ))
L : ℝ
hL : L > h.lim
n : ℕ
npos : 0 < n
hn : u n / (↑n : ℝ) < L
⊢ ∀ᶠ (b : ℕ) in atTop, u b / (↑b : ℝ) < L

Tactic:
h.eventually_div_lt_of_div_lt npos.ne' hn

Premises used: LT.lt.ne', Subadditive.eventually_div_lt_of_div_lt
-- Module: Mathlib.Analysis.Subadditive
Goal:
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (α := ℝ) (range fun (n : ℕ) ↦ u n / (↑n : ℝ))
L : ℝ
hL : L > h.lim
n : ℕ
npos : 0 < n
hn : u n / (↑n : ℝ) < L
⊢ ∀ᶠ (b : ℕ) in atTop, u b / (↑b : ℝ) < L

Tactic:
exact h.eventually_div_lt_of_div_lt npos.ne' hn

Premises used: LT.lt.ne', Subadditive.eventually_div_lt_of_div_lt
-- Module: Mathlib.Analysis.SumIntegralComparisons
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
⊢ LE.le (α := ℝ) (↑i : ℝ) (↑(i + 1) : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.SumIntegralComparisons
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
rw : IntegrableOn (mα := Real.measurableSpace) g (Ico (↑i : ℝ) (↑(i + 1) : ℝ)) volume
⊢ IntervalIntegrable g volume (↑i : ℝ) (↑(i + 1) : ℝ)

Tactic:
rw [intervalIntegrable_iff_integrableOn_Ico_of_le (by simp)]

Premises used: intervalIntegrable_iff_integrableOn_Ico_of_le
-- Module: Mathlib.Analysis.SumIntegralComparisons
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
apply : Subset (α := Set ℝ) (Ico (↑i : ℝ) (↑(i + 1) : ℝ)) (Ico (↑a : ℝ) (↑b : ℝ))
⊢ IntegrableOn (mα := Real.measurableSpace) g (Ico (↑i : ℝ) (↑(i + 1) : ℝ)) volume

Tactic:
apply hg.mono _ le_rfl

Premises used: le_rfl, MeasureTheory.IntegrableOn.mono
-- Module: Mathlib.Analysis.SumIntegralComparisons
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) : ℝ)
⊢ a ≤ i ∧ i < b

Tactic:
simp only [Finset.mem_Ico, mem_Ico] at hi ⊢

Premises used: Set.mem_Ico, Finset.mem_Ico
-- Module: Mathlib.Analysis.SumIntegralComparisons
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 : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x
h'x : x < (↑(i + 1) : ℝ)
hi : a ≤ i ∧ i < b
⊢ (↑a : ℝ) ≤ x ∧ x < (↑b : ℝ)

Tactic:
⟨le_trans (mod_cast hi.1) hx, h'x.trans_le (mod_cast hi.2)⟩

Premises used: cast, Nat.cast_le._simp_1, And.right, LT.lt.trans_le, And.intro, Eq.symm, le_trans
-- Module: Mathlib.Analysis.SumIntegralComparisons
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 : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x
h'x : x < (↑(i + 1) : ℝ)
hi : a ≤ i ∧ i < b
⊢ (↑a : ℝ) ≤ x ∧ x < (↑b : ℝ)

Tactic:
exact ⟨le_trans (mod_cast hi.1) hx, h'x.trans_le (mod_cast hi.2)⟩
-- Module: Mathlib.Analysis.SumIntegralComparisons
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) : ℝ)

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)⟩
-- Module: Mathlib.Analysis.SumIntegralComparisons
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, f (↑i : ℝ))
    (∑ i ∈ Finset.Ico a b, ∫ (x : ℝ) in (↑i : ℝ)..(↑(i + 1) : ℝ), f (↑i : ℝ))

Tactic:
simp
-- Module: Mathlib.Analysis.SumIntegralComparisons
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) : ℝ)
h₁ :
  ∀ (i : ℕ) (hi : i ∈ Finset.Ico a b),
    LE.le (α := ℝ) (∫ (x : ℝ) in (↑i : ℝ)..(↑(i + 1) : ℝ), f (↑i : ℝ)) (∫ (x : ℝ) in (↑i : ℝ)..(↑(i + 1) : ℝ), g x)
⊢ 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:
gcongr with i hi
-- Module: Mathlib.Analysis.SumIntegralComparisons
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 (α := ℝ) (↑i : ℝ) (↑(i + 1) : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.SumIntegralComparisons
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
⊢ IntervalIntegrable (ε := ℝ) (fun (u : ℝ) ↦ f (↑i : ℝ)) volume (↑i : ℝ) (↑(i + 1) : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.SumIntegralComparisons
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
apply : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioo (↑i : ℝ) (↑(i + 1) : ℝ)) x), f (↑i : ℝ) ≤ g x
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in (↑i : ℝ)..(↑(i + 1) : ℝ), f (↑i : ℝ)) (∫ (x : ℝ) in (↑i : ℝ)..(↑(i + 1) : ℝ), g x)

Tactic:
apply intervalIntegral.integral_mono_on_of_le_Ioo (by simp) (by simp) (A _ hi) (fun x hx ↦ ?_)

Premises used: intervalIntegral.integral_mono_on_of_le_Ioo
-- Module: Mathlib.Analysis.SumIntegralComparisons
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
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo (↑i : ℝ) (↑(i + 1) : ℝ)) x
⊢ i ∈ Ico a b

Tactic:
simpa using hi
-- Module: Mathlib.Analysis.SumIntegralComparisons
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
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo (↑i : ℝ) (↑(i + 1) : ℝ)) x
⊢ f (↑i : ℝ) ≤ g x

Tactic:
exact h _ (by simpa using hi) _ (Ioo_subset_Ico_self hx)

Premises used: Set.Ioo_subset_Ico_self
-- Module: Mathlib.Analysis.SumIntegralComparisons
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) : ℝ)
rw : ∀ k ∈ Ico a b, IntervalIntegrable g volume (↑k : ℝ) (↑(k + 1) : ℝ)
⊢ Eq (α := ℝ) (∑ i ∈ Finset.Ico a b, ∫ (x : ℝ) in (↑i : ℝ)..(↑(i + 1) : ℝ), g x) (∫ (x : ℝ) in (↑a : ℝ)..(↑b : ℝ), g x)

Tactic:
rw [intervalIntegral.sum_integral_adjacent_intervals_Ico (a := fun i ↦ i) hab]

Premises used: intervalIntegral.sum_integral_adjacent_intervals_Ico
-- Module: Mathlib.Analysis.SumIntegralComparisons
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 ∈ Ico a b
⊢ i ∈ Finset.Ico a b

Tactic:
simpa using hi
-- Module: Mathlib.Analysis.SumIntegralComparisons
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 ∈ Ico a b
⊢ IntervalIntegrable g volume (↑i : ℝ) (↑(i + 1) : ℝ)

Tactic:
exact A _ (by simpa using hi)
-- Module: Mathlib.Analysis.SumIntegralComparisons
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)
i₂ :
  Eq (α := ℝ) (∑ i ∈ Finset.Ico a b, ∫ (x : ℝ) in (↑i : ℝ)..(↑(i + 1) : ℝ), g x) (∫ (x : ℝ) in (↑a : ℝ)..(↑b : ℝ), g x)
⊢ LE.le (α := ℝ) (∑ i ∈ Finset.Ico a b, f (↑i : ℝ)) (∫ (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)

Premises used: Finset.Ico
-- Module: Mathlib.Analysis.SumIntegralComparisons
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 : ℝ))

Tactic:
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)

Premises used: sum_Ico_le_integral_of_le, neg_le_neg, MeasureTheory.IntegrableOn.neg
-- Module: Mathlib.Analysis.SumIntegralComparisons
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)
h₂ : Eq (α := ℝ) (∑ i ∈ Finset.Ico a b, f (↑i : ℝ)) (-∑ i ∈ Finset.Ico a b, (-f) (↑i : ℝ))
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in (↑a : ℝ)..(↑b : ℝ), g x) (∑ 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)

Premises used: sum_Ico_le_integral_of_le, neg_le_neg, MeasureTheory.IntegrableOn.neg
-- Module: Mathlib.Analysis.SumIntegralComparisons
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
⊢ Eq (α := ℝ) (∫ (x : ℝ) in (↑a : ℝ)..(↑b : ℝ), g x) (-∫ (x : ℝ) in (↑a : ℝ)..(↑b : ℝ), (-g) x)

Tactic:
simp
-- Module: Mathlib.Analysis.SumIntegralComparisons
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
⊢ Eq (α := ℝ) (∑ i ∈ Finset.Ico a b, f (↑i : ℝ)) (-∑ i ∈ Finset.Ico a b, (-f) (↑i : ℝ))

Tactic:
simp
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
k : ℕ
hk : k < a
⊢ IntervalIntegrable f volume (x₀ + (↑k : ℝ)) (x₀ + (↑(k + 1) : ℝ))

Tactic:
(hf.mono ?_).intervalIntegrable

Premises used: AntitoneOn.intervalIntegrable, AntitoneOn.mono