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
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)
    (∑ 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))
have 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)
Tactic: 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} (α := 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)
have 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)
Tactic: ext c
-- 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)
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)
have 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
Tactic: 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)
c : Composition (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) =
    v
have 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
Tactic: ext k
-- 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)}
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 (α := 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 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)
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]
-- 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
⊢ p.rightInv i x 0 = ContinuousMultilinearMap.uncurry0 𝕜 F x
have rw : Eq (α := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin 0) ↦ F) E)
  (ContinuousMultilinearMap.uncurry0 𝕜 F x) (ContinuousMultilinearMap.uncurry0 𝕜 F x)
Tactic: rw [rightInv]
-- 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
⊢ 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))
have 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)
Tactic: rw [rightInv]
-- 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
⊢ p.removeZero.rightInv i x = p.rightInv i x
have h : ∀ (n : ℕ), p.removeZero.rightInv i x n = p.rightInv i x n
Tactic: ext1 n
-- 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 : ℕ
⊢ p.removeZero.rightInv i x n = p.rightInv i x n
have 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
Tactic: induction n using Nat.strongRec' with | _ n IH
Cleared hypotheses: n
-- 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.rightInv i x m = p.rightInv i x m
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin (n + 2)) ↦ F) E)
    (p.removeZero.rightInv i x (n + 2)) (p.rightInv i x (n + 2))
have simp : Eq (α := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin (n + 2)) ↦ F) E)
  ((↑i.symm : F →L[𝕜] E).compContinuousMultilinearMap (M₁ := fun (i : Fin (n + 2)) ↦ F)
    (p.removeZero.comp (fun (k : ℕ) ↦ if k < n + 2 then p.removeZero.rightInv i x k else 0) (n + 2)))
  ((↑i.symm : F →L[𝕜] E).compContinuousMultilinearMap (M₁ := fun (i : Fin (n + 2)) ↦ F)
    (p.comp (fun (k : ℕ) ↦ if k < n + 2 then p.rightInv i x k else 0) (n + 2)))
Tactic: simp only [rightInv, neg_inj]
-- 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.rightInv i x m = p.rightInv i x m
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin (n + 2)) ↦ F) E)
    ((↑i.symm : F →L[𝕜] E).compContinuousMultilinearMap (M₁ := fun (i : Fin (n + 2)) ↦ F)
      (p.removeZero.comp (fun (k : ℕ) ↦ if k < n + 2 then p.removeZero.rightInv i x k else 0) (n + 2)))
    ((↑i.symm : F →L[𝕜] E).compContinuousMultilinearMap (M₁ := fun (i : Fin (n + 2)) ↦ F)
      (p.comp (fun (k : ℕ) ↦ if k < n + 2 then p.rightInv i x k else 0) (n + 2)))
have rw : Eq (α := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin (n + 2)) ↦ F) E)
  ((↑i.symm : F →L[𝕜] E).compContinuousMultilinearMap (M₁ := fun (i : Fin (n + 2)) ↦ F)
    (p.comp (fun (k : ℕ) ↦ if k < n + 2 then p.removeZero.rightInv i x k else 0) (n + 2)))
  ((↑i.symm : F →L[𝕜] E).compContinuousMultilinearMap (M₁ := fun (i : Fin (n + 2)) ↦ F)
    (p.comp (fun (k : ℕ) ↦ if k < n + 2 then p.rightInv i x k else 0) (n + 2)))
Tactic: rw [removeZero_comp_of_pos _ _ (add_pos_of_nonneg_of_pos n.zero_le zero_lt_two)]
-- 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.rightInv i x m = p.rightInv i x m
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin (n + 2)) ↦ F) E)
    ((↑i.symm : F →L[𝕜] E).compContinuousMultilinearMap (M₁ := fun (i : Fin (n + 2)) ↦ F)
      (p.comp (fun (k : ℕ) ↦ if k < n + 2 then p.removeZero.rightInv i x k else 0) (n + 2)))
    ((↑i.symm : F →L[𝕜] E).compContinuousMultilinearMap (M₁ := fun (i : Fin (n + 2)) ↦ F)
      (p.comp (fun (k : ℕ) ↦ if k < n + 2 then p.rightInv i x k else 0) (n + 2)))
have e_f : ∀ (k : ℕ) (x_1 : (i : Fin k) → F),
  Eq.{u_2 + 1} (α := E) ((if k < n + 2 then p.removeZero.rightInv i x k else 0 : (a : (i : Fin k) → F) → E) x_1 : E)
    ((if k < n + 2 then p.rightInv i x k else 0 : (a : (i : Fin k) → F) → E) x_1 : E)
Tactic: congr (config := { closePost := false }) 2 with k
-- 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.rightInv i x m = p.rightInv i x m
k : ℕ
x_1 : (i : Fin k) → F
⊢ Eq.{u_2 + 1} (α := E) ((if k < n + 2 then p.removeZero.rightInv i x k else 0 : (a : (i : Fin k) → F) → E) x_1 : E)
    ((if k < n + 2 then p.rightInv i x k else 0 : (a : (i : Fin k) → F) → E) x_1 : E)
have pos : ∀ (hk : k < n + 2),
  Eq.{u_2 + 1} (α := E) ((if k < n + 2 then p.removeZero.rightInv i x k else 0 : (a : (i : Fin k) → F) → E) x_1 : E)
    ((if k < n + 2 then p.rightInv i x k else 0 : (a : (i : Fin k) → F) → E) x_1 : E)
Tactic: by_cases hk : k < 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
n_1 n : ℕ
IH : ∀ m < n + 2, p.removeZero.rightInv i x m = p.rightInv i x m
k : ℕ
x_1 : (i : Fin k) → F
pos :
  ∀ (hk : k < n + 2),
    Eq.{u_2 + 1} (α := E) ((if k < n + 2 then p.removeZero.rightInv i x k else 0 : (a : (i : Fin k) → F) → E) x_1 : E)
      ((if k < n + 2 then p.rightInv i x k else 0 : (a : (i : Fin k) → F) → E) x_1 : E)
⊢ Eq.{u_2 + 1} (α := E) ((if k < n + 2 then p.removeZero.rightInv i x k else 0 : (a : (i : Fin k) → F) → E) x_1 : E)
    ((if k < n + 2 then p.rightInv i x k else 0 : (a : (i : Fin k) → F) → E) x_1 : E)
have neg : ∀ (hk : ¬k < n + 2),
  Eq.{u_2 + 1} (α := E) ((if k < n + 2 then p.removeZero.rightInv i x k else 0 : (a : (i : Fin k) → F) → E) x_1 : E)
    ((if k < n + 2 then p.rightInv i x k else 0 : (a : (i : Fin k) → F) → E) x_1 : E)
Tactic: by_cases hk : k < 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
n : ℕ
hn : 0 < n
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 F E
v : Fin n → F
⊢ Eq (α := Finset (Composition n)) univ (Set.toFinset {c : Composition n | 1 < c.length} ∪ {Composition.single n hn})
have refine : ∀ (c : Composition n),
  Membership.mem (γ := Finset (Composition n)) univ c →
    Membership.mem (γ := Finset (Composition n))
      (Set.toFinset {c : Composition n | 1 < c.length} ∪ {Composition.single n hn}) 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
n : ℕ
hn : 0 < n
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 F E
v : Fin n → F
c : Composition n
h : Membership.mem (γ := Finset (Composition n)) univ c
⊢ Membership.mem (γ := Finset (Composition n))
    (Set.toFinset {c : Composition n | 1 < c.length} ∪ {Composition.single n hn}) c
have pos : ∀ (h : 1 < c.length),
  Membership.mem (γ := Finset (Composition n))
    (Set.toFinset {c : Composition n | 1 < c.length} ∪ {Composition.single n hn}) c
Tactic: by_cases h : 1 < c.length
-- 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
n : ℕ
hn : 0 < n
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 F E
v : Fin n → F
c : Composition n
h : Membership.mem (γ := Finset (Composition n)) univ c
pos :
  ∀ (h : 1 < c.length),
    Membership.mem (γ := Finset (Composition n))
      (Set.toFinset {c : Composition n | 1 < c.length} ∪ {Composition.single n hn}) c
⊢ Membership.mem (γ := Finset (Composition n))
    (Set.toFinset {c : Composition n | 1 < c.length} ∪ {Composition.single n hn}) c
have neg : ∀ (h : ¬1 < c.length),
  Membership.mem (γ := Finset (Composition n))
    (Set.toFinset {c : Composition n | 1 < c.length} ∪ {Composition.single n hn}) c
Tactic: by_cases h : 1 < c.length
-- 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
n : ℕ
hn : 0 < n
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 F E
v : Fin n → F
c : Composition n
h_1 : Membership.mem (γ := Finset (Composition n)) univ c
h : ¬1 < c.length
⊢ c.length = 1
have refine : 1 ≤ c.length
Tactic: refine (eq_iff_le_not_lt.2 ⟨?_, h⟩).symm
-- 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
n : ℕ
hn : 0 < n
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 F E
v : Fin n → F
c : Composition n
h_1 : Membership.mem (γ := Finset (Composition n)) univ c
h : ¬1 < c.length
⊢ Membership.mem (γ := Finset (Composition n))
    (Set.toFinset {c : Composition n | 1 < c.length} ∪ {Composition.single n hn}) c
have this : c.length = 1
Tactic: have : c.length = 1 := by
        refine (eq_iff_le_not_lt.2 ⟨?_, h⟩).symm; exact c.length_pos_of_pos hn
-- 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
n : ℕ
hn : 0 < n
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 F E
v : Fin n → F
c : Composition n
h_1 : Membership.mem (γ := Finset (Composition n)) univ c
h : ¬1 < c.length
this : c.length = 1
⊢ Membership.mem (γ := Finset (Composition n))
    (Set.toFinset {c : Composition n | 1 < c.length} ∪ {Composition.single n hn}) c
have this₁ : c = Composition.single n hn
Tactic: rw [← Composition.eq_single_iff_length hn] at this
Cleared hypotheses: this