-- Mathlib/Analysis/Analytic/Inverse.lean
theorem comp_rightInv_aux1 {n : ℕ} (hn : 0 < n) (p : FormalMultilinearSeries 𝕜 E F)
    (q : FormalMultilinearSeries 𝕜 F E) (v : Fin n → F) :
    p.comp q n v =
      ∑ c ∈ {c : Composition n | 1 < c.length}.toFinset,
          p c.length (q.applyComposition c v) + p 1 fun _ => q n v

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
hn : 0 < n
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 F E
v : Fin n → F
A : univ = {c | 1 < c.length}.toFinset ∪ {Composition.single n hn}
B : Disjoint {c | 1 < c.length}.toFinset {Composition.single n hn}
⊢ (p.comp q n) v = ∑ c ∈ {c | 1 < c.length}.toFinset, (p c.length) (q.applyComposition c v) + (p 1) fun x => (q n) v

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]

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
hn : 0 < n
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 F E
v : Fin n → F
A : univ = {c | 1 < c.length}.toFinset ∪ {Composition.single n hn}
B : Disjoint {c | 1 < c.length}.toFinset {Composition.single n hn}
C : (p (Composition.single n hn).length) (q.applyComposition (Composition.single n hn) v) = (p 1) fun x => (q n) v
⊢ (p.comp q n) v = ∑ c ∈ {c | 1 < c.length}.toFinset, (p c.length) (q.applyComposition c v) + (p 1) fun x => (q n) v

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
hn : 0 < n
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 F E
v : Fin n → F
A : univ = {c | 1 < c.length}.toFinset ∪ {Composition.single n hn}
⊢ Disjoint {c | 1 < c.length}.toFinset {Composition.single n hn}

Tactic:
simp [Set.mem_toFinset (s := {c | 1 < Composition.length c})]

Result:
no goals

Proof state:
case neg
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
hn : 0 < n
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 F E
v : Fin n → F
c : Composition n
x✝ : c ∈ univ
h : ¬1 < c.length
this : c.length = 1
⊢ c ∈ {c | 1 < c.length}.toFinset ∪ {Composition.single n hn}

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

Result:
case neg
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
hn : 0 < n
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 F E
v : Fin n → F
c : Composition n
x✝ : c ∈ univ
h : ¬1 < c.length
this : c = Composition.single n hn
⊢ c ∈ {c | 1 < c.length}.toFinset ∪ {Composition.single n hn}

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
hn : 0 < n
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 F E
v : Fin n → F
c : Composition n
x✝ : c ∈ univ
h : ¬1 < c.length
⊢ 1 ≤ c.length

Tactic:
exact c.length_pos_of_pos hn

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
hn : 0 < n
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 F E
v : Fin n → F
A : univ = {c | 1 < c.length}.toFinset ∪ {Composition.single n hn}
B : Disjoint {c | 1 < c.length}.toFinset {Composition.single n hn}
C : (p (Composition.single n hn).length) (q.applyComposition (Composition.single n hn) v) = (p 1) fun x => (q n) v
⊢ (p.comp q n) v = ∑ c ∈ {c | 1 < c.length}.toFinset, (p c.length) (q.applyComposition c v) + (p 1) fun x => (q n) v

Tactic:
simp [FormalMultilinearSeries.comp, A, Finset.sum_union B, C, -Set.toFinset_setOf,
  -add_right_inj, -Composition.single_length]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
hn : 0 < n
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 F E
v : Fin n → F
c : Composition n
x✝ : c ∈ univ
h : ¬1 < c.length
⊢ c.length = 1

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

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
hn : 0 < n
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 F E
v : Fin n → F
c : Composition n
x✝ : c ∈ univ
h : ¬1 < c.length
⊢ 1 ≤ c.length