1. Physlib
  2. Mathematics
  3. Fin
Imports
/- Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ module public import Mathlib.Algebra.Order.Group.Nat public import Mathlib.Algebra.Order.Monoid.NatCast public import Mathlib.Logic.Equiv.Fin.Basic

Fin lemmas

The purpose of this file is to define some results Fin currently in Mathlib.

At some point these should either be up-streamed to Mathlib or replaced with definitions already in Mathlib.

@[expose] public section

Given a i and x in Fin n.succ.succ returns an element of Fin n.succ subtracting 1 if i.val ≤ x.val else casting x.

def predAboveI (i x : Fin n.succ.succ) : Fin n.succ := if h : x.val < i.val then ⟨x.val, n:ℕi:Fin n.succ.succx:Fin n.succ.succh:↑x < ↑i⊢ ↑x < n.succ All goals completed! 🐙⟩ else ⟨x.val - 1, n:ℕi:Fin n.succ.succx:Fin n.succ.succh:¬↑x < ↑i⊢ ↑x - 1 < n.succ All goals completed! 🐙⟩
lemma predAboveI_self (i : Fin n.succ.succ) : predAboveI i i = ⟨i.val - 1, n:ℕi:Fin n.succ.succ⊢ ↑i - 1 < n.succ All goals completed! 🐙⟩ := n:ℕi:Fin n.succ.succ⊢ predAboveI i i = ⟨↑i - 1, ⋯⟩ All goals completed! 🐙@[simp] lemma predAboveI_succAbove (i : Fin n.succ.succ) (x : Fin n.succ) : predAboveI i (Fin.succAbove i x) = x := n:ℕi:Fin n.succ.succx:Fin n.succ⊢ predAboveI i (i.succAbove x) = x n:ℕi:Fin n.succ.succx:Fin n.succ⊢ (if h : (if ↑x < ↑i then ↑x else ↑x + 1) < ↑i then if ↑x < ↑i then ↑x else ↑x + 1 else (if ↑x < ↑i then ↑x else ↑x + 1) - 1) = ↑x n:ℕi:Fin n.succ.succx:Fin n.succh✝:↑x < ↑i⊢ ↑x = ↑xn:ℕi:Fin n.succ.succx:Fin n.succh✝¹:¬↑x < ↑ih✝:↑x + 1 < ↑i⊢ ↑x + 1 = ↑xn:ℕi:Fin n.succ.succx:Fin n.succh✝¹:¬↑x < ↑ih✝:¬↑x + 1 < ↑i⊢ ↑x + 1 - 1 = ↑x n:ℕi:Fin n.succ.succx:Fin n.succh✝:↑x < ↑i⊢ ↑x = ↑xn:ℕi:Fin n.succ.succx:Fin n.succh✝¹:¬↑x < ↑ih✝:↑x + 1 < ↑i⊢ ↑x + 1 = ↑xn:ℕi:Fin n.succ.succx:Fin n.succh✝¹:¬↑x < ↑ih✝:¬↑x + 1 < ↑i⊢ ↑x + 1 - 1 = ↑x All goals completed! 🐙lemma succsAbove_predAboveI {i x : Fin n.succ.succ} (h : i ≠ x) : Fin.succAbove i (predAboveI i x) = x := n:ℕi:Fin n.succ.succx:Fin n.succ.succh:i ≠ x⊢ i.succAbove (predAboveI i x) = x n:ℕi:Fin n.succ.succx:Fin n.succ.succh:↑i ≠ ↑x⊢ i.succAbove (predAboveI i x) = x n:ℕi:Fin n.succ.succx:Fin n.succ.succh:↑i ≠ ↑x⊢ (if (if h : ↑x < ↑i then ↑x else ↑x - 1) < ↑i then if h : ↑x < ↑i then ↑x else ↑x - 1 else (if h : ↑x < ↑i then ↑x else ↑x - 1) + 1) = ↑x n:ℕi:Fin n.succ.succx:Fin n.succ.succh:↑i ≠ ↑xh✝:↑x < ↑i⊢ ↑x = ↑xn:ℕi:Fin n.succ.succx:Fin n.succ.succh:↑i ≠ ↑xh✝¹:¬↑x < ↑ih✝:↑x - 1 < ↑i⊢ ↑x - 1 = ↑xn:ℕi:Fin n.succ.succx:Fin n.succ.succh:↑i ≠ ↑xh✝¹:¬↑x < ↑ih✝:¬↑x - 1 < ↑i⊢ ↑x - 1 + 1 = ↑x n:ℕi:Fin n.succ.succx:Fin n.succ.succh:↑i ≠ ↑xh✝:↑x < ↑i⊢ ↑x = ↑xn:ℕi:Fin n.succ.succx:Fin n.succ.succh:↑i ≠ ↑xh✝¹:¬↑x < ↑ih✝:↑x - 1 < ↑i⊢ ↑x - 1 = ↑xn:ℕi:Fin n.succ.succx:Fin n.succ.succh:↑i ≠ ↑xh✝¹:¬↑x < ↑ih✝:¬↑x - 1 < ↑i⊢ ↑x - 1 + 1 = ↑x All goals completed! 🐙All goals completed! 🐙 n:ℕi:Fin n.succ.succx:Fin n.succ.succh✝:i ≠ xy:Fin n.succh:i.succAbove y = x⊢ y = predAboveI i x All goals completed! 🐙lemma predAboveI_lt {i x : Fin n.succ.succ} (h : x.val < i.val) : predAboveI i x = ⟨x.val, n:ℕi:Fin n.succ.succx:Fin n.succ.succh:↑x < ↑i⊢ ↑x < n.succ All goals completed! 🐙⟩ := n:ℕi:Fin n.succ.succx:Fin n.succ.succh:↑x < ↑i⊢ predAboveI i x = ⟨↑x, ⋯⟩ All goals completed! 🐙lemma predAboveI_ge {i x : Fin n.succ.succ} (h : i.val < x.val) : predAboveI i x = ⟨x.val - 1, n:ℕi:Fin n.succ.succx:Fin n.succ.succh:↑i < ↑x⊢ ↑x - 1 < n.succ All goals completed! 🐙⟩ := n:ℕi:Fin n.succ.succx:Fin n.succ.succh:↑i < ↑x⊢ predAboveI i x = ⟨↑x - 1, ⋯⟩ n:ℕi:Fin n.succ.succx:Fin n.succ.succh:↑i < ↑x⊢ x < i → ↑x = ↑x - 1 All goals completed! 🐙All goals completed! 🐙

The equivalence between Fin n.succ and Fin 1 ⊕ Fin n extracting the ith component.

def finExtractOne {n : ℕ} (i : Fin (n + 1)) : Fin (n + 1) ≃ Fin 1 ⊕ Fin n := (finCongr (n✝:ℕn:ℕi:Fin (n + 1)⊢ n.succ = ↑i + 1 + (n - ↑i) All goals completed! 🐙 : n.succ = i + 1 + (n - i))).trans <| finSumFinEquiv.symm.trans <| (Equiv.sumCongr (finSumFinEquiv.symm.trans (Equiv.sumComm (Fin i) (Fin 1))) (Equiv.refl (Fin (n-i)))).trans <| (Equiv.sumAssoc (Fin 1) (Fin i) (Fin (n - i))).trans <| Equiv.sumCongr (Equiv.refl (Fin 1)) (finSumFinEquiv.trans (finCongr (n✝:ℕn:ℕi:Fin (n + 1)⊢ ↑i + (n - ↑i) = n All goals completed! 🐙)))
n:ℕi:Fin n.succ⊢ i = (finExtractOne i).symm (Sum.inl 0) All goals completed! 🐙n:ℕi:Fin n.succx:Fin nhi:¬↑x < ↑ihp:n = ↑i + (n - ↑i)h1:finSumFinEquiv.symm (Fin.cast hp x) = Sum.inr ⟨↑x - ↑i, ⋯⟩⊢ ↑(finSumFinEquiv (Sum.map (⇑(finSumFinEquiv.symm.trans (Equiv.sumComm (Fin ↑i) (Fin 1))).symm) id ((Equiv.sumAssoc (Fin 1) (Fin ↑i) (Fin (n - ↑i))).symm (Sum.inr (Sum.inr ⟨↑x - ↑i, ⋯⟩))))) = ↑(if x.castSucc < i then x.castSucc else x.succ) n:ℕi:Fin n.succx:Fin nhi:¬↑x < ↑ihp:n = ↑i + (n - ↑i)h1:finSumFinEquiv.symm (Fin.cast hp x) = Sum.inr ⟨↑x - ↑i, ⋯⟩h✝:x.castSucc < i⊢ ↑(finSumFinEquiv (Sum.map (⇑(finSumFinEquiv.symm.trans (Equiv.sumComm (Fin ↑i) (Fin 1))).symm) id ((Equiv.sumAssoc (Fin 1) (Fin ↑i) (Fin (n - ↑i))).symm (Sum.inr (Sum.inr ⟨↑x - ↑i, ⋯⟩))))) = ↑x.castSuccn:ℕi:Fin n.succx:Fin nhi:¬↑x < ↑ihp:n = ↑i + (n - ↑i)h1:finSumFinEquiv.symm (Fin.cast hp x) = Sum.inr ⟨↑x - ↑i, ⋯⟩h✝:¬x.castSucc < i⊢ ↑(finSumFinEquiv (Sum.map (⇑(finSumFinEquiv.symm.trans (Equiv.sumComm (Fin ↑i) (Fin 1))).symm) id ((Equiv.sumAssoc (Fin 1) (Fin ↑i) (Fin (n - ↑i))).symm (Sum.inr (Sum.inr ⟨↑x - ↑i, ⋯⟩))))) = ↑x.succ n:ℕi:Fin n.succx:Fin nhi:¬↑x < ↑ihp:n = ↑i + (n - ↑i)h1:finSumFinEquiv.symm (Fin.cast hp x) = Sum.inr ⟨↑x - ↑i, ⋯⟩h✝:x.castSucc < i⊢ ↑(finSumFinEquiv (Sum.map (⇑(finSumFinEquiv.symm.trans (Equiv.sumComm (Fin ↑i) (Fin 1))).symm) id ((Equiv.sumAssoc (Fin 1) (Fin ↑i) (Fin (n - ↑i))).symm (Sum.inr (Sum.inr ⟨↑x - ↑i, ⋯⟩))))) = ↑x.castSucc n:ℕi:Fin n.succx:Fin nhi:¬↑x < ↑ihp:n = ↑i + (n - ↑i)h1:finSumFinEquiv.symm (Fin.cast hp x) = Sum.inr ⟨↑x - ↑i, ⋯⟩hn:x.castSucc < i⊢ ↑(finSumFinEquiv (Sum.map (⇑(finSumFinEquiv.symm.trans (Equiv.sumComm (Fin ↑i) (Fin 1))).symm) id ((Equiv.sumAssoc (Fin 1) (Fin ↑i) (Fin (n - ↑i))).symm (Sum.inr (Sum.inr ⟨↑x - ↑i, ⋯⟩))))) = ↑x.castSucc All goals completed! 🐙 n:ℕi:Fin n.succx:Fin nhi:¬↑x < ↑ihp:n = ↑i + (n - ↑i)h1:finSumFinEquiv.symm (Fin.cast hp x) = Sum.inr ⟨↑x - ↑i, ⋯⟩h✝:¬x.castSucc < i⊢ ↑i + 1 + (↑x - ↑i) = ↑x + 1 All goals completed! 🐙All goals completed! 🐙@[simp] lemma finExtractOne_symm_inl_apply {n : ℕ} (i : Fin n.succ) : (finExtractOne i).symm (Sum.inl 0) = i := n:ℕi:Fin n.succ⊢ (finExtractOne i).symm (Sum.inl 0) = i All goals completed! 🐙lemma finExtractOne_apply_neq {n : ℕ} (i j : Fin (n + 1 + 1)) (hij : i ≠ j) : finExtractOne i j = Sum.inr (predAboveI i j) := n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j⊢ (finExtractOne i) j = Sum.inr (predAboveI i j) n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j⊢ Sum.inr (predAboveI i j) = (finExtractOne i) j n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j⊢ (finExtractOne i).symm (Sum.inr (predAboveI i j)) = j n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j⊢ i.succAbove (predAboveI i j) = j All goals completed! 🐙

Given an equivalence Fin n.succ.succ ≃ Fin n.succ.succ, and an i : Fin n.succ.succ, the map Fin n.succ → Fin n.succ obtained by dropping i and it's image.

def finExtractOnPermHom {m : ℕ} (i : Fin n.succ.succ) (σ : Fin n.succ.succ ≃ Fin m.succ.succ) : Fin n.succ → Fin m.succ := fun x => predAboveI (σ i) (σ ((finExtractOne i).symm (Sum.inr x)))
n:ℕm:ℕi:Fin n.succ.succσ:Fin n.succ.succ ≃ Fin m.succ.succx:Fin n.succhσ:σ i ≠ σ (i.succAbove x)⊢ (finExtractOnPermHom (σ i) σ.symm ∘ finExtractOnPermHom i σ) x = id x All goals completed! 🐙

Given an equivalence Fin n.succ.succ ≃ Fin n.succ.succ, and an i : Fin n.succ.succ, the equivalence Fin n.succ ≃ Fin n.succ obtained by dropping i and it's image.

def finExtractOnePerm {m : ℕ} (i : Fin n.succ.succ) (σ : Fin n.succ.succ ≃ Fin m.succ.succ) : Fin n.succ ≃ Fin m.succ where toFun x := finExtractOnPermHom i σ x invFun x := finExtractOnPermHom (σ i) σ.symm x left_inv x := n:ℕm:ℕi:Fin n.succ.succσ:Fin n.succ.succ ≃ Fin m.succ.succx:Fin n.succ⊢ (fun x => finExtractOnPermHom (σ i) σ.symm x) ((fun x => finExtractOnPermHom i σ x) x) = x All goals completed! 🐙 right_inv x := n:ℕm:ℕi:Fin n.succ.succσ:Fin n.succ.succ ≃ Fin m.succ.succx:Fin m.succ⊢ (fun x => finExtractOnPermHom i σ x) ((fun x => finExtractOnPermHom (σ i) σ.symm x) x) = x All goals completed! 🐙
n:ℕm:ℕe:Fin n.succ.succ ≃ Fin m.succ.succi:Fin n.succ.succx:Fin (n + 1)hσ:e i ≠ e (i.succAbove x)⊢ (⇑e ∘ i.succAbove) x = ((e i).succAbove ∘ ⇑(finExtractOnePerm i e)) x All goals completed! 🐙@[simp] lemma finExtractOnePerm_apply (i : Fin n.succ.succ) (σ : Fin n.succ.succ ≃ Fin n.succ.succ) (x : Fin n.succ) : finExtractOnePerm i σ x = predAboveI (σ i) (σ ((finExtractOne i).symm (Sum.inr x))) := rfl@[simp] lemma finExtractOnePerm_symm_apply (i : Fin n.succ.succ) (σ : Fin n.succ.succ ≃ Fin n.succ.succ) (x : Fin n.succ) : (finExtractOnePerm i σ).symm x = predAboveI (σ.symm (σ i)) (σ.symm ((finExtractOne (σ i)).symm (Sum.inr x))) := rfl

The equivalence of types Fin n.succ.succ ≃ (Fin 1 ⊕ Fin 1) ⊕ Fin n extracting the i and (i.succAbove j).

def finExtractTwo {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ) : Fin n.succ.succ ≃ (Fin 1 ⊕ Fin 1) ⊕ Fin n := (finExtractOne i).trans <| (Equiv.sumCongr (Equiv.refl (Fin 1)) (finExtractOne j)).trans <| (Equiv.sumAssoc (Fin 1) (Fin 1) (Fin n)).symm
@[simp] lemma finExtractTwo_apply_fst {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ) : finExtractTwo i j i = Sum.inl (Sum.inl 0) := n:ℕi:Fin n.succ.succj:Fin n.succ⊢ (finExtractTwo i j) i = Sum.inl (Sum.inl 0) All goals completed! 🐙lemma finExtractTwo_symm_inr {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ) : (finExtractTwo i j).symm ∘ Sum.inr = i.succAbove ∘ j.succAbove := n:ℕi:Fin n.succ.succj:Fin n.succ⊢ ⇑(finExtractTwo i j).symm ∘ Sum.inr = i.succAbove ∘ j.succAbove n:ℕi:Fin n.succ.succj:Fin n.succx:Fin n⊢ (⇑(finExtractTwo i j).symm ∘ Sum.inr) x = (i.succAbove ∘ j.succAbove) x All goals completed! 🐙@[simp] lemma finExtractTwo_symm_inr_apply {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ) (x : Fin n) : (finExtractTwo i j).symm (Sum.inr x) = i.succAbove (j.succAbove x) := n:ℕi:Fin n.succ.succj:Fin n.succx:Fin n⊢ (finExtractTwo i j).symm (Sum.inr x) = i.succAbove (j.succAbove x) All goals completed! 🐙@[simp] lemma finExtractTwo_symm_inl_inr_apply {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ) : (finExtractTwo i j).symm (Sum.inl (Sum.inr 0)) = i.succAbove j := n:ℕi:Fin n.succ.succj:Fin n.succ⊢ (finExtractTwo i j).symm (Sum.inl (Sum.inr 0)) = i.succAbove j All goals completed! 🐙@[simp] lemma finExtractTwo_symm_inl_inl_apply {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ) : (finExtractTwo i j).symm (Sum.inl (Sum.inl 0)) = i := n:ℕi:Fin n.succ.succj:Fin n.succ⊢ (finExtractTwo i j).symm (Sum.inl (Sum.inl 0)) = i All goals completed! 🐙@[simp] lemma finExtractTwo_apply_snd {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ) : finExtractTwo i j (i.succAbove j) = Sum.inl (Sum.inr 0) := n:ℕi:Fin n.succ.succj:Fin n.succ⊢ (finExtractTwo i j) (i.succAbove j) = Sum.inl (Sum.inr 0) All goals completed! 🐙

Takes two maps Fin n → Fin n and returns the equivalence they form.

def finMapToEquiv (f1 : Fin n → Fin m) (f2 : Fin m → Fin n) (h : ∀ x, f1 (f2 x) = x := by decide) (h' : ∀ x, f2 (f1 x) = x := by decide) : Fin n ≃ Fin m where toFun := f1 invFun := f2 left_inv := h' right_inv := h
@[simp] lemma finMapToEquiv_apply {f1 : Fin n → Fin m} {f2 : Fin m → Fin n} {h : ∀ x, f1 (f2 x) = x} {h' : ∀ x, f2 (f1 x) = x} (x : Fin n) : finMapToEquiv f1 f2 h h' x = f1 x := rfl@[simp] lemma finMapToEquiv_symm_apply {f1 : Fin n → Fin m} {f2 : Fin m → Fin n} {h : ∀ x, f1 (f2 x) = x} {h' : ∀ x, f2 (f1 x) = x} (x : Fin m) : (finMapToEquiv f1 f2 h h').symm x = f2 x := rfllemma finMapToEquiv_symm_eq {f1 : Fin n → Fin m} {f2 : Fin m → Fin n} {h : ∀ x, f1 (f2 x) = x} {h' : ∀ x, f2 (f1 x) = x} : (finMapToEquiv f1 f2 h h').symm = finMapToEquiv f2 f1 h' h := rfl

Given an equivalence between Fin n and Fin m, the induced equivalence between Fin n.succ and Fin m.succ derived by Fin.cons.

def equivCons {n m : ℕ} (e : Fin n ≃ Fin m) : Fin n.succ ≃ Fin m.succ where toFun := Fin.cons 0 (Fin.succ ∘ e.toFun) invFun := Fin.cons 0 (Fin.succ ∘ e.invFun) left_inv i := n✝:ℕn:ℕm:ℕe:Fin n ≃ Fin mi:Fin n.succ⊢ Fin.cons 0 (Fin.succ ∘ e.invFun) (Fin.cons 0 (Fin.succ ∘ e.toFun) i) = i n✝:ℕn:ℕm:ℕe:Fin n ≃ Fin m⊢ Fin.cons 0 (Fin.succ ∘ e.invFun) (Fin.cons 0 (Fin.succ ∘ e.toFun) 0) = 0n✝:ℕn:ℕm:ℕe:Fin n ≃ Fin mi✝:Fin n⊢ Fin.cons 0 (Fin.succ ∘ e.invFun) (Fin.cons 0 (Fin.succ ∘ e.toFun) i✝.succ) = i✝.succ n✝:ℕn:ℕm:ℕe:Fin n ≃ Fin m⊢ Fin.cons 0 (Fin.succ ∘ e.invFun) (Fin.cons 0 (Fin.succ ∘ e.toFun) 0) = 0n✝:ℕn:ℕm:ℕe:Fin n ≃ Fin mi✝:Fin n⊢ Fin.cons 0 (Fin.succ ∘ e.invFun) (Fin.cons 0 (Fin.succ ∘ e.toFun) i✝.succ) = i✝.succ All goals completed! 🐙 right_inv i := n✝:ℕn:ℕm:ℕe:Fin n ≃ Fin mi:Fin m.succ⊢ Fin.cons 0 (Fin.succ ∘ e.toFun) (Fin.cons 0 (Fin.succ ∘ e.invFun) i) = i n✝:ℕn:ℕm:ℕe:Fin n ≃ Fin m⊢ Fin.cons 0 (Fin.succ ∘ e.toFun) (Fin.cons 0 (Fin.succ ∘ e.invFun) 0) = 0n✝:ℕn:ℕm:ℕe:Fin n ≃ Fin mi✝:Fin m⊢ Fin.cons 0 (Fin.succ ∘ e.toFun) (Fin.cons 0 (Fin.succ ∘ e.invFun) i✝.succ) = i✝.succ n✝:ℕn:ℕm:ℕe:Fin n ≃ Fin m⊢ Fin.cons 0 (Fin.succ ∘ e.toFun) (Fin.cons 0 (Fin.succ ∘ e.invFun) 0) = 0n✝:ℕn:ℕm:ℕe:Fin n ≃ Fin mi✝:Fin m⊢ Fin.cons 0 (Fin.succ ∘ e.toFun) (Fin.cons 0 (Fin.succ ∘ e.invFun) i✝.succ) = i✝.succ All goals completed! 🐙
@[simp] lemma equivCons_zero {n m : ℕ} (e : Fin n ≃ Fin m) : equivCons e 0 = 0 := rfl@[simp] lemma equivCons_trans {n m k : ℕ} (e : Fin n ≃ Fin m) (f : Fin m ≃ Fin k) : Fin.equivCons (e.trans f) = (Fin.equivCons e).trans (Fin.equivCons f) := n:ℕm:ℕk:ℕe:Fin n ≃ Fin mf:Fin m ≃ Fin k⊢ equivCons (e.trans f) = (equivCons e).trans (equivCons f) n:ℕm:ℕk:ℕe:Fin n ≃ Fin mf:Fin m ≃ Fin kx:Fin n.succ⊢ ↑((equivCons (e.trans f)) x) = ↑(((equivCons e).trans (equivCons f)) x) n:ℕm:ℕk:ℕe:Fin n ≃ Fin mf:Fin m ≃ Fin k⊢ ↑((equivCons (e.trans f)) 0) = ↑(((equivCons e).trans (equivCons f)) 0)n:ℕm:ℕk:ℕe:Fin n ≃ Fin mf:Fin m ≃ Fin ki✝:Fin n⊢ ↑((equivCons (e.trans f)) i✝.succ) = ↑(((equivCons e).trans (equivCons f)) i✝.succ) n:ℕm:ℕk:ℕe:Fin n ≃ Fin mf:Fin m ≃ Fin k⊢ ↑((equivCons (e.trans f)) 0) = ↑(((equivCons e).trans (equivCons f)) 0)n:ℕm:ℕk:ℕe:Fin n ≃ Fin mf:Fin m ≃ Fin ki✝:Fin n⊢ ↑((equivCons (e.trans f)) i✝.succ) = ↑(((equivCons e).trans (equivCons f)) i✝.succ) All goals completed! 🐙@[simp] lemma equivCons_castOrderIso {n m : ℕ} (h : n = m) : (Fin.equivCons (Fin.castOrderIso h).toEquiv) = (Fin.castOrderIso (n✝:ℕn:ℕm:ℕh:n = m⊢ n.succ = m.succ All goals completed! 🐙)).toEquiv := n:ℕm:ℕh:n = m⊢ equivCons (Fin.castOrderIso h).toEquiv = (Fin.castOrderIso ⋯).toEquiv n:ℕm:ℕh:n = mx:Fin n.succ⊢ ↑((equivCons (Fin.castOrderIso h).toEquiv) x) = ↑((Fin.castOrderIso ⋯).toEquiv x) n:ℕm:ℕh:n = m⊢ ↑((equivCons (Fin.castOrderIso h).toEquiv) 0) = ↑((Fin.castOrderIso ⋯).toEquiv 0)n:ℕm:ℕh:n = mi✝:Fin n⊢ ↑((equivCons (Fin.castOrderIso h).toEquiv) i✝.succ) = ↑((Fin.castOrderIso ⋯).toEquiv i✝.succ) n:ℕm:ℕh:n = m⊢ ↑((equivCons (Fin.castOrderIso h).toEquiv) 0) = ↑((Fin.castOrderIso ⋯).toEquiv 0)n:ℕm:ℕh:n = mi✝:Fin n⊢ ↑((equivCons (Fin.castOrderIso h).toEquiv) i✝.succ) = ↑((Fin.castOrderIso ⋯).toEquiv i✝.succ) All goals completed! 🐙@[simp] lemma equivCons_symm_succ {n m : ℕ} (e : Fin n ≃ Fin m) (i : ℕ) (hi : i + 1 < m.succ) : (Fin.equivCons e).symm ⟨i + 1, hi⟩ = (e.symm ⟨i, Nat.succ_lt_succ_iff.mp hi⟩).succ := rfl@[simp] lemma equivCons_succ {n m : ℕ} (e : Fin n ≃ Fin m) (i : ℕ) (hi : i + 1 < n.succ) : (Fin.equivCons e) ⟨i + 1, hi⟩ = (e ⟨i, Nat.succ_lt_succ_iff.mp hi⟩).succ := rfl