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
n : ℕ
v : Fin (n + 2) → F
N : 0 < n + 2
refine :
  ∀ (c : Composition (n + 2))
    (hc : Membership.mem (γ := Finset (Composition (n + 2))) (Set.toFinset {c : Composition (n + 2) | 1 < c.length}) c)
    (j : ℕ) (hj1 hj2 : j < c.length),
    applyComposition.{u_1, u_3, u_2} (𝕜 := 𝕜) (fun (k : ℕ) ↦ if k < n + 2 then p.rightInv i x k else 0) c v ⟨j, hj1⟩ =
      (p.rightInv i x).applyComposition c v (⟨j, hj2⟩ : Fin c.length)
⊢ Eq.{u_3 + 1} (α := F)
    (∑ c ∈ Set.toFinset {c : Composition (n + 2) | 1 < c.length},
      (p c.length : (a : (i : Fin c.length) → E) → F)
        (applyComposition.{u_1, u_3, u_2} (𝕜 := 𝕜) (fun (k : ℕ) ↦ if k < n + 2 then p.rightInv i x k else 0) c v))
    (∑ c ∈ Set.toFinset {c : Composition (n + 2) | 1 < c.length},
      (p c.length : (a : (i : Fin c.length) → E) → F) ((p.rightInv i x).applyComposition c v))

Tactic:
refine sum_congr rfl fun c hc => p.congr rfl fun j hj1 hj2 => ?_

Premises used: FormalMultilinearSeries.congr, 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 : ℕ
v : Fin (n + 2) → F
N : 0 < n + 2
c : Composition (n + 2)
hc : Membership.mem (γ := Finset (Composition (n + 2))) (Set.toFinset {c : Composition (n + 2) | 1 < c.length}) c
j : ℕ
hj1 hj2 : j < c.length
⊢ 1 < c.length

Tactic:
simp only [Set.mem_toFinset (s := {c : Composition (n + 2) | 1 < c.length}),
      Set.mem_setOf_eq] at hc

Premises used: Set.mem_setOf_eq, Set.mem_toFinset
-- 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 : ℕ
v : Fin (n + 2) → F
N : 0 < n + 2
c : Composition (n + 2)
j : ℕ
hj1 hj2 : j < c.length
hc : 1 < c.length
⊢ ∀ (k : Fin c.length), c.blocksFun k < n + 2

Tactic:
simp [← Composition.ne_single_iff N, Composition.eq_single_iff_length, ne_of_gt hc]

Premises used: ne_of_gt, Composition.ne_single_iff, Composition.eq_single_iff_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
n : ℕ
v : Fin (n + 2) → F
N : 0 < n + 2
c : Composition (n + 2)
hc : Membership.mem (γ := Finset (Composition (n + 2))) (Set.toFinset {c : Composition (n + 2) | 1 < c.length}) c
j : ℕ
hj1 hj2 : j < c.length
⊢ ∀ (k : Fin c.length), c.blocksFun k < n + 2

Tactic:
have : ∀ k, c.blocksFun k < n + 2 := by
    simp only [Set.mem_toFinset (s := {c : Composition (n + 2) | 1 < c.length}),
      Set.mem_setOf_eq] at hc
    simp [← Composition.ne_single_iff N, Composition.eq_single_iff_length, ne_of_gt 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 : ℕ
v : Fin (n + 2) → F
N : 0 < n + 2
c : Composition (n + 2)
hc : Membership.mem (γ := Finset (Composition (n + 2))) (Set.toFinset {c : Composition (n + 2) | 1 < c.length}) c
j : ℕ
hj1 hj2 : j < c.length
this : ∀ (k : Fin c.length), c.blocksFun k < n + 2
⊢ applyComposition.{u_1, u_3, u_2} (𝕜 := 𝕜) (fun (k : ℕ) ↦ if k < n + 2 then p.rightInv i x k else 0) c v ⟨j, hj1⟩ =
    (p.rightInv i x).applyComposition c v (⟨j, hj2⟩ : Fin c.length)

Tactic:
simp [applyComposition, this]

Premises used: FormalMultilinearSeries.applyComposition
-- 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) → F),
    Eq (α := F) ((p.comp (p.rightInv i x) n : (a : (i : Fin n) → F) → F) v : F)
      ((id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) 0) n : (a : (i : Fin n) → F) → F) v : F)
⊢ Eq (α := FormalMultilinearSeries 𝕜 F F) (p.comp (p.rightInv i x) : FormalMultilinearSeries 𝕜 F F)
    (id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) 0) : FormalMultilinearSeries 𝕜 F F)

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) → F
simp :
  Eq.{u_3 + 1} (α := F) ((p 0 : (a : (i : Fin 0) → E) → F) fun (_i : Fin 0) ↦ 0 : F)
    ((p 0 : (a : (i : Fin 0) → E) → F) ![] : F)
⊢ Eq (α := F) ((p.comp (p.rightInv i x) 0 : (a : (i : Fin 0) → F) → F) v : F)
    ((id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) 0) 0 : (a : (i : Fin 0) → F) → F) v : F)

Tactic:
simp only [comp_coeff_zero', Matrix.zero_empty, id_apply_zero]

Premises used: FormalMultilinearSeries.comp_coeff_zero', FormalMultilinearSeries.id_apply_zero, Matrix.zero_empty
-- 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) → F
h₁ : Eq.{u_2 + 1} (α := (i : Fin 0) → E) (fun (_i : Fin 0) ↦ 0) ![]
⊢ Eq.{u_3 + 1} (α := F) ((p 0 : (a : (i : Fin 0) → E) → F) fun (_i : Fin 0) ↦ 0 : F)
    ((p 0 : (a : (i : Fin 0) → E) → F) ![] : F)

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 : ℕ
v : (i : Fin 0) → F
h₁ : ∀ (i : Fin 0), Eq.{u_2 + 1} (α := E) 0 (![] i)
⊢ Eq.{u_2 + 1} (α := (i : Fin 0) → E) (fun (_i : Fin 0) ↦ 0) ![]

Tactic:
ext i
-- 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_1 : 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_1 : E →L[𝕜] F))
n : ℕ
v : (i : Fin 0) → F
i : Fin 0
⊢ Eq.{u_2 + 1} (α := E) 0 (![] i)

Tactic:
i.elim0

Premises used: Fin.elim0
-- 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_1 : 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_1 : E →L[𝕜] F))
n : ℕ
v : (i : Fin 0) → F
i : Fin 0
⊢ Eq.{u_2 + 1} (α := E) 0 (![] i)

Tactic:
exact i.elim0

Premises used: Fin.elim0
-- 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) → F
⊢ Eq (α := F) ((p.comp (p.rightInv i x) 1 : (a : (i : Fin 1) → F) → F) v : F)
    ((id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) 0) 1 : (a : (i : Fin 1) → F) → F) v : F)

Tactic:
simp only [comp_coeff_one, h, rightInv_coeff_one, ContinuousLinearEquiv.apply_symm_apply,
      id_apply_one, ContinuousLinearEquiv.coe_apply, continuousMultilinearCurryFin1_symm_apply]

Premises used: ContinuousLinearEquiv.apply_symm_apply, FormalMultilinearSeries.comp_coeff_one, ContinuousLinearEquiv.coe_apply, continuousMultilinearCurryFin1_symm_apply, FormalMultilinearSeries.id_apply_one, FormalMultilinearSeries.rightInv_coeff_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)) → F
⊢ 0 < 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)) → F
⊢ 0 < n + 2

Tactic:
have N : 0 < 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)) → F
N : 0 < n + 2
⊢ Eq (α := F) ((p.comp (p.rightInv i x) (n + 2) : (a : (i : Fin (n + 2)) → F) → F) v : F)
    ((id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) 0) (n + 2) : (a : (i : Fin (n + 2)) → F) → F) v : F)

Tactic:
simp [comp_rightInv_aux1 N, h, rightInv, comp_rightInv_aux2, -Set.toFinset_setOf]

Premises used: FormalMultilinearSeries.comp_rightInv_aux1, FormalMultilinearSeries.rightInv, FormalMultilinearSeries.comp_rightInv_aux2, Set.toFinset_setOf
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
h :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F) (p 1)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 E F) :
        (a : E →L[𝕜] F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F)
      (↑i : E →L[𝕜] F))
n : ℕ
v : (i : Fin n) → F
⊢ Eq (α := F) ((p.comp (p.rightInv i x) n : (a : (i : Fin n) → F) → F) v : F)
    ((id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) 0) n : (a : (i : Fin n) → F) → F) v : F)

Tactic:
match n with
  | 0 =>
    simp only [comp_coeff_zero', Matrix.zero_empty, id_apply_zero]
    congr
    ext i
    exact i.elim0
  | 1 =>
    simp only [comp_coeff_one, h, rightInv_coeff_one, ContinuousLinearEquiv.apply_symm_apply,
      id_apply_one, ContinuousLinearEquiv.coe_apply, continuousMultilinearCurryFin1_symm_apply]
  | n + 2 =>
    have N : 0 < n + 2 := by simp
    simp [comp_rightInv_aux1 N, h, rightInv, comp_rightInv_aux2, -Set.toFinset_setOf]
-- 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 : ℕ
hn : LE.le (α := ℕ) 2 0
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin 0) ↦ F) E) (p.rightInv i x 0)
    (-(↑i.symm : F →L[𝕜] E).compContinuousMultilinearMap (M₁ := fun (i : Fin 0) ↦ F)
        (∑ c ∈ Set.toFinset {c : Composition 0 | 1 < c.length}, p.compAlongComposition (p.rightInv i x) c))

Tactic:
False.elim (zero_lt_two.not_ge hn)

Premises used: False.elim, LT.lt.not_ge, zero_lt_two
-- 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 : ℕ
hn : LE.le (α := ℕ) 2 0
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin 0) ↦ F) E) (p.rightInv i x 0)
    (-(↑i.symm : F →L[𝕜] E).compContinuousMultilinearMap (M₁ := fun (i : Fin 0) ↦ F)
        (∑ c ∈ Set.toFinset {c : Composition 0 | 1 < c.length}, p.compAlongComposition (p.rightInv i x) c))

Tactic:
exact False.elim (zero_lt_two.not_ge hn)

Premises used: False.elim, LT.lt.not_ge, zero_lt_two
-- 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 : ℕ
hn : LE.le (α := ℕ) 2 1
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin 1) ↦ F) E) (p.rightInv i x 1)
    (-(↑i.symm : F →L[𝕜] E).compContinuousMultilinearMap (M₁ := fun (i : Fin 1) ↦ F)
        (∑ c ∈ Set.toFinset {c : Composition 1 | 1 < c.length}, p.compAlongComposition (p.rightInv i x) c))

Tactic:
False.elim (one_lt_two.not_ge hn)

Premises used: False.elim, one_lt_two, LT.lt.not_ge
-- 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 : ℕ
hn : LE.le (α := ℕ) 2 1
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin 1) ↦ F) E) (p.rightInv i x 1)
    (-(↑i.symm : F →L[𝕜] E).compContinuousMultilinearMap (M₁ := fun (i : Fin 1) ↦ F)
        (∑ c ∈ Set.toFinset {c : Composition 1 | 1 < c.length}, p.compAlongComposition (p.rightInv i x) c))

Tactic:
exact False.elim (one_lt_two.not_ge hn)

Premises used: False.elim, one_lt_two, LT.lt.not_ge
-- 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 : ℕ
hn : 2 ≤ n + 2
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.comp (fun (k : ℕ) ↦ if k < n + 2 then p.rightInv i x k else 0) (n + 2)))
    ((↑i.symm : F →L[𝕜] E).compContinuousMultilinearMap (M₁ := fun (i : Fin (n + 2)) ↦ F)
      (∑ c ∈ Set.toFinset {c : Composition (n + 2) | 1 < c.length}, p.compAlongComposition (p.rightInv i x) c))
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin (n + 2)) ↦ F) E) (p.rightInv i x (n + 2))
    (-(↑i.symm : F →L[𝕜] E).compContinuousMultilinearMap (M₁ := fun (i : Fin (n + 2)) ↦ F)
        (∑ c ∈ Set.toFinset {c : Composition (n + 2) | 1 < c.length}, p.compAlongComposition (p.rightInv i x) c))

Tactic:
simp only [rightInv, neg_inj]

Premises used: neg_inj, FormalMultilinearSeries.rightInv
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
n_1 n : ℕ
hn : 2 ≤ n + 2
e_f :
  Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n + 2)) ↦ F) F)
    (p.comp (fun (k : ℕ) ↦ if k < n + 2 then p.rightInv i x k else 0) (n + 2))
    (∑ c ∈ Set.toFinset {c : Composition (n + 2) | 1 < c.length}, p.compAlongComposition (p.rightInv i x) c)
⊢ 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.rightInv i x k else 0) (n + 2)))
    ((↑i.symm : F →L[𝕜] E).compContinuousMultilinearMap (M₁ := fun (i : Fin (n + 2)) ↦ F)
      (∑ c ∈ Set.toFinset {c : Composition (n + 2) | 1 < c.length}, p.compAlongComposition (p.rightInv i x) c))

Tactic:
congr (config := { closePost := false }) 1
-- 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 : ℕ
hn : 2 ≤ n + 2
e_f :
  ∀ (v : (i : Fin (n + 2)) → F),
    Eq (α := F)
      ((p.comp (fun (k : ℕ) ↦ if k < n + 2 then p.rightInv i x k else 0) (n + 2) : (a : (i : Fin (n + 2)) → F) → F) v :
        F)
      ((∑ c ∈ Set.toFinset {c : Composition (n + 2) | 1 < c.length}, p.compAlongComposition (p.rightInv i x) c :
            (a : (i : Fin (n + 2)) → F) → F)
          v :
        F)
⊢ Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n + 2)) ↦ F) F)
    (p.comp (fun (k : ℕ) ↦ if k < n + 2 then p.rightInv i x k else 0) (n + 2))
    (∑ c ∈ Set.toFinset {c : Composition (n + 2) | 1 < c.length}, p.compAlongComposition (p.rightInv i x) c)

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 : ℕ
hn : 2 ≤ n + 2
v : (i : Fin (n + 2)) → F
⊢ 0 < 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
n_1 n : ℕ
hn : 2 ≤ n + 2
v : (i : Fin (n + 2)) → F
⊢ 0 < n + 2

Tactic:
have N : 0 < 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
n_1 n : ℕ
hn : 2 ≤ n + 2
v : (i : Fin (n + 2)) → F
N : 0 < n + 2
⊢ Eq.{u_3 + 1} (α := F) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ 0 : F) (0 : F)

Tactic:
have : ((p 1) fun _ : Fin 1 => 0) = 0 := ContinuousMultilinearMap.map_zero _
-- 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 : ℕ
hn : 2 ≤ n + 2
v : (i : Fin (n + 2)) → F
N : 0 < n + 2
this : Eq.{u_3 + 1} (α := F) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ 0 : F) (0 : F)
⊢ Eq (α := F)
    ((p.comp (fun (k : ℕ) ↦ if k < n + 2 then p.rightInv i x k else 0) (n + 2) : (a : (i : Fin (n + 2)) → F) → F) v : F)
    ((∑ c ∈ Set.toFinset {c : Composition (n + 2) | 1 < c.length}, p.compAlongComposition (p.rightInv i x) c :
          (a : (i : Fin (n + 2)) → F) → F)
        v :
      F)

Tactic:
simp [comp_rightInv_aux1 N, this, comp_rightInv_aux2, -Set.toFinset_setOf]

Premises used: FormalMultilinearSeries.comp_rightInv_aux1, FormalMultilinearSeries.comp_rightInv_aux2, Set.toFinset_setOf
-- 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 : ℕ
hn : 2 ≤ n
⊢ p.rightInv i x n =
    -(↑i.symm : F →L[𝕜] E).compContinuousMultilinearMap (M₁ := fun (i : Fin n) ↦ F)
        (∑ c ∈ Set.toFinset {c : Composition n | 1 < c.length}, p.compAlongComposition (p.rightInv i x) c)

Tactic:
match n with
  | 0 => exact False.elim (zero_lt_two.not_ge hn)
  | 1 => exact False.elim (one_lt_two.not_ge hn)
  | n + 2 =>
    simp only [rightInv, neg_inj]
    congr (config := { closePost := false }) 1
    ext v
    have N : 0 < n + 2 := by simp
    have : ((p 1) fun _ : Fin 1 => 0) = 0 := ContinuousMultilinearMap.map_zero _
    simp [comp_rightInv_aux1 N, this, comp_rightInv_aux2, -Set.toFinset_setOf]
-- 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))
⊢ p.leftInv i x = (p.leftInv i x).comp (id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) 0))

Tactic:
simp