Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case neg.emb
𝕜 : 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)
⊢ ∀
    (a :
      Fin
        { length := c.length,
            partSize :=
              update (update c.partSize (c.index 0) (c.partSize (c.index 0) - 1)) (c.index 0)
                (update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) (c.index 0) + 1),
            partSize_pos := ⋯,
            emb := fun m ↦
              if h_1 : m = 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 : m = c.index 0 then (c.emb m (Fin.cast ⋯ j.succ)).pred ⋯
                      else (c.emb m (Fin.cast ⋯ j)).pred ⋯) ∘
                    Fin.cast ⋯,
            emb_strictMono := ⋯, parts_strictMono := ⋯, disjoint := ⋯, cover := ⋯ }.length)
    (a' : Fin c.length),
    a ≍ a' →
      { length := c.length,
              partSize :=
                update (update c.partSize (c.index 0) (c.partSize (c.index 0) - 1)) (c.index 0)
                  (update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) (c.index 0) + 1),
              partSize_pos := ⋯,
              emb := fun m ↦
                if h_1 : m = 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 : m = c.index 0 then (c.emb m (Fin.cast ⋯ j.succ)).pred ⋯
                        else (c.emb m (Fin.cast ⋯ j)).pred ⋯) ∘
                      Fin.cast ⋯,
              emb_strictMono := ⋯, parts_strictMono := ⋯, disjoint := ⋯, cover := ⋯ }.emb
          a ≍
        c.emb a'

Tactic:
simp only [heq_eq_eq, forall_eq']

Goal state after:
case neg.emb
𝕜 : 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)
⊢ ∀ (a : Fin c.length),
    (if h_1 : a = 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 : a = c.index 0 then (c.emb a (Fin.cast ⋯ j.succ)).pred ⋯ else (c.emb a (Fin.cast ⋯ j)).pred ⋯) ∘
            Fin.cast ⋯) ≍
      c.emb a