fix lean errors

Author: laurakim1215

Analysis/Section_4_1.lean

@@ -50,7 +50,7 @@ abbrev Int := Quotient PreInt.instSetoid
 
 abbrev Int.formalDiff (a b:ℕ)  : Int := Quotient.mk PreInt.instSetoid ⟨ a,b ⟩
 
-infix:70 " — " => Int.formalDiff
+infix:100 " — " => Int.formalDiff
 
 /-- Definition 4.1.1 (Integers) -/
 theorem Int.eq (a b c d:ℕ): a — b = c — d ↔ a + d = c + b := by

Analysis/Section_4_2.lean

@@ -31,43 +31,31 @@ theorem PreRat.eq (a b c d:ℤ) (hb: b ≠ 0) (hd: d ≠ 0): (⟨ a,b,hb ⟩: Pr
 abbrev Rat := Quotient PreRat.instSetoid
 
 /-- We give division a "junk" value of 0//1 if the denominator is zero -/
-abbrev Rat.formalDiv (a b:ℤ)  : Int := Quotient.mk PreInt.instSetoid if h:b ≠ 0 then ⟨ a,b,h ⟩ else ⟨ 0, 1, by decide ⟩
+abbrev Rat.formalDiv (a b:ℤ)  : Rat := Quotient.mk PreRat.instSetoid (if h:b ≠ 0 then ⟨ a,b,h ⟩ else ⟨ 0, 1, by decide ⟩)
 
-infix:70 " // " => Rat.formalDiv
+infix:100 " // " => Rat.formalDiv
 
 /-- Definition 4.2.1 (Rationals) -/
 theorem Rat.eq (a c:ℤ) {b d:ℤ} (hb: b ≠ 0) (hd: d ≠ 0): a // b = c // d ↔ a * d = c * b := by
-  simp [hb, hd]
-  constructor
-  . exact Quotient.exact
-  intro h; exact Quotient.sound h
+  simp [hb, hd, Setoid.r]
 
 /-- Definition 4.2.1 (Rationals) -/
 theorem Rat.eq_diff (n:Rat) : ∃ a b, b ≠ 0 ∧ n = a // b := by
   apply Quot.ind _ n; intro ⟨ a, b, h ⟩
   use a, b; refine ⟨ h, ?_ ⟩
   simp [Rat.formalDiv, h]
-
-/-- Lemma 4.2.3 (Addition well-defined) -/
-theorem Rat.add_congr_left (a b a' b' c d : ℤ) (hb: b ≠ 0) (hb': b' ≠ 0) (hd: d ≠ 0) (h: a // b = a' // b') : (a*d+b*c) // (b*d) = (a'*d+b'*c) // (b'*d) := by
-  have hbd: b*d ≠ 0 := by sorry
-  have hb'd: b'*d ≠ 0 := by sorry
-  simp only [Rat.eq _ _ hb hb', Rat.eq _ _ hbd hb'd] at h ⊢
-  calc
-    _ = (a*b')*d*d + b*b'*c*d := by ring
-    _ = (a'*b)*d*d + b*b'*c*d := by rw [h]
-    _ = _ := by ring
-
-theorem Rat.add_congr_right (a b c d c' d' : ℤ) (hb: b ≠ 0) (hd: d ≠ 0) (hd': d' ≠ 0) (h: c // d = c' // d') : (a*d+b*c) // (b*d) = (a*d'+b*c') // (b*d') := by sorry
-
-theorem Rat.add_congr (a b c d a' b' c' d' : ℤ) (hb: b ≠ 0) (hb': b' ≠ 0) (hd: d ≠ 0) (hd': d' ≠ 0) (h: a // b = a' // b') : (a*d+b*c) // (b*d) = (a*d'+b*c') // (b*d') := by sorry
+  rfl
 
 
 /-- Lemma 4.2.3 (Addition well-defined) -/
 instance Rat.add_inst : Add Rat where
   add := Quotient.lift₂ (fun ⟨ a, b, h1 ⟩ ⟨ c, d, h2 ⟩ ↦ (a*d+b*c) // (b*d)) (by
-    intros ⟨ a, b, h1 ⟩ ⟨ c, d, h2 ⟩ ⟨ a', b', h1' ⟩ ⟨ c', d', h2' ⟩ h1 h2
-    simp [Setoid.r] at *
-    exact Rat.add_congr_left a b a' b' c d c' d' h1 h1' h2 h2')
+    intro ⟨ a, b, h1 ⟩ ⟨ c, d, h2 ⟩ ⟨ a', b', h1' ⟩ ⟨ c', d', h2' ⟩ h3 h4
+    simp [Setoid.r, h1, h2, h1', h2'] at *
+    calc
+      _ = (a*b')*d*d' + b*b'*(c*d') := by ring
+      _ = (a'*b)*d*d' + b*b'*(c'*d) := by rw [h3, h4]
+      _ = _ := by ring
+  )
 
 end Section_4_2