-- Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
/-- Technical lemma used in the proof of `hasFTaylorSeriesUpTo_iteratedFDeriv`, to compare sums
over embedding of `Fin k` and `Fin (k + 1)`. -/
private lemma _root_.Equiv.succ_embeddingFinSucc_fst_symm_apply {ι : Type*} [DecidableEq ι]
    {n : ℕ} (e : Fin (n+1) ↪ ι) {k : ι}
    (h'k : k ∈ Set.range (Equiv.embeddingFinSucc n ι e).1) (hk : k ∈ Set.range e) :
    Fin.succ ((Equiv.embeddingFinSucc n ι e).1.toEquivRange.symm ⟨k, h'k⟩)
      = e.toEquivRange.symm ⟨k, hk⟩

Proof state:
case intro
ι : Type u_4
inst✝ : DecidableEq ι
n : ℕ
e : Fin (n + 1) ↪ ι
j : Fin (n + 1)
h'k : e j ∈ range ⇑((Equiv.embeddingFinSucc n ι) e).fst
hj : j ≠ 0
this : e j = ((Equiv.embeddingFinSucc n ι) e).fst (j.pred hj)
⊢ (((Equiv.embeddingFinSucc n ι) e).fst.toEquivRange.symm ⟨((Equiv.embeddingFinSucc n ι) e).fst (j.pred hj), ⋯⟩).succ =
    j

Tactic:
simp [-Equiv.embeddingFinSucc_fst]

Result:
no goals

Proof state:
case intro
ι : Type u_4
inst✝ : DecidableEq ι
n : ℕ
e : Fin (n + 1) ↪ ι
j : Fin (n + 1)
h'k : e j ∈ range ⇑((Equiv.embeddingFinSucc n ι) e).fst
hj : j ≠ 0
⊢ (((Equiv.embeddingFinSucc n ι) e).fst.toEquivRange.symm ⟨e j, h'k⟩).succ = j

Tactic:
have : e j = (Equiv.embeddingFinSucc n ι e).1 (Fin.pred j hj) := by simp

Result:
case intro
ι : Type u_4
inst✝ : DecidableEq ι
n : ℕ
e : Fin (n + 1) ↪ ι
j : Fin (n + 1)
h'k : e j ∈ range ⇑((Equiv.embeddingFinSucc n ι) e).fst
hj : j ≠ 0
this : e j = ((Equiv.embeddingFinSucc n ι) e).fst (j.pred hj)
⊢ (((Equiv.embeddingFinSucc n ι) e).fst.toEquivRange.symm ⟨e j, h'k⟩).succ = j

Proof state:
ι : Type u_4
inst✝ : DecidableEq ι
n : ℕ
e : Fin (n + 1) ↪ ι
j : Fin (n + 1)
h'k : e j ∈ range ⇑((Equiv.embeddingFinSucc n ι) e).fst
⊢ j ≠ 0

Tactic:
rintro rfl

Result:
ι : Type u_4
inst✝ : DecidableEq ι
n : ℕ
e : Fin (n + 1) ↪ ι
h'k : e 0 ∈ range ⇑((Equiv.embeddingFinSucc n ι) e).fst
⊢ False

Proof state:
case intro
ι : Type u_4
inst✝ : DecidableEq ι
n : ℕ
e : Fin (n + 1) ↪ ι
j : Fin (n + 1)
h'k : e j ∈ range ⇑((Equiv.embeddingFinSucc n ι) e).fst
hj : j ≠ 0
this : e j = ((Equiv.embeddingFinSucc n ι) e).fst (j.pred hj)
⊢ (((Equiv.embeddingFinSucc n ι) e).fst.toEquivRange.symm ⟨e j, h'k⟩).succ = j

Tactic:
simp_rw [this]

Result:
case intro
ι : Type u_4
inst✝ : DecidableEq ι
n : ℕ
e : Fin (n + 1) ↪ ι
j : Fin (n + 1)
h'k : e j ∈ range ⇑((Equiv.embeddingFinSucc n ι) e).fst
hj : j ≠ 0
this : e j = ((Equiv.embeddingFinSucc n ι) e).fst (j.pred hj)
⊢ (((Equiv.embeddingFinSucc n ι) e).fst.toEquivRange.symm ⟨((Equiv.embeddingFinSucc n ι) e).fst (j.pred hj), ⋯⟩).succ =
    j

Proof state:
case intro
ι : Type u_4
inst✝ : DecidableEq ι
n : ℕ
e : Fin (n + 1) ↪ ι
j : Fin (n + 1)
h'k : e j ∈ range ⇑((Equiv.embeddingFinSucc n ι) e).fst
⊢ (((Equiv.embeddingFinSucc n ι) e).fst.toEquivRange.symm ⟨e j, h'k⟩).succ = e.toEquivRange.symm ⟨e j, ⋯⟩

Tactic:
have hj : j ≠ 0 := by
  rintro rfl
  simp at h'k

Result:
case intro
ι : Type u_4
inst✝ : DecidableEq ι
n : ℕ
e : Fin (n + 1) ↪ ι
j : Fin (n + 1)
h'k : e j ∈ range ⇑((Equiv.embeddingFinSucc n ι) e).fst
hj : j ≠ 0
⊢ (((Equiv.embeddingFinSucc n ι) e).fst.toEquivRange.symm ⟨e j, h'k⟩).succ = e.toEquivRange.symm ⟨e j, ⋯⟩

Proof state:
ι : Type u_4
inst✝ : DecidableEq ι
n : ℕ
e : Fin (n + 1) ↪ ι
h'k : e 0 ∈ range ⇑((Equiv.embeddingFinSucc n ι) e).fst
⊢ False

Tactic:
simp at h'k

Result:
no goals

Proof state:
ι : Type u_4
inst✝ : DecidableEq ι
n : ℕ
e : Fin (n + 1) ↪ ι
j : Fin (n + 1)
h'k : e j ∈ range ⇑((Equiv.embeddingFinSucc n ι) e).fst
hj : j ≠ 0
⊢ e j = ((Equiv.embeddingFinSucc n ι) e).fst (j.pred hj)

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_4
inst✝ : DecidableEq ι
n : ℕ
e : Fin (n + 1) ↪ ι
k : ι
h'k : k ∈ range ⇑((Equiv.embeddingFinSucc n ι) e).fst
hk : k ∈ range ⇑e
⊢ (((Equiv.embeddingFinSucc n ι) e).fst.toEquivRange.symm ⟨k, h'k⟩).succ = e.toEquivRange.symm ⟨k, hk⟩

Tactic:
rcases hk with ⟨j, rfl⟩

Result:
case intro
ι : Type u_4
inst✝ : DecidableEq ι
n : ℕ
e : Fin (n + 1) ↪ ι
j : Fin (n + 1)
h'k : e j ∈ range ⇑((Equiv.embeddingFinSucc n ι) e).fst
⊢ (((Equiv.embeddingFinSucc n ι) e).fst.toEquivRange.symm ⟨e j, h'k⟩).succ = e.toEquivRange.symm ⟨e j, ⋯⟩

Proof state:
case intro
ι : Type u_4
inst✝ : DecidableEq ι
n : ℕ
e : Fin (n + 1) ↪ ι
j : Fin (n + 1)
h'k : e j ∈ range ⇑((Equiv.embeddingFinSucc n ι) e).fst
hj : j ≠ 0
⊢ (((Equiv.embeddingFinSucc n ι) e).fst.toEquivRange.symm ⟨e j, h'k⟩).succ = e.toEquivRange.symm ⟨e j, ⋯⟩

Tactic:
simp only [Function.Embedding.toEquivRange_symm_apply_self]

Result:
case intro
ι : Type u_4
inst✝ : DecidableEq ι
n : ℕ
e : Fin (n + 1) ↪ ι
j : Fin (n + 1)
h'k : e j ∈ range ⇑((Equiv.embeddingFinSucc n ι) e).fst
hj : j ≠ 0
⊢ (((Equiv.embeddingFinSucc n ι) e).fst.toEquivRange.symm ⟨e j, h'k⟩).succ = j