-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i j : Fin n
inst : NeZero n
h : i ≤ j
iin :
  Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin ((↑j : ℕ) + 1)) (⇑(castLEEmb ⋯) : (a : Fin ((↑j : ℕ) + 1)) → Fin n)) i
this :
  ((castLEEmb ⋯).toEquivRange :
        (a : Fin ((↑j : ℕ) + 1)) → (↑(Set.range (⇑(castLEEmb ⋯) : (a : Fin ((↑j : ℕ) + 1)) → Fin n)) : Type))
      (i.castLT ⋯) =
    Subtype.mk (p := fun (x : Fin n) ↦
      Membership.mem (γ := Set (Fin n))
        (Set.range (ι := Fin ((↑j : ℕ) + 1)) (⇑(castLEEmb ⋯) : (a : Fin ((↑j : ℕ) + 1)) → Fin n)) x)
      i iin
pos :
  ∀ (ch : i = j),
    Eq (α := Fin n)
      ((↑(Subtype.mk (p := fun (x : Fin n) ↦
              Membership.mem (γ := Set (Fin n))
                (Set.range (ι := Fin ((↑j : ℕ) + 1)) (⇑(castLEEmb ⋯) : (a : Fin ((↑j : ℕ) + 1)) → Fin n)) x)
              ((castLEEmb ⋯ : (a : Fin ((↑j : ℕ) + 1)) → Fin n)
                ((finRotate ((↑j : ℕ) + 1) : (a : Fin ((↑j : ℕ) + 1)) → Fin ((↑j : ℕ) + 1))
                  (((castLEEmb ⋯).toEquivRange.symm :
                      (a : { x : Fin n // x ∈ Set.range (⇑(castLEEmb ⋯) : (a : Fin ((↑j : ℕ) + 1)) → Fin n) }) →
                        Fin ((↑j : ℕ) + 1))
                    (Subtype.mk (p := fun (x : Fin n) ↦
                      Membership.mem (γ := Set (Fin n))
                        (Set.range (ι := Fin ((↑j : ℕ) + 1)) (⇑(castLEEmb ⋯) : (a : Fin ((↑j : ℕ) + 1)) → Fin n)) x)
                      i iin))))
              ⋯) :
          Fin n) :
        Fin n)
      (0 : Fin n)
neg :
  ∀ (ch : ¬i = j),
    (↑(Subtype.mk (p := fun (x : Fin n) ↦
            Membership.mem (γ := Set (Fin n))
              (Set.range (ι := Fin ((↑j : ℕ) + 1)) (⇑(castLEEmb ⋯) : (a : Fin ((↑j : ℕ) + 1)) → Fin n)) x)
            ((castLEEmb ⋯ : (a : Fin ((↑j : ℕ) + 1)) → Fin n)
              ((finRotate ((↑j : ℕ) + 1) : (a : Fin ((↑j : ℕ) + 1)) → Fin ((↑j : ℕ) + 1))
                (((castLEEmb ⋯).toEquivRange.symm :
                    (a : { x : Fin n // x ∈ Set.range (⇑(castLEEmb ⋯) : (a : Fin ((↑j : ℕ) + 1)) → Fin n) }) →
                      Fin ((↑j : ℕ) + 1))
                  (Subtype.mk (p := fun (x : Fin n) ↦
                    Membership.mem (γ := Set (Fin n))
                      (Set.range (ι := Fin ((↑j : ℕ) + 1)) (⇑(castLEEmb ⋯) : (a : Fin ((↑j : ℕ) + 1)) → Fin n)) x)
                    i iin))))
            ⋯) :
        Fin n) =
      i + 1
⊢ (↑(Subtype.mk (p := fun (x : Fin n) ↦
          Membership.mem (γ := Set (Fin n))
            (Set.range (ι := Fin ((↑j : ℕ) + 1)) (⇑(castLEEmb ⋯) : (a : Fin ((↑j : ℕ) + 1)) → Fin n)) x)
          ((castLEEmb ⋯ : (a : Fin ((↑j : ℕ) + 1)) → Fin n)
            ((finRotate ((↑j : ℕ) + 1) : (a : Fin ((↑j : ℕ) + 1)) → Fin ((↑j : ℕ) + 1))
              (((castLEEmb ⋯).toEquivRange.symm :
                  (a : { x : Fin n // x ∈ Set.range (⇑(castLEEmb ⋯) : (a : Fin ((↑j : ℕ) + 1)) → Fin n) }) →
                    Fin ((↑j : ℕ) + 1))
                (Subtype.mk (p := fun (x : Fin n) ↦
                  Membership.mem (γ := Set (Fin n))
                    (Set.range (ι := Fin ((↑j : ℕ) + 1)) (⇑(castLEEmb ⋯) : (a : Fin ((↑j : ℕ) + 1)) → Fin n)) x)
                  i iin))))
          ⋯) :
      Fin n) =
    if i = j then 0 else i + 1

Tactic:
split_ifs with ch