-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
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)
⊢ (↑(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
have neg : ∀ (ch : ¬i = j),
  (↑(Subtype.mk (p := fun (x : Fin n) ↦
          Membership.mem (γ := Set (Fin n))
            (Set.range (ι := Fin ((↑j : ℕ) + 1)) (⇑(castLEEmb sorry) : (a : Fin ((↑j : ℕ) + 1)) → Fin n)) x)
          ((castLEEmb sorry : (a : Fin ((↑j : ℕ) + 1)) → Fin n)
            ((finRotate ((↑j : ℕ) + 1) : (a : Fin ((↑j : ℕ) + 1)) → Fin ((↑j : ℕ) + 1))
              (((castLEEmb sorry).toEquivRange.symm :
                  (a : { x : Fin n // x ∈ Set.range (⇑(castLEEmb sorry) : (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 sorry) : (a : Fin ((↑j : ℕ) + 1)) → Fin n)) x)
                  i iin))))
          sorry) :
      Fin n) =
    i + 1
Tactic: split_ifs with ch