From 85263016c118b8b2f8363110a0ccc589e6c0222a Mon Sep 17 00:00:00 2001 From: Andre Date: Fri, 16 Jun 2023 00:00:20 -0400 Subject: [PATCH] fixed indentation for PolyType_0 --- CommAlg/final_poly_type.lean | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) diff --git a/CommAlg/final_poly_type.lean b/CommAlg/final_poly_type.lean index 4405e42..bfbef39 100644 --- a/CommAlg/final_poly_type.lean +++ b/CommAlg/final_poly_type.lean @@ -151,9 +151,11 @@ lemma PolyType_0 (f : ℤ → ℤ) : (PolyType f 0) ↔ (∃ (c : ℤ), ∃ (N : · rintro ⟨Poly, ⟨N, ⟨H1, H2⟩⟩⟩ have this1 : Polynomial.degree Poly = 0 := by rw [← H2]; rfl have this2 : ∃ (c : ℤ), Poly = Polynomial.C (c : ℚ) := by - have HH : ∃ (c : ℚ), Poly = Polynomial.C (c : ℚ) := ⟨Poly.coeff 0, Polynomial.eq_C_of_degree_eq_zero (by rw[← H2]; rfl)⟩ + have HH : ∃ (c : ℚ), Poly = Polynomial.C (c : ℚ) := + ⟨Poly.coeff 0, Polynomial.eq_C_of_degree_eq_zero (by rw[← H2]; rfl)⟩ cases' HH with c HHH - have HHHH : ∃ (d : ℤ), d = c := ⟨f N, by simp [(Poly_constant Poly c).mp HHH N, H1 N (le_refl N)]⟩ + have HHHH : ∃ (d : ℤ), d = c := + ⟨f N, by simp [(Poly_constant Poly c).mp HHH N, H1 N (le_refl N)]⟩ cases' HHHH with d H5; exact ⟨d, by rw[← H5] at HHH; exact HHH⟩ rcases this2 with ⟨c, hthis2⟩ use c; use N; intro n @@ -162,10 +164,13 @@ lemma PolyType_0 (f : ℤ → ℤ) : (PolyType f 0) ↔ (∃ (c : ℤ), ∃ (N : rw [hthis2]; simp only [map_intCast, Polynomial.eval_int_cast] exact fun HH1 => Iff.mp (Rat.coe_int_inj (f n) c) (by rw [←this4, H1 n HH1]) · intro c0 - simp only [hthis2, c0, Int.cast_zero, map_zero, Polynomial.degree_zero] at this1 + simp only [hthis2, c0, Int.cast_zero, map_zero, Polynomial.degree_zero] + at this1 · rintro ⟨c, N, hh⟩ - have H2 : (c : ℚ) ≠ 0 := by simp only [ne_eq, Int.cast_eq_zero]; exact (hh 0).2 - exact ⟨Polynomial.C (c : ℚ), N, fun n Nn => by rw [(hh n).1 Nn]; exact (((Poly_constant (Polynomial.C (c : ℚ)) (c : ℚ)).mp rfl) n).symm, by rw [Polynomial.degree_C H2]; rfl⟩ + have H2 : (c : ℚ) ≠ 0 := by simp only [ne_eq, Int.cast_eq_zero]; exact (hh 0).2 + exact ⟨Polynomial.C (c : ℚ), N, fun n Nn + => by rw [(hh n).1 Nn]; exact (((Poly_constant (Polynomial.C (c : ℚ)) + (c : ℚ)).mp rfl) n).symm, by rw [Polynomial.degree_C H2]; rfl⟩