[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 : α} {m 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,13 @@ 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
+  rw [fib_neg, cast_ite]
+  grind [neg_one_zpow_eq_ite]
 
 theorem fib_add_two (n : ℤ) : fib (n + 2) = fib n + fib (n + 1) := by
   rcases n with (n | n)