From bf7be1f52fa3cd1a6b68b82518616f9f32f4c7ff Mon Sep 17 00:00:00 2001 From: Aayush Rajasekaran Date: Mon, 23 Feb 2026 21:12:20 -0500 Subject: [PATCH] feat(L18Pset): drop unnecessary hypotheses --- Game/Levels/L18Pset/L06.lean | 2 +- Game/Levels/L18Pset/L07.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Game/Levels/L18Pset/L06.lean b/Game/Levels/L18Pset/L06.lean index 5a470b3..94b8a37 100644 --- a/Game/Levels/L18Pset/L06.lean +++ b/Game/Levels/L18Pset/L06.lean @@ -15,7 +15,7 @@ DisabledTheorem MonotoneSeriesEven /-- Prove `MonotoneSeriesEven` -/ -Statement {a : ℕ → ℝ} (ha : Antitone a) (apos : ∀ n, 0 ≤ a n) : +Statement {a : ℕ → ℝ} (ha : Antitone a) : Monotone (fun n ↦ ∑ k ∈ range (2 * n), (-1)^k * a k) := by apply Monotone_of_succ intro n diff --git a/Game/Levels/L18Pset/L07.lean b/Game/Levels/L18Pset/L07.lean index b92f4a0..80df2d6 100644 --- a/Game/Levels/L18Pset/L07.lean +++ b/Game/Levels/L18Pset/L07.lean @@ -17,7 +17,7 @@ DisabledTheorem AntitoneSeriesOdd /-- Prove `AntitoneSeriesOdd` -/ -Statement {a : ℕ → ℝ} (ha : Antitone a) (apos : ∀ n, 0 ≤ a n) : Antitone (fun n ↦ ∑ k ∈ range (2 * n + 1), (-1)^k * a k) := by +Statement {a : ℕ → ℝ} (ha : Antitone a) : Antitone (fun n ↦ ∑ k ∈ range (2 * n + 1), (-1)^k * a k) := by apply Antitone_of_succ intro n induction' n with n hn