From b210de95ad2d1bc4ebc5c1863cdaa49b2940ae5e Mon Sep 17 00:00:00 2001
From: GitHub Action <action@github.com>
Date: Sun, 23 Jun 2024 19:54:06 +0000
Subject: [PATCH] generated by GitHub Action

---
 Tutorial/Advanced/Analysis/Lecture1.lean | 2 --
 Tutorial/Basic/Lecture1.lean             | 2 +-
 2 files changed, 1 insertion(+), 3 deletions(-)

diff --git a/Tutorial/Advanced/Analysis/Lecture1.lean b/Tutorial/Advanced/Analysis/Lecture1.lean
index 7b0525b..caa7dae 100644
--- a/Tutorial/Advanced/Analysis/Lecture1.lean
+++ b/Tutorial/Advanced/Analysis/Lecture1.lean
@@ -265,8 +265,6 @@ theorem HasDerivAt.mul {f : ℝ → ℝ} (hf : HasDerivAt f f' a) (hg : HasDeriv
     case eq4 =>
       sorry
 
--- 次の問題で使うかも？
-#check Nat.succ_eq_add_one
 
 /-- 単項式の微分 -/
 theorem hasDerivAt_pow (n : ℕ) (a : ℝ) :
diff --git a/Tutorial/Basic/Lecture1.lean b/Tutorial/Basic/Lecture1.lean
index 776c5f7..8090111 100644
--- a/Tutorial/Basic/Lecture1.lean
+++ b/Tutorial/Basic/Lecture1.lean
@@ -1,4 +1,4 @@
-import Std
+import Batteries
 
 /- # 遊び方 -/