awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
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_1 n : ℕ
IH : ∀ m < n + 2, p.removeZero.leftInv i x m = p.leftInv i x m
c : { c : Composition (n + 2) // c.length < n + 2 }
cuniv : Membership.mem (γ := Finset { c : Composition (n + 2) // c.length < n + 2 }) univ c
⊢ ContinuousMultilinearMap.compAlongComposition (p.removeZero.compContinuousLinearMap (↑i.symm : F →L[𝕜] E))
      (↑c : Composition (n + 2)) (p.removeZero.leftInv i x (↑c : Composition (n + 2)).length) =
    ContinuousMultilinearMap.compAlongComposition (p.compContinuousLinearMap (↑i.symm : F →L[𝕜] E))
      (↑c : Composition (n + 2)) (p.leftInv i x (↑c : Composition (n + 2)).length)
have rcases : ∀ (c : Composition (n + 2)) (hc : c.length < n + 2)
  (cuniv :
    Membership.mem (γ := Finset { c : Composition (n + 2) // c.length < n + 2 }) univ
      (Subtype.mk (p := fun (c : Composition (n + 2)) ↦ c.length < n + 2) c hc)),
  ContinuousMultilinearMap.compAlongComposition (p.removeZero.compContinuousLinearMap (↑i.symm : F →L[𝕜] E))
      (↑(Subtype.mk (p := fun (c : Composition (n + 2)) ↦ c.length < n + 2) c hc) : Composition (n + 2))
      (p.removeZero.leftInv i x
        (↑(Subtype.mk (p := fun (c : Composition (n + 2)) ↦ c.length < n + 2) c hc) : Composition (n + 2)).length) =
    ContinuousMultilinearMap.compAlongComposition (p.compContinuousLinearMap (↑i.symm : F →L[𝕜] E))
      (↑(Subtype.mk (p := fun (c : Composition (n + 2)) ↦ c.length < n + 2) c hc) : Composition (n + 2))
      (p.leftInv i x
        (↑(Subtype.mk (p := fun (c : Composition (n + 2)) ↦ c.length < n + 2) c hc) : Composition (n + 2)).length)
Tactic: rcases c with ⟨c, hc⟩
Cleared hypotheses: c, cuniv
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
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_1 n : ℕ
IH : ∀ m < n + 2, p.removeZero.leftInv i x m = p.leftInv i x m
c : Composition (n + 2)
hc : c.length < n + 2
cuniv :
  Membership.mem (γ := Finset { c : Composition (n + 2) // c.length < n + 2 }) univ
    (Subtype.mk (p := fun (c : Composition (n + 2)) ↦ c.length < n + 2) c hc)
⊢ ContinuousMultilinearMap.compAlongComposition (p.removeZero.compContinuousLinearMap (↑i.symm : F →L[𝕜] E))
      (↑(Subtype.mk (p := fun (c : Composition (n + 2)) ↦ c.length < n + 2) c hc) : Composition (n + 2))
      (p.removeZero.leftInv i x
        (↑(Subtype.mk (p := fun (c : Composition (n + 2)) ↦ c.length < n + 2) c hc) : Composition (n + 2)).length) =
    ContinuousMultilinearMap.compAlongComposition (p.compContinuousLinearMap (↑i.symm : F →L[𝕜] E))
      (↑(Subtype.mk (p := fun (c : Composition (n + 2)) ↦ c.length < n + 2) c hc) : Composition (n + 2))
      (p.leftInv i x
        (↑(Subtype.mk (p := fun (c : Composition (n + 2)) ↦ c.length < n + 2) c hc) : Composition (n + 2)).length)
have H : ∀ (v : (i : Fin (n + 2)) → F),
  Eq.{u_2 + 1} (α := E)
    ((ContinuousMultilinearMap.compAlongComposition (p.removeZero.compContinuousLinearMap (↑i.symm : F →L[𝕜] E))
            (↑(Subtype.mk (p := fun (c : Composition (n + 2)) ↦ c.length < n + 2) c hc) : Composition (n + 2))
            (p.removeZero.leftInv i x
              (↑(Subtype.mk (p := fun (c : Composition (n + 2)) ↦ c.length < n + 2) c hc) :
                  Composition (n + 2)).length) :
          (a : (i : Fin (n + 2)) → F) → E)
        v :
      E)
    ((ContinuousMultilinearMap.compAlongComposition (p.compContinuousLinearMap (↑i.symm : F →L[𝕜] E))
            (↑(Subtype.mk (p := fun (c : Composition (n + 2)) ↦ c.length < n + 2) c hc) : Composition (n + 2))
            (p.leftInv i x
              (↑(Subtype.mk (p := fun (c : Composition (n + 2)) ↦ c.length < n + 2) c hc) :
                  Composition (n + 2)).length) :
          (a : (i : Fin (n + 2)) → F) → E)
        v :
      E)
Tactic: ext v
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
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))
⊢ Eq (α := FormalMultilinearSeries 𝕜 E E) ((p.leftInv i x).comp p : FormalMultilinearSeries 𝕜 E E)
    (id 𝕜 E x : FormalMultilinearSeries 𝕜 E E)
have h₁ : ∀ (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: ext n v
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
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)})
have 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
Tactic: refine Subset.antisymm (fun c _ => ?_) (subset_univ _)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
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
⊢ Membership.mem (γ := Finset (Composition (n + 2)))
    (Set.toFinset {c : Composition (n + 2) | c.length < n + 2} ∪ {Composition.ones (n + 2)}) c
have 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
Tactic: by_cases! h : c.length < n + 2
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
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
⊢ Membership.mem (γ := Finset (Composition (n + 2)))
    (Set.toFinset {c : Composition (n + 2) | c.length < n + 2} ∪ {Composition.ones (n + 2)}) c
have 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
Tactic: by_cases! h : c.length < n + 2
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (hypothesis)
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 (α := 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)
have A : 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]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (hypothesis)
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)})
⊢ 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)
have B : 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
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
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)
have 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 sorry (⟨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: apply FormalMultilinearSeries.congr _ (Composition.ones_length _) fun j hj1 hj2 => ?_
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (hypothesis)
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 (α := 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)
have 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 sorry 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
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
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)
have 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))
Tactic: simp only [leftInv, ContinuousMultilinearMap.neg_apply, neg_inj,
        ContinuousMultilinearMap.sum_apply]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
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))
have convert_2 : 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: 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
          _
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
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 ∈ 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))
have 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))
Tactic: simp only [compContinuousLinearMap_applyComposition,
        ContinuousMultilinearMap.compAlongComposition_apply]