1. Physlib
  2. Relativity
  3. Tensors
  4. Contraction
  5. SuccSuccAbove
Imports
/- Copyright (c) 2025 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.Data.Finset.Sort public import Mathlib.Data.Nat.SuccPred

Defining succSuccAbove

In Mathlib there is the Fin.succAbove function which gives an embedding of Fin n into Fin (n + 1) by leaving a hole at a specified index. We will need a version of this which gives an embedding of Fin n into Fin (n + 1 + 1) by leaving holes at two specified indices. We call this succSuccAbove.

We will also need an explicit inverse of this map from Fin (n + 1 + 1) to Fin n which is defined on the complement of the two specified indices. This is similar to Fin.predAbove (although not exactly the same), for this reason we call it predPredAbove.

Implementation

In previous versions of Physlib the function which is now called succSuccAbove was previously called dropPairEmb and the function which is now called predPredAbove was previously called dropPairEmbPre.

@[expose] public section

Defining succSuccAbove

The definition below is deliberately explicit. Later lemmas identify it with Finset.orderEmbOfFin and Finset.orderIsoOfFin, giving a bridge to the Mathlib API while keeping this form convenient for computation and goals solved by decide.

The embedding of Fin n into Fin (n + 1 + 1) which leaves a hole at i and j.

def succSuccAbove (i j : Fin (n + 1 + 1)) (m : Fin n) : Fin (n + 1 + 1) := if m.1 < i.1 ∧ m.1 < j.1 then ⟨m, C:Sort ?u.15n:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)m:Fin n⊢ ↑m < n + 1 + 1 All goals completed! 🐙⟩ else if m.1 + 1 < i.1 ∧ j.1 ≤ m.1 then ⟨m + 1, C:Sort ?u.15n:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)m:Fin n⊢ ↑m + 1 < n + 1 + 1 All goals completed! 🐙⟩ else if i.1 ≤ m.1 ∧ m.1 + 1 < j.1 then ⟨m + 1, C:Sort ?u.15n:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)m:Fin n⊢ ↑m + 1 < n + 1 + 1 All goals completed! 🐙⟩ else ⟨m + 2, C:Sort ?u.15n:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)m:Fin n⊢ ↑m + 2 < n + 1 + 1 All goals completed! 🐙⟩
lemma succSuccAbove_val (i j : Fin (n + 1 + 1)) (m : Fin n) : (succSuccAbove i j m).val = if m.1 < i.1 ∧ m.1 < j.1 then m.1 else if m.1 + 1 < i.1 ∧ j.1 ≤ m.1 then m.1 + 1 else if i.1 ≤ m.1 ∧ m.1 + 1 < j.1 then m.1 + 1 else m.1 + 2 := n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)m:Fin n⊢ ↑(i.succSuccAbove j m) = if ↑m < ↑i ∧ ↑m < ↑j then ↑m else if ↑m + 1 < ↑i ∧ ↑j ≤ ↑m then ↑m + 1 else if ↑i ≤ ↑m ∧ ↑m + 1 < ↑j then ↑m + 1 else ↑m + 2 n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)m:Fin n⊢ ↑(if ↑m < ↑i ∧ ↑m < ↑j then ⟨↑m, ⋯⟩ else if ↑m + 1 < ↑i ∧ ↑j ≤ ↑m then ⟨↑m + 1, ⋯⟩ else if ↑i ≤ ↑m ∧ ↑m + 1 < ↑j then ⟨↑m + 1, ⋯⟩ else ⟨↑m + 2, ⋯⟩) = if ↑m < ↑i ∧ ↑m < ↑j then ↑m else if ↑m + 1 < ↑i ∧ ↑j ≤ ↑m then ↑m + 1 else if ↑i ≤ ↑m ∧ ↑m + 1 < ↑j then ↑m + 1 else ↑m + 2 All goals completed! 🐙lemma succSuccAbove_self_apply (i : Fin (n + 1 + 1)) (m : Fin n) : succSuccAbove i i m = if m.1 < i.1 then ⟨m.1, C:Sort ?u.15n:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)m:Fin n⊢ ↑m < n + 1 + 1 All goals completed! 🐙⟩ else ⟨m.1 + 2, C:Sort ?u.15n:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)m:Fin n⊢ ↑m + 2 < n + 1 + 1 All goals completed! 🐙⟩ := n:ℕi:Fin (n + 1 + 1)m:Fin n⊢ i.succSuccAbove i m = if ↑m < ↑i then ⟨↑m, ⋯⟩ else ⟨↑m + 2, ⋯⟩ n:ℕi:Fin (n + 1 + 1)m:Fin n⊢ (if ↑m < ↑i then ⟨↑m, ⋯⟩ else if ↑m + 1 < ↑i ∧ ↑i ≤ ↑m then ⟨↑m + 1, ⋯⟩ else if ↑i ≤ ↑m ∧ ↑m + 1 < ↑i then ⟨↑m + 1, ⋯⟩ else ⟨↑m + 2, ⋯⟩) = if ↑m < ↑i then ⟨↑m, ⋯⟩ else ⟨↑m + 2, ⋯⟩ All goals completed! 🐙lemma succSuccAbove_eq_succAbove_succAbove (i : Fin (n + 1 + 1)) (j : Fin (n + 1)) : succSuccAbove i (i.succAbove j) = i.succAbove ∘ j.succAbove := n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1)⊢ i.succSuccAbove (i.succAbove j) = i.succAbove ∘ j.succAbove n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1)m:Fin n⊢ ↑(i.succSuccAbove (i.succAbove j) m) = ↑((i.succAbove ∘ j.succAbove) m) n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1)m:Fin n⊢ ↑(if ↑m < ↑i ∧ ↑m < ↑(if ↑j < ↑i then j.castSucc else j.succ) then ⟨↑m, ⋯⟩ else if ↑m + 1 < ↑i ∧ ↑(if ↑j < ↑i then j.castSucc else j.succ) ≤ ↑m then ⟨↑m + 1, ⋯⟩ else if ↑i ≤ ↑m ∧ ↑m + 1 < ↑(if ↑j < ↑i then j.castSucc else j.succ) then ⟨↑m + 1, ⋯⟩ else ⟨↑m + 2, ⋯⟩) = ↑(if ↑(if ↑m < ↑j then m.castSucc else m.succ) < ↑i then (if ↑m < ↑j then m.castSucc else m.succ).castSucc else (if ↑m < ↑j then m.castSucc else m.succ).succ) All goals completed! 🐙n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1)hij:i ≠ i.succAbove jx:Fin nhi:i ≠ 0h:i.succAbove j ≤ (i.pred hi).castSucc⊢ i.succAbove j < i All goals completed! 🐙lemma succSuccAbove_injective {n : ℕ} (i j : Fin (n + 1 + 1)) : Function.Injective (succSuccAbove i j) := n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)⊢ Function.Injective (i.succSuccAbove j) n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)a:Fin nb:Fin n⊢ i.succSuccAbove j a = i.succSuccAbove j b → a = b n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)a:Fin nb:Fin n⊢ ((if ↑a < ↑i ∧ ↑a < ↑j then ↑a else if ↑a + 1 < ↑i ∧ ↑j ≤ ↑a then ↑a + 1 else if ↑i ≤ ↑a ∧ ↑a + 1 < ↑j then ↑a + 1 else ↑a + 2) = if ↑b < ↑i ∧ ↑b < ↑j then ↑b else if ↑b + 1 < ↑i ∧ ↑j ≤ ↑b then ↑b + 1 else if ↑i ≤ ↑b ∧ ↑b + 1 < ↑j then ↑b + 1 else ↑b + 2) → ↑a = ↑b All goals completed! 🐙All goals completed! 🐙@[simp] lemma succSuccAbove_leq_iff_leq {n : ℕ} (i j : Fin (n + 1 + 1)) (m1 m2 : Fin n) : succSuccAbove i j m1 ≤ succSuccAbove i j m2 ↔ m1 ≤ m2 := n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)m1:Fin nm2:Fin n⊢ i.succSuccAbove j m1 ≤ i.succSuccAbove j m2 ↔ m1 ≤ m2 n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)m1:Fin nm2:Fin n⊢ ((if ↑m1 < ↑i ∧ ↑m1 < ↑j then ↑m1 else if ↑m1 + 1 < ↑i ∧ ↑j ≤ ↑m1 then ↑m1 + 1 else if ↑i ≤ ↑m1 ∧ ↑m1 + 1 < ↑j then ↑m1 + 1 else ↑m1 + 2) ≤ if ↑m2 < ↑i ∧ ↑m2 < ↑j then ↑m2 else if ↑m2 + 1 < ↑i ∧ ↑j ≤ ↑m2 then ↑m2 + 1 else if ↑i ≤ ↑m2 ∧ ↑m2 + 1 < ↑j then ↑m2 + 1 else ↑m2 + 2) ↔ ↑m1 ≤ ↑m2 All goals completed! 🐙@[simp] lemma succSuccAbove_lt_iff_lt {n : ℕ} (i j : Fin (n + 1 + 1)) (m1 m2 : Fin n) : succSuccAbove i j m1 < succSuccAbove i j m2 ↔ m1 < m2 := n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)m1:Fin nm2:Fin n⊢ i.succSuccAbove j m1 < i.succSuccAbove j m2 ↔ m1 < m2 n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)m1:Fin nm2:Fin n⊢ ((if ↑m1 < ↑i ∧ ↑m1 < ↑j then ↑m1 else if ↑m1 + 1 < ↑i ∧ ↑j ≤ ↑m1 then ↑m1 + 1 else if ↑i ≤ ↑m1 ∧ ↑m1 + 1 < ↑j then ↑m1 + 1 else ↑m1 + 2) < if ↑m2 < ↑i ∧ ↑m2 < ↑j then ↑m2 else if ↑m2 + 1 < ↑i ∧ ↑j ≤ ↑m2 then ↑m2 + 1 else if ↑i ≤ ↑m2 ∧ ↑m2 + 1 < ↑j then ↑m2 + 1 else ↑m2 + 2) ↔ ↑m1 < ↑m2 All goals completed! 🐙@[simp] lemma succSuccAbove_monotone {n : ℕ} (i j : Fin (n + 1 + 1)) : Monotone (succSuccAbove i j) := n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)⊢ Monotone (i.succSuccAbove j) n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)a:Fin nb:Fin n⊢ a ≤ b → i.succSuccAbove j a ≤ i.succSuccAbove j b All goals completed! 🐙lemma succSuccAbove_strictMono {n : ℕ} (i j : Fin (n + 1 + 1)) : StrictMono (succSuccAbove i j) := (succSuccAbove_monotone i j).strictMono_of_injective (succSuccAbove_injective i j)n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1)hij:i ≠ i.succAbove j⊢ i.succAbove '' {j}ᶜ = {i, i.succAbove j}ᶜ n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1)hij:i ≠ i.succAbove ja:Fin (n + 1 + 1)⊢ a ∈ i.succAbove '' {j}ᶜ ↔ a ∈ {i, i.succAbove j}ᶜ n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1)hij:i ≠ i.succAbove ja:Fin (n + 1 + 1)⊢ (∃ x, ¬x = j ∧ i.succAbove x = a) ↔ a ∉ {i, i.succAbove j} n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1)hij:i ≠ i.succAbove ja:Fin (n + 1 + 1)⊢ (∃ x, ¬x = j ∧ i.succAbove x = a) → a ∉ {i, i.succAbove j}n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1)hij:i ≠ i.succAbove ja:Fin (n + 1 + 1)⊢ a ∉ {i, i.succAbove j} → ∃ x, ¬x = j ∧ i.succAbove x = a n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1)hij:i ≠ i.succAbove ja:Fin (n + 1 + 1)⊢ (∃ x, ¬x = j ∧ i.succAbove x = a) → a ∉ {i, i.succAbove j} n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1)hij:i ≠ i.succAbove ja:Fin (n + 1 + 1)h:∃ x, ¬x = j ∧ i.succAbove x = a⊢ a ∉ {i, i.succAbove j} n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1)hij:i ≠ i.succAbove jb:Fin (n + 1)h1:¬b = j⊢ i.succAbove b ∉ {i, i.succAbove j} All goals completed! 🐙 n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1)hij:i ≠ i.succAbove ja:Fin (n + 1 + 1)⊢ a ∉ {i, i.succAbove j} → ∃ x, ¬x = j ∧ i.succAbove x = a n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1)hij:i ≠ i.succAbove ja:Fin (n + 1 + 1)h:a ∉ {i, i.succAbove j}⊢ ∃ x, ¬x = j ∧ i.succAbove x = a n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1)hij:i ≠ i.succAbove ja:Fin (n + 1 + 1)h:¬a = i ∧ ¬a = i.succAbove j⊢ ∃ x, ¬x = j ∧ i.succAbove x = a n:ℕj:Fin (n + 1)a:Fin (n + 1 + 1)hij:a ≠ a.succAbove jh:¬a = a ∧ ¬a = a.succAbove j⊢ ∃ x, ¬x = j ∧ a.succAbove x = an:ℕi:Fin (n + 1 + 1)j:Fin (n + 1)hij:i ≠ i.succAbove ja:Fin (n + 1)h:¬i.succAbove a = i ∧ ¬i.succAbove a = i.succAbove j⊢ ∃ x, ¬x = j ∧ i.succAbove x = i.succAbove a n:ℕj:Fin (n + 1)a:Fin (n + 1 + 1)hij:a ≠ a.succAbove jh:¬a = a ∧ ¬a = a.succAbove j⊢ ∃ x, ¬x = j ∧ a.succAbove x = a All goals completed! 🐙 n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1)hij:i ≠ i.succAbove ja:Fin (n + 1)h:¬i.succAbove a = i ∧ ¬i.succAbove a = i.succAbove j⊢ ¬a = j ∧ i.succAbove a = i.succAbove a All goals completed! 🐙C:Sort ?u.15n✝:ℕc:Fin (n✝ + 1 + 1) → Cn:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j⊢ Fintype.card (Fin (n + 1 + 1)) - {i, j}.card = n; All goals completed! 🐙) := n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j⊢ i.succSuccAbove j = ⇑({i, j}ᶜ.orderEmbOfFin ⋯) n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j⊢ Set.range (i.succSuccAbove j) = Set.range ⇑({i, j}ᶜ.orderEmbOfFin ⋯) All goals completed! 🐙lemma succSuccAbove_symm (i j : Fin (n + 1 + 1)) : succSuccAbove i j = succSuccAbove j i := n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)⊢ i.succSuccAbove j = j.succSuccAbove i n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)m:Fin n⊢ ↑(i.succSuccAbove j m) = ↑(j.succSuccAbove i m) n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)m:Fin n⊢ (if ↑m < ↑i ∧ ↑m < ↑j then ↑m else if ↑m + 1 < ↑i ∧ ↑j ≤ ↑m then ↑m + 1 else if ↑i ≤ ↑m ∧ ↑m + 1 < ↑j then ↑m + 1 else ↑m + 2) = if ↑m < ↑j ∧ ↑m < ↑i then ↑m else if ↑m + 1 < ↑j ∧ ↑i ≤ ↑m then ↑m + 1 else if ↑j ≤ ↑m ∧ ↑m + 1 < ↑i then ↑m + 1 else ↑m + 2 All goals completed! 🐙All goals completed! 🐙C:Sort ?u.15n:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jm:Fin n⊢ Fintype.card (Fin (n + 1 + 1)) - {i, j}.card = n; All goals completed! 🐙)) m := n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jm:Fin n⊢ i.succSuccAbove j m = ↑(({i, j}ᶜ.orderIsoOfFin ⋯) m) All goals completed! 🐙n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jX:Set (Fin n)⊢ i.succSuccAbove j '' Xᶜᶜ ∪ (Set.range (i.succSuccAbove j))ᶜ = ({i, j} ∪ i.succSuccAbove j '' X)ᶜᶜ n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jX:Set (Fin n)⊢ i.succSuccAbove j '' X ∪ {i, j} = {i, j} ∪ i.succSuccAbove j '' X All goals completed! 🐙@[simp] lemma fst_ne_succSuccAbove_pre (i j : Fin (n + 1 + 1)) (m : Fin n) : ¬ i = succSuccAbove i j m := n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)m:Fin n⊢ ¬i = i.succSuccAbove j m n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)m:Fin n⊢ ¬↑i = if ↑m < ↑i ∧ ↑m < ↑j then ↑m else if ↑m + 1 < ↑i ∧ ↑j ≤ ↑m then ↑m + 1 else if ↑i ≤ ↑m ∧ ↑m + 1 < ↑j then ↑m + 1 else ↑m + 2 All goals completed! 🐙@[simp] lemma succSuccAbove_ne_fst (i j : Fin (n + 1 + 1)) (m : Fin n) : ¬ succSuccAbove i j m = i := n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)m:Fin n⊢ ¬i.succSuccAbove j m = i n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)m:Fin n⊢ ¬(if ↑m < ↑i ∧ ↑m < ↑j then ↑m else if ↑m + 1 < ↑i ∧ ↑j ≤ ↑m then ↑m + 1 else if ↑i ≤ ↑m ∧ ↑m + 1 < ↑j then ↑m + 1 else ↑m + 2) = ↑i All goals completed! 🐙n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)m:Fin n⊢ ¬j = j.succSuccAbove i m All goals completed! 🐙@[simp] lemma succSuccAbove_ne_snd (i j : Fin (n + 1 + 1)) (m : Fin n) : ¬ succSuccAbove i j m = j := n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)m:Fin n⊢ ¬i.succSuccAbove j m = j n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)m:Fin n⊢ j ≠ i.succSuccAbove j m All goals completed! 🐙n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jm':Fin nh:¬i.succSuccAbove j m' = ih':¬i.succSuccAbove j m' = j⊢ i.succSuccAbove j m' = i ∨ i.succSuccAbove j m' = j ∨ ∃ m'_1, i.succSuccAbove j m' = i.succSuccAbove j m'_1 All goals completed! 🐙lemma succSuccAbove_apply_lt_lt {n : ℕ} (i j : Fin (n + 1 + 1)) (m : Fin n) (hi : m.val < i.val) (hj : m.val < j.val) : succSuccAbove i j m = m.castSucc.castSucc := n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)m:Fin nhi:↑m < ↑ihj:↑m < ↑j⊢ i.succSuccAbove j m = m.castSucc.castSucc n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)m:Fin nhi:↑m < ↑ihj:↑m < ↑j⊢ ↑(i.succSuccAbove j m) = ↑m.castSucc.castSucc All goals completed! 🐙lemma succSuccAbove_natAdd_apply_castAdd {n n1 : ℕ} (i j : Fin (n + 1 + 1)) (m : Fin n1) : (succSuccAbove (n := n1 + n) (Fin.natAdd n1 i) (Fin.natAdd n1 j)) (Fin.castAdd n m) = Fin.castAdd (n + 1 + 1) (m) := n:ℕn1:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)m:Fin n1⊢ (natAdd n1 i).succSuccAbove (natAdd n1 j) (castAdd n m) = castAdd (n + 1 + 1) m n:ℕn1:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)m:Fin n1⊢ (if ↑(castLE ⋯ m) < n1 + ↑i ∧ ↑(castLE ⋯ m) < n1 + ↑j then ↑(castLE ⋯ m) else if ↑(castLE ⋯ m) + 1 < n1 + ↑i ∧ n1 + ↑j ≤ ↑(castLE ⋯ m) then ↑(castLE ⋯ m) + 1 else if n1 + ↑i ≤ ↑(castLE ⋯ m) ∧ ↑(castLE ⋯ m) + 1 < n1 + ↑j then ↑(castLE ⋯ m) + 1 else ↑(castLE ⋯ m) + 2) = ↑(castLE ⋯ m) All goals completed! 🐙

Reinserting a left-block survivor a after removing the i-th slot of the left block and the j-th slot of the right block of Fin ((nA + 1) + (nB + 1)), the removal read at the contracted length (nA + nB) + 1 + 1. Unlike succSuccAbove_natAdd_apply_castAdd the two holes straddle the two blocks, so the statement carries the reshaping Fin.casts.

lemma succSuccAbove_castAdd_natAdd_apply_castAdd {nA nB : ℕ} (i : Fin (nA + 1)) (j : Fin (nB + 1)) (a : Fin nA) : Fin.cast (show (nA + nB) + 1 + 1 = (nA + 1) + (nB + 1) All goals completed! 🐙 All goals completed! 🐙) ((Fin.cast (show (nA + 1) + (nB + 1) = (nA + nB) + 1 + 1 All goals completed! 🐙 All goals completed! 🐙) (Fin.castAdd (nB + 1) i)).succSuccAbove (Fin.cast (show (nA + 1) + (nB + 1) = (nA + nB) + 1 + 1 All goals completed! 🐙 All goals completed! 🐙) (Fin.natAdd (nA + 1) j)) (Fin.castAdd nB a)) = Fin.castAdd (nB + 1) (i.succAbove a) := nA:ℕnB:ℕi:Fin (nA + 1)j:Fin (nB + 1)a:Fin nA⊢ Fin.cast ⋯ ((Fin.cast ⋯ (castAdd (nB + 1) i)).succSuccAbove (Fin.cast ⋯ (natAdd (nA + 1) j)) (castAdd nB a)) = castAdd (nB + 1) (i.succAbove a) nA:ℕnB:ℕi:Fin (nA + 1)j:Fin (nB + 1)a:Fin nA⊢ ↑(Fin.cast ⋯ ((Fin.cast ⋯ (castAdd (nB + 1) i)).succSuccAbove (Fin.cast ⋯ (natAdd (nA + 1) j)) (castAdd nB a))) = ↑(castAdd (nB + 1) (i.succAbove a)) nA:ℕnB:ℕi:Fin (nA + 1)j:Fin (nB + 1)a:Fin nA⊢ (if ↑a < ↑i ∧ ↑a < nA + 1 + ↑j then ↑a else if ↑a + 1 < ↑i ∧ nA + 1 + ↑j ≤ ↑a then ↑a + 1 else if ↑i ≤ ↑a ∧ ↑a + 1 < nA + 1 + ↑j then ↑a + 1 else ↑a + 2) = if ↑a < ↑i then ↑a else ↑a + 1 nA:ℕnB:ℕi:Fin (nA + 1)j:Fin (nB + 1)a:Fin nAh✝¹:↑a < ↑i ∧ ↑a < nA + 1 + ↑jh✝:↑a < ↑i⊢ ↑a = ↑anA:ℕnB:ℕi:Fin (nA + 1)j:Fin (nB + 1)a:Fin nAh✝¹:↑a < ↑i ∧ ↑a < nA + 1 + ↑jh✝:¬↑a < ↑i⊢ ↑a = ↑a + 1nA:ℕnB:ℕi:Fin (nA + 1)j:Fin (nB + 1)a:Fin nAh✝²:¬(↑a < ↑i ∧ ↑a < nA + 1 + ↑j)h✝¹:↑a + 1 < ↑i ∧ nA + 1 + ↑j ≤ ↑ah✝:↑a < ↑i⊢ ↑a + 1 = ↑anA:ℕnB:ℕi:Fin (nA + 1)j:Fin (nB + 1)a:Fin nAh✝²:¬(↑a < ↑i ∧ ↑a < nA + 1 + ↑j)h✝¹:↑a + 1 < ↑i ∧ nA + 1 + ↑j ≤ ↑ah✝:¬↑a < ↑i⊢ ↑a + 1 = ↑a + 1nA:ℕnB:ℕi:Fin (nA + 1)j:Fin (nB + 1)a:Fin nAh✝³:¬(↑a < ↑i ∧ ↑a < nA + 1 + ↑j)h✝²:¬(↑a + 1 < ↑i ∧ nA + 1 + ↑j ≤ ↑a)h✝¹:↑i ≤ ↑a ∧ ↑a + 1 < nA + 1 + ↑jh✝:↑a < ↑i⊢ ↑a + 1 = ↑anA:ℕnB:ℕi:Fin (nA + 1)j:Fin (nB + 1)a:Fin nAh✝³:¬(↑a < ↑i ∧ ↑a < nA + 1 + ↑j)h✝²:¬(↑a + 1 < ↑i ∧ nA + 1 + ↑j ≤ ↑a)h✝¹:↑i ≤ ↑a ∧ ↑a + 1 < nA + 1 + ↑jh✝:¬↑a < ↑i⊢ ↑a + 1 = ↑a + 1nA:ℕnB:ℕi:Fin (nA + 1)j:Fin (nB + 1)a:Fin nAh✝³:¬(↑a < ↑i ∧ ↑a < nA + 1 + ↑j)h✝²:¬(↑a + 1 < ↑i ∧ nA + 1 + ↑j ≤ ↑a)h✝¹:¬(↑i ≤ ↑a ∧ ↑a + 1 < nA + 1 + ↑j)h✝:↑a < ↑i⊢ ↑a + 2 = ↑anA:ℕnB:ℕi:Fin (nA + 1)j:Fin (nB + 1)a:Fin nAh✝³:¬(↑a < ↑i ∧ ↑a < nA + 1 + ↑j)h✝²:¬(↑a + 1 < ↑i ∧ nA + 1 + ↑j ≤ ↑a)h✝¹:¬(↑i ≤ ↑a ∧ ↑a + 1 < nA + 1 + ↑j)h✝:¬↑a < ↑i⊢ ↑a + 2 = ↑a + 1 nA:ℕnB:ℕi:Fin (nA + 1)j:Fin (nB + 1)a:Fin nAh✝¹:↑a < ↑i ∧ ↑a < nA + 1 + ↑jh✝:↑a < ↑i⊢ ↑a = ↑anA:ℕnB:ℕi:Fin (nA + 1)j:Fin (nB + 1)a:Fin nAh✝¹:↑a < ↑i ∧ ↑a < nA + 1 + ↑jh✝:¬↑a < ↑i⊢ ↑a = ↑a + 1nA:ℕnB:ℕi:Fin (nA + 1)j:Fin (nB + 1)a:Fin nAh✝²:¬(↑a < ↑i ∧ ↑a < nA + 1 + ↑j)h✝¹:↑a + 1 < ↑i ∧ nA + 1 + ↑j ≤ ↑ah✝:↑a < ↑i⊢ ↑a + 1 = ↑anA:ℕnB:ℕi:Fin (nA + 1)j:Fin (nB + 1)a:Fin nAh✝²:¬(↑a < ↑i ∧ ↑a < nA + 1 + ↑j)h✝¹:↑a + 1 < ↑i ∧ nA + 1 + ↑j ≤ ↑ah✝:¬↑a < ↑i⊢ ↑a + 1 = ↑a + 1nA:ℕnB:ℕi:Fin (nA + 1)j:Fin (nB + 1)a:Fin nAh✝³:¬(↑a < ↑i ∧ ↑a < nA + 1 + ↑j)h✝²:¬(↑a + 1 < ↑i ∧ nA + 1 + ↑j ≤ ↑a)h✝¹:↑i ≤ ↑a ∧ ↑a + 1 < nA + 1 + ↑jh✝:↑a < ↑i⊢ ↑a + 1 = ↑anA:ℕnB:ℕi:Fin (nA + 1)j:Fin (nB + 1)a:Fin nAh✝³:¬(↑a < ↑i ∧ ↑a < nA + 1 + ↑j)h✝²:¬(↑a + 1 < ↑i ∧ nA + 1 + ↑j ≤ ↑a)h✝¹:↑i ≤ ↑a ∧ ↑a + 1 < nA + 1 + ↑jh✝:¬↑a < ↑i⊢ ↑a + 1 = ↑a + 1nA:ℕnB:ℕi:Fin (nA + 1)j:Fin (nB + 1)a:Fin nAh✝³:¬(↑a < ↑i ∧ ↑a < nA + 1 + ↑j)h✝²:¬(↑a + 1 < ↑i ∧ nA + 1 + ↑j ≤ ↑a)h✝¹:¬(↑i ≤ ↑a ∧ ↑a + 1 < nA + 1 + ↑j)h✝:↑a < ↑i⊢ ↑a + 2 = ↑anA:ℕnB:ℕi:Fin (nA + 1)j:Fin (nB + 1)a:Fin nAh✝³:¬(↑a < ↑i ∧ ↑a < nA + 1 + ↑j)h✝²:¬(↑a + 1 < ↑i ∧ nA + 1 + ↑j ≤ ↑a)h✝¹:¬(↑i ≤ ↑a ∧ ↑a + 1 < nA + 1 + ↑j)h✝:¬↑a < ↑i⊢ ↑a + 2 = ↑a + 1 All goals completed! 🐙

Reinserting a right-block survivor, the mirror of Fin.succSuccAbove_castAdd_natAdd_apply_castAdd.

lemma succSuccAbove_castAdd_natAdd_apply_natAdd {nA nB : ℕ} (i : Fin (nA + 1)) (j : Fin (nB + 1)) (a : Fin nB) : Fin.cast (show (nA + nB) + 1 + 1 = (nA + 1) + (nB + 1) All goals completed! 🐙 All goals completed! 🐙) ((Fin.cast (show (nA + 1) + (nB + 1) = (nA + nB) + 1 + 1 All goals completed! 🐙 All goals completed! 🐙) (Fin.castAdd (nB + 1) i)).succSuccAbove (Fin.cast (show (nA + 1) + (nB + 1) = (nA + nB) + 1 + 1 All goals completed! 🐙 All goals completed! 🐙) (Fin.natAdd (nA + 1) j)) (Fin.natAdd nA a)) = Fin.natAdd (nA + 1) (j.succAbove a) := nA:ℕnB:ℕi:Fin (nA + 1)j:Fin (nB + 1)a:Fin nB⊢ Fin.cast ⋯ ((Fin.cast ⋯ (castAdd (nB + 1) i)).succSuccAbove (Fin.cast ⋯ (natAdd (nA + 1) j)) (natAdd nA a)) = natAdd (nA + 1) (j.succAbove a) nA:ℕnB:ℕi:Fin (nA + 1)j:Fin (nB + 1)a:Fin nB⊢ ↑(Fin.cast ⋯ ((Fin.cast ⋯ (castAdd (nB + 1) i)).succSuccAbove (Fin.cast ⋯ (natAdd (nA + 1) j)) (natAdd nA a))) = ↑(natAdd (nA + 1) (j.succAbove a)) nA:ℕnB:ℕi:Fin (nA + 1)j:Fin (nB + 1)a:Fin nB⊢ (if nA + ↑a < ↑i ∧ nA + ↑a < nA + 1 + ↑j then nA + ↑a else if nA + ↑a + 1 < ↑i ∧ nA + 1 + ↑j ≤ nA + ↑a then nA + ↑a + 1 else if ↑i ≤ nA + ↑a ∧ nA + ↑a + 1 < nA + 1 + ↑j then nA + ↑a + 1 else nA + ↑a + 2) = nA + 1 + if ↑a < ↑j then ↑a else ↑a + 1 nA:ℕnB:ℕi:Fin (nA + 1)j:Fin (nB + 1)a:Fin nBh✝¹:nA + ↑a < ↑i ∧ nA + ↑a < nA + 1 + ↑jh✝:↑a < ↑j⊢ nA + ↑a = nA + 1 + ↑anA:ℕnB:ℕi:Fin (nA + 1)j:Fin (nB + 1)a:Fin nBh✝¹:nA + ↑a < ↑i ∧ nA + ↑a < nA + 1 + ↑jh✝:¬↑a < ↑j⊢ nA + ↑a = nA + 1 + (↑a + 1)nA:ℕnB:ℕi:Fin (nA + 1)j:Fin (nB + 1)a:Fin nBh✝²:¬(nA + ↑a < ↑i ∧ nA + ↑a < nA + 1 + ↑j)h✝¹:nA + ↑a + 1 < ↑i ∧ nA + 1 + ↑j ≤ nA + ↑ah✝:↑a < ↑j⊢ nA + ↑a + 1 = nA + 1 + ↑anA:ℕnB:ℕi:Fin (nA + 1)j:Fin (nB + 1)a:Fin nBh✝²:¬(nA + ↑a < ↑i ∧ nA + ↑a < nA + 1 + ↑j)h✝¹:nA + ↑a + 1 < ↑i ∧ nA + 1 + ↑j ≤ nA + ↑ah✝:¬↑a < ↑j⊢ nA + ↑a + 1 = nA + 1 + (↑a + 1)nA:ℕnB:ℕi:Fin (nA + 1)j:Fin (nB + 1)a:Fin nBh✝³:¬(nA + ↑a < ↑i ∧ nA + ↑a < nA + 1 + ↑j)h✝²:¬(nA + ↑a + 1 < ↑i ∧ nA + 1 + ↑j ≤ nA + ↑a)h✝¹:↑i ≤ nA + ↑a ∧ nA + ↑a + 1 < nA + 1 + ↑jh✝:↑a < ↑j⊢ nA + ↑a + 1 = nA + 1 + ↑anA:ℕnB:ℕi:Fin (nA + 1)j:Fin (nB + 1)a:Fin nBh✝³:¬(nA + ↑a < ↑i ∧ nA + ↑a < nA + 1 + ↑j)h✝²:¬(nA + ↑a + 1 < ↑i ∧ nA + 1 + ↑j ≤ nA + ↑a)h✝¹:↑i ≤ nA + ↑a ∧ nA + ↑a + 1 < nA + 1 + ↑jh✝:¬↑a < ↑j⊢ nA + ↑a + 1 = nA + 1 + (↑a + 1)nA:ℕnB:ℕi:Fin (nA + 1)j:Fin (nB + 1)a:Fin nBh✝³:¬(nA + ↑a < ↑i ∧ nA + ↑a < nA + 1 + ↑j)h✝²:¬(nA + ↑a + 1 < ↑i ∧ nA + 1 + ↑j ≤ nA + ↑a)h✝¹:¬(↑i ≤ nA + ↑a ∧ nA + ↑a + 1 < nA + 1 + ↑j)h✝:↑a < ↑j⊢ nA + ↑a + 2 = nA + 1 + ↑anA:ℕnB:ℕi:Fin (nA + 1)j:Fin (nB + 1)a:Fin nBh✝³:¬(nA + ↑a < ↑i ∧ nA + ↑a < nA + 1 + ↑j)h✝²:¬(nA + ↑a + 1 < ↑i ∧ nA + 1 + ↑j ≤ nA + ↑a)h✝¹:¬(↑i ≤ nA + ↑a ∧ nA + ↑a + 1 < nA + 1 + ↑j)h✝:¬↑a < ↑j⊢ nA + ↑a + 2 = nA + 1 + (↑a + 1) nA:ℕnB:ℕi:Fin (nA + 1)j:Fin (nB + 1)a:Fin nBh✝¹:nA + ↑a < ↑i ∧ nA + ↑a < nA + 1 + ↑jh✝:↑a < ↑j⊢ nA + ↑a = nA + 1 + ↑anA:ℕnB:ℕi:Fin (nA + 1)j:Fin (nB + 1)a:Fin nBh✝¹:nA + ↑a < ↑i ∧ nA + ↑a < nA + 1 + ↑jh✝:¬↑a < ↑j⊢ nA + ↑a = nA + 1 + (↑a + 1)nA:ℕnB:ℕi:Fin (nA + 1)j:Fin (nB + 1)a:Fin nBh✝²:¬(nA + ↑a < ↑i ∧ nA + ↑a < nA + 1 + ↑j)h✝¹:nA + ↑a + 1 < ↑i ∧ nA + 1 + ↑j ≤ nA + ↑ah✝:↑a < ↑j⊢ nA + ↑a + 1 = nA + 1 + ↑anA:ℕnB:ℕi:Fin (nA + 1)j:Fin (nB + 1)a:Fin nBh✝²:¬(nA + ↑a < ↑i ∧ nA + ↑a < nA + 1 + ↑j)h✝¹:nA + ↑a + 1 < ↑i ∧ nA + 1 + ↑j ≤ nA + ↑ah✝:¬↑a < ↑j⊢ nA + ↑a + 1 = nA + 1 + (↑a + 1)nA:ℕnB:ℕi:Fin (nA + 1)j:Fin (nB + 1)a:Fin nBh✝³:¬(nA + ↑a < ↑i ∧ nA + ↑a < nA + 1 + ↑j)h✝²:¬(nA + ↑a + 1 < ↑i ∧ nA + 1 + ↑j ≤ nA + ↑a)h✝¹:↑i ≤ nA + ↑a ∧ nA + ↑a + 1 < nA + 1 + ↑jh✝:↑a < ↑j⊢ nA + ↑a + 1 = nA + 1 + ↑anA:ℕnB:ℕi:Fin (nA + 1)j:Fin (nB + 1)a:Fin nBh✝³:¬(nA + ↑a < ↑i ∧ nA + ↑a < nA + 1 + ↑j)h✝²:¬(nA + ↑a + 1 < ↑i ∧ nA + 1 + ↑j ≤ nA + ↑a)h✝¹:↑i ≤ nA + ↑a ∧ nA + ↑a + 1 < nA + 1 + ↑jh✝:¬↑a < ↑j⊢ nA + ↑a + 1 = nA + 1 + (↑a + 1)nA:ℕnB:ℕi:Fin (nA + 1)j:Fin (nB + 1)a:Fin nBh✝³:¬(nA + ↑a < ↑i ∧ nA + ↑a < nA + 1 + ↑j)h✝²:¬(nA + ↑a + 1 < ↑i ∧ nA + 1 + ↑j ≤ nA + ↑a)h✝¹:¬(↑i ≤ nA + ↑a ∧ nA + ↑a + 1 < nA + 1 + ↑j)h✝:↑a < ↑j⊢ nA + ↑a + 2 = nA + 1 + ↑anA:ℕnB:ℕi:Fin (nA + 1)j:Fin (nB + 1)a:Fin nBh✝³:¬(nA + ↑a < ↑i ∧ nA + ↑a < nA + 1 + ↑j)h✝²:¬(nA + ↑a + 1 < ↑i ∧ nA + 1 + ↑j ≤ nA + ↑a)h✝¹:¬(↑i ≤ nA + ↑a ∧ nA + ↑a + 1 < nA + 1 + ↑j)h✝:¬↑a < ↑j⊢ nA + ↑a + 2 = nA + 1 + (↑a + 1) All goals completed! 🐙
lemma succSuccAbove_natAdd_image_range_castAdd {n n1 : ℕ} (i j : Fin (n + 1 + 1)) : (succSuccAbove (n := n1 + n) (Fin.natAdd n1 i) (Fin.natAdd n1 j)) '' (Set.range (Fin.castAdd (m := n) (n := n1))) = {i | i.1 < n1} := n:ℕn1:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)⊢ (natAdd n1 i).succSuccAbove (natAdd n1 j) '' Set.range (castAdd n) = {i | ↑i < n1} n:ℕn1:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)a:Fin (n1 + n + 1 + 1)⊢ a ∈ (natAdd n1 i).succSuccAbove (natAdd n1 j) '' Set.range (castAdd n) ↔ a ∈ {i | ↑i < n1} n:ℕn1:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)a:Fin (n1 + n + 1 + 1)⊢ (∃ a_1, (natAdd n1 i).succSuccAbove (natAdd n1 j) (castAdd n a_1) = a) ↔ ↑a < n1 conv_lhs => n:ℕn1:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)a:Fin (n1 + n + 1 + 1)b:Fin n1| (natAdd n1 i).succSuccAbove (natAdd n1 j) (castAdd n b) = a n:ℕn1:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)a:Fin (n1 + n + 1 + 1)b:Fin n1| castAdd (n + 1 + 1) b = a n:ℕn1:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)a:Fin (n1 + n + 1 + 1)⊢ (∃ b, castAdd (n + 1 + 1) b = a) → ↑a < n1n:ℕn1:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)a:Fin (n1 + n + 1 + 1)⊢ ↑a < n1 → ∃ b, castAdd (n + 1 + 1) b = a n:ℕn1:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)a:Fin (n1 + n + 1 + 1)⊢ (∃ b, castAdd (n + 1 + 1) b = a) → ↑a < n1 n:ℕn1:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)b:Fin n1⊢ ↑(castAdd (n + 1 + 1) b) < n1 All goals completed! 🐙 n:ℕn1:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)a:Fin (n1 + n + 1 + 1)⊢ ↑a < n1 → ∃ b, castAdd (n + 1 + 1) b = a exact fun h ↦ ⟨⟨a, n:ℕn1:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)a:Fin (n1 + n + 1 + 1)h:↑a < n1⊢ ↑a < n1 All goals completed! 🐙⟩, n:ℕn1:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)a:Fin (n1 + n + 1 + 1)h:↑a < n1⊢ castAdd (n + 1 + 1) ⟨↑a, h⟩ = a All goals completed! 🐙⟩lemma succSuccAbove_comm_natAdd {n n1 : ℕ} (i j : Fin (n + 1 + 1)) (m : Fin n) : succSuccAbove (n := n1 + n) (Fin.natAdd n1 i) (Fin.natAdd n1 j) (Fin.natAdd n1 m) = Fin.natAdd (n1) (succSuccAbove i j m) := n:ℕn1:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)m:Fin n⊢ (natAdd n1 i).succSuccAbove (natAdd n1 j) (natAdd n1 m) = natAdd n1 (i.succSuccAbove j m) n:ℕn1:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)m:Fin n⊢ ↑(if ↑m < ↑i ∧ ↑m < ↑j then ⟨n1 + ↑m, ⋯⟩ else if n1 + ↑m + 1 < n1 + ↑i ∧ ↑j ≤ ↑m then ⟨n1 + ↑m + 1, ⋯⟩ else if ↑i ≤ ↑m ∧ n1 + ↑m + 1 < n1 + ↑j then ⟨n1 + ↑m + 1, ⋯⟩ else ⟨n1 + ↑m + 2, ⋯⟩) = n1 + ↑(if ↑m < ↑i ∧ ↑m < ↑j then ⟨↑m, ⋯⟩ else if ↑m + 1 < ↑i ∧ ↑j ≤ ↑m then ⟨↑m + 1, ⋯⟩ else if ↑i ≤ ↑m ∧ ↑m + 1 < ↑j then ⟨↑m + 1, ⋯⟩ else ⟨↑m + 2, ⋯⟩) All goals completed! 🐙

predPredAbove

The preimage of m under succSuccAbove i j hij given that m is not equal to i or j.

def predPredAbove (i j : Fin (n + 1 + 1)) (hij : i ≠ j) (m : Fin (n + 1 + 1)) (hm : m ≠ i ∧ m ≠ j) : Fin n := if h1 : m.1 < i.1 ∧ m.1 < j.1 then ⟨m, C:Sort ?u.15n:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jm:Fin (n + 1 + 1)hm:m ≠ i ∧ m ≠ jh1:↑m < ↑i ∧ ↑m < ↑j⊢ ↑m < n All goals completed! 🐙⟩ else if h2 : m.1 - 1 < i.1 ∧ j.1 ≤ m.1 then ⟨m - 1, C:Sort ?u.15n:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jm:Fin (n + 1 + 1)hm:m ≠ i ∧ m ≠ jh1:¬(↑m < ↑i ∧ ↑m < ↑j)h2:↑m - 1 < ↑i ∧ ↑j ≤ ↑m⊢ ↑m - 1 < n All goals completed! 🐙⟩ else if h3 : i.1 - 1 ≤ m.1 ∧ m.1 < j.1 then ⟨m - 1, C:Sort ?u.15n:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jm:Fin (n + 1 + 1)hm:m ≠ i ∧ m ≠ jh1:¬(↑m < ↑i ∧ ↑m < ↑j)h2:¬(↑m - 1 < ↑i ∧ ↑j ≤ ↑m)h3:↑i - 1 ≤ ↑m ∧ ↑m < ↑j⊢ ↑m - 1 < n All goals completed! 🐙⟩ else ⟨m - 2, C:Sort ?u.15n:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jm:Fin (n + 1 + 1)hm:m ≠ i ∧ m ≠ jh1:¬(↑m < ↑i ∧ ↑m < ↑j)h2:¬(↑m - 1 < ↑i ∧ ↑j ≤ ↑m)h3:¬(↑i - 1 ≤ ↑m ∧ ↑m < ↑j)⊢ ↑m - 2 < n All goals completed! 🐙⟩
lemma predPredAbove_val (i j : Fin (n + 1 + 1)) (hij : i ≠ j) (m : Fin (n + 1 + 1)) (hm : m ≠ i ∧ m ≠ j) : (predPredAbove i j hij m hm).val = if m.1 < i.1 ∧ m.1 < j.1 then m.1 else if m.1 - 1 < i.1 ∧ j.1 ≤ m.1 then m.1 - 1 else if i.1 - 1 ≤ m.1 ∧ m.1 < j.1 then m.1 - 1 else m.1 - 2 := n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jm:Fin (n + 1 + 1)hm:m ≠ i ∧ m ≠ j⊢ ↑(i.predPredAbove j hij m hm) = if ↑m < ↑i ∧ ↑m < ↑j then ↑m else if ↑m - 1 < ↑i ∧ ↑j ≤ ↑m then ↑m - 1 else if ↑i - 1 ≤ ↑m ∧ ↑m < ↑j then ↑m - 1 else ↑m - 2 n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jm:Fin (n + 1 + 1)hm:m ≠ i ∧ m ≠ j⊢ ↑(if h1 : ↑m < ↑i ∧ ↑m < ↑j then ⟨↑m, ⋯⟩ else if h2 : ↑m - 1 < ↑i ∧ ↑j ≤ ↑m then ⟨↑m - 1, ⋯⟩ else if h3 : ↑i - 1 ≤ ↑m ∧ ↑m < ↑j then ⟨↑m - 1, ⋯⟩ else ⟨↑m - 2, ⋯⟩) = if ↑m < ↑i ∧ ↑m < ↑j then ↑m else if ↑m - 1 < ↑i ∧ ↑j ≤ ↑m then ↑m - 1 else if ↑i - 1 ≤ ↑m ∧ ↑m < ↑j then ↑m - 1 else ↑m - 2 All goals completed! 🐙@[simp] lemma succSuccAbove_predPredAbove (i j : Fin (n + 1 + 1)) (hij : i ≠ j) (m : Fin (n + 1 + 1)) (hm : m ≠ i ∧ m ≠ j) : succSuccAbove i j (predPredAbove i j hij m hm) = m := n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jm:Fin (n + 1 + 1)hm:m ≠ i ∧ m ≠ j⊢ i.succSuccAbove j (i.predPredAbove j hij m hm) = m n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jm:Fin (n + 1 + 1)hm:m ≠ i ∧ m ≠ j⊢ (if ↑(if h1 : ↑m < ↑i ∧ ↑m < ↑j then ⟨↑m, ⋯⟩ else if h2 : ↑m - 1 < ↑i ∧ ↑j ≤ ↑m then ⟨↑m - 1, ⋯⟩ else if h3 : ↑i - 1 ≤ ↑m ∧ ↑m < ↑j then ⟨↑m - 1, ⋯⟩ else ⟨↑m - 2, ⋯⟩) < ↑i ∧ ↑(if h1 : ↑m < ↑i ∧ ↑m < ↑j then ⟨↑m, ⋯⟩ else if h2 : ↑m - 1 < ↑i ∧ ↑j ≤ ↑m then ⟨↑m - 1, ⋯⟩ else if h3 : ↑i - 1 ≤ ↑m ∧ ↑m < ↑j then ⟨↑m - 1, ⋯⟩ else ⟨↑m - 2, ⋯⟩) < ↑j then ⟨↑(if h1 : ↑m < ↑i ∧ ↑m < ↑j then ⟨↑m, ⋯⟩ else if h2 : ↑m - 1 < ↑i ∧ ↑j ≤ ↑m then ⟨↑m - 1, ⋯⟩ else if h3 : ↑i - 1 ≤ ↑m ∧ ↑m < ↑j then ⟨↑m - 1, ⋯⟩ else ⟨↑m - 2, ⋯⟩), ⋯⟩ else if ↑(if h1 : ↑m < ↑i ∧ ↑m < ↑j then ⟨↑m, ⋯⟩ else if h2 : ↑m - 1 < ↑i ∧ ↑j ≤ ↑m then ⟨↑m - 1, ⋯⟩ else if h3 : ↑i - 1 ≤ ↑m ∧ ↑m < ↑j then ⟨↑m - 1, ⋯⟩ else ⟨↑m - 2, ⋯⟩) + 1 < ↑i ∧ ↑j ≤ ↑(if h1 : ↑m < ↑i ∧ ↑m < ↑j then ⟨↑m, ⋯⟩ else if h2 : ↑m - 1 < ↑i ∧ ↑j ≤ ↑m then ⟨↑m - 1, ⋯⟩ else if h3 : ↑i - 1 ≤ ↑m ∧ ↑m < ↑j then ⟨↑m - 1, ⋯⟩ else ⟨↑m - 2, ⋯⟩) then ⟨↑(if h1 : ↑m < ↑i ∧ ↑m < ↑j then ⟨↑m, ⋯⟩ else if h2 : ↑m - 1 < ↑i ∧ ↑j ≤ ↑m then ⟨↑m - 1, ⋯⟩ else if h3 : ↑i - 1 ≤ ↑m ∧ ↑m < ↑j then ⟨↑m - 1, ⋯⟩ else ⟨↑m - 2, ⋯⟩) + 1, ⋯⟩ else if ↑i ≤ ↑(if h1 : ↑m < ↑i ∧ ↑m < ↑j then ⟨↑m, ⋯⟩ else if h2 : ↑m - 1 < ↑i ∧ ↑j ≤ ↑m then ⟨↑m - 1, ⋯⟩ else if h3 : ↑i - 1 ≤ ↑m ∧ ↑m < ↑j then ⟨↑m - 1, ⋯⟩ else ⟨↑m - 2, ⋯⟩) ∧ ↑(if h1 : ↑m < ↑i ∧ ↑m < ↑j then ⟨↑m, ⋯⟩ else if h2 : ↑m - 1 < ↑i ∧ ↑j ≤ ↑m then ⟨↑m - 1, ⋯⟩ else if h3 : ↑i - 1 ≤ ↑m ∧ ↑m < ↑j then ⟨↑m - 1, ⋯⟩ else ⟨↑m - 2, ⋯⟩) + 1 < ↑j then ⟨↑(if h1 : ↑m < ↑i ∧ ↑m < ↑j then ⟨↑m, ⋯⟩ else if h2 : ↑m - 1 < ↑i ∧ ↑j ≤ ↑m then ⟨↑m - 1, ⋯⟩ else if h3 : ↑i - 1 ≤ ↑m ∧ ↑m < ↑j then ⟨↑m - 1, ⋯⟩ else ⟨↑m - 2, ⋯⟩) + 1, ⋯⟩ else ⟨↑(if h1 : ↑m < ↑i ∧ ↑m < ↑j then ⟨↑m, ⋯⟩ else if h2 : ↑m - 1 < ↑i ∧ ↑j ≤ ↑m then ⟨↑m - 1, ⋯⟩ else if h3 : ↑i - 1 ≤ ↑m ∧ ↑m < ↑j then ⟨↑m - 1, ⋯⟩ else ⟨↑m - 2, ⋯⟩) + 2, ⋯⟩) = m All goals completed! 🐙C:Sort ?u.15n:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jm:Fin (n + 1 + 1)hm:m ≠ i ∧ m ≠ j⊢ Fintype.card (Fin (n + 1 + 1)) - {i, j}.card = n; All goals completed! 🐙)).symm ⟨m, C:Sort ?u.15n:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jm:Fin (n + 1 + 1)hm:m ≠ i ∧ m ≠ j⊢ m ∈ {i, j}ᶜ All goals completed! 🐙⟩ := n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jm:Fin (n + 1 + 1)hm:m ≠ i ∧ m ≠ j⊢ i.predPredAbove j hij m hm = ({i, j}ᶜ.orderIsoOfFin ⋯).symm ⟨m, ⋯⟩ n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jm:Fin (n + 1 + 1)hm:m ≠ i ∧ m ≠ j⊢ i.succSuccAbove j (i.predPredAbove j hij m hm) = i.succSuccAbove j (({i, j}ᶜ.orderIsoOfFin ⋯).symm ⟨m, ⋯⟩) conv_rhs => n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jm:Fin (n + 1 + 1)hm:m ≠ i ∧ m ≠ j| ↑(({i, j}ᶜ.orderIsoOfFin ⋯) (({i, j}ᶜ.orderIsoOfFin ⋯).symm ⟨m, ⋯⟩)) All goals completed! 🐙n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jm1:Fin (n + 1 + 1)m2:Fin (n + 1 + 1)hm1:m1 ≠ i ∧ m1 ≠ jhm2:m2 ≠ i ∧ m2 ≠ j⊢ i.succSuccAbove j (i.predPredAbove j hij m1 hm1) = i.succSuccAbove j (i.predPredAbove j hij m2 hm2) ↔ m1 = m2 All goals completed! 🐙lemma predPredAbove_surjective (i j : Fin (n + 1 + 1)) (hij : i ≠ j) (m : Fin n) : ∃ m' : Fin (n + 1 + 1), ∃ (h : m' ≠ i ∧ m' ≠ j), predPredAbove i j hij m' h = m := n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jm:Fin n⊢ ∃ m', ∃ (h : m' ≠ i ∧ m' ≠ j), i.predPredAbove j hij m' h = m refine ⟨succSuccAbove i j m, n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jm:Fin n⊢ i.succSuccAbove j m ≠ i ∧ i.succSuccAbove j m ≠ j All goals completed! 🐙, succSuccAbove_injective i j ?_⟩ All goals completed! 🐙@[simp] lemma predPredAbove_succSuccAbove (i j : Fin (n + 1 + 1)) (hij : i ≠ j) (m : Fin n) : predPredAbove i j hij (succSuccAbove i j m) (C:Sort ?u.15n:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jm:Fin n⊢ i.succSuccAbove j m ≠ i ∧ i.succSuccAbove j m ≠ j All goals completed! 🐙) = m := n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jm:Fin n⊢ i.predPredAbove j hij (i.succSuccAbove j m) ⋯ = m n:ℕi:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jm:Fin n⊢ i.succSuccAbove j (i.predPredAbove j hij (i.succSuccAbove j m) ⋯) = i.succSuccAbove j m All goals completed! 🐙

Commutativity of succSuccAbove

lemma succSuccAbove_comm (i1 j1 : Fin (n + 1 + 1 + 1 + 1)) (i2 j2 : Fin (n + 1 + 1)) (hij1 : i1 ≠ j1) (hij2 : i2 ≠ j2) : let i2' := (succSuccAbove i1 j1 i2); let j2' := (succSuccAbove i1 j1 j2); have hi2j2' : i2' ≠ j2' := C:Sort ?u.15n:ℕc:Fin (n + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1hij2:i2 ≠ j2i2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2⊢ i2' ≠ j2' All goals completed! 🐙; let i1' := (predPredAbove i2' j2' hi2j2' i1 (C:Sort ?u.15n:ℕc:Fin (n + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1hij2:i2 ≠ j2i2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2hi2j2':i2' ≠ j2'⊢ i1 ≠ i2' ∧ i1 ≠ j2' All goals completed! 🐙)); let j1' := (predPredAbove i2' j2' hi2j2' j1 (C:Sort ?u.15n:ℕc:Fin (n + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1hij2:i2 ≠ j2i2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2hi2j2':i2' ≠ j2'i1':Fin (n + 2) := i2'.predPredAbove j2' hi2j2' i1 ⋯⊢ j1 ≠ i2' ∧ j1 ≠ j2' All goals completed! 🐙)); succSuccAbove i1 j1 ∘ succSuccAbove i2 j2 = succSuccAbove i2' j2' ∘ succSuccAbove i1' j1':= n:ℕi1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1hij2:i2 ≠ j2⊢ let i2' := i1.succSuccAbove j1 i2; let j2' := i1.succSuccAbove j1 j2; have hi2j2' := ⋯; let i1' := i2'.predPredAbove j2' hi2j2' i1 ⋯; let j1' := i2'.predPredAbove j2' hi2j2' j1 ⋯; i1.succSuccAbove j1 ∘ i2.succSuccAbove j2 = i2'.succSuccAbove j2' ∘ i1'.succSuccAbove j1' n:ℕi1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1hij2:i2 ≠ j2m:Fin n⊢ ↑((i1.succSuccAbove j1 ∘ i2.succSuccAbove j2) m) = ↑(((i1.succSuccAbove j1 i2).succSuccAbove (i1.succSuccAbove j1 j2) ∘ ((i1.succSuccAbove j1 i2).predPredAbove (i1.succSuccAbove j1 j2) ⋯ i1 ⋯).succSuccAbove ((i1.succSuccAbove j1 i2).predPredAbove (i1.succSuccAbove j1 j2) ⋯ j1 ⋯)) m) n:ℕi1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1hij2:i2 ≠ j2m:Fin n⊢ (if (if ↑m < ↑i2 ∧ ↑m < ↑j2 then ↑m else if ↑m + 1 < ↑i2 ∧ ↑j2 ≤ ↑m then ↑m + 1 else if ↑i2 ≤ ↑m ∧ ↑m + 1 < ↑j2 then ↑m + 1 else ↑m + 2) < ↑i1 ∧ (if ↑m < ↑i2 ∧ ↑m < ↑j2 then ↑m else if ↑m + 1 < ↑i2 ∧ ↑j2 ≤ ↑m then ↑m + 1 else if ↑i2 ≤ ↑m ∧ ↑m + 1 < ↑j2 then ↑m + 1 else ↑m + 2) < ↑j1 then if ↑m < ↑i2 ∧ ↑m < ↑j2 then ↑m else if ↑m + 1 < ↑i2 ∧ ↑j2 ≤ ↑m then ↑m + 1 else if ↑i2 ≤ ↑m ∧ ↑m + 1 < ↑j2 then ↑m + 1 else ↑m + 2 else if (if ↑m < ↑i2 ∧ ↑m < ↑j2 then ↑m else if ↑m + 1 < ↑i2 ∧ ↑j2 ≤ ↑m then ↑m + 1 else if ↑i2 ≤ ↑m ∧ ↑m + 1 < ↑j2 then ↑m + 1 else ↑m + 2) + 1 < ↑i1 ∧ ↑j1 ≤ if ↑m < ↑i2 ∧ ↑m < ↑j2 then ↑m else if ↑m + 1 < ↑i2 ∧ ↑j2 ≤ ↑m then ↑m + 1 else if ↑i2 ≤ ↑m ∧ ↑m + 1 < ↑j2 then ↑m + 1 else ↑m + 2 then (if ↑m < ↑i2 ∧ ↑m < ↑j2 then ↑m else if ↑m + 1 < ↑i2 ∧ ↑j2 ≤ ↑m then ↑m + 1 else if ↑i2 ≤ ↑m ∧ ↑m + 1 < ↑j2 then ↑m + 1 else ↑m + 2) + 1 else if (↑i1 ≤ if ↑m < ↑i2 ∧ ↑m < ↑j2 then ↑m else if ↑m + 1 < ↑i2 ∧ ↑j2 ≤ ↑m then ↑m + 1 else if ↑i2 ≤ ↑m ∧ ↑m + 1 < ↑j2 then ↑m + 1 else ↑m + 2) ∧ (if ↑m < ↑i2 ∧ ↑m < ↑j2 then ↑m else if ↑m + 1 < ↑i2 ∧ ↑j2 ≤ ↑m then ↑m + 1 else if ↑i2 ≤ ↑m ∧ ↑m + 1 < ↑j2 then ↑m + 1 else ↑m + 2) + 1 < ↑j1 then (if ↑m < ↑i2 ∧ ↑m < ↑j2 then ↑m else if ↑m + 1 < ↑i2 ∧ ↑j2 ≤ ↑m then ↑m + 1 else if ↑i2 ≤ ↑m ∧ ↑m + 1 < ↑j2 then ↑m + 1 else ↑m + 2) + 1 else (if ↑m < ↑i2 ∧ ↑m < ↑j2 then ↑m else if ↑m + 1 < ↑i2 ∧ ↑j2 ≤ ↑m then ↑m + 1 else if ↑i2 ≤ ↑m ∧ ↑m + 1 < ↑j2 then ↑m + 1 else ↑m + 2) + 2) = if ((if (↑m < if (↑i1 < if ↑i2 < ↑i1 ∧ ↑i2 < ↑j1 then ↑i2 else if ↑i2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑i2 then ↑i2 + 1 else if ↑i1 ≤ ↑i2 ∧ ↑i2 + 1 < ↑j1 then ↑i2 + 1 else ↑i2 + 2) ∧ ↑i1 < if ↑j2 < ↑i1 ∧ ↑j2 < ↑j1 then ↑j2 else if ↑j2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑j2 then ↑j2 + 1 else if ↑i1 ≤ ↑j2 ∧ ↑j2 + 1 < ↑j1 then ↑j2 + 1 else ↑j2 + 2 then ↑i1 else if (↑i1 - 1 < if ↑i2 < ↑i1 ∧ ↑i2 < ↑j1 then ↑i2 else if ↑i2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑i2 then ↑i2 + 1 else if ↑i1 ≤ ↑i2 ∧ ↑i2 + 1 < ↑j1 then ↑i2 + 1 else ↑i2 + 2) ∧ (if ↑j2 < ↑i1 ∧ ↑j2 < ↑j1 then ↑j2 else if ↑j2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑j2 then ↑j2 + 1 else if ↑i1 ≤ ↑j2 ∧ ↑j2 + 1 < ↑j1 then ↑j2 + 1 else ↑j2 + 2) ≤ ↑i1 then ↑i1 - 1 else if (if ↑i2 < ↑i1 ∧ ↑i2 < ↑j1 then ↑i2 else if ↑i2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑i2 then ↑i2 + 1 else if ↑i1 ≤ ↑i2 ∧ ↑i2 + 1 < ↑j1 then ↑i2 + 1 else ↑i2 + 2) - 1 ≤ ↑i1 ∧ ↑i1 < if ↑j2 < ↑i1 ∧ ↑j2 < ↑j1 then ↑j2 else if ↑j2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑j2 then ↑j2 + 1 else if ↑i1 ≤ ↑j2 ∧ ↑j2 + 1 < ↑j1 then ↑j2 + 1 else ↑j2 + 2 then ↑i1 - 1 else ↑i1 - 2) ∧ ↑m < if (↑j1 < if ↑i2 < ↑i1 ∧ ↑i2 < ↑j1 then ↑i2 else if ↑i2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑i2 then ↑i2 + 1 else if ↑i1 ≤ ↑i2 ∧ ↑i2 + 1 < ↑j1 then ↑i2 + 1 else ↑i2 + 2) ∧ ↑j1 < if ↑j2 < ↑i1 ∧ ↑j2 < ↑j1 then ↑j2 else if ↑j2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑j2 then ↑j2 + 1 else if ↑i1 ≤ ↑j2 ∧ ↑j2 + 1 < ↑j1 then ↑j2 + 1 else ↑j2 + 2 then ↑j1 else if (↑j1 - 1 < if ↑i2 < ↑i1 ∧ ↑i2 < ↑j1 then ↑i2 else if ↑i2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑i2 then ↑i2 + 1 else if ↑i1 ≤ ↑i2 ∧ ↑i2 + 1 < ↑j1 then ↑i2 + 1 else ↑i2 + 2) ∧ (if ↑j2 < ↑i1 ∧ ↑j2 < ↑j1 then ↑j2 else if ↑j2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑j2 then ↑j2 + 1 else if ↑i1 ≤ ↑j2 ∧ ↑j2 + 1 < ↑j1 then ↑j2 + 1 else ↑j2 + 2) ≤ ↑j1 then ↑j1 - 1 else if (if ↑i2 < ↑i1 ∧ ↑i2 < ↑j1 then ↑i2 else if ↑i2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑i2 then ↑i2 + 1 else if ↑i1 ≤ ↑i2 ∧ ↑i2 + 1 < ↑j1 then ↑i2 + 1 else ↑i2 + 2) - 1 ≤ ↑j1 ∧ ↑j1 < if ↑j2 < ↑i1 ∧ ↑j2 < ↑j1 then ↑j2 else if ↑j2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑j2 then ↑j2 + 1 else if ↑i1 ≤ ↑j2 ∧ ↑j2 + 1 < ↑j1 then ↑j2 + 1 else ↑j2 + 2 then ↑j1 - 1 else ↑j1 - 2 then ↑m else if (↑m + 1 < if (↑i1 < if ↑i2 < ↑i1 ∧ ↑i2 < ↑j1 then ↑i2 else if ↑i2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑i2 then ↑i2 + 1 else if ↑i1 ≤ ↑i2 ∧ ↑i2 + 1 < ↑j1 then ↑i2 + 1 else ↑i2 + 2) ∧ ↑i1 < if ↑j2 < ↑i1 ∧ ↑j2 < ↑j1 then ↑j2 else if ↑j2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑j2 then ↑j2 + 1 else if ↑i1 ≤ ↑j2 ∧ ↑j2 + 1 < ↑j1 then ↑j2 + 1 else ↑j2 + 2 then ↑i1 else if (↑i1 - 1 < if ↑i2 < ↑i1 ∧ ↑i2 < ↑j1 then ↑i2 else if ↑i2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑i2 then ↑i2 + 1 else if ↑i1 ≤ ↑i2 ∧ ↑i2 + 1 < ↑j1 then ↑i2 + 1 else ↑i2 + 2) ∧ (if ↑j2 < ↑i1 ∧ ↑j2 < ↑j1 then ↑j2 else if ↑j2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑j2 then ↑j2 + 1 else if ↑i1 ≤ ↑j2 ∧ ↑j2 + 1 < ↑j1 then ↑j2 + 1 else ↑j2 + 2) ≤ ↑i1 then ↑i1 - 1 else if (if ↑i2 < ↑i1 ∧ ↑i2 < ↑j1 then ↑i2 else if ↑i2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑i2 then ↑i2 + 1 else if ↑i1 ≤ ↑i2 ∧ ↑i2 + 1 < ↑j1 then ↑i2 + 1 else ↑i2 + 2) - 1 ≤ ↑i1 ∧ ↑i1 < if ↑j2 < ↑i1 ∧ ↑j2 < ↑j1 then ↑j2 else if ↑j2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑j2 then ↑j2 + 1 else if ↑i1 ≤ ↑j2 ∧ ↑j2 + 1 < ↑j1 then ↑j2 + 1 else ↑j2 + 2 then ↑i1 - 1 else ↑i1 - 2) ∧ (if (↑j1 < if ↑i2 < ↑i1 ∧ ↑i2 < ↑j1 then ↑i2 else if ↑i2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑i2 then ↑i2 + 1 else if ↑i1 ≤ ↑i2 ∧ ↑i2 + 1 < ↑j1 then ↑i2 + 1 else ↑i2 + 2) ∧ ↑j1 < if ↑j2 < ↑i1 ∧ ↑j2 < ↑j1 then ↑j2 else if ↑j2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑j2 then ↑j2 + 1 else if ↑i1 ≤ ↑j2 ∧ ↑j2 + 1 < ↑j1 then ↑j2 + 1 else ↑j2 + 2 then ↑j1 else if (↑j1 - 1 < if ↑i2 < ↑i1 ∧ ↑i2 < ↑j1 then ↑i2 else if ↑i2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑i2 then ↑i2 + 1 else if ↑i1 ≤ ↑i2 ∧ ↑i2 + 1 < ↑j1 then ↑i2 + 1 else ↑i2 + 2) ∧ (if ↑j2 < ↑i1 ∧ ↑j2 < ↑j1 then ↑j2 else if ↑j2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑j2 then ↑j2 + 1 else if ↑i1 ≤ ↑j2 ∧ ↑j2 + 1 < ↑j1 then ↑j2 + 1 else ↑j2 + 2) ≤ ↑j1 then ↑j1 - 1 else if (if ↑i2 < ↑i1 ∧ ↑i2 < ↑j1 then ↑i2 else if ↑i2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑i2 then ↑i2 + 1 else if ↑i1 ≤ ↑i2 ∧ ↑i2 + 1 < ↑j1 then ↑i2 + 1 else ↑i2 + 2) - 1 ≤ ↑j1 ∧ ↑j1 < if ↑j2 < ↑i1 ∧ ↑j2 < ↑j1 then ↑j2 else if ↑j2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑j2 then ↑j2 + 1 else if ↑i1 ≤ ↑j2 ∧ ↑j2 + 1 < ↑j1 then ↑j2 + 1 else ↑j2 + 2 then ↑j1 - 1 else ↑j1 - 2) ≤ ↑m then ↑m + 1 else if (if (↑i1 < if ↑i2 < ↑i1 ∧ ↑i2 < ↑j1 then ↑i2 else if ↑i2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑i2 then ↑i2 + 1 else if ↑i1 ≤ ↑i2 ∧ ↑i2 + 1 < ↑j1 then ↑i2 + 1 else ↑i2 + 2) ∧ ↑i1 < if ↑j2 < ↑i1 ∧ ↑j2 < ↑j1 then ↑j2 else if ↑j2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑j2 then ↑j2 + 1 else if ↑i1 ≤ ↑j2 ∧ ↑j2 + 1 < ↑j1 then ↑j2 + 1 else ↑j2 + 2 then ↑i1 else if (↑i1 - 1 < if ↑i2 < ↑i1 ∧ ↑i2 < ↑j1 then ↑i2 else if ↑i2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑i2 then ↑i2 + 1 else if ↑i1 ≤ ↑i2 ∧ ↑i2 + 1 < ↑j1 then ↑i2 + 1 else ↑i2 + 2) ∧ (if ↑j2 < ↑i1 ∧ ↑j2 < ↑j1 then ↑j2 else if ↑j2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑j2 then ↑j2 + 1 else if ↑i1 ≤ ↑j2 ∧ ↑j2 + 1 < ↑j1 then ↑j2 + 1 else ↑j2 + 2) ≤ ↑i1 then ↑i1 - 1 else if (if ↑i2 < ↑i1 ∧ ↑i2 < ↑j1 then ↑i2 else if ↑i2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑i2 then ↑i2 + 1 else if ↑i1 ≤ ↑i2 ∧ ↑i2 + 1 < ↑j1 then ↑i2 + 1 else ↑i2 + 2) - 1 ≤ ↑i1 ∧ ↑i1 < if ↑j2 < ↑i1 ∧ ↑j2 < ↑j1 then ↑j2 else if ↑j2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑j2 then ↑j2 + 1 else if ↑i1 ≤ ↑j2 ∧ ↑j2 + 1 < ↑j1 then ↑j2 + 1 else ↑j2 + 2 then ↑i1 - 1 else ↑i1 - 2) ≤ ↑m ∧ ↑m + 1 < if (↑j1 < if ↑i2 < ↑i1 ∧ ↑i2 < ↑j1 then ↑i2 else if ↑i2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑i2 then ↑i2 + 1 else if ↑i1 ≤ ↑i2 ∧ ↑i2 + 1 < ↑j1 then ↑i2 + 1 else ↑i2 + 2) ∧ ↑j1 < if ↑j2 < ↑i1 ∧ ↑j2 < ↑j1 then ↑j2 else if ↑j2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑j2 then ↑j2 + 1 else if ↑i1 ≤ ↑j2 ∧ ↑j2 + 1 < ↑j1 then ↑j2 + 1 else ↑j2 + 2 then ↑j1 else if (↑j1 - 1 < if ↑i2 < ↑i1 ∧ ↑i2 < ↑j1 then ↑i2 else if ↑i2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑i2 then ↑i2 + 1 else if ↑i1 ≤ ↑i2 ∧ ↑i2 + 1 < ↑j1 then ↑i2 + 1 else ↑i2 + 2) ∧ (if ↑j2 < ↑i1 ∧ ↑j2 < ↑j1 then ↑j2 else if ↑j2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑j2 then ↑j2 + 1 else if ↑i1 ≤ ↑j2 ∧ ↑j2 + 1 < ↑j1 then ↑j2 + 1 else ↑j2 + 2) ≤ ↑j1 then ↑j1 - 1 else if (if ↑i2 < ↑i1 ∧ ↑i2 < ↑j1 then ↑i2 else if ↑i2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑i2 then ↑i2 + 1 else if ↑i1 ≤ ↑i2 ∧ ↑i2 + 1 < ↑j1 then ↑i2 + 1 else ↑i2 + 2) - 1 ≤ ↑j1 ∧ ↑j1 < if ↑j2 < ↑i1 ∧ ↑j2 < ↑j1 then ↑j2 else if ↑j2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑j2 then ↑j2 + 1 else if ↑i1 ≤ ↑j2 ∧ ↑j2 + 1 < ↑j1 then ↑j2 + 1 else ↑j2 + 2 then ↑j1 - 1 else ↑j1 - 2 then ↑m + 1 else ↑m + 2) < if ↑i2 < ↑i1 ∧ ↑i2 < ↑j1 then ↑i2 else if ↑i2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑i2 then ↑i2 + 1 else if ↑i1 ≤ ↑i2 ∧ ↑i2 + 1 < ↑j1 then ↑i2 + 1 else ↑i2 + 2) ∧ (if (↑m < if (↑i1 < if ↑i2 < ↑i1 ∧ ↑i2 < ↑j1 then ↑i2 else if ↑i2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑i2 then ↑i2 + 1 else if ↑i1 ≤ ↑i2 ∧ ↑i2 + 1 < ↑j1 then ↑i2 + 1 else ↑i2 + 2) ∧ ↑i1 < if ↑j2 < ↑i1 ∧ ↑j2 < ↑j1 then ↑j2 else if ↑j2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑j2 then ↑j2 + 1 else if ↑i1 ≤ ↑j2 ∧ ↑j2 + 1 < ↑j1 then ↑j2 + 1 else ↑j2 + 2 then ↑i1 else if (↑i1 - 1 < if ↑i2 < ↑i1 ∧ ↑i2 < ↑j1 then ↑i2 else if ↑i2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑i2 then ↑i2 + 1 else if ↑i1 ≤ ↑i2 ∧ ↑i2 + 1 < ↑j1 then ↑i2 + 1 else ↑i2 + 2) ∧ (if ↑j2 < ↑i1 ∧ ↑j2 < ↑j1 then ↑j2 else if ↑j2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑j2 then ↑j2 + 1 else if ↑i1 ≤ ↑j2 ∧ ↑j2 + 1 < ↑j1 then ↑j2 + 1 else ↑j2 + 2) ≤ ↑i1 then ↑i1 - 1 else if (if ↑i2 < ↑i1 ∧ ↑i2 < ↑j1 then ↑i2 else if ↑i2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑i2 then ↑i2 + 1 else if ↑i1 ≤ ↑i2 ∧ ↑i2 + 1 < ↑j1 then ↑i2 + 1 else ↑i2 + 2) - 1 ≤ ↑i1 ∧ ↑i1 < if ↑j2 < ↑i1 ∧ ↑j2 < ↑j1 then ↑j2 else if ↑j2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑j2 then ↑j2 + 1 else if ↑i1 ≤ ↑j2 ∧ ↑j2 + 1 < ↑j1 then ↑j2 + 1 else ↑j2 + 2 then ↑i1 - 1 else ↑i1 - 2) ∧ ↑m < if (↑j1 < if ↑i2 < ↑i1 ∧ ↑i2 < ↑j1 then ↑i2 else if ↑i2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑i2 then ↑i2 + 1 else if ↑i1 ≤ ↑i2 ∧ ↑i2 + 1 < ↑j1 then ↑i2 + 1 else ↑i2 + 2) ∧ ↑j1 < if ↑j2 < ↑i1 ∧ ↑j2 < ↑j1 then ↑j2 else if ↑j2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑j2 then ↑j2 + 1 else if ↑i1 ≤ ↑j2 ∧ ↑j2 + 1 < ↑j1 then ↑j2 + 1 else ↑j2 + 2 then ↑j1 else if (↑j1 - 1 < if ↑i2 < ↑i1 ∧ ↑i2 < ↑j1 then ↑i2 else if ↑i2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑i2 then ↑i2 + 1 else if ↑i1 ≤ ↑i2 ∧ ↑i2 + 1 < ↑j1 then ↑i2 + 1 else ↑i2 + 2) ∧ (if ↑j2 < ↑i1 ∧ ↑j2 < ↑j1 then ↑j2 else if ↑j2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑j2 then ↑j2 + 1 else if ↑i1 ≤ ↑j2 ∧ ↑j2 + 1 < ↑j1 then ↑j2 + 1 else ↑j2 + 2) ≤ ↑j1 then ↑j1 - 1 else if (if ↑i2 < ↑i1 ∧ ↑i2 < ↑j1 then ↑i2 else if ↑i2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑i2 then ↑i2 + 1 else if ↑i1 ≤ ↑i2 ∧ ↑i2 + 1 < ↑j1 then ↑i2 + 1 else ↑i2 + 2) - 1 ≤ ↑j1 ∧ ↑j1 < if ↑j2 < ↑i1 ∧ ↑j2 < ↑j1 then ↑j2 else if ↑j2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑j2 then ↑j2 + 1 else if ↑i1 ≤ ↑j2 ∧ ↑j2 + 1 < ↑j1 then ↑j2 + 1 else ↑j2 + 2 then ↑j1 - 1 else ↑j1 - 2 then ↑m else if (↑m + 1 < if (↑i1 < if ↑i2 < ↑i1 ∧ ↑i2 < ↑j1 then ↑i2 else if ↑i2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑i2 then ↑i2 + 1 else if ↑i1 ≤ ↑i2 ∧ ↑i2 + 1 < ↑j1 then ↑i2 + 1 else ↑i2 + 2) ∧ ↑i1 < if ↑j2 < ↑i1 ∧ ↑j2 < ↑j1 then ↑j2 else if ↑j2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑j2 then ↑j2 + 1 else if ↑i1 ≤ ↑j2 ∧ ↑j2 + 1 < ↑j1 then ↑j2 + 1 else ↑j2 + 2 then ↑i1 else if (↑i1 - 1 < if ↑i2 < ↑i1 ∧ ↑i2 < ↑j1 then ↑i2 else if ↑i2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑i2 then ↑i2 + 1 else if ↑i1 ≤ ↑i2 ∧ ↑i2 + 1 < ↑j1 then ↑i2 + 1 else ↑i2 + 2) ∧ (if ↑j2 < ↑i1 ∧ ↑j2 < ↑j1 then ↑j2 else if ↑j2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑j2 then ↑j2 + 1 else if ↑i1 ≤ ↑j2 ∧ ↑j2 + 1 < ↑j1 then ↑j2 + 1 else ↑j2 + 2) ≤ ↑i1 then ↑i1 - 1 else if (if ↑i2 < ↑i1 ∧ ↑i2 < ↑j1 then ↑i2 else if ↑i2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑i2 then ↑i2 + 1 else if ↑i1 ≤ ↑i2 ∧ ↑i2 + 1 < ↑j1 then ↑i2 + 1 else ↑i2 + 2) - 1 ≤ ↑i1 ∧ ↑i1 < if ↑j2 < ↑i1 ∧ ↑j2 < ↑j1 then ↑j2 else if ↑j2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑j2 then ↑j2 + 1 else if ↑i1 ≤ ↑j2 ∧ ↑j2 + 1 < ↑j1 then ↑j2 + 1 else ↑j2 + 2 then ↑i1 - 1 else ↑i1 - 2) ∧ (if (↑j1 < if ↑i2 < ↑i1 ∧ ↑i2 < ↑j1 then ↑i2 else if ↑i2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑i2 then ↑i2 + 1 else if ↑i1 ≤ ↑i2 ∧ ↑i2 + 1 < ↑j1 then ↑i2 + 1 else ↑i2 + 2) ∧ ↑j1 < if ↑j2 < ↑i1 ∧ ↑j2 < ↑j1 then ↑j2 else if ↑j2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑j2 then ↑j2 + 1 else if ↑i1 ≤ ↑j2 ∧ ↑j2 + 1 < ↑j1 then ↑j2 + 1 else ↑j2 + 2 then ↑j1 else if (↑j1 - 1 < if ↑i2 < ↑i1 ∧ ↑i2 < ↑j1 then ↑i2 else if ↑i2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑i2 then ↑i2 + 1 else if ↑i1 ≤ ↑i2 ∧ ↑i2 + 1 < ↑j1 then ↑i2 + 1 else ↑i2 + 2) ∧ (if ↑j2 < ↑i1 ∧ ↑j2 < ↑j1 then ↑j2 else if ↑j2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑j2 then ↑j2 + 1 else if ↑i1 ≤ ↑j2 ∧ ↑j2 + 1 < ↑j1 then ↑j2 + 1 else ↑j2 + 2) ≤ ↑j1 then ↑j1 - 1 else if (if ↑i2 < ↑i1 ∧ ↑i2 < ↑j1 then ↑i2 else if ↑i2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑i2 then ↑i2 + 1 else if ↑i1 ≤ ↑i2 ∧ ↑i2 + 1 < ↑j1 then ↑i2 + 1 else ↑i2 + 2) - 1 ≤ ↑j1 ∧ ↑j1 < if ↑j2 < ↑i1 ∧ ↑j2 < ↑j1 then ↑j2 else if ↑j2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑j2 then ↑j2 + 1 else if ↑i1 ≤ ↑j2 ∧ ↑j2 + 1 < ↑j1 then ↑j2 + 1 else ↑j2 + 2 then ↑j1 - 1 else ↑j1 - 2) ≤ ↑m then ↑m + 1 else if (if (↑i1 < if ↑i2 < ↑i1 ∧ ↑i2 < ↑j1 then ↑i2 else if ↑i2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑i2 then ↑i2 + 1 else if ↑i1 ≤ ↑i2 ∧ ↑i2 + 1 < ↑j1 then ↑i2 + 1 else ↑i2 + 2) ∧ ↑i1 < if ↑j2 < ↑i1 ∧ ↑j2 < ↑j1 then ↑j2 else if ↑j2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑j2 then ↑j2 + 1 else if ↑i1 ≤ ↑j2 ∧ ↑j2 + 1 < ↑j1 then ↑j2 + 1 else ↑j2 + 2 then ↑i1 else if (↑i1 - 1 < if ↑i2 < ↑i1 ∧ ↑i2 < ↑j1 then ↑i2 else if ↑i2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑i2 then ↑i2 + 1 else if ↑i1 ≤ ↑i2 ∧ ↑i2 + 1 < ↑j1 then ↑i2 + 1 else ↑i2 + 2) ∧ (if ↑j2 < ↑i1 ∧ ↑j2 < ↑j1 then ↑j2 else if ↑j2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑j2 then ↑j2 + 1 else if ↑i1 ≤ ↑j2 ∧ ↑j2 + 1 < ↑j1 then ↑j2 + 1 else ↑j2 + 2) ≤ ↑i1 then ↑i1 - 1 else if (if ↑i2 < ↑i1 ∧ ↑i2 < ↑j1 then ↑i2 else if ↑i2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑i2 then ↑i2 + 1 else if ↑i1 ≤ ↑i2 ∧ ↑i2 + 1 < ↑j1 then ↑i2 + 1 else ↑i2 + 2) - 1 ≤ ↑i1 ∧ ↑i1 < if ↑j2 < ↑i1 ∧ ↑j2 < ↑j1 then ↑j2 else if ↑j2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑j2 then ↑j2 + 1 else if ↑i1 ≤ ↑j2 ∧ ↑j2 + 1 < ↑j1 then ↑j2 + 1 else ↑j2 + 2 then ↑i1 - 1 else ↑i1 - 2) ≤ ↑m ∧ ↑m + 1 < if (↑j1 < if ↑i2 < ↑i1 ∧ ↑i2 < ↑j1 then ↑i2 else if ↑i2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑i2 then ↑i2 + 1 else if ↑i1 ≤ ↑i2 ∧ ↑i2 + 1 < ↑j1 then ↑i2 + 1 else ↑i2 + 2) ∧ ↑j1 < if ↑j2 < ↑i1 ∧ ↑j2 < ↑j1 then ↑j2 else if ↑j2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑j2 then ↑j2 + 1 else if ↑i1 ≤ ↑j2 ∧ ↑j2 + 1 < ↑j1 then ↑j2 + 1 else ↑j2 + 2 then ↑j1 else if (↑j1 - 1 < if ↑i2 < ↑i1 ∧ ↑i2 < ↑j1 then ↑i2 else if ↑i2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑i2 then ↑i2 + 1 else if ↑i1 ≤ ↑i2 ∧ ↑i2 + 1 < ↑j1 then ↑i2 + 1 else ↑i2 + 2) ∧ (if ↑j2 < ↑i1 ∧ ↑j2 < ↑j1 then ↑j2 else if ↑j2 + 1 < ↑i1 ∧ ↑j1 ≤ ↑j2 then ↑j2 + 1 else if ↑i1 ≤ ↑j2 ∧ ↑j2 + 1 < ↑j1 then ↑j2 + 1 else ↑j2 + 2) ≤ ↑j1 then ↑j1 - 1 else if (if ↑i2 < ↑i1 ∧ ↑i2 < ↑j1 then ↑i2 else if ↑i2 + 1 < ⋯ ∧ ⋯ then ⋯ else ⋯) - ⋯ ≤ ⋯ ∧ ⋯ then ⋯ else ⋯ then ⋯ else ⋯) < ⋯ then ⋯ else ⋯ All goals completed! 🐙n:ℕi1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1hij2:i2 ≠ j2m:Fin ni2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2hi2j2':i2' ≠ j2' := ···i1':Fin (n + 2) := i2'.predPredAbove j2' hi2j2' i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' hi2j2' j1 ⋯⊢ i2'.succSuccAbove j2' (i1'.succSuccAbove j1' m) = ((i1.succSuccAbove j1 i2).succSuccAbove (i1.succSuccAbove j1 j2) ∘ ((i1.succSuccAbove j1 i2).predPredAbove (i1.succSuccAbove j1 j2) ⋯ i1 ⋯).succSuccAbove ((i1.succSuccAbove j1 i2).predPredAbove (i1.succSuccAbove j1 j2) ⋯ j1 ⋯)) m All goals completed! 🐙

funPredPredAbove

Given a bijection Fin (n1 + 1 + 1) → Fin (n + 1 + 1)) and a pair i j : Fin (n1 + 1 + 1), then funPredPredAbove i j _ σ _ : Fin n1 → Fin n corresponds to the induced bijection formed by dropping i and j in the source and their image in the target.

def funPredPredAbove {n n1 : ℕ} (i j : Fin (n1 + 1 + 1)) (hij : i ≠ j) (σ : Fin (n1 + 1 + 1) → Fin (n + 1 + 1)) (hσ : Function.Bijective σ) (m : Fin n1) : Fin n := predPredAbove (σ i) (σ j) (C:Sort ?u.15n✝:ℕc:Fin (n✝ + 1 + 1) → Cn:ℕn1:ℕi:Fin (n1 + 1 + 1)j:Fin (n1 + 1 + 1)hij:i ≠ jσ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:Function.Bijective σm:Fin n1⊢ σ i ≠ σ j All goals completed! 🐙) (σ (succSuccAbove i j m)) (C:Sort ?u.15n✝:ℕc:Fin (n✝ + 1 + 1) → Cn:ℕn1:ℕi:Fin (n1 + 1 + 1)j:Fin (n1 + 1 + 1)hij:i ≠ jσ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:Function.Bijective σm:Fin n1⊢ σ (i.succSuccAbove j m) ≠ σ i ∧ σ (i.succSuccAbove j m) ≠ σ j All goals completed! 🐙)
lemma funPredPredAbove_injective {n n1 : ℕ} (i j : Fin (n1 + 1 + 1)) (hij : i ≠ j) (σ : Fin (n1 + 1 + 1) → Fin (n + 1 + 1)) (hσ : Function.Bijective σ) : Function.Injective (funPredPredAbove i j hij σ hσ) := n:ℕn1:ℕi:Fin (n1 + 1 + 1)j:Fin (n1 + 1 + 1)hij:i ≠ jσ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:Function.Bijective σ⊢ Function.Injective (i.funPredPredAbove j hij σ hσ) n:ℕn1:ℕi:Fin (n1 + 1 + 1)j:Fin (n1 + 1 + 1)hij:i ≠ jσ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:Function.Bijective σm1:Fin n1m2:Fin n1h:i.funPredPredAbove j hij σ hσ m1 = i.funPredPredAbove j hij σ hσ m2⊢ m1 = m2 All goals completed! 🐙n:ℕn1:ℕi:Fin (n1 + 1 + 1)j:Fin (n1 + 1 + 1)hij:i ≠ jσ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:Function.Bijective σm:Fin (n + 1 + 1)hm:m ≠ σ i ∧ m ≠ σ j⊢ ∃ a, (σ i).predPredAbove (σ j) ⋯ (σ (i.succSuccAbove j a)) ⋯ = (σ i).predPredAbove (σ j) ⋯ m hm n:ℕn1:ℕi:Fin (n1 + 1 + 1)j:Fin (n1 + 1 + 1)hij:i ≠ jσ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:Function.Bijective σm:Fin (n + 1 + 1)hm:m ≠ σ i ∧ m ≠ σ j⊢ ∃ a, σ (i.succSuccAbove j a) = m n:ℕn1:ℕi:Fin (n1 + 1 + 1)j:Fin (n1 + 1 + 1)hij:i ≠ jσ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:Function.Bijective σm':Fin (n1 + 1 + 1)hm:σ m' ≠ σ i ∧ σ m' ≠ σ j⊢ ∃ a, σ (i.succSuccAbove j a) = σ m' n:ℕn1:ℕi:Fin (n1 + 1 + 1)j:Fin (n1 + 1 + 1)hij:i ≠ jσ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:Function.Bijective σm':Fin (n1 + 1 + 1)hm:¬m' = i ∧ ¬m' = j⊢ ∃ a, i.succSuccAbove j a = m' n:ℕn1:ℕj:Fin (n1 + 1 + 1)σ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:Function.Bijective σm':Fin (n1 + 1 + 1)hij:m' ≠ jhm:¬m' = m' ∧ ¬m' = j⊢ ∃ a, m'.succSuccAbove j a = m'n:ℕn1:ℕi:Fin (n1 + 1 + 1)σ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:Function.Bijective σm':Fin (n1 + 1 + 1)hij:i ≠ m'hm:¬m' = i ∧ ¬m' = m'⊢ ∃ a, i.succSuccAbove m' a = m'n:ℕn1:ℕi:Fin (n1 + 1 + 1)j:Fin (n1 + 1 + 1)hij:i ≠ jσ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:Function.Bijective σm'':Fin n1hm:¬i.succSuccAbove j m'' = i ∧ ¬i.succSuccAbove j m'' = j⊢ ∃ a, i.succSuccAbove j a = i.succSuccAbove j m'' n:ℕn1:ℕj:Fin (n1 + 1 + 1)σ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:Function.Bijective σm':Fin (n1 + 1 + 1)hij:m' ≠ jhm:¬m' = m' ∧ ¬m' = j⊢ ∃ a, m'.succSuccAbove j a = m' All goals completed! 🐙 n:ℕn1:ℕi:Fin (n1 + 1 + 1)σ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:Function.Bijective σm':Fin (n1 + 1 + 1)hij:i ≠ m'hm:¬m' = i ∧ ¬m' = m'⊢ ∃ a, i.succSuccAbove m' a = m' All goals completed! 🐙 n:ℕn1:ℕi:Fin (n1 + 1 + 1)j:Fin (n1 + 1 + 1)hij:i ≠ jσ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:Function.Bijective σm'':Fin n1hm:¬i.succSuccAbove j m'' = i ∧ ¬i.succSuccAbove j m'' = j⊢ ∃ a, i.succSuccAbove j a = i.succSuccAbove j m'' All goals completed! 🐙lemma funPredPredAbove_bijective {n n1 : ℕ} (i j : Fin (n1 + 1 + 1)) (hij : i ≠ j) (σ : Fin (n1 + 1 + 1) → Fin (n + 1 + 1)) (hσ : Function.Bijective σ) : Function.Bijective (funPredPredAbove i j hij σ hσ) := n:ℕn1:ℕi:Fin (n1 + 1 + 1)j:Fin (n1 + 1 + 1)hij:i ≠ jσ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:Function.Bijective σ⊢ Function.Bijective (i.funPredPredAbove j hij σ hσ) n:ℕn1:ℕi:Fin (n1 + 1 + 1)j:Fin (n1 + 1 + 1)hij:i ≠ jσ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:Function.Bijective σ⊢ Function.Injective (i.funPredPredAbove j hij σ hσ)n:ℕn1:ℕi:Fin (n1 + 1 + 1)j:Fin (n1 + 1 + 1)hij:i ≠ jσ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:Function.Bijective σ⊢ Function.Surjective (i.funPredPredAbove j hij σ hσ) n:ℕn1:ℕi:Fin (n1 + 1 + 1)j:Fin (n1 + 1 + 1)hij:i ≠ jσ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:Function.Bijective σ⊢ Function.Injective (i.funPredPredAbove j hij σ hσ) All goals completed! 🐙 n:ℕn1:ℕi:Fin (n1 + 1 + 1)j:Fin (n1 + 1 + 1)hij:i ≠ jσ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:Function.Bijective σ⊢ Function.Surjective (i.funPredPredAbove j hij σ hσ) All goals completed! 🐙@[simp] lemma funPredPredAbove_id { n1 : ℕ} (i j : Fin (n1 + 1 + 1)) (hij : i ≠ j) : funPredPredAbove i j hij id (Function.bijective_id) = id := n1:ℕi:Fin (n1 + 1 + 1)j:Fin (n1 + 1 + 1)hij:i ≠ j⊢ i.funPredPredAbove j hij id ⋯ = id n1:ℕi:Fin (n1 + 1 + 1)j:Fin (n1 + 1 + 1)hij:i ≠ jm:Fin n1⊢ i.funPredPredAbove j hij id ⋯ m = id m All goals completed! 🐙