From 6a2848b114cc8f04f8656e1eba4315ec058a3fc9 Mon Sep 17 00:00:00 2001 From: Abdullah Date: Tue, 26 Nov 2024 14:09:12 +0000 Subject: [PATCH] fixed typo --- MIL/C02_Basics/S03_Using_Theorems_and_Lemmas.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/MIL/C02_Basics/S03_Using_Theorems_and_Lemmas.lean b/MIL/C02_Basics/S03_Using_Theorems_and_Lemmas.lean index 416dddb..e05ada3 100644 --- a/MIL/C02_Basics/S03_Using_Theorems_and_Lemmas.lean +++ b/MIL/C02_Basics/S03_Using_Theorems_and_Lemmas.lean @@ -93,7 +93,7 @@ within the block introduced by the dot, only one goal is visible, and it must be completed before the end of the block. Here we end the first block by starting a new one with another dot. We could just as well have decreased the indentation. -In the fourth example and in the last example, +In the third example and in the last example, we avoid going into tactic mode entirely: ``le_trans h₀ h₁`` and ``le_refl x`` are the proof terms we need.