-- 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:
𝕜 : 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)}
⊢ ((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

Tactic:
apply FormalMultilinearSeries.congr _ (Composition.ones_length _) fun j hj1 hj2 => ?_

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)}
j : ℕ
hj1 : j < (Composition.ones (n + 2)).length
hj2 : j < n + 2
⊢ ((p 1) fun x => v (Fin.castLE ⋯ ⟨j, hj1⟩)) = (p 1) fun x => v ⟨j, hj2⟩

Proof state:
case convert_2.e_f.h.h.e_6.h.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)
k : Fin c.length
⊢ p.applyComposition c (⇑↑i.symm ∘ fun j => (p 1) fun x => v j) k = p.applyComposition c v k

Tactic:
simp [h, Function.comp_def]

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)}
j : ℕ
hj1 : j < (Composition.ones (n + 2)).length
hj2 : j < n + 2
⊢ ((p 1) fun x => v (Fin.castLE ⋯ ⟨j, hj1⟩)) = (p 1) fun x => v ⟨j, hj2⟩

Tactic:
exact FormalMultilinearSeries.congr _ rfl fun k _ _ => by congr

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
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

Tactic:
simp [FormalMultilinearSeries.comp, show n + 2 ≠ 1 by omega, A, Finset.sum_union B,
  applyComposition_ones, C, D, -Set.toFinset_setOf]

Result:
no goals

Proof state:
case convert_2.e_f.h.h.e_6.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.applyComposition c (⇑↑i.symm ∘ fun j => (p 1) fun x => v j) = p.applyComposition c v

Tactic:
ext k

Result:
case convert_2.e_f.h.h.e_6.h.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)
k : Fin c.length
⊢ p.applyComposition c (⇑↑i.symm ∘ fun j => (p 1) fun x => v j) k = p.applyComposition c v k

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 (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)

Tactic:
simp only [leftInv, ContinuousMultilinearMap.neg_apply, neg_inj,
  ContinuousMultilinearMap.sum_apply]

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
⊢ (∑ 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)