awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
h :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F) (p 1)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 E F) :
        (a : E →L[𝕜] F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F)
      (↑i : E →L[𝕜] F))
n_1 n : ℕ
v : (i : Fin (n + 2)) → E
A :
  Eq (α := Finset (Composition (n + 2))) univ
    (Set.toFinset {c : Composition (n + 2) | c.length < n + 2} ∪ {Composition.ones (n + 2)})
B :
  Disjoint (α := Finset (Composition (n + 2))) (Set.toFinset {c : Composition (n + 2) | c.length < n + 2})
    {Composition.ones (n + 2)}
C :
  Eq.{u_2 + 1} (α := E)
    ((p.leftInv i x (Composition.length (n := n + 2) (Composition.ones (n + 2))) :
          (a : (i : Fin (Composition.ones (n + 2)).length) → F) → E)
        fun (j : Fin (Composition.length (n := n.succ.succ) (Composition.ones n.succ.succ))) ↦
        (p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ v (Fin.castLE ⋯ j) :
      E)
    ((p.leftInv i x (n + 2) : (a : (i : Fin (n + 2)) → F) → E) fun (j : Fin (n + 2)) ↦
        (p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ v j :
      E)
convert_2 :
  Eq.{u_2 + 1} (α := Composition (n + 2) → E)
    (fun (x_1 : Composition (n + 2)) ↦
      (p.leftInv i x x_1.length : (a : (i : Fin x_1.length) → F) → E)
        (p.applyComposition x_1
          (Function.comp.{1, u_3 + 1, u_2 + 1} (β := F) (⇑(↑i.symm : F →L[𝕜] E) : (a : F) → E) fun (j : Fin (n + 2)) ↦
            (p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ v j)))
    fun (c : Composition (n + 2)) ↦ (p.leftInv i x c.length : (a : (i : Fin c.length) → F) → E) (p.applyComposition c v)
⊢ Eq.{u_2 + 1} (α := E)
    (∑ x_1 ∈ Set.toFinset {x : Composition (n + 2) | x.length < n + 2},
      (p.leftInv i x x_1.length : (a : (i : Fin x_1.length) → F) → E)
        (p.applyComposition x_1
          (Function.comp.{1, u_3 + 1, u_2 + 1} (β := F) (⇑(↑i.symm : F →L[𝕜] E) : (a : F) → E) fun (j : Fin (n + 2)) ↦
            (p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ v j)))
    (∑ c ∈ Set.toFinset {x : Composition (n + 2) | x.length < n + 2},
      (p.leftInv i x c.length : (a : (i : Fin c.length) → F) → E) (p.applyComposition c v))

Tactic:
congr
-- 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
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
h :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F) (p 1)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 E F) :
        (a : E →L[𝕜] F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F)
      (↑i : E →L[𝕜] F))
n_1 n : ℕ
v : (i : Fin (n + 2)) → E
A :
  Eq (α := Finset (Composition (n + 2))) univ
    (Set.toFinset {c : Composition (n + 2) | c.length < n + 2} ∪ {Composition.ones (n + 2)})
B :
  Disjoint (α := Finset (Composition (n + 2))) (Set.toFinset {c : Composition (n + 2) | c.length < n + 2})
    {Composition.ones (n + 2)}
C :
  Eq.{u_2 + 1} (α := E)
    ((p.leftInv i x (Composition.length (n := n + 2) (Composition.ones (n + 2))) :
          (a : (i : Fin (Composition.ones (n + 2)).length) → F) → E)
        fun (j : Fin (Composition.length (n := n.succ.succ) (Composition.ones n.succ.succ))) ↦
        (p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ v (Fin.castLE ⋯ j) :
      E)
    ((p.leftInv i x (n + 2) : (a : (i : Fin (n + 2)) → F) → E) fun (j : Fin (n + 2)) ↦
        (p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ v j :
      E)
convert_2 :
  ∀ (c : Composition (n + 2)),
    Eq.{u_2 + 1} (α := E)
      ((p.leftInv i x c.length : (a : (i : Fin c.length) → F) → E)
          (p.applyComposition c
            (Function.comp.{1, u_3 + 1, u_2 + 1} (β := F) (⇑(↑i.symm : F →L[𝕜] E) : (a : F) → E) fun (j : Fin (n + 2)) ↦
              (p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ v j)) :
        E)
      ((p.leftInv i x c.length : (a : (i : Fin c.length) → F) → E) (p.applyComposition c v) : E)
⊢ Eq.{u_2 + 1} (α := Composition (n + 2) → E)
    (fun (x_1 : Composition (n + 2)) ↦
      (p.leftInv i x x_1.length : (a : (i : Fin x_1.length) → F) → E)
        (p.applyComposition x_1
          (Function.comp.{1, u_3 + 1, u_2 + 1} (β := F) (⇑(↑i.symm : F →L[𝕜] E) : (a : F) → E) fun (j : Fin (n + 2)) ↦
            (p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ v j)))
    fun (c : Composition (n + 2)) ↦ (p.leftInv i x c.length : (a : (i : Fin c.length) → F) → E) (p.applyComposition c v)

Tactic:
ext c
-- 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
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
h :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F) (p 1)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 E F) :
        (a : E →L[𝕜] F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F)
      (↑i : E →L[𝕜] F))
n_1 n : ℕ
v : (i : Fin (n + 2)) → E
A :
  Eq (α := Finset (Composition (n + 2))) univ
    (Set.toFinset {c : Composition (n + 2) | c.length < n + 2} ∪ {Composition.ones (n + 2)})
B :
  Disjoint (α := Finset (Composition (n + 2))) (Set.toFinset {c : Composition (n + 2) | c.length < n + 2})
    {Composition.ones (n + 2)}
C :
  Eq.{u_2 + 1} (α := E)
    ((p.leftInv i x (Composition.length (n := n + 2) (Composition.ones (n + 2))) :
          (a : (i : Fin (Composition.ones (n + 2)).length) → F) → E)
        fun (j : Fin (Composition.length (n := n.succ.succ) (Composition.ones n.succ.succ))) ↦
        (p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ v (Fin.castLE ⋯ j) :
      E)
    ((p.leftInv i x (n + 2) : (a : (i : Fin (n + 2)) → F) → E) fun (j : Fin (n + 2)) ↦
        (p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ v j :
      E)
c : Composition (n + 2)
convert_2 :
  (Function.comp.{1, u_3 + 1, u_2 + 1} (β := F) (⇑(↑i.symm : F →L[𝕜] E) : (a : F) → E) fun (j : Fin (n + 2)) ↦
      (p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ v j) =
    v
⊢ Eq.{u_2 + 1} (α := E)
    ((p.leftInv i x c.length : (a : (i : Fin c.length) → F) → E)
        (p.applyComposition c
          (Function.comp.{1, u_3 + 1, u_2 + 1} (β := F) (⇑(↑i.symm : F →L[𝕜] E) : (a : F) → E) fun (j : Fin (n + 2)) ↦
            (p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ v j)) :
      E)
    ((p.leftInv i x c.length : (a : (i : Fin c.length) → F) → E) (p.applyComposition c v) : E)

Tactic:
congr
-- 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
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
h :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F) (p 1)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 E F) :
        (a : E →L[𝕜] F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F)
      (↑i : E →L[𝕜] F))
n_1 n : ℕ
v : (i : Fin (n + 2)) → E
A :
  Eq (α := Finset (Composition (n + 2))) univ
    (Set.toFinset {c : Composition (n + 2) | c.length < n + 2} ∪ {Composition.ones (n + 2)})
B :
  Disjoint (α := Finset (Composition (n + 2))) (Set.toFinset {c : Composition (n + 2) | c.length < n + 2})
    {Composition.ones (n + 2)}
C :
  Eq.{u_2 + 1} (α := E)
    ((p.leftInv i x (Composition.length (n := n + 2) (Composition.ones (n + 2))) :
          (a : (i : Fin (Composition.ones (n + 2)).length) → F) → E)
        fun (j : Fin (Composition.length (n := n.succ.succ) (Composition.ones n.succ.succ))) ↦
        (p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ v (Fin.castLE ⋯ j) :
      E)
    ((p.leftInv i x (n + 2) : (a : (i : Fin (n + 2)) → F) → E) fun (j : Fin (n + 2)) ↦
        (p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ v j :
      E)
c : Composition (n + 2)
convert_2 :
  ∀ (k : Fin (n + 2)),
    Function.comp.{1, u_3 + 1, u_2 + 1} (β := F) (⇑(↑i.symm : F →L[𝕜] E) : (a : F) → E)
        (fun (j : Fin (n + 2)) ↦ (p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ v j) k =
      v k
⊢ (Function.comp.{1, u_3 + 1, u_2 + 1} (β := F) (⇑(↑i.symm : F →L[𝕜] E) : (a : F) → E) fun (j : Fin (n + 2)) ↦
      (p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ v j) =
    v

Tactic:
ext k
-- 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
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
h :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F) (p 1)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 E F) :
        (a : E →L[𝕜] F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F)
      (↑i : E →L[𝕜] F))
n_1 n : ℕ
v : (i : Fin (n + 2)) → E
A :
  Eq (α := Finset (Composition (n + 2))) univ
    (Set.toFinset {c : Composition (n + 2) | c.length < n + 2} ∪ {Composition.ones (n + 2)})
B :
  Disjoint (α := Finset (Composition (n + 2))) (Set.toFinset {c : Composition (n + 2) | c.length < n + 2})
    {Composition.ones (n + 2)}
C :
  Eq.{u_2 + 1} (α := E)
    ((p.leftInv i x (Composition.length (n := n + 2) (Composition.ones (n + 2))) :
          (a : (i : Fin (Composition.ones (n + 2)).length) → F) → E)
        fun (j : Fin (Composition.length (n := n.succ.succ) (Composition.ones n.succ.succ))) ↦
        (p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ v (Fin.castLE ⋯ j) :
      E)
    ((p.leftInv i x (n + 2) : (a : (i : Fin (n + 2)) → F) → E) fun (j : Fin (n + 2)) ↦
        (p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ v j :
      E)
c : Composition (n + 2)
k : Fin (n + 2)
⊢ Function.comp.{1, u_3 + 1, u_2 + 1} (β := F) (⇑(↑i.symm : F →L[𝕜] E) : (a : F) → E)
      (fun (j : Fin (n + 2)) ↦ (p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ v j) k =
    v k

Tactic:
simp [h]
-- 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
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
h :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F) (p 1)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 E F) :
        (a : E →L[𝕜] F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F)
      (↑i : E →L[𝕜] F))
n_1 n : ℕ
v : (i : Fin (n + 2)) → E
A :
  Eq (α := Finset (Composition (n + 2))) univ
    (Set.toFinset {c : Composition (n + 2) | c.length < n + 2} ∪ {Composition.ones (n + 2)})
B :
  Disjoint (α := Finset (Composition (n + 2))) (Set.toFinset {c : Composition (n + 2) | c.length < n + 2})
    {Composition.ones (n + 2)}
C :
  Eq.{u_2 + 1} (α := E)
    ((p.leftInv i x (Composition.length (n := n + 2) (Composition.ones (n + 2))) :
          (a : (i : Fin (Composition.ones (n + 2)).length) → F) → E)
        fun (j : Fin (Composition.length (n := n.succ.succ) (Composition.ones n.succ.succ))) ↦
        (p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ v (Fin.castLE ⋯ j) :
      E)
    ((p.leftInv i x (n + 2) : (a : (i : Fin (n + 2)) → F) → E) fun (j : Fin (n + 2)) ↦
        (p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ v j :
      E)
⊢ Eq.{u_2 + 1} (α := E)
    ((p.leftInv i x (n + 2) : (a : (i : Fin (n + 2)) → F) → E) fun (j : Fin (n + 2)) ↦
        (p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ v j :
      E)
    (-∑ c ∈ Set.toFinset {c : Composition (n + 2) | c.length < n + 2},
          (p.leftInv i x c.length : (a : (i : Fin c.length) → F) → E) (p.applyComposition c v) :
      E)

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]
-- 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
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
h :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F) (p 1)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 E F) :
        (a : E →L[𝕜] F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F)
      (↑i : E →L[𝕜] F))
n_1 n : ℕ
v : (i : Fin (n + 2)) → E
A :
  Eq (α := Finset (Composition (n + 2))) univ
    (Set.toFinset {c : Composition (n + 2) | c.length < n + 2} ∪ {Composition.ones (n + 2)})
B :
  Disjoint (α := Finset (Composition (n + 2))) (Set.toFinset {c : Composition (n + 2) | c.length < n + 2})
    {Composition.ones (n + 2)}
C :
  Eq.{u_2 + 1} (α := E)
    ((p.leftInv i x (Composition.length (n := n + 2) (Composition.ones (n + 2))) :
          (a : (i : Fin (Composition.ones (n + 2)).length) → F) → E)
        fun (j : Fin (Composition.length (n := n.succ.succ) (Composition.ones n.succ.succ))) ↦
        (p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ v (Fin.castLE ⋯ j) :
      E)
    ((p.leftInv i x (n + 2) : (a : (i : Fin (n + 2)) → F) → E) fun (j : Fin (n + 2)) ↦
        (p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ v j :
      E)
D :
  Eq.{u_2 + 1} (α := E)
    ((p.leftInv i x (n + 2) : (a : (i : Fin (n + 2)) → F) → E) fun (j : Fin (n + 2)) ↦
        (p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ v j :
      E)
    (-∑ c ∈ Set.toFinset {c : Composition (n + 2) | c.length < n + 2},
          (p.leftInv i x c.length : (a : (i : Fin c.length) → F) → E) (p.applyComposition c v) :
      E)
⊢ Eq (α := E) (((p.leftInv i x).comp p (n + 2) : (a : (i : Fin (n + 2)) → E) → E) v : E)
    ((id 𝕜 E x (n + 2) : (a : (i : Fin (n + 2)) → E) → E) v : E)

Tactic:
simp [FormalMultilinearSeries.comp, A, Finset.sum_union B,
      applyComposition_ones, C, D, -Set.toFinset_setOf, -Finset.union_singleton]

Premises used: Finset.sum_union, FormalMultilinearSeries.comp, Finset.union_singleton, Set.toFinset_setOf, FormalMultilinearSeries.applyComposition_ones
-- 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
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
h :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F) (p 1)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 E F) :
        (a : E →L[𝕜] F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F)
      (↑i : E →L[𝕜] F))
n : ℕ
v : (i : Fin n) → E
⊢ Eq (α := E) (((p.leftInv i x).comp p n : (a : (i : Fin n) → E) → E) v : E)
    ((id 𝕜 E x n : (a : (i : Fin n) → E) → E) v : E)

Tactic:
match n with
  | 0 =>
    simp only [comp_coeff_zero', leftInv_coeff_zero, ContinuousMultilinearMap.uncurry0_apply,
      id_apply_zero]
  | 1 =>
    simp only [leftInv_coeff_one, comp_coeff_one, h, id_apply_one, ContinuousLinearEquiv.coe_apply,
      ContinuousLinearEquiv.symm_apply_apply, continuousMultilinearCurryFin1_symm_apply]
  | n + 2 =>
    have A :
      (Finset.univ : Finset (Composition (n + 2))) =
        {c | Composition.length c < n + 2}.toFinset ∪ {Composition.ones (n + 2)} := by
      refine Subset.antisymm (fun c _ => ?_) (subset_univ _)
      by_cases! h : c.length < n + 2
      · simp [h]
      · simp [Composition.eq_ones_iff_le_length.2 h]
    have B :
      Disjoint ({c | Composition.length c < n + 2} : Set (Composition (n + 2))).toFinset
        {Composition.ones (n + 2)} := by
      simp
    have C :
      ((p.leftInv i x (Composition.ones (n + 2)).length)
          fun j : Fin (Composition.ones n.succ.succ).length =>
          p 1 fun _ => v ((Fin.castLE (Composition.length_le _)) j)) =
        p.leftInv i x (n + 2) fun j : Fin (n + 2) => p 1 fun _ => v j := by
      apply FormalMultilinearSeries.congr _ (Composition.ones_length _) fun j hj1 hj2 => ?_
      exact FormalMultilinearSeries.congr _ rfl fun k _ _ => by congr
    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]
    simp [FormalMultilinearSeries.comp, A, Finset.sum_union B,
      applyComposition_ones, C, D, -Set.toFinset_setOf, -Finset.union_singleton]
-- 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
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
h :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F) (p 1)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 E F) :
        (a : E →L[𝕜] F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F)
      (↑i : E →L[𝕜] F))
n : ℕ
v : (i : Fin n) → E
⊢ Eq (α := E) (((p.leftInv i x).comp p n : (a : (i : Fin n) → E) → E) v : E)
    ((id 𝕜 E x n : (a : (i : Fin n) → E) → E) v : E)

Tactic:
classical
  match n with
  | 0 =>
    simp only [comp_coeff_zero', leftInv_coeff_zero, ContinuousMultilinearMap.uncurry0_apply,
      id_apply_zero]
  | 1 =>
    simp only [leftInv_coeff_one, comp_coeff_one, h, id_apply_one, ContinuousLinearEquiv.coe_apply,
      ContinuousLinearEquiv.symm_apply_apply, continuousMultilinearCurryFin1_symm_apply]
  | n + 2 =>
    have A :
      (Finset.univ : Finset (Composition (n + 2))) =
        {c | Composition.length c < n + 2}.toFinset ∪ {Composition.ones (n + 2)} := by
      refine Subset.antisymm (fun c _ => ?_) (subset_univ _)
      by_cases! h : c.length < n + 2
      · simp [h]
      · simp [Composition.eq_ones_iff_le_length.2 h]
    have B :
      Disjoint ({c | Composition.length c < n + 2} : Set (Composition (n + 2))).toFinset
        {Composition.ones (n + 2)} := by
      simp
    have C :
      ((p.leftInv i x (Composition.ones (n + 2)).length)
          fun j : Fin (Composition.ones n.succ.succ).length =>
          p 1 fun _ => v ((Fin.castLE (Composition.length_le _)) j)) =
        p.leftInv i x (n + 2) fun j : Fin (n + 2) => p 1 fun _ => v j := by
      apply FormalMultilinearSeries.congr _ (Composition.ones_length _) fun j hj1 hj2 => ?_
      exact FormalMultilinearSeries.congr _ rfl fun k _ _ => by congr
    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]
    simp [FormalMultilinearSeries.comp, A, Finset.sum_union B,
      applyComposition_ones, C, D, -Set.toFinset_setOf, -Finset.union_singleton]
-- 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
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
rw rw₁ :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin 0) ↦ F) E)
    (ContinuousMultilinearMap.uncurry0 𝕜 F x) (ContinuousMultilinearMap.uncurry0 𝕜 F x)
⊢ p.rightInv i x 0 = ContinuousMultilinearMap.uncurry0 𝕜 F x

Tactic:
rw [rightInv]

Premises used: FormalMultilinearSeries.rightInv
-- 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
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
rw rw₁ :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin 1) ↦ F) E)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 F E) :
          (a : F →L[𝕜] E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ F) E)
        (↑i.symm : F →L[𝕜] E) :
      ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin 1) ↦ F) E)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 F E) :
          (a : F →L[𝕜] E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ F) E)
        (↑i.symm : F →L[𝕜] E) :
      ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin 1) ↦ F) E)
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin 1) ↦ F) E) (p.rightInv i x 1)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 F E) :
        (a : F →L[𝕜] E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ F) E)
      (↑i.symm : F →L[𝕜] E))

Tactic:
rw [rightInv]

Premises used: FormalMultilinearSeries.rightInv
-- 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
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
h : ∀ (n : ℕ), p.removeZero.rightInv i x n = p.rightInv i x n
⊢ p.removeZero.rightInv i x = p.rightInv i x

Tactic:
ext1 n
-- 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
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
n : ℕ
h :
  ∀ (n : ℕ) (IH : ∀ m < n, p.removeZero.rightInv i x m = p.rightInv i x m),
    p.removeZero.rightInv i x n = p.rightInv i x n
⊢ p.removeZero.rightInv i x n = p.rightInv i x n

Tactic:
induction n using Nat.strongRec' with | _ n IH