fix

Author: YaelDillies

Archive/Imo/Imo1994Q1.lean

@@ -3,6 +3,7 @@ Copyright (c) 2021 Antoine Labelle. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Antoine Labelle
 -/
+import Mathlib.Algebra.Group.Fin.Basic
 import Mathlib.Algebra.Order.BigOperators.Group.Finset
 import Mathlib.Data.Finset.Sort
 import Mathlib.Data.Fin.Interval

Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean

@@ -219,7 +219,7 @@ theorem oangle_ne_zero_and_ne_pi_iff_affineIndependent {p₁ p₂ p₃ : P} :
     ∡ p₁ p₂ p₃ ≠ 0 ∧ ∡ p₁ p₂ p₃ ≠ π ↔ AffineIndependent ℝ ![p₁, p₂, p₃] := by
   rw [oangle, o.oangle_ne_zero_and_ne_pi_iff_linearIndependent,
     affineIndependent_iff_linearIndependent_vsub ℝ _ (1 : Fin 3), ←
-    linearIndependent_equiv (finSuccAboveEquiv (1 : Fin 3)).toEquiv]
+    linearIndependent_equiv (finSuccAboveEquiv (1 : Fin 3))]
   convert Iff.rfl
   ext i
   fin_cases i <;> rfl

Mathlib/Order/Fin/Basic.lean

@@ -336,6 +336,14 @@ def OrderIso.finTwoArrowIso (α : Type*) [Preorder α] : (Fin 2 → α) ≃o α
   { OrderIso.piFinTwoIso fun _ => α with toEquiv := finTwoArrowEquiv α }
 #align order_iso.fin_two_arrow_iso OrderIso.finTwoArrowIso
 
+/-- Order isomorphism between `Π j : Fin (n + 1), α j` and
+`α i × Π j : Fin n, α (Fin.succAbove i j)`. -/
+def OrderIso.piFinSuccAboveIso (α : Fin (n + 1) → Type*) [∀ i, LE (α i)]
+    (i : Fin (n + 1)) : (∀ j, α j) ≃o α i × ∀ j, α (i.succAbove j) where
+  toEquiv := Equiv.piFinSuccAbove α i
+  map_rel_iff' := Iff.symm i.forall_iff_succAbove
+#align order_iso.pi_fin_succ_above_iso OrderIso.piFinSuccAboveIso
+
 /-- `Fin.succAbove` as an order isomorphism between `Fin n` and `{x : Fin (n + 1) // x ≠ p}`. -/
 def finSuccAboveOrderIso (p : Fin (n + 1)) : Fin n ≃o { x : Fin (n + 1) // x ≠ p } where
   __ := finSuccAboveEquiv p

Mathlib/SetTheory/Game/PGame.lean

@@ -3,7 +3,6 @@ Copyright (c) 2019 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Reid Barton, Mario Carneiro, Isabel Longbottom, Scott Morrison
 -/
-import Mathlib.Algebra.Group.Fin.Basic
 import Mathlib.Data.List.InsertNth
 import Mathlib.Logic.Relation
 import Mathlib.Logic.Small.Defs