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 : ℕ
v : (i : Fin 1) → E
⊢ Eq (α := E) (((p.leftInv i x).comp p 1 : (a : (i : Fin 1) → E) → E) v : E)
    ((id 𝕜 E x 1 : (a : (i : Fin 1) → E) → E) v : E)

Tactic:
simp only [leftInv_coeff_one, comp_coeff_one, h, id_apply_one, ContinuousLinearEquiv.coe_apply,
      ContinuousLinearEquiv.symm_apply_apply, continuousMultilinearCurryFin1_symm_apply]

Premises used: FormalMultilinearSeries.comp_coeff_one, FormalMultilinearSeries.leftInv_coeff_one, ContinuousLinearEquiv.coe_apply, ContinuousLinearEquiv.symm_apply_apply, continuousMultilinearCurryFin1_symm_apply, FormalMultilinearSeries.id_apply_one
-- 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
⊢ Eq (α := Finset (Composition (n + 2))) univ
    (Set.toFinset {c : Composition (n + 2) | c.length < n + 2} ∪ {Composition.ones (n + 2)})

Tactic:
Subset.antisymm (fun c _ => ?_) (subset_univ _)

Premises used: Finset.Subset.antisymm, Finset.subset_univ
-- 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
refine :
  ∀ (c : Composition (n + 2)),
    Membership.mem (γ := Finset (Composition (n + 2))) univ c →
      Membership.mem (γ := Finset (Composition (n + 2)))
        (Set.toFinset {c : Composition (n + 2) | c.length < n + 2} ∪ {Composition.ones (n + 2)}) c
⊢ Eq (α := Finset (Composition (n + 2))) univ
    (Set.toFinset {c : Composition (n + 2) | c.length < n + 2} ∪ {Composition.ones (n + 2)})

Tactic:
refine Subset.antisymm (fun c _ => ?_) (subset_univ _)

Premises used: Finset.Subset.antisymm, Finset.subset_univ
-- 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
c : Composition (n + 2)
h_1 : Membership.mem (γ := Finset (Composition (n + 2))) univ c
pos :
  ∀ (h : c.length < n + 2),
    Membership.mem (γ := Finset (Composition (n + 2)))
      (Set.toFinset {c : Composition (n + 2) | c.length < n + 2} ∪ {Composition.ones (n + 2)}) c
neg :
  ∀ (h : n + 2 ≤ c.length),
    Membership.mem (γ := Finset (Composition (n + 2)))
      (Set.toFinset {c : Composition (n + 2) | c.length < n + 2} ∪ {Composition.ones (n + 2)}) c
⊢ Membership.mem (γ := Finset (Composition (n + 2)))
    (Set.toFinset {c : Composition (n + 2) | c.length < n + 2} ∪ {Composition.ones (n + 2)}) c

Tactic:
by_cases! h : c.length < n + 2

Premises used: Composition.length
-- 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_1 :
  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
c : Composition (n + 2)
h_2 : Membership.mem (γ := Finset (Composition (n + 2))) univ c
h : c.length < n + 2
⊢ Membership.mem (γ := Finset (Composition (n + 2)))
    (Set.toFinset {c : Composition (n + 2) | c.length < n + 2} ∪ {Composition.ones (n + 2)}) c

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_1 :
  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
c : Composition (n + 2)
h_2 : Membership.mem (γ := Finset (Composition (n + 2))) univ c
h : n + 2 ≤ c.length
⊢ Membership.mem (γ := Finset (Composition (n + 2)))
    (Set.toFinset {c : Composition (n + 2) | c.length < n + 2} ∪ {Composition.ones (n + 2)}) c

Tactic:
simp [Composition.eq_ones_iff_le_length.2 h]

Premises used: Iff.mpr, Composition.eq_ones_iff_le_length
-- 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
⊢ Eq (α := Finset (Composition (n + 2))) univ
    (Set.toFinset {c : Composition (n + 2) | c.length < n + 2} ∪ {Composition.ones (n + 2)})

Tactic:
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]
-- 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)})
⊢ Disjoint (α := Finset (Composition (n + 2))) (Set.toFinset {c : Composition (n + 2) | c.length < n + 2})
    {Composition.ones (n + 2)}

Tactic:
simp
-- 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)})
⊢ Disjoint (α := Finset (Composition (n + 2))) (Set.toFinset {c : Composition (n + 2) | c.length < n + 2})
    {Composition.ones (n + 2)}

Tactic:
have B :
      Disjoint ({c | Composition.length c < n + 2} : Set (Composition (n + 2))).toFinset
        {Composition.ones (n + 2)} := by
      simp
-- 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)}
apply :
  ∀ (j : ℕ) (hj1 : j < Composition.length (n := n + 2) (Composition.ones (n + 2))) (hj2 : j < n + 2),
    Eq.{u_3 + 1} (α := F)
      ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦
          v (Fin.castLE ⋯ (⟨j, hj1⟩ : Fin (Composition.length (n := n + 2) (Composition.ones (n + 2))))) :
        F)
      ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ v ⟨j, hj2⟩ : F)
⊢ 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)

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

Premises used: FormalMultilinearSeries.congr, Composition.ones_length
-- 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)}
j : ℕ
hj1 : j < Composition.length (n := n + 2) (Composition.ones (n + 2))
hj2 : j < n + 2
k : ℕ
h_1 h_2 : k < 1
⊢ v (Fin.castLE ⋯ (⟨j, hj1⟩ : Fin (Composition.length (n := n + 2) (Composition.ones (n + 2))))) = v ⟨j, hj2⟩

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)}
j : ℕ
hj1 : j < Composition.length (n := n + 2) (Composition.ones (n + 2))
hj2 : j < n + 2
⊢ Eq.{u_3 + 1} (α := F)
    ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦
        v (Fin.castLE ⋯ (⟨j, hj1⟩ : Fin (Composition.length (n := n + 2) (Composition.ones (n + 2))))) :
      F)
    ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ v ⟨j, hj2⟩ : F)

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

Premises used: FormalMultilinearSeries.congr, rfl
-- 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)}
⊢ 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)

Tactic:
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
-- 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)
simp :
  Eq.{u_2 + 1} (α := E)
    (∑ a : { c : Composition (n + 2) // c.length < n + 2 },
      (ContinuousMultilinearMap.compAlongComposition (p.compContinuousLinearMap (↑i.symm : F →L[𝕜] E))
            (↑a : Composition (n + 2)) (p.leftInv i x (↑a : Composition (n + 2)).length) :
          (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)
    (∑ 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))
⊢ 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:
simp only [leftInv, ContinuousMultilinearMap.neg_apply, neg_inj,
        ContinuousMultilinearMap.sum_apply]

Premises used: ContinuousMultilinearMap.neg_apply, ContinuousMultilinearMap.sum_apply, neg_inj, FormalMultilinearSeries.leftInv
-- 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)
    (∑ a : { c : Composition (n + 2) // c.length < n + 2 },
      (ContinuousMultilinearMap.compAlongComposition (p.compContinuousLinearMap (↑i.symm : F →L[𝕜] E))
            (↑a : Composition (n + 2)) (p.leftInv i x (↑a : Composition (n + 2)).length) :
          (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)
    (∑ 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))

Tactic:
(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
          _

Premises used: ContinuousLinearEquiv.symm, Composition.length, ContinuousMultilinearMap.compAlongComposition, FormalMultilinearSeries.compContinuousLinearMap, HAdd.hAdd, Finset.sum_toFinset_eq_subtype, LT.lt, OfNat.ofNat, Eq.symm, DFunLike.coe, FormalMultilinearSeries.leftInv, Eq.trans, ContinuousLinearEquiv.toContinuousLinearMap
-- 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} (α := 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))
⊢ Eq.{u_2 + 1} (α := E)
    (∑ a ∈ Set.toFinset {x : Composition (n + 2) | x.length < n + 2},
      (ContinuousMultilinearMap.compAlongComposition (p.compContinuousLinearMap (↑i.symm : F →L[𝕜] E)) a
            (p.leftInv i x a.length) :
          (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)
    (∑ 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))

Tactic:
simp only [compContinuousLinearMap_applyComposition,
        ContinuousMultilinearMap.compAlongComposition_apply]

Premises used: FormalMultilinearSeries.compContinuousLinearMap_applyComposition, ContinuousMultilinearMap.compAlongComposition_apply