From a87624ef68f279bd63a136fc089f21fde8b69e0b Mon Sep 17 00:00:00 2001
From: Monica Omar <2497250a@research.gla.ac.uk>
Date: Tue, 25 Nov 2025 17:00:06 +0000
Subject: [PATCH 1/8] neg_one_zpow

---
 Mathlib/Algebra/Ring/Parity.lean | 26 +++++++++++++++-----------
 Mathlib/Data/Int/Fib.lean        | 10 ++++++----
 2 files changed, 21 insertions(+), 15 deletions(-)

diff --git a/Mathlib/Algebra/Ring/Parity.lean b/Mathlib/Algebra/Ring/Parity.lean
index dc90e859de55fc..d200242b366a14 100644
--- a/Mathlib/Algebra/Ring/Parity.lean
+++ b/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.
diff --git a/Mathlib/Data/Int/Fib.lean b/Mathlib/Data/Int/Fib.lean
index e5a383c8cc6ac3..b6c15c216fa6da 100644
--- a/Mathlib/Data/Int/Fib.lean
+++ b/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)

From c6445682d6c060d166913fc1f4cdbc32a986a528 Mon Sep 17 00:00:00 2001
From: Monica Omar <23701951+themathqueen@users.noreply.github.com>
Date: Tue, 25 Nov 2025 17:14:38 +0000
Subject: [PATCH 2/8] Update Parity.lean

---
 Mathlib/Algebra/Ring/Parity.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Algebra/Ring/Parity.lean b/Mathlib/Algebra/Ring/Parity.lean
index d200242b366a14..954b400d8e4f73 100644
--- a/Mathlib/Algebra/Ring/Parity.lean
+++ b/Mathlib/Algebra/Ring/Parity.lean
@@ -354,7 +354,7 @@ lemma neg_one_pow_eq_neg_one_iff_odd (h : (-1 : R) ≠ 1) :
 end DistribNeg
 
 section DivisionMonoid
-variable [DivisionMonoid α] [HasDistribNeg α] {a : α} {m n : ℤ}
+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]

From 3393ca8178ebeb221c73fd43bd0f97a466b763c7 Mon Sep 17 00:00:00 2001
From: Monica Omar <2497250a@research.gla.ac.uk>
Date: Tue, 25 Nov 2025 17:46:37 +0000
Subject: [PATCH 3/8] cleanup

---
 Mathlib/Data/Int/Fib.lean | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Data/Int/Fib.lean b/Mathlib/Data/Int/Fib.lean
index b6c15c216fa6da..27fe09736e3ce2 100644
--- a/Mathlib/Data/Int/Fib.lean
+++ b/Mathlib/Data/Int/Fib.lean
@@ -54,13 +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
+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
-  rw [fib_neg, cast_ite]
-  grind [neg_one_zpow_eq_ite]
+  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)

From 9ae8837b621e8ed49c1ebe0afd43df071f04b7d0 Mon Sep 17 00:00:00 2001
From: Monica Omar <2497250a@research.gla.ac.uk>
Date: Wed, 26 Nov 2025 03:23:30 +0000
Subject: [PATCH 4/8] change one lemma

---
 Mathlib/Data/Int/Fib.lean | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/Mathlib/Data/Int/Fib.lean b/Mathlib/Data/Int/Fib.lean
index 27fe09736e3ce2..07a07aeff47f78 100644
--- a/Mathlib/Data/Int/Fib.lean
+++ b/Mathlib/Data/Int/Fib.lean
@@ -150,24 +150,24 @@ 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]
+        reduceNeg]
       rcases neg_one_pow_eq_or ℤ (n + 1) with (h | h) <;> simp [h]
   · 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]
+        reduceNeg]
       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]
+    · simp only [gcd_neg, neg_gcd, Int.gcd_natCast_natCast, Nat.fib_gcd,
+        fib_neg_natCast, reduceNeg]
       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']
 
 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

From 5e11c6d862b6532f553fce3919fc47619fea89c9 Mon Sep 17 00:00:00 2001
From: Monica Omar <2497250a@research.gla.ac.uk>
Date: Wed, 26 Nov 2025 03:43:57 +0000
Subject: [PATCH 5/8] golf

---
 Mathlib/Data/Int/Fib.lean | 16 ++++++----------
 1 file changed, 6 insertions(+), 10 deletions(-)

diff --git a/Mathlib/Data/Int/Fib.lean b/Mathlib/Data/Int/Fib.lean
index 07a07aeff47f78..c30c38faa1ee63 100644
--- a/Mathlib/Data/Int/Fib.lean
+++ b/Mathlib/Data/Int/Fib.lean
@@ -154,17 +154,13 @@ 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]
-      rcases neg_one_pow_eq_or ℤ (n + 1) with (h | h) <;> simp [h]
+    · simp only [fib_neg, gcd_neg, Int.gcd_natCast_natCast, Nat.fib_gcd]
+      split_ifs <;> simp
   · 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]
-      rcases neg_one_pow_eq_or ℤ (m + 1) with (h | h) <;> simp [h]
-    · simp only [gcd_neg, neg_gcd, Int.gcd_natCast_natCast, Nat.fib_gcd,
-        fib_neg_natCast, reduceNeg]
-      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), gcd_fib, ← fib_natCast, (gcd_eq_left_iff_dvd (by simp)).mpr]

From 3f72e79ec26fb76139bb672142bf428a57add741 Mon Sep 17 00:00:00 2001
From: Monica Omar <2497250a@research.gla.ac.uk>
Date: Wed, 26 Nov 2025 04:09:23 +0000
Subject: [PATCH 6/8] further golf

---
 Mathlib/Data/Int/Fib.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/Mathlib/Data/Int/Fib.lean b/Mathlib/Data/Int/Fib.lean
index c30c38faa1ee63..aea927c03c93ea 100644
--- a/Mathlib/Data/Int/Fib.lean
+++ b/Mathlib/Data/Int/Fib.lean
@@ -154,8 +154,7 @@ 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 [fib_neg, gcd_neg, Int.gcd_natCast_natCast, Nat.fib_gcd]
-      split_ifs <;> simp
+    · simp [fib_neg, gcd_neg, Int.gcd_natCast_natCast, Nat.fib_gcd, apply_ite]
   · obtain ⟨n, (rfl | rfl)⟩ := n.eq_nat_or_neg
     · simp only [fib_neg, neg_gcd, Int.gcd_natCast_natCast, Nat.fib_gcd]
       split_ifs <;> simp

From 43ab6fdec17b32182ac1df379441b00fba78d8ae Mon Sep 17 00:00:00 2001
From: Monica Omar <2497250a@research.gla.ac.uk>
Date: Wed, 26 Nov 2025 04:10:35 +0000
Subject: [PATCH 7/8] cleanup

---
 Mathlib/Data/Int/Fib.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Data/Int/Fib.lean b/Mathlib/Data/Int/Fib.lean
index aea927c03c93ea..136c7d64427528 100644
--- a/Mathlib/Data/Int/Fib.lean
+++ b/Mathlib/Data/Int/Fib.lean
@@ -154,7 +154,7 @@ 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 [fib_neg, gcd_neg, Int.gcd_natCast_natCast, Nat.fib_gcd, apply_ite]
+    · simp [fib_neg, Nat.fib_gcd, apply_ite]
   · obtain ⟨n, (rfl | rfl)⟩ := n.eq_nat_or_neg
     · simp only [fib_neg, neg_gcd, Int.gcd_natCast_natCast, Nat.fib_gcd]
       split_ifs <;> simp

From 4d8e627c89efb2bf18e71ed28f671ff87e60b84b Mon Sep 17 00:00:00 2001
From: Monica Omar <2497250a@research.gla.ac.uk>
Date: Wed, 26 Nov 2025 04:47:20 +0000
Subject: [PATCH 8/8] golf further

---
 Mathlib/Data/Int/Fib.lean | 10 ++--------
 Mathlib/Logic/Basic.lean  |  3 +++
 2 files changed, 5 insertions(+), 8 deletions(-)

diff --git a/Mathlib/Data/Int/Fib.lean b/Mathlib/Data/Int/Fib.lean
index 136c7d64427528..6933de131b8d3c 100644
--- a/Mathlib/Data/Int/Fib.lean
+++ b/Mathlib/Data/Int/Fib.lean
@@ -152,14 +152,8 @@ theorem fib_two_mul_add_two (n : ℤ) :
 
 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 [fib_neg, Nat.fib_gcd, apply_ite]
-  · obtain ⟨n, (rfl | rfl)⟩ := n.eq_nat_or_neg
-    · 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
+    <;> obtain ⟨n, (rfl | rfl)⟩ := n.eq_nat_or_neg
+    <;> simp [fib_neg, Nat.fib_gcd, apply_ite, apply_ite_left]
 
 private theorem fib_natCast_dvd {m : ℕ} {n : ℤ} (h : (m : ℤ) ∣ n) : fib m ∣ fib n := by
   rwa [← gcd_eq_left_iff_dvd (by simp), gcd_fib, ← fib_natCast, (gcd_eq_left_iff_dvd (by simp)).mpr]
diff --git a/Mathlib/Logic/Basic.lean b/Mathlib/Logic/Basic.lean
index f0b8f120cba2b3..373037537c595a 100644
--- a/Mathlib/Logic/Basic.lean
+++ b/Mathlib/Logic/Basic.lean
@@ -912,6 +912,9 @@ either branch to `a`. -/
 theorem ite_apply (f g : ∀ a, σ a) (a : α) : (ite P f g) a = ite P (f a) (g a) :=
   dite_apply P (fun _ ↦ f) (fun _ ↦ g) a
 
+theorem apply_ite_left {α β γ : Sort*} (f : α → β → γ) (P : Prop) [Decidable P]
+    (x y : α) (z : β) : f (if P then x else y) z = if P then f x z else f y z := by grind
+
 section
 variable [Decidable Q]