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

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

Tactic:
simp only [rightInv_coeff_zero]

Result:
no goals

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.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]

Result:
no goals

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.rightInv i x n = p.rightInv 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.rightInv i x m = p.rightInv i x m
⊢ p.removeZero.rightInv i x n = p.rightInv 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 < 1, p.removeZero.rightInv i x m = p.rightInv i x m
⊢ p.removeZero.rightInv i x 1 = p.rightInv i x 1

Tactic:
simp only [rightInv_coeff_one]

Result:
no goals

Proof state:
case e_f.e_p.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✝ n : ℕ
IH : ∀ m < n + 2, p.removeZero.rightInv i x m = p.rightInv i x m
k : ℕ
x✝ : Fin k → F
⊢ (if k < n + 2 then p.removeZero.rightInv i x k else 0) x✝ = (if k < n + 2 then p.rightInv i x k else 0) x✝

Tactic:
by_cases hk : k < n + 2 <;> simp [hk, IH]

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.rightInv i x m = p.rightInv i x m
⊢ (↑i.symm).compContinuousMultilinearMap
      (p.comp (fun k => if k < n + 2 then p.removeZero.rightInv i x k else 0) (n + 2)) =
    (↑i.symm).compContinuousMultilinearMap (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

Result:
case e_f.e_p.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✝ n : ℕ
IH : ∀ m < n + 2, p.removeZero.rightInv i x m = p.rightInv i x m
k : ℕ
x✝ : Fin k → F
⊢ (if k < n + 2 then p.removeZero.rightInv i x k else 0) x✝ = (if k < n + 2 then p.rightInv i x k else 0) x✝

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.rightInv i x m = p.rightInv i x m
⊢ p.removeZero.rightInv i x (n + 2) = p.rightInv i x (n + 2)

Tactic:
simp only [rightInv, neg_inj]

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.rightInv i x m = p.rightInv i x m
⊢ (↑i.symm).compContinuousMultilinearMap
      (p.removeZero.comp (fun k => if k < n + 2 then p.removeZero.rightInv i x k else 0) (n + 2)) =
    (↑i.symm).compContinuousMultilinearMap (p.comp (fun k => if k < n + 2 then p.rightInv i x k else 0) (n + 2))

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.rightInv i x = p.rightInv 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.rightInv i x n = p.rightInv 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.rightInv i x m = p.rightInv i x m
⊢ (↑i.symm).compContinuousMultilinearMap
      (p.removeZero.comp (fun k => if k < n + 2 then p.removeZero.rightInv i x k else 0) (n + 2)) =
    (↑i.symm).compContinuousMultilinearMap (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)]

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.rightInv i x m = p.rightInv i x m
⊢ (↑i.symm).compContinuousMultilinearMap
      (p.comp (fun k => if k < n + 2 then p.removeZero.rightInv i x k else 0) (n + 2)) =
    (↑i.symm).compContinuousMultilinearMap (p.comp (fun k => if k < n + 2 then p.rightInv i x k else 0) (n + 2))