Merge pull request #487 from kvanvels/KEV_line_limit

Chore: Fixed a few lines that were over 100 characters.  Proof of Concept.

Author: teorth

Analysis/Appendix_A_1.lean

@@ -8,8 +8,10 @@ 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 +188,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 +201,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. -/

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

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
+