awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
z : F
rw : (p.unshift z).shift.radius (𝕜 := 𝕜) (E := E) (F := E →L[𝕜] F) = p.radius (𝕜 := 𝕜) (E := E) (F := E →L[𝕜] F)
rw₁ rw₂ : p.radius (𝕜 := 𝕜) (E := E) (F := E →L[𝕜] F) = p.radius (𝕜 := 𝕜) (E := E) (F := E →L[𝕜] F)
⊢ (p.unshift z).radius = p.radius (𝕜 := 𝕜) (E := E) (F := E →L[𝕜] F)

Tactic:
rw [← radius_shift, unshift_shift]

Premises used: FormalMultilinearSeries.radius_shift, FormalMultilinearSeries.unshift_shift
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
x : E
hx : Membership.mem (γ := Set E) (Metric.eball 0 p.radius) x
⊢ HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ x) (p.sum x)

Tactic:
(p.summable hx).hasSum

Premises used: Summable.hasSum, FormalMultilinearSeries.summable, FormalMultilinearSeries.sum
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
f : F →L[𝕜] G
⊢ p.radius ≤ radius (f.compFormalMultilinearSeries p)

Tactic:
ENNReal.le_of_forall_nnreal_lt fun r hr => ?_

Premises used: ENNReal.le_of_forall_nnreal_lt
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
f : F →L[𝕜] G
refine : ∀ (r : ℝ≥0) (hr : (↑r : ℝ≥0∞) < p.radius), (↑r : ℝ≥0∞) ≤ radius (f.compFormalMultilinearSeries p)
⊢ p.radius ≤ radius (f.compFormalMultilinearSeries p)

Tactic:
refine ENNReal.le_of_forall_nnreal_lt fun r hr => ?_

Premises used: ENNReal.le_of_forall_nnreal_lt
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
f : F →L[𝕜] G
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < p.radius
h : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖f.compFormalMultilinearSeries p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ 1
⊢ (↑r : ℝ≥0∞) ≤ radius (f.compFormalMultilinearSeries p)

Tactic:
apply le_radius_of_isBigO

Premises used: FormalMultilinearSeries.le_radius_of_isBigO
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
f : F →L[𝕜] G
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < p.radius
apply :
  IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖f.compFormalMultilinearSeries p n‖ * (↑r : ℝ) ^ n) fun (n : ℕ) ↦
    ‖p n‖ * (↑r : ℝ) ^ n
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖f.compFormalMultilinearSeries p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ 1

Tactic:
apply (IsBigO.trans_isLittleO _ (p.isLittleO_one_of_lt_radius hr)).isBigO

Premises used: FormalMultilinearSeries.isLittleO_one_of_lt_radius, Asymptotics.IsLittleO.isBigO, Asymptotics.IsBigO.trans_isLittleO
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
f : F →L[𝕜] G
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < p.radius
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖f.compFormalMultilinearSeries p n‖ * (↑r : ℝ) ^ n) fun (n : ℕ) ↦
    ‖p n‖ * (↑r : ℝ) ^ n

Tactic:
IsBigO.mul (@IsBigOWith.isBigO _ _ _ _ _ ‖f‖ _ _ _ ?_) (isBigO_refl _ _)

Premises used: Asymptotics.IsBigO.mul, Asymptotics.IsBigOWith.isBigO, Asymptotics.isBigO_refl
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
f : F →L[𝕜] G
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < p.radius
refine : IsBigOWith (E := ℝ) (F := ℝ) ‖f‖ atTop (fun (n : ℕ) ↦ ‖f.compFormalMultilinearSeries p n‖) fun (n : ℕ) ↦ ‖p n‖
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖f.compFormalMultilinearSeries p n‖ * (↑r : ℝ) ^ n) fun (n : ℕ) ↦
    ‖p n‖ * (↑r : ℝ) ^ n

Tactic:
refine IsBigO.mul (@IsBigOWith.isBigO _ _ _ _ _ ‖f‖ _ _ _ ?_) (isBigO_refl _ _)

Premises used: Asymptotics.IsBigO.mul, Asymptotics.IsBigOWith.isBigO
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
f : F →L[𝕜] G
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < p.radius
⊢ IsBigOWith (E := ℝ) (F := ℝ) ‖f‖ atTop (fun (n : ℕ) ↦ ‖f.compFormalMultilinearSeries p n‖) fun (n : ℕ) ↦ ‖p n‖

Tactic:
IsBigOWith.of_bound (Eventually.of_forall fun n => ?_)

Premises used: Filter.Eventually.of_forall, Asymptotics.IsBigOWith.of_bound
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
f : F →L[𝕜] G
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < p.radius
refine : ∀ (n : ℕ), ‖‖f.compFormalMultilinearSeries p n‖‖ ≤ ‖f‖ * ‖‖p n‖‖
⊢ IsBigOWith (E := ℝ) (F := ℝ) ‖f‖ atTop (fun (n : ℕ) ↦ ‖f.compFormalMultilinearSeries p n‖) fun (n : ℕ) ↦ ‖p n‖

Tactic:
refine IsBigOWith.of_bound (Eventually.of_forall fun n => ?_)

Premises used: Filter.Eventually.of_forall, Asymptotics.IsBigOWith.of_bound
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
f : F →L[𝕜] G
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < p.radius
n : ℕ
⊢ ‖‖f.compFormalMultilinearSeries p n‖‖ ≤ ‖f‖ * ‖‖p n‖‖

Tactic:
simpa only [norm_norm] using f.norm_compContinuousMultilinearMap_le (p n)

Premises used: ContinuousLinearMap.norm_compContinuousMultilinearMap_le, norm_norm
-- 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.leftInv i x 0 = ContinuousMultilinearMap.uncurry0 𝕜 F x

Tactic:
rw [leftInv]

Premises used: 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
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.leftInv 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 [leftInv]

Premises used: 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 : ∀ (n : ℕ), p.removeZero.leftInv i x n = p.leftInv i x n
⊢ p.removeZero.leftInv i x = p.leftInv 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.leftInv i x m = p.leftInv i x m), p.removeZero.leftInv i x n = p.leftInv i x n
⊢ p.removeZero.leftInv i x n = p.leftInv i x n

Tactic:
induction n using Nat.strongRec' with | _ n IH
-- 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 : ℕ
IH : ∀ m < 0, p.removeZero.leftInv i x m = p.leftInv i x m
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin 0) ↦ F) E) (p.removeZero.leftInv i x 0)
    (p.leftInv i x 0)

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
n : ℕ
IH : ∀ m < 1, p.removeZero.leftInv i x m = p.leftInv i x m
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin 1) ↦ F) E) (p.removeZero.leftInv i x 1)
    (p.leftInv i x 1)

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
n_1 n : ℕ
IH : ∀ m < n + 2, p.removeZero.leftInv i x m = p.leftInv i x m
simp :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin (n + 2)) ↦ F) E)
    (∑ c : { c : Composition (n + 2) // c.length < n + 2 },
      ContinuousMultilinearMap.compAlongComposition (p.removeZero.compContinuousLinearMap (↑i.symm : F →L[𝕜] E))
        (↑c : Composition (n + 2)) (p.removeZero.leftInv i x (↑c : Composition (n + 2)).length))
    (∑ c : { c : Composition (n + 2) // c.length < n + 2 },
      ContinuousMultilinearMap.compAlongComposition (p.compContinuousLinearMap (↑i.symm : F →L[𝕜] E))
        (↑c : Composition (n + 2)) (p.leftInv i x (↑c : Composition (n + 2)).length))
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin (n + 2)) ↦ F) E)
    (p.removeZero.leftInv i x (n + 2)) (p.leftInv i x (n + 2))

Tactic:
simp only [leftInv, neg_inj]

Premises used: 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
n_1 n : ℕ
IH : ∀ m < n + 2, p.removeZero.leftInv i x m = p.leftInv i x m
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin (n + 2)) ↦ F) E)
    (∑ c : { c : Composition (n + 2) // c.length < n + 2 },
      ContinuousMultilinearMap.compAlongComposition (p.removeZero.compContinuousLinearMap (↑i.symm : F →L[𝕜] E))
        (↑c : Composition (n + 2)) (p.removeZero.leftInv i x (↑c : Composition (n + 2)).length))
    (∑ c : { c : Composition (n + 2) // c.length < n + 2 },
      ContinuousMultilinearMap.compAlongComposition (p.compContinuousLinearMap (↑i.symm : F →L[𝕜] E))
        (↑c : Composition (n + 2)) (p.leftInv i x (↑c : Composition (n + 2)).length))

Tactic:
Finset.sum_congr rfl fun c cuniv => ?_

Premises used: Finset.sum_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
n_1 n : ℕ
IH : ∀ m < n + 2, p.removeZero.leftInv i x m = p.leftInv i x m
refine :
  ∀ (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)
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin (n + 2)) ↦ F) E)
    (∑ c : { c : Composition (n + 2) // c.length < n + 2 },
      ContinuousMultilinearMap.compAlongComposition (p.removeZero.compContinuousLinearMap (↑i.symm : F →L[𝕜] E))
        (↑c : Composition (n + 2)) (p.removeZero.leftInv i x (↑c : Composition (n + 2)).length))
    (∑ c : { c : Composition (n + 2) // c.length < n + 2 },
      ContinuousMultilinearMap.compAlongComposition (p.compContinuousLinearMap (↑i.symm : F →L[𝕜] E))
        (↑c : Composition (n + 2)) (p.leftInv i x (↑c : Composition (n + 2)).length))

Tactic:
refine Finset.sum_congr rfl fun c cuniv => ?_

Premises used: Finset.sum_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
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
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)
⊢ 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)

Tactic:
rcases c with ⟨c, hc⟩
-- 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_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)
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)
⊢ 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:
ext v
-- 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_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)
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:
simp [IH _ hc]
-- 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 : ℕ
IH : ∀ m < n, p.removeZero.leftInv i x m = p.leftInv i x m
⊢ p.removeZero.leftInv i x n = p.leftInv i x n

Tactic:
match n with
  | 0 => simp -- if one replaces `simp` with `refl`, the proof times out in the kernel.
  | 1 => simp -- TODO: why?
  | n + 2 =>
    simp only [leftInv, neg_inj]
    refine Finset.sum_congr rfl fun c cuniv => ?_
    rcases c with ⟨c, hc⟩
    ext v
    simp [IH _ hc]
-- 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))
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)
⊢ Eq (α := FormalMultilinearSeries 𝕜 E E) ((p.leftInv i x).comp p : FormalMultilinearSeries 𝕜 E E)
    (id 𝕜 E x : FormalMultilinearSeries 𝕜 E E)

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

Tactic:
simp only [comp_coeff_zero', leftInv_coeff_zero, ContinuousMultilinearMap.uncurry0_apply,
      id_apply_zero]

Premises used: FormalMultilinearSeries.comp_coeff_zero', FormalMultilinearSeries.id_apply_zero, FormalMultilinearSeries.leftInv_coeff_zero, ContinuousMultilinearMap.uncurry0_apply