-- Mathlib/Analysis/Analytic/Inverse.lean
theorem leftInv_comp (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E)
    (h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm i) :
    (leftInv p i x).comp p = id 𝕜 E x

Proof state:
case pos
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
h✝ : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i
n✝ n : ℕ
v : Fin (n + 2) → E
c : Composition (n + 2)
x✝ : c ∈ univ
h : c.length < n + 2
⊢ c ∈ {c | c.length < n + 2}.toFinset ∪ {Composition.ones (n + 2)}

Tactic:
simp [h, Set.mem_toFinset (s := {c | Composition.length c < n + 2})]

Result:
no goals

Proof state:
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i
n✝ n : ℕ
v : Fin (n + 2) → E
A : univ = {c | c.length < n + 2}.toFinset ∪ {Composition.ones (n + 2)}
B : Disjoint {c | c.length < n + 2}.toFinset {Composition.ones (n + 2)}
C :
  ((p.leftInv i x (Composition.ones (n + 2)).length) fun j => (p 1) fun x => v (Fin.castLE ⋯ j)) =
    (p.leftInv i x (n + 2)) fun j => (p 1) fun x => v j
⊢ ((p.leftInv i x).comp p (n + 2)) v = (id 𝕜 E x (n + 2)) v

Tactic:
have D :
  (p.leftInv i x (n + 2) fun j : Fin (n + 2) => p 1 fun _ => v j) =
    -∑ c ∈ {c : Composition (n + 2) | c.length < n + 2}.toFinset,
        (p.leftInv i x c.length) (p.applyComposition c v) := by
  simp only [leftInv, ContinuousMultilinearMap.neg_apply, neg_inj,
    ContinuousMultilinearMap.sum_apply]
  convert
    (sum_toFinset_eq_subtype
      (fun c : Composition (n + 2) => c.length < n + 2)
      (fun c : Composition (n + 2) =>
      (ContinuousMultilinearMap.compAlongComposition
        (p.compContinuousLinearMap (i.symm : F →L[𝕜] E)) c (p.leftInv i x c.length))
        fun j : Fin (n + 2) => p 1 fun _ : Fin 1 => v j)).symm.trans
      _
  simp only [compContinuousLinearMap_applyComposition,
    ContinuousMultilinearMap.compAlongComposition_apply]
  congr
  ext c
  congr
  ext k
  simp [h, Function.comp_def]

Result:
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i
n✝ n : ℕ
v : Fin (n + 2) → E
A : univ = {c | c.length < n + 2}.toFinset ∪ {Composition.ones (n + 2)}
B : Disjoint {c | c.length < n + 2}.toFinset {Composition.ones (n + 2)}
C :
  ((p.leftInv i x (Composition.ones (n + 2)).length) fun j => (p 1) fun x => v (Fin.castLE ⋯ j)) =
    (p.leftInv i x (n + 2)) fun j => (p 1) fun x => v j
D :
  ((p.leftInv i x (n + 2)) fun j => (p 1) fun x => v j) =
    -∑ c ∈ {c | c.length < n + 2}.toFinset, (p.leftInv i x c.length) (p.applyComposition c v)
⊢ ((p.leftInv i x).comp p (n + 2)) v = (id 𝕜 E x (n + 2)) v

Proof state:
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i
n✝ n : ℕ
v : Fin (n + 2) → E
A : univ = {c | c.length < n + 2}.toFinset ∪ {Composition.ones (n + 2)}
B : Disjoint {c | c.length < n + 2}.toFinset {Composition.ones (n + 2)}
C :
  ((p.leftInv i x (Composition.ones (n + 2)).length) fun j => (p 1) fun x => v (Fin.castLE ⋯ j)) =
    (p.leftInv i x (n + 2)) fun j => (p 1) fun x => v j
⊢ (∑ a : { c // c.length < n + 2 },
      (ContinuousMultilinearMap.compAlongComposition (p.compContinuousLinearMap ↑i.symm) (↑a)
          (p.leftInv i x (↑a).length))
        fun j => (p 1) fun x => v j) =
    ∑ c ∈ {c | c.length < n + 2}.toFinset, (p.leftInv i x c.length) (p.applyComposition c v)

Tactic:
convert
  (sum_toFinset_eq_subtype
    (fun c : Composition (n + 2) => c.length < n + 2)
    (fun c : Composition (n + 2) =>
    (ContinuousMultilinearMap.compAlongComposition
      (p.compContinuousLinearMap (i.symm : F →L[𝕜] E)) c (p.leftInv i x c.length))
      fun j : Fin (n + 2) => p 1 fun _ : Fin 1 => v j)).symm.trans
    _

Result:
case convert_2
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i
n✝ n : ℕ
v : Fin (n + 2) → E
A : univ = {c | c.length < n + 2}.toFinset ∪ {Composition.ones (n + 2)}
B : Disjoint {c | c.length < n + 2}.toFinset {Composition.ones (n + 2)}
C :
  ((p.leftInv i x (Composition.ones (n + 2)).length) fun j => (p 1) fun x => v (Fin.castLE ⋯ j)) =
    (p.leftInv i x (n + 2)) fun j => (p 1) fun x => v j
⊢ (∑ a ∈ {x | x.length < n + 2}.toFinset,
      (ContinuousMultilinearMap.compAlongComposition (p.compContinuousLinearMap ↑i.symm) a (p.leftInv i x a.length))
        fun j => (p 1) fun x => v j) =
    ∑ c ∈ {c | c.length < n + 2}.toFinset, (p.leftInv i x c.length) (p.applyComposition c v)

Proof state:
case convert_2.e_f
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i
n✝ n : ℕ
v : Fin (n + 2) → E
A : univ = {c | c.length < n + 2}.toFinset ∪ {Composition.ones (n + 2)}
B : Disjoint {c | c.length < n + 2}.toFinset {Composition.ones (n + 2)}
C :
  ((p.leftInv i x (Composition.ones (n + 2)).length) fun j => (p 1) fun x => v (Fin.castLE ⋯ j)) =
    (p.leftInv i x (n + 2)) fun j => (p 1) fun x => v j
⊢ (fun x_1 => (p.leftInv i x x_1.length) (p.applyComposition x_1 (⇑↑i.symm ∘ fun j => (p 1) fun x => v j))) = fun c =>
    (p.leftInv i x c.length) (p.applyComposition c v)

Tactic:
ext c

Result:
case convert_2.e_f.h
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i
n✝ n : ℕ
v : Fin (n + 2) → E
A : univ = {c | c.length < n + 2}.toFinset ∪ {Composition.ones (n + 2)}
B : Disjoint {c | c.length < n + 2}.toFinset {Composition.ones (n + 2)}
C :
  ((p.leftInv i x (Composition.ones (n + 2)).length) fun j => (p 1) fun x => v (Fin.castLE ⋯ j)) =
    (p.leftInv i x (n + 2)) fun j => (p 1) fun x => v j
c : Composition (n + 2)
⊢ (p.leftInv i x c.length) (p.applyComposition c (⇑↑i.symm ∘ fun j => (p 1) fun x => v j)) =
    (p.leftInv i x c.length) (p.applyComposition c v)