-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
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) :
      ι)
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))
          ⋯)) =
    j
⊢ 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

Tactic:
simp_rw [this]