awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Oscillation (goal)
Goal:
E : Type u
F : Type v
inst : PseudoEMetricSpace F
inst_1 : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : (r : ℝ) → Set E := fun (r : ℝ) ↦ {x : E | ∃ a > r, ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
S_open : ∀ r > 0, IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (S r)
S_cover : K ⊆ ⋃ (r : ℝ), ⋃ (_ : r > 0), S r
S_antitone : ∀ (r₁ r₂ : ℝ), r₁ ≤ r₂ → S r₂ ⊆ S r₁
⊢ ∃ δ > 0, ∀ x ∈ K, ediam (f '' (eball x (ENNReal.ofReal δ) ∩ D)) ≤ ε
have obtain : ∀ (δ : ℝ) (δ0 : δ > 0) (hδ : K ⊆ S δ), ∃ δ > 0, ∀ x ∈ K, ediam (f '' (eball x (ENNReal.ofReal δ) ∩ D)) ≤ ε
Tactic: obtain ⟨δ, δ0, hδ⟩ : ∃ r > 0, K ⊆ S r := by
    obtain ⟨T, Tb, Tfin, hT⟩ := comp.elim_finite_subcover_image S_open S_cover
    by_cases T_nonempty : T.Nonempty
    · use Tfin.isWF.min T_nonempty, Tb (Tfin.isWF.min_mem T_nonempty)
      intro x hx
      obtain ⟨r, hr⟩ := mem_iUnion.1 (hT hx)
      simp only [mem_iUnion, exists_prop] at hr
      exact (S_antitone _ r (IsWF.min_le Tfin.isWF T_nonempty hr.1)) hr.2
    · rw [not_nonempty_iff_eq_empty] at T_nonempty
      use 1, one_pos, subset_trans hT (by simp [T_nonempty])
-- Lean 4 proof step from Mathlib.Analysis.Oscillation (goal)
Goal:
E : Type u
F : Type v
inst : PseudoEMetricSpace F
inst_1 : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : (r : ℝ) → Set E := fun (r : ℝ) ↦ {x : E | ∃ a > r, ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
S_open : ∀ r > 0, IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (S r)
S_cover : K ⊆ ⋃ (r : ℝ), ⋃ (_ : r > 0), S r
S_antitone : ∀ (r₁ r₂ : ℝ), r₁ ≤ r₂ → S r₂ ⊆ S r₁
δ : ℝ
δ0 : δ > 0
hδ : K ⊆ S δ
⊢ ∃ δ > 0, ∀ x ∈ K, ediam (f '' (eball x (ENNReal.ofReal δ) ∩ D)) ≤ ε
have right : ∀ x ∈ K, ediam (f '' (eball x (ENNReal.ofReal δ) ∩ D)) ≤ ε
Tactic: use δ, δ0
-- Lean 4 proof step from Mathlib.Analysis.Oscillation (goal)
Goal:
E : Type u
F : Type v
inst : PseudoEMetricSpace F
inst_1 : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : (r : ℝ) → Set E := fun (r : ℝ) ↦ {x : E | ∃ a > r, ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
S_open : ∀ r > 0, IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (S r)
S_cover : K ⊆ ⋃ (r : ℝ), ⋃ (_ : r > 0), S r
S_antitone : ∀ (r₁ r₂ : ℝ), r₁ ≤ r₂ → S r₂ ⊆ S r₁
δ : ℝ
δ0 : δ > 0
hδ : K ⊆ S δ
x : E
xK : x ∈ K
⊢ ediam (f '' (eball x (ENNReal.ofReal δ) ∩ D)) ≤ ε
have right : ∀ (a : ℝ) (δa : a > δ) (ha : ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε),
  ediam (f '' (eball x (ENNReal.ofReal δ) ∩ D)) ≤ ε
Tactic: obtain ⟨a, δa, ha⟩ := hδ xK
-- Lean 4 proof step from Mathlib.Analysis.Oscillation (goal)
Goal:
E : Type u
F : Type v
inst : PseudoEMetricSpace F
inst_1 : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : (r : ℝ) → Set E := fun (r : ℝ) ↦ {x : E | ∃ a > r, ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
S_open : ∀ r > 0, IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (S r)
S_cover : K ⊆ ⋃ (r : ℝ), ⋃ (_ : r > 0), S r
S_antitone : ∀ (r₁ r₂ : ℝ), r₁ ≤ r₂ → S r₂ ⊆ S r₁
δ : ℝ
δ0 : δ > 0
hδ : K ⊆ S δ
x : E
xK : x ∈ K
a : ℝ
δa : a > δ
ha : ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε
⊢ ediam (f '' (eball x (ENNReal.ofReal δ) ∩ D)) ≤ ε
have right : ediam (f '' (eball x (ENNReal.ofReal δ) ∩ D)) ≤ ediam (f '' (eball x (ENNReal.ofReal a) ∩ D))
Tactic: grw [← ha]
-- Lean 4 proof step from Mathlib.Analysis.Oscillation (hypothesis)
Goal:
E : Type u
F : Type v
inst : PseudoEMetricSpace F
inst_1 : PseudoEMetricSpace E
K : Set E
comp : IsCompact K
f : E → F
ε : ℝ≥0∞
hK : ∀ x ∈ K, oscillation f x < ε
⊢ ∃ δ > 0, ∀ x ∈ K, ediam (f '' eball x (ENNReal.ofReal δ)) ≤ ε
have hK₁ : ∀ x ∈ K, oscillationWithin f univ x < ε
Tactic: simp only [← oscillationWithin_univ_eq_oscillation] at hK
Cleared hypotheses: hK
-- Lean 4 proof step from Mathlib.Analysis.Oscillation (goal)
Goal:
E : Type u
F : Type v
inst : PseudoEMetricSpace F
inst_1 : PseudoEMetricSpace E
K : Set E
comp : IsCompact K
f : E → F
ε : ℝ≥0∞
hK : ∀ x ∈ K, oscillationWithin f univ x < ε
⊢ ∃ δ > 0, ∀ x ∈ K, ediam (f '' eball x (ENNReal.ofReal δ)) ≤ ε
have h : ∀ (x : ℝ), ∀ a ∈ K, eball a (ENNReal.ofReal x) ∩ univ = eball a (ENNReal.ofReal x)
Tactic: convert! ← comp.uniform_oscillationWithin hK
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : Monotone u
n : ℕ
ihn : LE.le.{u_1} (α := M) (∑ k ∈ Ico (u 0) (u n), f k) (∑ k ∈ range n, (u (k + 1) - u k) • f (u k))
this : ∑ k ∈ Ico (u n) (u (n + 1)), f k ≤ (u (n + 1) - u n) • f (u n)
⊢ LE.le.{u_1} (α := M) (∑ k ∈ Ico (u 0) (u (n + 1)), f k) (∑ k ∈ range (n + 1), (u (k + 1) - u k) • f (u k))
have rw : HAdd.hAdd (α := M) (∑ i ∈ Ico (u 0) (u n), f i) (∑ i ∈ Ico (u n) (u (n + 1)), f i) ≤
  ∑ x ∈ range n, (u (x + 1) - u x) • f (u x) + (u (n + 1) - u n) • f (u n)
Tactic: rw [sum_range_succ, ← sum_Ico_consecutive]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : Monotone u
n : ℕ
ihn : LE.le.{u_1} (α := M) (∑ k ∈ Ico (u 0) (u n), f k) (∑ k ∈ range n, (u (k + 1) - u k) • f (u k))
this : ∑ k ∈ Ico (u n) (u (n + 1)), f k ≤ (u (n + 1) - u n) • f (u n)
rw :
  HAdd.hAdd (α := M) (∑ i ∈ Ico (u 0) (u n), f i) (∑ i ∈ Ico (u n) (u (n + 1)), f i) ≤
    ∑ x ∈ range n, (u (x + 1) - u x) • f (u x) + (u (n + 1) - u n) • f (u n)
n₁ : ℕ
⊢ LE.le.{u_1} (α := M) (∑ k ∈ Ico (u 0) (u (n + 1)), f k) (∑ k ∈ range (n + 1), (u (k + 1) - u k) • f (u k))
have hmn : u 0 ≤ u n
Tactic: rw [sum_range_succ, ← sum_Ico_consecutive]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : Monotone u
n : ℕ
ihn : LE.le.{u_1} (α := M) (∑ k ∈ Ico (u 0) (u n), f k) (∑ k ∈ range n, (u (k + 1) - u k) • f (u k))
this : ∑ k ∈ Ico (u n) (u (n + 1)), f k ≤ (u (n + 1) - u n) • f (u n)
rw :
  HAdd.hAdd (α := M) (∑ i ∈ Ico (u 0) (u n), f i) (∑ i ∈ Ico (u n) (u (n + 1)), f i) ≤
    ∑ x ∈ range n, (u (x + 1) - u x) • f (u x) + (u (n + 1) - u n) • f (u n)
n₁ : ℕ
hmn : u 0 ≤ u n
⊢ LE.le.{u_1} (α := M) (∑ k ∈ Ico (u 0) (u (n + 1)), f k) (∑ k ∈ range (n + 1), (u (k + 1) - u k) • f (u k))
have hnk : u n ≤ u (n + 1)
Tactic: rw [sum_range_succ, ← sum_Ico_consecutive]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : Monotone u
n : ℕ
ihn : LE.le.{u_1} (α := M) (∑ k ∈ Ico (u 0) (u n), f k) (∑ k ∈ range n, (u (k + 1) - u k) • f (u k))
⊢ LE.le.{u_1} (α := M) (∑ k ∈ Ico (u 0) (u (n + 1)), f k) (∑ k ∈ range (n + 1), (u (k + 1) - u k) • f (u k))
have succ : ∑ k ∈ Ico (u n) (u (n + 1)), f k ≤ (u (n + 1) - u n) • f (u n)
Tactic: suffices (∑ k ∈ Ico (u n) (u (n + 1)), f k) ≤ (u (n + 1) - u n) • f (u n) by
      rw [sum_range_succ, ← sum_Ico_consecutive]
      · exact add_le_add ihn this
      exacts [hu n.zero_le, hu n.le_succ]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (hypothesis)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : Monotone u
n : ℕ
ihn : LE.le.{u_1} (α := M) (∑ k ∈ Ico (u 0) (u n), f k) (∑ k ∈ range n, (u (k + 1) - u k) • f (u k))
⊢ ∑ k ∈ Ico (u n) (u (n + 1)), f k ≤ (u (n + 1) - u n) • f (u n)
have this : ∀ k ∈ Ico (u n) (u (n + 1)), f k ≤ f (u n)
Tactic: have : ∀ k ∈ Ico (u n) (u (n + 1)), f k ≤ f (u n) := fun k hk =>
      hf (Nat.succ_le_of_lt (h_pos n)) (mem_Ico.mp hk).1
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : Monotone u
n : ℕ
ihn : LE.le.{u_1} (α := M) (∑ k ∈ Ico (u 0) (u n), f k) (∑ k ∈ range n, (u (k + 1) - u k) • f (u k))
this : ∀ k ∈ Ico (u n) (u (n + 1)), f k ≤ f (u n)
⊢ ∑ k ∈ Ico (u n) (u (n + 1)), f k ≤ (u (n + 1) - u n) • f (u n)
have h : (u (n + 1) - u n) • f (u n) = ∑ i ∈ Ico (u n) (u (n + 1)), f (u n)
Tactic: convert! sum_le_sum this
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : Monotone u
n : ℕ
⊢ LE.le.{u_1} (α := M) (∑ k ∈ Ico (u 0) (u n), f k) (∑ k ∈ range n, (u (k + 1) - u k) • f (u k))
have zero : LE.le.{u_1} (α := M) (∑ k ∈ Ico (u 0) (u 0), f k) (∑ k ∈ range 0, (u (k + 1) - u k) • f (u k))
Tactic: induction n with
  | zero => simp
  | succ n ihn =>
    suffices (∑ k ∈ Ico (u n) (u (n + 1)), f k) ≤ (u (n + 1) - u n) • f (u n) by
      rw [sum_range_succ, ← sum_Ico_consecutive]
      · exact add_le_add ihn this
      exacts [hu n.zero_le, hu n.le_succ]
    have : ∀ k ∈ Ico (u n) (u (n + 1)), f k ≤ f (u n) := fun k hk =>
      hf (Nat.succ_le_of_lt (h_pos n)) (mem_Ico.mp hk).1
    convert! sum_le_sum this
    simp
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : Monotone u
n : ℕ
zero : LE.le.{u_1} (α := M) (∑ k ∈ Ico (u 0) (u 0), f k) (∑ k ∈ range 0, (u (k + 1) - u k) • f (u k))
⊢ LE.le.{u_1} (α := M) (∑ k ∈ Ico (u 0) (u n), f k) (∑ k ∈ range n, (u (k + 1) - u k) • f (u k))
have succ : ∀ (n : ℕ) (ihn : LE.le.{u_1} (α := M) (∑ k ∈ Ico (u 0) (u n), f k) (∑ k ∈ range n, (u (k + 1) - u k) • f (u k))),
  LE.le.{u_1} (α := M) (∑ k ∈ Ico (u 0) (u (n + 1)), f k) (∑ k ∈ range (n + 1), (u (k + 1) - u k) • f (u k))
Tactic: induction n with
  | zero => simp
  | succ n ihn =>
    suffices (∑ k ∈ Ico (u n) (u (n + 1)), f k) ≤ (u (n + 1) - u n) • f (u n) by
      rw [sum_range_succ, ← sum_Ico_consecutive]
      · exact add_le_add ihn this
      exacts [hu n.zero_le, hu n.le_succ]
    have : ∀ k ∈ Ico (u n) (u (n + 1)), f k ≤ f (u n) := fun k hk =>
      hf (Nat.succ_le_of_lt (h_pos n)) (mem_Ico.mp hk).1
    convert! sum_le_sum this
    simp
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
f : ℕ → M
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
n : ℕ
⊢ LE.le.{u_1} (α := M) (∑ k ∈ Ico 1 (HPow.hPow (α := ℕ) 2 n), f k)
    (∑ k ∈ range n, HPow.hPow (α := ℕ) 2 k • f (HPow.hPow (α := ℕ) 2 k))
have h : ∀ x ∈ range n,
  HPow.hPow (α := ℕ) 2 x • f (HPow.hPow (α := ℕ) 2 x) =
    (HPow.hPow (α := ℕ) 2 (x + 1) - HPow.hPow (α := ℕ) 2 x) • f (HPow.hPow (α := ℕ) 2 x)
Tactic: convert!
    le_sum_schlomilch' hf (fun n => pow_pos zero_lt_two n)
      (fun m n hm => pow_right_mono₀ one_le_two hm) n using 2
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : Monotone u
n : ℕ
⊢ ∑ k ∈ range (u n), f k ≤ HAdd.hAdd (α := M) (∑ k ∈ range (u 0), f k) (∑ k ∈ range n, (u (k + 1) - u k) • f (u k))
have grw : ∑ k ∈ range (u n), f k ≤ HAdd.hAdd (α := M) (∑ k ∈ range (u 0), f k) (∑ k ∈ Ico (u 0) (u n), f k)
Tactic: grw [← le_sum_schlomilch' hf h_pos hu n, ← sum_range_add_sum_Ico _ (hu n.zero_le)]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : Monotone u
n : ℕ
grw : ∑ k ∈ range (u n), f k ≤ HAdd.hAdd (α := M) (∑ k ∈ range (u 0), f k) (∑ k ∈ Ico (u 0) (u n), f k)
⊢ ∑ k ∈ range (u n), f k ≤ HAdd.hAdd (α := M) (∑ k ∈ range (u 0), f k) (∑ k ∈ range n, (u (k + 1) - u k) • f (u k))
have grw₁ : HAdd.hAdd (α := M) (∑ k ∈ range (u 0), f k) (∑ k ∈ Ico (u 0) (u n), f k) ≤
  HAdd.hAdd (α := M) (∑ k ∈ range (u 0), f k) (∑ k ∈ Ico (u 0) (u n), f k)
Tactic: grw [← le_sum_schlomilch' hf h_pos hu n, ← sum_range_add_sum_Ico _ (hu n.zero_le)]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
f : ℕ → M
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
n : ℕ
⊢ ∑ k ∈ range (HPow.hPow (α := ℕ) 2 n), f k ≤ f 0 + ∑ k ∈ range n, HPow.hPow (α := ℕ) 2 k • f (HPow.hPow (α := ℕ) 2 k)
have grw : ∑ k ∈ range (HPow.hPow (α := ℕ) 2 n), f k ≤ f 0 + ∑ k ∈ Ico 1 (HPow.hPow (α := ℕ) 2 n), f k
Tactic: grw [← le_sum_condensed' hf n, ← sum_range_add_sum_Ico _ n.one_le_two_pow, sum_range_succ,
    sum_range_zero, zero_add]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
f : ℕ → M
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
n : ℕ
grw : ∑ k ∈ range (HPow.hPow (α := ℕ) 2 n), f k ≤ f 0 + ∑ k ∈ Ico 1 (HPow.hPow (α := ℕ) 2 n), f k
⊢ ∑ k ∈ range (HPow.hPow (α := ℕ) 2 n), f k ≤ f 0 + ∑ k ∈ range n, HPow.hPow (α := ℕ) 2 k • f (HPow.hPow (α := ℕ) 2 k)
have grw₁ : HAdd.hAdd (α := M) (∑ k ∈ range 1, f k) (∑ k ∈ Ico 1 (HPow.hPow (α := ℕ) 2 n), f k) ≤
  f 0 + ∑ k ∈ Ico 1 (HPow.hPow (α := ℕ) 2 n), f k
Tactic: grw [← le_sum_condensed' hf n, ← sum_range_add_sum_Ico _ n.one_le_two_pow, sum_range_succ,
    sum_range_zero, zero_add]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
f : ℕ → M
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
n : ℕ
grw : ∑ k ∈ range (HPow.hPow (α := ℕ) 2 n), f k ≤ f 0 + ∑ k ∈ Ico 1 (HPow.hPow (α := ℕ) 2 n), f k
grw₁ :
  HAdd.hAdd (α := M) (∑ k ∈ range 1, f k) (∑ k ∈ Ico 1 (HPow.hPow (α := ℕ) 2 n), f k) ≤
    f 0 + ∑ k ∈ Ico 1 (HPow.hPow (α := ℕ) 2 n), f k
⊢ ∑ k ∈ range (HPow.hPow (α := ℕ) 2 n), f k ≤ f 0 + ∑ k ∈ range n, HPow.hPow (α := ℕ) 2 k • f (HPow.hPow (α := ℕ) 2 k)
have grw₂ : ∑ x ∈ range 0, f x + f 0 + ∑ k ∈ Ico 1 (HPow.hPow (α := ℕ) 2 n), f k ≤ f 0 + ∑ k ∈ Ico 1 (HPow.hPow (α := ℕ) 2 n), f k
Tactic: grw [← le_sum_condensed' hf n, ← sum_range_add_sum_Ico _ n.one_le_two_pow, sum_range_succ,
    sum_range_zero, zero_add]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
f : ℕ → M
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
n : ℕ
grw : ∑ k ∈ range (HPow.hPow (α := ℕ) 2 n), f k ≤ f 0 + ∑ k ∈ Ico 1 (HPow.hPow (α := ℕ) 2 n), f k
grw₁ :
  HAdd.hAdd (α := M) (∑ k ∈ range 1, f k) (∑ k ∈ Ico 1 (HPow.hPow (α := ℕ) 2 n), f k) ≤
    f 0 + ∑ k ∈ Ico 1 (HPow.hPow (α := ℕ) 2 n), f k
grw₂ :
  ∑ x ∈ range 0, f x + f 0 + ∑ k ∈ Ico 1 (HPow.hPow (α := ℕ) 2 n), f k ≤ f 0 + ∑ k ∈ Ico 1 (HPow.hPow (α := ℕ) 2 n), f k
⊢ ∑ k ∈ range (HPow.hPow (α := ℕ) 2 n), f k ≤ f 0 + ∑ k ∈ range n, HPow.hPow (α := ℕ) 2 k • f (HPow.hPow (α := ℕ) 2 k)
have grw₃ : 0 + f 0 + ∑ k ∈ Ico 1 (HPow.hPow (α := ℕ) 2 n), f k ≤ f 0 + ∑ k ∈ Ico 1 (HPow.hPow (α := ℕ) 2 n), f k
Tactic: grw [← le_sum_condensed' hf n, ← sum_range_add_sum_Ico _ n.one_le_two_pow, sum_range_succ,
    sum_range_zero, zero_add]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
f : ℕ → M
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
n : ℕ
grw : ∑ k ∈ range (HPow.hPow (α := ℕ) 2 n), f k ≤ f 0 + ∑ k ∈ Ico 1 (HPow.hPow (α := ℕ) 2 n), f k
grw₁ :
  HAdd.hAdd (α := M) (∑ k ∈ range 1, f k) (∑ k ∈ Ico 1 (HPow.hPow (α := ℕ) 2 n), f k) ≤
    f 0 + ∑ k ∈ Ico 1 (HPow.hPow (α := ℕ) 2 n), f k
grw₂ :
  ∑ x ∈ range 0, f x + f 0 + ∑ k ∈ Ico 1 (HPow.hPow (α := ℕ) 2 n), f k ≤ f 0 + ∑ k ∈ Ico 1 (HPow.hPow (α := ℕ) 2 n), f k
grw₃ : 0 + f 0 + ∑ k ∈ Ico 1 (HPow.hPow (α := ℕ) 2 n), f k ≤ f 0 + ∑ k ∈ Ico 1 (HPow.hPow (α := ℕ) 2 n), f k
⊢ ∑ k ∈ range (HPow.hPow (α := ℕ) 2 n), f k ≤ f 0 + ∑ k ∈ range n, HPow.hPow (α := ℕ) 2 k • f (HPow.hPow (α := ℕ) 2 k)
have grw₄ : f 0 + ∑ k ∈ Ico 1 (HPow.hPow (α := ℕ) 2 n), f k ≤ f 0 + ∑ k ∈ Ico 1 (HPow.hPow (α := ℕ) 2 n), f k
Tactic: grw [← le_sum_condensed' hf n, ← sum_range_add_sum_Ico _ n.one_le_two_pow, sum_range_succ,
    sum_range_zero, zero_add]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : Monotone u
n : ℕ
ihn : LE.le.{u_1} (α := M) (∑ k ∈ range n, (u (k + 1) - u k) • f (u (k + 1))) (∑ k ∈ Ico (u 0 + 1) (u n + 1), f k)
this : (u (n + 1) - u n) • f (u (n + 1)) ≤ ∑ k ∈ Ico (u n + 1) (u (n + 1) + 1), f k
⊢ LE.le.{u_1} (α := M) (∑ k ∈ range (n + 1), (u (k + 1) - u k) • f (u (k + 1)))
    (∑ k ∈ Ico (u 0 + 1) (u (n + 1) + 1), f k)
have rw : ∑ x ∈ range n, (u (x + 1) - u x) • f (u (x + 1)) + (u (n + 1) - u n) • f (u (n + 1)) ≤
  HAdd.hAdd (α := M) (∑ i ∈ Ico (u 0 + 1) (u n + 1), f i) (∑ i ∈ Ico (u n + 1) (u (n + 1) + 1), f i)
Tactic: rw [sum_range_succ, ← sum_Ico_consecutive]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : Monotone u
n : ℕ
ihn : LE.le.{u_1} (α := M) (∑ k ∈ range n, (u (k + 1) - u k) • f (u (k + 1))) (∑ k ∈ Ico (u 0 + 1) (u n + 1), f k)
this : (u (n + 1) - u n) • f (u (n + 1)) ≤ ∑ k ∈ Ico (u n + 1) (u (n + 1) + 1), f k
rw :
  ∑ x ∈ range n, (u (x + 1) - u x) • f (u (x + 1)) + (u (n + 1) - u n) • f (u (n + 1)) ≤
    HAdd.hAdd (α := M) (∑ i ∈ Ico (u 0 + 1) (u n + 1), f i) (∑ i ∈ Ico (u n + 1) (u (n + 1) + 1), f i)
n₁ : ℕ
⊢ LE.le.{u_1} (α := M) (∑ k ∈ range (n + 1), (u (k + 1) - u k) • f (u (k + 1)))
    (∑ k ∈ Ico (u 0 + 1) (u (n + 1) + 1), f k)
have hmn : u 0 + 1 ≤ u n + 1
Tactic: rw [sum_range_succ, ← sum_Ico_consecutive]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : Monotone u
n : ℕ
ihn : LE.le.{u_1} (α := M) (∑ k ∈ range n, (u (k + 1) - u k) • f (u (k + 1))) (∑ k ∈ Ico (u 0 + 1) (u n + 1), f k)
this : (u (n + 1) - u n) • f (u (n + 1)) ≤ ∑ k ∈ Ico (u n + 1) (u (n + 1) + 1), f k
rw :
  ∑ x ∈ range n, (u (x + 1) - u x) • f (u (x + 1)) + (u (n + 1) - u n) • f (u (n + 1)) ≤
    HAdd.hAdd (α := M) (∑ i ∈ Ico (u 0 + 1) (u n + 1), f i) (∑ i ∈ Ico (u n + 1) (u (n + 1) + 1), f i)
n₁ : ℕ
hmn : u 0 + 1 ≤ u n + 1
⊢ LE.le.{u_1} (α := M) (∑ k ∈ range (n + 1), (u (k + 1) - u k) • f (u (k + 1)))
    (∑ k ∈ Ico (u 0 + 1) (u (n + 1) + 1), f k)
have hnk : u n + 1 ≤ u (n + 1) + 1
Tactic: rw [sum_range_succ, ← sum_Ico_consecutive]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : Monotone u
n : ℕ
ihn : LE.le.{u_1} (α := M) (∑ k ∈ range n, (u (k + 1) - u k) • f (u (k + 1))) (∑ k ∈ Ico (u 0 + 1) (u n + 1), f k)
⊢ LE.le.{u_1} (α := M) (∑ k ∈ range (n + 1), (u (k + 1) - u k) • f (u (k + 1)))
    (∑ k ∈ Ico (u 0 + 1) (u (n + 1) + 1), f k)
have succ : (u (n + 1) - u n) • f (u (n + 1)) ≤ ∑ k ∈ Ico (u n + 1) (u (n + 1) + 1), f k
Tactic: suffices (u (n + 1) - u n) • f (u (n + 1)) ≤ ∑ k ∈ Ico (u n + 1) (u (n + 1) + 1), f k by
      rw [sum_range_succ, ← sum_Ico_consecutive]
      exacts [add_le_add ihn this,
        (add_le_add_left (hu n.zero_le) _ : u 0 + 1 ≤ u n + 1),
        add_le_add_left (hu n.le_succ) _]
-- Lean 4 proof step from Mathlib.Analysis.PSeries (hypothesis)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : Monotone u
n : ℕ
ihn : LE.le.{u_1} (α := M) (∑ k ∈ range n, (u (k + 1) - u k) • f (u (k + 1))) (∑ k ∈ Ico (u 0 + 1) (u n + 1), f k)
⊢ (u (n + 1) - u n) • f (u (n + 1)) ≤ ∑ k ∈ Ico (u n + 1) (u (n + 1) + 1), f k
have this : ∀ k ∈ Ico (u n + 1) (u (n + 1) + 1), f (u (n + 1)) ≤ f k
Tactic: have : ∀ k ∈ Ico (u n + 1) (u (n + 1) + 1), f (u (n + 1)) ≤ f k := fun k hk =>
      hf (Nat.lt_of_le_of_lt (Nat.succ_le_of_lt (h_pos n)) <| (Nat.lt_succ_of_le le_rfl).trans_le
        (mem_Ico.mp hk).1) (Nat.le_of_lt_succ <| (mem_Ico.mp hk).2)
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : Monotone u
n : ℕ
ihn : LE.le.{u_1} (α := M) (∑ k ∈ range n, (u (k + 1) - u k) • f (u (k + 1))) (∑ k ∈ Ico (u 0 + 1) (u n + 1), f k)
this : ∀ k ∈ Ico (u n + 1) (u (n + 1) + 1), f (u (n + 1)) ≤ f k
⊢ (u (n + 1) - u n) • f (u (n + 1)) ≤ ∑ k ∈ Ico (u n + 1) (u (n + 1) + 1), f k
have h : (u (n + 1) - u n) • f (u (n + 1)) = ∑ i ∈ Ico (u n + 1) (u (n + 1) + 1), f (u (n + 1))
Tactic: convert! sum_le_sum this
-- Lean 4 proof step from Mathlib.Analysis.PSeries (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : Monotone u
n : ℕ
⊢ LE.le.{u_1} (α := M) (∑ k ∈ range n, (u (k + 1) - u k) • f (u (k + 1))) (∑ k ∈ Ico (u 0 + 1) (u n + 1), f k)
have zero : LE.le.{u_1} (α := M) (∑ k ∈ range 0, (u (k + 1) - u k) • f (u (k + 1))) (∑ k ∈ Ico (u 0 + 1) (u 0 + 1), f k)
Tactic: induction n with
  | zero => simp
  | succ n ihn =>
    suffices (u (n + 1) - u n) • f (u (n + 1)) ≤ ∑ k ∈ Ico (u n + 1) (u (n + 1) + 1), f k by
      rw [sum_range_succ, ← sum_Ico_consecutive]
      exacts [add_le_add ihn this,
        (add_le_add_left (hu n.zero_le) _ : u 0 + 1 ≤ u n + 1),
        add_le_add_left (hu n.le_succ) _]
    have : ∀ k ∈ Ico (u n + 1) (u (n + 1) + 1), f (u (n + 1)) ≤ f k := fun k hk =>
      hf (Nat.lt_of_le_of_lt (Nat.succ_le_of_lt (h_pos n)) <| (Nat.lt_succ_of_le le_rfl).trans_le
        (mem_Ico.mp hk).1) (Nat.le_of_lt_succ <| (mem_Ico.mp hk).2)
    convert! sum_le_sum this
    simp
Cleared hypotheses: n