-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
hn : 0 < n
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 F E
v : Fin n → F
have :
  Eq (α := Finset (Composition n)) univ (Set.toFinset {c : Composition n | 1 < c.length} ∪ {Composition.single n hn})
have₁ :
  ∀
    (A :
      Eq (α := Finset (Composition n)) univ
        (Set.toFinset {c : Composition n | 1 < c.length} ∪ {Composition.single n hn})),
    (p.comp q n : (a : (i : Fin n) → F) → F) v =
      HAdd.hAdd (α := F) (β := F)
        (∑ c ∈ Set.toFinset {c : Composition n | 1 < c.length},
            (p c.length : (a : (i : Fin c.length) → E) → F) (q.applyComposition c v) :
          F)
        ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ (q n : (a : (i : Fin n) → F) → E) v : F)
have₂ :
  Eq (α := Finset (Composition n)) univ (Set.toFinset {c : Composition n | 1 < c.length} ∪ {Composition.single n hn})
have₃ have₄ :
  ∀
    (A :
      Eq (α := Finset (Composition n)) univ
        (Set.toFinset {c : Composition n | 1 < c.length} ∪ {Composition.single n hn})),
    (p.comp q n : (a : (i : Fin n) → F) → F) v =
      HAdd.hAdd (α := F) (β := F)
        (∑ c ∈ Set.toFinset {c : Composition n | 1 < c.length},
            (p c.length : (a : (i : Fin c.length) → E) → F) (q.applyComposition c v) :
          F)
        ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ (q n : (a : (i : Fin n) → F) → E) v : F)
have₅ :
  ∀
    (A :
      Eq (α := Finset (Composition n)) univ
        (Set.toFinset {c : Composition n | 1 < c.length} ∪ {Composition.single n hn}))
    (B :
      Disjoint (α := Finset (Composition n)) (Set.toFinset {c : Composition n | 1 < c.length})
        {Composition.single n hn}),
    (p.comp q n : (a : (i : Fin n) → F) → F) v =
      HAdd.hAdd (α := F) (β := F)
        (∑ c ∈ Set.toFinset {c : Composition n | 1 < c.length},
            (p c.length : (a : (i : Fin c.length) → E) → F) (q.applyComposition c v) :
          F)
        ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ (q n : (a : (i : Fin n) → F) → E) v : F)
have₆ :
  ∀
    (A :
      Eq (α := Finset (Composition n)) univ
        (Set.toFinset {c : Composition n | 1 < c.length} ∪ {Composition.single n hn}))
    (B :
      Disjoint (α := Finset (Composition n)) (Set.toFinset {c : Composition n | 1 < c.length})
        {Composition.single n hn})
    (C :
      Eq.{u_3 + 1} (α := F)
        ((p (Composition.single n hn).length : (a : (i : Fin (Composition.single n hn).length) → E) → F)
            (q.applyComposition (Composition.single n hn) v) :
          F)
        ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ (q n : (a : (i : Fin n) → F) → E) v : F)),
    (p.comp q n : (a : (i : Fin n) → F) → F) v =
      HAdd.hAdd (α := F) (β := F)
        (∑ c ∈ Set.toFinset {c : Composition n | 1 < c.length},
            (p c.length : (a : (i : Fin c.length) → E) → F) (q.applyComposition c v) :
          F)
        ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ (q n : (a : (i : Fin n) → F) → E) v : F)
⊢ (p.comp q n : (a : (i : Fin n) → F) → F) v =
    HAdd.hAdd (α := F) (β := F)
      (∑ c ∈ Set.toFinset {c : Composition n | 1 < c.length},
          (p c.length : (a : (i : Fin c.length) → E) → F) (q.applyComposition c v) :
        F)
      ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ (q n : (a : (i : Fin n) → F) → E) v : F)

Tactic:
classical
  have A :
    (Finset.univ : Finset (Composition n)) =
      {c | 1 < Composition.length c}.toFinset ∪ {Composition.single n hn} := by
    refine Subset.antisymm (fun c _ => ?_) (subset_univ _)
    by_cases h : 1 < c.length
    · simp [h]
    · have : c.length = 1 := by
        refine (eq_iff_le_not_lt.2 ⟨?_, h⟩).symm; exact c.length_pos_of_pos hn
      rw [← Composition.eq_single_iff_length hn] at this
      simp [this]
  have B :
    Disjoint ({c | 1 < Composition.length c} : Set (Composition n)).toFinset
      {Composition.single n hn} := by
    simp
  have C :
    p (Composition.single n hn).length (q.applyComposition (Composition.single n hn) v) =
      p 1 fun _ : Fin 1 => q n v := by
    apply p.congr (Composition.single_length hn) fun j hj1 _ => ?_
    simp [applyComposition_single]
  simp [FormalMultilinearSeries.comp, A, Finset.sum_union B, C, -Set.toFinset_setOf,
    -add_right_inj, -Composition.single_length, -Finset.union_singleton]

Premises used: Composition.single_length, FormalMultilinearSeries.comp, Finset.union_singleton, add_right_inj, Set.toFinset_setOf