cleaned up some proofs

FriezePatterns/Chapter1/section1.lean

@@ -58,24 +58,24 @@ class nzPattern_n (F : Type*) [Field F] (f : ℕ × ℕ → F) (n : ℕ) extends
 
 -- Continuant property for patterns of finite width
 -- This is probably a better formulation:
-lemma finiteContinuant (F : Type*) [Field F] (f : ℕ×ℕ → F) (n: ℕ) [nzPattern_n F f n] : ∀ i, i ≤ n+1 → ∀m, f (i+2,m) = f (1,m+i+1)*f (i+1,m) - f (i,m) := by sorry
-lemma finiteContinuantOld (F : Type*) [Field F] (f : ℕ×ℕ → F) (n i: ℕ) [nzPattern_n F f n] (hi: i ≤ n+1) : ∀m, f (i+2,m) = f (1,m+i+1)*f (i+1,m) - f (i,m) := by
+lemma finiteContinuant (F : Type*) [Field F] (f : ℕ×ℕ → F) (n: ℕ) [nzPattern_n F f n] : ∀ i, i ≤ n+1 → ∀m, f (i+2,m) = f (1,m+i+1)*f (i+1,m) - f (i,m) := by
+ intro i
  induction i with
  | zero =>
-  intro m
-  simp
-  have h₀ : f (0,m) = 1 ∧ f (0,m+1) = 1 := by exact ⟨pattern_n.topBordOnes n m, pattern_n.topBordOnes n (m + 1)⟩
-  rw [h₀.1, ← zero_add 2]
-  nth_rw 1 [← zero_add 1]
-  nth_rw 3 [← zero_add 1]
-  rw[mul_comm, pattern_n.diamond n m 0, h₀.2]
-  simp
+ intro _ m
+ simp
+ have h₀ : f (0,m) = 1 ∧ f (0,m+1) = 1 := by exact ⟨pattern_n.topBordOnes n m, pattern_n.topBordOnes n (m + 1)⟩
+ rw [h₀.1, ← zero_add 2]
+ nth_rw 1 [← zero_add 1]
+ nth_rw 3 [← zero_add 1]
+ rw[mul_comm, pattern_n.diamond n m 0, h₀.2]
+ simp
  | succ k ih =>
- intro m
+ intro h m
  have h₁ : f (k+2,m+1) = f (1, m +1 + k + 1) * f (k + 1, m+1) - f (k, m+1) := by
   rw [ih]
   linarith
- have h₂ : f (k + 1, m+1) ≠ 0 := by exact nzPattern_n.non_zero (k + 1) (m + 1) hi
+ have h₂ : f (k + 1, m+1) ≠ 0 := by exact nzPattern_n.non_zero (k + 1) (m + 1) h
  calc f (k + 1 + 2, m) = f (k + 1 + 2, m) * f (k + 1, m+1) * (f (k + 1, m+1))⁻¹ := by rw [mul_inv_cancel_right₀ h₂ (f (k + 1 + 2, m))]
   _= (f (k+2,m)*f (k+2,m+1) - 1) * (f (k + 1, m+1))⁻¹ := by rw [pattern_n.diamond n m (k+1)]
   _= (f (k+2,m)*(f (1, m +1 + k + 1) * f (k + 1, m+1) - f (k, m+1)) - 1) * (f (k + 1, m+1))⁻¹ := by rw [h₁]
@@ -85,8 +85,11 @@ lemma finiteContinuantOld (F : Type*) [Field F] (f : ℕ×ℕ → F) (n i: ℕ)
   _= f (1, m +1 + k + 1)*f (k+2,m) - f (k+1,m) := by rw [mul_inv_cancel_right₀ h₂ (f (1, m +1 + k + 1)*f (k+2,m)), mul_inv_cancel_right₀ h₂ (f (k+1,m))]
   _= f (1, m + (k + 1) + 1) * f (k + 1 + 1, m) - f (k + 1, m) := by ring
 
+
 -- This is a finiteContinuant lemma "in the other direction"
-lemma reverseFiniteContinuant (F : Type*) [Field F] (f : ℕ×ℕ → F) (n: ℕ) [nzPattern_n F f n] : ∀ i, i ≤ n+1 → ∀m, f (i,m+2) = f (n,m+2)*f (i+1,m+1) - f (i+2,m) := by sorry
+lemma reverseFiniteContinuant (F : Type*) [Field F] (f : ℕ×ℕ → F) (n: ℕ) [nzPattern_n F f n] : ∀i, i≤n+1→∀m, f (i,m+2) = f (n,m+2)*f (i+1,m+1)-f (i+2,m) := by
+  sorry
+  -- The induction should be from n downwards
 
 lemma glide0 (F : Type*) [Field F] (f : ℕ×ℕ → F) (n: ℕ) [nzPattern_n F f n] : ∀m, f (0,m) = f (n+1, m+1) := by
   intro m
@@ -130,12 +133,13 @@ lemma glideSymm (F : Type*) [Field F] (f : ℕ×ℕ → F) (n: ℕ) [nzPattern_n
    _= f (1,m+i+1)* f (n - i, m + (i + 1) + 1) - f (n + 1 - i, m + i + 1) := by rw [hii m]
    _= f (n, m+i+1+2)* f (n - i, m + (i + 1) + 1) - f (n + 1 - i, m + i + 1) := by rw [glide1 F f n (m+i+1)]
    _= f (n,(m+i+1)+2)* f (n - i, (m + i + 1) + 1)-f (n + 1 - i, m + i + 1) := by rw [add_assoc m]
-   _= f (n,(m+i+1)+2)*f (n - (i+1)+1, (m + i + 1) + 1) - f (n -(i+1)+2, m + i + 1) := by sorry -- This is arithmetic in ℕ nonsense
+   _= f (n,(m+i+1)+2)*f (n - (i+1)+1, (m + i + 1) + 1) - f (n -(i+1)+2, m + i + 1) := by sorry -- This is arithmetic-in-ℕ nonsense
    _= f (n - (i+1), (m+i+1)+2) := by exact Eq.symm (reverseFiniteContinuant F f n (n - (i+1)) h'' (m+i+1))
 
 
 lemma translateInvar (F : Type*) [Field F] (f : ℕ×ℕ → F) (n: ℕ) [nzPattern_n F f n] : ∀ i, i ≤ n+1 → ∀ m, f (i,m) = f (i,m+n+3) := by
   intro i h m
-  calc f (i,m) = f (n+1-i, m+i+1) := by sorry -- glide symm
-  _= f (n+1-(n+1-i), (m+i+1)+(n+1-i)+1) := by sorry -- glide symm again
-  _= f (i,m+n+3) := by sorry -- arithmetic in ℕ
+  have h₁ : n+1-i ≤ n+1 := by simp
+  calc f (i,m) = f (n+1-i, m+i+1) := by exact glideSymm F f n i h m
+  _= f (n+1-(n+1-i), (m+i+1)+(n+1-i)+1) := by exact glideSymm F f n (n+1-i) h₁ (m+i+1)
+  _= f (i,m+n+3) := by sorry -- This is arithmetic-in-ℕ nonsense