awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
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
⊢ 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)
have 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)
Tactic: rw [K]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
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
⊢ 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)
have 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)
Tactic: try rw [K]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
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
⊢ 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))
have 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 : ℕ), sorry⟩ :
              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 : ℕ), sorry⟩ :
              Fin
                (compChangeOfVariables 2 (n + 1) n (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) H).snd (β :=
                    fun (n : ℕ) ↦ Composition n).length)))
Tactic: rw [Fin.heq_fun_iff K.symm]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
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
⊢ 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)))
have 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))
Tactic: rw [compChangeOfVariables_blocksFun]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
Goal:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
⊢ 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)
have 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)
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)))]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
Goal:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
⊢ 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)
have 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
Tactic: congr! with j
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
Goal:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
j : ℕ
h : 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
have 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
Tactic: simp only [← @MultilinearMap.mkPiAlgebra_apply ℝ (Fin j) _ ℝ]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
Goal:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
j : ℕ
h : j ∈ Ico 2 (n + 1)
⊢ (∑ 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
have 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
Tactic: simp only [←
        MultilinearMap.map_sum_finset (MultilinearMap.mkPiAlgebra ℝ (Fin j) ℝ) fun _ (m : ℕ) =>
          r * (a ^ m * p m)]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
Goal:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
j : ℕ
h : j ∈ Ico 2 (n + 1)
⊢ ((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
have 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
Tactic: simp only [MultilinearMap.mkPiAlgebra_apply]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
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)‖
⊢ 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))
have 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))
Tactic: congr! 2 with j hj
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
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)
⊢ 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))
have 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))
Tactic: rw [rightInv_coeff _ _ _ _ (mem_Ico.1 hj).1, norm_neg]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
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))
⊢ 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))
have 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))
Tactic: rw [rightInv_coeff _ _ _ _ (mem_Ico.1 hj).1, norm_neg]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
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)‖
⊢ 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)))
have 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))
Tactic: gcongr with j
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
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)
⊢ 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))
have 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))
Tactic: apply (ContinuousLinearMap.norm_compContinuousMultilinearMap_le _ _).trans
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
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.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))
have 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))
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
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)
⊢ 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))
have 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)))
Tactic: apply (norm_sum_le _ _).trans
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
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)
⊢ 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)))
have 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))
Tactic: gcongr