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

Tactic:
simp only [rightInv_coeff_zero]

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

Tactic:
simp only [rightInv_coeff_one]

Premises used: 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
n_1 n : ℕ
IH : ∀ m < n + 2, p.removeZero.rightInv i x m = p.rightInv i x m
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)))
⊢ 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))

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 : ℕ
IH : ∀ m < n + 2, p.removeZero.rightInv i x m = p.rightInv i x m
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)))
⊢ 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:
rw [removeZero_comp_of_pos _ _ (add_pos_of_nonneg_of_pos n.zero_le zero_lt_two)]

Premises used: Nat.zero_le, FormalMultilinearSeries.removeZero_comp_of_pos, add_pos_of_nonneg_of_pos, 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_1 n : ℕ
IH : ∀ m < n + 2, p.removeZero.rightInv i x m = p.rightInv i x m
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)
⊢ 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:
congr (config := { closePost := false }) 2 with k
-- 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.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)
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)
⊢ 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
-- 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.rightInv i x m = p.rightInv i x m
k : ℕ
x_1 : (i : Fin k) → F
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:
simp [hk, 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_1 n : ℕ
IH : ∀ m < n + 2, p.removeZero.rightInv i x m = p.rightInv i x m
k : ℕ
x_1 : (i : Fin k) → F
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:
simp [hk, 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 < n, p.removeZero.rightInv i x m = p.rightInv i x m
⊢ p.removeZero.rightInv i x n = p.rightInv i x n

Tactic:
match n with
  | 0 => simp only [rightInv_coeff_zero]
  | 1 => simp only [rightInv_coeff_one]
  | n + 2 =>
    simp only [rightInv, neg_inj]
    rw [removeZero_comp_of_pos _ _ (add_pos_of_nonneg_of_pos n.zero_le zero_lt_two)]
    congr (config := { closePost := false }) 2 with k
    by_cases hk : k < n + 2 <;> simp [hk, 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
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})

Tactic:
Subset.antisymm (fun c _ => ?_) (subset_univ _)

Premises used: Finset.Subset.antisymm, Finset.subset_univ
-- 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
n : ℕ
hn : 0 < n
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 F E
v : Fin n → F
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
⊢ Eq (α := Finset (Composition n)) univ (Set.toFinset {c : Composition n | 1 < c.length} ∪ {Composition.single n hn})

Tactic:
refine Subset.antisymm (fun c _ => ?_) (subset_univ _)

Premises used: Finset.Subset.antisymm, Finset.subset_univ
-- 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
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
neg :
  ∀ (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

Tactic:
by_cases h : 1 < c.length

Premises used: Composition.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
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

Tactic:
simp [h]
-- 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
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

Tactic:
(eq_iff_le_not_lt.2 ⟨?_, h⟩).symm

Premises used: Iff.mpr, And.intro, eq_iff_le_not_lt, Eq.symm
-- 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
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
refine : 1 ≤ c.length
⊢ c.length = 1

Tactic:
refine (eq_iff_le_not_lt.2 ⟨?_, h⟩).symm

Premises used: Iff.mpr, And.intro, eq_iff_le_not_lt, Eq.symm
-- 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
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
⊢ 1 ≤ c.length

Tactic:
c.length_pos_of_pos hn

Premises used: Composition.length_pos_of_pos, Nat.lt
-- 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
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
⊢ 1 ≤ c.length

Tactic:
exact c.length_pos_of_pos hn

Premises used: Composition.length_pos_of_pos
-- 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
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

Tactic:
have : c.length = 1 := by
        refine (eq_iff_le_not_lt.2 ⟨?_, h⟩).symm; exact c.length_pos_of_pos hn
-- 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
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
⊢ c = Composition.single n hn

Tactic:
rw [← Composition.eq_single_iff_length hn] at this

Premises used: 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
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 = Composition.single n hn
⊢ Membership.mem (γ := Finset (Composition n))
    (Set.toFinset {c : Composition n | 1 < c.length} ∪ {Composition.single n hn}) c

Tactic:
simp [this]
-- 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
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})

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]
-- 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
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})
⊢ Disjoint (α := Finset (Composition n)) (Set.toFinset {c : Composition n | 1 < c.length}) {Composition.single n hn}

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
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})
⊢ 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
-- 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
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}
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
⊢ 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:
apply p.congr (Composition.single_length hn) fun j hj1 _ => ?_

Premises used: FormalMultilinearSeries.congr, Composition.single_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
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}
j : ℕ
hj1 : j < (Composition.single n hn).length
h : 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:
simp [applyComposition_single]

Premises used: FormalMultilinearSeries.applyComposition_single
-- 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
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)

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]
-- 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
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}
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)
⊢ (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:
simp [FormalMultilinearSeries.comp, A, Finset.sum_union B, C, -Set.toFinset_setOf,
    -add_right_inj, -Composition.single_length, -Finset.union_singleton]

Premises used: Composition.single_length, Finset.sum_union, FormalMultilinearSeries.comp, Finset.union_singleton, add_right_inj, 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 : ℕ
v : 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 : ℕ
v : 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 : ℕ
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))

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

Premises used: FormalMultilinearSeries.congr, Finset.sum_congr, rfl