From 0f9c909817b4e0672d0bb04aa1cfdf67aa0d8536 Mon Sep 17 00:00:00 2001 From: Kent Van Vels Date: Sat, 11 Apr 2026 19:04:48 -0400 Subject: [PATCH 1/2] added an import of Section_3_3 in Section_3_5 so we have access to function.import --- Analysis/Section_3_6.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Analysis/Section_3_6.lean b/Analysis/Section_3_6.lean index d53d28db..b5a171e1 100644 --- a/Analysis/Section_3_6.lean +++ b/Analysis/Section_3_6.lean @@ -1,4 +1,5 @@ import Mathlib.Tactic +import Analysis.Section_3_3 import Analysis.Section_3_5 /-! From 751dde8d4e01902fc36220d18616dd9aa9bf081b Mon Sep 17 00:00:00 2001 From: Kent Van Vels Date: Sat, 11 Apr 2026 20:19:14 -0400 Subject: [PATCH 2/2] test to see if changing comments messes up verso documentation --- Analysis/Appendix_A_1.lean | 12 +++++++++--- Analysis/Section_2_1.lean | 24 ++++++++++-------------- Analysis/Section_2_2.lean | 31 ++++++++++++++++--------------- 3 files changed, 35 insertions(+), 32 deletions(-) diff --git a/Analysis/Appendix_A_1.lean b/Analysis/Appendix_A_1.lean index cba37ad1..562b763f 100644 --- a/Analysis/Appendix_A_1.lean +++ b/Analysis/Appendix_A_1.lean @@ -8,7 +8,11 @@ An introduction to mathematical statements. Showcases some basic tactics and Le -/ --- Example A.1.1. What the textbook calls "statements" are objects of type `Prop` in Lean. Also, in Lean we tend to assign "junk" values to expressions that might normally be considered undefined, so discussions regarding undefined terms in the textbook should be adjusted accordingly. +/- Example A.1.1. What + the textbook calls "statements" are objects of type `Prop` in Lean. + Also, in Lean we tend to assign "junk" values to expressions that might normally be + considered undefined, so discussions regarding undefined + terms in the textbook should be adjusted accordingly. -/ #check 2+2=4 #check 2+2=5 @@ -186,7 +190,8 @@ example {X Y Z:Prop} (hXY: X ↔ Y) (hXZ: X ↔ Z) : [X,Y,Z].TFAE := by tfae_have 1 ↔ 3 := by exact hXZ -- This line is optional tfae_finish -/-- Note for the {name (full := List.TFAE.out)}`out` method that one indexes starting from 0, in contrast to the {tactic}`tfae_have` tactic. -/ +/-- Note for the {name (full := List.TFAE.out)}`out` method that one indexes starting from 0, in +contrast to the {tactic}`tfae_have` tactic. -/ example {X Y Z:Prop} (h: [X,Y,Z].TFAE) : X ↔ Y := by exact h.out 0 1 @@ -198,7 +203,8 @@ example {X Y:Prop} : ¬ (X ↔ Y) ↔ sorry := by sorry /-- Exercise A.1.3. -/ def Exercise_A_1_3 : Decidable (∀ (X Y: Prop), (X → Y) → (¬X → ¬ Y) → (X ↔ Y)) := by - -- the first line of this construction should be either `apply isTrue` or `apply isFalse`, depending on whether you believe the given statement to be true or false. + --the first line of this construction should be either `apply isTrue` or `apply isFalse`, + --depending on whether you believe the given statement to be true or false. sorry /-- Exercise A.1.4. -/ diff --git a/Analysis/Section_2_1.lean b/Analysis/Section_2_1.lean index 7054178a..6d09df3e 100644 --- a/Analysis/Section_2_1.lean +++ b/Analysis/Section_2_1.lean @@ -14,12 +14,12 @@ so. Main constructions and results of this section: -- Definition of the "Chapter 2" natural numbers, `Chapter2.Nat`, abbreviated as {name}`Nat` within the - Chapter2 namespace. (In the book, the natural numbers are treated in a purely axiomatic +- Definition of the "Chapter 2" natural numbers, `Chapter2.Nat`,abbreviated as {name}`Nat` within + the Chapter2 namespace. (In the book, the natural numbers are treated in a purely axiomatic fashion, as a type that obeys the Peano axioms; but here we take advantage of Lean's native - inductive types to explicitly construct a version of the natural numbers that obey those - axioms. One could also proceed more axiomatically, as is done in Section 3 for set theory: - see the epilogue to this chapter.) + inductive types to explicitly construct a version of the natural numbers that obey those axioms. + One could also proceed more axiomatically, as is done in Section 3 for set theory: see the + epilogue to this chapter.) - Establishment of the Peano axioms for `Chapter2.Nat`. - Recursive definitions for `Chapter2.Nat`. @@ -50,11 +50,9 @@ postfix:100 "++" => Nat.succ #check (fun n ↦ n++) -/-- - Definition 2.1.3 (Definition of the numerals 0, 1, 2, etc.). Note: to avoid ambiguity, one may - need to use explicit casts such as {lean}`(0:Nat)`, {lean}`(1:Nat)`, etc. to refer to this chapter's version - of the natural numbers. --/ +/-- Definition 2.1.3 (Definition of the numerals 0, 1, 2, etc.). Note: to avoid ambiguity, one may + need to use explicit casts such as {lean}`(0:Nat)`, {lean}`(1:Nat)`, etc. to refer to this + chapter's version of the natural numbers. -/ instance Nat.instOfNat {n:_root_.Nat} : OfNat Nat n where ofNat := _root_.Nat.rec 0 (fun _ n ↦ n++) n @@ -115,10 +113,8 @@ theorem Nat.six_ne_two : (6:Nat) ≠ 2 := by theorem Nat.six_ne_two' : (6:Nat) ≠ 2 := by decide -/-- - Axiom 2.5 (Principle of mathematical induction). The {tactic}`induction` (or {tactic}`induction'`) tactic in - Mathlib serves as a substitute for this axiom. --/ +/-- Axiom 2.5 (Principle of mathematical induction). The {tactic}`induction` (or + {tactic}`induction'`) tactic in Mathlib serves as a substitute for this axiom. -/ theorem Nat.induction (P : Nat → Prop) (hbase : P 0) (hind : ∀ n, P n → P (n++)) : ∀ n, P n := by intro n diff --git a/Analysis/Section_2_2.lean b/Analysis/Section_2_2.lean index 1709e87c..d0f003f7 100644 --- a/Analysis/Section_2_2.lean +++ b/Analysis/Section_2_2.lean @@ -24,7 +24,8 @@ standard Mathlib class {name}`_root_.Nat`, or {lean}`ℕ`. However, we will dev ## Tips from past users -Users of the companion who have completed the exercises in this section are welcome to send their tips for future users in this section as PRs. +Users of the companion who have completed the exercises in this section are welcome to send their +tips for future users in this section as PRs. - (Add tip here) @@ -36,9 +37,9 @@ namespace Chapter2 Compare with Mathlib's {name}`Nat.add` -/ abbrev Nat.add (n m : Nat) : Nat := Nat.recurse (fun _ sum ↦ sum++) m n -/-- This instance allows for the {kw (of := «term_+_»)}`+` notation to be used for natural number addition. -/ -instance Nat.instAdd : Add Nat where - add := add +/-- This instance allows for the {kw (of := «term_+_»)}`+` notation to be used for natural number + addition.-/ +instance Nat.instAdd : Add Nat where add := add /-- Compare with Mathlib's {name}`Nat.zero_add`. -/ @[simp] @@ -113,7 +114,7 @@ theorem Nat.add_left_cancel (a b c:Nat) (habc: a + b = a + c) : b = c := by /-- (Not from textbook) {name}`Nat` can be given the structure of a commutative additive monoid. -This permits tactics such as {tactic}`abel` to apply to the Chapter 2 natural numbers. -/ + This permits tactics such as {tactic}`abel` to apply to the Chapter 2 natural numbers. -/ instance Nat.addCommMonoid : AddCommMonoid Nat where add_assoc := add_assoc add_comm := add_comm @@ -143,8 +144,8 @@ theorem Nat.add_pos_left {a:Nat} (b:Nat) (ha: a.IsPos) : (a + b).IsPos := by /-- Compare with Mathlib's {name}`Nat.add_pos_right`. -This theorem is a consequence of the previous theorem and {name}`add_comm`, and {tactic}`grind` can automatically discover such proofs. --/ +This theorem is a consequence of the previous theorem and {name}`add_comm`, and {tactic}`grind` can +automatically discover such proofs. -/ theorem Nat.add_pos_right {a:Nat} (b:Nat) (ha: a.IsPos) : (b + a).IsPos := by grind [add_comm, add_pos_left] @@ -320,10 +321,10 @@ theorem Nat.trichotomous (a b:Nat) : a < b ∨ a = b ∨ a > b := by tauto /-- - (Not from textbook) Establish the decidability of this order computably. The portion of the - proof involving decidability has been provided; the remaining sorries involve claims about the - natural numbers. One could also have established this result by the {tactic}`classical` tactic - followed by {syntax tactic}`exact Classical.decRel _`, but this would make this definition (as well as some + (Not from textbook) Establish the decidability of this order computably. The portion of the proof + involving decidability has been provided; the remaining sorries involve claims about the natural + numbers. One could also have established this result by the {tactic}`classical` tactic followed + by {syntax tactic}`exact Classical.decRel _`, but this would make this definition (as well as some instances below) noncomputable. Compare with Mathlib's {name}`Nat.decLe`. @@ -376,7 +377,8 @@ instance Nat.instLinearOrder : LinearOrder Nat where example (a b c d:Nat) (hab: a ≤ b) (hbc: b ≤ c) (hcd: c ≤ d) (hda: d ≤ a) : a = c := by order -/-- An illustration of the {tactic}`calc` tactic with {kw (of := «term_≤_»)}`≤`/{kw (of := «term_<_»)}`<`. -/ +/-- An illustration of the {tactic}`calc` tactic with {kw (of := «term_≤_»)}`≤`/ + {kw (of :=«term_<_»)}`<`. -/ example (a b c d e:Nat) (hab: a ≤ b) (hbc: b < c) (hcd: c ≤ d) (hde: d ≤ e) : a + 0 < e := by calc @@ -387,7 +389,7 @@ example (a b c d e:Nat) (hab: a ≤ b) (hbc: b < c) (hcd: c ≤ d) _ ≤ e := hde /-- (Not from textbook) {name}`Nat` has the structure of an ordered monoid. This allows for tactics -such as {tactic}`gcongr` to be applicable to the Chapter 2 natural numbers. -/ + such as {tactic}`gcongr` to be applicable to the Chapter 2 natural numbers. -/ instance Nat.isOrderedAddMonoid : IsOrderedAddMonoid Nat where add_le_add_left a b hab c := (Nat.add_le_add_right a b c).mp hab @@ -419,6 +421,5 @@ theorem Nat.induction_from {n:Nat} {P: Nat → Prop} (hind: ∀ m, P m → P (m+ P n → ∀ m, m ≥ n → P m := by sorry - - end Chapter2 +