-- Mathlib/Analysis/Analytic/Inverse.lean
theorem leftInv_removeZero (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E) :
    p.removeZero.leftInv i x = p.leftInv i x

Proof state:
case h
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
n : ℕ
⊢ p.removeZero.leftInv i x n = p.leftInv i x n

Tactic:
induction' n using Nat.strongRec' with n IH

Result:
case h.H
𝕜 : 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
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

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
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
⊢ p.removeZero.leftInv i x 0 = p.leftInv i x 0

Tactic:
simp

Result:
no goals

Proof state:
case mk.H
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
n✝ 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 : ⟨c, hc⟩ ∈ univ
v : Fin (n + 2) → F
⊢ (p.removeZero.leftInv i x c.length) ((p.removeZero.compContinuousLinearMap ↑i.symm).applyComposition c v) =
    (p.leftInv i x c.length) ((p.compContinuousLinearMap ↑i.symm).applyComposition c v)

Tactic:
simp [IH _ hc]

Result:
no goals

Proof state:
case mk
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
n✝ 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 : ⟨c, hc⟩ ∈ univ
⊢ ContinuousMultilinearMap.compAlongComposition (p.removeZero.compContinuousLinearMap ↑i.symm) (↑⟨c, hc⟩)
      (p.removeZero.leftInv i x (↑⟨c, hc⟩).length) =
    ContinuousMultilinearMap.compAlongComposition (p.compContinuousLinearMap ↑i.symm) (↑⟨c, hc⟩)
      (p.leftInv i x (↑⟨c, hc⟩).length)

Tactic:
ext v

Result:
case mk.H
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
n✝ 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 : ⟨c, hc⟩ ∈ univ
v : Fin (n + 2) → F
⊢ (ContinuousMultilinearMap.compAlongComposition (p.removeZero.compContinuousLinearMap ↑i.symm) (↑⟨c, hc⟩)
        (p.removeZero.leftInv i x (↑⟨c, hc⟩).length))
      v =
    (ContinuousMultilinearMap.compAlongComposition (p.compContinuousLinearMap ↑i.symm) (↑⟨c, hc⟩)
        (p.leftInv i x (↑⟨c, hc⟩).length))
      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
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
⊢ p.removeZero.leftInv i x = p.leftInv i x

Tactic:
ext1 n

Result:
case h
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
n : ℕ
⊢ p.removeZero.leftInv i x n = p.leftInv i x n

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
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
n✝ n : ℕ
IH : ∀ m < n + 2, p.removeZero.leftInv i x m = p.leftInv i x m
⊢ ∑ c : { c // c.length < n + 2 },
      ContinuousMultilinearMap.compAlongComposition (p.removeZero.compContinuousLinearMap ↑i.symm) (↑c)
        (p.removeZero.leftInv i x (↑c).length) =
    ∑ c : { c // c.length < n + 2 },
      ContinuousMultilinearMap.compAlongComposition (p.compContinuousLinearMap ↑i.symm) (↑c) (p.leftInv i x (↑c).length)

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

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
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
n✝ n : ℕ
IH : ∀ m < n + 2, p.removeZero.leftInv i x m = p.leftInv i x m
c : { c // c.length < n + 2 }
cuniv : c ∈ univ
⊢ ContinuousMultilinearMap.compAlongComposition (p.removeZero.compContinuousLinearMap ↑i.symm) (↑c)
      (p.removeZero.leftInv i x (↑c).length) =
    ContinuousMultilinearMap.compAlongComposition (p.compContinuousLinearMap ↑i.symm) (↑c) (p.leftInv i x (↑c).length)

Proof state:
case h.H
𝕜 : 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
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 | 1 => simp | n + 2 =>
  simp only [leftInv, neg_inj]
  refine Finset.sum_congr rfl fun c cuniv => ?_
  rcases c with ⟨c, hc⟩
  ext v
  dsimp
  simp [IH _ hc]

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
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
n✝ n : ℕ
IH : ∀ m < n + 2, p.removeZero.leftInv i x m = p.leftInv i x m
c : { c // c.length < n + 2 }
cuniv : c ∈ univ
⊢ ContinuousMultilinearMap.compAlongComposition (p.removeZero.compContinuousLinearMap ↑i.symm) (↑c)
      (p.removeZero.leftInv i x (↑c).length) =
    ContinuousMultilinearMap.compAlongComposition (p.compContinuousLinearMap ↑i.symm) (↑c) (p.leftInv i x (↑c).length)

Tactic:
rcases c with ⟨c, hc⟩

Result:
case mk
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
n✝ 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 : ⟨c, hc⟩ ∈ univ
⊢ ContinuousMultilinearMap.compAlongComposition (p.removeZero.compContinuousLinearMap ↑i.symm) (↑⟨c, hc⟩)
      (p.removeZero.leftInv i x (↑⟨c, hc⟩).length) =
    ContinuousMultilinearMap.compAlongComposition (p.compContinuousLinearMap ↑i.symm) (↑⟨c, hc⟩)
      (p.leftInv i x (↑⟨c, hc⟩).length)