-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
Goal:
ι : Type u_4
inst : DecidableEq ι
n : ℕ
e : Fin (n + 1) ↪ ι
j : Fin (n + 1)
h'k :
  Membership.mem (α := ι) (γ := Set ι)
    (range (ι := Fin n)
      (⇑(Sigma.fst (β := fun (e : Fin n ↪ ι) ↦ { i : ι // i ∉ range (ι := Fin n) (⇑e : (a : Fin n) → ι) })
            ((Equiv.embeddingFinSucc n ι :
                (a : Fin (n + 1) ↪ ι) → (e : Fin n ↪ ι) × { i : ι // i ∉ range (⇑e : (a : Fin n) → ι) })
              e)) :
        (a : Fin n) → ι))
    ((e : (a : Fin (n + 1)) → ι) j : ι)
hj : j ≠ 0
this :
  Eq (α := ι) ((e : (a : Fin (n + 1)) → ι) j : ι)
    ((Sigma.fst (β := fun (e : Fin n ↪ ι) ↦ { i : ι // i ∉ range (ι := Fin n) (⇑e : (a : Fin n) → ι) })
            ((Equiv.embeddingFinSucc n ι :
                (a : Fin (n + 1) ↪ ι) → (e : Fin n ↪ ι) × { i : ι // i ∉ range (⇑e : (a : Fin n) → ι) })
              e) :
          (a : Fin n) → ι)
        (j.pred hj) :
      ι)
⊢ Fin.succ
      (((Equiv.symm
              (Function.Embedding.toEquivRange
                (Sigma.fst (β := fun (e : Fin n ↪ ι) ↦ { i : ι // i ∉ range (ι := Fin n) (⇑e : (a : Fin n) → ι) })
                  ((Equiv.embeddingFinSucc n ι :
                      (a : Fin (n + 1) ↪ ι) → (e : Fin n ↪ ι) × { i : ι // i ∉ range (⇑e : (a : Fin n) → ι) })
                    e))) :
            (↑(range (ι := Fin n)
                    (⇑(Sigma.fst (β := fun (e : Fin n ↪ ι) ↦ { i : ι // i ∉ range (ι := Fin n) (⇑e : (a : Fin n) → ι) })
                          ((Equiv.embeddingFinSucc n ι :
                              (a : Fin (n + 1) ↪ ι) → (e : Fin n ↪ ι) × { i : ι // i ∉ range (⇑e : (a : Fin n) → ι) })
                            e)) :
                      (a : Fin n) → ι)) :
                Type u_4) ≃
              Fin n) :
          (a :
              (↑(range
                    (⇑((Equiv.embeddingFinSucc n ι :
                              (a : Fin (n + 1) ↪ ι) → (e : Fin n ↪ ι) × { i : ι // i ∉ range (⇑e : (a : Fin n) → ι) })
                            e).fst :
                      (a : Fin n) → ι)) :
                Type u_4)) →
            Fin n)
        (Subtype.mk (p := fun (x : ι) ↦
          Membership.mem (γ := Set ι)
            (range (ι := Fin n)
              (⇑(Sigma.fst (β := fun (e : Fin n ↪ ι) ↦ { i : ι // i ∉ range (ι := Fin n) (⇑e : (a : Fin n) → ι) })
                    ((Equiv.embeddingFinSucc n ι :
                        (a : Fin (n + 1) ↪ ι) → (e : Fin n ↪ ι) × { i : ι // i ∉ range (⇑e : (a : Fin n) → ι) })
                      e)) :
                (a : Fin n) → ι))
            x)
          ((e : (a : Fin (n + 1)) → ι) j) h'k)) =
    j
have simp_rw : Fin.succ
    (((Equiv.symm
            (Function.Embedding.toEquivRange
              (Sigma.fst (β := fun (e : Fin n ↪ ι) ↦ { i : ι // i ∉ range (ι := Fin n) (⇑e : (a : Fin n) → ι) })
                ((Equiv.embeddingFinSucc n ι :
                    (a : Fin (n + 1) ↪ ι) → (e : Fin n ↪ ι) × { i : ι // i ∉ range (⇑e : (a : Fin n) → ι) })
                  e))) :
          (↑(range (ι := Fin n)
                  (⇑(Sigma.fst (β := fun (e : Fin n ↪ ι) ↦ { i : ι // i ∉ range (ι := Fin n) (⇑e : (a : Fin n) → ι) })
                        ((Equiv.embeddingFinSucc n ι :
                            (a : Fin (n + 1) ↪ ι) → (e : Fin n ↪ ι) × { i : ι // i ∉ range (⇑e : (a : Fin n) → ι) })
                          e)) :
                    (a : Fin n) → ι)) :
              Type u_4) ≃
            Fin n) :
        (a :
            (↑(range
                  (⇑((Equiv.embeddingFinSucc n ι :
                            (a : Fin (n + 1) ↪ ι) → (e : Fin n ↪ ι) × { i : ι // i ∉ range (⇑e : (a : Fin n) → ι) })
                          e).fst :
                    (a : Fin n) → ι)) :
              Type u_4)) →
          Fin n)
      (Subtype.mk (p := fun (x : ι) ↦
        Membership.mem (γ := Set ι)
          (range (ι := Fin n)
            (⇑(Sigma.fst (β := fun (e : Fin n ↪ ι) ↦ { i : ι // i ∉ range (ι := Fin n) (⇑e : (a : Fin n) → ι) })
                  ((Equiv.embeddingFinSucc n ι :
                      (a : Fin (n + 1) ↪ ι) → (e : Fin n ↪ ι) × { i : ι // i ∉ range (⇑e : (a : Fin n) → ι) })
                    e)) :
              (a : Fin n) → ι))
          x)
        ((Sigma.fst (β := fun (e : Fin n ↪ ι) ↦ { i : ι // i ∉ range (ι := Fin n) (⇑e : (a : Fin n) → ι) })
              ((Equiv.embeddingFinSucc n ι :
                  (a : Fin (n + 1) ↪ ι) → (e : Fin n ↪ ι) × { i : ι // i ∉ range (⇑e : (a : Fin n) → ι) })
                e) :
            (a : Fin n) → ι)
          (j.pred hj))
        sorry)) =
  j
Tactic: simp_rw [this]