Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case neg.emb.refine_2.inl
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n✝ : ℕ
c✝ : OrderedFinpartition n✝
n : ℕ
c : OrderedFinpartition (n + 1)
h : ¬range (c.emb 0) = {0}
B : c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0)
j : Fin (c.partSize (c.index 0))
⊢ c.emb (c.index 0) j =
    (if h_1 : c.index 0 = c.index 0 then
        (fun i ↦ cases 0 (succ ∘ fun j ↦ (c.emb (c.index 0) (Fin.cast ⋯ j.succ)).pred ⋯) i) ∘ Fin.cast ⋯
      else
        succ ∘
          (fun j ↦
              if h : c.index 0 = c.index 0 then (c.emb (c.index 0) (Fin.cast ⋯ j.succ)).pred ⋯
              else (c.emb (c.index 0) (Fin.cast ⋯ j)).pred ⋯) ∘
            Fin.cast ⋯)
      ⟨↑j, ⋯⟩

pp: case neg.emb.refine_2.inr
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n✝ : ℕ
c✝ : OrderedFinpartition n✝
n : ℕ
c : OrderedFinpartition (n + 1)
h : ¬range (c.emb 0) = {0}
B : c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0)
i : Fin c.length
j : Fin (c.partSize i)
hi : i ≠ c.index 0
⊢ c.emb i j =
    (if h_1 : i = c.index 0 then
        (fun i ↦ cases 0 (succ ∘ fun j ↦ (c.emb (c.index 0) (Fin.cast ⋯ j.succ)).pred ⋯) i) ∘ Fin.cast ⋯
      else
        succ ∘
          (fun j ↦
              if h : i = c.index 0 then (c.emb i (Fin.cast ⋯ j.succ)).pred ⋯ else (c.emb i (Fin.cast ⋯ j)).pred ⋯) ∘
            Fin.cast ⋯)
      ⟨↑j, ⋯⟩

Tactic:
· simp only [↓reduceDIte, comp_apply]
            rcases eq_or_ne j 0 with rfl | hj
            · simpa using c.emb_zero
            · let j' := Fin.pred (j.cast B.symm) (by simpa using hj)
              have : j = (succ j').cast B := by simp [j']
              simp only [this, val_cast, val_succ, cast_mk, cases_succ', comp_apply, succ_mk,
                succ_pred]
              rfl

Goal state after:
case neg.emb.refine_2.inr
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n✝ : ℕ
c✝ : OrderedFinpartition n✝
n : ℕ
c : OrderedFinpartition (n + 1)
h : ¬range (c.emb 0) = {0}
B : c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0)
i : Fin c.length
j : Fin (c.partSize i)
hi : i ≠ c.index 0
⊢ c.emb i j =
    (if h_1 : i = c.index 0 then
        (fun i ↦ cases 0 (succ ∘ fun j ↦ (c.emb (c.index 0) (Fin.cast ⋯ j.succ)).pred ⋯) i) ∘ Fin.cast ⋯
      else
        succ ∘
          (fun j ↦
              if h : i = c.index 0 then (c.emb i (Fin.cast ⋯ j.succ)).pred ⋯ else (c.emb i (Fin.cast ⋯ j)).pred ⋯) ∘
            Fin.cast ⋯)
      ⟨↑j, ⋯⟩