-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
ι : Type u_4
inst : DecidableEq ι
n : ℕ
e : Fin (n + 1) ↪ ι
k : ι
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) → ι))
    k
hk : Membership.mem (γ := Set ι) (range (ι := Fin (n + 1)) (⇑e : (a : Fin (n + 1)) → ι)) k
rcases :
  ∀ (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 : ι)),
    Eq (α := Fin (n + 1))
      (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)))
      ((e.toEquivRange.symm : (a : (↑(range (⇑e : (a : Fin (n + 1)) → ι)) : Type u_4)) → Fin (n + 1))
        (Subtype.mk (p := fun (x : ι) ↦
          Membership.mem (γ := Set ι) (range (ι := Fin (n + 1)) (⇑e : (a : Fin (n + 1)) → ι)) x)
          ((e : (a : Fin (n + 1)) → ι) j) ⋯))
⊢ Eq (α := Fin (n + 1))
    (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)
          k h'k)))
    ((e.toEquivRange.symm : (a : (↑(range (⇑e : (a : Fin (n + 1)) → ι)) : Type u_4)) → Fin (n + 1))
      (Subtype.mk (p := fun (x : ι) ↦
        Membership.mem (γ := Set ι) (range (ι := Fin (n + 1)) (⇑e : (a : Fin (n + 1)) → ι)) x) k hk))

Tactic:
rcases hk with ⟨j, rfl⟩

Premises used: rfl