awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
k : ℕ
blocksFun : Fin k → ℕ
H : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun ∈ compPartialSumSource 2 (n + 1) n
K :
  (compChangeOfVariables 2 (n + 1) n (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) H).snd (β := fun (n : ℕ) ↦
        Composition n).length =
    k
h h₁ :
  HEq (α :=
    Fintype (Fin (Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun))))
    (Fin.fintype (Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun)))
    (Fin.fintype k)
⊢ HEq (α :=
    Fintype (Fin (Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun))))
    (Fin.fintype (Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun))) (β :=
    Fintype
      (Fin
        (compChangeOfVariables 2 (n + 1) n (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) H).snd (β :=
            fun (n : ℕ) ↦ Composition n).length))
    (Fin.fintype
      (compChangeOfVariables 2 (n + 1) n (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) H).snd (β :=
          fun (n : ℕ) ↦ Composition n).length)

Tactic:
try rw [K]
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
k : ℕ
blocksFun : Fin k → ℕ
H : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun ∈ compPartialSumSource 2 (n + 1) n
K :
  (compChangeOfVariables 2 (n + 1) n (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) H).snd (β := fun (n : ℕ) ↦
        Composition n).length =
    k
h :
  ∀ (i : Fin k),
    r *
        (HPow.hPow (β := ℕ) a
            (Sigma.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) i : ℕ) *
          p (Sigma.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) i)) =
      r *
        (a ^
            (compChangeOfVariables 2 (n + 1) n (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) H).snd (β :=
                  fun (n : ℕ) ↦ Composition n).blocksFun
              (⟨(↑i : ℕ), ⋯⟩ :
                Fin
                  (compChangeOfVariables 2 (n + 1) n (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) H).snd (β :=
                      fun (n : ℕ) ↦ Composition n).length) *
          p
            ((compChangeOfVariables 2 (n + 1) n (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) H).snd (β :=
                  fun (n : ℕ) ↦ Composition n).blocksFun
              (⟨(↑i : ℕ), ⋯⟩ :
                Fin
                  (compChangeOfVariables 2 (n + 1) n (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) H).snd (β :=
                      fun (n : ℕ) ↦ Composition n).length)))
⊢ HEq (α := Fin (Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun)) → ℝ)
    fun (j : Fin (Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun))) ↦
    r *
      (HPow.hPow (β := ℕ) a
          (Sigma.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) j : ℕ) *
        p (Sigma.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) j))
    (β :=
    Fin
        (compChangeOfVariables 2 (n + 1) n (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) H).snd (β :=
            fun (n : ℕ) ↦ Composition n).length →
      ℝ)
    fun
      (j :
        Fin
          (compChangeOfVariables 2 (n + 1) n (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) H).snd (β :=
              fun (n : ℕ) ↦ Composition n).length) ↦
    r *
      (a ^
          (compChangeOfVariables 2 (n + 1) n (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) H).snd (β :=
                fun (n : ℕ) ↦ Composition n).blocksFun
            j *
        p
          ((compChangeOfVariables 2 (n + 1) n (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) H).snd (β :=
                fun (n : ℕ) ↦ Composition n).blocksFun
            j))

Tactic:
rw [Fin.heq_fun_iff K.symm]

Premises used: Fin.heq_fun_iff, Eq.symm
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
k : ℕ
blocksFun : Fin k → ℕ
H : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun ∈ compPartialSumSource 2 (n + 1) n
K :
  (compChangeOfVariables 2 (n + 1) n (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) H).snd (β := fun (n : ℕ) ↦
        Composition n).length =
    k
j : Fin k
h h₁ :
  r *
      (HPow.hPow (β := ℕ) a
          (Sigma.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) j : ℕ) *
        p (Sigma.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) j)) =
    r *
      (HPow.hPow (β := ℕ) a
          (Sigma.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) j : ℕ) *
        p (Sigma.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) j))
⊢ r *
      (HPow.hPow (β := ℕ) a
          (Sigma.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) j : ℕ) *
        p (Sigma.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) j)) =
    r *
      (a ^
          (compChangeOfVariables 2 (n + 1) n (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) H).snd (β :=
                fun (n : ℕ) ↦ Composition n).blocksFun
            (⟨(↑j : ℕ), ⋯⟩ :
              Fin
                (compChangeOfVariables 2 (n + 1) n (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) H).snd (β :=
                    fun (n : ℕ) ↦ Composition n).length) *
        p
          ((compChangeOfVariables 2 (n + 1) n (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) H).snd (β :=
                fun (n : ℕ) ↦ Composition n).blocksFun
            (⟨(↑j : ℕ), ⋯⟩ :
              Fin
                (compChangeOfVariables 2 (n + 1) n (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) H).snd (β :=
                    fun (n : ℕ) ↦ Composition n).length)))

Tactic:
rw [compChangeOfVariables_blocksFun]

Premises used: FormalMultilinearSeries.compChangeOfVariables_blocksFun
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
rw :
  Eq (α := ℝ)
    (∑ a_1 ∈ Ico 2 (n + 1),
      ∑ s ∈ Fintype.piFinset (δ := fun (a : Fin a_1) ↦ ℕ) fun (x : Fin a_1) ↦ Ico 1 n,
        ∏ j : Fin a_1, r * (a ^ s j * p (s j)))
    (∑ j ∈ Ico 2 (n + 1), r ^ j * HPow.hPow (α := ℝ) (∑ k ∈ Ico 1 n, a ^ k * p k) j)
⊢ Eq (α := ℝ)
    (∑ e ∈ compPartialSumSource 2 (n + 1) n,
      ∏ j : Fin e.fst, r * (a ^ e.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) j * p (e.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) j)))
    (∑ j ∈ Ico 2 (n + 1), r ^ j * HPow.hPow (α := ℝ) (∑ k ∈ Ico 1 n, a ^ k * p k) j)

Tactic:
rw [compPartialSumSource,
        ← sum_sigma' (Ico 2 (n + 1))
          (fun k : ℕ => (Fintype.piFinset fun _ : Fin k => Ico 1 n : Finset (Fin k → ℕ)))
          (fun n e => ∏ j : Fin n, r * (a ^ e j * p (e j)))]

Premises used: HMul.hMul, Finset.univ, FormalMultilinearSeries.compPartialSumSource, Finset.Ico, Finset.sum_sigma', Fintype.piFinset, Finset.prod, HPow.hPow, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
a₁ :
  ∀ j ∈ Ico 2 (n + 1),
    ∑ s ∈ Fintype.piFinset (δ := fun (a : Fin j) ↦ ℕ) fun (x : Fin j) ↦ Ico 1 n, ∏ j : Fin j, r * (a ^ s j * p (s j)) =
      r ^ j * HPow.hPow (α := ℝ) (∑ k ∈ Ico 1 n, a ^ k * p k) j
⊢ Eq (α := ℝ)
    (∑ a_1 ∈ Ico 2 (n + 1),
      ∑ s ∈ Fintype.piFinset (δ := fun (a : Fin a_1) ↦ ℕ) fun (x : Fin a_1) ↦ Ico 1 n,
        ∏ j : Fin a_1, r * (a ^ s j * p (s j)))
    (∑ j ∈ Ico 2 (n + 1), r ^ j * HPow.hPow (α := ℝ) (∑ k ∈ Ico 1 n, a ^ k * p k) j)

Tactic:
congr! with j
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
j : ℕ
h : j ∈ Ico 2 (n + 1)
a₁ :
  (∑ x ∈ Fintype.piFinset (δ := fun (a : Fin j) ↦ ℕ) fun (x : Fin j) ↦ Ico 1 n,
      (MultilinearMap.mkPiAlgebra ℝ (Fin j) ℝ : (a : (i : Fin j) → ℝ) → ℝ) fun (j : Fin j) ↦ r * (a ^ x j * p (x j))) =
    r ^ j * HPow.hPow (α := ℝ) (∑ k ∈ Ico 1 n, a ^ k * p k) j
⊢ ∑ s ∈ Fintype.piFinset (δ := fun (a : Fin j) ↦ ℕ) fun (x : Fin j) ↦ Ico 1 n, ∏ j : Fin j, r * (a ^ s j * p (s j)) =
    r ^ j * HPow.hPow (α := ℝ) (∑ k ∈ Ico 1 n, a ^ k * p k) j

Tactic:
simp only [← @MultilinearMap.mkPiAlgebra_apply ℝ (Fin j) _ ℝ]

Premises used: MultilinearMap.mkPiAlgebra_apply
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
j : ℕ
h : j ∈ Ico 2 (n + 1)
a₁ :
  ((MultilinearMap.mkPiAlgebra ℝ (Fin j) ℝ : (a : (i : Fin j) → ℝ) → ℝ) fun (i : Fin j) ↦
      ∑ j ∈ Ico 1 n, r * (a ^ j * p j)) =
    r ^ j * HPow.hPow (α := ℝ) (∑ k ∈ Ico 1 n, a ^ k * p k) j
⊢ (∑ x ∈ Fintype.piFinset (δ := fun (a : Fin j) ↦ ℕ) fun (x : Fin j) ↦ Ico 1 n,
      (MultilinearMap.mkPiAlgebra ℝ (Fin j) ℝ : (a : (i : Fin j) → ℝ) → ℝ) fun (j : Fin j) ↦ r * (a ^ x j * p (x j))) =
    r ^ j * HPow.hPow (α := ℝ) (∑ k ∈ Ico 1 n, a ^ k * p k) j

Tactic:
simp only [←
        MultilinearMap.map_sum_finset (MultilinearMap.mkPiAlgebra ℝ (Fin j) ℝ) fun _ (m : ℕ) =>
          r * (a ^ m * p m)]

Premises used: Real, HMul.hMul, MultilinearMap.mkPiAlgebra, HPow.hPow, MultilinearMap.map_sum_finset, Fin
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
j : ℕ
h : j ∈ Ico 2 (n + 1)
a₁ : ∏ i : Fin j, ∑ j ∈ Ico 1 n, r * (a ^ j * p j) = r ^ j * HPow.hPow (α := ℝ) (∑ k ∈ Ico 1 n, a ^ k * p k) j
⊢ ((MultilinearMap.mkPiAlgebra ℝ (Fin j) ℝ : (a : (i : Fin j) → ℝ) → ℝ) fun (i : Fin j) ↦
      ∑ j ∈ Ico 1 n, r * (a ^ j * p j)) =
    r ^ j * HPow.hPow (α := ℝ) (∑ k ∈ Ico 1 n, a ^ k * p k) j

Tactic:
simp only [MultilinearMap.mkPiAlgebra_apply]

Premises used: MultilinearMap.mkPiAlgebra_apply
-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
j : ℕ
h : j ∈ Ico 2 (n + 1)
⊢ ∏ i : Fin j, ∑ j ∈ Ico 1 n, r * (a ^ j * p j) = r ^ j * HPow.hPow (α := ℝ) (∑ k ∈ Ico 1 n, a ^ k * p k) j

Tactic:
simp [prod_const, ← mul_sum, mul_pow]

Premises used: Finset.mul_sum, Finset.prod_const, mul_pow
-- 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
x : E
n : ℕ
hn : 2 ≤ n + 1
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
r a C : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
hC : 0 ≤ C
hp : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ‖(↑i.symm : F →L[𝕜] E)‖
⊢ ∑ k ∈ Ico 1 (n + 1), a ^ k * ‖p.rightInv i x k‖ = a * I + ∑ k ∈ Ico 2 (n + 1), a ^ k * ‖p.rightInv i x k‖

Tactic:
simp only [I, LinearIsometryEquiv.norm_map, pow_one, rightInv_coeff_one,
        show Ico (1 : ℕ) 2 = {1} from Nat.Ico_succ_singleton 1,
        sum_singleton, ← sum_Ico_consecutive _ one_le_two hn]

Premises used: LinearIsometryEquiv.norm_map, Finset.sum_singleton, pow_one, Finset.sum_Ico_consecutive, one_le_two, Nat.Ico_succ_singleton, OfNat.ofNat, 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
x : E
n : ℕ
hn : 2 ≤ n + 1
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
r a C : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
hC : 0 ≤ C
hp : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ‖(↑i.symm : F →L[𝕜] E)‖
h :
  ∀ (j : ℕ) (hj : j ∈ Ico 2 (n + 1)),
    a ^ j * ‖p.rightInv i x j‖ =
      a ^ j *
        norm (E := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin j) ↦ F) E)
          ((↑i.symm : F →L[𝕜] E).compContinuousMultilinearMap (M₁ := fun (i : Fin j) ↦ F)
            (∑ c ∈ Set.toFinset {c : Composition j | 1 < c.length}, p.compAlongComposition (p.rightInv i x) c))
⊢ a * I + ∑ k ∈ Ico 2 (n + 1), a ^ k * ‖p.rightInv i x k‖ =
    a * I +
      ∑ k ∈ Ico 2 (n + 1),
        a ^ k *
          norm (E := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin k) ↦ F) E)
            ((↑i.symm : F →L[𝕜] E).compContinuousMultilinearMap (M₁ := fun (i : Fin k) ↦ F)
              (∑ c ∈ Set.toFinset {c : Composition k | 1 < c.length}, p.compAlongComposition (p.rightInv i x) c))

Tactic:
congr! 2 with j hj
-- 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
x : E
n : ℕ
hn : 2 ≤ n + 1
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
r a C : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
hC : 0 ≤ C
hp : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ‖(↑i.symm : F →L[𝕜] E)‖
j : ℕ
hj : j ∈ Ico 2 (n + 1)
h :
  a ^ j *
      norm (E := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin j) ↦ F) E)
        (-(↑i.symm : F →L[𝕜] E).compContinuousMultilinearMap (M₁ := fun (i : Fin j) ↦ F)
            (∑ c ∈ Set.toFinset {c : Composition j | 1 < c.length}, p.compAlongComposition (p.rightInv i x) c)) =
    a ^ j *
      norm (E := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin j) ↦ F) E)
        ((↑i.symm : F →L[𝕜] E).compContinuousMultilinearMap (M₁ := fun (i : Fin j) ↦ F)
          (∑ c ∈ Set.toFinset {c : Composition j | 1 < c.length}, p.compAlongComposition (p.rightInv i x) c))
h₁ h₂ :
  a ^ j *
      norm (E := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin j) ↦ F) E)
        ((↑i.symm : F →L[𝕜] E).compContinuousMultilinearMap (M₁ := fun (i : Fin j) ↦ F)
          (∑ c ∈ Set.toFinset {c : Composition j | 1 < c.length}, p.compAlongComposition (p.rightInv i x) c)) =
    a ^ j *
      norm (E := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin j) ↦ F) E)
        ((↑i.symm : F →L[𝕜] E).compContinuousMultilinearMap (M₁ := fun (i : Fin j) ↦ F)
          (∑ c ∈ Set.toFinset {c : Composition j | 1 < c.length}, p.compAlongComposition (p.rightInv i x) c))
⊢ a ^ j * ‖p.rightInv i x j‖ =
    a ^ j *
      norm (E := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin j) ↦ F) E)
        ((↑i.symm : F →L[𝕜] E).compContinuousMultilinearMap (M₁ := fun (i : Fin j) ↦ F)
          (∑ c ∈ Set.toFinset {c : Composition j | 1 < c.length}, p.compAlongComposition (p.rightInv i x) c))

Tactic:
rw [rightInv_coeff _ _ _ _ (mem_Ico.1 hj).1, norm_neg]

Premises used: And.left, norm_neg, Iff.mp, FormalMultilinearSeries.rightInv_coeff, Finset.mem_Ico
-- 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
x : E
n : ℕ
hn : 2 ≤ n + 1
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
r a C : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
hC : 0 ≤ C
hp : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ‖(↑i.symm : F →L[𝕜] E)‖
bc :
  ∀ j ∈ Ico 2 (n + 1),
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin j) ↦ F) E)
        ((↑i.symm : F →L[𝕜] E).compContinuousMultilinearMap (M₁ := fun (i : Fin j) ↦ F)
          (∑ c ∈ Set.toFinset {c : Composition j | 1 < c.length}, p.compAlongComposition (p.rightInv i x) c)) ≤
      I *
        ∑ c ∈ Set.toFinset {c : Composition j | 1 < c.length},
          C * r ^ c.length *
            ∏ j_1 : Fin c.length,
              norm (E := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin (c.blocksFun j_1)) ↦ F) E)
                (p.rightInv i x (c.blocksFun j_1))
⊢ a * I +
      ∑ k ∈ Ico 2 (n + 1),
        a ^ k *
          norm (E := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin k) ↦ F) E)
            ((↑i.symm : F →L[𝕜] E).compContinuousMultilinearMap (M₁ := fun (i : Fin k) ↦ F)
              (∑ c ∈ Set.toFinset {c : Composition k | 1 < c.length}, p.compAlongComposition (p.rightInv i x) c)) ≤
    a * ‖(↑i.symm : F →L[𝕜] E)‖ +
      ∑ k ∈ Ico 2 (n + 1),
        a ^ k *
          (I *
            ∑ c ∈ Set.toFinset {c : Composition k | 1 < c.length},
              C * r ^ c.length *
                ∏ j : Fin c.length,
                  norm (E := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin (c.blocksFun j)) ↦ F) E)
                    (p.rightInv i x (c.blocksFun j)))

Tactic:
gcongr with j
-- 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
x : E
n : ℕ
hn : 2 ≤ n + 1
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
r a C : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
hC : 0 ≤ C
hp : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ‖(↑i.symm : F →L[𝕜] E)‖
j : ℕ
h : j ∈ Ico 2 (n + 1)
bc :
  ‖(↑i.symm : F →L[𝕜] E)‖ *
      norm.{u_3} (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin j) ↦ F) F)
        (∑ c ∈ Set.toFinset {c : Composition j | 1 < c.length}, p.compAlongComposition (p.rightInv i x) c) ≤
    I *
      ∑ c ∈ Set.toFinset {c : Composition j | 1 < c.length},
        C * r ^ c.length *
          ∏ j_1 : Fin c.length,
            norm (E := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin (c.blocksFun j_1)) ↦ F) E)
              (p.rightInv i x (c.blocksFun j_1))
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin j) ↦ F) E)
      ((↑i.symm : F →L[𝕜] E).compContinuousMultilinearMap (M₁ := fun (i : Fin j) ↦ F)
        (∑ c ∈ Set.toFinset {c : Composition j | 1 < c.length}, p.compAlongComposition (p.rightInv i x) c)) ≤
    I *
      ∑ c ∈ Set.toFinset {c : Composition j | 1 < c.length},
        C * r ^ c.length *
          ∏ j_1 : Fin c.length,
            norm (E := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin (c.blocksFun j_1)) ↦ F) E)
              (p.rightInv i x (c.blocksFun j_1))

Tactic:
apply (ContinuousLinearMap.norm_compContinuousMultilinearMap_le _ _).trans

Premises used: ContinuousLinearMap.norm_compContinuousMultilinearMap_le, LE.le.trans
-- 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
x : E
n : ℕ
hn : 2 ≤ n + 1
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
r a C : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
hC : 0 ≤ C
hp : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ‖(↑i.symm : F →L[𝕜] E)‖
j : ℕ
h : j ∈ Ico 2 (n + 1)
bc :
  norm.{u_3} (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin j) ↦ F) F)
      (∑ c ∈ Set.toFinset {c : Composition j | 1 < c.length}, p.compAlongComposition (p.rightInv i x) c) ≤
    ∑ c ∈ Set.toFinset {c : Composition j | 1 < c.length},
      C * r ^ c.length *
        ∏ j_1 : Fin c.length,
          norm (E := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin (c.blocksFun j_1)) ↦ F) E)
            (p.rightInv i x (c.blocksFun j_1))
⊢ ‖(↑i.symm : F →L[𝕜] E)‖ *
      norm.{u_3} (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin j) ↦ F) F)
        (∑ c ∈ Set.toFinset {c : Composition j | 1 < c.length}, p.compAlongComposition (p.rightInv i x) c) ≤
    I *
      ∑ c ∈ Set.toFinset {c : Composition j | 1 < c.length},
        C * r ^ c.length *
          ∏ j_1 : Fin c.length,
            norm (E := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin (c.blocksFun j_1)) ↦ F) E)
              (p.rightInv i x (c.blocksFun j_1))

Tactic:
gcongr
-- 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
x : E
n : ℕ
hn : 2 ≤ n + 1
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
r a C : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
hC : 0 ≤ C
hp : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ‖(↑i.symm : F →L[𝕜] E)‖
j : ℕ
h : j ∈ Ico 2 (n + 1)
bc :
  LE.le (α := ℝ)
    (∑ i_1 ∈ Set.toFinset {c : Composition j | 1 < c.length}, ‖p.compAlongComposition (p.rightInv i x) i_1‖)
    (∑ c ∈ Set.toFinset {c : Composition j | 1 < c.length},
      C * r ^ c.length *
        ∏ j_1 : Fin c.length,
          norm (E := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin (c.blocksFun j_1)) ↦ F) E)
            (p.rightInv i x (c.blocksFun j_1)))
⊢ norm.{u_3} (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin j) ↦ F) F)
      (∑ c ∈ Set.toFinset {c : Composition j | 1 < c.length}, p.compAlongComposition (p.rightInv i x) c) ≤
    ∑ c ∈ Set.toFinset {c : Composition j | 1 < c.length},
      C * r ^ c.length *
        ∏ j_1 : Fin c.length,
          norm (E := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin (c.blocksFun j_1)) ↦ F) E)
            (p.rightInv i x (c.blocksFun j_1))

Tactic:
apply (norm_sum_le _ _).trans

Premises used: LE.le.trans, norm_sum_le
-- 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
x : E
n : ℕ
hn : 2 ≤ n + 1
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
r a C : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
hC : 0 ≤ C
hp : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ‖(↑i.symm : F →L[𝕜] E)‖
j : ℕ
h : j ∈ Ico 2 (n + 1)
bc :
  ∀ (i_1 : Composition j),
    Membership.mem (γ := Finset (Composition j)) (Set.toFinset {c : Composition j | 1 < c.length}) i_1 →
      ‖p.compAlongComposition (p.rightInv i x) i_1‖ ≤
        C * r ^ i_1.length *
          ∏ j_1 : Fin i_1.length,
            norm (E := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin (i_1.blocksFun j_1)) ↦ F) E)
              (p.rightInv i x (i_1.blocksFun j_1))
⊢ LE.le (α := ℝ)
    (∑ i_1 ∈ Set.toFinset {c : Composition j | 1 < c.length}, ‖p.compAlongComposition (p.rightInv i x) i_1‖)
    (∑ c ∈ Set.toFinset {c : Composition j | 1 < c.length},
      C * r ^ c.length *
        ∏ j_1 : Fin c.length,
          norm (E := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin (c.blocksFun j_1)) ↦ F) E)
            (p.rightInv i x (c.blocksFun j_1)))

Tactic:
gcongr
-- 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
x : E
n : ℕ
hn : 2 ≤ n + 1
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
r a C : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
hC : 0 ≤ C
hp : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ‖(↑i.symm : F →L[𝕜] E)‖
j : ℕ
h : j ∈ Ico 2 (n + 1)
i_1 : Composition j
h_1 : Membership.mem (γ := Finset (Composition j)) (Set.toFinset {c : Composition j | 1 < c.length}) i_1
bc :
  norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i_1.length) ↦ E) F) (p i_1.length) *
      ∏ i_2 : Fin i_1.length,
        norm (E := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin (i_1.blocksFun i_2)) ↦ F) E)
          (p.rightInv i x (i_1.blocksFun i_2)) ≤
    C * r ^ i_1.length *
      ∏ j_1 : Fin i_1.length,
        norm (E := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin (i_1.blocksFun j_1)) ↦ F) E)
          (p.rightInv i x (i_1.blocksFun j_1))
⊢ ‖p.compAlongComposition (p.rightInv i x) i_1‖ ≤
    C * r ^ i_1.length *
      ∏ j_1 : Fin i_1.length,
        norm (E := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin (i_1.blocksFun j_1)) ↦ F) E)
          (p.rightInv i x (i_1.blocksFun j_1))

Tactic:
apply (compAlongComposition_norm _ _ _).trans

Premises used: FormalMultilinearSeries.compAlongComposition_norm, LE.le.trans