awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ (p.comp q n : (a : (i : Fin n) → F) → F) v =
    HAdd.hAdd (α := F) (β := F)
      (∑ c ∈ Set.toFinset {c : Composition n | 1 < c.length},
          (p c.length : (a : (i : Fin c.length) → E) → F) (q.applyComposition c v) :
        F)
      ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ (q n : (a : (i : Fin n) → F) → E) v : F)
have A : Eq (α := Finset (Composition n)) univ (Set.toFinset {c : Composition n | 1 < c.length} ∪ {Composition.single n hn})
Tactic: have A :
    (Finset.univ : Finset (Composition n)) =
      {c | 1 < Composition.length c}.toFinset ∪ {Composition.single n hn} := by
    refine Subset.antisymm (fun c _ => ?_) (subset_univ _)
    by_cases h : 1 < c.length
    · simp [h]
    · have : c.length = 1 := by
        refine (eq_iff_le_not_lt.2 ⟨?_, h⟩).symm; exact c.length_pos_of_pos hn
      rw [← Composition.eq_single_iff_length hn] at this
      simp [this]
-- 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
A : Eq (α := Finset (Composition n)) univ (Set.toFinset {c : Composition n | 1 < c.length} ∪ {Composition.single n hn})
⊢ (p.comp q n : (a : (i : Fin n) → F) → F) v =
    HAdd.hAdd (α := F) (β := F)
      (∑ c ∈ Set.toFinset {c : Composition n | 1 < c.length},
          (p c.length : (a : (i : Fin c.length) → E) → F) (q.applyComposition c v) :
        F)
      ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ (q n : (a : (i : Fin n) → F) → E) v : F)
have B : Disjoint (α := Finset (Composition n)) (Set.toFinset {c : Composition n | 1 < c.length}) {Composition.single n hn}
Tactic: have B :
    Disjoint ({c | 1 < Composition.length c} : Set (Composition n)).toFinset
      {Composition.single n hn} := 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
n : ℕ
hn : 0 < n
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 F E
v : Fin n → F
A : Eq (α := Finset (Composition n)) univ (Set.toFinset {c : Composition n | 1 < c.length} ∪ {Composition.single n hn})
B : Disjoint (α := Finset (Composition n)) (Set.toFinset {c : Composition n | 1 < c.length}) {Composition.single n hn}
⊢ Eq.{u_3 + 1} (α := F)
    ((p (Composition.single n hn).length : (a : (i : Fin (Composition.single n hn).length) → E) → F)
        (q.applyComposition (Composition.single n hn) v) :
      F)
    ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ (q n : (a : (i : Fin n) → F) → E) v : F)
have apply : ∀ (j : ℕ) (hj1 : j < (Composition.single n hn).length),
  j < 1 →
    q.applyComposition (Composition.single n hn) v (⟨j, hj1⟩ : Fin (Composition.single n hn).length) =
      (q n : (a : (i : Fin n) → F) → E) v
Tactic: apply p.congr (Composition.single_length hn) fun j hj1 _ => ?_
-- 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
A : Eq (α := Finset (Composition n)) univ (Set.toFinset {c : Composition n | 1 < c.length} ∪ {Composition.single n hn})
B : Disjoint (α := Finset (Composition n)) (Set.toFinset {c : Composition n | 1 < c.length}) {Composition.single n hn}
⊢ (p.comp q n : (a : (i : Fin n) → F) → F) v =
    HAdd.hAdd (α := F) (β := F)
      (∑ c ∈ Set.toFinset {c : Composition n | 1 < c.length},
          (p c.length : (a : (i : Fin c.length) → E) → F) (q.applyComposition c v) :
        F)
      ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ (q n : (a : (i : Fin n) → F) → E) v : F)
have C : Eq.{u_3 + 1} (α := F)
  ((p (Composition.single n hn).length : (a : (i : Fin (Composition.single n hn).length) → E) → F)
      (q.applyComposition (Composition.single n hn) v) :
    F)
  ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ (q n : (a : (i : Fin n) → F) → E) v : F)
Tactic: have C :
    p (Composition.single n hn).length (q.applyComposition (Composition.single n hn) v) =
      p 1 fun _ : Fin 1 => q n v := by
    apply p.congr (Composition.single_length hn) fun j hj1 _ => ?_
    simp [applyComposition_single]
-- 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
⊢ (p.comp q n : (a : (i : Fin n) → F) → F) v =
    HAdd.hAdd (α := F) (β := F)
      (∑ c ∈ Set.toFinset {c : Composition n | 1 < c.length},
          (p c.length : (a : (i : Fin c.length) → E) → F) (q.applyComposition c v) :
        F)
      ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ (q n : (a : (i : Fin n) → F) → E) v : F)
have have : Eq (α := Finset (Composition n)) univ (Set.toFinset {c : Composition n | 1 < c.length} ∪ {Composition.single n hn})
Tactic: classical
  have A :
    (Finset.univ : Finset (Composition n)) =
      {c | 1 < Composition.length c}.toFinset ∪ {Composition.single n hn} := by
    refine Subset.antisymm (fun c _ => ?_) (subset_univ _)
    by_cases h : 1 < c.length
    · simp [h]
    · have : c.length = 1 := by
        refine (eq_iff_le_not_lt.2 ⟨?_, h⟩).symm; exact c.length_pos_of_pos hn
      rw [← Composition.eq_single_iff_length hn] at this
      simp [this]
  have B :
    Disjoint ({c | 1 < Composition.length c} : Set (Composition n)).toFinset
      {Composition.single n hn} := by
    simp
  have C :
    p (Composition.single n hn).length (q.applyComposition (Composition.single n hn) v) =
      p 1 fun _ : Fin 1 => q n v := by
    apply p.congr (Composition.single_length hn) fun j hj1 _ => ?_
    simp [applyComposition_single]
  simp [FormalMultilinearSeries.comp, A, Finset.sum_union B, C, -Set.toFinset_setOf,
    -add_right_inj, -Composition.single_length, -Finset.union_singleton]
-- 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
have :
  Eq (α := Finset (Composition n)) univ (Set.toFinset {c : Composition n | 1 < c.length} ∪ {Composition.single n hn})
⊢ (p.comp q n : (a : (i : Fin n) → F) → F) v =
    HAdd.hAdd (α := F) (β := F)
      (∑ c ∈ Set.toFinset {c : Composition n | 1 < c.length},
          (p c.length : (a : (i : Fin c.length) → E) → F) (q.applyComposition c v) :
        F)
      ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ (q n : (a : (i : Fin n) → F) → E) v : F)
have have₁ : ∀
  (A :
    Eq (α := Finset (Composition n)) univ
      (Set.toFinset {c : Composition n | 1 < c.length} ∪ {Composition.single n hn})),
  (p.comp q n : (a : (i : Fin n) → F) → F) v =
    HAdd.hAdd (α := F) (β := F)
      (∑ c ∈ Set.toFinset {c : Composition n | 1 < c.length},
          (p c.length : (a : (i : Fin c.length) → E) → F) (q.applyComposition c v) :
        F)
      ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ (q n : (a : (i : Fin n) → F) → E) v : F)
Tactic: classical
  have A :
    (Finset.univ : Finset (Composition n)) =
      {c | 1 < Composition.length c}.toFinset ∪ {Composition.single n hn} := by
    refine Subset.antisymm (fun c _ => ?_) (subset_univ _)
    by_cases h : 1 < c.length
    · simp [h]
    · have : c.length = 1 := by
        refine (eq_iff_le_not_lt.2 ⟨?_, h⟩).symm; exact c.length_pos_of_pos hn
      rw [← Composition.eq_single_iff_length hn] at this
      simp [this]
  have B :
    Disjoint ({c | 1 < Composition.length c} : Set (Composition n)).toFinset
      {Composition.single n hn} := by
    simp
  have C :
    p (Composition.single n hn).length (q.applyComposition (Composition.single n hn) v) =
      p 1 fun _ : Fin 1 => q n v := by
    apply p.congr (Composition.single_length hn) fun j hj1 _ => ?_
    simp [applyComposition_single]
  simp [FormalMultilinearSeries.comp, A, Finset.sum_union B, C, -Set.toFinset_setOf,
    -add_right_inj, -Composition.single_length, -Finset.union_singleton]
-- 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
n : ℕ
v : Fin (n + 2) → F
⊢ 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))
have N : 0 < n + 2
Tactic: have N : 0 < 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
n : ℕ
v : Fin (n + 2) → F
N : 0 < n + 2
⊢ 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))
have 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)
Tactic: refine sum_congr rfl fun c hc => p.congr rfl 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
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
have hc₁ : 1 < c.length
Tactic: simp only [Set.mem_toFinset (s := {c : Composition (n + 2) | 1 < c.length}),
      Set.mem_setOf_eq] at hc
Cleared hypotheses: hc
-- 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
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
⊢ 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)
have this : ∀ (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]
-- 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 𝕜 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)
have 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)
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 : ℕ
v : (i : Fin 0) → 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)
have 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)
Tactic: simp only [comp_coeff_zero', Matrix.zero_empty, id_apply_zero]
-- 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 : ℕ
v : (i : Fin 0) → F
⊢ 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)
have h₁ : Eq.{u_2 + 1} (α := (i : Fin 0) → E) (fun (_i : Fin 0) ↦ 0) ![]
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 : ℕ
v : (i : Fin 0) → F
⊢ Eq.{u_2 + 1} (α := (i : Fin 0) → E) (fun (_i : Fin 0) ↦ 0) ![]
have h₁ : ∀ (i : Fin 0), Eq.{u_2 + 1} (α := E) 0 (![] i)
Tactic: ext i
-- 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)) → F
⊢ 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)
have N : 0 < n + 2
Tactic: have N : 0 < 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
n_1 n : ℕ
hn : 2 ≤ n + 2
⊢ 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))
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.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: 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 : ℕ
hn : 2 ≤ n + 2
⊢ 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))
have 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)
Tactic: congr (config := { closePost := false }) 1
-- 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 : ℕ
hn : 2 ≤ n + 2
⊢ 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)
have 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)
Tactic: ext v
-- 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
n_1 n : ℕ
hn : 2 ≤ n + 2
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)
have N : 0 < n + 2
Tactic: have N : 0 < n + 2 := by simp
-- 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
n_1 n : ℕ
hn : 2 ≤ n + 2
v : (i : Fin (n + 2)) → F
N : 0 < n + 2
⊢ 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)
have this : 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 _
-- 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 𝕜 F E)
    ((p.leftInv i x).comp (id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) 0)) : FormalMultilinearSeries 𝕜 F E)
    ((p.leftInv i x).comp (p.comp (p.rightInv i x)) : FormalMultilinearSeries 𝕜 F E)
have rw : Eq (α := FormalMultilinearSeries 𝕜 F E)
  ((p.leftInv i x).comp (id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) 0)) : FormalMultilinearSeries 𝕜 F E)
  ((p.leftInv i x).comp (id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) 0)) : FormalMultilinearSeries 𝕜 F E)
Tactic: rw [comp_rightInv p i _ 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
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 𝕜 F E)
    ((p.leftInv i x).comp (p.comp (p.rightInv i x)) : FormalMultilinearSeries 𝕜 F E)
    (FormalMultilinearSeries.comp ((p.leftInv i x).comp p) (p.rightInv i x) : FormalMultilinearSeries 𝕜 F E)
have rw : Eq (α := FormalMultilinearSeries 𝕜 F E) ((p.leftInv i x).comp (p.comp (p.rightInv i x)) : FormalMultilinearSeries 𝕜 F E)
  ((p.leftInv i x).comp (p.comp (p.rightInv i x)) : FormalMultilinearSeries 𝕜 F E)
Tactic: rw [comp_assoc]