awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ADEInequality (hypothesis)
Goal:
q r : ℕ+
hqr : q ≤ r
H : 4 ≤ q
h4r : 4 ≤ r
⊢ HAdd.hAdd (α := ℚ) (↑(↑2 : ℕ) : ℚ)⁻¹ (↑(↑q : ℕ) : ℚ)⁻¹ + (↑(↑r : ℕ) : ℚ)⁻¹ ≤ 1
have hq : LE.le (α := ℚ) (↑(↑q : ℕ) : ℚ)⁻¹ 4⁻¹
Tactic: have hq : (q : ℚ)⁻¹ ≤ 4⁻¹ := inv_anti₀ (by positivity) (by exact_mod_cast H)
-- Lean 4 proof step from Mathlib.NumberTheory.ADEInequality (hypothesis)
Goal:
q r : ℕ+
hqr : q ≤ r
H : 4 ≤ q
h4r : 4 ≤ r
hq : LE.le (α := ℚ) (↑(↑q : ℕ) : ℚ)⁻¹ 4⁻¹
⊢ HAdd.hAdd (α := ℚ) (↑(↑2 : ℕ) : ℚ)⁻¹ (↑(↑q : ℕ) : ℚ)⁻¹ + (↑(↑r : ℕ) : ℚ)⁻¹ ≤ 1
have hr : LE.le (α := ℚ) (↑(↑r : ℕ) : ℚ)⁻¹ 4⁻¹
Tactic: have hr : (r : ℚ)⁻¹ ≤ 4⁻¹ := inv_anti₀ (by positivity) (by exact_mod_cast h4r)
-- Lean 4 proof step from Mathlib.NumberTheory.ADEInequality (goal)
Goal:
q r : ℕ+
hqr : q ≤ r
H : 4 ≤ q
h4r : 4 ≤ r
hq : LE.le (α := ℚ) (↑(↑q : ℕ) : ℚ)⁻¹ 4⁻¹
hr : LE.le (α := ℚ) (↑(↑r : ℕ) : ℚ)⁻¹ 4⁻¹
⊢ HAdd.hAdd (α := ℚ) (↑(↑2 : ℕ) : ℚ)⁻¹ (↑(↑q : ℕ) : ℚ)⁻¹ + (↑(↑r : ℕ) : ℚ)⁻¹ ≤ 1
have add_le_add : HAdd.hAdd (α := ℚ) 2⁻¹ 4⁻¹ + 4⁻¹ = 1
Tactic: calc
    (2⁻¹ + (q : ℚ)⁻¹ + (r : ℚ)⁻¹) ≤ 2⁻¹ + 4⁻¹ + 4⁻¹ := add_le_add (add_le_add le_rfl hq) hr
    _ = 1 := by norm_num
-- Lean 4 proof step from Mathlib.NumberTheory.ADEInequality (goal)
Goal:
r : ℕ+
H : 1 < sumInv {2, 3, r}
⊢ r < 6
have contrapose! : ∀ (H : 6 ≤ r), sumInv {2, 3, r} ≤ 1
Tactic: contrapose! H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.NumberTheory.ADEInequality (goal)
Goal:
r : ℕ+
H : 6 ≤ r
⊢ sumInv {2, 3, r} ≤ 1
have rw : HAdd.hAdd (α := ℚ) (↑(↑2 : ℕ) : ℚ)⁻¹ (↑(↑3 : ℕ) : ℚ)⁻¹ + (↑(↑r : ℕ) : ℚ)⁻¹ ≤ 1
Tactic: rw [sumInv_pqr]
-- Lean 4 proof step from Mathlib.NumberTheory.ADEInequality (hypothesis)
Goal:
r : ℕ+
H : 6 ≤ r
⊢ HAdd.hAdd (α := ℚ) (↑(↑2 : ℕ) : ℚ)⁻¹ (↑(↑3 : ℕ) : ℚ)⁻¹ + (↑(↑r : ℕ) : ℚ)⁻¹ ≤ 1
have hr : LE.le (α := ℚ) (↑(↑r : ℕ) : ℚ)⁻¹ 6⁻¹
Tactic: have hr : (r : ℚ)⁻¹ ≤ 6⁻¹ := inv_anti₀ (by positivity) (by exact_mod_cast H)
-- Lean 4 proof step from Mathlib.NumberTheory.ADEInequality (goal)
Goal:
r : ℕ+
H : 6 ≤ r
hr : LE.le (α := ℚ) (↑(↑r : ℕ) : ℚ)⁻¹ 6⁻¹
⊢ HAdd.hAdd (α := ℚ) (↑(↑2 : ℕ) : ℚ)⁻¹ (↑(↑3 : ℕ) : ℚ)⁻¹ + (↑(↑r : ℕ) : ℚ)⁻¹ ≤ 1
have add_le_add : HAdd.hAdd (α := ℚ) 2⁻¹ 3⁻¹ + 6⁻¹ = 1
Tactic: calc
    (2⁻¹ + 3⁻¹ + (r : ℚ)⁻¹ : ℚ) ≤ 2⁻¹ + 3⁻¹ + 6⁻¹ := add_le_add (add_le_add le_rfl le_rfl) hr
    _ = 1 := by norm_num
-- Lean 4 proof step from Mathlib.NumberTheory.ADEInequality (hypothesis)
Goal:
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 1 < sumInv {p, q, r}
⊢ Admissible {p, q, r}
have hp3 : p < 3
Tactic: have hp3 : p < 3 := lt_three hpq hqr H
-- Lean 4 proof step from Mathlib.NumberTheory.ADEInequality (hypothesis)
Goal:
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 1 < sumInv {p, q, r}
hp3 : p < 3
⊢ Admissible {p, q, r}
have hp3₁ : Membership.mem (γ := Finset ℕ+) (Finset.Iio 3) p
Tactic: replace hp3 := Finset.mem_Iio.mpr hp3
Cleared hypotheses: hp3
-- Lean 4 proof step from Mathlib.NumberTheory.ADEInequality (hypothesis)
Goal:
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 1 < sumInv {p, q, r}
hp3 : Membership.mem (γ := Finset ℕ+) (Finset.Iio 3) p
⊢ Admissible {p, q, r}
have hp3₁ : Membership.mem (γ := Multiset ℕ+) {1, 2} p
Tactic: conv at hp3 => change p ∈ ({1, 2} : Multiset ℕ+)
Cleared hypotheses: hp3
-- Lean 4 proof step from Mathlib.NumberTheory.ADEInequality (goal)
Goal:
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 1 < sumInv {p, q, r}
hp3 : Membership.mem (γ := Multiset ℕ+) {1, 2} p
⊢ Admissible {p, q, r}
have 0 : ∀ (hpq : 1 ≤ q) (H : 1 < sumInv {1, q, r}), Admissible {1, q, r}
Tactic: fin_cases hp3
Cleared hypotheses: p, hpq, H, hp3
-- Lean 4 proof step from Mathlib.NumberTheory.ADEInequality (goal)
Goal:
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 1 < sumInv {p, q, r}
hp3 : Membership.mem (γ := Multiset ℕ+) {1, 2} p
0 : ∀ (hpq : 1 ≤ q) (H : 1 < sumInv {1, q, r}), Admissible {1, q, r}
⊢ Admissible {p, q, r}
have 1 : ∀ (hpq : 2 ≤ q) (H : 1 < sumInv {2, q, r}), Admissible {2, q, r}
Tactic: fin_cases hp3
Cleared hypotheses: p, hpq, H, hp3
-- Lean 4 proof step from Mathlib.NumberTheory.ADEInequality (hypothesis)
Goal:
q r : ℕ+
hqr : q ≤ r
hpq : 2 ≤ q
H : 1 < sumInv {2, q, r}
⊢ Admissible {2, q, r}
have hq4 : q < 4
Tactic: have hq4 : q < 4 := lt_four hqr H
-- Lean 4 proof step from Mathlib.NumberTheory.ADEInequality (hypothesis)
Goal:
q r : ℕ+
hqr : q ≤ r
hpq : 2 ≤ q
H : 1 < sumInv {2, q, r}
hq4 : q < 4
⊢ Admissible {2, q, r}
have hq4₁ : Membership.mem (γ := Finset ℕ+) (Finset.Ico 2 4) q
Tactic: replace hq4 := Finset.mem_Ico.mpr ⟨hpq, hq4⟩
Cleared hypotheses: hq4
-- Lean 4 proof step from Mathlib.NumberTheory.ADEInequality (hypothesis)
Goal:
q r : ℕ+
hqr : q ≤ r
H : 1 < sumInv {2, q, r}
hq4 : Membership.mem (γ := Finset ℕ+) (Finset.Ico 2 4) q
⊢ Admissible {2, q, r}
have hq4₁ : Membership.mem (γ := Multiset ℕ+) {2, 3} q
Tactic: conv at hq4 => change q ∈ ({2, 3} : Multiset ℕ+)
Cleared hypotheses: hq4
-- Lean 4 proof step from Mathlib.NumberTheory.ADEInequality (goal)
Goal:
q r : ℕ+
hqr : q ≤ r
H : 1 < sumInv {2, q, r}
hq4 : Membership.mem (γ := Multiset ℕ+) {2, 3} q
⊢ Admissible {2, q, r}
have 1 : ∀ (hqr : 2 ≤ r) (H : 1 < sumInv {2, 2, r}), Admissible {2, 2, r}
Tactic: fin_cases hq4
Cleared hypotheses: q, hqr, H, hq4
-- Lean 4 proof step from Mathlib.NumberTheory.ADEInequality (goal)
Goal:
q r : ℕ+
hqr : q ≤ r
H : 1 < sumInv {2, q, r}
hq4 : Membership.mem (γ := Multiset ℕ+) {2, 3} q
1 : ∀ (hqr : 2 ≤ r) (H : 1 < sumInv {2, 2, r}), Admissible {2, 2, r}
⊢ Admissible {2, q, r}
have 1₁ : ∀ (hqr : 3 ≤ r) (H : 1 < sumInv {2, 3, r}), Admissible {2, 3, r}
Tactic: fin_cases hq4
Cleared hypotheses: q, hqr, H, hq4
-- Lean 4 proof step from Mathlib.NumberTheory.ADEInequality (hypothesis)
Goal:
r : ℕ+
hqr : 3 ≤ r
H : 1 < sumInv {2, 3, r}
⊢ Admissible {2, 3, r}
have hr6 : r < 6
Tactic: have hr6 : r < 6 := lt_six H
-- Lean 4 proof step from Mathlib.NumberTheory.ADEInequality (hypothesis)
Goal:
r : ℕ+
hqr : 3 ≤ r
H : 1 < sumInv {2, 3, r}
hr6 : r < 6
⊢ Admissible {2, 3, r}
have hr6₁ : Membership.mem (γ := Finset ℕ+) (Finset.Ico 3 6) r
Tactic: replace hr6 := Finset.mem_Ico.mpr ⟨hqr, hr6⟩
Cleared hypotheses: hr6
-- Lean 4 proof step from Mathlib.NumberTheory.ADEInequality (hypothesis)
Goal:
r : ℕ+
H : 1 < sumInv {2, 3, r}
hr6 : Membership.mem (γ := Finset ℕ+) (Finset.Ico 3 6) r
⊢ Admissible {2, 3, r}
have hr6₁ : Membership.mem (γ := Multiset ℕ+) {3, 4, 5} r
Tactic: conv at hr6 => change r ∈ ({3, 4, 5} : Multiset ℕ+)
Cleared hypotheses: hr6
-- Lean 4 proof step from Mathlib.NumberTheory.ADEInequality (goal)
Goal:
r : ℕ+
H : 1 < sumInv {2, 3, r}
hr6 : Membership.mem (γ := Multiset ℕ+) {3, 4, 5} r
⊢ Admissible {2, 3, r}
have 1 : ∀ (H : 1 < sumInv {2, 3, 3}), Admissible {2, 3, 3}
Tactic: fin_cases hr6
Cleared hypotheses: r, H, hr6
-- Lean 4 proof step from Mathlib.NumberTheory.ADEInequality (goal)
Goal:
r : ℕ+
H : 1 < sumInv {2, 3, r}
hr6 : Membership.mem (γ := Multiset ℕ+) {3, 4, 5} r
1 : ∀ (H : 1 < sumInv {2, 3, 3}), Admissible {2, 3, 3}
⊢ Admissible {2, 3, r}
have 1₁ : ∀ (H : 1 < sumInv {2, 3, 4}), Admissible {2, 3, 4}
Tactic: fin_cases hr6
Cleared hypotheses: r, H, hr6
-- Lean 4 proof step from Mathlib.NumberTheory.ADEInequality (goal)
Goal:
r : ℕ+
H : 1 < sumInv {2, 3, r}
hr6 : Membership.mem (γ := Multiset ℕ+) {3, 4, 5} r
1 : ∀ (H : 1 < sumInv {2, 3, 3}), Admissible {2, 3, 3}
h : ∀ (H : 1 < sumInv {2, 3, 4}), Admissible {2, 3, 4}
⊢ Admissible {2, 3, r}
have 1₁ : ∀ (H : 1 < sumInv {2, 3, 5}), Admissible {2, 3, 5}
Tactic: fin_cases hr6
Cleared hypotheses: r, H, hr6
-- Lean 4 proof step from Mathlib.NumberTheory.ADEInequality (hypothesis)
Goal:
p q r : ℕ+
hs : [p, q, r].SortedLE
h : [p, q, r].length = 3
H : 1 < sumInv (↑[p, q, r] : Multiset ℕ+)
⊢ Admissible (↑[p, q, r] : Multiset ℕ+)
have hqr : q ≤ r
Tactic: obtain ⟨⟨hpq, -⟩, hqr⟩ : (p ≤ q ∧ p ≤ r) ∧ q ≤ r := by simpa using hs.pairwise
-- Lean 4 proof step from Mathlib.NumberTheory.ADEInequality (hypothesis)
Goal:
p q r : ℕ+
hs : [p, q, r].SortedLE
h : [p, q, r].length = 3
H : 1 < sumInv (↑[p, q, r] : Multiset ℕ+)
hqr : q ≤ r
⊢ Admissible (↑[p, q, r] : Multiset ℕ+)
have hpq : p ≤ q
Tactic: obtain ⟨⟨hpq, -⟩, hqr⟩ : (p ≤ q ∧ p ≤ r) ∧ q ≤ r := by simpa using hs.pairwise
-- Lean 4 proof step from Mathlib.NumberTheory.ADEInequality (hypothesis)
Goal:
p q r : ℕ+
H : 1 < sumInv {p, q, r}
S : List ℕ+ := sort {p, q, r} fun (a b : ℕ+) ↦ a ≤ b
⊢ (∃ (q_1 : ℕ+) (r_1 : ℕ+), A' q_1 r_1 = {p, q, r}) ∨
    (∃ (r_1 : ℕ+), D' r_1 = {p, q, r}) ∨ E' 3 = {p, q, r} ∨ E' 4 = {p, q, r} ∨ E' 5 = {p, q, r}
have hS : S.SortedLE
Tactic: have hS : S.SortedLE := (pairwise_sort _ _).sortedLE
-- Lean 4 proof step from Mathlib.NumberTheory.ADEInequality (hypothesis)
Goal:
p q r : ℕ+
H : 1 < sumInv {p, q, r}
S : List ℕ+ := sort {p, q, r} fun (a b : ℕ+) ↦ a ≤ b
hS : S.SortedLE
⊢ (∃ (q_1 : ℕ+) (r_1 : ℕ+), A' q_1 r_1 = {p, q, r}) ∨
    (∃ (r_1 : ℕ+), D' r_1 = {p, q, r}) ∨ E' 3 = {p, q, r} ∨ E' 4 = {p, q, r} ∨ E' 5 = {p, q, r}
have hpqr : {p, q, r} = (↑S : Multiset ℕ+)
Tactic: have hpqr : ({p, q, r} : Multiset ℕ+) = S := (sort_eq {p, q, r} LE.le).symm
-- Lean 4 proof step from Mathlib.NumberTheory.ADEInequality (goal)
Goal:
p q r : ℕ+
H : 1 < sumInv {p, q, r}
S : List ℕ+ := sort {p, q, r} fun (a b : ℕ+) ↦ a ≤ b
hS : S.SortedLE
hpqr : {p, q, r} = (↑S : Multiset ℕ+)
⊢ (∃ (q_1 : ℕ+) (r_1 : ℕ+), A' q_1 r_1 = {p, q, r}) ∨
    (∃ (r_1 : ℕ+), D' r_1 = {p, q, r}) ∨ E' 3 = {p, q, r} ∨ E' 4 = {p, q, r} ∨ E' 5 = {p, q, r}
have rw : (∃ (q : ℕ+) (r : ℕ+), A' q r = (↑S : Multiset ℕ+)) ∨
  (∃ (r : ℕ+), D' r = (↑S : Multiset ℕ+)) ∨
    E' 3 = (↑S : Multiset ℕ+) ∨ E' 4 = (↑S : Multiset ℕ+) ∨ E' 5 = (↑S : Multiset ℕ+)
Tactic: rw [hpqr]
-- Lean 4 proof step from Mathlib.NumberTheory.ADEInequality (hypothesis)
Goal:
p q r : ℕ+
H : 1 < sumInv {p, q, r}
S : List ℕ+ := sort {p, q, r} fun (a b : ℕ+) ↦ a ≤ b
hS : S.SortedLE
hpqr : {p, q, r} = (↑S : Multiset ℕ+)
⊢ (∃ (q : ℕ+) (r : ℕ+), A' q r = (↑S : Multiset ℕ+)) ∨
    (∃ (r : ℕ+), D' r = (↑S : Multiset ℕ+)) ∨
      E' 3 = (↑S : Multiset ℕ+) ∨ E' 4 = (↑S : Multiset ℕ+) ∨ E' 5 = (↑S : Multiset ℕ+)
have H₁ : 1 < sumInv (↑S : Multiset ℕ+)
Tactic: rw [hpqr] at H
Cleared hypotheses: H, hS, hpqr
-- Lean 4 proof step from Mathlib.NumberTheory.ADEInequality (goal)
Goal:
p q r : ℕ+
S : List ℕ+ := sort {p, q, r} fun (a b : ℕ+) ↦ a ≤ b
H : 1 < sumInv (↑S : Multiset ℕ+)
hS : S.SortedLE
hpqr : {p, q, r} = (↑S : Multiset ℕ+)
⊢ (∃ (q : ℕ+) (r : ℕ+), A' q r = (↑S : Multiset ℕ+)) ∨
    (∃ (r : ℕ+), D' r = (↑S : Multiset ℕ+)) ∨
      E' 3 = (↑S : Multiset ℕ+) ∨ E' 4 = (↑S : Multiset ℕ+) ∨ E' 5 = (↑S : Multiset ℕ+)
have apply : S.length = 3
Tactic: apply admissible_of_one_lt_sumInv_aux hS _ H
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
m n : ℕ
⊢ ∀ᵐ (t : ℝ),
    t ∈ Set.Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) →
      Eq.{u_1 + 1} (α := 𝕜) (∑ k ∈ Icc m ⌊t⌋₊, c k) (∑ k ∈ Icc m n, c k)
have h : ∀ (t : ℝ) (h : Set.Ico (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) t = Set.Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) t)
  (ht : t ∈ Set.Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)),
  Eq.{u_1 + 1} (α := 𝕜) (∑ k ∈ Icc m ⌊t⌋₊, c k) (∑ k ∈ Icc m n, c k)
Tactic: filter_upwards [Ico_ae_eq_Icc] with t h ht
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
m n : ℕ
t : ℝ
h : Set.Ico (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) t = Set.Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) t
ht : t ∈ Set.Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ Eq.{u_1 + 1} (α := 𝕜) (∑ k ∈ Icc m ⌊t⌋₊, c k) (∑ k ∈ Icc m n, c k)
have h₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ k ∈ Icc m n, c k) (∑ k ∈ Icc m n, c k)
Tactic: rw [Nat.floor_eq_on_Ico _ _ (h.mpr ht)]
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc a b) volume
t₁ t₂ : ℝ
n : ℕ
h : t₁ ≤ t₂
h₁ : (↑n : ℝ) ≤ t₁
h₂ : t₂ ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
h₃ : a ≤ t₁
h₄ : t₂ ≤ b
⊢ ∫ (t : ℝ) in t₁..t₂, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k = (f t₂ - f t₁) * ∑ k ∈ Icc 0 n, c k
have h_inc₁ : Ι t₁ t₂ ⊆ Set.Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
Tactic: have h_inc₁ : Ι t₁ t₂ ⊆ Set.Icc n (n + 1) :=
    Set.uIoc_of_le h ▸ Set.Ioc_subset_Icc_self.trans <| Set.Icc_subset_Icc h₁ h₂
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc a b) volume
t₁ t₂ : ℝ
n : ℕ
h : t₁ ≤ t₂
h₁ : (↑n : ℝ) ≤ t₁
h₂ : t₂ ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
h₃ : a ≤ t₁
h₄ : t₂ ≤ b
h_inc₁ : Ι t₁ t₂ ⊆ Set.Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ ∫ (t : ℝ) in t₁..t₂, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k = (f t₂ - f t₁) * ∑ k ∈ Icc 0 n, c k
have h_inc₂ : [[t₁, t₂]] ⊆ Set.Icc a b
Tactic: have h_inc₂ : Set.uIcc t₁ t₂ ⊆ Set.Icc a b := Set.uIcc_of_le h ▸ Set.Icc_subset_Icc h₃ h₄
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc a b) volume
t₁ t₂ : ℝ
n : ℕ
h : t₁ ≤ t₂
h₁ : (↑n : ℝ) ≤ t₁
h₂ : t₂ ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
h₃ : a ≤ t₁
h₄ : t₂ ≤ b
h_inc₁ : Ι t₁ t₂ ⊆ Set.Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
h_inc₂ : [[t₁, t₂]] ⊆ Set.Icc a b
⊢ ∫ (t : ℝ) in t₁..t₂, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k = (f t₂ - f t₁) * ∑ k ∈ Icc 0 n, c k
have rw : Eq.{u_1 + 1} (α := 𝕜) (∫ (t : ℝ) in t₁..t₂, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k)
  (∫ (x : ℝ) in t₁..t₂, deriv f x * ∑ k ∈ Icc 0 n, c k)
Tactic: rw [← integral_deriv_eq_sub (fun t ht ↦ hf_diff t (h_inc₂ ht)),
      ← intervalIntegral.integral_mul_const]
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc a b) volume
t₁ t₂ : ℝ
n : ℕ
h : t₁ ≤ t₂
h₁ : (↑n : ℝ) ≤ t₁
h₂ : t₂ ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
h₃ : a ≤ t₁
h₄ : t₂ ≤ b
h_inc₁ : Ι t₁ t₂ ⊆ Set.Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
h_inc₂ : [[t₁, t₂]] ⊆ Set.Icc a b
rw :
  Eq.{u_1 + 1} (α := 𝕜) (∫ (t : ℝ) in t₁..t₂, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k)
    (∫ (x : ℝ) in t₁..t₂, deriv f x * ∑ k ∈ Icc 0 n, c k)
⊢ ∫ (t : ℝ) in t₁..t₂, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k = (f t₂ - f t₁) * ∑ k ∈ Icc 0 n, c k
have rw₁ : IntervalIntegrable (deriv f) volume t₁ t₂
Tactic: rw [← integral_deriv_eq_sub (fun t ht ↦ hf_diff t (h_inc₂ ht)),
      ← intervalIntegral.integral_mul_const]
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc a b) volume
t₁ t₂ : ℝ
n : ℕ
h : t₁ ≤ t₂
h₁ : (↑n : ℝ) ≤ t₁
h₂ : t₂ ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
h₃ : a ≤ t₁
h₄ : t₂ ≤ b
h_inc₁ : Ι t₁ t₂ ⊆ Set.Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
h_inc₂ : [[t₁, t₂]] ⊆ Set.Icc a b
⊢ Eq.{u_1 + 1} (α := 𝕜) (∫ (t : ℝ) in t₁..t₂, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k)
    (∫ (x : ℝ) in t₁..t₂, deriv f x * ∑ k ∈ Icc 0 n, c k)
have refine : ∀ᵐ (x : ℝ), x ∈ Ι t₁ t₂ → deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k = deriv f x * ∑ k ∈ Icc 0 n, c k
Tactic: refine integral_congr_ae ?_
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc a b) volume
t₁ t₂ : ℝ
n : ℕ
h : t₁ ≤ t₂
h₁ : (↑n : ℝ) ≤ t₁
h₂ : t₂ ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
h₃ : a ≤ t₁
h₄ : t₂ ≤ b
h_inc₁ : Ι t₁ t₂ ⊆ Set.Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
h_inc₂ : [[t₁, t₂]] ⊆ Set.Icc a b
⊢ ∀ᵐ (x : ℝ), x ∈ Ι t₁ t₂ → deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k = deriv f x * ∑ k ∈ Icc 0 n, c k
have h₅ : ∀ (t : ℝ)
  (h :
    t ∈ Set.Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) →
      Eq.{u_1 + 1} (α := 𝕜) (∑ k ∈ Icc 0 ⌊t⌋₊, c k) (∑ k ∈ Icc 0 n, c k))
  (h' : t ∈ Ι t₁ t₂), deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k = deriv f t * ∑ k ∈ Icc 0 n, c k
Tactic: filter_upwards [sumlocc c n] with t h h'
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc a b) volume
t₁ t₂ : ℝ
n : ℕ
h_1 : t₁ ≤ t₂
h₁ : (↑n : ℝ) ≤ t₁
h₂ : t₂ ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
h₃ : a ≤ t₁
h₄ : t₂ ≤ b
h_inc₁ : Ι t₁ t₂ ⊆ Set.Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
h_inc₂ : [[t₁, t₂]] ⊆ Set.Icc a b
t : ℝ
h :
  t ∈ Set.Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) →
    Eq.{u_1 + 1} (α := 𝕜) (∑ k ∈ Icc 0 ⌊t⌋₊, c k) (∑ k ∈ Icc 0 n, c k)
h' : t ∈ Ι t₁ t₂
⊢ deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k = deriv f t * ∑ k ∈ Icc 0 n, c k
have h₅ : deriv f t * ∑ k ∈ Icc 0 n, c k = deriv f t * ∑ k ∈ Icc 0 n, c k
Tactic: rw [h (h_inc₁ h')]
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc a b) volume
t₁ t₂ : ℝ
n : ℕ
h : t₁ ≤ t₂
h₁ : (↑n : ℝ) ≤ t₁
h₂ : t₂ ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
h₃ : a ≤ t₁
h₄ : t₂ ≤ b
h_inc₁ : Ι t₁ t₂ ⊆ Set.Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
h_inc₂ : [[t₁, t₂]] ⊆ Set.Icc a b
⊢ IntervalIntegrable (deriv f) volume t₁ t₂
have refine : Set.Icc t₁ t₂ ⊆ Set.Icc a b
Tactic: refine (intervalIntegrable_iff_integrableOn_Icc_of_le h).mpr (hf_int.mono_set ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
a b : ℝ
k : ℕ
hk : k ∈ Set.Ico (⌊a⌋₊ + 1) ⌊b⌋₊
⊢ a ≤ (↑k : ℝ) ∧ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 ≤ b
have left : a ≤ (↑k : ℝ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
a b : ℝ
k : ℕ
hk : k ∈ Set.Ico (⌊a⌋₊ + 1) ⌊b⌋₊
left : a ≤ (↑k : ℝ)
⊢ a ≤ (↑k : ℝ) ∧ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 ≤ b
have right : HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 ≤ b
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (hypothesis)
Goal:
a b : ℝ
k : ℕ
hk : k ∈ Set.Ico (⌊a⌋₊ + 1) ⌊b⌋₊
⊢ a ≤ (↑k : ℝ)
have this : ⌊a⌋₊ + 1 ≤ k
Tactic: have := (Set.mem_Ico.mp hk).1
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
a b : ℝ
k : ℕ
hk : k ∈ Set.Ico (⌊a⌋₊ + 1) ⌊b⌋₊
⊢ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 ≤ b
have right : k.succ ≤ ⌊b⌋₊
Tactic: rw [← Nat.cast_add_one, ← Nat.le_floor_iff' (Nat.succ_ne_zero k)]
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
a b : ℝ
k : ℕ
hk : k ∈ Ico (⌊a⌋₊ + 1) ⌊b⌋₊
⊢ k ∈ Set.Ico (⌊a⌋₊ + 1) ⌊b⌋₊
have rwa : k ∈ (↑(Ico (⌊a⌋₊ + 1) ⌊b⌋₊) : Set ℕ)
Tactic: rwa [← Finset.coe_Ico]
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (Set.Icc a b) volume
⊢ IntegrableOn.{0, u_1} (ε := 𝕜) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k)
    (Set.Icc a b) volume
have inl : ∀ (hab : a ≤ b),
  IntegrableOn.{0, u_1} (ε := 𝕜) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k)
    (Set.Icc a b) volume
Tactic: obtain hab | hab := le_or_gt a b
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (Set.Icc a b) volume
inl :
  ∀ (hab : a ≤ b),
    IntegrableOn.{0, u_1} (ε := 𝕜) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k)
      (Set.Icc a b) volume
⊢ IntegrableOn.{0, u_1} (ε := 𝕜) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k)
    (Set.Icc a b) volume
have inr : ∀ (hab : b < a),
  IntegrableOn.{0, u_1} (ε := 𝕜) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k)
    (Set.Icc a b) volume
Tactic: obtain hab | hab := le_or_gt a b
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (Set.Icc a b) volume
hab : a ≤ b
⊢ IntegrableOn.{0, u_1} (ε := 𝕜) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k)
    (Set.Icc a b) volume
have inl : ∀ (hb : ⌊a⌋₊ = ⌊b⌋₊),
  IntegrableOn.{0, u_1} (ε := 𝕜) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k)
    (Set.Icc a b) volume
Tactic: obtain hb | hb := eq_or_lt_of_le (Nat.floor_le_floor hab)
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (Set.Icc a b) volume
hab : a ≤ b
inl :
  ∀ (hb : ⌊a⌋₊ = ⌊b⌋₊),
    IntegrableOn.{0, u_1} (ε := 𝕜) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k)
      (Set.Icc a b) volume
⊢ IntegrableOn.{0, u_1} (ε := 𝕜) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k)
    (Set.Icc a b) volume
have inl₁ : ∀ (hb : ⌊a⌋₊ < ⌊b⌋₊),
  IntegrableOn.{0, u_1} (ε := 𝕜) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k)
    (Set.Icc a b) volume
Tactic: obtain hb | hb := eq_or_lt_of_le (Nat.floor_le_floor hab)
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ = ⌊b⌋₊
⊢ ∀ᵐ (t : ℝ), t ∈ Set.Icc a b → Eq.{u_1 + 1} (α := 𝕜) (∑ k ∈ Icc m ⌊a⌋₊, c k) (∑ k ∈ Icc m ⌊t⌋₊, c k)
have h : ∀ (t : ℝ)
  (ht₁ :
    t ∈ Set.Icc (↑⌊a⌋₊ : ℝ) (HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1) →
      Eq.{u_1 + 1} (α := 𝕜) (∑ k ∈ Icc m ⌊t⌋₊, c k) (∑ k ∈ Icc m ⌊a⌋₊, c k))
  (ht₂ : t ∈ Set.Icc a b), Eq.{u_1 + 1} (α := 𝕜) (∑ k ∈ Icc m ⌊a⌋₊, c k) (∑ k ∈ Icc m ⌊t⌋₊, c k)
Tactic: filter_upwards [sumlocc c ⌊a⌋₊] with t ht₁ ht₂
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ = ⌊b⌋₊
t : ℝ
ht₁ :
  t ∈ Set.Icc (↑⌊a⌋₊ : ℝ) (HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1) →
    Eq.{u_1 + 1} (α := 𝕜) (∑ k ∈ Icc m ⌊t⌋₊, c k) (∑ k ∈ Icc m ⌊a⌋₊, c k)
ht₂ : t ∈ Set.Icc a b
⊢ Eq.{u_1 + 1} (α := 𝕜) (∑ k ∈ Icc m ⌊a⌋₊, c k) (∑ k ∈ Icc m ⌊t⌋₊, c k)
have h : Eq.{u_1 + 1} (α := 𝕜) (∑ k ∈ Icc m ⌊a⌋₊, c k) (∑ k ∈ Icc m ⌊a⌋₊, c k)
Tactic: rw [ht₁ ⟨(Nat.floor_le ha).trans ht₂.1, hb ▸ ht₂.2.trans (Nat.lt_floor_add_one b).le⟩]
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ = ⌊b⌋₊
⊢ IntegrableOn.{0, u_1} (ε := 𝕜) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k)
    (Set.Icc a b) volume
have this : ∀ᵐ (t : ℝ), t ∈ Set.Icc a b → Eq.{u_1 + 1} (α := 𝕜) (∑ k ∈ Icc m ⌊a⌋₊, c k) (∑ k ∈ Icc m ⌊t⌋₊, c k)
Tactic: have : ∀ᵐ t, t ∈ Set.Icc a b → ∑ k ∈ Icc m ⌊a⌋₊, c k = ∑ k ∈ Icc m ⌊t⌋₊, c k := by
        filter_upwards [sumlocc c ⌊a⌋₊] with t ht₁ ht₂
        rw [ht₁ ⟨(Nat.floor_le ha).trans ht₂.1, hb ▸ ht₂.2.trans (Nat.lt_floor_add_one b).le⟩]