case refine'_1
n : ℕ
e : Perm (Fin n)
p : Fin (n + 1)
x : Fin n
⊢ ↑(↑decomposeFin.symm (0, e)) (Fin.succ x) = ↑(swap 0 0) (Fin.succ (↑e x))

case refine'_2
n : ℕ
e : Perm (Fin n)
p : Fin (n + 1)
x : Fin n
⊢ ∀ (i : Fin n), ↑(↑decomposeFin.symm (Fin.succ i, e)) (Fin.succ x) = ↑(swap 0 (Fin.succ i)) (Fin.succ (↑e x))
n : ℕ
e : Perm (Fin n)
p : Fin (n + 1)
x : Fin n
⊢ ↑(↑decomposeFin.symm (p, e)) (Fin.succ x) = ↑(swap 0 p) (Fin.succ (↑e x))
refine' Fin.cases _ _ p
no goals
case refine'_1
n : ℕ
e : Perm (Fin n)
p : Fin (n + 1)
x : Fin n
⊢ ↑(↑decomposeFin.symm (0, e)) (Fin.succ x) = ↑(swap 0 0) (Fin.succ (↑e x))
simp [Equiv.Perm.decomposeFin, EquivFunctor.map]
case refine'_2
n : ℕ
e : Perm (Fin n)
p : Fin (n + 1)
x i : Fin n
⊢ ↑(↑decomposeFin.symm (Fin.succ i, e)) (Fin.succ x) = ↑(swap 0 (Fin.succ i)) (Fin.succ (↑e x))
case refine'_2
n : ℕ
e : Perm (Fin n)
p : Fin (n + 1)
x : Fin n
⊢ ∀ (i : Fin n), ↑(↑decomposeFin.symm (Fin.succ i, e)) (Fin.succ x) = ↑(swap 0 (Fin.succ i)) (Fin.succ (↑e x))
intro i
case pos
n : ℕ
e : Perm (Fin n)
p : Fin (n + 1)
x i : Fin n
h : i = ↑e x
⊢ ↑(↑decomposeFin.symm (Fin.succ i, e)) (Fin.succ x) = ↑(swap 0 (Fin.succ i)) (Fin.succ (↑e x))

case neg
n : ℕ
e : Perm (Fin n)
p : Fin (n + 1)
x i : Fin n
h : ¬i = ↑e x
⊢ ↑(↑decomposeFin.symm (Fin.succ i, e)) (Fin.succ x) = ↑(swap 0 (Fin.succ i)) (Fin.succ (↑e x))
case refine'_2
n : ℕ
e : Perm (Fin n)
p : Fin (n + 1)
x i : Fin n
⊢ ↑(↑decomposeFin.symm (Fin.succ i, e)) (Fin.succ x) = ↑(swap 0 (Fin.succ i)) (Fin.succ (↑e x))
by_cases h : i = e x
no goals
case pos
n : ℕ
e : Perm (Fin n)
p : Fin (n + 1)
x i : Fin n
h : i = ↑e x
⊢ ↑(↑decomposeFin.symm (Fin.succ i, e)) (Fin.succ x) = ↑(swap 0 (Fin.succ i)) (Fin.succ (↑e x))
simp [h, Equiv.Perm.decomposeFin, EquivFunctor.map]
no goals
case neg
n : ℕ
e : Perm (Fin n)
p : Fin (n + 1)
x i : Fin n
h : ¬i = ↑e x
⊢ ↑(↑decomposeFin.symm (Fin.succ i, e)) (Fin.succ x) = ↑(swap 0 (Fin.succ i)) (Fin.succ (↑e x))
simp [h, Fin.succ_ne_zero, Equiv.Perm.decomposeFin, EquivFunctor.map,
  swap_apply_def, Ne.symm h]