[Merged by Bors] - chore(Data/Int/Fib): add fib_neg

Mathlib/Algebra/Ring/Parity.lean

@@ -5,7 +5,7 @@ Authors: Damiano Testa
 -/
 module
 
-public import Mathlib.Algebra.Group.Nat.Even
+public import Mathlib.Algebra.Group.Int.Even
 public import Mathlib.Data.Nat.Cast.Basic
 public import Mathlib.Data.Nat.Cast.Commute
 public import Mathlib.Data.Set.Operations
@@ -48,16 +48,6 @@ lemma Even.neg_one_pow (h : Even n) : (-1 : α) ^ n = 1 := by rw [h.neg_pow, one
 
 end Monoid
 
-section DivisionMonoid
-variable [DivisionMonoid α] [HasDistribNeg α] {a : α} {n : ℤ}
-
-lemma Even.neg_zpow : Even n → ∀ a : α, (-a) ^ n = a ^ n := by
-  rintro ⟨c, rfl⟩ a; simp_rw [← Int.two_mul, zpow_mul, zpow_two, neg_mul_neg]
-
-lemma Even.neg_one_zpow (h : Even n) : (-1 : α) ^ n = 1 := by rw [h.neg_zpow, one_zpow]
-
-end DivisionMonoid
-
 @[simp] lemma IsSquare.zero [MulZeroClass α] : IsSquare (0 : α) := ⟨0, (mul_zero _).symm⟩
 
 section Semiring
@@ -363,6 +353,20 @@ lemma neg_one_pow_eq_neg_one_iff_odd (h : (-1 : R) ≠ 1) :
 
 end DistribNeg
 
+section DivisionMonoid
+variable [DivisionMonoid α] [HasDistribNeg α] {a : α} {n : ℤ}
+
+lemma Even.neg_zpow : Even n → ∀ a : α, (-a) ^ n = a ^ n := by
+  rintro ⟨c, rfl⟩ a; simp_rw [← Int.two_mul, zpow_mul, zpow_two, neg_mul_neg]
+
+lemma Even.neg_one_zpow (h : Even n) : (-1 : α) ^ n = 1 := by rw [h.neg_zpow, one_zpow]
+
+lemma neg_one_zpow_eq_ite : (-1 : α) ^ n = if Even n then 1 else -1 := by
+  obtain ⟨n, _⟩ := n.eq_nat_or_neg
+  aesop (add safe (by rw [neg_one_pow_eq_ite]))
+
+end DivisionMonoid
+
 section CharTwo
 
 -- We state the following theorems in terms of the slightly more general `2 = 0` hypothesis.

Mathlib/Data/Int/Fib.lean

@@ -54,11 +54,12 @@ theorem fib_neg_natCast (n : ℕ) : fib (-n) = (-1) ^ (n + 1) * n.fib := by
   · simp [fib, hn, pow_add]
   · simp [fib_of_odd, hn]
 
+theorem fib_neg (n : ℤ) : fib (-n) = if Even n then -fib n else fib n := by
+  obtain ⟨n, _⟩ := n.eq_nat_or_neg
+  aesop (add safe (by rw [fib_neg_natCast]))
+
 theorem coe_fib_neg (n : ℤ) : (fib (-n) : ℚ) = (-1) ^ (n + 1) * fib n := by
-  obtain ⟨n, (rfl | rfl)⟩ := n.eq_nat_or_neg
-  · exact_mod_cast fib_neg_natCast _
-  · rw [fib_neg_natCast, pow_add, Rat.zpow_add (by simp)]
-    simp
+  aesop (add safe (by rw [fib_neg, neg_one_zpow_eq_ite]))
 
 theorem fib_add_two (n : ℤ) : fib (n + 2) = fib n + fib (n + 1) := by
   rcases n with (n | n)
@@ -149,24 +150,19 @@ theorem fib_two_mul_add_two (n : ℤ) :
   rw [← mul_add_one, fib_two_mul]
   grind [fib_add_two]
 
-theorem fib_gcd (m n : ℤ) : fib (gcd m n) = gcd (fib m) (fib n) := by
+theorem gcd_fib (m n : ℤ) : gcd (fib m) (fib n) = Nat.fib (gcd m n) := by
   obtain ⟨m, (rfl | rfl)⟩ := m.eq_nat_or_neg
   · obtain ⟨n, (rfl | rfl)⟩ := n.eq_nat_or_neg
     · simp [Nat.fib_gcd]
-    · simp only [gcd_neg, Int.gcd_natCast_natCast, fib_natCast, Nat.fib_gcd, fib_neg_natCast,
-        reduceNeg, Nat.cast_inj]
-      rcases neg_one_pow_eq_or ℤ (n + 1) with (h | h) <;> simp [h]
+    · simp [fib_neg, Nat.fib_gcd, apply_ite]
   · obtain ⟨n, (rfl | rfl)⟩ := n.eq_nat_or_neg
-    · simp only [neg_gcd, Int.gcd_natCast_natCast, fib_natCast, Nat.fib_gcd, fib_neg_natCast,
-        reduceNeg, Nat.cast_inj]
-      rcases neg_one_pow_eq_or ℤ (m + 1) with (h | h) <;> simp [h]
-    · simp only [gcd_neg, neg_gcd, Int.gcd_natCast_natCast, fib_natCast, Nat.fib_gcd,
-        fib_neg_natCast, reduceNeg, Nat.cast_inj]
-      rcases neg_one_pow_eq_or ℤ (n + 1) with (h | h) <;>
-        rcases neg_one_pow_eq_or ℤ (m + 1) with (h' | h') <;> simp [h, h']
+    · simp only [fib_neg, neg_gcd, Int.gcd_natCast_natCast, Nat.fib_gcd]
+      split_ifs <;> simp
+    · simp only [fib_neg, gcd_neg, neg_gcd, Int.gcd_natCast_natCast, Nat.fib_gcd]
+      split_ifs <;> simp
 
 private theorem fib_natCast_dvd {m : ℕ} {n : ℤ} (h : (m : ℤ) ∣ n) : fib m ∣ fib n := by
-  rwa [← gcd_eq_left_iff_dvd (by simp), ← fib_gcd, gcd_eq_left_iff_dvd (by simp) |>.mpr]
+  rwa [← gcd_eq_left_iff_dvd (by simp), gcd_fib, ← fib_natCast, (gcd_eq_left_iff_dvd (by simp)).mpr]
 
 theorem fib_dvd (m n : ℤ) (h : m ∣ n) : fib m ∣ fib n := by
   obtain ⟨m, (rfl | rfl)⟩ := m.eq_nat_or_neg