From c8797956abb9c28e2a3eaa97e25a5b926b4cbc40 Mon Sep 17 00:00:00 2001
From: Andre <espietandre@gmail.com>
Date: Fri, 16 Jun 2023 15:11:07 -0400
Subject: [PATCH 1/7] golfed foo

---
 CommAlg/final_poly_type.lean | 39 ++++++------------------------------
 1 file changed, 6 insertions(+), 33 deletions(-)

diff --git a/CommAlg/final_poly_type.lean b/CommAlg/final_poly_type.lean
index 85b01a2..07b7bf4 100644
--- a/CommAlg/final_poly_type.lean
+++ b/CommAlg/final_poly_type.lean
@@ -194,45 +194,18 @@ lemma Δ_1_ (f : ℤ → ℤ) (d : ℕ) : PolyType (Δ f 1) d → PolyType f (d
   sorry
 
 
-lemma foo (d : ℕ) : (f : ℤ → ℤ) → (∃ (c : ℤ), ∃ (N : ℤ), (∀ (n : ℤ), N ≤ n → (Δ f d) (n) = c) ∧ c ≠ 0) → (PolyType f d)  := by
+lemma foo (d : ℕ) : (f : ℤ → ℤ) → (∃ (c : ℤ), ∃ (N : ℤ), (∀ (n : ℤ), N ≤ n → 
+    (Δ f d) (n) = c) ∧ c ≠ 0) → (PolyType f d)  := by
   induction' d with d hd
-
   -- Base case
-  · intro f
-    intro h
-    rcases h with ⟨c, N, hh⟩
-    rw [PolyType_0]
-    use c
-    use N
-    tauto
-
+  · rintro f ⟨c, N, hh⟩; rw [PolyType_0 f]; exact ⟨c, N, hh⟩
   -- Induction step
-  · intro f
-    intro h
-    rcases h with ⟨c, N, h⟩
-    have this : PolyType f (d + 1) := by
-      rcases h with ⟨H,c0⟩
-      let g := (Δ f 1)
-      have this1 : (∃ (c : ℤ), ∃ (N : ℤ), (∀ (n : ℤ), N ≤ n → (Δ g d) (n) = c) ∧ c ≠ 0) := by
-        use c; use N
-        constructor
-        · intro n
-          specialize H n
-          intro h
-          have this : Δ f (d + 1) n = c := by tauto
-          rw [←this]
-          rw [Δ_1_s_equiv_Δ_s_1] 
-        · tauto 
-      have this2 : PolyType g d := by
-        apply hd
-        tauto
-      exact Δ_1_ f d this2
-    exact this
+  · exact fun f ⟨c, N, ⟨H, c0⟩⟩ =>
+      Δ_1_ f d (hd (Δ f 1) ⟨c, N, fun n h => by rw [← H n h, Δ_1_s_equiv_Δ_s_1], c0⟩)
 
 -- [BH, 4.1.2] (a) => (b)
 -- Δ^d f (n) = c for some nonzero integer c for n >> 0 → f is of polynomial type d
-lemma a_to_b (f : ℤ → ℤ) (d : ℕ) : (∃ (c : ℤ), ∃ (N : ℤ), (∀ (n : ℤ), N ≤ n → (Δ f d) (n) = c) ∧ c ≠ 0) → PolyType f d := by
-  sorry
+lemma a_to_b (f : ℤ → ℤ) (d : ℕ) : (∃ (c : ℤ), ∃ (N : ℤ), (∀ (n : ℤ), N ≤ n → (Δ f d) (n) = c) ∧ c ≠ 0) → PolyType f d := fun h => (foo d f) h
 
 -- [BH, 4.1.2] (a) <= (b)
 -- f is of polynomial type d → Δ^d f (n) = c for some nonzero integer c for n >> 0

From 3e8aafd23d5e659f989faa2f8acc167fa78dd913 Mon Sep 17 00:00:00 2001
From: Andre <espietandre@gmail.com>
Date: Fri, 16 Jun 2023 15:17:43 -0400
Subject: [PATCH 2/7] golfed delta_

---
 CommAlg/final_poly_type.lean | 13 +++----------
 1 file changed, 3 insertions(+), 10 deletions(-)

diff --git a/CommAlg/final_poly_type.lean b/CommAlg/final_poly_type.lean
index 07b7bf4..8bc6b9e 100644
--- a/CommAlg/final_poly_type.lean
+++ b/CommAlg/final_poly_type.lean
@@ -53,8 +53,6 @@ noncomputable section
 def PolyType (f : ℤ → ℤ) (d : ℕ) := ∃ Poly : Polynomial ℚ, ∃ (N : ℤ), (∀ (n : ℤ), N ≤ n → f n = Polynomial.eval (n : ℚ) Poly) ∧ d = Polynomial.degree Poly
 section
 
-#check PolyType
-
 example (f : ℤ → ℤ) (hf : ∀ x, f x = x ^ 2) : PolyType f 2 := by
   unfold PolyType
   sorry
@@ -132,8 +130,8 @@ lemma PolyType_0 (f : ℤ → ℤ) : (PolyType f 0) ↔ (∃ (c : ℤ), ∃ (N :
 
 -- Δ of 0 times preserves the function
 lemma Δ_0 (f : ℤ → ℤ) : (Δ f 0) = f := by rfl
-  --simp only [Δ]
--- Δ of 1 times decreaes the polynomial type by one
+
+-- Δ of 1 times decreaes the polynomial type by one --can be golfed
 lemma Δ_1 (f : ℤ → ℤ) (d : ℕ) : PolyType f (d + 1) → PolyType (Δ f 1) d := by
   intro h
   simp only [PolyType, Δ, Int.cast_sub, exists_and_right]
@@ -186,20 +184,15 @@ lemma Δ_d_PolyType_d_to_PolyType_0 (f : ℤ → ℤ) (d : ℕ): PolyType f d 
 
 -- The "reverse" of Δ of 1 times increases the polynomial type by one
 lemma Δ_1_ (f : ℤ → ℤ) (d : ℕ) : PolyType (Δ f 1) d → PolyType f (d + 1) := by
-  intro h
+  rintro ⟨P, N, ⟨h1, h2⟩⟩ 
   simp only [PolyType, Nat.cast_add, Nat.cast_one, exists_and_right]
-  rcases h with ⟨P, N, h⟩
-  rcases h with ⟨h1, h2⟩
   let G := fun (q : ℤ) => f (N)
   sorry
 
-
 lemma foo (d : ℕ) : (f : ℤ → ℤ) → (∃ (c : ℤ), ∃ (N : ℤ), (∀ (n : ℤ), N ≤ n → 
     (Δ f d) (n) = c) ∧ c ≠ 0) → (PolyType f d)  := by
   induction' d with d hd
-  -- Base case
   · rintro f ⟨c, N, hh⟩; rw [PolyType_0 f]; exact ⟨c, N, hh⟩
-  -- Induction step
   · exact fun f ⟨c, N, ⟨H, c0⟩⟩ =>
       Δ_1_ f d (hd (Δ f 1) ⟨c, N, fun n h => by rw [← H n h, Δ_1_s_equiv_Δ_s_1], c0⟩)
 

From 24d2f8e1f082b81dcebe9db0cefe17c1c00b81e5 Mon Sep 17 00:00:00 2001
From: chelseaandmadrid <53058005+chelseaandmadrid@users.noreply.github.com>
Date: Fri, 16 Jun 2023 12:20:24 -0700
Subject: [PATCH 3/7] finish poly_shifting

---
 CommAlg/final_poly_type.lean | 18 ++++++++++++++----
 1 file changed, 14 insertions(+), 4 deletions(-)

diff --git a/CommAlg/final_poly_type.lean b/CommAlg/final_poly_type.lean
index 85b01a2..6c9e556 100644
--- a/CommAlg/final_poly_type.lean
+++ b/CommAlg/final_poly_type.lean
@@ -15,6 +15,7 @@ macro "obviously" : tactic =>
         | simp; tauto; done; dbg_trace "it was simp tauto"
         | rfl; done; dbg_trace "it was rfl"
         | norm_num; done; dbg_trace "it was norm_num"
+        | norm_cast; done; dbg_trace "it was norm_cast"
         | /-change (@Eq ℝ _ _);-/ linarith; done; dbg_trace "it was linarith"
         -- | gcongr; done
         | ring; done; dbg_trace "it was ring"
@@ -84,7 +85,7 @@ lemma Polynomial_shifting (F : Polynomial ℚ) (s : ℚ) : ∃ (G : Polynomial 
   sorry
 
 -- Shifting doesn't change the polynomial type
-lemma Poly_shifting (f : ℤ → ℤ) (g : ℤ → ℤ) (hf : PolyType f d) (s : ℤ) (hfg : ∀ (n : ℤ), f (n + s) = g (n)) : PolyType g d := by
+lemma Poly_shifting (f : ℤ → ℤ) (g : ℤ → ℤ) (hf : PolyType f d) (s : ℕ) (hfg : ∀ (n : ℤ), f (n + s) = g (n)) : PolyType g d := by
   simp only [PolyType]
   rcases hf with ⟨F, hh⟩
   rcases hh with ⟨N,s1, s2⟩
@@ -97,9 +98,15 @@ lemma Poly_shifting (f : ℤ → ℤ) (g : ℤ → ℤ) (hf : PolyType f d) (s :
   · intro n
     specialize s1 (n + s)
     intro hN
-    have this1 : f (n + s) = Polynomial.eval (n + s : ℚ) F := by
-      sorry
-    sorry
+    have this1 : f (n + s) = Polynomial.eval (n + (s : ℚ)) F := by
+      have this2 : N ≤ n + s := by linarith
+      have this3 : ↑(f (n + ↑s)) = Polynomial.eval (↑(n + ↑s)) F := by tauto
+      rw [this3]
+      norm_cast
+    specialize hfg n
+    rw [←hfg, this1]
+    specialize h1 n
+    tauto
   · rw [h2, s2]
 
 -- PolyType 0 = constant function
@@ -241,6 +248,9 @@ lemma b_to_a (f : ℤ → ℤ) (d : ℕ) (poly : PolyType f d) :
   rw [←PolyType_0]; exact Δ_d_PolyType_d_to_PolyType_0 f d poly
 
 end
+
+
+
 -- @Additive lemma of length for a SES
 -- Given a SES 0 → A → B → C → 0, then length (A) - length (B) + length (C) = 0 
 section

From cb4e0ead26d54fd6e615dbc1a576fbd8bf7dcbef Mon Sep 17 00:00:00 2001
From: chelseaandmadrid <53058005+chelseaandmadrid@users.noreply.github.com>
Date: Fri, 16 Jun 2023 13:16:46 -0700
Subject: [PATCH 4/7] trivial change

---
 CommAlg/final_poly_type.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/CommAlg/final_poly_type.lean b/CommAlg/final_poly_type.lean
index 9388083..85e322f 100644
--- a/CommAlg/final_poly_type.lean
+++ b/CommAlg/final_poly_type.lean
@@ -5,7 +5,7 @@ import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
 set_option maxHeartbeats 0
 macro "ls" : tactic => `(tactic|library_search)
 
--- New tactic "obviously"
+-- From Kyle : New tactic "obviously"
 macro "obviously" : tactic =>
   `(tactic| (
       first

From 3588faa23ce477c043cce51f800dc1a471120dce Mon Sep 17 00:00:00 2001
From: chelseaandmadrid <53058005+chelseaandmadrid@users.noreply.github.com>
Date: Fri, 16 Jun 2023 14:34:28 -0700
Subject: [PATCH 5/7] add something in Polynomial_shifting

---
 CommAlg/final_poly_type.lean | 28 +++++++++++++++++++++++++++-
 1 file changed, 27 insertions(+), 1 deletion(-)

diff --git a/CommAlg/final_poly_type.lean b/CommAlg/final_poly_type.lean
index 85e322f..2820552 100644
--- a/CommAlg/final_poly_type.lean
+++ b/CommAlg/final_poly_type.lean
@@ -80,7 +80,33 @@ lemma Poly_constant (F : Polynomial ℚ) (c : ℚ) :
 
 -- Get the polynomial G (X) = F (X + s) from the polynomial F(X)
 lemma Polynomial_shifting (F : Polynomial ℚ) (s : ℚ) : ∃ (G : Polynomial ℚ), (∀ (x : ℚ), Polynomial.eval x G = Polynomial.eval (x + s) F) ∧ (Polynomial.degree G = Polynomial.degree F) := by  
-  sorry
+  let Shift := (Polynomial.monomial 1 (1 : ℚ)) + (Polynomial.C s)
+  let G := Polynomial.comp Shift F
+  use G
+  constructor
+  · intro t
+    have this : Polynomial.eval t G = Polynomial.eval (Polynomial.eval t Shift) F:= by
+      sorry
+    have this1 : Polynomial.eval t Shift = t + s := by
+      dsimp; simp
+    rw [this1] at this
+    exact this
+  · have this : Polynomial.degree G = (Polynomial.degree F) * (Polynomial.degree Shift) := by
+      sorry
+    have Shift_degree : Polynomial.degree Shift = 1 := by
+      have this2 : Polynomial.degree (Polynomial.monomial 1 (1 : ℚ)) = 1 := by
+        have this3 : (1 : ℚ) ≠ 0 := by norm_num
+        exact Polynomial.degree_monomial 1 this3
+      have this1 : Polynomial.degree Shift = (Polynomial.degree (Polynomial.monomial 1 (1 : ℚ))) + (Polynomial.degree (Polynomial.C s)) := by
+        sorry
+      have this3 : Polynomial.degree (Polynomial.C s) = 0 := by
+        sorry
+      rw [this1, this2, this3]
+      trivial
+    rw [Shift_degree] at this
+    rw [this]
+    norm_num
+
 
 -- Shifting doesn't change the polynomial type
 lemma Poly_shifting (f : ℤ → ℤ) (g : ℤ → ℤ) (hf : PolyType f d) (s : ℕ) (hfg : ∀ (n : ℤ), f (n + s) = g (n)) : PolyType g d := by

From 01fb5fbd8b6d10e488ed72800c0838664dfe8446 Mon Sep 17 00:00:00 2001
From: Andre <espietandre@gmail.com>
Date: Fri, 16 Jun 2023 17:37:02 -0400
Subject: [PATCH 6/7] finished refactoring

---
 CommAlg/final_poly_type.lean | 51 ++++++++++++++----------------------
 1 file changed, 19 insertions(+), 32 deletions(-)

diff --git a/CommAlg/final_poly_type.lean b/CommAlg/final_poly_type.lean
index 9388083..449da0d 100644
--- a/CommAlg/final_poly_type.lean
+++ b/CommAlg/final_poly_type.lean
@@ -5,7 +5,7 @@ import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
 set_option maxHeartbeats 0
 macro "ls" : tactic => `(tactic|library_search)
 
--- New tactic "obviously"
+-- From Kyle : New tactic "obviously"
 macro "obviously" : tactic =>
   `(tactic| (
       first
@@ -41,7 +41,7 @@ example : Polynomial.eval (100 : ℚ) F = (2 : ℚ) := by
   refine Iff.mpr (Rat.ext_iff (Polynomial.eval 100 F) 2) ?_
   simp only [Rat.ofNat_num, Rat.ofNat_den]
   rw [F]
-  simp
+  simp [simp]
 
 -- Treat polynomial f ∈ ℚ[X] as a function f : ℚ → ℚ
 
@@ -51,7 +51,9 @@ end section
 noncomputable section
 -- Polynomial type of degree d
 @[simp]
-def PolyType (f : ℤ → ℤ) (d : ℕ) := ∃ Poly : Polynomial ℚ, ∃ (N : ℤ), (∀ (n : ℤ), N ≤ n → f n = Polynomial.eval (n : ℚ) Poly) ∧ d = Polynomial.degree Poly
+def PolyType (f : ℤ → ℤ) (d : ℕ) := 
+  ∃ Poly : Polynomial ℚ, ∃ (N : ℤ), (∀ (n : ℤ), N ≤ n → f n = Polynomial.eval (n : ℚ) Poly) ∧ 
+    d = Polynomial.degree Poly
 section
 
 example (f : ℤ → ℤ) (hf : ∀ x, f x = x ^ 2) : PolyType f 2 := by
@@ -68,43 +70,30 @@ def Δ : (ℤ → ℤ) → ℕ → (ℤ → ℤ)
 
 -- (NO need to prove another direction) Constant polynomial function = constant function
 lemma Poly_constant (F : Polynomial ℚ) (c : ℚ) : 
-  (F = Polynomial.C (c : ℚ)) ↔ (∀ r : ℚ, (Polynomial.eval r F) = (c : ℚ)) := by
+    (F = Polynomial.C (c : ℚ)) ↔ (∀ r : ℚ, (Polynomial.eval r F) = (c : ℚ)) := by
   constructor
-  · intro h
-    rintro r
+  · intro h r
     refine Iff.mpr (Rat.ext_iff (Polynomial.eval r F) c) ?_
     simp only [Rat.ofNat_num, Rat.ofNat_den]
-    rw [h]
-    simp
+    simp [h]
   · sorry
 
 -- Get the polynomial G (X) = F (X + s) from the polynomial F(X)
-lemma Polynomial_shifting (F : Polynomial ℚ) (s : ℚ) : ∃ (G : Polynomial ℚ), (∀ (x : ℚ), Polynomial.eval x G = Polynomial.eval (x + s) F) ∧ (Polynomial.degree G = Polynomial.degree F) := by  
+lemma Polynomial_shifting (F : Polynomial ℚ) (s : ℚ) : ∃ (G : Polynomial ℚ), (∀ (x : ℚ), 
+    Polynomial.eval x G = Polynomial.eval (x + s) F) ∧ 
+    (Polynomial.degree G = Polynomial.degree F) := by  
   sorry
 
 -- Shifting doesn't change the polynomial type
-lemma Poly_shifting (f : ℤ → ℤ) (g : ℤ → ℤ) (hf : PolyType f d) (s : ℕ) (hfg : ∀ (n : ℤ), f (n + s) = g (n)) : PolyType g d := by
-  simp only [PolyType]
-  rcases hf with ⟨F, hh⟩
-  rcases hh with ⟨N,s1, s2⟩
-  have this : ∃ (G : Polynomial ℚ), (∀ (x : ℚ), Polynomial.eval x G = Polynomial.eval (x + s) F) ∧ (Polynomial.degree G = Polynomial.degree F) := by
-    exact Polynomial_shifting F s
-  rcases this with ⟨Poly, h1, h2⟩
-  use Poly
-  use N
-  constructor
-  · intro n
-    specialize s1 (n + s)
-    intro hN
+lemma Poly_shifting (f : ℤ → ℤ) (g : ℤ → ℤ) (hf : PolyType f d) (s : ℕ) 
+    (hfg : ∀ (n : ℤ), f (n + s) = g (n)) : PolyType g d := by
+  rcases hf with ⟨F, ⟨N, s1, s2⟩⟩
+  rcases (Polynomial_shifting F s) with ⟨Poly, h1, h2⟩
+  use Poly, N; constructor
+  · intro n hN
     have this1 : f (n + s) = Polynomial.eval (n + (s : ℚ)) F := by
-      have this2 : N ≤ n + s := by linarith
-      have this3 : ↑(f (n + ↑s)) = Polynomial.eval (↑(n + ↑s)) F := by tauto
-      rw [this3]
-      norm_cast
-    specialize hfg n
-    rw [←hfg, this1]
-    specialize h1 n
-    tauto
+      rw [s1 (n + s) (by linarith)]; norm_cast
+    rw [←hfg n, this1]; exact (h1 n).symm
   · rw [h2, s2]
 
 -- PolyType 0 = constant function
@@ -215,8 +204,6 @@ lemma b_to_a (f : ℤ → ℤ) (d : ℕ) (poly : PolyType f d) :
 
 end
 
-
-
 -- @Additive lemma of length for a SES
 -- Given a SES 0 → A → B → C → 0, then length (A) - length (B) + length (C) = 0 
 section

From dbdb06fb587de57a84f7b8a453b04706bc76a485 Mon Sep 17 00:00:00 2001
From: Andre <espietandre@gmail.com>
Date: Fri, 16 Jun 2023 17:42:48 -0400
Subject: [PATCH 7/7] removed a comment

---
 CommAlg/final_poly_type.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/CommAlg/final_poly_type.lean b/CommAlg/final_poly_type.lean
index e96aae3..dd35253 100644
--- a/CommAlg/final_poly_type.lean
+++ b/CommAlg/final_poly_type.lean
@@ -5,7 +5,6 @@ import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
 set_option maxHeartbeats 0
 macro "ls" : tactic => `(tactic|library_search)
 
--- From Kyle : New tactic "obviously"
 -- From Kyle : New tactic "obviously"
 macro "obviously" : tactic =>
   `(tactic| (